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