Maude-help mailing list

[mp463634 AT mail.inf.tu-dresden.de]

Hello,

I am playing around with FullMaude 2.1 and parameterized modules, thinking
of the very simple graph theory with a module for finite paths over a
graph

think of the very simple example code
**********************
(fth graph is
        sorts N E .
        ops s t : E -> N .
endfth)

(fmod path(G :: graph) is
        sort P(G) .
        subsort 
G@E
 < P(G) .
        op _;_ : P(G) P(G) ~> P(G) [assoc] .

        ops s t : P(G) -> 
G@N
 .
        cmb g:P`(G`) ; h:P`(G`) : P(G) if t(g:P`(G`)) = s(h:P`(G`)) .

        var g h : P(G) .

        ceq s(g ; h) = s(g) if t(g) = s(h) .
        ceq t(g ; h) = t(h) if t(g) = s(h) .
endfm)
**************************

it can directly be executed

while
        cmb g:P`(G`) ; h:P`(G`) : P(G) if t(g:P`(G`)) = s(h:P`(G`)) .
may be cumbersome, it can be done, however
        ceq s(g ; h) = s(g) if t(g) = s(h) .
cannot stand, it should and in some cases has to be replaced by
        ceq s(g ; h) = s(g) if (g ; h) : P(G) .
or anything like this, however i seem unable to get a correct syntax for
this... usually the error goes like: could not find sort "P`(G`)"
but instantiating P(G) to P`(G`) gives parse errors

matching equations like
        ceq s(f) = s(g) if g ; h := f .
work but are not always applicable

looking for help, martin


*****************************************
for testing:

(fmod nc is
        including graph .

        ops A B : -> N .
        ops z y : -> E .

        eq s(z) = A .
        eq t(z) = B .
        eq s(y) = B .
        eq t(y) = B .
endfm)

(view gnc from graph to nc is
         sort N to N .
         sort E to E .
endv)