X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskFlattener.v;h=59636bf87830880d016ab7372c6f2629a4cd453f;hp=a5f42618b89ea2de829e7cb8e842ee82870c7510;hb=3a2879d925d4e13e9c89bc768df111684d2b4a59;hpb=bebffa435dbc5afd126f6972fbf220977455854d diff --git a/src/HaskFlattener.v b/src/HaskFlattener.v index a5f4261..59636bf 100644 --- a/src/HaskFlattener.v +++ b/src/HaskFlattener.v @@ -9,6 +9,7 @@ Generalizable All Variables. Require Import Preamble. Require Import General. Require Import NaturalDeduction. +Require Import NaturalDeductionContext. Require Import Coq.Strings.String. Require Import Coq.Lists.List. @@ -45,52 +46,6 @@ Set Printing Width 130. *) Section HaskFlattener. - Definition getlev {Γ}{κ}(lht:LeveledHaskType Γ κ) : HaskLevel Γ := - match lht with t @@ l => l end. - - Definition arrange : - forall {T} (Σ:Tree ??T) (f:T -> bool), - Arrange Σ (dropT (mkFlags (liftBoolFunc false f) Σ),,( (dropT (mkFlags (liftBoolFunc false (bnot ○ f)) Σ)))). - intros. - induction Σ. - simpl. - destruct a. - simpl. - destruct (f t); simpl. - apply RuCanL. - apply RuCanR. - simpl. - apply RuCanL. - simpl in *. - eapply RComp; [ idtac | apply arrangeSwapMiddle ]. - eapply RComp. - eapply RLeft. - apply IHΣ2. - eapply RRight. - apply IHΣ1. - Defined. - - Definition arrange' : - forall {T} (Σ:Tree ??T) (f:T -> bool), - Arrange (dropT (mkFlags (liftBoolFunc false f) Σ),,( (dropT (mkFlags (liftBoolFunc false (bnot ○ f)) Σ)))) Σ. - intros. - induction Σ. - simpl. - destruct a. - simpl. - destruct (f t); simpl. - apply RCanL. - apply RCanR. - simpl. - apply RCanL. - simpl in *. - eapply RComp; [ apply arrangeSwapMiddle | idtac ]. - eapply RComp. - eapply RLeft. - apply IHΣ2. - eapply RRight. - apply IHΣ1. - Defined. Ltac eqd_dec_refl' := match goal with @@ -177,29 +132,11 @@ Section HaskFlattener. 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)] ] => @@ -224,9 +161,6 @@ Section HaskFlattener. (*******************************************************************************) - Context (hetmet_flatten : WeakExprVar). - Context (hetmet_unflatten : WeakExprVar). - Context (hetmet_id : WeakExprVar). Context {unitTy : forall TV, RawHaskType TV ECKind -> RawHaskType TV ★ }. Context {prodTy : forall TV, RawHaskType TV ECKind -> RawHaskType TV ★ -> RawHaskType TV ★ -> RawHaskType TV ★ }. Context {gaTy : forall TV, RawHaskType TV ECKind -> RawHaskType TV ★ -> RawHaskType TV ★ -> RawHaskType TV ★ }. @@ -308,71 +242,52 @@ Section HaskFlattener. Axiom globals_do_not_have_code_types : forall (Γ:TypeEnv) (g:Global Γ) v, flatten_type (g v) = g v. - (* This tries to assign a single level to the entire succedent of a judgment. If the succedent has types from different - * levels (should not happen) it just picks one; if the succedent has no non-None leaves (also should not happen) it - * picks nil *) - Definition getΓ (j:Judg) := match j with Γ > _ > _ |- _ => Γ end. - Definition getSuc (j:Judg) : Tree ??(LeveledHaskType (getΓ j) ★) := - match j as J return Tree ??(LeveledHaskType (getΓ J) ★) with Γ > _ > _ |- s => s end. - Fixpoint getjlev {Γ}(tt:Tree ??(LeveledHaskType Γ ★)) : HaskLevel Γ := - match tt with - | T_Leaf None => nil - | T_Leaf (Some (_ @@ lev)) => lev - | T_Branch b1 b2 => - match getjlev b1 with - | nil => getjlev b2 - | lev => lev - end - end. - (* "n" is the maximum depth remaining AFTER flattening *) Definition flatten_judgment (j:Judg) := match j as J return Judg with - Γ > Δ > ant |- suc => - match getjlev suc with - | nil => Γ > Δ > mapOptionTree flatten_leveled_type ant - |- mapOptionTree flatten_leveled_type suc - - | (ec::lev') => Γ > Δ > mapOptionTree flatten_leveled_type (drop_lev (ec::lev') ant) - |- [ga_mk (v2t ec) - (mapOptionTree (flatten_type ○ unlev) (take_lev (ec::lev') ant)) - (mapOptionTree (flatten_type ○ unlev) suc ) - @@ nil] (* we know the level of all of suc *) - end + | Γ > Δ > ant |- suc @ nil => Γ > Δ > mapOptionTree flatten_leveled_type ant + |- mapOptionTree flatten_type suc @ nil + | Γ > Δ > ant |- suc @ (ec::lev') => Γ > Δ > mapOptionTree flatten_leveled_type (drop_lev (ec::lev') ant) + |- [ga_mk (v2t ec) + (mapOptionTree (flatten_type ○ unlev) (take_lev (ec::lev') ant)) + (mapOptionTree flatten_type suc ) + ] @ nil end. Class garrow := - { ga_id : ∀ Γ Δ ec l a , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec a a @@ l] ] - ; ga_cancelr : ∀ Γ Δ ec l a , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec (a,,[]) a @@ l] ] - ; ga_cancell : ∀ Γ Δ ec l a , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec ([],,a) a @@ l] ] - ; ga_uncancelr : ∀ Γ Δ ec l a , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec a (a,,[]) @@ l] ] - ; ga_uncancell : ∀ Γ Δ ec l a , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec a ([],,a) @@ l] ] - ; ga_assoc : ∀ Γ Δ ec l a b c, ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec ((a,,b),,c) (a,,(b,,c)) @@ l] ] - ; ga_unassoc : ∀ Γ Δ ec l a b c, ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec (a,,(b,,c)) ((a,,b),,c) @@ l] ] - ; ga_swap : ∀ Γ Δ ec l a b , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec (a,,b) (b,,a) @@ l] ] - ; ga_drop : ∀ Γ Δ ec l a , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec a [] @@ l] ] - ; ga_copy : ∀ Γ Δ ec l a , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec a (a,,a) @@ l] ] - ; ga_first : ∀ Γ Δ ec l a b x, ND Rule [] [Γ > Δ > [@ga_mk Γ ec a b @@ l] |- [@ga_mk Γ ec (a,,x) (b,,x) @@ l] ] - ; ga_second : ∀ Γ Δ ec l a b x, ND Rule [] [Γ > Δ > [@ga_mk Γ ec a b @@ l] |- [@ga_mk Γ ec (x,,a) (x,,b) @@ l] ] - ; ga_lit : ∀ Γ Δ ec l lit , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec [] [literalType lit] @@ l] ] - ; ga_curry : ∀ Γ Δ ec l a b c, ND Rule [] [Γ > Δ > [@ga_mk Γ ec (a,,[b]) [c] @@ l] |- [@ga_mk Γ ec a [b ---> c] @@ l] ] - ; ga_comp : ∀ Γ Δ ec l a b c, ND Rule [] [Γ > Δ > [@ga_mk Γ ec a b @@ l],,[@ga_mk Γ ec b c @@ l] |- [@ga_mk Γ ec a c @@ l] ] + { ga_id : ∀ Γ Δ ec l a , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec a a ]@l ] + ; ga_cancelr : ∀ Γ Δ ec l a , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec (a,,[]) a ]@l ] + ; ga_cancell : ∀ Γ Δ ec l a , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec ([],,a) a ]@l ] + ; ga_uncancelr : ∀ Γ Δ ec l a , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec a (a,,[]) ]@l ] + ; ga_uncancell : ∀ Γ Δ ec l a , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec a ([],,a) ]@l ] + ; ga_assoc : ∀ Γ Δ ec l a b c, ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec ((a,,b),,c) (a,,(b,,c)) ]@l ] + ; ga_unassoc : ∀ Γ Δ ec l a b c, ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec (a,,(b,,c)) ((a,,b),,c) ]@l ] + ; ga_swap : ∀ Γ Δ ec l a b , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec (a,,b) (b,,a) ]@l ] + ; ga_drop : ∀ Γ Δ ec l a , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec a [] ]@l ] + ; ga_copy : ∀ Γ Δ ec l a , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec a (a,,a) ]@l ] + ; ga_first : ∀ Γ Δ ec l a b x, ND Rule [] [Γ > Δ > [@ga_mk Γ ec a b @@l] |- [@ga_mk Γ ec (a,,x) (b,,x) ]@l ] + ; ga_second : ∀ Γ Δ ec l a b x, ND Rule [] [Γ > Δ > [@ga_mk Γ ec a b @@l] |- [@ga_mk Γ ec (x,,a) (x,,b) ]@l ] + ; ga_lit : ∀ Γ Δ ec l lit , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec [] [literalType lit] ]@l ] + ; ga_curry : ∀ Γ Δ ec l a b c, ND Rule [] [Γ > Δ > [@ga_mk Γ ec (a,,[b]) [c] @@ l] |- [@ga_mk Γ ec a [b ---> c] ]@ l ] + ; ga_loopl : ∀ Γ Δ ec l x y z, ND Rule [] [Γ > Δ > [@ga_mk Γ ec (z,,x) (z,,y) @@ l] |- [@ga_mk Γ ec x y ]@ l ] + ; ga_loopr : ∀ Γ Δ ec l x y z, ND Rule [] [Γ > Δ > [@ga_mk Γ ec (x,,z) (y,,z) @@ l] |- [@ga_mk Γ ec x y ]@ l ] + ; ga_comp : ∀ Γ Δ ec l a b c, ND Rule [] [Γ > Δ > [@ga_mk Γ ec a b @@ l],,[@ga_mk Γ ec b c @@ l] |- [@ga_mk Γ ec a c ]@l ] ; ga_apply : ∀ Γ Δ ec l a a' b c, - ND Rule [] [Γ > Δ > [@ga_mk Γ ec a [b ---> c] @@ l],,[@ga_mk Γ ec a' [b] @@ l] |- [@ga_mk Γ ec (a,,a') [c] @@ l] ] + ND Rule [] [Γ > Δ > [@ga_mk Γ ec a [b ---> c] @@ l],,[@ga_mk Γ ec a' [b] @@ l] |- [@ga_mk Γ ec (a,,a') [c] ]@l ] ; ga_kappa : ∀ Γ Δ ec l a b Σ, ND Rule - [Γ > Δ > Σ,,[@ga_mk Γ ec [] a @@ l] |- [@ga_mk Γ ec [] b @@ l] ] - [Γ > Δ > Σ |- [@ga_mk Γ ec a b @@ l] ] + [Γ > Δ > Σ,,[@ga_mk Γ ec [] a @@ l] |- [@ga_mk Γ ec [] b ]@l ] + [Γ > Δ > Σ |- [@ga_mk Γ ec a b ]@l ] }. Context `(gar:garrow). Notation "a ~~~~> b" := (@ga_mk _ _ a b) (at level 20). Definition boost : forall Γ Δ ant x y {lev}, - ND Rule [] [ Γ > Δ > [x@@lev] |- [y@@lev] ] -> - ND Rule [ Γ > Δ > ant |- [x@@lev] ] [ Γ > Δ > ant |- [y@@lev] ]. + 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 ACanR ]. + eapply nd_comp; [ idtac | apply RLet ]. eapply nd_comp; [ apply nd_rlecnac | idtac ]. apply nd_prod. apply nd_id. @@ -380,142 +295,118 @@ 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 AuCanR. + 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] ]. + [ Γ > Δ > 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 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; apply RExch ]. - - apply nd_rule. - apply RLet. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AExch ]. + 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 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 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 ALeft; eapply AExch ]. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AuAssoc ]. + apply precompose. + Defined. - Definition firstify : ∀ Γ Δ ec lev a b c Σ, - ND Rule [] [ Γ > Δ > Σ |- [@ga_mk Γ ec a b @@ lev] ] -> - ND Rule [] [ Γ > Δ > Σ |- [@ga_mk Γ ec (a,,c) (b,,c) @@ lev] ]. + 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 RArrange; eapply RCanL ]. - eapply nd_comp; [ idtac | eapply nd_rule; apply RLet ]. - eapply nd_comp; [ apply nd_llecnac | idtac ]. + eapply nd_comp; [ idtac | eapply RLet ]. + eapply nd_comp; [ apply nd_rlecnac | idtac ]. apply nd_prod. - apply X. - eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RuCanL ]. - apply ga_first. + apply nd_id. + apply ga_comp. 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 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 nd_rule; apply RLet ]. - eapply nd_comp; [ apply nd_llecnac | idtac ]. - apply nd_prod. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ACanL ]. + eapply nd_comp; [ idtac | eapply postcompose_ ]. apply X. - eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RuCanL ]. - apply ga_second. Defined. - Lemma ga_unkappa : ∀ Γ Δ ec l z a b Σ, - ND Rule - [Γ > Δ > Σ |- [@ga_mk Γ ec a b @@ l] ] - [Γ > Δ > Σ,,[@ga_mk Γ ec z a @@ l] |- [@ga_mk Γ ec z b @@ l] ]. + 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. - set (ga_comp Γ Δ ec l z a b) as q. - - set (@RLet Γ Δ) as q'. - set (@RLet Γ Δ [@ga_mk _ ec z a @@ l] Σ (@ga_mk _ ec z b) (@ga_mk _ ec a b) l) as q''. - eapply nd_comp. - Focus 2. - eapply nd_rule. - eapply RArrange. - apply RExch. - - eapply nd_comp. - Focus 2. - eapply nd_rule. - apply q''. - - idtac. - clear q'' q'. - eapply nd_comp. - apply nd_rlecnac. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ACanR ]. + eapply nd_comp; [ idtac | apply RLet ]. + eapply nd_comp; [ apply nd_rlecnac | idtac ]. apply nd_prod. apply nd_id. - apply q. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AuCanR ]. + apply ga_first. Defined. - 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] ]. + Definition firstify : ∀ Γ Δ ec lev a b c Σ, + 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 RLet ]. - eapply nd_comp; [ apply nd_llecnac | idtac ]. - apply nd_prod. - apply ga_first. + eapply nd_comp. + apply X. + apply first_nd. + Defined. - eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ]. - eapply nd_comp; [ apply nd_llecnac | idtac ]. + 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 ACanR ]. + eapply nd_comp; [ idtac | apply RLet ]. + eapply nd_comp; [ apply nd_rlecnac | idtac ]. apply nd_prod. - apply postcompose. - apply ga_uncancell. - apply precompose. + apply nd_id. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AuCanR ]. + apply ga_second. Defined. - Lemma ga_kappa' : ∀ Γ Δ ec l a b Σ x, - ND Rule - [Γ > Δ > Σ,,[@ga_mk Γ ec [] a @@ l] |- [@ga_mk Γ ec x b @@ l] ] - [Γ > Δ > Σ |- [@ga_mk Γ ec (a,,x) b @@ l] ]. - apply (Prelude_error "ga_kappa not supported yet (BIG FIXME)"). + 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. + eapply nd_comp. + apply X. + apply second_nd. Defined. + 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 AExch ]. + eapply nd_comp; [ idtac | eapply RLet ]. + eapply nd_comp; [ apply nd_llecnac | idtac ]. + apply nd_prod. + apply ga_first. + + eapply nd_comp; [ idtac | 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 AExch ]. + apply precompose. + Defined. + (* useful for cutting down on the pretty-printed noise Notation "` x" := (take_lev _ x) (at level 20). @@ -526,50 +417,50 @@ Section HaskFlattener. forall Γ (Δ:CoercionEnv Γ) (ec:HaskTyVar Γ ECKind) (lev:HaskLevel Γ) (ant1 ant2:Tree ??(LeveledHaskType Γ ★)) (r:Arrange ant1 ant2), ND Rule [] [Γ > Δ > [] |- [@ga_mk _ (v2t ec) (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) ant2)) - (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) ant1)) @@ nil] ]. + (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) ant1)) ]@nil ]. intros Γ Δ ec lev. refine (fix flatten ant1 ant2 (r:Arrange ant1 ant2): ND Rule [] [Γ > Δ > [] |- [@ga_mk _ (v2t ec) (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) ant2)) - (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) ant1)) @@ nil]] := + (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) ant1)) ]@nil] := match r as R in Arrange A B return ND Rule [] [Γ > Δ > [] |- [@ga_mk _ (v2t ec) (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) B)) - (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) A)) @@ nil]] + (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 _ _ _ _ _ - | RuCanR a => let case_RuCanR := tt in ga_cancelr _ _ _ _ _ - | RAssoc a b c => let case_RAssoc := tt in ga_assoc _ _ _ _ _ _ _ - | RCossa a b c => let case_RCossa := tt in ga_unassoc _ _ _ _ _ _ _ - | RExch a b => let case_RExch := tt in ga_swap _ _ _ _ _ _ - | RWeak a => let case_RWeak := tt in ga_drop _ _ _ _ _ - | RCont a => let case_RCont := tt in ga_copy _ _ _ _ _ - | RLeft a b c r' => let case_RLeft := tt in flatten _ _ r' ;; boost _ _ _ _ _ (ga_second _ _ _ _ _ _ _) - | RRight a b c r' => let case_RRight := tt in flatten _ _ r' ;; boost _ _ _ _ _ (ga_first _ _ _ _ _ _ _) - | RComp c b a r1 r2 => let case_RComp := tt in (fun r1' r2' => _) (flatten _ _ r1) (flatten _ _ r2) + | AId a => let case_AId := tt in ga_id _ _ _ _ _ + | ACanL a => let case_ACanL := tt in ga_uncancell _ _ _ _ _ + | ACanR a => let case_ACanR := tt in ga_uncancelr _ _ _ _ _ + | AuCanL a => let case_AuCanL := tt in ga_cancell _ _ _ _ _ + | AuCanR a => let case_AuCanR := tt in ga_cancelr _ _ _ _ _ + | AAssoc a b c => let case_AAssoc := tt in ga_assoc _ _ _ _ _ _ _ + | AuAssoc a b c => let case_AuAssoc := tt in ga_unassoc _ _ _ _ _ _ _ + | AExch a b => let case_AExch := tt in ga_swap _ _ _ _ _ _ + | AWeak a => let case_AWeak := tt in ga_drop _ _ _ _ _ + | ACont a => let case_ACont := tt in ga_copy _ _ _ _ _ + | ALeft a b c r' => let case_ALeft := tt in flatten _ _ r' ;; boost _ _ _ _ _ (ga_second _ _ _ _ _ _ _) + | ARight a b c r' => let case_ARight := tt in flatten _ _ r' ;; boost _ _ _ _ _ (ga_first _ _ _ _ _ _ _) + | AComp c b a r1 r2 => let case_AComp := tt in (fun r1' r2' => _) (flatten _ _ r1) (flatten _ _ r2) end); clear flatten; repeat take_simplify; repeat drop_simplify; intros. - destruct case_RComp. + destruct case_AComp. set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) a)) as a' in *. set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) b)) as b' in *. 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')) ]. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply ACanL ]. + eapply nd_comp; [ idtac | apply + (@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 AuCanR ]. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply ACanL ]. + eapply nd_comp; [ idtac | apply RLet ]. eapply nd_comp; [ apply nd_llecnac | idtac ]. eapply nd_prod. apply r1'. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AExch ]. apply ga_comp. Defined. @@ -580,11 +471,11 @@ Section HaskFlattener. [Γ > Δ > mapOptionTree (flatten_leveled_type ) (drop_lev n ant1) |- [@ga_mk _ (v2t ec) (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) ant1)) - (mapOptionTree (flatten_type ○ unlev) succ) @@ nil]] + (mapOptionTree (flatten_type ) succ) ]@nil] [Γ > Δ > mapOptionTree (flatten_leveled_type ) (drop_lev n ant2) |- [@ga_mk _ (v2t ec) (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) ant2)) - (mapOptionTree (flatten_type ○ unlev) succ) @@ nil]]. + (mapOptionTree (flatten_type ) succ) ]@nil]. intros. refine ( _ ;; (boost _ _ _ _ _ (postcompose _ _ _ _ _ _ _ (flatten_arrangement' Γ Δ ec lev ant1 ant2 r)))). apply nd_rule. @@ -593,87 +484,86 @@ 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 _ - | RuCanR a => let case_RuCanR := tt in RuCanR _ - | RAssoc a b c => let case_RAssoc := tt in RAssoc _ _ _ - | RCossa a b c => let case_RCossa := tt in RCossa _ _ _ - | RExch a b => let case_RExch := tt in RExch _ _ - | RWeak a => let case_RWeak := tt in RWeak _ - | RCont a => let case_RCont := tt in RCont _ - | RLeft a b c r' => let case_RLeft := tt in RLeft _ (flatten _ _ r') - | RRight a b c r' => let case_RRight := tt in RRight _ (flatten _ _ r') - | RComp a b c r1 r2 => let case_RComp := tt in RComp (flatten _ _ r1) (flatten _ _ r2) + | AId a => let case_AId := tt in AId _ + | ACanL a => let case_ACanL := tt in ACanL _ + | ACanR a => let case_ACanR := tt in ACanR _ + | AuCanL a => let case_AuCanL := tt in AuCanL _ + | AuCanR a => let case_AuCanR := tt in AuCanR _ + | AAssoc a b c => let case_AAssoc := tt in AAssoc _ _ _ + | AuAssoc a b c => let case_AuAssoc := tt in AuAssoc _ _ _ + | AExch a b => let case_AExch := tt in AExch _ _ + | AWeak a => let case_AWeak := tt in AWeak _ + | ACont a => let case_ACont := tt in ACont _ + | ALeft a b c r' => let case_ALeft := tt in ALeft _ (flatten _ _ r') + | ARight a b c r' => let case_ARight := tt in ARight _ (flatten _ _ r') + | AComp a b c r1 r2 => let case_AComp := tt in AComp (flatten _ _ r1) (flatten _ _ r2) end) ant1 ant2 r); clear flatten; repeat take_simplify; repeat drop_simplify; intros. Defined. Definition flatten_arrangement'' : - forall Γ Δ ant1 ant2 succ (r:Arrange ant1 ant2), - ND Rule (mapOptionTree (flatten_judgment ) [Γ > Δ > ant1 |- succ]) - (mapOptionTree (flatten_judgment ) [Γ > Δ > ant2 |- succ]). + forall Γ Δ ant1 ant2 succ l (r:Arrange ant1 ant2), + ND Rule (mapOptionTree (flatten_judgment ) [Γ > Δ > ant1 |- succ @ l]) + (mapOptionTree (flatten_judgment ) [Γ > Δ > ant2 |- succ @ l]). intros. simpl. - set (getjlev succ) as succ_lev. - assert (succ_lev=getjlev succ). - reflexivity. - - destruct succ_lev. + destruct l. 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 RWeak. - apply RCont. - apply RLeft; auto. - apply RRight; auto. - eapply RComp; [ apply IHr1 | apply IHr2 ]. + apply AId. + apply ACanL. + apply ACanR. + apply AuCanL. + apply AuCanR. + apply AAssoc. + apply AuAssoc. + apply AExch. (* TO DO: check for all-leaf trees here *) + apply AWeak. + apply ACont. + apply ALeft; auto. + apply ARight; auto. + eapply AComp; [ apply IHr1 | apply IHr2 ]. apply flatten_arrangement. apply r. Defined. Definition ga_join Γ Δ Σ₁ Σ₂ a b ec : - ND Rule [] [Γ > Δ > Σ₁ |- [@ga_mk _ ec [] a @@ nil]] -> - ND Rule [] [Γ > Δ > Σ₂ |- [@ga_mk _ ec [] b @@ nil]] -> - ND Rule [] [Γ > Δ > Σ₁,,Σ₂ |- [@ga_mk _ ec [] (a,,b) @@ nil]]. + ND Rule [] [Γ > Δ > Σ₁ |- [@ga_mk _ ec [] a ]@nil] -> + ND Rule [] [Γ > Δ > Σ₂ |- [@ga_mk _ ec [] b ]@nil] -> + ND Rule [] [Γ > Δ > Σ₁,,Σ₂ |- [@ga_mk _ ec [] (a,,b) ]@nil]. intro pfa. intro pfb. apply secondify with (c:=a) in pfb. - eapply nd_comp. - Focus 2. - eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ]. + apply firstify with (c:=[]) in pfa. + eapply nd_comp; [ idtac | 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 RArrange; eapply RCanL ]. - apply precompose'. + + eapply nd_comp; [ idtac | eapply RLet ]. + eapply nd_comp; [ apply nd_llecnac | idtac ]. + apply nd_prod. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ACanL ]. + eapply nd_comp; [ idtac | eapply postcompose_ ]. apply ga_uncancelr. - apply nd_id. + + eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AExch ]. + 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] |- [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] + [Γ > Δ > mapOptionTree (flatten_leveled_type ) succ |- [t]@nil]. + intros. unfold drop_lev. - set (@arrange' _ succ (levelMatch (ec::nil))) as q. + set (@arrangeUnPartition _ succ (levelMatch (ec::nil))) as q. set (arrangeMap _ _ flatten_leveled_type q) as y. eapply nd_comp. Focus 2. @@ -682,9 +572,10 @@ Section HaskFlattener. apply y. idtac. clear y q. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AExch ]. simpl. eapply nd_comp; [ apply nd_llecnac | idtac ]. - eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ]. + eapply nd_comp; [ idtac | eapply RLet ]. apply nd_prod. Focus 2. apply nd_id. @@ -722,66 +613,14 @@ 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 |- [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] |- [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. - set (@arrange _ succ (levelMatch (ec::nil))) as q. + set (@arrangePartition _ succ (levelMatch (ec::nil))) as q. set (@drop_lev Γ (ec::nil) succ) as q'. assert (@drop_lev Γ (ec::nil) succ=q') as H. reflexivity. @@ -801,27 +640,27 @@ Section HaskFlattener. destruct s. simpl. - eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RExch ]. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply AExch ]. set (fun z z' => @RLet Γ Δ z (mapOptionTree flatten_leveled_type q') t z' nil) as q''. - eapply nd_comp; [ idtac | eapply nd_rule; apply q'' ]. + eapply nd_comp; [ idtac | 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 AComp; [ idtac | apply ACanR ]. + apply ALeft. + apply (@arrangeCancelEmptyTree _ _ _ _ e). + eapply nd_comp. eapply nd_rule. eapply (@RVar Γ Δ t nil). apply nd_rule. apply RArrange. - eapply RComp. - apply RuCanL. - apply RRight. - apply RWeak. + eapply AComp. + apply AuCanR. + apply ALeft. + apply AWeak. (* eapply decide_tree_empty. @@ -845,25 +684,19 @@ Section HaskFlattener. simpl. apply nd_rule. apply RArrange. - apply RLeft. - apply RWeak. + apply ALeft. + apply AWeak. simpl. apply nd_rule. unfold take_lev. simpl. apply RArrange. - apply RLeft. - apply RWeak. + apply ALeft. + apply AWeak. apply (Prelude_error "escapifying code with multi-leaf antecedents is not supported"). *) Defined. - Lemma mapOptionTree_distributes - : forall T R (a b:Tree ??T) (f:T->R), - mapOptionTree f (a,,b) = (mapOptionTree f a),,(mapOptionTree f b). - reflexivity. - Qed. - Lemma unlev_relev : forall {Γ}(t:Tree ??(HaskType Γ ★)) lev, mapOptionTree unlev (t @@@ lev) = t. intros. induction t. @@ -873,52 +706,45 @@ Section HaskFlattener. reflexivity. Qed. - Lemma tree_of_nothing : forall Γ ec t a, - Arrange (a,,mapOptionTree flatten_leveled_type (drop_lev(Γ:=Γ) (ec :: nil) (t @@@ (ec :: nil)))) a. + 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 a0. + induction t; try destruct o; try destruct a. simpl. drop_simplify. simpl. - apply RCanR. + apply AId. simpl. - apply RCanR. + apply AId. + eapply AComp; [ idtac | apply ACanL ]. + eapply AComp; [ idtac | eapply ALeft; apply IHt2 ]. Opaque drop_lev. simpl. Transparent drop_lev. + idtac. drop_simplify. - simpl. - eapply RComp. - eapply RComp. - eapply RAssoc. - eapply RRight. + apply ARight. apply IHt1. - apply IHt2. Defined. - Lemma tree_of_nothing' : forall Γ ec t a, - Arrange a (a,,mapOptionTree flatten_leveled_type (drop_lev(Γ:=Γ) (ec :: nil) (t @@@ (ec :: nil)))). + 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 a0. + induction t; try destruct o; try destruct a. simpl. drop_simplify. simpl. - apply RuCanR. + apply AId. simpl. - apply RuCanR. + apply AId. + eapply AComp; [ apply AuCanL | idtac ]. + eapply AComp; [ eapply ARight; apply IHt1 | idtac ]. Opaque drop_lev. simpl. Transparent drop_lev. + idtac. drop_simplify. - simpl. - eapply RComp. - Focus 2. - eapply RComp. - Focus 2. - eapply RCossa. - Focus 2. - eapply RRight. - apply IHt1. + apply ALeft. apply IHt2. Defined. @@ -948,16 +774,28 @@ Section HaskFlattener. (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 : + Lemma drop_to_nothing : forall (Γ:TypeEnv) Σ (lev:HaskLevel Γ), + drop_lev lev (Σ @@@ lev) = mapTree (fun _ => None) (mapTree (fun _ => tt) Σ). + intros. + induction Σ. + destruct a; simpl. + drop_simplify. + auto. + drop_simplify. + auto. + simpl. + rewrite <- IHΣ1. + rewrite <- IHΣ2. + reflexivity. + Qed. + + Definition flatten_skolemized_proof : forall {h}{c}, ND SRule h c -> ND Rule (mapOptionTree (flatten_judgment ) h) (mapOptionTree (flatten_judgment ) c). @@ -976,7 +814,7 @@ Section HaskFlattener. destruct case_SFlat. refine (match r as R in Rule H C with - | RArrange Γ Δ a b x d => let case_RArrange := tt in _ + | RArrange Γ Δ a b x l d => let case_RArrange := tt in _ | RNote Γ Δ Σ τ l n => let case_RNote := tt in _ | RLit Γ Δ l _ => let case_RLit := tt in _ | RVar Γ Δ σ lev => let case_RVar := tt in _ @@ -988,9 +826,10 @@ Section HaskFlattener. | RAppCo Γ Δ Σ κ σ₁ σ₂ γ σ lev => let case_RAppCo := tt in _ | RAbsCo Γ Δ Σ κ σ σ₁ σ₂ lev => let case_RAbsCo := tt in _ | RApp Γ Δ Σ₁ Σ₂ tx te lev => let case_RApp := tt in _ - | RLet Γ Δ Σ₁ Σ₂ σ₁ σ₂ lev => let case_RLet := tt in _ - | RJoin Γ p lri m x q => let case_RJoin := tt in _ - | RVoid _ _ => let case_RVoid := tt in _ + | RCut Γ Δ Σ Σ₁ Σ₁₂ Σ₂ Σ₃ l => let case_RCut := tt in _ + | RLeft Γ Δ Σ₁ Σ₂ Σ l => let case_RLeft := tt in _ + | RRight Γ Δ Σ₁ Σ₂ Σ l => let case_RRight := tt in _ + | RVoid _ _ l => let case_RVoid := tt in _ | RBrak Γ Δ t ec succ lev => let case_RBrak := tt in _ | REsc Γ Δ t ec succ lev => let case_REsc := tt in _ | RCase Γ Δ lev tc Σ avars tbranches alts => let case_RCase := tt in _ @@ -998,7 +837,7 @@ Section HaskFlattener. end); clear X h c. destruct case_RArrange. - apply (flatten_arrangement'' Γ Δ a b x d). + apply (flatten_arrangement'' Γ Δ a b x _ d). destruct case_RBrak. apply (Prelude_error "found unskolemized Brak rule; this shouldn't happen"). @@ -1031,7 +870,6 @@ Section HaskFlattener. Transparent flatten_judgment. idtac. unfold flatten_judgment. - unfold getjlev. destruct lev. apply nd_rule. apply RVar. repeat drop_simplify. @@ -1044,6 +882,7 @@ Section HaskFlattener. rename l into g. rename σ into l. destruct l as [|ec lev]; simpl. + (* destruct (eqd_dec (g:CoreVar) (hetmet_flatten:CoreVar)). set (flatten_type (g wev)) as t. set (RGlobal _ Δ nil (mkGlobal Γ t hetmet_id)) as q. @@ -1058,6 +897,7 @@ Section HaskFlattener. apply nd_rule. apply q. apply INil. + *) unfold flatten_leveled_type. simpl. apply nd_rule; rewrite globals_do_not_have_code_types. apply RGlobal. @@ -1074,7 +914,7 @@ Section HaskFlattener. eapply nd_rule. eapply RArrange. simpl. - apply RCanR. + apply ACanR. apply boost. simpl. apply ga_curry. @@ -1086,23 +926,14 @@ Section HaskFlattener. apply flatten_coercion; auto. apply (Prelude_error "RCast at level >0; casting inside of code brackets is currently not supported"). - destruct case_RJoin. - simpl. - destruct (getjlev x); destruct (getjlev q); - [ apply nd_rule; apply RJoin | idtac | idtac | idtac ]; - apply (Prelude_error "RJoin at depth >0"). - destruct case_RApp. simpl. - destruct lev as [|ec lev]. simpl. apply nd_rule. - unfold flatten_leveled_type at 4. - unfold flatten_leveled_type at 2. + destruct lev as [|ec lev]. + unfold flatten_type at 1. simpl. - replace (flatten_type (tx ---> te)) - with (flatten_type tx ---> flatten_type te). + apply nd_rule. apply RApp. - reflexivity. repeat drop_simplify. repeat take_simplify. @@ -1123,34 +954,151 @@ Section HaskFlattener. Notation "!<[@]> x" := (mapOptionTree flatten_leveled_type x) (at level 1). *) - destruct case_RLet. + destruct case_RCut. simpl. - destruct lev as [|ec lev]; simpl; [ apply nd_rule; apply RLet; auto | idtac ]. - repeat drop_simplify. - repeat take_simplify. + destruct l as [|ec lev]; simpl. + apply nd_rule. + replace (mapOptionTree flatten_leveled_type (Σ₁₂ @@@ nil)) with (mapOptionTree flatten_type Σ₁₂ @@@ nil). + apply RCut. + induction Σ₁₂; try destruct a; auto. + simpl. + rewrite <- IHΣ₁₂1. + rewrite <- IHΣ₁₂2. + reflexivity. + simpl; repeat drop_simplify. + simpl; repeat take_simplify. simpl. - - eapply nd_comp. - eapply nd_prod; [ idtac | apply nd_id ]. - eapply boost. - apply ga_second. - - eapply nd_comp. - eapply nd_prod. + set (drop_lev (ec :: lev) (Σ₁₂ @@@ (ec :: lev))) as x1. + rewrite take_lemma'. + rewrite mapOptionTree_compose. + rewrite mapOptionTree_compose. + rewrite mapOptionTree_compose. + rewrite mapOptionTree_compose. + rewrite unlev_relev. + rewrite <- mapOptionTree_compose. + rewrite <- mapOptionTree_compose. + rewrite <- mapOptionTree_compose. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RCut ]. + apply nd_prod. apply nd_id. eapply nd_comp. eapply nd_rule. eapply RArrange. - apply RCanR. - eapply precompose. + eapply ALeft. + eapply ARight. + unfold x1. + rewrite drop_to_nothing. + apply arrangeCancelEmptyTree with (q:=(mapTree (fun _ : ??(HaskType Γ ★) => tt) Σ₁₂)). + induction Σ₁₂; try destruct a; auto. + simpl. + rewrite <- IHΣ₁₂1 at 2. + rewrite <- IHΣ₁₂2 at 2. + reflexivity. + eapply nd_comp; [ eapply nd_rule; eapply RArrange; eapply ALeft; eapply ACanL | idtac ]. + set (mapOptionTree flatten_type Σ₁₂) as a. + set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) Σ₁)) as b. + set (mapOptionTree flatten_leveled_type (drop_lev (ec :: lev) Σ₂)) as c. + set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) Σ₂)) as d. + set (mapOptionTree flatten_leveled_type (drop_lev (ec :: lev) Σ)) as e. + set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) Σ)) as f. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RCut ]. + eapply nd_comp; [ apply nd_llecnac | idtac ]. + apply nd_prod. + simpl. + eapply secondify. + apply ga_first. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ALeft; eapply AExch ]. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AuAssoc ]. + simpl. + apply precompose. - apply nd_rule. - apply RLet. + destruct case_RLeft. + simpl. + destruct l as [|ec lev]. + simpl. + replace (mapOptionTree flatten_leveled_type (Σ @@@ nil)) with (mapOptionTree flatten_type Σ @@@ nil). + apply nd_rule. + apply RLeft. + induction Σ; try destruct a; auto. + simpl. + rewrite <- IHΣ1. + rewrite <- IHΣ2. + reflexivity. + repeat drop_simplify. + rewrite drop_to_nothing. + simpl. + eapply nd_comp. + Focus 2. + eapply nd_rule. + eapply RArrange. + eapply ARight. + apply arrangeUnCancelEmptyTree with (q:=(mapTree (fun _ : ??(HaskType Γ ★) => tt) Σ)). + induction Σ; try destruct a; auto. + simpl. + rewrite <- IHΣ1 at 2. + rewrite <- IHΣ2 at 2. + reflexivity. + idtac. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AuCanL ]. + apply boost. + take_simplify. + simpl. + replace (take_lev (ec :: lev) (Σ @@@ (ec :: lev))) with (Σ @@@ (ec::lev)). + rewrite mapOptionTree_compose. + rewrite mapOptionTree_compose. + rewrite unlev_relev. + apply ga_second. + rewrite take_lemma'. + reflexivity. + + destruct case_RRight. + simpl. + destruct l as [|ec lev]. + simpl. + replace (mapOptionTree flatten_leveled_type (Σ @@@ nil)) with (mapOptionTree flatten_type Σ @@@ nil). + apply nd_rule. + apply RRight. + induction Σ; try destruct a; auto. + simpl. + rewrite <- IHΣ1. + rewrite <- IHΣ2. + reflexivity. + repeat drop_simplify. + rewrite drop_to_nothing. + simpl. + eapply nd_comp. + Focus 2. + eapply nd_rule. + eapply RArrange. + eapply ALeft. + apply arrangeUnCancelEmptyTree with (q:=(mapTree (fun _ : ??(HaskType Γ ★) => tt) Σ)). + induction Σ; try destruct a; auto. + simpl. + rewrite <- IHΣ1 at 2. + rewrite <- IHΣ2 at 2. + reflexivity. + idtac. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AuCanR ]. + apply boost. + take_simplify. + simpl. + replace (take_lev (ec :: lev) (Σ @@@ (ec :: lev))) with (Σ @@@ (ec::lev)). + rewrite mapOptionTree_compose. + rewrite mapOptionTree_compose. + rewrite unlev_relev. + apply ga_first. + rewrite take_lemma'. + reflexivity. destruct case_RVoid. simpl. + destruct l. apply nd_rule. apply RVoid. + drop_simplify. + take_simplify. + simpl. + apply ga_id. destruct case_RAppT. simpl. destruct lev; simpl. @@ -1166,9 +1114,6 @@ Section HaskFlattener. destruct case_RAbsT. simpl. destruct lev; simpl. - unfold flatten_leveled_type at 4. - unfold flatten_leveled_type at 2. - simpl. rewrite flatten_commutes_with_HaskTAll. rewrite flatten_commutes_with_HaskTApp. eapply nd_comp; [ idtac | eapply nd_rule; eapply RAbsT ]. @@ -1197,8 +1142,6 @@ Section HaskFlattener. destruct case_RAppCo. simpl. destruct lev; simpl. - unfold flatten_leveled_type at 4. - unfold flatten_leveled_type at 2. unfold flatten_type. simpl. apply nd_rule. @@ -1216,8 +1159,41 @@ Section HaskFlattener. destruct case_RLetRec. rename t into lev. + simpl. destruct lev; simpl. + apply nd_rule. + set (@RLetRec Γ Δ (mapOptionTree flatten_leveled_type lri) (flatten_type x) (mapOptionTree flatten_type y) nil) as q. + replace (mapOptionTree flatten_leveled_type (y @@@ nil)) with (mapOptionTree flatten_type y @@@ nil). + apply q. + induction y; try destruct a; auto. + simpl. + rewrite IHy1. + rewrite IHy2. + reflexivity. + repeat drop_simplify. + repeat take_simplify. simpl. - apply (Prelude_error "LetRec not supported (FIXME)"). + rewrite drop_to_nothing. + eapply nd_comp. + eapply nd_rule. + eapply RArrange. + eapply AComp. + eapply ARight. + apply arrangeCancelEmptyTree with (q:=y). + induction y; try destruct a; auto. + simpl. + rewrite <- IHy1. + rewrite <- IHy2. + reflexivity. + apply ACanL. + rewrite take_lemma'. + set (mapOptionTree (flatten_type ○ unlev) (take_lev (h :: lev) lri)) as lri'. + set (mapOptionTree flatten_leveled_type (drop_lev (h :: lev) lri)) as lri''. + replace (mapOptionTree (flatten_type ○ unlev) (y @@@ (h :: lev))) with (mapOptionTree flatten_type y). + apply boost. + apply ga_loopl. + rewrite <- mapOptionTree_compose. + simpl. + reflexivity. destruct case_RCase. simpl. @@ -1235,18 +1211,21 @@ Section HaskFlattener. 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; apply tree_of_nothing | idtac ]. - refine (ga_unkappa' Γ Δ (v2t ec) nil _ _ _ _ ;; _). + eapply nd_comp; [ eapply nd_rule; eapply RArrange; eapply ALeft; apply tree_of_nothing | idtac ]. + eapply nd_comp; [ eapply nd_rule; eapply RArrange; eapply ACanR | idtac ]. + refine (ga_unkappa Γ Δ (v2t ec) nil _ _ _ _ ;; _). + eapply nd_comp; [ idtac | eapply arrange_brak ]. unfold succ_host. unfold succ_guest. - apply arrange_brak. + eapply nd_rule. + eapply RArrange. + apply AExch. apply (Prelude_error "found Brak at depth >0 indicating 3-level code; only two-level code is currently supported"). destruct case_SEsc. @@ -1260,7 +1239,8 @@ Section HaskFlattener. take_simplify. drop_simplify. simpl. - eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply tree_of_nothing' ]. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ALeft; apply tree_of_nothing' ]. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ACanR ]. simpl. rewrite take_lemma'. rewrite unlev_relev. @@ -1276,13 +1256,15 @@ Section HaskFlattener. 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 RCanR ]. - eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ]. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply AuCanR ]. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply AuCanR ]. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply ACanL ]. + eapply nd_comp; [ idtac | 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 ]. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ACanL ]. simpl. apply ga_join. apply IHx1. @@ -1307,12 +1289,19 @@ Section HaskFlattener. apply IHx2. (* environment has non-empty leaves *) - apply ga_kappa'. + 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 flatten_proof : + forall {h}{c}, + ND Rule h c -> + ND Rule h c. + apply (Prelude_error "sorry, non-skolemized flattening isn't implemented"). + Defined. + Definition skolemize_and_flatten_proof : forall {h}{c}, ND Rule h c -> @@ -1322,7 +1311,7 @@ Section HaskFlattener. intros. rewrite mapOptionTree_compose. rewrite mapOptionTree_compose. - apply flatten_proof. + apply flatten_skolemized_proof. apply skolemize_proof. apply X. Defined.