CALM bug? - instantiation using X

[zhangyuanlin]

There is a syntax error complaint for (instantiation starts with X) the following code:

        ...... 
        t1, t2, t3 in names
        % define the sort toasts
        X in toasts where instance(X, names)
          side1 = s1(X)
          side2 = s2(X)
      .... 

However, if I use t(X), i.e., introducing a Herbrand function in the code:

......
        1, 2, 3 in names
        % define the sort toasts
        t(X) in toasts where instance(X,names)
          side1 = s1(t(X))
          side2 = s2(t(X))
......

There is no syntax error BUT I got an exception.

Let the first program be P1 and second P2.

Error message for P1:

Syntax Error: (/Users/yuazhang/Desktop/CALM/examples/simple_frenchtoast-x.p [X (24:8)]) unexpected token {X}, expected one of {<EOF>, 'temporal', 'planning', 'diagnostic'}.

Exception info for P2: (not sure if it is because of oversimplification)

Exception in thread "main" java.lang.IndexOutOfBoundsException: Index: 1, Size: 1
    at java.util.ArrayList.rangeCheck(ArrayList.java:653)
......

The program P1 (I tried to minimize the 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 in toasts
        % s1t1,s2t1 in sides
        % introduce toast names first
        t1, t2, t3 in names
        % define the sort toasts
        X in toasts where instance(X, names)
          side1 = s1(X)
          side2 = s2(X)
        % s1(X), s2(X) in sides for all X in names
        s1(X), s2(X) in sides where instance(X, names)

Program P2:

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 in toasts
        % s1t1,s2t1 in sides
        % introduce toast names first
        1, 2, 3 in names
        % define the sort toasts
        t(X) in toasts where instance(X)
          side1 = s1(t(X))
          side2 = s2(t(X))
        % s1(X), s2(X) in sides for all X in names
        s1(X), s2(X) in sides where instance(X, names)

[Topology]

Issue with P1

X in toasts where instance(X, names)

This effectively makes names a subsort of toasts without declaring it in the sort hierarchy. I can add permission for variables, but this seems like something a record sort, parameterized constant, or functor would better take care of.

Issue with P2

t(X) in toasts where instance(X)

This exception is caused by the lack of argument in the second position of the instance functions.

Issue 2 with P2

When names is added as the second hand argument, the program complains about s1(t(X))) being an undefined function.

This directly plays into the Herbrand term on the right hand side. I will need to work on that. However we need to discuss how complex of a solution. Are we going to require a ground Herbrand term? Our last discussion was to basically turn off all checking and pass it through to SPARC. This gets increasingly complicated with the more nesting we allow in the Herbrand terms.

I am leaning heavily against using recursive definitions with attributes in this way and having a more coherent treatment of "records" or "functors" at the theory level that co-instantiates instances in related sorts. But this fundamental relationship really belongs in the theory.

[zhangyuanlin]

I can add permission for variables, but this seems like something a record sort, parameterized constant, or functor would better take care of.

I don't see a reason to prevent such a use which might not be related to "record" we are discussing. for example, we might have

X in toasts where instance(X, names) PLUS other properties on X 

This directly plays into the Herbrand term on the right hand side. I will need to work on that. However we need to discuss how complex of a solution. Are we going to require a ground Herbrand term?

I move comments on this to the Herbrand term thread #16.

[Topology]

Both P1 and P2 now have answersets with the latest calm.jar. Is this sufficient to close this issue as separate from other herbrand term related issues?

[zhangyuanlin]

sure.