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 (hetmet_flatten : WeakExprVar).
165 Context (hetmet_unflatten : WeakExprVar).
166 Context (hetmet_id : WeakExprVar).
167 Context {unitTy : forall TV, RawHaskType TV ECKind -> RawHaskType TV ★ }.
168 Context {prodTy : forall TV, RawHaskType TV ECKind -> RawHaskType TV ★ -> RawHaskType TV ★ -> RawHaskType TV ★ }.
169 Context {gaTy : forall TV, RawHaskType TV ECKind -> RawHaskType TV ★ -> RawHaskType TV ★ -> RawHaskType TV ★ }.
171 Definition ga_mk_tree' {TV}(ec:RawHaskType TV ECKind)(tr:Tree ??(RawHaskType TV ★)) : RawHaskType TV ★ :=
172 reduceTree (unitTy TV ec) (prodTy TV ec) tr.
174 Definition ga_mk_tree {Γ}(ec:HaskType Γ ECKind)(tr:Tree ??(HaskType Γ ★)) : HaskType Γ ★ :=
175 fun TV ite => ga_mk_tree' (ec TV ite) (mapOptionTree (fun x => x TV ite) tr).
177 Definition ga_mk_raw {TV}(ec:RawHaskType TV ECKind)(ant suc:Tree ??(RawHaskType TV ★)) : RawHaskType TV ★ :=
180 (ga_mk_tree' ec suc).
182 Definition ga_mk {Γ}(ec:HaskType Γ ECKind)(ant suc:Tree ??(HaskType Γ ★)) : HaskType Γ ★ :=
183 fun TV ite => gaTy TV (ec TV ite) (ga_mk_tree ec ant TV ite) (ga_mk_tree ec suc TV ite).
187 * - code types <[t]>@c become garrows c () t
188 * - free variables of type t at a level lev deeper than the succedent become garrows c () t
189 * - free variables at the level of the succedent become
191 Fixpoint flatten_rawtype {TV}{κ}(exp: RawHaskType TV κ) : RawHaskType TV κ :=
194 | TAll _ y => TAll _ (fun v => flatten_rawtype (y v))
195 | TApp _ _ x y => TApp (flatten_rawtype x) (flatten_rawtype y)
197 | TCoerc _ t1 t2 t => TCoerc (flatten_rawtype t1) (flatten_rawtype t2) (flatten_rawtype t)
199 | TCode ec e => let e' := flatten_rawtype e
200 in ga_mk_raw ec (unleaves_ (take_arg_types e')) [drop_arg_types e']
201 | TyFunApp tfc kl k lt => TyFunApp tfc kl k (flatten_rawtype_list _ lt)
203 with flatten_rawtype_list {TV}(lk:list Kind)(exp:@RawHaskTypeList TV lk) : @RawHaskTypeList TV lk :=
204 match exp in @RawHaskTypeList _ LK return @RawHaskTypeList TV LK with
205 | TyFunApp_nil => TyFunApp_nil
206 | TyFunApp_cons κ kl t rest => TyFunApp_cons _ _ (flatten_rawtype t) (flatten_rawtype_list _ rest)
209 Definition flatten_type {Γ}{κ}(ht:HaskType Γ κ) : HaskType Γ κ :=
210 fun TV ite => flatten_rawtype (ht TV ite).
212 Fixpoint levels_to_tcode {Γ}(ht:HaskType Γ ★)(lev:HaskLevel Γ) : HaskType Γ ★ :=
214 | nil => flatten_type ht
215 | ec::lev' => @ga_mk _ (v2t ec) [] [levels_to_tcode ht lev']
218 Definition flatten_leveled_type {Γ}(ht:LeveledHaskType Γ ★) : LeveledHaskType Γ ★ :=
219 levels_to_tcode (unlev ht) (getlev ht) @@ nil.
223 Axiom literal_types_unchanged : forall Γ l, flatten_type (literalType l) = literalType(Γ:=Γ) l.
225 Axiom flatten_coercion : forall Γ Δ κ (σ τ:HaskType Γ κ) (γ:HaskCoercion Γ Δ (σ ∼∼∼ τ)),
226 HaskCoercion Γ Δ (flatten_type σ ∼∼∼ flatten_type τ).
228 Axiom flatten_commutes_with_substT :
229 forall κ Γ (Δ:CoercionEnv Γ) (σ:∀ TV, InstantiatedTypeEnv TV Γ → TV κ → RawHaskType TV ★) (τ:HaskType Γ κ),
230 flatten_type (substT σ τ) = substT (fun TV ite v => flatten_rawtype (σ TV ite v))
233 Axiom flatten_commutes_with_HaskTAll :
234 forall κ Γ (Δ:CoercionEnv Γ) (σ:∀ TV, InstantiatedTypeEnv TV Γ → TV κ → RawHaskType TV ★),
235 flatten_type (HaskTAll κ σ) = HaskTAll κ (fun TV ite v => flatten_rawtype (σ TV ite v)).
237 Axiom flatten_commutes_with_HaskTApp :
238 forall κ Γ (Δ:CoercionEnv Γ) (σ:∀ TV, InstantiatedTypeEnv TV Γ → TV κ → RawHaskType TV ★),
239 flatten_type (HaskTApp (weakF σ) (FreshHaskTyVar κ)) =
240 HaskTApp (weakF (fun TV ite v => flatten_rawtype (σ TV ite v))) (FreshHaskTyVar κ).
242 Axiom flatten_commutes_with_weakLT : forall (Γ:TypeEnv) κ t,
243 flatten_leveled_type (weakLT(Γ:=Γ)(κ:=κ) t) = weakLT(Γ:=Γ)(κ:=κ) (flatten_leveled_type t).
245 Axiom globals_do_not_have_code_types : forall (Γ:TypeEnv) (g:Global Γ) v,
246 flatten_type (g v) = g v.
248 (* "n" is the maximum depth remaining AFTER flattening *)
249 Definition flatten_judgment (j:Judg) :=
250 match j as J return Judg with
251 | Γ > Δ > ant |- suc @ nil => Γ > Δ > mapOptionTree flatten_leveled_type ant
252 |- mapOptionTree flatten_type suc @ nil
253 | Γ > Δ > ant |- suc @ (ec::lev') => Γ > Δ > mapOptionTree flatten_leveled_type (drop_lev (ec::lev') ant)
255 (mapOptionTree (flatten_type ○ unlev) (take_lev (ec::lev') ant))
256 (mapOptionTree flatten_type suc )
261 { ga_id : ∀ Γ Δ ec l a , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec a a ]@l ]
262 ; ga_cancelr : ∀ Γ Δ ec l a , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec (a,,[]) a ]@l ]
263 ; ga_cancell : ∀ Γ Δ ec l a , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec ([],,a) a ]@l ]
264 ; ga_uncancelr : ∀ Γ Δ ec l a , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec a (a,,[]) ]@l ]
265 ; ga_uncancell : ∀ Γ Δ ec l a , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec a ([],,a) ]@l ]
266 ; ga_assoc : ∀ Γ Δ ec l a b c, ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec ((a,,b),,c) (a,,(b,,c)) ]@l ]
267 ; ga_unassoc : ∀ Γ Δ ec l a b c, ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec (a,,(b,,c)) ((a,,b),,c) ]@l ]
268 ; ga_swap : ∀ Γ Δ ec l a b , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec (a,,b) (b,,a) ]@l ]
269 ; ga_drop : ∀ Γ Δ ec l a , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec a [] ]@l ]
270 ; ga_copy : ∀ Γ Δ ec l a , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec a (a,,a) ]@l ]
271 ; ga_first : ∀ Γ Δ ec l a b x, ND Rule [] [Γ > Δ > [@ga_mk Γ ec a b @@l] |- [@ga_mk Γ ec (a,,x) (b,,x) ]@l ]
272 ; ga_second : ∀ Γ Δ ec l a b x, ND Rule [] [Γ > Δ > [@ga_mk Γ ec a b @@l] |- [@ga_mk Γ ec (x,,a) (x,,b) ]@l ]
273 ; ga_lit : ∀ Γ Δ ec l lit , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec [] [literalType lit] ]@l ]
274 ; ga_curry : ∀ Γ Δ ec l a b c, ND Rule [] [Γ > Δ > [@ga_mk Γ ec (a,,[b]) [c] @@ l] |- [@ga_mk Γ ec a [b ---> c] ]@ l ]
275 ; ga_loopl : ∀ Γ Δ ec l x y z, ND Rule [] [Γ > Δ > [@ga_mk Γ ec (z,,x) (z,,y) @@ l] |- [@ga_mk Γ ec x y ]@ l ]
276 ; ga_loopr : ∀ Γ Δ ec l x y z, ND Rule [] [Γ > Δ > [@ga_mk Γ ec (x,,z) (y,,z) @@ l] |- [@ga_mk Γ ec x y ]@ l ]
277 ; 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 ]
278 ; ga_apply : ∀ Γ Δ ec l a a' b c,
279 ND Rule [] [Γ > Δ > [@ga_mk Γ ec a [b ---> c] @@ l],,[@ga_mk Γ ec a' [b] @@ l] |- [@ga_mk Γ ec (a,,a') [c] ]@l ]
280 ; ga_kappa : ∀ Γ Δ ec l a b Σ, ND Rule
281 [Γ > Δ > Σ,,[@ga_mk Γ ec [] a @@ l] |- [@ga_mk Γ ec [] b ]@l ]
282 [Γ > Δ > Σ |- [@ga_mk Γ ec a b ]@l ]
284 Context `(gar:garrow).
286 Notation "a ~~~~> b" := (@ga_mk _ _ a b) (at level 20).
288 Definition boost : forall Γ Δ ant x y {lev},
289 ND Rule [] [ Γ > Δ > [x@@lev] |- [y]@lev ] ->
290 ND Rule [ Γ > Δ > ant |- [x]@lev ] [ Γ > Δ > ant |- [y]@lev ].
292 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ACanR ].
293 eapply nd_comp; [ idtac | apply RLet ].
294 eapply nd_comp; [ apply nd_rlecnac | idtac ].
304 Definition precompose Γ Δ ec : forall a x y z lev,
306 [ Γ > Δ > a |- [@ga_mk _ ec y z ]@lev ]
307 [ Γ > Δ > a,,[@ga_mk _ ec x y @@ lev] |- [@ga_mk _ ec x z ]@lev ].
309 eapply nd_comp; [ idtac | eapply RLet ].
310 eapply nd_comp; [ apply nd_rlecnac | idtac ].
313 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AExch ].
317 Definition precompose' Γ Δ ec : forall a b x y z lev,
319 [ Γ > Δ > a,,b |- [@ga_mk _ ec y z ]@lev ]
320 [ Γ > Δ > a,,([@ga_mk _ ec x y @@ lev],,b) |- [@ga_mk _ ec x z ]@lev ].
322 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ALeft; eapply AExch ].
323 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AuAssoc ].
327 Definition postcompose_ Γ Δ ec : forall a x y z lev,
329 [ Γ > Δ > a |- [@ga_mk _ ec x y ]@lev ]
330 [ Γ > Δ > a,,[@ga_mk _ ec y z @@ lev] |- [@ga_mk _ ec x z ]@lev ].
332 eapply nd_comp; [ idtac | eapply RLet ].
333 eapply nd_comp; [ apply nd_rlecnac | idtac ].
339 Definition postcompose Γ Δ ec : forall x y z lev,
340 ND Rule [] [ Γ > Δ > [] |- [@ga_mk _ ec x y ]@lev ] ->
341 ND Rule [] [ Γ > Δ > [@ga_mk _ ec y z @@ lev] |- [@ga_mk _ ec x z ]@lev ].
343 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ACanL ].
344 eapply nd_comp; [ idtac | eapply postcompose_ ].
348 Definition first_nd : ∀ Γ Δ ec lev a b c Σ,
349 ND Rule [ Γ > Δ > Σ |- [@ga_mk Γ ec a b ]@lev ]
350 [ Γ > Δ > Σ |- [@ga_mk Γ ec (a,,c) (b,,c) ]@lev ].
352 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ACanR ].
353 eapply nd_comp; [ idtac | apply RLet ].
354 eapply nd_comp; [ apply nd_rlecnac | idtac ].
357 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AuCanR ].
361 Definition firstify : ∀ Γ Δ ec lev a b c Σ,
362 ND Rule [] [ Γ > Δ > Σ |- [@ga_mk Γ ec a b ]@lev ] ->
363 ND Rule [] [ Γ > Δ > Σ |- [@ga_mk Γ ec (a,,c) (b,,c) ]@lev ].
370 Definition second_nd : ∀ Γ Δ ec lev a b c Σ,
372 [ Γ > Δ > Σ |- [@ga_mk Γ ec a b ]@lev ]
373 [ Γ > Δ > Σ |- [@ga_mk Γ ec (c,,a) (c,,b) ]@lev ].
375 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ACanR ].
376 eapply nd_comp; [ idtac | apply RLet ].
377 eapply nd_comp; [ apply nd_rlecnac | idtac ].
380 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AuCanR ].
384 Definition secondify : ∀ Γ Δ ec lev a b c Σ,
385 ND Rule [] [ Γ > Δ > Σ |- [@ga_mk Γ ec a b ]@lev ] ->
386 ND Rule [] [ Γ > Δ > Σ |- [@ga_mk Γ ec (c,,a) (c,,b) ]@lev ].
393 Lemma ga_unkappa : ∀ Γ Δ ec l a b Σ x,
395 [Γ > Δ > Σ |- [@ga_mk Γ ec (a,,x) b ]@l ]
396 [Γ > Δ > Σ,,[@ga_mk Γ ec [] a @@ l] |- [@ga_mk Γ ec x b ]@l ].
398 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AExch ].
399 eapply nd_comp; [ idtac | eapply RLet ].
400 eapply nd_comp; [ apply nd_llecnac | idtac ].
404 eapply nd_comp; [ idtac | eapply RLet ].
405 eapply nd_comp; [ apply nd_llecnac | idtac ].
409 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AExch ].
413 (* useful for cutting down on the pretty-printed noise
415 Notation "` x" := (take_lev _ x) (at level 20).
416 Notation "`` x" := (mapOptionTree unlev x) (at level 20).
417 Notation "``` x" := (drop_lev _ x) (at level 20).
419 Definition flatten_arrangement' :
420 forall Γ (Δ:CoercionEnv Γ)
421 (ec:HaskTyVar Γ ECKind) (lev:HaskLevel Γ) (ant1 ant2:Tree ??(LeveledHaskType Γ ★)) (r:Arrange ant1 ant2),
422 ND Rule [] [Γ > Δ > [] |- [@ga_mk _ (v2t ec) (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) ant2))
423 (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) ant1)) ]@nil ].
426 refine (fix flatten ant1 ant2 (r:Arrange ant1 ant2):
427 ND Rule [] [Γ > Δ > [] |- [@ga_mk _ (v2t ec)
428 (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) ant2))
429 (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) ant1)) ]@nil] :=
430 match r as R in Arrange A B return
431 ND Rule [] [Γ > Δ > [] |- [@ga_mk _ (v2t ec)
432 (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) B))
433 (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) A)) ]@nil]
435 | AId a => let case_AId := tt in ga_id _ _ _ _ _
436 | ACanL a => let case_ACanL := tt in ga_uncancell _ _ _ _ _
437 | ACanR a => let case_ACanR := tt in ga_uncancelr _ _ _ _ _
438 | AuCanL a => let case_AuCanL := tt in ga_cancell _ _ _ _ _
439 | AuCanR a => let case_AuCanR := tt in ga_cancelr _ _ _ _ _
440 | AAssoc a b c => let case_AAssoc := tt in ga_assoc _ _ _ _ _ _ _
441 | AuAssoc a b c => let case_AuAssoc := tt in ga_unassoc _ _ _ _ _ _ _
442 | AExch a b => let case_AExch := tt in ga_swap _ _ _ _ _ _
443 | AWeak a => let case_AWeak := tt in ga_drop _ _ _ _ _
444 | ACont a => let case_ACont := tt in ga_copy _ _ _ _ _
445 | ALeft a b c r' => let case_ALeft := tt in flatten _ _ r' ;; boost _ _ _ _ _ (ga_second _ _ _ _ _ _ _)
446 | ARight a b c r' => let case_ARight := tt in flatten _ _ r' ;; boost _ _ _ _ _ (ga_first _ _ _ _ _ _ _)
447 | AComp c b a r1 r2 => let case_AComp := tt in (fun r1' r2' => _) (flatten _ _ r1) (flatten _ _ r2)
448 end); clear flatten; repeat take_simplify; repeat drop_simplify; intros.
451 set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) a)) as a' in *.
452 set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) b)) as b' in *.
453 set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) c)) as c' in *.
454 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply ACanL ].
455 eapply nd_comp; [ idtac | apply
456 (@RLet Γ Δ [] [] (@ga_mk _ (v2t ec) a' b') (@ga_mk _ (v2t ec) a' c')) ].
457 eapply nd_comp; [ apply nd_llecnac | idtac ].
460 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply AuCanR ].
461 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply ACanL ].
462 eapply nd_comp; [ idtac | apply RLet ].
463 eapply nd_comp; [ apply nd_llecnac | idtac ].
466 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AExch ].
470 Definition flatten_arrangement :
471 forall Γ (Δ:CoercionEnv Γ) n
472 (ec:HaskTyVar Γ ECKind) (lev:HaskLevel Γ) (ant1 ant2:Tree ??(LeveledHaskType Γ ★)) (r:Arrange ant1 ant2) succ,
474 [Γ > Δ > mapOptionTree (flatten_leveled_type ) (drop_lev n ant1)
475 |- [@ga_mk _ (v2t ec)
476 (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) ant1))
477 (mapOptionTree (flatten_type ) succ) ]@nil]
478 [Γ > Δ > mapOptionTree (flatten_leveled_type ) (drop_lev n ant2)
479 |- [@ga_mk _ (v2t ec)
480 (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) ant2))
481 (mapOptionTree (flatten_type ) succ) ]@nil].
483 refine ( _ ;; (boost _ _ _ _ _ (postcompose _ _ _ _ _ _ _ (flatten_arrangement' Γ Δ ec lev ant1 ant2 r)))).
486 refine ((fix flatten ant1 ant2 (r:Arrange ant1 ant2) :=
487 match r as R in Arrange A B return
488 Arrange (mapOptionTree (flatten_leveled_type ) (drop_lev _ A))
489 (mapOptionTree (flatten_leveled_type ) (drop_lev _ B)) with
490 | AId a => let case_AId := tt in AId _
491 | ACanL a => let case_ACanL := tt in ACanL _
492 | ACanR a => let case_ACanR := tt in ACanR _
493 | AuCanL a => let case_AuCanL := tt in AuCanL _
494 | AuCanR a => let case_AuCanR := tt in AuCanR _
495 | AAssoc a b c => let case_AAssoc := tt in AAssoc _ _ _
496 | AuAssoc a b c => let case_AuAssoc := tt in AuAssoc _ _ _
497 | AExch a b => let case_AExch := tt in AExch _ _
498 | AWeak a => let case_AWeak := tt in AWeak _
499 | ACont a => let case_ACont := tt in ACont _
500 | ALeft a b c r' => let case_ALeft := tt in ALeft _ (flatten _ _ r')
501 | ARight a b c r' => let case_ARight := tt in ARight _ (flatten _ _ r')
502 | AComp a b c r1 r2 => let case_AComp := tt in AComp (flatten _ _ r1) (flatten _ _ r2)
503 end) ant1 ant2 r); clear flatten; repeat take_simplify; repeat drop_simplify; intros.
506 Definition flatten_arrangement'' :
507 forall Γ Δ ant1 ant2 succ l (r:Arrange ant1 ant2),
508 ND Rule (mapOptionTree (flatten_judgment ) [Γ > Δ > ant1 |- succ @ l])
509 (mapOptionTree (flatten_judgment ) [Γ > Δ > ant2 |- succ @ l]).
523 apply AExch. (* TO DO: check for all-leaf trees here *)
528 eapply AComp; [ apply IHr1 | apply IHr2 ].
530 apply flatten_arrangement.
534 Definition ga_join Γ Δ Σ₁ Σ₂ a b ec :
535 ND Rule [] [Γ > Δ > Σ₁ |- [@ga_mk _ ec [] a ]@nil] ->
536 ND Rule [] [Γ > Δ > Σ₂ |- [@ga_mk _ ec [] b ]@nil] ->
537 ND Rule [] [Γ > Δ > Σ₁,,Σ₂ |- [@ga_mk _ ec [] (a,,b) ]@nil].
540 apply secondify with (c:=a) in pfb.
541 apply firstify with (c:=[]) in pfa.
542 eapply nd_comp; [ idtac | eapply RLet ].
543 eapply nd_comp; [ eapply nd_llecnac | idtac ].
548 eapply nd_comp; [ idtac | eapply RLet ].
549 eapply nd_comp; [ apply nd_llecnac | idtac ].
551 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ACanL ].
552 eapply nd_comp; [ idtac | eapply postcompose_ ].
555 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AExch ].
556 eapply nd_comp; [ idtac | eapply precompose ].
560 Definition arrange_brak : forall Γ Δ ec succ t,
563 [(@ga_mk _ (v2t ec) [] (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: nil) succ))) @@ nil],,
564 mapOptionTree (flatten_leveled_type ) (drop_lev (ec :: nil) succ) |- [t]@nil]
565 [Γ > Δ > mapOptionTree (flatten_leveled_type ) succ |- [t]@nil].
569 set (@arrangeUnPartition _ succ (levelMatch (ec::nil))) as q.
570 set (arrangeMap _ _ flatten_leveled_type q) as y.
578 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AExch ].
580 eapply nd_comp; [ apply nd_llecnac | idtac ].
581 eapply nd_comp; [ idtac | eapply RLet ].
586 induction succ; try destruct a; simpl.
592 destruct l as [t' lev'].
593 destruct lev' as [|ec' lev'].
597 set (@eqd_dec (HaskLevel Γ) (haskLevelEqDecidable Γ) (ec' :: lev') (ec :: nil)) as q.
602 unfold flatten_leveled_type.
619 Definition arrange_esc : forall Γ Δ ec succ t,
621 [Γ > Δ > mapOptionTree (flatten_leveled_type ) succ |- [t]@nil]
623 [(@ga_mk _ (v2t ec) [] (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: nil) succ))) @@ nil],,
624 mapOptionTree (flatten_leveled_type ) (drop_lev (ec :: nil) succ) |- [t]@nil].
626 set (@arrangePartition _ succ (levelMatch (ec::nil))) as q.
627 set (@drop_lev Γ (ec::nil) succ) as q'.
628 assert (@drop_lev Γ (ec::nil) succ=q') as H.
630 unfold drop_lev in H.
631 unfold mkDropFlags in H.
634 set (arrangeMap _ _ flatten_leveled_type q) as y.
641 set (mapOptionTree flatten_leveled_type (dropT (mkFlags (liftBoolFunc false (bnot ○ levelMatch (ec :: nil))) succ))) as q.
642 destruct (decide_tree_empty q); [ idtac | apply (Prelude_error "escapifying open code not yet supported") ].
646 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply AExch ].
647 set (fun z z' => @RLet Γ Δ z (mapOptionTree flatten_leveled_type q') t z' nil) as q''.
648 eapply nd_comp; [ idtac | apply RLet ].
650 eapply nd_comp; [ apply nd_rlecnac | idtac ].
654 eapply AComp; [ idtac | apply ACanR ].
656 apply (@arrangeCancelEmptyTree _ _ _ _ e).
660 eapply (@RVar Γ Δ t nil).
668 eapply decide_tree_empty.
671 set (dropT (mkFlags (liftBoolFunc false (bnot ○ levelMatch (ec :: nil))) succ)) as escapified.
672 destruct (decide_tree_empty escapified).
679 unfold mkDropFlags; simpl.
683 destruct (General.list_eq_dec h0 (ec :: nil)).
699 apply (Prelude_error "escapifying code with multi-leaf antecedents is not supported").
703 Lemma unlev_relev : forall {Γ}(t:Tree ??(HaskType Γ ★)) lev, mapOptionTree unlev (t @@@ lev) = t.
706 destruct a; reflexivity.
707 rewrite <- IHt1 at 2.
708 rewrite <- IHt2 at 2.
712 Lemma tree_of_nothing : forall Γ ec t,
713 Arrange (mapOptionTree flatten_leveled_type (drop_lev(Γ:=Γ) (ec :: nil) (t @@@ (ec :: nil)))) [].
715 induction t; try destruct o; try destruct a.
722 eapply AComp; [ idtac | apply ACanL ].
723 eapply AComp; [ idtac | eapply ALeft; apply IHt2 ].
726 Transparent drop_lev.
733 Lemma tree_of_nothing' : forall Γ ec t,
734 Arrange [] (mapOptionTree flatten_leveled_type (drop_lev(Γ:=Γ) (ec :: nil) (t @@@ (ec :: nil)))).
736 induction t; try destruct o; try destruct a.
743 eapply AComp; [ apply AuCanL | idtac ].
744 eapply AComp; [ eapply ARight; apply IHt1 | idtac ].
747 Transparent drop_lev.
754 Lemma krunk : forall Γ (ec:HaskTyVar Γ ECKind) t,
755 flatten_type (<[ ec |- t ]>)
757 (mapOptionTree flatten_type (take_arg_types_as_tree t))
758 [ flatten_type (drop_arg_types_as_tree t)].
760 unfold flatten_type at 1.
763 apply phoas_extensionality.
768 rewrite <- mapOptionTree_compose.
769 unfold take_arg_types_as_tree.
771 replace (flatten_type (drop_arg_types_as_tree t) tv ite)
772 with (drop_arg_types (flatten_rawtype (t tv ite))).
773 replace (unleaves_ (take_arg_types (flatten_rawtype (t tv ite))))
774 with ((mapOptionTree (fun x : HaskType Γ ★ => flatten_type x tv ite)
776 (take_trustme (count_arg_types (t (fun _ : Kind => unit) (ite_unit Γ)))
777 (fun TV : Kind → Type => take_arg_types ○ t TV))))).
780 clear hetmet_flatten.
781 clear hetmet_unflatten.
789 Lemma drop_to_nothing : forall (Γ:TypeEnv) Σ (lev:HaskLevel Γ),
790 drop_lev lev (Σ @@@ lev) = mapTree (fun _ => None) (mapTree (fun _ => tt) Σ).
804 Definition flatten_skolemized_proof :
807 ND Rule (mapOptionTree (flatten_judgment ) h) (mapOptionTree (flatten_judgment ) c).
809 eapply nd_map'; [ idtac | apply X ].
815 (match X as R in SRule H C with
816 | SBrak Γ Δ t ec succ lev => let case_SBrak := tt in _
817 | SEsc Γ Δ t ec succ lev => let case_SEsc := tt in _
818 | SFlat h c r => let case_SFlat := tt in _
822 refine (match r as R in Rule H C with
823 | RArrange Γ Δ a b x l d => let case_RArrange := tt in _
824 | RNote Γ Δ Σ τ l n => let case_RNote := tt in _
825 | RLit Γ Δ l _ => let case_RLit := tt in _
826 | RVar Γ Δ σ lev => let case_RVar := tt in _
827 | RGlobal Γ Δ σ l wev => let case_RGlobal := tt in _
828 | RLam Γ Δ Σ tx te lev => let case_RLam := tt in _
829 | RCast Γ Δ Σ σ τ lev γ => let case_RCast := tt in _
830 | RAbsT Γ Δ Σ κ σ lev => let case_RAbsT := tt in _
831 | RAppT Γ Δ Σ κ σ τ lev => let case_RAppT := tt in _
832 | RAppCo Γ Δ Σ κ σ₁ σ₂ γ σ lev => let case_RAppCo := tt in _
833 | RAbsCo Γ Δ Σ κ σ σ₁ σ₂ lev => let case_RAbsCo := tt in _
834 | RApp Γ Δ Σ₁ Σ₂ tx te lev => let case_RApp := tt in _
835 | RCut Γ Δ Σ Σ₁ Σ₁₂ Σ₂ Σ₃ l => let case_RCut := tt in _
836 | RLeft Γ Δ Σ₁ Σ₂ Σ l => let case_RLeft := tt in _
837 | RRight Γ Δ Σ₁ Σ₂ Σ l => let case_RRight := tt in _
838 | RVoid _ _ l => let case_RVoid := tt in _
839 | RBrak Γ Δ t ec succ lev => let case_RBrak := tt in _
840 | REsc Γ Δ t ec succ lev => let case_REsc := tt in _
841 | RCase Γ Δ lev tc Σ avars tbranches alts => let case_RCase := tt in _
842 | RLetRec Γ Δ lri x y t => let case_RLetRec := tt in _
845 destruct case_RArrange.
846 apply (flatten_arrangement'' Γ Δ a b x _ d).
849 apply (Prelude_error "found unskolemized Brak rule; this shouldn't happen").
852 apply (Prelude_error "found unskolemized Esc rule; this shouldn't happen").
857 apply nd_rule; apply RNote; auto.
858 apply nd_rule; apply RNote; auto.
863 unfold flatten_leveled_type.
865 rewrite literal_types_unchanged.
866 apply nd_rule; apply RLit.
867 unfold take_lev; simpl.
868 unfold drop_lev; simpl.
870 rewrite literal_types_unchanged.
874 Opaque flatten_judgment.
876 Transparent flatten_judgment.
878 unfold flatten_judgment.
880 apply nd_rule. apply RVar.
881 repeat drop_simplify.
882 repeat take_simplify.
886 destruct case_RGlobal.
890 destruct l as [|ec lev]; simpl.
891 destruct (eqd_dec (g:CoreVar) (hetmet_flatten:CoreVar)).
892 set (flatten_type (g wev)) as t.
893 set (RGlobal _ Δ nil (mkGlobal Γ t hetmet_id)) as q.
898 destruct (eqd_dec (g:CoreVar) (hetmet_unflatten:CoreVar)).
899 set (flatten_type (g wev)) as t.
900 set (RGlobal _ Δ nil (mkGlobal Γ t hetmet_id)) as q.
905 unfold flatten_leveled_type. simpl.
906 apply nd_rule; rewrite globals_do_not_have_code_types.
908 apply (Prelude_error "found RGlobal at depth >0; globals should never appear inside code brackets unless escaped").
914 destruct lev as [|ec lev]; simpl; [ apply nd_rule; apply RLam; auto | idtac ].
915 repeat drop_simplify.
916 repeat take_simplify.
928 destruct lev as [|ec lev]; simpl; [ apply nd_rule; apply RCast; auto | idtac ].
930 apply flatten_coercion; auto.
931 apply (Prelude_error "RCast at level >0; casting inside of code brackets is currently not supported").
936 destruct lev as [|ec lev].
937 unfold flatten_type at 1.
942 repeat drop_simplify.
943 repeat take_simplify.
944 rewrite mapOptionTree_distributes.
945 set (mapOptionTree (flatten_leveled_type ) (drop_lev (ec :: lev) Σ₁)) as Σ₁'.
946 set (mapOptionTree (flatten_leveled_type ) (drop_lev (ec :: lev) Σ₂)) as Σ₂'.
947 set (take_lev (ec :: lev) Σ₁) as Σ₁''.
948 set (take_lev (ec :: lev) Σ₂) as Σ₂''.
949 replace (flatten_type (tx ---> te)) with ((flatten_type tx) ---> (flatten_type te)).
950 apply (Prelude_error "FIXME: ga_apply").
954 Notation "` x" := (take_lev _ x).
955 Notation "`` x" := (mapOptionTree unlev x) (at level 20).
956 Notation "``` x" := ((drop_lev _ x)) (at level 20).
957 Notation "!<[]> x" := (flatten_type _ x) (at level 1).
958 Notation "!<[@]> x" := (mapOptionTree flatten_leveled_type x) (at level 1).
963 destruct l as [|ec lev]; simpl.
965 replace (mapOptionTree flatten_leveled_type (Σ₁₂ @@@ nil)) with (mapOptionTree flatten_type Σ₁₂ @@@ nil).
967 induction Σ₁₂; try destruct a; auto.
972 simpl; repeat drop_simplify.
973 simpl; repeat take_simplify.
975 set (drop_lev (ec :: lev) (Σ₁₂ @@@ (ec :: lev))) as x1.
977 rewrite mapOptionTree_compose.
978 rewrite mapOptionTree_compose.
979 rewrite mapOptionTree_compose.
980 rewrite mapOptionTree_compose.
982 rewrite <- mapOptionTree_compose.
983 rewrite <- mapOptionTree_compose.
984 rewrite <- mapOptionTree_compose.
985 eapply nd_comp; [ idtac | eapply nd_rule; eapply RCut ].
994 rewrite drop_to_nothing.
995 apply arrangeCancelEmptyTree with (q:=(mapTree (fun _ : ??(HaskType Γ ★) => tt) Σ₁₂)).
996 induction Σ₁₂; try destruct a; auto.
998 rewrite <- IHΣ₁₂1 at 2.
999 rewrite <- IHΣ₁₂2 at 2.
1001 eapply nd_comp; [ eapply nd_rule; eapply RArrange; eapply ALeft; eapply ACanL | idtac ].
1002 set (mapOptionTree flatten_type Σ₁₂) as a.
1003 set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) Σ₁)) as b.
1004 set (mapOptionTree flatten_leveled_type (drop_lev (ec :: lev) Σ₂)) as c.
1005 set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) Σ₂)) as d.
1006 set (mapOptionTree flatten_leveled_type (drop_lev (ec :: lev) Σ)) as e.
1007 set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) Σ)) as f.
1008 eapply nd_comp; [ idtac | eapply nd_rule; eapply RCut ].
1009 eapply nd_comp; [ apply nd_llecnac | idtac ].
1014 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ALeft; eapply AExch ].
1015 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AuAssoc ].
1019 destruct case_RLeft.
1021 destruct l as [|ec lev].
1023 replace (mapOptionTree flatten_leveled_type (Σ @@@ nil)) with (mapOptionTree flatten_type Σ @@@ nil).
1026 induction Σ; try destruct a; auto.
1031 repeat drop_simplify.
1032 rewrite drop_to_nothing.
1039 apply arrangeUnCancelEmptyTree with (q:=(mapTree (fun _ : ??(HaskType Γ ★) => tt) Σ)).
1040 induction Σ; try destruct a; auto.
1042 rewrite <- IHΣ1 at 2.
1043 rewrite <- IHΣ2 at 2.
1046 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AuCanL ].
1050 replace (take_lev (ec :: lev) (Σ @@@ (ec :: lev))) with (Σ @@@ (ec::lev)).
1051 rewrite mapOptionTree_compose.
1052 rewrite mapOptionTree_compose.
1053 rewrite unlev_relev.
1055 rewrite take_lemma'.
1058 destruct case_RRight.
1060 destruct l as [|ec lev].
1062 replace (mapOptionTree flatten_leveled_type (Σ @@@ nil)) with (mapOptionTree flatten_type Σ @@@ nil).
1065 induction Σ; try destruct a; auto.
1070 repeat drop_simplify.
1071 rewrite drop_to_nothing.
1078 apply arrangeUnCancelEmptyTree with (q:=(mapTree (fun _ : ??(HaskType Γ ★) => tt) Σ)).
1079 induction Σ; try destruct a; auto.
1081 rewrite <- IHΣ1 at 2.
1082 rewrite <- IHΣ2 at 2.
1085 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AuCanR ].
1089 replace (take_lev (ec :: lev) (Σ @@@ (ec :: lev))) with (Σ @@@ (ec::lev)).
1090 rewrite mapOptionTree_compose.
1091 rewrite mapOptionTree_compose.
1092 rewrite unlev_relev.
1094 rewrite take_lemma'.
1097 destruct case_RVoid.
1107 destruct case_RAppT.
1108 simpl. destruct lev; simpl.
1109 unfold flatten_leveled_type.
1111 rewrite flatten_commutes_with_HaskTAll.
1112 rewrite flatten_commutes_with_substT.
1117 apply (Prelude_error "found type application at level >0; this is not supported").
1119 destruct case_RAbsT.
1120 simpl. destruct lev; simpl.
1121 rewrite flatten_commutes_with_HaskTAll.
1122 rewrite flatten_commutes_with_HaskTApp.
1123 eapply nd_comp; [ idtac | eapply nd_rule; eapply RAbsT ].
1125 set (mapOptionTree (flatten_leveled_type ) (mapOptionTree (weakLT(κ:=κ)) Σ)) as a.
1126 set (mapOptionTree (weakLT(κ:=κ)) (mapOptionTree (flatten_leveled_type ) Σ)) as q'.
1134 rewrite flatten_commutes_with_weakLT.
1145 apply (Prelude_error "found type abstraction at level >0; this is not supported").
1147 destruct case_RAppCo.
1148 simpl. destruct lev; simpl.
1149 unfold flatten_type.
1153 apply flatten_coercion.
1155 apply (Prelude_error "found coercion application at level >0; this is not supported").
1157 destruct case_RAbsCo.
1158 simpl. destruct lev; simpl.
1159 unfold flatten_type.
1161 apply (Prelude_error "AbsCo not supported (FIXME)").
1162 apply (Prelude_error "found coercion abstraction at level >0; this is not supported").
1164 destruct case_RLetRec.
1166 simpl. destruct lev; simpl.
1168 set (@RLetRec Γ Δ (mapOptionTree flatten_leveled_type lri) (flatten_type x) (mapOptionTree flatten_type y) nil) as q.
1169 replace (mapOptionTree flatten_leveled_type (y @@@ nil)) with (mapOptionTree flatten_type y @@@ nil).
1171 induction y; try destruct a; auto.
1176 repeat drop_simplify.
1177 repeat take_simplify.
1179 rewrite drop_to_nothing.
1185 apply arrangeCancelEmptyTree with (q:=y).
1186 induction y; try destruct a; auto.
1192 rewrite take_lemma'.
1193 set (mapOptionTree (flatten_type ○ unlev) (take_lev (h :: lev) lri)) as lri'.
1194 set (mapOptionTree flatten_leveled_type (drop_lev (h :: lev) lri)) as lri''.
1195 replace (mapOptionTree (flatten_type ○ unlev) (y @@@ (h :: lev))) with (mapOptionTree flatten_type y).
1198 rewrite <- mapOptionTree_compose.
1202 destruct case_RCase.
1204 apply (Prelude_error "Case not supported (BIG FIXME)").
1206 destruct case_SBrak.
1210 set (drop_lev (ec :: nil) (take_arg_types_as_tree t @@@ (ec :: nil))) as empty_tree.
1212 rewrite take_lemma'.
1214 rewrite mapOptionTree_compose.
1215 rewrite mapOptionTree_compose.
1216 rewrite unlev_relev.
1217 rewrite <- mapOptionTree_compose.
1220 set (mapOptionTree flatten_leveled_type (drop_lev (ec :: nil) succ)) as succ_host.
1221 set (mapOptionTree (flatten_type ○ unlev)(take_lev (ec :: nil) succ)) as succ_guest.
1222 set (mapOptionTree flatten_type (take_arg_types_as_tree t)) as succ_args.
1224 eapply nd_comp; [ eapply nd_rule; eapply RArrange; eapply ALeft; apply tree_of_nothing | idtac ].
1225 eapply nd_comp; [ eapply nd_rule; eapply RArrange; eapply ACanR | idtac ].
1226 refine (ga_unkappa Γ Δ (v2t ec) nil _ _ _ _ ;; _).
1227 eapply nd_comp; [ idtac | eapply arrange_brak ].
1233 apply (Prelude_error "found Brak at depth >0 indicating 3-level code; only two-level code is currently supported").
1239 unfold flatten_leveled_type at 2.
1242 rewrite mapOptionTree_compose.
1246 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ALeft; apply tree_of_nothing' ].
1247 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ACanR ].
1249 rewrite take_lemma'.
1250 rewrite unlev_relev.
1251 rewrite <- mapOptionTree_compose.
1252 eapply nd_comp; [ apply (arrange_esc _ _ ec) | idtac ].
1254 set (decide_tree_empty (take_lev (ec :: nil) succ)) as q'.
1260 set (mapOptionTree flatten_leveled_type (drop_lev (ec :: nil) succ)) as succ_host.
1261 set (mapOptionTree flatten_type (take_arg_types_as_tree t)) as succ_args.
1263 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply AuCanR ].
1264 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply AuCanR ].
1265 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply ACanL ].
1266 eapply nd_comp; [ idtac | eapply RLet ].
1267 eapply nd_comp; [ apply nd_llecnac | idtac ].
1268 apply nd_prod; [ idtac | eapply boost ].
1271 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ACanL ].
1279 refine ( _ ;; (boost _ _ _ _ _ (postcompose _ _ _ _ _ _ _ _))).
1287 refine ( _ ;; (boost _ _ _ _ _ (postcompose _ _ _ _ _ _ _ _))).
1289 refine ( _ ;; (boost _ _ _ _ _ (postcompose _ _ _ _ _ _ _ _))).
1295 (* environment has non-empty leaves *)
1296 apply (Prelude_error "ga_kappa not supported yet (BIG FIXME)").
1298 (* nesting too deep *)
1299 apply (Prelude_error "found Esc at depth >0 indicating 3-level code; only two-level code is currently supported").
1302 Definition flatten_proof :
1306 apply (Prelude_error "sorry, non-skolemized flattening isn't implemented").
1309 Definition skolemize_and_flatten_proof :
1313 (mapOptionTree (flatten_judgment ○ skolemize_judgment) h)
1314 (mapOptionTree (flatten_judgment ○ skolemize_judgment) c).
1316 rewrite mapOptionTree_compose.
1317 rewrite mapOptionTree_compose.
1318 apply flatten_skolemized_proof.
1319 apply skolemize_proof.
1324 (* to do: establish some metric on judgments (max length of level of any succedent type, probably), show how to
1325 * calculate it, and show that the flattening procedure above drives it down by one *)
1328 Instance FlatteningFunctor {Γ}{Δ}{ec} : Functor (JudgmentsL (PCF Γ Δ ec)) (TypesL (SystemFCa Γ Δ)) (obact) :=
1329 { fmor := FlatteningFunctor_fmor }.
1331 Definition ReificationFunctor Γ Δ : Functor (JudgmentsL _ _ (PCF n Γ Δ)) SystemFCa' (mapOptionTree brakifyJudg).
1332 refine {| fmor := ReificationFunctor_fmor Γ Δ |}; unfold hom; unfold ob; simpl ; intros.
1334 Definition PCF_SMME (n:nat)(Γ:TypeEnv)(Δ:CoercionEnv Γ) : ProgrammingLanguageSMME.
1335 refine {| plsmme_pl := PCF n Γ Δ |}.
1338 Definition SystemFCa_SMME (n:nat)(Γ:TypeEnv)(Δ:CoercionEnv Γ) : ProgrammingLanguageSMME.
1339 refine {| plsmme_pl := SystemFCa n Γ Δ |}.
1342 Definition ReificationFunctorMonoidal n : MonoidalFunctor (JudgmentsN n) (JudgmentsN (S n)) (ReificationFunctor n).
1346 Definition PCF_SystemFCa_two_level n Γ Δ : TwoLevelLanguage (PCF_SMME n Γ Δ) (SystemFCa_SMME (S n) Γ Δ).
1349 (* ... and the retraction exists *)
1353 Implicit Arguments garrow [ ].