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 ★ :=
209 (ga_mk_tree' ec (ant,,(mapOptionTreeAndFlatten (unleaves ○ take_arg_types) suc)))
210 (ga_mk_tree' ec ( mapOptionTree drop_arg_types suc) ).
212 Definition ga_mk {Γ}(ec:HaskType Γ ECKind )(ant suc:Tree ??(HaskType Γ ★)) : HaskType Γ ★ :=
213 fun TV ite => ga_mk_raw (ec TV ite) (mapOptionTree (fun x => x TV ite) ant) (mapOptionTree (fun x => x TV ite) suc).
217 * - code types <[t]>@c become garrows c () t
218 * - free variables of type t at a level lev deeper than the succedent become garrows c () t
219 * - free variables at the level of the succedent become
221 Fixpoint flatten_rawtype {TV}{κ}(exp: RawHaskType TV κ) : RawHaskType TV κ :=
224 | TAll _ y => TAll _ (fun v => flatten_rawtype (y v))
225 | TApp _ _ x y => TApp (flatten_rawtype x) (flatten_rawtype y)
227 | TCoerc _ t1 t2 t => TCoerc (flatten_rawtype t1) (flatten_rawtype t2) (flatten_rawtype t)
229 | TCode ec e => ga_mk_raw ec [] [flatten_rawtype e]
230 | TyFunApp tfc kl k lt => TyFunApp tfc kl k (flatten_rawtype_list _ lt)
232 with flatten_rawtype_list {TV}(lk:list Kind)(exp:@RawHaskTypeList TV lk) : @RawHaskTypeList TV lk :=
233 match exp in @RawHaskTypeList _ LK return @RawHaskTypeList TV LK with
234 | TyFunApp_nil => TyFunApp_nil
235 | TyFunApp_cons κ kl t rest => TyFunApp_cons _ _ (flatten_rawtype t) (flatten_rawtype_list _ rest)
238 Definition flatten_type {Γ}{κ}(ht:HaskType Γ κ) : HaskType Γ κ :=
239 fun TV ite => flatten_rawtype (ht TV ite).
241 Fixpoint levels_to_tcode {Γ}(ht:HaskType Γ ★)(lev:HaskLevel Γ) : HaskType Γ ★ :=
244 | ec::lev' => fun TV ite => TCode (v2t ec TV ite) (levels_to_tcode ht lev' TV ite)
247 Definition flatten_leveled_type {Γ}(ht:LeveledHaskType Γ ★) : LeveledHaskType Γ ★ :=
248 flatten_type (levels_to_tcode (unlev ht) (getlev ht)) @@ nil.
252 Axiom literal_types_unchanged : forall Γ l, flatten_type (literalType l) = literalType(Γ:=Γ) l.
254 Axiom flatten_coercion : forall Γ Δ κ (σ τ:HaskType Γ κ) (γ:HaskCoercion Γ Δ (σ ∼∼∼ τ)),
255 HaskCoercion Γ Δ (flatten_type σ ∼∼∼ flatten_type τ).
257 Axiom flatten_commutes_with_substT :
258 forall κ Γ (Δ:CoercionEnv Γ) (σ:∀ TV, InstantiatedTypeEnv TV Γ → TV κ → RawHaskType TV ★) (τ:HaskType Γ κ),
259 flatten_type (substT σ τ) = substT (fun TV ite v => flatten_rawtype (σ TV ite v))
262 Axiom flatten_commutes_with_HaskTAll :
263 forall κ Γ (Δ:CoercionEnv Γ) (σ:∀ TV, InstantiatedTypeEnv TV Γ → TV κ → RawHaskType TV ★),
264 flatten_type (HaskTAll κ σ) = HaskTAll κ (fun TV ite v => flatten_rawtype (σ TV ite v)).
266 Axiom flatten_commutes_with_HaskTApp :
267 forall κ Γ (Δ:CoercionEnv Γ) (σ:∀ TV, InstantiatedTypeEnv TV Γ → TV κ → RawHaskType TV ★),
268 flatten_type (HaskTApp (weakF σ) (FreshHaskTyVar κ)) =
269 HaskTApp (weakF (fun TV ite v => flatten_rawtype (σ TV ite v))) (FreshHaskTyVar κ).
271 Axiom flatten_commutes_with_weakLT : forall (Γ:TypeEnv) κ t,
272 flatten_leveled_type (weakLT(Γ:=Γ)(κ:=κ) t) = weakLT(Γ:=Γ)(κ:=κ) (flatten_leveled_type t).
274 Axiom globals_do_not_have_code_types : forall (Γ:TypeEnv) (g:Global Γ) v,
275 flatten_type (g v) = g v.
277 (* This tries to assign a single level to the entire succedent of a judgment. If the succedent has types from different
278 * levels (should not happen) it just picks one; if the succedent has no non-None leaves (also should not happen) it
280 Definition getΓ (j:Judg) := match j with Γ > _ > _ |- _ => Γ end.
281 Definition getSuc (j:Judg) : Tree ??(LeveledHaskType (getΓ j) ★) :=
282 match j as J return Tree ??(LeveledHaskType (getΓ J) ★) with Γ > _ > _ |- s => s end.
283 Fixpoint getjlev {Γ}(tt:Tree ??(LeveledHaskType Γ ★)) : HaskLevel Γ :=
286 | T_Leaf (Some (_ @@ lev)) => lev
288 match getjlev b1 with
294 (* "n" is the maximum depth remaining AFTER flattening *)
295 Definition flatten_judgment (j:Judg) :=
296 match j as J return Judg with
297 Γ > Δ > ant |- suc =>
298 match getjlev suc with
299 | nil => Γ > Δ > mapOptionTree flatten_leveled_type ant
300 |- mapOptionTree flatten_leveled_type suc
302 | (ec::lev') => Γ > Δ > mapOptionTree flatten_leveled_type (drop_lev (ec::lev') ant)
304 (mapOptionTree (flatten_type ○ unlev) (take_lev (ec::lev') ant))
305 (mapOptionTree (flatten_type ○ unlev) suc )
306 @@ nil] (* we know the level of all of suc *)
311 { ga_id : ∀ Γ Δ ec l a , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec a a @@ l] ]
312 ; ga_cancelr : ∀ Γ Δ ec l a , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec (a,,[]) a @@ l] ]
313 ; ga_cancell : ∀ Γ Δ ec l a , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec ([],,a) a @@ l] ]
314 ; ga_uncancelr : ∀ Γ Δ ec l a , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec a (a,,[]) @@ l] ]
315 ; ga_uncancell : ∀ Γ Δ ec l a , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec a ([],,a) @@ l] ]
316 ; ga_assoc : ∀ Γ Δ ec l a b c, ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec ((a,,b),,c) (a,,(b,,c)) @@ l] ]
317 ; ga_unassoc : ∀ Γ Δ ec l a b c, ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec (a,,(b,,c)) ((a,,b),,c) @@ l] ]
318 ; ga_swap : ∀ Γ Δ ec l a b , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec (a,,b) (b,,a) @@ l] ]
319 ; ga_drop : ∀ Γ Δ ec l a , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec a [] @@ l] ]
320 ; ga_copy : ∀ Γ Δ ec l a , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec a (a,,a) @@ l] ]
321 ; ga_first : ∀ Γ Δ ec l a b x, ND Rule [] [Γ > Δ > [@ga_mk Γ ec a b @@ l] |- [@ga_mk Γ ec (a,,x) (b,,x) @@ l] ]
322 ; ga_second : ∀ Γ Δ ec l a b x, ND Rule [] [Γ > Δ > [@ga_mk Γ ec a b @@ l] |- [@ga_mk Γ ec (x,,a) (x,,b) @@ l] ]
323 ; ga_lit : ∀ Γ Δ ec l lit , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec [] [literalType lit] @@ l] ]
324 ; ga_curry : ∀ Γ Δ ec l a b c, ND Rule [] [Γ > Δ > [@ga_mk Γ ec (a,,[b]) [c] @@ l] |- [@ga_mk Γ ec a [b ---> c] @@ l] ]
325 ; 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] ]
326 ; ga_apply : ∀ Γ Δ ec l a a' b c,
327 ND Rule [] [Γ > Δ > [@ga_mk Γ ec a [b ---> c] @@ l],,[@ga_mk Γ ec a' [b] @@ l] |- [@ga_mk Γ ec (a,,a') [c] @@ l] ]
328 ; ga_kappa : ∀ Γ Δ ec l a b Σ, ND Rule
329 [Γ > Δ > Σ,,[@ga_mk Γ ec [] a @@ l] |- [@ga_mk Γ ec [] b @@ l] ]
330 [Γ > Δ > Σ |- [@ga_mk Γ ec a b @@ l] ]
332 Context `(gar:garrow).
334 Notation "a ~~~~> b" := (@ga_mk _ _ a b) (at level 20).
336 Definition boost : forall Γ Δ ant x y {lev},
337 ND Rule [] [ Γ > Δ > [x@@lev] |- [y@@lev] ] ->
338 ND Rule [ Γ > Δ > ant |- [x@@lev] ] [ Γ > Δ > ant |- [y@@lev] ].
340 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanL ].
341 eapply nd_comp; [ idtac | eapply nd_rule; apply (@RLet Γ Δ [] ant y x lev) ].
342 eapply nd_comp; [ apply nd_rlecnac | idtac ].
352 Definition postcompose' : ∀ Γ Δ ec lev a b c Σ,
353 ND Rule [] [ Γ > Δ > Σ |- [@ga_mk Γ ec a b @@ lev] ] ->
354 ND Rule [] [ Γ > Δ > Σ,,[@ga_mk Γ ec b c @@ lev] |- [@ga_mk Γ ec a c @@ lev] ].
356 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RExch ].
357 eapply nd_comp; [ idtac
358 | eapply nd_rule; apply (@RLet Γ Δ [@ga_mk _ ec b c @@lev] Σ (@ga_mk _ ec a c) (@ga_mk _ ec a b) lev) ].
359 eapply nd_comp; [ apply nd_llecnac | idtac ].
362 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RExch ].
366 Definition precompose Γ Δ ec : forall a x y z lev,
368 [ Γ > Δ > a |- [@ga_mk _ ec y z @@ lev] ]
369 [ Γ > Δ > a,,[@ga_mk _ ec x y @@ lev] |- [@ga_mk _ ec x z @@ lev] ].
378 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RExch ].
384 Definition precompose' : ∀ Γ Δ ec lev a b c Σ,
385 ND Rule [] [ Γ > Δ > Σ |- [@ga_mk Γ ec b c @@ lev] ] ->
386 ND Rule [] [ Γ > Δ > Σ,,[@ga_mk Γ ec a b @@ lev] |- [@ga_mk Γ ec a c @@ lev] ].
393 Definition postcompose : ∀ Γ Δ ec lev a b c,
394 ND Rule [] [ Γ > Δ > [] |- [@ga_mk Γ ec a b @@ lev] ] ->
395 ND Rule [] [ Γ > Δ > [@ga_mk Γ ec b c @@ lev] |- [@ga_mk Γ ec a c @@ lev] ].
405 Definition firstify : ∀ Γ Δ ec lev a b c Σ,
406 ND Rule [] [ Γ > Δ > Σ |- [@ga_mk Γ ec a b @@ lev] ] ->
407 ND Rule [] [ Γ > Δ > Σ |- [@ga_mk Γ ec (a,,c) (b,,c) @@ lev] ].
409 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanL ].
410 eapply nd_comp; [ idtac | eapply nd_rule; apply RLet ].
411 eapply nd_comp; [ apply nd_llecnac | idtac ].
414 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RuCanL ].
418 Definition secondify : ∀ Γ Δ ec lev a b c Σ,
419 ND Rule [] [ Γ > Δ > Σ |- [@ga_mk Γ ec a b @@ lev] ] ->
420 ND Rule [] [ Γ > Δ > Σ |- [@ga_mk Γ ec (c,,a) (c,,b) @@ lev] ].
422 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanL ].
423 eapply nd_comp; [ idtac | eapply nd_rule; apply RLet ].
424 eapply nd_comp; [ apply nd_llecnac | idtac ].
427 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RuCanL ].
431 Lemma ga_unkappa : ∀ Γ Δ ec l a b Σ,
433 [Γ > Δ > Σ |- [@ga_mk Γ ec a b @@ l] ]
434 [Γ > Δ > Σ,,[@ga_mk Γ ec [] a @@ l] |- [@ga_mk Γ ec [] b @@ l] ].
436 set (ga_comp Γ Δ ec l [] a b) as q.
438 set (@RLet Γ Δ) as q'.
439 set (@RLet Γ Δ [@ga_mk _ ec [] a @@ l] Σ (@ga_mk _ ec [] b) (@ga_mk _ ec a b) l) as q''.
460 (* useful for cutting down on the pretty-printed noise
462 Notation "` x" := (take_lev _ x) (at level 20).
463 Notation "`` x" := (mapOptionTree unlev x) (at level 20).
464 Notation "``` x" := (drop_lev _ x) (at level 20).
466 Definition flatten_arrangement' :
467 forall Γ (Δ:CoercionEnv Γ)
468 (ec:HaskTyVar Γ ECKind) (lev:HaskLevel Γ) (ant1 ant2:Tree ??(LeveledHaskType Γ ★)) (r:Arrange ant1 ant2),
469 ND Rule [] [Γ > Δ > [] |- [@ga_mk _ (v2t ec) (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) ant2))
470 (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) ant1)) @@ nil] ].
473 refine (fix flatten ant1 ant2 (r:Arrange ant1 ant2):
474 ND Rule [] [Γ > Δ > [] |- [@ga_mk _ (v2t ec)
475 (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) ant2))
476 (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) ant1)) @@ nil]] :=
477 match r as R in Arrange A B return
478 ND Rule [] [Γ > Δ > [] |- [@ga_mk _ (v2t ec)
479 (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) B))
480 (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) A)) @@ nil]]
482 | RCanL a => let case_RCanL := tt in ga_uncancell _ _ _ _ _
483 | RCanR a => let case_RCanR := tt in ga_uncancelr _ _ _ _ _
484 | RuCanL a => let case_RuCanL := tt in ga_cancell _ _ _ _ _
485 | RuCanR a => let case_RuCanR := tt in ga_cancelr _ _ _ _ _
486 | RAssoc a b c => let case_RAssoc := tt in ga_assoc _ _ _ _ _ _ _
487 | RCossa a b c => let case_RCossa := tt in ga_unassoc _ _ _ _ _ _ _
488 | RExch a b => let case_RExch := tt in ga_swap _ _ _ _ _ _
489 | RWeak a => let case_RWeak := tt in ga_drop _ _ _ _ _
490 | RCont a => let case_RCont := tt in ga_copy _ _ _ _ _
491 | RLeft a b c r' => let case_RLeft := tt in flatten _ _ r' ;; boost _ _ _ _ _ (ga_second _ _ _ _ _ _ _)
492 | RRight a b c r' => let case_RRight := tt in flatten _ _ r' ;; boost _ _ _ _ _ (ga_first _ _ _ _ _ _ _)
493 | RComp c b a r1 r2 => let case_RComp := tt in (fun r1' r2' => _) (flatten _ _ r1) (flatten _ _ r2)
494 end); clear flatten; repeat take_simplify; repeat drop_simplify; intros.
497 set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) a)) as a' in *.
498 set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) b)) as b' in *.
499 set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) c)) as c' in *.
500 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RCanL ].
501 eapply nd_comp; [ idtac | eapply nd_rule; apply
502 (@RLet Γ Δ [] [] (@ga_mk _ (v2t ec) a' c') (@ga_mk _ (v2t ec) a' b')) ].
503 eapply nd_comp; [ apply nd_llecnac | idtac ].
506 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RuCanL ].
507 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RCanR ].
508 eapply nd_comp; [ idtac | eapply nd_rule; apply
509 (@RLet Γ Δ [@ga_mk _ (v2t ec) a' b' @@ _] [] (@ga_mk _ (v2t ec) a' c') (@ga_mk _ (v2t ec) b' c'))].
510 eapply nd_comp; [ apply nd_llecnac | idtac ].
516 Definition flatten_arrangement :
517 forall Γ (Δ:CoercionEnv Γ) n
518 (ec:HaskTyVar Γ ECKind) (lev:HaskLevel Γ) (ant1 ant2:Tree ??(LeveledHaskType Γ ★)) (r:Arrange ant1 ant2) succ,
520 [Γ > Δ > mapOptionTree (flatten_leveled_type ) (drop_lev n ant1)
521 |- [@ga_mk _ (v2t ec)
522 (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) ant1))
523 (mapOptionTree (flatten_type ○ unlev) succ) @@ nil]]
524 [Γ > Δ > mapOptionTree (flatten_leveled_type ) (drop_lev n ant2)
525 |- [@ga_mk _ (v2t ec)
526 (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) ant2))
527 (mapOptionTree (flatten_type ○ unlev) succ) @@ nil]].
529 refine ( _ ;; (boost _ _ _ _ _ (postcompose _ _ _ _ _ _ _ (flatten_arrangement' Γ Δ ec lev ant1 ant2 r)))).
532 refine ((fix flatten ant1 ant2 (r:Arrange ant1 ant2) :=
533 match r as R in Arrange A B return
534 Arrange (mapOptionTree (flatten_leveled_type ) (drop_lev _ A))
535 (mapOptionTree (flatten_leveled_type ) (drop_lev _ B)) with
536 | RCanL a => let case_RCanL := tt in RCanL _
537 | RCanR a => let case_RCanR := tt in RCanR _
538 | RuCanL a => let case_RuCanL := tt in RuCanL _
539 | RuCanR a => let case_RuCanR := tt in RuCanR _
540 | RAssoc a b c => let case_RAssoc := tt in RAssoc _ _ _
541 | RCossa a b c => let case_RCossa := tt in RCossa _ _ _
542 | RExch a b => let case_RExch := tt in RExch _ _
543 | RWeak a => let case_RWeak := tt in RWeak _
544 | RCont a => let case_RCont := tt in RCont _
545 | RLeft a b c r' => let case_RLeft := tt in RLeft _ (flatten _ _ r')
546 | RRight a b c r' => let case_RRight := tt in RRight _ (flatten _ _ r')
547 | RComp a b c r1 r2 => let case_RComp := tt in RComp (flatten _ _ r1) (flatten _ _ r2)
548 end) ant1 ant2 r); clear flatten; repeat take_simplify; repeat drop_simplify; intros.
551 Definition flatten_arrangement'' :
552 forall Γ Δ ant1 ant2 succ (r:Arrange ant1 ant2),
553 ND Rule (mapOptionTree (flatten_judgment ) [Γ > Δ > ant1 |- succ])
554 (mapOptionTree (flatten_judgment ) [Γ > Δ > ant2 |- succ]).
557 set (getjlev succ) as succ_lev.
558 assert (succ_lev=getjlev succ).
576 eapply RComp; [ apply IHr1 | apply IHr2 ].
578 apply flatten_arrangement.
582 Definition ga_join Γ Δ Σ₁ Σ₂ a b ec :
583 ND Rule [] [Γ > Δ > Σ₁ |- [@ga_mk _ ec [] a @@ nil]] ->
584 ND Rule [] [Γ > Δ > Σ₂ |- [@ga_mk _ ec [] b @@ nil]] ->
585 ND Rule [] [Γ > Δ > Σ₁,,Σ₂ |- [@ga_mk _ ec [] (a,,b) @@ nil]].
588 apply secondify with (c:=a) in pfb.
591 eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
592 eapply nd_comp; [ eapply nd_llecnac | idtac ].
601 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanL ].
607 Definition arrange_brak : forall Γ Δ ec succ t,
609 [Γ > Δ > mapOptionTree (flatten_leveled_type ) (drop_lev (ec :: nil) succ),,
610 [(@ga_mk _ (v2t ec) []
611 (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: nil) succ)))
612 @@ nil] |- [(@ga_mk _ (v2t ec) [] [flatten_type t]) @@ nil]]
613 [Γ > Δ > mapOptionTree (flatten_leveled_type ) succ |- [(@ga_mk _ (v2t ec) [] [flatten_type t]) @@ nil]].
616 set (@arrange' _ succ (levelMatch (ec::nil))) as q.
617 set (arrangeMap _ _ flatten_leveled_type q) as y.
626 eapply nd_comp; [ apply nd_llecnac | idtac ].
627 eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
632 induction succ; try destruct a; simpl.
638 destruct l as [t' lev'].
639 destruct lev' as [|ec' lev'].
643 set (@eqd_dec (HaskLevel Γ) (haskLevelEqDecidable Γ) (ec' :: lev') (ec :: nil)) as q.
648 unfold flatten_leveled_type.
662 Definition arrange_esc : forall Γ Δ ec succ t,
664 [Γ > Δ > mapOptionTree (flatten_leveled_type ) succ |- [(@ga_mk _ (v2t ec) [] [flatten_type t]) @@ nil]]
665 [Γ > Δ > mapOptionTree (flatten_leveled_type ) (drop_lev (ec :: nil) succ),,
666 [(@ga_mk _ (v2t ec) []
667 (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: nil) succ))) @@ nil]
668 |- [(@ga_mk _ (v2t ec) [] [flatten_type t]) @@ nil]].
671 set (@arrange _ succ (levelMatch (ec::nil))) as q.
672 set (arrangeMap _ _ flatten_leveled_type q) as y.
684 unfold mkDropFlags; simpl.
688 destruct (General.list_eq_dec h0 (ec :: nil)).
704 apply (Prelude_error "escapifying code with multi-leaf antecedents is not supported").
707 Lemma mapOptionTree_distributes
708 : forall T R (a b:Tree ??T) (f:T->R),
709 mapOptionTree f (a,,b) = (mapOptionTree f a),,(mapOptionTree f b).
713 Definition decide_tree_empty : forall {T:Type}(t:Tree ??T),
714 sum { q:Tree unit & t = mapTree (fun _ => None) q } unit.
719 | T_Branch b1 b2 => let b1' := foo b1 in let b2' := foo b2 in _
739 Definition flatten_proof :
742 ND Rule (mapOptionTree (flatten_judgment ) h) (mapOptionTree (flatten_judgment ) c).
744 eapply nd_map'; [ idtac | apply X ].
749 refine (match X as R in Rule H C with
750 | RArrange Γ Δ a b x d => let case_RArrange := tt in _
751 | RNote Γ Δ Σ τ l n => let case_RNote := tt in _
752 | RLit Γ Δ l _ => let case_RLit := tt in _
753 | RVar Γ Δ σ lev => let case_RVar := tt in _
754 | RGlobal Γ Δ σ l wev => let case_RGlobal := tt in _
755 | RLam Γ Δ Σ tx te lev => let case_RLam := tt in _
756 | RCast Γ Δ Σ σ τ lev γ => let case_RCast := tt in _
757 | RAbsT Γ Δ Σ κ σ lev => let case_RAbsT := tt in _
758 | RAppT Γ Δ Σ κ σ τ lev => let case_RAppT := tt in _
759 | RAppCo Γ Δ Σ κ σ₁ σ₂ γ σ lev => let case_RAppCo := tt in _
760 | RAbsCo Γ Δ Σ κ σ σ₁ σ₂ lev => let case_RAbsCo := tt in _
761 | RApp Γ Δ Σ₁ Σ₂ tx te lev => let case_RApp := tt in _
762 | RLet Γ Δ Σ₁ Σ₂ σ₁ σ₂ lev => let case_RLet := tt in _
763 | RJoin Γ p lri m x q => let case_RJoin := tt in _
764 | RVoid _ _ => let case_RVoid := tt in _
765 | RBrak Γ Δ t ec succ lev => let case_RBrak := tt in _
766 | REsc Γ Δ t ec succ lev => let case_REsc := tt in _
767 | RCase Γ Δ lev tc Σ avars tbranches alts => let case_RCase := tt in _
768 | RLetRec Γ Δ lri x y t => let case_RLetRec := tt in _
771 destruct case_RArrange.
772 apply (flatten_arrangement'' Γ Δ a b x d).
777 change ([flatten_type (<[ ec |- t ]>) @@ nil])
778 with ([ga_mk (v2t ec) [] [flatten_type t] @@ nil]).
779 refine (ga_unkappa Γ Δ (v2t ec) nil (mapOptionTree (flatten_type ○ unlev) (take_lev (ec::nil) succ)) _
780 (mapOptionTree (flatten_leveled_type) (drop_lev (ec::nil) succ)) ;; _ ).
782 apply (Prelude_error "found Brak at depth >0 indicating 3-level code; only two-level code is currently supported").
788 change ([flatten_leveled_type (<[ ec |- t ]> @@ nil)])
789 with ([ga_mk (v2t ec) [] [flatten_type t] @@ nil]).
790 eapply nd_comp; [ apply arrange_esc | idtac ].
791 set (decide_tree_empty (take_lev (ec :: nil) succ)) as q'.
797 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanR ].
798 eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
799 eapply nd_comp; [ apply nd_llecnac | idtac ].
800 apply nd_prod; [ idtac | eapply boost ].
803 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanR ].
812 (* environment has non-empty leaves *)
813 apply (ga_kappa Γ Δ (v2t ec) nil (mapOptionTree (flatten_type ○ unlev) (take_lev (ec::nil) succ)) _ _).
814 apply (Prelude_error "found Esc at depth >0 indicating 3-level code; only two-level code is currently supported").
819 apply nd_rule; apply RNote; auto.
820 apply nd_rule; apply RNote; auto.
825 unfold flatten_leveled_type.
827 rewrite literal_types_unchanged.
828 apply nd_rule; apply RLit.
829 unfold take_lev; simpl.
830 unfold drop_lev; simpl.
832 rewrite literal_types_unchanged.
836 Opaque flatten_judgment.
838 Transparent flatten_judgment.
840 unfold flatten_judgment.
843 apply nd_rule. apply RVar.
844 repeat drop_simplify.
845 repeat take_simplify.
849 destruct case_RGlobal.
853 destruct l as [|ec lev]; simpl.
854 destruct (eqd_dec (g:CoreVar) (hetmet_flatten:CoreVar)).
855 set (flatten_type (g wev)) as t.
856 set (RGlobal _ Δ nil (mkGlobal Γ t hetmet_id)) as q.
861 destruct (eqd_dec (g:CoreVar) (hetmet_unflatten:CoreVar)).
862 set (flatten_type (g wev)) as t.
863 set (RGlobal _ Δ nil (mkGlobal Γ t hetmet_id)) as q.
868 unfold flatten_leveled_type. simpl.
869 apply nd_rule; rewrite globals_do_not_have_code_types.
871 apply (Prelude_error "found RGlobal at depth >0; globals should never appear inside code brackets unless escaped").
877 destruct lev as [|ec lev]; simpl; [ apply nd_rule; apply RLam; auto | idtac ].
878 repeat drop_simplify.
879 repeat take_simplify.
891 destruct lev as [|ec lev]; simpl; [ apply nd_rule; apply RCast; auto | idtac ].
892 apply flatten_coercion; auto.
893 apply (Prelude_error "RCast at level >0; casting inside of code brackets is currently not supported").
897 destruct (getjlev x); destruct (getjlev q);
898 [ apply nd_rule; apply RJoin | idtac | idtac | idtac ];
899 apply (Prelude_error "RJoin at depth >0").
904 destruct lev as [|ec lev]. simpl. apply nd_rule.
905 unfold flatten_leveled_type at 4.
906 unfold flatten_leveled_type at 2.
908 replace (flatten_type (tx ---> te))
909 with (flatten_type tx ---> flatten_type te).
913 repeat drop_simplify.
914 repeat take_simplify.
915 rewrite mapOptionTree_distributes.
916 set (mapOptionTree (flatten_leveled_type ) (drop_lev (ec :: lev) Σ₁)) as Σ₁'.
917 set (mapOptionTree (flatten_leveled_type ) (drop_lev (ec :: lev) Σ₂)) as Σ₂'.
918 set (take_lev (ec :: lev) Σ₁) as Σ₁''.
919 set (take_lev (ec :: lev) Σ₂) as Σ₂''.
920 replace (flatten_type (tx ---> te)) with ((flatten_type tx) ---> (flatten_type te)).
921 apply (Prelude_error "FIXME: ga_apply").
925 Notation "` x" := (take_lev _ x).
926 Notation "`` x" := (mapOptionTree unlev x) (at level 20).
927 Notation "``` x" := ((drop_lev _ x)) (at level 20).
928 Notation "!<[]> x" := (flatten_type _ x) (at level 1).
929 Notation "!<[@]> x" := (mapOptionTree flatten_leveled_type x) (at level 1).
934 destruct lev as [|ec lev]; simpl; [ apply nd_rule; apply RLet; auto | idtac ].
935 repeat drop_simplify.
936 repeat take_simplify.
940 eapply nd_prod; [ idtac | apply nd_id ].
962 simpl. destruct lev; simpl.
963 unfold flatten_leveled_type.
965 rewrite flatten_commutes_with_HaskTAll.
966 rewrite flatten_commutes_with_substT.
971 apply (Prelude_error "found type application at level >0; this is not supported").
974 simpl. destruct lev; simpl.
975 unfold flatten_leveled_type at 4.
976 unfold flatten_leveled_type at 2.
978 rewrite flatten_commutes_with_HaskTAll.
979 rewrite flatten_commutes_with_HaskTApp.
980 eapply nd_comp; [ idtac | eapply nd_rule; eapply RAbsT ].
982 set (mapOptionTree (flatten_leveled_type ) (mapOptionTree (weakLT(κ:=κ)) Σ)) as a.
983 set (mapOptionTree (weakLT(κ:=κ)) (mapOptionTree (flatten_leveled_type ) Σ)) as q'.
991 rewrite flatten_commutes_with_weakLT.
1002 apply (Prelude_error "found type abstraction at level >0; this is not supported").
1004 destruct case_RAppCo.
1005 simpl. destruct lev; simpl.
1006 unfold flatten_leveled_type at 4.
1007 unfold flatten_leveled_type at 2.
1008 unfold flatten_type.
1012 apply flatten_coercion.
1014 apply (Prelude_error "found coercion application at level >0; this is not supported").
1016 destruct case_RAbsCo.
1017 simpl. destruct lev; simpl.
1018 unfold flatten_type.
1020 apply (Prelude_error "AbsCo not supported (FIXME)").
1021 apply (Prelude_error "found coercion abstraction at level >0; this is not supported").
1023 destruct case_RLetRec.
1026 apply (Prelude_error "LetRec not supported (FIXME)").
1028 destruct case_RCase.
1030 apply (Prelude_error "Case not supported (BIG FIXME)").
1034 (* to do: establish some metric on judgments (max length of level of any succedent type, probably), show how to
1035 * calculate it, and show that the flattening procedure above drives it down by one *)
1038 Instance FlatteningFunctor {Γ}{Δ}{ec} : Functor (JudgmentsL (PCF Γ Δ ec)) (TypesL (SystemFCa Γ Δ)) (obact) :=
1039 { fmor := FlatteningFunctor_fmor }.
1041 Definition ReificationFunctor Γ Δ : Functor (JudgmentsL _ _ (PCF n Γ Δ)) SystemFCa' (mapOptionTree brakifyJudg).
1042 refine {| fmor := ReificationFunctor_fmor Γ Δ |}; unfold hom; unfold ob; simpl ; intros.
1044 Definition PCF_SMME (n:nat)(Γ:TypeEnv)(Δ:CoercionEnv Γ) : ProgrammingLanguageSMME.
1045 refine {| plsmme_pl := PCF n Γ Δ |}.
1048 Definition SystemFCa_SMME (n:nat)(Γ:TypeEnv)(Δ:CoercionEnv Γ) : ProgrammingLanguageSMME.
1049 refine {| plsmme_pl := SystemFCa n Γ Δ |}.
1052 Definition ReificationFunctorMonoidal n : MonoidalFunctor (JudgmentsN n) (JudgmentsN (S n)) (ReificationFunctor n).
1056 Definition PCF_SystemFCa_two_level n Γ Δ : TwoLevelLanguage (PCF_SMME n Γ Δ) (SystemFCa_SMME (S n) Γ Δ).
1059 (* ... and the retraction exists *)
1063 Implicit Arguments garrow [ ].