23 |
23 |
24 (* embedding types into type schemata *) |
24 (* embedding types into type schemata *) |
25 consts |
25 consts |
26 mk_scheme :: typ => type_scheme |
26 mk_scheme :: typ => type_scheme |
27 |
27 |
28 primrec mk_scheme typ |
28 primrec |
29 "mk_scheme (TVar n) = (FVar n)" |
29 "mk_scheme (TVar n) = (FVar n)" |
30 "mk_scheme (t1 -> t2) = ((mk_scheme t1) =-> (mk_scheme t2))" |
30 "mk_scheme (t1 -> t2) = ((mk_scheme t1) =-> (mk_scheme t2))" |
31 |
31 |
32 |
32 |
33 instance typ::type_struct |
33 instance typ::type_struct |
39 (* free_tv s: the type variables occuring freely in the type structure s *) |
39 (* free_tv s: the type variables occuring freely in the type structure s *) |
40 |
40 |
41 consts |
41 consts |
42 free_tv :: ['a::type_struct] => nat set |
42 free_tv :: ['a::type_struct] => nat set |
43 |
43 |
44 primrec free_tv typ |
44 primrec |
45 free_tv_TVar "free_tv (TVar m) = {m}" |
45 free_tv_TVar "free_tv (TVar m) = {m}" |
46 free_tv_Fun "free_tv (t1 -> t2) = (free_tv t1) Un (free_tv t2)" |
46 free_tv_Fun "free_tv (t1 -> t2) = (free_tv t1) Un (free_tv t2)" |
47 |
47 |
48 primrec free_tv type_scheme |
48 primrec |
49 "free_tv (FVar m) = {m}" |
49 "free_tv (FVar m) = {m}" |
50 "free_tv (BVar m) = {}" |
50 "free_tv (BVar m) = {}" |
51 "free_tv (S1 =-> S2) = (free_tv S1) Un (free_tv S2)" |
51 "free_tv (S1 =-> S2) = (free_tv S1) Un (free_tv S2)" |
52 |
52 |
53 primrec free_tv list |
53 primrec |
54 "free_tv [] = {}" |
54 "free_tv [] = {}" |
55 "free_tv (x#l) = (free_tv x) Un (free_tv l)" |
55 "free_tv (x#l) = (free_tv x) Un (free_tv l)" |
56 |
56 |
57 |
57 |
58 (* executable version of free_tv: Implementation with lists *) |
58 (* executable version of free_tv: Implementation with lists *) |
59 consts |
59 consts |
60 free_tv_ML :: ['a::type_struct] => nat list |
60 free_tv_ML :: ['a::type_struct] => nat list |
61 |
61 |
62 primrec free_tv_ML type_scheme |
62 primrec |
63 "free_tv_ML (FVar m) = [m]" |
63 "free_tv_ML (FVar m) = [m]" |
64 "free_tv_ML (BVar m) = []" |
64 "free_tv_ML (BVar m) = []" |
65 "free_tv_ML (S1 =-> S2) = (free_tv_ML S1) @ (free_tv_ML S2)" |
65 "free_tv_ML (S1 =-> S2) = (free_tv_ML S1) @ (free_tv_ML S2)" |
66 |
66 |
67 primrec free_tv_ML list |
67 primrec |
68 "free_tv_ML [] = []" |
68 "free_tv_ML [] = []" |
69 "free_tv_ML (x#l) = (free_tv_ML x) @ (free_tv_ML l)" |
69 "free_tv_ML (x#l) = (free_tv_ML x) @ (free_tv_ML l)" |
70 |
70 |
71 |
71 |
72 (* new_tv s n computes whether n is a new type variable w.r.t. a type |
72 (* new_tv s n computes whether n is a new type variable w.r.t. a type |
80 (* bound_tv s: the type variables occuring bound in the type structure s *) |
80 (* bound_tv s: the type variables occuring bound in the type structure s *) |
81 |
81 |
82 consts |
82 consts |
83 bound_tv :: ['a::type_struct] => nat set |
83 bound_tv :: ['a::type_struct] => nat set |
84 |
84 |
85 primrec bound_tv type_scheme |
85 primrec |
86 "bound_tv (FVar m) = {}" |
86 "bound_tv (FVar m) = {}" |
87 "bound_tv (BVar m) = {m}" |
87 "bound_tv (BVar m) = {m}" |
88 "bound_tv (S1 =-> S2) = (bound_tv S1) Un (bound_tv S2)" |
88 "bound_tv (S1 =-> S2) = (bound_tv S1) Un (bound_tv S2)" |
89 |
89 |
90 primrec bound_tv list |
90 primrec |
91 "bound_tv [] = {}" |
91 "bound_tv [] = {}" |
92 "bound_tv (x#l) = (bound_tv x) Un (bound_tv l)" |
92 "bound_tv (x#l) = (bound_tv x) Un (bound_tv l)" |
93 |
93 |
94 |
94 |
95 (* minimal new free / bound variable *) |
95 (* minimal new free / bound variable *) |
96 |
96 |
97 consts |
97 consts |
98 min_new_bound_tv :: 'a::type_struct => nat |
98 min_new_bound_tv :: 'a::type_struct => nat |
99 |
99 |
100 primrec min_new_bound_tv type_scheme |
100 primrec |
101 "min_new_bound_tv (FVar n) = 0" |
101 "min_new_bound_tv (FVar n) = 0" |
102 "min_new_bound_tv (BVar n) = Suc n" |
102 "min_new_bound_tv (BVar n) = Suc n" |
103 "min_new_bound_tv (sch1 =-> sch2) = max (min_new_bound_tv sch1) (min_new_bound_tv sch2)" |
103 "min_new_bound_tv (sch1 =-> sch2) = max (min_new_bound_tv sch1) (min_new_bound_tv sch2)" |
104 |
104 |
105 |
105 |
116 |
116 |
117 (* extension of substitution to type structures *) |
117 (* extension of substitution to type structures *) |
118 consts |
118 consts |
119 app_subst :: [subst, 'a::type_struct] => 'a::type_struct ("$") |
119 app_subst :: [subst, 'a::type_struct] => 'a::type_struct ("$") |
120 |
120 |
121 primrec app_subst typ |
121 primrec |
122 app_subst_TVar "$ S (TVar n) = S n" |
122 app_subst_TVar "$ S (TVar n) = S n" |
123 app_subst_Fun "$ S (t1 -> t2) = ($ S t1) -> ($ S t2)" |
123 app_subst_Fun "$ S (t1 -> t2) = ($ S t1) -> ($ S t2)" |
124 |
124 |
125 primrec app_subst type_scheme |
125 primrec |
126 "$ S (FVar n) = mk_scheme (S n)" |
126 "$ S (FVar n) = mk_scheme (S n)" |
127 "$ S (BVar n) = (BVar n)" |
127 "$ S (BVar n) = (BVar n)" |
128 "$ S (sch1 =-> sch2) = ($ S sch1) =-> ($ S sch2)" |
128 "$ S (sch1 =-> sch2) = ($ S sch1) =-> ($ S sch2)" |
129 |
129 |
130 defs |
130 defs |