packages feed

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) )