more efficient encoding of function types

diff --git a/src/HaskFlattener.v b/src/HaskFlattener.v
index 09f7070..ed3ca43 100644 (file)
--- 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
     | 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 :=
     | 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
             (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 _ _ _ _ _
           | 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
         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 _
           | 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 nd_rule.
       apply RArrange.
       induction r; simpl.

+        apply RId.

         apply RCanL.
         apply RCanR.
         apply RuCanL.
         apply RCanL.
         apply RCanR.
         apply RuCanL.

@@ -852,9 +855,6 @@ Section HaskFlattener.
     apply IHt2.
     Defined.
 
     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)
   Lemma krunk : forall Γ (ec:HaskTyVar Γ ECKind) t,
     flatten_type (<[ ec |- t ]>)
     = @ga_mk Γ (v2t ec)

@@ -864,7 +864,7 @@ Section HaskFlattener.
     unfold flatten_type at 1.
     simpl.
     unfold ga_mk.
     unfold flatten_type at 1.
     simpl.
     unfold ga_mk.

-    apply extensionality.
+    apply phoas_extensionality.

     intros.
     unfold v2t.
     unfold ga_mk_raw.
     intros.
     unfold v2t.
     unfold ga_mk_raw.

@@ -874,9 +874,9 @@ Section HaskFlattener.
     simpl.
     replace (flatten_type (drop_arg_types_as_tree t) tv ite)
       with (drop_arg_types (flatten_rawtype (t tv ite))).
     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)
       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.
               (take_trustme (count_arg_types (t (fun _ : Kind => unit) (ite_unit Γ)))
                  (fun TV : Kind → Type => take_arg_types ○ t TV))))).
     reflexivity.

diff --git a/src/HaskSkolemizer.v b/src/HaskSkolemizer.v
index 2c1c9d2..bfbdf0e 100644 (file)
--- a/src/HaskSkolemizer.v
+++ b/src/HaskSkolemizer.v
@@ -66,11 +66,20 @@ Section HaskSkolemizer.
       | a::b => mkArrows b (a ---> t)
     end.
 
       | a::b => mkArrows b (a ---> t)
     end.
 

+(*

   Fixpoint unleaves_ {Γ}(t:Tree ??(LeveledHaskType Γ ★))(l:list (HaskType Γ ★)) lev : Tree ??(LeveledHaskType Γ ★) :=
     match l with
       | nil  => t
       | a::b => unleaves_ (t,,[a @@ lev]) b lev
     end.
   Fixpoint unleaves_ {Γ}(t:Tree ??(LeveledHaskType Γ ★))(l:list (HaskType Γ ★)) lev : Tree ??(LeveledHaskType Γ ★) :=
     match l with
       | nil  => t
       | a::b => unleaves_ (t,,[a @@ lev]) b lev
     end.

+*)
+  (* weak inverse of "leaves" *)
+  Fixpoint unleaves_ {A:Type}(l:list A) : Tree (option A) :=
+    match l with
+      | nil      => []
+      | (a::nil) => [a]
+      | (a::b)   => [a],,(unleaves_ b)
+    end.

 
   (* rules of skolemized proofs *)
   Definition getΓ (j:Judg) := match j with Γ > _ > _ |- _ => Γ end.
 
   (* rules of skolemized proofs *)
   Definition getΓ (j:Judg) := match j with Γ > _ > _ |- _ => Γ end.

@@ -105,8 +114,11 @@ Section HaskSkolemizer.
                 end)
     end.
                   
                 end)
     end.
                   

+  Axiom phoas_extensionality : forall Γ Q (f g:forall TV, InstantiatedTypeEnv TV Γ -> Q TV),
+    (forall tv ite, f tv ite = g tv ite) -> f=g.
+

   Definition take_arg_types_as_tree {Γ}(ht:HaskType Γ ★) : Tree ??(HaskType Γ ★ ) :=
   Definition take_arg_types_as_tree {Γ}(ht:HaskType Γ ★) : Tree ??(HaskType Γ ★ ) :=

-    unleaves
+    unleaves_

     (take_trustme
       (count_arg_types (ht _ (ite_unit _)))
       (fun TV ite => take_arg_types (ht TV ite))).
     (take_trustme
       (count_arg_types (ht _ (ite_unit _)))
       (fun TV ite => take_arg_types (ht TV ite))).

@@ -117,13 +129,47 @@ Section HaskSkolemizer.
   Implicit Arguments take_arg_types_as_tree [[Γ]].
   Implicit Arguments drop_arg_types_as_tree [[Γ]].
 
   Implicit Arguments take_arg_types_as_tree [[Γ]].
   Implicit Arguments drop_arg_types_as_tree [[Γ]].
 

-  Lemma take_works : forall {Γ}(t1 t2:HaskType Γ ★),
-    take_arg_types_as_tree (t1 ---> t2) = [t1],,(take_arg_types_as_tree t2).
+  Definition take_arrange : forall {Γ} (tx te:HaskType Γ ★) lev,
+    Arrange ([tx @@ lev],, take_arg_types_as_tree te @@@ lev)
+      (take_arg_types_as_tree (tx ---> te) @@@ lev).

     intros.
     intros.

-    unfold take_arg_types_as_tree at 1. 
-    simpl.
-    admit.
-    Qed.
+    destruct (eqd_dec ([tx],, take_arg_types_as_tree te) (take_arg_types_as_tree (tx ---> te))).
+      rewrite <- e.
+      simpl.
+      apply RId.
+    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 phoas_extensionality.
+        reflexivity.
+    apply (Prelude_error "should not be possible").
+    Defined.
+    Transparent take_arg_types_as_tree.
+
+  Definition take_unarrange : forall {Γ} (tx te:HaskType Γ ★) lev,
+    Arrange (take_arg_types_as_tree (tx ---> te) @@@ lev)
+      ([tx @@ lev],, take_arg_types_as_tree te @@@ lev).
+    intros.
+    destruct (eqd_dec ([tx],, take_arg_types_as_tree te) (take_arg_types_as_tree (tx ---> te))).
+      rewrite <- e.
+      simpl.
+      apply RId.
+    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 phoas_extensionality.
+        reflexivity.
+    apply (Prelude_error "should not be possible").
+    Defined.
+    Transparent take_arg_types_as_tree.

 
   Lemma drop_works : forall {Γ}(t1 t2:HaskType Γ ★),
     drop_arg_types_as_tree (t1 ---> t2) = (drop_arg_types_as_tree t2).
 
   Lemma drop_works : forall {Γ}(t1 t2:HaskType Γ ★),
     drop_arg_types_as_tree (t1 ---> t2) = (drop_arg_types_as_tree t2).

@@ -296,12 +342,14 @@ Section HaskSkolemizer.
           simpl.
           apply RLam.
         simpl.
           simpl.
           apply RLam.
         simpl.

-        rewrite take_works.

         rewrite drop_works.
         apply nd_rule.
           apply SFlat.
           apply RArrange.
         rewrite drop_works.
         apply nd_rule.
           apply SFlat.
           apply RArrange.

+          eapply RComp.

           apply RCossa.
           apply RCossa.

+          apply RLeft.
+          apply take_arrange.

 
       destruct case_RCast.
         simpl.
 
       destruct case_RCast.
         simpl.

@@ -328,7 +376,6 @@ Section HaskSkolemizer.
         apply nd_rule.
         apply SFlat.
         apply RApp.
         apply nd_rule.
         apply SFlat.
         apply RApp.

-        rewrite take_works.

         rewrite drop_works.
         set (check_hof tx) as hof_tx.
         destruct hof_tx; [ apply (Prelude_error "attempt tp apply a higher-order function at depth>0") | idtac ].
         rewrite drop_works.
         set (check_hof tx) as hof_tx.
         destruct hof_tx; [ apply (Prelude_error "attempt tp apply a higher-order function at depth>0") | idtac ].

@@ -346,8 +393,13 @@ Section HaskSkolemizer.
         apply SFlat.
         apply RArrange.
         apply RCanR.
         apply SFlat.
         apply RArrange.
         apply RCanR.

-        eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply RArrange; apply RAssoc ].
-        apply nd_rule; apply SFlat; apply RArrange; apply RLeft; eapply RExch.
+        apply nd_rule.
+          apply SFlat.
+          apply RArrange.
+          eapply RComp; [ idtac | eapply RAssoc ].
+          apply RLeft.
+          eapply RComp; [ idtac | apply RExch ].
+          apply take_unarrange.

 
       destruct case_RLet.
         simpl.
 
       destruct case_RLet.
         simpl.