From c64ac559ed9448b8aa24abedbc2ad5ca800d1d24 Mon Sep 17 00:00:00 2001 From: Adam Megacz Date: Fri, 13 May 2011 20:33:00 -0700 Subject: [PATCH] integrate skolemization pass with flattening --- src/ExtractionMain.v | 14 ++++++++-- src/HaskFlattener.v | 30 ++++++++++++++++------ src/HaskSkolemizer.v | 68 +++++++++++++++++++++++-------------------------- src/HaskStrongTypes.v | 42 ++++++++++++++++++++++++++++++ 4 files changed, 108 insertions(+), 46 deletions(-) diff --git a/src/ExtractionMain.v b/src/ExtractionMain.v index e4281d7..5be5280 100644 --- a/src/ExtractionMain.v +++ b/src/ExtractionMain.v @@ -306,12 +306,21 @@ Section core2proof. Definition ga_unit TV (ec:RawHaskType TV ECKind) : RawHaskType TV ★ := @TyFunApp TV hetmet_PGArrow_unit_TyCon (ECKind::nil) ★ (TyFunApp_cons _ _ ec TyFunApp_nil). + Definition ga_prod TV (ec:RawHaskType TV ECKind) (a b:RawHaskType TV ★) : RawHaskType TV ★ := - TApp (TApp (@TyFunApp TV hetmet_PGArrow_tensor_TyCon (ECKind::nil) _ (TyFunApp_cons _ _ ec TyFunApp_nil)) a) b. + (@TyFunApp TV + hetmet_PGArrow_tensor_TyCon + (ECKind::★ ::★ ::nil) ★ + (TyFunApp_cons _ _ ec + (TyFunApp_cons _ _ a + (TyFunApp_cons _ _ b + TyFunApp_nil)))). + Definition ga_type {TV}(a:RawHaskType TV ECKind)(b c:RawHaskType TV ★) : RawHaskType TV ★ := TApp (TApp (TApp (@TyFunApp TV hetmet_PGArrowTyCon nil _ TyFunApp_nil) a) b) c. + Definition ga := @ga_mk ga_unit ga_prod (@ga_type). Definition ga_type' {Γ}(a:HaskType Γ ECKind)(b c:HaskType Γ ★) : HaskType Γ ★ := @@ -421,7 +430,7 @@ Section core2proof. ((weakExprToStrongExpr Γ Δ φ ψ ξ (fun _ => true) τ nil we) >>= fun e => (addErrorMessage ("HaskStrong...") - (let haskProof := flatten_proof hetmet_flatten' hetmet_unflatten' + (let haskProof := skolemize_and_flatten_proof hetmet_flatten' hetmet_unflatten' hetmet_flattened_id' my_ga (@expr2proof _ _ _ _ _ _ e) in (* insert HaskProof-to-HaskProof manipulations here *) OK ((@proof2expr nat _ FreshNat _ _ _ _ (fun _ => Prelude_error "unbound unique") _ haskProof) O) @@ -520,6 +529,7 @@ Section core2proof. hetmet_pga_applyr hetmet_pga_curryl *) + . End core2proof. diff --git a/src/HaskFlattener.v b/src/HaskFlattener.v index 46e6af5..90785b0 100644 --- a/src/HaskFlattener.v +++ b/src/HaskFlattener.v @@ -239,11 +239,11 @@ Section HaskFlattener. Definition ga_mk_raw {TV}(ec:RawHaskType TV ECKind)(ant suc:Tree ??(RawHaskType TV ★)) : RawHaskType TV ★ := gaTy TV ec - (ga_mk_tree' ec (ant,,(mapOptionTreeAndFlatten (unleaves ○ take_arg_types) suc))) - (ga_mk_tree' ec ( mapOptionTree drop_arg_types suc) ). + (ga_mk_tree' ec ant) + (ga_mk_tree' ec suc). - Definition ga_mk {Γ}(ec:HaskType Γ ECKind )(ant suc:Tree ??(HaskType Γ ★)) : HaskType Γ ★ := - fun TV ite => ga_mk_raw (ec TV ite) (mapOptionTree (fun x => x TV ite) ant) (mapOptionTree (fun x => x TV ite) suc). + Definition ga_mk {Γ}(ec:HaskType Γ ECKind)(ant suc:Tree ??(HaskType Γ ★)) : HaskType Γ ★ := + fun TV ite => gaTy TV (ec TV ite) (ga_mk_tree ec ant TV ite) (ga_mk_tree ec suc TV ite). (* * The story: @@ -855,7 +855,7 @@ Section HaskFlattener. Lemma krunk : forall Γ (ec:HaskTyVar Γ ECKind) t, flatten_type (<[ ec |- t ]>) = @ga_mk Γ (v2t ec) - (mapOptionTree flatten_type (take_arg_types_as_tree Γ t)) + (mapOptionTree flatten_type (take_arg_types_as_tree t)) [ flatten_type (drop_arg_types_as_tree t)]. intros. @@ -1136,7 +1136,7 @@ Section HaskFlattener. simpl. destruct lev. drop_simplify. - set (drop_lev (ec :: nil) (take_arg_types_as_tree Γ t @@@ (ec :: nil))) as empty_tree. + set (drop_lev (ec :: nil) (take_arg_types_as_tree t @@@ (ec :: nil))) as empty_tree. take_simplify. rewrite take_lemma'. simpl. @@ -1149,7 +1149,7 @@ Section HaskFlattener. rewrite krunk. set (mapOptionTree flatten_leveled_type (drop_lev (ec :: nil) succ)) as succ_host. set (mapOptionTree (flatten_type ○ unlev)(take_lev (ec :: nil) succ)) as succ_guest. - set (mapOptionTree flatten_type (take_arg_types_as_tree Γ t)) as succ_args. + set (mapOptionTree flatten_type (take_arg_types_as_tree t)) as succ_args. unfold empty_tree. eapply nd_comp; [ eapply nd_rule; eapply RArrange; apply tree_of_nothing | idtac ]. refine (ga_unkappa' Γ Δ (v2t ec) nil _ _ _ _ ;; _). @@ -1183,7 +1183,7 @@ Section HaskFlattener. clear e. set (mapOptionTree flatten_leveled_type (drop_lev (ec :: nil) succ)) as succ_host. - set (mapOptionTree flatten_type (take_arg_types_as_tree Γ t)) as succ_args. + set (mapOptionTree flatten_type (take_arg_types_as_tree t)) as succ_args. eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RCanR ]. eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ]. @@ -1222,6 +1222,20 @@ Section HaskFlattener. apply (Prelude_error "found Esc at depth >0 indicating 3-level code; only two-level code is currently supported"). Defined. + Definition skolemize_and_flatten_proof : + forall {h}{c}, + ND Rule h c -> + ND Rule + (mapOptionTree (flatten_judgment ○ skolemize_judgment) h) + (mapOptionTree (flatten_judgment ○ skolemize_judgment) c). + intros. + rewrite mapOptionTree_compose. + rewrite mapOptionTree_compose. + apply flatten_proof. + apply skolemize_proof. + apply X. + Defined. + (* to do: establish some metric on judgments (max length of level of any succedent type, probably), show how to * calculate it, and show that the flattening procedure above drives it down by one *) diff --git a/src/HaskSkolemizer.v b/src/HaskSkolemizer.v index c1b5708..2c1c9d2 100644 --- a/src/HaskSkolemizer.v +++ b/src/HaskSkolemizer.v @@ -87,36 +87,29 @@ Section HaskSkolemizer. end end. - Definition ite_unit : ∀ Γ, InstantiatedTypeEnv (fun _ => unit) Γ. - intros. - induction Γ. - apply INil. - apply ICons; auto. - apply tt. - Defined. - - Fixpoint grab (n:nat) {T} (l:list T) : T := - match l with - | nil => Prelude_error "grab failed" - | h::t => match n with - | 0 => h - | S n' => grab n' t - end - end. + Fixpoint take_trustme {Γ} + (n:nat) + (l:forall TV, InstantiatedTypeEnv TV Γ -> list (RawHaskType TV ★)) + : list (HaskType Γ ★) := - Fixpoint count' (n:nat)(ln:list nat) : list nat := match n with - | 0 => ln - | S n' => count' n' (n'::ln) + | 0 => nil + | S n' => (fun TV ite => match l TV ite with + | nil => Prelude_error "impossible" + | a::b => a + end) + :: + take_trustme n' (fun TV ite => match l TV ite with + | nil => Prelude_error "impossible" + | a::b => b + end) end. - - Definition count (n:nat) := count' n nil. - - Definition rebundle {Γ}(X:forall TV, InstantiatedTypeEnv TV Γ -> list (RawHaskType TV ★)) : list (HaskType Γ ★ ) := - map (fun n => fun TV ite => grab n (X TV ite)) (count (length (X _ (ite_unit _)))). - - Definition take_arg_types_as_tree Γ (ht:HaskType Γ ★) := - (unleaves' (rebundle (fun TV ite => (take_arg_types (ht TV ite))))). + + Definition take_arg_types_as_tree {Γ}(ht:HaskType Γ ★) : Tree ??(HaskType Γ ★ ) := + unleaves + (take_trustme + (count_arg_types (ht _ (ite_unit _))) + (fun TV ite => take_arg_types (ht TV ite))). Definition drop_arg_types_as_tree {Γ} (ht:HaskType Γ ★) : HaskType Γ ★ := fun TV ite => drop_arg_types (ht TV ite). @@ -127,8 +120,8 @@ Section HaskSkolemizer. Lemma take_works : forall {Γ}(t1 t2:HaskType Γ ★), take_arg_types_as_tree (t1 ---> t2) = [t1],,(take_arg_types_as_tree t2). intros. - unfold take_arg_types_as_tree; simpl. - unfold rebundle at 1. + unfold take_arg_types_as_tree at 1. + simpl. admit. Qed. @@ -182,6 +175,7 @@ Section HaskSkolemizer. left; auto. Defined. + Opaque take_arg_types_as_tree. Definition skolemize_proof : forall {h}{c}, ND Rule h c -> @@ -296,17 +290,18 @@ Section HaskSkolemizer. apply RGlobal. destruct case_RLam. - simpl. destruct lev. - apply nd_rule. - apply SFlat. - apply RLam. + apply nd_rule. + apply SFlat. + simpl. + apply RLam. + simpl. rewrite take_works. rewrite drop_works. apply nd_rule. - apply SFlat. - apply RArrange. - apply RCossa. + apply SFlat. + apply RArrange. + apply RCossa. destruct case_RCast. simpl. @@ -425,5 +420,6 @@ Section HaskSkolemizer. simpl. apply (Prelude_error "CASE: BIG FIXME"). Defined. + Transparent take_arg_types_as_tree. End HaskSkolemizer. diff --git a/src/HaskStrongTypes.v b/src/HaskStrongTypes.v index 035bc9a..764e95f 100644 --- a/src/HaskStrongTypes.v +++ b/src/HaskStrongTypes.v @@ -239,6 +239,48 @@ Fixpoint take_arg_types {TV}{κ}(exp: RawHaskType TV κ) {struct exp} : list (Ra | _ => nil end. +Fixpoint count_arg_types {TV}{κ}(exp: RawHaskType TV κ) {struct exp} : nat := + match exp as E in RawHaskType _ K return nat with + | TApp κ₁ κ₂ x y => + (match κ₁ as K1 return RawHaskType TV (κ₂ ⇛ K1) -> nat -> nat with + | KindStar => + match κ₂ as K2 return RawHaskType TV (K2 ⇛ KindStar) -> nat -> nat with + | KindStar => fun x' => + match x' return nat -> nat with + | TApp κ₁'' κ₂'' w'' x'' => + match κ₂'' as K2'' return RawHaskType TV K2'' -> nat -> nat with + | KindStar => + match w'' with + | TArrow => fun a b => S b + | _ => fun _ _ => 0 + end + | _ => fun _ _ => 0 + end x'' + | _ => fun _ => 0 + end + | _ => fun _ _ => 0 + end + | _ => fun _ _ => 0 + end) x (count_arg_types y) + | _ => 0 + end. + + Definition ite_unit : ∀ Γ, InstantiatedTypeEnv (fun _ => unit) Γ. + intros. + induction Γ. + apply INil. + apply ICons; auto. + apply tt. + Defined. + +Definition take_arg_type {Γ}{κ}(ht:HaskType Γ κ) : (gt (count_arg_types (ht _ (ite_unit _))) 0) -> HaskType Γ κ := + fun pf => + fun TV ite => + match take_arg_types (ht TV ite) with + | nil => Prelude_error "impossible" + | x::y => x + end. + (* From (t1->(t2->(t3-> ... t))), return t *) (* this is a billion times uglier than it needs to be as a result of how primitive Coq's termiation checker is *) Fixpoint drop_arg_types {TV}{κ}(exp: RawHaskType TV κ) : RawHaskType TV κ := -- 1.7.10.4