X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskFlattener.v;h=08485a1307f781e3923c00b53c4c302190dcd45a;hp=90785b0832966abc4ed54714987976618dfd2be9;hb=a9a60dc234f76a4740b32c0f62aa0fe3a89fea83;hpb=c64ac559ed9448b8aa24abedbc2ad5ca800d1d24

diff --git a/src/HaskFlattener.v b/src/HaskFlattener.v
index 90785b0..08485a1 100644
--- a/src/HaskFlattener.v
+++ b/src/HaskFlattener.v
@@ -260,7 +260,7 @@ Section HaskFlattener.
     | TCoerc _ t1 t2 t      => TCoerc    (flatten_rawtype t1) (flatten_rawtype t2) (flatten_rawtype t)
     | TArrow                => TArrow
     | TCode     ec e        => let e' := flatten_rawtype e
-                               in  ga_mk_raw ec (unleaves' (take_arg_types e')) [drop_arg_types e']
+                               in  ga_mk_raw ec (unleaves_ (take_arg_types e')) [drop_arg_types e']
     | TyFunApp  tfc kl k lt => TyFunApp tfc kl k (flatten_rawtype_list _ lt)
     end
     with flatten_rawtype_list {TV}(lk:list Kind)(exp:@RawHaskTypeList TV lk) : @RawHaskTypeList TV lk :=
@@ -371,8 +371,8 @@ Section HaskFlattener.
     ND Rule []                          [ Γ > Δ > [x@@lev] |- [y@@lev] ] ->
     ND Rule [ Γ > Δ > ant |- [x@@lev] ] [ Γ > Δ > ant      |- [y@@lev] ].
     intros.
-    eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanL ].
-    eapply nd_comp; [ idtac | eapply nd_rule; apply (@RLet Γ Δ [] ant y x lev) ].
+    eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanR ].
+    eapply nd_comp; [ idtac | eapply nd_rule; apply RLet ].
     eapply nd_comp; [ apply nd_rlecnac | idtac ].
     apply nd_prod.
     apply nd_id.
@@ -380,141 +380,117 @@ Section HaskFlattener.
       apply X.
       eapply nd_rule.
       eapply RArrange.
-      apply RuCanL.
-      Defined.
-
-  Definition postcompose' : ∀ Γ Δ ec lev a b c Σ,
-     ND Rule [] [ Γ > Δ > Σ                        |- [@ga_mk Γ ec a b @@ lev] ] ->
-     ND Rule [] [ Γ > Δ > Σ,,[@ga_mk Γ ec b c @@ lev] |- [@ga_mk Γ ec a c @@ lev] ].
-     intros.
-     eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RExch ].
-     eapply nd_comp; [ idtac
-       | eapply nd_rule; apply (@RLet Γ Δ [@ga_mk _ ec b c @@lev] Σ (@ga_mk _ ec a c) (@ga_mk _ ec a b) lev) ].
-     eapply nd_comp; [ apply nd_llecnac | idtac ].
-     apply nd_prod.
-     apply X.
-     eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RExch ].
-     apply ga_comp.
-     Defined.
+      apply RuCanR.
+    Defined.
 
   Definition precompose Γ Δ ec : forall a x y z lev,
     ND Rule
       [ Γ > Δ > a                           |- [@ga_mk _ ec y z @@ lev] ]
       [ Γ > Δ > a,,[@ga_mk _ ec x y @@ lev] |- [@ga_mk _ ec x z @@ lev] ].
     intros.
-    eapply nd_comp.
-    apply nd_rlecnac.
-    eapply nd_comp.
-    eapply nd_prod.
+    eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
+    eapply nd_comp; [ apply nd_rlecnac | idtac ].
+    apply nd_prod.
     apply nd_id.
-    eapply ga_comp.
-
-    eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RExch ].
-
-    apply nd_rule.
-    apply RLet.
+    eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RExch ].
+    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 precompose' Γ Δ ec : forall a b x y z lev,
+    ND Rule
+      [ Γ > Δ > a,,b                             |- [@ga_mk _ ec y z @@ lev] ]
+      [ Γ > Δ > a,,([@ga_mk _ ec x y @@ lev],,b) |- [@ga_mk _ ec x z @@ lev] ].
+    intros.
+    eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RLeft; eapply RExch ].
+    eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCossa ].
+    apply precompose.
+    Defined.
 
-  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 postcompose_ Γ Δ ec : forall a x y z lev,
+    ND Rule
+      [ Γ > Δ > a                           |- [@ga_mk _ ec x y @@ lev] ]
+      [ Γ > Δ > a,,[@ga_mk _ ec y z @@ lev] |- [@ga_mk _ ec x z @@ lev] ].
+    intros.
+    eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
+    eapply nd_comp; [ apply nd_rlecnac | idtac ].
+    apply nd_prod.
+    apply nd_id.
+    apply ga_comp.
+    Defined.
 
-  Definition 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 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 postcompose_ ].
     apply X.
-    eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RuCanL ].
-    apply ga_first.
     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 first_nd : ∀ Γ Δ ec lev a b c Σ,
+    ND Rule [ Γ > Δ > Σ                    |- [@ga_mk Γ ec a b @@ lev] ]
+            [ Γ > Δ > Σ                    |- [@ga_mk Γ ec (a,,c) (b,,c) @@ lev] ].
     intros.
-    eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanL ].
+    eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanR ].
     eapply nd_comp; [ idtac | eapply nd_rule; apply RLet ].
-    eapply nd_comp; [ apply nd_llecnac | idtac ].
+    eapply nd_comp; [ apply nd_rlecnac | idtac ].
     apply nd_prod.
-    apply X.
-    eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RuCanL ].
-    apply ga_second.
+    apply nd_id.
+    eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RuCanR ].
+    apply ga_first.
     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 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.
-    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''.
+    apply X.
+    apply first_nd.
+    Defined.
 
-    idtac.
-    clear q'' q'.
-    eapply nd_comp.
-    apply nd_rlecnac.
+  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 RCanR ].
+    eapply nd_comp; [ idtac | eapply nd_rule; 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 RuCanR ].
+    apply ga_second.
     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 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; [ idtac | eapply nd_rule; 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; [ apply nd_llecnac | idtac ].
-    apply nd_prod.
-    apply postcompose.
-    apply ga_uncancell.
-    apply precompose.
+    eapply nd_comp.
+    apply X.
+    apply second_nd.
     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)").
-    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 RExch ].
+     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; [ idtac | eapply nd_rule; eapply RLet ].
+     eapply nd_comp; [ apply nd_llecnac | idtac ].
+     apply nd_prod.
+     apply postcompose.
+     apply ga_uncancell.
+     eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RExch ].
+     apply precompose.
+     Defined.
 
   (* useful for cutting down on the pretty-printed noise
   
@@ -538,6 +514,7 @@ Section HaskFlattener.
             (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) B))
             (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) A)) @@ nil]]
           with
+          | RId  a               => let case_RId := tt    in ga_id _ _ _ _ _
           | RCanL  a             => let case_RCanL := tt  in ga_uncancell _ _ _ _ _
           | RCanR  a             => let case_RCanR := tt  in ga_uncancelr _ _ _ _ _
           | RuCanL a             => let case_RuCanL := tt in ga_cancell _ _ _ _ _
@@ -558,17 +535,17 @@ Section HaskFlattener.
           set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) c)) as c' in *.
           eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RCanL ].
           eapply nd_comp; [ idtac | eapply nd_rule; apply
-             (@RLet Γ Δ [] [] (@ga_mk _ (v2t ec) a' c') (@ga_mk _ (v2t ec) a' b')) ].
+             (@RLet Γ Δ [] [] (@ga_mk _ (v2t ec) a' b') (@ga_mk _ (v2t ec) a' c')) ].
           eapply nd_comp; [ apply nd_llecnac | idtac ].
           apply nd_prod.
           apply r2'.
-          eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RuCanL ].
-          eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RCanR ].
-          eapply nd_comp; [ idtac | eapply nd_rule;  apply 
-            (@RLet Γ Δ [@ga_mk _ (v2t ec) a' b' @@ _] [] (@ga_mk _ (v2t ec) a' c') (@ga_mk _ (v2t ec) b' c'))].
+          eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RuCanR ].
+          eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RCanL ].
+          eapply nd_comp; [ idtac | eapply nd_rule;  apply RLet ].
           eapply nd_comp; [ apply nd_llecnac | idtac ].
           eapply nd_prod.
           apply r1'.
+          eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RExch ].
           apply ga_comp.
           Defined.
 
@@ -592,6 +569,7 @@ Section HaskFlattener.
         match r as R in Arrange A B return
           Arrange (mapOptionTree (flatten_leveled_type ) (drop_lev _ A))
           (mapOptionTree (flatten_leveled_type ) (drop_lev _ B)) with
+          | RId  a               => let case_RId := tt  in RId _
           | RCanL  a             => let case_RCanL := tt  in RCanL _
           | RCanR  a             => let case_RCanR := tt  in RCanR _
           | RuCanL a             => let case_RuCanL := tt in RuCanL _
@@ -621,13 +599,14 @@ Section HaskFlattener.
       apply nd_rule.
       apply RArrange.
       induction r; simpl.
+        apply RId.
         apply RCanL.
         apply RCanR.
         apply RuCanL.
         apply RuCanR.
         apply RAssoc.
         apply RCossa.
-        apply RExch.
+        apply RExch.    (* TO DO: check for all-leaf trees here *)
         apply RWeak.
         apply RCont.
         apply RLeft; auto.
@@ -645,29 +624,32 @@ Section HaskFlattener.
     intro pfa.
     intro pfb.
     apply secondify with (c:=a)  in pfb.
-    eapply nd_comp.
-    Focus 2.
+    apply firstify  with (c:=[])  in pfa.
     eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
     eapply nd_comp; [ eapply nd_llecnac | idtac ].
-    eapply nd_prod.
-    apply pfb.
-    clear pfb.
-    apply postcompose'.
-    eapply nd_comp.
+    apply nd_prod.
     apply pfa.
     clear pfa.
-    apply boost.
+
+    eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
+    eapply nd_comp; [ apply nd_llecnac | idtac ].
+    apply nd_prod.
     eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanL ].
-    apply precompose'.
+    eapply nd_comp; [ idtac | eapply postcompose_ ].
     apply ga_uncancelr.
-    apply nd_id.
+
+    eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RExch ].
+    eapply nd_comp; [ idtac | eapply precompose ].
+    apply pfb.
     Defined.
 
   Definition arrange_brak : forall Γ Δ ec succ t,
    ND Rule
-     [Γ > Δ > mapOptionTree (flatten_leveled_type ) (drop_lev (ec :: nil) succ),,
-      [(@ga_mk _ (v2t ec) [] (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: nil) succ))) @@  nil] |- [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.
@@ -679,6 +661,7 @@ Section HaskFlattener.
     apply y.
     idtac.
     clear y q.
+    eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RExch ].
     simpl.
     eapply nd_comp; [ apply nd_llecnac | idtac ].
     eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
@@ -719,24 +702,117 @@ Section HaskFlattener.
       apply IHsucc2.
     Defined.
 
+  Definition arrange_empty_tree : forall {T}{A}(q:Tree A)(t:Tree ??T),
+    t = mapTree (fun _:A => None) q ->
+    Arrange t [].
+    intros T A q.
+    induction q; intros.
+      simpl in H.
+      rewrite H.
+      apply RId.
+    simpl in *.
+    destruct t; try destruct o; inversion H.
+      set (IHq1 _ H1) as x1.
+      set (IHq2 _ H2) as x2.
+      eapply RComp.
+        eapply RRight.
+        rewrite <- H1.
+        apply x1.
+      eapply RComp.
+        apply RCanL.
+        rewrite <- H2.
+        apply x2.
+      Defined.
+
+(*  Definition unarrange_empty_tree : forall {T}{A}(t:Tree ??T)(q:Tree A),
+    t = mapTree (fun _:A => None) q ->
+    Arrange [] t.
+  Defined.*)
+
+  Definition decide_tree_empty : forall {T:Type}(t:Tree ??T),
+    sum { q:Tree unit & t = mapTree (fun _ => None) q } unit.
+    intro T.
+    refine (fix foo t :=
+      match t with
+        | T_Leaf x => _
+        | T_Branch b1 b2 => let b1' := foo b1 in let b2' := foo b2 in _
+      end).
+    intros.
+    destruct x.
+    right; apply tt.
+    left.
+      exists (T_Leaf tt).
+      auto.
+    destruct b1'.
+    destruct b2'.
+    destruct s.
+    destruct s0.
+    subst.
+    left.
+    exists (x,,x0).
+    reflexivity.
+    right; auto.
+    right; auto.
+    Defined.
+
   Definition arrange_esc : forall Γ Δ ec succ t,
    ND Rule
      [Γ > Δ > mapOptionTree (flatten_leveled_type ) succ |- [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]].
+     [Γ > Δ > 
+      [(@ga_mk _ (v2t ec) [] (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: nil) succ))) @@  nil],,
+      mapOptionTree (flatten_leveled_type ) (drop_lev (ec :: nil) succ)  |- [t @@  nil]].
     intros.
-    unfold drop_lev.
     set (@arrange _ succ (levelMatch (ec::nil))) as q.
+    set (@drop_lev Γ (ec::nil) succ) as q'.
+    assert (@drop_lev Γ (ec::nil) succ=q') as H.
+      reflexivity.
+    unfold drop_lev in H.
+    unfold mkDropFlags in H.
+    rewrite H in q.
+    clear H.
     set (arrangeMap _ _ flatten_leveled_type q) as y.
     eapply nd_comp.
     eapply nd_rule.
     eapply RArrange.
     apply y.
-    idtac.
     clear y q.
 
+    set (mapOptionTree flatten_leveled_type (dropT (mkFlags (liftBoolFunc false (bnot ○ levelMatch (ec :: nil))) succ))) as q.
+    destruct (decide_tree_empty q); [ idtac | apply (Prelude_error "escapifying open code not yet supported") ].
+    destruct s.
+
+    simpl.
+    eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RExch ].
+    set (fun z z' => @RLet Γ Δ z (mapOptionTree flatten_leveled_type q') t z' nil) as q''.
+    eapply nd_comp; [ idtac | eapply nd_rule; apply RLet ].
+    clear q''.
+    eapply nd_comp; [ apply nd_rlecnac | idtac ].
+    apply nd_prod.
+    apply nd_rule.
+    apply RArrange.
+    eapply RComp; [ idtac | apply RCanR ].
+    apply RLeft.
+    apply (@arrange_empty_tree _ _ _ _ e).
+   
+    eapply nd_comp.
+      eapply nd_rule.
+      eapply (@RVar Γ Δ t nil).
+    apply nd_rule.
+      apply RArrange.
+      eapply RComp.
+      apply RuCanR.
+      apply RLeft.
+      apply RWeak.
+(*
+    eapply decide_tree_empty.
+
+    simpl.
+    set (dropT (mkFlags (liftBoolFunc false (bnot ○ levelMatch (ec :: nil))) succ)) as escapified.
+    destruct (decide_tree_empty escapified).
+
     induction succ.
     destruct a.
+      unfold drop_lev.
       destruct l.
       simpl.
       unfold mkDropFlags; simpl.
@@ -760,6 +836,7 @@ Section HaskFlattener.
         apply RLeft.
         apply RWeak.
       apply (Prelude_error "escapifying code with multi-leaf antecedents is not supported").
+*)
       Defined.
 
   Lemma mapOptionTree_distributes
@@ -768,32 +845,6 @@ Section HaskFlattener.
     reflexivity.
     Qed.
 
-  Definition decide_tree_empty : forall {T:Type}(t:Tree ??T),
-    sum { q:Tree unit & t = mapTree (fun _ => None) q } unit.
-    intro T.
-    refine (fix foo t :=
-      match t with
-        | T_Leaf x => _
-        | T_Branch b1 b2 => let b1' := foo b1 in let b2' := foo b2 in _
-      end).
-    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.
-
   Lemma unlev_relev : forall {Γ}(t:Tree ??(HaskType Γ ★)) lev, mapOptionTree unlev (t @@@ lev) = t.
     intros.
     induction t.
@@ -803,52 +854,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 RId.
     simpl.
-    apply RCanR.
+    apply RId.
+    eapply RComp; [ idtac | apply RCanL ].
+    eapply RComp; [ idtac | eapply RLeft; apply IHt2 ].
     Opaque drop_lev.
     simpl.
     Transparent drop_lev.
+    idtac.
     drop_simplify.
-    simpl.
-    eapply RComp.
-    eapply RComp.
-    eapply RAssoc.
-    eapply RRight.
+    apply RRight.
     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 RId.
     simpl.
-    apply RuCanR.
+    apply RId.
+    eapply RComp; [ apply RuCanL | idtac ].
+    eapply RComp; [ eapply RRight; 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 RLeft.
     apply IHt2.
     Defined.
 
@@ -857,13 +901,34 @@ Section HaskFlattener.
     = @ga_mk Γ (v2t ec)
     (mapOptionTree flatten_type (take_arg_types_as_tree t))
     [ flatten_type (drop_arg_types_as_tree   t)].
-
     intros.
     unfold flatten_type at 1.
     simpl.
     unfold ga_mk.
+    apply phoas_extensionality.
+    intros.
     unfold v2t.
-    admit. (* BIG HUGE CHEAT FIXME *)
+    unfold ga_mk_raw.
+    unfold ga_mk_tree.
+    rewrite <- mapOptionTree_compose.
+    unfold take_arg_types_as_tree.
+    simpl.
+    replace (flatten_type (drop_arg_types_as_tree t) tv ite)
+      with (drop_arg_types (flatten_rawtype (t tv ite))).
+    replace (unleaves_ (take_arg_types (flatten_rawtype (t tv ite))))
+      with ((mapOptionTree (fun x : HaskType Γ ★ => flatten_type x tv ite)
+           (unleaves_
+              (take_trustme (count_arg_types (t (fun _ : Kind => unit) (ite_unit Γ)))
+                 (fun TV : Kind → Type => take_arg_types ○ t TV))))).
+    reflexivity.
+    unfold flatten_type.
+    clear hetmet_flatten.
+    clear hetmet_unflatten.
+    clear hetmet_id.
+    clear gar.
+    set (t tv ite) as x.
+    admit.
+    admit.
     Qed.
 
   Definition flatten_proof :
@@ -898,6 +963,7 @@ Section HaskFlattener.
       | RAbsCo   Γ Δ Σ κ σ  σ₁ σ₂  lev => let case_RAbsCo := tt        in _
       | RApp     Γ Δ Σ₁ Σ₂ tx te lev   => let case_RApp := tt          in _
       | RLet     Γ Δ Σ₁ Σ₂ σ₁ σ₂ lev   => let case_RLet := tt          in _
+      | RWhere   Γ Δ Σ₁ Σ₂ Σ₃ σ₁ σ₂ lev   => let case_RWhere := tt          in _
       | RJoin    Γ p lri m x q         => let case_RJoin := tt in _
       | RVoid    _ _                   => let case_RVoid := tt   in _
       | RBrak    Γ Δ t ec succ lev           => let case_RBrak := tt         in _
@@ -1039,22 +1105,51 @@ Section HaskFlattener.
       repeat take_simplify.
       simpl.
 
+      set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) Σ₁)) as Σ₁'.
+      set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) Σ₂)) as Σ₂'.
+      set (mapOptionTree flatten_leveled_type (drop_lev (ec :: lev) Σ₁)) as Σ₁''.
+      set (mapOptionTree flatten_leveled_type (drop_lev (ec :: lev) Σ₂)) as Σ₂''.
+
       eapply nd_comp.
       eapply nd_prod; [ idtac | apply nd_id ].
       eapply boost.
-      apply ga_second.
+      apply (ga_first _ _ _ _ _ _ Σ₂').
 
-      eapply nd_comp.
-      eapply nd_prod.
+      eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
+      apply nd_prod.
       apply nd_id.
+      eapply nd_comp; [ eapply nd_rule; eapply RArrange; eapply RCanL | idtac ].
+      eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RExch (* okay *)].
+      apply precompose.
+
+    destruct case_RWhere.
+      simpl.
+      destruct lev as [|ec lev]; simpl; [ apply nd_rule; apply RWhere; auto | idtac ].
+      repeat take_simplify.
+      repeat drop_simplify.
+      simpl.
+
+      set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) Σ₁)) as Σ₁'.
+      set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) Σ₂)) as Σ₂'.
+      set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) Σ₃)) as Σ₃'.
+      set (mapOptionTree flatten_leveled_type (drop_lev (ec :: lev) Σ₁)) as Σ₁''.
+      set (mapOptionTree flatten_leveled_type (drop_lev (ec :: lev) Σ₂)) as Σ₂''.
+      set (mapOptionTree flatten_leveled_type (drop_lev (ec :: lev) Σ₃)) as Σ₃''.
+
       eapply nd_comp.
-      eapply nd_rule.
-      eapply RArrange.
-      apply RCanR.
-      eapply precompose.
+      eapply nd_prod; [ eapply nd_id | idtac ].
+      eapply (first_nd _ _ _ _ _ _ Σ₃').
+      eapply nd_comp.
+      eapply nd_prod; [ eapply nd_id | idtac ].
+      eapply (second_nd _ _ _ _ _ _ Σ₁').
 
+      eapply nd_comp; [ idtac | eapply nd_rule; eapply RWhere ].
+      apply nd_prod; [ idtac | apply nd_id ].
+      eapply nd_comp; [ idtac | eapply precompose' ].
       apply nd_rule.
-      apply RLet.
+      apply RArrange.
+      apply RLeft.
+      apply RCanL.
 
     destruct case_RVoid.
       simpl.
@@ -1125,8 +1220,29 @@ Section HaskFlattener.
 
     destruct case_RLetRec.
       rename t into lev.
+      simpl. destruct lev; simpl.
+      replace (getjlev (y @@@ nil)) with (nil: (HaskLevel Γ)).
+      replace (mapOptionTree flatten_leveled_type (y @@@ nil))
+        with  ((mapOptionTree flatten_type y) @@@ nil).
+      unfold flatten_leveled_type at 2.
+      simpl.
+      unfold flatten_leveled_type at 3.
       simpl.
-      apply (Prelude_error "LetRec not supported (FIXME)").
+      apply nd_rule.
+      set (@RLetRec Γ Δ (mapOptionTree flatten_leveled_type lri) (flatten_type x) (mapOptionTree flatten_type y) nil) as q.
+      simpl in q.
+      apply q.
+        induction y; try destruct a; auto.
+        simpl.
+        rewrite IHy1.
+        rewrite IHy2.
+        reflexivity.
+        induction y; try destruct a; auto.
+        simpl.
+        rewrite <- IHy1.
+        rewrite <- IHy2.
+        reflexivity.
+      apply (Prelude_error "LetRec not supported inside brackets yet (FIXME)").
 
     destruct case_RCase.
       simpl.
@@ -1151,11 +1267,15 @@ Section HaskFlattener.
       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 RLeft; apply tree_of_nothing | idtac ].
+      eapply nd_comp; [ eapply nd_rule; eapply RArrange; eapply RCanR | idtac ].
+      refine (ga_unkappa Γ Δ (v2t ec) nil _ _ _ _ ;; _).
+      eapply nd_comp; [ idtac | eapply arrange_brak ].
       unfold succ_host.
       unfold succ_guest.
-      apply arrange_brak.
+      eapply nd_rule.
+        eapply RArrange.
+        apply RExch.
       apply (Prelude_error "found Brak at depth >0 indicating 3-level code; only two-level code is currently supported").
 
     destruct case_SEsc.
@@ -1169,7 +1289,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 RLeft; apply tree_of_nothing' ].
+      eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanR ].
       simpl.
       rewrite take_lemma'.
       rewrite unlev_relev.
@@ -1185,13 +1306,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 RArrange; apply RuCanR ].
+      eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RuCanR ].
+      eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RCanL ].
       eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
       eapply nd_comp; [ apply nd_llecnac | idtac ].
       apply nd_prod; [ idtac | eapply boost ].
       induction x.
         apply ga_id.
-        eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanR ].
+        eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanL ].
         simpl.
         apply ga_join.
           apply IHx1.
@@ -1216,7 +1339,7 @@ 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").