1 {-# OPTIONS_GHC -fno-warn-unused-binds #-}
2 module Extraction ( coqCoreToStringPass )
15 import qualified MkCore
16 import qualified TysWiredIn
17 import qualified TysPrim
18 import qualified Outputable
19 import qualified PrelNames
21 import qualified Literal
23 import qualified TypeRep
24 import qualified DataCon
25 import qualified TyCon
26 import qualified Coercion
29 import qualified FastString
30 import qualified BasicTypes
31 import qualified DataCon
32 import qualified CoreSyn
33 import qualified Class
34 import qualified Data.Char
36 import Data.Bits ((.&.), shiftL, (.|.))
37 import Prelude ( (++), (+), (==), Show, show, Char )
39 dataConEqTheta' dc = map (\p -> {-FIXME-}) (DataCon.dataConEqTheta dc)
41 nat2int :: Nat -> Prelude.Int
43 nat2int (S x) = 1 + (nat2int x)
45 nat2string :: Nat -> Prelude.String
46 nat2string n = show (nat2int n)
48 -- only needs to sanitize characters which might appear in Haskell identifiers
49 sanitizeForLatex :: Prelude.String -> Prelude.String
50 sanitizeForLatex [] = []
51 sanitizeForLatex ('_':x) = "\\_"++(sanitizeForLatex x)
52 sanitizeForLatex ('$':x) = "\\$"++(sanitizeForLatex x)
53 sanitizeForLatex ('#':x) = "\\#"++(sanitizeForLatex x)
54 sanitizeForLatex (c:x) = c:(sanitizeForLatex x)
56 coreKindToKind :: TypeRep.Kind -> Kind
58 case Coercion.splitKindFunTy_maybe k of
59 Prelude.Just (k1,k2) -> KindTypeFunction (coreKindToKind k1) (coreKindToKind k2)
61 if (Coercion.isLiftedTypeKind k) then KindType
62 else if (Coercion.isUnliftedTypeKind k) then KindUnliftedType
63 else if (Coercion.isOpenTypeKind k) then KindOpenType
64 else if (Coercion.isArgTypeKind k) then KindArgType
65 else if (Coercion.isUbxTupleKind k) then KindUnboxedTuple
66 else if (Coercion.isTySuperKind k) then Prelude.error "coreKindToKind got the kind-of-the-kind-of-types"
67 else if (Coercion.isCoSuperKind k) then Prelude.error "coreKindToKind got the kind-of-the-kind-of-coercions"
68 else Prelude.error ((Prelude.++) "coreKindToKind got an unknown kind: "
69 (Outputable.showSDoc (Outputable.ppr k)))
70 coreVarSort :: Var.Var -> CoreVarSort
71 coreVarSort v | Id.isId v = CoreExprVar (Var.varType{-AsType-} v)
72 coreVarSort v | Var.isTyVar v = CoreTypeVar (coreKindToKind (Var.varType v))
73 coreVarSort v | Var.isCoVar v = CoreCoerVar (Coercion.coercionKind v)
74 coreVarSort v | otherwise = Prelude.error "Var.Var that is neither an expression variable, type variable, nor coercion variable!"
76 outputableToString :: Outputable -> String
77 outputableToString = (\x -> Outputable.showSDoc (Outputable.ppr x))