Stream: MetaCoq

Topic: Access the defined constant of tmMkInductive

Pedro Abreu (Jul 01 2022 at 13:11):

I notice that tmLemma tmDefinition, and tmAxiomRed all returns the defined constant which makes it easier to manipulate the generated term, however the same is not true to tmMkInductive. What's the reason for this? And is there an easy way to retrieve it?

I've been banging my head against this issue for a while now and the only solution I could find for now is to break the program in two runs and provide the defined constant on the second one, which is annoying.

Kenji Maillard (Jul 01 2022 at 13:59):

I guess tmMkInductive introduce multiple new constants (for the type, its constructors, and possibly also the generated eliminators) and not a single one. Couldn't you tmUnquote what you need just after making the inductive ?

Pedro Abreu (Jul 01 2022 at 14:58):

That's what I was doing, but then I need to manipulate terms of that type later in the monad and I can't destruct them, would you have a suggestion how to deal with that?

Pedro Abreu (Jul 01 2022 at 14:59):

I think I would have the same issue with tmDefinition and alike though, I can't run the function that was just defined, can I?

Pedro Abreu (Jul 01 2022 at 16:34):

I think I'm having difficulty to find what exactly should I tmUnquote in this case. For example, assume we have

MetaCoq Run (
          t <- tmLocate1 "bool";;
          tbool <- match t with
                 | IndRef ind => ...?
                 | _ => tmFail "not IndRef"
                 end
).

What should I unquote here to have the type constructor bool at hand?

Pedro Abreu (Jul 01 2022 at 16:46):

I tried to QuoteConstant the inductive_mind but I get an error

MetaCoq Run (
          t <- tmLocate1 "bool";;
          mind <- match t with
                 | IndRef {| inductive_mind := mind |} =>
                     tmReturn mind
                 | _ => tmFail "not Const"
                 end ;;


      t <- tmQuoteConstant mind false).

Error: Anomaly "File "clib/int.ml", line 46, characters 14-20: Assertion failed."
Please report at http://coq.inria.fr/bugs/.

And if I do QuoteInductive I don't seem to find what exactly should I get from the mutual_inductive_body. Sorry if I'm missing something obvious.

Matthieu Sozeau (Jul 06 2022 at 09:37):

Your "t" is already the global reference corrsponding to bool, and mind its representation. You can then either use mib <- tmQuoteInductive mind which gives you the mutual inductive declaration, and then nth_error (mib.(ind_bodies)) 0 will be the first (and only) inductive declaration, or just use tInd mind [] to refer to bool in a term.

Matthieu Sozeau (Jul 06 2022 at 09:37):

Also, tConstruct mind 0 [] will refer to the first bool constructor

Last updated: Aug 11 2022 at 02:03 UTC