HaskFlattener: support escapifying multi-leaf contexts
[coq-hetmet.git] / src / HaskFlattener.v
index 09f7070..a5f4261 100644 (file)
@@ -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 :=
@@ -538,6 +538,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 _ _ _ _ _
@@ -592,6 +593,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,6 +623,7 @@ Section HaskFlattener.
       apply nd_rule.
       apply RArrange.
       induction r; simpl.
+        apply RId.
         apply RCanL.
         apply RCanR.
         apply RuCanL.
@@ -719,24 +722,116 @@ 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]].
     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 q'' ].
+    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 RuCanL.
+      apply RRight.
+      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 +855,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 +864,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.
@@ -852,9 +922,6 @@ Section HaskFlattener.
     apply IHt2.
     Defined.
 
-  Axiom extensionality : forall Γ Q (f g:forall TV, InstantiatedTypeEnv TV Γ -> Q TV),
-    (forall tv ite, f tv ite = g tv ite) -> f=g.
-
   Lemma krunk : forall Γ (ec:HaskTyVar Γ ECKind) t,
     flatten_type (<[ ec |- t ]>)
     = @ga_mk Γ (v2t ec)
@@ -864,7 +931,7 @@ Section HaskFlattener.
     unfold flatten_type at 1.
     simpl.
     unfold ga_mk.
-    apply extensionality.
+    apply phoas_extensionality.
     intros.
     unfold v2t.
     unfold ga_mk_raw.
@@ -874,9 +941,9 @@ Section HaskFlattener.
     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))))
+    replace (unleaves_ (take_arg_types (flatten_rawtype (t tv ite))))
       with ((mapOptionTree (fun x : HaskType Γ ★ => flatten_type x tv ite)
-           (unleaves
+           (unleaves_
               (take_trustme (count_arg_types (t (fun _ : Kind => unit) (ite_unit Γ)))
                  (fun TV : Kind → Type => take_arg_types ○ t TV))))).
     reflexivity.