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 (hetmet_flatten : WeakExprVar).
 165   Context (hetmet_unflatten : WeakExprVar).
 166   Context (hetmet_id      : WeakExprVar).
 167   Context {unitTy : forall TV, RawHaskType TV ECKind  -> RawHaskType TV ★                                          }.
 168   Context {prodTy : forall TV, RawHaskType TV ECKind  -> RawHaskType TV ★  -> RawHaskType TV ★ -> RawHaskType TV ★ }.
 169   Context {gaTy   : forall TV, RawHaskType TV ECKind  -> RawHaskType TV ★ -> RawHaskType TV ★  -> RawHaskType TV ★ }.
 170
 171   Definition ga_mk_tree' {TV}(ec:RawHaskType TV ECKind)(tr:Tree ??(RawHaskType TV ★)) : RawHaskType TV ★ :=
 172     reduceTree (unitTy TV ec) (prodTy TV ec) tr.
 173
 174   Definition ga_mk_tree {Γ}(ec:HaskType Γ ECKind)(tr:Tree ??(HaskType Γ ★)) : HaskType Γ ★ :=
 175     fun TV ite => ga_mk_tree' (ec TV ite) (mapOptionTree (fun x => x TV ite) tr).
 176
 177   Definition ga_mk_raw {TV}(ec:RawHaskType TV ECKind)(ant suc:Tree ??(RawHaskType TV ★)) : RawHaskType TV ★ :=
 178     gaTy TV ec
 179     (ga_mk_tree' ec ant)
 180     (ga_mk_tree' ec suc).
 181
 182   Definition ga_mk {Γ}(ec:HaskType Γ ECKind)(ant suc:Tree ??(HaskType Γ ★)) : HaskType Γ ★ :=
 183     fun TV ite => gaTy TV (ec TV ite) (ga_mk_tree ec ant TV ite) (ga_mk_tree ec suc TV ite).
 184
 185   (*
 186    *  The story:
 187    *    - code types <[t]>@c                                                become garrows  c () t
 188    *    - free variables of type t at a level lev deeper than the succedent become garrows  c () t
 189    *    - free variables at the level of the succedent become
 190    *)
 191   Fixpoint flatten_rawtype {TV}{κ}(exp: RawHaskType TV κ) : RawHaskType TV κ :=
 192     match exp with
 193     | TVar    _  x          => TVar x
 194     | TAll     _ y          => TAll   _  (fun v => flatten_rawtype (y v))
 195     | TApp   _ _ x y        => TApp      (flatten_rawtype x) (flatten_rawtype y)
 196     | TCon       tc         => TCon      tc
 197     | TCoerc _ t1 t2 t      => TCoerc    (flatten_rawtype t1) (flatten_rawtype t2) (flatten_rawtype t)
 198     | TArrow                => TArrow
 199     | TCode     ec e        => let e' := flatten_rawtype e
 200                                in  ga_mk_raw ec (unleaves_ (take_arg_types e')) [drop_arg_types e']
 201     | TyFunApp  tfc kl k lt => TyFunApp tfc kl k (flatten_rawtype_list _ lt)
 202     end
 203     with flatten_rawtype_list {TV}(lk:list Kind)(exp:@RawHaskTypeList TV lk) : @RawHaskTypeList TV lk :=
 204     match exp in @RawHaskTypeList _ LK return @RawHaskTypeList TV LK with
 205     | TyFunApp_nil               => TyFunApp_nil
 206     | TyFunApp_cons  κ kl t rest => TyFunApp_cons _ _ (flatten_rawtype t) (flatten_rawtype_list _ rest)
 207     end.
 208
 209   Definition flatten_type {Γ}{κ}(ht:HaskType Γ κ) : HaskType Γ κ :=
 210     fun TV ite => flatten_rawtype (ht TV ite).
 211
 212   Fixpoint levels_to_tcode {Γ}(ht:HaskType Γ ★)(lev:HaskLevel Γ) : HaskType Γ ★ :=
 213     match lev with
 214       | nil      => flatten_type ht
 215       | ec::lev' => @ga_mk _ (v2t ec) [] [levels_to_tcode ht lev']
 216     end.
 217
 218   Definition flatten_leveled_type {Γ}(ht:LeveledHaskType Γ ★) : LeveledHaskType Γ ★ :=
 219     levels_to_tcode (unlev ht) (getlev ht) @@ nil.
 220
 221   (* AXIOMS *)
 222
 223   Axiom literal_types_unchanged : forall Γ l, flatten_type (literalType l) = literalType(Γ:=Γ) l.
 224
 225   Axiom flatten_coercion : forall Γ Δ κ (σ τ:HaskType Γ κ) (γ:HaskCoercion Γ Δ (σ ∼∼∼ τ)),
 226     HaskCoercion Γ Δ (flatten_type σ ∼∼∼ flatten_type τ).
 227
 228   Axiom flatten_commutes_with_substT :
 229     forall  κ Γ (Δ:CoercionEnv Γ) (σ:∀ TV, InstantiatedTypeEnv TV Γ → TV κ → RawHaskType TV ★) (τ:HaskType Γ κ),
 230     flatten_type  (substT σ τ) = substT (fun TV ite v => flatten_rawtype  (σ TV ite v))
 231       (flatten_type  τ).
 232
 233   Axiom flatten_commutes_with_HaskTAll :
 234     forall  κ Γ (Δ:CoercionEnv Γ) (σ:∀ TV, InstantiatedTypeEnv TV Γ → TV κ → RawHaskType TV ★),
 235     flatten_type  (HaskTAll κ σ) = HaskTAll κ (fun TV ite v => flatten_rawtype (σ TV ite v)).
 236
 237   Axiom flatten_commutes_with_HaskTApp :
 238     forall  κ Γ (Δ:CoercionEnv Γ) (σ:∀ TV, InstantiatedTypeEnv TV Γ → TV κ → RawHaskType TV ★),
 239     flatten_type  (HaskTApp (weakF σ) (FreshHaskTyVar κ)) =
 240     HaskTApp (weakF (fun TV ite v => flatten_rawtype  (σ TV ite v))) (FreshHaskTyVar κ).
 241
 242   Axiom flatten_commutes_with_weakLT : forall (Γ:TypeEnv) κ  t,
 243     flatten_leveled_type  (weakLT(Γ:=Γ)(κ:=κ) t) = weakLT(Γ:=Γ)(κ:=κ) (flatten_leveled_type  t).
 244
 245   Axiom globals_do_not_have_code_types : forall (Γ:TypeEnv) (g:Global Γ) v,
 246     flatten_type (g v) = g v.
 247
 248   (* "n" is the maximum depth remaining AFTER flattening *)
 249   Definition flatten_judgment (j:Judg) :=
 250     match j as J return Judg with
 251       | Γ > Δ > ant |- suc @ nil        => Γ > Δ > mapOptionTree flatten_leveled_type ant
 252                                                 |- mapOptionTree flatten_type suc @ nil
 253       | Γ > Δ > ant |- suc @ (ec::lev') => Γ > Δ > mapOptionTree flatten_leveled_type (drop_lev (ec::lev') ant)
 254                                                 |- [ga_mk (v2t ec)
 255                                                   (mapOptionTree (flatten_type ○ unlev) (take_lev (ec::lev') ant))
 256                                                   (mapOptionTree  flatten_type                               suc )
 257                                                   ] @ nil
 258     end.
 259
 260   Class garrow :=
 261   { ga_id        : ∀ Γ Δ ec l a    , ND Rule [] [Γ > Δ >                          [] |- [@ga_mk Γ ec a a ]@l ]
 262   ; ga_cancelr   : ∀ Γ Δ ec l a    , ND Rule [] [Γ > Δ >                          [] |- [@ga_mk Γ ec (a,,[]) a ]@l ]
 263   ; ga_cancell   : ∀ Γ Δ ec l a    , ND Rule [] [Γ > Δ >                          [] |- [@ga_mk Γ ec ([],,a) a ]@l ]
 264   ; ga_uncancelr : ∀ Γ Δ ec l a    , ND Rule [] [Γ > Δ >                          [] |- [@ga_mk Γ ec a (a,,[]) ]@l ]
 265   ; ga_uncancell : ∀ Γ Δ ec l a    , ND Rule [] [Γ > Δ >                          [] |- [@ga_mk Γ ec a ([],,a) ]@l ]
 266   ; ga_assoc     : ∀ Γ Δ ec l a b c, ND Rule [] [Γ > Δ >                          [] |- [@ga_mk Γ ec ((a,,b),,c) (a,,(b,,c)) ]@l ]
 267   ; ga_unassoc   : ∀ Γ Δ ec l a b c, ND Rule [] [Γ > Δ >                          [] |- [@ga_mk Γ ec (a,,(b,,c)) ((a,,b),,c) ]@l ]
 268   ; ga_swap      : ∀ Γ Δ ec l a b  , ND Rule [] [Γ > Δ >                          [] |- [@ga_mk Γ ec (a,,b) (b,,a) ]@l ]
 269   ; ga_drop      : ∀ Γ Δ ec l a    , ND Rule [] [Γ > Δ >                          [] |- [@ga_mk Γ ec a [] ]@l ]
 270   ; ga_copy      : ∀ Γ Δ ec l a    , ND Rule [] [Γ > Δ >                          [] |- [@ga_mk Γ ec a (a,,a) ]@l ]
 271   ; ga_first     : ∀ Γ Δ ec l a b x, ND Rule [] [Γ > Δ >      [@ga_mk Γ ec a b @@l] |- [@ga_mk Γ ec (a,,x) (b,,x) ]@l ]
 272   ; ga_second    : ∀ Γ Δ ec l a b x, ND Rule [] [Γ > Δ >      [@ga_mk Γ ec a b @@l] |- [@ga_mk Γ ec (x,,a) (x,,b) ]@l ]
 273   ; ga_lit       : ∀ Γ Δ ec l lit  , ND Rule [] [Γ > Δ >                          [] |- [@ga_mk Γ ec [] [literalType lit] ]@l ]
 274   ; ga_curry     : ∀ Γ Δ ec l a b c, ND Rule [] [Γ > Δ > [@ga_mk Γ ec (a,,[b]) [c] @@ l] |- [@ga_mk Γ ec a [b ---> c] ]@ l ]
 275   ; 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 ]
 276   ; ga_apply     : ∀ Γ Δ ec l a a' b c,
 277                  ND Rule [] [Γ > Δ > [@ga_mk Γ ec a [b ---> c] @@ l],,[@ga_mk Γ ec a' [b] @@ l] |- [@ga_mk Γ ec (a,,a') [c] ]@l ]
 278   ; ga_kappa     : ∀ Γ Δ ec l a b Σ, ND Rule
 279   [Γ > Δ > Σ,,[@ga_mk Γ ec [] a @@ l] |- [@ga_mk Γ ec [] b ]@l ]
 280   [Γ > Δ > Σ          |- [@ga_mk Γ ec a  b ]@l ]
 281   }.
 282   Context `(gar:garrow).
 283
 284   Notation "a ~~~~> b" := (@ga_mk _ _ a b) (at level 20).
 285
 286   Definition boost : forall Γ Δ ant x y {lev},
 287     ND Rule []                         [ Γ > Δ > [x@@lev] |- [y]@lev ] ->
 288     ND Rule [ Γ > Δ > ant |- [x]@lev ] [ Γ > Δ > ant      |- [y]@lev ].
 289     intros.
 290     eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ACanR ].
 291     eapply nd_comp; [ idtac | eapply nd_rule; apply RLet ].
 292     eapply nd_comp; [ apply nd_rlecnac | idtac ].
 293     apply nd_prod.
 294     apply nd_id.
 295     eapply nd_comp.
 296       apply X.
 297       eapply nd_rule.
 298       eapply RArrange.
 299       apply AuCanR.
 300     Defined.
 301
 302   Definition precompose Γ Δ ec : forall a x y z lev,
 303     ND Rule
 304       [ Γ > Δ > a                           |- [@ga_mk _ ec y z ]@lev ]
 305       [ Γ > Δ > a,,[@ga_mk _ ec x y @@ lev] |- [@ga_mk _ ec x z ]@lev ].
 306     intros.
 307     eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
 308     eapply nd_comp; [ apply nd_rlecnac | idtac ].
 309     apply nd_prod.
 310     apply nd_id.
 311     eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AExch ].
 312     apply ga_comp.
 313     Defined.
 314
 315   Definition precompose' Γ Δ ec : forall a b x y z lev,
 316     ND Rule
 317       [ Γ > Δ > a,,b                             |- [@ga_mk _ ec y z ]@lev ]
 318       [ Γ > Δ > a,,([@ga_mk _ ec x y @@ lev],,b) |- [@ga_mk _ ec x z ]@lev ].
 319     intros.
 320     eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ALeft; eapply AExch ].
 321     eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AuAssoc ].
 322     apply precompose.
 323     Defined.
 324
 325   Definition postcompose_ Γ Δ ec : forall a x y z lev,
 326     ND Rule
 327       [ Γ > Δ > a                           |- [@ga_mk _ ec x y ]@lev ]
 328       [ Γ > Δ > a,,[@ga_mk _ ec y z @@ lev] |- [@ga_mk _ ec x z ]@lev ].
 329     intros.
 330     eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
 331     eapply nd_comp; [ apply nd_rlecnac | idtac ].
 332     apply nd_prod.
 333     apply nd_id.
 334     apply ga_comp.
 335     Defined.
 336
 337   Definition postcompose  Γ Δ ec : forall x y z lev,
 338     ND Rule [] [ Γ > Δ > []                       |- [@ga_mk _ ec x y ]@lev ] ->
 339     ND Rule [] [ Γ > Δ > [@ga_mk _ ec y z @@ lev] |- [@ga_mk _ ec x z ]@lev ].
 340     intros.
 341     eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ACanL ].
 342     eapply nd_comp; [ idtac | eapply postcompose_ ].
 343     apply X.
 344     Defined.
 345
 346   Definition first_nd : ∀ Γ Δ ec lev a b c Σ,
 347     ND Rule [ Γ > Δ > Σ                    |- [@ga_mk Γ ec a b ]@lev ]
 348             [ Γ > Δ > Σ                    |- [@ga_mk Γ ec (a,,c) (b,,c) ]@lev ].
 349     intros.
 350     eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ACanR ].
 351     eapply nd_comp; [ idtac | eapply nd_rule; apply RLet ].
 352     eapply nd_comp; [ apply nd_rlecnac | idtac ].
 353     apply nd_prod.
 354     apply nd_id.
 355     eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AuCanR ].
 356     apply ga_first.
 357     Defined.
 358
 359   Definition firstify : ∀ Γ Δ ec lev a b c Σ,
 360     ND Rule [] [ Γ > Δ > Σ                    |- [@ga_mk Γ ec a b ]@lev ] ->
 361     ND Rule [] [ Γ > Δ > Σ                    |- [@ga_mk Γ ec (a,,c) (b,,c) ]@lev ].
 362     intros.
 363     eapply nd_comp.
 364     apply X.
 365     apply first_nd.
 366     Defined.
 367
 368   Definition second_nd : ∀ Γ Δ ec lev a b c Σ,
 369      ND Rule
 370      [ Γ > Δ > Σ                    |- [@ga_mk Γ ec a b ]@lev ]
 371      [ Γ > Δ > Σ                    |- [@ga_mk Γ ec (c,,a) (c,,b) ]@lev ].
 372     intros.
 373     eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ACanR ].
 374     eapply nd_comp; [ idtac | eapply nd_rule; apply RLet ].
 375     eapply nd_comp; [ apply nd_rlecnac | idtac ].
 376     apply nd_prod.
 377     apply nd_id.
 378     eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AuCanR ].
 379     apply ga_second.
 380     Defined.
 381
 382   Definition secondify : ∀ Γ Δ ec lev a b c Σ,
 383      ND Rule [] [ Γ > Δ > Σ                    |- [@ga_mk Γ ec a b ]@lev ] ->
 384      ND Rule [] [ Γ > Δ > Σ                    |- [@ga_mk Γ ec (c,,a) (c,,b) ]@lev ].
 385     intros.
 386     eapply nd_comp.
 387     apply X.
 388     apply second_nd.
 389     Defined.
 390
 391    Lemma ga_unkappa     : ∀ Γ Δ ec l a b Σ x,
 392      ND Rule
 393      [Γ > Δ > Σ                          |- [@ga_mk Γ ec (a,,x)  b ]@l ]
 394      [Γ > Δ > Σ,,[@ga_mk Γ ec [] a @@ l] |- [@ga_mk Γ ec x       b ]@l ].
 395      intros.
 396      eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AExch ].
 397      eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
 398      eapply nd_comp; [ apply nd_llecnac | idtac ].
 399      apply nd_prod.
 400      apply ga_first.
 401
 402      eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
 403      eapply nd_comp; [ apply nd_llecnac | idtac ].
 404      apply nd_prod.
 405      apply postcompose.
 406      apply ga_uncancell.
 407      eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AExch ].
 408      apply precompose.
 409      Defined.
 410
 411   (* useful for cutting down on the pretty-printed noise
 412
 413   Notation "`  x" := (take_lev _ x) (at level 20).
 414   Notation "`` x" := (mapOptionTree unlev x) (at level 20).
 415   Notation "``` x" := (drop_lev _ x) (at level 20).
 416   *)
 417   Definition flatten_arrangement' :
 418     forall Γ (Δ:CoercionEnv Γ)
 419       (ec:HaskTyVar Γ ECKind) (lev:HaskLevel Γ) (ant1 ant2:Tree ??(LeveledHaskType Γ ★)) (r:Arrange ant1 ant2),
 420       ND Rule [] [Γ > Δ > [] |- [@ga_mk _ (v2t ec) (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) ant2))
 421         (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) ant1)) ]@nil ].
 422
 423       intros Γ Δ ec lev.
 424       refine (fix flatten ant1 ant2 (r:Arrange ant1 ant2):
 425            ND Rule [] [Γ > Δ > [] |- [@ga_mk _ (v2t ec)
 426              (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) ant2))
 427              (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) ant1)) ]@nil] :=
 428         match r as R in Arrange A B return
 429           ND Rule [] [Γ > Δ > [] |- [@ga_mk _ (v2t ec)
 430             (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) B))
 431             (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) A)) ]@nil]
 432           with
 433           | AId  a               => let case_AId := tt    in ga_id _ _ _ _ _
 434           | ACanL  a             => let case_ACanL := tt  in ga_uncancell _ _ _ _ _
 435           | ACanR  a             => let case_ACanR := tt  in ga_uncancelr _ _ _ _ _
 436           | AuCanL a             => let case_AuCanL := tt in ga_cancell _ _ _ _ _
 437           | AuCanR a             => let case_AuCanR := tt in ga_cancelr _ _ _ _ _
 438           | AAssoc a b c         => let case_AAssoc := tt in ga_assoc _ _ _ _ _ _ _
 439           | AuAssoc a b c         => let case_AuAssoc := tt in ga_unassoc _ _ _ _ _ _ _
 440           | AExch  a b           => let case_AExch := tt  in ga_swap  _ _ _ _ _ _
 441           | AWeak  a             => let case_AWeak := tt  in ga_drop _ _ _ _ _
 442           | ACont  a             => let case_ACont := tt  in ga_copy  _ _ _ _ _
 443           | ALeft  a b c r'      => let case_ALeft := tt  in flatten _ _ r' ;; boost _ _ _ _ _ (ga_second _ _ _ _ _ _ _)
 444           | ARight a b c r'      => let case_ARight := tt in flatten _ _ r' ;; boost _ _ _ _ _ (ga_first  _ _ _ _ _ _ _)
 445           | AComp  c b a r1 r2   => let case_AComp := tt  in (fun r1' r2' => _) (flatten _ _ r1) (flatten _ _ r2)
 446         end); clear flatten; repeat take_simplify; repeat drop_simplify; intros.
 447
 448         destruct case_AComp.
 449           set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) a)) as a' in *.
 450           set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) b)) as b' in *.
 451           set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) c)) as c' in *.
 452           eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply ACanL ].
 453           eapply nd_comp; [ idtac | eapply nd_rule; apply
 454              (@RLet Γ Δ [] [] (@ga_mk _ (v2t ec) a' b') (@ga_mk _ (v2t ec) a' c')) ].
 455           eapply nd_comp; [ apply nd_llecnac | idtac ].
 456           apply nd_prod.
 457           apply r2'.
 458           eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply AuCanR ].
 459           eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply ACanL ].
 460           eapply nd_comp; [ idtac | eapply nd_rule;  apply RLet ].
 461           eapply nd_comp; [ apply nd_llecnac | idtac ].
 462           eapply nd_prod.
 463           apply r1'.
 464           eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AExch ].
 465           apply ga_comp.
 466           Defined.
 467
 468   Definition flatten_arrangement :
 469     forall Γ (Δ:CoercionEnv Γ) n
 470       (ec:HaskTyVar Γ ECKind) (lev:HaskLevel Γ) (ant1 ant2:Tree ??(LeveledHaskType Γ ★)) (r:Arrange ant1 ant2) succ,
 471       ND Rule
 472       [Γ > Δ > mapOptionTree (flatten_leveled_type ) (drop_lev n ant1)
 473         |- [@ga_mk _ (v2t ec)
 474           (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) ant1))
 475           (mapOptionTree (flatten_type ) succ) ]@nil]
 476       [Γ > Δ > mapOptionTree (flatten_leveled_type ) (drop_lev n ant2)
 477         |- [@ga_mk _ (v2t ec)
 478           (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) ant2))
 479           (mapOptionTree (flatten_type ) succ) ]@nil].
 480       intros.
 481       refine ( _ ;; (boost _ _ _ _ _ (postcompose _ _ _ _ _ _ _ (flatten_arrangement' Γ Δ ec lev ant1 ant2 r)))).
 482       apply nd_rule.
 483       apply RArrange.
 484       refine ((fix flatten ant1 ant2 (r:Arrange ant1 ant2) :=
 485         match r as R in Arrange A B return
 486           Arrange (mapOptionTree (flatten_leveled_type ) (drop_lev _ A))
 487           (mapOptionTree (flatten_leveled_type ) (drop_lev _ B)) with
 488           | AId  a               => let case_AId := tt  in AId _
 489           | ACanL  a             => let case_ACanL := tt  in ACanL _
 490           | ACanR  a             => let case_ACanR := tt  in ACanR _
 491           | AuCanL a             => let case_AuCanL := tt in AuCanL _
 492           | AuCanR a             => let case_AuCanR := tt in AuCanR _
 493           | AAssoc a b c         => let case_AAssoc := tt in AAssoc _ _ _
 494           | AuAssoc a b c         => let case_AuAssoc := tt in AuAssoc _ _ _
 495           | AExch  a b           => let case_AExch := tt  in AExch _ _
 496           | AWeak  a             => let case_AWeak := tt  in AWeak _
 497           | ACont  a             => let case_ACont := tt  in ACont _
 498           | ALeft  a b c r'      => let case_ALeft := tt  in ALeft  _ (flatten _ _ r')
 499           | ARight a b c r'      => let case_ARight := tt in ARight _ (flatten _ _ r')
 500           | AComp  a b c r1 r2   => let case_AComp := tt  in AComp    (flatten _ _ r1) (flatten _ _ r2)
 501         end) ant1 ant2 r); clear flatten; repeat take_simplify; repeat drop_simplify; intros.
 502         Defined.
 503
 504   Definition flatten_arrangement'' :
 505     forall  Γ Δ ant1 ant2 succ l (r:Arrange ant1 ant2),
 506       ND Rule (mapOptionTree (flatten_judgment ) [Γ > Δ > ant1 |- succ @ l])
 507       (mapOptionTree (flatten_judgment ) [Γ > Δ > ant2 |- succ @ l]).
 508     intros.
 509     simpl.
 510     destruct l.
 511       apply nd_rule.
 512       apply RArrange.
 513       induction r; simpl.
 514         apply AId.
 515         apply ACanL.
 516         apply ACanR.
 517         apply AuCanL.
 518         apply AuCanR.
 519         apply AAssoc.
 520         apply AuAssoc.
 521         apply AExch.    (* TO DO: check for all-leaf trees here *)
 522         apply AWeak.
 523         apply ACont.
 524         apply ALeft; auto.
 525         apply ARight; auto.
 526         eapply AComp; [ apply IHr1 | apply IHr2 ].
 527
 528       apply flatten_arrangement.
 529         apply r.
 530         Defined.
 531
 532   Definition ga_join Γ Δ Σ₁ Σ₂ a b ec :
 533     ND Rule [] [Γ > Δ > Σ₁     |- [@ga_mk _ ec [] a      ]@nil] ->
 534     ND Rule [] [Γ > Δ > Σ₂     |- [@ga_mk _ ec [] b      ]@nil] ->
 535     ND Rule [] [Γ > Δ > Σ₁,,Σ₂ |- [@ga_mk _ ec [] (a,,b) ]@nil].
 536     intro pfa.
 537     intro pfb.
 538     apply secondify with (c:=a)  in pfb.
 539     apply firstify  with (c:=[])  in pfa.
 540     eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
 541     eapply nd_comp; [ eapply nd_llecnac | idtac ].
 542     apply nd_prod.
 543     apply pfa.
 544     clear pfa.
 545
 546     eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
 547     eapply nd_comp; [ apply nd_llecnac | idtac ].
 548     apply nd_prod.
 549     eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ACanL ].
 550     eapply nd_comp; [ idtac | eapply postcompose_ ].
 551     apply ga_uncancelr.
 552
 553     eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AExch ].
 554     eapply nd_comp; [ idtac | eapply precompose ].
 555     apply pfb.
 556     Defined.
 557
 558   Definition arrange_brak : forall Γ Δ ec succ t,
 559    ND Rule
 560      [Γ > Δ >
 561       [(@ga_mk _ (v2t ec) [] (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: nil) succ))) @@  nil],,
 562       mapOptionTree (flatten_leveled_type ) (drop_lev (ec :: nil) succ) |- [t]@nil]
 563      [Γ > Δ > mapOptionTree (flatten_leveled_type ) succ |- [t]@nil].
 564
 565     intros.
 566     unfold drop_lev.
 567     set (@arrangeUnPartition _ succ (levelMatch (ec::nil))) as q.
 568     set (arrangeMap _ _ flatten_leveled_type q) as y.
 569     eapply nd_comp.
 570     Focus 2.
 571     eapply nd_rule.
 572     eapply RArrange.
 573     apply y.
 574     idtac.
 575     clear y q.
 576     eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AExch ].
 577     simpl.
 578     eapply nd_comp; [ apply nd_llecnac | idtac ].
 579     eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
 580     apply nd_prod.
 581     Focus 2.
 582     apply nd_id.
 583     idtac.
 584     induction succ; try destruct a; simpl.
 585     unfold take_lev.
 586     unfold mkTakeFlags.
 587     unfold mkFlags.
 588     unfold bnot.
 589     simpl.
 590     destruct l as [t' lev'].
 591     destruct lev' as [|ec' lev'].
 592     simpl.
 593     apply ga_id.
 594     unfold levelMatch.
 595     set (@eqd_dec (HaskLevel Γ) (haskLevelEqDecidable Γ) (ec' :: lev') (ec :: nil)) as q.
 596     destruct q.
 597     inversion e; subst.
 598     simpl.
 599     apply nd_rule.
 600     unfold flatten_leveled_type.
 601     simpl.
 602     unfold flatten_type.
 603     simpl.
 604     unfold ga_mk.
 605     simpl.
 606     apply RVar.
 607     simpl.
 608     apply ga_id.
 609     apply ga_id.
 610     unfold take_lev.
 611     simpl.
 612     apply ga_join.
 613       apply IHsucc1.
 614       apply IHsucc2.
 615     Defined.
 616
 617   Definition arrange_esc : forall Γ Δ ec succ t,
 618    ND Rule
 619      [Γ > Δ > mapOptionTree (flatten_leveled_type ) succ |- [t]@nil]
 620      [Γ > Δ >
 621       [(@ga_mk _ (v2t ec) [] (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: nil) succ))) @@  nil],,
 622       mapOptionTree (flatten_leveled_type ) (drop_lev (ec :: nil) succ)  |- [t]@nil].
 623     intros.
 624     set (@arrangePartition _ succ (levelMatch (ec::nil))) as q.
 625     set (@drop_lev Γ (ec::nil) succ) as q'.
 626     assert (@drop_lev Γ (ec::nil) succ=q') as H.
 627       reflexivity.
 628     unfold drop_lev in H.
 629     unfold mkDropFlags in H.
 630     rewrite H in q.
 631     clear H.
 632     set (arrangeMap _ _ flatten_leveled_type q) as y.
 633     eapply nd_comp.
 634     eapply nd_rule.
 635     eapply RArrange.
 636     apply y.
 637     clear y q.
 638
 639     set (mapOptionTree flatten_leveled_type (dropT (mkFlags (liftBoolFunc false (bnot ○ levelMatch (ec :: nil))) succ))) as q.
 640     destruct (decide_tree_empty q); [ idtac | apply (Prelude_error "escapifying open code not yet supported") ].
 641     destruct s.
 642
 643     simpl.
 644     eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply AExch ].
 645     set (fun z z' => @RLet Γ Δ z (mapOptionTree flatten_leveled_type q') t z' nil) as q''.
 646     eapply nd_comp; [ idtac | eapply nd_rule; apply RLet ].
 647     clear q''.
 648     eapply nd_comp; [ apply nd_rlecnac | idtac ].
 649     apply nd_prod.
 650     apply nd_rule.
 651     apply RArrange.
 652     eapply AComp; [ idtac | apply ACanR ].
 653     apply ALeft.
 654     apply (@arrangeCancelEmptyTree _ _ _ _ e).
 655
 656     eapply nd_comp.
 657       eapply nd_rule.
 658       eapply (@RVar Γ Δ t nil).
 659     apply nd_rule.
 660       apply RArrange.
 661       eapply AComp.
 662       apply AuCanR.
 663       apply ALeft.
 664       apply AWeak.
 665 (*
 666     eapply decide_tree_empty.
 667
 668     simpl.
 669     set (dropT (mkFlags (liftBoolFunc false (bnot ○ levelMatch (ec :: nil))) succ)) as escapified.
 670     destruct (decide_tree_empty escapified).
 671
 672     induction succ.
 673     destruct a.
 674       unfold drop_lev.
 675       destruct l.
 676       simpl.
 677       unfold mkDropFlags; simpl.
 678       unfold take_lev.
 679       unfold mkTakeFlags.
 680       simpl.
 681       destruct (General.list_eq_dec h0 (ec :: nil)).
 682         simpl.
 683         rewrite e.
 684         apply nd_id.
 685         simpl.
 686         apply nd_rule.
 687         apply RArrange.
 688         apply ALeft.
 689         apply AWeak.
 690       simpl.
 691         apply nd_rule.
 692         unfold take_lev.
 693         simpl.
 694         apply RArrange.
 695         apply ALeft.
 696         apply AWeak.
 697       apply (Prelude_error "escapifying code with multi-leaf antecedents is not supported").
 698 *)
 699       Defined.
 700
 701   Lemma unlev_relev : forall {Γ}(t:Tree ??(HaskType Γ ★)) lev, mapOptionTree unlev (t @@@ lev) = t.
 702     intros.
 703     induction t.
 704     destruct a; reflexivity.
 705     rewrite <- IHt1 at 2.
 706     rewrite <- IHt2 at 2.
 707     reflexivity.
 708     Qed.
 709
 710   Lemma tree_of_nothing : forall Γ ec t,
 711     Arrange (mapOptionTree flatten_leveled_type (drop_lev(Γ:=Γ) (ec :: nil) (t @@@ (ec :: nil)))) [].
 712     intros.
 713     induction t; try destruct o; try destruct a.
 714     simpl.
 715     drop_simplify.
 716     simpl.
 717     apply AId.
 718     simpl.
 719     apply AId.
 720     eapply AComp; [ idtac | apply ACanL ].
 721     eapply AComp; [ idtac | eapply ALeft; apply IHt2 ].
 722     Opaque drop_lev.
 723     simpl.
 724     Transparent drop_lev.
 725     idtac.
 726     drop_simplify.
 727     apply ARight.
 728     apply IHt1.
 729     Defined.
 730
 731   Lemma tree_of_nothing' : forall Γ ec t,
 732     Arrange [] (mapOptionTree flatten_leveled_type (drop_lev(Γ:=Γ) (ec :: nil) (t @@@ (ec :: nil)))).
 733     intros.
 734     induction t; try destruct o; try destruct a.
 735     simpl.
 736     drop_simplify.
 737     simpl.
 738     apply AId.
 739     simpl.
 740     apply AId.
 741     eapply AComp; [ apply AuCanL | idtac ].
 742     eapply AComp; [ eapply ARight; apply IHt1 | idtac ].
 743     Opaque drop_lev.
 744     simpl.
 745     Transparent drop_lev.
 746     idtac.
 747     drop_simplify.
 748     apply ALeft.
 749     apply IHt2.
 750     Defined.
 751
 752   Lemma krunk : forall Γ (ec:HaskTyVar Γ ECKind) t,
 753     flatten_type (<[ ec |- t ]>)
 754     = @ga_mk Γ (v2t ec)
 755     (mapOptionTree flatten_type (take_arg_types_as_tree t))
 756     [ flatten_type (drop_arg_types_as_tree   t)].
 757     intros.
 758     unfold flatten_type at 1.
 759     simpl.
 760     unfold ga_mk.
 761     apply phoas_extensionality.
 762     intros.
 763     unfold v2t.
 764     unfold ga_mk_raw.
 765     unfold ga_mk_tree.
 766     rewrite <- mapOptionTree_compose.
 767     unfold take_arg_types_as_tree.
 768     simpl.
 769     replace (flatten_type (drop_arg_types_as_tree t) tv ite)
 770       with (drop_arg_types (flatten_rawtype (t tv ite))).
 771     replace (unleaves_ (take_arg_types (flatten_rawtype (t tv ite))))
 772       with ((mapOptionTree (fun x : HaskType Γ ★ => flatten_type x tv ite)
 773            (unleaves_
 774               (take_trustme (count_arg_types (t (fun _ : Kind => unit) (ite_unit Γ)))
 775                  (fun TV : Kind → Type => take_arg_types ○ t TV))))).
 776     reflexivity.
 777     unfold flatten_type.
 778     clear hetmet_flatten.
 779     clear hetmet_unflatten.
 780     clear hetmet_id.
 781     clear gar.
 782     set (t tv ite) as x.
 783     admit.
 784     admit.
 785     Qed.
 786
 787   Lemma drop_to_nothing : forall (Γ:TypeEnv) Σ (lev:HaskLevel Γ),
 788     drop_lev lev (Σ @@@ lev) = mapTree (fun _ => None) (mapTree (fun _ => tt) Σ).
 789     intros.
 790     induction Σ.
 791     destruct a; simpl.
 792     drop_simplify.
 793     auto.
 794     drop_simplify.
 795     auto.
 796     simpl.
 797     rewrite <- IHΣ1.
 798     rewrite <- IHΣ2.
 799     reflexivity.
 800     Qed.
 801
 802   Definition flatten_skolemized_proof :
 803     forall  {h}{c},
 804       ND SRule h c ->
 805       ND  Rule (mapOptionTree (flatten_judgment ) h) (mapOptionTree (flatten_judgment ) c).
 806     intros.
 807     eapply nd_map'; [ idtac | apply X ].
 808     clear h c X.
 809     intros.
 810     simpl in *.
 811
 812     refine
 813       (match X as R in SRule H C with
 814       | SBrak    Γ Δ t ec succ lev           => let case_SBrak := tt         in _
 815       | SEsc     Γ Δ t ec succ lev           => let case_SEsc := tt          in _
 816       | SFlat    h c r                       => let case_SFlat := tt         in _
 817       end).
 818
 819     destruct case_SFlat.
 820     refine (match r as R in Rule H C with
 821       | RArrange Γ Δ a b x l d         => let case_RArrange := tt      in _
 822       | RNote    Γ Δ Σ τ l n           => let case_RNote := tt         in _
 823       | RLit     Γ Δ l     _           => let case_RLit := tt          in _
 824       | RVar     Γ Δ σ           lev   => let case_RVar := tt          in _
 825       | RGlobal  Γ Δ σ l wev           => let case_RGlobal := tt       in _
 826       | RLam     Γ Δ Σ tx te     lev   => let case_RLam := tt          in _
 827       | RCast    Γ Δ Σ σ τ lev γ       => let case_RCast := tt         in _
 828       | RAbsT    Γ Δ Σ κ σ lev         => let case_RAbsT := tt         in _
 829       | RAppT    Γ Δ Σ κ σ τ     lev   => let case_RAppT := tt         in _
 830       | RAppCo   Γ Δ Σ κ σ₁ σ₂ γ σ lev => let case_RAppCo := tt        in _
 831       | RAbsCo   Γ Δ Σ κ σ  σ₁ σ₂  lev => let case_RAbsCo := tt        in _
 832       | RApp     Γ Δ Σ₁ Σ₂ tx te lev   => let case_RApp := tt          in _
 833       | RLet     Γ Δ Σ₁ Σ₂ σ₁ σ₂ lev   => let case_RLet := tt          in _
 834       | RCut     Γ Δ Σ Σ₁ Σ₁₂ Σ₂ Σ₃ l  => let case_RCut := tt          in _
 835       | RLeft    Γ Δ Σ₁ Σ₂  Σ     l    => let case_RLeft := tt in _
 836       | RRight   Γ Δ Σ₁ Σ₂  Σ     l    => let case_RRight := tt in _
 837       | RWhere   Γ Δ Σ₁ Σ₂ Σ₃ σ₁ σ₂ lev   => let case_RWhere := tt          in _
 838       | RVoid    _ _       l           => let case_RVoid := tt   in _
 839       | RBrak    Γ Δ t ec succ lev           => let case_RBrak := tt         in _
 840       | REsc     Γ Δ t ec succ lev           => let case_REsc := tt          in _
 841       | RCase    Γ Δ lev tc Σ avars tbranches alts => let case_RCase := tt         in _
 842       | RLetRec  Γ Δ lri x y t         => let case_RLetRec := tt       in _
 843       end); clear X h c.
 844
 845     destruct case_RArrange.
 846       apply (flatten_arrangement''  Γ Δ a b x _ d).
 847
 848     destruct case_RBrak.
 849       apply (Prelude_error "found unskolemized Brak rule; this shouldn't happen").
 850
 851     destruct case_REsc.
 852       apply (Prelude_error "found unskolemized Esc rule; this shouldn't happen").
 853
 854     destruct case_RNote.
 855       simpl.
 856       destruct l; simpl.
 857         apply nd_rule; apply RNote; auto.
 858         apply nd_rule; apply RNote; auto.
 859
 860     destruct case_RLit.
 861       simpl.
 862       destruct l0; simpl.
 863         unfold flatten_leveled_type.
 864         simpl.
 865         rewrite literal_types_unchanged.
 866           apply nd_rule; apply RLit.
 867         unfold take_lev; simpl.
 868         unfold drop_lev; simpl.
 869         simpl.
 870         rewrite literal_types_unchanged.
 871         apply ga_lit.
 872
 873     destruct case_RVar.
 874       Opaque flatten_judgment.
 875       simpl.
 876       Transparent flatten_judgment.
 877       idtac.
 878       unfold flatten_judgment.
 879       destruct lev.
 880       apply nd_rule. apply RVar.
 881       repeat drop_simplify.
 882       repeat take_simplify.
 883       simpl.
 884       apply ga_id.
 885
 886     destruct case_RGlobal.
 887       simpl.
 888       rename l into g.
 889       rename σ into l.
 890       destruct l as [|ec lev]; simpl.
 891         destruct (eqd_dec (g:CoreVar) (hetmet_flatten:CoreVar)).
 892           set (flatten_type (g wev)) as t.
 893           set (RGlobal _ Δ nil (mkGlobal Γ t hetmet_id)) as q.
 894           simpl in q.
 895           apply nd_rule.
 896           apply q.
 897           apply INil.
 898         destruct (eqd_dec (g:CoreVar) (hetmet_unflatten:CoreVar)).
 899           set (flatten_type (g wev)) as t.
 900           set (RGlobal _ Δ nil (mkGlobal Γ t hetmet_id)) as q.
 901           simpl in q.
 902           apply nd_rule.
 903           apply q.
 904           apply INil.
 905         unfold flatten_leveled_type. simpl.
 906           apply nd_rule; rewrite globals_do_not_have_code_types.
 907           apply RGlobal.
 908       apply (Prelude_error "found RGlobal at depth >0; globals should never appear inside code brackets unless escaped").
 909
 910     destruct case_RLam.
 911       Opaque drop_lev.
 912       Opaque take_lev.
 913       simpl.
 914       destruct lev as [|ec lev]; simpl; [ apply nd_rule; apply RLam; auto | idtac ].
 915       repeat drop_simplify.
 916       repeat take_simplify.
 917       eapply nd_comp.
 918         eapply nd_rule.
 919         eapply RArrange.
 920         simpl.
 921         apply ACanR.
 922       apply boost.
 923       simpl.
 924       apply ga_curry.
 925
 926     destruct case_RCast.
 927       simpl.
 928       destruct lev as [|ec lev]; simpl; [ apply nd_rule; apply RCast; auto | idtac ].
 929       simpl.
 930       apply flatten_coercion; auto.
 931       apply (Prelude_error "RCast at level >0; casting inside of code brackets is currently not supported").
 932
 933     destruct case_RApp.
 934       simpl.
 935
 936       destruct lev as [|ec lev].
 937         unfold flatten_type at 1.
 938         simpl.
 939         apply nd_rule.
 940         apply RApp.
 941
 942         repeat drop_simplify.
 943           repeat take_simplify.
 944           rewrite mapOptionTree_distributes.
 945           set (mapOptionTree (flatten_leveled_type ) (drop_lev (ec :: lev) Σ₁)) as Σ₁'.
 946           set (mapOptionTree (flatten_leveled_type ) (drop_lev (ec :: lev) Σ₂)) as Σ₂'.
 947           set (take_lev (ec :: lev) Σ₁) as Σ₁''.
 948           set (take_lev (ec :: lev) Σ₂) as Σ₂''.
 949           replace (flatten_type  (tx ---> te)) with ((flatten_type  tx) ---> (flatten_type  te)).
 950           apply (Prelude_error "FIXME: ga_apply").
 951           reflexivity.
 952
 953 (*
 954   Notation "`  x" := (take_lev _ x).
 955   Notation "`` x" := (mapOptionTree unlev x) (at level 20).
 956   Notation "``` x" := ((drop_lev _ x)) (at level 20).
 957   Notation "!<[]> x" := (flatten_type _ x) (at level 1).
 958   Notation "!<[@]> x" := (mapOptionTree flatten_leveled_type x) (at level 1).
 959 *)
 960
 961     destruct case_RLet.
 962       simpl.
 963       destruct lev as [|ec lev]; simpl; [ apply nd_rule; apply RLet; auto | idtac ].
 964       repeat drop_simplify.
 965       repeat take_simplify.
 966       simpl.
 967
 968       set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) Σ₁)) as Σ₁'.
 969       set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) Σ₂)) as Σ₂'.
 970       set (mapOptionTree flatten_leveled_type (drop_lev (ec :: lev) Σ₁)) as Σ₁''.
 971       set (mapOptionTree flatten_leveled_type (drop_lev (ec :: lev) Σ₂)) as Σ₂''.
 972
 973       eapply nd_comp.
 974       eapply nd_prod; [ idtac | apply nd_id ].
 975       eapply boost.
 976       apply (ga_first _ _ _ _ _ _ Σ₂').
 977
 978       eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
 979       apply nd_prod.
 980       apply nd_id.
 981       eapply nd_comp; [ eapply nd_rule; eapply RArrange; eapply ACanL | idtac ].
 982       eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AExch (* okay *)].
 983       apply precompose.
 984
 985     destruct case_RWhere.
 986       simpl.
 987       destruct lev as [|ec lev]; simpl; [ apply nd_rule; apply RWhere; auto | idtac ].
 988       repeat take_simplify.
 989       repeat drop_simplify.
 990       simpl.
 991
 992       set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) Σ₁)) as Σ₁'.
 993       set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) Σ₂)) as Σ₂'.
 994       set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) Σ₃)) as Σ₃'.
 995       set (mapOptionTree flatten_leveled_type (drop_lev (ec :: lev) Σ₁)) as Σ₁''.
 996       set (mapOptionTree flatten_leveled_type (drop_lev (ec :: lev) Σ₂)) as Σ₂''.
 997       set (mapOptionTree flatten_leveled_type (drop_lev (ec :: lev) Σ₃)) as Σ₃''.
 998
 999       eapply nd_comp.
1000       eapply nd_prod; [ eapply nd_id | idtac ].
1001       eapply (first_nd _ _ _ _ _ _ Σ₃').
1002       eapply nd_comp.
1003       eapply nd_prod; [ eapply nd_id | idtac ].
1004       eapply (second_nd _ _ _ _ _ _ Σ₁').
1005
1006       eapply nd_comp; [ idtac | eapply nd_rule; eapply RWhere ].
1007       apply nd_prod; [ idtac | apply nd_id ].
1008       eapply nd_comp; [ idtac | eapply precompose' ].
1009       apply nd_rule.
1010       apply RArrange.
1011       apply ALeft.
1012       apply ACanL.
1013
1014     destruct case_RCut.
1015       simpl.
1016       destruct l as [|ec lev]; simpl.
1017         apply nd_rule.
1018         replace (mapOptionTree flatten_leveled_type (Σ₁₂ @@@ nil)) with (mapOptionTree flatten_type Σ₁₂ @@@ nil).
1019         apply RCut.
1020         induction Σ₁₂; try destruct a; auto.
1021         simpl.
1022         rewrite <- IHΣ₁₂1.
1023         rewrite <- IHΣ₁₂2.
1024         reflexivity.
1025       simpl; repeat drop_simplify.
1026       simpl; repeat take_simplify.
1027       simpl.
1028       set (drop_lev (ec :: lev) (Σ₁₂ @@@ (ec :: lev))) as x1.
1029       rewrite take_lemma'.
1030       rewrite mapOptionTree_compose.
1031       rewrite mapOptionTree_compose.
1032       rewrite mapOptionTree_compose.
1033       rewrite mapOptionTree_compose.
1034       rewrite unlev_relev.
1035       rewrite <- mapOptionTree_compose.
1036       rewrite <- mapOptionTree_compose.
1037       rewrite <- mapOptionTree_compose.
1038       eapply nd_comp; [ idtac | eapply nd_rule; eapply RCut ].
1039       apply nd_prod.
1040       apply nd_id.
1041       eapply nd_comp.
1042       eapply nd_rule.
1043       eapply RArrange.
1044       eapply ALeft.
1045       eapply ARight.
1046       unfold x1.
1047       rewrite drop_to_nothing.
1048       apply arrangeCancelEmptyTree with (q:=(mapTree (fun _ : ??(HaskType Γ ★) => tt) Σ₁₂)).
1049       admit. (* OK *)
1050       eapply nd_comp; [ eapply nd_rule; eapply RArrange; eapply ALeft; eapply ACanL | idtac ].
1051       set (mapOptionTree flatten_type Σ₁₂) as a.
1052       set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) Σ₁)) as b.
1053       set (mapOptionTree flatten_leveled_type (drop_lev (ec :: lev) Σ₂)) as c.
1054       set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) Σ₂)) as d.
1055       set (mapOptionTree flatten_leveled_type (drop_lev (ec :: lev) Σ)) as e.
1056       set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) Σ)) as f.
1057       eapply nd_comp; [ idtac | eapply nd_rule; eapply RCut ].
1058       eapply nd_comp; [ apply nd_llecnac | idtac ].
1059       apply nd_prod.
1060       simpl.
1061       eapply secondify.
1062       apply ga_first.
1063       eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ALeft; eapply AExch ].
1064       eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AuAssoc ].
1065       simpl.
1066       apply precompose.
1067
1068     destruct case_RLeft.
1069       simpl.
1070       destruct l as [|ec lev].
1071       simpl.
1072         replace (mapOptionTree flatten_leveled_type (Σ @@@ nil)) with (mapOptionTree flatten_type Σ @@@ nil).
1073         apply nd_rule.
1074         apply RLeft.
1075         induction Σ; try destruct a; auto.
1076         simpl.
1077         rewrite <- IHΣ1.
1078         rewrite <- IHΣ2.
1079         reflexivity.
1080       repeat drop_simplify.
1081         rewrite drop_to_nothing.
1082         simpl.
1083         eapply nd_comp.
1084         Focus 2.
1085         eapply nd_rule.
1086         eapply RArrange.
1087         eapply ARight.
1088         apply arrangeUnCancelEmptyTree with (q:=(mapTree (fun _ : ??(HaskType Γ ★) => tt) Σ)).
1089         admit (* FIXME *).
1090         idtac.
1091         eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AuCanL ].
1092         apply boost.
1093         take_simplify.
1094         simpl.
1095         replace (take_lev (ec :: lev) (Σ @@@ (ec :: lev))) with (Σ @@@ (ec::lev)).
1096         rewrite mapOptionTree_compose.
1097         rewrite mapOptionTree_compose.
1098         rewrite unlev_relev.
1099         apply ga_second.
1100       rewrite take_lemma'.
1101       reflexivity.
1102
1103     destruct case_RRight.
1104       simpl.
1105       destruct l as [|ec lev].
1106       simpl.
1107         replace (mapOptionTree flatten_leveled_type (Σ @@@ nil)) with (mapOptionTree flatten_type Σ @@@ nil).
1108         apply nd_rule.
1109         apply RRight.
1110         induction Σ; try destruct a; auto.
1111         simpl.
1112         rewrite <- IHΣ1.
1113         rewrite <- IHΣ2.
1114         reflexivity.
1115       repeat drop_simplify.
1116         rewrite drop_to_nothing.
1117         simpl.
1118         eapply nd_comp.
1119         Focus 2.
1120         eapply nd_rule.
1121         eapply RArrange.
1122         eapply ALeft.
1123         apply arrangeUnCancelEmptyTree with (q:=(mapTree (fun _ : ??(HaskType Γ ★) => tt) Σ)).
1124         admit (* FIXME *).
1125         idtac.
1126         eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AuCanR ].
1127         apply boost.
1128         take_simplify.
1129         simpl.
1130         replace (take_lev (ec :: lev) (Σ @@@ (ec :: lev))) with (Σ @@@ (ec::lev)).
1131         rewrite mapOptionTree_compose.
1132         rewrite mapOptionTree_compose.
1133         rewrite unlev_relev.
1134         apply ga_first.
1135       rewrite take_lemma'.
1136       reflexivity.
1137
1138     destruct case_RVoid.
1139       simpl.
1140       apply nd_rule.
1141       destruct l.
1142       apply RVoid.
1143       apply (Prelude_error "RVoid at level >0").
1144
1145     destruct case_RAppT.
1146       simpl. destruct lev; simpl.
1147       unfold flatten_leveled_type.
1148       simpl.
1149       rewrite flatten_commutes_with_HaskTAll.
1150       rewrite flatten_commutes_with_substT.
1151       apply nd_rule.
1152       apply RAppT.
1153       apply Δ.
1154       apply Δ.
1155       apply (Prelude_error "found type application at level >0; this is not supported").
1156
1157     destruct case_RAbsT.
1158       simpl. destruct lev; simpl.
1159       rewrite flatten_commutes_with_HaskTAll.
1160       rewrite flatten_commutes_with_HaskTApp.
1161       eapply nd_comp; [ idtac | eapply nd_rule; eapply RAbsT ].
1162       simpl.
1163       set (mapOptionTree (flatten_leveled_type ) (mapOptionTree (weakLT(κ:=κ)) Σ)) as a.
1164       set (mapOptionTree (weakLT(κ:=κ)) (mapOptionTree (flatten_leveled_type ) Σ)) as q'.
1165       assert (a=q').
1166         unfold a.
1167         unfold q'.
1168         clear a q'.
1169         induction Σ.
1170           destruct a.
1171           simpl.
1172           rewrite flatten_commutes_with_weakLT.
1173           reflexivity.
1174           reflexivity.
1175           simpl.
1176           rewrite <- IHΣ1.
1177           rewrite <- IHΣ2.
1178           reflexivity.
1179       rewrite H.
1180       apply nd_id.
1181       apply Δ.
1182       apply Δ.
1183       apply (Prelude_error "found type abstraction at level >0; this is not supported").
1184
1185     destruct case_RAppCo.
1186       simpl. destruct lev; simpl.
1187       unfold flatten_type.
1188       simpl.
1189       apply nd_rule.
1190       apply RAppCo.
1191       apply flatten_coercion.
1192       apply γ.
1193       apply (Prelude_error "found coercion application at level >0; this is not supported").
1194
1195     destruct case_RAbsCo.
1196       simpl. destruct lev; simpl.
1197       unfold flatten_type.
1198       simpl.
1199       apply (Prelude_error "AbsCo not supported (FIXME)").
1200       apply (Prelude_error "found coercion abstraction at level >0; this is not supported").
1201
1202     destruct case_RLetRec.
1203       rename t into lev.
1204       simpl. destruct lev; simpl.
1205       apply nd_rule.
1206       set (@RLetRec Γ Δ (mapOptionTree flatten_leveled_type lri) (flatten_type x) (mapOptionTree flatten_type y) nil) as q.
1207       replace (mapOptionTree flatten_leveled_type (y @@@ nil)) with (mapOptionTree flatten_type y @@@ nil).
1208       apply q.
1209         induction y; try destruct a; auto.
1210         simpl.
1211         rewrite IHy1.
1212         rewrite IHy2.
1213         reflexivity.
1214       apply (Prelude_error "LetRec not supported inside brackets yet (FIXME)").
1215
1216     destruct case_RCase.
1217       simpl.
1218       apply (Prelude_error "Case not supported (BIG FIXME)").
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 nd_rule; 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 [ ].