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 Open Scope nd_scope.
  34 Set Printing Width 130.
  35
  36 (*
  37  *  The flattening transformation.  Currently only TWO-level languages are
  38  *  supported, and the level-1 sublanguage is rather limited.
  39  *
  40  *  This file abuses terminology pretty badly.  For purposes of this file,
  41  *  "PCF" means "the level-1 sublanguage" and "FC" (aka System FC) means
  42  *  the whole language (level-0 language including bracketed level-1 terms)
  43  *)
  44 Section HaskFlattener.
  45
  46   Definition arrange :
  47     forall {T} (Σ:Tree ??T) (f:T -> bool),
  48       Arrange Σ (dropT (mkFlags (liftBoolFunc false f) Σ),,( (dropT (mkFlags (liftBoolFunc false (bnot ○ f)) Σ)))).
  49     intros.
  50     induction Σ.
  51       simpl.
  52       destruct a.
  53       simpl.
  54       destruct (f t); simpl.
  55       apply RuCanL.
  56       apply RuCanR.
  57       simpl.
  58       apply RuCanL.
  59       simpl in *.
  60       eapply RComp; [ idtac | apply arrangeSwapMiddle ].
  61       eapply RComp.
  62       eapply RLeft.
  63       apply IHΣ2.
  64       eapply RRight.
  65       apply IHΣ1.
  66       Defined.
  67
  68   Definition arrange' :
  69     forall {T} (Σ:Tree ??T) (f:T -> bool),
  70       Arrange (dropT (mkFlags (liftBoolFunc false f) Σ),,( (dropT (mkFlags (liftBoolFunc false (bnot ○ f)) Σ)))) Σ.
  71     intros.
  72     induction Σ.
  73       simpl.
  74       destruct a.
  75       simpl.
  76       destruct (f t); simpl.
  77       apply RCanL.
  78       apply RCanR.
  79       simpl.
  80       apply RCanL.
  81       simpl in *.
  82       eapply RComp; [ apply arrangeSwapMiddle | idtac ].
  83       eapply RComp.
  84       eapply RLeft.
  85       apply IHΣ2.
  86       eapply RRight.
  87       apply IHΣ1.
  88       Defined.
  89
  90   Ltac eqd_dec_refl' :=
  91     match goal with
  92       | [ |- context[@eqd_dec ?T ?V ?X ?X] ] =>
  93         destruct (@eqd_dec T V X X) as [eqd_dec1 | eqd_dec2];
  94           [ clear eqd_dec1 | set (eqd_dec2 (refl_equal _)) as eqd_dec2'; inversion eqd_dec2' ]
  95   end.
  96
  97   Definition v2t {Γ}(ec:HaskTyVar Γ ECKind) : HaskType Γ ECKind := fun TV ite => TVar (ec TV ite).
  98
  99   Definition levelMatch {Γ}(lev:HaskLevel Γ) : LeveledHaskType Γ ★ -> bool :=
 100     fun t => match t with ttype@@tlev => if eqd_dec tlev lev then true else false end.
 101
 102   (* In a tree of types, replace any type at depth "lev" or greater None *)
 103   Definition mkDropFlags {Γ}(lev:HaskLevel Γ)(tt:Tree ??(LeveledHaskType Γ ★)) : TreeFlags tt :=
 104     mkFlags (liftBoolFunc false (levelMatch lev)) tt.
 105
 106   Definition drop_lev {Γ}(lev:HaskLevel Γ)(tt:Tree ??(LeveledHaskType Γ ★)) : Tree ??(LeveledHaskType Γ ★) :=
 107     dropT (mkDropFlags lev tt).
 108
 109   (* The opposite: replace any type which is NOT at level "lev" with None *)
 110   Definition mkTakeFlags {Γ}(lev:HaskLevel Γ)(tt:Tree ??(LeveledHaskType Γ ★)) : TreeFlags tt :=
 111     mkFlags (liftBoolFunc true (bnot ○ levelMatch lev)) tt.
 112
 113   Definition take_lev {Γ}(lev:HaskLevel Γ)(tt:Tree ??(LeveledHaskType Γ ★)) : Tree ??(LeveledHaskType Γ ★) :=
 114     dropT (mkTakeFlags lev tt).
 115 (*
 116     mapOptionTree (fun x => flatten_type (unlev x))
 117     (maybeTree (takeT tt (mkFlags (
 118       fun t => match t with
 119                  | Some (ttype @@ tlev) => if eqd_dec tlev lev then true else false
 120                  | _                    => true
 121                end
 122     ) tt))).
 123
 124   Definition maybeTree {T}(t:??(Tree ??T)) : Tree ??T :=
 125     match t with
 126       | None   => []
 127       | Some x => x
 128     end.
 129 *)
 130
 131   Lemma drop_lev_lemma : forall Γ (lev:HaskLevel Γ) x, drop_lev lev [x @@  lev] = [].
 132     intros; simpl.
 133     Opaque eqd_dec.
 134     unfold drop_lev.
 135     simpl.
 136     unfold mkDropFlags.
 137     simpl.
 138     Transparent eqd_dec.
 139     eqd_dec_refl'.
 140     auto.
 141     Qed.
 142
 143   Lemma drop_lev_lemma_s : forall Γ (lev:HaskLevel Γ) ec x, drop_lev (ec::lev) [x @@  (ec :: lev)] = [].
 144     intros; simpl.
 145     Opaque eqd_dec.
 146     unfold drop_lev.
 147     unfold mkDropFlags.
 148     simpl.
 149     Transparent eqd_dec.
 150     eqd_dec_refl'.
 151     auto.
 152     Qed.
 153
 154   Lemma take_lemma : forall Γ (lev:HaskLevel Γ) x, take_lev lev [x @@  lev] = [x @@ lev].
 155     intros; simpl.
 156     Opaque eqd_dec.
 157     unfold take_lev.
 158     unfold mkTakeFlags.
 159     simpl.
 160     Transparent eqd_dec.
 161     eqd_dec_refl'.
 162     auto.
 163     Qed.
 164
 165   Ltac drop_simplify :=
 166     match goal with
 167       | [ |- context[@drop_lev ?G ?L [ ?X @@ ?L ] ] ] =>
 168         rewrite (drop_lev_lemma G L X)
 169       | [ |- context[@drop_lev ?G (?E :: ?L) [ ?X @@ (?E :: ?L) ] ] ] =>
 170         rewrite (drop_lev_lemma_s G L E X)
 171       | [ |- context[@drop_lev ?G ?N (?A,,?B)] ] =>
 172       change (@drop_lev G N (A,,B)) with ((@drop_lev G N A),,(@drop_lev G N B))
 173       | [ |- context[@drop_lev ?G ?N (T_Leaf None)] ] =>
 174       change (@drop_lev G N (T_Leaf (@None (LeveledHaskType G ★)))) with (T_Leaf (@None (LeveledHaskType G ★)))
 175     end.
 176
 177   Ltac take_simplify :=
 178     match goal with
 179       | [ |- context[@take_lev ?G ?L [ ?X @@ ?L ] ] ] =>
 180         rewrite (take_lemma G L X)
 181       | [ |- context[@take_lev ?G ?N (?A,,?B)] ] =>
 182       change (@take_lev G N (A,,B)) with ((@take_lev G N A),,(@take_lev G N B))
 183       | [ |- context[@take_lev ?G ?N (T_Leaf None)] ] =>
 184       change (@take_lev G N (T_Leaf (@None (LeveledHaskType G ★)))) with (T_Leaf (@None (LeveledHaskType G ★)))
 185     end.
 186
 187
 188   (*******************************************************************************)
 189
 190
 191   Context (hetmet_flatten : WeakExprVar).
 192   Context (hetmet_unflatten : WeakExprVar).
 193   Context (hetmet_id      : WeakExprVar).
 194   Context {unitTy : forall TV, RawHaskType TV ECKind  -> RawHaskType TV ★                                          }.
 195   Context {prodTy : forall TV, RawHaskType TV ECKind  -> RawHaskType TV ★  -> RawHaskType TV ★ -> RawHaskType TV ★ }.
 196   Context {gaTy   : forall TV, RawHaskType TV ECKind  -> RawHaskType TV ★ -> RawHaskType TV ★  -> RawHaskType TV ★ }.
 197
 198   Definition ga_mk_tree {Γ}(ec:HaskType Γ ECKind)(tr:Tree ??(HaskType Γ ★)) : HaskType Γ ★ :=
 199     fun TV ite => reduceTree (unitTy TV (ec TV ite)) (prodTy TV (ec TV ite)) (mapOptionTree (fun x => x TV ite) tr).
 200
 201   Definition ga_mk {Γ}(ec:HaskType Γ ECKind )(ant suc:Tree ??(HaskType Γ ★)) : HaskType Γ ★ :=
 202     fun TV ite => gaTy TV (ec TV ite) (ga_mk_tree ec ant TV ite) (ga_mk_tree ec suc TV ite).
 203
 204   (*
 205    *  The story:
 206    *    - code types <[t]>@c                                                become garrows  c () t
 207    *    - free variables of type t at a level lev deeper than the succedent become garrows  c () t
 208    *    - free variables at the level of the succedent become
 209    *)
 210   Fixpoint flatten_rawtype {TV}{κ}(exp: RawHaskType TV κ) : RawHaskType TV κ :=
 211     match exp with
 212     | TVar    _  x          => TVar x
 213     | TAll     _ y          => TAll   _  (fun v => flatten_rawtype (y v))
 214     | TApp   _ _ x y        => TApp      (flatten_rawtype x) (flatten_rawtype y)
 215     | TCon       tc         => TCon      tc
 216     | TCoerc _ t1 t2 t      => TCoerc    (flatten_rawtype t1) (flatten_rawtype t2) (flatten_rawtype t)
 217     | TArrow                => TArrow
 218     | TCode      v e        => gaTy TV v (unitTy TV v) (flatten_rawtype 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 =>
 229       flatten_rawtype (ht TV ite).
 230
 231   Fixpoint flatten_leveled_type' {Γ}(ht:HaskType Γ ★)(lev:HaskLevel Γ) : HaskType Γ ★ :=
 232     match lev with
 233       | nil      => flatten_type ht
 234       | ec::lev' => @ga_mk _ (v2t ec) [] [flatten_leveled_type' ht lev']
 235     end.
 236
 237   Definition flatten_leveled_type {Γ}(ht:LeveledHaskType Γ ★) : LeveledHaskType Γ ★ :=
 238     match ht with
 239       htt @@ lev =>
 240       flatten_leveled_type' htt lev @@ nil
 241     end.
 242
 243   (* AXIOMS *)
 244
 245   Axiom literal_types_unchanged : forall Γ l, flatten_type (literalType l) = literalType(Γ:=Γ) l.
 246
 247   Axiom flatten_coercion : forall Γ Δ κ (σ τ:HaskType Γ κ) (γ:HaskCoercion Γ Δ (σ ∼∼∼ τ)),
 248     HaskCoercion Γ Δ (flatten_type σ ∼∼∼ flatten_type τ).
 249
 250   Axiom flatten_commutes_with_substT :
 251     forall  κ Γ (Δ:CoercionEnv Γ) (σ:∀ TV, InstantiatedTypeEnv TV Γ → TV κ → RawHaskType TV ★) (τ:HaskType Γ κ),
 252     flatten_type  (substT σ τ) = substT (fun TV ite v => flatten_rawtype  (σ TV ite v))
 253       (flatten_type  τ).
 254
 255   Axiom flatten_commutes_with_HaskTAll :
 256     forall  κ Γ (Δ:CoercionEnv Γ) (σ:∀ TV, InstantiatedTypeEnv TV Γ → TV κ → RawHaskType TV ★),
 257     flatten_type  (HaskTAll κ σ) = HaskTAll κ (fun TV ite v => flatten_rawtype (σ TV ite v)).
 258
 259   Axiom flatten_commutes_with_HaskTApp :
 260     forall  κ Γ (Δ:CoercionEnv Γ) (σ:∀ TV, InstantiatedTypeEnv TV Γ → TV κ → RawHaskType TV ★),
 261     flatten_type  (HaskTApp (weakF σ) (FreshHaskTyVar κ)) =
 262     HaskTApp (weakF (fun TV ite v => flatten_rawtype  (σ TV ite v))) (FreshHaskTyVar κ).
 263
 264   Axiom flatten_commutes_with_weakLT : forall (Γ:TypeEnv) κ  t,
 265     flatten_leveled_type  (weakLT(Γ:=Γ)(κ:=κ) t) = weakLT(Γ:=Γ)(κ:=κ) (flatten_leveled_type  t).
 266
 267   Axiom globals_do_not_have_code_types : forall (Γ:TypeEnv) (g:Global Γ) v,
 268     flatten_type (g v) = g v.
 269
 270   (* This tries to assign a single level to the entire succedent of a judgment.  If the succedent has types from different
 271    * levels (should not happen) it just picks one; if the succedent has no non-None leaves (also should not happen) it
 272    * picks nil *)
 273   Definition getΓ (j:Judg) := match j with Γ > _ > _ |- _ => Γ end.
 274   Definition getSuc (j:Judg) : Tree ??(LeveledHaskType (getΓ j) ★) :=
 275     match j as J return Tree ??(LeveledHaskType (getΓ J) ★) with Γ > _ > _ |- s => s end.
 276   Fixpoint getjlev {Γ}(tt:Tree ??(LeveledHaskType Γ ★)) : HaskLevel Γ :=
 277     match tt with
 278       | T_Leaf None              => nil
 279       | T_Leaf (Some (_ @@ lev)) => lev
 280       | T_Branch b1 b2 =>
 281         match getjlev b1 with
 282           | nil => getjlev b2
 283           | lev => lev
 284         end
 285     end.
 286
 287   (* "n" is the maximum depth remaining AFTER flattening *)
 288   Definition flatten_judgment (j:Judg) :=
 289     match j as J return Judg with
 290       Γ > Δ > ant |- suc =>
 291         match getjlev suc with
 292           | nil        => Γ > Δ > mapOptionTree flatten_leveled_type ant
 293                                |- mapOptionTree flatten_leveled_type suc
 294
 295           | (ec::lev') => Γ > Δ > mapOptionTree flatten_leveled_type (drop_lev (ec::lev') ant)
 296                                |- [ga_mk (v2t ec)
 297                                          (mapOptionTree (flatten_type ○ unlev) (take_lev (ec::lev') ant))
 298                                          (mapOptionTree (flatten_type ○ unlev)                      suc )
 299                                          @@ nil]  (* we know the level of all of suc *)
 300         end
 301     end.
 302
 303   Class garrow :=
 304   { ga_id        : ∀ Γ Δ ec l a    , ND Rule [] [Γ > Δ >                          [] |- [@ga_mk Γ ec a a @@ l] ]
 305   ; ga_cancelr   : ∀ Γ Δ ec l a    , ND Rule [] [Γ > Δ >                          [] |- [@ga_mk Γ ec (a,,[]) a @@ l] ]
 306   ; ga_cancell   : ∀ Γ Δ ec l a    , ND Rule [] [Γ > Δ >                          [] |- [@ga_mk Γ ec ([],,a) a @@ l] ]
 307   ; ga_uncancelr : ∀ Γ Δ ec l a    , ND Rule [] [Γ > Δ >                          [] |- [@ga_mk Γ ec a (a,,[]) @@ l] ]
 308   ; ga_uncancell : ∀ Γ Δ ec l a    , ND Rule [] [Γ > Δ >                          [] |- [@ga_mk Γ ec a ([],,a) @@ l] ]
 309   ; ga_assoc     : ∀ Γ Δ ec l a b c, ND Rule [] [Γ > Δ >                          [] |- [@ga_mk Γ ec ((a,,b),,c) (a,,(b,,c)) @@ l] ]
 310   ; ga_unassoc   : ∀ Γ Δ ec l a b c, ND Rule [] [Γ > Δ >                          [] |- [@ga_mk Γ ec (a,,(b,,c)) ((a,,b),,c) @@ l] ]
 311   ; ga_swap      : ∀ Γ Δ ec l a b  , ND Rule [] [Γ > Δ >                          [] |- [@ga_mk Γ ec (a,,b) (b,,a) @@ l] ]
 312   ; ga_drop      : ∀ Γ Δ ec l a    , ND Rule [] [Γ > Δ >                          [] |- [@ga_mk Γ ec a [] @@ l] ]
 313   ; ga_copy      : ∀ Γ Δ ec l a    , ND Rule [] [Γ > Δ >                          [] |- [@ga_mk Γ ec a (a,,a) @@ l] ]
 314   ; ga_first     : ∀ Γ Δ ec l a b x, ND Rule [] [Γ > Δ >      [@ga_mk Γ ec a b @@ l] |- [@ga_mk Γ ec (a,,x) (b,,x) @@ l] ]
 315   ; ga_second    : ∀ Γ Δ ec l a b x, ND Rule [] [Γ > Δ >      [@ga_mk Γ ec a b @@ l] |- [@ga_mk Γ ec (x,,a) (x,,b) @@ l] ]
 316   ; ga_lit       : ∀ Γ Δ ec l lit  , ND Rule [] [Γ > Δ >                          [] |- [@ga_mk Γ ec [] [literalType lit] @@ l] ]
 317   ; ga_curry     : ∀ Γ Δ ec l a b c, ND Rule [] [Γ > Δ > [@ga_mk Γ ec (a,,[b]) [c] @@ l] |- [@ga_mk Γ ec a [b ---> c] @@ l] ]
 318   ; 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] ]
 319   ; ga_apply     : ∀ Γ Δ ec l a a' b c,
 320                  ND Rule [] [Γ > Δ > [@ga_mk Γ ec a [b ---> c] @@ l],,[@ga_mk Γ ec a' [b] @@ l] |- [@ga_mk Γ ec (a,,a') [c] @@ l] ]
 321   ; ga_kappa     : ∀ Γ Δ ec l a b Σ, ND Rule
 322   [Γ > Δ > Σ,,[@ga_mk Γ ec [] a @@ l] |- [@ga_mk Γ ec [] b @@ l] ]
 323   [Γ > Δ > Σ          |- [@ga_mk Γ ec a  b @@ l] ]
 324   }.
 325   Context `(gar:garrow).
 326
 327   Notation "a ~~~~> b" := (@ga_mk _ _ a b) (at level 20).
 328
 329   Definition boost : forall Γ Δ ant x y {lev},
 330     ND Rule []                          [ Γ > Δ > [x@@lev] |- [y@@lev] ] ->
 331     ND Rule [ Γ > Δ > ant |- [x@@lev] ] [ Γ > Δ > ant      |- [y@@lev] ].
 332     intros.
 333     eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanL ].
 334     eapply nd_comp; [ idtac | eapply nd_rule; apply (@RLet Γ Δ [] ant y x lev) ].
 335     eapply nd_comp; [ apply nd_rlecnac | idtac ].
 336     apply nd_prod.
 337     apply nd_id.
 338     eapply nd_comp.
 339       apply X.
 340       eapply nd_rule.
 341       eapply RArrange.
 342       apply RuCanL.
 343       Defined.
 344
 345   Definition postcompose' : ∀ Γ Δ ec lev a b c Σ,
 346      ND Rule [] [ Γ > Δ > Σ                        |- [@ga_mk Γ ec a b @@ lev] ] ->
 347      ND Rule [] [ Γ > Δ > Σ,,[@ga_mk Γ ec b c @@ lev] |- [@ga_mk Γ ec a c @@ lev] ].
 348      intros.
 349      eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RExch ].
 350      eapply nd_comp; [ idtac
 351        | eapply nd_rule; apply (@RLet Γ Δ [@ga_mk _ ec b c @@lev] Σ (@ga_mk _ ec a c) (@ga_mk _ ec a b) lev) ].
 352      eapply nd_comp; [ apply nd_llecnac | idtac ].
 353      apply nd_prod.
 354      apply X.
 355      eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RExch ].
 356      apply ga_comp.
 357      Defined.
 358
 359   Definition precompose Γ Δ ec : forall a x y z lev,
 360     ND Rule
 361       [ Γ > Δ > a                           |- [@ga_mk _ ec y z @@ lev] ]
 362       [ Γ > Δ > a,,[@ga_mk _ ec x y @@ lev] |- [@ga_mk _ ec x z @@ lev] ].
 363     intros.
 364     eapply nd_comp.
 365     apply nd_rlecnac.
 366     eapply nd_comp.
 367     eapply nd_prod.
 368     apply nd_id.
 369     eapply ga_comp.
 370
 371     eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RExch ].
 372
 373     apply nd_rule.
 374     apply RLet.
 375     Defined.
 376
 377   Definition precompose' : ∀ Γ Δ ec lev a b c Σ,
 378      ND Rule [] [ Γ > Δ > Σ                           |- [@ga_mk Γ ec b c @@ lev] ] ->
 379      ND Rule [] [ Γ > Δ > Σ,,[@ga_mk Γ ec a b @@ lev] |- [@ga_mk Γ ec a c @@ lev] ].
 380      intros.
 381      eapply nd_comp.
 382      apply X.
 383      apply precompose.
 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.
 391      apply postcompose'.
 392      apply X.
 393      apply nd_rule.
 394      apply RArrange.
 395      apply RCanL.
 396      Defined.
 397
 398   Definition firstify : ∀ Γ Δ ec lev a b c Σ,
 399     ND Rule [] [ Γ > Δ > Σ                     |- [@ga_mk Γ ec a b @@ lev] ] ->
 400     ND Rule [] [ Γ > Δ > Σ                    |- [@ga_mk Γ ec (a,,c) (b,,c) @@ lev] ].
 401     intros.
 402     eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanL ].
 403     eapply nd_comp; [ idtac | eapply nd_rule; apply RLet ].
 404     eapply nd_comp; [ apply nd_llecnac | idtac ].
 405     apply nd_prod.
 406     apply X.
 407     eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RuCanL ].
 408     apply ga_first.
 409     Defined.
 410
 411   Definition secondify : ∀ Γ Δ ec lev a b c Σ,
 412      ND Rule [] [ Γ > Δ > Σ                    |- [@ga_mk Γ ec a b @@ lev] ] ->
 413      ND Rule [] [ Γ > Δ > Σ                    |- [@ga_mk Γ ec (c,,a) (c,,b) @@ lev] ].
 414     intros.
 415     eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanL ].
 416     eapply nd_comp; [ idtac | eapply nd_rule; apply RLet ].
 417     eapply nd_comp; [ apply nd_llecnac | idtac ].
 418     apply nd_prod.
 419     apply X.
 420     eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RuCanL ].
 421     apply ga_second.
 422     Defined.
 423
 424   Lemma ga_unkappa     : ∀ Γ Δ ec l a b Σ,
 425     ND Rule
 426     [Γ > Δ > Σ |- [@ga_mk Γ ec a  b @@ l] ]
 427     [Γ > Δ > Σ,,[@ga_mk Γ ec [] a @@ l] |- [@ga_mk Γ ec [] b @@ l] ].
 428     intros.
 429     set (ga_comp Γ Δ ec l [] a b) as q.
 430
 431     set (@RLet Γ Δ) as q'.
 432     set (@RLet Γ Δ [@ga_mk _ ec [] a @@ l] Σ (@ga_mk _ ec [] b) (@ga_mk _ ec a b) l) as q''.
 433     eapply nd_comp.
 434     Focus 2.
 435     eapply nd_rule.
 436     eapply RArrange.
 437     apply RExch.
 438
 439     eapply nd_comp.
 440     Focus 2.
 441     eapply nd_rule.
 442     apply q''.
 443
 444     idtac.
 445     clear q'' q'.
 446     eapply nd_comp.
 447     apply nd_rlecnac.
 448     apply nd_prod.
 449     apply nd_id.
 450     apply q.
 451     Defined.
 452
 453   (* useful for cutting down on the pretty-printed noise
 454
 455   Notation "`  x" := (take_lev _ x) (at level 20).
 456   Notation "`` x" := (mapOptionTree unlev x) (at level 20).
 457   Notation "``` x" := (drop_lev _ x) (at level 20).
 458   *)
 459   Definition flatten_arrangement' :
 460     forall Γ (Δ:CoercionEnv Γ)
 461       (ec:HaskTyVar Γ ECKind) (lev:HaskLevel Γ) (ant1 ant2:Tree ??(LeveledHaskType Γ ★)) (r:Arrange ant1 ant2),
 462       ND Rule [] [Γ > Δ > [] |- [@ga_mk _ (v2t ec) (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) ant2))
 463         (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) ant1)) @@ nil] ].
 464
 465       intros Γ Δ ec lev.
 466       refine (fix flatten ant1 ant2 (r:Arrange ant1 ant2):
 467            ND Rule [] [Γ > Δ > [] |- [@ga_mk _ (v2t ec)
 468              (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) ant2))
 469              (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) ant1)) @@ nil]] :=
 470         match r as R in Arrange A B return
 471           ND Rule [] [Γ > Δ > [] |- [@ga_mk _ (v2t ec)
 472             (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) B))
 473             (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) A)) @@ nil]]
 474           with
 475           | RCanL  a             => let case_RCanL := tt  in ga_uncancell _ _ _ _ _
 476           | RCanR  a             => let case_RCanR := tt  in ga_uncancelr _ _ _ _ _
 477           | RuCanL a             => let case_RuCanL := tt in ga_cancell _ _ _ _ _
 478           | RuCanR a             => let case_RuCanR := tt in ga_cancelr _ _ _ _ _
 479           | RAssoc a b c         => let case_RAssoc := tt in ga_assoc _ _ _ _ _ _ _
 480           | RCossa a b c         => let case_RCossa := tt in ga_unassoc _ _ _ _ _ _ _
 481           | RExch  a b           => let case_RExch := tt  in ga_swap  _ _ _ _ _ _
 482           | RWeak  a             => let case_RWeak := tt  in ga_drop _ _ _ _ _
 483           | RCont  a             => let case_RCont := tt  in ga_copy  _ _ _ _ _
 484           | RLeft  a b c r'      => let case_RLeft := tt  in flatten _ _ r' ;; boost _ _ _ _ _ (ga_second _ _ _ _ _ _ _)
 485           | RRight a b c r'      => let case_RRight := tt in flatten _ _ r' ;; boost _ _ _ _ _ (ga_first  _ _ _ _ _ _ _)
 486           | RComp  c b a r1 r2   => let case_RComp := tt  in (fun r1' r2' => _) (flatten _ _ r1) (flatten _ _ r2)
 487         end); clear flatten; repeat take_simplify; repeat drop_simplify; intros.
 488
 489         destruct case_RComp.
 490           set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) a)) as a' in *.
 491           set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) b)) as b' in *.
 492           set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) c)) as c' in *.
 493           eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RCanL ].
 494           eapply nd_comp; [ idtac | eapply nd_rule; apply
 495              (@RLet Γ Δ [] [] (@ga_mk _ (v2t ec) a' c') (@ga_mk _ (v2t ec) a' b')) ].
 496           eapply nd_comp; [ apply nd_llecnac | idtac ].
 497           apply nd_prod.
 498           apply r2'.
 499           eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RuCanL ].
 500           eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RCanR ].
 501           eapply nd_comp; [ idtac | eapply nd_rule;  apply
 502             (@RLet Γ Δ [@ga_mk _ (v2t ec) a' b' @@ _] [] (@ga_mk _ (v2t ec) a' c') (@ga_mk _ (v2t ec) b' c'))].
 503           eapply nd_comp; [ apply nd_llecnac | idtac ].
 504           eapply nd_prod.
 505           apply r1'.
 506           apply ga_comp.
 507           Defined.
 508
 509   Definition flatten_arrangement :
 510     forall Γ (Δ:CoercionEnv Γ) n
 511       (ec:HaskTyVar Γ ECKind) (lev:HaskLevel Γ) (ant1 ant2:Tree ??(LeveledHaskType Γ ★)) (r:Arrange ant1 ant2) succ,
 512       ND Rule
 513       [Γ > Δ > mapOptionTree (flatten_leveled_type ) (drop_lev n ant1)
 514         |- [@ga_mk _ (v2t ec)
 515           (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) ant1))
 516           (mapOptionTree (flatten_type ○ unlev) succ) @@ nil]]
 517       [Γ > Δ > mapOptionTree (flatten_leveled_type ) (drop_lev n ant2)
 518         |- [@ga_mk _ (v2t ec)
 519           (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) ant2))
 520           (mapOptionTree (flatten_type ○ unlev) succ) @@ nil]].
 521       intros.
 522       refine ( _ ;; (boost _ _ _ _ _ (postcompose _ _ _ _ _ _ _ (flatten_arrangement' Γ Δ ec lev ant1 ant2 r)))).
 523       apply nd_rule.
 524       apply RArrange.
 525       refine ((fix flatten ant1 ant2 (r:Arrange ant1 ant2) :=
 526         match r as R in Arrange A B return
 527           Arrange (mapOptionTree (flatten_leveled_type ) (drop_lev _ A))
 528           (mapOptionTree (flatten_leveled_type ) (drop_lev _ B)) with
 529           | RCanL  a             => let case_RCanL := tt  in RCanL _
 530           | RCanR  a             => let case_RCanR := tt  in RCanR _
 531           | RuCanL a             => let case_RuCanL := tt in RuCanL _
 532           | RuCanR a             => let case_RuCanR := tt in RuCanR _
 533           | RAssoc a b c         => let case_RAssoc := tt in RAssoc _ _ _
 534           | RCossa a b c         => let case_RCossa := tt in RCossa _ _ _
 535           | RExch  a b           => let case_RExch := tt  in RExch _ _
 536           | RWeak  a             => let case_RWeak := tt  in RWeak _
 537           | RCont  a             => let case_RCont := tt  in RCont _
 538           | RLeft  a b c r'      => let case_RLeft := tt  in RLeft  _ (flatten _ _ r')
 539           | RRight a b c r'      => let case_RRight := tt in RRight _ (flatten _ _ r')
 540           | RComp  a b c r1 r2   => let case_RComp := tt  in RComp    (flatten _ _ r1) (flatten _ _ r2)
 541         end) ant1 ant2 r); clear flatten; repeat take_simplify; repeat drop_simplify; intros.
 542         Defined.
 543
 544   Definition flatten_arrangement'' :
 545     forall  Γ Δ ant1 ant2 succ (r:Arrange ant1 ant2),
 546       ND Rule (mapOptionTree (flatten_judgment ) [Γ > Δ > ant1 |- succ])
 547       (mapOptionTree (flatten_judgment ) [Γ > Δ > ant2 |- succ]).
 548     intros.
 549     simpl.
 550     set (getjlev succ) as succ_lev.
 551     assert (succ_lev=getjlev succ).
 552       reflexivity.
 553
 554     destruct succ_lev.
 555       apply nd_rule.
 556       apply RArrange.
 557       induction r; simpl.
 558         apply RCanL.
 559         apply RCanR.
 560         apply RuCanL.
 561         apply RuCanR.
 562         apply RAssoc.
 563         apply RCossa.
 564         apply RExch.
 565         apply RWeak.
 566         apply RCont.
 567         apply RLeft; auto.
 568         apply RRight; auto.
 569         eapply RComp; [ apply IHr1 | apply IHr2 ].
 570
 571       apply flatten_arrangement.
 572         apply r.
 573         Defined.
 574
 575   Definition ga_join Γ Δ Σ₁ Σ₂ a b ec :
 576     ND Rule [] [Γ > Δ > Σ₁     |- [@ga_mk _ ec [] a      @@ nil]] ->
 577     ND Rule [] [Γ > Δ > Σ₂     |- [@ga_mk _ ec [] b      @@ nil]] ->
 578     ND Rule [] [Γ > Δ > Σ₁,,Σ₂ |- [@ga_mk _ ec [] (a,,b) @@ nil]].
 579     intro pfa.
 580     intro pfb.
 581     apply secondify with (c:=a)  in pfb.
 582     eapply nd_comp.
 583     Focus 2.
 584     eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
 585     eapply nd_comp; [ eapply nd_llecnac | idtac ].
 586     eapply nd_prod.
 587     apply pfb.
 588     clear pfb.
 589     apply postcompose'.
 590     eapply nd_comp.
 591     apply pfa.
 592     clear pfa.
 593     apply boost.
 594     eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanL ].
 595     apply precompose'.
 596     apply ga_uncancelr.
 597     apply nd_id.
 598     Defined.
 599
 600   Definition arrange_brak : forall Γ Δ ec succ t,
 601    ND Rule
 602      [Γ > Δ > mapOptionTree (flatten_leveled_type ) (drop_lev (ec :: nil) succ),,
 603       [(@ga_mk _ (v2t ec) []
 604         (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: nil) succ)))
 605       @@  nil] |- [(@ga_mk _ (v2t ec) [] [flatten_type  t]) @@  nil]]
 606      [Γ > Δ > mapOptionTree (flatten_leveled_type ) succ |- [(@ga_mk _ (v2t ec) [] [flatten_type  t]) @@  nil]].
 607     intros.
 608     unfold drop_lev.
 609     set (@arrange' _ succ (levelMatch (ec::nil))) as q.
 610     set (arrangeMap _ _ flatten_leveled_type q) as y.
 611     eapply nd_comp.
 612     Focus 2.
 613     eapply nd_rule.
 614     eapply RArrange.
 615     apply y.
 616     idtac.
 617     clear y q.
 618     simpl.
 619     eapply nd_comp; [ apply nd_llecnac | idtac ].
 620     eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
 621     apply nd_prod.
 622     Focus 2.
 623     apply nd_id.
 624     idtac.
 625     induction succ; try destruct a; simpl.
 626     unfold take_lev.
 627     unfold mkTakeFlags.
 628     unfold mkFlags.
 629     unfold bnot.
 630     simpl.
 631     destruct l as [t' lev'].
 632     destruct lev' as [|ec' lev'].
 633     simpl.
 634     apply ga_id.
 635     unfold levelMatch.
 636     set (@eqd_dec (HaskLevel Γ) (haskLevelEqDecidable Γ) (ec' :: lev') (ec :: nil)) as q.
 637     destruct q.
 638     inversion e; subst.
 639     simpl.
 640     apply nd_rule.
 641     apply RVar.
 642     simpl.
 643     apply ga_id.
 644     apply ga_id.
 645     unfold take_lev.
 646     simpl.
 647     apply ga_join.
 648       apply IHsucc1.
 649       apply IHsucc2.
 650     Defined.
 651
 652   Definition arrange_esc : forall Γ Δ ec succ t,
 653    ND Rule
 654      [Γ > Δ > mapOptionTree (flatten_leveled_type ) succ |- [(@ga_mk _ (v2t ec) [] [flatten_type  t]) @@  nil]]
 655      [Γ > Δ > mapOptionTree (flatten_leveled_type ) (drop_lev (ec :: nil) succ),,
 656       [(@ga_mk _ (v2t ec) []
 657         (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: nil) succ))) @@  nil]
 658       |- [(@ga_mk _ (v2t ec) [] [flatten_type  t]) @@  nil]].
 659     intros.
 660     unfold drop_lev.
 661     set (@arrange _ succ (levelMatch (ec::nil))) as q.
 662     set (arrangeMap _ _ flatten_leveled_type q) as y.
 663     eapply nd_comp.
 664     eapply nd_rule.
 665     eapply RArrange.
 666     apply y.
 667     idtac.
 668     clear y q.
 669
 670     induction succ.
 671     destruct a.
 672       destruct l.
 673       simpl.
 674       unfold mkDropFlags; simpl.
 675       unfold take_lev.
 676       unfold mkTakeFlags.
 677       simpl.
 678       destruct (General.list_eq_dec h0 (ec :: nil)).
 679         simpl.
 680         unfold flatten_leveled_type'.
 681         rewrite e.
 682         apply nd_id.
 683         simpl.
 684         apply nd_rule.
 685         apply RArrange.
 686         apply RLeft.
 687         apply RWeak.
 688       simpl.
 689         apply nd_rule.
 690         unfold take_lev.
 691         simpl.
 692         apply RArrange.
 693         apply RLeft.
 694         apply RWeak.
 695       apply (Prelude_error "escapifying code with multi-leaf antecedents is not supported").
 696       Defined.
 697
 698   Lemma mapOptionTree_distributes
 699     : forall T R (a b:Tree ??T) (f:T->R),
 700       mapOptionTree f (a,,b) = (mapOptionTree f a),,(mapOptionTree f b).
 701     reflexivity.
 702     Qed.
 703
 704   Definition decide_tree_empty : forall {T:Type}(t:Tree ??T),
 705     sum { q:Tree unit & t = mapTree (fun _ => None) q } unit.
 706     intro T.
 707     refine (fix foo t :=
 708       match t with
 709         | T_Leaf x => _
 710         | T_Branch b1 b2 => let b1' := foo b1 in let b2' := foo b2 in _
 711       end).
 712     intros.
 713     destruct x.
 714     right; apply tt.
 715     left.
 716       exists (T_Leaf tt).
 717       auto.
 718     destruct b1'.
 719     destruct b2'.
 720     destruct s.
 721     destruct s0.
 722     subst.
 723     left.
 724     exists (x,,x0).
 725     reflexivity.
 726     right; auto.
 727     right; auto.
 728     Defined.
 729
 730   Definition flatten_proof :
 731     forall  {h}{c},
 732       ND Rule h c ->
 733       ND Rule (mapOptionTree (flatten_judgment ) h) (mapOptionTree (flatten_judgment ) c).
 734     intros.
 735     eapply nd_map'; [ idtac | apply X ].
 736     clear h c X.
 737     intros.
 738     simpl in *.
 739
 740     refine (match X as R in Rule H C with
 741       | RArrange Γ Δ a b x d           => let case_RArrange := tt      in _
 742       | RNote    Γ Δ Σ τ l n           => let case_RNote := tt         in _
 743       | RLit     Γ Δ l     _           => let case_RLit := tt          in _
 744       | RVar     Γ Δ σ           lev   => let case_RVar := tt          in _
 745       | RGlobal  Γ Δ σ l wev           => let case_RGlobal := tt       in _
 746       | RLam     Γ Δ Σ tx te     lev   => let case_RLam := tt          in _
 747       | RCast    Γ Δ Σ σ τ lev γ       => let case_RCast := tt         in _
 748       | RAbsT    Γ Δ Σ κ σ lev         => let case_RAbsT := tt         in _
 749       | RAppT    Γ Δ Σ κ σ τ     lev   => let case_RAppT := tt         in _
 750       | RAppCo   Γ Δ Σ κ σ₁ σ₂ γ σ lev => let case_RAppCo := tt        in _
 751       | RAbsCo   Γ Δ Σ κ σ  σ₁ σ₂  lev => let case_RAbsCo := tt        in _
 752       | RApp     Γ Δ Σ₁ Σ₂ tx te lev   => let case_RApp := tt          in _
 753       | RLet     Γ Δ Σ₁ Σ₂ σ₁ σ₂ lev   => let case_RLet := tt          in _
 754       | RJoin    Γ p lri m x q         => let case_RJoin := tt in _
 755       | RVoid    _ _                   => let case_RVoid := tt   in _
 756       | RBrak    Γ Δ t ec succ lev           => let case_RBrak := tt         in _
 757       | REsc     Γ Δ t ec succ lev           => let case_REsc := tt          in _
 758       | RCase    Γ Δ lev tc Σ avars tbranches alts => let case_RCase := tt         in _
 759       | RLetRec  Γ Δ lri x y t         => let case_RLetRec := tt       in _
 760       end); clear X h c.
 761
 762     destruct case_RArrange.
 763       apply (flatten_arrangement''  Γ Δ a b x d).
 764
 765     destruct case_RBrak.
 766       simpl.
 767       destruct lev.
 768       change ([flatten_type  (<[ ec |- t ]>) @@  nil])
 769         with ([ga_mk (v2t ec) [] [flatten_type  t] @@  nil]).
 770       refine (ga_unkappa Γ Δ (v2t ec) nil (mapOptionTree (flatten_type ○ unlev) (take_lev (ec::nil) succ)) _
 771         (mapOptionTree (flatten_leveled_type) (drop_lev (ec::nil) succ)) ;; _ ).
 772       apply arrange_brak.
 773       apply (Prelude_error "found Brak at depth >0 indicating 3-level code; only two-level code is currently supported").
 774
 775     destruct case_REsc.
 776       simpl.
 777       destruct lev.
 778       simpl.
 779       change ([flatten_type (<[ ec |- t ]>) @@  nil])
 780         with ([ga_mk (v2t ec) [] [flatten_type  t] @@  nil]).
 781       eapply nd_comp; [ apply arrange_esc | idtac ].
 782       set (decide_tree_empty (take_lev (ec :: nil) succ)) as q'.
 783       destruct q'.
 784       destruct s.
 785       rewrite e.
 786       clear e.
 787
 788       eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanR ].
 789       eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
 790       eapply nd_comp; [ apply nd_llecnac | idtac ].
 791       apply nd_prod; [ idtac | eapply boost ].
 792       induction x.
 793       apply ga_id.
 794       eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanR ].
 795       simpl.
 796       apply ga_join.
 797       apply IHx1.
 798       apply IHx2.
 799       simpl.
 800       apply postcompose.
 801       apply ga_drop.
 802
 803       (* environment has non-empty leaves *)
 804       apply (ga_kappa Γ Δ (v2t ec) nil (mapOptionTree (flatten_type ○ unlev) (take_lev (ec::nil) succ)) _ _).
 805       apply (Prelude_error "found Esc at depth >0 indicating 3-level code; only two-level code is currently supported").
 806
 807     destruct case_RNote.
 808       simpl.
 809       destruct l; simpl.
 810         apply nd_rule; apply RNote; auto.
 811         apply nd_rule; apply RNote; auto.
 812
 813     destruct case_RLit.
 814       simpl.
 815       destruct l0; simpl.
 816         rewrite literal_types_unchanged.
 817           apply nd_rule; apply RLit.
 818         unfold take_lev; simpl.
 819         unfold drop_lev; simpl.
 820         simpl.
 821         rewrite literal_types_unchanged.
 822         apply ga_lit.
 823
 824     destruct case_RVar.
 825       Opaque flatten_judgment.
 826       simpl.
 827       Transparent flatten_judgment.
 828       idtac.
 829       unfold flatten_judgment.
 830       unfold getjlev.
 831       destruct lev.
 832       apply nd_rule. apply RVar.
 833       repeat drop_simplify.
 834       repeat take_simplify.
 835       simpl.
 836       apply ga_id.
 837
 838     destruct case_RGlobal.
 839       simpl.
 840       rename l into g.
 841       rename σ into l.
 842       destruct l as [|ec lev]; simpl.
 843         destruct (eqd_dec (g:CoreVar) (hetmet_flatten:CoreVar)).
 844           set (flatten_type (g wev)) as t.
 845           set (RGlobal _ Δ nil (mkGlobal Γ t hetmet_id)) as q.
 846           simpl in q.
 847           apply nd_rule.
 848           apply q.
 849           apply INil.
 850         destruct (eqd_dec (g:CoreVar) (hetmet_unflatten:CoreVar)).
 851           set (flatten_type (g wev)) as t.
 852           set (RGlobal _ Δ nil (mkGlobal Γ t hetmet_id)) as q.
 853           simpl in q.
 854           apply nd_rule.
 855           apply q.
 856           apply INil.
 857         apply nd_rule; rewrite globals_do_not_have_code_types.
 858           apply RGlobal.
 859       apply (Prelude_error "found RGlobal at depth >0; globals should never appear inside code brackets unless escaped").
 860
 861     destruct case_RLam.
 862       Opaque drop_lev.
 863       Opaque take_lev.
 864       simpl.
 865       destruct lev as [|ec lev]; simpl; [ apply nd_rule; apply RLam; auto | idtac ].
 866       repeat drop_simplify.
 867       repeat take_simplify.
 868       eapply nd_comp.
 869         eapply nd_rule.
 870         eapply RArrange.
 871         simpl.
 872         apply RCanR.
 873       apply boost.
 874       simpl.
 875       apply ga_curry.
 876
 877     destruct case_RCast.
 878       simpl.
 879       destruct lev as [|ec lev]; simpl; [ apply nd_rule; apply RCast; auto | idtac ].
 880       apply flatten_coercion; auto.
 881       apply (Prelude_error "RCast at level >0; casting inside of code brackets is currently not supported").
 882
 883     destruct case_RJoin.
 884       simpl.
 885       destruct (getjlev x); destruct (getjlev q);
 886         [ apply nd_rule; apply RJoin | idtac | idtac | idtac ];
 887         apply (Prelude_error "RJoin at depth >0").
 888
 889     destruct case_RApp.
 890       simpl.
 891
 892       destruct lev as [|ec lev]. simpl. apply nd_rule.
 893         replace (flatten_type  (tx ---> te)) with ((flatten_type  tx) ---> (flatten_type  te)).
 894         apply RApp.
 895         reflexivity.
 896
 897         repeat drop_simplify.
 898           repeat take_simplify.
 899           rewrite mapOptionTree_distributes.
 900           set (mapOptionTree (flatten_leveled_type ) (drop_lev (ec :: lev) Σ₁)) as Σ₁'.
 901           set (mapOptionTree (flatten_leveled_type ) (drop_lev (ec :: lev) Σ₂)) as Σ₂'.
 902           set (take_lev (ec :: lev) Σ₁) as Σ₁''.
 903           set (take_lev (ec :: lev) Σ₂) as Σ₂''.
 904           replace (flatten_type  (tx ---> te)) with ((flatten_type  tx) ---> (flatten_type  te)).
 905           apply (Prelude_error "FIXME: ga_apply").
 906           reflexivity.
 907
 908 (*
 909   Notation "`  x" := (take_lev _ x).
 910   Notation "`` x" := (mapOptionTree unlev x) (at level 20).
 911   Notation "``` x" := ((drop_lev _ x)) (at level 20).
 912   Notation "!<[]> x" := (flatten_type _ x) (at level 1).
 913   Notation "!<[@]> x" := (mapOptionTree flatten_leveled_type x) (at level 1).
 914 *)
 915
 916     destruct case_RLet.
 917       simpl.
 918       destruct lev as [|ec lev]; simpl; [ apply nd_rule; apply RLet; auto | idtac ].
 919       repeat drop_simplify.
 920       repeat take_simplify.
 921       simpl.
 922
 923       eapply nd_comp.
 924       eapply nd_prod; [ idtac | apply nd_id ].
 925       eapply boost.
 926       apply ga_second.
 927
 928       eapply nd_comp.
 929       eapply nd_prod.
 930       apply nd_id.
 931       eapply nd_comp.
 932       eapply nd_rule.
 933       eapply RArrange.
 934       apply RCanR.
 935       eapply precompose.
 936
 937       apply nd_rule.
 938       apply RLet.
 939
 940     destruct case_RVoid.
 941       simpl.
 942       apply nd_rule.
 943       apply RVoid.
 944
 945     destruct case_RAppT.
 946       simpl. destruct lev; simpl.
 947       rewrite flatten_commutes_with_HaskTAll.
 948       rewrite flatten_commutes_with_substT.
 949       apply nd_rule.
 950       apply RAppT.
 951       apply Δ.
 952       apply Δ.
 953       apply (Prelude_error "found type application at level >0; this is not supported").
 954
 955     destruct case_RAbsT.
 956       simpl. destruct lev; simpl.
 957       rewrite flatten_commutes_with_HaskTAll.
 958       rewrite flatten_commutes_with_HaskTApp.
 959       eapply nd_comp; [ idtac | eapply nd_rule; eapply RAbsT ].
 960       simpl.
 961       set (mapOptionTree (flatten_leveled_type ) (mapOptionTree (weakLT(κ:=κ)) Σ)) as a.
 962       set (mapOptionTree (weakLT(κ:=κ)) (mapOptionTree (flatten_leveled_type ) Σ)) as q'.
 963       assert (a=q').
 964         unfold a.
 965         unfold q'.
 966         clear a q'.
 967         induction Σ.
 968           destruct a.
 969           simpl.
 970           rewrite flatten_commutes_with_weakLT.
 971           reflexivity.
 972           reflexivity.
 973           simpl.
 974           rewrite <- IHΣ1.
 975           rewrite <- IHΣ2.
 976           reflexivity.
 977       rewrite H.
 978       apply nd_id.
 979       apply Δ.
 980       apply Δ.
 981       apply (Prelude_error "found type abstraction at level >0; this is not supported").
 982
 983     destruct case_RAppCo.
 984       simpl. destruct lev; simpl.
 985       unfold flatten_type.
 986       simpl.
 987       apply nd_rule.
 988       apply RAppCo.
 989       apply flatten_coercion.
 990       apply γ.
 991       apply (Prelude_error "found coercion application at level >0; this is not supported").
 992
 993     destruct case_RAbsCo.
 994       simpl. destruct lev; simpl.
 995       unfold flatten_type.
 996       simpl.
 997       apply (Prelude_error "AbsCo not supported (FIXME)").
 998       apply (Prelude_error "found coercion abstraction at level >0; this is not supported").
 999
1000     destruct case_RLetRec.
1001       rename t into lev.
1002       simpl.
1003       apply (Prelude_error "LetRec not supported (FIXME)").
1004
1005     destruct case_RCase.
1006       simpl.
1007       apply (Prelude_error "Case not supported (BIG FIXME)").
1008       Defined.
1009
1010
1011   (* to do: establish some metric on judgments (max length of level of any succedent type, probably), show how to
1012    * calculate it, and show that the flattening procedure above drives it down by one *)
1013
1014   (*
1015   Instance FlatteningFunctor {Γ}{Δ}{ec} : Functor (JudgmentsL (PCF Γ Δ ec)) (TypesL (SystemFCa Γ Δ)) (obact) :=
1016     { fmor := FlatteningFunctor_fmor }.
1017
1018   Definition ReificationFunctor Γ Δ : Functor (JudgmentsL _ _ (PCF n Γ Δ)) SystemFCa' (mapOptionTree brakifyJudg).
1019     refine {| fmor := ReificationFunctor_fmor Γ Δ |}; unfold hom; unfold ob; simpl ; intros.
1020
1021   Definition PCF_SMME (n:nat)(Γ:TypeEnv)(Δ:CoercionEnv Γ) : ProgrammingLanguageSMME.
1022     refine {| plsmme_pl := PCF n Γ Δ |}.
1023     Defined.
1024
1025   Definition SystemFCa_SMME (n:nat)(Γ:TypeEnv)(Δ:CoercionEnv Γ) : ProgrammingLanguageSMME.
1026     refine {| plsmme_pl := SystemFCa n Γ Δ |}.
1027     Defined.
1028
1029   Definition ReificationFunctorMonoidal n : MonoidalFunctor (JudgmentsN n) (JudgmentsN (S n)) (ReificationFunctor n).
1030     Defined.
1031
1032   (* 5.1.4 *)
1033   Definition PCF_SystemFCa_two_level n Γ Δ : TwoLevelLanguage (PCF_SMME n Γ Δ) (SystemFCa_SMME (S n) Γ Δ).
1034     Defined.
1035   *)
1036   (*  ... and the retraction exists *)
1037
1038 End HaskFlattener.
1039
1040 Implicit Arguments garrow [ ].