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 -- used for extracting strings
  30 bin2ascii =
  31   (\ b0 b1 b2 b3 b4 b5 b6 b7 ->
  32      let f b i = if b then 1 `shiftL` i else 0
  33      in Data.Char.chr (f b0 0 .|. f b1 1 .|. f b2 2 .|. f b3 3 .|. f b4 4 .|. f b5 5 .|. f b6 6 .|. f b7 7))
  34 --bin2ascii' =
  35 --  (\ f c -> let n = Char.code c in let h i = (n .&. (1 `shiftL` i)) /= 0 in f (h 0) (h 1) (h 2) (h 3) (h 4) (h 5) (h 6) (h 7))
  36 --shiftAscii =
  37 --  \ b c -> Data.Char.chr (((Char.code c) `shiftL` 1) .&. 255 .|. if b then 1 else 0)
  38
  39 -- crude way of casting Coq "error monad" into Haskell exceptions
  40 errOrFail :: OrError a -> a
  41 errOrFail (OK x)    = x
  42 errOrFail (Error s) = Prelude.error s
  43
  44 getTyConTyVars :: TyCon.TyCon -> [Var.TyVar]
  45 getTyConTyVars tc = if TyCon.isFunTyCon tc then [] else if TyCon.isPrimTyCon tc then [] else TyCon.tyConTyVars tc
  46
  47 -- to do: this could be moved into Coq
  48 coreVarToWeakVar :: Var.Var -> WeakVar
  49 coreVarToWeakVar v | Id.isId     v = WExprVar (WeakExprVar v (errOrFail (coreTypeToWeakType (Var.varType v))))
  50 coreVarToWeakVar v | Var.isTyVar v = WTypeVar (WeakTypeVar v (coreKindToKind (Var.varType v)))
  51 coreVarToWeakVar v | Var.isCoVar v = WCoerVar (WeakCoerVar v (Prelude.error "FIXME") (Prelude.error "FIXME"))
  52 coreVarToWeakVar _                 =
  53    Prelude.error "Var.Var that is neither an expression variable, type variable, nor coercion variable!"
  54
  55 tyConOrTyFun :: TyCon.TyCon -> Prelude.Either TyCon.TyCon TyCon.TyCon
  56 --FIXME: go back to this
  57 --tyConOrTyFun n = if TyCon.isFamInstTyCon n then Prelude.Left n else Prelude.Right n
  58 tyConOrTyFun n = if TyCon.isFamInstTyCon n then Prelude.Left n else Prelude.Left n
  59
  60 tyFunResultKind :: TyCon.TyCon -> Kind
  61 tyFunResultKind tc = coreKindToKind (TyCon.tyConKind tc)
  62
  63 nat2int :: Nat -> Prelude.Int
  64 nat2int O     = 0
  65 nat2int (S x) = 1 + (nat2int x)
  66
  67 natToString :: Nat -> Prelude.String
  68 natToString n = show (nat2int n)
  69
  70 -- only needs to sanitize characters which might appear in Haskell identifiers
  71 sanitizeForLatex :: Prelude.String -> Prelude.String
  72 sanitizeForLatex []    = []
  73 sanitizeForLatex ('_':x) = "\\_"++(sanitizeForLatex x)
  74 sanitizeForLatex ('$':x) = "\\$"++(sanitizeForLatex x)
  75 sanitizeForLatex ('#':x) = "\\#"++(sanitizeForLatex x)
  76 sanitizeForLatex (c:x) = c:(sanitizeForLatex x)
  77
  78 coreKindToKind :: TypeRep.Kind -> Kind
  79 coreKindToKind k =
  80   case Coercion.splitKindFunTy_maybe k of
  81       Prelude.Just (k1,k2) -> KindTypeFunction (coreKindToKind k1) (coreKindToKind k2)
  82       Prelude.Nothing ->
  83                       if      (Coercion.isLiftedTypeKind k)   then KindType
  84                  else if (Coercion.isUnliftedTypeKind k) then KindUnliftedType
  85                  else if (Coercion.isOpenTypeKind k)     then KindOpenType
  86                  else if (Coercion.isArgTypeKind k)      then KindArgType
  87                  else if (Coercion.isUbxTupleKind k)     then KindUnboxedTuple
  88                  else if (Coercion.isTySuperKind k)      then Prelude.error "coreKindToKind got the kind-of-the-kind-of-types"
  89                  else if (Coercion.isCoSuperKind k)      then Prelude.error "coreKindToKind got the kind-of-the-kind-of-coercions"
  90                  else                                         Prelude.error ((Prelude.++) "coreKindToKind got an unknown kind: "
  91                                                                                (Outputable.showSDoc (Outputable.ppr k)))
  92 outputableToString :: Outputable.Outputable a => a -> Prelude.String
  93 outputableToString = (\x -> Outputable.showSDoc (Outputable.ppr x))
  94
  95 -- TO DO: I think we can remove this now
  96 checkTypeEquality :: Type.Type -> Type.Type -> Prelude.Bool
  97 checkTypeEquality t1 t2 = Type.tcEqType (Type.expandTypeSynonyms t1) (Type.expandTypeSynonyms t2)
  98
  99 --showType t = outputableToString (Type.expandTypeSynonyms t)
 100 showType t = outputableToString (coreViewDeep t)
 101
 102 coreViewDeep :: Type.Type -> Type.Type
 103 coreViewDeep t =
 104     case t of
 105       TypeRep.TyVarTy tv       -> TypeRep.TyVarTy tv
 106       TypeRep.FunTy arg res    -> TypeRep.FunTy (coreViewDeep arg) (coreViewDeep res)
 107       TypeRep.AppTy fun arg    -> TypeRep.AppTy (coreViewDeep fun) (coreViewDeep arg)
 108       TypeRep.ForAllTy fun arg -> TypeRep.ForAllTy fun (coreViewDeep arg)
 109       TypeRep.TyConApp tc tys  -> let t' = TypeRep.TyConApp tc (Prelude.map coreViewDeep tys)
 110                         in case Type.coreView t' of
 111                                Prelude.Nothing     -> t'
 112                                Prelude.Just    t'' -> t''
 113       TypeRep.PredTy p         -> case Type.coreView t of
 114                                Prelude.Nothing     -> TypeRep.PredTy p
 115                                Prelude.Just    t'  -> t'