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 Definition v2t {Γ}(ec:HaskTyVar Γ ECKind) : HaskType Γ ECKind := fun TV ite => TVar (ec TV ite).
99 Definition levelMatch {Γ}(lev:HaskLevel Γ) : LeveledHaskType Γ ★ -> bool :=
100 fun t => match t with ttype@@tlev => if eqd_dec tlev lev then true else false end.
102 (* In a tree of types, replace any type at depth "lev" or greater None *)
103 Definition mkDropFlags {Γ}(lev:HaskLevel Γ)(tt:Tree ??(LeveledHaskType Γ ★)) : TreeFlags tt :=
104 mkFlags (liftBoolFunc false (levelMatch lev)) tt.
106 Definition drop_lev {Γ}(lev:HaskLevel Γ)(tt:Tree ??(LeveledHaskType Γ ★)) : Tree ??(LeveledHaskType Γ ★) :=
107 dropT (mkDropFlags lev tt).
109 (* The opposite: replace any type which is NOT at level "lev" with None *)
110 Definition mkTakeFlags {Γ}(lev:HaskLevel Γ)(tt:Tree ??(LeveledHaskType Γ ★)) : TreeFlags tt :=
111 mkFlags (liftBoolFunc true (bnot ○ levelMatch lev)) tt.
113 Definition take_lev {Γ}(lev:HaskLevel Γ)(tt:Tree ??(LeveledHaskType Γ ★)) : Tree ??(LeveledHaskType Γ ★) :=
114 dropT (mkTakeFlags lev tt).
116 mapOptionTree (fun x => flatten_type (unlev x))
117 (maybeTree (takeT tt (mkFlags (
118 fun t => match t with
119 | Some (ttype @@ tlev) => if eqd_dec tlev lev then true else false
124 Definition maybeTree {T}(t:??(Tree ??T)) : Tree ??T :=
131 Lemma drop_lev_lemma : forall Γ (lev:HaskLevel Γ) x, drop_lev lev [x @@ lev] = [].
143 Lemma drop_lev_lemma_s : forall Γ (lev:HaskLevel Γ) ec x, drop_lev (ec::lev) [x @@ (ec :: lev)] = [].
154 Lemma take_lemma : forall Γ (lev:HaskLevel Γ) x, take_lev lev [x @@ lev] = [x @@ lev].
165 Ltac drop_simplify :=
167 | [ |- context[@drop_lev ?G ?L [ ?X @@ ?L ] ] ] =>
168 rewrite (drop_lev_lemma G L X)
169 | [ |- context[@drop_lev ?G (?E :: ?L) [ ?X @@ (?E :: ?L) ] ] ] =>
170 rewrite (drop_lev_lemma_s G L E X)
171 | [ |- context[@drop_lev ?G ?N (?A,,?B)] ] =>
172 change (@drop_lev G N (A,,B)) with ((@drop_lev G N A),,(@drop_lev G N B))
173 | [ |- context[@drop_lev ?G ?N (T_Leaf None)] ] =>
174 change (@drop_lev G N (T_Leaf (@None (LeveledHaskType G ★)))) with (T_Leaf (@None (LeveledHaskType G ★)))
177 Ltac take_simplify :=
179 | [ |- context[@take_lev ?G ?L [ ?X @@ ?L ] ] ] =>
180 rewrite (take_lemma G L X)
181 | [ |- context[@take_lev ?G ?N (?A,,?B)] ] =>
182 change (@take_lev G N (A,,B)) with ((@take_lev G N A),,(@take_lev G N B))
183 | [ |- context[@take_lev ?G ?N (T_Leaf None)] ] =>
184 change (@take_lev G N (T_Leaf (@None (LeveledHaskType G ★)))) with (T_Leaf (@None (LeveledHaskType G ★)))
188 (*******************************************************************************)
191 Context (hetmet_flatten : WeakExprVar).
192 Context (hetmet_unflatten : WeakExprVar).
193 Context (hetmet_id : WeakExprVar).
194 Context {unitTy : forall TV, RawHaskType TV ECKind -> RawHaskType TV ★ }.
195 Context {prodTy : forall TV, RawHaskType TV ECKind -> RawHaskType TV ★ -> RawHaskType TV ★ -> RawHaskType TV ★ }.
196 Context {gaTy : forall TV, RawHaskType TV ECKind -> RawHaskType TV ★ -> RawHaskType TV ★ -> RawHaskType TV ★ }.
198 Definition ga_mk_tree {Γ}(ec:HaskType Γ ECKind)(tr:Tree ??(HaskType Γ ★)) : HaskType Γ ★ :=
199 fun TV ite => reduceTree (unitTy TV (ec TV ite)) (prodTy TV (ec TV ite)) (mapOptionTree (fun x => x TV ite) tr).
201 Definition ga_mk {Γ}(ec:HaskType Γ ECKind )(ant suc:Tree ??(HaskType Γ ★)) : HaskType Γ ★ :=
202 fun TV ite => gaTy TV (ec TV ite) (ga_mk_tree ec ant TV ite) (ga_mk_tree ec suc TV ite).
206 * - code types <[t]>@c become garrows c () t
207 * - free variables of type t at a level lev deeper than the succedent become garrows c () t
208 * - free variables at the level of the succedent become
210 Fixpoint flatten_rawtype {TV}{κ}(exp: RawHaskType TV κ) : RawHaskType TV κ :=
213 | TAll _ y => TAll _ (fun v => flatten_rawtype (y v))
214 | TApp _ _ x y => TApp (flatten_rawtype x) (flatten_rawtype y)
216 | TCoerc _ t1 t2 t => TCoerc (flatten_rawtype t1) (flatten_rawtype t2) (flatten_rawtype t)
218 | TCode v e => gaTy TV v (unitTy TV v) (flatten_rawtype e)
219 | TyFunApp tfc kl k lt => TyFunApp tfc kl k (flatten_rawtype_list _ lt)
221 with flatten_rawtype_list {TV}(lk:list Kind)(exp:@RawHaskTypeList TV lk) : @RawHaskTypeList TV lk :=
222 match exp in @RawHaskTypeList _ LK return @RawHaskTypeList TV LK with
223 | TyFunApp_nil => TyFunApp_nil
224 | TyFunApp_cons κ kl t rest => TyFunApp_cons _ _ (flatten_rawtype t) (flatten_rawtype_list _ rest)
227 Definition flatten_type {Γ}{κ}(ht:HaskType Γ κ) : HaskType Γ κ :=
229 flatten_rawtype (ht TV ite).
231 Fixpoint flatten_leveled_type' {Γ}(ht:HaskType Γ ★)(lev:HaskLevel Γ) : HaskType Γ ★ :=
233 | nil => flatten_type ht
234 | ec::lev' => @ga_mk _ (v2t ec) [] [flatten_leveled_type' ht lev']
237 Definition flatten_leveled_type {Γ}(ht:LeveledHaskType Γ ★) : LeveledHaskType Γ ★ :=
240 flatten_leveled_type' htt lev @@ nil
245 Axiom literal_types_unchanged : forall Γ l, flatten_type (literalType l) = literalType(Γ:=Γ) l.
247 Axiom flatten_coercion : forall Γ Δ κ (σ τ:HaskType Γ κ) (γ:HaskCoercion Γ Δ (σ ∼∼∼ τ)),
248 HaskCoercion Γ Δ (flatten_type σ ∼∼∼ flatten_type τ).
250 Axiom flatten_commutes_with_substT :
251 forall κ Γ (Δ:CoercionEnv Γ) (σ:∀ TV, InstantiatedTypeEnv TV Γ → TV κ → RawHaskType TV ★) (τ:HaskType Γ κ),
252 flatten_type (substT σ τ) = substT (fun TV ite v => flatten_rawtype (σ TV ite v))
255 Axiom flatten_commutes_with_HaskTAll :
256 forall κ Γ (Δ:CoercionEnv Γ) (σ:∀ TV, InstantiatedTypeEnv TV Γ → TV κ → RawHaskType TV ★),
257 flatten_type (HaskTAll κ σ) = HaskTAll κ (fun TV ite v => flatten_rawtype (σ TV ite v)).
259 Axiom flatten_commutes_with_HaskTApp :
260 forall κ Γ (Δ:CoercionEnv Γ) (σ:∀ TV, InstantiatedTypeEnv TV Γ → TV κ → RawHaskType TV ★),
261 flatten_type (HaskTApp (weakF σ) (FreshHaskTyVar κ)) =
262 HaskTApp (weakF (fun TV ite v => flatten_rawtype (σ TV ite v))) (FreshHaskTyVar κ).
264 Axiom flatten_commutes_with_weakLT : forall (Γ:TypeEnv) κ t,
265 flatten_leveled_type (weakLT(Γ:=Γ)(κ:=κ) t) = weakLT(Γ:=Γ)(κ:=κ) (flatten_leveled_type t).
267 Axiom globals_do_not_have_code_types : forall (Γ:TypeEnv) (g:Global Γ) v,
268 flatten_type (g v) = g v.
270 (* This tries to assign a single level to the entire succedent of a judgment. If the succedent has types from different
271 * levels (should not happen) it just picks one; if the succedent has no non-None leaves (also should not happen) it
273 Definition getΓ (j:Judg) := match j with Γ > _ > _ |- _ => Γ end.
274 Definition getSuc (j:Judg) : Tree ??(LeveledHaskType (getΓ j) ★) :=
275 match j as J return Tree ??(LeveledHaskType (getΓ J) ★) with Γ > _ > _ |- s => s end.
276 Fixpoint getjlev {Γ}(tt:Tree ??(LeveledHaskType Γ ★)) : HaskLevel Γ :=
279 | T_Leaf (Some (_ @@ lev)) => lev
281 match getjlev b1 with
287 (* "n" is the maximum depth remaining AFTER flattening *)
288 Definition flatten_judgment (j:Judg) :=
289 match j as J return Judg with
290 Γ > Δ > ant |- suc =>
291 match getjlev suc with
292 | nil => Γ > Δ > mapOptionTree flatten_leveled_type ant
293 |- mapOptionTree flatten_leveled_type suc
295 | (ec::lev') => Γ > Δ > mapOptionTree flatten_leveled_type (drop_lev (ec::lev') ant)
297 (mapOptionTree (flatten_type ○ unlev) (take_lev (ec::lev') ant))
298 (mapOptionTree (flatten_type ○ unlev) suc )
299 @@ nil] (* we know the level of all of suc *)
304 { ga_id : ∀ Γ Δ ec l a , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec a a @@ l] ]
305 ; ga_cancelr : ∀ Γ Δ ec l a , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec (a,,[]) a @@ l] ]
306 ; ga_cancell : ∀ Γ Δ ec l a , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec ([],,a) a @@ l] ]
307 ; ga_uncancelr : ∀ Γ Δ ec l a , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec a (a,,[]) @@ l] ]
308 ; ga_uncancell : ∀ Γ Δ ec l a , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec a ([],,a) @@ l] ]
309 ; ga_assoc : ∀ Γ Δ ec l a b c, ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec ((a,,b),,c) (a,,(b,,c)) @@ l] ]
310 ; ga_unassoc : ∀ Γ Δ ec l a b c, ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec (a,,(b,,c)) ((a,,b),,c) @@ l] ]
311 ; ga_swap : ∀ Γ Δ ec l a b , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec (a,,b) (b,,a) @@ l] ]
312 ; ga_drop : ∀ Γ Δ ec l a , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec a [] @@ l] ]
313 ; ga_copy : ∀ Γ Δ ec l a , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec a (a,,a) @@ l] ]
314 ; ga_first : ∀ Γ Δ ec l a b x, ND Rule [] [Γ > Δ > [@ga_mk Γ ec a b @@ l] |- [@ga_mk Γ ec (a,,x) (b,,x) @@ l] ]
315 ; ga_second : ∀ Γ Δ ec l a b x, ND Rule [] [Γ > Δ > [@ga_mk Γ ec a b @@ l] |- [@ga_mk Γ ec (x,,a) (x,,b) @@ l] ]
316 ; ga_lit : ∀ Γ Δ ec l lit , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec [] [literalType lit] @@ l] ]
317 ; ga_curry : ∀ Γ Δ ec l a b c, ND Rule [] [Γ > Δ > [@ga_mk Γ ec (a,,[b]) [c] @@ l] |- [@ga_mk Γ ec a [b ---> c] @@ l] ]
318 ; 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] ]
319 ; ga_apply : ∀ Γ Δ ec l a a' b c,
320 ND Rule [] [Γ > Δ > [@ga_mk Γ ec a [b ---> c] @@ l],,[@ga_mk Γ ec a' [b] @@ l] |- [@ga_mk Γ ec (a,,a') [c] @@ l] ]
321 ; ga_kappa : ∀ Γ Δ ec l a b Σ, ND Rule
322 [Γ > Δ > Σ,,[@ga_mk Γ ec [] a @@ l] |- [@ga_mk Γ ec [] b @@ l] ]
323 [Γ > Δ > Σ |- [@ga_mk Γ ec a b @@ l] ]
325 Context `(gar:garrow).
327 Notation "a ~~~~> b" := (@ga_mk _ _ a b) (at level 20).
329 Definition boost : forall Γ Δ ant x y {lev},
330 ND Rule [] [ Γ > Δ > [x@@lev] |- [y@@lev] ] ->
331 ND Rule [ Γ > Δ > ant |- [x@@lev] ] [ Γ > Δ > ant |- [y@@lev] ].
333 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanL ].
334 eapply nd_comp; [ idtac | eapply nd_rule; apply (@RLet Γ Δ [] ant y x lev) ].
335 eapply nd_comp; [ apply nd_rlecnac | idtac ].
345 Definition postcompose' : ∀ Γ Δ ec lev a b c Σ,
346 ND Rule [] [ Γ > Δ > Σ |- [@ga_mk Γ ec a b @@ lev] ] ->
347 ND Rule [] [ Γ > Δ > Σ,,[@ga_mk Γ ec b c @@ lev] |- [@ga_mk Γ ec a c @@ lev] ].
349 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RExch ].
350 eapply nd_comp; [ idtac
351 | eapply nd_rule; apply (@RLet Γ Δ [@ga_mk _ ec b c @@lev] Σ (@ga_mk _ ec a c) (@ga_mk _ ec a b) lev) ].
352 eapply nd_comp; [ apply nd_llecnac | idtac ].
355 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RExch ].
359 Definition precompose Γ Δ ec : forall a x y z lev,
361 [ Γ > Δ > a |- [@ga_mk _ ec y z @@ lev] ]
362 [ Γ > Δ > a,,[@ga_mk _ ec x y @@ lev] |- [@ga_mk _ ec x z @@ lev] ].
371 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RExch ].
377 Definition precompose' : ∀ Γ Δ ec lev a b c Σ,
378 ND Rule [] [ Γ > Δ > Σ |- [@ga_mk Γ ec b c @@ lev] ] ->
379 ND Rule [] [ Γ > Δ > Σ,,[@ga_mk Γ ec a b @@ lev] |- [@ga_mk Γ ec a c @@ lev] ].
386 Definition postcompose : ∀ Γ Δ ec lev a b c,
387 ND Rule [] [ Γ > Δ > [] |- [@ga_mk Γ ec a b @@ lev] ] ->
388 ND Rule [] [ Γ > Δ > [@ga_mk Γ ec b c @@ lev] |- [@ga_mk Γ ec a c @@ lev] ].
398 Definition firstify : ∀ Γ Δ ec lev a b c Σ,
399 ND Rule [] [ Γ > Δ > Σ |- [@ga_mk Γ ec a b @@ lev] ] ->
400 ND Rule [] [ Γ > Δ > Σ |- [@ga_mk Γ ec (a,,c) (b,,c) @@ lev] ].
402 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanL ].
403 eapply nd_comp; [ idtac | eapply nd_rule; apply RLet ].
404 eapply nd_comp; [ apply nd_llecnac | idtac ].
407 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RuCanL ].
411 Definition secondify : ∀ Γ Δ ec lev a b c Σ,
412 ND Rule [] [ Γ > Δ > Σ |- [@ga_mk Γ ec a b @@ lev] ] ->
413 ND Rule [] [ Γ > Δ > Σ |- [@ga_mk Γ ec (c,,a) (c,,b) @@ lev] ].
415 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanL ].
416 eapply nd_comp; [ idtac | eapply nd_rule; apply RLet ].
417 eapply nd_comp; [ apply nd_llecnac | idtac ].
420 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RuCanL ].
424 Lemma ga_unkappa : ∀ Γ Δ ec l a b Σ,
426 [Γ > Δ > Σ |- [@ga_mk Γ ec a b @@ l] ]
427 [Γ > Δ > Σ,,[@ga_mk Γ ec [] a @@ l] |- [@ga_mk Γ ec [] b @@ l] ].
429 set (ga_comp Γ Δ ec l [] a b) as q.
431 set (@RLet Γ Δ) as q'.
432 set (@RLet Γ Δ [@ga_mk _ ec [] a @@ l] Σ (@ga_mk _ ec [] b) (@ga_mk _ ec a b) l) as q''.
453 (* useful for cutting down on the pretty-printed noise
455 Notation "` x" := (take_lev _ x) (at level 20).
456 Notation "`` x" := (mapOptionTree unlev x) (at level 20).
457 Notation "``` x" := (drop_lev _ x) (at level 20).
459 Definition flatten_arrangement' :
460 forall Γ (Δ:CoercionEnv Γ)
461 (ec:HaskTyVar Γ ECKind) (lev:HaskLevel Γ) (ant1 ant2:Tree ??(LeveledHaskType Γ ★)) (r:Arrange ant1 ant2),
462 ND Rule [] [Γ > Δ > [] |- [@ga_mk _ (v2t ec) (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) ant2))
463 (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) ant1)) @@ nil] ].
466 refine (fix flatten ant1 ant2 (r:Arrange ant1 ant2):
467 ND Rule [] [Γ > Δ > [] |- [@ga_mk _ (v2t ec)
468 (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) ant2))
469 (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) ant1)) @@ nil]] :=
470 match r as R in Arrange A B return
471 ND Rule [] [Γ > Δ > [] |- [@ga_mk _ (v2t ec)
472 (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) B))
473 (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) A)) @@ nil]]
475 | RCanL a => let case_RCanL := tt in ga_uncancell _ _ _ _ _
476 | RCanR a => let case_RCanR := tt in ga_uncancelr _ _ _ _ _
477 | RuCanL a => let case_RuCanL := tt in ga_cancell _ _ _ _ _
478 | RuCanR a => let case_RuCanR := tt in ga_cancelr _ _ _ _ _
479 | RAssoc a b c => let case_RAssoc := tt in ga_assoc _ _ _ _ _ _ _
480 | RCossa a b c => let case_RCossa := tt in ga_unassoc _ _ _ _ _ _ _
481 | RExch a b => let case_RExch := tt in ga_swap _ _ _ _ _ _
482 | RWeak a => let case_RWeak := tt in ga_drop _ _ _ _ _
483 | RCont a => let case_RCont := tt in ga_copy _ _ _ _ _
484 | RLeft a b c r' => let case_RLeft := tt in flatten _ _ r' ;; boost _ _ _ _ _ (ga_second _ _ _ _ _ _ _)
485 | RRight a b c r' => let case_RRight := tt in flatten _ _ r' ;; boost _ _ _ _ _ (ga_first _ _ _ _ _ _ _)
486 | RComp c b a r1 r2 => let case_RComp := tt in (fun r1' r2' => _) (flatten _ _ r1) (flatten _ _ r2)
487 end); clear flatten; repeat take_simplify; repeat drop_simplify; intros.
490 set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) a)) as a' in *.
491 set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) b)) as b' in *.
492 set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) c)) as c' in *.
493 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RCanL ].
494 eapply nd_comp; [ idtac | eapply nd_rule; apply
495 (@RLet Γ Δ [] [] (@ga_mk _ (v2t ec) a' c') (@ga_mk _ (v2t ec) a' b')) ].
496 eapply nd_comp; [ apply nd_llecnac | idtac ].
499 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RuCanL ].
500 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RCanR ].
501 eapply nd_comp; [ idtac | eapply nd_rule; apply
502 (@RLet Γ Δ [@ga_mk _ (v2t ec) a' b' @@ _] [] (@ga_mk _ (v2t ec) a' c') (@ga_mk _ (v2t ec) b' c'))].
503 eapply nd_comp; [ apply nd_llecnac | idtac ].
509 Definition flatten_arrangement :
510 forall Γ (Δ:CoercionEnv Γ) n
511 (ec:HaskTyVar Γ ECKind) (lev:HaskLevel Γ) (ant1 ant2:Tree ??(LeveledHaskType Γ ★)) (r:Arrange ant1 ant2) succ,
513 [Γ > Δ > mapOptionTree (flatten_leveled_type ) (drop_lev n ant1)
514 |- [@ga_mk _ (v2t ec)
515 (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) ant1))
516 (mapOptionTree (flatten_type ○ unlev) succ) @@ nil]]
517 [Γ > Δ > mapOptionTree (flatten_leveled_type ) (drop_lev n ant2)
518 |- [@ga_mk _ (v2t ec)
519 (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) ant2))
520 (mapOptionTree (flatten_type ○ unlev) succ) @@ nil]].
522 refine ( _ ;; (boost _ _ _ _ _ (postcompose _ _ _ _ _ _ _ (flatten_arrangement' Γ Δ ec lev ant1 ant2 r)))).
525 refine ((fix flatten ant1 ant2 (r:Arrange ant1 ant2) :=
526 match r as R in Arrange A B return
527 Arrange (mapOptionTree (flatten_leveled_type ) (drop_lev _ A))
528 (mapOptionTree (flatten_leveled_type ) (drop_lev _ B)) with
529 | RCanL a => let case_RCanL := tt in RCanL _
530 | RCanR a => let case_RCanR := tt in RCanR _
531 | RuCanL a => let case_RuCanL := tt in RuCanL _
532 | RuCanR a => let case_RuCanR := tt in RuCanR _
533 | RAssoc a b c => let case_RAssoc := tt in RAssoc _ _ _
534 | RCossa a b c => let case_RCossa := tt in RCossa _ _ _
535 | RExch a b => let case_RExch := tt in RExch _ _
536 | RWeak a => let case_RWeak := tt in RWeak _
537 | RCont a => let case_RCont := tt in RCont _
538 | RLeft a b c r' => let case_RLeft := tt in RLeft _ (flatten _ _ r')
539 | RRight a b c r' => let case_RRight := tt in RRight _ (flatten _ _ r')
540 | RComp a b c r1 r2 => let case_RComp := tt in RComp (flatten _ _ r1) (flatten _ _ r2)
541 end) ant1 ant2 r); clear flatten; repeat take_simplify; repeat drop_simplify; intros.
544 Definition flatten_arrangement'' :
545 forall Γ Δ ant1 ant2 succ (r:Arrange ant1 ant2),
546 ND Rule (mapOptionTree (flatten_judgment ) [Γ > Δ > ant1 |- succ])
547 (mapOptionTree (flatten_judgment ) [Γ > Δ > ant2 |- succ]).
550 set (getjlev succ) as succ_lev.
551 assert (succ_lev=getjlev succ).
569 eapply RComp; [ apply IHr1 | apply IHr2 ].
571 apply flatten_arrangement.
575 Definition ga_join Γ Δ Σ₁ Σ₂ a b ec :
576 ND Rule [] [Γ > Δ > Σ₁ |- [@ga_mk _ ec [] a @@ nil]] ->
577 ND Rule [] [Γ > Δ > Σ₂ |- [@ga_mk _ ec [] b @@ nil]] ->
578 ND Rule [] [Γ > Δ > Σ₁,,Σ₂ |- [@ga_mk _ ec [] (a,,b) @@ nil]].
581 apply secondify with (c:=a) in pfb.
584 eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
585 eapply nd_comp; [ eapply nd_llecnac | idtac ].
594 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanL ].
600 Definition arrange_brak : forall Γ Δ ec succ t,
602 [Γ > Δ > mapOptionTree (flatten_leveled_type ) (drop_lev (ec :: nil) succ),,
603 [(@ga_mk _ (v2t ec) []
604 (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: nil) succ)))
605 @@ nil] |- [(@ga_mk _ (v2t ec) [] [flatten_type t]) @@ nil]]
606 [Γ > Δ > mapOptionTree (flatten_leveled_type ) succ |- [(@ga_mk _ (v2t ec) [] [flatten_type t]) @@ nil]].
609 set (@arrange' _ succ (levelMatch (ec::nil))) as q.
610 set (arrangeMap _ _ flatten_leveled_type q) as y.
619 eapply nd_comp; [ apply nd_llecnac | idtac ].
620 eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
625 induction succ; try destruct a; simpl.
631 destruct l as [t' lev'].
632 destruct lev' as [|ec' lev'].
636 set (@eqd_dec (HaskLevel Γ) (haskLevelEqDecidable Γ) (ec' :: lev') (ec :: nil)) as q.
652 Definition arrange_esc : forall Γ Δ ec succ t,
654 [Γ > Δ > mapOptionTree (flatten_leveled_type ) succ |- [(@ga_mk _ (v2t ec) [] [flatten_type t]) @@ nil]]
655 [Γ > Δ > mapOptionTree (flatten_leveled_type ) (drop_lev (ec :: nil) succ),,
656 [(@ga_mk _ (v2t ec) []
657 (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: nil) succ))) @@ nil]
658 |- [(@ga_mk _ (v2t ec) [] [flatten_type t]) @@ nil]].
661 set (@arrange _ succ (levelMatch (ec::nil))) as q.
662 set (arrangeMap _ _ flatten_leveled_type q) as y.
674 unfold mkDropFlags; simpl.
678 destruct (General.list_eq_dec h0 (ec :: nil)).
680 unfold flatten_leveled_type'.
695 apply (Prelude_error "escapifying code with multi-leaf antecedents is not supported").
698 Lemma mapOptionTree_distributes
699 : forall T R (a b:Tree ??T) (f:T->R),
700 mapOptionTree f (a,,b) = (mapOptionTree f a),,(mapOptionTree f b).
704 Definition decide_tree_empty : forall {T:Type}(t:Tree ??T),
705 sum { q:Tree unit & t = mapTree (fun _ => None) q } unit.
710 | T_Branch b1 b2 => let b1' := foo b1 in let b2' := foo b2 in _
730 Definition flatten_proof :
733 ND Rule (mapOptionTree (flatten_judgment ) h) (mapOptionTree (flatten_judgment ) c).
735 eapply nd_map'; [ idtac | apply X ].
740 refine (match X as R in Rule H C with
741 | RArrange Γ Δ a b x d => let case_RArrange := tt in _
742 | RNote Γ Δ Σ τ l n => let case_RNote := tt in _
743 | RLit Γ Δ l _ => let case_RLit := tt in _
744 | RVar Γ Δ σ lev => let case_RVar := tt in _
745 | RGlobal Γ Δ σ l wev => let case_RGlobal := tt in _
746 | RLam Γ Δ Σ tx te lev => let case_RLam := tt in _
747 | RCast Γ Δ Σ σ τ lev γ => let case_RCast := tt in _
748 | RAbsT Γ Δ Σ κ σ lev => let case_RAbsT := tt in _
749 | RAppT Γ Δ Σ κ σ τ lev => let case_RAppT := tt in _
750 | RAppCo Γ Δ Σ κ σ₁ σ₂ γ σ lev => let case_RAppCo := tt in _
751 | RAbsCo Γ Δ Σ κ σ σ₁ σ₂ lev => let case_RAbsCo := tt in _
752 | RApp Γ Δ Σ₁ Σ₂ tx te lev => let case_RApp := tt in _
753 | RLet Γ Δ Σ₁ Σ₂ σ₁ σ₂ lev => let case_RLet := tt in _
754 | RJoin Γ p lri m x q => let case_RJoin := tt in _
755 | RVoid _ _ => let case_RVoid := tt in _
756 | RBrak Γ Δ t ec succ lev => let case_RBrak := tt in _
757 | REsc Γ Δ t ec succ lev => let case_REsc := tt in _
758 | RCase Γ Δ lev tc Σ avars tbranches alts => let case_RCase := tt in _
759 | RLetRec Γ Δ lri x y t => let case_RLetRec := tt in _
762 destruct case_RArrange.
763 apply (flatten_arrangement'' Γ Δ a b x d).
768 change ([flatten_type (<[ ec |- t ]>) @@ nil])
769 with ([ga_mk (v2t ec) [] [flatten_type t] @@ nil]).
770 refine (ga_unkappa Γ Δ (v2t ec) nil (mapOptionTree (flatten_type ○ unlev) (take_lev (ec::nil) succ)) _
771 (mapOptionTree (flatten_leveled_type) (drop_lev (ec::nil) succ)) ;; _ ).
773 apply (Prelude_error "found Brak at depth >0 indicating 3-level code; only two-level code is currently supported").
779 change ([flatten_type (<[ ec |- t ]>) @@ nil])
780 with ([ga_mk (v2t ec) [] [flatten_type t] @@ nil]).
781 eapply nd_comp; [ apply arrange_esc | idtac ].
782 set (decide_tree_empty (take_lev (ec :: nil) succ)) as q'.
788 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanR ].
789 eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
790 eapply nd_comp; [ apply nd_llecnac | idtac ].
791 apply nd_prod; [ idtac | eapply boost ].
794 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanR ].
803 (* environment has non-empty leaves *)
804 apply (ga_kappa Γ Δ (v2t ec) nil (mapOptionTree (flatten_type ○ unlev) (take_lev (ec::nil) succ)) _ _).
805 apply (Prelude_error "found Esc at depth >0 indicating 3-level code; only two-level code is currently supported").
810 apply nd_rule; apply RNote; auto.
811 apply nd_rule; apply RNote; auto.
816 rewrite literal_types_unchanged.
817 apply nd_rule; apply RLit.
818 unfold take_lev; simpl.
819 unfold drop_lev; simpl.
821 rewrite literal_types_unchanged.
825 Opaque flatten_judgment.
827 Transparent flatten_judgment.
829 unfold flatten_judgment.
832 apply nd_rule. apply RVar.
833 repeat drop_simplify.
834 repeat take_simplify.
838 destruct case_RGlobal.
842 destruct l as [|ec lev]; simpl.
843 destruct (eqd_dec (g:CoreVar) (hetmet_flatten:CoreVar)).
844 set (flatten_type (g wev)) as t.
845 set (RGlobal _ Δ nil (mkGlobal Γ t hetmet_id)) as q.
850 destruct (eqd_dec (g:CoreVar) (hetmet_unflatten:CoreVar)).
851 set (flatten_type (g wev)) as t.
852 set (RGlobal _ Δ nil (mkGlobal Γ t hetmet_id)) as q.
857 apply nd_rule; rewrite globals_do_not_have_code_types.
859 apply (Prelude_error "found RGlobal at depth >0; globals should never appear inside code brackets unless escaped").
865 destruct lev as [|ec lev]; simpl; [ apply nd_rule; apply RLam; auto | idtac ].
866 repeat drop_simplify.
867 repeat take_simplify.
879 destruct lev as [|ec lev]; simpl; [ apply nd_rule; apply RCast; auto | idtac ].
880 apply flatten_coercion; auto.
881 apply (Prelude_error "RCast at level >0; casting inside of code brackets is currently not supported").
885 destruct (getjlev x); destruct (getjlev q);
886 [ apply nd_rule; apply RJoin | idtac | idtac | idtac ];
887 apply (Prelude_error "RJoin at depth >0").
892 destruct lev as [|ec lev]. simpl. apply nd_rule.
893 replace (flatten_type (tx ---> te)) with ((flatten_type tx) ---> (flatten_type te)).
897 repeat drop_simplify.
898 repeat take_simplify.
899 rewrite mapOptionTree_distributes.
900 set (mapOptionTree (flatten_leveled_type ) (drop_lev (ec :: lev) Σ₁)) as Σ₁'.
901 set (mapOptionTree (flatten_leveled_type ) (drop_lev (ec :: lev) Σ₂)) as Σ₂'.
902 set (take_lev (ec :: lev) Σ₁) as Σ₁''.
903 set (take_lev (ec :: lev) Σ₂) as Σ₂''.
904 replace (flatten_type (tx ---> te)) with ((flatten_type tx) ---> (flatten_type te)).
905 apply (Prelude_error "FIXME: ga_apply").
909 Notation "` x" := (take_lev _ x).
910 Notation "`` x" := (mapOptionTree unlev x) (at level 20).
911 Notation "``` x" := ((drop_lev _ x)) (at level 20).
912 Notation "!<[]> x" := (flatten_type _ x) (at level 1).
913 Notation "!<[@]> x" := (mapOptionTree flatten_leveled_type x) (at level 1).
918 destruct lev as [|ec lev]; simpl; [ apply nd_rule; apply RLet; auto | idtac ].
919 repeat drop_simplify.
920 repeat take_simplify.
924 eapply nd_prod; [ idtac | apply nd_id ].
946 simpl. destruct lev; simpl.
947 rewrite flatten_commutes_with_HaskTAll.
948 rewrite flatten_commutes_with_substT.
953 apply (Prelude_error "found type application at level >0; this is not supported").
956 simpl. destruct lev; simpl.
957 rewrite flatten_commutes_with_HaskTAll.
958 rewrite flatten_commutes_with_HaskTApp.
959 eapply nd_comp; [ idtac | eapply nd_rule; eapply RAbsT ].
961 set (mapOptionTree (flatten_leveled_type ) (mapOptionTree (weakLT(κ:=κ)) Σ)) as a.
962 set (mapOptionTree (weakLT(κ:=κ)) (mapOptionTree (flatten_leveled_type ) Σ)) as q'.
970 rewrite flatten_commutes_with_weakLT.
981 apply (Prelude_error "found type abstraction at level >0; this is not supported").
983 destruct case_RAppCo.
984 simpl. destruct lev; simpl.
989 apply flatten_coercion.
991 apply (Prelude_error "found coercion application at level >0; this is not supported").
993 destruct case_RAbsCo.
994 simpl. destruct lev; simpl.
997 apply (Prelude_error "AbsCo not supported (FIXME)").
998 apply (Prelude_error "found coercion abstraction at level >0; this is not supported").
1000 destruct case_RLetRec.
1003 apply (Prelude_error "LetRec not supported (FIXME)").
1005 destruct case_RCase.
1007 apply (Prelude_error "Case not supported (BIG FIXME)").
1011 (* to do: establish some metric on judgments (max length of level of any succedent type, probably), show how to
1012 * calculate it, and show that the flattening procedure above drives it down by one *)
1015 Instance FlatteningFunctor {Γ}{Δ}{ec} : Functor (JudgmentsL (PCF Γ Δ ec)) (TypesL (SystemFCa Γ Δ)) (obact) :=
1016 { fmor := FlatteningFunctor_fmor }.
1018 Definition ReificationFunctor Γ Δ : Functor (JudgmentsL _ _ (PCF n Γ Δ)) SystemFCa' (mapOptionTree brakifyJudg).
1019 refine {| fmor := ReificationFunctor_fmor Γ Δ |}; unfold hom; unfold ob; simpl ; intros.
1021 Definition PCF_SMME (n:nat)(Γ:TypeEnv)(Δ:CoercionEnv Γ) : ProgrammingLanguageSMME.
1022 refine {| plsmme_pl := PCF n Γ Δ |}.
1025 Definition SystemFCa_SMME (n:nat)(Γ:TypeEnv)(Δ:CoercionEnv Γ) : ProgrammingLanguageSMME.
1026 refine {| plsmme_pl := SystemFCa n Γ Δ |}.
1029 Definition ReificationFunctorMonoidal n : MonoidalFunctor (JudgmentsN n) (JudgmentsN (S n)) (ReificationFunctor n).
1033 Definition PCF_SystemFCa_two_level n Γ Δ : TwoLevelLanguage (PCF_SMME n Γ Δ) (SystemFCa_SMME (S n) Γ Δ).
1036 (* ... and the retraction exists *)
1040 Implicit Arguments garrow [ ].