--- /dev/null
+(*********************************************************************************************************************************)
+(* 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.
+
projects / coq-hetmet.git / blobdiff