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.
52 | [ |- context[@eqd_dec ?T ?V ?X ?X] ] =>
53 destruct (@eqd_dec T V X X) as [eqd_dec1 | eqd_dec2];
54 [ clear eqd_dec1 | set (eqd_dec2 (refl_equal _)) as eqd_dec2'; inversion eqd_dec2' ]
57 Definition v2t {Γ}(ec:HaskTyVar Γ ECKind) : HaskType Γ ECKind := fun TV ite => TVar (ec TV ite).
59 Definition levelMatch {Γ}(lev:HaskLevel Γ) : LeveledHaskType Γ ★ -> bool :=
60 fun t => match t with ttype@@tlev => if eqd_dec tlev lev then true else false end.
62 (* In a tree of types, replace any type at depth "lev" or greater None *)
63 Definition mkDropFlags {Γ}(lev:HaskLevel Γ)(tt:Tree ??(LeveledHaskType Γ ★)) : TreeFlags tt :=
64 mkFlags (liftBoolFunc false (levelMatch lev)) tt.
66 Definition drop_lev {Γ}(lev:HaskLevel Γ)(tt:Tree ??(LeveledHaskType Γ ★)) : Tree ??(LeveledHaskType Γ ★) :=
67 dropT (mkDropFlags lev tt).
69 (* The opposite: replace any type which is NOT at level "lev" with None *)
70 Definition mkTakeFlags {Γ}(lev:HaskLevel Γ)(tt:Tree ??(LeveledHaskType Γ ★)) : TreeFlags tt :=
71 mkFlags (liftBoolFunc true (bnot ○ levelMatch lev)) tt.
73 Definition take_lev {Γ}(lev:HaskLevel Γ)(tt:Tree ??(LeveledHaskType Γ ★)) : Tree ??(LeveledHaskType Γ ★) :=
74 dropT (mkTakeFlags lev tt).
76 mapOptionTree (fun x => flatten_type (unlev x))
77 (maybeTree (takeT tt (mkFlags (
79 | Some (ttype @@ tlev) => if eqd_dec tlev lev then true else false
84 Definition maybeTree {T}(t:??(Tree ??T)) : Tree ??T :=
91 Lemma drop_lev_lemma : forall Γ (lev:HaskLevel Γ) x, drop_lev lev [x @@ lev] = [].
103 Lemma drop_lev_lemma_s : forall Γ (lev:HaskLevel Γ) ec x, drop_lev (ec::lev) [x @@ (ec :: lev)] = [].
114 Lemma take_lemma : forall Γ (lev:HaskLevel Γ) x, take_lev lev [x @@ lev] = [x @@ lev].
125 Lemma take_lemma' : forall Γ (lev:HaskLevel Γ) x, take_lev lev (x @@@ lev) = x @@@ lev.
128 destruct a; simpl; try reflexivity.
131 rewrite <- IHx1 at 2.
132 rewrite <- IHx2 at 2.
136 Ltac drop_simplify :=
138 | [ |- context[@drop_lev ?G ?L [ ?X @@ ?L ] ] ] =>
139 rewrite (drop_lev_lemma G L X)
140 | [ |- context[@drop_lev ?G (?E :: ?L) [ ?X @@ (?E :: ?L) ] ] ] =>
141 rewrite (drop_lev_lemma_s G L E X)
142 | [ |- context[@drop_lev ?G ?N (?A,,?B)] ] =>
143 change (@drop_lev G N (A,,B)) with ((@drop_lev G N A),,(@drop_lev G N B))
144 | [ |- context[@drop_lev ?G ?N (T_Leaf None)] ] =>
145 change (@drop_lev G N (T_Leaf (@None (LeveledHaskType G ★)))) with (T_Leaf (@None (LeveledHaskType G ★)))
148 Ltac take_simplify :=
150 | [ |- context[@take_lev ?G ?L [ ?X @@ ?L ] ] ] =>
151 rewrite (take_lemma G L X)
152 | [ |- context[@take_lev ?G ?L [ ?X @@@ ?L ] ] ] =>
153 rewrite (take_lemma' G L X)
154 | [ |- context[@take_lev ?G ?N (?A,,?B)] ] =>
155 change (@take_lev G N (A,,B)) with ((@take_lev G N A),,(@take_lev G N B))
156 | [ |- context[@take_lev ?G ?N (T_Leaf None)] ] =>
157 change (@take_lev G N (T_Leaf (@None (LeveledHaskType G ★)))) with (T_Leaf (@None (LeveledHaskType G ★)))
161 (*******************************************************************************)
164 Context {unitTy : forall TV, RawHaskType TV ECKind -> RawHaskType TV ★ }.
165 Context {prodTy : forall TV, RawHaskType TV ECKind -> RawHaskType TV ★ -> RawHaskType TV ★ -> RawHaskType TV ★ }.
166 Context {gaTy : forall TV, RawHaskType TV ECKind -> RawHaskType TV ★ -> RawHaskType TV ★ -> RawHaskType TV ★ }.
168 Definition ga_mk_tree' {TV}(ec:RawHaskType TV ECKind)(tr:Tree ??(RawHaskType TV ★)) : RawHaskType TV ★ :=
169 reduceTree (unitTy TV ec) (prodTy TV ec) tr.
171 Definition ga_mk_tree {Γ}(ec:HaskType Γ ECKind)(tr:Tree ??(HaskType Γ ★)) : HaskType Γ ★ :=
172 fun TV ite => ga_mk_tree' (ec TV ite) (mapOptionTree (fun x => x TV ite) tr).
174 Definition ga_mk_raw {TV}(ec:RawHaskType TV ECKind)(ant suc:Tree ??(RawHaskType TV ★)) : RawHaskType TV ★ :=
177 (ga_mk_tree' ec suc).
179 Definition ga_mk {Γ}(ec:HaskType Γ ECKind)(ant suc:Tree ??(HaskType Γ ★)) : HaskType Γ ★ :=
180 fun TV ite => gaTy TV (ec TV ite) (ga_mk_tree ec ant TV ite) (ga_mk_tree ec suc TV ite).
184 * - code types <[t]>@c become garrows c () t
185 * - free variables of type t at a level lev deeper than the succedent become garrows c () t
186 * - free variables at the level of the succedent become
188 Fixpoint flatten_rawtype {TV}{κ}(exp: RawHaskType TV κ) : RawHaskType TV κ :=
191 | TAll _ y => TAll _ (fun v => flatten_rawtype (y v))
192 | TApp _ _ x y => TApp (flatten_rawtype x) (flatten_rawtype y)
194 | TCoerc _ t1 t2 t => TCoerc (flatten_rawtype t1) (flatten_rawtype t2) (flatten_rawtype t)
196 | TCode ec e => let e' := flatten_rawtype e
197 in ga_mk_raw ec (unleaves_ (take_arg_types e')) [drop_arg_types e']
198 | TyFunApp tfc kl k lt => TyFunApp tfc kl k (flatten_rawtype_list _ lt)
200 with flatten_rawtype_list {TV}(lk:list Kind)(exp:@RawHaskTypeList TV lk) : @RawHaskTypeList TV lk :=
201 match exp in @RawHaskTypeList _ LK return @RawHaskTypeList TV LK with
202 | TyFunApp_nil => TyFunApp_nil
203 | TyFunApp_cons κ kl t rest => TyFunApp_cons _ _ (flatten_rawtype t) (flatten_rawtype_list _ rest)
206 Definition flatten_type {Γ}{κ}(ht:HaskType Γ κ) : HaskType Γ κ :=
207 fun TV ite => flatten_rawtype (ht TV ite).
209 Fixpoint levels_to_tcode {Γ}(ht:HaskType Γ ★)(lev:HaskLevel Γ) : HaskType Γ ★ :=
211 | nil => flatten_type ht
212 | ec::lev' => @ga_mk _ (v2t ec) [] [levels_to_tcode ht lev']
215 Definition flatten_leveled_type {Γ}(ht:LeveledHaskType Γ ★) : LeveledHaskType Γ ★ :=
216 levels_to_tcode (unlev ht) (getlev ht) @@ nil.
220 Axiom literal_types_unchanged : forall Γ l, flatten_type (literalType l) = literalType(Γ:=Γ) l.
222 Axiom flatten_coercion : forall Γ Δ κ (σ τ:HaskType Γ κ) (γ:HaskCoercion Γ Δ (σ ∼∼∼ τ)),
223 HaskCoercion Γ Δ (flatten_type σ ∼∼∼ flatten_type τ).
225 Axiom flatten_commutes_with_substT :
226 forall κ Γ (Δ:CoercionEnv Γ) (σ:∀ TV, InstantiatedTypeEnv TV Γ → TV κ → RawHaskType TV ★) (τ:HaskType Γ κ),
227 flatten_type (substT σ τ) = substT (fun TV ite v => flatten_rawtype (σ TV ite v))
230 Axiom flatten_commutes_with_HaskTAll :
231 forall κ Γ (Δ:CoercionEnv Γ) (σ:∀ TV, InstantiatedTypeEnv TV Γ → TV κ → RawHaskType TV ★),
232 flatten_type (HaskTAll κ σ) = HaskTAll κ (fun TV ite v => flatten_rawtype (σ TV ite v)).
234 Axiom flatten_commutes_with_HaskTApp :
235 forall κ Γ (Δ:CoercionEnv Γ) (σ:∀ TV, InstantiatedTypeEnv TV Γ → TV κ → RawHaskType TV ★),
236 flatten_type (HaskTApp (weakF σ) (FreshHaskTyVar κ)) =
237 HaskTApp (weakF (fun TV ite v => flatten_rawtype (σ TV ite v))) (FreshHaskTyVar κ).
239 Axiom flatten_commutes_with_weakLT : forall (Γ:TypeEnv) κ t,
240 flatten_leveled_type (weakLT(Γ:=Γ)(κ:=κ) t) = weakLT(Γ:=Γ)(κ:=κ) (flatten_leveled_type t).
242 Axiom globals_do_not_have_code_types : forall (Γ:TypeEnv) (g:Global Γ) v,
243 flatten_type (g v) = g v.
245 (* "n" is the maximum depth remaining AFTER flattening *)
246 Definition flatten_judgment (j:Judg) :=
247 match j as J return Judg with
248 | Γ > Δ > ant |- suc @ nil => Γ > Δ > mapOptionTree flatten_leveled_type ant
249 |- mapOptionTree flatten_type suc @ nil
250 | Γ > Δ > ant |- suc @ (ec::lev') => Γ > Δ > mapOptionTree flatten_leveled_type (drop_lev (ec::lev') ant)
252 (mapOptionTree (flatten_type ○ unlev) (take_lev (ec::lev') ant))
253 (mapOptionTree flatten_type suc )
258 { ga_id : ∀ Γ Δ ec l a , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec a a ]@l ]
259 ; ga_cancelr : ∀ Γ Δ ec l a , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec (a,,[]) a ]@l ]
260 ; ga_cancell : ∀ Γ Δ ec l a , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec ([],,a) a ]@l ]
261 ; ga_uncancelr : ∀ Γ Δ ec l a , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec a (a,,[]) ]@l ]
262 ; ga_uncancell : ∀ Γ Δ ec l a , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec a ([],,a) ]@l ]
263 ; ga_assoc : ∀ Γ Δ ec l a b c, ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec ((a,,b),,c) (a,,(b,,c)) ]@l ]
264 ; ga_unassoc : ∀ Γ Δ ec l a b c, ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec (a,,(b,,c)) ((a,,b),,c) ]@l ]
265 ; ga_swap : ∀ Γ Δ ec l a b , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec (a,,b) (b,,a) ]@l ]
266 ; ga_drop : ∀ Γ Δ ec l a , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec a [] ]@l ]
267 ; ga_copy : ∀ Γ Δ ec l a , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec a (a,,a) ]@l ]
268 ; ga_first : ∀ Γ Δ ec l a b x, ND Rule [] [Γ > Δ > [@ga_mk Γ ec a b @@l] |- [@ga_mk Γ ec (a,,x) (b,,x) ]@l ]
269 ; ga_second : ∀ Γ Δ ec l a b x, ND Rule [] [Γ > Δ > [@ga_mk Γ ec a b @@l] |- [@ga_mk Γ ec (x,,a) (x,,b) ]@l ]
270 ; ga_lit : ∀ Γ Δ ec l lit , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec [] [literalType lit] ]@l ]
271 ; ga_curry : ∀ Γ Δ ec l a b c, ND Rule [] [Γ > Δ > [@ga_mk Γ ec (a,,[b]) [c] @@ l] |- [@ga_mk Γ ec a [b ---> c] ]@ l ]
272 ; ga_loopl : ∀ Γ Δ ec l x y z, ND Rule [] [Γ > Δ > [@ga_mk Γ ec (z,,x) (z,,y) @@ l] |- [@ga_mk Γ ec x y ]@ l ]
273 ; ga_loopr : ∀ Γ Δ ec l x y z, ND Rule [] [Γ > Δ > [@ga_mk Γ ec (x,,z) (y,,z) @@ l] |- [@ga_mk Γ ec x y ]@ l ]
274 ; 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 ]
275 ; ga_apply : ∀ Γ Δ ec l a a' b c,
276 ND Rule [] [Γ > Δ > [@ga_mk Γ ec a [b ---> c] @@ l],,[@ga_mk Γ ec a' [b] @@ l] |- [@ga_mk Γ ec (a,,a') [c] ]@l ]
277 ; ga_kappa : ∀ Γ Δ ec l a b Σ, ND Rule
278 [Γ > Δ > Σ,,[@ga_mk Γ ec [] a @@ l] |- [@ga_mk Γ ec [] b ]@l ]
279 [Γ > Δ > Σ |- [@ga_mk Γ ec a b ]@l ]
281 Context `(gar:garrow).
283 Notation "a ~~~~> b" := (@ga_mk _ _ a b) (at level 20).
285 Definition boost : forall Γ Δ ant x y {lev},
286 ND Rule [] [ Γ > Δ > [x@@lev] |- [y]@lev ] ->
287 ND Rule [ Γ > Δ > ant |- [x]@lev ] [ Γ > Δ > ant |- [y]@lev ].
289 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ACanR ].
290 eapply nd_comp; [ idtac | apply RLet ].
291 eapply nd_comp; [ apply nd_rlecnac | idtac ].
301 Definition precompose Γ Δ ec : forall a x y z lev,
303 [ Γ > Δ > a |- [@ga_mk _ ec y z ]@lev ]
304 [ Γ > Δ > a,,[@ga_mk _ ec x y @@ lev] |- [@ga_mk _ ec x z ]@lev ].
306 eapply nd_comp; [ idtac | eapply RLet ].
307 eapply nd_comp; [ apply nd_rlecnac | idtac ].
310 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AExch ].
314 Definition precompose' Γ Δ ec : forall a b x y z lev,
316 [ Γ > Δ > a,,b |- [@ga_mk _ ec y z ]@lev ]
317 [ Γ > Δ > a,,([@ga_mk _ ec x y @@ lev],,b) |- [@ga_mk _ ec x z ]@lev ].
319 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ALeft; eapply AExch ].
320 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AuAssoc ].
324 Definition postcompose_ Γ Δ ec : forall a x y z lev,
326 [ Γ > Δ > a |- [@ga_mk _ ec x y ]@lev ]
327 [ Γ > Δ > a,,[@ga_mk _ ec y z @@ lev] |- [@ga_mk _ ec x z ]@lev ].
329 eapply nd_comp; [ idtac | eapply RLet ].
330 eapply nd_comp; [ apply nd_rlecnac | idtac ].
336 Definition postcompose Γ Δ ec : forall x y z lev,
337 ND Rule [] [ Γ > Δ > [] |- [@ga_mk _ ec x y ]@lev ] ->
338 ND Rule [] [ Γ > Δ > [@ga_mk _ ec y z @@ lev] |- [@ga_mk _ ec x z ]@lev ].
340 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ACanL ].
341 eapply nd_comp; [ idtac | eapply postcompose_ ].
345 Definition first_nd : ∀ Γ Δ ec lev a b c Σ,
346 ND Rule [ Γ > Δ > Σ |- [@ga_mk Γ ec a b ]@lev ]
347 [ Γ > Δ > Σ |- [@ga_mk Γ ec (a,,c) (b,,c) ]@lev ].
349 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ACanR ].
350 eapply nd_comp; [ idtac | apply RLet ].
351 eapply nd_comp; [ apply nd_rlecnac | idtac ].
354 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AuCanR ].
358 Definition firstify : ∀ Γ Δ ec lev a b c Σ,
359 ND Rule [] [ Γ > Δ > Σ |- [@ga_mk Γ ec a b ]@lev ] ->
360 ND Rule [] [ Γ > Δ > Σ |- [@ga_mk Γ ec (a,,c) (b,,c) ]@lev ].
367 Definition second_nd : ∀ Γ Δ ec lev a b c Σ,
369 [ Γ > Δ > Σ |- [@ga_mk Γ ec a b ]@lev ]
370 [ Γ > Δ > Σ |- [@ga_mk Γ ec (c,,a) (c,,b) ]@lev ].
372 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ACanR ].
373 eapply nd_comp; [ idtac | apply RLet ].
374 eapply nd_comp; [ apply nd_rlecnac | idtac ].
377 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AuCanR ].
381 Definition secondify : ∀ Γ Δ ec lev a b c Σ,
382 ND Rule [] [ Γ > Δ > Σ |- [@ga_mk Γ ec a b ]@lev ] ->
383 ND Rule [] [ Γ > Δ > Σ |- [@ga_mk Γ ec (c,,a) (c,,b) ]@lev ].
390 Lemma ga_unkappa : ∀ Γ Δ ec l a b Σ x,
392 [Γ > Δ > Σ |- [@ga_mk Γ ec (a,,x) b ]@l ]
393 [Γ > Δ > Σ,,[@ga_mk Γ ec [] a @@ l] |- [@ga_mk Γ ec x b ]@l ].
395 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AExch ].
396 eapply nd_comp; [ idtac | eapply RLet ].
397 eapply nd_comp; [ apply nd_llecnac | idtac ].
401 eapply nd_comp; [ idtac | eapply RLet ].
402 eapply nd_comp; [ apply nd_llecnac | idtac ].
406 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AExch ].
410 (* useful for cutting down on the pretty-printed noise
412 Notation "` x" := (take_lev _ x) (at level 20).
413 Notation "`` x" := (mapOptionTree unlev x) (at level 20).
414 Notation "``` x" := (drop_lev _ x) (at level 20).
416 Definition flatten_arrangement' :
417 forall Γ (Δ:CoercionEnv Γ)
418 (ec:HaskTyVar Γ ECKind) (lev:HaskLevel Γ) (ant1 ant2:Tree ??(LeveledHaskType Γ ★)) (r:Arrange ant1 ant2),
419 ND Rule [] [Γ > Δ > [] |- [@ga_mk _ (v2t ec) (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) ant2))
420 (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) ant1)) ]@nil ].
423 refine (fix flatten ant1 ant2 (r:Arrange ant1 ant2):
424 ND Rule [] [Γ > Δ > [] |- [@ga_mk _ (v2t ec)
425 (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) ant2))
426 (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) ant1)) ]@nil] :=
427 match r as R in Arrange A B return
428 ND Rule [] [Γ > Δ > [] |- [@ga_mk _ (v2t ec)
429 (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) B))
430 (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) A)) ]@nil]
432 | AId a => let case_AId := tt in ga_id _ _ _ _ _
433 | ACanL a => let case_ACanL := tt in ga_uncancell _ _ _ _ _
434 | ACanR a => let case_ACanR := tt in ga_uncancelr _ _ _ _ _
435 | AuCanL a => let case_AuCanL := tt in ga_cancell _ _ _ _ _
436 | AuCanR a => let case_AuCanR := tt in ga_cancelr _ _ _ _ _
437 | AAssoc a b c => let case_AAssoc := tt in ga_assoc _ _ _ _ _ _ _
438 | AuAssoc a b c => let case_AuAssoc := tt in ga_unassoc _ _ _ _ _ _ _
439 | AExch a b => let case_AExch := tt in ga_swap _ _ _ _ _ _
440 | AWeak a => let case_AWeak := tt in ga_drop _ _ _ _ _
441 | ACont a => let case_ACont := tt in ga_copy _ _ _ _ _
442 | ALeft a b c r' => let case_ALeft := tt in flatten _ _ r' ;; boost _ _ _ _ _ (ga_second _ _ _ _ _ _ _)
443 | ARight a b c r' => let case_ARight := tt in flatten _ _ r' ;; boost _ _ _ _ _ (ga_first _ _ _ _ _ _ _)
444 | AComp c b a r1 r2 => let case_AComp := tt in (fun r1' r2' => _) (flatten _ _ r1) (flatten _ _ r2)
445 end); clear flatten; repeat take_simplify; repeat drop_simplify; intros.
448 set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) a)) as a' in *.
449 set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) b)) as b' in *.
450 set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) c)) as c' in *.
451 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply ACanL ].
452 eapply nd_comp; [ idtac | apply
453 (@RLet Γ Δ [] [] (@ga_mk _ (v2t ec) a' b') (@ga_mk _ (v2t ec) a' c')) ].
454 eapply nd_comp; [ apply nd_llecnac | idtac ].
457 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply AuCanR ].
458 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply ACanL ].
459 eapply nd_comp; [ idtac | apply RLet ].
460 eapply nd_comp; [ apply nd_llecnac | idtac ].
463 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AExch ].
467 Definition flatten_arrangement :
468 forall Γ (Δ:CoercionEnv Γ) n
469 (ec:HaskTyVar Γ ECKind) (lev:HaskLevel Γ) (ant1 ant2:Tree ??(LeveledHaskType Γ ★)) (r:Arrange ant1 ant2) succ,
471 [Γ > Δ > mapOptionTree (flatten_leveled_type ) (drop_lev n ant1)
472 |- [@ga_mk _ (v2t ec)
473 (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) ant1))
474 (mapOptionTree (flatten_type ) succ) ]@nil]
475 [Γ > Δ > mapOptionTree (flatten_leveled_type ) (drop_lev n ant2)
476 |- [@ga_mk _ (v2t ec)
477 (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) ant2))
478 (mapOptionTree (flatten_type ) succ) ]@nil].
480 refine ( _ ;; (boost _ _ _ _ _ (postcompose _ _ _ _ _ _ _ (flatten_arrangement' Γ Δ ec lev ant1 ant2 r)))).
483 refine ((fix flatten ant1 ant2 (r:Arrange ant1 ant2) :=
484 match r as R in Arrange A B return
485 Arrange (mapOptionTree (flatten_leveled_type ) (drop_lev _ A))
486 (mapOptionTree (flatten_leveled_type ) (drop_lev _ B)) with
487 | AId a => let case_AId := tt in AId _
488 | ACanL a => let case_ACanL := tt in ACanL _
489 | ACanR a => let case_ACanR := tt in ACanR _
490 | AuCanL a => let case_AuCanL := tt in AuCanL _
491 | AuCanR a => let case_AuCanR := tt in AuCanR _
492 | AAssoc a b c => let case_AAssoc := tt in AAssoc _ _ _
493 | AuAssoc a b c => let case_AuAssoc := tt in AuAssoc _ _ _
494 | AExch a b => let case_AExch := tt in AExch _ _
495 | AWeak a => let case_AWeak := tt in AWeak _
496 | ACont a => let case_ACont := tt in ACont _
497 | ALeft a b c r' => let case_ALeft := tt in ALeft _ (flatten _ _ r')
498 | ARight a b c r' => let case_ARight := tt in ARight _ (flatten _ _ r')
499 | AComp a b c r1 r2 => let case_AComp := tt in AComp (flatten _ _ r1) (flatten _ _ r2)
500 end) ant1 ant2 r); clear flatten; repeat take_simplify; repeat drop_simplify; intros.
503 Definition flatten_arrangement'' :
504 forall Γ Δ ant1 ant2 succ l (r:Arrange ant1 ant2),
505 ND Rule (mapOptionTree (flatten_judgment ) [Γ > Δ > ant1 |- succ @ l])
506 (mapOptionTree (flatten_judgment ) [Γ > Δ > ant2 |- succ @ l]).
520 apply AExch. (* TO DO: check for all-leaf trees here *)
525 eapply AComp; [ apply IHr1 | apply IHr2 ].
527 apply flatten_arrangement.
531 Definition ga_join Γ Δ Σ₁ Σ₂ a b ec :
532 ND Rule [] [Γ > Δ > Σ₁ |- [@ga_mk _ ec [] a ]@nil] ->
533 ND Rule [] [Γ > Δ > Σ₂ |- [@ga_mk _ ec [] b ]@nil] ->
534 ND Rule [] [Γ > Δ > Σ₁,,Σ₂ |- [@ga_mk _ ec [] (a,,b) ]@nil].
537 apply secondify with (c:=a) in pfb.
538 apply firstify with (c:=[]) in pfa.
539 eapply nd_comp; [ idtac | eapply RLet ].
540 eapply nd_comp; [ eapply nd_llecnac | idtac ].
545 eapply nd_comp; [ idtac | eapply RLet ].
546 eapply nd_comp; [ apply nd_llecnac | idtac ].
548 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ACanL ].
549 eapply nd_comp; [ idtac | eapply postcompose_ ].
552 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AExch ].
553 eapply nd_comp; [ idtac | eapply precompose ].
557 Definition arrange_brak : forall Γ Δ ec succ t,
560 [(@ga_mk _ (v2t ec) [] (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: nil) succ))) @@ nil],,
561 mapOptionTree (flatten_leveled_type ) (drop_lev (ec :: nil) succ) |- [t]@nil]
562 [Γ > Δ > mapOptionTree (flatten_leveled_type ) succ |- [t]@nil].
566 set (@arrangeUnPartition _ succ (levelMatch (ec::nil))) as q.
567 set (arrangeMap _ _ flatten_leveled_type q) as y.
575 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AExch ].
577 eapply nd_comp; [ apply nd_llecnac | idtac ].
578 eapply nd_comp; [ idtac | eapply RLet ].
583 induction succ; try destruct a; simpl.
589 destruct l as [t' lev'].
590 destruct lev' as [|ec' lev'].
594 set (@eqd_dec (HaskLevel Γ) (haskLevelEqDecidable Γ) (ec' :: lev') (ec :: nil)) as q.
599 unfold flatten_leveled_type.
616 Definition arrange_esc : forall Γ Δ ec succ t,
618 [Γ > Δ > mapOptionTree (flatten_leveled_type ) succ |- [t]@nil]
620 [(@ga_mk _ (v2t ec) [] (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: nil) succ))) @@ nil],,
621 mapOptionTree (flatten_leveled_type ) (drop_lev (ec :: nil) succ) |- [t]@nil].
623 set (@arrangePartition _ succ (levelMatch (ec::nil))) as q.
624 set (@drop_lev Γ (ec::nil) succ) as q'.
625 assert (@drop_lev Γ (ec::nil) succ=q') as H.
627 unfold drop_lev in H.
628 unfold mkDropFlags in H.
631 set (arrangeMap _ _ flatten_leveled_type q) as y.
638 set (mapOptionTree flatten_leveled_type (dropT (mkFlags (liftBoolFunc false (bnot ○ levelMatch (ec :: nil))) succ))) as q.
639 destruct (decide_tree_empty q); [ idtac | apply (Prelude_error "escapifying open code not yet supported") ].
643 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply AExch ].
644 set (fun z z' => @RLet Γ Δ z (mapOptionTree flatten_leveled_type q') t z' nil) as q''.
645 eapply nd_comp; [ idtac | apply RLet ].
647 eapply nd_comp; [ apply nd_rlecnac | idtac ].
651 eapply AComp; [ idtac | apply ACanR ].
653 apply (@arrangeCancelEmptyTree _ _ _ _ e).
657 eapply (@RVar Γ Δ t nil).
665 eapply decide_tree_empty.
668 set (dropT (mkFlags (liftBoolFunc false (bnot ○ levelMatch (ec :: nil))) succ)) as escapified.
669 destruct (decide_tree_empty escapified).
676 unfold mkDropFlags; simpl.
680 destruct (General.list_eq_dec h0 (ec :: nil)).
696 apply (Prelude_error "escapifying code with multi-leaf antecedents is not supported").
700 Lemma unlev_relev : forall {Γ}(t:Tree ??(HaskType Γ ★)) lev, mapOptionTree unlev (t @@@ lev) = t.
703 destruct a; reflexivity.
704 rewrite <- IHt1 at 2.
705 rewrite <- IHt2 at 2.
709 Lemma tree_of_nothing : forall Γ ec t,
710 Arrange (mapOptionTree flatten_leveled_type (drop_lev(Γ:=Γ) (ec :: nil) (t @@@ (ec :: nil)))) [].
712 induction t; try destruct o; try destruct a.
719 eapply AComp; [ idtac | apply ACanL ].
720 eapply AComp; [ idtac | eapply ALeft; apply IHt2 ].
723 Transparent drop_lev.
730 Lemma tree_of_nothing' : forall Γ ec t,
731 Arrange [] (mapOptionTree flatten_leveled_type (drop_lev(Γ:=Γ) (ec :: nil) (t @@@ (ec :: nil)))).
733 induction t; try destruct o; try destruct a.
740 eapply AComp; [ apply AuCanL | idtac ].
741 eapply AComp; [ eapply ARight; apply IHt1 | idtac ].
744 Transparent drop_lev.
751 Lemma krunk : forall Γ (ec:HaskTyVar Γ ECKind) t,
752 flatten_type (<[ ec |- t ]>)
754 (mapOptionTree flatten_type (take_arg_types_as_tree t))
755 [ flatten_type (drop_arg_types_as_tree t)].
757 unfold flatten_type at 1.
760 apply phoas_extensionality.
765 rewrite <- mapOptionTree_compose.
766 unfold take_arg_types_as_tree.
768 replace (flatten_type (drop_arg_types_as_tree t) tv ite)
769 with (drop_arg_types (flatten_rawtype (t tv ite))).
770 replace (unleaves_ (take_arg_types (flatten_rawtype (t tv ite))))
771 with ((mapOptionTree (fun x : HaskType Γ ★ => flatten_type x tv ite)
773 (take_trustme (count_arg_types (t (fun _ : Kind => unit) (ite_unit Γ)))
774 (fun TV : Kind → Type => take_arg_types ○ t TV))))).
783 Lemma drop_to_nothing : forall (Γ:TypeEnv) Σ (lev:HaskLevel Γ),
784 drop_lev lev (Σ @@@ lev) = mapTree (fun _ => None) (mapTree (fun _ => tt) Σ).
798 Definition flatten_skolemized_proof :
801 ND Rule (mapOptionTree (flatten_judgment ) h) (mapOptionTree (flatten_judgment ) c).
803 eapply nd_map'; [ idtac | apply X ].
809 (match X as R in SRule H C with
810 | SBrak Γ Δ t ec succ lev => let case_SBrak := tt in _
811 | SEsc Γ Δ t ec succ lev => let case_SEsc := tt in _
812 | SFlat h c r => let case_SFlat := tt in _
816 refine (match r as R in Rule H C with
817 | RArrange Γ Δ a b x l d => let case_RArrange := tt in _
818 | RNote Γ Δ Σ τ l n => let case_RNote := tt in _
819 | RLit Γ Δ l _ => let case_RLit := tt in _
820 | RVar Γ Δ σ lev => let case_RVar := tt in _
821 | RGlobal Γ Δ σ l wev => let case_RGlobal := tt in _
822 | RLam Γ Δ Σ tx te lev => let case_RLam := tt in _
823 | RCast Γ Δ Σ σ τ lev γ => let case_RCast := tt in _
824 | RAbsT Γ Δ Σ κ σ lev => let case_RAbsT := tt in _
825 | RAppT Γ Δ Σ κ σ τ lev => let case_RAppT := tt in _
826 | RAppCo Γ Δ Σ κ σ₁ σ₂ γ σ lev => let case_RAppCo := tt in _
827 | RAbsCo Γ Δ Σ κ σ σ₁ σ₂ lev => let case_RAbsCo := tt in _
828 | RApp Γ Δ Σ₁ Σ₂ tx te lev => let case_RApp := tt in _
829 | RCut Γ Δ Σ Σ₁ Σ₁₂ Σ₂ Σ₃ l => let case_RCut := tt in _
830 | RLeft Γ Δ Σ₁ Σ₂ Σ l => let case_RLeft := tt in _
831 | RRight Γ Δ Σ₁ Σ₂ Σ l => let case_RRight := tt in _
832 | RVoid _ _ l => let case_RVoid := tt in _
833 | RBrak Γ Δ t ec succ lev => let case_RBrak := tt in _
834 | REsc Γ Δ t ec succ lev => let case_REsc := tt in _
835 | RCase Γ Δ lev tc Σ avars tbranches alts => let case_RCase := tt in _
836 | RLetRec Γ Δ lri x y t => let case_RLetRec := tt in _
839 destruct case_RArrange.
840 apply (flatten_arrangement'' Γ Δ a b x _ d).
843 apply (Prelude_error "found unskolemized Brak rule; this shouldn't happen").
846 apply (Prelude_error "found unskolemized Esc rule; this shouldn't happen").
851 apply nd_rule; apply RNote; auto.
852 apply nd_rule; apply RNote; auto.
857 unfold flatten_leveled_type.
859 rewrite literal_types_unchanged.
860 apply nd_rule; apply RLit.
861 unfold take_lev; simpl.
862 unfold drop_lev; simpl.
864 rewrite literal_types_unchanged.
868 Opaque flatten_judgment.
870 Transparent flatten_judgment.
872 unfold flatten_judgment.
874 apply nd_rule. apply RVar.
875 repeat drop_simplify.
876 repeat take_simplify.
880 destruct case_RGlobal.
884 destruct l as [|ec lev]; simpl.
886 destruct (eqd_dec (g:CoreVar) (hetmet_flatten:CoreVar)).
887 set (flatten_type (g wev)) as t.
888 set (RGlobal _ Δ nil (mkGlobal Γ t hetmet_id)) as q.
893 destruct (eqd_dec (g:CoreVar) (hetmet_unflatten:CoreVar)).
894 set (flatten_type (g wev)) as t.
895 set (RGlobal _ Δ nil (mkGlobal Γ t hetmet_id)) as q.
901 unfold flatten_leveled_type. simpl.
902 apply nd_rule; rewrite globals_do_not_have_code_types.
904 apply (Prelude_error "found RGlobal at depth >0; globals should never appear inside code brackets unless escaped").
910 destruct lev as [|ec lev]; simpl; [ apply nd_rule; apply RLam; auto | idtac ].
911 repeat drop_simplify.
912 repeat take_simplify.
924 destruct lev as [|ec lev]; simpl; [ apply nd_rule; apply RCast; auto | idtac ].
926 apply flatten_coercion; auto.
927 apply (Prelude_error "RCast at level >0; casting inside of code brackets is currently not supported").
932 destruct lev as [|ec lev].
933 unfold flatten_type at 1.
938 repeat drop_simplify.
939 repeat take_simplify.
940 rewrite mapOptionTree_distributes.
941 set (mapOptionTree (flatten_leveled_type ) (drop_lev (ec :: lev) Σ₁)) as Σ₁'.
942 set (mapOptionTree (flatten_leveled_type ) (drop_lev (ec :: lev) Σ₂)) as Σ₂'.
943 set (take_lev (ec :: lev) Σ₁) as Σ₁''.
944 set (take_lev (ec :: lev) Σ₂) as Σ₂''.
945 replace (flatten_type (tx ---> te)) with ((flatten_type tx) ---> (flatten_type te)).
946 apply (Prelude_error "FIXME: ga_apply").
950 Notation "` x" := (take_lev _ x).
951 Notation "`` x" := (mapOptionTree unlev x) (at level 20).
952 Notation "``` x" := ((drop_lev _ x)) (at level 20).
953 Notation "!<[]> x" := (flatten_type _ x) (at level 1).
954 Notation "!<[@]> x" := (mapOptionTree flatten_leveled_type x) (at level 1).
959 destruct l as [|ec lev]; simpl.
961 replace (mapOptionTree flatten_leveled_type (Σ₁₂ @@@ nil)) with (mapOptionTree flatten_type Σ₁₂ @@@ nil).
963 induction Σ₁₂; try destruct a; auto.
968 simpl; repeat drop_simplify.
969 simpl; repeat take_simplify.
971 set (drop_lev (ec :: lev) (Σ₁₂ @@@ (ec :: lev))) as x1.
973 rewrite mapOptionTree_compose.
974 rewrite mapOptionTree_compose.
975 rewrite mapOptionTree_compose.
976 rewrite mapOptionTree_compose.
978 rewrite <- mapOptionTree_compose.
979 rewrite <- mapOptionTree_compose.
980 rewrite <- mapOptionTree_compose.
981 eapply nd_comp; [ idtac | eapply nd_rule; eapply RCut ].
990 rewrite drop_to_nothing.
991 apply arrangeCancelEmptyTree with (q:=(mapTree (fun _ : ??(HaskType Γ ★) => tt) Σ₁₂)).
992 induction Σ₁₂; try destruct a; auto.
994 rewrite <- IHΣ₁₂1 at 2.
995 rewrite <- IHΣ₁₂2 at 2.
997 eapply nd_comp; [ eapply nd_rule; eapply RArrange; eapply ALeft; eapply ACanL | idtac ].
998 set (mapOptionTree flatten_type Σ₁₂) as a.
999 set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) Σ₁)) as b.
1000 set (mapOptionTree flatten_leveled_type (drop_lev (ec :: lev) Σ₂)) as c.
1001 set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) Σ₂)) as d.
1002 set (mapOptionTree flatten_leveled_type (drop_lev (ec :: lev) Σ)) as e.
1003 set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) Σ)) as f.
1004 eapply nd_comp; [ idtac | eapply nd_rule; eapply RCut ].
1005 eapply nd_comp; [ apply nd_llecnac | idtac ].
1010 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ALeft; eapply AExch ].
1011 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AuAssoc ].
1015 destruct case_RLeft.
1017 destruct l as [|ec lev].
1019 replace (mapOptionTree flatten_leveled_type (Σ @@@ nil)) with (mapOptionTree flatten_type Σ @@@ nil).
1022 induction Σ; try destruct a; auto.
1027 repeat drop_simplify.
1028 rewrite drop_to_nothing.
1035 apply arrangeUnCancelEmptyTree with (q:=(mapTree (fun _ : ??(HaskType Γ ★) => tt) Σ)).
1036 induction Σ; try destruct a; auto.
1038 rewrite <- IHΣ1 at 2.
1039 rewrite <- IHΣ2 at 2.
1042 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AuCanL ].
1046 replace (take_lev (ec :: lev) (Σ @@@ (ec :: lev))) with (Σ @@@ (ec::lev)).
1047 rewrite mapOptionTree_compose.
1048 rewrite mapOptionTree_compose.
1049 rewrite unlev_relev.
1051 rewrite take_lemma'.
1054 destruct case_RRight.
1056 destruct l as [|ec lev].
1058 replace (mapOptionTree flatten_leveled_type (Σ @@@ nil)) with (mapOptionTree flatten_type Σ @@@ nil).
1061 induction Σ; try destruct a; auto.
1066 repeat drop_simplify.
1067 rewrite drop_to_nothing.
1074 apply arrangeUnCancelEmptyTree with (q:=(mapTree (fun _ : ??(HaskType Γ ★) => tt) Σ)).
1075 induction Σ; try destruct a; auto.
1077 rewrite <- IHΣ1 at 2.
1078 rewrite <- IHΣ2 at 2.
1081 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AuCanR ].
1085 replace (take_lev (ec :: lev) (Σ @@@ (ec :: lev))) with (Σ @@@ (ec::lev)).
1086 rewrite mapOptionTree_compose.
1087 rewrite mapOptionTree_compose.
1088 rewrite unlev_relev.
1090 rewrite take_lemma'.
1093 destruct case_RVoid.
1103 destruct case_RAppT.
1104 simpl. destruct lev; simpl.
1105 unfold flatten_leveled_type.
1107 rewrite flatten_commutes_with_HaskTAll.
1108 rewrite flatten_commutes_with_substT.
1113 apply (Prelude_error "found type application at level >0; this is not supported").
1115 destruct case_RAbsT.
1116 simpl. destruct lev; simpl.
1117 rewrite flatten_commutes_with_HaskTAll.
1118 rewrite flatten_commutes_with_HaskTApp.
1119 eapply nd_comp; [ idtac | eapply nd_rule; eapply RAbsT ].
1121 set (mapOptionTree (flatten_leveled_type ) (mapOptionTree (weakLT(κ:=κ)) Σ)) as a.
1122 set (mapOptionTree (weakLT(κ:=κ)) (mapOptionTree (flatten_leveled_type ) Σ)) as q'.
1130 rewrite flatten_commutes_with_weakLT.
1141 apply (Prelude_error "found type abstraction at level >0; this is not supported").
1143 destruct case_RAppCo.
1144 simpl. destruct lev; simpl.
1145 unfold flatten_type.
1149 apply flatten_coercion.
1151 apply (Prelude_error "found coercion application at level >0; this is not supported").
1153 destruct case_RAbsCo.
1154 simpl. destruct lev; simpl.
1155 unfold flatten_type.
1157 apply (Prelude_error "AbsCo not supported (FIXME)").
1158 apply (Prelude_error "found coercion abstraction at level >0; this is not supported").
1160 destruct case_RLetRec.
1162 simpl. destruct lev; simpl.
1164 set (@RLetRec Γ Δ (mapOptionTree flatten_leveled_type lri) (flatten_type x) (mapOptionTree flatten_type y) nil) as q.
1165 replace (mapOptionTree flatten_leveled_type (y @@@ nil)) with (mapOptionTree flatten_type y @@@ nil).
1167 induction y; try destruct a; auto.
1172 repeat drop_simplify.
1173 repeat take_simplify.
1175 rewrite drop_to_nothing.
1181 apply arrangeCancelEmptyTree with (q:=y).
1182 induction y; try destruct a; auto.
1188 rewrite take_lemma'.
1189 set (mapOptionTree (flatten_type ○ unlev) (take_lev (h :: lev) lri)) as lri'.
1190 set (mapOptionTree flatten_leveled_type (drop_lev (h :: lev) lri)) as lri''.
1191 replace (mapOptionTree (flatten_type ○ unlev) (y @@@ (h :: lev))) with (mapOptionTree flatten_type y).
1194 rewrite <- mapOptionTree_compose.
1198 destruct case_RCase.
1200 apply (Prelude_error "Case not supported (BIG FIXME)").
1202 destruct case_SBrak.
1206 set (drop_lev (ec :: nil) (take_arg_types_as_tree t @@@ (ec :: nil))) as empty_tree.
1208 rewrite take_lemma'.
1210 rewrite mapOptionTree_compose.
1211 rewrite mapOptionTree_compose.
1212 rewrite unlev_relev.
1213 rewrite <- mapOptionTree_compose.
1216 set (mapOptionTree flatten_leveled_type (drop_lev (ec :: nil) succ)) as succ_host.
1217 set (mapOptionTree (flatten_type ○ unlev)(take_lev (ec :: nil) succ)) as succ_guest.
1218 set (mapOptionTree flatten_type (take_arg_types_as_tree t)) as succ_args.
1220 eapply nd_comp; [ eapply nd_rule; eapply RArrange; eapply ALeft; apply tree_of_nothing | idtac ].
1221 eapply nd_comp; [ eapply nd_rule; eapply RArrange; eapply ACanR | idtac ].
1222 refine (ga_unkappa Γ Δ (v2t ec) nil _ _ _ _ ;; _).
1223 eapply nd_comp; [ idtac | eapply arrange_brak ].
1229 apply (Prelude_error "found Brak at depth >0 indicating 3-level code; only two-level code is currently supported").
1235 unfold flatten_leveled_type at 2.
1238 rewrite mapOptionTree_compose.
1242 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ALeft; apply tree_of_nothing' ].
1243 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ACanR ].
1245 rewrite take_lemma'.
1246 rewrite unlev_relev.
1247 rewrite <- mapOptionTree_compose.
1248 eapply nd_comp; [ apply (arrange_esc _ _ ec) | idtac ].
1250 set (decide_tree_empty (take_lev (ec :: nil) succ)) as q'.
1256 set (mapOptionTree flatten_leveled_type (drop_lev (ec :: nil) succ)) as succ_host.
1257 set (mapOptionTree flatten_type (take_arg_types_as_tree t)) as succ_args.
1259 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply AuCanR ].
1260 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply AuCanR ].
1261 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply ACanL ].
1262 eapply nd_comp; [ idtac | eapply RLet ].
1263 eapply nd_comp; [ apply nd_llecnac | idtac ].
1264 apply nd_prod; [ idtac | eapply boost ].
1267 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ACanL ].
1275 refine ( _ ;; (boost _ _ _ _ _ (postcompose _ _ _ _ _ _ _ _))).
1283 refine ( _ ;; (boost _ _ _ _ _ (postcompose _ _ _ _ _ _ _ _))).
1285 refine ( _ ;; (boost _ _ _ _ _ (postcompose _ _ _ _ _ _ _ _))).
1291 (* environment has non-empty leaves *)
1292 apply (Prelude_error "ga_kappa not supported yet (BIG FIXME)").
1294 (* nesting too deep *)
1295 apply (Prelude_error "found Esc at depth >0 indicating 3-level code; only two-level code is currently supported").
1298 Definition flatten_proof :
1302 apply (Prelude_error "sorry, non-skolemized flattening isn't implemented").
1305 Definition skolemize_and_flatten_proof :
1309 (mapOptionTree (flatten_judgment ○ skolemize_judgment) h)
1310 (mapOptionTree (flatten_judgment ○ skolemize_judgment) c).
1312 rewrite mapOptionTree_compose.
1313 rewrite mapOptionTree_compose.
1314 apply flatten_skolemized_proof.
1315 apply skolemize_proof.
1320 (* to do: establish some metric on judgments (max length of level of any succedent type, probably), show how to
1321 * calculate it, and show that the flattening procedure above drives it down by one *)
1324 Instance FlatteningFunctor {Γ}{Δ}{ec} : Functor (JudgmentsL (PCF Γ Δ ec)) (TypesL (SystemFCa Γ Δ)) (obact) :=
1325 { fmor := FlatteningFunctor_fmor }.
1327 Definition ReificationFunctor Γ Δ : Functor (JudgmentsL _ _ (PCF n Γ Δ)) SystemFCa' (mapOptionTree brakifyJudg).
1328 refine {| fmor := ReificationFunctor_fmor Γ Δ |}; unfold hom; unfold ob; simpl ; intros.
1330 Definition PCF_SMME (n:nat)(Γ:TypeEnv)(Δ:CoercionEnv Γ) : ProgrammingLanguageSMME.
1331 refine {| plsmme_pl := PCF n Γ Δ |}.
1334 Definition SystemFCa_SMME (n:nat)(Γ:TypeEnv)(Δ:CoercionEnv Γ) : ProgrammingLanguageSMME.
1335 refine {| plsmme_pl := SystemFCa n Γ Δ |}.
1338 Definition ReificationFunctorMonoidal n : MonoidalFunctor (JudgmentsN n) (JudgmentsN (S n)) (ReificationFunctor n).
1342 Definition PCF_SystemFCa_two_level n Γ Δ : TwoLevelLanguage (PCF_SMME n Γ Δ) (SystemFCa_SMME (S n) Γ Δ).
1345 (* ... and the retraction exists *)
1349 Implicit Arguments garrow [ ].