Stream: Coq devs & plugin devs

Topic: Working out the type of bindings introduced by a case

Kiran Gopinathan (Oct 19 2022 at 03:12):

Hi, For various reasons, I'm working on some code that traverses Coq's Constr.t type.

I'd like to work out the type of arguments introduced by the bindings in each case of the Case constructor of the Constr.t type.

For example:

match Constr.kind c with
  ...
  | Constr.Case (info, _univ, _ty, _ret, _inv, _vl, cases) ->
    ...

By iterating through the cases binding above, I can obtain the subterms within a given proof term by looking at the second component of each element in cases. The first component seems to tell me the variables that are bound by case, but don't include the types of these variables.

Could someone point me to any of the Coq API's I could use to retrieve this information?

Kiran Gopinathan (Oct 19 2022 at 03:32):

Okay, after digging around, I figure the right direction to go is something like:

    let mind = Environ.lookup_mind (fst info.ci_ind) coq_env in
    (* do something with mind.mind_packets *)

Is this the correct approach, or is there something simpler?

Pierre-Marie Pédrot (Oct 19 2022 at 08:53):

For EConstr, there is a function EConstr.annotate_case that does this. Otherwise you can either do it by hand using the same kind of code, or destruct the branches generated by Constr.expand_case with number of declarations given by the names.

Kiran Gopinathan (Oct 19 2022 at 12:46):

Ah, nice! Constr.expand_case looks like exactly what I need. Thanks for the help!

Last updated: Dec 01 2023 at 06:01 UTC