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 {Γ}(ec:HaskType Γ ECKind )(ant suc:Tree ??(HaskType Γ ★)) : HaskType Γ ★ :=
208 fun TV ite => gaTy TV (ec TV ite) (ga_mk_tree ec ant TV ite) (ga_mk_tree ec suc TV ite).
212 * - code types <[t]>@c become garrows c () t
213 * - free variables of type t at a level lev deeper than the succedent become garrows c () t
214 * - free variables at the level of the succedent become
216 Fixpoint flatten_rawtype {TV}{κ}(exp: RawHaskType TV κ) : RawHaskType TV κ :=
219 | TAll _ y => TAll _ (fun v => flatten_rawtype (y v))
220 | TApp _ _ x y => TApp (flatten_rawtype x) (flatten_rawtype y)
222 | TCoerc _ t1 t2 t => TCoerc (flatten_rawtype t1) (flatten_rawtype t2) (flatten_rawtype t)
224 | TCode ec e => let e' := flatten_rawtype e
225 (* in let args := take_arg_types e'
226 in let t := drop_arg_types e'
227 in gaTy TV ec (ga_mk_tree' ec (unleaves args)) t*)
228 in gaTy TV ec (unitTy TV ec) e'
229 | TyFunApp tfc kl k lt => TyFunApp tfc kl k (flatten_rawtype_list _ lt)
231 with flatten_rawtype_list {TV}(lk:list Kind)(exp:@RawHaskTypeList TV lk) : @RawHaskTypeList TV lk :=
232 match exp in @RawHaskTypeList _ LK return @RawHaskTypeList TV LK with
233 | TyFunApp_nil => TyFunApp_nil
234 | TyFunApp_cons κ kl t rest => TyFunApp_cons _ _ (flatten_rawtype t) (flatten_rawtype_list _ rest)
237 Definition flatten_type {Γ}{κ}(ht:HaskType Γ κ) : HaskType Γ κ :=
238 fun TV ite => flatten_rawtype (ht TV ite).
240 Fixpoint levels_to_tcode {Γ}(ht:HaskType Γ ★)(lev:HaskLevel Γ) : HaskType Γ ★ :=
243 | ec::lev' => fun TV ite => TCode (v2t ec TV ite) (levels_to_tcode ht lev' TV ite)
246 Definition flatten_leveled_type {Γ}(ht:LeveledHaskType Γ ★) : LeveledHaskType Γ ★ :=
247 flatten_type (levels_to_tcode (unlev ht) (getlev ht)) @@ nil.
251 Axiom literal_types_unchanged : forall Γ l, flatten_type (literalType l) = literalType(Γ:=Γ) l.
253 Axiom flatten_coercion : forall Γ Δ κ (σ τ:HaskType Γ κ) (γ:HaskCoercion Γ Δ (σ ∼∼∼ τ)),
254 HaskCoercion Γ Δ (flatten_type σ ∼∼∼ flatten_type τ).
256 Axiom flatten_commutes_with_substT :
257 forall κ Γ (Δ:CoercionEnv Γ) (σ:∀ TV, InstantiatedTypeEnv TV Γ → TV κ → RawHaskType TV ★) (τ:HaskType Γ κ),
258 flatten_type (substT σ τ) = substT (fun TV ite v => flatten_rawtype (σ TV ite v))
261 Axiom flatten_commutes_with_HaskTAll :
262 forall κ Γ (Δ:CoercionEnv Γ) (σ:∀ TV, InstantiatedTypeEnv TV Γ → TV κ → RawHaskType TV ★),
263 flatten_type (HaskTAll κ σ) = HaskTAll κ (fun TV ite v => flatten_rawtype (σ TV ite v)).
265 Axiom flatten_commutes_with_HaskTApp :
266 forall κ Γ (Δ:CoercionEnv Γ) (σ:∀ TV, InstantiatedTypeEnv TV Γ → TV κ → RawHaskType TV ★),
267 flatten_type (HaskTApp (weakF σ) (FreshHaskTyVar κ)) =
268 HaskTApp (weakF (fun TV ite v => flatten_rawtype (σ TV ite v))) (FreshHaskTyVar κ).
270 Axiom flatten_commutes_with_weakLT : forall (Γ:TypeEnv) κ t,
271 flatten_leveled_type (weakLT(Γ:=Γ)(κ:=κ) t) = weakLT(Γ:=Γ)(κ:=κ) (flatten_leveled_type t).
273 Axiom globals_do_not_have_code_types : forall (Γ:TypeEnv) (g:Global Γ) v,
274 flatten_type (g v) = g v.
276 (* This tries to assign a single level to the entire succedent of a judgment. If the succedent has types from different
277 * levels (should not happen) it just picks one; if the succedent has no non-None leaves (also should not happen) it
279 Definition getΓ (j:Judg) := match j with Γ > _ > _ |- _ => Γ end.
280 Definition getSuc (j:Judg) : Tree ??(LeveledHaskType (getΓ j) ★) :=
281 match j as J return Tree ??(LeveledHaskType (getΓ J) ★) with Γ > _ > _ |- s => s end.
282 Fixpoint getjlev {Γ}(tt:Tree ??(LeveledHaskType Γ ★)) : HaskLevel Γ :=
285 | T_Leaf (Some (_ @@ lev)) => lev
287 match getjlev b1 with
293 (* "n" is the maximum depth remaining AFTER flattening *)
294 Definition flatten_judgment (j:Judg) :=
295 match j as J return Judg with
296 Γ > Δ > ant |- suc =>
297 match getjlev suc with
298 | nil => Γ > Δ > mapOptionTree flatten_leveled_type ant
299 |- mapOptionTree flatten_leveled_type suc
301 | (ec::lev') => Γ > Δ > mapOptionTree flatten_leveled_type (drop_lev (ec::lev') ant)
303 (mapOptionTree (flatten_type ○ unlev) (take_lev (ec::lev') ant))
304 (mapOptionTree (flatten_type ○ unlev) suc )
305 @@ nil] (* we know the level of all of suc *)
310 { ga_id : ∀ Γ Δ ec l a , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec a a @@ l] ]
311 ; ga_cancelr : ∀ Γ Δ ec l a , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec (a,,[]) a @@ l] ]
312 ; ga_cancell : ∀ Γ Δ ec l a , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec ([],,a) a @@ l] ]
313 ; ga_uncancelr : ∀ Γ Δ ec l a , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec a (a,,[]) @@ l] ]
314 ; ga_uncancell : ∀ Γ Δ ec l a , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec a ([],,a) @@ l] ]
315 ; ga_assoc : ∀ Γ Δ ec l a b c, ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec ((a,,b),,c) (a,,(b,,c)) @@ l] ]
316 ; ga_unassoc : ∀ Γ Δ ec l a b c, ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec (a,,(b,,c)) ((a,,b),,c) @@ l] ]
317 ; ga_swap : ∀ Γ Δ ec l a b , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec (a,,b) (b,,a) @@ l] ]
318 ; ga_drop : ∀ Γ Δ ec l a , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec a [] @@ l] ]
319 ; ga_copy : ∀ Γ Δ ec l a , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec a (a,,a) @@ l] ]
320 ; ga_first : ∀ Γ Δ ec l a b x, ND Rule [] [Γ > Δ > [@ga_mk Γ ec a b @@ l] |- [@ga_mk Γ ec (a,,x) (b,,x) @@ l] ]
321 ; ga_second : ∀ Γ Δ ec l a b x, ND Rule [] [Γ > Δ > [@ga_mk Γ ec a b @@ l] |- [@ga_mk Γ ec (x,,a) (x,,b) @@ l] ]
322 ; ga_lit : ∀ Γ Δ ec l lit , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec [] [literalType lit] @@ l] ]
323 ; ga_curry : ∀ Γ Δ ec l a b c, ND Rule [] [Γ > Δ > [@ga_mk Γ ec (a,,[b]) [c] @@ l] |- [@ga_mk Γ ec a [b ---> c] @@ l] ]
324 ; 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] ]
325 ; ga_apply : ∀ Γ Δ ec l a a' b c,
326 ND Rule [] [Γ > Δ > [@ga_mk Γ ec a [b ---> c] @@ l],,[@ga_mk Γ ec a' [b] @@ l] |- [@ga_mk Γ ec (a,,a') [c] @@ l] ]
327 ; ga_kappa : ∀ Γ Δ ec l a b Σ, ND Rule
328 [Γ > Δ > Σ,,[@ga_mk Γ ec [] a @@ l] |- [@ga_mk Γ ec [] b @@ l] ]
329 [Γ > Δ > Σ |- [@ga_mk Γ ec a b @@ l] ]
331 Context `(gar:garrow).
333 Notation "a ~~~~> b" := (@ga_mk _ _ a b) (at level 20).
335 Definition boost : forall Γ Δ ant x y {lev},
336 ND Rule [] [ Γ > Δ > [x@@lev] |- [y@@lev] ] ->
337 ND Rule [ Γ > Δ > ant |- [x@@lev] ] [ Γ > Δ > ant |- [y@@lev] ].
339 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanL ].
340 eapply nd_comp; [ idtac | eapply nd_rule; apply (@RLet Γ Δ [] ant y x lev) ].
341 eapply nd_comp; [ apply nd_rlecnac | idtac ].
351 Definition postcompose' : ∀ Γ Δ ec lev a b c Σ,
352 ND Rule [] [ Γ > Δ > Σ |- [@ga_mk Γ ec a b @@ lev] ] ->
353 ND Rule [] [ Γ > Δ > Σ,,[@ga_mk Γ ec b c @@ lev] |- [@ga_mk Γ ec a c @@ lev] ].
355 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RExch ].
356 eapply nd_comp; [ idtac
357 | eapply nd_rule; apply (@RLet Γ Δ [@ga_mk _ ec b c @@lev] Σ (@ga_mk _ ec a c) (@ga_mk _ ec a b) lev) ].
358 eapply nd_comp; [ apply nd_llecnac | idtac ].
361 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RExch ].
365 Definition precompose Γ Δ ec : forall a x y z lev,
367 [ Γ > Δ > a |- [@ga_mk _ ec y z @@ lev] ]
368 [ Γ > Δ > a,,[@ga_mk _ ec x y @@ lev] |- [@ga_mk _ ec x z @@ lev] ].
377 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RExch ].
383 Definition precompose' : ∀ Γ Δ ec lev a b c Σ,
384 ND Rule [] [ Γ > Δ > Σ |- [@ga_mk Γ ec b c @@ lev] ] ->
385 ND Rule [] [ Γ > Δ > Σ,,[@ga_mk Γ ec a b @@ lev] |- [@ga_mk Γ ec a c @@ lev] ].
392 Definition postcompose : ∀ Γ Δ ec lev a b c,
393 ND Rule [] [ Γ > Δ > [] |- [@ga_mk Γ ec a b @@ lev] ] ->
394 ND Rule [] [ Γ > Δ > [@ga_mk Γ ec b c @@ lev] |- [@ga_mk Γ ec a c @@ lev] ].
404 Definition firstify : ∀ Γ Δ ec lev a b c Σ,
405 ND Rule [] [ Γ > Δ > Σ |- [@ga_mk Γ ec a b @@ lev] ] ->
406 ND Rule [] [ Γ > Δ > Σ |- [@ga_mk Γ ec (a,,c) (b,,c) @@ lev] ].
408 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanL ].
409 eapply nd_comp; [ idtac | eapply nd_rule; apply RLet ].
410 eapply nd_comp; [ apply nd_llecnac | idtac ].
413 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RuCanL ].
417 Definition secondify : ∀ Γ Δ ec lev a b c Σ,
418 ND Rule [] [ Γ > Δ > Σ |- [@ga_mk Γ ec a b @@ lev] ] ->
419 ND Rule [] [ Γ > Δ > Σ |- [@ga_mk Γ ec (c,,a) (c,,b) @@ lev] ].
421 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanL ].
422 eapply nd_comp; [ idtac | eapply nd_rule; apply RLet ].
423 eapply nd_comp; [ apply nd_llecnac | idtac ].
426 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RuCanL ].
430 Lemma ga_unkappa : ∀ Γ Δ ec l a b Σ,
432 [Γ > Δ > Σ |- [@ga_mk Γ ec a b @@ l] ]
433 [Γ > Δ > Σ,,[@ga_mk Γ ec [] a @@ l] |- [@ga_mk Γ ec [] b @@ l] ].
435 set (ga_comp Γ Δ ec l [] a b) as q.
437 set (@RLet Γ Δ) as q'.
438 set (@RLet Γ Δ [@ga_mk _ ec [] a @@ l] Σ (@ga_mk _ ec [] b) (@ga_mk _ ec a b) l) as q''.
459 (* useful for cutting down on the pretty-printed noise
461 Notation "` x" := (take_lev _ x) (at level 20).
462 Notation "`` x" := (mapOptionTree unlev x) (at level 20).
463 Notation "``` x" := (drop_lev _ x) (at level 20).
465 Definition flatten_arrangement' :
466 forall Γ (Δ:CoercionEnv Γ)
467 (ec:HaskTyVar Γ ECKind) (lev:HaskLevel Γ) (ant1 ant2:Tree ??(LeveledHaskType Γ ★)) (r:Arrange ant1 ant2),
468 ND Rule [] [Γ > Δ > [] |- [@ga_mk _ (v2t ec) (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) ant2))
469 (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) ant1)) @@ nil] ].
472 refine (fix flatten ant1 ant2 (r:Arrange ant1 ant2):
473 ND Rule [] [Γ > Δ > [] |- [@ga_mk _ (v2t ec)
474 (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) ant2))
475 (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) ant1)) @@ nil]] :=
476 match r as R in Arrange A B return
477 ND Rule [] [Γ > Δ > [] |- [@ga_mk _ (v2t ec)
478 (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) B))
479 (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) A)) @@ nil]]
481 | RCanL a => let case_RCanL := tt in ga_uncancell _ _ _ _ _
482 | RCanR a => let case_RCanR := tt in ga_uncancelr _ _ _ _ _
483 | RuCanL a => let case_RuCanL := tt in ga_cancell _ _ _ _ _
484 | RuCanR a => let case_RuCanR := tt in ga_cancelr _ _ _ _ _
485 | RAssoc a b c => let case_RAssoc := tt in ga_assoc _ _ _ _ _ _ _
486 | RCossa a b c => let case_RCossa := tt in ga_unassoc _ _ _ _ _ _ _
487 | RExch a b => let case_RExch := tt in ga_swap _ _ _ _ _ _
488 | RWeak a => let case_RWeak := tt in ga_drop _ _ _ _ _
489 | RCont a => let case_RCont := tt in ga_copy _ _ _ _ _
490 | RLeft a b c r' => let case_RLeft := tt in flatten _ _ r' ;; boost _ _ _ _ _ (ga_second _ _ _ _ _ _ _)
491 | RRight a b c r' => let case_RRight := tt in flatten _ _ r' ;; boost _ _ _ _ _ (ga_first _ _ _ _ _ _ _)
492 | RComp c b a r1 r2 => let case_RComp := tt in (fun r1' r2' => _) (flatten _ _ r1) (flatten _ _ r2)
493 end); clear flatten; repeat take_simplify; repeat drop_simplify; intros.
496 set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) a)) as a' in *.
497 set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) b)) as b' in *.
498 set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) c)) as c' in *.
499 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RCanL ].
500 eapply nd_comp; [ idtac | eapply nd_rule; apply
501 (@RLet Γ Δ [] [] (@ga_mk _ (v2t ec) a' c') (@ga_mk _ (v2t ec) a' b')) ].
502 eapply nd_comp; [ apply nd_llecnac | idtac ].
505 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RuCanL ].
506 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RCanR ].
507 eapply nd_comp; [ idtac | eapply nd_rule; apply
508 (@RLet Γ Δ [@ga_mk _ (v2t ec) a' b' @@ _] [] (@ga_mk _ (v2t ec) a' c') (@ga_mk _ (v2t ec) b' c'))].
509 eapply nd_comp; [ apply nd_llecnac | idtac ].
515 Definition flatten_arrangement :
516 forall Γ (Δ:CoercionEnv Γ) n
517 (ec:HaskTyVar Γ ECKind) (lev:HaskLevel Γ) (ant1 ant2:Tree ??(LeveledHaskType Γ ★)) (r:Arrange ant1 ant2) succ,
519 [Γ > Δ > mapOptionTree (flatten_leveled_type ) (drop_lev n ant1)
520 |- [@ga_mk _ (v2t ec)
521 (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) ant1))
522 (mapOptionTree (flatten_type ○ unlev) succ) @@ nil]]
523 [Γ > Δ > mapOptionTree (flatten_leveled_type ) (drop_lev n ant2)
524 |- [@ga_mk _ (v2t ec)
525 (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) ant2))
526 (mapOptionTree (flatten_type ○ unlev) succ) @@ nil]].
528 refine ( _ ;; (boost _ _ _ _ _ (postcompose _ _ _ _ _ _ _ (flatten_arrangement' Γ Δ ec lev ant1 ant2 r)))).
531 refine ((fix flatten ant1 ant2 (r:Arrange ant1 ant2) :=
532 match r as R in Arrange A B return
533 Arrange (mapOptionTree (flatten_leveled_type ) (drop_lev _ A))
534 (mapOptionTree (flatten_leveled_type ) (drop_lev _ B)) with
535 | RCanL a => let case_RCanL := tt in RCanL _
536 | RCanR a => let case_RCanR := tt in RCanR _
537 | RuCanL a => let case_RuCanL := tt in RuCanL _
538 | RuCanR a => let case_RuCanR := tt in RuCanR _
539 | RAssoc a b c => let case_RAssoc := tt in RAssoc _ _ _
540 | RCossa a b c => let case_RCossa := tt in RCossa _ _ _
541 | RExch a b => let case_RExch := tt in RExch _ _
542 | RWeak a => let case_RWeak := tt in RWeak _
543 | RCont a => let case_RCont := tt in RCont _
544 | RLeft a b c r' => let case_RLeft := tt in RLeft _ (flatten _ _ r')
545 | RRight a b c r' => let case_RRight := tt in RRight _ (flatten _ _ r')
546 | RComp a b c r1 r2 => let case_RComp := tt in RComp (flatten _ _ r1) (flatten _ _ r2)
547 end) ant1 ant2 r); clear flatten; repeat take_simplify; repeat drop_simplify; intros.
550 Definition flatten_arrangement'' :
551 forall Γ Δ ant1 ant2 succ (r:Arrange ant1 ant2),
552 ND Rule (mapOptionTree (flatten_judgment ) [Γ > Δ > ant1 |- succ])
553 (mapOptionTree (flatten_judgment ) [Γ > Δ > ant2 |- succ]).
556 set (getjlev succ) as succ_lev.
557 assert (succ_lev=getjlev succ).
575 eapply RComp; [ apply IHr1 | apply IHr2 ].
577 apply flatten_arrangement.
581 Definition ga_join Γ Δ Σ₁ Σ₂ a b ec :
582 ND Rule [] [Γ > Δ > Σ₁ |- [@ga_mk _ ec [] a @@ nil]] ->
583 ND Rule [] [Γ > Δ > Σ₂ |- [@ga_mk _ ec [] b @@ nil]] ->
584 ND Rule [] [Γ > Δ > Σ₁,,Σ₂ |- [@ga_mk _ ec [] (a,,b) @@ nil]].
587 apply secondify with (c:=a) in pfb.
590 eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
591 eapply nd_comp; [ eapply nd_llecnac | idtac ].
600 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanL ].
606 Definition arrange_brak : forall Γ Δ ec succ t,
608 [Γ > Δ > mapOptionTree (flatten_leveled_type ) (drop_lev (ec :: nil) succ),,
609 [(@ga_mk _ (v2t ec) []
610 (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: nil) succ)))
611 @@ nil] |- [(@ga_mk _ (v2t ec) [] [flatten_type t]) @@ nil]]
612 [Γ > Δ > mapOptionTree (flatten_leveled_type ) succ |- [(@ga_mk _ (v2t ec) [] [flatten_type t]) @@ nil]].
615 set (@arrange' _ succ (levelMatch (ec::nil))) as q.
616 set (arrangeMap _ _ flatten_leveled_type q) as y.
625 eapply nd_comp; [ apply nd_llecnac | idtac ].
626 eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
631 induction succ; try destruct a; simpl.
637 destruct l as [t' lev'].
638 destruct lev' as [|ec' lev'].
642 set (@eqd_dec (HaskLevel Γ) (haskLevelEqDecidable Γ) (ec' :: lev') (ec :: nil)) as q.
647 unfold flatten_leveled_type.
661 Definition arrange_esc : forall Γ Δ ec succ t,
663 [Γ > Δ > mapOptionTree (flatten_leveled_type ) succ |- [(@ga_mk _ (v2t ec) [] [flatten_type t]) @@ nil]]
664 [Γ > Δ > mapOptionTree (flatten_leveled_type ) (drop_lev (ec :: nil) succ),,
665 [(@ga_mk _ (v2t ec) []
666 (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: nil) succ))) @@ nil]
667 |- [(@ga_mk _ (v2t ec) [] [flatten_type t]) @@ nil]].
670 set (@arrange _ succ (levelMatch (ec::nil))) as q.
671 set (arrangeMap _ _ flatten_leveled_type q) as y.
683 unfold mkDropFlags; simpl.
687 destruct (General.list_eq_dec h0 (ec :: nil)).
703 apply (Prelude_error "escapifying code with multi-leaf antecedents is not supported").
706 Lemma mapOptionTree_distributes
707 : forall T R (a b:Tree ??T) (f:T->R),
708 mapOptionTree f (a,,b) = (mapOptionTree f a),,(mapOptionTree f b).
712 Definition decide_tree_empty : forall {T:Type}(t:Tree ??T),
713 sum { q:Tree unit & t = mapTree (fun _ => None) q } unit.
718 | T_Branch b1 b2 => let b1' := foo b1 in let b2' := foo b2 in _
738 Definition flatten_proof :
741 ND Rule (mapOptionTree (flatten_judgment ) h) (mapOptionTree (flatten_judgment ) c).
743 eapply nd_map'; [ idtac | apply X ].
748 refine (match X as R in Rule H C with
749 | RArrange Γ Δ a b x d => let case_RArrange := tt in _
750 | RNote Γ Δ Σ τ l n => let case_RNote := tt in _
751 | RLit Γ Δ l _ => let case_RLit := tt in _
752 | RVar Γ Δ σ lev => let case_RVar := tt in _
753 | RGlobal Γ Δ σ l wev => let case_RGlobal := tt in _
754 | RLam Γ Δ Σ tx te lev => let case_RLam := tt in _
755 | RCast Γ Δ Σ σ τ lev γ => let case_RCast := tt in _
756 | RAbsT Γ Δ Σ κ σ lev => let case_RAbsT := tt in _
757 | RAppT Γ Δ Σ κ σ τ lev => let case_RAppT := tt in _
758 | RAppCo Γ Δ Σ κ σ₁ σ₂ γ σ lev => let case_RAppCo := tt in _
759 | RAbsCo Γ Δ Σ κ σ σ₁ σ₂ lev => let case_RAbsCo := tt in _
760 | RApp Γ Δ Σ₁ Σ₂ tx te lev => let case_RApp := tt in _
761 | RLet Γ Δ Σ₁ Σ₂ σ₁ σ₂ lev => let case_RLet := tt in _
762 | RJoin Γ p lri m x q => let case_RJoin := tt in _
763 | RVoid _ _ => let case_RVoid := tt in _
764 | RBrak Γ Δ t ec succ lev => let case_RBrak := tt in _
765 | REsc Γ Δ t ec succ lev => let case_REsc := tt in _
766 | RCase Γ Δ lev tc Σ avars tbranches alts => let case_RCase := tt in _
767 | RLetRec Γ Δ lri x y t => let case_RLetRec := tt in _
770 destruct case_RArrange.
771 apply (flatten_arrangement'' Γ Δ a b x d).
776 change ([flatten_type (<[ ec |- t ]>) @@ nil])
777 with ([ga_mk (v2t ec) [] [flatten_type t] @@ nil]).
778 refine (ga_unkappa Γ Δ (v2t ec) nil (mapOptionTree (flatten_type ○ unlev) (take_lev (ec::nil) succ)) _
779 (mapOptionTree (flatten_leveled_type) (drop_lev (ec::nil) succ)) ;; _ ).
781 apply (Prelude_error "found Brak at depth >0 indicating 3-level code; only two-level code is currently supported").
787 change ([flatten_leveled_type (<[ ec |- t ]> @@ nil)])
788 with ([ga_mk (v2t ec) [] [flatten_type t] @@ nil]).
789 eapply nd_comp; [ apply arrange_esc | idtac ].
790 set (decide_tree_empty (take_lev (ec :: nil) succ)) as q'.
796 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanR ].
797 eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
798 eapply nd_comp; [ apply nd_llecnac | idtac ].
799 apply nd_prod; [ idtac | eapply boost ].
802 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanR ].
811 (* environment has non-empty leaves *)
812 apply (ga_kappa Γ Δ (v2t ec) nil (mapOptionTree (flatten_type ○ unlev) (take_lev (ec::nil) succ)) _ _).
813 apply (Prelude_error "found Esc at depth >0 indicating 3-level code; only two-level code is currently supported").
818 apply nd_rule; apply RNote; auto.
819 apply nd_rule; apply RNote; auto.
824 unfold flatten_leveled_type.
826 rewrite literal_types_unchanged.
827 apply nd_rule; apply RLit.
828 unfold take_lev; simpl.
829 unfold drop_lev; simpl.
831 rewrite literal_types_unchanged.
835 Opaque flatten_judgment.
837 Transparent flatten_judgment.
839 unfold flatten_judgment.
842 apply nd_rule. apply RVar.
843 repeat drop_simplify.
844 repeat take_simplify.
848 destruct case_RGlobal.
852 destruct l as [|ec lev]; simpl.
853 destruct (eqd_dec (g:CoreVar) (hetmet_flatten:CoreVar)).
854 set (flatten_type (g wev)) as t.
855 set (RGlobal _ Δ nil (mkGlobal Γ t hetmet_id)) as q.
860 destruct (eqd_dec (g:CoreVar) (hetmet_unflatten:CoreVar)).
861 set (flatten_type (g wev)) as t.
862 set (RGlobal _ Δ nil (mkGlobal Γ t hetmet_id)) as q.
867 unfold flatten_leveled_type. simpl.
868 apply nd_rule; rewrite globals_do_not_have_code_types.
870 apply (Prelude_error "found RGlobal at depth >0; globals should never appear inside code brackets unless escaped").
876 destruct lev as [|ec lev]; simpl; [ apply nd_rule; apply RLam; auto | idtac ].
877 repeat drop_simplify.
878 repeat take_simplify.
890 destruct lev as [|ec lev]; simpl; [ apply nd_rule; apply RCast; auto | idtac ].
891 apply flatten_coercion; auto.
892 apply (Prelude_error "RCast at level >0; casting inside of code brackets is currently not supported").
896 destruct (getjlev x); destruct (getjlev q);
897 [ apply nd_rule; apply RJoin | idtac | idtac | idtac ];
898 apply (Prelude_error "RJoin at depth >0").
903 destruct lev as [|ec lev]. simpl. apply nd_rule.
904 unfold flatten_leveled_type at 4.
905 unfold flatten_leveled_type at 2.
907 replace (flatten_type (tx ---> te))
908 with (flatten_type tx ---> flatten_type te).
912 repeat drop_simplify.
913 repeat take_simplify.
914 rewrite mapOptionTree_distributes.
915 set (mapOptionTree (flatten_leveled_type ) (drop_lev (ec :: lev) Σ₁)) as Σ₁'.
916 set (mapOptionTree (flatten_leveled_type ) (drop_lev (ec :: lev) Σ₂)) as Σ₂'.
917 set (take_lev (ec :: lev) Σ₁) as Σ₁''.
918 set (take_lev (ec :: lev) Σ₂) as Σ₂''.
919 replace (flatten_type (tx ---> te)) with ((flatten_type tx) ---> (flatten_type te)).
920 apply (Prelude_error "FIXME: ga_apply").
924 Notation "` x" := (take_lev _ x).
925 Notation "`` x" := (mapOptionTree unlev x) (at level 20).
926 Notation "``` x" := ((drop_lev _ x)) (at level 20).
927 Notation "!<[]> x" := (flatten_type _ x) (at level 1).
928 Notation "!<[@]> x" := (mapOptionTree flatten_leveled_type x) (at level 1).
933 destruct lev as [|ec lev]; simpl; [ apply nd_rule; apply RLet; auto | idtac ].
934 repeat drop_simplify.
935 repeat take_simplify.
939 eapply nd_prod; [ idtac | apply nd_id ].
961 simpl. destruct lev; simpl.
962 unfold flatten_leveled_type.
964 rewrite flatten_commutes_with_HaskTAll.
965 rewrite flatten_commutes_with_substT.
970 apply (Prelude_error "found type application at level >0; this is not supported").
973 simpl. destruct lev; simpl.
974 unfold flatten_leveled_type at 4.
975 unfold flatten_leveled_type at 2.
977 rewrite flatten_commutes_with_HaskTAll.
978 rewrite flatten_commutes_with_HaskTApp.
979 eapply nd_comp; [ idtac | eapply nd_rule; eapply RAbsT ].
981 set (mapOptionTree (flatten_leveled_type ) (mapOptionTree (weakLT(κ:=κ)) Σ)) as a.
982 set (mapOptionTree (weakLT(κ:=κ)) (mapOptionTree (flatten_leveled_type ) Σ)) as q'.
990 rewrite flatten_commutes_with_weakLT.
1001 apply (Prelude_error "found type abstraction at level >0; this is not supported").
1003 destruct case_RAppCo.
1004 simpl. destruct lev; simpl.
1005 unfold flatten_leveled_type at 4.
1006 unfold flatten_leveled_type at 2.
1007 unfold flatten_type.
1011 apply flatten_coercion.
1013 apply (Prelude_error "found coercion application at level >0; this is not supported").
1015 destruct case_RAbsCo.
1016 simpl. destruct lev; simpl.
1017 unfold flatten_type.
1019 apply (Prelude_error "AbsCo not supported (FIXME)").
1020 apply (Prelude_error "found coercion abstraction at level >0; this is not supported").
1022 destruct case_RLetRec.
1025 apply (Prelude_error "LetRec not supported (FIXME)").
1027 destruct case_RCase.
1029 apply (Prelude_error "Case not supported (BIG FIXME)").
1033 (* to do: establish some metric on judgments (max length of level of any succedent type, probably), show how to
1034 * calculate it, and show that the flattening procedure above drives it down by one *)
1037 Instance FlatteningFunctor {Γ}{Δ}{ec} : Functor (JudgmentsL (PCF Γ Δ ec)) (TypesL (SystemFCa Γ Δ)) (obact) :=
1038 { fmor := FlatteningFunctor_fmor }.
1040 Definition ReificationFunctor Γ Δ : Functor (JudgmentsL _ _ (PCF n Γ Δ)) SystemFCa' (mapOptionTree brakifyJudg).
1041 refine {| fmor := ReificationFunctor_fmor Γ Δ |}; unfold hom; unfold ob; simpl ; intros.
1043 Definition PCF_SMME (n:nat)(Γ:TypeEnv)(Δ:CoercionEnv Γ) : ProgrammingLanguageSMME.
1044 refine {| plsmme_pl := PCF n Γ Δ |}.
1047 Definition SystemFCa_SMME (n:nat)(Γ:TypeEnv)(Δ:CoercionEnv Γ) : ProgrammingLanguageSMME.
1048 refine {| plsmme_pl := SystemFCa n Γ Δ |}.
1051 Definition ReificationFunctorMonoidal n : MonoidalFunctor (JudgmentsN n) (JudgmentsN (S n)) (ReificationFunctor n).
1055 Definition PCF_SystemFCa_two_level n Γ Δ : TwoLevelLanguage (PCF_SMME n Γ Δ) (SystemFCa_SMME (S n) Γ Δ).
1058 (* ... and the retraction exists *)
1062 Implicit Arguments garrow [ ].