From 025c2de2effdd7177ca875998b65f51236c8c7c6 Mon Sep 17 00:00:00 2001 From: Adam Megacz Date: Sat, 1 Oct 2011 19:39:02 -0700 Subject: [PATCH] add partial support for flattening kappa-expressions (mostly commented out) --- src/ExtractionMain.v | 24 ++++++++++++---- src/HaskCoreToWeak.v | 71 +++++++++++++++++++++++++++++++++++++++++------- src/HaskStrongTypes.v | 4 +++ src/HaskWeak.v | 4 +++ src/HaskWeakToCore.v | 4 +++ src/HaskWeakToStrong.v | 4 +++ 6 files changed, 95 insertions(+), 16 deletions(-) diff --git a/src/ExtractionMain.v b/src/ExtractionMain.v index 88714c7..9f0fc1a 100644 --- a/src/ExtractionMain.v +++ b/src/ExtractionMain.v @@ -179,9 +179,11 @@ Section core2proof. Definition mkWeakExprVar (u:Unique)(t:WeakType) : WeakExprVar := weakExprVar (mkExVar (mkSystemName u "ev" O) (weakTypeToCoreType t)) t. - Context (hetmet_brak : WeakExprVar). - Context (hetmet_esc : WeakExprVar). - Context (uniqueSupply : UniqSupply). + Context (hetmet_brak : WeakExprVar). + Context (hetmet_esc : WeakExprVar). + Context (hetmet_kappa : WeakExprVar). + Context (hetmet_kappa_app : WeakExprVar). + Context (uniqueSupply : UniqSupply). Definition useUniqueSupply {T}(ut:UniqM T) : ???T := match ut with @@ -311,6 +313,8 @@ Section core2proof. (do_skolemize : bool) (hetmet_brak : CoreVar) (hetmet_esc : CoreVar) + (hetmet_kappa : WeakExprVar) + (hetmet_kappa_app : WeakExprVar) (uniqueSupply : UniqSupply) (lbinds:list (@CoreBind CoreVar)) (hetmet_PGArrowTyCon : TyFun) @@ -451,6 +455,8 @@ Section core2proof. Definition hetmet_brak' := coreVarToWeakExprVarOrError hetmet_brak. Definition hetmet_esc' := coreVarToWeakExprVarOrError hetmet_esc. + Definition hetmet_kappa' := coreVarToWeakExprVarOrError hetmet_kappa. + Definition hetmet_kappa_app' := coreVarToWeakExprVarOrError hetmet_kappa_app. Definition coreToCoreExpr' (cex:@CoreExpr CoreVar) : ???(@CoreExpr CoreVar) := addErrorMessage ("input CoreSyn: " +++ toString cex) @@ -472,7 +478,7 @@ Section core2proof. OK ((@proof2expr nat _ FreshNat _ _ (flatten_type τ) nil _ (fun _ => Prelude_error "unbound unique") _ haskProof) O) >>= fun e' => (snd e') >>= fun e'' => - strongExprToWeakExpr hetmet_brak' hetmet_esc' + strongExprToWeakExpr hetmet_brak' hetmet_esc' (*hetmet_kappa' hetmet_kappa_app'*) mkWeakTypeVar mkWeakCoerVar mkWeakExprVar uniqueSupply (projT2 e'') INil >>= fun q => OK (weakExprToCoreExpr q)) @@ -483,7 +489,7 @@ Section core2proof. OK ((@proof2expr nat _ FreshNat _ _ τ nil _ (fun _ => Prelude_error "unbound unique") _ haskProof) O) >>= fun e' => (snd e') >>= fun e'' => - strongExprToWeakExpr hetmet_brak' hetmet_esc' + strongExprToWeakExpr hetmet_brak' hetmet_esc' (*hetmet_kappa' hetmet_kappa_app'*) mkWeakTypeVar mkWeakCoerVar mkWeakExprVar uniqueSupply (projT2 e'') INil >>= fun q => OK (weakExprToCoreExpr q)) @@ -493,7 +499,7 @@ Section core2proof. OK ((@proof2expr nat _ FreshNat _ _ τ nil _ (fun _ => Prelude_error "unbound unique") _ haskProof) O) >>= fun e' => (snd e') >>= fun e'' => - strongExprToWeakExpr hetmet_brak' hetmet_esc' + strongExprToWeakExpr hetmet_brak' hetmet_esc' (*hetmet_kappa' hetmet_kappa_app'*) mkWeakTypeVar mkWeakCoerVar mkWeakExprVar uniqueSupply (projT2 e'') INil >>= fun q => OK (weakExprToCoreExpr q)))) @@ -538,6 +544,8 @@ Section core2proof. : CoreM (list (@CoreBind CoreVar)) := dsLookupVar "GHC.HetMet.CodeTypes" "hetmet_brak" >>= fun hetmet_brak => dsLookupVar "GHC.HetMet.CodeTypes" "hetmet_esc" >>= fun hetmet_esc => + dsLookupVar "GHC.HetMet.CodeTypes" "hetmet_kappa" >>= fun hetmet_kappa => + dsLookupVar "GHC.HetMet.CodeTypes" "hetmet_kappa_app" >>= fun hetmet_kappa_app => dsLookupTyc "GHC.HetMet.Private" "PGArrow" >>= fun hetmet_PGArrow => dsLookupTyc "GHC.HetMet.GArrow" "GArrowUnit" >>= fun hetmet_PGArrow_unit => dsLookupTyc "GHC.HetMet.GArrow" "GArrowTensor" >>= fun hetmet_PGArrow_tensor => @@ -569,6 +577,10 @@ Section core2proof. do_skolemize hetmet_brak hetmet_esc + (* + hetmet_kappa + hetmet_kappa_app + *) uniqueSupply hetmet_PGArrow hetmet_PGArrow_unit diff --git a/src/HaskCoreToWeak.v b/src/HaskCoreToWeak.v index 7669e5d..a287b20 100644 --- a/src/HaskCoreToWeak.v +++ b/src/HaskCoreToWeak.v @@ -28,6 +28,9 @@ Variable coreVarCoreName : CoreVar -> CoreName. Extract Inlined Constant co Variable hetmet_brak_name : CoreName. Extract Inlined Constant hetmet_brak_name => "PrelNames.hetmet_brak_name". Variable hetmet_esc_name : CoreName. Extract Inlined Constant hetmet_esc_name => "PrelNames.hetmet_esc_name". Variable hetmet_csp_name : CoreName. Extract Inlined Constant hetmet_csp_name => "PrelNames.hetmet_csp_name". +Variable hetmet_kappa_name : CoreName. Extract Inlined Constant hetmet_kappa_name => "PrelNames.hetmet_kappa_name". +Variable hetmet_kappa_app_name: CoreName. +Extract Inlined Constant hetmet_kappa_app_name => "PrelNames.hetmet_kappa_app_name". Definition mkTyFunApplication (tf:TyFun)(lwt:list WeakType) : ???WeakType := split_list lwt (length (fst (tyFunKind tf))) >>= @@ -146,6 +149,32 @@ match ce with | _ => None end. +Definition isKappa (ce:@CoreExpr CoreVar) : bool := +match ce with + | (CoreEApp + (CoreEApp + (CoreEApp + (CoreEVar v) + (CoreEType t1)) + (CoreEType t2)) + (CoreEType t3)) + => if coreName_eq hetmet_kappa_name (coreVarCoreName v) then true else false + | _ => false +end. + +Definition isKappaApp (ce:@CoreExpr CoreVar) : bool := +match ce with + | (CoreEApp (CoreEApp + (CoreEApp + (CoreEApp + (CoreEVar v) + (CoreEType t1)) + (CoreEType t2)) + (CoreEType t3)) _) + => if coreName_eq hetmet_kappa_app_name (coreVarCoreName v) then true else false + | _ => false +end. + Definition isCSP (ce:@CoreExpr CoreVar) : ??(WeakExprVar * WeakTypeVar * CoreType) := match ce with | (CoreEApp (CoreEApp (CoreEVar v) (CoreEType (TyVarTy ec))) (CoreEType tbody)) @@ -216,16 +245,38 @@ Fixpoint coreExprToWeakExpr (ce:@CoreExpr CoreVar) : ???WeakExpr := coreExprToWeakExpr e2 >>= fun e' => coreTypeToWeakType t >>= fun t' => OK (WECSP v tv e' t') - | None => coreExprToWeakExpr e1 >>= fun e1' => - match e2 with - | CoreEType t => - coreTypeToWeakType t >>= fun t' => - OK (WETyApp e1' t') - | _ => coreExprToWeakExpr e2 - >>= fun e2' => OK (WEApp e1' e2') - end - end - end + | None => + (* + if isKappa e1 + then match e2 with + | CoreELam v e => match coreVarToWeakVar' v with + | OK (WExprVar ev) => + coreExprToWeakExpr e >>= fun e' => + OK (WEKappa ev e') + | _ => Error "bogus" + end + | _ => Error "bogus" + end + else if isKappaApp e1 + then match e1 with + | (CoreEApp (CoreEApp (CoreEApp (CoreEApp _ _) _) _) e1') => + coreExprToWeakExpr e1' >>= fun e1'' => + coreExprToWeakExpr e2 >>= fun e2'' => + OK (WEKappaApp e1'' e2'') + | _ => Error "bogus" + end + else + *) + coreExprToWeakExpr e1 >>= fun e1' => + match e2 with + | CoreEType t => + coreTypeToWeakType t >>= fun t' => + OK (WETyApp e1' t') + | _ => coreExprToWeakExpr e2 + >>= fun e2' => OK (WEApp e1' e2') + end + end + end end | CoreELam v e => coreVarToWeakVar' v >>= fun v' => match v' with diff --git a/src/HaskStrongTypes.v b/src/HaskStrongTypes.v index 4740acb..a7bd11a 100644 --- a/src/HaskStrongTypes.v +++ b/src/HaskStrongTypes.v @@ -66,6 +66,9 @@ Section Raw. | TVar : ∀ κ, TV κ -> RawHaskType κ (* a *) | TCon : ∀ tc, RawHaskType (tyConKind' tc) (* T *) | TArrow : RawHaskType (★ ⇛★ ⇛★ ) (* (->) *) + (* + | TKappa : RawHaskType (★ ⇛★ ⇛★ ) (* (~~>) *) + *) | TCoerc : ∀ κ, RawHaskType κ -> RawHaskType κ -> RawHaskType ★ -> RawHaskType ★ (* (+>) *) | TApp : ∀ κ₁ κ₂, RawHaskType (κ₂⇛κ₁) -> RawHaskType κ₂ -> RawHaskType κ₁ (* φ φ *) | TAll : ∀ κ, (TV κ -> RawHaskType ★) -> RawHaskType ★ (* ∀a:κ.φ *) @@ -111,6 +114,7 @@ Implicit Arguments TApp [ [TV] [κ₁] [κ₂] ]. Implicit Arguments TAll [ [TV] ]. Notation "t1 ---> t2" := (fun TV env => (TApp (TApp TArrow (t1 TV env)) (t2 TV env))). +(*Notation "t1 ~~~> t2" := (fun TV env => (TApp (TApp TKappa (t1 TV env)) (t2 TV env))).*) Notation "φ₁ ∼∼ φ₂ ⇒ φ₃" := (fun TV env => TCoerc (φ₁ TV env) (φ₂ TV env) (φ₃ TV env)). (* Kind and Coercion Environments *) diff --git a/src/HaskWeak.v b/src/HaskWeak.v index 077f7b5..9d39f44 100644 --- a/src/HaskWeak.v +++ b/src/HaskWeak.v @@ -31,6 +31,10 @@ Inductive WeakExpr := | WETyApp : WeakExpr -> WeakType -> WeakExpr | WECoApp : WeakExpr -> WeakCoercion -> WeakExpr | WELam : WeakExprVar -> WeakExpr -> WeakExpr +(* +| WEKappa : WeakExprVar -> WeakExpr -> WeakExpr +| WEKappaApp : WeakExpr -> WeakExpr -> WeakExpr +*) | WETyLam : WeakTypeVar -> WeakExpr -> WeakExpr | WECoLam : WeakCoerVar -> WeakExpr -> WeakExpr diff --git a/src/HaskWeakToCore.v b/src/HaskWeakToCore.v index c3e90a4..7d24277 100644 --- a/src/HaskWeakToCore.v +++ b/src/HaskWeakToCore.v @@ -84,6 +84,10 @@ Fixpoint weakExprToCoreExpr (me:WeakExpr) : @CoreExpr CoreVar := (weakExprToCoreExpr e):: nil) (CoreEVar v) + (* + | WEKappa v e => Prelude_error "FIXME: weakExprToCoreExpr case for WEKappa" + | WEKappaApp e1 e2 => Prelude_error "FIXME: weakExprToCoreExpr case for WEKappaApp" + *) | WELet (weakExprVar v _) ve e => mkCoreLet (CoreNonRec v (weakExprToCoreExpr ve)) (weakExprToCoreExpr e) | WECase vscrut escrut tbranches tc types alts => CoreECase (weakExprToCoreExpr escrut) vscrut (weakTypeToCoreType tbranches) diff --git a/src/HaskWeakToStrong.v b/src/HaskWeakToStrong.v index 0acc0af..f6dc701 100644 --- a/src/HaskWeakToStrong.v +++ b/src/HaskWeakToStrong.v @@ -489,6 +489,10 @@ Fixpoint doesWeakVarOccur (wev:WeakExprVar)(me:WeakExpr) : bool := | WELet cv e1 e2 => doesWeakVarOccur wev e1 || (if eqd_dec (wev:CoreVar) (cv:CoreVar)then false else doesWeakVarOccur wev e2) | WEApp e1 e2 => doesWeakVarOccur wev e1 || doesWeakVarOccur wev e2 | WELam cv e => if eqd_dec (wev:CoreVar) (cv:CoreVar) then false else doesWeakVarOccur wev e +(* + | WEKappaApp e1 e2 => doesWeakVarOccur wev e1 || doesWeakVarOccur wev e2 + | WEKappa cv e => if eqd_dec (wev:CoreVar) (cv:CoreVar) then false else doesWeakVarOccur wev e +*) | WETyLam cv e => doesWeakVarOccur wev e | WECoLam cv e => doesWeakVarOccur wev e | WECase vscrut escrut tbranches tc avars alts => -- 1.7.10.4