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
|
|
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
|