search

HOL-Theorem-Prover / HOL

Canonical sources for HOL4 theorem-proving system. Branch develop is where “mainline development” occurs; when develop passes our regression tests, master is merged forward to catch up.
https://hol-theorem-prover.org
Other
626 stars 143 forks source link

Define does not allow wildcards on right hand side #241

Closed thtuerk closed 9 years ago

thtuerk commented 9 years ago

There is support for handling wildcards on the left-hand-side of definitions. They are replaced with proper variable names. However, this functionality also checks that there are no underscores on the right hand side. If there are, the definition is not accepted and we get an appropriate error message. The problem is that these checks happen on quotations, not terms. This means that the term-postprocessing hooks which might remove underscores had no chance to run, yet. To get tools like Define working with case-expressions there is special code that ignores wildcards in case-magic expresssions. However, if one uses other terms on the right that contain wildcards which turn into bound variables by term-postprocessing, this feature causes trouble. For this reason, I can't use my own PMATCH-based case-expressions with wildcards in new function definitions (see example deep_matches).

The relevant check is in src/tfl/src/Defn.sml line 1585. I propose just deleting this check. This would solve my problem and only result in worse error messages otherwise. Wildcards on the right-hand side which are not removed by term post-processing are catched via the free variable checks. However we would get worse error messages. Instead of getting wildcards on rhs we get The following variables are free in the right hand side of the proposed definition: "_0".

Is it OK, if I delete this check? Do I miss something?

mn200 commented 9 years ago

I think I noticed this previously, and thought it odd. I'd be quite happy for you to change the behaviour.

thtuerk commented 9 years ago

Thanks. I changed it in commit b01102b.

konrad-slind commented 9 years ago

Seems OK to me. --Konrad.

On Sat, Mar 7, 2015 at 5:41 PM, Michael Norrish notifications@github.com wrote:

I think I noticed this previously, and thought it odd. I'd be quite happy for you to change the behaviour.

— Reply to this email directly or view it on GitHub https://github.com/HOL-Theorem-Prover/HOL/issues/241#issuecomment-77718259 .