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

1400

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

1300

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)"

1400

16 
I_Abs "I (Abs e) a n s = ( (s,t,m) := I e ((TVar n)#a) (Suc n) s;


17 
Ok(s, TVar n > t, m) )"

1300

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

1400

19 
( (s1,t1,m1) := I e1 a n s;


20 
(s2,t2,m2) := I e2 a m1 s1;


21 
u := mgu ($s2 t1) ($s2 t2 > TVar m2);


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

1300

23 
end
