Added the ability to reflect Inductive definitions

[aa755]

This is implemented as the command Make Inductive. See demo.v for a demo.

[gmalecha]

Thanks for the PR. This is a great feature to have.

Is there a reason that you chose not to use the existing quoting of inductive types? In particular (https://github.com/gmalecha/template-coq/blob/master/theories/Ast.v#L63) Does it not contain enough information? My worry with exposing such low level types is two fold:

1. They don't fit naturally into the mental model that users have (maybe that is the wrong mental model?)
2. They are difficult (verbose?) to program with.

[aa755]

That information is not sufficient, as pointed out by Jason: https://github.com/gmalecha/template-coq/issues/17

All the fields in Ast.mutual_inductive_entry and Ast.one_inductive_entry (except maybe mind_entry_private) seem semantically relevant to me.

[gmalecha]

I don't doubt that they are semantically relevant, it just seems like it is a representation that is not natural to Coq users.

To address the problem that @JasonGross pointed out, would it be sufficient to add a type to the inductive as a whole? Something like:

| PType : ident -> term (* the type *)-> list (ident * inductive_body) -> program -> program

My worry is that everyone that uses this library is going to have to reverse engineer what this type does. A better solution (if it can be made to work) would be to have something that maps more directly to how Coq users write inductive types.

[aa755]

I did have some difficulty in figuring out the de-bruijn indices for the types of constructors. I may sometime write in Gallina a high-level wrapper to compute the argument to Make Inductive, perhaps from something that is named (instead of de-bruijn) and looks close to how Coq users write inductives. However, I would prefer to keep the OCaml part (in reify.ml4) as simple as possible.

Your suggested representation still loses information that is relevant to me (parameters vs indices, flags for template/universe polymorphism).

[JasonGross]

I believe mind_entry_private is about whether or not it's okay to pattern match on the inductive outside the module it's defined in; this is to allow Licata's HIT trick.

[gmalecha]

I think then env + term representation would be a good route to go here. At minimum this would mean pulling the constructors of program out and make them the environment values.

@mattam82 I got confused about the last comment in your comment. Do you think that we should convert these new definitions to something like PType in Gallina, or in the plugin?

[mattam82]

@gmalecha in Gallina, as part of the plugin's v files we could have an env + term -> program function to get back the closed representation.

[mattam82]

Yes

On Fri, Dec 2, 2016 at 5:14 PM Abhishek Anand notifications@github.com wrote:

@aa755 commented on this pull request.

In theories/Ast.v https://github.com/gmalecha/template-coq/pull/32:

@@ -63,3 +63,34 @@ Inductive program : Set := list (ident inductive_body) -> program -> program | PAxiom : ident -> term ( the type ) -> program -> program | PIn : term -> program. + + +( representation of mutual inductives. copied, more or less, from Coq/kernel/entries.mli +*) + +Record one_inductive_entry : Set := {

• mind_entry_typename : ident;
• mind_entry_arity : term;
• mind_entry_template : bool; ( template polymorphism ? )
• mind_entry_consnames : list ident;
• mind_entry_lc : list term}.

• +Definition local_entry : Set := term. +(*

Does LocalDef stand for local let bindings?

— You are receiving this because you were mentioned.

Reply to this email directly, view it on GitHub https://github.com/gmalecha/template-coq/pull/32, or mute the thread https://github.com/notifications/unsubscribe-auth/AAGARSu5ImchGCkEzBJIq0dfim9Ls2OCks5rEEPkgaJpZM4LCCXt .

[gmalecha]

@aa755 Why don't we export the entire type for this PR, and then open a second issue and PR to add the environment representation that @mattam82 suggested. That will let us merge this relatively quickly and it won't break anything for users.

[gmalecha]

Merging!