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 {-  -- used for extracting strings WITHOUT the patch for Coq
  39 bin2ascii =
  40   (\ b0 b1 b2 b3 b4 b5 b6 b7 ->
  41      let f b i = if b then 1 `shiftL` i else 0
  42      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))
  43 -}
  44
  45 getTyConTyVars :: TyCon.TyCon -> [Var.TyVar]
  46 getTyConTyVars tc =
  47   if TyCon.isFunTyCon tc
  48   then []
  49   else if TyCon.isPrimTyCon tc
  50        then []
  51        else TyCon.tyConTyVars tc
  52
  53 cmpAlts :: (CoreSyn.AltCon,[Var.Var],CoreSyn.Expr Var.Var) -> (CoreSyn.AltCon,[Var.Var],CoreSyn.Expr Var.Var) -> Data.Ord.Ordering
  54 cmpAlts (CoreSyn.DEFAULT,_,_) _   = Data.Ord.LT
  55 cmpAlts _ (CoreSyn.DEFAULT,_,_)   = Data.Ord.GT
  56 cmpAlts (a1,_,_) (a2,_,_)         = Data.Ord.compare a2 a1
  57
  58 sortAlts :: [(CoreSyn.AltCon,[Var.Var],CoreSyn.Expr Var.Var)] -> [(CoreSyn.AltCon,[Var.Var],CoreSyn.Expr Var.Var)]
  59 sortAlts x = Data.List.sortBy (\a b -> if a `CoreSyn.ltAlt` b then Data.Ord.LT else Data.Ord.GT) x
  60
  61 -- to do: this could be moved into Coq
  62 coreVarToWeakVar :: Var.Var -> WeakVar
  63 coreVarToWeakVar v | Id.isId     v = WExprVar (WeakExprVar v (errOrFail (coreTypeToWeakType (Var.varType v))))
  64  where
  65   errOrFail (OK x)    = x
  66   errOrFail (Error s) = Prelude.error s
  67 coreVarToWeakVar v | Var.isTyVar v = WTypeVar (WeakTypeVar v (coreKindToKind (Var.varType v)))
  68 coreVarToWeakVar v | Var.isCoVar v = WCoerVar (WeakCoerVar v (Prelude.error "FIXME")
  69                                                              (Prelude.error "FIXME") (Prelude.error "FIXME"))
  70 coreVarToWeakVar _                 =
  71    Prelude.error "Var.Var that is neither an expression variable, type variable, nor coercion variable!"
  72
  73 tyConOrTyFun :: TyCon.TyCon -> Prelude.Either TyCon.TyCon TyCon.TyCon
  74 tyConOrTyFun n =
  75    if n == TysPrim.statePrimTyCon     -- special-purpose hack treat State# as a type family since it has kind *->* but no tyvars
  76    then Prelude.Right n
  77    else if TyCon.isFamInstTyCon n
  78         then Prelude.Right n
  79         else Prelude.Left n
  80
  81 nat2int :: Nat -> Prelude.Int
  82 nat2int O     = 0
  83 nat2int (S x) = 1 + (nat2int x)
  84
  85 natToString :: Nat -> Prelude.String
  86 natToString n = show (nat2int n)
  87
  88 -- only needs to sanitize characters which might appear in Haskell identifiers
  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          = TypeRep.liftedTypeKind
  98 kindToCoreKind (KindArrow k1 k2) = Coercion.mkArrowKind (kindToCoreKind k1) (kindToCoreKind k2)
  99 kindToCoreKind _                 = Prelude.error "kindToCoreKind does not know how to handle that"
 100
 101 coreKindToKind :: TypeRep.Kind -> Kind
 102 coreKindToKind k =
 103   case Coercion.splitKindFunTy_maybe k of
 104       Prelude.Just (k1,k2) -> KindArrow (coreKindToKind k1) (coreKindToKind k2)
 105       Prelude.Nothing ->
 106                       if (Coercion.isLiftedTypeKind k)   then KindStar
 107                  else if (Coercion.isUnliftedTypeKind k) then KindStar
 108                  else if (Coercion.isArgTypeKind k)      then KindStar
 109                  else if (Coercion.isUbxTupleKind k)     then KindStar
 110                  else if (Coercion.isOpenTypeKind k)     then KindStar
 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                  else if (Coercion.isTySuperKind k)      then Prelude.error "coreKindToKind got the kind-of-the-kind-of-types"
 116                  else if (Coercion.isCoSuperKind k)      then Prelude.error "coreKindToKind got the kind-of-the-kind-of-coercions"
 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.showSDoc (Outputable.ppr x))
 121
 122 -- I'm leaving this here (commented out) in case I ever need it again)
 123 --checkTypeEquality :: Type.Type -> Type.Type -> Prelude.Bool
 124 --checkTypeEquality t1 t2 = Type.tcEqType (Type.expandTypeSynonyms t1) (Type.expandTypeSynonyms t2)
 125
 126 coreViewDeep :: Type.Type -> Type.Type
 127 coreViewDeep t =
 128     case t of
 129       TypeRep.TyVarTy tv       -> TypeRep.TyVarTy tv
 130       TypeRep.FunTy arg res    -> TypeRep.FunTy (coreViewDeep arg) (coreViewDeep res)
 131       TypeRep.AppTy fun arg    -> TypeRep.AppTy (coreViewDeep fun) (coreViewDeep arg)
 132       TypeRep.ForAllTy fun arg -> TypeRep.ForAllTy fun (coreViewDeep arg)
 133       TypeRep.TyConApp tc tys  -> let t' = TypeRep.TyConApp tc (Prelude.map coreViewDeep tys)
 134                         in case Type.coreView t' of
 135                                Prelude.Nothing     -> t'
 136                                Prelude.Just    t'' -> t''
 137       TypeRep.PredTy p         -> case Type.coreView t of
 138                                Prelude.Nothing     -> TypeRep.PredTy p
 139                                Prelude.Just    t'  -> t'
 140
 141 -- FIXME: cotycon applications may be oversaturated
 142 coreCoercionToWeakCoercion :: Type.Type -> WeakCoercion
 143 coreCoercionToWeakCoercion c =
 144  case c of
 145   TypeRep.TyVarTy  v     -> WCoVar (WeakCoerVar v (Prelude.error "FIXME") (Prelude.error "FIXME") (Prelude.error "FIXME"))
 146   TypeRep.AppTy    t1 t2 -> WCoApp   (coreCoercionToWeakCoercion t1) (coreCoercionToWeakCoercion t2)
 147   TypeRep.TyConApp tc t  ->
 148       case TyCon.isCoercionTyCon_maybe tc of
 149         Prelude.Nothing -> Prelude.error ((Prelude.++) "coreCoercionToWeakCoercion got " (outputableToString c))
 150         Prelude.Just (_, ctcd) ->
 151             case (ctcd,t) of
 152               (TyCon.CoTrans , [x,y]     ) -> WCoComp   (coreCoercionToWeakCoercion x) (coreCoercionToWeakCoercion y)
 153               (TyCon.CoSym   , [x]       ) -> WCoSym    (coreCoercionToWeakCoercion x)
 154               (TyCon.CoLeft  , [x]       ) -> WCoLeft   (coreCoercionToWeakCoercion x)
 155               (TyCon.CoRight , [x]       ) -> WCoLeft   (coreCoercionToWeakCoercion x)
 156 -- FIXME      (TyCon.CoUnsafe, [t1, t2 ] ) -> WCoUnsafe (coreTypeToWeakType t1) (coreTypeToWeakType t2)
 157               (TyCon.CoTrans , []        ) -> Prelude.error "CoTrans is not in post-publication-appendix SystemFC1"
 158               (TyCon.CoCsel1 , []        ) -> Prelude.error "CoCsel1 is not in post-publication-appendix SystemFC1"
 159               (TyCon.CoCsel2 , []        ) -> Prelude.error "CoCsel2 is not in post-publication-appendix SystemFC1"
 160               (TyCon.CoCselR , []        ) -> Prelude.error "CoCselR is not in post-publication-appendix SystemFC1"
 161               (TyCon.CoInst  , []        ) -> Prelude.error "CoInst  is not in post-publication-appendix SystemFC1"
 162 --              (TyCon.CoAxiom , []        ) -> Prelude.error "CoAxiom is not yet implemented (FIXME)"
 163               _ -> Prelude.error ((Prelude.++) "coreCoercionToWeakCoercion got " (outputableToString c))
 164   _ -> Prelude.error ((Prelude.++) "coreCoercionToWeakCoercion got " (outputableToString c))
 165 --  TypeRep.ForAllTy v t   -> WCoAll  (Prelude.error "FIXME") (coreTypeToWeakType t)
 166 -- FIXME   x y                                  -> WCoAppT    (coreCoercionToWeakCoercion x) (coreCoercionToWeakType y)
 167 --  CoreSyn.Type t                            -> WCoType   (coreTypeToWeakType t)
 168
 169 {-
 170 weakCoercionToCoreCoercion :: CoreCoercion -> Type.Type
 171 | WCoVar     (weakCoerVar _ _ t1 t2) => (t1,t2)
 172 | WCoType    t                       => Prelude_error "FIXME WCoType"
 173 | WCoApp     c1 c2                   => Prelude_error "FIXME WCoApp"
 174 | WCoAppT    c t                     => Prelude_error "FIXME WCoAppT"
 175 | WCoAll     k f                     => Prelude_error "FIXME WCoAll"
 176 | WCoSym     c                       => let (t2,t1) := weakCoercionTypes c in (t1,t2)
 177 | WCoComp    c1 c2                   => Prelude_error "FIXME WCoComp"
 178 | WCoLeft    c                       => Prelude_error "FIXME WCoLeft"
 179 | WCoRight   c                       => Prelude_error "FIXME WCoRight"
 180 | WCoUnsafe  t1 t2                   => (t1,t2)
 181 -}
 182
 183
 184 --trace = Debug.Trace.trace
 185 --trace msg x = x
 186 trace msg x = System.IO.Unsafe.unsafePerformIO $ Prelude.return x
 187 {-
 188 trace s x = x
 189 trace msg x = System.IO.Unsafe.unsafePerformIO $
 190                 (Prelude.>>=) (System.IO.hPutStrLn System.IO.stdout msg) (\_ -> Prelude.return x)
 191 trace msg x = System.IO.Unsafe.unsafePerformIO $
 192                 (Prelude.>>=) (System.IO.hPutStr System.IO.stdout " ") (\_ -> Prelude.return x)
 193 -}