diff --git a/quotation/theories/ToPCUIC/Common/BasicAst.v b/quotation/theories/ToPCUIC/Common/BasicAst.v index 490570209..37516b436 100644 --- a/quotation/theories/ToPCUIC/Common/BasicAst.v +++ b/quotation/theories/ToPCUIC/Common/BasicAst.v @@ -1,6 +1,6 @@ From MetaRocq.Quotation.ToPCUIC Require Import Init. From MetaRocq.Quotation.ToPCUIC Require Import (hints) Stdlib.Init Stdlib.Floats Stdlib.Numbers. -From MetaRocq.Quotation.ToPCUIC.Utils Require Import (hints) utils. +From MetaRocq.Quotation.ToPCUIC.Utils Require Import (hints) utils MROption. From MetaRocq.Quotation.ToPCUIC.Common Require Import (hints) Kernames. From MetaRocq.Common Require Import BasicAst. From MetaRocq.Utils Require Import MRUtils. @@ -18,9 +18,14 @@ From MetaRocq.Template Require Import AstUtils (* for tFixType *). #[export] Instance quote_def {term} {qterm : quotation_of term} {quote_term : ground_quotable term} : ground_quotable (def term) := ltac:(destruct 1; exact _). #[export] Instance quote_judgment_ {term univ} {qterm : quotation_of term} {uterm : quotation_of univ} {quote_term : ground_quotable term} {quote_univ : ground_quotable univ} : ground_quotable (judgment_ term univ) := ltac:(destruct 1; exact _). #[export] Instance quote_context_decl {term} {qterm : quotation_of term} {quote_term : ground_quotable term} : ground_quotable (context_decl term) := ltac:(destruct 1; exact _). +#[export] Instance quotation_of_context_decl {term} {qterm : quotation_of term} {d : context_decl term} {qd : ondecl quotation_of d} : quotation_of d := ltac:(destruct d; cbv [ondecl BasicAst.decl_body BasicAst.decl_type] in qd; destruct_head'_prod; exact _). +#[export] Hint Extern 0 (ondecl quotation_of _) => assumption : typeclass_instances. +#[export] Instance quotation_of_context {term} {qterm : quotation_of term} {ctx : list (context_decl term)} {qctx : onctx quotation_of ctx} : quotation_of ctx := ltac:(induction qctx; exact _). +#[export] Hint Extern 0 (onctx quotation_of _) => assumption : typeclass_instances. #[export] Hint Unfold mfixpoint : quotation. #[export] Typeclasses Transparent mfixpoint. #[local] Hint Unfold dtype dbody : quotation. #[export] Instance quotation_of_mfixpoint {term} {m : mfixpoint term} {qterm : quotation_of term} {qm : tFixType quotation_of quotation_of m} : quotation_of m := ltac:(induction qm; destruct_head'_prod; destruct_head' def; exact _). +#[export] Hint Extern 0 (tFixType quotation_of quotation_of ?m) => assumption : typeclass_instances. #[export] Hint Unfold eq_binder_annot : quotation. #[export] Typeclasses Transparent eq_binder_annot. diff --git a/quotation/theories/ToPCUIC/PCUIC/PCUICAst.v b/quotation/theories/ToPCUIC/PCUIC/PCUICAst.v index bad376ab7..2f6c2a631 100644 --- a/quotation/theories/ToPCUIC/PCUIC/PCUICAst.v +++ b/quotation/theories/ToPCUIC/PCUIC/PCUICAst.v @@ -6,10 +6,16 @@ From MetaRocq.Quotation.ToPCUIC.Common Require Import Environment EnvironmentTyp From MetaRocq.Quotation.ToPCUIC.PCUIC Require Import (hints) utils.PCUICPrimitive. From MetaRocq.Quotation.ToPCUIC.QuotationOf.Common Require Import Environment.Sig EnvironmentTyping.Sig. From MetaRocq.Quotation.ToPCUIC.QuotationOf.PCUIC Require Import PCUICAst.Instances Syntax.PCUICReflect.Instances. +From MetaRocq.Utils Require Import MRUtils. #[export] Instance quote_predicate {term} {qterm : quotation_of term} {quote_term : ground_quotable term} : ground_quotable (predicate term) := ltac:(destruct 1; exact _). #[export] Instance quote_branch {term} {qterm : quotation_of term} {quote_term : ground_quotable term} : ground_quotable (branch term) := ltac:(destruct 1; exact _). -#[local] Hint Extern 1 => assumption : typeclass_instances. + +#[local] Instance quotation_of_predicate {term} {p : predicate term} {qterm : quotation_of term} {qp : tCasePredProp quotation_of quotation_of p} : quotation_of p := ltac:(induction p; cbv [tCasePredProp PCUICAst.pparams PCUICAst.pcontext PCUICAst.preturn] in *; destruct_head'_prod; exact _). +#[export] Hint Extern 0 (@tCasePredProp ?term quotation_of quotation_of ?p) => assumption : typeclass_instances. +#[local] Instance quotation_of_branch {term} {qterm : quotation_of term} {b : branch term} {qctx : onctx quotation_of b.(bcontext)} {qbody : quotation_of b.(bbody)} : quotation_of b := ltac:(destruct b; cbv [PCUICAst.bcontext PCUICAst.bbody] in *; exact _). +#[local] Instance quotation_of_branches {term} {qterm : quotation_of term} {l : list (branch term)} {ql : tCaseBrsProp quotation_of l} : quotation_of l := ltac:(cbv [tCaseBrsProp] in ql; induction ql; destruct_head'_prod; exact _). +#[export] Hint Extern 0 (@tCaseBrsProp _ quotation_of _) => assumption : typeclass_instances. #[export] Instance quote_term : ground_quotable term := ltac:(induction 1 using term_forall_list_ind; exact _). diff --git a/quotation/theories/ToPCUIC/PCUIC/utils/PCUICPrimitive.v b/quotation/theories/ToPCUIC/PCUIC/utils/PCUICPrimitive.v index 4cf70f5e5..ce4c5f0f1 100644 --- a/quotation/theories/ToPCUIC/PCUIC/utils/PCUICPrimitive.v +++ b/quotation/theories/ToPCUIC/PCUIC/utils/PCUICPrimitive.v @@ -13,6 +13,7 @@ From MetaRocq.Quotation.ToPCUIC.Utils Require Import (hints) All_Forall. #[export] Hint Extern 0 (@tPrimProp ?term quotation_of ?a) => lazymatch goal with | [ H : @tPrimProp _ quotation_of _ |- _ ] => assumption + | [ H : @tPrimProp _ (fun x => quotation_of x) _ |- _ ] => assumption end : typeclass_instances. #[export] Instance quote_prim_model {term tag} {qterm : quotation_of term} {quote_term : ground_quotable term} : ground_quotable (prim_model term tag) := ltac:(destruct 1; eauto). diff --git a/quotation/theories/ToPCUIC/Stdlib/Init.v b/quotation/theories/ToPCUIC/Stdlib/Init.v index 1f37cd309..64d5fef67 100644 --- a/quotation/theories/ToPCUIC/Stdlib/Init.v +++ b/quotation/theories/ToPCUIC/Stdlib/Init.v @@ -36,10 +36,7 @@ Defined. #[export] Polymorphic Instance quote_prod {A B} {qA : quotation_of A} {qB : quotation_of B} {quoteA : ground_quotable A} {quoteB : ground_quotable B} : ground_quotable (prod A B) := (ltac:(induction 1; exact _)). #[export] Polymorphic Instance quote_list {A} {qA : quotation_of A} {quoteA : ground_quotable A} : ground_quotable (list A) := (ltac:(induction 1; exact _)). #[export] Polymorphic Instance quotation_of_list {A ls} {qA : quotation_of A} {qls : @All A quotation_of ls} : quotation_of ls := ltac:(induction qls; exact _). -#[export] Hint Extern 0 (@All ?A quotation_of ?ls) -=> lazymatch goal with - | [ H : @All _ quotation_of _ |- _ ] => assumption - end : typeclass_instances. +#[export] Hint Extern 0 (@All ?A quotation_of ?ls) => assumption : typeclass_instances. #[export] Instance quote_comparison : ground_quotable comparison := ltac:(destruct 1; exact _). #[export] Instance quote_CompareSpec {Peq Plt Pgt : Prop} {qPeq : quotation_of Peq} {qPlt : quotation_of Plt} {qPgt : quotation_of Pgt} {quote_Peq : ground_quotable Peq} {quote_Plt : ground_quotable Plt} {quote_Pgt : ground_quotable Pgt} {c} : ground_quotable (CompareSpec Peq Plt Pgt c). Proof. diff --git a/quotation/theories/ToPCUIC/Utils/MROption.v b/quotation/theories/ToPCUIC/Utils/MROption.v index 67ed534aa..3bbd18317 100644 --- a/quotation/theories/ToPCUIC/Utils/MROption.v +++ b/quotation/theories/ToPCUIC/Utils/MROption.v @@ -22,6 +22,9 @@ Defined. #[export] Polymorphic Instance quote_option_default {A P o b} {quoteP : forall x, o = Some x -> ground_quotable (P x)} {quoteP' : o = None -> ground_quotable b} : ground_quotable (@option_default A Type P o b) := ltac:(destruct o; cbv [option_default]; exact _). #[export] Polymorphic Instance quote_option_defaultP {A o} {P : A -> Prop} {b : Prop} {quoteP : forall x, o = Some x -> ground_quotable (P x)} {quoteP' : o = None -> ground_quotable b} : ground_quotable (@option_default A Prop P o b) := ltac:(destruct o; cbv [option_default]; exact _). +#[export] Polymorphic Instance quotation_of_option_default {A} {qA : quotation_of A} {o : option A} {b} {qb : ground_quotable b} {qo : option_default quotation_of o b} : quotation_of o := ltac:(destruct o; cbv [option_default] in qo; exact _). +#[export] Hint Extern 0 (option_default quotation_of _ _) => assumption : typeclass_instances. + #[export] Instance quote_on_Some {A P o} {quoteP : forall x, o = Some x -> ground_quotable (P x:Prop)} : ground_quotable (@on_Some A P o) := ltac:(destruct o; cbv [on_Some]; exact _). #[export] Typeclasses Opaque on_Some. #[export] Instance quote_on_Some_or_None {A P o} {quoteP : forall x, o = Some x -> ground_quotable (P x:Prop)} : ground_quotable (@on_Some_or_None A P o) := ltac:(destruct o; cbv [on_Some_or_None]; exact _). diff --git a/quotation/theories/ToTemplate/Common/BasicAst.v b/quotation/theories/ToTemplate/Common/BasicAst.v index ff37aeda9..06c46ac7c 100644 --- a/quotation/theories/ToTemplate/Common/BasicAst.v +++ b/quotation/theories/ToTemplate/Common/BasicAst.v @@ -22,5 +22,6 @@ From MetaRocq.Template Require Import AstUtils (* for tFixType *). #[export] Typeclasses Transparent mfixpoint. #[local] Hint Unfold dtype dbody : quotation. #[export] Instance quotation_of_mfixpoint {term} {m : mfixpoint term} {qterm : quotation_of term} {qm : tFixType quotation_of quotation_of m} : quotation_of m := ltac:(induction qm; destruct_head'_prod; destruct_head' def; exact _). +#[export] Hint Extern 0 (tFixType quotation_of quotation_of ?m) => assumption : typeclass_instances. #[export] Hint Unfold eq_binder_annot : quotation. #[export] Typeclasses Transparent eq_binder_annot. diff --git a/quotation/theories/ToTemplate/Stdlib/Init.v b/quotation/theories/ToTemplate/Stdlib/Init.v index 8b3fd7166..d5c7164c3 100644 --- a/quotation/theories/ToTemplate/Stdlib/Init.v +++ b/quotation/theories/ToTemplate/Stdlib/Init.v @@ -36,10 +36,7 @@ Defined. #[export] Polymorphic Instance quote_prod {A B} {qA : quotation_of A} {qB : quotation_of B} {quoteA : ground_quotable A} {quoteB : ground_quotable B} : ground_quotable (prod A B) := (ltac:(induction 1; exact _)). #[export] Polymorphic Instance quote_list {A} {qA : quotation_of A} {quoteA : ground_quotable A} : ground_quotable (list A) := (ltac:(induction 1; exact _)). #[export] Polymorphic Instance quotation_of_list {A ls} {qA : quotation_of A} {qls : @All A quotation_of ls} : quotation_of ls := ltac:(induction qls; exact _). -#[export] Hint Extern 0 (@All ?A quotation_of ?ls) -=> lazymatch goal with - | [ H : @All _ quotation_of _ |- _ ] => assumption - end : typeclass_instances. +#[export] Hint Extern 0 (@All ?A quotation_of ?ls) => assumption : typeclass_instances. #[export] Instance quote_comparison : ground_quotable comparison := ltac:(destruct 1; exact _). #[export] Instance quote_CompareSpec {Peq Plt Pgt : Prop} {qPeq : quotation_of Peq} {qPlt : quotation_of Plt} {qPgt : quotation_of Pgt} {quote_Peq : ground_quotable Peq} {quote_Plt : ground_quotable Plt} {quote_Pgt : ground_quotable Pgt} {c} : ground_quotable (CompareSpec Peq Plt Pgt c). Proof. diff --git a/quotation/theories/ToTemplate/Template/Ast.v b/quotation/theories/ToTemplate/Template/Ast.v index a349dbd74..3d8b7d772 100644 --- a/quotation/theories/ToTemplate/Template/Ast.v +++ b/quotation/theories/ToTemplate/Template/Ast.v @@ -5,12 +5,16 @@ From MetaRocq.Quotation.ToTemplate.Common Require Import (hints) Universes Basic From MetaRocq.Quotation.ToTemplate.Common Require Import Environment EnvironmentTyping. From MetaRocq.Quotation.ToTemplate.QuotationOf.Common Require Import Environment.Sig EnvironmentTyping.Sig. From MetaRocq.Quotation.ToTemplate.QuotationOf.Template Require Import Ast.Instances ReflectAst.Instances. +From MetaRocq.Utils Require Import MRUtils. #[export] Instance quote_pstring : ground_quotable PrimString.string := fun s => Ast.tString s. #[export] Instance quote_predicate {term} {qterm : quotation_of term} {quote_term : ground_quotable term} : ground_quotable (predicate term) := ltac:(destruct 1; exact _). #[export] Instance quote_branch {term} {qterm : quotation_of term} {quote_term : ground_quotable term} : ground_quotable (branch term) := ltac:(destruct 1; exact _). -#[local] Hint Extern 1 => assumption : typeclass_instances. + +#[local] Instance quotation_of_predicate {term} {p : predicate term} {qterm : quotation_of term} {qp : tCasePredProp quotation_of quotation_of p} : quotation_of p := ltac:(induction p; cbv [tCasePredProp Ast.pparams Ast.preturn] in *; destruct_head'_prod; exact _). +#[export] Hint Extern 0 (@tCasePredProp ?term quotation_of quotation_of ?p) => assumption : typeclass_instances. + #[export] Instance quote_term : ground_quotable term := ltac:(induction 1 using term_forall_list_rect; exact _). Module QuoteTemplateTerm <: QuoteTerm TemplateTerm.