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.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
33 -- used for extracting strings
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))
39 getTyConTyVars :: TyCon.TyCon -> [Var.TyVar]
41 if TyCon.isFunTyCon tc
43 else if TyCon.isPrimTyCon tc
45 else TyCon.tyConTyVars tc
47 sortAlts :: [(CoreSyn.AltCon,[Var.Var],CoreSyn.Expr Var.Var)] -> [(CoreSyn.AltCon,[Var.Var],CoreSyn.Expr Var.Var)]
48 sortAlts x = Data.List.sortBy (\(a1,_,_) -> \(a2,_,_) -> Data.Ord.compare a1 a2) x
50 -- to do: this could be moved into Coq
51 coreVarToWeakVar :: Var.Var -> WeakVar
52 coreVarToWeakVar v | Id.isId v = WExprVar (WeakExprVar v (errOrFail (coreTypeToWeakType (Var.varType v))))
55 errOrFail (Error s) = Prelude.error s
56 coreVarToWeakVar v | Var.isTyVar v = WTypeVar (WeakTypeVar v (coreKindToKind (Var.varType v)))
57 coreVarToWeakVar v | Var.isCoVar v = WCoerVar (WeakCoerVar v (Prelude.error "FIXME")
58 (Prelude.error "FIXME") (Prelude.error "FIXME"))
60 Prelude.error "Var.Var that is neither an expression variable, type variable, nor coercion variable!"
62 tyConOrTyFun :: TyCon.TyCon -> Prelude.Either TyCon.TyCon TyCon.TyCon
64 if n == TysPrim.statePrimTyCon -- special-purpose hack treat State# as a type family since it has kind *->* but no tyvars
66 else if TyCon.isFamInstTyCon n
70 nat2int :: Nat -> Prelude.Int
72 nat2int (S x) = 1 + (nat2int x)
74 natToString :: Nat -> Prelude.String
75 natToString n = show (nat2int n)
77 -- only needs to sanitize characters which might appear in Haskell identifiers
78 sanitizeForLatex :: Prelude.String -> Prelude.String
79 sanitizeForLatex [] = []
80 sanitizeForLatex ('_':x) = "\\_"++(sanitizeForLatex x)
81 sanitizeForLatex ('$':x) = "\\$"++(sanitizeForLatex x)
82 sanitizeForLatex ('#':x) = "\\#"++(sanitizeForLatex x)
83 sanitizeForLatex (c:x) = c:(sanitizeForLatex x)
85 coreKindToKind :: TypeRep.Kind -> Kind
87 case Coercion.splitKindFunTy_maybe k of
88 Prelude.Just (k1,k2) -> KindArrow (coreKindToKind k1) (coreKindToKind k2)
90 if (Coercion.isLiftedTypeKind k) then KindStar
91 else if (Coercion.isUnliftedTypeKind k) then KindStar
92 else if (Coercion.isArgTypeKind k) then KindStar
93 else if (Coercion.isUbxTupleKind k) then KindStar
94 else if (Coercion.isOpenTypeKind k) then KindStar
95 -- else if (Coercion.isUnliftedTypeKind k) then KindUnliftedType
96 -- else if (Coercion.isOpenTypeKind k) then KindOpenType
97 -- else if (Coercion.isArgTypeKind k) then KindArgType
98 -- else if (Coercion.isUbxTupleKind k) then KindUnboxedTuple
99 else if (Coercion.isTySuperKind k) then Prelude.error "coreKindToKind got the kind-of-the-kind-of-types"
100 else if (Coercion.isCoSuperKind k) then Prelude.error "coreKindToKind got the kind-of-the-kind-of-coercions"
101 else Prelude.error ((Prelude.++) "coreKindToKind got an unknown kind: "
102 (Outputable.showSDoc (Outputable.ppr k)))
103 outputableToString :: Outputable.Outputable a => a -> Prelude.String
104 outputableToString = (\x -> Outputable.showSDoc (Outputable.ppr x))
106 -- I'm leaving this here (commented out) in case I ever need it again)
107 --checkTypeEquality :: Type.Type -> Type.Type -> Prelude.Bool
108 --checkTypeEquality t1 t2 = Type.tcEqType (Type.expandTypeSynonyms t1) (Type.expandTypeSynonyms t2)
110 coreViewDeep :: Type.Type -> Type.Type
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'
125 -- FIXME: cotycon applications may be oversaturated
126 coreCoercionToWeakCoercion :: Type.Type -> WeakCoercion
127 coreCoercionToWeakCoercion c =
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) ->
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)
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)