9 |
9 |
10 consts |
10 consts |
11 I :: [expr, typ list, nat, subst] => result_W |
11 I :: [expr, typ list, nat, subst] => result_W |
12 |
12 |
13 primrec I expr |
13 primrec I expr |
14 I_Var "I (Var i) a n s = (if i < length a then Ok(s, nth i a, n) |
14 "I (Var i) a n s = (if i < length a then Ok(s, nth i a, n) |
15 else Fail)" |
15 else Fail)" |
16 I_Abs "I (Abs e) a n s = ( (s,t,m) := I e ((TVar n)#a) (Suc n) s; |
16 "I (Abs e) a n s = ( (s,t,m) := I e ((TVar n)#a) (Suc n) s; |
17 Ok(s, TVar n -> t, m) )" |
17 Ok(s, TVar n -> t, m) )" |
18 I_App "I (App e1 e2) a n s = |
18 "I (App e1 e2) a n s = |
19 ( (s1,t1,m1) := I e1 a n s; |
19 ( (s1,t1,m1) := I e1 a n s; |
20 (s2,t2,m2) := I e2 a m1 s1; |
20 (s2,t2,m2) := I e2 a m1 s1; |
21 u := mgu ($s2 t1) ($s2 t2 -> TVar m2); |
21 u := mgu ($s2 t1) ($s2 t2 -> TVar m2); |
22 Ok($u o s2, TVar m2, Suc m2) )" |
22 Ok($u o s2, TVar m2, Suc m2) )" |
23 end |
23 end |