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 -- crude way of casting Coq "error monad" into Haskell exceptions
30 errOrFail :: OrError a -> a
32 errOrFail (Error s) = Prelude.error s
34 -- to do: this could be moved into Coq
35 coreVarToWeakVar :: Var.Var -> WeakVar
36 coreVarToWeakVar v | Id.isId v = WExprVar (WeakExprVar v (errOrFail (coreTypeToWeakType (Var.varType v))))
37 coreVarToWeakVar v | Var.isTyVar v = WTypeVar (WeakTypeVar v (coreKindToKind (Var.varType v)))
38 coreVarToWeakVar v | Var.isCoVar v = Prelude.error "FIXME coerVarSort not fully implemented"
40 Prelude.error "Var.Var that is neither an expression variable, type variable, nor coercion variable!"
42 nat2int :: Nat -> Prelude.Int
44 nat2int (S x) = 1 + (nat2int x)
46 nat2string :: Nat -> Prelude.String
47 nat2string n = show (nat2int n)
49 -- only needs to sanitize characters which might appear in Haskell identifiers
50 sanitizeForLatex :: Prelude.String -> Prelude.String
51 sanitizeForLatex [] = []
52 sanitizeForLatex ('_':x) = "\\_"++(sanitizeForLatex x)
53 sanitizeForLatex ('$':x) = "\\$"++(sanitizeForLatex x)
54 sanitizeForLatex ('#':x) = "\\#"++(sanitizeForLatex x)
55 sanitizeForLatex (c:x) = c:(sanitizeForLatex x)
57 coreKindToKind :: TypeRep.Kind -> Kind
59 case Coercion.splitKindFunTy_maybe k of
60 Prelude.Just (k1,k2) -> KindTypeFunction (coreKindToKind k1) (coreKindToKind k2)
62 if (Coercion.isLiftedTypeKind k) then KindType
63 else if (Coercion.isUnliftedTypeKind k) then KindUnliftedType
64 else if (Coercion.isOpenTypeKind k) then KindOpenType
65 else if (Coercion.isArgTypeKind k) then KindArgType
66 else if (Coercion.isUbxTupleKind k) then KindUnboxedTuple
67 else if (Coercion.isTySuperKind k) then Prelude.error "coreKindToKind got the kind-of-the-kind-of-types"
68 else if (Coercion.isCoSuperKind k) then Prelude.error "coreKindToKind got the kind-of-the-kind-of-coercions"
69 else Prelude.error ((Prelude.++) "coreKindToKind got an unknown kind: "
70 (Outputable.showSDoc (Outputable.ppr k)))
71 outputableToString :: Outputable.Outputable a => a -> Prelude.String
72 outputableToString = (\x -> Outputable.showSDoc (Outputable.ppr x))
74 checkTypeEquality :: Type.Type -> Type.Type -> Prelude.Bool
75 -- checkTypeEquality t1 t2 = Type.coreEqType (coreViewDeep t1) (coreViewDeep t2)
76 -- checkTypeEquality t1 t2 = Type.tcEqType (coreViewDeep t1) (coreViewDeep t2)
77 checkTypeEquality t1 t2 = Type.tcEqType (Type.expandTypeSynonyms t1) (Type.expandTypeSynonyms t2)
79 --showType t = outputableToString (Type.expandTypeSynonyms t)
80 showType t = outputableToString (coreViewDeep t)
82 coreViewDeep :: Type.Type -> Type.Type
85 TypeRep.TyVarTy tv -> TypeRep.TyVarTy tv
86 TypeRep.FunTy arg res -> TypeRep.FunTy (coreViewDeep arg) (coreViewDeep res)
87 TypeRep.AppTy fun arg -> TypeRep.AppTy (coreViewDeep fun) (coreViewDeep arg)
88 TypeRep.ForAllTy fun arg -> TypeRep.ForAllTy fun (coreViewDeep arg)
89 TypeRep.TyConApp tc tys -> let t' = TypeRep.TyConApp tc (Prelude.map coreViewDeep tys)
90 in case Type.coreView t' of
92 Prelude.Just t'' -> t''
93 TypeRep.PredTy p -> case Type.coreView t of
94 Prelude.Nothing -> TypeRep.PredTy p