Julin S (Jan 03 2022 at 10:20): Julin S (Jan 03 2022 at 10:20):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.
Julin S (Jan 03 2022 at 10:55):As in mixing metacoq and non-metacoq together.
Théo Winterhalter (Jan 03 2022 at 11:00):I don't think so. Quoting and unquoting are not internal.
Fabian Kunze (Jan 03 2022 at 13:14):Do you know that you can use the TemplateMonad to write Programms for MetaCoq as coq functions?
Fabian Kunze (Jan 03 2022 at 13:16):This way, one can implement transformations inside Coq, and only for executing those monadic functions, a 'special' Command (MetaCoq Run) is needed.
Fabian Kunze (Jan 03 2022 at 13:21):See https://github.com/MetaCoq/metacoq/blob/coq-8.13/examples/demo.v
Julin S (Jan 04 2022 at 04:06):Thanks. I hadn't tried templatemonad. I'll try that.
Julin S (Jan 07 2022 at 04:36):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?
Julin S (Jan 07 2022 at 04:37):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?
Julin S (Jan 07 2022 at 05:43):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