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 Lemma drop_lev_lemma' : forall Γ (lev:HaskLevel Γ) x, drop_lev lev (x @@@ lev) = [].
139 destruct a; simpl; try reflexivity.
140 apply drop_lev_lemma.
142 change (@drop_lev _ lev (x1 @@@ lev ,, x2 @@@ lev))
143 with ((@drop_lev _ lev (x1 @@@ lev)) ,, (@drop_lev _ lev (x2 @@@ lev))).
150 Ltac drop_simplify :=
152 | [ |- context[@drop_lev ?G ?L [ ?X @@ ?L ] ] ] =>
153 rewrite (drop_lev_lemma G L X)
155 | [ |- context[@drop_lev ?G ?L [ ?X @@@ ?L ] ] ] =>
156 rewrite (drop_lev_lemma' G L X)
158 | [ |- context[@drop_lev ?G (?E :: ?L) [ ?X @@ (?E :: ?L) ] ] ] =>
159 rewrite (drop_lev_lemma_s G L E X)
160 | [ |- context[@drop_lev ?G ?N (?A,,?B)] ] =>
161 change (@drop_lev G N (A,,B)) with ((@drop_lev G N A),,(@drop_lev G N B))
162 | [ |- context[@drop_lev ?G ?N (T_Leaf None)] ] =>
163 change (@drop_lev G N (T_Leaf (@None (LeveledHaskType G ★)))) with (T_Leaf (@None (LeveledHaskType G ★)))
166 Ltac take_simplify :=
168 | [ |- context[@take_lev ?G ?L [ ?X @@ ?L ] ] ] =>
169 rewrite (take_lemma G L X)
170 | [ |- context[@take_lev ?G ?L [ ?X @@@ ?L ] ] ] =>
171 rewrite (take_lemma' G L X)
172 | [ |- context[@take_lev ?G ?N (?A,,?B)] ] =>
173 change (@take_lev G N (A,,B)) with ((@take_lev G N A),,(@take_lev G N B))
174 | [ |- context[@take_lev ?G ?N (T_Leaf None)] ] =>
175 change (@take_lev G N (T_Leaf (@None (LeveledHaskType G ★)))) with (T_Leaf (@None (LeveledHaskType G ★)))
179 (*******************************************************************************)
182 Context (hetmet_flatten : WeakExprVar).
183 Context (hetmet_unflatten : WeakExprVar).
184 Context (hetmet_id : WeakExprVar).
185 Context {unitTy : forall TV, RawHaskType TV ECKind -> RawHaskType TV ★ }.
186 Context {prodTy : forall TV, RawHaskType TV ECKind -> RawHaskType TV ★ -> RawHaskType TV ★ -> RawHaskType TV ★ }.
187 Context {gaTy : forall TV, RawHaskType TV ECKind -> RawHaskType TV ★ -> RawHaskType TV ★ -> RawHaskType TV ★ }.
189 Definition ga_mk_tree' {TV}(ec:RawHaskType TV ECKind)(tr:Tree ??(RawHaskType TV ★)) : RawHaskType TV ★ :=
190 reduceTree (unitTy TV ec) (prodTy TV ec) tr.
192 Definition ga_mk_tree {Γ}(ec:HaskType Γ ECKind)(tr:Tree ??(HaskType Γ ★)) : HaskType Γ ★ :=
193 fun TV ite => ga_mk_tree' (ec TV ite) (mapOptionTree (fun x => x TV ite) tr).
195 Definition ga_mk_raw {TV}(ec:RawHaskType TV ECKind)(ant suc:Tree ??(RawHaskType TV ★)) : RawHaskType TV ★ :=
198 (ga_mk_tree' ec suc).
200 Definition ga_mk {Γ}(ec:HaskType Γ ECKind)(ant suc:Tree ??(HaskType Γ ★)) : HaskType Γ ★ :=
201 fun TV ite => gaTy TV (ec TV ite) (ga_mk_tree ec ant TV ite) (ga_mk_tree ec suc TV ite).
205 * - code types <[t]>@c become garrows c () t
206 * - free variables of type t at a level lev deeper than the succedent become garrows c () t
207 * - free variables at the level of the succedent become
209 Fixpoint flatten_rawtype {TV}{κ}(exp: RawHaskType TV κ) : RawHaskType TV κ :=
212 | TAll _ y => TAll _ (fun v => flatten_rawtype (y v))
213 | TApp _ _ x y => TApp (flatten_rawtype x) (flatten_rawtype y)
215 | TCoerc _ t1 t2 t => TCoerc (flatten_rawtype t1) (flatten_rawtype t2) (flatten_rawtype t)
217 | TCode ec e => let e' := flatten_rawtype e
218 in ga_mk_raw ec (unleaves_ (take_arg_types e')) [drop_arg_types e']
219 | TyFunApp tfc kl k lt => TyFunApp tfc kl k (flatten_rawtype_list _ lt)
221 with flatten_rawtype_list {TV}(lk:list Kind)(exp:@RawHaskTypeList TV lk) : @RawHaskTypeList TV lk :=
222 match exp in @RawHaskTypeList _ LK return @RawHaskTypeList TV LK with
223 | TyFunApp_nil => TyFunApp_nil
224 | TyFunApp_cons κ kl t rest => TyFunApp_cons _ _ (flatten_rawtype t) (flatten_rawtype_list _ rest)
227 Definition flatten_type {Γ}{κ}(ht:HaskType Γ κ) : HaskType Γ κ :=
228 fun TV ite => flatten_rawtype (ht TV ite).
230 Fixpoint levels_to_tcode {Γ}(ht:HaskType Γ ★)(lev:HaskLevel Γ) : HaskType Γ ★ :=
232 | nil => flatten_type ht
233 | ec::lev' => @ga_mk _ (v2t ec) [] [levels_to_tcode ht lev']
236 Definition flatten_leveled_type {Γ}(ht:LeveledHaskType Γ ★) : LeveledHaskType Γ ★ :=
237 levels_to_tcode (unlev ht) (getlev ht) @@ nil.
241 Axiom literal_types_unchanged : forall Γ l, flatten_type (literalType l) = literalType(Γ:=Γ) l.
243 Axiom flatten_coercion : forall Γ Δ κ (σ τ:HaskType Γ κ) (γ:HaskCoercion Γ Δ (σ ∼∼∼ τ)),
244 HaskCoercion Γ Δ (flatten_type σ ∼∼∼ flatten_type τ).
246 Axiom flatten_commutes_with_substT :
247 forall κ Γ (Δ:CoercionEnv Γ) (σ:∀ TV, InstantiatedTypeEnv TV Γ → TV κ → RawHaskType TV ★) (τ:HaskType Γ κ),
248 flatten_type (substT σ τ) = substT (fun TV ite v => flatten_rawtype (σ TV ite v))
251 Axiom flatten_commutes_with_HaskTAll :
252 forall κ Γ (Δ:CoercionEnv Γ) (σ:∀ TV, InstantiatedTypeEnv TV Γ → TV κ → RawHaskType TV ★),
253 flatten_type (HaskTAll κ σ) = HaskTAll κ (fun TV ite v => flatten_rawtype (σ TV ite v)).
255 Axiom flatten_commutes_with_HaskTApp :
256 forall κ Γ (Δ:CoercionEnv Γ) (σ:∀ TV, InstantiatedTypeEnv TV Γ → TV κ → RawHaskType TV ★),
257 flatten_type (HaskTApp (weakF σ) (FreshHaskTyVar κ)) =
258 HaskTApp (weakF (fun TV ite v => flatten_rawtype (σ TV ite v))) (FreshHaskTyVar κ).
260 Axiom flatten_commutes_with_weakLT : forall (Γ:TypeEnv) κ t,
261 flatten_leveled_type (weakLT(Γ:=Γ)(κ:=κ) t) = weakLT(Γ:=Γ)(κ:=κ) (flatten_leveled_type t).
263 Axiom globals_do_not_have_code_types : forall (Γ:TypeEnv) (g:Global Γ) v,
264 flatten_type (g v) = g v.
266 (* "n" is the maximum depth remaining AFTER flattening *)
267 Definition flatten_judgment (j:Judg) :=
268 match j as J return Judg with
269 | Γ > Δ > ant |- suc @ nil => Γ > Δ > mapOptionTree flatten_leveled_type ant
270 |- mapOptionTree flatten_type suc @ nil
271 | Γ > Δ > ant |- suc @ (ec::lev') => Γ > Δ > mapOptionTree flatten_leveled_type (drop_lev (ec::lev') ant)
273 (mapOptionTree (flatten_type ○ unlev) (take_lev (ec::lev') ant))
274 (mapOptionTree flatten_type suc )
279 { ga_id : ∀ Γ Δ ec l a , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec a a ]@l ]
280 ; ga_cancelr : ∀ Γ Δ ec l a , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec (a,,[]) a ]@l ]
281 ; ga_cancell : ∀ Γ Δ ec l a , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec ([],,a) a ]@l ]
282 ; ga_uncancelr : ∀ Γ Δ ec l a , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec a (a,,[]) ]@l ]
283 ; ga_uncancell : ∀ Γ Δ ec l a , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec a ([],,a) ]@l ]
284 ; ga_assoc : ∀ Γ Δ ec l a b c, ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec ((a,,b),,c) (a,,(b,,c)) ]@l ]
285 ; ga_unassoc : ∀ Γ Δ ec l a b c, ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec (a,,(b,,c)) ((a,,b),,c) ]@l ]
286 ; ga_swap : ∀ Γ Δ ec l a b , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec (a,,b) (b,,a) ]@l ]
287 ; ga_drop : ∀ Γ Δ ec l a , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec a [] ]@l ]
288 ; ga_copy : ∀ Γ Δ ec l a , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec a (a,,a) ]@l ]
289 ; ga_first : ∀ Γ Δ ec l a b x, ND Rule [] [Γ > Δ > [@ga_mk Γ ec a b @@l] |- [@ga_mk Γ ec (a,,x) (b,,x) ]@l ]
290 ; ga_second : ∀ Γ Δ ec l a b x, ND Rule [] [Γ > Δ > [@ga_mk Γ ec a b @@l] |- [@ga_mk Γ ec (x,,a) (x,,b) ]@l ]
291 ; ga_lit : ∀ Γ Δ ec l lit , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec [] [literalType lit] ]@l ]
292 ; ga_curry : ∀ Γ Δ ec l a b c, ND Rule [] [Γ > Δ > [@ga_mk Γ ec (a,,[b]) [c] @@ l] |- [@ga_mk Γ ec a [b ---> c] ]@ l ]
293 ; 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 ]
294 ; ga_apply : ∀ Γ Δ ec l a a' b c,
295 ND Rule [] [Γ > Δ > [@ga_mk Γ ec a [b ---> c] @@ l],,[@ga_mk Γ ec a' [b] @@ l] |- [@ga_mk Γ ec (a,,a') [c] ]@l ]
296 ; ga_kappa : ∀ Γ Δ ec l a b Σ, ND Rule
297 [Γ > Δ > Σ,,[@ga_mk Γ ec [] a @@ l] |- [@ga_mk Γ ec [] b ]@l ]
298 [Γ > Δ > Σ |- [@ga_mk Γ ec a b ]@l ]
300 Context `(gar:garrow).
302 Notation "a ~~~~> b" := (@ga_mk _ _ a b) (at level 20).
304 Definition boost : forall Γ Δ ant x y {lev},
305 ND Rule [] [ Γ > Δ > [x@@lev] |- [y]@lev ] ->
306 ND Rule [ Γ > Δ > ant |- [x]@lev ] [ Γ > Δ > ant |- [y]@lev ].
308 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanR ].
309 eapply nd_comp; [ idtac | eapply nd_rule; apply RLet ].
310 eapply nd_comp; [ apply nd_rlecnac | idtac ].
320 Definition precompose Γ Δ ec : forall a x y z lev,
322 [ Γ > Δ > a |- [@ga_mk _ ec y z ]@lev ]
323 [ Γ > Δ > a,,[@ga_mk _ ec x y @@ lev] |- [@ga_mk _ ec x z ]@lev ].
325 eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
326 eapply nd_comp; [ apply nd_rlecnac | idtac ].
329 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RExch ].
333 Definition precompose' Γ Δ ec : forall a b x y z lev,
335 [ Γ > Δ > a,,b |- [@ga_mk _ ec y z ]@lev ]
336 [ Γ > Δ > a,,([@ga_mk _ ec x y @@ lev],,b) |- [@ga_mk _ ec x z ]@lev ].
338 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RLeft; eapply RExch ].
339 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCossa ].
343 Definition postcompose_ Γ Δ ec : forall a x y z lev,
345 [ Γ > Δ > a |- [@ga_mk _ ec x y ]@lev ]
346 [ Γ > Δ > a,,[@ga_mk _ ec y z @@ lev] |- [@ga_mk _ ec x z ]@lev ].
348 eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
349 eapply nd_comp; [ apply nd_rlecnac | idtac ].
355 Definition postcompose Γ Δ ec : forall x y z lev,
356 ND Rule [] [ Γ > Δ > [] |- [@ga_mk _ ec x y ]@lev ] ->
357 ND Rule [] [ Γ > Δ > [@ga_mk _ ec y z @@ lev] |- [@ga_mk _ ec x z ]@lev ].
359 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanL ].
360 eapply nd_comp; [ idtac | eapply postcompose_ ].
364 Definition first_nd : ∀ Γ Δ ec lev a b c Σ,
365 ND Rule [ Γ > Δ > Σ |- [@ga_mk Γ ec a b ]@lev ]
366 [ Γ > Δ > Σ |- [@ga_mk Γ ec (a,,c) (b,,c) ]@lev ].
368 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanR ].
369 eapply nd_comp; [ idtac | eapply nd_rule; apply RLet ].
370 eapply nd_comp; [ apply nd_rlecnac | idtac ].
373 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RuCanR ].
377 Definition firstify : ∀ Γ Δ ec lev a b c Σ,
378 ND Rule [] [ Γ > Δ > Σ |- [@ga_mk Γ ec a b ]@lev ] ->
379 ND Rule [] [ Γ > Δ > Σ |- [@ga_mk Γ ec (a,,c) (b,,c) ]@lev ].
386 Definition second_nd : ∀ Γ Δ ec lev a b c Σ,
388 [ Γ > Δ > Σ |- [@ga_mk Γ ec a b ]@lev ]
389 [ Γ > Δ > Σ |- [@ga_mk Γ ec (c,,a) (c,,b) ]@lev ].
391 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanR ].
392 eapply nd_comp; [ idtac | eapply nd_rule; apply RLet ].
393 eapply nd_comp; [ apply nd_rlecnac | idtac ].
396 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RuCanR ].
400 Definition secondify : ∀ Γ Δ ec lev a b c Σ,
401 ND Rule [] [ Γ > Δ > Σ |- [@ga_mk Γ ec a b ]@lev ] ->
402 ND Rule [] [ Γ > Δ > Σ |- [@ga_mk Γ ec (c,,a) (c,,b) ]@lev ].
409 Lemma ga_unkappa : ∀ Γ Δ ec l a b Σ x,
411 [Γ > Δ > Σ |- [@ga_mk Γ ec (a,,x) b ]@l ]
412 [Γ > Δ > Σ,,[@ga_mk Γ ec [] a @@ l] |- [@ga_mk Γ ec x b ]@l ].
414 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RExch ].
415 eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
416 eapply nd_comp; [ apply nd_llecnac | idtac ].
420 eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
421 eapply nd_comp; [ apply nd_llecnac | idtac ].
425 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RExch ].
429 (* useful for cutting down on the pretty-printed noise
431 Notation "` x" := (take_lev _ x) (at level 20).
432 Notation "`` x" := (mapOptionTree unlev x) (at level 20).
433 Notation "``` x" := (drop_lev _ x) (at level 20).
435 Definition flatten_arrangement' :
436 forall Γ (Δ:CoercionEnv Γ)
437 (ec:HaskTyVar Γ ECKind) (lev:HaskLevel Γ) (ant1 ant2:Tree ??(LeveledHaskType Γ ★)) (r:Arrange ant1 ant2),
438 ND Rule [] [Γ > Δ > [] |- [@ga_mk _ (v2t ec) (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) ant2))
439 (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) ant1)) ]@nil ].
442 refine (fix flatten ant1 ant2 (r:Arrange ant1 ant2):
443 ND Rule [] [Γ > Δ > [] |- [@ga_mk _ (v2t ec)
444 (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) ant2))
445 (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) ant1)) ]@nil] :=
446 match r as R in Arrange A B return
447 ND Rule [] [Γ > Δ > [] |- [@ga_mk _ (v2t ec)
448 (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) B))
449 (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) A)) ]@nil]
451 | RId a => let case_RId := tt in ga_id _ _ _ _ _
452 | RCanL a => let case_RCanL := tt in ga_uncancell _ _ _ _ _
453 | RCanR a => let case_RCanR := tt in ga_uncancelr _ _ _ _ _
454 | RuCanL a => let case_RuCanL := tt in ga_cancell _ _ _ _ _
455 | RuCanR a => let case_RuCanR := tt in ga_cancelr _ _ _ _ _
456 | RAssoc a b c => let case_RAssoc := tt in ga_assoc _ _ _ _ _ _ _
457 | RCossa a b c => let case_RCossa := tt in ga_unassoc _ _ _ _ _ _ _
458 | RExch a b => let case_RExch := tt in ga_swap _ _ _ _ _ _
459 | RWeak a => let case_RWeak := tt in ga_drop _ _ _ _ _
460 | RCont a => let case_RCont := tt in ga_copy _ _ _ _ _
461 | RLeft a b c r' => let case_RLeft := tt in flatten _ _ r' ;; boost _ _ _ _ _ (ga_second _ _ _ _ _ _ _)
462 | RRight a b c r' => let case_RRight := tt in flatten _ _ r' ;; boost _ _ _ _ _ (ga_first _ _ _ _ _ _ _)
463 | RComp c b a r1 r2 => let case_RComp := tt in (fun r1' r2' => _) (flatten _ _ r1) (flatten _ _ r2)
464 end); clear flatten; repeat take_simplify; repeat drop_simplify; intros.
467 set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) a)) as a' in *.
468 set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) b)) as b' in *.
469 set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) c)) as c' in *.
470 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RCanL ].
471 eapply nd_comp; [ idtac | eapply nd_rule; apply
472 (@RLet Γ Δ [] [] (@ga_mk _ (v2t ec) a' b') (@ga_mk _ (v2t ec) a' c')) ].
473 eapply nd_comp; [ apply nd_llecnac | idtac ].
476 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RuCanR ].
477 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RCanL ].
478 eapply nd_comp; [ idtac | eapply nd_rule; apply RLet ].
479 eapply nd_comp; [ apply nd_llecnac | idtac ].
482 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RExch ].
486 Definition flatten_arrangement :
487 forall Γ (Δ:CoercionEnv Γ) n
488 (ec:HaskTyVar Γ ECKind) (lev:HaskLevel Γ) (ant1 ant2:Tree ??(LeveledHaskType Γ ★)) (r:Arrange ant1 ant2) succ,
490 [Γ > Δ > mapOptionTree (flatten_leveled_type ) (drop_lev n ant1)
491 |- [@ga_mk _ (v2t ec)
492 (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) ant1))
493 (mapOptionTree (flatten_type ) succ) ]@nil]
494 [Γ > Δ > mapOptionTree (flatten_leveled_type ) (drop_lev n ant2)
495 |- [@ga_mk _ (v2t ec)
496 (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) ant2))
497 (mapOptionTree (flatten_type ) succ) ]@nil].
499 refine ( _ ;; (boost _ _ _ _ _ (postcompose _ _ _ _ _ _ _ (flatten_arrangement' Γ Δ ec lev ant1 ant2 r)))).
502 refine ((fix flatten ant1 ant2 (r:Arrange ant1 ant2) :=
503 match r as R in Arrange A B return
504 Arrange (mapOptionTree (flatten_leveled_type ) (drop_lev _ A))
505 (mapOptionTree (flatten_leveled_type ) (drop_lev _ B)) with
506 | RId a => let case_RId := tt in RId _
507 | RCanL a => let case_RCanL := tt in RCanL _
508 | RCanR a => let case_RCanR := tt in RCanR _
509 | RuCanL a => let case_RuCanL := tt in RuCanL _
510 | RuCanR a => let case_RuCanR := tt in RuCanR _
511 | RAssoc a b c => let case_RAssoc := tt in RAssoc _ _ _
512 | RCossa a b c => let case_RCossa := tt in RCossa _ _ _
513 | RExch a b => let case_RExch := tt in RExch _ _
514 | RWeak a => let case_RWeak := tt in RWeak _
515 | RCont a => let case_RCont := tt in RCont _
516 | RLeft a b c r' => let case_RLeft := tt in RLeft _ (flatten _ _ r')
517 | RRight a b c r' => let case_RRight := tt in RRight _ (flatten _ _ r')
518 | RComp a b c r1 r2 => let case_RComp := tt in RComp (flatten _ _ r1) (flatten _ _ r2)
519 end) ant1 ant2 r); clear flatten; repeat take_simplify; repeat drop_simplify; intros.
522 Definition flatten_arrangement'' :
523 forall Γ Δ ant1 ant2 succ l (r:Arrange ant1 ant2),
524 ND Rule (mapOptionTree (flatten_judgment ) [Γ > Δ > ant1 |- succ @ l])
525 (mapOptionTree (flatten_judgment ) [Γ > Δ > ant2 |- succ @ l]).
539 apply RExch. (* TO DO: check for all-leaf trees here *)
544 eapply RComp; [ apply IHr1 | apply IHr2 ].
546 apply flatten_arrangement.
550 Definition ga_join Γ Δ Σ₁ Σ₂ a b ec :
551 ND Rule [] [Γ > Δ > Σ₁ |- [@ga_mk _ ec [] a ]@nil] ->
552 ND Rule [] [Γ > Δ > Σ₂ |- [@ga_mk _ ec [] b ]@nil] ->
553 ND Rule [] [Γ > Δ > Σ₁,,Σ₂ |- [@ga_mk _ ec [] (a,,b) ]@nil].
556 apply secondify with (c:=a) in pfb.
557 apply firstify with (c:=[]) in pfa.
558 eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
559 eapply nd_comp; [ eapply nd_llecnac | idtac ].
564 eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
565 eapply nd_comp; [ apply nd_llecnac | idtac ].
567 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanL ].
568 eapply nd_comp; [ idtac | eapply postcompose_ ].
571 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RExch ].
572 eapply nd_comp; [ idtac | eapply precompose ].
576 Definition arrange_brak : forall Γ Δ ec succ t,
579 [(@ga_mk _ (v2t ec) [] (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: nil) succ))) @@ nil],,
580 mapOptionTree (flatten_leveled_type ) (drop_lev (ec :: nil) succ) |- [t]@nil]
581 [Γ > Δ > mapOptionTree (flatten_leveled_type ) succ |- [t]@nil].
585 set (@arrange' _ succ (levelMatch (ec::nil))) as q.
586 set (arrangeMap _ _ flatten_leveled_type q) as y.
594 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RExch ].
596 eapply nd_comp; [ apply nd_llecnac | idtac ].
597 eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
602 induction succ; try destruct a; simpl.
608 destruct l as [t' lev'].
609 destruct lev' as [|ec' lev'].
613 set (@eqd_dec (HaskLevel Γ) (haskLevelEqDecidable Γ) (ec' :: lev') (ec :: nil)) as q.
618 unfold flatten_leveled_type.
635 Definition arrange_empty_tree : forall {T}{A}(q:Tree A)(t:Tree ??T),
636 t = mapTree (fun _:A => None) q ->
644 destruct t; try destruct o; inversion H.
645 set (IHq1 _ H1) as x1.
646 set (IHq2 _ H2) as x2.
657 (* Definition unarrange_empty_tree : forall {T}{A}(t:Tree ??T)(q:Tree A),
658 t = mapTree (fun _:A => None) q ->
662 Definition decide_tree_empty : forall {T:Type}(t:Tree ??T),
663 sum { q:Tree unit & t = mapTree (fun _ => None) q } unit.
668 | T_Branch b1 b2 => let b1' := foo b1 in let b2' := foo b2 in _
688 Definition arrange_esc : forall Γ Δ ec succ t,
690 [Γ > Δ > mapOptionTree (flatten_leveled_type ) succ |- [t]@nil]
692 [(@ga_mk _ (v2t ec) [] (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: nil) succ))) @@ nil],,
693 mapOptionTree (flatten_leveled_type ) (drop_lev (ec :: nil) succ) |- [t]@nil].
695 set (@arrange _ succ (levelMatch (ec::nil))) as q.
696 set (@drop_lev Γ (ec::nil) succ) as q'.
697 assert (@drop_lev Γ (ec::nil) succ=q') as H.
699 unfold drop_lev in H.
700 unfold mkDropFlags in H.
703 set (arrangeMap _ _ flatten_leveled_type q) as y.
710 set (mapOptionTree flatten_leveled_type (dropT (mkFlags (liftBoolFunc false (bnot ○ levelMatch (ec :: nil))) succ))) as q.
711 destruct (decide_tree_empty q); [ idtac | apply (Prelude_error "escapifying open code not yet supported") ].
715 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RExch ].
716 set (fun z z' => @RLet Γ Δ z (mapOptionTree flatten_leveled_type q') t z' nil) as q''.
717 eapply nd_comp; [ idtac | eapply nd_rule; apply RLet ].
719 eapply nd_comp; [ apply nd_rlecnac | idtac ].
723 eapply RComp; [ idtac | apply RCanR ].
725 apply (@arrange_empty_tree _ _ _ _ e).
729 eapply (@RVar Γ Δ t nil).
737 eapply decide_tree_empty.
740 set (dropT (mkFlags (liftBoolFunc false (bnot ○ levelMatch (ec :: nil))) succ)) as escapified.
741 destruct (decide_tree_empty escapified).
748 unfold mkDropFlags; simpl.
752 destruct (General.list_eq_dec h0 (ec :: nil)).
768 apply (Prelude_error "escapifying code with multi-leaf antecedents is not supported").
772 Lemma mapOptionTree_distributes
773 : forall T R (a b:Tree ??T) (f:T->R),
774 mapOptionTree f (a,,b) = (mapOptionTree f a),,(mapOptionTree f b).
778 Lemma unlev_relev : forall {Γ}(t:Tree ??(HaskType Γ ★)) lev, mapOptionTree unlev (t @@@ lev) = t.
781 destruct a; reflexivity.
782 rewrite <- IHt1 at 2.
783 rewrite <- IHt2 at 2.
787 Lemma tree_of_nothing : forall Γ ec t,
788 Arrange (mapOptionTree flatten_leveled_type (drop_lev(Γ:=Γ) (ec :: nil) (t @@@ (ec :: nil)))) [].
790 induction t; try destruct o; try destruct a.
797 eapply RComp; [ idtac | apply RCanL ].
798 eapply RComp; [ idtac | eapply RLeft; apply IHt2 ].
801 Transparent drop_lev.
808 Lemma tree_of_nothing' : forall Γ ec t,
809 Arrange [] (mapOptionTree flatten_leveled_type (drop_lev(Γ:=Γ) (ec :: nil) (t @@@ (ec :: nil)))).
811 induction t; try destruct o; try destruct a.
818 eapply RComp; [ apply RuCanL | idtac ].
819 eapply RComp; [ eapply RRight; apply IHt1 | idtac ].
822 Transparent drop_lev.
829 Lemma krunk : forall Γ (ec:HaskTyVar Γ ECKind) t,
830 flatten_type (<[ ec |- t ]>)
832 (mapOptionTree flatten_type (take_arg_types_as_tree t))
833 [ flatten_type (drop_arg_types_as_tree t)].
835 unfold flatten_type at 1.
838 apply phoas_extensionality.
843 rewrite <- mapOptionTree_compose.
844 unfold take_arg_types_as_tree.
846 replace (flatten_type (drop_arg_types_as_tree t) tv ite)
847 with (drop_arg_types (flatten_rawtype (t tv ite))).
848 replace (unleaves_ (take_arg_types (flatten_rawtype (t tv ite))))
849 with ((mapOptionTree (fun x : HaskType Γ ★ => flatten_type x tv ite)
851 (take_trustme (count_arg_types (t (fun _ : Kind => unit) (ite_unit Γ)))
852 (fun TV : Kind → Type => take_arg_types ○ t TV))))).
855 clear hetmet_flatten.
856 clear hetmet_unflatten.
864 Definition flatten_proof :
867 ND Rule (mapOptionTree (flatten_judgment ) h) (mapOptionTree (flatten_judgment ) c).
869 eapply nd_map'; [ idtac | apply X ].
875 (match X as R in SRule H C with
876 | SBrak Γ Δ t ec succ lev => let case_SBrak := tt in _
877 | SEsc Γ Δ t ec succ lev => let case_SEsc := tt in _
878 | SFlat h c r => let case_SFlat := tt in _
882 refine (match r as R in Rule H C with
883 | RArrange Γ Δ a b x l d => let case_RArrange := tt in _
884 | RNote Γ Δ Σ τ l n => let case_RNote := tt in _
885 | RLit Γ Δ l _ => let case_RLit := tt in _
886 | RVar Γ Δ σ lev => let case_RVar := tt in _
887 | RGlobal Γ Δ σ l wev => let case_RGlobal := tt in _
888 | RLam Γ Δ Σ tx te lev => let case_RLam := tt in _
889 | RCast Γ Δ Σ σ τ lev γ => let case_RCast := tt in _
890 | RAbsT Γ Δ Σ κ σ lev => let case_RAbsT := tt in _
891 | RAppT Γ Δ Σ κ σ τ lev => let case_RAppT := tt in _
892 | RAppCo Γ Δ Σ κ σ₁ σ₂ γ σ lev => let case_RAppCo := tt in _
893 | RAbsCo Γ Δ Σ κ σ σ₁ σ₂ lev => let case_RAbsCo := tt in _
894 | RApp Γ Δ Σ₁ Σ₂ tx te lev => let case_RApp := tt in _
895 | RLet Γ Δ Σ₁ Σ₂ σ₁ σ₂ lev => let case_RLet := tt in _
896 | RWhere Γ Δ Σ₁ Σ₂ Σ₃ σ₁ σ₂ lev => let case_RWhere := tt in _
897 | RJoin Γ p lri m x q l => let case_RJoin := tt in _
898 | RVoid _ _ l => let case_RVoid := tt in _
899 | RBrak Γ Δ t ec succ lev => let case_RBrak := tt in _
900 | REsc Γ Δ t ec succ lev => let case_REsc := tt in _
901 | RCase Γ Δ lev tc Σ avars tbranches alts => let case_RCase := tt in _
902 | RLetRec Γ Δ lri x y t => let case_RLetRec := tt in _
905 destruct case_RArrange.
906 apply (flatten_arrangement'' Γ Δ a b x _ d).
909 apply (Prelude_error "found unskolemized Brak rule; this shouldn't happen").
912 apply (Prelude_error "found unskolemized Esc rule; this shouldn't happen").
917 apply nd_rule; apply RNote; auto.
918 apply nd_rule; apply RNote; auto.
923 unfold flatten_leveled_type.
925 rewrite literal_types_unchanged.
926 apply nd_rule; apply RLit.
927 unfold take_lev; simpl.
928 unfold drop_lev; simpl.
930 rewrite literal_types_unchanged.
934 Opaque flatten_judgment.
936 Transparent flatten_judgment.
938 unfold flatten_judgment.
940 apply nd_rule. apply RVar.
941 repeat drop_simplify.
942 repeat take_simplify.
946 destruct case_RGlobal.
950 destruct l as [|ec lev]; simpl.
951 destruct (eqd_dec (g:CoreVar) (hetmet_flatten:CoreVar)).
952 set (flatten_type (g wev)) as t.
953 set (RGlobal _ Δ nil (mkGlobal Γ t hetmet_id)) as q.
958 destruct (eqd_dec (g:CoreVar) (hetmet_unflatten:CoreVar)).
959 set (flatten_type (g wev)) as t.
960 set (RGlobal _ Δ nil (mkGlobal Γ t hetmet_id)) as q.
965 unfold flatten_leveled_type. simpl.
966 apply nd_rule; rewrite globals_do_not_have_code_types.
968 apply (Prelude_error "found RGlobal at depth >0; globals should never appear inside code brackets unless escaped").
974 destruct lev as [|ec lev]; simpl; [ apply nd_rule; apply RLam; auto | idtac ].
975 repeat drop_simplify.
976 repeat take_simplify.
988 destruct lev as [|ec lev]; simpl; [ apply nd_rule; apply RCast; auto | idtac ].
990 apply flatten_coercion; auto.
991 apply (Prelude_error "RCast at level >0; casting inside of code brackets is currently not supported").
996 [ apply nd_rule; apply RJoin | idtac ];
997 apply (Prelude_error "RJoin at depth >0").
1002 destruct lev as [|ec lev].
1003 unfold flatten_type at 1.
1008 repeat drop_simplify.
1009 repeat take_simplify.
1010 rewrite mapOptionTree_distributes.
1011 set (mapOptionTree (flatten_leveled_type ) (drop_lev (ec :: lev) Σ₁)) as Σ₁'.
1012 set (mapOptionTree (flatten_leveled_type ) (drop_lev (ec :: lev) Σ₂)) as Σ₂'.
1013 set (take_lev (ec :: lev) Σ₁) as Σ₁''.
1014 set (take_lev (ec :: lev) Σ₂) as Σ₂''.
1015 replace (flatten_type (tx ---> te)) with ((flatten_type tx) ---> (flatten_type te)).
1016 apply (Prelude_error "FIXME: ga_apply").
1020 Notation "` x" := (take_lev _ x).
1021 Notation "`` x" := (mapOptionTree unlev x) (at level 20).
1022 Notation "``` x" := ((drop_lev _ x)) (at level 20).
1023 Notation "!<[]> x" := (flatten_type _ x) (at level 1).
1024 Notation "!<[@]> x" := (mapOptionTree flatten_leveled_type x) (at level 1).
1029 destruct lev as [|ec lev]; simpl; [ apply nd_rule; apply RLet; auto | idtac ].
1030 repeat drop_simplify.
1031 repeat take_simplify.
1034 set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) Σ₁)) as Σ₁'.
1035 set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) Σ₂)) as Σ₂'.
1036 set (mapOptionTree flatten_leveled_type (drop_lev (ec :: lev) Σ₁)) as Σ₁''.
1037 set (mapOptionTree flatten_leveled_type (drop_lev (ec :: lev) Σ₂)) as Σ₂''.
1040 eapply nd_prod; [ idtac | apply nd_id ].
1042 apply (ga_first _ _ _ _ _ _ Σ₂').
1044 eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
1047 eapply nd_comp; [ eapply nd_rule; eapply RArrange; eapply RCanL | idtac ].
1048 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RExch (* okay *)].
1051 destruct case_RWhere.
1053 destruct lev as [|ec lev]; simpl; [ apply nd_rule; apply RWhere; auto | idtac ].
1054 repeat take_simplify.
1055 repeat drop_simplify.
1058 set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) Σ₁)) as Σ₁'.
1059 set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) Σ₂)) as Σ₂'.
1060 set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) Σ₃)) as Σ₃'.
1061 set (mapOptionTree flatten_leveled_type (drop_lev (ec :: lev) Σ₁)) as Σ₁''.
1062 set (mapOptionTree flatten_leveled_type (drop_lev (ec :: lev) Σ₂)) as Σ₂''.
1063 set (mapOptionTree flatten_leveled_type (drop_lev (ec :: lev) Σ₃)) as Σ₃''.
1066 eapply nd_prod; [ eapply nd_id | idtac ].
1067 eapply (first_nd _ _ _ _ _ _ Σ₃').
1069 eapply nd_prod; [ eapply nd_id | idtac ].
1070 eapply (second_nd _ _ _ _ _ _ Σ₁').
1072 eapply nd_comp; [ idtac | eapply nd_rule; eapply RWhere ].
1073 apply nd_prod; [ idtac | apply nd_id ].
1074 eapply nd_comp; [ idtac | eapply precompose' ].
1080 destruct case_RVoid.
1085 apply (Prelude_error "RVoid at level >0").
1087 destruct case_RAppT.
1088 simpl. destruct lev; simpl.
1089 unfold flatten_leveled_type.
1091 rewrite flatten_commutes_with_HaskTAll.
1092 rewrite flatten_commutes_with_substT.
1097 apply (Prelude_error "found type application at level >0; this is not supported").
1099 destruct case_RAbsT.
1100 simpl. destruct lev; simpl.
1101 rewrite flatten_commutes_with_HaskTAll.
1102 rewrite flatten_commutes_with_HaskTApp.
1103 eapply nd_comp; [ idtac | eapply nd_rule; eapply RAbsT ].
1105 set (mapOptionTree (flatten_leveled_type ) (mapOptionTree (weakLT(κ:=κ)) Σ)) as a.
1106 set (mapOptionTree (weakLT(κ:=κ)) (mapOptionTree (flatten_leveled_type ) Σ)) as q'.
1114 rewrite flatten_commutes_with_weakLT.
1125 apply (Prelude_error "found type abstraction at level >0; this is not supported").
1127 destruct case_RAppCo.
1128 simpl. destruct lev; simpl.
1129 unfold flatten_type.
1133 apply flatten_coercion.
1135 apply (Prelude_error "found coercion application at level >0; this is not supported").
1137 destruct case_RAbsCo.
1138 simpl. destruct lev; simpl.
1139 unfold flatten_type.
1141 apply (Prelude_error "AbsCo not supported (FIXME)").
1142 apply (Prelude_error "found coercion abstraction at level >0; this is not supported").
1144 destruct case_RLetRec.
1146 simpl. destruct lev; simpl.
1148 set (@RLetRec Γ Δ (mapOptionTree flatten_leveled_type lri) (flatten_type x) (mapOptionTree flatten_type y) nil) as q.
1149 replace (mapOptionTree flatten_leveled_type (y @@@ nil)) with (mapOptionTree flatten_type y @@@ nil).
1151 induction y; try destruct a; auto.
1156 apply (Prelude_error "LetRec not supported inside brackets yet (FIXME)").
1158 destruct case_RCase.
1160 apply (Prelude_error "Case not supported (BIG FIXME)").
1162 destruct case_SBrak.
1166 set (drop_lev (ec :: nil) (take_arg_types_as_tree t @@@ (ec :: nil))) as empty_tree.
1168 rewrite take_lemma'.
1170 rewrite mapOptionTree_compose.
1171 rewrite mapOptionTree_compose.
1172 rewrite unlev_relev.
1173 rewrite <- mapOptionTree_compose.
1176 set (mapOptionTree flatten_leveled_type (drop_lev (ec :: nil) succ)) as succ_host.
1177 set (mapOptionTree (flatten_type ○ unlev)(take_lev (ec :: nil) succ)) as succ_guest.
1178 set (mapOptionTree flatten_type (take_arg_types_as_tree t)) as succ_args.
1180 eapply nd_comp; [ eapply nd_rule; eapply RArrange; eapply RLeft; apply tree_of_nothing | idtac ].
1181 eapply nd_comp; [ eapply nd_rule; eapply RArrange; eapply RCanR | idtac ].
1182 refine (ga_unkappa Γ Δ (v2t ec) nil _ _ _ _ ;; _).
1183 eapply nd_comp; [ idtac | eapply arrange_brak ].
1189 apply (Prelude_error "found Brak at depth >0 indicating 3-level code; only two-level code is currently supported").
1195 unfold flatten_leveled_type at 2.
1198 rewrite mapOptionTree_compose.
1202 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RLeft; apply tree_of_nothing' ].
1203 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanR ].
1205 rewrite take_lemma'.
1206 rewrite unlev_relev.
1207 rewrite <- mapOptionTree_compose.
1208 eapply nd_comp; [ apply (arrange_esc _ _ ec) | idtac ].
1210 set (decide_tree_empty (take_lev (ec :: nil) succ)) as q'.
1216 set (mapOptionTree flatten_leveled_type (drop_lev (ec :: nil) succ)) as succ_host.
1217 set (mapOptionTree flatten_type (take_arg_types_as_tree t)) as succ_args.
1219 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RuCanR ].
1220 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RuCanR ].
1221 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RCanL ].
1222 eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
1223 eapply nd_comp; [ apply nd_llecnac | idtac ].
1224 apply nd_prod; [ idtac | eapply boost ].
1227 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanL ].
1235 refine ( _ ;; (boost _ _ _ _ _ (postcompose _ _ _ _ _ _ _ _))).
1243 refine ( _ ;; (boost _ _ _ _ _ (postcompose _ _ _ _ _ _ _ _))).
1245 refine ( _ ;; (boost _ _ _ _ _ (postcompose _ _ _ _ _ _ _ _))).
1251 (* environment has non-empty leaves *)
1252 apply (Prelude_error "ga_kappa not supported yet (BIG FIXME)").
1254 (* nesting too deep *)
1255 apply (Prelude_error "found Esc at depth >0 indicating 3-level code; only two-level code is currently supported").
1258 Definition skolemize_and_flatten_proof :
1262 (mapOptionTree (flatten_judgment ○ skolemize_judgment) h)
1263 (mapOptionTree (flatten_judgment ○ skolemize_judgment) c).
1265 rewrite mapOptionTree_compose.
1266 rewrite mapOptionTree_compose.
1267 apply flatten_proof.
1268 apply skolemize_proof.
1273 (* to do: establish some metric on judgments (max length of level of any succedent type, probably), show how to
1274 * calculate it, and show that the flattening procedure above drives it down by one *)
1277 Instance FlatteningFunctor {Γ}{Δ}{ec} : Functor (JudgmentsL (PCF Γ Δ ec)) (TypesL (SystemFCa Γ Δ)) (obact) :=
1278 { fmor := FlatteningFunctor_fmor }.
1280 Definition ReificationFunctor Γ Δ : Functor (JudgmentsL _ _ (PCF n Γ Δ)) SystemFCa' (mapOptionTree brakifyJudg).
1281 refine {| fmor := ReificationFunctor_fmor Γ Δ |}; unfold hom; unfold ob; simpl ; intros.
1283 Definition PCF_SMME (n:nat)(Γ:TypeEnv)(Δ:CoercionEnv Γ) : ProgrammingLanguageSMME.
1284 refine {| plsmme_pl := PCF n Γ Δ |}.
1287 Definition SystemFCa_SMME (n:nat)(Γ:TypeEnv)(Δ:CoercionEnv Γ) : ProgrammingLanguageSMME.
1288 refine {| plsmme_pl := SystemFCa n Γ Δ |}.
1291 Definition ReificationFunctorMonoidal n : MonoidalFunctor (JudgmentsN n) (JudgmentsN (S n)) (ReificationFunctor n).
1295 Definition PCF_SystemFCa_two_level n Γ Δ : TwoLevelLanguage (PCF_SMME n Γ Δ) (SystemFCa_SMME (S n) Γ Δ).
1298 (* ... and the retraction exists *)
1302 Implicit Arguments garrow [ ].