Maude-help mailing list

[Ich bin es <br_marty AT yahoo.com>]

let me put forward another question with a probably
obvious answer, but i simply cannot figure it out

the object of interest is again the standard graph
example (i seem not to get the grasp of how to use
maude i guess) this time it is loaded and introduced,
i simply cannot execute a single reduce, it always
nags:

>Advisory: bad operator declaration eSortToSort(....

and

>Error: Incorrect command.

now i thought it was the subsort overloading issue,
with regard to parameterization (which is supposed to
be disallowed in maude, :( ) but after disambiguating
the names and making the overloading explicit via
axioms, the problem remains and i cannot figure out
just  (not sure if this is necessary, the manual says
so, the examples suggest otherwise) what exactly is
incorrect

the example in question, this time in all detail:

(fth GRAPH is
        sorts Edge Node .
        ops src tar : Edge -> Node .
 endfth)

(fmod GRAPH1 is
        sorts Node Edge .
        ops s t : Edge -> Node .

    ops a b c d : ->  Node .
    ops aa ab bc bd ca : ->  Edge .

    eq s(aa) = a .
    eq t(aa) = a .
    eq s(ab) = a .
    eq t(ab) = b .
    eq s(bc) = b .
    eq t(bc) = c .
    eq s(bd) = b .
    eq t(bd) = d .
    eq s(ca) = c .
    eq t(ca) = a .
 endfm)

(view Gview from GRAPH to GRAPH1 is
    sort Edge to Edge .
    sort Node to Node .
    op src to s .
    op tar to t .
 endv)

(fmod PATH(G :: GRAPH) is
        sort Path(G) .
        subsorts 
G@Edge
 < Path(G) .

        ops s t : Path(G) -> 
G@Node
 .
        op _;_ : [Path(G)] [Path(G)] -> [Path(G)] [assoc] .

        var E : 
G@Edge
 .
        var N : 
G@Node
 .
        vars P Q : Path(G) .

        eq s(E) = src(E) .
        eq t(E) = tar(E) .
        ceq s(E ; P) = s(E) if t(E) == s(P) .
        ceq t(P ; E) = t(E) if t(P) == s(E) .

        cmb E ; P : Path(G) if t(E) == s(P) .

 endfm)

(fmod Pmod is
    protecting PATH(Gview) .
 endfm)


with this one should be able to reduce things like:

(red ab .)
(red s(ab ; bc) .)

or whatever would be a correct reduce, the thing is it
never gets through to the module itself

________________________________________________________________________
Download Yahoo! Messenger now for a chance to win Live At Knebworth DVDs
http://www.yahoo.co.uk/robbiewilliams