Zero-ary constructed type functions cannot conveniently be used in interpretations

[Broes De Cat]

Please fix soon ;)

[Bart Bogaerts]

Attached another file, with what was probably intended...

[Bart Bogaerts]

Note that this has to do with the differences between simple domain element and compound domain element. If you force the "and" in the interpretation to be a compound domain element, e.g.~by replacing it with and(), it works.

This is undesired as we are allowed to use functions without brackets in theories...

[JoD]

Ben er naar aan het kijken...

[JoD]

Allright, fix should be available in this branch: https://bitbucket.org/krr/idp/src/b6fa259731002fdce899e7da9f24037a48289f7d/?at=constr_bug_fix. Go ahead an test it :)

[Bart Bogaerts]

Does not really work with overloading yet

[JoD]

Also, the following will never work unless the parser knows the exact type of the symbol it is interpreting:

vocabulary V{ type T constr from {A} type S P(S) }

structure S:V{ P={A} }

Bart's solution: always interpret strings in a structure as domain elements, and return a warning message if they could be constructors.

[Broes De Cat]

It seems more logical to do the reverse: always prefer a symbol if it is available (as the user explicitly declared that symbol) otherwise, in a theory, it is a variable (otherwise, they can still quantify it) otherwise, in a structure, it is a string (otherwise, they can still quote it)

[JoD]

No problem, will change it if there is consensus.

[JoD]

Broes fixed this: identifier without brackets in structures are interpreted as symbols if there is such a symbol. Domain elements can be designated by "..."