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