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   (* In a tree of types, replace any type at level "lev" with None *)
  65   Definition drop_lev {Γ}(lev:HaskLevel Γ)(tt:Tree ??(LeveledHaskType Γ ★)) : Tree ??(LeveledHaskType Γ ★) :=
  66     mapTree (fun t => match t with
  67                         | Some (ttype @@ tlev) => if eqd_dec tlev lev then None else t
  68                         | _ => t
  69                       end) tt.
  70   (* The opposite: replace any type which is NOT at level "lev" with None *)
  71   Definition take_lev {Γ}(lev:HaskLevel Γ)(tt:Tree ??(LeveledHaskType Γ ★)) : Tree ??(HaskType Γ ★) :=
  72     mapTree (fun t => match t with
  73                         | Some (ttype @@ tlev) => if eqd_dec tlev lev then Some ttype else None
  74                         | _                    => None
  75                       end) tt.
  76
  77   (* In a tree of types, replace any type at depth "lev" or greater None *)
  78   Definition drop_depth {Γ}(n:nat)(tt:Tree ??(LeveledHaskType Γ ★)) : Tree ??(LeveledHaskType Γ ★) :=
  79     mapTree (fun t => match t with
  80                         | Some (ttype @@ tlev) => if eqd_dec (length tlev) n then None else t
  81                         | _ => t
  82                       end) tt.
  83
  84   (* delete from the tree any type which is NOT at level "lev" *)
  85
  86   Fixpoint take_lev' {Γ}(lev:HaskLevel Γ)(tt:Tree ??(LeveledHaskType Γ ★)) : ??(Tree ??(HaskType Γ ★)) :=
  87     match tt with
  88       | T_Leaf   None  => Some (T_Leaf None)    (* FIXME: unsure of this; it ends up on both sides *)
  89       | T_Branch b1 b2 =>
  90         let b1' := take_lev' lev b1 in
  91           let b2' := take_lev' lev b2 in
  92             match b1' with
  93               | None => b2'
  94               | Some b1'' => match b2' with
  95                                | None => Some b1''
  96                                | Some b2'' => Some (b1'',,b2'')
  97                              end
  98             end
  99       | T_Leaf   (Some (ttype@@tlev))  =>
 100                 if eqd_dec tlev lev
 101                   then Some [ttype]
 102                   else None
 103     end.
 104
 105   Context (ga' : forall TV, TV ★ -> Tree ??(RawHaskType TV ★) -> Tree ??(RawHaskType TV ★) -> RawHaskType TV ★).
 106
 107   Definition ga : forall Γ, HaskTyVar Γ ★ -> Tree ??(HaskType Γ ★) -> Tree ??(HaskType Γ ★) -> HaskType Γ ★
 108     := fun Γ ec ant suc =>
 109       fun TV ite =>
 110         ga'
 111         TV
 112         (ec TV ite)
 113         (mapOptionTree (fun x => x TV ite) ant)
 114         (mapOptionTree (fun x => x TV ite) suc).
 115
 116   Implicit Arguments ga [ [Γ] ].
 117   Notation "a ~~~~> b" := (@ga _ _ a b) (at level 20).
 118
 119   Context (unit_type : forall TV, RawHaskType TV ★).
 120
 121   (*
 122    *  The story:
 123    *    - code types <[t]>@c                                                become garrows  c () t
 124    *    - free variables of type t at a level lev deeper than the succedent become garrows  c () t
 125    *    - free variables at the level of the succedent become
 126    *)
 127   Fixpoint flatten_rawtype {TV}{κ}(depth:nat)(exp: RawHaskType TV κ) : RawHaskType TV κ :=
 128     match exp with
 129     | TVar    _  x        => TVar x
 130     | TAll     _ y        => TAll   _  (fun v => flatten_rawtype depth (y v))
 131     | TApp   _ _ x y      => TApp      (flatten_rawtype depth x) (flatten_rawtype depth y)
 132     | TCon       tc       => TCon      tc
 133     | TCoerc _ t1 t2 t    => TCoerc    (flatten_rawtype depth t1) (flatten_rawtype depth t2) (flatten_rawtype depth t)
 134     | TArrow              => TArrow
 135     | TCode      v e      => match depth with
 136                                | O => match v return RawHaskType TV ★ with
 137                                         | TVar ★ ec => ga' TV ec [] [flatten_rawtype depth e]
 138                                         | _         => unit_type TV
 139                                       end
 140                                | (S depth') => TCode v (flatten_rawtype depth' e)
 141                              end
 142     | TyFunApp     tfc lt => TyFunApp tfc (flatten_rawtype_list _ depth lt)
 143     end
 144     with flatten_rawtype_list {TV}(lk:list Kind)(depth:nat)(exp:@RawHaskTypeList TV lk) : @RawHaskTypeList TV lk :=
 145     match exp in @RawHaskTypeList _ LK return @RawHaskTypeList TV LK with
 146     | TyFunApp_nil               => TyFunApp_nil
 147     | TyFunApp_cons  κ kl t rest => TyFunApp_cons _ _ (flatten_rawtype depth t) (flatten_rawtype_list _ depth rest)
 148     end.
 149
 150   Inductive AllT {T:Type}{P:T->Prop} : Tree ??T -> Prop :=
 151     | allt_none   :                  AllT []
 152     | allt_some   : forall t, P t -> AllT [t]
 153     | allt_branch : forall b1 b2, AllT b1 -> AllT b2 -> AllT (b1,,b2)
 154     .
 155   Implicit Arguments AllT [[T]].
 156
 157   Definition getΓ (j:Judg) := match j with Γ > _ > _ |- _ => Γ end.
 158
 159   Definition getSuc (j:Judg) : Tree ??(LeveledHaskType (getΓ j) ★) :=
 160     match j as J return Tree ??(LeveledHaskType (getΓ J) ★) with
 161       Γ > _ > _ |- s => s
 162         end.
 163
 164   Definition getlev {Γ}{κ}(lht:LeveledHaskType Γ κ) :=
 165     match lht with t@@l => l end.
 166
 167   (* This tries to assign a single level to the entire succedent of a judgment.  If the succedent has types from different
 168    * levels (should not happen) it just picks one; if the succedent has no non-None leaves (also should not happen) it
 169    * picks nil *)
 170   Fixpoint getjlev {Γ}(tt:Tree ??(LeveledHaskType Γ ★)) : HaskLevel Γ :=
 171     match tt with
 172       | T_Leaf None              => nil
 173       | T_Leaf (Some (_ @@ lev)) => lev
 174       | T_Branch b1 b2 =>
 175         match getjlev b1 with
 176           | nil => getjlev b2
 177           | lev => lev
 178         end
 179     end.
 180
 181   (* an XJudg is a Judg for which the SUCCEDENT types all come from the same level, and that level is no deeper than "n" *)
 182   (* even the empty succedent [] has a level... *)
 183   Definition QJudg (n:nat)(j:Judg) := le (length (getjlev (getSuc j))) n.
 184
 185 (*  Definition qjudg2judg {n}(qj:QJudg n) : Judg := projT1 qj.*)
 186
 187   Inductive QRule : nat -> Tree ??Judg -> Tree ??Judg -> Type :=
 188     mkQRule : forall n h c,
 189       Rule h c ->
 190       ITree _ (QJudg n) h ->
 191       ITree _ (QJudg n) c ->
 192       QRule n h c.
 193
 194   Definition QND n := ND (QRule n).
 195
 196   (*
 197    * Any type   "t"   at a level with length "n"   becomes (g () t)
 198    * Any type "<[t]>" at a level with length "n-1" becomes (g () t)
 199    *)
 200
 201   Definition flatten_type {Γ}(n:nat)(ht:HaskType Γ ★) : HaskType Γ ★ :=
 202     fun TV ite =>
 203       flatten_rawtype n (ht TV ite).
 204
 205   Definition minus' n m :=
 206     match m with
 207       | 0 => n
 208       | _ => n - m
 209     end.
 210
 211   (* to do: integrate this more cleanly with qjudg *)
 212   Definition flatten_leveled_type {Γ}(n:nat)(ht:LeveledHaskType Γ ★) : LeveledHaskType Γ ★ :=
 213     match ht with
 214       htt @@ htlev =>
 215       flatten_type (minus' n (length htlev)) htt @@ htlev
 216     end.
 217
 218   Definition flatten_qjudg_ok (n:nat)(j:Judg) : Judg :=
 219     match j with
 220       Γ > Δ > ant |- suc =>
 221         let ant' := mapOptionTree (flatten_leveled_type n) ant in
 222           let suc' := mapOptionTree (flatten_leveled_type n) suc
 223             in  (Γ > Δ > ant' |- suc')
 224     end.
 225
 226   Definition take_lev'' {Γ}(lev:HaskLevel Γ)(tt:Tree ??(LeveledHaskType Γ ★)) : Tree ??(HaskType Γ ★) :=
 227     match (take_lev' lev tt) with
 228       | None => []
 229       | Some x => x
 230     end.
 231
 232   Definition flatten_qjudg : forall (n:nat), Judg -> Judg.
 233     refine (fun {n}{j} =>
 234       match j as J return Judg with
 235         Γ > Δ > ant |- suc =>
 236           match getjlev suc with
 237             | nil        => flatten_qjudg_ok n j
 238             | (ec::lev') => if eqd_dec (length lev') n
 239                             then let ant_host    := drop_depth (S n) ant in
 240                                    let ant_guest := take_lev (ec::lev') ant in  (* FIXME: I want take_lev''!!!!! *)
 241                                      (Γ > Δ > ant_host |- [ga ec ant_guest (mapOptionTree unlev suc) @@ lev'])
 242                             else flatten_qjudg_ok n j
 243           end
 244       end).
 245     Defined.
 246
 247   Axiom literal_types_unchanged : forall n Γ l, flatten_type n (literalType l) = literalType(Γ:=Γ) l.
 248
 249   Lemma drop_depth_lemma : forall Γ (lev:HaskLevel Γ) x, drop_depth (length lev) [x @@  lev] = [].
 250     admit.
 251     Defined.
 252
 253   Lemma drop_depth_lemma_s : forall Γ (lev:HaskLevel Γ) ec x, drop_depth (S (length lev)) [x @@  (ec :: lev)] = [].
 254     admit.
 255     Defined.
 256
 257   Ltac drop_simplify :=
 258     match goal with
 259       | [ |- context[@drop_depth ?G (length ?L) [ ?X @@ ?L ] ] ] =>
 260         rewrite (drop_depth_lemma G L X)
 261       | [ |- context[@drop_depth ?G (S (length ?L)) [ ?X @@ (?E :: ?L) ] ] ] =>
 262         rewrite (drop_depth_lemma_s G L E X)
 263       | [ |- context[@drop_depth ?G ?N (?A,,?B)] ] =>
 264       change (@drop_depth G N (A,,B)) with ((@drop_depth G N A),,(@drop_depth G N B))
 265       | [ |- context[@drop_depth ?G ?N (T_Leaf None)] ] =>
 266       change (@drop_depth G N (T_Leaf (@None (LeveledHaskType G ★)))) with (T_Leaf (@None (LeveledHaskType G ★)))
 267     end.
 268
 269   Lemma take_lemma : forall Γ (lev:HaskLevel Γ) x, take_lev lev [x @@  lev] = [x].
 270     admit.
 271     Defined.
 272
 273   Ltac take_simplify :=
 274     match goal with
 275       | [ |- context[@take_lev ?G ?L [ ?X @@ ?L ] ] ] =>
 276         rewrite (take_lemma G L X)
 277       | [ |- context[@take_lev ?G ?N (?A,,?B)] ] =>
 278       change (@take_lev G N (A,,B)) with ((@take_lev G N A),,(@take_lev G N B))
 279       | [ |- context[@take_lev ?G ?N (T_Leaf None)] ] =>
 280       change (@take_lev G N (T_Leaf (@None (LeveledHaskType G ★)))) with (T_Leaf (@None (LeveledHaskType G ★)))
 281     end.
 282
 283   Class garrow :=
 284   { ga_id        : ∀ Γ Δ ec lev a    , ND Rule [] [Γ > Δ >                                           [] |- [@ga Γ ec a a @@ lev] ]
 285   ; ga_comp      : ∀ Γ Δ ec lev a b c, ND Rule [] [Γ > Δ > [@ga Γ ec a b @@ lev],,[@ga Γ ec b c @@ lev] |- [@ga Γ ec a c @@ lev] ]
 286   ; ga_cancelr   : ∀ Γ Δ ec lev a    , ND Rule [] [Γ > Δ >                                           [] |- [@ga Γ ec (a,,[]) a @@ lev] ]
 287   ; ga_cancell   : ∀ Γ Δ ec lev a    , ND Rule [] [Γ > Δ >                                           [] |- [@ga Γ ec ([],,a) a @@ lev] ]
 288   ; ga_uncancelr : ∀ Γ Δ ec lev a    , ND Rule [] [Γ > Δ >                                           [] |- [@ga Γ ec a (a,,[]) @@ lev] ]
 289   ; ga_uncancell : ∀ Γ Δ ec lev a    , ND Rule [] [Γ > Δ >                                           [] |- [@ga Γ ec a ([],,a) @@ lev] ]
 290   ; ga_assoc     : ∀ Γ Δ ec lev a b c, ND Rule [] [Γ > Δ >                                           [] |- [@ga Γ ec ((a,,b),,c) (a,,(b,,c)) @@ lev] ]
 291   ; ga_unassoc   : ∀ Γ Δ ec lev a b c, ND Rule [] [Γ > Δ >                                           [] |- [@ga Γ ec (a,,(b,,c)) ((a,,b),,c) @@ lev] ]
 292   ; ga_swap      : ∀ Γ Δ ec lev a b  , ND Rule [] [Γ > Δ >                                           [] |- [@ga Γ ec (a,,b) (b,,a) @@ lev] ]
 293   ; ga_drop      : ∀ Γ Δ ec lev a    , ND Rule [] [Γ > Δ >                                           [] |- [@ga Γ ec a [] @@ lev] ]
 294   ; ga_copy      : ∀ Γ Δ ec lev a    , ND Rule [] [Γ > Δ >                                           [] |- [@ga Γ ec a (a,,a) @@ lev] ]
 295   ; ga_first     : ∀ Γ Δ ec lev a b x, ND Rule [] [Γ > Δ >                        [@ga Γ ec a b @@ lev] |- [@ga Γ ec (a,,x) (b,,x) @@ lev] ]
 296   ; ga_second    : ∀ Γ Δ ec lev a b x, ND Rule [] [Γ > Δ >                        [@ga Γ ec a b @@ lev] |- [@ga Γ ec (x,,a) (x,,b) @@ lev] ]
 297   ; ga_lit       : ∀ Γ Δ ec lev lit  , ND Rule [] [Γ > Δ >                                           [] |- [@ga Γ ec [] [literalType lit] @@ lev] ]
 298   ; ga_curry     : ∀ Γ Δ ec lev a b c, ND Rule [] [Γ > Δ >               [@ga Γ ec (a,,[b]) [c] @@ lev] |- [@ga Γ ec a [b ---> c] @@ lev] ]
 299   ; ga_apply     : ∀ Γ Δ ec lev a a' b c, ND Rule [] [Γ > Δ >
 300     [@ga Γ ec a [b ---> c] @@ lev],,[@ga Γ ec a' [b] @@ lev]
 301     |-
 302     [@ga Γ ec (a,,a') [c] @@ lev] ]
 303   }.
 304
 305   Context (gar:garrow).
 306
 307   Definition boost : forall Γ Δ ant x y,
 308      ND Rule []                   [ Γ > Δ > x   |- y ] ->
 309      ND Rule [ Γ > Δ > ant |- x ] [ Γ > Δ > ant |- y ].
 310      admit.
 311      Defined.
 312   Definition postcompose : ∀ Γ Δ ec lev a b c,
 313      ND Rule [] [ Γ > Δ > []                    |- [@ga Γ ec a b @@ lev] ] ->
 314      ND Rule [] [ Γ > Δ > [@ga Γ ec b c @@ lev] |- [@ga Γ ec a c @@ lev] ].
 315      admit.
 316      Defined.
 317   Definition precompose : ∀ Γ Δ lev a b c x,
 318      ND Rule [] [ Γ > Δ > a |- x,,[b @@ lev] ] ->
 319      ND Rule [] [ Γ > Δ > [b @@ lev] |- [c @@ lev] ] ->
 320      ND Rule [] [ Γ > Δ > a,,x |- [c @@ lev] ].
 321      admit.
 322      Defined.
 323
 324   Set Printing Width 130.
 325
 326   Definition garrowfy_arrangement' :
 327     forall Γ (Δ:CoercionEnv Γ)
 328       (ec:HaskTyVar Γ ★) (lev:HaskLevel Γ) (ant1 ant2:Tree ??(LeveledHaskType Γ ★)) (r:Arrange ant1 ant2),
 329       ND Rule [] [Γ > Δ > [] |- [@ga _ ec (take_lev (ec :: lev) ant2) (take_lev (ec :: lev) ant1) @@ lev] ].
 330
 331       intros Γ Δ ec lev.
 332       refine (fix garrowfy ant1 ant2 (r:Arrange ant1 ant2):
 333            ND Rule [] [Γ > Δ > [] |- [@ga _ ec (take_lev (ec :: lev) ant2) (take_lev (ec :: lev) ant1) @@ lev]] :=
 334         match r as R in Arrange A B return
 335           ND Rule [] [Γ > Δ > [] |- [@ga _ ec (take_lev (ec :: lev) B) (take_lev (ec :: lev) A) @@ lev]]
 336           with
 337           | RCanL  a             => let case_RCanL := tt  in ga_uncancell _ _ _ _ _
 338           | RCanR  a             => let case_RCanR := tt  in ga_uncancelr _ _ _ _ _
 339           | RuCanL a             => let case_RuCanL := tt in ga_cancell _ _ _ _ _
 340           | RuCanR a             => let case_RuCanR := tt in ga_cancelr _ _ _ _ _
 341           | RAssoc a b c         => let case_RAssoc := tt in ga_assoc _ _ _ _ _ _ _
 342           | RCossa a b c         => let case_RCossa := tt in ga_unassoc _ _ _ _ _ _ _
 343           | RExch  a b           => let case_RExch := tt  in ga_swap  _ _ _ _ _ _
 344           | RWeak  a             => let case_RWeak := tt  in ga_drop  _ _ _ _ _
 345           | RCont  a             => let case_RCont := tt  in ga_copy  _ _ _ _ _
 346           | RLeft  a b c r'      => let case_RLeft := tt  in garrowfy _ _ r' ;; boost _ _ _ _ _ (ga_second _ _ _ _ _ _ _)
 347           | RRight a b c r'      => let case_RRight := tt in garrowfy _ _ r' ;; boost _ _ _ _ _ (ga_first  _ _ _ _ _ _ _)
 348           | RComp  a b c r1 r2   => let case_RComp := tt  in (fun r1' r2' => _) (garrowfy _ _ r1) (garrowfy _ _ r2)
 349         end); clear garrowfy; repeat take_simplify; repeat drop_simplify; intros.
 350
 351         destruct case_RComp.
 352           (*
 353           set (ga_comp Γ Δ ec lev (``c) (``b) (``a)) as q.
 354           eapply precompose.
 355           Focus 2.
 356           apply q.
 357           refine ( _ ;; boost _ _ _ _ _ (ga_comp _ _ _ _ _ _ _)).
 358           apply precompose.
 359           Focus 2.
 360           eapply ga_comp.
 361           *)
 362           admit.
 363           Defined.
 364
 365   Definition garrowfy_arrangement :
 366     forall Γ (Δ:CoercionEnv Γ) n
 367       (ec:HaskTyVar Γ ★) (lev:HaskLevel Γ) (ant1 ant2:Tree ??(LeveledHaskType Γ ★)) (r:Arrange ant1 ant2) succ,
 368       (*ec :: lev = getjlev succ ->*)
 369       (* H0 : left (Datatypes.length lev ≠ n) e = Peano_dec.eq_nat_dec (Datatypes.length lev) n *)
 370       ND Rule
 371       [Γ > Δ > drop_depth n ant1 |- [@ga _ ec (take_lev (ec :: lev) ant1) (mapOptionTree unlev succ) @@ lev]]
 372       [Γ > Δ > drop_depth n ant2 |- [@ga _ ec (take_lev (ec :: lev) ant2) (mapOptionTree unlev succ) @@ lev]].
 373       intros.
 374       refine ( _ ;; (boost _ _ _ _ _ (postcompose _ _ _ _ _ _ _ (garrowfy_arrangement' Γ Δ ec lev ant1 ant2 r)))).
 375       apply nd_rule.
 376       apply RArrange.
 377       refine ((fix garrowfy ant1 ant2 (r:Arrange ant1 ant2) :=
 378         match r as R in Arrange A B return Arrange (drop_depth _ A) (drop_depth _ B) with
 379           | RCanL  a             => let case_RCanL := tt  in RCanL _
 380           | RCanR  a             => let case_RCanR := tt  in RCanR _
 381           | RuCanL a             => let case_RuCanL := tt in RuCanL _
 382           | RuCanR a             => let case_RuCanR := tt in RuCanR _
 383           | RAssoc a b c         => let case_RAssoc := tt in RAssoc _ _ _
 384           | RCossa a b c         => let case_RCossa := tt in RCossa _ _ _
 385           | RExch  a b           => let case_RExch := tt  in RExch _ _
 386           | RWeak  a             => let case_RWeak := tt  in RWeak _
 387           | RCont  a             => let case_RCont := tt  in RCont _
 388           | RLeft  a b c r'      => let case_RLeft := tt  in RLeft  _ (garrowfy _ _ r')
 389           | RRight a b c r'      => let case_RRight := tt in RRight _ (garrowfy _ _ r')
 390           | RComp  a b c r1 r2   => let case_RComp := tt  in RComp    (garrowfy _ _ r1) (garrowfy _ _ r2)
 391         end) ant1 ant2 r); clear garrowfy; repeat take_simplify; repeat drop_simplify; intros.
 392         Defined.
 393
 394   Definition flatten_arrangement :
 395     forall n Γ Δ ant1 ant2 succ (r:Arrange ant1 ant2),
 396       ND Rule (mapOptionTree (flatten_qjudg n) [Γ > Δ > ant1 |- succ])
 397       (mapOptionTree (flatten_qjudg n) [Γ > Δ > ant2 |- succ]).
 398     intros.
 399     simpl.
 400     set (getjlev succ) as succ_lev.
 401     assert (succ_lev=getjlev succ).
 402       reflexivity.
 403
 404     destruct succ_lev.
 405       apply nd_rule.
 406       apply RArrange.
 407       induction r; simpl.
 408         apply RCanL.
 409         apply RCanR.
 410         apply RuCanL.
 411         apply RuCanR.
 412         apply RAssoc.
 413         apply RCossa.
 414         apply RExch.
 415         apply RWeak.
 416         apply RCont.
 417         apply RLeft; auto.
 418         apply RRight; auto.
 419         eapply RComp; [ apply IHr1 | apply IHr2 ].
 420
 421     set (Peano_dec.eq_nat_dec (Datatypes.length succ_lev) n) as lev_is_n.
 422       assert (lev_is_n=Peano_dec.eq_nat_dec (Datatypes.length succ_lev) n).
 423         reflexivity.
 424       destruct lev_is_n.
 425         rewrite <- e.
 426         apply garrowfy_arrangement.
 427         apply r.
 428         auto.
 429       apply nd_rule.
 430       apply RArrange.
 431       induction r; simpl.
 432         apply RCanL.
 433         apply RCanR.
 434         apply RuCanL.
 435         apply RuCanR.
 436         apply RAssoc.
 437         apply RCossa.
 438         apply RExch.
 439         apply RWeak.
 440         apply RCont.
 441         apply RLeft; auto.
 442         apply RRight; auto.
 443         eapply RComp; [ apply IHr1 | apply IHr2 ].
 444         Defined.
 445
 446   Lemma flatten_coercion : forall n Γ Δ σ τ (γ:HaskCoercion Γ Δ (σ ∼∼∼ τ)),
 447     HaskCoercion Γ Δ (flatten_type n σ ∼∼∼ flatten_type n τ).
 448     admit.
 449     Defined.
 450
 451   Ltac eqd_dec_refl' :=
 452     match goal with
 453       | [ |- context[@eqd_dec ?T ?V ?X ?X] ] =>
 454         destruct (@eqd_dec T V X X) as [eqd_dec1 | eqd_dec2];
 455           [ clear eqd_dec1 | set (eqd_dec2 (refl_equal _)) as eqd_dec2'; inversion eqd_dec2' ]
 456   end.
 457
 458
 459 (*
 460   Lemma foog : forall Γ Δ,
 461     ND Rule
 462     ( [ Γ > Δ > Σ₁ |- a ],,[ Γ > Δ > Σ₂ |- b ] )
 463       [ Γ > Δ > Σ₁,,Σ₂ |- a,,b ]
 464 *)
 465
 466   Notation "`  x" := (take_lev _ x) (at level 20).
 467   Notation "`` x" := (mapOptionTree unlev x) (at level 20).
 468   Notation "``` x" := (drop_depth _ x) (at level 20).
 469
 470   Definition flatten :
 471     forall n {h}{c},
 472       QND (S n) h c ->
 473       ND Rule (mapOptionTree (flatten_qjudg n) h) (mapOptionTree (flatten_qjudg n) c).
 474     intros.
 475     eapply nd_map'; [ idtac | apply X ].
 476     clear h c X.
 477     intros.
 478     simpl in *.
 479
 480     inversion X.
 481     subst.
 482     refine (match X0 as R in Rule H C with
 483       | RArrange Γ Δ a b x d           => let case_RArrange := tt      in _
 484       | RNote    Γ Δ Σ τ l n           => let case_RNote := tt         in _
 485       | RLit     Γ Δ l     _           => let case_RLit := tt          in _
 486       | RVar     Γ Δ σ           lev   => let case_RVar := tt          in _
 487       | RGlobal  Γ Δ σ l wev           => let case_RGlobal := tt       in _
 488       | RLam     Γ Δ Σ tx te     lev   => let case_RLam := tt          in _
 489       | RCast    Γ Δ Σ σ τ lev γ       => let case_RCast := tt         in _
 490       | RAbsT    Γ Δ Σ κ σ lev         => let case_RAbsT := tt         in _
 491       | RAppT    Γ Δ Σ κ σ τ     lev   => let case_RAppT := tt         in _
 492       | RAppCo   Γ Δ Σ κ σ₁ σ₂ γ σ lev => let case_RAppCo := tt        in _
 493       | RAbsCo   Γ Δ Σ κ σ  σ₁ σ₂  lev => let case_RAbsCo := tt        in _
 494       | RApp     Γ Δ Σ₁ Σ₂ tx te lev   => let case_RApp := tt          in _
 495       | RLet     Γ Δ Σ₁ Σ₂ σ₁ σ₂ lev   => let case_RLet := tt          in _
 496       | RJoin    Γ p lri m x q         => let case_RJoin := tt in _
 497       | RVoid    _ _                   => let case_RVoid := tt   in _
 498       | RBrak    Σ a b c n m           => let case_RBrak := tt         in _
 499       | REsc     Σ a b c n m           => let case_REsc := tt          in _
 500       | RCase    Γ Δ lev tc Σ avars tbranches alts => let case_RCase := tt         in _
 501       | RLetRec  Γ Δ lri x y t         => let case_RLetRec := tt       in _
 502       end); clear X X0 X1 X2 h c.
 503
 504     destruct case_RArrange.
 505       apply (flatten_arrangement n Γ Δ a b x d).
 506
 507     destruct case_RBrak.
 508       admit.
 509
 510     destruct case_REsc.
 511       admit.
 512
 513     destruct case_RNote.
 514       simpl.
 515       destruct l; simpl.
 516         apply nd_rule; apply RNote; auto.
 517         destruct (Peano_dec.eq_nat_dec (Datatypes.length l) n).
 518         apply nd_rule; apply RNote; auto.
 519         apply nd_rule; apply RNote; auto.
 520
 521     destruct case_RLit.
 522       simpl.
 523       destruct l0; simpl.
 524         rewrite literal_types_unchanged.
 525           apply nd_rule; apply RLit.
 526         destruct (Peano_dec.eq_nat_dec (Datatypes.length l0) n); unfold mapTree; unfold mapOptionTree; simpl.
 527         unfold take_lev; simpl.
 528         unfold drop_depth; simpl.
 529         apply ga_lit.
 530         rewrite literal_types_unchanged.
 531         apply nd_rule.
 532         apply RLit.
 533
 534     destruct case_RVar.
 535       simpl.
 536       destruct lev as [|ec lev]; simpl; [ apply nd_rule; apply RVar | idtac ].
 537       destruct (Peano_dec.eq_nat_dec (Datatypes.length lev) n); [ idtac | apply nd_rule; apply RVar ]; simpl.
 538       rewrite <- e.
 539       clear e n.
 540       repeat drop_simplify.
 541       repeat take_simplify.
 542       apply ga_id.
 543
 544     destruct case_RGlobal.
 545       simpl.
 546       destruct l as [|ec lev]; simpl; [ apply nd_rule; apply RGlobal; auto | idtac ].
 547       destruct (Peano_dec.eq_nat_dec (Datatypes.length lev) n); [ idtac | apply nd_rule; apply RGlobal; auto ]; simpl.
 548       apply (Prelude_error "found RGlobal at depth >0").
 549
 550     destruct case_RLam.
 551       simpl.
 552       destruct lev as [|ec lev]; simpl; [ apply nd_rule; apply RLam; auto | idtac ].
 553       destruct (Peano_dec.eq_nat_dec (Datatypes.length lev) n); [ idtac | apply nd_rule; apply RLam; auto ]; simpl.
 554       rewrite <- e.
 555       clear e n.
 556       repeat drop_simplify.
 557       repeat take_simplify.
 558       eapply nd_comp.
 559         eapply nd_rule.
 560         eapply RArrange.
 561         apply RCanR.
 562       apply boost.
 563       apply ga_curry.
 564
 565     destruct case_RCast.
 566       simpl.
 567       destruct lev as [|ec lev]; simpl; [ apply nd_rule; apply RCast; auto | idtac ].
 568       apply flatten_coercion; auto.
 569       destruct (Peano_dec.eq_nat_dec (Datatypes.length lev) n); [ idtac | apply nd_rule; apply RCast; auto ]; simpl.
 570       apply (Prelude_error "RCast at level >0").
 571       apply flatten_coercion; auto.
 572
 573     destruct case_RJoin.
 574       simpl.
 575       destruct (getjlev x); destruct (getjlev q).
 576       apply nd_rule.
 577       apply RJoin.
 578       apply (Prelude_error "RJoin at depth >0").
 579       apply (Prelude_error "RJoin at depth >0").
 580       apply (Prelude_error "RJoin at depth >0").
 581
 582     destruct case_RApp.
 583       simpl.
 584
 585       destruct lev as [|ec lev]. simpl. apply nd_rule.
 586         replace (flatten_type n (tx ---> te)) with ((flatten_type n tx) ---> (flatten_type n te)).
 587         apply RApp.
 588         unfold flatten_type.
 589         simpl.
 590         reflexivity.
 591
 592         destruct (Peano_dec.eq_nat_dec (Datatypes.length lev) n).
 593           eapply nd_comp.
 594           eapply nd_rule.
 595           apply RJoin.
 596           repeat drop_simplify.
 597           repeat take_simplify.
 598           apply boost.
 599           apply ga_apply.
 600
 601           replace (flatten_type (minus' n (length (ec::lev))) (tx ---> te))
 602             with ((flatten_type (minus' n (length (ec::lev))) tx) ---> (flatten_type (minus' n (length (ec::lev))) te)).
 603           apply nd_rule.
 604           apply RApp.
 605           unfold flatten_type.
 606           simpl.
 607           reflexivity.
 608
 609     destruct case_RLet.
 610       simpl.
 611       destruct lev as [|ec lev]; simpl; [ apply nd_rule; apply RLet; auto | idtac ].
 612       destruct (Peano_dec.eq_nat_dec (Datatypes.length lev) n); [ idtac | apply nd_rule; apply RLet; auto ]; simpl.
 613       repeat drop_simplify.
 614       repeat take_simplify.
 615       admit.  (* FIXME *)
 616
 617     destruct case_RVoid.
 618       simpl.
 619       apply nd_rule.
 620       apply RVoid.
 621
 622     destruct case_RAppT.
 623       simpl. destruct lev; simpl.
 624       admit.
 625       admit.
 626
 627     destruct case_RAbsT.
 628       simpl. destruct lev; simpl.
 629       admit.
 630       admit.
 631
 632     destruct case_RAppCo.
 633       simpl. destruct lev; simpl.
 634       admit.
 635       admit.
 636
 637     destruct case_RAbsCo.
 638       simpl. destruct lev; simpl.
 639       admit.
 640       admit.
 641
 642     destruct case_RLetRec.
 643       simpl.
 644       admit.
 645
 646     destruct case_RCase.
 647       simpl.
 648       admit.
 649       Defined.
 650
 651     Lemma flatten_qjudg_qjudg : forall {n}{j} (q:QJudg (S n) j), QJudg n (flatten_qjudg n j).
 652       admit.
 653       (*
 654       intros.
 655       destruct q.
 656       destruct a.
 657       unfold flatten_qjudg.
 658       destruct j.
 659       destruct (eqd_dec (Datatypes.length x) (S n)).
 660       destruct x.
 661       inversion e.
 662       exists x; split.
 663         simpl in e.
 664         inversion e.
 665         auto.
 666         simpl in *.
 667         apply allt_some.
 668         simpl.
 669         auto.
 670       unfold QJudg.
 671       exists x.
 672       split; auto.
 673         clear a.
 674         Set Printing Implicit.
 675         simpl.
 676         set (length x) as x'.
 677         assert (x'=length x).
 678           reflexivity.
 679           simpl in *.
 680           rewrite <- H.
 681           Unset Printing Implicit.
 682           idtac.
 683           omega.
 684     simpl in *.
 685       induction t0.
 686       destruct a0; simpl in *.
 687       apply allt_some.
 688       inversion a.
 689       subst.
 690       destruct l0.
 691       simpl.
 692       auto.
 693       apply allt_none.
 694       simpl in *.
 695       inversion a; subst.
 696       apply allt_branch.
 697         apply IHt0_1; auto.
 698         apply IHt0_2; auto.
 699         *)
 700         Defined.
 701
 702
 703   (*
 704   Instance FlatteningFunctor {Γ}{Δ}{ec} : Functor (JudgmentsL (PCF Γ Δ ec)) (TypesL (SystemFCa Γ Δ)) (obact) :=
 705     { fmor := FlatteningFunctor_fmor }.
 706     Admitted.
 707
 708   Definition ReificationFunctor Γ Δ : Functor (JudgmentsL _ _ (PCF n Γ Δ)) SystemFCa' (mapOptionTree brakifyJudg).
 709     refine {| fmor := ReificationFunctor_fmor Γ Δ |}; unfold hom; unfold ob; simpl ; intros.
 710     Admitted.
 711
 712   Definition PCF_SMME (n:nat)(Γ:TypeEnv)(Δ:CoercionEnv Γ) : ProgrammingLanguageSMME.
 713     refine {| plsmme_pl := PCF n Γ Δ |}.
 714     admit.
 715     Defined.
 716
 717   Definition SystemFCa_SMME (n:nat)(Γ:TypeEnv)(Δ:CoercionEnv Γ) : ProgrammingLanguageSMME.
 718     refine {| plsmme_pl := SystemFCa n Γ Δ |}.
 719     admit.
 720     Defined.
 721
 722   Definition ReificationFunctorMonoidal n : MonoidalFunctor (JudgmentsN n) (JudgmentsN (S n)) (ReificationFunctor n).
 723     admit.
 724     Defined.
 725
 726   (* 5.1.4 *)
 727   Definition PCF_SystemFCa_two_level n Γ Δ : TwoLevelLanguage (PCF_SMME n Γ Δ) (SystemFCa_SMME (S n) Γ Δ).
 728     admit.
 729     Defined.
 730   *)
 731   (*  ... and the retraction exists *)
 732
 733 End HaskFlattener.
 734
 735
 736
 737
 738
 739
 740
 741
 742
 743 (*
 744
 745   Old flattening code; ignore this - just to remind me how I used to do it
 746
 747   (*
 748    * Here it is, what you've all been waiting for!  When reading this,
 749    * it might help to have the definition for "Inductive ND" (see
 750    * NaturalDeduction.v) handy as a cross-reference.
 751    *)
 752   Hint Constructors Rule_Flat.
 753   Definition FlatteningFunctor_fmor
 754     : forall h c,
 755       (ND (PCFRule Γ Δ ec) h c) ->
 756       ((obact h)====>(obact c)).
 757
 758     set (@nil (HaskTyVar Γ ★)) as lev.
 759
 760     unfold hom; unfold ob; unfold ehom; simpl; unfold pmon_I; unfold obact; intros.
 761
 762     induction X; simpl.
 763
 764     (* the proof from no hypotheses of no conclusions (nd_id0) becomes RVoid *)
 765     apply nd_rule; apply (org_fc Γ Δ [] [(_,_)] (RVoid _ _)). apply Flat_RVoid.
 766
 767     (* the proof from hypothesis X of conclusion X (nd_id1) becomes RVar *)
 768     apply nd_rule; apply (org_fc _ _ [] [(_,_)] (RVar _ _ _ _)). apply Flat_RVar.
 769
 770     (* the proof from hypothesis X of no conclusions (nd_weak) becomes RWeak;;RVoid *)
 771     eapply nd_comp;
 772       [ idtac
 773       | eapply nd_rule
 774       ; eapply (org_fc  _ _ [(_,_)] [(_,_)] (RArrange _ _ _ _ _ (RWeak _)))
 775       ; auto ].
 776       eapply nd_rule.
 777       eapply (org_fc _ _ [] [(_,_)] (RVoid _ _)); auto. apply Flat_RVoid.
 778       apply Flat_RArrange.
 779
 780     (* the proof from hypothesis X of two identical conclusions X,,X (nd_copy) becomes RVar;;RJoin;;RCont *)
 781     eapply nd_comp; [ idtac | eapply nd_rule; eapply (org_fc _ _ [(_,_)] [(_,_)] (RArrange _ _ _ _ _ (RCont _))) ].
 782       eapply nd_comp; [ apply nd_llecnac | idtac ].
 783       set (snd_initial(SequentND:=pl_snd(ProgrammingLanguage:=SystemFCa Γ Δ))
 784         (mapOptionTree (guestJudgmentAsGArrowType) h @@@ lev)) as q.
 785       eapply nd_comp.
 786       eapply nd_prod.
 787       apply q.
 788       apply q.
 789       apply nd_rule.
 790       eapply (org_fc _ _ ([(_,_)],,[(_,_)]) [(_,_)] (RJoin _ _ _ _ _ _ )).
 791       destruct h; simpl.
 792       destruct o.
 793       simpl.
 794       apply Flat_RJoin.
 795       apply Flat_RJoin.
 796       apply Flat_RJoin.
 797       apply Flat_RArrange.
 798
 799     (* nd_prod becomes nd_llecnac;;nd_prod;;RJoin *)
 800     eapply nd_comp.
 801       apply (nd_llecnac ;; nd_prod IHX1 IHX2).
 802       apply nd_rule.
 803       eapply (org_fc _ _ ([(_,_)],,[(_,_)]) [(_,_)] (RJoin _ _ _ _ _ _ )).
 804       apply (Flat_RJoin Γ Δ (mapOptionTree guestJudgmentAsGArrowType h1 @@@ nil)
 805        (mapOptionTree guestJudgmentAsGArrowType h2 @@@ nil)
 806        (mapOptionTree guestJudgmentAsGArrowType c1 @@@ nil)
 807        (mapOptionTree guestJudgmentAsGArrowType c2 @@@ nil)).
 808
 809     (* nd_comp becomes pl_subst (aka nd_cut) *)
 810     eapply nd_comp.
 811       apply (nd_llecnac ;; nd_prod IHX1 IHX2).
 812       clear IHX1 IHX2 X1 X2.
 813       apply (@snd_cut _ _ _ _ (pl_snd(ProgrammingLanguage:=SystemFCa Γ Δ))).
 814
 815     (* nd_cancell becomes RVar;;RuCanL *)
 816     eapply nd_comp;
 817       [ idtac | eapply nd_rule; apply (org_fc _ _ [(_,_)] [(_,_)] (RArrange _ _ _ _ _ (RuCanL _))) ].
 818       apply (snd_initial(SequentND:=pl_cnd(ProgrammingLanguage:=(SystemFCa Γ Δ)))).
 819       apply Flat_RArrange.
 820
 821     (* nd_cancelr becomes RVar;;RuCanR *)
 822     eapply nd_comp;
 823       [ idtac | eapply nd_rule; apply (org_fc _ _ [(_,_)] [(_,_)] (RArrange _ _ _ _ _ (RuCanR _))) ].
 824       apply (snd_initial(SequentND:=pl_cnd(ProgrammingLanguage:=(SystemFCa Γ Δ)))).
 825       apply Flat_RArrange.
 826
 827     (* nd_llecnac becomes RVar;;RCanL *)
 828     eapply nd_comp;
 829       [ idtac | eapply nd_rule; apply (org_fc _ _ [(_,_)] [(_,_)] (RArrange _ _ _ _ _ (RCanL _))) ].
 830       apply (snd_initial(SequentND:=pl_cnd(ProgrammingLanguage:=(SystemFCa Γ Δ)))).
 831       apply Flat_RArrange.
 832
 833     (* nd_rlecnac becomes RVar;;RCanR *)
 834     eapply nd_comp;
 835       [ idtac | eapply nd_rule; apply (org_fc _ _ [(_,_)] [(_,_)] (RArrange _ _ _ _ _ (RCanR _))) ].
 836       apply (snd_initial(SequentND:=pl_cnd(ProgrammingLanguage:=(SystemFCa Γ Δ)))).
 837       apply Flat_RArrange.
 838
 839     (* nd_assoc becomes RVar;;RAssoc *)
 840     eapply nd_comp;
 841       [ idtac | eapply nd_rule; apply (org_fc _ _ [(_,_)] [(_,_)] (RArrange _ _ _ _ _ (RAssoc _ _ _))) ].
 842       apply (snd_initial(SequentND:=pl_cnd(ProgrammingLanguage:=(SystemFCa Γ Δ)))).
 843       apply Flat_RArrange.
 844
 845     (* nd_cossa becomes RVar;;RCossa *)
 846     eapply nd_comp;
 847       [ idtac | eapply nd_rule; apply (org_fc _ _ [(_,_)] [(_,_)] (RArrange _ _ _ _ _ (RCossa _ _ _))) ].
 848       apply (snd_initial(SequentND:=pl_cnd(ProgrammingLanguage:=(SystemFCa Γ Δ)))).
 849       apply Flat_RArrange.
 850
 851       destruct r as [r rp].
 852       rename h into h'.
 853       rename c into c'.
 854       rename r into r'.
 855
 856       refine (match rp as R in @Rule_PCF _ _ _ H C _
 857                 return
 858                 ND (OrgR Γ Δ) []
 859                 [sequent (mapOptionTree guestJudgmentAsGArrowType H @@@ nil)
 860                   (mapOptionTree guestJudgmentAsGArrowType C @@@ nil)]
 861                 with
 862                 | PCF_RArrange         h c r q          => let case_RURule        := tt in _
 863                 | PCF_RLit             lit              => let case_RLit          := tt in _
 864                 | PCF_RNote            Σ τ   n          => let case_RNote         := tt in _
 865                 | PCF_RVar             σ                => let case_RVar          := tt in _
 866                 | PCF_RLam             Σ tx te          => let case_RLam          := tt in _
 867                 | PCF_RApp             Σ tx te   p      => let case_RApp          := tt in _
 868                 | PCF_RLet             Σ σ₁ σ₂   p      => let case_RLet          := tt in _
 869                 | PCF_RJoin    b c d e          => let case_RJoin := tt in _
 870                 | PCF_RVoid                       => let case_RVoid   := tt in _
 871               (*| PCF_RCase            T κlen κ θ l x   => let case_RCase         := tt in _*)
 872               (*| PCF_RLetRec          Σ₁ τ₁ τ₂ lev     => let case_RLetRec       := tt in _*)
 873               end); simpl in *.
 874       clear rp h' c' r'.
 875
 876       rewrite (unlev_lemma h (ec::nil)).
 877       rewrite (unlev_lemma c (ec::nil)).
 878       destruct case_RURule.
 879         refine (match q as Q in Arrange H C
 880                 return
 881                 H=(h @@@ (ec :: nil)) ->
 882                 C=(c @@@ (ec :: nil)) ->
 883                 ND (OrgR Γ Δ) []
 884                 [sequent
 885                   [ga_type (ga_rep (mapOptionTree unlev H)) (ga_rep r) @@ nil ]
 886                   [ga_type (ga_rep (mapOptionTree unlev C)) (ga_rep r) @@ nil ] ]
 887                   with
 888           | RLeft   a b c r => let case_RLeft  := tt in _
 889           | RRight  a b c r => let case_RRight := tt in _
 890           | RCanL     b     => let case_RCanL  := tt in _
 891           | RCanR     b     => let case_RCanR  := tt in _
 892           | RuCanL    b     => let case_RuCanL := tt in _
 893           | RuCanR    b     => let case_RuCanR := tt in _
 894           | RAssoc    b c d => let case_RAssoc := tt in _
 895           | RCossa    b c d => let case_RCossa := tt in _
 896           | RExch     b c   => let case_RExch  := tt in _
 897           | RWeak     b     => let case_RWeak  := tt in _
 898           | RCont     b     => let case_RCont  := tt in _
 899           | RComp a b c f g => let case_RComp  := tt in _
 900         end (refl_equal _) (refl_equal _));
 901         intros; simpl in *;
 902         subst;
 903         try rewrite <- unlev_lemma in *.
 904
 905       destruct case_RCanL.
 906         apply magic.
 907         apply ga_uncancell.
 908
 909       destruct case_RCanR.
 910         apply magic.
 911         apply ga_uncancelr.
 912
 913       destruct case_RuCanL.
 914         apply magic.
 915         apply ga_cancell.
 916
 917       destruct case_RuCanR.
 918         apply magic.
 919         apply ga_cancelr.
 920
 921       destruct case_RAssoc.
 922         apply magic.
 923         apply ga_assoc.
 924
 925       destruct case_RCossa.
 926         apply magic.
 927         apply ga_unassoc.
 928
 929       destruct case_RExch.
 930         apply magic.
 931         apply ga_swap.
 932
 933       destruct case_RWeak.
 934         apply magic.
 935         apply ga_drop.
 936
 937       destruct case_RCont.
 938         apply magic.
 939         apply ga_copy.
 940
 941       destruct case_RLeft.
 942         apply magic.
 943         (*apply ga_second.*)
 944         admit.
 945
 946       destruct case_RRight.
 947         apply magic.
 948         (*apply ga_first.*)
 949         admit.
 950
 951       destruct case_RComp.
 952         apply magic.
 953         (*apply ga_comp.*)
 954         admit.
 955
 956       destruct case_RLit.
 957         apply ga_lit.
 958
 959       (* hey cool, I figured out how to pass CoreNote's through... *)
 960       destruct case_RNote.
 961         eapply nd_comp.
 962         eapply nd_rule.
 963         eapply (org_fc _ _ [] [(_,_)] (RVar _ _ _ _)) . auto.
 964         apply Flat_RVar.
 965         apply nd_rule.
 966         apply (org_fc _ _ [(_,_)] [(_,_)] (RNote _ _ _ _ _ n)). auto.
 967         apply Flat_RNote.
 968
 969       destruct case_RVar.
 970         apply ga_id.
 971
 972       (*
 973        *   class GArrow g (**) u => GArrowApply g (**) u (~>) where
 974        *     ga_applyl    :: g (x**(x~>y)   ) y
 975        *     ga_applyr    :: g (   (x~>y)**x) y
 976        *
 977        *   class GArrow g (**) u => GArrowCurry g (**) u (~>) where
 978        *     ga_curryl    :: g (x**y) z  ->  g x (y~>z)
 979        *     ga_curryr    :: g (x**y) z  ->  g y (x~>z)
 980        *)
 981       destruct case_RLam.
 982         (* GArrowCurry.ga_curry *)
 983         admit.
 984
 985       destruct case_RApp.
 986         (* GArrowApply.ga_apply *)
 987         admit.
 988
 989       destruct case_RLet.
 990         admit.
 991
 992       destruct case_RVoid.
 993         apply ga_id.
 994
 995       destruct case_RJoin.
 996         (* this assumes we want effects to occur in syntactically-left-to-right order *)
 997         admit.
 998         Defined.
 999 *)