src/Extraction-prefix.hs

   1 {-# OPTIONS_GHC -fno-warn-unused-binds  #-}
   2 module Extraction ( coqCoreToStringPass )
   3 where
   4 --import HsSyn
   5 --import TcType
   6 --import CoreFVs
   7 --import CoreUtils
   8 --import MkCore
   9 --import Var
  10 --import BasicTypes
  11 --import Bag
  12 --import VarSet
  13 --import SrcLoc
  14 --import Data.List
  15
  16 import qualified TysWiredIn
  17 import qualified TysPrim
  18 import qualified Outputable
  19 import qualified PrelNames
  20 import qualified Name
  21 import qualified Literal
  22 import qualified Type
  23 import qualified TypeRep
  24 import qualified DataCon
  25 import qualified TyCon
  26 import qualified Coercion
  27 import qualified Var
  28 import qualified Id
  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
  35
  36 import Data.Bits ((.&.), shiftL, (.|.))
  37 import Prelude ( (++), (+), (==), Show, show, Char )
  38
  39 {-
  40 nat2int :: Nat -> Prelude.Int
  41 nat2int O     = 0
  42 nat2int (S x) = 1 + (nat2int x)
  43
  44 nat2string :: Nat -> Prelude.String
  45 nat2string n = show (nat2int n)
  46
  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)
  54
  55 coreKindToKind :: TypeRep.Kind -> Kind
  56 coreKindToKind k =
  57   case Coercion.splitKindFunTy_maybe k of
  58       Prelude.Just (k1,k2) -> KindTypeFunction (coreKindToKind k1) (coreKindToKind k2)
  59       Prelude.Nothing ->
  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!"
  74
  75 outputableToString :: Outputable -> String
  76 outputableToString = (\x -> Outputable.showSDoc (Outputable.ppr x))
  77 -}