-- |
-- Module: Symtegration.Symbolic.Simplify.SymbolicFolding
-- Description: Folding of symbolic terms.
-- Copyright: Copyright 2025 Yoo Chung
-- License: Apache-2.0
-- Maintainer: dev@chungyc.org
--
-- This merges symbolic 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.
module Symtegration.Symbolic.Simplify.SymbolicFolding (simplify) where

import Symtegration.Symbolic

-- | Folds symbolic terms as much as it can to simplify expressions.
--
-- Assumes algebraic ring ordering has been applied.
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)

-- | Folds symbolic terms for unary expressions.
--
-- The arguments should already have been simplified.
unary :: Expression -> Expression
unary :: Expression -> Expression
unary (Negate' (Negate' Expression
x)) = Expression -> Expression
simplify Expression
x
unary (Negate' Expression
x) = (-Expression
1) Expression -> Expression -> Expression
forall a. Num a => a -> a -> a
* Expression
x
unary Expression
e = Expression
e

-- | Folds symbolic terms for binary expressions.
--
-- The arguments should already have been simplified.
binary :: Expression -> Expression
-- Fold addition.
binary :: Expression -> Expression
binary e :: Expression
e@(Expression
x :+: Negate' Expression
y)
  | Expression
x Expression -> Expression -> Bool
forall a. Eq a => a -> a -> Bool
== Expression
y = Integer -> Expression
Number Integer
0
  | Bool
otherwise = Expression
e
binary e :: Expression
e@(Negate' Expression
x :+: Expression
y)
  | Expression
x Expression -> Expression -> Bool
forall a. Eq a => a -> a -> Bool
== Expression
y = Integer -> Expression
Number Integer
0
  | Bool
otherwise = Expression
e
binary (Number Integer
0 :+: Expression
x) = Expression
x
binary (Expression
x :+: Number Integer
0) = Expression
x
binary e :: Expression
e@((Number Integer
n :*: Expression
x) :+: ((Number Integer
m :*: Expression
y) :+: Expression
z))
  | Expression
x Expression -> Expression -> Bool
forall a. Eq a => a -> a -> Bool
== Expression
y = Expression -> Expression
simplify (Expression -> Expression) -> Expression -> Expression
forall a b. (a -> b) -> a -> b
$ (Integer -> Expression
Number (Integer
m Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
n) Expression -> Expression -> Expression
:*: Expression
x) Expression -> Expression -> Expression
:+: Expression
z
  | Bool
otherwise = Expression
e
binary e :: Expression
e@((Number Integer
n :*: Expression
x) :+: (Expression
y :+: Expression
z))
  | Expression
x Expression -> Expression -> Bool
forall a. Eq a => a -> a -> Bool
== Expression
y = Expression -> Expression
simplify (Expression -> Expression) -> Expression -> Expression
forall a b. (a -> b) -> a -> b
$ (Integer -> Expression
Number (Integer
n Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1) Expression -> Expression -> Expression
:*: Expression
x) Expression -> Expression -> Expression
:+: Expression
z
  | Bool
otherwise = Expression
e
binary e :: Expression
e@(Expression
x :+: ((Number Integer
n :*: Expression
y) :+: Expression
z))
  | Expression
x Expression -> Expression -> Bool
forall a. Eq a => a -> a -> Bool
== Expression
y = Expression -> Expression
simplify (Integer -> Expression
Number (Integer
n Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1) Expression -> Expression -> Expression
:*: Expression
x) Expression -> Expression -> Expression
:+: Expression
z
  | Bool
otherwise = Expression
e
binary e :: Expression
e@((Number Integer
n :*: Expression
x) :+: (Number Integer
m :*: Expression
y))
  | Expression
x Expression -> Expression -> Bool
forall a. Eq a => a -> a -> Bool
== Expression
y = Expression -> Expression
simplify (Expression -> Expression) -> Expression -> Expression
forall a b. (a -> b) -> a -> b
$ Integer -> Expression
Number (Integer
n Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
m) Expression -> Expression -> Expression
:*: Expression
x
  | Bool
otherwise = Expression
e
binary e :: Expression
e@(Expression
x :+: (Number Integer
n :*: Expression
y))
  | Expression
x Expression -> Expression -> Bool
forall a. Eq a => a -> a -> Bool
== Expression
y = Expression -> Expression
simplify (Expression -> Expression) -> Expression -> Expression
forall a b. (a -> b) -> a -> b
$ Integer -> Expression
Number (Integer
n Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1) Expression -> Expression -> Expression
:*: Expression
x
  | Bool
otherwise = Expression
e
binary e :: Expression
e@((Number Integer
n :*: Expression
x) :+: Expression
y)
  | Expression
x Expression -> Expression -> Bool
forall a. Eq a => a -> a -> Bool
== Expression
y = Expression -> Expression
simplify (Expression -> Expression) -> Expression -> Expression
forall a b. (a -> b) -> a -> b
$ Integer -> Expression
Number (Integer
n Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1) Expression -> Expression -> Expression
:*: Expression
x
  | Bool
otherwise = Expression
e
binary e :: Expression
e@(Expression
x :+: (Expression
y :+: Expression
z))
  | Expression
x Expression -> Expression -> Bool
forall a. Eq a => a -> a -> Bool
== Expression
y = Expression -> Expression
simplify (Expression -> Expression) -> Expression -> Expression
forall a b. (a -> b) -> a -> b
$ Integer -> Expression
Number Integer
2 Expression -> Expression -> Expression
:*: Expression
x Expression -> Expression -> Expression
:+: Expression
z
  | Bool
otherwise = Expression
e
binary e :: Expression
e@(Expression
x :+: Expression
y)
  | Expression
x Expression -> Expression -> Bool
forall a. Eq a => a -> a -> Bool
== Expression
y = Expression -> Expression
simplify (Expression -> Expression) -> Expression -> Expression
forall a b. (a -> b) -> a -> b
$ Integer -> Expression
Number Integer
2 Expression -> Expression -> Expression
:*: Expression
x
  | Bool
otherwise = Expression
e
-- Fold multiplication.
binary (Number Integer
0 :*: Expression
_) = Integer -> Expression
Number Integer
0
binary (Expression
_ :*: Number Integer
0) = Integer -> Expression
Number Integer
0
binary (Expression
x :*: Number Integer
1) = Expression
x
binary (Number Integer
1 :*: Expression
x) = Expression
x
binary e :: Expression
e@(Expression
x :*: (Expression
y :**: Number Integer
n))
  | Expression
x Expression -> Expression -> Bool
forall a. Eq a => a -> a -> Bool
== Expression
y = Expression -> Expression
simplify (Expression -> Expression) -> Expression -> Expression
forall a b. (a -> b) -> a -> b
$ Expression
x Expression -> Expression -> Expression
:**: Integer -> Expression
Number (Integer
n Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1)
  | Bool
otherwise = Expression
e
binary e :: Expression
e@((Expression
x :**: Expression
y) :*: (Expression
x' :**: Expression
y'))
  | Expression
x Expression -> Expression -> Bool
forall a. Eq a => a -> a -> Bool
== Expression
x' = 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
y')
  | Bool
otherwise = Expression
e
binary e :: Expression
e@(Expression
x :*: ((Expression
y :**: Number Integer
n) :*: Expression
z))
  | Expression
x Expression -> Expression -> Bool
forall a. Eq a => a -> a -> Bool
== Expression
y = Expression -> Expression
simplify (Expression -> Expression) -> Expression -> Expression
forall a b. (a -> b) -> a -> b
$ (Expression
x Expression -> Expression -> Expression
:**: Integer -> Expression
Number (Integer
n Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1)) Expression -> Expression -> Expression
:*: Expression
z
  | Bool
otherwise = Expression
e
binary e :: Expression
e@((Expression
x :**: Number Integer
n) :*: (Expression
y :*: Expression
z))
  | Expression
x Expression -> Expression -> Bool
forall a. Eq a => a -> a -> Bool
== Expression
y = Expression -> Expression
simplify (Expression -> Expression) -> Expression -> Expression
forall a b. (a -> b) -> a -> b
$ (Expression
x Expression -> Expression -> Expression
:**: Integer -> Expression
Number (Integer
n Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1)) Expression -> Expression -> Expression
:*: Expression
z
  | Bool
otherwise = Expression
e
binary e :: Expression
e@(Expression
x :*: (Expression
y :*: Expression
z))
  | Expression
x Expression -> Expression -> Bool
forall a. Eq a => a -> a -> Bool
== Expression
y = Expression -> Expression
simplify (Expression -> Expression) -> Expression -> Expression
forall a b. (a -> b) -> a -> b
$ (Expression
x Expression -> Expression -> Expression
:**: Integer -> Expression
Number Integer
2) Expression -> Expression -> Expression
:*: Expression
z
  | Bool
otherwise = Expression
e
binary e :: Expression
e@(Expression
x :*: Expression
y)
  | Expression
x Expression -> Expression -> Bool
forall a. Eq a => a -> a -> Bool
== Expression
y = Expression -> Expression
simplify (Expression -> Expression) -> Expression -> Expression
forall a b. (a -> b) -> a -> b
$ Expression
x Expression -> Expression -> Expression
:**: Integer -> Expression
Number Integer
2
  | Bool
otherwise = Expression
e
-- Fold division.
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 ((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 (Expression
x :/: Number Integer
1) = Expression
x
binary (Expression
x :/: Number (-1)) = (-Expression
1) Expression -> Expression -> Expression
forall a. Num a => a -> a -> a
* Expression
x
-- Fold powers.
binary (Expression
_ :**: Number Integer
0) = Integer -> Expression
Number Integer
1
binary (Expression
x :**: Number Integer
1) = Expression
x
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)
-- Fold subtraction.
binary e :: Expression
e@(Expression
x :-: Expression
y)
  | Expression
x Expression -> Expression -> Bool
forall a. Eq a => a -> a -> Bool
== Expression
y = Integer -> Expression
Number Integer
0
  | Bool
otherwise = Expression
e
binary Expression
e = Expression
e