author | berghofe |
Fri, 24 Jul 1998 13:19:38 +0200 | |
changeset 5184 | 9b8547a9496a |
parent 4502 | 337c073de95e |
permissions | -rw-r--r-- |
2520 | 1 |
(* Title: HOL/W0/I.thy |
2 |
ID: $Id$ |
|
3 |
Author: Thomas Stauner |
|
4 |
Copyright 1995 TU Muenchen |
|
2518
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
5 |
|
2520 | 6 |
Recursive definition of type inference algorithm I for Mini_ML. |
2518
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 |
I = W + |
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 |
consts |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
12 |
I :: [expr, typ list, nat, subst] => result_W |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
13 |
|
5184 | 14 |
primrec |
4502 | 15 |
"I (Var i) a n s = (if i < length a then Ok(s, a!i, n) |
2518
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
16 |
else Fail)" |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
17 |
"I (Abs e) a n s = ( (s,t,m) := I e ((TVar n)#a) (Suc n) s; |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
18 |
Ok(s, TVar n -> t, m) )" |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
19 |
"I (App e1 e2) a n s = |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
20 |
( (s1,t1,m1) := I e1 a n s; |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
21 |
(s2,t2,m2) := I e2 a m1 s1; |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
22 |
u := mgu ($s2 t1) ($s2 t2 -> TVar m2); |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
23 |
Ok($u o s2, TVar m2, Suc m2) )" |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
24 |
end |