Maude-help mailing list

[Keith Ó Dúlaigh <keithod AT cs.nuim.ie>]

Hi,

Does Maude support functional theories with a parameterised sort as the 
return type of some operator?

Some toy code that might give an idea of what I'm trying to do is shown 
below. The commented out lines cause errors when uncommented.

Thanks,
Keith



loop init .

(fmod EXTENDED-INT is
    including INT .
    including MAP{Int, Int} .

    op mapElt : -> Map{Int, Int} .
    eq mapElt = (1 |-> 2) .
endfm)

(fth EXAMPLE-THEORY is
    including TRIV .

    op getElt    : -> Elt .
---    op getMapElt : -> Map{X, X} .
endfth)

(view ExampleView from EXAMPLE-THEORY to EXTENDED-INT is
    sort Elt to Int .

    op getElt to 0 .
---    op getMapElt to mapElt .
endv)

(fmod PARAM-MODULE{X :: EXAMPLE-THEORY} is
    op someOp : -> X$Elt .
    eq someOp = getElt .

---   op someOtherOp : -> Map{X, X} .
---   eq someOtherOp = getMapElt .
endfm)

(fmod TEST is
    including PARAM-MODULE{ExampleView} .

    op test1 : -> Int .
    eq test1 = someOp .

---    op test2 : -> Map{Int, Int} .
---    eq test2 = someOtherOp .
endfm)

(reduce test1 .)

---(reduce test2 .)