X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskSkolemizer.v;h=bfbdf0eb73f67eb362ba61c4e7af0139de5b3926;hp=c1b570851ac5fb102f0264fbb0256a7fa3d8429b;hb=f6ee1ec88c9b94c62eccbd4119082ae11073a886;hpb=4a32fb619ddda1fedb0855a0c7acad0a41704da8

diff --git a/src/HaskSkolemizer.v b/src/HaskSkolemizer.v
index c1b5708..bfbdf0e 100644
--- a/src/HaskSkolemizer.v
+++ b/src/HaskSkolemizer.v
@@ -66,11 +66,20 @@ Section HaskSkolemizer.
       | 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.
+*)
+  (* 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.
@@ -87,36 +96,32 @@ Section HaskSkolemizer.
         end
     end.
 
-  Definition ite_unit : ∀ Γ, InstantiatedTypeEnv (fun _ => unit) Γ.
-    intros.
-    induction Γ.
-    apply INil.
-    apply ICons; auto.
-    apply tt.
-    Defined.
-
-  Fixpoint grab (n:nat) {T} (l:list T) : T :=
-    match l with
-      | nil  => Prelude_error "grab failed"
-      | h::t => match n with
-                  | 0    => h
-                  | S n' => grab n' t
-                end
-    end.
+  Fixpoint take_trustme {Γ}
+    (n:nat)
+    (l:forall TV, InstantiatedTypeEnv TV Γ -> list (RawHaskType TV ★))
+    : list (HaskType Γ ★) :=
 
-  Fixpoint count' (n:nat)(ln:list nat) : list nat :=
     match n with
-      | 0    => ln
-      | S n' => count' n' (n'::ln)
+      | 0    => nil
+      | S n' => (fun TV ite => match l TV ite with
+                | nil  => Prelude_error "impossible"
+                | a::b => a
+                end)
+                ::
+                take_trustme n' (fun TV ite => match l TV ite with
+                | nil  => Prelude_error "impossible"
+                | a::b => b
+                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 count (n:nat) := count' n nil.
-
-  Definition rebundle {Γ}(X:forall TV, InstantiatedTypeEnv TV Γ -> list (RawHaskType TV ★)) : list (HaskType Γ ★ ) :=
-    map (fun n => fun TV ite => grab n (X TV ite)) (count (length (X _ (ite_unit _)))).
-
-  Definition take_arg_types_as_tree Γ (ht:HaskType Γ ★) :=
-    (unleaves' (rebundle (fun TV ite => (take_arg_types (ht TV ite))))).
+  Definition take_arg_types_as_tree {Γ}(ht:HaskType Γ ★) : Tree ??(HaskType Γ ★ ) :=
+    unleaves_
+    (take_trustme
+      (count_arg_types (ht _ (ite_unit _)))
+      (fun TV ite => take_arg_types (ht TV ite))).
 
   Definition drop_arg_types_as_tree {Γ} (ht:HaskType Γ ★) : HaskType Γ ★ :=
     fun TV ite => drop_arg_types (ht TV ite).
@@ -124,13 +129,47 @@ Section HaskSkolemizer.
   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.
-    unfold take_arg_types_as_tree; simpl.
-    unfold rebundle at 1.
-    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).
@@ -182,6 +221,7 @@ Section HaskSkolemizer.
     left; auto.
     Defined.
 
+  Opaque take_arg_types_as_tree.
   Definition skolemize_proof :
     forall  {h}{c},
       ND Rule  h c ->
@@ -296,17 +336,20 @@ Section HaskSkolemizer.
         apply RGlobal.
 
       destruct case_RLam.
-        simpl.
         destruct lev.
-        apply nd_rule.
-        apply SFlat.
-        apply RLam.
-        rewrite take_works.
+          apply nd_rule.
+          apply SFlat.
+          simpl.
+          apply RLam.
+        simpl.
         rewrite drop_works.
         apply nd_rule.
-        apply SFlat.
-        apply RArrange.
-        apply RCossa.
+          apply SFlat.
+          apply RArrange.
+          eapply RComp.
+          apply RCossa.
+          apply RLeft.
+          apply take_arrange.
 
       destruct case_RCast.
         simpl.
@@ -333,7 +376,6 @@ Section HaskSkolemizer.
         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 ].
@@ -351,8 +393,13 @@ Section HaskSkolemizer.
         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.
@@ -425,5 +472,6 @@ Section HaskSkolemizer.
         simpl.
         apply (Prelude_error "CASE: BIG FIXME").
         Defined.
+  Transparent take_arg_types_as_tree.
 
 End HaskSkolemizer.