Enzo Crance (Feb 24 2023 at 15:33): Enzo Crance (Feb 24 2023 at 15:33):Hello. With the two following definitions for a predicate f, why does the query f X fail on the first one and succeed on the second one?
f (uvar as X) :- X = 2.
f X :- var X, X = 2.
Until today I've used the uvar as X pattern everywhere to do something different when given a variable, but for some reason, if I'm directly filling X in the body, it fails.
Enrico Tassi (Feb 24 2023 at 17:07):the uvar keyword should only be used in arguments in input mode. The type checker should error otherwise, but it is not implemented.
Enzo Crance (Feb 27 2023 at 16:20):Out of curiosity, why are both uvar and var used in this code?
https://github.com/LPCIC/coq-elpi/blob/efcf63c433834592beb221c09a5e76f9a847128a/elpi/coq-lib.elpi#L126
Enrico Tassi (Feb 27 2023 at 21:03):Eh eh, that is nasty. There is no clear separation between the code which can be invoked in CHR (at the meta level) and code which can be invoked in the regular level. At the meta level uvar is like a regular term constructor, while at normal level it is a keyword. At the regular level X is a variable, so var seems redundant, but that rule could also apply at the meta level, where X is rigid.
The last two rules of copy are, respectively, for the regular level and for the meta level.
A nice way to make it clear would be something like prefixing the latter by an attribute, eg :CHR ..., but nothing like that exists. Hence the var thing :-/
Last updated: Oct 13 2024 at 01:02 UTC