--- a/src/HOL/MiniML/W.thy Fri Jan 17 18:35:44 1997 +0100
+++ b/src/HOL/MiniML/W.thy Fri Jan 17 18:50:04 1997 +0100
@@ -1,28 +1,38 @@
(* Title: HOL/MiniML/W.thy
ID: $Id$
- Author: Dieter Nazareth and Tobias Nipkow
- Copyright 1995 TU Muenchen
+ Author: Wolfgang Naraschewski and Tobias Nipkow
+ Copyright 1996 TU Muenchen
Type inference algorithm W
*)
+
W = MiniML +
types
- result_W = "(subst * typ * nat)maybe"
+ result_W = "(subst * typ * nat)option"
(* type inference algorithm W *)
+
consts
- W :: [expr, typ list, nat] => result_W
+ W :: [expr, ctxt, nat] => result_W
primrec W expr
- "W (Var i) a n = (if i < length a then Ok(id_subst, nth i a, n)
- else Fail)"
- "W (Abs e) a n = ( (s,t,m) := W e ((TVar n)#a) (Suc n);
- Ok(s, (s n) -> t, m) )"
- "W (App e1 e2) a n =
- ( (s1,t1,m1) := W e1 a n;
- (s2,t2,m2) := W e2 ($s1 a) m1;
- u := mgu ($s2 t1) (t2 -> (TVar m2));
- Ok( $u o $s2 o s1, $u (TVar m2), Suc m2) )"
+ "W (Var i) A n =
+ (if i < length A then Some( id_subst,
+ bound_typ_inst (%b. TVar(b+n)) (nth i A),
+ n + (min_new_bound_tv (nth i A)) )
+ else None)"
+
+ "W (Abs e) A n = ( (S,t,m) := W e ((FVar n)#A) (Suc n);
+ Some( S, (S n) -> t, m) )"
+
+ "W (App e1 e2) A n = ( (S1,t1,m1) := W e1 A n;
+ (S2,t2,m2) := W e2 ($S1 A) m1;
+ U := mgu ($S2 t1) (t2 -> (TVar m2));
+ Some( $U o $S2 o S1, U m2, Suc m2) )"
+
+ "W (LET e1 e2) A n = ( (S1,t1,m1) := W e1 A n;
+ (S2,t2,m2) := W e2 ((gen ($S1 A) t1)#($S1 A)) m1;
+ Some( $S2 o S1, t2, m2) )"
end