eval term in setof

[ko56]

I don't know if this is related to #102, but the following doesn't work as I expect:

(in-package :shop-user)

(defdomain tst
  (
    (:op (!mkalist)
      :precond
      (and
    (setof (eval (cons ?x ?y)) (and (oper ?x) (area ?y)) ?al)
    )
      :add ((op-area-spec ?al))
      )
    )
  )

(defproblem check tst
  (
    (area north) (area south)  (area east)  (area west)
    (oper opA)  (oper opB)  (oper opC)
    )
    ((!mkalist))
  )

(shop-trace :operators :states)
(find-plans 'check)

[rpgoldman]

The problem with the above is that the first argument to setof is not a goal, it's a term, so it won't be proven.

To be honest, this makes me wonder why the manual has "call terms" and "eval terms". We have call and eval expressions, and that makes sense, because they can appear where any other goal appears and the theorem prover will invoke lisp to evaluate them. But it is not possible to just sprinkle call and eval around and expect them to be evaluated.

I should look into the history here (if it extends far enough) and see where those came from. Probably this whole syntax discussion needs to be revisited and made more accurate.

While we ponder this, the following is a way to do what you want:

(defdomain tst
  (
    (:op (!mkalist)
      :precond
      (and
    (setof ?z (and (oper ?x) (area ?y) (assign ?z (cons '?x '?y))) ?al)
    )
      :add ((op-area-spec ?al))
      )
    )
  )

The following will also work:

(defdomain tst
  (
    (:op (!mkalist)
      :precond
      (and
    (setof (?x . ?y) (and (oper ?x) (area ?y)) ?al)
    )
      :add ((op-area-spec ?al))
      )
    )
  )

[ko56]

Thanks for the answer. As a side effect, it raised some questions in the code I'm writing...

Coming to the issue of terms, I think at the beginning of sec. 4.3 you need variables, constants, numbers, lists, and something that says that a term can be formed by applying a function to a number of other terms. Using the present terminology, that would be a "call" term. Unless you want to do away with function application altogether, but that would be too severe, since the simplest logical expression (atomic formula) is an application of an n-ary predicate to n terms. About eval terms, I'm not sure.

If we admit the above, the issue is, as you say, that you can't use non-simple terms at will. Therefore, are there any other problematic places thansetof/bagof? Given your answer to my question about setof, I see that allowing general terms in the first argument of setof/bagof is not as needed as I thought. (I don't know about the note in sec. 4.5.10 saying that general terms were admitted in SHOP 3.4.)

On the other hand, saying that the 1st argument to setof is a term, even a general term, doesn't seem to agree with the example (setof (pair ?u1 ?u2) ...) in 4.5.10: the argument there is an atomic formula.

Finally, w.r.t. the manual, I've made some more improvements in the text (I think), and some more typesetting fixes. See the end of

76, revised today.