X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskFlattener.v;h=1731aad97818d64f9789162903b55bd2b82cfbc1;hp=c5587c158a34a562ae9bfdc122d1b4a4143a7e63;hb=af41ffb1692ae207554342ccdc3bf73abaa75a01;hpb=c90b598203ef23bf8d44d6b5b4a5a4b5901039cf

diff --git a/src/HaskFlattener.v b/src/HaskFlattener.v
index c5587c1..1731aad 100644
--- a/src/HaskFlattener.v
+++ b/src/HaskFlattener.v
@@ -288,7 +288,7 @@ Section HaskFlattener.
     ND Rule [ Γ > Δ > ant |- [x]@lev ] [ Γ > Δ > ant      |- [y]@lev ].
     intros.
     eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ACanR ].
-    eapply nd_comp; [ idtac | eapply nd_rule; apply RLet ].
+    eapply nd_comp; [ idtac | apply RLet ].
     eapply nd_comp; [ apply nd_rlecnac | idtac ].
     apply nd_prod.
     apply nd_id.
@@ -304,7 +304,7 @@ Section HaskFlattener.
       [ Γ > Δ > a                           |- [@ga_mk _ ec y z ]@lev ]
       [ Γ > Δ > a,,[@ga_mk _ ec x y @@ lev] |- [@ga_mk _ ec x z ]@lev ].
     intros.
-    eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
+    eapply nd_comp; [ idtac | eapply RLet ].
     eapply nd_comp; [ apply nd_rlecnac | idtac ].
     apply nd_prod.
     apply nd_id.
@@ -327,7 +327,7 @@ Section HaskFlattener.
       [ Γ > Δ > 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; [ idtac | eapply RLet ].
     eapply nd_comp; [ apply nd_rlecnac | idtac ].
     apply nd_prod.
     apply nd_id.
@@ -348,7 +348,7 @@ Section HaskFlattener.
             [ Γ > Δ > Σ                    |- [@ga_mk Γ ec (a,,c) (b,,c) ]@lev ].
     intros.
     eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ACanR ].
-    eapply nd_comp; [ idtac | eapply nd_rule; apply RLet ].
+    eapply nd_comp; [ idtac | apply RLet ].
     eapply nd_comp; [ apply nd_rlecnac | idtac ].
     apply nd_prod.
     apply nd_id.
@@ -371,7 +371,7 @@ Section HaskFlattener.
      [ Γ > Δ > Σ                    |- [@ga_mk Γ ec (c,,a) (c,,b) ]@lev ].
     intros.
     eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ACanR ].
-    eapply nd_comp; [ idtac | eapply nd_rule; apply RLet ].
+    eapply nd_comp; [ idtac | apply RLet ].
     eapply nd_comp; [ apply nd_rlecnac | idtac ].
     apply nd_prod.
     apply nd_id.
@@ -394,12 +394,12 @@ Section HaskFlattener.
      [Γ > Δ > Σ,,[@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 nd_rule; eapply RLet ].
+     eapply nd_comp; [ idtac | eapply RLet ].
      eapply nd_comp; [ apply nd_llecnac | idtac ].
      apply nd_prod.
      apply ga_first.
 
-     eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
+     eapply nd_comp; [ idtac | eapply RLet ].
      eapply nd_comp; [ apply nd_llecnac | idtac ].
      apply nd_prod.
      apply postcompose.
@@ -450,14 +450,14 @@ Section HaskFlattener.
           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 ACanL ].
-          eapply nd_comp; [ idtac | eapply nd_rule; apply
+          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 AuCanR ].
           eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply ACanL ].
-          eapply nd_comp; [ idtac | eapply nd_rule;  apply RLet ].
+          eapply nd_comp; [ idtac | apply RLet ].
           eapply nd_comp; [ apply nd_llecnac | idtac ].
           eapply nd_prod.
           apply r1'.
@@ -537,13 +537,13 @@ Section HaskFlattener.
     intro pfb.
     apply secondify with (c:=a)  in pfb.
     apply firstify  with (c:=[])  in pfa.
-    eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
+    eapply nd_comp; [ idtac | eapply RLet ].
     eapply nd_comp; [ eapply nd_llecnac | idtac ].
     apply nd_prod.
     apply pfa.
     clear pfa.
 
-    eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
+    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 ].
@@ -576,7 +576,7 @@ Section HaskFlattener.
     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.
@@ -643,7 +643,7 @@ Section HaskFlattener.
     simpl.
     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 RLet ].
+    eapply nd_comp; [ idtac | apply RLet ].
     clear q''.
     eapply nd_comp; [ apply nd_rlecnac | idtac ].
     apply nd_prod.
@@ -799,7 +799,7 @@ Section HaskFlattener.
     reflexivity.
     Qed.
 
-  Definition flatten_proof :
+  Definition flatten_skolemized_proof :
     forall  {h}{c},
       ND SRule h c ->
       ND  Rule (mapOptionTree (flatten_judgment ) h) (mapOptionTree (flatten_judgment ) c).
@@ -830,12 +830,9 @@ 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 _
-      | 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 _
+      | 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 _
@@ -931,12 +928,6 @@ 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 l;
-        [ apply nd_rule; apply RJoin | idtac ];
-        apply (Prelude_error "RJoin at depth >0").
-
     destruct case_RApp.
       simpl.
 
@@ -965,59 +956,6 @@ Section HaskFlattener.
   Notation "!<[@]> x" := (mapOptionTree flatten_leveled_type x) (at level 1).
 *)
 
-    destruct case_RLet.
-      simpl.
-      destruct lev as [|ec lev]; simpl; [ apply nd_rule; apply RLet; auto | idtac ].
-      repeat drop_simplify.
-      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_first _ _ _ _ _ _ Σ₂').
-
-      eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
-      apply nd_prod.
-      apply nd_id.
-      eapply nd_comp; [ eapply nd_rule; eapply RArrange; eapply ACanL | idtac ].
-      eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AExch (* 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_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 RArrange.
-      apply ALeft.
-      apply ACanL.
-
     destruct case_RCut.
       simpl.
       destruct l as [|ec lev]; simpl.
@@ -1029,41 +967,46 @@ Section HaskFlattener.
         rewrite <- IHΣ₁₂1.
         rewrite <- IHΣ₁₂2.
         reflexivity.
-      simpl.
-      repeat drop_simplify.
-      simpl.
-      repeat take_simplify.
+      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 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.
+      eapply ALeft.
       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 ].
+      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 ga_first.
-      eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AExch ].
+      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.
 
@@ -1279,7 +1222,7 @@ Section HaskFlattener.
       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 nd_rule; eapply RLet ].
+      eapply nd_comp; [ idtac | eapply RLet ].
       eapply nd_comp; [ apply nd_llecnac | idtac ].
       apply nd_prod; [ idtac | eapply boost ].
       induction x.
@@ -1315,6 +1258,13 @@ Section HaskFlattener.
       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 ->
@@ -1324,7 +1274,7 @@ Section HaskFlattener.
     intros.
     rewrite mapOptionTree_compose.
     rewrite mapOptionTree_compose.
-    apply flatten_proof.
+    apply flatten_skolemized_proof.
     apply skolemize_proof.
     apply X.
     Defined.