let RCut take a left environment as well

[coq-hetmet.git] / src / HaskSkolemizer.v

diff --git a/src/HaskSkolemizer.v b/src/HaskSkolemizer.v
index 76e1bdb..b1d65e6 100644 (file)
--- a/src/HaskSkolemizer.v
+++ b/src/HaskSkolemizer.v
@@ -125,14 +125,14 @@ Section HaskSkolemizer.
     destruct (eqd_dec ([tx],,take_arg_types_as_tree te) (take_arg_types_as_tree (tx ---> te))).
       rewrite <- e.
       simpl.
-      apply RId.
+      apply AId.
     unfold take_arg_types_as_tree.
       Opaque take_arg_types_as_tree.
       simpl.
       destruct (count_arg_types (te (fun _ : Kind => unit) (ite_unit Γ))).
       simpl.
       replace (tx) with (fun (TV : Kind → Type) (ite : InstantiatedTypeEnv TV Γ) => tx TV ite).
-      apply RCanR.
+      apply ACanR.
         apply phoas_extensionality.
         reflexivity.
     apply (Prelude_error "should not be possible").
@@ -146,14 +146,14 @@ Section HaskSkolemizer.
     destruct (eqd_dec ([tx],,take_arg_types_as_tree te) (take_arg_types_as_tree (tx ---> te))).
       rewrite <- e.
       simpl.
-      apply RId.
+      apply AId.
     unfold take_arg_types_as_tree.
       Opaque take_arg_types_as_tree.
       simpl.
       destruct (count_arg_types (te (fun _ : Kind => unit) (ite_unit Γ))).
       simpl.
       replace (tx) with (fun (TV : Kind → Type) (ite : InstantiatedTypeEnv TV Γ) => tx TV ite).
-      apply RuCanR.
+      apply AuCanR.
         apply phoas_extensionality.
         reflexivity.
     apply (Prelude_error "should not be possible").
@@ -232,8 +232,10 @@ 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 _
       | RBrak    Γ Δ t ec succ lev     => let case_RBrak := tt         in _
       | REsc     Γ Δ t ec succ lev     => let case_REsc := tt          in _
@@ -251,7 +253,7 @@ Section HaskSkolemizer.
         apply nd_rule.
         apply SFlat.
         apply RArrange.
-        apply RRight.
+        apply ARight.
         apply d.
 
       destruct case_RBrak.
@@ -288,7 +290,7 @@ Section HaskSkolemizer.
         rewrite H.
         rewrite H0.
         simpl.
-        eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; apply RuCanL ].
+        eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; apply AuCanL ].
         apply nd_rule.
         apply SFlat.
         apply RLit.
@@ -303,7 +305,7 @@ Section HaskSkolemizer.
         rewrite H.
         rewrite H0.
         simpl.
-        eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply RArrange; apply RuCanR ].
+        eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply RArrange; apply AuCanR ].
         apply nd_rule.
         apply SFlat.
         apply RVar.
@@ -318,7 +320,7 @@ Section HaskSkolemizer.
         rewrite H.
         rewrite H0.
         simpl.
-        eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply RArrange; apply RuCanR ].
+        eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply RArrange; apply AuCanR ].
         apply nd_rule.
         apply SFlat.
         apply RGlobal.
@@ -334,9 +336,9 @@ Section HaskSkolemizer.
         apply nd_rule.
           apply SFlat.
           apply RArrange.
-          eapply RComp.
-          eapply RCossa.
-          eapply RLeft.
+          eapply AComp.
+          eapply AuAssoc.
+          eapply ALeft.
           apply take_arrange.
 
       destruct case_RCast.
@@ -348,14 +350,6 @@ Section HaskSkolemizer.
         apply γ.
         apply (Prelude_error "found RCast at level >0").
 
-      destruct case_RJoin.
-        simpl.
-        destruct l.
-        apply nd_rule.
-        apply SFlat.
-        apply RJoin.
-        apply (Prelude_error "found RJoin at level >0").
-
       destruct case_RApp.
         simpl.
         destruct lev.
@@ -370,14 +364,14 @@ Section HaskSkolemizer.
         rewrite H0.
         simpl.
         eapply nd_comp.
-        eapply nd_prod; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply RCanR ].
+        eapply nd_prod; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply ACanR ].
         eapply nd_rule.
         eapply SFlat.
         eapply RArrange.
-        eapply RLeft.
+        eapply ALeft.
         eapply take_unarrange.
 
-        eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply RArrange; apply RAssoc ].
+        eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply RArrange; apply AAssoc ].
         eapply nd_rule; eapply SFlat; apply RWhere.
 
       destruct case_RLet.
@@ -393,17 +387,17 @@ Section HaskSkolemizer.
         rewrite H0.
 
         eapply nd_comp.
-        eapply nd_prod; [ eapply nd_rule; eapply SFlat; eapply RArrange; eapply RCanR | eapply nd_id ].
+        eapply nd_prod; [ eapply nd_rule; eapply SFlat; eapply RArrange; eapply ACanR | eapply nd_id ].
 
         set (@RLet Γ Δ Σ₁ (Σ₂,,(take_arg_types_as_tree σ₂ @@@ (h::lev))) σ₁ (drop_arg_types_as_tree σ₂) (h::lev)) as q.
-        eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply RArrange; apply RAssoc ].
+        eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply RArrange; apply AAssoc ].
         eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply q ].
         apply nd_prod.
           apply nd_id.
           apply nd_rule.
           eapply SFlat.
           eapply RArrange.
-          eapply RCossa.
+          eapply AuAssoc.
 
       destruct case_RWhere.
         simpl.
@@ -418,16 +412,97 @@ Section HaskSkolemizer.
         rewrite H0.
 
         eapply nd_comp.
-        eapply nd_prod; [ apply nd_id | eapply nd_rule; eapply SFlat; eapply RArrange; eapply RCanR ].
-        eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply RAssoc ].
-        eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply RLeft; eapply RAssoc ].
+        eapply nd_prod; [ apply nd_id | eapply nd_rule; eapply SFlat; eapply RArrange; eapply ACanR ].
+        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 AAssoc ].
         eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RWhere ].
         apply nd_prod; [ idtac | eapply nd_id ].
         eapply nd_rule; apply SFlat; eapply RArrange.
-        eapply RComp.
-        eapply RCossa.
-        apply RLeft.
-        eapply RCossa.
+        eapply AComp.
+        eapply AuAssoc.
+        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 (Σ₁₂'' @@@ (h::l)));
+          [ 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.
+        clear e.
+        destruct s.
+        eapply nd_comp.
+          eapply nd_prod.
+          eapply nd_rule.
+          eapply SFlat.
+          eapply RArrange.
+          eapply AComp.
+          eapply ALeft.
+          eapply arrangeCancelEmptyTree with (q:=x).
+          apply e.
+          apply ACanR.
+          apply nd_id.
+        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 AAssoc ].
+        eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RCut ].
+        apply nd_prod.
+        apply nd_id.
+        eapply nd_rule.
+          eapply SFlat.
+          eapply RArrange.
+          eapply AComp.
+          eapply AuAssoc.
+          eapply ALeft.
+          eapply AComp.
+          eapply AuAssoc.
+          eapply ALeft.
+          eapply AId.
+
+      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.
@@ -435,7 +510,7 @@ Section HaskSkolemizer.
         apply nd_rule.
         apply SFlat.
         apply RVoid.
-        eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply RuCanL ].
+        eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply AuCanL ].
         apply nd_rule.
         apply SFlat.
         apply RVoid.