From 0f137f4fbe7076b7a0f6b33d661b4f7aa8b4f160 Mon Sep 17 00:00:00 2001 From: Adam Megacz Date: Mon, 30 May 2011 22:48:14 -0700 Subject: [PATCH] update for new GHC coercion representation --- src/Extraction-prefix.hs | 78 +++++++--------------------------------------- src/ExtractionMain.v | 2 +- src/HaskCore.v | 5 ++- src/HaskCoreToWeak.v | 11 ++++--- src/HaskCoreTypes.v | 33 ++++++++++++++++++-- src/HaskStrongTypes.v | 2 +- src/HaskWeakToCore.v | 12 ++----- 7 files changed, 57 insertions(+), 86 deletions(-) diff --git a/src/Extraction-prefix.hs b/src/Extraction-prefix.hs index 7fb0160..09f4b34 100644 --- a/src/Extraction-prefix.hs +++ b/src/Extraction-prefix.hs @@ -2,6 +2,7 @@ module CoqPass ( coqPassCoreToString, coqPassCoreToCore ) where import qualified Unique +import qualified Kind import qualified UniqSupply import qualified MkCore import qualified TysWiredIn @@ -18,6 +19,7 @@ import qualified TyCon import qualified Coercion import qualified Var import qualified Id +import qualified Pair import qualified FastString import qualified BasicTypes import qualified DataCon @@ -53,8 +55,7 @@ sortAlts x = Data.List.sortBy (\a b -> if a `CoreSyn.ltAlt` b then Data.Ord.LT e coreVarToWeakVar :: Var.Var -> CoreVarToWeakVarResult coreVarToWeakVar v | Id.isId v = CVTWVR_EVar (Var.varType v) coreVarToWeakVar v | Var.isTyVar v = CVTWVR_TyVar (coreKindToKind (Var.varType v)) -coreVarToWeakVar v | Var.isCoVar v = CVTWVR_CoVar (Prelude.fst (Coercion.coercionKind (Var.varType v))) - (Prelude.snd (Coercion.coercionKind (Var.varType v))) +coreVarToWeakVar v | Coercion.isCoVar v = CVTWVR_CoVar (Prelude.fst (Coercion.coVarKind v)) (Prelude.snd (Coercion.coVarKind v)) coreVarToWeakVar _ = Prelude.error "Var.Var that is neither an expression, type variable, nor coercion variable!" rawTyFunKind :: TyCon.TyCon -> ( [Kind] , Kind ) @@ -88,21 +89,21 @@ sanitizeForLatex ('#':x) = "\\#"++(sanitizeForLatex x) sanitizeForLatex (c:x) = c:(sanitizeForLatex x) kindToCoreKind :: Kind -> TypeRep.Kind -kindToCoreKind KindStar = TypeRep.liftedTypeKind -kindToCoreKind (KindArrow k1 k2) = Coercion.mkArrowKind (kindToCoreKind k1) (kindToCoreKind k2) +kindToCoreKind KindStar = Kind.liftedTypeKind +kindToCoreKind (KindArrow k1 k2) = Kind.mkArrowKind (kindToCoreKind k1) (kindToCoreKind k2) 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 + case Kind.splitKindFunTy_maybe k of Prelude.Just (k1,k2) -> KindArrow (coreKindToKind k1) (coreKindToKind k2) Prelude.Nothing -> - if (Coercion.isLiftedTypeKind k) then KindStar - else if (Coercion.isUnliftedTypeKind k) then KindStar - else if (Coercion.isArgTypeKind k) then KindStar - else if (Coercion.isUbxTupleKind k) then KindStar - else if (Coercion.isOpenTypeKind k) then KindStar + if (Kind.isLiftedTypeKind k) then KindStar + else if (Kind.isUnliftedTypeKind k) then KindStar + else if (Kind.isArgTypeKind k) then KindStar + else if (Kind.isUbxTupleKind k) then KindStar + else if (Kind.isOpenTypeKind k) then KindStar -- -- The "subkinding" in GHC is not dealt with in System FC, and dealing -- with it is not actually as simple as you'd think. @@ -112,8 +113,7 @@ coreKindToKind k = -- else if (Coercion.isArgTypeKind k) then KindArgType -- else if (Coercion.isUbxTupleKind k) then KindUnboxedTuple -- - else if (Coercion.isTySuperKind k) then Prelude.error "coreKindToKind got the kind-of-the-kind-of-types" - else if (Coercion.isCoSuperKind k) then Prelude.error "coreKindToKind got the kind-of-the-kind-of-coercions" + else if (Kind.isTySuperKind k) then Prelude.error "coreKindToKind got the kind-of-the-kind-of-types" else Prelude.error ((Prelude.++) "coreKindToKind got an unknown kind: " (Outputable.showSDoc (Outputable.ppr k))) outputableToString :: Outputable.Outputable a => a -> Prelude.String @@ -134,52 +134,6 @@ coreViewDeep t = Prelude.Nothing -> TypeRep.PredTy p Prelude.Just t' -> t' -getSourceAndTargetTypesOfCoercion :: Type.Type -> (Type.Type,Type.Type) -getSourceAndTargetTypesOfCoercion c = Coercion.coercionKind (Coercion.typeKind 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 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) --- (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)" - ( _, [ 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) - -{- -weakCoercionToCoreCoercion :: CoreCoercion -> Type.Type -| WCoVar (weakCoerVar _ _ t1 t2) => (t1,t2) -| WCoType t => Prelude_error "FIXME WCoType" -| WCoApp c1 c2 => Prelude_error "FIXME WCoApp" -| WCoAppT c t => Prelude_error "FIXME WCoAppT" -| WCoAll k f => Prelude_error "FIXME WCoAll" -| WCoSym c => let (t2,t1) := weakCoercionTypes c in (t1,t2) -| WCoComp c1 c2 => Prelude_error "FIXME WCoComp" -| WCoLeft c => Prelude_error "FIXME WCoLeft" -| WCoRight c => Prelude_error "FIXME WCoRight" -| WCoUnsafe t1 t2 => (t1,t2) --} - {-# NOINLINE trace #-} trace :: Prelude.String -> a -> a trace msg x = x @@ -193,14 +147,6 @@ trace msg x = 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 = - (\ b0 b1 b2 b3 b4 b5 b6 b7 -> - let f b i = if b then 1 `shiftL` i else 0 - 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)) --} - -- I'm leaving this here (commented out) in case I ever need it again) --checkTypeEquality :: Type.Type -> Type.Type -> Prelude.Bool --checkTypeEquality t1 t2 = Type.tcEqType (Type.expandTypeSynonyms t1) (Type.expandTypeSynonyms t2) diff --git a/src/ExtractionMain.v b/src/ExtractionMain.v index 2e51d0e..d70cd58 100644 --- a/src/ExtractionMain.v +++ b/src/ExtractionMain.v @@ -71,7 +71,7 @@ Variable mkSystemName : Unique -> string -> nat -> Name. Variable mkTyVar : Name -> Kind -> CoreVar. Extract Inlined Constant mkTyVar => "(\n k -> Var.mkTyVar n (kindToCoreKind k))". Variable mkCoVar : Name -> CoreType -> CoreType -> CoreVar. - Extract Inlined Constant mkCoVar => "(\n t1 t2 -> Var.mkCoVar n (Coercion.mkCoKind t1 t2))". + Extract Inlined Constant mkCoVar => "(\n t1 t2 -> Var.mkCoVar n (Coercion.mkCoType t1 t2))". Variable mkExVar : Name -> CoreType -> CoreVar. Extract Inlined Constant mkExVar => "Id.mkLocalId". diff --git a/src/HaskCore.v b/src/HaskCore.v index b05c34f..13a263e 100644 --- a/src/HaskCore.v +++ b/src/HaskCore.v @@ -23,6 +23,7 @@ Inductive CoreExpr {b:Type} := | CoreECast : CoreExpr -> CoreCoercion -> CoreExpr | CoreENote : Note -> CoreExpr -> CoreExpr | CoreEType : CoreType -> CoreExpr +| CoreECoercion : CoreCoercion -> CoreExpr with CoreBind {b:Type} := | CoreNonRec : b -> CoreExpr -> CoreBind | CoreRec : list (b * CoreExpr ) -> CoreBind. @@ -36,7 +37,9 @@ Extract Inductive CoreExpr => "CoreSyn.Case" "CoreSyn.Cast" "CoreSyn.Note" - "CoreSyn.Type" ]. + "CoreSyn.Type" + "CoreSyn.Coercion" + ]. Extract Inductive CoreBind => "CoreSyn.Bind" [ "CoreSyn.NonRec" "CoreSyn.Rec" ]. diff --git a/src/HaskCoreToWeak.v b/src/HaskCoreToWeak.v index 673b999..7669e5d 100644 --- a/src/HaskCoreToWeak.v +++ b/src/HaskCoreToWeak.v @@ -16,10 +16,10 @@ Require Import HaskWeakVars. Require Import HaskWeakTypes. Require Import HaskWeak. -Variable tyConOrTyFun : CoreTyCon -> sum TyCon TyFun. Extract Inlined Constant tyConOrTyFun => "tyConOrTyFun". -Variable coreViewDeep : CoreType -> CoreType. Extract Inlined Constant coreViewDeep => "coreViewDeep". -Variable getSourceAndTargetTypesOfCoercion : CoreCoercion -> (CoreType * CoreType). - Extract Inlined Constant getSourceAndTargetTypesOfCoercion => "getSourceAndTargetTypesOfCoercion". +Variable tyConOrTyFun : CoreTyCon -> sum TyCon TyFun. Extract Inlined Constant tyConOrTyFun => "tyConOrTyFun". +Variable coreViewDeep : CoreType -> CoreType. Extract Inlined Constant coreViewDeep => "coreViewDeep". +Variable coercionKind : CoreCoercion -> (CoreType * CoreType). + Extract Inlined Constant coercionKind => "(\x -> Pair.unPair (Coercion.coercionKind x))". (* extracts the Name from a CoreVar *) Variable coreVarCoreName : CoreVar -> CoreName. Extract Inlined Constant coreVarCoreName => "Var.varName". @@ -188,8 +188,9 @@ Fixpoint coreExprToWeakExpr (ce:@CoreExpr CoreVar) : ???WeakExpr := | CoreELit lit => OK (WELit lit) | CoreENote n e => coreExprToWeakExpr e >>= fun e' => OK (WENote n e') | CoreEType t => Error "encountered CoreEType in a position where an Expr should have been" + | CoreECoercion co => Error "encountered CoreECoercion in a position where an Expr should have been" | CoreECast e co => coreExprToWeakExpr e >>= fun e' => - let (ct1,ct2) := getSourceAndTargetTypesOfCoercion co + let (ct1,ct2) := coercionKind co in coreTypeToWeakType ct1 >>= fun t1 => coreTypeToWeakType ct2 >>= fun t2 => OK (WECast e' (WCoUnsafe t1 t2)) diff --git a/src/HaskCoreTypes.v b/src/HaskCoreTypes.v index 4babf36..79ab342 100644 --- a/src/HaskCoreTypes.v +++ b/src/HaskCoreTypes.v @@ -12,7 +12,9 @@ Require Import HaskCoreVars. Require Import HaskLiterals. Require Import HaskTyCons. -Variable CoreCoercion : Type. Extract Inlined Constant CoreCoercion => "Coercion.Coercion". +Variable CoreCoercionCoAxiom : Type. Extract Inlined Constant CoreCoercionCoAxiom => "Coercion.CoAxiom". +Variable Int : Type. Extract Inlined Constant Int => "Prelude.Int". + Variable classTyCon : Class_ -> CoreTyCon. Extract Inlined Constant classTyCon => "Class.classTyCon". Variable coreTyConToString : CoreTyCon -> string. Extract Inlined Constant coreTyConToString => "outputableToString". Variable coreDataConToString : CoreDataCon -> string. Extract Inlined Constant coreDataConToString => "outputableToString". @@ -34,11 +36,38 @@ Extract Inductive CoreType => Extract Inductive PredType => "TypeRep.PredType" [ "TypeRep.ClassP" "TypeRep.IParam" "TypeRep.EqPred" ]. +Inductive CoreCoercion : Type := + CoreCoercionRefl : CoreType -> CoreCoercion + | CoreCoercionTyConAppCo : CoreTyCon -> list CoreCoercion -> CoreCoercion + | CoreCoercionAppCo : CoreCoercion -> CoreCoercion -> CoreCoercion + | CoreCoercionForAllCo : CoreVar -> CoreCoercion -> CoreCoercion + | CoreCoercionCoVarCo : CoreVar -> CoreCoercion + | CoreCoercionAxiomInstCo : CoreCoercionCoAxiom -> list CoreCoercion -> CoreCoercion + | CoreCoercionUnsafeCo : CoreType -> CoreType -> CoreCoercion + | CoreCoercionSymCo : CoreCoercion -> CoreCoercion + | CoreCoercionTransCo : CoreCoercion -> CoreCoercion -> CoreCoercion + | CoreCoercionNthCo : Int -> CoreCoercion -> CoreCoercion + | CoreCoercionInstCo : CoreCoercion -> CoreType -> CoreCoercion. + +Extract Inductive CoreCoercion => + "Coercion.Coercion" [ + "Coercion.Refl" + "Coercion.TyConAppCo" + "Coercion.AppCo" + "Coercion.ForAllCo" + "Coercion.CoVarCo" + "Coercion.AxiomInstCo" + "Coercion.UnsafeCo" + "Coercion.SymCo" + "Coercion.TransCo" + "Coercion.NthCo" + "Coercion.InstCo" ]. + Variable coreNameToString : CoreName -> string. Extract Inlined Constant coreNameToString => "outputableToString". Variable coreCoercionToString : CoreCoercion -> string. Extract Inlined Constant coreCoercionToString => "outputableToString". Variable coreCoercionKind : Kind -> CoreType*CoreType. Extract Inlined Constant coreCoercionKind => "(Coercion.coercionKind . kindToCoreKind)". -Variable kindOfCoreType : CoreType -> Kind. Extract Inlined Constant kindOfCoreType => "(coreKindToKind . Coercion.typeKind)". +Variable kindOfCoreType : CoreType -> Kind. Extract Inlined Constant kindOfCoreType => "(coreKindToKind . Kind.typeKind)". Variable coreTypeToString : CoreType -> string. Extract Inlined Constant coreTypeToString => "(outputableToString . coreViewDeep)". Variable setVarType : CoreVar -> CoreType -> CoreVar. Extract Inlined Constant setVarType => "Var.setVarType". diff --git a/src/HaskStrongTypes.v b/src/HaskStrongTypes.v index 60e84b6..e5a10ba 100644 --- a/src/HaskStrongTypes.v +++ b/src/HaskStrongTypes.v @@ -19,7 +19,7 @@ Require Import HaskCoreToWeak. Variable dataConTyCon : CoreDataCon -> TyCon. Extract Inlined Constant dataConTyCon => "DataCon.dataConTyCon". Variable dataConExVars_ : CoreDataCon -> list CoreVar. Extract Inlined Constant dataConExVars_ => "DataCon.dataConExTyVars". -Variable dataConEqTheta_ : CoreDataCon -> list PredType. Extract Inlined Constant dataConEqTheta_ => "DataCon.dataConEqTheta". +Variable dataConEqTheta_ : CoreDataCon -> list PredType. Extract Inlined Constant dataConEqTheta_ => "DataCon.dataConTheta". Variable dataConOrigArgTys_: CoreDataCon -> list CoreType. Extract Inlined Constant dataConOrigArgTys_=>"DataCon.dataConOrigArgTys". Definition dataConExTyVars cdc := diff --git a/src/HaskWeakToCore.v b/src/HaskWeakToCore.v index 8ceb0b7..c3e90a4 100644 --- a/src/HaskWeakToCore.v +++ b/src/HaskWeakToCore.v @@ -25,13 +25,6 @@ Variable sortAlts : forall {a}{b}, list (@triple CoreAltCon a b) -> list (@trip Extract Inlined Constant sortAlts => "sortAlts". Implicit Arguments sortAlts [[a][b]]. -Variable mkUnsafeCoercion : CoreType -> CoreType -> CoreCoercion. - Extract Inlined Constant mkUnsafeCoercion => "Coercion.mkUnsafeCoercion". - -(* Coercion and Type are actually the same thing in GHC, but we don't tell Coq about that. This lets us get around it. *) -Variable coreCoercionsAreReallyTypes : CoreCoercion -> CoreType. - Extract Inlined Constant coreCoercionsAreReallyTypes => "(\x -> x)". - Definition weakAltConToCoreAltCon (wa:WeakAltCon) : CoreAltCon := match wa with | WeakDataAlt cdc => DataAlt cdc @@ -59,7 +52,7 @@ Fixpoint weakTypeToCoreType (wt:WeakType) : CoreType := end. Definition weakCoercionToCoreCoercion (wc:WeakCoercion) : CoreCoercion := - mkUnsafeCoercion (weakTypeToCoreType (fst (weakCoercionTypes wc))) (weakTypeToCoreType (snd (weakCoercionTypes wc))). + CoreCoercionUnsafeCo (weakTypeToCoreType (fst (weakCoercionTypes wc))) (weakTypeToCoreType (snd (weakCoercionTypes wc))). Fixpoint weakExprToCoreExpr (me:WeakExpr) : @CoreExpr CoreVar := match me with @@ -67,8 +60,7 @@ Fixpoint weakExprToCoreExpr (me:WeakExpr) : @CoreExpr CoreVar := | WELit lit => CoreELit lit | WEApp e1 e2 => CoreEApp (weakExprToCoreExpr e1) (weakExprToCoreExpr e2) | WETyApp e t => CoreEApp (weakExprToCoreExpr e ) (CoreEType (weakTypeToCoreType t)) - | WECoApp e co => CoreEApp (weakExprToCoreExpr e ) - (CoreEType (coreCoercionsAreReallyTypes (weakCoercionToCoreCoercion co))) + | WECoApp e co => CoreEApp (weakExprToCoreExpr e ) (CoreECoercion (weakCoercionToCoreCoercion co)) | WENote n e => CoreENote n (weakExprToCoreExpr e ) | WELam (weakExprVar ev _ ) e => CoreELam ev (weakExprToCoreExpr e ) | WETyLam (weakTypeVar tv _ ) e => CoreELam tv (weakExprToCoreExpr e ) -- 1.7.10.4