X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskFlattener.v;h=08485a1307f781e3923c00b53c4c302190dcd45a;hp=47315bb2b265b87f1dc001b8bd8ce69d31193cd7;hb=a9a60dc234f76a4740b32c0f62aa0fe3a89fea83;hpb=1215a7fa07083dadaad909ca023a305fc75f7632 diff --git a/src/HaskFlattener.v b/src/HaskFlattener.v index 47315bb..08485a1 100644 --- a/src/HaskFlattener.v +++ b/src/HaskFlattener.v @@ -30,6 +30,8 @@ Require Import HaskStrongToProof. Require Import HaskProofToStrong. Require Import HaskWeakToStrong. +Require Import HaskSkolemizer. + Open Scope nd_scope. Set Printing Width 130. @@ -165,10 +167,39 @@ Section HaskFlattener. auto. Qed. + Lemma take_lemma' : forall Γ (lev:HaskLevel Γ) x, take_lev lev (x @@@ lev) = x @@@ lev. + intros. + induction x. + destruct a; simpl; try reflexivity. + apply take_lemma. + simpl. + rewrite <- IHx1 at 2. + rewrite <- IHx2 at 2. + reflexivity. + Qed. +(* + Lemma drop_lev_lemma' : forall Γ (lev:HaskLevel Γ) x, drop_lev lev (x @@@ lev) = []. + intros. + induction x. + destruct a; simpl; try reflexivity. + apply drop_lev_lemma. + simpl. + change (@drop_lev _ lev (x1 @@@ lev ,, x2 @@@ lev)) + with ((@drop_lev _ lev (x1 @@@ lev)) ,, (@drop_lev _ lev (x2 @@@ lev))). + simpl. + rewrite IHx1. + rewrite IHx2. + reflexivity. + Qed. +*) Ltac drop_simplify := match goal with | [ |- context[@drop_lev ?G ?L [ ?X @@ ?L ] ] ] => rewrite (drop_lev_lemma G L X) +(* + | [ |- context[@drop_lev ?G ?L [ ?X @@@ ?L ] ] ] => + rewrite (drop_lev_lemma' G L X) +*) | [ |- context[@drop_lev ?G (?E :: ?L) [ ?X @@ (?E :: ?L) ] ] ] => rewrite (drop_lev_lemma_s G L E X) | [ |- context[@drop_lev ?G ?N (?A,,?B)] ] => @@ -181,6 +212,8 @@ Section HaskFlattener. match goal with | [ |- context[@take_lev ?G ?L [ ?X @@ ?L ] ] ] => rewrite (take_lemma G L X) + | [ |- context[@take_lev ?G ?L [ ?X @@@ ?L ] ] ] => + rewrite (take_lemma' G L X) | [ |- context[@take_lev ?G ?N (?A,,?B)] ] => change (@take_lev G N (A,,B)) with ((@take_lev G N A),,(@take_lev G N B)) | [ |- context[@take_lev ?G ?N (T_Leaf None)] ] => @@ -204,11 +237,13 @@ Section HaskFlattener. Definition ga_mk_tree {Γ}(ec:HaskType Γ ECKind)(tr:Tree ??(HaskType Γ ★)) : HaskType Γ ★ := fun TV ite => ga_mk_tree' (ec TV ite) (mapOptionTree (fun x => x TV ite) tr). - Definition ga_mk_raw {TV}(ec:RawHaskType TV ECKind )(ant suc:Tree ??(RawHaskType TV ★)) : RawHaskType TV ★ := - gaTy TV ec (ga_mk_tree' ec ant) (ga_mk_tree' ec suc). + Definition ga_mk_raw {TV}(ec:RawHaskType TV ECKind)(ant suc:Tree ??(RawHaskType TV ★)) : RawHaskType TV ★ := + gaTy TV ec + (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: @@ -224,7 +259,8 @@ Section HaskFlattener. | TCon tc => TCon tc | TCoerc _ t1 t2 t => TCoerc (flatten_rawtype t1) (flatten_rawtype t2) (flatten_rawtype t) | TArrow => TArrow - | TCode ec e => ga_mk_raw ec [] [flatten_rawtype e] + | TCode ec e => let e' := flatten_rawtype 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 := @@ -238,12 +274,12 @@ Section HaskFlattener. Fixpoint levels_to_tcode {Γ}(ht:HaskType Γ ★)(lev:HaskLevel Γ) : HaskType Γ ★ := match lev with - | nil => ht - | ec::lev' => fun TV ite => TCode (v2t ec TV ite) (levels_to_tcode ht lev' TV ite) + | nil => flatten_type ht + | ec::lev' => @ga_mk _ (v2t ec) [] [levels_to_tcode ht lev'] end. Definition flatten_leveled_type {Γ}(ht:LeveledHaskType Γ ★) : LeveledHaskType Γ ★ := - flatten_type (levels_to_tcode (unlev ht) (getlev ht)) @@ nil. + levels_to_tcode (unlev ht) (getlev ht) @@ nil. (* AXIOMS *) @@ -335,8 +371,8 @@ Section HaskFlattener. ND Rule [] [ Γ > Δ > [x@@lev] |- [y@@lev] ] -> ND Rule [ Γ > Δ > ant |- [x@@lev] ] [ Γ > Δ > ant |- [y@@lev] ]. intros. - eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanL ]. - eapply nd_comp; [ idtac | eapply nd_rule; apply (@RLet Γ Δ [] ant y x lev) ]. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanR ]. + eapply nd_comp; [ idtac | eapply nd_rule; apply RLet ]. eapply nd_comp; [ apply nd_rlecnac | idtac ]. apply nd_prod. apply nd_id. @@ -344,116 +380,117 @@ Section HaskFlattener. apply X. eapply nd_rule. eapply RArrange. - apply RuCanL. - Defined. - - Definition postcompose' : ∀ Γ Δ ec lev a b c Σ, - ND Rule [] [ Γ > Δ > Σ |- [@ga_mk Γ ec a b @@ lev] ] -> - ND Rule [] [ Γ > Δ > Σ,,[@ga_mk Γ ec b c @@ lev] |- [@ga_mk Γ ec a c @@ lev] ]. - intros. - eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RExch ]. - eapply nd_comp; [ idtac - | eapply nd_rule; apply (@RLet Γ Δ [@ga_mk _ ec b c @@lev] Σ (@ga_mk _ ec a c) (@ga_mk _ ec a b) lev) ]. - eapply nd_comp; [ apply nd_llecnac | idtac ]. - apply nd_prod. - apply X. - eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RExch ]. - apply ga_comp. - Defined. + apply RuCanR. + Defined. Definition precompose Γ Δ ec : forall a x y z lev, ND Rule [ Γ > Δ > a |- [@ga_mk _ ec y z @@ lev] ] [ Γ > Δ > a,,[@ga_mk _ ec x y @@ lev] |- [@ga_mk _ ec x z @@ lev] ]. intros. - eapply nd_comp. - apply nd_rlecnac. - eapply nd_comp. - eapply nd_prod. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ]. + eapply nd_comp; [ apply nd_rlecnac | idtac ]. + apply nd_prod. apply nd_id. - eapply ga_comp. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RExch ]. + apply ga_comp. + Defined. - eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RExch ]. + Definition precompose' Γ Δ ec : forall a b x y z lev, + ND Rule + [ Γ > Δ > a,,b |- [@ga_mk _ ec y z @@ lev] ] + [ Γ > Δ > a,,([@ga_mk _ ec x y @@ lev],,b) |- [@ga_mk _ ec x z @@ lev] ]. + intros. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RLeft; eapply RExch ]. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCossa ]. + apply precompose. + Defined. - apply nd_rule. - apply RLet. + Definition postcompose_ Γ Δ ec : forall a x y z lev, + ND Rule + [ Γ > Δ > a |- [@ga_mk _ ec x y @@ lev] ] + [ Γ > Δ > a,,[@ga_mk _ ec y z @@ lev] |- [@ga_mk _ ec x z @@ lev] ]. + intros. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ]. + eapply nd_comp; [ apply nd_rlecnac | idtac ]. + apply nd_prod. + apply nd_id. + apply ga_comp. Defined. - Definition precompose' : ∀ Γ Δ ec lev a b c Σ, - ND Rule [] [ Γ > Δ > Σ |- [@ga_mk Γ ec b c @@ lev] ] -> - ND Rule [] [ Γ > Δ > Σ,,[@ga_mk Γ ec a b @@ lev] |- [@ga_mk Γ ec a c @@ lev] ]. - intros. - eapply nd_comp. - apply X. - apply precompose. - Defined. + Definition postcompose Γ Δ ec : forall x y z lev, + ND Rule [] [ Γ > Δ > [] |- [@ga_mk _ ec x y @@ lev] ] -> + ND Rule [] [ Γ > Δ > [@ga_mk _ ec y z @@ lev] |- [@ga_mk _ ec x z @@ lev] ]. + intros. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanL ]. + eapply nd_comp; [ idtac | eapply postcompose_ ]. + apply X. + Defined. - Definition postcompose : ∀ Γ Δ ec lev a b c, - ND Rule [] [ Γ > Δ > [] |- [@ga_mk Γ ec a b @@ lev] ] -> - ND Rule [] [ Γ > Δ > [@ga_mk Γ ec b c @@ lev] |- [@ga_mk Γ ec a c @@ lev] ]. - intros. - eapply nd_comp. - apply postcompose'. - apply X. - apply nd_rule. - apply RArrange. - apply RCanL. - Defined. + Definition first_nd : ∀ Γ Δ ec lev a b c Σ, + ND Rule [ Γ > Δ > Σ |- [@ga_mk Γ ec a b @@ lev] ] + [ Γ > Δ > Σ |- [@ga_mk Γ ec (a,,c) (b,,c) @@ lev] ]. + intros. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanR ]. + eapply nd_comp; [ idtac | eapply nd_rule; apply RLet ]. + eapply nd_comp; [ apply nd_rlecnac | idtac ]. + apply nd_prod. + apply nd_id. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RuCanR ]. + apply ga_first. + Defined. Definition firstify : ∀ Γ Δ ec lev a b c Σ, - ND Rule [] [ Γ > Δ > Σ |- [@ga_mk Γ ec a b @@ lev] ] -> + ND Rule [] [ Γ > Δ > Σ |- [@ga_mk Γ ec a b @@ lev] ] -> ND Rule [] [ Γ > Δ > Σ |- [@ga_mk Γ ec (a,,c) (b,,c) @@ lev] ]. intros. - eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanL ]. - eapply nd_comp; [ idtac | eapply nd_rule; apply RLet ]. - eapply nd_comp; [ apply nd_llecnac | idtac ]. - apply nd_prod. + eapply nd_comp. apply X. - eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RuCanL ]. - apply ga_first. + apply first_nd. Defined. - Definition secondify : ∀ Γ Δ ec lev a b c Σ, - ND Rule [] [ Γ > Δ > Σ |- [@ga_mk Γ ec a b @@ lev] ] -> - ND Rule [] [ Γ > Δ > Σ |- [@ga_mk Γ ec (c,,a) (c,,b) @@ lev] ]. + Definition second_nd : ∀ Γ Δ ec lev a b c Σ, + ND Rule + [ Γ > Δ > Σ |- [@ga_mk Γ ec a b @@ lev] ] + [ Γ > Δ > Σ |- [@ga_mk Γ ec (c,,a) (c,,b) @@ lev] ]. intros. - eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanL ]. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanR ]. eapply nd_comp; [ idtac | eapply nd_rule; apply RLet ]. - eapply nd_comp; [ apply nd_llecnac | idtac ]. + eapply nd_comp; [ apply nd_rlecnac | idtac ]. apply nd_prod. - apply X. - eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RuCanL ]. + apply nd_id. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RuCanR ]. apply ga_second. Defined. - Lemma ga_unkappa : ∀ Γ Δ ec l a b Σ, - ND Rule - [Γ > Δ > Σ |- [@ga_mk Γ ec a b @@ l] ] - [Γ > Δ > Σ,,[@ga_mk Γ ec [] a @@ l] |- [@ga_mk Γ ec [] b @@ l] ]. + Definition secondify : ∀ Γ Δ ec lev a b c Σ, + ND Rule [] [ Γ > Δ > Σ |- [@ga_mk Γ ec a b @@ lev] ] -> + ND Rule [] [ Γ > Δ > Σ |- [@ga_mk Γ ec (c,,a) (c,,b) @@ lev] ]. intros. - set (ga_comp Γ Δ ec l [] a b) as q. - - set (@RLet Γ Δ) as q'. - set (@RLet Γ Δ [@ga_mk _ ec [] a @@ l] Σ (@ga_mk _ ec [] b) (@ga_mk _ ec a b) l) as q''. eapply nd_comp. - Focus 2. - eapply nd_rule. - eapply RArrange. - apply RExch. + apply X. + apply second_nd. + Defined. - eapply nd_comp. - Focus 2. - eapply nd_rule. - apply q''. + Lemma ga_unkappa : ∀ Γ Δ ec l a b Σ x, + ND Rule + [Γ > Δ > Σ |- [@ga_mk Γ ec (a,,x) b @@ l] ] + [Γ > Δ > Σ,,[@ga_mk Γ ec [] a @@ l] |- [@ga_mk Γ ec x b @@ l] ]. + intros. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RExch ]. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ]. + eapply nd_comp; [ apply nd_llecnac | idtac ]. + apply nd_prod. + apply ga_first. - idtac. - clear q'' q'. - eapply nd_comp. - apply nd_rlecnac. - apply nd_prod. - apply nd_id. - apply q. - Defined. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ]. + eapply nd_comp; [ apply nd_llecnac | idtac ]. + apply nd_prod. + apply postcompose. + apply ga_uncancell. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RExch ]. + apply precompose. + Defined. (* useful for cutting down on the pretty-printed noise @@ -477,6 +514,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 _ _ _ _ _ @@ -497,17 +535,17 @@ Section HaskFlattener. set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) c)) as c' in *. eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RCanL ]. eapply nd_comp; [ idtac | eapply nd_rule; apply - (@RLet Γ Δ [] [] (@ga_mk _ (v2t ec) a' c') (@ga_mk _ (v2t ec) a' b')) ]. + (@RLet Γ Δ [] [] (@ga_mk _ (v2t ec) a' b') (@ga_mk _ (v2t ec) a' c')) ]. eapply nd_comp; [ apply nd_llecnac | idtac ]. apply nd_prod. apply r2'. - eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RuCanL ]. - eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RCanR ]. - eapply nd_comp; [ idtac | eapply nd_rule; apply - (@RLet Γ Δ [@ga_mk _ (v2t ec) a' b' @@ _] [] (@ga_mk _ (v2t ec) a' c') (@ga_mk _ (v2t ec) b' c'))]. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RuCanR ]. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RCanL ]. + eapply nd_comp; [ idtac | eapply nd_rule; apply RLet ]. eapply nd_comp; [ apply nd_llecnac | idtac ]. eapply nd_prod. apply r1'. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RExch ]. apply ga_comp. Defined. @@ -531,6 +569,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 _ @@ -560,13 +599,14 @@ Section HaskFlattener. apply nd_rule. apply RArrange. induction r; simpl. + apply RId. apply RCanL. apply RCanR. apply RuCanL. apply RuCanR. apply RAssoc. apply RCossa. - apply RExch. + apply RExch. (* TO DO: check for all-leaf trees here *) apply RWeak. apply RCont. apply RLeft; auto. @@ -584,31 +624,32 @@ Section HaskFlattener. intro pfa. intro pfb. apply secondify with (c:=a) in pfb. - eapply nd_comp. - Focus 2. + apply firstify with (c:=[]) in pfa. eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ]. eapply nd_comp; [ eapply nd_llecnac | idtac ]. - eapply nd_prod. - apply pfb. - clear pfb. - apply postcompose'. - eapply nd_comp. + apply nd_prod. apply pfa. clear pfa. - apply boost. + + eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ]. + eapply nd_comp; [ apply nd_llecnac | idtac ]. + apply nd_prod. eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanL ]. - apply precompose'. + eapply nd_comp; [ idtac | eapply postcompose_ ]. apply ga_uncancelr. - apply nd_id. + + eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RExch ]. + eapply nd_comp; [ idtac | eapply precompose ]. + apply pfb. Defined. Definition arrange_brak : forall Γ Δ ec succ t, ND Rule - [Γ > Δ > mapOptionTree (flatten_leveled_type ) (drop_lev (ec :: nil) succ),, - [(@ga_mk _ (v2t ec) [] - (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: nil) succ))) - @@ nil] |- [(@ga_mk _ (v2t ec) [] [flatten_type t]) @@ nil]] - [Γ > Δ > mapOptionTree (flatten_leveled_type ) succ |- [(@ga_mk _ (v2t ec) [] [flatten_type t]) @@ nil]]. + [Γ > Δ > + [(@ga_mk _ (v2t ec) [] (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: nil) succ))) @@ nil],, + mapOptionTree (flatten_leveled_type ) (drop_lev (ec :: nil) succ) |- [t @@ nil]] + [Γ > Δ > mapOptionTree (flatten_leveled_type ) succ |- [t @@ nil]]. + intros. unfold drop_lev. set (@arrange' _ succ (levelMatch (ec::nil))) as q. @@ -620,6 +661,7 @@ Section HaskFlattener. apply y. idtac. clear y q. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RExch ]. simpl. eapply nd_comp; [ apply nd_llecnac | idtac ]. eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ]. @@ -646,6 +688,9 @@ Section HaskFlattener. unfold flatten_leveled_type. simpl. unfold flatten_type. + simpl. + unfold ga_mk. + simpl. apply RVar. simpl. apply ga_id. @@ -657,26 +702,117 @@ Section HaskFlattener. apply IHsucc2. Defined. + Definition arrange_empty_tree : forall {T}{A}(q:Tree A)(t:Tree ??T), + t = mapTree (fun _:A => None) q -> + Arrange t []. + intros T A q. + induction q; intros. + simpl in H. + rewrite H. + apply RId. + simpl in *. + destruct t; try destruct o; inversion H. + set (IHq1 _ H1) as x1. + set (IHq2 _ H2) as x2. + eapply RComp. + eapply RRight. + rewrite <- H1. + apply x1. + eapply RComp. + apply RCanL. + rewrite <- H2. + apply x2. + Defined. + +(* Definition unarrange_empty_tree : forall {T}{A}(t:Tree ??T)(q:Tree A), + t = mapTree (fun _:A => None) q -> + Arrange [] t. + Defined.*) + + Definition decide_tree_empty : forall {T:Type}(t:Tree ??T), + sum { q:Tree unit & t = mapTree (fun _ => None) q } unit. + intro T. + refine (fix foo t := + match t with + | T_Leaf x => _ + | T_Branch b1 b2 => let b1' := foo b1 in let b2' := foo b2 in _ + end). + intros. + destruct x. + right; apply tt. + left. + exists (T_Leaf tt). + auto. + destruct b1'. + destruct b2'. + destruct s. + destruct s0. + subst. + left. + exists (x,,x0). + reflexivity. + right; auto. + right; auto. + Defined. + Definition arrange_esc : forall Γ Δ ec succ t, ND Rule - [Γ > Δ > mapOptionTree (flatten_leveled_type ) succ |- [(@ga_mk _ (v2t ec) [] [flatten_type t]) @@ nil]] - [Γ > Δ > mapOptionTree (flatten_leveled_type ) (drop_lev (ec :: nil) succ),, - [(@ga_mk _ (v2t ec) [] - (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: nil) succ))) @@ nil] - |- [(@ga_mk _ (v2t ec) [] [flatten_type t]) @@ nil]]. + [Γ > Δ > mapOptionTree (flatten_leveled_type ) succ |- [t @@ nil]] + [Γ > Δ > + [(@ga_mk _ (v2t ec) [] (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: nil) succ))) @@ nil],, + mapOptionTree (flatten_leveled_type ) (drop_lev (ec :: nil) succ) |- [t @@ nil]]. intros. - unfold drop_lev. set (@arrange _ succ (levelMatch (ec::nil))) as q. + set (@drop_lev Γ (ec::nil) succ) as q'. + assert (@drop_lev Γ (ec::nil) succ=q') as H. + reflexivity. + unfold drop_lev in H. + unfold mkDropFlags in H. + rewrite H in q. + clear H. set (arrangeMap _ _ flatten_leveled_type q) as y. eapply nd_comp. eapply nd_rule. eapply RArrange. apply y. - idtac. clear y q. + set (mapOptionTree flatten_leveled_type (dropT (mkFlags (liftBoolFunc false (bnot ○ levelMatch (ec :: nil))) succ))) as q. + destruct (decide_tree_empty q); [ idtac | apply (Prelude_error "escapifying open code not yet supported") ]. + destruct s. + + simpl. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RExch ]. + set (fun z z' => @RLet Γ Δ z (mapOptionTree flatten_leveled_type q') t z' nil) as q''. + eapply nd_comp; [ idtac | eapply nd_rule; apply RLet ]. + clear q''. + eapply nd_comp; [ apply nd_rlecnac | idtac ]. + apply nd_prod. + apply nd_rule. + apply RArrange. + eapply RComp; [ idtac | apply RCanR ]. + apply RLeft. + apply (@arrange_empty_tree _ _ _ _ e). + + eapply nd_comp. + eapply nd_rule. + eapply (@RVar Γ Δ t nil). + apply nd_rule. + apply RArrange. + eapply RComp. + apply RuCanR. + apply RLeft. + apply RWeak. +(* + eapply decide_tree_empty. + + simpl. + set (dropT (mkFlags (liftBoolFunc false (bnot ○ levelMatch (ec :: nil))) succ)) as escapified. + destruct (decide_tree_empty escapified). + induction succ. destruct a. + unfold drop_lev. destruct l. simpl. unfold mkDropFlags; simpl. @@ -700,6 +836,7 @@ Section HaskFlattener. apply RLeft. apply RWeak. apply (Prelude_error "escapifying code with multi-leaf antecedents is not supported"). +*) Defined. Lemma mapOptionTree_distributes @@ -708,43 +845,111 @@ Section HaskFlattener. reflexivity. Qed. - Definition decide_tree_empty : forall {T:Type}(t:Tree ??T), - sum { q:Tree unit & t = mapTree (fun _ => None) q } unit. - intro T. - refine (fix foo t := - match t with - | T_Leaf x => _ - | T_Branch b1 b2 => let b1' := foo b1 in let b2' := foo b2 in _ - end). + Lemma unlev_relev : forall {Γ}(t:Tree ??(HaskType Γ ★)) lev, mapOptionTree unlev (t @@@ lev) = t. intros. - destruct x. - right; apply tt. - left. - exists (T_Leaf tt). - auto. - destruct b1'. - destruct b2'. - destruct s. - destruct s0. - subst. - left. - exists (x,,x0). + induction t. + destruct a; reflexivity. + rewrite <- IHt1 at 2. + rewrite <- IHt2 at 2. reflexivity. - right; auto. - right; auto. + Qed. + + Lemma tree_of_nothing : forall Γ ec t, + Arrange (mapOptionTree flatten_leveled_type (drop_lev(Γ:=Γ) (ec :: nil) (t @@@ (ec :: nil)))) []. + intros. + induction t; try destruct o; try destruct a. + simpl. + drop_simplify. + simpl. + apply RId. + simpl. + apply RId. + eapply RComp; [ idtac | apply RCanL ]. + eapply RComp; [ idtac | eapply RLeft; apply IHt2 ]. + Opaque drop_lev. + simpl. + Transparent drop_lev. + idtac. + drop_simplify. + apply RRight. + apply IHt1. + Defined. + + Lemma tree_of_nothing' : forall Γ ec t, + Arrange [] (mapOptionTree flatten_leveled_type (drop_lev(Γ:=Γ) (ec :: nil) (t @@@ (ec :: nil)))). + intros. + induction t; try destruct o; try destruct a. + simpl. + drop_simplify. + simpl. + apply RId. + simpl. + apply RId. + eapply RComp; [ apply RuCanL | idtac ]. + eapply RComp; [ eapply RRight; apply IHt1 | idtac ]. + Opaque drop_lev. + simpl. + Transparent drop_lev. + idtac. + drop_simplify. + apply RLeft. + apply IHt2. Defined. + Lemma krunk : forall Γ (ec:HaskTyVar Γ ECKind) t, + flatten_type (<[ ec |- t ]>) + = @ga_mk Γ (v2t ec) + (mapOptionTree flatten_type (take_arg_types_as_tree t)) + [ flatten_type (drop_arg_types_as_tree t)]. + intros. + unfold flatten_type at 1. + simpl. + unfold ga_mk. + apply phoas_extensionality. + intros. + unfold v2t. + unfold ga_mk_raw. + unfold ga_mk_tree. + rewrite <- mapOptionTree_compose. + unfold take_arg_types_as_tree. + 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)))) + with ((mapOptionTree (fun x : HaskType Γ ★ => flatten_type x tv ite) + (unleaves_ + (take_trustme (count_arg_types (t (fun _ : Kind => unit) (ite_unit Γ))) + (fun TV : Kind → Type => take_arg_types ○ t TV))))). + reflexivity. + unfold flatten_type. + clear hetmet_flatten. + clear hetmet_unflatten. + clear hetmet_id. + clear gar. + set (t tv ite) as x. + admit. + admit. + Qed. + Definition flatten_proof : forall {h}{c}, - ND Rule h c -> - ND Rule (mapOptionTree (flatten_judgment ) h) (mapOptionTree (flatten_judgment ) c). + ND SRule h c -> + ND Rule (mapOptionTree (flatten_judgment ) h) (mapOptionTree (flatten_judgment ) c). intros. eapply nd_map'; [ idtac | apply X ]. clear h c X. intros. simpl in *. - refine (match X as R in Rule H C with + refine + (match X as R in SRule H C with + | SBrak Γ Δ t ec succ lev => let case_SBrak := tt in _ + | SEsc Γ Δ t ec succ lev => let case_SEsc := tt in _ + | SFlat h c r => let case_SFlat := tt in _ + end). + + destruct case_SFlat. + refine (match r as R in Rule H C with | RArrange Γ Δ a b x d => let case_RArrange := tt in _ | RNote Γ Δ Σ τ l n => let case_RNote := tt in _ | RLit Γ Δ l _ => let case_RLit := tt in _ @@ -758,6 +963,7 @@ Section HaskFlattener. | RAbsCo Γ Δ Σ κ σ σ₁ σ₂ lev => let case_RAbsCo := tt in _ | RApp Γ Δ Σ₁ Σ₂ tx te lev => let case_RApp := tt in _ | RLet Γ Δ Σ₁ Σ₂ σ₁ σ₂ lev => let case_RLet := tt in _ + | RWhere Γ Δ Σ₁ Σ₂ Σ₃ σ₁ σ₂ lev => let case_RWhere := tt in _ | RJoin Γ p lri m x q => let case_RJoin := tt in _ | RVoid _ _ => let case_RVoid := tt in _ | RBrak Γ Δ t ec succ lev => let case_RBrak := tt in _ @@ -770,46 +976,10 @@ Section HaskFlattener. apply (flatten_arrangement'' Γ Δ a b x d). destruct case_RBrak. - simpl. - destruct lev. - change ([flatten_type (<[ ec |- t ]>) @@ nil]) - with ([ga_mk (v2t ec) [] [flatten_type t] @@ nil]). - refine (ga_unkappa Γ Δ (v2t ec) nil (mapOptionTree (flatten_type ○ unlev) (take_lev (ec::nil) succ)) _ - (mapOptionTree (flatten_leveled_type) (drop_lev (ec::nil) succ)) ;; _ ). - apply arrange_brak. - apply (Prelude_error "found Brak at depth >0 indicating 3-level code; only two-level code is currently supported"). + apply (Prelude_error "found unskolemized Brak rule; this shouldn't happen"). destruct case_REsc. - simpl. - destruct lev. - simpl. - change ([flatten_leveled_type (<[ ec |- t ]> @@ nil)]) - with ([ga_mk (v2t ec) [] [flatten_type t] @@ nil]). - eapply nd_comp; [ apply arrange_esc | idtac ]. - set (decide_tree_empty (take_lev (ec :: nil) succ)) as q'. - destruct q'. - destruct s. - rewrite e. - clear e. - - eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanR ]. - eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ]. - eapply nd_comp; [ apply nd_llecnac | idtac ]. - apply nd_prod; [ idtac | eapply boost ]. - induction x. - apply ga_id. - eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanR ]. - simpl. - apply ga_join. - apply IHx1. - apply IHx2. - simpl. - apply postcompose. - apply ga_drop. - - (* environment has non-empty leaves *) - apply (ga_kappa Γ Δ (v2t ec) nil (mapOptionTree (flatten_type ○ unlev) (take_lev (ec::nil) succ)) _ _). - apply (Prelude_error "found Esc at depth >0 indicating 3-level code; only two-level code is currently supported"). + apply (Prelude_error "found unskolemized Esc rule; this shouldn't happen"). destruct case_RNote. simpl. @@ -887,6 +1057,7 @@ Section HaskFlattener. destruct case_RCast. simpl. destruct lev as [|ec lev]; simpl; [ apply nd_rule; apply RCast; auto | idtac ]. + simpl. apply flatten_coercion; auto. apply (Prelude_error "RCast at level >0; casting inside of code brackets is currently not supported"). @@ -934,22 +1105,51 @@ Section HaskFlattener. repeat take_simplify. simpl. + set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) Σ₁)) as Σ₁'. + set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) Σ₂)) as Σ₂'. + set (mapOptionTree flatten_leveled_type (drop_lev (ec :: lev) Σ₁)) as Σ₁''. + set (mapOptionTree flatten_leveled_type (drop_lev (ec :: lev) Σ₂)) as Σ₂''. + eapply nd_comp. eapply nd_prod; [ idtac | apply nd_id ]. eapply boost. - apply ga_second. + apply (ga_first _ _ _ _ _ _ Σ₂'). - eapply nd_comp. - eapply nd_prod. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ]. + apply nd_prod. apply nd_id. + eapply nd_comp; [ eapply nd_rule; eapply RArrange; eapply RCanL | idtac ]. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RExch (* okay *)]. + apply precompose. + + destruct case_RWhere. + simpl. + destruct lev as [|ec lev]; simpl; [ apply nd_rule; apply RWhere; auto | idtac ]. + repeat take_simplify. + repeat drop_simplify. + simpl. + + set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) Σ₁)) as Σ₁'. + set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) Σ₂)) as Σ₂'. + set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) Σ₃)) as Σ₃'. + set (mapOptionTree flatten_leveled_type (drop_lev (ec :: lev) Σ₁)) as Σ₁''. + set (mapOptionTree flatten_leveled_type (drop_lev (ec :: lev) Σ₂)) as Σ₂''. + set (mapOptionTree flatten_leveled_type (drop_lev (ec :: lev) Σ₃)) as Σ₃''. + eapply nd_comp. - eapply nd_rule. - eapply RArrange. - apply RCanR. - eapply precompose. + eapply nd_prod; [ eapply nd_id | idtac ]. + eapply (first_nd _ _ _ _ _ _ Σ₃'). + eapply nd_comp. + eapply nd_prod; [ eapply nd_id | idtac ]. + eapply (second_nd _ _ _ _ _ _ Σ₁'). + eapply nd_comp; [ idtac | eapply nd_rule; eapply RWhere ]. + apply nd_prod; [ idtac | apply nd_id ]. + eapply nd_comp; [ idtac | eapply precompose' ]. apply nd_rule. - apply RLet. + apply RArrange. + apply RLeft. + apply RCanL. destruct case_RVoid. simpl. @@ -1020,14 +1220,145 @@ Section HaskFlattener. destruct case_RLetRec. rename t into lev. + simpl. destruct lev; simpl. + replace (getjlev (y @@@ nil)) with (nil: (HaskLevel Γ)). + replace (mapOptionTree flatten_leveled_type (y @@@ nil)) + with ((mapOptionTree flatten_type y) @@@ nil). + unfold flatten_leveled_type at 2. + simpl. + unfold flatten_leveled_type at 3. simpl. - apply (Prelude_error "LetRec not supported (FIXME)"). + apply nd_rule. + set (@RLetRec Γ Δ (mapOptionTree flatten_leveled_type lri) (flatten_type x) (mapOptionTree flatten_type y) nil) as q. + simpl in q. + apply q. + induction y; try destruct a; auto. + simpl. + rewrite IHy1. + rewrite IHy2. + reflexivity. + induction y; try destruct a; auto. + simpl. + rewrite <- IHy1. + rewrite <- IHy2. + reflexivity. + apply (Prelude_error "LetRec not supported inside brackets yet (FIXME)"). destruct case_RCase. simpl. apply (Prelude_error "Case not supported (BIG FIXME)"). + + destruct case_SBrak. + simpl. + destruct lev. + drop_simplify. + set (drop_lev (ec :: nil) (take_arg_types_as_tree t @@@ (ec :: nil))) as empty_tree. + take_simplify. + rewrite take_lemma'. + simpl. + rewrite mapOptionTree_compose. + rewrite mapOptionTree_compose. + rewrite unlev_relev. + rewrite <- mapOptionTree_compose. + unfold flatten_leveled_type at 4. + simpl. + 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. + unfold empty_tree. + eapply nd_comp; [ eapply nd_rule; eapply RArrange; eapply RLeft; apply tree_of_nothing | idtac ]. + eapply nd_comp; [ eapply nd_rule; eapply RArrange; eapply RCanR | idtac ]. + refine (ga_unkappa Γ Δ (v2t ec) nil _ _ _ _ ;; _). + eapply nd_comp; [ idtac | eapply arrange_brak ]. + unfold succ_host. + unfold succ_guest. + eapply nd_rule. + eapply RArrange. + apply RExch. + apply (Prelude_error "found Brak at depth >0 indicating 3-level code; only two-level code is currently supported"). + + destruct case_SEsc. + simpl. + destruct lev. + simpl. + unfold flatten_leveled_type at 2. + simpl. + rewrite krunk. + rewrite mapOptionTree_compose. + take_simplify. + drop_simplify. + simpl. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RLeft; apply tree_of_nothing' ]. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanR ]. + simpl. + rewrite take_lemma'. + rewrite unlev_relev. + rewrite <- mapOptionTree_compose. + eapply nd_comp; [ apply (arrange_esc _ _ ec) | idtac ]. + + set (decide_tree_empty (take_lev (ec :: nil) succ)) as q'. + destruct q'. + destruct s. + rewrite e. + 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. + + eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RuCanR ]. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RuCanR ]. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RCanL ]. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ]. + eapply nd_comp; [ apply nd_llecnac | idtac ]. + apply nd_prod; [ idtac | eapply boost ]. + induction x. + apply ga_id. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanL ]. + simpl. + apply ga_join. + apply IHx1. + apply IHx2. + simpl. + apply postcompose. + + refine ( _ ;; (boost _ _ _ _ _ (postcompose _ _ _ _ _ _ _ _))). + apply ga_cancell. + apply firstify. + + induction x. + destruct a; simpl. + apply ga_id. + simpl. + refine ( _ ;; (boost _ _ _ _ _ (postcompose _ _ _ _ _ _ _ _))). + apply ga_cancell. + refine ( _ ;; (boost _ _ _ _ _ (postcompose _ _ _ _ _ _ _ _))). + eapply firstify. + apply IHx1. + apply secondify. + apply IHx2. + + (* environment has non-empty leaves *) + apply (Prelude_error "ga_kappa not supported yet (BIG FIXME)"). + + (* nesting too deep *) + 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 *)