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 | RJoin Γ p lri m x q l => let case_RJoin := tt in _
839 | RVoid _ _ l => let case_RVoid := tt in _
840 | RBrak Γ Δ t ec succ lev => let case_RBrak := tt in _
841 | REsc Γ Δ t ec succ lev => let case_REsc := tt in _
842 | RCase Γ Δ lev tc Σ avars tbranches alts => let case_RCase := tt in _
843 | RLetRec Γ Δ lri x y t => let case_RLetRec := tt in _
846 destruct case_RArrange.
847 apply (flatten_arrangement'' Γ Δ a b x _ d).
850 apply (Prelude_error "found unskolemized Brak rule; this shouldn't happen").
853 apply (Prelude_error "found unskolemized Esc rule; this shouldn't happen").
858 apply nd_rule; apply RNote; auto.
859 apply nd_rule; apply RNote; auto.
864 unfold flatten_leveled_type.
866 rewrite literal_types_unchanged.
867 apply nd_rule; apply RLit.
868 unfold take_lev; simpl.
869 unfold drop_lev; simpl.
871 rewrite literal_types_unchanged.
875 Opaque flatten_judgment.
877 Transparent flatten_judgment.
879 unfold flatten_judgment.
881 apply nd_rule. apply RVar.
882 repeat drop_simplify.
883 repeat take_simplify.
887 destruct case_RGlobal.
891 destruct l as [|ec lev]; simpl.
892 destruct (eqd_dec (g:CoreVar) (hetmet_flatten:CoreVar)).
893 set (flatten_type (g wev)) as t.
894 set (RGlobal _ Δ nil (mkGlobal Γ t hetmet_id)) as q.
899 destruct (eqd_dec (g:CoreVar) (hetmet_unflatten:CoreVar)).
900 set (flatten_type (g wev)) as t.
901 set (RGlobal _ Δ nil (mkGlobal Γ t hetmet_id)) as q.
906 unfold flatten_leveled_type. simpl.
907 apply nd_rule; rewrite globals_do_not_have_code_types.
909 apply (Prelude_error "found RGlobal at depth >0; globals should never appear inside code brackets unless escaped").
915 destruct lev as [|ec lev]; simpl; [ apply nd_rule; apply RLam; auto | idtac ].
916 repeat drop_simplify.
917 repeat take_simplify.
929 destruct lev as [|ec lev]; simpl; [ apply nd_rule; apply RCast; auto | idtac ].
931 apply flatten_coercion; auto.
932 apply (Prelude_error "RCast at level >0; casting inside of code brackets is currently not supported").
937 [ apply nd_rule; apply RJoin | idtac ];
938 apply (Prelude_error "RJoin at depth >0").
943 destruct lev as [|ec lev].
944 unfold flatten_type at 1.
949 repeat drop_simplify.
950 repeat take_simplify.
951 rewrite mapOptionTree_distributes.
952 set (mapOptionTree (flatten_leveled_type ) (drop_lev (ec :: lev) Σ₁)) as Σ₁'.
953 set (mapOptionTree (flatten_leveled_type ) (drop_lev (ec :: lev) Σ₂)) as Σ₂'.
954 set (take_lev (ec :: lev) Σ₁) as Σ₁''.
955 set (take_lev (ec :: lev) Σ₂) as Σ₂''.
956 replace (flatten_type (tx ---> te)) with ((flatten_type tx) ---> (flatten_type te)).
957 apply (Prelude_error "FIXME: ga_apply").
961 Notation "` x" := (take_lev _ x).
962 Notation "`` x" := (mapOptionTree unlev x) (at level 20).
963 Notation "``` x" := ((drop_lev _ x)) (at level 20).
964 Notation "!<[]> x" := (flatten_type _ x) (at level 1).
965 Notation "!<[@]> x" := (mapOptionTree flatten_leveled_type x) (at level 1).
970 destruct lev as [|ec lev]; simpl; [ apply nd_rule; apply RLet; auto | idtac ].
971 repeat drop_simplify.
972 repeat take_simplify.
975 set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) Σ₁)) as Σ₁'.
976 set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) Σ₂)) as Σ₂'.
977 set (mapOptionTree flatten_leveled_type (drop_lev (ec :: lev) Σ₁)) as Σ₁''.
978 set (mapOptionTree flatten_leveled_type (drop_lev (ec :: lev) Σ₂)) as Σ₂''.
981 eapply nd_prod; [ idtac | apply nd_id ].
983 apply (ga_first _ _ _ _ _ _ Σ₂').
985 eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
988 eapply nd_comp; [ eapply nd_rule; eapply RArrange; eapply ACanL | idtac ].
989 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AExch (* okay *)].
992 destruct case_RWhere.
994 destruct lev as [|ec lev]; simpl; [ apply nd_rule; apply RWhere; auto | idtac ].
995 repeat take_simplify.
996 repeat drop_simplify.
999 set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) Σ₁)) as Σ₁'.
1000 set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) Σ₂)) as Σ₂'.
1001 set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) Σ₃)) as Σ₃'.
1002 set (mapOptionTree flatten_leveled_type (drop_lev (ec :: lev) Σ₁)) as Σ₁''.
1003 set (mapOptionTree flatten_leveled_type (drop_lev (ec :: lev) Σ₂)) as Σ₂''.
1004 set (mapOptionTree flatten_leveled_type (drop_lev (ec :: lev) Σ₃)) as Σ₃''.
1007 eapply nd_prod; [ eapply nd_id | idtac ].
1008 eapply (first_nd _ _ _ _ _ _ Σ₃').
1010 eapply nd_prod; [ eapply nd_id | idtac ].
1011 eapply (second_nd _ _ _ _ _ _ Σ₁').
1013 eapply nd_comp; [ idtac | eapply nd_rule; eapply RWhere ].
1014 apply nd_prod; [ idtac | apply nd_id ].
1015 eapply nd_comp; [ idtac | eapply precompose' ].
1023 destruct l as [|ec lev]; simpl.
1025 replace (mapOptionTree flatten_leveled_type (Σ₁₂ @@@ nil)) with (mapOptionTree flatten_type Σ₁₂ @@@ nil).
1027 induction Σ₁₂; try destruct a; auto.
1033 repeat drop_simplify.
1035 repeat take_simplify.
1037 set (drop_lev (ec :: lev) (Σ₁₂ @@@ (ec :: lev))) as x1.
1038 rewrite take_lemma'.
1039 rewrite mapOptionTree_compose.
1040 rewrite mapOptionTree_compose.
1041 rewrite mapOptionTree_compose.
1042 rewrite unlev_relev.
1043 rewrite <- mapOptionTree_compose.
1044 rewrite <- mapOptionTree_compose.
1045 eapply nd_comp; [ idtac | eapply nd_rule; eapply RCut ].
1053 rewrite drop_to_nothing.
1054 apply arrangeCancelEmptyTree with (q:=(mapTree (fun _ : ??(HaskType Γ ★) => tt) Σ₁₂)).
1056 eapply nd_comp; [ eapply nd_rule; eapply RArrange; eapply ACanL | idtac ].
1057 set (mapOptionTree flatten_type Σ₁₂) as a.
1058 set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) Σ₁)) as b.
1059 set (mapOptionTree flatten_leveled_type (drop_lev (ec :: lev) Σ₂)) as c.
1060 set (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: lev) Σ₂)) as d.
1061 eapply nd_comp; [ idtac | eapply nd_rule; eapply RCut ].
1062 eapply nd_comp; [ apply nd_llecnac | idtac ].
1066 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AExch ].
1070 destruct case_RLeft.
1072 destruct l as [|ec lev].
1074 replace (mapOptionTree flatten_leveled_type (Σ @@@ nil)) with (mapOptionTree flatten_type Σ @@@ nil).
1077 induction Σ; try destruct a; auto.
1082 repeat drop_simplify.
1083 rewrite drop_to_nothing.
1090 apply arrangeUnCancelEmptyTree with (q:=(mapTree (fun _ : ??(HaskType Γ ★) => tt) Σ)).
1093 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AuCanL ].
1097 replace (take_lev (ec :: lev) (Σ @@@ (ec :: lev))) with (Σ @@@ (ec::lev)).
1098 rewrite mapOptionTree_compose.
1099 rewrite mapOptionTree_compose.
1100 rewrite unlev_relev.
1102 rewrite take_lemma'.
1105 destruct case_RRight.
1107 destruct l as [|ec lev].
1109 replace (mapOptionTree flatten_leveled_type (Σ @@@ nil)) with (mapOptionTree flatten_type Σ @@@ nil).
1112 induction Σ; try destruct a; auto.
1117 repeat drop_simplify.
1118 rewrite drop_to_nothing.
1125 apply arrangeUnCancelEmptyTree with (q:=(mapTree (fun _ : ??(HaskType Γ ★) => tt) Σ)).
1128 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply AuCanR ].
1132 replace (take_lev (ec :: lev) (Σ @@@ (ec :: lev))) with (Σ @@@ (ec::lev)).
1133 rewrite mapOptionTree_compose.
1134 rewrite mapOptionTree_compose.
1135 rewrite unlev_relev.
1137 rewrite take_lemma'.
1140 destruct case_RVoid.
1145 apply (Prelude_error "RVoid at level >0").
1147 destruct case_RAppT.
1148 simpl. destruct lev; simpl.
1149 unfold flatten_leveled_type.
1151 rewrite flatten_commutes_with_HaskTAll.
1152 rewrite flatten_commutes_with_substT.
1157 apply (Prelude_error "found type application at level >0; this is not supported").
1159 destruct case_RAbsT.
1160 simpl. destruct lev; simpl.
1161 rewrite flatten_commutes_with_HaskTAll.
1162 rewrite flatten_commutes_with_HaskTApp.
1163 eapply nd_comp; [ idtac | eapply nd_rule; eapply RAbsT ].
1165 set (mapOptionTree (flatten_leveled_type ) (mapOptionTree (weakLT(κ:=κ)) Σ)) as a.
1166 set (mapOptionTree (weakLT(κ:=κ)) (mapOptionTree (flatten_leveled_type ) Σ)) as q'.
1174 rewrite flatten_commutes_with_weakLT.
1185 apply (Prelude_error "found type abstraction at level >0; this is not supported").
1187 destruct case_RAppCo.
1188 simpl. destruct lev; simpl.
1189 unfold flatten_type.
1193 apply flatten_coercion.
1195 apply (Prelude_error "found coercion application at level >0; this is not supported").
1197 destruct case_RAbsCo.
1198 simpl. destruct lev; simpl.
1199 unfold flatten_type.
1201 apply (Prelude_error "AbsCo not supported (FIXME)").
1202 apply (Prelude_error "found coercion abstraction at level >0; this is not supported").
1204 destruct case_RLetRec.
1206 simpl. destruct lev; simpl.
1208 set (@RLetRec Γ Δ (mapOptionTree flatten_leveled_type lri) (flatten_type x) (mapOptionTree flatten_type y) nil) as q.
1209 replace (mapOptionTree flatten_leveled_type (y @@@ nil)) with (mapOptionTree flatten_type y @@@ nil).
1211 induction y; try destruct a; auto.
1216 apply (Prelude_error "LetRec not supported inside brackets yet (FIXME)").
1218 destruct case_RCase.
1220 apply (Prelude_error "Case not supported (BIG FIXME)").
1222 destruct case_SBrak.
1226 set (drop_lev (ec :: nil) (take_arg_types_as_tree t @@@ (ec :: nil))) as empty_tree.
1228 rewrite take_lemma'.
1230 rewrite mapOptionTree_compose.
1231 rewrite mapOptionTree_compose.
1232 rewrite unlev_relev.
1233 rewrite <- mapOptionTree_compose.
1236 set (mapOptionTree flatten_leveled_type (drop_lev (ec :: nil) succ)) as succ_host.
1237 set (mapOptionTree (flatten_type ○ unlev)(take_lev (ec :: nil) succ)) as succ_guest.
1238 set (mapOptionTree flatten_type (take_arg_types_as_tree t)) as succ_args.
1240 eapply nd_comp; [ eapply nd_rule; eapply RArrange; eapply ALeft; apply tree_of_nothing | idtac ].
1241 eapply nd_comp; [ eapply nd_rule; eapply RArrange; eapply ACanR | idtac ].
1242 refine (ga_unkappa Γ Δ (v2t ec) nil _ _ _ _ ;; _).
1243 eapply nd_comp; [ idtac | eapply arrange_brak ].
1249 apply (Prelude_error "found Brak at depth >0 indicating 3-level code; only two-level code is currently supported").
1255 unfold flatten_leveled_type at 2.
1258 rewrite mapOptionTree_compose.
1262 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ALeft; apply tree_of_nothing' ].
1263 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ACanR ].
1265 rewrite take_lemma'.
1266 rewrite unlev_relev.
1267 rewrite <- mapOptionTree_compose.
1268 eapply nd_comp; [ apply (arrange_esc _ _ ec) | idtac ].
1270 set (decide_tree_empty (take_lev (ec :: nil) succ)) as q'.
1276 set (mapOptionTree flatten_leveled_type (drop_lev (ec :: nil) succ)) as succ_host.
1277 set (mapOptionTree flatten_type (take_arg_types_as_tree t)) as succ_args.
1279 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply AuCanR ].
1280 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply AuCanR ].
1281 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply ACanL ].
1282 eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
1283 eapply nd_comp; [ apply nd_llecnac | idtac ].
1284 apply nd_prod; [ idtac | eapply boost ].
1287 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ACanL ].
1295 refine ( _ ;; (boost _ _ _ _ _ (postcompose _ _ _ _ _ _ _ _))).
1303 refine ( _ ;; (boost _ _ _ _ _ (postcompose _ _ _ _ _ _ _ _))).
1305 refine ( _ ;; (boost _ _ _ _ _ (postcompose _ _ _ _ _ _ _ _))).
1311 (* environment has non-empty leaves *)
1312 apply (Prelude_error "ga_kappa not supported yet (BIG FIXME)").
1314 (* nesting too deep *)
1315 apply (Prelude_error "found Esc at depth >0 indicating 3-level code; only two-level code is currently supported").
1318 Definition flatten_proof :
1322 apply (Prelude_error "sorry, non-skolemized flattening isn't implemented").
1325 Definition skolemize_and_flatten_proof :
1329 (mapOptionTree (flatten_judgment ○ skolemize_judgment) h)
1330 (mapOptionTree (flatten_judgment ○ skolemize_judgment) c).
1332 rewrite mapOptionTree_compose.
1333 rewrite mapOptionTree_compose.
1334 apply flatten_skolemized_proof.
1335 apply skolemize_proof.
1340 (* to do: establish some metric on judgments (max length of level of any succedent type, probably), show how to
1341 * calculate it, and show that the flattening procedure above drives it down by one *)
1344 Instance FlatteningFunctor {Γ}{Δ}{ec} : Functor (JudgmentsL (PCF Γ Δ ec)) (TypesL (SystemFCa Γ Δ)) (obact) :=
1345 { fmor := FlatteningFunctor_fmor }.
1347 Definition ReificationFunctor Γ Δ : Functor (JudgmentsL _ _ (PCF n Γ Δ)) SystemFCa' (mapOptionTree brakifyJudg).
1348 refine {| fmor := ReificationFunctor_fmor Γ Δ |}; unfold hom; unfold ob; simpl ; intros.
1350 Definition PCF_SMME (n:nat)(Γ:TypeEnv)(Δ:CoercionEnv Γ) : ProgrammingLanguageSMME.
1351 refine {| plsmme_pl := PCF n Γ Δ |}.
1354 Definition SystemFCa_SMME (n:nat)(Γ:TypeEnv)(Δ:CoercionEnv Γ) : ProgrammingLanguageSMME.
1355 refine {| plsmme_pl := SystemFCa n Γ Δ |}.
1358 Definition ReificationFunctorMonoidal n : MonoidalFunctor (JudgmentsN n) (JudgmentsN (S n)) (ReificationFunctor n).
1362 Definition PCF_SystemFCa_two_level n Γ Δ : TwoLevelLanguage (PCF_SMME n Γ Δ) (SystemFCa_SMME (S n) Γ Δ).
1365 (* ... and the retraction exists *)
1369 Implicit Arguments garrow [ ].