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   Definition flatten_proof :
 788     forall  {h}{c},
 789       ND SRule h c ->
 790       ND  Rule (mapOptionTree (flatten_judgment ) h) (mapOptionTree (flatten_judgment ) c).
 791     intros.
 792     eapply nd_map'; [ idtac | apply X ].
 793     clear h c X.
 794     intros.
 795     simpl in *.
 796
 797     refine
 798       (match X as R in SRule H C with
 799       | SBrak    Γ Δ t ec succ lev           => let case_SBrak := tt         in _
 800       | SEsc     Γ Δ t ec succ lev           => let case_SEsc := tt          in _
 801       | SFlat    h c r                       => let case_SFlat := tt         in _
 802       end).
 803
 804     destruct case_SFlat.
 805     refine (match r as R in Rule H C with
 806       | RArrange Γ Δ a b x l d         => let case_RArrange := tt      in _
 807       | RNote    Γ Δ Σ τ l n           => let case_RNote := tt         in _
 808       | RLit     Γ Δ l     _           => let case_RLit := tt          in _
 809       | RVar     Γ Δ σ           lev   => let case_RVar := tt          in _
 810       | RGlobal  Γ Δ σ l wev           => let case_RGlobal := tt       in _
 811       | RLam     Γ Δ Σ tx te     lev   => let case_RLam := tt          in _
 812       | RCast    Γ Δ Σ σ τ lev γ       => let case_RCast := tt         in _
 813       | RAbsT    Γ Δ Σ κ σ lev         => let case_RAbsT := tt         in _
 814       | RAppT    Γ Δ Σ κ σ τ     lev   => let case_RAppT := tt         in _
 815       | RAppCo   Γ Δ Σ κ σ₁ σ₂ γ σ lev => let case_RAppCo := tt        in _
 816       | RAbsCo   Γ Δ Σ κ σ  σ₁ σ₂  lev => let case_RAbsCo := tt        in _
 817       | RApp     Γ Δ Σ₁ Σ₂ tx te lev   => let case_RApp := tt          in _
 818       | RLet     Γ Δ Σ₁ Σ₂ σ₁ σ₂ lev   => let case_RLet := tt          in _
 819       | RWhere   Γ Δ Σ₁ Σ₂ Σ₃ σ₁ σ₂ lev   => let case_RWhere := tt          in _
 820       | RJoin    Γ p lri m x q l       => let case_RJoin := tt in _
 821       | RVoid    _ _       l           => let case_RVoid := tt   in _
 822       | RBrak    Γ Δ t ec succ lev           => let case_RBrak := tt         in _
 823       | REsc     Γ Δ t ec succ lev           => let case_REsc := tt          in _
 824       | RCase    Γ Δ lev tc Σ avars tbranches alts => let case_RCase := tt         in _
 825       | RLetRec  Γ Δ lri x y t         => let case_RLetRec := tt       in _
 826       end); clear X h c.
 827
 828     destruct case_RArrange.
 829       apply (flatten_arrangement''  Γ Δ a b x _ d).
 830
 831     destruct case_RBrak.
 832       apply (Prelude_error "found unskolemized Brak rule; this shouldn't happen").
 833
 834     destruct case_REsc.
 835       apply (Prelude_error "found unskolemized Esc rule; this shouldn't happen").
 836
 837     destruct case_RNote.
 838       simpl.
 839       destruct l; simpl.
 840         apply nd_rule; apply RNote; auto.
 841         apply nd_rule; apply RNote; auto.
 842
 843     destruct case_RLit.
 844       simpl.
 845       destruct l0; simpl.
 846         unfold flatten_leveled_type.
 847         simpl.
 848         rewrite literal_types_unchanged.
 849           apply nd_rule; apply RLit.
 850         unfold take_lev; simpl.
 851         unfold drop_lev; simpl.
 852         simpl.
 853         rewrite literal_types_unchanged.
 854         apply ga_lit.
 855
 856     destruct case_RVar.
 857       Opaque flatten_judgment.
 858       simpl.
 859       Transparent flatten_judgment.
 860       idtac.
 861       unfold flatten_judgment.
 862       destruct lev.
 863       apply nd_rule. apply RVar.
 864       repeat drop_simplify.
 865       repeat take_simplify.
 866       simpl.
 867       apply ga_id.
 868
 869     destruct case_RGlobal.
 870       simpl.
 871       rename l into g.
 872       rename σ into l.
 873       destruct l as [|ec lev]; simpl.
 874         destruct (eqd_dec (g:CoreVar) (hetmet_flatten:CoreVar)).
 875           set (flatten_type (g wev)) as t.
 876           set (RGlobal _ Δ nil (mkGlobal Γ t hetmet_id)) as q.
 877           simpl in q.
 878           apply nd_rule.
 879           apply q.
 880           apply INil.
 881         destruct (eqd_dec (g:CoreVar) (hetmet_unflatten:CoreVar)).
 882           set (flatten_type (g wev)) as t.
 883           set (RGlobal _ Δ nil (mkGlobal Γ t hetmet_id)) as q.
 884           simpl in q.
 885           apply nd_rule.
 886           apply q.
 887           apply INil.
 888         unfold flatten_leveled_type. simpl.
 889           apply nd_rule; rewrite globals_do_not_have_code_types.
 890           apply RGlobal.
 891       apply (Prelude_error "found RGlobal at depth >0; globals should never appear inside code brackets unless escaped").
 892
 893     destruct case_RLam.
 894       Opaque drop_lev.
 895       Opaque take_lev.
 896       simpl.
 897       destruct lev as [|ec lev]; simpl; [ apply nd_rule; apply RLam; auto | idtac ].
 898       repeat drop_simplify.
 899       repeat take_simplify.
 900       eapply nd_comp.
 901         eapply nd_rule.
 902         eapply RArrange.
 903         simpl.
 904         apply ACanR.
 905       apply boost.
 906       simpl.
 907       apply ga_curry.
 908
 909     destruct case_RCast.
 910       simpl.
 911       destruct lev as [|ec lev]; simpl; [ apply nd_rule; apply RCast; auto | idtac ].
 912       simpl.
 913       apply flatten_coercion; auto.
 914       apply (Prelude_error "RCast at level >0; casting inside of code brackets is currently not supported").
 915
 916     destruct case_RJoin.
 917       simpl.
 918       destruct l;
 919         [ apply nd_rule; apply RJoin | idtac ];
 920         apply (Prelude_error "RJoin at depth >0").
 921
 922     destruct case_RApp.
 923       simpl.
 924
 925       destruct lev as [|ec lev].
 926         unfold flatten_type at 1.
 927         simpl.
 928         apply nd_rule.
 929         apply RApp.
 930
 931         repeat drop_simplify.
 932           repeat take_simplify.
 933           rewrite mapOptionTree_distributes.
 934           set (mapOptionTree (flatten_leveled_type ) (drop_lev (ec :: lev) Σ₁)) as Σ₁'.
 935           set (mapOptionTree (flatten_leveled_type ) (drop_lev (ec :: lev) Σ₂)) as Σ₂'.
 936           set (take_lev (ec :: lev) Σ₁) as Σ₁''.
 937           set (take_lev (ec :: lev) Σ₂) as Σ₂''.
 938           replace (flatten_type  (tx ---> te)) with ((flatten_type  tx) ---> (flatten_type  te)).
 939           apply (Prelude_error "FIXME: ga_apply").
 940           reflexivity.
 941
 942 (*
 943   Notation "`  x" := (take_lev _ x).
 944   Notation "`` x" := (mapOptionTree unlev x) (at level 20).
 945   Notation "``` x" := ((drop_lev _ x)) (at level 20).
 946   Notation "!<[]> x" := (flatten_type _ x) (at level 1).
 947   Notation "!<[@]> x" := (mapOptionTree flatten_leveled_type x) (at level 1).
 948 *)
 949
 950     destruct case_RLet.
 951       simpl.
 952       destruct lev as [|ec lev]; simpl; [ apply nd_rule; apply RLet; auto | idtac ].
 953       repeat drop_simplify.
 954       repeat take_simplify.
 955       simpl.
 956
 957       set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) Σ₁)) as Σ₁'.
 958       set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) Σ₂)) as Σ₂'.
 959       set (mapOptionTree flatten_leveled_type (drop_lev (ec :: lev) Σ₁)) as Σ₁''.
 960       set (mapOptionTree flatten_leveled_type (drop_lev (ec :: lev) Σ₂)) as Σ₂''.
 961
 962       eapply nd_comp.
 963       eapply nd_prod; [ idtac | apply nd_id ].
 964       eapply boost.
 965       apply (ga_first _ _ _ _ _ _ Σ₂').
 966
 967       eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
 968       apply nd_prod.
 969       apply nd_id.
 970       eapply nd_comp; [ eapply nd_rule; eapply RArrange; eapply ACanL | idtac ].
 971       eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AExch (* okay *)].
 972       apply precompose.
 973
 974     destruct case_RWhere.
 975       simpl.
 976       destruct lev as [|ec lev]; simpl; [ apply nd_rule; apply RWhere; auto | idtac ].
 977       repeat take_simplify.
 978       repeat drop_simplify.
 979       simpl.
 980
 981       set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) Σ₁)) as Σ₁'.
 982       set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) Σ₂)) as Σ₂'.
 983       set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) Σ₃)) as Σ₃'.
 984       set (mapOptionTree flatten_leveled_type (drop_lev (ec :: lev) Σ₁)) as Σ₁''.
 985       set (mapOptionTree flatten_leveled_type (drop_lev (ec :: lev) Σ₂)) as Σ₂''.
 986       set (mapOptionTree flatten_leveled_type (drop_lev (ec :: lev) Σ₃)) as Σ₃''.
 987
 988       eapply nd_comp.
 989       eapply nd_prod; [ eapply nd_id | idtac ].
 990       eapply (first_nd _ _ _ _ _ _ Σ₃').
 991       eapply nd_comp.
 992       eapply nd_prod; [ eapply nd_id | idtac ].
 993       eapply (second_nd _ _ _ _ _ _ Σ₁').
 994
 995       eapply nd_comp; [ idtac | eapply nd_rule; eapply RWhere ].
 996       apply nd_prod; [ idtac | apply nd_id ].
 997       eapply nd_comp; [ idtac | eapply precompose' ].
 998       apply nd_rule.
 999       apply RArrange.
1000       apply ALeft.
1001       apply ACanL.
1002
1003     destruct case_RVoid.
1004       simpl.
1005       apply nd_rule.
1006       destruct l.
1007       apply RVoid.
1008       apply (Prelude_error "RVoid at level >0").
1009
1010     destruct case_RAppT.
1011       simpl. destruct lev; simpl.
1012       unfold flatten_leveled_type.
1013       simpl.
1014       rewrite flatten_commutes_with_HaskTAll.
1015       rewrite flatten_commutes_with_substT.
1016       apply nd_rule.
1017       apply RAppT.
1018       apply Δ.
1019       apply Δ.
1020       apply (Prelude_error "found type application at level >0; this is not supported").
1021
1022     destruct case_RAbsT.
1023       simpl. destruct lev; simpl.
1024       rewrite flatten_commutes_with_HaskTAll.
1025       rewrite flatten_commutes_with_HaskTApp.
1026       eapply nd_comp; [ idtac | eapply nd_rule; eapply RAbsT ].
1027       simpl.
1028       set (mapOptionTree (flatten_leveled_type ) (mapOptionTree (weakLT(κ:=κ)) Σ)) as a.
1029       set (mapOptionTree (weakLT(κ:=κ)) (mapOptionTree (flatten_leveled_type ) Σ)) as q'.
1030       assert (a=q').
1031         unfold a.
1032         unfold q'.
1033         clear a q'.
1034         induction Σ.
1035           destruct a.
1036           simpl.
1037           rewrite flatten_commutes_with_weakLT.
1038           reflexivity.
1039           reflexivity.
1040           simpl.
1041           rewrite <- IHΣ1.
1042           rewrite <- IHΣ2.
1043           reflexivity.
1044       rewrite H.
1045       apply nd_id.
1046       apply Δ.
1047       apply Δ.
1048       apply (Prelude_error "found type abstraction at level >0; this is not supported").
1049
1050     destruct case_RAppCo.
1051       simpl. destruct lev; simpl.
1052       unfold flatten_type.
1053       simpl.
1054       apply nd_rule.
1055       apply RAppCo.
1056       apply flatten_coercion.
1057       apply γ.
1058       apply (Prelude_error "found coercion application at level >0; this is not supported").
1059
1060     destruct case_RAbsCo.
1061       simpl. destruct lev; simpl.
1062       unfold flatten_type.
1063       simpl.
1064       apply (Prelude_error "AbsCo not supported (FIXME)").
1065       apply (Prelude_error "found coercion abstraction at level >0; this is not supported").
1066
1067     destruct case_RLetRec.
1068       rename t into lev.
1069       simpl. destruct lev; simpl.
1070       apply nd_rule.
1071       set (@RLetRec Γ Δ (mapOptionTree flatten_leveled_type lri) (flatten_type x) (mapOptionTree flatten_type y) nil) as q.
1072       replace (mapOptionTree flatten_leveled_type (y @@@ nil)) with (mapOptionTree flatten_type y @@@ nil).
1073       apply q.
1074         induction y; try destruct a; auto.
1075         simpl.
1076         rewrite IHy1.
1077         rewrite IHy2.
1078         reflexivity.
1079       apply (Prelude_error "LetRec not supported inside brackets yet (FIXME)").
1080
1081     destruct case_RCase.
1082       simpl.
1083       apply (Prelude_error "Case not supported (BIG FIXME)").
1084
1085     destruct case_SBrak.
1086       simpl.
1087       destruct lev.
1088       drop_simplify.
1089       set (drop_lev (ec :: nil) (take_arg_types_as_tree t @@@ (ec :: nil))) as empty_tree.
1090       take_simplify.
1091       rewrite take_lemma'.
1092       simpl.
1093       rewrite mapOptionTree_compose.
1094       rewrite mapOptionTree_compose.
1095       rewrite unlev_relev.
1096       rewrite <- mapOptionTree_compose.
1097       simpl.
1098       rewrite krunk.
1099       set (mapOptionTree flatten_leveled_type (drop_lev (ec :: nil) succ)) as succ_host.
1100       set (mapOptionTree (flatten_type ○ unlev)(take_lev (ec :: nil) succ)) as succ_guest.
1101       set (mapOptionTree flatten_type (take_arg_types_as_tree t)) as succ_args.
1102       unfold empty_tree.
1103       eapply nd_comp; [ eapply nd_rule; eapply RArrange; eapply ALeft; apply tree_of_nothing | idtac ].
1104       eapply nd_comp; [ eapply nd_rule; eapply RArrange; eapply ACanR | idtac ].
1105       refine (ga_unkappa Γ Δ (v2t ec) nil _ _ _ _ ;; _).
1106       eapply nd_comp; [ idtac | eapply arrange_brak ].
1107       unfold succ_host.
1108       unfold succ_guest.
1109       eapply nd_rule.
1110         eapply RArrange.
1111         apply AExch.
1112       apply (Prelude_error "found Brak at depth >0 indicating 3-level code; only two-level code is currently supported").
1113
1114     destruct case_SEsc.
1115       simpl.
1116       destruct lev.
1117       simpl.
1118       unfold flatten_leveled_type at 2.
1119       simpl.
1120       rewrite krunk.
1121       rewrite mapOptionTree_compose.
1122       take_simplify.
1123       drop_simplify.
1124       simpl.
1125       eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ALeft; apply tree_of_nothing' ].
1126       eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ACanR ].
1127       simpl.
1128       rewrite take_lemma'.
1129       rewrite unlev_relev.
1130       rewrite <- mapOptionTree_compose.
1131       eapply nd_comp; [ apply (arrange_esc _ _ ec) | idtac ].
1132
1133       set (decide_tree_empty (take_lev (ec :: nil) succ)) as q'.
1134       destruct q'.
1135       destruct s.
1136       rewrite e.
1137       clear e.
1138
1139       set (mapOptionTree flatten_leveled_type (drop_lev (ec :: nil) succ)) as succ_host.
1140       set (mapOptionTree flatten_type (take_arg_types_as_tree t)) as succ_args.
1141
1142       eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply AuCanR ].
1143       eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply AuCanR ].
1144       eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply ACanL ].
1145       eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
1146       eapply nd_comp; [ apply nd_llecnac | idtac ].
1147       apply nd_prod; [ idtac | eapply boost ].
1148       induction x.
1149         apply ga_id.
1150         eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ACanL ].
1151         simpl.
1152         apply ga_join.
1153           apply IHx1.
1154           apply IHx2.
1155           simpl.
1156           apply postcompose.
1157
1158       refine ( _ ;; (boost _ _ _ _ _ (postcompose _ _ _ _ _ _ _ _))).
1159       apply ga_cancell.
1160       apply firstify.
1161
1162       induction x.
1163         destruct a; simpl.
1164         apply ga_id.
1165         simpl.
1166         refine ( _ ;; (boost _ _ _ _ _ (postcompose _ _ _ _ _ _ _ _))).
1167         apply ga_cancell.
1168         refine ( _ ;; (boost _ _ _ _ _ (postcompose _ _ _ _ _ _ _ _))).
1169         eapply firstify.
1170         apply IHx1.
1171         apply secondify.
1172         apply IHx2.
1173
1174       (* environment has non-empty leaves *)
1175       apply (Prelude_error "ga_kappa not supported yet (BIG FIXME)").
1176
1177       (* nesting too deep *)
1178       apply (Prelude_error "found Esc at depth >0 indicating 3-level code; only two-level code is currently supported").
1179       Defined.
1180
1181   Definition skolemize_and_flatten_proof :
1182     forall  {h}{c},
1183       ND  Rule h c ->
1184       ND  Rule
1185            (mapOptionTree (flatten_judgment ○ skolemize_judgment) h)
1186            (mapOptionTree (flatten_judgment ○ skolemize_judgment) c).
1187     intros.
1188     rewrite mapOptionTree_compose.
1189     rewrite mapOptionTree_compose.
1190     apply flatten_proof.
1191     apply skolemize_proof.
1192     apply X.
1193     Defined.
1194
1195
1196   (* to do: establish some metric on judgments (max length of level of any succedent type, probably), show how to
1197    * calculate it, and show that the flattening procedure above drives it down by one *)
1198
1199   (*
1200   Instance FlatteningFunctor {Γ}{Δ}{ec} : Functor (JudgmentsL (PCF Γ Δ ec)) (TypesL (SystemFCa Γ Δ)) (obact) :=
1201     { fmor := FlatteningFunctor_fmor }.
1202
1203   Definition ReificationFunctor Γ Δ : Functor (JudgmentsL _ _ (PCF n Γ Δ)) SystemFCa' (mapOptionTree brakifyJudg).
1204     refine {| fmor := ReificationFunctor_fmor Γ Δ |}; unfold hom; unfold ob; simpl ; intros.
1205
1206   Definition PCF_SMME (n:nat)(Γ:TypeEnv)(Δ:CoercionEnv Γ) : ProgrammingLanguageSMME.
1207     refine {| plsmme_pl := PCF n Γ Δ |}.
1208     Defined.
1209
1210   Definition SystemFCa_SMME (n:nat)(Γ:TypeEnv)(Δ:CoercionEnv Γ) : ProgrammingLanguageSMME.
1211     refine {| plsmme_pl := SystemFCa n Γ Δ |}.
1212     Defined.
1213
1214   Definition ReificationFunctorMonoidal n : MonoidalFunctor (JudgmentsN n) (JudgmentsN (S n)) (ReificationFunctor n).
1215     Defined.
1216
1217   (* 5.1.4 *)
1218   Definition PCF_SystemFCa_two_level n Γ Δ : TwoLevelLanguage (PCF_SMME n Γ Δ) (SystemFCa_SMME (S n) Γ Δ).
1219     Defined.
1220   *)
1221   (*  ... and the retraction exists *)
1222
1223 End HaskFlattener.
1224
1225 Implicit Arguments garrow [ ].