src/HaskFlattener.v

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