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 ★ :=
243 (ga_mk_tree' ec suc).
245 Definition ga_mk {Γ}(ec:HaskType Γ ECKind)(ant suc:Tree ??(HaskType Γ ★)) : HaskType Γ ★ :=
246 fun TV ite => gaTy TV (ec TV ite) (ga_mk_tree ec ant TV ite) (ga_mk_tree ec suc TV ite).
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 Axiom extensionality : forall Γ Q (f g:forall TV, InstantiatedTypeEnv TV Γ -> Q TV),
856 (forall tv ite, f tv ite = g tv ite) -> f=g.
858 Lemma krunk : forall Γ (ec:HaskTyVar Γ ECKind) t,
859 flatten_type (<[ ec |- t ]>)
861 (mapOptionTree flatten_type (take_arg_types_as_tree t))
862 [ flatten_type (drop_arg_types_as_tree t)].
864 unfold flatten_type at 1.
867 apply extensionality.
872 rewrite <- mapOptionTree_compose.
873 unfold take_arg_types_as_tree.
875 replace (flatten_type (drop_arg_types_as_tree t) tv ite)
876 with (drop_arg_types (flatten_rawtype (t tv ite))).
877 replace (unleaves (take_arg_types (flatten_rawtype (t tv ite))))
878 with ((mapOptionTree (fun x : HaskType Γ ★ => flatten_type x tv ite)
880 (take_trustme (count_arg_types (t (fun _ : Kind => unit) (ite_unit Γ)))
881 (fun TV : Kind → Type => take_arg_types ○ t TV))))).
884 clear hetmet_flatten.
885 clear hetmet_unflatten.
893 Definition flatten_proof :
896 ND Rule (mapOptionTree (flatten_judgment ) h) (mapOptionTree (flatten_judgment ) c).
898 eapply nd_map'; [ idtac | apply X ].
904 (match X as R in SRule H C with
905 | SBrak Γ Δ t ec succ lev => let case_SBrak := tt in _
906 | SEsc Γ Δ t ec succ lev => let case_SEsc := tt in _
907 | SFlat h c r => let case_SFlat := tt in _
911 refine (match r as R in Rule H C with
912 | RArrange Γ Δ a b x d => let case_RArrange := tt in _
913 | RNote Γ Δ Σ τ l n => let case_RNote := tt in _
914 | RLit Γ Δ l _ => let case_RLit := tt in _
915 | RVar Γ Δ σ lev => let case_RVar := tt in _
916 | RGlobal Γ Δ σ l wev => let case_RGlobal := tt in _
917 | RLam Γ Δ Σ tx te lev => let case_RLam := tt in _
918 | RCast Γ Δ Σ σ τ lev γ => let case_RCast := tt in _
919 | RAbsT Γ Δ Σ κ σ lev => let case_RAbsT := tt in _
920 | RAppT Γ Δ Σ κ σ τ lev => let case_RAppT := tt in _
921 | RAppCo Γ Δ Σ κ σ₁ σ₂ γ σ lev => let case_RAppCo := tt in _
922 | RAbsCo Γ Δ Σ κ σ σ₁ σ₂ lev => let case_RAbsCo := tt in _
923 | RApp Γ Δ Σ₁ Σ₂ tx te lev => let case_RApp := tt in _
924 | RLet Γ Δ Σ₁ Σ₂ σ₁ σ₂ lev => let case_RLet := tt in _
925 | RJoin Γ p lri m x q => let case_RJoin := tt in _
926 | RVoid _ _ => let case_RVoid := tt in _
927 | RBrak Γ Δ t ec succ lev => let case_RBrak := tt in _
928 | REsc Γ Δ t ec succ lev => let case_REsc := tt in _
929 | RCase Γ Δ lev tc Σ avars tbranches alts => let case_RCase := tt in _
930 | RLetRec Γ Δ lri x y t => let case_RLetRec := tt in _
933 destruct case_RArrange.
934 apply (flatten_arrangement'' Γ Δ a b x d).
937 apply (Prelude_error "found unskolemized Brak rule; this shouldn't happen").
940 apply (Prelude_error "found unskolemized Esc rule; this shouldn't happen").
945 apply nd_rule; apply RNote; auto.
946 apply nd_rule; apply RNote; auto.
951 unfold flatten_leveled_type.
953 rewrite literal_types_unchanged.
954 apply nd_rule; apply RLit.
955 unfold take_lev; simpl.
956 unfold drop_lev; simpl.
958 rewrite literal_types_unchanged.
962 Opaque flatten_judgment.
964 Transparent flatten_judgment.
966 unfold flatten_judgment.
969 apply nd_rule. apply RVar.
970 repeat drop_simplify.
971 repeat take_simplify.
975 destruct case_RGlobal.
979 destruct l as [|ec lev]; simpl.
980 destruct (eqd_dec (g:CoreVar) (hetmet_flatten:CoreVar)).
981 set (flatten_type (g wev)) as t.
982 set (RGlobal _ Δ nil (mkGlobal Γ t hetmet_id)) as q.
987 destruct (eqd_dec (g:CoreVar) (hetmet_unflatten:CoreVar)).
988 set (flatten_type (g wev)) as t.
989 set (RGlobal _ Δ nil (mkGlobal Γ t hetmet_id)) as q.
994 unfold flatten_leveled_type. simpl.
995 apply nd_rule; rewrite globals_do_not_have_code_types.
997 apply (Prelude_error "found RGlobal at depth >0; globals should never appear inside code brackets unless escaped").
1003 destruct lev as [|ec lev]; simpl; [ apply nd_rule; apply RLam; auto | idtac ].
1004 repeat drop_simplify.
1005 repeat take_simplify.
1015 destruct case_RCast.
1017 destruct lev as [|ec lev]; simpl; [ apply nd_rule; apply RCast; auto | idtac ].
1019 apply flatten_coercion; auto.
1020 apply (Prelude_error "RCast at level >0; casting inside of code brackets is currently not supported").
1022 destruct case_RJoin.
1024 destruct (getjlev x); destruct (getjlev q);
1025 [ apply nd_rule; apply RJoin | idtac | idtac | idtac ];
1026 apply (Prelude_error "RJoin at depth >0").
1031 destruct lev as [|ec lev]. simpl. apply nd_rule.
1032 unfold flatten_leveled_type at 4.
1033 unfold flatten_leveled_type at 2.
1035 replace (flatten_type (tx ---> te))
1036 with (flatten_type tx ---> flatten_type te).
1040 repeat drop_simplify.
1041 repeat take_simplify.
1042 rewrite mapOptionTree_distributes.
1043 set (mapOptionTree (flatten_leveled_type ) (drop_lev (ec :: lev) Σ₁)) as Σ₁'.
1044 set (mapOptionTree (flatten_leveled_type ) (drop_lev (ec :: lev) Σ₂)) as Σ₂'.
1045 set (take_lev (ec :: lev) Σ₁) as Σ₁''.
1046 set (take_lev (ec :: lev) Σ₂) as Σ₂''.
1047 replace (flatten_type (tx ---> te)) with ((flatten_type tx) ---> (flatten_type te)).
1048 apply (Prelude_error "FIXME: ga_apply").
1052 Notation "` x" := (take_lev _ x).
1053 Notation "`` x" := (mapOptionTree unlev x) (at level 20).
1054 Notation "``` x" := ((drop_lev _ x)) (at level 20).
1055 Notation "!<[]> x" := (flatten_type _ x) (at level 1).
1056 Notation "!<[@]> x" := (mapOptionTree flatten_leveled_type x) (at level 1).
1061 destruct lev as [|ec lev]; simpl; [ apply nd_rule; apply RLet; auto | idtac ].
1062 repeat drop_simplify.
1063 repeat take_simplify.
1067 eapply nd_prod; [ idtac | apply nd_id ].
1083 destruct case_RVoid.
1088 destruct case_RAppT.
1089 simpl. destruct lev; simpl.
1090 unfold flatten_leveled_type.
1092 rewrite flatten_commutes_with_HaskTAll.
1093 rewrite flatten_commutes_with_substT.
1098 apply (Prelude_error "found type application at level >0; this is not supported").
1100 destruct case_RAbsT.
1101 simpl. destruct lev; simpl.
1102 unfold flatten_leveled_type at 4.
1103 unfold flatten_leveled_type at 2.
1105 rewrite flatten_commutes_with_HaskTAll.
1106 rewrite flatten_commutes_with_HaskTApp.
1107 eapply nd_comp; [ idtac | eapply nd_rule; eapply RAbsT ].
1109 set (mapOptionTree (flatten_leveled_type ) (mapOptionTree (weakLT(κ:=κ)) Σ)) as a.
1110 set (mapOptionTree (weakLT(κ:=κ)) (mapOptionTree (flatten_leveled_type ) Σ)) as q'.
1118 rewrite flatten_commutes_with_weakLT.
1129 apply (Prelude_error "found type abstraction at level >0; this is not supported").
1131 destruct case_RAppCo.
1132 simpl. destruct lev; simpl.
1133 unfold flatten_leveled_type at 4.
1134 unfold flatten_leveled_type at 2.
1135 unfold flatten_type.
1139 apply flatten_coercion.
1141 apply (Prelude_error "found coercion application at level >0; this is not supported").
1143 destruct case_RAbsCo.
1144 simpl. destruct lev; simpl.
1145 unfold flatten_type.
1147 apply (Prelude_error "AbsCo not supported (FIXME)").
1148 apply (Prelude_error "found coercion abstraction at level >0; this is not supported").
1150 destruct case_RLetRec.
1153 apply (Prelude_error "LetRec not supported (FIXME)").
1155 destruct case_RCase.
1157 apply (Prelude_error "Case not supported (BIG FIXME)").
1159 destruct case_SBrak.
1163 set (drop_lev (ec :: nil) (take_arg_types_as_tree t @@@ (ec :: nil))) as empty_tree.
1165 rewrite take_lemma'.
1167 rewrite mapOptionTree_compose.
1168 rewrite mapOptionTree_compose.
1169 rewrite unlev_relev.
1170 rewrite <- mapOptionTree_compose.
1171 unfold flatten_leveled_type at 4.
1174 set (mapOptionTree flatten_leveled_type (drop_lev (ec :: nil) succ)) as succ_host.
1175 set (mapOptionTree (flatten_type ○ unlev)(take_lev (ec :: nil) succ)) as succ_guest.
1176 set (mapOptionTree flatten_type (take_arg_types_as_tree t)) as succ_args.
1178 eapply nd_comp; [ eapply nd_rule; eapply RArrange; apply tree_of_nothing | idtac ].
1179 refine (ga_unkappa' Γ Δ (v2t ec) nil _ _ _ _ ;; _).
1183 apply (Prelude_error "found Brak at depth >0 indicating 3-level code; only two-level code is currently supported").
1189 unfold flatten_leveled_type at 2.
1192 rewrite mapOptionTree_compose.
1196 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply tree_of_nothing' ].
1198 rewrite take_lemma'.
1199 rewrite unlev_relev.
1200 rewrite <- mapOptionTree_compose.
1201 eapply nd_comp; [ apply (arrange_esc _ _ ec) | idtac ].
1203 set (decide_tree_empty (take_lev (ec :: nil) succ)) as q'.
1209 set (mapOptionTree flatten_leveled_type (drop_lev (ec :: nil) succ)) as succ_host.
1210 set (mapOptionTree flatten_type (take_arg_types_as_tree t)) as succ_args.
1212 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RCanR ].
1213 eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
1214 eapply nd_comp; [ apply nd_llecnac | idtac ].
1215 apply nd_prod; [ idtac | eapply boost ].
1218 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanR ].
1226 refine ( _ ;; (boost _ _ _ _ _ (postcompose _ _ _ _ _ _ _ _))).
1234 refine ( _ ;; (boost _ _ _ _ _ (postcompose _ _ _ _ _ _ _ _))).
1236 refine ( _ ;; (boost _ _ _ _ _ (postcompose _ _ _ _ _ _ _ _))).
1242 (* environment has non-empty leaves *)
1245 (* nesting too deep *)
1246 apply (Prelude_error "found Esc at depth >0 indicating 3-level code; only two-level code is currently supported").
1249 Definition skolemize_and_flatten_proof :
1253 (mapOptionTree (flatten_judgment ○ skolemize_judgment) h)
1254 (mapOptionTree (flatten_judgment ○ skolemize_judgment) c).
1256 rewrite mapOptionTree_compose.
1257 rewrite mapOptionTree_compose.
1258 apply flatten_proof.
1259 apply skolemize_proof.
1264 (* to do: establish some metric on judgments (max length of level of any succedent type, probably), show how to
1265 * calculate it, and show that the flattening procedure above drives it down by one *)
1268 Instance FlatteningFunctor {Γ}{Δ}{ec} : Functor (JudgmentsL (PCF Γ Δ ec)) (TypesL (SystemFCa Γ Δ)) (obact) :=
1269 { fmor := FlatteningFunctor_fmor }.
1271 Definition ReificationFunctor Γ Δ : Functor (JudgmentsL _ _ (PCF n Γ Δ)) SystemFCa' (mapOptionTree brakifyJudg).
1272 refine {| fmor := ReificationFunctor_fmor Γ Δ |}; unfold hom; unfold ob; simpl ; intros.
1274 Definition PCF_SMME (n:nat)(Γ:TypeEnv)(Δ:CoercionEnv Γ) : ProgrammingLanguageSMME.
1275 refine {| plsmme_pl := PCF n Γ Δ |}.
1278 Definition SystemFCa_SMME (n:nat)(Γ:TypeEnv)(Δ:CoercionEnv Γ) : ProgrammingLanguageSMME.
1279 refine {| plsmme_pl := SystemFCa n Γ Δ |}.
1282 Definition ReificationFunctorMonoidal n : MonoidalFunctor (JudgmentsN n) (JudgmentsN (S n)) (ReificationFunctor n).
1286 Definition PCF_SystemFCa_two_level n Γ Δ : TwoLevelLanguage (PCF_SMME n Γ Δ) (SystemFCa_SMME (S n) Γ Δ).
1289 (* ... and the retraction exists *)
1293 Implicit Arguments garrow [ ].