1 (*********************************************************************************************************************************)
2 (* HaskProofFlattener: *)
4 (* The Flattening Functor. *)
6 (*********************************************************************************************************************************)
8 Generalizable All Variables.
9 Require Import Preamble.
10 Require Import General.
11 Require Import NaturalDeduction.
12 Require Import Coq.Strings.String.
13 Require Import Coq.Lists.List.
15 Require Import HaskKinds.
16 Require Import HaskCoreTypes.
17 Require Import HaskLiteralsAndTyCons.
18 Require Import HaskStrongTypes.
19 Require Import HaskProof.
20 Require Import NaturalDeduction.
21 Require Import NaturalDeductionCategory.
23 Require Import Algebras_ch4.
24 Require Import Categories_ch1_3.
25 Require Import Functors_ch1_4.
26 Require Import Isomorphisms_ch1_5.
27 Require Import ProductCategories_ch1_6_1.
28 Require Import OppositeCategories_ch1_6_2.
29 Require Import Enrichment_ch2_8.
30 Require Import Subcategories_ch7_1.
31 Require Import NaturalTransformations_ch7_4.
32 Require Import NaturalIsomorphisms_ch7_5.
33 Require Import BinoidalCategories.
34 Require Import PreMonoidalCategories.
35 Require Import MonoidalCategories_ch7_8.
36 Require Import Coherence_ch7_8.
38 Require Import HaskStrongTypes.
39 Require Import HaskStrong.
40 Require Import HaskProof.
41 Require Import HaskStrongToProof.
42 Require Import HaskProofToStrong.
43 Require Import ProgrammingLanguage.
44 Require Import HaskProofStratified.
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)
56 Section HaskProofFlattener.
59 Context {Δ:CoercionEnv Γ}.
60 Context {ec:HaskTyVar Γ ★}.
62 Lemma unlev_lemma : forall (x:Tree ??(HaskType Γ ★)) lev, x = mapOptionTree unlev (x @@@ lev).
64 rewrite <- mapOptionTree_compose.
67 destruct a; simpl; auto.
74 Context (ga_rep : Tree ??(HaskType Γ ★) -> HaskType Γ ★ ).
75 Context (ga_type : HaskType Γ ★ -> HaskType Γ ★ -> HaskType Γ ★).
77 Lemma magic : forall a b c,
78 ([] ~~{TypesL (SystemFCa Γ Δ)}~~> [ga_type a b @@ nil]) ->
79 ([ga_type b c @@ nil] ~~{TypesL (SystemFCa Γ Δ)}~~> [ga_type a c @@ nil]).
83 Context (ga_lit : forall lit, [] ~~{TypesL (SystemFCa Γ Δ)}~~> [ga_type (ga_rep [] ) (ga_rep [literalType lit])@@ nil]).
84 Context (ga_id : forall σ, [] ~~{TypesL (SystemFCa Γ Δ)}~~> [ga_type (ga_rep σ ) (ga_rep σ )@@ nil]).
85 Context (ga_cancell : forall c , [] ~~{TypesL (SystemFCa Γ Δ)}~~> [ga_type (ga_rep ([],,c)) (ga_rep c )@@ nil]).
86 Context (ga_cancelr : forall c , [] ~~{TypesL (SystemFCa Γ Δ)}~~> [ga_type (ga_rep (c,,[])) (ga_rep c )@@ nil]).
87 Context (ga_uncancell : forall c , [] ~~{TypesL (SystemFCa Γ Δ)}~~> [ga_type (ga_rep c ) (ga_rep ([],,c) )@@ nil]).
88 Context (ga_uncancelr : forall c , [] ~~{TypesL (SystemFCa Γ Δ)}~~> [ga_type (ga_rep c ) (ga_rep (c,,[]) )@@ nil]).
89 Context (ga_assoc : forall a b c, [] ~~{TypesL (SystemFCa Γ Δ)}~~> [ga_type (ga_rep ((a,,b),,c)) (ga_rep (a,,(b,,c)) )@@ nil]).
90 Context (ga_unassoc : forall a b c, [] ~~{TypesL (SystemFCa Γ Δ)}~~> [ga_type (ga_rep ( a,,(b,,c))) (ga_rep ((a,,b),,c)) @@ nil]).
91 Context (ga_swap : forall a b, [] ~~{TypesL (SystemFCa Γ Δ)}~~> [ga_type (ga_rep (a,,b) ) (ga_rep (b,,a) )@@ nil]).
92 Context (ga_copy : forall a , [] ~~{TypesL (SystemFCa Γ Δ)}~~> [ga_type (ga_rep a ) (ga_rep (a,,a) )@@ nil]).
93 Context (ga_drop : forall a , [] ~~{TypesL (SystemFCa Γ Δ)}~~> [ga_type (ga_rep a ) (ga_rep [] )@@ nil]).
94 Context (ga_first : forall a b c, [ga_type (ga_rep a) (ga_rep b) @@nil] ~~{TypesL (SystemFCa Γ Δ)}~~> [ga_type (ga_rep (a,,c)) (ga_rep (b,,c)) @@nil]).
95 Context (ga_second : forall a b c, [ga_type (ga_rep a) (ga_rep b) @@nil] ~~{TypesL (SystemFCa Γ Δ)}~~> [ga_type (ga_rep (c,,a)) (ga_rep (c,,b)) @@nil]).
96 Context (ga_comp : forall a b c,
97 [ga_type (ga_rep a) (ga_rep b) @@nil],,[ga_type (ga_rep b) (ga_rep c) @@nil]
98 ~~{TypesL (SystemFCa Γ Δ)}~~>
99 [ga_type (ga_rep a) (ga_rep c) @@nil]).
101 Definition guestJudgmentAsGArrowType (lt:PCFJudg Γ ec) : HaskType Γ ★ :=
103 (x,y) => (ga_type (ga_rep x) (ga_rep y))
106 Definition obact (X:Tree ??(PCFJudg Γ ec)) : Tree ??(LeveledHaskType Γ ★) :=
107 mapOptionTree guestJudgmentAsGArrowType X @@@ nil.
109 Hint Constructors Rule_Flat.
110 Context {ndr:@ND_Relation _ Rule}.
113 * Here it is, what you've all been waiting for! When reading this,
114 * it might help to have the definition for "Inductive ND" (see
115 * NaturalDeduction.v) handy as a cross-reference.
117 Hint Constructors Rule_Flat.
118 Definition FlatteningFunctor_fmor
120 (h~~{JudgmentsL (PCF Γ Δ ec)}~~>c) ->
121 ((obact h)~~{TypesL (SystemFCa Γ Δ)}~~>(obact c)).
123 set (@nil (HaskTyVar Γ ★)) as lev.
125 unfold hom; unfold ob; unfold ehom; simpl; unfold pmon_I; unfold obact; intros.
129 (* the proof from no hypotheses of no conclusions (nd_id0) becomes RVoid *)
130 apply nd_rule; apply (org_fc _ _ [] [(_,_)] (RVoid _ _)). apply Flat_RVoid.
132 (* the proof from hypothesis X of conclusion X (nd_id1) becomes RVar *)
133 apply nd_rule; apply (org_fc _ _ [] [(_,_)] (RVar _ _ _ _)). apply Flat_RVar.
135 (* the proof from hypothesis X of no conclusions (nd_weak) becomes RWeak;;RVoid *)
139 ; eapply (org_fc _ _ [(_,_)] [(_,_)] (RArrange _ _ _ _ _ (RWeak _)))
142 eapply (org_fc _ _ [] [(_,_)] (RVoid _ _)); auto. apply Flat_RVoid.
145 (* the proof from hypothesis X of two identical conclusions X,,X (nd_copy) becomes RVar;;RJoin;;RCont *)
146 eapply nd_comp; [ idtac | eapply nd_rule; eapply (org_fc _ _ [(_,_)] [(_,_)] (RArrange _ _ _ _ _ (RCont _))) ].
147 eapply nd_comp; [ apply nd_llecnac | idtac ].
148 set (snd_initial(SequentND:=pl_snd(ProgrammingLanguage:=SystemFCa Γ Δ))
149 (mapOptionTree (guestJudgmentAsGArrowType) h @@@ lev)) as q.
155 eapply (org_fc _ _ ([(_,_)],,[(_,_)]) [(_,_)] (RJoin _ _ _ _ _ _ )).
164 (* nd_prod becomes nd_llecnac;;nd_prod;;RJoin *)
166 apply (nd_llecnac ;; nd_prod IHX1 IHX2).
168 eapply (org_fc _ _ ([(_,_)],,[(_,_)]) [(_,_)] (RJoin _ _ _ _ _ _ )).
169 apply (Flat_RJoin Γ Δ (mapOptionTree guestJudgmentAsGArrowType h1 @@@ nil)
170 (mapOptionTree guestJudgmentAsGArrowType h2 @@@ nil)
171 (mapOptionTree guestJudgmentAsGArrowType c1 @@@ nil)
172 (mapOptionTree guestJudgmentAsGArrowType c2 @@@ nil)).
174 (* nd_comp becomes pl_subst (aka nd_cut) *)
176 apply (nd_llecnac ;; nd_prod IHX1 IHX2).
177 clear IHX1 IHX2 X1 X2.
178 apply (@snd_cut _ _ _ _ (pl_snd(ProgrammingLanguage:=SystemFCa Γ Δ))).
180 (* nd_cancell becomes RVar;;RuCanL *)
182 [ idtac | eapply nd_rule; apply (org_fc _ _ [(_,_)] [(_,_)] (RArrange _ _ _ _ _ (RuCanL _))) ].
183 apply (snd_initial(SequentND:=pl_cnd(ProgrammingLanguage:=(SystemFCa Γ Δ)))).
186 (* nd_cancelr becomes RVar;;RuCanR *)
188 [ idtac | eapply nd_rule; apply (org_fc _ _ [(_,_)] [(_,_)] (RArrange _ _ _ _ _ (RuCanR _))) ].
189 apply (snd_initial(SequentND:=pl_cnd(ProgrammingLanguage:=(SystemFCa Γ Δ)))).
192 (* nd_llecnac becomes RVar;;RCanL *)
194 [ idtac | eapply nd_rule; apply (org_fc _ _ [(_,_)] [(_,_)] (RArrange _ _ _ _ _ (RCanL _))) ].
195 apply (snd_initial(SequentND:=pl_cnd(ProgrammingLanguage:=(SystemFCa Γ Δ)))).
198 (* nd_rlecnac becomes RVar;;RCanR *)
200 [ idtac | eapply nd_rule; apply (org_fc _ _ [(_,_)] [(_,_)] (RArrange _ _ _ _ _ (RCanR _))) ].
201 apply (snd_initial(SequentND:=pl_cnd(ProgrammingLanguage:=(SystemFCa Γ Δ)))).
204 (* nd_assoc becomes RVar;;RAssoc *)
206 [ idtac | eapply nd_rule; apply (org_fc _ _ [(_,_)] [(_,_)] (RArrange _ _ _ _ _ (RAssoc _ _ _))) ].
207 apply (snd_initial(SequentND:=pl_cnd(ProgrammingLanguage:=(SystemFCa Γ Δ)))).
210 (* nd_cossa becomes RVar;;RCossa *)
212 [ idtac | eapply nd_rule; apply (org_fc _ _ [(_,_)] [(_,_)] (RArrange _ _ _ _ _ (RCossa _ _ _))) ].
213 apply (snd_initial(SequentND:=pl_cnd(ProgrammingLanguage:=(SystemFCa Γ Δ)))).
216 destruct r as [r rp].
221 refine (match rp as R in @Rule_PCF _ _ _ H C _
224 [sequent (mapOptionTree guestJudgmentAsGArrowType H @@@ nil)
225 (mapOptionTree guestJudgmentAsGArrowType C @@@ nil)]
227 | PCF_RArrange h c r q => let case_RURule := tt in _
228 | PCF_RLit lit => let case_RLit := tt in _
229 | PCF_RNote Σ τ n => let case_RNote := tt in _
230 | PCF_RVar σ => let case_RVar := tt in _
231 | PCF_RLam Σ tx te => let case_RLam := tt in _
232 | PCF_RApp Σ tx te p => let case_RApp := tt in _
233 | PCF_RLet Σ σ₁ σ₂ p => let case_RLet := tt in _
234 | PCF_RJoin b c d e => let case_RJoin := tt in _
235 | PCF_RVoid => let case_RVoid := tt in _
236 (*| PCF_RCase T κlen κ θ l x => let case_RCase := tt in _*)
237 (*| PCF_RLetRec Σ₁ τ₁ τ₂ lev => let case_RLetRec := tt in _*)
241 rewrite (unlev_lemma h (ec::nil)).
242 rewrite (unlev_lemma c (ec::nil)).
243 destruct case_RURule.
244 refine (match q as Q in Arrange H C
246 H=(h @@@ (ec :: nil)) ->
247 C=(c @@@ (ec :: nil)) ->
250 [ga_type (ga_rep (mapOptionTree unlev H)) (ga_rep r) @@ nil ]
251 [ga_type (ga_rep (mapOptionTree unlev C)) (ga_rep r) @@ nil ] ]
253 | RLeft a b c r => let case_RLeft := tt in _
254 | RRight a b c r => let case_RRight := tt in _
255 | RCanL b => let case_RCanL := tt in _
256 | RCanR b => let case_RCanR := tt in _
257 | RuCanL b => let case_RuCanL := tt in _
258 | RuCanR b => let case_RuCanR := tt in _
259 | RAssoc b c d => let case_RAssoc := tt in _
260 | RCossa b c d => let case_RCossa := tt in _
261 | RExch b c => let case_RExch := tt in _
262 | RWeak b => let case_RWeak := tt in _
263 | RCont b => let case_RCont := tt in _
264 | RComp a b c f g => let case_RComp := tt in _
265 end (refl_equal _) (refl_equal _));
268 try rewrite <- unlev_lemma in *.
278 destruct case_RuCanL.
282 destruct case_RuCanR.
286 destruct case_RAssoc.
290 destruct case_RCossa.
311 destruct case_RRight.
324 (* hey cool, I figured out how to pass CoreNote's through... *)
328 eapply (org_fc _ _ [] [(_,_)] (RVar _ _ _ _)) . auto.
331 apply (org_fc _ _ [(_,_)] [(_,_)] (RNote _ _ _ _ _ n)). auto.
338 * class GArrow g (**) u => GArrowApply g (**) u (~>) where
339 * ga_applyl :: g (x**(x~>y) ) y
340 * ga_applyr :: g ( (x~>y)**x) y
342 * class GArrow g (**) u => GArrowCurry g (**) u (~>) where
343 * ga_curryl :: g (x**y) z -> g x (y~>z)
344 * ga_curryr :: g (x**y) z -> g y (x~>z)
347 (* GArrowCurry.ga_curry *)
351 (* GArrowApply.ga_apply *)
361 (* this assumes we want effects to occur in syntactically-left-to-right order *)
366 Instance FlatteningFunctor {Γ}{Δ}{ec} : Functor (JudgmentsL (PCF Γ Δ ec)) (TypesL (SystemFCa Γ Δ)) (obact) :=
367 { fmor := FlatteningFunctor_fmor }.
370 Definition ReificationFunctor Γ Δ : Functor (JudgmentsL _ _ (PCF n Γ Δ)) SystemFCa' (mapOptionTree brakifyJudg).
371 refine {| fmor := ReificationFunctor_fmor Γ Δ |}; unfold hom; unfold ob; simpl ; intros.
374 Definition PCF_SMME (n:nat)(Γ:TypeEnv)(Δ:CoercionEnv Γ) : ProgrammingLanguageSMME.
375 refine {| plsmme_pl := PCF n Γ Δ |}.
379 Definition SystemFCa_SMME (n:nat)(Γ:TypeEnv)(Δ:CoercionEnv Γ) : ProgrammingLanguageSMME.
380 refine {| plsmme_pl := SystemFCa n Γ Δ |}.
384 Definition ReificationFunctorMonoidal n : MonoidalFunctor (JudgmentsN n) (JudgmentsN (S n)) (ReificationFunctor n).
389 Definition PCF_SystemFCa_two_level n Γ Δ : TwoLevelLanguage (PCF_SMME n Γ Δ) (SystemFCa_SMME (S n) Γ Δ).
393 (* ... and the retraction exists *)
395 End HaskProofFlattener.