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