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 HaskCoreVars.
18 Require Import HaskWeakTypes.
19 Require Import HaskWeakVars.
20 Require Import HaskLiterals.
21 Require Import HaskTyCons.
22 Require Import HaskStrongTypes.
23 Require Import HaskProof.
24 Require Import NaturalDeduction.
26 Require Import HaskStrongTypes.
27 Require Import HaskStrong.
28 Require Import HaskProof.
29 Require Import HaskStrongToProof.
30 Require Import HaskProofToStrong.
31 Require Import HaskWeakToStrong.
33 Require Import HaskSkolemizer.
36 Set Printing Width 130.
39 * The flattening transformation. Currently only TWO-level languages are
40 * supported, and the level-1 sublanguage is rather limited.
42 * This file abuses terminology pretty badly. For purposes of this file,
43 * "PCF" means "the level-1 sublanguage" and "FC" (aka System FC) means
44 * the whole language (level-0 language including bracketed level-1 terms)
46 Section HaskFlattener.
48 Definition getlev {Γ}{κ}(lht:LeveledHaskType Γ κ) : HaskLevel Γ :=
49 match lht with t @@ l => l end.
52 forall {T} (Σ:Tree ??T) (f:T -> bool),
53 Arrange Σ (dropT (mkFlags (liftBoolFunc false f) Σ),,( (dropT (mkFlags (liftBoolFunc false (bnot ○ f)) Σ)))).
59 destruct (f t); simpl.
65 eapply RComp; [ idtac | apply arrangeSwapMiddle ].
74 forall {T} (Σ:Tree ??T) (f:T -> bool),
75 Arrange (dropT (mkFlags (liftBoolFunc false f) Σ),,( (dropT (mkFlags (liftBoolFunc false (bnot ○ f)) Σ)))) Σ.
81 destruct (f t); simpl.
87 eapply RComp; [ apply arrangeSwapMiddle | idtac ].
97 | [ |- context[@eqd_dec ?T ?V ?X ?X] ] =>
98 destruct (@eqd_dec T V X X) as [eqd_dec1 | eqd_dec2];
99 [ clear eqd_dec1 | set (eqd_dec2 (refl_equal _)) as eqd_dec2'; inversion eqd_dec2' ]
102 Definition v2t {Γ}(ec:HaskTyVar Γ ECKind) : HaskType Γ ECKind := fun TV ite => TVar (ec TV ite).
104 Definition levelMatch {Γ}(lev:HaskLevel Γ) : LeveledHaskType Γ ★ -> bool :=
105 fun t => match t with ttype@@tlev => if eqd_dec tlev lev then true else false end.
107 (* In a tree of types, replace any type at depth "lev" or greater None *)
108 Definition mkDropFlags {Γ}(lev:HaskLevel Γ)(tt:Tree ??(LeveledHaskType Γ ★)) : TreeFlags tt :=
109 mkFlags (liftBoolFunc false (levelMatch lev)) tt.
111 Definition drop_lev {Γ}(lev:HaskLevel Γ)(tt:Tree ??(LeveledHaskType Γ ★)) : Tree ??(LeveledHaskType Γ ★) :=
112 dropT (mkDropFlags lev tt).
114 (* The opposite: replace any type which is NOT at level "lev" with None *)
115 Definition mkTakeFlags {Γ}(lev:HaskLevel Γ)(tt:Tree ??(LeveledHaskType Γ ★)) : TreeFlags tt :=
116 mkFlags (liftBoolFunc true (bnot ○ levelMatch lev)) tt.
118 Definition take_lev {Γ}(lev:HaskLevel Γ)(tt:Tree ??(LeveledHaskType Γ ★)) : Tree ??(LeveledHaskType Γ ★) :=
119 dropT (mkTakeFlags lev tt).
121 mapOptionTree (fun x => flatten_type (unlev x))
122 (maybeTree (takeT tt (mkFlags (
123 fun t => match t with
124 | Some (ttype @@ tlev) => if eqd_dec tlev lev then true else false
129 Definition maybeTree {T}(t:??(Tree ??T)) : Tree ??T :=
136 Lemma drop_lev_lemma : forall Γ (lev:HaskLevel Γ) x, drop_lev lev [x @@ lev] = [].
148 Lemma drop_lev_lemma_s : forall Γ (lev:HaskLevel Γ) ec x, drop_lev (ec::lev) [x @@ (ec :: lev)] = [].
159 Lemma take_lemma : forall Γ (lev:HaskLevel Γ) x, take_lev lev [x @@ lev] = [x @@ lev].
170 Lemma take_lemma' : forall Γ (lev:HaskLevel Γ) x, take_lev lev (x @@@ lev) = x @@@ lev.
173 destruct a; simpl; try reflexivity.
176 rewrite <- IHx1 at 2.
177 rewrite <- IHx2 at 2.
181 Lemma drop_lev_lemma' : forall Γ (lev:HaskLevel Γ) x, drop_lev lev (x @@@ lev) = [].
184 destruct a; simpl; try reflexivity.
185 apply drop_lev_lemma.
187 change (@drop_lev _ lev (x1 @@@ lev ,, x2 @@@ lev))
188 with ((@drop_lev _ lev (x1 @@@ lev)) ,, (@drop_lev _ lev (x2 @@@ lev))).
195 Ltac drop_simplify :=
197 | [ |- context[@drop_lev ?G ?L [ ?X @@ ?L ] ] ] =>
198 rewrite (drop_lev_lemma G L X)
200 | [ |- context[@drop_lev ?G ?L [ ?X @@@ ?L ] ] ] =>
201 rewrite (drop_lev_lemma' G L X)
203 | [ |- context[@drop_lev ?G (?E :: ?L) [ ?X @@ (?E :: ?L) ] ] ] =>
204 rewrite (drop_lev_lemma_s G L E X)
205 | [ |- context[@drop_lev ?G ?N (?A,,?B)] ] =>
206 change (@drop_lev G N (A,,B)) with ((@drop_lev G N A),,(@drop_lev G N B))
207 | [ |- context[@drop_lev ?G ?N (T_Leaf None)] ] =>
208 change (@drop_lev G N (T_Leaf (@None (LeveledHaskType G ★)))) with (T_Leaf (@None (LeveledHaskType G ★)))
211 Ltac take_simplify :=
213 | [ |- context[@take_lev ?G ?L [ ?X @@ ?L ] ] ] =>
214 rewrite (take_lemma G L X)
215 | [ |- context[@take_lev ?G ?L [ ?X @@@ ?L ] ] ] =>
216 rewrite (take_lemma' G L X)
217 | [ |- context[@take_lev ?G ?N (?A,,?B)] ] =>
218 change (@take_lev G N (A,,B)) with ((@take_lev G N A),,(@take_lev G N B))
219 | [ |- context[@take_lev ?G ?N (T_Leaf None)] ] =>
220 change (@take_lev G N (T_Leaf (@None (LeveledHaskType G ★)))) with (T_Leaf (@None (LeveledHaskType G ★)))
224 (*******************************************************************************)
227 Context (hetmet_flatten : WeakExprVar).
228 Context (hetmet_unflatten : WeakExprVar).
229 Context (hetmet_id : WeakExprVar).
230 Context {unitTy : forall TV, RawHaskType TV ECKind -> RawHaskType TV ★ }.
231 Context {prodTy : forall TV, RawHaskType TV ECKind -> RawHaskType TV ★ -> RawHaskType TV ★ -> RawHaskType TV ★ }.
232 Context {gaTy : forall TV, RawHaskType TV ECKind -> RawHaskType TV ★ -> RawHaskType TV ★ -> RawHaskType TV ★ }.
234 Definition ga_mk_tree' {TV}(ec:RawHaskType TV ECKind)(tr:Tree ??(RawHaskType TV ★)) : RawHaskType TV ★ :=
235 reduceTree (unitTy TV ec) (prodTy TV ec) tr.
237 Definition ga_mk_tree {Γ}(ec:HaskType Γ ECKind)(tr:Tree ??(HaskType Γ ★)) : HaskType Γ ★ :=
238 fun TV ite => ga_mk_tree' (ec TV ite) (mapOptionTree (fun x => x TV ite) tr).
240 Definition ga_mk_raw {TV}(ec:RawHaskType TV ECKind)(ant suc:Tree ??(RawHaskType TV ★)) : RawHaskType TV ★ :=
243 (ga_mk_tree' ec suc).
245 Definition ga_mk {Γ}(ec:HaskType Γ ECKind)(ant suc:Tree ??(HaskType Γ ★)) : HaskType Γ ★ :=
246 fun TV ite => gaTy TV (ec TV ite) (ga_mk_tree ec ant TV ite) (ga_mk_tree ec suc TV ite).
250 * - code types <[t]>@c become garrows c () t
251 * - free variables of type t at a level lev deeper than the succedent become garrows c () t
252 * - free variables at the level of the succedent become
254 Fixpoint flatten_rawtype {TV}{κ}(exp: RawHaskType TV κ) : RawHaskType TV κ :=
257 | TAll _ y => TAll _ (fun v => flatten_rawtype (y v))
258 | TApp _ _ x y => TApp (flatten_rawtype x) (flatten_rawtype y)
260 | TCoerc _ t1 t2 t => TCoerc (flatten_rawtype t1) (flatten_rawtype t2) (flatten_rawtype t)
262 | TCode ec e => let e' := flatten_rawtype e
263 in ga_mk_raw ec (unleaves_ (take_arg_types e')) [drop_arg_types e']
264 | TyFunApp tfc kl k lt => TyFunApp tfc kl k (flatten_rawtype_list _ lt)
266 with flatten_rawtype_list {TV}(lk:list Kind)(exp:@RawHaskTypeList TV lk) : @RawHaskTypeList TV lk :=
267 match exp in @RawHaskTypeList _ LK return @RawHaskTypeList TV LK with
268 | TyFunApp_nil => TyFunApp_nil
269 | TyFunApp_cons κ kl t rest => TyFunApp_cons _ _ (flatten_rawtype t) (flatten_rawtype_list _ rest)
272 Definition flatten_type {Γ}{κ}(ht:HaskType Γ κ) : HaskType Γ κ :=
273 fun TV ite => flatten_rawtype (ht TV ite).
275 Fixpoint levels_to_tcode {Γ}(ht:HaskType Γ ★)(lev:HaskLevel Γ) : HaskType Γ ★ :=
277 | nil => flatten_type ht
278 | ec::lev' => @ga_mk _ (v2t ec) [] [levels_to_tcode ht lev']
281 Definition flatten_leveled_type {Γ}(ht:LeveledHaskType Γ ★) : LeveledHaskType Γ ★ :=
282 levels_to_tcode (unlev ht) (getlev ht) @@ nil.
286 Axiom literal_types_unchanged : forall Γ l, flatten_type (literalType l) = literalType(Γ:=Γ) l.
288 Axiom flatten_coercion : forall Γ Δ κ (σ τ:HaskType Γ κ) (γ:HaskCoercion Γ Δ (σ ∼∼∼ τ)),
289 HaskCoercion Γ Δ (flatten_type σ ∼∼∼ flatten_type τ).
291 Axiom flatten_commutes_with_substT :
292 forall κ Γ (Δ:CoercionEnv Γ) (σ:∀ TV, InstantiatedTypeEnv TV Γ → TV κ → RawHaskType TV ★) (τ:HaskType Γ κ),
293 flatten_type (substT σ τ) = substT (fun TV ite v => flatten_rawtype (σ TV ite v))
296 Axiom flatten_commutes_with_HaskTAll :
297 forall κ Γ (Δ:CoercionEnv Γ) (σ:∀ TV, InstantiatedTypeEnv TV Γ → TV κ → RawHaskType TV ★),
298 flatten_type (HaskTAll κ σ) = HaskTAll κ (fun TV ite v => flatten_rawtype (σ TV ite v)).
300 Axiom flatten_commutes_with_HaskTApp :
301 forall κ Γ (Δ:CoercionEnv Γ) (σ:∀ TV, InstantiatedTypeEnv TV Γ → TV κ → RawHaskType TV ★),
302 flatten_type (HaskTApp (weakF σ) (FreshHaskTyVar κ)) =
303 HaskTApp (weakF (fun TV ite v => flatten_rawtype (σ TV ite v))) (FreshHaskTyVar κ).
305 Axiom flatten_commutes_with_weakLT : forall (Γ:TypeEnv) κ t,
306 flatten_leveled_type (weakLT(Γ:=Γ)(κ:=κ) t) = weakLT(Γ:=Γ)(κ:=κ) (flatten_leveled_type t).
308 Axiom globals_do_not_have_code_types : forall (Γ:TypeEnv) (g:Global Γ) v,
309 flatten_type (g v) = g v.
311 (* This tries to assign a single level to the entire succedent of a judgment. If the succedent has types from different
312 * levels (should not happen) it just picks one; if the succedent has no non-None leaves (also should not happen) it
314 Definition getΓ (j:Judg) := match j with Γ > _ > _ |- _ => Γ end.
315 Definition getSuc (j:Judg) : Tree ??(LeveledHaskType (getΓ j) ★) :=
316 match j as J return Tree ??(LeveledHaskType (getΓ J) ★) with Γ > _ > _ |- s => s end.
317 Fixpoint getjlev {Γ}(tt:Tree ??(LeveledHaskType Γ ★)) : HaskLevel Γ :=
320 | T_Leaf (Some (_ @@ lev)) => lev
322 match getjlev b1 with
328 (* "n" is the maximum depth remaining AFTER flattening *)
329 Definition flatten_judgment (j:Judg) :=
330 match j as J return Judg with
331 Γ > Δ > ant |- suc =>
332 match getjlev suc with
333 | nil => Γ > Δ > mapOptionTree flatten_leveled_type ant
334 |- mapOptionTree flatten_leveled_type suc
336 | (ec::lev') => Γ > Δ > mapOptionTree flatten_leveled_type (drop_lev (ec::lev') ant)
338 (mapOptionTree (flatten_type ○ unlev) (take_lev (ec::lev') ant))
339 (mapOptionTree (flatten_type ○ unlev) suc )
340 @@ nil] (* we know the level of all of suc *)
345 { ga_id : ∀ Γ Δ ec l a , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec a a @@ l] ]
346 ; ga_cancelr : ∀ Γ Δ ec l a , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec (a,,[]) a @@ l] ]
347 ; ga_cancell : ∀ Γ Δ ec l a , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec ([],,a) a @@ l] ]
348 ; ga_uncancelr : ∀ Γ Δ ec l a , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec a (a,,[]) @@ l] ]
349 ; ga_uncancell : ∀ Γ Δ ec l a , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec a ([],,a) @@ l] ]
350 ; ga_assoc : ∀ Γ Δ ec l a b c, ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec ((a,,b),,c) (a,,(b,,c)) @@ l] ]
351 ; ga_unassoc : ∀ Γ Δ ec l a b c, ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec (a,,(b,,c)) ((a,,b),,c) @@ l] ]
352 ; ga_swap : ∀ Γ Δ ec l a b , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec (a,,b) (b,,a) @@ l] ]
353 ; ga_drop : ∀ Γ Δ ec l a , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec a [] @@ l] ]
354 ; ga_copy : ∀ Γ Δ ec l a , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec a (a,,a) @@ l] ]
355 ; ga_first : ∀ Γ Δ ec l a b x, ND Rule [] [Γ > Δ > [@ga_mk Γ ec a b @@ l] |- [@ga_mk Γ ec (a,,x) (b,,x) @@ l] ]
356 ; ga_second : ∀ Γ Δ ec l a b x, ND Rule [] [Γ > Δ > [@ga_mk Γ ec a b @@ l] |- [@ga_mk Γ ec (x,,a) (x,,b) @@ l] ]
357 ; ga_lit : ∀ Γ Δ ec l lit , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec [] [literalType lit] @@ l] ]
358 ; ga_curry : ∀ Γ Δ ec l a b c, ND Rule [] [Γ > Δ > [@ga_mk Γ ec (a,,[b]) [c] @@ l] |- [@ga_mk Γ ec a [b ---> c] @@ l] ]
359 ; ga_comp : ∀ Γ Δ ec l a b c, ND Rule [] [Γ > Δ > [@ga_mk Γ ec a b @@ l],,[@ga_mk Γ ec b c @@ l] |- [@ga_mk Γ ec a c @@ l] ]
360 ; ga_apply : ∀ Γ Δ ec l a a' b c,
361 ND Rule [] [Γ > Δ > [@ga_mk Γ ec a [b ---> c] @@ l],,[@ga_mk Γ ec a' [b] @@ l] |- [@ga_mk Γ ec (a,,a') [c] @@ l] ]
362 ; ga_kappa : ∀ Γ Δ ec l a b Σ, ND Rule
363 [Γ > Δ > Σ,,[@ga_mk Γ ec [] a @@ l] |- [@ga_mk Γ ec [] b @@ l] ]
364 [Γ > Δ > Σ |- [@ga_mk Γ ec a b @@ l] ]
366 Context `(gar:garrow).
368 Notation "a ~~~~> b" := (@ga_mk _ _ a b) (at level 20).
370 Definition boost : forall Γ Δ ant x y {lev},
371 ND Rule [] [ Γ > Δ > [x@@lev] |- [y@@lev] ] ->
372 ND Rule [ Γ > Δ > ant |- [x@@lev] ] [ Γ > Δ > ant |- [y@@lev] ].
374 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanL ].
375 eapply nd_comp; [ idtac | eapply nd_rule; apply (@RLet Γ Δ [] ant y x lev) ].
376 eapply nd_comp; [ apply nd_rlecnac | idtac ].
386 Definition postcompose' : ∀ Γ Δ ec lev a b c Σ,
387 ND Rule [] [ Γ > Δ > Σ |- [@ga_mk Γ ec a b @@ lev] ] ->
388 ND Rule [] [ Γ > Δ > Σ,,[@ga_mk Γ ec b c @@ lev] |- [@ga_mk Γ ec a c @@ lev] ].
390 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RExch ].
391 eapply nd_comp; [ idtac
392 | eapply nd_rule; apply (@RLet Γ Δ [@ga_mk _ ec b c @@lev] Σ (@ga_mk _ ec a c) (@ga_mk _ ec a b) lev) ].
393 eapply nd_comp; [ apply nd_llecnac | idtac ].
396 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RExch ].
400 Definition precompose Γ Δ ec : forall a x y z lev,
402 [ Γ > Δ > a |- [@ga_mk _ ec y z @@ lev] ]
403 [ Γ > Δ > a,,[@ga_mk _ ec x y @@ lev] |- [@ga_mk _ ec x z @@ lev] ].
412 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RExch ].
418 Definition precompose' : ∀ Γ Δ ec lev a b c Σ,
419 ND Rule [] [ Γ > Δ > Σ |- [@ga_mk Γ ec b c @@ lev] ] ->
420 ND Rule [] [ Γ > Δ > Σ,,[@ga_mk Γ ec a b @@ lev] |- [@ga_mk Γ ec a c @@ lev] ].
427 Definition postcompose : ∀ Γ Δ ec lev a b c,
428 ND Rule [] [ Γ > Δ > [] |- [@ga_mk Γ ec a b @@ lev] ] ->
429 ND Rule [] [ Γ > Δ > [@ga_mk Γ ec b c @@ lev] |- [@ga_mk Γ ec a c @@ lev] ].
439 Definition firstify : ∀ Γ Δ ec lev a b c Σ,
440 ND Rule [] [ Γ > Δ > Σ |- [@ga_mk Γ ec a b @@ lev] ] ->
441 ND Rule [] [ Γ > Δ > Σ |- [@ga_mk Γ ec (a,,c) (b,,c) @@ lev] ].
443 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanL ].
444 eapply nd_comp; [ idtac | eapply nd_rule; apply RLet ].
445 eapply nd_comp; [ apply nd_llecnac | idtac ].
448 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RuCanL ].
452 Definition secondify : ∀ Γ Δ ec lev a b c Σ,
453 ND Rule [] [ Γ > Δ > Σ |- [@ga_mk Γ ec a b @@ lev] ] ->
454 ND Rule [] [ Γ > Δ > Σ |- [@ga_mk Γ ec (c,,a) (c,,b) @@ lev] ].
456 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanL ].
457 eapply nd_comp; [ idtac | eapply nd_rule; apply RLet ].
458 eapply nd_comp; [ apply nd_llecnac | idtac ].
461 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RuCanL ].
465 Lemma ga_unkappa : ∀ Γ Δ ec l z a b Σ,
467 [Γ > Δ > Σ |- [@ga_mk Γ ec a b @@ l] ]
468 [Γ > Δ > Σ,,[@ga_mk Γ ec z a @@ l] |- [@ga_mk Γ ec z b @@ l] ].
470 set (ga_comp Γ Δ ec l z a b) as q.
472 set (@RLet Γ Δ) as q'.
473 set (@RLet Γ Δ [@ga_mk _ ec z a @@ l] Σ (@ga_mk _ ec z b) (@ga_mk _ ec a b) l) as q''.
494 Lemma ga_unkappa' : ∀ Γ Δ ec l a b Σ x,
496 [Γ > Δ > Σ |- [@ga_mk Γ ec (a,,x) b @@ l] ]
497 [Γ > Δ > Σ,,[@ga_mk Γ ec [] a @@ l] |- [@ga_mk Γ ec x b @@ l] ].
499 eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
500 eapply nd_comp; [ apply nd_llecnac | idtac ].
504 eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
505 eapply nd_comp; [ apply nd_llecnac | idtac ].
512 Lemma ga_kappa' : ∀ Γ Δ ec l a b Σ x,
514 [Γ > Δ > Σ,,[@ga_mk Γ ec [] a @@ l] |- [@ga_mk Γ ec x b @@ l] ]
515 [Γ > Δ > Σ |- [@ga_mk Γ ec (a,,x) b @@ l] ].
516 apply (Prelude_error "ga_kappa not supported yet (BIG FIXME)").
519 (* useful for cutting down on the pretty-printed noise
521 Notation "` x" := (take_lev _ x) (at level 20).
522 Notation "`` x" := (mapOptionTree unlev x) (at level 20).
523 Notation "``` x" := (drop_lev _ x) (at level 20).
525 Definition flatten_arrangement' :
526 forall Γ (Δ:CoercionEnv Γ)
527 (ec:HaskTyVar Γ ECKind) (lev:HaskLevel Γ) (ant1 ant2:Tree ??(LeveledHaskType Γ ★)) (r:Arrange ant1 ant2),
528 ND Rule [] [Γ > Δ > [] |- [@ga_mk _ (v2t ec) (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) ant2))
529 (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) ant1)) @@ nil] ].
532 refine (fix flatten ant1 ant2 (r:Arrange ant1 ant2):
533 ND Rule [] [Γ > Δ > [] |- [@ga_mk _ (v2t ec)
534 (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) ant2))
535 (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) ant1)) @@ nil]] :=
536 match r as R in Arrange A B return
537 ND Rule [] [Γ > Δ > [] |- [@ga_mk _ (v2t ec)
538 (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) B))
539 (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) A)) @@ nil]]
541 | RId a => let case_RId := tt in ga_id _ _ _ _ _
542 | RCanL a => let case_RCanL := tt in ga_uncancell _ _ _ _ _
543 | RCanR a => let case_RCanR := tt in ga_uncancelr _ _ _ _ _
544 | RuCanL a => let case_RuCanL := tt in ga_cancell _ _ _ _ _
545 | RuCanR a => let case_RuCanR := tt in ga_cancelr _ _ _ _ _
546 | RAssoc a b c => let case_RAssoc := tt in ga_assoc _ _ _ _ _ _ _
547 | RCossa a b c => let case_RCossa := tt in ga_unassoc _ _ _ _ _ _ _
548 | RExch a b => let case_RExch := tt in ga_swap _ _ _ _ _ _
549 | RWeak a => let case_RWeak := tt in ga_drop _ _ _ _ _
550 | RCont a => let case_RCont := tt in ga_copy _ _ _ _ _
551 | RLeft a b c r' => let case_RLeft := tt in flatten _ _ r' ;; boost _ _ _ _ _ (ga_second _ _ _ _ _ _ _)
552 | RRight a b c r' => let case_RRight := tt in flatten _ _ r' ;; boost _ _ _ _ _ (ga_first _ _ _ _ _ _ _)
553 | RComp c b a r1 r2 => let case_RComp := tt in (fun r1' r2' => _) (flatten _ _ r1) (flatten _ _ r2)
554 end); clear flatten; repeat take_simplify; repeat drop_simplify; intros.
557 set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) a)) as a' in *.
558 set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) b)) as b' in *.
559 set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) c)) as c' in *.
560 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RCanL ].
561 eapply nd_comp; [ idtac | eapply nd_rule; apply
562 (@RLet Γ Δ [] [] (@ga_mk _ (v2t ec) a' c') (@ga_mk _ (v2t ec) a' b')) ].
563 eapply nd_comp; [ apply nd_llecnac | idtac ].
566 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RuCanL ].
567 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RCanR ].
568 eapply nd_comp; [ idtac | eapply nd_rule; apply
569 (@RLet Γ Δ [@ga_mk _ (v2t ec) a' b' @@ _] [] (@ga_mk _ (v2t ec) a' c') (@ga_mk _ (v2t ec) b' c'))].
570 eapply nd_comp; [ apply nd_llecnac | idtac ].
576 Definition flatten_arrangement :
577 forall Γ (Δ:CoercionEnv Γ) n
578 (ec:HaskTyVar Γ ECKind) (lev:HaskLevel Γ) (ant1 ant2:Tree ??(LeveledHaskType Γ ★)) (r:Arrange ant1 ant2) succ,
580 [Γ > Δ > mapOptionTree (flatten_leveled_type ) (drop_lev n ant1)
581 |- [@ga_mk _ (v2t ec)
582 (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) ant1))
583 (mapOptionTree (flatten_type ○ unlev) succ) @@ nil]]
584 [Γ > Δ > mapOptionTree (flatten_leveled_type ) (drop_lev n ant2)
585 |- [@ga_mk _ (v2t ec)
586 (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) ant2))
587 (mapOptionTree (flatten_type ○ unlev) succ) @@ nil]].
589 refine ( _ ;; (boost _ _ _ _ _ (postcompose _ _ _ _ _ _ _ (flatten_arrangement' Γ Δ ec lev ant1 ant2 r)))).
592 refine ((fix flatten ant1 ant2 (r:Arrange ant1 ant2) :=
593 match r as R in Arrange A B return
594 Arrange (mapOptionTree (flatten_leveled_type ) (drop_lev _ A))
595 (mapOptionTree (flatten_leveled_type ) (drop_lev _ B)) with
596 | RId a => let case_RId := tt in RId _
597 | RCanL a => let case_RCanL := tt in RCanL _
598 | RCanR a => let case_RCanR := tt in RCanR _
599 | RuCanL a => let case_RuCanL := tt in RuCanL _
600 | RuCanR a => let case_RuCanR := tt in RuCanR _
601 | RAssoc a b c => let case_RAssoc := tt in RAssoc _ _ _
602 | RCossa a b c => let case_RCossa := tt in RCossa _ _ _
603 | RExch a b => let case_RExch := tt in RExch _ _
604 | RWeak a => let case_RWeak := tt in RWeak _
605 | RCont a => let case_RCont := tt in RCont _
606 | RLeft a b c r' => let case_RLeft := tt in RLeft _ (flatten _ _ r')
607 | RRight a b c r' => let case_RRight := tt in RRight _ (flatten _ _ r')
608 | RComp a b c r1 r2 => let case_RComp := tt in RComp (flatten _ _ r1) (flatten _ _ r2)
609 end) ant1 ant2 r); clear flatten; repeat take_simplify; repeat drop_simplify; intros.
612 Definition flatten_arrangement'' :
613 forall Γ Δ ant1 ant2 succ (r:Arrange ant1 ant2),
614 ND Rule (mapOptionTree (flatten_judgment ) [Γ > Δ > ant1 |- succ])
615 (mapOptionTree (flatten_judgment ) [Γ > Δ > ant2 |- succ]).
618 set (getjlev succ) as succ_lev.
619 assert (succ_lev=getjlev succ).
638 eapply RComp; [ apply IHr1 | apply IHr2 ].
640 apply flatten_arrangement.
644 Definition ga_join Γ Δ Σ₁ Σ₂ a b ec :
645 ND Rule [] [Γ > Δ > Σ₁ |- [@ga_mk _ ec [] a @@ nil]] ->
646 ND Rule [] [Γ > Δ > Σ₂ |- [@ga_mk _ ec [] b @@ nil]] ->
647 ND Rule [] [Γ > Δ > Σ₁,,Σ₂ |- [@ga_mk _ ec [] (a,,b) @@ nil]].
650 apply secondify with (c:=a) in pfb.
653 eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
654 eapply nd_comp; [ eapply nd_llecnac | idtac ].
663 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanL ].
669 Definition arrange_brak : forall Γ Δ ec succ t,
671 [Γ > Δ > mapOptionTree (flatten_leveled_type ) (drop_lev (ec :: nil) succ),,
672 [(@ga_mk _ (v2t ec) [] (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: nil) succ))) @@ nil] |- [t @@ nil]]
673 [Γ > Δ > mapOptionTree (flatten_leveled_type ) succ |- [t @@ nil]].
676 set (@arrange' _ succ (levelMatch (ec::nil))) as q.
677 set (arrangeMap _ _ flatten_leveled_type q) as y.
686 eapply nd_comp; [ apply nd_llecnac | idtac ].
687 eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
692 induction succ; try destruct a; simpl.
698 destruct l as [t' lev'].
699 destruct lev' as [|ec' lev'].
703 set (@eqd_dec (HaskLevel Γ) (haskLevelEqDecidable Γ) (ec' :: lev') (ec :: nil)) as q.
708 unfold flatten_leveled_type.
725 Definition arrange_empty_tree : forall {T}{A}(q:Tree A)(t:Tree ??T),
726 t = mapTree (fun _:A => None) q ->
734 destruct t; try destruct o; inversion H.
735 set (IHq1 _ H1) as x1.
736 set (IHq2 _ H2) as x2.
747 (* Definition unarrange_empty_tree : forall {T}{A}(t:Tree ??T)(q:Tree A),
748 t = mapTree (fun _:A => None) q ->
752 Definition decide_tree_empty : forall {T:Type}(t:Tree ??T),
753 sum { q:Tree unit & t = mapTree (fun _ => None) q } unit.
758 | T_Branch b1 b2 => let b1' := foo b1 in let b2' := foo b2 in _
778 Definition arrange_esc : forall Γ Δ ec succ t,
780 [Γ > Δ > mapOptionTree (flatten_leveled_type ) succ |- [t @@ nil]]
781 [Γ > Δ > mapOptionTree (flatten_leveled_type ) (drop_lev (ec :: nil) succ),,
782 [(@ga_mk _ (v2t ec) [] (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: nil) succ))) @@ nil] |- [t @@ nil]].
784 set (@arrange _ succ (levelMatch (ec::nil))) as q.
785 set (@drop_lev Γ (ec::nil) succ) as q'.
786 assert (@drop_lev Γ (ec::nil) succ=q') as H.
788 unfold drop_lev in H.
789 unfold mkDropFlags in H.
792 set (arrangeMap _ _ flatten_leveled_type q) as y.
799 set (mapOptionTree flatten_leveled_type (dropT (mkFlags (liftBoolFunc false (bnot ○ levelMatch (ec :: nil))) succ))) as q.
800 destruct (decide_tree_empty q); [ idtac | apply (Prelude_error "escapifying open code not yet supported") ].
804 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RExch ].
805 set (fun z z' => @RLet Γ Δ z (mapOptionTree flatten_leveled_type q') t z' nil) as q''.
806 eapply nd_comp; [ idtac | eapply nd_rule; apply q'' ].
808 eapply nd_comp; [ apply nd_rlecnac | idtac ].
812 eapply RComp; [ idtac | apply RCanR ].
814 apply (@arrange_empty_tree _ _ _ _ e).
818 eapply (@RVar Γ Δ t nil).
826 eapply decide_tree_empty.
829 set (dropT (mkFlags (liftBoolFunc false (bnot ○ levelMatch (ec :: nil))) succ)) as escapified.
830 destruct (decide_tree_empty escapified).
837 unfold mkDropFlags; simpl.
841 destruct (General.list_eq_dec h0 (ec :: nil)).
857 apply (Prelude_error "escapifying code with multi-leaf antecedents is not supported").
861 Lemma mapOptionTree_distributes
862 : forall T R (a b:Tree ??T) (f:T->R),
863 mapOptionTree f (a,,b) = (mapOptionTree f a),,(mapOptionTree f b).
867 Lemma unlev_relev : forall {Γ}(t:Tree ??(HaskType Γ ★)) lev, mapOptionTree unlev (t @@@ lev) = t.
870 destruct a; reflexivity.
871 rewrite <- IHt1 at 2.
872 rewrite <- IHt2 at 2.
876 Lemma tree_of_nothing : forall Γ ec t a,
877 Arrange (a,,mapOptionTree flatten_leveled_type (drop_lev(Γ:=Γ) (ec :: nil) (t @@@ (ec :: nil)))) a.
879 induction t; try destruct o; try destruct a0.
888 Transparent drop_lev.
899 Lemma tree_of_nothing' : forall Γ ec t a,
900 Arrange a (a,,mapOptionTree flatten_leveled_type (drop_lev(Γ:=Γ) (ec :: nil) (t @@@ (ec :: nil)))).
902 induction t; try destruct o; try destruct a0.
911 Transparent drop_lev.
925 Lemma krunk : forall Γ (ec:HaskTyVar Γ ECKind) t,
926 flatten_type (<[ ec |- t ]>)
928 (mapOptionTree flatten_type (take_arg_types_as_tree t))
929 [ flatten_type (drop_arg_types_as_tree t)].
931 unfold flatten_type at 1.
934 apply phoas_extensionality.
939 rewrite <- mapOptionTree_compose.
940 unfold take_arg_types_as_tree.
942 replace (flatten_type (drop_arg_types_as_tree t) tv ite)
943 with (drop_arg_types (flatten_rawtype (t tv ite))).
944 replace (unleaves_ (take_arg_types (flatten_rawtype (t tv ite))))
945 with ((mapOptionTree (fun x : HaskType Γ ★ => flatten_type x tv ite)
947 (take_trustme (count_arg_types (t (fun _ : Kind => unit) (ite_unit Γ)))
948 (fun TV : Kind → Type => take_arg_types ○ t TV))))).
951 clear hetmet_flatten.
952 clear hetmet_unflatten.
960 Definition flatten_proof :
963 ND Rule (mapOptionTree (flatten_judgment ) h) (mapOptionTree (flatten_judgment ) c).
965 eapply nd_map'; [ idtac | apply X ].
971 (match X as R in SRule H C with
972 | SBrak Γ Δ t ec succ lev => let case_SBrak := tt in _
973 | SEsc Γ Δ t ec succ lev => let case_SEsc := tt in _
974 | SFlat h c r => let case_SFlat := tt in _
978 refine (match r as R in Rule H C with
979 | RArrange Γ Δ a b x d => let case_RArrange := tt in _
980 | RNote Γ Δ Σ τ l n => let case_RNote := tt in _
981 | RLit Γ Δ l _ => let case_RLit := tt in _
982 | RVar Γ Δ σ lev => let case_RVar := tt in _
983 | RGlobal Γ Δ σ l wev => let case_RGlobal := tt in _
984 | RLam Γ Δ Σ tx te lev => let case_RLam := tt in _
985 | RCast Γ Δ Σ σ τ lev γ => let case_RCast := tt in _
986 | RAbsT Γ Δ Σ κ σ lev => let case_RAbsT := tt in _
987 | RAppT Γ Δ Σ κ σ τ lev => let case_RAppT := tt in _
988 | RAppCo Γ Δ Σ κ σ₁ σ₂ γ σ lev => let case_RAppCo := tt in _
989 | RAbsCo Γ Δ Σ κ σ σ₁ σ₂ lev => let case_RAbsCo := tt in _
990 | RApp Γ Δ Σ₁ Σ₂ tx te lev => let case_RApp := tt in _
991 | RLet Γ Δ Σ₁ Σ₂ σ₁ σ₂ lev => let case_RLet := tt in _
992 | RJoin Γ p lri m x q => let case_RJoin := tt in _
993 | RVoid _ _ => let case_RVoid := tt in _
994 | RBrak Γ Δ t ec succ lev => let case_RBrak := tt in _
995 | REsc Γ Δ t ec succ lev => let case_REsc := tt in _
996 | RCase Γ Δ lev tc Σ avars tbranches alts => let case_RCase := tt in _
997 | RLetRec Γ Δ lri x y t => let case_RLetRec := tt in _
1000 destruct case_RArrange.
1001 apply (flatten_arrangement'' Γ Δ a b x d).
1003 destruct case_RBrak.
1004 apply (Prelude_error "found unskolemized Brak rule; this shouldn't happen").
1007 apply (Prelude_error "found unskolemized Esc rule; this shouldn't happen").
1009 destruct case_RNote.
1012 apply nd_rule; apply RNote; auto.
1013 apply nd_rule; apply RNote; auto.
1018 unfold flatten_leveled_type.
1020 rewrite literal_types_unchanged.
1021 apply nd_rule; apply RLit.
1022 unfold take_lev; simpl.
1023 unfold drop_lev; simpl.
1025 rewrite literal_types_unchanged.
1029 Opaque flatten_judgment.
1031 Transparent flatten_judgment.
1033 unfold flatten_judgment.
1036 apply nd_rule. apply RVar.
1037 repeat drop_simplify.
1038 repeat take_simplify.
1042 destruct case_RGlobal.
1046 destruct l as [|ec lev]; simpl.
1047 destruct (eqd_dec (g:CoreVar) (hetmet_flatten:CoreVar)).
1048 set (flatten_type (g wev)) as t.
1049 set (RGlobal _ Δ nil (mkGlobal Γ t hetmet_id)) as q.
1054 destruct (eqd_dec (g:CoreVar) (hetmet_unflatten:CoreVar)).
1055 set (flatten_type (g wev)) as t.
1056 set (RGlobal _ Δ nil (mkGlobal Γ t hetmet_id)) as q.
1061 unfold flatten_leveled_type. simpl.
1062 apply nd_rule; rewrite globals_do_not_have_code_types.
1064 apply (Prelude_error "found RGlobal at depth >0; globals should never appear inside code brackets unless escaped").
1070 destruct lev as [|ec lev]; simpl; [ apply nd_rule; apply RLam; auto | idtac ].
1071 repeat drop_simplify.
1072 repeat take_simplify.
1082 destruct case_RCast.
1084 destruct lev as [|ec lev]; simpl; [ apply nd_rule; apply RCast; auto | idtac ].
1086 apply flatten_coercion; auto.
1087 apply (Prelude_error "RCast at level >0; casting inside of code brackets is currently not supported").
1089 destruct case_RJoin.
1091 destruct (getjlev x); destruct (getjlev q);
1092 [ apply nd_rule; apply RJoin | idtac | idtac | idtac ];
1093 apply (Prelude_error "RJoin at depth >0").
1098 destruct lev as [|ec lev]. simpl. apply nd_rule.
1099 unfold flatten_leveled_type at 4.
1100 unfold flatten_leveled_type at 2.
1102 replace (flatten_type (tx ---> te))
1103 with (flatten_type tx ---> flatten_type te).
1107 repeat drop_simplify.
1108 repeat take_simplify.
1109 rewrite mapOptionTree_distributes.
1110 set (mapOptionTree (flatten_leveled_type ) (drop_lev (ec :: lev) Σ₁)) as Σ₁'.
1111 set (mapOptionTree (flatten_leveled_type ) (drop_lev (ec :: lev) Σ₂)) as Σ₂'.
1112 set (take_lev (ec :: lev) Σ₁) as Σ₁''.
1113 set (take_lev (ec :: lev) Σ₂) as Σ₂''.
1114 replace (flatten_type (tx ---> te)) with ((flatten_type tx) ---> (flatten_type te)).
1115 apply (Prelude_error "FIXME: ga_apply").
1119 Notation "` x" := (take_lev _ x).
1120 Notation "`` x" := (mapOptionTree unlev x) (at level 20).
1121 Notation "``` x" := ((drop_lev _ x)) (at level 20).
1122 Notation "!<[]> x" := (flatten_type _ x) (at level 1).
1123 Notation "!<[@]> x" := (mapOptionTree flatten_leveled_type x) (at level 1).
1128 destruct lev as [|ec lev]; simpl; [ apply nd_rule; apply RLet; auto | idtac ].
1129 repeat drop_simplify.
1130 repeat take_simplify.
1134 eapply nd_prod; [ idtac | apply nd_id ].
1150 destruct case_RVoid.
1155 destruct case_RAppT.
1156 simpl. destruct lev; simpl.
1157 unfold flatten_leveled_type.
1159 rewrite flatten_commutes_with_HaskTAll.
1160 rewrite flatten_commutes_with_substT.
1165 apply (Prelude_error "found type application at level >0; this is not supported").
1167 destruct case_RAbsT.
1168 simpl. destruct lev; simpl.
1169 unfold flatten_leveled_type at 4.
1170 unfold flatten_leveled_type at 2.
1172 rewrite flatten_commutes_with_HaskTAll.
1173 rewrite flatten_commutes_with_HaskTApp.
1174 eapply nd_comp; [ idtac | eapply nd_rule; eapply RAbsT ].
1176 set (mapOptionTree (flatten_leveled_type ) (mapOptionTree (weakLT(κ:=κ)) Σ)) as a.
1177 set (mapOptionTree (weakLT(κ:=κ)) (mapOptionTree (flatten_leveled_type ) Σ)) as q'.
1185 rewrite flatten_commutes_with_weakLT.
1196 apply (Prelude_error "found type abstraction at level >0; this is not supported").
1198 destruct case_RAppCo.
1199 simpl. destruct lev; simpl.
1200 unfold flatten_leveled_type at 4.
1201 unfold flatten_leveled_type at 2.
1202 unfold flatten_type.
1206 apply flatten_coercion.
1208 apply (Prelude_error "found coercion application at level >0; this is not supported").
1210 destruct case_RAbsCo.
1211 simpl. destruct lev; simpl.
1212 unfold flatten_type.
1214 apply (Prelude_error "AbsCo not supported (FIXME)").
1215 apply (Prelude_error "found coercion abstraction at level >0; this is not supported").
1217 destruct case_RLetRec.
1220 apply (Prelude_error "LetRec not supported (FIXME)").
1222 destruct case_RCase.
1224 apply (Prelude_error "Case not supported (BIG FIXME)").
1226 destruct case_SBrak.
1230 set (drop_lev (ec :: nil) (take_arg_types_as_tree t @@@ (ec :: nil))) as empty_tree.
1232 rewrite take_lemma'.
1234 rewrite mapOptionTree_compose.
1235 rewrite mapOptionTree_compose.
1236 rewrite unlev_relev.
1237 rewrite <- mapOptionTree_compose.
1238 unfold flatten_leveled_type at 4.
1241 set (mapOptionTree flatten_leveled_type (drop_lev (ec :: nil) succ)) as succ_host.
1242 set (mapOptionTree (flatten_type ○ unlev)(take_lev (ec :: nil) succ)) as succ_guest.
1243 set (mapOptionTree flatten_type (take_arg_types_as_tree t)) as succ_args.
1245 eapply nd_comp; [ eapply nd_rule; eapply RArrange; apply tree_of_nothing | idtac ].
1246 refine (ga_unkappa' Γ Δ (v2t ec) nil _ _ _ _ ;; _).
1250 apply (Prelude_error "found Brak at depth >0 indicating 3-level code; only two-level code is currently supported").
1256 unfold flatten_leveled_type at 2.
1259 rewrite mapOptionTree_compose.
1263 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply tree_of_nothing' ].
1265 rewrite take_lemma'.
1266 rewrite unlev_relev.
1267 rewrite <- mapOptionTree_compose.
1268 eapply nd_comp; [ apply (arrange_esc _ _ ec) | idtac ].
1270 set (decide_tree_empty (take_lev (ec :: nil) succ)) as q'.
1276 set (mapOptionTree flatten_leveled_type (drop_lev (ec :: nil) succ)) as succ_host.
1277 set (mapOptionTree flatten_type (take_arg_types_as_tree t)) as succ_args.
1279 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RCanR ].
1280 eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
1281 eapply nd_comp; [ apply nd_llecnac | idtac ].
1282 apply nd_prod; [ idtac | eapply boost ].
1285 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanR ].
1293 refine ( _ ;; (boost _ _ _ _ _ (postcompose _ _ _ _ _ _ _ _))).
1301 refine ( _ ;; (boost _ _ _ _ _ (postcompose _ _ _ _ _ _ _ _))).
1303 refine ( _ ;; (boost _ _ _ _ _ (postcompose _ _ _ _ _ _ _ _))).
1309 (* environment has non-empty leaves *)
1312 (* nesting too deep *)
1313 apply (Prelude_error "found Esc at depth >0 indicating 3-level code; only two-level code is currently supported").
1316 Definition skolemize_and_flatten_proof :
1320 (mapOptionTree (flatten_judgment ○ skolemize_judgment) h)
1321 (mapOptionTree (flatten_judgment ○ skolemize_judgment) c).
1323 rewrite mapOptionTree_compose.
1324 rewrite mapOptionTree_compose.
1325 apply flatten_proof.
1326 apply skolemize_proof.
1331 (* to do: establish some metric on judgments (max length of level of any succedent type, probably), show how to
1332 * calculate it, and show that the flattening procedure above drives it down by one *)
1335 Instance FlatteningFunctor {Γ}{Δ}{ec} : Functor (JudgmentsL (PCF Γ Δ ec)) (TypesL (SystemFCa Γ Δ)) (obact) :=
1336 { fmor := FlatteningFunctor_fmor }.
1338 Definition ReificationFunctor Γ Δ : Functor (JudgmentsL _ _ (PCF n Γ Δ)) SystemFCa' (mapOptionTree brakifyJudg).
1339 refine {| fmor := ReificationFunctor_fmor Γ Δ |}; unfold hom; unfold ob; simpl ; intros.
1341 Definition PCF_SMME (n:nat)(Γ:TypeEnv)(Δ:CoercionEnv Γ) : ProgrammingLanguageSMME.
1342 refine {| plsmme_pl := PCF n Γ Δ |}.
1345 Definition SystemFCa_SMME (n:nat)(Γ:TypeEnv)(Δ:CoercionEnv Γ) : ProgrammingLanguageSMME.
1346 refine {| plsmme_pl := SystemFCa n Γ Δ |}.
1349 Definition ReificationFunctorMonoidal n : MonoidalFunctor (JudgmentsN n) (JudgmentsN (S n)) (ReificationFunctor n).
1353 Definition PCF_SystemFCa_two_level n Γ Δ : TwoLevelLanguage (PCF_SMME n Γ Δ) (SystemFCa_SMME (S n) Γ Δ).
1356 (* ... and the retraction exists *)
1360 Implicit Arguments garrow [ ].