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 {- -- used for extracting strings WITHOUT the patch for Coq
40 (\ b0 b1 b2 b3 b4 b5 b6 b7 ->
41 let f b i = if b then 1 `shiftL` i else 0
42 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))
45 getTyConTyVars :: TyCon.TyCon -> [Var.TyVar]
47 if TyCon.isFunTyCon tc
49 else if TyCon.isPrimTyCon tc
51 else TyCon.tyConTyVars tc
53 cmpAlts :: (CoreSyn.AltCon,[Var.Var],CoreSyn.Expr Var.Var) -> (CoreSyn.AltCon,[Var.Var],CoreSyn.Expr Var.Var) -> Data.Ord.Ordering
54 cmpAlts (CoreSyn.DEFAULT,_,_) _ = Data.Ord.LT
55 cmpAlts _ (CoreSyn.DEFAULT,_,_) = Data.Ord.GT
56 cmpAlts (a1,_,_) (a2,_,_) = Data.Ord.compare a2 a1
58 sortAlts :: [(CoreSyn.AltCon,[Var.Var],CoreSyn.Expr Var.Var)] -> [(CoreSyn.AltCon,[Var.Var],CoreSyn.Expr Var.Var)]
59 sortAlts x = Data.List.sortBy (\a b -> if a `CoreSyn.ltAlt` b then Data.Ord.LT else Data.Ord.GT) x
61 -- to do: this could be moved into Coq
62 coreVarToWeakVar :: Var.Var -> WeakVar
63 coreVarToWeakVar v | Id.isId v = WExprVar (WeakExprVar v (errOrFail (coreTypeToWeakType (Var.varType v))))
66 errOrFail (Error s) = Prelude.error s
67 coreVarToWeakVar v | Var.isTyVar v = WTypeVar (WeakTypeVar v (coreKindToKind (Var.varType v)))
68 coreVarToWeakVar v | Var.isCoVar v = WCoerVar (WeakCoerVar v (Prelude.error "FIXME")
69 (Prelude.error "FIXME") (Prelude.error "FIXME"))
71 Prelude.error "Var.Var that is neither an expression variable, type variable, nor coercion variable!"
73 tyConOrTyFun :: TyCon.TyCon -> Prelude.Either TyCon.TyCon TyCon.TyCon
75 if n == TysPrim.statePrimTyCon -- special-purpose hack treat State# as a type family since it has kind *->* but no tyvars
77 else if TyCon.isFamInstTyCon n
81 nat2int :: Nat -> Prelude.Int
83 nat2int (S x) = 1 + (nat2int x)
85 natToString :: Nat -> Prelude.String
86 natToString n = show (nat2int n)
88 -- only needs to sanitize characters which might appear in Haskell identifiers
89 sanitizeForLatex :: Prelude.String -> Prelude.String
90 sanitizeForLatex [] = []
91 sanitizeForLatex ('_':x) = "\\_"++(sanitizeForLatex x)
92 sanitizeForLatex ('$':x) = "\\$"++(sanitizeForLatex x)
93 sanitizeForLatex ('#':x) = "\\#"++(sanitizeForLatex x)
94 sanitizeForLatex (c:x) = c:(sanitizeForLatex x)
96 kindToCoreKind :: Kind -> TypeRep.Kind
97 kindToCoreKind KindStar = TypeRep.liftedTypeKind
98 kindToCoreKind (KindArrow k1 k2) = Coercion.mkArrowKind (kindToCoreKind k1) (kindToCoreKind k2)
99 kindToCoreKind _ = Prelude.error "kindToCoreKind does not know how to handle that"
101 coreKindToKind :: TypeRep.Kind -> Kind
103 case Coercion.splitKindFunTy_maybe k of
104 Prelude.Just (k1,k2) -> KindArrow (coreKindToKind k1) (coreKindToKind k2)
106 if (Coercion.isLiftedTypeKind k) then KindStar
107 else if (Coercion.isUnliftedTypeKind k) then KindStar
108 else if (Coercion.isArgTypeKind k) then KindStar
109 else if (Coercion.isUbxTupleKind k) then KindStar
110 else if (Coercion.isOpenTypeKind k) then KindStar
111 -- else if (Coercion.isUnliftedTypeKind k) then KindUnliftedType
112 -- else if (Coercion.isOpenTypeKind k) then KindOpenType
113 -- else if (Coercion.isArgTypeKind k) then KindArgType
114 -- else if (Coercion.isUbxTupleKind k) then KindUnboxedTuple
115 else if (Coercion.isTySuperKind k) then Prelude.error "coreKindToKind got the kind-of-the-kind-of-types"
116 else if (Coercion.isCoSuperKind k) then Prelude.error "coreKindToKind got the kind-of-the-kind-of-coercions"
117 else Prelude.error ((Prelude.++) "coreKindToKind got an unknown kind: "
118 (Outputable.showSDoc (Outputable.ppr k)))
119 outputableToString :: Outputable.Outputable a => a -> Prelude.String
120 outputableToString = (\x -> Outputable.showSDoc (Outputable.ppr x))
122 -- I'm leaving this here (commented out) in case I ever need it again)
123 --checkTypeEquality :: Type.Type -> Type.Type -> Prelude.Bool
124 --checkTypeEquality t1 t2 = Type.tcEqType (Type.expandTypeSynonyms t1) (Type.expandTypeSynonyms t2)
126 coreViewDeep :: Type.Type -> Type.Type
129 TypeRep.TyVarTy tv -> TypeRep.TyVarTy tv
130 TypeRep.FunTy arg res -> TypeRep.FunTy (coreViewDeep arg) (coreViewDeep res)
131 TypeRep.AppTy fun arg -> TypeRep.AppTy (coreViewDeep fun) (coreViewDeep arg)
132 TypeRep.ForAllTy fun arg -> TypeRep.ForAllTy fun (coreViewDeep arg)
133 TypeRep.TyConApp tc tys -> let t' = TypeRep.TyConApp tc (Prelude.map coreViewDeep tys)
134 in case Type.coreView t' of
135 Prelude.Nothing -> t'
136 Prelude.Just t'' -> t''
137 TypeRep.PredTy p -> case Type.coreView t of
138 Prelude.Nothing -> TypeRep.PredTy p
139 Prelude.Just t' -> t'
141 -- FIXME: cotycon applications may be oversaturated
142 coreCoercionToWeakCoercion :: Type.Type -> WeakCoercion
143 coreCoercionToWeakCoercion c =
145 TypeRep.TyVarTy v -> WCoVar (WeakCoerVar v (Prelude.error "FIXME") (Prelude.error "FIXME") (Prelude.error "FIXME"))
146 TypeRep.AppTy t1 t2 -> WCoApp (coreCoercionToWeakCoercion t1) (coreCoercionToWeakCoercion t2)
147 TypeRep.TyConApp tc t ->
148 case TyCon.isCoercionTyCon_maybe tc of
149 Prelude.Nothing -> Prelude.error ((Prelude.++) "coreCoercionToWeakCoercion got " (outputableToString c))
150 Prelude.Just (_, ctcd) ->
152 (TyCon.CoTrans , [x,y] ) -> WCoComp (coreCoercionToWeakCoercion x) (coreCoercionToWeakCoercion y)
153 (TyCon.CoSym , [x] ) -> WCoSym (coreCoercionToWeakCoercion x)
154 (TyCon.CoLeft , [x] ) -> WCoLeft (coreCoercionToWeakCoercion x)
155 (TyCon.CoRight , [x] ) -> WCoLeft (coreCoercionToWeakCoercion x)
156 -- FIXME (TyCon.CoUnsafe, [t1, t2 ] ) -> WCoUnsafe (coreTypeToWeakType t1) (coreTypeToWeakType t2)
157 (TyCon.CoTrans , [] ) -> Prelude.error "CoTrans is not in post-publication-appendix SystemFC1"
158 (TyCon.CoCsel1 , [] ) -> Prelude.error "CoCsel1 is not in post-publication-appendix SystemFC1"
159 (TyCon.CoCsel2 , [] ) -> Prelude.error "CoCsel2 is not in post-publication-appendix SystemFC1"
160 (TyCon.CoCselR , [] ) -> Prelude.error "CoCselR is not in post-publication-appendix SystemFC1"
161 (TyCon.CoInst , [] ) -> Prelude.error "CoInst is not in post-publication-appendix SystemFC1"
162 -- (TyCon.CoAxiom , [] ) -> Prelude.error "CoAxiom is not yet implemented (FIXME)"
163 _ -> Prelude.error ((Prelude.++) "coreCoercionToWeakCoercion got " (outputableToString c))
164 _ -> Prelude.error ((Prelude.++) "coreCoercionToWeakCoercion got " (outputableToString c))
165 -- TypeRep.ForAllTy v t -> WCoAll (Prelude.error "FIXME") (coreTypeToWeakType t)
166 -- FIXME x y -> WCoAppT (coreCoercionToWeakCoercion x) (coreCoercionToWeakType y)
167 -- CoreSyn.Type t -> WCoType (coreTypeToWeakType t)
170 weakCoercionToCoreCoercion :: CoreCoercion -> Type.Type
171 | WCoVar (weakCoerVar _ _ t1 t2) => (t1,t2)
172 | WCoType t => Prelude_error "FIXME WCoType"
173 | WCoApp c1 c2 => Prelude_error "FIXME WCoApp"
174 | WCoAppT c t => Prelude_error "FIXME WCoAppT"
175 | WCoAll k f => Prelude_error "FIXME WCoAll"
176 | WCoSym c => let (t2,t1) := weakCoercionTypes c in (t1,t2)
177 | WCoComp c1 c2 => Prelude_error "FIXME WCoComp"
178 | WCoLeft c => Prelude_error "FIXME WCoLeft"
179 | WCoRight c => Prelude_error "FIXME WCoRight"
180 | WCoUnsafe t1 t2 => (t1,t2)
184 --trace = Debug.Trace.trace
186 trace msg x = System.IO.Unsafe.unsafePerformIO $ Prelude.return x
189 trace msg x = System.IO.Unsafe.unsafePerformIO $
190 (Prelude.>>=) (System.IO.hPutStrLn System.IO.stdout msg) (\_ -> Prelude.return x)
191 trace msg x = System.IO.Unsafe.unsafePerformIO $
192 (Prelude.>>=) (System.IO.hPutStr System.IO.stdout " ") (\_ -> Prelude.return x)