maude-help AT lists.cs.illinois.edu

Subject: Maude-help mailing list

List archive

[Maude-help] bad token ^ when using default code in prelude.maude and redefine again

From: Mandy Martin <tesleft AT hotmail.com>
To: "maude-help AT cs.uiuc.edu" <maude-help AT cs.uiuc.edu>
Subject: [Maude-help] bad token ^ when using default code in prelude.maude and redefine again
Date: Sun, 14 Jun 2015 23:08:57 +0800
Importance: Normal
List-archive: <http://lists.cs.uiuc.edu/pipermail/maude-help/>
List-id: <maude-help.cs.uiuc.edu>

i copy the NAT from prelude.maude in source .tar.gz

and it redefine the NAT in maude console, but together with the polynomial code, though it use NAT and RAT the same as default,

it has error bad token ^. why same default code, there is error?

in fact, i want to redefine NAT with two different NAT1 and NAT2, however, there is already difficulty in using default code.

Maude> fmod QID-RAT-POLY is

> pr RAT-POLY{Qid} .

> endfm

Advisory: redefining module QID-RAT-POLY.

Warning: unusable view Qid while evaluating module instantiation RAT-POLY{Qid}.

Maude> red in QID-RAT-POLY : (((3) ('X ^ 2) ('X ^ 3)) -- ((1) ('X ^ 5))) ++ ((2) ('X ^ 5)) .

Warning: <standard input>, line 646: bad token ^.

Warning: <standard input>, line 646: no parse for term.

fmod NAT is

protecting BOOL .

sorts Zero NzNat Nat .

subsort Zero NzNat < Nat .

op 0 : -> Zero [ctor] .

op s_ : Nat -> NzNat

[ctor iter

special (id-hook SuccSymbol

term-hook zeroTerm (0))] .

op _+_ : NzNat Nat -> NzNat

[assoc comm prec 33

special (id-hook ACU_NumberOpSymbol (+)

op-hook succSymbol (s_ : Nat ~> NzNat))] .

op _+_ : Nat Nat -> Nat [ditto] .

op sd : Nat Nat -> Nat

[comm

special (id-hook CUI_NumberOpSymbol (sd)

op-hook succSymbol (s_ : Nat ~> NzNat))] .

op _*_ : NzNat NzNat -> NzNat

[assoc comm prec 31

special (id-hook ACU_NumberOpSymbol (*)

op-hook succSymbol (s_ : Nat ~> NzNat))] .

op _*_ : Nat Nat -> Nat [ditto] .

op _quo_ : Nat NzNat -> Nat

[prec 31 gather (E e)

special (id-hook NumberOpSymbol (quo)

op-hook succSymbol (s_ : Nat ~> NzNat))] .

op _rem_ : Nat NzNat -> Nat

[prec 31 gather (E e)

special (id-hook NumberOpSymbol (rem)

op-hook succSymbol (s_ : Nat ~> NzNat))] .

op _^_ : Nat Nat -> Nat

[prec 29 gather (E e)

special (id-hook NumberOpSymbol (^)

op-hook succSymbol (s_ : Nat ~> NzNat))] .

op _^_ : NzNat Nat -> NzNat [ditto] .

op modExp : Nat Nat NzNat ~> Nat

[special (id-hook NumberOpSymbol (modExp)

op-hook succSymbol (s_ : Nat ~> NzNat))] .

op gcd : NzNat Nat -> NzNat

[assoc comm

special (id-hook ACU_NumberOpSymbol (gcd)

op-hook succSymbol (s_ : Nat ~> NzNat))] .

op gcd : Nat Nat -> Nat [ditto] .

op lcm : NzNat NzNat -> NzNat

[assoc comm

special (id-hook ACU_NumberOpSymbol (lcm)

op-hook succSymbol (s_ : Nat ~> NzNat))] .

op lcm : Nat Nat -> Nat [ditto] .

op min : NzNat NzNat -> NzNat

[assoc comm

special (id-hook ACU_NumberOpSymbol (min)

op-hook succSymbol (s_ : Nat ~> NzNat))] .

op min : Nat Nat -> Nat [ditto] .

op max : NzNat Nat -> NzNat

[assoc comm

special (id-hook ACU_NumberOpSymbol (max)

op-hook succSymbol (s_ : Nat ~> NzNat))] .

op max : Nat Nat -> Nat [ditto] .

op _xor_ : Nat Nat -> Nat

[assoc comm prec 55

special (id-hook ACU_NumberOpSymbol (xor)

op-hook succSymbol (s_ : Nat ~> NzNat))] .

op _&_ : Nat Nat -> Nat

[assoc comm prec 53

special (id-hook ACU_NumberOpSymbol (&)

op-hook succSymbol (s_ : Nat ~> NzNat))] .

op _|_ : NzNat Nat -> NzNat

[assoc comm prec 57

special (id-hook ACU_NumberOpSymbol (|)

op-hook succSymbol (s_ : Nat ~> NzNat))] .

op _|_ : Nat Nat -> Nat [ditto] .

op _>>_ : Nat Nat -> Nat

[prec 35 gather (E e)

special (id-hook NumberOpSymbol (>>)

op-hook succSymbol (s_ : Nat ~> NzNat))] .

op _<<_ : Nat Nat -> Nat

[prec 35 gather (E e)

special (id-hook NumberOpSymbol (<<)

op-hook succSymbol (s_ : Nat ~> NzNat))] .

op _<_ : Nat Nat -> Bool

[prec 37

special (id-hook NumberOpSymbol (<)

op-hook succSymbol (s_ : Nat ~> NzNat)

term-hook trueTerm (true)

term-hook falseTerm (false))] .

op _<=_ : Nat Nat -> Bool

[prec 37

special (id-hook NumberOpSymbol (<=)

op-hook succSymbol (s_ : Nat ~> NzNat)

term-hook trueTerm (true)

term-hook falseTerm (false))] .

op _>_ : Nat Nat -> Bool

[prec 37

special (id-hook NumberOpSymbol (>)

op-hook succSymbol (s_ : Nat ~> NzNat)

term-hook trueTerm (true)

term-hook falseTerm (false))] .

op _>=_ : Nat Nat -> Bool

[prec 37

special (id-hook NumberOpSymbol (>=)

op-hook succSymbol (s_ : Nat ~> NzNat)

term-hook trueTerm (true)

term-hook falseTerm (false))] .

op _divides_ : NzNat Nat -> Bool

[prec 51

special (id-hook NumberOpSymbol (divides)

op-hook succSymbol (s_ : Nat ~> NzNat)

term-hook trueTerm (true)

term-hook falseTerm (false))] .

endfm

fmod INT is

protecting NAT .

sorts NzInt Int .

subsorts NzNat < NzInt Nat < Int .

op -_ : NzNat -> NzInt

[ctor

special (id-hook MinusSymbol

op-hook succSymbol (s_ : Nat ~> NzNat)

op-hook minusSymbol (-_ : NzNat ~> Int))] .

op -_ : NzInt -> NzInt [ditto] .

op -_ : Int -> Int [ditto] .

op _+_ : Int Int -> Int

[assoc comm prec 33

special (id-hook ACU_NumberOpSymbol (+)

op-hook succSymbol (s_ : Nat ~> NzNat)

op-hook minusSymbol (-_ : NzNat ~> Int))] .

op _-_ : Int Int -> Int

[prec 33 gather (E e)

special (id-hook NumberOpSymbol (-)

op-hook succSymbol (s_ : Nat ~> NzNat)

op-hook minusSymbol (-_ : NzNat ~> Int))] .

op _*_ : NzInt NzInt -> NzInt

[assoc comm prec 31

special (id-hook ACU_NumberOpSymbol (*)

op-hook succSymbol (s_ : Nat ~> NzNat)

op-hook minusSymbol (-_ : NzNat ~> Int))] .

op _*_ : Int Int -> Int [ditto] .

op _quo_ : Int NzInt -> Int

[prec 31 gather (E e)

special (id-hook NumberOpSymbol (quo)

op-hook succSymbol (s_ : Nat ~> NzNat)

op-hook minusSymbol (-_ : NzNat ~> Int))] .

op _rem_ : Int NzInt -> Int

[prec 31 gather (E e)

special (id-hook NumberOpSymbol (rem)

op-hook succSymbol (s_ : Nat ~> NzNat)

op-hook minusSymbol (-_ : NzNat ~> Int))] .

op _^_ : Int Nat -> Int

[prec 29 gather (E e)

special (id-hook NumberOpSymbol (^)

op-hook succSymbol (s_ : Nat ~> NzNat)

op-hook minusSymbol (-_ : NzNat ~> Int))] .

op _^_ : NzInt Nat -> NzInt [ditto] .

op abs : NzInt -> NzNat

[special (id-hook NumberOpSymbol (abs)

op-hook succSymbol (s_ : Nat ~> NzNat)

op-hook minusSymbol (-_ : NzNat ~> Int))] .

op abs : Int -> Nat [ditto] .

op gcd : NzInt Int -> NzNat

[assoc comm

special (id-hook ACU_NumberOpSymbol (gcd)

op-hook succSymbol (s_ : Nat ~> NzNat)

op-hook minusSymbol (-_ : NzNat ~> Int))] .

op gcd : Int Int -> Nat [ditto] .

op lcm : NzInt NzInt -> NzNat

[assoc comm

special (id-hook ACU_NumberOpSymbol (lcm)

op-hook succSymbol (s_ : Nat ~> NzNat)

op-hook minusSymbol (-_ : NzNat ~> Int))] .

op lcm : Int Int -> Nat [ditto] .

op min : NzInt NzInt -> NzInt

[assoc comm

special (id-hook ACU_NumberOpSymbol (min)

op-hook succSymbol (s_ : Nat ~> NzNat)

op-hook minusSymbol (-_ : NzNat ~> Int))] .

op min : Int Int -> Int [ditto] .

op max : NzInt NzInt -> NzInt

[assoc comm

special (id-hook ACU_NumberOpSymbol (max)

op-hook succSymbol (s_ : Nat ~> NzNat)

op-hook minusSymbol (-_ : NzNat ~> Int))] .

op max : Int Int -> Int [ditto] .

op max : NzNat Int -> NzNat [ditto] .

op max : Nat Int -> Nat [ditto] .

op ~_ : Int -> Int

[special (id-hook NumberOpSymbol (~)

op-hook succSymbol (s_ : Nat ~> NzNat)

op-hook minusSymbol (-_ : NzNat ~> Int))] .

op _xor_ : Int Int -> Int

[assoc comm prec 55

special (id-hook ACU_NumberOpSymbol (xor)

op-hook succSymbol (s_ : Nat ~> NzNat)

op-hook minusSymbol (-_ : NzNat ~> Int))] .

op _&_ : Nat Int -> Nat

[assoc comm prec 53

special (id-hook ACU_NumberOpSymbol (&)

op-hook succSymbol (s_ : Nat ~> NzNat)

op-hook minusSymbol (-_ : NzNat ~> Int))] .

op _&_ : Int Int -> Int [ditto] .

op _|_ : NzInt Int -> NzInt

[assoc comm prec 57

special (id-hook ACU_NumberOpSymbol (|)

op-hook succSymbol (s_ : Nat ~> NzNat)

op-hook minusSymbol (-_ : NzNat ~> Int))] .

op _|_ : Int Int -> Int [ditto] .

op _>>_ : Int Nat -> Int

[prec 35 gather (E e)

special (id-hook NumberOpSymbol (>>)

op-hook succSymbol (s_ : Nat ~> NzNat)

op-hook minusSymbol (-_ : NzNat ~> Int))] .

op _<<_ : Int Nat -> Int

[prec 35 gather (E e)

special (id-hook NumberOpSymbol (<<)

op-hook succSymbol (s_ : Nat ~> NzNat)

op-hook minusSymbol (-_ : NzNat ~> Int))] .

op _<_ : Int Int -> Bool

[prec 37

special (id-hook NumberOpSymbol (<)

op-hook succSymbol (s_ : Nat ~> NzNat)

op-hook minusSymbol (-_ : NzNat ~> Int)

term-hook trueTerm (true)

term-hook falseTerm (false))] .

op _<=_ : Int Int -> Bool

[prec 37

special (id-hook NumberOpSymbol (<=)

op-hook succSymbol (s_ : Nat ~> NzNat)

op-hook minusSymbol (-_ : NzNat ~> Int)

term-hook trueTerm (true)

term-hook falseTerm (false))] .

op _>_ : Int Int -> Bool

[prec 37

special (id-hook NumberOpSymbol (>)

op-hook succSymbol (s_ : Nat ~> NzNat)

op-hook minusSymbol (-_ : NzNat ~> Int)

term-hook trueTerm (true)

term-hook falseTerm (false))] .

op _>=_ : Int Int -> Bool

[prec 37

special (id-hook NumberOpSymbol (>=)

op-hook succSymbol (s_ : Nat ~> NzNat)

op-hook minusSymbol (-_ : NzNat ~> Int)

term-hook trueTerm (true)

term-hook falseTerm (false))] .

op _divides_ : NzInt Int -> Bool

[prec 51

special (id-hook NumberOpSymbol (divides)

op-hook succSymbol (s_ : Nat ~> NzNat)

op-hook minusSymbol (-_ : NzNat ~> Int)

term-hook trueTerm (true)

term-hook falseTerm (false))] .

endfm

fmod RAT is

protecting INT .

sorts PosRat NzRat Rat .

subsorts NzInt < NzRat Int < Rat .

subsorts NzNat < PosRat < NzRat .

op _/_ : NzInt NzNat -> NzRat

[ctor prec 31 gather (E e)

special (id-hook DivisionSymbol

op-hook succSymbol (s_ : Nat ~> NzNat)

op-hook minusSymbol (-_ : NzNat ~> Int))] .

var I J : NzInt .

var N M : NzNat .

var K : Int .

var Z : Nat .

var Q : NzRat .

var R : Rat .

op _/_ : NzNat NzNat -> PosRat [ctor ditto] .

op _/_ : PosRat PosRat -> PosRat [ditto] .

op _/_ : NzRat NzRat -> NzRat [ditto] .

op _/_ : Rat NzRat -> Rat [ditto] .

eq 0 / Q = 0 .

eq I / - N = - I / N .

eq (I / N) / (J / M) = (I * M) / (J * N) .

eq (I / N) / J = I / (J * N) .

eq I / (J / M) = (I * M) / J .

op -_ : NzRat -> NzRat [ditto] .

op -_ : Rat -> Rat [ditto] .

eq - (I / N) = - I / N .

op _+_ : PosRat PosRat -> PosRat [ditto] .

op _+_ : PosRat Nat -> PosRat [ditto] .

op _+_ : Rat Rat -> Rat [ditto] .

eq I / N + J / M = (I * M + J * N) / (N * M) .

eq I / N + K = (I + K * N) / N .

op _-_ : Rat Rat -> Rat [ditto] .

eq I / N - J / M = (I * M - J * N) / (N * M) .

eq I / N - K = (I - K * N) / N .

eq K - J / M = (K * M - J ) / M .

op _*_ : PosRat PosRat -> PosRat [ditto] .

op _*_ : NzRat NzRat -> NzRat [ditto] .

op _*_ : Rat Rat -> Rat [ditto] .

eq Q * 0 = 0 .

eq (I / N) * (J / M) = (I * J) / (N * M).

eq (I / N) * K = (I * K) / N .

op _quo_ : PosRat PosRat -> Nat [ditto] .

op _quo_ : Rat NzRat -> Int [ditto] .

eq (I / N) quo Q = I quo (N * Q) .

eq K quo (J / M) = (K * M) quo J .

op _rem_ : Rat NzRat -> Rat [ditto] .

eq (I / N) rem (J / M) = ((I * M) rem (J * N)) / (N * M) .

eq K rem (J / M) = ((K * M) rem J) / M .

eq (I / N) rem J = (I rem (J * N)) / N .

op _^_ : PosRat Nat -> PosRat [ditto] .

op _^_ : NzRat Nat -> NzRat [ditto] .

op _^_ : Rat Nat -> Rat [ditto] .

eq (I / N) ^ Z = (I ^ Z) / (N ^ Z) .

op abs : NzRat -> PosRat [ditto] .

op abs : Rat -> Rat [ditto] .

eq abs(I / N) = abs(I) / N .

op gcd : NzRat Rat -> PosRat [ditto] .

op gcd : Rat Rat -> Rat [ditto] .

eq gcd(I / N, R) = gcd(I, N * R) / N .

op lcm : NzRat NzRat -> PosRat [ditto] .

op lcm : Rat Rat -> Rat [ditto] .

eq lcm(I / N, R) = lcm(I, N * R) / N .

op min : PosRat PosRat -> PosRat [ditto] .

op min : NzRat NzRat -> NzRat [ditto] .

op min : Rat Rat -> Rat [ditto] .

eq min(I / N, R) = min(I, N * R) / N .

op max : PosRat Rat -> PosRat [ditto] .

op max : NzRat NzRat -> NzRat [ditto] .

op max : Rat Rat -> Rat [ditto] .

eq max(I / N, R) = max(I, N * R) / N .

op _<_ : Rat Rat -> Bool [ditto] .

eq (I / N) < (J / M) = (I * M) < (J * N) .

eq (I / N) < K = I < (K * N) .

eq K < (J / M) = (K * M) < J .

op _<=_ : Rat Rat -> Bool [ditto] .

eq (I / N) <= (J / M) = (I * M) <= (J * N) .

eq (I / N) <= K = I <= (K * N) .

eq K <= (J / M) = (K * M) <= J .

op _>_ : Rat Rat -> Bool [ditto] .

eq (I / N) > (J / M) = (I * M) > (J * N) .

eq (I / N) > K = I > (K * N) .

eq K > (J / M) = (K * M) > J .

op _>=_ : Rat Rat -> Bool [ditto] .

eq (I / N) >= (J / M) = (I * M) >= (J * N) .

eq (I / N) >= K = I >= (K * N) .

eq K >= (J / M) = (K * M) >= J .

op _divides_ : NzRat Rat -> Bool [ditto] .

eq (I / N) divides K = I divides N * K .

eq Q divides (J / M) = Q * M divides J .

op trunc : PosRat -> Nat .

op trunc : Rat -> Int .

eq trunc(K) = K .

eq trunc(I / N) = I quo N .

op frac : Rat -> Rat .

eq frac(K) = 0 .

eq frac(I / N) = (I rem N) / N .

op floor : PosRat -> Nat .

op floor : Rat -> Int .

op ceiling : PosRat -> NzNat .

op ceiling : Rat -> Int .

eq floor(K) = K .

eq ceiling(K) = K .

eq floor(N / M) = N quo M .

eq ceiling(N / M) = ((N + M) - 1) quo M .

eq floor(- N / M) = - ceiling(N / M) .

eq ceiling(- N / M) = - floor(N / M) .

endfm

fmod FLOAT is

protecting BOOL .

sorts FiniteFloat Float .

subsort FiniteFloat < Float .

*** pseudo constructor for the set of double precision floats

op <Floats> : -> FiniteFloat [special (id-hook FloatSymbol)] .

op <Floats> : -> Float [ditto] .

op -_ : Float -> Float

[prec 15

special (id-hook FloatOpSymbol (-)

op-hook floatSymbol (<Floats> : ~> Float))] .

op -_ : FiniteFloat -> FiniteFloat [ditto] .

op _+_ : Float Float -> Float

[prec 33 gather (E e)

special (id-hook FloatOpSymbol (+)

op-hook floatSymbol (<Floats> : ~> Float))] .

op _-_ : Float Float -> Float

[prec 33 gather (E e)

special (id-hook FloatOpSymbol (-)

op-hook floatSymbol (<Floats> : ~> Float))] .

op _*_ : Float Float -> Float

[prec 31 gather (E e)

special (id-hook FloatOpSymbol (*)

op-hook floatSymbol (<Floats> : ~> Float))] .

op _/_ : Float Float ~> Float

[prec 31 gather (E e)

special (id-hook FloatOpSymbol (/)

op-hook floatSymbol (<Floats> : ~> Float))] .

op _rem_ : Float Float ~> Float

[prec 31 gather (E e)

special (id-hook FloatOpSymbol (rem)

op-hook floatSymbol (<Floats> : ~> Float))] .

op _^_ : Float Float ~> Float

[prec 29 gather (E e)

special (id-hook FloatOpSymbol (^)

op-hook floatSymbol (<Floats> : ~> Float))] .

op abs : Float -> Float

[special (id-hook FloatOpSymbol (abs)

op-hook floatSymbol (<Floats> : ~> Float))] .

op abs : FiniteFloat -> FiniteFloat [ditto] .

op floor : Float -> Float

[special (id-hook FloatOpSymbol (floor)

op-hook floatSymbol (<Floats> : ~> Float))] .

op ceiling : Float -> Float

[special (id-hook FloatOpSymbol (ceiling)

op-hook floatSymbol (<Floats> : ~> Float))] .

op min : Float Float -> Float

[special (id-hook FloatOpSymbol (min)

op-hook floatSymbol (<Floats> : ~> Float))] .

op max : Float Float -> Float

[special (id-hook FloatOpSymbol (max)

op-hook floatSymbol (<Floats> : ~> Float))] .

op sqrt : Float ~> Float

[special (id-hook FloatOpSymbol (sqrt)

op-hook floatSymbol (<Floats> : ~> Float))] .

op exp : Float -> Float

[special (id-hook FloatOpSymbol (exp)

op-hook floatSymbol (<Floats> : ~> Float))] .

op log : Float ~> Float

[special (id-hook FloatOpSymbol (log)

op-hook floatSymbol (<Floats> : ~> Float))] .

op sin : Float -> Float

[special (id-hook FloatOpSymbol (sin)

op-hook floatSymbol (<Floats> : ~> Float))] .

op cos : Float -> Float

[special (id-hook FloatOpSymbol (cos)

op-hook floatSymbol (<Floats> : ~> Float))] .

op tan : Float -> Float

[special (id-hook FloatOpSymbol (tan)

op-hook floatSymbol (<Floats> : ~> Float))] .

op asin : Float ~> Float

[special (id-hook FloatOpSymbol (asin)

op-hook floatSymbol (<Floats> : ~> Float))] .

op acos : Float ~> Float

[special (id-hook FloatOpSymbol (acos)

op-hook floatSymbol (<Floats> : ~> Float))] .

op atan : Float -> Float

[special (id-hook FloatOpSymbol (atan)

op-hook floatSymbol (<Floats> : ~> Float))] .

op atan : Float Float -> Float

[special (id-hook FloatOpSymbol (atan)

op-hook floatSymbol (<Floats> : ~> Float))] .

op _<_ : Float Float -> Bool

[prec 51

special (id-hook FloatOpSymbol (<)

op-hook floatSymbol (<Floats> : ~> Float)

term-hook trueTerm (true)

term-hook falseTerm (false))] .

op _<=_ : Float Float -> Bool

[prec 51

special (id-hook FloatOpSymbol (<=)

op-hook floatSymbol (<Floats> : ~> Float)

term-hook trueTerm (true)

term-hook falseTerm (false))] .

op _>_ : Float Float -> Bool

[prec 51

special (id-hook FloatOpSymbol (>)

op-hook floatSymbol (<Floats> : ~> Float)

term-hook trueTerm (true)

term-hook falseTerm (false))] .

op _>=_ : Float Float -> Bool

[prec 51

special (id-hook FloatOpSymbol (>=)

op-hook floatSymbol (<Floats> : ~> Float)

term-hook trueTerm (true)

term-hook falseTerm (false))] .

op pi : -> FiniteFloat .

eq pi = 3.1415926535897931 .

op _=[_]_ : Float FiniteFloat Float -> Bool [prec 51 format (d d d d d s d)] .

var X Y : Float .

var Z : FiniteFloat .

eq X =[Z] Y = abs(X - Y) < Z .

endfm

fth RING is

sort Ring .

ops z e : -> Ring .

op _+_ : Ring Ring -> Ring [assoc comm id: z] .

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] .

eq A * (B - C) = (A * B) - (A * C) [nonexec] .

endfth

fmod MONOMIAL{X :: TRIV} is

protecting NAT1 .

protecting NAT2 .

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} -> Poly{R, X} [assoc] .

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 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 U) = (A -- B) U .

eq (A U) (B V) = (A B) (U V) .

eq A B = A * B .

eq A ++ B = A + B .

eq A -- B = A - B .

endfm

view RingToRat from RING to RAT is

sort Ring to Rat .

op e to term 1 .

op z to 0 .

endv

fmod RAT-POLY{X :: TRIV} is

protecting POLYNOMIAL{RingToRat, X} .

endfm

fmod QID-RAT-POLY is

pr RAT-POLY{Qid} .

endfm

Regards,

Martin Lee

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

[Maude-help] how to simulate this natural numbers system, Mandy Martin, 06/10/2015
- Re: [Maude-help] how to simulate this natural numbers system, Mandy Martin, 06/10/2015
  - Re: [Maude-help] how to simulate this natural numbers system, Mandy Martin, 06/10/2015
    - [Maude-help] how to use the traditional polynomials example in manual, Mandy Martin, 06/11/2015
      - Re: [Maude-help] how to use the traditional polynomials example in manual, Francisco Durán, 06/12/2015
        
        Re: [Maude-help] how to use the traditional polynomials example in manual, Mandy Martin, 06/12/2015
        
        [Maude-help] how to use predicates.maude in Igor2.3 and how to get the result from Rewrite Result, Mandy Martin, 06/12/2015
        
        [Maude-help] bad token ^ when using default code in prelude.maude and redefine again, Mandy Martin, 06/14/2015
        
        Re: [Maude-help] how to use the traditional polynomials example in manual, Mandy Martin, 06/13/2015
        
        Re: [Maude-help] how to use the traditional polynomials example in manual, Mandy Martin, 06/13/2015
        [Maude-help] why minus result is wrong and how to return understandable result from haskell maude, Mandy Martin, 06/13/2015
        
        [Maude-help] why sign of two terms exchanged in minus case, Mandy Martin, 06/13/2015
        
        Re: [Maude-help] why sign of two terms exchanged in minus case, Mandy Martin, 06/13/2015