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 HaskLiterals.
33 Require Import HaskTyCons.
34 Require Import HaskStrongTypes.
35 Require Import HaskProof.
36 Require Import NaturalDeduction.
37 Require Import NaturalDeductionCategory.
39 Require Import HaskStrongTypes.
40 Require Import HaskStrong.
41 Require Import HaskProof.
42 Require Import HaskStrongToProof.
43 Require Import HaskProofToStrong.
44 Require Import ProgrammingLanguage.
50 * The flattening transformation. Currently only TWO-level languages are
51 * supported, and the level-1 sublanguage is rather limited.
53 * This file abuses terminology pretty badly. For purposes of this file,
54 * "PCF" means "the level-1 sublanguage" and "FC" (aka System FC) means
55 * the whole language (level-0 language including bracketed level-1 terms)
61 Context {ndr_systemfc:@ND_Relation _ Rule}.
62 Context Γ (Δ:CoercionEnv Γ).
64 Definition PCFJudg (ec:HaskTyVar Γ ECKind) :=
65 @prod (Tree ??(HaskType Γ ★)) (Tree ??(HaskType Γ ★)).
66 Definition pcfjudg (ec:HaskTyVar Γ ECKind) :=
67 @pair (Tree ??(HaskType Γ ★)) (Tree ??(HaskType Γ ★)).
69 (* given an PCFJudg at depth (ec::depth) we can turn it into an PCFJudg
70 * from depth (depth) by wrapping brackets around everything in the
71 * succedent and repopulating *)
72 Definition brakify {ec} (j:PCFJudg ec) : Judg :=
74 (Σ,τ) => Γ > Δ > (Σ@@@(ec::nil)) |- (mapOptionTree (fun t => HaskBrak ec t) τ @@@ nil)
77 Definition pcf_vars {Γ}(ec:HaskTyVar Γ ECKind)(t:Tree ??(LeveledHaskType Γ ★)) : Tree ??(HaskType Γ ★)
78 := mapOptionTreeAndFlatten (fun lt =>
79 match lt with t @@ l => match l with
80 | ec'::nil => if eqd_dec ec ec' then [t] else []
85 Inductive MatchingJudgments {ec} : Tree ??(PCFJudg ec) -> Tree ??Judg -> Type :=
86 | match_nil : MatchingJudgments [] []
87 | match_branch : forall a b c d, MatchingJudgments a b -> MatchingJudgments c d -> MatchingJudgments (a,,c) (b,,d)
91 [((pcf_vars ec Σ) , τ )]
92 [Γ > Δ > Σ |- (mapOptionTree (HaskBrak ec) τ @@@ lev)].
94 Definition pcfjudg2judg ec (cj:PCFJudg ec) :=
95 match cj with (Σ,τ) => Γ > Δ > (Σ @@@ (ec::nil)) |- (τ @@@ (ec::nil)) end.
97 (* Rules allowed in PCF; i.e. rules we know how to turn into GArrows *)
98 (* Rule_PCF consists of the rules allowed in flat PCF: everything except *)
99 (* AppT, AbsT, AppC, AbsC, Cast, Global, and some Case statements *)
100 Inductive Rule_PCF (ec:HaskTyVar Γ ECKind)
101 : forall (h c:Tree ??(PCFJudg ec)), Rule (mapOptionTree (pcfjudg2judg ec) h) (mapOptionTree (pcfjudg2judg ec) c) -> Type :=
102 | PCF_RArrange : ∀ x y t a, Rule_PCF ec [(_, _)] [(_, _)] (RArrange Γ Δ (x@@@(ec::nil)) (y@@@(ec::nil)) (t@@@(ec::nil)) a)
103 | PCF_RLit : ∀ lit , Rule_PCF ec [ ] [ ([],[_]) ] (RLit Γ Δ lit (ec::nil))
104 | PCF_RNote : ∀ Σ τ n , Rule_PCF ec [(_,[_])] [(_,[_])] (RNote Γ Δ (Σ@@@(ec::nil)) τ (ec::nil) n)
105 | PCF_RVar : ∀ σ , Rule_PCF ec [ ] [([_],[_])] (RVar Γ Δ σ (ec::nil) )
106 | PCF_RLam : ∀ Σ tx te , Rule_PCF ec [((_,,[_]),[_])] [(_,[_])] (RLam Γ Δ (Σ@@@(ec::nil)) tx te (ec::nil) )
108 | PCF_RApp : ∀ Σ Σ' tx te ,
109 Rule_PCF ec ([(_,[_])],,[(_,[_])]) [((_,,_),[_])]
110 (RApp Γ Δ (Σ@@@(ec::nil))(Σ'@@@(ec::nil)) tx te (ec::nil))
112 | PCF_RLet : ∀ Σ Σ' σ₂ p,
113 Rule_PCF ec ([(_,[_])],,[((_,,[_]),[_])]) [((_,,_),[_])]
114 (RLet Γ Δ (Σ@@@(ec::nil)) (Σ'@@@(ec::nil)) σ₂ p (ec::nil))
116 | PCF_RVoid : Rule_PCF ec [ ] [([],[])] (RVoid Γ Δ )
117 (*| PCF_RLetRec : ∀ Σ₁ τ₁ τ₂ , Rule_PCF (ec::nil) _ _ (RLetRec Γ Δ Σ₁ τ₁ τ₂ (ec::nil) )*)
118 | PCF_RJoin : ∀ Σ₁ Σ₂ τ₁ τ₂, Rule_PCF ec ([(_,_)],,[(_,_)]) [((_,,_),(_,,_))]
119 (RJoin Γ Δ (Σ₁@@@(ec::nil)) (Σ₂@@@(ec::nil)) (τ₁@@@(ec::nil)) (τ₂@@@(ec::nil))).
120 (* need int/boolean case *)
121 Implicit Arguments Rule_PCF [ ].
123 Definition PCFRule lev h c := { r:_ & @Rule_PCF lev h c r }.
126 Definition mkEsc Γ Δ ec (h:Tree ??(PCFJudg Γ ec))
128 (mapOptionTree (brakify Γ Δ) h)
129 (mapOptionTree (pcfjudg2judg Γ Δ ec) h).
130 apply nd_replicate; intros.
131 destruct o; simpl in *.
137 apply (Prelude_error "mkEsc got multi-leaf succedent").
140 Definition mkBrak Γ Δ ec (h:Tree ??(PCFJudg Γ ec))
142 (mapOptionTree (pcfjudg2judg Γ Δ ec) h)
143 (mapOptionTree (brakify Γ Δ) h).
144 apply nd_replicate; intros.
145 destruct o; simpl in *.
151 apply (Prelude_error "mkBrak got multi-leaf succedent").
154 Definition pcfToND Γ Δ : forall ec h c,
155 ND (PCFRule Γ Δ ec) h c -> ND Rule (mapOptionTree (pcfjudg2judg Γ Δ ec) h) (mapOptionTree (pcfjudg2judg Γ Δ ec) c).
157 eapply (fun q => nd_map' _ q X).
164 Instance OrgPCF Γ Δ lev : @ND_Relation _ (PCFRule Γ Δ lev) :=
165 { ndr_eqv := fun a b f g => (pcfToND _ _ _ _ _ f) === (pcfToND _ _ _ _ _ g) }.
168 Hint Constructors Rule_Flat.
170 Definition PCF_Arrange {Γ}{Δ}{lev} : forall x y z, Arrange x y -> ND (PCFRule Γ Δ lev) [(x,z)] [(y,z)].
174 Definition PCF_cut Γ Δ lev : forall a b c, ND (PCFRule Γ Δ lev) ([(a,b)],,[(b,c)]) [(a,c)].
181 (* when the cut is a single leaf and the RHS is a single leaf: *)
185 apply (PCF_Arrange [h] ([],,[h]) [h0]).
187 eapply nd_comp; [ idtac | apply (PCF_Arrange ([],,a) a [h0]); apply ACanL ].
190 set (@RLet Γ Δ [] (a@@@(ec::nil)) h0 h (ec::nil)) as q.
192 apply (PCF_RLet _ [] a h0 h).
193 apply (Prelude_error "cut rule invoked with [a|=[b]] [[b]|=[]]").
194 apply (Prelude_error "cut rule invoked with [a|=[b]] [[b]|=[x,,y]]").
195 apply (Prelude_error "cut rule invoked with [a|=[]] [[]|=c]").
196 apply (Prelude_error "cut rule invoked with [a|=[b,,c]] [[b,,c]|=z]").
200 Instance PCF_sequents Γ Δ lev ec : @SequentND _ (PCFRule Γ Δ lev) _ (pcfjudg Γ ec) :=
201 { snd_cut := PCF_cut Γ Δ lev }.
202 apply Build_SequentND.
207 exists (RVar _ _ _ _).
213 eapply nd_comp; [ apply nd_llecnac | idtac ].
214 apply (nd_prod IHa1 IHa2).
216 exists (RJoin _ _ _ _ _ _).
221 Definition PCF_left Γ Δ lev a b c : ND (PCFRule Γ Δ lev) [(b,c)] [((a,,b),(a,,c))].
222 eapply nd_comp; [ apply nd_llecnac | eapply nd_comp; [ idtac | idtac ] ].
223 eapply nd_prod; [ apply snd_initial | apply nd_id ].
225 set (@PCF_RJoin Γ Δ lev a b a c) as q'.
226 refine (existT _ _ _).
230 Definition PCF_right Γ Δ lev a b c : ND (PCFRule Γ Δ lev) [(b,c)] [((b,,a),(c,,a))].
231 eapply nd_comp; [ apply nd_rlecnac | eapply nd_comp; [ idtac | idtac ] ].
232 eapply nd_prod; [ apply nd_id | apply snd_initial ].
234 set (@PCF_RJoin Γ Δ lev b a c a) as q'.
235 refine (existT _ _ _).
239 Instance PCF_sequent_join Γ Δ lev : @ContextND _ (PCFRule Γ Δ lev) _ (pcfjudg Γ lev) _ :=
240 { cnd_expand_left := fun a b c => PCF_left Γ Δ lev c a b
241 ; cnd_expand_right := fun a b c => PCF_right Γ Δ lev c a b }.
243 intros; apply nd_rule. unfold PCFRule. simpl.
244 exists (RArrange _ _ _ _ _ (AuAssoc _ _ _)).
245 apply (PCF_RArrange _ _ lev ((a,,b),,c) (a,,(b,,c)) x).
247 intros; apply nd_rule. unfold PCFRule. simpl.
248 exists (RArrange _ _ _ _ _ (AAssoc _ _ _)).
249 apply (PCF_RArrange _ _ lev (a,,(b,,c)) ((a,,b),,c) x).
251 intros; apply nd_rule. unfold PCFRule. simpl.
252 exists (RArrange _ _ _ _ _ (ACanL _)).
253 apply (PCF_RArrange _ _ lev ([],,a) _ _).
255 intros; apply nd_rule. unfold PCFRule. simpl.
256 exists (RArrange _ _ _ _ _ (ACanR _)).
257 apply (PCF_RArrange _ _ lev (a,,[]) _ _).
259 intros; apply nd_rule. unfold PCFRule. simpl.
260 exists (RArrange _ _ _ _ _ (AuCanL _)).
261 apply (PCF_RArrange _ _ lev _ ([],,a) _).
263 intros; apply nd_rule. unfold PCFRule. simpl.
264 exists (RArrange _ _ _ _ _ (AuCanR _)).
265 apply (PCF_RArrange _ _ lev _ (a,,[]) _).
268 Instance OrgPCF_SequentND_Relation Γ Δ lev : SequentND_Relation (PCF_sequent_join Γ Δ lev) (OrgPCF Γ Δ lev).
272 Definition OrgPCF_ContextND_Relation Γ Δ lev
273 : @ContextND_Relation _ _ _ _ _ (PCF_sequent_join Γ Δ lev) (OrgPCF Γ Δ lev) (OrgPCF_SequentND_Relation Γ Δ lev).
278 Instance PCF Γ Δ lev : ProgrammingLanguage :=
279 { pl_cnd := PCF_sequent_join Γ Δ lev
280 ; pl_eqv := OrgPCF_ContextND_Relation Γ Δ lev