Is there a way to call metacoq quote and unquote (of template-coq) from within coq functions?

Something like

```
Definition foo := MetaCoq Unquote
(tInd
{|
inductive_mind := (MPfile ["Datatypes"; "Init"; "Coq"], "nat");
inductive_ind := 0 |} []).
```

instead of

```
MetaCoq Unquote Definition unqNat :=
(tInd
{|
inductive_mind := (MPfile ["Datatypes"; "Init"; "Coq"], "nat");
inductive_ind := 0 |} []).
```

I was sort of trying to see if something like

```
Definition unqt (t : term) : Type :=
let MetaCoq Unquote Defintion temp := t in
temp.
```

was possible.

As in mixing metacoq and non-metacoq together.

I don't think so. Quoting and unquoting are not internal.

Do you know that you can use the TemplateMonad to write Programms for MetaCoq as coq functions?

This way, one can implement transformations inside Coq, and only for executing those monadic functions, a 'special' Command (`MetaCoq Run`

) is needed.

See https://github.com/MetaCoq/metacoq/blob/coq-8.13/examples/demo.v

Thanks. I hadn't tried templatemonad. I'll try that.

I tried imitating this function from the demo.v for metacoq1.0~beta1+8.12,

```
Definition printConstant' (name : qualid): TemplateMonad unit :=
gr <- tmLocate1 name ;;
match gr with
| ConstRef kn => X <- tmUnquote (tConst kn []) ;;
X' <- tmEval all (my_projT2 X) ;;
tmPrint X'
| _ => tmFail ("[" ++ name ++ "] is not a constant")
end.
```

I tried

```
Definition foo := (tInd
{|
inductive_mind := (MPfile ["Datatypes"; "Init"; "Coq"], "nat");
inductive_ind := 0 |} []).
MetaCoq Test Unquote foo. (* nat *)
Definition bar (t : term): TemplateMonad unit :=
match t with
| tInd ind u =>
x <- tmUnquote t ;;
x' <- tmEval all (my_projT2 x) ;;
tmPrint x'
| _ => tmFail ("not a tInd")
end.
```

But the result still looks like a quoted term.

```
Compute bar foo.
(*
= tmBind
(tmUnquote
(tInd
{|
inductive_mind := (MPfile ["Datatypes"; "Init"; "Coq"], "nat");
inductive_ind := 0 |} []))
(fun x : typed_term =>
tmBind (tmEval all (my_projT2 x))
(fun x0 : my_projT1 x => tmPrint x0))
: TemplateMonad unit
*)
```

Where am I going wrong?

`tmLocate1`

is used to find a definition based on its name, right? If so, it is not needed for `bar`

as the argument itself is a quoted term?

Oh.. I guess I needed to use `MetaCoq Run`

as was mentioned earlier.

Working now.

```
MetaCoq Run (bar foo).
(* nat *)
```

Last updated: May 31 2023 at 09:01 UTC