-- -- -- 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 * 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