author  skalberg 
Thu, 09 Oct 2003 18:13:32 +0200  
changeset 14223  0ee05eef881b 
parent 14204  2fa6ecb87d47 
child 14645  83776a9f0a9c 
permissions  rwrr 
1526  1 
(* Title: Pure/theory.ML 
2 
ID: $Id$ 

3 
Author: Lawrence C Paulson and Markus Wenzel 

12785  4 
License: GPL (GNU GENERAL PUBLIC LICENSE) 
1526  5 

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

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

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

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

3996  13 
val rep_theory: theory > 
3814  14 
{sign: Sign.sg, 
9320  15 
const_deps: unit Graph.T, 
14223
0ee05eef881b
Added support for making constants final, that is, ensuring that no
skalberg
parents:
14204
diff
changeset

16 
final_consts: typ list Symtab.table, 
3996  17 
axioms: term Symtab.table, 
4996  18 
oracles: ((Sign.sg * Object.T > term) * stamp) Symtab.table, 
4019  19 
parents: theory list, 
20 
ancestors: theory list} 

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

4019  25 
val ancestors_of: theory > theory list 
3996  26 
val subthy: theory * theory > bool 
27 
val eq_thy: theory * theory > bool 

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

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

3996  31 
val read_axm: Sign.sg > string * string > string * term 
32 
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

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

34 

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

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

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

37 
include BASIC_THEORY 
3996  38 
val axiomK: string 
39 
val oracleK: string 

4912  40 
(*theory extension primitives*) 
3996  41 
val add_classes: (bclass * xclass list) list > theory > theory 
42 
val add_classes_i: (bclass * class list) list > theory > theory 

43 
val add_classrel: (xclass * xclass) list > theory > theory 

44 
val add_classrel_i: (class * class) list > theory > theory 

8897  45 
val add_defsort: string > theory > theory 
3996  46 
val add_defsort_i: sort > theory > theory 
47 
val add_types: (bstring * int * mixfix) list > theory > theory 

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

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

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

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

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

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

61 
val add_trfuns: 

4344  62 
(string * (Syntax.ast list > Syntax.ast)) list * 
63 
(string * (term list > term)) list * 

64 
(string * (term list > term)) list * 

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

3996  66 
val add_trfunsT: 
4344  67 
(string * (bool > typ > term list > term)) list > theory > theory 
2693  68 
val add_tokentrfuns: 
6311  69 
(string * string * (string > string * real)) list > theory > theory 
70 
val add_mode_tokentrfuns: string > (string * (string > string * real)) list 

71 
> theory > theory 

4617  72 
val add_trrules: (xstring * string) Syntax.trrule list > theory > theory 
3996  73 
val add_trrules_i: Syntax.ast Syntax.trrule list > theory > theory 
74 
val add_axioms: (bstring * string) list > theory > theory 

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

4996  76 
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

77 
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

78 
val add_finals_i: bool > term list > theory > theory 
9320  79 
val add_defs: bool > (bstring * string) list > theory > theory 
80 
val add_defs_i: bool > (bstring * term) list > theory > theory 

3996  81 
val add_path: string > theory > theory 
4846  82 
val parent_path: theory > theory 
83 
val root_path: theory > theory 

11501  84 
val absolute_path: theory > theory 
12588  85 
val hide_space: bool > string * xstring list > theory > theory 
86 
val hide_space_i: bool > string * string list > theory > theory 

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

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

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

3996  90 
val add_name: string > theory > theory 
5862  91 
val copy: theory > theory 
6661  92 
val prep_ext: theory > theory 
3996  93 
val prep_ext_merge: theory list > theory 
4970  94 
val requires: theory > string > string > unit 
6369  95 
val assert_super: theory > theory > theory 
3996  96 
val pre_pure: theory 
1526  97 
end; 
98 

6188  99 
signature PRIVATE_THEORY = 
5642  100 
sig 
101 
include THEORY 

6546  102 
val init_data: Object.kind > (Object.T * (Object.T > Object.T) * (Object.T > Object.T) * 
12311  103 
(Object.T * Object.T > Object.T) * (Sign.sg > Object.T > unit)) > theory > theory 
5642  104 
val print_data: Object.kind > theory > unit 
105 
val get_data: Object.kind > (Object.T > 'a) > theory > 'a 

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

107 
end; 

1526  108 

5642  109 

6188  110 
structure Theory: PRIVATE_THEORY = 
1526  111 
struct 
2206  112 

3996  113 

2206  114 
(** datatype theory **) 
1526  115 

9320  116 
(*Note: dependencies are only tracked for nonoverloaded constant definitions*) 
117 

1526  118 
datatype theory = 
119 
Theory of { 

120 
sign: Sign.sg, 

9320  121 
const_deps: unit Graph.T, 
14223
0ee05eef881b
Added support for making constants final, that is, ensuring that no
skalberg
parents:
14204
diff
changeset

122 
final_consts: typ list Symtab.table, 
3996  123 
axioms: term Symtab.table, 
4996  124 
oracles: ((Sign.sg * Object.T > term) * stamp) Symtab.table, 
4019  125 
parents: theory list, 
126 
ancestors: theory list}; 

1526  127 

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

128 
fun make_theory sign const_deps final_consts axioms oracles parents ancestors = 
0ee05eef881b
Added support for making constants final, that is, ensuring that no
skalberg
parents:
14204
diff
changeset

129 
Theory {sign = sign, const_deps = const_deps, final_consts = final_consts, axioms = axioms, 
0ee05eef881b
Added support for making constants final, that is, ensuring that no
skalberg
parents:
14204
diff
changeset

130 
oracles = oracles, parents = parents, ancestors = ancestors}; 
3996  131 

1526  132 
fun rep_theory (Theory args) = args; 
133 

3996  134 
val sign_of = #sign o rep_theory; 
6188  135 
val is_draft = Sign.is_draft o sign_of; 
3996  136 
val syn_of = #syn o Sign.rep_sg o sign_of; 
137 
val parents_of = #parents o rep_theory; 

4019  138 
val ancestors_of = #ancestors o rep_theory; 
3996  139 

1526  140 
(*errors involving theories*) 
141 
exception THEORY of string * theory list; 

142 

143 
(*compare theories*) 

144 
val subthy = Sign.subsig o pairself sign_of; 

145 
val eq_thy = Sign.eq_sg o pairself sign_of; 

146 

6369  147 
(*check for some theory*) 
4970  148 
fun requires thy name what = 
10930  149 
if Sign.exists_stamp name (sign_of thy) then () 
4846  150 
else error ("Require theory " ^ quote name ^ " as an ancestor for " ^ what); 
1526  151 

6369  152 
fun assert_super thy1 thy2 = 
153 
if subthy (thy1, thy2) then thy2 

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

155 

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

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

158 
make_theory Sign.pre_pure Graph.empty Symtab.empty Symtab.empty Symtab.empty [] []; 
1526  159 

160 

161 

162 
(** extend theory **) 

163 

8725  164 
(*name spaces*) 
3996  165 
val axiomK = "axiom"; 
3814  166 
val oracleK = "oracle"; 
167 

168 

169 
(* extend logical part of a theory *) 

170 

1526  171 
fun err_dup_axms names = 
10494  172 
error ("Duplicate axiom name(s): " ^ commas_quote names); 
1526  173 

3814  174 
fun err_dup_oras names = 
10494  175 
error ("Duplicate oracles: " ^ commas_quote names); 
3814  176 

9320  177 
fun ext_theory thy ext_sg ext_deps new_axms new_oras = 
1526  178 
let 
14223
0ee05eef881b
Added support for making constants final, that is, ensuring that no
skalberg
parents:
14204
diff
changeset

179 
val Theory {sign, const_deps, final_consts, axioms, oracles, parents, ancestors} = thy; 
1526  180 
val draft = Sign.is_draft sign; 
3996  181 
val axioms' = 
4488  182 
Symtab.extend (if draft then axioms else Symtab.empty, new_axms) 
1526  183 
handle Symtab.DUPS names => err_dup_axms names; 
3814  184 
val oracles' = 
4488  185 
Symtab.extend (oracles, new_oras) 
3814  186 
handle Symtab.DUPS names => err_dup_oras names; 
4019  187 
val (parents', ancestors') = 
188 
if draft then (parents, ancestors) else ([thy], thy :: ancestors); 

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

190 
make_theory (ext_sg sign) (ext_deps const_deps) final_consts axioms' oracles' parents' ancestors' 
1526  191 
end; 
192 

193 

194 
(* extend signature of a theory *) 

195 

9320  196 
fun ext_sign extfun decls thy = ext_theory thy (extfun decls) I [] []; 
1526  197 

4996  198 
val add_classes = ext_sign Sign.add_classes; 
199 
val add_classes_i = ext_sign Sign.add_classes_i; 

200 
val add_classrel = ext_sign Sign.add_classrel; 

201 
val add_classrel_i = ext_sign Sign.add_classrel_i; 

202 
val add_defsort = ext_sign Sign.add_defsort; 

203 
val add_defsort_i = ext_sign Sign.add_defsort_i; 

204 
val add_types = ext_sign Sign.add_types; 

205 
val add_nonterminals = ext_sign Sign.add_nonterminals; 

206 
val add_tyabbrs = ext_sign Sign.add_tyabbrs; 

207 
val add_tyabbrs_i = ext_sign Sign.add_tyabbrs_i; 

208 
val add_arities = ext_sign Sign.add_arities; 

209 
val add_arities_i = ext_sign Sign.add_arities_i; 

210 
val add_consts = ext_sign Sign.add_consts; 

211 
val add_consts_i = ext_sign Sign.add_consts_i; 

212 
val add_syntax = ext_sign Sign.add_syntax; 

213 
val add_syntax_i = ext_sign Sign.add_syntax_i; 

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

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

216 
val add_trfuns = ext_sign Sign.add_trfuns; 

217 
val add_trfunsT = ext_sign Sign.add_trfunsT; 

218 
val add_tokentrfuns = ext_sign Sign.add_tokentrfuns; 

6311  219 
fun add_mode_tokentrfuns m = add_tokentrfuns o map (fn (s, f) => (m, s, f)); 
4996  220 
val add_trrules = ext_sign Sign.add_trrules; 
221 
val add_trrules_i = ext_sign Sign.add_trrules_i; 

222 
val add_path = ext_sign Sign.add_path; 

4846  223 
val parent_path = add_path ".."; 
224 
val root_path = add_path "/"; 

11501  225 
val absolute_path = add_path "//"; 
4996  226 
val add_space = ext_sign Sign.add_space; 
12588  227 
val hide_space = ext_sign o Sign.hide_space; 
228 
val hide_space_i = ext_sign o Sign.hide_space_i; 

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

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

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

4996  232 
val add_name = ext_sign Sign.add_name; 
6546  233 
val copy = ext_sign (K Sign.copy) (); 
6661  234 
val prep_ext = ext_sign (K Sign.prep_ext) (); 
3814  235 

3996  236 

6311  237 

3814  238 
(** add axioms **) 
239 

1526  240 
(* prepare axioms *) 
241 

242 
fun err_in_axm name = 

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

244 

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

245 
fun no_vars sg tm = (case (term_vars tm, term_tvars tm) of 
2e0e02d68cbb
Changed no_vars such that it outputs list of illegal schematic variables.
berghofe
parents:
13646
diff
changeset

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

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

248 
(Pretty.str "Illegal schematic variable(s) in term:" :: 
2e0e02d68cbb
Changed no_vars such that it outputs list of illegal schematic variables.
berghofe
parents:
13646
diff
changeset

249 
map (Sign.pretty_term sg) ts @ 
2e0e02d68cbb
Changed no_vars such that it outputs list of illegal schematic variables.
berghofe
parents:
13646
diff
changeset

250 
map (Sign.pretty_typ sg o TVar) ixns))))); 
1526  251 

252 
fun cert_axm sg (name, raw_tm) = 

253 
let 

254 
val (t, T, _) = Sign.certify_term sg raw_tm 

2979  255 
handle TYPE (msg, _, _) => error msg 
3996  256 
 TERM (msg, _) => error msg; 
1526  257 
in 
9537  258 
Term.no_dummy_patterns t handle TERM (msg, _) => error msg; 
1526  259 
assert (T = propT) "Term not of type prop"; 
14184
2e0e02d68cbb
Changed no_vars such that it outputs list of illegal schematic variables.
berghofe
parents:
13646
diff
changeset

260 
(name, no_vars sg t) 
9629  261 
end; 
1526  262 

5057  263 
(*some duplication of code with read_def_cterm*) 
6661  264 
fun read_def_axm (sg, types, sorts) used (name, str) = 
3814  265 
let 
266 
val ts = Syntax.read (#syn (Sign.rep_sg sg)) propT str; 

5057  267 
val (t, _) = Sign.infer_types sg types sorts used true (ts, propT); 
9320  268 
in cert_axm sg (name, t) end 
1960
ae390b599213
Improved error handling: if there are syntax or typechecking
paulson
parents:
1539
diff
changeset

269 
handle ERROR => err_in_axm name; 
1526  270 

5057  271 
fun read_axm sg name_str = read_def_axm (sg, K None, K None) [] name_str; 
272 

1526  273 
fun inferT_axm sg (name, pre_tm) = 
3814  274 
let 
4251  275 
val (t, _) = Sign.infer_types sg (K None) (K None) [] true ([pre_tm], propT); 
14184
2e0e02d68cbb
Changed no_vars such that it outputs list of illegal schematic variables.
berghofe
parents:
13646
diff
changeset

276 
in (name, no_vars sg t) end 
1526  277 
handle ERROR => err_in_axm name; 
278 

279 

280 
(* extend axioms of a theory *) 

281 

3814  282 
fun ext_axms prep_axm raw_axms (thy as Theory {sign, ...}) = 
1526  283 
let 
3814  284 
val raw_axms' = map (apfst (Sign.full_name sign)) raw_axms; 
285 
val axioms = 

286 
map (apsnd (Term.compress_term o Logic.varify) o prep_axm sign) raw_axms'; 

4996  287 
val ext_sg = Sign.add_space (axiomK, map fst axioms); 
9320  288 
in ext_theory thy ext_sg I axioms [] end; 
1526  289 

290 
val add_axioms = ext_axms read_axm; 

291 
val add_axioms_i = ext_axms cert_axm; 

292 

293 

3814  294 
(* add oracle **) 
295 

296 
fun add_oracle (raw_name, oracle) (thy as Theory {sign, ...}) = 

297 
let 

298 
val name = Sign.full_name sign raw_name; 

4996  299 
val ext_sg = Sign.add_space (oracleK, [name]); 
9320  300 
in ext_theory thy ext_sg I [] [(name, (oracle, stamp ()))] end; 
3814  301 

302 

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

303 

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

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

305 

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

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

307 

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

308 
(*check if types have common instance (ignoring sorts)*) 
e2bb53d8dd26
moved theory stuff (add_defs etc.) here from drule.ML;
wenzelm
parents:
2979
diff
changeset

309 

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

310 
fun clash_types ty1 ty2 = 
e2bb53d8dd26
moved theory stuff (add_defs etc.) here from drule.ML;
wenzelm
parents:
2979
diff
changeset

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

312 
val ty1' = Type.varifyT ty1; 
e2bb53d8dd26
moved theory stuff (add_defs etc.) here from drule.ML;
wenzelm
parents:
2979
diff
changeset

313 
val ty2' = incr_tvar (maxidx_of_typ ty1' + 1) (Type.varifyT ty2); 
9320  314 
in Type.raw_unify (ty1', ty2') end; 
3767
e2bb53d8dd26
moved theory stuff (add_defs etc.) here from drule.ML;
wenzelm
parents:
2979
diff
changeset

315 

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

316 
fun clash_consts (c1, ty1) (c2, ty2) = 
e2bb53d8dd26
moved theory stuff (add_defs etc.) here from drule.ML;
wenzelm
parents:
2979
diff
changeset

317 
c1 = c2 andalso clash_types ty1 ty2; 
e2bb53d8dd26
moved theory stuff (add_defs etc.) here from drule.ML;
wenzelm
parents:
2979
diff
changeset

318 

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 
(* clash_defns *) 
e2bb53d8dd26
moved theory stuff (add_defs etc.) here from drule.ML;
wenzelm
parents:
2979
diff
changeset

321 

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

322 
fun clash_defn c_ty (name, tm) = 
14204  323 
let val (c, ty') = dest_Const (head_of (fst (Logic.dest_equals (Logic.strip_imp_concl tm)))) in 
3767
e2bb53d8dd26
moved theory stuff (add_defs etc.) here from drule.ML;
wenzelm
parents:
2979
diff
changeset

324 
if clash_consts c_ty (c, ty') then Some (name, ty') else None 
e2bb53d8dd26
moved theory stuff (add_defs etc.) here from drule.ML;
wenzelm
parents:
2979
diff
changeset

325 
end handle TERM _ => None; 
e2bb53d8dd26
moved theory stuff (add_defs etc.) here from drule.ML;
wenzelm
parents:
2979
diff
changeset

326 

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

327 
fun clash_defns c_ty axms = 
e2bb53d8dd26
moved theory stuff (add_defs etc.) here from drule.ML;
wenzelm
parents:
2979
diff
changeset

328 
distinct (mapfilter (clash_defn c_ty) axms); 
e2bb53d8dd26
moved theory stuff (add_defs etc.) here from drule.ML;
wenzelm
parents:
2979
diff
changeset

329 

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

330 

9320  331 
(* overloading *) 
9280  332 

9320  333 
datatype overloading = NoOverloading  Useless  Plain; 
334 

335 
fun overloading sg declT defT = 

10403  336 
let val T = Term.incr_tvar (maxidx_of_typ declT + 1) (Type.varifyT defT) in 
337 
if Sign.typ_instance sg (declT, T) then NoOverloading 

338 
else if Sign.typ_instance sg (Type.rem_sorts declT, Type.rem_sorts T) then Useless 

9320  339 
else Plain 
9280  340 
end; 
341 

342 

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

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

344 

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

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

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

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

348 

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

349 
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

350 
handle TERM _ => err "Not a metaequality (==)"; 
e2bb53d8dd26
moved theory stuff (add_defs etc.) here from drule.ML;
wenzelm
parents:
2979
diff
changeset

351 
val (head, args) = strip_comb lhs; 
9320  352 
val c_ty as (c, ty) = dest_Const head 
3767
e2bb53d8dd26
moved theory stuff (add_defs etc.) here from drule.ML;
wenzelm
parents:
2979
diff
changeset

353 
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

354 

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

357 
 dest_free _ = raise Match; 

358 

359 
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

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

361 

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

362 
val lhs_dups = duplicates args; 
e2bb53d8dd26
moved theory stuff (add_defs etc.) here from drule.ML;
wenzelm
parents:
2979
diff
changeset

363 
val rhs_extras = gen_rems (op =) (term_frees rhs, args); 
e2bb53d8dd26
moved theory stuff (add_defs etc.) here from drule.ML;
wenzelm
parents:
2979
diff
changeset

364 
val rhs_extrasT = gen_rems (op =) (term_tfrees rhs, typ_tfrees ty); 
e2bb53d8dd26
moved theory stuff (add_defs etc.) here from drule.ML;
wenzelm
parents:
2979
diff
changeset

365 
in 
4141  366 
if not (forall (can dest_free) args) then 
3767
e2bb53d8dd26
moved theory stuff (add_defs etc.) here from drule.ML;
wenzelm
parents:
2979
diff
changeset

367 
err "Arguments (on lhs) must be variables" 
e2bb53d8dd26
moved theory stuff (add_defs etc.) here from drule.ML;
wenzelm
parents:
2979
diff
changeset

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

369 
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

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

371 
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

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

373 
err ("Extra type variables on rhs: " ^ show_tfrees rhs_extrasT) 
9282
0181ac100520
Defs are now checked for circularity (if not overloaded).
nipkow
parents:
9280
diff
changeset

374 
else if exists_Const (fn c_ty' => c_ty' = c_ty) rhs then 
3767
e2bb53d8dd26
moved theory stuff (add_defs etc.) here from drule.ML;
wenzelm
parents:
2979
diff
changeset

375 
err ("Constant to be defined occurs on rhs") 
9320  376 
else (c_ty, rhs) 
3767
e2bb53d8dd26
moved theory stuff (add_defs etc.) here from drule.ML;
wenzelm
parents:
2979
diff
changeset

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

378 

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

379 

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

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

381 

3814  382 
fun err_in_defn sg name msg = 
9320  383 
(error_msg msg; 
384 
error ("The error(s) above occurred in definition " ^ quote (Sign.full_name sg name))); 

385 

9332  386 
fun cycle_msg namess = "Cyclic dependency of constants:\n" ^ 
387 
cat_lines (map (space_implode " > " o map quote o rev) namess); 

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

388 

9320  389 
fun add_deps (c, cs) deps = 
390 
let fun declare (G, x) = Graph.new_node (x, ()) G handle Graph.DUP _ => G 

391 
in foldl declare (deps, c :: cs) > Graph.add_deps_acyclic (c, cs) end; 

392 

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

393 
fun check_defn sg overloaded final_consts ((deps, axms), def as (name, tm)) = 
0ee05eef881b
Added support for making constants final, that is, ensuring that no
skalberg
parents:
14204
diff
changeset

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

395 
fun is_final (c, ty) = 
0ee05eef881b
Added support for making constants final, that is, ensuring that no
skalberg
parents:
14204
diff
changeset

396 
case Symtab.lookup(final_consts,c) of 
0ee05eef881b
Added support for making constants final, that is, ensuring that no
skalberg
parents:
14204
diff
changeset

397 
Some [] => true 
0ee05eef881b
Added support for making constants final, that is, ensuring that no
skalberg
parents:
14204
diff
changeset

398 
 Some tys => exists (curry (Sign.typ_instance sg) ty) tys 
0ee05eef881b
Added support for making constants final, that is, ensuring that no
skalberg
parents:
14204
diff
changeset

399 
 None => false; 
9320  400 

10494  401 
fun pretty_const (c, ty) = [Pretty.str c, Pretty.str " ::", Pretty.brk 1, 
402 
Pretty.quote (Sign.pretty_typ sg (#1 (Type.freeze_thaw_type ty)))]; 

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

403 

10494  404 
fun def_txt (c_ty, txt) = Pretty.block 
405 
(Pretty.str "Definition of " :: pretty_const c_ty @ 

406 
(if txt = "" then [] else [Pretty.str txt])); 

407 

408 
fun show_defn c (dfn, ty') = Pretty.block 

409 
(Pretty.str " " :: pretty_const (c, ty') @ [Pretty.str " in ", Pretty.str dfn]); 

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

410 

9320  411 
val (c_ty as (c, ty), rhs) = dest_defn tm 
9280  412 
handle TERM (msg, _) => err_in_defn sg name msg; 
9320  413 
val c_decl = 
414 
(case Sign.const_type sg c of Some T => T 

415 
 None => err_in_defn sg name ("Undeclared constant " ^ quote c)); 

416 

417 
val clashed = clash_defns c_ty axms; 

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

418 
in 
9320  419 
if not (null clashed) then 
10494  420 
err_in_defn sg name (Pretty.string_of (Pretty.chunks 
421 
(def_txt (c_ty, " clashes with") :: map (show_defn c) clashed))) 

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

422 
else if is_final c_ty then 
0ee05eef881b
Added support for making constants final, that is, ensuring that no
skalberg
parents:
14204
diff
changeset

423 
err_in_defn sg name (Pretty.string_of (Pretty.block 
0ee05eef881b
Added support for making constants final, that is, ensuring that no
skalberg
parents:
14204
diff
changeset

424 
([Pretty.str "The constant",Pretty.brk 1] @ 
0ee05eef881b
Added support for making constants final, that is, ensuring that no
skalberg
parents:
14204
diff
changeset

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

426 
[Pretty.brk 1,Pretty.str "has been declared final"]))) 
9320  427 
else 
428 
(case overloading sg c_decl ty of 

429 
NoOverloading => 

13646  430 
(add_deps (c, Term.term_consts rhs) deps 
9320  431 
handle Graph.CYCLES namess => err_in_defn sg name (cycle_msg namess), 
432 
def :: axms) 

433 
 Useless => 

10494  434 
err_in_defn sg name (Pretty.string_of (Pretty.chunks 
435 
[Library.setmp show_sorts true def_txt (c_ty, ""), Pretty.str 

436 
"imposes additional sort constraints on the declared type of the constant"])) 

9320  437 
 Plain => 
10494  438 
(if not overloaded then warning (Pretty.string_of (Pretty.chunks 
439 
[def_txt (c_ty, ""), Pretty.str ("is strictly less general than the declared type (see " 

440 
^ quote (Sign.full_name sg name) ^ ")")])) 

9320  441 
else (); (deps, def :: axms))) 
3767
e2bb53d8dd26
moved theory stuff (add_defs etc.) here from drule.ML;
wenzelm
parents:
2979
diff
changeset

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

443 

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

444 

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

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

446 

9320  447 
fun ext_defns prep_axm overloaded raw_axms thy = 
3767
e2bb53d8dd26
moved theory stuff (add_defs etc.) here from drule.ML;
wenzelm
parents:
2979
diff
changeset

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

449 
val Theory {sign, const_deps, final_consts, axioms, oracles, parents, ancestors} = thy; 
9320  450 
val all_axioms = flat (map (Symtab.dest o #axioms o rep_theory) (thy :: ancestors)); 
451 

452 
val axms = map (prep_axm sign) raw_axms; 

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

453 
val (const_deps', _) = foldl (check_defn sign overloaded final_consts) ((const_deps, all_axioms), axms); 
3767
e2bb53d8dd26
moved theory stuff (add_defs etc.) here from drule.ML;
wenzelm
parents:
2979
diff
changeset

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

455 
make_theory sign const_deps' final_consts axioms oracles parents ancestors 
9320  456 
> add_axioms_i axms 
3767
e2bb53d8dd26
moved theory stuff (add_defs etc.) here from drule.ML;
wenzelm
parents:
2979
diff
changeset

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

458 

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

459 
val add_defs_i = ext_defns cert_axm; 
e2bb53d8dd26
moved theory stuff (add_defs etc.) here from drule.ML;
wenzelm
parents:
2979
diff
changeset

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

461 

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

462 

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

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

464 

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

465 
fun ext_finals prep_term overloaded raw_terms thy = 
0ee05eef881b
Added support for making constants final, that is, ensuring that no
skalberg
parents:
14204
diff
changeset

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

467 
val Theory {sign, const_deps, final_consts, axioms, oracles, parents, ancestors} = thy; 
0ee05eef881b
Added support for making constants final, that is, ensuring that no
skalberg
parents:
14204
diff
changeset

468 
fun mk_final (finals,tm) = 
0ee05eef881b
Added support for making constants final, that is, ensuring that no
skalberg
parents:
14204
diff
changeset

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

470 
fun err msg = raise TERM(msg,[tm]); 
0ee05eef881b
Added support for making constants final, that is, ensuring that no
skalberg
parents:
14204
diff
changeset

471 
val (c,ty) = dest_Const tm 
0ee05eef881b
Added support for making constants final, that is, ensuring that no
skalberg
parents:
14204
diff
changeset

472 
handle TERM _ => err "Can only make constants final"; 
0ee05eef881b
Added support for making constants final, that is, ensuring that no
skalberg
parents:
14204
diff
changeset

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

474 
(case Sign.const_type sign c of Some T => T 
0ee05eef881b
Added support for making constants final, that is, ensuring that no
skalberg
parents:
14204
diff
changeset

475 
 None => err ("Undeclared constant " ^ quote c)); 
0ee05eef881b
Added support for making constants final, that is, ensuring that no
skalberg
parents:
14204
diff
changeset

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

477 
case overloading sign c_decl ty of 
0ee05eef881b
Added support for making constants final, that is, ensuring that no
skalberg
parents:
14204
diff
changeset

478 
NoOverloading => true 
0ee05eef881b
Added support for making constants final, that is, ensuring that no
skalberg
parents:
14204
diff
changeset

479 
 Useless => err "Sort restrictions too strong" 
0ee05eef881b
Added support for making constants final, that is, ensuring that no
skalberg
parents:
14204
diff
changeset

480 
 Plain => if overloaded then false 
0ee05eef881b
Added support for making constants final, that is, ensuring that no
skalberg
parents:
14204
diff
changeset

481 
else err "Type is more general than declared"; 
0ee05eef881b
Added support for making constants final, that is, ensuring that no
skalberg
parents:
14204
diff
changeset

482 
val typ_instance = Sign.typ_instance sign; 
0ee05eef881b
Added support for making constants final, that is, ensuring that no
skalberg
parents:
14204
diff
changeset

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

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

485 
(case Symtab.lookup(finals,c) of 
0ee05eef881b
Added support for making constants final, that is, ensuring that no
skalberg
parents:
14204
diff
changeset

486 
Some [] => err "Constant already final" 
0ee05eef881b
Added support for making constants final, that is, ensuring that no
skalberg
parents:
14204
diff
changeset

487 
 _ => Symtab.update((c,[]),finals)) 
0ee05eef881b
Added support for making constants final, that is, ensuring that no
skalberg
parents:
14204
diff
changeset

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

489 
(case Symtab.lookup(finals,c) of 
0ee05eef881b
Added support for making constants final, that is, ensuring that no
skalberg
parents:
14204
diff
changeset

490 
Some [] => err "Constant already completely final" 
0ee05eef881b
Added support for making constants final, that is, ensuring that no
skalberg
parents:
14204
diff
changeset

491 
 Some tys => if exists (curry typ_instance ty) tys 
0ee05eef881b
Added support for making constants final, that is, ensuring that no
skalberg
parents:
14204
diff
changeset

492 
then err "Instance of constant is already final" 
0ee05eef881b
Added support for making constants final, that is, ensuring that no
skalberg
parents:
14204
diff
changeset

493 
else Symtab.update((c,ty::gen_rem typ_instance (tys,ty)),finals) 
0ee05eef881b
Added support for making constants final, that is, ensuring that no
skalberg
parents:
14204
diff
changeset

494 
 None => Symtab.update((c,[ty]),finals)) 
0ee05eef881b
Added support for making constants final, that is, ensuring that no
skalberg
parents:
14204
diff
changeset

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

496 
val consts = map (prep_term sign) raw_terms; 
0ee05eef881b
Added support for making constants final, that is, ensuring that no
skalberg
parents:
14204
diff
changeset

497 
val final_consts' = foldl mk_final (final_consts,consts); 
0ee05eef881b
Added support for making constants final, that is, ensuring that no
skalberg
parents:
14204
diff
changeset

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

499 
make_theory sign const_deps final_consts' axioms oracles parents ancestors 
0ee05eef881b
Added support for making constants final, that is, ensuring that no
skalberg
parents:
14204
diff
changeset

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

501 

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

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

503 
fun read_term sg = Sign.simple_read_term sg TypeInfer.logicT; 
0ee05eef881b
Added support for making constants final, that is, ensuring that no
skalberg
parents:
14204
diff
changeset

504 
val cert_term = #1 oo Sign.certify_term; 
0ee05eef881b
Added support for making constants final, that is, ensuring that no
skalberg
parents:
14204
diff
changeset

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

506 
val add_finals = ext_finals read_term; 
0ee05eef881b
Added support for making constants final, that is, ensuring that no
skalberg
parents:
14204
diff
changeset

507 
val add_finals_i = ext_finals cert_term; 
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 
fun merge_final sg = 
0ee05eef881b
Added support for making constants final, that is, ensuring that no
skalberg
parents:
14204
diff
changeset

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

512 
fun merge_single (tys,ty) = 
0ee05eef881b
Added support for making constants final, that is, ensuring that no
skalberg
parents:
14204
diff
changeset

513 
if exists (curry (Sign.typ_instance sg) ty) tys 
0ee05eef881b
Added support for making constants final, that is, ensuring that no
skalberg
parents:
14204
diff
changeset

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

515 
else (ty::gen_rem (Sign.typ_instance sg) (tys,ty)); 
0ee05eef881b
Added support for making constants final, that is, ensuring that no
skalberg
parents:
14204
diff
changeset

516 
fun merge ([],_) = [] 
0ee05eef881b
Added support for making constants final, that is, ensuring that no
skalberg
parents:
14204
diff
changeset

517 
 merge (_,[]) = [] 
0ee05eef881b
Added support for making constants final, that is, ensuring that no
skalberg
parents:
14204
diff
changeset

518 
 merge input = foldl merge_single input; 
0ee05eef881b
Added support for making constants final, that is, ensuring that no
skalberg
parents:
14204
diff
changeset

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

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

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

522 

3878  523 

3865  524 
(** additional theory data **) 
525 

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

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

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

3865  530 

531 

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

532 

6661  533 
(** merge theories **) (*exception ERROR*) 
4019  534 

535 
fun merge_sign (sg, thy) = 

4627  536 
Sign.nontriv_merge (sg, sign_of thy) handle TERM (msg, _) => error msg; 
1526  537 

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

539 
fun prep_ext_merge thys = 
3996  540 
if null thys then 
4019  541 
error "Merge: no parent theories" 
6188  542 
else if exists is_draft thys then 
4019  543 
error "Attempt to merge draft theories" 
3996  544 
else 
545 
let 

546 
val sign' = 

4019  547 
foldl merge_sign (sign_of (hd thys), tl thys) 
3996  548 
> Sign.prep_ext 
549 
> Sign.add_path "/"; 

3814  550 

9282
0181ac100520
Defs are now checked for circularity (if not overloaded).
nipkow
parents:
9280
diff
changeset

551 
val depss = map (#const_deps o rep_theory) thys; 
9320  552 
val deps' = foldl (Graph.merge_acyclic (K true)) (hd depss, tl depss) 
553 
handle Graph.CYCLES namess => error (cycle_msg namess); 

9282
0181ac100520
Defs are now checked for circularity (if not overloaded).
nipkow
parents:
9280
diff
changeset

554 

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

555 
val final_constss = map (#final_consts o rep_theory) thys; 
0ee05eef881b
Added support for making constants final, that is, ensuring that no
skalberg
parents:
14204
diff
changeset

556 
val final_consts' = foldl (Symtab.join (merge_final sign')) (hd final_constss, 
0ee05eef881b
Added support for making constants final, that is, ensuring that no
skalberg
parents:
14204
diff
changeset

557 
tl final_constss); 
4488  558 
val axioms' = Symtab.empty; 
4019  559 

3996  560 
fun eq_ora ((_, (_, s1: stamp)), (_, (_, s2))) = s1 = s2; 
561 
val oracles' = 

562 
Symtab.make (gen_distinct eq_ora 

563 
(flat (map (Symtab.dest o #oracles o rep_theory) thys))) 

564 
handle Symtab.DUPS names => err_dup_oras names; 

4019  565 

566 
val parents' = gen_distinct eq_thy thys; 

567 
val ancestors' = 

568 
gen_distinct eq_thy (parents' @ flat (map ancestors_of thys)); 

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

570 
make_theory sign' deps' final_consts' axioms' oracles' parents' ancestors' 
3996  571 
end; 
1526  572 

3885  573 

1526  574 
end; 
575 

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

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

577 
open BasicTheory; 