src/Extraction-prefix.hs

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