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