1 {-# OPTIONS_GHC -fno-warn-unused-matches -fno-warn-unused-binds -fno-warn-unused-imports #-}
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, (.), ($) )
33 import qualified Prelude
34 import qualified GHC.Base
35 import qualified System.IO.Unsafe
37 getTyConTyVars :: TyCon.TyCon -> [Var.TyVar]
39 if TyCon.isFunTyCon tc
41 else if TyCon.isPrimTyCon tc
43 else TyCon.tyConTyVars tc
45 cmpAlts :: (CoreSyn.AltCon,[Var.Var],CoreSyn.Expr Var.Var) -> (CoreSyn.AltCon,[Var.Var],CoreSyn.Expr Var.Var) -> Data.Ord.Ordering
46 cmpAlts (CoreSyn.DEFAULT,_,_) _ = Data.Ord.LT
47 cmpAlts _ (CoreSyn.DEFAULT,_,_) = Data.Ord.GT
48 cmpAlts (a1,_,_) (a2,_,_) = Data.Ord.compare a2 a1
50 sortAlts :: [(CoreSyn.AltCon,[Var.Var],CoreSyn.Expr Var.Var)] -> [(CoreSyn.AltCon,[Var.Var],CoreSyn.Expr Var.Var)]
51 sortAlts x = Data.List.sortBy (\a b -> if a `CoreSyn.ltAlt` b then Data.Ord.LT else Data.Ord.GT) x
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
57 = WCoerVar (WeakCoerVar v
58 (errOrFail (coreTypeToWeakType (Prelude.fst (Coercion.coercionKind (Var.varType v)))))
59 (errOrFail (coreTypeToWeakType (Prelude.snd (Coercion.coercionKind (Var.varType v))))))
61 Prelude.error "Var.Var that is neither an expression variable, type variable, nor coercion variable!"
63 errOrFail :: OrError t -> t
65 errOrFail (Error s) = Prelude.error s
67 rawTyFunKind :: TyCon.TyCon -> ( [Kind] , Kind )
68 rawTyFunKind tc = ((Prelude.map coreKindToKind (Prelude.take (TyCon.tyConArity tc) argk))
70 coreKindToKind (Coercion.mkArrowKinds (Prelude.drop (TyCon.tyConArity tc) argk) retk))
71 where (argk,retk) = Coercion.splitKindFunTys (TyCon.tyConKind tc)
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
79 else if TyCon.isSynTyCon n
83 nat2int :: Nat -> Prelude.Int
85 nat2int (S x) = 1 + (nat2int x)
87 natToString :: Nat -> Prelude.String
88 natToString n = show (nat2int n)
90 sanitizeForLatex :: Prelude.String -> Prelude.String
91 sanitizeForLatex [] = []
92 sanitizeForLatex ('_':x) = "\\_"++(sanitizeForLatex x)
93 sanitizeForLatex ('$':x) = "\\$"++(sanitizeForLatex x)
94 sanitizeForLatex ('#':x) = "\\#"++(sanitizeForLatex x)
95 sanitizeForLatex (c:x) = c:(sanitizeForLatex x)
97 kindToCoreKind :: Kind -> TypeRep.Kind
98 kindToCoreKind KindStar = TypeRep.liftedTypeKind
99 kindToCoreKind (KindArrow k1 k2) = Coercion.mkArrowKind (kindToCoreKind k1) (kindToCoreKind k2)
100 kindToCoreKind k = Prelude.error ((Prelude.++)
101 "kindToCoreKind does not know how to handle kind "
103 coreKindToKind :: TypeRep.Kind -> Kind
105 case Coercion.splitKindFunTy_maybe k of
106 Prelude.Just (k1,k2) -> KindArrow (coreKindToKind k1) (coreKindToKind k2)
108 if (Coercion.isLiftedTypeKind k) then KindStar
109 else if (Coercion.isUnliftedTypeKind k) then KindStar
110 else if (Coercion.isArgTypeKind k) then KindStar
111 else if (Coercion.isUbxTupleKind k) then KindStar
112 else if (Coercion.isOpenTypeKind k) then KindStar
114 -- The "subkinding" in GHC is not dealt with in System FC, and dealing
115 -- with it is not actually as simple as you'd think.
117 -- else if (Coercion.isUnliftedTypeKind k) then KindUnliftedType
118 -- else if (Coercion.isOpenTypeKind k) then KindOpenType
119 -- else if (Coercion.isArgTypeKind k) then KindArgType
120 -- else if (Coercion.isUbxTupleKind k) then KindUnboxedTuple
122 else if (Coercion.isTySuperKind k) then Prelude.error "coreKindToKind got the kind-of-the-kind-of-types"
123 else if (Coercion.isCoSuperKind k) then Prelude.error "coreKindToKind got the kind-of-the-kind-of-coercions"
124 else Prelude.error ((Prelude.++) "coreKindToKind got an unknown kind: "
125 (Outputable.showSDoc (Outputable.ppr k)))
126 outputableToString :: Outputable.Outputable a => a -> Prelude.String
127 outputableToString = (\x -> Outputable.showSDocDebug (Outputable.ppr x))
129 coreViewDeep :: Type.Type -> Type.Type
132 TypeRep.TyVarTy tv -> TypeRep.TyVarTy tv
133 TypeRep.FunTy arg res -> TypeRep.FunTy (coreViewDeep arg) (coreViewDeep res)
134 TypeRep.AppTy fun arg -> TypeRep.AppTy (coreViewDeep fun) (coreViewDeep arg)
135 TypeRep.ForAllTy fun arg -> TypeRep.ForAllTy fun (coreViewDeep arg)
136 TypeRep.TyConApp tc tys -> let t' = TypeRep.TyConApp tc (Prelude.map coreViewDeep tys)
137 in case Type.coreView t' of
138 Prelude.Nothing -> t'
139 Prelude.Just t'' -> t''
140 TypeRep.PredTy p -> case Type.coreView t of
141 Prelude.Nothing -> TypeRep.PredTy p
142 Prelude.Just t' -> t'
144 coreCoercionToWeakCoercion :: Type.Type -> WeakCoercion
145 coreCoercionToWeakCoercion c =
146 WCoUnsafe (errOrFail (coreTypeToWeakType t1)) (errOrFail (coreTypeToWeakType t2))
148 (t1,t2) = Coercion.coercionKind c
150 -- REMEMBER: cotycon applications may be oversaturated
152 TypeRep.TyVarTy v -> WCoVar (WeakCoerVar v (Prelude.error "FIXME") (Prelude.error "FIXME") (Prelude.error "FIXME"))
153 TypeRep.AppTy t1 t2 -> WCoApp (coreCoercionToWeakCoercion t1) (coreCoercionToWeakCoercion t2)
154 TypeRep.TyConApp tc t ->
155 case TyCon.isCoercionTyCon_maybe tc of
156 Prelude.Nothing -> Prelude.error ((Prelude.++) "coreCoercionToWeakCoercion got isCoercionTyCon_maybe " (outputableToString c))
157 Prelude.Just (_, ctcd) ->
159 (TyCon.CoTrans , [x,y] ) -> WCoComp (coreCoercionToWeakCoercion x) (coreCoercionToWeakCoercion y)
160 (TyCon.CoSym , [x] ) -> WCoSym (coreCoercionToWeakCoercion x)
161 (TyCon.CoLeft , [x] ) -> WCoLeft (coreCoercionToWeakCoercion x)
162 (TyCon.CoRight , [x] ) -> WCoLeft (coreCoercionToWeakCoercion x)
163 -- (TyCon.CoUnsafe, [t1, t2 ] ) -> WCoUnsafe (coreTypeToWeakType t1) (coreTypeToWeakType t2)
164 (TyCon.CoTrans , [] ) -> Prelude.error "CoTrans is not in post-publication-appendix SystemFC1"
165 (TyCon.CoCsel1 , [] ) -> Prelude.error "CoCsel1 is not in post-publication-appendix SystemFC1"
166 (TyCon.CoCsel2 , [] ) -> Prelude.error "CoCsel2 is not in post-publication-appendix SystemFC1"
167 (TyCon.CoCselR , [] ) -> Prelude.error "CoCselR is not in post-publication-appendix SystemFC1"
168 (TyCon.CoInst , [] ) -> Prelude.error "CoInst is not in post-publication-appendix SystemFC1"
169 (TyCon.CoAxiom _ _ _ , _ ) -> Prelude.error "CoAxiom is not yet implemented (FIXME)"
170 ( _, [ t1 , t2 ]) -> WCoUnsafe (errOrFail (coreTypeToWeakType t1)) (errOrFail (coreTypeToWeakType t2))
171 _ -> Prelude.error ((Prelude.++) "coreCoercionToWeakCoercion got " (outputableToString c))
172 _ -> Prelude.error ((Prelude.++) "coreCoercionToWeakCoercion got " (outputableToString c))
174 -- TypeRep.ForAllTy v t -> WCoAll (Prelude.error "FIXME") (coreTypeToWeakType t)
175 -- FIXME x y -> WCoAppT (coreCoercionToWeakCoercion x) (coreCoercionToWeakType y)
176 -- CoreSyn.Type t -> WCoType (coreTypeToWeakType t)
179 weakCoercionToCoreCoercion :: CoreCoercion -> Type.Type
180 | WCoVar (weakCoerVar _ _ t1 t2) => (t1,t2)
181 | WCoType t => Prelude_error "FIXME WCoType"
182 | WCoApp c1 c2 => Prelude_error "FIXME WCoApp"
183 | WCoAppT c t => Prelude_error "FIXME WCoAppT"
184 | WCoAll k f => Prelude_error "FIXME WCoAll"
185 | WCoSym c => let (t2,t1) := weakCoercionTypes c in (t1,t2)
186 | WCoComp c1 c2 => Prelude_error "FIXME WCoComp"
187 | WCoLeft c => Prelude_error "FIXME WCoLeft"
188 | WCoRight c => Prelude_error "FIXME WCoRight"
189 | WCoUnsafe t1 t2 => (t1,t2)
192 {-# NOINLINE trace #-}
193 trace :: Prelude.String -> a -> a
196 --trace = Debug.Trace.trace
198 --trace msg x = System.IO.Unsafe.unsafePerformIO $ Prelude.return x
200 --trace msg x = System.IO.Unsafe.unsafePerformIO $
201 -- (Prelude.>>=) (System.IO.hPutStrLn System.IO.stdout msg) (\_ -> Prelude.return x)
202 --trace msg x = System.IO.Unsafe.unsafePerformIO $
203 -- (Prelude.>>=) (System.IO.hPutStr System.IO.stdout " ") (\_ -> Prelude.return x)
206 {- -- used for extracting strings WITHOUT the patch for Coq
208 (\ b0 b1 b2 b3 b4 b5 b6 b7 ->
209 let f b i = if b then 1 `shiftL` i else 0
210 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))
213 -- I'm leaving this here (commented out) in case I ever need it again)
214 --checkTypeEquality :: Type.Type -> Type.Type -> Prelude.Bool
215 --checkTypeEquality t1 t2 = Type.tcEqType (Type.expandTypeSynonyms t1) (Type.expandTypeSynonyms t2)