1300
|
1 |
(* Title: HOL/MiniML/W.thy
|
|
2 |
ID: $Id$
|
2525
|
3 |
Author: Wolfgang Naraschewski and Tobias Nipkow
|
|
4 |
Copyright 1996 TU Muenchen
|
1300
|
5 |
|
|
6 |
Type inference algorithm W
|
|
7 |
*)
|
|
8 |
|
2525
|
9 |
|
1300
|
10 |
W = MiniML +
|
|
11 |
|
|
12 |
types
|
2525
|
13 |
result_W = "(subst * typ * nat)option"
|
1300
|
14 |
|
|
15 |
(* type inference algorithm W *)
|
2525
|
16 |
|
1300
|
17 |
consts
|
2525
|
18 |
W :: [expr, ctxt, nat] => result_W
|
1300
|
19 |
|
|
20 |
primrec W expr
|
2525
|
21 |
"W (Var i) A n =
|
|
22 |
(if i < length A then Some( id_subst,
|
|
23 |
bound_typ_inst (%b. TVar(b+n)) (nth i A),
|
|
24 |
n + (min_new_bound_tv (nth i A)) )
|
|
25 |
else None)"
|
|
26 |
|
|
27 |
"W (Abs e) A n = ( (S,t,m) := W e ((FVar n)#A) (Suc n);
|
|
28 |
Some( S, (S n) -> t, m) )"
|
|
29 |
|
|
30 |
"W (App e1 e2) A n = ( (S1,t1,m1) := W e1 A n;
|
|
31 |
(S2,t2,m2) := W e2 ($S1 A) m1;
|
|
32 |
U := mgu ($S2 t1) (t2 -> (TVar m2));
|
|
33 |
Some( $U o $S2 o S1, U m2, Suc m2) )"
|
|
34 |
|
|
35 |
"W (LET e1 e2) A n = ( (S1,t1,m1) := W e1 A n;
|
|
36 |
(S2,t2,m2) := W e2 ((gen ($S1 A) t1)#($S1 A)) m1;
|
|
37 |
Some( $S2 o S1, t2, m2) )"
|
1300
|
38 |
end
|