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_loopl     : ∀ Γ Δ ec l x y z, ND Rule [] [Γ > Δ > [@ga_mk Γ ec (z,,x) (z,,y) @@ l] |- [@ga_mk Γ ec x y ]@ l ]
 276   ; ga_loopr     : ∀ Γ Δ ec l x y z, ND Rule [] [Γ > Δ > [@ga_mk Γ ec (x,,z) (y,,z) @@ l] |- [@ga_mk Γ ec x y ]@ l ]
 277   ; 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 ]
 278   ; ga_apply     : ∀ Γ Δ ec l a a' b c,
 279                  ND Rule [] [Γ > Δ > [@ga_mk Γ ec a [b ---> c] @@ l],,[@ga_mk Γ ec a' [b] @@ l] |- [@ga_mk Γ ec (a,,a') [c] ]@l ]
 280   ; ga_kappa     : ∀ Γ Δ ec l a b Σ, ND Rule
 281   [Γ > Δ > Σ,,[@ga_mk Γ ec [] a @@ l] |- [@ga_mk Γ ec [] b ]@l ]
 282   [Γ > Δ > Σ          |- [@ga_mk Γ ec a  b ]@l ]
 283   }.
 284   Context `(gar:garrow).
 285
 286   Notation "a ~~~~> b" := (@ga_mk _ _ a b) (at level 20).
 287
 288   Definition boost : forall Γ Δ ant x y {lev},
 289     ND Rule []                         [ Γ > Δ > [x@@lev] |- [y]@lev ] ->
 290     ND Rule [ Γ > Δ > ant |- [x]@lev ] [ Γ > Δ > ant      |- [y]@lev ].
 291     intros.
 292     eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ACanR ].
 293     eapply nd_comp; [ idtac | apply RLet ].
 294     eapply nd_comp; [ apply nd_rlecnac | idtac ].
 295     apply nd_prod.
 296     apply nd_id.
 297     eapply nd_comp.
 298       apply X.
 299       eapply nd_rule.
 300       eapply RArrange.
 301       apply AuCanR.
 302     Defined.
 303
 304   Definition precompose Γ Δ ec : forall a x y z lev,
 305     ND Rule
 306       [ Γ > Δ > a                           |- [@ga_mk _ ec y z ]@lev ]
 307       [ Γ > Δ > a,,[@ga_mk _ ec x y @@ lev] |- [@ga_mk _ ec x z ]@lev ].
 308     intros.
 309     eapply nd_comp; [ idtac | eapply RLet ].
 310     eapply nd_comp; [ apply nd_rlecnac | idtac ].
 311     apply nd_prod.
 312     apply nd_id.
 313     eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AExch ].
 314     apply ga_comp.
 315     Defined.
 316
 317   Definition precompose' Γ Δ ec : forall a b x y z lev,
 318     ND Rule
 319       [ Γ > Δ > a,,b                             |- [@ga_mk _ ec y z ]@lev ]
 320       [ Γ > Δ > a,,([@ga_mk _ ec x y @@ lev],,b) |- [@ga_mk _ ec x z ]@lev ].
 321     intros.
 322     eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ALeft; eapply AExch ].
 323     eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AuAssoc ].
 324     apply precompose.
 325     Defined.
 326
 327   Definition postcompose_ Γ Δ ec : forall a x y z lev,
 328     ND Rule
 329       [ Γ > Δ > a                           |- [@ga_mk _ ec x y ]@lev ]
 330       [ Γ > Δ > a,,[@ga_mk _ ec y z @@ lev] |- [@ga_mk _ ec x z ]@lev ].
 331     intros.
 332     eapply nd_comp; [ idtac | eapply RLet ].
 333     eapply nd_comp; [ apply nd_rlecnac | idtac ].
 334     apply nd_prod.
 335     apply nd_id.
 336     apply ga_comp.
 337     Defined.
 338
 339   Definition postcompose  Γ Δ ec : forall x y z lev,
 340     ND Rule [] [ Γ > Δ > []                       |- [@ga_mk _ ec x y ]@lev ] ->
 341     ND Rule [] [ Γ > Δ > [@ga_mk _ ec y z @@ lev] |- [@ga_mk _ ec x z ]@lev ].
 342     intros.
 343     eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ACanL ].
 344     eapply nd_comp; [ idtac | eapply postcompose_ ].
 345     apply X.
 346     Defined.
 347
 348   Definition first_nd : ∀ Γ Δ ec lev a b c Σ,
 349     ND Rule [ Γ > Δ > Σ                    |- [@ga_mk Γ ec a b ]@lev ]
 350             [ Γ > Δ > Σ                    |- [@ga_mk Γ ec (a,,c) (b,,c) ]@lev ].
 351     intros.
 352     eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ACanR ].
 353     eapply nd_comp; [ idtac | apply RLet ].
 354     eapply nd_comp; [ apply nd_rlecnac | idtac ].
 355     apply nd_prod.
 356     apply nd_id.
 357     eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AuCanR ].
 358     apply ga_first.
 359     Defined.
 360
 361   Definition firstify : ∀ Γ Δ ec lev a b c Σ,
 362     ND Rule [] [ Γ > Δ > Σ                    |- [@ga_mk Γ ec a b ]@lev ] ->
 363     ND Rule [] [ Γ > Δ > Σ                    |- [@ga_mk Γ ec (a,,c) (b,,c) ]@lev ].
 364     intros.
 365     eapply nd_comp.
 366     apply X.
 367     apply first_nd.
 368     Defined.
 369
 370   Definition second_nd : ∀ Γ Δ ec lev a b c Σ,
 371      ND Rule
 372      [ Γ > Δ > Σ                    |- [@ga_mk Γ ec a b ]@lev ]
 373      [ Γ > Δ > Σ                    |- [@ga_mk Γ ec (c,,a) (c,,b) ]@lev ].
 374     intros.
 375     eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ACanR ].
 376     eapply nd_comp; [ idtac | apply RLet ].
 377     eapply nd_comp; [ apply nd_rlecnac | idtac ].
 378     apply nd_prod.
 379     apply nd_id.
 380     eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AuCanR ].
 381     apply ga_second.
 382     Defined.
 383
 384   Definition secondify : ∀ Γ Δ ec lev a b c Σ,
 385      ND Rule [] [ Γ > Δ > Σ                    |- [@ga_mk Γ ec a b ]@lev ] ->
 386      ND Rule [] [ Γ > Δ > Σ                    |- [@ga_mk Γ ec (c,,a) (c,,b) ]@lev ].
 387     intros.
 388     eapply nd_comp.
 389     apply X.
 390     apply second_nd.
 391     Defined.
 392
 393    Lemma ga_unkappa     : ∀ Γ Δ ec l a b Σ x,
 394      ND Rule
 395      [Γ > Δ > Σ                          |- [@ga_mk Γ ec (a,,x)  b ]@l ]
 396      [Γ > Δ > Σ,,[@ga_mk Γ ec [] a @@ l] |- [@ga_mk Γ ec x       b ]@l ].
 397      intros.
 398      eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AExch ].
 399      eapply nd_comp; [ idtac | eapply RLet ].
 400      eapply nd_comp; [ apply nd_llecnac | idtac ].
 401      apply nd_prod.
 402      apply ga_first.
 403
 404      eapply nd_comp; [ idtac | eapply RLet ].
 405      eapply nd_comp; [ apply nd_llecnac | idtac ].
 406      apply nd_prod.
 407      apply postcompose.
 408      apply ga_uncancell.
 409      eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AExch ].
 410      apply precompose.
 411      Defined.
 412
 413   (* useful for cutting down on the pretty-printed noise
 414
 415   Notation "`  x" := (take_lev _ x) (at level 20).
 416   Notation "`` x" := (mapOptionTree unlev x) (at level 20).
 417   Notation "``` x" := (drop_lev _ x) (at level 20).
 418   *)
 419   Definition flatten_arrangement' :
 420     forall Γ (Δ:CoercionEnv Γ)
 421       (ec:HaskTyVar Γ ECKind) (lev:HaskLevel Γ) (ant1 ant2:Tree ??(LeveledHaskType Γ ★)) (r:Arrange ant1 ant2),
 422       ND Rule [] [Γ > Δ > [] |- [@ga_mk _ (v2t ec) (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) ant2))
 423         (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) ant1)) ]@nil ].
 424
 425       intros Γ Δ ec lev.
 426       refine (fix flatten ant1 ant2 (r:Arrange ant1 ant2):
 427            ND Rule [] [Γ > Δ > [] |- [@ga_mk _ (v2t ec)
 428              (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) ant2))
 429              (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) ant1)) ]@nil] :=
 430         match r as R in Arrange A B return
 431           ND Rule [] [Γ > Δ > [] |- [@ga_mk _ (v2t ec)
 432             (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) B))
 433             (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) A)) ]@nil]
 434           with
 435           | AId  a               => let case_AId := tt    in ga_id _ _ _ _ _
 436           | ACanL  a             => let case_ACanL := tt  in ga_uncancell _ _ _ _ _
 437           | ACanR  a             => let case_ACanR := tt  in ga_uncancelr _ _ _ _ _
 438           | AuCanL a             => let case_AuCanL := tt in ga_cancell _ _ _ _ _
 439           | AuCanR a             => let case_AuCanR := tt in ga_cancelr _ _ _ _ _
 440           | AAssoc a b c         => let case_AAssoc := tt in ga_assoc _ _ _ _ _ _ _
 441           | AuAssoc a b c         => let case_AuAssoc := tt in ga_unassoc _ _ _ _ _ _ _
 442           | AExch  a b           => let case_AExch := tt  in ga_swap  _ _ _ _ _ _
 443           | AWeak  a             => let case_AWeak := tt  in ga_drop _ _ _ _ _
 444           | ACont  a             => let case_ACont := tt  in ga_copy  _ _ _ _ _
 445           | ALeft  a b c r'      => let case_ALeft := tt  in flatten _ _ r' ;; boost _ _ _ _ _ (ga_second _ _ _ _ _ _ _)
 446           | ARight a b c r'      => let case_ARight := tt in flatten _ _ r' ;; boost _ _ _ _ _ (ga_first  _ _ _ _ _ _ _)
 447           | AComp  c b a r1 r2   => let case_AComp := tt  in (fun r1' r2' => _) (flatten _ _ r1) (flatten _ _ r2)
 448         end); clear flatten; repeat take_simplify; repeat drop_simplify; intros.
 449
 450         destruct case_AComp.
 451           set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) a)) as a' in *.
 452           set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) b)) as b' in *.
 453           set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) c)) as c' in *.
 454           eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply ACanL ].
 455           eapply nd_comp; [ idtac | apply
 456              (@RLet Γ Δ [] [] (@ga_mk _ (v2t ec) a' b') (@ga_mk _ (v2t ec) a' c')) ].
 457           eapply nd_comp; [ apply nd_llecnac | idtac ].
 458           apply nd_prod.
 459           apply r2'.
 460           eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply AuCanR ].
 461           eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply ACanL ].
 462           eapply nd_comp; [ idtac | apply RLet ].
 463           eapply nd_comp; [ apply nd_llecnac | idtac ].
 464           eapply nd_prod.
 465           apply r1'.
 466           eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AExch ].
 467           apply ga_comp.
 468           Defined.
 469
 470   Definition flatten_arrangement :
 471     forall Γ (Δ:CoercionEnv Γ) n
 472       (ec:HaskTyVar Γ ECKind) (lev:HaskLevel Γ) (ant1 ant2:Tree ??(LeveledHaskType Γ ★)) (r:Arrange ant1 ant2) succ,
 473       ND Rule
 474       [Γ > Δ > mapOptionTree (flatten_leveled_type ) (drop_lev n ant1)
 475         |- [@ga_mk _ (v2t ec)
 476           (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) ant1))
 477           (mapOptionTree (flatten_type ) succ) ]@nil]
 478       [Γ > Δ > mapOptionTree (flatten_leveled_type ) (drop_lev n ant2)
 479         |- [@ga_mk _ (v2t ec)
 480           (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) ant2))
 481           (mapOptionTree (flatten_type ) succ) ]@nil].
 482       intros.
 483       refine ( _ ;; (boost _ _ _ _ _ (postcompose _ _ _ _ _ _ _ (flatten_arrangement' Γ Δ ec lev ant1 ant2 r)))).
 484       apply nd_rule.
 485       apply RArrange.
 486       refine ((fix flatten ant1 ant2 (r:Arrange ant1 ant2) :=
 487         match r as R in Arrange A B return
 488           Arrange (mapOptionTree (flatten_leveled_type ) (drop_lev _ A))
 489           (mapOptionTree (flatten_leveled_type ) (drop_lev _ B)) with
 490           | AId  a               => let case_AId := tt  in AId _
 491           | ACanL  a             => let case_ACanL := tt  in ACanL _
 492           | ACanR  a             => let case_ACanR := tt  in ACanR _
 493           | AuCanL a             => let case_AuCanL := tt in AuCanL _
 494           | AuCanR a             => let case_AuCanR := tt in AuCanR _
 495           | AAssoc a b c         => let case_AAssoc := tt in AAssoc _ _ _
 496           | AuAssoc a b c         => let case_AuAssoc := tt in AuAssoc _ _ _
 497           | AExch  a b           => let case_AExch := tt  in AExch _ _
 498           | AWeak  a             => let case_AWeak := tt  in AWeak _
 499           | ACont  a             => let case_ACont := tt  in ACont _
 500           | ALeft  a b c r'      => let case_ALeft := tt  in ALeft  _ (flatten _ _ r')
 501           | ARight a b c r'      => let case_ARight := tt in ARight _ (flatten _ _ r')
 502           | AComp  a b c r1 r2   => let case_AComp := tt  in AComp    (flatten _ _ r1) (flatten _ _ r2)
 503         end) ant1 ant2 r); clear flatten; repeat take_simplify; repeat drop_simplify; intros.
 504         Defined.
 505
 506   Definition flatten_arrangement'' :
 507     forall  Γ Δ ant1 ant2 succ l (r:Arrange ant1 ant2),
 508       ND Rule (mapOptionTree (flatten_judgment ) [Γ > Δ > ant1 |- succ @ l])
 509       (mapOptionTree (flatten_judgment ) [Γ > Δ > ant2 |- succ @ l]).
 510     intros.
 511     simpl.
 512     destruct l.
 513       apply nd_rule.
 514       apply RArrange.
 515       induction r; simpl.
 516         apply AId.
 517         apply ACanL.
 518         apply ACanR.
 519         apply AuCanL.
 520         apply AuCanR.
 521         apply AAssoc.
 522         apply AuAssoc.
 523         apply AExch.    (* TO DO: check for all-leaf trees here *)
 524         apply AWeak.
 525         apply ACont.
 526         apply ALeft; auto.
 527         apply ARight; auto.
 528         eapply AComp; [ apply IHr1 | apply IHr2 ].
 529
 530       apply flatten_arrangement.
 531         apply r.
 532         Defined.
 533
 534   Definition ga_join Γ Δ Σ₁ Σ₂ a b ec :
 535     ND Rule [] [Γ > Δ > Σ₁     |- [@ga_mk _ ec [] a      ]@nil] ->
 536     ND Rule [] [Γ > Δ > Σ₂     |- [@ga_mk _ ec [] b      ]@nil] ->
 537     ND Rule [] [Γ > Δ > Σ₁,,Σ₂ |- [@ga_mk _ ec [] (a,,b) ]@nil].
 538     intro pfa.
 539     intro pfb.
 540     apply secondify with (c:=a)  in pfb.
 541     apply firstify  with (c:=[])  in pfa.
 542     eapply nd_comp; [ idtac | eapply RLet ].
 543     eapply nd_comp; [ eapply nd_llecnac | idtac ].
 544     apply nd_prod.
 545     apply pfa.
 546     clear pfa.
 547
 548     eapply nd_comp; [ idtac | eapply RLet ].
 549     eapply nd_comp; [ apply nd_llecnac | idtac ].
 550     apply nd_prod.
 551     eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ACanL ].
 552     eapply nd_comp; [ idtac | eapply postcompose_ ].
 553     apply ga_uncancelr.
 554
 555     eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AExch ].
 556     eapply nd_comp; [ idtac | eapply precompose ].
 557     apply pfb.
 558     Defined.
 559
 560   Definition arrange_brak : forall Γ Δ ec succ t,
 561    ND Rule
 562      [Γ > Δ >
 563       [(@ga_mk _ (v2t ec) [] (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: nil) succ))) @@  nil],,
 564       mapOptionTree (flatten_leveled_type ) (drop_lev (ec :: nil) succ) |- [t]@nil]
 565      [Γ > Δ > mapOptionTree (flatten_leveled_type ) succ |- [t]@nil].
 566
 567     intros.
 568     unfold drop_lev.
 569     set (@arrangeUnPartition _ succ (levelMatch (ec::nil))) as q.
 570     set (arrangeMap _ _ flatten_leveled_type q) as y.
 571     eapply nd_comp.
 572     Focus 2.
 573     eapply nd_rule.
 574     eapply RArrange.
 575     apply y.
 576     idtac.
 577     clear y q.
 578     eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AExch ].
 579     simpl.
 580     eapply nd_comp; [ apply nd_llecnac | idtac ].
 581     eapply nd_comp; [ idtac | eapply RLet ].
 582     apply nd_prod.
 583     Focus 2.
 584     apply nd_id.
 585     idtac.
 586     induction succ; try destruct a; simpl.
 587     unfold take_lev.
 588     unfold mkTakeFlags.
 589     unfold mkFlags.
 590     unfold bnot.
 591     simpl.
 592     destruct l as [t' lev'].
 593     destruct lev' as [|ec' lev'].
 594     simpl.
 595     apply ga_id.
 596     unfold levelMatch.
 597     set (@eqd_dec (HaskLevel Γ) (haskLevelEqDecidable Γ) (ec' :: lev') (ec :: nil)) as q.
 598     destruct q.
 599     inversion e; subst.
 600     simpl.
 601     apply nd_rule.
 602     unfold flatten_leveled_type.
 603     simpl.
 604     unfold flatten_type.
 605     simpl.
 606     unfold ga_mk.
 607     simpl.
 608     apply RVar.
 609     simpl.
 610     apply ga_id.
 611     apply ga_id.
 612     unfold take_lev.
 613     simpl.
 614     apply ga_join.
 615       apply IHsucc1.
 616       apply IHsucc2.
 617     Defined.
 618
 619   Definition arrange_esc : forall Γ Δ ec succ t,
 620    ND Rule
 621      [Γ > Δ > mapOptionTree (flatten_leveled_type ) succ |- [t]@nil]
 622      [Γ > Δ >
 623       [(@ga_mk _ (v2t ec) [] (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: nil) succ))) @@  nil],,
 624       mapOptionTree (flatten_leveled_type ) (drop_lev (ec :: nil) succ)  |- [t]@nil].
 625     intros.
 626     set (@arrangePartition _ succ (levelMatch (ec::nil))) as q.
 627     set (@drop_lev Γ (ec::nil) succ) as q'.
 628     assert (@drop_lev Γ (ec::nil) succ=q') as H.
 629       reflexivity.
 630     unfold drop_lev in H.
 631     unfold mkDropFlags in H.
 632     rewrite H in q.
 633     clear H.
 634     set (arrangeMap _ _ flatten_leveled_type q) as y.
 635     eapply nd_comp.
 636     eapply nd_rule.
 637     eapply RArrange.
 638     apply y.
 639     clear y q.
 640
 641     set (mapOptionTree flatten_leveled_type (dropT (mkFlags (liftBoolFunc false (bnot ○ levelMatch (ec :: nil))) succ))) as q.
 642     destruct (decide_tree_empty q); [ idtac | apply (Prelude_error "escapifying open code not yet supported") ].
 643     destruct s.
 644
 645     simpl.
 646     eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply AExch ].
 647     set (fun z z' => @RLet Γ Δ z (mapOptionTree flatten_leveled_type q') t z' nil) as q''.
 648     eapply nd_comp; [ idtac | apply RLet ].
 649     clear q''.
 650     eapply nd_comp; [ apply nd_rlecnac | idtac ].
 651     apply nd_prod.
 652     apply nd_rule.
 653     apply RArrange.
 654     eapply AComp; [ idtac | apply ACanR ].
 655     apply ALeft.
 656     apply (@arrangeCancelEmptyTree _ _ _ _ e).
 657
 658     eapply nd_comp.
 659       eapply nd_rule.
 660       eapply (@RVar Γ Δ t nil).
 661     apply nd_rule.
 662       apply RArrange.
 663       eapply AComp.
 664       apply AuCanR.
 665       apply ALeft.
 666       apply AWeak.
 667 (*
 668     eapply decide_tree_empty.
 669
 670     simpl.
 671     set (dropT (mkFlags (liftBoolFunc false (bnot ○ levelMatch (ec :: nil))) succ)) as escapified.
 672     destruct (decide_tree_empty escapified).
 673
 674     induction succ.
 675     destruct a.
 676       unfold drop_lev.
 677       destruct l.
 678       simpl.
 679       unfold mkDropFlags; simpl.
 680       unfold take_lev.
 681       unfold mkTakeFlags.
 682       simpl.
 683       destruct (General.list_eq_dec h0 (ec :: nil)).
 684         simpl.
 685         rewrite e.
 686         apply nd_id.
 687         simpl.
 688         apply nd_rule.
 689         apply RArrange.
 690         apply ALeft.
 691         apply AWeak.
 692       simpl.
 693         apply nd_rule.
 694         unfold take_lev.
 695         simpl.
 696         apply RArrange.
 697         apply ALeft.
 698         apply AWeak.
 699       apply (Prelude_error "escapifying code with multi-leaf antecedents is not supported").
 700 *)
 701       Defined.
 702
 703   Lemma unlev_relev : forall {Γ}(t:Tree ??(HaskType Γ ★)) lev, mapOptionTree unlev (t @@@ lev) = t.
 704     intros.
 705     induction t.
 706     destruct a; reflexivity.
 707     rewrite <- IHt1 at 2.
 708     rewrite <- IHt2 at 2.
 709     reflexivity.
 710     Qed.
 711
 712   Lemma tree_of_nothing : forall Γ ec t,
 713     Arrange (mapOptionTree flatten_leveled_type (drop_lev(Γ:=Γ) (ec :: nil) (t @@@ (ec :: nil)))) [].
 714     intros.
 715     induction t; try destruct o; try destruct a.
 716     simpl.
 717     drop_simplify.
 718     simpl.
 719     apply AId.
 720     simpl.
 721     apply AId.
 722     eapply AComp; [ idtac | apply ACanL ].
 723     eapply AComp; [ idtac | eapply ALeft; apply IHt2 ].
 724     Opaque drop_lev.
 725     simpl.
 726     Transparent drop_lev.
 727     idtac.
 728     drop_simplify.
 729     apply ARight.
 730     apply IHt1.
 731     Defined.
 732
 733   Lemma tree_of_nothing' : forall Γ ec t,
 734     Arrange [] (mapOptionTree flatten_leveled_type (drop_lev(Γ:=Γ) (ec :: nil) (t @@@ (ec :: nil)))).
 735     intros.
 736     induction t; try destruct o; try destruct a.
 737     simpl.
 738     drop_simplify.
 739     simpl.
 740     apply AId.
 741     simpl.
 742     apply AId.
 743     eapply AComp; [ apply AuCanL | idtac ].
 744     eapply AComp; [ eapply ARight; apply IHt1 | idtac ].
 745     Opaque drop_lev.
 746     simpl.
 747     Transparent drop_lev.
 748     idtac.
 749     drop_simplify.
 750     apply ALeft.
 751     apply IHt2.
 752     Defined.
 753
 754   Lemma krunk : forall Γ (ec:HaskTyVar Γ ECKind) t,
 755     flatten_type (<[ ec |- t ]>)
 756     = @ga_mk Γ (v2t ec)
 757     (mapOptionTree flatten_type (take_arg_types_as_tree t))
 758     [ flatten_type (drop_arg_types_as_tree   t)].
 759     intros.
 760     unfold flatten_type at 1.
 761     simpl.
 762     unfold ga_mk.
 763     apply phoas_extensionality.
 764     intros.
 765     unfold v2t.
 766     unfold ga_mk_raw.
 767     unfold ga_mk_tree.
 768     rewrite <- mapOptionTree_compose.
 769     unfold take_arg_types_as_tree.
 770     simpl.
 771     replace (flatten_type (drop_arg_types_as_tree t) tv ite)
 772       with (drop_arg_types (flatten_rawtype (t tv ite))).
 773     replace (unleaves_ (take_arg_types (flatten_rawtype (t tv ite))))
 774       with ((mapOptionTree (fun x : HaskType Γ ★ => flatten_type x tv ite)
 775            (unleaves_
 776               (take_trustme (count_arg_types (t (fun _ : Kind => unit) (ite_unit Γ)))
 777                  (fun TV : Kind → Type => take_arg_types ○ t TV))))).
 778     reflexivity.
 779     unfold flatten_type.
 780     clear hetmet_flatten.
 781     clear hetmet_unflatten.
 782     clear hetmet_id.
 783     clear gar.
 784     set (t tv ite) as x.
 785     admit.
 786     admit.
 787     Qed.
 788
 789   Lemma drop_to_nothing : forall (Γ:TypeEnv) Σ (lev:HaskLevel Γ),
 790     drop_lev lev (Σ @@@ lev) = mapTree (fun _ => None) (mapTree (fun _ => tt) Σ).
 791     intros.
 792     induction Σ.
 793     destruct a; simpl.
 794     drop_simplify.
 795     auto.
 796     drop_simplify.
 797     auto.
 798     simpl.
 799     rewrite <- IHΣ1.
 800     rewrite <- IHΣ2.
 801     reflexivity.
 802     Qed.
 803
 804   Definition flatten_skolemized_proof :
 805     forall  {h}{c},
 806       ND SRule h c ->
 807       ND  Rule (mapOptionTree (flatten_judgment ) h) (mapOptionTree (flatten_judgment ) c).
 808     intros.
 809     eapply nd_map'; [ idtac | apply X ].
 810     clear h c X.
 811     intros.
 812     simpl in *.
 813
 814     refine
 815       (match X as R in SRule H C with
 816       | SBrak    Γ Δ t ec succ lev           => let case_SBrak := tt         in _
 817       | SEsc     Γ Δ t ec succ lev           => let case_SEsc := tt          in _
 818       | SFlat    h c r                       => let case_SFlat := tt         in _
 819       end).
 820
 821     destruct case_SFlat.
 822     refine (match r as R in Rule H C with
 823       | RArrange Γ Δ a b x l d         => let case_RArrange := tt      in _
 824       | RNote    Γ Δ Σ τ l n           => let case_RNote := tt         in _
 825       | RLit     Γ Δ l     _           => let case_RLit := tt          in _
 826       | RVar     Γ Δ σ           lev   => let case_RVar := tt          in _
 827       | RGlobal  Γ Δ σ l wev           => let case_RGlobal := tt       in _
 828       | RLam     Γ Δ Σ tx te     lev   => let case_RLam := tt          in _
 829       | RCast    Γ Δ Σ σ τ lev γ       => let case_RCast := tt         in _
 830       | RAbsT    Γ Δ Σ κ σ lev         => let case_RAbsT := tt         in _
 831       | RAppT    Γ Δ Σ κ σ τ     lev   => let case_RAppT := tt         in _
 832       | RAppCo   Γ Δ Σ κ σ₁ σ₂ γ σ lev => let case_RAppCo := tt        in _
 833       | RAbsCo   Γ Δ Σ κ σ  σ₁ σ₂  lev => let case_RAbsCo := tt        in _
 834       | RApp     Γ Δ Σ₁ Σ₂ tx te lev   => let case_RApp := tt          in _
 835       | RCut     Γ Δ Σ Σ₁ Σ₁₂ Σ₂ Σ₃ l  => let case_RCut := tt          in _
 836       | RLeft    Γ Δ Σ₁ Σ₂  Σ     l    => let case_RLeft := tt in _
 837       | RRight   Γ Δ Σ₁ Σ₂  Σ     l    => let case_RRight := 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_RCut.
 962       simpl.
 963       destruct l as [|ec lev]; simpl.
 964         apply nd_rule.
 965         replace (mapOptionTree flatten_leveled_type (Σ₁₂ @@@ nil)) with (mapOptionTree flatten_type Σ₁₂ @@@ nil).
 966         apply RCut.
 967         induction Σ₁₂; try destruct a; auto.
 968         simpl.
 969         rewrite <- IHΣ₁₂1.
 970         rewrite <- IHΣ₁₂2.
 971         reflexivity.
 972       simpl; repeat drop_simplify.
 973       simpl; repeat take_simplify.
 974       simpl.
 975       set (drop_lev (ec :: lev) (Σ₁₂ @@@ (ec :: lev))) as x1.
 976       rewrite take_lemma'.
 977       rewrite mapOptionTree_compose.
 978       rewrite mapOptionTree_compose.
 979       rewrite mapOptionTree_compose.
 980       rewrite mapOptionTree_compose.
 981       rewrite unlev_relev.
 982       rewrite <- mapOptionTree_compose.
 983       rewrite <- mapOptionTree_compose.
 984       rewrite <- mapOptionTree_compose.
 985       eapply nd_comp; [ idtac | eapply nd_rule; eapply RCut ].
 986       apply nd_prod.
 987       apply nd_id.
 988       eapply nd_comp.
 989       eapply nd_rule.
 990       eapply RArrange.
 991       eapply ALeft.
 992       eapply ARight.
 993       unfold x1.
 994       rewrite drop_to_nothing.
 995       apply arrangeCancelEmptyTree with (q:=(mapTree (fun _ : ??(HaskType Γ ★) => tt) Σ₁₂)).
 996         induction Σ₁₂; try destruct a; auto.
 997         simpl.
 998         rewrite <- IHΣ₁₂1 at 2.
 999         rewrite <- IHΣ₁₂2 at 2.
1000         reflexivity.
1001       eapply nd_comp; [ eapply nd_rule; eapply RArrange; eapply ALeft; eapply ACanL | idtac ].
1002       set (mapOptionTree flatten_type Σ₁₂) as a.
1003       set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) Σ₁)) as b.
1004       set (mapOptionTree flatten_leveled_type (drop_lev (ec :: lev) Σ₂)) as c.
1005       set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) Σ₂)) as d.
1006       set (mapOptionTree flatten_leveled_type (drop_lev (ec :: lev) Σ)) as e.
1007       set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) Σ)) as f.
1008       eapply nd_comp; [ idtac | eapply nd_rule; eapply RCut ].
1009       eapply nd_comp; [ apply nd_llecnac | idtac ].
1010       apply nd_prod.
1011       simpl.
1012       eapply secondify.
1013       apply ga_first.
1014       eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ALeft; eapply AExch ].
1015       eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AuAssoc ].
1016       simpl.
1017       apply precompose.
1018
1019     destruct case_RLeft.
1020       simpl.
1021       destruct l as [|ec lev].
1022       simpl.
1023         replace (mapOptionTree flatten_leveled_type (Σ @@@ nil)) with (mapOptionTree flatten_type Σ @@@ nil).
1024         apply nd_rule.
1025         apply RLeft.
1026         induction Σ; try destruct a; auto.
1027         simpl.
1028         rewrite <- IHΣ1.
1029         rewrite <- IHΣ2.
1030         reflexivity.
1031       repeat drop_simplify.
1032         rewrite drop_to_nothing.
1033         simpl.
1034         eapply nd_comp.
1035         Focus 2.
1036         eapply nd_rule.
1037         eapply RArrange.
1038         eapply ARight.
1039         apply arrangeUnCancelEmptyTree with (q:=(mapTree (fun _ : ??(HaskType Γ ★) => tt) Σ)).
1040           induction Σ; try destruct a; auto.
1041           simpl.
1042           rewrite <- IHΣ1 at 2.
1043           rewrite <- IHΣ2 at 2.
1044           reflexivity.
1045         idtac.
1046         eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AuCanL ].
1047         apply boost.
1048         take_simplify.
1049         simpl.
1050         replace (take_lev (ec :: lev) (Σ @@@ (ec :: lev))) with (Σ @@@ (ec::lev)).
1051         rewrite mapOptionTree_compose.
1052         rewrite mapOptionTree_compose.
1053         rewrite unlev_relev.
1054         apply ga_second.
1055       rewrite take_lemma'.
1056       reflexivity.
1057
1058     destruct case_RRight.
1059       simpl.
1060       destruct l as [|ec lev].
1061       simpl.
1062         replace (mapOptionTree flatten_leveled_type (Σ @@@ nil)) with (mapOptionTree flatten_type Σ @@@ nil).
1063         apply nd_rule.
1064         apply RRight.
1065         induction Σ; try destruct a; auto.
1066         simpl.
1067         rewrite <- IHΣ1.
1068         rewrite <- IHΣ2.
1069         reflexivity.
1070       repeat drop_simplify.
1071         rewrite drop_to_nothing.
1072         simpl.
1073         eapply nd_comp.
1074         Focus 2.
1075         eapply nd_rule.
1076         eapply RArrange.
1077         eapply ALeft.
1078         apply arrangeUnCancelEmptyTree with (q:=(mapTree (fun _ : ??(HaskType Γ ★) => tt) Σ)).
1079           induction Σ; try destruct a; auto.
1080           simpl.
1081           rewrite <- IHΣ1 at 2.
1082           rewrite <- IHΣ2 at 2.
1083           reflexivity.
1084         idtac.
1085         eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AuCanR ].
1086         apply boost.
1087         take_simplify.
1088         simpl.
1089         replace (take_lev (ec :: lev) (Σ @@@ (ec :: lev))) with (Σ @@@ (ec::lev)).
1090         rewrite mapOptionTree_compose.
1091         rewrite mapOptionTree_compose.
1092         rewrite unlev_relev.
1093         apply ga_first.
1094       rewrite take_lemma'.
1095       reflexivity.
1096
1097     destruct case_RVoid.
1098       simpl.
1099       destruct l.
1100       apply nd_rule.
1101       apply RVoid.
1102       drop_simplify.
1103       take_simplify.
1104       simpl.
1105       apply ga_id.
1106
1107     destruct case_RAppT.
1108       simpl. destruct lev; simpl.
1109       unfold flatten_leveled_type.
1110       simpl.
1111       rewrite flatten_commutes_with_HaskTAll.
1112       rewrite flatten_commutes_with_substT.
1113       apply nd_rule.
1114       apply RAppT.
1115       apply Δ.
1116       apply Δ.
1117       apply (Prelude_error "found type application at level >0; this is not supported").
1118
1119     destruct case_RAbsT.
1120       simpl. destruct lev; simpl.
1121       rewrite flatten_commutes_with_HaskTAll.
1122       rewrite flatten_commutes_with_HaskTApp.
1123       eapply nd_comp; [ idtac | eapply nd_rule; eapply RAbsT ].
1124       simpl.
1125       set (mapOptionTree (flatten_leveled_type ) (mapOptionTree (weakLT(κ:=κ)) Σ)) as a.
1126       set (mapOptionTree (weakLT(κ:=κ)) (mapOptionTree (flatten_leveled_type ) Σ)) as q'.
1127       assert (a=q').
1128         unfold a.
1129         unfold q'.
1130         clear a q'.
1131         induction Σ.
1132           destruct a.
1133           simpl.
1134           rewrite flatten_commutes_with_weakLT.
1135           reflexivity.
1136           reflexivity.
1137           simpl.
1138           rewrite <- IHΣ1.
1139           rewrite <- IHΣ2.
1140           reflexivity.
1141       rewrite H.
1142       apply nd_id.
1143       apply Δ.
1144       apply Δ.
1145       apply (Prelude_error "found type abstraction at level >0; this is not supported").
1146
1147     destruct case_RAppCo.
1148       simpl. destruct lev; simpl.
1149       unfold flatten_type.
1150       simpl.
1151       apply nd_rule.
1152       apply RAppCo.
1153       apply flatten_coercion.
1154       apply γ.
1155       apply (Prelude_error "found coercion application at level >0; this is not supported").
1156
1157     destruct case_RAbsCo.
1158       simpl. destruct lev; simpl.
1159       unfold flatten_type.
1160       simpl.
1161       apply (Prelude_error "AbsCo not supported (FIXME)").
1162       apply (Prelude_error "found coercion abstraction at level >0; this is not supported").
1163
1164     destruct case_RLetRec.
1165       rename t into lev.
1166       simpl. destruct lev; simpl.
1167       apply nd_rule.
1168       set (@RLetRec Γ Δ (mapOptionTree flatten_leveled_type lri) (flatten_type x) (mapOptionTree flatten_type y) nil) as q.
1169       replace (mapOptionTree flatten_leveled_type (y @@@ nil)) with (mapOptionTree flatten_type y @@@ nil).
1170       apply q.
1171         induction y; try destruct a; auto.
1172         simpl.
1173         rewrite IHy1.
1174         rewrite IHy2.
1175         reflexivity.
1176       repeat drop_simplify.
1177       repeat take_simplify.
1178       simpl.
1179       rewrite drop_to_nothing.
1180       eapply nd_comp.
1181         eapply nd_rule.
1182         eapply RArrange.
1183         eapply AComp.
1184         eapply ARight.
1185         apply arrangeCancelEmptyTree with (q:=y).
1186           induction y; try destruct a; auto.
1187           simpl.
1188           rewrite <- IHy1.
1189           rewrite <- IHy2.
1190           reflexivity.
1191         apply ACanL.
1192         rewrite take_lemma'.
1193         set (mapOptionTree (flatten_type ○ unlev) (take_lev (h :: lev) lri)) as lri'.
1194         set (mapOptionTree flatten_leveled_type (drop_lev (h :: lev) lri)) as lri''.
1195         replace (mapOptionTree (flatten_type ○ unlev) (y @@@ (h :: lev))) with (mapOptionTree flatten_type y).
1196         apply boost.
1197         apply ga_loopl.
1198         rewrite <- mapOptionTree_compose.
1199         simpl.
1200         reflexivity.
1201
1202     destruct case_RCase.
1203       simpl.
1204       apply (Prelude_error "Case not supported (BIG FIXME)").
1205
1206     destruct case_SBrak.
1207       simpl.
1208       destruct lev.
1209       drop_simplify.
1210       set (drop_lev (ec :: nil) (take_arg_types_as_tree t @@@ (ec :: nil))) as empty_tree.
1211       take_simplify.
1212       rewrite take_lemma'.
1213       simpl.
1214       rewrite mapOptionTree_compose.
1215       rewrite mapOptionTree_compose.
1216       rewrite unlev_relev.
1217       rewrite <- mapOptionTree_compose.
1218       simpl.
1219       rewrite krunk.
1220       set (mapOptionTree flatten_leveled_type (drop_lev (ec :: nil) succ)) as succ_host.
1221       set (mapOptionTree (flatten_type ○ unlev)(take_lev (ec :: nil) succ)) as succ_guest.
1222       set (mapOptionTree flatten_type (take_arg_types_as_tree t)) as succ_args.
1223       unfold empty_tree.
1224       eapply nd_comp; [ eapply nd_rule; eapply RArrange; eapply ALeft; apply tree_of_nothing | idtac ].
1225       eapply nd_comp; [ eapply nd_rule; eapply RArrange; eapply ACanR | idtac ].
1226       refine (ga_unkappa Γ Δ (v2t ec) nil _ _ _ _ ;; _).
1227       eapply nd_comp; [ idtac | eapply arrange_brak ].
1228       unfold succ_host.
1229       unfold succ_guest.
1230       eapply nd_rule.
1231         eapply RArrange.
1232         apply AExch.
1233       apply (Prelude_error "found Brak at depth >0 indicating 3-level code; only two-level code is currently supported").
1234
1235     destruct case_SEsc.
1236       simpl.
1237       destruct lev.
1238       simpl.
1239       unfold flatten_leveled_type at 2.
1240       simpl.
1241       rewrite krunk.
1242       rewrite mapOptionTree_compose.
1243       take_simplify.
1244       drop_simplify.
1245       simpl.
1246       eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ALeft; apply tree_of_nothing' ].
1247       eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ACanR ].
1248       simpl.
1249       rewrite take_lemma'.
1250       rewrite unlev_relev.
1251       rewrite <- mapOptionTree_compose.
1252       eapply nd_comp; [ apply (arrange_esc _ _ ec) | idtac ].
1253
1254       set (decide_tree_empty (take_lev (ec :: nil) succ)) as q'.
1255       destruct q'.
1256       destruct s.
1257       rewrite e.
1258       clear e.
1259
1260       set (mapOptionTree flatten_leveled_type (drop_lev (ec :: nil) succ)) as succ_host.
1261       set (mapOptionTree flatten_type (take_arg_types_as_tree t)) as succ_args.
1262
1263       eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply AuCanR ].
1264       eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply AuCanR ].
1265       eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply ACanL ].
1266       eapply nd_comp; [ idtac | eapply RLet ].
1267       eapply nd_comp; [ apply nd_llecnac | idtac ].
1268       apply nd_prod; [ idtac | eapply boost ].
1269       induction x.
1270         apply ga_id.
1271         eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ACanL ].
1272         simpl.
1273         apply ga_join.
1274           apply IHx1.
1275           apply IHx2.
1276           simpl.
1277           apply postcompose.
1278
1279       refine ( _ ;; (boost _ _ _ _ _ (postcompose _ _ _ _ _ _ _ _))).
1280       apply ga_cancell.
1281       apply firstify.
1282
1283       induction x.
1284         destruct a; simpl.
1285         apply ga_id.
1286         simpl.
1287         refine ( _ ;; (boost _ _ _ _ _ (postcompose _ _ _ _ _ _ _ _))).
1288         apply ga_cancell.
1289         refine ( _ ;; (boost _ _ _ _ _ (postcompose _ _ _ _ _ _ _ _))).
1290         eapply firstify.
1291         apply IHx1.
1292         apply secondify.
1293         apply IHx2.
1294
1295       (* environment has non-empty leaves *)
1296       apply (Prelude_error "ga_kappa not supported yet (BIG FIXME)").
1297
1298       (* nesting too deep *)
1299       apply (Prelude_error "found Esc at depth >0 indicating 3-level code; only two-level code is currently supported").
1300       Defined.
1301
1302   Definition flatten_proof :
1303     forall  {h}{c},
1304       ND  Rule h c ->
1305       ND  Rule h c.
1306     apply (Prelude_error "sorry, non-skolemized flattening isn't implemented").
1307     Defined.
1308
1309   Definition skolemize_and_flatten_proof :
1310     forall  {h}{c},
1311       ND  Rule h c ->
1312       ND  Rule
1313            (mapOptionTree (flatten_judgment ○ skolemize_judgment) h)
1314            (mapOptionTree (flatten_judgment ○ skolemize_judgment) c).
1315     intros.
1316     rewrite mapOptionTree_compose.
1317     rewrite mapOptionTree_compose.
1318     apply flatten_skolemized_proof.
1319     apply skolemize_proof.
1320     apply X.
1321     Defined.
1322
1323
1324   (* to do: establish some metric on judgments (max length of level of any succedent type, probably), show how to
1325    * calculate it, and show that the flattening procedure above drives it down by one *)
1326
1327   (*
1328   Instance FlatteningFunctor {Γ}{Δ}{ec} : Functor (JudgmentsL (PCF Γ Δ ec)) (TypesL (SystemFCa Γ Δ)) (obact) :=
1329     { fmor := FlatteningFunctor_fmor }.
1330
1331   Definition ReificationFunctor Γ Δ : Functor (JudgmentsL _ _ (PCF n Γ Δ)) SystemFCa' (mapOptionTree brakifyJudg).
1332     refine {| fmor := ReificationFunctor_fmor Γ Δ |}; unfold hom; unfold ob; simpl ; intros.
1333
1334   Definition PCF_SMME (n:nat)(Γ:TypeEnv)(Δ:CoercionEnv Γ) : ProgrammingLanguageSMME.
1335     refine {| plsmme_pl := PCF n Γ Δ |}.
1336     Defined.
1337
1338   Definition SystemFCa_SMME (n:nat)(Γ:TypeEnv)(Δ:CoercionEnv Γ) : ProgrammingLanguageSMME.
1339     refine {| plsmme_pl := SystemFCa n Γ Δ |}.
1340     Defined.
1341
1342   Definition ReificationFunctorMonoidal n : MonoidalFunctor (JudgmentsN n) (JudgmentsN (S n)) (ReificationFunctor n).
1343     Defined.
1344
1345   (* 5.1.4 *)
1346   Definition PCF_SystemFCa_two_level n Γ Δ : TwoLevelLanguage (PCF_SMME n Γ Δ) (SystemFCa_SMME (S n) Γ Δ).
1347     Defined.
1348   *)
1349   (*  ... and the retraction exists *)
1350
1351 End HaskFlattener.
1352
1353 Implicit Arguments garrow [ ].