第６回

課題４

・type_check_exprの作り方

まあ実装ゲーです。レジュメの最後に載っている推論規則をコードに直せば終わり。（タプル・リストに対応させようと思ったら自分で考えるしかないですが）

たとえば推論規則

ーーーーーーーーーーーーーーーーーーーーーーーーーーー Γ├e_1 aop e_2:int,{t_1=int}∪{t_2=int}∪C_1∪C_2

をコードに直すには、この推論規則を次のように読みます。

(1)式e_1を型推論した結果導出された型と制約を(t_1,C_1)とし、

(2)式e_2を型推論した結果導出された型と制約を(t_2,C_2)とすると、

(3)式「e_1 aop e_2」の型は「int」で、制約は「{t_1=int}∪{t_2=int}∪C_1∪C_2」である。

つまり、再帰的にe_1,e_2にtype_check_exprを適用した結果をlet 〜 in式で(t_1,C_1),(t_2,C_2)とおいておき（別に置かなくてもできるけど、ごちゃごちゃする）、

型、制約の組として「(int,(t_1,int)::(t_2,int)::(C_1@C_2)」を返せばいいってこと。

具体的には以下（ADD）。 

   1   |ADD(e1,e2) ->
   2      let (t1,c1) = type_check_expr typeenv e1 in
   3      let (t2,c2) = type_check_expr typeenv e2 in
   4         (INT,t1::t2::(c1@c2))

まあ、SUBとかMULとかもこのパターンにORパターンでまとめて記述するといいと思うよ。

Categoryノート