1 (*********************************************************************************************************************************)
4 (* The Flattening Functor. *)
6 (*********************************************************************************************************************************)
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.
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.
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.
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.
50 * The flattening transformation. Currently only TWO-level languages are
51 * supported, and the level-1 sublanguage is rather limited.
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)
57 Section HaskFlattener.
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*)
62 (* lemma: if a proof from no hypotheses contains no Brak's or Esc's, then the context contains no variables at level!=0 *)
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
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
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
84 (* delete from the tree any type which is NOT at level "lev" *)
86 Fixpoint take_lev' {Γ}(lev:HaskLevel Γ)(tt:Tree ??(LeveledHaskType Γ ★)) : ??(Tree ??(HaskType Γ ★)) :=
88 | T_Leaf None => Some (T_Leaf None) (* FIXME: unsure of this; it ends up on both sides *)
90 let b1' := take_lev' lev b1 in
91 let b2' := take_lev' lev b2 in
94 | Some b1'' => match b2' with
96 | Some b2'' => Some (b1'',,b2'')
99 | T_Leaf (Some (ttype@@tlev)) =>
105 Context (ga' : forall TV, TV ★ -> Tree ??(RawHaskType TV ★) -> Tree ??(RawHaskType TV ★) -> RawHaskType TV ★).
107 Definition ga : forall Γ, HaskTyVar Γ ★ -> Tree ??(HaskType Γ ★) -> Tree ??(HaskType Γ ★) -> HaskType Γ ★
108 := fun Γ ec ant suc =>
113 (mapOptionTree (fun x => x TV ite) ant)
114 (mapOptionTree (fun x => x TV ite) suc).
116 Implicit Arguments ga [ [Γ] ].
117 Notation "a ~~~~> b" := (@ga _ _ a b) (at level 20).
119 Context (unit_type : forall TV, RawHaskType TV ★).
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
127 Fixpoint flatten_rawtype {TV}{κ}(depth:nat)(exp: RawHaskType TV κ) : RawHaskType TV κ :=
130 | TAll _ y => TAll _ (fun v => flatten_rawtype depth (y v))
131 | TApp _ _ x y => TApp (flatten_rawtype depth x) (flatten_rawtype depth y)
133 | TCoerc _ t1 t2 t => TCoerc (flatten_rawtype depth t1) (flatten_rawtype depth t2) (flatten_rawtype depth t)
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]
140 | (S depth') => TCode v (flatten_rawtype depth' e)
142 | TyFunApp tfc lt => TyFunApp tfc (flatten_rawtype_list _ depth lt)
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)
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)
155 Implicit Arguments AllT [[T]].
157 Definition getΓ (j:Judg) := match j with Γ > _ > _ |- _ => Γ end.
159 Definition getSuc (j:Judg) : Tree ??(LeveledHaskType (getΓ j) ★) :=
160 match j as J return Tree ??(LeveledHaskType (getΓ J) ★) with
164 Definition getlev {Γ}{κ}(lht:LeveledHaskType Γ κ) :=
165 match lht with t@@l => l end.
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
170 Fixpoint getjlev {Γ}(tt:Tree ??(LeveledHaskType Γ ★)) : HaskLevel Γ :=
173 | T_Leaf (Some (_ @@ lev)) => lev
175 match getjlev b1 with
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.
185 (* Definition qjudg2judg {n}(qj:QJudg n) : Judg := projT1 qj.*)
187 Inductive QRule : nat -> Tree ??Judg -> Tree ??Judg -> Type :=
188 mkQRule : forall n h c,
190 ITree _ (QJudg n) h ->
191 ITree _ (QJudg n) c ->
194 Definition QND n := ND (QRule n).
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)
201 Definition flatten_type {Γ}(n:nat)(ht:HaskType Γ ★) : HaskType Γ ★ :=
203 flatten_rawtype n (ht TV ite).
205 Definition minus' n m :=
211 (* to do: integrate this more cleanly with qjudg *)
212 Definition flatten_leveled_type {Γ}(n:nat)(ht:LeveledHaskType Γ ★) : LeveledHaskType Γ ★ :=
215 flatten_type (minus' n (length htlev)) htt @@ htlev
218 Definition flatten_qjudg_ok (n:nat)(j:Judg) : Judg :=
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')
226 Definition take_lev'' {Γ}(lev:HaskLevel Γ)(tt:Tree ??(LeveledHaskType Γ ★)) : Tree ??(HaskType Γ ★) :=
227 match (take_lev' lev tt) with
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
247 Axiom literal_types_unchanged : forall n Γ l, flatten_type n (literalType l) = literalType(Γ:=Γ) l.
249 Lemma drop_depth_lemma : forall Γ (lev:HaskLevel Γ) x, drop_depth (length lev) [x @@ lev] = [].
253 Lemma drop_depth_lemma_s : forall Γ (lev:HaskLevel Γ) ec x, drop_depth (S (length lev)) [x @@ (ec :: lev)] = [].
257 Ltac drop_simplify :=
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 ★)))
269 Lemma take_lemma : forall Γ (lev:HaskLevel Γ) x, take_lev lev [x @@ lev] = [x].
273 Ltac take_simplify :=
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 ★)))
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]
302 [@ga Γ ec (a,,a') [c] @@ lev] ]
305 Context (gar:garrow).
307 Definition boost : forall Γ Δ ant x y,
308 ND Rule [] [ Γ > Δ > x |- y ] ->
309 ND Rule [ Γ > Δ > ant |- x ] [ Γ > Δ > ant |- y ].
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] ].
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] ].
324 Set Printing Width 130.
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] ].
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]]
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.
353 set (ga_comp Γ Δ ec lev (``c) (``b) (``a)) as q.
357 refine ( _ ;; boost _ _ _ _ _ (ga_comp _ _ _ _ _ _ _)).
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 *)
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]].
374 refine ( _ ;; (boost _ _ _ _ _ (postcompose _ _ _ _ _ _ _ (garrowfy_arrangement' Γ Δ ec lev ant1 ant2 r)))).
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.
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]).
400 set (getjlev succ) as succ_lev.
401 assert (succ_lev=getjlev succ).
419 eapply RComp; [ apply IHr1 | apply IHr2 ].
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).
426 apply garrowfy_arrangement.
443 eapply RComp; [ apply IHr1 | apply IHr2 ].
446 Lemma flatten_coercion : forall n Γ Δ σ τ (γ:HaskCoercion Γ Δ (σ ∼∼∼ τ)),
447 HaskCoercion Γ Δ (flatten_type n σ ∼∼∼ flatten_type n τ).
451 Ltac eqd_dec_refl' :=
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' ]
460 Lemma foog : forall Γ Δ,
462 ( [ Γ > Δ > Σ₁ |- a ],,[ Γ > Δ > Σ₂ |- b ] )
463 [ Γ > Δ > Σ₁,,Σ₂ |- a,,b ]
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).
473 ND Rule (mapOptionTree (flatten_qjudg n) h) (mapOptionTree (flatten_qjudg n) c).
475 eapply nd_map'; [ idtac | apply X ].
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.
504 destruct case_RArrange.
505 apply (flatten_arrangement n Γ Δ a b x d).
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.
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.
530 rewrite literal_types_unchanged.
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.
540 repeat drop_simplify.
541 repeat take_simplify.
544 destruct case_RGlobal.
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").
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.
556 repeat drop_simplify.
557 repeat take_simplify.
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.
575 destruct (getjlev x); destruct (getjlev q).
578 apply (Prelude_error "RJoin at depth >0").
579 apply (Prelude_error "RJoin at depth >0").
580 apply (Prelude_error "RJoin at depth >0").
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)).
592 destruct (Peano_dec.eq_nat_dec (Datatypes.length lev) n).
596 repeat drop_simplify.
597 repeat take_simplify.
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)).
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.
623 simpl. destruct lev; simpl.
628 simpl. destruct lev; simpl.
632 destruct case_RAppCo.
633 simpl. destruct lev; simpl.
637 destruct case_RAbsCo.
638 simpl. destruct lev; simpl.
642 destruct case_RLetRec.
651 Lemma flatten_qjudg_qjudg : forall {n}{j} (q:QJudg (S n) j), QJudg n (flatten_qjudg n j).
657 unfold flatten_qjudg.
659 destruct (eqd_dec (Datatypes.length x) (S n)).
674 Set Printing Implicit.
676 set (length x) as x'.
677 assert (x'=length x).
681 Unset Printing Implicit.
686 destruct a0; simpl in *.
704 Instance FlatteningFunctor {Γ}{Δ}{ec} : Functor (JudgmentsL (PCF Γ Δ ec)) (TypesL (SystemFCa Γ Δ)) (obact) :=
705 { fmor := FlatteningFunctor_fmor }.
708 Definition ReificationFunctor Γ Δ : Functor (JudgmentsL _ _ (PCF n Γ Δ)) SystemFCa' (mapOptionTree brakifyJudg).
709 refine {| fmor := ReificationFunctor_fmor Γ Δ |}; unfold hom; unfold ob; simpl ; intros.
712 Definition PCF_SMME (n:nat)(Γ:TypeEnv)(Δ:CoercionEnv Γ) : ProgrammingLanguageSMME.
713 refine {| plsmme_pl := PCF n Γ Δ |}.
717 Definition SystemFCa_SMME (n:nat)(Γ:TypeEnv)(Δ:CoercionEnv Γ) : ProgrammingLanguageSMME.
718 refine {| plsmme_pl := SystemFCa n Γ Δ |}.
722 Definition ReificationFunctorMonoidal n : MonoidalFunctor (JudgmentsN n) (JudgmentsN (S n)) (ReificationFunctor n).
727 Definition PCF_SystemFCa_two_level n Γ Δ : TwoLevelLanguage (PCF_SMME n Γ Δ) (SystemFCa_SMME (S n) Γ Δ).
731 (* ... and the retraction exists *)
745 Old flattening code; ignore this - just to remind me how I used to do it
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.
752 Hint Constructors Rule_Flat.
753 Definition FlatteningFunctor_fmor
755 (ND (PCFRule Γ Δ ec) h c) ->
756 ((obact h)====>(obact c)).
758 set (@nil (HaskTyVar Γ ★)) as lev.
760 unfold hom; unfold ob; unfold ehom; simpl; unfold pmon_I; unfold obact; intros.
764 (* the proof from no hypotheses of no conclusions (nd_id0) becomes RVoid *)
765 apply nd_rule; apply (org_fc Γ Δ [] [(_,_)] (RVoid _ _)). apply Flat_RVoid.
767 (* the proof from hypothesis X of conclusion X (nd_id1) becomes RVar *)
768 apply nd_rule; apply (org_fc _ _ [] [(_,_)] (RVar _ _ _ _)). apply Flat_RVar.
770 (* the proof from hypothesis X of no conclusions (nd_weak) becomes RWeak;;RVoid *)
774 ; eapply (org_fc _ _ [(_,_)] [(_,_)] (RArrange _ _ _ _ _ (RWeak _)))
777 eapply (org_fc _ _ [] [(_,_)] (RVoid _ _)); auto. apply Flat_RVoid.
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.
790 eapply (org_fc _ _ ([(_,_)],,[(_,_)]) [(_,_)] (RJoin _ _ _ _ _ _ )).
799 (* nd_prod becomes nd_llecnac;;nd_prod;;RJoin *)
801 apply (nd_llecnac ;; nd_prod IHX1 IHX2).
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)).
809 (* nd_comp becomes pl_subst (aka nd_cut) *)
811 apply (nd_llecnac ;; nd_prod IHX1 IHX2).
812 clear IHX1 IHX2 X1 X2.
813 apply (@snd_cut _ _ _ _ (pl_snd(ProgrammingLanguage:=SystemFCa Γ Δ))).
815 (* nd_cancell becomes RVar;;RuCanL *)
817 [ idtac | eapply nd_rule; apply (org_fc _ _ [(_,_)] [(_,_)] (RArrange _ _ _ _ _ (RuCanL _))) ].
818 apply (snd_initial(SequentND:=pl_cnd(ProgrammingLanguage:=(SystemFCa Γ Δ)))).
821 (* nd_cancelr becomes RVar;;RuCanR *)
823 [ idtac | eapply nd_rule; apply (org_fc _ _ [(_,_)] [(_,_)] (RArrange _ _ _ _ _ (RuCanR _))) ].
824 apply (snd_initial(SequentND:=pl_cnd(ProgrammingLanguage:=(SystemFCa Γ Δ)))).
827 (* nd_llecnac becomes RVar;;RCanL *)
829 [ idtac | eapply nd_rule; apply (org_fc _ _ [(_,_)] [(_,_)] (RArrange _ _ _ _ _ (RCanL _))) ].
830 apply (snd_initial(SequentND:=pl_cnd(ProgrammingLanguage:=(SystemFCa Γ Δ)))).
833 (* nd_rlecnac becomes RVar;;RCanR *)
835 [ idtac | eapply nd_rule; apply (org_fc _ _ [(_,_)] [(_,_)] (RArrange _ _ _ _ _ (RCanR _))) ].
836 apply (snd_initial(SequentND:=pl_cnd(ProgrammingLanguage:=(SystemFCa Γ Δ)))).
839 (* nd_assoc becomes RVar;;RAssoc *)
841 [ idtac | eapply nd_rule; apply (org_fc _ _ [(_,_)] [(_,_)] (RArrange _ _ _ _ _ (RAssoc _ _ _))) ].
842 apply (snd_initial(SequentND:=pl_cnd(ProgrammingLanguage:=(SystemFCa Γ Δ)))).
845 (* nd_cossa becomes RVar;;RCossa *)
847 [ idtac | eapply nd_rule; apply (org_fc _ _ [(_,_)] [(_,_)] (RArrange _ _ _ _ _ (RCossa _ _ _))) ].
848 apply (snd_initial(SequentND:=pl_cnd(ProgrammingLanguage:=(SystemFCa Γ Δ)))).
851 destruct r as [r rp].
856 refine (match rp as R in @Rule_PCF _ _ _ H C _
859 [sequent (mapOptionTree guestJudgmentAsGArrowType H @@@ nil)
860 (mapOptionTree guestJudgmentAsGArrowType C @@@ nil)]
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 _*)
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
881 H=(h @@@ (ec :: nil)) ->
882 C=(c @@@ (ec :: nil)) ->
885 [ga_type (ga_rep (mapOptionTree unlev H)) (ga_rep r) @@ nil ]
886 [ga_type (ga_rep (mapOptionTree unlev C)) (ga_rep r) @@ nil ] ]
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 _));
903 try rewrite <- unlev_lemma in *.
913 destruct case_RuCanL.
917 destruct case_RuCanR.
921 destruct case_RAssoc.
925 destruct case_RCossa.
946 destruct case_RRight.
959 (* hey cool, I figured out how to pass CoreNote's through... *)
963 eapply (org_fc _ _ [] [(_,_)] (RVar _ _ _ _)) . auto.
966 apply (org_fc _ _ [(_,_)] [(_,_)] (RNote _ _ _ _ _ n)). auto.
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
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)
982 (* GArrowCurry.ga_curry *)
986 (* GArrowApply.ga_apply *)
996 (* this assumes we want effects to occur in syntactically-left-to-right order *)