equal
deleted
inserted
replaced
|
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 |
|
12 result_W = "(subst * typ * nat)maybe" |
|
13 |
|
14 (* type inference algorithm W *) |
|
15 consts |
|
16 W :: [expr, typ list, nat] => result_W |
|
17 |
|
18 primrec W expr |
|
19 "W (Var i) a n = (if i < length a then Ok(id_subst, nth i a, n) |
|
20 else Fail)" |
|
21 "W (Abs e) a n = ( (s,t,m) := W e ((TVar n)#a) (Suc n); |
|
22 Ok(s, (s n) -> t, m) )" |
|
23 "W (App e1 e2) a n = |
|
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) )" |
|
28 end |