src/Extraction-prefix.hs

   1 {-# OPTIONS_GHC -fno-warn-unused-matches -fno-warn-unused-binds -fno-warn-unused-imports #-}
   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, (.), ($) )
  33 import qualified Prelude
  34 import qualified GHC.Base
  35 import qualified System.IO.Unsafe
  36
  37 getTyConTyVars :: TyCon.TyCon -> [Var.TyVar]
  38 getTyConTyVars tc =
  39   if TyCon.isFunTyCon tc
  40   then []
  41   else if TyCon.isPrimTyCon tc
  42        then []
  43        else TyCon.tyConTyVars tc
  44
  45 cmpAlts :: (CoreSyn.AltCon,[Var.Var],CoreSyn.Expr Var.Var) -> (CoreSyn.AltCon,[Var.Var],CoreSyn.Expr Var.Var) -> Data.Ord.Ordering
  46 cmpAlts (CoreSyn.DEFAULT,_,_) _   = Data.Ord.LT
  47 cmpAlts _ (CoreSyn.DEFAULT,_,_)   = Data.Ord.GT
  48 cmpAlts (a1,_,_) (a2,_,_)         = Data.Ord.compare a2 a1
  49
  50 sortAlts :: [(CoreSyn.AltCon,[Var.Var],CoreSyn.Expr Var.Var)] -> [(CoreSyn.AltCon,[Var.Var],CoreSyn.Expr Var.Var)]
  51 sortAlts x = Data.List.sortBy (\a b -> if a `CoreSyn.ltAlt` b then Data.Ord.LT else Data.Ord.GT) x
  52
  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
  57   = WCoerVar (WeakCoerVar v
  58                           (errOrFail (coreTypeToWeakType (Prelude.fst (Coercion.coercionKind (Var.varType v)))))
  59                           (errOrFail (coreTypeToWeakType (Prelude.snd (Coercion.coercionKind (Var.varType v))))))
  60 coreVarToWeakVar _                 =
  61    Prelude.error "Var.Var that is neither an expression variable, type variable, nor coercion variable!"
  62
  63 errOrFail :: OrError t -> t
  64 errOrFail (OK x)    = x
  65 errOrFail (Error s) = Prelude.error s
  66
  67 rawTyFunKind :: TyCon.TyCon -> ( [Kind] , Kind )
  68 rawTyFunKind tc = ((Prelude.map coreKindToKind (Prelude.take (TyCon.tyConArity tc) argk))
  69                   ,
  70                    coreKindToKind (Coercion.mkArrowKinds (Prelude.drop (TyCon.tyConArity tc) argk) retk))
  71                    where (argk,retk) = Coercion.splitKindFunTys (TyCon.tyConKind tc)
  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 if TyCon.isSynTyCon n
  80              then Prelude.Right n
  81              else Prelude.Left n
  82
  83 nat2int :: Nat -> Prelude.Int
  84 nat2int O     = 0
  85 nat2int (S x) = 1 + (nat2int x)
  86
  87 natToString :: Nat -> Prelude.String
  88 natToString n = show (nat2int n)
  89
  90 sanitizeForLatex :: Prelude.String -> Prelude.String
  91 sanitizeForLatex []      = []
  92 sanitizeForLatex ('_':x) = "\\_"++(sanitizeForLatex x)
  93 sanitizeForLatex ('$':x) = "\\$"++(sanitizeForLatex x)
  94 sanitizeForLatex ('#':x) = "\\#"++(sanitizeForLatex x)
  95 sanitizeForLatex (c:x)   = c:(sanitizeForLatex x)
  96
  97 kindToCoreKind :: Kind -> TypeRep.Kind
  98 kindToCoreKind KindStar          = TypeRep.liftedTypeKind
  99 kindToCoreKind (KindArrow k1 k2) = Coercion.mkArrowKind (kindToCoreKind k1) (kindToCoreKind k2)
 100 kindToCoreKind k                 = Prelude.error ((Prelude.++)
 101                                                     "kindToCoreKind does not know how to handle kind "
 102                                                                                (kindToString k))
 103 coreKindToKind :: TypeRep.Kind -> Kind
 104 coreKindToKind k =
 105   case Coercion.splitKindFunTy_maybe k of
 106       Prelude.Just (k1,k2) -> KindArrow (coreKindToKind k1) (coreKindToKind k2)
 107       Prelude.Nothing ->
 108                       if (Coercion.isLiftedTypeKind k)   then KindStar
 109                  else if (Coercion.isUnliftedTypeKind k) then KindStar
 110                  else if (Coercion.isArgTypeKind k)      then KindStar
 111                  else if (Coercion.isUbxTupleKind k)     then KindStar
 112                  else if (Coercion.isOpenTypeKind k)     then KindStar
 113 --
 114 -- The "subkinding" in GHC is not dealt with in System FC, and dealing
 115 -- with it is not actually as simple as you'd think.
 116 --
 117 --                 else if (Coercion.isUnliftedTypeKind k) then KindUnliftedType
 118 --                 else if (Coercion.isOpenTypeKind k)     then KindOpenType
 119 --                 else if (Coercion.isArgTypeKind k)      then KindArgType
 120 --                 else if (Coercion.isUbxTupleKind k)     then KindUnboxedTuple
 121 --
 122                  else if (Coercion.isTySuperKind k)      then Prelude.error "coreKindToKind got the kind-of-the-kind-of-types"
 123                  else if (Coercion.isCoSuperKind k)      then Prelude.error "coreKindToKind got the kind-of-the-kind-of-coercions"
 124                  else                                         Prelude.error ((Prelude.++) "coreKindToKind got an unknown kind: "
 125                                                                                (Outputable.showSDoc (Outputable.ppr k)))
 126 outputableToString :: Outputable.Outputable a => a -> Prelude.String
 127 outputableToString = (\x -> Outputable.showSDocDebug (Outputable.ppr x))
 128
 129 coreViewDeep :: Type.Type -> Type.Type
 130 coreViewDeep t =
 131     case t of
 132       TypeRep.TyVarTy tv       -> TypeRep.TyVarTy tv
 133       TypeRep.FunTy arg res    -> TypeRep.FunTy (coreViewDeep arg) (coreViewDeep res)
 134       TypeRep.AppTy fun arg    -> TypeRep.AppTy (coreViewDeep fun) (coreViewDeep arg)
 135       TypeRep.ForAllTy fun arg -> TypeRep.ForAllTy fun (coreViewDeep arg)
 136       TypeRep.TyConApp tc tys  -> let t' = TypeRep.TyConApp tc (Prelude.map coreViewDeep tys)
 137                         in case Type.coreView t' of
 138                                Prelude.Nothing     -> t'
 139                                Prelude.Just    t'' -> t''
 140       TypeRep.PredTy p         -> case Type.coreView t of
 141                                Prelude.Nothing     -> TypeRep.PredTy p
 142                                Prelude.Just    t'  -> t'
 143
 144 coreCoercionToWeakCoercion :: Type.Type -> WeakCoercion
 145 coreCoercionToWeakCoercion c =
 146  WCoUnsafe (errOrFail (coreTypeToWeakType t1)) (errOrFail (coreTypeToWeakType t2))
 147    where
 148     (t1,t2) = Coercion.coercionKind c
 149 {-
 150 -- REMEMBER: cotycon applications may be oversaturated
 151  case c of
 152   TypeRep.TyVarTy  v     -> WCoVar (WeakCoerVar v (Prelude.error "FIXME") (Prelude.error "FIXME") (Prelude.error "FIXME"))
 153   TypeRep.AppTy    t1 t2 -> WCoApp   (coreCoercionToWeakCoercion t1) (coreCoercionToWeakCoercion t2)
 154   TypeRep.TyConApp tc t  ->
 155       case TyCon.isCoercionTyCon_maybe tc of
 156         Prelude.Nothing -> Prelude.error ((Prelude.++) "coreCoercionToWeakCoercion got isCoercionTyCon_maybe " (outputableToString c))
 157         Prelude.Just (_, ctcd) ->
 158             case (ctcd,t) of
 159               (TyCon.CoTrans , [x,y]     ) -> WCoComp   (coreCoercionToWeakCoercion x) (coreCoercionToWeakCoercion y)
 160               (TyCon.CoSym   , [x]       ) -> WCoSym    (coreCoercionToWeakCoercion x)
 161               (TyCon.CoLeft  , [x]       ) -> WCoLeft   (coreCoercionToWeakCoercion x)
 162               (TyCon.CoRight , [x]       ) -> WCoLeft   (coreCoercionToWeakCoercion x)
 163 --            (TyCon.CoUnsafe, [t1, t2 ] ) -> WCoUnsafe (coreTypeToWeakType t1) (coreTypeToWeakType t2)
 164               (TyCon.CoTrans , []        ) -> Prelude.error "CoTrans is not in post-publication-appendix SystemFC1"
 165               (TyCon.CoCsel1 , []        ) -> Prelude.error "CoCsel1 is not in post-publication-appendix SystemFC1"
 166               (TyCon.CoCsel2 , []        ) -> Prelude.error "CoCsel2 is not in post-publication-appendix SystemFC1"
 167               (TyCon.CoCselR , []        ) -> Prelude.error "CoCselR is not in post-publication-appendix SystemFC1"
 168               (TyCon.CoInst  , []        ) -> Prelude.error "CoInst  is not in post-publication-appendix SystemFC1"
 169               (TyCon.CoAxiom _ _ _ , _   ) -> Prelude.error "CoAxiom is not yet implemented (FIXME)"
 170               ( _, [ t1 , t2 ]) -> WCoUnsafe (errOrFail (coreTypeToWeakType t1)) (errOrFail (coreTypeToWeakType t2))
 171               _ -> Prelude.error ((Prelude.++) "coreCoercionToWeakCoercion got " (outputableToString c))
 172   _ -> Prelude.error ((Prelude.++) "coreCoercionToWeakCoercion got " (outputableToString c))
 173 -}
 174 --  TypeRep.ForAllTy v t   -> WCoAll  (Prelude.error "FIXME") (coreTypeToWeakType t)
 175 -- FIXME   x y                                  -> WCoAppT    (coreCoercionToWeakCoercion x) (coreCoercionToWeakType y)
 176 --  CoreSyn.Type t                            -> WCoType   (coreTypeToWeakType t)
 177
 178 {-
 179 weakCoercionToCoreCoercion :: CoreCoercion -> Type.Type
 180 | WCoVar     (weakCoerVar _ _ t1 t2) => (t1,t2)
 181 | WCoType    t                       => Prelude_error "FIXME WCoType"
 182 | WCoApp     c1 c2                   => Prelude_error "FIXME WCoApp"
 183 | WCoAppT    c t                     => Prelude_error "FIXME WCoAppT"
 184 | WCoAll     k f                     => Prelude_error "FIXME WCoAll"
 185 | WCoSym     c                       => let (t2,t1) := weakCoercionTypes c in (t1,t2)
 186 | WCoComp    c1 c2                   => Prelude_error "FIXME WCoComp"
 187 | WCoLeft    c                       => Prelude_error "FIXME WCoLeft"
 188 | WCoRight   c                       => Prelude_error "FIXME WCoRight"
 189 | WCoUnsafe  t1 t2                   => (t1,t2)
 190 -}
 191
 192 {-# NOINLINE trace #-}
 193 trace :: Prelude.String -> a -> a
 194 trace msg x = x
 195
 196 --trace = Debug.Trace.trace
 197 --trace msg x = x
 198 --trace msg x = System.IO.Unsafe.unsafePerformIO $ Prelude.return x
 199 --trace s x = x
 200 --trace msg x = System.IO.Unsafe.unsafePerformIO $
 201 --                (Prelude.>>=) (System.IO.hPutStrLn System.IO.stdout msg) (\_ -> Prelude.return x)
 202 --trace msg x = System.IO.Unsafe.unsafePerformIO $
 203 --                (Prelude.>>=) (System.IO.hPutStr System.IO.stdout " ") (\_ -> Prelude.return x)
 204
 205
 206 {-  -- used for extracting strings WITHOUT the patch for Coq
 207 bin2ascii =
 208   (\ b0 b1 b2 b3 b4 b5 b6 b7 ->
 209      let f b i = if b then 1 `shiftL` i else 0
 210      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))
 211 -}
 212
 213 -- I'm leaving this here (commented out) in case I ever need it again)
 214 --checkTypeEquality :: Type.Type -> Type.Type -> Prelude.Bool
 215 --checkTypeEquality t1 t2 = Type.tcEqType (Type.expandTypeSynonyms t1) (Type.expandTypeSynonyms t2)