src/HaskFlattener.v

   1 (*********************************************************************************************************************************)
   2 (* HaskFlattener:                                                                                                                *)
   3 (*                                                                                                                               *)
   4 (*    The Flattening Functor.                                                                                                    *)
   5 (*                                                                                                                               *)
   6 (*********************************************************************************************************************************)
   7
   8 Generalizable All Variables.
   9 Require Import Preamble.
  10 Require Import General.
  11 Require Import NaturalDeduction.
  12 Require Import Coq.Strings.String.
  13 Require Import Coq.Lists.List.
  14
  15 Require Import HaskKinds.
  16 Require Import HaskCoreTypes.
  17 Require Import HaskCoreVars.
  18 Require Import HaskWeakTypes.
  19 Require Import HaskWeakVars.
  20 Require Import HaskLiterals.
  21 Require Import HaskTyCons.
  22 Require Import HaskStrongTypes.
  23 Require Import HaskProof.
  24 Require Import NaturalDeduction.
  25
  26 Require Import HaskStrongTypes.
  27 Require Import HaskStrong.
  28 Require Import HaskProof.
  29 Require Import HaskStrongToProof.
  30 Require Import HaskProofToStrong.
  31 Require Import HaskWeakToStrong.
  32
  33 Open Scope nd_scope.
  34
  35 (*
  36  *  The flattening transformation.  Currently only TWO-level languages are
  37  *  supported, and the level-1 sublanguage is rather limited.
  38  *
  39  *  This file abuses terminology pretty badly.  For purposes of this file,
  40  *  "PCF" means "the level-1 sublanguage" and "FC" (aka System FC) means
  41  *  the whole language (level-0 language including bracketed level-1 terms)
  42  *)
  43 Section HaskFlattener.
  44
  45   Inductive TreeFlags {T:Type} : Tree T -> Type :=
  46   | tf_leaf_true  : forall x, TreeFlags (T_Leaf x)
  47   | tf_leaf_false : forall x, TreeFlags (T_Leaf x)
  48   | tf_branch     : forall b1 b2, TreeFlags b1 -> TreeFlags b2 -> TreeFlags (b1,,b2).
  49
  50   Fixpoint mkFlags {T}(f:T -> bool)(t:Tree T) : TreeFlags t :=
  51     match t as T return TreeFlags T with
  52       | T_Leaf x => if f x then tf_leaf_true x else tf_leaf_false x
  53       | T_Branch b1 b2 => tf_branch _ _ (mkFlags f b1) (mkFlags f b2)
  54     end.
  55
  56   (* take and drop are not exact inverses *)
  57
  58   (* drop replaces each leaf where the flag is set with a [] *)
  59   Fixpoint drop {T}{Σ:Tree ??T}(tf:TreeFlags Σ) : Tree ??T :=
  60     match tf with
  61       | tf_leaf_true  x         => []
  62       | tf_leaf_false x         => Σ
  63       | tf_branch b1 b2 tb1 tb2 => (drop tb1),,(drop tb2)
  64     end.
  65
  66   (* take returns only those leaves for which the flag is set; all others are omitted entirely from the tree *)
  67   Fixpoint take {T}{Σ:Tree T}(tf:TreeFlags Σ) : ??(Tree T) :=
  68     match tf with
  69       | tf_leaf_true  x         => Some Σ
  70       | tf_leaf_false x         => None
  71       | tf_branch b1 b2 tb1 tb2 =>
  72         match take tb1 with
  73           | None     => take tb2
  74           | Some b1' => match take tb2 with
  75                           | None     => Some b1'
  76                           | Some b2' => Some (b1',,b2')
  77                         end
  78         end
  79     end.
  80
  81   Definition maybeTree {T}(t:??(Tree ??T)) : Tree ??T :=
  82     match t with
  83       | None => []
  84       | Some x => x
  85     end.
  86
  87   Definition setNone {T}(b:bool)(f:T -> bool) : ??T -> bool :=
  88     fun t =>
  89       match t with
  90         | None => b
  91         | Some x => f x
  92       end.
  93
  94   (* "Arrange" objects are parametric in the type of the leaves of the tree *)
  95   Definition arrangeMap :
  96     forall {T} (Σ₁ Σ₂:Tree ??T) {R} (f:T -> R),
  97       Arrange Σ₁ Σ₂ ->
  98       Arrange (mapOptionTree f Σ₁) (mapOptionTree f Σ₂).
  99     intros.
 100     induction X; simpl.
 101     apply RCanL.
 102     apply RCanR.
 103     apply RuCanL.
 104     apply RuCanR.
 105     apply RAssoc.
 106     apply RCossa.
 107     apply RExch.
 108     apply RWeak.
 109     apply RCont.
 110     apply RLeft; auto.
 111     apply RRight; auto.
 112     eapply RComp; [ apply IHX1 | apply IHX2 ].
 113     Defined.
 114
 115   Definition bnot (b:bool) : bool := if b then false else true.
 116
 117   Definition swapMiddle {T} (a b c d:Tree ??T) :
 118     Arrange ((a,,b),,(c,,d)) ((a,,c),,(b,,d)).
 119     eapply RComp.
 120     apply RCossa.
 121     eapply RComp.
 122     eapply RLeft.
 123     eapply RComp.
 124     eapply RAssoc.
 125     eapply RRight.
 126     apply RExch.
 127     eapply RComp.
 128     eapply RLeft.
 129     eapply RCossa.
 130     eapply RAssoc.
 131     Defined.
 132
 133   Definition arrange :
 134     forall {T} (Σ:Tree ??T) (f:T -> bool),
 135       Arrange Σ (drop (mkFlags (setNone false f) Σ),,( (drop (mkFlags (setNone false (bnot ○ f)) Σ)))).
 136     intros.
 137     induction Σ.
 138       simpl.
 139       destruct a.
 140       simpl.
 141       destruct (f t); simpl.
 142       apply RuCanL.
 143       apply RuCanR.
 144       simpl.
 145       apply RuCanL.
 146       simpl in *.
 147       eapply RComp; [ idtac | apply swapMiddle ].
 148       eapply RComp.
 149       eapply RLeft.
 150       apply IHΣ2.
 151       eapply RRight.
 152       apply IHΣ1.
 153       Defined.
 154
 155   Definition arrange' :
 156     forall {T} (Σ:Tree ??T) (f:T -> bool),
 157       Arrange (drop (mkFlags (setNone false f) Σ),,( (drop (mkFlags (setNone false (bnot ○ f)) Σ)))) Σ.
 158     intros.
 159     induction Σ.
 160       simpl.
 161       destruct a.
 162       simpl.
 163       destruct (f t); simpl.
 164       apply RCanL.
 165       apply RCanR.
 166       simpl.
 167       apply RCanL.
 168       simpl in *.
 169       eapply RComp; [ apply swapMiddle | idtac ].
 170       eapply RComp.
 171       eapply RLeft.
 172       apply IHΣ2.
 173       eapply RRight.
 174       apply IHΣ1.
 175       Defined.
 176
 177   Definition minus' n m :=
 178     match m with
 179       | 0 => n
 180       | _ => match n with
 181                | 0 => 0
 182                | _ => n - m
 183              end
 184     end.
 185
 186   Ltac eqd_dec_refl' :=
 187     match goal with
 188       | [ |- context[@eqd_dec ?T ?V ?X ?X] ] =>
 189         destruct (@eqd_dec T V X X) as [eqd_dec1 | eqd_dec2];
 190           [ clear eqd_dec1 | set (eqd_dec2 (refl_equal _)) as eqd_dec2'; inversion eqd_dec2' ]
 191   end.
 192
 193   Fixpoint reduceTree {T}(unit:T)(merge:T -> T -> T)(tt:Tree ??T) : T :=
 194     match tt with
 195       | T_Leaf None     => unit
 196       | T_Leaf (Some x) => x
 197       | T_Branch b1 b2  => merge (reduceTree unit merge b1) (reduceTree unit merge b2)
 198     end.
 199
 200   Set Printing Width 130.
 201
 202   Context (hetmet_flatten : WeakExprVar).
 203   Context (hetmet_unflatten : WeakExprVar).
 204   Context (hetmet_id      : WeakExprVar).
 205   Context {unitTy : forall TV, RawHaskType TV ★                                          }.
 206   Context {prodTy : forall TV, RawHaskType TV ★  -> RawHaskType TV ★ -> RawHaskType TV ★ }.
 207   Context {gaTy   : forall TV, RawHaskType TV ECKind  -> RawHaskType TV ★ -> RawHaskType TV ★  -> RawHaskType TV ★ }.
 208
 209   Definition ga_mk_tree {Γ} (tr:Tree ??(HaskType Γ ★)) : HaskType Γ ★ :=
 210     fun TV ite => reduceTree (unitTy TV) (prodTy TV) (mapOptionTree (fun x => x TV ite) tr).
 211
 212   Definition ga_mk {Γ}(ec:HaskType Γ ECKind )(ant suc:Tree ??(HaskType Γ ★)) : HaskType Γ ★ :=
 213     fun TV ite => gaTy TV (ec TV ite) (ga_mk_tree ant TV ite) (ga_mk_tree suc TV ite).
 214
 215   Class garrow :=
 216   { ga_id        : ∀ Γ Δ ec l a    , ND Rule [] [Γ > Δ >                           [] |- [@ga_mk Γ ec a a @@ l] ]
 217   ; ga_cancelr   : ∀ Γ Δ ec l a    , ND Rule [] [Γ > Δ >                           [] |- [@ga_mk Γ ec (a,,[]) a @@ l] ]
 218   ; ga_cancell   : ∀ Γ Δ ec l a    , ND Rule [] [Γ > Δ >                           [] |- [@ga_mk Γ ec ([],,a) a @@ l] ]
 219   ; ga_uncancelr : ∀ Γ Δ ec l a    , ND Rule [] [Γ > Δ >                           [] |- [@ga_mk Γ ec a (a,,[]) @@ l] ]
 220   ; ga_uncancell : ∀ Γ Δ ec l a    , ND Rule [] [Γ > Δ >                           [] |- [@ga_mk Γ ec a ([],,a) @@ l] ]
 221   ; ga_assoc     : ∀ Γ Δ ec l a b c, ND Rule [] [Γ > Δ >                           [] |- [@ga_mk Γ ec ((a,,b),,c) (a,,(b,,c)) @@ l] ]
 222   ; ga_unassoc   : ∀ Γ Δ ec l a b c, ND Rule [] [Γ > Δ >                           [] |- [@ga_mk Γ ec (a,,(b,,c)) ((a,,b),,c) @@ l] ]
 223   ; ga_swap      : ∀ Γ Δ ec l a b  , ND Rule [] [Γ > Δ >                           [] |- [@ga_mk Γ ec (a,,b) (b,,a) @@ l] ]
 224   ; ga_drop      : ∀ Γ Δ ec l a    , ND Rule [] [Γ > Δ >                           [] |- [@ga_mk Γ ec a [] @@ l] ]
 225   ; ga_copy      : ∀ Γ Δ ec l a    , ND Rule [] [Γ > Δ >                           [] |- [@ga_mk Γ ec a (a,,a) @@ l] ]
 226   ; ga_first     : ∀ Γ Δ ec l a b x, ND Rule [] [Γ > Δ >          [@ga_mk Γ ec a b @@ l] |- [@ga_mk Γ ec (a,,x) (b,,x) @@ l] ]
 227   ; ga_second    : ∀ Γ Δ ec l a b x, ND Rule [] [Γ > Δ >          [@ga_mk Γ ec a b @@ l] |- [@ga_mk Γ ec (x,,a) (x,,b) @@ l] ]
 228   ; ga_lit       : ∀ Γ Δ ec l lit  , ND Rule [] [Γ > Δ >                           [] |- [@ga_mk Γ ec [] [literalType lit] @@ l] ]
 229   ; ga_curry     : ∀ Γ Δ ec l a b c, ND Rule [] [Γ > Δ > [@ga_mk Γ ec (a,,[b]) [c] @@ l] |- [@ga_mk Γ ec a [b ---> c] @@ l] ]
 230   ; ga_comp      : ∀ Γ Δ ec l a b c, ND Rule [] [Γ > Δ > [@ga_mk Γ ec a b @@ l],,[@ga_mk Γ ec b c @@ l] |- [@ga_mk Γ ec a c @@ l] ]
 231   ; ga_apply     : ∀ Γ Δ ec l a a' b c, ND Rule []
 232                                   [Γ > Δ > [@ga_mk Γ ec a [b ---> c] @@ l],,[@ga_mk Γ ec a' [b] @@ l] |- [@ga_mk Γ ec (a,,a') [c] @@ l] ]
 233   ; ga_kappa     : ∀ Γ Δ ec l a b Σ, ND Rule
 234   [Γ > Δ > Σ,,[@ga_mk Γ ec [] a @@ l] |- [@ga_mk Γ ec [] b @@ l] ]
 235   [Γ > Δ > Σ          |- [@ga_mk Γ ec a  b @@ l] ]
 236   }.
 237   Context `(gar:garrow).
 238
 239   Notation "a ~~~~> b" := (@ga_mk _ _ a b) (at level 20).
 240
 241   (*
 242    *  The story:
 243    *    - code types <[t]>@c                                                become garrows  c () t
 244    *    - free variables of type t at a level lev deeper than the succedent become garrows  c () t
 245    *    - free variables at the level of the succedent become
 246    *)
 247   Fixpoint garrowfy_raw_codetypes {TV}{κ}(exp: RawHaskType TV κ) : RawHaskType TV κ :=
 248     match exp with
 249     | TVar    _  x          => TVar x
 250     | TAll     _ y          => TAll   _  (fun v => garrowfy_raw_codetypes (y v))
 251     | TApp   _ _ x y        => TApp      (garrowfy_raw_codetypes x) (garrowfy_raw_codetypes y)
 252     | TCon       tc         => TCon      tc
 253     | TCoerc _ t1 t2 t      => TCoerc    (garrowfy_raw_codetypes t1) (garrowfy_raw_codetypes t2)
 254                                          (garrowfy_raw_codetypes t)
 255     | TArrow                => TArrow
 256     | TCode      v e        => gaTy TV v (unitTy TV) (garrowfy_raw_codetypes e)
 257     | TyFunApp  tfc kl k lt => TyFunApp tfc kl k (garrowfy_raw_codetypes_list _ lt)
 258     end
 259     with garrowfy_raw_codetypes_list {TV}(lk:list Kind)(exp:@RawHaskTypeList TV lk) : @RawHaskTypeList TV lk :=
 260     match exp in @RawHaskTypeList _ LK return @RawHaskTypeList TV LK with
 261     | TyFunApp_nil               => TyFunApp_nil
 262     | TyFunApp_cons  κ kl t rest => TyFunApp_cons _ _ (garrowfy_raw_codetypes t) (garrowfy_raw_codetypes_list _ rest)
 263     end.
 264   Definition garrowfy_code_types {Γ}{κ}(ht:HaskType Γ κ) : HaskType Γ κ :=
 265     fun TV ite =>
 266       garrowfy_raw_codetypes (ht TV ite).
 267
 268   Definition v2t {Γ}(ec:HaskTyVar Γ ECKind) := fun TV ite => TVar (ec TV ite).
 269
 270   Fixpoint garrowfy_leveled_code_types' {Γ}(ht:HaskType Γ ★)(lev:HaskLevel Γ) : HaskType Γ ★ :=
 271     match lev with
 272       | nil      => garrowfy_code_types ht
 273       | ec::lev' => @ga_mk _ (v2t ec) [] [garrowfy_leveled_code_types' ht lev']
 274     end.
 275
 276   Definition garrowfy_leveled_code_types {Γ}(ht:LeveledHaskType Γ ★) : LeveledHaskType Γ ★ :=
 277     match ht with
 278       htt @@ lev =>
 279       garrowfy_leveled_code_types' htt lev @@ nil
 280     end.
 281
 282   Definition levelMatch {Γ}(lev:HaskLevel Γ) : LeveledHaskType Γ ★ -> bool :=
 283     fun t => match t with ttype@@tlev => if eqd_dec tlev lev then true else false end.
 284
 285   (* In a tree of types, replace any type at depth "lev" or greater None *)
 286   Definition mkDropFlags {Γ}(lev:HaskLevel Γ)(tt:Tree ??(LeveledHaskType Γ ★)) : TreeFlags tt :=
 287     mkFlags (setNone false (levelMatch lev)) tt.
 288
 289   Definition drop_lev {Γ}(lev:HaskLevel Γ)(tt:Tree ??(LeveledHaskType Γ ★)) : Tree ??(LeveledHaskType Γ ★) :=
 290     drop (mkDropFlags lev tt).
 291
 292   (* The opposite: replace any type which is NOT at level "lev" with None *)
 293   Definition mkTakeFlags {Γ}(lev:HaskLevel Γ)(tt:Tree ??(LeveledHaskType Γ ★)) : TreeFlags tt :=
 294     mkFlags (setNone true (bnot ○ levelMatch lev)) tt.
 295
 296   Definition take_lev {Γ}(lev:HaskLevel Γ)(tt:Tree ??(LeveledHaskType Γ ★)) : Tree ??(HaskType Γ ★) :=
 297     mapOptionTree (fun x => garrowfy_code_types (unlev x)) (drop (mkTakeFlags lev tt)).
 298 (*
 299     mapOptionTree (fun x => garrowfy_code_types (unlev x))
 300     (maybeTree (take tt (mkFlags (
 301       fun t => match t with
 302                  | Some (ttype @@ tlev) => if eqd_dec tlev lev then true else false
 303                  | _                    => true
 304                end
 305     ) tt))).
 306 *)
 307
 308   Lemma drop_lev_lemma : forall Γ (lev:HaskLevel Γ) x, drop_lev lev [x @@  lev] = [].
 309     intros; simpl.
 310     Opaque eqd_dec.
 311     unfold drop_lev.
 312     simpl.
 313     unfold mkDropFlags.
 314     simpl.
 315     Transparent eqd_dec.
 316     eqd_dec_refl'.
 317     auto.
 318     Qed.
 319
 320   Lemma drop_lev_lemma_s : forall Γ (lev:HaskLevel Γ) ec x, drop_lev (ec::lev) [x @@  (ec :: lev)] = [].
 321     intros; simpl.
 322     Opaque eqd_dec.
 323     unfold drop_lev.
 324     unfold mkDropFlags.
 325     simpl.
 326     Transparent eqd_dec.
 327     eqd_dec_refl'.
 328     auto.
 329     Qed.
 330
 331   Lemma take_lemma : forall Γ (lev:HaskLevel Γ) x, take_lev lev [x @@  lev] = [garrowfy_code_types x].
 332     intros; simpl.
 333     Opaque eqd_dec.
 334     unfold take_lev.
 335     unfold mkTakeFlags.
 336     simpl.
 337     Transparent eqd_dec.
 338     eqd_dec_refl'.
 339     auto.
 340     Qed.
 341
 342   Ltac drop_simplify :=
 343     match goal with
 344       | [ |- context[@drop_lev ?G ?L [ ?X @@ ?L ] ] ] =>
 345         rewrite (drop_lev_lemma G L X)
 346       | [ |- context[@drop_lev ?G (?E :: ?L) [ ?X @@ (?E :: ?L) ] ] ] =>
 347         rewrite (drop_lev_lemma_s G L E X)
 348       | [ |- context[@drop_lev ?G ?N (?A,,?B)] ] =>
 349       change (@drop_lev G N (A,,B)) with ((@drop_lev G N A),,(@drop_lev G N B))
 350       | [ |- context[@drop_lev ?G ?N (T_Leaf None)] ] =>
 351       change (@drop_lev G N (T_Leaf (@None (LeveledHaskType G ★)))) with (T_Leaf (@None (LeveledHaskType G ★)))
 352     end.
 353
 354   Ltac take_simplify :=
 355     match goal with
 356       | [ |- context[@take_lev ?G ?L [ ?X @@ ?L ] ] ] =>
 357         rewrite (take_lemma G L X)
 358       | [ |- context[@take_lev ?G ?N (?A,,?B)] ] =>
 359       change (@take_lev G N (A,,B)) with ((@take_lev G N A),,(@take_lev G N B))
 360       | [ |- context[@take_lev ?G ?N (T_Leaf None)] ] =>
 361       change (@take_lev G N (T_Leaf (@None (LeveledHaskType G ★)))) with (T_Leaf (@None (LeveledHaskType G ★)))
 362     end.
 363
 364   Axiom literal_types_unchanged : forall Γ l, garrowfy_code_types (literalType l) = literalType(Γ:=Γ) l.
 365
 366   Axiom flatten_coercion : forall Γ Δ κ (σ τ:HaskType Γ κ) (γ:HaskCoercion Γ Δ (σ ∼∼∼ τ)),
 367     HaskCoercion Γ Δ (garrowfy_code_types σ ∼∼∼ garrowfy_code_types τ).
 368
 369   (* This tries to assign a single level to the entire succedent of a judgment.  If the succedent has types from different
 370    * levels (should not happen) it just picks one; if the succedent has no non-None leaves (also should not happen) it
 371    * picks nil *)
 372   Definition getΓ (j:Judg) := match j with Γ > _ > _ |- _ => Γ end.
 373   Definition getSuc (j:Judg) : Tree ??(LeveledHaskType (getΓ j) ★) :=
 374     match j as J return Tree ??(LeveledHaskType (getΓ J) ★) with Γ > _ > _ |- s => s end.
 375   Fixpoint getjlev {Γ}(tt:Tree ??(LeveledHaskType Γ ★)) : HaskLevel Γ :=
 376     match tt with
 377       | T_Leaf None              => nil
 378       | T_Leaf (Some (_ @@ lev)) => lev
 379       | T_Branch b1 b2 =>
 380         match getjlev b1 with
 381           | nil => getjlev b2
 382           | lev => lev
 383         end
 384     end.
 385
 386   Definition unlev' {Γ} (x:LeveledHaskType Γ ★) :=
 387     garrowfy_code_types (unlev x).
 388
 389   (* "n" is the maximum depth remaining AFTER flattening *)
 390   Definition flatten_judgment (j:Judg) :=
 391     match j as J return Judg with
 392       Γ > Δ > ant |- suc =>
 393         match getjlev suc with
 394           | nil        => Γ > Δ > mapOptionTree garrowfy_leveled_code_types ant
 395                                |- mapOptionTree garrowfy_leveled_code_types suc
 396
 397           | (ec::lev') => Γ > Δ > mapOptionTree garrowfy_leveled_code_types (drop_lev (ec::lev') ant)
 398                                |- [ga_mk (v2t ec)
 399                                          (take_lev (ec::lev') ant)
 400                                          (mapOptionTree unlev' suc)  (* we know the level of all of suc *)
 401                                          @@ nil]
 402         end
 403     end.
 404
 405   Definition boost : forall Γ Δ ant x y {lev},
 406     ND Rule []                          [ Γ > Δ > [x@@lev] |- [y@@lev] ] ->
 407     ND Rule [ Γ > Δ > ant |- [x@@lev] ] [ Γ > Δ > ant      |- [y@@lev] ].
 408     intros.
 409     eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanL ].
 410     eapply nd_comp; [ idtac | eapply nd_rule; apply (@RLet Γ Δ [] ant y x lev) ].
 411     eapply nd_comp; [ apply nd_rlecnac | idtac ].
 412     apply nd_prod.
 413     apply nd_id.
 414     eapply nd_comp.
 415       apply X.
 416       eapply nd_rule.
 417       eapply RArrange.
 418       apply RuCanL.
 419       Defined.
 420
 421   Definition postcompose' : ∀ Γ Δ ec lev a b c Σ,
 422      ND Rule [] [ Γ > Δ > Σ                        |- [@ga_mk Γ ec a b @@ lev] ] ->
 423      ND Rule [] [ Γ > Δ > Σ,,[@ga_mk Γ ec b c @@ lev] |- [@ga_mk Γ ec a c @@ lev] ].
 424      intros.
 425      eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RExch ].
 426      eapply nd_comp; [ idtac | eapply nd_rule; apply (@RLet Γ Δ [@ga_mk _ ec b c @@lev] Σ (@ga_mk _ ec a c) (@ga_mk _ ec a b) lev) ].
 427      eapply nd_comp; [ apply nd_llecnac | idtac ].
 428      apply nd_prod.
 429      apply X.
 430      eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RExch ].
 431      apply ga_comp.
 432      Defined.
 433
 434   Definition precompose' : ∀ Γ Δ ec lev a b c Σ,
 435      ND Rule [] [ Γ > Δ > Σ                        |- [@ga_mk Γ ec b c @@ lev] ] ->
 436      ND Rule [] [ Γ > Δ > Σ,,[@ga_mk Γ ec a b @@ lev] |- [@ga_mk Γ ec a c @@ lev] ].
 437      intros.
 438      eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RExch ].
 439      eapply nd_comp; [ idtac | eapply nd_rule; apply (@RLet Γ Δ [@ga_mk _ ec a b @@lev] Σ (@ga_mk _ ec a c) (@ga_mk _ ec b c) lev) ].
 440      eapply nd_comp; [ apply nd_llecnac | idtac ].
 441      apply nd_prod.
 442      apply X.
 443      apply ga_comp.
 444      Defined.
 445
 446   Definition postcompose : ∀ Γ Δ ec lev a b c,
 447      ND Rule [] [ Γ > Δ > []                    |- [@ga_mk Γ ec a b @@ lev] ] ->
 448      ND Rule [] [ Γ > Δ > [@ga_mk Γ ec b c @@ lev] |- [@ga_mk Γ ec a c @@ lev] ].
 449      intros.
 450      eapply nd_comp.
 451      apply postcompose'.
 452      apply X.
 453      apply nd_rule.
 454      apply RArrange.
 455      apply RCanL.
 456      Defined.
 457
 458   Definition firstify : ∀ Γ Δ ec lev a b c Σ,
 459     ND Rule [] [ Γ > Δ > Σ                     |- [@ga_mk Γ ec a b @@ lev] ] ->
 460     ND Rule [] [ Γ > Δ > Σ                    |- [@ga_mk Γ ec (a,,c) (b,,c) @@ lev] ].
 461     intros.
 462     eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanL ].
 463     eapply nd_comp; [ idtac | eapply nd_rule; apply RLet ].
 464     eapply nd_comp; [ apply nd_llecnac | idtac ].
 465     apply nd_prod.
 466     apply X.
 467     eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RuCanL ].
 468     apply ga_first.
 469     Defined.
 470
 471   Definition secondify : ∀ Γ Δ ec lev a b c Σ,
 472      ND Rule [] [ Γ > Δ > Σ                    |- [@ga_mk Γ ec a b @@ lev] ] ->
 473      ND Rule [] [ Γ > Δ > Σ                    |- [@ga_mk Γ ec (c,,a) (c,,b) @@ lev] ].
 474     intros.
 475     eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanL ].
 476     eapply nd_comp; [ idtac | eapply nd_rule; apply RLet ].
 477     eapply nd_comp; [ apply nd_llecnac | idtac ].
 478     apply nd_prod.
 479     apply X.
 480     eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RuCanL ].
 481     apply ga_second.
 482     Defined.
 483
 484   Lemma ga_unkappa     : ∀ Γ Δ ec l a b Σ,
 485     ND Rule
 486     [Γ > Δ > Σ |- [@ga_mk Γ ec a  b @@ l] ]
 487     [Γ > Δ > Σ,,[@ga_mk Γ ec [] a @@ l] |- [@ga_mk Γ ec [] b @@ l] ].
 488     intros.
 489     set (ga_comp Γ Δ ec l [] a b) as q.
 490
 491     set (@RLet Γ Δ) as q'.
 492     set (@RLet Γ Δ [@ga_mk _ ec [] a @@ l] Σ (@ga_mk _ ec [] b) (@ga_mk _ ec a b) l) as q''.
 493     eapply nd_comp.
 494     Focus 2.
 495     eapply nd_rule.
 496     eapply RArrange.
 497     apply RExch.
 498
 499     eapply nd_comp.
 500     Focus 2.
 501     eapply nd_rule.
 502     apply q''.
 503
 504     idtac.
 505     clear q'' q'.
 506     eapply nd_comp.
 507     apply nd_rlecnac.
 508     apply nd_prod.
 509     apply nd_id.
 510     apply q.
 511     Defined.
 512
 513 (*
 514   Notation "`  x" := (take_lev _ x) (at level 20).
 515   Notation "`` x" := (mapOptionTree unlev x) (at level 20).
 516   Notation "``` x" := (drop_lev _ x) (at level 20).
 517 *)
 518   Definition garrowfy_arrangement' :
 519     forall Γ (Δ:CoercionEnv Γ)
 520       (ec:HaskTyVar Γ ECKind) (lev:HaskLevel Γ) (ant1 ant2:Tree ??(LeveledHaskType Γ ★)) (r:Arrange ant1 ant2),
 521       ND Rule [] [Γ > Δ > [] |- [@ga_mk _ (v2t ec) (take_lev (ec :: lev) ant2) (take_lev (ec :: lev) ant1) @@ nil] ].
 522
 523       intros Γ Δ ec lev.
 524       refine (fix garrowfy ant1 ant2 (r:Arrange ant1 ant2):
 525            ND Rule [] [Γ > Δ > [] |- [@ga_mk _ (v2t ec) (take_lev (ec :: lev) ant2) (take_lev (ec :: lev) ant1) @@ nil]] :=
 526         match r as R in Arrange A B return
 527           ND Rule [] [Γ > Δ > [] |- [@ga_mk _ (v2t ec) (take_lev (ec :: lev) B) (take_lev (ec :: lev) A) @@ nil]]
 528           with
 529           | RCanL  a             => let case_RCanL := tt  in ga_uncancell _ _ _ _ _
 530           | RCanR  a             => let case_RCanR := tt  in ga_uncancelr _ _ _ _ _
 531           | RuCanL a             => let case_RuCanL := tt in ga_cancell _ _ _ _ _
 532           | RuCanR a             => let case_RuCanR := tt in ga_cancelr _ _ _ _ _
 533           | RAssoc a b c         => let case_RAssoc := tt in ga_assoc _ _ _ _ _ _ _
 534           | RCossa a b c         => let case_RCossa := tt in ga_unassoc _ _ _ _ _ _ _
 535           | RExch  a b           => let case_RExch := tt  in ga_swap  _ _ _ _ _ _
 536           | RWeak  a             => let case_RWeak := tt  in ga_drop  _ _ _ _ _
 537           | RCont  a             => let case_RCont := tt  in ga_copy  _ _ _ _ _
 538           | RLeft  a b c r'      => let case_RLeft := tt  in garrowfy _ _ r' ;; boost _ _ _ _ _ (ga_second _ _ _ _ _ _ _)
 539           | RRight a b c r'      => let case_RRight := tt in garrowfy _ _ r' ;; boost _ _ _ _ _ (ga_first  _ _ _ _ _ _ _)
 540           | RComp  c b a r1 r2   => let case_RComp := tt  in (fun r1' r2' => _) (garrowfy _ _ r1) (garrowfy _ _ r2)
 541         end); clear garrowfy; repeat take_simplify; repeat drop_simplify; intros.
 542
 543         destruct case_RComp.
 544           set (take_lev (ec :: lev) a) as a' in *.
 545           set (take_lev (ec :: lev) b) as b' in *.
 546           set (take_lev (ec :: lev) c) as c' in *.
 547           eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RCanL ].
 548           eapply nd_comp; [ idtac | eapply nd_rule; apply
 549              (@RLet Γ Δ [] [] (@ga_mk _ (v2t ec) a' c') (@ga_mk _ (v2t ec) a' b')) ].
 550           eapply nd_comp; [ apply nd_llecnac | idtac ].
 551           apply nd_prod.
 552           apply r2'.
 553           eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RuCanL ].
 554           eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RCanR ].
 555           eapply nd_comp; [ idtac | eapply nd_rule;  apply
 556             (@RLet Γ Δ [@ga_mk _ (v2t ec) a' b' @@ _] [] (@ga_mk _ (v2t ec) a' c') (@ga_mk _ (v2t ec) b' c'))].
 557           eapply nd_comp; [ apply nd_llecnac | idtac ].
 558           eapply nd_prod.
 559           apply r1'.
 560           apply ga_comp.
 561           Defined.
 562
 563   Definition garrowfy_arrangement :
 564     forall Γ (Δ:CoercionEnv Γ) n
 565       (ec:HaskTyVar Γ ECKind) (lev:HaskLevel Γ) (ant1 ant2:Tree ??(LeveledHaskType Γ ★)) (r:Arrange ant1 ant2) succ,
 566       ND Rule
 567       [Γ > Δ > mapOptionTree (garrowfy_leveled_code_types ) (drop_lev n ant1)
 568         |- [@ga_mk _ (v2t ec) (take_lev (ec :: lev) ant1) (mapOptionTree (unlev' ) succ) @@ nil]]
 569       [Γ > Δ > mapOptionTree (garrowfy_leveled_code_types ) (drop_lev n ant2)
 570         |- [@ga_mk _ (v2t ec) (take_lev (ec :: lev) ant2) (mapOptionTree (unlev' ) succ) @@ nil]].
 571       intros.
 572       refine ( _ ;; (boost _ _ _ _ _ (postcompose _ _ _ _ _ _ _ (garrowfy_arrangement' Γ Δ ec lev ant1 ant2 r)))).
 573       apply nd_rule.
 574       apply RArrange.
 575       refine ((fix garrowfy ant1 ant2 (r:Arrange ant1 ant2) :=
 576         match r as R in Arrange A B return
 577           Arrange (mapOptionTree (garrowfy_leveled_code_types ) (drop_lev _ A))
 578           (mapOptionTree (garrowfy_leveled_code_types ) (drop_lev _ B)) with
 579           | RCanL  a             => let case_RCanL := tt  in RCanL _
 580           | RCanR  a             => let case_RCanR := tt  in RCanR _
 581           | RuCanL a             => let case_RuCanL := tt in RuCanL _
 582           | RuCanR a             => let case_RuCanR := tt in RuCanR _
 583           | RAssoc a b c         => let case_RAssoc := tt in RAssoc _ _ _
 584           | RCossa a b c         => let case_RCossa := tt in RCossa _ _ _
 585           | RExch  a b           => let case_RExch := tt  in RExch _ _
 586           | RWeak  a             => let case_RWeak := tt  in RWeak _
 587           | RCont  a             => let case_RCont := tt  in RCont _
 588           | RLeft  a b c r'      => let case_RLeft := tt  in RLeft  _ (garrowfy _ _ r')
 589           | RRight a b c r'      => let case_RRight := tt in RRight _ (garrowfy _ _ r')
 590           | RComp  a b c r1 r2   => let case_RComp := tt  in RComp    (garrowfy _ _ r1) (garrowfy _ _ r2)
 591         end) ant1 ant2 r); clear garrowfy; repeat take_simplify; repeat drop_simplify; intros.
 592         Defined.
 593
 594   Definition flatten_arrangement :
 595     forall  Γ Δ ant1 ant2 succ (r:Arrange ant1 ant2),
 596       ND Rule (mapOptionTree (flatten_judgment ) [Γ > Δ > ant1 |- succ])
 597       (mapOptionTree (flatten_judgment ) [Γ > Δ > ant2 |- succ]).
 598     intros.
 599     simpl.
 600     set (getjlev succ) as succ_lev.
 601     assert (succ_lev=getjlev succ).
 602       reflexivity.
 603
 604     destruct succ_lev.
 605       apply nd_rule.
 606       apply RArrange.
 607       induction r; simpl.
 608         apply RCanL.
 609         apply RCanR.
 610         apply RuCanL.
 611         apply RuCanR.
 612         apply RAssoc.
 613         apply RCossa.
 614         apply RExch.
 615         apply RWeak.
 616         apply RCont.
 617         apply RLeft; auto.
 618         apply RRight; auto.
 619         eapply RComp; [ apply IHr1 | apply IHr2 ].
 620
 621       apply garrowfy_arrangement.
 622         apply r.
 623         Defined.
 624
 625   Definition ga_join Γ Δ Σ₁ Σ₂ a b ec :
 626     ND Rule [] [Γ > Δ > Σ₁     |- [@ga_mk _ ec [] a      @@ nil]] ->
 627     ND Rule [] [Γ > Δ > Σ₂     |- [@ga_mk _ ec [] b      @@ nil]] ->
 628     ND Rule [] [Γ > Δ > Σ₁,,Σ₂ |- [@ga_mk _ ec [] (a,,b) @@ nil]].
 629     intro pfa.
 630     intro pfb.
 631     apply secondify with (c:=a)  in pfb.
 632     eapply nd_comp.
 633     Focus 2.
 634     eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
 635     eapply nd_comp; [ eapply nd_llecnac | idtac ].
 636     eapply nd_prod.
 637     apply pfb.
 638     clear pfb.
 639     apply postcompose'.
 640     eapply nd_comp.
 641     apply pfa.
 642     clear pfa.
 643     apply boost.
 644     eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanL ].
 645     apply precompose'.
 646     apply ga_uncancelr.
 647     apply nd_id.
 648     Defined.
 649
 650   Definition arrange_brak : forall Γ Δ ec succ t,
 651    ND Rule
 652      [Γ > Δ > mapOptionTree (garrowfy_leveled_code_types ) (drop_lev (ec :: nil) succ),,
 653       [(@ga_mk _ (v2t ec) [] (take_lev (ec :: nil) succ)) @@  nil] |- [(@ga_mk _ (v2t ec) [] [garrowfy_code_types  t]) @@  nil]]
 654      [Γ > Δ > mapOptionTree (garrowfy_leveled_code_types ) succ |- [(@ga_mk _ (v2t ec) [] [garrowfy_code_types  t]) @@  nil]].
 655     intros.
 656     unfold drop_lev.
 657     set (@arrange' _ succ (levelMatch (ec::nil))) as q.
 658     set (arrangeMap _ _ garrowfy_leveled_code_types q) as y.
 659     eapply nd_comp.
 660     Focus 2.
 661     eapply nd_rule.
 662     eapply RArrange.
 663     apply y.
 664     idtac.
 665     clear y q.
 666     simpl.
 667     eapply nd_comp; [ apply nd_llecnac | idtac ].
 668     eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
 669     apply nd_prod.
 670     Focus 2.
 671     apply nd_id.
 672     idtac.
 673     induction succ; try destruct a; simpl.
 674     unfold take_lev.
 675     unfold mkTakeFlags.
 676     unfold mkFlags.
 677     unfold bnot.
 678     simpl.
 679     destruct l as [t' lev'].
 680     destruct lev' as [|ec' lev'].
 681     simpl.
 682     apply ga_id.
 683     unfold levelMatch.
 684     set (@eqd_dec (HaskLevel Γ) (haskLevelEqDecidable Γ) (ec' :: lev') (ec :: nil)) as q.
 685     destruct q.
 686     inversion e; subst.
 687     simpl.
 688     apply nd_rule.
 689     apply RVar.
 690     simpl.
 691     apply ga_id.
 692     apply ga_id.
 693     unfold take_lev.
 694     simpl.
 695     apply ga_join.
 696       apply IHsucc1.
 697       apply IHsucc2.
 698     Defined.
 699
 700   Definition arrange_esc : forall Γ Δ ec succ t,
 701    ND Rule
 702      [Γ > Δ > mapOptionTree (garrowfy_leveled_code_types ) succ |- [(@ga_mk _ (v2t ec) [] [garrowfy_code_types  t]) @@  nil]]
 703      [Γ > Δ > mapOptionTree (garrowfy_leveled_code_types ) (drop_lev (ec :: nil) succ),,
 704       [(@ga_mk _ (v2t ec) [] (take_lev (ec :: nil) succ)) @@  nil] |- [(@ga_mk _ (v2t ec) [] [garrowfy_code_types  t]) @@  nil]].
 705     intros.
 706     unfold drop_lev.
 707     set (@arrange _ succ (levelMatch (ec::nil))) as q.
 708     set (arrangeMap _ _ garrowfy_leveled_code_types q) as y.
 709     eapply nd_comp.
 710     eapply nd_rule.
 711     eapply RArrange.
 712     apply y.
 713     idtac.
 714     clear y q.
 715
 716     induction succ.
 717     destruct a.
 718       destruct l.
 719       simpl.
 720       unfold mkDropFlags; simpl.
 721       unfold take_lev.
 722       unfold mkTakeFlags.
 723       simpl.
 724       destruct (General.list_eq_dec h0 (ec :: nil)).
 725         simpl.
 726         unfold garrowfy_leveled_code_types'.
 727         rewrite e.
 728         apply nd_id.
 729         simpl.
 730         apply nd_rule.
 731         apply RArrange.
 732         apply RLeft.
 733         apply RWeak.
 734       simpl.
 735         apply nd_rule.
 736         unfold take_lev.
 737         simpl.
 738         apply RArrange.
 739         apply RLeft.
 740         apply RWeak.
 741       apply (Prelude_error "escapifying code with multi-leaf antecedents is not supported").
 742       Defined.
 743
 744   Lemma mapOptionTree_distributes
 745     : forall T R (a b:Tree ??T) (f:T->R),
 746       mapOptionTree f (a,,b) = (mapOptionTree f a),,(mapOptionTree f b).
 747     reflexivity.
 748     Qed.
 749
 750   Axiom garrowfy_commutes_with_substT :
 751     forall  κ Γ (Δ:CoercionEnv Γ) (σ:∀ TV, InstantiatedTypeEnv TV Γ → TV κ → RawHaskType TV ★) (τ:HaskType Γ κ),
 752     garrowfy_code_types  (substT σ τ) = substT (fun TV ite v => garrowfy_raw_codetypes  (σ TV ite v))
 753       (garrowfy_code_types  τ).
 754
 755   Axiom garrowfy_commutes_with_HaskTAll :
 756     forall  κ Γ (Δ:CoercionEnv Γ) (σ:∀ TV, InstantiatedTypeEnv TV Γ → TV κ → RawHaskType TV ★),
 757     garrowfy_code_types  (HaskTAll κ σ) = HaskTAll κ (fun TV ite v => garrowfy_raw_codetypes (σ TV ite v)).
 758
 759   Axiom garrowfy_commutes_with_HaskTApp :
 760     forall  κ Γ (Δ:CoercionEnv Γ) (σ:∀ TV, InstantiatedTypeEnv TV Γ → TV κ → RawHaskType TV ★),
 761     garrowfy_code_types  (HaskTApp (weakF σ) (FreshHaskTyVar κ)) =
 762     HaskTApp (weakF (fun TV ite v => garrowfy_raw_codetypes  (σ TV ite v))) (FreshHaskTyVar κ).
 763
 764   Axiom garrowfy_commutes_with_weakLT : forall (Γ:TypeEnv) κ  t,
 765     garrowfy_leveled_code_types  (weakLT(Γ:=Γ)(κ:=κ) t) = weakLT(Γ:=Γ)(κ:=κ) (garrowfy_leveled_code_types  t).
 766
 767   Axiom globals_do_not_have_code_types : forall (Γ:TypeEnv) (g:Global Γ) v,
 768     garrowfy_code_types (g v) = g v.
 769
 770   Definition decide_tree_empty : forall {T:Type}(t:Tree ??T),
 771     sum { q:Tree unit & t = mapTree (fun _ => None) q } unit.
 772     intro T.
 773     refine (fix foo t :=
 774       match t with
 775         | T_Leaf x => _
 776         | T_Branch b1 b2 => let b1' := foo b1 in let b2' := foo b2 in _
 777       end).
 778     intros.
 779     destruct x.
 780     right; apply tt.
 781     left.
 782       exists (T_Leaf tt).
 783       auto.
 784     destruct b1'.
 785     destruct b2'.
 786     destruct s.
 787     destruct s0.
 788     subst.
 789     left.
 790     exists (x,,x0).
 791     reflexivity.
 792     right; auto.
 793     right; auto.
 794     Defined.
 795
 796
 797   Definition flatten_proof :
 798     forall  {h}{c},
 799       ND Rule h c ->
 800       ND Rule (mapOptionTree (flatten_judgment ) h) (mapOptionTree (flatten_judgment ) c).
 801     intros.
 802     eapply nd_map'; [ idtac | apply X ].
 803     clear h c X.
 804     intros.
 805     simpl in *.
 806
 807     refine (match X as R in Rule H C with
 808       | RArrange Γ Δ a b x d           => let case_RArrange := tt      in _
 809       | RNote    Γ Δ Σ τ l n           => let case_RNote := tt         in _
 810       | RLit     Γ Δ l     _           => let case_RLit := tt          in _
 811       | RVar     Γ Δ σ           lev   => let case_RVar := tt          in _
 812       | RGlobal  Γ Δ σ l wev           => let case_RGlobal := tt       in _
 813       | RLam     Γ Δ Σ tx te     lev   => let case_RLam := tt          in _
 814       | RCast    Γ Δ Σ σ τ lev γ       => let case_RCast := tt         in _
 815       | RAbsT    Γ Δ Σ κ σ lev         => let case_RAbsT := tt         in _
 816       | RAppT    Γ Δ Σ κ σ τ     lev   => let case_RAppT := tt         in _
 817       | RAppCo   Γ Δ Σ κ σ₁ σ₂ γ σ lev => let case_RAppCo := tt        in _
 818       | RAbsCo   Γ Δ Σ κ σ  σ₁ σ₂  lev => let case_RAbsCo := tt        in _
 819       | RApp     Γ Δ Σ₁ Σ₂ tx te lev   => let case_RApp := tt          in _
 820       | RLet     Γ Δ Σ₁ Σ₂ σ₁ σ₂ lev   => let case_RLet := tt          in _
 821       | RJoin    Γ p lri m x q         => let case_RJoin := tt in _
 822       | RVoid    _ _                   => let case_RVoid := tt   in _
 823       | RBrak    Γ Δ t ec succ lev           => let case_RBrak := tt         in _
 824       | REsc     Γ Δ t ec succ lev           => let case_REsc := tt          in _
 825       | RCase    Γ Δ lev tc Σ avars tbranches alts => let case_RCase := tt         in _
 826       | RLetRec  Γ Δ lri x y t         => let case_RLetRec := tt       in _
 827       end); clear X h c.
 828
 829     destruct case_RArrange.
 830       apply (flatten_arrangement  Γ Δ a b x d).
 831
 832     destruct case_RBrak.
 833       simpl.
 834       destruct lev.
 835       change ([garrowfy_code_types  (<[ ec |- t ]>) @@  nil])
 836         with ([ga_mk (v2t ec) [] [garrowfy_code_types  t] @@  nil]).
 837       refine (ga_unkappa Γ Δ (v2t ec) nil (take_lev (ec::nil) succ) _
 838         (mapOptionTree (garrowfy_leveled_code_types) (drop_lev (ec::nil) succ)) ;; _ ).
 839       apply arrange_brak.
 840       apply (Prelude_error "found Brak at depth >0 (a)").
 841
 842     destruct case_REsc.
 843       simpl.
 844       destruct lev.
 845       simpl.
 846       change ([garrowfy_code_types (<[ ec |- t ]>) @@  nil])
 847         with ([ga_mk (v2t ec) [] [garrowfy_code_types  t] @@  nil]).
 848       eapply nd_comp; [ apply arrange_esc | idtac ].
 849       set (decide_tree_empty (take_lev (ec :: nil) succ)) as q'.
 850       destruct q'.
 851       destruct s.
 852       rewrite e.
 853       clear e.
 854
 855       eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanR ].
 856       eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
 857       eapply nd_comp; [ apply nd_llecnac | idtac ].
 858       apply nd_prod; [ idtac | eapply boost ].
 859       induction x.
 860       apply ga_id.
 861       eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanR ].
 862       apply ga_join.
 863       apply IHx1.
 864       apply IHx2.
 865       unfold unlev'.
 866       simpl.
 867       apply postcompose.
 868       apply ga_drop.
 869
 870       (* environment has non-empty leaves *)
 871       apply (ga_kappa Γ Δ (v2t ec) nil (take_lev (ec::nil) succ) _ _).
 872       apply (Prelude_error "found Esc at depth >0 (a)").
 873
 874     destruct case_RNote.
 875       simpl.
 876       destruct l; simpl.
 877         apply nd_rule; apply RNote; auto.
 878         apply nd_rule; apply RNote; auto.
 879
 880     destruct case_RLit.
 881       simpl.
 882       destruct l0; simpl.
 883         rewrite literal_types_unchanged.
 884           apply nd_rule; apply RLit.
 885         unfold take_lev; simpl.
 886         unfold drop_lev; simpl.
 887         unfold unlev'.
 888         simpl.
 889         rewrite literal_types_unchanged.
 890         apply ga_lit.
 891
 892     destruct case_RVar.
 893       Opaque flatten_judgment.
 894       simpl.
 895       Transparent flatten_judgment.
 896       idtac.
 897       unfold flatten_judgment.
 898       unfold getjlev.
 899       destruct lev.
 900       apply nd_rule. apply RVar.
 901       repeat drop_simplify.
 902       unfold unlev'.
 903       repeat take_simplify.
 904       simpl.
 905       apply ga_id.
 906
 907     destruct case_RGlobal.
 908       simpl.
 909       rename l into g.
 910       rename σ into l.
 911       destruct l as [|ec lev]; simpl.
 912         destruct (eqd_dec (g:CoreVar) (hetmet_flatten:CoreVar)).
 913           set (garrowfy_code_types (g wev)) as t.
 914           set (RGlobal _ Δ nil (mkGlobal Γ t hetmet_id)) as q.
 915           simpl in q.
 916           apply nd_rule.
 917           apply q.
 918           apply INil.
 919         destruct (eqd_dec (g:CoreVar) (hetmet_unflatten:CoreVar)).
 920           set (garrowfy_code_types (g wev)) as t.
 921           set (RGlobal _ Δ nil (mkGlobal Γ t hetmet_id)) as q.
 922           simpl in q.
 923           apply nd_rule.
 924           apply q.
 925           apply INil.
 926         apply nd_rule; rewrite globals_do_not_have_code_types.
 927           apply RGlobal.
 928       apply (Prelude_error "found RGlobal at depth >0").
 929
 930     destruct case_RLam.
 931       Opaque drop_lev.
 932       Opaque take_lev.
 933       simpl.
 934       destruct lev as [|ec lev]; simpl; [ apply nd_rule; apply RLam; auto | idtac ].
 935       repeat drop_simplify.
 936       repeat take_simplify.
 937       eapply nd_comp.
 938         eapply nd_rule.
 939         eapply RArrange.
 940         simpl.
 941         apply RCanR.
 942       apply boost.
 943       apply ga_curry.
 944
 945     destruct case_RCast.
 946       simpl.
 947       destruct lev as [|ec lev]; simpl; [ apply nd_rule; apply RCast; auto | idtac ].
 948       apply flatten_coercion; auto.
 949       apply (Prelude_error "RCast at level >0").
 950
 951     destruct case_RJoin.
 952       simpl.
 953       destruct (getjlev x); destruct (getjlev q).
 954       apply nd_rule.
 955       apply RJoin.
 956       apply (Prelude_error "RJoin at depth >0").
 957       apply (Prelude_error "RJoin at depth >0").
 958       apply (Prelude_error "RJoin at depth >0").
 959
 960     destruct case_RApp.
 961       simpl.
 962
 963       destruct lev as [|ec lev]. simpl. apply nd_rule.
 964         replace (garrowfy_code_types  (tx ---> te)) with ((garrowfy_code_types  tx) ---> (garrowfy_code_types  te)).
 965         apply RApp.
 966         reflexivity.
 967
 968         repeat drop_simplify.
 969           repeat take_simplify.
 970           rewrite mapOptionTree_distributes.
 971           set (mapOptionTree (garrowfy_leveled_code_types ) (drop_lev (ec :: lev) Σ₁)) as Σ₁'.
 972           set (mapOptionTree (garrowfy_leveled_code_types ) (drop_lev (ec :: lev) Σ₂)) as Σ₂'.
 973           set (take_lev (ec :: lev) Σ₁) as Σ₁''.
 974           set (take_lev (ec :: lev) Σ₂) as Σ₂''.
 975           replace (garrowfy_code_types  (tx ---> te)) with ((garrowfy_code_types  tx) ---> (garrowfy_code_types  te)).
 976           apply (Prelude_error "FIXME: ga_apply").
 977           reflexivity.
 978 (*
 979   Notation "`  x" := (take_lev _ x) (at level 20).
 980   Notation "`` x" := (mapOptionTree unlev x) (at level 20).
 981   Notation "``` x" := ((drop_lev _ x)) (at level 20).
 982   Notation "!<[]> x" := (garrowfy_code_types _ x) (at level 1).
 983   Notation "!<[@]>" := (garrowfy_leveled_code_types _) (at level 1).
 984 *)
 985     destruct case_RLet.
 986       apply (Prelude_error "FIXME: RLet").
 987 (*
 988       simpl.
 989       destruct lev as [|ec lev]; simpl; [ apply nd_rule; apply RLet; auto | idtac ].
 990       destruct (Peano_dec.eq_nat_dec (Datatypes.length lev) n); [ idtac | apply nd_rule; apply RLet; auto ]; simpl.
 991       repeat drop_simplify.
 992       repeat take_simplify.
 993       rename σ₁ into a.
 994       rename σ₂ into b.
 995       rewrite mapOptionTree_distributes.
 996       rewrite mapOptionTree_distributes.
 997       set (mapOptionTree (garrowfy_leveled_code_types (S n)) (drop_lev (ec :: lev) Σ₁)) as A.
 998       set (take_lev (ec :: lev) Σ₁) as A'.
 999       set (mapOptionTree (garrowfy_leveled_code_types (S n)) (drop_lev (ec :: lev) Σ₂)) as B.
1000       set (take_lev (ec :: lev) Σ₂) as B'.
1001       simpl.
1002
1003       eapply nd_comp.
1004       Focus 2.
1005       eapply nd_rule.
1006       eapply RLet.
1007
1008       apply nd_prod.
1009
1010       apply boost.
1011       apply ga_second.
1012
1013       eapply nd_comp.
1014       Focus 2.
1015       eapply boost.
1016       apply ga_comp.
1017
1018       eapply nd_comp.
1019       eapply nd_rule.
1020       eapply RArrange.
1021       eapply RCanR.
1022
1023       eapply nd_comp.
1024       Focus 2.
1025       eapply nd_rule.
1026       eapply RArrange.
1027       eapply RExch.
1028       idtac.
1029
1030       eapply nd_comp.
1031       apply nd_llecnac.
1032       eapply nd_comp.
1033       Focus 2.
1034       eapply nd_rule.
1035       apply RJoin.
1036       apply nd_prod.
1037
1038       eapply nd_rule.
1039       eapply RVar.
1040
1041       apply nd_id.
1042 *)
1043     destruct case_RVoid.
1044       simpl.
1045       apply nd_rule.
1046       apply RVoid.
1047
1048     destruct case_RAppT.
1049       simpl. destruct lev; simpl.
1050       rewrite garrowfy_commutes_with_HaskTAll.
1051       rewrite garrowfy_commutes_with_substT.
1052       apply nd_rule.
1053       apply RAppT.
1054       apply Δ.
1055       apply Δ.
1056       apply (Prelude_error "ga_apply").
1057
1058     destruct case_RAbsT.
1059       simpl. destruct lev; simpl.
1060       rewrite garrowfy_commutes_with_HaskTAll.
1061       rewrite garrowfy_commutes_with_HaskTApp.
1062       eapply nd_comp; [ idtac | eapply nd_rule; eapply RAbsT ].
1063       simpl.
1064       set (mapOptionTree (garrowfy_leveled_code_types ) (mapOptionTree (weakLT(κ:=κ)) Σ)) as a.
1065       set (mapOptionTree (weakLT(κ:=κ)) (mapOptionTree (garrowfy_leveled_code_types ) Σ)) as q'.
1066       assert (a=q').
1067         unfold a.
1068         unfold q'.
1069         clear a q'.
1070         induction Σ.
1071           destruct a.
1072           simpl.
1073           rewrite garrowfy_commutes_with_weakLT.
1074           reflexivity.
1075           reflexivity.
1076           simpl.
1077           rewrite <- IHΣ1.
1078           rewrite <- IHΣ2.
1079           reflexivity.
1080       rewrite H.
1081       apply nd_id.
1082       apply Δ.
1083       apply Δ.
1084       apply (Prelude_error "AbsT at depth>0").
1085
1086     destruct case_RAppCo.
1087       simpl. destruct lev; simpl.
1088       unfold garrowfy_code_types.
1089       simpl.
1090       apply nd_rule.
1091       apply RAppCo.
1092       apply flatten_coercion.
1093       apply γ.
1094       apply (Prelude_error "AppCo at depth>0").
1095
1096     destruct case_RAbsCo.
1097       simpl. destruct lev; simpl.
1098       unfold garrowfy_code_types.
1099       simpl.
1100       apply (Prelude_error "AbsCo not supported (FIXME)").
1101       apply (Prelude_error "AbsCo at depth>0").
1102
1103     destruct case_RLetRec.
1104       rename t into lev.
1105       apply (Prelude_error "LetRec not supported (FIXME)").
1106
1107     destruct case_RCase.
1108       simpl.
1109       apply (Prelude_error "Case not supported (FIXME)").
1110       Defined.
1111
1112
1113   (* to do: establish some metric on judgments (max length of level of any succedent type, probably), show how to
1114    * calculate it, and show that the flattening procedure above drives it down by one *)
1115
1116   (*
1117   Instance FlatteningFunctor {Γ}{Δ}{ec} : Functor (JudgmentsL (PCF Γ Δ ec)) (TypesL (SystemFCa Γ Δ)) (obact) :=
1118     { fmor := FlatteningFunctor_fmor }.
1119
1120   Definition ReificationFunctor Γ Δ : Functor (JudgmentsL _ _ (PCF n Γ Δ)) SystemFCa' (mapOptionTree brakifyJudg).
1121     refine {| fmor := ReificationFunctor_fmor Γ Δ |}; unfold hom; unfold ob; simpl ; intros.
1122
1123   Definition PCF_SMME (n:nat)(Γ:TypeEnv)(Δ:CoercionEnv Γ) : ProgrammingLanguageSMME.
1124     refine {| plsmme_pl := PCF n Γ Δ |}.
1125     Defined.
1126
1127   Definition SystemFCa_SMME (n:nat)(Γ:TypeEnv)(Δ:CoercionEnv Γ) : ProgrammingLanguageSMME.
1128     refine {| plsmme_pl := SystemFCa n Γ Δ |}.
1129     Defined.
1130
1131   Definition ReificationFunctorMonoidal n : MonoidalFunctor (JudgmentsN n) (JudgmentsN (S n)) (ReificationFunctor n).
1132     Defined.
1133
1134   (* 5.1.4 *)
1135   Definition PCF_SystemFCa_two_level n Γ Δ : TwoLevelLanguage (PCF_SMME n Γ Δ) (SystemFCa_SMME (S n) Γ Δ).
1136     Defined.
1137   *)
1138   (*  ... and the retraction exists *)
1139
1140 End HaskFlattener.
1141
1142 Implicit Arguments garrow [ ].