The Coq mailing list

[Kenneth Roe <kendroe AT hotmail.com>]

Actually, the above only partially answers my question. I still need to know how to generate "modpath" and "dirpath".  I'm starting with the string "C_Top.x" and I presume that "C_Top" is the path for the top level environment.

                - Ken

---

From: Kenneth Roe <kendroe AT hotmail.com>
Sent: Thursday, November 16, 2017 11:31 AM
To: Talia Ringer
Subject: Re: [Coq-Club] Looking up definitions from inside an ml plugin

 

Thanks.  By the way, you might want to take a look at the repository at https://github.com/kendroe/CoqRewriter.  This is the rewriting plugin that I'm creating.  The Coq interface is based on your printAST code.  I recently converted this code to Coq 8.7.  You can take the plugin.ml4 file and strip out all the stuff related to the rewriter.  I kept the printAST function intact.

                               - Ken

---

From: coq-club-request AT inria.fr <coq-club-request AT inria.fr> on behalf of Talia Ringer <tringer AT cs.washington.edu>
Sent: Thursday, November 16, 2017 10:31 AM
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Looking up definitions from inside an ml plugin

 

I should note that, if you have access to the term itself, unquestionably the best way to do this is to not make it a string to begin with. In traversing the AST for the term:

forall x, x=Const 4

When traversing the product Prod (n, t, b), and then recursing in and evaluating t, you should eventually get a term Ind((i, _), _). Similarly, when recursing into the body b, you should find that it is a constructor Construct (((i, _), _, _). So you can pass that in directly to look up the inductive type.

If the user is providing you an argument, then rather than making that argument a string, you can make that argument a term. You'll have to intern that term to then traverse the AST in the current environment.

The only time I had to ever go to strings was when I was working around limitations of my tool, so it's understandable that it can happen sometimes, but often you're able to use a much better format and never deal with strings at all.

On Thu, Nov 16, 2017 at 10:17 AM, Talia Ringer <tringer AT cs.washington.edu> wrote:

It is an i of type mutual_inductive, which is an alias for MutInd.t. You can find MutInd.t in names.mli.

You can get that from the AST in this way:

| Construct (((i, _), _, _) ->

   let mutind_body = lookup_mind i env in ...

| Ind ((i, _), _) ->

   let mutind_body = lookup_mind i env in ...

To actually construct a name of an inductive type from a string is a little more complicated. I do it in this plugin in the function inductive_of_elim. It looks roughly like this:

let ind_label = Label.of_id (Id.of_string_soft ind_label_string) in

let ind_name = MutInd.make1 (KerName.make modpath dirpath ind_label) in

let body = lookup_mind ind_name env in ...

Where modpath and dirpath make the name fully-qualified.

I'm not sure why you have a string, but if you have a constant somewhere and just want to modify it a bit and then use that string to lookup_mind, your job is a little easier, because you can repr the fully qualified name:

let kn = Constant.canonical c in 

let (modpath, dirpath, label) = KerName.repr kn in ...

Anyways, I suggest looking at names.mli, or whatever the equivalent is in the newest Coq plugin API.