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 ECKind  -> RawHaskType TV ★                                          }.
 101   Context {prodTy : forall TV, RawHaskType TV ECKind  -> 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 {Γ}(ec:HaskType Γ ECKind)(tr:Tree ??(HaskType Γ ★)) : HaskType Γ ★ :=
 105     fun TV ite => reduceTree (unitTy TV (ec TV ite)) (prodTy TV (ec TV ite)) (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 ec ant TV ite) (ga_mk_tree ec 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 v) (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
 350        | eapply nd_rule; apply (@RLet Γ Δ [@ga_mk _ ec b c @@lev] Σ (@ga_mk _ ec a c) (@ga_mk _ ec a b) lev) ].
 351      eapply nd_comp; [ apply nd_llecnac | idtac ].
 352      apply nd_prod.
 353      apply X.
 354      eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RExch ].
 355      apply ga_comp.
 356      Defined.
 357
 358   Definition precompose Γ Δ ec : forall a x y z lev,
 359     ND Rule
 360       [ Γ > Δ > a                           |- [@ga_mk _ ec y z @@ lev] ]
 361       [ Γ > Δ > a,,[@ga_mk _ ec x y @@ lev] |- [@ga_mk _ ec x z @@ lev] ].
 362     intros.
 363     eapply nd_comp.
 364     apply nd_rlecnac.
 365     eapply nd_comp.
 366     eapply nd_prod.
 367     apply nd_id.
 368     eapply ga_comp.
 369
 370     eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RExch ].
 371
 372     apply nd_rule.
 373     apply RLet.
 374     Defined.
 375
 376   Definition precompose' : ∀ Γ Δ ec lev a b c Σ,
 377      ND Rule [] [ Γ > Δ > Σ                           |- [@ga_mk Γ ec b c @@ lev] ] ->
 378      ND Rule [] [ Γ > Δ > Σ,,[@ga_mk Γ ec a b @@ lev] |- [@ga_mk Γ ec a c @@ lev] ].
 379      intros.
 380      eapply nd_comp.
 381      apply X.
 382      apply precompose.
 383      Defined.
 384
 385   Definition postcompose : ∀ Γ Δ ec lev a b c,
 386      ND Rule [] [ Γ > Δ > []                    |- [@ga_mk Γ ec a b @@ lev] ] ->
 387      ND Rule [] [ Γ > Δ > [@ga_mk Γ ec b c @@ lev] |- [@ga_mk Γ ec a c @@ lev] ].
 388      intros.
 389      eapply nd_comp.
 390      apply postcompose'.
 391      apply X.
 392      apply nd_rule.
 393      apply RArrange.
 394      apply RCanL.
 395      Defined.
 396
 397   Definition firstify : ∀ Γ Δ ec lev a b c Σ,
 398     ND Rule [] [ Γ > Δ > Σ                     |- [@ga_mk Γ ec a b @@ lev] ] ->
 399     ND Rule [] [ Γ > Δ > Σ                    |- [@ga_mk Γ ec (a,,c) (b,,c) @@ lev] ].
 400     intros.
 401     eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanL ].
 402     eapply nd_comp; [ idtac | eapply nd_rule; apply RLet ].
 403     eapply nd_comp; [ apply nd_llecnac | idtac ].
 404     apply nd_prod.
 405     apply X.
 406     eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RuCanL ].
 407     apply ga_first.
 408     Defined.
 409
 410   Definition secondify : ∀ Γ Δ ec lev a b c Σ,
 411      ND Rule [] [ Γ > Δ > Σ                    |- [@ga_mk Γ ec a b @@ lev] ] ->
 412      ND Rule [] [ Γ > Δ > Σ                    |- [@ga_mk Γ ec (c,,a) (c,,b) @@ lev] ].
 413     intros.
 414     eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanL ].
 415     eapply nd_comp; [ idtac | eapply nd_rule; apply RLet ].
 416     eapply nd_comp; [ apply nd_llecnac | idtac ].
 417     apply nd_prod.
 418     apply X.
 419     eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RuCanL ].
 420     apply ga_second.
 421     Defined.
 422
 423   Lemma ga_unkappa     : ∀ Γ Δ ec l a b Σ,
 424     ND Rule
 425     [Γ > Δ > Σ |- [@ga_mk Γ ec a  b @@ l] ]
 426     [Γ > Δ > Σ,,[@ga_mk Γ ec [] a @@ l] |- [@ga_mk Γ ec [] b @@ l] ].
 427     intros.
 428     set (ga_comp Γ Δ ec l [] a b) as q.
 429
 430     set (@RLet Γ Δ) as q'.
 431     set (@RLet Γ Δ [@ga_mk _ ec [] a @@ l] Σ (@ga_mk _ ec [] b) (@ga_mk _ ec a b) l) as q''.
 432     eapply nd_comp.
 433     Focus 2.
 434     eapply nd_rule.
 435     eapply RArrange.
 436     apply RExch.
 437
 438     eapply nd_comp.
 439     Focus 2.
 440     eapply nd_rule.
 441     apply q''.
 442
 443     idtac.
 444     clear q'' q'.
 445     eapply nd_comp.
 446     apply nd_rlecnac.
 447     apply nd_prod.
 448     apply nd_id.
 449     apply q.
 450     Defined.
 451
 452   (* useful for cutting down on the pretty-printed noise
 453
 454   Notation "`  x" := (take_lev _ x) (at level 20).
 455   Notation "`` x" := (mapOptionTree unlev x) (at level 20).
 456   Notation "``` x" := (drop_lev _ x) (at level 20).
 457   *)
 458   Definition garrowfy_arrangement' :
 459     forall Γ (Δ:CoercionEnv Γ)
 460       (ec:HaskTyVar Γ ECKind) (lev:HaskLevel Γ) (ant1 ant2:Tree ??(LeveledHaskType Γ ★)) (r:Arrange ant1 ant2),
 461       ND Rule [] [Γ > Δ > [] |- [@ga_mk _ (v2t ec) (take_lev (ec :: lev) ant2) (take_lev (ec :: lev) ant1) @@ nil] ].
 462
 463       intros Γ Δ ec lev.
 464       refine (fix garrowfy ant1 ant2 (r:Arrange ant1 ant2):
 465            ND Rule [] [Γ > Δ > [] |- [@ga_mk _ (v2t ec) (take_lev (ec :: lev) ant2) (take_lev (ec :: lev) ant1) @@ nil]] :=
 466         match r as R in Arrange A B return
 467           ND Rule [] [Γ > Δ > [] |- [@ga_mk _ (v2t ec) (take_lev (ec :: lev) B) (take_lev (ec :: lev) A) @@ nil]]
 468           with
 469           | RCanL  a             => let case_RCanL := tt  in ga_uncancell _ _ _ _ _
 470           | RCanR  a             => let case_RCanR := tt  in ga_uncancelr _ _ _ _ _
 471           | RuCanL a             => let case_RuCanL := tt in ga_cancell _ _ _ _ _
 472           | RuCanR a             => let case_RuCanR := tt in ga_cancelr _ _ _ _ _
 473           | RAssoc a b c         => let case_RAssoc := tt in ga_assoc _ _ _ _ _ _ _
 474           | RCossa a b c         => let case_RCossa := tt in ga_unassoc _ _ _ _ _ _ _
 475           | RExch  a b           => let case_RExch := tt  in ga_swap  _ _ _ _ _ _
 476           | RWeak  a             => let case_RWeak := tt  in ga_drop _ _ _ _ _
 477           | RCont  a             => let case_RCont := tt  in ga_copy  _ _ _ _ _
 478           | RLeft  a b c r'      => let case_RLeft := tt  in garrowfy _ _ r' ;; boost _ _ _ _ _ (ga_second _ _ _ _ _ _ _)
 479           | RRight a b c r'      => let case_RRight := tt in garrowfy _ _ r' ;; boost _ _ _ _ _ (ga_first  _ _ _ _ _ _ _)
 480           | RComp  c b a r1 r2   => let case_RComp := tt  in (fun r1' r2' => _) (garrowfy _ _ r1) (garrowfy _ _ r2)
 481         end); clear garrowfy; repeat take_simplify; repeat drop_simplify; intros.
 482
 483         destruct case_RComp.
 484           set (take_lev (ec :: lev) a) as a' in *.
 485           set (take_lev (ec :: lev) b) as b' in *.
 486           set (take_lev (ec :: lev) c) as c' in *.
 487           eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RCanL ].
 488           eapply nd_comp; [ idtac | eapply nd_rule; apply
 489              (@RLet Γ Δ [] [] (@ga_mk _ (v2t ec) a' c') (@ga_mk _ (v2t ec) a' b')) ].
 490           eapply nd_comp; [ apply nd_llecnac | idtac ].
 491           apply nd_prod.
 492           apply r2'.
 493           eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RuCanL ].
 494           eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RCanR ].
 495           eapply nd_comp; [ idtac | eapply nd_rule;  apply
 496             (@RLet Γ Δ [@ga_mk _ (v2t ec) a' b' @@ _] [] (@ga_mk _ (v2t ec) a' c') (@ga_mk _ (v2t ec) b' c'))].
 497           eapply nd_comp; [ apply nd_llecnac | idtac ].
 498           eapply nd_prod.
 499           apply r1'.
 500           apply ga_comp.
 501           Defined.
 502
 503   Definition garrowfy_arrangement :
 504     forall Γ (Δ:CoercionEnv Γ) n
 505       (ec:HaskTyVar Γ ECKind) (lev:HaskLevel Γ) (ant1 ant2:Tree ??(LeveledHaskType Γ ★)) (r:Arrange ant1 ant2) succ,
 506       ND Rule
 507       [Γ > Δ > mapOptionTree (garrowfy_leveled_code_types ) (drop_lev n ant1)
 508         |- [@ga_mk _ (v2t ec) (take_lev (ec :: lev) ant1) (mapOptionTree (unlev' ) succ) @@ nil]]
 509       [Γ > Δ > mapOptionTree (garrowfy_leveled_code_types ) (drop_lev n ant2)
 510         |- [@ga_mk _ (v2t ec) (take_lev (ec :: lev) ant2) (mapOptionTree (unlev' ) succ) @@ nil]].
 511       intros.
 512       refine ( _ ;; (boost _ _ _ _ _ (postcompose _ _ _ _ _ _ _ (garrowfy_arrangement' Γ Δ ec lev ant1 ant2 r)))).
 513       apply nd_rule.
 514       apply RArrange.
 515       refine ((fix garrowfy ant1 ant2 (r:Arrange ant1 ant2) :=
 516         match r as R in Arrange A B return
 517           Arrange (mapOptionTree (garrowfy_leveled_code_types ) (drop_lev _ A))
 518           (mapOptionTree (garrowfy_leveled_code_types ) (drop_lev _ B)) with
 519           | RCanL  a             => let case_RCanL := tt  in RCanL _
 520           | RCanR  a             => let case_RCanR := tt  in RCanR _
 521           | RuCanL a             => let case_RuCanL := tt in RuCanL _
 522           | RuCanR a             => let case_RuCanR := tt in RuCanR _
 523           | RAssoc a b c         => let case_RAssoc := tt in RAssoc _ _ _
 524           | RCossa a b c         => let case_RCossa := tt in RCossa _ _ _
 525           | RExch  a b           => let case_RExch := tt  in RExch _ _
 526           | RWeak  a             => let case_RWeak := tt  in RWeak _
 527           | RCont  a             => let case_RCont := tt  in RCont _
 528           | RLeft  a b c r'      => let case_RLeft := tt  in RLeft  _ (garrowfy _ _ r')
 529           | RRight a b c r'      => let case_RRight := tt in RRight _ (garrowfy _ _ r')
 530           | RComp  a b c r1 r2   => let case_RComp := tt  in RComp    (garrowfy _ _ r1) (garrowfy _ _ r2)
 531         end) ant1 ant2 r); clear garrowfy; repeat take_simplify; repeat drop_simplify; intros.
 532         Defined.
 533
 534   Definition flatten_arrangement :
 535     forall  Γ Δ ant1 ant2 succ (r:Arrange ant1 ant2),
 536       ND Rule (mapOptionTree (flatten_judgment ) [Γ > Δ > ant1 |- succ])
 537       (mapOptionTree (flatten_judgment ) [Γ > Δ > ant2 |- succ]).
 538     intros.
 539     simpl.
 540     set (getjlev succ) as succ_lev.
 541     assert (succ_lev=getjlev succ).
 542       reflexivity.
 543
 544     destruct succ_lev.
 545       apply nd_rule.
 546       apply RArrange.
 547       induction r; simpl.
 548         apply RCanL.
 549         apply RCanR.
 550         apply RuCanL.
 551         apply RuCanR.
 552         apply RAssoc.
 553         apply RCossa.
 554         apply RExch.
 555         apply RWeak.
 556         apply RCont.
 557         apply RLeft; auto.
 558         apply RRight; auto.
 559         eapply RComp; [ apply IHr1 | apply IHr2 ].
 560
 561       apply garrowfy_arrangement.
 562         apply r.
 563         Defined.
 564
 565   Definition ga_join Γ Δ Σ₁ Σ₂ a b ec :
 566     ND Rule [] [Γ > Δ > Σ₁     |- [@ga_mk _ ec [] a      @@ nil]] ->
 567     ND Rule [] [Γ > Δ > Σ₂     |- [@ga_mk _ ec [] b      @@ nil]] ->
 568     ND Rule [] [Γ > Δ > Σ₁,,Σ₂ |- [@ga_mk _ ec [] (a,,b) @@ nil]].
 569     intro pfa.
 570     intro pfb.
 571     apply secondify with (c:=a)  in pfb.
 572     eapply nd_comp.
 573     Focus 2.
 574     eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
 575     eapply nd_comp; [ eapply nd_llecnac | idtac ].
 576     eapply nd_prod.
 577     apply pfb.
 578     clear pfb.
 579     apply postcompose'.
 580     eapply nd_comp.
 581     apply pfa.
 582     clear pfa.
 583     apply boost.
 584     eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanL ].
 585     apply precompose'.
 586     apply ga_uncancelr.
 587     apply nd_id.
 588     Defined.
 589
 590   Definition arrange_brak : forall Γ Δ ec succ t,
 591    ND Rule
 592      [Γ > Δ > mapOptionTree (garrowfy_leveled_code_types ) (drop_lev (ec :: nil) succ),,
 593       [(@ga_mk _ (v2t ec) [] (take_lev (ec :: nil) succ)) @@  nil] |- [(@ga_mk _ (v2t ec) [] [garrowfy_code_types  t]) @@  nil]]
 594      [Γ > Δ > mapOptionTree (garrowfy_leveled_code_types ) succ |- [(@ga_mk _ (v2t ec) [] [garrowfy_code_types  t]) @@  nil]].
 595     intros.
 596     unfold drop_lev.
 597     set (@arrange' _ succ (levelMatch (ec::nil))) as q.
 598     set (arrangeMap _ _ garrowfy_leveled_code_types q) as y.
 599     eapply nd_comp.
 600     Focus 2.
 601     eapply nd_rule.
 602     eapply RArrange.
 603     apply y.
 604     idtac.
 605     clear y q.
 606     simpl.
 607     eapply nd_comp; [ apply nd_llecnac | idtac ].
 608     eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
 609     apply nd_prod.
 610     Focus 2.
 611     apply nd_id.
 612     idtac.
 613     induction succ; try destruct a; simpl.
 614     unfold take_lev.
 615     unfold mkTakeFlags.
 616     unfold mkFlags.
 617     unfold bnot.
 618     simpl.
 619     destruct l as [t' lev'].
 620     destruct lev' as [|ec' lev'].
 621     simpl.
 622     apply ga_id.
 623     unfold levelMatch.
 624     set (@eqd_dec (HaskLevel Γ) (haskLevelEqDecidable Γ) (ec' :: lev') (ec :: nil)) as q.
 625     destruct q.
 626     inversion e; subst.
 627     simpl.
 628     apply nd_rule.
 629     apply RVar.
 630     simpl.
 631     apply ga_id.
 632     apply ga_id.
 633     unfold take_lev.
 634     simpl.
 635     apply ga_join.
 636       apply IHsucc1.
 637       apply IHsucc2.
 638     Defined.
 639
 640   Definition arrange_esc : forall Γ Δ ec succ t,
 641    ND Rule
 642      [Γ > Δ > mapOptionTree (garrowfy_leveled_code_types ) succ |- [(@ga_mk _ (v2t ec) [] [garrowfy_code_types  t]) @@  nil]]
 643      [Γ > Δ > mapOptionTree (garrowfy_leveled_code_types ) (drop_lev (ec :: nil) succ),,
 644       [(@ga_mk _ (v2t ec) [] (take_lev (ec :: nil) succ)) @@  nil] |- [(@ga_mk _ (v2t ec) [] [garrowfy_code_types  t]) @@  nil]].
 645     intros.
 646     unfold drop_lev.
 647     set (@arrange _ succ (levelMatch (ec::nil))) as q.
 648     set (arrangeMap _ _ garrowfy_leveled_code_types q) as y.
 649     eapply nd_comp.
 650     eapply nd_rule.
 651     eapply RArrange.
 652     apply y.
 653     idtac.
 654     clear y q.
 655
 656     induction succ.
 657     destruct a.
 658       destruct l.
 659       simpl.
 660       unfold mkDropFlags; simpl.
 661       unfold take_lev.
 662       unfold mkTakeFlags.
 663       simpl.
 664       destruct (General.list_eq_dec h0 (ec :: nil)).
 665         simpl.
 666         unfold garrowfy_leveled_code_types'.
 667         rewrite e.
 668         apply nd_id.
 669         simpl.
 670         apply nd_rule.
 671         apply RArrange.
 672         apply RLeft.
 673         apply RWeak.
 674       simpl.
 675         apply nd_rule.
 676         unfold take_lev.
 677         simpl.
 678         apply RArrange.
 679         apply RLeft.
 680         apply RWeak.
 681       apply (Prelude_error "escapifying code with multi-leaf antecedents is not supported").
 682       Defined.
 683
 684   Lemma mapOptionTree_distributes
 685     : forall T R (a b:Tree ??T) (f:T->R),
 686       mapOptionTree f (a,,b) = (mapOptionTree f a),,(mapOptionTree f b).
 687     reflexivity.
 688     Qed.
 689
 690   Definition decide_tree_empty : forall {T:Type}(t:Tree ??T),
 691     sum { q:Tree unit & t = mapTree (fun _ => None) q } unit.
 692     intro T.
 693     refine (fix foo t :=
 694       match t with
 695         | T_Leaf x => _
 696         | T_Branch b1 b2 => let b1' := foo b1 in let b2' := foo b2 in _
 697       end).
 698     intros.
 699     destruct x.
 700     right; apply tt.
 701     left.
 702       exists (T_Leaf tt).
 703       auto.
 704     destruct b1'.
 705     destruct b2'.
 706     destruct s.
 707     destruct s0.
 708     subst.
 709     left.
 710     exists (x,,x0).
 711     reflexivity.
 712     right; auto.
 713     right; auto.
 714     Defined.
 715
 716   Definition flatten_proof :
 717     forall  {h}{c},
 718       ND Rule h c ->
 719       ND Rule (mapOptionTree (flatten_judgment ) h) (mapOptionTree (flatten_judgment ) c).
 720     intros.
 721     eapply nd_map'; [ idtac | apply X ].
 722     clear h c X.
 723     intros.
 724     simpl in *.
 725
 726     refine (match X as R in Rule H C with
 727       | RArrange Γ Δ a b x d           => let case_RArrange := tt      in _
 728       | RNote    Γ Δ Σ τ l n           => let case_RNote := tt         in _
 729       | RLit     Γ Δ l     _           => let case_RLit := tt          in _
 730       | RVar     Γ Δ σ           lev   => let case_RVar := tt          in _
 731       | RGlobal  Γ Δ σ l wev           => let case_RGlobal := tt       in _
 732       | RLam     Γ Δ Σ tx te     lev   => let case_RLam := tt          in _
 733       | RCast    Γ Δ Σ σ τ lev γ       => let case_RCast := tt         in _
 734       | RAbsT    Γ Δ Σ κ σ lev         => let case_RAbsT := tt         in _
 735       | RAppT    Γ Δ Σ κ σ τ     lev   => let case_RAppT := tt         in _
 736       | RAppCo   Γ Δ Σ κ σ₁ σ₂ γ σ lev => let case_RAppCo := tt        in _
 737       | RAbsCo   Γ Δ Σ κ σ  σ₁ σ₂  lev => let case_RAbsCo := tt        in _
 738       | RApp     Γ Δ Σ₁ Σ₂ tx te lev   => let case_RApp := tt          in _
 739       | RLet     Γ Δ Σ₁ Σ₂ σ₁ σ₂ lev   => let case_RLet := tt          in _
 740       | RJoin    Γ p lri m x q         => let case_RJoin := tt in _
 741       | RVoid    _ _                   => let case_RVoid := tt   in _
 742       | RBrak    Γ Δ t ec succ lev           => let case_RBrak := tt         in _
 743       | REsc     Γ Δ t ec succ lev           => let case_REsc := tt          in _
 744       | RCase    Γ Δ lev tc Σ avars tbranches alts => let case_RCase := tt         in _
 745       | RLetRec  Γ Δ lri x y t         => let case_RLetRec := tt       in _
 746       end); clear X h c.
 747
 748     destruct case_RArrange.
 749       apply (flatten_arrangement  Γ Δ a b x d).
 750
 751     destruct case_RBrak.
 752       simpl.
 753       destruct lev.
 754       change ([garrowfy_code_types  (<[ ec |- t ]>) @@  nil])
 755         with ([ga_mk (v2t ec) [] [garrowfy_code_types  t] @@  nil]).
 756       refine (ga_unkappa Γ Δ (v2t ec) nil (take_lev (ec::nil) succ) _
 757         (mapOptionTree (garrowfy_leveled_code_types) (drop_lev (ec::nil) succ)) ;; _ ).
 758       apply arrange_brak.
 759       apply (Prelude_error "found Brak at depth >0 indicating 3-level code; only two-level code is currently supported").
 760
 761     destruct case_REsc.
 762       simpl.
 763       destruct lev.
 764       simpl.
 765       change ([garrowfy_code_types (<[ ec |- t ]>) @@  nil])
 766         with ([ga_mk (v2t ec) [] [garrowfy_code_types  t] @@  nil]).
 767       eapply nd_comp; [ apply arrange_esc | idtac ].
 768       set (decide_tree_empty (take_lev (ec :: nil) succ)) as q'.
 769       destruct q'.
 770       destruct s.
 771       rewrite e.
 772       clear e.
 773
 774       eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanR ].
 775       eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
 776       eapply nd_comp; [ apply nd_llecnac | idtac ].
 777       apply nd_prod; [ idtac | eapply boost ].
 778       induction x.
 779       apply ga_id.
 780       eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanR ].
 781       apply ga_join.
 782       apply IHx1.
 783       apply IHx2.
 784       unfold unlev'.
 785       simpl.
 786       apply postcompose.
 787       apply ga_drop.
 788
 789       (* environment has non-empty leaves *)
 790       apply (ga_kappa Γ Δ (v2t ec) nil (take_lev (ec::nil) succ) _ _).
 791       apply (Prelude_error "found Esc at depth >0 indicating 3-level code; only two-level code is currently supported").
 792
 793     destruct case_RNote.
 794       simpl.
 795       destruct l; simpl.
 796         apply nd_rule; apply RNote; auto.
 797         apply nd_rule; apply RNote; auto.
 798
 799     destruct case_RLit.
 800       simpl.
 801       destruct l0; simpl.
 802         rewrite literal_types_unchanged.
 803           apply nd_rule; apply RLit.
 804         unfold take_lev; simpl.
 805         unfold drop_lev; simpl.
 806         unfold unlev'.
 807         simpl.
 808         rewrite literal_types_unchanged.
 809         apply ga_lit.
 810
 811     destruct case_RVar.
 812       Opaque flatten_judgment.
 813       simpl.
 814       Transparent flatten_judgment.
 815       idtac.
 816       unfold flatten_judgment.
 817       unfold getjlev.
 818       destruct lev.
 819       apply nd_rule. apply RVar.
 820       repeat drop_simplify.
 821       unfold unlev'.
 822       repeat take_simplify.
 823       simpl.
 824       apply ga_id.
 825
 826     destruct case_RGlobal.
 827       simpl.
 828       rename l into g.
 829       rename σ into l.
 830       destruct l as [|ec lev]; simpl.
 831         destruct (eqd_dec (g:CoreVar) (hetmet_flatten:CoreVar)).
 832           set (garrowfy_code_types (g wev)) as t.
 833           set (RGlobal _ Δ nil (mkGlobal Γ t hetmet_id)) as q.
 834           simpl in q.
 835           apply nd_rule.
 836           apply q.
 837           apply INil.
 838         destruct (eqd_dec (g:CoreVar) (hetmet_unflatten:CoreVar)).
 839           set (garrowfy_code_types (g wev)) as t.
 840           set (RGlobal _ Δ nil (mkGlobal Γ t hetmet_id)) as q.
 841           simpl in q.
 842           apply nd_rule.
 843           apply q.
 844           apply INil.
 845         apply nd_rule; rewrite globals_do_not_have_code_types.
 846           apply RGlobal.
 847       apply (Prelude_error "found RGlobal at depth >0; globals should never appear inside code brackets unless escaped").
 848
 849     destruct case_RLam.
 850       Opaque drop_lev.
 851       Opaque take_lev.
 852       simpl.
 853       destruct lev as [|ec lev]; simpl; [ apply nd_rule; apply RLam; auto | idtac ].
 854       repeat drop_simplify.
 855       repeat take_simplify.
 856       eapply nd_comp.
 857         eapply nd_rule.
 858         eapply RArrange.
 859         simpl.
 860         apply RCanR.
 861       apply boost.
 862       apply ga_curry.
 863
 864     destruct case_RCast.
 865       simpl.
 866       destruct lev as [|ec lev]; simpl; [ apply nd_rule; apply RCast; auto | idtac ].
 867       apply flatten_coercion; auto.
 868       apply (Prelude_error "RCast at level >0; casting inside of code brackets is currently not supported").
 869
 870     destruct case_RJoin.
 871       simpl.
 872       destruct (getjlev x); destruct (getjlev q);
 873         [ apply nd_rule; apply RJoin | idtac | idtac | idtac ];
 874         apply (Prelude_error "RJoin at depth >0").
 875
 876     destruct case_RApp.
 877       simpl.
 878
 879       destruct lev as [|ec lev]. simpl. apply nd_rule.
 880         replace (garrowfy_code_types  (tx ---> te)) with ((garrowfy_code_types  tx) ---> (garrowfy_code_types  te)).
 881         apply RApp.
 882         reflexivity.
 883
 884         repeat drop_simplify.
 885           repeat take_simplify.
 886           rewrite mapOptionTree_distributes.
 887           set (mapOptionTree (garrowfy_leveled_code_types ) (drop_lev (ec :: lev) Σ₁)) as Σ₁'.
 888           set (mapOptionTree (garrowfy_leveled_code_types ) (drop_lev (ec :: lev) Σ₂)) as Σ₂'.
 889           set (take_lev (ec :: lev) Σ₁) as Σ₁''.
 890           set (take_lev (ec :: lev) Σ₂) as Σ₂''.
 891           replace (garrowfy_code_types  (tx ---> te)) with ((garrowfy_code_types  tx) ---> (garrowfy_code_types  te)).
 892           apply (Prelude_error "FIXME: ga_apply").
 893           reflexivity.
 894
 895 (*
 896   Notation "`  x" := (take_lev _ x).
 897   Notation "`` x" := (mapOptionTree unlev x) (at level 20).
 898   Notation "``` x" := ((drop_lev _ x)) (at level 20).
 899   Notation "!<[]> x" := (garrowfy_code_types _ x) (at level 1).
 900   Notation "!<[@]> x" := (mapOptionTree garrowfy_leveled_code_types x) (at level 1).
 901 *)
 902
 903     destruct case_RLet.
 904       simpl.
 905       destruct lev as [|ec lev]; simpl; [ apply nd_rule; apply RLet; auto | idtac ].
 906       repeat drop_simplify.
 907       repeat take_simplify.
 908       simpl.
 909
 910       eapply nd_comp.
 911       eapply nd_prod; [ idtac | apply nd_id ].
 912       eapply boost.
 913       apply ga_second.
 914
 915       eapply nd_comp.
 916       eapply nd_prod.
 917       apply nd_id.
 918       eapply nd_comp.
 919       eapply nd_rule.
 920       eapply RArrange.
 921       apply RCanR.
 922       eapply precompose.
 923
 924       apply nd_rule.
 925       apply RLet.
 926
 927     destruct case_RVoid.
 928       simpl.
 929       apply nd_rule.
 930       apply RVoid.
 931
 932     destruct case_RAppT.
 933       simpl. destruct lev; simpl.
 934       rewrite garrowfy_commutes_with_HaskTAll.
 935       rewrite garrowfy_commutes_with_substT.
 936       apply nd_rule.
 937       apply RAppT.
 938       apply Δ.
 939       apply Δ.
 940       apply (Prelude_error "found type application at level >0; this is not supported").
 941
 942     destruct case_RAbsT.
 943       simpl. destruct lev; simpl.
 944       rewrite garrowfy_commutes_with_HaskTAll.
 945       rewrite garrowfy_commutes_with_HaskTApp.
 946       eapply nd_comp; [ idtac | eapply nd_rule; eapply RAbsT ].
 947       simpl.
 948       set (mapOptionTree (garrowfy_leveled_code_types ) (mapOptionTree (weakLT(κ:=κ)) Σ)) as a.
 949       set (mapOptionTree (weakLT(κ:=κ)) (mapOptionTree (garrowfy_leveled_code_types ) Σ)) as q'.
 950       assert (a=q').
 951         unfold a.
 952         unfold q'.
 953         clear a q'.
 954         induction Σ.
 955           destruct a.
 956           simpl.
 957           rewrite garrowfy_commutes_with_weakLT.
 958           reflexivity.
 959           reflexivity.
 960           simpl.
 961           rewrite <- IHΣ1.
 962           rewrite <- IHΣ2.
 963           reflexivity.
 964       rewrite H.
 965       apply nd_id.
 966       apply Δ.
 967       apply Δ.
 968       apply (Prelude_error "found type abstraction at level >0; this is not supported").
 969
 970     destruct case_RAppCo.
 971       simpl. destruct lev; simpl.
 972       unfold garrowfy_code_types.
 973       simpl.
 974       apply nd_rule.
 975       apply RAppCo.
 976       apply flatten_coercion.
 977       apply γ.
 978       apply (Prelude_error "found coercion application at level >0; this is not supported").
 979
 980     destruct case_RAbsCo.
 981       simpl. destruct lev; simpl.
 982       unfold garrowfy_code_types.
 983       simpl.
 984       apply (Prelude_error "AbsCo not supported (FIXME)").
 985       apply (Prelude_error "found coercion abstraction at level >0; this is not supported").
 986
 987     destruct case_RLetRec.
 988       rename t into lev.
 989       simpl.
 990       apply (Prelude_error "LetRec not supported (FIXME)").
 991
 992     destruct case_RCase.
 993       simpl.
 994       apply (Prelude_error "Case not supported (BIG FIXME)").
 995       Defined.
 996
 997
 998   (* to do: establish some metric on judgments (max length of level of any succedent type, probably), show how to
 999    * calculate it, and show that the flattening procedure above drives it down by one *)
1000
1001   (*
1002   Instance FlatteningFunctor {Γ}{Δ}{ec} : Functor (JudgmentsL (PCF Γ Δ ec)) (TypesL (SystemFCa Γ Δ)) (obact) :=
1003     { fmor := FlatteningFunctor_fmor }.
1004
1005   Definition ReificationFunctor Γ Δ : Functor (JudgmentsL _ _ (PCF n Γ Δ)) SystemFCa' (mapOptionTree brakifyJudg).
1006     refine {| fmor := ReificationFunctor_fmor Γ Δ |}; unfold hom; unfold ob; simpl ; intros.
1007
1008   Definition PCF_SMME (n:nat)(Γ:TypeEnv)(Δ:CoercionEnv Γ) : ProgrammingLanguageSMME.
1009     refine {| plsmme_pl := PCF n Γ Δ |}.
1010     Defined.
1011
1012   Definition SystemFCa_SMME (n:nat)(Γ:TypeEnv)(Δ:CoercionEnv Γ) : ProgrammingLanguageSMME.
1013     refine {| plsmme_pl := SystemFCa n Γ Δ |}.
1014     Defined.
1015
1016   Definition ReificationFunctorMonoidal n : MonoidalFunctor (JudgmentsN n) (JudgmentsN (S n)) (ReificationFunctor n).
1017     Defined.
1018
1019   (* 5.1.4 *)
1020   Definition PCF_SystemFCa_two_level n Γ Δ : TwoLevelLanguage (PCF_SMME n Γ Δ) (SystemFCa_SMME (S n) Γ Δ).
1021     Defined.
1022   *)
1023   (*  ... and the retraction exists *)
1024
1025 End HaskFlattener.
1026
1027 Implicit Arguments garrow [ ].