Maude-help mailing list

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

I think that it is just that your list should be of sort List{NAT-COND-LTH}.

Francisco

fmod TEST-FILTER is

----  protecting LIST{Nat} .

  protecting FILTER{NAT-COND-LTH} .

  **** Here is my question: why did I need this line ? I have looked at

  **** the definition of  WEAKLY-SORTABLE-LIST{X :: STRICT-WEAK-ORDER}

  **** in the prelude.maude file, I no such subsort declaration is

  **** needed. What did I miss ?

----  subsort List{Nat} <  List{NAT-COND-LTH} .

----  op l : -> List{Nat} .

  op l : -> List{NAT-COND-LTH} .

  eq l = 3 4 2 8 6 9 3 2 .

endfm

El 18/01/2010, a las 16:02, Marc Boyer escribió:

ear all,

I am trying to implement some parametrized programming. As simple
example, I try to build a module that filter a list given some
condition. The example is to remove all elements of a list
of Nat <= a given bound.

My question is in the middle of the code. I have put english
remarks in Maude comments to allow to cut/paste and run it.

**** I need some "generic condition".

fth COND is
  including TRIV .
  protecting BOOL .
  sort CmpParam .
  op select( _ , _ ) : Elt CmpParam -> Bool .
endfth

**** I then can write my Filtering generic module.

*** This view allow toi have a LIST of X :: COND
view COND from TRIV to COND is endv

**** Main module
fmod FILTER{ X :: COND } is
  protecting LIST{COND}{X} *
            ( sort List{COND}{X} to List{X},
              sort NeList{COND}{X} to NeList{X}
        ).
  op filter( _ , _ ) : List{X} X$CmpParam -> List{X} .

  var x : X$Elt .
  var cmp : X$CmpParam .
  var l : List{X} .
  eq filter( nil , cmp ) = nil .
  eq filter( x l , cmp) =
    if ( select( x , cmp) ) then
       x filter( l , cmp )
    else
       filter( l , cmp )
    fi .
endfm


**** Then, I have to instanciate it

view NAT-COND-LTH from COND to NAT is
  sort Elt to Nat .
  sort CmpParam to Nat .
  op select( X:Elt , Y:CmpParam ) to term ( X:Nat < Y:Nat )  .
endv

fmod TEST-FILTER is
  protecting LIST{Nat} .
  protecting FILTER{NAT-COND-LTH} .
  **** Here is my question: why did I need this line ? I have looked at
  **** the definition of  WEAKLY-SORTABLE-LIST{X :: STRICT-WEAK-ORDER}
  **** in the prelude.maude file, I no such subsort declaration is
  **** needed. What did I miss ?
  subsort List{Nat} <  List{NAT-COND-LTH} .

  op l : -> List{Nat} .
  eq l = 3 4 2 8 6 9 3 2 .
endfm
red filter( l , 3 ) .

--
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
_______________________________________________
Maude-help mailing list
Maude-help AT cs.uiuc.edu
http://lists.cs.uiuc.edu/mailman/listinfo/maude-help