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