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.
46 Definition getlev {Γ}{κ}(lht:LeveledHaskType Γ κ) : HaskLevel Γ :=
47 match lht with t @@ l => l end.
50 forall {T} (Σ:Tree ??T) (f:T -> bool),
51 Arrange Σ (dropT (mkFlags (liftBoolFunc false f) Σ),,( (dropT (mkFlags (liftBoolFunc false (bnot ○ f)) Σ)))).
57 destruct (f t); simpl.
63 eapply RComp; [ idtac | apply arrangeSwapMiddle ].
72 forall {T} (Σ:Tree ??T) (f:T -> bool),
73 Arrange (dropT (mkFlags (liftBoolFunc false f) Σ),,( (dropT (mkFlags (liftBoolFunc false (bnot ○ f)) Σ)))) Σ.
79 destruct (f t); simpl.
85 eapply RComp; [ apply arrangeSwapMiddle | idtac ].
95 | [ |- context[@eqd_dec ?T ?V ?X ?X] ] =>
96 destruct (@eqd_dec T V X X) as [eqd_dec1 | eqd_dec2];
97 [ clear eqd_dec1 | set (eqd_dec2 (refl_equal _)) as eqd_dec2'; inversion eqd_dec2' ]
100 Definition v2t {Γ}(ec:HaskTyVar Γ ECKind) : HaskType Γ ECKind := fun TV ite => TVar (ec TV ite).
102 Definition levelMatch {Γ}(lev:HaskLevel Γ) : LeveledHaskType Γ ★ -> bool :=
103 fun t => match t with ttype@@tlev => if eqd_dec tlev lev then true else false end.
105 (* In a tree of types, replace any type at depth "lev" or greater None *)
106 Definition mkDropFlags {Γ}(lev:HaskLevel Γ)(tt:Tree ??(LeveledHaskType Γ ★)) : TreeFlags tt :=
107 mkFlags (liftBoolFunc false (levelMatch lev)) tt.
109 Definition drop_lev {Γ}(lev:HaskLevel Γ)(tt:Tree ??(LeveledHaskType Γ ★)) : Tree ??(LeveledHaskType Γ ★) :=
110 dropT (mkDropFlags lev tt).
112 (* The opposite: replace any type which is NOT at level "lev" with None *)
113 Definition mkTakeFlags {Γ}(lev:HaskLevel Γ)(tt:Tree ??(LeveledHaskType Γ ★)) : TreeFlags tt :=
114 mkFlags (liftBoolFunc true (bnot ○ levelMatch lev)) tt.
116 Definition take_lev {Γ}(lev:HaskLevel Γ)(tt:Tree ??(LeveledHaskType Γ ★)) : Tree ??(LeveledHaskType Γ ★) :=
117 dropT (mkTakeFlags lev tt).
119 mapOptionTree (fun x => flatten_type (unlev x))
120 (maybeTree (takeT tt (mkFlags (
121 fun t => match t with
122 | Some (ttype @@ tlev) => if eqd_dec tlev lev then true else false
127 Definition maybeTree {T}(t:??(Tree ??T)) : Tree ??T :=
134 Lemma drop_lev_lemma : forall Γ (lev:HaskLevel Γ) x, drop_lev lev [x @@ lev] = [].
146 Lemma drop_lev_lemma_s : forall Γ (lev:HaskLevel Γ) ec x, drop_lev (ec::lev) [x @@ (ec :: lev)] = [].
157 Lemma take_lemma : forall Γ (lev:HaskLevel Γ) x, take_lev lev [x @@ lev] = [x @@ lev].
168 Ltac drop_simplify :=
170 | [ |- context[@drop_lev ?G ?L [ ?X @@ ?L ] ] ] =>
171 rewrite (drop_lev_lemma G L X)
172 | [ |- context[@drop_lev ?G (?E :: ?L) [ ?X @@ (?E :: ?L) ] ] ] =>
173 rewrite (drop_lev_lemma_s G L E X)
174 | [ |- context[@drop_lev ?G ?N (?A,,?B)] ] =>
175 change (@drop_lev G N (A,,B)) with ((@drop_lev G N A),,(@drop_lev G N B))
176 | [ |- context[@drop_lev ?G ?N (T_Leaf None)] ] =>
177 change (@drop_lev G N (T_Leaf (@None (LeveledHaskType G ★)))) with (T_Leaf (@None (LeveledHaskType G ★)))
180 Ltac take_simplify :=
182 | [ |- context[@take_lev ?G ?L [ ?X @@ ?L ] ] ] =>
183 rewrite (take_lemma G L X)
184 | [ |- context[@take_lev ?G ?N (?A,,?B)] ] =>
185 change (@take_lev G N (A,,B)) with ((@take_lev G N A),,(@take_lev G N B))
186 | [ |- context[@take_lev ?G ?N (T_Leaf None)] ] =>
187 change (@take_lev G N (T_Leaf (@None (LeveledHaskType G ★)))) with (T_Leaf (@None (LeveledHaskType G ★)))
191 (*******************************************************************************)
194 Context (hetmet_flatten : WeakExprVar).
195 Context (hetmet_unflatten : WeakExprVar).
196 Context (hetmet_id : WeakExprVar).
197 Context {unitTy : forall TV, RawHaskType TV ECKind -> RawHaskType TV ★ }.
198 Context {prodTy : forall TV, RawHaskType TV ECKind -> RawHaskType TV ★ -> RawHaskType TV ★ -> RawHaskType TV ★ }.
199 Context {gaTy : forall TV, RawHaskType TV ECKind -> RawHaskType TV ★ -> RawHaskType TV ★ -> RawHaskType TV ★ }.
201 Definition ga_mk_tree' {TV}(ec:RawHaskType TV ECKind)(tr:Tree ??(RawHaskType TV ★)) : RawHaskType TV ★ :=
202 reduceTree (unitTy TV ec) (prodTy TV ec) tr.
204 Definition ga_mk_tree {Γ}(ec:HaskType Γ ECKind)(tr:Tree ??(HaskType Γ ★)) : HaskType Γ ★ :=
205 fun TV ite => ga_mk_tree' (ec TV ite) (mapOptionTree (fun x => x TV ite) tr).
207 Definition ga_mk_raw {TV}(ec:RawHaskType TV ECKind )(ant suc:Tree ??(RawHaskType TV ★)) : RawHaskType TV ★ :=
208 gaTy TV ec (ga_mk_tree' ec ant) (ga_mk_tree' ec suc).
210 Definition ga_mk {Γ}(ec:HaskType Γ ECKind )(ant suc:Tree ??(HaskType Γ ★)) : HaskType Γ ★ :=
211 fun TV ite => ga_mk_raw (ec TV ite) (mapOptionTree (fun x => x TV ite) ant) (mapOptionTree (fun x => x TV ite) suc).
215 * - code types <[t]>@c become garrows c () t
216 * - free variables of type t at a level lev deeper than the succedent become garrows c () t
217 * - free variables at the level of the succedent become
219 Fixpoint flatten_rawtype {TV}{κ}(exp: RawHaskType TV κ) : RawHaskType TV κ :=
222 | TAll _ y => TAll _ (fun v => flatten_rawtype (y v))
223 | TApp _ _ x y => TApp (flatten_rawtype x) (flatten_rawtype y)
225 | TCoerc _ t1 t2 t => TCoerc (flatten_rawtype t1) (flatten_rawtype t2) (flatten_rawtype t)
227 | TCode ec e => ga_mk_raw ec [] [flatten_rawtype e]
228 | TyFunApp tfc kl k lt => TyFunApp tfc kl k (flatten_rawtype_list _ lt)
230 with flatten_rawtype_list {TV}(lk:list Kind)(exp:@RawHaskTypeList TV lk) : @RawHaskTypeList TV lk :=
231 match exp in @RawHaskTypeList _ LK return @RawHaskTypeList TV LK with
232 | TyFunApp_nil => TyFunApp_nil
233 | TyFunApp_cons κ kl t rest => TyFunApp_cons _ _ (flatten_rawtype t) (flatten_rawtype_list _ rest)
236 Definition flatten_type {Γ}{κ}(ht:HaskType Γ κ) : HaskType Γ κ :=
237 fun TV ite => flatten_rawtype (ht TV ite).
239 Fixpoint levels_to_tcode {Γ}(ht:HaskType Γ ★)(lev:HaskLevel Γ) : HaskType Γ ★ :=
242 | ec::lev' => fun TV ite => TCode (v2t ec TV ite) (levels_to_tcode ht lev' TV ite)
245 Definition flatten_leveled_type {Γ}(ht:LeveledHaskType Γ ★) : LeveledHaskType Γ ★ :=
246 flatten_type (levels_to_tcode (unlev ht) (getlev ht)) @@ nil.
250 Axiom literal_types_unchanged : forall Γ l, flatten_type (literalType l) = literalType(Γ:=Γ) l.
252 Axiom flatten_coercion : forall Γ Δ κ (σ τ:HaskType Γ κ) (γ:HaskCoercion Γ Δ (σ ∼∼∼ τ)),
253 HaskCoercion Γ Δ (flatten_type σ ∼∼∼ flatten_type τ).
255 Axiom flatten_commutes_with_substT :
256 forall κ Γ (Δ:CoercionEnv Γ) (σ:∀ TV, InstantiatedTypeEnv TV Γ → TV κ → RawHaskType TV ★) (τ:HaskType Γ κ),
257 flatten_type (substT σ τ) = substT (fun TV ite v => flatten_rawtype (σ TV ite v))
260 Axiom flatten_commutes_with_HaskTAll :
261 forall κ Γ (Δ:CoercionEnv Γ) (σ:∀ TV, InstantiatedTypeEnv TV Γ → TV κ → RawHaskType TV ★),
262 flatten_type (HaskTAll κ σ) = HaskTAll κ (fun TV ite v => flatten_rawtype (σ TV ite v)).
264 Axiom flatten_commutes_with_HaskTApp :
265 forall κ Γ (Δ:CoercionEnv Γ) (σ:∀ TV, InstantiatedTypeEnv TV Γ → TV κ → RawHaskType TV ★),
266 flatten_type (HaskTApp (weakF σ) (FreshHaskTyVar κ)) =
267 HaskTApp (weakF (fun TV ite v => flatten_rawtype (σ TV ite v))) (FreshHaskTyVar κ).
269 Axiom flatten_commutes_with_weakLT : forall (Γ:TypeEnv) κ t,
270 flatten_leveled_type (weakLT(Γ:=Γ)(κ:=κ) t) = weakLT(Γ:=Γ)(κ:=κ) (flatten_leveled_type t).
272 Axiom globals_do_not_have_code_types : forall (Γ:TypeEnv) (g:Global Γ) v,
273 flatten_type (g v) = g v.
275 (* This tries to assign a single level to the entire succedent of a judgment. If the succedent has types from different
276 * levels (should not happen) it just picks one; if the succedent has no non-None leaves (also should not happen) it
278 Definition getΓ (j:Judg) := match j with Γ > _ > _ |- _ => Γ end.
279 Definition getSuc (j:Judg) : Tree ??(LeveledHaskType (getΓ j) ★) :=
280 match j as J return Tree ??(LeveledHaskType (getΓ J) ★) with Γ > _ > _ |- s => s end.
281 Fixpoint getjlev {Γ}(tt:Tree ??(LeveledHaskType Γ ★)) : HaskLevel Γ :=
284 | T_Leaf (Some (_ @@ lev)) => lev
286 match getjlev b1 with
292 (* "n" is the maximum depth remaining AFTER flattening *)
293 Definition flatten_judgment (j:Judg) :=
294 match j as J return Judg with
295 Γ > Δ > ant |- suc =>
296 match getjlev suc with
297 | nil => Γ > Δ > mapOptionTree flatten_leveled_type ant
298 |- mapOptionTree flatten_leveled_type suc
300 | (ec::lev') => Γ > Δ > mapOptionTree flatten_leveled_type (drop_lev (ec::lev') ant)
302 (mapOptionTree (flatten_type ○ unlev) (take_lev (ec::lev') ant))
303 (mapOptionTree (flatten_type ○ unlev) suc )
304 @@ nil] (* we know the level of all of suc *)
309 { ga_id : ∀ Γ Δ ec l a , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec a a @@ l] ]
310 ; ga_cancelr : ∀ Γ Δ ec l a , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec (a,,[]) a @@ l] ]
311 ; ga_cancell : ∀ Γ Δ ec l a , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec ([],,a) a @@ l] ]
312 ; ga_uncancelr : ∀ Γ Δ ec l a , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec a (a,,[]) @@ l] ]
313 ; ga_uncancell : ∀ Γ Δ ec l a , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec a ([],,a) @@ l] ]
314 ; ga_assoc : ∀ Γ Δ ec l a b c, ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec ((a,,b),,c) (a,,(b,,c)) @@ l] ]
315 ; ga_unassoc : ∀ Γ Δ ec l a b c, ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec (a,,(b,,c)) ((a,,b),,c) @@ l] ]
316 ; ga_swap : ∀ Γ Δ ec l a b , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec (a,,b) (b,,a) @@ l] ]
317 ; ga_drop : ∀ Γ Δ ec l a , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec a [] @@ l] ]
318 ; ga_copy : ∀ Γ Δ ec l a , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec a (a,,a) @@ l] ]
319 ; ga_first : ∀ Γ Δ ec l a b x, ND Rule [] [Γ > Δ > [@ga_mk Γ ec a b @@ l] |- [@ga_mk Γ ec (a,,x) (b,,x) @@ l] ]
320 ; ga_second : ∀ Γ Δ ec l a b x, ND Rule [] [Γ > Δ > [@ga_mk Γ ec a b @@ l] |- [@ga_mk Γ ec (x,,a) (x,,b) @@ l] ]
321 ; ga_lit : ∀ Γ Δ ec l lit , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec [] [literalType lit] @@ l] ]
322 ; ga_curry : ∀ Γ Δ ec l a b c, ND Rule [] [Γ > Δ > [@ga_mk Γ ec (a,,[b]) [c] @@ l] |- [@ga_mk Γ ec a [b ---> c] @@ l] ]
323 ; 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] ]
324 ; ga_apply : ∀ Γ Δ ec l a a' b c,
325 ND Rule [] [Γ > Δ > [@ga_mk Γ ec a [b ---> c] @@ l],,[@ga_mk Γ ec a' [b] @@ l] |- [@ga_mk Γ ec (a,,a') [c] @@ l] ]
326 ; ga_kappa : ∀ Γ Δ ec l a b Σ, ND Rule
327 [Γ > Δ > Σ,,[@ga_mk Γ ec [] a @@ l] |- [@ga_mk Γ ec [] b @@ l] ]
328 [Γ > Δ > Σ |- [@ga_mk Γ ec a b @@ l] ]
330 Context `(gar:garrow).
332 Notation "a ~~~~> b" := (@ga_mk _ _ a b) (at level 20).
334 Definition boost : forall Γ Δ ant x y {lev},
335 ND Rule [] [ Γ > Δ > [x@@lev] |- [y@@lev] ] ->
336 ND Rule [ Γ > Δ > ant |- [x@@lev] ] [ Γ > Δ > ant |- [y@@lev] ].
338 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanL ].
339 eapply nd_comp; [ idtac | eapply nd_rule; apply (@RLet Γ Δ [] ant y x lev) ].
340 eapply nd_comp; [ apply nd_rlecnac | idtac ].
350 Definition postcompose' : ∀ Γ Δ ec lev a b c Σ,
351 ND Rule [] [ Γ > Δ > Σ |- [@ga_mk Γ ec a b @@ lev] ] ->
352 ND Rule [] [ Γ > Δ > Σ,,[@ga_mk Γ ec b c @@ lev] |- [@ga_mk Γ ec a c @@ lev] ].
354 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RExch ].
355 eapply nd_comp; [ idtac
356 | eapply nd_rule; apply (@RLet Γ Δ [@ga_mk _ ec b c @@lev] Σ (@ga_mk _ ec a c) (@ga_mk _ ec a b) lev) ].
357 eapply nd_comp; [ apply nd_llecnac | idtac ].
360 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RExch ].
364 Definition precompose Γ Δ ec : forall a x y z lev,
366 [ Γ > Δ > a |- [@ga_mk _ ec y z @@ lev] ]
367 [ Γ > Δ > a,,[@ga_mk _ ec x y @@ lev] |- [@ga_mk _ ec x z @@ lev] ].
376 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RExch ].
382 Definition precompose' : ∀ Γ Δ ec lev a b c Σ,
383 ND Rule [] [ Γ > Δ > Σ |- [@ga_mk Γ ec b c @@ lev] ] ->
384 ND Rule [] [ Γ > Δ > Σ,,[@ga_mk Γ ec a b @@ lev] |- [@ga_mk Γ ec a c @@ lev] ].
391 Definition postcompose : ∀ Γ Δ ec lev a b c,
392 ND Rule [] [ Γ > Δ > [] |- [@ga_mk Γ ec a b @@ lev] ] ->
393 ND Rule [] [ Γ > Δ > [@ga_mk Γ ec b c @@ lev] |- [@ga_mk Γ ec a c @@ lev] ].
403 Definition firstify : ∀ Γ Δ ec lev a b c Σ,
404 ND Rule [] [ Γ > Δ > Σ |- [@ga_mk Γ ec a b @@ lev] ] ->
405 ND Rule [] [ Γ > Δ > Σ |- [@ga_mk Γ ec (a,,c) (b,,c) @@ lev] ].
407 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanL ].
408 eapply nd_comp; [ idtac | eapply nd_rule; apply RLet ].
409 eapply nd_comp; [ apply nd_llecnac | idtac ].
412 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RuCanL ].
416 Definition secondify : ∀ Γ Δ ec lev a b c Σ,
417 ND Rule [] [ Γ > Δ > Σ |- [@ga_mk Γ ec a b @@ lev] ] ->
418 ND Rule [] [ Γ > Δ > Σ |- [@ga_mk Γ ec (c,,a) (c,,b) @@ lev] ].
420 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanL ].
421 eapply nd_comp; [ idtac | eapply nd_rule; apply RLet ].
422 eapply nd_comp; [ apply nd_llecnac | idtac ].
425 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RuCanL ].
429 Lemma ga_unkappa : ∀ Γ Δ ec l a b Σ,
431 [Γ > Δ > Σ |- [@ga_mk Γ ec a b @@ l] ]
432 [Γ > Δ > Σ,,[@ga_mk Γ ec [] a @@ l] |- [@ga_mk Γ ec [] b @@ l] ].
434 set (ga_comp Γ Δ ec l [] a b) as q.
436 set (@RLet Γ Δ) as q'.
437 set (@RLet Γ Δ [@ga_mk _ ec [] a @@ l] Σ (@ga_mk _ ec [] b) (@ga_mk _ ec a b) l) as q''.
458 (* useful for cutting down on the pretty-printed noise
460 Notation "` x" := (take_lev _ x) (at level 20).
461 Notation "`` x" := (mapOptionTree unlev x) (at level 20).
462 Notation "``` x" := (drop_lev _ x) (at level 20).
464 Definition flatten_arrangement' :
465 forall Γ (Δ:CoercionEnv Γ)
466 (ec:HaskTyVar Γ ECKind) (lev:HaskLevel Γ) (ant1 ant2:Tree ??(LeveledHaskType Γ ★)) (r:Arrange ant1 ant2),
467 ND Rule [] [Γ > Δ > [] |- [@ga_mk _ (v2t ec) (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) ant2))
468 (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) ant1)) @@ nil] ].
471 refine (fix flatten ant1 ant2 (r:Arrange ant1 ant2):
472 ND Rule [] [Γ > Δ > [] |- [@ga_mk _ (v2t ec)
473 (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) ant2))
474 (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) ant1)) @@ nil]] :=
475 match r as R in Arrange A B return
476 ND Rule [] [Γ > Δ > [] |- [@ga_mk _ (v2t ec)
477 (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) B))
478 (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) A)) @@ nil]]
480 | RCanL a => let case_RCanL := tt in ga_uncancell _ _ _ _ _
481 | RCanR a => let case_RCanR := tt in ga_uncancelr _ _ _ _ _
482 | RuCanL a => let case_RuCanL := tt in ga_cancell _ _ _ _ _
483 | RuCanR a => let case_RuCanR := tt in ga_cancelr _ _ _ _ _
484 | RAssoc a b c => let case_RAssoc := tt in ga_assoc _ _ _ _ _ _ _
485 | RCossa a b c => let case_RCossa := tt in ga_unassoc _ _ _ _ _ _ _
486 | RExch a b => let case_RExch := tt in ga_swap _ _ _ _ _ _
487 | RWeak a => let case_RWeak := tt in ga_drop _ _ _ _ _
488 | RCont a => let case_RCont := tt in ga_copy _ _ _ _ _
489 | RLeft a b c r' => let case_RLeft := tt in flatten _ _ r' ;; boost _ _ _ _ _ (ga_second _ _ _ _ _ _ _)
490 | RRight a b c r' => let case_RRight := tt in flatten _ _ r' ;; boost _ _ _ _ _ (ga_first _ _ _ _ _ _ _)
491 | RComp c b a r1 r2 => let case_RComp := tt in (fun r1' r2' => _) (flatten _ _ r1) (flatten _ _ r2)
492 end); clear flatten; repeat take_simplify; repeat drop_simplify; intros.
495 set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) a)) as a' in *.
496 set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) b)) as b' in *.
497 set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) c)) as c' in *.
498 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RCanL ].
499 eapply nd_comp; [ idtac | eapply nd_rule; apply
500 (@RLet Γ Δ [] [] (@ga_mk _ (v2t ec) a' c') (@ga_mk _ (v2t ec) a' b')) ].
501 eapply nd_comp; [ apply nd_llecnac | idtac ].
504 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RuCanL ].
505 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RCanR ].
506 eapply nd_comp; [ idtac | eapply nd_rule; apply
507 (@RLet Γ Δ [@ga_mk _ (v2t ec) a' b' @@ _] [] (@ga_mk _ (v2t ec) a' c') (@ga_mk _ (v2t ec) b' c'))].
508 eapply nd_comp; [ apply nd_llecnac | idtac ].
514 Definition flatten_arrangement :
515 forall Γ (Δ:CoercionEnv Γ) n
516 (ec:HaskTyVar Γ ECKind) (lev:HaskLevel Γ) (ant1 ant2:Tree ??(LeveledHaskType Γ ★)) (r:Arrange ant1 ant2) succ,
518 [Γ > Δ > mapOptionTree (flatten_leveled_type ) (drop_lev n ant1)
519 |- [@ga_mk _ (v2t ec)
520 (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) ant1))
521 (mapOptionTree (flatten_type ○ unlev) succ) @@ nil]]
522 [Γ > Δ > mapOptionTree (flatten_leveled_type ) (drop_lev n ant2)
523 |- [@ga_mk _ (v2t ec)
524 (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) ant2))
525 (mapOptionTree (flatten_type ○ unlev) succ) @@ nil]].
527 refine ( _ ;; (boost _ _ _ _ _ (postcompose _ _ _ _ _ _ _ (flatten_arrangement' Γ Δ ec lev ant1 ant2 r)))).
530 refine ((fix flatten ant1 ant2 (r:Arrange ant1 ant2) :=
531 match r as R in Arrange A B return
532 Arrange (mapOptionTree (flatten_leveled_type ) (drop_lev _ A))
533 (mapOptionTree (flatten_leveled_type ) (drop_lev _ B)) with
534 | RCanL a => let case_RCanL := tt in RCanL _
535 | RCanR a => let case_RCanR := tt in RCanR _
536 | RuCanL a => let case_RuCanL := tt in RuCanL _
537 | RuCanR a => let case_RuCanR := tt in RuCanR _
538 | RAssoc a b c => let case_RAssoc := tt in RAssoc _ _ _
539 | RCossa a b c => let case_RCossa := tt in RCossa _ _ _
540 | RExch a b => let case_RExch := tt in RExch _ _
541 | RWeak a => let case_RWeak := tt in RWeak _
542 | RCont a => let case_RCont := tt in RCont _
543 | RLeft a b c r' => let case_RLeft := tt in RLeft _ (flatten _ _ r')
544 | RRight a b c r' => let case_RRight := tt in RRight _ (flatten _ _ r')
545 | RComp a b c r1 r2 => let case_RComp := tt in RComp (flatten _ _ r1) (flatten _ _ r2)
546 end) ant1 ant2 r); clear flatten; repeat take_simplify; repeat drop_simplify; intros.
549 Definition flatten_arrangement'' :
550 forall Γ Δ ant1 ant2 succ (r:Arrange ant1 ant2),
551 ND Rule (mapOptionTree (flatten_judgment ) [Γ > Δ > ant1 |- succ])
552 (mapOptionTree (flatten_judgment ) [Γ > Δ > ant2 |- succ]).
555 set (getjlev succ) as succ_lev.
556 assert (succ_lev=getjlev succ).
574 eapply RComp; [ apply IHr1 | apply IHr2 ].
576 apply flatten_arrangement.
580 Definition ga_join Γ Δ Σ₁ Σ₂ a b ec :
581 ND Rule [] [Γ > Δ > Σ₁ |- [@ga_mk _ ec [] a @@ nil]] ->
582 ND Rule [] [Γ > Δ > Σ₂ |- [@ga_mk _ ec [] b @@ nil]] ->
583 ND Rule [] [Γ > Δ > Σ₁,,Σ₂ |- [@ga_mk _ ec [] (a,,b) @@ nil]].
586 apply secondify with (c:=a) in pfb.
589 eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
590 eapply nd_comp; [ eapply nd_llecnac | idtac ].
599 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanL ].
605 Definition arrange_brak : forall Γ Δ ec succ t,
607 [Γ > Δ > mapOptionTree (flatten_leveled_type ) (drop_lev (ec :: nil) succ),,
608 [(@ga_mk _ (v2t ec) []
609 (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: nil) succ)))
610 @@ nil] |- [(@ga_mk _ (v2t ec) [] [flatten_type t]) @@ nil]]
611 [Γ > Δ > mapOptionTree (flatten_leveled_type ) succ |- [(@ga_mk _ (v2t ec) [] [flatten_type t]) @@ nil]].
614 set (@arrange' _ succ (levelMatch (ec::nil))) as q.
615 set (arrangeMap _ _ flatten_leveled_type q) as y.
624 eapply nd_comp; [ apply nd_llecnac | idtac ].
625 eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
630 induction succ; try destruct a; simpl.
636 destruct l as [t' lev'].
637 destruct lev' as [|ec' lev'].
641 set (@eqd_dec (HaskLevel Γ) (haskLevelEqDecidable Γ) (ec' :: lev') (ec :: nil)) as q.
646 unfold flatten_leveled_type.
660 Definition arrange_esc : forall Γ Δ ec succ t,
662 [Γ > Δ > mapOptionTree (flatten_leveled_type ) succ |- [(@ga_mk _ (v2t ec) [] [flatten_type t]) @@ nil]]
663 [Γ > Δ > mapOptionTree (flatten_leveled_type ) (drop_lev (ec :: nil) succ),,
664 [(@ga_mk _ (v2t ec) []
665 (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: nil) succ))) @@ nil]
666 |- [(@ga_mk _ (v2t ec) [] [flatten_type t]) @@ nil]].
669 set (@arrange _ succ (levelMatch (ec::nil))) as q.
670 set (arrangeMap _ _ flatten_leveled_type q) as y.
682 unfold mkDropFlags; simpl.
686 destruct (General.list_eq_dec h0 (ec :: nil)).
702 apply (Prelude_error "escapifying code with multi-leaf antecedents is not supported").
705 Lemma mapOptionTree_distributes
706 : forall T R (a b:Tree ??T) (f:T->R),
707 mapOptionTree f (a,,b) = (mapOptionTree f a),,(mapOptionTree f b).
711 Definition decide_tree_empty : forall {T:Type}(t:Tree ??T),
712 sum { q:Tree unit & t = mapTree (fun _ => None) q } unit.
717 | T_Branch b1 b2 => let b1' := foo b1 in let b2' := foo b2 in _
737 Definition flatten_proof :
740 ND Rule (mapOptionTree (flatten_judgment ) h) (mapOptionTree (flatten_judgment ) c).
742 eapply nd_map'; [ idtac | apply X ].
747 refine (match X as R in Rule H C with
748 | RArrange Γ Δ a b x d => let case_RArrange := tt in _
749 | RNote Γ Δ Σ τ l n => let case_RNote := tt in _
750 | RLit Γ Δ l _ => let case_RLit := tt in _
751 | RVar Γ Δ σ lev => let case_RVar := tt in _
752 | RGlobal Γ Δ σ l wev => let case_RGlobal := tt in _
753 | RLam Γ Δ Σ tx te lev => let case_RLam := tt in _
754 | RCast Γ Δ Σ σ τ lev γ => let case_RCast := tt in _
755 | RAbsT Γ Δ Σ κ σ lev => let case_RAbsT := tt in _
756 | RAppT Γ Δ Σ κ σ τ lev => let case_RAppT := tt in _
757 | RAppCo Γ Δ Σ κ σ₁ σ₂ γ σ lev => let case_RAppCo := tt in _
758 | RAbsCo Γ Δ Σ κ σ σ₁ σ₂ lev => let case_RAbsCo := tt in _
759 | RApp Γ Δ Σ₁ Σ₂ tx te lev => let case_RApp := tt in _
760 | RLet Γ Δ Σ₁ Σ₂ σ₁ σ₂ lev => let case_RLet := tt in _
761 | RJoin Γ p lri m x q => let case_RJoin := tt in _
762 | RVoid _ _ => let case_RVoid := tt in _
763 | RBrak Γ Δ t ec succ lev => let case_RBrak := tt in _
764 | REsc Γ Δ t ec succ lev => let case_REsc := tt in _
765 | RCase Γ Δ lev tc Σ avars tbranches alts => let case_RCase := tt in _
766 | RLetRec Γ Δ lri x y t => let case_RLetRec := tt in _
769 destruct case_RArrange.
770 apply (flatten_arrangement'' Γ Δ a b x d).
775 change ([flatten_type (<[ ec |- t ]>) @@ nil])
776 with ([ga_mk (v2t ec) [] [flatten_type t] @@ nil]).
777 refine (ga_unkappa Γ Δ (v2t ec) nil (mapOptionTree (flatten_type ○ unlev) (take_lev (ec::nil) succ)) _
778 (mapOptionTree (flatten_leveled_type) (drop_lev (ec::nil) succ)) ;; _ ).
780 apply (Prelude_error "found Brak at depth >0 indicating 3-level code; only two-level code is currently supported").
786 change ([flatten_leveled_type (<[ ec |- t ]> @@ nil)])
787 with ([ga_mk (v2t ec) [] [flatten_type t] @@ nil]).
788 eapply nd_comp; [ apply arrange_esc | idtac ].
789 set (decide_tree_empty (take_lev (ec :: nil) succ)) as q'.
795 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanR ].
796 eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
797 eapply nd_comp; [ apply nd_llecnac | idtac ].
798 apply nd_prod; [ idtac | eapply boost ].
801 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanR ].
810 (* environment has non-empty leaves *)
811 apply (ga_kappa Γ Δ (v2t ec) nil (mapOptionTree (flatten_type ○ unlev) (take_lev (ec::nil) succ)) _ _).
812 apply (Prelude_error "found Esc at depth >0 indicating 3-level code; only two-level code is currently supported").
817 apply nd_rule; apply RNote; auto.
818 apply nd_rule; apply RNote; auto.
823 unfold flatten_leveled_type.
825 rewrite literal_types_unchanged.
826 apply nd_rule; apply RLit.
827 unfold take_lev; simpl.
828 unfold drop_lev; simpl.
830 rewrite literal_types_unchanged.
834 Opaque flatten_judgment.
836 Transparent flatten_judgment.
838 unfold flatten_judgment.
841 apply nd_rule. apply RVar.
842 repeat drop_simplify.
843 repeat take_simplify.
847 destruct case_RGlobal.
851 destruct l as [|ec lev]; simpl.
852 destruct (eqd_dec (g:CoreVar) (hetmet_flatten:CoreVar)).
853 set (flatten_type (g wev)) as t.
854 set (RGlobal _ Δ nil (mkGlobal Γ t hetmet_id)) as q.
859 destruct (eqd_dec (g:CoreVar) (hetmet_unflatten:CoreVar)).
860 set (flatten_type (g wev)) as t.
861 set (RGlobal _ Δ nil (mkGlobal Γ t hetmet_id)) as q.
866 unfold flatten_leveled_type. simpl.
867 apply nd_rule; rewrite globals_do_not_have_code_types.
869 apply (Prelude_error "found RGlobal at depth >0; globals should never appear inside code brackets unless escaped").
875 destruct lev as [|ec lev]; simpl; [ apply nd_rule; apply RLam; auto | idtac ].
876 repeat drop_simplify.
877 repeat take_simplify.
889 destruct lev as [|ec lev]; simpl; [ apply nd_rule; apply RCast; auto | idtac ].
890 apply flatten_coercion; auto.
891 apply (Prelude_error "RCast at level >0; casting inside of code brackets is currently not supported").
895 destruct (getjlev x); destruct (getjlev q);
896 [ apply nd_rule; apply RJoin | idtac | idtac | idtac ];
897 apply (Prelude_error "RJoin at depth >0").
902 destruct lev as [|ec lev]. simpl. apply nd_rule.
903 unfold flatten_leveled_type at 4.
904 unfold flatten_leveled_type at 2.
906 replace (flatten_type (tx ---> te))
907 with (flatten_type tx ---> flatten_type te).
911 repeat drop_simplify.
912 repeat take_simplify.
913 rewrite mapOptionTree_distributes.
914 set (mapOptionTree (flatten_leveled_type ) (drop_lev (ec :: lev) Σ₁)) as Σ₁'.
915 set (mapOptionTree (flatten_leveled_type ) (drop_lev (ec :: lev) Σ₂)) as Σ₂'.
916 set (take_lev (ec :: lev) Σ₁) as Σ₁''.
917 set (take_lev (ec :: lev) Σ₂) as Σ₂''.
918 replace (flatten_type (tx ---> te)) with ((flatten_type tx) ---> (flatten_type te)).
919 apply (Prelude_error "FIXME: ga_apply").
923 Notation "` x" := (take_lev _ x).
924 Notation "`` x" := (mapOptionTree unlev x) (at level 20).
925 Notation "``` x" := ((drop_lev _ x)) (at level 20).
926 Notation "!<[]> x" := (flatten_type _ x) (at level 1).
927 Notation "!<[@]> x" := (mapOptionTree flatten_leveled_type x) (at level 1).
932 destruct lev as [|ec lev]; simpl; [ apply nd_rule; apply RLet; auto | idtac ].
933 repeat drop_simplify.
934 repeat take_simplify.
938 eapply nd_prod; [ idtac | apply nd_id ].
960 simpl. destruct lev; simpl.
961 unfold flatten_leveled_type.
963 rewrite flatten_commutes_with_HaskTAll.
964 rewrite flatten_commutes_with_substT.
969 apply (Prelude_error "found type application at level >0; this is not supported").
972 simpl. destruct lev; simpl.
973 unfold flatten_leveled_type at 4.
974 unfold flatten_leveled_type at 2.
976 rewrite flatten_commutes_with_HaskTAll.
977 rewrite flatten_commutes_with_HaskTApp.
978 eapply nd_comp; [ idtac | eapply nd_rule; eapply RAbsT ].
980 set (mapOptionTree (flatten_leveled_type ) (mapOptionTree (weakLT(κ:=κ)) Σ)) as a.
981 set (mapOptionTree (weakLT(κ:=κ)) (mapOptionTree (flatten_leveled_type ) Σ)) as q'.
989 rewrite flatten_commutes_with_weakLT.
1000 apply (Prelude_error "found type abstraction at level >0; this is not supported").
1002 destruct case_RAppCo.
1003 simpl. destruct lev; simpl.
1004 unfold flatten_leveled_type at 4.
1005 unfold flatten_leveled_type at 2.
1006 unfold flatten_type.
1010 apply flatten_coercion.
1012 apply (Prelude_error "found coercion application at level >0; this is not supported").
1014 destruct case_RAbsCo.
1015 simpl. destruct lev; simpl.
1016 unfold flatten_type.
1018 apply (Prelude_error "AbsCo not supported (FIXME)").
1019 apply (Prelude_error "found coercion abstraction at level >0; this is not supported").
1021 destruct case_RLetRec.
1024 apply (Prelude_error "LetRec not supported (FIXME)").
1026 destruct case_RCase.
1028 apply (Prelude_error "Case not supported (BIG FIXME)").
1032 (* to do: establish some metric on judgments (max length of level of any succedent type, probably), show how to
1033 * calculate it, and show that the flattening procedure above drives it down by one *)
1036 Instance FlatteningFunctor {Γ}{Δ}{ec} : Functor (JudgmentsL (PCF Γ Δ ec)) (TypesL (SystemFCa Γ Δ)) (obact) :=
1037 { fmor := FlatteningFunctor_fmor }.
1039 Definition ReificationFunctor Γ Δ : Functor (JudgmentsL _ _ (PCF n Γ Δ)) SystemFCa' (mapOptionTree brakifyJudg).
1040 refine {| fmor := ReificationFunctor_fmor Γ Δ |}; unfold hom; unfold ob; simpl ; intros.
1042 Definition PCF_SMME (n:nat)(Γ:TypeEnv)(Δ:CoercionEnv Γ) : ProgrammingLanguageSMME.
1043 refine {| plsmme_pl := PCF n Γ Δ |}.
1046 Definition SystemFCa_SMME (n:nat)(Γ:TypeEnv)(Δ:CoercionEnv Γ) : ProgrammingLanguageSMME.
1047 refine {| plsmme_pl := SystemFCa n Γ Δ |}.
1050 Definition ReificationFunctorMonoidal n : MonoidalFunctor (JudgmentsN n) (JudgmentsN (S n)) (ReificationFunctor n).
1054 Definition PCF_SystemFCa_two_level n Γ Δ : TwoLevelLanguage (PCF_SMME n Γ Δ) (SystemFCa_SMME (S n) Γ Δ).
1057 (* ... and the retraction exists *)
1061 Implicit Arguments garrow [ ].