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_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 ]
276 ; ga_apply : ∀ Γ Δ ec l a a' b c,
277 ND Rule [] [Γ > Δ > [@ga_mk Γ ec a [b ---> c] @@ l],,[@ga_mk Γ ec a' [b] @@ l] |- [@ga_mk Γ ec (a,,a') [c] ]@l ]
278 ; ga_kappa : ∀ Γ Δ ec l a b Σ, ND Rule
279 [Γ > Δ > Σ,,[@ga_mk Γ ec [] a @@ l] |- [@ga_mk Γ ec [] b ]@l ]
280 [Γ > Δ > Σ |- [@ga_mk Γ ec a b ]@l ]
282 Context `(gar:garrow).
284 Notation "a ~~~~> b" := (@ga_mk _ _ a b) (at level 20).
286 Definition boost : forall Γ Δ ant x y {lev},
287 ND Rule [] [ Γ > Δ > [x@@lev] |- [y]@lev ] ->
288 ND Rule [ Γ > Δ > ant |- [x]@lev ] [ Γ > Δ > ant |- [y]@lev ].
290 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ACanR ].
291 eapply nd_comp; [ idtac | eapply nd_rule; apply RLet ].
292 eapply nd_comp; [ apply nd_rlecnac | idtac ].
302 Definition precompose Γ Δ ec : forall a x y z lev,
304 [ Γ > Δ > a |- [@ga_mk _ ec y z ]@lev ]
305 [ Γ > Δ > a,,[@ga_mk _ ec x y @@ lev] |- [@ga_mk _ ec x z ]@lev ].
307 eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
308 eapply nd_comp; [ apply nd_rlecnac | idtac ].
311 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AExch ].
315 Definition precompose' Γ Δ ec : forall a b x y z lev,
317 [ Γ > Δ > a,,b |- [@ga_mk _ ec y z ]@lev ]
318 [ Γ > Δ > a,,([@ga_mk _ ec x y @@ lev],,b) |- [@ga_mk _ ec x z ]@lev ].
320 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ALeft; eapply AExch ].
321 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AuAssoc ].
325 Definition postcompose_ Γ Δ ec : forall a x y z lev,
327 [ Γ > Δ > a |- [@ga_mk _ ec x y ]@lev ]
328 [ Γ > Δ > a,,[@ga_mk _ ec y z @@ lev] |- [@ga_mk _ ec x z ]@lev ].
330 eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
331 eapply nd_comp; [ apply nd_rlecnac | idtac ].
337 Definition postcompose Γ Δ ec : forall x y z lev,
338 ND Rule [] [ Γ > Δ > [] |- [@ga_mk _ ec x y ]@lev ] ->
339 ND Rule [] [ Γ > Δ > [@ga_mk _ ec y z @@ lev] |- [@ga_mk _ ec x z ]@lev ].
341 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ACanL ].
342 eapply nd_comp; [ idtac | eapply postcompose_ ].
346 Definition first_nd : ∀ Γ Δ ec lev a b c Σ,
347 ND Rule [ Γ > Δ > Σ |- [@ga_mk Γ ec a b ]@lev ]
348 [ Γ > Δ > Σ |- [@ga_mk Γ ec (a,,c) (b,,c) ]@lev ].
350 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ACanR ].
351 eapply nd_comp; [ idtac | eapply nd_rule; apply RLet ].
352 eapply nd_comp; [ apply nd_rlecnac | idtac ].
355 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AuCanR ].
359 Definition firstify : ∀ Γ Δ ec lev a b c Σ,
360 ND Rule [] [ Γ > Δ > Σ |- [@ga_mk Γ ec a b ]@lev ] ->
361 ND Rule [] [ Γ > Δ > Σ |- [@ga_mk Γ ec (a,,c) (b,,c) ]@lev ].
368 Definition second_nd : ∀ Γ Δ ec lev a b c Σ,
370 [ Γ > Δ > Σ |- [@ga_mk Γ ec a b ]@lev ]
371 [ Γ > Δ > Σ |- [@ga_mk Γ ec (c,,a) (c,,b) ]@lev ].
373 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ACanR ].
374 eapply nd_comp; [ idtac | eapply nd_rule; apply RLet ].
375 eapply nd_comp; [ apply nd_rlecnac | idtac ].
378 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AuCanR ].
382 Definition secondify : ∀ Γ Δ ec lev a b c Σ,
383 ND Rule [] [ Γ > Δ > Σ |- [@ga_mk Γ ec a b ]@lev ] ->
384 ND Rule [] [ Γ > Δ > Σ |- [@ga_mk Γ ec (c,,a) (c,,b) ]@lev ].
391 Lemma ga_unkappa : ∀ Γ Δ ec l a b Σ x,
393 [Γ > Δ > Σ |- [@ga_mk Γ ec (a,,x) b ]@l ]
394 [Γ > Δ > Σ,,[@ga_mk Γ ec [] a @@ l] |- [@ga_mk Γ ec x b ]@l ].
396 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AExch ].
397 eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
398 eapply nd_comp; [ apply nd_llecnac | idtac ].
402 eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
403 eapply nd_comp; [ apply nd_llecnac | idtac ].
407 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AExch ].
411 (* useful for cutting down on the pretty-printed noise
413 Notation "` x" := (take_lev _ x) (at level 20).
414 Notation "`` x" := (mapOptionTree unlev x) (at level 20).
415 Notation "``` x" := (drop_lev _ x) (at level 20).
417 Definition flatten_arrangement' :
418 forall Γ (Δ:CoercionEnv Γ)
419 (ec:HaskTyVar Γ ECKind) (lev:HaskLevel Γ) (ant1 ant2:Tree ??(LeveledHaskType Γ ★)) (r:Arrange ant1 ant2),
420 ND Rule [] [Γ > Δ > [] |- [@ga_mk _ (v2t ec) (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) ant2))
421 (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) ant1)) ]@nil ].
424 refine (fix flatten ant1 ant2 (r:Arrange ant1 ant2):
425 ND Rule [] [Γ > Δ > [] |- [@ga_mk _ (v2t ec)
426 (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) ant2))
427 (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) ant1)) ]@nil] :=
428 match r as R in Arrange A B return
429 ND Rule [] [Γ > Δ > [] |- [@ga_mk _ (v2t ec)
430 (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) B))
431 (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) A)) ]@nil]
433 | AId a => let case_AId := tt in ga_id _ _ _ _ _
434 | ACanL a => let case_ACanL := tt in ga_uncancell _ _ _ _ _
435 | ACanR a => let case_ACanR := tt in ga_uncancelr _ _ _ _ _
436 | AuCanL a => let case_AuCanL := tt in ga_cancell _ _ _ _ _
437 | AuCanR a => let case_AuCanR := tt in ga_cancelr _ _ _ _ _
438 | AAssoc a b c => let case_AAssoc := tt in ga_assoc _ _ _ _ _ _ _
439 | AuAssoc a b c => let case_AuAssoc := tt in ga_unassoc _ _ _ _ _ _ _
440 | AExch a b => let case_AExch := tt in ga_swap _ _ _ _ _ _
441 | AWeak a => let case_AWeak := tt in ga_drop _ _ _ _ _
442 | ACont a => let case_ACont := tt in ga_copy _ _ _ _ _
443 | ALeft a b c r' => let case_ALeft := tt in flatten _ _ r' ;; boost _ _ _ _ _ (ga_second _ _ _ _ _ _ _)
444 | ARight a b c r' => let case_ARight := tt in flatten _ _ r' ;; boost _ _ _ _ _ (ga_first _ _ _ _ _ _ _)
445 | AComp c b a r1 r2 => let case_AComp := tt in (fun r1' r2' => _) (flatten _ _ r1) (flatten _ _ r2)
446 end); clear flatten; repeat take_simplify; repeat drop_simplify; intros.
449 set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) a)) as a' in *.
450 set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) b)) as b' in *.
451 set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) c)) as c' in *.
452 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply ACanL ].
453 eapply nd_comp; [ idtac | eapply nd_rule; apply
454 (@RLet Γ Δ [] [] (@ga_mk _ (v2t ec) a' b') (@ga_mk _ (v2t ec) a' c')) ].
455 eapply nd_comp; [ apply nd_llecnac | idtac ].
458 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply AuCanR ].
459 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply ACanL ].
460 eapply nd_comp; [ idtac | eapply nd_rule; apply RLet ].
461 eapply nd_comp; [ apply nd_llecnac | idtac ].
464 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AExch ].
468 Definition flatten_arrangement :
469 forall Γ (Δ:CoercionEnv Γ) n
470 (ec:HaskTyVar Γ ECKind) (lev:HaskLevel Γ) (ant1 ant2:Tree ??(LeveledHaskType Γ ★)) (r:Arrange ant1 ant2) succ,
472 [Γ > Δ > mapOptionTree (flatten_leveled_type ) (drop_lev n ant1)
473 |- [@ga_mk _ (v2t ec)
474 (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) ant1))
475 (mapOptionTree (flatten_type ) succ) ]@nil]
476 [Γ > Δ > mapOptionTree (flatten_leveled_type ) (drop_lev n ant2)
477 |- [@ga_mk _ (v2t ec)
478 (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) ant2))
479 (mapOptionTree (flatten_type ) succ) ]@nil].
481 refine ( _ ;; (boost _ _ _ _ _ (postcompose _ _ _ _ _ _ _ (flatten_arrangement' Γ Δ ec lev ant1 ant2 r)))).
484 refine ((fix flatten ant1 ant2 (r:Arrange ant1 ant2) :=
485 match r as R in Arrange A B return
486 Arrange (mapOptionTree (flatten_leveled_type ) (drop_lev _ A))
487 (mapOptionTree (flatten_leveled_type ) (drop_lev _ B)) with
488 | AId a => let case_AId := tt in AId _
489 | ACanL a => let case_ACanL := tt in ACanL _
490 | ACanR a => let case_ACanR := tt in ACanR _
491 | AuCanL a => let case_AuCanL := tt in AuCanL _
492 | AuCanR a => let case_AuCanR := tt in AuCanR _
493 | AAssoc a b c => let case_AAssoc := tt in AAssoc _ _ _
494 | AuAssoc a b c => let case_AuAssoc := tt in AuAssoc _ _ _
495 | AExch a b => let case_AExch := tt in AExch _ _
496 | AWeak a => let case_AWeak := tt in AWeak _
497 | ACont a => let case_ACont := tt in ACont _
498 | ALeft a b c r' => let case_ALeft := tt in ALeft _ (flatten _ _ r')
499 | ARight a b c r' => let case_ARight := tt in ARight _ (flatten _ _ r')
500 | AComp a b c r1 r2 => let case_AComp := tt in AComp (flatten _ _ r1) (flatten _ _ r2)
501 end) ant1 ant2 r); clear flatten; repeat take_simplify; repeat drop_simplify; intros.
504 Definition flatten_arrangement'' :
505 forall Γ Δ ant1 ant2 succ l (r:Arrange ant1 ant2),
506 ND Rule (mapOptionTree (flatten_judgment ) [Γ > Δ > ant1 |- succ @ l])
507 (mapOptionTree (flatten_judgment ) [Γ > Δ > ant2 |- succ @ l]).
521 apply AExch. (* TO DO: check for all-leaf trees here *)
526 eapply AComp; [ apply IHr1 | apply IHr2 ].
528 apply flatten_arrangement.
532 Definition ga_join Γ Δ Σ₁ Σ₂ a b ec :
533 ND Rule [] [Γ > Δ > Σ₁ |- [@ga_mk _ ec [] a ]@nil] ->
534 ND Rule [] [Γ > Δ > Σ₂ |- [@ga_mk _ ec [] b ]@nil] ->
535 ND Rule [] [Γ > Δ > Σ₁,,Σ₂ |- [@ga_mk _ ec [] (a,,b) ]@nil].
538 apply secondify with (c:=a) in pfb.
539 apply firstify with (c:=[]) in pfa.
540 eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
541 eapply nd_comp; [ eapply nd_llecnac | idtac ].
546 eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
547 eapply nd_comp; [ apply nd_llecnac | idtac ].
549 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ACanL ].
550 eapply nd_comp; [ idtac | eapply postcompose_ ].
553 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AExch ].
554 eapply nd_comp; [ idtac | eapply precompose ].
558 Definition arrange_brak : forall Γ Δ ec succ t,
561 [(@ga_mk _ (v2t ec) [] (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: nil) succ))) @@ nil],,
562 mapOptionTree (flatten_leveled_type ) (drop_lev (ec :: nil) succ) |- [t]@nil]
563 [Γ > Δ > mapOptionTree (flatten_leveled_type ) succ |- [t]@nil].
567 set (@arrangeUnPartition _ succ (levelMatch (ec::nil))) as q.
568 set (arrangeMap _ _ flatten_leveled_type q) as y.
576 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AExch ].
578 eapply nd_comp; [ apply nd_llecnac | idtac ].
579 eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
584 induction succ; try destruct a; simpl.
590 destruct l as [t' lev'].
591 destruct lev' as [|ec' lev'].
595 set (@eqd_dec (HaskLevel Γ) (haskLevelEqDecidable Γ) (ec' :: lev') (ec :: nil)) as q.
600 unfold flatten_leveled_type.
617 Definition arrange_esc : forall Γ Δ ec succ t,
619 [Γ > Δ > mapOptionTree (flatten_leveled_type ) succ |- [t]@nil]
621 [(@ga_mk _ (v2t ec) [] (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: nil) succ))) @@ nil],,
622 mapOptionTree (flatten_leveled_type ) (drop_lev (ec :: nil) succ) |- [t]@nil].
624 set (@arrangePartition _ succ (levelMatch (ec::nil))) as q.
625 set (@drop_lev Γ (ec::nil) succ) as q'.
626 assert (@drop_lev Γ (ec::nil) succ=q') as H.
628 unfold drop_lev in H.
629 unfold mkDropFlags in H.
632 set (arrangeMap _ _ flatten_leveled_type q) as y.
639 set (mapOptionTree flatten_leveled_type (dropT (mkFlags (liftBoolFunc false (bnot ○ levelMatch (ec :: nil))) succ))) as q.
640 destruct (decide_tree_empty q); [ idtac | apply (Prelude_error "escapifying open code not yet supported") ].
644 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply AExch ].
645 set (fun z z' => @RLet Γ Δ z (mapOptionTree flatten_leveled_type q') t z' nil) as q''.
646 eapply nd_comp; [ idtac | eapply nd_rule; apply RLet ].
648 eapply nd_comp; [ apply nd_rlecnac | idtac ].
652 eapply AComp; [ idtac | apply ACanR ].
654 apply (@arrangeCancelEmptyTree _ _ _ _ e).
658 eapply (@RVar Γ Δ t nil).
666 eapply decide_tree_empty.
669 set (dropT (mkFlags (liftBoolFunc false (bnot ○ levelMatch (ec :: nil))) succ)) as escapified.
670 destruct (decide_tree_empty escapified).
677 unfold mkDropFlags; simpl.
681 destruct (General.list_eq_dec h0 (ec :: nil)).
697 apply (Prelude_error "escapifying code with multi-leaf antecedents is not supported").
701 Lemma unlev_relev : forall {Γ}(t:Tree ??(HaskType Γ ★)) lev, mapOptionTree unlev (t @@@ lev) = t.
704 destruct a; reflexivity.
705 rewrite <- IHt1 at 2.
706 rewrite <- IHt2 at 2.
710 Lemma tree_of_nothing : forall Γ ec t,
711 Arrange (mapOptionTree flatten_leveled_type (drop_lev(Γ:=Γ) (ec :: nil) (t @@@ (ec :: nil)))) [].
713 induction t; try destruct o; try destruct a.
720 eapply AComp; [ idtac | apply ACanL ].
721 eapply AComp; [ idtac | eapply ALeft; apply IHt2 ].
724 Transparent drop_lev.
731 Lemma tree_of_nothing' : forall Γ ec t,
732 Arrange [] (mapOptionTree flatten_leveled_type (drop_lev(Γ:=Γ) (ec :: nil) (t @@@ (ec :: nil)))).
734 induction t; try destruct o; try destruct a.
741 eapply AComp; [ apply AuCanL | idtac ].
742 eapply AComp; [ eapply ARight; apply IHt1 | idtac ].
745 Transparent drop_lev.
752 Lemma krunk : forall Γ (ec:HaskTyVar Γ ECKind) t,
753 flatten_type (<[ ec |- t ]>)
755 (mapOptionTree flatten_type (take_arg_types_as_tree t))
756 [ flatten_type (drop_arg_types_as_tree t)].
758 unfold flatten_type at 1.
761 apply phoas_extensionality.
766 rewrite <- mapOptionTree_compose.
767 unfold take_arg_types_as_tree.
769 replace (flatten_type (drop_arg_types_as_tree t) tv ite)
770 with (drop_arg_types (flatten_rawtype (t tv ite))).
771 replace (unleaves_ (take_arg_types (flatten_rawtype (t tv ite))))
772 with ((mapOptionTree (fun x : HaskType Γ ★ => flatten_type x tv ite)
774 (take_trustme (count_arg_types (t (fun _ : Kind => unit) (ite_unit Γ)))
775 (fun TV : Kind → Type => take_arg_types ○ t TV))))).
778 clear hetmet_flatten.
779 clear hetmet_unflatten.
787 Lemma drop_to_nothing : forall (Γ:TypeEnv) Σ (lev:HaskLevel Γ),
788 drop_lev lev (Σ @@@ lev) = mapTree (fun _ => None) (mapTree (fun _ => tt) Σ).
802 Definition flatten_skolemized_proof :
805 ND Rule (mapOptionTree (flatten_judgment ) h) (mapOptionTree (flatten_judgment ) c).
807 eapply nd_map'; [ idtac | apply X ].
813 (match X as R in SRule H C with
814 | SBrak Γ Δ t ec succ lev => let case_SBrak := tt in _
815 | SEsc Γ Δ t ec succ lev => let case_SEsc := tt in _
816 | SFlat h c r => let case_SFlat := tt in _
820 refine (match r as R in Rule H C with
821 | RArrange Γ Δ a b x l d => let case_RArrange := tt in _
822 | RNote Γ Δ Σ τ l n => let case_RNote := tt in _
823 | RLit Γ Δ l _ => let case_RLit := tt in _
824 | RVar Γ Δ σ lev => let case_RVar := tt in _
825 | RGlobal Γ Δ σ l wev => let case_RGlobal := tt in _
826 | RLam Γ Δ Σ tx te lev => let case_RLam := tt in _
827 | RCast Γ Δ Σ σ τ lev γ => let case_RCast := tt in _
828 | RAbsT Γ Δ Σ κ σ lev => let case_RAbsT := tt in _
829 | RAppT Γ Δ Σ κ σ τ lev => let case_RAppT := tt in _
830 | RAppCo Γ Δ Σ κ σ₁ σ₂ γ σ lev => let case_RAppCo := tt in _
831 | RAbsCo Γ Δ Σ κ σ σ₁ σ₂ lev => let case_RAbsCo := tt in _
832 | RApp Γ Δ Σ₁ Σ₂ tx te lev => let case_RApp := tt in _
833 | RLet Γ Δ Σ₁ Σ₂ σ₁ σ₂ lev => let case_RLet := tt in _
834 | RCut Γ Δ Σ₁ Σ₁₂ Σ₂ Σ₃ l => let case_RCut := tt in _
835 | RLeft Γ Δ Σ₁ Σ₂ Σ l => let case_RLeft := tt in _
836 | RRight Γ Δ Σ₁ Σ₂ Σ l => let case_RRight := tt in _
837 | RWhere Γ Δ Σ₁ Σ₂ Σ₃ σ₁ σ₂ lev => let case_RWhere := 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 lev as [|ec lev]; simpl; [ apply nd_rule; apply RLet; auto | idtac ].
964 repeat drop_simplify.
965 repeat take_simplify.
968 set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) Σ₁)) as Σ₁'.
969 set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) Σ₂)) as Σ₂'.
970 set (mapOptionTree flatten_leveled_type (drop_lev (ec :: lev) Σ₁)) as Σ₁''.
971 set (mapOptionTree flatten_leveled_type (drop_lev (ec :: lev) Σ₂)) as Σ₂''.
974 eapply nd_prod; [ idtac | apply nd_id ].
976 apply (ga_first _ _ _ _ _ _ Σ₂').
978 eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
981 eapply nd_comp; [ eapply nd_rule; eapply RArrange; eapply ACanL | idtac ].
982 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AExch (* okay *)].
985 destruct case_RWhere.
987 destruct lev as [|ec lev]; simpl; [ apply nd_rule; apply RWhere; auto | idtac ].
988 repeat take_simplify.
989 repeat drop_simplify.
992 set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) Σ₁)) as Σ₁'.
993 set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) Σ₂)) as Σ₂'.
994 set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) Σ₃)) as Σ₃'.
995 set (mapOptionTree flatten_leveled_type (drop_lev (ec :: lev) Σ₁)) as Σ₁''.
996 set (mapOptionTree flatten_leveled_type (drop_lev (ec :: lev) Σ₂)) as Σ₂''.
997 set (mapOptionTree flatten_leveled_type (drop_lev (ec :: lev) Σ₃)) as Σ₃''.
1000 eapply nd_prod; [ eapply nd_id | idtac ].
1001 eapply (first_nd _ _ _ _ _ _ Σ₃').
1003 eapply nd_prod; [ eapply nd_id | idtac ].
1004 eapply (second_nd _ _ _ _ _ _ Σ₁').
1006 eapply nd_comp; [ idtac | eapply nd_rule; eapply RWhere ].
1007 apply nd_prod; [ idtac | apply nd_id ].
1008 eapply nd_comp; [ idtac | eapply precompose' ].
1016 destruct l as [|ec lev]; simpl.
1018 replace (mapOptionTree flatten_leveled_type (Σ₁₂ @@@ nil)) with (mapOptionTree flatten_type Σ₁₂ @@@ nil).
1020 induction Σ₁₂; try destruct a; auto.
1026 repeat drop_simplify.
1028 repeat take_simplify.
1030 set (drop_lev (ec :: lev) (Σ₁₂ @@@ (ec :: lev))) as x1.
1031 rewrite take_lemma'.
1032 rewrite mapOptionTree_compose.
1033 rewrite mapOptionTree_compose.
1034 rewrite mapOptionTree_compose.
1035 rewrite unlev_relev.
1036 rewrite <- mapOptionTree_compose.
1037 rewrite <- mapOptionTree_compose.
1038 eapply nd_comp; [ idtac | eapply nd_rule; eapply RCut ].
1046 rewrite drop_to_nothing.
1047 apply arrangeCancelEmptyTree with (q:=(mapTree (fun _ : ??(HaskType Γ ★) => tt) Σ₁₂)).
1049 eapply nd_comp; [ eapply nd_rule; eapply RArrange; eapply ACanL | idtac ].
1050 set (mapOptionTree flatten_type Σ₁₂) as a.
1051 set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) Σ₁)) as b.
1052 set (mapOptionTree flatten_leveled_type (drop_lev (ec :: lev) Σ₂)) as c.
1053 set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) Σ₂)) as d.
1054 eapply nd_comp; [ idtac | eapply nd_rule; eapply RCut ].
1055 eapply nd_comp; [ apply nd_llecnac | idtac ].
1059 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AExch ].
1063 destruct case_RLeft.
1065 destruct l as [|ec lev].
1067 replace (mapOptionTree flatten_leveled_type (Σ @@@ nil)) with (mapOptionTree flatten_type Σ @@@ nil).
1070 induction Σ; try destruct a; auto.
1075 repeat drop_simplify.
1076 rewrite drop_to_nothing.
1083 apply arrangeUnCancelEmptyTree with (q:=(mapTree (fun _ : ??(HaskType Γ ★) => tt) Σ)).
1086 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AuCanL ].
1090 replace (take_lev (ec :: lev) (Σ @@@ (ec :: lev))) with (Σ @@@ (ec::lev)).
1091 rewrite mapOptionTree_compose.
1092 rewrite mapOptionTree_compose.
1093 rewrite unlev_relev.
1095 rewrite take_lemma'.
1098 destruct case_RRight.
1100 destruct l as [|ec lev].
1102 replace (mapOptionTree flatten_leveled_type (Σ @@@ nil)) with (mapOptionTree flatten_type Σ @@@ nil).
1105 induction Σ; try destruct a; auto.
1110 repeat drop_simplify.
1111 rewrite drop_to_nothing.
1118 apply arrangeUnCancelEmptyTree with (q:=(mapTree (fun _ : ??(HaskType Γ ★) => tt) Σ)).
1121 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AuCanR ].
1125 replace (take_lev (ec :: lev) (Σ @@@ (ec :: lev))) with (Σ @@@ (ec::lev)).
1126 rewrite mapOptionTree_compose.
1127 rewrite mapOptionTree_compose.
1128 rewrite unlev_relev.
1130 rewrite take_lemma'.
1133 destruct case_RVoid.
1138 apply (Prelude_error "RVoid at level >0").
1140 destruct case_RAppT.
1141 simpl. destruct lev; simpl.
1142 unfold flatten_leveled_type.
1144 rewrite flatten_commutes_with_HaskTAll.
1145 rewrite flatten_commutes_with_substT.
1150 apply (Prelude_error "found type application at level >0; this is not supported").
1152 destruct case_RAbsT.
1153 simpl. destruct lev; simpl.
1154 rewrite flatten_commutes_with_HaskTAll.
1155 rewrite flatten_commutes_with_HaskTApp.
1156 eapply nd_comp; [ idtac | eapply nd_rule; eapply RAbsT ].
1158 set (mapOptionTree (flatten_leveled_type ) (mapOptionTree (weakLT(κ:=κ)) Σ)) as a.
1159 set (mapOptionTree (weakLT(κ:=κ)) (mapOptionTree (flatten_leveled_type ) Σ)) as q'.
1167 rewrite flatten_commutes_with_weakLT.
1178 apply (Prelude_error "found type abstraction at level >0; this is not supported").
1180 destruct case_RAppCo.
1181 simpl. destruct lev; simpl.
1182 unfold flatten_type.
1186 apply flatten_coercion.
1188 apply (Prelude_error "found coercion application at level >0; this is not supported").
1190 destruct case_RAbsCo.
1191 simpl. destruct lev; simpl.
1192 unfold flatten_type.
1194 apply (Prelude_error "AbsCo not supported (FIXME)").
1195 apply (Prelude_error "found coercion abstraction at level >0; this is not supported").
1197 destruct case_RLetRec.
1199 simpl. destruct lev; simpl.
1201 set (@RLetRec Γ Δ (mapOptionTree flatten_leveled_type lri) (flatten_type x) (mapOptionTree flatten_type y) nil) as q.
1202 replace (mapOptionTree flatten_leveled_type (y @@@ nil)) with (mapOptionTree flatten_type y @@@ nil).
1204 induction y; try destruct a; auto.
1209 apply (Prelude_error "LetRec not supported inside brackets yet (FIXME)").
1211 destruct case_RCase.
1213 apply (Prelude_error "Case not supported (BIG FIXME)").
1215 destruct case_SBrak.
1219 set (drop_lev (ec :: nil) (take_arg_types_as_tree t @@@ (ec :: nil))) as empty_tree.
1221 rewrite take_lemma'.
1223 rewrite mapOptionTree_compose.
1224 rewrite mapOptionTree_compose.
1225 rewrite unlev_relev.
1226 rewrite <- mapOptionTree_compose.
1229 set (mapOptionTree flatten_leveled_type (drop_lev (ec :: nil) succ)) as succ_host.
1230 set (mapOptionTree (flatten_type ○ unlev)(take_lev (ec :: nil) succ)) as succ_guest.
1231 set (mapOptionTree flatten_type (take_arg_types_as_tree t)) as succ_args.
1233 eapply nd_comp; [ eapply nd_rule; eapply RArrange; eapply ALeft; apply tree_of_nothing | idtac ].
1234 eapply nd_comp; [ eapply nd_rule; eapply RArrange; eapply ACanR | idtac ].
1235 refine (ga_unkappa Γ Δ (v2t ec) nil _ _ _ _ ;; _).
1236 eapply nd_comp; [ idtac | eapply arrange_brak ].
1242 apply (Prelude_error "found Brak at depth >0 indicating 3-level code; only two-level code is currently supported").
1248 unfold flatten_leveled_type at 2.
1251 rewrite mapOptionTree_compose.
1255 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ALeft; apply tree_of_nothing' ].
1256 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ACanR ].
1258 rewrite take_lemma'.
1259 rewrite unlev_relev.
1260 rewrite <- mapOptionTree_compose.
1261 eapply nd_comp; [ apply (arrange_esc _ _ ec) | idtac ].
1263 set (decide_tree_empty (take_lev (ec :: nil) succ)) as q'.
1269 set (mapOptionTree flatten_leveled_type (drop_lev (ec :: nil) succ)) as succ_host.
1270 set (mapOptionTree flatten_type (take_arg_types_as_tree t)) as succ_args.
1272 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply AuCanR ].
1273 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply AuCanR ].
1274 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply ACanL ].
1275 eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
1276 eapply nd_comp; [ apply nd_llecnac | idtac ].
1277 apply nd_prod; [ idtac | eapply boost ].
1280 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ACanL ].
1288 refine ( _ ;; (boost _ _ _ _ _ (postcompose _ _ _ _ _ _ _ _))).
1296 refine ( _ ;; (boost _ _ _ _ _ (postcompose _ _ _ _ _ _ _ _))).
1298 refine ( _ ;; (boost _ _ _ _ _ (postcompose _ _ _ _ _ _ _ _))).
1304 (* environment has non-empty leaves *)
1305 apply (Prelude_error "ga_kappa not supported yet (BIG FIXME)").
1307 (* nesting too deep *)
1308 apply (Prelude_error "found Esc at depth >0 indicating 3-level code; only two-level code is currently supported").
1311 Definition flatten_proof :
1315 apply (Prelude_error "sorry, non-skolemized flattening isn't implemented").
1318 Definition skolemize_and_flatten_proof :
1322 (mapOptionTree (flatten_judgment ○ skolemize_judgment) h)
1323 (mapOptionTree (flatten_judgment ○ skolemize_judgment) c).
1325 rewrite mapOptionTree_compose.
1326 rewrite mapOptionTree_compose.
1327 apply flatten_skolemized_proof.
1328 apply skolemize_proof.
1333 (* to do: establish some metric on judgments (max length of level of any succedent type, probably), show how to
1334 * calculate it, and show that the flattening procedure above drives it down by one *)
1337 Instance FlatteningFunctor {Γ}{Δ}{ec} : Functor (JudgmentsL (PCF Γ Δ ec)) (TypesL (SystemFCa Γ Δ)) (obact) :=
1338 { fmor := FlatteningFunctor_fmor }.
1340 Definition ReificationFunctor Γ Δ : Functor (JudgmentsL _ _ (PCF n Γ Δ)) SystemFCa' (mapOptionTree brakifyJudg).
1341 refine {| fmor := ReificationFunctor_fmor Γ Δ |}; unfold hom; unfold ob; simpl ; intros.
1343 Definition PCF_SMME (n:nat)(Γ:TypeEnv)(Δ:CoercionEnv Γ) : ProgrammingLanguageSMME.
1344 refine {| plsmme_pl := PCF n Γ Δ |}.
1347 Definition SystemFCa_SMME (n:nat)(Γ:TypeEnv)(Δ:CoercionEnv Γ) : ProgrammingLanguageSMME.
1348 refine {| plsmme_pl := SystemFCa n Γ Δ |}.
1351 Definition ReificationFunctorMonoidal n : MonoidalFunctor (JudgmentsN n) (JudgmentsN (S n)) (ReificationFunctor n).
1355 Definition PCF_SystemFCa_two_level n Γ Δ : TwoLevelLanguage (PCF_SMME n Γ Δ) (SystemFCa_SMME (S n) Γ Δ).
1358 (* ... and the retraction exists *)
1362 Implicit Arguments garrow [ ].