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 ECKind -> RawHaskType TV ★ }.
101 Context {prodTy : forall TV, RawHaskType TV ECKind -> 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 {Γ}(ec:HaskType Γ ECKind)(tr:Tree ??(HaskType Γ ★)) : HaskType Γ ★ :=
105 fun TV ite => reduceTree (unitTy TV (ec TV ite)) (prodTy TV (ec TV ite)) (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 ec ant TV ite) (ga_mk_tree ec 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 v) (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
350 | eapply nd_rule; apply (@RLet Γ Δ [@ga_mk _ ec b c @@lev] Σ (@ga_mk _ ec a c) (@ga_mk _ ec a b) lev) ].
351 eapply nd_comp; [ apply nd_llecnac | idtac ].
354 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RExch ].
358 Definition precompose Γ Δ ec : forall a x y z lev,
360 [ Γ > Δ > a |- [@ga_mk _ ec y z @@ lev] ]
361 [ Γ > Δ > a,,[@ga_mk _ ec x y @@ lev] |- [@ga_mk _ ec x z @@ lev] ].
370 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RExch ].
376 Definition precompose' : ∀ Γ Δ ec lev a b c Σ,
377 ND Rule [] [ Γ > Δ > Σ |- [@ga_mk Γ ec b c @@ lev] ] ->
378 ND Rule [] [ Γ > Δ > Σ,,[@ga_mk Γ ec a b @@ lev] |- [@ga_mk Γ ec a c @@ lev] ].
385 Definition postcompose : ∀ Γ Δ ec lev a b c,
386 ND Rule [] [ Γ > Δ > [] |- [@ga_mk Γ ec a b @@ lev] ] ->
387 ND Rule [] [ Γ > Δ > [@ga_mk Γ ec b c @@ lev] |- [@ga_mk Γ ec a c @@ lev] ].
397 Definition firstify : ∀ Γ Δ ec lev a b c Σ,
398 ND Rule [] [ Γ > Δ > Σ |- [@ga_mk Γ ec a b @@ lev] ] ->
399 ND Rule [] [ Γ > Δ > Σ |- [@ga_mk Γ ec (a,,c) (b,,c) @@ lev] ].
401 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanL ].
402 eapply nd_comp; [ idtac | eapply nd_rule; apply RLet ].
403 eapply nd_comp; [ apply nd_llecnac | idtac ].
406 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RuCanL ].
410 Definition secondify : ∀ Γ Δ ec lev a b c Σ,
411 ND Rule [] [ Γ > Δ > Σ |- [@ga_mk Γ ec a b @@ lev] ] ->
412 ND Rule [] [ Γ > Δ > Σ |- [@ga_mk Γ ec (c,,a) (c,,b) @@ lev] ].
414 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanL ].
415 eapply nd_comp; [ idtac | eapply nd_rule; apply RLet ].
416 eapply nd_comp; [ apply nd_llecnac | idtac ].
419 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RuCanL ].
423 Lemma ga_unkappa : ∀ Γ Δ ec l a b Σ,
425 [Γ > Δ > Σ |- [@ga_mk Γ ec a b @@ l] ]
426 [Γ > Δ > Σ,,[@ga_mk Γ ec [] a @@ l] |- [@ga_mk Γ ec [] b @@ l] ].
428 set (ga_comp Γ Δ ec l [] a b) as q.
430 set (@RLet Γ Δ) as q'.
431 set (@RLet Γ Δ [@ga_mk _ ec [] a @@ l] Σ (@ga_mk _ ec [] b) (@ga_mk _ ec a b) l) as q''.
452 (* useful for cutting down on the pretty-printed noise
454 Notation "` x" := (take_lev _ x) (at level 20).
455 Notation "`` x" := (mapOptionTree unlev x) (at level 20).
456 Notation "``` x" := (drop_lev _ x) (at level 20).
458 Definition garrowfy_arrangement' :
459 forall Γ (Δ:CoercionEnv Γ)
460 (ec:HaskTyVar Γ ECKind) (lev:HaskLevel Γ) (ant1 ant2:Tree ??(LeveledHaskType Γ ★)) (r:Arrange ant1 ant2),
461 ND Rule [] [Γ > Δ > [] |- [@ga_mk _ (v2t ec) (take_lev (ec :: lev) ant2) (take_lev (ec :: lev) ant1) @@ nil] ].
464 refine (fix garrowfy ant1 ant2 (r:Arrange ant1 ant2):
465 ND Rule [] [Γ > Δ > [] |- [@ga_mk _ (v2t ec) (take_lev (ec :: lev) ant2) (take_lev (ec :: lev) ant1) @@ nil]] :=
466 match r as R in Arrange A B return
467 ND Rule [] [Γ > Δ > [] |- [@ga_mk _ (v2t ec) (take_lev (ec :: lev) B) (take_lev (ec :: lev) A) @@ nil]]
469 | RCanL a => let case_RCanL := tt in ga_uncancell _ _ _ _ _
470 | RCanR a => let case_RCanR := tt in ga_uncancelr _ _ _ _ _
471 | RuCanL a => let case_RuCanL := tt in ga_cancell _ _ _ _ _
472 | RuCanR a => let case_RuCanR := tt in ga_cancelr _ _ _ _ _
473 | RAssoc a b c => let case_RAssoc := tt in ga_assoc _ _ _ _ _ _ _
474 | RCossa a b c => let case_RCossa := tt in ga_unassoc _ _ _ _ _ _ _
475 | RExch a b => let case_RExch := tt in ga_swap _ _ _ _ _ _
476 | RWeak a => let case_RWeak := tt in ga_drop _ _ _ _ _
477 | RCont a => let case_RCont := tt in ga_copy _ _ _ _ _
478 | RLeft a b c r' => let case_RLeft := tt in garrowfy _ _ r' ;; boost _ _ _ _ _ (ga_second _ _ _ _ _ _ _)
479 | RRight a b c r' => let case_RRight := tt in garrowfy _ _ r' ;; boost _ _ _ _ _ (ga_first _ _ _ _ _ _ _)
480 | RComp c b a r1 r2 => let case_RComp := tt in (fun r1' r2' => _) (garrowfy _ _ r1) (garrowfy _ _ r2)
481 end); clear garrowfy; repeat take_simplify; repeat drop_simplify; intros.
484 set (take_lev (ec :: lev) a) as a' in *.
485 set (take_lev (ec :: lev) b) as b' in *.
486 set (take_lev (ec :: lev) c) as c' in *.
487 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RCanL ].
488 eapply nd_comp; [ idtac | eapply nd_rule; apply
489 (@RLet Γ Δ [] [] (@ga_mk _ (v2t ec) a' c') (@ga_mk _ (v2t ec) a' b')) ].
490 eapply nd_comp; [ apply nd_llecnac | idtac ].
493 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RuCanL ].
494 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RCanR ].
495 eapply nd_comp; [ idtac | eapply nd_rule; apply
496 (@RLet Γ Δ [@ga_mk _ (v2t ec) a' b' @@ _] [] (@ga_mk _ (v2t ec) a' c') (@ga_mk _ (v2t ec) b' c'))].
497 eapply nd_comp; [ apply nd_llecnac | idtac ].
503 Definition garrowfy_arrangement :
504 forall Γ (Δ:CoercionEnv Γ) n
505 (ec:HaskTyVar Γ ECKind) (lev:HaskLevel Γ) (ant1 ant2:Tree ??(LeveledHaskType Γ ★)) (r:Arrange ant1 ant2) succ,
507 [Γ > Δ > mapOptionTree (garrowfy_leveled_code_types ) (drop_lev n ant1)
508 |- [@ga_mk _ (v2t ec) (take_lev (ec :: lev) ant1) (mapOptionTree (unlev' ) succ) @@ nil]]
509 [Γ > Δ > mapOptionTree (garrowfy_leveled_code_types ) (drop_lev n ant2)
510 |- [@ga_mk _ (v2t ec) (take_lev (ec :: lev) ant2) (mapOptionTree (unlev' ) succ) @@ nil]].
512 refine ( _ ;; (boost _ _ _ _ _ (postcompose _ _ _ _ _ _ _ (garrowfy_arrangement' Γ Δ ec lev ant1 ant2 r)))).
515 refine ((fix garrowfy ant1 ant2 (r:Arrange ant1 ant2) :=
516 match r as R in Arrange A B return
517 Arrange (mapOptionTree (garrowfy_leveled_code_types ) (drop_lev _ A))
518 (mapOptionTree (garrowfy_leveled_code_types ) (drop_lev _ B)) with
519 | RCanL a => let case_RCanL := tt in RCanL _
520 | RCanR a => let case_RCanR := tt in RCanR _
521 | RuCanL a => let case_RuCanL := tt in RuCanL _
522 | RuCanR a => let case_RuCanR := tt in RuCanR _
523 | RAssoc a b c => let case_RAssoc := tt in RAssoc _ _ _
524 | RCossa a b c => let case_RCossa := tt in RCossa _ _ _
525 | RExch a b => let case_RExch := tt in RExch _ _
526 | RWeak a => let case_RWeak := tt in RWeak _
527 | RCont a => let case_RCont := tt in RCont _
528 | RLeft a b c r' => let case_RLeft := tt in RLeft _ (garrowfy _ _ r')
529 | RRight a b c r' => let case_RRight := tt in RRight _ (garrowfy _ _ r')
530 | RComp a b c r1 r2 => let case_RComp := tt in RComp (garrowfy _ _ r1) (garrowfy _ _ r2)
531 end) ant1 ant2 r); clear garrowfy; repeat take_simplify; repeat drop_simplify; intros.
534 Definition flatten_arrangement :
535 forall Γ Δ ant1 ant2 succ (r:Arrange ant1 ant2),
536 ND Rule (mapOptionTree (flatten_judgment ) [Γ > Δ > ant1 |- succ])
537 (mapOptionTree (flatten_judgment ) [Γ > Δ > ant2 |- succ]).
540 set (getjlev succ) as succ_lev.
541 assert (succ_lev=getjlev succ).
559 eapply RComp; [ apply IHr1 | apply IHr2 ].
561 apply garrowfy_arrangement.
565 Definition ga_join Γ Δ Σ₁ Σ₂ a b ec :
566 ND Rule [] [Γ > Δ > Σ₁ |- [@ga_mk _ ec [] a @@ nil]] ->
567 ND Rule [] [Γ > Δ > Σ₂ |- [@ga_mk _ ec [] b @@ nil]] ->
568 ND Rule [] [Γ > Δ > Σ₁,,Σ₂ |- [@ga_mk _ ec [] (a,,b) @@ nil]].
571 apply secondify with (c:=a) in pfb.
574 eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
575 eapply nd_comp; [ eapply nd_llecnac | idtac ].
584 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanL ].
590 Definition arrange_brak : forall Γ Δ ec succ t,
592 [Γ > Δ > mapOptionTree (garrowfy_leveled_code_types ) (drop_lev (ec :: nil) succ),,
593 [(@ga_mk _ (v2t ec) [] (take_lev (ec :: nil) succ)) @@ nil] |- [(@ga_mk _ (v2t ec) [] [garrowfy_code_types t]) @@ nil]]
594 [Γ > Δ > mapOptionTree (garrowfy_leveled_code_types ) succ |- [(@ga_mk _ (v2t ec) [] [garrowfy_code_types t]) @@ nil]].
597 set (@arrange' _ succ (levelMatch (ec::nil))) as q.
598 set (arrangeMap _ _ garrowfy_leveled_code_types q) as y.
607 eapply nd_comp; [ apply nd_llecnac | idtac ].
608 eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
613 induction succ; try destruct a; simpl.
619 destruct l as [t' lev'].
620 destruct lev' as [|ec' lev'].
624 set (@eqd_dec (HaskLevel Γ) (haskLevelEqDecidable Γ) (ec' :: lev') (ec :: nil)) as q.
640 Definition arrange_esc : forall Γ Δ ec succ t,
642 [Γ > Δ > mapOptionTree (garrowfy_leveled_code_types ) succ |- [(@ga_mk _ (v2t ec) [] [garrowfy_code_types t]) @@ nil]]
643 [Γ > Δ > mapOptionTree (garrowfy_leveled_code_types ) (drop_lev (ec :: nil) succ),,
644 [(@ga_mk _ (v2t ec) [] (take_lev (ec :: nil) succ)) @@ nil] |- [(@ga_mk _ (v2t ec) [] [garrowfy_code_types t]) @@ nil]].
647 set (@arrange _ succ (levelMatch (ec::nil))) as q.
648 set (arrangeMap _ _ garrowfy_leveled_code_types q) as y.
660 unfold mkDropFlags; simpl.
664 destruct (General.list_eq_dec h0 (ec :: nil)).
666 unfold garrowfy_leveled_code_types'.
681 apply (Prelude_error "escapifying code with multi-leaf antecedents is not supported").
684 Lemma mapOptionTree_distributes
685 : forall T R (a b:Tree ??T) (f:T->R),
686 mapOptionTree f (a,,b) = (mapOptionTree f a),,(mapOptionTree f b).
690 Definition decide_tree_empty : forall {T:Type}(t:Tree ??T),
691 sum { q:Tree unit & t = mapTree (fun _ => None) q } unit.
696 | T_Branch b1 b2 => let b1' := foo b1 in let b2' := foo b2 in _
716 Definition flatten_proof :
719 ND Rule (mapOptionTree (flatten_judgment ) h) (mapOptionTree (flatten_judgment ) c).
721 eapply nd_map'; [ idtac | apply X ].
726 refine (match X as R in Rule H C with
727 | RArrange Γ Δ a b x d => let case_RArrange := tt in _
728 | RNote Γ Δ Σ τ l n => let case_RNote := tt in _
729 | RLit Γ Δ l _ => let case_RLit := tt in _
730 | RVar Γ Δ σ lev => let case_RVar := tt in _
731 | RGlobal Γ Δ σ l wev => let case_RGlobal := tt in _
732 | RLam Γ Δ Σ tx te lev => let case_RLam := tt in _
733 | RCast Γ Δ Σ σ τ lev γ => let case_RCast := tt in _
734 | RAbsT Γ Δ Σ κ σ lev => let case_RAbsT := tt in _
735 | RAppT Γ Δ Σ κ σ τ lev => let case_RAppT := tt in _
736 | RAppCo Γ Δ Σ κ σ₁ σ₂ γ σ lev => let case_RAppCo := tt in _
737 | RAbsCo Γ Δ Σ κ σ σ₁ σ₂ lev => let case_RAbsCo := tt in _
738 | RApp Γ Δ Σ₁ Σ₂ tx te lev => let case_RApp := tt in _
739 | RLet Γ Δ Σ₁ Σ₂ σ₁ σ₂ lev => let case_RLet := tt in _
740 | RJoin Γ p lri m x q => let case_RJoin := tt in _
741 | RVoid _ _ => let case_RVoid := tt in _
742 | RBrak Γ Δ t ec succ lev => let case_RBrak := tt in _
743 | REsc Γ Δ t ec succ lev => let case_REsc := tt in _
744 | RCase Γ Δ lev tc Σ avars tbranches alts => let case_RCase := tt in _
745 | RLetRec Γ Δ lri x y t => let case_RLetRec := tt in _
748 destruct case_RArrange.
749 apply (flatten_arrangement Γ Δ a b x d).
754 change ([garrowfy_code_types (<[ ec |- t ]>) @@ nil])
755 with ([ga_mk (v2t ec) [] [garrowfy_code_types t] @@ nil]).
756 refine (ga_unkappa Γ Δ (v2t ec) nil (take_lev (ec::nil) succ) _
757 (mapOptionTree (garrowfy_leveled_code_types) (drop_lev (ec::nil) succ)) ;; _ ).
759 apply (Prelude_error "found Brak at depth >0 indicating 3-level code; only two-level code is currently supported").
765 change ([garrowfy_code_types (<[ ec |- t ]>) @@ nil])
766 with ([ga_mk (v2t ec) [] [garrowfy_code_types t] @@ nil]).
767 eapply nd_comp; [ apply arrange_esc | idtac ].
768 set (decide_tree_empty (take_lev (ec :: nil) succ)) as q'.
774 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanR ].
775 eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
776 eapply nd_comp; [ apply nd_llecnac | idtac ].
777 apply nd_prod; [ idtac | eapply boost ].
780 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanR ].
789 (* environment has non-empty leaves *)
790 apply (ga_kappa Γ Δ (v2t ec) nil (take_lev (ec::nil) succ) _ _).
791 apply (Prelude_error "found Esc at depth >0 indicating 3-level code; only two-level code is currently supported").
796 apply nd_rule; apply RNote; auto.
797 apply nd_rule; apply RNote; auto.
802 rewrite literal_types_unchanged.
803 apply nd_rule; apply RLit.
804 unfold take_lev; simpl.
805 unfold drop_lev; simpl.
808 rewrite literal_types_unchanged.
812 Opaque flatten_judgment.
814 Transparent flatten_judgment.
816 unfold flatten_judgment.
819 apply nd_rule. apply RVar.
820 repeat drop_simplify.
822 repeat take_simplify.
826 destruct case_RGlobal.
830 destruct l as [|ec lev]; simpl.
831 destruct (eqd_dec (g:CoreVar) (hetmet_flatten:CoreVar)).
832 set (garrowfy_code_types (g wev)) as t.
833 set (RGlobal _ Δ nil (mkGlobal Γ t hetmet_id)) as q.
838 destruct (eqd_dec (g:CoreVar) (hetmet_unflatten:CoreVar)).
839 set (garrowfy_code_types (g wev)) as t.
840 set (RGlobal _ Δ nil (mkGlobal Γ t hetmet_id)) as q.
845 apply nd_rule; rewrite globals_do_not_have_code_types.
847 apply (Prelude_error "found RGlobal at depth >0; globals should never appear inside code brackets unless escaped").
853 destruct lev as [|ec lev]; simpl; [ apply nd_rule; apply RLam; auto | idtac ].
854 repeat drop_simplify.
855 repeat take_simplify.
866 destruct lev as [|ec lev]; simpl; [ apply nd_rule; apply RCast; auto | idtac ].
867 apply flatten_coercion; auto.
868 apply (Prelude_error "RCast at level >0; casting inside of code brackets is currently not supported").
872 destruct (getjlev x); destruct (getjlev q);
873 [ apply nd_rule; apply RJoin | idtac | idtac | idtac ];
874 apply (Prelude_error "RJoin at depth >0").
879 destruct lev as [|ec lev]. simpl. apply nd_rule.
880 replace (garrowfy_code_types (tx ---> te)) with ((garrowfy_code_types tx) ---> (garrowfy_code_types te)).
884 repeat drop_simplify.
885 repeat take_simplify.
886 rewrite mapOptionTree_distributes.
887 set (mapOptionTree (garrowfy_leveled_code_types ) (drop_lev (ec :: lev) Σ₁)) as Σ₁'.
888 set (mapOptionTree (garrowfy_leveled_code_types ) (drop_lev (ec :: lev) Σ₂)) as Σ₂'.
889 set (take_lev (ec :: lev) Σ₁) as Σ₁''.
890 set (take_lev (ec :: lev) Σ₂) as Σ₂''.
891 replace (garrowfy_code_types (tx ---> te)) with ((garrowfy_code_types tx) ---> (garrowfy_code_types te)).
892 apply (Prelude_error "FIXME: ga_apply").
896 Notation "` x" := (take_lev _ x).
897 Notation "`` x" := (mapOptionTree unlev x) (at level 20).
898 Notation "``` x" := ((drop_lev _ x)) (at level 20).
899 Notation "!<[]> x" := (garrowfy_code_types _ x) (at level 1).
900 Notation "!<[@]> x" := (mapOptionTree garrowfy_leveled_code_types x) (at level 1).
905 destruct lev as [|ec lev]; simpl; [ apply nd_rule; apply RLet; auto | idtac ].
906 repeat drop_simplify.
907 repeat take_simplify.
911 eapply nd_prod; [ idtac | apply nd_id ].
933 simpl. destruct lev; simpl.
934 rewrite garrowfy_commutes_with_HaskTAll.
935 rewrite garrowfy_commutes_with_substT.
940 apply (Prelude_error "found type application at level >0; this is not supported").
943 simpl. destruct lev; simpl.
944 rewrite garrowfy_commutes_with_HaskTAll.
945 rewrite garrowfy_commutes_with_HaskTApp.
946 eapply nd_comp; [ idtac | eapply nd_rule; eapply RAbsT ].
948 set (mapOptionTree (garrowfy_leveled_code_types ) (mapOptionTree (weakLT(κ:=κ)) Σ)) as a.
949 set (mapOptionTree (weakLT(κ:=κ)) (mapOptionTree (garrowfy_leveled_code_types ) Σ)) as q'.
957 rewrite garrowfy_commutes_with_weakLT.
968 apply (Prelude_error "found type abstraction at level >0; this is not supported").
970 destruct case_RAppCo.
971 simpl. destruct lev; simpl.
972 unfold garrowfy_code_types.
976 apply flatten_coercion.
978 apply (Prelude_error "found coercion application at level >0; this is not supported").
980 destruct case_RAbsCo.
981 simpl. destruct lev; simpl.
982 unfold garrowfy_code_types.
984 apply (Prelude_error "AbsCo not supported (FIXME)").
985 apply (Prelude_error "found coercion abstraction at level >0; this is not supported").
987 destruct case_RLetRec.
990 apply (Prelude_error "LetRec not supported (FIXME)").
994 apply (Prelude_error "Case not supported (BIG FIXME)").
998 (* to do: establish some metric on judgments (max length of level of any succedent type, probably), show how to
999 * calculate it, and show that the flattening procedure above drives it down by one *)
1002 Instance FlatteningFunctor {Γ}{Δ}{ec} : Functor (JudgmentsL (PCF Γ Δ ec)) (TypesL (SystemFCa Γ Δ)) (obact) :=
1003 { fmor := FlatteningFunctor_fmor }.
1005 Definition ReificationFunctor Γ Δ : Functor (JudgmentsL _ _ (PCF n Γ Δ)) SystemFCa' (mapOptionTree brakifyJudg).
1006 refine {| fmor := ReificationFunctor_fmor Γ Δ |}; unfold hom; unfold ob; simpl ; intros.
1008 Definition PCF_SMME (n:nat)(Γ:TypeEnv)(Δ:CoercionEnv Γ) : ProgrammingLanguageSMME.
1009 refine {| plsmme_pl := PCF n Γ Δ |}.
1012 Definition SystemFCa_SMME (n:nat)(Γ:TypeEnv)(Δ:CoercionEnv Γ) : ProgrammingLanguageSMME.
1013 refine {| plsmme_pl := SystemFCa n Γ Δ |}.
1016 Definition ReificationFunctorMonoidal n : MonoidalFunctor (JudgmentsN n) (JudgmentsN (S n)) (ReificationFunctor n).
1020 Definition PCF_SystemFCa_two_level n Γ Δ : TwoLevelLanguage (PCF_SMME n Γ Δ) (SystemFCa_SMME (S n) Γ Δ).
1023 (* ... and the retraction exists *)
1027 Implicit Arguments garrow [ ].