1 {-# OPTIONS_GHC -fno-warn-unused-binds #-}
2 module CoqPass ( coqPassCoreToString, coqPassCoreToCore )
4 import qualified Unique
5 import qualified UniqSupply
6 import qualified MkCore
7 import qualified TysWiredIn
8 import qualified TysPrim
9 import qualified Outputable
10 import qualified PrelNames
11 import qualified OccName
13 import qualified Literal
15 import qualified TypeRep
16 import qualified DataCon
17 import qualified TyCon
18 import qualified Coercion
21 import qualified FastString
22 import qualified BasicTypes
23 import qualified DataCon
24 import qualified CoreSyn
25 import qualified CoreUtils
26 import qualified Class
27 import qualified Data.Char
28 import qualified Data.List
29 import qualified Data.Ord
30 import qualified Data.Typeable
31 import Data.Bits ((.&.), shiftL, (.|.))
32 import Prelude ( (++), (+), (==), Show, show, Char, (.) )
33 import qualified Prelude
34 import qualified GHC.Base
36 -- used for extracting strings
38 (\ b0 b1 b2 b3 b4 b5 b6 b7 ->
39 let f b i = if b then 1 `shiftL` i else 0
40 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))
42 getTyConTyVars :: TyCon.TyCon -> [Var.TyVar]
44 if TyCon.isFunTyCon tc
46 else if TyCon.isPrimTyCon tc
48 else TyCon.tyConTyVars tc
50 cmpAlts :: (CoreSyn.AltCon,[Var.Var],CoreSyn.Expr Var.Var) -> (CoreSyn.AltCon,[Var.Var],CoreSyn.Expr Var.Var) -> Data.Ord.Ordering
51 cmpAlts (CoreSyn.DEFAULT,_,_) _ = Data.Ord.LT
52 cmpAlts _ (CoreSyn.DEFAULT,_,_) = Data.Ord.GT
53 cmpAlts (a1,_,_) (a2,_,_) = Data.Ord.compare a2 a1
55 sortAlts :: [(CoreSyn.AltCon,[Var.Var],CoreSyn.Expr Var.Var)] -> [(CoreSyn.AltCon,[Var.Var],CoreSyn.Expr Var.Var)]
56 sortAlts x = Data.List.sortBy (\a b -> if a `CoreSyn.ltAlt` b then Data.Ord.LT else Data.Ord.GT) x
58 -- to do: this could be moved into Coq
59 coreVarToWeakVar :: Var.Var -> WeakVar
60 coreVarToWeakVar v | Id.isId v = WExprVar (WeakExprVar v (errOrFail (coreTypeToWeakType (Var.varType v))))
63 errOrFail (Error s) = Prelude.error s
64 coreVarToWeakVar v | Var.isTyVar v = WTypeVar (WeakTypeVar v (coreKindToKind (Var.varType v)))
65 coreVarToWeakVar v | Var.isCoVar v = WCoerVar (WeakCoerVar v (Prelude.error "FIXME")
66 (Prelude.error "FIXME") (Prelude.error "FIXME"))
68 Prelude.error "Var.Var that is neither an expression variable, type variable, nor coercion variable!"
70 tyConOrTyFun :: TyCon.TyCon -> Prelude.Either TyCon.TyCon TyCon.TyCon
72 if n == TysPrim.statePrimTyCon -- special-purpose hack treat State# as a type family since it has kind *->* but no tyvars
74 else if TyCon.isFamInstTyCon n
78 nat2int :: Nat -> Prelude.Int
80 nat2int (S x) = 1 + (nat2int x)
82 natToString :: Nat -> Prelude.String
83 natToString n = show (nat2int n)
85 -- only needs to sanitize characters which might appear in Haskell identifiers
86 sanitizeForLatex :: Prelude.String -> Prelude.String
87 sanitizeForLatex [] = []
88 sanitizeForLatex ('_':x) = "\\_"++(sanitizeForLatex x)
89 sanitizeForLatex ('$':x) = "\\$"++(sanitizeForLatex x)
90 sanitizeForLatex ('#':x) = "\\#"++(sanitizeForLatex x)
91 sanitizeForLatex (c:x) = c:(sanitizeForLatex x)
93 kindToCoreKind :: Kind -> TypeRep.Kind
94 kindToCoreKind KindStar = TypeRep.liftedTypeKind
95 kindToCoreKind (KindArrow k1 k2) = Coercion.mkArrowKind (kindToCoreKind k1) (kindToCoreKind k2)
96 kindToCoreKind _ = Prelude.error "kindToCoreKind does not know how to handle that"
98 coreKindToKind :: TypeRep.Kind -> Kind
100 case Coercion.splitKindFunTy_maybe k of
101 Prelude.Just (k1,k2) -> KindArrow (coreKindToKind k1) (coreKindToKind k2)
103 if (Coercion.isLiftedTypeKind k) then KindStar
104 else if (Coercion.isUnliftedTypeKind k) then KindStar
105 else if (Coercion.isArgTypeKind k) then KindStar
106 else if (Coercion.isUbxTupleKind k) then KindStar
107 else if (Coercion.isOpenTypeKind k) then KindStar
108 -- else if (Coercion.isUnliftedTypeKind k) then KindUnliftedType
109 -- else if (Coercion.isOpenTypeKind k) then KindOpenType
110 -- else if (Coercion.isArgTypeKind k) then KindArgType
111 -- else if (Coercion.isUbxTupleKind k) then KindUnboxedTuple
112 else if (Coercion.isTySuperKind k) then Prelude.error "coreKindToKind got the kind-of-the-kind-of-types"
113 else if (Coercion.isCoSuperKind k) then Prelude.error "coreKindToKind got the kind-of-the-kind-of-coercions"
114 else Prelude.error ((Prelude.++) "coreKindToKind got an unknown kind: "
115 (Outputable.showSDoc (Outputable.ppr k)))
116 outputableToString :: Outputable.Outputable a => a -> Prelude.String
117 outputableToString = (\x -> Outputable.showSDoc (Outputable.ppr x))
119 -- I'm leaving this here (commented out) in case I ever need it again)
120 --checkTypeEquality :: Type.Type -> Type.Type -> Prelude.Bool
121 --checkTypeEquality t1 t2 = Type.tcEqType (Type.expandTypeSynonyms t1) (Type.expandTypeSynonyms t2)
123 coreViewDeep :: Type.Type -> Type.Type
126 TypeRep.TyVarTy tv -> TypeRep.TyVarTy tv
127 TypeRep.FunTy arg res -> TypeRep.FunTy (coreViewDeep arg) (coreViewDeep res)
128 TypeRep.AppTy fun arg -> TypeRep.AppTy (coreViewDeep fun) (coreViewDeep arg)
129 TypeRep.ForAllTy fun arg -> TypeRep.ForAllTy fun (coreViewDeep arg)
130 TypeRep.TyConApp tc tys -> let t' = TypeRep.TyConApp tc (Prelude.map coreViewDeep tys)
131 in case Type.coreView t' of
132 Prelude.Nothing -> t'
133 Prelude.Just t'' -> t''
134 TypeRep.PredTy p -> case Type.coreView t of
135 Prelude.Nothing -> TypeRep.PredTy p
136 Prelude.Just t' -> t'
138 -- FIXME: cotycon applications may be oversaturated
139 coreCoercionToWeakCoercion :: Type.Type -> WeakCoercion
140 coreCoercionToWeakCoercion c =
142 TypeRep.TyVarTy v -> WCoVar (WeakCoerVar v (Prelude.error "FIXME") (Prelude.error "FIXME") (Prelude.error "FIXME"))
143 TypeRep.AppTy t1 t2 -> WCoApp (coreCoercionToWeakCoercion t1) (coreCoercionToWeakCoercion t2)
144 TypeRep.TyConApp tc t ->
145 case TyCon.isCoercionTyCon_maybe tc of
146 Prelude.Nothing -> Prelude.error ((Prelude.++) "coreCoercionToWeakCoercion got " (outputableToString c))
147 Prelude.Just (_, ctcd) ->
149 (TyCon.CoTrans , [x,y] ) -> WCoComp (coreCoercionToWeakCoercion x) (coreCoercionToWeakCoercion y)
150 (TyCon.CoSym , [x] ) -> WCoSym (coreCoercionToWeakCoercion x)
151 (TyCon.CoLeft , [x] ) -> WCoLeft (coreCoercionToWeakCoercion x)
152 (TyCon.CoRight , [x] ) -> WCoLeft (coreCoercionToWeakCoercion x)
153 -- FIXME (TyCon.CoUnsafe, [t1, t2 ] ) -> WCoUnsafe (coreTypeToWeakType t1) (coreTypeToWeakType t2)
154 (TyCon.CoTrans , [] ) -> Prelude.error "CoTrans is not in post-publication-appendix SystemFC1"
155 (TyCon.CoCsel1 , [] ) -> Prelude.error "CoCsel1 is not in post-publication-appendix SystemFC1"
156 (TyCon.CoCsel2 , [] ) -> Prelude.error "CoCsel2 is not in post-publication-appendix SystemFC1"
157 (TyCon.CoCselR , [] ) -> Prelude.error "CoCselR is not in post-publication-appendix SystemFC1"
158 (TyCon.CoInst , [] ) -> Prelude.error "CoInst is not in post-publication-appendix SystemFC1"
159 -- (TyCon.CoAxiom , [] ) -> Prelude.error "CoAxiom is not yet implemented (FIXME)"
160 _ -> Prelude.error ((Prelude.++) "coreCoercionToWeakCoercion got " (outputableToString c))
161 _ -> Prelude.error ((Prelude.++) "coreCoercionToWeakCoercion got " (outputableToString c))
162 -- TypeRep.ForAllTy v t -> WCoAll (Prelude.error "FIXME") (coreTypeToWeakType t)
163 -- FIXME x y -> WCoAppT (coreCoercionToWeakCoercion x) (coreCoercionToWeakType y)
164 -- CoreSyn.Type t -> WCoType (coreTypeToWeakType t)
167 weakCoercionToCoreCoercion :: CoreCoercion -> Type.Type
168 | WCoVar (weakCoerVar _ _ t1 t2) => (t1,t2)
169 | WCoType t => Prelude_error "FIXME WCoType"
170 | WCoApp c1 c2 => Prelude_error "FIXME WCoApp"
171 | WCoAppT c t => Prelude_error "FIXME WCoAppT"
172 | WCoAll k f => Prelude_error "FIXME WCoAll"
173 | WCoSym c => let (t2,t1) := weakCoercionTypes c in (t1,t2)
174 | WCoComp c1 c2 => Prelude_error "FIXME WCoComp"
175 | WCoLeft c => Prelude_error "FIXME WCoLeft"
176 | WCoRight c => Prelude_error "FIXME WCoRight"
177 | WCoUnsafe t1 t2 => (t1,t2)