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 NaturalDeductionContext.
13 Require Import Coq.Strings.String.
14 Require Import Coq.Lists.List.
16 Require Import HaskKinds.
17 Require Import HaskCoreTypes.
18 Require Import HaskCoreVars.
19 Require Import HaskWeakTypes.
20 Require Import HaskWeakVars.
21 Require Import HaskLiterals.
22 Require Import HaskTyCons.
23 Require Import HaskStrongTypes.
24 Require Import HaskProof.
25 Require Import NaturalDeduction.
27 Require Import HaskStrongTypes.
28 Require Import HaskStrong.
29 Require Import HaskProof.
30 Require Import HaskStrongToProof.
31 Require Import HaskProofToStrong.
32 Require Import HaskWeakToStrong.
34 Require Import HaskSkolemizer.
37 Set Printing Width 130.
40 * The flattening transformation. Currently only TWO-level languages are
41 * supported, and the level-1 sublanguage is rather limited.
43 * This file abuses terminology pretty badly. For purposes of this file,
44 * "PCF" means "the level-1 sublanguage" and "FC" (aka System FC) means
45 * the whole language (level-0 language including bracketed level-1 terms)
47 Section HaskFlattener.
52 | [ |- context[@eqd_dec ?T ?V ?X ?X] ] =>
53 destruct (@eqd_dec T V X X) as [eqd_dec1 | eqd_dec2];
54 [ clear eqd_dec1 | set (eqd_dec2 (refl_equal _)) as eqd_dec2'; inversion eqd_dec2' ]
57 Definition v2t {Γ}(ec:HaskTyVar Γ ECKind) : HaskType Γ ECKind := fun TV ite => TVar (ec TV ite).
59 Definition levelMatch {Γ}(lev:HaskLevel Γ) : LeveledHaskType Γ ★ -> bool :=
60 fun t => match t with ttype@@tlev => if eqd_dec tlev lev then true else false end.
62 (* In a tree of types, replace any type at depth "lev" or greater None *)
63 Definition mkDropFlags {Γ}(lev:HaskLevel Γ)(tt:Tree ??(LeveledHaskType Γ ★)) : TreeFlags tt :=
64 mkFlags (liftBoolFunc false (levelMatch lev)) tt.
66 Definition drop_lev {Γ}(lev:HaskLevel Γ)(tt:Tree ??(LeveledHaskType Γ ★)) : Tree ??(LeveledHaskType Γ ★) :=
67 dropT (mkDropFlags lev tt).
69 (* The opposite: replace any type which is NOT at level "lev" with None *)
70 Definition mkTakeFlags {Γ}(lev:HaskLevel Γ)(tt:Tree ??(LeveledHaskType Γ ★)) : TreeFlags tt :=
71 mkFlags (liftBoolFunc true (bnot ○ levelMatch lev)) tt.
73 Definition take_lev {Γ}(lev:HaskLevel Γ)(tt:Tree ??(LeveledHaskType Γ ★)) : Tree ??(LeveledHaskType Γ ★) :=
74 dropT (mkTakeFlags lev tt).
76 mapOptionTree (fun x => flatten_type (unlev x))
77 (maybeTree (takeT tt (mkFlags (
79 | Some (ttype @@ tlev) => if eqd_dec tlev lev then true else false
84 Definition maybeTree {T}(t:??(Tree ??T)) : Tree ??T :=
91 Lemma drop_lev_lemma : forall Γ (lev:HaskLevel Γ) x, drop_lev lev [x @@ lev] = [].
103 Lemma drop_lev_lemma_s : forall Γ (lev:HaskLevel Γ) ec x, drop_lev (ec::lev) [x @@ (ec :: lev)] = [].
114 Lemma take_lemma : forall Γ (lev:HaskLevel Γ) x, take_lev lev [x @@ lev] = [x @@ lev].
125 Lemma take_lemma' : forall Γ (lev:HaskLevel Γ) x, take_lev lev (x @@@ lev) = x @@@ lev.
128 destruct a; simpl; try reflexivity.
131 rewrite <- IHx1 at 2.
132 rewrite <- IHx2 at 2.
136 Ltac drop_simplify :=
138 | [ |- context[@drop_lev ?G ?L [ ?X @@ ?L ] ] ] =>
139 rewrite (drop_lev_lemma G L X)
140 | [ |- context[@drop_lev ?G (?E :: ?L) [ ?X @@ (?E :: ?L) ] ] ] =>
141 rewrite (drop_lev_lemma_s G L E X)
142 | [ |- context[@drop_lev ?G ?N (?A,,?B)] ] =>
143 change (@drop_lev G N (A,,B)) with ((@drop_lev G N A),,(@drop_lev G N B))
144 | [ |- context[@drop_lev ?G ?N (T_Leaf None)] ] =>
145 change (@drop_lev G N (T_Leaf (@None (LeveledHaskType G ★)))) with (T_Leaf (@None (LeveledHaskType G ★)))
148 Ltac take_simplify :=
150 | [ |- context[@take_lev ?G ?L [ ?X @@ ?L ] ] ] =>
151 rewrite (take_lemma G L X)
152 | [ |- context[@take_lev ?G ?L [ ?X @@@ ?L ] ] ] =>
153 rewrite (take_lemma' G L X)
154 | [ |- context[@take_lev ?G ?N (?A,,?B)] ] =>
155 change (@take_lev G N (A,,B)) with ((@take_lev G N A),,(@take_lev G N B))
156 | [ |- context[@take_lev ?G ?N (T_Leaf None)] ] =>
157 change (@take_lev G N (T_Leaf (@None (LeveledHaskType G ★)))) with (T_Leaf (@None (LeveledHaskType G ★)))
161 (*******************************************************************************)
164 Context (hetmet_flatten : WeakExprVar).
165 Context (hetmet_unflatten : WeakExprVar).
166 Context (hetmet_id : WeakExprVar).
167 Context {unitTy : forall TV, RawHaskType TV ECKind -> RawHaskType TV ★ }.
168 Context {prodTy : forall TV, RawHaskType TV ECKind -> RawHaskType TV ★ -> RawHaskType TV ★ -> RawHaskType TV ★ }.
169 Context {gaTy : forall TV, RawHaskType TV ECKind -> RawHaskType TV ★ -> RawHaskType TV ★ -> RawHaskType TV ★ }.
171 Definition ga_mk_tree' {TV}(ec:RawHaskType TV ECKind)(tr:Tree ??(RawHaskType TV ★)) : RawHaskType TV ★ :=
172 reduceTree (unitTy TV ec) (prodTy TV ec) tr.
174 Definition ga_mk_tree {Γ}(ec:HaskType Γ ECKind)(tr:Tree ??(HaskType Γ ★)) : HaskType Γ ★ :=
175 fun TV ite => ga_mk_tree' (ec TV ite) (mapOptionTree (fun x => x TV ite) tr).
177 Definition ga_mk_raw {TV}(ec:RawHaskType TV ECKind)(ant suc:Tree ??(RawHaskType TV ★)) : RawHaskType TV ★ :=
180 (ga_mk_tree' ec suc).
182 Definition ga_mk {Γ}(ec:HaskType Γ ECKind)(ant suc:Tree ??(HaskType Γ ★)) : HaskType Γ ★ :=
183 fun TV ite => gaTy TV (ec TV ite) (ga_mk_tree ec ant TV ite) (ga_mk_tree ec suc TV ite).
187 * - code types <[t]>@c become garrows c () t
188 * - free variables of type t at a level lev deeper than the succedent become garrows c () t
189 * - free variables at the level of the succedent become
191 Fixpoint flatten_rawtype {TV}{κ}(exp: RawHaskType TV κ) : RawHaskType TV κ :=
194 | TAll _ y => TAll _ (fun v => flatten_rawtype (y v))
195 | TApp _ _ x y => TApp (flatten_rawtype x) (flatten_rawtype y)
197 | TCoerc _ t1 t2 t => TCoerc (flatten_rawtype t1) (flatten_rawtype t2) (flatten_rawtype t)
199 | TCode ec e => let e' := flatten_rawtype e
200 in ga_mk_raw ec (unleaves_ (take_arg_types e')) [drop_arg_types e']
201 | TyFunApp tfc kl k lt => TyFunApp tfc kl k (flatten_rawtype_list _ lt)
203 with flatten_rawtype_list {TV}(lk:list Kind)(exp:@RawHaskTypeList TV lk) : @RawHaskTypeList TV lk :=
204 match exp in @RawHaskTypeList _ LK return @RawHaskTypeList TV LK with
205 | TyFunApp_nil => TyFunApp_nil
206 | TyFunApp_cons κ kl t rest => TyFunApp_cons _ _ (flatten_rawtype t) (flatten_rawtype_list _ rest)
209 Definition flatten_type {Γ}{κ}(ht:HaskType Γ κ) : HaskType Γ κ :=
210 fun TV ite => flatten_rawtype (ht TV ite).
212 Fixpoint levels_to_tcode {Γ}(ht:HaskType Γ ★)(lev:HaskLevel Γ) : HaskType Γ ★ :=
214 | nil => flatten_type ht
215 | ec::lev' => @ga_mk _ (v2t ec) [] [levels_to_tcode ht lev']
218 Definition flatten_leveled_type {Γ}(ht:LeveledHaskType Γ ★) : LeveledHaskType Γ ★ :=
219 levels_to_tcode (unlev ht) (getlev ht) @@ nil.
223 Axiom literal_types_unchanged : forall Γ l, flatten_type (literalType l) = literalType(Γ:=Γ) l.
225 Axiom flatten_coercion : forall Γ Δ κ (σ τ:HaskType Γ κ) (γ:HaskCoercion Γ Δ (σ ∼∼∼ τ)),
226 HaskCoercion Γ Δ (flatten_type σ ∼∼∼ flatten_type τ).
228 Axiom flatten_commutes_with_substT :
229 forall κ Γ (Δ:CoercionEnv Γ) (σ:∀ TV, InstantiatedTypeEnv TV Γ → TV κ → RawHaskType TV ★) (τ:HaskType Γ κ),
230 flatten_type (substT σ τ) = substT (fun TV ite v => flatten_rawtype (σ TV ite v))
233 Axiom flatten_commutes_with_HaskTAll :
234 forall κ Γ (Δ:CoercionEnv Γ) (σ:∀ TV, InstantiatedTypeEnv TV Γ → TV κ → RawHaskType TV ★),
235 flatten_type (HaskTAll κ σ) = HaskTAll κ (fun TV ite v => flatten_rawtype (σ TV ite v)).
237 Axiom flatten_commutes_with_HaskTApp :
238 forall κ Γ (Δ:CoercionEnv Γ) (σ:∀ TV, InstantiatedTypeEnv TV Γ → TV κ → RawHaskType TV ★),
239 flatten_type (HaskTApp (weakF σ) (FreshHaskTyVar κ)) =
240 HaskTApp (weakF (fun TV ite v => flatten_rawtype (σ TV ite v))) (FreshHaskTyVar κ).
242 Axiom flatten_commutes_with_weakLT : forall (Γ:TypeEnv) κ t,
243 flatten_leveled_type (weakLT(Γ:=Γ)(κ:=κ) t) = weakLT(Γ:=Γ)(κ:=κ) (flatten_leveled_type t).
245 Axiom globals_do_not_have_code_types : forall (Γ:TypeEnv) (g:Global Γ) v,
246 flatten_type (g v) = g v.
248 (* "n" is the maximum depth remaining AFTER flattening *)
249 Definition flatten_judgment (j:Judg) :=
250 match j as J return Judg with
251 | Γ > Δ > ant |- suc @ nil => Γ > Δ > mapOptionTree flatten_leveled_type ant
252 |- mapOptionTree flatten_type suc @ nil
253 | Γ > Δ > ant |- suc @ (ec::lev') => Γ > Δ > mapOptionTree flatten_leveled_type (drop_lev (ec::lev') ant)
255 (mapOptionTree (flatten_type ○ unlev) (take_lev (ec::lev') ant))
256 (mapOptionTree flatten_type suc )
261 { ga_id : ∀ Γ Δ ec l a , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec a a ]@l ]
262 ; ga_cancelr : ∀ Γ Δ ec l a , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec (a,,[]) a ]@l ]
263 ; ga_cancell : ∀ Γ Δ ec l a , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec ([],,a) a ]@l ]
264 ; ga_uncancelr : ∀ Γ Δ ec l a , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec a (a,,[]) ]@l ]
265 ; ga_uncancell : ∀ Γ Δ ec l a , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec a ([],,a) ]@l ]
266 ; ga_assoc : ∀ Γ Δ ec l a b c, ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec ((a,,b),,c) (a,,(b,,c)) ]@l ]
267 ; ga_unassoc : ∀ Γ Δ ec l a b c, ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec (a,,(b,,c)) ((a,,b),,c) ]@l ]
268 ; ga_swap : ∀ Γ Δ ec l a b , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec (a,,b) (b,,a) ]@l ]
269 ; ga_drop : ∀ Γ Δ ec l a , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec a [] ]@l ]
270 ; ga_copy : ∀ Γ Δ ec l a , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec a (a,,a) ]@l ]
271 ; ga_first : ∀ Γ Δ ec l a b x, ND Rule [] [Γ > Δ > [@ga_mk Γ ec a b @@l] |- [@ga_mk Γ ec (a,,x) (b,,x) ]@l ]
272 ; ga_second : ∀ Γ Δ ec l a b x, ND Rule [] [Γ > Δ > [@ga_mk Γ ec a b @@l] |- [@ga_mk Γ ec (x,,a) (x,,b) ]@l ]
273 ; ga_lit : ∀ Γ Δ ec l lit , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec [] [literalType lit] ]@l ]
274 ; ga_curry : ∀ Γ Δ ec l a b c, ND Rule [] [Γ > Δ > [@ga_mk Γ ec (a,,[b]) [c] @@ l] |- [@ga_mk Γ ec a [b ---> c] ]@ l ]
275 ; 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 ]
276 ; ga_apply : ∀ Γ Δ ec l a a' b c,
277 ND Rule [] [Γ > Δ > [@ga_mk Γ ec a [b ---> c] @@ l],,[@ga_mk Γ ec a' [b] @@ l] |- [@ga_mk Γ ec (a,,a') [c] ]@l ]
278 ; ga_kappa : ∀ Γ Δ ec l a b Σ, ND Rule
279 [Γ > Δ > Σ,,[@ga_mk Γ ec [] a @@ l] |- [@ga_mk Γ ec [] b ]@l ]
280 [Γ > Δ > Σ |- [@ga_mk Γ ec a b ]@l ]
282 Context `(gar:garrow).
284 Notation "a ~~~~> b" := (@ga_mk _ _ a b) (at level 20).
286 Definition boost : forall Γ Δ ant x y {lev},
287 ND Rule [] [ Γ > Δ > [x@@lev] |- [y]@lev ] ->
288 ND Rule [ Γ > Δ > ant |- [x]@lev ] [ Γ > Δ > ant |- [y]@lev ].
290 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ACanR ].
291 eapply nd_comp; [ idtac | eapply nd_rule; apply RLet ].
292 eapply nd_comp; [ apply nd_rlecnac | idtac ].
302 Definition precompose Γ Δ ec : forall a x y z lev,
304 [ Γ > Δ > a |- [@ga_mk _ ec y z ]@lev ]
305 [ Γ > Δ > a,,[@ga_mk _ ec x y @@ lev] |- [@ga_mk _ ec x z ]@lev ].
307 eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
308 eapply nd_comp; [ apply nd_rlecnac | idtac ].
311 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AExch ].
315 Definition precompose' Γ Δ ec : forall a b x y z lev,
317 [ Γ > Δ > a,,b |- [@ga_mk _ ec y z ]@lev ]
318 [ Γ > Δ > a,,([@ga_mk _ ec x y @@ lev],,b) |- [@ga_mk _ ec x z ]@lev ].
320 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ALeft; eapply AExch ].
321 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AuAssoc ].
325 Definition postcompose_ Γ Δ ec : forall a x y z lev,
327 [ Γ > Δ > a |- [@ga_mk _ ec x y ]@lev ]
328 [ Γ > Δ > a,,[@ga_mk _ ec y z @@ lev] |- [@ga_mk _ ec x z ]@lev ].
330 eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
331 eapply nd_comp; [ apply nd_rlecnac | idtac ].
337 Definition postcompose Γ Δ ec : forall x y z lev,
338 ND Rule [] [ Γ > Δ > [] |- [@ga_mk _ ec x y ]@lev ] ->
339 ND Rule [] [ Γ > Δ > [@ga_mk _ ec y z @@ lev] |- [@ga_mk _ ec x z ]@lev ].
341 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ACanL ].
342 eapply nd_comp; [ idtac | eapply postcompose_ ].
346 Definition first_nd : ∀ Γ Δ ec lev a b c Σ,
347 ND Rule [ Γ > Δ > Σ |- [@ga_mk Γ ec a b ]@lev ]
348 [ Γ > Δ > Σ |- [@ga_mk Γ ec (a,,c) (b,,c) ]@lev ].
350 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ACanR ].
351 eapply nd_comp; [ idtac | eapply nd_rule; apply RLet ].
352 eapply nd_comp; [ apply nd_rlecnac | idtac ].
355 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AuCanR ].
359 Definition firstify : ∀ Γ Δ ec lev a b c Σ,
360 ND Rule [] [ Γ > Δ > Σ |- [@ga_mk Γ ec a b ]@lev ] ->
361 ND Rule [] [ Γ > Δ > Σ |- [@ga_mk Γ ec (a,,c) (b,,c) ]@lev ].
368 Definition second_nd : ∀ Γ Δ ec lev a b c Σ,
370 [ Γ > Δ > Σ |- [@ga_mk Γ ec a b ]@lev ]
371 [ Γ > Δ > Σ |- [@ga_mk Γ ec (c,,a) (c,,b) ]@lev ].
373 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ACanR ].
374 eapply nd_comp; [ idtac | eapply nd_rule; apply RLet ].
375 eapply nd_comp; [ apply nd_rlecnac | idtac ].
378 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AuCanR ].
382 Definition secondify : ∀ Γ Δ ec lev a b c Σ,
383 ND Rule [] [ Γ > Δ > Σ |- [@ga_mk Γ ec a b ]@lev ] ->
384 ND Rule [] [ Γ > Δ > Σ |- [@ga_mk Γ ec (c,,a) (c,,b) ]@lev ].
391 Lemma ga_unkappa : ∀ Γ Δ ec l a b Σ x,
393 [Γ > Δ > Σ |- [@ga_mk Γ ec (a,,x) b ]@l ]
394 [Γ > Δ > Σ,,[@ga_mk Γ ec [] a @@ l] |- [@ga_mk Γ ec x b ]@l ].
396 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AExch ].
397 eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
398 eapply nd_comp; [ apply nd_llecnac | idtac ].
402 eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
403 eapply nd_comp; [ apply nd_llecnac | idtac ].
407 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AExch ].
411 (* useful for cutting down on the pretty-printed noise
413 Notation "` x" := (take_lev _ x) (at level 20).
414 Notation "`` x" := (mapOptionTree unlev x) (at level 20).
415 Notation "``` x" := (drop_lev _ x) (at level 20).
417 Definition flatten_arrangement' :
418 forall Γ (Δ:CoercionEnv Γ)
419 (ec:HaskTyVar Γ ECKind) (lev:HaskLevel Γ) (ant1 ant2:Tree ??(LeveledHaskType Γ ★)) (r:Arrange ant1 ant2),
420 ND Rule [] [Γ > Δ > [] |- [@ga_mk _ (v2t ec) (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) ant2))
421 (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) ant1)) ]@nil ].
424 refine (fix flatten ant1 ant2 (r:Arrange ant1 ant2):
425 ND Rule [] [Γ > Δ > [] |- [@ga_mk _ (v2t ec)
426 (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) ant2))
427 (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) ant1)) ]@nil] :=
428 match r as R in Arrange A B return
429 ND Rule [] [Γ > Δ > [] |- [@ga_mk _ (v2t ec)
430 (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) B))
431 (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) A)) ]@nil]
433 | AId a => let case_AId := tt in ga_id _ _ _ _ _
434 | ACanL a => let case_ACanL := tt in ga_uncancell _ _ _ _ _
435 | ACanR a => let case_ACanR := tt in ga_uncancelr _ _ _ _ _
436 | AuCanL a => let case_AuCanL := tt in ga_cancell _ _ _ _ _
437 | AuCanR a => let case_AuCanR := tt in ga_cancelr _ _ _ _ _
438 | AAssoc a b c => let case_AAssoc := tt in ga_assoc _ _ _ _ _ _ _
439 | AuAssoc a b c => let case_AuAssoc := tt in ga_unassoc _ _ _ _ _ _ _
440 | AExch a b => let case_AExch := tt in ga_swap _ _ _ _ _ _
441 | AWeak a => let case_AWeak := tt in ga_drop _ _ _ _ _
442 | ACont a => let case_ACont := tt in ga_copy _ _ _ _ _
443 | ALeft a b c r' => let case_ALeft := tt in flatten _ _ r' ;; boost _ _ _ _ _ (ga_second _ _ _ _ _ _ _)
444 | ARight a b c r' => let case_ARight := tt in flatten _ _ r' ;; boost _ _ _ _ _ (ga_first _ _ _ _ _ _ _)
445 | AComp c b a r1 r2 => let case_AComp := tt in (fun r1' r2' => _) (flatten _ _ r1) (flatten _ _ r2)
446 end); clear flatten; repeat take_simplify; repeat drop_simplify; intros.
449 set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) a)) as a' in *.
450 set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) b)) as b' in *.
451 set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) c)) as c' in *.
452 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply ACanL ].
453 eapply nd_comp; [ idtac | eapply nd_rule; apply
454 (@RLet Γ Δ [] [] (@ga_mk _ (v2t ec) a' b') (@ga_mk _ (v2t ec) a' c')) ].
455 eapply nd_comp; [ apply nd_llecnac | idtac ].
458 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply AuCanR ].
459 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply ACanL ].
460 eapply nd_comp; [ idtac | eapply nd_rule; apply RLet ].
461 eapply nd_comp; [ apply nd_llecnac | idtac ].
464 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AExch ].
468 Definition flatten_arrangement :
469 forall Γ (Δ:CoercionEnv Γ) n
470 (ec:HaskTyVar Γ ECKind) (lev:HaskLevel Γ) (ant1 ant2:Tree ??(LeveledHaskType Γ ★)) (r:Arrange ant1 ant2) succ,
472 [Γ > Δ > mapOptionTree (flatten_leveled_type ) (drop_lev n ant1)
473 |- [@ga_mk _ (v2t ec)
474 (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) ant1))
475 (mapOptionTree (flatten_type ) succ) ]@nil]
476 [Γ > Δ > mapOptionTree (flatten_leveled_type ) (drop_lev n ant2)
477 |- [@ga_mk _ (v2t ec)
478 (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) ant2))
479 (mapOptionTree (flatten_type ) succ) ]@nil].
481 refine ( _ ;; (boost _ _ _ _ _ (postcompose _ _ _ _ _ _ _ (flatten_arrangement' Γ Δ ec lev ant1 ant2 r)))).
484 refine ((fix flatten ant1 ant2 (r:Arrange ant1 ant2) :=
485 match r as R in Arrange A B return
486 Arrange (mapOptionTree (flatten_leveled_type ) (drop_lev _ A))
487 (mapOptionTree (flatten_leveled_type ) (drop_lev _ B)) with
488 | AId a => let case_AId := tt in AId _
489 | ACanL a => let case_ACanL := tt in ACanL _
490 | ACanR a => let case_ACanR := tt in ACanR _
491 | AuCanL a => let case_AuCanL := tt in AuCanL _
492 | AuCanR a => let case_AuCanR := tt in AuCanR _
493 | AAssoc a b c => let case_AAssoc := tt in AAssoc _ _ _
494 | AuAssoc a b c => let case_AuAssoc := tt in AuAssoc _ _ _
495 | AExch a b => let case_AExch := tt in AExch _ _
496 | AWeak a => let case_AWeak := tt in AWeak _
497 | ACont a => let case_ACont := tt in ACont _
498 | ALeft a b c r' => let case_ALeft := tt in ALeft _ (flatten _ _ r')
499 | ARight a b c r' => let case_ARight := tt in ARight _ (flatten _ _ r')
500 | AComp a b c r1 r2 => let case_AComp := tt in AComp (flatten _ _ r1) (flatten _ _ r2)
501 end) ant1 ant2 r); clear flatten; repeat take_simplify; repeat drop_simplify; intros.
504 Definition flatten_arrangement'' :
505 forall Γ Δ ant1 ant2 succ l (r:Arrange ant1 ant2),
506 ND Rule (mapOptionTree (flatten_judgment ) [Γ > Δ > ant1 |- succ @ l])
507 (mapOptionTree (flatten_judgment ) [Γ > Δ > ant2 |- succ @ l]).
521 apply AExch. (* TO DO: check for all-leaf trees here *)
526 eapply AComp; [ apply IHr1 | apply IHr2 ].
528 apply flatten_arrangement.
532 Definition ga_join Γ Δ Σ₁ Σ₂ a b ec :
533 ND Rule [] [Γ > Δ > Σ₁ |- [@ga_mk _ ec [] a ]@nil] ->
534 ND Rule [] [Γ > Δ > Σ₂ |- [@ga_mk _ ec [] b ]@nil] ->
535 ND Rule [] [Γ > Δ > Σ₁,,Σ₂ |- [@ga_mk _ ec [] (a,,b) ]@nil].
538 apply secondify with (c:=a) in pfb.
539 apply firstify with (c:=[]) in pfa.
540 eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
541 eapply nd_comp; [ eapply nd_llecnac | idtac ].
546 eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
547 eapply nd_comp; [ apply nd_llecnac | idtac ].
549 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ACanL ].
550 eapply nd_comp; [ idtac | eapply postcompose_ ].
553 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AExch ].
554 eapply nd_comp; [ idtac | eapply precompose ].
558 Definition arrange_brak : forall Γ Δ ec succ t,
561 [(@ga_mk _ (v2t ec) [] (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: nil) succ))) @@ nil],,
562 mapOptionTree (flatten_leveled_type ) (drop_lev (ec :: nil) succ) |- [t]@nil]
563 [Γ > Δ > mapOptionTree (flatten_leveled_type ) succ |- [t]@nil].
567 set (@arrangeUnPartition _ succ (levelMatch (ec::nil))) as q.
568 set (arrangeMap _ _ flatten_leveled_type q) as y.
576 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AExch ].
578 eapply nd_comp; [ apply nd_llecnac | idtac ].
579 eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
584 induction succ; try destruct a; simpl.
590 destruct l as [t' lev'].
591 destruct lev' as [|ec' lev'].
595 set (@eqd_dec (HaskLevel Γ) (haskLevelEqDecidable Γ) (ec' :: lev') (ec :: nil)) as q.
600 unfold flatten_leveled_type.
617 Definition arrange_esc : forall Γ Δ ec succ t,
619 [Γ > Δ > mapOptionTree (flatten_leveled_type ) succ |- [t]@nil]
621 [(@ga_mk _ (v2t ec) [] (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: nil) succ))) @@ nil],,
622 mapOptionTree (flatten_leveled_type ) (drop_lev (ec :: nil) succ) |- [t]@nil].
624 set (@arrangePartition _ succ (levelMatch (ec::nil))) as q.
625 set (@drop_lev Γ (ec::nil) succ) as q'.
626 assert (@drop_lev Γ (ec::nil) succ=q') as H.
628 unfold drop_lev in H.
629 unfold mkDropFlags in H.
632 set (arrangeMap _ _ flatten_leveled_type q) as y.
639 set (mapOptionTree flatten_leveled_type (dropT (mkFlags (liftBoolFunc false (bnot ○ levelMatch (ec :: nil))) succ))) as q.
640 destruct (decide_tree_empty q); [ idtac | apply (Prelude_error "escapifying open code not yet supported") ].
644 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply AExch ].
645 set (fun z z' => @RLet Γ Δ z (mapOptionTree flatten_leveled_type q') t z' nil) as q''.
646 eapply nd_comp; [ idtac | eapply nd_rule; apply RLet ].
648 eapply nd_comp; [ apply nd_rlecnac | idtac ].
652 eapply AComp; [ idtac | apply ACanR ].
654 apply (@arrangeCancelEmptyTree _ _ _ _ e).
658 eapply (@RVar Γ Δ t nil).
666 eapply decide_tree_empty.
669 set (dropT (mkFlags (liftBoolFunc false (bnot ○ levelMatch (ec :: nil))) succ)) as escapified.
670 destruct (decide_tree_empty escapified).
677 unfold mkDropFlags; simpl.
681 destruct (General.list_eq_dec h0 (ec :: nil)).
697 apply (Prelude_error "escapifying code with multi-leaf antecedents is not supported").
701 Lemma unlev_relev : forall {Γ}(t:Tree ??(HaskType Γ ★)) lev, mapOptionTree unlev (t @@@ lev) = t.
704 destruct a; reflexivity.
705 rewrite <- IHt1 at 2.
706 rewrite <- IHt2 at 2.
710 Lemma tree_of_nothing : forall Γ ec t,
711 Arrange (mapOptionTree flatten_leveled_type (drop_lev(Γ:=Γ) (ec :: nil) (t @@@ (ec :: nil)))) [].
713 induction t; try destruct o; try destruct a.
720 eapply AComp; [ idtac | apply ACanL ].
721 eapply AComp; [ idtac | eapply ALeft; apply IHt2 ].
724 Transparent drop_lev.
731 Lemma tree_of_nothing' : forall Γ ec t,
732 Arrange [] (mapOptionTree flatten_leveled_type (drop_lev(Γ:=Γ) (ec :: nil) (t @@@ (ec :: nil)))).
734 induction t; try destruct o; try destruct a.
741 eapply AComp; [ apply AuCanL | idtac ].
742 eapply AComp; [ eapply ARight; apply IHt1 | idtac ].
745 Transparent drop_lev.
752 Lemma krunk : forall Γ (ec:HaskTyVar Γ ECKind) t,
753 flatten_type (<[ ec |- t ]>)
755 (mapOptionTree flatten_type (take_arg_types_as_tree t))
756 [ flatten_type (drop_arg_types_as_tree t)].
758 unfold flatten_type at 1.
761 apply phoas_extensionality.
766 rewrite <- mapOptionTree_compose.
767 unfold take_arg_types_as_tree.
769 replace (flatten_type (drop_arg_types_as_tree t) tv ite)
770 with (drop_arg_types (flatten_rawtype (t tv ite))).
771 replace (unleaves_ (take_arg_types (flatten_rawtype (t tv ite))))
772 with ((mapOptionTree (fun x : HaskType Γ ★ => flatten_type x tv ite)
774 (take_trustme (count_arg_types (t (fun _ : Kind => unit) (ite_unit Γ)))
775 (fun TV : Kind → Type => take_arg_types ○ t TV))))).
778 clear hetmet_flatten.
779 clear hetmet_unflatten.
787 Definition flatten_proof :
790 ND Rule (mapOptionTree (flatten_judgment ) h) (mapOptionTree (flatten_judgment ) c).
792 eapply nd_map'; [ idtac | apply X ].
798 (match X as R in SRule H C with
799 | SBrak Γ Δ t ec succ lev => let case_SBrak := tt in _
800 | SEsc Γ Δ t ec succ lev => let case_SEsc := tt in _
801 | SFlat h c r => let case_SFlat := tt in _
805 refine (match r as R in Rule H C with
806 | RArrange Γ Δ a b x l d => let case_RArrange := tt in _
807 | RNote Γ Δ Σ τ l n => let case_RNote := tt in _
808 | RLit Γ Δ l _ => let case_RLit := tt in _
809 | RVar Γ Δ σ lev => let case_RVar := tt in _
810 | RGlobal Γ Δ σ l wev => let case_RGlobal := tt in _
811 | RLam Γ Δ Σ tx te lev => let case_RLam := tt in _
812 | RCast Γ Δ Σ σ τ lev γ => let case_RCast := tt in _
813 | RAbsT Γ Δ Σ κ σ lev => let case_RAbsT := tt in _
814 | RAppT Γ Δ Σ κ σ τ lev => let case_RAppT := tt in _
815 | RAppCo Γ Δ Σ κ σ₁ σ₂ γ σ lev => let case_RAppCo := tt in _
816 | RAbsCo Γ Δ Σ κ σ σ₁ σ₂ lev => let case_RAbsCo := tt in _
817 | RApp Γ Δ Σ₁ Σ₂ tx te lev => let case_RApp := tt in _
818 | RLet Γ Δ Σ₁ Σ₂ σ₁ σ₂ lev => let case_RLet := tt in _
819 | RWhere Γ Δ Σ₁ Σ₂ Σ₃ σ₁ σ₂ lev => let case_RWhere := tt in _
820 | RJoin Γ p lri m x q l => let case_RJoin := tt in _
821 | RVoid _ _ l => let case_RVoid := tt in _
822 | RBrak Γ Δ t ec succ lev => let case_RBrak := tt in _
823 | REsc Γ Δ t ec succ lev => let case_REsc := tt in _
824 | RCase Γ Δ lev tc Σ avars tbranches alts => let case_RCase := tt in _
825 | RLetRec Γ Δ lri x y t => let case_RLetRec := tt in _
828 destruct case_RArrange.
829 apply (flatten_arrangement'' Γ Δ a b x _ d).
832 apply (Prelude_error "found unskolemized Brak rule; this shouldn't happen").
835 apply (Prelude_error "found unskolemized Esc rule; this shouldn't happen").
840 apply nd_rule; apply RNote; auto.
841 apply nd_rule; apply RNote; auto.
846 unfold flatten_leveled_type.
848 rewrite literal_types_unchanged.
849 apply nd_rule; apply RLit.
850 unfold take_lev; simpl.
851 unfold drop_lev; simpl.
853 rewrite literal_types_unchanged.
857 Opaque flatten_judgment.
859 Transparent flatten_judgment.
861 unfold flatten_judgment.
863 apply nd_rule. apply RVar.
864 repeat drop_simplify.
865 repeat take_simplify.
869 destruct case_RGlobal.
873 destruct l as [|ec lev]; simpl.
874 destruct (eqd_dec (g:CoreVar) (hetmet_flatten:CoreVar)).
875 set (flatten_type (g wev)) as t.
876 set (RGlobal _ Δ nil (mkGlobal Γ t hetmet_id)) as q.
881 destruct (eqd_dec (g:CoreVar) (hetmet_unflatten:CoreVar)).
882 set (flatten_type (g wev)) as t.
883 set (RGlobal _ Δ nil (mkGlobal Γ t hetmet_id)) as q.
888 unfold flatten_leveled_type. simpl.
889 apply nd_rule; rewrite globals_do_not_have_code_types.
891 apply (Prelude_error "found RGlobal at depth >0; globals should never appear inside code brackets unless escaped").
897 destruct lev as [|ec lev]; simpl; [ apply nd_rule; apply RLam; auto | idtac ].
898 repeat drop_simplify.
899 repeat take_simplify.
911 destruct lev as [|ec lev]; simpl; [ apply nd_rule; apply RCast; auto | idtac ].
913 apply flatten_coercion; auto.
914 apply (Prelude_error "RCast at level >0; casting inside of code brackets is currently not supported").
919 [ apply nd_rule; apply RJoin | idtac ];
920 apply (Prelude_error "RJoin at depth >0").
925 destruct lev as [|ec lev].
926 unfold flatten_type at 1.
931 repeat drop_simplify.
932 repeat take_simplify.
933 rewrite mapOptionTree_distributes.
934 set (mapOptionTree (flatten_leveled_type ) (drop_lev (ec :: lev) Σ₁)) as Σ₁'.
935 set (mapOptionTree (flatten_leveled_type ) (drop_lev (ec :: lev) Σ₂)) as Σ₂'.
936 set (take_lev (ec :: lev) Σ₁) as Σ₁''.
937 set (take_lev (ec :: lev) Σ₂) as Σ₂''.
938 replace (flatten_type (tx ---> te)) with ((flatten_type tx) ---> (flatten_type te)).
939 apply (Prelude_error "FIXME: ga_apply").
943 Notation "` x" := (take_lev _ x).
944 Notation "`` x" := (mapOptionTree unlev x) (at level 20).
945 Notation "``` x" := ((drop_lev _ x)) (at level 20).
946 Notation "!<[]> x" := (flatten_type _ x) (at level 1).
947 Notation "!<[@]> x" := (mapOptionTree flatten_leveled_type x) (at level 1).
952 destruct lev as [|ec lev]; simpl; [ apply nd_rule; apply RLet; auto | idtac ].
953 repeat drop_simplify.
954 repeat take_simplify.
957 set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) Σ₁)) as Σ₁'.
958 set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) Σ₂)) as Σ₂'.
959 set (mapOptionTree flatten_leveled_type (drop_lev (ec :: lev) Σ₁)) as Σ₁''.
960 set (mapOptionTree flatten_leveled_type (drop_lev (ec :: lev) Σ₂)) as Σ₂''.
963 eapply nd_prod; [ idtac | apply nd_id ].
965 apply (ga_first _ _ _ _ _ _ Σ₂').
967 eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
970 eapply nd_comp; [ eapply nd_rule; eapply RArrange; eapply ACanL | idtac ].
971 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AExch (* okay *)].
974 destruct case_RWhere.
976 destruct lev as [|ec lev]; simpl; [ apply nd_rule; apply RWhere; auto | idtac ].
977 repeat take_simplify.
978 repeat drop_simplify.
981 set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) Σ₁)) as Σ₁'.
982 set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) Σ₂)) as Σ₂'.
983 set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) Σ₃)) as Σ₃'.
984 set (mapOptionTree flatten_leveled_type (drop_lev (ec :: lev) Σ₁)) as Σ₁''.
985 set (mapOptionTree flatten_leveled_type (drop_lev (ec :: lev) Σ₂)) as Σ₂''.
986 set (mapOptionTree flatten_leveled_type (drop_lev (ec :: lev) Σ₃)) as Σ₃''.
989 eapply nd_prod; [ eapply nd_id | idtac ].
990 eapply (first_nd _ _ _ _ _ _ Σ₃').
992 eapply nd_prod; [ eapply nd_id | idtac ].
993 eapply (second_nd _ _ _ _ _ _ Σ₁').
995 eapply nd_comp; [ idtac | eapply nd_rule; eapply RWhere ].
996 apply nd_prod; [ idtac | apply nd_id ].
997 eapply nd_comp; [ idtac | eapply precompose' ].
1003 destruct case_RVoid.
1008 apply (Prelude_error "RVoid at level >0").
1010 destruct case_RAppT.
1011 simpl. destruct lev; simpl.
1012 unfold flatten_leveled_type.
1014 rewrite flatten_commutes_with_HaskTAll.
1015 rewrite flatten_commutes_with_substT.
1020 apply (Prelude_error "found type application at level >0; this is not supported").
1022 destruct case_RAbsT.
1023 simpl. destruct lev; simpl.
1024 rewrite flatten_commutes_with_HaskTAll.
1025 rewrite flatten_commutes_with_HaskTApp.
1026 eapply nd_comp; [ idtac | eapply nd_rule; eapply RAbsT ].
1028 set (mapOptionTree (flatten_leveled_type ) (mapOptionTree (weakLT(κ:=κ)) Σ)) as a.
1029 set (mapOptionTree (weakLT(κ:=κ)) (mapOptionTree (flatten_leveled_type ) Σ)) as q'.
1037 rewrite flatten_commutes_with_weakLT.
1048 apply (Prelude_error "found type abstraction at level >0; this is not supported").
1050 destruct case_RAppCo.
1051 simpl. destruct lev; simpl.
1052 unfold flatten_type.
1056 apply flatten_coercion.
1058 apply (Prelude_error "found coercion application at level >0; this is not supported").
1060 destruct case_RAbsCo.
1061 simpl. destruct lev; simpl.
1062 unfold flatten_type.
1064 apply (Prelude_error "AbsCo not supported (FIXME)").
1065 apply (Prelude_error "found coercion abstraction at level >0; this is not supported").
1067 destruct case_RLetRec.
1069 simpl. destruct lev; simpl.
1071 set (@RLetRec Γ Δ (mapOptionTree flatten_leveled_type lri) (flatten_type x) (mapOptionTree flatten_type y) nil) as q.
1072 replace (mapOptionTree flatten_leveled_type (y @@@ nil)) with (mapOptionTree flatten_type y @@@ nil).
1074 induction y; try destruct a; auto.
1079 apply (Prelude_error "LetRec not supported inside brackets yet (FIXME)").
1081 destruct case_RCase.
1083 apply (Prelude_error "Case not supported (BIG FIXME)").
1085 destruct case_SBrak.
1089 set (drop_lev (ec :: nil) (take_arg_types_as_tree t @@@ (ec :: nil))) as empty_tree.
1091 rewrite take_lemma'.
1093 rewrite mapOptionTree_compose.
1094 rewrite mapOptionTree_compose.
1095 rewrite unlev_relev.
1096 rewrite <- mapOptionTree_compose.
1099 set (mapOptionTree flatten_leveled_type (drop_lev (ec :: nil) succ)) as succ_host.
1100 set (mapOptionTree (flatten_type ○ unlev)(take_lev (ec :: nil) succ)) as succ_guest.
1101 set (mapOptionTree flatten_type (take_arg_types_as_tree t)) as succ_args.
1103 eapply nd_comp; [ eapply nd_rule; eapply RArrange; eapply ALeft; apply tree_of_nothing | idtac ].
1104 eapply nd_comp; [ eapply nd_rule; eapply RArrange; eapply ACanR | idtac ].
1105 refine (ga_unkappa Γ Δ (v2t ec) nil _ _ _ _ ;; _).
1106 eapply nd_comp; [ idtac | eapply arrange_brak ].
1112 apply (Prelude_error "found Brak at depth >0 indicating 3-level code; only two-level code is currently supported").
1118 unfold flatten_leveled_type at 2.
1121 rewrite mapOptionTree_compose.
1125 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ALeft; apply tree_of_nothing' ].
1126 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ACanR ].
1128 rewrite take_lemma'.
1129 rewrite unlev_relev.
1130 rewrite <- mapOptionTree_compose.
1131 eapply nd_comp; [ apply (arrange_esc _ _ ec) | idtac ].
1133 set (decide_tree_empty (take_lev (ec :: nil) succ)) as q'.
1139 set (mapOptionTree flatten_leveled_type (drop_lev (ec :: nil) succ)) as succ_host.
1140 set (mapOptionTree flatten_type (take_arg_types_as_tree t)) as succ_args.
1142 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply AuCanR ].
1143 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply AuCanR ].
1144 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply ACanL ].
1145 eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
1146 eapply nd_comp; [ apply nd_llecnac | idtac ].
1147 apply nd_prod; [ idtac | eapply boost ].
1150 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ACanL ].
1158 refine ( _ ;; (boost _ _ _ _ _ (postcompose _ _ _ _ _ _ _ _))).
1166 refine ( _ ;; (boost _ _ _ _ _ (postcompose _ _ _ _ _ _ _ _))).
1168 refine ( _ ;; (boost _ _ _ _ _ (postcompose _ _ _ _ _ _ _ _))).
1174 (* environment has non-empty leaves *)
1175 apply (Prelude_error "ga_kappa not supported yet (BIG FIXME)").
1177 (* nesting too deep *)
1178 apply (Prelude_error "found Esc at depth >0 indicating 3-level code; only two-level code is currently supported").
1181 Definition skolemize_and_flatten_proof :
1185 (mapOptionTree (flatten_judgment ○ skolemize_judgment) h)
1186 (mapOptionTree (flatten_judgment ○ skolemize_judgment) c).
1188 rewrite mapOptionTree_compose.
1189 rewrite mapOptionTree_compose.
1190 apply flatten_proof.
1191 apply skolemize_proof.
1196 (* to do: establish some metric on judgments (max length of level of any succedent type, probably), show how to
1197 * calculate it, and show that the flattening procedure above drives it down by one *)
1200 Instance FlatteningFunctor {Γ}{Δ}{ec} : Functor (JudgmentsL (PCF Γ Δ ec)) (TypesL (SystemFCa Γ Δ)) (obact) :=
1201 { fmor := FlatteningFunctor_fmor }.
1203 Definition ReificationFunctor Γ Δ : Functor (JudgmentsL _ _ (PCF n Γ Δ)) SystemFCa' (mapOptionTree brakifyJudg).
1204 refine {| fmor := ReificationFunctor_fmor Γ Δ |}; unfold hom; unfold ob; simpl ; intros.
1206 Definition PCF_SMME (n:nat)(Γ:TypeEnv)(Δ:CoercionEnv Γ) : ProgrammingLanguageSMME.
1207 refine {| plsmme_pl := PCF n Γ Δ |}.
1210 Definition SystemFCa_SMME (n:nat)(Γ:TypeEnv)(Δ:CoercionEnv Γ) : ProgrammingLanguageSMME.
1211 refine {| plsmme_pl := SystemFCa n Γ Δ |}.
1214 Definition ReificationFunctorMonoidal n : MonoidalFunctor (JudgmentsN n) (JudgmentsN (S n)) (ReificationFunctor n).
1218 Definition PCF_SystemFCa_two_level n Γ Δ : TwoLevelLanguage (PCF_SMME n Γ Δ) (SystemFCa_SMME (S n) Γ Δ).
1221 (* ... and the retraction exists *)
1225 Implicit Arguments garrow [ ].