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.
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)
57 Section HaskProofFlattener.
61 Definition code2garrow0 {Γ}(ec t1 t2:RawHaskType Γ ★) : RawHaskType Γ ★.
64 Definition code2garrow Γ (ec t:RawHaskType Γ ★) :=
66 (* | TApp ★ ★ (TApp _ ★ TArrow tx) t' => code2garrow0 ec tx t'*)
67 | _ => code2garrow0 ec unitType t
70 Fixpoint typeMap {TV}{κ}(ty:@RawHaskType TV κ) : @RawHaskType TV κ :=
71 match ty as TY in RawHaskType _ K return RawHaskType TV K with
72 | TCode ec t => code2garrow _ ec t
73 | TApp _ _ t1 t2 => TApp (typeMap t1) (typeMap t2)
74 | TAll _ f => TAll _ (fun tv => typeMap (f tv))
75 | TCoerc _ t1 t2 t3 => TCoerc (typeMap t1) (typeMap t2) (typeMap t3)
79 | TyFunApp tf rhtl => (* FIXME *) TyFunApp tf rhtl
85 Definition code2garrow Γ (ec t:RawHaskType Γ ★) :=
87 (* | TApp ★ ★ (TApp _ ★ TArrow tx) t' => code2garrow0 ec tx t'*)
88 | _ => code2garrow0 ec unitType t
91 Fixpoint typeMap {TV}{κ}(ty:@RawHaskType TV κ) : @RawHaskType TV κ :=
92 match ty as TY in RawHaskType _ K return RawHaskType TV K with
93 | TCode ec t => code2garrow _ ec t
94 | TApp _ _ t1 t2 => TApp (typeMap t1) (typeMap t2)
95 | TAll _ f => TAll _ (fun tv => typeMap (f tv))
96 | TCoerc _ t1 t2 t3 => TCoerc (typeMap t1) (typeMap t2) (typeMap t3)
100 | TyFunApp tf rhtl => (* FIXME *) TyFunApp tf rhtl
103 Definition typeMapL {Γ}(lht:LeveledHaskType Γ ★) : LeveledHaskType Γ ★ :=
105 (* | t @@ nil => (fun TV ite => typeMap (t TV ite)) @@ lev*)
106 | t @@ lev => (fun TV ite => typeMap (t TV ite)) @@ lev
110 (* gathers a tree of guest-language types into a single host-language types via the tensor *)
111 Definition tensorizeType {Γ} (lt:Tree ??(HaskType Γ ★)) : HaskType Γ ★.
115 Definition mkGA {Γ} : HaskType Γ ★ -> HaskType Γ ★ -> HaskType Γ ★.
119 Definition guestJudgmentAsGArrowType {Γ}{Δ}(lt:PCFJudg Γ Δ) : HaskType Γ ★ :=
121 (x,y) => (mkGA (tensorizeType x) (tensorizeType y))
124 Definition obact {Γ}{Δ} (X:Tree ??(PCFJudg Γ Δ)) : Tree ??(LeveledHaskType Γ ★) :=
125 mapOptionTree guestJudgmentAsGArrowType X @@@ nil.
127 Hint Constructors Rule_Flat.
128 Context {ndr:@ND_Relation _ Rule}.
131 * Here it is, what you've all been waiting for! When reading this,
132 * it might help to have the definition for "Inductive ND" (see
133 * NaturalDeduction.v) handy as a cross-reference.
135 Hint Constructors Rule_Flat.
136 Definition FlatteningFunctor_fmor {Γ}{Δ}{ec}
138 (h~~{JudgmentsL (PCF Γ Δ ec)}~~>c) ->
139 ((obact(Δ:=ec) h)~~{TypesL (SystemFCa Γ Δ)}~~>(obact(Δ:=ec) c)).
141 set (@nil (HaskTyVar Γ ★)) as lev.
143 unfold hom; unfold ob; unfold ehom; simpl; unfold pmon_I; unfold obact; intros.
147 (* the proof from no hypotheses of no conclusions (nd_id0) becomes RVoid *)
148 apply nd_rule; apply (org_fc _ _ [] [(_,_)] (RVoid _ _)). apply Flat_RVoid.
150 (* the proof from hypothesis X of conclusion X (nd_id1) becomes RVar *)
151 apply nd_rule; apply (org_fc _ _ [] [(_,_)] (RVar _ _ _ _)). apply Flat_RVar.
153 (* the proof from hypothesis X of no conclusions (nd_weak) becomes RWeak;;RVoid *)
157 ; eapply (org_fc _ _ [(_,_)] [(_,_)] (RArrange _ _ _ _ _ (RWeak _)))
160 eapply (org_fc _ _ [] [(_,_)] (RVoid _ _)); auto. apply Flat_RVoid.
163 (* the proof from hypothesis X of two identical conclusions X,,X (nd_copy) becomes RVar;;RJoin;;RCont *)
164 eapply nd_comp; [ idtac | eapply nd_rule; eapply (org_fc _ _ [(_,_)] [(_,_)] (RArrange _ _ _ _ _ (RCont _))) ].
165 eapply nd_comp; [ apply nd_llecnac | idtac ].
166 set (snd_initial(SequentND:=pl_snd(ProgrammingLanguage:=SystemFCa Γ Δ))
167 (mapOptionTree (guestJudgmentAsGArrowType(Δ:=ec)) h @@@ lev)) as q.
173 eapply (org_fc _ _ ([(_,_)],,[(_,_)]) [(_,_)] (RJoin _ _ _ _ _ _ )).
182 (* nd_prod becomes nd_llecnac;;nd_prod;;RJoin *)
184 apply (nd_llecnac ;; nd_prod IHX1 IHX2).
186 eapply (org_fc _ _ ([(_,_)],,[(_,_)]) [(_,_)] (RJoin _ _ _ _ _ _ )).
187 apply (Flat_RJoin Γ Δ (mapOptionTree guestJudgmentAsGArrowType h1 @@@ nil)
188 (mapOptionTree guestJudgmentAsGArrowType h2 @@@ nil)
189 (mapOptionTree guestJudgmentAsGArrowType c1 @@@ nil)
190 (mapOptionTree guestJudgmentAsGArrowType c2 @@@ nil)).
192 (* nd_comp becomes pl_subst (aka nd_cut) *)
194 apply (nd_llecnac ;; nd_prod IHX1 IHX2).
195 clear IHX1 IHX2 X1 X2.
197 apply (@snd_cut _ _ _ _ _ _ (@pl_cnd _ _ _ _ (SystemFCa Γ Δ))).
201 (* nd_cancell becomes RVar;;RuCanL *)
203 [ idtac | eapply nd_rule; apply (org_fc _ _ [(_,_)] [(_,_)] (RArrange _ _ _ _ _ (RuCanL _))) ].
204 apply (snd_initial(SequentND:=pl_cnd(ProgrammingLanguage:=(SystemFCa Γ Δ)))).
207 (* nd_cancelr becomes RVar;;RuCanR *)
209 [ idtac | eapply nd_rule; apply (org_fc _ _ [(_,_)] [(_,_)] (RArrange _ _ _ _ _ (RuCanR _))) ].
210 apply (snd_initial(SequentND:=pl_cnd(ProgrammingLanguage:=(SystemFCa Γ Δ)))).
213 (* nd_llecnac becomes RVar;;RCanL *)
215 [ idtac | eapply nd_rule; apply (org_fc _ _ [(_,_)] [(_,_)] (RArrange _ _ _ _ _ (RCanL _))) ].
216 apply (snd_initial(SequentND:=pl_cnd(ProgrammingLanguage:=(SystemFCa Γ Δ)))).
219 (* nd_rlecnac becomes RVar;;RCanR *)
221 [ idtac | eapply nd_rule; apply (org_fc _ _ [(_,_)] [(_,_)] (RArrange _ _ _ _ _ (RCanR _))) ].
222 apply (snd_initial(SequentND:=pl_cnd(ProgrammingLanguage:=(SystemFCa Γ Δ)))).
225 (* nd_assoc becomes RVar;;RAssoc *)
227 [ idtac | eapply nd_rule; apply (org_fc _ _ [(_,_)] [(_,_)] (RArrange _ _ _ _ _ (RAssoc _ _ _))) ].
228 apply (snd_initial(SequentND:=pl_cnd(ProgrammingLanguage:=(SystemFCa Γ Δ)))).
231 (* nd_cossa becomes RVar;;RCossa *)
233 [ idtac | eapply nd_rule; apply (org_fc _ _ [(_,_)] [(_,_)] (RArrange _ _ _ _ _ (RCossa _ _ _))) ].
234 apply (snd_initial(SequentND:=pl_cnd(ProgrammingLanguage:=(SystemFCa Γ Δ)))).
237 destruct r as [r rp].
238 refine (match rp as R in @Rule_PCF _ _ _ H C _ with
239 | PCF_RArrange h c r q => let case_RURule := tt in _
240 | PCF_RLit lit => let case_RLit := tt in _
241 | PCF_RNote Σ τ n => let case_RNote := tt in _
242 | PCF_RVar σ => let case_RVar := tt in _
243 | PCF_RLam Σ tx te => let case_RLam := tt in _
244 | PCF_RApp Σ tx te p => let case_RApp := tt in _
245 | PCF_RLet Σ σ₁ σ₂ p => let case_RLet := tt in _
246 | PCF_RJoin b c d e => let case_RJoin := tt in _
247 | PCF_RVoid => let case_RVoid := tt in _
248 (*| PCF_RCase T κlen κ θ l x => let case_RCase := tt in _*)
249 (*| PCF_RLetRec Σ₁ τ₁ τ₂ lev => let case_RLetRec := tt in _*)
253 rename r0 into r; rename h0 into h; rename c0 into c.
255 destruct case_RURule.
257 | RLeft a b c r => let case_RLeft := tt in _
258 | RRight a b c r => let case_RRight := tt in _
259 | RCanL b => let case_RCanL := tt in _
260 | RCanR b => let case_RCanR := tt in _
261 | RuCanL b => let case_RuCanL := tt in _
262 | RuCanR b => let case_RuCanR := tt in _
263 | RAssoc b c d => let case_RAssoc := tt in _
264 | RCossa b c d => let case_RCossa := tt in _
265 | RExch b c => let case_RExch := tt in _
266 | RWeak b => let case_RWeak := tt in _
267 | RCont b => let case_RCont := tt in _
268 | RComp a b c f g => let case_RComp := tt in _
279 destruct case_RuCanL.
283 destruct case_RuCanR.
287 destruct case_RAssoc.
291 destruct case_RCossa.
311 destruct case_RRight.
323 (* hey cool, I figured out how to pass CoreNote's through... *)
327 eapply (org_fc _ _ [] [(_,_)] (RVar _ _ _ _)) . auto.
330 apply (org_fc _ _ [(_,_)] [(_,_)] (RNote _ _ _ _ _ n)). auto.
338 (* ga_curry, but try to avoid this someday in the future if the argument type isn't a function *)
346 (* ga_comp! perhaps this means the ga_curry avoidance can be done by turning lambdas into lets? *)
354 (* ga_first+ga_second; technically this assumes a specific evaluation order, which is bad *)
359 Instance FlatteningFunctor {Γ}{Δ}{ec} : Functor (JudgmentsL (PCF Γ Δ ec)) (TypesL (SystemFCa Γ Δ)) (obact) :=
360 { fmor := FlatteningFunctor_fmor }.
367 Definition ReificationFunctor Γ Δ : Functor (JudgmentsL _ _ (PCF n Γ Δ)) SystemFCa' (mapOptionTree brakifyJudg).
368 refine {| fmor := ReificationFunctor_fmor Γ Δ |}; unfold hom; unfold ob; simpl ; intros.
369 unfold ReificationFunctor_fmor; simpl.
371 unfold ReificationFunctor_fmor; simpl.
373 unfold ReificationFunctor_fmor; simpl.
377 Definition PCF_SMME (n:nat)(Γ:TypeEnv)(Δ:CoercionEnv Γ) : ProgrammingLanguageSMME.
378 refine {| plsmme_pl := PCF n Γ Δ |}.
382 Definition SystemFCa_SMME (n:nat)(Γ:TypeEnv)(Δ:CoercionEnv Γ) : ProgrammingLanguageSMME.
383 refine {| plsmme_pl := SystemFCa n Γ Δ |}.
387 Definition ReificationFunctorMonoidal n : MonoidalFunctor (JudgmentsN n) (JudgmentsN (S n)) (ReificationFunctor n).
392 Definition PCF_SystemFCa_two_level n Γ Δ : TwoLevelLanguage (PCF_SMME n Γ Δ) (SystemFCa_SMME (S n) Γ Δ).
394 (* ... and the retraction exists *)
397 (* Any particular proof in HaskProof is only finitely large, so it uses only finitely many levels of nesting, so
398 * it falls within (SystemFCa n) for some n. This function calculates that "n" and performs the translation *)
400 Definition HaskProof_to_SystemFCa :
401 forall h c (pf:ND Rule h c),
402 { n:nat & h ~~{JudgmentsL (SystemFCa_SMME n)}~~> c }.
404 (* for every n we have a functor from the category of (n+1)-bounded proofs to the category of n-bounded proofs *)
406 End HaskProofFlattener.