Stream: MetaCoq

Topic: Way to call unquote from a coq function


view this post on Zulip 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 |} []).

view this post on Zulip Julin S (Jan 03 2022 at 10:24):

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.

view this post on Zulip Julin S (Jan 03 2022 at 10:55):

As in mixing metacoq and non-metacoq together.

view this post on Zulip Théo Winterhalter (Jan 03 2022 at 11:00):

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

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Fabian Kunze (Jan 03 2022 at 13:21):

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

view this post on Zulip Julin S (Jan 04 2022 at 04:06):

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

view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip 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: Aug 11 2022 at 01:03 UTC