Maude-help mailing list

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

Dear Marc and Min,

I agree on Min's comments.

You don't have to worry about the advisories, they are just harmless.  
You can ask Maude not to show them if you don't want to see them with  
set show advisories off. Notice that you cannot do this with warnings  
or errors.

But you have to worry about warnings, because sooner or later you may  
get undesired results. And what is worst, you cannot trust what you  
get. Maude assumes preregularity, and the user is responsible to get it.

In this case what is happening is just that you are getting to  
different instantiations of lists that are in the same connected  
component. You can solve the problem by renaming the conflicting  
operators. You can find below the compete specification where the  
LIST{FUNCTION-ARG}{F} modulo gets all the sorts and operators coming  
from LIST renamed (I'm sure you can find a more appropriate  
renaming ;)).

Cheers,

Francisco Duran


**********************************************************************
***  Parametrized MAP

fth FUNCTION is
  sorts Arg Dom Param .
  op f( _ , _ ) : Arg Param -> Dom .
endfth

view FUNCTION-ARG  from TRIV to FUNCTION is
  sort Elt to Arg .
endv

view FUNCTION-DOM  from TRIV to FUNCTION is
  sort Elt to Dom .
endv

fmod MAP{ F :: FUNCTION } is
  protecting LIST{FUNCTION-ARG}{F} *
             ( sort List{FUNCTION-ARG}{F} to List{Arg},
               sort NeList{FUNCTION-ARG}{F} to NeList{Arg},
               op nil to nilA,
               op __ to _`,_,
               op tail to tailA,
               op front to frontA,
               op reverse to reverseA,
               op $reverse to $reverseA,
               op append to appendA,
               op head to headA,
               op last to lastA,
               op occurs to occursA,
               op size to sizeA,
               op $size to $sizeA ) .
  protecting LIST{FUNCTION-DOM}{F} *
             ( sort List{FUNCTION-DOM}{F} to List{Dom},
               sort NeList{FUNCTION-DOM}{F} to NeList{Dom} ) .

  op map( _ , _ ): List{Arg} F$Param -> List{Dom} .

  var arg : F$Arg .
  var p : F$Param .
  var l-arg : List{Arg} .
  eq map( nilA , p ) = nil .
  eq map((arg , l-arg) , p ) = f( arg , p ) map( l-arg , p ) .
endfm

view ADD from FUNCTION to NAT is
  sort Arg to Nat .
  sort Dom to Nat .
  sort Param to Nat .
  op f( A:Arg , P:Param ) to term ( A:Nat + P:Nat ) .
endv

fmod TEST-MAP-INC is
  ----protecting LIST{Nat} .
  protecting MAP{ADD} .
  ----subsort List{Nat} < List{Arg} .

  op l : -> List{Arg} .
  eq l = 3, 4, 2, 8, 6, 9, 3, 2 .
  op a : -> List{Arg} .
endfm

red map( l , p:Nat ) .
red map( l , 10 ) .
red map( a , 10 ) .

view LARGE from FUNCTION to NAT is
  sort Arg to Nat .
  sort Dom to Bool .
  sort Param to Nat .
  op f( A:Arg , P:Param ) to term ( A:Nat > P:Nat ) .
endv

fmod TEST-MAP-INC is
  ----protecting LIST{Nat} .
  protecting MAP{LARGE} .
  ----subsort List{Nat} < List{Arg} .

  op l : -> List{Arg} .
  eq l = 3, 4, 2, 8, 6, 9, 3, 2 .
  op a : -> List{Arg} .
endfm

red map( l , p:Nat ) .
red map( l , 5 ) .
red map( a , 5 ) .