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 Require Import NaturalDeductionCategory.
  22
  23 Require Import Algebras_ch4.
  24 Require Import Categories_ch1_3.
  25 Require Import Functors_ch1_4.
  26 Require Import Isomorphisms_ch1_5.
  27 Require Import ProductCategories_ch1_6_1.
  28 Require Import OppositeCategories_ch1_6_2.
  29 Require Import Enrichment_ch2_8.
  30 Require Import Subcategories_ch7_1.
  31 Require Import NaturalTransformations_ch7_4.
  32 Require Import NaturalIsomorphisms_ch7_5.
  33 Require Import BinoidalCategories.
  34 Require Import PreMonoidalCategories.
  35 Require Import MonoidalCategories_ch7_8.
  36 Require Import Coherence_ch7_8.
  37
  38 Require Import HaskStrongTypes.
  39 Require Import HaskStrong.
  40 Require Import HaskProof.
  41 Require Import HaskStrongToProof.
  42 Require Import HaskProofToStrong.
  43 Require Import ProgrammingLanguage.
  44 Require Import HaskProgrammingLanguage.
  45 Require Import PCF.
  46
  47 Open Scope nd_scope.
  48
  49 (*
  50  *  The flattening transformation.  Currently only TWO-level languages are
  51  *  supported, and the level-1 sublanguage is rather limited.
  52  *
  53  *  This file abuses terminology pretty badly.  For purposes of this file,
  54  *  "PCF" means "the level-1 sublanguage" and "FC" (aka System FC) means
  55  *  the whole language (level-0 language including bracketed level-1 terms)
  56  *)
  57 Section HaskFlattener.
  58
  59   (* this actually has nothing to do with categories; it shows that proofs [|-A]//[|-B] are one-to-one with []//[A|-B] *)
  60   (* TODO Lemma hom_functor_full*)
  61
  62   (* lemma: if a proof from no hypotheses contains no Brak's or Esc's, then the context contains no variables at level!=0 *)
  63
  64   Definition minus' n m :=
  65     match m with
  66       | 0 => n
  67       | _ => match n with
  68                | 0 => 0
  69                | _ => n - m
  70              end
  71     end.
  72
  73   Ltac eqd_dec_refl' :=
  74     match goal with
  75       | [ |- context[@eqd_dec ?T ?V ?X ?X] ] =>
  76         destruct (@eqd_dec T V X X) as [eqd_dec1 | eqd_dec2];
  77           [ clear eqd_dec1 | set (eqd_dec2 (refl_equal _)) as eqd_dec2'; inversion eqd_dec2' ]
  78   end.
  79
  80   (* The opposite: replace any type which is NOT at level "lev" with None *)
  81   Definition take_lev {Γ}(lev:HaskLevel Γ)(tt:Tree ??(LeveledHaskType Γ ★)) : Tree ??(HaskType Γ ★) :=
  82     mapTree (fun t => match t with
  83                         | Some (ttype @@ tlev) => if eqd_dec tlev lev then Some ttype else None
  84                         | _                    => None
  85                       end) tt.
  86
  87   (* In a tree of types, replace any type at depth "lev" or greater None *)
  88   Definition drop_depth {Γ}(lev:HaskLevel Γ)(tt:Tree ??(LeveledHaskType Γ ★)) : Tree ??(LeveledHaskType Γ ★) :=
  89     mapTree (fun t => match t with
  90                         | Some (ttype @@ tlev) => if eqd_dec tlev lev then None else t
  91                         | _ => t
  92                       end) tt.
  93
  94   Lemma drop_depth_lemma : forall Γ (lev:HaskLevel Γ) x, drop_depth lev [x @@  lev] = [].
  95     intros; simpl.
  96     Opaque eqd_dec.
  97     unfold drop_depth.
  98     simpl.
  99     Transparent eqd_dec.
 100     eqd_dec_refl'.
 101     auto.
 102     Qed.
 103
 104   Lemma drop_depth_lemma_s : forall Γ (lev:HaskLevel Γ) ec x, drop_depth (ec::lev) [x @@  (ec :: lev)] = [].
 105     intros; simpl.
 106     Opaque eqd_dec.
 107     unfold drop_depth.
 108     simpl.
 109     Transparent eqd_dec.
 110     eqd_dec_refl'.
 111     auto.
 112     Qed.
 113
 114   Lemma take_lemma : forall Γ (lev:HaskLevel Γ) x, take_lev lev [x @@  lev] = [x].
 115     intros; simpl.
 116     Opaque eqd_dec.
 117     unfold take_lev.
 118     simpl.
 119     Transparent eqd_dec.
 120     eqd_dec_refl'.
 121     auto.
 122     Qed.
 123
 124   Ltac drop_simplify :=
 125     match goal with
 126       | [ |- context[@drop_depth ?G ?L [ ?X @@ ?L ] ] ] =>
 127         rewrite (drop_depth_lemma G L X)
 128       | [ |- context[@drop_depth ?G (?E :: ?L) [ ?X @@ (?E :: ?L) ] ] ] =>
 129         rewrite (drop_depth_lemma_s G L E X)
 130       | [ |- context[@drop_depth ?G ?N (?A,,?B)] ] =>
 131       change (@drop_depth G N (A,,B)) with ((@drop_depth G N A),,(@drop_depth G N B))
 132       | [ |- context[@drop_depth ?G ?N (T_Leaf None)] ] =>
 133       change (@drop_depth G N (T_Leaf (@None (LeveledHaskType G ★)))) with (T_Leaf (@None (LeveledHaskType G ★)))
 134     end.
 135
 136   Ltac take_simplify :=
 137     match goal with
 138       | [ |- context[@take_lev ?G ?L [ ?X @@ ?L ] ] ] =>
 139         rewrite (take_lemma G L X)
 140       | [ |- context[@take_lev ?G ?N (?A,,?B)] ] =>
 141       change (@take_lev G N (A,,B)) with ((@take_lev G N A),,(@take_lev G N B))
 142       | [ |- context[@take_lev ?G ?N (T_Leaf None)] ] =>
 143       change (@take_lev G N (T_Leaf (@None (LeveledHaskType G ★)))) with (T_Leaf (@None (LeveledHaskType G ★)))
 144     end.
 145
 146   Fixpoint reduceTree {T}(unit:T)(merge:T -> T -> T)(tt:Tree ??T) : T :=
 147     match tt with
 148       | T_Leaf None     => unit
 149       | T_Leaf (Some x) => x
 150       | T_Branch b1 b2  => merge (reduceTree unit merge b1) (reduceTree unit merge b2)
 151     end.
 152
 153   Set Printing Width 130.
 154
 155   Context {unitTy : forall TV, RawHaskType TV  ★             }.
 156   Context {prodTy : forall TV, RawHaskType TV (★ ⇛ ★ ⇛ ★)    }.
 157   Context {gaTy   : forall TV, RawHaskType TV (★ ⇛ ★ ⇛ ★ ⇛ ★)}.
 158
 159   Definition ga_tree      := fun TV tr => reduceTree (unitTy TV) (fun t1 t2 => TApp (TApp (prodTy TV) t1) t2) tr.
 160   Definition ga'          := fun TV ec ant' suc' => TApp (TApp (TApp (gaTy TV) ec) (ga_tree TV ant')) (ga_tree TV suc').
 161   Definition ga {Γ} : HaskType Γ ★ -> Tree ??(HaskType Γ ★) -> Tree ??(HaskType Γ ★) -> HaskType Γ ★ :=
 162     fun ec ant suc =>
 163                                fun TV ite =>
 164                                  let ant' := mapOptionTree (fun x => x TV ite) ant in
 165                                    let suc' := mapOptionTree (fun x => x TV ite) suc in
 166                                      ga' TV (ec TV ite) ant' suc'.
 167
 168   Class garrow :=
 169   { ga_id        : ∀ Γ Δ ec l a    , ND Rule [] [Γ > Δ >                           [] |- [@ga Γ ec a a @@ l] ]
 170   ; ga_cancelr   : ∀ Γ Δ ec l a    , ND Rule [] [Γ > Δ >                           [] |- [@ga Γ ec (a,,[]) a @@ l] ]
 171   ; ga_cancell   : ∀ Γ Δ ec l a    , ND Rule [] [Γ > Δ >                           [] |- [@ga Γ ec ([],,a) a @@ l] ]
 172   ; ga_uncancelr : ∀ Γ Δ ec l a    , ND Rule [] [Γ > Δ >                           [] |- [@ga Γ ec a (a,,[]) @@ l] ]
 173   ; ga_uncancell : ∀ Γ Δ ec l a    , ND Rule [] [Γ > Δ >                           [] |- [@ga Γ ec a ([],,a) @@ l] ]
 174   ; ga_assoc     : ∀ Γ Δ ec l a b c, ND Rule [] [Γ > Δ >                           [] |- [@ga Γ ec ((a,,b),,c) (a,,(b,,c)) @@ l] ]
 175   ; ga_unassoc   : ∀ Γ Δ ec l a b c, ND Rule [] [Γ > Δ >                           [] |- [@ga Γ ec (a,,(b,,c)) ((a,,b),,c) @@ l] ]
 176   ; ga_swap      : ∀ Γ Δ ec l a b  , ND Rule [] [Γ > Δ >                           [] |- [@ga Γ ec (a,,b) (b,,a) @@ l] ]
 177   ; ga_drop      : ∀ Γ Δ ec l a    , ND Rule [] [Γ > Δ >                           [] |- [@ga Γ ec a [] @@ l] ]
 178   ; ga_copy      : ∀ Γ Δ ec l a    , ND Rule [] [Γ > Δ >                           [] |- [@ga Γ ec a (a,,a) @@ l] ]
 179   ; ga_first     : ∀ Γ Δ ec l a b x, ND Rule [] [Γ > Δ >          [@ga Γ ec a b @@ l] |- [@ga Γ ec (a,,x) (b,,x) @@ l] ]
 180   ; ga_second    : ∀ Γ Δ ec l a b x, ND Rule [] [Γ > Δ >          [@ga Γ ec a b @@ l] |- [@ga Γ ec (x,,a) (x,,b) @@ l] ]
 181   ; ga_lit       : ∀ Γ Δ ec l lit  , ND Rule [] [Γ > Δ >                           [] |- [@ga Γ ec [] [literalType lit] @@ l] ]
 182   ; ga_curry     : ∀ Γ Δ ec l a b c, ND Rule [] [Γ > Δ > [@ga Γ ec (a,,[b]) [c] @@ l] |- [@ga Γ ec a [b ---> c] @@ l] ]
 183   ; ga_comp      : ∀ Γ Δ ec l a b c, ND Rule [] [Γ > Δ > [@ga Γ ec a b @@ l],,[@ga Γ ec b c @@ l] |- [@ga Γ ec a c @@ l] ]
 184   ; ga_apply     : ∀ Γ Δ ec l a a' b c, ND Rule []
 185                                   [Γ > Δ > [@ga Γ ec a [b ---> c] @@ l],,[@ga Γ ec a' [b] @@ l] |- [@ga Γ ec (a,,a') [c] @@ l] ]
 186   ; ga_kappa     : ∀ Γ Δ ec l a b Σ, ND Rule
 187   [Γ > Δ > Σ,,[@ga Γ ec [] a @@ l] |- [@ga Γ ec [] b @@ l] ]
 188   [Γ > Δ > Σ          |- [@ga Γ ec a  b @@ l] ]
 189   }.
 190   Context `(gar:garrow).
 191
 192   Notation "a ~~~~> b" := (@ga _ _ a b) (at level 20).
 193
 194   (*
 195    *  The story:
 196    *    - code types <[t]>@c                                                become garrows  c () t
 197    *    - free variables of type t at a level lev deeper than the succedent become garrows  c () t
 198    *    - free variables at the level of the succedent become
 199    *)
 200   Fixpoint garrowfy_raw_codetypes {TV}{κ}(depth:nat)(exp: RawHaskType TV κ) : RawHaskType TV κ :=
 201     match exp with
 202     | TVar    _  x        => TVar x
 203     | TAll     _ y        => TAll   _  (fun v => garrowfy_raw_codetypes depth (y v))
 204     | TApp   _ _ x y      => TApp      (garrowfy_raw_codetypes depth x) (garrowfy_raw_codetypes depth y)
 205     | TCon       tc       => TCon      tc
 206     | TCoerc _ t1 t2 t    => TCoerc    (garrowfy_raw_codetypes depth t1) (garrowfy_raw_codetypes depth t2)
 207                                        (garrowfy_raw_codetypes depth t)
 208     | TArrow              => TArrow
 209     | TCode      v e      => match depth with
 210                                | O          => ga' TV v [] [(*garrowfy_raw_codetypes depth*) e]
 211                                | (S depth') => TCode v (garrowfy_raw_codetypes depth' e)
 212                              end
 213     | TyFunApp     tfc lt => TyFunApp tfc (garrowfy_raw_codetypes_list _ depth lt)
 214     end
 215     with garrowfy_raw_codetypes_list {TV}(lk:list Kind)(depth:nat)(exp:@RawHaskTypeList TV lk) : @RawHaskTypeList TV lk :=
 216     match exp in @RawHaskTypeList _ LK return @RawHaskTypeList TV LK with
 217     | TyFunApp_nil               => TyFunApp_nil
 218     | TyFunApp_cons  κ kl t rest => TyFunApp_cons _ _ (garrowfy_raw_codetypes depth t) (garrowfy_raw_codetypes_list _ depth rest)
 219     end.
 220   Definition garrowfy_code_types {Γ}{κ}(n:nat)(ht:HaskType Γ κ) : HaskType Γ κ :=
 221     fun TV ite =>
 222       garrowfy_raw_codetypes n (ht TV ite).
 223   Definition garrowfy_leveled_code_types {Γ}(n:nat)(ht:LeveledHaskType Γ ★) : LeveledHaskType Γ ★ :=
 224     match ht with htt @@ htlev => garrowfy_code_types (minus' n (length htlev)) htt @@ htlev end.
 225
 226   Axiom literal_types_unchanged : forall n Γ l, garrowfy_code_types n (literalType l) = literalType(Γ:=Γ) l.
 227
 228   Axiom flatten_coercion : forall n Γ Δ κ (σ τ:HaskType Γ κ) (γ:HaskCoercion Γ Δ (σ ∼∼∼ τ)),
 229     HaskCoercion Γ Δ (garrowfy_code_types n σ ∼∼∼ garrowfy_code_types n τ).
 230
 231   (* This tries to assign a single level to the entire succedent of a judgment.  If the succedent has types from different
 232    * levels (should not happen) it just picks one; if the succedent has no non-None leaves (also should not happen) it
 233    * picks nil *)
 234   Definition getΓ (j:Judg) := match j with Γ > _ > _ |- _ => Γ end.
 235   Definition getSuc (j:Judg) : Tree ??(LeveledHaskType (getΓ j) ★) :=
 236     match j as J return Tree ??(LeveledHaskType (getΓ J) ★) with Γ > _ > _ |- s => s end.
 237   Fixpoint getjlev {Γ}(tt:Tree ??(LeveledHaskType Γ ★)) : HaskLevel Γ :=
 238     match tt with
 239       | T_Leaf None              => nil
 240       | T_Leaf (Some (_ @@ lev)) => lev
 241       | T_Branch b1 b2 =>
 242         match getjlev b1 with
 243           | nil => getjlev b2
 244           | lev => lev
 245         end
 246     end.
 247
 248   Definition v2t {Γ}(ec:HaskTyVar Γ ★) := fun TV ite => TVar (ec TV ite).
 249
 250   (* "n" is the maximum depth remaining AFTER flattening *)
 251   Definition flatten_judgment (n:nat)(j:Judg) :=
 252     match j as J return Judg with
 253       Γ > Δ > ant |- suc =>
 254         match (match getjlev suc with
 255                  | nil        => inl _ tt
 256                  | (ec::lev') => if eqd_dec (length lev') n
 257                                  (* If the judgment's level is the deepest in the proof, flatten it by turning
 258                                   * all antecedent variables at this level into None's, garrowfying any other
 259                                   * antecedent variables (from other levels) at the same depth, and turning the
 260                                   * succedent into a garrow type *)
 261                                  then inr _ (Γ > Δ > mapOptionTree (garrowfy_leveled_code_types n) (drop_depth (ec::lev') ant)
 262                                                   |- [ga (v2t ec) (take_lev (ec::lev') ant) (mapOptionTree unlev suc) @@ lev'])
 263                                  else inl _ tt
 264                end) with
 265
 266         (* otherwise, just garrowfy all code types of the specified depth, throughout the judgment *)
 267         | inl tt => Γ > Δ > mapOptionTree (garrowfy_leveled_code_types n) ant |- mapOptionTree (garrowfy_leveled_code_types n) suc
 268         | inr r => r
 269         end
 270     end.
 271
 272   Definition boost : forall Γ Δ ant x y,
 273      ND Rule []                   [ Γ > Δ > x   |- y ] ->
 274      ND Rule [ Γ > Δ > ant |- x ] [ Γ > Δ > ant |- y ].
 275      admit.
 276      Defined.
 277
 278   Definition postcompose : ∀ Γ Δ ec lev a b c,
 279      ND Rule [] [ Γ > Δ > []                    |- [@ga Γ ec a b @@ lev] ] ->
 280      ND Rule [] [ Γ > Δ > [@ga Γ ec b c @@ lev] |- [@ga Γ ec a c @@ lev] ].
 281      admit.
 282      Defined.
 283
 284   Definition seq : ∀ Γ Δ lev a b,
 285      ND Rule [] [ Γ > Δ > [] |- [a @@ lev] ] ->
 286      ND Rule [] [ Γ > Δ > [] |- [b @@ lev] ] ->
 287      ND Rule [] [ Γ > Δ > [] |- [a @@ lev],,[b @@ lev] ].
 288      admit.
 289      Defined.
 290
 291   Lemma ga_unkappa     : ∀ Γ Δ ec l a b Σ,
 292     ND Rule
 293     [Γ > Δ > Σ |- [@ga Γ ec a  b @@ l] ]
 294     [Γ > Δ > Σ,,[@ga Γ ec [] a @@ l] |- [@ga Γ ec [] b @@ l] ].
 295     intros.
 296     set (ga_comp Γ Δ ec l [] a b) as q.
 297
 298     set (@RLet Γ Δ) as q'.
 299     set (@RLet Γ Δ [@ga _ ec [] a @@ l] Σ (@ga _ ec [] b) (@ga _ ec a b) l) as q''.
 300     eapply nd_comp.
 301     Focus 2.
 302     eapply nd_rule.
 303     eapply RArrange.
 304     apply RExch.
 305
 306     eapply nd_comp.
 307     Focus 2.
 308     eapply nd_rule.
 309     apply q''.
 310
 311     idtac.
 312     clear q'' q'.
 313     eapply nd_comp.
 314     apply nd_rlecnac.
 315     apply nd_prod.
 316     apply nd_id.
 317     apply q.
 318     Defined.
 319
 320 (*
 321   Notation "`  x" := (take_lev _ x) (at level 20).
 322   Notation "`` x" := (mapOptionTree unlev x) (at level 20).
 323   Notation "``` x" := (drop_depth _ x) (at level 20).
 324 *)
 325   Definition garrowfy_arrangement' :
 326     forall Γ (Δ:CoercionEnv Γ)
 327       (ec:HaskTyVar Γ ★) (lev:HaskLevel Γ) (ant1 ant2:Tree ??(LeveledHaskType Γ ★)) (r:Arrange ant1 ant2),
 328       ND Rule [] [Γ > Δ > [] |- [@ga _ (v2t ec) (take_lev (ec :: lev) ant2) (take_lev (ec :: lev) ant1) @@ lev] ].
 329
 330       intros Γ Δ ec lev.
 331       refine (fix garrowfy ant1 ant2 (r:Arrange ant1 ant2):
 332            ND Rule [] [Γ > Δ > [] |- [@ga _ (v2t ec) (take_lev (ec :: lev) ant2) (take_lev (ec :: lev) ant1) @@ lev]] :=
 333         match r as R in Arrange A B return
 334           ND Rule [] [Γ > Δ > [] |- [@ga _ (v2t ec) (take_lev (ec :: lev) B) (take_lev (ec :: lev) A) @@ lev]]
 335           with
 336           | RCanL  a             => let case_RCanL := tt  in ga_uncancell _ _ _ _ _
 337           | RCanR  a             => let case_RCanR := tt  in ga_uncancelr _ _ _ _ _
 338           | RuCanL a             => let case_RuCanL := tt in ga_cancell _ _ _ _ _
 339           | RuCanR a             => let case_RuCanR := tt in ga_cancelr _ _ _ _ _
 340           | RAssoc a b c         => let case_RAssoc := tt in ga_assoc _ _ _ _ _ _ _
 341           | RCossa a b c         => let case_RCossa := tt in ga_unassoc _ _ _ _ _ _ _
 342           | RExch  a b           => let case_RExch := tt  in ga_swap  _ _ _ _ _ _
 343           | RWeak  a             => let case_RWeak := tt  in ga_drop  _ _ _ _ _
 344           | RCont  a             => let case_RCont := tt  in ga_copy  _ _ _ _ _
 345           | RLeft  a b c r'      => let case_RLeft := tt  in garrowfy _ _ r' ;; boost _ _ _ _ _ (ga_second _ _ _ _ _ _ _)
 346           | RRight a b c r'      => let case_RRight := tt in garrowfy _ _ r' ;; boost _ _ _ _ _ (ga_first  _ _ _ _ _ _ _)
 347           | RComp  a b c r1 r2   => let case_RComp := tt  in (fun r1' r2' => _) (garrowfy _ _ r1) (garrowfy _ _ r2)
 348         end); clear garrowfy; repeat take_simplify; repeat drop_simplify; intros.
 349
 350         destruct case_RComp.
 351           refine ( _ ;; boost _ _ _ _ _ (ga_comp _ _ _ _ _ _ _)).
 352           apply seq.
 353           apply r2'.
 354           apply r1'.
 355           Defined.
 356
 357   Definition garrowfy_arrangement :
 358     forall Γ (Δ:CoercionEnv Γ) n
 359       (ec:HaskTyVar Γ ★) (lev:HaskLevel Γ) (ant1 ant2:Tree ??(LeveledHaskType Γ ★)) (r:Arrange ant1 ant2) succ,
 360       ND Rule
 361       [Γ > Δ > mapOptionTree (garrowfy_leveled_code_types ((length lev))) (drop_depth n ant1)
 362         |- [@ga _ (v2t ec) (take_lev (ec :: lev) ant1) (mapOptionTree unlev succ) @@ lev]]
 363       [Γ > Δ > mapOptionTree (garrowfy_leveled_code_types ((length lev))) (drop_depth n ant2)
 364         |- [@ga _ (v2t ec) (take_lev (ec :: lev) ant2) (mapOptionTree unlev succ) @@ lev]].
 365       intros.
 366       refine ( _ ;; (boost _ _ _ _ _ (postcompose _ _ _ _ _ _ _ (garrowfy_arrangement' Γ Δ ec lev ant1 ant2 r)))).
 367       apply nd_rule.
 368       apply RArrange.
 369       refine ((fix garrowfy ant1 ant2 (r:Arrange ant1 ant2) :=
 370         match r as R in Arrange A B return
 371           Arrange (mapOptionTree (garrowfy_leveled_code_types ((length lev))) (drop_depth _ A))
 372           (mapOptionTree (garrowfy_leveled_code_types ((length lev))) (drop_depth _ B)) with
 373           | RCanL  a             => let case_RCanL := tt  in RCanL _
 374           | RCanR  a             => let case_RCanR := tt  in RCanR _
 375           | RuCanL a             => let case_RuCanL := tt in RuCanL _
 376           | RuCanR a             => let case_RuCanR := tt in RuCanR _
 377           | RAssoc a b c         => let case_RAssoc := tt in RAssoc _ _ _
 378           | RCossa a b c         => let case_RCossa := tt in RCossa _ _ _
 379           | RExch  a b           => let case_RExch := tt  in RExch _ _
 380           | RWeak  a             => let case_RWeak := tt  in RWeak _
 381           | RCont  a             => let case_RCont := tt  in RCont _
 382           | RLeft  a b c r'      => let case_RLeft := tt  in RLeft  _ (garrowfy _ _ r')
 383           | RRight a b c r'      => let case_RRight := tt in RRight _ (garrowfy _ _ r')
 384           | RComp  a b c r1 r2   => let case_RComp := tt  in RComp    (garrowfy _ _ r1) (garrowfy _ _ r2)
 385         end) ant1 ant2 r); clear garrowfy; repeat take_simplify; repeat drop_simplify; intros.
 386         Defined.
 387
 388   Definition flatten_arrangement :
 389     forall n Γ Δ ant1 ant2 succ (r:Arrange ant1 ant2),
 390       ND Rule (mapOptionTree (flatten_judgment n) [Γ > Δ > ant1 |- succ])
 391       (mapOptionTree (flatten_judgment n) [Γ > Δ > ant2 |- succ]).
 392     intros.
 393     simpl.
 394     set (getjlev succ) as succ_lev.
 395     assert (succ_lev=getjlev succ).
 396       reflexivity.
 397
 398     destruct succ_lev.
 399       apply nd_rule.
 400       apply RArrange.
 401       induction r; simpl.
 402         apply RCanL.
 403         apply RCanR.
 404         apply RuCanL.
 405         apply RuCanR.
 406         apply RAssoc.
 407         apply RCossa.
 408         apply RExch.
 409         apply RWeak.
 410         apply RCont.
 411         apply RLeft; auto.
 412         apply RRight; auto.
 413         eapply RComp; [ apply IHr1 | apply IHr2 ].
 414
 415     set (Peano_dec.eq_nat_dec (Datatypes.length succ_lev) n) as lev_is_n.
 416       assert (lev_is_n=Peano_dec.eq_nat_dec (Datatypes.length succ_lev) n).
 417         reflexivity.
 418       destruct lev_is_n.
 419         rewrite <- e.
 420         apply garrowfy_arrangement.
 421         apply r.
 422         auto.
 423       apply nd_rule.
 424       apply RArrange.
 425       induction r; simpl.
 426         apply RCanL.
 427         apply RCanR.
 428         apply RuCanL.
 429         apply RuCanR.
 430         apply RAssoc.
 431         apply RCossa.
 432         apply RExch.
 433         apply RWeak.
 434         apply RCont.
 435         apply RLeft; auto.
 436         apply RRight; auto.
 437         eapply RComp; [ apply IHr1 | apply IHr2 ].
 438         Defined.
 439
 440   Definition arrange_brak : forall Γ Δ ec succ t,
 441     ND Rule
 442      [Γ > Δ >
 443       mapOptionTree (garrowfy_leveled_code_types 0) (drop_depth (ec :: nil) succ),,
 444       [(@ga _ (v2t ec) [] (take_lev (ec :: nil) succ)) @@  nil] |-
 445       [(@ga _ (v2t ec) [] [t]) @@  nil]]
 446         [Γ > Δ > mapOptionTree (garrowfy_leveled_code_types 0) succ |- [(@ga _ (v2t ec) [] [t]) @@  nil]].
 447     admit.
 448     Defined.
 449
 450   Definition arrange_esc : forall Γ Δ ec succ t,
 451     ND Rule
 452      [Γ > Δ > mapOptionTree (garrowfy_leveled_code_types 0) succ |- [(@ga _ (v2t ec) [] [t]) @@  nil]]
 453      [Γ > Δ >
 454       mapOptionTree (garrowfy_leveled_code_types 0) (drop_depth (ec :: nil) succ),,
 455       [(@ga _ (v2t ec) [] (take_lev (ec :: nil) succ)) @@  nil] |- [(@ga _ (v2t ec) [] [t]) @@  nil]].
 456     admit.
 457     Defined.
 458
 459   Lemma mapOptionTree_distributes
 460     : forall T R (a b:Tree ??T) (f:T->R),
 461       mapOptionTree f (a,,b) = (mapOptionTree f a),,(mapOptionTree f b).
 462     reflexivity.
 463     Qed.
 464
 465   Lemma garrowfy_commutes_with_substT :
 466     forall n κ Γ (Δ:CoercionEnv Γ) (σ:∀ TV, InstantiatedTypeEnv TV Γ → TV κ → RawHaskType TV ★) (τ:HaskType Γ κ),
 467     garrowfy_code_types n (substT σ τ) = substT (fun TV ite v => garrowfy_raw_codetypes n (σ TV ite v))
 468       (garrowfy_code_types n τ).
 469     admit.
 470     Qed.
 471
 472   Lemma garrowfy_commutes_with_HaskTAll :
 473     forall n κ Γ (Δ:CoercionEnv Γ) (σ:∀ TV, InstantiatedTypeEnv TV Γ → TV κ → RawHaskType TV ★),
 474     garrowfy_code_types n (HaskTAll κ σ) = HaskTAll κ (fun TV ite v => garrowfy_raw_codetypes n (σ TV ite v)).
 475     admit.
 476     Qed.
 477
 478   Lemma garrowfy_commutes_with_HaskTApp :
 479     forall n κ Γ (Δ:CoercionEnv Γ) (σ:∀ TV, InstantiatedTypeEnv TV Γ → TV κ → RawHaskType TV ★),
 480     garrowfy_code_types n (HaskTApp (weakF σ) (FreshHaskTyVar κ)) =
 481     HaskTApp (weakF (fun TV ite v => garrowfy_raw_codetypes n (σ TV ite v))) (FreshHaskTyVar κ).
 482     admit.
 483     Qed.
 484
 485   Lemma garrowfy_commutes_with_weakLT : forall (Γ:TypeEnv) κ n t,
 486     garrowfy_leveled_code_types n (weakLT(Γ:=Γ)(κ:=κ) t) = weakLT(Γ:=Γ)(κ:=κ) (garrowfy_leveled_code_types n t).
 487     admit.
 488     Qed.
 489
 490   Definition flatten_proof :
 491     forall n {h}{c},
 492       ND Rule h c ->
 493       ND Rule (mapOptionTree (flatten_judgment n) h) (mapOptionTree (flatten_judgment n) c).
 494     intros.
 495     eapply nd_map'; [ idtac | apply X ].
 496     clear h c X.
 497     intros.
 498     simpl in *.
 499
 500     refine (match X as R in Rule H C with
 501       | RArrange Γ Δ a b x d           => let case_RArrange := tt      in _
 502       | RNote    Γ Δ Σ τ l n           => let case_RNote := tt         in _
 503       | RLit     Γ Δ l     _           => let case_RLit := tt          in _
 504       | RVar     Γ Δ σ           lev   => let case_RVar := tt          in _
 505       | RGlobal  Γ Δ σ l wev           => let case_RGlobal := tt       in _
 506       | RLam     Γ Δ Σ tx te     lev   => let case_RLam := tt          in _
 507       | RCast    Γ Δ Σ σ τ lev γ       => let case_RCast := tt         in _
 508       | RAbsT    Γ Δ Σ κ σ lev         => let case_RAbsT := tt         in _
 509       | RAppT    Γ Δ Σ κ σ τ     lev   => let case_RAppT := tt         in _
 510       | RAppCo   Γ Δ Σ κ σ₁ σ₂ γ σ lev => let case_RAppCo := tt        in _
 511       | RAbsCo   Γ Δ Σ κ σ  σ₁ σ₂  lev => let case_RAbsCo := tt        in _
 512       | RApp     Γ Δ Σ₁ Σ₂ tx te lev   => let case_RApp := tt          in _
 513       | RLet     Γ Δ Σ₁ Σ₂ σ₁ σ₂ lev   => let case_RLet := tt          in _
 514       | RJoin    Γ p lri m x q         => let case_RJoin := tt in _
 515       | RVoid    _ _                   => let case_RVoid := tt   in _
 516       | RBrak    Γ Δ t ec succ lev           => let case_RBrak := tt         in _
 517       | REsc     Γ Δ t ec succ lev           => let case_REsc := tt          in _
 518       | RCase    Γ Δ lev tc Σ avars tbranches alts => let case_RCase := tt         in _
 519       | RLetRec  Γ Δ lri x y t         => let case_RLetRec := tt       in _
 520       end); clear X h c.
 521
 522     destruct case_RArrange.
 523       apply (flatten_arrangement n Γ Δ a b x d).
 524
 525     destruct case_RBrak.
 526       simpl.
 527       destruct (Peano_dec.eq_nat_dec (Datatypes.length lev) n).
 528       destruct lev.
 529       simpl.
 530       simpl.
 531       destruct n.
 532       change ([garrowfy_code_types 0 (<[ ec |- t ]>) @@  nil])
 533         with ([ga (v2t ec) [] [t] @@  nil]).
 534       refine (ga_unkappa Γ Δ (v2t ec) nil (take_lev (ec::nil) succ) [t]
 535         (mapOptionTree (garrowfy_leveled_code_types 0) (drop_depth (ec::nil) succ)) ;; _).
 536       apply arrange_brak.
 537       inversion e.
 538       apply (Prelude_error "found Brak at depth >0").
 539       apply (Prelude_error "found Brak at depth >0").
 540
 541     destruct case_REsc.
 542       simpl.
 543       destruct (Peano_dec.eq_nat_dec (Datatypes.length lev) n).
 544       destruct lev.
 545       simpl.
 546       destruct n.
 547       change ([garrowfy_code_types 0 (<[ ec |- t ]>) @@  nil])
 548         with ([ga (v2t ec) [] [t] @@  nil]).
 549       refine (_ ;; ga_kappa Γ Δ (v2t ec) nil (take_lev (ec::nil) succ) [t]
 550         (mapOptionTree (garrowfy_leveled_code_types 0) (drop_depth (ec::nil) succ))).
 551       apply arrange_esc.
 552       inversion e.
 553       apply (Prelude_error "found Esc at depth >0").
 554       apply (Prelude_error "found Esc at depth >0").
 555
 556     destruct case_RNote.
 557       simpl.
 558       destruct l; simpl.
 559         apply nd_rule; apply RNote; auto.
 560         destruct (Peano_dec.eq_nat_dec (Datatypes.length l) n).
 561         apply nd_rule; apply RNote; auto.
 562         apply nd_rule; apply RNote; auto.
 563
 564     destruct case_RLit.
 565       simpl.
 566       destruct l0; simpl.
 567         rewrite literal_types_unchanged.
 568           apply nd_rule; apply RLit.
 569         destruct (Peano_dec.eq_nat_dec (Datatypes.length l0) n); unfold mapTree; unfold mapOptionTree; simpl.
 570         unfold take_lev; simpl.
 571         unfold drop_depth; simpl.
 572         apply ga_lit.
 573         rewrite literal_types_unchanged.
 574         apply nd_rule.
 575         apply RLit.
 576
 577     destruct case_RVar.
 578       Opaque flatten_judgment.
 579       simpl.
 580       Transparent flatten_judgment.
 581       idtac.
 582       unfold flatten_judgment.
 583       unfold getjlev.
 584       destruct lev.
 585       apply nd_rule. apply RVar.
 586       destruct (eqd_dec (Datatypes.length lev) n).
 587
 588       repeat drop_simplify.
 589       repeat take_simplify.
 590       simpl.
 591       apply ga_id.
 592
 593       apply nd_rule.
 594       apply RVar.
 595
 596     destruct case_RGlobal.
 597       simpl.
 598       destruct l as [|ec lev]; simpl; [ apply nd_rule; apply RGlobal; auto | idtac ].
 599       destruct (Peano_dec.eq_nat_dec (Datatypes.length lev) n); [ idtac | apply nd_rule; apply RGlobal; auto ]; simpl.
 600       apply (Prelude_error "found RGlobal at depth >0").
 601
 602     destruct case_RLam.
 603       Opaque drop_depth.
 604       Opaque take_lev.
 605       simpl.
 606       destruct lev as [|ec lev]; simpl; [ apply nd_rule; apply RLam; auto | idtac ].
 607       destruct (Peano_dec.eq_nat_dec (Datatypes.length lev) n); [ idtac | apply nd_rule; apply RLam; auto ]; simpl.
 608       rewrite <- e.
 609       clear e n.
 610       repeat drop_simplify.
 611       repeat take_simplify.
 612       eapply nd_comp.
 613         eapply nd_rule.
 614         eapply RArrange.
 615         simpl.
 616         apply RCanR.
 617       apply boost.
 618       apply ga_curry.
 619
 620     destruct case_RCast.
 621       simpl.
 622       destruct lev as [|ec lev]; simpl; [ apply nd_rule; apply RCast; auto | idtac ].
 623       apply flatten_coercion; auto.
 624       destruct (Peano_dec.eq_nat_dec (Datatypes.length lev) n); [ idtac | apply nd_rule; apply RCast; auto ]; simpl.
 625       apply (Prelude_error "RCast at level >0").
 626       apply flatten_coercion; auto.
 627
 628     destruct case_RJoin.
 629       simpl.
 630       destruct (getjlev x); destruct (getjlev q).
 631       apply nd_rule.
 632       apply RJoin.
 633       apply (Prelude_error "RJoin at depth >0").
 634       apply (Prelude_error "RJoin at depth >0").
 635       apply (Prelude_error "RJoin at depth >0").
 636
 637     destruct case_RApp.
 638       simpl.
 639
 640       destruct lev as [|ec lev]. simpl. apply nd_rule.
 641         replace (garrowfy_code_types n (tx ---> te)) with ((garrowfy_code_types n tx) ---> (garrowfy_code_types n te)).
 642         apply RApp.
 643         unfold garrowfy_code_types.
 644         simpl.
 645         reflexivity.
 646
 647         destruct (Peano_dec.eq_nat_dec (Datatypes.length lev) n).
 648           eapply nd_comp.
 649           eapply nd_rule.
 650           apply RJoin.
 651           repeat drop_simplify.
 652           repeat take_simplify.
 653           apply boost.
 654           apply ga_apply.
 655
 656           replace (garrowfy_code_types (minus' n (length (ec::lev))) (tx ---> te))
 657             with ((garrowfy_code_types (minus' n (length (ec::lev))) tx) --->
 658               (garrowfy_code_types (minus' n (length (ec::lev))) te)).
 659           apply nd_rule.
 660           apply RApp.
 661           unfold garrowfy_code_types.
 662           simpl.
 663           reflexivity.
 664 (*
 665   Notation "`  x" := (take_lev _ x) (at level 20).
 666   Notation "`` x" := (mapOptionTree unlev x) (at level 20).
 667   Notation "``` x" := ((drop_depth _ x)) (at level 20).
 668   Notation "!<[]> x" := (garrowfy_code_types _ x) (at level 1).
 669   Notation "!<[@]>" := (garrowfy_leveled_code_types _) (at level 1).
 670 *)
 671     destruct case_RLet.
 672       simpl.
 673       destruct lev as [|ec lev]; simpl; [ apply nd_rule; apply RLet; auto | idtac ].
 674       destruct (Peano_dec.eq_nat_dec (Datatypes.length lev) n); [ idtac | apply nd_rule; apply RLet; auto ]; simpl.
 675       repeat drop_simplify.
 676       repeat take_simplify.
 677       rename σ₁ into a.
 678       rename σ₂ into b.
 679       rewrite mapOptionTree_distributes.
 680       rewrite mapOptionTree_distributes.
 681       set (mapOptionTree (garrowfy_leveled_code_types (S n)) (drop_depth (ec :: lev) Σ₁)) as A.
 682       set (take_lev (ec :: lev) Σ₁) as A'.
 683       set (mapOptionTree (garrowfy_leveled_code_types (S n)) (drop_depth (ec :: lev) Σ₂)) as B.
 684       set (take_lev (ec :: lev) Σ₂) as B'.
 685       simpl.
 686
 687       eapply nd_comp.
 688       Focus 2.
 689       eapply nd_rule.
 690       eapply RLet.
 691
 692       apply nd_prod.
 693
 694       apply boost.
 695       apply ga_second.
 696
 697       eapply nd_comp.
 698       Focus 2.
 699       eapply boost.
 700       apply ga_comp.
 701
 702       eapply nd_comp.
 703       eapply nd_rule.
 704       eapply RArrange.
 705       eapply RCanR.
 706
 707       eapply nd_comp.
 708       Focus 2.
 709       eapply nd_rule.
 710       eapply RArrange.
 711       eapply RExch.
 712       idtac.
 713
 714       eapply nd_comp.
 715       apply nd_llecnac.
 716       eapply nd_comp.
 717       Focus 2.
 718       eapply nd_rule.
 719       apply RJoin.
 720       apply nd_prod.
 721
 722       eapply nd_rule.
 723       eapply RVar.
 724
 725       apply nd_id.
 726
 727     destruct case_RVoid.
 728       simpl.
 729       apply nd_rule.
 730       apply RVoid.
 731
 732     destruct case_RAppT.
 733       simpl. destruct lev; simpl.
 734       rewrite garrowfy_commutes_with_HaskTAll.
 735       rewrite garrowfy_commutes_with_substT.
 736       apply nd_rule.
 737       apply RAppT.
 738       apply Δ.
 739       apply Δ.
 740       apply (Prelude_error "AppT at depth>0").
 741
 742     destruct case_RAbsT.
 743       simpl. destruct lev; simpl.
 744       rewrite garrowfy_commutes_with_HaskTAll.
 745       rewrite garrowfy_commutes_with_HaskTApp.
 746       eapply nd_comp; [ idtac | eapply nd_rule; eapply RAbsT ].
 747       simpl.
 748       set (mapOptionTree (garrowfy_leveled_code_types n) (mapOptionTree (weakLT(κ:=κ)) Σ)) as a.
 749       set (mapOptionTree (weakLT(κ:=κ)) (mapOptionTree (garrowfy_leveled_code_types n) Σ)) as q'.
 750       assert (a=q').
 751         unfold a.
 752         unfold q'.
 753         clear a q'.
 754         induction Σ.
 755           destruct a.
 756           simpl.
 757           rewrite garrowfy_commutes_with_weakLT.
 758           reflexivity.
 759           reflexivity.
 760           simpl.
 761           rewrite <- IHΣ1.
 762           rewrite <- IHΣ2.
 763           reflexivity.
 764       rewrite H.
 765       apply nd_id.
 766       apply Δ.
 767       apply Δ.
 768       apply (Prelude_error "AbsT at depth>0").
 769
 770     destruct case_RAppCo.
 771       simpl. destruct lev; simpl.
 772       unfold garrowfy_code_types.
 773       simpl.
 774       apply nd_rule.
 775       apply RAppCo.
 776       apply flatten_coercion.
 777       apply γ.
 778       apply (Prelude_error "AppCo at depth>0").
 779
 780     destruct case_RAbsCo.
 781       simpl. destruct lev; simpl.
 782       unfold garrowfy_code_types.
 783       simpl.
 784       apply (Prelude_error "AbsCo not supported (FIXME)").
 785       apply (Prelude_error "AbsCo at depth>0").
 786
 787     destruct case_RLetRec.
 788       rename t into lev.
 789       apply (Prelude_error "LetRec not supported (FIXME)").
 790
 791     destruct case_RCase.
 792       simpl.
 793       apply (Prelude_error "Case not supported (FIXME)").
 794       Defined.
 795
 796
 797   (* to do: establish some metric on judgments (max length of level of any succedent type, probably), show how to
 798    * calculate it, and show that the flattening procedure above drives it down by one *)
 799
 800   (*
 801   Instance FlatteningFunctor {Γ}{Δ}{ec} : Functor (JudgmentsL (PCF Γ Δ ec)) (TypesL (SystemFCa Γ Δ)) (obact) :=
 802     { fmor := FlatteningFunctor_fmor }.
 803
 804   Definition ReificationFunctor Γ Δ : Functor (JudgmentsL _ _ (PCF n Γ Δ)) SystemFCa' (mapOptionTree brakifyJudg).
 805     refine {| fmor := ReificationFunctor_fmor Γ Δ |}; unfold hom; unfold ob; simpl ; intros.
 806
 807   Definition PCF_SMME (n:nat)(Γ:TypeEnv)(Δ:CoercionEnv Γ) : ProgrammingLanguageSMME.
 808     refine {| plsmme_pl := PCF n Γ Δ |}.
 809     Defined.
 810
 811   Definition SystemFCa_SMME (n:nat)(Γ:TypeEnv)(Δ:CoercionEnv Γ) : ProgrammingLanguageSMME.
 812     refine {| plsmme_pl := SystemFCa n Γ Δ |}.
 813     Defined.
 814
 815   Definition ReificationFunctorMonoidal n : MonoidalFunctor (JudgmentsN n) (JudgmentsN (S n)) (ReificationFunctor n).
 816     Defined.
 817
 818   (* 5.1.4 *)
 819   Definition PCF_SystemFCa_two_level n Γ Δ : TwoLevelLanguage (PCF_SMME n Γ Δ) (SystemFCa_SMME (S n) Γ Δ).
 820     Defined.
 821   *)
 822   (*  ... and the retraction exists *)
 823
 824 End HaskFlattener.
 825
 826 Implicit Arguments garrow [ ].