author | wenzelm |
Fri, 04 Mar 1994 12:14:21 +0100 | |
changeset 277 | 4abe17e92130 |
parent 267 | ab78019b8ec8 |
child 386 | e9ba9f7e2542 |
permissions | -rw-r--r-- |
19 | 1 |
(* Title: Pure/sign.ML |
0 | 2 |
ID: $Id$ |
251 | 3 |
Author: Lawrence C Paulson and Markus Wenzel |
0 | 4 |
|
251 | 5 |
The abstract type "sg" of signatures. |
6 |
||
7 |
TODO: |
|
8 |
a clean modular sequential Sign.extend (using sg_ext list); |
|
0 | 9 |
*) |
10 |
||
19 | 11 |
signature SIGN = |
0 | 12 |
sig |
13 |
structure Symtab: SYMTAB |
|
14 |
structure Syntax: SYNTAX |
|
251 | 15 |
structure Type: TYPE |
143 | 16 |
sharing Symtab = Type.Symtab |
251 | 17 |
local open Type in |
18 |
type sg |
|
19 |
val rep_sg: sg -> |
|
20 |
{tsig: type_sig, |
|
21 |
const_tab: typ Symtab.table, |
|
22 |
syn: Syntax.syntax, |
|
23 |
stamps: string ref list} |
|
24 |
val subsig: sg * sg -> bool |
|
25 |
val eq_sg: sg * sg -> bool |
|
26 |
val print_sg: sg -> unit |
|
27 |
val pprint_sg: sg -> pprint_args -> unit |
|
28 |
val pretty_term: sg -> term -> Syntax.Pretty.T |
|
29 |
val pretty_typ: sg -> typ -> Syntax.Pretty.T |
|
30 |
val string_of_term: sg -> term -> string |
|
31 |
val string_of_typ: sg -> typ -> string |
|
32 |
val pprint_term: sg -> term -> pprint_args -> unit |
|
33 |
val pprint_typ: sg -> typ -> pprint_args -> unit |
|
34 |
val certify_typ: sg -> typ -> typ |
|
35 |
val certify_term: sg -> term -> term * typ * int |
|
36 |
val read_typ: sg * (indexname -> sort option) -> string -> typ |
|
37 |
val extend: sg -> string -> |
|
38 |
(class * class list) list * class list * |
|
39 |
(string list * int) list * |
|
40 |
(string * string list * string) list * |
|
41 |
(string list * (sort list * class)) list * |
|
42 |
(string list * string) list * Syntax.sext option -> sg |
|
43 |
val merge: sg * sg -> sg |
|
44 |
val pure: sg |
|
45 |
end |
|
0 | 46 |
end; |
47 |
||
251 | 48 |
functor SignFun(structure Syntax: SYNTAX and Type: TYPE): SIGN = |
143 | 49 |
struct |
0 | 50 |
|
51 |
structure Symtab = Type.Symtab; |
|
52 |
structure Syntax = Syntax; |
|
251 | 53 |
structure Pretty = Syntax.Pretty; |
54 |
structure Type = Type; |
|
55 |
open Type; |
|
0 | 56 |
|
143 | 57 |
|
251 | 58 |
(** datatype sg **) |
59 |
||
60 |
(*the "ref" in stamps ensures that no two signatures are identical -- it is |
|
61 |
impossible to forge a signature*) |
|
143 | 62 |
|
19 | 63 |
datatype sg = |
143 | 64 |
Sg of { |
251 | 65 |
tsig: type_sig, (*order-sorted signature of types*) |
143 | 66 |
const_tab: typ Symtab.table, (*types of constants*) |
67 |
syn: Syntax.syntax, (*syntax for parsing and printing*) |
|
68 |
stamps: string ref list}; (*unique theory indentifier*) |
|
0 | 69 |
|
70 |
fun rep_sg (Sg args) = args; |
|
71 |
||
206
0d624d1ba9cc
added subsig: sg * sg -> bool to test if one signature is contained in another.
nipkow
parents:
200
diff
changeset
|
72 |
|
251 | 73 |
fun subsig (Sg {stamps = s1, ...}, Sg {stamps = s2, ...}) = s1 subset s2; |
0 | 74 |
|
266 | 75 |
fun eq_sg (Sg {stamps = s1, ...}, Sg {stamps = s2, ...}) = eq_set (s1, s2); |
0 | 76 |
|
77 |
||
78 |
||
251 | 79 |
(** print signature **) |
80 |
||
81 |
fun print_sg sg = |
|
82 |
let |
|
83 |
fun prt_typ syn ty = Pretty.quote (Syntax.pretty_typ syn ty); |
|
84 |
||
85 |
fun pretty_sort [cl] = Pretty.str cl |
|
86 |
| pretty_sort cls = Pretty.str_list "{" "}" cls; |
|
87 |
||
88 |
fun pretty_subclass (cl, cls) = Pretty.block |
|
89 |
[Pretty.str (cl ^ " <"), Pretty.brk 1, pretty_sort cls]; |
|
90 |
||
91 |
fun pretty_default cls = Pretty.block |
|
92 |
[Pretty.str "default:", Pretty.brk 1, pretty_sort cls]; |
|
93 |
||
94 |
fun pretty_arg (ty, n) = Pretty.str (ty ^ " " ^ string_of_int n); |
|
95 |
||
96 |
fun pretty_abbr syn (ty, (vs, rhs)) = Pretty.block |
|
97 |
[prt_typ syn (Type (ty, map (fn v => TVar (v, [])) vs)), |
|
98 |
Pretty.str " =", Pretty.brk 1, prt_typ syn rhs]; |
|
99 |
||
100 |
fun pretty_arity ty (cl, []) = Pretty.block |
|
101 |
[Pretty.str (ty ^ " ::"), Pretty.brk 1, Pretty.str cl] |
|
102 |
| pretty_arity ty (cl, srts) = Pretty.block |
|
103 |
[Pretty.str (ty ^ " ::"), Pretty.brk 1, |
|
104 |
Pretty.list "(" ")" (map pretty_sort srts), |
|
105 |
Pretty.brk 1, Pretty.str cl]; |
|
106 |
||
107 |
fun pretty_coreg (ty, ars) = map (pretty_arity ty) ars; |
|
108 |
||
109 |
fun pretty_const syn (c, ty) = Pretty.block |
|
266 | 110 |
[Pretty.str (quote c ^ " ::"), Pretty.brk 1, prt_typ syn ty]; |
251 | 111 |
|
112 |
||
113 |
val Sg {tsig, const_tab, syn, stamps} = sg; |
|
114 |
val {classes, subclass, default, args, abbrs, coreg} = rep_tsig tsig; |
|
115 |
in |
|
116 |
Pretty.writeln (Pretty.strs ("stamps:" :: map ! stamps)); |
|
117 |
Pretty.writeln (Pretty.strs ("classes:" :: classes)); |
|
118 |
Pretty.writeln (Pretty.big_list "subclass:" (map pretty_subclass subclass)); |
|
119 |
Pretty.writeln (pretty_default default); |
|
120 |
Pretty.writeln (Pretty.big_list "types:" (map pretty_arg args)); |
|
121 |
Pretty.writeln (Pretty.big_list "abbrs:" (map (pretty_abbr syn) abbrs)); |
|
122 |
Pretty.writeln (Pretty.big_list "coreg:" (flat (map pretty_coreg coreg))); |
|
123 |
Pretty.writeln (Pretty.big_list "consts:" |
|
124 |
(map (pretty_const syn) (Symtab.alist_of const_tab))) |
|
125 |
end; |
|
126 |
||
127 |
||
128 |
fun pprint_sg (Sg {stamps, ...}) = |
|
129 |
Pretty.pprint (Pretty.str_list "{" "}" (map ! stamps)); |
|
130 |
||
131 |
||
132 |
||
133 |
(** pretty printing of terms and types **) |
|
134 |
||
135 |
fun pretty_term (Sg {syn, ...}) = Syntax.pretty_term syn; |
|
136 |
fun pretty_typ (Sg {syn, ...}) = Syntax.pretty_typ syn; |
|
137 |
||
138 |
fun string_of_term (Sg {syn, ...}) = Syntax.string_of_term syn; |
|
139 |
fun string_of_typ (Sg {syn, ...}) = Syntax.string_of_typ syn; |
|
140 |
||
141 |
fun pprint_term sg = Pretty.pprint o Pretty.quote o (pretty_term sg); |
|
142 |
fun pprint_typ sg = Pretty.pprint o Pretty.quote o (pretty_typ sg); |
|
0 | 143 |
|
144 |
||
169 | 145 |
|
251 | 146 |
(** certify types and terms **) |
147 |
||
148 |
(*errors are indicated by exception TYPE*) |
|
149 |
||
150 |
fun certify_typ (Sg {tsig, ...}) ty = cert_typ tsig ty; |
|
151 |
||
152 |
||
153 |
(* FIXME -> term.ML (?) *) |
|
154 |
fun mapfilter_atoms f (Abs (_, _, t)) = mapfilter_atoms f t |
|
155 |
| mapfilter_atoms f (t $ u) = mapfilter_atoms f t @ mapfilter_atoms f u |
|
156 |
| mapfilter_atoms f a = (case f a of Some y => [y] | None => []); |
|
0 | 157 |
|
251 | 158 |
fun certify_term (sg as Sg {tsig, const_tab, ...}) tm = |
159 |
let |
|
160 |
fun valid_const a T = |
|
161 |
(case Symtab.lookup (const_tab, a) of |
|
162 |
Some U => typ_instance (tsig, T, U) |
|
163 |
| _ => false); |
|
169 | 164 |
|
251 | 165 |
fun atom_err (Const (a, T)) = |
166 |
if valid_const a T then None |
|
167 |
else Some ("Illegal type for constant " ^ quote a ^ " :: " ^ |
|
168 |
quote (string_of_typ sg T)) |
|
169 |
| atom_err (Var ((x, i), _)) = |
|
170 |
if i < 0 then Some ("Negative index for Var " ^ quote x) else None |
|
171 |
| atom_err _ = None; |
|
172 |
||
169 | 173 |
|
251 | 174 |
val norm_tm = |
175 |
(case it_term_types (typ_errors tsig) (tm, []) of |
|
176 |
[] => map_term_types (norm_typ tsig) tm |
|
177 |
| errs => raise_type (cat_lines errs) [] [tm]); |
|
178 |
in |
|
179 |
(case mapfilter_atoms atom_err norm_tm of |
|
180 |
[] => (norm_tm, type_of norm_tm, maxidx_of_term norm_tm) |
|
181 |
| errs => raise_type (cat_lines errs) [] [norm_tm]) |
|
182 |
end; |
|
183 |
||
184 |
||
185 |
||
186 |
(** read types **) |
|
187 |
||
188 |
(*read and certify typ wrt a signature; errors are indicated by |
|
189 |
exception ERROR (with messages already printed)*) |
|
169 | 190 |
|
251 | 191 |
fun rd_typ tsig syn sort_of s = |
192 |
let |
|
193 |
val def_sort = defaultS tsig; |
|
194 |
val raw_ty = (*this may raise ERROR, too!*) |
|
195 |
Syntax.read_typ syn (fn x => if_none (sort_of x) def_sort) s; |
|
196 |
in |
|
197 |
cert_typ tsig raw_ty |
|
198 |
handle TYPE (msg, _, _) => error msg |
|
199 |
end |
|
200 |
handle ERROR => error ("The error(s) above occurred in type " ^ quote s); |
|
169 | 201 |
|
251 | 202 |
fun read_typ (Sg {tsig, syn, ...}, sort_of) s = rd_typ tsig syn sort_of s; |
203 |
||
204 |
||
205 |
||
206 |
(** extend signature **) |
|
207 |
||
208 |
(*errors are indicated by exception ERROR (with messages already printed)*) |
|
209 |
||
210 |
fun extend sg name (classes, default, types, abbrs, arities, consts, opt_sext) = |
|
211 |
let |
|
267 | 212 |
fun read_abbr syn (c, vs, rhs_src) = |
213 |
(c, (map (rpair 0) vs, varifyT (Syntax.read_typ syn (K []) rhs_src))) |
|
214 |
handle ERROR => error ("The error(s) above occurred in the rhs " ^ |
|
215 |
quote rhs_src ^ "\nof type abbreviation " ^ quote c); |
|
216 |
||
251 | 217 |
(*reset TVar indices to 0, renaming to preserve distinctness*) |
218 |
fun zero_tvar_idxs T = |
|
169 | 219 |
let |
220 |
val inxSs = typ_tvars T; |
|
221 |
val nms' = variantlist (map (#1 o #1) inxSs, []); |
|
251 | 222 |
val tye = map2 (fn ((v, S), a) => (v, TVar ((a, 0), S))) (inxSs, nms'); |
223 |
in |
|
224 |
typ_subst_TVars tye T |
|
225 |
end; |
|
169 | 226 |
|
227 |
(*read and check the type mentioned in a const declaration; zero type var |
|
228 |
indices because type inference requires it*) |
|
251 | 229 |
fun read_const tsig syn (c, s) = |
230 |
(c, zero_tvar_idxs (varifyT (rd_typ tsig syn (K None) s))) |
|
231 |
handle ERROR => error ("in declaration of constant " ^ quote c); |
|
169 | 232 |
|
0 | 233 |
|
251 | 234 |
val Sg {tsig, const_tab, syn, stamps} = sg; |
235 |
val xconsts = map #1 classes @ flat (map #1 types) @ map #1 abbrs @ |
|
236 |
flat (map #1 consts); |
|
237 |
val sext = if_none opt_sext Syntax.empty_sext; |
|
143 | 238 |
|
251 | 239 |
val tsig' = extend_tsig tsig (classes, default, types, arities); |
267 | 240 |
val tsig1 = ext_tsig_abbrs tsig' (map (read_abbr syn) abbrs); |
200 | 241 |
|
251 | 242 |
val syn1 = Syntax.extend syn (rd_typ tsig1 syn (K None)) |
243 |
(logical_types tsig1, xconsts, sext); |
|
143 | 244 |
|
251 | 245 |
val all_consts = flat (map (fn (cs, s) => map (rpair s) cs) |
246 |
(Syntax.constants sext @ consts)); |
|
169 | 247 |
|
277
4abe17e92130
fixed misfeature in Sign.extend: types of consts were read wrt. the new syntax;
wenzelm
parents:
267
diff
changeset
|
248 |
val const_tab1 = |
4abe17e92130
fixed misfeature in Sign.extend: types of consts were read wrt. the new syntax;
wenzelm
parents:
267
diff
changeset
|
249 |
Symtab.extend (K false) (const_tab, map (read_const tsig1 syn) all_consts) |
251 | 250 |
handle Symtab.DUPLICATE c |
251 |
=> error ("Constant " ^ quote c ^ " declared twice"); |
|
169 | 252 |
|
251 | 253 |
val stamps1 = |
254 |
if exists (equal name o !) stamps then |
|
255 |
error ("Theory already contains a " ^ quote name ^ " component") |
|
256 |
else stamps @ [ref name]; |
|
143 | 257 |
in |
251 | 258 |
Sg {tsig = tsig1, const_tab = const_tab1, syn = syn1, stamps = stamps1} |
143 | 259 |
end; |
0 | 260 |
|
261 |
||
251 | 262 |
|
263 |
(** merge signatures **) |
|
264 |
||
265 |
(*errors are indicated by exception TERM*) |
|
143 | 266 |
|
251 | 267 |
fun check_stamps stamps = |
268 |
(case duplicates (map ! stamps) of |
|
269 |
[] => stamps |
|
270 |
| dups => raise_term ("Attempt to merge different versions of theories " ^ |
|
271 |
commas (map quote dups)) []); |
|
143 | 272 |
|
251 | 273 |
fun merge (sg1, sg2) = |
274 |
if subsig (sg2, sg1) then sg1 |
|
275 |
else if subsig (sg1, sg2) then sg2 |
|
276 |
else |
|
277 |
(*neither is union already; must form union*) |
|
278 |
let |
|
279 |
val Sg {tsig = tsig1, const_tab = const_tab1, syn = syn1, |
|
280 |
stamps = stamps1} = sg1; |
|
281 |
val Sg {tsig = tsig2, const_tab = const_tab2, syn = syn2, |
|
282 |
stamps = stamps2} = sg2; |
|
283 |
||
284 |
val tsig = merge_tsigs (tsig1, tsig2); |
|
285 |
||
286 |
val const_tab = Symtab.merge (op =) (const_tab1, const_tab2) |
|
287 |
handle Symtab.DUPLICATE c => |
|
288 |
raise_term ("Incompatible types for constant " ^ quote c) []; |
|
289 |
||
290 |
val syn = Syntax.merge (logical_types tsig) syn1 syn2; |
|
291 |
||
292 |
val stamps = check_stamps (merge_lists stamps1 stamps2); |
|
293 |
in |
|
294 |
Sg {tsig = tsig, const_tab = const_tab, syn = syn, stamps = stamps} |
|
295 |
end; |
|
143 | 296 |
|
0 | 297 |
|
298 |
||
251 | 299 |
(** the Pure signature **) |
0 | 300 |
|
251 | 301 |
val sg0 = Sg {tsig = tsig0, const_tab = Symtab.null, |
302 |
syn = Syntax.type_syn, stamps = []}; |
|
0 | 303 |
|
251 | 304 |
val pure = extend sg0 "Pure" |
305 |
([("logic", [])], |
|
306 |
["logic"], |
|
307 |
[(["fun"], 2), |
|
308 |
(["prop"], 0), |
|
309 |
(Syntax.syntax_types, 0)], |
|
310 |
[], |
|
311 |
[(["fun"], ([["logic"], ["logic"]], "logic")), |
|
312 |
(["prop"], ([], "logic"))], |
|
313 |
([Syntax.constrainC], "'a::{} => 'a") :: Syntax.syntax_consts, |
|
314 |
Some Syntax.pure_sext); |
|
0 | 315 |
|
316 |
||
317 |
end; |
|
143 | 318 |