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_empty_tree : forall {T}{A}(q:Tree A)(t:Tree ??T),
 726     t = mapTree (fun _:A => None) q ->
 727     Arrange t [].
 728     intros T A q.
 729     induction q; intros.
 730       simpl in H.
 731       rewrite H.
 732       apply RId.
 733     simpl in *.
 734     destruct t; try destruct o; inversion H.
 735       set (IHq1 _ H1) as x1.
 736       set (IHq2 _ H2) as x2.
 737       eapply RComp.
 738         eapply RRight.
 739         rewrite <- H1.
 740         apply x1.
 741       eapply RComp.
 742         apply RCanL.
 743         rewrite <- H2.
 744         apply x2.
 745       Defined.
 746
 747 (*  Definition unarrange_empty_tree : forall {T}{A}(t:Tree ??T)(q:Tree A),
 748     t = mapTree (fun _:A => None) q ->
 749     Arrange [] t.
 750   Defined.*)
 751
 752   Definition decide_tree_empty : forall {T:Type}(t:Tree ??T),
 753     sum { q:Tree unit & t = mapTree (fun _ => None) q } unit.
 754     intro T.
 755     refine (fix foo t :=
 756       match t with
 757         | T_Leaf x => _
 758         | T_Branch b1 b2 => let b1' := foo b1 in let b2' := foo b2 in _
 759       end).
 760     intros.
 761     destruct x.
 762     right; apply tt.
 763     left.
 764       exists (T_Leaf tt).
 765       auto.
 766     destruct b1'.
 767     destruct b2'.
 768     destruct s.
 769     destruct s0.
 770     subst.
 771     left.
 772     exists (x,,x0).
 773     reflexivity.
 774     right; auto.
 775     right; auto.
 776     Defined.
 777
 778   Definition arrange_esc : forall Γ Δ ec succ t,
 779    ND Rule
 780      [Γ > Δ > mapOptionTree (flatten_leveled_type ) succ |- [t @@  nil]]
 781      [Γ > Δ > mapOptionTree (flatten_leveled_type ) (drop_lev (ec :: nil) succ),,
 782       [(@ga_mk _ (v2t ec) [] (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: nil) succ))) @@  nil] |- [t @@  nil]].
 783     intros.
 784     set (@arrange _ succ (levelMatch (ec::nil))) as q.
 785     set (@drop_lev Γ (ec::nil) succ) as q'.
 786     assert (@drop_lev Γ (ec::nil) succ=q') as H.
 787       reflexivity.
 788     unfold drop_lev in H.
 789     unfold mkDropFlags in H.
 790     rewrite H in q.
 791     clear H.
 792     set (arrangeMap _ _ flatten_leveled_type q) as y.
 793     eapply nd_comp.
 794     eapply nd_rule.
 795     eapply RArrange.
 796     apply y.
 797     clear y q.
 798
 799     set (mapOptionTree flatten_leveled_type (dropT (mkFlags (liftBoolFunc false (bnot ○ levelMatch (ec :: nil))) succ))) as q.
 800     destruct (decide_tree_empty q); [ idtac | apply (Prelude_error "escapifying open code not yet supported") ].
 801     destruct s.
 802
 803     simpl.
 804     eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RExch ].
 805     set (fun z z' => @RLet Γ Δ z (mapOptionTree flatten_leveled_type q') t z' nil) as q''.
 806     eapply nd_comp; [ idtac | eapply nd_rule; apply q'' ].
 807     clear q''.
 808     eapply nd_comp; [ apply nd_rlecnac | idtac ].
 809     apply nd_prod.
 810     apply nd_rule.
 811     apply RArrange.
 812     eapply RComp; [ idtac | apply RCanR ].
 813     apply RLeft.
 814     apply (@arrange_empty_tree _ _ _ _ e).
 815
 816     eapply nd_comp.
 817       eapply nd_rule.
 818       eapply (@RVar Γ Δ t nil).
 819     apply nd_rule.
 820       apply RArrange.
 821       eapply RComp.
 822       apply RuCanL.
 823       apply RRight.
 824       apply RWeak.
 825 (*
 826     eapply decide_tree_empty.
 827
 828     simpl.
 829     set (dropT (mkFlags (liftBoolFunc false (bnot ○ levelMatch (ec :: nil))) succ)) as escapified.
 830     destruct (decide_tree_empty escapified).
 831
 832     induction succ.
 833     destruct a.
 834       unfold drop_lev.
 835       destruct l.
 836       simpl.
 837       unfold mkDropFlags; simpl.
 838       unfold take_lev.
 839       unfold mkTakeFlags.
 840       simpl.
 841       destruct (General.list_eq_dec h0 (ec :: nil)).
 842         simpl.
 843         rewrite e.
 844         apply nd_id.
 845         simpl.
 846         apply nd_rule.
 847         apply RArrange.
 848         apply RLeft.
 849         apply RWeak.
 850       simpl.
 851         apply nd_rule.
 852         unfold take_lev.
 853         simpl.
 854         apply RArrange.
 855         apply RLeft.
 856         apply RWeak.
 857       apply (Prelude_error "escapifying code with multi-leaf antecedents is not supported").
 858 *)
 859       Defined.
 860
 861   Lemma mapOptionTree_distributes
 862     : forall T R (a b:Tree ??T) (f:T->R),
 863       mapOptionTree f (a,,b) = (mapOptionTree f a),,(mapOptionTree f b).
 864     reflexivity.
 865     Qed.
 866
 867   Lemma unlev_relev : forall {Γ}(t:Tree ??(HaskType Γ ★)) lev, mapOptionTree unlev (t @@@ lev) = t.
 868     intros.
 869     induction t.
 870     destruct a; reflexivity.
 871     rewrite <- IHt1 at 2.
 872     rewrite <- IHt2 at 2.
 873     reflexivity.
 874     Qed.
 875
 876   Lemma tree_of_nothing : forall Γ ec t a,
 877     Arrange (a,,mapOptionTree flatten_leveled_type (drop_lev(Γ:=Γ) (ec :: nil) (t @@@ (ec :: nil)))) a.
 878     intros.
 879     induction t; try destruct o; try destruct a0.
 880     simpl.
 881     drop_simplify.
 882     simpl.
 883     apply RCanR.
 884     simpl.
 885     apply RCanR.
 886     Opaque drop_lev.
 887     simpl.
 888     Transparent drop_lev.
 889     drop_simplify.
 890     simpl.
 891     eapply RComp.
 892     eapply RComp.
 893     eapply RAssoc.
 894     eapply RRight.
 895     apply IHt1.
 896     apply IHt2.
 897     Defined.
 898
 899   Lemma tree_of_nothing' : forall Γ ec t a,
 900     Arrange a (a,,mapOptionTree flatten_leveled_type (drop_lev(Γ:=Γ) (ec :: nil) (t @@@ (ec :: nil)))).
 901     intros.
 902     induction t; try destruct o; try destruct a0.
 903     simpl.
 904     drop_simplify.
 905     simpl.
 906     apply RuCanR.
 907     simpl.
 908     apply RuCanR.
 909     Opaque drop_lev.
 910     simpl.
 911     Transparent drop_lev.
 912     drop_simplify.
 913     simpl.
 914     eapply RComp.
 915     Focus 2.
 916     eapply RComp.
 917     Focus 2.
 918     eapply RCossa.
 919     Focus 2.
 920     eapply RRight.
 921     apply IHt1.
 922     apply IHt2.
 923     Defined.
 924
 925   Lemma krunk : forall Γ (ec:HaskTyVar Γ ECKind) t,
 926     flatten_type (<[ ec |- t ]>)
 927     = @ga_mk Γ (v2t ec)
 928     (mapOptionTree flatten_type (take_arg_types_as_tree t))
 929     [ flatten_type (drop_arg_types_as_tree   t)].
 930     intros.
 931     unfold flatten_type at 1.
 932     simpl.
 933     unfold ga_mk.
 934     apply phoas_extensionality.
 935     intros.
 936     unfold v2t.
 937     unfold ga_mk_raw.
 938     unfold ga_mk_tree.
 939     rewrite <- mapOptionTree_compose.
 940     unfold take_arg_types_as_tree.
 941     simpl.
 942     replace (flatten_type (drop_arg_types_as_tree t) tv ite)
 943       with (drop_arg_types (flatten_rawtype (t tv ite))).
 944     replace (unleaves_ (take_arg_types (flatten_rawtype (t tv ite))))
 945       with ((mapOptionTree (fun x : HaskType Γ ★ => flatten_type x tv ite)
 946            (unleaves_
 947               (take_trustme (count_arg_types (t (fun _ : Kind => unit) (ite_unit Γ)))
 948                  (fun TV : Kind → Type => take_arg_types ○ t TV))))).
 949     reflexivity.
 950     unfold flatten_type.
 951     clear hetmet_flatten.
 952     clear hetmet_unflatten.
 953     clear hetmet_id.
 954     clear gar.
 955     set (t tv ite) as x.
 956     admit.
 957     admit.
 958     Qed.
 959
 960   Definition flatten_proof :
 961     forall  {h}{c},
 962       ND SRule h c ->
 963       ND  Rule (mapOptionTree (flatten_judgment ) h) (mapOptionTree (flatten_judgment ) c).
 964     intros.
 965     eapply nd_map'; [ idtac | apply X ].
 966     clear h c X.
 967     intros.
 968     simpl in *.
 969
 970     refine
 971       (match X as R in SRule H C with
 972       | SBrak    Γ Δ t ec succ lev           => let case_SBrak := tt         in _
 973       | SEsc     Γ Δ t ec succ lev           => let case_SEsc := tt          in _
 974       | SFlat    h c r                       => let case_SFlat := tt         in _
 975       end).
 976
 977     destruct case_SFlat.
 978     refine (match r as R in Rule H C with
 979       | RArrange Γ Δ a b x d           => let case_RArrange := tt      in _
 980       | RNote    Γ Δ Σ τ l n           => let case_RNote := tt         in _
 981       | RLit     Γ Δ l     _           => let case_RLit := tt          in _
 982       | RVar     Γ Δ σ           lev   => let case_RVar := tt          in _
 983       | RGlobal  Γ Δ σ l wev           => let case_RGlobal := tt       in _
 984       | RLam     Γ Δ Σ tx te     lev   => let case_RLam := tt          in _
 985       | RCast    Γ Δ Σ σ τ lev γ       => let case_RCast := tt         in _
 986       | RAbsT    Γ Δ Σ κ σ lev         => let case_RAbsT := tt         in _
 987       | RAppT    Γ Δ Σ κ σ τ     lev   => let case_RAppT := tt         in _
 988       | RAppCo   Γ Δ Σ κ σ₁ σ₂ γ σ lev => let case_RAppCo := tt        in _
 989       | RAbsCo   Γ Δ Σ κ σ  σ₁ σ₂  lev => let case_RAbsCo := tt        in _
 990       | RApp     Γ Δ Σ₁ Σ₂ tx te lev   => let case_RApp := tt          in _
 991       | RLet     Γ Δ Σ₁ Σ₂ σ₁ σ₂ lev   => let case_RLet := tt          in _
 992       | RJoin    Γ p lri m x q         => let case_RJoin := tt in _
 993       | RVoid    _ _                   => let case_RVoid := tt   in _
 994       | RBrak    Γ Δ t ec succ lev           => let case_RBrak := tt         in _
 995       | REsc     Γ Δ t ec succ lev           => let case_REsc := tt          in _
 996       | RCase    Γ Δ lev tc Σ avars tbranches alts => let case_RCase := tt         in _
 997       | RLetRec  Γ Δ lri x y t         => let case_RLetRec := tt       in _
 998       end); clear X h c.
 999
1000     destruct case_RArrange.
1001       apply (flatten_arrangement''  Γ Δ a b x d).
1002
1003     destruct case_RBrak.
1004       apply (Prelude_error "found unskolemized Brak rule; this shouldn't happen").
1005
1006     destruct case_REsc.
1007       apply (Prelude_error "found unskolemized Esc rule; this shouldn't happen").
1008
1009     destruct case_RNote.
1010       simpl.
1011       destruct l; simpl.
1012         apply nd_rule; apply RNote; auto.
1013         apply nd_rule; apply RNote; auto.
1014
1015     destruct case_RLit.
1016       simpl.
1017       destruct l0; simpl.
1018         unfold flatten_leveled_type.
1019         simpl.
1020         rewrite literal_types_unchanged.
1021           apply nd_rule; apply RLit.
1022         unfold take_lev; simpl.
1023         unfold drop_lev; simpl.
1024         simpl.
1025         rewrite literal_types_unchanged.
1026         apply ga_lit.
1027
1028     destruct case_RVar.
1029       Opaque flatten_judgment.
1030       simpl.
1031       Transparent flatten_judgment.
1032       idtac.
1033       unfold flatten_judgment.
1034       unfold getjlev.
1035       destruct lev.
1036       apply nd_rule. apply RVar.
1037       repeat drop_simplify.
1038       repeat take_simplify.
1039       simpl.
1040       apply ga_id.
1041
1042     destruct case_RGlobal.
1043       simpl.
1044       rename l into g.
1045       rename σ into l.
1046       destruct l as [|ec lev]; simpl.
1047         destruct (eqd_dec (g:CoreVar) (hetmet_flatten:CoreVar)).
1048           set (flatten_type (g wev)) as t.
1049           set (RGlobal _ Δ nil (mkGlobal Γ t hetmet_id)) as q.
1050           simpl in q.
1051           apply nd_rule.
1052           apply q.
1053           apply INil.
1054         destruct (eqd_dec (g:CoreVar) (hetmet_unflatten:CoreVar)).
1055           set (flatten_type (g wev)) as t.
1056           set (RGlobal _ Δ nil (mkGlobal Γ t hetmet_id)) as q.
1057           simpl in q.
1058           apply nd_rule.
1059           apply q.
1060           apply INil.
1061         unfold flatten_leveled_type. simpl.
1062           apply nd_rule; rewrite globals_do_not_have_code_types.
1063           apply RGlobal.
1064       apply (Prelude_error "found RGlobal at depth >0; globals should never appear inside code brackets unless escaped").
1065
1066     destruct case_RLam.
1067       Opaque drop_lev.
1068       Opaque take_lev.
1069       simpl.
1070       destruct lev as [|ec lev]; simpl; [ apply nd_rule; apply RLam; auto | idtac ].
1071       repeat drop_simplify.
1072       repeat take_simplify.
1073       eapply nd_comp.
1074         eapply nd_rule.
1075         eapply RArrange.
1076         simpl.
1077         apply RCanR.
1078       apply boost.
1079       simpl.
1080       apply ga_curry.
1081
1082     destruct case_RCast.
1083       simpl.
1084       destruct lev as [|ec lev]; simpl; [ apply nd_rule; apply RCast; auto | idtac ].
1085       simpl.
1086       apply flatten_coercion; auto.
1087       apply (Prelude_error "RCast at level >0; casting inside of code brackets is currently not supported").
1088
1089     destruct case_RJoin.
1090       simpl.
1091       destruct (getjlev x); destruct (getjlev q);
1092         [ apply nd_rule; apply RJoin | idtac | idtac | idtac ];
1093         apply (Prelude_error "RJoin at depth >0").
1094
1095     destruct case_RApp.
1096       simpl.
1097
1098       destruct lev as [|ec lev]. simpl. apply nd_rule.
1099         unfold flatten_leveled_type at 4.
1100         unfold flatten_leveled_type at 2.
1101         simpl.
1102         replace (flatten_type (tx ---> te))
1103           with (flatten_type tx ---> flatten_type te).
1104         apply RApp.
1105         reflexivity.
1106
1107         repeat drop_simplify.
1108           repeat take_simplify.
1109           rewrite mapOptionTree_distributes.
1110           set (mapOptionTree (flatten_leveled_type ) (drop_lev (ec :: lev) Σ₁)) as Σ₁'.
1111           set (mapOptionTree (flatten_leveled_type ) (drop_lev (ec :: lev) Σ₂)) as Σ₂'.
1112           set (take_lev (ec :: lev) Σ₁) as Σ₁''.
1113           set (take_lev (ec :: lev) Σ₂) as Σ₂''.
1114           replace (flatten_type  (tx ---> te)) with ((flatten_type  tx) ---> (flatten_type  te)).
1115           apply (Prelude_error "FIXME: ga_apply").
1116           reflexivity.
1117
1118 (*
1119   Notation "`  x" := (take_lev _ x).
1120   Notation "`` x" := (mapOptionTree unlev x) (at level 20).
1121   Notation "``` x" := ((drop_lev _ x)) (at level 20).
1122   Notation "!<[]> x" := (flatten_type _ x) (at level 1).
1123   Notation "!<[@]> x" := (mapOptionTree flatten_leveled_type x) (at level 1).
1124 *)
1125
1126     destruct case_RLet.
1127       simpl.
1128       destruct lev as [|ec lev]; simpl; [ apply nd_rule; apply RLet; auto | idtac ].
1129       repeat drop_simplify.
1130       repeat take_simplify.
1131       simpl.
1132
1133       eapply nd_comp.
1134       eapply nd_prod; [ idtac | apply nd_id ].
1135       eapply boost.
1136       apply ga_second.
1137
1138       eapply nd_comp.
1139       eapply nd_prod.
1140       apply nd_id.
1141       eapply nd_comp.
1142       eapply nd_rule.
1143       eapply RArrange.
1144       apply RCanR.
1145       eapply precompose.
1146
1147       apply nd_rule.
1148       apply RLet.
1149
1150     destruct case_RVoid.
1151       simpl.
1152       apply nd_rule.
1153       apply RVoid.
1154
1155     destruct case_RAppT.
1156       simpl. destruct lev; simpl.
1157       unfold flatten_leveled_type.
1158       simpl.
1159       rewrite flatten_commutes_with_HaskTAll.
1160       rewrite flatten_commutes_with_substT.
1161       apply nd_rule.
1162       apply RAppT.
1163       apply Δ.
1164       apply Δ.
1165       apply (Prelude_error "found type application at level >0; this is not supported").
1166
1167     destruct case_RAbsT.
1168       simpl. destruct lev; simpl.
1169       unfold flatten_leveled_type at 4.
1170       unfold flatten_leveled_type at 2.
1171       simpl.
1172       rewrite flatten_commutes_with_HaskTAll.
1173       rewrite flatten_commutes_with_HaskTApp.
1174       eapply nd_comp; [ idtac | eapply nd_rule; eapply RAbsT ].
1175       simpl.
1176       set (mapOptionTree (flatten_leveled_type ) (mapOptionTree (weakLT(κ:=κ)) Σ)) as a.
1177       set (mapOptionTree (weakLT(κ:=κ)) (mapOptionTree (flatten_leveled_type ) Σ)) as q'.
1178       assert (a=q').
1179         unfold a.
1180         unfold q'.
1181         clear a q'.
1182         induction Σ.
1183           destruct a.
1184           simpl.
1185           rewrite flatten_commutes_with_weakLT.
1186           reflexivity.
1187           reflexivity.
1188           simpl.
1189           rewrite <- IHΣ1.
1190           rewrite <- IHΣ2.
1191           reflexivity.
1192       rewrite H.
1193       apply nd_id.
1194       apply Δ.
1195       apply Δ.
1196       apply (Prelude_error "found type abstraction at level >0; this is not supported").
1197
1198     destruct case_RAppCo.
1199       simpl. destruct lev; simpl.
1200       unfold flatten_leveled_type at 4.
1201       unfold flatten_leveled_type at 2.
1202       unfold flatten_type.
1203       simpl.
1204       apply nd_rule.
1205       apply RAppCo.
1206       apply flatten_coercion.
1207       apply γ.
1208       apply (Prelude_error "found coercion application at level >0; this is not supported").
1209
1210     destruct case_RAbsCo.
1211       simpl. destruct lev; simpl.
1212       unfold flatten_type.
1213       simpl.
1214       apply (Prelude_error "AbsCo not supported (FIXME)").
1215       apply (Prelude_error "found coercion abstraction at level >0; this is not supported").
1216
1217     destruct case_RLetRec.
1218       rename t into lev.
1219       simpl.
1220       apply (Prelude_error "LetRec not supported (FIXME)").
1221
1222     destruct case_RCase.
1223       simpl.
1224       apply (Prelude_error "Case not supported (BIG FIXME)").
1225
1226     destruct case_SBrak.
1227       simpl.
1228       destruct lev.
1229       drop_simplify.
1230       set (drop_lev (ec :: nil) (take_arg_types_as_tree t @@@ (ec :: nil))) as empty_tree.
1231       take_simplify.
1232       rewrite take_lemma'.
1233       simpl.
1234       rewrite mapOptionTree_compose.
1235       rewrite mapOptionTree_compose.
1236       rewrite unlev_relev.
1237       rewrite <- mapOptionTree_compose.
1238       unfold flatten_leveled_type at 4.
1239       simpl.
1240       rewrite krunk.
1241       set (mapOptionTree flatten_leveled_type (drop_lev (ec :: nil) succ)) as succ_host.
1242       set (mapOptionTree (flatten_type ○ unlev)(take_lev (ec :: nil) succ)) as succ_guest.
1243       set (mapOptionTree flatten_type (take_arg_types_as_tree t)) as succ_args.
1244       unfold empty_tree.
1245       eapply nd_comp; [ eapply nd_rule; eapply RArrange; apply tree_of_nothing | idtac ].
1246       refine (ga_unkappa' Γ Δ (v2t ec) nil _ _ _ _ ;; _).
1247       unfold succ_host.
1248       unfold succ_guest.
1249       apply arrange_brak.
1250       apply (Prelude_error "found Brak at depth >0 indicating 3-level code; only two-level code is currently supported").
1251
1252     destruct case_SEsc.
1253       simpl.
1254       destruct lev.
1255       simpl.
1256       unfold flatten_leveled_type at 2.
1257       simpl.
1258       rewrite krunk.
1259       rewrite mapOptionTree_compose.
1260       take_simplify.
1261       drop_simplify.
1262       simpl.
1263       eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply tree_of_nothing' ].
1264       simpl.
1265       rewrite take_lemma'.
1266       rewrite unlev_relev.
1267       rewrite <- mapOptionTree_compose.
1268       eapply nd_comp; [ apply (arrange_esc _ _ ec) | idtac ].
1269
1270       set (decide_tree_empty (take_lev (ec :: nil) succ)) as q'.
1271       destruct q'.
1272       destruct s.
1273       rewrite e.
1274       clear e.
1275
1276       set (mapOptionTree flatten_leveled_type (drop_lev (ec :: nil) succ)) as succ_host.
1277       set (mapOptionTree flatten_type (take_arg_types_as_tree t)) as succ_args.
1278
1279       eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RCanR ].
1280       eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
1281       eapply nd_comp; [ apply nd_llecnac | idtac ].
1282       apply nd_prod; [ idtac | eapply boost ].
1283       induction x.
1284         apply ga_id.
1285         eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanR ].
1286         simpl.
1287         apply ga_join.
1288           apply IHx1.
1289           apply IHx2.
1290           simpl.
1291           apply postcompose.
1292
1293       refine ( _ ;; (boost _ _ _ _ _ (postcompose _ _ _ _ _ _ _ _))).
1294       apply ga_cancell.
1295       apply firstify.
1296
1297       induction x.
1298         destruct a; simpl.
1299         apply ga_id.
1300         simpl.
1301         refine ( _ ;; (boost _ _ _ _ _ (postcompose _ _ _ _ _ _ _ _))).
1302         apply ga_cancell.
1303         refine ( _ ;; (boost _ _ _ _ _ (postcompose _ _ _ _ _ _ _ _))).
1304         eapply firstify.
1305         apply IHx1.
1306         apply secondify.
1307         apply IHx2.
1308
1309       (* environment has non-empty leaves *)
1310       apply ga_kappa'.
1311
1312       (* nesting too deep *)
1313       apply (Prelude_error "found Esc at depth >0 indicating 3-level code; only two-level code is currently supported").
1314       Defined.
1315
1316   Definition skolemize_and_flatten_proof :
1317     forall  {h}{c},
1318       ND  Rule h c ->
1319       ND  Rule
1320            (mapOptionTree (flatten_judgment ○ skolemize_judgment) h)
1321            (mapOptionTree (flatten_judgment ○ skolemize_judgment) c).
1322     intros.
1323     rewrite mapOptionTree_compose.
1324     rewrite mapOptionTree_compose.
1325     apply flatten_proof.
1326     apply skolemize_proof.
1327     apply X.
1328     Defined.
1329
1330
1331   (* to do: establish some metric on judgments (max length of level of any succedent type, probably), show how to
1332    * calculate it, and show that the flattening procedure above drives it down by one *)
1333
1334   (*
1335   Instance FlatteningFunctor {Γ}{Δ}{ec} : Functor (JudgmentsL (PCF Γ Δ ec)) (TypesL (SystemFCa Γ Δ)) (obact) :=
1336     { fmor := FlatteningFunctor_fmor }.
1337
1338   Definition ReificationFunctor Γ Δ : Functor (JudgmentsL _ _ (PCF n Γ Δ)) SystemFCa' (mapOptionTree brakifyJudg).
1339     refine {| fmor := ReificationFunctor_fmor Γ Δ |}; unfold hom; unfold ob; simpl ; intros.
1340
1341   Definition PCF_SMME (n:nat)(Γ:TypeEnv)(Δ:CoercionEnv Γ) : ProgrammingLanguageSMME.
1342     refine {| plsmme_pl := PCF n Γ Δ |}.
1343     Defined.
1344
1345   Definition SystemFCa_SMME (n:nat)(Γ:TypeEnv)(Δ:CoercionEnv Γ) : ProgrammingLanguageSMME.
1346     refine {| plsmme_pl := SystemFCa n Γ Δ |}.
1347     Defined.
1348
1349   Definition ReificationFunctorMonoidal n : MonoidalFunctor (JudgmentsN n) (JudgmentsN (S n)) (ReificationFunctor n).
1350     Defined.
1351
1352   (* 5.1.4 *)
1353   Definition PCF_SystemFCa_two_level n Γ Δ : TwoLevelLanguage (PCF_SMME n Γ Δ) (SystemFCa_SMME (S n) Γ Δ).
1354     Defined.
1355   *)
1356   (*  ... and the retraction exists *)
1357
1358 End HaskFlattener.
1359
1360 Implicit Arguments garrow [ ].