src/HaskFlattener.v

   1 (*********************************************************************************************************************************)
   2 (* HaskFlattener:                                                                                                                *)
   3 (*                                                                                                                               *)
   4 (*    The Flattening Functor.                                                                                                    *)
   5 (*                                                                                                                               *)
   6 (*********************************************************************************************************************************)
   7
   8 Generalizable All Variables.
   9 Require Import Preamble.
  10 Require Import General.
  11 Require Import NaturalDeduction.
  12 Require Import Coq.Strings.String.
  13 Require Import Coq.Lists.List.
  14
  15 Require Import HaskKinds.
  16 Require Import HaskCoreTypes.
  17 Require Import HaskCoreVars.
  18 Require Import HaskWeakTypes.
  19 Require Import HaskWeakVars.
  20 Require Import HaskLiterals.
  21 Require Import HaskTyCons.
  22 Require Import HaskStrongTypes.
  23 Require Import HaskProof.
  24 Require Import NaturalDeduction.
  25
  26 Require Import HaskStrongTypes.
  27 Require Import HaskStrong.
  28 Require Import HaskProof.
  29 Require Import HaskStrongToProof.
  30 Require Import HaskProofToStrong.
  31 Require Import HaskWeakToStrong.
  32
  33 Require Import HaskSkolemizer.
  34
  35 Open Scope nd_scope.
  36 Set Printing Width 130.
  37
  38 (*
  39  *  The flattening transformation.  Currently only TWO-level languages are
  40  *  supported, and the level-1 sublanguage is rather limited.
  41  *
  42  *  This file abuses terminology pretty badly.  For purposes of this file,
  43  *  "PCF" means "the level-1 sublanguage" and "FC" (aka System FC) means
  44  *  the whole language (level-0 language including bracketed level-1 terms)
  45  *)
  46 Section HaskFlattener.
  47
  48   Definition getlev {Γ}{κ}(lht:LeveledHaskType Γ κ) : HaskLevel Γ :=
  49     match lht with t @@ l => l end.
  50
  51   Definition arrange :
  52     forall {T} (Σ:Tree ??T) (f:T -> bool),
  53       Arrange Σ (dropT (mkFlags (liftBoolFunc false f) Σ),,( (dropT (mkFlags (liftBoolFunc false (bnot ○ f)) Σ)))).
  54     intros.
  55     induction Σ.
  56       simpl.
  57       destruct a.
  58       simpl.
  59       destruct (f t); simpl.
  60       apply RuCanL.
  61       apply RuCanR.
  62       simpl.
  63       apply RuCanL.
  64       simpl in *.
  65       eapply RComp; [ idtac | apply arrangeSwapMiddle ].
  66       eapply RComp.
  67       eapply RLeft.
  68       apply IHΣ2.
  69       eapply RRight.
  70       apply IHΣ1.
  71       Defined.
  72
  73   Definition arrange' :
  74     forall {T} (Σ:Tree ??T) (f:T -> bool),
  75       Arrange (dropT (mkFlags (liftBoolFunc false f) Σ),,( (dropT (mkFlags (liftBoolFunc false (bnot ○ f)) Σ)))) Σ.
  76     intros.
  77     induction Σ.
  78       simpl.
  79       destruct a.
  80       simpl.
  81       destruct (f t); simpl.
  82       apply RCanL.
  83       apply RCanR.
  84       simpl.
  85       apply RCanL.
  86       simpl in *.
  87       eapply RComp; [ apply arrangeSwapMiddle | idtac ].
  88       eapply RComp.
  89       eapply RLeft.
  90       apply IHΣ2.
  91       eapply RRight.
  92       apply IHΣ1.
  93       Defined.
  94
  95   Ltac eqd_dec_refl' :=
  96     match goal with
  97       | [ |- context[@eqd_dec ?T ?V ?X ?X] ] =>
  98         destruct (@eqd_dec T V X X) as [eqd_dec1 | eqd_dec2];
  99           [ clear eqd_dec1 | set (eqd_dec2 (refl_equal _)) as eqd_dec2'; inversion eqd_dec2' ]
 100   end.
 101
 102   Definition v2t {Γ}(ec:HaskTyVar Γ ECKind) : HaskType Γ ECKind := fun TV ite => TVar (ec TV ite).
 103
 104   Definition levelMatch {Γ}(lev:HaskLevel Γ) : LeveledHaskType Γ ★ -> bool :=
 105     fun t => match t with ttype@@tlev => if eqd_dec tlev lev then true else false end.
 106
 107   (* In a tree of types, replace any type at depth "lev" or greater None *)
 108   Definition mkDropFlags {Γ}(lev:HaskLevel Γ)(tt:Tree ??(LeveledHaskType Γ ★)) : TreeFlags tt :=
 109     mkFlags (liftBoolFunc false (levelMatch lev)) tt.
 110
 111   Definition drop_lev {Γ}(lev:HaskLevel Γ)(tt:Tree ??(LeveledHaskType Γ ★)) : Tree ??(LeveledHaskType Γ ★) :=
 112     dropT (mkDropFlags lev tt).
 113
 114   (* The opposite: replace any type which is NOT at level "lev" with None *)
 115   Definition mkTakeFlags {Γ}(lev:HaskLevel Γ)(tt:Tree ??(LeveledHaskType Γ ★)) : TreeFlags tt :=
 116     mkFlags (liftBoolFunc true (bnot ○ levelMatch lev)) tt.
 117
 118   Definition take_lev {Γ}(lev:HaskLevel Γ)(tt:Tree ??(LeveledHaskType Γ ★)) : Tree ??(LeveledHaskType Γ ★) :=
 119     dropT (mkTakeFlags lev tt).
 120 (*
 121     mapOptionTree (fun x => flatten_type (unlev x))
 122     (maybeTree (takeT tt (mkFlags (
 123       fun t => match t with
 124                  | Some (ttype @@ tlev) => if eqd_dec tlev lev then true else false
 125                  | _                    => true
 126                end
 127     ) tt))).
 128
 129   Definition maybeTree {T}(t:??(Tree ??T)) : Tree ??T :=
 130     match t with
 131       | None   => []
 132       | Some x => x
 133     end.
 134 *)
 135
 136   Lemma drop_lev_lemma : forall Γ (lev:HaskLevel Γ) x, drop_lev lev [x @@  lev] = [].
 137     intros; simpl.
 138     Opaque eqd_dec.
 139     unfold drop_lev.
 140     simpl.
 141     unfold mkDropFlags.
 142     simpl.
 143     Transparent eqd_dec.
 144     eqd_dec_refl'.
 145     auto.
 146     Qed.
 147
 148   Lemma drop_lev_lemma_s : forall Γ (lev:HaskLevel Γ) ec x, drop_lev (ec::lev) [x @@  (ec :: lev)] = [].
 149     intros; simpl.
 150     Opaque eqd_dec.
 151     unfold drop_lev.
 152     unfold mkDropFlags.
 153     simpl.
 154     Transparent eqd_dec.
 155     eqd_dec_refl'.
 156     auto.
 157     Qed.
 158
 159   Lemma take_lemma : forall Γ (lev:HaskLevel Γ) x, take_lev lev [x @@  lev] = [x @@ lev].
 160     intros; simpl.
 161     Opaque eqd_dec.
 162     unfold take_lev.
 163     unfold mkTakeFlags.
 164     simpl.
 165     Transparent eqd_dec.
 166     eqd_dec_refl'.
 167     auto.
 168     Qed.
 169
 170   Lemma take_lemma' : forall Γ (lev:HaskLevel Γ) x, take_lev lev (x @@@ lev) = x @@@ lev.
 171     intros.
 172     induction x.
 173     destruct a; simpl; try reflexivity.
 174     apply take_lemma.
 175     simpl.
 176     rewrite <- IHx1 at 2.
 177     rewrite <- IHx2 at 2.
 178     reflexivity.
 179     Qed.
 180 (*
 181   Lemma drop_lev_lemma' : forall Γ (lev:HaskLevel Γ) x, drop_lev lev (x @@@ lev) = [].
 182     intros.
 183     induction x.
 184     destruct a; simpl; try reflexivity.
 185     apply drop_lev_lemma.
 186     simpl.
 187     change (@drop_lev _ lev (x1 @@@ lev ,, x2 @@@ lev))
 188       with ((@drop_lev _ lev (x1 @@@ lev)) ,, (@drop_lev _ lev (x2 @@@ lev))).
 189     simpl.
 190     rewrite IHx1.
 191     rewrite IHx2.
 192     reflexivity.
 193     Qed.
 194 *)
 195   Ltac drop_simplify :=
 196     match goal with
 197       | [ |- context[@drop_lev ?G ?L [ ?X @@ ?L ] ] ] =>
 198         rewrite (drop_lev_lemma G L X)
 199 (*
 200       | [ |- context[@drop_lev ?G ?L [ ?X @@@ ?L ] ] ] =>
 201         rewrite (drop_lev_lemma' G L X)
 202 *)
 203       | [ |- context[@drop_lev ?G (?E :: ?L) [ ?X @@ (?E :: ?L) ] ] ] =>
 204         rewrite (drop_lev_lemma_s G L E X)
 205       | [ |- context[@drop_lev ?G ?N (?A,,?B)] ] =>
 206       change (@drop_lev G N (A,,B)) with ((@drop_lev G N A),,(@drop_lev G N B))
 207       | [ |- context[@drop_lev ?G ?N (T_Leaf None)] ] =>
 208       change (@drop_lev G N (T_Leaf (@None (LeveledHaskType G ★)))) with (T_Leaf (@None (LeveledHaskType G ★)))
 209     end.
 210
 211   Ltac take_simplify :=
 212     match goal with
 213       | [ |- context[@take_lev ?G ?L [ ?X @@ ?L ] ] ] =>
 214         rewrite (take_lemma G L X)
 215       | [ |- context[@take_lev ?G ?L [ ?X @@@ ?L ] ] ] =>
 216         rewrite (take_lemma' G L X)
 217       | [ |- context[@take_lev ?G ?N (?A,,?B)] ] =>
 218       change (@take_lev G N (A,,B)) with ((@take_lev G N A),,(@take_lev G N B))
 219       | [ |- context[@take_lev ?G ?N (T_Leaf None)] ] =>
 220       change (@take_lev G N (T_Leaf (@None (LeveledHaskType G ★)))) with (T_Leaf (@None (LeveledHaskType G ★)))
 221     end.
 222
 223
 224   (*******************************************************************************)
 225
 226
 227   Context (hetmet_flatten : WeakExprVar).
 228   Context (hetmet_unflatten : WeakExprVar).
 229   Context (hetmet_id      : WeakExprVar).
 230   Context {unitTy : forall TV, RawHaskType TV ECKind  -> RawHaskType TV ★                                          }.
 231   Context {prodTy : forall TV, RawHaskType TV ECKind  -> RawHaskType TV ★  -> RawHaskType TV ★ -> RawHaskType TV ★ }.
 232   Context {gaTy   : forall TV, RawHaskType TV ECKind  -> RawHaskType TV ★ -> RawHaskType TV ★  -> RawHaskType TV ★ }.
 233
 234   Definition ga_mk_tree' {TV}(ec:RawHaskType TV ECKind)(tr:Tree ??(RawHaskType TV ★)) : RawHaskType TV ★ :=
 235     reduceTree (unitTy TV ec) (prodTy TV ec) tr.
 236
 237   Definition ga_mk_tree {Γ}(ec:HaskType Γ ECKind)(tr:Tree ??(HaskType Γ ★)) : HaskType Γ ★ :=
 238     fun TV ite => ga_mk_tree' (ec TV ite) (mapOptionTree (fun x => x TV ite) tr).
 239
 240   Definition ga_mk_raw {TV}(ec:RawHaskType TV ECKind)(ant suc:Tree ??(RawHaskType TV ★)) : RawHaskType TV ★ :=
 241     gaTy TV ec
 242     (ga_mk_tree' ec ant)
 243     (ga_mk_tree' ec suc).
 244
 245   Definition ga_mk {Γ}(ec:HaskType Γ ECKind)(ant suc:Tree ??(HaskType Γ ★)) : HaskType Γ ★ :=
 246     fun TV ite => gaTy TV (ec TV ite) (ga_mk_tree ec ant TV ite) (ga_mk_tree ec suc TV ite).
 247
 248   (*
 249    *  The story:
 250    *    - code types <[t]>@c                                                become garrows  c () t
 251    *    - free variables of type t at a level lev deeper than the succedent become garrows  c () t
 252    *    - free variables at the level of the succedent become
 253    *)
 254   Fixpoint flatten_rawtype {TV}{κ}(exp: RawHaskType TV κ) : RawHaskType TV κ :=
 255     match exp with
 256     | TVar    _  x          => TVar x
 257     | TAll     _ y          => TAll   _  (fun v => flatten_rawtype (y v))
 258     | TApp   _ _ x y        => TApp      (flatten_rawtype x) (flatten_rawtype y)
 259     | TCon       tc         => TCon      tc
 260     | TCoerc _ t1 t2 t      => TCoerc    (flatten_rawtype t1) (flatten_rawtype t2) (flatten_rawtype t)
 261     | TArrow                => TArrow
 262     | TCode     ec e        => let e' := flatten_rawtype e
 263                                in  ga_mk_raw ec (unleaves (take_arg_types e')) [drop_arg_types e']
 264     | TyFunApp  tfc kl k lt => TyFunApp tfc kl k (flatten_rawtype_list _ lt)
 265     end
 266     with flatten_rawtype_list {TV}(lk:list Kind)(exp:@RawHaskTypeList TV lk) : @RawHaskTypeList TV lk :=
 267     match exp in @RawHaskTypeList _ LK return @RawHaskTypeList TV LK with
 268     | TyFunApp_nil               => TyFunApp_nil
 269     | TyFunApp_cons  κ kl t rest => TyFunApp_cons _ _ (flatten_rawtype t) (flatten_rawtype_list _ rest)
 270     end.
 271
 272   Definition flatten_type {Γ}{κ}(ht:HaskType Γ κ) : HaskType Γ κ :=
 273     fun TV ite => flatten_rawtype (ht TV ite).
 274
 275   Fixpoint levels_to_tcode {Γ}(ht:HaskType Γ ★)(lev:HaskLevel Γ) : HaskType Γ ★ :=
 276     match lev with
 277       | nil      => flatten_type ht
 278       | ec::lev' => @ga_mk _ (v2t ec) [] [levels_to_tcode ht lev']
 279     end.
 280
 281   Definition flatten_leveled_type {Γ}(ht:LeveledHaskType Γ ★) : LeveledHaskType Γ ★ :=
 282     levels_to_tcode (unlev ht) (getlev ht) @@ nil.
 283
 284   (* AXIOMS *)
 285
 286   Axiom literal_types_unchanged : forall Γ l, flatten_type (literalType l) = literalType(Γ:=Γ) l.
 287
 288   Axiom flatten_coercion : forall Γ Δ κ (σ τ:HaskType Γ κ) (γ:HaskCoercion Γ Δ (σ ∼∼∼ τ)),
 289     HaskCoercion Γ Δ (flatten_type σ ∼∼∼ flatten_type τ).
 290
 291   Axiom flatten_commutes_with_substT :
 292     forall  κ Γ (Δ:CoercionEnv Γ) (σ:∀ TV, InstantiatedTypeEnv TV Γ → TV κ → RawHaskType TV ★) (τ:HaskType Γ κ),
 293     flatten_type  (substT σ τ) = substT (fun TV ite v => flatten_rawtype  (σ TV ite v))
 294       (flatten_type  τ).
 295
 296   Axiom flatten_commutes_with_HaskTAll :
 297     forall  κ Γ (Δ:CoercionEnv Γ) (σ:∀ TV, InstantiatedTypeEnv TV Γ → TV κ → RawHaskType TV ★),
 298     flatten_type  (HaskTAll κ σ) = HaskTAll κ (fun TV ite v => flatten_rawtype (σ TV ite v)).
 299
 300   Axiom flatten_commutes_with_HaskTApp :
 301     forall  κ Γ (Δ:CoercionEnv Γ) (σ:∀ TV, InstantiatedTypeEnv TV Γ → TV κ → RawHaskType TV ★),
 302     flatten_type  (HaskTApp (weakF σ) (FreshHaskTyVar κ)) =
 303     HaskTApp (weakF (fun TV ite v => flatten_rawtype  (σ TV ite v))) (FreshHaskTyVar κ).
 304
 305   Axiom flatten_commutes_with_weakLT : forall (Γ:TypeEnv) κ  t,
 306     flatten_leveled_type  (weakLT(Γ:=Γ)(κ:=κ) t) = weakLT(Γ:=Γ)(κ:=κ) (flatten_leveled_type  t).
 307
 308   Axiom globals_do_not_have_code_types : forall (Γ:TypeEnv) (g:Global Γ) v,
 309     flatten_type (g v) = g v.
 310
 311   (* This tries to assign a single level to the entire succedent of a judgment.  If the succedent has types from different
 312    * levels (should not happen) it just picks one; if the succedent has no non-None leaves (also should not happen) it
 313    * picks nil *)
 314   Definition getΓ (j:Judg) := match j with Γ > _ > _ |- _ => Γ end.
 315   Definition getSuc (j:Judg) : Tree ??(LeveledHaskType (getΓ j) ★) :=
 316     match j as J return Tree ??(LeveledHaskType (getΓ J) ★) with Γ > _ > _ |- s => s end.
 317   Fixpoint getjlev {Γ}(tt:Tree ??(LeveledHaskType Γ ★)) : HaskLevel Γ :=
 318     match tt with
 319       | T_Leaf None              => nil
 320       | T_Leaf (Some (_ @@ lev)) => lev
 321       | T_Branch b1 b2 =>
 322         match getjlev b1 with
 323           | nil => getjlev b2
 324           | lev => lev
 325         end
 326     end.
 327
 328   (* "n" is the maximum depth remaining AFTER flattening *)
 329   Definition flatten_judgment (j:Judg) :=
 330     match j as J return Judg with
 331       Γ > Δ > ant |- suc =>
 332         match getjlev suc with
 333           | nil        => Γ > Δ > mapOptionTree flatten_leveled_type ant
 334                                |- mapOptionTree flatten_leveled_type suc
 335
 336           | (ec::lev') => Γ > Δ > mapOptionTree flatten_leveled_type (drop_lev (ec::lev') ant)
 337                                |- [ga_mk (v2t ec)
 338                                          (mapOptionTree (flatten_type ○ unlev) (take_lev (ec::lev') ant))
 339                                          (mapOptionTree (flatten_type ○ unlev)                      suc )
 340                                          @@ nil]  (* we know the level of all of suc *)
 341         end
 342     end.
 343
 344   Class garrow :=
 345   { ga_id        : ∀ Γ Δ ec l a    , ND Rule [] [Γ > Δ >                          [] |- [@ga_mk Γ ec a a @@ l] ]
 346   ; ga_cancelr   : ∀ Γ Δ ec l a    , ND Rule [] [Γ > Δ >                          [] |- [@ga_mk Γ ec (a,,[]) a @@ l] ]
 347   ; ga_cancell   : ∀ Γ Δ ec l a    , ND Rule [] [Γ > Δ >                          [] |- [@ga_mk Γ ec ([],,a) a @@ l] ]
 348   ; ga_uncancelr : ∀ Γ Δ ec l a    , ND Rule [] [Γ > Δ >                          [] |- [@ga_mk Γ ec a (a,,[]) @@ l] ]
 349   ; ga_uncancell : ∀ Γ Δ ec l a    , ND Rule [] [Γ > Δ >                          [] |- [@ga_mk Γ ec a ([],,a) @@ l] ]
 350   ; ga_assoc     : ∀ Γ Δ ec l a b c, ND Rule [] [Γ > Δ >                          [] |- [@ga_mk Γ ec ((a,,b),,c) (a,,(b,,c)) @@ l] ]
 351   ; ga_unassoc   : ∀ Γ Δ ec l a b c, ND Rule [] [Γ > Δ >                          [] |- [@ga_mk Γ ec (a,,(b,,c)) ((a,,b),,c) @@ l] ]
 352   ; ga_swap      : ∀ Γ Δ ec l a b  , ND Rule [] [Γ > Δ >                          [] |- [@ga_mk Γ ec (a,,b) (b,,a) @@ l] ]
 353   ; ga_drop      : ∀ Γ Δ ec l a    , ND Rule [] [Γ > Δ >                          [] |- [@ga_mk Γ ec a [] @@ l] ]
 354   ; ga_copy      : ∀ Γ Δ ec l a    , ND Rule [] [Γ > Δ >                          [] |- [@ga_mk Γ ec a (a,,a) @@ l] ]
 355   ; ga_first     : ∀ Γ Δ ec l a b x, ND Rule [] [Γ > Δ >      [@ga_mk Γ ec a b @@ l] |- [@ga_mk Γ ec (a,,x) (b,,x) @@ l] ]
 356   ; ga_second    : ∀ Γ Δ ec l a b x, ND Rule [] [Γ > Δ >      [@ga_mk Γ ec a b @@ l] |- [@ga_mk Γ ec (x,,a) (x,,b) @@ l] ]
 357   ; ga_lit       : ∀ Γ Δ ec l lit  , ND Rule [] [Γ > Δ >                          [] |- [@ga_mk Γ ec [] [literalType lit] @@ l] ]
 358   ; ga_curry     : ∀ Γ Δ ec l a b c, ND Rule [] [Γ > Δ > [@ga_mk Γ ec (a,,[b]) [c] @@ l] |- [@ga_mk Γ ec a [b ---> c] @@ l] ]
 359   ; ga_comp      : ∀ Γ Δ ec l a b c, ND Rule [] [Γ > Δ > [@ga_mk Γ ec a b @@ l],,[@ga_mk Γ ec b c @@ l] |- [@ga_mk Γ ec a c @@ l] ]
 360   ; ga_apply     : ∀ Γ Δ ec l a a' b c,
 361                  ND Rule [] [Γ > Δ > [@ga_mk Γ ec a [b ---> c] @@ l],,[@ga_mk Γ ec a' [b] @@ l] |- [@ga_mk Γ ec (a,,a') [c] @@ l] ]
 362   ; ga_kappa     : ∀ Γ Δ ec l a b Σ, ND Rule
 363   [Γ > Δ > Σ,,[@ga_mk Γ ec [] a @@ l] |- [@ga_mk Γ ec [] b @@ l] ]
 364   [Γ > Δ > Σ          |- [@ga_mk Γ ec a  b @@ l] ]
 365   }.
 366   Context `(gar:garrow).
 367
 368   Notation "a ~~~~> b" := (@ga_mk _ _ a b) (at level 20).
 369
 370   Definition boost : forall Γ Δ ant x y {lev},
 371     ND Rule []                          [ Γ > Δ > [x@@lev] |- [y@@lev] ] ->
 372     ND Rule [ Γ > Δ > ant |- [x@@lev] ] [ Γ > Δ > ant      |- [y@@lev] ].
 373     intros.
 374     eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanL ].
 375     eapply nd_comp; [ idtac | eapply nd_rule; apply (@RLet Γ Δ [] ant y x lev) ].
 376     eapply nd_comp; [ apply nd_rlecnac | idtac ].
 377     apply nd_prod.
 378     apply nd_id.
 379     eapply nd_comp.
 380       apply X.
 381       eapply nd_rule.
 382       eapply RArrange.
 383       apply RuCanL.
 384       Defined.
 385
 386   Definition postcompose' : ∀ Γ Δ ec lev a b c Σ,
 387      ND Rule [] [ Γ > Δ > Σ                        |- [@ga_mk Γ ec a b @@ lev] ] ->
 388      ND Rule [] [ Γ > Δ > Σ,,[@ga_mk Γ ec b c @@ lev] |- [@ga_mk Γ ec a c @@ lev] ].
 389      intros.
 390      eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RExch ].
 391      eapply nd_comp; [ idtac
 392        | eapply nd_rule; apply (@RLet Γ Δ [@ga_mk _ ec b c @@lev] Σ (@ga_mk _ ec a c) (@ga_mk _ ec a b) lev) ].
 393      eapply nd_comp; [ apply nd_llecnac | idtac ].
 394      apply nd_prod.
 395      apply X.
 396      eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RExch ].
 397      apply ga_comp.
 398      Defined.
 399
 400   Definition precompose Γ Δ ec : forall a x y z lev,
 401     ND Rule
 402       [ Γ > Δ > a                           |- [@ga_mk _ ec y z @@ lev] ]
 403       [ Γ > Δ > a,,[@ga_mk _ ec x y @@ lev] |- [@ga_mk _ ec x z @@ lev] ].
 404     intros.
 405     eapply nd_comp.
 406     apply nd_rlecnac.
 407     eapply nd_comp.
 408     eapply nd_prod.
 409     apply nd_id.
 410     eapply ga_comp.
 411
 412     eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RExch ].
 413
 414     apply nd_rule.
 415     apply RLet.
 416     Defined.
 417
 418   Definition precompose' : ∀ Γ Δ ec lev a b c Σ,
 419      ND Rule [] [ Γ > Δ > Σ                           |- [@ga_mk Γ ec b c @@ lev] ] ->
 420      ND Rule [] [ Γ > Δ > Σ,,[@ga_mk Γ ec a b @@ lev] |- [@ga_mk Γ ec a c @@ lev] ].
 421      intros.
 422      eapply nd_comp.
 423      apply X.
 424      apply precompose.
 425      Defined.
 426
 427   Definition postcompose : ∀ Γ Δ ec lev a b c,
 428      ND Rule [] [ Γ > Δ > []                    |- [@ga_mk Γ ec a b @@ lev] ] ->
 429      ND Rule [] [ Γ > Δ > [@ga_mk Γ ec b c @@ lev] |- [@ga_mk Γ ec a c @@ lev] ].
 430      intros.
 431      eapply nd_comp.
 432      apply postcompose'.
 433      apply X.
 434      apply nd_rule.
 435      apply RArrange.
 436      apply RCanL.
 437      Defined.
 438
 439   Definition firstify : ∀ Γ Δ ec lev a b c Σ,
 440     ND Rule [] [ Γ > Δ > Σ                     |- [@ga_mk Γ ec a b @@ lev] ] ->
 441     ND Rule [] [ Γ > Δ > Σ                    |- [@ga_mk Γ ec (a,,c) (b,,c) @@ lev] ].
 442     intros.
 443     eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanL ].
 444     eapply nd_comp; [ idtac | eapply nd_rule; apply RLet ].
 445     eapply nd_comp; [ apply nd_llecnac | idtac ].
 446     apply nd_prod.
 447     apply X.
 448     eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RuCanL ].
 449     apply ga_first.
 450     Defined.
 451
 452   Definition secondify : ∀ Γ Δ ec lev a b c Σ,
 453      ND Rule [] [ Γ > Δ > Σ                    |- [@ga_mk Γ ec a b @@ lev] ] ->
 454      ND Rule [] [ Γ > Δ > Σ                    |- [@ga_mk Γ ec (c,,a) (c,,b) @@ lev] ].
 455     intros.
 456     eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanL ].
 457     eapply nd_comp; [ idtac | eapply nd_rule; apply RLet ].
 458     eapply nd_comp; [ apply nd_llecnac | idtac ].
 459     apply nd_prod.
 460     apply X.
 461     eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RuCanL ].
 462     apply ga_second.
 463     Defined.
 464
 465   Lemma ga_unkappa     : ∀ Γ Δ ec l z a b Σ,
 466     ND Rule
 467     [Γ > Δ > Σ                         |- [@ga_mk Γ ec a b @@ l] ]
 468     [Γ > Δ > Σ,,[@ga_mk Γ ec z a @@ l] |- [@ga_mk Γ ec z b @@ l] ].
 469     intros.
 470     set (ga_comp Γ Δ ec l z a b) as q.
 471
 472     set (@RLet Γ Δ) as q'.
 473     set (@RLet Γ Δ [@ga_mk _ ec z a @@ l] Σ (@ga_mk _ ec z b) (@ga_mk _ ec a b) l) as q''.
 474     eapply nd_comp.
 475     Focus 2.
 476     eapply nd_rule.
 477     eapply RArrange.
 478     apply RExch.
 479
 480     eapply nd_comp.
 481     Focus 2.
 482     eapply nd_rule.
 483     apply q''.
 484
 485     idtac.
 486     clear q'' q'.
 487     eapply nd_comp.
 488     apply nd_rlecnac.
 489     apply nd_prod.
 490     apply nd_id.
 491     apply q.
 492     Defined.
 493
 494   Lemma ga_unkappa'     : ∀ Γ Δ ec l a b Σ x,
 495     ND Rule
 496     [Γ > Δ > Σ                          |- [@ga_mk Γ ec (a,,x)  b @@ l] ]
 497     [Γ > Δ > Σ,,[@ga_mk Γ ec [] a @@ l] |- [@ga_mk Γ ec x       b @@ l] ].
 498     intros.
 499     eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
 500     eapply nd_comp; [ apply nd_llecnac | idtac ].
 501     apply nd_prod.
 502     apply ga_first.
 503
 504     eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
 505     eapply nd_comp; [ apply nd_llecnac | idtac ].
 506     apply nd_prod.
 507     apply postcompose.
 508     apply ga_uncancell.
 509     apply precompose.
 510     Defined.
 511
 512   Lemma ga_kappa'     : ∀ Γ Δ ec l a b Σ x,
 513     ND Rule
 514     [Γ > Δ > Σ,,[@ga_mk Γ ec [] a @@ l] |- [@ga_mk Γ ec x b @@ l] ]
 515     [Γ > Δ > Σ                          |- [@ga_mk Γ ec (a,,x)  b @@ l] ].
 516     apply (Prelude_error "ga_kappa not supported yet (BIG FIXME)").
 517     Defined.
 518
 519   (* useful for cutting down on the pretty-printed noise
 520
 521   Notation "`  x" := (take_lev _ x) (at level 20).
 522   Notation "`` x" := (mapOptionTree unlev x) (at level 20).
 523   Notation "``` x" := (drop_lev _ x) (at level 20).
 524   *)
 525   Definition flatten_arrangement' :
 526     forall Γ (Δ:CoercionEnv Γ)
 527       (ec:HaskTyVar Γ ECKind) (lev:HaskLevel Γ) (ant1 ant2:Tree ??(LeveledHaskType Γ ★)) (r:Arrange ant1 ant2),
 528       ND Rule [] [Γ > Δ > [] |- [@ga_mk _ (v2t ec) (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) ant2))
 529         (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) ant1)) @@ nil] ].
 530
 531       intros Γ Δ ec lev.
 532       refine (fix flatten ant1 ant2 (r:Arrange ant1 ant2):
 533            ND Rule [] [Γ > Δ > [] |- [@ga_mk _ (v2t ec)
 534              (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) ant2))
 535              (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) ant1)) @@ nil]] :=
 536         match r as R in Arrange A B return
 537           ND Rule [] [Γ > Δ > [] |- [@ga_mk _ (v2t ec)
 538             (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) B))
 539             (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) A)) @@ nil]]
 540           with
 541           | RCanL  a             => let case_RCanL := tt  in ga_uncancell _ _ _ _ _
 542           | RCanR  a             => let case_RCanR := tt  in ga_uncancelr _ _ _ _ _
 543           | RuCanL a             => let case_RuCanL := tt in ga_cancell _ _ _ _ _
 544           | RuCanR a             => let case_RuCanR := tt in ga_cancelr _ _ _ _ _
 545           | RAssoc a b c         => let case_RAssoc := tt in ga_assoc _ _ _ _ _ _ _
 546           | RCossa a b c         => let case_RCossa := tt in ga_unassoc _ _ _ _ _ _ _
 547           | RExch  a b           => let case_RExch := tt  in ga_swap  _ _ _ _ _ _
 548           | RWeak  a             => let case_RWeak := tt  in ga_drop _ _ _ _ _
 549           | RCont  a             => let case_RCont := tt  in ga_copy  _ _ _ _ _
 550           | RLeft  a b c r'      => let case_RLeft := tt  in flatten _ _ r' ;; boost _ _ _ _ _ (ga_second _ _ _ _ _ _ _)
 551           | RRight a b c r'      => let case_RRight := tt in flatten _ _ r' ;; boost _ _ _ _ _ (ga_first  _ _ _ _ _ _ _)
 552           | RComp  c b a r1 r2   => let case_RComp := tt  in (fun r1' r2' => _) (flatten _ _ r1) (flatten _ _ r2)
 553         end); clear flatten; repeat take_simplify; repeat drop_simplify; intros.
 554
 555         destruct case_RComp.
 556           set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) a)) as a' in *.
 557           set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) b)) as b' in *.
 558           set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) c)) as c' in *.
 559           eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RCanL ].
 560           eapply nd_comp; [ idtac | eapply nd_rule; apply
 561              (@RLet Γ Δ [] [] (@ga_mk _ (v2t ec) a' c') (@ga_mk _ (v2t ec) a' b')) ].
 562           eapply nd_comp; [ apply nd_llecnac | idtac ].
 563           apply nd_prod.
 564           apply r2'.
 565           eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RuCanL ].
 566           eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RCanR ].
 567           eapply nd_comp; [ idtac | eapply nd_rule;  apply
 568             (@RLet Γ Δ [@ga_mk _ (v2t ec) a' b' @@ _] [] (@ga_mk _ (v2t ec) a' c') (@ga_mk _ (v2t ec) b' c'))].
 569           eapply nd_comp; [ apply nd_llecnac | idtac ].
 570           eapply nd_prod.
 571           apply r1'.
 572           apply ga_comp.
 573           Defined.
 574
 575   Definition flatten_arrangement :
 576     forall Γ (Δ:CoercionEnv Γ) n
 577       (ec:HaskTyVar Γ ECKind) (lev:HaskLevel Γ) (ant1 ant2:Tree ??(LeveledHaskType Γ ★)) (r:Arrange ant1 ant2) succ,
 578       ND Rule
 579       [Γ > Δ > mapOptionTree (flatten_leveled_type ) (drop_lev n ant1)
 580         |- [@ga_mk _ (v2t ec)
 581           (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) ant1))
 582           (mapOptionTree (flatten_type ○ unlev) succ) @@ nil]]
 583       [Γ > Δ > mapOptionTree (flatten_leveled_type ) (drop_lev n ant2)
 584         |- [@ga_mk _ (v2t ec)
 585           (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) ant2))
 586           (mapOptionTree (flatten_type ○ unlev) succ) @@ nil]].
 587       intros.
 588       refine ( _ ;; (boost _ _ _ _ _ (postcompose _ _ _ _ _ _ _ (flatten_arrangement' Γ Δ ec lev ant1 ant2 r)))).
 589       apply nd_rule.
 590       apply RArrange.
 591       refine ((fix flatten ant1 ant2 (r:Arrange ant1 ant2) :=
 592         match r as R in Arrange A B return
 593           Arrange (mapOptionTree (flatten_leveled_type ) (drop_lev _ A))
 594           (mapOptionTree (flatten_leveled_type ) (drop_lev _ B)) with
 595           | RCanL  a             => let case_RCanL := tt  in RCanL _
 596           | RCanR  a             => let case_RCanR := tt  in RCanR _
 597           | RuCanL a             => let case_RuCanL := tt in RuCanL _
 598           | RuCanR a             => let case_RuCanR := tt in RuCanR _
 599           | RAssoc a b c         => let case_RAssoc := tt in RAssoc _ _ _
 600           | RCossa a b c         => let case_RCossa := tt in RCossa _ _ _
 601           | RExch  a b           => let case_RExch := tt  in RExch _ _
 602           | RWeak  a             => let case_RWeak := tt  in RWeak _
 603           | RCont  a             => let case_RCont := tt  in RCont _
 604           | RLeft  a b c r'      => let case_RLeft := tt  in RLeft  _ (flatten _ _ r')
 605           | RRight a b c r'      => let case_RRight := tt in RRight _ (flatten _ _ r')
 606           | RComp  a b c r1 r2   => let case_RComp := tt  in RComp    (flatten _ _ r1) (flatten _ _ r2)
 607         end) ant1 ant2 r); clear flatten; repeat take_simplify; repeat drop_simplify; intros.
 608         Defined.
 609
 610   Definition flatten_arrangement'' :
 611     forall  Γ Δ ant1 ant2 succ (r:Arrange ant1 ant2),
 612       ND Rule (mapOptionTree (flatten_judgment ) [Γ > Δ > ant1 |- succ])
 613       (mapOptionTree (flatten_judgment ) [Γ > Δ > ant2 |- succ]).
 614     intros.
 615     simpl.
 616     set (getjlev succ) as succ_lev.
 617     assert (succ_lev=getjlev succ).
 618       reflexivity.
 619
 620     destruct succ_lev.
 621       apply nd_rule.
 622       apply RArrange.
 623       induction r; simpl.
 624         apply RCanL.
 625         apply RCanR.
 626         apply RuCanL.
 627         apply RuCanR.
 628         apply RAssoc.
 629         apply RCossa.
 630         apply RExch.
 631         apply RWeak.
 632         apply RCont.
 633         apply RLeft; auto.
 634         apply RRight; auto.
 635         eapply RComp; [ apply IHr1 | apply IHr2 ].
 636
 637       apply flatten_arrangement.
 638         apply r.
 639         Defined.
 640
 641   Definition ga_join Γ Δ Σ₁ Σ₂ a b ec :
 642     ND Rule [] [Γ > Δ > Σ₁     |- [@ga_mk _ ec [] a      @@ nil]] ->
 643     ND Rule [] [Γ > Δ > Σ₂     |- [@ga_mk _ ec [] b      @@ nil]] ->
 644     ND Rule [] [Γ > Δ > Σ₁,,Σ₂ |- [@ga_mk _ ec [] (a,,b) @@ nil]].
 645     intro pfa.
 646     intro pfb.
 647     apply secondify with (c:=a)  in pfb.
 648     eapply nd_comp.
 649     Focus 2.
 650     eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
 651     eapply nd_comp; [ eapply nd_llecnac | idtac ].
 652     eapply nd_prod.
 653     apply pfb.
 654     clear pfb.
 655     apply postcompose'.
 656     eapply nd_comp.
 657     apply pfa.
 658     clear pfa.
 659     apply boost.
 660     eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanL ].
 661     apply precompose'.
 662     apply ga_uncancelr.
 663     apply nd_id.
 664     Defined.
 665
 666   Definition arrange_brak : forall Γ Δ ec succ t,
 667    ND Rule
 668      [Γ > Δ > mapOptionTree (flatten_leveled_type ) (drop_lev (ec :: nil) succ),,
 669       [(@ga_mk _ (v2t ec) [] (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: nil) succ))) @@  nil] |- [t @@ nil]]
 670      [Γ > Δ > mapOptionTree (flatten_leveled_type ) succ |- [t @@  nil]].
 671     intros.
 672     unfold drop_lev.
 673     set (@arrange' _ succ (levelMatch (ec::nil))) as q.
 674     set (arrangeMap _ _ flatten_leveled_type q) as y.
 675     eapply nd_comp.
 676     Focus 2.
 677     eapply nd_rule.
 678     eapply RArrange.
 679     apply y.
 680     idtac.
 681     clear y q.
 682     simpl.
 683     eapply nd_comp; [ apply nd_llecnac | idtac ].
 684     eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
 685     apply nd_prod.
 686     Focus 2.
 687     apply nd_id.
 688     idtac.
 689     induction succ; try destruct a; simpl.
 690     unfold take_lev.
 691     unfold mkTakeFlags.
 692     unfold mkFlags.
 693     unfold bnot.
 694     simpl.
 695     destruct l as [t' lev'].
 696     destruct lev' as [|ec' lev'].
 697     simpl.
 698     apply ga_id.
 699     unfold levelMatch.
 700     set (@eqd_dec (HaskLevel Γ) (haskLevelEqDecidable Γ) (ec' :: lev') (ec :: nil)) as q.
 701     destruct q.
 702     inversion e; subst.
 703     simpl.
 704     apply nd_rule.
 705     unfold flatten_leveled_type.
 706     simpl.
 707     unfold flatten_type.
 708     simpl.
 709     unfold ga_mk.
 710     simpl.
 711     apply RVar.
 712     simpl.
 713     apply ga_id.
 714     apply ga_id.
 715     unfold take_lev.
 716     simpl.
 717     apply ga_join.
 718       apply IHsucc1.
 719       apply IHsucc2.
 720     Defined.
 721
 722   Definition arrange_esc : forall Γ Δ ec succ t,
 723    ND Rule
 724      [Γ > Δ > mapOptionTree (flatten_leveled_type ) succ |- [t @@  nil]]
 725      [Γ > Δ > mapOptionTree (flatten_leveled_type ) (drop_lev (ec :: nil) succ),,
 726       [(@ga_mk _ (v2t ec) [] (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: nil) succ))) @@  nil] |- [t @@  nil]].
 727     intros.
 728     unfold drop_lev.
 729     set (@arrange _ succ (levelMatch (ec::nil))) as q.
 730     set (arrangeMap _ _ flatten_leveled_type q) as y.
 731     eapply nd_comp.
 732     eapply nd_rule.
 733     eapply RArrange.
 734     apply y.
 735     idtac.
 736     clear y q.
 737
 738     induction succ.
 739     destruct a.
 740       destruct l.
 741       simpl.
 742       unfold mkDropFlags; simpl.
 743       unfold take_lev.
 744       unfold mkTakeFlags.
 745       simpl.
 746       destruct (General.list_eq_dec h0 (ec :: nil)).
 747         simpl.
 748         rewrite e.
 749         apply nd_id.
 750         simpl.
 751         apply nd_rule.
 752         apply RArrange.
 753         apply RLeft.
 754         apply RWeak.
 755       simpl.
 756         apply nd_rule.
 757         unfold take_lev.
 758         simpl.
 759         apply RArrange.
 760         apply RLeft.
 761         apply RWeak.
 762       apply (Prelude_error "escapifying code with multi-leaf antecedents is not supported").
 763       Defined.
 764
 765   Lemma mapOptionTree_distributes
 766     : forall T R (a b:Tree ??T) (f:T->R),
 767       mapOptionTree f (a,,b) = (mapOptionTree f a),,(mapOptionTree f b).
 768     reflexivity.
 769     Qed.
 770
 771   Definition decide_tree_empty : forall {T:Type}(t:Tree ??T),
 772     sum { q:Tree unit & t = mapTree (fun _ => None) q } unit.
 773     intro T.
 774     refine (fix foo t :=
 775       match t with
 776         | T_Leaf x => _
 777         | T_Branch b1 b2 => let b1' := foo b1 in let b2' := foo b2 in _
 778       end).
 779     intros.
 780     destruct x.
 781     right; apply tt.
 782     left.
 783       exists (T_Leaf tt).
 784       auto.
 785     destruct b1'.
 786     destruct b2'.
 787     destruct s.
 788     destruct s0.
 789     subst.
 790     left.
 791     exists (x,,x0).
 792     reflexivity.
 793     right; auto.
 794     right; auto.
 795     Defined.
 796
 797   Lemma unlev_relev : forall {Γ}(t:Tree ??(HaskType Γ ★)) lev, mapOptionTree unlev (t @@@ lev) = t.
 798     intros.
 799     induction t.
 800     destruct a; reflexivity.
 801     rewrite <- IHt1 at 2.
 802     rewrite <- IHt2 at 2.
 803     reflexivity.
 804     Qed.
 805
 806   Lemma tree_of_nothing : forall Γ ec t a,
 807     Arrange (a,,mapOptionTree flatten_leveled_type (drop_lev(Γ:=Γ) (ec :: nil) (t @@@ (ec :: nil)))) a.
 808     intros.
 809     induction t; try destruct o; try destruct a0.
 810     simpl.
 811     drop_simplify.
 812     simpl.
 813     apply RCanR.
 814     simpl.
 815     apply RCanR.
 816     Opaque drop_lev.
 817     simpl.
 818     Transparent drop_lev.
 819     drop_simplify.
 820     simpl.
 821     eapply RComp.
 822     eapply RComp.
 823     eapply RAssoc.
 824     eapply RRight.
 825     apply IHt1.
 826     apply IHt2.
 827     Defined.
 828
 829   Lemma tree_of_nothing' : forall Γ ec t a,
 830     Arrange a (a,,mapOptionTree flatten_leveled_type (drop_lev(Γ:=Γ) (ec :: nil) (t @@@ (ec :: nil)))).
 831     intros.
 832     induction t; try destruct o; try destruct a0.
 833     simpl.
 834     drop_simplify.
 835     simpl.
 836     apply RuCanR.
 837     simpl.
 838     apply RuCanR.
 839     Opaque drop_lev.
 840     simpl.
 841     Transparent drop_lev.
 842     drop_simplify.
 843     simpl.
 844     eapply RComp.
 845     Focus 2.
 846     eapply RComp.
 847     Focus 2.
 848     eapply RCossa.
 849     Focus 2.
 850     eapply RRight.
 851     apply IHt1.
 852     apply IHt2.
 853     Defined.
 854
 855   Axiom extensionality : forall Γ Q (f g:forall TV, InstantiatedTypeEnv TV Γ -> Q TV),
 856     (forall tv ite, f tv ite = g tv ite) -> f=g.
 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 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 [ ].