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