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