“use” and “include” were clear in the absence of overloading. They are not any more. In the current implementation they are equivalent.
The current rules:
Subsort declarations must involve at least one sort that is not imported in restricted mode.
The signatures of an operator imported in restricted mode may only be supplemented by signatures that differ in at least one domain kind.
No rules may be added that match operator signatures imported in restricted mode.
This causes lots of special cases. Perhaps it should not be exposed (reserved for builtin modules) and handled with less generality and less checking.
In Maude, left and right hand side must be of the same kind. In OBJ3, the right-hand side must be of lower sort. This is the currently implemented behavior.
fmod ABCD is sorts A B C D . subsort A C < B . subsort C < D . op a : -> A . op b : -> B . op c : -> C . op d : -> D . op foo : A -> A . eq a = b . eq b = c . eq c = d . endfm
reduce in ABCD : foo(a) . rewrites: 3 result [D,B]: foo(d)
- currently ‘quote’, ‘unquote’, and ‘unquote-splicing’ cannot be used as identifiers because of the Lisp-liks syntax for quoted symbols and unquotes
In non-strict mode, extraneous variable declarations should be allowed.