packages feed

egison-4.0.3: lib/math/normalize.egi

--
--
-- Term Rewriting
--
--

--mathNormalize := id
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 * π)) * $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 _ #π) * _ -> 0
        | $a * #`sin (mult $n #π / #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 [#π]) * $mr -> a *' (-1) ^ abs n *' mr
        | _ * #`cos (mult _ #π / #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