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.
33 Require Import HaskSkolemizer.
36 Set Printing Width 130.
39 * The flattening transformation. Currently only TWO-level languages are
40 * supported, and the level-1 sublanguage is rather limited.
42 * This file abuses terminology pretty badly. For purposes of this file,
43 * "PCF" means "the level-1 sublanguage" and "FC" (aka System FC) means
44 * the whole language (level-0 language including bracketed level-1 terms)
46 Section HaskFlattener.
48 Definition getlev {Γ}{κ}(lht:LeveledHaskType Γ κ) : HaskLevel Γ :=
49 match lht with t @@ l => l end.
52 forall {T} (Σ:Tree ??T) (f:T -> bool),
53 Arrange Σ (dropT (mkFlags (liftBoolFunc false f) Σ),,( (dropT (mkFlags (liftBoolFunc false (bnot ○ f)) Σ)))).
59 destruct (f t); simpl.
65 eapply RComp; [ idtac | apply arrangeSwapMiddle ].
74 forall {T} (Σ:Tree ??T) (f:T -> bool),
75 Arrange (dropT (mkFlags (liftBoolFunc false f) Σ),,( (dropT (mkFlags (liftBoolFunc false (bnot ○ f)) Σ)))) Σ.
81 destruct (f t); simpl.
87 eapply RComp; [ apply arrangeSwapMiddle | idtac ].
97 | [ |- context[@eqd_dec ?T ?V ?X ?X] ] =>
98 destruct (@eqd_dec T V X X) as [eqd_dec1 | eqd_dec2];
99 [ clear eqd_dec1 | set (eqd_dec2 (refl_equal _)) as eqd_dec2'; inversion eqd_dec2' ]
102 Definition v2t {Γ}(ec:HaskTyVar Γ ECKind) : HaskType Γ ECKind := fun TV ite => TVar (ec TV ite).
104 Definition levelMatch {Γ}(lev:HaskLevel Γ) : LeveledHaskType Γ ★ -> bool :=
105 fun t => match t with ttype@@tlev => if eqd_dec tlev lev then true else false end.
107 (* In a tree of types, replace any type at depth "lev" or greater None *)
108 Definition mkDropFlags {Γ}(lev:HaskLevel Γ)(tt:Tree ??(LeveledHaskType Γ ★)) : TreeFlags tt :=
109 mkFlags (liftBoolFunc false (levelMatch lev)) tt.
111 Definition drop_lev {Γ}(lev:HaskLevel Γ)(tt:Tree ??(LeveledHaskType Γ ★)) : Tree ??(LeveledHaskType Γ ★) :=
112 dropT (mkDropFlags lev tt).
114 (* The opposite: replace any type which is NOT at level "lev" with None *)
115 Definition mkTakeFlags {Γ}(lev:HaskLevel Γ)(tt:Tree ??(LeveledHaskType Γ ★)) : TreeFlags tt :=
116 mkFlags (liftBoolFunc true (bnot ○ levelMatch lev)) tt.
118 Definition take_lev {Γ}(lev:HaskLevel Γ)(tt:Tree ??(LeveledHaskType Γ ★)) : Tree ??(LeveledHaskType Γ ★) :=
119 dropT (mkTakeFlags lev tt).
121 mapOptionTree (fun x => flatten_type (unlev x))
122 (maybeTree (takeT tt (mkFlags (
123 fun t => match t with
124 | Some (ttype @@ tlev) => if eqd_dec tlev lev then true else false
129 Definition maybeTree {T}(t:??(Tree ??T)) : Tree ??T :=
136 Lemma drop_lev_lemma : forall Γ (lev:HaskLevel Γ) x, drop_lev lev [x @@ lev] = [].
148 Lemma drop_lev_lemma_s : forall Γ (lev:HaskLevel Γ) ec x, drop_lev (ec::lev) [x @@ (ec :: lev)] = [].
159 Lemma take_lemma : forall Γ (lev:HaskLevel Γ) x, take_lev lev [x @@ lev] = [x @@ lev].
170 Lemma take_lemma' : forall Γ (lev:HaskLevel Γ) x, take_lev lev (x @@@ lev) = x @@@ lev.
173 destruct a; simpl; try reflexivity.
176 rewrite <- IHx1 at 2.
177 rewrite <- IHx2 at 2.
181 Lemma drop_lev_lemma' : forall Γ (lev:HaskLevel Γ) x, drop_lev lev (x @@@ lev) = [].
184 destruct a; simpl; try reflexivity.
185 apply drop_lev_lemma.
187 change (@drop_lev _ lev (x1 @@@ lev ,, x2 @@@ lev))
188 with ((@drop_lev _ lev (x1 @@@ lev)) ,, (@drop_lev _ lev (x2 @@@ lev))).
195 Ltac drop_simplify :=
197 | [ |- context[@drop_lev ?G ?L [ ?X @@ ?L ] ] ] =>
198 rewrite (drop_lev_lemma G L X)
200 | [ |- context[@drop_lev ?G ?L [ ?X @@@ ?L ] ] ] =>
201 rewrite (drop_lev_lemma' G L X)
203 | [ |- context[@drop_lev ?G (?E :: ?L) [ ?X @@ (?E :: ?L) ] ] ] =>
204 rewrite (drop_lev_lemma_s G L E X)
205 | [ |- context[@drop_lev ?G ?N (?A,,?B)] ] =>
206 change (@drop_lev G N (A,,B)) with ((@drop_lev G N A),,(@drop_lev G N B))
207 | [ |- context[@drop_lev ?G ?N (T_Leaf None)] ] =>
208 change (@drop_lev G N (T_Leaf (@None (LeveledHaskType G ★)))) with (T_Leaf (@None (LeveledHaskType G ★)))
211 Ltac take_simplify :=
213 | [ |- context[@take_lev ?G ?L [ ?X @@ ?L ] ] ] =>
214 rewrite (take_lemma G L X)
215 | [ |- context[@take_lev ?G ?L [ ?X @@@ ?L ] ] ] =>
216 rewrite (take_lemma' G L X)
217 | [ |- context[@take_lev ?G ?N (?A,,?B)] ] =>
218 change (@take_lev G N (A,,B)) with ((@take_lev G N A),,(@take_lev G N B))
219 | [ |- context[@take_lev ?G ?N (T_Leaf None)] ] =>
220 change (@take_lev G N (T_Leaf (@None (LeveledHaskType G ★)))) with (T_Leaf (@None (LeveledHaskType G ★)))
224 (*******************************************************************************)
227 Context (hetmet_flatten : WeakExprVar).
228 Context (hetmet_unflatten : WeakExprVar).
229 Context (hetmet_id : WeakExprVar).
230 Context {unitTy : forall TV, RawHaskType TV ECKind -> RawHaskType TV ★ }.
231 Context {prodTy : forall TV, RawHaskType TV ECKind -> RawHaskType TV ★ -> RawHaskType TV ★ -> RawHaskType TV ★ }.
232 Context {gaTy : forall TV, RawHaskType TV ECKind -> RawHaskType TV ★ -> RawHaskType TV ★ -> RawHaskType TV ★ }.
234 Definition ga_mk_tree' {TV}(ec:RawHaskType TV ECKind)(tr:Tree ??(RawHaskType TV ★)) : RawHaskType TV ★ :=
235 reduceTree (unitTy TV ec) (prodTy TV ec) tr.
237 Definition ga_mk_tree {Γ}(ec:HaskType Γ ECKind)(tr:Tree ??(HaskType Γ ★)) : HaskType Γ ★ :=
238 fun TV ite => ga_mk_tree' (ec TV ite) (mapOptionTree (fun x => x TV ite) tr).
240 Definition ga_mk_raw {TV}(ec:RawHaskType TV ECKind)(ant suc:Tree ??(RawHaskType TV ★)) : RawHaskType TV ★ :=
242 (ga_mk_tree' ec (ant,,(mapOptionTreeAndFlatten (unleaves ○ take_arg_types) suc)))
243 (ga_mk_tree' ec ( mapOptionTree drop_arg_types suc) ).
245 Definition ga_mk {Γ}(ec:HaskType Γ ECKind )(ant suc:Tree ??(HaskType Γ ★)) : HaskType Γ ★ :=
246 fun TV ite => ga_mk_raw (ec TV ite) (mapOptionTree (fun x => x TV ite) ant) (mapOptionTree (fun x => x TV ite) suc).
250 * - code types <[t]>@c become garrows c () t
251 * - free variables of type t at a level lev deeper than the succedent become garrows c () t
252 * - free variables at the level of the succedent become
254 Fixpoint flatten_rawtype {TV}{κ}(exp: RawHaskType TV κ) : RawHaskType TV κ :=
257 | TAll _ y => TAll _ (fun v => flatten_rawtype (y v))
258 | TApp _ _ x y => TApp (flatten_rawtype x) (flatten_rawtype y)
260 | TCoerc _ t1 t2 t => TCoerc (flatten_rawtype t1) (flatten_rawtype t2) (flatten_rawtype t)
262 | TCode ec e => let e' := flatten_rawtype e
263 in ga_mk_raw ec (unleaves' (take_arg_types e')) [drop_arg_types e']
264 | TyFunApp tfc kl k lt => TyFunApp tfc kl k (flatten_rawtype_list _ lt)
266 with flatten_rawtype_list {TV}(lk:list Kind)(exp:@RawHaskTypeList TV lk) : @RawHaskTypeList TV lk :=
267 match exp in @RawHaskTypeList _ LK return @RawHaskTypeList TV LK with
268 | TyFunApp_nil => TyFunApp_nil
269 | TyFunApp_cons κ kl t rest => TyFunApp_cons _ _ (flatten_rawtype t) (flatten_rawtype_list _ rest)
272 Definition flatten_type {Γ}{κ}(ht:HaskType Γ κ) : HaskType Γ κ :=
273 fun TV ite => flatten_rawtype (ht TV ite).
275 Fixpoint levels_to_tcode {Γ}(ht:HaskType Γ ★)(lev:HaskLevel Γ) : HaskType Γ ★ :=
277 | nil => flatten_type ht
278 | ec::lev' => @ga_mk _ (v2t ec) [] [levels_to_tcode ht lev']
281 Definition flatten_leveled_type {Γ}(ht:LeveledHaskType Γ ★) : LeveledHaskType Γ ★ :=
282 levels_to_tcode (unlev ht) (getlev ht) @@ nil.
286 Axiom literal_types_unchanged : forall Γ l, flatten_type (literalType l) = literalType(Γ:=Γ) l.
288 Axiom flatten_coercion : forall Γ Δ κ (σ τ:HaskType Γ κ) (γ:HaskCoercion Γ Δ (σ ∼∼∼ τ)),
289 HaskCoercion Γ Δ (flatten_type σ ∼∼∼ flatten_type τ).
291 Axiom flatten_commutes_with_substT :
292 forall κ Γ (Δ:CoercionEnv Γ) (σ:∀ TV, InstantiatedTypeEnv TV Γ → TV κ → RawHaskType TV ★) (τ:HaskType Γ κ),
293 flatten_type (substT σ τ) = substT (fun TV ite v => flatten_rawtype (σ TV ite v))
296 Axiom flatten_commutes_with_HaskTAll :
297 forall κ Γ (Δ:CoercionEnv Γ) (σ:∀ TV, InstantiatedTypeEnv TV Γ → TV κ → RawHaskType TV ★),
298 flatten_type (HaskTAll κ σ) = HaskTAll κ (fun TV ite v => flatten_rawtype (σ TV ite v)).
300 Axiom flatten_commutes_with_HaskTApp :
301 forall κ Γ (Δ:CoercionEnv Γ) (σ:∀ TV, InstantiatedTypeEnv TV Γ → TV κ → RawHaskType TV ★),
302 flatten_type (HaskTApp (weakF σ) (FreshHaskTyVar κ)) =
303 HaskTApp (weakF (fun TV ite v => flatten_rawtype (σ TV ite v))) (FreshHaskTyVar κ).
305 Axiom flatten_commutes_with_weakLT : forall (Γ:TypeEnv) κ t,
306 flatten_leveled_type (weakLT(Γ:=Γ)(κ:=κ) t) = weakLT(Γ:=Γ)(κ:=κ) (flatten_leveled_type t).
308 Axiom globals_do_not_have_code_types : forall (Γ:TypeEnv) (g:Global Γ) v,
309 flatten_type (g v) = g v.
311 (* This tries to assign a single level to the entire succedent of a judgment. If the succedent has types from different
312 * levels (should not happen) it just picks one; if the succedent has no non-None leaves (also should not happen) it
314 Definition getΓ (j:Judg) := match j with Γ > _ > _ |- _ => Γ end.
315 Definition getSuc (j:Judg) : Tree ??(LeveledHaskType (getΓ j) ★) :=
316 match j as J return Tree ??(LeveledHaskType (getΓ J) ★) with Γ > _ > _ |- s => s end.
317 Fixpoint getjlev {Γ}(tt:Tree ??(LeveledHaskType Γ ★)) : HaskLevel Γ :=
320 | T_Leaf (Some (_ @@ lev)) => lev
322 match getjlev b1 with
328 (* "n" is the maximum depth remaining AFTER flattening *)
329 Definition flatten_judgment (j:Judg) :=
330 match j as J return Judg with
331 Γ > Δ > ant |- suc =>
332 match getjlev suc with
333 | nil => Γ > Δ > mapOptionTree flatten_leveled_type ant
334 |- mapOptionTree flatten_leveled_type suc
336 | (ec::lev') => Γ > Δ > mapOptionTree flatten_leveled_type (drop_lev (ec::lev') ant)
338 (mapOptionTree (flatten_type ○ unlev) (take_lev (ec::lev') ant))
339 (mapOptionTree (flatten_type ○ unlev) suc )
340 @@ nil] (* we know the level of all of suc *)
345 { ga_id : ∀ Γ Δ ec l a , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec a a @@ l] ]
346 ; ga_cancelr : ∀ Γ Δ ec l a , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec (a,,[]) a @@ l] ]
347 ; ga_cancell : ∀ Γ Δ ec l a , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec ([],,a) a @@ l] ]
348 ; ga_uncancelr : ∀ Γ Δ ec l a , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec a (a,,[]) @@ l] ]
349 ; ga_uncancell : ∀ Γ Δ ec l a , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec a ([],,a) @@ l] ]
350 ; ga_assoc : ∀ Γ Δ ec l a b c, ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec ((a,,b),,c) (a,,(b,,c)) @@ l] ]
351 ; ga_unassoc : ∀ Γ Δ ec l a b c, ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec (a,,(b,,c)) ((a,,b),,c) @@ l] ]
352 ; ga_swap : ∀ Γ Δ ec l a b , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec (a,,b) (b,,a) @@ l] ]
353 ; ga_drop : ∀ Γ Δ ec l a , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec a [] @@ l] ]
354 ; ga_copy : ∀ Γ Δ ec l a , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec a (a,,a) @@ l] ]
355 ; ga_first : ∀ Γ Δ ec l a b x, ND Rule [] [Γ > Δ > [@ga_mk Γ ec a b @@ l] |- [@ga_mk Γ ec (a,,x) (b,,x) @@ l] ]
356 ; ga_second : ∀ Γ Δ ec l a b x, ND Rule [] [Γ > Δ > [@ga_mk Γ ec a b @@ l] |- [@ga_mk Γ ec (x,,a) (x,,b) @@ l] ]
357 ; ga_lit : ∀ Γ Δ ec l lit , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec [] [literalType lit] @@ l] ]
358 ; ga_curry : ∀ Γ Δ ec l a b c, ND Rule [] [Γ > Δ > [@ga_mk Γ ec (a,,[b]) [c] @@ l] |- [@ga_mk Γ ec a [b ---> c] @@ l] ]
359 ; 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] ]
360 ; ga_apply : ∀ Γ Δ ec l a a' b c,
361 ND Rule [] [Γ > Δ > [@ga_mk Γ ec a [b ---> c] @@ l],,[@ga_mk Γ ec a' [b] @@ l] |- [@ga_mk Γ ec (a,,a') [c] @@ l] ]
362 ; ga_kappa : ∀ Γ Δ ec l a b Σ, ND Rule
363 [Γ > Δ > Σ,,[@ga_mk Γ ec [] a @@ l] |- [@ga_mk Γ ec [] b @@ l] ]
364 [Γ > Δ > Σ |- [@ga_mk Γ ec a b @@ l] ]
366 Context `(gar:garrow).
368 Notation "a ~~~~> b" := (@ga_mk _ _ a b) (at level 20).
370 Definition boost : forall Γ Δ ant x y {lev},
371 ND Rule [] [ Γ > Δ > [x@@lev] |- [y@@lev] ] ->
372 ND Rule [ Γ > Δ > ant |- [x@@lev] ] [ Γ > Δ > ant |- [y@@lev] ].
374 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanL ].
375 eapply nd_comp; [ idtac | eapply nd_rule; apply (@RLet Γ Δ [] ant y x lev) ].
376 eapply nd_comp; [ apply nd_rlecnac | idtac ].
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] ].
390 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RExch ].
391 eapply nd_comp; [ idtac
392 | eapply nd_rule; apply (@RLet Γ Δ [@ga_mk _ ec b c @@lev] Σ (@ga_mk _ ec a c) (@ga_mk _ ec a b) lev) ].
393 eapply nd_comp; [ apply nd_llecnac | idtac ].
396 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RExch ].
400 Definition precompose Γ Δ ec : forall a x y z lev,
402 [ Γ > Δ > a |- [@ga_mk _ ec y z @@ lev] ]
403 [ Γ > Δ > a,,[@ga_mk _ ec x y @@ lev] |- [@ga_mk _ ec x z @@ lev] ].
412 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RExch ].
418 Definition precompose' : ∀ Γ Δ ec lev a b c Σ,
419 ND Rule [] [ Γ > Δ > Σ |- [@ga_mk Γ ec b c @@ lev] ] ->
420 ND Rule [] [ Γ > Δ > Σ,,[@ga_mk Γ ec a b @@ lev] |- [@ga_mk Γ ec a c @@ lev] ].
427 Definition postcompose : ∀ Γ Δ ec lev a b c,
428 ND Rule [] [ Γ > Δ > [] |- [@ga_mk Γ ec a b @@ lev] ] ->
429 ND Rule [] [ Γ > Δ > [@ga_mk Γ ec b c @@ lev] |- [@ga_mk Γ ec a c @@ lev] ].
439 Definition firstify : ∀ Γ Δ ec lev a b c Σ,
440 ND Rule [] [ Γ > Δ > Σ |- [@ga_mk Γ ec a b @@ lev] ] ->
441 ND Rule [] [ Γ > Δ > Σ |- [@ga_mk Γ ec (a,,c) (b,,c) @@ lev] ].
443 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanL ].
444 eapply nd_comp; [ idtac | eapply nd_rule; apply RLet ].
445 eapply nd_comp; [ apply nd_llecnac | idtac ].
448 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RuCanL ].
452 Definition secondify : ∀ Γ Δ ec lev a b c Σ,
453 ND Rule [] [ Γ > Δ > Σ |- [@ga_mk Γ ec a b @@ lev] ] ->
454 ND Rule [] [ Γ > Δ > Σ |- [@ga_mk Γ ec (c,,a) (c,,b) @@ lev] ].
456 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanL ].
457 eapply nd_comp; [ idtac | eapply nd_rule; apply RLet ].
458 eapply nd_comp; [ apply nd_llecnac | idtac ].
461 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RuCanL ].
465 Lemma ga_unkappa : ∀ Γ Δ ec l z a b Σ,
467 [Γ > Δ > Σ |- [@ga_mk Γ ec a b @@ l] ]
468 [Γ > Δ > Σ,,[@ga_mk Γ ec z a @@ l] |- [@ga_mk Γ ec z b @@ l] ].
470 set (ga_comp Γ Δ ec l z a b) as q.
472 set (@RLet Γ Δ) as q'.
473 set (@RLet Γ Δ [@ga_mk _ ec z a @@ l] Σ (@ga_mk _ ec z b) (@ga_mk _ ec a b) l) as q''.
494 Lemma ga_unkappa' : ∀ Γ Δ ec l a b Σ x,
496 [Γ > Δ > Σ |- [@ga_mk Γ ec (a,,x) b @@ l] ]
497 [Γ > Δ > Σ,,[@ga_mk Γ ec [] a @@ l] |- [@ga_mk Γ ec x b @@ l] ].
499 eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
500 eapply nd_comp; [ apply nd_llecnac | idtac ].
504 eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
505 eapply nd_comp; [ apply nd_llecnac | idtac ].
512 Lemma ga_kappa' : ∀ Γ Δ ec l a b Σ x,
514 [Γ > Δ > Σ,,[@ga_mk Γ ec [] a @@ l] |- [@ga_mk Γ ec x b @@ l] ]
515 [Γ > Δ > Σ |- [@ga_mk Γ ec (a,,x) b @@ l] ].
516 apply (Prelude_error "ga_kappa not supported yet (BIG FIXME)").
519 (* useful for cutting down on the pretty-printed noise
521 Notation "` x" := (take_lev _ x) (at level 20).
522 Notation "`` x" := (mapOptionTree unlev x) (at level 20).
523 Notation "``` x" := (drop_lev _ x) (at level 20).
525 Definition flatten_arrangement' :
526 forall Γ (Δ:CoercionEnv Γ)
527 (ec:HaskTyVar Γ ECKind) (lev:HaskLevel Γ) (ant1 ant2:Tree ??(LeveledHaskType Γ ★)) (r:Arrange ant1 ant2),
528 ND Rule [] [Γ > Δ > [] |- [@ga_mk _ (v2t ec) (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) ant2))
529 (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) ant1)) @@ nil] ].
532 refine (fix flatten ant1 ant2 (r:Arrange ant1 ant2):
533 ND Rule [] [Γ > Δ > [] |- [@ga_mk _ (v2t ec)
534 (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) ant2))
535 (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) ant1)) @@ nil]] :=
536 match r as R in Arrange A B return
537 ND Rule [] [Γ > Δ > [] |- [@ga_mk _ (v2t ec)
538 (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) B))
539 (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) A)) @@ nil]]
541 | RCanL a => let case_RCanL := tt in ga_uncancell _ _ _ _ _
542 | RCanR a => let case_RCanR := tt in ga_uncancelr _ _ _ _ _
543 | RuCanL a => let case_RuCanL := tt in ga_cancell _ _ _ _ _
544 | RuCanR a => let case_RuCanR := tt in ga_cancelr _ _ _ _ _
545 | RAssoc a b c => let case_RAssoc := tt in ga_assoc _ _ _ _ _ _ _
546 | RCossa a b c => let case_RCossa := tt in ga_unassoc _ _ _ _ _ _ _
547 | RExch a b => let case_RExch := tt in ga_swap _ _ _ _ _ _
548 | RWeak a => let case_RWeak := tt in ga_drop _ _ _ _ _
549 | RCont a => let case_RCont := tt in ga_copy _ _ _ _ _
550 | RLeft a b c r' => let case_RLeft := tt in flatten _ _ r' ;; boost _ _ _ _ _ (ga_second _ _ _ _ _ _ _)
551 | RRight a b c r' => let case_RRight := tt in flatten _ _ r' ;; boost _ _ _ _ _ (ga_first _ _ _ _ _ _ _)
552 | RComp c b a r1 r2 => let case_RComp := tt in (fun r1' r2' => _) (flatten _ _ r1) (flatten _ _ r2)
553 end); clear flatten; repeat take_simplify; repeat drop_simplify; intros.
556 set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) a)) as a' in *.
557 set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) b)) as b' in *.
558 set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) c)) as c' in *.
559 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RCanL ].
560 eapply nd_comp; [ idtac | eapply nd_rule; apply
561 (@RLet Γ Δ [] [] (@ga_mk _ (v2t ec) a' c') (@ga_mk _ (v2t ec) a' b')) ].
562 eapply nd_comp; [ apply nd_llecnac | idtac ].
565 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RuCanL ].
566 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RCanR ].
567 eapply nd_comp; [ idtac | eapply nd_rule; apply
568 (@RLet Γ Δ [@ga_mk _ (v2t ec) a' b' @@ _] [] (@ga_mk _ (v2t ec) a' c') (@ga_mk _ (v2t ec) b' c'))].
569 eapply nd_comp; [ apply nd_llecnac | idtac ].
575 Definition flatten_arrangement :
576 forall Γ (Δ:CoercionEnv Γ) n
577 (ec:HaskTyVar Γ ECKind) (lev:HaskLevel Γ) (ant1 ant2:Tree ??(LeveledHaskType Γ ★)) (r:Arrange ant1 ant2) succ,
579 [Γ > Δ > mapOptionTree (flatten_leveled_type ) (drop_lev n ant1)
580 |- [@ga_mk _ (v2t ec)
581 (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) ant1))
582 (mapOptionTree (flatten_type ○ unlev) succ) @@ nil]]
583 [Γ > Δ > mapOptionTree (flatten_leveled_type ) (drop_lev n ant2)
584 |- [@ga_mk _ (v2t ec)
585 (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) ant2))
586 (mapOptionTree (flatten_type ○ unlev) succ) @@ nil]].
588 refine ( _ ;; (boost _ _ _ _ _ (postcompose _ _ _ _ _ _ _ (flatten_arrangement' Γ Δ ec lev ant1 ant2 r)))).
591 refine ((fix flatten ant1 ant2 (r:Arrange ant1 ant2) :=
592 match r as R in Arrange A B return
593 Arrange (mapOptionTree (flatten_leveled_type ) (drop_lev _ A))
594 (mapOptionTree (flatten_leveled_type ) (drop_lev _ B)) with
595 | RCanL a => let case_RCanL := tt in RCanL _
596 | RCanR a => let case_RCanR := tt in RCanR _
597 | RuCanL a => let case_RuCanL := tt in RuCanL _
598 | RuCanR a => let case_RuCanR := tt in RuCanR _
599 | RAssoc a b c => let case_RAssoc := tt in RAssoc _ _ _
600 | RCossa a b c => let case_RCossa := tt in RCossa _ _ _
601 | RExch a b => let case_RExch := tt in RExch _ _
602 | RWeak a => let case_RWeak := tt in RWeak _
603 | RCont a => let case_RCont := tt in RCont _
604 | RLeft a b c r' => let case_RLeft := tt in RLeft _ (flatten _ _ r')
605 | RRight a b c r' => let case_RRight := tt in RRight _ (flatten _ _ r')
606 | RComp a b c r1 r2 => let case_RComp := tt in RComp (flatten _ _ r1) (flatten _ _ r2)
607 end) ant1 ant2 r); clear flatten; repeat take_simplify; repeat drop_simplify; intros.
610 Definition flatten_arrangement'' :
611 forall Γ Δ ant1 ant2 succ (r:Arrange ant1 ant2),
612 ND Rule (mapOptionTree (flatten_judgment ) [Γ > Δ > ant1 |- succ])
613 (mapOptionTree (flatten_judgment ) [Γ > Δ > ant2 |- succ]).
616 set (getjlev succ) as succ_lev.
617 assert (succ_lev=getjlev succ).
635 eapply RComp; [ apply IHr1 | apply IHr2 ].
637 apply flatten_arrangement.
641 Definition ga_join Γ Δ Σ₁ Σ₂ a b ec :
642 ND Rule [] [Γ > Δ > Σ₁ |- [@ga_mk _ ec [] a @@ nil]] ->
643 ND Rule [] [Γ > Δ > Σ₂ |- [@ga_mk _ ec [] b @@ nil]] ->
644 ND Rule [] [Γ > Δ > Σ₁,,Σ₂ |- [@ga_mk _ ec [] (a,,b) @@ nil]].
647 apply secondify with (c:=a) in pfb.
650 eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
651 eapply nd_comp; [ eapply nd_llecnac | idtac ].
660 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanL ].
666 Definition arrange_brak : forall Γ Δ ec succ t,
668 [Γ > Δ > mapOptionTree (flatten_leveled_type ) (drop_lev (ec :: nil) succ),,
669 [(@ga_mk _ (v2t ec) [] (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: nil) succ))) @@ nil] |- [t @@ nil]]
670 [Γ > Δ > mapOptionTree (flatten_leveled_type ) succ |- [t @@ nil]].
673 set (@arrange' _ succ (levelMatch (ec::nil))) as q.
674 set (arrangeMap _ _ flatten_leveled_type q) as y.
683 eapply nd_comp; [ apply nd_llecnac | idtac ].
684 eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
689 induction succ; try destruct a; simpl.
695 destruct l as [t' lev'].
696 destruct lev' as [|ec' lev'].
700 set (@eqd_dec (HaskLevel Γ) (haskLevelEqDecidable Γ) (ec' :: lev') (ec :: nil)) as q.
705 unfold flatten_leveled_type.
722 Definition arrange_esc : forall Γ Δ ec succ t,
724 [Γ > Δ > mapOptionTree (flatten_leveled_type ) succ |- [t @@ nil]]
725 [Γ > Δ > mapOptionTree (flatten_leveled_type ) (drop_lev (ec :: nil) succ),,
726 [(@ga_mk _ (v2t ec) [] (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: nil) succ))) @@ nil] |- [t @@ nil]].
729 set (@arrange _ succ (levelMatch (ec::nil))) as q.
730 set (arrangeMap _ _ flatten_leveled_type q) as y.
742 unfold mkDropFlags; simpl.
746 destruct (General.list_eq_dec h0 (ec :: nil)).
762 apply (Prelude_error "escapifying code with multi-leaf antecedents is not supported").
765 Lemma mapOptionTree_distributes
766 : forall T R (a b:Tree ??T) (f:T->R),
767 mapOptionTree f (a,,b) = (mapOptionTree f a),,(mapOptionTree f b).
771 Definition decide_tree_empty : forall {T:Type}(t:Tree ??T),
772 sum { q:Tree unit & t = mapTree (fun _ => None) q } unit.
777 | T_Branch b1 b2 => let b1' := foo b1 in let b2' := foo b2 in _
797 Lemma unlev_relev : forall {Γ}(t:Tree ??(HaskType Γ ★)) lev, mapOptionTree unlev (t @@@ lev) = t.
800 destruct a; reflexivity.
801 rewrite <- IHt1 at 2.
802 rewrite <- IHt2 at 2.
806 Lemma tree_of_nothing : forall Γ ec t a,
807 Arrange (a,,mapOptionTree flatten_leveled_type (drop_lev(Γ:=Γ) (ec :: nil) (t @@@ (ec :: nil)))) a.
809 induction t; try destruct o; try destruct a0.
818 Transparent drop_lev.
829 Lemma tree_of_nothing' : forall Γ ec t a,
830 Arrange a (a,,mapOptionTree flatten_leveled_type (drop_lev(Γ:=Γ) (ec :: nil) (t @@@ (ec :: nil)))).
832 induction t; try destruct o; try destruct a0.
841 Transparent drop_lev.
855 Lemma krunk : forall Γ (ec:HaskTyVar Γ ECKind) t,
856 flatten_type (<[ ec |- t ]>)
858 (mapOptionTree flatten_type (take_arg_types_as_tree Γ t))
859 [ flatten_type (drop_arg_types_as_tree t)].
862 unfold flatten_type at 1.
866 admit. (* BIG HUGE CHEAT FIXME *)
869 Definition flatten_proof :
872 ND Rule (mapOptionTree (flatten_judgment ) h) (mapOptionTree (flatten_judgment ) c).
874 eapply nd_map'; [ idtac | apply X ].
880 (match X as R in SRule H C with
881 | SBrak Γ Δ t ec succ lev => let case_SBrak := tt in _
882 | SEsc Γ Δ t ec succ lev => let case_SEsc := tt in _
883 | SFlat h c r => let case_SFlat := tt in _
887 refine (match r as R in Rule H C with
888 | RArrange Γ Δ a b x d => let case_RArrange := tt in _
889 | RNote Γ Δ Σ τ l n => let case_RNote := tt in _
890 | RLit Γ Δ l _ => let case_RLit := tt in _
891 | RVar Γ Δ σ lev => let case_RVar := tt in _
892 | RGlobal Γ Δ σ l wev => let case_RGlobal := tt in _
893 | RLam Γ Δ Σ tx te lev => let case_RLam := tt in _
894 | RCast Γ Δ Σ σ τ lev γ => let case_RCast := tt in _
895 | RAbsT Γ Δ Σ κ σ lev => let case_RAbsT := tt in _
896 | RAppT Γ Δ Σ κ σ τ lev => let case_RAppT := tt in _
897 | RAppCo Γ Δ Σ κ σ₁ σ₂ γ σ lev => let case_RAppCo := tt in _
898 | RAbsCo Γ Δ Σ κ σ σ₁ σ₂ lev => let case_RAbsCo := tt in _
899 | RApp Γ Δ Σ₁ Σ₂ tx te lev => let case_RApp := tt in _
900 | RLet Γ Δ Σ₁ Σ₂ σ₁ σ₂ lev => let case_RLet := tt in _
901 | RJoin Γ p lri m x q => let case_RJoin := tt in _
902 | RVoid _ _ => let case_RVoid := tt in _
903 | RBrak Γ Δ t ec succ lev => let case_RBrak := tt in _
904 | REsc Γ Δ t ec succ lev => let case_REsc := tt in _
905 | RCase Γ Δ lev tc Σ avars tbranches alts => let case_RCase := tt in _
906 | RLetRec Γ Δ lri x y t => let case_RLetRec := tt in _
909 destruct case_RArrange.
910 apply (flatten_arrangement'' Γ Δ a b x d).
913 apply (Prelude_error "found unskolemized Brak rule; this shouldn't happen").
916 apply (Prelude_error "found unskolemized Esc rule; this shouldn't happen").
921 apply nd_rule; apply RNote; auto.
922 apply nd_rule; apply RNote; auto.
927 unfold flatten_leveled_type.
929 rewrite literal_types_unchanged.
930 apply nd_rule; apply RLit.
931 unfold take_lev; simpl.
932 unfold drop_lev; simpl.
934 rewrite literal_types_unchanged.
938 Opaque flatten_judgment.
940 Transparent flatten_judgment.
942 unfold flatten_judgment.
945 apply nd_rule. apply RVar.
946 repeat drop_simplify.
947 repeat take_simplify.
951 destruct case_RGlobal.
955 destruct l as [|ec lev]; simpl.
956 destruct (eqd_dec (g:CoreVar) (hetmet_flatten:CoreVar)).
957 set (flatten_type (g wev)) as t.
958 set (RGlobal _ Δ nil (mkGlobal Γ t hetmet_id)) as q.
963 destruct (eqd_dec (g:CoreVar) (hetmet_unflatten:CoreVar)).
964 set (flatten_type (g wev)) as t.
965 set (RGlobal _ Δ nil (mkGlobal Γ t hetmet_id)) as q.
970 unfold flatten_leveled_type. simpl.
971 apply nd_rule; rewrite globals_do_not_have_code_types.
973 apply (Prelude_error "found RGlobal at depth >0; globals should never appear inside code brackets unless escaped").
979 destruct lev as [|ec lev]; simpl; [ apply nd_rule; apply RLam; auto | idtac ].
980 repeat drop_simplify.
981 repeat take_simplify.
993 destruct lev as [|ec lev]; simpl; [ apply nd_rule; apply RCast; auto | idtac ].
995 apply flatten_coercion; auto.
996 apply (Prelude_error "RCast at level >0; casting inside of code brackets is currently not supported").
1000 destruct (getjlev x); destruct (getjlev q);
1001 [ apply nd_rule; apply RJoin | idtac | idtac | idtac ];
1002 apply (Prelude_error "RJoin at depth >0").
1007 destruct lev as [|ec lev]. simpl. apply nd_rule.
1008 unfold flatten_leveled_type at 4.
1009 unfold flatten_leveled_type at 2.
1011 replace (flatten_type (tx ---> te))
1012 with (flatten_type tx ---> flatten_type te).
1016 repeat drop_simplify.
1017 repeat take_simplify.
1018 rewrite mapOptionTree_distributes.
1019 set (mapOptionTree (flatten_leveled_type ) (drop_lev (ec :: lev) Σ₁)) as Σ₁'.
1020 set (mapOptionTree (flatten_leveled_type ) (drop_lev (ec :: lev) Σ₂)) as Σ₂'.
1021 set (take_lev (ec :: lev) Σ₁) as Σ₁''.
1022 set (take_lev (ec :: lev) Σ₂) as Σ₂''.
1023 replace (flatten_type (tx ---> te)) with ((flatten_type tx) ---> (flatten_type te)).
1024 apply (Prelude_error "FIXME: ga_apply").
1028 Notation "` x" := (take_lev _ x).
1029 Notation "`` x" := (mapOptionTree unlev x) (at level 20).
1030 Notation "``` x" := ((drop_lev _ x)) (at level 20).
1031 Notation "!<[]> x" := (flatten_type _ x) (at level 1).
1032 Notation "!<[@]> x" := (mapOptionTree flatten_leveled_type x) (at level 1).
1037 destruct lev as [|ec lev]; simpl; [ apply nd_rule; apply RLet; auto | idtac ].
1038 repeat drop_simplify.
1039 repeat take_simplify.
1043 eapply nd_prod; [ idtac | apply nd_id ].
1059 destruct case_RVoid.
1064 destruct case_RAppT.
1065 simpl. destruct lev; simpl.
1066 unfold flatten_leveled_type.
1068 rewrite flatten_commutes_with_HaskTAll.
1069 rewrite flatten_commutes_with_substT.
1074 apply (Prelude_error "found type application at level >0; this is not supported").
1076 destruct case_RAbsT.
1077 simpl. destruct lev; simpl.
1078 unfold flatten_leveled_type at 4.
1079 unfold flatten_leveled_type at 2.
1081 rewrite flatten_commutes_with_HaskTAll.
1082 rewrite flatten_commutes_with_HaskTApp.
1083 eapply nd_comp; [ idtac | eapply nd_rule; eapply RAbsT ].
1085 set (mapOptionTree (flatten_leveled_type ) (mapOptionTree (weakLT(κ:=κ)) Σ)) as a.
1086 set (mapOptionTree (weakLT(κ:=κ)) (mapOptionTree (flatten_leveled_type ) Σ)) as q'.
1094 rewrite flatten_commutes_with_weakLT.
1105 apply (Prelude_error "found type abstraction at level >0; this is not supported").
1107 destruct case_RAppCo.
1108 simpl. destruct lev; simpl.
1109 unfold flatten_leveled_type at 4.
1110 unfold flatten_leveled_type at 2.
1111 unfold flatten_type.
1115 apply flatten_coercion.
1117 apply (Prelude_error "found coercion application at level >0; this is not supported").
1119 destruct case_RAbsCo.
1120 simpl. destruct lev; simpl.
1121 unfold flatten_type.
1123 apply (Prelude_error "AbsCo not supported (FIXME)").
1124 apply (Prelude_error "found coercion abstraction at level >0; this is not supported").
1126 destruct case_RLetRec.
1129 apply (Prelude_error "LetRec not supported (FIXME)").
1131 destruct case_RCase.
1133 apply (Prelude_error "Case not supported (BIG FIXME)").
1135 destruct case_SBrak.
1139 set (drop_lev (ec :: nil) (take_arg_types_as_tree Γ t @@@ (ec :: nil))) as empty_tree.
1141 rewrite take_lemma'.
1143 rewrite mapOptionTree_compose.
1144 rewrite mapOptionTree_compose.
1145 rewrite unlev_relev.
1146 rewrite <- mapOptionTree_compose.
1147 unfold flatten_leveled_type at 4.
1150 set (mapOptionTree flatten_leveled_type (drop_lev (ec :: nil) succ)) as succ_host.
1151 set (mapOptionTree (flatten_type ○ unlev)(take_lev (ec :: nil) succ)) as succ_guest.
1152 set (mapOptionTree flatten_type (take_arg_types_as_tree Γ t)) as succ_args.
1154 eapply nd_comp; [ eapply nd_rule; eapply RArrange; apply tree_of_nothing | idtac ].
1155 refine (ga_unkappa' Γ Δ (v2t ec) nil _ _ _ _ ;; _).
1159 apply (Prelude_error "found Brak at depth >0 indicating 3-level code; only two-level code is currently supported").
1165 unfold flatten_leveled_type at 2.
1168 rewrite mapOptionTree_compose.
1172 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply tree_of_nothing' ].
1174 rewrite take_lemma'.
1175 rewrite unlev_relev.
1176 rewrite <- mapOptionTree_compose.
1177 eapply nd_comp; [ apply (arrange_esc _ _ ec) | idtac ].
1179 set (decide_tree_empty (take_lev (ec :: nil) succ)) as q'.
1185 set (mapOptionTree flatten_leveled_type (drop_lev (ec :: nil) succ)) as succ_host.
1186 set (mapOptionTree flatten_type (take_arg_types_as_tree Γ t)) as succ_args.
1188 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RCanR ].
1189 eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
1190 eapply nd_comp; [ apply nd_llecnac | idtac ].
1191 apply nd_prod; [ idtac | eapply boost ].
1194 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanR ].
1202 refine ( _ ;; (boost _ _ _ _ _ (postcompose _ _ _ _ _ _ _ _))).
1210 refine ( _ ;; (boost _ _ _ _ _ (postcompose _ _ _ _ _ _ _ _))).
1212 refine ( _ ;; (boost _ _ _ _ _ (postcompose _ _ _ _ _ _ _ _))).
1218 (* environment has non-empty leaves *)
1221 (* nesting too deep *)
1222 apply (Prelude_error "found Esc at depth >0 indicating 3-level code; only two-level code is currently supported").
1226 (* to do: establish some metric on judgments (max length of level of any succedent type, probably), show how to
1227 * calculate it, and show that the flattening procedure above drives it down by one *)
1230 Instance FlatteningFunctor {Γ}{Δ}{ec} : Functor (JudgmentsL (PCF Γ Δ ec)) (TypesL (SystemFCa Γ Δ)) (obact) :=
1231 { fmor := FlatteningFunctor_fmor }.
1233 Definition ReificationFunctor Γ Δ : Functor (JudgmentsL _ _ (PCF n Γ Δ)) SystemFCa' (mapOptionTree brakifyJudg).
1234 refine {| fmor := ReificationFunctor_fmor Γ Δ |}; unfold hom; unfold ob; simpl ; intros.
1236 Definition PCF_SMME (n:nat)(Γ:TypeEnv)(Δ:CoercionEnv Γ) : ProgrammingLanguageSMME.
1237 refine {| plsmme_pl := PCF n Γ Δ |}.
1240 Definition SystemFCa_SMME (n:nat)(Γ:TypeEnv)(Δ:CoercionEnv Γ) : ProgrammingLanguageSMME.
1241 refine {| plsmme_pl := SystemFCa n Γ Δ |}.
1244 Definition ReificationFunctorMonoidal n : MonoidalFunctor (JudgmentsN n) (JudgmentsN (S n)) (ReificationFunctor n).
1248 Definition PCF_SystemFCa_two_level n Γ Δ : TwoLevelLanguage (PCF_SMME n Γ Δ) (SystemFCa_SMME (S n) Γ Δ).
1251 (* ... and the retraction exists *)
1255 Implicit Arguments garrow [ ].