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 pcfjudg2judg ec (cj:PCFJudg ec) :=
94 match cj with (Σ,τ) => Γ > Δ > (Σ @@@ (ec::nil)) |- (τ @@@ (ec::nil)) end.
96 (* Rules allowed in PCF; i.e. rules we know how to turn into GArrows *)
97 (* Rule_PCF consists of the rules allowed in flat PCF: everything except *)
98 (* AppT, AbsT, AppC, AbsC, Cast, Global, and some Case statements *)
99 Inductive Rule_PCF (ec:HaskTyVar Γ ★)
100 : forall (h c:Tree ??(PCFJudg ec)), Rule (mapOptionTree (pcfjudg2judg ec) h) (mapOptionTree (pcfjudg2judg ec) c) -> Type :=
101 | PCF_RArrange : ∀ x y t a, Rule_PCF ec [(_, _)] [(_, _)] (RArrange Γ Δ (x@@@(ec::nil)) (y@@@(ec::nil)) (t@@@(ec::nil)) a)
102 | PCF_RLit : ∀ lit , Rule_PCF ec [ ] [ ([],[_]) ] (RLit Γ Δ lit (ec::nil))
103 | PCF_RNote : ∀ Σ τ n , Rule_PCF ec [(_,[_])] [(_,[_])] (RNote Γ Δ (Σ@@@(ec::nil)) τ (ec::nil) n)
104 | PCF_RVar : ∀ σ , Rule_PCF ec [ ] [([_],[_])] (RVar Γ Δ σ (ec::nil) )
105 | PCF_RLam : ∀ Σ tx te , Rule_PCF ec [((_,,[_]),[_])] [(_,[_])] (RLam Γ Δ (Σ@@@(ec::nil)) tx te (ec::nil) )
107 | PCF_RApp : ∀ Σ Σ' tx te ,
108 Rule_PCF ec ([(_,[_])],,[(_,[_])]) [((_,,_),[_])]
109 (RApp Γ Δ (Σ@@@(ec::nil))(Σ'@@@(ec::nil)) tx te (ec::nil))
111 | PCF_RLet : ∀ Σ Σ' σ₂ p,
112 Rule_PCF ec ([(_,[_])],,[((_,,[_]),[_])]) [((_,,_),[_])]
113 (RLet Γ Δ (Σ@@@(ec::nil)) (Σ'@@@(ec::nil)) σ₂ p (ec::nil))
115 | PCF_RVoid : Rule_PCF ec [ ] [([],[])] (RVoid Γ Δ )
116 (*| PCF_RLetRec : ∀ Σ₁ τ₁ τ₂ , Rule_PCF (ec::nil) _ _ (RLetRec Γ Δ Σ₁ τ₁ τ₂ (ec::nil) )*)
117 | PCF_RJoin : ∀ Σ₁ Σ₂ τ₁ τ₂, Rule_PCF ec ([(_,_)],,[(_,_)]) [((_,,_),(_,,_))]
118 (RJoin Γ Δ (Σ₁@@@(ec::nil)) (Σ₂@@@(ec::nil)) (τ₁@@@(ec::nil)) (τ₂@@@(ec::nil))).
119 (* need int/boolean case *)
120 Implicit Arguments Rule_PCF [ ].
122 Definition PCFRule lev h c := { r:_ & @Rule_PCF lev h c r }.
125 Definition mkEsc Γ Δ ec (h:Tree ??(PCFJudg Γ ec))
127 (mapOptionTree (brakify Γ Δ) h)
128 (mapOptionTree (pcfjudg2judg Γ Δ ec) h).
129 apply nd_replicate; intros.
130 destruct o; simpl in *.
136 apply (Prelude_error "mkEsc got multi-leaf succedent").
139 Definition mkBrak Γ Δ ec (h:Tree ??(PCFJudg Γ ec))
141 (mapOptionTree (pcfjudg2judg Γ Δ ec) h)
142 (mapOptionTree (brakify Γ Δ) h).
143 apply nd_replicate; intros.
144 destruct o; simpl in *.
150 apply (Prelude_error "mkBrak got multi-leaf succedent").
153 Definition pcfToND Γ Δ : forall ec h c,
154 ND (PCFRule Γ Δ ec) h c -> ND Rule (mapOptionTree (pcfjudg2judg Γ Δ ec) h) (mapOptionTree (pcfjudg2judg Γ Δ ec) c).
156 eapply (fun q => nd_map' _ q X).
163 Instance OrgPCF Γ Δ lev : @ND_Relation _ (PCFRule Γ Δ lev) :=
164 { ndr_eqv := fun a b f g => (pcfToND _ _ _ _ _ f) === (pcfToND _ _ _ _ _ g) }.
167 Hint Constructors Rule_Flat.
169 Definition PCF_Arrange {Γ}{Δ}{lev} : forall x y z, Arrange x y -> ND (PCFRule Γ Δ lev) [(x,z)] [(y,z)].
173 Definition PCF_cut Γ Δ lev : forall a b c, ND (PCFRule Γ Δ lev) ([(a,b)],,[(b,c)]) [(a,c)].
180 (* when the cut is a single leaf and the RHS is a single leaf: *)
184 apply (PCF_Arrange [h] ([],,[h]) [h0]).
186 eapply nd_comp; [ idtac | apply (PCF_Arrange ([],,a) a [h0]); apply RCanL ].
189 set (@RLet Γ Δ [] (a@@@(ec::nil)) h0 h (ec::nil)) as q.
191 apply (PCF_RLet _ [] a h0 h).
192 apply (Prelude_error "cut rule invoked with [a|=[b]] [[b]|=[]]").
193 apply (Prelude_error "cut rule invoked with [a|=[b]] [[b]|=[x,,y]]").
194 apply (Prelude_error "cut rule invoked with [a|=[]] [[]|=c]").
195 apply (Prelude_error "cut rule invoked with [a|=[b,,c]] [[b,,c]|=z]").
199 Instance PCF_sequents Γ Δ lev ec : @SequentND _ (PCFRule Γ Δ lev) _ (pcfjudg Γ ec) :=
200 { snd_cut := PCF_cut Γ Δ lev }.
201 apply Build_SequentND.
206 exists (RVar _ _ _ _).
212 eapply nd_comp; [ apply nd_llecnac | idtac ].
213 apply (nd_prod IHa1 IHa2).
215 exists (RJoin _ _ _ _ _ _).
220 Definition PCF_left Γ Δ lev a b c : ND (PCFRule Γ Δ lev) [(b,c)] [((a,,b),(a,,c))].
221 eapply nd_comp; [ apply nd_llecnac | eapply nd_comp; [ idtac | idtac ] ].
222 eapply nd_prod; [ apply snd_initial | apply nd_id ].
224 set (@PCF_RJoin Γ Δ lev a b a c) as q'.
225 refine (existT _ _ _).
229 Definition PCF_right Γ Δ lev a b c : ND (PCFRule Γ Δ lev) [(b,c)] [((b,,a),(c,,a))].
230 eapply nd_comp; [ apply nd_rlecnac | eapply nd_comp; [ idtac | idtac ] ].
231 eapply nd_prod; [ apply nd_id | apply snd_initial ].
233 set (@PCF_RJoin Γ Δ lev b a c a) as q'.
234 refine (existT _ _ _).
238 Instance PCF_sequent_join Γ Δ lev : @ContextND _ (PCFRule Γ Δ lev) _ (pcfjudg Γ lev) _ :=
239 { cnd_expand_left := fun a b c => PCF_left Γ Δ lev c a b
240 ; cnd_expand_right := fun a b c => PCF_right Γ Δ lev c a b }.
242 intros; apply nd_rule. unfold PCFRule. simpl.
243 exists (RArrange _ _ _ _ _ (RCossa _ _ _)).
244 apply (PCF_RArrange _ _ lev ((a,,b),,c) (a,,(b,,c)) x).
246 intros; apply nd_rule. unfold PCFRule. simpl.
247 exists (RArrange _ _ _ _ _ (RAssoc _ _ _)).
248 apply (PCF_RArrange _ _ lev (a,,(b,,c)) ((a,,b),,c) x).
250 intros; apply nd_rule. unfold PCFRule. simpl.
251 exists (RArrange _ _ _ _ _ (RCanL _)).
252 apply (PCF_RArrange _ _ lev ([],,a) _ _).
254 intros; apply nd_rule. unfold PCFRule. simpl.
255 exists (RArrange _ _ _ _ _ (RCanR _)).
256 apply (PCF_RArrange _ _ lev (a,,[]) _ _).
258 intros; apply nd_rule. unfold PCFRule. simpl.
259 exists (RArrange _ _ _ _ _ (RuCanL _)).
260 apply (PCF_RArrange _ _ lev _ ([],,a) _).
262 intros; apply nd_rule. unfold PCFRule. simpl.
263 exists (RArrange _ _ _ _ _ (RuCanR _)).
264 apply (PCF_RArrange _ _ lev _ (a,,[]) _).
267 Instance OrgPCF_SequentND_Relation Γ Δ lev : SequentND_Relation (PCF_sequent_join Γ Δ lev) (OrgPCF Γ Δ lev).
271 Definition OrgPCF_ContextND_Relation Γ Δ lev
272 : @ContextND_Relation _ _ _ _ _ (PCF_sequent_join Γ Δ lev) (OrgPCF Γ Δ lev) (OrgPCF_SequentND_Relation Γ Δ lev).
277 Instance PCF Γ Δ lev : ProgrammingLanguage :=
278 { pl_cnd := PCF_sequent_join Γ Δ lev
279 ; pl_eqv := OrgPCF_ContextND_Relation Γ Δ lev