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_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       | RJoin    Γ p lri m x q l       => let case_RJoin := tt in _
 839       | RVoid    _ _       l           => let case_RVoid := tt   in _
 840       | RBrak    Γ Δ t ec succ lev           => let case_RBrak := tt         in _
 841       | REsc     Γ Δ t ec succ lev           => let case_REsc := tt          in _
 842       | RCase    Γ Δ lev tc Σ avars tbranches alts => let case_RCase := tt         in _
 843       | RLetRec  Γ Δ lri x y t         => let case_RLetRec := tt       in _
 844       end); clear X h c.
 845
 846     destruct case_RArrange.
 847       apply (flatten_arrangement''  Γ Δ a b x _ d).
 848
 849     destruct case_RBrak.
 850       apply (Prelude_error "found unskolemized Brak rule; this shouldn't happen").
 851
 852     destruct case_REsc.
 853       apply (Prelude_error "found unskolemized Esc rule; this shouldn't happen").
 854
 855     destruct case_RNote.
 856       simpl.
 857       destruct l; simpl.
 858         apply nd_rule; apply RNote; auto.
 859         apply nd_rule; apply RNote; auto.
 860
 861     destruct case_RLit.
 862       simpl.
 863       destruct l0; simpl.
 864         unfold flatten_leveled_type.
 865         simpl.
 866         rewrite literal_types_unchanged.
 867           apply nd_rule; apply RLit.
 868         unfold take_lev; simpl.
 869         unfold drop_lev; simpl.
 870         simpl.
 871         rewrite literal_types_unchanged.
 872         apply ga_lit.
 873
 874     destruct case_RVar.
 875       Opaque flatten_judgment.
 876       simpl.
 877       Transparent flatten_judgment.
 878       idtac.
 879       unfold flatten_judgment.
 880       destruct lev.
 881       apply nd_rule. apply RVar.
 882       repeat drop_simplify.
 883       repeat take_simplify.
 884       simpl.
 885       apply ga_id.
 886
 887     destruct case_RGlobal.
 888       simpl.
 889       rename l into g.
 890       rename σ into l.
 891       destruct l as [|ec lev]; simpl.
 892         destruct (eqd_dec (g:CoreVar) (hetmet_flatten:CoreVar)).
 893           set (flatten_type (g wev)) as t.
 894           set (RGlobal _ Δ nil (mkGlobal Γ t hetmet_id)) as q.
 895           simpl in q.
 896           apply nd_rule.
 897           apply q.
 898           apply INil.
 899         destruct (eqd_dec (g:CoreVar) (hetmet_unflatten:CoreVar)).
 900           set (flatten_type (g wev)) as t.
 901           set (RGlobal _ Δ nil (mkGlobal Γ t hetmet_id)) as q.
 902           simpl in q.
 903           apply nd_rule.
 904           apply q.
 905           apply INil.
 906         unfold flatten_leveled_type. simpl.
 907           apply nd_rule; rewrite globals_do_not_have_code_types.
 908           apply RGlobal.
 909       apply (Prelude_error "found RGlobal at depth >0; globals should never appear inside code brackets unless escaped").
 910
 911     destruct case_RLam.
 912       Opaque drop_lev.
 913       Opaque take_lev.
 914       simpl.
 915       destruct lev as [|ec lev]; simpl; [ apply nd_rule; apply RLam; auto | idtac ].
 916       repeat drop_simplify.
 917       repeat take_simplify.
 918       eapply nd_comp.
 919         eapply nd_rule.
 920         eapply RArrange.
 921         simpl.
 922         apply ACanR.
 923       apply boost.
 924       simpl.
 925       apply ga_curry.
 926
 927     destruct case_RCast.
 928       simpl.
 929       destruct lev as [|ec lev]; simpl; [ apply nd_rule; apply RCast; auto | idtac ].
 930       simpl.
 931       apply flatten_coercion; auto.
 932       apply (Prelude_error "RCast at level >0; casting inside of code brackets is currently not supported").
 933
 934     destruct case_RJoin.
 935       simpl.
 936       destruct l;
 937         [ apply nd_rule; apply RJoin | idtac ];
 938         apply (Prelude_error "RJoin at depth >0").
 939
 940     destruct case_RApp.
 941       simpl.
 942
 943       destruct lev as [|ec lev].
 944         unfold flatten_type at 1.
 945         simpl.
 946         apply nd_rule.
 947         apply RApp.
 948
 949         repeat drop_simplify.
 950           repeat take_simplify.
 951           rewrite mapOptionTree_distributes.
 952           set (mapOptionTree (flatten_leveled_type ) (drop_lev (ec :: lev) Σ₁)) as Σ₁'.
 953           set (mapOptionTree (flatten_leveled_type ) (drop_lev (ec :: lev) Σ₂)) as Σ₂'.
 954           set (take_lev (ec :: lev) Σ₁) as Σ₁''.
 955           set (take_lev (ec :: lev) Σ₂) as Σ₂''.
 956           replace (flatten_type  (tx ---> te)) with ((flatten_type  tx) ---> (flatten_type  te)).
 957           apply (Prelude_error "FIXME: ga_apply").
 958           reflexivity.
 959
 960 (*
 961   Notation "`  x" := (take_lev _ x).
 962   Notation "`` x" := (mapOptionTree unlev x) (at level 20).
 963   Notation "``` x" := ((drop_lev _ x)) (at level 20).
 964   Notation "!<[]> x" := (flatten_type _ x) (at level 1).
 965   Notation "!<[@]> x" := (mapOptionTree flatten_leveled_type x) (at level 1).
 966 *)
 967
 968     destruct case_RLet.
 969       simpl.
 970       destruct lev as [|ec lev]; simpl; [ apply nd_rule; apply RLet; auto | idtac ].
 971       repeat drop_simplify.
 972       repeat take_simplify.
 973       simpl.
 974
 975       set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) Σ₁)) as Σ₁'.
 976       set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) Σ₂)) as Σ₂'.
 977       set (mapOptionTree flatten_leveled_type (drop_lev (ec :: lev) Σ₁)) as Σ₁''.
 978       set (mapOptionTree flatten_leveled_type (drop_lev (ec :: lev) Σ₂)) as Σ₂''.
 979
 980       eapply nd_comp.
 981       eapply nd_prod; [ idtac | apply nd_id ].
 982       eapply boost.
 983       apply (ga_first _ _ _ _ _ _ Σ₂').
 984
 985       eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
 986       apply nd_prod.
 987       apply nd_id.
 988       eapply nd_comp; [ eapply nd_rule; eapply RArrange; eapply ACanL | idtac ].
 989       eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AExch (* okay *)].
 990       apply precompose.
 991
 992     destruct case_RWhere.
 993       simpl.
 994       destruct lev as [|ec lev]; simpl; [ apply nd_rule; apply RWhere; auto | idtac ].
 995       repeat take_simplify.
 996       repeat drop_simplify.
 997       simpl.
 998
 999       set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) Σ₁)) as Σ₁'.
1000       set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) Σ₂)) as Σ₂'.
1001       set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) Σ₃)) as Σ₃'.
1002       set (mapOptionTree flatten_leveled_type (drop_lev (ec :: lev) Σ₁)) as Σ₁''.
1003       set (mapOptionTree flatten_leveled_type (drop_lev (ec :: lev) Σ₂)) as Σ₂''.
1004       set (mapOptionTree flatten_leveled_type (drop_lev (ec :: lev) Σ₃)) as Σ₃''.
1005
1006       eapply nd_comp.
1007       eapply nd_prod; [ eapply nd_id | idtac ].
1008       eapply (first_nd _ _ _ _ _ _ Σ₃').
1009       eapply nd_comp.
1010       eapply nd_prod; [ eapply nd_id | idtac ].
1011       eapply (second_nd _ _ _ _ _ _ Σ₁').
1012
1013       eapply nd_comp; [ idtac | eapply nd_rule; eapply RWhere ].
1014       apply nd_prod; [ idtac | apply nd_id ].
1015       eapply nd_comp; [ idtac | eapply precompose' ].
1016       apply nd_rule.
1017       apply RArrange.
1018       apply ALeft.
1019       apply ACanL.
1020
1021     destruct case_RCut.
1022       simpl.
1023       destruct l as [|ec lev]; simpl.
1024         apply nd_rule.
1025         replace (mapOptionTree flatten_leveled_type (Σ₁₂ @@@ nil)) with (mapOptionTree flatten_type Σ₁₂ @@@ nil).
1026         apply RCut.
1027         induction Σ₁₂; try destruct a; auto.
1028         simpl.
1029         rewrite <- IHΣ₁₂1.
1030         rewrite <- IHΣ₁₂2.
1031         reflexivity.
1032       simpl.
1033       repeat drop_simplify.
1034       simpl.
1035       repeat take_simplify.
1036       simpl.
1037       set (drop_lev (ec :: lev) (Σ₁₂ @@@ (ec :: lev))) as x1.
1038       rewrite take_lemma'.
1039       rewrite mapOptionTree_compose.
1040       rewrite mapOptionTree_compose.
1041       rewrite mapOptionTree_compose.
1042       rewrite unlev_relev.
1043       rewrite <- mapOptionTree_compose.
1044       rewrite <- mapOptionTree_compose.
1045       eapply nd_comp; [ idtac | eapply nd_rule; eapply RCut ].
1046       apply nd_prod.
1047       apply nd_id.
1048       eapply nd_comp.
1049       eapply nd_rule.
1050       eapply RArrange.
1051       eapply ARight.
1052       unfold x1.
1053       rewrite drop_to_nothing.
1054       apply arrangeCancelEmptyTree with (q:=(mapTree (fun _ : ??(HaskType Γ ★) => tt) Σ₁₂)).
1055       admit. (* OK *)
1056       eapply nd_comp; [ eapply nd_rule; eapply RArrange; eapply ACanL | idtac ].
1057       set (mapOptionTree flatten_type Σ₁₂) as a.
1058       set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) Σ₁)) as b.
1059       set (mapOptionTree flatten_leveled_type (drop_lev (ec :: lev) Σ₂)) as c.
1060       set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) Σ₂)) as d.
1061       eapply nd_comp; [ idtac | eapply nd_rule; eapply RCut ].
1062       eapply nd_comp; [ apply nd_llecnac | idtac ].
1063       apply nd_prod.
1064       simpl.
1065       eapply ga_first.
1066       eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AExch ].
1067       simpl.
1068       apply precompose.
1069
1070     destruct case_RLeft.
1071       simpl.
1072       destruct l as [|ec lev].
1073       simpl.
1074         replace (mapOptionTree flatten_leveled_type (Σ @@@ nil)) with (mapOptionTree flatten_type Σ @@@ nil).
1075         apply nd_rule.
1076         apply RLeft.
1077         induction Σ; try destruct a; auto.
1078         simpl.
1079         rewrite <- IHΣ1.
1080         rewrite <- IHΣ2.
1081         reflexivity.
1082       repeat drop_simplify.
1083         rewrite drop_to_nothing.
1084         simpl.
1085         eapply nd_comp.
1086         Focus 2.
1087         eapply nd_rule.
1088         eapply RArrange.
1089         eapply ARight.
1090         apply arrangeUnCancelEmptyTree with (q:=(mapTree (fun _ : ??(HaskType Γ ★) => tt) Σ)).
1091         admit (* FIXME *).
1092         idtac.
1093         eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AuCanL ].
1094         apply boost.
1095         take_simplify.
1096         simpl.
1097         replace (take_lev (ec :: lev) (Σ @@@ (ec :: lev))) with (Σ @@@ (ec::lev)).
1098         rewrite mapOptionTree_compose.
1099         rewrite mapOptionTree_compose.
1100         rewrite unlev_relev.
1101         apply ga_second.
1102       rewrite take_lemma'.
1103       reflexivity.
1104
1105     destruct case_RRight.
1106       simpl.
1107       destruct l as [|ec lev].
1108       simpl.
1109         replace (mapOptionTree flatten_leveled_type (Σ @@@ nil)) with (mapOptionTree flatten_type Σ @@@ nil).
1110         apply nd_rule.
1111         apply RRight.
1112         induction Σ; try destruct a; auto.
1113         simpl.
1114         rewrite <- IHΣ1.
1115         rewrite <- IHΣ2.
1116         reflexivity.
1117       repeat drop_simplify.
1118         rewrite drop_to_nothing.
1119         simpl.
1120         eapply nd_comp.
1121         Focus 2.
1122         eapply nd_rule.
1123         eapply RArrange.
1124         eapply ALeft.
1125         apply arrangeUnCancelEmptyTree with (q:=(mapTree (fun _ : ??(HaskType Γ ★) => tt) Σ)).
1126         admit (* FIXME *).
1127         idtac.
1128         eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AuCanR ].
1129         apply boost.
1130         take_simplify.
1131         simpl.
1132         replace (take_lev (ec :: lev) (Σ @@@ (ec :: lev))) with (Σ @@@ (ec::lev)).
1133         rewrite mapOptionTree_compose.
1134         rewrite mapOptionTree_compose.
1135         rewrite unlev_relev.
1136         apply ga_first.
1137       rewrite take_lemma'.
1138       reflexivity.
1139
1140     destruct case_RVoid.
1141       simpl.
1142       apply nd_rule.
1143       destruct l.
1144       apply RVoid.
1145       apply (Prelude_error "RVoid at level >0").
1146
1147     destruct case_RAppT.
1148       simpl. destruct lev; simpl.
1149       unfold flatten_leveled_type.
1150       simpl.
1151       rewrite flatten_commutes_with_HaskTAll.
1152       rewrite flatten_commutes_with_substT.
1153       apply nd_rule.
1154       apply RAppT.
1155       apply Δ.
1156       apply Δ.
1157       apply (Prelude_error "found type application at level >0; this is not supported").
1158
1159     destruct case_RAbsT.
1160       simpl. destruct lev; simpl.
1161       rewrite flatten_commutes_with_HaskTAll.
1162       rewrite flatten_commutes_with_HaskTApp.
1163       eapply nd_comp; [ idtac | eapply nd_rule; eapply RAbsT ].
1164       simpl.
1165       set (mapOptionTree (flatten_leveled_type ) (mapOptionTree (weakLT(κ:=κ)) Σ)) as a.
1166       set (mapOptionTree (weakLT(κ:=κ)) (mapOptionTree (flatten_leveled_type ) Σ)) as q'.
1167       assert (a=q').
1168         unfold a.
1169         unfold q'.
1170         clear a q'.
1171         induction Σ.
1172           destruct a.
1173           simpl.
1174           rewrite flatten_commutes_with_weakLT.
1175           reflexivity.
1176           reflexivity.
1177           simpl.
1178           rewrite <- IHΣ1.
1179           rewrite <- IHΣ2.
1180           reflexivity.
1181       rewrite H.
1182       apply nd_id.
1183       apply Δ.
1184       apply Δ.
1185       apply (Prelude_error "found type abstraction at level >0; this is not supported").
1186
1187     destruct case_RAppCo.
1188       simpl. destruct lev; simpl.
1189       unfold flatten_type.
1190       simpl.
1191       apply nd_rule.
1192       apply RAppCo.
1193       apply flatten_coercion.
1194       apply γ.
1195       apply (Prelude_error "found coercion application at level >0; this is not supported").
1196
1197     destruct case_RAbsCo.
1198       simpl. destruct lev; simpl.
1199       unfold flatten_type.
1200       simpl.
1201       apply (Prelude_error "AbsCo not supported (FIXME)").
1202       apply (Prelude_error "found coercion abstraction at level >0; this is not supported").
1203
1204     destruct case_RLetRec.
1205       rename t into lev.
1206       simpl. destruct lev; simpl.
1207       apply nd_rule.
1208       set (@RLetRec Γ Δ (mapOptionTree flatten_leveled_type lri) (flatten_type x) (mapOptionTree flatten_type y) nil) as q.
1209       replace (mapOptionTree flatten_leveled_type (y @@@ nil)) with (mapOptionTree flatten_type y @@@ nil).
1210       apply q.
1211         induction y; try destruct a; auto.
1212         simpl.
1213         rewrite IHy1.
1214         rewrite IHy2.
1215         reflexivity.
1216       apply (Prelude_error "LetRec not supported inside brackets yet (FIXME)").
1217
1218     destruct case_RCase.
1219       simpl.
1220       apply (Prelude_error "Case not supported (BIG FIXME)").
1221
1222     destruct case_SBrak.
1223       simpl.
1224       destruct lev.
1225       drop_simplify.
1226       set (drop_lev (ec :: nil) (take_arg_types_as_tree t @@@ (ec :: nil))) as empty_tree.
1227       take_simplify.
1228       rewrite take_lemma'.
1229       simpl.
1230       rewrite mapOptionTree_compose.
1231       rewrite mapOptionTree_compose.
1232       rewrite unlev_relev.
1233       rewrite <- mapOptionTree_compose.
1234       simpl.
1235       rewrite krunk.
1236       set (mapOptionTree flatten_leveled_type (drop_lev (ec :: nil) succ)) as succ_host.
1237       set (mapOptionTree (flatten_type ○ unlev)(take_lev (ec :: nil) succ)) as succ_guest.
1238       set (mapOptionTree flatten_type (take_arg_types_as_tree t)) as succ_args.
1239       unfold empty_tree.
1240       eapply nd_comp; [ eapply nd_rule; eapply RArrange; eapply ALeft; apply tree_of_nothing | idtac ].
1241       eapply nd_comp; [ eapply nd_rule; eapply RArrange; eapply ACanR | idtac ].
1242       refine (ga_unkappa Γ Δ (v2t ec) nil _ _ _ _ ;; _).
1243       eapply nd_comp; [ idtac | eapply arrange_brak ].
1244       unfold succ_host.
1245       unfold succ_guest.
1246       eapply nd_rule.
1247         eapply RArrange.
1248         apply AExch.
1249       apply (Prelude_error "found Brak at depth >0 indicating 3-level code; only two-level code is currently supported").
1250
1251     destruct case_SEsc.
1252       simpl.
1253       destruct lev.
1254       simpl.
1255       unfold flatten_leveled_type at 2.
1256       simpl.
1257       rewrite krunk.
1258       rewrite mapOptionTree_compose.
1259       take_simplify.
1260       drop_simplify.
1261       simpl.
1262       eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ALeft; apply tree_of_nothing' ].
1263       eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ACanR ].
1264       simpl.
1265       rewrite take_lemma'.
1266       rewrite unlev_relev.
1267       rewrite <- mapOptionTree_compose.
1268       eapply nd_comp; [ apply (arrange_esc _ _ ec) | idtac ].
1269
1270       set (decide_tree_empty (take_lev (ec :: nil) succ)) as q'.
1271       destruct q'.
1272       destruct s.
1273       rewrite e.
1274       clear e.
1275
1276       set (mapOptionTree flatten_leveled_type (drop_lev (ec :: nil) succ)) as succ_host.
1277       set (mapOptionTree flatten_type (take_arg_types_as_tree t)) as succ_args.
1278
1279       eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply AuCanR ].
1280       eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply AuCanR ].
1281       eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply ACanL ].
1282       eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
1283       eapply nd_comp; [ apply nd_llecnac | idtac ].
1284       apply nd_prod; [ idtac | eapply boost ].
1285       induction x.
1286         apply ga_id.
1287         eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ACanL ].
1288         simpl.
1289         apply ga_join.
1290           apply IHx1.
1291           apply IHx2.
1292           simpl.
1293           apply postcompose.
1294
1295       refine ( _ ;; (boost _ _ _ _ _ (postcompose _ _ _ _ _ _ _ _))).
1296       apply ga_cancell.
1297       apply firstify.
1298
1299       induction x.
1300         destruct a; simpl.
1301         apply ga_id.
1302         simpl.
1303         refine ( _ ;; (boost _ _ _ _ _ (postcompose _ _ _ _ _ _ _ _))).
1304         apply ga_cancell.
1305         refine ( _ ;; (boost _ _ _ _ _ (postcompose _ _ _ _ _ _ _ _))).
1306         eapply firstify.
1307         apply IHx1.
1308         apply secondify.
1309         apply IHx2.
1310
1311       (* environment has non-empty leaves *)
1312       apply (Prelude_error "ga_kappa not supported yet (BIG FIXME)").
1313
1314       (* nesting too deep *)
1315       apply (Prelude_error "found Esc at depth >0 indicating 3-level code; only two-level code is currently supported").
1316       Defined.
1317
1318   Definition skolemize_and_flatten_proof :
1319     forall  {h}{c},
1320       ND  Rule h c ->
1321       ND  Rule
1322            (mapOptionTree (flatten_judgment ○ skolemize_judgment) h)
1323            (mapOptionTree (flatten_judgment ○ skolemize_judgment) c).
1324     intros.
1325     rewrite mapOptionTree_compose.
1326     rewrite mapOptionTree_compose.
1327     apply flatten_proof.
1328     apply skolemize_proof.
1329     apply X.
1330     Defined.
1331
1332
1333   (* to do: establish some metric on judgments (max length of level of any succedent type, probably), show how to
1334    * calculate it, and show that the flattening procedure above drives it down by one *)
1335
1336   (*
1337   Instance FlatteningFunctor {Γ}{Δ}{ec} : Functor (JudgmentsL (PCF Γ Δ ec)) (TypesL (SystemFCa Γ Δ)) (obact) :=
1338     { fmor := FlatteningFunctor_fmor }.
1339
1340   Definition ReificationFunctor Γ Δ : Functor (JudgmentsL _ _ (PCF n Γ Δ)) SystemFCa' (mapOptionTree brakifyJudg).
1341     refine {| fmor := ReificationFunctor_fmor Γ Δ |}; unfold hom; unfold ob; simpl ; intros.
1342
1343   Definition PCF_SMME (n:nat)(Γ:TypeEnv)(Δ:CoercionEnv Γ) : ProgrammingLanguageSMME.
1344     refine {| plsmme_pl := PCF n Γ Δ |}.
1345     Defined.
1346
1347   Definition SystemFCa_SMME (n:nat)(Γ:TypeEnv)(Δ:CoercionEnv Γ) : ProgrammingLanguageSMME.
1348     refine {| plsmme_pl := SystemFCa n Γ Δ |}.
1349     Defined.
1350
1351   Definition ReificationFunctorMonoidal n : MonoidalFunctor (JudgmentsN n) (JudgmentsN (S n)) (ReificationFunctor n).
1352     Defined.
1353
1354   (* 5.1.4 *)
1355   Definition PCF_SystemFCa_two_level n Γ Δ : TwoLevelLanguage (PCF_SMME n Γ Δ) (SystemFCa_SMME (S n) Γ Δ).
1356     Defined.
1357   *)
1358   (*  ... and the retraction exists *)
1359
1360 End HaskFlattener.
1361
1362 Implicit Arguments garrow [ ].