Maude-help mailing list

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

Hi Min,

You are right. Full Maude cannot handle a user defined operator _=_ : A A -> 
Bool . I have added it to the to do list. I'll try to figure out a way around 
it, but it is really tricky. 

The problem however is not only with the name of the operator. It is also 
that its type is Bool. The following module parses.

(fmod EQ is 
   sorts A B .
   op _=_ : A A -> B [comm] .
   op s_ : A -> A .

   vars A1 A2 : A .
   eq (s A1 = s A2).B = (A1 = A2) .
endfm)

You may not want to ask your users to write an operator different from =, but 
you could use a sort different from Bool in your spec.

Cheers,

Francisco


El 06/04/2011, a las 18:25, zhangmin escribió:

> Hi, all:
> 
> I have  a functional module which cannot be parsed by Full Maude, but
> can be admitted by Core Maude.  The problem is probably caused by the
> symbol "=". Here is a toy example:
> 
> (fmod EQ is 
>    sort A .
>    op _=_ : A A -> Bool [comm] .
>    op s_ : A -> A .
> 
>    vars A1 A2 : A .
>    eq (s A1 = s A2) = (A1 = A2) .
> endfm)
> 
> I have the following feedback from Full Maude after feeding the above
> module into Full Maude. 
> 
> Warning: Ambiguous parsing for ((s A1 = s A2))=((A1 = A2))
> Error: no parse for eq(s A1 = s A2) ~ (A1 = A2)
> 
> 
> If I choose other symbol like "~" instead of "=" to define the equation
> relation on A, the module can be successfully parsed by Full Maude. 
> 
> Are there some other better alternatives to avoid this issue, because we
> may not want to ask users not to choose the symbol "=" to define their
> own equation relations?
> 
> Best regards, 
> Zhang Min
> 
> 
> 
> _______________________________________________
> Maude-help mailing list
> Maude-help AT cs.uiuc.edu
> http://lists.cs.uiuc.edu/mailman/listinfo/maude-help