src/HOL/MiniML/W.thy
 changeset 2525 477c05586286 parent 1900 c7a869229091 child 4502 337c073de95e
```--- 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
+   Author:    Wolfgang Naraschewski and Tobias Nipkow

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```