Maude-help mailing list

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

You forgot to include NAT. Several other points:

(1) This is legal CoreMaude, which has more informative error reporting.
(2) The singleton case is unneeded since it is covered by the general 
case, with M taking empty.
(3) The owise case is also unnecessary.
(4) You can use the sort Entry{Z, P} to capture whole map entries.

So I would write your example as:

fmod MAP-UTILS {Z :: TRIV , P :: TRIV } is
   inc MAP{Z, P} .
   inc NAT .

   op length : Map {Z, P} -> Nat .
   var M : Map{Z, P} .
   var E : Entry{Z, P} .

   eq length(empty) = 0 .
   eq length((E, M)) = s(length(M)) .
endfm

fmod TEST is
  inc MAP-UTILS{String, String} .
endfm

red length(
  insert("second", "b", insert("first", "a", empty))
) .

Steven

On 1/9/14 7:52 AM, Keith Ó Dúlaigh wrote:
> Hi,
>
> I'm trying to include a parameterised module within a parameterised 
> module like this:
>
> (fmod MAP-UTILS { Z :: TRIV , P :: TRIV } is
>    inc MAP{Z, P} .
>
>    var M : Map{Z, P} .
>    var I : Z$Elt .
>    var J : P$Elt .
>
>    op length : Map {Z, P} -> Nat .
>    eq length(empty) = 0 .
>    eq length((I |-> J)) = 1 .
>    eq length((I |-> J, M)) = s(length(M)) .
>    eq length(M) = 0 [owise] .
> endfm)
>
> which gives this error message in Maude 2.6 with Full Maude 2.5b:
>
> Warning:(length(empty))=(0)
> Error: no parse for eq length(empty) ~ 0
> Warning:(length(empty))=(0)
> Error: no parse for eq length(empty) ~ 0
> Introduced module MAP-UTILS
>
> Any comments on what is wrong with this would be appreciated.
>
> Thanks,
> Keith
> _______________________________________________
> Maude-help mailing list
> Maude-help AT cs.uiuc.edu
> http://lists.cs.uiuc.edu/mailman/listinfo/maude-help