src/Extraction-prefix.hs

   1 {-# OPTIONS_GHC -fno-warn-unused-matches -fno-warn-unused-binds -fno-warn-unused-imports #-}
   2 module CoqPass ( coqPassCoreToString, coqPassCoreToCore )
   3 where
   4 import qualified Unique
   5 import qualified Kind
   6 import qualified UniqSupply
   7 import qualified MkCore
   8 import qualified TysWiredIn
   9 import qualified TysPrim
  10 import qualified Outputable
  11 import qualified PrelNames
  12 import qualified OccName
  13 import qualified Name
  14 import qualified Literal
  15 import qualified Type
  16 import qualified TypeRep
  17 import qualified DataCon
  18 import qualified TyCon
  19 import qualified Coercion
  20 import qualified Var
  21 import qualified Id
  22 import qualified Pair
  23 import qualified FastString
  24 import qualified BasicTypes
  25 import qualified DataCon
  26 import qualified CoreSyn
  27 import qualified CoreUtils
  28 import qualified Class
  29 import qualified Data.Char
  30 import qualified Data.List
  31 import qualified Data.Ord
  32 import qualified Data.Typeable
  33 import Data.Bits ((.&.), shiftL, (.|.))
  34 import Prelude ( (++), (+), (==), Show, show, (.), ($) )
  35 import qualified Prelude
  36 import qualified GHC.Base
  37 import qualified System.IO.Unsafe
  38
  39 getTyConTyVars :: TyCon.TyCon -> [Var.TyVar]
  40 getTyConTyVars tc =
  41   if TyCon.isFunTyCon tc
  42   then []
  43   else if TyCon.isPrimTyCon tc
  44        then []
  45        else TyCon.tyConTyVars tc
  46
  47 cmpAlts :: (CoreSyn.AltCon,[Var.Var],CoreSyn.Expr Var.Var) -> (CoreSyn.AltCon,[Var.Var],CoreSyn.Expr Var.Var) -> Data.Ord.Ordering
  48 cmpAlts (CoreSyn.DEFAULT,_,_) _   = Data.Ord.LT
  49 cmpAlts _ (CoreSyn.DEFAULT,_,_)   = Data.Ord.GT
  50 cmpAlts (a1,_,_) (a2,_,_)         = Data.Ord.compare a2 a1
  51
  52 sortAlts :: [(CoreSyn.AltCon,[Var.Var],CoreSyn.Expr Var.Var)] -> [(CoreSyn.AltCon,[Var.Var],CoreSyn.Expr Var.Var)]
  53 sortAlts x = Data.List.sortBy (\a b -> if a `CoreSyn.ltAlt` b then Data.Ord.LT else Data.Ord.GT) x
  54
  55 coreVarToWeakVar :: Var.Var -> CoreVarToWeakVarResult
  56 coreVarToWeakVar v | Id.isId     v = CVTWVR_EVar  (Var.varType v)
  57 coreVarToWeakVar v | Var.isTyVar v = CVTWVR_TyVar (coreKindToKind (Var.varType v))
  58 coreVarToWeakVar v | Coercion.isCoVar v = CVTWVR_CoVar (Prelude.fst (Coercion.coVarKind v)) (Prelude.snd (Coercion.coVarKind v))
  59 coreVarToWeakVar _                 = Prelude.error "Var.Var that is neither an expression, type variable, nor coercion variable!"
  60
  61 rawTyFunKind :: TyCon.TyCon -> ( [Kind] , Kind )
  62 rawTyFunKind tc = ((Prelude.map coreKindToKind (Prelude.take (TyCon.tyConArity tc) argk))
  63                   ,
  64                    coreKindToKind (Coercion.mkArrowKinds (Prelude.drop (TyCon.tyConArity tc) argk) retk))
  65                    where (argk,retk) = Coercion.splitKindFunTys (TyCon.tyConKind tc)
  66
  67 tyConOrTyFun :: TyCon.TyCon -> Prelude.Either TyCon.TyCon TyCon.TyCon
  68 tyConOrTyFun n =
  69    if n == TysPrim.statePrimTyCon     -- special-purpose hack treat State# as a type family since it has kind *->* but no tyvars
  70    then Prelude.Right n
  71    else if TyCon.isFamInstTyCon n
  72         then Prelude.Right n
  73         else if TyCon.isSynTyCon n
  74              then Prelude.Right n
  75              else Prelude.Left n
  76
  77 nat2int :: Nat -> Prelude.Int
  78 nat2int O     = 0
  79 nat2int (S x) = 1 + (nat2int x)
  80
  81 natToString :: Nat -> Prelude.String
  82 natToString n = show (nat2int n)
  83
  84 sanitizeForLatex :: Prelude.String -> Prelude.String
  85 sanitizeForLatex []      = []
  86 sanitizeForLatex ('_':x) = "\\_"++(sanitizeForLatex x)
  87 sanitizeForLatex ('$':x) = "\\$"++(sanitizeForLatex x)
  88 sanitizeForLatex ('#':x) = "\\#"++(sanitizeForLatex x)
  89 sanitizeForLatex (c:x)   = c:(sanitizeForLatex x)
  90
  91 kindToCoreKind :: Kind -> TypeRep.Kind
  92 kindToCoreKind KindStar          = Kind.liftedTypeKind
  93 kindToCoreKind (KindArrow k1 k2) = Kind.mkArrowKind (kindToCoreKind k1) (kindToCoreKind k2)
  94 kindToCoreKind k                 = Prelude.error ((Prelude.++)
  95                                                     "kindToCoreKind does not know how to handle kind "
  96                                                                                (kindToString k))
  97 coreKindToKind :: TypeRep.Kind -> Kind
  98 coreKindToKind k =
  99   case Kind.splitKindFunTy_maybe k of
 100       Prelude.Just (k1,k2) -> KindArrow (coreKindToKind k1) (coreKindToKind k2)
 101       Prelude.Nothing ->
 102                       if (Kind.isLiftedTypeKind k)   then KindStar
 103                  else if (Kind.isUnliftedTypeKind k) then KindStar
 104                  else if (Kind.isArgTypeKind k)      then KindStar
 105                  else if (Kind.isUbxTupleKind k)     then KindStar
 106                  else if (Kind.isOpenTypeKind k)     then KindStar
 107 --
 108 -- The "subkinding" in GHC is not dealt with in System FC, and dealing
 109 -- with it is not actually as simple as you'd think.
 110 --
 111 --                 else if (Coercion.isUnliftedTypeKind k) then KindUnliftedType
 112 --                 else if (Coercion.isOpenTypeKind k)     then KindOpenType
 113 --                 else if (Coercion.isArgTypeKind k)      then KindArgType
 114 --                 else if (Coercion.isUbxTupleKind k)     then KindUnboxedTuple
 115 --
 116                  else if (Kind.isTySuperKind k)      then Prelude.error "coreKindToKind got the kind-of-the-kind-of-types"
 117                  else                                         Prelude.error ((Prelude.++) "coreKindToKind got an unknown kind: "
 118                                                                                (Outputable.showSDoc (Outputable.ppr k)))
 119 outputableToString :: Outputable.Outputable a => a -> Prelude.String
 120 outputableToString = (\x -> Outputable.showSDocDebug (Outputable.ppr x))
 121
 122 coreViewDeep :: Type.Type -> Type.Type
 123 coreViewDeep t =
 124     case t of
 125       TypeRep.TyVarTy tv       -> TypeRep.TyVarTy tv
 126       TypeRep.FunTy arg res    -> TypeRep.FunTy (coreViewDeep arg) (coreViewDeep res)
 127       TypeRep.AppTy fun arg    -> TypeRep.AppTy (coreViewDeep fun) (coreViewDeep arg)
 128       TypeRep.ForAllTy fun arg -> TypeRep.ForAllTy fun (coreViewDeep arg)
 129       TypeRep.TyConApp tc tys  -> let t' = TypeRep.TyConApp tc (Prelude.map coreViewDeep tys)
 130                         in case Type.coreView t' of
 131                                Prelude.Nothing     -> t'
 132                                Prelude.Just    t'' -> t''
 133       TypeRep.PredTy p         -> case Type.coreView t of
 134                                Prelude.Nothing     -> TypeRep.PredTy p
 135                                Prelude.Just    t'  -> t'
 136
 137 {-# NOINLINE trace #-}
 138 trace :: Prelude.String -> a -> a
 139 trace msg x = x
 140
 141 --trace = Debug.Trace.trace
 142 --trace msg x = x
 143 --trace msg x = System.IO.Unsafe.unsafePerformIO $ Prelude.return x
 144 --trace s x = x
 145 --trace msg x = System.IO.Unsafe.unsafePerformIO $
 146 --                (Prelude.>>=) (System.IO.hPutStrLn System.IO.stdout msg) (\_ -> Prelude.return x)
 147 --trace msg x = System.IO.Unsafe.unsafePerformIO $
 148 --                (Prelude.>>=) (System.IO.hPutStr System.IO.stdout " ") (\_ -> Prelude.return x)
 149
 150 -- I'm leaving this here (commented out) in case I ever need it again)
 151 --checkTypeEquality :: Type.Type -> Type.Type -> Prelude.Bool
 152 --checkTypeEquality t1 t2 = Type.tcEqType (Type.expandTypeSynonyms t1) (Type.expandTypeSynonyms t2)