Add Jikka.Core.Convert.EqualitySolving

[hotman78]

close #126

特にList周りについて合ってるのか不安なのですが、一人で悩んでも埒が明かなそうなのでpull requestとして投げさせて頂きました。

[hotman78]

作成中にわからない点がいくつか出てきてしまったので質問させていただいてよろしいでしょうか
a==b
を
a-b==0
に変える変換は<=等でも成り立つ気がしますがこれは別のファイルでやるべきということですか？

単射の関数として
例えば
(a^b)-(c^b)==0 を a-c に変える変換等は行うべきですか？

[kmyk]

<=等でも成り立つ気がしますがこれは別のファイルでやるべきということですか？

同じファイルでも別ファイルでもどちらでも構いません。やりやすい方で大丈夫です

(a^b)-(c^b)==0 を a-c に変える変換等は行うべきですか？

単射性を使った変換はなし (あるいは簡単にできるところまで) で大丈夫です

(#126 のチェックリストはとりあえず思い付いたものを列挙してみただけなので、リストにないものでも、あった方がよさそうなら足しておいてくれるとうれしい。逆に、リストに書かれてても、なくてもよさそうなものは無視してしまってください)

---

examples/dp_z-kubaru.py の変換が壊れてしまってるみたいです。
$ stack run convert examples/dp_z-kubaru.py とか $ python3 scripts/integration_test.py -k dp_z-kubaru とかすると詳細が出てくるので確認してみてほしい。

[kmyk]

この行は間違えていそう。
nil == nil の場合は Equal' _ a b | a == b -> Just LitTrue があるので大丈夫なのですが、たとえば nil == (let xs = nil in xs) みたいな場合に False になってしまいます。

[hotman78]

examples/dp_z-kubaru.pyの変換エラーですが、Jikka.Core.Convert.EqualitySolvingより少し上流で起こってる気がしてきました
例えば
return (-n)*(n+1)
が
return -n+n*n
に変換されてます
もうちょっと調べてみます

[kmyk]

(-n)*(n+1) を -n-n*n に変換するための rule は src/Jikka/Core/Convert/ArithmeticalExpr.hs にあって、その本体は src/Jikka/Core/Language/ArithmeticalExpr.hs にあります。その感じだとこいつらがバグってそう (すまん……)

[hotman78]

ありがとうございます！
おそらく原因特定できました。

[kmyk]

@hotman78 まだ Draft になってるけど、バグなく動いてそうだし、ひとまずマージしてしまうのはどうだろう？ まだやることがあったりなかったりするかもだけど、必要なら後から追加でやればよいので

[hotman78]

ありがとうございます！！
ちょうど単射のやつをどこまでやるか悩んでいた所なので、そうさせていだだきます！！

[kmyk]

マージしました