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