From 3198ad2979e549627942e946cbb93edd554c775b Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Sat, 11 Feb 2023 15:00:42 -0800 Subject: [PATCH 1/3] Add support for quoting constants in TypingWf --- quotation/_CoqProject.in | 1 + quotation/theories/CommonUtils.v | 1 + quotation/theories/ToTemplate/Template/TypingWf.v | 8 ++++++++ 3 files changed, 10 insertions(+) create mode 100644 quotation/theories/ToTemplate/Template/TypingWf.v diff --git a/quotation/_CoqProject.in b/quotation/_CoqProject.in index deabd85f1..831c4d369 100644 --- a/quotation/_CoqProject.in +++ b/quotation/_CoqProject.in @@ -88,6 +88,7 @@ theories/ToTemplate/Template/LiftSubst.v theories/ToTemplate/Template/ReflectAst.v theories/ToTemplate/Template/TermEquality.v theories/ToTemplate/Template/Typing.v +theories/ToTemplate/Template/TypingWf.v theories/ToTemplate/Template/UnivSubst.v theories/ToTemplate/Template/WfAst.v theories/ToTemplate/Utils/All_Forall.v diff --git a/quotation/theories/CommonUtils.v b/quotation/theories/CommonUtils.v index e9e73a70b..a68c79e9d 100644 --- a/quotation/theories/CommonUtils.v +++ b/quotation/theories/CommonUtils.v @@ -1,3 +1,4 @@ +From MetaCoq.Template Require TypingWf. (* Kludge to avoid universe inconsistencies that arise when this file is required later, things like Error: Universe inconsistency. Cannot enforce Coq.Init.Datatypes.26 < replace_quotation_of.u0 because replace_quotation_of.u0 <= MetaCoq.Template.MonadAst.6 <= prod.u0 = Coq.Init.Datatypes.26. *) From MetaCoq.Utils Require Import utils monad_utils MCList. From MetaCoq.Common Require Import Kernames MonadBasicAst. From MetaCoq.Template Require MonadAst TemplateMonad Ast Loader. diff --git a/quotation/theories/ToTemplate/Template/TypingWf.v b/quotation/theories/ToTemplate/Template/TypingWf.v new file mode 100644 index 000000000..0ca45b7c4 --- /dev/null +++ b/quotation/theories/ToTemplate/Template/TypingWf.v @@ -0,0 +1,8 @@ +From MetaCoq.Template Require Import TypingWf. +From MetaCoq.Quotation.ToTemplate Require Import Init. +From MetaCoq.Quotation.ToTemplate Require Import (hints) Coq.Init. +From MetaCoq.Quotation.ToTemplate.Utils Require Import (hints) All_Forall. +From MetaCoq.Quotation.ToTemplate.Common Require Import (hints) BasicAst. +From MetaCoq.Quotation.ToTemplate.Template Require Import (hints) Ast WfAst. + +#[export] Instance quote_wf_inductive_body {Σ idecl} : ground_quotable (@wf_inductive_body Σ idecl) := ltac:(destruct 1; exact _). From 554525b2cd2f309f8a3c178740fd1e9ad5678cb5 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 4 Apr 2023 23:02:55 -0700 Subject: [PATCH 2/3] Remove kludge --- quotation/theories/CommonUtils.v | 1 - 1 file changed, 1 deletion(-) diff --git a/quotation/theories/CommonUtils.v b/quotation/theories/CommonUtils.v index a68c79e9d..e9e73a70b 100644 --- a/quotation/theories/CommonUtils.v +++ b/quotation/theories/CommonUtils.v @@ -1,4 +1,3 @@ -From MetaCoq.Template Require TypingWf. (* Kludge to avoid universe inconsistencies that arise when this file is required later, things like Error: Universe inconsistency. Cannot enforce Coq.Init.Datatypes.26 < replace_quotation_of.u0 because replace_quotation_of.u0 <= MetaCoq.Template.MonadAst.6 <= prod.u0 = Coq.Init.Datatypes.26. *) From MetaCoq.Utils Require Import utils monad_utils MCList. From MetaCoq.Common Require Import Kernames MonadBasicAst. From MetaCoq.Template Require MonadAst TemplateMonad Ast Loader. From d2098c0ec77bbdde374a1fc04c23262ee68d996e Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Sat, 8 Apr 2023 12:35:25 -0700 Subject: [PATCH 3/3] Require TypingWf in Quotation.ToTemplate.All --- quotation/theories/ToTemplate/All.v | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/quotation/theories/ToTemplate/All.v b/quotation/theories/ToTemplate/All.v index 030b0bb17..9c19423c8 100644 --- a/quotation/theories/ToTemplate/All.v +++ b/quotation/theories/ToTemplate/All.v @@ -1,7 +1,7 @@ From MetaCoq.Common Require Import config. From MetaCoq.Template Require Import Ast Typing. -From MetaCoq.Template Require WfAst (*WfTyping*). -From MetaCoq.Quotation.ToTemplate.Template Require Ast Typing WfAst (*WfTyping*). +From MetaCoq.Template Require WfAst TypingWf. +From MetaCoq.Quotation.ToTemplate.Template Require Ast Typing WfAst TypingWf. (* without typing derivations *) Module Raw. @@ -14,7 +14,7 @@ Module Raw. Module WfAst. Definition quote_wf {Σ t} : @WfAst.wf Σ t -> Ast.term := WfAst.quote_wf. End WfAst. - (* TODO: do we want anything from WfTyping? Is there anything else missing here? *) + (* TODO: do we want anything from TypingWf? Is there anything else missing here? *) End Raw. (* eventually we'll have proofs that the above definitions are well-typed *)