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 HaskLiteralsAndTyCons.
21 Require Import HaskStrongTypes.
22 Require Import HaskProof.
23 Require Import NaturalDeduction.
25 Require Import HaskStrongTypes.
26 Require Import HaskStrong.
27 Require Import HaskProof.
28 Require Import HaskStrongToProof.
29 Require Import HaskProofToStrong.
30 Require Import HaskWeakToStrong.
35 * The flattening transformation. Currently only TWO-level languages are
36 * supported, and the level-1 sublanguage is rather limited.
38 * This file abuses terminology pretty badly. For purposes of this file,
39 * "PCF" means "the level-1 sublanguage" and "FC" (aka System FC) means
40 * the whole language (level-0 language including bracketed level-1 terms)
42 Section HaskFlattener.
44 Inductive TreeFlags {T:Type} : Tree T -> Type :=
45 | tf_leaf_true : forall x, TreeFlags (T_Leaf x)
46 | tf_leaf_false : forall x, TreeFlags (T_Leaf x)
47 | tf_branch : forall b1 b2, TreeFlags b1 -> TreeFlags b2 -> TreeFlags (b1,,b2).
49 Fixpoint mkFlags {T}(f:T -> bool)(t:Tree T) : TreeFlags t :=
50 match t as T return TreeFlags T with
51 | T_Leaf x => if f x then tf_leaf_true x else tf_leaf_false x
52 | T_Branch b1 b2 => tf_branch _ _ (mkFlags f b1) (mkFlags f b2)
55 (* take and drop are not exact inverses *)
57 (* drop replaces each leaf where the flag is set with a [] *)
58 Fixpoint drop {T}{Σ:Tree ??T}(tf:TreeFlags Σ) : Tree ??T :=
60 | tf_leaf_true x => []
61 | tf_leaf_false x => Σ
62 | tf_branch b1 b2 tb1 tb2 => (drop tb1),,(drop tb2)
65 (* take returns only those leaves for which the flag is set; all others are omitted entirely from the tree *)
66 Fixpoint take {T}{Σ:Tree T}(tf:TreeFlags Σ) : ??(Tree T) :=
68 | tf_leaf_true x => Some Σ
69 | tf_leaf_false x => None
70 | tf_branch b1 b2 tb1 tb2 =>
73 | Some b1' => match take tb2 with
75 | Some b2' => Some (b1',,b2')
80 Definition maybeTree {T}(t:??(Tree ??T)) : Tree ??T :=
86 Definition setNone {T}(b:bool)(f:T -> bool) : ??T -> bool :=
93 (* "Arrange" objects are parametric in the type of the leaves of the tree *)
94 Definition arrangeMap :
95 forall {T} (Σ₁ Σ₂:Tree ??T) {R} (f:T -> R),
97 Arrange (mapOptionTree f Σ₁) (mapOptionTree f Σ₂).
111 eapply RComp; [ apply IHX1 | apply IHX2 ].
114 Definition bnot (b:bool) : bool := if b then false else true.
116 Definition swapMiddle {T} (a b c d:Tree ??T) :
117 Arrange ((a,,b),,(c,,d)) ((a,,c),,(b,,d)).
133 forall {T} (Σ:Tree ??T) (f:T -> bool),
134 Arrange Σ (drop (mkFlags (setNone false f) Σ),,( (drop (mkFlags (setNone false (bnot ○ f)) Σ)))).
140 destruct (f t); simpl.
146 eapply RComp; [ idtac | apply swapMiddle ].
154 Definition arrange' :
155 forall {T} (Σ:Tree ??T) (f:T -> bool),
156 Arrange (drop (mkFlags (setNone false f) Σ),,( (drop (mkFlags (setNone false (bnot ○ f)) Σ)))) Σ.
162 destruct (f t); simpl.
168 eapply RComp; [ apply swapMiddle | idtac ].
176 Definition minus' n m :=
185 Ltac eqd_dec_refl' :=
187 | [ |- context[@eqd_dec ?T ?V ?X ?X] ] =>
188 destruct (@eqd_dec T V X X) as [eqd_dec1 | eqd_dec2];
189 [ clear eqd_dec1 | set (eqd_dec2 (refl_equal _)) as eqd_dec2'; inversion eqd_dec2' ]
192 Fixpoint reduceTree {T}(unit:T)(merge:T -> T -> T)(tt:Tree ??T) : T :=
194 | T_Leaf None => unit
195 | T_Leaf (Some x) => x
196 | T_Branch b1 b2 => merge (reduceTree unit merge b1) (reduceTree unit merge b2)
199 Set Printing Width 130.
201 Context (hetmet_flatten : WeakExprVar).
202 Context (hetmet_id : WeakExprVar).
203 Context {unitTy : forall TV, RawHaskType TV ★ }.
204 Context {prodTy : forall TV, RawHaskType TV ★ -> RawHaskType TV ★ -> RawHaskType TV ★ }.
205 Context {gaTy : forall TV, RawHaskType TV ECKind -> RawHaskType TV ★ -> RawHaskType TV ★ -> RawHaskType TV ★ }.
207 Definition ga_mk_tree {Γ} (tr:Tree ??(HaskType Γ ★)) : HaskType Γ ★ :=
208 fun TV ite => reduceTree (unitTy TV) (prodTy TV) (mapOptionTree (fun x => x TV ite) tr).
210 Definition ga_mk {Γ}(ec:HaskType Γ ECKind )(ant suc:Tree ??(HaskType Γ ★)) : HaskType Γ ★ :=
211 fun TV ite => gaTy TV (ec TV ite) (ga_mk_tree ant TV ite) (ga_mk_tree suc TV ite).
214 { ga_id : ∀ Γ Δ ec l a , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec a a @@ l] ]
215 ; ga_cancelr : ∀ Γ Δ ec l a , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec (a,,[]) a @@ l] ]
216 ; ga_cancell : ∀ Γ Δ ec l a , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec ([],,a) a @@ l] ]
217 ; ga_uncancelr : ∀ Γ Δ ec l a , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec a (a,,[]) @@ l] ]
218 ; ga_uncancell : ∀ Γ Δ ec l a , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec a ([],,a) @@ l] ]
219 ; ga_assoc : ∀ Γ Δ ec l a b c, ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec ((a,,b),,c) (a,,(b,,c)) @@ l] ]
220 ; ga_unassoc : ∀ Γ Δ ec l a b c, ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec (a,,(b,,c)) ((a,,b),,c) @@ l] ]
221 ; ga_swap : ∀ Γ Δ ec l a b , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec (a,,b) (b,,a) @@ l] ]
222 ; ga_drop : ∀ Γ Δ ec l a , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec a [] @@ l] ]
223 ; ga_copy : ∀ Γ Δ ec l a , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec a (a,,a) @@ l] ]
224 ; ga_first : ∀ Γ Δ ec l a b x, ND Rule [] [Γ > Δ > [@ga_mk Γ ec a b @@ l] |- [@ga_mk Γ ec (a,,x) (b,,x) @@ l] ]
225 ; ga_second : ∀ Γ Δ ec l a b x, ND Rule [] [Γ > Δ > [@ga_mk Γ ec a b @@ l] |- [@ga_mk Γ ec (x,,a) (x,,b) @@ l] ]
226 ; ga_lit : ∀ Γ Δ ec l lit , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec [] [literalType lit] @@ l] ]
227 ; ga_curry : ∀ Γ Δ ec l a b c, ND Rule [] [Γ > Δ > [@ga_mk Γ ec (a,,[b]) [c] @@ l] |- [@ga_mk Γ ec a [b ---> c] @@ l] ]
228 ; 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] ]
229 ; ga_apply : ∀ Γ Δ ec l a a' b c, ND Rule []
230 [Γ > Δ > [@ga_mk Γ ec a [b ---> c] @@ l],,[@ga_mk Γ ec a' [b] @@ l] |- [@ga_mk Γ ec (a,,a') [c] @@ l] ]
231 ; ga_kappa : ∀ Γ Δ ec l a b Σ, ND Rule
232 [Γ > Δ > Σ,,[@ga_mk Γ ec [] a @@ l] |- [@ga_mk Γ ec [] b @@ l] ]
233 [Γ > Δ > Σ |- [@ga_mk Γ ec a b @@ l] ]
235 Context `(gar:garrow).
237 Notation "a ~~~~> b" := (@ga_mk _ _ a b) (at level 20).
241 * - code types <[t]>@c become garrows c () t
242 * - free variables of type t at a level lev deeper than the succedent become garrows c () t
243 * - free variables at the level of the succedent become
245 Fixpoint garrowfy_raw_codetypes {TV}{κ}(exp: RawHaskType TV κ) : RawHaskType TV κ :=
248 | TAll _ y => TAll _ (fun v => garrowfy_raw_codetypes (y v))
249 | TApp _ _ x y => TApp (garrowfy_raw_codetypes x) (garrowfy_raw_codetypes y)
251 | TCoerc _ t1 t2 t => TCoerc (garrowfy_raw_codetypes t1) (garrowfy_raw_codetypes t2)
252 (garrowfy_raw_codetypes t)
254 | TCode v e => gaTy TV v (unitTy TV) (garrowfy_raw_codetypes e)
255 | TyFunApp tfc kl k lt => TyFunApp tfc kl k (garrowfy_raw_codetypes_list _ lt)
257 with garrowfy_raw_codetypes_list {TV}(lk:list Kind)(exp:@RawHaskTypeList TV lk) : @RawHaskTypeList TV lk :=
258 match exp in @RawHaskTypeList _ LK return @RawHaskTypeList TV LK with
259 | TyFunApp_nil => TyFunApp_nil
260 | TyFunApp_cons κ kl t rest => TyFunApp_cons _ _ (garrowfy_raw_codetypes t) (garrowfy_raw_codetypes_list _ rest)
262 Definition garrowfy_code_types {Γ}{κ}(ht:HaskType Γ κ) : HaskType Γ κ :=
264 garrowfy_raw_codetypes (ht TV ite).
266 Definition v2t {Γ}(ec:HaskTyVar Γ ECKind) := fun TV ite => TVar (ec TV ite).
268 Fixpoint garrowfy_leveled_code_types' {Γ}(ht:HaskType Γ ★)(lev:HaskLevel Γ) : HaskType Γ ★ :=
270 | nil => garrowfy_code_types ht
271 | ec::lev' => @ga_mk _ (v2t ec) [] [garrowfy_leveled_code_types' ht lev']
274 Definition garrowfy_leveled_code_types {Γ}(ht:LeveledHaskType Γ ★) : LeveledHaskType Γ ★ :=
277 garrowfy_leveled_code_types' htt lev @@ nil
280 Definition levelMatch {Γ}(lev:HaskLevel Γ) : LeveledHaskType Γ ★ -> bool :=
281 fun t => match t with ttype@@tlev => if eqd_dec tlev lev then true else false end.
283 (* In a tree of types, replace any type at depth "lev" or greater None *)
284 Definition mkDropFlags {Γ}(lev:HaskLevel Γ)(tt:Tree ??(LeveledHaskType Γ ★)) : TreeFlags tt :=
285 mkFlags (setNone false (levelMatch lev)) tt.
287 Definition drop_lev {Γ}(lev:HaskLevel Γ)(tt:Tree ??(LeveledHaskType Γ ★)) : Tree ??(LeveledHaskType Γ ★) :=
288 drop (mkDropFlags lev tt).
290 (* The opposite: replace any type which is NOT at level "lev" with None *)
291 Definition mkTakeFlags {Γ}(lev:HaskLevel Γ)(tt:Tree ??(LeveledHaskType Γ ★)) : TreeFlags tt :=
292 mkFlags (setNone true (bnot ○ levelMatch lev)) tt.
294 Definition take_lev {Γ}(lev:HaskLevel Γ)(tt:Tree ??(LeveledHaskType Γ ★)) : Tree ??(HaskType Γ ★) :=
295 mapOptionTree (fun x => garrowfy_code_types (unlev x)) (drop (mkTakeFlags lev tt)).
297 mapOptionTree (fun x => garrowfy_code_types (unlev x))
298 (maybeTree (take tt (mkFlags (
299 fun t => match t with
300 | Some (ttype @@ tlev) => if eqd_dec tlev lev then true else false
306 Lemma drop_lev_lemma : forall Γ (lev:HaskLevel Γ) x, drop_lev lev [x @@ lev] = [].
318 Lemma drop_lev_lemma_s : forall Γ (lev:HaskLevel Γ) ec x, drop_lev (ec::lev) [x @@ (ec :: lev)] = [].
329 Lemma take_lemma : forall Γ (lev:HaskLevel Γ) x, take_lev lev [x @@ lev] = [garrowfy_code_types x].
340 Ltac drop_simplify :=
342 | [ |- context[@drop_lev ?G ?L [ ?X @@ ?L ] ] ] =>
343 rewrite (drop_lev_lemma G L X)
344 | [ |- context[@drop_lev ?G (?E :: ?L) [ ?X @@ (?E :: ?L) ] ] ] =>
345 rewrite (drop_lev_lemma_s G L E X)
346 | [ |- context[@drop_lev ?G ?N (?A,,?B)] ] =>
347 change (@drop_lev G N (A,,B)) with ((@drop_lev G N A),,(@drop_lev G N B))
348 | [ |- context[@drop_lev ?G ?N (T_Leaf None)] ] =>
349 change (@drop_lev G N (T_Leaf (@None (LeveledHaskType G ★)))) with (T_Leaf (@None (LeveledHaskType G ★)))
352 Ltac take_simplify :=
354 | [ |- context[@take_lev ?G ?L [ ?X @@ ?L ] ] ] =>
355 rewrite (take_lemma G L X)
356 | [ |- context[@take_lev ?G ?N (?A,,?B)] ] =>
357 change (@take_lev G N (A,,B)) with ((@take_lev G N A),,(@take_lev G N B))
358 | [ |- context[@take_lev ?G ?N (T_Leaf None)] ] =>
359 change (@take_lev G N (T_Leaf (@None (LeveledHaskType G ★)))) with (T_Leaf (@None (LeveledHaskType G ★)))
362 Axiom literal_types_unchanged : forall Γ l, garrowfy_code_types (literalType l) = literalType(Γ:=Γ) l.
364 Axiom flatten_coercion : forall Γ Δ κ (σ τ:HaskType Γ κ) (γ:HaskCoercion Γ Δ (σ ∼∼∼ τ)),
365 HaskCoercion Γ Δ (garrowfy_code_types σ ∼∼∼ garrowfy_code_types τ).
367 (* This tries to assign a single level to the entire succedent of a judgment. If the succedent has types from different
368 * levels (should not happen) it just picks one; if the succedent has no non-None leaves (also should not happen) it
370 Definition getΓ (j:Judg) := match j with Γ > _ > _ |- _ => Γ end.
371 Definition getSuc (j:Judg) : Tree ??(LeveledHaskType (getΓ j) ★) :=
372 match j as J return Tree ??(LeveledHaskType (getΓ J) ★) with Γ > _ > _ |- s => s end.
373 Fixpoint getjlev {Γ}(tt:Tree ??(LeveledHaskType Γ ★)) : HaskLevel Γ :=
376 | T_Leaf (Some (_ @@ lev)) => lev
378 match getjlev b1 with
384 Definition unlev' {Γ} (x:LeveledHaskType Γ ★) :=
385 garrowfy_code_types (unlev x).
387 (* "n" is the maximum depth remaining AFTER flattening *)
388 Definition flatten_judgment (j:Judg) :=
389 match j as J return Judg with
390 Γ > Δ > ant |- suc =>
391 match getjlev suc with
392 | nil => Γ > Δ > mapOptionTree garrowfy_leveled_code_types ant
393 |- mapOptionTree garrowfy_leveled_code_types suc
395 | (ec::lev') => Γ > Δ > mapOptionTree garrowfy_leveled_code_types (drop_lev (ec::lev') ant)
397 (take_lev (ec::lev') ant)
398 (mapOptionTree unlev' suc) (* we know the level of all of suc *)
403 Definition boost : forall Γ Δ ant x y {lev},
404 ND Rule [] [ Γ > Δ > [x@@lev] |- [y@@lev] ] ->
405 ND Rule [ Γ > Δ > ant |- [x@@lev] ] [ Γ > Δ > ant |- [y@@lev] ].
407 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanL ].
408 eapply nd_comp; [ idtac | eapply nd_rule; apply (@RLet Γ Δ [] ant y x lev) ].
409 eapply nd_comp; [ apply nd_rlecnac | idtac ].
419 Definition postcompose' : ∀ Γ Δ ec lev a b c Σ,
420 ND Rule [] [ Γ > Δ > Σ |- [@ga_mk Γ ec a b @@ lev] ] ->
421 ND Rule [] [ Γ > Δ > Σ,,[@ga_mk Γ ec b c @@ lev] |- [@ga_mk Γ ec a c @@ lev] ].
423 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RExch ].
424 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) ].
425 eapply nd_comp; [ apply nd_llecnac | idtac ].
428 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RExch ].
432 Definition precompose' : ∀ Γ Δ ec lev a b c Σ,
433 ND Rule [] [ Γ > Δ > Σ |- [@ga_mk Γ ec b c @@ lev] ] ->
434 ND Rule [] [ Γ > Δ > Σ,,[@ga_mk Γ ec a b @@ lev] |- [@ga_mk Γ ec a c @@ lev] ].
436 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RExch ].
437 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) ].
438 eapply nd_comp; [ apply nd_llecnac | idtac ].
444 Definition postcompose : ∀ Γ Δ ec lev a b c,
445 ND Rule [] [ Γ > Δ > [] |- [@ga_mk Γ ec a b @@ lev] ] ->
446 ND Rule [] [ Γ > Δ > [@ga_mk Γ ec b c @@ lev] |- [@ga_mk Γ ec a c @@ lev] ].
456 Definition firstify : ∀ Γ Δ ec lev a b c Σ,
457 ND Rule [] [ Γ > Δ > Σ |- [@ga_mk Γ ec a b @@ lev] ] ->
458 ND Rule [] [ Γ > Δ > Σ |- [@ga_mk Γ ec (a,,c) (b,,c) @@ lev] ].
460 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanL ].
461 eapply nd_comp; [ idtac | eapply nd_rule; apply RLet ].
462 eapply nd_comp; [ apply nd_llecnac | idtac ].
465 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RuCanL ].
469 Definition secondify : ∀ Γ Δ ec lev a b c Σ,
470 ND Rule [] [ Γ > Δ > Σ |- [@ga_mk Γ ec a b @@ lev] ] ->
471 ND Rule [] [ Γ > Δ > Σ |- [@ga_mk Γ ec (c,,a) (c,,b) @@ lev] ].
473 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanL ].
474 eapply nd_comp; [ idtac | eapply nd_rule; apply RLet ].
475 eapply nd_comp; [ apply nd_llecnac | idtac ].
478 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RuCanL ].
482 Lemma ga_unkappa : ∀ Γ Δ ec l a b Σ,
484 [Γ > Δ > Σ |- [@ga_mk Γ ec a b @@ l] ]
485 [Γ > Δ > Σ,,[@ga_mk Γ ec [] a @@ l] |- [@ga_mk Γ ec [] b @@ l] ].
487 set (ga_comp Γ Δ ec l [] a b) as q.
489 set (@RLet Γ Δ) as q'.
490 set (@RLet Γ Δ [@ga_mk _ ec [] a @@ l] Σ (@ga_mk _ ec [] b) (@ga_mk _ ec a b) l) as q''.
512 Notation "` x" := (take_lev _ x) (at level 20).
513 Notation "`` x" := (mapOptionTree unlev x) (at level 20).
514 Notation "``` x" := (drop_lev _ x) (at level 20).
516 Definition garrowfy_arrangement' :
517 forall Γ (Δ:CoercionEnv Γ)
518 (ec:HaskTyVar Γ ECKind) (lev:HaskLevel Γ) (ant1 ant2:Tree ??(LeveledHaskType Γ ★)) (r:Arrange ant1 ant2),
519 ND Rule [] [Γ > Δ > [] |- [@ga_mk _ (v2t ec) (take_lev (ec :: lev) ant2) (take_lev (ec :: lev) ant1) @@ nil] ].
522 refine (fix garrowfy ant1 ant2 (r:Arrange ant1 ant2):
523 ND Rule [] [Γ > Δ > [] |- [@ga_mk _ (v2t ec) (take_lev (ec :: lev) ant2) (take_lev (ec :: lev) ant1) @@ nil]] :=
524 match r as R in Arrange A B return
525 ND Rule [] [Γ > Δ > [] |- [@ga_mk _ (v2t ec) (take_lev (ec :: lev) B) (take_lev (ec :: lev) A) @@ nil]]
527 | RCanL a => let case_RCanL := tt in ga_uncancell _ _ _ _ _
528 | RCanR a => let case_RCanR := tt in ga_uncancelr _ _ _ _ _
529 | RuCanL a => let case_RuCanL := tt in ga_cancell _ _ _ _ _
530 | RuCanR a => let case_RuCanR := tt in ga_cancelr _ _ _ _ _
531 | RAssoc a b c => let case_RAssoc := tt in ga_assoc _ _ _ _ _ _ _
532 | RCossa a b c => let case_RCossa := tt in ga_unassoc _ _ _ _ _ _ _
533 | RExch a b => let case_RExch := tt in ga_swap _ _ _ _ _ _
534 | RWeak a => let case_RWeak := tt in ga_drop _ _ _ _ _
535 | RCont a => let case_RCont := tt in ga_copy _ _ _ _ _
536 | RLeft a b c r' => let case_RLeft := tt in garrowfy _ _ r' ;; boost _ _ _ _ _ (ga_second _ _ _ _ _ _ _)
537 | RRight a b c r' => let case_RRight := tt in garrowfy _ _ r' ;; boost _ _ _ _ _ (ga_first _ _ _ _ _ _ _)
538 | RComp c b a r1 r2 => let case_RComp := tt in (fun r1' r2' => _) (garrowfy _ _ r1) (garrowfy _ _ r2)
539 end); clear garrowfy; repeat take_simplify; repeat drop_simplify; intros.
542 set (take_lev (ec :: lev) a) as a' in *.
543 set (take_lev (ec :: lev) b) as b' in *.
544 set (take_lev (ec :: lev) c) as c' in *.
545 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RCanL ].
546 eapply nd_comp; [ idtac | eapply nd_rule; apply
547 (@RLet Γ Δ [] [] (@ga_mk _ (v2t ec) a' c') (@ga_mk _ (v2t ec) a' b')) ].
548 eapply nd_comp; [ apply nd_llecnac | idtac ].
551 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RuCanL ].
552 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RCanR ].
553 eapply nd_comp; [ idtac | eapply nd_rule; apply
554 (@RLet Γ Δ [@ga_mk _ (v2t ec) a' b' @@ _] [] (@ga_mk _ (v2t ec) a' c') (@ga_mk _ (v2t ec) b' c'))].
555 eapply nd_comp; [ apply nd_llecnac | idtac ].
561 Definition garrowfy_arrangement :
562 forall Γ (Δ:CoercionEnv Γ) n
563 (ec:HaskTyVar Γ ECKind) (lev:HaskLevel Γ) (ant1 ant2:Tree ??(LeveledHaskType Γ ★)) (r:Arrange ant1 ant2) succ,
565 [Γ > Δ > mapOptionTree (garrowfy_leveled_code_types ) (drop_lev n ant1)
566 |- [@ga_mk _ (v2t ec) (take_lev (ec :: lev) ant1) (mapOptionTree (unlev' ) succ) @@ nil]]
567 [Γ > Δ > mapOptionTree (garrowfy_leveled_code_types ) (drop_lev n ant2)
568 |- [@ga_mk _ (v2t ec) (take_lev (ec :: lev) ant2) (mapOptionTree (unlev' ) succ) @@ nil]].
570 refine ( _ ;; (boost _ _ _ _ _ (postcompose _ _ _ _ _ _ _ (garrowfy_arrangement' Γ Δ ec lev ant1 ant2 r)))).
573 refine ((fix garrowfy ant1 ant2 (r:Arrange ant1 ant2) :=
574 match r as R in Arrange A B return
575 Arrange (mapOptionTree (garrowfy_leveled_code_types ) (drop_lev _ A))
576 (mapOptionTree (garrowfy_leveled_code_types ) (drop_lev _ B)) with
577 | RCanL a => let case_RCanL := tt in RCanL _
578 | RCanR a => let case_RCanR := tt in RCanR _
579 | RuCanL a => let case_RuCanL := tt in RuCanL _
580 | RuCanR a => let case_RuCanR := tt in RuCanR _
581 | RAssoc a b c => let case_RAssoc := tt in RAssoc _ _ _
582 | RCossa a b c => let case_RCossa := tt in RCossa _ _ _
583 | RExch a b => let case_RExch := tt in RExch _ _
584 | RWeak a => let case_RWeak := tt in RWeak _
585 | RCont a => let case_RCont := tt in RCont _
586 | RLeft a b c r' => let case_RLeft := tt in RLeft _ (garrowfy _ _ r')
587 | RRight a b c r' => let case_RRight := tt in RRight _ (garrowfy _ _ r')
588 | RComp a b c r1 r2 => let case_RComp := tt in RComp (garrowfy _ _ r1) (garrowfy _ _ r2)
589 end) ant1 ant2 r); clear garrowfy; repeat take_simplify; repeat drop_simplify; intros.
592 Definition flatten_arrangement :
593 forall Γ Δ ant1 ant2 succ (r:Arrange ant1 ant2),
594 ND Rule (mapOptionTree (flatten_judgment ) [Γ > Δ > ant1 |- succ])
595 (mapOptionTree (flatten_judgment ) [Γ > Δ > ant2 |- succ]).
598 set (getjlev succ) as succ_lev.
599 assert (succ_lev=getjlev succ).
617 eapply RComp; [ apply IHr1 | apply IHr2 ].
619 apply garrowfy_arrangement.
623 Definition ga_join Γ Δ Σ₁ Σ₂ a b ec :
624 ND Rule [] [Γ > Δ > Σ₁ |- [@ga_mk _ ec [] a @@ nil]] ->
625 ND Rule [] [Γ > Δ > Σ₂ |- [@ga_mk _ ec [] b @@ nil]] ->
626 ND Rule [] [Γ > Δ > Σ₁,,Σ₂ |- [@ga_mk _ ec [] (a,,b) @@ nil]].
629 apply secondify with (c:=a) in pfb.
632 eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
633 eapply nd_comp; [ eapply nd_llecnac | idtac ].
642 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanL ].
648 Definition arrange_brak : forall Γ Δ ec succ t,
650 [Γ > Δ > mapOptionTree (garrowfy_leveled_code_types ) (drop_lev (ec :: nil) succ),,
651 [(@ga_mk _ (v2t ec) [] (take_lev (ec :: nil) succ)) @@ nil] |- [(@ga_mk _ (v2t ec) [] [garrowfy_code_types t]) @@ nil]]
652 [Γ > Δ > mapOptionTree (garrowfy_leveled_code_types ) succ |- [(@ga_mk _ (v2t ec) [] [garrowfy_code_types t]) @@ nil]].
655 set (@arrange' _ succ (levelMatch (ec::nil))) as q.
656 set (arrangeMap _ _ garrowfy_leveled_code_types q) as y.
665 eapply nd_comp; [ apply nd_llecnac | idtac ].
666 eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
671 induction succ; try destruct a; simpl.
677 destruct l as [t' lev'].
678 destruct lev' as [|ec' lev'].
682 set (@eqd_dec (HaskLevel Γ) (haskLevelEqDecidable Γ) (ec' :: lev') (ec :: nil)) as q.
698 Definition arrange_esc : forall Γ Δ ec succ t,
700 [Γ > Δ > mapOptionTree (garrowfy_leveled_code_types ) succ |- [(@ga_mk _ (v2t ec) [] [garrowfy_code_types t]) @@ nil]]
701 [Γ > Δ > mapOptionTree (garrowfy_leveled_code_types ) (drop_lev (ec :: nil) succ),,
702 [(@ga_mk _ (v2t ec) [] (take_lev (ec :: nil) succ)) @@ nil] |- [(@ga_mk _ (v2t ec) [] [garrowfy_code_types t]) @@ nil]].
705 set (@arrange _ succ (levelMatch (ec::nil))) as q.
706 set (arrangeMap _ _ garrowfy_leveled_code_types q) as y.
718 unfold mkDropFlags; simpl.
722 destruct (General.list_eq_dec h0 (ec :: nil)).
724 unfold garrowfy_leveled_code_types'.
739 apply (Prelude_error "escapifying code with multi-leaf antecedents is not supported").
742 Lemma mapOptionTree_distributes
743 : forall T R (a b:Tree ??T) (f:T->R),
744 mapOptionTree f (a,,b) = (mapOptionTree f a),,(mapOptionTree f b).
748 Axiom garrowfy_commutes_with_substT :
749 forall κ Γ (Δ:CoercionEnv Γ) (σ:∀ TV, InstantiatedTypeEnv TV Γ → TV κ → RawHaskType TV ★) (τ:HaskType Γ κ),
750 garrowfy_code_types (substT σ τ) = substT (fun TV ite v => garrowfy_raw_codetypes (σ TV ite v))
751 (garrowfy_code_types τ).
753 Axiom garrowfy_commutes_with_HaskTAll :
754 forall κ Γ (Δ:CoercionEnv Γ) (σ:∀ TV, InstantiatedTypeEnv TV Γ → TV κ → RawHaskType TV ★),
755 garrowfy_code_types (HaskTAll κ σ) = HaskTAll κ (fun TV ite v => garrowfy_raw_codetypes (σ TV ite v)).
757 Axiom garrowfy_commutes_with_HaskTApp :
758 forall κ Γ (Δ:CoercionEnv Γ) (σ:∀ TV, InstantiatedTypeEnv TV Γ → TV κ → RawHaskType TV ★),
759 garrowfy_code_types (HaskTApp (weakF σ) (FreshHaskTyVar κ)) =
760 HaskTApp (weakF (fun TV ite v => garrowfy_raw_codetypes (σ TV ite v))) (FreshHaskTyVar κ).
762 Axiom garrowfy_commutes_with_weakLT : forall (Γ:TypeEnv) κ t,
763 garrowfy_leveled_code_types (weakLT(Γ:=Γ)(κ:=κ) t) = weakLT(Γ:=Γ)(κ:=κ) (garrowfy_leveled_code_types t).
765 Axiom globals_do_not_have_code_types : forall (Γ:TypeEnv) (g:Global Γ) v,
766 garrowfy_code_types (g v) = g v.
768 Definition decide_tree_empty : forall {T:Type}(t:Tree ??T),
769 sum { q:Tree unit & t = mapTree (fun _ => None) q } unit.
774 | T_Branch b1 b2 => let b1' := foo b1 in let b2' := foo b2 in _
795 Definition flatten_proof :
798 ND Rule (mapOptionTree (flatten_judgment ) h) (mapOptionTree (flatten_judgment ) c).
800 eapply nd_map'; [ idtac | apply X ].
805 refine (match X as R in Rule H C with
806 | RArrange Γ Δ a b x d => let case_RArrange := tt in _
807 | RNote Γ Δ Σ τ l n => let case_RNote := tt in _
808 | RLit Γ Δ l _ => let case_RLit := tt in _
809 | RVar Γ Δ σ lev => let case_RVar := tt in _
810 | RGlobal Γ Δ σ l wev => let case_RGlobal := tt in _
811 | RLam Γ Δ Σ tx te lev => let case_RLam := tt in _
812 | RCast Γ Δ Σ σ τ lev γ => let case_RCast := tt in _
813 | RAbsT Γ Δ Σ κ σ lev => let case_RAbsT := tt in _
814 | RAppT Γ Δ Σ κ σ τ lev => let case_RAppT := tt in _
815 | RAppCo Γ Δ Σ κ σ₁ σ₂ γ σ lev => let case_RAppCo := tt in _
816 | RAbsCo Γ Δ Σ κ σ σ₁ σ₂ lev => let case_RAbsCo := tt in _
817 | RApp Γ Δ Σ₁ Σ₂ tx te lev => let case_RApp := tt in _
818 | RLet Γ Δ Σ₁ Σ₂ σ₁ σ₂ lev => let case_RLet := tt in _
819 | RJoin Γ p lri m x q => let case_RJoin := tt in _
820 | RVoid _ _ => let case_RVoid := tt in _
821 | RBrak Γ Δ t ec succ lev => let case_RBrak := tt in _
822 | REsc Γ Δ t ec succ lev => let case_REsc := tt in _
823 | RCase Γ Δ lev tc Σ avars tbranches alts => let case_RCase := tt in _
824 | RLetRec Γ Δ lri x y t => let case_RLetRec := tt in _
827 destruct case_RArrange.
828 apply (flatten_arrangement Γ Δ a b x d).
833 change ([garrowfy_code_types (<[ ec |- t ]>) @@ nil])
834 with ([ga_mk (v2t ec) [] [garrowfy_code_types t] @@ nil]).
835 refine (ga_unkappa Γ Δ (v2t ec) nil (take_lev (ec::nil) succ) _
836 (mapOptionTree (garrowfy_leveled_code_types) (drop_lev (ec::nil) succ)) ;; _ ).
838 apply (Prelude_error "found Brak at depth >0 (a)").
844 change ([garrowfy_code_types (<[ ec |- t ]>) @@ nil])
845 with ([ga_mk (v2t ec) [] [garrowfy_code_types t] @@ nil]).
846 eapply nd_comp; [ apply arrange_esc | idtac ].
847 set (decide_tree_empty (take_lev (ec :: nil) succ)) as q'.
853 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanR ].
854 eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
855 eapply nd_comp; [ apply nd_llecnac | idtac ].
856 apply nd_prod; [ idtac | eapply boost ].
859 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanR ].
868 (* environment has non-empty leaves *)
869 apply (ga_kappa Γ Δ (v2t ec) nil (take_lev (ec::nil) succ) _ _).
870 apply (Prelude_error "found Esc at depth >0 (a)").
875 apply nd_rule; apply RNote; auto.
876 apply nd_rule; apply RNote; auto.
881 rewrite literal_types_unchanged.
882 apply nd_rule; apply RLit.
883 unfold take_lev; simpl.
884 unfold drop_lev; simpl.
887 rewrite literal_types_unchanged.
891 Opaque flatten_judgment.
893 Transparent flatten_judgment.
895 unfold flatten_judgment.
898 apply nd_rule. apply RVar.
899 repeat drop_simplify.
901 repeat take_simplify.
905 destruct case_RGlobal.
909 destruct l as [|ec lev]; simpl.
910 destruct (eqd_dec (g:CoreVar) (hetmet_flatten:CoreVar)).
911 set (garrowfy_code_types (g wev)) as t.
912 set (RGlobal _ Δ nil (mkGlobal Γ t hetmet_id)) as q.
917 apply nd_rule; rewrite globals_do_not_have_code_types.
919 apply (Prelude_error "found RGlobal at depth >0").
925 destruct lev as [|ec lev]; simpl; [ apply nd_rule; apply RLam; auto | idtac ].
926 repeat drop_simplify.
927 repeat take_simplify.
938 destruct lev as [|ec lev]; simpl; [ apply nd_rule; apply RCast; auto | idtac ].
939 apply flatten_coercion; auto.
940 apply (Prelude_error "RCast at level >0").
944 destruct (getjlev x); destruct (getjlev q).
947 apply (Prelude_error "RJoin at depth >0").
948 apply (Prelude_error "RJoin at depth >0").
949 apply (Prelude_error "RJoin at depth >0").
954 destruct lev as [|ec lev]. simpl. apply nd_rule.
955 replace (garrowfy_code_types (tx ---> te)) with ((garrowfy_code_types tx) ---> (garrowfy_code_types te)).
959 repeat drop_simplify.
960 repeat take_simplify.
961 rewrite mapOptionTree_distributes.
962 set (mapOptionTree (garrowfy_leveled_code_types ) (drop_lev (ec :: lev) Σ₁)) as Σ₁'.
963 set (mapOptionTree (garrowfy_leveled_code_types ) (drop_lev (ec :: lev) Σ₂)) as Σ₂'.
964 set (take_lev (ec :: lev) Σ₁) as Σ₁''.
965 set (take_lev (ec :: lev) Σ₂) as Σ₂''.
966 replace (garrowfy_code_types (tx ---> te)) with ((garrowfy_code_types tx) ---> (garrowfy_code_types te)).
967 apply (Prelude_error "FIXME: ga_apply").
970 Notation "` x" := (take_lev _ x) (at level 20).
971 Notation "`` x" := (mapOptionTree unlev x) (at level 20).
972 Notation "``` x" := ((drop_lev _ x)) (at level 20).
973 Notation "!<[]> x" := (garrowfy_code_types _ x) (at level 1).
974 Notation "!<[@]>" := (garrowfy_leveled_code_types _) (at level 1).
977 apply (Prelude_error "FIXME: RLet").
980 destruct lev as [|ec lev]; simpl; [ apply nd_rule; apply RLet; auto | idtac ].
981 destruct (Peano_dec.eq_nat_dec (Datatypes.length lev) n); [ idtac | apply nd_rule; apply RLet; auto ]; simpl.
982 repeat drop_simplify.
983 repeat take_simplify.
986 rewrite mapOptionTree_distributes.
987 rewrite mapOptionTree_distributes.
988 set (mapOptionTree (garrowfy_leveled_code_types (S n)) (drop_lev (ec :: lev) Σ₁)) as A.
989 set (take_lev (ec :: lev) Σ₁) as A'.
990 set (mapOptionTree (garrowfy_leveled_code_types (S n)) (drop_lev (ec :: lev) Σ₂)) as B.
991 set (take_lev (ec :: lev) Σ₂) as B'.
1034 destruct case_RVoid.
1039 destruct case_RAppT.
1040 simpl. destruct lev; simpl.
1041 rewrite garrowfy_commutes_with_HaskTAll.
1042 rewrite garrowfy_commutes_with_substT.
1047 apply (Prelude_error "ga_apply").
1049 destruct case_RAbsT.
1050 simpl. destruct lev; simpl.
1051 rewrite garrowfy_commutes_with_HaskTAll.
1052 rewrite garrowfy_commutes_with_HaskTApp.
1053 eapply nd_comp; [ idtac | eapply nd_rule; eapply RAbsT ].
1055 set (mapOptionTree (garrowfy_leveled_code_types ) (mapOptionTree (weakLT(κ:=κ)) Σ)) as a.
1056 set (mapOptionTree (weakLT(κ:=κ)) (mapOptionTree (garrowfy_leveled_code_types ) Σ)) as q'.
1064 rewrite garrowfy_commutes_with_weakLT.
1075 apply (Prelude_error "AbsT at depth>0").
1077 destruct case_RAppCo.
1078 simpl. destruct lev; simpl.
1079 unfold garrowfy_code_types.
1083 apply flatten_coercion.
1085 apply (Prelude_error "AppCo at depth>0").
1087 destruct case_RAbsCo.
1088 simpl. destruct lev; simpl.
1089 unfold garrowfy_code_types.
1091 apply (Prelude_error "AbsCo not supported (FIXME)").
1092 apply (Prelude_error "AbsCo at depth>0").
1094 destruct case_RLetRec.
1096 apply (Prelude_error "LetRec not supported (FIXME)").
1098 destruct case_RCase.
1100 apply (Prelude_error "Case not supported (FIXME)").
1104 (* to do: establish some metric on judgments (max length of level of any succedent type, probably), show how to
1105 * calculate it, and show that the flattening procedure above drives it down by one *)
1108 Instance FlatteningFunctor {Γ}{Δ}{ec} : Functor (JudgmentsL (PCF Γ Δ ec)) (TypesL (SystemFCa Γ Δ)) (obact) :=
1109 { fmor := FlatteningFunctor_fmor }.
1111 Definition ReificationFunctor Γ Δ : Functor (JudgmentsL _ _ (PCF n Γ Δ)) SystemFCa' (mapOptionTree brakifyJudg).
1112 refine {| fmor := ReificationFunctor_fmor Γ Δ |}; unfold hom; unfold ob; simpl ; intros.
1114 Definition PCF_SMME (n:nat)(Γ:TypeEnv)(Δ:CoercionEnv Γ) : ProgrammingLanguageSMME.
1115 refine {| plsmme_pl := PCF n Γ Δ |}.
1118 Definition SystemFCa_SMME (n:nat)(Γ:TypeEnv)(Δ:CoercionEnv Γ) : ProgrammingLanguageSMME.
1119 refine {| plsmme_pl := SystemFCa n Γ Δ |}.
1122 Definition ReificationFunctorMonoidal n : MonoidalFunctor (JudgmentsN n) (JudgmentsN (S n)) (ReificationFunctor n).
1126 Definition PCF_SystemFCa_two_level n Γ Δ : TwoLevelLanguage (PCF_SMME n Γ Δ) (SystemFCa_SMME (S n) Γ Δ).
1129 (* ... and the retraction exists *)
1133 Implicit Arguments garrow [ ].