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.Typeable
  26 import Data.Bits ((.&.), shiftL, (.|.))
  27 import Prelude ( (++), (+), (==), Show, show, Char, (.) )
  28 import qualified Prelude
  29 import qualified GHC.Base
  30
  31 -- used for extracting strings
  32 bin2ascii =
  33   (\ b0 b1 b2 b3 b4 b5 b6 b7 ->
  34      let f b i = if b then 1 `shiftL` i else 0
  35      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))
  36 --bin2ascii' =
  37 --  (\ f c -> let n = Char.code c in let h i = (n .&. (1 `shiftL` i)) /= 0 in f (h 0) (h 1) (h 2) (h 3) (h 4) (h 5) (h 6) (h 7))
  38 --shiftAscii =
  39 --  \ b c -> Data.Char.chr (((Char.code c) `shiftL` 1) .&. 255 .|. if b then 1 else 0)
  40
  41 -- crude way of casting Coq "error monad" into Haskell exceptions
  42 errOrFail :: OrError a -> a
  43 errOrFail (OK x)    = x
  44 errOrFail (Error s) = Prelude.error s
  45
  46 getTyConTyVars :: TyCon.TyCon -> [Var.TyVar]
  47 getTyConTyVars tc = if TyCon.isFunTyCon tc then [] else if TyCon.isPrimTyCon tc then [] else TyCon.tyConTyVars tc
  48
  49 sortAlts :: [(CoreSyn.AltCon,a,b)] -> [(CoreSyn.AltCon,a,b)]
  50 sortAlts x = x -- FIXME
  51
  52 -- to do: this could be moved into Coq
  53 coreVarToWeakVar :: Var.Var -> WeakVar
  54 coreVarToWeakVar v | Id.isId     v = WExprVar (WeakExprVar v (errOrFail (coreTypeToWeakType (Var.varType v))))
  55 coreVarToWeakVar v | Var.isTyVar v = WTypeVar (WeakTypeVar v (coreKindToKind (Var.varType v)))
  56 coreVarToWeakVar v | Var.isCoVar v = WCoerVar (WeakCoerVar v (Prelude.error "FIXME")
  57                                                              (Prelude.error "FIXME") (Prelude.error "FIXME"))
  58 coreVarToWeakVar _                 =
  59    Prelude.error "Var.Var that is neither an expression variable, type variable, nor coercion variable!"
  60
  61 tyConOrTyFun :: TyCon.TyCon -> Prelude.Either TyCon.TyCon TyCon.TyCon
  62 --FIXME: go back to this
  63 --tyConOrTyFun n = if TyCon.isFamInstTyCon n then Prelude.Left n else Prelude.Right n
  64 tyConOrTyFun n = if TyCon.isFamInstTyCon n then Prelude.Left n else Prelude.Left n
  65
  66 tyFunResultKind :: TyCon.TyCon -> Kind
  67 tyFunResultKind tc = coreKindToKind (TyCon.tyConKind tc)
  68
  69 nat2int :: Nat -> Prelude.Int
  70 nat2int O     = 0
  71 nat2int (S x) = 1 + (nat2int x)
  72
  73 natToString :: Nat -> Prelude.String
  74 natToString n = show (nat2int n)
  75
  76 -- only needs to sanitize characters which might appear in Haskell identifiers
  77 sanitizeForLatex :: Prelude.String -> Prelude.String
  78 sanitizeForLatex []    = []
  79 sanitizeForLatex ('_':x) = "\\_"++(sanitizeForLatex x)
  80 sanitizeForLatex ('$':x) = "\\$"++(sanitizeForLatex x)
  81 sanitizeForLatex ('#':x) = "\\#"++(sanitizeForLatex x)
  82 sanitizeForLatex (c:x) = c:(sanitizeForLatex x)
  83
  84 coreKindToKind :: TypeRep.Kind -> Kind
  85 coreKindToKind k =
  86   case Coercion.splitKindFunTy_maybe k of
  87       Prelude.Just (k1,k2) -> KindTypeFunction (coreKindToKind k1) (coreKindToKind k2)
  88       Prelude.Nothing ->
  89                       if (Coercion.isLiftedTypeKind k)   then KindType
  90                  else if (Coercion.isUnliftedTypeKind k) then KindUnliftedType
  91                  else if (Coercion.isOpenTypeKind k)     then KindOpenType
  92                  else if (Coercion.isArgTypeKind k)      then KindArgType
  93                  else if (Coercion.isUbxTupleKind k)     then KindUnboxedTuple
  94                  else if (Coercion.isTySuperKind k)      then Prelude.error "coreKindToKind got the kind-of-the-kind-of-types"
  95                  else if (Coercion.isCoSuperKind k)      then Prelude.error "coreKindToKind got the kind-of-the-kind-of-coercions"
  96                  else                                         Prelude.error ((Prelude.++) "coreKindToKind got an unknown kind: "
  97                                                                                (Outputable.showSDoc (Outputable.ppr k)))
  98 outputableToString :: Outputable.Outputable a => a -> Prelude.String
  99 outputableToString = (\x -> Outputable.showSDoc (Outputable.ppr x))
 100
 101 -- TO DO: I think we can remove this now
 102 checkTypeEquality :: Type.Type -> Type.Type -> Prelude.Bool
 103 checkTypeEquality t1 t2 = Type.tcEqType (Type.expandTypeSynonyms t1) (Type.expandTypeSynonyms t2)
 104
 105 --showType t = outputableToString (Type.expandTypeSynonyms t)
 106 showType t = outputableToString (coreViewDeep t)
 107
 108 coreViewDeep :: Type.Type -> Type.Type
 109 coreViewDeep t =
 110     case t of
 111       TypeRep.TyVarTy tv       -> TypeRep.TyVarTy tv
 112       TypeRep.FunTy arg res    -> TypeRep.FunTy (coreViewDeep arg) (coreViewDeep res)
 113       TypeRep.AppTy fun arg    -> TypeRep.AppTy (coreViewDeep fun) (coreViewDeep arg)
 114       TypeRep.ForAllTy fun arg -> TypeRep.ForAllTy fun (coreViewDeep arg)
 115       TypeRep.TyConApp tc tys  -> let t' = TypeRep.TyConApp tc (Prelude.map coreViewDeep tys)
 116                         in case Type.coreView t' of
 117                                Prelude.Nothing     -> t'
 118                                Prelude.Just    t'' -> t''
 119       TypeRep.PredTy p         -> case Type.coreView t of
 120                                Prelude.Nothing     -> TypeRep.PredTy p
 121                                Prelude.Just    t'  -> t'
 122
 123 -- FIXME: cotycon applications may be oversaturated
 124 coreCoercionToWeakCoercion :: Type.Type -> WeakCoercion
 125 coreCoercionToWeakCoercion c =
 126  case c of
 127   TypeRep.TyVarTy  v     -> WCoVar (WeakCoerVar v (Prelude.error "FIXME") (Prelude.error "FIXME") (Prelude.error "FIXME"))
 128   TypeRep.AppTy    t1 t2 -> WCoApp   (coreCoercionToWeakCoercion t1) (coreCoercionToWeakCoercion t2)
 129   TypeRep.TyConApp tc t  ->
 130       case TyCon.isCoercionTyCon_maybe tc of
 131         Prelude.Nothing -> Prelude.error ((Prelude.++) "coreCoercionToWeakCoercion got " (outputableToString c))
 132         Prelude.Just (_, ctcd) ->
 133             case (ctcd,t) of
 134               (TyCon.CoTrans , [x,y]     ) -> WCoComp   (coreCoercionToWeakCoercion x) (coreCoercionToWeakCoercion y)
 135               (TyCon.CoSym   , [x]       ) -> WCoSym    (coreCoercionToWeakCoercion x)
 136               (TyCon.CoLeft  , [x]       ) -> WCoLeft   (coreCoercionToWeakCoercion x)
 137               (TyCon.CoRight , [x]       ) -> WCoLeft   (coreCoercionToWeakCoercion x)
 138 -- FIXME      (TyCon.CoUnsafe, [t1, t2 ] ) -> WCoUnsafe (coreTypeToWeakType t1) (coreTypeToWeakType t2)
 139               (TyCon.CoTrans , []        ) -> Prelude.error "CoTrans is not in post-publication-appendix SystemFC1"
 140               (TyCon.CoCsel1 , []        ) -> Prelude.error "CoCsel1 is not in post-publication-appendix SystemFC1"
 141               (TyCon.CoCsel2 , []        ) -> Prelude.error "CoCsel2 is not in post-publication-appendix SystemFC1"
 142               (TyCon.CoCselR , []        ) -> Prelude.error "CoCselR is not in post-publication-appendix SystemFC1"
 143               (TyCon.CoInst  , []        ) -> Prelude.error "CoInst  is not in post-publication-appendix SystemFC1"
 144 --              (TyCon.CoAxiom , []        ) -> Prelude.error "CoAxiom is not yet implemented (FIXME)"
 145               _ -> Prelude.error ((Prelude.++) "coreCoercionToWeakCoercion got " (outputableToString c))
 146   _ -> Prelude.error ((Prelude.++) "coreCoercionToWeakCoercion got " (outputableToString c))
 147 --  TypeRep.ForAllTy v t   -> WCoAll  (Prelude.error "FIXME") (coreTypeToWeakType t)
 148 -- FIXME   x y                                  -> WCoAppT    (coreCoercionToWeakCoercion x) (coreCoercionToWeakType y)
 149 --  CoreSyn.Type t                            -> WCoType   (coreTypeToWeakType t)
 150
 151 {-
 152 weakCoercionToCoreCoercion :: CoreCoercion -> Type.Type
 153 | WCoVar     (weakCoerVar _ _ t1 t2) => (t1,t2)
 154 | WCoType    t                       => Prelude_error "FIXME WCoType"
 155 | WCoApp     c1 c2                   => Prelude_error "FIXME WCoApp"
 156 | WCoAppT    c t                     => Prelude_error "FIXME WCoAppT"
 157 | WCoAll     k f                     => Prelude_error "FIXME WCoAll"
 158 | WCoSym     c                       => let (t2,t1) := weakCoercionTypes c in (t1,t2)
 159 | WCoComp    c1 c2                   => Prelude_error "FIXME WCoComp"
 160 | WCoLeft    c                       => Prelude_error "FIXME WCoLeft"
 161 | WCoRight   c                       => Prelude_error "FIXME WCoRight"
 162 | WCoUnsafe  t1 t2                   => (t1,t2)
 163 -}