From 013a93a8fbae4b8c8df290e9eff226f786770762 Mon Sep 17 00:00:00 2001 From: Adam Megacz Date: Sun, 15 May 2011 00:55:34 -0700 Subject: [PATCH] more efficient encoding of function types --- src/HaskFlattener.v | 14 +++++----- src/HaskSkolemizer.v | 74 ++++++++++++++++++++++++++++++++++++++++++-------- 2 files changed, 70 insertions(+), 18 deletions(-) diff --git a/src/HaskFlattener.v b/src/HaskFlattener.v index 09f7070..ed3ca43 100644 --- a/src/HaskFlattener.v +++ b/src/HaskFlattener.v @@ -260,7 +260,7 @@ Section HaskFlattener. | TCoerc _ t1 t2 t => TCoerc (flatten_rawtype t1) (flatten_rawtype t2) (flatten_rawtype t) | TArrow => TArrow | TCode ec e => let e' := flatten_rawtype e - in ga_mk_raw ec (unleaves (take_arg_types e')) [drop_arg_types e'] + in ga_mk_raw ec (unleaves_ (take_arg_types e')) [drop_arg_types e'] | TyFunApp tfc kl k lt => TyFunApp tfc kl k (flatten_rawtype_list _ lt) end with flatten_rawtype_list {TV}(lk:list Kind)(exp:@RawHaskTypeList TV lk) : @RawHaskTypeList TV lk := @@ -538,6 +538,7 @@ Section HaskFlattener. (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) B)) (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) A)) @@ nil]] with + | RId a => let case_RId := tt in ga_id _ _ _ _ _ | RCanL a => let case_RCanL := tt in ga_uncancell _ _ _ _ _ | RCanR a => let case_RCanR := tt in ga_uncancelr _ _ _ _ _ | RuCanL a => let case_RuCanL := tt in ga_cancell _ _ _ _ _ @@ -592,6 +593,7 @@ Section HaskFlattener. match r as R in Arrange A B return Arrange (mapOptionTree (flatten_leveled_type ) (drop_lev _ A)) (mapOptionTree (flatten_leveled_type ) (drop_lev _ B)) with + | RId a => let case_RId := tt in RId _ | RCanL a => let case_RCanL := tt in RCanL _ | RCanR a => let case_RCanR := tt in RCanR _ | RuCanL a => let case_RuCanL := tt in RuCanL _ @@ -621,6 +623,7 @@ Section HaskFlattener. apply nd_rule. apply RArrange. induction r; simpl. + apply RId. apply RCanL. apply RCanR. apply RuCanL. @@ -852,9 +855,6 @@ Section HaskFlattener. apply IHt2. Defined. - Axiom extensionality : forall Γ Q (f g:forall TV, InstantiatedTypeEnv TV Γ -> Q TV), - (forall tv ite, f tv ite = g tv ite) -> f=g. - Lemma krunk : forall Γ (ec:HaskTyVar Γ ECKind) t, flatten_type (<[ ec |- t ]>) = @ga_mk Γ (v2t ec) @@ -864,7 +864,7 @@ Section HaskFlattener. unfold flatten_type at 1. simpl. unfold ga_mk. - apply extensionality. + apply phoas_extensionality. intros. unfold v2t. unfold ga_mk_raw. @@ -874,9 +874,9 @@ Section HaskFlattener. simpl. replace (flatten_type (drop_arg_types_as_tree t) tv ite) with (drop_arg_types (flatten_rawtype (t tv ite))). - replace (unleaves (take_arg_types (flatten_rawtype (t tv ite)))) + replace (unleaves_ (take_arg_types (flatten_rawtype (t tv ite)))) with ((mapOptionTree (fun x : HaskType Γ ★ => flatten_type x tv ite) - (unleaves + (unleaves_ (take_trustme (count_arg_types (t (fun _ : Kind => unit) (ite_unit Γ))) (fun TV : Kind → Type => take_arg_types ○ t TV))))). reflexivity. diff --git a/src/HaskSkolemizer.v b/src/HaskSkolemizer.v index 2c1c9d2..bfbdf0e 100644 --- a/src/HaskSkolemizer.v +++ b/src/HaskSkolemizer.v @@ -66,11 +66,20 @@ Section HaskSkolemizer. | a::b => mkArrows b (a ---> t) end. +(* Fixpoint unleaves_ {Γ}(t:Tree ??(LeveledHaskType Γ ★))(l:list (HaskType Γ ★)) lev : Tree ??(LeveledHaskType Γ ★) := match l with | nil => t | a::b => unleaves_ (t,,[a @@ lev]) b lev end. +*) + (* weak inverse of "leaves" *) + Fixpoint unleaves_ {A:Type}(l:list A) : Tree (option A) := + match l with + | nil => [] + | (a::nil) => [a] + | (a::b) => [a],,(unleaves_ b) + end. (* rules of skolemized proofs *) Definition getΓ (j:Judg) := match j with Γ > _ > _ |- _ => Γ end. @@ -105,8 +114,11 @@ Section HaskSkolemizer. end) end. + Axiom phoas_extensionality : forall Γ Q (f g:forall TV, InstantiatedTypeEnv TV Γ -> Q TV), + (forall tv ite, f tv ite = g tv ite) -> f=g. + Definition take_arg_types_as_tree {Γ}(ht:HaskType Γ ★) : Tree ??(HaskType Γ ★ ) := - unleaves + unleaves_ (take_trustme (count_arg_types (ht _ (ite_unit _))) (fun TV ite => take_arg_types (ht TV ite))). @@ -117,13 +129,47 @@ Section HaskSkolemizer. Implicit Arguments take_arg_types_as_tree [[Γ]]. Implicit Arguments drop_arg_types_as_tree [[Γ]]. - Lemma take_works : forall {Γ}(t1 t2:HaskType Γ ★), - take_arg_types_as_tree (t1 ---> t2) = [t1],,(take_arg_types_as_tree t2). + Definition take_arrange : forall {Γ} (tx te:HaskType Γ ★) lev, + Arrange ([tx @@ lev],, take_arg_types_as_tree te @@@ lev) + (take_arg_types_as_tree (tx ---> te) @@@ lev). intros. - unfold take_arg_types_as_tree at 1. - simpl. - admit. - Qed. + destruct (eqd_dec ([tx],, take_arg_types_as_tree te) (take_arg_types_as_tree (tx ---> te))). + rewrite <- e. + simpl. + apply RId. + unfold take_arg_types_as_tree. + Opaque take_arg_types_as_tree. + simpl. + destruct (count_arg_types (te (fun _ : Kind => unit) (ite_unit Γ))). + simpl. + replace (tx) with (fun (TV : Kind → Type) (ite : InstantiatedTypeEnv TV Γ) => tx TV ite). + apply RCanR. + apply phoas_extensionality. + reflexivity. + apply (Prelude_error "should not be possible"). + Defined. + Transparent take_arg_types_as_tree. + + Definition take_unarrange : forall {Γ} (tx te:HaskType Γ ★) lev, + Arrange (take_arg_types_as_tree (tx ---> te) @@@ lev) + ([tx @@ lev],, take_arg_types_as_tree te @@@ lev). + intros. + destruct (eqd_dec ([tx],, take_arg_types_as_tree te) (take_arg_types_as_tree (tx ---> te))). + rewrite <- e. + simpl. + apply RId. + unfold take_arg_types_as_tree. + Opaque take_arg_types_as_tree. + simpl. + destruct (count_arg_types (te (fun _ : Kind => unit) (ite_unit Γ))). + simpl. + replace (tx) with (fun (TV : Kind → Type) (ite : InstantiatedTypeEnv TV Γ) => tx TV ite). + apply RuCanR. + apply phoas_extensionality. + reflexivity. + apply (Prelude_error "should not be possible"). + Defined. + Transparent take_arg_types_as_tree. Lemma drop_works : forall {Γ}(t1 t2:HaskType Γ ★), drop_arg_types_as_tree (t1 ---> t2) = (drop_arg_types_as_tree t2). @@ -296,12 +342,14 @@ Section HaskSkolemizer. simpl. apply RLam. simpl. - rewrite take_works. rewrite drop_works. apply nd_rule. apply SFlat. apply RArrange. + eapply RComp. apply RCossa. + apply RLeft. + apply take_arrange. destruct case_RCast. simpl. @@ -328,7 +376,6 @@ Section HaskSkolemizer. apply nd_rule. apply SFlat. apply RApp. - rewrite take_works. rewrite drop_works. set (check_hof tx) as hof_tx. destruct hof_tx; [ apply (Prelude_error "attempt tp apply a higher-order function at depth>0") | idtac ]. @@ -346,8 +393,13 @@ Section HaskSkolemizer. apply SFlat. apply RArrange. apply RCanR. - eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply RArrange; apply RAssoc ]. - apply nd_rule; apply SFlat; apply RArrange; apply RLeft; eapply RExch. + apply nd_rule. + apply SFlat. + apply RArrange. + eapply RComp; [ idtac | eapply RAssoc ]. + apply RLeft. + eapply RComp; [ idtac | apply RExch ]. + apply take_unarrange. destruct case_RLet. simpl. -- 1.7.10.4