equal
deleted
inserted
replaced
11 types |
11 types |
12 result_W = "(subst * type_expr * nat)maybe" |
12 result_W = "(subst * type_expr * nat)maybe" |
13 |
13 |
14 (* type inference algorithm W *) |
14 (* type inference algorithm W *) |
15 consts |
15 consts |
16 W :: "[expr, type_expr list, nat] => result_W" |
16 W :: [expr, type_expr list, nat] => result_W |
17 |
17 |
18 primrec W expr |
18 primrec W expr |
19 W_Var "W (Var i) a n = (if i < length a then Ok(id_subst, nth i a, n) |
19 W_Var "W (Var i) a n = (if i < length a then Ok(id_subst, nth i a, n) |
20 else Fail)" |
20 else Fail)" |
21 W_Abs "W (Abs e) a n = W e ((TVar n)#a) (Suc n) bind |
21 W_Abs "W (Abs e) a n = W e ((TVar n)#a) (Suc n) bind |