Maude-help mailing list

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

Mandy,

What is X suppose to be? A variable? The only X I can see is the label of one of the parameters. The terms to be rewritten should be ground, but you can still use variables, but need to be in the module, or defined on the fly, something like X:Ring.

Cheers,

Paco

On 11/6/2015, at 20:51, Mandy Martin <tesleft AT hotmail.com> wrote:

Hi,

Maude> rew in MYPOLY : X + X . Warning: <standard input>, line 60: bad token X. Warning: <standard input>, line 60: no parse for term.

fth TRIV is 
 sort Elt .
endfth

fth RING is  
    sort Ring .  
    ops z e : -> Ring .  
    op _+_ : Ring Ring -> Ring [assoc comm id: z] .  
    op _*_ : Ring Ring -> Ring [assoc comm id: e] .  
    op -_ : Ring -> Ring .  
    vars A B C : Ring .  
    eq A + (- A) = z [nonexec] .  
    eq A * (B + C) = (A * B) + (A * C) [nonexec] .  
endfth

fmod MONOMIAL{X :: TRIV} is  
    protecting NAT .  
    sorts Pow{X} Mon{X} .  
    subsorts Pow{X} < Mon{X} .  
    *** multiplication  
    op __ : Mon{X} Mon{X} -> Mon{X} [assoc comm] .  
    op _^_ : X$Elt NzNat -> Pow{X} .  
    var  X : X$Elt .  
    vars N M : NzNat .  
    eq (X ^ N) (X ^ M) = X ^ (N + M) .  
endfm

fmod POLYNOMIAL{R :: RING, X :: TRIV} is  
    protecting MONOMIAL{X} .  
    sorts Poly{R, X} .  
    subsorts R$Ring < Poly{R, X} .  
    *** multiplication  
    op __ : Poly{R, X} Poly{R, X} -> Poly{R, X} [assoc comm] .  
    *** addition  
    op _++_ : Poly{R, X} Poly{R, X} -> Poly{R, X} [assoc comm] .  
    op --_ : Poly{R, X} -> Poly{R, X} .  
    op __ : R$Ring Mon{X} -> Poly{R, X} .  

    vars A B : R$Ring .  
    vars U V : Mon{X} .  
    vars P Q R : Poly{R, X} .  
    eq P ++ z = P .  
    eq P ++ (-- P) = z .  
    eq P e = P .  
    eq -- (P ++ Q) = (-- P) ++ (-- Q) .  
    eq -- (A U) = (- A) U .  
    eq P (Q ++ R) = (P Q) ++ (P R) .  
    eq z U = z .  
    eq z P = z .  
    eq A (B U) = (A B) U .  
    eq (A U) ++ (B U) = (A ++ B) U .  
    eq (A U) (B V) = (A B) (U V) .  
    eq A B = A * B .  
    eq A ++ B = A + B .  
endfm

fmod MYPOLY is 
 inc POLYNOMIAL{RING, TRIV2PACKET} .
endfm

rew in MYPOLY : X + X

Regards,

Martin Lee

_______________________________________________
Maude-help mailing list
Maude-help AT cs.uiuc.edu
http://lists.cs.uiuc.edu/mailman/listinfo/maude-help