more efficient encoding of function types

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

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
-                               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.
@@ -852,9 +855,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 +864,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 +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))).
-    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.