CALM bug? - instance literal in instantiation statement

[zhangyuanlin]

CALM doesn't complain about instance(X) (last line in the program below).
Sort seems to be missing from the literal (intended: instance(X, names)).

Program:

system description simple_french_toast
    theory french_toast
        module cooking_toast
            sort declarations
                things :: universe
                sides :: things
                % NEW a good example for using Herbrand function
                % to represent two sides of a toast.
                toasts :: things
                  attributes
                    side1: sides
                    side2: sides
                %   We need some auxiliary sort for an easy definition of sides of toasts
                names :: universe

structure toastbread
    instances
        t1, t2, t3 in names
        % define the sort toasts
        s1(X), s2(X) in sides where instance(X) 

[Topology]

I will fix this soon. It is clearly a bug. There will not be a syntax error. I will have to catch it as a semantic error.

Questions about how to handle this scenario:

1. Is the user allowed to use the name 'instance' for a user defined function if the signature is different than the special function instance: universe * nodes -> booleans
2. Should this be an undefined function error, or a misuse of the special function error?

[zhangyuanlin]

1. Is the user allowed to use the name 'instance' for a user defined function if the signature is different than the special function instance: universe * nodes -> booleans

CALM does not allow "overload" a function name, right? If so, I think we won't allow programmer to use instance as a function name.

2. Should this be an undefined function error, or a misuse of the special function error?

The latter. Points 1 and 2 should apply to other special functions too.

[Topology]

The fix for this will be in the next calm.jar release. This particular issue is now fixed in code.