src/HaskFlattener.v

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