1 (*********************************************************************************************************************************)
4 (* The Flattening Functor. *)
6 (*********************************************************************************************************************************)
8 Generalizable All Variables.
9 Require Import Preamble.
10 Require Import General.
11 Require Import NaturalDeduction.
12 Require Import Coq.Strings.String.
13 Require Import Coq.Lists.List.
15 Require Import HaskKinds.
16 Require Import HaskCoreTypes.
17 Require Import HaskLiteralsAndTyCons.
18 Require Import HaskStrongTypes.
19 Require Import HaskProof.
20 Require Import NaturalDeduction.
22 Require Import HaskStrongTypes.
23 Require Import HaskStrong.
24 Require Import HaskProof.
25 Require Import HaskStrongToProof.
26 Require Import HaskProofToStrong.
31 * The flattening transformation. Currently only TWO-level languages are
32 * supported, and the level-1 sublanguage is rather limited.
34 * This file abuses terminology pretty badly. For purposes of this file,
35 * "PCF" means "the level-1 sublanguage" and "FC" (aka System FC) means
36 * the whole language (level-0 language including bracketed level-1 terms)
38 Section HaskFlattener.
40 Inductive TreeFlags {T:Type} : Tree T -> Type :=
41 | tf_leaf_true : forall x, TreeFlags (T_Leaf x)
42 | tf_leaf_false : forall x, TreeFlags (T_Leaf x)
43 | tf_branch : forall b1 b2, TreeFlags b1 -> TreeFlags b2 -> TreeFlags (b1,,b2).
45 Fixpoint mkFlags {T}(f:T -> bool)(t:Tree T) : TreeFlags t :=
46 match t as T return TreeFlags T with
47 | T_Leaf x => if f x then tf_leaf_true x else tf_leaf_false x
48 | T_Branch b1 b2 => tf_branch _ _ (mkFlags f b1) (mkFlags f b2)
51 (* take and drop are not exact inverses *)
53 (* drop replaces each leaf where the flag is set with a [] *)
54 Fixpoint drop {T}{Σ:Tree ??T}(tf:TreeFlags Σ) : Tree ??T :=
56 | tf_leaf_true x => []
57 | tf_leaf_false x => Σ
58 | tf_branch b1 b2 tb1 tb2 => (drop tb1),,(drop tb2)
61 (* take returns only those leaves for which the flag is set; all others are omitted entirely from the tree *)
62 Fixpoint take {T}{Σ:Tree T}(tf:TreeFlags Σ) : ??(Tree T) :=
64 | tf_leaf_true x => Some Σ
65 | tf_leaf_false x => None
66 | tf_branch b1 b2 tb1 tb2 =>
69 | Some b1' => match take tb2 with
71 | Some b2' => Some (b1',,b2')
76 Definition maybeTree {T}(t:??(Tree ??T)) : Tree ??T :=
82 Definition setNone {T}(b:bool)(f:T -> bool) : ??T -> bool :=
89 (* "Arrange" objects are parametric in the type of the leaves of the tree *)
90 Definition arrangeMap :
91 forall {T} (Σ₁ Σ₂:Tree ??T) {R} (f:T -> R),
93 Arrange (mapOptionTree f Σ₁) (mapOptionTree f Σ₂).
107 eapply RComp; [ apply IHX1 | apply IHX2 ].
110 Definition bnot (b:bool) : bool := if b then false else true.
112 Definition swapMiddle {T} (a b c d:Tree ??T) :
113 Arrange ((a,,b),,(c,,d)) ((a,,c),,(b,,d)).
129 forall {T} (Σ:Tree ??T) (f:T -> bool),
130 Arrange Σ (drop (mkFlags (setNone false f) Σ),,( (drop (mkFlags (setNone false (bnot ○ f)) Σ)))).
136 destruct (f t); simpl.
142 eapply RComp; [ idtac | apply swapMiddle ].
150 Definition arrange' :
151 forall {T} (Σ:Tree ??T) (f:T -> bool),
152 Arrange (drop (mkFlags (setNone false f) Σ),,( (drop (mkFlags (setNone false (bnot ○ f)) Σ)))) Σ.
158 destruct (f t); simpl.
164 eapply RComp; [ apply swapMiddle | idtac ].
172 Definition minus' n m :=
181 Ltac eqd_dec_refl' :=
183 | [ |- context[@eqd_dec ?T ?V ?X ?X] ] =>
184 destruct (@eqd_dec T V X X) as [eqd_dec1 | eqd_dec2];
185 [ clear eqd_dec1 | set (eqd_dec2 (refl_equal _)) as eqd_dec2'; inversion eqd_dec2' ]
188 Fixpoint reduceTree {T}(unit:T)(merge:T -> T -> T)(tt:Tree ??T) : T :=
190 | T_Leaf None => unit
191 | T_Leaf (Some x) => x
192 | T_Branch b1 b2 => merge (reduceTree unit merge b1) (reduceTree unit merge b2)
195 Set Printing Width 130.
197 Context {unitTy : forall TV, RawHaskType TV ★ }.
198 Context {prodTy : forall TV, RawHaskType TV ★ -> RawHaskType TV ★ -> RawHaskType TV ★ }.
199 Context {gaTy : forall TV, RawHaskType TV ★ -> RawHaskType TV ★ -> RawHaskType TV ★ -> RawHaskType TV ★ }.
201 Definition ga_mk_tree {Γ} (tr:Tree ??(HaskType Γ ★)) : HaskType Γ ★ :=
202 fun TV ite => reduceTree (unitTy TV) (prodTy TV) (mapOptionTree (fun x => x TV ite) tr).
204 Definition ga_mk {Γ}(ec:HaskType Γ ★ )(ant suc:Tree ??(HaskType Γ ★)) : HaskType Γ ★ :=
205 fun TV ite => gaTy TV (ec TV ite) (ga_mk_tree ant TV ite) (ga_mk_tree suc TV ite).
208 { ga_id : ∀ Γ Δ ec l a , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec a a @@ l] ]
209 ; ga_cancelr : ∀ Γ Δ ec l a , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec (a,,[]) a @@ l] ]
210 ; ga_cancell : ∀ Γ Δ ec l a , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec ([],,a) a @@ l] ]
211 ; ga_uncancelr : ∀ Γ Δ ec l a , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec a (a,,[]) @@ l] ]
212 ; ga_uncancell : ∀ Γ Δ ec l a , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec a ([],,a) @@ l] ]
213 ; ga_assoc : ∀ Γ Δ ec l a b c, ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec ((a,,b),,c) (a,,(b,,c)) @@ l] ]
214 ; ga_unassoc : ∀ Γ Δ ec l a b c, ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec (a,,(b,,c)) ((a,,b),,c) @@ l] ]
215 ; ga_swap : ∀ Γ Δ ec l a b , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec (a,,b) (b,,a) @@ l] ]
216 ; ga_drop : ∀ Γ Δ ec l a , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec a [] @@ l] ]
217 ; ga_copy : ∀ Γ Δ ec l a , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec a (a,,a) @@ l] ]
218 ; ga_first : ∀ Γ Δ ec l a b x, ND Rule [] [Γ > Δ > [@ga_mk Γ ec a b @@ l] |- [@ga_mk Γ ec (a,,x) (b,,x) @@ l] ]
219 ; ga_second : ∀ Γ Δ ec l a b x, ND Rule [] [Γ > Δ > [@ga_mk Γ ec a b @@ l] |- [@ga_mk Γ ec (x,,a) (x,,b) @@ l] ]
220 ; ga_lit : ∀ Γ Δ ec l lit , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec [] [literalType lit] @@ l] ]
221 ; ga_curry : ∀ Γ Δ ec l a b c, ND Rule [] [Γ > Δ > [@ga_mk Γ ec (a,,[b]) [c] @@ l] |- [@ga_mk Γ ec a [b ---> c] @@ l] ]
222 ; 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] ]
223 ; ga_apply : ∀ Γ Δ ec l a a' b c, ND Rule []
224 [Γ > Δ > [@ga_mk Γ ec a [b ---> c] @@ l],,[@ga_mk Γ ec a' [b] @@ l] |- [@ga_mk Γ ec (a,,a') [c] @@ l] ]
225 ; ga_kappa : ∀ Γ Δ ec l a b Σ, ND Rule
226 [Γ > Δ > Σ,,[@ga_mk Γ ec [] a @@ l] |- [@ga_mk Γ ec [] b @@ l] ]
227 [Γ > Δ > Σ |- [@ga_mk Γ ec a b @@ l] ]
229 Context `(gar:garrow).
231 Notation "a ~~~~> b" := (@ga_mk _ _ a b) (at level 20).
235 * - code types <[t]>@c become garrows c () t
236 * - free variables of type t at a level lev deeper than the succedent become garrows c () t
237 * - free variables at the level of the succedent become
239 Fixpoint garrowfy_raw_codetypes {TV}{κ}(exp: RawHaskType TV κ) : RawHaskType TV κ :=
242 | TAll _ y => TAll _ (fun v => garrowfy_raw_codetypes (y v))
243 | TApp _ _ x y => TApp (garrowfy_raw_codetypes x) (garrowfy_raw_codetypes y)
245 | TCoerc _ t1 t2 t => TCoerc (garrowfy_raw_codetypes t1) (garrowfy_raw_codetypes t2)
246 (garrowfy_raw_codetypes t)
248 | TCode v e => gaTy TV v (unitTy TV) (garrowfy_raw_codetypes e)
249 | TyFunApp tfc kl k lt => TyFunApp tfc kl k (garrowfy_raw_codetypes_list _ lt)
251 with garrowfy_raw_codetypes_list {TV}(lk:list Kind)(exp:@RawHaskTypeList TV lk) : @RawHaskTypeList TV lk :=
252 match exp in @RawHaskTypeList _ LK return @RawHaskTypeList TV LK with
253 | TyFunApp_nil => TyFunApp_nil
254 | TyFunApp_cons κ kl t rest => TyFunApp_cons _ _ (garrowfy_raw_codetypes t) (garrowfy_raw_codetypes_list _ rest)
256 Definition garrowfy_code_types {Γ}{κ}(ht:HaskType Γ κ) : HaskType Γ κ :=
258 garrowfy_raw_codetypes (ht TV ite).
260 Definition v2t {Γ}(ec:HaskTyVar Γ ★) := fun TV ite => TVar (ec TV ite).
262 Fixpoint garrowfy_leveled_code_types' {Γ}(ht:HaskType Γ ★)(lev:HaskLevel Γ) : HaskType Γ ★ :=
264 | nil => garrowfy_code_types ht
265 | ec::lev' => @ga_mk _ (v2t ec) [] [garrowfy_leveled_code_types' ht lev']
268 Definition garrowfy_leveled_code_types {Γ}(ht:LeveledHaskType Γ ★) : LeveledHaskType Γ ★ :=
271 garrowfy_leveled_code_types' htt lev @@ nil
274 Definition levelMatch {Γ}(lev:HaskLevel Γ) : LeveledHaskType Γ ★ -> bool :=
275 fun t => match t with ttype@@tlev => if eqd_dec tlev lev then true else false end.
277 (* In a tree of types, replace any type at depth "lev" or greater None *)
278 Definition mkDropFlags {Γ}(lev:HaskLevel Γ)(tt:Tree ??(LeveledHaskType Γ ★)) : TreeFlags tt :=
279 mkFlags (setNone false (levelMatch lev)) tt.
281 Definition drop_lev {Γ}(lev:HaskLevel Γ)(tt:Tree ??(LeveledHaskType Γ ★)) : Tree ??(LeveledHaskType Γ ★) :=
282 drop (mkDropFlags lev tt).
284 (* The opposite: replace any type which is NOT at level "lev" with None *)
285 Definition mkTakeFlags {Γ}(lev:HaskLevel Γ)(tt:Tree ??(LeveledHaskType Γ ★)) : TreeFlags tt :=
286 mkFlags (setNone true (bnot ○ levelMatch lev)) tt.
288 Definition take_lev {Γ}(lev:HaskLevel Γ)(tt:Tree ??(LeveledHaskType Γ ★)) : Tree ??(HaskType Γ ★) :=
289 mapOptionTree (fun x => garrowfy_code_types (unlev x)) (drop (mkTakeFlags lev tt)).
291 mapOptionTree (fun x => garrowfy_code_types (unlev x))
292 (maybeTree (take tt (mkFlags (
293 fun t => match t with
294 | Some (ttype @@ tlev) => if eqd_dec tlev lev then true else false
300 Lemma drop_lev_lemma : forall Γ (lev:HaskLevel Γ) x, drop_lev lev [x @@ lev] = [].
312 Lemma drop_lev_lemma_s : forall Γ (lev:HaskLevel Γ) ec x, drop_lev (ec::lev) [x @@ (ec :: lev)] = [].
323 Lemma take_lemma : forall Γ (lev:HaskLevel Γ) x, take_lev lev [x @@ lev] = [garrowfy_code_types x].
334 Ltac drop_simplify :=
336 | [ |- context[@drop_lev ?G ?L [ ?X @@ ?L ] ] ] =>
337 rewrite (drop_lev_lemma G L X)
338 | [ |- context[@drop_lev ?G (?E :: ?L) [ ?X @@ (?E :: ?L) ] ] ] =>
339 rewrite (drop_lev_lemma_s G L E X)
340 | [ |- context[@drop_lev ?G ?N (?A,,?B)] ] =>
341 change (@drop_lev G N (A,,B)) with ((@drop_lev G N A),,(@drop_lev G N B))
342 | [ |- context[@drop_lev ?G ?N (T_Leaf None)] ] =>
343 change (@drop_lev G N (T_Leaf (@None (LeveledHaskType G ★)))) with (T_Leaf (@None (LeveledHaskType G ★)))
346 Ltac take_simplify :=
348 | [ |- context[@take_lev ?G ?L [ ?X @@ ?L ] ] ] =>
349 rewrite (take_lemma G L X)
350 | [ |- context[@take_lev ?G ?N (?A,,?B)] ] =>
351 change (@take_lev G N (A,,B)) with ((@take_lev G N A),,(@take_lev G N B))
352 | [ |- context[@take_lev ?G ?N (T_Leaf None)] ] =>
353 change (@take_lev G N (T_Leaf (@None (LeveledHaskType G ★)))) with (T_Leaf (@None (LeveledHaskType G ★)))
356 Axiom literal_types_unchanged : forall Γ l, garrowfy_code_types (literalType l) = literalType(Γ:=Γ) l.
358 Axiom flatten_coercion : forall Γ Δ κ (σ τ:HaskType Γ κ) (γ:HaskCoercion Γ Δ (σ ∼∼∼ τ)),
359 HaskCoercion Γ Δ (garrowfy_code_types σ ∼∼∼ garrowfy_code_types τ).
361 (* This tries to assign a single level to the entire succedent of a judgment. If the succedent has types from different
362 * levels (should not happen) it just picks one; if the succedent has no non-None leaves (also should not happen) it
364 Definition getΓ (j:Judg) := match j with Γ > _ > _ |- _ => Γ end.
365 Definition getSuc (j:Judg) : Tree ??(LeveledHaskType (getΓ j) ★) :=
366 match j as J return Tree ??(LeveledHaskType (getΓ J) ★) with Γ > _ > _ |- s => s end.
367 Fixpoint getjlev {Γ}(tt:Tree ??(LeveledHaskType Γ ★)) : HaskLevel Γ :=
370 | T_Leaf (Some (_ @@ lev)) => lev
372 match getjlev b1 with
378 Definition unlev' {Γ} (x:LeveledHaskType Γ ★) :=
379 garrowfy_code_types (unlev x).
381 (* "n" is the maximum depth remaining AFTER flattening *)
382 Definition flatten_judgment (j:Judg) :=
383 match j as J return Judg with
384 Γ > Δ > ant |- suc =>
385 match getjlev suc with
386 | nil => Γ > Δ > mapOptionTree garrowfy_leveled_code_types ant
387 |- mapOptionTree garrowfy_leveled_code_types suc
389 | (ec::lev') => Γ > Δ > mapOptionTree garrowfy_leveled_code_types (drop_lev (ec::lev') ant)
391 (take_lev (ec::lev') ant)
392 (mapOptionTree unlev' suc) (* we know the level of all of suc *)
397 Definition boost : forall Γ Δ ant x y {lev},
398 ND Rule [] [ Γ > Δ > [x@@lev] |- [y@@lev] ] ->
399 ND Rule [ Γ > Δ > ant |- [x@@lev] ] [ Γ > Δ > ant |- [y@@lev] ].
401 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanL ].
402 eapply nd_comp; [ idtac | eapply nd_rule; apply (@RLet Γ Δ [] ant y x lev) ].
403 eapply nd_comp; [ apply nd_rlecnac | idtac ].
413 Definition postcompose' : ∀ Γ Δ ec lev a b c Σ,
414 ND Rule [] [ Γ > Δ > Σ |- [@ga_mk Γ ec a b @@ lev] ] ->
415 ND Rule [] [ Γ > Δ > Σ,,[@ga_mk Γ ec b c @@ lev] |- [@ga_mk Γ ec a c @@ lev] ].
417 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RExch ].
418 eapply nd_comp; [ idtac | eapply nd_rule; apply (@RLet Γ Δ [@ga_mk _ ec b c @@lev] Σ (@ga_mk _ ec a c) (@ga_mk _ ec a b) lev) ].
419 eapply nd_comp; [ apply nd_llecnac | idtac ].
422 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RExch ].
426 Definition precompose' : ∀ Γ Δ ec lev a b c Σ,
427 ND Rule [] [ Γ > Δ > Σ |- [@ga_mk Γ ec b c @@ lev] ] ->
428 ND Rule [] [ Γ > Δ > Σ,,[@ga_mk Γ ec a b @@ lev] |- [@ga_mk Γ ec a c @@ lev] ].
430 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RExch ].
431 eapply nd_comp; [ idtac | eapply nd_rule; apply (@RLet Γ Δ [@ga_mk _ ec a b @@lev] Σ (@ga_mk _ ec a c) (@ga_mk _ ec b c) lev) ].
432 eapply nd_comp; [ apply nd_llecnac | idtac ].
438 Definition postcompose : ∀ Γ Δ ec lev a b c,
439 ND Rule [] [ Γ > Δ > [] |- [@ga_mk Γ ec a b @@ lev] ] ->
440 ND Rule [] [ Γ > Δ > [@ga_mk Γ ec b c @@ lev] |- [@ga_mk Γ ec a c @@ lev] ].
450 Definition firstify : ∀ Γ Δ ec lev a b c Σ,
451 ND Rule [] [ Γ > Δ > Σ |- [@ga_mk Γ ec a b @@ lev] ] ->
452 ND Rule [] [ Γ > Δ > Σ |- [@ga_mk Γ ec (a,,c) (b,,c) @@ lev] ].
454 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanL ].
455 eapply nd_comp; [ idtac | eapply nd_rule; apply RLet ].
456 eapply nd_comp; [ apply nd_llecnac | idtac ].
459 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RuCanL ].
463 Definition secondify : ∀ Γ Δ ec lev a b c Σ,
464 ND Rule [] [ Γ > Δ > Σ |- [@ga_mk Γ ec a b @@ lev] ] ->
465 ND Rule [] [ Γ > Δ > Σ |- [@ga_mk Γ ec (c,,a) (c,,b) @@ lev] ].
467 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanL ].
468 eapply nd_comp; [ idtac | eapply nd_rule; apply RLet ].
469 eapply nd_comp; [ apply nd_llecnac | idtac ].
472 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RuCanL ].
476 Lemma ga_unkappa : ∀ Γ Δ ec l a b Σ,
478 [Γ > Δ > Σ |- [@ga_mk Γ ec a b @@ l] ]
479 [Γ > Δ > Σ,,[@ga_mk Γ ec [] a @@ l] |- [@ga_mk Γ ec [] b @@ l] ].
481 set (ga_comp Γ Δ ec l [] a b) as q.
483 set (@RLet Γ Δ) as q'.
484 set (@RLet Γ Δ [@ga_mk _ ec [] a @@ l] Σ (@ga_mk _ ec [] b) (@ga_mk _ ec a b) l) as q''.
506 Notation "` x" := (take_lev _ x) (at level 20).
507 Notation "`` x" := (mapOptionTree unlev x) (at level 20).
508 Notation "``` x" := (drop_lev _ x) (at level 20).
510 Definition garrowfy_arrangement' :
511 forall Γ (Δ:CoercionEnv Γ)
512 (ec:HaskTyVar Γ ★) (lev:HaskLevel Γ) (ant1 ant2:Tree ??(LeveledHaskType Γ ★)) (r:Arrange ant1 ant2),
513 ND Rule [] [Γ > Δ > [] |- [@ga_mk _ (v2t ec) (take_lev (ec :: lev) ant2) (take_lev (ec :: lev) ant1) @@ nil] ].
516 refine (fix garrowfy ant1 ant2 (r:Arrange ant1 ant2):
517 ND Rule [] [Γ > Δ > [] |- [@ga_mk _ (v2t ec) (take_lev (ec :: lev) ant2) (take_lev (ec :: lev) ant1) @@ nil]] :=
518 match r as R in Arrange A B return
519 ND Rule [] [Γ > Δ > [] |- [@ga_mk _ (v2t ec) (take_lev (ec :: lev) B) (take_lev (ec :: lev) A) @@ nil]]
521 | RCanL a => let case_RCanL := tt in ga_uncancell _ _ _ _ _
522 | RCanR a => let case_RCanR := tt in ga_uncancelr _ _ _ _ _
523 | RuCanL a => let case_RuCanL := tt in ga_cancell _ _ _ _ _
524 | RuCanR a => let case_RuCanR := tt in ga_cancelr _ _ _ _ _
525 | RAssoc a b c => let case_RAssoc := tt in ga_assoc _ _ _ _ _ _ _
526 | RCossa a b c => let case_RCossa := tt in ga_unassoc _ _ _ _ _ _ _
527 | RExch a b => let case_RExch := tt in ga_swap _ _ _ _ _ _
528 | RWeak a => let case_RWeak := tt in ga_drop _ _ _ _ _
529 | RCont a => let case_RCont := tt in ga_copy _ _ _ _ _
530 | RLeft a b c r' => let case_RLeft := tt in garrowfy _ _ r' ;; boost _ _ _ _ _ (ga_second _ _ _ _ _ _ _)
531 | RRight a b c r' => let case_RRight := tt in garrowfy _ _ r' ;; boost _ _ _ _ _ (ga_first _ _ _ _ _ _ _)
532 | RComp c b a r1 r2 => let case_RComp := tt in (fun r1' r2' => _) (garrowfy _ _ r1) (garrowfy _ _ r2)
533 end); clear garrowfy; repeat take_simplify; repeat drop_simplify; intros.
536 set (take_lev (ec :: lev) a) as a' in *.
537 set (take_lev (ec :: lev) b) as b' in *.
538 set (take_lev (ec :: lev) c) as c' in *.
539 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RCanL ].
540 eapply nd_comp; [ idtac | eapply nd_rule; apply
541 (@RLet Γ Δ [] [] (@ga_mk _ (v2t ec) a' c') (@ga_mk _ (v2t ec) a' b')) ].
542 eapply nd_comp; [ apply nd_llecnac | idtac ].
545 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RuCanL ].
546 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RCanR ].
547 eapply nd_comp; [ idtac | eapply nd_rule; apply
548 (@RLet Γ Δ [@ga_mk _ (v2t ec) a' b' @@ _] [] (@ga_mk _ (v2t ec) a' c') (@ga_mk _ (v2t ec) b' c'))].
549 eapply nd_comp; [ apply nd_llecnac | idtac ].
555 Definition garrowfy_arrangement :
556 forall Γ (Δ:CoercionEnv Γ) n
557 (ec:HaskTyVar Γ ★) (lev:HaskLevel Γ) (ant1 ant2:Tree ??(LeveledHaskType Γ ★)) (r:Arrange ant1 ant2) succ,
559 [Γ > Δ > mapOptionTree (garrowfy_leveled_code_types ) (drop_lev n ant1)
560 |- [@ga_mk _ (v2t ec) (take_lev (ec :: lev) ant1) (mapOptionTree (unlev' ) succ) @@ nil]]
561 [Γ > Δ > mapOptionTree (garrowfy_leveled_code_types ) (drop_lev n ant2)
562 |- [@ga_mk _ (v2t ec) (take_lev (ec :: lev) ant2) (mapOptionTree (unlev' ) succ) @@ nil]].
564 refine ( _ ;; (boost _ _ _ _ _ (postcompose _ _ _ _ _ _ _ (garrowfy_arrangement' Γ Δ ec lev ant1 ant2 r)))).
567 refine ((fix garrowfy ant1 ant2 (r:Arrange ant1 ant2) :=
568 match r as R in Arrange A B return
569 Arrange (mapOptionTree (garrowfy_leveled_code_types ) (drop_lev _ A))
570 (mapOptionTree (garrowfy_leveled_code_types ) (drop_lev _ B)) with
571 | RCanL a => let case_RCanL := tt in RCanL _
572 | RCanR a => let case_RCanR := tt in RCanR _
573 | RuCanL a => let case_RuCanL := tt in RuCanL _
574 | RuCanR a => let case_RuCanR := tt in RuCanR _
575 | RAssoc a b c => let case_RAssoc := tt in RAssoc _ _ _
576 | RCossa a b c => let case_RCossa := tt in RCossa _ _ _
577 | RExch a b => let case_RExch := tt in RExch _ _
578 | RWeak a => let case_RWeak := tt in RWeak _
579 | RCont a => let case_RCont := tt in RCont _
580 | RLeft a b c r' => let case_RLeft := tt in RLeft _ (garrowfy _ _ r')
581 | RRight a b c r' => let case_RRight := tt in RRight _ (garrowfy _ _ r')
582 | RComp a b c r1 r2 => let case_RComp := tt in RComp (garrowfy _ _ r1) (garrowfy _ _ r2)
583 end) ant1 ant2 r); clear garrowfy; repeat take_simplify; repeat drop_simplify; intros.
586 Definition flatten_arrangement :
587 forall Γ Δ ant1 ant2 succ (r:Arrange ant1 ant2),
588 ND Rule (mapOptionTree (flatten_judgment ) [Γ > Δ > ant1 |- succ])
589 (mapOptionTree (flatten_judgment ) [Γ > Δ > ant2 |- succ]).
592 set (getjlev succ) as succ_lev.
593 assert (succ_lev=getjlev succ).
611 eapply RComp; [ apply IHr1 | apply IHr2 ].
613 apply garrowfy_arrangement.
617 Definition ga_join Γ Δ Σ₁ Σ₂ a b ec :
618 ND Rule [] [Γ > Δ > Σ₁ |- [@ga_mk _ ec [] a @@ nil]] ->
619 ND Rule [] [Γ > Δ > Σ₂ |- [@ga_mk _ ec [] b @@ nil]] ->
620 ND Rule [] [Γ > Δ > Σ₁,,Σ₂ |- [@ga_mk _ ec [] (a,,b) @@ nil]].
623 apply secondify with (c:=a) in pfb.
626 eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
627 eapply nd_comp; [ eapply nd_llecnac | idtac ].
636 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanL ].
642 Definition arrange_brak : forall Γ Δ ec succ t,
644 [Γ > Δ > mapOptionTree (garrowfy_leveled_code_types ) (drop_lev (ec :: nil) succ),,
645 [(@ga_mk _ (v2t ec) [] (take_lev (ec :: nil) succ)) @@ nil] |- [(@ga_mk _ (v2t ec) [] [garrowfy_code_types t]) @@ nil]]
646 [Γ > Δ > mapOptionTree (garrowfy_leveled_code_types ) succ |- [(@ga_mk _ (v2t ec) [] [garrowfy_code_types t]) @@ nil]].
649 set (@arrange' _ succ (levelMatch (ec::nil))) as q.
650 set (arrangeMap _ _ garrowfy_leveled_code_types q) as y.
659 eapply nd_comp; [ apply nd_llecnac | idtac ].
660 eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
665 induction succ; try destruct a; simpl.
671 destruct l as [t' lev'].
672 destruct lev' as [|ec' lev'].
676 set (@eqd_dec (HaskLevel Γ) (haskLevelEqDecidable Γ) (ec' :: lev') (ec :: nil)) as q.
692 Definition arrange_esc : forall Γ Δ ec succ t,
694 [Γ > Δ > mapOptionTree (garrowfy_leveled_code_types ) succ |- [(@ga_mk _ (v2t ec) [] [garrowfy_code_types t]) @@ nil]]
695 [Γ > Δ > mapOptionTree (garrowfy_leveled_code_types ) (drop_lev (ec :: nil) succ),,
696 [(@ga_mk _ (v2t ec) [] (take_lev (ec :: nil) succ)) @@ nil] |- [(@ga_mk _ (v2t ec) [] [garrowfy_code_types t]) @@ nil]].
699 set (@arrange _ succ (levelMatch (ec::nil))) as q.
700 set (arrangeMap _ _ garrowfy_leveled_code_types q) as y.
712 unfold mkDropFlags; simpl.
716 destruct (General.list_eq_dec h0 (ec :: nil)).
718 unfold garrowfy_leveled_code_types'.
733 apply (Prelude_error "escapifying code with multi-leaf antecedents is not supported").
736 Lemma mapOptionTree_distributes
737 : forall T R (a b:Tree ??T) (f:T->R),
738 mapOptionTree f (a,,b) = (mapOptionTree f a),,(mapOptionTree f b).
742 Axiom garrowfy_commutes_with_substT :
743 forall κ Γ (Δ:CoercionEnv Γ) (σ:∀ TV, InstantiatedTypeEnv TV Γ → TV κ → RawHaskType TV ★) (τ:HaskType Γ κ),
744 garrowfy_code_types (substT σ τ) = substT (fun TV ite v => garrowfy_raw_codetypes (σ TV ite v))
745 (garrowfy_code_types τ).
747 Axiom garrowfy_commutes_with_HaskTAll :
748 forall κ Γ (Δ:CoercionEnv Γ) (σ:∀ TV, InstantiatedTypeEnv TV Γ → TV κ → RawHaskType TV ★),
749 garrowfy_code_types (HaskTAll κ σ) = HaskTAll κ (fun TV ite v => garrowfy_raw_codetypes (σ TV ite v)).
751 Axiom garrowfy_commutes_with_HaskTApp :
752 forall κ Γ (Δ:CoercionEnv Γ) (σ:∀ TV, InstantiatedTypeEnv TV Γ → TV κ → RawHaskType TV ★),
753 garrowfy_code_types (HaskTApp (weakF σ) (FreshHaskTyVar κ)) =
754 HaskTApp (weakF (fun TV ite v => garrowfy_raw_codetypes (σ TV ite v))) (FreshHaskTyVar κ).
756 Axiom garrowfy_commutes_with_weakLT : forall (Γ:TypeEnv) κ t,
757 garrowfy_leveled_code_types (weakLT(Γ:=Γ)(κ:=κ) t) = weakLT(Γ:=Γ)(κ:=κ) (garrowfy_leveled_code_types t).
759 Axiom globals_do_not_have_code_types : forall (Γ:TypeEnv) (g:Global Γ) v,
760 garrowfy_code_types (g v) = g v.
762 Definition decide_tree_empty : forall {T:Type}(t:Tree ??T),
763 sum { q:Tree unit & t = mapTree (fun _ => None) q } unit.
768 | T_Branch b1 b2 => let b1' := foo b1 in let b2' := foo b2 in _
789 Definition flatten_proof :
792 ND Rule (mapOptionTree (flatten_judgment ) h) (mapOptionTree (flatten_judgment ) c).
794 eapply nd_map'; [ idtac | apply X ].
799 refine (match X as R in Rule H C with
800 | RArrange Γ Δ a b x d => let case_RArrange := tt in _
801 | RNote Γ Δ Σ τ l n => let case_RNote := tt in _
802 | RLit Γ Δ l _ => let case_RLit := tt in _
803 | RVar Γ Δ σ lev => let case_RVar := tt in _
804 | RGlobal Γ Δ σ l wev => let case_RGlobal := tt in _
805 | RLam Γ Δ Σ tx te lev => let case_RLam := tt in _
806 | RCast Γ Δ Σ σ τ lev γ => let case_RCast := tt in _
807 | RAbsT Γ Δ Σ κ σ lev => let case_RAbsT := tt in _
808 | RAppT Γ Δ Σ κ σ τ lev => let case_RAppT := tt in _
809 | RAppCo Γ Δ Σ κ σ₁ σ₂ γ σ lev => let case_RAppCo := tt in _
810 | RAbsCo Γ Δ Σ κ σ σ₁ σ₂ lev => let case_RAbsCo := tt in _
811 | RApp Γ Δ Σ₁ Σ₂ tx te lev => let case_RApp := tt in _
812 | RLet Γ Δ Σ₁ Σ₂ σ₁ σ₂ lev => let case_RLet := tt in _
813 | RJoin Γ p lri m x q => let case_RJoin := tt in _
814 | RVoid _ _ => let case_RVoid := tt in _
815 | RBrak Γ Δ t ec succ lev => let case_RBrak := tt in _
816 | REsc Γ Δ t ec succ lev => let case_REsc := tt in _
817 | RCase Γ Δ lev tc Σ avars tbranches alts => let case_RCase := tt in _
818 | RLetRec Γ Δ lri x y t => let case_RLetRec := tt in _
821 destruct case_RArrange.
822 apply (flatten_arrangement Γ Δ a b x d).
827 change ([garrowfy_code_types (<[ ec |- t ]>) @@ nil])
828 with ([ga_mk (v2t ec) [] [garrowfy_code_types t] @@ nil]).
829 refine (ga_unkappa Γ Δ (v2t ec) nil (take_lev (ec::nil) succ) _
830 (mapOptionTree (garrowfy_leveled_code_types) (drop_lev (ec::nil) succ)) ;; _ ).
832 apply (Prelude_error "found Brak at depth >0 (a)").
838 change ([garrowfy_code_types (<[ ec |- t ]>) @@ nil])
839 with ([ga_mk (v2t ec) [] [garrowfy_code_types t] @@ nil]).
840 eapply nd_comp; [ apply arrange_esc | idtac ].
841 set (decide_tree_empty (take_lev (ec :: nil) succ)) as q'.
847 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanR ].
848 eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
849 eapply nd_comp; [ apply nd_llecnac | idtac ].
850 apply nd_prod; [ idtac | eapply boost ].
853 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanR ].
862 (* environment has non-empty leaves *)
863 apply (ga_kappa Γ Δ (v2t ec) nil (take_lev (ec::nil) succ) _ _).
864 apply (Prelude_error "found Esc at depth >0 (a)").
869 apply nd_rule; apply RNote; auto.
870 apply nd_rule; apply RNote; auto.
875 rewrite literal_types_unchanged.
876 apply nd_rule; apply RLit.
877 unfold take_lev; simpl.
878 unfold drop_lev; simpl.
881 rewrite literal_types_unchanged.
885 Opaque flatten_judgment.
887 Transparent flatten_judgment.
889 unfold flatten_judgment.
892 apply nd_rule. apply RVar.
893 repeat drop_simplify.
895 repeat take_simplify.
899 destruct case_RGlobal.
903 destruct l as [|ec lev]; simpl; [ apply nd_rule; rewrite globals_do_not_have_code_types; apply RGlobal; auto | idtac ].
904 apply (Prelude_error "found RGlobal at depth >0").
910 destruct lev as [|ec lev]; simpl; [ apply nd_rule; apply RLam; auto | idtac ].
911 repeat drop_simplify.
912 repeat take_simplify.
923 destruct lev as [|ec lev]; simpl; [ apply nd_rule; apply RCast; auto | idtac ].
924 apply flatten_coercion; auto.
925 apply (Prelude_error "RCast at level >0").
929 destruct (getjlev x); destruct (getjlev q).
932 apply (Prelude_error "RJoin at depth >0").
933 apply (Prelude_error "RJoin at depth >0").
934 apply (Prelude_error "RJoin at depth >0").
939 destruct lev as [|ec lev]. simpl. apply nd_rule.
940 replace (garrowfy_code_types (tx ---> te)) with ((garrowfy_code_types tx) ---> (garrowfy_code_types te)).
944 repeat drop_simplify.
945 repeat take_simplify.
946 rewrite mapOptionTree_distributes.
947 set (mapOptionTree (garrowfy_leveled_code_types ) (drop_lev (ec :: lev) Σ₁)) as Σ₁'.
948 set (mapOptionTree (garrowfy_leveled_code_types ) (drop_lev (ec :: lev) Σ₂)) as Σ₂'.
949 set (take_lev (ec :: lev) Σ₁) as Σ₁''.
950 set (take_lev (ec :: lev) Σ₂) as Σ₂''.
951 replace (garrowfy_code_types (tx ---> te)) with ((garrowfy_code_types tx) ---> (garrowfy_code_types te)).
952 apply (Prelude_error "FIXME: ga_apply").
955 Notation "` x" := (take_lev _ x) (at level 20).
956 Notation "`` x" := (mapOptionTree unlev x) (at level 20).
957 Notation "``` x" := ((drop_lev _ x)) (at level 20).
958 Notation "!<[]> x" := (garrowfy_code_types _ x) (at level 1).
959 Notation "!<[@]>" := (garrowfy_leveled_code_types _) (at level 1).
962 apply (Prelude_error "FIXME: RLet").
965 destruct lev as [|ec lev]; simpl; [ apply nd_rule; apply RLet; auto | idtac ].
966 destruct (Peano_dec.eq_nat_dec (Datatypes.length lev) n); [ idtac | apply nd_rule; apply RLet; auto ]; simpl.
967 repeat drop_simplify.
968 repeat take_simplify.
971 rewrite mapOptionTree_distributes.
972 rewrite mapOptionTree_distributes.
973 set (mapOptionTree (garrowfy_leveled_code_types (S n)) (drop_lev (ec :: lev) Σ₁)) as A.
974 set (take_lev (ec :: lev) Σ₁) as A'.
975 set (mapOptionTree (garrowfy_leveled_code_types (S n)) (drop_lev (ec :: lev) Σ₂)) as B.
976 set (take_lev (ec :: lev) Σ₂) as B'.
1019 destruct case_RVoid.
1024 destruct case_RAppT.
1025 simpl. destruct lev; simpl.
1026 rewrite garrowfy_commutes_with_HaskTAll.
1027 rewrite garrowfy_commutes_with_substT.
1032 apply (Prelude_error "ga_apply").
1034 destruct case_RAbsT.
1035 simpl. destruct lev; simpl.
1036 rewrite garrowfy_commutes_with_HaskTAll.
1037 rewrite garrowfy_commutes_with_HaskTApp.
1038 eapply nd_comp; [ idtac | eapply nd_rule; eapply RAbsT ].
1040 set (mapOptionTree (garrowfy_leveled_code_types ) (mapOptionTree (weakLT(κ:=κ)) Σ)) as a.
1041 set (mapOptionTree (weakLT(κ:=κ)) (mapOptionTree (garrowfy_leveled_code_types ) Σ)) as q'.
1049 rewrite garrowfy_commutes_with_weakLT.
1060 apply (Prelude_error "AbsT at depth>0").
1062 destruct case_RAppCo.
1063 simpl. destruct lev; simpl.
1064 unfold garrowfy_code_types.
1068 apply flatten_coercion.
1070 apply (Prelude_error "AppCo at depth>0").
1072 destruct case_RAbsCo.
1073 simpl. destruct lev; simpl.
1074 unfold garrowfy_code_types.
1076 apply (Prelude_error "AbsCo not supported (FIXME)").
1077 apply (Prelude_error "AbsCo at depth>0").
1079 destruct case_RLetRec.
1081 apply (Prelude_error "LetRec not supported (FIXME)").
1083 destruct case_RCase.
1085 apply (Prelude_error "Case not supported (FIXME)").
1089 (* to do: establish some metric on judgments (max length of level of any succedent type, probably), show how to
1090 * calculate it, and show that the flattening procedure above drives it down by one *)
1093 Instance FlatteningFunctor {Γ}{Δ}{ec} : Functor (JudgmentsL (PCF Γ Δ ec)) (TypesL (SystemFCa Γ Δ)) (obact) :=
1094 { fmor := FlatteningFunctor_fmor }.
1096 Definition ReificationFunctor Γ Δ : Functor (JudgmentsL _ _ (PCF n Γ Δ)) SystemFCa' (mapOptionTree brakifyJudg).
1097 refine {| fmor := ReificationFunctor_fmor Γ Δ |}; unfold hom; unfold ob; simpl ; intros.
1099 Definition PCF_SMME (n:nat)(Γ:TypeEnv)(Δ:CoercionEnv Γ) : ProgrammingLanguageSMME.
1100 refine {| plsmme_pl := PCF n Γ Δ |}.
1103 Definition SystemFCa_SMME (n:nat)(Γ:TypeEnv)(Δ:CoercionEnv Γ) : ProgrammingLanguageSMME.
1104 refine {| plsmme_pl := SystemFCa n Γ Δ |}.
1107 Definition ReificationFunctorMonoidal n : MonoidalFunctor (JudgmentsN n) (JudgmentsN (S n)) (ReificationFunctor n).
1111 Definition PCF_SystemFCa_two_level n Γ Δ : TwoLevelLanguage (PCF_SMME n Γ Δ) (SystemFCa_SMME (S n) Γ Δ).
1114 (* ... and the retraction exists *)
1118 Implicit Arguments garrow [ ].