型検査と制約解決：全体の手順

次の5段階になるかな。

1. 式（スクリプトコード）からデータフローグラフを作る。
2. データフローグラフをもとに、不等式版の型単一化を行い制約系（連立不等式系）を作る。
3. 制約系（連立不等式系）は論理式なので、推論により論理式を簡約する（より短く単純な形にする）。
4. 制約系を解いて解を求める。解がうまく求まらないなら、実行時チェック条件を書き出す。
5. 制約系の解と実行時チェック条件の情報を埋め込んだ式（スクリプトコード）を作る。

このなかで、データフローグラフを作る部分は色々と応用があるから汎用的な操作。不等式ベースの単一化も他の用途に流用できるかもしれない。

論理簡約は、やらなくてもなんとかなる。やっておけば、次の制約解決フェーズが楽なる。

制約解決の部分はバリエーションがある。とりあえず使えるものを作って、だんだんに精度を上げていけばいいだろう。