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

@@ -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 *)

quotation/theories/ToPCUIC/Common/Environment.v

@@ -106,13 +106,16 @@ 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 _).
 
   #[export] Instance quote_primitive_invariants {cdecl} : ground_quotable (primitive_invariants cdecl) := ltac:(cbv [primitive_invariants]; exact _).
 
   #[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.

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

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).

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 *)

quotation/theories/ToTemplate/Common/Environment.v

@@ -106,13 +106,16 @@ 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 _).
 
   #[export] Instance quote_primitive_invariants {cdecl} : ground_quotable (primitive_invariants cdecl) := ltac:(cbv [primitive_invariants]; exact _).
 
   #[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.

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

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).