***(

    This file is part of the Maude 2 interpreter.

    Copyright 1997-2005 SRI International, Menlo Park, CA 94025, USA.

    This program is free software; you can redistribute it and/or modify
    it under the terms of the GNU General Public License as published by
    the Free Software Foundation; either version 2 of the License, or
    (at your option) any later version.

    This program is distributed in the hope that it will be useful,
    but WITHOUT ANY WARRANTY; without even the implied warranty of
    MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
    GNU General Public License for more details.

    You should have received a copy of the GNU General Public License
    along with this program; if not, write to the Free Software
    Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307, USA.

)

***
***	Alternative version of the number hierarchy from the Maude 2 prelude.
***	This version avoids built-in semantics and defines all operations by
***	equational rewriting. The special for s_ is retained since this is a
***	constructor with no special semantics apart from i/o and internal
***	representation considerations.
***

fmod NAT is
  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))] .

  vars N M L : Nat .
  vars N' M' L' : NzNat .

  op _+_ : NzNat Nat -> NzNat [assoc comm prec 33] .
  op _+_ : Nat Nat -> Nat [ditto] .
  eq N + 0 = N .
  eq N + s M = s (N + M) .

  op sd : Nat Nat -> Nat [comm] .
  eq sd(N , 0) = N .
  eq sd(s N, s M) = sd(N, M) .

  op _*_ : NzNat NzNat -> NzNat [assoc comm prec 31] .
  op _*_ : Nat Nat -> Nat [ditto] .
  eq N * 0 = 0 .
  eq N * s M = N * M + N .

  op _quo_ : Nat NzNat -> Nat [prec 31 gather (E e)] .
  eq N quo M' = $quoAux(N, M', M') .

  op $quoAux : Nat Nat NzNat -> Nat .
  eq $quoAux(0, L', M') = 0 .
  eq $quoAux(N, 0, M') = s $quoAux(N, M', M') .
  eq $quoAux(s N, s L, M') = $quoAux(N, L, M') .

  op _rem_ : Nat NzNat -> Nat [prec 31 gather (E e)] .
  eq N rem M' = sd(M', $remAux(N, M', M')) .

  op $remAux : Nat Nat NzNat -> NzNat .
  eq $remAux(0, L', M') = L' .
  eq $remAux(N, 0, M') = $remAux(N, M', M') .
  eq $remAux(s N, s L, M') = $remAux(N, L, M') .

  op _^_ : Nat Nat -> Nat [prec 29  gather (E e)] .
  op _^_ : NzNat Nat -> NzNat [ditto] .
  eq N ^ 0 = 1 .
  eq N ^ s M = N ^ M * N .

  op modExp : Nat Nat NzNat ~> Nat .
  eq modExp(N, M, L') = N ^ M rem L' .

  op gcd : NzNat Nat -> NzNat [assoc comm] .
  op gcd : Nat Nat -> Nat [ditto] .
  eq gcd(N, M) = $gcd(N, M) .

  op $gcd : Nat Nat -> Nat .
  eq $gcd(N, 0) = N .
  eq $gcd(N, M') = $gcd(M', N rem M') .

  op lcm : NzNat NzNat -> NzNat [assoc comm] .
  op lcm : Nat Nat -> Nat [ditto] .
  eq lcm(N, 0) = 0 .
  eq lcm(N, M') = (N quo $gcd(N, M')) * M' .

  op min : NzNat NzNat -> NzNat [assoc comm] .
  op min : Nat Nat -> Nat [ditto] .
  eq min(N, 0) = 0 .
  eq min(s N, s M) = s min(N, M) .

  op max : NzNat Nat -> NzNat [assoc comm] .
  op max : Nat Nat -> Nat [ditto] .
  eq max(N, 0) = N .
  eq max(s N, s M) = s max(N, M) .

  op _xor_ : Nat Nat -> Nat [assoc comm prec 55] .
  eq N xor 0 = N .
  eq N' xor M' = sd(N' rem 2, M' rem 2) + 2 * ((N' quo 2) xor (M' quo 2)) .

  op _&_ : Nat Nat -> Nat [assoc comm prec 53] .
  eq N & 0 = 0 .
  eq N' & M' = (N' rem 2) * (M' rem 2) + 2 * ((N' quo 2) & (M' quo 2)) .

  op _|_ : NzNat Nat -> NzNat [assoc comm prec 57] .
  op _|_ : Nat Nat -> Nat [ditto] .
  eq N | M = N & M xor N xor M .

  op _>>_ : Nat Nat -> Nat [prec 35 gather (E e)] .
  eq N >> 0 = N .
  eq N >> s M = (N >> M) quo 2 .

  op _<<_ : Nat Nat -> Nat [prec 35 gather (E e)] .
  eq N << 0 = N .
  eq N << s M = (N << M) * 2 .

  op _<_ : Nat Nat -> Bool [prec 37] .
  eq N < 0 = false .
  eq 0 < M' = true .
  eq s N < s M = N < M .

  op _<=_ : Nat Nat -> Bool [prec 37] .
  eq N' <= 0 = false .
  eq 0 <= M = true .
  eq s N <= s M = N <= M .

  op _>_ : Nat Nat -> Bool [prec 37] .
  eq N > M = M < N .

  op _>=_ : Nat Nat -> Bool [prec 37] .
  eq N >= M = M <= N .

  op _divides_ : NzNat Nat -> Bool .
  eq N' divides M = $dividesAux(M, N', N') .

  op $dividesAux : Nat Nat NzNat -> Bool .
  eq $dividesAux(0, 0, M') = true .
  eq $dividesAux(0, L', M') = false .
  eq $dividesAux(N', 0, M') = $dividesAux(N', M', M') .
  eq $dividesAux(s N, s L, M') = $dividesAux(N, L, M') .
endfm

fmod INT is
  protecting NAT .
  sorts NzInt Int .
  subsorts NzNat < NzInt Nat < Int .

  vars N M : Nat .
  vars N' M' : NzNat .
  vars I J : Int .

  op -_ : NzNat -> NzInt [ctor] .
  op -_ : NzInt -> NzInt .
  op -_ : Int -> Int .
  eq - 0 = 0 .
  eq - - N = N .

  op _+_ : Int Int -> Int [ditto] .
  eq I + 0 = I .
  eq - s N + s M = - N + M .
  eq - N' + - M' = -(N' + M') .

  op _-_ : Int Int -> Int [prec 33 gather (E e)] .
  eq I - J = I + - J .

  op _*_ : NzInt NzInt -> NzInt [ditto] .
  eq I * 0 = 0 .
  eq I * - M' = -(I * M') .

  op _quo_ : Int NzInt -> Int [ditto] .
  eq I quo - M' = -(I quo M') .
  eq - N' quo M' = -(N' quo M') .

  op _rem_ : Int NzInt -> Int [ditto] .
  eq I rem - M' = I rem M' .
  eq - N' rem M' = -(N' rem M') .

  op _^_ : Int Nat -> Int [ditto] .
  op _^_ : NzInt Nat -> NzInt [ditto] .
  eq I ^ 0 = 1 .
  eq I ^ s M = I ^ M * I .

  op abs : NzInt -> NzNat .
  op abs : Int -> Nat .
  eq abs(N) = abs(N) .
  eq abs(- N') = abs(N') .

  op gcd : NzInt Int -> NzNat [ditto] .
  op gcd : Int Int -> Nat [ditto] .
  eq gcd(- N', I) = gcd(N', I) .

  op lcm : NzInt NzInt -> NzNat [ditto] .
  op lcm : Int Int -> Nat [ditto] .
  eq lcm(- N', I) = lcm(N', I) .

  op min : NzInt NzInt -> NzInt [ditto] .
  op min : Int Int -> Int [ditto] .
  eq min(- N', M) = - N' .
  eq min(- N', - M') = - max(N', M') .

  op max : NzInt NzInt -> NzInt [ditto] .
  op max : Int Int -> Int [ditto] .
  op max : NzNat Int -> NzNat [ditto] .
  op max : Nat Int -> Nat [ditto] .
  eq max(- N', M) = M .
  eq max(- N', - M') = - min(N', M') .

  op ~_ : Int -> Int .
  eq ~ I = - I - 1 .

  op _xor_ : Int Int -> Int [ditto] .
  eq - s N xor  J = ~ (N xor J) .

  op _&_ : Nat Int -> Nat [ditto] .
  op _&_ : Int Int -> Int [ditto] .
  eq I & 0 = 0 .
  eq - s N & M' = (s N rem 2) * (M' rem 2) + 2 * (~(N quo 2) & (M' quo 2)) .
  eq - s N & - s M = ~(N | M) .

  op _|_ : NzInt Int -> NzInt [ditto] .
  op _|_ : Int Int -> Int [ditto] .
  eq I | J = I & J xor I xor J .

  op _>>_ : Int Nat -> Int [ditto] .
  eq - s N >> M = ~(N >> M) .

  op _<<_ : Int Nat -> Int [ditto] .
  eq I << 0 = I .
  eq I << s M = (I << M) * 2 .

  op _<_ : Int Int -> Bool [ditto] .
  eq - N' < M = true .
  eq N < - M' = false .
  eq - N' < - M' = N' > M' .

  op _<=_ : Int Int -> Bool [ditto] .
  eq - N' <= M = true .
  eq N <= - M' = false .
  eq - N' <= - M' = N' >= M' .

  op _>_ : Int Int -> Bool [ditto] .
  eq I > J = J < I .

  op _>=_ : Int Int -> Bool [ditto] .
  eq I >= J = J <= I .

  op _divides_ : NzInt Int -> Bool [ditto] .
  eq - N' divides J = N' divides J .
  eq N' divides - M' = N' divides M' .
endfm

fmod RAT is
  protecting INT .
  sorts PosRat NzRat Rat .
  subsorts NzInt < NzRat Int < Rat .
  subsorts NzNat < PosRat < NzRat .

  var I J : NzInt .
  var N M : NzNat .
  var K : Int .
  var Z : Nat .
  var Q : NzRat .
  var R : Rat .

  op _/_ : NzInt NzNat -> NzRat [ctor prec 31 gather (E e)] .
  op _/_ : NzNat NzNat -> PosRat [ctor ditto] .
  ceq I / N = (I quo gcd(I, N)) / (N quo gcd(I, N)) if gcd(I, N) > 1 .

  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