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