src/Extraction-prefix.hs

   1 {-# OPTIONS_GHC -fno-warn-unused-binds  #-}
   2 module CoqPass ( coqPassCoreToString, coqPassCoreToCore )
   3 where
   4 import qualified MkCore
   5 import qualified TysWiredIn
   6 import qualified TysPrim
   7 import qualified Outputable
   8 import qualified PrelNames
   9 import qualified Name
  10 import qualified Literal
  11 import qualified Type
  12 import qualified TypeRep
  13 import qualified DataCon
  14 import qualified TyCon
  15 import qualified Coercion
  16 import qualified Var
  17 import qualified Id
  18 import qualified FastString
  19 import qualified BasicTypes
  20 import qualified DataCon
  21 import qualified CoreSyn
  22 import qualified CoreUtils
  23 import qualified Class
  24 import qualified Data.Char
  25 import qualified Data.List
  26 import qualified Data.Ord
  27 import qualified Data.Typeable
  28 import Data.Bits ((.&.), shiftL, (.|.))
  29 import Prelude ( (++), (+), (==), Show, show, Char, (.) )
  30 import qualified Prelude
  31 import qualified GHC.Base
  32
  33 -- used for extracting strings
  34 bin2ascii =
  35   (\ b0 b1 b2 b3 b4 b5 b6 b7 ->
  36      let f b i = if b then 1 `shiftL` i else 0
  37      in Data.Char.chr (f b0 0 .|. f b1 1 .|. f b2 2 .|. f b3 3 .|. f b4 4 .|. f b5 5 .|. f b6 6 .|. f b7 7))
  38 --bin2ascii' =
  39 --  (\ f c -> let n = Char.code c in let h i = (n .&. (1 `shiftL` i)) /= 0 in f (h 0) (h 1) (h 2) (h 3) (h 4) (h 5) (h 6) (h 7))
  40 --shiftAscii =
  41 --  \ b c -> Data.Char.chr (((Char.code c) `shiftL` 1) .&. 255 .|. if b then 1 else 0)
  42
  43 -- crude way of casting Coq "error monad" into Haskell exceptions
  44 errOrFail :: OrError a -> a
  45 errOrFail (OK x)    = x
  46 errOrFail (Error s) = Prelude.error s
  47
  48 getTyConTyVars :: TyCon.TyCon -> [Var.TyVar]
  49 getTyConTyVars tc = if TyCon.isFunTyCon tc then [] else if TyCon.isPrimTyCon tc then [] else TyCon.tyConTyVars tc
  50
  51 sortAlts :: [(CoreSyn.AltCon,[Var.Var],CoreSyn.Expr Var.Var)] -> [(CoreSyn.AltCon,[Var.Var],CoreSyn.Expr Var.Var)]
  52 sortAlts x = Data.List.sortBy (\(a1,_,_) -> \(a2,_,_) -> Data.Ord.compare a1 a2) x
  53
  54 -- to do: this could be moved into Coq
  55 coreVarToWeakVar :: Var.Var -> WeakVar
  56 coreVarToWeakVar v | Id.isId     v = WExprVar (WeakExprVar v (errOrFail (coreTypeToWeakType (Var.varType v))))
  57 coreVarToWeakVar v | Var.isTyVar v = WTypeVar (WeakTypeVar v (coreKindToKind (Var.varType v)))
  58 coreVarToWeakVar v | Var.isCoVar v = WCoerVar (WeakCoerVar v (Prelude.error "FIXME")
  59                                                              (Prelude.error "FIXME") (Prelude.error "FIXME"))
  60 coreVarToWeakVar _                 =
  61    Prelude.error "Var.Var that is neither an expression variable, type variable, nor coercion variable!"
  62
  63 tyConOrTyFun :: TyCon.TyCon -> Prelude.Either TyCon.TyCon TyCon.TyCon
  64 --FIXME: go back to this
  65 --tyConOrTyFun n = if TyCon.isFamInstTyCon n then Prelude.Left n else Prelude.Right n
  66 tyConOrTyFun n = if TyCon.isFamInstTyCon n then Prelude.Left n else Prelude.Left n
  67
  68 tyFunResultKind :: TyCon.TyCon -> Kind
  69 tyFunResultKind tc = coreKindToKind (TyCon.tyConKind tc)
  70
  71 nat2int :: Nat -> Prelude.Int
  72 nat2int O     = 0
  73 nat2int (S x) = 1 + (nat2int x)
  74
  75 natToString :: Nat -> Prelude.String
  76 natToString n = show (nat2int n)
  77
  78 -- only needs to sanitize characters which might appear in Haskell identifiers
  79 sanitizeForLatex :: Prelude.String -> Prelude.String
  80 sanitizeForLatex []    = []
  81 sanitizeForLatex ('_':x) = "\\_"++(sanitizeForLatex x)
  82 sanitizeForLatex ('$':x) = "\\$"++(sanitizeForLatex x)
  83 sanitizeForLatex ('#':x) = "\\#"++(sanitizeForLatex x)
  84 sanitizeForLatex (c:x) = c:(sanitizeForLatex x)
  85
  86 coreKindToKind :: TypeRep.Kind -> Kind
  87 coreKindToKind k =
  88   case Coercion.splitKindFunTy_maybe k of
  89       Prelude.Just (k1,k2) -> KindTypeFunction (coreKindToKind k1) (coreKindToKind k2)
  90       Prelude.Nothing ->
  91                       if (Coercion.isLiftedTypeKind k)   then KindType
  92                  else if (Coercion.isUnliftedTypeKind k) then KindUnliftedType
  93                  else if (Coercion.isOpenTypeKind k)     then KindOpenType
  94                  else if (Coercion.isArgTypeKind k)      then KindArgType
  95                  else if (Coercion.isUbxTupleKind k)     then KindUnboxedTuple
  96                  else if (Coercion.isTySuperKind k)      then Prelude.error "coreKindToKind got the kind-of-the-kind-of-types"
  97                  else if (Coercion.isCoSuperKind k)      then Prelude.error "coreKindToKind got the kind-of-the-kind-of-coercions"
  98                  else                                         Prelude.error ((Prelude.++) "coreKindToKind got an unknown kind: "
  99                                                                                (Outputable.showSDoc (Outputable.ppr k)))
 100 outputableToString :: Outputable.Outputable a => a -> Prelude.String
 101 outputableToString = (\x -> Outputable.showSDoc (Outputable.ppr x))
 102
 103 -- TO DO: I think we can remove this now
 104 checkTypeEquality :: Type.Type -> Type.Type -> Prelude.Bool
 105 checkTypeEquality t1 t2 = Type.tcEqType (Type.expandTypeSynonyms t1) (Type.expandTypeSynonyms t2)
 106
 107 --showType t = outputableToString (Type.expandTypeSynonyms t)
 108 showType t = outputableToString (coreViewDeep t)
 109
 110 coreViewDeep :: Type.Type -> Type.Type
 111 coreViewDeep t =
 112     case t of
 113       TypeRep.TyVarTy tv       -> TypeRep.TyVarTy tv
 114       TypeRep.FunTy arg res    -> TypeRep.FunTy (coreViewDeep arg) (coreViewDeep res)
 115       TypeRep.AppTy fun arg    -> TypeRep.AppTy (coreViewDeep fun) (coreViewDeep arg)
 116       TypeRep.ForAllTy fun arg -> TypeRep.ForAllTy fun (coreViewDeep arg)
 117       TypeRep.TyConApp tc tys  -> let t' = TypeRep.TyConApp tc (Prelude.map coreViewDeep tys)
 118                         in case Type.coreView t' of
 119                                Prelude.Nothing     -> t'
 120                                Prelude.Just    t'' -> t''
 121       TypeRep.PredTy p         -> case Type.coreView t of
 122                                Prelude.Nothing     -> TypeRep.PredTy p
 123                                Prelude.Just    t'  -> t'
 124
 125 -- FIXME: cotycon applications may be oversaturated
 126 coreCoercionToWeakCoercion :: Type.Type -> WeakCoercion
 127 coreCoercionToWeakCoercion c =
 128  case c of
 129   TypeRep.TyVarTy  v     -> WCoVar (WeakCoerVar v (Prelude.error "FIXME") (Prelude.error "FIXME") (Prelude.error "FIXME"))
 130   TypeRep.AppTy    t1 t2 -> WCoApp   (coreCoercionToWeakCoercion t1) (coreCoercionToWeakCoercion t2)
 131   TypeRep.TyConApp tc t  ->
 132       case TyCon.isCoercionTyCon_maybe tc of
 133         Prelude.Nothing -> Prelude.error ((Prelude.++) "coreCoercionToWeakCoercion got " (outputableToString c))
 134         Prelude.Just (_, ctcd) ->
 135             case (ctcd,t) of
 136               (TyCon.CoTrans , [x,y]     ) -> WCoComp   (coreCoercionToWeakCoercion x) (coreCoercionToWeakCoercion y)
 137               (TyCon.CoSym   , [x]       ) -> WCoSym    (coreCoercionToWeakCoercion x)
 138               (TyCon.CoLeft  , [x]       ) -> WCoLeft   (coreCoercionToWeakCoercion x)
 139               (TyCon.CoRight , [x]       ) -> WCoLeft   (coreCoercionToWeakCoercion x)
 140 -- FIXME      (TyCon.CoUnsafe, [t1, t2 ] ) -> WCoUnsafe (coreTypeToWeakType t1) (coreTypeToWeakType t2)
 141               (TyCon.CoTrans , []        ) -> Prelude.error "CoTrans is not in post-publication-appendix SystemFC1"
 142               (TyCon.CoCsel1 , []        ) -> Prelude.error "CoCsel1 is not in post-publication-appendix SystemFC1"
 143               (TyCon.CoCsel2 , []        ) -> Prelude.error "CoCsel2 is not in post-publication-appendix SystemFC1"
 144               (TyCon.CoCselR , []        ) -> Prelude.error "CoCselR is not in post-publication-appendix SystemFC1"
 145               (TyCon.CoInst  , []        ) -> Prelude.error "CoInst  is not in post-publication-appendix SystemFC1"
 146 --              (TyCon.CoAxiom , []        ) -> Prelude.error "CoAxiom is not yet implemented (FIXME)"
 147               _ -> Prelude.error ((Prelude.++) "coreCoercionToWeakCoercion got " (outputableToString c))
 148   _ -> Prelude.error ((Prelude.++) "coreCoercionToWeakCoercion got " (outputableToString c))
 149 --  TypeRep.ForAllTy v t   -> WCoAll  (Prelude.error "FIXME") (coreTypeToWeakType t)
 150 -- FIXME   x y                                  -> WCoAppT    (coreCoercionToWeakCoercion x) (coreCoercionToWeakType y)
 151 --  CoreSyn.Type t                            -> WCoType   (coreTypeToWeakType t)
 152
 153 {-
 154 weakCoercionToCoreCoercion :: CoreCoercion -> Type.Type
 155 | WCoVar     (weakCoerVar _ _ t1 t2) => (t1,t2)
 156 | WCoType    t                       => Prelude_error "FIXME WCoType"
 157 | WCoApp     c1 c2                   => Prelude_error "FIXME WCoApp"
 158 | WCoAppT    c t                     => Prelude_error "FIXME WCoAppT"
 159 | WCoAll     k f                     => Prelude_error "FIXME WCoAll"
 160 | WCoSym     c                       => let (t2,t1) := weakCoercionTypes c in (t1,t2)
 161 | WCoComp    c1 c2                   => Prelude_error "FIXME WCoComp"
 162 | WCoLeft    c                       => Prelude_error "FIXME WCoLeft"
 163 | WCoRight   c                       => Prelude_error "FIXME WCoRight"
 164 | WCoUnsafe  t1 t2                   => (t1,t2)
 165 -}