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