The Coq mailing list

[Kenneth Roe <kendroe AT hotmail.com>]

Things seem to be getting closer.  Here is the code that I currently have:

    let rec sl h r = match r with

                     | [x] -> (h,x)

                     | [] -> (h,"")

                     | (f::r) -> sl (List.append h [f]) r

                     in

    let (path,name) = sl [] (String.split_on_char '.' root) in

    let dirpath = DirPath.make (List.map Id.of_string path) in

    let modpath = ModPath.MPfile dirpath in

    let (evm, env) = Lemmas.get_current_context() in

    let d = Environ.lookup_mind (MutInd.make2 modpath (Names.Label.make name)) env in

Given that "root" has the string "C_Top.x", I am trying to find the definition.  This code does not seem to work.  What do I need to change to make the code work?

Note that I have two separate questions on the mailing list.  The first is to find a definition given a string with a path.  The second question (which is separate) is how to traverse the environment.

                      - Ken

---

From: Talia Ringer <tringer AT cs.washington.edu>
Sent: Friday, November 17, 2017 11:33 AM
To: Kenneth Roe
Cc: Coq-Club
Subject: Re: [Coq-Club] Looking up definitions from inside an ml plugin

 

Again, my high-level advice is not to get a string there if possible. Do you absolutely need that to be a string? If it's tactic input, it can refer directly to the term, and then you do not need a string.

If you must use a string (which can happen), you should look at the interfaces in names.mli. You probably want something like:

let modpath = ModPath.MPfile dirpath in

lookup_mind (MutInd.make2 modpath label) env

And to get a dirpath, you can use DirPath.make. For example, to make Coq.Init.Logic from a list of strings:

DirPath.make (List.map Id.of_string ["Logic"; "Init"; "Coq"])

But what is confusing to me is why you have a non-hardcoded (presumably user-provided) string with none of this information. If the user were providing you a constant instead, then you would be able to recover its modpath, dirpath, and label using repr. I've only ever had to construct a DirPath to refer to a specific hard-coded term in the Coq code, like the identity function.

It would probably help to see your code, but if you really need a string then you're going to want to at the interfaces for ModPath, DirPath, Label, MutInd and so on.

On Fri, Nov 17, 2017 at 5:49 AM, Kenneth Roe <kendroe AT hotmail.com> wrote:

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.