1300
|
1 |
(* Title: MiniML.thy
|
|
2 |
Author: Thomas Stauner
|
|
3 |
Copyright 1995 TU Muenchen
|
|
4 |
|
|
5 |
Recursive definition of type inference algorithm I for Mini_ML.
|
|
6 |
*)
|
|
7 |
|
|
8 |
I = W +
|
|
9 |
|
|
10 |
consts
|
1476
|
11 |
I :: [expr, typ list, nat, subst] => result_W
|
1300
|
12 |
|
|
13 |
primrec I expr
|
1900
|
14 |
"I (Var i) a n s = (if i < length a then Ok(s, nth i a, n)
|
1300
|
15 |
else Fail)"
|
1900
|
16 |
"I (Abs e) a n s = ( (s,t,m) := I e ((TVar n)#a) (Suc n) s;
|
1400
|
17 |
Ok(s, TVar n -> t, m) )"
|
1900
|
18 |
"I (App e1 e2) a n s =
|
1476
|
19 |
( (s1,t1,m1) := I e1 a n s;
|
|
20 |
(s2,t2,m2) := I e2 a m1 s1;
|
|
21 |
u := mgu ($s2 t1) ($s2 t2 -> TVar m2);
|
|
22 |
Ok($u o s2, TVar m2, Suc m2) )"
|
1300
|
23 |
end
|