1 {-# OPTIONS_GHC -fno-warn-unused-binds #-}
2 module Extraction ( coqCoreToStringPass )
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 )
40 nat2int :: Nat -> Prelude.Int
42 nat2int (S x) = 1 + (nat2int x)
44 nat2string :: Nat -> Prelude.String
45 nat2string n = show (nat2int n)
47 -- only needs to sanitize characters which might appear in Haskell identifiers
48 sanitizeForLatex :: Prelude.String -> Prelude.String
49 sanitizeForLatex [] = []
50 sanitizeForLatex ('_':x) = "\\_"++(sanitizeForLatex x)
51 sanitizeForLatex ('$':x) = "\\$"++(sanitizeForLatex x)
52 sanitizeForLatex ('#':x) = "\\#"++(sanitizeForLatex x)
53 sanitizeForLatex (c:x) = c:(sanitizeForLatex x)
55 coreKindToKind :: TypeRep.Kind -> Kind
57 case Coercion.splitKindFunTy_maybe k of
58 Prelude.Just (k1,k2) -> KindTypeFunction (coreKindToKind k1) (coreKindToKind k2)
60 if (Coercion.isLiftedTypeKind k) then KindType
61 else if (Coercion.isUnliftedTypeKind k) then KindUnliftedType
62 else if (Coercion.isOpenTypeKind k) then KindOpenType
63 else if (Coercion.isArgTypeKind k) then KindArgType
64 else if (Coercion.isUbxTupleKind k) then KindUnboxedTuple
65 else if (Coercion.isTySuperKind k) then Prelude.error "coreKindToKind got the kind-of-the-kind-of-types"
66 else if (Coercion.isCoSuperKind k) then Prelude.error "coreKindToKind got the kind-of-the-kind-of-coercions"
67 else Prelude.error ((Prelude.++) "coreKindToKind got an unknown kind: "
68 (Outputable.showSDoc (Outputable.ppr k)))
69 coreVarSort :: Var.Var -> CoreVarSort
70 coreVarSort v | Id.isId v = CoreExprVar (Var.varType{-AsType-} v)
71 coreVarSort v | Var.isTyVar v = CoreTypeVar (coreKindToKind (Var.varType v))
72 coreVarSort v | Var.isCoVar v = CoreCoerVar (Coercion.coercionKind v)
73 coreVarSort v | otherwise = Prelude.error "Var.Var that is neither an expression variable, type variable, nor coercion variable!"
75 outputableToString :: Outputable -> String
76 outputableToString = (\x -> Outputable.showSDoc (Outputable.ppr x))