first draft of skolemization pass
authorAdam Megacz <megacz@cs.berkeley.edu>
Fri, 13 May 2011 07:36:09 +0000 (00:36 -0700)
committerAdam Megacz <megacz@cs.berkeley.edu>
Fri, 13 May 2011 07:36:09 +0000 (00:36 -0700)
src/HaskFlattener.v
src/HaskSkolemizer.v [new file with mode: 0644]

index cd5bd57..46e6af5 100644 (file)
@@ -30,6 +30,8 @@ Require Import HaskStrongToProof.
 Require Import HaskProofToStrong.
 Require Import HaskWeakToStrong.
 
+Require Import HaskSkolemizer.
+
 Open Scope nd_scope.
 Set Printing Width 130.
 
@@ -165,10 +167,39 @@ Section HaskFlattener.
     auto.
     Qed.
 
+  Lemma take_lemma' : forall Γ (lev:HaskLevel Γ) x, take_lev lev (x @@@ lev) = x @@@ lev.
+    intros.
+    induction x.
+    destruct a; simpl; try reflexivity.
+    apply take_lemma.
+    simpl.
+    rewrite <- IHx1 at 2.
+    rewrite <- IHx2 at 2.
+    reflexivity.
+    Qed.
+(*
+  Lemma drop_lev_lemma' : forall Γ (lev:HaskLevel Γ) x, drop_lev lev (x @@@ lev) = [].
+    intros.
+    induction x.
+    destruct a; simpl; try reflexivity.
+    apply drop_lev_lemma.
+    simpl.
+    change (@drop_lev _ lev (x1 @@@ lev ,, x2 @@@ lev))
+      with ((@drop_lev _ lev (x1 @@@ lev)) ,, (@drop_lev _ lev (x2 @@@ lev))).
+    simpl.
+    rewrite IHx1.
+    rewrite IHx2.
+    reflexivity.
+    Qed.
+*)
   Ltac drop_simplify :=
     match goal with
       | [ |- context[@drop_lev ?G ?L [ ?X @@ ?L ] ] ] =>
         rewrite (drop_lev_lemma G L X)
+(*
+      | [ |- context[@drop_lev ?G ?L [ ?X @@@ ?L ] ] ] =>
+        rewrite (drop_lev_lemma' G L X)
+*)
       | [ |- context[@drop_lev ?G (?E :: ?L) [ ?X @@ (?E :: ?L) ] ] ] =>
         rewrite (drop_lev_lemma_s G L E X)
       | [ |- context[@drop_lev ?G ?N (?A,,?B)] ] =>
@@ -181,6 +212,8 @@ Section HaskFlattener.
     match goal with
       | [ |- context[@take_lev ?G ?L [ ?X @@ ?L ] ] ] =>
         rewrite (take_lemma G L X)
+      | [ |- context[@take_lev ?G ?L [ ?X @@@ ?L ] ] ] =>
+        rewrite (take_lemma' G L X)
       | [ |- context[@take_lev ?G ?N (?A,,?B)] ] =>
       change (@take_lev G N (A,,B)) with ((@take_lev G N A),,(@take_lev G N B))
       | [ |- context[@take_lev ?G ?N (T_Leaf None)] ] =>
@@ -226,7 +259,8 @@ Section HaskFlattener.
     | TCon       tc         => TCon      tc
     | TCoerc _ t1 t2 t      => TCoerc    (flatten_rawtype t1) (flatten_rawtype t2) (flatten_rawtype t)
     | TArrow                => TArrow
-    | TCode     ec e        => ga_mk_raw ec [] [flatten_rawtype e]
+    | TCode     ec e        => let e' := flatten_rawtype 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 :=
@@ -240,12 +274,12 @@ Section HaskFlattener.
 
   Fixpoint levels_to_tcode {Γ}(ht:HaskType Γ ★)(lev:HaskLevel Γ) : HaskType Γ ★ :=
     match lev with
-      | nil      => ht
-      | ec::lev' => fun TV ite => TCode (v2t ec TV ite) (levels_to_tcode ht lev' TV ite)
+      | nil      => flatten_type ht
+      | ec::lev' => @ga_mk _ (v2t ec) [] [levels_to_tcode ht lev']
     end.
 
   Definition flatten_leveled_type {Γ}(ht:LeveledHaskType Γ ★) : LeveledHaskType Γ ★ :=
-    flatten_type (levels_to_tcode (unlev ht) (getlev ht)) @@ nil.
+    levels_to_tcode (unlev ht) (getlev ht) @@ nil.
 
   (* AXIOMS *)
 
@@ -428,15 +462,15 @@ Section HaskFlattener.
     apply ga_second.
     Defined.
 
-  Lemma ga_unkappa     : ∀ Γ Δ ec l a b Σ,
+  Lemma ga_unkappa     : ∀ Γ Δ ec l z a b Σ,
     ND Rule
-    [Γ > Δ > Σ |- [@ga_mk Γ ec a  b @@ l] ] 
-    [Γ > Δ > Σ,,[@ga_mk Γ ec [] a @@ l] |- [@ga_mk Γ ec [] b @@ l] ].
+    [Γ > Δ > Σ                         |- [@ga_mk Γ ec a b @@ l] ] 
+    [Γ > Δ > Σ,,[@ga_mk Γ ec z a @@ l] |- [@ga_mk Γ ec z b @@ l] ].
     intros.
-    set (ga_comp Γ Δ ec l [] a b) as q.
+    set (ga_comp Γ Δ ec l z a b) as q.
 
     set (@RLet Γ Δ) as q'.
-    set (@RLet Γ Δ [@ga_mk _ ec [] a @@ l] Σ (@ga_mk _ ec [] b) (@ga_mk _ ec a b) l) 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.
@@ -457,6 +491,31 @@ Section HaskFlattener.
     apply q.
     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 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.
+    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.
+
   (* useful for cutting down on the pretty-printed noise
   
   Notation "`  x" := (take_lev _ x) (at level 20).
@@ -607,10 +666,8 @@ Section HaskFlattener.
   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] |- [(@ga_mk _ (v2t ec) [] [flatten_type  t]) @@  nil]]
-     [Γ > Δ > mapOptionTree (flatten_leveled_type ) succ |- [(@ga_mk _ (v2t ec) [] [flatten_type  t]) @@  nil]].
+      [(@ga_mk _ (v2t ec) [] (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: nil) succ))) @@  nil] |- [t @@ nil]]
+     [Γ > Δ > mapOptionTree (flatten_leveled_type ) succ |- [t @@  nil]].
     intros.
     unfold drop_lev.
     set (@arrange' _ succ (levelMatch (ec::nil))) as q.
@@ -648,6 +705,9 @@ Section HaskFlattener.
     unfold flatten_leveled_type.
     simpl.
     unfold flatten_type.
+    simpl.
+    unfold ga_mk.
+    simpl.
     apply RVar.
     simpl.
     apply ga_id.
@@ -661,11 +721,9 @@ Section HaskFlattener.
 
   Definition arrange_esc : forall Γ Δ ec succ t,
    ND Rule
-     [Γ > Δ > mapOptionTree (flatten_leveled_type ) succ |- [(@ga_mk _ (v2t ec) [] [flatten_type  t]) @@  nil]]
+     [Γ > Δ > 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]
-      |- [(@ga_mk _ (v2t ec) [] [flatten_type  t]) @@  nil]].
+      [(@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.
@@ -736,17 +794,97 @@ Section HaskFlattener.
     right; auto.
     Defined.
 
+  Lemma unlev_relev : forall {Γ}(t:Tree ??(HaskType Γ ★)) lev, mapOptionTree unlev (t @@@ lev) = t.
+    intros.
+    induction t.
+    destruct a; reflexivity.
+    rewrite <- IHt1 at 2.
+    rewrite <- IHt2 at 2.
+    reflexivity.
+    Qed.
+
+  Lemma tree_of_nothing : forall Γ ec t a,
+    Arrange (a,,mapOptionTree flatten_leveled_type (drop_lev(Γ:=Γ) (ec :: nil) (t @@@ (ec :: nil)))) a.
+    intros.
+    induction t; try destruct o; try destruct a0.
+    simpl.
+    drop_simplify.
+    simpl.
+    apply RCanR.
+    simpl.
+    apply RCanR.
+    Opaque drop_lev.
+    simpl.
+    Transparent drop_lev.
+    drop_simplify.
+    simpl.
+    eapply RComp.
+    eapply RComp.
+    eapply RAssoc.
+    eapply 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)))).
+    intros.
+    induction t; try destruct o; try destruct a0.
+    simpl.
+    drop_simplify.
+    simpl.
+    apply RuCanR.
+    simpl.
+    apply RuCanR.
+    Opaque drop_lev.
+    simpl.
+    Transparent drop_lev.
+    drop_simplify.
+    simpl.
+    eapply RComp.
+    Focus 2.
+    eapply RComp.
+    Focus 2.
+    eapply RCossa.
+    Focus 2.
+    eapply RRight.
+    apply IHt1.
+    apply IHt2.
+    Defined.
+
+  Lemma krunk : forall Γ (ec:HaskTyVar Γ ECKind) t,
+    flatten_type (<[ ec |- t ]>)
+    = @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.
+    unfold v2t.
+    admit. (* BIG HUGE CHEAT FIXME *)
+    Qed.
+
   Definition flatten_proof :
     forall  {h}{c},
-      ND Rule h c ->
-      ND Rule (mapOptionTree (flatten_judgment ) h) (mapOptionTree (flatten_judgment ) c).
+      ND SRule h c ->
+      ND  Rule (mapOptionTree (flatten_judgment ) h) (mapOptionTree (flatten_judgment ) c).
     intros.
     eapply nd_map'; [ idtac | apply X ].
     clear h c X.
     intros.
     simpl in *.
 
-    refine (match X as R in Rule H C with
+    refine 
+      (match X as R in SRule H C with
+      | SBrak    Γ Δ t ec succ lev           => let case_SBrak := tt         in _
+      | SEsc     Γ Δ t ec succ lev           => let case_SEsc := tt          in _
+      | SFlat    h c r                       => let case_SFlat := tt         in _
+      end).
+
+    destruct case_SFlat.
+    refine (match r as R in Rule H C with
       | RArrange Γ Δ a b x d           => let case_RArrange := tt      in _
       | RNote    Γ Δ Σ τ l n           => let case_RNote := tt         in _
       | RLit     Γ Δ l     _           => let case_RLit := tt          in _
@@ -772,46 +910,10 @@ Section HaskFlattener.
       apply (flatten_arrangement''  Γ Δ a b x d).
 
     destruct case_RBrak.
-      simpl.
-      destruct lev.
-      change ([flatten_type  (<[ ec |- t ]>) @@  nil])
-        with ([ga_mk (v2t ec) [] [flatten_type  t] @@  nil]).
-      refine (ga_unkappa Γ Δ (v2t ec) nil (mapOptionTree (flatten_type ○ unlev) (take_lev (ec::nil) succ)) _
-        (mapOptionTree (flatten_leveled_type) (drop_lev (ec::nil) succ)) ;; _ ).
-      apply arrange_brak.
-      apply (Prelude_error "found Brak at depth >0 indicating 3-level code; only two-level code is currently supported").
+      apply (Prelude_error "found unskolemized Brak rule; this shouldn't happen").
 
     destruct case_REsc.
-      simpl.
-      destruct lev.
-      simpl.
-      change ([flatten_leveled_type (<[ ec |- t ]> @@  nil)])
-        with ([ga_mk (v2t ec) [] [flatten_type  t] @@  nil]).
-      eapply nd_comp; [ apply arrange_esc | idtac ].
-      set (decide_tree_empty (take_lev (ec :: nil) succ)) as q'.
-      destruct q'.
-      destruct s.
-      rewrite e.
-      clear e.
-
-      eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanR ].
-      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 ].
-      simpl.
-      apply ga_join.
-      apply IHx1.
-      apply IHx2.
-      simpl.
-      apply postcompose.
-      apply ga_drop.
-
-      (* environment has non-empty leaves *)
-      apply (ga_kappa Γ Δ (v2t ec) nil (mapOptionTree (flatten_type ○ unlev) (take_lev (ec::nil) succ)) _ _).
-      apply (Prelude_error "found Esc at depth >0 indicating 3-level code; only two-level code is currently supported").
+      apply (Prelude_error "found unskolemized Esc rule; this shouldn't happen").
       
     destruct case_RNote.
       simpl.
@@ -889,6 +991,7 @@ Section HaskFlattener.
     destruct case_RCast.
       simpl.
       destruct lev as [|ec lev]; simpl; [ apply nd_rule; apply RCast; auto | idtac ].
+      simpl.
       apply flatten_coercion; auto.
       apply (Prelude_error "RCast at level >0; casting inside of code brackets is currently not supported").
 
@@ -1028,6 +1131,95 @@ Section HaskFlattener.
     destruct case_RCase.
       simpl.
       apply (Prelude_error "Case not supported (BIG FIXME)").
+
+    destruct case_SBrak.
+      simpl.
+      destruct lev.
+      drop_simplify.
+      set (drop_lev (ec :: nil) (take_arg_types_as_tree Γ t @@@ (ec :: nil))) as empty_tree.
+      take_simplify.
+      rewrite take_lemma'.
+      simpl.
+      rewrite mapOptionTree_compose.
+      rewrite mapOptionTree_compose.
+      rewrite unlev_relev.
+      rewrite <- mapOptionTree_compose.
+      unfold flatten_leveled_type at 4.
+      simpl.
+      rewrite krunk.
+      set (mapOptionTree flatten_leveled_type (drop_lev (ec :: nil) succ)) as succ_host.
+      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 _ _ _ _ ;; _).
+      unfold succ_host.
+      unfold succ_guest.
+      apply arrange_brak.
+      apply (Prelude_error "found Brak at depth >0 indicating 3-level code; only two-level code is currently supported").
+
+    destruct case_SEsc.
+      simpl.
+      destruct lev.
+      simpl.
+      unfold flatten_leveled_type at 2.
+      simpl.
+      rewrite krunk.
+      rewrite mapOptionTree_compose.
+      take_simplify.
+      drop_simplify.
+      simpl.
+      eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply tree_of_nothing' ].
+      simpl.
+      rewrite take_lemma'.
+      rewrite unlev_relev.
+      rewrite <- mapOptionTree_compose.
+      eapply nd_comp; [ apply (arrange_esc _ _ ec) | idtac ].
+
+      set (decide_tree_empty (take_lev (ec :: nil) succ)) as q'.
+      destruct q'.
+      destruct s.
+      rewrite e.
+      clear e.
+
+      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 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 ].
+        simpl.
+        apply ga_join.
+          apply IHx1.
+          apply IHx2.
+          simpl.
+          apply postcompose.
+
+      refine ( _ ;; (boost _ _ _ _ _ (postcompose _ _ _ _ _ _ _ _))).
+      apply ga_cancell.
+      apply firstify.
+
+      induction x.
+        destruct a; simpl.
+        apply ga_id.
+        simpl.
+        refine ( _ ;; (boost _ _ _ _ _ (postcompose _ _ _ _ _ _ _ _))).
+        apply ga_cancell.
+        refine ( _ ;; (boost _ _ _ _ _ (postcompose _ _ _ _ _ _ _ _))).
+        eapply firstify.
+        apply IHx1.
+        apply secondify.
+        apply IHx2.
+
+      (* environment has non-empty leaves *)
+      apply ga_kappa'.
+
+      (* nesting too deep *)
+      apply (Prelude_error "found Esc at depth >0 indicating 3-level code; only two-level code is currently supported").
       Defined.
 
 
diff --git a/src/HaskSkolemizer.v b/src/HaskSkolemizer.v
new file mode 100644 (file)
index 0000000..c1b5708
--- /dev/null
@@ -0,0 +1,429 @@
+(*********************************************************************************************************************************)
+(* HaskSkolemizer:                                                                                                               *)
+(*                                                                                                                               *)
+(*   Skolemizes the portion of a proof which uses judgments at level >0                                                          *)
+(*                                                                                                                               *)
+(*********************************************************************************************************************************)
+
+Generalizable All Variables.
+Require Import Preamble.
+Require Import General.
+Require Import NaturalDeduction.
+Require Import Coq.Strings.String.
+Require Import Coq.Lists.List.
+
+Require Import HaskKinds.
+Require Import HaskCoreTypes.
+Require Import HaskCoreVars.
+Require Import HaskWeakTypes.
+Require Import HaskWeakVars.
+Require Import HaskLiterals.
+Require Import HaskTyCons.
+Require Import HaskStrongTypes.
+Require Import HaskProof.
+Require Import NaturalDeduction.
+
+Require Import HaskStrongTypes.
+Require Import HaskStrong.
+Require Import HaskProof.
+Require Import HaskStrongToProof.
+Require Import HaskProofToStrong.
+Require Import HaskWeakToStrong.
+
+Open Scope nd_scope.
+Set Printing Width 130.
+
+Section HaskSkolemizer.
+
+(*
+  Fixpoint debruijn2phoas {κ} (exp: RawHaskType (fun _ => nat) κ) : HaskType TV κ :=
+     match exp with
+    | TVar    _  x          => x
+    | TAll     _ y          => TAll   _  (fun v => debruijn2phoas  (y (TVar v)))
+    | TApp   _ _ x y        => TApp      (debruijn2phoas  x) (debruijn2phoas  y)
+    | TCon       tc         => TCon      tc
+    | TCoerc _ t1 t2 t      => TCoerc    (debruijn2phoas  t1) (debruijn2phoas  t2)   (debruijn2phoas  t)
+    | TArrow                => TArrow
+    | TCode      v e        => TCode     (debruijn2phoas  v) (debruijn2phoas  e)
+    | TyFunApp  tfc kl k lt => TyFunApp tfc kl k (debruijn2phoasyFunApp _ lt)
+    end
+    with debruijn2phoasyFunApp (lk:list Kind)(exp:@RawHaskTypeList (fun _ => nat) lk) : @HaskTypeList TV lk :=
+    match exp in @RawHaskTypeList _ LK return @RawHaskTypeList TV LK with
+    | TyFunApp_nil               => TyFunApp_nil
+    | TyFunApp_cons  κ kl t rest => TyFunApp_cons _ _ (debruijn2phoas  t) (debruijn2phoasyFunApp _ rest)
+    end.
+*)
+  Definition isNotBrakOrEsc {h}{c} (r:Rule h c) : Prop :=
+    match r with
+      | RBrak _ _ _ _ _ _ => False
+      | REsc  _ _ _ _ _ _ => False
+      | _                 => True
+    end.
+
+  Fixpoint mkArrows {Γ}(lt:list (HaskType Γ ★))(t:HaskType Γ ★) : HaskType Γ ★ :=
+    match lt with
+      | nil => t
+      | 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.
+
+  (* rules of skolemized proofs *)
+  Definition getΓ (j:Judg) := match j with Γ > _ > _ |- _ => Γ end.
+  Definition getSuc (j:Judg) : Tree ??(LeveledHaskType (getΓ j) ★) :=
+    match j as J return Tree ??(LeveledHaskType (getΓ J) ★) with Γ > _ > _ |- s => s end.
+  Fixpoint getjlev {Γ}(tt:Tree ??(LeveledHaskType Γ ★)) : HaskLevel Γ :=
+    match tt with
+      | T_Leaf None              => nil
+      | T_Leaf (Some (_ @@ lev)) => lev
+      | T_Branch b1 b2 =>
+        match getjlev b1 with
+          | nil => getjlev b2
+          | lev => lev
+        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 count' (n:nat)(ln:list nat) : list nat :=
+    match n with
+      | 0    => ln
+      | S n' => count' n' (n'::ln)
+    end.
+
+  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 drop_arg_types_as_tree {Γ} (ht:HaskType Γ ★) : HaskType Γ ★ :=
+    fun TV ite => drop_arg_types (ht TV ite).
+
+  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).
+    intros.
+    unfold take_arg_types_as_tree; simpl.
+    unfold rebundle at 1.
+    admit.
+    Qed.
+
+  Lemma drop_works : forall {Γ}(t1 t2:HaskType Γ ★),
+    drop_arg_types_as_tree (t1 ---> t2) = (drop_arg_types_as_tree t2).
+    intros.
+    unfold drop_arg_types_as_tree.
+    simpl.
+    reflexivity.
+    Qed.
+
+  Inductive SRule : Tree ??Judg -> Tree ??Judg -> Type :=
+(*  | SFlat  : forall h c (r:Rule h c), isNotBrakOrEsc r -> SRule h c*)
+  | SFlat  : forall h c, Rule h c -> SRule h c
+  | SBrak  : forall Γ Δ t ec Σ l,
+    SRule
+    [Γ > Δ > Σ,, (take_arg_types_as_tree t @@@ (ec::l)) |- [ drop_arg_types_as_tree t        @@ (ec::l) ]]
+    [Γ > Δ > Σ                                  |- [<[ec |- t]>              @@      l  ]]
+
+  | SEsc   : forall Γ Δ t ec Σ l,
+    SRule
+    [Γ > Δ > Σ                                  |- [<[ec |- t]>              @@      l  ]]
+    [Γ > Δ > Σ,, (take_arg_types_as_tree t @@@ (ec::l)) |- [ drop_arg_types_as_tree t        @@ (ec::l) ]]
+    .
+
+  Definition take_arg_types_as_tree' {Γ}(lt:LeveledHaskType Γ ★) :=
+    match lt with t @@ l => take_arg_types_as_tree t @@@ l end.
+
+  Definition drop_arg_types_as_tree' {Γ}(lt:LeveledHaskType Γ ★) :=
+    match lt with t @@ l => drop_arg_types_as_tree t @@ l end.
+
+  Definition skolemize_judgment (j:Judg) : Judg :=
+    match j with
+      Γ > Δ > Σ₁ |- Σ₂ =>
+        match getjlev Σ₂ with
+          | nil => j
+          | lev => Γ > Δ > Σ₁,,(mapOptionTreeAndFlatten take_arg_types_as_tree' Σ₂) |- mapOptionTree drop_arg_types_as_tree' Σ₂
+        end
+    end.
+
+  Definition check_hof : forall {Γ}(t:HaskType Γ ★),
+    sumbool
+    True
+    (take_arg_types_as_tree t = [] /\ drop_arg_types_as_tree t = t).
+    intros.
+    destruct (eqd_dec (take_arg_types_as_tree t) []);
+    destruct (eqd_dec (drop_arg_types_as_tree t) t).
+    right; auto.
+    left; auto.
+    left; auto.
+    left; auto.
+    Defined.
+
+  Definition skolemize_proof :
+    forall  {h}{c},
+      ND Rule  h c ->
+      ND SRule (mapOptionTree skolemize_judgment h) (mapOptionTree skolemize_judgment c).
+    intros.
+    eapply nd_map'; [ idtac | apply X ].
+    clear h c X.
+    intros.
+
+    refine (match X as R in Rule H C with
+      | RArrange Γ Δ a b x d           => let case_RArrange := tt      in _
+      | RNote    Γ Δ Σ τ l n           => let case_RNote := tt         in _
+      | RLit     Γ Δ l     _           => let case_RLit := tt          in _
+      | RVar     Γ Δ σ           lev   => let case_RVar := tt          in _
+      | RGlobal  Γ Δ σ l wev           => let case_RGlobal := tt       in _
+      | RLam     Γ Δ Σ tx te     lev   => let case_RLam := tt          in _
+      | RCast    Γ Δ Σ σ τ lev γ       => let case_RCast := tt         in _
+      | RAbsT    Γ Δ Σ κ σ lev         => let case_RAbsT := tt         in _
+      | RAppT    Γ Δ Σ κ σ τ     lev   => let case_RAppT := tt         in _
+      | RAppCo   Γ Δ Σ κ σ₁ σ₂ γ σ lev => let case_RAppCo := tt        in _
+      | RAbsCo   Γ Δ Σ κ σ  σ₁ σ₂  lev => let case_RAbsCo := tt        in _
+      | RApp     Γ Δ Σ₁ Σ₂ tx te lev   => let case_RApp := tt          in _
+      | RLet     Γ Δ Σ₁ Σ₂ σ₁ σ₂ lev   => let case_RLet := 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 _
+      | REsc     Γ Δ t ec succ lev           => let case_REsc := tt          in _
+      | RCase    Γ Δ lev tc Σ avars tbranches alts => let case_RCase := tt         in _
+      | RLetRec  Γ Δ lri x y t         => let case_RLetRec := tt       in _
+      end); clear X h c.
+
+      destruct case_RArrange.
+        simpl.
+        destruct (getjlev x).
+        apply nd_rule.
+        apply SFlat.
+        apply RArrange.
+        apply d.
+        apply nd_rule.
+        apply SFlat.
+        apply RArrange.
+        apply RRight.
+        apply d.
+
+      destruct case_RBrak.
+        simpl.
+        destruct lev; [ idtac | apply (Prelude_error "Brak with nesting depth >1") ].
+        apply nd_rule.
+        apply SBrak.
+
+      destruct case_REsc.
+        simpl.
+        destruct lev; [ idtac | apply (Prelude_error "Esc with nesting depth >1") ].
+        apply nd_rule.
+        apply SEsc.
+
+      destruct case_RNote.
+        apply nd_rule.
+        apply SFlat.
+        simpl.
+        destruct l.
+        apply RNote.
+        apply n.
+        apply RNote.
+        apply n.
+
+      destruct case_RLit.
+        simpl.
+        destruct l0.
+        apply nd_rule.
+        apply SFlat.
+        apply RLit.
+        set (check_hof (@literalType l Γ)) as hof.
+        destruct hof; [ apply (Prelude_error "attempt to use a literal with higher-order type at depth>0") | idtac ].
+        destruct a.
+        rewrite H.
+        rewrite H0.
+        simpl.
+        eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; apply RuCanL ].
+        apply nd_rule.
+        apply SFlat.
+        apply RLit.
+
+      destruct case_RVar.
+        simpl.
+        destruct lev.
+        apply nd_rule; apply SFlat; apply RVar.
+        set (check_hof σ) as hof.
+        destruct hof; [ apply (Prelude_error "attempt to use a variable with higher-order type at depth>0") | idtac ].
+        destruct a.
+        rewrite H.
+        rewrite H0.
+        simpl.
+        eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply RArrange; apply RuCanR ].
+        apply nd_rule.
+        apply SFlat.
+        apply RVar.
+
+      destruct case_RGlobal.
+        simpl.
+        destruct σ.
+        apply nd_rule; apply SFlat; apply RGlobal.
+        set (check_hof (l wev)) as hof.
+        destruct hof; [ apply (Prelude_error "attempt to use a global with higher-order type at depth>0") | idtac ].
+        destruct a.
+        rewrite H.
+        rewrite H0.
+        simpl.
+        eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply RArrange; apply RuCanR ].
+        apply nd_rule.
+        apply SFlat.
+        apply RGlobal.
+
+      destruct case_RLam.
+        simpl.
+        destruct lev.
+        apply nd_rule.
+        apply SFlat.
+        apply RLam.
+        rewrite take_works.
+        rewrite drop_works.
+        apply nd_rule.
+        apply SFlat.
+        apply RArrange.
+        apply RCossa.
+
+      destruct case_RCast.
+        simpl.
+        destruct lev.
+        apply nd_rule.
+        apply SFlat.
+        apply RCast.
+        apply γ.
+        apply (Prelude_error "found RCast at level >0").
+
+      destruct case_RJoin.
+        simpl.
+        destruct (getjlev x).
+        destruct (getjlev q).
+        apply nd_rule.
+        apply SFlat.
+        apply RJoin.
+        apply (Prelude_error "found RJoin at level >0").
+        apply (Prelude_error "found RJoin at level >0").
+
+      destruct case_RApp.
+        simpl.
+        destruct lev.
+        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 ].
+        destruct a.
+        rewrite H.
+        rewrite H0.
+        simpl.
+        set (@RLet Γ Δ (Σ₂,,take_arg_types_as_tree te @@@ (h :: lev)) Σ₁ (drop_arg_types_as_tree te) tx (h::lev)) as q.
+        eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply RArrange; apply RAssoc ].
+        eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply RArrange; apply RExch ].
+        eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply q ].
+        clear q.
+        apply nd_prod.
+        apply nd_rule.
+        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.
+
+      destruct case_RLet.
+        simpl.
+        destruct lev.
+        apply nd_rule.
+        apply SFlat.
+        apply RLet.
+        set (check_hof σ₂) as hof_tx.
+        destruct hof_tx; [ apply (Prelude_error "attempt to let-bind a higher-order function at depth>0") | idtac ].
+        destruct a.
+        rewrite H.
+        rewrite H0.
+        set (@RLet Γ Δ (Σ₁,,(take_arg_types_as_tree σ₁ @@@ (h::lev))) Σ₂ (drop_arg_types_as_tree σ₁) σ₂ (h::lev)) as q.
+        eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply RArrange; apply RAssoc ].
+        eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply RArrange; eapply RLeft; apply RExch ].
+        eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply RArrange; apply RCossa ].
+        eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply q ].
+        clear q.
+        apply nd_prod.
+        apply nd_rule.
+        apply SFlat.
+        apply RArrange.
+        apply RCanR.
+        eapply nd_comp; [ eapply nd_rule; apply SFlat; eapply RArrange; apply RCossa | idtac ].
+        eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply RArrange; apply RAssoc ].
+        apply nd_rule.
+        apply SFlat.
+        apply RArrange.
+        apply RLeft.
+        eapply RExch.
+
+      destruct case_RVoid.
+        simpl.
+        apply nd_rule.
+        apply SFlat.
+        apply RVoid.
+
+      destruct case_RAppT.
+        simpl.
+        destruct lev; [ apply nd_rule; apply SFlat; apply RAppT | idtac ].
+        apply (Prelude_error "RAppT at depth>0").
+
+      destruct case_RAbsT.
+        simpl.
+        destruct lev; simpl; [ apply nd_rule; apply SFlat; apply (@RAbsT _ _ _ _ _ nil) | idtac ].
+        apply (Prelude_error "RAbsT at depth>0").
+
+      destruct case_RAppCo.
+        simpl.
+        destruct lev; [ apply nd_rule; apply SFlat; apply RAppCo | idtac ].
+        apply γ.
+        apply (Prelude_error "RAppCo at depth>0").
+
+      destruct case_RAbsCo.
+        simpl.
+        destruct lev; [ apply nd_rule; apply SFlat; apply RAbsCo | idtac ].
+        apply (Prelude_error "RAbsCo at depth>0").
+
+      destruct case_RLetRec.
+        simpl.
+        destruct t.
+        destruct (getjlev (y @@@ nil)).
+        apply nd_rule.
+        apply SFlat.
+        apply (@RLetRec Γ Δ lri x y nil).
+        apply (Prelude_error "RLetRec at depth>0").
+        apply (Prelude_error "RLetRec at depth>0").
+
+      destruct case_RCase.
+        simpl.
+        apply (Prelude_error "CASE: BIG FIXME").
+        Defined.
+
+End HaskSkolemizer.