The Coq mailing list

[Gregory Malecha <gmalecha AT gmail.com>]

I'm not certain about the details of the quote plugin, but the Reify plugin in MirrorCore is programmable enough to do what you want to do and decoupled from the rest of the system enough that you can reify to any language that you would like.

On Mon, Jan 11, 2016 at 5:50 AM, Robbert Krebbers <mailinglists AT robbertkrebbers.nl> wrote:

I was looking for some means to do some lightweight reification without the need for writing an OCaml plugin or the using Ltac/type classes/canonical structures (which are too slow), so I stumbled on the [quote] tactic. Unfortunately, I cannot get it to work for polymorphic data types like lists, see below.

Does anyone know whether I am doing something wrong, or whether [quote] just does not support my use case below.

======================================

Require Import Quote.

Inductive formula : Type :=
  | f_nil : formula
  | f_app : formula -> formula -> formula
  | f_atom : index -> formula.

Fixpoint interp_f {A} (vm : varmap (list A)) (f:formula) : list A :=
  match f with
  | f_nil => nil
  | f_app f1 f2 => interp_f vm f1 ++ interp_f vm f2
  | f_atom i => varmap_find nil i vm
  end.

Goal forall x : list nat, True.
intros.

quote interp_f in (x ++ x ++ nil)%list using (fun x => idtac x).
(* Yields nonsense *)

quote (@interp_f nat) in (x ++ x ++ nil)%list using (fun x => idtac x).
(* Fails with Syntax error: [prim:ident] expected after 'quote' (in [tactic:simple_tactic]). *)

--

gregory malecha