author  wenzelm 
Thu, 09 Jun 2005 12:03:26 +0200  
changeset 16339  b02b6da609c3 
parent 16313  79b37d5e50b1 
child 16369  96d73621fabb 
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 
12588  97 
val hide_space: bool > string * xstring list > theory > theory 
98 
val hide_space_i: bool > string * string list > theory > theory 

99 
val hide_classes: bool > string list > theory > theory 

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

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

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

6188  111 
signature PRIVATE_THEORY = 
5642  112 
sig 
113 
include THEORY 

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

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

119 
end; 

1526  120 

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

3996  124 

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

127 
datatype theory = 

128 
Theory of { 

129 
sign: Sign.sg, 

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

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

1526  135 

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

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

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

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

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

150 

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

153 

154 
(*compare theories*) 

155 
val subthy = Sign.subsig o pairself sign_of; 

156 
val eq_thy = Sign.eq_sg o pairself sign_of; 

157 

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

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

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

166 

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

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

171 

172 

173 
(** extend theory **) 

174 

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

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

1526  179 

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

16339  184 
val naming = Sign.naming_of sign; 
185 

186 
val axioms' = NameSpace.extend_table naming 

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

188 
handle Symtab.DUPS dups => err_dup_axms dups; 

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

190 
handle Symtab.DUPS dups => err_dup_oras dups; 

191 

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

1526  195 

196 

197 
(* extend signature of a theory *) 

198 

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

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

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

203 
val add_classrel = ext_sign Sign.add_classrel; 

204 
val add_classrel_i = ext_sign Sign.add_classrel_i; 

205 
val add_defsort = ext_sign Sign.add_defsort; 

206 
val add_defsort_i = ext_sign Sign.add_defsort_i; 

207 
val add_types = ext_sign Sign.add_types; 

208 
val add_nonterminals = ext_sign Sign.add_nonterminals; 

209 
val add_tyabbrs = ext_sign Sign.add_tyabbrs; 

210 
val add_tyabbrs_i = ext_sign Sign.add_tyabbrs_i; 

211 
val add_arities = ext_sign Sign.add_arities; 

212 
val add_arities_i = ext_sign Sign.add_arities_i; 

213 
val add_consts = ext_sign Sign.add_consts; 

214 
val add_consts_i = ext_sign Sign.add_consts_i; 

215 
val add_syntax = ext_sign Sign.add_syntax; 

216 
val add_syntax_i = ext_sign Sign.add_syntax_i; 

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

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

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

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

223 
val add_advanced_trfuns = ext_sign Sign.add_advanced_trfuns; 

224 
val add_advanced_trfunsT = ext_sign Sign.add_advanced_trfunsT; 

225 
val add_tokentrfuns = ext_sign Sign.add_tokentrfuns; 

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

229 
val add_path = ext_sign Sign.add_path; 

230 
val parent_path = add_path ".."; 

231 
val root_path = add_path "/"; 

232 
val absolute_path = add_path "//"; 

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

233 
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

234 
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

235 
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

236 
val set_policy = ext_sign Sign.set_policy; 
16190  237 
val restore_naming = ext_sign Sign.restore_naming o sign_of; 
14645  238 
val hide_space = ext_sign o Sign.hide_space; 
239 
val hide_space_i = ext_sign o Sign.hide_space_i; 

240 
fun hide_classes b = curry (hide_space_i b) Sign.classK; 

241 
fun hide_types b = curry (hide_space_i b) Sign.typeK; 

242 
fun hide_consts b = curry (hide_space_i b) Sign.constK; 

243 
val add_name = ext_sign Sign.add_name; 

244 
val copy = ext_sign (K Sign.copy) (); 

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

3814  246 

3996  247 

6311  248 

3814  249 
(** add axioms **) 
250 

1526  251 
(* prepare axioms *) 
252 

253 
fun err_in_axm name = 

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

255 

16291  256 
fun no_vars pp tm = 
257 
(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

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

259 
 (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

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

263 
fun cert_axm sg (name, raw_tm) = 

264 
let 

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

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

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

281 
handle ERROR => err_in_axm name; 
1526  282 

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

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

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

289 
in (name, no_vars pp t) end 

1526  290 
handle ERROR => err_in_axm name; 
291 

292 

293 
(* extend axioms of a theory *) 

294 

16291  295 
local 
296 

297 
fun gen_add_axioms prep_axm raw_axms thy = 

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

1526  302 

16291  303 
in 
304 

305 
val add_axioms = gen_add_axioms read_axm; 

306 
val add_axioms_i = gen_add_axioms cert_axm; 

307 

308 
end; 

1526  309 

310 

3814  311 
(* add oracle **) 
312 

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

3814  315 

316 

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

317 

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

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

319 

9320  320 
(* overloading *) 
9280  321 

16291  322 
datatype overloading = Clean  Implicit  Useless; 
9320  323 

16291  324 
fun overloading sg overloaded declT defT = 
325 
let 

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

327 
in 

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

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

330 
else if overloaded then Clean 

331 
else Implicit 

9280  332 
end; 
333 

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

334 

16291  335 
(* dest_def *) 
336 

337 
fun dest_def pp tm = 

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

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

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

340 

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

341 
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

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

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

345 
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

346 

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

349 
 dest_free _ = raise Match; 

350 

16291  351 
val show_terms = commas_quote o map (Pretty.string_of_term pp); 
4141  352 
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

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

354 

16291  355 
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

356 
val lhs_dups = duplicates args; 
16291  357 
val rhs_extras = term_frees rhs > fold (remove op =) args; 
358 
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

359 
in 
16291  360 
if not (null lhs_nofrees) then 
361 
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

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

363 
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

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

365 
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

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

367 
err ("Extra type variables on rhs: " ^ show_tfrees rhs_extrasT) 
16291  368 
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

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

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

372 

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

373 

16291  374 
(* check_def *) 
375 

376 
fun pretty_const pp (c, T) = 

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

378 
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

379 

16291  380 
(* FIXME move error messages to defs.ML !? *) 
9320  381 

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

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

385 
[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

386 

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

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

388 
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

389 
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

390 

16291  391 
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

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

395 
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

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

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

9320  400 

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

403 
> Pretty.block > Pretty.string_of; 

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

404 

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

407 
let val T = Sign.the_const_type sg c 

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

10494  409 

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

410 

16291  411 
fun check_def sg overloaded (bname, tm) defs = 
412 
let 

413 
val pp = Sign.pp sg; 

414 
val name = Sign.full_name sg bname; 

415 

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

417 
[Pretty.str msg, 

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

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

420 

421 
fun show_def const txt = 

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

423 
> Pretty.chunks > Pretty.string_of; 

9320  424 

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

427 
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

428 

16291  429 
val _ = 
430 
(case overloading sg overloaded declT defT of 

431 
Clean => () 

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

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

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

435 
"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

436 

16291  437 
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

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

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

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

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

444 
 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

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

446 

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

447 

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

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

449 

16291  450 
local 
9320  451 

16291  452 
fun gen_add_defs prep_axm overloaded raw_axms thy = 
453 
let 

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

9320  455 
val axms = map (prep_axm sign) raw_axms; 
16291  456 
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

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

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

461 

16291  462 
in 
463 

464 
val add_defs_i = gen_add_defs cert_axm; 

465 
val add_defs = gen_add_defs read_axm; 

466 

467 
end; 

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

468 

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

469 

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

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

471 

16291  472 
local 
473 

474 
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

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

478 
let 

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

480 
val (c, defT) = 

481 
(case tm of Const x => x 

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

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

484 
val declT = Sign.the_const_type sign c 

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

486 
val _ = 

487 
(case overloading sign overloaded declT defT of 

488 
Clean => () 

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

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

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

492 
in 

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

494 
end; 

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

496 
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

497 

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

500 

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

501 
in 
16291  502 

503 
val add_finals = gen_add_finals read_term; 

504 
val add_finals_i = gen_add_finals cert_term; 

505 

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

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

507 

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

508 

3878  509 

3865  510 
(** additional theory data **) 
511 

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

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

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

3865  516 

517 

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

518 

6661  519 
(** merge theories **) (*exception ERROR*) 
4019  520 

3878  521 
(*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

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

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

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

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

15703  530 

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

532 

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

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

15703  542 
val parents' = gen_distinct eq_thy thys; 
543 
val ancestors' = 

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

16291  545 
in make_theory sign' defs' axioms' oracles' parents' ancestors' end; 
1526  546 

3885  547 

1526  548 
end; 
549 

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

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

551 
open BasicTheory; 