1300
|
1 |
(* Title: HOL/MiniML/Type.thy
|
|
2 |
ID: $Id$
|
2525
|
3 |
Author: Wolfgang Naraschewski and Tobias Nipkow
|
|
4 |
Copyright 1996 TU Muenchen
|
1300
|
5 |
|
|
6 |
MiniML-types and type substitutions.
|
|
7 |
*)
|
|
8 |
|
|
9 |
Type = Maybe +
|
|
10 |
|
|
11 |
(* new class for structures containing type variables *)
|
2525
|
12 |
axclass type_struct < term
|
|
13 |
|
1300
|
14 |
|
|
15 |
(* type expressions *)
|
|
16 |
datatype
|
1476
|
17 |
typ = TVar nat | "->" typ typ (infixr 70)
|
1300
|
18 |
|
2525
|
19 |
(* type schemata *)
|
|
20 |
datatype
|
|
21 |
type_scheme = FVar nat | BVar nat | "=->" type_scheme type_scheme (infixr 70)
|
|
22 |
|
|
23 |
|
|
24 |
(* embedding types into type schemata *)
|
|
25 |
consts
|
|
26 |
mk_scheme :: typ => type_scheme
|
|
27 |
|
|
28 |
primrec mk_scheme typ
|
|
29 |
"mk_scheme (TVar n) = (FVar n)"
|
|
30 |
"mk_scheme (t1 -> t2) = ((mk_scheme t1) =-> (mk_scheme t2))"
|
|
31 |
|
|
32 |
|
|
33 |
instance typ::type_struct
|
|
34 |
instance type_scheme::type_struct
|
|
35 |
instance list::(type_struct)type_struct
|
|
36 |
instance fun::(term,type_struct)type_struct
|
|
37 |
|
|
38 |
|
|
39 |
(* free_tv s: the type variables occuring freely in the type structure s *)
|
|
40 |
|
|
41 |
consts
|
|
42 |
free_tv :: ['a::type_struct] => nat set
|
|
43 |
|
|
44 |
primrec free_tv typ
|
|
45 |
free_tv_TVar "free_tv (TVar m) = {m}"
|
|
46 |
free_tv_Fun "free_tv (t1 -> t2) = (free_tv t1) Un (free_tv t2)"
|
|
47 |
|
|
48 |
primrec free_tv type_scheme
|
|
49 |
"free_tv (FVar m) = {m}"
|
|
50 |
"free_tv (BVar m) = {}"
|
|
51 |
"free_tv (S1 =-> S2) = (free_tv S1) Un (free_tv S2)"
|
|
52 |
|
|
53 |
primrec free_tv list
|
|
54 |
"free_tv [] = {}"
|
|
55 |
"free_tv (x#l) = (free_tv x) Un (free_tv l)"
|
|
56 |
|
2625
|
57 |
|
2525
|
58 |
(* executable version of free_tv: Implementation with lists *)
|
|
59 |
consts
|
|
60 |
free_tv_ML :: ['a::type_struct] => nat list
|
|
61 |
|
|
62 |
primrec free_tv_ML type_scheme
|
|
63 |
"free_tv_ML (FVar m) = [m]"
|
|
64 |
"free_tv_ML (BVar m) = []"
|
|
65 |
"free_tv_ML (S1 =-> S2) = (free_tv_ML S1) @ (free_tv_ML S2)"
|
|
66 |
|
|
67 |
primrec free_tv_ML list
|
|
68 |
"free_tv_ML [] = []"
|
|
69 |
"free_tv_ML (x#l) = (free_tv_ML x) @ (free_tv_ML l)"
|
|
70 |
|
|
71 |
|
|
72 |
(* new_tv s n computes whether n is a new type variable w.r.t. a type
|
|
73 |
structure s, i.e. whether n is greater than any type variable
|
|
74 |
occuring in the type structure *)
|
|
75 |
constdefs
|
|
76 |
new_tv :: [nat,'a::type_struct] => bool
|
|
77 |
"new_tv n ts == ! m. m:(free_tv ts) --> m<n"
|
|
78 |
|
|
79 |
|
|
80 |
(* bound_tv s: the type variables occuring bound in the type structure s *)
|
|
81 |
|
|
82 |
consts
|
|
83 |
bound_tv :: ['a::type_struct] => nat set
|
|
84 |
|
|
85 |
primrec bound_tv type_scheme
|
|
86 |
"bound_tv (FVar m) = {}"
|
|
87 |
"bound_tv (BVar m) = {m}"
|
|
88 |
"bound_tv (S1 =-> S2) = (bound_tv S1) Un (bound_tv S2)"
|
|
89 |
|
|
90 |
primrec bound_tv list
|
|
91 |
"bound_tv [] = {}"
|
|
92 |
"bound_tv (x#l) = (bound_tv x) Un (bound_tv l)"
|
|
93 |
|
|
94 |
|
|
95 |
(* minimal new free / bound variable *)
|
|
96 |
|
|
97 |
consts
|
|
98 |
min_new_bound_tv :: 'a::type_struct => nat
|
|
99 |
|
|
100 |
primrec min_new_bound_tv type_scheme
|
|
101 |
"min_new_bound_tv (FVar n) = 0"
|
|
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)"
|
|
104 |
|
|
105 |
|
|
106 |
(* substitutions *)
|
|
107 |
|
|
108 |
(* type variable substitution *)
|
1300
|
109 |
types
|
1476
|
110 |
subst = nat => typ
|
1300
|
111 |
|
|
112 |
(* identity *)
|
1557
|
113 |
constdefs
|
1476
|
114 |
id_subst :: subst
|
1557
|
115 |
"id_subst == (%n.TVar n)"
|
1300
|
116 |
|
|
117 |
(* extension of substitution to type structures *)
|
|
118 |
consts
|
2525
|
119 |
app_subst :: [subst, 'a::type_struct] => 'a::type_struct ("$")
|
1300
|
120 |
|
2525
|
121 |
primrec app_subst typ
|
|
122 |
app_subst_TVar "$ S (TVar n) = S n"
|
|
123 |
app_subst_Fun "$ S (t1 -> t2) = ($ S t1) -> ($ S t2)"
|
|
124 |
|
|
125 |
primrec app_subst type_scheme
|
|
126 |
"$ S (FVar n) = mk_scheme (S n)"
|
|
127 |
"$ S (BVar n) = (BVar n)"
|
|
128 |
"$ S (sch1 =-> sch2) = ($ S sch1) =-> ($ S sch2)"
|
1604
|
129 |
|
1300
|
130 |
defs
|
2525
|
131 |
app_subst_list "$ S == map ($ S)"
|
1300
|
132 |
|
|
133 |
(* domain of a substitution *)
|
1557
|
134 |
constdefs
|
1476
|
135 |
dom :: subst => nat set
|
2525
|
136 |
"dom S == {n. S n ~= TVar n}"
|
1300
|
137 |
|
2525
|
138 |
(* codomain of a substitution: the introduced variables *)
|
|
139 |
|
1557
|
140 |
constdefs
|
1575
|
141 |
cod :: subst => nat set
|
2525
|
142 |
"cod S == (UN m:dom S. (free_tv (S m)))"
|
1300
|
143 |
|
|
144 |
defs
|
2525
|
145 |
free_tv_subst "free_tv S == (dom S) Un (cod S)"
|
1300
|
146 |
|
2525
|
147 |
|
1300
|
148 |
(* unification algorithm mgu *)
|
|
149 |
consts
|
2525
|
150 |
mgu :: [typ,typ] => subst option
|
1300
|
151 |
rules
|
2525
|
152 |
mgu_eq "mgu t1 t2 = Some U ==> $U t1 = $U t2"
|
|
153 |
mgu_mg "[| (mgu t1 t2) = Some U; $S t1 = $S t2 |] ==>
|
|
154 |
? R. S = $R o U"
|
|
155 |
mgu_Some "$S t1 = $S t2 ==> ? U. mgu t1 t2 = Some U"
|
|
156 |
mgu_free "mgu t1 t2 = Some U ==> \
|
|
157 |
\ (free_tv U) <= (free_tv t1) Un (free_tv t2)"
|
1300
|
158 |
|
|
159 |
end
|