1 module CoqPass ( coqPassCoreToString, coqPassCoreToCore )
3 import qualified Unique
4 import qualified UniqSupply
5 import qualified MkCore
6 import qualified TysWiredIn
7 import qualified TysPrim
8 import qualified Outputable
9 import qualified PrelNames
10 import qualified OccName
12 import qualified Literal
14 import qualified TypeRep
15 import qualified DataCon
16 import qualified TyCon
17 import qualified Coercion
20 import qualified FastString
21 import qualified BasicTypes
22 import qualified DataCon
23 import qualified CoreSyn
24 import qualified CoreUtils
25 import qualified Class
26 import qualified Data.Char
27 import qualified Data.List
28 import qualified Data.Ord
29 import qualified Data.Typeable
30 import Data.Bits ((.&.), shiftL, (.|.))
31 import Prelude ( (++), (+), (==), Show, show, Char, (.), ($) )
32 import qualified Prelude
33 import qualified Debug.Trace
34 import qualified GHC.Base
35 import qualified System.IO
36 import qualified System.IO.Unsafe
38 getTyConTyVars :: TyCon.TyCon -> [Var.TyVar]
40 if TyCon.isFunTyCon tc
42 else if TyCon.isPrimTyCon tc
44 else TyCon.tyConTyVars tc
46 cmpAlts :: (CoreSyn.AltCon,[Var.Var],CoreSyn.Expr Var.Var) -> (CoreSyn.AltCon,[Var.Var],CoreSyn.Expr Var.Var) -> Data.Ord.Ordering
47 cmpAlts (CoreSyn.DEFAULT,_,_) _ = Data.Ord.LT
48 cmpAlts _ (CoreSyn.DEFAULT,_,_) = Data.Ord.GT
49 cmpAlts (a1,_,_) (a2,_,_) = Data.Ord.compare a2 a1
51 sortAlts :: [(CoreSyn.AltCon,[Var.Var],CoreSyn.Expr Var.Var)] -> [(CoreSyn.AltCon,[Var.Var],CoreSyn.Expr Var.Var)]
52 sortAlts x = Data.List.sortBy (\a b -> if a `CoreSyn.ltAlt` b then Data.Ord.LT else Data.Ord.GT) x
54 coreVarToWeakVar :: Var.Var -> WeakVar
55 coreVarToWeakVar v | Id.isId v = WExprVar (WeakExprVar v (errOrFail (coreTypeToWeakType (Var.varType v))))
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!"
63 errOrFail (Error s) = Prelude.error s
65 tyConOrTyFun :: TyCon.TyCon -> Prelude.Either TyCon.TyCon TyCon.TyCon
67 if n == TysPrim.statePrimTyCon -- special-purpose hack treat State# as a type family since it has kind *->* but no tyvars
69 else if TyCon.isFamInstTyCon n
73 nat2int :: Nat -> Prelude.Int
75 nat2int (S x) = 1 + (nat2int x)
77 natToString :: Nat -> Prelude.String
78 natToString n = show (nat2int n)
80 sanitizeForLatex :: Prelude.String -> Prelude.String
81 sanitizeForLatex [] = []
82 sanitizeForLatex ('_':x) = "\\_"++(sanitizeForLatex x)
83 sanitizeForLatex ('$':x) = "\\$"++(sanitizeForLatex x)
84 sanitizeForLatex ('#':x) = "\\#"++(sanitizeForLatex x)
85 sanitizeForLatex (c:x) = c:(sanitizeForLatex x)
87 kindToCoreKind :: Kind -> TypeRep.Kind
88 kindToCoreKind KindStar = TypeRep.liftedTypeKind
89 kindToCoreKind (KindArrow k1 k2) = Coercion.mkArrowKind (kindToCoreKind k1) (kindToCoreKind k2)
90 kindToCoreKind _ = Prelude.error "kindToCoreKind does not know how to handle that"
92 coreKindToKind :: TypeRep.Kind -> Kind
94 case Coercion.splitKindFunTy_maybe k of
95 Prelude.Just (k1,k2) -> KindArrow (coreKindToKind k1) (coreKindToKind k2)
97 if (Coercion.isLiftedTypeKind k) then KindStar
98 else if (Coercion.isUnliftedTypeKind k) then KindStar
99 else if (Coercion.isArgTypeKind k) then KindStar
100 else if (Coercion.isUbxTupleKind k) then KindStar
101 else if (Coercion.isOpenTypeKind k) then KindStar
103 -- The "subkinding" in GHC is not dealt with in System FC, and dealing
104 -- with it is not actually as simple as you'd think.
106 -- else if (Coercion.isUnliftedTypeKind k) then KindUnliftedType
107 -- else if (Coercion.isOpenTypeKind k) then KindOpenType
108 -- else if (Coercion.isArgTypeKind k) then KindArgType
109 -- else if (Coercion.isUbxTupleKind k) then KindUnboxedTuple
111 else if (Coercion.isTySuperKind k) then Prelude.error "coreKindToKind got the kind-of-the-kind-of-types"
112 else if (Coercion.isCoSuperKind k) then Prelude.error "coreKindToKind got the kind-of-the-kind-of-coercions"
113 else Prelude.error ((Prelude.++) "coreKindToKind got an unknown kind: "
114 (Outputable.showSDoc (Outputable.ppr k)))
115 outputableToString :: Outputable.Outputable a => a -> Prelude.String
116 outputableToString = (\x -> Outputable.showSDoc (Outputable.ppr x))
118 coreViewDeep :: Type.Type -> Type.Type
121 TypeRep.TyVarTy tv -> TypeRep.TyVarTy tv
122 TypeRep.FunTy arg res -> TypeRep.FunTy (coreViewDeep arg) (coreViewDeep res)
123 TypeRep.AppTy fun arg -> TypeRep.AppTy (coreViewDeep fun) (coreViewDeep arg)
124 TypeRep.ForAllTy fun arg -> TypeRep.ForAllTy fun (coreViewDeep arg)
125 TypeRep.TyConApp tc tys -> let t' = TypeRep.TyConApp tc (Prelude.map coreViewDeep tys)
126 in case Type.coreView t' of
127 Prelude.Nothing -> t'
128 Prelude.Just t'' -> t''
129 TypeRep.PredTy p -> case Type.coreView t of
130 Prelude.Nothing -> TypeRep.PredTy p
131 Prelude.Just t' -> t'
133 coreCoercionToWeakCoercion :: Type.Type -> WeakCoercion
134 coreCoercionToWeakCoercion c =
135 WCoUnsafe (errOrFail (coreTypeToWeakType t1)) (errOrFail (coreTypeToWeakType t2))
137 (t1,t2) = Coercion.coercionKind c
139 -- REMEMBER: cotycon applications may be oversaturated
141 TypeRep.TyVarTy v -> WCoVar (WeakCoerVar v (Prelude.error "FIXME") (Prelude.error "FIXME") (Prelude.error "FIXME"))
142 TypeRep.AppTy t1 t2 -> WCoApp (coreCoercionToWeakCoercion t1) (coreCoercionToWeakCoercion t2)
143 TypeRep.TyConApp tc t ->
144 case TyCon.isCoercionTyCon_maybe tc of
145 Prelude.Nothing -> Prelude.error ((Prelude.++) "coreCoercionToWeakCoercion got isCoercionTyCon_maybe " (outputableToString c))
146 Prelude.Just (_, ctcd) ->
148 (TyCon.CoTrans , [x,y] ) -> WCoComp (coreCoercionToWeakCoercion x) (coreCoercionToWeakCoercion y)
149 (TyCon.CoSym , [x] ) -> WCoSym (coreCoercionToWeakCoercion x)
150 (TyCon.CoLeft , [x] ) -> WCoLeft (coreCoercionToWeakCoercion x)
151 (TyCon.CoRight , [x] ) -> WCoLeft (coreCoercionToWeakCoercion x)
152 -- (TyCon.CoUnsafe, [t1, t2 ] ) -> WCoUnsafe (coreTypeToWeakType t1) (coreTypeToWeakType t2)
153 (TyCon.CoTrans , [] ) -> Prelude.error "CoTrans is not in post-publication-appendix SystemFC1"
154 (TyCon.CoCsel1 , [] ) -> Prelude.error "CoCsel1 is not in post-publication-appendix SystemFC1"
155 (TyCon.CoCsel2 , [] ) -> Prelude.error "CoCsel2 is not in post-publication-appendix SystemFC1"
156 (TyCon.CoCselR , [] ) -> Prelude.error "CoCselR is not in post-publication-appendix SystemFC1"
157 (TyCon.CoInst , [] ) -> Prelude.error "CoInst is not in post-publication-appendix SystemFC1"
158 (TyCon.CoAxiom _ _ _ , _ ) -> Prelude.error "CoAxiom is not yet implemented (FIXME)"
159 ( _, [ t1 , t2 ]) -> WCoUnsafe (errOrFail (coreTypeToWeakType t1)) (errOrFail (coreTypeToWeakType t2))
160 _ -> Prelude.error ((Prelude.++) "coreCoercionToWeakCoercion got " (outputableToString c))
161 _ -> Prelude.error ((Prelude.++) "coreCoercionToWeakCoercion got " (outputableToString c))
163 -- TypeRep.ForAllTy v t -> WCoAll (Prelude.error "FIXME") (coreTypeToWeakType t)
164 -- FIXME x y -> WCoAppT (coreCoercionToWeakCoercion x) (coreCoercionToWeakType y)
165 -- CoreSyn.Type t -> WCoType (coreTypeToWeakType t)
168 weakCoercionToCoreCoercion :: CoreCoercion -> Type.Type
169 | WCoVar (weakCoerVar _ _ t1 t2) => (t1,t2)
170 | WCoType t => Prelude_error "FIXME WCoType"
171 | WCoApp c1 c2 => Prelude_error "FIXME WCoApp"
172 | WCoAppT c t => Prelude_error "FIXME WCoAppT"
173 | WCoAll k f => Prelude_error "FIXME WCoAll"
174 | WCoSym c => let (t2,t1) := weakCoercionTypes c in (t1,t2)
175 | WCoComp c1 c2 => Prelude_error "FIXME WCoComp"
176 | WCoLeft c => Prelude_error "FIXME WCoLeft"
177 | WCoRight c => Prelude_error "FIXME WCoRight"
178 | WCoUnsafe t1 t2 => (t1,t2)
182 --trace = Debug.Trace.trace
184 trace msg x = System.IO.Unsafe.unsafePerformIO $ Prelude.return x
187 trace msg x = System.IO.Unsafe.unsafePerformIO $
188 (Prelude.>>=) (System.IO.hPutStrLn System.IO.stdout msg) (\_ -> Prelude.return x)
189 trace msg x = System.IO.Unsafe.unsafePerformIO $
190 (Prelude.>>=) (System.IO.hPutStr System.IO.stdout " ") (\_ -> Prelude.return x)
193 {- -- used for extracting strings WITHOUT the patch for Coq
195 (\ b0 b1 b2 b3 b4 b5 b6 b7 ->
196 let f b i = if b then 1 `shiftL` i else 0
197 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))
200 -- I'm leaving this here (commented out) in case I ever need it again)
201 --checkTypeEquality :: Type.Type -> Type.Type -> Prelude.Bool
202 --checkTypeEquality t1 t2 = Type.tcEqType (Type.expandTypeSynonyms t1) (Type.expandTypeSynonyms t2)