egison-4.0.0: lib/math/normalize.egi
--
--
-- Term Rewriting
--
--
mathNormalize $x :=
if isInteger x
then x
else (foldr compose id (map 2#%1 (filter 2#(%2 x) rewriteRules))) x
rewriteRules :=
[ (rewriteRuleForI, 1#(containSymbol i %1))
, (rewriteRuleForWTerm, 1#(containSymbol w %1))
, (rewriteRuleForRtuTerm, 1#(containFunction `rtu %1))
, (rewriteRuleForPower, 1#(containFunction `(^) %1))
, (rewriteRuleForExp, 1#(containFunction `exp %1))
, (rewriteRuleForWPoly, 1#(containSymbol w %1))
, (rewriteRuleForRtuPoly, 1#(containFunction `rtu %1))
, (rewriteRuleForSqrt, 1#(containFunction `sqrt %1))
, (rewriteRuleForRt, 1#(containFunction `rt %1))
, (rewriteRuleForSin, 1#(containFunction `sin %1))
, (rewriteRuleForCos, 1#(containFunction `cos %1))
, (rewriteRuleForLog, 1#(containFunction `log %1))
, (rewriteRuleForCosToSin, 1#(containFunctionWithOrder `cos 2 %1))
, (rewriteRuleForD/d, 1#True) ]
--
-- i
--
rewriteRuleForI := rewriteRuleForITerm
rewriteRuleForITerm := 1#(mapTerms rewriteRuleForITerm' %1)
rewriteRuleForITerm' term :=
match term as mathExpr with
| $a * #i ^ (?isEven & $k) * $r -> a *' (-1) ^' quotient k 2 *' r
| $a * #i ^ $k * $r -> a *' (-1) ^' quotient k 2 *' r *' i
| _ -> term
--
-- w
--
rewriteRuleForW := 1#(compose rewriteRuleForWTerm rewriteRuleForWPoly %1)
rewriteRuleForWTerm := 1#(mapTerms rewriteRuleForWTerm' %1)
rewriteRuleForWPoly := 1#(mapPolys rewriteRuleForWPoly' %1)
rewriteRuleForWTerm' term :=
match term as mathExpr with
| $a * #w ^ (?(>= 3) & $k) * $r -> a *' r *' w ^' (k % 3)
| _ -> term
rewriteRuleForWPoly' poly :=
match poly as mathExpr with
| $a * #w ^ #2 * $mr + $b * #w * #mr + $pr ->
rewriteRuleForWPoly' (pr +' (-1) *' a *' mr +' (b - a) *' mr *' w)
| _ -> poly
--
-- rtu (include i and w)
--
rewriteRuleForRtu :=
compose
1#(mapTerms rewriteRuleForRtuTerm %1)
1#(mapPolys rewriteRuleForRtuPoly %1)
rewriteRuleForRtuTerm := 1#(mapTerms rewriteRuleForRtuTerm' %1)
rewriteRuleForRtuPoly := 1#(mapPolys rewriteRuleForRtuPoly' %1)
rewriteRuleForRtuTerm' term :=
match term as mathExpr with
| $a * #`rtu $n ^ (?(>= n) & $k) * $r -> a *' rtu n ^' (k % n) *' r
| _ -> term
rewriteRuleForRtuPoly' poly :=
match poly as mathExpr with
| $a * #rtu $n ^ #1 * $mr + (loop $i (2, #(n - 1))
(#a * #(rtu n) ^ #i * #mr + ...)
$pr) ->
rewriteRuleForRtuPoly' (pr +' (-1) *' a *' mr)
| _ -> poly
--
-- sqrt
--
rewriteRuleForSqrt := 1#(mapTerms rewriteRuleForSqrtTerm %1)
rewriteRuleForSqrtTerm term :=
match term as mathExpr with
| $a * #`sqrt $x * #`sqrt #x * $r -> rewriteRuleForSqrt (a *' x *' r)
| $a * #`sqrt (?isTerm & $x) * #`sqrt (?isTerm & $y) * $r ->
let d := gcd x y
(a1, x1) := fromMonomial (x / d)
(a2, y1) := fromMonomial (y / d)
in a *' d *' sqrt (a1 *' a2) *' sqrt x1 *' sqrt y1 *' r
| _ -> term
--
-- rt (include sqrt)
--
rewriteRuleForRt := 1#(mapTerms rewriteRuleForRtTerm %1)
rewriteRuleForRtTerm term :=
match term as mathExpr with
| $a * #`rt $n $x ^ (?(>= n) & $k) * $r ->
a *' x ^' quotient k n *' rt n x ^' (k % n) *' r
| _ -> term
--
-- exp
--
rewriteRuleForExp := 1#(mapTerms rewriteRuleForExpTerm %1)
rewriteRuleForExpTerm term :=
match term as mathExpr with
| $a * #`exp #0 * $r -> a *' r
| $a * #`exp #1 * $r -> a *' e *' r
| $a * #`exp (mult $x #(i * pi)) * $r -> a *' (-1) ^ x *' r
| $a * #`exp $x ^ (?(>= 2) & $n) * $r ->
rewriteRuleForExp (a *' exp (x * n) *' r)
| $a * #`exp $x * #`exp $y * $r -> rewriteRuleForExp (a *' exp (x + y) *' r)
| _ -> term
--
-- log
--
rewriteRuleForLog mExpr := mapTerms f mExpr
where
f term :=
match term as mathExpr with
| _ * #`log #1 * _ -> 0
| $a * #`log #e * $mr -> a *' mr
| _ -> term
--
-- power
--
rewriteRuleForPower := 1#(mapTerms rewriteRuleForPowerTerm %1)
rewriteRuleForPowerTerm term :=
match term as mathExpr with
| $a * #`(^) #1 _ ^ _ * $r -> rewriteRuleForPower (a *' r)
| $a * #`(^) $x $y ^ (?(>= 2) & $n) * $r ->
rewriteRuleForPower (a *' x ^ (y * n) *' r)
| $a * #`(^) $x $y * #`(^) #x $z * $r ->
rewriteRuleForPower (a *' x ^ (y + z) *' r)
| _ -> term
--
-- cos, sin
--
rewriteRuleForCosAndSin := 1#(mapPolys rewriteRuleForCosAndSinPoly %1)
rewriteRuleForCosAndSinExpr expr :=
match (expr, expr) as (mathExpr, mathExpr) with
| ( ($a * #`cos $x * $mr + $pr1) / $pr2
, ( _ * (#`cos #(x / 2) | #`sin #(x / 2)) * _ + _) / _
| _ / (_ * (#`cos #(x / 2) | #`sin #(x / 2)) * _ + _) ) ->
rewriteRuleForCosAndSinExpr
((a *' (cos (x / 2) ^ 2 -' sin (x / 2) ^ 2) *' mr +' pr1) /' pr2)
| ( ($a * #`sin $x * $mr + $pr1) / $pr2
, ( _ * (#`cos #(x / 2) | #`sin #(x / 2)) * _ + _) / _
| _ / (_ * (#`cos #(x / 2) | #`sin #(x / 2)) * _ + _) ) ->
rewriteRuleForCosAndSinExpr
((a *' 2 *' cos (x / 2) *' sin (x / 2) *' mr +' pr1) /' pr2)
| ( $pr2 / ($a * #`cos $x * $mr + $pr1)
, ( _ * (#`cos #(x / 2) | #`sin #(x / 2)) * _ + _) / _
| _ / (_ * (#`cos #(x / 2) | #`sin #(x / 2)) * _ + _) ) ->
rewriteRuleForCosAndSinExpr
(pr2 /' (a *' (cos (x / 2) ^ 2 -' sin (x / 2) ^ 2) *' mr +' pr1))
| ( $pr2 / ($a * #`sin $x * $mr + $pr1)
, ( _ * (#`cos #(x / 2) | #`sin #(x / 2)) * _ + _) / _
| _ / (_ * (#`cos #(x / 2) | #`sin #(x / 2)) * _ + _) ) ->
rewriteRuleForCosAndSinExpr
(pr2 /' (a *' 2 *' cos (x / 2) *' sin (x / 2) *' mr +' pr1))
| _ -> expr
rewriteRuleForCosAndSinPoly poly :=
match poly as mathExpr with
| $a * #`cos $x ^ #2 * $mr + #a * #`sin #x ^ #2 * #mr + $pr ->
rewriteRuleForCosAndSinPoly (pr +' a *' mr)
| $a * $mr + #(- a) * #`sin $x ^ #2 * #mr + $pr ->
rewriteRuleForCosAndSinPoly (pr +' a *' cos x ^ 2 *' mr)
| $a * $mr + #(- a) * #`cos $x ^ #2 * #mr + $pr ->
rewriteRuleForCosAndSinPoly (pr +' a *' sin x ^ 2 *' mr)
| _ -> poly
rewriteRuleForCosToSin := 1#(mapTerms rewriteRuleForCosToSinTerm' %1)
rewriteRuleForCosToSinTerm' term :=
match term as mathExpr with
| $a * #`cos $x ^ #2 * $mr ->
a *' (1 -' sin x ^ 2) *' rewriteRuleForCosToSinTerm' mr
| _ -> term
rewriteRuleForSin mExpr := mapTerms f mExpr
where
f term :=
match term as mathExpr with
| _ * #`sin #0 * _ -> 0
| _ * #`sin (mult _ #pi) * _ -> 0
| $a * #`sin (mult $n #pi / #2) * $mr ->
a *' (-1) ^ ((abs n - 1) / 2) *' mr
| _ -> term
rewriteRuleForCos mExpr := mapTerms f mExpr
where
f term :=
match term as mathExpr with
| $a * #`cos #0 * $mr -> a *' mr
| $a * #`cos (term $n [#pi]) * $mr -> a *' (-1) ^ abs n *' mr
| _ * #`cos (mult _ #pi / #2) * _ -> 0
| _ -> term
--
-- d
--
rewriteRuleForD := 1#(mapTerms rewriteRuleForDTerm %1)
rewriteRuleForDTerm term :=
match term as mathExpr with
| _ * #d _ * #d _ * _ -> 0
| _ -> term
--
-- d/d
--
rewriteRuleForD/d := 1#(mapPolys rewriteRuleForD/dPoly %1)
rewriteRuleForD/dPoly poly :=
match poly as mathExpr with
| $a * ($f & (func $g _ $arg $js)) ^ $n * $mr +
$b * func #g _ #arg ?1#(eqAs (multiset something) js %1) ^ #n * #mr + $pr ->
rewriteRuleForD/dPoly ((a + b) *' f ^ n *' mr +' pr)
| _ -> poly