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