The Coq mailing list

[Talia Ringer <tringer AT cs.washington.edu>]

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.