-- |
-- Module: Symtegration.Symbolic.Simplify.NumericFolding
-- Description: Constant folding of numeric constants.
-- Copyright: Copyright 2024 Yoo Chung
-- License: Apache-2.0
-- Maintainer: dev@chungyc.org
--
-- This merges numeric terms as much as it can to simplify expressions.
-- Simplifications are finitely equivalent; i.e., any calculation with
-- finite inputs should result in the equivalent finite input.
-- The changes will also be exact, and no numeric constant will be replaced
-- by an approximate floating-point number.
module Symtegration.Symbolic.Simplify.NumericFolding (simplify) where

import Symtegration.Numeric (root)
import Symtegration.Symbolic

-- $setup
-- >>> import Symtegration.Symbolic.Haskell

-- | Simplifies computations involving numeric constants.
-- Basically, it computes as much as it can as long as any change is exact.
--
-- >>> toHaskell $ simplify $ 1 + 4
-- "5"
-- >>> toHaskell $ simplify $ 8 ** (1/3)
-- "2"
-- >>> toHaskell $ simplify $ 7 ** (1/3)
-- "7 ** (1 / 3)"
-- >>> toHaskell $ simplify $ 5 * 10 * "x"
-- "50 * x"
--
-- It will replace subtraction by addition and square roots by powers of \(\frac{1}{2}\).
simplify :: Expression -> Expression
simplify :: Expression -> Expression
simplify e :: Expression
e@(Number Integer
_) = Expression
e
simplify e :: Expression
e@(Symbol Text
_) = Expression
e
simplify (UnaryApply UnaryFunction
func Expression
x) = Expression -> Expression
unary (Expression -> Expression) -> Expression -> Expression
forall a b. (a -> b) -> a -> b
$ UnaryFunction -> Expression -> Expression
UnaryApply UnaryFunction
func (Expression -> Expression) -> Expression -> Expression
forall a b. (a -> b) -> a -> b
$ Expression -> Expression
simplify Expression
x
simplify (BinaryApply BinaryFunction
func Expression
x Expression
y) = Expression -> Expression
binary (Expression -> Expression) -> Expression -> Expression
forall a b. (a -> b) -> a -> b
$ BinaryFunction -> Expression -> Expression -> Expression
BinaryApply BinaryFunction
func (Expression -> Expression
simplify Expression
x) (Expression -> Expression
simplify Expression
y)

-- | Simplify computations involving numeric constants in unary expressions.
-- The arguments should already have been simplified.
unary :: Expression -> Expression
unary :: Expression -> Expression
unary (Negate' (Number Integer
n)) = Integer -> Expression
Number (-Integer
n)
unary (Negate' (Number Integer
n :/: Number Integer
m))
  | Integer
m Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
0 = Expression -> Expression
simplify (Expression -> Expression) -> Expression -> Expression
forall a b. (a -> b) -> a -> b
$ Integer -> Expression
Number Integer
n Expression -> Expression -> Expression
:/: Integer -> Expression
Number (-Integer
m)
  | Bool
otherwise = Expression -> Expression
simplify (Expression -> Expression) -> Expression -> Expression
forall a b. (a -> b) -> a -> b
$ Integer -> Expression
Number (-Integer
n) Expression -> Expression -> Expression
:/: Integer -> Expression
Number Integer
m
unary (Abs' (Number Integer
n)) = Integer -> Expression
Number (Integer -> Expression) -> Integer -> Expression
forall a b. (a -> b) -> a -> b
$ Integer -> Integer
forall a. Num a => a -> a
abs Integer
n
unary (Signum' (Number Integer
n)) = Integer -> Expression
Number (Integer -> Expression) -> Integer -> Expression
forall a b. (a -> b) -> a -> b
$ Integer -> Integer
forall a. Num a => a -> a
signum Integer
n
unary (Exp' Expression
x) = Expression -> Expression
simplifyExp Expression
x
unary (Log' Expression
x) = Expression -> Expression
simplifyLog Expression
x
unary (Sqrt' Expression
x) = Expression -> Expression
simplify (Expression -> Expression) -> Expression -> Expression
forall a b. (a -> b) -> a -> b
$ Expression
x Expression -> Expression -> Expression
:**: (Integer -> Expression
Number Integer
1 Expression -> Expression -> Expression
:/: Integer -> Expression
Number Integer
2)
unary (Sin' Expression
x) = Expression -> Expression
simplifySin Expression
x
unary (Cos' Expression
x) = Expression -> Expression
simplifyCos Expression
x
unary (Tan' Expression
x) = Expression -> Expression
simplifyTan Expression
x
unary Expression
e = Expression
e

-- | Simplify computations involving numeric constants in binary expressions.
-- The arguments should already have been simplified.
binary :: Expression -> Expression
-- Fold addition.
binary :: Expression -> Expression
binary (Number Integer
0 :+: Expression
x) = Expression
x
binary (Expression
x :+: Number Integer
0) = Expression
x
binary (Number Integer
n :+: Number Integer
m) = Integer -> Expression
Number (Integer
n Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
m)
binary ((Number Integer
n :/: Number Integer
m) :+: Number Integer
k) = Integer -> Integer -> Expression
reduceRatio (Integer
n Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
m Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
k) Integer
m
binary (Number Integer
n :+: (Number Integer
m :/: Number Integer
k)) = Integer -> Integer -> Expression
reduceRatio (Integer
n Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
k Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
m) Integer
k
binary ((Number Integer
n :/: Number Integer
m) :+: (Number Integer
k :/: Number Integer
l)) = Integer -> Integer -> Expression
reduceRatio (Integer
n Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
l Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
k Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
m) (Integer
m Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
l)
binary ((Expression
x :+: Number Integer
n) :+: Number Integer
m) = Integer -> Expression
Number (Integer
n Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
m) Expression -> Expression -> Expression
:+: Expression
x
binary ((Number Integer
n :+: Expression
x) :+: Number Integer
m) = Integer -> Expression
Number (Integer
n Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
m) Expression -> Expression -> Expression
:+: Expression
x
binary (Number Integer
n :+: (Expression
x :+: Number Integer
m)) = Integer -> Expression
Number (Integer
n Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
m) Expression -> Expression -> Expression
:+: Expression
x
binary (Number Integer
n :+: (Number Integer
m :+: Expression
x)) = Integer -> Expression
Number (Integer
n Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
m) Expression -> Expression -> Expression
:+: Expression
x
-- Fold multiplication.
binary (Number Integer
0 :*: Expression
_) = Integer -> Expression
Number Integer
0
binary (Expression
_ :*: Number Integer
0) = Integer -> Expression
Number Integer
0
binary (Number Integer
1 :*: Expression
x) = Expression
x
binary (Expression
x :*: Number Integer
1) = Expression
x
binary (Number Integer
n :*: Number Integer
m) = Integer -> Expression
Number (Integer
n Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
m)
binary (Number Integer
n :*: (Number Integer
m :/: Number Integer
k)) = Integer -> Integer -> Expression
reduceRatio (Integer
n Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
m) Integer
k
binary ((Number Integer
n :/: Number Integer
m) :*: Number Integer
k) = Integer -> Integer -> Expression
reduceRatio (Integer
n Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
k) Integer
m
binary ((Number Integer
n :/: Number Integer
m) :*: (Number Integer
k :/: Number Integer
l)) = Integer -> Integer -> Expression
reduceRatio (Integer
n Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
k) (Integer
m Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
l)
binary ((Expression
x :*: Number Integer
n) :*: Number Integer
m) = Integer -> Expression
Number (Integer
n Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
m) Expression -> Expression -> Expression
:*: Expression
x
binary ((Number Integer
n :*: Expression
x) :*: Number Integer
m) = Integer -> Expression
Number (Integer
n Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
m) Expression -> Expression -> Expression
:*: Expression
x
binary (Number Integer
n :*: (Expression
x :*: Number Integer
m)) = Integer -> Expression
Number (Integer
n Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
m) Expression -> Expression -> Expression
:*: Expression
x
binary (Number Integer
n :*: (Number Integer
m :*: Expression
x)) = Integer -> Expression
Number (Integer
n Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
m) Expression -> Expression -> Expression
:*: Expression
x
binary e :: Expression
e@(Number Integer
n :*: (Expression
x :/: Number Integer
m)) | Integer
m Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
/= Integer
0, Integer
m Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
n = Expression
x | Bool
otherwise = Expression
e
binary e :: Expression
e@((Expression
x :/: Number Integer
n) :*: Number Integer
m) | Integer
n Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
/= Integer
0, Integer
m Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
n = Expression
x | Bool
otherwise = Expression
e
binary (x :: Expression
x@(Number Integer
_) :*: (y :: Expression
y@(Number Integer
_ :/: Number Integer
_) :*: Expression
z)) = Expression -> Expression
simplify (Expression
x Expression -> Expression -> Expression
:*: Expression
y) Expression -> Expression -> Expression
:*: Expression
z
binary (x :: Expression
x@(Number Integer
_ :/: Number Integer
_) :*: (y :: Expression
y@(Number Integer
_ :/: Number Integer
_) :*: Expression
z)) = Expression -> Expression
simplify (Expression
x Expression -> Expression -> Expression
:*: Expression
y) Expression -> Expression -> Expression
:*: Expression
z
-- Subtractions are turned into addition.
binary (Expression
x :-: Expression
y) = Expression -> Expression
simplify (Expression -> Expression) -> Expression -> Expression
forall a b. (a -> b) -> a -> b
$ Expression
x Expression -> Expression -> Expression
:+: Expression -> Expression
Negate' Expression
y
-- Fold division.
binary e :: Expression
e@(Expression
_ :/: (Expression
_ :/: Expression
0)) = Expression
e
binary (Expression
x :/: (Expression
y :/: Expression
z)) = Expression -> Expression
simplify (Expression -> Expression) -> Expression -> Expression
forall a b. (a -> b) -> a -> b
$ (Expression
x Expression -> Expression -> Expression
:*: Expression
z) Expression -> Expression -> Expression
:/: Expression
y
binary e :: Expression
e@((Expression
_ :/: Expression
0) :/: Expression
_) = Expression
e
binary e :: Expression
e@((Expression
_ :/: Expression
_) :/: Expression
0) = Expression
e
binary ((Expression
x :/: Expression
y) :/: Expression
z) = Expression -> Expression
simplify (Expression -> Expression) -> Expression -> Expression
forall a b. (a -> b) -> a -> b
$ Expression
x Expression -> Expression -> Expression
:/: (Expression
y Expression -> Expression -> Expression
:*: Expression
z)
binary (Number Integer
n :/: Number Integer
m) = Integer -> Integer -> Expression
reduceRatio Integer
n Integer
m
-- Fold exponentiation.
binary e :: Expression
e@(Number Integer
0 :**: Number Integer
0) = Expression
e
binary (Number Integer
_ :**: Number Integer
0) = Integer -> Expression
Number Integer
1
binary (Number Integer
1 :**: Expression
_) = Integer -> Expression
Number Integer
1
binary (Number Integer
n :**: Number Integer
m)
  | Integer
m Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
0 = Integer -> Expression
Number (Integer
n Integer -> Integer -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^ Integer
m)
  | Bool
otherwise = Integer -> Expression
Number Integer
1 Expression -> Expression -> Expression
:/: Integer -> Expression
Number (Integer
n Integer -> Integer -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^ (-Integer
m))
binary ((Number Integer
n :/: Number Integer
m) :**: Number Integer
k)
  | Integer
k Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
0 = Integer -> Expression
Number (Integer
n Integer -> Integer -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^ Integer
k) Expression -> Expression -> Expression
:/: Integer -> Expression
Number (Integer
m Integer -> Integer -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^ Integer
k)
  | Bool
otherwise = Integer -> Expression
Number (Integer
m Integer -> Integer -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^ (-Integer
k)) Expression -> Expression -> Expression
:/: Integer -> Expression
Number (Integer
n Integer -> Integer -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^ (-Integer
k))
binary e :: Expression
e@(Number Integer
n :**: (Number Integer
m :/: Number Integer
k))
  | (Just Integer
l) <- Integer -> Integer -> Maybe Integer
root Integer
n Integer
k, Integer
m Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
0 = Integer -> Expression
Number (Integer
l Integer -> Integer -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^ Integer
m)
  | (Just Integer
l) <- Integer -> Integer -> Maybe Integer
root Integer
n Integer
k, Integer
m Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
0 = Expression
1 Expression -> Expression -> Expression
:/: Integer -> Expression
Number (Integer
l Integer -> Integer -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^ (-Integer
m))
  | Bool
otherwise = Expression
e
binary e :: Expression
e@((Number Integer
n :/: Number Integer
m) :**: (Number Integer
k :/: Number Integer
l))
  | (Just Integer
n', Just Integer
m') <- (Integer -> Integer -> Maybe Integer
root Integer
n Integer
l, Integer -> Integer -> Maybe Integer
root Integer
m Integer
l) = (Integer -> Expression
Number Integer
n' Expression -> Expression -> Expression
:/: Integer -> Expression
Number Integer
m') Expression -> Expression -> Expression
:**: Integer -> Expression
Number Integer
k
  | Bool
otherwise = Expression
e
-- Turn LogBase into Log.
binary (LogBase' Expression
b Expression
x) = Expression -> Expression
simplify (Expression -> Expression) -> Expression -> Expression
forall a b. (a -> b) -> a -> b
$ Expression -> Expression
Log' Expression
x Expression -> Expression -> Expression
:/: Expression -> Expression
Log' Expression
b
binary Expression
e = Expression
e

-- | Simplify integer ratios.  Basically turns them into integers if possible,
-- and if not, reduce the fractions so that the denominator and numerator
-- do not have a common factor.
reduceRatio :: Integer -> Integer -> Expression
reduceRatio :: Integer -> Integer -> Expression
reduceRatio Integer
n Integer
0 = Integer -> Expression
Number Integer
n Expression -> Expression -> Expression
:/: Integer -> Expression
Number Integer
0
reduceRatio Integer
n Integer
1 = Integer -> Expression
Number Integer
n
reduceRatio Integer
n Integer
m
  | Integer
m Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
d = Integer -> Expression
Number (Integer
n Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`div` Integer
m)
  | Integer
m Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== -Integer
d = Integer -> Expression
Number (Integer
n Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`div` Integer
m)
  | Integer
n Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
0, Integer
m Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
0 = Integer -> Expression
Number (-(Integer
n Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`div` Integer
d)) Expression -> Expression -> Expression
:/: Integer -> Expression
Number (-(Integer
m Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`div` Integer
d))
  | Bool
otherwise = Integer -> Expression
Number (Integer
n Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`div` Integer
d) Expression -> Expression -> Expression
:/: Integer -> Expression
Number (Integer
m Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`div` Integer
d)
  where
    d :: Integer
d = Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
gcd Integer
n Integer
m

-- | Simplify an exponential of Euler's number.  I.e., simplify \(e^X\).
-- Only the exponent is given as an argument, while the return value is
-- the full simplified expression.
simplifyExp :: Expression -> Expression
simplifyExp :: Expression -> Expression
simplifyExp (Number Integer
0) = Integer -> Expression
Number Integer
1
simplifyExp (Log' Expression
x) = Expression
x
simplifyExp Expression
e = Expression -> Expression
Exp' Expression
e

-- | Simplify a logarithm.  I.e., simplify \(log X\).
-- Only the parameter \(X\) is given as an argument, while the return value is
-- the full simplified expression.
simplifyLog :: Expression -> Expression
simplifyLog :: Expression -> Expression
simplifyLog (Number Integer
1) = Integer -> Expression
Number Integer
0
simplifyLog (Exp' Expression
x) = Expression
x
simplifyLog Expression
e = Expression -> Expression
Log' Expression
e

-- | Simplify a sine.  I.e., simplify \(\sin X\).
-- Only the parameter \(X\) is given as an argument, while the return value is
-- the full simplified expression.
simplifySin :: Expression -> Expression
simplifySin :: Expression -> Expression
simplifySin (Number Integer
0) = Expression
0
simplifySin (Number Integer
_ :*: Expression
Pi') = Expression
0
simplifySin (Expression
Pi' :*: Number Integer
_) = Expression
0
simplifySin ((Number Integer
n :/: Expression
2) :*: Expression
Pi')
  | Integer -> Bool
forall a. Integral a => a -> Bool
even Integer
n = Expression
0
  | Integer -> Bool
forall a. Integral a => a -> Bool
odd ((Integer
n Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1) Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`div` Integer
2) = Expression
1
  | Bool
otherwise = -Expression
1
simplifySin (Expression
Pi' :*: (Number Integer
n :/: Expression
2))
  | Integer -> Bool
forall a. Integral a => a -> Bool
even Integer
n = Expression
0
  | Integer -> Bool
forall a. Integral a => a -> Bool
odd ((Integer
n Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1) Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`div` Integer
2) = Expression
1
  | Bool
otherwise = -Expression
1
simplifySin Expression
e = Expression -> Expression
Sin' Expression
e

-- | Simplify a cosine.  I.e., simplify \(\cos X\).
-- Only the parameter \(X\) is given as an argument, while the return value is
-- the full simplified expression.
simplifyCos :: Expression -> Expression
simplifyCos :: Expression -> Expression
simplifyCos (Number Integer
0) = Expression
1
simplifyCos (Number Integer
n :*: Expression
Pi') | Integer -> Bool
forall a. Integral a => a -> Bool
even Integer
n = Expression
1 | Integer -> Bool
forall a. Integral a => a -> Bool
odd Integer
n = -Expression
1
simplifyCos (Expression
Pi' :*: Number Integer
n) | Integer -> Bool
forall a. Integral a => a -> Bool
even Integer
n = Expression
1 | Integer -> Bool
forall a. Integral a => a -> Bool
odd Integer
n = -Expression
1
-- Any 2k/2 would have been simplified to k already.
simplifyCos ((Number Integer
_ :/: Expression
2) :*: Expression
Pi') = Expression
0
simplifyCos (Expression
Pi' :*: (Number Integer
_ :/: Expression
2)) = Expression
0
simplifyCos Expression
e = Expression -> Expression
Cos' Expression
e

-- | Simplify a tangent.  I.e., simplify \(\tan X\).
-- Only the parameter \(X\) is given as an argument, while the return value is
-- the full simplified expression.
simplifyTan :: Expression -> Expression
simplifyTan :: Expression -> Expression
simplifyTan (Number Integer
0) = Expression
0
simplifyTan Expression
e = Expression -> Expression
Tan' Expression
e