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 CoreUtils
  23 import qualified Class
  24 import qualified Data.Char
  25 import qualified Data.List
  26 import qualified Data.Ord
  27 import qualified Data.Typeable
  28 import Data.Bits ((.&.), shiftL, (.|.))
  29 import Prelude ( (++), (+), (==), Show, show, Char, (.) )
  30 import qualified Prelude
  31 import qualified GHC.Base
  32
  33 -- used for extracting strings
  34 bin2ascii =
  35   (\ b0 b1 b2 b3 b4 b5 b6 b7 ->
  36      let f b i = if b then 1 `shiftL` i else 0
  37      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))
  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 sortAlts :: [(CoreSyn.AltCon,[Var.Var],CoreSyn.Expr Var.Var)] -> [(CoreSyn.AltCon,[Var.Var],CoreSyn.Expr Var.Var)]
  48 sortAlts x = Data.List.sortBy (\(a1,_,_) -> \(a2,_,_) -> Data.Ord.compare a1 a2) x
  49
  50 -- to do: this could be moved into Coq
  51 coreVarToWeakVar :: Var.Var -> WeakVar
  52 coreVarToWeakVar v | Id.isId     v = WExprVar (WeakExprVar v (errOrFail (coreTypeToWeakType (Var.varType v))))
  53  where
  54   errOrFail (OK x)    = x
  55   errOrFail (Error s) = Prelude.error s
  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 tyConOrTyFun :: TyCon.TyCon -> Prelude.Either TyCon.TyCon TyCon.TyCon
  63 tyConOrTyFun n =
  64    if n == TysPrim.statePrimTyCon     -- special-purpose hack treat State# as a type family since it has kind *->* but no tyvars
  65    then Prelude.Right n
  66    else if TyCon.isFamInstTyCon n
  67         then Prelude.Right n
  68         else Prelude.Left n
  69
  70 nat2int :: Nat -> Prelude.Int
  71 nat2int O     = 0
  72 nat2int (S x) = 1 + (nat2int x)
  73
  74 natToString :: Nat -> Prelude.String
  75 natToString n = show (nat2int n)
  76
  77 -- only needs to sanitize characters which might appear in Haskell identifiers
  78 sanitizeForLatex :: Prelude.String -> Prelude.String
  79 sanitizeForLatex []      = []
  80 sanitizeForLatex ('_':x) = "\\_"++(sanitizeForLatex x)
  81 sanitizeForLatex ('$':x) = "\\$"++(sanitizeForLatex x)
  82 sanitizeForLatex ('#':x) = "\\#"++(sanitizeForLatex x)
  83 sanitizeForLatex (c:x)   = c:(sanitizeForLatex x)
  84
  85 coreKindToKind :: TypeRep.Kind -> Kind
  86 coreKindToKind k =
  87   case Coercion.splitKindFunTy_maybe k of
  88       Prelude.Just (k1,k2) -> KindTypeFunction (coreKindToKind k1) (coreKindToKind k2)
  89       Prelude.Nothing ->
  90                       if (Coercion.isLiftedTypeKind k)   then KindType
  91                  else if (Coercion.isUnliftedTypeKind k) then KindType
  92                  else if (Coercion.isArgTypeKind k)      then KindType
  93                  else if (Coercion.isUbxTupleKind k)     then KindType
  94                  else if (Coercion.isOpenTypeKind k)     then KindType
  95 --                 else if (Coercion.isUnliftedTypeKind k) then KindUnliftedType
  96 --                 else if (Coercion.isOpenTypeKind k)     then KindOpenType
  97 --                 else if (Coercion.isArgTypeKind k)      then KindArgType
  98 --                 else if (Coercion.isUbxTupleKind k)     then KindUnboxedTuple
  99                  else if (Coercion.isTySuperKind k)      then Prelude.error "coreKindToKind got the kind-of-the-kind-of-types"
 100                  else if (Coercion.isCoSuperKind k)      then Prelude.error "coreKindToKind got the kind-of-the-kind-of-coercions"
 101                  else                                         Prelude.error ((Prelude.++) "coreKindToKind got an unknown kind: "
 102                                                                                (Outputable.showSDoc (Outputable.ppr k)))
 103 outputableToString :: Outputable.Outputable a => a -> Prelude.String
 104 outputableToString = (\x -> Outputable.showSDoc (Outputable.ppr x))
 105
 106 -- I'm leaving this here (commented out) in case I ever need it again)
 107 --checkTypeEquality :: Type.Type -> Type.Type -> Prelude.Bool
 108 --checkTypeEquality t1 t2 = Type.tcEqType (Type.expandTypeSynonyms t1) (Type.expandTypeSynonyms t2)
 109
 110 coreViewDeep :: Type.Type -> Type.Type
 111 coreViewDeep t =
 112     case t of
 113       TypeRep.TyVarTy tv       -> TypeRep.TyVarTy tv
 114       TypeRep.FunTy arg res    -> TypeRep.FunTy (coreViewDeep arg) (coreViewDeep res)
 115       TypeRep.AppTy fun arg    -> TypeRep.AppTy (coreViewDeep fun) (coreViewDeep arg)
 116       TypeRep.ForAllTy fun arg -> TypeRep.ForAllTy fun (coreViewDeep arg)
 117       TypeRep.TyConApp tc tys  -> let t' = TypeRep.TyConApp tc (Prelude.map coreViewDeep tys)
 118                         in case Type.coreView t' of
 119                                Prelude.Nothing     -> t'
 120                                Prelude.Just    t'' -> t''
 121       TypeRep.PredTy p         -> case Type.coreView t of
 122                                Prelude.Nothing     -> TypeRep.PredTy p
 123                                Prelude.Just    t'  -> t'
 124
 125 -- FIXME: cotycon applications may be oversaturated
 126 coreCoercionToWeakCoercion :: Type.Type -> WeakCoercion
 127 coreCoercionToWeakCoercion c =
 128  case c of
 129   TypeRep.TyVarTy  v     -> WCoVar (WeakCoerVar v (Prelude.error "FIXME") (Prelude.error "FIXME") (Prelude.error "FIXME"))
 130   TypeRep.AppTy    t1 t2 -> WCoApp   (coreCoercionToWeakCoercion t1) (coreCoercionToWeakCoercion t2)
 131   TypeRep.TyConApp tc t  ->
 132       case TyCon.isCoercionTyCon_maybe tc of
 133         Prelude.Nothing -> Prelude.error ((Prelude.++) "coreCoercionToWeakCoercion got " (outputableToString c))
 134         Prelude.Just (_, ctcd) ->
 135             case (ctcd,t) of
 136               (TyCon.CoTrans , [x,y]     ) -> WCoComp   (coreCoercionToWeakCoercion x) (coreCoercionToWeakCoercion y)
 137               (TyCon.CoSym   , [x]       ) -> WCoSym    (coreCoercionToWeakCoercion x)
 138               (TyCon.CoLeft  , [x]       ) -> WCoLeft   (coreCoercionToWeakCoercion x)
 139               (TyCon.CoRight , [x]       ) -> WCoLeft   (coreCoercionToWeakCoercion x)
 140 -- FIXME      (TyCon.CoUnsafe, [t1, t2 ] ) -> WCoUnsafe (coreTypeToWeakType t1) (coreTypeToWeakType t2)
 141               (TyCon.CoTrans , []        ) -> Prelude.error "CoTrans is not in post-publication-appendix SystemFC1"
 142               (TyCon.CoCsel1 , []        ) -> Prelude.error "CoCsel1 is not in post-publication-appendix SystemFC1"
 143               (TyCon.CoCsel2 , []        ) -> Prelude.error "CoCsel2 is not in post-publication-appendix SystemFC1"
 144               (TyCon.CoCselR , []        ) -> Prelude.error "CoCselR is not in post-publication-appendix SystemFC1"
 145               (TyCon.CoInst  , []        ) -> Prelude.error "CoInst  is not in post-publication-appendix SystemFC1"
 146 --              (TyCon.CoAxiom , []        ) -> Prelude.error "CoAxiom is not yet implemented (FIXME)"
 147               _ -> Prelude.error ((Prelude.++) "coreCoercionToWeakCoercion got " (outputableToString c))
 148   _ -> Prelude.error ((Prelude.++) "coreCoercionToWeakCoercion got " (outputableToString c))
 149 --  TypeRep.ForAllTy v t   -> WCoAll  (Prelude.error "FIXME") (coreTypeToWeakType t)
 150 -- FIXME   x y                                  -> WCoAppT    (coreCoercionToWeakCoercion x) (coreCoercionToWeakType y)
 151 --  CoreSyn.Type t                            -> WCoType   (coreTypeToWeakType t)
 152
 153 {-
 154 weakCoercionToCoreCoercion :: CoreCoercion -> Type.Type
 155 | WCoVar     (weakCoerVar _ _ t1 t2) => (t1,t2)
 156 | WCoType    t                       => Prelude_error "FIXME WCoType"
 157 | WCoApp     c1 c2                   => Prelude_error "FIXME WCoApp"
 158 | WCoAppT    c t                     => Prelude_error "FIXME WCoAppT"
 159 | WCoAll     k f                     => Prelude_error "FIXME WCoAll"
 160 | WCoSym     c                       => let (t2,t1) := weakCoercionTypes c in (t1,t2)
 161 | WCoComp    c1 c2                   => Prelude_error "FIXME WCoComp"
 162 | WCoLeft    c                       => Prelude_error "FIXME WCoLeft"
 163 | WCoRight   c                       => Prelude_error "FIXME WCoRight"
 164 | WCoUnsafe  t1 t2                   => (t1,t2)
 165 -}