Maude-help mailing list

[minzhang <zhmtechie AT gmail.com>]

Hi, Marc:

It is really interesting to formalize the map in calm with Maude. If I
understood you correctly, the following modification of your code should
work.

In the functional module MAP{ F :: FUNCTION }, change Param to F$Param,
like:

fmod MAP{ F :: FUNCTION } is
   protecting LIST{FUNCTION-ARG}{F} *
              ( sort List{FUNCTION-ARG}{F} to List{Arg} ) .
   protecting LIST{FUNCTION-DOM}{F} *
              ( sort List{FUNCTION-DOM}{F} to List{Dom} ) .

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

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

red map( l , p:Param ) . ==> red map( l , N:Nat ) .

p:Param cannot be parsed since Param is declared in the theory, it has
been mapped into Nat in the module TEST-MAP-INC. You should use Nat here
instead. 

In the module TEST-MAP-INC, I don't think the following statements
  protecting LIST{Nat} .
  subsort List{Nat} < List{Arg} 
 
are necessary since actually List{Nat} and List{Arg} are the same. 

By the way, you may get some advisories that some operators are imported
with no common ancestor, since both of the sorts Arg and Dom are mapped
to Nat. Consequently, both of the sorts List{FUNCTION-ARG}{ADD} and
List{FUNCTION-DOM}{ADD} represent list of natural numbers. 

I'm not sure how to avoid these advisories. However, they can be
neglected. Some Maude experts may know how to solve this problem.

You may try mapping another operation like >:

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

You will find these advisories are gone. 

Well, it is my understanding of your problem. If there are some
different opinions, I would be glad to know. 

Best regards!

Min Zhang

from JAIST


On Fri, 2010-01-22 at 16:57 +0100, Marc Boyer wrote:
> Dear All,
> 
> I am still working with parametrized modules. I am trying to make
> some map (like the calm list map, but with a third parameter).
> 
> **********************************************************************
> ***  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} ) .
>    protecting LIST{FUNCTION-DOM}{F} *
>               ( sort List{FUNCTION-DOM}{F} to List{Dom} ) .
> 
>    op map( _ , _ ): List{Arg} Param -> List{Dom} .
> 
>    var arg   : F$Arg .
>    var p : Param .
>    var l-arg :  List{Arg} .
>    eq map( nil , p ) = nil .
>    eq map(arg l-arg , p ) = f( arg , p ) map( l-arg , p ) .
> endfm
> 
> 
> **********************************************************************
> *** Here come instantiation
> 
> 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{Nat} .
>    eq l = 3 4 2 8 6 9 3 2 .
>    op a : -> List{Arg} .
> endfm
> 
> **** Add here is the problem: is can parse the first statement,
> *** but none of the two others.
> 
> red map( l , p:Param ) .
> red map( l , 10 ) .
> red map( a , 10 ) .
> 
> *** End of code
> 
> Any idea ?
> 
> Regards,
>    Marc Boyer


-- 
Best regards!

Min Zhang