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 NaturalDeductionContext.
13 Require Import Coq.Strings.String.
14 Require Import Coq.Lists.List.
16 Require Import HaskKinds.
17 Require Import HaskCoreTypes.
18 Require Import HaskCoreVars.
19 Require Import HaskWeakTypes.
20 Require Import HaskWeakVars.
21 Require Import HaskLiterals.
22 Require Import HaskTyCons.
23 Require Import HaskStrongTypes.
24 Require Import HaskProof.
25 Require Import NaturalDeduction.
27 Require Import HaskStrongTypes.
28 Require Import HaskStrong.
29 Require Import HaskProof.
30 Require Import HaskStrongToProof.
31 Require Import HaskProofToStrong.
32 Require Import HaskWeakToStrong.
34 Require Import HaskSkolemizer.
37 Set Printing Width 130.
40 * The flattening transformation. Currently only TWO-level languages are
41 * supported, and the level-1 sublanguage is rather limited.
43 * This file abuses terminology pretty badly. For purposes of this file,
44 * "PCF" means "the level-1 sublanguage" and "FC" (aka System FC) means
45 * the whole language (level-0 language including bracketed level-1 terms)
47 Section HaskFlattener.
51 | [ |- context[@eqd_dec ?T ?V ?X ?X] ] =>
52 destruct (@eqd_dec T V X X) as [eqd_dec1 | eqd_dec2];
53 [ clear eqd_dec1 | set (eqd_dec2 (refl_equal _)) as eqd_dec2'; inversion eqd_dec2' ]
56 Definition v2t {Γ}(ec:HaskTyVar Γ ECKind) : HaskType Γ ECKind := fun TV ite => TVar (ec TV ite).
58 Definition levelMatch {Γ}(lev:HaskLevel Γ) : LeveledHaskType Γ ★ -> bool :=
59 fun t => match t with ttype@@tlev => if eqd_dec tlev lev then true else false end.
61 (* In a tree of types, replace any type at depth "lev" or greater None *)
62 Definition mkDropFlags {Γ}(lev:HaskLevel Γ)(tt:Tree ??(LeveledHaskType Γ ★)) : TreeFlags tt :=
63 mkFlags (liftBoolFunc false (levelMatch lev)) tt.
65 Definition drop_lev {Γ}(lev:HaskLevel Γ)(tt:Tree ??(LeveledHaskType Γ ★)) : Tree ??(LeveledHaskType Γ ★) :=
66 dropT (mkDropFlags lev tt).
68 (* The opposite: replace any type which is NOT at level "lev" with None *)
69 Definition mkTakeFlags {Γ}(lev:HaskLevel Γ)(tt:Tree ??(LeveledHaskType Γ ★)) : TreeFlags tt :=
70 mkFlags (liftBoolFunc true (bnot ○ levelMatch lev)) tt.
72 Definition take_lev {Γ}(lev:HaskLevel Γ)(tt:Tree ??(LeveledHaskType Γ ★)) : Tree ??(LeveledHaskType Γ ★) :=
73 dropT (mkTakeFlags lev tt).
75 mapOptionTree (fun x => flatten_type (unlev x))
76 (maybeTree (takeT tt (mkFlags (
78 | Some (ttype @@ tlev) => if eqd_dec tlev lev then true else false
83 Definition maybeTree {T}(t:??(Tree ??T)) : Tree ??T :=
90 Lemma drop_lev_lemma : forall Γ (lev:HaskLevel Γ) x, drop_lev lev [x @@ lev] = [].
102 Lemma drop_lev_lemma_s : forall Γ (lev:HaskLevel Γ) ec x, drop_lev (ec::lev) [x @@ (ec :: lev)] = [].
113 Lemma take_lemma : forall Γ (lev:HaskLevel Γ) x, take_lev lev [x @@ lev] = [x @@ lev].
124 Lemma take_lemma' : forall Γ (lev:HaskLevel Γ) x, take_lev lev (x @@@ lev) = x @@@ lev.
127 destruct a; simpl; try reflexivity.
130 rewrite <- IHx1 at 2.
131 rewrite <- IHx2 at 2.
135 Ltac drop_simplify :=
137 | [ |- context[@drop_lev ?G ?L [ ?X @@ ?L ] ] ] =>
138 rewrite (drop_lev_lemma G L X)
139 | [ |- context[@drop_lev ?G (?E :: ?L) [ ?X @@ (?E :: ?L) ] ] ] =>
140 rewrite (drop_lev_lemma_s G L E X)
141 | [ |- context[@drop_lev ?G ?N (?A,,?B)] ] =>
142 change (@drop_lev G N (A,,B)) with ((@drop_lev G N A),,(@drop_lev G N B))
143 | [ |- context[@drop_lev ?G ?N (T_Leaf None)] ] =>
144 change (@drop_lev G N (T_Leaf (@None (LeveledHaskType G ★)))) with (T_Leaf (@None (LeveledHaskType G ★)))
147 Ltac take_simplify :=
149 | [ |- context[@take_lev ?G ?L [ ?X @@ ?L ] ] ] =>
150 rewrite (take_lemma G L X)
151 | [ |- context[@take_lev ?G ?L [ ?X @@@ ?L ] ] ] =>
152 rewrite (take_lemma' G L X)
153 | [ |- context[@take_lev ?G ?N (?A,,?B)] ] =>
154 change (@take_lev G N (A,,B)) with ((@take_lev G N A),,(@take_lev G N B))
155 | [ |- context[@take_lev ?G ?N (T_Leaf None)] ] =>
156 change (@take_lev G N (T_Leaf (@None (LeveledHaskType G ★)))) with (T_Leaf (@None (LeveledHaskType G ★)))
160 (*******************************************************************************)
163 Context {unitTy : forall TV, RawHaskType TV ECKind -> RawHaskType TV ★ }.
164 Context {prodTy : forall TV, RawHaskType TV ECKind -> RawHaskType TV ★ -> RawHaskType TV ★ -> RawHaskType TV ★ }.
165 Context {gaTy : forall TV, RawHaskType TV ECKind -> RawHaskType TV ★ -> RawHaskType TV ★ -> RawHaskType TV ★ }.
167 Definition ga_mk_tree' {TV}(ec:RawHaskType TV ECKind)(tr:Tree ??(RawHaskType TV ★)) : RawHaskType TV ★ :=
168 reduceTree (unitTy TV ec) (prodTy TV ec) tr.
170 Definition ga_mk_tree {Γ}(ec:HaskType Γ ECKind)(tr:Tree ??(HaskType Γ ★)) : HaskType Γ ★ :=
171 fun TV ite => ga_mk_tree' (ec TV ite) (mapOptionTree (fun x => x TV ite) tr).
173 Definition ga_mk_raw {TV}(ec:RawHaskType TV ECKind)(ant suc:Tree ??(RawHaskType TV ★)) : RawHaskType TV ★ :=
176 (ga_mk_tree' ec suc).
178 Definition ga_mk {Γ}(ec:HaskType Γ ECKind)(ant suc:Tree ??(HaskType Γ ★)) : HaskType Γ ★ :=
179 fun TV ite => gaTy TV (ec TV ite) (ga_mk_tree ec ant TV ite) (ga_mk_tree ec suc TV ite).
183 * - code types <[t]>@c become garrows c () t
184 * - free variables of type t at a level lev deeper than the succedent become garrows c () t
185 * - free variables at the level of the succedent become
187 Fixpoint flatten_rawtype {TV}{κ}(exp: RawHaskType TV κ) : RawHaskType TV κ :=
190 | TAll _ y => TAll _ (fun v => flatten_rawtype (y v))
191 | TApp _ _ x y => TApp (flatten_rawtype x) (flatten_rawtype y)
193 | TCoerc _ t1 t2 t => TCoerc (flatten_rawtype t1) (flatten_rawtype t2) (flatten_rawtype t)
195 | TCode ec e => let e' := flatten_rawtype e
196 in ga_mk_raw ec (unleaves_ (take_arg_types e')) [drop_arg_types e']
197 | TyFunApp tfc kl k lt => TyFunApp tfc kl k (flatten_rawtype_list _ lt)
199 with flatten_rawtype_list {TV}(lk:list Kind)(exp:@RawHaskTypeList TV lk) : @RawHaskTypeList TV lk :=
200 match exp in @RawHaskTypeList _ LK return @RawHaskTypeList TV LK with
201 | TyFunApp_nil => TyFunApp_nil
202 | TyFunApp_cons κ kl t rest => TyFunApp_cons _ _ (flatten_rawtype t) (flatten_rawtype_list _ rest)
205 Definition flatten_type {Γ}{κ}(ht:HaskType Γ κ) : HaskType Γ κ :=
206 fun TV ite => flatten_rawtype (ht TV ite).
208 Fixpoint levels_to_tcode {Γ}(ht:HaskType Γ ★)(lev:HaskLevel Γ) : HaskType Γ ★ :=
210 | nil => flatten_type ht
211 | ec::lev' => @ga_mk _ (v2t ec) [] [levels_to_tcode ht lev']
214 Definition flatten_leveled_type {Γ}(ht:LeveledHaskType Γ ★) : LeveledHaskType Γ ★ :=
215 levels_to_tcode (unlev ht) (getlev ht) @@ nil.
219 Axiom literal_types_unchanged : forall Γ l, flatten_type (literalType l) = literalType(Γ:=Γ) l.
221 Axiom flatten_coercion : forall Γ Δ κ (σ τ:HaskType Γ κ) (γ:HaskCoercion Γ Δ (σ ∼∼∼ τ)),
222 HaskCoercion Γ Δ (flatten_type σ ∼∼∼ flatten_type τ).
224 Axiom flatten_commutes_with_substT :
225 forall κ Γ (Δ:CoercionEnv Γ) (σ:∀ TV, InstantiatedTypeEnv TV Γ → TV κ → RawHaskType TV ★) (τ:HaskType Γ κ),
226 flatten_type (substT σ τ) = substT (fun TV ite v => flatten_rawtype (σ TV ite v))
229 Axiom flatten_commutes_with_HaskTAll :
230 forall κ Γ (Δ:CoercionEnv Γ) (σ:∀ TV, InstantiatedTypeEnv TV Γ → TV κ → RawHaskType TV ★),
231 flatten_type (HaskTAll κ σ) = HaskTAll κ (fun TV ite v => flatten_rawtype (σ TV ite v)).
233 Axiom flatten_commutes_with_HaskTApp :
234 forall n κ Γ (Δ:CoercionEnv Γ) (σ:∀ TV, InstantiatedTypeEnv TV Γ → TV κ → RawHaskType TV ★),
235 flatten_type (HaskTApp (weakF_ σ) (FreshHaskTyVar_ κ)) =
236 HaskTApp (weakF_ (fun TV ite v => flatten_rawtype (σ TV ite v))) (FreshHaskTyVar_(n:=n) κ).
238 Axiom flatten_commutes_with_weakLT : forall n (Γ:TypeEnv) κ t,
239 flatten_leveled_type (weakLT_(n:=n)(Γ:=Γ)(κ:=κ) t) = weakLT_(n:=n)(Γ:=Γ)(κ:=κ) (flatten_leveled_type t).
241 Axiom globals_do_not_have_code_types : forall (Γ:TypeEnv) (g:Global Γ) v,
242 flatten_type (g v) = g v.
244 (* "n" is the maximum depth remaining AFTER flattening *)
245 Definition flatten_judgment (j:Judg) :=
246 match j as J return Judg with
247 | Γ > Δ > ant |- suc @ nil => Γ > Δ > mapOptionTree flatten_leveled_type ant
248 |- mapOptionTree flatten_type suc @ nil
249 | Γ > Δ > ant |- suc @ (ec::lev') => Γ > Δ > mapOptionTree flatten_leveled_type (drop_lev (ec::lev') ant)
251 (mapOptionTree (flatten_type ○ unlev) (take_lev (ec::lev') ant))
252 (mapOptionTree flatten_type suc )
257 { ga_id : ∀ Γ Δ ec l a , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec a a ]@l ]
258 ; ga_cancelr : ∀ Γ Δ ec l a , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec (a,,[]) a ]@l ]
259 ; ga_cancell : ∀ Γ Δ ec l a , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec ([],,a) a ]@l ]
260 ; ga_uncancelr : ∀ Γ Δ ec l a , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec a (a,,[]) ]@l ]
261 ; ga_uncancell : ∀ Γ Δ ec l a , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec a ([],,a) ]@l ]
262 ; ga_assoc : ∀ Γ Δ ec l a b c, ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec ((a,,b),,c) (a,,(b,,c)) ]@l ]
263 ; ga_unassoc : ∀ Γ Δ ec l a b c, ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec (a,,(b,,c)) ((a,,b),,c) ]@l ]
264 ; ga_swap : ∀ Γ Δ ec l a b , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec (a,,b) (b,,a) ]@l ]
265 ; ga_drop : ∀ Γ Δ ec l a , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec a [] ]@l ]
266 ; ga_copy : ∀ Γ Δ ec l a , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec a (a,,a) ]@l ]
267 ; ga_first : ∀ Γ Δ ec l a b x, ND Rule [] [Γ > Δ > [@ga_mk Γ ec a b @@l] |- [@ga_mk Γ ec (a,,x) (b,,x) ]@l ]
268 ; ga_second : ∀ Γ Δ ec l a b x, ND Rule [] [Γ > Δ > [@ga_mk Γ ec a b @@l] |- [@ga_mk Γ ec (x,,a) (x,,b) ]@l ]
269 ; ga_lit : ∀ Γ Δ ec l lit , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec [] [literalType lit] ]@l ]
270 ; ga_curry : ∀ Γ Δ ec l a b c, ND Rule [] [Γ > Δ > [@ga_mk Γ ec (a,,[b]) [c] @@ l] |- [@ga_mk Γ ec a [b ---> c] ]@ l ]
271 ; ga_loopl : ∀ Γ Δ ec l x y z, ND Rule [] [Γ > Δ > [@ga_mk Γ ec (z,,x) (z,,y) @@ l] |- [@ga_mk Γ ec x y ]@ l ]
272 ; ga_loopr : ∀ Γ Δ ec l x y z, ND Rule [] [Γ > Δ > [@ga_mk Γ ec (x,,z) (y,,z) @@ l] |- [@ga_mk Γ ec x y ]@ l ]
273 ; 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 ]
274 ; ga_apply : ∀ Γ Δ ec l a a' b c,
275 ND Rule [] [Γ > Δ > [@ga_mk Γ ec a [b ---> c] @@ l],,[@ga_mk Γ ec a' [b] @@ l] |- [@ga_mk Γ ec (a,,a') [c] ]@l ]
276 ; ga_kappa : ∀ Γ Δ ec l a b c Σ, ND Rule
277 [Γ > Δ > Σ,,[@ga_mk Γ ec [] a @@ l] |- [@ga_mk Γ ec b c ]@l ]
278 [Γ > Δ > Σ |- [@ga_mk Γ ec (a,,b) c ]@l ]
280 Context `(gar:garrow).
282 Notation "a ~~~~> b" := (@ga_mk _ _ a b) (at level 20).
284 Definition boost : forall Γ Δ ant x y {lev},
285 ND Rule [] [ Γ > Δ > [x@@lev] |- [y]@lev ] ->
286 ND Rule [ Γ > Δ > ant |- [x]@lev ] [ Γ > Δ > ant |- [y]@lev ].
288 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ACanR ].
289 eapply nd_comp; [ idtac | apply RLet ].
290 eapply nd_comp; [ apply nd_rlecnac | idtac ].
300 Definition precompose Γ Δ ec : forall a x y z lev,
302 [ Γ > Δ > a |- [@ga_mk _ ec y z ]@lev ]
303 [ Γ > Δ > a,,[@ga_mk _ ec x y @@ lev] |- [@ga_mk _ ec x z ]@lev ].
305 eapply nd_comp; [ idtac | eapply RLet ].
306 eapply nd_comp; [ apply nd_rlecnac | idtac ].
309 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AExch ].
313 Definition precompose' Γ Δ ec : forall a b x y z lev,
315 [ Γ > Δ > a,,b |- [@ga_mk _ ec y z ]@lev ]
316 [ Γ > Δ > a,,([@ga_mk _ ec x y @@ lev],,b) |- [@ga_mk _ ec x z ]@lev ].
318 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ALeft; eapply AExch ].
319 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AuAssoc ].
323 Definition postcompose_ Γ Δ ec : forall a x y z lev,
325 [ Γ > Δ > a |- [@ga_mk _ ec x y ]@lev ]
326 [ Γ > Δ > a,,[@ga_mk _ ec y z @@ lev] |- [@ga_mk _ ec x z ]@lev ].
328 eapply nd_comp; [ idtac | eapply RLet ].
329 eapply nd_comp; [ apply nd_rlecnac | idtac ].
335 Definition postcompose Γ Δ ec : forall x y z lev,
336 ND Rule [] [ Γ > Δ > [] |- [@ga_mk _ ec x y ]@lev ] ->
337 ND Rule [] [ Γ > Δ > [@ga_mk _ ec y z @@ lev] |- [@ga_mk _ ec x z ]@lev ].
339 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ACanL ].
340 eapply nd_comp; [ idtac | eapply postcompose_ ].
344 Definition first_nd : ∀ Γ Δ ec lev a b c Σ,
345 ND Rule [ Γ > Δ > Σ |- [@ga_mk Γ ec a b ]@lev ]
346 [ Γ > Δ > Σ |- [@ga_mk Γ ec (a,,c) (b,,c) ]@lev ].
348 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ACanR ].
349 eapply nd_comp; [ idtac | apply RLet ].
350 eapply nd_comp; [ apply nd_rlecnac | idtac ].
353 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AuCanR ].
357 Definition firstify : ∀ Γ Δ ec lev a b c Σ,
358 ND Rule [] [ Γ > Δ > Σ |- [@ga_mk Γ ec a b ]@lev ] ->
359 ND Rule [] [ Γ > Δ > Σ |- [@ga_mk Γ ec (a,,c) (b,,c) ]@lev ].
366 Definition second_nd : ∀ Γ Δ ec lev a b c Σ,
368 [ Γ > Δ > Σ |- [@ga_mk Γ ec a b ]@lev ]
369 [ Γ > Δ > Σ |- [@ga_mk Γ ec (c,,a) (c,,b) ]@lev ].
371 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ACanR ].
372 eapply nd_comp; [ idtac | apply RLet ].
373 eapply nd_comp; [ apply nd_rlecnac | idtac ].
376 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AuCanR ].
380 Definition secondify : ∀ Γ Δ ec lev a b c Σ,
381 ND Rule [] [ Γ > Δ > Σ |- [@ga_mk Γ ec a b ]@lev ] ->
382 ND Rule [] [ Γ > Δ > Σ |- [@ga_mk Γ ec (c,,a) (c,,b) ]@lev ].
389 Lemma ga_unkappa : ∀ Γ Δ ec l a b Σ x,
391 [Γ > Δ > Σ |- [@ga_mk Γ ec (a,,x) b ]@l ]
392 [Γ > Δ > Σ,,[@ga_mk Γ ec [] a @@ l] |- [@ga_mk Γ ec x b ]@l ].
394 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AExch ].
395 eapply nd_comp; [ idtac | eapply RLet ].
396 eapply nd_comp; [ apply nd_llecnac | idtac ].
400 eapply nd_comp; [ idtac | eapply RLet ].
401 eapply nd_comp; [ apply nd_llecnac | idtac ].
405 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AExch ].
412 (* useful for cutting down on the pretty-printed noise
414 Notation "` x" := (take_lev _ x) (at level 20).
415 Notation "`` x" := (mapOptionTree unlev x) (at level 20).
416 Notation "``` x" := (drop_lev _ x) (at level 20).
418 Definition flatten_arrangement' :
419 forall Γ (Δ:CoercionEnv Γ)
420 (ec:HaskTyVar Γ ECKind) (lev:HaskLevel Γ) (ant1 ant2:Tree ??(LeveledHaskType Γ ★)) (r:Arrange ant1 ant2),
421 ND Rule [] [Γ > Δ > [] |- [@ga_mk _ (v2t ec) (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) ant2))
422 (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) ant1)) ]@nil ].
425 refine (fix flatten ant1 ant2 (r:Arrange ant1 ant2):
426 ND Rule [] [Γ > Δ > [] |- [@ga_mk _ (v2t ec)
427 (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) ant2))
428 (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) ant1)) ]@nil] :=
429 match r as R in Arrange A B return
430 ND Rule [] [Γ > Δ > [] |- [@ga_mk _ (v2t ec)
431 (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) B))
432 (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) A)) ]@nil]
434 | AId a => let case_AId := tt in ga_id _ _ _ _ _
435 | ACanL a => let case_ACanL := tt in ga_uncancell _ _ _ _ _
436 | ACanR a => let case_ACanR := tt in ga_uncancelr _ _ _ _ _
437 | AuCanL a => let case_AuCanL := tt in ga_cancell _ _ _ _ _
438 | AuCanR a => let case_AuCanR := tt in ga_cancelr _ _ _ _ _
439 | AAssoc a b c => let case_AAssoc := tt in ga_assoc _ _ _ _ _ _ _
440 | AuAssoc a b c => let case_AuAssoc := tt in ga_unassoc _ _ _ _ _ _ _
441 | AExch a b => let case_AExch := tt in ga_swap _ _ _ _ _ _
442 | AWeak a => let case_AWeak := tt in ga_drop _ _ _ _ _
443 | ACont a => let case_ACont := tt in ga_copy _ _ _ _ _
444 | ALeft a b c r' => let case_ALeft := tt in flatten _ _ r' ;; boost _ _ _ _ _ (ga_second _ _ _ _ _ _ _)
445 | ARight a b c r' => let case_ARight := tt in flatten _ _ r' ;; boost _ _ _ _ _ (ga_first _ _ _ _ _ _ _)
446 | AComp c b a r1 r2 => let case_AComp := tt in (fun r1' r2' => _) (flatten _ _ r1) (flatten _ _ r2)
447 end); clear flatten; repeat take_simplify; repeat drop_simplify; intros.
450 set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) a)) as a' in *.
451 set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) b)) as b' in *.
452 set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) c)) as c' in *.
453 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply ACanL ].
454 eapply nd_comp; [ idtac | apply
455 (@RLet Γ Δ [] [] (@ga_mk _ (v2t ec) a' b') (@ga_mk _ (v2t ec) a' c')) ].
456 eapply nd_comp; [ apply nd_llecnac | idtac ].
459 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply AuCanR ].
460 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply ACanL ].
461 eapply nd_comp; [ idtac | apply RLet ].
462 eapply nd_comp; [ apply nd_llecnac | idtac ].
465 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AExch ].
469 Definition flatten_arrangement :
470 forall Γ (Δ:CoercionEnv Γ) n
471 (ec:HaskTyVar Γ ECKind) (lev:HaskLevel Γ) (ant1 ant2:Tree ??(LeveledHaskType Γ ★)) (r:Arrange ant1 ant2) succ,
473 [Γ > Δ > mapOptionTree (flatten_leveled_type ) (drop_lev n ant1)
474 |- [@ga_mk _ (v2t ec)
475 (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) ant1))
476 (mapOptionTree (flatten_type ) succ) ]@nil]
477 [Γ > Δ > mapOptionTree (flatten_leveled_type ) (drop_lev n ant2)
478 |- [@ga_mk _ (v2t ec)
479 (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) ant2))
480 (mapOptionTree (flatten_type ) succ) ]@nil].
482 refine ( _ ;; (boost _ _ _ _ _ (postcompose _ _ _ _ _ _ _ (flatten_arrangement' Γ Δ ec lev ant1 ant2 r)))).
485 refine ((fix flatten ant1 ant2 (r:Arrange ant1 ant2) :=
486 match r as R in Arrange A B return
487 Arrange (mapOptionTree (flatten_leveled_type ) (drop_lev _ A))
488 (mapOptionTree (flatten_leveled_type ) (drop_lev _ B)) with
489 | AId a => let case_AId := tt in AId _
490 | ACanL a => let case_ACanL := tt in ACanL _
491 | ACanR a => let case_ACanR := tt in ACanR _
492 | AuCanL a => let case_AuCanL := tt in AuCanL _
493 | AuCanR a => let case_AuCanR := tt in AuCanR _
494 | AAssoc a b c => let case_AAssoc := tt in AAssoc _ _ _
495 | AuAssoc a b c => let case_AuAssoc := tt in AuAssoc _ _ _
496 | AExch a b => let case_AExch := tt in AExch _ _
497 | AWeak a => let case_AWeak := tt in AWeak _
498 | ACont a => let case_ACont := tt in ACont _
499 | ALeft a b c r' => let case_ALeft := tt in ALeft _ (flatten _ _ r')
500 | ARight a b c r' => let case_ARight := tt in ARight _ (flatten _ _ r')
501 | AComp a b c r1 r2 => let case_AComp := tt in AComp (flatten _ _ r1) (flatten _ _ r2)
502 end) ant1 ant2 r); clear flatten; repeat take_simplify; repeat drop_simplify; intros.
505 Definition flatten_arrangement'' :
506 forall Γ Δ ant1 ant2 succ l (r:Arrange ant1 ant2),
507 ND Rule (mapOptionTree (flatten_judgment ) [Γ > Δ > ant1 |- succ @ l])
508 (mapOptionTree (flatten_judgment ) [Γ > Δ > ant2 |- succ @ l]).
522 apply AExch. (* TO DO: check for all-leaf trees here *)
527 eapply AComp; [ apply IHr1 | apply IHr2 ].
529 apply flatten_arrangement.
533 Definition ga_join Γ Δ Σ₁ Σ₂ a b ec :
534 ND Rule [] [Γ > Δ > Σ₁ |- [@ga_mk _ ec [] a ]@nil] ->
535 ND Rule [] [Γ > Δ > Σ₂ |- [@ga_mk _ ec [] b ]@nil] ->
536 ND Rule [] [Γ > Δ > Σ₁,,Σ₂ |- [@ga_mk _ ec [] (a,,b) ]@nil].
539 apply secondify with (c:=a) in pfb.
540 apply firstify with (c:=[]) in pfa.
541 eapply nd_comp; [ idtac | eapply RLet ].
542 eapply nd_comp; [ eapply nd_llecnac | idtac ].
547 eapply nd_comp; [ idtac | eapply RLet ].
548 eapply nd_comp; [ apply nd_llecnac | idtac ].
550 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ACanL ].
551 eapply nd_comp; [ idtac | eapply postcompose_ ].
554 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AExch ].
555 eapply nd_comp; [ idtac | eapply precompose ].
559 Definition arrange_brak : forall Γ Δ ec succ t,
562 [(@ga_mk _ (v2t ec) [] (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: nil) succ))) @@ nil],,
563 mapOptionTree (flatten_leveled_type ) (drop_lev (ec :: nil) succ) |- [t]@nil]
564 [Γ > Δ > mapOptionTree (flatten_leveled_type ) succ |- [t]@nil].
568 set (@arrangeUnPartition _ succ (levelMatch (ec::nil))) as q.
569 set (arrangeMap _ _ flatten_leveled_type q) as y.
577 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AExch ].
579 eapply nd_comp; [ apply nd_llecnac | idtac ].
580 eapply nd_comp; [ idtac | eapply RLet ].
585 induction succ; try destruct a; simpl.
591 destruct l as [t' lev'].
592 destruct lev' as [|ec' lev'].
596 set (@eqd_dec (HaskLevel Γ) (haskLevelEqDecidable Γ) (ec' :: lev') (ec :: nil)) as q.
601 unfold flatten_leveled_type.
618 Definition arrange_esc : forall Γ Δ ec succ t,
620 [Γ > Δ > mapOptionTree (flatten_leveled_type ) succ |- [t]@nil]
622 [(@ga_mk _ (v2t ec) [] (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: nil) succ))) @@ nil],,
623 mapOptionTree (flatten_leveled_type ) (drop_lev (ec :: nil) succ) |- [t]@nil].
625 set (@arrangePartition _ succ (levelMatch (ec::nil))) as q.
626 set (@drop_lev Γ (ec::nil) succ) as q'.
627 assert (@drop_lev Γ (ec::nil) succ=q') as H.
629 unfold drop_lev in H.
630 unfold mkDropFlags in H.
633 set (arrangeMap _ _ flatten_leveled_type q) as y.
640 set (mapOptionTree flatten_leveled_type (dropT (mkFlags (liftBoolFunc false (bnot ○ levelMatch (ec :: nil))) succ))) as q.
641 destruct (decide_tree_empty q).
645 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply AExch ].
646 set (fun z z' => @RLet Γ Δ z (mapOptionTree flatten_leveled_type q') t z' nil) as q''.
647 eapply nd_comp; [ idtac | apply RLet ].
649 eapply nd_comp; [ apply nd_rlecnac | idtac ].
653 eapply AComp; [ idtac | apply ACanR ].
655 apply (@arrangeCancelEmptyTree _ _ _ _ e).
659 eapply (@RVar Γ Δ t nil).
675 destruct l as [t' l'].
677 Transparent drop_lev.
686 unfold flatten_leveled_type.
687 destruct (General.list_eq_dec l' (ec :: nil)); simpl.
689 unfold levels_to_tcode.
706 set (mapOptionTree flatten_leveled_type (drop_lev (ec :: nil) succ2)) as d2 in *.
707 set (mapOptionTree flatten_leveled_type (drop_lev (ec :: nil) succ1)) as d1 in *.
708 set (mapOptionTree flatten_leveled_type (dropT (mkFlags
709 (liftBoolFunc false (bnot ○ levelMatch (ec :: nil))) succ1))) as s1 in *.
710 set (mapOptionTree flatten_leveled_type (dropT (mkFlags
711 (liftBoolFunc false (bnot ○ levelMatch (ec :: nil))) succ2))) as s2 in *.
712 set (mapOptionTree (flatten_type ○ unlev) (dropT (mkFlags
713 (liftBoolFunc true (bnot ○ levelMatch (ec :: nil))) succ1))) as s1' in *.
714 set (mapOptionTree (flatten_type ○ unlev) (dropT (mkFlags
715 (liftBoolFunc true (bnot ○ levelMatch (ec :: nil))) succ2))) as s2' in *.
718 apply arrangeSwapMiddle.
729 apply arrangeSwapMiddle.
737 set (mapOptionTree (flatten_type ○ unlev) (dropT (mkFlags
738 (liftBoolFunc true (bnot ○ levelMatch (ec :: nil))) succ1))) as s1' in *.
739 set (mapOptionTree (flatten_type ○ unlev) (dropT (mkFlags
740 (liftBoolFunc true (bnot ○ levelMatch (ec :: nil))) succ2))) as s2' in *.
742 apply (Prelude_error "almost there!").
745 Lemma unlev_relev : forall {Γ}(t:Tree ??(HaskType Γ ★)) lev, mapOptionTree unlev (t @@@ lev) = t.
748 destruct a; reflexivity.
749 rewrite <- IHt1 at 2.
750 rewrite <- IHt2 at 2.
754 Lemma tree_of_nothing : forall Γ ec t,
755 Arrange (mapOptionTree flatten_leveled_type (drop_lev(Γ:=Γ) (ec :: nil) (t @@@ (ec :: nil)))) [].
757 induction t; try destruct o; try destruct a.
764 eapply AComp; [ idtac | apply ACanL ].
765 eapply AComp; [ idtac | eapply ALeft; apply IHt2 ].
768 Transparent drop_lev.
775 Lemma tree_of_nothing' : forall Γ ec t,
776 Arrange [] (mapOptionTree flatten_leveled_type (drop_lev(Γ:=Γ) (ec :: nil) (t @@@ (ec :: nil)))).
778 induction t; try destruct o; try destruct a.
785 eapply AComp; [ apply AuCanL | idtac ].
786 eapply AComp; [ eapply ARight; apply IHt1 | idtac ].
789 Transparent drop_lev.
796 Lemma krunk : forall Γ (ec:HaskTyVar Γ ECKind) t,
797 flatten_type (<[ ec |- t ]>)
799 (mapOptionTree flatten_type (take_arg_types_as_tree t))
800 [ flatten_type (drop_arg_types_as_tree t)].
802 unfold flatten_type at 1.
805 apply phoas_extensionality.
810 rewrite <- mapOptionTree_compose.
811 unfold take_arg_types_as_tree.
813 replace (flatten_type (drop_arg_types_as_tree t) tv ite)
814 with (drop_arg_types (flatten_rawtype (t tv ite))).
815 replace (unleaves_ (take_arg_types (flatten_rawtype (t tv ite))))
816 with ((mapOptionTree (fun x : HaskType Γ ★ => flatten_type x tv ite)
818 (take_trustme (count_arg_types (t (fun _ : Kind => unit) (ite_unit Γ)))
819 (fun TV : Kind → Type => take_arg_types ○ t TV))))).
828 Lemma drop_to_nothing : forall (Γ:TypeEnv) Σ (lev:HaskLevel Γ),
829 drop_lev lev (Σ @@@ lev) = mapTree (fun _ => None) (mapTree (fun _ => tt) Σ).
843 Definition flatten_skolemized_proof :
846 ND Rule (mapOptionTree (flatten_judgment ) h) (mapOptionTree (flatten_judgment ) c).
848 eapply nd_map'; [ idtac | apply X ].
854 (match X as R in SRule H C with
855 | SBrak Γ Δ t ec succ lev => let case_SBrak := tt in _
856 | SEsc Γ Δ t ec succ lev => let case_SEsc := tt in _
857 | SFlat h c r => let case_SFlat := tt in _
861 refine (match r as R in Rule H C with
862 | RArrange Γ Δ a b x l d => let case_RArrange := tt in _
863 | RNote Γ Δ Σ τ l n => let case_RNote := tt in _
864 | RLit Γ Δ l _ => let case_RLit := tt in _
865 | RVar Γ Δ σ lev => let case_RVar := tt in _
866 | RGlobal Γ Δ σ l wev => let case_RGlobal := tt in _
867 | RLam Γ Δ Σ tx te lev => let case_RLam := tt in _
868 | RCast Γ Δ Σ σ τ lev γ => let case_RCast := tt in _
869 | RAbsT Γ Δ Σ κ σ lev n => let case_RAbsT := tt in _
870 | RAppT Γ Δ Σ κ σ τ lev => let case_RAppT := tt in _
871 | RAppCo Γ Δ Σ κ σ₁ σ₂ γ σ lev => let case_RAppCo := tt in _
872 | RAbsCo Γ Δ Σ κ σ σ₁ σ₂ lev => let case_RAbsCo := tt in _
873 | RApp Γ Δ Σ₁ Σ₂ tx te lev => let case_RApp := tt in _
874 | RCut Γ Δ Σ Σ₁ Σ₁₂ Σ₂ Σ₃ l => let case_RCut := tt in _
875 | RLeft Γ Δ Σ₁ Σ₂ Σ l => let case_RLeft := tt in _
876 | RRight Γ Δ Σ₁ Σ₂ Σ l => let case_RRight := tt in _
877 | RVoid _ _ l => let case_RVoid := tt in _
878 | RBrak Γ Δ t ec succ lev => let case_RBrak := tt in _
879 | REsc Γ Δ t ec succ lev => let case_REsc := tt in _
880 | RCase Γ Δ lev tc Σ avars tbranches alts => let case_RCase := tt in _
881 | RLetRec Γ Δ lri x y t => let case_RLetRec := tt in _
884 destruct case_RArrange.
885 apply (flatten_arrangement'' Γ Δ a b x _ d).
888 apply (Prelude_error "found unskolemized Brak rule; this shouldn't happen").
891 apply (Prelude_error "found unskolemized Esc rule; this shouldn't happen").
896 apply nd_rule; apply RNote; auto.
897 apply nd_rule; apply RNote; auto.
902 unfold flatten_leveled_type.
904 rewrite literal_types_unchanged.
905 apply nd_rule; apply RLit.
906 unfold take_lev; simpl.
907 unfold drop_lev; simpl.
909 rewrite literal_types_unchanged.
913 Opaque flatten_judgment.
915 Transparent flatten_judgment.
917 unfold flatten_judgment.
919 apply nd_rule. apply RVar.
920 repeat drop_simplify.
921 repeat take_simplify.
925 destruct case_RGlobal.
929 destruct l as [|ec lev]; simpl.
931 destruct (eqd_dec (g:CoreVar) (hetmet_flatten:CoreVar)).
932 set (flatten_type (g wev)) as t.
933 set (RGlobal _ Δ nil (mkGlobal Γ t hetmet_id)) as q.
938 destruct (eqd_dec (g:CoreVar) (hetmet_unflatten:CoreVar)).
939 set (flatten_type (g wev)) as t.
940 set (RGlobal _ Δ nil (mkGlobal Γ t hetmet_id)) as q.
946 unfold flatten_leveled_type. simpl.
947 apply nd_rule; rewrite globals_do_not_have_code_types.
949 apply (Prelude_error "found RGlobal at depth >0; globals should never appear inside code brackets unless escaped").
955 destruct lev as [|ec lev]; simpl; [ apply nd_rule; apply RLam; auto | idtac ].
956 repeat drop_simplify.
957 repeat take_simplify.
969 destruct lev as [|ec lev]; simpl; [ apply nd_rule; apply RCast; auto | idtac ].
971 apply flatten_coercion; auto.
972 apply (Prelude_error "RCast at level >0; casting inside of code brackets is currently not supported").
977 destruct lev as [|ec lev].
978 unfold flatten_type at 1.
983 repeat drop_simplify.
984 repeat take_simplify.
985 rewrite mapOptionTree_distributes.
986 set (mapOptionTree (flatten_leveled_type ) (drop_lev (ec :: lev) Σ₁)) as Σ₁'.
987 set (mapOptionTree (flatten_leveled_type ) (drop_lev (ec :: lev) Σ₂)) as Σ₂'.
988 set (take_lev (ec :: lev) Σ₁) as Σ₁''.
989 set (take_lev (ec :: lev) Σ₂) as Σ₂''.
990 replace (flatten_type (tx ---> te)) with ((flatten_type tx) ---> (flatten_type te)).
991 apply (Prelude_error "FIXME: ga_apply").
995 Notation "` x" := (take_lev _ x).
996 Notation "`` x" := (mapOptionTree unlev x) (at level 20).
997 Notation "``` x" := ((drop_lev _ x)) (at level 20).
998 Notation "!<[]> x" := (flatten_type _ x) (at level 1).
999 Notation "!<[@]> x" := (mapOptionTree flatten_leveled_type x) (at level 1).
1004 destruct l as [|ec lev]; simpl.
1006 replace (mapOptionTree flatten_leveled_type (Σ₁₂ @@@ nil)) with (mapOptionTree flatten_type Σ₁₂ @@@ nil).
1008 induction Σ₁₂; try destruct a; auto.
1013 simpl; repeat drop_simplify.
1014 simpl; repeat take_simplify.
1016 set (drop_lev (ec :: lev) (Σ₁₂ @@@ (ec :: lev))) as x1.
1017 rewrite take_lemma'.
1018 rewrite mapOptionTree_compose.
1019 rewrite mapOptionTree_compose.
1020 rewrite mapOptionTree_compose.
1021 rewrite mapOptionTree_compose.
1022 rewrite unlev_relev.
1023 rewrite <- mapOptionTree_compose.
1024 rewrite <- mapOptionTree_compose.
1025 rewrite <- mapOptionTree_compose.
1026 eapply nd_comp; [ idtac | eapply nd_rule; eapply RCut ].
1035 rewrite drop_to_nothing.
1036 apply arrangeCancelEmptyTree with (q:=(mapTree (fun _ : ??(HaskType Γ ★) => tt) Σ₁₂)).
1037 induction Σ₁₂; try destruct a; auto.
1039 rewrite <- IHΣ₁₂1 at 2.
1040 rewrite <- IHΣ₁₂2 at 2.
1042 eapply nd_comp; [ eapply nd_rule; eapply RArrange; eapply ALeft; eapply ACanL | idtac ].
1043 set (mapOptionTree flatten_type Σ₁₂) as a.
1044 set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) Σ₁)) as b.
1045 set (mapOptionTree flatten_leveled_type (drop_lev (ec :: lev) Σ₂)) as c.
1046 set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) Σ₂)) as d.
1047 set (mapOptionTree flatten_leveled_type (drop_lev (ec :: lev) Σ)) as e.
1048 set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) Σ)) as f.
1049 eapply nd_comp; [ idtac | eapply nd_rule; eapply RCut ].
1050 eapply nd_comp; [ apply nd_llecnac | idtac ].
1055 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ALeft; eapply AExch ].
1056 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AuAssoc ].
1060 destruct case_RLeft.
1062 destruct l as [|ec lev].
1064 replace (mapOptionTree flatten_leveled_type (Σ @@@ nil)) with (mapOptionTree flatten_type Σ @@@ nil).
1067 induction Σ; try destruct a; auto.
1072 repeat drop_simplify.
1073 rewrite drop_to_nothing.
1080 apply arrangeUnCancelEmptyTree with (q:=(mapTree (fun _ : ??(HaskType Γ ★) => tt) Σ)).
1081 induction Σ; try destruct a; auto.
1083 rewrite <- IHΣ1 at 2.
1084 rewrite <- IHΣ2 at 2.
1087 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AuCanL ].
1091 replace (take_lev (ec :: lev) (Σ @@@ (ec :: lev))) with (Σ @@@ (ec::lev)).
1092 rewrite mapOptionTree_compose.
1093 rewrite mapOptionTree_compose.
1094 rewrite unlev_relev.
1096 rewrite take_lemma'.
1099 destruct case_RRight.
1101 destruct l as [|ec lev].
1103 replace (mapOptionTree flatten_leveled_type (Σ @@@ nil)) with (mapOptionTree flatten_type Σ @@@ nil).
1106 induction Σ; try destruct a; auto.
1111 repeat drop_simplify.
1112 rewrite drop_to_nothing.
1119 apply arrangeUnCancelEmptyTree with (q:=(mapTree (fun _ : ??(HaskType Γ ★) => tt) Σ)).
1120 induction Σ; try destruct a; auto.
1122 rewrite <- IHΣ1 at 2.
1123 rewrite <- IHΣ2 at 2.
1126 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AuCanR ].
1130 replace (take_lev (ec :: lev) (Σ @@@ (ec :: lev))) with (Σ @@@ (ec::lev)).
1131 rewrite mapOptionTree_compose.
1132 rewrite mapOptionTree_compose.
1133 rewrite unlev_relev.
1135 rewrite take_lemma'.
1138 destruct case_RVoid.
1148 destruct case_RAppT.
1149 simpl. destruct lev; simpl.
1150 unfold flatten_leveled_type.
1152 rewrite flatten_commutes_with_HaskTAll.
1153 rewrite flatten_commutes_with_substT.
1158 apply (Prelude_error "found type application at level >0; this is not supported").
1160 destruct case_RAbsT.
1161 simpl. destruct lev; simpl.
1162 rewrite flatten_commutes_with_HaskTAll.
1163 rewrite flatten_commutes_with_HaskTApp.
1164 eapply nd_comp; [ idtac | eapply nd_rule; eapply RAbsT ].
1166 set (mapOptionTree (flatten_leveled_type ) (mapOptionTree (weakLT_(n:=n)(κ:=κ)) Σ)) as a.
1167 set (mapOptionTree (weakLT_(n:=n)(κ:=κ)) (mapOptionTree (flatten_leveled_type ) Σ)) as q'.
1175 rewrite flatten_commutes_with_weakLT.
1186 apply (Prelude_error "found type abstraction at level >0; this is not supported").
1188 destruct case_RAppCo.
1189 simpl. destruct lev; simpl.
1190 unfold flatten_type.
1194 apply flatten_coercion.
1196 apply (Prelude_error "found coercion application at level >0; this is not supported").
1198 destruct case_RAbsCo.
1199 simpl. destruct lev; simpl.
1200 unfold flatten_type.
1202 apply (Prelude_error "AbsCo not supported (FIXME)").
1203 apply (Prelude_error "found coercion abstraction at level >0; this is not supported").
1205 destruct case_RLetRec.
1207 simpl. destruct lev; simpl.
1209 set (@RLetRec Γ Δ (mapOptionTree flatten_leveled_type lri) (flatten_type x) (mapOptionTree flatten_type y) nil) as q.
1210 replace (mapOptionTree flatten_leveled_type (y @@@ nil)) with (mapOptionTree flatten_type y @@@ nil).
1212 induction y; try destruct a; auto.
1217 repeat drop_simplify.
1218 repeat take_simplify.
1220 rewrite drop_to_nothing.
1226 apply arrangeCancelEmptyTree with (q:=y).
1227 induction y; try destruct a; auto.
1233 rewrite take_lemma'.
1234 set (mapOptionTree (flatten_type ○ unlev) (take_lev (h :: lev) lri)) as lri'.
1235 set (mapOptionTree flatten_leveled_type (drop_lev (h :: lev) lri)) as lri''.
1236 replace (mapOptionTree (flatten_type ○ unlev) (y @@@ (h :: lev))) with (mapOptionTree flatten_type y).
1239 rewrite <- mapOptionTree_compose.
1243 destruct case_RCase.
1244 destruct lev; [ idtac | apply (Prelude_error "case at depth >0") ]; simpl.
1246 rewrite <- mapOptionTree_compose.
1247 replace (mapOptionTree
1248 (fun x => flatten_judgment (pcb_judg (snd x)))
1249 alts,, [Γ > Δ > mapOptionTree flatten_leveled_type Σ |- [flatten_type (caseType tc avars)] @ nil])
1252 (fun x => @pcb_judg tc Γ Δ nil (flatten_type tbranches) avars (fst x) (snd x))
1254 [Γ > Δ > mapOptionTree flatten_leveled_type Σ |- [caseType tc avars] @ nil]).
1255 replace (mapOptionTree flatten_leveled_type
1256 (mapOptionTreeAndFlatten
1257 (fun x => (snd x)) alts))
1258 with (mapOptionTreeAndFlatten
1265 destruct case_SBrak.
1269 set (drop_lev (ec :: nil) (take_arg_types_as_tree t @@@ (ec :: nil))) as empty_tree.
1271 rewrite take_lemma'.
1273 rewrite mapOptionTree_compose.
1274 rewrite mapOptionTree_compose.
1275 rewrite unlev_relev.
1276 rewrite <- mapOptionTree_compose.
1279 set (mapOptionTree flatten_leveled_type (drop_lev (ec :: nil) succ)) as succ_host.
1280 set (mapOptionTree (flatten_type ○ unlev)(take_lev (ec :: nil) succ)) as succ_guest.
1281 set (mapOptionTree flatten_type (take_arg_types_as_tree t)) as succ_args.
1283 eapply nd_comp; [ eapply nd_rule; eapply RArrange; eapply ALeft; apply tree_of_nothing | idtac ].
1284 eapply nd_comp; [ eapply nd_rule; eapply RArrange; eapply ACanR | idtac ].
1285 refine (ga_unkappa Γ Δ (v2t ec) nil _ _ _ _ ;; _).
1286 eapply nd_comp; [ idtac | eapply arrange_brak ].
1292 apply (Prelude_error "found Brak at depth >0 indicating 3-level code; only two-level code is currently supported").
1298 unfold flatten_leveled_type at 2.
1301 rewrite mapOptionTree_compose.
1305 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ALeft; apply tree_of_nothing' ].
1306 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ACanR ].
1308 rewrite take_lemma'.
1309 rewrite unlev_relev.
1310 rewrite <- mapOptionTree_compose.
1311 eapply nd_comp; [ apply (arrange_esc _ _ ec) | idtac ].
1313 set (decide_tree_empty (take_lev (ec :: nil) succ)) as q'.
1319 set (mapOptionTree flatten_leveled_type (drop_lev (ec :: nil) succ)) as succ_host.
1320 set (mapOptionTree flatten_type (take_arg_types_as_tree t)) as succ_args.
1322 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply AuCanR ].
1323 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply AuCanR ].
1324 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply ACanL ].
1325 eapply nd_comp; [ idtac | eapply RLet ].
1326 eapply nd_comp; [ apply nd_llecnac | idtac ].
1327 apply nd_prod; [ idtac | eapply boost ].
1330 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ACanL ].
1338 refine ( _ ;; (boost _ _ _ _ _ (postcompose _ _ _ _ _ _ _ _))).
1346 refine ( _ ;; (boost _ _ _ _ _ (postcompose _ _ _ _ _ _ _ _))).
1348 refine ( _ ;; (boost _ _ _ _ _ (postcompose _ _ _ _ _ _ _ _))).
1354 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AuCanR ].
1355 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AuCanR ].
1357 replace (mapOptionTree (fun ht => levels_to_tcode (unlev ht) (getlev ht) @@ nil) (drop_lev (ec :: nil) succ))
1358 with (mapOptionTree flatten_leveled_type (drop_lev (ec :: nil) succ)).
1359 eapply nd_comp; [ eapply nd_rule; eapply RArrange; eapply AExch | idtac ].
1364 Transparent drop_lev.
1370 destruct (General.list_eq_dec h1 (ec :: nil)).
1374 unfold flatten_leveled_type.
1386 (* nesting too deep *)
1387 apply (Prelude_error "found Esc at depth >0 indicating 3-level code; only two-level code is currently supported").
1390 Definition flatten_proof :
1394 apply (Prelude_error "sorry, non-skolemized flattening isn't implemented").
1397 Definition skolemize_and_flatten_proof :
1401 (mapOptionTree (flatten_judgment ○ skolemize_judgment) h)
1402 (mapOptionTree (flatten_judgment ○ skolemize_judgment) c).
1404 rewrite mapOptionTree_compose.
1405 rewrite mapOptionTree_compose.
1406 apply flatten_skolemized_proof.
1407 apply skolemize_proof.
1412 (* to do: establish some metric on judgments (max length of level of any succedent type, probably), show how to
1413 * calculate it, and show that the flattening procedure above drives it down by one *)
1416 Instance FlatteningFunctor {Γ}{Δ}{ec} : Functor (JudgmentsL (PCF Γ Δ ec)) (TypesL (SystemFCa Γ Δ)) (obact) :=
1417 { fmor := FlatteningFunctor_fmor }.
1419 Definition ReificationFunctor Γ Δ : Functor (JudgmentsL _ _ (PCF n Γ Δ)) SystemFCa' (mapOptionTree brakifyJudg).
1420 refine {| fmor := ReificationFunctor_fmor Γ Δ |}; unfold hom; unfold ob; simpl ; intros.
1422 Definition PCF_SMME (n:nat)(Γ:TypeEnv)(Δ:CoercionEnv Γ) : ProgrammingLanguageSMME.
1423 refine {| plsmme_pl := PCF n Γ Δ |}.
1426 Definition SystemFCa_SMME (n:nat)(Γ:TypeEnv)(Δ:CoercionEnv Γ) : ProgrammingLanguageSMME.
1427 refine {| plsmme_pl := SystemFCa n Γ Δ |}.
1430 Definition ReificationFunctorMonoidal n : MonoidalFunctor (JudgmentsN n) (JudgmentsN (S n)) (ReificationFunctor n).
1434 Definition PCF_SystemFCa_two_level n Γ Δ : TwoLevelLanguage (PCF_SMME n Γ Δ) (SystemFCa_SMME (S n) Γ Δ).
1437 (* ... and the retraction exists *)
1441 Implicit Arguments garrow [ ].