equal
deleted
inserted
replaced
12 classes |
12 classes |
13 type_struct < term |
13 type_struct < term |
14 |
14 |
15 (* type expressions *) |
15 (* type expressions *) |
16 datatype |
16 datatype |
17 type_expr = TVar nat | Fun type_expr type_expr |
17 typ = TVar nat | "->" typ typ (infixr 70) |
18 |
18 |
19 (* type variable substitution *) |
19 (* type variable substitution *) |
20 types |
20 types |
21 subst = nat => type_expr |
21 subst = nat => typ |
22 |
22 |
23 arities |
23 arities |
24 type_expr::type_struct |
24 typ::type_struct |
25 list::(type_struct)type_struct |
25 list::(type_struct)type_struct |
26 fun::(term,type_struct)type_struct |
26 fun::(term,type_struct)type_struct |
27 |
27 |
28 (* substitutions *) |
28 (* substitutions *) |
29 |
29 |
37 consts |
37 consts |
38 app_subst :: [subst, 'a::type_struct] => 'a::type_struct ("$") |
38 app_subst :: [subst, 'a::type_struct] => 'a::type_struct ("$") |
39 |
39 |
40 rules |
40 rules |
41 app_subst_TVar "$ s (TVar n) = s n" |
41 app_subst_TVar "$ s (TVar n) = s n" |
42 app_subst_Fun "$ s (Fun t1 t2) = Fun ($ s t1) ($ s t2)" |
42 app_subst_Fun "$ s (t1 -> t2) = ($ s t1) -> ($ s t2)" |
43 defs |
43 defs |
44 app_subst_list "$ s == map ($ s)" |
44 app_subst_list "$ s == map ($ s)" |
45 |
45 |
46 (* free_tv s: the type variables occuring freely in the type structure s *) |
46 (* free_tv s: the type variables occuring freely in the type structure s *) |
47 consts |
47 consts |
48 free_tv :: ['a::type_struct] => nat set |
48 free_tv :: ['a::type_struct] => nat set |
49 |
49 |
50 rules |
50 rules |
51 free_tv_TVar "free_tv (TVar m) = {m}" |
51 free_tv_TVar "free_tv (TVar m) = {m}" |
52 free_tv_Fun "free_tv (Fun t1 t2) = (free_tv t1) Un (free_tv t2)" |
52 free_tv_Fun "free_tv (t1 -> t2) = (free_tv t1) Un (free_tv t2)" |
53 free_tv_Nil "free_tv [] = {}" |
53 free_tv_Nil "free_tv [] = {}" |
54 free_tv_Cons "free_tv (x#l) = (free_tv x) Un (free_tv l)" |
54 free_tv_Cons "free_tv (x#l) = (free_tv x) Un (free_tv l)" |
55 |
55 |
56 (* domain of a substitution *) |
56 (* domain of a substitution *) |
57 consts |
57 consts |
76 defs |
76 defs |
77 new_tv_def "new_tv n ts == ! m. m:free_tv ts --> m<n" |
77 new_tv_def "new_tv n ts == ! m. m:free_tv ts --> m<n" |
78 |
78 |
79 (* unification algorithm mgu *) |
79 (* unification algorithm mgu *) |
80 consts |
80 consts |
81 mgu :: [type_expr,type_expr] => subst maybe |
81 mgu :: [typ,typ] => subst maybe |
82 rules |
82 rules |
83 mgu_eq "mgu t1 t2 = Ok u ==> $ u t1 = $ u t2" |
83 mgu_eq "mgu t1 t2 = Ok u ==> $u t1 = $u t2" |
84 mgu_mg "[| (mgu t1 t2) = Ok u; $ s t1 = $ s t2 |] ==> |
84 mgu_mg "[| (mgu t1 t2) = Ok u; $s t1 = $s t2 |] ==> |
85 ? r. s = ($ r) o u" |
85 ? r. s = $r o u" |
86 mgu_Ok "$ s t1 = $ s t2 ==> ? u. mgu t1 t2 = Ok u" |
86 mgu_Ok "$s t1 = $s t2 ==> ? u. mgu t1 t2 = Ok u" |
87 mgu_free "mgu t1 t2 = Ok u ==> free_tv u <= free_tv t1 Un free_tv t2" |
87 mgu_free "mgu t1 t2 = Ok u ==> free_tv u <= free_tv t1 Un free_tv t2" |
88 |
88 |
89 end |
89 end |
90 |
90 |