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

1476

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

1300

17 


18 
primrec W expr

1900

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

1476

20 
else Fail)"

1900

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

1476

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

1900

23 
"W (App e1 e2) a n =

1476

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


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
