1 {-# OPTIONS_GHC -fno-warn-unused-binds #-}
2 module CoqPass ( coqPassCoreToString, coqPassCoreToCore )
4 import qualified MkCore
5 import qualified TysWiredIn
6 import qualified TysPrim
7 import qualified Outputable
8 import qualified PrelNames
10 import qualified Literal
12 import qualified TypeRep
13 import qualified DataCon
14 import qualified TyCon
15 import qualified Coercion
18 import qualified FastString
19 import qualified BasicTypes
20 import qualified DataCon
21 import qualified CoreSyn
22 import qualified Class
23 import qualified Data.Char
24 import Data.Bits ((.&.), shiftL, (.|.))
25 import Prelude ( (++), (+), (==), Show, show, Char )
26 import qualified Prelude
27 import qualified GHC.Base
29 -- used for extracting strings
31 (\ b0 b1 b2 b3 b4 b5 b6 b7 ->
32 let f b i = if b then 1 `shiftL` i else 0
33 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))
35 -- (\ f c -> let n = Char.code c in let h i = (n .&. (1 `shiftL` i)) /= 0 in f (h 0) (h 1) (h 2) (h 3) (h 4) (h 5) (h 6) (h 7))
37 -- \ b c -> Data.Char.chr (((Char.code c) `shiftL` 1) .&. 255 .|. if b then 1 else 0)
39 -- crude way of casting Coq "error monad" into Haskell exceptions
40 errOrFail :: OrError a -> a
42 errOrFail (Error s) = Prelude.error s
44 getTyConTyVars :: TyCon.TyCon -> [Var.TyVar]
45 getTyConTyVars tc = if TyCon.isFunTyCon tc then [] else if TyCon.isPrimTyCon tc then [] else TyCon.tyConTyVars tc
47 -- to do: this could be moved into Coq
48 coreVarToWeakVar :: Var.Var -> WeakVar
49 coreVarToWeakVar v | Id.isId v = WExprVar (WeakExprVar v (errOrFail (coreTypeToWeakType (Var.varType v))))
50 coreVarToWeakVar v | Var.isTyVar v = WTypeVar (WeakTypeVar v (coreKindToKind (Var.varType v)))
51 coreVarToWeakVar v | Var.isCoVar v = WCoerVar (WeakCoerVar v (Prelude.error "FIXME") (Prelude.error "FIXME"))
53 Prelude.error "Var.Var that is neither an expression variable, type variable, nor coercion variable!"
55 tyConOrTyFun :: TyCon.TyCon -> Prelude.Either TyCon.TyCon TyCon.TyCon
56 --FIXME: go back to this
57 --tyConOrTyFun n = if TyCon.isFamInstTyCon n then Prelude.Left n else Prelude.Right n
58 tyConOrTyFun n = if TyCon.isFamInstTyCon n then Prelude.Left n else Prelude.Left n
60 tyFunResultKind :: TyCon.TyCon -> Kind
61 tyFunResultKind tc = coreKindToKind (TyCon.tyConKind tc)
63 nat2int :: Nat -> Prelude.Int
65 nat2int (S x) = 1 + (nat2int x)
67 natToString :: Nat -> Prelude.String
68 natToString n = show (nat2int n)
70 -- only needs to sanitize characters which might appear in Haskell identifiers
71 sanitizeForLatex :: Prelude.String -> Prelude.String
72 sanitizeForLatex [] = []
73 sanitizeForLatex ('_':x) = "\\_"++(sanitizeForLatex x)
74 sanitizeForLatex ('$':x) = "\\$"++(sanitizeForLatex x)
75 sanitizeForLatex ('#':x) = "\\#"++(sanitizeForLatex x)
76 sanitizeForLatex (c:x) = c:(sanitizeForLatex x)
78 coreKindToKind :: TypeRep.Kind -> Kind
80 case Coercion.splitKindFunTy_maybe k of
81 Prelude.Just (k1,k2) -> KindTypeFunction (coreKindToKind k1) (coreKindToKind k2)
83 if (Coercion.isLiftedTypeKind k) then KindType
84 else if (Coercion.isUnliftedTypeKind k) then KindUnliftedType
85 else if (Coercion.isOpenTypeKind k) then KindOpenType
86 else if (Coercion.isArgTypeKind k) then KindArgType
87 else if (Coercion.isUbxTupleKind k) then KindUnboxedTuple
88 else if (Coercion.isTySuperKind k) then Prelude.error "coreKindToKind got the kind-of-the-kind-of-types"
89 else if (Coercion.isCoSuperKind k) then Prelude.error "coreKindToKind got the kind-of-the-kind-of-coercions"
90 else Prelude.error ((Prelude.++) "coreKindToKind got an unknown kind: "
91 (Outputable.showSDoc (Outputable.ppr k)))
92 outputableToString :: Outputable.Outputable a => a -> Prelude.String
93 outputableToString = (\x -> Outputable.showSDoc (Outputable.ppr x))
95 -- TO DO: I think we can remove this now
96 checkTypeEquality :: Type.Type -> Type.Type -> Prelude.Bool
97 checkTypeEquality t1 t2 = Type.tcEqType (Type.expandTypeSynonyms t1) (Type.expandTypeSynonyms t2)
99 --showType t = outputableToString (Type.expandTypeSynonyms t)
100 showType t = outputableToString (coreViewDeep t)
102 coreViewDeep :: Type.Type -> Type.Type
105 TypeRep.TyVarTy tv -> TypeRep.TyVarTy tv
106 TypeRep.FunTy arg res -> TypeRep.FunTy (coreViewDeep arg) (coreViewDeep res)
107 TypeRep.AppTy fun arg -> TypeRep.AppTy (coreViewDeep fun) (coreViewDeep arg)
108 TypeRep.ForAllTy fun arg -> TypeRep.ForAllTy fun (coreViewDeep arg)
109 TypeRep.TyConApp tc tys -> let t' = TypeRep.TyConApp tc (Prelude.map coreViewDeep tys)
110 in case Type.coreView t' of
111 Prelude.Nothing -> t'
112 Prelude.Just t'' -> t''
113 TypeRep.PredTy p -> case Type.coreView t of
114 Prelude.Nothing -> TypeRep.PredTy p
115 Prelude.Just t' -> t'