equal
deleted
inserted
replaced
|
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 |
|
11 I :: "[expr, type_expr list, nat, subst] => result_W" |
|
12 |
|
13 primrec I expr |
|
14 I_Var "I (Var i) a n s = (if i < length a then Ok(s, nth i a, n) |
|
15 else Fail)" |
|
16 I_Abs "I (Abs e) a n s = I e ((TVar n)#a) (Suc n) s bind |
|
17 (%(s,t,m). Ok(s, Fun (TVar n) t, m) )" |
|
18 I_App "I (App e1 e2) a n s = |
|
19 I e1 a n s bind |
|
20 (%(s1,t1,m1). I e2 a m1 s1 bind |
|
21 (%(s2,t2,m2). mgu ($s2 t1) (Fun ($s2 t2) (TVar m2)) bind |
|
22 (%u. Ok($u o s2, TVar m2, Suc m2) ) ))" |
|
23 |
|
24 end |