From 9bbf95bd7f6ad15d4de541e02c0a375bbf687c44 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 17 Oct 2023 19:48:34 -0700 Subject: [PATCH] Add quotation API for context and global_env_ext Useful for externally defining cojoin a la https://docs.google.com/presentation/d/1fUYQ_H0NAaQzCWYidUyWqKUhyHrL_5ofjzi9mzrsEEo/edit?usp=sharing --- quotation/theories/ToPCUIC/All.v | 14 ++++++++++++++ quotation/theories/ToPCUIC/Common/Environment.v | 7 +++++-- quotation/theories/ToPCUIC/Init.v | 1 + .../ToPCUIC/QuotationOf/Common/Environment/Sig.v | 4 ++++ quotation/theories/ToTemplate/All.v | 14 ++++++++++++++ quotation/theories/ToTemplate/Common/Environment.v | 7 +++++-- quotation/theories/ToTemplate/Init.v | 1 + .../QuotationOf/Common/Environment/Sig.v | 4 ++++ 8 files changed, 48 insertions(+), 4 deletions(-) diff --git a/quotation/theories/ToPCUIC/All.v b/quotation/theories/ToPCUIC/All.v index bd46876a3..00a8a5e06 100644 --- a/quotation/theories/ToPCUIC/All.v +++ b/quotation/theories/ToPCUIC/All.v @@ -5,12 +5,26 @@ From MetaCoq.Quotation.ToPCUIC.PCUIC Require PCUICAst PCUICTyping PCUICCumulativ (* without typing derivations *) Module Raw. (* These are probably the only quotation functions that users of this development will want to use; other files should be considered internal to the development of quotation *) + Definition quote_checker_flags : checker_flags -> PCUICAst.term := config.quote_checker_flags. + Definition quote_global_env_ext : global_env_ext -> PCUICAst.term := PCUICAst.QuotePCUICEnvironment.quote_global_env_ext. + Definition quote_context : context -> PCUICAst.term := PCUICAst.QuotePCUICEnvironment.quote_context. Definition quote_term : PCUICAst.term -> PCUICAst.term := PCUICAst.quote_term. Definition quote_typing {cf : checker_flags} {Σ Γ t T} : (Σ ;;; Γ |- t : T) -> PCUICAst.term := PCUICTyping.quote_typing. Definition quote_red {Σ Γ x y} : @red Σ Γ x y -> PCUICAst.term := PCUICReduction.quote_red. Definition quote_wf_local {cf : checker_flags} {Σ Γ} : wf_local Σ Γ -> PCUICAst.term := PCUICTyping.quote_wf_local. Definition quote_wf {cf Σ} : @wf cf Σ -> PCUICAst.term := PCUICTyping.quote_wf. Definition quote_wf_ext {cf Σ} : @wf_ext cf Σ -> PCUICAst.term := PCUICTyping.quote_wf_ext. + + (** N.B. Only works if you [Import Raw.QuoteNotationHints] *) + Notation quote := Init.quoted_term_of (only parsing). + Module QuoteNotationHints. + Export (hints) Quotation.ToPCUIC.Init + Quotation.ToPCUIC.PCUIC.PCUICAst + Quotation.ToPCUIC.PCUIC.PCUICTyping + Quotation.ToPCUIC.PCUIC.PCUICCumulativitySpec + Quotation.ToPCUIC.PCUIC.PCUICReduction + . + End QuoteNotationHints. End Raw. (* eventually we'll have proofs that the above definitions are well-typed *) diff --git a/quotation/theories/ToPCUIC/Common/Environment.v b/quotation/theories/ToPCUIC/Common/Environment.v index 7375dc51b..1fda16d64 100644 --- a/quotation/theories/ToPCUIC/Common/Environment.v +++ b/quotation/theories/ToPCUIC/Common/Environment.v @@ -106,8 +106,8 @@ Module QuoteEnvironment (T : Term) (Import E : EnvironmentSig T) (Import QEH : Q #[export] Instance qextends_alt : quotation_of extends_alt := ltac:(cbv [extends_alt]; exact _). #[export] Instance qextends_decls_alt : quotation_of extends_decls_alt := ltac:(cbv [extends_decls_alt]; exact _). - #[export] Instance quote_extends {Σ Σ'} : ground_quotable (@extends Σ Σ') := ground_quotable_of_iffT extends_alt_iff. - #[export] Instance quote_extends_decls {Σ Σ'} : ground_quotable (@extends_decls Σ Σ') := ground_quotable_of_iffT (@extends_decls_alt_iff Σ Σ'). + #[export] Instance quote_extends {Σ Σ'} : ground_quotable (@extends Σ Σ') := ground_quotable_of_iffT extends_alt_iff. + #[export] Instance quote_extends_decls {Σ Σ'} : ground_quotable (@extends_decls Σ Σ') := ground_quotable_of_iffT (@extends_decls_alt_iff Σ Σ'). #[export] Instance quote_extends_strictly_on_decls {Σ Σ'} : ground_quotable (@extends_strictly_on_decls Σ Σ') := ltac:(cbv [extends_strictly_on_decls]; exact _). #[export] Instance quote_strictly_extends_decls {Σ Σ'} : ground_quotable (@strictly_extends_decls Σ Σ') := ltac:(cbv [strictly_extends_decls]; exact _). @@ -115,4 +115,7 @@ Module QuoteEnvironment (T : Term) (Import E : EnvironmentSig T) (Import QEH : Q #[export] Instance quote_All_decls {P t t'} {qP : quotation_of P} {quoteP : forall t t', ground_quotable (P t t')} : ground_quotable (All_decls P t t') := ltac:(induction 1; exact _). #[export] Instance quote_All_decls_alpha {P t t'} {qP : quotation_of P} {quoteP : forall t t', ground_quotable (P t t')} : ground_quotable (All_decls_alpha P t t') := ltac:(induction 1; exact _). + + Definition quote_context : ground_quotable context := ltac:(cbv [context]; exact _). + Definition quote_global_env_ext : ground_quotable global_env_ext := ltac:(cbv [global_env_ext]; exact _). End QuoteEnvironment. diff --git a/quotation/theories/ToPCUIC/Init.v b/quotation/theories/ToPCUIC/Init.v index bd3aebcee..926fbc2b0 100644 --- a/quotation/theories/ToPCUIC/Init.v +++ b/quotation/theories/ToPCUIC/Init.v @@ -15,6 +15,7 @@ Local Open Scope bs. Import MCMonadNotation. Class quotation_of {T} (t : T) := quoted_term_of : PCUICAst.term. +#[global] Arguments quoted_term_of {T} t {_}. Class ground_quotable T := quote_ground : forall t : T, quotation_of t. Class inductive_quotation_of {T} (t : T) := { qinductive : inductive diff --git a/quotation/theories/ToPCUIC/QuotationOf/Common/Environment/Sig.v b/quotation/theories/ToPCUIC/QuotationOf/Common/Environment/Sig.v index 31de3ebc0..cd220308a 100644 --- a/quotation/theories/ToPCUIC/QuotationOf/Common/Environment/Sig.v +++ b/quotation/theories/ToPCUIC/QuotationOf/Common/Environment/Sig.v @@ -47,6 +47,10 @@ Module Type QuoteEnvironmentSig (T : Term) (Import E : EnvironmentSig T). #[export] Declare Instance quote_All_decls {P t t'} {qP : quotation_of P} {quoteP : forall t t', ground_quotable (P t t')} : ground_quotable (All_decls P t t'). #[export] Declare Instance quote_All_decls_alpha {P t t'} {qP : quotation_of P} {quoteP : forall t t', ground_quotable (P t t')} : ground_quotable (All_decls_alpha P t t'). + + (** We need to declare these unfoldable for conversion anyway, so we don't register these instances, but we want them for the external interface *) + Axiom quote_global_env_ext : ground_quotable global_env_ext. + Axiom quote_context : ground_quotable context. End QuoteEnvironmentSig. Module Type QuotationOfEnvironmentDecide (T : Term) (E : EnvironmentSig T) (ED : EnvironmentDecide T E). diff --git a/quotation/theories/ToTemplate/All.v b/quotation/theories/ToTemplate/All.v index cfe1a9713..89d87a394 100644 --- a/quotation/theories/ToTemplate/All.v +++ b/quotation/theories/ToTemplate/All.v @@ -6,6 +6,9 @@ From MetaCoq.Quotation.ToTemplate.Template Require Ast Typing WfAst TypingWf. (* without typing derivations *) Module Raw. (* These are probably the only quotation functions that users of this development will want to use; other files should be considered internal to the development of quotation *) + Definition quote_checker_flags : checker_flags -> Ast.term := config.quote_checker_flags. + Definition quote_global_env_ext : global_env_ext -> Ast.term := Ast.QuoteEnv.quote_global_env_ext. + Definition quote_context : context -> Ast.term := Ast.QuoteEnv.quote_context. Definition quote_term : Ast.term -> Ast.term := Ast.quote_term. Definition quote_typing {cf : checker_flags} {Σ Γ t T} : (Σ ;;; Γ |- t : T) -> Ast.term := Typing.quote_typing. Definition quote_red {Σ Γ x y} : @red Σ Γ x y -> Ast.term := Typing.quote_red. @@ -16,6 +19,17 @@ Module Raw. Definition quote_wf {Σ t} : @WfAst.wf Σ t -> Ast.term := WfAst.quote_wf. End WfAst. (* TODO: do we want anything from TypingWf? Is there anything else missing here? *) + + (** N.B. Only works if you [Import Raw.QuoteNotationHints] *) + Notation quote := Init.quoted_term_of (only parsing). + Module QuoteNotationHints. + Export (hints) Quotation.ToTemplate.Init + Quotation.ToTemplate.Template.Ast + Quotation.ToTemplate.Template.Typing + Quotation.ToTemplate.Template.WfAst + Quotation.ToTemplate.Template.TypingWf + . + End QuoteNotationHints. End Raw. (* eventually we'll have proofs that the above definitions are well-typed *) diff --git a/quotation/theories/ToTemplate/Common/Environment.v b/quotation/theories/ToTemplate/Common/Environment.v index a2a3abdce..8297330e3 100644 --- a/quotation/theories/ToTemplate/Common/Environment.v +++ b/quotation/theories/ToTemplate/Common/Environment.v @@ -106,8 +106,8 @@ Module QuoteEnvironment (T : Term) (Import E : EnvironmentSig T) (Import QEH : Q #[export] Instance qextends_alt : quotation_of extends_alt := ltac:(cbv [extends_alt]; exact _). #[export] Instance qextends_decls_alt : quotation_of extends_decls_alt := ltac:(cbv [extends_decls_alt]; exact _). - #[export] Instance quote_extends {Σ Σ'} : ground_quotable (@extends Σ Σ') := ground_quotable_of_iffT extends_alt_iff. - #[export] Instance quote_extends_decls {Σ Σ'} : ground_quotable (@extends_decls Σ Σ') := ground_quotable_of_iffT (@extends_decls_alt_iff Σ Σ'). + #[export] Instance quote_extends {Σ Σ'} : ground_quotable (@extends Σ Σ') := ground_quotable_of_iffT extends_alt_iff. + #[export] Instance quote_extends_decls {Σ Σ'} : ground_quotable (@extends_decls Σ Σ') := ground_quotable_of_iffT (@extends_decls_alt_iff Σ Σ'). #[export] Instance quote_extends_strictly_on_decls {Σ Σ'} : ground_quotable (@extends_strictly_on_decls Σ Σ') := ltac:(cbv [extends_strictly_on_decls]; exact _). #[export] Instance quote_strictly_extends_decls {Σ Σ'} : ground_quotable (@strictly_extends_decls Σ Σ') := ltac:(cbv [strictly_extends_decls]; exact _). @@ -115,4 +115,7 @@ Module QuoteEnvironment (T : Term) (Import E : EnvironmentSig T) (Import QEH : Q #[export] Instance quote_All_decls {P t t'} {qP : quotation_of P} {quoteP : forall t t', ground_quotable (P t t')} : ground_quotable (All_decls P t t') := ltac:(induction 1; exact _). #[export] Instance quote_All_decls_alpha {P t t'} {qP : quotation_of P} {quoteP : forall t t', ground_quotable (P t t')} : ground_quotable (All_decls_alpha P t t') := ltac:(induction 1; exact _). + + Definition quote_context : ground_quotable context := ltac:(cbv [context]; exact _). + Definition quote_global_env_ext : ground_quotable global_env_ext := ltac:(cbv [global_env_ext]; exact _). End QuoteEnvironment. diff --git a/quotation/theories/ToTemplate/Init.v b/quotation/theories/ToTemplate/Init.v index 4bf46f2f7..caa06369e 100644 --- a/quotation/theories/ToTemplate/Init.v +++ b/quotation/theories/ToTemplate/Init.v @@ -14,6 +14,7 @@ Local Open Scope bs. Import MCMonadNotation. Class quotation_of {T} (t : T) := quoted_term_of : Ast.term. +#[global] Arguments quoted_term_of {T} t {_}. Class ground_quotable T := quote_ground : forall t : T, quotation_of t. Class inductive_quotation_of {T} (t : T) := { qinductive : inductive diff --git a/quotation/theories/ToTemplate/QuotationOf/Common/Environment/Sig.v b/quotation/theories/ToTemplate/QuotationOf/Common/Environment/Sig.v index 7bfba4ce3..c89745924 100644 --- a/quotation/theories/ToTemplate/QuotationOf/Common/Environment/Sig.v +++ b/quotation/theories/ToTemplate/QuotationOf/Common/Environment/Sig.v @@ -47,6 +47,10 @@ Module Type QuoteEnvironmentSig (T : Term) (Import E : EnvironmentSig T). #[export] Declare Instance quote_All_decls {P t t'} {qP : quotation_of P} {quoteP : forall t t', ground_quotable (P t t')} : ground_quotable (All_decls P t t'). #[export] Declare Instance quote_All_decls_alpha {P t t'} {qP : quotation_of P} {quoteP : forall t t', ground_quotable (P t t')} : ground_quotable (All_decls_alpha P t t'). + + (** We need to declare these unfoldable for conversion anyway, so we don't register these instances, but we want them for the external interface *) + Axiom quote_global_env_ext : ground_quotable global_env_ext. + Axiom quote_context : ground_quotable context. End QuoteEnvironmentSig. Module Type QuotationOfEnvironmentDecide (T : Term) (E : EnvironmentSig T) (ED : EnvironmentDecide T E).