Maude-help mailing list

[Marc Boyer <Marc.Boyer AT onera.fr>]

Sorry for the previous mail. In fact, it works. Here is the code.
The solution was not renaming, but subsorting: we need to declare
   List{Nat} < List{Arg}
*and*
   NeList{Nat} < NeList{Arg}

And a little bit of syntax (NeList{Arg}{F}) to be able to have two
instances in the same module.

**********************************************************************
***  Map, fold : applying function on all terms

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}{F},
     sort NeList{FUNCTION-ARG}{F} to NeList{Arg}{F} ) .
  protecting LIST{FUNCTION-DOM}{F}
    * ( sort List{FUNCTION-DOM}{F}   to List{Dom}{F} ,
        sort NeList{FUNCTION-DOM}{F} to NeList{Dom}{F} ) .

  op map( _ , _ ): List{Arg}{F} F$Param -> List{Dom}{F} .
  **** Note: there is no overloading
  ***    NeList{Arg} -> NeList{Dom}
  *** since the function f can produce nil on some value

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

endfm

**********************************************************************
*** Basic illustrative use and test of the MAP module
**********************************************************************


****************************************
***  Just map an increment function

view INC 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{INC} .
  subsort List{Nat} < List{Arg}{INC} .
  subsort NeList{Nat} < NeList{Arg}{INC} .
  subsort List{Nat} < List{Dom}{INC} .
  subsort NeList{Nat} < NeList{Dom}{INC} .

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

red map( l , 10 ) .
red map( a , 10 ) .

****************************************
***  Map in the same module INC and POW

view POW 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-and-POW is
  protecting LIST{Nat} .
  protecting MAP{INC} * ( op map( _ , _) to map-inc ) .
  protecting MAP{POW} * ( op map( _ , _) to map-pow ) .
  subsorts List{Nat} < List{Arg}{INC} List{Dom}{INC} List{Arg}{POW} 
List{Dom}{POW} .
  subsorts NeList{Nat} < NeList{Arg}{INC} NeList{Dom}{INC} 
NeList{Arg}{POW} NeList{Dom}{POW} .

  op l : -> List{Nat} .
  eq l = 3 4 2 8 6 9 3 2 .

endfm

red map-inc( l , 2 ) .
red map-pow( l , 2 ) .
red map-inc( map-pow( l , 2 ) , 3 ) .

Marc Boyer
--
Marc Boyer, Ingenieur de recherche                              ONERA
Tel: (33)  5.62.25.26.36                                         DTIM
Fax: (33)  5.62.25.26.52                          2, av Edouard Belin
http://www.onera.fr/staff/marc-boyer/          31055 TOULOUSE Cedex 4