Quentin VERMANDE (Nov 17 2023 at 14:00): Quentin VERMANDE (Nov 17 2023 at 14:00):Hello. I would like to check if a term uses constants that are not declared in the context. I tried to typecheck the term, hoping to get a failure if it does, but the try ... with block in coq_elpi_builtins.ml does not catch the exception. Is it possible to do that, or even only check if a given global constant is declared?
Enzo Crance (Nov 17 2023 at 14:34):The coq.typecheck predicate has a diagnostic as its last argument, meaning that you can call it strictly by providing ok (and it will yield an Elpi error if the term is ill typed), or in a more permissive way by putting a variable at this position. If the term is ill typed you get the variable filled with the error message. In that way you can pattern-match on the variable and if it is error _ then the term is ill typed but Elpi does not crash and you can do your own failure handler
Quentin VERMANDE (Nov 17 2023 at 14:40):Thank you. I had tried with error S instead of a variable to pattern-match on, I guess this should not make a difference with your proposal. Actually, I tried changing the catchall branch of the error handler in coq_elpi_builtins.ml into a failwith and did not get an anomaly, so I guess the exception that Coq raises is never catched by the code in coq-elpi.
Enrico Tassi (Nov 17 2023 at 19:13):How can a constant not be declared? What are you doing exactly?
Quentin VERMANDE (Nov 18 2023 at 11:09):I have a term that is defined using section variables. After the section is closed, the term now refers to constants that do not exist anymore.
Enrico Tassi (Nov 19 2023 at 09:00):In that case you can use the API to get the list of section variables and lambda abstract hem. There is code for it in HB.
Enrico Tassi (Nov 19 2023 at 09:01):Closing a section an still mentioning it's variable is going to result inanomalies
Last updated: Oct 13 2024 at 01:02 UTC