author | paulson |
Fri, 12 May 2000 15:05:02 +0200 | |
changeset 8862 | 78643f8449c6 |
parent 5184 | 9b8547a9496a |
permissions | -rw-r--r-- |
2518
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
1 |
(* Title: HOL/MiniML/W.thy |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
2 |
ID: $Id$ |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
3 |
Author: Dieter Nazareth and Tobias Nipkow |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
4 |
Copyright 1995 TU Muenchen |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
5 |
|
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
6 |
Type inference algorithm W |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
7 |
*) |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
8 |
|
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
9 |
W = MiniML + |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
10 |
|
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
11 |
types |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
12 |
result_W = "(subst * typ * nat)maybe" |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
13 |
|
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
14 |
(* type inference algorithm W *) |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
15 |
consts |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
16 |
W :: [expr, typ list, nat] => result_W |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
17 |
|
5184 | 18 |
primrec |
4502 | 19 |
"W (Var i) a n = (if i < length a then Ok(id_subst, a!i, n) |
20 |
else Fail)" |
|
2518
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
21 |
"W (Abs e) a n = ( (s,t,m) := W e ((TVar n)#a) (Suc n); |
4502 | 22 |
Ok(s, (s n) -> t, m) )" |
2518
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
23 |
"W (App e1 e2) a n = |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
24 |
( (s1,t1,m1) := W e1 a n; |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
25 |
(s2,t2,m2) := W e2 ($s1 a) m1; |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
26 |
u := mgu ($s2 t1) (t2 -> (TVar m2)); |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
27 |
Ok( $u o $s2 o s1, $u (TVar m2), Suc m2) )" |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
28 |
end |