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 TyCon
19 import qualified Coercion
23 import qualified FastString
24 import qualified BasicTypes
25 import qualified DataCon
26 import qualified CoreSyn
27 import qualified CoreUtils
28 import qualified Class
29 import qualified Data.Char
30 import qualified Data.List
31 import qualified Data.Ord
32 import qualified Data.Typeable
33 import Data.Bits ((.&.), shiftL, (.|.))
34 import Prelude ( (++), (+), (==), Show, show, (.), ($) )
35 import qualified Prelude
36 import qualified GHC.Base
37 import qualified System.IO.Unsafe
39 getTyConTyVars :: TyCon.TyCon -> [Var.TyVar]
41 if TyCon.isFunTyCon tc
43 else if TyCon.isPrimTyCon tc
45 else TyCon.tyConTyVars tc
47 cmpAlts :: (CoreSyn.AltCon,[Var.Var],CoreSyn.Expr Var.Var) -> (CoreSyn.AltCon,[Var.Var],CoreSyn.Expr Var.Var) -> Data.Ord.Ordering
48 cmpAlts (CoreSyn.DEFAULT,_,_) _ = Data.Ord.LT
49 cmpAlts _ (CoreSyn.DEFAULT,_,_) = Data.Ord.GT
50 cmpAlts (a1,_,_) (a2,_,_) = Data.Ord.compare a2 a1
52 sortAlts :: [(CoreSyn.AltCon,[Var.Var],CoreSyn.Expr Var.Var)] -> [(CoreSyn.AltCon,[Var.Var],CoreSyn.Expr Var.Var)]
53 sortAlts x = Data.List.sortBy (\a b -> if a `CoreSyn.ltAlt` b then Data.Ord.LT else Data.Ord.GT) x
55 coreVarToWeakVar :: Var.Var -> CoreVarToWeakVarResult
56 coreVarToWeakVar v | Id.isId v = CVTWVR_EVar (Var.varType v)
57 coreVarToWeakVar v | Var.isTyVar v = CVTWVR_TyVar (coreKindToKind (Var.varType v))
58 coreVarToWeakVar v | Coercion.isCoVar v = CVTWVR_CoVar (Prelude.fst (Coercion.coVarKind v)) (Prelude.snd (Coercion.coVarKind v))
59 coreVarToWeakVar _ = Prelude.error "Var.Var that is neither an expression, type variable, nor coercion variable!"
61 rawTyFunKind :: TyCon.TyCon -> ( [Kind] , Kind )
62 rawTyFunKind tc = ((Prelude.map coreKindToKind (Prelude.take (TyCon.tyConArity tc) argk))
64 coreKindToKind (Coercion.mkArrowKinds (Prelude.drop (TyCon.tyConArity tc) argk) retk))
65 where (argk,retk) = Coercion.splitKindFunTys (TyCon.tyConKind tc)
67 tyConOrTyFun :: TyCon.TyCon -> Prelude.Either TyCon.TyCon TyCon.TyCon
69 if n == TysPrim.statePrimTyCon -- special-purpose hack treat State# as a type family since it has kind *->* but no tyvars
71 else if TyCon.isFamInstTyCon n
73 else if TyCon.isSynTyCon n
77 nat2int :: Nat -> Prelude.Int
79 nat2int (S x) = 1 + (nat2int x)
81 natToString :: Nat -> Prelude.String
82 natToString n = show (nat2int n)
84 sanitizeForLatex :: Prelude.String -> Prelude.String
85 sanitizeForLatex [] = []
86 sanitizeForLatex ('_':x) = "\\_"++(sanitizeForLatex x)
87 sanitizeForLatex ('$':x) = "\\$"++(sanitizeForLatex x)
88 sanitizeForLatex ('#':x) = "\\#"++(sanitizeForLatex x)
89 sanitizeForLatex (c:x) = c:(sanitizeForLatex x)
91 kindToCoreKind :: Kind -> TypeRep.Kind
92 kindToCoreKind KindStar = Kind.liftedTypeKind
93 kindToCoreKind (KindArrow k1 k2) = Kind.mkArrowKind (kindToCoreKind k1) (kindToCoreKind k2)
94 kindToCoreKind k = Prelude.error ((Prelude.++)
95 "kindToCoreKind does not know how to handle kind "
97 coreKindToKind :: TypeRep.Kind -> Kind
99 case Kind.splitKindFunTy_maybe k of
100 Prelude.Just (k1,k2) -> KindArrow (coreKindToKind k1) (coreKindToKind k2)
102 if (Kind.isLiftedTypeKind k) then KindStar
103 else if (Kind.isUnliftedTypeKind k) then KindStar
104 else if (Kind.isArgTypeKind k) then KindStar
105 else if (Kind.isUbxTupleKind k) then KindStar
106 else if (Kind.isOpenTypeKind k) then KindStar
108 -- The "subkinding" in GHC is not dealt with in System FC, and dealing
109 -- with it is not actually as simple as you'd think.
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
116 else if (Kind.isTySuperKind k) then Prelude.error "coreKindToKind got the kind-of-the-kind-of-types"
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.showSDocDebug (Outputable.ppr x))
122 coreViewDeep :: Type.Type -> Type.Type
125 TypeRep.TyVarTy tv -> TypeRep.TyVarTy tv
126 TypeRep.FunTy arg res -> TypeRep.FunTy (coreViewDeep arg) (coreViewDeep res)
127 TypeRep.AppTy fun arg -> TypeRep.AppTy (coreViewDeep fun) (coreViewDeep arg)
128 TypeRep.ForAllTy fun arg -> TypeRep.ForAllTy fun (coreViewDeep arg)
129 TypeRep.TyConApp tc tys -> let t' = TypeRep.TyConApp tc (Prelude.map coreViewDeep tys)
130 in case Type.coreView t' of
131 Prelude.Nothing -> t'
132 Prelude.Just t'' -> t''
133 TypeRep.PredTy p -> case Type.coreView t of
134 Prelude.Nothing -> TypeRep.PredTy p
135 Prelude.Just t' -> t'
137 {-# NOINLINE trace #-}
138 trace :: Prelude.String -> a -> a
141 --trace = Debug.Trace.trace
143 --trace msg x = System.IO.Unsafe.unsafePerformIO $ Prelude.return x
145 --trace msg x = System.IO.Unsafe.unsafePerformIO $
146 -- (Prelude.>>=) (System.IO.hPutStrLn System.IO.stdout msg) (\_ -> Prelude.return x)
147 --trace msg x = System.IO.Unsafe.unsafePerformIO $
148 -- (Prelude.>>=) (System.IO.hPutStr System.IO.stdout " ") (\_ -> Prelude.return x)
150 -- I'm leaving this here (commented out) in case I ever need it again)
151 --checkTypeEquality :: Type.Type -> Type.Type -> Prelude.Bool
152 --checkTypeEquality t1 t2 = Type.tcEqType (Type.expandTypeSynonyms t1) (Type.expandTypeSynonyms t2)