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   (* This tries to assign a single level to the entire succedent of a judgment.  If the succedent has types from different
 312    * levels (should not happen) it just picks one; if the succedent has no non-None leaves (also should not happen) it
 313    * picks nil *)
 314   Definition getΓ (j:Judg) := match j with Γ > _ > _ |- _ => Γ end.
 315   Definition getSuc (j:Judg) : Tree ??(LeveledHaskType (getΓ j) ★) :=
 316     match j as J return Tree ??(LeveledHaskType (getΓ J) ★) with Γ > _ > _ |- s => s end.
 317   Fixpoint getjlev {Γ}(tt:Tree ??(LeveledHaskType Γ ★)) : HaskLevel Γ :=
 318     match tt with
 319       | T_Leaf None              => nil
 320       | T_Leaf (Some (_ @@ lev)) => lev
 321       | T_Branch b1 b2 =>
 322         match getjlev b1 with
 323           | nil => getjlev b2
 324           | lev => lev
 325         end
 326     end.
 327
 328   (* "n" is the maximum depth remaining AFTER flattening *)
 329   Definition flatten_judgment (j:Judg) :=
 330     match j as J return Judg with
 331       Γ > Δ > ant |- suc =>
 332         match getjlev suc with
 333           | nil        => Γ > Δ > mapOptionTree flatten_leveled_type ant
 334                                |- mapOptionTree flatten_leveled_type suc
 335
 336           | (ec::lev') => Γ > Δ > mapOptionTree flatten_leveled_type (drop_lev (ec::lev') ant)
 337                                |- [ga_mk (v2t ec)
 338                                          (mapOptionTree (flatten_type ○ unlev) (take_lev (ec::lev') ant))
 339                                          (mapOptionTree (flatten_type ○ unlev)                      suc )
 340                                          @@ nil]  (* we know the level of all of suc *)
 341         end
 342     end.
 343
 344   Class garrow :=
 345   { ga_id        : ∀ Γ Δ ec l a    , ND Rule [] [Γ > Δ >                          [] |- [@ga_mk Γ ec a a @@ l] ]
 346   ; ga_cancelr   : ∀ Γ Δ ec l a    , ND Rule [] [Γ > Δ >                          [] |- [@ga_mk Γ ec (a,,[]) a @@ l] ]
 347   ; ga_cancell   : ∀ Γ Δ ec l a    , ND Rule [] [Γ > Δ >                          [] |- [@ga_mk Γ ec ([],,a) a @@ l] ]
 348   ; ga_uncancelr : ∀ Γ Δ ec l a    , ND Rule [] [Γ > Δ >                          [] |- [@ga_mk Γ ec a (a,,[]) @@ l] ]
 349   ; ga_uncancell : ∀ Γ Δ ec l a    , ND Rule [] [Γ > Δ >                          [] |- [@ga_mk Γ ec a ([],,a) @@ l] ]
 350   ; ga_assoc     : ∀ Γ Δ ec l a b c, ND Rule [] [Γ > Δ >                          [] |- [@ga_mk Γ ec ((a,,b),,c) (a,,(b,,c)) @@ l] ]
 351   ; ga_unassoc   : ∀ Γ Δ ec l a b c, ND Rule [] [Γ > Δ >                          [] |- [@ga_mk Γ ec (a,,(b,,c)) ((a,,b),,c) @@ l] ]
 352   ; ga_swap      : ∀ Γ Δ ec l a b  , ND Rule [] [Γ > Δ >                          [] |- [@ga_mk Γ ec (a,,b) (b,,a) @@ l] ]
 353   ; ga_drop      : ∀ Γ Δ ec l a    , ND Rule [] [Γ > Δ >                          [] |- [@ga_mk Γ ec a [] @@ l] ]
 354   ; ga_copy      : ∀ Γ Δ ec l a    , ND Rule [] [Γ > Δ >                          [] |- [@ga_mk Γ ec a (a,,a) @@ l] ]
 355   ; ga_first     : ∀ Γ Δ ec l a b x, ND Rule [] [Γ > Δ >      [@ga_mk Γ ec a b @@ l] |- [@ga_mk Γ ec (a,,x) (b,,x) @@ l] ]
 356   ; ga_second    : ∀ Γ Δ ec l a b x, ND Rule [] [Γ > Δ >      [@ga_mk Γ ec a b @@ l] |- [@ga_mk Γ ec (x,,a) (x,,b) @@ l] ]
 357   ; ga_lit       : ∀ Γ Δ ec l lit  , ND Rule [] [Γ > Δ >                          [] |- [@ga_mk Γ ec [] [literalType lit] @@ l] ]
 358   ; ga_curry     : ∀ Γ Δ ec l a b c, ND Rule [] [Γ > Δ > [@ga_mk Γ ec (a,,[b]) [c] @@ l] |- [@ga_mk Γ ec a [b ---> c] @@ l] ]
 359   ; 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] ]
 360   ; ga_apply     : ∀ Γ Δ ec l a a' b c,
 361                  ND Rule [] [Γ > Δ > [@ga_mk Γ ec a [b ---> c] @@ l],,[@ga_mk Γ ec a' [b] @@ l] |- [@ga_mk Γ ec (a,,a') [c] @@ l] ]
 362   ; ga_kappa     : ∀ Γ Δ ec l a b Σ, ND Rule
 363   [Γ > Δ > Σ,,[@ga_mk Γ ec [] a @@ l] |- [@ga_mk Γ ec [] b @@ l] ]
 364   [Γ > Δ > Σ          |- [@ga_mk Γ ec a  b @@ l] ]
 365   }.
 366   Context `(gar:garrow).
 367
 368   Notation "a ~~~~> b" := (@ga_mk _ _ a b) (at level 20).
 369
 370   Definition boost : forall Γ Δ ant x y {lev},
 371     ND Rule []                          [ Γ > Δ > [x@@lev] |- [y@@lev] ] ->
 372     ND Rule [ Γ > Δ > ant |- [x@@lev] ] [ Γ > Δ > ant      |- [y@@lev] ].
 373     intros.
 374     eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanL ].
 375     eapply nd_comp; [ idtac | eapply nd_rule; apply (@RLet Γ Δ [] ant y x lev) ].
 376     eapply nd_comp; [ apply nd_rlecnac | idtac ].
 377     apply nd_prod.
 378     apply nd_id.
 379     eapply nd_comp.
 380       apply X.
 381       eapply nd_rule.
 382       eapply RArrange.
 383       apply RuCanL.
 384       Defined.
 385
 386   Definition postcompose' : ∀ Γ Δ ec lev a b c Σ,
 387      ND Rule [] [ Γ > Δ > Σ                        |- [@ga_mk Γ ec a b @@ lev] ] ->
 388      ND Rule [] [ Γ > Δ > Σ,,[@ga_mk Γ ec b c @@ lev] |- [@ga_mk Γ ec a c @@ lev] ].
 389      intros.
 390      eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RExch ].
 391      eapply nd_comp; [ idtac
 392        | eapply nd_rule; apply (@RLet Γ Δ [@ga_mk _ ec b c @@lev] Σ (@ga_mk _ ec a c) (@ga_mk _ ec a b) lev) ].
 393      eapply nd_comp; [ apply nd_llecnac | idtac ].
 394      apply nd_prod.
 395      apply X.
 396      eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RExch ].
 397      apply ga_comp.
 398      Defined.
 399
 400   Definition precompose Γ Δ ec : forall a x y z lev,
 401     ND Rule
 402       [ Γ > Δ > a                           |- [@ga_mk _ ec y z @@ lev] ]
 403       [ Γ > Δ > a,,[@ga_mk _ ec x y @@ lev] |- [@ga_mk _ ec x z @@ lev] ].
 404     intros.
 405     eapply nd_comp.
 406     apply nd_rlecnac.
 407     eapply nd_comp.
 408     eapply nd_prod.
 409     apply nd_id.
 410     eapply ga_comp.
 411
 412     eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RExch ].
 413
 414     apply nd_rule.
 415     apply RLet.
 416     Defined.
 417
 418   Definition precompose' : ∀ Γ Δ ec lev a b c Σ,
 419      ND Rule [] [ Γ > Δ > Σ                           |- [@ga_mk Γ ec b c @@ lev] ] ->
 420      ND Rule [] [ Γ > Δ > Σ,,[@ga_mk Γ ec a b @@ lev] |- [@ga_mk Γ ec a c @@ lev] ].
 421      intros.
 422      eapply nd_comp.
 423      apply X.
 424      apply precompose.
 425      Defined.
 426
 427   Definition postcompose : ∀ Γ Δ ec lev a b c,
 428      ND Rule [] [ Γ > Δ > []                    |- [@ga_mk Γ ec a b @@ lev] ] ->
 429      ND Rule [] [ Γ > Δ > [@ga_mk Γ ec b c @@ lev] |- [@ga_mk Γ ec a c @@ lev] ].
 430      intros.
 431      eapply nd_comp.
 432      apply postcompose'.
 433      apply X.
 434      apply nd_rule.
 435      apply RArrange.
 436      apply RCanL.
 437      Defined.
 438
 439   Definition firstify : ∀ Γ Δ ec lev a b c Σ,
 440     ND Rule [] [ Γ > Δ > Σ                     |- [@ga_mk Γ ec a b @@ lev] ] ->
 441     ND Rule [] [ Γ > Δ > Σ                    |- [@ga_mk Γ ec (a,,c) (b,,c) @@ lev] ].
 442     intros.
 443     eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanL ].
 444     eapply nd_comp; [ idtac | eapply nd_rule; apply RLet ].
 445     eapply nd_comp; [ apply nd_llecnac | idtac ].
 446     apply nd_prod.
 447     apply X.
 448     eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RuCanL ].
 449     apply ga_first.
 450     Defined.
 451
 452   Definition secondify : ∀ Γ Δ ec lev a b c Σ,
 453      ND Rule [] [ Γ > Δ > Σ                    |- [@ga_mk Γ ec a b @@ lev] ] ->
 454      ND Rule [] [ Γ > Δ > Σ                    |- [@ga_mk Γ ec (c,,a) (c,,b) @@ lev] ].
 455     intros.
 456     eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanL ].
 457     eapply nd_comp; [ idtac | eapply nd_rule; apply RLet ].
 458     eapply nd_comp; [ apply nd_llecnac | idtac ].
 459     apply nd_prod.
 460     apply X.
 461     eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RuCanL ].
 462     apply ga_second.
 463     Defined.
 464
 465   Lemma ga_unkappa     : ∀ Γ Δ ec l z a b Σ,
 466     ND Rule
 467     [Γ > Δ > Σ                         |- [@ga_mk Γ ec a b @@ l] ]
 468     [Γ > Δ > Σ,,[@ga_mk Γ ec z a @@ l] |- [@ga_mk Γ ec z b @@ l] ].
 469     intros.
 470     set (ga_comp Γ Δ ec l z a b) as q.
 471
 472     set (@RLet Γ Δ) as q'.
 473     set (@RLet Γ Δ [@ga_mk _ ec z a @@ l] Σ (@ga_mk _ ec z b) (@ga_mk _ ec a b) l) as q''.
 474     eapply nd_comp.
 475     Focus 2.
 476     eapply nd_rule.
 477     eapply RArrange.
 478     apply RExch.
 479
 480     eapply nd_comp.
 481     Focus 2.
 482     eapply nd_rule.
 483     apply q''.
 484
 485     idtac.
 486     clear q'' q'.
 487     eapply nd_comp.
 488     apply nd_rlecnac.
 489     apply nd_prod.
 490     apply nd_id.
 491     apply q.
 492     Defined.
 493
 494   Lemma ga_unkappa'     : ∀ Γ Δ ec l a b Σ x,
 495     ND Rule
 496     [Γ > Δ > Σ                          |- [@ga_mk Γ ec (a,,x)  b @@ l] ]
 497     [Γ > Δ > Σ,,[@ga_mk Γ ec [] a @@ l] |- [@ga_mk Γ ec x       b @@ l] ].
 498     intros.
 499     eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
 500     eapply nd_comp; [ apply nd_llecnac | idtac ].
 501     apply nd_prod.
 502     apply ga_first.
 503
 504     eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
 505     eapply nd_comp; [ apply nd_llecnac | idtac ].
 506     apply nd_prod.
 507     apply postcompose.
 508     apply ga_uncancell.
 509     apply precompose.
 510     Defined.
 511
 512   Lemma ga_kappa'     : ∀ Γ Δ ec l a b Σ x,
 513     ND Rule
 514     [Γ > Δ > Σ,,[@ga_mk Γ ec [] a @@ l] |- [@ga_mk Γ ec x b @@ l] ]
 515     [Γ > Δ > Σ                          |- [@ga_mk Γ ec (a,,x)  b @@ l] ].
 516     apply (Prelude_error "ga_kappa not supported yet (BIG FIXME)").
 517     Defined.
 518
 519   (* useful for cutting down on the pretty-printed noise
 520
 521   Notation "`  x" := (take_lev _ x) (at level 20).
 522   Notation "`` x" := (mapOptionTree unlev x) (at level 20).
 523   Notation "``` x" := (drop_lev _ x) (at level 20).
 524   *)
 525   Definition flatten_arrangement' :
 526     forall Γ (Δ:CoercionEnv Γ)
 527       (ec:HaskTyVar Γ ECKind) (lev:HaskLevel Γ) (ant1 ant2:Tree ??(LeveledHaskType Γ ★)) (r:Arrange ant1 ant2),
 528       ND Rule [] [Γ > Δ > [] |- [@ga_mk _ (v2t ec) (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) ant2))
 529         (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) ant1)) @@ nil] ].
 530
 531       intros Γ Δ ec lev.
 532       refine (fix flatten ant1 ant2 (r:Arrange ant1 ant2):
 533            ND Rule [] [Γ > Δ > [] |- [@ga_mk _ (v2t ec)
 534              (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) ant2))
 535              (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) ant1)) @@ nil]] :=
 536         match r as R in Arrange A B return
 537           ND Rule [] [Γ > Δ > [] |- [@ga_mk _ (v2t ec)
 538             (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) B))
 539             (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) A)) @@ nil]]
 540           with
 541           | RCanL  a             => let case_RCanL := tt  in ga_uncancell _ _ _ _ _
 542           | RCanR  a             => let case_RCanR := tt  in ga_uncancelr _ _ _ _ _
 543           | RuCanL a             => let case_RuCanL := tt in ga_cancell _ _ _ _ _
 544           | RuCanR a             => let case_RuCanR := tt in ga_cancelr _ _ _ _ _
 545           | RAssoc a b c         => let case_RAssoc := tt in ga_assoc _ _ _ _ _ _ _
 546           | RCossa a b c         => let case_RCossa := tt in ga_unassoc _ _ _ _ _ _ _
 547           | RExch  a b           => let case_RExch := tt  in ga_swap  _ _ _ _ _ _
 548           | RWeak  a             => let case_RWeak := tt  in ga_drop _ _ _ _ _
 549           | RCont  a             => let case_RCont := tt  in ga_copy  _ _ _ _ _
 550           | RLeft  a b c r'      => let case_RLeft := tt  in flatten _ _ r' ;; boost _ _ _ _ _ (ga_second _ _ _ _ _ _ _)
 551           | RRight a b c r'      => let case_RRight := tt in flatten _ _ r' ;; boost _ _ _ _ _ (ga_first  _ _ _ _ _ _ _)
 552           | RComp  c b a r1 r2   => let case_RComp := tt  in (fun r1' r2' => _) (flatten _ _ r1) (flatten _ _ r2)
 553         end); clear flatten; repeat take_simplify; repeat drop_simplify; intros.
 554
 555         destruct case_RComp.
 556           set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) a)) as a' in *.
 557           set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) b)) as b' in *.
 558           set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) c)) as c' in *.
 559           eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RCanL ].
 560           eapply nd_comp; [ idtac | eapply nd_rule; apply
 561              (@RLet Γ Δ [] [] (@ga_mk _ (v2t ec) a' c') (@ga_mk _ (v2t ec) a' b')) ].
 562           eapply nd_comp; [ apply nd_llecnac | idtac ].
 563           apply nd_prod.
 564           apply r2'.
 565           eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RuCanL ].
 566           eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RCanR ].
 567           eapply nd_comp; [ idtac | eapply nd_rule;  apply
 568             (@RLet Γ Δ [@ga_mk _ (v2t ec) a' b' @@ _] [] (@ga_mk _ (v2t ec) a' c') (@ga_mk _ (v2t ec) b' c'))].
 569           eapply nd_comp; [ apply nd_llecnac | idtac ].
 570           eapply nd_prod.
 571           apply r1'.
 572           apply ga_comp.
 573           Defined.
 574
 575   Definition flatten_arrangement :
 576     forall Γ (Δ:CoercionEnv Γ) n
 577       (ec:HaskTyVar Γ ECKind) (lev:HaskLevel Γ) (ant1 ant2:Tree ??(LeveledHaskType Γ ★)) (r:Arrange ant1 ant2) succ,
 578       ND Rule
 579       [Γ > Δ > mapOptionTree (flatten_leveled_type ) (drop_lev n ant1)
 580         |- [@ga_mk _ (v2t ec)
 581           (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) ant1))
 582           (mapOptionTree (flatten_type ○ unlev) succ) @@ nil]]
 583       [Γ > Δ > mapOptionTree (flatten_leveled_type ) (drop_lev n ant2)
 584         |- [@ga_mk _ (v2t ec)
 585           (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) ant2))
 586           (mapOptionTree (flatten_type ○ unlev) succ) @@ nil]].
 587       intros.
 588       refine ( _ ;; (boost _ _ _ _ _ (postcompose _ _ _ _ _ _ _ (flatten_arrangement' Γ Δ ec lev ant1 ant2 r)))).
 589       apply nd_rule.
 590       apply RArrange.
 591       refine ((fix flatten ant1 ant2 (r:Arrange ant1 ant2) :=
 592         match r as R in Arrange A B return
 593           Arrange (mapOptionTree (flatten_leveled_type ) (drop_lev _ A))
 594           (mapOptionTree (flatten_leveled_type ) (drop_lev _ B)) with
 595           | RCanL  a             => let case_RCanL := tt  in RCanL _
 596           | RCanR  a             => let case_RCanR := tt  in RCanR _
 597           | RuCanL a             => let case_RuCanL := tt in RuCanL _
 598           | RuCanR a             => let case_RuCanR := tt in RuCanR _
 599           | RAssoc a b c         => let case_RAssoc := tt in RAssoc _ _ _
 600           | RCossa a b c         => let case_RCossa := tt in RCossa _ _ _
 601           | RExch  a b           => let case_RExch := tt  in RExch _ _
 602           | RWeak  a             => let case_RWeak := tt  in RWeak _
 603           | RCont  a             => let case_RCont := tt  in RCont _
 604           | RLeft  a b c r'      => let case_RLeft := tt  in RLeft  _ (flatten _ _ r')
 605           | RRight a b c r'      => let case_RRight := tt in RRight _ (flatten _ _ r')
 606           | RComp  a b c r1 r2   => let case_RComp := tt  in RComp    (flatten _ _ r1) (flatten _ _ r2)
 607         end) ant1 ant2 r); clear flatten; repeat take_simplify; repeat drop_simplify; intros.
 608         Defined.
 609
 610   Definition flatten_arrangement'' :
 611     forall  Γ Δ ant1 ant2 succ (r:Arrange ant1 ant2),
 612       ND Rule (mapOptionTree (flatten_judgment ) [Γ > Δ > ant1 |- succ])
 613       (mapOptionTree (flatten_judgment ) [Γ > Δ > ant2 |- succ]).
 614     intros.
 615     simpl.
 616     set (getjlev succ) as succ_lev.
 617     assert (succ_lev=getjlev succ).
 618       reflexivity.
 619
 620     destruct succ_lev.
 621       apply nd_rule.
 622       apply RArrange.
 623       induction r; simpl.
 624         apply RCanL.
 625         apply RCanR.
 626         apply RuCanL.
 627         apply RuCanR.
 628         apply RAssoc.
 629         apply RCossa.
 630         apply RExch.
 631         apply RWeak.
 632         apply RCont.
 633         apply RLeft; auto.
 634         apply RRight; auto.
 635         eapply RComp; [ apply IHr1 | apply IHr2 ].
 636
 637       apply flatten_arrangement.
 638         apply r.
 639         Defined.
 640
 641   Definition ga_join Γ Δ Σ₁ Σ₂ a b ec :
 642     ND Rule [] [Γ > Δ > Σ₁     |- [@ga_mk _ ec [] a      @@ nil]] ->
 643     ND Rule [] [Γ > Δ > Σ₂     |- [@ga_mk _ ec [] b      @@ nil]] ->
 644     ND Rule [] [Γ > Δ > Σ₁,,Σ₂ |- [@ga_mk _ ec [] (a,,b) @@ nil]].
 645     intro pfa.
 646     intro pfb.
 647     apply secondify with (c:=a)  in pfb.
 648     eapply nd_comp.
 649     Focus 2.
 650     eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
 651     eapply nd_comp; [ eapply nd_llecnac | idtac ].
 652     eapply nd_prod.
 653     apply pfb.
 654     clear pfb.
 655     apply postcompose'.
 656     eapply nd_comp.
 657     apply pfa.
 658     clear pfa.
 659     apply boost.
 660     eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanL ].
 661     apply precompose'.
 662     apply ga_uncancelr.
 663     apply nd_id.
 664     Defined.
 665
 666   Definition arrange_brak : forall Γ Δ ec succ t,
 667    ND Rule
 668      [Γ > Δ > mapOptionTree (flatten_leveled_type ) (drop_lev (ec :: nil) succ),,
 669       [(@ga_mk _ (v2t ec) [] (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: nil) succ))) @@  nil] |- [t @@ nil]]
 670      [Γ > Δ > mapOptionTree (flatten_leveled_type ) succ |- [t @@  nil]].
 671     intros.
 672     unfold drop_lev.
 673     set (@arrange' _ succ (levelMatch (ec::nil))) as q.
 674     set (arrangeMap _ _ flatten_leveled_type q) as y.
 675     eapply nd_comp.
 676     Focus 2.
 677     eapply nd_rule.
 678     eapply RArrange.
 679     apply y.
 680     idtac.
 681     clear y q.
 682     simpl.
 683     eapply nd_comp; [ apply nd_llecnac | idtac ].
 684     eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
 685     apply nd_prod.
 686     Focus 2.
 687     apply nd_id.
 688     idtac.
 689     induction succ; try destruct a; simpl.
 690     unfold take_lev.
 691     unfold mkTakeFlags.
 692     unfold mkFlags.
 693     unfold bnot.
 694     simpl.
 695     destruct l as [t' lev'].
 696     destruct lev' as [|ec' lev'].
 697     simpl.
 698     apply ga_id.
 699     unfold levelMatch.
 700     set (@eqd_dec (HaskLevel Γ) (haskLevelEqDecidable Γ) (ec' :: lev') (ec :: nil)) as q.
 701     destruct q.
 702     inversion e; subst.
 703     simpl.
 704     apply nd_rule.
 705     unfold flatten_leveled_type.
 706     simpl.
 707     unfold flatten_type.
 708     simpl.
 709     unfold ga_mk.
 710     simpl.
 711     apply RVar.
 712     simpl.
 713     apply ga_id.
 714     apply ga_id.
 715     unfold take_lev.
 716     simpl.
 717     apply ga_join.
 718       apply IHsucc1.
 719       apply IHsucc2.
 720     Defined.
 721
 722   Definition arrange_esc : forall Γ Δ ec succ t,
 723    ND Rule
 724      [Γ > Δ > mapOptionTree (flatten_leveled_type ) succ |- [t @@  nil]]
 725      [Γ > Δ > mapOptionTree (flatten_leveled_type ) (drop_lev (ec :: nil) succ),,
 726       [(@ga_mk _ (v2t ec) [] (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: nil) succ))) @@  nil] |- [t @@  nil]].
 727     intros.
 728     unfold drop_lev.
 729     set (@arrange _ succ (levelMatch (ec::nil))) as q.
 730     set (arrangeMap _ _ flatten_leveled_type q) as y.
 731     eapply nd_comp.
 732     eapply nd_rule.
 733     eapply RArrange.
 734     apply y.
 735     idtac.
 736     clear y q.
 737
 738     induction succ.
 739     destruct a.
 740       destruct l.
 741       simpl.
 742       unfold mkDropFlags; simpl.
 743       unfold take_lev.
 744       unfold mkTakeFlags.
 745       simpl.
 746       destruct (General.list_eq_dec h0 (ec :: nil)).
 747         simpl.
 748         rewrite e.
 749         apply nd_id.
 750         simpl.
 751         apply nd_rule.
 752         apply RArrange.
 753         apply RLeft.
 754         apply RWeak.
 755       simpl.
 756         apply nd_rule.
 757         unfold take_lev.
 758         simpl.
 759         apply RArrange.
 760         apply RLeft.
 761         apply RWeak.
 762       apply (Prelude_error "escapifying code with multi-leaf antecedents is not supported").
 763       Defined.
 764
 765   Lemma mapOptionTree_distributes
 766     : forall T R (a b:Tree ??T) (f:T->R),
 767       mapOptionTree f (a,,b) = (mapOptionTree f a),,(mapOptionTree f b).
 768     reflexivity.
 769     Qed.
 770
 771   Definition decide_tree_empty : forall {T:Type}(t:Tree ??T),
 772     sum { q:Tree unit & t = mapTree (fun _ => None) q } unit.
 773     intro T.
 774     refine (fix foo t :=
 775       match t with
 776         | T_Leaf x => _
 777         | T_Branch b1 b2 => let b1' := foo b1 in let b2' := foo b2 in _
 778       end).
 779     intros.
 780     destruct x.
 781     right; apply tt.
 782     left.
 783       exists (T_Leaf tt).
 784       auto.
 785     destruct b1'.
 786     destruct b2'.
 787     destruct s.
 788     destruct s0.
 789     subst.
 790     left.
 791     exists (x,,x0).
 792     reflexivity.
 793     right; auto.
 794     right; auto.
 795     Defined.
 796
 797   Lemma unlev_relev : forall {Γ}(t:Tree ??(HaskType Γ ★)) lev, mapOptionTree unlev (t @@@ lev) = t.
 798     intros.
 799     induction t.
 800     destruct a; reflexivity.
 801     rewrite <- IHt1 at 2.
 802     rewrite <- IHt2 at 2.
 803     reflexivity.
 804     Qed.
 805
 806   Lemma tree_of_nothing : forall Γ ec t a,
 807     Arrange (a,,mapOptionTree flatten_leveled_type (drop_lev(Γ:=Γ) (ec :: nil) (t @@@ (ec :: nil)))) a.
 808     intros.
 809     induction t; try destruct o; try destruct a0.
 810     simpl.
 811     drop_simplify.
 812     simpl.
 813     apply RCanR.
 814     simpl.
 815     apply RCanR.
 816     Opaque drop_lev.
 817     simpl.
 818     Transparent drop_lev.
 819     drop_simplify.
 820     simpl.
 821     eapply RComp.
 822     eapply RComp.
 823     eapply RAssoc.
 824     eapply RRight.
 825     apply IHt1.
 826     apply IHt2.
 827     Defined.
 828
 829   Lemma tree_of_nothing' : forall Γ ec t a,
 830     Arrange a (a,,mapOptionTree flatten_leveled_type (drop_lev(Γ:=Γ) (ec :: nil) (t @@@ (ec :: nil)))).
 831     intros.
 832     induction t; try destruct o; try destruct a0.
 833     simpl.
 834     drop_simplify.
 835     simpl.
 836     apply RuCanR.
 837     simpl.
 838     apply RuCanR.
 839     Opaque drop_lev.
 840     simpl.
 841     Transparent drop_lev.
 842     drop_simplify.
 843     simpl.
 844     eapply RComp.
 845     Focus 2.
 846     eapply RComp.
 847     Focus 2.
 848     eapply RCossa.
 849     Focus 2.
 850     eapply RRight.
 851     apply IHt1.
 852     apply IHt2.
 853     Defined.
 854
 855   Lemma krunk : forall Γ (ec:HaskTyVar Γ ECKind) t,
 856     flatten_type (<[ ec |- t ]>)
 857     = @ga_mk Γ (v2t ec)
 858     (mapOptionTree flatten_type (take_arg_types_as_tree t))
 859     [ flatten_type (drop_arg_types_as_tree   t)].
 860
 861     intros.
 862     unfold flatten_type at 1.
 863     simpl.
 864     unfold ga_mk.
 865     unfold v2t.
 866     admit. (* BIG HUGE CHEAT FIXME *)
 867     Qed.
 868
 869   Definition flatten_proof :
 870     forall  {h}{c},
 871       ND SRule h c ->
 872       ND  Rule (mapOptionTree (flatten_judgment ) h) (mapOptionTree (flatten_judgment ) c).
 873     intros.
 874     eapply nd_map'; [ idtac | apply X ].
 875     clear h c X.
 876     intros.
 877     simpl in *.
 878
 879     refine
 880       (match X as R in SRule H C with
 881       | SBrak    Γ Δ t ec succ lev           => let case_SBrak := tt         in _
 882       | SEsc     Γ Δ t ec succ lev           => let case_SEsc := tt          in _
 883       | SFlat    h c r                       => let case_SFlat := tt         in _
 884       end).
 885
 886     destruct case_SFlat.
 887     refine (match r as R in Rule H C with
 888       | RArrange Γ Δ a b x d           => let case_RArrange := tt      in _
 889       | RNote    Γ Δ Σ τ l n           => let case_RNote := tt         in _
 890       | RLit     Γ Δ l     _           => let case_RLit := tt          in _
 891       | RVar     Γ Δ σ           lev   => let case_RVar := tt          in _
 892       | RGlobal  Γ Δ σ l wev           => let case_RGlobal := tt       in _
 893       | RLam     Γ Δ Σ tx te     lev   => let case_RLam := tt          in _
 894       | RCast    Γ Δ Σ σ τ lev γ       => let case_RCast := tt         in _
 895       | RAbsT    Γ Δ Σ κ σ lev         => let case_RAbsT := tt         in _
 896       | RAppT    Γ Δ Σ κ σ τ     lev   => let case_RAppT := tt         in _
 897       | RAppCo   Γ Δ Σ κ σ₁ σ₂ γ σ lev => let case_RAppCo := tt        in _
 898       | RAbsCo   Γ Δ Σ κ σ  σ₁ σ₂  lev => let case_RAbsCo := tt        in _
 899       | RApp     Γ Δ Σ₁ Σ₂ tx te lev   => let case_RApp := tt          in _
 900       | RLet     Γ Δ Σ₁ Σ₂ σ₁ σ₂ lev   => let case_RLet := tt          in _
 901       | RJoin    Γ p lri m x q         => let case_RJoin := tt in _
 902       | RVoid    _ _                   => let case_RVoid := tt   in _
 903       | RBrak    Γ Δ t ec succ lev           => let case_RBrak := tt         in _
 904       | REsc     Γ Δ t ec succ lev           => let case_REsc := tt          in _
 905       | RCase    Γ Δ lev tc Σ avars tbranches alts => let case_RCase := tt         in _
 906       | RLetRec  Γ Δ lri x y t         => let case_RLetRec := tt       in _
 907       end); clear X h c.
 908
 909     destruct case_RArrange.
 910       apply (flatten_arrangement''  Γ Δ a b x d).
 911
 912     destruct case_RBrak.
 913       apply (Prelude_error "found unskolemized Brak rule; this shouldn't happen").
 914
 915     destruct case_REsc.
 916       apply (Prelude_error "found unskolemized Esc rule; this shouldn't happen").
 917
 918     destruct case_RNote.
 919       simpl.
 920       destruct l; simpl.
 921         apply nd_rule; apply RNote; auto.
 922         apply nd_rule; apply RNote; auto.
 923
 924     destruct case_RLit.
 925       simpl.
 926       destruct l0; simpl.
 927         unfold flatten_leveled_type.
 928         simpl.
 929         rewrite literal_types_unchanged.
 930           apply nd_rule; apply RLit.
 931         unfold take_lev; simpl.
 932         unfold drop_lev; simpl.
 933         simpl.
 934         rewrite literal_types_unchanged.
 935         apply ga_lit.
 936
 937     destruct case_RVar.
 938       Opaque flatten_judgment.
 939       simpl.
 940       Transparent flatten_judgment.
 941       idtac.
 942       unfold flatten_judgment.
 943       unfold getjlev.
 944       destruct lev.
 945       apply nd_rule. apply RVar.
 946       repeat drop_simplify.
 947       repeat take_simplify.
 948       simpl.
 949       apply ga_id.
 950
 951     destruct case_RGlobal.
 952       simpl.
 953       rename l into g.
 954       rename σ into l.
 955       destruct l as [|ec lev]; simpl.
 956         destruct (eqd_dec (g:CoreVar) (hetmet_flatten:CoreVar)).
 957           set (flatten_type (g wev)) as t.
 958           set (RGlobal _ Δ nil (mkGlobal Γ t hetmet_id)) as q.
 959           simpl in q.
 960           apply nd_rule.
 961           apply q.
 962           apply INil.
 963         destruct (eqd_dec (g:CoreVar) (hetmet_unflatten:CoreVar)).
 964           set (flatten_type (g wev)) as t.
 965           set (RGlobal _ Δ nil (mkGlobal Γ t hetmet_id)) as q.
 966           simpl in q.
 967           apply nd_rule.
 968           apply q.
 969           apply INil.
 970         unfold flatten_leveled_type. simpl.
 971           apply nd_rule; rewrite globals_do_not_have_code_types.
 972           apply RGlobal.
 973       apply (Prelude_error "found RGlobal at depth >0; globals should never appear inside code brackets unless escaped").
 974
 975     destruct case_RLam.
 976       Opaque drop_lev.
 977       Opaque take_lev.
 978       simpl.
 979       destruct lev as [|ec lev]; simpl; [ apply nd_rule; apply RLam; auto | idtac ].
 980       repeat drop_simplify.
 981       repeat take_simplify.
 982       eapply nd_comp.
 983         eapply nd_rule.
 984         eapply RArrange.
 985         simpl.
 986         apply RCanR.
 987       apply boost.
 988       simpl.
 989       apply ga_curry.
 990
 991     destruct case_RCast.
 992       simpl.
 993       destruct lev as [|ec lev]; simpl; [ apply nd_rule; apply RCast; auto | idtac ].
 994       simpl.
 995       apply flatten_coercion; auto.
 996       apply (Prelude_error "RCast at level >0; casting inside of code brackets is currently not supported").
 997
 998     destruct case_RJoin.
 999       simpl.
1000       destruct (getjlev x); destruct (getjlev q);
1001         [ apply nd_rule; apply RJoin | idtac | idtac | idtac ];
1002         apply (Prelude_error "RJoin at depth >0").
1003
1004     destruct case_RApp.
1005       simpl.
1006
1007       destruct lev as [|ec lev]. simpl. apply nd_rule.
1008         unfold flatten_leveled_type at 4.
1009         unfold flatten_leveled_type at 2.
1010         simpl.
1011         replace (flatten_type (tx ---> te))
1012           with (flatten_type tx ---> flatten_type te).
1013         apply RApp.
1014         reflexivity.
1015
1016         repeat drop_simplify.
1017           repeat take_simplify.
1018           rewrite mapOptionTree_distributes.
1019           set (mapOptionTree (flatten_leveled_type ) (drop_lev (ec :: lev) Σ₁)) as Σ₁'.
1020           set (mapOptionTree (flatten_leveled_type ) (drop_lev (ec :: lev) Σ₂)) as Σ₂'.
1021           set (take_lev (ec :: lev) Σ₁) as Σ₁''.
1022           set (take_lev (ec :: lev) Σ₂) as Σ₂''.
1023           replace (flatten_type  (tx ---> te)) with ((flatten_type  tx) ---> (flatten_type  te)).
1024           apply (Prelude_error "FIXME: ga_apply").
1025           reflexivity.
1026
1027 (*
1028   Notation "`  x" := (take_lev _ x).
1029   Notation "`` x" := (mapOptionTree unlev x) (at level 20).
1030   Notation "``` x" := ((drop_lev _ x)) (at level 20).
1031   Notation "!<[]> x" := (flatten_type _ x) (at level 1).
1032   Notation "!<[@]> x" := (mapOptionTree flatten_leveled_type x) (at level 1).
1033 *)
1034
1035     destruct case_RLet.
1036       simpl.
1037       destruct lev as [|ec lev]; simpl; [ apply nd_rule; apply RLet; auto | idtac ].
1038       repeat drop_simplify.
1039       repeat take_simplify.
1040       simpl.
1041
1042       eapply nd_comp.
1043       eapply nd_prod; [ idtac | apply nd_id ].
1044       eapply boost.
1045       apply ga_second.
1046
1047       eapply nd_comp.
1048       eapply nd_prod.
1049       apply nd_id.
1050       eapply nd_comp.
1051       eapply nd_rule.
1052       eapply RArrange.
1053       apply RCanR.
1054       eapply precompose.
1055
1056       apply nd_rule.
1057       apply RLet.
1058
1059     destruct case_RVoid.
1060       simpl.
1061       apply nd_rule.
1062       apply RVoid.
1063
1064     destruct case_RAppT.
1065       simpl. destruct lev; simpl.
1066       unfold flatten_leveled_type.
1067       simpl.
1068       rewrite flatten_commutes_with_HaskTAll.
1069       rewrite flatten_commutes_with_substT.
1070       apply nd_rule.
1071       apply RAppT.
1072       apply Δ.
1073       apply Δ.
1074       apply (Prelude_error "found type application at level >0; this is not supported").
1075
1076     destruct case_RAbsT.
1077       simpl. destruct lev; simpl.
1078       unfold flatten_leveled_type at 4.
1079       unfold flatten_leveled_type at 2.
1080       simpl.
1081       rewrite flatten_commutes_with_HaskTAll.
1082       rewrite flatten_commutes_with_HaskTApp.
1083       eapply nd_comp; [ idtac | eapply nd_rule; eapply RAbsT ].
1084       simpl.
1085       set (mapOptionTree (flatten_leveled_type ) (mapOptionTree (weakLT(κ:=κ)) Σ)) as a.
1086       set (mapOptionTree (weakLT(κ:=κ)) (mapOptionTree (flatten_leveled_type ) Σ)) as q'.
1087       assert (a=q').
1088         unfold a.
1089         unfold q'.
1090         clear a q'.
1091         induction Σ.
1092           destruct a.
1093           simpl.
1094           rewrite flatten_commutes_with_weakLT.
1095           reflexivity.
1096           reflexivity.
1097           simpl.
1098           rewrite <- IHΣ1.
1099           rewrite <- IHΣ2.
1100           reflexivity.
1101       rewrite H.
1102       apply nd_id.
1103       apply Δ.
1104       apply Δ.
1105       apply (Prelude_error "found type abstraction at level >0; this is not supported").
1106
1107     destruct case_RAppCo.
1108       simpl. destruct lev; simpl.
1109       unfold flatten_leveled_type at 4.
1110       unfold flatten_leveled_type at 2.
1111       unfold flatten_type.
1112       simpl.
1113       apply nd_rule.
1114       apply RAppCo.
1115       apply flatten_coercion.
1116       apply γ.
1117       apply (Prelude_error "found coercion application at level >0; this is not supported").
1118
1119     destruct case_RAbsCo.
1120       simpl. destruct lev; simpl.
1121       unfold flatten_type.
1122       simpl.
1123       apply (Prelude_error "AbsCo not supported (FIXME)").
1124       apply (Prelude_error "found coercion abstraction at level >0; this is not supported").
1125
1126     destruct case_RLetRec.
1127       rename t into lev.
1128       simpl.
1129       apply (Prelude_error "LetRec not supported (FIXME)").
1130
1131     destruct case_RCase.
1132       simpl.
1133       apply (Prelude_error "Case not supported (BIG FIXME)").
1134
1135     destruct case_SBrak.
1136       simpl.
1137       destruct lev.
1138       drop_simplify.
1139       set (drop_lev (ec :: nil) (take_arg_types_as_tree t @@@ (ec :: nil))) as empty_tree.
1140       take_simplify.
1141       rewrite take_lemma'.
1142       simpl.
1143       rewrite mapOptionTree_compose.
1144       rewrite mapOptionTree_compose.
1145       rewrite unlev_relev.
1146       rewrite <- mapOptionTree_compose.
1147       unfold flatten_leveled_type at 4.
1148       simpl.
1149       rewrite krunk.
1150       set (mapOptionTree flatten_leveled_type (drop_lev (ec :: nil) succ)) as succ_host.
1151       set (mapOptionTree (flatten_type ○ unlev)(take_lev (ec :: nil) succ)) as succ_guest.
1152       set (mapOptionTree flatten_type (take_arg_types_as_tree t)) as succ_args.
1153       unfold empty_tree.
1154       eapply nd_comp; [ eapply nd_rule; eapply RArrange; apply tree_of_nothing | idtac ].
1155       refine (ga_unkappa' Γ Δ (v2t ec) nil _ _ _ _ ;; _).
1156       unfold succ_host.
1157       unfold succ_guest.
1158       apply arrange_brak.
1159       apply (Prelude_error "found Brak at depth >0 indicating 3-level code; only two-level code is currently supported").
1160
1161     destruct case_SEsc.
1162       simpl.
1163       destruct lev.
1164       simpl.
1165       unfold flatten_leveled_type at 2.
1166       simpl.
1167       rewrite krunk.
1168       rewrite mapOptionTree_compose.
1169       take_simplify.
1170       drop_simplify.
1171       simpl.
1172       eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply tree_of_nothing' ].
1173       simpl.
1174       rewrite take_lemma'.
1175       rewrite unlev_relev.
1176       rewrite <- mapOptionTree_compose.
1177       eapply nd_comp; [ apply (arrange_esc _ _ ec) | idtac ].
1178
1179       set (decide_tree_empty (take_lev (ec :: nil) succ)) as q'.
1180       destruct q'.
1181       destruct s.
1182       rewrite e.
1183       clear e.
1184
1185       set (mapOptionTree flatten_leveled_type (drop_lev (ec :: nil) succ)) as succ_host.
1186       set (mapOptionTree flatten_type (take_arg_types_as_tree t)) as succ_args.
1187
1188       eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RCanR ].
1189       eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
1190       eapply nd_comp; [ apply nd_llecnac | idtac ].
1191       apply nd_prod; [ idtac | eapply boost ].
1192       induction x.
1193         apply ga_id.
1194         eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanR ].
1195         simpl.
1196         apply ga_join.
1197           apply IHx1.
1198           apply IHx2.
1199           simpl.
1200           apply postcompose.
1201
1202       refine ( _ ;; (boost _ _ _ _ _ (postcompose _ _ _ _ _ _ _ _))).
1203       apply ga_cancell.
1204       apply firstify.
1205
1206       induction x.
1207         destruct a; simpl.
1208         apply ga_id.
1209         simpl.
1210         refine ( _ ;; (boost _ _ _ _ _ (postcompose _ _ _ _ _ _ _ _))).
1211         apply ga_cancell.
1212         refine ( _ ;; (boost _ _ _ _ _ (postcompose _ _ _ _ _ _ _ _))).
1213         eapply firstify.
1214         apply IHx1.
1215         apply secondify.
1216         apply IHx2.
1217
1218       (* environment has non-empty leaves *)
1219       apply ga_kappa'.
1220
1221       (* nesting too deep *)
1222       apply (Prelude_error "found Esc at depth >0 indicating 3-level code; only two-level code is currently supported").
1223       Defined.
1224
1225   Definition skolemize_and_flatten_proof :
1226     forall  {h}{c},
1227       ND  Rule h c ->
1228       ND  Rule
1229            (mapOptionTree (flatten_judgment ○ skolemize_judgment) h)
1230            (mapOptionTree (flatten_judgment ○ skolemize_judgment) c).
1231     intros.
1232     rewrite mapOptionTree_compose.
1233     rewrite mapOptionTree_compose.
1234     apply flatten_proof.
1235     apply skolemize_proof.
1236     apply X.
1237     Defined.
1238
1239
1240   (* to do: establish some metric on judgments (max length of level of any succedent type, probably), show how to
1241    * calculate it, and show that the flattening procedure above drives it down by one *)
1242
1243   (*
1244   Instance FlatteningFunctor {Γ}{Δ}{ec} : Functor (JudgmentsL (PCF Γ Δ ec)) (TypesL (SystemFCa Γ Δ)) (obact) :=
1245     { fmor := FlatteningFunctor_fmor }.
1246
1247   Definition ReificationFunctor Γ Δ : Functor (JudgmentsL _ _ (PCF n Γ Δ)) SystemFCa' (mapOptionTree brakifyJudg).
1248     refine {| fmor := ReificationFunctor_fmor Γ Δ |}; unfold hom; unfold ob; simpl ; intros.
1249
1250   Definition PCF_SMME (n:nat)(Γ:TypeEnv)(Δ:CoercionEnv Γ) : ProgrammingLanguageSMME.
1251     refine {| plsmme_pl := PCF n Γ Δ |}.
1252     Defined.
1253
1254   Definition SystemFCa_SMME (n:nat)(Γ:TypeEnv)(Δ:CoercionEnv Γ) : ProgrammingLanguageSMME.
1255     refine {| plsmme_pl := SystemFCa n Γ Δ |}.
1256     Defined.
1257
1258   Definition ReificationFunctorMonoidal n : MonoidalFunctor (JudgmentsN n) (JudgmentsN (S n)) (ReificationFunctor n).
1259     Defined.
1260
1261   (* 5.1.4 *)
1262   Definition PCF_SystemFCa_two_level n Γ Δ : TwoLevelLanguage (PCF_SMME n Γ Δ) (SystemFCa_SMME (S n) Γ Δ).
1263     Defined.
1264   *)
1265   (*  ... and the retraction exists *)
1266
1267 End HaskFlattener.
1268
1269 Implicit Arguments garrow [ ].