Maude-help mailing list

[Narsis Amini <narsisa90 AT yahoo.com>]

Dear All,

 

I have the following spec which defines typed lists

but it is not parsed correctly.

I use Maude 2.4 running on a Windows workstation.

 

would you please help me with this problem?

 

  fmod LIST-CONS{X :: TRIV} is
    protecting NAT .
    sorts NeList{X} List{X} .
    subsort NeList{X} < List{X} .

    op [] : -> List{X} [ctor] .
    op _:_ : X$Elt List{X} -> NeList{X} [ctor] .
    op tail : NeList{X} -> List{X} .
    op head : NeList{X} -> X$Elt .
   
    vars E E' : X$Elt .
    var N : Nat .
    vars L L' L'' : List{X} .

    eq tail(E : L) = L .
    eq head(E : L) = E .

    op _ ++ _ : List{X} List{X} -> List{X} .
    op length : List{X} -> Nat .
    op reverse : List{X} -> List{X} .
   
    eq [] ++ L = L .
    eq (E : L) ++ L' = E : (L ++ L') .

    eq length([]) = 0 .
    eq length(E : L) = 1 + length(L) .
    eq reverse([]) = [] .
    eq reverse(E : L) = reverse(L) ++ (E : []) .
   
  endfm

fmod MYCONF is
 pr BOOL .
 pr INT .
 pr FLOAT .
 protecting STRING .
 inc LIST-CONS { String } .
 protecting META-LEVEL .

 sorts Msg MsgQ event .
 op bcastMsg : List{String} Msg -> Msg .
endfm