egison-4.1.3: lib/math/normalize.egi

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

def mathNormalize $x :=
  if isInteger x
    then x
    else if containFunction 'rtu x
          then rewriteRuleForRtu (symbolNormalize x)
          else symbolNormalize x

--
-- rtu (include i and w)
--
def rewriteRuleForRtu := mapPolys rewriteRuleForRtuPoly
  where
    rewriteRuleForRtuPoly := mapPolys rewriteRuleForRtuPoly'
    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