1300

1 
(* Title: MiniML.thy


2 
Author: Thomas Stauner


3 
Copyright 1995 TU Muenchen


4 


5 
Recursive definition of type inference algorithm I for Mini_ML.


6 
*)


7 


8 
I = W +


9 


10 
consts


11 
I :: "[expr, type_expr list, nat, subst] => result_W"


12 


13 
primrec I expr


14 
I_Var "I (Var i) a n s = (if i < length a then Ok(s, nth i a, n)


15 
else Fail)"


16 
I_Abs "I (Abs e) a n s = I e ((TVar n)#a) (Suc n) s bind


17 
(%(s,t,m). Ok(s, Fun (TVar n) t, m) )"


18 
I_App "I (App e1 e2) a n s =


19 
I e1 a n s bind


20 
(%(s1,t1,m1). I e2 a m1 s1 bind


21 
(%(s2,t2,m2). mgu ($s2 t1) (Fun ($s2 t2) (TVar m2)) bind


22 
(%u. Ok($u o s2, TVar m2, Suc m2) ) ))"


23 


24 
end
