1 (*********************************************************************************************************************************)
4 (* An alternate representation for HaskProof which ensures that deductions on a given level are grouped into contiguous *)
5 (* blocks. This representation lacks the attractive compositionality properties of HaskProof, but makes it easier to *)
6 (* perform the flattening process. *)
8 (*********************************************************************************************************************************)
10 Generalizable All Variables.
11 Require Import Preamble.
12 Require Import General.
13 Require Import NaturalDeduction.
14 Require Import Coq.Strings.String.
15 Require Import Coq.Lists.List.
17 Require Import Algebras_ch4.
18 Require Import Categories_ch1_3.
19 Require Import Functors_ch1_4.
20 Require Import Isomorphisms_ch1_5.
21 Require Import ProductCategories_ch1_6_1.
22 Require Import OppositeCategories_ch1_6_2.
23 Require Import Enrichment_ch2_8.
24 Require Import Subcategories_ch7_1.
25 Require Import NaturalTransformations_ch7_4.
26 Require Import NaturalIsomorphisms_ch7_5.
27 Require Import MonoidalCategories_ch7_8.
28 Require Import Coherence_ch7_8.
30 Require Import HaskKinds.
31 Require Import HaskCoreTypes.
32 Require Import HaskLiteralsAndTyCons.
33 Require Import HaskStrongTypes.
34 Require Import HaskProof.
35 Require Import NaturalDeduction.
36 Require Import NaturalDeductionCategory.
38 Require Import HaskStrongTypes.
39 Require Import HaskStrong.
40 Require Import HaskProof.
41 Require Import HaskStrongToProof.
42 Require Import HaskProofToStrong.
43 Require Import ProgrammingLanguage.
49 * The flattening transformation. Currently only TWO-level languages are
50 * supported, and the level-1 sublanguage is rather limited.
52 * This file abuses terminology pretty badly. For purposes of this file,
53 * "PCF" means "the level-1 sublanguage" and "FC" (aka System FC) means
54 * the whole language (level-0 language including bracketed level-1 terms)
60 Context {ndr_systemfc:@ND_Relation _ Rule}.
61 Context Γ (Δ:CoercionEnv Γ).
63 Definition PCFJudg (ec:HaskTyVar Γ ★) :=
64 @prod (Tree ??(HaskType Γ ★)) (Tree ??(HaskType Γ ★)).
65 Definition pcfjudg (ec:HaskTyVar Γ ★) :=
66 @pair (Tree ??(HaskType Γ ★)) (Tree ??(HaskType Γ ★)).
68 (* given an PCFJudg at depth (ec::depth) we can turn it into an PCFJudg
69 * from depth (depth) by wrapping brackets around everything in the
70 * succedent and repopulating *)
71 Definition brakify {ec} (j:PCFJudg ec) : Judg :=
73 (Σ,τ) => Γ > Δ > (Σ@@@(ec::nil)) |- (mapOptionTree (fun t => HaskBrak ec t) τ @@@ nil)
76 Definition pcf_vars {Γ}(ec:HaskTyVar Γ ★)(t:Tree ??(LeveledHaskType Γ ★)) : Tree ??(HaskType Γ ★)
77 := mapOptionTreeAndFlatten (fun lt =>
78 match lt with t @@ l => match l with
79 | ec'::nil => if eqd_dec ec ec' then [t] else []
84 Inductive MatchingJudgments {ec} : Tree ??(PCFJudg ec) -> Tree ??Judg -> Type :=
85 | match_nil : MatchingJudgments [] []
86 | match_branch : forall a b c d, MatchingJudgments a b -> MatchingJudgments c d -> MatchingJudgments (a,,c) (b,,d)
90 [((pcf_vars ec Σ) , τ )]
91 [Γ > Δ > Σ |- (mapOptionTree (HaskBrak ec) τ @@@ lev)].
93 Definition fc_vars {Γ}(ec:HaskTyVar Γ ★)(t:Tree ??(LeveledHaskType Γ ★)) : Tree ??(HaskType Γ ★)
94 := mapOptionTreeAndFlatten (fun lt =>
95 match lt with t @@ l => match l with
96 | ec'::nil => if eqd_dec ec ec' then [] else [t]
102 @prod (Tree ??(LeveledHaskType Γ ★)) (Tree ??(LeveledHaskType Γ ★)).
103 Definition fcjudg2judg (fc:FCJudg) :=
105 (x,y) => Γ > Δ > x |- y
107 Coercion fcjudg2judg : FCJudg >-> Judg.
109 Definition pcfjudg2judg ec (cj:PCFJudg ec) :=
110 match cj with (Σ,τ) => Γ > Δ > (Σ @@@ (ec::nil)) |- (τ @@@ (ec::nil)) end.
112 Definition pcfjudg2fcjudg ec (fc:PCFJudg ec) : FCJudg :=
114 (x,y) => (x @@@ (ec::nil),y @@@ (ec::nil))
117 (* Rules allowed in PCF; i.e. rules we know how to turn into GArrows *)
118 (* Rule_PCF consists of the rules allowed in flat PCF: everything except *)
119 (* AppT, AbsT, AppC, AbsC, Cast, Global, and some Case statements *)
120 Inductive Rule_PCF (ec:HaskTyVar Γ ★)
121 : forall (h c:Tree ??(PCFJudg ec)), Rule (mapOptionTree (pcfjudg2judg ec) h) (mapOptionTree (pcfjudg2judg ec) c) -> Type :=
122 | PCF_RArrange : ∀ x y t a, Rule_PCF ec [(_, _)] [(_, _)] (RArrange Γ Δ (x@@@(ec::nil)) (y@@@(ec::nil)) (t@@@(ec::nil)) a)
123 | PCF_RLit : ∀ lit , Rule_PCF ec [ ] [ ([],[_]) ] (RLit Γ Δ lit (ec::nil))
124 | PCF_RNote : ∀ Σ τ n , Rule_PCF ec [(_,[_])] [(_,[_])] (RNote Γ Δ (Σ@@@(ec::nil)) τ (ec::nil) n)
125 | PCF_RVar : ∀ σ , Rule_PCF ec [ ] [([_],[_])] (RVar Γ Δ σ (ec::nil) )
126 | PCF_RLam : ∀ Σ tx te , Rule_PCF ec [((_,,[_]),[_])] [(_,[_])] (RLam Γ Δ (Σ@@@(ec::nil)) tx te (ec::nil) )
128 | PCF_RApp : ∀ Σ Σ' tx te ,
129 Rule_PCF ec ([(_,[_])],,[(_,[_])]) [((_,,_),[_])]
130 (RApp Γ Δ (Σ@@@(ec::nil))(Σ'@@@(ec::nil)) tx te (ec::nil))
132 | PCF_RLet : ∀ Σ Σ' σ₂ p,
133 Rule_PCF ec ([(_,[_])],,[((_,,[_]),[_])]) [((_,,_),[_])]
134 (RLet Γ Δ (Σ@@@(ec::nil)) (Σ'@@@(ec::nil)) σ₂ p (ec::nil))
136 | PCF_RVoid : Rule_PCF ec [ ] [([],[])] (RVoid Γ Δ )
137 (*| PCF_RLetRec : ∀ Σ₁ τ₁ τ₂ , Rule_PCF (ec::nil) _ _ (RLetRec Γ Δ Σ₁ τ₁ τ₂ (ec::nil) )*)
138 | PCF_RJoin : ∀ Σ₁ Σ₂ τ₁ τ₂, Rule_PCF ec ([(_,_)],,[(_,_)]) [((_,,_),(_,,_))]
139 (RJoin Γ Δ (Σ₁@@@(ec::nil)) (Σ₂@@@(ec::nil)) (τ₁@@@(ec::nil)) (τ₂@@@(ec::nil))).
140 (* need int/boolean case *)
141 Implicit Arguments Rule_PCF [ ].
143 Definition PCFRule lev h c := { r:_ & @Rule_PCF lev h c r }.
146 Definition mkEsc Γ Δ ec (h:Tree ??(PCFJudg Γ ec))
148 (mapOptionTree (brakify Γ Δ) h)
149 (mapOptionTree (pcfjudg2judg Γ Δ ec) h).
150 apply nd_replicate; intros.
151 destruct o; simpl in *.
157 apply (Prelude_error "mkEsc got multi-leaf succedent").
160 Definition mkBrak Γ Δ ec (h:Tree ??(PCFJudg Γ ec))
162 (mapOptionTree (pcfjudg2judg Γ Δ ec) h)
163 (mapOptionTree (brakify Γ Δ) h).
164 apply nd_replicate; intros.
165 destruct o; simpl in *.
171 apply (Prelude_error "mkBrak got multi-leaf succedent").
175 Definition Partition {Γ} ec (Σ:Tree ??(LeveledHaskType Γ ★)) :=
177 fc_vars ec Σ = fst vars /\
178 pcf_vars ec Σ = snd vars }.
181 Definition pcfToND Γ Δ : forall ec h c,
182 ND (PCFRule Γ Δ ec) h c -> ND Rule (mapOptionTree (pcfjudg2judg Γ Δ ec) h) (mapOptionTree (pcfjudg2judg Γ Δ ec) c).
184 eapply (fun q => nd_map' _ q X).
191 Instance OrgPCF Γ Δ lev : @ND_Relation _ (PCFRule Γ Δ lev) :=
192 { ndr_eqv := fun a b f g => (pcfToND _ _ _ _ _ f) === (pcfToND _ _ _ _ _ g) }.
196 * An intermediate representation necessitated by Coq's termination
197 * conditions. This is basically a tree where each node is a
198 * subproof which is either entirely level-1 or entirely level-0
200 Inductive Alternating : Tree ??Judg -> Type :=
202 | alt_nil : Alternating []
204 | alt_branch : forall a b,
205 Alternating a -> Alternating b -> Alternating (a,,b)
207 | alt_fc : forall h c,
212 | alt_pcf : forall Γ Δ ec h c h' c',
213 MatchingJudgments Γ Δ h h' ->
214 MatchingJudgments Γ Δ c c' ->
216 ND (PCFRule Γ Δ ec) h c ->
219 Require Import Coq.Logic.Eqdep.
221 Lemma magic a b c d ec e :
222 ClosedSIND(Rule:=Rule) [a > b > c |- [d @@ (ec :: e)]] ->
223 ClosedSIND(Rule:=Rule) [a > b > pcf_vars ec c @@@ (ec :: nil) |- [d @@ (ec :: nil)]].
227 Definition orgify : forall Γ Δ Σ τ (pf:ClosedSIND(Rule:=Rule) [Γ > Δ > Σ |- τ]), Alternating [Γ > Δ > Σ |- τ].
230 fix orgify_fc' Γ Δ Σ τ (pf:ClosedSIND [Γ > Δ > Σ |- τ]) {struct pf} : Alternating [Γ > Δ > Σ |- τ] :=
231 let case_main := tt in _
232 with orgify_fc c (pf:ClosedSIND c) {struct pf} : Alternating c :=
233 (match c as C return C=c -> Alternating C with
234 | T_Leaf None => fun _ => alt_nil
235 | T_Leaf (Some (Γ > Δ > Σ |- τ)) => let case_leaf := tt in fun eqpf => _
236 | T_Branch b1 b2 => let case_branch := tt in fun eqpf => _
238 with orgify_pcf Γ Δ ec pcfj j (m:MatchingJudgments Γ Δ pcfj j)
239 (pf:ClosedSIND (mapOptionTree (pcfjudg2judg Γ Δ ec) pcfj)) {struct pf} : Alternating j :=
240 let case_pcf := tt in _
245 set (alt_fc _ _ (orgify_fc _ X) (nd_rule X0)) as backup.
246 refine (match X0 as R in Rule H C return
248 | T_Leaf (Some (Γ > Δ > Σ |- τ)) =>
249 h=H -> Alternating [Γ > Δ > Σ |- τ] -> Alternating [Γ > Δ > Σ |- τ]
253 | RBrak Σ a b c n m => let case_RBrak := tt in fun pf' backup => _
254 | REsc Σ a b c n m => let case_REsc := tt in fun pf' backup => _
255 | _ => fun pf' x => x
256 end (refl_equal _) backup).
257 clear backup0 backup.
261 set (@match_leaf Σ0 a ec n [b] m) as q.
262 set (orgify_pcf Σ0 a ec _ _ q) as q'.
270 apply (Prelude_error "encountered Esc in wrong side of mkalt").
277 destruct case_branch.
278 rewrite <- eqpf in pf.
280 apply no_rules_with_multiple_conclusions in X0.
282 exists b1. exists b2.
284 apply (alt_branch _ _ (orgify_fc _ X) (orgify_fc _ X0)).
289 Definition pcfify Γ Δ ec : forall Σ τ,
290 ClosedSIND(Rule:=Rule) [ Γ > Δ > Σ@@@(ec::nil) |- τ @@@ (ec::nil)]
291 -> ND (PCFRule Γ Δ ec) [] [(Σ,τ)].
294 fix pcfify Σ τ (pn:@ClosedSIND _ Rule [ Γ > Δ > Σ@@@(ec::nil) |- τ @@@ (ec::nil)]) {struct pn}
295 : ND (PCFRule Γ Δ ec) [] [(Σ,τ)] :=
296 (match pn in @ClosedSIND _ _ J return J=[Γ > Δ > Σ@@@(ec::nil) |- τ @@@ (ec::nil)] -> _ with
297 | cnd_weak => let case_nil := tt in _
298 | cnd_rule h c cnd' r => let case_rule := tt in _
299 | cnd_branch _ _ c1 c2 => let case_branch := tt in _
300 end (refl_equal _)))).
304 destruct c; try destruct o; inversion H.
309 Hint Constructors Rule_Flat.
311 Definition PCF_Arrange {Γ}{Δ}{lev} : forall x y z, Arrange x y -> ND (PCFRule Γ Δ lev) [(x,z)] [(y,z)].
315 Definition PCF_cut Γ Δ lev : forall a b c, ND (PCFRule Γ Δ lev) ([(a,b)],,[(b,c)]) [(a,c)].
322 (* when the cut is a single leaf and the RHS is a single leaf: *)
326 apply (PCF_Arrange [h] ([],,[h]) [h0]).
328 eapply nd_comp; [ idtac | apply (PCF_Arrange ([],,a) a [h0]); apply RCanL ].
331 set (@RLet Γ Δ [] (a@@@(ec::nil)) h0 h (ec::nil)) as q.
333 apply (PCF_RLet _ [] a h0 h).
334 apply (Prelude_error "cut rule invoked with [a|=[b]] [[b]|=[]]").
335 apply (Prelude_error "cut rule invoked with [a|=[b]] [[b]|=[x,,y]]").
336 apply (Prelude_error "cut rule invoked with [a|=[]] [[]|=c]").
337 apply (Prelude_error "cut rule invoked with [a|=[b,,c]] [[b,,c]|=z]").
341 Instance PCF_sequents Γ Δ lev ec : @SequentND _ (PCFRule Γ Δ lev) _ (pcfjudg Γ ec) :=
342 { snd_cut := PCF_cut Γ Δ lev }.
343 apply Build_SequentND.
348 exists (RVar _ _ _ _).
354 eapply nd_comp; [ apply nd_llecnac | idtac ].
355 apply (nd_prod IHa1 IHa2).
357 exists (RJoin _ _ _ _ _ _).
362 Definition PCF_left Γ Δ lev a b c : ND (PCFRule Γ Δ lev) [(b,c)] [((a,,b),(a,,c))].
363 eapply nd_comp; [ apply nd_llecnac | eapply nd_comp; [ idtac | idtac ] ].
364 eapply nd_prod; [ apply snd_initial | apply nd_id ].
366 set (@PCF_RJoin Γ Δ lev a b a c) as q'.
367 refine (existT _ _ _).
371 Definition PCF_right Γ Δ lev a b c : ND (PCFRule Γ Δ lev) [(b,c)] [((b,,a),(c,,a))].
372 eapply nd_comp; [ apply nd_rlecnac | eapply nd_comp; [ idtac | idtac ] ].
373 eapply nd_prod; [ apply nd_id | apply snd_initial ].
375 set (@PCF_RJoin Γ Δ lev b a c a) as q'.
376 refine (existT _ _ _).
380 Instance PCF_sequent_join Γ Δ lev : @ContextND _ (PCFRule Γ Δ lev) _ (pcfjudg Γ lev) _ :=
381 { cnd_expand_left := fun a b c => PCF_left Γ Δ lev c a b
382 ; cnd_expand_right := fun a b c => PCF_right Γ Δ lev c a b }.
384 intros; apply nd_rule. unfold PCFRule. simpl.
385 exists (RArrange _ _ _ _ _ (RCossa _ _ _)).
386 apply (PCF_RArrange _ _ lev ((a,,b),,c) (a,,(b,,c)) x).
388 intros; apply nd_rule. unfold PCFRule. simpl.
389 exists (RArrange _ _ _ _ _ (RAssoc _ _ _)).
390 apply (PCF_RArrange _ _ lev (a,,(b,,c)) ((a,,b),,c) x).
392 intros; apply nd_rule. unfold PCFRule. simpl.
393 exists (RArrange _ _ _ _ _ (RCanL _)).
394 apply (PCF_RArrange _ _ lev ([],,a) _ _).
396 intros; apply nd_rule. unfold PCFRule. simpl.
397 exists (RArrange _ _ _ _ _ (RCanR _)).
398 apply (PCF_RArrange _ _ lev (a,,[]) _ _).
400 intros; apply nd_rule. unfold PCFRule. simpl.
401 exists (RArrange _ _ _ _ _ (RuCanL _)).
402 apply (PCF_RArrange _ _ lev _ ([],,a) _).
404 intros; apply nd_rule. unfold PCFRule. simpl.
405 exists (RArrange _ _ _ _ _ (RuCanR _)).
406 apply (PCF_RArrange _ _ lev _ (a,,[]) _).
409 Instance OrgPCF_SequentND_Relation Γ Δ lev : SequentND_Relation (PCF_sequent_join Γ Δ lev) (OrgPCF Γ Δ lev).
413 Definition OrgPCF_ContextND_Relation Γ Δ lev
414 : @ContextND_Relation _ _ _ _ _ (PCF_sequent_join Γ Δ lev) (OrgPCF Γ Δ lev) (OrgPCF_SequentND_Relation Γ Δ lev).
419 Instance PCF Γ Δ lev : ProgrammingLanguage :=
420 { pl_cnd := PCF_sequent_join Γ Δ lev
421 ; pl_eqv := OrgPCF_ContextND_Relation Γ Δ lev