add RCut, RLeft, RRight rules

diff --git a/src/HaskFlattener.v b/src/HaskFlattener.v
index 1bb35c6..c5587c1 100644 (file)
--- a/src/HaskFlattener.v
+++ b/src/HaskFlattener.v
@@ -784,6 +784,21 @@ Section HaskFlattener.
     admit.
     Qed.
 
+  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_proof :
     forall  {h}{c},
       ND SRule h c ->
@@ -816,6 +831,9 @@ 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 _
+      | RCut    Γ Δ Σ₁ Σ₁₂ Σ₂ Σ₃ l    => let case_RCut := tt          in _
+      | RLeft   Γ Δ Σ₁ Σ₂  Σ     l    => let case_RLeft := tt in _
+      | RRight  Γ Δ Σ₁ Σ₂  Σ     l    => let case_RRight := tt in _
       | RWhere   Γ Δ Σ₁ Σ₂ Σ₃ σ₁ σ₂ lev   => let case_RWhere := tt          in _
       | RJoin    Γ p lri m x q l       => let case_RJoin := tt in _
       | RVoid    _ _       l           => let case_RVoid := tt   in _
@@ -1000,6 +1018,125 @@ Section HaskFlattener.
       apply ALeft.
       apply ACanL.
 
+    destruct case_RCut.
+      simpl.
+      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.
+      set (drop_lev (ec :: lev) (Σ₁₂ @@@ (ec :: lev))) as x1.
+      rewrite take_lemma'.
+      rewrite mapOptionTree_compose.
+      rewrite mapOptionTree_compose.
+      rewrite mapOptionTree_compose.
+      rewrite unlev_relev.
+      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.
+      eapply ARight.
+      unfold x1.
+      rewrite drop_to_nothing.
+      apply arrangeCancelEmptyTree with (q:=(mapTree (fun _ : ??(HaskType Γ ★) => tt) Σ₁₂)).
+      admit. (* OK *)
+      eapply nd_comp; [ eapply nd_rule; eapply RArrange; 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.
+      eapply nd_comp; [ idtac | eapply nd_rule; eapply RCut ].
+      eapply nd_comp; [ apply nd_llecnac | idtac ].
+      apply nd_prod.
+      simpl.
+      eapply ga_first.
+      eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AExch ].
+      simpl.
+      apply precompose.
+
+    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) Σ)).
+        admit (* FIXME *).
+        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) Σ)).
+        admit (* FIXME *).
+        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.
       apply nd_rule.

diff --git a/src/HaskProof.v b/src/HaskProof.v
index 9787c62..46009f8 100644 (file)
--- a/src/HaskProof.v
+++ b/src/HaskProof.v
@@ -73,6 +73,10 @@ Inductive Rule : Tree ??Judg -> Tree ??Judg -> Type :=
 | RLet           : ∀ Γ Δ Σ₁ Σ₂ σ₁ σ₂ l,  Rule ([Γ>Δ> Σ₁ |- [σ₁]@l],,[Γ>Δ> [σ₁@@l],,Σ₂ |- [σ₂]@l ])     [Γ>Δ> Σ₁,,Σ₂ |- [σ₂   ]@l]
 | RWhere         : ∀ Γ Δ Σ₁ Σ₂ Σ₃ σ₁ σ₂ l,  Rule ([Γ>Δ> Σ₁,,([σ₁@@l],,Σ₃) |- [σ₂]@l ],,[Γ>Δ> Σ₂ |- [σ₁]@l])     [Γ>Δ> Σ₁,,(Σ₂,,Σ₃) |- [σ₂ ]@l]
 
+| RCut           : ∀ Γ Δ Σ₁ Σ₁₂ Σ₂ Σ₃ l,  Rule ([Γ>Δ> Σ₁ |- Σ₁₂ @l],,[Γ>Δ> (Σ₁₂@@@l),,Σ₂ |- Σ₃@l ]) [Γ>Δ> Σ₁,,Σ₂ |- Σ₃@l]
+| RLeft          : ∀ Γ Δ Σ₁ Σ₂  Σ     l,  Rule  [Γ>Δ> Σ₁ |- Σ₂  @l]                                 [Γ>Δ> (Σ@@@l),,Σ₁ |- Σ,,Σ₂@l]
+| RRight         : ∀ Γ Δ Σ₁ Σ₂  Σ     l,  Rule  [Γ>Δ> Σ₁ |- Σ₂  @l]                                 [Γ>Δ> Σ₁,,(Σ@@@l) |- Σ₂,,Σ@l]
+
 | RVoid    : ∀ Γ Δ l,               Rule [] [Γ > Δ > [] |- [] @l ]
 
 | RAppT   : forall Γ Δ Σ κ σ (τ:HaskType Γ κ) l,      Rule [Γ>Δ> Σ   |- [HaskTAll κ σ]@l]      [Γ>Δ>    Σ     |- [substT σ τ]@l]
@@ -147,6 +151,9 @@ Lemma no_rules_with_multiple_conclusions : forall c h,
     destruct X0; destruct s; inversion e.
     destruct X0; destruct s; inversion e.
     destruct X0; destruct s; inversion e.
+    destruct X0; destruct s; inversion e.
+    destruct X0; destruct s; inversion e.
+    destruct X0; destruct s; inversion e.
     Qed.
 
 Lemma systemfc_all_rules_one_conclusion : forall h c1 c2 (r:Rule h (c1,,c2)), False.

diff --git a/src/HaskProofToLatex.v b/src/HaskProofToLatex.v
index 99af119..dedc152 100644 (file)
--- a/src/HaskProofToLatex.v
+++ b/src/HaskProofToLatex.v
@@ -190,6 +190,9 @@ Fixpoint nd_ruleToRawLatexMath {h}{c}(r:Rule h c) : string :=
     | RAbsCo        _ _ _ _ _ _ _ _   => "AbsCo"
     | RApp          _ _ _ _ _ _ _     => "App"
     | RLet          _ _ _ _ _ _ _     => "Let"
+    | RCut          _ _ _ _ _ _ _     => "Cut"
+    | RLeft         _ _ _ _ _ _       => "Left"
+    | RRight        _ _ _ _ _ _       => "Right"
     | RWhere        _ _ _ _ _ _ _ _   => "Where"
     | RJoin         _ _ _ _ _ _ _     => "RJoin"
     | RLetRec       _ _ _ _ _ _       => "LetRec"

diff --git a/src/HaskProofToStrong.v b/src/HaskProofToStrong.v
index 299a83b..b16d4a8 100644 (file)
--- a/src/HaskProofToStrong.v
+++ b/src/HaskProofToStrong.v
@@ -509,6 +509,242 @@ Section HaskProofToStrong.
 
     Defined.
 
+  Lemma manyFresh : forall Γ Σ (ξ0:VV -> LeveledHaskType Γ ★),
+    FreshM { vars : _ & { ξ : VV -> LeveledHaskType Γ ★ & Σ = mapOptionTree ξ vars } }.
+    intros Γ Σ.
+    induction Σ; intro ξ.
+    destruct a.
+    destruct l as [τ l].
+    set (fresh_lemma' Γ [τ] [] [] ξ l (refl_equal _)) as q.
+    refine (q >>>= fun q' => return _).
+    apply FreshMon.
+    clear q.
+    destruct q' as [varstypes [pf1 [pf2 distpf]]].
+    exists (mapOptionTree (@fst _ _) varstypes).
+    exists (update_xi ξ l (leaves varstypes)).
+    symmetry; auto.
+    refine (return _).
+    exists [].
+    exists ξ; auto.
+    refine (bind f1 = IHΣ1 ξ ; _).
+    apply FreshMon.
+    destruct f1 as [vars1 [ξ1 pf1]].
+    refine (bind f2 = IHΣ2 ξ1 ; _).
+    apply FreshMon.
+    destruct f2 as [vars2 [ξ2 pf22]].
+    refine (return _).
+    exists (vars1,,vars2).
+    exists ξ2.
+    simpl.
+    rewrite pf22.
+    rewrite pf1.
+    admit.         (* freshness assumption *)
+    Defined.
+
+  Definition rlet Γ Δ Σ₁ Σ₂ σ₁ σ₂ p :
+    forall (X_ : ITree Judg judg2exprType
+         ([Γ > Δ > Σ₁ |- [σ₁] @ p],, [Γ > Δ > [σ₁ @@  p],, Σ₂ |- [σ₂] @ p])),
+   ITree Judg judg2exprType [Γ > Δ > Σ₁,, Σ₂ |- [σ₂] @ p].
+    intros.
+    apply ILeaf.
+    simpl in *; intros.
+    destruct vars; try destruct o; inversion H.
+
+    refine (fresh_lemma _ ξ _ _ σ₁ p H2 >>>= (fun pf => _)).
+    apply FreshMon.
+
+    destruct pf as [ vnew [ pf1 pf2 ]].
+    set (update_xi ξ p (((vnew, σ₁ )) :: nil)) as ξ' in *.
+    inversion X_.
+    apply ileaf in X.
+    apply ileaf in X0.
+    simpl in *.
+
+    refine (X ξ vars1 _ >>>= fun X0' => _).
+    apply FreshMon.
+    simpl.
+    auto.
+
+    refine (X0 ξ' ([vnew],,vars2) _ >>>= fun X1' => _).
+    apply FreshMon.
+    simpl.
+    rewrite pf2.
+    rewrite pf1.
+    reflexivity.
+    apply FreshMon.
+
+    apply ILeaf.
+    apply ileaf in X1'.
+    apply ileaf in X0'.
+    simpl in *.
+    apply ELet with (ev:=vnew)(tv:=σ₁).
+    apply X0'.
+    apply X1'.
+    Defined.
+
+  Definition vartree Γ Δ Σ lev ξ :
+    forall vars, Σ @@@ lev = mapOptionTree ξ vars ->
+    ITree (HaskType Γ ★) (fun t : HaskType Γ ★ => Expr Γ Δ ξ t lev) Σ.
+    induction Σ; intros.
+    destruct a.
+    intros; simpl in *.
+    apply ILeaf.
+    destruct vars; try destruct o; inversion H.
+    set (EVar Γ Δ ξ v) as q.
+    rewrite <- H1 in q.
+    apply q.
+    intros.
+    apply INone.
+    intros.
+    destruct vars; try destruct o; inversion H.
+    apply IBranch.
+    eapply IHΣ1.
+    apply H1.
+    eapply IHΣ2.
+    apply H2.
+    Defined.
+
+
+  Definition rdrop  Γ Δ Σ₁ Σ₁₂ a lev :
+    ITree Judg judg2exprType [Γ > Δ > Σ₁ |- a,,Σ₁₂ @ lev] ->
+    ITree Judg judg2exprType [Γ > Δ > Σ₁ |- a @ lev].
+    intros.
+    apply ileaf in X.
+    apply ILeaf.
+    simpl in *.
+    intros.
+    set (X ξ vars H) as q.
+    simpl in q.
+    refine (q >>>= fun q' => return _).
+    apply FreshMon.
+    inversion q'.
+    apply X0.
+    Defined.
+
+  Definition rdrop'  Γ Δ Σ₁ Σ₁₂ a lev :
+    ITree Judg judg2exprType [Γ > Δ > Σ₁ |- Σ₁₂,,a @ lev] ->
+    ITree Judg judg2exprType [Γ > Δ > Σ₁ |- a @ lev].
+    intros.
+    apply ileaf in X.
+    apply ILeaf.
+    simpl in *.
+    intros.
+    set (X ξ vars H) as q.
+    simpl in q.
+    refine (q >>>= fun q' => return _).
+    apply FreshMon.
+    inversion q'.
+    auto.
+    Defined.
+
+  Definition rdrop''  Γ Δ Σ₁ Σ₁₂ lev :
+    ITree Judg judg2exprType [Γ > Δ > [],,Σ₁ |- Σ₁₂ @ lev] ->
+    ITree Judg judg2exprType [Γ > Δ > Σ₁ |- Σ₁₂ @ lev].
+    intros.
+    apply ileaf in X.
+    apply ILeaf.
+    simpl in *; intros.
+    eapply X with (vars:=[],,vars).
+    rewrite H; reflexivity.
+    Defined.
+
+  Definition rdrop'''  Γ Δ a Σ₁ Σ₁₂ lev :
+    ITree Judg judg2exprType [Γ > Δ > Σ₁ |- Σ₁₂ @ lev] ->
+    ITree Judg judg2exprType [Γ > Δ > a,,Σ₁ |- Σ₁₂ @ lev].
+    intros.
+    apply ileaf in X.
+    apply ILeaf.
+    simpl in *; intros.
+    destruct vars; try destruct o; inversion H.
+    eapply X with (vars:=vars2).
+    auto.
+    Defined.
+
+  Definition rassoc  Γ Δ Σ₁ a b c lev :
+    ITree Judg judg2exprType [Γ > Δ > ((a,,b),,c) |- Σ₁ @ lev] ->
+    ITree Judg judg2exprType [Γ > Δ > (a,,(b,,c)) |- Σ₁ @ lev].
+    intros.
+    apply ileaf in X.
+    apply ILeaf.
+    simpl in *; intros.
+    destruct vars; try destruct o; inversion H.
+    destruct vars2; try destruct o; inversion H2.
+    apply X with (vars:=(vars1,,vars2_1),,vars2_2).
+    subst; reflexivity.
+    Defined.
+
+  Definition rassoc'  Γ Δ Σ₁ a b c lev :
+    ITree Judg judg2exprType [Γ > Δ > (a,,(b,,c)) |- Σ₁ @ lev] ->
+    ITree Judg judg2exprType [Γ > Δ > ((a,,b),,c) |- Σ₁ @ lev].
+    intros.
+    apply ileaf in X.
+    apply ILeaf.
+    simpl in *; intros.
+    destruct vars; try destruct o; inversion H.
+    destruct vars1; try destruct o; inversion H1.
+    apply X with (vars:=vars1_1,,(vars1_2,,vars2)).
+    subst; reflexivity.
+    Defined.
+
+  Definition swapr  Γ Δ Σ₁ a b c lev :
+    ITree Judg judg2exprType [Γ > Δ > ((a,,b),,c) |- Σ₁ @ lev] ->
+    ITree Judg judg2exprType [Γ > Δ > ((b,,a),,c) |- Σ₁ @ lev].
+    intros.
+    apply ileaf in X.
+    apply ILeaf.
+    simpl in *; intros.
+    destruct vars; try destruct o; inversion H.
+    destruct vars1; try destruct o; inversion H1.
+    apply X with (vars:=(vars1_2,,vars1_1),,vars2).
+    subst; reflexivity.
+    Defined.
+
+  Definition rdup  Γ Δ Σ₁ a  c lev :
+    ITree Judg judg2exprType [Γ > Δ > ((a,,a),,c) |- Σ₁ @ lev] ->
+    ITree Judg judg2exprType [Γ > Δ > (a,,c) |- Σ₁ @ lev].
+    intros.
+    apply ileaf in X.
+    apply ILeaf.
+    simpl in *; intros.
+    destruct vars; try destruct o; inversion H.
+    apply X with (vars:=(vars1,,vars1),,vars2).    (* is this allowed? *)
+    subst; reflexivity.
+    Defined.
+
+  (* holy cow this is ugly *)
+  Definition rcut Γ Δ  Σ₃ lev  Σ₁₂  :
+    forall Σ₁ Σ₂,
+    ITree Judg judg2exprType [Γ > Δ > Σ₁ |-  Σ₁₂ @ lev] ->
+    ITree Judg judg2exprType [Γ > Δ >  Σ₁₂ @@@ lev,,Σ₂ |- [Σ₃] @ lev] ->
+    ITree Judg judg2exprType [Γ > Δ > Σ₁,,Σ₂ |- [Σ₃] @ lev].
+
+    induction Σ₁₂.
+    intros.
+    destruct a.
+
+    eapply rlet.
+    apply IBranch.
+    apply X.
+    apply X0.
+
+    simpl in X0.
+    apply rdrop'' in X0.
+    apply rdrop'''.
+    apply X0.
+
+    intros.
+    simpl in X0.
+    apply rassoc in X0.
+    set (IHΣ₁₂1 _ _ (rdrop  _ _ _ _ _ _ X) X0) as q.
+    set (IHΣ₁₂2 _ (Σ₁,,Σ₂) (rdrop' _ _ _ _ _ _ X)) as q'.
+    apply rassoc' in q.
+    apply swapr in q.
+    apply rassoc in q.
+    set (q' q) as q''.
+    apply rassoc' in q''.
+    apply rdup in q''.
+    apply q''.
+    Defined.
 
   Definition rule2expr : forall h j (r:Rule h j), ITree _ judg2exprType h -> ITree _ judg2exprType j.
 
@@ -528,6 +764,9 @@ Section HaskProofToStrong.
       | RAbsCo  Γ Δ Σ κ σ  σ₁ σ₂  y   => let case_RAbsCo := tt        in _
       | RApp    Γ Δ Σ₁ Σ₂ tx te p     => let case_RApp := tt          in _
       | RLet    Γ Δ Σ₁ Σ₂ σ₁ σ₂ p     => let case_RLet := tt          in _
+      | RCut    Γ Δ Σ₁ Σ₁₂ Σ₂ Σ₃ l    => let case_RCut := tt          in _
+      | RLeft   Γ Δ Σ₁ Σ₂  Σ     l    => let case_RLeft := tt in _
+      | RRight  Γ Δ Σ₁ Σ₂  Σ     l    => let case_RRight := tt in _
       | RWhere  Γ Δ Σ₁ Σ₂ Σ₃ σ₁ σ₂ p  => let case_RWhere := tt          in _
       | RJoin   Γ p lri m x q l       => let case_RJoin := tt in _
       | RVoid   _ _ l                 => let case_RVoid := tt   in _
@@ -645,40 +884,8 @@ Section HaskProofToStrong.
     apply (EApp _ _ _ _ _ _ q1' q2').
 
   destruct case_RLet.
-    apply ILeaf.
-    simpl in *; intros.
-    destruct vars; try destruct o; inversion H.
-
-    refine (fresh_lemma _ ξ _ _ σ₁ p H2 >>>= (fun pf => _)).
-    apply FreshMon.
-
-    destruct pf as [ vnew [ pf1 pf2 ]].
-    set (update_xi ξ p (((vnew, σ₁ )) :: nil)) as ξ' in *.
-    inversion X_.
-    apply ileaf in X.
-    apply ileaf in X0.
-    simpl in *.
-
-    refine (X ξ vars1 _ >>>= fun X0' => _).
-    apply FreshMon.
-    simpl.
-    auto.
-
-    refine (X0 ξ' ([vnew],,vars2) _ >>>= fun X1' => _).
-    apply FreshMon.
-    simpl.
-    rewrite pf2.
-    rewrite pf1.
-    reflexivity.
-    apply FreshMon.
-
-    apply ILeaf.
-    apply ileaf in X1'.
-    apply ileaf in X0'.
-    simpl in *.
-    apply ELet with (ev:=vnew)(tv:=σ₁).
-    apply X0'.
-    apply X1'.
+    eapply rlet.
+    apply X_.
 
   destruct case_RWhere.
     apply ILeaf.
@@ -720,6 +927,57 @@ Section HaskProofToStrong.
     apply X1'.
     apply X0'.
 
+  destruct case_RCut.
+    inversion X_.
+    subst.
+    clear X_.
+    induction Σ₃.
+    destruct a.
+    subst.
+    eapply rcut.
+    apply X.
+    apply X0.
+
+    apply ILeaf.
+    simpl.
+    intros.
+    refine (return _).
+    apply INone.
+    set (IHΣ₃1 (rdrop  _ _ _ _ _ _ X0)) as q1.
+    set (IHΣ₃2 (rdrop' _ _ _ _ _ _ X0)) as q2.
+    apply ileaf in q1.
+    apply ileaf in q2.
+    simpl in *.
+    apply ILeaf.
+    simpl.
+    intros.
+    refine (q1 _ _ H >>>= fun q1' => q2 _ _ H >>>= fun q2' => return _).
+    apply FreshMon.
+    apply FreshMon.
+    apply IBranch; auto.
+
+  destruct case_RLeft.
+    apply ILeaf.
+    simpl; intros.
+    destruct vars; try destruct o; inversion H.
+    refine (X_ _ _ H2 >>>= fun X' => return _).
+    apply FreshMon.
+    apply IBranch.
+    eapply vartree.
+    apply H1.
+    apply X'.
+
+  destruct case_RRight.
+    apply ILeaf.
+    simpl; intros.
+    destruct vars; try destruct o; inversion H.
+    refine (X_ _ _ H1 >>>= fun X' => return _).
+    apply FreshMon.
+    apply IBranch.
+    apply X'.
+    eapply vartree.
+    apply H2.
+
   destruct case_RVoid.
     apply ILeaf; simpl; intros.
     refine (return _).
@@ -825,38 +1083,6 @@ Section HaskProofToStrong.
     | scnd_branch _ _ _ c1 c2   => let case_branch := tt in fun q => IBranch _ _ (closed2expr _ _ c1 q) (closed2expr _ _ c2 q)
     end.
 
-  Lemma manyFresh : forall Γ Σ (ξ0:VV -> LeveledHaskType Γ ★),
-    FreshM { vars : _ & { ξ : VV -> LeveledHaskType Γ ★ & Σ = mapOptionTree ξ vars } }.
-    intros Γ Σ.
-    induction Σ; intro ξ.
-    destruct a.
-    destruct l as [τ l].
-    set (fresh_lemma' Γ [τ] [] [] ξ l (refl_equal _)) as q.
-    refine (q >>>= fun q' => return _).
-    apply FreshMon.
-    clear q.
-    destruct q' as [varstypes [pf1 [pf2 distpf]]].
-    exists (mapOptionTree (@fst _ _) varstypes).
-    exists (update_xi ξ l (leaves varstypes)).
-    symmetry; auto.
-    refine (return _).
-    exists [].
-    exists ξ; auto.
-    refine (bind f1 = IHΣ1 ξ ; _).
-    apply FreshMon.
-    destruct f1 as [vars1 [ξ1 pf1]].
-    refine (bind f2 = IHΣ2 ξ1 ; _).
-    apply FreshMon.
-    destruct f2 as [vars2 [ξ2 pf22]].
-    refine (return _).
-    exists (vars1,,vars2).
-    exists ξ2.
-    simpl.
-    rewrite pf22.
-    rewrite pf1.
-    admit.
-    Defined.
-
   Definition proof2expr Γ Δ τ l Σ (ξ0: VV -> LeveledHaskType Γ ★)
     {zz:ToString VV} : ND Rule [] [Γ > Δ > Σ |- [τ] @ l] ->
     FreshM (???{ ξ : _ & Expr Γ Δ ξ τ l}).

diff --git a/src/HaskSkolemizer.v b/src/HaskSkolemizer.v
index 259d24e..6b6c756 100644 (file)
--- a/src/HaskSkolemizer.v
+++ b/src/HaskSkolemizer.v
@@ -232,6 +232,9 @@ Section HaskSkolemizer.
       | RAbsCo   Γ Δ Σ κ σ  σ₁ σ₂  lev => let case_RAbsCo := tt        in _
       | RApp     Γ Δ Σ₁ Σ₂ tx te lev   => let case_RApp := tt          in _
       | RLet     Γ Δ Σ₁ Σ₂ σ₁ σ₂ lev   => let case_RLet := tt          in _
+      | RCut    Γ Δ Σ₁ Σ₁₂ Σ₂ Σ₃ l    => let case_RCut := tt          in _
+      | RLeft   Γ Δ Σ₁ Σ₂  Σ     l    => let case_RLeft := tt in _
+      | RRight  Γ Δ Σ₁ Σ₂  Σ     l    => let case_RRight := tt in _
       | RWhere   Γ Δ Σ₁ Σ₂ Σ₃ σ₁ σ₂ lev => let case_RWhere := tt          in _
       | RJoin    Γ p lri m x q l       => let case_RJoin := tt in _
       | RVoid    _ _           l       => let case_RVoid := tt   in _
@@ -429,6 +432,73 @@ Section HaskSkolemizer.
         apply ALeft.
         eapply AuAssoc.
 
+      destruct case_RCut.
+        simpl; destruct l; [ apply nd_rule; apply SFlat; apply RCut | idtac ].
+        set (mapOptionTreeAndFlatten take_arg_types_as_tree Σ₃) as Σ₃''.
+        set (mapOptionTree drop_arg_types_as_tree Σ₃) as Σ₃'''.
+        set (mapOptionTreeAndFlatten take_arg_types_as_tree Σ₁₂) as Σ₁₂''.
+        set (mapOptionTree drop_arg_types_as_tree Σ₁₂) as Σ₁₂'''.
+        destruct (decide_tree_empty Σ₁₂''); [ idtac | apply (Prelude_error "used RCut on a variable with function type") ].
+        destruct (eqd_dec Σ₁₂ Σ₁₂'''); [ idtac | apply (Prelude_error "used RCut on a variable with function type") ].
+        rewrite <- e.
+        eapply nd_comp.
+        eapply nd_prod; [ apply nd_id | eapply nd_rule; eapply SFlat; eapply RArrange; eapply AuAssoc ].
+        eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply AAssoc ].
+        eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RCut ].
+        apply nd_prod.
+        eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply ACanR ].
+        apply nd_rule.
+        apply SFlat.
+        apply RArrange.
+        apply ALeft.
+        destruct s.
+        eapply arrangeCancelEmptyTree with (q:=x).
+        rewrite e0.
+        admit.   (* FIXME, but not serious *)
+        apply nd_id.
+
+      destruct case_RLeft.
+        simpl; destruct l; [ apply nd_rule; apply SFlat; apply RLeft | idtac ].
+        set (mapOptionTreeAndFlatten take_arg_types_as_tree Σ₂) as Σ₂'.
+        set (mapOptionTreeAndFlatten take_arg_types_as_tree Σ) as Σ'.
+        set (mapOptionTree drop_arg_types_as_tree Σ₂) as Σ₂''.
+        set (mapOptionTree drop_arg_types_as_tree Σ) as Σ''.
+        destruct (decide_tree_empty (Σ' @@@ (h::l)));
+          [ idtac | apply (Prelude_error "used RLeft on a variable with function type") ].
+        destruct (eqd_dec Σ Σ''); [ idtac | apply (Prelude_error "used RLeft on a variable with function type") ].
+        rewrite <- e.
+        clear Σ'' e.
+        destruct s.
+        set (arrangeUnCancelEmptyTree _ _ e) as q.
+        eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply ALeft; eapply ARight; eapply q ].
+        eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply ALeft; eapply AuCanL; eapply q ].
+        eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply AAssoc ].
+        apply nd_rule.
+        eapply SFlat.
+        eapply RLeft.
+        
+      destruct case_RRight.
+        simpl; destruct l; [ apply nd_rule; apply SFlat; apply RRight | idtac ].
+        set (mapOptionTreeAndFlatten take_arg_types_as_tree Σ₂) as Σ₂'.
+        set (mapOptionTreeAndFlatten take_arg_types_as_tree Σ) as Σ'.
+        set (mapOptionTree drop_arg_types_as_tree Σ₂) as Σ₂''.
+        set (mapOptionTree drop_arg_types_as_tree Σ) as Σ''.
+        destruct (decide_tree_empty (Σ' @@@ (h::l)));
+          [ idtac | apply (Prelude_error "used RRight on a variable with function type") ].
+        destruct (eqd_dec Σ Σ''); [ idtac | apply (Prelude_error "used RRight on a variable with function type") ].
+        rewrite <- e.
+        clear Σ'' e.
+        destruct s.
+        set (arrangeUnCancelEmptyTree _ _ e) as q.
+        eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply ALeft; eapply ALeft; eapply q ].
+        eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply ALeft; eapply AuCanR ].
+        eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply AAssoc ].
+        eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply ALeft; eapply AExch ].  (* yuck *)
+        eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply AuAssoc ].
+        eapply nd_rule.
+        eapply SFlat.
+        apply RRight.
+
       destruct case_RVoid.
         simpl.
         destruct l.