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 Definition minus' n m :=
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' ]
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
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
94 Lemma drop_depth_lemma : forall Γ (lev:HaskLevel Γ) x, drop_depth lev [x @@ lev] = [].
104 Lemma drop_depth_lemma_s : forall Γ (lev:HaskLevel Γ) ec x, drop_depth (ec::lev) [x @@ (ec :: lev)] = [].
114 Lemma take_lemma : forall Γ (lev:HaskLevel Γ) x, take_lev lev [x @@ lev] = [x].
124 Ltac drop_simplify :=
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 ★)))
136 Ltac take_simplify :=
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 ★)))
146 Fixpoint reduceTree {T}(unit:T)(merge:T -> T -> T)(tt:Tree ??T) : T :=
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)
153 Set Printing Width 130.
155 Context {unitTy : forall TV, RawHaskType TV ★ }.
156 Context {prodTy : forall TV, RawHaskType TV (★ ⇛ ★ ⇛ ★) }.
157 Context {gaTy : forall TV, RawHaskType TV (★ ⇛ ★ ⇛ ★ ⇛ ★)}.
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 Γ ★ :=
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'.
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] ]
190 Context `(gar:garrow).
192 Notation "a ~~~~> b" := (@ga _ _ a b) (at level 20).
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
200 Fixpoint garrowfy_raw_codetypes {TV}{κ}(depth:nat)(exp: RawHaskType TV κ) : RawHaskType TV κ :=
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)
206 | TCoerc _ t1 t2 t => TCoerc (garrowfy_raw_codetypes depth t1) (garrowfy_raw_codetypes depth t2)
207 (garrowfy_raw_codetypes depth t)
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)
213 | TyFunApp tfc lt => TyFunApp tfc (garrowfy_raw_codetypes_list _ depth lt)
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)
220 Definition garrowfy_code_types {Γ}{κ}(n:nat)(ht:HaskType Γ κ) : HaskType Γ κ :=
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.
226 Axiom literal_types_unchanged : forall n Γ l, garrowfy_code_types n (literalType l) = literalType(Γ:=Γ) l.
228 Axiom flatten_coercion : forall n Γ Δ κ (σ τ:HaskType Γ κ) (γ:HaskCoercion Γ Δ (σ ∼∼∼ τ)),
229 HaskCoercion Γ Δ (garrowfy_code_types n σ ∼∼∼ garrowfy_code_types n τ).
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
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 Γ :=
240 | T_Leaf (Some (_ @@ lev)) => lev
242 match getjlev b1 with
248 Definition v2t {Γ}(ec:HaskTyVar Γ ★) := fun TV ite => TVar (ec TV ite).
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
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'])
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
272 Definition boost : forall Γ Δ ant x y,
273 ND Rule [] [ Γ > Δ > x |- y ] ->
274 ND Rule [ Γ > Δ > ant |- x ] [ Γ > Δ > ant |- y ].
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] ].
284 Definition seq : ∀ Γ Δ lev a b,
285 ND Rule [] [ Γ > Δ > [] |- [a @@ lev] ] ->
286 ND Rule [] [ Γ > Δ > [] |- [b @@ lev] ] ->
287 ND Rule [] [ Γ > Δ > [] |- [a @@ lev],,[b @@ lev] ].
291 Lemma ga_unkappa : ∀ Γ Δ ec l a b Σ,
293 [Γ > Δ > Σ |- [@ga Γ ec a b @@ l] ]
294 [Γ > Δ > Σ,,[@ga Γ ec [] a @@ l] |- [@ga Γ ec [] b @@ l] ].
296 set (ga_comp Γ Δ ec l [] a b) as q.
298 set (@RLet Γ Δ) as q'.
299 set (@RLet Γ Δ [@ga _ ec [] a @@ l] Σ (@ga _ ec [] b) (@ga _ ec a b) l) as q''.
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).
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] ].
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]]
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.
351 refine ( _ ;; boost _ _ _ _ _ (ga_comp _ _ _ _ _ _ _)).
357 Definition garrowfy_arrangement :
358 forall Γ (Δ:CoercionEnv Γ) n
359 (ec:HaskTyVar Γ ★) (lev:HaskLevel Γ) (ant1 ant2:Tree ??(LeveledHaskType Γ ★)) (r:Arrange ant1 ant2) succ,
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]].
366 refine ( _ ;; (boost _ _ _ _ _ (postcompose _ _ _ _ _ _ _ (garrowfy_arrangement' Γ Δ ec lev ant1 ant2 r)))).
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.
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]).
394 set (getjlev succ) as succ_lev.
395 assert (succ_lev=getjlev succ).
413 eapply RComp; [ apply IHr1 | apply IHr2 ].
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).
420 apply garrowfy_arrangement.
437 eapply RComp; [ apply IHr1 | apply IHr2 ].
440 Definition arrange_brak : forall Γ Δ ec succ t,
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]].
450 Definition arrange_esc : forall Γ Δ ec succ t,
452 [Γ > Δ > mapOptionTree (garrowfy_leveled_code_types 0) succ |- [(@ga _ (v2t ec) [] [t]) @@ nil]]
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]].
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).
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 τ).
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)).
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 κ).
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).
490 Definition flatten_proof :
493 ND Rule (mapOptionTree (flatten_judgment n) h) (mapOptionTree (flatten_judgment n) c).
495 eapply nd_map'; [ idtac | apply X ].
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 _
522 destruct case_RArrange.
523 apply (flatten_arrangement n Γ Δ a b x d).
527 destruct (Peano_dec.eq_nat_dec (Datatypes.length lev) 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)) ;; _).
538 apply (Prelude_error "found Brak at depth >0").
539 apply (Prelude_error "found Brak at depth >0").
543 destruct (Peano_dec.eq_nat_dec (Datatypes.length lev) 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))).
553 apply (Prelude_error "found Esc at depth >0").
554 apply (Prelude_error "found Esc at depth >0").
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.
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.
573 rewrite literal_types_unchanged.
578 Opaque flatten_judgment.
580 Transparent flatten_judgment.
582 unfold flatten_judgment.
585 apply nd_rule. apply RVar.
586 destruct (eqd_dec (Datatypes.length lev) n).
588 repeat drop_simplify.
589 repeat take_simplify.
596 destruct case_RGlobal.
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").
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.
610 repeat drop_simplify.
611 repeat take_simplify.
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.
630 destruct (getjlev x); destruct (getjlev q).
633 apply (Prelude_error "RJoin at depth >0").
634 apply (Prelude_error "RJoin at depth >0").
635 apply (Prelude_error "RJoin at depth >0").
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)).
643 unfold garrowfy_code_types.
647 destruct (Peano_dec.eq_nat_dec (Datatypes.length lev) n).
651 repeat drop_simplify.
652 repeat take_simplify.
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)).
661 unfold garrowfy_code_types.
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).
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.
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'.
733 simpl. destruct lev; simpl.
734 rewrite garrowfy_commutes_with_HaskTAll.
735 rewrite garrowfy_commutes_with_substT.
740 apply (Prelude_error "AppT at depth>0").
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 ].
748 set (mapOptionTree (garrowfy_leveled_code_types n) (mapOptionTree (weakLT(κ:=κ)) Σ)) as a.
749 set (mapOptionTree (weakLT(κ:=κ)) (mapOptionTree (garrowfy_leveled_code_types n) Σ)) as q'.
757 rewrite garrowfy_commutes_with_weakLT.
768 apply (Prelude_error "AbsT at depth>0").
770 destruct case_RAppCo.
771 simpl. destruct lev; simpl.
772 unfold garrowfy_code_types.
776 apply flatten_coercion.
778 apply (Prelude_error "AppCo at depth>0").
780 destruct case_RAbsCo.
781 simpl. destruct lev; simpl.
782 unfold garrowfy_code_types.
784 apply (Prelude_error "AbsCo not supported (FIXME)").
785 apply (Prelude_error "AbsCo at depth>0").
787 destruct case_RLetRec.
789 apply (Prelude_error "LetRec not supported (FIXME)").
793 apply (Prelude_error "Case not supported (FIXME)").
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 *)
801 Instance FlatteningFunctor {Γ}{Δ}{ec} : Functor (JudgmentsL (PCF Γ Δ ec)) (TypesL (SystemFCa Γ Δ)) (obact) :=
802 { fmor := FlatteningFunctor_fmor }.
804 Definition ReificationFunctor Γ Δ : Functor (JudgmentsL _ _ (PCF n Γ Δ)) SystemFCa' (mapOptionTree brakifyJudg).
805 refine {| fmor := ReificationFunctor_fmor Γ Δ |}; unfold hom; unfold ob; simpl ; intros.
807 Definition PCF_SMME (n:nat)(Γ:TypeEnv)(Δ:CoercionEnv Γ) : ProgrammingLanguageSMME.
808 refine {| plsmme_pl := PCF n Γ Δ |}.
811 Definition SystemFCa_SMME (n:nat)(Γ:TypeEnv)(Δ:CoercionEnv Γ) : ProgrammingLanguageSMME.
812 refine {| plsmme_pl := SystemFCa n Γ Δ |}.
815 Definition ReificationFunctorMonoidal n : MonoidalFunctor (JudgmentsN n) (JudgmentsN (S n)) (ReificationFunctor n).
819 Definition PCF_SystemFCa_two_level n Γ Δ : TwoLevelLanguage (PCF_SMME n Γ Δ) (SystemFCa_SMME (S n) Γ Δ).
822 (* ... and the retraction exists *)
826 Implicit Arguments garrow [ ].