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