src/Extraction-prefix.hs

   1 {-# OPTIONS_GHC -fno-warn-unused-binds  #-}
   2 module CoqPass ( coqPassCoreToString, coqPassCoreToCore )
   3 where
   4 import qualified MkCore
   5 import qualified TysWiredIn
   6 import qualified TysPrim
   7 import qualified Outputable
   8 import qualified PrelNames
   9 import qualified Name
  10 import qualified Literal
  11 import qualified Type
  12 import qualified TypeRep
  13 import qualified DataCon
  14 import qualified TyCon
  15 import qualified Coercion
  16 import qualified Var
  17 import qualified Id
  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
  28
  29 -- crude way of casting Coq "error monad" into Haskell exceptions
  30 errOrFail :: OrError a -> a
  31 errOrFail (OK x)    = x
  32 errOrFail (Error s) = Prelude.error s
  33
  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"
  39 coreVarToWeakVar _                 =
  40    Prelude.error "Var.Var that is neither an expression variable, type variable, nor coercion variable!"
  41
  42 nat2int :: Nat -> Prelude.Int
  43 nat2int O     = 0
  44 nat2int (S x) = 1 + (nat2int x)
  45
  46 nat2string :: Nat -> Prelude.String
  47 nat2string n = show (nat2int n)
  48
  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)
  56
  57 coreKindToKind :: TypeRep.Kind -> Kind
  58 coreKindToKind k =
  59   case Coercion.splitKindFunTy_maybe k of
  60       Prelude.Just (k1,k2) -> KindTypeFunction (coreKindToKind k1) (coreKindToKind k2)
  61       Prelude.Nothing ->
  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))
  73
  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)
  78
  79 --showType t = outputableToString (Type.expandTypeSynonyms t)
  80 showType t = outputableToString (coreViewDeep t)
  81
  82 coreViewDeep :: Type.Type -> Type.Type
  83 coreViewDeep t =
  84     case t of
  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
  91                                Prelude.Nothing     -> t'
  92                                Prelude.Just    t'' -> t''
  93       TypeRep.PredTy p         -> case Type.coreView t of
  94                                Prelude.Nothing     -> TypeRep.PredTy p
  95                                Prelude.Just    t'  -> t'