等式や不等式を解くやつをもっとかしこくする

[kmyk]

Description / 説明

@hotman78 が #135 で src/Jikka/Core/Convert/EqualitySolving.hs を足してくれた。整数についてはそこそこ動く。しかし全部をやりきったわけではないはずで、さらなる改善の余地はある。

例:

• b >= a や b > a を a <= b や a < b に直す。>= と > のことは考えなくてよくなって楽
  • a <= b を a < b || a == b にするとか a < b を a <= b && a != b にするとかは、するべきかすべきでないか不明
• 等号の対称律を使った変換。つまり左右を入れ替える。複雑な式を左辺に集めて定数を右辺に集めることにしておくと他の規則が書きやすいはず
• 組み込み関数の単射性を用いた最適化。単射 f に対し f(a) = f(b) があったら a = b にできる
  • 整数の場合は ... = 0 に揃えられてるので f(a) - f(b) = 0 や - f(a) + f(b) = 0 を a - b = 0 にするやつも
  • もう一方がすでに計算済みの場合にもうまくやる。たとえば - a = - b を a = b にできるだけでなく - a = 0 も a = 0 にできる