feat: Add Symbol to TemplateMonad

Author: TDiazT

template-rocq/src/run_template_monad.ml

@@ -365,6 +365,17 @@ let rec run_template_program_rec ~poly ?(intactic=false) (k : Constr.t Plugin_co
       Declare.declare_variable ~typing_flags:None ~name ~kind (SectionLocalAssum { typ; impl=Glob_term.Explicit; univs=empty_mono_univ_entry });
       let env = Global.env () in
       k ~st env evm (Lazy.force unit_tt)
+ | TmSymbol (name, typ) ->
+    if intactic then not_in_tactic "tmSymbol"
+    else
+      let name = unquote_ident (reduce_all env evm name) in
+      let udecl = UState.default_univ_decl in
+      let univs = Evd.check_univ_decl ~poly evm udecl in
+      let entry = Declare.symbol_entry ~univs ~unfold_fix:false typ in
+      let kn = Declare.declare_constant ~name ~kind:Decls.IsSymbol (Declare.SymbolEntry entry) in
+      let () = Declare.assumption_message name in
+      let env = Global.env () in
+      k ~st env evm (Constr.mkConstU (kn, UVars.Instance.empty))
   | TmDefinition (opaque,name,s,typ,body) ->
     if intactic
     then not_in_tactic "tmDefinition"

template-rocq/src/template_monad.ml

@@ -24,6 +24,7 @@ let (ptmReturn,
      ptmMkDefinition,
      ptmMkInductive,
      ptmVariable,
+     ptmSymbol,
 
      ptmFreshName,
 
@@ -67,6 +68,7 @@ let (ptmReturn,
    r_template_monad_prop_p "tmMkDefinition",
    r_template_monad_prop_p "tmMkInductive",
    r_template_monad_prop_p "tmVariable",
+   r_template_monad_prop_p "tmSymbol",
 
    r_template_monad_prop_p "tmFreshName",
 
@@ -179,6 +181,7 @@ type template_monad =
   | TmAxiomTerm of Constr.t * Constr.t
   | TmMkInductive of Constr.t * Constr.t
   | TmVariable of Constr.t * Constr.t
+  | TmSymbol of Constr.t * Constr.t
 
   | TmFreshName of Constr.t
 
@@ -400,6 +403,10 @@ let next_action env evd (pgm : constr) : template_monad * _ =
     match args with
     | name::ty::[] -> (TmVariable (name,ty) , universes)
     | _ -> monad_failure "tmVariable" 2
+  else if eq_gr ptmSymbol then
+    match args with
+    | name :: ty :: [] -> (TmSymbol (name, ty), universes)
+    | _ -> monad_failure "tmSymbol" 2
   else if eq_gr ttmInductive then
     match args with
     | inferu :: mind::[] -> (TmMkInductive (inferu, mind), universes)

template-rocq/src/template_monad.mli

@@ -30,6 +30,7 @@ type template_monad =
   | TmAxiomTerm of Constr.t * Constr.t
   | TmMkInductive of Constr.t * Constr.t
   | TmVariable of Constr.t * Constr.t
+  | TmSymbol of Constr.t * Constr.t
 
   | TmFreshName of Constr.t
 

template-rocq/theories/Constants.v

@@ -245,6 +245,7 @@ Register MetaRocq.Template.TemplateMonad.Core.tmMsg as metarocq.templatemonad.pr
 Register MetaRocq.Template.TemplateMonad.Core.tmFail as metarocq.templatemonad.prop.tmFail.
 Register MetaRocq.Template.TemplateMonad.Core.tmEval as metarocq.templatemonad.prop.tmEval.
 Register MetaRocq.Template.TemplateMonad.Core.tmVariable as metarocq.templatemonad.prop.tmVariable.
+Register MetaRocq.Template.TemplateMonad.Core.tmSymbol as metarocq.templatemonad.prop.tmSymbol.
 Register MetaRocq.Template.TemplateMonad.Core.tmLemma as metarocq.templatemonad.prop.tmLemma.
 Register MetaRocq.Template.TemplateMonad.Core.tmDefinitionRed_ as metarocq.templatemonad.prop.tmDefinitionRed_.
 Register MetaRocq.Template.TemplateMonad.Core.tmAxiomRed as metarocq.templatemonad.prop.tmAxiomRed.

template-rocq/theories/TemplateMonad/Core.v

@@ -33,6 +33,7 @@ Cumulative Inductive TemplateMonad@{t u} : Type@{t} -> Prop :=
 | tmDefinitionRed_ : forall (opaque : bool), ident -> option reductionStrategy -> forall {A:Type@{t}}, A -> TemplateMonad A
 | tmAxiomRed : ident -> option reductionStrategy -> forall A : Type@{t}, TemplateMonad A
 | tmVariable : ident -> Type@{t} -> TemplateMonad unit
+| tmSymbol : ident -> Type@{t} -> TemplateMonad unit
 
 (* Guaranteed to not cause "... already declared" error *)
 | tmFreshName : ident -> TemplateMonad ident