src/Extraction-prefix.hs

   1 module CoqPass ( coqPassCoreToString, coqPassCoreToCore )
   2 where
   3 import qualified Unique
   4 import qualified UniqSupply
   5 import qualified MkCore
   6 import qualified TysWiredIn
   7 import qualified TysPrim
   8 import qualified Outputable
   9 import qualified PrelNames
  10 import qualified OccName
  11 import qualified Name
  12 import qualified Literal
  13 import qualified Type
  14 import qualified TypeRep
  15 import qualified DataCon
  16 import qualified TyCon
  17 import qualified Coercion
  18 import qualified Var
  19 import qualified Id
  20 import qualified FastString
  21 import qualified BasicTypes
  22 import qualified DataCon
  23 import qualified CoreSyn
  24 import qualified CoreUtils
  25 import qualified Class
  26 import qualified Data.Char
  27 import qualified Data.List
  28 import qualified Data.Ord
  29 import qualified Data.Typeable
  30 import Data.Bits ((.&.), shiftL, (.|.))
  31 import Prelude ( (++), (+), (==), Show, show, Char, (.), ($) )
  32 import qualified Prelude
  33 import qualified Debug.Trace
  34 import qualified GHC.Base
  35 import qualified System.IO
  36 import qualified System.IO.Unsafe
  37
  38 getTyConTyVars :: TyCon.TyCon -> [Var.TyVar]
  39 getTyConTyVars tc =
  40   if TyCon.isFunTyCon tc
  41   then []
  42   else if TyCon.isPrimTyCon tc
  43        then []
  44        else TyCon.tyConTyVars tc
  45
  46 cmpAlts :: (CoreSyn.AltCon,[Var.Var],CoreSyn.Expr Var.Var) -> (CoreSyn.AltCon,[Var.Var],CoreSyn.Expr Var.Var) -> Data.Ord.Ordering
  47 cmpAlts (CoreSyn.DEFAULT,_,_) _   = Data.Ord.LT
  48 cmpAlts _ (CoreSyn.DEFAULT,_,_)   = Data.Ord.GT
  49 cmpAlts (a1,_,_) (a2,_,_)         = Data.Ord.compare a2 a1
  50
  51 sortAlts :: [(CoreSyn.AltCon,[Var.Var],CoreSyn.Expr Var.Var)] -> [(CoreSyn.AltCon,[Var.Var],CoreSyn.Expr Var.Var)]
  52 sortAlts x = Data.List.sortBy (\a b -> if a `CoreSyn.ltAlt` b then Data.Ord.LT else Data.Ord.GT) x
  53
  54 coreVarToWeakVar :: Var.Var -> WeakVar
  55 coreVarToWeakVar v | Id.isId     v = WExprVar (WeakExprVar v (errOrFail (coreTypeToWeakType (Var.varType v))))
  56 coreVarToWeakVar v | Var.isTyVar v = WTypeVar (WeakTypeVar v (coreKindToKind (Var.varType v)))
  57 coreVarToWeakVar v | Var.isCoVar v = WCoerVar (WeakCoerVar v (Prelude.error "FIXME")
  58                                                              (Prelude.error "FIXME") (Prelude.error "FIXME"))
  59 coreVarToWeakVar _                 =
  60    Prelude.error "Var.Var that is neither an expression variable, type variable, nor coercion variable!"
  61
  62 errOrFail (OK x)    = x
  63 errOrFail (Error s) = Prelude.error s
  64
  65 tyConOrTyFun :: TyCon.TyCon -> Prelude.Either TyCon.TyCon TyCon.TyCon
  66 tyConOrTyFun n =
  67    if n == TysPrim.statePrimTyCon     -- special-purpose hack treat State# as a type family since it has kind *->* but no tyvars
  68    then Prelude.Right n
  69    else if TyCon.isFamInstTyCon n
  70         then Prelude.Right n
  71         else Prelude.Left n
  72
  73 nat2int :: Nat -> Prelude.Int
  74 nat2int O     = 0
  75 nat2int (S x) = 1 + (nat2int x)
  76
  77 natToString :: Nat -> Prelude.String
  78 natToString n = show (nat2int n)
  79
  80 sanitizeForLatex :: Prelude.String -> Prelude.String
  81 sanitizeForLatex []      = []
  82 sanitizeForLatex ('_':x) = "\\_"++(sanitizeForLatex x)
  83 sanitizeForLatex ('$':x) = "\\$"++(sanitizeForLatex x)
  84 sanitizeForLatex ('#':x) = "\\#"++(sanitizeForLatex x)
  85 sanitizeForLatex (c:x)   = c:(sanitizeForLatex x)
  86
  87 kindToCoreKind :: Kind -> TypeRep.Kind
  88 kindToCoreKind KindStar          = TypeRep.liftedTypeKind
  89 kindToCoreKind (KindArrow k1 k2) = Coercion.mkArrowKind (kindToCoreKind k1) (kindToCoreKind k2)
  90 kindToCoreKind _                 = Prelude.error "kindToCoreKind does not know how to handle that"
  91
  92 coreKindToKind :: TypeRep.Kind -> Kind
  93 coreKindToKind k =
  94   case Coercion.splitKindFunTy_maybe k of
  95       Prelude.Just (k1,k2) -> KindArrow (coreKindToKind k1) (coreKindToKind k2)
  96       Prelude.Nothing ->
  97                       if (Coercion.isLiftedTypeKind k)   then KindStar
  98                  else if (Coercion.isUnliftedTypeKind k) then KindStar
  99                  else if (Coercion.isArgTypeKind k)      then KindStar
 100                  else if (Coercion.isUbxTupleKind k)     then KindStar
 101                  else if (Coercion.isOpenTypeKind k)     then KindStar
 102 --
 103 -- The "subkinding" in GHC is not dealt with in System FC, and dealing
 104 -- with it is not actually as simple as you'd think.
 105 --
 106 --                 else if (Coercion.isUnliftedTypeKind k) then KindUnliftedType
 107 --                 else if (Coercion.isOpenTypeKind k)     then KindOpenType
 108 --                 else if (Coercion.isArgTypeKind k)      then KindArgType
 109 --                 else if (Coercion.isUbxTupleKind k)     then KindUnboxedTuple
 110 --
 111                  else if (Coercion.isTySuperKind k)      then Prelude.error "coreKindToKind got the kind-of-the-kind-of-types"
 112                  else if (Coercion.isCoSuperKind k)      then Prelude.error "coreKindToKind got the kind-of-the-kind-of-coercions"
 113                  else                                         Prelude.error ((Prelude.++) "coreKindToKind got an unknown kind: "
 114                                                                                (Outputable.showSDoc (Outputable.ppr k)))
 115 outputableToString :: Outputable.Outputable a => a -> Prelude.String
 116 outputableToString = (\x -> Outputable.showSDoc (Outputable.ppr x))
 117
 118 coreViewDeep :: Type.Type -> Type.Type
 119 coreViewDeep t =
 120     case t of
 121       TypeRep.TyVarTy tv       -> TypeRep.TyVarTy tv
 122       TypeRep.FunTy arg res    -> TypeRep.FunTy (coreViewDeep arg) (coreViewDeep res)
 123       TypeRep.AppTy fun arg    -> TypeRep.AppTy (coreViewDeep fun) (coreViewDeep arg)
 124       TypeRep.ForAllTy fun arg -> TypeRep.ForAllTy fun (coreViewDeep arg)
 125       TypeRep.TyConApp tc tys  -> let t' = TypeRep.TyConApp tc (Prelude.map coreViewDeep tys)
 126                         in case Type.coreView t' of
 127                                Prelude.Nothing     -> t'
 128                                Prelude.Just    t'' -> t''
 129       TypeRep.PredTy p         -> case Type.coreView t of
 130                                Prelude.Nothing     -> TypeRep.PredTy p
 131                                Prelude.Just    t'  -> t'
 132
 133 coreCoercionToWeakCoercion :: Type.Type -> WeakCoercion
 134 coreCoercionToWeakCoercion c =
 135  WCoUnsafe (errOrFail (coreTypeToWeakType t1)) (errOrFail (coreTypeToWeakType t2))
 136    where
 137     (t1,t2) = Coercion.coercionKind c
 138 {-
 139 -- REMEMBER: cotycon applications may be oversaturated
 140  case c of
 141   TypeRep.TyVarTy  v     -> WCoVar (WeakCoerVar v (Prelude.error "FIXME") (Prelude.error "FIXME") (Prelude.error "FIXME"))
 142   TypeRep.AppTy    t1 t2 -> WCoApp   (coreCoercionToWeakCoercion t1) (coreCoercionToWeakCoercion t2)
 143   TypeRep.TyConApp tc t  ->
 144       case TyCon.isCoercionTyCon_maybe tc of
 145         Prelude.Nothing -> Prelude.error ((Prelude.++) "coreCoercionToWeakCoercion got isCoercionTyCon_maybe " (outputableToString c))
 146         Prelude.Just (_, ctcd) ->
 147             case (ctcd,t) of
 148               (TyCon.CoTrans , [x,y]     ) -> WCoComp   (coreCoercionToWeakCoercion x) (coreCoercionToWeakCoercion y)
 149               (TyCon.CoSym   , [x]       ) -> WCoSym    (coreCoercionToWeakCoercion x)
 150               (TyCon.CoLeft  , [x]       ) -> WCoLeft   (coreCoercionToWeakCoercion x)
 151               (TyCon.CoRight , [x]       ) -> WCoLeft   (coreCoercionToWeakCoercion x)
 152 --            (TyCon.CoUnsafe, [t1, t2 ] ) -> WCoUnsafe (coreTypeToWeakType t1) (coreTypeToWeakType t2)
 153               (TyCon.CoTrans , []        ) -> Prelude.error "CoTrans is not in post-publication-appendix SystemFC1"
 154               (TyCon.CoCsel1 , []        ) -> Prelude.error "CoCsel1 is not in post-publication-appendix SystemFC1"
 155               (TyCon.CoCsel2 , []        ) -> Prelude.error "CoCsel2 is not in post-publication-appendix SystemFC1"
 156               (TyCon.CoCselR , []        ) -> Prelude.error "CoCselR is not in post-publication-appendix SystemFC1"
 157               (TyCon.CoInst  , []        ) -> Prelude.error "CoInst  is not in post-publication-appendix SystemFC1"
 158               (TyCon.CoAxiom _ _ _ , _   ) -> Prelude.error "CoAxiom is not yet implemented (FIXME)"
 159               ( _, [ t1 , t2 ]) -> WCoUnsafe (errOrFail (coreTypeToWeakType t1)) (errOrFail (coreTypeToWeakType t2))
 160               _ -> Prelude.error ((Prelude.++) "coreCoercionToWeakCoercion got " (outputableToString c))
 161   _ -> Prelude.error ((Prelude.++) "coreCoercionToWeakCoercion got " (outputableToString c))
 162 -}
 163 --  TypeRep.ForAllTy v t   -> WCoAll  (Prelude.error "FIXME") (coreTypeToWeakType t)
 164 -- FIXME   x y                                  -> WCoAppT    (coreCoercionToWeakCoercion x) (coreCoercionToWeakType y)
 165 --  CoreSyn.Type t                            -> WCoType   (coreTypeToWeakType t)
 166
 167 {-
 168 weakCoercionToCoreCoercion :: CoreCoercion -> Type.Type
 169 | WCoVar     (weakCoerVar _ _ t1 t2) => (t1,t2)
 170 | WCoType    t                       => Prelude_error "FIXME WCoType"
 171 | WCoApp     c1 c2                   => Prelude_error "FIXME WCoApp"
 172 | WCoAppT    c t                     => Prelude_error "FIXME WCoAppT"
 173 | WCoAll     k f                     => Prelude_error "FIXME WCoAll"
 174 | WCoSym     c                       => let (t2,t1) := weakCoercionTypes c in (t1,t2)
 175 | WCoComp    c1 c2                   => Prelude_error "FIXME WCoComp"
 176 | WCoLeft    c                       => Prelude_error "FIXME WCoLeft"
 177 | WCoRight   c                       => Prelude_error "FIXME WCoRight"
 178 | WCoUnsafe  t1 t2                   => (t1,t2)
 179 -}
 180
 181
 182 --trace = Debug.Trace.trace
 183 --trace msg x = x
 184 trace msg x = System.IO.Unsafe.unsafePerformIO $ Prelude.return x
 185 {-
 186 trace s x = x
 187 trace msg x = System.IO.Unsafe.unsafePerformIO $
 188                 (Prelude.>>=) (System.IO.hPutStrLn System.IO.stdout msg) (\_ -> Prelude.return x)
 189 trace msg x = System.IO.Unsafe.unsafePerformIO $
 190                 (Prelude.>>=) (System.IO.hPutStr System.IO.stdout " ") (\_ -> Prelude.return x)
 191 -}
 192
 193 {-  -- used for extracting strings WITHOUT the patch for Coq
 194 bin2ascii =
 195   (\ b0 b1 b2 b3 b4 b5 b6 b7 ->
 196      let f b i = if b then 1 `shiftL` i else 0
 197      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))
 198 -}
 199
 200 -- I'm leaving this here (commented out) in case I ever need it again)
 201 --checkTypeEquality :: Type.Type -> Type.Type -> Prelude.Bool
 202 --checkTypeEquality t1 t2 = Type.tcEqType (Type.expandTypeSynonyms t1) (Type.expandTypeSynonyms t2)