From 37232027d12240d5225c1d6286cd3528b3350f02 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Fri, 21 Oct 2022 21:16:43 +0530 Subject: [PATCH] Add PCUIC versions of the template monad This will allow easier creation of developments that reason about doubly-quoted terms and judgments. --- pcuic/_CoqProject.in | 8 + pcuic/theories/Loader.v | 7 + pcuic/theories/PCUICTemplateMonad.v | 3 + pcuic/theories/PCUICTemplateMonad/Common.v | 21 +++ pcuic/theories/PCUICTemplateMonad/Core.v | 27 ++++ pcuic/theories/PCUICToTemplate.v | 28 ++++ pcuic/theories/TemplateMonadToPCUIC.v | 153 ++++++++++++++++++ template-coq/_CoqProject | 4 + .../gen-src/cRelationClasses.mli.orig | 22 +-- template-coq/theories/MonadAst.v | 58 +++++++ template-coq/theories/MonadBasicAst.v | 78 +++++++++ template-coq/theories/TemplateMonad/Common.v | 9 +- template-coq/theories/TemplateMonad/Core.v | 19 +++ .../theories/TemplateMonad/Extractable.v | 3 + 14 files changed, 430 insertions(+), 10 deletions(-) create mode 100644 pcuic/theories/Loader.v create mode 100644 pcuic/theories/PCUICTemplateMonad.v create mode 100644 pcuic/theories/PCUICTemplateMonad/Common.v create mode 100644 pcuic/theories/PCUICTemplateMonad/Core.v create mode 100644 pcuic/theories/TemplateMonadToPCUIC.v create mode 100644 template-coq/theories/MonadAst.v create mode 100644 template-coq/theories/MonadBasicAst.v diff --git a/pcuic/_CoqProject.in b/pcuic/_CoqProject.in index 87ecee475d..7e6f43ddb0 100644 --- a/pcuic/_CoqProject.in +++ b/pcuic/_CoqProject.in @@ -91,6 +91,7 @@ theories/PCUICSafeLemmata.v theories/PCUICEtaExpand.v theories/PCUICProgram.v +theories/TemplateMonadToPCUIC.v theories/TemplateToPCUIC.v theories/TemplateToPCUICCorrectness.v theories/TemplateToPCUICWcbvEval.v @@ -101,6 +102,13 @@ theories/PCUICExpandLets.v theories/PCUICExpandLetsCorrectness.v theories/PCUICTransform.v +# The Template monad +theories/Loader.v +theories/PCUICTemplateMonad.v +theories/PCUICTemplateMonad/Common.v +theories/PCUICTemplateMonad/Core.v +theories/PCUICTemplateMonad/Extractable.v + theories/Bidirectional/BDTyping.v theories/Bidirectional/BDToPCUIC.v theories/Bidirectional/BDFromPCUIC.v diff --git a/pcuic/theories/Loader.v b/pcuic/theories/Loader.v new file mode 100644 index 0000000000..0a477ea0c6 --- /dev/null +++ b/pcuic/theories/Loader.v @@ -0,0 +1,7 @@ +(* Distributed under the terms of the MIT license. *) +From MetaCoq.Template Require Import Loader. +From MetaCoq.PCUIC.PCUICTemplateMonad Require Core. +From MetaCoq.PCUIC Require Import TemplateMonadToPCUIC. + +Notation "<% x %>" := (ltac:(let p y := exact y in let p y := run_template_program (@monad_trans Core.TypeInstance Core.TemplateMonad_Monad y) p in quote_term x p)) + (only parsing). diff --git a/pcuic/theories/PCUICTemplateMonad.v b/pcuic/theories/PCUICTemplateMonad.v new file mode 100644 index 0000000000..4c58094388 --- /dev/null +++ b/pcuic/theories/PCUICTemplateMonad.v @@ -0,0 +1,3 @@ +(* Distributed under the terms of the MIT license. *) +From MetaCoq.Template Require Export TemplateMonad. +From MetaCoq.PCUIC.PCUICTemplateMonad Require Export Common Core. diff --git a/pcuic/theories/PCUICTemplateMonad/Common.v b/pcuic/theories/PCUICTemplateMonad/Common.v new file mode 100644 index 0000000000..0b6473b70a --- /dev/null +++ b/pcuic/theories/PCUICTemplateMonad/Common.v @@ -0,0 +1,21 @@ +(* Distributed under the terms of the MIT license. *) +From MetaCoq.Template Require Import utils Ast. +From MetaCoq.Template.TemplateMonad Require Export Common. +From MetaCoq.PCUIC Require Import PCUICAst TemplateMonadToPCUIC TemplateToPCUIC PCUICToTemplate. + +Local Set Universe Polymorphism. +Import MCMonadNotation. + +Section with_tc. + Context {TM : TMInstance}. + Local Notation TemplateMonad := (@TemplateMonad TM). + Context {M : Monad TemplateMonad}. + + Definition tmQuoteInductive (kn : kername) : TemplateMonad mutual_inductive_body := tmQuoteInductive kn. + Definition tmQuoteConstant (kn : kername) (bypass_opacity : bool) : TemplateMonad constant_body := + cb <- tmQuoteConstant TM kn bypass_opacity;; monad_trans_constant_body cb. + (* +Definition tmMkInductive (b : bool) (mie : mutual_inductive_entry) : TemplateMonad unit + := tmMkInductive b (PCUICToTemplate.trans_mutual_inductive_entry mie). + *) +End with_tc. diff --git a/pcuic/theories/PCUICTemplateMonad/Core.v b/pcuic/theories/PCUICTemplateMonad/Core.v new file mode 100644 index 0000000000..461c4b41da --- /dev/null +++ b/pcuic/theories/PCUICTemplateMonad/Core.v @@ -0,0 +1,27 @@ +(* Distributed under the terms of the MIT license. *) +From MetaCoq.Template Require Import utils Ast AstUtils Common. +From MetaCoq.Template.TemplateMonad Require Export Core. +From MetaCoq.PCUIC Require Import PCUICAst TemplateMonadToPCUIC TemplateToPCUIC PCUICToTemplate. + +Local Set Universe Polymorphism. +Import MCMonadNotation. + +Local Notation monad_trans := (@monad_trans TypeInstance _). + +Definition tmQuote {A:Type} (a : A) : TemplateMonad PCUICAst.term := (qa <- tmQuote a;; monad_trans qa). +Definition tmQuoteRecTransp {A:Type} (a : A) (bypass_opacity : bool) : TemplateMonad PCUICProgram.pcuic_program := + (p <- tmQuoteRecTransp a bypass_opacity;; ret (trans_template_program p)). +Definition tmQuoteInductive (kn : kername) : TemplateMonad mutual_inductive_body := tmQuoteInductive (TM:=TypeInstance) kn. +Definition tmQuoteConstant (kn : kername) (bypass_opacity : bool) : TemplateMonad constant_body := + cb <- tmQuoteConstant kn bypass_opacity;; monad_trans_constant_body (TM:=TypeInstance) cb. +(* +Definition tmMkInductive (b : bool) (mie : mutual_inductive_entry) : TemplateMonad unit + := tmMkInductive b (PCUICToTemplate.trans_mutual_inductive_entry mie). + *) +Definition tmUnquote (t : PCUICAst.term) : TemplateMonad typed_term := tmUnquote (PCUICToTemplate.trans t). +Definition tmUnquoteTyped A (t : PCUICAst.term) : TemplateMonad A := tmUnquoteTyped A (PCUICToTemplate.trans t). + +(** We keep the original behaviour of [tmQuoteRec]: it quotes all the dependencies regardless of the opaqueness settings *) +Definition tmQuoteRec {A} (a : A) := tmQuoteRecTransp a true. + +Definition tmMkDefinition (id : ident) (tm : PCUICAst.term) : TemplateMonad unit := tmMkDefinition id (PCUICToTemplate.trans tm). diff --git a/pcuic/theories/PCUICToTemplate.v b/pcuic/theories/PCUICToTemplate.v index 24901b2f93..dd7af97c19 100644 --- a/pcuic/theories/PCUICToTemplate.v +++ b/pcuic/theories/PCUICToTemplate.v @@ -111,3 +111,31 @@ Definition trans_global_env (d : PCUICEnvironment.global_env) : global_env := Definition trans_global (Σ : PCUICEnvironment.global_env_ext) : global_env_ext := (trans_global_env (fst Σ), snd Σ). + +Definition trans_one_inductive_entry (oie : PCUICAst.one_inductive_entry) : one_inductive_entry + := {| mind_entry_typename := oie.(PCUICAst.mind_entry_typename); + mind_entry_arity := trans oie.(PCUICAst.mind_entry_arity); + mind_entry_consnames := oie.(PCUICAst.mind_entry_consnames); + mind_entry_lc := List.map trans oie.(PCUICAst.mind_entry_lc); |}. + +(* +(* It would be nice to have this, but it seems to not be possible *) +Definition trans_mutual_inductive_entry (mie : PCUICAst.mutual_inductive_entry) : mutual_inductive_entry. + refine {| mind_entry_record := mie.(PCUICAst.mind_entry_record); + mind_entry_finite := mie.(PCUICAst.mind_entry_finite); + mind_entry_private := mie.(PCUICAst.mind_entry_private); + mind_entry_universes := universes_entry_of_decl mie.(PCUICAst.mind_entry_universes); + mind_entry_inds := List.map trans_one_inductive_entry mie.(PCUICAst.mind_entry_inds); + mind_entry_params := trans_local + (* TODO Should this be extracted? *) + (List.map (fun '(id, le) + => let dname := {| binder_name := nNamed id ; binder_relevance := _ (* ??? *) |} in + match le with + | LocalDef x => {| decl_name := dname ; decl_type := _ (* ??? *) ; decl_body := Some x |} + | LocalAssum x => {| decl_name := dname ; decl_type := x ; decl_body := None |} + end) + mie.(PCUICAst.mind_entry_params)); + mind_entry_variance := _ (* ??? *); + mind_entry_template := false |}. +Abort. +*) diff --git a/pcuic/theories/TemplateMonadToPCUIC.v b/pcuic/theories/TemplateMonadToPCUIC.v new file mode 100644 index 0000000000..ddfe896c34 --- /dev/null +++ b/pcuic/theories/TemplateMonadToPCUIC.v @@ -0,0 +1,153 @@ +(* Distributed under the terms of the MIT license. *) +From Coq Require Import Uint63 FloatOps FloatAxioms. +From MetaCoq.Template Require Import config utils AstUtils MonadAst MonadBasicAst Primitive EnvMap. +From MetaCoq.Template Require TemplateProgram. +From MetaCoq.Template Require Import TemplateMonad.Common monad_utils. +From MetaCoq.PCUIC Require Import PCUICAst PCUICPrimitive PCUICCases PCUICProgram TemplateToPCUIC. + +Import MCMonadNotation. + +(** XXX FIXME THIS IS A HACK *) +Local Unset Guard Checking. +Fixpoint tmFix' {TM : TMInstance} {A B} (f : (A -> @TemplateMonad TM B) -> (A -> @TemplateMonad TM B)) (dummy : unit) {struct dummy} : A -> @TemplateMonad TM B + := f (fun a => tmFix' f tt a). +Local Set Guard Checking. + +Section with_tc. + Context {TM : TMInstance}. + Local Notation TemplateMonad := (@TemplateMonad TM). + Context {M : Monad TemplateMonad}. + + Definition tmFix {A B} (f : (A -> TemplateMonad B) -> (A -> TemplateMonad B)) : A -> TemplateMonad B + := tmFix' f tt. + + Section helpers. + Context (monad_trans : Ast.term -> TemplateMonad term). + + Definition monad_trans_decl' (d : Ast.Env.context_decl) := + decl_body <- monad_option_map monad_trans d.(decl_body);; + decl_type <- monad_trans d.(decl_type);; + ret {| decl_name := d.(decl_name); + decl_body := decl_body; + decl_type := decl_type |}. + + Definition monad_trans_local' Γ := monad_map monad_trans_decl' Γ. + + Definition monad_trans_constructor_body' (d : Ast.Env.constructor_body) := + cstr_args <- monad_trans_local' d.(Ast.Env.cstr_args);; + cstr_indices <- monad_map monad_trans d.(Ast.Env.cstr_indices);; + cstr_type <- monad_trans d.(Ast.Env.cstr_type);; + ret {| cstr_name := d.(Ast.Env.cstr_name); + cstr_args := cstr_args; + cstr_indices := cstr_indices; + cstr_type := cstr_type; + cstr_arity := d.(Ast.Env.cstr_arity) |}. + Definition monad_trans_projection_body' (d : Ast.Env.projection_body) := + proj_type <- monad_trans d.(Ast.Env.proj_type);; + ret {| proj_name := d.(Ast.Env.proj_name); + proj_type := proj_type; + proj_relevance := d.(Ast.Env.proj_relevance) |}. + + Definition monad_trans_one_ind_body' (d : Ast.Env.one_inductive_body) := + ind_indices <- monad_trans_local' d.(Ast.Env.ind_indices);; + ind_type <- monad_trans d.(Ast.Env.ind_type);; + ind_ctors <- monad_map monad_trans_constructor_body' d.(Ast.Env.ind_ctors);; + ind_projs <- monad_map monad_trans_projection_body' d.(Ast.Env.ind_projs);; + ret {| ind_name := d.(Ast.Env.ind_name); + ind_relevance := d.(Ast.Env.ind_relevance); + ind_indices := ind_indices; + ind_sort := d.(Ast.Env.ind_sort); + ind_type := ind_type; + ind_kelim := d.(Ast.Env.ind_kelim); + ind_ctors := ind_ctors; + ind_projs := ind_projs |}. + + Definition monad_trans_constant_body' bd := + cst_type <- monad_trans bd.(Ast.Env.cst_type);; + cst_body <- monad_option_map monad_trans bd.(Ast.Env.cst_body);; + ret {| cst_type := cst_type; + cst_body := cst_body; + cst_universes := bd.(Ast.Env.cst_universes); + cst_relevance := bd.(Ast.Env.cst_relevance) |}. + + Definition monad_trans_minductive_body' md := + ind_params <- monad_trans_local' md.(Ast.Env.ind_params);; + ind_bodies <- monad_map monad_trans_one_ind_body' md.(Ast.Env.ind_bodies);; + ret {| ind_finite := md.(Ast.Env.ind_finite); + ind_npars := md.(Ast.Env.ind_npars); + ind_params := ind_params; + ind_bodies := ind_bodies; + ind_universes := md.(Ast.Env.ind_universes); + ind_variance := md.(Ast.Env.ind_variance) |}. + + Definition monad_trans_global_decl' (d : Ast.Env.global_decl) := + match d with + | Ast.Env.ConstantDecl bd => bd <- monad_trans_constant_body' bd;; ret (ConstantDecl bd) + | Ast.Env.InductiveDecl bd => bd <- monad_trans_minductive_body' bd;; ret (InductiveDecl bd) + end. + + Definition tmQuoteInductive' (mind : kername) : TemplateMonad mutual_inductive_body := + bd <- tmQuoteInductive TM mind;; + monad_trans_minductive_body' bd. + + Definition TransLookup_lookup_inductive' (ind : inductive) : TemplateMonad (mutual_inductive_body × one_inductive_body) := + mdecl <- tmQuoteInductive' (inductive_mind ind);; + match nth_error (ind_bodies mdecl) (inductive_ind ind) with + | Some idecl => ret (mdecl, idecl) + | None => tmFail TM "TransLookup.lookup_inductive: nth_error: Not_found" + end. + + End helpers. + + Section with_helper. + Context (TransLookup_lookup_inductive' : inductive -> TemplateMonad (mutual_inductive_body × one_inductive_body)). + + Fixpoint monad_trans' (t : Ast.term) : TemplateMonad term + := match t with + | Ast.tRel n => ret (tRel n) + | Ast.tVar n => ret (tVar n) + | Ast.tEvar ev args => args <- monad_map monad_trans' args;; ret (tEvar ev args) + | Ast.tSort u => ret (tSort u) + | Ast.tConst c u => ret (tConst c u) + | Ast.tInd c u => ret (tInd c u) + | Ast.tConstruct c k u => ret (tConstruct c k u) + | Ast.tLambda na T M => T <- monad_trans' T;; M <- monad_trans' M;; ret (tLambda na T M) + | Ast.tApp u v => u <- monad_trans' u;; v <- monad_map monad_trans' v;; ret (mkApps u v) + | Ast.tProd na A B => A <- monad_trans' A;; B <- monad_trans' B;; ret (tProd na A B) + | Ast.tCast c kind t => t <- monad_trans' t;; c <- monad_trans' c;; ret (tApp (tLambda (mkBindAnn nAnon Relevant) t (tRel 0)) c) + | Ast.tLetIn na b t b' => b <- monad_trans' b;; t <- monad_trans' t;; b' <- monad_trans' b';; ret (tLetIn na b t b') + | Ast.tCase ci p c brs => + p' <- monad_map_predicate ret monad_trans' monad_trans' p;; + brs' <- monad_map (monad_map_branch monad_trans') brs;; + '(mdecl, idecl) <- TransLookup_lookup_inductive' ci.(ci_ind);; + let tp := trans_predicate ci.(ci_ind) mdecl idecl p'.(Ast.pparams) p'.(Ast.puinst) p'.(Ast.pcontext) p'.(Ast.preturn) in + let tbrs := + map2 (fun cdecl br => trans_branch ci.(ci_ind) mdecl cdecl br.(Ast.bcontext) br.(Ast.bbody)) + idecl.(ind_ctors) brs' in + c <- monad_trans' c;; + ret (tCase ci tp c tbrs) + | Ast.tProj p c => c <- monad_trans' c;; ret (tProj p c) + | Ast.tFix mfix idx => + mfix' <- monad_map (monad_map_def monad_trans' monad_trans') mfix;; + ret (tFix mfix' idx) + | Ast.tCoFix mfix idx => + mfix' <- monad_map (monad_map_def monad_trans' monad_trans') mfix;; + ret (tCoFix mfix' idx) + | Ast.tInt n => ret (tPrim (primInt; primIntModel n)) + | Ast.tFloat n => ret (tPrim (primFloat; primFloatModel n)) + end. + End with_helper. + + Definition monad_trans : (Ast.term -> TemplateMonad term) + := tmFix (fun monad_trans => monad_trans' (TransLookup_lookup_inductive' monad_trans)). + + Definition monad_trans_decl := monad_trans_decl' monad_trans. + Definition monad_trans_local := monad_trans_local' monad_trans. + Definition monad_trans_constructor_body := monad_trans_constructor_body' monad_trans. + Definition monad_trans_projection_body := monad_trans_projection_body' monad_trans. + Definition monad_trans_one_ind_body := monad_trans_one_ind_body' monad_trans. + Definition monad_trans_constant_body := monad_trans_constant_body' monad_trans. + Definition monad_trans_minductive_body := monad_trans_minductive_body' monad_trans. + Definition monad_trans_global_decl := monad_trans_global_decl' monad_trans. + Definition tmQuoteInductive := tmQuoteInductive' monad_trans. +End with_tc. diff --git a/template-coq/_CoqProject b/template-coq/_CoqProject index aedc2aed0d..a240738fb9 100644 --- a/template-coq/_CoqProject +++ b/template-coq/_CoqProject @@ -75,6 +75,10 @@ theories/TemplateMonad/Core.v theories/TemplateMonad/Extractable.v theories/monad_utils.v +# Extra Template monad +theories/MonadAst.v +theories/MonadBasicAst.v + # Bindings of Coq terms to the "metacoq.*" names theories/Constants.v diff --git a/template-coq/gen-src/cRelationClasses.mli.orig b/template-coq/gen-src/cRelationClasses.mli.orig index c49080220d..49a8d3f488 100644 --- a/template-coq/gen-src/cRelationClasses.mli.orig +++ b/template-coq/gen-src/cRelationClasses.mli.orig @@ -14,6 +14,10 @@ type ('a, 'r) coq_Reflexive = 'a -> 'r val reflexivity : ('a1, 'a2) coq_Reflexive -> 'a1 -> 'a2 +type ('a, 'r) complement = __ + +type ('a, 'r) coq_Irreflexive = ('a, ('a, 'r) complement) coq_Reflexive + type ('a, 'r) coq_Symmetric = 'a -> 'a -> 'r -> 'r val symmetry : ('a1, 'a2) coq_Symmetric -> 'a1 -> 'a1 -> 'a2 -> 'a2 @@ -33,9 +37,10 @@ val coq_PreOrder_Reflexive : val coq_PreOrder_Transitive : ('a1, 'a2) coq_PreOrder -> ('a1, 'a2) coq_Transitive -type ('a, 'r) coq_StrictOrder = - ('a, 'r) coq_Transitive - (* singleton inductive, whose constructor was Build_StrictOrder *) +type ('a, 'r) coq_StrictOrder = { coq_StrictOrder_Irreflexive : ('a, 'r) + coq_Irreflexive; + coq_StrictOrder_Transitive : ('a, 'r) + coq_Transitive } val coq_StrictOrder_Transitive : ('a1, 'a2) coq_StrictOrder -> ('a1, 'a2) coq_Transitive @@ -104,19 +109,18 @@ val iff_equivalence : (__, __) coq_Equivalence val arrow_Reflexive_obligation_1 : ('a1, 'a1) arrow -val arrow_Reflexive : ('a1, 'a1) arrow +val arrow_Reflexive : (__, __) arrow val arrow_Transitive_obligation_1 : ('a1, 'a2) arrow -> ('a2, 'a3) arrow -> ('a1, 'a3) arrow -val arrow_Transitive : - ('a1, 'a2) arrow -> ('a2, 'a3) arrow -> ('a1, 'a3) arrow +val arrow_Transitive : (__, __) arrow -> (__, __) arrow -> (__, __) arrow -val iffT_Reflexive : ('a1, 'a1) iffT +val iffT_Reflexive : (__, __) iffT -val iffT_Symmetric : ('a1, 'a2) iffT -> ('a2, 'a1) iffT +val iffT_Symmetric : (__, __) iffT -> (__, __) iffT -val iffT_Transitive : ('a1, 'a2) iffT -> ('a2, 'a3) iffT -> ('a1, 'a3) iffT +val iffT_Transitive : (__, __) iffT -> (__, __) iffT -> (__, __) iffT type ('a, 'x0, 'x) relation_equivalence = 'a -> 'a -> ('x0, 'x) iffT diff --git a/template-coq/theories/MonadAst.v b/template-coq/theories/MonadAst.v new file mode 100644 index 0000000000..d8c87b7fcb --- /dev/null +++ b/template-coq/theories/MonadAst.v @@ -0,0 +1,58 @@ +(* Distributed under the terms of the MIT license. *) +From MetaCoq.Template Require Import utils. +From MetaCoq.Template Require Import Ast. +From MetaCoq.Template Require Import TemplateMonad.Common monad_utils. + +Import MCMonadNotation. + +Section with_tc. + Context {TM : TMInstance}. + Local Notation TemplateMonad := (@TemplateMonad TM). + Context {M : Monad TemplateMonad}. + + Section map_predicate. + Context {term term' : Type}. + Context (uf : Instance.t -> TemplateMonad Instance.t). + Context (paramf preturnf : term -> TemplateMonad term'). + + Definition monad_map_predicate (p : predicate term) := + pparams <- monad_map paramf p.(pparams);; + puinst <- uf p.(puinst);; + preturn <- preturnf p.(preturn);; + ret {| pparams := pparams; + puinst := puinst; + pcontext := p.(pcontext); + preturn := preturn |}. + End map_predicate. + + Section map_predicate_k. + Context {term : Type}. + Context (uf : Instance.t -> TemplateMonad Instance.t). + Context (f : nat -> term -> TemplateMonad term). + + Definition monad_map_predicate_k k (p : predicate term) := + pparams <- monad_map (f k) p.(pparams);; + puinst <- uf p.(puinst);; + preturn <- f (#|p.(pcontext)| + k) p.(preturn);; + ret {| pparams := pparams; + puinst := puinst; + pcontext := p.(pcontext); + preturn := preturn |}. + + End map_predicate_k. + + Section map_branch. + Context {term term' : Type}. + Context (bbodyf : term -> TemplateMonad term'). + + Definition monad_map_branch (b : branch term) := + bbody <- bbodyf b.(bbody);; + ret {| bcontext := b.(bcontext); + bbody := bbody |}. + End map_branch. + + Definition monad_map_branches {term B} (f : term -> TemplateMonad B) l := monad_map (monad_map_branch f) l. + + Notation map_branches_k f k brs := + (monad_map (fun b => monad_map_branch (f (#|b.(bcontext)| + k)) b) brs). +End with_tc. diff --git a/template-coq/theories/MonadBasicAst.v b/template-coq/theories/MonadBasicAst.v new file mode 100644 index 0000000000..6ff3ac17fe --- /dev/null +++ b/template-coq/theories/MonadBasicAst.v @@ -0,0 +1,78 @@ +(* Distributed under the terms of the MIT license. *) +From MetaCoq.Template Require Import utils. +From MetaCoq.Template Require Import BasicAst. +From MetaCoq.Template Require Import TemplateMonad.Common monad_utils. + +Import MCMonadNotation. +Local Set Universe Polymorphism. +Local Unset Universe Minimization ToSet. + +Section with_tc. + Context {TM : TMInstance}. + Local Notation TemplateMonad := (@TemplateMonad TM). + Context {M : Monad TemplateMonad}. + + Definition monad_map_binder_annot {A B} (f : A -> TemplateMonad B) (b : binder_annot A) : TemplateMonad (binder_annot B) := + binder_name <- f b.(binder_name);; ret {| binder_name := binder_name; binder_relevance := b.(binder_relevance) |}. + + Definition monad_map_def {A B} (tyf bodyf : A -> TemplateMonad B) (d : def A) := + dtype <- tyf d.(dtype);; dbody <- bodyf d.(dbody);; ret {| dname := d.(dname); dtype := dtype; dbody := dbody; rarg := d.(rarg) |}. + + Definition monad_typ_or_sort_map {T T'} (f: T -> TemplateMonad T') t := + match t with + | Typ T => fT <- f T;; ret (Typ fT) + | Sort => ret Sort + end. + + Definition monad_map_decl {term term'} (f : term -> TemplateMonad term') (d : context_decl term) : TemplateMonad (context_decl term') := + decl_body <- monad_option_map f d.(decl_body);; + decl_type <- f d.(decl_type);; + ret {| decl_name := d.(decl_name); + decl_body := decl_body; + decl_type := decl_type |}. + + Definition monad_map_context {term term'} (f : term -> TemplateMonad term') (c : list (context_decl term)) := + monad_map (monad_map_decl f) c. + + Section ContextMap. + Context {term term' : Type} (f : nat -> term -> TemplateMonad term'). + + (* N.B. this does not universe check without [Local Unset Universe Minimization ToSet.] above *) + Fixpoint monad_mapi_context (c : list (context_decl term)) : TemplateMonad (list (context_decl term')) := + match c with + | d :: Γ => d <- monad_map_decl (f #|Γ|) d;; Γ <- monad_mapi_context Γ;; ret (d :: Γ) + | [] => ret [] + end. + End ContextMap. + + Section Contexts. + Context {term term' term'' : Type}. + Notation context term := (list (context_decl term)). + + Definition monad_fold_context_k (f : nat -> term -> TemplateMonad term') Γ := + Γ <- monad_map_i (fun k' decl => monad_map_decl (f k') decl) (List.rev Γ);; ret (List.rev Γ). + + Arguments monad_fold_context_k f Γ%list_scope. + + Local Set Keyed Unification. + + Equations monad_mapi_context_In (ctx : context term) (f : nat -> forall (x : context_decl term), In x ctx -> TemplateMonad (context_decl term)) : TemplateMonad (context term) := + monad_mapi_context_In nil _ := ret nil; + monad_mapi_context_In (cons x xs) f := fx <- (f #|xs| x _);; fxs <- monad_mapi_context_In xs (fun n x H => f n x _);; ret (cons fx fxs). + + Equations monad_fold_context_In (ctx : context term) (f : context term -> forall (x : context_decl term), In x ctx -> TemplateMonad (context_decl term)) : TemplateMonad (context term) := + monad_fold_context_In nil _ := ret nil; + monad_fold_context_In (cons x xs) f := + xs' <- monad_fold_context_In xs (fun n x H => f n x _);; + x' <- f xs' x _;; + ret (cons x' xs'). + + Equations monad_fold_context (f : context term -> context_decl term -> TemplateMonad (context_decl term)) (ctx : context term) : TemplateMonad (context term) := + monad_fold_context f nil := ret nil; + monad_fold_context f (cons x xs) := + xs' <- monad_fold_context f xs;; + x' <- f xs' x;; + ret (cons x' xs'). + + End Contexts. +End with_tc. diff --git a/template-coq/theories/TemplateMonad/Common.v b/template-coq/theories/TemplateMonad/Common.v index e404e941a8..60ac98e0dc 100644 --- a/template-coq/theories/TemplateMonad/Common.v +++ b/template-coq/theories/TemplateMonad/Common.v @@ -5,7 +5,7 @@ Local Set Universe Polymorphism. (** Reduction strategy to apply, beware [cbv], [cbn] and [lazy] are _strong_. *) - + Monomorphic Variant reductionStrategy : Set := cbv | cbn | hnf | all | lazy | unfold (i : kername). @@ -52,3 +52,10 @@ Monomorphic Variant import_status : Set := Monomorphic Variant locality := | Discharge | Global (_ : import_status). + +(** XXX FIXME THIS IS A HACK *) +Local Unset Guard Checking. +Definition tmFix (TM : TMInstance) {A B} (f : (A -> TemplateMonad TM B) -> (A -> TemplateMonad TM B)) : A -> TemplateMonad TM B + := (fix tmFix (dummy : unit) {struct dummy} : A -> @TemplateMonad TM B + := f (fun a => tmFix tt a)) tt. +Local Set Guard Checking. diff --git a/template-coq/theories/TemplateMonad/Core.v b/template-coq/theories/TemplateMonad/Core.v index 7e3d594fa7..9b82b1e397 100644 --- a/template-coq/theories/TemplateMonad/Core.v +++ b/template-coq/theories/TemplateMonad/Core.v @@ -2,6 +2,7 @@ From MetaCoq.Template Require Import utils Ast AstUtils Common. Local Set Universe Polymorphism. +Local Unset Universe Minimization ToSet. Import MCMonadNotation. (** * The Template Monad @@ -117,3 +118,21 @@ Definition tmMkDefinition (id : ident) (tm : term) : TemplateMonad unit t'' <- tmEval (unfold (Common_kn "my_projT2")) (my_projT2 t') ;; tmDefinitionRed id (Some (unfold (Common_kn "my_projT1"))) t'' ;; tmReturn tt. + +Definition TypeInstance : Common.TMInstance := + {| Common.TemplateMonad := TemplateMonad + ; Common.tmReturn:=@tmReturn + ; Common.tmBind:=@tmBind + ; Common.tmFail:=@tmFail + ; Common.tmFreshName:=@tmFreshName + ; Common.tmLocate:=@tmLocate + ; Common.tmCurrentModPath:=@tmCurrentModPath + ; Common.tmQuoteInductive:=@tmQuoteInductive + ; Common.tmQuoteUniverses:=@tmQuoteUniverses + ; Common.tmQuoteConstant:=@tmQuoteConstant + ; Common.tmMkInductive:=@tmMkInductive + ; Common.tmExistingInstance:=@tmExistingInstance + |}. + +Definition tmFix {A B} (f : (A -> TemplateMonad B) -> (A -> TemplateMonad B)) : A -> TemplateMonad B + := @tmFix TypeInstance A B f. diff --git a/template-coq/theories/TemplateMonad/Extractable.v b/template-coq/theories/TemplateMonad/Extractable.v index 596bb09f0d..4a4e7271f7 100644 --- a/template-coq/theories/TemplateMonad/Extractable.v +++ b/template-coq/theories/TemplateMonad/Extractable.v @@ -108,3 +108,6 @@ Definition tmDefinitionRed (opaque : bool) (i : ident) (rd : reductionStrategy) Definition tmInferInstanceRed (rd : reductionStrategy) (type : Ast.term) : TM (option Ast.term) := tmBind (tmEval rd type) (fun type => tmInferInstance type). + +Definition tmFix {A B} (f : (A -> TM B) -> (A -> TM B)) : A -> TM B + := @tmFix TypeInstance A B f.