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.
34 Set Printing Width 130.
37 * The flattening transformation. Currently only TWO-level languages are
38 * supported, and the level-1 sublanguage is rather limited.
40 * This file abuses terminology pretty badly. For purposes of this file,
41 * "PCF" means "the level-1 sublanguage" and "FC" (aka System FC) means
42 * the whole language (level-0 language including bracketed level-1 terms)
44 Section HaskFlattener.
47 forall {T} (Σ:Tree ??T) (f:T -> bool),
48 Arrange Σ (dropT (mkFlags (liftBoolFunc false f) Σ),,( (dropT (mkFlags (liftBoolFunc false (bnot ○ f)) Σ)))).
54 destruct (f t); simpl.
60 eapply RComp; [ idtac | apply arrangeSwapMiddle ].
69 forall {T} (Σ:Tree ??T) (f:T -> bool),
70 Arrange (dropT (mkFlags (liftBoolFunc false f) Σ),,( (dropT (mkFlags (liftBoolFunc false (bnot ○ f)) Σ)))) Σ.
76 destruct (f t); simpl.
82 eapply RComp; [ apply arrangeSwapMiddle | idtac ].
92 | [ |- context[@eqd_dec ?T ?V ?X ?X] ] =>
93 destruct (@eqd_dec T V X X) as [eqd_dec1 | eqd_dec2];
94 [ clear eqd_dec1 | set (eqd_dec2 (refl_equal _)) as eqd_dec2'; inversion eqd_dec2' ]
97 Context (hetmet_flatten : WeakExprVar).
98 Context (hetmet_unflatten : WeakExprVar).
99 Context (hetmet_id : WeakExprVar).
100 Context {unitTy : forall TV, RawHaskType TV ★ }.
101 Context {prodTy : forall TV, RawHaskType TV ★ -> RawHaskType TV ★ -> RawHaskType TV ★ }.
102 Context {gaTy : forall TV, RawHaskType TV ECKind -> RawHaskType TV ★ -> RawHaskType TV ★ -> RawHaskType TV ★ }.
104 Definition ga_mk_tree {Γ} (tr:Tree ??(HaskType Γ ★)) : HaskType Γ ★ :=
105 fun TV ite => reduceTree (unitTy TV) (prodTy TV) (mapOptionTree (fun x => x TV ite) tr).
107 Definition ga_mk {Γ}(ec:HaskType Γ ECKind )(ant suc:Tree ??(HaskType Γ ★)) : HaskType Γ ★ :=
108 fun TV ite => gaTy TV (ec TV ite) (ga_mk_tree ant TV ite) (ga_mk_tree suc TV ite).
111 { ga_id : ∀ Γ Δ ec l a , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec a a @@ l] ]
112 ; ga_cancelr : ∀ Γ Δ ec l a , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec (a,,[]) a @@ l] ]
113 ; ga_cancell : ∀ Γ Δ ec l a , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec ([],,a) a @@ l] ]
114 ; ga_uncancelr : ∀ Γ Δ ec l a , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec a (a,,[]) @@ l] ]
115 ; ga_uncancell : ∀ Γ Δ ec l a , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec a ([],,a) @@ l] ]
116 ; ga_assoc : ∀ Γ Δ ec l a b c, ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec ((a,,b),,c) (a,,(b,,c)) @@ l] ]
117 ; ga_unassoc : ∀ Γ Δ ec l a b c, ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec (a,,(b,,c)) ((a,,b),,c) @@ l] ]
118 ; ga_swap : ∀ Γ Δ ec l a b , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec (a,,b) (b,,a) @@ l] ]
119 ; ga_drop : ∀ Γ Δ ec l a , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec a [] @@ l] ]
120 ; ga_copy : ∀ Γ Δ ec l a , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec a (a,,a) @@ l] ]
121 ; ga_first : ∀ Γ Δ ec l a b x, ND Rule [] [Γ > Δ > [@ga_mk Γ ec a b @@ l] |- [@ga_mk Γ ec (a,,x) (b,,x) @@ l] ]
122 ; ga_second : ∀ Γ Δ ec l a b x, ND Rule [] [Γ > Δ > [@ga_mk Γ ec a b @@ l] |- [@ga_mk Γ ec (x,,a) (x,,b) @@ l] ]
123 ; ga_lit : ∀ Γ Δ ec l lit , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec [] [literalType lit] @@ l] ]
124 ; ga_curry : ∀ Γ Δ ec l a b c, ND Rule [] [Γ > Δ > [@ga_mk Γ ec (a,,[b]) [c] @@ l] |- [@ga_mk Γ ec a [b ---> c] @@ l] ]
125 ; 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] ]
126 ; ga_apply : ∀ Γ Δ ec l a a' b c, ND Rule []
127 [Γ > Δ > [@ga_mk Γ ec a [b ---> c] @@ l],,[@ga_mk Γ ec a' [b] @@ l] |- [@ga_mk Γ ec (a,,a') [c] @@ l] ]
128 ; ga_kappa : ∀ Γ Δ ec l a b Σ, ND Rule
129 [Γ > Δ > Σ,,[@ga_mk Γ ec [] a @@ l] |- [@ga_mk Γ ec [] b @@ l] ]
130 [Γ > Δ > Σ |- [@ga_mk Γ ec a b @@ l] ]
132 Context `(gar:garrow).
134 Notation "a ~~~~> b" := (@ga_mk _ _ a b) (at level 20).
138 * - code types <[t]>@c become garrows c () t
139 * - free variables of type t at a level lev deeper than the succedent become garrows c () t
140 * - free variables at the level of the succedent become
142 Fixpoint garrowfy_raw_codetypes {TV}{κ}(exp: RawHaskType TV κ) : RawHaskType TV κ :=
145 | TAll _ y => TAll _ (fun v => garrowfy_raw_codetypes (y v))
146 | TApp _ _ x y => TApp (garrowfy_raw_codetypes x) (garrowfy_raw_codetypes y)
148 | TCoerc _ t1 t2 t => TCoerc (garrowfy_raw_codetypes t1) (garrowfy_raw_codetypes t2)
149 (garrowfy_raw_codetypes t)
151 | TCode v e => gaTy TV v (unitTy TV) (garrowfy_raw_codetypes e)
152 | TyFunApp tfc kl k lt => TyFunApp tfc kl k (garrowfy_raw_codetypes_list _ lt)
154 with garrowfy_raw_codetypes_list {TV}(lk:list Kind)(exp:@RawHaskTypeList TV lk) : @RawHaskTypeList TV lk :=
155 match exp in @RawHaskTypeList _ LK return @RawHaskTypeList TV LK with
156 | TyFunApp_nil => TyFunApp_nil
157 | TyFunApp_cons κ kl t rest => TyFunApp_cons _ _ (garrowfy_raw_codetypes t) (garrowfy_raw_codetypes_list _ rest)
159 Definition garrowfy_code_types {Γ}{κ}(ht:HaskType Γ κ) : HaskType Γ κ :=
161 garrowfy_raw_codetypes (ht TV ite).
163 Definition v2t {Γ}(ec:HaskTyVar Γ ECKind) := fun TV ite => TVar (ec TV ite).
165 Fixpoint garrowfy_leveled_code_types' {Γ}(ht:HaskType Γ ★)(lev:HaskLevel Γ) : HaskType Γ ★ :=
167 | nil => garrowfy_code_types ht
168 | ec::lev' => @ga_mk _ (v2t ec) [] [garrowfy_leveled_code_types' ht lev']
171 Definition garrowfy_leveled_code_types {Γ}(ht:LeveledHaskType Γ ★) : LeveledHaskType Γ ★ :=
174 garrowfy_leveled_code_types' htt lev @@ nil
177 Definition levelMatch {Γ}(lev:HaskLevel Γ) : LeveledHaskType Γ ★ -> bool :=
178 fun t => match t with ttype@@tlev => if eqd_dec tlev lev then true else false end.
180 (* In a tree of types, replace any type at depth "lev" or greater None *)
181 Definition mkDropFlags {Γ}(lev:HaskLevel Γ)(tt:Tree ??(LeveledHaskType Γ ★)) : TreeFlags tt :=
182 mkFlags (liftBoolFunc false (levelMatch lev)) tt.
184 Definition drop_lev {Γ}(lev:HaskLevel Γ)(tt:Tree ??(LeveledHaskType Γ ★)) : Tree ??(LeveledHaskType Γ ★) :=
185 dropT (mkDropFlags lev tt).
187 (* The opposite: replace any type which is NOT at level "lev" with None *)
188 Definition mkTakeFlags {Γ}(lev:HaskLevel Γ)(tt:Tree ??(LeveledHaskType Γ ★)) : TreeFlags tt :=
189 mkFlags (liftBoolFunc true (bnot ○ levelMatch lev)) tt.
191 Definition take_lev {Γ}(lev:HaskLevel Γ)(tt:Tree ??(LeveledHaskType Γ ★)) : Tree ??(HaskType Γ ★) :=
192 mapOptionTree (fun x => garrowfy_code_types (unlev x)) (dropT (mkTakeFlags lev tt)).
194 mapOptionTree (fun x => garrowfy_code_types (unlev x))
195 (maybeTree (takeT tt (mkFlags (
196 fun t => match t with
197 | Some (ttype @@ tlev) => if eqd_dec tlev lev then true else false
202 Definition maybeTree {T}(t:??(Tree ??T)) : Tree ??T :=
209 Lemma drop_lev_lemma : forall Γ (lev:HaskLevel Γ) x, drop_lev lev [x @@ lev] = [].
221 Lemma drop_lev_lemma_s : forall Γ (lev:HaskLevel Γ) ec x, drop_lev (ec::lev) [x @@ (ec :: lev)] = [].
232 Lemma take_lemma : forall Γ (lev:HaskLevel Γ) x, take_lev lev [x @@ lev] = [garrowfy_code_types x].
243 Ltac drop_simplify :=
245 | [ |- context[@drop_lev ?G ?L [ ?X @@ ?L ] ] ] =>
246 rewrite (drop_lev_lemma G L X)
247 | [ |- context[@drop_lev ?G (?E :: ?L) [ ?X @@ (?E :: ?L) ] ] ] =>
248 rewrite (drop_lev_lemma_s G L E X)
249 | [ |- context[@drop_lev ?G ?N (?A,,?B)] ] =>
250 change (@drop_lev G N (A,,B)) with ((@drop_lev G N A),,(@drop_lev G N B))
251 | [ |- context[@drop_lev ?G ?N (T_Leaf None)] ] =>
252 change (@drop_lev G N (T_Leaf (@None (LeveledHaskType G ★)))) with (T_Leaf (@None (LeveledHaskType G ★)))
255 Ltac take_simplify :=
257 | [ |- context[@take_lev ?G ?L [ ?X @@ ?L ] ] ] =>
258 rewrite (take_lemma G L X)
259 | [ |- context[@take_lev ?G ?N (?A,,?B)] ] =>
260 change (@take_lev G N (A,,B)) with ((@take_lev G N A),,(@take_lev G N B))
261 | [ |- context[@take_lev ?G ?N (T_Leaf None)] ] =>
262 change (@take_lev G N (T_Leaf (@None (LeveledHaskType G ★)))) with (T_Leaf (@None (LeveledHaskType G ★)))
267 Axiom literal_types_unchanged : forall Γ l, garrowfy_code_types (literalType l) = literalType(Γ:=Γ) l.
269 Axiom flatten_coercion : forall Γ Δ κ (σ τ:HaskType Γ κ) (γ:HaskCoercion Γ Δ (σ ∼∼∼ τ)),
270 HaskCoercion Γ Δ (garrowfy_code_types σ ∼∼∼ garrowfy_code_types τ).
272 Axiom garrowfy_commutes_with_substT :
273 forall κ Γ (Δ:CoercionEnv Γ) (σ:∀ TV, InstantiatedTypeEnv TV Γ → TV κ → RawHaskType TV ★) (τ:HaskType Γ κ),
274 garrowfy_code_types (substT σ τ) = substT (fun TV ite v => garrowfy_raw_codetypes (σ TV ite v))
275 (garrowfy_code_types τ).
277 Axiom garrowfy_commutes_with_HaskTAll :
278 forall κ Γ (Δ:CoercionEnv Γ) (σ:∀ TV, InstantiatedTypeEnv TV Γ → TV κ → RawHaskType TV ★),
279 garrowfy_code_types (HaskTAll κ σ) = HaskTAll κ (fun TV ite v => garrowfy_raw_codetypes (σ TV ite v)).
281 Axiom garrowfy_commutes_with_HaskTApp :
282 forall κ Γ (Δ:CoercionEnv Γ) (σ:∀ TV, InstantiatedTypeEnv TV Γ → TV κ → RawHaskType TV ★),
283 garrowfy_code_types (HaskTApp (weakF σ) (FreshHaskTyVar κ)) =
284 HaskTApp (weakF (fun TV ite v => garrowfy_raw_codetypes (σ TV ite v))) (FreshHaskTyVar κ).
286 Axiom garrowfy_commutes_with_weakLT : forall (Γ:TypeEnv) κ t,
287 garrowfy_leveled_code_types (weakLT(Γ:=Γ)(κ:=κ) t) = weakLT(Γ:=Γ)(κ:=κ) (garrowfy_leveled_code_types t).
289 Axiom globals_do_not_have_code_types : forall (Γ:TypeEnv) (g:Global Γ) v,
290 garrowfy_code_types (g v) = g v.
292 (* This tries to assign a single level to the entire succedent of a judgment. If the succedent has types from different
293 * levels (should not happen) it just picks one; if the succedent has no non-None leaves (also should not happen) it
295 Definition getΓ (j:Judg) := match j with Γ > _ > _ |- _ => Γ end.
296 Definition getSuc (j:Judg) : Tree ??(LeveledHaskType (getΓ j) ★) :=
297 match j as J return Tree ??(LeveledHaskType (getΓ J) ★) with Γ > _ > _ |- s => s end.
298 Fixpoint getjlev {Γ}(tt:Tree ??(LeveledHaskType Γ ★)) : HaskLevel Γ :=
301 | T_Leaf (Some (_ @@ lev)) => lev
303 match getjlev b1 with
309 Definition unlev' {Γ} (x:LeveledHaskType Γ ★) :=
310 garrowfy_code_types (unlev x).
312 (* "n" is the maximum depth remaining AFTER flattening *)
313 Definition flatten_judgment (j:Judg) :=
314 match j as J return Judg with
315 Γ > Δ > ant |- suc =>
316 match getjlev suc with
317 | nil => Γ > Δ > mapOptionTree garrowfy_leveled_code_types ant
318 |- mapOptionTree garrowfy_leveled_code_types suc
320 | (ec::lev') => Γ > Δ > mapOptionTree garrowfy_leveled_code_types (drop_lev (ec::lev') ant)
322 (take_lev (ec::lev') ant)
323 (mapOptionTree unlev' suc) (* we know the level of all of suc *)
328 Definition boost : forall Γ Δ ant x y {lev},
329 ND Rule [] [ Γ > Δ > [x@@lev] |- [y@@lev] ] ->
330 ND Rule [ Γ > Δ > ant |- [x@@lev] ] [ Γ > Δ > ant |- [y@@lev] ].
332 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanL ].
333 eapply nd_comp; [ idtac | eapply nd_rule; apply (@RLet Γ Δ [] ant y x lev) ].
334 eapply nd_comp; [ apply nd_rlecnac | idtac ].
344 Definition postcompose' : ∀ Γ Δ ec lev a b c Σ,
345 ND Rule [] [ Γ > Δ > Σ |- [@ga_mk Γ ec a b @@ lev] ] ->
346 ND Rule [] [ Γ > Δ > Σ,,[@ga_mk Γ ec b c @@ lev] |- [@ga_mk Γ ec a c @@ lev] ].
348 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RExch ].
349 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) ].
350 eapply nd_comp; [ apply nd_llecnac | idtac ].
353 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RExch ].
357 Definition precompose' : ∀ Γ Δ ec lev a b c Σ,
358 ND Rule [] [ Γ > Δ > Σ |- [@ga_mk Γ ec b c @@ lev] ] ->
359 ND Rule [] [ Γ > Δ > Σ,,[@ga_mk Γ ec a b @@ lev] |- [@ga_mk Γ ec a c @@ lev] ].
361 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RExch ].
362 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) ].
363 eapply nd_comp; [ apply nd_llecnac | idtac ].
369 Definition postcompose : ∀ Γ Δ ec lev a b c,
370 ND Rule [] [ Γ > Δ > [] |- [@ga_mk Γ ec a b @@ lev] ] ->
371 ND Rule [] [ Γ > Δ > [@ga_mk Γ ec b c @@ lev] |- [@ga_mk Γ ec a c @@ lev] ].
381 Definition firstify : ∀ Γ Δ ec lev a b c Σ,
382 ND Rule [] [ Γ > Δ > Σ |- [@ga_mk Γ ec a b @@ lev] ] ->
383 ND Rule [] [ Γ > Δ > Σ |- [@ga_mk Γ ec (a,,c) (b,,c) @@ lev] ].
385 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanL ].
386 eapply nd_comp; [ idtac | eapply nd_rule; apply RLet ].
387 eapply nd_comp; [ apply nd_llecnac | idtac ].
390 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RuCanL ].
394 Definition secondify : ∀ Γ Δ ec lev a b c Σ,
395 ND Rule [] [ Γ > Δ > Σ |- [@ga_mk Γ ec a b @@ lev] ] ->
396 ND Rule [] [ Γ > Δ > Σ |- [@ga_mk Γ ec (c,,a) (c,,b) @@ lev] ].
398 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanL ].
399 eapply nd_comp; [ idtac | eapply nd_rule; apply RLet ].
400 eapply nd_comp; [ apply nd_llecnac | idtac ].
403 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RuCanL ].
407 Lemma ga_unkappa : ∀ Γ Δ ec l a b Σ,
409 [Γ > Δ > Σ |- [@ga_mk Γ ec a b @@ l] ]
410 [Γ > Δ > Σ,,[@ga_mk Γ ec [] a @@ l] |- [@ga_mk Γ ec [] b @@ l] ].
412 set (ga_comp Γ Δ ec l [] a b) as q.
414 set (@RLet Γ Δ) as q'.
415 set (@RLet Γ Δ [@ga_mk _ ec [] a @@ l] Σ (@ga_mk _ ec [] b) (@ga_mk _ ec a b) l) as q''.
436 (* useful for cutting down on the pretty-printed noise
438 Notation "` x" := (take_lev _ x) (at level 20).
439 Notation "`` x" := (mapOptionTree unlev x) (at level 20).
440 Notation "``` x" := (drop_lev _ x) (at level 20).
442 Definition garrowfy_arrangement' :
443 forall Γ (Δ:CoercionEnv Γ)
444 (ec:HaskTyVar Γ ECKind) (lev:HaskLevel Γ) (ant1 ant2:Tree ??(LeveledHaskType Γ ★)) (r:Arrange ant1 ant2),
445 ND Rule [] [Γ > Δ > [] |- [@ga_mk _ (v2t ec) (take_lev (ec :: lev) ant2) (take_lev (ec :: lev) ant1) @@ nil] ].
448 refine (fix garrowfy ant1 ant2 (r:Arrange ant1 ant2):
449 ND Rule [] [Γ > Δ > [] |- [@ga_mk _ (v2t ec) (take_lev (ec :: lev) ant2) (take_lev (ec :: lev) ant1) @@ nil]] :=
450 match r as R in Arrange A B return
451 ND Rule [] [Γ > Δ > [] |- [@ga_mk _ (v2t ec) (take_lev (ec :: lev) B) (take_lev (ec :: lev) A) @@ nil]]
453 | RCanL a => let case_RCanL := tt in ga_uncancell _ _ _ _ _
454 | RCanR a => let case_RCanR := tt in ga_uncancelr _ _ _ _ _
455 | RuCanL a => let case_RuCanL := tt in ga_cancell _ _ _ _ _
456 | RuCanR a => let case_RuCanR := tt in ga_cancelr _ _ _ _ _
457 | RAssoc a b c => let case_RAssoc := tt in ga_assoc _ _ _ _ _ _ _
458 | RCossa a b c => let case_RCossa := tt in ga_unassoc _ _ _ _ _ _ _
459 | RExch a b => let case_RExch := tt in ga_swap _ _ _ _ _ _
460 | RWeak a => let case_RWeak := tt in ga_drop _ _ _ _ _
461 | RCont a => let case_RCont := tt in ga_copy _ _ _ _ _
462 | RLeft a b c r' => let case_RLeft := tt in garrowfy _ _ r' ;; boost _ _ _ _ _ (ga_second _ _ _ _ _ _ _)
463 | RRight a b c r' => let case_RRight := tt in garrowfy _ _ r' ;; boost _ _ _ _ _ (ga_first _ _ _ _ _ _ _)
464 | RComp c b a r1 r2 => let case_RComp := tt in (fun r1' r2' => _) (garrowfy _ _ r1) (garrowfy _ _ r2)
465 end); clear garrowfy; repeat take_simplify; repeat drop_simplify; intros.
468 set (take_lev (ec :: lev) a) as a' in *.
469 set (take_lev (ec :: lev) b) as b' in *.
470 set (take_lev (ec :: lev) c) as c' in *.
471 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RCanL ].
472 eapply nd_comp; [ idtac | eapply nd_rule; apply
473 (@RLet Γ Δ [] [] (@ga_mk _ (v2t ec) a' c') (@ga_mk _ (v2t ec) a' b')) ].
474 eapply nd_comp; [ apply nd_llecnac | idtac ].
477 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RuCanL ].
478 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RCanR ].
479 eapply nd_comp; [ idtac | eapply nd_rule; apply
480 (@RLet Γ Δ [@ga_mk _ (v2t ec) a' b' @@ _] [] (@ga_mk _ (v2t ec) a' c') (@ga_mk _ (v2t ec) b' c'))].
481 eapply nd_comp; [ apply nd_llecnac | idtac ].
487 Definition garrowfy_arrangement :
488 forall Γ (Δ:CoercionEnv Γ) n
489 (ec:HaskTyVar Γ ECKind) (lev:HaskLevel Γ) (ant1 ant2:Tree ??(LeveledHaskType Γ ★)) (r:Arrange ant1 ant2) succ,
491 [Γ > Δ > mapOptionTree (garrowfy_leveled_code_types ) (drop_lev n ant1)
492 |- [@ga_mk _ (v2t ec) (take_lev (ec :: lev) ant1) (mapOptionTree (unlev' ) succ) @@ nil]]
493 [Γ > Δ > mapOptionTree (garrowfy_leveled_code_types ) (drop_lev n ant2)
494 |- [@ga_mk _ (v2t ec) (take_lev (ec :: lev) ant2) (mapOptionTree (unlev' ) succ) @@ nil]].
496 refine ( _ ;; (boost _ _ _ _ _ (postcompose _ _ _ _ _ _ _ (garrowfy_arrangement' Γ Δ ec lev ant1 ant2 r)))).
499 refine ((fix garrowfy ant1 ant2 (r:Arrange ant1 ant2) :=
500 match r as R in Arrange A B return
501 Arrange (mapOptionTree (garrowfy_leveled_code_types ) (drop_lev _ A))
502 (mapOptionTree (garrowfy_leveled_code_types ) (drop_lev _ B)) with
503 | RCanL a => let case_RCanL := tt in RCanL _
504 | RCanR a => let case_RCanR := tt in RCanR _
505 | RuCanL a => let case_RuCanL := tt in RuCanL _
506 | RuCanR a => let case_RuCanR := tt in RuCanR _
507 | RAssoc a b c => let case_RAssoc := tt in RAssoc _ _ _
508 | RCossa a b c => let case_RCossa := tt in RCossa _ _ _
509 | RExch a b => let case_RExch := tt in RExch _ _
510 | RWeak a => let case_RWeak := tt in RWeak _
511 | RCont a => let case_RCont := tt in RCont _
512 | RLeft a b c r' => let case_RLeft := tt in RLeft _ (garrowfy _ _ r')
513 | RRight a b c r' => let case_RRight := tt in RRight _ (garrowfy _ _ r')
514 | RComp a b c r1 r2 => let case_RComp := tt in RComp (garrowfy _ _ r1) (garrowfy _ _ r2)
515 end) ant1 ant2 r); clear garrowfy; repeat take_simplify; repeat drop_simplify; intros.
518 Definition flatten_arrangement :
519 forall Γ Δ ant1 ant2 succ (r:Arrange ant1 ant2),
520 ND Rule (mapOptionTree (flatten_judgment ) [Γ > Δ > ant1 |- succ])
521 (mapOptionTree (flatten_judgment ) [Γ > Δ > ant2 |- succ]).
524 set (getjlev succ) as succ_lev.
525 assert (succ_lev=getjlev succ).
543 eapply RComp; [ apply IHr1 | apply IHr2 ].
545 apply garrowfy_arrangement.
549 Definition ga_join Γ Δ Σ₁ Σ₂ a b ec :
550 ND Rule [] [Γ > Δ > Σ₁ |- [@ga_mk _ ec [] a @@ nil]] ->
551 ND Rule [] [Γ > Δ > Σ₂ |- [@ga_mk _ ec [] b @@ nil]] ->
552 ND Rule [] [Γ > Δ > Σ₁,,Σ₂ |- [@ga_mk _ ec [] (a,,b) @@ nil]].
555 apply secondify with (c:=a) in pfb.
558 eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
559 eapply nd_comp; [ eapply nd_llecnac | idtac ].
568 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanL ].
574 Definition arrange_brak : forall Γ Δ ec succ t,
576 [Γ > Δ > mapOptionTree (garrowfy_leveled_code_types ) (drop_lev (ec :: nil) succ),,
577 [(@ga_mk _ (v2t ec) [] (take_lev (ec :: nil) succ)) @@ nil] |- [(@ga_mk _ (v2t ec) [] [garrowfy_code_types t]) @@ nil]]
578 [Γ > Δ > mapOptionTree (garrowfy_leveled_code_types ) succ |- [(@ga_mk _ (v2t ec) [] [garrowfy_code_types t]) @@ nil]].
581 set (@arrange' _ succ (levelMatch (ec::nil))) as q.
582 set (arrangeMap _ _ garrowfy_leveled_code_types q) as y.
591 eapply nd_comp; [ apply nd_llecnac | idtac ].
592 eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
597 induction succ; try destruct a; simpl.
603 destruct l as [t' lev'].
604 destruct lev' as [|ec' lev'].
608 set (@eqd_dec (HaskLevel Γ) (haskLevelEqDecidable Γ) (ec' :: lev') (ec :: nil)) as q.
624 Definition arrange_esc : forall Γ Δ ec succ t,
626 [Γ > Δ > mapOptionTree (garrowfy_leveled_code_types ) succ |- [(@ga_mk _ (v2t ec) [] [garrowfy_code_types t]) @@ nil]]
627 [Γ > Δ > mapOptionTree (garrowfy_leveled_code_types ) (drop_lev (ec :: nil) succ),,
628 [(@ga_mk _ (v2t ec) [] (take_lev (ec :: nil) succ)) @@ nil] |- [(@ga_mk _ (v2t ec) [] [garrowfy_code_types t]) @@ nil]].
631 set (@arrange _ succ (levelMatch (ec::nil))) as q.
632 set (arrangeMap _ _ garrowfy_leveled_code_types q) as y.
644 unfold mkDropFlags; simpl.
648 destruct (General.list_eq_dec h0 (ec :: nil)).
650 unfold garrowfy_leveled_code_types'.
665 apply (Prelude_error "escapifying code with multi-leaf antecedents is not supported").
668 Lemma mapOptionTree_distributes
669 : forall T R (a b:Tree ??T) (f:T->R),
670 mapOptionTree f (a,,b) = (mapOptionTree f a),,(mapOptionTree f b).
674 Definition decide_tree_empty : forall {T:Type}(t:Tree ??T),
675 sum { q:Tree unit & t = mapTree (fun _ => None) q } unit.
680 | T_Branch b1 b2 => let b1' := foo b1 in let b2' := foo b2 in _
701 Definition flatten_proof :
704 ND Rule (mapOptionTree (flatten_judgment ) h) (mapOptionTree (flatten_judgment ) c).
706 eapply nd_map'; [ idtac | apply X ].
711 refine (match X as R in Rule H C with
712 | RArrange Γ Δ a b x d => let case_RArrange := tt in _
713 | RNote Γ Δ Σ τ l n => let case_RNote := tt in _
714 | RLit Γ Δ l _ => let case_RLit := tt in _
715 | RVar Γ Δ σ lev => let case_RVar := tt in _
716 | RGlobal Γ Δ σ l wev => let case_RGlobal := tt in _
717 | RLam Γ Δ Σ tx te lev => let case_RLam := tt in _
718 | RCast Γ Δ Σ σ τ lev γ => let case_RCast := tt in _
719 | RAbsT Γ Δ Σ κ σ lev => let case_RAbsT := tt in _
720 | RAppT Γ Δ Σ κ σ τ lev => let case_RAppT := tt in _
721 | RAppCo Γ Δ Σ κ σ₁ σ₂ γ σ lev => let case_RAppCo := tt in _
722 | RAbsCo Γ Δ Σ κ σ σ₁ σ₂ lev => let case_RAbsCo := tt in _
723 | RApp Γ Δ Σ₁ Σ₂ tx te lev => let case_RApp := tt in _
724 | RLet Γ Δ Σ₁ Σ₂ σ₁ σ₂ lev => let case_RLet := tt in _
725 | RJoin Γ p lri m x q => let case_RJoin := tt in _
726 | RVoid _ _ => let case_RVoid := tt in _
727 | RBrak Γ Δ t ec succ lev => let case_RBrak := tt in _
728 | REsc Γ Δ t ec succ lev => let case_REsc := tt in _
729 | RCase Γ Δ lev tc Σ avars tbranches alts => let case_RCase := tt in _
730 | RLetRec Γ Δ lri x y t => let case_RLetRec := tt in _
733 destruct case_RArrange.
734 apply (flatten_arrangement Γ Δ a b x d).
739 change ([garrowfy_code_types (<[ ec |- t ]>) @@ nil])
740 with ([ga_mk (v2t ec) [] [garrowfy_code_types t] @@ nil]).
741 refine (ga_unkappa Γ Δ (v2t ec) nil (take_lev (ec::nil) succ) _
742 (mapOptionTree (garrowfy_leveled_code_types) (drop_lev (ec::nil) succ)) ;; _ ).
744 apply (Prelude_error "found Brak at depth >0 (a)").
750 change ([garrowfy_code_types (<[ ec |- t ]>) @@ nil])
751 with ([ga_mk (v2t ec) [] [garrowfy_code_types t] @@ nil]).
752 eapply nd_comp; [ apply arrange_esc | idtac ].
753 set (decide_tree_empty (take_lev (ec :: nil) succ)) as q'.
759 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanR ].
760 eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
761 eapply nd_comp; [ apply nd_llecnac | idtac ].
762 apply nd_prod; [ idtac | eapply boost ].
765 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanR ].
774 (* environment has non-empty leaves *)
775 apply (ga_kappa Γ Δ (v2t ec) nil (take_lev (ec::nil) succ) _ _).
776 apply (Prelude_error "found Esc at depth >0 (a)").
781 apply nd_rule; apply RNote; auto.
782 apply nd_rule; apply RNote; auto.
787 rewrite literal_types_unchanged.
788 apply nd_rule; apply RLit.
789 unfold take_lev; simpl.
790 unfold drop_lev; simpl.
793 rewrite literal_types_unchanged.
797 Opaque flatten_judgment.
799 Transparent flatten_judgment.
801 unfold flatten_judgment.
804 apply nd_rule. apply RVar.
805 repeat drop_simplify.
807 repeat take_simplify.
811 destruct case_RGlobal.
815 destruct l as [|ec lev]; simpl.
816 destruct (eqd_dec (g:CoreVar) (hetmet_flatten:CoreVar)).
817 set (garrowfy_code_types (g wev)) as t.
818 set (RGlobal _ Δ nil (mkGlobal Γ t hetmet_id)) as q.
823 destruct (eqd_dec (g:CoreVar) (hetmet_unflatten:CoreVar)).
824 set (garrowfy_code_types (g wev)) as t.
825 set (RGlobal _ Δ nil (mkGlobal Γ t hetmet_id)) as q.
830 apply nd_rule; rewrite globals_do_not_have_code_types.
832 apply (Prelude_error "found RGlobal at depth >0").
838 destruct lev as [|ec lev]; simpl; [ apply nd_rule; apply RLam; auto | idtac ].
839 repeat drop_simplify.
840 repeat take_simplify.
851 destruct lev as [|ec lev]; simpl; [ apply nd_rule; apply RCast; auto | idtac ].
852 apply flatten_coercion; auto.
853 apply (Prelude_error "RCast at level >0").
857 destruct (getjlev x); destruct (getjlev q).
860 apply (Prelude_error "RJoin at depth >0").
861 apply (Prelude_error "RJoin at depth >0").
862 apply (Prelude_error "RJoin at depth >0").
867 destruct lev as [|ec lev]. simpl. apply nd_rule.
868 replace (garrowfy_code_types (tx ---> te)) with ((garrowfy_code_types tx) ---> (garrowfy_code_types te)).
872 repeat drop_simplify.
873 repeat take_simplify.
874 rewrite mapOptionTree_distributes.
875 set (mapOptionTree (garrowfy_leveled_code_types ) (drop_lev (ec :: lev) Σ₁)) as Σ₁'.
876 set (mapOptionTree (garrowfy_leveled_code_types ) (drop_lev (ec :: lev) Σ₂)) as Σ₂'.
877 set (take_lev (ec :: lev) Σ₁) as Σ₁''.
878 set (take_lev (ec :: lev) Σ₂) as Σ₂''.
879 replace (garrowfy_code_types (tx ---> te)) with ((garrowfy_code_types tx) ---> (garrowfy_code_types te)).
880 apply (Prelude_error "FIXME: ga_apply").
883 Notation "` x" := (take_lev _ x) (at level 20).
884 Notation "`` x" := (mapOptionTree unlev x) (at level 20).
885 Notation "``` x" := ((drop_lev _ x)) (at level 20).
886 Notation "!<[]> x" := (garrowfy_code_types _ x) (at level 1).
887 Notation "!<[@]>" := (garrowfy_leveled_code_types _) (at level 1).
890 apply (Prelude_error "FIXME: RLet").
893 destruct lev as [|ec lev]; simpl; [ apply nd_rule; apply RLet; auto | idtac ].
894 destruct (Peano_dec.eq_nat_dec (Datatypes.length lev) n); [ idtac | apply nd_rule; apply RLet; auto ]; simpl.
895 repeat drop_simplify.
896 repeat take_simplify.
899 rewrite mapOptionTree_distributes.
900 rewrite mapOptionTree_distributes.
901 set (mapOptionTree (garrowfy_leveled_code_types (S n)) (drop_lev (ec :: lev) Σ₁)) as A.
902 set (take_lev (ec :: lev) Σ₁) as A'.
903 set (mapOptionTree (garrowfy_leveled_code_types (S n)) (drop_lev (ec :: lev) Σ₂)) as B.
904 set (take_lev (ec :: lev) Σ₂) as B'.
953 simpl. destruct lev; simpl.
954 rewrite garrowfy_commutes_with_HaskTAll.
955 rewrite garrowfy_commutes_with_substT.
960 apply (Prelude_error "ga_apply").
963 simpl. destruct lev; simpl.
964 rewrite garrowfy_commutes_with_HaskTAll.
965 rewrite garrowfy_commutes_with_HaskTApp.
966 eapply nd_comp; [ idtac | eapply nd_rule; eapply RAbsT ].
968 set (mapOptionTree (garrowfy_leveled_code_types ) (mapOptionTree (weakLT(κ:=κ)) Σ)) as a.
969 set (mapOptionTree (weakLT(κ:=κ)) (mapOptionTree (garrowfy_leveled_code_types ) Σ)) as q'.
977 rewrite garrowfy_commutes_with_weakLT.
988 apply (Prelude_error "AbsT at depth>0").
990 destruct case_RAppCo.
991 simpl. destruct lev; simpl.
992 unfold garrowfy_code_types.
996 apply flatten_coercion.
998 apply (Prelude_error "AppCo at depth>0").
1000 destruct case_RAbsCo.
1001 simpl. destruct lev; simpl.
1002 unfold garrowfy_code_types.
1004 apply (Prelude_error "AbsCo not supported (FIXME)").
1005 apply (Prelude_error "AbsCo at depth>0").
1007 destruct case_RLetRec.
1009 apply (Prelude_error "LetRec not supported (FIXME)").
1011 destruct case_RCase.
1013 apply (Prelude_error "Case not supported (FIXME)").
1017 (* to do: establish some metric on judgments (max length of level of any succedent type, probably), show how to
1018 * calculate it, and show that the flattening procedure above drives it down by one *)
1021 Instance FlatteningFunctor {Γ}{Δ}{ec} : Functor (JudgmentsL (PCF Γ Δ ec)) (TypesL (SystemFCa Γ Δ)) (obact) :=
1022 { fmor := FlatteningFunctor_fmor }.
1024 Definition ReificationFunctor Γ Δ : Functor (JudgmentsL _ _ (PCF n Γ Δ)) SystemFCa' (mapOptionTree brakifyJudg).
1025 refine {| fmor := ReificationFunctor_fmor Γ Δ |}; unfold hom; unfold ob; simpl ; intros.
1027 Definition PCF_SMME (n:nat)(Γ:TypeEnv)(Δ:CoercionEnv Γ) : ProgrammingLanguageSMME.
1028 refine {| plsmme_pl := PCF n Γ Δ |}.
1031 Definition SystemFCa_SMME (n:nat)(Γ:TypeEnv)(Δ:CoercionEnv Γ) : ProgrammingLanguageSMME.
1032 refine {| plsmme_pl := SystemFCa n Γ Δ |}.
1035 Definition ReificationFunctorMonoidal n : MonoidalFunctor (JudgmentsN n) (JudgmentsN (S n)) (ReificationFunctor n).
1039 Definition PCF_SystemFCa_two_level n Γ Δ : TwoLevelLanguage (PCF_SMME n Γ Δ) (SystemFCa_SMME (S n) Γ Δ).
1042 (* ... and the retraction exists *)
1046 Implicit Arguments garrow [ ].