author  wenzelm 
Sat, 11 Jun 2005 22:15:54 +0200  
changeset 16369  96d73621fabb 
parent 16339  b02b6da609c3 
child 16443  82a116532e3e 
permissions  rwrr 
1526  1 
(* Title: Pure/theory.ML 
2 
ID: $Id$ 

3 
Author: Lawrence C Paulson and Markus Wenzel 

4 

5025  5 
The abstract type "theory" of theories. 
1526  6 
*) 
16291  7 

3767
e2bb53d8dd26
moved theory stuff (add_defs etc.) here from drule.ML;
wenzelm
parents:
2979
diff
changeset

8 
signature BASIC_THEORY = 
e2bb53d8dd26
moved theory stuff (add_defs etc.) here from drule.ML;
wenzelm
parents:
2979
diff
changeset

9 
sig 
1526  10 
type theory 
11 
exception THEORY of string * theory list 

3996  12 
val rep_theory: theory > 
3814  13 
{sign: Sign.sg, 
16291  14 
defs: Defs.graph, 
16339  15 
axioms: term NameSpace.table, 
16 
oracles: ((Sign.sg * Object.T > term) * stamp) NameSpace.table, 

4019  17 
parents: theory list, 
18 
ancestors: theory list} 

3996  19 
val sign_of: theory > Sign.sg 
6188  20 
val is_draft: theory > bool 
3996  21 
val syn_of: theory > Syntax.syntax 
22 
val parents_of: theory > theory list 

4019  23 
val ancestors_of: theory > theory list 
3996  24 
val subthy: theory * theory > bool 
25 
val eq_thy: theory * theory > bool 

26 
val cert_axm: Sign.sg > string * term > string * term 

6311  27 
val read_def_axm: Sign.sg * (indexname > typ option) * (indexname > sort option) > 
28 
string list > string * string > string * term 

3996  29 
val read_axm: Sign.sg > string * string > string * term 
30 
val inferT_axm: Sign.sg > string * term > string * term 

3767
e2bb53d8dd26
moved theory stuff (add_defs etc.) here from drule.ML;
wenzelm
parents:
2979
diff
changeset

31 
end 
e2bb53d8dd26
moved theory stuff (add_defs etc.) here from drule.ML;
wenzelm
parents:
2979
diff
changeset

32 

e2bb53d8dd26
moved theory stuff (add_defs etc.) here from drule.ML;
wenzelm
parents:
2979
diff
changeset

33 
signature THEORY = 
e2bb53d8dd26
moved theory stuff (add_defs etc.) here from drule.ML;
wenzelm
parents:
2979
diff
changeset

34 
sig 
e2bb53d8dd26
moved theory stuff (add_defs etc.) here from drule.ML;
wenzelm
parents:
2979
diff
changeset

35 
include BASIC_THEORY 
16339  36 
val axioms_of: theory > (string * term) list 
37 
val all_axioms_of: theory > (string * term) list 

38 
val add_classes: (bstring * xstring list) list > theory > theory 

39 
val add_classes_i: (bstring * class list) list > theory > theory 

40 
val add_classrel: (xstring * xstring) list > theory > theory 

3996  41 
val add_classrel_i: (class * class) list > theory > theory 
8897  42 
val add_defsort: string > theory > theory 
3996  43 
val add_defsort_i: sort > theory > theory 
44 
val add_types: (bstring * int * mixfix) list > theory > theory 

4846  45 
val add_nonterminals: bstring list > theory > theory 
3996  46 
val add_tyabbrs: (bstring * string list * string * mixfix) list 
1526  47 
> theory > theory 
3996  48 
val add_tyabbrs_i: (bstring * string list * typ * mixfix) list 
1526  49 
> theory > theory 
8897  50 
val add_arities: (xstring * string list * string) list > theory > theory 
3996  51 
val add_arities_i: (string * sort list * sort) list > theory > theory 
52 
val add_consts: (bstring * string * mixfix) list > theory > theory 

53 
val add_consts_i: (bstring * typ * mixfix) list > theory > theory 

54 
val add_syntax: (bstring * string * mixfix) list > theory > theory 

55 
val add_syntax_i: (bstring * typ * mixfix) list > theory > theory 

56 
val add_modesyntax: string * bool > (bstring * string * mixfix) list > theory > theory 

57 
val add_modesyntax_i: string * bool > (bstring * typ * mixfix) list > theory > theory 

15747  58 
val del_modesyntax: string * bool > (bstring * string * mixfix) list > theory > theory 
59 
val del_modesyntax_i: string * bool > (bstring * typ * mixfix) list > theory > theory 

3996  60 
val add_trfuns: 
4344  61 
(string * (Syntax.ast list > Syntax.ast)) list * 
62 
(string * (term list > term)) list * 

63 
(string * (term list > term)) list * 

64 
(string * (Syntax.ast list > Syntax.ast)) list > theory > theory 

3996  65 
val add_trfunsT: 
4344  66 
(string * (bool > typ > term list > term)) list > theory > theory 
14645  67 
val add_advanced_trfuns: 
68 
(string * (Sign.sg > Syntax.ast list > Syntax.ast)) list * 

69 
(string * (Sign.sg > term list > term)) list * 

70 
(string * (Sign.sg > term list > term)) list * 

71 
(string * (Sign.sg > Syntax.ast list > Syntax.ast)) list > theory > theory 

72 
val add_advanced_trfunsT: 

73 
(string * (Sign.sg > bool > typ > term list > term)) list > theory > theory 

2693  74 
val add_tokentrfuns: 
6311  75 
(string * string * (string > string * real)) list > theory > theory 
76 
val add_mode_tokentrfuns: string > (string * (string > string * real)) list 

77 
> theory > theory 

4617  78 
val add_trrules: (xstring * string) Syntax.trrule list > theory > theory 
3996  79 
val add_trrules_i: Syntax.ast Syntax.trrule list > theory > theory 
80 
val add_axioms: (bstring * string) list > theory > theory 

81 
val add_axioms_i: (bstring * term) list > theory > theory 

4996  82 
val add_oracle: bstring * (Sign.sg * Object.T > term) > theory > theory 
14223
0ee05eef881b
Added support for making constants final, that is, ensuring that no
skalberg
parents:
14204
diff
changeset

83 
val add_finals: bool > string list > theory > theory 
0ee05eef881b
Added support for making constants final, that is, ensuring that no
skalberg
parents:
14204
diff
changeset

84 
val add_finals_i: bool > term list > theory > theory 
9320  85 
val add_defs: bool > (bstring * string) list > theory > theory 
86 
val add_defs_i: bool > (bstring * term) list > theory > theory 

3996  87 
val add_path: string > theory > theory 
4846  88 
val parent_path: theory > theory 
89 
val root_path: theory > theory 

11501  90 
val absolute_path: theory > theory 
16134
89ea482e1649
added qualified_names, no_base_names, custom_accesses, set_policy, restore_naming;
wenzelm
parents:
16113
diff
changeset

91 
val qualified_names: theory > theory 
89ea482e1649
added qualified_names, no_base_names, custom_accesses, set_policy, restore_naming;
wenzelm
parents:
16113
diff
changeset

92 
val no_base_names: theory > theory 
89ea482e1649
added qualified_names, no_base_names, custom_accesses, set_policy, restore_naming;
wenzelm
parents:
16113
diff
changeset

93 
val custom_accesses: (string list > string list list) > theory > theory 
89ea482e1649
added qualified_names, no_base_names, custom_accesses, set_policy, restore_naming;
wenzelm
parents:
16113
diff
changeset

94 
val set_policy: (string > bstring > string) * (string list > string list list) > 
89ea482e1649
added qualified_names, no_base_names, custom_accesses, set_policy, restore_naming;
wenzelm
parents:
16113
diff
changeset

95 
theory > theory 
89ea482e1649
added qualified_names, no_base_names, custom_accesses, set_policy, restore_naming;
wenzelm
parents:
16113
diff
changeset

96 
val restore_naming: theory > theory > theory 
16369  97 
val hide_classes: bool > xstring list > theory > theory 
98 
val hide_classes_i: bool > string list > theory > theory 

99 
val hide_types: bool > xstring list > theory > theory 

100 
val hide_types_i: bool > string list > theory > theory 

101 
val hide_consts: bool > xstring list > theory > theory 

102 
val hide_consts_i: bool > string list > theory > theory 

3996  103 
val add_name: string > theory > theory 
5862  104 
val copy: theory > theory 
6661  105 
val prep_ext: theory > theory 
3996  106 
val prep_ext_merge: theory list > theory 
4970  107 
val requires: theory > string > string > unit 
6369  108 
val assert_super: theory > theory > theory 
3996  109 
val pre_pure: theory 
1526  110 
end; 
111 

6188  112 
signature PRIVATE_THEORY = 
5642  113 
sig 
114 
include THEORY 

6546  115 
val init_data: Object.kind > (Object.T * (Object.T > Object.T) * (Object.T > Object.T) * 
12311  116 
(Object.T * Object.T > Object.T) * (Sign.sg > Object.T > unit)) > theory > theory 
5642  117 
val print_data: Object.kind > theory > unit 
118 
val get_data: Object.kind > (Object.T > 'a) > theory > 'a 

119 
val put_data: Object.kind > ('a > Object.T) > 'a > theory > theory 

120 
end; 

1526  121 

6188  122 
structure Theory: PRIVATE_THEORY = 
1526  123 
struct 
2206  124 

3996  125 

2206  126 
(** datatype theory **) 
1526  127 

128 
datatype theory = 

129 
Theory of { 

130 
sign: Sign.sg, 

16291  131 
defs: Defs.graph, 
16339  132 
axioms: term NameSpace.table, 
133 
oracles: ((Sign.sg * Object.T > term) * stamp) NameSpace.table, 

4019  134 
parents: theory list, 
135 
ancestors: theory list}; 

1526  136 

16291  137 
fun make_theory sign defs axioms oracles parents ancestors = 
138 
Theory {sign = sign, defs = defs, axioms = axioms, 

16190  139 
oracles = oracles, parents = parents, ancestors = ancestors}; 
3996  140 

1526  141 
fun rep_theory (Theory args) = args; 
142 

3996  143 
val sign_of = #sign o rep_theory; 
6188  144 
val is_draft = Sign.is_draft o sign_of; 
14645  145 
val syn_of = Sign.syn_of o sign_of; 
3996  146 
val parents_of = #parents o rep_theory; 
4019  147 
val ancestors_of = #ancestors o rep_theory; 
3996  148 

16339  149 
val axioms_of = Symtab.dest o #2 o #axioms o rep_theory; 
150 
fun all_axioms_of thy = List.concat (map axioms_of (thy :: ancestors_of thy)); 

151 

1526  152 
(*errors involving theories*) 
153 
exception THEORY of string * theory list; 

154 

155 
(*compare theories*) 

156 
val subthy = Sign.subsig o pairself sign_of; 

157 
val eq_thy = Sign.eq_sg o pairself sign_of; 

158 

6369  159 
(*check for some theory*) 
4970  160 
fun requires thy name what = 
10930  161 
if Sign.exists_stamp name (sign_of thy) then () 
4846  162 
else error ("Require theory " ^ quote name ^ " as an ancestor for " ^ what); 
1526  163 

6369  164 
fun assert_super thy1 thy2 = 
165 
if subthy (thy1, thy2) then thy2 

166 
else raise THEORY ("Not a super theory", [thy1, thy2]); 

167 

4846  168 
(*partial Pure theory*) 
9282
0181ac100520
Defs are now checked for circularity (if not overloaded).
nipkow
parents:
9280
diff
changeset

169 
val pre_pure = 
16339  170 
make_theory Sign.pre_pure Defs.empty NameSpace.empty_table NameSpace.empty_table [] []; 
1526  171 

172 

173 

174 
(** extend theory **) 

175 

3814  176 
(* extend logical part of a theory *) 
177 

16339  178 
fun err_dup_axms dups = error ("Duplicate axiom(s): " ^ commas_quote dups); 
179 
fun err_dup_oras dups = error ("Duplicate oracle(s): " ^ commas_quote dups); 

1526  180 

16339  181 
fun ext_theory thy ext_sg axms oras = 
1526  182 
let 
16291  183 
val Theory {sign, defs, axioms, oracles, parents, ancestors} = thy; 
184 
val draft = Sign.is_draft sign; 

16339  185 
val naming = Sign.naming_of sign; 
186 

187 
val axioms' = NameSpace.extend_table naming 

188 
(if draft then axioms else NameSpace.empty_table, axms) 

189 
handle Symtab.DUPS dups => err_dup_axms dups; 

190 
val oracles' = NameSpace.extend_table naming (oracles, oras) 

191 
handle Symtab.DUPS dups => err_dup_oras dups; 

192 

4019  193 
val (parents', ancestors') = 
16291  194 
if draft then (parents, ancestors) else ([thy], thy :: ancestors); 
195 
in make_theory (ext_sg sign) defs axioms' oracles' parents' ancestors' end; 

1526  196 

197 

198 
(* extend signature of a theory *) 

199 

16158
2c3565b74b7a
Removed final_consts from theory data. Now const_deps deals with final
obua
parents:
16134
diff
changeset

200 
fun ext_sign ext_sg args thy = ext_theory thy (ext_sg args) [] []; 
1526  201 

14645  202 
val add_classes = ext_sign Sign.add_classes; 
203 
val add_classes_i = ext_sign Sign.add_classes_i; 

204 
val add_classrel = ext_sign Sign.add_classrel; 

205 
val add_classrel_i = ext_sign Sign.add_classrel_i; 

206 
val add_defsort = ext_sign Sign.add_defsort; 

207 
val add_defsort_i = ext_sign Sign.add_defsort_i; 

208 
val add_types = ext_sign Sign.add_types; 

209 
val add_nonterminals = ext_sign Sign.add_nonterminals; 

210 
val add_tyabbrs = ext_sign Sign.add_tyabbrs; 

211 
val add_tyabbrs_i = ext_sign Sign.add_tyabbrs_i; 

212 
val add_arities = ext_sign Sign.add_arities; 

213 
val add_arities_i = ext_sign Sign.add_arities_i; 

214 
val add_consts = ext_sign Sign.add_consts; 

215 
val add_consts_i = ext_sign Sign.add_consts_i; 

216 
val add_syntax = ext_sign Sign.add_syntax; 

217 
val add_syntax_i = ext_sign Sign.add_syntax_i; 

218 
val add_modesyntax = curry (ext_sign Sign.add_modesyntax); 

219 
val add_modesyntax_i = curry (ext_sign Sign.add_modesyntax_i); 

15747  220 
val del_modesyntax = curry (ext_sign Sign.del_modesyntax); 
221 
val del_modesyntax_i = curry (ext_sign Sign.del_modesyntax_i); 

14645  222 
val add_trfuns = ext_sign Sign.add_trfuns; 
223 
val add_trfunsT = ext_sign Sign.add_trfunsT; 

224 
val add_advanced_trfuns = ext_sign Sign.add_advanced_trfuns; 

225 
val add_advanced_trfunsT = ext_sign Sign.add_advanced_trfunsT; 

226 
val add_tokentrfuns = ext_sign Sign.add_tokentrfuns; 

6311  227 
fun add_mode_tokentrfuns m = add_tokentrfuns o map (fn (s, f) => (m, s, f)); 
14645  228 
val add_trrules = ext_sign Sign.add_trrules; 
229 
val add_trrules_i = ext_sign Sign.add_trrules_i; 

230 
val add_path = ext_sign Sign.add_path; 

231 
val parent_path = add_path ".."; 

232 
val root_path = add_path "/"; 

233 
val absolute_path = add_path "//"; 

16134
89ea482e1649
added qualified_names, no_base_names, custom_accesses, set_policy, restore_naming;
wenzelm
parents:
16113
diff
changeset

234 
val qualified_names = ext_sign (K Sign.qualified_names) (); 
89ea482e1649
added qualified_names, no_base_names, custom_accesses, set_policy, restore_naming;
wenzelm
parents:
16113
diff
changeset

235 
val no_base_names = ext_sign (K Sign.no_base_names) (); 
89ea482e1649
added qualified_names, no_base_names, custom_accesses, set_policy, restore_naming;
wenzelm
parents:
16113
diff
changeset

236 
val custom_accesses = ext_sign Sign.custom_accesses; 
89ea482e1649
added qualified_names, no_base_names, custom_accesses, set_policy, restore_naming;
wenzelm
parents:
16113
diff
changeset

237 
val set_policy = ext_sign Sign.set_policy; 
16190  238 
val restore_naming = ext_sign Sign.restore_naming o sign_of; 
16369  239 
val hide_classes = ext_sign o Sign.hide_classes; 
240 
val hide_classes_i = ext_sign o Sign.hide_classes_i; 

241 
val hide_types = ext_sign o Sign.hide_types; 

242 
val hide_types_i = ext_sign o Sign.hide_types_i; 

243 
val hide_consts = ext_sign o Sign.hide_consts; 

244 
val hide_consts_i = ext_sign o Sign.hide_consts_i; 

14645  245 
val add_name = ext_sign Sign.add_name; 
246 
val copy = ext_sign (K Sign.copy) (); 

247 
val prep_ext = ext_sign (K Sign.prep_ext) (); 

3814  248 

3996  249 

6311  250 

3814  251 
(** add axioms **) 
252 

1526  253 
(* prepare axioms *) 
254 

255 
fun err_in_axm name = 

256 
error ("The error(s) above occurred in axiom " ^ quote name); 

257 

16291  258 
fun no_vars pp tm = 
259 
(case (Term.term_vars tm, Term.term_tvars tm) of 

14184
2e0e02d68cbb
Changed no_vars such that it outputs list of illegal schematic variables.
berghofe
parents:
13646
diff
changeset

260 
([], []) => tm 
2e0e02d68cbb
Changed no_vars such that it outputs list of illegal schematic variables.
berghofe
parents:
13646
diff
changeset

261 
 (ts, ixns) => error (Pretty.string_of (Pretty.block (Pretty.breaks 
2e0e02d68cbb
Changed no_vars such that it outputs list of illegal schematic variables.
berghofe
parents:
13646
diff
changeset

262 
(Pretty.str "Illegal schematic variable(s) in term:" :: 
16291  263 
map (Pretty.term pp) ts @ map (Pretty.typ pp o TVar) ixns))))); 
1526  264 

265 
fun cert_axm sg (name, raw_tm) = 

266 
let 

16291  267 
val pp = Sign.pp sg; 
268 
val (t, T, _) = Sign.certify_term pp sg raw_tm 

2979  269 
handle TYPE (msg, _, _) => error msg 
16291  270 
 TERM (msg, _) => error msg; 
1526  271 
in 
9537  272 
Term.no_dummy_patterns t handle TERM (msg, _) => error msg; 
1526  273 
assert (T = propT) "Term not of type prop"; 
16291  274 
(name, no_vars pp t) 
9629  275 
end; 
1526  276 

5057  277 
(*some duplication of code with read_def_cterm*) 
6661  278 
fun read_def_axm (sg, types, sorts) used (name, str) = 
3814  279 
let 
14914  280 
val ts = Syntax.read (Sign.is_logtype sg) (Sign.syn_of sg) propT str; 
14828  281 
val (t, _) = Sign.infer_types (Sign.pp sg) sg types sorts used true (ts, propT); 
9320  282 
in cert_axm sg (name, t) end 
1960
ae390b599213
Improved error handling: if there are syntax or typechecking
paulson
parents:
1539
diff
changeset

283 
handle ERROR => err_in_axm name; 
1526  284 

15531  285 
fun read_axm sg name_str = read_def_axm (sg, K NONE, K NONE) [] name_str; 
5057  286 

1526  287 
fun inferT_axm sg (name, pre_tm) = 
16291  288 
let 
289 
val pp = Sign.pp sg; 

290 
val (t, _) = Sign.infer_types pp sg (K NONE) (K NONE) [] true ([pre_tm], propT); 

291 
in (name, no_vars pp t) end 

1526  292 
handle ERROR => err_in_axm name; 
293 

294 

295 
(* extend axioms of a theory *) 

296 

16291  297 
local 
298 

299 
fun gen_add_axioms prep_axm raw_axms thy = 

1526  300 
let 
16291  301 
val sg = sign_of thy; 
16339  302 
val axms = map (apsnd (Term.compress_term o Logic.varify) o prep_axm sg) raw_axms; 
303 
in ext_theory thy I axms [] end; 

1526  304 

16291  305 
in 
306 

307 
val add_axioms = gen_add_axioms read_axm; 

308 
val add_axioms_i = gen_add_axioms cert_axm; 

309 

310 
end; 

1526  311 

312 

3814  313 
(* add oracle **) 
314 

16339  315 
fun add_oracle (bname, oracle) thy = 
316 
ext_theory thy I [] [(bname, (oracle, stamp ()))]; 

3814  317 

318 

3767
e2bb53d8dd26
moved theory stuff (add_defs etc.) here from drule.ML;
wenzelm
parents:
2979
diff
changeset

319 

e2bb53d8dd26
moved theory stuff (add_defs etc.) here from drule.ML;
wenzelm
parents:
2979
diff
changeset

320 
(** add constant definitions **) 
e2bb53d8dd26
moved theory stuff (add_defs etc.) here from drule.ML;
wenzelm
parents:
2979
diff
changeset

321 

9320  322 
(* overloading *) 
9280  323 

16291  324 
datatype overloading = Clean  Implicit  Useless; 
9320  325 

16291  326 
fun overloading sg overloaded declT defT = 
327 
let 

328 
val defT' = Term.incr_tvar (maxidx_of_typ declT + 1) (Type.varifyT defT); 

329 
in 

330 
if Sign.typ_instance sg (declT, defT') then Clean 

331 
else if Sign.typ_instance sg (Type.strip_sorts declT, Type.strip_sorts defT') then Useless 

332 
else if overloaded then Clean 

333 
else Implicit 

9280  334 
end; 
335 

3767
e2bb53d8dd26
moved theory stuff (add_defs etc.) here from drule.ML;
wenzelm
parents:
2979
diff
changeset

336 

16291  337 
(* dest_def *) 
338 

339 
fun dest_def pp tm = 

3767
e2bb53d8dd26
moved theory stuff (add_defs etc.) here from drule.ML;
wenzelm
parents:
2979
diff
changeset

340 
let 
3787
67571f49ebe3
new internal forms: add_classes_i, add_classrel_i, add_defsort_i, add_arities_i
wenzelm
parents:
3767
diff
changeset

341 
fun err msg = raise TERM (msg, [tm]); 
3767
e2bb53d8dd26
moved theory stuff (add_defs etc.) here from drule.ML;
wenzelm
parents:
2979
diff
changeset

342 

e2bb53d8dd26
moved theory stuff (add_defs etc.) here from drule.ML;
wenzelm
parents:
2979
diff
changeset

343 
val (lhs, rhs) = Logic.dest_equals (Logic.strip_imp_concl tm) 
e2bb53d8dd26
moved theory stuff (add_defs etc.) here from drule.ML;
wenzelm
parents:
2979
diff
changeset

344 
handle TERM _ => err "Not a metaequality (==)"; 
16291  345 
val (head, args) = Term.strip_comb lhs; 
346 
val (c, T) = Term.dest_Const head 

3767
e2bb53d8dd26
moved theory stuff (add_defs etc.) here from drule.ML;
wenzelm
parents:
2979
diff
changeset

347 
handle TERM _ => err "Head of lhs not a constant"; 
e2bb53d8dd26
moved theory stuff (add_defs etc.) here from drule.ML;
wenzelm
parents:
2979
diff
changeset

348 

4141  349 
fun dest_free (Free (x, _)) = x 
350 
 dest_free (Const ("TYPE", Type ("itself", [TFree (x, _)]))) = x 

351 
 dest_free _ = raise Match; 

352 

16291  353 
val show_terms = commas_quote o map (Pretty.string_of_term pp); 
4141  354 
val show_frees = commas_quote o map dest_free; 
3767
e2bb53d8dd26
moved theory stuff (add_defs etc.) here from drule.ML;
wenzelm
parents:
2979
diff
changeset

355 
val show_tfrees = commas_quote o map fst; 
e2bb53d8dd26
moved theory stuff (add_defs etc.) here from drule.ML;
wenzelm
parents:
2979
diff
changeset

356 

16291  357 
val lhs_nofrees = filter (not o can dest_free) args; 
3767
e2bb53d8dd26
moved theory stuff (add_defs etc.) here from drule.ML;
wenzelm
parents:
2979
diff
changeset

358 
val lhs_dups = duplicates args; 
16291  359 
val rhs_extras = term_frees rhs > fold (remove op =) args; 
360 
val rhs_extrasT = term_tfrees rhs > fold (remove op =) (typ_tfrees T); 

3767
e2bb53d8dd26
moved theory stuff (add_defs etc.) here from drule.ML;
wenzelm
parents:
2979
diff
changeset

361 
in 
16291  362 
if not (null lhs_nofrees) then 
363 
err ("Nonvariables as arguments on lhs: " ^ show_terms lhs_nofrees) 

3767
e2bb53d8dd26
moved theory stuff (add_defs etc.) here from drule.ML;
wenzelm
parents:
2979
diff
changeset

364 
else if not (null lhs_dups) then 
e2bb53d8dd26
moved theory stuff (add_defs etc.) here from drule.ML;
wenzelm
parents:
2979
diff
changeset

365 
err ("Duplicate variables on lhs: " ^ show_frees lhs_dups) 
e2bb53d8dd26
moved theory stuff (add_defs etc.) here from drule.ML;
wenzelm
parents:
2979
diff
changeset

366 
else if not (null rhs_extras) then 
e2bb53d8dd26
moved theory stuff (add_defs etc.) here from drule.ML;
wenzelm
parents:
2979
diff
changeset

367 
err ("Extra variables on rhs: " ^ show_frees rhs_extras) 
e2bb53d8dd26
moved theory stuff (add_defs etc.) here from drule.ML;
wenzelm
parents:
2979
diff
changeset

368 
else if not (null rhs_extrasT) then 
e2bb53d8dd26
moved theory stuff (add_defs etc.) here from drule.ML;
wenzelm
parents:
2979
diff
changeset

369 
err ("Extra type variables on rhs: " ^ show_tfrees rhs_extrasT) 
16291  370 
else if exists_Const (equal (c, T)) rhs then 
3767
e2bb53d8dd26
moved theory stuff (add_defs etc.) here from drule.ML;
wenzelm
parents:
2979
diff
changeset

371 
err ("Constant to be defined occurs on rhs") 
16291  372 
else ((c, T), rhs) 
3767
e2bb53d8dd26
moved theory stuff (add_defs etc.) here from drule.ML;
wenzelm
parents:
2979
diff
changeset

373 
end; 
e2bb53d8dd26
moved theory stuff (add_defs etc.) here from drule.ML;
wenzelm
parents:
2979
diff
changeset

374 

e2bb53d8dd26
moved theory stuff (add_defs etc.) here from drule.ML;
wenzelm
parents:
2979
diff
changeset

375 

16291  376 
(* check_def *) 
377 

378 
fun pretty_const pp (c, T) = 

379 
[Pretty.str c, Pretty.str " ::", Pretty.brk 1, 

380 
Pretty.quote (Pretty.typ pp (Type.freeze_type T))]; (* FIXME zero indexes!? *) 

3767
e2bb53d8dd26
moved theory stuff (add_defs etc.) here from drule.ML;
wenzelm
parents:
2979
diff
changeset

381 

16291  382 
(* FIXME move error messages to defs.ML !? *) 
9320  383 

16291  384 
fun pretty_path pp path = fold_rev (fn (T, c, def) => 
385 
fn [] => [Pretty.block (pretty_const pp (c, T))] 

386 
 prts => Pretty.block (pretty_const pp (c, T) @ 

387 
[Pretty.brk 1, Pretty.str ("depends via " ^ quote def ^ " on")]) :: prts) path []; 

3767
e2bb53d8dd26
moved theory stuff (add_defs etc.) here from drule.ML;
wenzelm
parents:
2979
diff
changeset

388 

16313
79b37d5e50b1
A flag DEFS_CHAIN_HISTORY can be used to improve the error message
obua
parents:
16291
diff
changeset

389 
fun chain_history_msg s = 
79b37d5e50b1
A flag DEFS_CHAIN_HISTORY can be used to improve the error message
obua
parents:
16291
diff
changeset

390 
if Defs.chain_history () then s^": " 
79b37d5e50b1
A flag DEFS_CHAIN_HISTORY can be used to improve the error message
obua
parents:
16291
diff
changeset

391 
else s^" (set DEFS_CHAIN_HISTORY=ON for full history): " 
79b37d5e50b1
A flag DEFS_CHAIN_HISTORY can be used to improve the error message
obua
parents:
16291
diff
changeset

392 

16291  393 
fun defs_circular pp path = 
16313
79b37d5e50b1
A flag DEFS_CHAIN_HISTORY can be used to improve the error message
obua
parents:
16291
diff
changeset

394 
Pretty.str (chain_history_msg "Cyclic dependency of definitions") :: pretty_path pp path 
16291  395 
> Pretty.chunks > Pretty.string_of; 
396 

397 
fun defs_infinite_chain pp path = 

16313
79b37d5e50b1
A flag DEFS_CHAIN_HISTORY can be used to improve the error message
obua
parents:
16291
diff
changeset

398 
Pretty.str (chain_history_msg "Infinite chain of definitions") :: pretty_path pp path 
16291  399 
> Pretty.chunks > Pretty.string_of; 
400 

401 
fun defs_clash def1 def2 = "Type clash in definitions " ^ quote def1 ^ " and " ^ quote def2; 

9320  402 

16291  403 
fun defs_final pp const = 
404 
(Pretty.str "Attempt to define final constant" :: Pretty.brk 1 :: pretty_const pp const) 

405 
> Pretty.block > Pretty.string_of; 

3767
e2bb53d8dd26
moved theory stuff (add_defs etc.) here from drule.ML;
wenzelm
parents:
2979
diff
changeset

406 

16291  407 
(* FIXME move to defs.ML; avoid exceptions *) 
408 
fun declare sg c defs = 

409 
let val T = Sign.the_const_type sg c 

410 
in if_none (try (Defs.declare defs) (c, T)) defs end; 

10494  411 

16108
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
15747
diff
changeset

412 

16291  413 
fun check_def sg overloaded (bname, tm) defs = 
414 
let 

415 
val pp = Sign.pp sg; 

416 
val name = Sign.full_name sg bname; 

417 

418 
fun err msg = error (Pretty.string_of (Pretty.chunks 

419 
[Pretty.str msg, 

420 
Pretty.block [Pretty.str ("The error(s) above occurred in definition " ^ quote name ^ ":"), 

421 
Pretty.fbrk, Pretty.quote (Pretty.term pp tm)]])); 

422 

423 
fun show_def const txt = 

424 
[Pretty.block (Pretty.str "Definition of " :: pretty_const pp const), Pretty.str txt] 

425 
> Pretty.chunks > Pretty.string_of; 

9320  426 

16291  427 
val ((c, defT), rhs) = dest_def pp tm handle TERM (msg, _) => err msg; 
428 
val rhs_consts = Term.term_constsT rhs; 

429 
val declT = Sign.the_const_type sg c; 

16108
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
15747
diff
changeset

430 

16291  431 
val _ = 
432 
(case overloading sg overloaded declT defT of 

433 
Clean => () 

434 
 Implicit => warning (show_def (c, defT) 

435 
("is strictly less general than the declared type (see " ^ quote name ^ ")")) 

436 
 Useless => err (Library.setmp show_sorts true (show_def (c, defT)) 

437 
"imposes additional sort constraints on the declared type of the constant")); 

16108
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
15747
diff
changeset

438 

16291  439 
val decl_defs = defs > declare sg c > fold (declare sg) (map #1 rhs_consts); 
3767
e2bb53d8dd26
moved theory stuff (add_defs etc.) here from drule.ML;
wenzelm
parents:
2979
diff
changeset

440 
in 
16291  441 
Defs.define decl_defs (c, defT) name rhs_consts 
442 
handle Defs.DEFS msg => err ("DEFS: " ^ msg) (* FIXME sys_error!? *) 

443 
 Defs.CIRCULAR path => err (defs_circular pp path) 

444 
 Defs.INFINITE_CHAIN path => err (defs_infinite_chain pp path) 

445 
 Defs.CLASH (_, def1, def2) => err (defs_clash def1 def2) 

446 
 Defs.FINAL const => err (defs_final pp const) 

3767
e2bb53d8dd26
moved theory stuff (add_defs etc.) here from drule.ML;
wenzelm
parents:
2979
diff
changeset

447 
end; 
e2bb53d8dd26
moved theory stuff (add_defs etc.) here from drule.ML;
wenzelm
parents:
2979
diff
changeset

448 

e2bb53d8dd26
moved theory stuff (add_defs etc.) here from drule.ML;
wenzelm
parents:
2979
diff
changeset

449 

e2bb53d8dd26
moved theory stuff (add_defs etc.) here from drule.ML;
wenzelm
parents:
2979
diff
changeset

450 
(* add_defs *) 
e2bb53d8dd26
moved theory stuff (add_defs etc.) here from drule.ML;
wenzelm
parents:
2979
diff
changeset

451 

16291  452 
local 
9320  453 

16291  454 
fun gen_add_defs prep_axm overloaded raw_axms thy = 
455 
let 

456 
val Theory {sign, defs, axioms, oracles, parents, ancestors} = thy; 

9320  457 
val axms = map (prep_axm sign) raw_axms; 
16291  458 
val defs' = fold (check_def sign overloaded) axms defs; 
3767
e2bb53d8dd26
moved theory stuff (add_defs etc.) here from drule.ML;
wenzelm
parents:
2979
diff
changeset

459 
in 
16291  460 
make_theory sign defs' axioms oracles parents ancestors 
9320  461 
> add_axioms_i axms 
3767
e2bb53d8dd26
moved theory stuff (add_defs etc.) here from drule.ML;
wenzelm
parents:
2979
diff
changeset

462 
end; 
e2bb53d8dd26
moved theory stuff (add_defs etc.) here from drule.ML;
wenzelm
parents:
2979
diff
changeset

463 

16291  464 
in 
465 

466 
val add_defs_i = gen_add_defs cert_axm; 

467 
val add_defs = gen_add_defs read_axm; 

468 

469 
end; 

3767
e2bb53d8dd26
moved theory stuff (add_defs etc.) here from drule.ML;
wenzelm
parents:
2979
diff
changeset

470 

e2bb53d8dd26
moved theory stuff (add_defs etc.) here from drule.ML;
wenzelm
parents:
2979
diff
changeset

471 

14223
0ee05eef881b
Added support for making constants final, that is, ensuring that no
skalberg
parents:
14204
diff
changeset

472 
(* add_finals *) 
0ee05eef881b
Added support for making constants final, that is, ensuring that no
skalberg
parents:
14204
diff
changeset

473 

16291  474 
local 
475 

476 
fun gen_add_finals prep_term overloaded raw_terms thy = 

14223
0ee05eef881b
Added support for making constants final, that is, ensuring that no
skalberg
parents:
14204
diff
changeset

477 
let 
16291  478 
val Theory {sign, defs, axioms, oracles, parents, ancestors} = thy; 
479 
fun finalize tm finals = 

480 
let 

481 
fun err msg = raise TERM (msg, [tm]); (* FIXME error!? *) 

482 
val (c, defT) = 

483 
(case tm of Const x => x 

484 
 Free _ => err "Attempt to finalize variable (or undeclared constant)" 

485 
 _ => err "Attempt to finalize nonconstant term"); 

486 
val declT = Sign.the_const_type sign c 

487 
handle TYPE (msg, _, _) => err msg; 

488 
val _ = 

489 
(case overloading sign overloaded declT defT of 

490 
Clean => () 

491 
 Implcit => warning ("Finalizing " ^ quote c ^ 

492 
" at a strictly less general type than declared") 

493 
 Useless => err "Sort constraints stronger than declared"); 

494 
in 

495 
Defs.finalize (if_none (try (Defs.declare finals) (c, declT)) finals) (c, defT) 

496 
end; 

497 
val defs' = fold finalize (map (prep_term sign) raw_terms) defs; 

498 
in make_theory sign defs' axioms oracles parents ancestors end; 

14223
0ee05eef881b
Added support for making constants final, that is, ensuring that no
skalberg
parents:
14204
diff
changeset

499 

16291  500 
fun read_term sg = Sign.simple_read_term sg TypeInfer.logicT; 
501 
fun cert_term sg = #1 o Sign.certify_term (Sign.pp sg) sg; 

502 

14223
0ee05eef881b
Added support for making constants final, that is, ensuring that no
skalberg
parents:
14204
diff
changeset

503 
in 
16291  504 

505 
val add_finals = gen_add_finals read_term; 

506 
val add_finals_i = gen_add_finals cert_term; 

507 

14223
0ee05eef881b
Added support for making constants final, that is, ensuring that no
skalberg
parents:
14204
diff
changeset

508 
end; 
0ee05eef881b
Added support for making constants final, that is, ensuring that no
skalberg
parents:
14204
diff
changeset

509 

0ee05eef881b
Added support for making constants final, that is, ensuring that no
skalberg
parents:
14204
diff
changeset

510 

3878  511 

3865  512 
(** additional theory data **) 
513 

4996  514 
val init_data = curry (ext_sign Sign.init_data); 
515 
fun print_data kind = Sign.print_data kind o sign_of; 

516 
fun get_data kind f = Sign.get_data kind f o sign_of; 

517 
fun put_data kind f = ext_sign (Sign.put_data kind f); 

3865  518 

519 

3767
e2bb53d8dd26
moved theory stuff (add_defs etc.) here from drule.ML;
wenzelm
parents:
2979
diff
changeset

520 

6661  521 
(** merge theories **) (*exception ERROR*) 
4019  522 

3878  523 
(*merge list of theories from left to right, preparing extend*) 
3967
edd5ff9371f8
sg_ref: automatic adjustment of thms of draft theories;
wenzelm
parents:
3956
diff
changeset

524 
fun prep_ext_merge thys = 
15703  525 
let 
16291  526 
val sign' = Sign.prep_ext_merge (map sign_of thys); 
3814  527 

16291  528 
val defss = map (#defs o rep_theory) thys; 
529 
val defs' = foldl (uncurry Defs.merge) (hd defss) (tl defss) 

530 
handle Defs.CIRCULAR namess => error (defs_circular (Sign.pp sign') namess) 

531 
 Defs.INFINITE_CHAIN namess => error (defs_infinite_chain (Sign.pp sign') namess); 

15703  532 

16339  533 
val axioms' = NameSpace.empty_table; 
9282
0181ac100520
Defs are now checked for circularity (if not overloaded).
nipkow
parents:
9280
diff
changeset

534 

16339  535 
val oras_spaces = map (#1 o #oracles o rep_theory) thys; 
536 
val oras_space' = Library.foldl NameSpace.merge (hd oras_spaces, tl oras_spaces); 

15703  537 
fun eq_ora ((_, (_, s1: stamp)), (_, (_, s2))) = s1 = s2; 
16339  538 
val oras' = 
15703  539 
Symtab.make (gen_distinct eq_ora 
16339  540 
(List.concat (map (Symtab.dest o #2 o #oracles o rep_theory) thys))) 
15703  541 
handle Symtab.DUPS names => err_dup_oras names; 
16339  542 
val oracles' = (oras_space', oras'); 
4019  543 

15703  544 
val parents' = gen_distinct eq_thy thys; 
545 
val ancestors' = 

546 
gen_distinct eq_thy (parents' @ List.concat (map ancestors_of thys)); 

16291  547 
in make_theory sign' defs' axioms' oracles' parents' ancestors' end; 
1526  548 

3885  549 

1526  550 
end; 
551 

3767
e2bb53d8dd26
moved theory stuff (add_defs etc.) here from drule.ML;
wenzelm
parents:
2979
diff
changeset

552 
structure BasicTheory: BASIC_THEORY = Theory; 
e2bb53d8dd26
moved theory stuff (add_defs etc.) here from drule.ML;
wenzelm
parents:
2979
diff
changeset

553 
open BasicTheory; 