Maude-help mailing list

[Steven Eker <eker AT csl.sri.com>]

Core Maude does not support parametrized theories at all. However I see 
you are using Full Maude, which does. I suspect the problem is that you 
are using a parameter X that is not declared in fth EXAMPLE-THEORY - but 
Paco is the expert on the intricacies of Full Maude.

Steven

On 1/28/14 7:53 AM, Keith Ó Dúlaigh wrote:
> 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)
>
> ( 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 .)
> _______________________________________________
> Maude-help mailing list
> Maude-help AT cs.uiuc.edu
> http://lists.cs.uiuc.edu/mailman/listinfo/maude-help