1300

1 
(* Title: HOL/MiniML/W.thy


2 
ID: $Id$


3 
Author: Dieter Nazareth and Tobias Nipkow


4 
Copyright 1995 TU Muenchen


5 


6 
Type inference algorithm W


7 
*)


8 


9 
W = MiniML +


10 


11 
types

1400

12 
result_W = "(subst * typ * nat)maybe"

1300

13 


14 
(* type inference algorithm W *)


15 
consts

1400

16 
W :: [expr, typ list, nat] => result_W

1300

17 


18 
primrec W expr


19 
W_Var "W (Var i) a n = (if i < length a then Ok(id_subst, nth i a, n)


20 
else Fail)"

1400

21 
W_Abs "W (Abs e) a n = ( (s,t,m) := W e ((TVar n)#a) (Suc n);


22 
Ok(s, (s n) > t, m) )"

1300

23 
W_App "W (App e1 e2) a n =

1400

24 
( (s1,t1,m1) := W e1 a n;

1402

25 
(s2,t2,m2) := W e2 ($s1 a) m1;


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


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

1300

28 
end
