X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=src%2FHaskProofFlattener.v;fp=src%2FHaskProofFlattener.v;h=980697dd96ed7cb4dde3725cdb89e6bb7ab84424;hb=e3e2ce9cb83acdd8191049b4e9bd3d4fcf6a4db4;hp=0000000000000000000000000000000000000000;hpb=9adf3f5756893322d0114f89c0908590817eda2b;p=coq-hetmet.git diff --git a/src/HaskProofFlattener.v b/src/HaskProofFlattener.v new file mode 100644 index 0000000..980697d --- /dev/null +++ b/src/HaskProofFlattener.v @@ -0,0 +1,392 @@ +(*********************************************************************************************************************************) +(* HaskProofFlattener: *) +(* *) +(* The Flattening Functor. *) +(* *) +(*********************************************************************************************************************************) + +Generalizable All Variables. +Require Import Preamble. +Require Import General. +Require Import NaturalDeduction. +Require Import Coq.Strings.String. +Require Import Coq.Lists.List. + +Require Import HaskKinds. +Require Import HaskCoreTypes. +Require Import HaskLiteralsAndTyCons. +Require Import HaskStrongTypes. +Require Import HaskProof. +Require Import NaturalDeduction. +Require Import NaturalDeductionCategory. + +Require Import Algebras_ch4. +Require Import Categories_ch1_3. +Require Import Functors_ch1_4. +Require Import Isomorphisms_ch1_5. +Require Import ProductCategories_ch1_6_1. +Require Import OppositeCategories_ch1_6_2. +Require Import Enrichment_ch2_8. +Require Import Subcategories_ch7_1. +Require Import NaturalTransformations_ch7_4. +Require Import NaturalIsomorphisms_ch7_5. +Require Import MonoidalCategories_ch7_8. +Require Import Coherence_ch7_8. + +Require Import HaskStrongTypes. +Require Import HaskStrong. +Require Import HaskProof. +Require Import HaskStrongToProof. +Require Import HaskProofToStrong. +Require Import ProgrammingLanguage. +Require Import HaskProofStratified. + +Open Scope nd_scope. + + +(* + * The flattening transformation. Currently only TWO-level languages are + * supported, and the level-1 sublanguage is rather limited. +* + * This file abuses terminology pretty badly. For purposes of this file, + * "PCF" means "the level-1 sublanguage" and "FC" (aka System FC) means + * the whole language (level-0 language including bracketed level-1 terms) + *) +Section HaskProofFlattener. + + +(* + Definition code2garrow0 {Γ}(ec t1 t2:RawHaskType Γ ★) : RawHaskType Γ ★. + admit. + Defined. + Definition code2garrow Γ (ec t:RawHaskType Γ ★) := + match t with +(* | TApp ★ ★ (TApp _ ★ TArrow tx) t' => code2garrow0 ec tx t'*) + | _ => code2garrow0 ec unitType t + end. + Opaque code2garrow. + Fixpoint typeMap {TV}{κ}(ty:@RawHaskType TV κ) : @RawHaskType TV κ := + match ty as TY in RawHaskType _ K return RawHaskType TV K with + | TCode ec t => code2garrow _ ec t + | TApp _ _ t1 t2 => TApp (typeMap t1) (typeMap t2) + | TAll _ f => TAll _ (fun tv => typeMap (f tv)) + | TCoerc _ t1 t2 t3 => TCoerc (typeMap t1) (typeMap t2) (typeMap t3) + | TVar _ v => TVar v + | TArrow => TArrow + | TCon tc => TCon tc + | TyFunApp tf rhtl => (* FIXME *) TyFunApp tf rhtl + end. +*) + + +(* + Definition code2garrow Γ (ec t:RawHaskType Γ ★) := + match t with +(* | TApp ★ ★ (TApp _ ★ TArrow tx) t' => code2garrow0 ec tx t'*) + | _ => code2garrow0 ec unitType t + end. + Opaque code2garrow. + Fixpoint typeMap {TV}{κ}(ty:@RawHaskType TV κ) : @RawHaskType TV κ := + match ty as TY in RawHaskType _ K return RawHaskType TV K with + | TCode ec t => code2garrow _ ec t + | TApp _ _ t1 t2 => TApp (typeMap t1) (typeMap t2) + | TAll _ f => TAll _ (fun tv => typeMap (f tv)) + | TCoerc _ t1 t2 t3 => TCoerc (typeMap t1) (typeMap t2) (typeMap t3) + | TVar _ v => TVar v + | TArrow => TArrow + | TCon tc => TCon tc + | TyFunApp tf rhtl => (* FIXME *) TyFunApp tf rhtl + end. + + Definition typeMapL {Γ}(lht:LeveledHaskType Γ ★) : LeveledHaskType Γ ★ := + match lht with +(* | t @@ nil => (fun TV ite => typeMap (t TV ite)) @@ lev*) + | t @@ lev => (fun TV ite => typeMap (t TV ite)) @@ lev + end. +*) + + (* gathers a tree of guest-language types into a single host-language types via the tensor *) + Definition tensorizeType {Γ} (lt:Tree ??(HaskType Γ ★)) : HaskType Γ ★. + admit. + Defined. + + Definition mkGA {Γ} : HaskType Γ ★ -> HaskType Γ ★ -> HaskType Γ ★. + admit. + Defined. + + Definition guestJudgmentAsGArrowType {Γ}{Δ}{ec}(lt:PCFJudg Γ Δ ec) : HaskType Γ ★ := + match lt with + pcfjudg x y => + (mkGA (tensorizeType x) (tensorizeType y)) + end. + + Definition obact {Γ}{Δ} ec (X:Tree ??(PCFJudg Γ Δ ec)) : Tree ??(LeveledHaskType Γ ★) := + mapOptionTree guestJudgmentAsGArrowType X @@@ nil. + + Hint Constructors Rule_Flat. + Context {ndr:@ND_Relation _ Rule}. + + (* + * Here it is, what you've all been waiting for! When reading this, + * it might help to have the definition for "Inductive ND" (see + * NaturalDeduction.v) handy as a cross-reference. + *) + Definition FlatteningFunctor_fmor {Γ}{Δ}{ec} + : forall h c, + (h~~{JudgmentsL _ _ (PCF _ Γ Δ ec)}~~>c) -> + ((obact ec h)~~{TypesL _ _ (SystemFCa _ Γ Δ)}~~>(obact ec c)). + + set (@nil (HaskTyVar Γ ★)) as lev. + + unfold hom; unfold ob; unfold ehom; simpl; unfold mon_i; unfold obact; intros. + + induction X; simpl. + + (* the proof from no hypotheses of no conclusions (nd_id0) becomes REmptyGroup *) + apply nd_rule; apply (org_fc _ _ (REmptyGroup _ _ )). auto. + + (* the proof from hypothesis X of conclusion X (nd_id1) becomes RVar *) + apply nd_rule; apply (org_fc _ _ (RVar _ _ _ _)). auto. + + (* the proof from hypothesis X of no conclusions (nd_weak) becomes RWeak;;REmptyGroup *) + eapply nd_comp; + [ idtac + | eapply nd_rule + ; eapply (org_fc _ _ (RArrange _ _ _ _ _ (RWeak _))) + ; auto ]. + eapply nd_rule. + eapply (org_fc _ _ (REmptyGroup _ _)); auto. + + (* the proof from hypothesis X of two identical conclusions X,,X (nd_copy) becomes RVar;;RBindingGroup;;RCont *) + eapply nd_comp; [ idtac | eapply nd_rule; eapply (org_fc _ _ (RArrange _ _ _ _ _ (RCont _))) ]. + eapply nd_comp; [ apply nd_llecnac | idtac ]. + set (nd_seq_reflexive(SequentCalculus:=@pl_sc _ _ _ _ (SystemFCa _ Γ Δ)) + (mapOptionTree guestJudgmentAsGArrowType h @@@ lev)) as q. + eapply nd_comp. + eapply nd_prod. + apply q. + apply q. + apply nd_rule. + eapply (org_fc _ _ (RBindingGroup _ _ _ _ _ _ )). + auto. + auto. + + (* nd_prod becomes nd_llecnac;;nd_prod;;RBindingGroup *) + eapply nd_comp. + apply (nd_llecnac ;; nd_prod IHX1 IHX2). + apply nd_rule. + eapply (org_fc _ _ (RBindingGroup _ _ _ _ _ _ )). + auto. + + (* nd_comp becomes pl_subst (aka nd_cut) *) + eapply nd_comp. + apply (nd_llecnac ;; nd_prod IHX1 IHX2). + clear IHX1 IHX2 X1 X2. + apply (@nd_cut _ _ _ _ _ _ (@pl_subst _ _ _ _ (SystemFCa _ Γ Δ))). + + (* nd_cancell becomes RVar;;RuCanL *) + eapply nd_comp; + [ idtac | eapply nd_rule; apply (org_fc _ _ (RArrange _ _ _ _ _ (RuCanL _))) ]. + apply (nd_seq_reflexive(SequentCalculus:=@pl_sc _ _ _ _ (SystemFCa _ Γ Δ))). + auto. + + (* nd_cancelr becomes RVar;;RuCanR *) + eapply nd_comp; + [ idtac | eapply nd_rule; apply (org_fc _ _ (RArrange _ _ _ _ _ (RuCanR _))) ]. + apply (nd_seq_reflexive(SequentCalculus:=@pl_sc _ _ _ _ (SystemFCa _ Γ Δ))). + auto. + + (* nd_llecnac becomes RVar;;RCanL *) + eapply nd_comp; + [ idtac | eapply nd_rule; apply (org_fc _ _ (RArrange _ _ _ _ _ (RCanL _))) ]. + apply (nd_seq_reflexive(SequentCalculus:=@pl_sc _ _ _ _ (SystemFCa _ Γ Δ))). + auto. + + (* nd_rlecnac becomes RVar;;RCanR *) + eapply nd_comp; + [ idtac | eapply nd_rule; apply (org_fc _ _ (RArrange _ _ _ _ _ (RCanR _))) ]. + apply (nd_seq_reflexive(SequentCalculus:=@pl_sc _ _ _ _ (SystemFCa _ Γ Δ))). + auto. + + (* nd_assoc becomes RVar;;RAssoc *) + eapply nd_comp; + [ idtac | eapply nd_rule; apply (org_fc _ _ (RArrange _ _ _ _ _ (RAssoc _ _ _))) ]. + apply (nd_seq_reflexive(SequentCalculus:=@pl_sc _ _ _ _ (SystemFCa _ Γ Δ))). + auto. + + (* nd_cossa becomes RVar;;RCossa *) + eapply nd_comp; + [ idtac | eapply nd_rule; apply (org_fc _ _ (RArrange _ _ _ _ _ (RCossa _ _ _))) ]. + apply (nd_seq_reflexive(SequentCalculus:=@pl_sc _ _ _ _ (SystemFCa _ Γ Δ))). + auto. + + destruct r as [r rp]. + refine (match rp as R in @Rule_PCF _ _ _ H C _ with + | PCF_RArrange h c r q => let case_RURule := tt in _ + | PCF_RLit lit => let case_RLit := tt in _ + | PCF_RNote Σ τ n => let case_RNote := tt in _ + | PCF_RVar σ => let case_RVar := tt in _ + | PCF_RLam Σ tx te => let case_RLam := tt in _ + | PCF_RApp Σ tx te p => let case_RApp := tt in _ + | PCF_RLet Σ σ₁ σ₂ p => let case_RLet := tt in _ + | PCF_RBindingGroup b c d e => let case_RBindingGroup := tt in _ + | PCF_REmptyGroup => let case_REmptyGroup := tt in _ + (*| PCF_RCase T κlen κ θ l x => let case_RCase := tt in _*) + (*| PCF_RLetRec Σ₁ τ₁ τ₂ lev => let case_RLetRec := tt in _*) + end); simpl in *. + clear rp. + clear r h c. + rename r0 into r; rename h0 into h; rename c0 into c. + + destruct case_RURule. + refine (match q with + | RLeft a b c r => let case_RLeft := tt in _ + | RRight a b c r => let case_RRight := tt in _ + | RCanL b => let case_RCanL := tt in _ + | RCanR b => let case_RCanR := tt in _ + | RuCanL b => let case_RuCanL := tt in _ + | RuCanR b => let case_RuCanR := tt in _ + | RAssoc b c d => let case_RAssoc := tt in _ + | RCossa b c d => let case_RCossa := tt in _ + | RExch b c => let case_RExch := tt in _ + | RWeak b => let case_RWeak := tt in _ + | RCont b => let case_RCont := tt in _ + | RComp a b c f g => let case_RComp := tt in _ + end). + + destruct case_RCanL. + (* ga_cancell *) + admit. + + destruct case_RCanR. + (* ga_cancelr *) + admit. + + destruct case_RuCanL. + (* ga_uncancell *) + admit. + + destruct case_RuCanR. + (* ga_uncancelr *) + admit. + + destruct case_RAssoc. + (* ga_assoc *) + admit. + + destruct case_RCossa. + (* ga_unassoc *) + admit. + + destruct case_RExch. + (* ga_swap *) + admit. + + destruct case_RWeak. + (* ga_drop *) + admit. + + destruct case_RCont. + (* ga_copy *) + admit. + + destruct case_RLeft. + (* ga_second *) + admit. + + destruct case_RRight. + (* ga_first *) + admit. + + destruct case_RComp. + (* ga_comp *) + admit. + + destruct case_RLit. + (* ga_literal *) + admit. + + (* hey cool, I figured out how to pass CoreNote's through... *) + destruct case_RNote. + eapply nd_comp. + eapply nd_rule. + eapply (org_fc _ _ (RVar _ _ _ _)) . auto. + apply nd_rule. + apply (org_fc _ _ (RNote _ _ _ _ _ n)). auto. + + destruct case_RVar. + (* ga_id *) + admit. + + destruct case_RLam. + (* ga_curry, but try to avoid this someday in the future if the argument type isn't a function *) + admit. + + destruct case_RApp. + (* ga_apply *) + admit. + + destruct case_RLet. + (* ga_comp! perhaps this means the ga_curry avoidance can be done by turning lambdas into lets? *) + admit. + + destruct case_REmptyGroup. + (* ga_id u *) + admit. + + destruct case_RBindingGroup. + (* ga_first+ga_second; technically this assumes a specific evaluation order, which is bad *) + admit. + + Defined. + + Instance FlatteningFunctor {Γ}{Δ}{ec} : Functor (JudgmentsL _ _ (PCF _ Γ Δ ec)) (TypesL _ _ (SystemFCa _ Γ Δ)) (obact ec) := + { fmor := FlatteningFunctor_fmor }. + admit. + admit. + admit. + Defined. +(* + Definition ReificationFunctor Γ Δ : Functor (JudgmentsL _ _ (PCF n Γ Δ)) SystemFCa' (mapOptionTree brakifyJudg). + refine {| fmor := ReificationFunctor_fmor Γ Δ |}; unfold hom; unfold ob; simpl ; intros. + unfold ReificationFunctor_fmor; simpl. + admit. + unfold ReificationFunctor_fmor; simpl. + admit. + unfold ReificationFunctor_fmor; simpl. + admit. + Defined. + + + Definition PCF_SMME (n:nat)(Γ:TypeEnv)(Δ:CoercionEnv Γ) : ProgrammingLanguageSMME. + refine {| plsmme_pl := PCF n Γ Δ |}. + admit. + Defined. + + Definition SystemFCa_SMME (n:nat)(Γ:TypeEnv)(Δ:CoercionEnv Γ) : ProgrammingLanguageSMME. + refine {| plsmme_pl := SystemFCa n Γ Δ |}. + admit. + Defined. + + Definition ReificationFunctorMonoidal n : MonoidalFunctor (JudgmentsN n) (JudgmentsN (S n)) (ReificationFunctor n). + admit. + Defined. + + (* 5.1.4 *) + Definition PCF_SystemFCa_two_level n Γ Δ : TwoLevelLanguage (PCF_SMME n Γ Δ) (SystemFCa_SMME (S n) Γ Δ). + admit. + (* ... and the retraction exists *) + Defined. +*) + (* Any particular proof in HaskProof is only finitely large, so it uses only finitely many levels of nesting, so + * it falls within (SystemFCa n) for some n. This function calculates that "n" and performs the translation *) + (* + Definition HaskProof_to_SystemFCa : + forall h c (pf:ND Rule h c), + { n:nat & h ~~{JudgmentsL (SystemFCa_SMME n)}~~> c }. + *) + + (* for every n we have a functor from the category of (n+1)-bounded proofs to the category of n-bounded proofs *) + +End HaskProofFlattener. +