1 {-# OPTIONS_GHC -fno-warn-unused-matches -fno-warn-unused-binds -fno-warn-unused-imports #-}
2 module CoqPass ( coqPassCoreToString, coqPassCoreToCore )
4 import qualified Unique
6 import qualified UniqSupply
7 import qualified MkCore
8 import qualified TysWiredIn
9 import qualified TysPrim
10 import qualified Outputable
11 import qualified PrelNames
12 import qualified OccName
14 import qualified Literal
16 import qualified TypeRep
17 import qualified DataCon
18 import qualified DsMonad
19 import qualified IOEnv
20 import qualified TcRnTypes
21 import qualified TyCon
22 import qualified Coercion
26 import qualified FastString
27 import qualified BasicTypes
28 import qualified DataCon
29 import qualified CoreSyn
30 import qualified CoreUtils
31 import qualified Class
32 import qualified Data.Char
33 import qualified Data.List
34 import qualified Data.Ord
35 import qualified Data.Typeable
36 import Data.Bits ((.&.), shiftL, (.|.))
37 import Prelude ( (++), (+), (==), Show, show, (.), ($) )
38 import qualified Prelude
39 import qualified HscTypes
40 import qualified GHC.Base
41 import qualified CoreMonad
42 import qualified System.IO.Unsafe
44 getTyConTyVars :: TyCon.TyCon -> [Var.TyVar]
46 if TyCon.isFunTyCon tc
48 else if TyCon.isPrimTyCon tc
50 else TyCon.tyConTyVars tc
52 cmpAlts :: (CoreSyn.AltCon,[Var.Var],CoreSyn.Expr Var.Var) -> (CoreSyn.AltCon,[Var.Var],CoreSyn.Expr Var.Var) -> Data.Ord.Ordering
53 cmpAlts (CoreSyn.DEFAULT,_,_) _ = Data.Ord.LT
54 cmpAlts _ (CoreSyn.DEFAULT,_,_) = Data.Ord.GT
55 cmpAlts (a1,_,_) (a2,_,_) = Data.Ord.compare a2 a1
57 sortAlts :: [(CoreSyn.AltCon,[Var.Var],CoreSyn.Expr Var.Var)] -> [(CoreSyn.AltCon,[Var.Var],CoreSyn.Expr Var.Var)]
58 sortAlts x = Data.List.sortBy (\a b -> if a `CoreSyn.ltAlt` b then Data.Ord.LT else Data.Ord.GT) x
60 coreVarToWeakVar :: Var.Var -> CoreVarToWeakVarResult
61 coreVarToWeakVar v | Id.isId v = CVTWVR_EVar (Var.varType v)
62 coreVarToWeakVar v | Var.isTyVar v = CVTWVR_TyVar (coreKindToKind (Var.varType v))
63 coreVarToWeakVar v | Coercion.isCoVar v = CVTWVR_CoVar (Prelude.fst (Coercion.coVarKind v)) (Prelude.snd (Coercion.coVarKind v))
64 coreVarToWeakVar _ = Prelude.error "Var.Var that is neither an expression, type variable, nor coercion variable!"
66 rawTyFunKind :: TyCon.TyCon -> ( [Kind] , Kind )
67 rawTyFunKind tc = ((Prelude.map coreKindToKind (Prelude.take (TyCon.tyConArity tc) argk))
69 coreKindToKind (Coercion.mkArrowKinds (Prelude.drop (TyCon.tyConArity tc) argk) retk))
70 where (argk,retk) = Coercion.splitKindFunTys (TyCon.tyConKind tc)
72 tyConOrTyFun :: TyCon.TyCon -> Prelude.Either TyCon.TyCon TyCon.TyCon
74 if n == TysPrim.statePrimTyCon -- special-purpose hack treat State# as a type family since it has kind *->* but no tyvars
76 else if TyCon.isFamInstTyCon n
78 else if TyCon.isSynTyCon n
82 nat2int :: Nat -> Prelude.Int
84 nat2int (S x) = 1 + (nat2int x)
86 natToString :: Nat -> Prelude.String
87 natToString n = show (nat2int n)
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 = Kind.liftedTypeKind
98 kindToCoreKind (KindArrow k1 k2) = Kind.mkArrowKind (kindToCoreKind k1) (kindToCoreKind k2)
99 kindToCoreKind k = Prelude.error ((Prelude.++)
100 "kindToCoreKind does not know how to handle kind "
102 coreKindToKind :: TypeRep.Kind -> Kind
104 case Kind.splitKindFunTy_maybe k of
105 Prelude.Just (k1,k2) -> KindArrow (coreKindToKind k1) (coreKindToKind k2)
107 if (Kind.isLiftedTypeKind k) then KindStar
108 else if (Kind.isUnliftedTypeKind k) then KindStar
109 else if (Kind.isArgTypeKind k) then KindStar
110 else if (Kind.isUbxTupleKind k) then KindStar
111 else if (Kind.isOpenTypeKind k) then KindStar
113 -- The "subkinding" in GHC is not dealt with in System FC, and dealing
114 -- with it is not actually as simple as you'd think.
116 -- else if (Coercion.isUnliftedTypeKind k) then KindUnliftedType
117 -- else if (Coercion.isOpenTypeKind k) then KindOpenType
118 -- else if (Coercion.isArgTypeKind k) then KindArgType
119 -- else if (Coercion.isUbxTupleKind k) then KindUnboxedTuple
121 else if (Kind.isTySuperKind k) then Prelude.error "coreKindToKind got the kind-of-the-kind-of-types"
122 else Prelude.error ((Prelude.++) "coreKindToKind got an unknown kind: "
123 (Outputable.showSDoc (Outputable.ppr k)))
124 outputableToString :: Outputable.Outputable a => a -> Prelude.String
125 outputableToString = (\x -> Outputable.showSDocDebug (Outputable.ppr x))
127 coreViewDeep :: Type.Type -> Type.Type
130 TypeRep.TyVarTy tv -> TypeRep.TyVarTy tv
131 TypeRep.FunTy arg res -> TypeRep.FunTy (coreViewDeep arg) (coreViewDeep res)
132 TypeRep.AppTy fun arg -> TypeRep.AppTy (coreViewDeep fun) (coreViewDeep arg)
133 TypeRep.ForAllTy fun arg -> TypeRep.ForAllTy fun (coreViewDeep arg)
134 TypeRep.TyConApp tc tys -> let t' = TypeRep.TyConApp tc (Prelude.map coreViewDeep tys)
135 in case Type.coreView t' of
136 Prelude.Nothing -> t'
137 Prelude.Just t'' -> t''
138 TypeRep.PredTy p -> case Type.coreView t of
139 Prelude.Nothing -> TypeRep.PredTy p
140 Prelude.Just t' -> t'
142 {-# NOINLINE trace #-}
143 trace :: Prelude.String -> a -> a
146 --trace = Debug.Trace.trace
148 --trace msg x = System.IO.Unsafe.unsafePerformIO $ Prelude.return x
150 --trace msg x = System.IO.Unsafe.unsafePerformIO $
151 -- (Prelude.>>=) (System.IO.hPutStrLn System.IO.stdout msg) (\_ -> Prelude.return x)
152 --trace msg x = System.IO.Unsafe.unsafePerformIO $
153 -- (Prelude.>>=) (System.IO.hPutStr System.IO.stdout " ") (\_ -> Prelude.return x)
155 -- I'm leaving this here (commented out) in case I ever need it again)
156 --checkTypeEquality :: Type.Type -> Type.Type -> Prelude.Bool
157 --checkTypeEquality t1 t2 = Type.tcEqType (Type.expandTypeSynonyms t1) (Type.expandTypeSynonyms t2)