From: Adam Megacz Date: Mon, 14 Mar 2011 10:22:31 +0000 (-0700) Subject: first pass at proper handling of coercions in HaskWeak X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=commitdiff_plain;h=ab2e0681a81695cc2380b007f2a3314005ec1c99 first pass at proper handling of coercions in HaskWeak --- diff --git a/src/Extraction-prefix.hs b/src/Extraction-prefix.hs index 4abbf69..d0b6ffa 100644 --- a/src/Extraction-prefix.hs +++ b/src/Extraction-prefix.hs @@ -19,10 +19,12 @@ import qualified FastString import qualified BasicTypes import qualified DataCon import qualified CoreSyn +import qualified CoreUtils import qualified Class import qualified Data.Char +import qualified Data.Typeable import Data.Bits ((.&.), shiftL, (.|.)) -import Prelude ( (++), (+), (==), Show, show, Char ) +import Prelude ( (++), (+), (==), Show, show, Char, (.) ) import qualified Prelude import qualified GHC.Base @@ -44,11 +46,15 @@ errOrFail (Error s) = Prelude.error s getTyConTyVars :: TyCon.TyCon -> [Var.TyVar] getTyConTyVars tc = if TyCon.isFunTyCon tc then [] else if TyCon.isPrimTyCon tc then [] else TyCon.tyConTyVars tc +sortAlts :: [(CoreSyn.AltCon,a,b)] -> [(CoreSyn.AltCon,a,b)] +sortAlts x = x -- FIXME + -- to do: this could be moved into Coq coreVarToWeakVar :: Var.Var -> WeakVar coreVarToWeakVar v | Id.isId v = WExprVar (WeakExprVar v (errOrFail (coreTypeToWeakType (Var.varType v)))) 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")) +coreVarToWeakVar v | Var.isCoVar v = WCoerVar (WeakCoerVar v (Prelude.error "FIXME") + (Prelude.error "FIXME") (Prelude.error "FIXME")) coreVarToWeakVar _ = Prelude.error "Var.Var that is neither an expression variable, type variable, nor coercion variable!" @@ -80,7 +86,7 @@ coreKindToKind k = case Coercion.splitKindFunTy_maybe k of Prelude.Just (k1,k2) -> KindTypeFunction (coreKindToKind k1) (coreKindToKind k2) Prelude.Nothing -> - if (Coercion.isLiftedTypeKind k) then KindType + if (Coercion.isLiftedTypeKind k) then KindType else if (Coercion.isUnliftedTypeKind k) then KindUnliftedType else if (Coercion.isOpenTypeKind k) then KindOpenType else if (Coercion.isArgTypeKind k) then KindArgType @@ -113,3 +119,45 @@ coreViewDeep t = TypeRep.PredTy p -> case Type.coreView t of Prelude.Nothing -> TypeRep.PredTy p Prelude.Just t' -> t' + +-- FIXME: cotycon applications may be oversaturated +coreCoercionToWeakCoercion :: Type.Type -> WeakCoercion +coreCoercionToWeakCoercion c = + 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.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.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)" + _ -> 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) +-} \ No newline at end of file diff --git a/src/HaskCoreToWeak.v b/src/HaskCoreToWeak.v index 1734637..1cbaf22 100644 --- a/src/HaskCoreToWeak.v +++ b/src/HaskCoreToWeak.v @@ -14,7 +14,6 @@ Require Import HaskCore. Require Import HaskWeakVars. Require Import HaskWeakTypes. Require Import HaskWeak. -Require Import HaskWeakToCore. Axiom tycons_distinct : ~(ArrowTyCon=ModalBoxTyCon). Variable tyConOrTyFun : CoreTyCon -> sum TyCon TyFun. Extract Inlined Constant tyConOrTyFun => "tyConOrTyFun". @@ -44,7 +43,7 @@ Fixpoint coreTypeToWeakType' (ct:CoreType) : ???WeakType := | WExprVar _ => Error "encountered expression variable in a modal box type" | WCoerVar _ => Error "encountered coercion variable in a modal box type" end - | _ => Error "mis-applied modal box tycon" + | _ => Error ("mis-applied modal box tycon: " +++ ct) end else let tc' := if eqd_dec tc ArrowTyCon then WFunTyCon @@ -75,9 +74,6 @@ Fixpoint coreTypeToWeakType' (ct:CoreType) : ???WeakType := Variable coreViewDeep : CoreType -> CoreType. Extract Inlined Constant coreViewDeep => "coreViewDeep". Definition coreTypeToWeakType t := coreTypeToWeakType' (coreViewDeep t). -Definition weakTypeOfWeakExpr (we:WeakExpr) : ???WeakType := - coreTypeToWeakType (coreTypeOfCoreExpr (weakExprToCoreExpr we)). - (* detects our crude Core-encoding of modal type introduction/elimination forms *) Definition isBrak (ce:@CoreExpr CoreVar) : ??(CoreVar * WeakTypeVar * CoreType) := match ce with @@ -102,11 +98,14 @@ match ce with | _ => None end. -Definition coreCoercionToWeakCoercion (cc:CoreCoercion) : ???WeakCoercion := +Variable coreCoercionToWeakCoercion : CoreCoercion -> WeakCoercion. + Extract Inlined Constant coreCoercionToWeakCoercion => "coreCoercionToWeakCoercion". +(* let (t1,t2) := coreCoercionKind cc in coreTypeToWeakType t1 >>= fun t1' => - coreTypeToWeakType t2 >>= fun t2' => - OK (weakCoercion (kindOfCoreType t1) t1' t2' cc). + coreTypeToWeakType t2 >>= fun t2' => + OK (WCoUnsafe t1' t2'). +*) Fixpoint coreExprToWeakExpr (ce:@CoreExpr CoreVar) : ???WeakExpr := match ce with @@ -114,8 +113,7 @@ Fixpoint coreExprToWeakExpr (ce:@CoreExpr CoreVar) : ???WeakExpr := | 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" | CoreECast e co => coreExprToWeakExpr e >>= fun e' => - coreCoercionToWeakCoercion co >>= fun co' => - OK (WECast e' co') + OK (WECast e' (coreCoercionToWeakCoercion co)) | CoreEVar v => match coreVarToWeakVar v with | WExprVar ev => OK (WEVar ev) @@ -178,8 +176,8 @@ Fixpoint coreExprToWeakExpr (ce:@CoreExpr CoreVar) : ???WeakExpr := | WTypeVar _ => Error "found a type variable in a case" | WCoerVar _ => Error "found a coercion variable in a case" | WExprVar ev => - coreExprToWeakExpr e >>= fun e' => - weakTypeOfWeakExpr e' >>= fun te' => + coreTypeToWeakType (coreTypeOfCoreExpr e) >>= fun te' => + coreExprToWeakExpr e >>= fun e' => (match isTyConApp te' nil with None => Error "expectTyConApp encountered strange type" | Some x => OK x end) >>= fun tca => let (tc,lt) := tca in diff --git a/src/HaskStrongTypes.v b/src/HaskStrongTypes.v index 81beb65..e79927a 100644 --- a/src/HaskStrongTypes.v +++ b/src/HaskStrongTypes.v @@ -13,6 +13,7 @@ Require Import HaskCoreTypes. Require Import HaskCoreVars. Require Import HaskWeakTypes. Require Import HaskWeakVars. +Require Import HaskWeak. Require Import HaskCoreToWeak. Variable dataConTyCon : CoreDataCon -> TyCon. Extract Inlined Constant dataConTyCon => "DataCon.dataConTyCon". diff --git a/src/HaskWeakToCore.v b/src/HaskWeakToCore.v index 88c6830..e4a4d1f 100644 --- a/src/HaskWeakToCore.v +++ b/src/HaskWeakToCore.v @@ -15,6 +15,7 @@ Require Import HaskCore. Require Import HaskWeakVars. Require Import HaskWeakTypes. Require Import HaskWeak. +Require Import HaskCoreToWeak. Variable mkCoreLet : @CoreBind CoreVar -> @CoreExpr CoreVar -> @CoreExpr CoreVar. Extract Inlined Constant mkCoreLet => "MkCore.mkCoreLet". @@ -23,16 +24,15 @@ Variable sortAlts : forall {a}{b}, list (@triple AltCon a b) -> list (@triple A Extract Inlined Constant sortAlts => "sortAlts". Implicit Arguments sortAlts [[a][b]]. -Variable trustMeCoercion : CoreCoercion. - Extract Inlined Constant trustMeCoercion => "Coercion.unsafeCoerce". +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 weakCoercionToCoreCoercion : WeakCoercion -> CoreCoercion := - fun _ => trustMeCoercion. - + Definition weakCoercionToCoreCoercion (wc:WeakCoercion) : CoreCoercion := + mkUnsafeCoercion (weakTypeToCoreType (fst (weakCoercionTypes wc))) (weakTypeToCoreType (snd (weakCoercionTypes wc))). Fixpoint weakExprToCoreExpr (me:WeakExpr) : @CoreExpr CoreVar := match me with @@ -87,8 +87,9 @@ Definition weakCoercionToCoreCoercion : WeakCoercion -> CoreCoercion := (weakExprToCoreExpr e) end. +Definition weakTypeOfWeakExpr (we:WeakExpr) : ???WeakType := + coreTypeToWeakType (coreTypeOfCoreExpr (weakExprToCoreExpr we)). Instance weakExprToString : ToString WeakExpr := { toString := fun we => toString (weakExprToCoreExpr we) }. - diff --git a/src/HaskWeakToStrong.v b/src/HaskWeakToStrong.v index d765f0f..e5c88f8 100644 --- a/src/HaskWeakToStrong.v +++ b/src/HaskWeakToStrong.v @@ -19,7 +19,6 @@ Require Import HaskStrongTypes. Require Import HaskStrong. Require Import HaskCoreTypes. Require Import HaskCoreVars. -Require Import HaskCoreToWeak. Open Scope string_scope. Definition TyVarResolver Γ := forall wt:WeakTypeVar, ???(HaskTyVar Γ wt). @@ -559,7 +558,7 @@ Definition weakExprToStrongExpr : forall weakExprToStrongExpr Γ (_ :: Δ) φ (weakψ ψ) ξ te' lev e >>= fun e' => castExpr we "WECoLam" _ (ECoLam Γ Δ cv te' t1' t2' ξ lev e') - | WECast e co => let (_,t1,t2,_) := co in + | WECast e co => let (t1,t2) := weakCoercionTypes co in weakTypeToType'' φ t1 ★ >>= fun t1' => weakTypeToType'' φ t2 ★ >>= fun t2' => weakExprToStrongExpr Γ Δ φ ψ ξ t1' lev e >>= fun e' => diff --git a/src/HaskWeakTypes.v b/src/HaskWeakTypes.v index 593bccf..cdbc9e7 100644 --- a/src/HaskWeakTypes.v +++ b/src/HaskWeakTypes.v @@ -55,6 +55,39 @@ Instance WeakTypeVarEqDecidable : EqDecidable WeakTypeVar. right; intro; apply n; inversion H; subst; auto. Defined. +(* a WeakCoerVar just wraps a CoreVar and tags it with the pair of types amongst which it coerces *) +Inductive WeakCoerVar := weakCoerVar : CoreVar -> Kind -> WeakType -> WeakType -> WeakCoerVar. + +Inductive WeakCoercion : Type := +| WCoVar : WeakCoerVar -> WeakCoercion (* g *) +| WCoType : WeakType -> WeakCoercion (* τ *) +| WCoApp : WeakCoercion -> WeakCoercion -> WeakCoercion (* γ γ *) +| WCoAppT : WeakCoercion -> WeakType -> WeakCoercion (* γ@v *) +| WCoAll : Kind -> (WeakTypeVar -> WeakCoercion) -> WeakCoercion (* ∀a:κ.γ *) +| WCoSym : WeakCoercion -> WeakCoercion (* sym *) +| WCoComp : WeakCoercion -> WeakCoercion -> WeakCoercion (* ◯ *) +| WCoLeft : WeakCoercion -> WeakCoercion (* left *) +| WCoRight : WeakCoercion -> WeakCoercion (* right *) +| WCoUnsafe : WeakType -> WeakType -> WeakCoercion (* unsafe *) +(*| WCoCFApp : ∀ n, CoFunConst n -> vec WeakCoercion n -> WeakCoercion (* C γⁿ *)*) +(*| WCoTFApp : ∀ n, TyFunConst n -> vec WeakCoercion n -> WeakCoercion (* S_n γⁿ *)*) +. + +Variable Prelude_error : forall {A}, string -> A. Extract Inlined Constant Prelude_error => "Prelude.error". +Fixpoint weakCoercionTypes (wc:WeakCoercion) : WeakType * WeakType := +match wc with +| 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) +end. + (* TO DO: write a proper EqDecidable instance for WeakType and then move the rest of this into HaskWeakToCore *) Variable ModalBoxTyCon : TyCon. Extract Inlined Constant ModalBoxTyCon => "TysWiredIn.hetMetCodeTypeTyCon". Variable ArrowTyCon : TyCon. Extract Constant ArrowTyCon => "Type.funTyCon". diff --git a/src/HaskWeakVars.v b/src/HaskWeakVars.v index 8a77e09..f174563 100644 --- a/src/HaskWeakVars.v +++ b/src/HaskWeakVars.v @@ -13,12 +13,6 @@ Require Import HaskCoreVars. Require Import HaskCoreTypes. Require Import HaskWeakTypes. -(* TO DO: finish this *) -Inductive WeakCoercion : Type := weakCoercion : Kind -> WeakType -> WeakType -> CoreCoercion -> WeakCoercion. - -(* a WeakCoerVar just wraps a CoreVar and tags it with the pair of types amongst which it coerces *) -Inductive WeakCoerVar := weakCoerVar : CoreVar -> Kind -> WeakType -> WeakType -> WeakCoerVar. - (* a WeakExprVar just wraps a CoreVar and tags it with the type of its value *) Inductive WeakExprVar := weakExprVar : CoreVar -> WeakType -> WeakExprVar.