+{-# OPTIONS_GHC -fno-warn-unused-matches -fno-warn-unused-binds -fno-warn-unused-imports #-}
module CoqPass ( coqPassCoreToString, coqPassCoreToCore )
where
import qualified Unique
import qualified Data.Ord
import qualified Data.Typeable
import Data.Bits ((.&.), shiftL, (.|.))
-import Prelude ( (++), (+), (==), Show, show, Char, (.), ($) )
+import Prelude ( (++), (+), (==), Show, show, (.), ($) )
import qualified Prelude
-import qualified Debug.Trace
import qualified GHC.Base
-import qualified System.IO
import qualified System.IO.Unsafe
getTyConTyVars :: TyCon.TyCon -> [Var.TyVar]
coreVarToWeakVar :: Var.Var -> WeakVar
coreVarToWeakVar v | Id.isId v = WExprVar (WeakExprVar v (errOrFail (coreTypeToWeakType (Var.varType v))))
- where
- errOrFail (OK x) = x
- errOrFail (Error s) = Prelude.error s
coreVarToWeakVar v | Var.isTyVar v = WTypeVar (WeakTypeVar v (coreKindToKind (Var.varType v)))
-coreVarToWeakVar v | Var.isCoVar v = WCoerVar (WeakCoerVar v (Prelude.error "FIXME")
- (Prelude.error "FIXME") (Prelude.error "FIXME"))
+coreVarToWeakVar v | Var.isCoVar v
+ = WCoerVar (WeakCoerVar v
+ (errOrFail (coreTypeToWeakType (Prelude.fst (Coercion.coercionKind (Var.varType v)))))
+ (errOrFail (coreTypeToWeakType (Prelude.snd (Coercion.coercionKind (Var.varType v))))))
coreVarToWeakVar _ =
Prelude.error "Var.Var that is neither an expression variable, type variable, nor coercion variable!"
+errOrFail :: OrError t -> t
+errOrFail (OK x) = x
+errOrFail (Error s) = Prelude.error s
+
+rawTyFunKind :: TyCon.TyCon -> ( [Kind] , Kind )
+rawTyFunKind tc = ((Prelude.map coreKindToKind (Prelude.take (TyCon.tyConArity tc) argk))
+ ,
+ coreKindToKind (Coercion.mkArrowKinds (Prelude.drop (TyCon.tyConArity tc) argk) retk))
+ where (argk,retk) = Coercion.splitKindFunTys (TyCon.tyConKind tc)
+
tyConOrTyFun :: TyCon.TyCon -> Prelude.Either TyCon.TyCon TyCon.TyCon
tyConOrTyFun n =
if n == TysPrim.statePrimTyCon -- special-purpose hack treat State# as a type family since it has kind *->* but no tyvars
then Prelude.Right n
else if TyCon.isFamInstTyCon n
then Prelude.Right n
- else Prelude.Left n
+ else if TyCon.isSynTyCon n
+ then Prelude.Right n
+ else Prelude.Left n
nat2int :: Nat -> Prelude.Int
nat2int O = 0
kindToCoreKind :: Kind -> TypeRep.Kind
kindToCoreKind KindStar = TypeRep.liftedTypeKind
kindToCoreKind (KindArrow k1 k2) = Coercion.mkArrowKind (kindToCoreKind k1) (kindToCoreKind k2)
-kindToCoreKind _ = Prelude.error "kindToCoreKind does not know how to handle that"
-
+kindToCoreKind k = Prelude.error ((Prelude.++)
+ "kindToCoreKind does not know how to handle kind "
+ (kindToString k))
coreKindToKind :: TypeRep.Kind -> Kind
coreKindToKind k =
case Coercion.splitKindFunTy_maybe k of
else Prelude.error ((Prelude.++) "coreKindToKind got an unknown kind: "
(Outputable.showSDoc (Outputable.ppr k)))
outputableToString :: Outputable.Outputable a => a -> Prelude.String
-outputableToString = (\x -> Outputable.showSDoc (Outputable.ppr x))
+outputableToString = (\x -> Outputable.showSDocDebug (Outputable.ppr x))
coreViewDeep :: Type.Type -> Type.Type
coreViewDeep t =
Prelude.Nothing -> TypeRep.PredTy p
Prelude.Just t' -> t'
--- FIXME: cotycon applications may be oversaturated
coreCoercionToWeakCoercion :: Type.Type -> WeakCoercion
coreCoercionToWeakCoercion c =
+ WCoUnsafe (errOrFail (coreTypeToWeakType t1)) (errOrFail (coreTypeToWeakType t2))
+ where
+ (t1,t2) = Coercion.coercionKind c
+{-
+-- REMEMBER: cotycon applications may be oversaturated
case c of
TypeRep.TyVarTy v -> WCoVar (WeakCoerVar v (Prelude.error "FIXME") (Prelude.error "FIXME") (Prelude.error "FIXME"))
TypeRep.AppTy t1 t2 -> WCoApp (coreCoercionToWeakCoercion t1) (coreCoercionToWeakCoercion t2)
TypeRep.TyConApp tc t ->
case TyCon.isCoercionTyCon_maybe tc of
- Prelude.Nothing -> Prelude.error ((Prelude.++) "coreCoercionToWeakCoercion got " (outputableToString c))
+ Prelude.Nothing -> Prelude.error ((Prelude.++) "coreCoercionToWeakCoercion got isCoercionTyCon_maybe " (outputableToString c))
Prelude.Just (_, ctcd) ->
case (ctcd,t) of
(TyCon.CoTrans , [x,y] ) -> WCoComp (coreCoercionToWeakCoercion x) (coreCoercionToWeakCoercion y)
(TyCon.CoSym , [x] ) -> WCoSym (coreCoercionToWeakCoercion x)
(TyCon.CoLeft , [x] ) -> WCoLeft (coreCoercionToWeakCoercion x)
(TyCon.CoRight , [x] ) -> WCoLeft (coreCoercionToWeakCoercion x)
--- FIXME (TyCon.CoUnsafe, [t1, t2 ] ) -> WCoUnsafe (coreTypeToWeakType t1) (coreTypeToWeakType t2)
+-- (TyCon.CoUnsafe, [t1, t2 ] ) -> WCoUnsafe (coreTypeToWeakType t1) (coreTypeToWeakType t2)
(TyCon.CoTrans , [] ) -> Prelude.error "CoTrans is not in post-publication-appendix SystemFC1"
(TyCon.CoCsel1 , [] ) -> Prelude.error "CoCsel1 is not in post-publication-appendix SystemFC1"
(TyCon.CoCsel2 , [] ) -> Prelude.error "CoCsel2 is not in post-publication-appendix SystemFC1"
(TyCon.CoCselR , [] ) -> Prelude.error "CoCselR is not in post-publication-appendix SystemFC1"
(TyCon.CoInst , [] ) -> Prelude.error "CoInst is not in post-publication-appendix SystemFC1"
- (TyCon.CoAxiom , [] ) -> Prelude.error "CoAxiom is not yet implemented (FIXME)"
+ (TyCon.CoAxiom _ _ _ , _ ) -> Prelude.error "CoAxiom is not yet implemented (FIXME)"
+ ( _, [ t1 , t2 ]) -> WCoUnsafe (errOrFail (coreTypeToWeakType t1)) (errOrFail (coreTypeToWeakType t2))
_ -> Prelude.error ((Prelude.++) "coreCoercionToWeakCoercion got " (outputableToString c))
_ -> Prelude.error ((Prelude.++) "coreCoercionToWeakCoercion got " (outputableToString c))
+-}
-- TypeRep.ForAllTy v t -> WCoAll (Prelude.error "FIXME") (coreTypeToWeakType t)
-- FIXME x y -> WCoAppT (coreCoercionToWeakCoercion x) (coreCoercionToWeakType y)
-- CoreSyn.Type t -> WCoType (coreTypeToWeakType t)
| WCoUnsafe t1 t2 => (t1,t2)
-}
+{-# NOINLINE trace #-}
+trace :: Prelude.String -> a -> a
+trace msg x = x
--trace = Debug.Trace.trace
--trace msg x = x
-trace msg x = System.IO.Unsafe.unsafePerformIO $ Prelude.return x
-{-
-trace s x = x
-trace msg x = System.IO.Unsafe.unsafePerformIO $
- (Prelude.>>=) (System.IO.hPutStrLn System.IO.stdout msg) (\_ -> Prelude.return x)
-trace msg x = System.IO.Unsafe.unsafePerformIO $
- (Prelude.>>=) (System.IO.hPutStr System.IO.stdout " ") (\_ -> Prelude.return x)
--}
+--trace msg x = System.IO.Unsafe.unsafePerformIO $ Prelude.return x
+--trace s x = x
+--trace msg x = System.IO.Unsafe.unsafePerformIO $
+-- (Prelude.>>=) (System.IO.hPutStrLn System.IO.stdout msg) (\_ -> Prelude.return x)
+--trace msg x = System.IO.Unsafe.unsafePerformIO $
+-- (Prelude.>>=) (System.IO.hPutStr System.IO.stdout " ") (\_ -> Prelude.return x)
+
{- -- used for extracting strings WITHOUT the patch for Coq
bin2ascii =