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 NaturalDeductionContext.
  13 Require Import Coq.Strings.String.
  14 Require Import Coq.Lists.List.
  15
  16 Require Import HaskKinds.
  17 Require Import HaskCoreTypes.
  18 Require Import HaskCoreVars.
  19 Require Import HaskWeakTypes.
  20 Require Import HaskWeakVars.
  21 Require Import HaskLiterals.
  22 Require Import HaskTyCons.
  23 Require Import HaskStrongTypes.
  24 Require Import HaskProof.
  25 Require Import NaturalDeduction.
  26
  27 Require Import HaskStrongTypes.
  28 Require Import HaskStrong.
  29 Require Import HaskProof.
  30 Require Import HaskStrongToProof.
  31 Require Import HaskProofToStrong.
  32 Require Import HaskWeakToStrong.
  33
  34 Require Import HaskSkolemizer.
  35
  36 Open Scope nd_scope.
  37 Set Printing Width 130.
  38
  39 (*
  40  *  The flattening transformation.  Currently only TWO-level languages are
  41  *  supported, and the level-1 sublanguage is rather limited.
  42  *
  43  *  This file abuses terminology pretty badly.  For purposes of this file,
  44  *  "PCF" means "the level-1 sublanguage" and "FC" (aka System FC) means
  45  *  the whole language (level-0 language including bracketed level-1 terms)
  46  *)
  47 Section HaskFlattener.
  48
  49
  50   Ltac eqd_dec_refl' :=
  51     match goal with
  52       | [ |- context[@eqd_dec ?T ?V ?X ?X] ] =>
  53         destruct (@eqd_dec T V X X) as [eqd_dec1 | eqd_dec2];
  54           [ clear eqd_dec1 | set (eqd_dec2 (refl_equal _)) as eqd_dec2'; inversion eqd_dec2' ]
  55   end.
  56
  57   Definition v2t {Γ}(ec:HaskTyVar Γ ECKind) : HaskType Γ ECKind := fun TV ite => TVar (ec TV ite).
  58
  59   Definition levelMatch {Γ}(lev:HaskLevel Γ) : LeveledHaskType Γ ★ -> bool :=
  60     fun t => match t with ttype@@tlev => if eqd_dec tlev lev then true else false end.
  61
  62   (* In a tree of types, replace any type at depth "lev" or greater None *)
  63   Definition mkDropFlags {Γ}(lev:HaskLevel Γ)(tt:Tree ??(LeveledHaskType Γ ★)) : TreeFlags tt :=
  64     mkFlags (liftBoolFunc false (levelMatch lev)) tt.
  65
  66   Definition drop_lev {Γ}(lev:HaskLevel Γ)(tt:Tree ??(LeveledHaskType Γ ★)) : Tree ??(LeveledHaskType Γ ★) :=
  67     dropT (mkDropFlags lev tt).
  68
  69   (* The opposite: replace any type which is NOT at level "lev" with None *)
  70   Definition mkTakeFlags {Γ}(lev:HaskLevel Γ)(tt:Tree ??(LeveledHaskType Γ ★)) : TreeFlags tt :=
  71     mkFlags (liftBoolFunc true (bnot ○ levelMatch lev)) tt.
  72
  73   Definition take_lev {Γ}(lev:HaskLevel Γ)(tt:Tree ??(LeveledHaskType Γ ★)) : Tree ??(LeveledHaskType Γ ★) :=
  74     dropT (mkTakeFlags lev tt).
  75 (*
  76     mapOptionTree (fun x => flatten_type (unlev x))
  77     (maybeTree (takeT tt (mkFlags (
  78       fun t => match t with
  79                  | Some (ttype @@ tlev) => if eqd_dec tlev lev then true else false
  80                  | _                    => true
  81                end
  82     ) tt))).
  83
  84   Definition maybeTree {T}(t:??(Tree ??T)) : Tree ??T :=
  85     match t with
  86       | None   => []
  87       | Some x => x
  88     end.
  89 *)
  90
  91   Lemma drop_lev_lemma : forall Γ (lev:HaskLevel Γ) x, drop_lev lev [x @@  lev] = [].
  92     intros; simpl.
  93     Opaque eqd_dec.
  94     unfold drop_lev.
  95     simpl.
  96     unfold mkDropFlags.
  97     simpl.
  98     Transparent eqd_dec.
  99     eqd_dec_refl'.
 100     auto.
 101     Qed.
 102
 103   Lemma drop_lev_lemma_s : forall Γ (lev:HaskLevel Γ) ec x, drop_lev (ec::lev) [x @@  (ec :: lev)] = [].
 104     intros; simpl.
 105     Opaque eqd_dec.
 106     unfold drop_lev.
 107     unfold mkDropFlags.
 108     simpl.
 109     Transparent eqd_dec.
 110     eqd_dec_refl'.
 111     auto.
 112     Qed.
 113
 114   Lemma take_lemma : forall Γ (lev:HaskLevel Γ) x, take_lev lev [x @@  lev] = [x @@ lev].
 115     intros; simpl.
 116     Opaque eqd_dec.
 117     unfold take_lev.
 118     unfold mkTakeFlags.
 119     simpl.
 120     Transparent eqd_dec.
 121     eqd_dec_refl'.
 122     auto.
 123     Qed.
 124
 125   Lemma take_lemma' : forall Γ (lev:HaskLevel Γ) x, take_lev lev (x @@@ lev) = x @@@ lev.
 126     intros.
 127     induction x.
 128     destruct a; simpl; try reflexivity.
 129     apply take_lemma.
 130     simpl.
 131     rewrite <- IHx1 at 2.
 132     rewrite <- IHx2 at 2.
 133     reflexivity.
 134     Qed.
 135 (*
 136   Lemma drop_lev_lemma' : forall Γ (lev:HaskLevel Γ) x, drop_lev lev (x @@@ lev) = [].
 137     intros.
 138     induction x.
 139     destruct a; simpl; try reflexivity.
 140     apply drop_lev_lemma.
 141     simpl.
 142     change (@drop_lev _ lev (x1 @@@ lev ,, x2 @@@ lev))
 143       with ((@drop_lev _ lev (x1 @@@ lev)) ,, (@drop_lev _ lev (x2 @@@ lev))).
 144     simpl.
 145     rewrite IHx1.
 146     rewrite IHx2.
 147     reflexivity.
 148     Qed.
 149 *)
 150   Ltac drop_simplify :=
 151     match goal with
 152       | [ |- context[@drop_lev ?G ?L [ ?X @@ ?L ] ] ] =>
 153         rewrite (drop_lev_lemma G L X)
 154 (*
 155       | [ |- context[@drop_lev ?G ?L [ ?X @@@ ?L ] ] ] =>
 156         rewrite (drop_lev_lemma' G L X)
 157 *)
 158       | [ |- context[@drop_lev ?G (?E :: ?L) [ ?X @@ (?E :: ?L) ] ] ] =>
 159         rewrite (drop_lev_lemma_s G L E X)
 160       | [ |- context[@drop_lev ?G ?N (?A,,?B)] ] =>
 161       change (@drop_lev G N (A,,B)) with ((@drop_lev G N A),,(@drop_lev G N B))
 162       | [ |- context[@drop_lev ?G ?N (T_Leaf None)] ] =>
 163       change (@drop_lev G N (T_Leaf (@None (LeveledHaskType G ★)))) with (T_Leaf (@None (LeveledHaskType G ★)))
 164     end.
 165
 166   Ltac take_simplify :=
 167     match goal with
 168       | [ |- context[@take_lev ?G ?L [ ?X @@ ?L ] ] ] =>
 169         rewrite (take_lemma G L X)
 170       | [ |- context[@take_lev ?G ?L [ ?X @@@ ?L ] ] ] =>
 171         rewrite (take_lemma' G L X)
 172       | [ |- context[@take_lev ?G ?N (?A,,?B)] ] =>
 173       change (@take_lev G N (A,,B)) with ((@take_lev G N A),,(@take_lev G N B))
 174       | [ |- context[@take_lev ?G ?N (T_Leaf None)] ] =>
 175       change (@take_lev G N (T_Leaf (@None (LeveledHaskType G ★)))) with (T_Leaf (@None (LeveledHaskType G ★)))
 176     end.
 177
 178
 179   (*******************************************************************************)
 180
 181
 182   Context (hetmet_flatten : WeakExprVar).
 183   Context (hetmet_unflatten : WeakExprVar).
 184   Context (hetmet_id      : WeakExprVar).
 185   Context {unitTy : forall TV, RawHaskType TV ECKind  -> RawHaskType TV ★                                          }.
 186   Context {prodTy : forall TV, RawHaskType TV ECKind  -> RawHaskType TV ★  -> RawHaskType TV ★ -> RawHaskType TV ★ }.
 187   Context {gaTy   : forall TV, RawHaskType TV ECKind  -> RawHaskType TV ★ -> RawHaskType TV ★  -> RawHaskType TV ★ }.
 188
 189   Definition ga_mk_tree' {TV}(ec:RawHaskType TV ECKind)(tr:Tree ??(RawHaskType TV ★)) : RawHaskType TV ★ :=
 190     reduceTree (unitTy TV ec) (prodTy TV ec) tr.
 191
 192   Definition ga_mk_tree {Γ}(ec:HaskType Γ ECKind)(tr:Tree ??(HaskType Γ ★)) : HaskType Γ ★ :=
 193     fun TV ite => ga_mk_tree' (ec TV ite) (mapOptionTree (fun x => x TV ite) tr).
 194
 195   Definition ga_mk_raw {TV}(ec:RawHaskType TV ECKind)(ant suc:Tree ??(RawHaskType TV ★)) : RawHaskType TV ★ :=
 196     gaTy TV ec
 197     (ga_mk_tree' ec ant)
 198     (ga_mk_tree' ec suc).
 199
 200   Definition ga_mk {Γ}(ec:HaskType Γ ECKind)(ant suc:Tree ??(HaskType Γ ★)) : HaskType Γ ★ :=
 201     fun TV ite => gaTy TV (ec TV ite) (ga_mk_tree ec ant TV ite) (ga_mk_tree ec suc TV ite).
 202
 203   (*
 204    *  The story:
 205    *    - code types <[t]>@c                                                become garrows  c () t
 206    *    - free variables of type t at a level lev deeper than the succedent become garrows  c () t
 207    *    - free variables at the level of the succedent become
 208    *)
 209   Fixpoint flatten_rawtype {TV}{κ}(exp: RawHaskType TV κ) : RawHaskType TV κ :=
 210     match exp with
 211     | TVar    _  x          => TVar x
 212     | TAll     _ y          => TAll   _  (fun v => flatten_rawtype (y v))
 213     | TApp   _ _ x y        => TApp      (flatten_rawtype x) (flatten_rawtype y)
 214     | TCon       tc         => TCon      tc
 215     | TCoerc _ t1 t2 t      => TCoerc    (flatten_rawtype t1) (flatten_rawtype t2) (flatten_rawtype t)
 216     | TArrow                => TArrow
 217     | TCode     ec e        => let e' := flatten_rawtype e
 218                                in  ga_mk_raw ec (unleaves_ (take_arg_types e')) [drop_arg_types e']
 219     | TyFunApp  tfc kl k lt => TyFunApp tfc kl k (flatten_rawtype_list _ lt)
 220     end
 221     with flatten_rawtype_list {TV}(lk:list Kind)(exp:@RawHaskTypeList TV lk) : @RawHaskTypeList TV lk :=
 222     match exp in @RawHaskTypeList _ LK return @RawHaskTypeList TV LK with
 223     | TyFunApp_nil               => TyFunApp_nil
 224     | TyFunApp_cons  κ kl t rest => TyFunApp_cons _ _ (flatten_rawtype t) (flatten_rawtype_list _ rest)
 225     end.
 226
 227   Definition flatten_type {Γ}{κ}(ht:HaskType Γ κ) : HaskType Γ κ :=
 228     fun TV ite => flatten_rawtype (ht TV ite).
 229
 230   Fixpoint levels_to_tcode {Γ}(ht:HaskType Γ ★)(lev:HaskLevel Γ) : HaskType Γ ★ :=
 231     match lev with
 232       | nil      => flatten_type ht
 233       | ec::lev' => @ga_mk _ (v2t ec) [] [levels_to_tcode ht lev']
 234     end.
 235
 236   Definition flatten_leveled_type {Γ}(ht:LeveledHaskType Γ ★) : LeveledHaskType Γ ★ :=
 237     levels_to_tcode (unlev ht) (getlev ht) @@ nil.
 238
 239   (* AXIOMS *)
 240
 241   Axiom literal_types_unchanged : forall Γ l, flatten_type (literalType l) = literalType(Γ:=Γ) l.
 242
 243   Axiom flatten_coercion : forall Γ Δ κ (σ τ:HaskType Γ κ) (γ:HaskCoercion Γ Δ (σ ∼∼∼ τ)),
 244     HaskCoercion Γ Δ (flatten_type σ ∼∼∼ flatten_type τ).
 245
 246   Axiom flatten_commutes_with_substT :
 247     forall  κ Γ (Δ:CoercionEnv Γ) (σ:∀ TV, InstantiatedTypeEnv TV Γ → TV κ → RawHaskType TV ★) (τ:HaskType Γ κ),
 248     flatten_type  (substT σ τ) = substT (fun TV ite v => flatten_rawtype  (σ TV ite v))
 249       (flatten_type  τ).
 250
 251   Axiom flatten_commutes_with_HaskTAll :
 252     forall  κ Γ (Δ:CoercionEnv Γ) (σ:∀ TV, InstantiatedTypeEnv TV Γ → TV κ → RawHaskType TV ★),
 253     flatten_type  (HaskTAll κ σ) = HaskTAll κ (fun TV ite v => flatten_rawtype (σ TV ite v)).
 254
 255   Axiom flatten_commutes_with_HaskTApp :
 256     forall  κ Γ (Δ:CoercionEnv Γ) (σ:∀ TV, InstantiatedTypeEnv TV Γ → TV κ → RawHaskType TV ★),
 257     flatten_type  (HaskTApp (weakF σ) (FreshHaskTyVar κ)) =
 258     HaskTApp (weakF (fun TV ite v => flatten_rawtype  (σ TV ite v))) (FreshHaskTyVar κ).
 259
 260   Axiom flatten_commutes_with_weakLT : forall (Γ:TypeEnv) κ  t,
 261     flatten_leveled_type  (weakLT(Γ:=Γ)(κ:=κ) t) = weakLT(Γ:=Γ)(κ:=κ) (flatten_leveled_type  t).
 262
 263   Axiom globals_do_not_have_code_types : forall (Γ:TypeEnv) (g:Global Γ) v,
 264     flatten_type (g v) = g v.
 265
 266   (* "n" is the maximum depth remaining AFTER flattening *)
 267   Definition flatten_judgment (j:Judg) :=
 268     match j as J return Judg with
 269       | Γ > Δ > ant |- suc @ nil        => Γ > Δ > mapOptionTree flatten_leveled_type ant
 270                                                 |- mapOptionTree flatten_type suc @ nil
 271       | Γ > Δ > ant |- suc @ (ec::lev') => Γ > Δ > mapOptionTree flatten_leveled_type (drop_lev (ec::lev') ant)
 272                                                 |- [ga_mk (v2t ec)
 273                                                   (mapOptionTree (flatten_type ○ unlev) (take_lev (ec::lev') ant))
 274                                                   (mapOptionTree  flatten_type                               suc )
 275                                                   ] @ nil
 276     end.
 277
 278   Class garrow :=
 279   { ga_id        : ∀ Γ Δ ec l a    , ND Rule [] [Γ > Δ >                          [] |- [@ga_mk Γ ec a a ]@l ]
 280   ; ga_cancelr   : ∀ Γ Δ ec l a    , ND Rule [] [Γ > Δ >                          [] |- [@ga_mk Γ ec (a,,[]) a ]@l ]
 281   ; ga_cancell   : ∀ Γ Δ ec l a    , ND Rule [] [Γ > Δ >                          [] |- [@ga_mk Γ ec ([],,a) a ]@l ]
 282   ; ga_uncancelr : ∀ Γ Δ ec l a    , ND Rule [] [Γ > Δ >                          [] |- [@ga_mk Γ ec a (a,,[]) ]@l ]
 283   ; ga_uncancell : ∀ Γ Δ ec l a    , ND Rule [] [Γ > Δ >                          [] |- [@ga_mk Γ ec a ([],,a) ]@l ]
 284   ; ga_assoc     : ∀ Γ Δ ec l a b c, ND Rule [] [Γ > Δ >                          [] |- [@ga_mk Γ ec ((a,,b),,c) (a,,(b,,c)) ]@l ]
 285   ; ga_unassoc   : ∀ Γ Δ ec l a b c, ND Rule [] [Γ > Δ >                          [] |- [@ga_mk Γ ec (a,,(b,,c)) ((a,,b),,c) ]@l ]
 286   ; ga_swap      : ∀ Γ Δ ec l a b  , ND Rule [] [Γ > Δ >                          [] |- [@ga_mk Γ ec (a,,b) (b,,a) ]@l ]
 287   ; ga_drop      : ∀ Γ Δ ec l a    , ND Rule [] [Γ > Δ >                          [] |- [@ga_mk Γ ec a [] ]@l ]
 288   ; ga_copy      : ∀ Γ Δ ec l a    , ND Rule [] [Γ > Δ >                          [] |- [@ga_mk Γ ec a (a,,a) ]@l ]
 289   ; ga_first     : ∀ Γ Δ ec l a b x, ND Rule [] [Γ > Δ >      [@ga_mk Γ ec a b @@l] |- [@ga_mk Γ ec (a,,x) (b,,x) ]@l ]
 290   ; ga_second    : ∀ Γ Δ ec l a b x, ND Rule [] [Γ > Δ >      [@ga_mk Γ ec a b @@l] |- [@ga_mk Γ ec (x,,a) (x,,b) ]@l ]
 291   ; ga_lit       : ∀ Γ Δ ec l lit  , ND Rule [] [Γ > Δ >                          [] |- [@ga_mk Γ ec [] [literalType lit] ]@l ]
 292   ; ga_curry     : ∀ Γ Δ ec l a b c, ND Rule [] [Γ > Δ > [@ga_mk Γ ec (a,,[b]) [c] @@ l] |- [@ga_mk Γ ec a [b ---> c] ]@ l ]
 293   ; 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 ]
 294   ; ga_apply     : ∀ Γ Δ ec l a a' b c,
 295                  ND Rule [] [Γ > Δ > [@ga_mk Γ ec a [b ---> c] @@ l],,[@ga_mk Γ ec a' [b] @@ l] |- [@ga_mk Γ ec (a,,a') [c] ]@l ]
 296   ; ga_kappa     : ∀ Γ Δ ec l a b Σ, ND Rule
 297   [Γ > Δ > Σ,,[@ga_mk Γ ec [] a @@ l] |- [@ga_mk Γ ec [] b ]@l ]
 298   [Γ > Δ > Σ          |- [@ga_mk Γ ec a  b ]@l ]
 299   }.
 300   Context `(gar:garrow).
 301
 302   Notation "a ~~~~> b" := (@ga_mk _ _ a b) (at level 20).
 303
 304   Definition boost : forall Γ Δ ant x y {lev},
 305     ND Rule []                         [ Γ > Δ > [x@@lev] |- [y]@lev ] ->
 306     ND Rule [ Γ > Δ > ant |- [x]@lev ] [ Γ > Δ > ant      |- [y]@lev ].
 307     intros.
 308     eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanR ].
 309     eapply nd_comp; [ idtac | eapply nd_rule; apply RLet ].
 310     eapply nd_comp; [ apply nd_rlecnac | idtac ].
 311     apply nd_prod.
 312     apply nd_id.
 313     eapply nd_comp.
 314       apply X.
 315       eapply nd_rule.
 316       eapply RArrange.
 317       apply RuCanR.
 318     Defined.
 319
 320   Definition precompose Γ Δ ec : forall a x y z lev,
 321     ND Rule
 322       [ Γ > Δ > a                           |- [@ga_mk _ ec y z ]@lev ]
 323       [ Γ > Δ > a,,[@ga_mk _ ec x y @@ lev] |- [@ga_mk _ ec x z ]@lev ].
 324     intros.
 325     eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
 326     eapply nd_comp; [ apply nd_rlecnac | idtac ].
 327     apply nd_prod.
 328     apply nd_id.
 329     eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RExch ].
 330     apply ga_comp.
 331     Defined.
 332
 333   Definition precompose' Γ Δ ec : forall a b x y z lev,
 334     ND Rule
 335       [ Γ > Δ > a,,b                             |- [@ga_mk _ ec y z ]@lev ]
 336       [ Γ > Δ > a,,([@ga_mk _ ec x y @@ lev],,b) |- [@ga_mk _ ec x z ]@lev ].
 337     intros.
 338     eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RLeft; eapply RExch ].
 339     eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCossa ].
 340     apply precompose.
 341     Defined.
 342
 343   Definition postcompose_ Γ Δ ec : forall a x y z lev,
 344     ND Rule
 345       [ Γ > Δ > a                           |- [@ga_mk _ ec x y ]@lev ]
 346       [ Γ > Δ > a,,[@ga_mk _ ec y z @@ lev] |- [@ga_mk _ ec x z ]@lev ].
 347     intros.
 348     eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
 349     eapply nd_comp; [ apply nd_rlecnac | idtac ].
 350     apply nd_prod.
 351     apply nd_id.
 352     apply ga_comp.
 353     Defined.
 354
 355   Definition postcompose  Γ Δ ec : forall x y z lev,
 356     ND Rule [] [ Γ > Δ > []                       |- [@ga_mk _ ec x y ]@lev ] ->
 357     ND Rule [] [ Γ > Δ > [@ga_mk _ ec y z @@ lev] |- [@ga_mk _ ec x z ]@lev ].
 358     intros.
 359     eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanL ].
 360     eapply nd_comp; [ idtac | eapply postcompose_ ].
 361     apply X.
 362     Defined.
 363
 364   Definition first_nd : ∀ Γ Δ ec lev a b c Σ,
 365     ND Rule [ Γ > Δ > Σ                    |- [@ga_mk Γ ec a b ]@lev ]
 366             [ Γ > Δ > Σ                    |- [@ga_mk Γ ec (a,,c) (b,,c) ]@lev ].
 367     intros.
 368     eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanR ].
 369     eapply nd_comp; [ idtac | eapply nd_rule; apply RLet ].
 370     eapply nd_comp; [ apply nd_rlecnac | idtac ].
 371     apply nd_prod.
 372     apply nd_id.
 373     eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RuCanR ].
 374     apply ga_first.
 375     Defined.
 376
 377   Definition firstify : ∀ Γ Δ ec lev a b c Σ,
 378     ND Rule [] [ Γ > Δ > Σ                    |- [@ga_mk Γ ec a b ]@lev ] ->
 379     ND Rule [] [ Γ > Δ > Σ                    |- [@ga_mk Γ ec (a,,c) (b,,c) ]@lev ].
 380     intros.
 381     eapply nd_comp.
 382     apply X.
 383     apply first_nd.
 384     Defined.
 385
 386   Definition second_nd : ∀ Γ Δ ec lev a b c Σ,
 387      ND Rule
 388      [ Γ > Δ > Σ                    |- [@ga_mk Γ ec a b ]@lev ]
 389      [ Γ > Δ > Σ                    |- [@ga_mk Γ ec (c,,a) (c,,b) ]@lev ].
 390     intros.
 391     eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanR ].
 392     eapply nd_comp; [ idtac | eapply nd_rule; apply RLet ].
 393     eapply nd_comp; [ apply nd_rlecnac | idtac ].
 394     apply nd_prod.
 395     apply nd_id.
 396     eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RuCanR ].
 397     apply ga_second.
 398     Defined.
 399
 400   Definition secondify : ∀ Γ Δ ec lev a b c Σ,
 401      ND Rule [] [ Γ > Δ > Σ                    |- [@ga_mk Γ ec a b ]@lev ] ->
 402      ND Rule [] [ Γ > Δ > Σ                    |- [@ga_mk Γ ec (c,,a) (c,,b) ]@lev ].
 403     intros.
 404     eapply nd_comp.
 405     apply X.
 406     apply second_nd.
 407     Defined.
 408
 409    Lemma ga_unkappa     : ∀ Γ Δ ec l a b Σ x,
 410      ND Rule
 411      [Γ > Δ > Σ                          |- [@ga_mk Γ ec (a,,x)  b ]@l ]
 412      [Γ > Δ > Σ,,[@ga_mk Γ ec [] a @@ l] |- [@ga_mk Γ ec x       b ]@l ].
 413      intros.
 414      eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RExch ].
 415      eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
 416      eapply nd_comp; [ apply nd_llecnac | idtac ].
 417      apply nd_prod.
 418      apply ga_first.
 419
 420      eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
 421      eapply nd_comp; [ apply nd_llecnac | idtac ].
 422      apply nd_prod.
 423      apply postcompose.
 424      apply ga_uncancell.
 425      eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RExch ].
 426      apply precompose.
 427      Defined.
 428
 429   (* useful for cutting down on the pretty-printed noise
 430
 431   Notation "`  x" := (take_lev _ x) (at level 20).
 432   Notation "`` x" := (mapOptionTree unlev x) (at level 20).
 433   Notation "``` x" := (drop_lev _ x) (at level 20).
 434   *)
 435   Definition flatten_arrangement' :
 436     forall Γ (Δ:CoercionEnv Γ)
 437       (ec:HaskTyVar Γ ECKind) (lev:HaskLevel Γ) (ant1 ant2:Tree ??(LeveledHaskType Γ ★)) (r:Arrange ant1 ant2),
 438       ND Rule [] [Γ > Δ > [] |- [@ga_mk _ (v2t ec) (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) ant2))
 439         (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) ant1)) ]@nil ].
 440
 441       intros Γ Δ ec lev.
 442       refine (fix flatten ant1 ant2 (r:Arrange ant1 ant2):
 443            ND Rule [] [Γ > Δ > [] |- [@ga_mk _ (v2t ec)
 444              (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) ant2))
 445              (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) ant1)) ]@nil] :=
 446         match r as R in Arrange A B return
 447           ND Rule [] [Γ > Δ > [] |- [@ga_mk _ (v2t ec)
 448             (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) B))
 449             (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) A)) ]@nil]
 450           with
 451           | RId  a               => let case_RId := tt    in ga_id _ _ _ _ _
 452           | RCanL  a             => let case_RCanL := tt  in ga_uncancell _ _ _ _ _
 453           | RCanR  a             => let case_RCanR := tt  in ga_uncancelr _ _ _ _ _
 454           | RuCanL a             => let case_RuCanL := tt in ga_cancell _ _ _ _ _
 455           | RuCanR a             => let case_RuCanR := tt in ga_cancelr _ _ _ _ _
 456           | RAssoc a b c         => let case_RAssoc := tt in ga_assoc _ _ _ _ _ _ _
 457           | RCossa a b c         => let case_RCossa := tt in ga_unassoc _ _ _ _ _ _ _
 458           | RExch  a b           => let case_RExch := tt  in ga_swap  _ _ _ _ _ _
 459           | RWeak  a             => let case_RWeak := tt  in ga_drop _ _ _ _ _
 460           | RCont  a             => let case_RCont := tt  in ga_copy  _ _ _ _ _
 461           | RLeft  a b c r'      => let case_RLeft := tt  in flatten _ _ r' ;; boost _ _ _ _ _ (ga_second _ _ _ _ _ _ _)
 462           | RRight a b c r'      => let case_RRight := tt in flatten _ _ r' ;; boost _ _ _ _ _ (ga_first  _ _ _ _ _ _ _)
 463           | RComp  c b a r1 r2   => let case_RComp := tt  in (fun r1' r2' => _) (flatten _ _ r1) (flatten _ _ r2)
 464         end); clear flatten; repeat take_simplify; repeat drop_simplify; intros.
 465
 466         destruct case_RComp.
 467           set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) a)) as a' in *.
 468           set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) b)) as b' in *.
 469           set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) c)) as c' in *.
 470           eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RCanL ].
 471           eapply nd_comp; [ idtac | eapply nd_rule; apply
 472              (@RLet Γ Δ [] [] (@ga_mk _ (v2t ec) a' b') (@ga_mk _ (v2t ec) a' c')) ].
 473           eapply nd_comp; [ apply nd_llecnac | idtac ].
 474           apply nd_prod.
 475           apply r2'.
 476           eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RuCanR ].
 477           eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RCanL ].
 478           eapply nd_comp; [ idtac | eapply nd_rule;  apply RLet ].
 479           eapply nd_comp; [ apply nd_llecnac | idtac ].
 480           eapply nd_prod.
 481           apply r1'.
 482           eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RExch ].
 483           apply ga_comp.
 484           Defined.
 485
 486   Definition flatten_arrangement :
 487     forall Γ (Δ:CoercionEnv Γ) n
 488       (ec:HaskTyVar Γ ECKind) (lev:HaskLevel Γ) (ant1 ant2:Tree ??(LeveledHaskType Γ ★)) (r:Arrange ant1 ant2) succ,
 489       ND Rule
 490       [Γ > Δ > mapOptionTree (flatten_leveled_type ) (drop_lev n ant1)
 491         |- [@ga_mk _ (v2t ec)
 492           (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) ant1))
 493           (mapOptionTree (flatten_type ) succ) ]@nil]
 494       [Γ > Δ > mapOptionTree (flatten_leveled_type ) (drop_lev n ant2)
 495         |- [@ga_mk _ (v2t ec)
 496           (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) ant2))
 497           (mapOptionTree (flatten_type ) succ) ]@nil].
 498       intros.
 499       refine ( _ ;; (boost _ _ _ _ _ (postcompose _ _ _ _ _ _ _ (flatten_arrangement' Γ Δ ec lev ant1 ant2 r)))).
 500       apply nd_rule.
 501       apply RArrange.
 502       refine ((fix flatten ant1 ant2 (r:Arrange ant1 ant2) :=
 503         match r as R in Arrange A B return
 504           Arrange (mapOptionTree (flatten_leveled_type ) (drop_lev _ A))
 505           (mapOptionTree (flatten_leveled_type ) (drop_lev _ B)) with
 506           | RId  a               => let case_RId := tt  in RId _
 507           | RCanL  a             => let case_RCanL := tt  in RCanL _
 508           | RCanR  a             => let case_RCanR := tt  in RCanR _
 509           | RuCanL a             => let case_RuCanL := tt in RuCanL _
 510           | RuCanR a             => let case_RuCanR := tt in RuCanR _
 511           | RAssoc a b c         => let case_RAssoc := tt in RAssoc _ _ _
 512           | RCossa a b c         => let case_RCossa := tt in RCossa _ _ _
 513           | RExch  a b           => let case_RExch := tt  in RExch _ _
 514           | RWeak  a             => let case_RWeak := tt  in RWeak _
 515           | RCont  a             => let case_RCont := tt  in RCont _
 516           | RLeft  a b c r'      => let case_RLeft := tt  in RLeft  _ (flatten _ _ r')
 517           | RRight a b c r'      => let case_RRight := tt in RRight _ (flatten _ _ r')
 518           | RComp  a b c r1 r2   => let case_RComp := tt  in RComp    (flatten _ _ r1) (flatten _ _ r2)
 519         end) ant1 ant2 r); clear flatten; repeat take_simplify; repeat drop_simplify; intros.
 520         Defined.
 521
 522   Definition flatten_arrangement'' :
 523     forall  Γ Δ ant1 ant2 succ l (r:Arrange ant1 ant2),
 524       ND Rule (mapOptionTree (flatten_judgment ) [Γ > Δ > ant1 |- succ @ l])
 525       (mapOptionTree (flatten_judgment ) [Γ > Δ > ant2 |- succ @ l]).
 526     intros.
 527     simpl.
 528     destruct l.
 529       apply nd_rule.
 530       apply RArrange.
 531       induction r; simpl.
 532         apply RId.
 533         apply RCanL.
 534         apply RCanR.
 535         apply RuCanL.
 536         apply RuCanR.
 537         apply RAssoc.
 538         apply RCossa.
 539         apply RExch.    (* TO DO: check for all-leaf trees here *)
 540         apply RWeak.
 541         apply RCont.
 542         apply RLeft; auto.
 543         apply RRight; auto.
 544         eapply RComp; [ apply IHr1 | apply IHr2 ].
 545
 546       apply flatten_arrangement.
 547         apply r.
 548         Defined.
 549
 550   Definition ga_join Γ Δ Σ₁ Σ₂ a b ec :
 551     ND Rule [] [Γ > Δ > Σ₁     |- [@ga_mk _ ec [] a      ]@nil] ->
 552     ND Rule [] [Γ > Δ > Σ₂     |- [@ga_mk _ ec [] b      ]@nil] ->
 553     ND Rule [] [Γ > Δ > Σ₁,,Σ₂ |- [@ga_mk _ ec [] (a,,b) ]@nil].
 554     intro pfa.
 555     intro pfb.
 556     apply secondify with (c:=a)  in pfb.
 557     apply firstify  with (c:=[])  in pfa.
 558     eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
 559     eapply nd_comp; [ eapply nd_llecnac | idtac ].
 560     apply nd_prod.
 561     apply pfa.
 562     clear pfa.
 563
 564     eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
 565     eapply nd_comp; [ apply nd_llecnac | idtac ].
 566     apply nd_prod.
 567     eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanL ].
 568     eapply nd_comp; [ idtac | eapply postcompose_ ].
 569     apply ga_uncancelr.
 570
 571     eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RExch ].
 572     eapply nd_comp; [ idtac | eapply precompose ].
 573     apply pfb.
 574     Defined.
 575
 576   Definition arrange_brak : forall Γ Δ ec succ t,
 577    ND Rule
 578      [Γ > Δ >
 579       [(@ga_mk _ (v2t ec) [] (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: nil) succ))) @@  nil],,
 580       mapOptionTree (flatten_leveled_type ) (drop_lev (ec :: nil) succ) |- [t]@nil]
 581      [Γ > Δ > mapOptionTree (flatten_leveled_type ) succ |- [t]@nil].
 582
 583     intros.
 584     unfold drop_lev.
 585     set (@arrange' _ succ (levelMatch (ec::nil))) as q.
 586     set (arrangeMap _ _ flatten_leveled_type q) as y.
 587     eapply nd_comp.
 588     Focus 2.
 589     eapply nd_rule.
 590     eapply RArrange.
 591     apply y.
 592     idtac.
 593     clear y q.
 594     eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RExch ].
 595     simpl.
 596     eapply nd_comp; [ apply nd_llecnac | idtac ].
 597     eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
 598     apply nd_prod.
 599     Focus 2.
 600     apply nd_id.
 601     idtac.
 602     induction succ; try destruct a; simpl.
 603     unfold take_lev.
 604     unfold mkTakeFlags.
 605     unfold mkFlags.
 606     unfold bnot.
 607     simpl.
 608     destruct l as [t' lev'].
 609     destruct lev' as [|ec' lev'].
 610     simpl.
 611     apply ga_id.
 612     unfold levelMatch.
 613     set (@eqd_dec (HaskLevel Γ) (haskLevelEqDecidable Γ) (ec' :: lev') (ec :: nil)) as q.
 614     destruct q.
 615     inversion e; subst.
 616     simpl.
 617     apply nd_rule.
 618     unfold flatten_leveled_type.
 619     simpl.
 620     unfold flatten_type.
 621     simpl.
 622     unfold ga_mk.
 623     simpl.
 624     apply RVar.
 625     simpl.
 626     apply ga_id.
 627     apply ga_id.
 628     unfold take_lev.
 629     simpl.
 630     apply ga_join.
 631       apply IHsucc1.
 632       apply IHsucc2.
 633     Defined.
 634
 635   Definition arrange_empty_tree : forall {T}{A}(q:Tree A)(t:Tree ??T),
 636     t = mapTree (fun _:A => None) q ->
 637     Arrange t [].
 638     intros T A q.
 639     induction q; intros.
 640       simpl in H.
 641       rewrite H.
 642       apply RId.
 643     simpl in *.
 644     destruct t; try destruct o; inversion H.
 645       set (IHq1 _ H1) as x1.
 646       set (IHq2 _ H2) as x2.
 647       eapply RComp.
 648         eapply RRight.
 649         rewrite <- H1.
 650         apply x1.
 651       eapply RComp.
 652         apply RCanL.
 653         rewrite <- H2.
 654         apply x2.
 655       Defined.
 656
 657 (*  Definition unarrange_empty_tree : forall {T}{A}(t:Tree ??T)(q:Tree A),
 658     t = mapTree (fun _:A => None) q ->
 659     Arrange [] t.
 660   Defined.*)
 661
 662   Definition decide_tree_empty : forall {T:Type}(t:Tree ??T),
 663     sum { q:Tree unit & t = mapTree (fun _ => None) q } unit.
 664     intro T.
 665     refine (fix foo t :=
 666       match t with
 667         | T_Leaf x => _
 668         | T_Branch b1 b2 => let b1' := foo b1 in let b2' := foo b2 in _
 669       end).
 670     intros.
 671     destruct x.
 672     right; apply tt.
 673     left.
 674       exists (T_Leaf tt).
 675       auto.
 676     destruct b1'.
 677     destruct b2'.
 678     destruct s.
 679     destruct s0.
 680     subst.
 681     left.
 682     exists (x,,x0).
 683     reflexivity.
 684     right; auto.
 685     right; auto.
 686     Defined.
 687
 688   Definition arrange_esc : forall Γ Δ ec succ t,
 689    ND Rule
 690      [Γ > Δ > mapOptionTree (flatten_leveled_type ) succ |- [t]@nil]
 691      [Γ > Δ >
 692       [(@ga_mk _ (v2t ec) [] (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: nil) succ))) @@  nil],,
 693       mapOptionTree (flatten_leveled_type ) (drop_lev (ec :: nil) succ)  |- [t]@nil].
 694     intros.
 695     set (@arrange _ succ (levelMatch (ec::nil))) as q.
 696     set (@drop_lev Γ (ec::nil) succ) as q'.
 697     assert (@drop_lev Γ (ec::nil) succ=q') as H.
 698       reflexivity.
 699     unfold drop_lev in H.
 700     unfold mkDropFlags in H.
 701     rewrite H in q.
 702     clear H.
 703     set (arrangeMap _ _ flatten_leveled_type q) as y.
 704     eapply nd_comp.
 705     eapply nd_rule.
 706     eapply RArrange.
 707     apply y.
 708     clear y q.
 709
 710     set (mapOptionTree flatten_leveled_type (dropT (mkFlags (liftBoolFunc false (bnot ○ levelMatch (ec :: nil))) succ))) as q.
 711     destruct (decide_tree_empty q); [ idtac | apply (Prelude_error "escapifying open code not yet supported") ].
 712     destruct s.
 713
 714     simpl.
 715     eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RExch ].
 716     set (fun z z' => @RLet Γ Δ z (mapOptionTree flatten_leveled_type q') t z' nil) as q''.
 717     eapply nd_comp; [ idtac | eapply nd_rule; apply RLet ].
 718     clear q''.
 719     eapply nd_comp; [ apply nd_rlecnac | idtac ].
 720     apply nd_prod.
 721     apply nd_rule.
 722     apply RArrange.
 723     eapply RComp; [ idtac | apply RCanR ].
 724     apply RLeft.
 725     apply (@arrange_empty_tree _ _ _ _ e).
 726
 727     eapply nd_comp.
 728       eapply nd_rule.
 729       eapply (@RVar Γ Δ t nil).
 730     apply nd_rule.
 731       apply RArrange.
 732       eapply RComp.
 733       apply RuCanR.
 734       apply RLeft.
 735       apply RWeak.
 736 (*
 737     eapply decide_tree_empty.
 738
 739     simpl.
 740     set (dropT (mkFlags (liftBoolFunc false (bnot ○ levelMatch (ec :: nil))) succ)) as escapified.
 741     destruct (decide_tree_empty escapified).
 742
 743     induction succ.
 744     destruct a.
 745       unfold drop_lev.
 746       destruct l.
 747       simpl.
 748       unfold mkDropFlags; simpl.
 749       unfold take_lev.
 750       unfold mkTakeFlags.
 751       simpl.
 752       destruct (General.list_eq_dec h0 (ec :: nil)).
 753         simpl.
 754         rewrite e.
 755         apply nd_id.
 756         simpl.
 757         apply nd_rule.
 758         apply RArrange.
 759         apply RLeft.
 760         apply RWeak.
 761       simpl.
 762         apply nd_rule.
 763         unfold take_lev.
 764         simpl.
 765         apply RArrange.
 766         apply RLeft.
 767         apply RWeak.
 768       apply (Prelude_error "escapifying code with multi-leaf antecedents is not supported").
 769 *)
 770       Defined.
 771
 772   Lemma mapOptionTree_distributes
 773     : forall T R (a b:Tree ??T) (f:T->R),
 774       mapOptionTree f (a,,b) = (mapOptionTree f a),,(mapOptionTree f b).
 775     reflexivity.
 776     Qed.
 777
 778   Lemma unlev_relev : forall {Γ}(t:Tree ??(HaskType Γ ★)) lev, mapOptionTree unlev (t @@@ lev) = t.
 779     intros.
 780     induction t.
 781     destruct a; reflexivity.
 782     rewrite <- IHt1 at 2.
 783     rewrite <- IHt2 at 2.
 784     reflexivity.
 785     Qed.
 786
 787   Lemma tree_of_nothing : forall Γ ec t,
 788     Arrange (mapOptionTree flatten_leveled_type (drop_lev(Γ:=Γ) (ec :: nil) (t @@@ (ec :: nil)))) [].
 789     intros.
 790     induction t; try destruct o; try destruct a.
 791     simpl.
 792     drop_simplify.
 793     simpl.
 794     apply RId.
 795     simpl.
 796     apply RId.
 797     eapply RComp; [ idtac | apply RCanL ].
 798     eapply RComp; [ idtac | eapply RLeft; apply IHt2 ].
 799     Opaque drop_lev.
 800     simpl.
 801     Transparent drop_lev.
 802     idtac.
 803     drop_simplify.
 804     apply RRight.
 805     apply IHt1.
 806     Defined.
 807
 808   Lemma tree_of_nothing' : forall Γ ec t,
 809     Arrange [] (mapOptionTree flatten_leveled_type (drop_lev(Γ:=Γ) (ec :: nil) (t @@@ (ec :: nil)))).
 810     intros.
 811     induction t; try destruct o; try destruct a.
 812     simpl.
 813     drop_simplify.
 814     simpl.
 815     apply RId.
 816     simpl.
 817     apply RId.
 818     eapply RComp; [ apply RuCanL | idtac ].
 819     eapply RComp; [ eapply RRight; apply IHt1 | idtac ].
 820     Opaque drop_lev.
 821     simpl.
 822     Transparent drop_lev.
 823     idtac.
 824     drop_simplify.
 825     apply RLeft.
 826     apply IHt2.
 827     Defined.
 828
 829   Lemma krunk : forall Γ (ec:HaskTyVar Γ ECKind) t,
 830     flatten_type (<[ ec |- t ]>)
 831     = @ga_mk Γ (v2t ec)
 832     (mapOptionTree flatten_type (take_arg_types_as_tree t))
 833     [ flatten_type (drop_arg_types_as_tree   t)].
 834     intros.
 835     unfold flatten_type at 1.
 836     simpl.
 837     unfold ga_mk.
 838     apply phoas_extensionality.
 839     intros.
 840     unfold v2t.
 841     unfold ga_mk_raw.
 842     unfold ga_mk_tree.
 843     rewrite <- mapOptionTree_compose.
 844     unfold take_arg_types_as_tree.
 845     simpl.
 846     replace (flatten_type (drop_arg_types_as_tree t) tv ite)
 847       with (drop_arg_types (flatten_rawtype (t tv ite))).
 848     replace (unleaves_ (take_arg_types (flatten_rawtype (t tv ite))))
 849       with ((mapOptionTree (fun x : HaskType Γ ★ => flatten_type x tv ite)
 850            (unleaves_
 851               (take_trustme (count_arg_types (t (fun _ : Kind => unit) (ite_unit Γ)))
 852                  (fun TV : Kind → Type => take_arg_types ○ t TV))))).
 853     reflexivity.
 854     unfold flatten_type.
 855     clear hetmet_flatten.
 856     clear hetmet_unflatten.
 857     clear hetmet_id.
 858     clear gar.
 859     set (t tv ite) as x.
 860     admit.
 861     admit.
 862     Qed.
 863
 864   Definition flatten_proof :
 865     forall  {h}{c},
 866       ND SRule h c ->
 867       ND  Rule (mapOptionTree (flatten_judgment ) h) (mapOptionTree (flatten_judgment ) c).
 868     intros.
 869     eapply nd_map'; [ idtac | apply X ].
 870     clear h c X.
 871     intros.
 872     simpl in *.
 873
 874     refine
 875       (match X as R in SRule H C with
 876       | SBrak    Γ Δ t ec succ lev           => let case_SBrak := tt         in _
 877       | SEsc     Γ Δ t ec succ lev           => let case_SEsc := tt          in _
 878       | SFlat    h c r                       => let case_SFlat := tt         in _
 879       end).
 880
 881     destruct case_SFlat.
 882     refine (match r as R in Rule H C with
 883       | RArrange Γ Δ a b x l d         => let case_RArrange := tt      in _
 884       | RNote    Γ Δ Σ τ l n           => let case_RNote := tt         in _
 885       | RLit     Γ Δ l     _           => let case_RLit := tt          in _
 886       | RVar     Γ Δ σ           lev   => let case_RVar := tt          in _
 887       | RGlobal  Γ Δ σ l wev           => let case_RGlobal := tt       in _
 888       | RLam     Γ Δ Σ tx te     lev   => let case_RLam := tt          in _
 889       | RCast    Γ Δ Σ σ τ lev γ       => let case_RCast := tt         in _
 890       | RAbsT    Γ Δ Σ κ σ lev         => let case_RAbsT := tt         in _
 891       | RAppT    Γ Δ Σ κ σ τ     lev   => let case_RAppT := tt         in _
 892       | RAppCo   Γ Δ Σ κ σ₁ σ₂ γ σ lev => let case_RAppCo := tt        in _
 893       | RAbsCo   Γ Δ Σ κ σ  σ₁ σ₂  lev => let case_RAbsCo := tt        in _
 894       | RApp     Γ Δ Σ₁ Σ₂ tx te lev   => let case_RApp := tt          in _
 895       | RLet     Γ Δ Σ₁ Σ₂ σ₁ σ₂ lev   => let case_RLet := tt          in _
 896       | RWhere   Γ Δ Σ₁ Σ₂ Σ₃ σ₁ σ₂ lev   => let case_RWhere := tt          in _
 897       | RJoin    Γ p lri m x q l       => let case_RJoin := tt in _
 898       | RVoid    _ _       l           => let case_RVoid := tt   in _
 899       | RBrak    Γ Δ t ec succ lev           => let case_RBrak := tt         in _
 900       | REsc     Γ Δ t ec succ lev           => let case_REsc := tt          in _
 901       | RCase    Γ Δ lev tc Σ avars tbranches alts => let case_RCase := tt         in _
 902       | RLetRec  Γ Δ lri x y t         => let case_RLetRec := tt       in _
 903       end); clear X h c.
 904
 905     destruct case_RArrange.
 906       apply (flatten_arrangement''  Γ Δ a b x _ d).
 907
 908     destruct case_RBrak.
 909       apply (Prelude_error "found unskolemized Brak rule; this shouldn't happen").
 910
 911     destruct case_REsc.
 912       apply (Prelude_error "found unskolemized Esc rule; this shouldn't happen").
 913
 914     destruct case_RNote.
 915       simpl.
 916       destruct l; simpl.
 917         apply nd_rule; apply RNote; auto.
 918         apply nd_rule; apply RNote; auto.
 919
 920     destruct case_RLit.
 921       simpl.
 922       destruct l0; simpl.
 923         unfold flatten_leveled_type.
 924         simpl.
 925         rewrite literal_types_unchanged.
 926           apply nd_rule; apply RLit.
 927         unfold take_lev; simpl.
 928         unfold drop_lev; simpl.
 929         simpl.
 930         rewrite literal_types_unchanged.
 931         apply ga_lit.
 932
 933     destruct case_RVar.
 934       Opaque flatten_judgment.
 935       simpl.
 936       Transparent flatten_judgment.
 937       idtac.
 938       unfold flatten_judgment.
 939       destruct lev.
 940       apply nd_rule. apply RVar.
 941       repeat drop_simplify.
 942       repeat take_simplify.
 943       simpl.
 944       apply ga_id.
 945
 946     destruct case_RGlobal.
 947       simpl.
 948       rename l into g.
 949       rename σ into l.
 950       destruct l as [|ec lev]; simpl.
 951         destruct (eqd_dec (g:CoreVar) (hetmet_flatten:CoreVar)).
 952           set (flatten_type (g wev)) as t.
 953           set (RGlobal _ Δ nil (mkGlobal Γ t hetmet_id)) as q.
 954           simpl in q.
 955           apply nd_rule.
 956           apply q.
 957           apply INil.
 958         destruct (eqd_dec (g:CoreVar) (hetmet_unflatten:CoreVar)).
 959           set (flatten_type (g wev)) as t.
 960           set (RGlobal _ Δ nil (mkGlobal Γ t hetmet_id)) as q.
 961           simpl in q.
 962           apply nd_rule.
 963           apply q.
 964           apply INil.
 965         unfold flatten_leveled_type. simpl.
 966           apply nd_rule; rewrite globals_do_not_have_code_types.
 967           apply RGlobal.
 968       apply (Prelude_error "found RGlobal at depth >0; globals should never appear inside code brackets unless escaped").
 969
 970     destruct case_RLam.
 971       Opaque drop_lev.
 972       Opaque take_lev.
 973       simpl.
 974       destruct lev as [|ec lev]; simpl; [ apply nd_rule; apply RLam; auto | idtac ].
 975       repeat drop_simplify.
 976       repeat take_simplify.
 977       eapply nd_comp.
 978         eapply nd_rule.
 979         eapply RArrange.
 980         simpl.
 981         apply RCanR.
 982       apply boost.
 983       simpl.
 984       apply ga_curry.
 985
 986     destruct case_RCast.
 987       simpl.
 988       destruct lev as [|ec lev]; simpl; [ apply nd_rule; apply RCast; auto | idtac ].
 989       simpl.
 990       apply flatten_coercion; auto.
 991       apply (Prelude_error "RCast at level >0; casting inside of code brackets is currently not supported").
 992
 993     destruct case_RJoin.
 994       simpl.
 995       destruct l;
 996         [ apply nd_rule; apply RJoin | idtac ];
 997         apply (Prelude_error "RJoin at depth >0").
 998
 999     destruct case_RApp.
1000       simpl.
1001
1002       destruct lev as [|ec lev].
1003         unfold flatten_type at 1.
1004         simpl.
1005         apply nd_rule.
1006         apply RApp.
1007
1008         repeat drop_simplify.
1009           repeat take_simplify.
1010           rewrite mapOptionTree_distributes.
1011           set (mapOptionTree (flatten_leveled_type ) (drop_lev (ec :: lev) Σ₁)) as Σ₁'.
1012           set (mapOptionTree (flatten_leveled_type ) (drop_lev (ec :: lev) Σ₂)) as Σ₂'.
1013           set (take_lev (ec :: lev) Σ₁) as Σ₁''.
1014           set (take_lev (ec :: lev) Σ₂) as Σ₂''.
1015           replace (flatten_type  (tx ---> te)) with ((flatten_type  tx) ---> (flatten_type  te)).
1016           apply (Prelude_error "FIXME: ga_apply").
1017           reflexivity.
1018
1019 (*
1020   Notation "`  x" := (take_lev _ x).
1021   Notation "`` x" := (mapOptionTree unlev x) (at level 20).
1022   Notation "``` x" := ((drop_lev _ x)) (at level 20).
1023   Notation "!<[]> x" := (flatten_type _ x) (at level 1).
1024   Notation "!<[@]> x" := (mapOptionTree flatten_leveled_type x) (at level 1).
1025 *)
1026
1027     destruct case_RLet.
1028       simpl.
1029       destruct lev as [|ec lev]; simpl; [ apply nd_rule; apply RLet; auto | idtac ].
1030       repeat drop_simplify.
1031       repeat take_simplify.
1032       simpl.
1033
1034       set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) Σ₁)) as Σ₁'.
1035       set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) Σ₂)) as Σ₂'.
1036       set (mapOptionTree flatten_leveled_type (drop_lev (ec :: lev) Σ₁)) as Σ₁''.
1037       set (mapOptionTree flatten_leveled_type (drop_lev (ec :: lev) Σ₂)) as Σ₂''.
1038
1039       eapply nd_comp.
1040       eapply nd_prod; [ idtac | apply nd_id ].
1041       eapply boost.
1042       apply (ga_first _ _ _ _ _ _ Σ₂').
1043
1044       eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
1045       apply nd_prod.
1046       apply nd_id.
1047       eapply nd_comp; [ eapply nd_rule; eapply RArrange; eapply RCanL | idtac ].
1048       eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RExch (* okay *)].
1049       apply precompose.
1050
1051     destruct case_RWhere.
1052       simpl.
1053       destruct lev as [|ec lev]; simpl; [ apply nd_rule; apply RWhere; auto | idtac ].
1054       repeat take_simplify.
1055       repeat drop_simplify.
1056       simpl.
1057
1058       set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) Σ₁)) as Σ₁'.
1059       set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) Σ₂)) as Σ₂'.
1060       set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) Σ₃)) as Σ₃'.
1061       set (mapOptionTree flatten_leveled_type (drop_lev (ec :: lev) Σ₁)) as Σ₁''.
1062       set (mapOptionTree flatten_leveled_type (drop_lev (ec :: lev) Σ₂)) as Σ₂''.
1063       set (mapOptionTree flatten_leveled_type (drop_lev (ec :: lev) Σ₃)) as Σ₃''.
1064
1065       eapply nd_comp.
1066       eapply nd_prod; [ eapply nd_id | idtac ].
1067       eapply (first_nd _ _ _ _ _ _ Σ₃').
1068       eapply nd_comp.
1069       eapply nd_prod; [ eapply nd_id | idtac ].
1070       eapply (second_nd _ _ _ _ _ _ Σ₁').
1071
1072       eapply nd_comp; [ idtac | eapply nd_rule; eapply RWhere ].
1073       apply nd_prod; [ idtac | apply nd_id ].
1074       eapply nd_comp; [ idtac | eapply precompose' ].
1075       apply nd_rule.
1076       apply RArrange.
1077       apply RLeft.
1078       apply RCanL.
1079
1080     destruct case_RVoid.
1081       simpl.
1082       apply nd_rule.
1083       destruct l.
1084       apply RVoid.
1085       apply (Prelude_error "RVoid at level >0").
1086
1087     destruct case_RAppT.
1088       simpl. destruct lev; simpl.
1089       unfold flatten_leveled_type.
1090       simpl.
1091       rewrite flatten_commutes_with_HaskTAll.
1092       rewrite flatten_commutes_with_substT.
1093       apply nd_rule.
1094       apply RAppT.
1095       apply Δ.
1096       apply Δ.
1097       apply (Prelude_error "found type application at level >0; this is not supported").
1098
1099     destruct case_RAbsT.
1100       simpl. destruct lev; simpl.
1101       rewrite flatten_commutes_with_HaskTAll.
1102       rewrite flatten_commutes_with_HaskTApp.
1103       eapply nd_comp; [ idtac | eapply nd_rule; eapply RAbsT ].
1104       simpl.
1105       set (mapOptionTree (flatten_leveled_type ) (mapOptionTree (weakLT(κ:=κ)) Σ)) as a.
1106       set (mapOptionTree (weakLT(κ:=κ)) (mapOptionTree (flatten_leveled_type ) Σ)) as q'.
1107       assert (a=q').
1108         unfold a.
1109         unfold q'.
1110         clear a q'.
1111         induction Σ.
1112           destruct a.
1113           simpl.
1114           rewrite flatten_commutes_with_weakLT.
1115           reflexivity.
1116           reflexivity.
1117           simpl.
1118           rewrite <- IHΣ1.
1119           rewrite <- IHΣ2.
1120           reflexivity.
1121       rewrite H.
1122       apply nd_id.
1123       apply Δ.
1124       apply Δ.
1125       apply (Prelude_error "found type abstraction at level >0; this is not supported").
1126
1127     destruct case_RAppCo.
1128       simpl. destruct lev; simpl.
1129       unfold flatten_type.
1130       simpl.
1131       apply nd_rule.
1132       apply RAppCo.
1133       apply flatten_coercion.
1134       apply γ.
1135       apply (Prelude_error "found coercion application at level >0; this is not supported").
1136
1137     destruct case_RAbsCo.
1138       simpl. destruct lev; simpl.
1139       unfold flatten_type.
1140       simpl.
1141       apply (Prelude_error "AbsCo not supported (FIXME)").
1142       apply (Prelude_error "found coercion abstraction at level >0; this is not supported").
1143
1144     destruct case_RLetRec.
1145       rename t into lev.
1146       simpl. destruct lev; simpl.
1147       apply nd_rule.
1148       set (@RLetRec Γ Δ (mapOptionTree flatten_leveled_type lri) (flatten_type x) (mapOptionTree flatten_type y) nil) as q.
1149       replace (mapOptionTree flatten_leveled_type (y @@@ nil)) with (mapOptionTree flatten_type y @@@ nil).
1150       apply q.
1151         induction y; try destruct a; auto.
1152         simpl.
1153         rewrite IHy1.
1154         rewrite IHy2.
1155         reflexivity.
1156       apply (Prelude_error "LetRec not supported inside brackets yet (FIXME)").
1157
1158     destruct case_RCase.
1159       simpl.
1160       apply (Prelude_error "Case not supported (BIG FIXME)").
1161
1162     destruct case_SBrak.
1163       simpl.
1164       destruct lev.
1165       drop_simplify.
1166       set (drop_lev (ec :: nil) (take_arg_types_as_tree t @@@ (ec :: nil))) as empty_tree.
1167       take_simplify.
1168       rewrite take_lemma'.
1169       simpl.
1170       rewrite mapOptionTree_compose.
1171       rewrite mapOptionTree_compose.
1172       rewrite unlev_relev.
1173       rewrite <- mapOptionTree_compose.
1174       simpl.
1175       rewrite krunk.
1176       set (mapOptionTree flatten_leveled_type (drop_lev (ec :: nil) succ)) as succ_host.
1177       set (mapOptionTree (flatten_type ○ unlev)(take_lev (ec :: nil) succ)) as succ_guest.
1178       set (mapOptionTree flatten_type (take_arg_types_as_tree t)) as succ_args.
1179       unfold empty_tree.
1180       eapply nd_comp; [ eapply nd_rule; eapply RArrange; eapply RLeft; apply tree_of_nothing | idtac ].
1181       eapply nd_comp; [ eapply nd_rule; eapply RArrange; eapply RCanR | idtac ].
1182       refine (ga_unkappa Γ Δ (v2t ec) nil _ _ _ _ ;; _).
1183       eapply nd_comp; [ idtac | eapply arrange_brak ].
1184       unfold succ_host.
1185       unfold succ_guest.
1186       eapply nd_rule.
1187         eapply RArrange.
1188         apply RExch.
1189       apply (Prelude_error "found Brak at depth >0 indicating 3-level code; only two-level code is currently supported").
1190
1191     destruct case_SEsc.
1192       simpl.
1193       destruct lev.
1194       simpl.
1195       unfold flatten_leveled_type at 2.
1196       simpl.
1197       rewrite krunk.
1198       rewrite mapOptionTree_compose.
1199       take_simplify.
1200       drop_simplify.
1201       simpl.
1202       eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RLeft; apply tree_of_nothing' ].
1203       eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanR ].
1204       simpl.
1205       rewrite take_lemma'.
1206       rewrite unlev_relev.
1207       rewrite <- mapOptionTree_compose.
1208       eapply nd_comp; [ apply (arrange_esc _ _ ec) | idtac ].
1209
1210       set (decide_tree_empty (take_lev (ec :: nil) succ)) as q'.
1211       destruct q'.
1212       destruct s.
1213       rewrite e.
1214       clear e.
1215
1216       set (mapOptionTree flatten_leveled_type (drop_lev (ec :: nil) succ)) as succ_host.
1217       set (mapOptionTree flatten_type (take_arg_types_as_tree t)) as succ_args.
1218
1219       eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RuCanR ].
1220       eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RuCanR ].
1221       eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RCanL ].
1222       eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
1223       eapply nd_comp; [ apply nd_llecnac | idtac ].
1224       apply nd_prod; [ idtac | eapply boost ].
1225       induction x.
1226         apply ga_id.
1227         eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanL ].
1228         simpl.
1229         apply ga_join.
1230           apply IHx1.
1231           apply IHx2.
1232           simpl.
1233           apply postcompose.
1234
1235       refine ( _ ;; (boost _ _ _ _ _ (postcompose _ _ _ _ _ _ _ _))).
1236       apply ga_cancell.
1237       apply firstify.
1238
1239       induction x.
1240         destruct a; simpl.
1241         apply ga_id.
1242         simpl.
1243         refine ( _ ;; (boost _ _ _ _ _ (postcompose _ _ _ _ _ _ _ _))).
1244         apply ga_cancell.
1245         refine ( _ ;; (boost _ _ _ _ _ (postcompose _ _ _ _ _ _ _ _))).
1246         eapply firstify.
1247         apply IHx1.
1248         apply secondify.
1249         apply IHx2.
1250
1251       (* environment has non-empty leaves *)
1252       apply (Prelude_error "ga_kappa not supported yet (BIG FIXME)").
1253
1254       (* nesting too deep *)
1255       apply (Prelude_error "found Esc at depth >0 indicating 3-level code; only two-level code is currently supported").
1256       Defined.
1257
1258   Definition skolemize_and_flatten_proof :
1259     forall  {h}{c},
1260       ND  Rule h c ->
1261       ND  Rule
1262            (mapOptionTree (flatten_judgment ○ skolemize_judgment) h)
1263            (mapOptionTree (flatten_judgment ○ skolemize_judgment) c).
1264     intros.
1265     rewrite mapOptionTree_compose.
1266     rewrite mapOptionTree_compose.
1267     apply flatten_proof.
1268     apply skolemize_proof.
1269     apply X.
1270     Defined.
1271
1272
1273   (* to do: establish some metric on judgments (max length of level of any succedent type, probably), show how to
1274    * calculate it, and show that the flattening procedure above drives it down by one *)
1275
1276   (*
1277   Instance FlatteningFunctor {Γ}{Δ}{ec} : Functor (JudgmentsL (PCF Γ Δ ec)) (TypesL (SystemFCa Γ Δ)) (obact) :=
1278     { fmor := FlatteningFunctor_fmor }.
1279
1280   Definition ReificationFunctor Γ Δ : Functor (JudgmentsL _ _ (PCF n Γ Δ)) SystemFCa' (mapOptionTree brakifyJudg).
1281     refine {| fmor := ReificationFunctor_fmor Γ Δ |}; unfold hom; unfold ob; simpl ; intros.
1282
1283   Definition PCF_SMME (n:nat)(Γ:TypeEnv)(Δ:CoercionEnv Γ) : ProgrammingLanguageSMME.
1284     refine {| plsmme_pl := PCF n Γ Δ |}.
1285     Defined.
1286
1287   Definition SystemFCa_SMME (n:nat)(Γ:TypeEnv)(Δ:CoercionEnv Γ) : ProgrammingLanguageSMME.
1288     refine {| plsmme_pl := SystemFCa n Γ Δ |}.
1289     Defined.
1290
1291   Definition ReificationFunctorMonoidal n : MonoidalFunctor (JudgmentsN n) (JudgmentsN (S n)) (ReificationFunctor n).
1292     Defined.
1293
1294   (* 5.1.4 *)
1295   Definition PCF_SystemFCa_two_level n Γ Δ : TwoLevelLanguage (PCF_SMME n Γ Δ) (SystemFCa_SMME (S n) Γ Δ).
1296     Defined.
1297   *)
1298   (*  ... and the retraction exists *)
1299
1300 End HaskFlattener.
1301
1302 Implicit Arguments garrow [ ].