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 NaturalDeductionContext.
  13 Require Import Coq.Strings.String.
  14 Require Import Coq.Lists.List.
  15
  16 Require Import HaskKinds.
  17 Require Import HaskCoreTypes.
  18 Require Import HaskCoreVars.
  19 Require Import HaskWeakTypes.
  20 Require Import HaskWeakVars.
  21 Require Import HaskLiterals.
  22 Require Import HaskTyCons.
  23 Require Import HaskStrongTypes.
  24 Require Import HaskProof.
  25 Require Import NaturalDeduction.
  26
  27 Require Import HaskStrongTypes.
  28 Require Import HaskStrong.
  29 Require Import HaskProof.
  30 Require Import HaskStrongToProof.
  31 Require Import HaskProofToStrong.
  32 Require Import HaskWeakToStrong.
  33
  34 Require Import HaskSkolemizer.
  35
  36 Open Scope nd_scope.
  37 Set Printing Width 130.
  38
  39 (*
  40  *  The flattening transformation.  Currently only TWO-level languages are
  41  *  supported, and the level-1 sublanguage is rather limited.
  42  *
  43  *  This file abuses terminology pretty badly.  For purposes of this file,
  44  *  "PCF" means "the level-1 sublanguage" and "FC" (aka System FC) means
  45  *  the whole language (level-0 language including bracketed level-1 terms)
  46  *)
  47 Section HaskFlattener.
  48
  49
  50   Ltac eqd_dec_refl' :=
  51     match goal with
  52       | [ |- context[@eqd_dec ?T ?V ?X ?X] ] =>
  53         destruct (@eqd_dec T V X X) as [eqd_dec1 | eqd_dec2];
  54           [ clear eqd_dec1 | set (eqd_dec2 (refl_equal _)) as eqd_dec2'; inversion eqd_dec2' ]
  55   end.
  56
  57   Definition v2t {Γ}(ec:HaskTyVar Γ ECKind) : HaskType Γ ECKind := fun TV ite => TVar (ec TV ite).
  58
  59   Definition levelMatch {Γ}(lev:HaskLevel Γ) : LeveledHaskType Γ ★ -> bool :=
  60     fun t => match t with ttype@@tlev => if eqd_dec tlev lev then true else false end.
  61
  62   (* In a tree of types, replace any type at depth "lev" or greater None *)
  63   Definition mkDropFlags {Γ}(lev:HaskLevel Γ)(tt:Tree ??(LeveledHaskType Γ ★)) : TreeFlags tt :=
  64     mkFlags (liftBoolFunc false (levelMatch lev)) tt.
  65
  66   Definition drop_lev {Γ}(lev:HaskLevel Γ)(tt:Tree ??(LeveledHaskType Γ ★)) : Tree ??(LeveledHaskType Γ ★) :=
  67     dropT (mkDropFlags lev tt).
  68
  69   (* The opposite: replace any type which is NOT at level "lev" with None *)
  70   Definition mkTakeFlags {Γ}(lev:HaskLevel Γ)(tt:Tree ??(LeveledHaskType Γ ★)) : TreeFlags tt :=
  71     mkFlags (liftBoolFunc true (bnot ○ levelMatch lev)) tt.
  72
  73   Definition take_lev {Γ}(lev:HaskLevel Γ)(tt:Tree ??(LeveledHaskType Γ ★)) : Tree ??(LeveledHaskType Γ ★) :=
  74     dropT (mkTakeFlags lev tt).
  75 (*
  76     mapOptionTree (fun x => flatten_type (unlev x))
  77     (maybeTree (takeT tt (mkFlags (
  78       fun t => match t with
  79                  | Some (ttype @@ tlev) => if eqd_dec tlev lev then true else false
  80                  | _                    => true
  81                end
  82     ) tt))).
  83
  84   Definition maybeTree {T}(t:??(Tree ??T)) : Tree ??T :=
  85     match t with
  86       | None   => []
  87       | Some x => x
  88     end.
  89 *)
  90
  91   Lemma drop_lev_lemma : forall Γ (lev:HaskLevel Γ) x, drop_lev lev [x @@  lev] = [].
  92     intros; simpl.
  93     Opaque eqd_dec.
  94     unfold drop_lev.
  95     simpl.
  96     unfold mkDropFlags.
  97     simpl.
  98     Transparent eqd_dec.
  99     eqd_dec_refl'.
 100     auto.
 101     Qed.
 102
 103   Lemma drop_lev_lemma_s : forall Γ (lev:HaskLevel Γ) ec x, drop_lev (ec::lev) [x @@  (ec :: lev)] = [].
 104     intros; simpl.
 105     Opaque eqd_dec.
 106     unfold drop_lev.
 107     unfold mkDropFlags.
 108     simpl.
 109     Transparent eqd_dec.
 110     eqd_dec_refl'.
 111     auto.
 112     Qed.
 113
 114   Lemma take_lemma : forall Γ (lev:HaskLevel Γ) x, take_lev lev [x @@  lev] = [x @@ lev].
 115     intros; simpl.
 116     Opaque eqd_dec.
 117     unfold take_lev.
 118     unfold mkTakeFlags.
 119     simpl.
 120     Transparent eqd_dec.
 121     eqd_dec_refl'.
 122     auto.
 123     Qed.
 124
 125   Lemma take_lemma' : forall Γ (lev:HaskLevel Γ) x, take_lev lev (x @@@ lev) = x @@@ lev.
 126     intros.
 127     induction x.
 128     destruct a; simpl; try reflexivity.
 129     apply take_lemma.
 130     simpl.
 131     rewrite <- IHx1 at 2.
 132     rewrite <- IHx2 at 2.
 133     reflexivity.
 134     Qed.
 135
 136   Ltac drop_simplify :=
 137     match goal with
 138       | [ |- context[@drop_lev ?G ?L [ ?X @@ ?L ] ] ] =>
 139         rewrite (drop_lev_lemma G L X)
 140       | [ |- context[@drop_lev ?G (?E :: ?L) [ ?X @@ (?E :: ?L) ] ] ] =>
 141         rewrite (drop_lev_lemma_s G L E X)
 142       | [ |- context[@drop_lev ?G ?N (?A,,?B)] ] =>
 143       change (@drop_lev G N (A,,B)) with ((@drop_lev G N A),,(@drop_lev G N B))
 144       | [ |- context[@drop_lev ?G ?N (T_Leaf None)] ] =>
 145       change (@drop_lev G N (T_Leaf (@None (LeveledHaskType G ★)))) with (T_Leaf (@None (LeveledHaskType G ★)))
 146     end.
 147
 148   Ltac take_simplify :=
 149     match goal with
 150       | [ |- context[@take_lev ?G ?L [ ?X @@ ?L ] ] ] =>
 151         rewrite (take_lemma G L X)
 152       | [ |- context[@take_lev ?G ?L [ ?X @@@ ?L ] ] ] =>
 153         rewrite (take_lemma' G L X)
 154       | [ |- context[@take_lev ?G ?N (?A,,?B)] ] =>
 155       change (@take_lev G N (A,,B)) with ((@take_lev G N A),,(@take_lev G N B))
 156       | [ |- context[@take_lev ?G ?N (T_Leaf None)] ] =>
 157       change (@take_lev G N (T_Leaf (@None (LeveledHaskType G ★)))) with (T_Leaf (@None (LeveledHaskType G ★)))
 158     end.
 159
 160
 161   (*******************************************************************************)
 162
 163
 164   Context {unitTy : forall TV, RawHaskType TV ECKind  -> RawHaskType TV ★                                          }.
 165   Context {prodTy : forall TV, RawHaskType TV ECKind  -> RawHaskType TV ★  -> RawHaskType TV ★ -> RawHaskType TV ★ }.
 166   Context {gaTy   : forall TV, RawHaskType TV ECKind  -> RawHaskType TV ★ -> RawHaskType TV ★  -> RawHaskType TV ★ }.
 167
 168   Definition ga_mk_tree' {TV}(ec:RawHaskType TV ECKind)(tr:Tree ??(RawHaskType TV ★)) : RawHaskType TV ★ :=
 169     reduceTree (unitTy TV ec) (prodTy TV ec) tr.
 170
 171   Definition ga_mk_tree {Γ}(ec:HaskType Γ ECKind)(tr:Tree ??(HaskType Γ ★)) : HaskType Γ ★ :=
 172     fun TV ite => ga_mk_tree' (ec TV ite) (mapOptionTree (fun x => x TV ite) tr).
 173
 174   Definition ga_mk_raw {TV}(ec:RawHaskType TV ECKind)(ant suc:Tree ??(RawHaskType TV ★)) : RawHaskType TV ★ :=
 175     gaTy TV ec
 176     (ga_mk_tree' ec ant)
 177     (ga_mk_tree' ec suc).
 178
 179   Definition ga_mk {Γ}(ec:HaskType Γ ECKind)(ant suc:Tree ??(HaskType Γ ★)) : HaskType Γ ★ :=
 180     fun TV ite => gaTy TV (ec TV ite) (ga_mk_tree ec ant TV ite) (ga_mk_tree ec suc TV ite).
 181
 182   (*
 183    *  The story:
 184    *    - code types <[t]>@c                                                become garrows  c () t
 185    *    - free variables of type t at a level lev deeper than the succedent become garrows  c () t
 186    *    - free variables at the level of the succedent become
 187    *)
 188   Fixpoint flatten_rawtype {TV}{κ}(exp: RawHaskType TV κ) : RawHaskType TV κ :=
 189     match exp with
 190     | TVar    _  x          => TVar x
 191     | TAll     _ y          => TAll   _  (fun v => flatten_rawtype (y v))
 192     | TApp   _ _ x y        => TApp      (flatten_rawtype x) (flatten_rawtype y)
 193     | TCon       tc         => TCon      tc
 194     | TCoerc _ t1 t2 t      => TCoerc    (flatten_rawtype t1) (flatten_rawtype t2) (flatten_rawtype t)
 195     | TArrow                => TArrow
 196     | TCode     ec e        => let e' := flatten_rawtype e
 197                                in  ga_mk_raw ec (unleaves_ (take_arg_types e')) [drop_arg_types e']
 198     | TyFunApp  tfc kl k lt => TyFunApp tfc kl k (flatten_rawtype_list _ lt)
 199     end
 200     with flatten_rawtype_list {TV}(lk:list Kind)(exp:@RawHaskTypeList TV lk) : @RawHaskTypeList TV lk :=
 201     match exp in @RawHaskTypeList _ LK return @RawHaskTypeList TV LK with
 202     | TyFunApp_nil               => TyFunApp_nil
 203     | TyFunApp_cons  κ kl t rest => TyFunApp_cons _ _ (flatten_rawtype t) (flatten_rawtype_list _ rest)
 204     end.
 205
 206   Definition flatten_type {Γ}{κ}(ht:HaskType Γ κ) : HaskType Γ κ :=
 207     fun TV ite => flatten_rawtype (ht TV ite).
 208
 209   Fixpoint levels_to_tcode {Γ}(ht:HaskType Γ ★)(lev:HaskLevel Γ) : HaskType Γ ★ :=
 210     match lev with
 211       | nil      => flatten_type ht
 212       | ec::lev' => @ga_mk _ (v2t ec) [] [levels_to_tcode ht lev']
 213     end.
 214
 215   Definition flatten_leveled_type {Γ}(ht:LeveledHaskType Γ ★) : LeveledHaskType Γ ★ :=
 216     levels_to_tcode (unlev ht) (getlev ht) @@ nil.
 217
 218   (* AXIOMS *)
 219
 220   Axiom literal_types_unchanged : forall Γ l, flatten_type (literalType l) = literalType(Γ:=Γ) l.
 221
 222   Axiom flatten_coercion : forall Γ Δ κ (σ τ:HaskType Γ κ) (γ:HaskCoercion Γ Δ (σ ∼∼∼ τ)),
 223     HaskCoercion Γ Δ (flatten_type σ ∼∼∼ flatten_type τ).
 224
 225   Axiom flatten_commutes_with_substT :
 226     forall  κ Γ (Δ:CoercionEnv Γ) (σ:∀ TV, InstantiatedTypeEnv TV Γ → TV κ → RawHaskType TV ★) (τ:HaskType Γ κ),
 227     flatten_type  (substT σ τ) = substT (fun TV ite v => flatten_rawtype  (σ TV ite v))
 228       (flatten_type  τ).
 229
 230   Axiom flatten_commutes_with_HaskTAll :
 231     forall  κ Γ (Δ:CoercionEnv Γ) (σ:∀ TV, InstantiatedTypeEnv TV Γ → TV κ → RawHaskType TV ★),
 232     flatten_type  (HaskTAll κ σ) = HaskTAll κ (fun TV ite v => flatten_rawtype (σ TV ite v)).
 233
 234   Axiom flatten_commutes_with_HaskTApp :
 235     forall  κ Γ (Δ:CoercionEnv Γ) (σ:∀ TV, InstantiatedTypeEnv TV Γ → TV κ → RawHaskType TV ★),
 236     flatten_type  (HaskTApp (weakF σ) (FreshHaskTyVar κ)) =
 237     HaskTApp (weakF (fun TV ite v => flatten_rawtype  (σ TV ite v))) (FreshHaskTyVar κ).
 238
 239   Axiom flatten_commutes_with_weakLT : forall (Γ:TypeEnv) κ  t,
 240     flatten_leveled_type  (weakLT(Γ:=Γ)(κ:=κ) t) = weakLT(Γ:=Γ)(κ:=κ) (flatten_leveled_type  t).
 241
 242   Axiom globals_do_not_have_code_types : forall (Γ:TypeEnv) (g:Global Γ) v,
 243     flatten_type (g v) = g v.
 244
 245   (* "n" is the maximum depth remaining AFTER flattening *)
 246   Definition flatten_judgment (j:Judg) :=
 247     match j as J return Judg with
 248       | Γ > Δ > ant |- suc @ nil        => Γ > Δ > mapOptionTree flatten_leveled_type ant
 249                                                 |- mapOptionTree flatten_type suc @ nil
 250       | Γ > Δ > ant |- suc @ (ec::lev') => Γ > Δ > mapOptionTree flatten_leveled_type (drop_lev (ec::lev') ant)
 251                                                 |- [ga_mk (v2t ec)
 252                                                   (mapOptionTree (flatten_type ○ unlev) (take_lev (ec::lev') ant))
 253                                                   (mapOptionTree  flatten_type                               suc )
 254                                                   ] @ nil
 255     end.
 256
 257   Class garrow :=
 258   { ga_id        : ∀ Γ Δ ec l a    , ND Rule [] [Γ > Δ >                          [] |- [@ga_mk Γ ec a a ]@l ]
 259   ; ga_cancelr   : ∀ Γ Δ ec l a    , ND Rule [] [Γ > Δ >                          [] |- [@ga_mk Γ ec (a,,[]) a ]@l ]
 260   ; ga_cancell   : ∀ Γ Δ ec l a    , ND Rule [] [Γ > Δ >                          [] |- [@ga_mk Γ ec ([],,a) a ]@l ]
 261   ; ga_uncancelr : ∀ Γ Δ ec l a    , ND Rule [] [Γ > Δ >                          [] |- [@ga_mk Γ ec a (a,,[]) ]@l ]
 262   ; ga_uncancell : ∀ Γ Δ ec l a    , ND Rule [] [Γ > Δ >                          [] |- [@ga_mk Γ ec a ([],,a) ]@l ]
 263   ; ga_assoc     : ∀ Γ Δ ec l a b c, ND Rule [] [Γ > Δ >                          [] |- [@ga_mk Γ ec ((a,,b),,c) (a,,(b,,c)) ]@l ]
 264   ; ga_unassoc   : ∀ Γ Δ ec l a b c, ND Rule [] [Γ > Δ >                          [] |- [@ga_mk Γ ec (a,,(b,,c)) ((a,,b),,c) ]@l ]
 265   ; ga_swap      : ∀ Γ Δ ec l a b  , ND Rule [] [Γ > Δ >                          [] |- [@ga_mk Γ ec (a,,b) (b,,a) ]@l ]
 266   ; ga_drop      : ∀ Γ Δ ec l a    , ND Rule [] [Γ > Δ >                          [] |- [@ga_mk Γ ec a [] ]@l ]
 267   ; ga_copy      : ∀ Γ Δ ec l a    , ND Rule [] [Γ > Δ >                          [] |- [@ga_mk Γ ec a (a,,a) ]@l ]
 268   ; ga_first     : ∀ Γ Δ ec l a b x, ND Rule [] [Γ > Δ >      [@ga_mk Γ ec a b @@l] |- [@ga_mk Γ ec (a,,x) (b,,x) ]@l ]
 269   ; ga_second    : ∀ Γ Δ ec l a b x, ND Rule [] [Γ > Δ >      [@ga_mk Γ ec a b @@l] |- [@ga_mk Γ ec (x,,a) (x,,b) ]@l ]
 270   ; ga_lit       : ∀ Γ Δ ec l lit  , ND Rule [] [Γ > Δ >                          [] |- [@ga_mk Γ ec [] [literalType lit] ]@l ]
 271   ; ga_curry     : ∀ Γ Δ ec l a b c, ND Rule [] [Γ > Δ > [@ga_mk Γ ec (a,,[b]) [c] @@ l] |- [@ga_mk Γ ec a [b ---> c] ]@ l ]
 272   ; ga_loopl     : ∀ Γ Δ ec l x y z, ND Rule [] [Γ > Δ > [@ga_mk Γ ec (z,,x) (z,,y) @@ l] |- [@ga_mk Γ ec x y ]@ l ]
 273   ; ga_loopr     : ∀ Γ Δ ec l x y z, ND Rule [] [Γ > Δ > [@ga_mk Γ ec (x,,z) (y,,z) @@ l] |- [@ga_mk Γ ec x y ]@ l ]
 274   ; 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 ]
 275   ; ga_apply     : ∀ Γ Δ ec l a a' b c,
 276                  ND Rule [] [Γ > Δ > [@ga_mk Γ ec a [b ---> c] @@ l],,[@ga_mk Γ ec a' [b] @@ l] |- [@ga_mk Γ ec (a,,a') [c] ]@l ]
 277   ; ga_kappa     : ∀ Γ Δ ec l a b Σ, ND Rule
 278   [Γ > Δ > Σ,,[@ga_mk Γ ec [] a @@ l] |- [@ga_mk Γ ec [] b ]@l ]
 279   [Γ > Δ > Σ          |- [@ga_mk Γ ec a  b ]@l ]
 280   }.
 281   Context `(gar:garrow).
 282
 283   Notation "a ~~~~> b" := (@ga_mk _ _ a b) (at level 20).
 284
 285   Definition boost : forall Γ Δ ant x y {lev},
 286     ND Rule []                         [ Γ > Δ > [x@@lev] |- [y]@lev ] ->
 287     ND Rule [ Γ > Δ > ant |- [x]@lev ] [ Γ > Δ > ant      |- [y]@lev ].
 288     intros.
 289     eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ACanR ].
 290     eapply nd_comp; [ idtac | apply RLet ].
 291     eapply nd_comp; [ apply nd_rlecnac | idtac ].
 292     apply nd_prod.
 293     apply nd_id.
 294     eapply nd_comp.
 295       apply X.
 296       eapply nd_rule.
 297       eapply RArrange.
 298       apply AuCanR.
 299     Defined.
 300
 301   Definition precompose Γ Δ ec : forall a x y z lev,
 302     ND Rule
 303       [ Γ > Δ > a                           |- [@ga_mk _ ec y z ]@lev ]
 304       [ Γ > Δ > a,,[@ga_mk _ ec x y @@ lev] |- [@ga_mk _ ec x z ]@lev ].
 305     intros.
 306     eapply nd_comp; [ idtac | eapply RLet ].
 307     eapply nd_comp; [ apply nd_rlecnac | idtac ].
 308     apply nd_prod.
 309     apply nd_id.
 310     eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AExch ].
 311     apply ga_comp.
 312     Defined.
 313
 314   Definition precompose' Γ Δ ec : forall a b x y z lev,
 315     ND Rule
 316       [ Γ > Δ > a,,b                             |- [@ga_mk _ ec y z ]@lev ]
 317       [ Γ > Δ > a,,([@ga_mk _ ec x y @@ lev],,b) |- [@ga_mk _ ec x z ]@lev ].
 318     intros.
 319     eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ALeft; eapply AExch ].
 320     eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AuAssoc ].
 321     apply precompose.
 322     Defined.
 323
 324   Definition postcompose_ Γ Δ ec : forall a x y z lev,
 325     ND Rule
 326       [ Γ > Δ > a                           |- [@ga_mk _ ec x y ]@lev ]
 327       [ Γ > Δ > a,,[@ga_mk _ ec y z @@ lev] |- [@ga_mk _ ec x z ]@lev ].
 328     intros.
 329     eapply nd_comp; [ idtac | eapply RLet ].
 330     eapply nd_comp; [ apply nd_rlecnac | idtac ].
 331     apply nd_prod.
 332     apply nd_id.
 333     apply ga_comp.
 334     Defined.
 335
 336   Definition postcompose  Γ Δ ec : forall x y z lev,
 337     ND Rule [] [ Γ > Δ > []                       |- [@ga_mk _ ec x y ]@lev ] ->
 338     ND Rule [] [ Γ > Δ > [@ga_mk _ ec y z @@ lev] |- [@ga_mk _ ec x z ]@lev ].
 339     intros.
 340     eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ACanL ].
 341     eapply nd_comp; [ idtac | eapply postcompose_ ].
 342     apply X.
 343     Defined.
 344
 345   Definition first_nd : ∀ Γ Δ ec lev a b c Σ,
 346     ND Rule [ Γ > Δ > Σ                    |- [@ga_mk Γ ec a b ]@lev ]
 347             [ Γ > Δ > Σ                    |- [@ga_mk Γ ec (a,,c) (b,,c) ]@lev ].
 348     intros.
 349     eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ACanR ].
 350     eapply nd_comp; [ idtac | apply RLet ].
 351     eapply nd_comp; [ apply nd_rlecnac | idtac ].
 352     apply nd_prod.
 353     apply nd_id.
 354     eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AuCanR ].
 355     apply ga_first.
 356     Defined.
 357
 358   Definition firstify : ∀ Γ Δ ec lev a b c Σ,
 359     ND Rule [] [ Γ > Δ > Σ                    |- [@ga_mk Γ ec a b ]@lev ] ->
 360     ND Rule [] [ Γ > Δ > Σ                    |- [@ga_mk Γ ec (a,,c) (b,,c) ]@lev ].
 361     intros.
 362     eapply nd_comp.
 363     apply X.
 364     apply first_nd.
 365     Defined.
 366
 367   Definition second_nd : ∀ Γ Δ ec lev a b c Σ,
 368      ND Rule
 369      [ Γ > Δ > Σ                    |- [@ga_mk Γ ec a b ]@lev ]
 370      [ Γ > Δ > Σ                    |- [@ga_mk Γ ec (c,,a) (c,,b) ]@lev ].
 371     intros.
 372     eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ACanR ].
 373     eapply nd_comp; [ idtac | apply RLet ].
 374     eapply nd_comp; [ apply nd_rlecnac | idtac ].
 375     apply nd_prod.
 376     apply nd_id.
 377     eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AuCanR ].
 378     apply ga_second.
 379     Defined.
 380
 381   Definition secondify : ∀ Γ Δ ec lev a b c Σ,
 382      ND Rule [] [ Γ > Δ > Σ                    |- [@ga_mk Γ ec a b ]@lev ] ->
 383      ND Rule [] [ Γ > Δ > Σ                    |- [@ga_mk Γ ec (c,,a) (c,,b) ]@lev ].
 384     intros.
 385     eapply nd_comp.
 386     apply X.
 387     apply second_nd.
 388     Defined.
 389
 390    Lemma ga_unkappa     : ∀ Γ Δ ec l a b Σ x,
 391      ND Rule
 392      [Γ > Δ > Σ                          |- [@ga_mk Γ ec (a,,x)  b ]@l ]
 393      [Γ > Δ > Σ,,[@ga_mk Γ ec [] a @@ l] |- [@ga_mk Γ ec x       b ]@l ].
 394      intros.
 395      eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AExch ].
 396      eapply nd_comp; [ idtac | eapply RLet ].
 397      eapply nd_comp; [ apply nd_llecnac | idtac ].
 398      apply nd_prod.
 399      apply ga_first.
 400
 401      eapply nd_comp; [ idtac | eapply RLet ].
 402      eapply nd_comp; [ apply nd_llecnac | idtac ].
 403      apply nd_prod.
 404      apply postcompose.
 405      apply ga_uncancell.
 406      eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AExch ].
 407      apply precompose.
 408      Defined.
 409
 410   (* useful for cutting down on the pretty-printed noise
 411
 412   Notation "`  x" := (take_lev _ x) (at level 20).
 413   Notation "`` x" := (mapOptionTree unlev x) (at level 20).
 414   Notation "``` x" := (drop_lev _ x) (at level 20).
 415   *)
 416   Definition flatten_arrangement' :
 417     forall Γ (Δ:CoercionEnv Γ)
 418       (ec:HaskTyVar Γ ECKind) (lev:HaskLevel Γ) (ant1 ant2:Tree ??(LeveledHaskType Γ ★)) (r:Arrange ant1 ant2),
 419       ND Rule [] [Γ > Δ > [] |- [@ga_mk _ (v2t ec) (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) ant2))
 420         (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) ant1)) ]@nil ].
 421
 422       intros Γ Δ ec lev.
 423       refine (fix flatten ant1 ant2 (r:Arrange ant1 ant2):
 424            ND Rule [] [Γ > Δ > [] |- [@ga_mk _ (v2t ec)
 425              (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) ant2))
 426              (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) ant1)) ]@nil] :=
 427         match r as R in Arrange A B return
 428           ND Rule [] [Γ > Δ > [] |- [@ga_mk _ (v2t ec)
 429             (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) B))
 430             (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) A)) ]@nil]
 431           with
 432           | AId  a               => let case_AId := tt    in ga_id _ _ _ _ _
 433           | ACanL  a             => let case_ACanL := tt  in ga_uncancell _ _ _ _ _
 434           | ACanR  a             => let case_ACanR := tt  in ga_uncancelr _ _ _ _ _
 435           | AuCanL a             => let case_AuCanL := tt in ga_cancell _ _ _ _ _
 436           | AuCanR a             => let case_AuCanR := tt in ga_cancelr _ _ _ _ _
 437           | AAssoc a b c         => let case_AAssoc := tt in ga_assoc _ _ _ _ _ _ _
 438           | AuAssoc a b c         => let case_AuAssoc := tt in ga_unassoc _ _ _ _ _ _ _
 439           | AExch  a b           => let case_AExch := tt  in ga_swap  _ _ _ _ _ _
 440           | AWeak  a             => let case_AWeak := tt  in ga_drop _ _ _ _ _
 441           | ACont  a             => let case_ACont := tt  in ga_copy  _ _ _ _ _
 442           | ALeft  a b c r'      => let case_ALeft := tt  in flatten _ _ r' ;; boost _ _ _ _ _ (ga_second _ _ _ _ _ _ _)
 443           | ARight a b c r'      => let case_ARight := tt in flatten _ _ r' ;; boost _ _ _ _ _ (ga_first  _ _ _ _ _ _ _)
 444           | AComp  c b a r1 r2   => let case_AComp := tt  in (fun r1' r2' => _) (flatten _ _ r1) (flatten _ _ r2)
 445         end); clear flatten; repeat take_simplify; repeat drop_simplify; intros.
 446
 447         destruct case_AComp.
 448           set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) a)) as a' in *.
 449           set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) b)) as b' in *.
 450           set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) c)) as c' in *.
 451           eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply ACanL ].
 452           eapply nd_comp; [ idtac | apply
 453              (@RLet Γ Δ [] [] (@ga_mk _ (v2t ec) a' b') (@ga_mk _ (v2t ec) a' c')) ].
 454           eapply nd_comp; [ apply nd_llecnac | idtac ].
 455           apply nd_prod.
 456           apply r2'.
 457           eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply AuCanR ].
 458           eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply ACanL ].
 459           eapply nd_comp; [ idtac | apply RLet ].
 460           eapply nd_comp; [ apply nd_llecnac | idtac ].
 461           eapply nd_prod.
 462           apply r1'.
 463           eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AExch ].
 464           apply ga_comp.
 465           Defined.
 466
 467   Definition flatten_arrangement :
 468     forall Γ (Δ:CoercionEnv Γ) n
 469       (ec:HaskTyVar Γ ECKind) (lev:HaskLevel Γ) (ant1 ant2:Tree ??(LeveledHaskType Γ ★)) (r:Arrange ant1 ant2) succ,
 470       ND Rule
 471       [Γ > Δ > mapOptionTree (flatten_leveled_type ) (drop_lev n ant1)
 472         |- [@ga_mk _ (v2t ec)
 473           (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) ant1))
 474           (mapOptionTree (flatten_type ) succ) ]@nil]
 475       [Γ > Δ > mapOptionTree (flatten_leveled_type ) (drop_lev n ant2)
 476         |- [@ga_mk _ (v2t ec)
 477           (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) ant2))
 478           (mapOptionTree (flatten_type ) succ) ]@nil].
 479       intros.
 480       refine ( _ ;; (boost _ _ _ _ _ (postcompose _ _ _ _ _ _ _ (flatten_arrangement' Γ Δ ec lev ant1 ant2 r)))).
 481       apply nd_rule.
 482       apply RArrange.
 483       refine ((fix flatten ant1 ant2 (r:Arrange ant1 ant2) :=
 484         match r as R in Arrange A B return
 485           Arrange (mapOptionTree (flatten_leveled_type ) (drop_lev _ A))
 486           (mapOptionTree (flatten_leveled_type ) (drop_lev _ B)) with
 487           | AId  a               => let case_AId := tt  in AId _
 488           | ACanL  a             => let case_ACanL := tt  in ACanL _
 489           | ACanR  a             => let case_ACanR := tt  in ACanR _
 490           | AuCanL a             => let case_AuCanL := tt in AuCanL _
 491           | AuCanR a             => let case_AuCanR := tt in AuCanR _
 492           | AAssoc a b c         => let case_AAssoc := tt in AAssoc _ _ _
 493           | AuAssoc a b c         => let case_AuAssoc := tt in AuAssoc _ _ _
 494           | AExch  a b           => let case_AExch := tt  in AExch _ _
 495           | AWeak  a             => let case_AWeak := tt  in AWeak _
 496           | ACont  a             => let case_ACont := tt  in ACont _
 497           | ALeft  a b c r'      => let case_ALeft := tt  in ALeft  _ (flatten _ _ r')
 498           | ARight a b c r'      => let case_ARight := tt in ARight _ (flatten _ _ r')
 499           | AComp  a b c r1 r2   => let case_AComp := tt  in AComp    (flatten _ _ r1) (flatten _ _ r2)
 500         end) ant1 ant2 r); clear flatten; repeat take_simplify; repeat drop_simplify; intros.
 501         Defined.
 502
 503   Definition flatten_arrangement'' :
 504     forall  Γ Δ ant1 ant2 succ l (r:Arrange ant1 ant2),
 505       ND Rule (mapOptionTree (flatten_judgment ) [Γ > Δ > ant1 |- succ @ l])
 506       (mapOptionTree (flatten_judgment ) [Γ > Δ > ant2 |- succ @ l]).
 507     intros.
 508     simpl.
 509     destruct l.
 510       apply nd_rule.
 511       apply RArrange.
 512       induction r; simpl.
 513         apply AId.
 514         apply ACanL.
 515         apply ACanR.
 516         apply AuCanL.
 517         apply AuCanR.
 518         apply AAssoc.
 519         apply AuAssoc.
 520         apply AExch.    (* TO DO: check for all-leaf trees here *)
 521         apply AWeak.
 522         apply ACont.
 523         apply ALeft; auto.
 524         apply ARight; auto.
 525         eapply AComp; [ apply IHr1 | apply IHr2 ].
 526
 527       apply flatten_arrangement.
 528         apply r.
 529         Defined.
 530
 531   Definition ga_join Γ Δ Σ₁ Σ₂ a b ec :
 532     ND Rule [] [Γ > Δ > Σ₁     |- [@ga_mk _ ec [] a      ]@nil] ->
 533     ND Rule [] [Γ > Δ > Σ₂     |- [@ga_mk _ ec [] b      ]@nil] ->
 534     ND Rule [] [Γ > Δ > Σ₁,,Σ₂ |- [@ga_mk _ ec [] (a,,b) ]@nil].
 535     intro pfa.
 536     intro pfb.
 537     apply secondify with (c:=a)  in pfb.
 538     apply firstify  with (c:=[])  in pfa.
 539     eapply nd_comp; [ idtac | eapply RLet ].
 540     eapply nd_comp; [ eapply nd_llecnac | idtac ].
 541     apply nd_prod.
 542     apply pfa.
 543     clear pfa.
 544
 545     eapply nd_comp; [ idtac | eapply RLet ].
 546     eapply nd_comp; [ apply nd_llecnac | idtac ].
 547     apply nd_prod.
 548     eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ACanL ].
 549     eapply nd_comp; [ idtac | eapply postcompose_ ].
 550     apply ga_uncancelr.
 551
 552     eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AExch ].
 553     eapply nd_comp; [ idtac | eapply precompose ].
 554     apply pfb.
 555     Defined.
 556
 557   Definition arrange_brak : forall Γ Δ ec succ t,
 558    ND Rule
 559      [Γ > Δ >
 560       [(@ga_mk _ (v2t ec) [] (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: nil) succ))) @@  nil],,
 561       mapOptionTree (flatten_leveled_type ) (drop_lev (ec :: nil) succ) |- [t]@nil]
 562      [Γ > Δ > mapOptionTree (flatten_leveled_type ) succ |- [t]@nil].
 563
 564     intros.
 565     unfold drop_lev.
 566     set (@arrangeUnPartition _ succ (levelMatch (ec::nil))) as q.
 567     set (arrangeMap _ _ flatten_leveled_type q) as y.
 568     eapply nd_comp.
 569     Focus 2.
 570     eapply nd_rule.
 571     eapply RArrange.
 572     apply y.
 573     idtac.
 574     clear y q.
 575     eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AExch ].
 576     simpl.
 577     eapply nd_comp; [ apply nd_llecnac | idtac ].
 578     eapply nd_comp; [ idtac | eapply RLet ].
 579     apply nd_prod.
 580     Focus 2.
 581     apply nd_id.
 582     idtac.
 583     induction succ; try destruct a; simpl.
 584     unfold take_lev.
 585     unfold mkTakeFlags.
 586     unfold mkFlags.
 587     unfold bnot.
 588     simpl.
 589     destruct l as [t' lev'].
 590     destruct lev' as [|ec' lev'].
 591     simpl.
 592     apply ga_id.
 593     unfold levelMatch.
 594     set (@eqd_dec (HaskLevel Γ) (haskLevelEqDecidable Γ) (ec' :: lev') (ec :: nil)) as q.
 595     destruct q.
 596     inversion e; subst.
 597     simpl.
 598     apply nd_rule.
 599     unfold flatten_leveled_type.
 600     simpl.
 601     unfold flatten_type.
 602     simpl.
 603     unfold ga_mk.
 604     simpl.
 605     apply RVar.
 606     simpl.
 607     apply ga_id.
 608     apply ga_id.
 609     unfold take_lev.
 610     simpl.
 611     apply ga_join.
 612       apply IHsucc1.
 613       apply IHsucc2.
 614     Defined.
 615
 616   Definition arrange_esc : forall Γ Δ ec succ t,
 617    ND Rule
 618      [Γ > Δ > mapOptionTree (flatten_leveled_type ) succ |- [t]@nil]
 619      [Γ > Δ >
 620       [(@ga_mk _ (v2t ec) [] (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: nil) succ))) @@  nil],,
 621       mapOptionTree (flatten_leveled_type ) (drop_lev (ec :: nil) succ)  |- [t]@nil].
 622     intros.
 623     set (@arrangePartition _ succ (levelMatch (ec::nil))) as q.
 624     set (@drop_lev Γ (ec::nil) succ) as q'.
 625     assert (@drop_lev Γ (ec::nil) succ=q') as H.
 626       reflexivity.
 627     unfold drop_lev in H.
 628     unfold mkDropFlags in H.
 629     rewrite H in q.
 630     clear H.
 631     set (arrangeMap _ _ flatten_leveled_type q) as y.
 632     eapply nd_comp.
 633     eapply nd_rule.
 634     eapply RArrange.
 635     apply y.
 636     clear y q.
 637
 638     set (mapOptionTree flatten_leveled_type (dropT (mkFlags (liftBoolFunc false (bnot ○ levelMatch (ec :: nil))) succ))) as q.
 639     destruct (decide_tree_empty q); [ idtac | apply (Prelude_error "escapifying open code not yet supported") ].
 640     destruct s.
 641
 642     simpl.
 643     eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply AExch ].
 644     set (fun z z' => @RLet Γ Δ z (mapOptionTree flatten_leveled_type q') t z' nil) as q''.
 645     eapply nd_comp; [ idtac | apply RLet ].
 646     clear q''.
 647     eapply nd_comp; [ apply nd_rlecnac | idtac ].
 648     apply nd_prod.
 649     apply nd_rule.
 650     apply RArrange.
 651     eapply AComp; [ idtac | apply ACanR ].
 652     apply ALeft.
 653     apply (@arrangeCancelEmptyTree _ _ _ _ e).
 654
 655     eapply nd_comp.
 656       eapply nd_rule.
 657       eapply (@RVar Γ Δ t nil).
 658     apply nd_rule.
 659       apply RArrange.
 660       eapply AComp.
 661       apply AuCanR.
 662       apply ALeft.
 663       apply AWeak.
 664 (*
 665     eapply decide_tree_empty.
 666
 667     simpl.
 668     set (dropT (mkFlags (liftBoolFunc false (bnot ○ levelMatch (ec :: nil))) succ)) as escapified.
 669     destruct (decide_tree_empty escapified).
 670
 671     induction succ.
 672     destruct a.
 673       unfold drop_lev.
 674       destruct l.
 675       simpl.
 676       unfold mkDropFlags; simpl.
 677       unfold take_lev.
 678       unfold mkTakeFlags.
 679       simpl.
 680       destruct (General.list_eq_dec h0 (ec :: nil)).
 681         simpl.
 682         rewrite e.
 683         apply nd_id.
 684         simpl.
 685         apply nd_rule.
 686         apply RArrange.
 687         apply ALeft.
 688         apply AWeak.
 689       simpl.
 690         apply nd_rule.
 691         unfold take_lev.
 692         simpl.
 693         apply RArrange.
 694         apply ALeft.
 695         apply AWeak.
 696       apply (Prelude_error "escapifying code with multi-leaf antecedents is not supported").
 697 *)
 698       Defined.
 699
 700   Lemma unlev_relev : forall {Γ}(t:Tree ??(HaskType Γ ★)) lev, mapOptionTree unlev (t @@@ lev) = t.
 701     intros.
 702     induction t.
 703     destruct a; reflexivity.
 704     rewrite <- IHt1 at 2.
 705     rewrite <- IHt2 at 2.
 706     reflexivity.
 707     Qed.
 708
 709   Lemma tree_of_nothing : forall Γ ec t,
 710     Arrange (mapOptionTree flatten_leveled_type (drop_lev(Γ:=Γ) (ec :: nil) (t @@@ (ec :: nil)))) [].
 711     intros.
 712     induction t; try destruct o; try destruct a.
 713     simpl.
 714     drop_simplify.
 715     simpl.
 716     apply AId.
 717     simpl.
 718     apply AId.
 719     eapply AComp; [ idtac | apply ACanL ].
 720     eapply AComp; [ idtac | eapply ALeft; apply IHt2 ].
 721     Opaque drop_lev.
 722     simpl.
 723     Transparent drop_lev.
 724     idtac.
 725     drop_simplify.
 726     apply ARight.
 727     apply IHt1.
 728     Defined.
 729
 730   Lemma tree_of_nothing' : forall Γ ec t,
 731     Arrange [] (mapOptionTree flatten_leveled_type (drop_lev(Γ:=Γ) (ec :: nil) (t @@@ (ec :: nil)))).
 732     intros.
 733     induction t; try destruct o; try destruct a.
 734     simpl.
 735     drop_simplify.
 736     simpl.
 737     apply AId.
 738     simpl.
 739     apply AId.
 740     eapply AComp; [ apply AuCanL | idtac ].
 741     eapply AComp; [ eapply ARight; apply IHt1 | idtac ].
 742     Opaque drop_lev.
 743     simpl.
 744     Transparent drop_lev.
 745     idtac.
 746     drop_simplify.
 747     apply ALeft.
 748     apply IHt2.
 749     Defined.
 750
 751   Lemma krunk : forall Γ (ec:HaskTyVar Γ ECKind) t,
 752     flatten_type (<[ ec |- t ]>)
 753     = @ga_mk Γ (v2t ec)
 754     (mapOptionTree flatten_type (take_arg_types_as_tree t))
 755     [ flatten_type (drop_arg_types_as_tree   t)].
 756     intros.
 757     unfold flatten_type at 1.
 758     simpl.
 759     unfold ga_mk.
 760     apply phoas_extensionality.
 761     intros.
 762     unfold v2t.
 763     unfold ga_mk_raw.
 764     unfold ga_mk_tree.
 765     rewrite <- mapOptionTree_compose.
 766     unfold take_arg_types_as_tree.
 767     simpl.
 768     replace (flatten_type (drop_arg_types_as_tree t) tv ite)
 769       with (drop_arg_types (flatten_rawtype (t tv ite))).
 770     replace (unleaves_ (take_arg_types (flatten_rawtype (t tv ite))))
 771       with ((mapOptionTree (fun x : HaskType Γ ★ => flatten_type x tv ite)
 772            (unleaves_
 773               (take_trustme (count_arg_types (t (fun _ : Kind => unit) (ite_unit Γ)))
 774                  (fun TV : Kind → Type => take_arg_types ○ t TV))))).
 775     reflexivity.
 776     unfold flatten_type.
 777     clear gar.
 778     set (t tv ite) as x.
 779     admit.
 780     admit.
 781     Qed.
 782
 783   Lemma drop_to_nothing : forall (Γ:TypeEnv) Σ (lev:HaskLevel Γ),
 784     drop_lev lev (Σ @@@ lev) = mapTree (fun _ => None) (mapTree (fun _ => tt) Σ).
 785     intros.
 786     induction Σ.
 787     destruct a; simpl.
 788     drop_simplify.
 789     auto.
 790     drop_simplify.
 791     auto.
 792     simpl.
 793     rewrite <- IHΣ1.
 794     rewrite <- IHΣ2.
 795     reflexivity.
 796     Qed.
 797
 798   Definition flatten_skolemized_proof :
 799     forall  {h}{c},
 800       ND SRule h c ->
 801       ND  Rule (mapOptionTree (flatten_judgment ) h) (mapOptionTree (flatten_judgment ) c).
 802     intros.
 803     eapply nd_map'; [ idtac | apply X ].
 804     clear h c X.
 805     intros.
 806     simpl in *.
 807
 808     refine
 809       (match X as R in SRule H C with
 810       | SBrak    Γ Δ t ec succ lev           => let case_SBrak := tt         in _
 811       | SEsc     Γ Δ t ec succ lev           => let case_SEsc := tt          in _
 812       | SFlat    h c r                       => let case_SFlat := tt         in _
 813       end).
 814
 815     destruct case_SFlat.
 816     refine (match r as R in Rule H C with
 817       | RArrange Γ Δ a b x l d         => let case_RArrange := tt      in _
 818       | RNote    Γ Δ Σ τ l n           => let case_RNote := tt         in _
 819       | RLit     Γ Δ l     _           => let case_RLit := tt          in _
 820       | RVar     Γ Δ σ           lev   => let case_RVar := tt          in _
 821       | RGlobal  Γ Δ σ l wev           => let case_RGlobal := tt       in _
 822       | RLam     Γ Δ Σ tx te     lev   => let case_RLam := tt          in _
 823       | RCast    Γ Δ Σ σ τ lev γ       => let case_RCast := tt         in _
 824       | RAbsT    Γ Δ Σ κ σ lev         => let case_RAbsT := tt         in _
 825       | RAppT    Γ Δ Σ κ σ τ     lev   => let case_RAppT := tt         in _
 826       | RAppCo   Γ Δ Σ κ σ₁ σ₂ γ σ lev => let case_RAppCo := tt        in _
 827       | RAbsCo   Γ Δ Σ κ σ  σ₁ σ₂  lev => let case_RAbsCo := tt        in _
 828       | RApp     Γ Δ Σ₁ Σ₂ tx te lev   => let case_RApp := tt          in _
 829       | RCut     Γ Δ Σ Σ₁ Σ₁₂ Σ₂ Σ₃ l  => let case_RCut := tt          in _
 830       | RLeft    Γ Δ Σ₁ Σ₂  Σ     l    => let case_RLeft := tt in _
 831       | RRight   Γ Δ Σ₁ Σ₂  Σ     l    => let case_RRight := tt in _
 832       | RVoid    _ _       l           => let case_RVoid := tt   in _
 833       | RBrak    Γ Δ t ec succ lev           => let case_RBrak := tt         in _
 834       | REsc     Γ Δ t ec succ lev           => let case_REsc := tt          in _
 835       | RCase    Γ Δ lev tc Σ avars tbranches alts => let case_RCase := tt         in _
 836       | RLetRec  Γ Δ lri x y t         => let case_RLetRec := tt       in _
 837       end); clear X h c.
 838
 839     destruct case_RArrange.
 840       apply (flatten_arrangement''  Γ Δ a b x _ d).
 841
 842     destruct case_RBrak.
 843       apply (Prelude_error "found unskolemized Brak rule; this shouldn't happen").
 844
 845     destruct case_REsc.
 846       apply (Prelude_error "found unskolemized Esc rule; this shouldn't happen").
 847
 848     destruct case_RNote.
 849       simpl.
 850       destruct l; simpl.
 851         apply nd_rule; apply RNote; auto.
 852         apply nd_rule; apply RNote; auto.
 853
 854     destruct case_RLit.
 855       simpl.
 856       destruct l0; simpl.
 857         unfold flatten_leveled_type.
 858         simpl.
 859         rewrite literal_types_unchanged.
 860           apply nd_rule; apply RLit.
 861         unfold take_lev; simpl.
 862         unfold drop_lev; simpl.
 863         simpl.
 864         rewrite literal_types_unchanged.
 865         apply ga_lit.
 866
 867     destruct case_RVar.
 868       Opaque flatten_judgment.
 869       simpl.
 870       Transparent flatten_judgment.
 871       idtac.
 872       unfold flatten_judgment.
 873       destruct lev.
 874       apply nd_rule. apply RVar.
 875       repeat drop_simplify.
 876       repeat take_simplify.
 877       simpl.
 878       apply ga_id.
 879
 880     destruct case_RGlobal.
 881       simpl.
 882       rename l into g.
 883       rename σ into l.
 884       destruct l as [|ec lev]; simpl.
 885         (*
 886         destruct (eqd_dec (g:CoreVar) (hetmet_flatten:CoreVar)).
 887           set (flatten_type (g wev)) as t.
 888           set (RGlobal _ Δ nil (mkGlobal Γ t hetmet_id)) as q.
 889           simpl in q.
 890           apply nd_rule.
 891           apply q.
 892           apply INil.
 893         destruct (eqd_dec (g:CoreVar) (hetmet_unflatten:CoreVar)).
 894           set (flatten_type (g wev)) as t.
 895           set (RGlobal _ Δ nil (mkGlobal Γ t hetmet_id)) as q.
 896           simpl in q.
 897           apply nd_rule.
 898           apply q.
 899           apply INil.
 900           *)
 901         unfold flatten_leveled_type. simpl.
 902           apply nd_rule; rewrite globals_do_not_have_code_types.
 903           apply RGlobal.
 904       apply (Prelude_error "found RGlobal at depth >0; globals should never appear inside code brackets unless escaped").
 905
 906     destruct case_RLam.
 907       Opaque drop_lev.
 908       Opaque take_lev.
 909       simpl.
 910       destruct lev as [|ec lev]; simpl; [ apply nd_rule; apply RLam; auto | idtac ].
 911       repeat drop_simplify.
 912       repeat take_simplify.
 913       eapply nd_comp.
 914         eapply nd_rule.
 915         eapply RArrange.
 916         simpl.
 917         apply ACanR.
 918       apply boost.
 919       simpl.
 920       apply ga_curry.
 921
 922     destruct case_RCast.
 923       simpl.
 924       destruct lev as [|ec lev]; simpl; [ apply nd_rule; apply RCast; auto | idtac ].
 925       simpl.
 926       apply flatten_coercion; auto.
 927       apply (Prelude_error "RCast at level >0; casting inside of code brackets is currently not supported").
 928
 929     destruct case_RApp.
 930       simpl.
 931
 932       destruct lev as [|ec lev].
 933         unfold flatten_type at 1.
 934         simpl.
 935         apply nd_rule.
 936         apply RApp.
 937
 938         repeat drop_simplify.
 939           repeat take_simplify.
 940           rewrite mapOptionTree_distributes.
 941           set (mapOptionTree (flatten_leveled_type ) (drop_lev (ec :: lev) Σ₁)) as Σ₁'.
 942           set (mapOptionTree (flatten_leveled_type ) (drop_lev (ec :: lev) Σ₂)) as Σ₂'.
 943           set (take_lev (ec :: lev) Σ₁) as Σ₁''.
 944           set (take_lev (ec :: lev) Σ₂) as Σ₂''.
 945           replace (flatten_type  (tx ---> te)) with ((flatten_type  tx) ---> (flatten_type  te)).
 946           apply (Prelude_error "FIXME: ga_apply").
 947           reflexivity.
 948
 949 (*
 950   Notation "`  x" := (take_lev _ x).
 951   Notation "`` x" := (mapOptionTree unlev x) (at level 20).
 952   Notation "``` x" := ((drop_lev _ x)) (at level 20).
 953   Notation "!<[]> x" := (flatten_type _ x) (at level 1).
 954   Notation "!<[@]> x" := (mapOptionTree flatten_leveled_type x) (at level 1).
 955 *)
 956
 957     destruct case_RCut.
 958       simpl.
 959       destruct l as [|ec lev]; simpl.
 960         apply nd_rule.
 961         replace (mapOptionTree flatten_leveled_type (Σ₁₂ @@@ nil)) with (mapOptionTree flatten_type Σ₁₂ @@@ nil).
 962         apply RCut.
 963         induction Σ₁₂; try destruct a; auto.
 964         simpl.
 965         rewrite <- IHΣ₁₂1.
 966         rewrite <- IHΣ₁₂2.
 967         reflexivity.
 968       simpl; repeat drop_simplify.
 969       simpl; repeat take_simplify.
 970       simpl.
 971       set (drop_lev (ec :: lev) (Σ₁₂ @@@ (ec :: lev))) as x1.
 972       rewrite take_lemma'.
 973       rewrite mapOptionTree_compose.
 974       rewrite mapOptionTree_compose.
 975       rewrite mapOptionTree_compose.
 976       rewrite mapOptionTree_compose.
 977       rewrite unlev_relev.
 978       rewrite <- mapOptionTree_compose.
 979       rewrite <- mapOptionTree_compose.
 980       rewrite <- mapOptionTree_compose.
 981       eapply nd_comp; [ idtac | eapply nd_rule; eapply RCut ].
 982       apply nd_prod.
 983       apply nd_id.
 984       eapply nd_comp.
 985       eapply nd_rule.
 986       eapply RArrange.
 987       eapply ALeft.
 988       eapply ARight.
 989       unfold x1.
 990       rewrite drop_to_nothing.
 991       apply arrangeCancelEmptyTree with (q:=(mapTree (fun _ : ??(HaskType Γ ★) => tt) Σ₁₂)).
 992         induction Σ₁₂; try destruct a; auto.
 993         simpl.
 994         rewrite <- IHΣ₁₂1 at 2.
 995         rewrite <- IHΣ₁₂2 at 2.
 996         reflexivity.
 997       eapply nd_comp; [ eapply nd_rule; eapply RArrange; eapply ALeft; eapply ACanL | idtac ].
 998       set (mapOptionTree flatten_type Σ₁₂) as a.
 999       set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) Σ₁)) as b.
1000       set (mapOptionTree flatten_leveled_type (drop_lev (ec :: lev) Σ₂)) as c.
1001       set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) Σ₂)) as d.
1002       set (mapOptionTree flatten_leveled_type (drop_lev (ec :: lev) Σ)) as e.
1003       set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) Σ)) as f.
1004       eapply nd_comp; [ idtac | eapply nd_rule; eapply RCut ].
1005       eapply nd_comp; [ apply nd_llecnac | idtac ].
1006       apply nd_prod.
1007       simpl.
1008       eapply secondify.
1009       apply ga_first.
1010       eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ALeft; eapply AExch ].
1011       eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AuAssoc ].
1012       simpl.
1013       apply precompose.
1014
1015     destruct case_RLeft.
1016       simpl.
1017       destruct l as [|ec lev].
1018       simpl.
1019         replace (mapOptionTree flatten_leveled_type (Σ @@@ nil)) with (mapOptionTree flatten_type Σ @@@ nil).
1020         apply nd_rule.
1021         apply RLeft.
1022         induction Σ; try destruct a; auto.
1023         simpl.
1024         rewrite <- IHΣ1.
1025         rewrite <- IHΣ2.
1026         reflexivity.
1027       repeat drop_simplify.
1028         rewrite drop_to_nothing.
1029         simpl.
1030         eapply nd_comp.
1031         Focus 2.
1032         eapply nd_rule.
1033         eapply RArrange.
1034         eapply ARight.
1035         apply arrangeUnCancelEmptyTree with (q:=(mapTree (fun _ : ??(HaskType Γ ★) => tt) Σ)).
1036           induction Σ; try destruct a; auto.
1037           simpl.
1038           rewrite <- IHΣ1 at 2.
1039           rewrite <- IHΣ2 at 2.
1040           reflexivity.
1041         idtac.
1042         eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AuCanL ].
1043         apply boost.
1044         take_simplify.
1045         simpl.
1046         replace (take_lev (ec :: lev) (Σ @@@ (ec :: lev))) with (Σ @@@ (ec::lev)).
1047         rewrite mapOptionTree_compose.
1048         rewrite mapOptionTree_compose.
1049         rewrite unlev_relev.
1050         apply ga_second.
1051       rewrite take_lemma'.
1052       reflexivity.
1053
1054     destruct case_RRight.
1055       simpl.
1056       destruct l as [|ec lev].
1057       simpl.
1058         replace (mapOptionTree flatten_leveled_type (Σ @@@ nil)) with (mapOptionTree flatten_type Σ @@@ nil).
1059         apply nd_rule.
1060         apply RRight.
1061         induction Σ; try destruct a; auto.
1062         simpl.
1063         rewrite <- IHΣ1.
1064         rewrite <- IHΣ2.
1065         reflexivity.
1066       repeat drop_simplify.
1067         rewrite drop_to_nothing.
1068         simpl.
1069         eapply nd_comp.
1070         Focus 2.
1071         eapply nd_rule.
1072         eapply RArrange.
1073         eapply ALeft.
1074         apply arrangeUnCancelEmptyTree with (q:=(mapTree (fun _ : ??(HaskType Γ ★) => tt) Σ)).
1075           induction Σ; try destruct a; auto.
1076           simpl.
1077           rewrite <- IHΣ1 at 2.
1078           rewrite <- IHΣ2 at 2.
1079           reflexivity.
1080         idtac.
1081         eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AuCanR ].
1082         apply boost.
1083         take_simplify.
1084         simpl.
1085         replace (take_lev (ec :: lev) (Σ @@@ (ec :: lev))) with (Σ @@@ (ec::lev)).
1086         rewrite mapOptionTree_compose.
1087         rewrite mapOptionTree_compose.
1088         rewrite unlev_relev.
1089         apply ga_first.
1090       rewrite take_lemma'.
1091       reflexivity.
1092
1093     destruct case_RVoid.
1094       simpl.
1095       destruct l.
1096       apply nd_rule.
1097       apply RVoid.
1098       drop_simplify.
1099       take_simplify.
1100       simpl.
1101       apply ga_id.
1102
1103     destruct case_RAppT.
1104       simpl. destruct lev; simpl.
1105       unfold flatten_leveled_type.
1106       simpl.
1107       rewrite flatten_commutes_with_HaskTAll.
1108       rewrite flatten_commutes_with_substT.
1109       apply nd_rule.
1110       apply RAppT.
1111       apply Δ.
1112       apply Δ.
1113       apply (Prelude_error "found type application at level >0; this is not supported").
1114
1115     destruct case_RAbsT.
1116       simpl. destruct lev; simpl.
1117       rewrite flatten_commutes_with_HaskTAll.
1118       rewrite flatten_commutes_with_HaskTApp.
1119       eapply nd_comp; [ idtac | eapply nd_rule; eapply RAbsT ].
1120       simpl.
1121       set (mapOptionTree (flatten_leveled_type ) (mapOptionTree (weakLT(κ:=κ)) Σ)) as a.
1122       set (mapOptionTree (weakLT(κ:=κ)) (mapOptionTree (flatten_leveled_type ) Σ)) as q'.
1123       assert (a=q').
1124         unfold a.
1125         unfold q'.
1126         clear a q'.
1127         induction Σ.
1128           destruct a.
1129           simpl.
1130           rewrite flatten_commutes_with_weakLT.
1131           reflexivity.
1132           reflexivity.
1133           simpl.
1134           rewrite <- IHΣ1.
1135           rewrite <- IHΣ2.
1136           reflexivity.
1137       rewrite H.
1138       apply nd_id.
1139       apply Δ.
1140       apply Δ.
1141       apply (Prelude_error "found type abstraction at level >0; this is not supported").
1142
1143     destruct case_RAppCo.
1144       simpl. destruct lev; simpl.
1145       unfold flatten_type.
1146       simpl.
1147       apply nd_rule.
1148       apply RAppCo.
1149       apply flatten_coercion.
1150       apply γ.
1151       apply (Prelude_error "found coercion application at level >0; this is not supported").
1152
1153     destruct case_RAbsCo.
1154       simpl. destruct lev; simpl.
1155       unfold flatten_type.
1156       simpl.
1157       apply (Prelude_error "AbsCo not supported (FIXME)").
1158       apply (Prelude_error "found coercion abstraction at level >0; this is not supported").
1159
1160     destruct case_RLetRec.
1161       rename t into lev.
1162       simpl. destruct lev; simpl.
1163       apply nd_rule.
1164       set (@RLetRec Γ Δ (mapOptionTree flatten_leveled_type lri) (flatten_type x) (mapOptionTree flatten_type y) nil) as q.
1165       replace (mapOptionTree flatten_leveled_type (y @@@ nil)) with (mapOptionTree flatten_type y @@@ nil).
1166       apply q.
1167         induction y; try destruct a; auto.
1168         simpl.
1169         rewrite IHy1.
1170         rewrite IHy2.
1171         reflexivity.
1172       repeat drop_simplify.
1173       repeat take_simplify.
1174       simpl.
1175       rewrite drop_to_nothing.
1176       eapply nd_comp.
1177         eapply nd_rule.
1178         eapply RArrange.
1179         eapply AComp.
1180         eapply ARight.
1181         apply arrangeCancelEmptyTree with (q:=y).
1182           induction y; try destruct a; auto.
1183           simpl.
1184           rewrite <- IHy1.
1185           rewrite <- IHy2.
1186           reflexivity.
1187         apply ACanL.
1188         rewrite take_lemma'.
1189         set (mapOptionTree (flatten_type ○ unlev) (take_lev (h :: lev) lri)) as lri'.
1190         set (mapOptionTree flatten_leveled_type (drop_lev (h :: lev) lri)) as lri''.
1191         replace (mapOptionTree (flatten_type ○ unlev) (y @@@ (h :: lev))) with (mapOptionTree flatten_type y).
1192         apply boost.
1193         apply ga_loopl.
1194         rewrite <- mapOptionTree_compose.
1195         simpl.
1196         reflexivity.
1197
1198     destruct case_RCase.
1199       destruct lev; [ idtac | apply (Prelude_error "case at depth >0") ]; simpl.
1200       apply nd_rule.
1201       rewrite <- mapOptionTree_compose.
1202       replace (mapOptionTree
1203         (fun x  => flatten_judgment (pcb_judg (snd x)))
1204         alts,, [Γ > Δ > mapOptionTree flatten_leveled_type Σ |- [flatten_type (caseType tc avars)] @ nil])
1205       with
1206         (mapOptionTree
1207            (fun x  => @pcb_judg tc Γ Δ nil (flatten_type tbranches) avars (fst x) (snd x))
1208            alts,,
1209            [Γ > Δ > mapOptionTree flatten_leveled_type Σ |- [caseType tc avars] @ nil]).
1210       replace (mapOptionTree flatten_leveled_type
1211         (mapOptionTreeAndFlatten
1212            (fun x  => (snd x)) alts))
1213       with (mapOptionTreeAndFlatten
1214            (fun x =>
1215             (snd x)) alts).
1216       apply RCase.
1217       admit.
1218       admit.
1219
1220     destruct case_SBrak.
1221       simpl.
1222       destruct lev.
1223       drop_simplify.
1224       set (drop_lev (ec :: nil) (take_arg_types_as_tree t @@@ (ec :: nil))) as empty_tree.
1225       take_simplify.
1226       rewrite take_lemma'.
1227       simpl.
1228       rewrite mapOptionTree_compose.
1229       rewrite mapOptionTree_compose.
1230       rewrite unlev_relev.
1231       rewrite <- mapOptionTree_compose.
1232       simpl.
1233       rewrite krunk.
1234       set (mapOptionTree flatten_leveled_type (drop_lev (ec :: nil) succ)) as succ_host.
1235       set (mapOptionTree (flatten_type ○ unlev)(take_lev (ec :: nil) succ)) as succ_guest.
1236       set (mapOptionTree flatten_type (take_arg_types_as_tree t)) as succ_args.
1237       unfold empty_tree.
1238       eapply nd_comp; [ eapply nd_rule; eapply RArrange; eapply ALeft; apply tree_of_nothing | idtac ].
1239       eapply nd_comp; [ eapply nd_rule; eapply RArrange; eapply ACanR | idtac ].
1240       refine (ga_unkappa Γ Δ (v2t ec) nil _ _ _ _ ;; _).
1241       eapply nd_comp; [ idtac | eapply arrange_brak ].
1242       unfold succ_host.
1243       unfold succ_guest.
1244       eapply nd_rule.
1245         eapply RArrange.
1246         apply AExch.
1247       apply (Prelude_error "found Brak at depth >0 indicating 3-level code; only two-level code is currently supported").
1248
1249     destruct case_SEsc.
1250       simpl.
1251       destruct lev.
1252       simpl.
1253       unfold flatten_leveled_type at 2.
1254       simpl.
1255       rewrite krunk.
1256       rewrite mapOptionTree_compose.
1257       take_simplify.
1258       drop_simplify.
1259       simpl.
1260       eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ALeft; apply tree_of_nothing' ].
1261       eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ACanR ].
1262       simpl.
1263       rewrite take_lemma'.
1264       rewrite unlev_relev.
1265       rewrite <- mapOptionTree_compose.
1266       eapply nd_comp; [ apply (arrange_esc _ _ ec) | idtac ].
1267
1268       set (decide_tree_empty (take_lev (ec :: nil) succ)) as q'.
1269       destruct q'.
1270       destruct s.
1271       rewrite e.
1272       clear e.
1273
1274       set (mapOptionTree flatten_leveled_type (drop_lev (ec :: nil) succ)) as succ_host.
1275       set (mapOptionTree flatten_type (take_arg_types_as_tree t)) as succ_args.
1276
1277       eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply AuCanR ].
1278       eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply AuCanR ].
1279       eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply ACanL ].
1280       eapply nd_comp; [ idtac | eapply RLet ].
1281       eapply nd_comp; [ apply nd_llecnac | idtac ].
1282       apply nd_prod; [ idtac | eapply boost ].
1283       induction x.
1284         apply ga_id.
1285         eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ACanL ].
1286         simpl.
1287         apply ga_join.
1288           apply IHx1.
1289           apply IHx2.
1290           simpl.
1291           apply postcompose.
1292
1293       refine ( _ ;; (boost _ _ _ _ _ (postcompose _ _ _ _ _ _ _ _))).
1294       apply ga_cancell.
1295       apply firstify.
1296
1297       induction x.
1298         destruct a; simpl.
1299         apply ga_id.
1300         simpl.
1301         refine ( _ ;; (boost _ _ _ _ _ (postcompose _ _ _ _ _ _ _ _))).
1302         apply ga_cancell.
1303         refine ( _ ;; (boost _ _ _ _ _ (postcompose _ _ _ _ _ _ _ _))).
1304         eapply firstify.
1305         apply IHx1.
1306         apply secondify.
1307         apply IHx2.
1308
1309       (* environment has non-empty leaves *)
1310       apply (Prelude_error "ga_kappa not supported yet (BIG FIXME)").
1311
1312       (* nesting too deep *)
1313       apply (Prelude_error "found Esc at depth >0 indicating 3-level code; only two-level code is currently supported").
1314       Defined.
1315
1316   Definition flatten_proof :
1317     forall  {h}{c},
1318       ND  Rule h c ->
1319       ND  Rule h c.
1320     apply (Prelude_error "sorry, non-skolemized flattening isn't implemented").
1321     Defined.
1322
1323   Definition skolemize_and_flatten_proof :
1324     forall  {h}{c},
1325       ND  Rule h c ->
1326       ND  Rule
1327            (mapOptionTree (flatten_judgment ○ skolemize_judgment) h)
1328            (mapOptionTree (flatten_judgment ○ skolemize_judgment) c).
1329     intros.
1330     rewrite mapOptionTree_compose.
1331     rewrite mapOptionTree_compose.
1332     apply flatten_skolemized_proof.
1333     apply skolemize_proof.
1334     apply X.
1335     Defined.
1336
1337
1338   (* to do: establish some metric on judgments (max length of level of any succedent type, probably), show how to
1339    * calculate it, and show that the flattening procedure above drives it down by one *)
1340
1341   (*
1342   Instance FlatteningFunctor {Γ}{Δ}{ec} : Functor (JudgmentsL (PCF Γ Δ ec)) (TypesL (SystemFCa Γ Δ)) (obact) :=
1343     { fmor := FlatteningFunctor_fmor }.
1344
1345   Definition ReificationFunctor Γ Δ : Functor (JudgmentsL _ _ (PCF n Γ Δ)) SystemFCa' (mapOptionTree brakifyJudg).
1346     refine {| fmor := ReificationFunctor_fmor Γ Δ |}; unfold hom; unfold ob; simpl ; intros.
1347
1348   Definition PCF_SMME (n:nat)(Γ:TypeEnv)(Δ:CoercionEnv Γ) : ProgrammingLanguageSMME.
1349     refine {| plsmme_pl := PCF n Γ Δ |}.
1350     Defined.
1351
1352   Definition SystemFCa_SMME (n:nat)(Γ:TypeEnv)(Δ:CoercionEnv Γ) : ProgrammingLanguageSMME.
1353     refine {| plsmme_pl := SystemFCa n Γ Δ |}.
1354     Defined.
1355
1356   Definition ReificationFunctorMonoidal n : MonoidalFunctor (JudgmentsN n) (JudgmentsN (S n)) (ReificationFunctor n).
1357     Defined.
1358
1359   (* 5.1.4 *)
1360   Definition PCF_SystemFCa_two_level n Γ Δ : TwoLevelLanguage (PCF_SMME n Γ Δ) (SystemFCa_SMME (S n) Γ Δ).
1361     Defined.
1362   *)
1363   (*  ... and the retraction exists *)
1364
1365 End HaskFlattener.
1366
1367 Implicit Arguments garrow [ ].