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 RCanR ].
375 eapply nd_comp; [ idtac | eapply nd_rule; apply RLet ].
376 eapply nd_comp; [ apply nd_rlecnac | idtac ].
386 Definition precompose Γ Δ ec : forall a x y z lev,
388 [ Γ > Δ > a |- [@ga_mk _ ec y z @@ lev] ]
389 [ Γ > Δ > a,,[@ga_mk _ ec x y @@ lev] |- [@ga_mk _ ec x z @@ lev] ].
391 eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
392 eapply nd_comp; [ apply nd_rlecnac | idtac ].
395 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RExch ].
399 Definition precompose' Γ Δ ec : forall a b x y z lev,
401 [ Γ > Δ > a,,b |- [@ga_mk _ ec y z @@ lev] ]
402 [ Γ > Δ > a,,([@ga_mk _ ec x y @@ lev],,b) |- [@ga_mk _ ec x z @@ lev] ].
404 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RLeft; eapply RExch ].
405 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCossa ].
409 Definition postcompose_ Γ Δ ec : forall a x y z lev,
411 [ Γ > Δ > a |- [@ga_mk _ ec x y @@ lev] ]
412 [ Γ > Δ > a,,[@ga_mk _ ec y z @@ lev] |- [@ga_mk _ ec x z @@ lev] ].
414 eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
415 eapply nd_comp; [ apply nd_rlecnac | idtac ].
421 Definition postcompose Γ Δ ec : forall x y z lev,
422 ND Rule [] [ Γ > Δ > [] |- [@ga_mk _ ec x y @@ lev] ] ->
423 ND Rule [] [ Γ > Δ > [@ga_mk _ ec y z @@ lev] |- [@ga_mk _ ec x z @@ lev] ].
425 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanL ].
426 eapply nd_comp; [ idtac | eapply postcompose_ ].
430 Definition first_nd : ∀ Γ Δ ec lev a b c Σ,
431 ND Rule [ Γ > Δ > Σ |- [@ga_mk Γ ec a b @@ lev] ]
432 [ Γ > Δ > Σ |- [@ga_mk Γ ec (a,,c) (b,,c) @@ lev] ].
434 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanR ].
435 eapply nd_comp; [ idtac | eapply nd_rule; apply RLet ].
436 eapply nd_comp; [ apply nd_rlecnac | idtac ].
439 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RuCanR ].
443 Definition firstify : ∀ Γ Δ ec lev a b c Σ,
444 ND Rule [] [ Γ > Δ > Σ |- [@ga_mk Γ ec a b @@ lev] ] ->
445 ND Rule [] [ Γ > Δ > Σ |- [@ga_mk Γ ec (a,,c) (b,,c) @@ lev] ].
452 Definition second_nd : ∀ Γ Δ ec lev a b c Σ,
454 [ Γ > Δ > Σ |- [@ga_mk Γ ec a b @@ lev] ]
455 [ Γ > Δ > Σ |- [@ga_mk Γ ec (c,,a) (c,,b) @@ lev] ].
457 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanR ].
458 eapply nd_comp; [ idtac | eapply nd_rule; apply RLet ].
459 eapply nd_comp; [ apply nd_rlecnac | idtac ].
462 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RuCanR ].
466 Definition secondify : ∀ Γ Δ ec lev a b c Σ,
467 ND Rule [] [ Γ > Δ > Σ |- [@ga_mk Γ ec a b @@ lev] ] ->
468 ND Rule [] [ Γ > Δ > Σ |- [@ga_mk Γ ec (c,,a) (c,,b) @@ lev] ].
475 Lemma ga_unkappa : ∀ Γ Δ ec l a b Σ x,
477 [Γ > Δ > Σ |- [@ga_mk Γ ec (a,,x) b @@ l] ]
478 [Γ > Δ > Σ,,[@ga_mk Γ ec [] a @@ l] |- [@ga_mk Γ ec x b @@ l] ].
480 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RExch ].
481 eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
482 eapply nd_comp; [ apply nd_llecnac | idtac ].
486 eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
487 eapply nd_comp; [ apply nd_llecnac | idtac ].
491 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RExch ].
495 (* useful for cutting down on the pretty-printed noise
497 Notation "` x" := (take_lev _ x) (at level 20).
498 Notation "`` x" := (mapOptionTree unlev x) (at level 20).
499 Notation "``` x" := (drop_lev _ x) (at level 20).
501 Definition flatten_arrangement' :
502 forall Γ (Δ:CoercionEnv Γ)
503 (ec:HaskTyVar Γ ECKind) (lev:HaskLevel Γ) (ant1 ant2:Tree ??(LeveledHaskType Γ ★)) (r:Arrange ant1 ant2),
504 ND Rule [] [Γ > Δ > [] |- [@ga_mk _ (v2t ec) (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) ant2))
505 (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) ant1)) @@ nil] ].
508 refine (fix flatten ant1 ant2 (r:Arrange ant1 ant2):
509 ND Rule [] [Γ > Δ > [] |- [@ga_mk _ (v2t ec)
510 (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) ant2))
511 (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) ant1)) @@ nil]] :=
512 match r as R in Arrange A B return
513 ND Rule [] [Γ > Δ > [] |- [@ga_mk _ (v2t ec)
514 (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) B))
515 (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) A)) @@ nil]]
517 | RId a => let case_RId := tt in ga_id _ _ _ _ _
518 | RCanL a => let case_RCanL := tt in ga_uncancell _ _ _ _ _
519 | RCanR a => let case_RCanR := tt in ga_uncancelr _ _ _ _ _
520 | RuCanL a => let case_RuCanL := tt in ga_cancell _ _ _ _ _
521 | RuCanR a => let case_RuCanR := tt in ga_cancelr _ _ _ _ _
522 | RAssoc a b c => let case_RAssoc := tt in ga_assoc _ _ _ _ _ _ _
523 | RCossa a b c => let case_RCossa := tt in ga_unassoc _ _ _ _ _ _ _
524 | RExch a b => let case_RExch := tt in ga_swap _ _ _ _ _ _
525 | RWeak a => let case_RWeak := tt in ga_drop _ _ _ _ _
526 | RCont a => let case_RCont := tt in ga_copy _ _ _ _ _
527 | RLeft a b c r' => let case_RLeft := tt in flatten _ _ r' ;; boost _ _ _ _ _ (ga_second _ _ _ _ _ _ _)
528 | RRight a b c r' => let case_RRight := tt in flatten _ _ r' ;; boost _ _ _ _ _ (ga_first _ _ _ _ _ _ _)
529 | RComp c b a r1 r2 => let case_RComp := tt in (fun r1' r2' => _) (flatten _ _ r1) (flatten _ _ r2)
530 end); clear flatten; repeat take_simplify; repeat drop_simplify; intros.
533 set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) a)) as a' in *.
534 set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) b)) as b' in *.
535 set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) c)) as c' in *.
536 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RCanL ].
537 eapply nd_comp; [ idtac | eapply nd_rule; apply
538 (@RLet Γ Δ [] [] (@ga_mk _ (v2t ec) a' b') (@ga_mk _ (v2t ec) a' c')) ].
539 eapply nd_comp; [ apply nd_llecnac | idtac ].
542 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RuCanR ].
543 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RCanL ].
544 eapply nd_comp; [ idtac | eapply nd_rule; apply RLet ].
545 eapply nd_comp; [ apply nd_llecnac | idtac ].
548 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RExch ].
552 Definition flatten_arrangement :
553 forall Γ (Δ:CoercionEnv Γ) n
554 (ec:HaskTyVar Γ ECKind) (lev:HaskLevel Γ) (ant1 ant2:Tree ??(LeveledHaskType Γ ★)) (r:Arrange ant1 ant2) succ,
556 [Γ > Δ > mapOptionTree (flatten_leveled_type ) (drop_lev n ant1)
557 |- [@ga_mk _ (v2t ec)
558 (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) ant1))
559 (mapOptionTree (flatten_type ○ unlev) succ) @@ nil]]
560 [Γ > Δ > mapOptionTree (flatten_leveled_type ) (drop_lev n ant2)
561 |- [@ga_mk _ (v2t ec)
562 (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) ant2))
563 (mapOptionTree (flatten_type ○ unlev) succ) @@ nil]].
565 refine ( _ ;; (boost _ _ _ _ _ (postcompose _ _ _ _ _ _ _ (flatten_arrangement' Γ Δ ec lev ant1 ant2 r)))).
568 refine ((fix flatten ant1 ant2 (r:Arrange ant1 ant2) :=
569 match r as R in Arrange A B return
570 Arrange (mapOptionTree (flatten_leveled_type ) (drop_lev _ A))
571 (mapOptionTree (flatten_leveled_type ) (drop_lev _ B)) with
572 | RId a => let case_RId := tt in RId _
573 | RCanL a => let case_RCanL := tt in RCanL _
574 | RCanR a => let case_RCanR := tt in RCanR _
575 | RuCanL a => let case_RuCanL := tt in RuCanL _
576 | RuCanR a => let case_RuCanR := tt in RuCanR _
577 | RAssoc a b c => let case_RAssoc := tt in RAssoc _ _ _
578 | RCossa a b c => let case_RCossa := tt in RCossa _ _ _
579 | RExch a b => let case_RExch := tt in RExch _ _
580 | RWeak a => let case_RWeak := tt in RWeak _
581 | RCont a => let case_RCont := tt in RCont _
582 | RLeft a b c r' => let case_RLeft := tt in RLeft _ (flatten _ _ r')
583 | RRight a b c r' => let case_RRight := tt in RRight _ (flatten _ _ r')
584 | RComp a b c r1 r2 => let case_RComp := tt in RComp (flatten _ _ r1) (flatten _ _ r2)
585 end) ant1 ant2 r); clear flatten; repeat take_simplify; repeat drop_simplify; intros.
588 Definition flatten_arrangement'' :
589 forall Γ Δ ant1 ant2 succ (r:Arrange ant1 ant2),
590 ND Rule (mapOptionTree (flatten_judgment ) [Γ > Δ > ant1 |- succ])
591 (mapOptionTree (flatten_judgment ) [Γ > Δ > ant2 |- succ]).
594 set (getjlev succ) as succ_lev.
595 assert (succ_lev=getjlev succ).
609 apply RExch. (* TO DO: check for all-leaf trees here *)
614 eapply RComp; [ apply IHr1 | apply IHr2 ].
616 apply flatten_arrangement.
620 Definition ga_join Γ Δ Σ₁ Σ₂ a b ec :
621 ND Rule [] [Γ > Δ > Σ₁ |- [@ga_mk _ ec [] a @@ nil]] ->
622 ND Rule [] [Γ > Δ > Σ₂ |- [@ga_mk _ ec [] b @@ nil]] ->
623 ND Rule [] [Γ > Δ > Σ₁,,Σ₂ |- [@ga_mk _ ec [] (a,,b) @@ nil]].
626 apply secondify with (c:=a) in pfb.
627 apply firstify with (c:=[]) in pfa.
628 eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
629 eapply nd_comp; [ eapply nd_llecnac | idtac ].
634 eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
635 eapply nd_comp; [ apply nd_llecnac | idtac ].
637 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanL ].
638 eapply nd_comp; [ idtac | eapply postcompose_ ].
641 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RExch ].
642 eapply nd_comp; [ idtac | eapply precompose ].
646 Definition arrange_brak : forall Γ Δ ec succ t,
649 [(@ga_mk _ (v2t ec) [] (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: nil) succ))) @@ nil],,
650 mapOptionTree (flatten_leveled_type ) (drop_lev (ec :: nil) succ) |- [t @@ nil]]
651 [Γ > Δ > mapOptionTree (flatten_leveled_type ) succ |- [t @@ nil]].
655 set (@arrange' _ succ (levelMatch (ec::nil))) as q.
656 set (arrangeMap _ _ flatten_leveled_type q) as y.
664 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RExch ].
666 eapply nd_comp; [ apply nd_llecnac | idtac ].
667 eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
672 induction succ; try destruct a; simpl.
678 destruct l as [t' lev'].
679 destruct lev' as [|ec' lev'].
683 set (@eqd_dec (HaskLevel Γ) (haskLevelEqDecidable Γ) (ec' :: lev') (ec :: nil)) as q.
688 unfold flatten_leveled_type.
705 Definition arrange_empty_tree : forall {T}{A}(q:Tree A)(t:Tree ??T),
706 t = mapTree (fun _:A => None) q ->
714 destruct t; try destruct o; inversion H.
715 set (IHq1 _ H1) as x1.
716 set (IHq2 _ H2) as x2.
727 (* Definition unarrange_empty_tree : forall {T}{A}(t:Tree ??T)(q:Tree A),
728 t = mapTree (fun _:A => None) q ->
732 Definition decide_tree_empty : forall {T:Type}(t:Tree ??T),
733 sum { q:Tree unit & t = mapTree (fun _ => None) q } unit.
738 | T_Branch b1 b2 => let b1' := foo b1 in let b2' := foo b2 in _
758 Definition arrange_esc : forall Γ Δ ec succ t,
760 [Γ > Δ > mapOptionTree (flatten_leveled_type ) succ |- [t @@ nil]]
762 [(@ga_mk _ (v2t ec) [] (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: nil) succ))) @@ nil],,
763 mapOptionTree (flatten_leveled_type ) (drop_lev (ec :: nil) succ) |- [t @@ nil]].
765 set (@arrange _ succ (levelMatch (ec::nil))) as q.
766 set (@drop_lev Γ (ec::nil) succ) as q'.
767 assert (@drop_lev Γ (ec::nil) succ=q') as H.
769 unfold drop_lev in H.
770 unfold mkDropFlags in H.
773 set (arrangeMap _ _ flatten_leveled_type q) as y.
780 set (mapOptionTree flatten_leveled_type (dropT (mkFlags (liftBoolFunc false (bnot ○ levelMatch (ec :: nil))) succ))) as q.
781 destruct (decide_tree_empty q); [ idtac | apply (Prelude_error "escapifying open code not yet supported") ].
785 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RExch ].
786 set (fun z z' => @RLet Γ Δ z (mapOptionTree flatten_leveled_type q') t z' nil) as q''.
787 eapply nd_comp; [ idtac | eapply nd_rule; apply RLet ].
789 eapply nd_comp; [ apply nd_rlecnac | idtac ].
793 eapply RComp; [ idtac | apply RCanR ].
795 apply (@arrange_empty_tree _ _ _ _ e).
799 eapply (@RVar Γ Δ t nil).
807 eapply decide_tree_empty.
810 set (dropT (mkFlags (liftBoolFunc false (bnot ○ levelMatch (ec :: nil))) succ)) as escapified.
811 destruct (decide_tree_empty escapified).
818 unfold mkDropFlags; simpl.
822 destruct (General.list_eq_dec h0 (ec :: nil)).
838 apply (Prelude_error "escapifying code with multi-leaf antecedents is not supported").
842 Lemma mapOptionTree_distributes
843 : forall T R (a b:Tree ??T) (f:T->R),
844 mapOptionTree f (a,,b) = (mapOptionTree f a),,(mapOptionTree f b).
848 Lemma unlev_relev : forall {Γ}(t:Tree ??(HaskType Γ ★)) lev, mapOptionTree unlev (t @@@ lev) = t.
851 destruct a; reflexivity.
852 rewrite <- IHt1 at 2.
853 rewrite <- IHt2 at 2.
857 Lemma tree_of_nothing : forall Γ ec t,
858 Arrange (mapOptionTree flatten_leveled_type (drop_lev(Γ:=Γ) (ec :: nil) (t @@@ (ec :: nil)))) [].
860 induction t; try destruct o; try destruct a.
867 eapply RComp; [ idtac | apply RCanL ].
868 eapply RComp; [ idtac | eapply RLeft; apply IHt2 ].
871 Transparent drop_lev.
878 Lemma tree_of_nothing' : forall Γ ec t,
879 Arrange [] (mapOptionTree flatten_leveled_type (drop_lev(Γ:=Γ) (ec :: nil) (t @@@ (ec :: nil)))).
881 induction t; try destruct o; try destruct a.
888 eapply RComp; [ apply RuCanL | idtac ].
889 eapply RComp; [ eapply RRight; apply IHt1 | idtac ].
892 Transparent drop_lev.
899 Lemma krunk : forall Γ (ec:HaskTyVar Γ ECKind) t,
900 flatten_type (<[ ec |- t ]>)
902 (mapOptionTree flatten_type (take_arg_types_as_tree t))
903 [ flatten_type (drop_arg_types_as_tree t)].
905 unfold flatten_type at 1.
908 apply phoas_extensionality.
913 rewrite <- mapOptionTree_compose.
914 unfold take_arg_types_as_tree.
916 replace (flatten_type (drop_arg_types_as_tree t) tv ite)
917 with (drop_arg_types (flatten_rawtype (t tv ite))).
918 replace (unleaves_ (take_arg_types (flatten_rawtype (t tv ite))))
919 with ((mapOptionTree (fun x : HaskType Γ ★ => flatten_type x tv ite)
921 (take_trustme (count_arg_types (t (fun _ : Kind => unit) (ite_unit Γ)))
922 (fun TV : Kind → Type => take_arg_types ○ t TV))))).
925 clear hetmet_flatten.
926 clear hetmet_unflatten.
934 Definition flatten_proof :
937 ND Rule (mapOptionTree (flatten_judgment ) h) (mapOptionTree (flatten_judgment ) c).
939 eapply nd_map'; [ idtac | apply X ].
945 (match X as R in SRule H C with
946 | SBrak Γ Δ t ec succ lev => let case_SBrak := tt in _
947 | SEsc Γ Δ t ec succ lev => let case_SEsc := tt in _
948 | SFlat h c r => let case_SFlat := tt in _
952 refine (match r as R in Rule H C with
953 | RArrange Γ Δ a b x d => let case_RArrange := tt in _
954 | RNote Γ Δ Σ τ l n => let case_RNote := tt in _
955 | RLit Γ Δ l _ => let case_RLit := tt in _
956 | RVar Γ Δ σ lev => let case_RVar := tt in _
957 | RGlobal Γ Δ σ l wev => let case_RGlobal := tt in _
958 | RLam Γ Δ Σ tx te lev => let case_RLam := tt in _
959 | RCast Γ Δ Σ σ τ lev γ => let case_RCast := tt in _
960 | RAbsT Γ Δ Σ κ σ lev => let case_RAbsT := tt in _
961 | RAppT Γ Δ Σ κ σ τ lev => let case_RAppT := tt in _
962 | RAppCo Γ Δ Σ κ σ₁ σ₂ γ σ lev => let case_RAppCo := tt in _
963 | RAbsCo Γ Δ Σ κ σ σ₁ σ₂ lev => let case_RAbsCo := tt in _
964 | RApp Γ Δ Σ₁ Σ₂ tx te lev => let case_RApp := tt in _
965 | RLet Γ Δ Σ₁ Σ₂ σ₁ σ₂ lev => let case_RLet := tt in _
966 | RWhere Γ Δ Σ₁ Σ₂ Σ₃ σ₁ σ₂ lev => let case_RWhere := tt in _
967 | RJoin Γ p lri m x q => let case_RJoin := tt in _
968 | RVoid _ _ => let case_RVoid := tt in _
969 | RBrak Γ Δ t ec succ lev => let case_RBrak := tt in _
970 | REsc Γ Δ t ec succ lev => let case_REsc := tt in _
971 | RCase Γ Δ lev tc Σ avars tbranches alts => let case_RCase := tt in _
972 | RLetRec Γ Δ lri x y t => let case_RLetRec := tt in _
975 destruct case_RArrange.
976 apply (flatten_arrangement'' Γ Δ a b x d).
979 apply (Prelude_error "found unskolemized Brak rule; this shouldn't happen").
982 apply (Prelude_error "found unskolemized Esc rule; this shouldn't happen").
987 apply nd_rule; apply RNote; auto.
988 apply nd_rule; apply RNote; auto.
993 unfold flatten_leveled_type.
995 rewrite literal_types_unchanged.
996 apply nd_rule; apply RLit.
997 unfold take_lev; simpl.
998 unfold drop_lev; simpl.
1000 rewrite literal_types_unchanged.
1004 Opaque flatten_judgment.
1006 Transparent flatten_judgment.
1008 unfold flatten_judgment.
1011 apply nd_rule. apply RVar.
1012 repeat drop_simplify.
1013 repeat take_simplify.
1017 destruct case_RGlobal.
1021 destruct l as [|ec lev]; simpl.
1022 destruct (eqd_dec (g:CoreVar) (hetmet_flatten:CoreVar)).
1023 set (flatten_type (g wev)) as t.
1024 set (RGlobal _ Δ nil (mkGlobal Γ t hetmet_id)) as q.
1029 destruct (eqd_dec (g:CoreVar) (hetmet_unflatten:CoreVar)).
1030 set (flatten_type (g wev)) as t.
1031 set (RGlobal _ Δ nil (mkGlobal Γ t hetmet_id)) as q.
1036 unfold flatten_leveled_type. simpl.
1037 apply nd_rule; rewrite globals_do_not_have_code_types.
1039 apply (Prelude_error "found RGlobal at depth >0; globals should never appear inside code brackets unless escaped").
1045 destruct lev as [|ec lev]; simpl; [ apply nd_rule; apply RLam; auto | idtac ].
1046 repeat drop_simplify.
1047 repeat take_simplify.
1057 destruct case_RCast.
1059 destruct lev as [|ec lev]; simpl; [ apply nd_rule; apply RCast; auto | idtac ].
1061 apply flatten_coercion; auto.
1062 apply (Prelude_error "RCast at level >0; casting inside of code brackets is currently not supported").
1064 destruct case_RJoin.
1066 destruct (getjlev x); destruct (getjlev q);
1067 [ apply nd_rule; apply RJoin | idtac | idtac | idtac ];
1068 apply (Prelude_error "RJoin at depth >0").
1073 destruct lev as [|ec lev]. simpl. apply nd_rule.
1074 unfold flatten_leveled_type at 4.
1075 unfold flatten_leveled_type at 2.
1077 replace (flatten_type (tx ---> te))
1078 with (flatten_type tx ---> flatten_type te).
1082 repeat drop_simplify.
1083 repeat take_simplify.
1084 rewrite mapOptionTree_distributes.
1085 set (mapOptionTree (flatten_leveled_type ) (drop_lev (ec :: lev) Σ₁)) as Σ₁'.
1086 set (mapOptionTree (flatten_leveled_type ) (drop_lev (ec :: lev) Σ₂)) as Σ₂'.
1087 set (take_lev (ec :: lev) Σ₁) as Σ₁''.
1088 set (take_lev (ec :: lev) Σ₂) as Σ₂''.
1089 replace (flatten_type (tx ---> te)) with ((flatten_type tx) ---> (flatten_type te)).
1090 apply (Prelude_error "FIXME: ga_apply").
1094 Notation "` x" := (take_lev _ x).
1095 Notation "`` x" := (mapOptionTree unlev x) (at level 20).
1096 Notation "``` x" := ((drop_lev _ x)) (at level 20).
1097 Notation "!<[]> x" := (flatten_type _ x) (at level 1).
1098 Notation "!<[@]> x" := (mapOptionTree flatten_leveled_type x) (at level 1).
1103 destruct lev as [|ec lev]; simpl; [ apply nd_rule; apply RLet; auto | idtac ].
1104 repeat drop_simplify.
1105 repeat take_simplify.
1108 set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) Σ₁)) as Σ₁'.
1109 set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) Σ₂)) as Σ₂'.
1110 set (mapOptionTree flatten_leveled_type (drop_lev (ec :: lev) Σ₁)) as Σ₁''.
1111 set (mapOptionTree flatten_leveled_type (drop_lev (ec :: lev) Σ₂)) as Σ₂''.
1114 eapply nd_prod; [ idtac | apply nd_id ].
1116 apply (ga_first _ _ _ _ _ _ Σ₂').
1118 eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
1121 eapply nd_comp; [ eapply nd_rule; eapply RArrange; eapply RCanL | idtac ].
1122 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RExch (* okay *)].
1125 destruct case_RWhere.
1127 destruct lev as [|ec lev]; simpl; [ apply nd_rule; apply RWhere; auto | idtac ].
1128 repeat take_simplify.
1129 repeat drop_simplify.
1132 set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) Σ₁)) as Σ₁'.
1133 set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) Σ₂)) as Σ₂'.
1134 set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) Σ₃)) as Σ₃'.
1135 set (mapOptionTree flatten_leveled_type (drop_lev (ec :: lev) Σ₁)) as Σ₁''.
1136 set (mapOptionTree flatten_leveled_type (drop_lev (ec :: lev) Σ₂)) as Σ₂''.
1137 set (mapOptionTree flatten_leveled_type (drop_lev (ec :: lev) Σ₃)) as Σ₃''.
1140 eapply nd_prod; [ eapply nd_id | idtac ].
1141 eapply (first_nd _ _ _ _ _ _ Σ₃').
1143 eapply nd_prod; [ eapply nd_id | idtac ].
1144 eapply (second_nd _ _ _ _ _ _ Σ₁').
1146 eapply nd_comp; [ idtac | eapply nd_rule; eapply RWhere ].
1147 apply nd_prod; [ idtac | apply nd_id ].
1148 eapply nd_comp; [ idtac | eapply precompose' ].
1154 destruct case_RVoid.
1159 destruct case_RAppT.
1160 simpl. destruct lev; simpl.
1161 unfold flatten_leveled_type.
1163 rewrite flatten_commutes_with_HaskTAll.
1164 rewrite flatten_commutes_with_substT.
1169 apply (Prelude_error "found type application at level >0; this is not supported").
1171 destruct case_RAbsT.
1172 simpl. destruct lev; simpl.
1173 unfold flatten_leveled_type at 4.
1174 unfold flatten_leveled_type at 2.
1176 rewrite flatten_commutes_with_HaskTAll.
1177 rewrite flatten_commutes_with_HaskTApp.
1178 eapply nd_comp; [ idtac | eapply nd_rule; eapply RAbsT ].
1180 set (mapOptionTree (flatten_leveled_type ) (mapOptionTree (weakLT(κ:=κ)) Σ)) as a.
1181 set (mapOptionTree (weakLT(κ:=κ)) (mapOptionTree (flatten_leveled_type ) Σ)) as q'.
1189 rewrite flatten_commutes_with_weakLT.
1200 apply (Prelude_error "found type abstraction at level >0; this is not supported").
1202 destruct case_RAppCo.
1203 simpl. destruct lev; simpl.
1204 unfold flatten_leveled_type at 4.
1205 unfold flatten_leveled_type at 2.
1206 unfold flatten_type.
1210 apply flatten_coercion.
1212 apply (Prelude_error "found coercion application at level >0; this is not supported").
1214 destruct case_RAbsCo.
1215 simpl. destruct lev; simpl.
1216 unfold flatten_type.
1218 apply (Prelude_error "AbsCo not supported (FIXME)").
1219 apply (Prelude_error "found coercion abstraction at level >0; this is not supported").
1221 destruct case_RLetRec.
1223 simpl. destruct lev; simpl.
1224 replace (getjlev (y @@@ nil)) with (nil: (HaskLevel Γ)).
1225 replace (mapOptionTree flatten_leveled_type (y @@@ nil))
1226 with ((mapOptionTree flatten_type y) @@@ nil).
1227 unfold flatten_leveled_type at 2.
1229 unfold flatten_leveled_type at 3.
1232 set (@RLetRec Γ Δ (mapOptionTree flatten_leveled_type lri) (flatten_type x) (mapOptionTree flatten_type y) nil) as q.
1235 induction y; try destruct a; auto.
1240 induction y; try destruct a; auto.
1245 apply (Prelude_error "LetRec not supported inside brackets yet (FIXME)").
1247 destruct case_RCase.
1249 apply (Prelude_error "Case not supported (BIG FIXME)").
1251 destruct case_SBrak.
1255 set (drop_lev (ec :: nil) (take_arg_types_as_tree t @@@ (ec :: nil))) as empty_tree.
1257 rewrite take_lemma'.
1259 rewrite mapOptionTree_compose.
1260 rewrite mapOptionTree_compose.
1261 rewrite unlev_relev.
1262 rewrite <- mapOptionTree_compose.
1263 unfold flatten_leveled_type at 4.
1266 set (mapOptionTree flatten_leveled_type (drop_lev (ec :: nil) succ)) as succ_host.
1267 set (mapOptionTree (flatten_type ○ unlev)(take_lev (ec :: nil) succ)) as succ_guest.
1268 set (mapOptionTree flatten_type (take_arg_types_as_tree t)) as succ_args.
1270 eapply nd_comp; [ eapply nd_rule; eapply RArrange; eapply RLeft; apply tree_of_nothing | idtac ].
1271 eapply nd_comp; [ eapply nd_rule; eapply RArrange; eapply RCanR | idtac ].
1272 refine (ga_unkappa Γ Δ (v2t ec) nil _ _ _ _ ;; _).
1273 eapply nd_comp; [ idtac | eapply arrange_brak ].
1279 apply (Prelude_error "found Brak at depth >0 indicating 3-level code; only two-level code is currently supported").
1285 unfold flatten_leveled_type at 2.
1288 rewrite mapOptionTree_compose.
1292 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RLeft; apply tree_of_nothing' ].
1293 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanR ].
1295 rewrite take_lemma'.
1296 rewrite unlev_relev.
1297 rewrite <- mapOptionTree_compose.
1298 eapply nd_comp; [ apply (arrange_esc _ _ ec) | idtac ].
1300 set (decide_tree_empty (take_lev (ec :: nil) succ)) as q'.
1306 set (mapOptionTree flatten_leveled_type (drop_lev (ec :: nil) succ)) as succ_host.
1307 set (mapOptionTree flatten_type (take_arg_types_as_tree t)) as succ_args.
1309 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RuCanR ].
1310 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RuCanR ].
1311 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RCanL ].
1312 eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
1313 eapply nd_comp; [ apply nd_llecnac | idtac ].
1314 apply nd_prod; [ idtac | eapply boost ].
1317 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanL ].
1325 refine ( _ ;; (boost _ _ _ _ _ (postcompose _ _ _ _ _ _ _ _))).
1333 refine ( _ ;; (boost _ _ _ _ _ (postcompose _ _ _ _ _ _ _ _))).
1335 refine ( _ ;; (boost _ _ _ _ _ (postcompose _ _ _ _ _ _ _ _))).
1341 (* environment has non-empty leaves *)
1342 apply (Prelude_error "ga_kappa not supported yet (BIG FIXME)").
1344 (* nesting too deep *)
1345 apply (Prelude_error "found Esc at depth >0 indicating 3-level code; only two-level code is currently supported").
1348 Definition skolemize_and_flatten_proof :
1352 (mapOptionTree (flatten_judgment ○ skolemize_judgment) h)
1353 (mapOptionTree (flatten_judgment ○ skolemize_judgment) c).
1355 rewrite mapOptionTree_compose.
1356 rewrite mapOptionTree_compose.
1357 apply flatten_proof.
1358 apply skolemize_proof.
1363 (* to do: establish some metric on judgments (max length of level of any succedent type, probably), show how to
1364 * calculate it, and show that the flattening procedure above drives it down by one *)
1367 Instance FlatteningFunctor {Γ}{Δ}{ec} : Functor (JudgmentsL (PCF Γ Δ ec)) (TypesL (SystemFCa Γ Δ)) (obact) :=
1368 { fmor := FlatteningFunctor_fmor }.
1370 Definition ReificationFunctor Γ Δ : Functor (JudgmentsL _ _ (PCF n Γ Δ)) SystemFCa' (mapOptionTree brakifyJudg).
1371 refine {| fmor := ReificationFunctor_fmor Γ Δ |}; unfold hom; unfold ob; simpl ; intros.
1373 Definition PCF_SMME (n:nat)(Γ:TypeEnv)(Δ:CoercionEnv Γ) : ProgrammingLanguageSMME.
1374 refine {| plsmme_pl := PCF n Γ Δ |}.
1377 Definition SystemFCa_SMME (n:nat)(Γ:TypeEnv)(Δ:CoercionEnv Γ) : ProgrammingLanguageSMME.
1378 refine {| plsmme_pl := SystemFCa n Γ Δ |}.
1381 Definition ReificationFunctorMonoidal n : MonoidalFunctor (JudgmentsN n) (JudgmentsN (S n)) (ReificationFunctor n).
1385 Definition PCF_SystemFCa_two_level n Γ Δ : TwoLevelLanguage (PCF_SMME n Γ Δ) (SystemFCa_SMME (S n) Γ Δ).
1388 (* ... and the retraction exists *)
1392 Implicit Arguments garrow [ ].