egison-4.1.3: lib/math/common/arithmetic.egi
--
--
-- Arithmetic Operation
--
--
def toMathExpr arg := mathNormalize (toMathExpr' arg)
infixl expression 6 +
infixl expression 6 -
infixl expression 7 *
infixl expression 7 /
infixl expression 8 ^
infixl expression 6 +'
infixl expression 6 -'
infixl expression 7 *'
infixl expression 7 /'
infixl expression 8 ^'
def (+') := b.+
def (-') := b.-
def (*') := b.*
def (/') := b./
def (+) $x $y :=
match (isFloat x, isFloat y) as eq with
| #(True, True) -> f.+ x y
| #(True, False) -> f.+ x (itof y)
| #(False, True) -> f.+ (itof x) y
| _ -> mathNormalize (x +' y)
def (-) $x $y :=
match (isFloat x, isFloat y) as eq with
| #(True, True) -> f.- x y
| #(True, False) -> f.- x (itof y)
| #(False, True) -> f.- (itof x) y
| _ -> mathNormalize (x -' y)
def (*) $x $y :=
match (isFloat x, isFloat y) as eq with
| #(True, True) -> f.* x y
| #(True, False) -> f.* x (itof y)
| #(False, True) -> f.* (itof x) y
| _ -> mathNormalize (x *' y)
def (/) $x $y :=
match (isFloat x, isFloat y) as eq with
| #(True, True) -> f./ x y
| #(True, False) -> f./ x (itof y)
| #(False, True) -> f./ (itof x) y
| _ -> x /' y
def sum xs := foldl (+) 0 xs
def sum' xs := foldl (+') 0 xs
def product xs := foldl (*) 1 xs
def product' xs := foldl (*') 1 xs
def power $x $n := mathNormalize (power' x n)
def power' $x $n := foldl (*') 1 (take n (repeat1 x))
def (^) $x $n :=
if x = e
then exp n
else if isRational n
then if n >= 0
then if isInteger n then power x n else '(^) x n
else 1 / x ^ neg n
else '(^) x n
def (^') $x $n :=
if x = e
then exp n
else if isRational n
then if n >= 0
then if isInteger n then power' x n else '(^) x n
else 1 /' x ^' neg n
else '(^) x n
def gcd $x $y :=
match (x, y) as (termExpr, termExpr) with
| (_, #0) -> x
| (#0, _) -> y
| (term $a $xs, term $b $ys) ->
gcd' (abs a) (abs b) *' foldl (*') 1 (map (\(s, n) -> s ^' n) (AC.intersect xs ys))
def gcd' $x $y :=
match (x, y) as (integer, integer) with
| (_, #0) -> x
| (#0, _) -> y
| (_, ?(>= x)) -> gcd' (modulo y x) x
| (_, _) -> gcd' y x
def P./ fx $gx $x :=
let xs := reverse (coefficients fx x)
ys := reverse (coefficients gx x)
(zs, rs) := L./ xs ys
in ( sum' (map2 (\c n -> c *' x ^' n) (reverse zs) nats0)
, sum' (map2 (\c n -> c *' x ^' n) (reverse rs) nats0) )