Maude-help mailing list

[Francisco Durán <duran AT lcc.uma.es>]

Hi Keith,

Maude doesn't support parameterized theories, which implies that you cannot 
have parameterized sorts, with unbound parameters, in theories. Full Maude 
neither support parameterized theories.

I'm not sure what you intend in your spec, but if you wanted a theory 
requiring a get function taking some value from a map I'd write it as 

fth EXAMPLE-THEORY{X :: TRIV} is
   including MAP{X, X} .
   op getElt : Map{X, X} -> X$Elt .
endfth

Maude does not support parameterized theories (neither Core Maude nor Full 
Maude). Having a theory parameterized with another theory is semantically 
equivalent to an inclusion, that is, 

fth T1{X :: T2} is
 ...
endfth

is equivalent to 

fth T1 is
  inc T2 .
  ... 
endfth

The problem in your case is what to do with the importation of MAP. (By the 
way, semantically it is different including and protecting a module into a 
theory). I'd express the requirement with a theory as 

fth EXAMPLE-THEORY is
   ---- including MAP{X, X} .
   including TRIV .
   sort Map .
   ---- you should specify here all the reuirements on the Map sort
   op getMapElt : Map -> Elt .
 endfth

You can then use normal theories and parameterized modules to get you you 
intend.

Cheers,

Paco










On 28/01/2014, at 16:53, 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)
> 
> (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 .)
> _______________________________________________
> Maude-help mailing list
> Maude-help AT cs.uiuc.edu
> http://lists.cs.uiuc.edu/mailman/listinfo/maude-help