| author | oheimb |
| Wed, 12 Nov 1997 18:58:50 +0100 | |
| changeset 4223 | f60e3d2c81d3 |
| parent 2518 | bee082efaa46 |
| child 4502 | 337c073de95e |
| 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 |
|
|
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
18 |
primrec W expr |
|
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
19 |
"W (Var i) a n = (if i < length a then Ok(id_subst, nth i a, n) |
|
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
20 |
else Fail)" |
|
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); |
|
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
22 |
Ok(s, (s n) -> t, m) )" |
|
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 |