author  wenzelm 
Fri, 04 Aug 2000 23:00:01 +0200  
changeset 9537  7e0ba737f98e 
parent 9332  ff3a86a00ea5 
child 9629  50f1c4222aea 
permissions  rwrr 
1526  1 
(* Title: Pure/theory.ML 
2 
ID: $Id$ 

3 
Author: Lawrence C Paulson and Markus Wenzel 

4 
Copyright 1996 University of Cambridge 

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, 
3996  16 
axioms: term Symtab.table, 
4996  17 
oracles: ((Sign.sg * Object.T > term) * stamp) Symtab.table, 
4019  18 
parents: theory list, 
19 
ancestors: theory list} 

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

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

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

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

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

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

33 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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 
2693  67 
val add_tokentrfuns: 
6311  68 
(string * string * (string > string * real)) list > theory > theory 
69 
val add_mode_tokentrfuns: string > (string * (string > string * real)) list 

70 
> theory > theory 

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

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

4996  75 
val add_oracle: bstring * (Sign.sg * Object.T > term) > theory > theory 
9320  76 
val add_defs: bool > (bstring * string) list > theory > theory 
77 
val add_defs_i: bool > (bstring * term) list > theory > theory 

3996  78 
val add_path: string > theory > theory 
4846  79 
val parent_path: theory > theory 
80 
val root_path: theory > theory 

8725  81 
val hide_space: string * xstring list > theory > theory 
82 
val hide_space_i: string * string list > theory > theory 

83 
val hide_classes: string list > theory > theory 

84 
val hide_types: string list > theory > theory 

85 
val hide_consts: string list > theory > theory 

3996  86 
val add_name: string > theory > theory 
5862  87 
val copy: theory > theory 
6661  88 
val prep_ext: theory > theory 
3996  89 
val prep_ext_merge: theory list > theory 
4970  90 
val requires: theory > string > string > unit 
6369  91 
val assert_super: theory > theory > theory 
3996  92 
val pre_pure: theory 
1526  93 
end; 
94 

6188  95 
signature PRIVATE_THEORY = 
5642  96 
sig 
97 
include THEORY 

6546  98 
val init_data: Object.kind > (Object.T * (Object.T > Object.T) * (Object.T > Object.T) * 
5642  99 
(Object.T * Object.T > Object.T) * (Sign.sg > Object.T > unit)) > theory > theory 
100 
val print_data: Object.kind > theory > unit 

101 
val get_data: Object.kind > (Object.T > 'a) > theory > 'a 

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

103 
end; 

1526  104 

5642  105 

6188  106 
structure Theory: PRIVATE_THEORY = 
1526  107 
struct 
2206  108 

3996  109 

2206  110 
(** datatype theory **) 
1526  111 

9320  112 
(*Note: dependencies are only tracked for nonoverloaded constant definitions*) 
113 

1526  114 
datatype theory = 
115 
Theory of { 

116 
sign: Sign.sg, 

9320  117 
const_deps: unit Graph.T, 
3996  118 
axioms: term Symtab.table, 
4996  119 
oracles: ((Sign.sg * Object.T > term) * stamp) Symtab.table, 
4019  120 
parents: theory list, 
121 
ancestors: theory list}; 

1526  122 

9320  123 
fun make_theory sign const_deps axioms oracles parents ancestors = 
124 
Theory {sign = sign, const_deps = const_deps, axioms = axioms, oracles = oracles, 

4019  125 
parents = parents, ancestors = ancestors}; 
3996  126 

1526  127 
fun rep_theory (Theory args) = args; 
128 

3996  129 
val sign_of = #sign o rep_theory; 
6188  130 
val is_draft = Sign.is_draft o sign_of; 
3996  131 
val syn_of = #syn o Sign.rep_sg o sign_of; 
132 
val parents_of = #parents o rep_theory; 

4019  133 
val ancestors_of = #ancestors o rep_theory; 
3996  134 

1526  135 
(*errors involving theories*) 
136 
exception THEORY of string * theory list; 

137 

138 
(*compare theories*) 

139 
val subthy = Sign.subsig o pairself sign_of; 

140 
val eq_thy = Sign.eq_sg o pairself sign_of; 

141 

6369  142 
(*check for some theory*) 
4970  143 
fun requires thy name what = 
4846  144 
if exists (equal name) (Sign.stamp_names_of (sign_of thy)) then () 
145 
else error ("Require theory " ^ quote name ^ " as an ancestor for " ^ what); 

1526  146 

6369  147 
fun assert_super thy1 thy2 = 
148 
if subthy (thy1, thy2) then thy2 

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

150 

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

152 
val pre_pure = 
9320  153 
make_theory Sign.pre_pure Graph.empty Symtab.empty Symtab.empty [] []; 
1526  154 

155 

156 

157 
(** extend theory **) 

158 

8725  159 
(*name spaces*) 
3996  160 
val axiomK = "axiom"; 
3814  161 
val oracleK = "oracle"; 
162 

163 

164 
(* extend logical part of a theory *) 

165 

1526  166 
fun err_dup_axms names = 
167 
error ("Duplicate axiom name(s) " ^ commas_quote names); 

168 

3814  169 
fun err_dup_oras names = 
170 
error ("Duplicate oracles " ^ commas_quote names); 

171 

9320  172 
fun ext_theory thy ext_sg ext_deps new_axms new_oras = 
1526  173 
let 
9282
0181ac100520
Defs are now checked for circularity (if not overloaded).
nipkow
parents:
9280
diff
changeset

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

1526  184 
in 
9320  185 
make_theory (ext_sg sign) (ext_deps const_deps) axioms' oracles' parents' ancestors' 
1526  186 
end; 
187 

188 

189 
(* extend signature of a theory *) 

190 

9320  191 
fun ext_sign extfun decls thy = ext_theory thy (extfun decls) I [] []; 
1526  192 

4996  193 
val add_classes = ext_sign Sign.add_classes; 
194 
val add_classes_i = ext_sign Sign.add_classes_i; 

195 
val add_classrel = ext_sign Sign.add_classrel; 

196 
val add_classrel_i = ext_sign Sign.add_classrel_i; 

197 
val add_defsort = ext_sign Sign.add_defsort; 

198 
val add_defsort_i = ext_sign Sign.add_defsort_i; 

199 
val add_types = ext_sign Sign.add_types; 

200 
val add_nonterminals = ext_sign Sign.add_nonterminals; 

201 
val add_tyabbrs = ext_sign Sign.add_tyabbrs; 

202 
val add_tyabbrs_i = ext_sign Sign.add_tyabbrs_i; 

203 
val add_arities = ext_sign Sign.add_arities; 

204 
val add_arities_i = ext_sign Sign.add_arities_i; 

205 
val add_consts = ext_sign Sign.add_consts; 

206 
val add_consts_i = ext_sign Sign.add_consts_i; 

207 
val add_syntax = ext_sign Sign.add_syntax; 

208 
val add_syntax_i = ext_sign Sign.add_syntax_i; 

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

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

211 
val add_trfuns = ext_sign Sign.add_trfuns; 

212 
val add_trfunsT = ext_sign Sign.add_trfunsT; 

213 
val add_tokentrfuns = ext_sign Sign.add_tokentrfuns; 

6311  214 
fun add_mode_tokentrfuns m = add_tokentrfuns o map (fn (s, f) => (m, s, f)); 
4996  215 
val add_trrules = ext_sign Sign.add_trrules; 
216 
val add_trrules_i = ext_sign Sign.add_trrules_i; 

217 
val add_path = ext_sign Sign.add_path; 

4846  218 
val parent_path = add_path ".."; 
219 
val root_path = add_path "/"; 

4996  220 
val add_space = ext_sign Sign.add_space; 
8725  221 
val hide_space = ext_sign Sign.hide_space; 
222 
val hide_space_i = ext_sign Sign.hide_space_i; 

223 
val hide_classes = curry hide_space_i Sign.classK; 

224 
val hide_types = curry hide_space_i Sign.typeK; 

225 
val hide_consts = curry hide_space_i Sign.constK; 

4996  226 
val add_name = ext_sign Sign.add_name; 
6546  227 
val copy = ext_sign (K Sign.copy) (); 
6661  228 
val prep_ext = ext_sign (K Sign.prep_ext) (); 
3814  229 

3996  230 

6311  231 

3814  232 
(** add axioms **) 
233 

1526  234 
(* prepare axioms *) 
235 

236 
fun err_in_axm name = 

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

238 

239 
fun no_vars tm = 

240 
if null (term_vars tm) andalso null (term_tvars tm) then tm 

241 
else error "Illegal schematic variable(s) in term"; 

242 

243 
fun cert_axm sg (name, raw_tm) = 

244 
let 

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

2979  246 
handle TYPE (msg, _, _) => error msg 
3996  247 
 TERM (msg, _) => error msg; 
1526  248 
in 
9537  249 
Term.no_dummy_patterns t handle TERM (msg, _) => error msg; 
1526  250 
assert (T = propT) "Term not of type prop"; 
251 
(name, no_vars t) 

252 
end 

253 
handle ERROR => err_in_axm name; 

254 

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

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

261 
handle ERROR => err_in_axm name; 
1526  262 

5057  263 
fun read_axm sg name_str = read_def_axm (sg, K None, K None) [] name_str; 
264 

1526  265 
fun inferT_axm sg (name, pre_tm) = 
3814  266 
let 
4251  267 
val (t, _) = Sign.infer_types sg (K None) (K None) [] true ([pre_tm], propT); 
3814  268 
in (name, no_vars t) end 
1526  269 
handle ERROR => err_in_axm name; 
270 

271 

272 
(* extend axioms of a theory *) 

273 

3814  274 
fun ext_axms prep_axm raw_axms (thy as Theory {sign, ...}) = 
1526  275 
let 
3814  276 
val raw_axms' = map (apfst (Sign.full_name sign)) raw_axms; 
277 
val axioms = 

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

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

282 
val add_axioms = ext_axms read_axm; 

283 
val add_axioms_i = ext_axms cert_axm; 

284 

285 

3814  286 
(* add oracle **) 
287 

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

289 
let 

290 
val name = Sign.full_name sign raw_name; 

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

294 

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

295 

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

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

297 

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

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

299 

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

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

301 

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

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

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

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

305 
val ty2' = incr_tvar (maxidx_of_typ ty1' + 1) (Type.varifyT ty2); 
9320  306 
in Type.raw_unify (ty1', ty2') end; 
3767
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 
fun clash_consts (c1, ty1) (c2, ty2) = 
e2bb53d8dd26
moved theory stuff (add_defs etc.) here from drule.ML;
wenzelm
parents:
2979
diff
changeset

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

310 

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

311 

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

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

313 

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

314 
fun clash_defn c_ty (name, tm) = 
e2bb53d8dd26
moved theory stuff (add_defs etc.) here from drule.ML;
wenzelm
parents:
2979
diff
changeset

315 
let val (c, ty') = dest_Const (head_of (fst (Logic.dest_equals tm))) in 
e2bb53d8dd26
moved theory stuff (add_defs etc.) here from drule.ML;
wenzelm
parents:
2979
diff
changeset

316 
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

317 
end handle TERM _ => None; 
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 
fun clash_defns c_ty axms = 
e2bb53d8dd26
moved theory stuff (add_defs etc.) here from drule.ML;
wenzelm
parents:
2979
diff
changeset

320 
distinct (mapfilter (clash_defn c_ty) axms); 
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 

9320  323 
(* overloading *) 
9280  324 

9320  325 
datatype overloading = NoOverloading  Useless  Plain; 
326 

327 
fun overloading sg declT defT = 

9280  328 
let 
9320  329 
val tsig = Sign.tsig_of sg; 
330 
val T = Term.incr_tvar (maxidx_of_typ declT + 1) (Type.varifyT defT); 

9280  331 
in 
9320  332 
if Type.typ_instance (tsig, declT, T) then NoOverloading 
333 
else if Type.typ_instance (tsig, Type.rem_sorts declT, Type.rem_sorts T) then Useless 

334 
else Plain 

9280  335 
end; 
336 

337 

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

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

339 

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

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

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

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

343 

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

344 
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

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

346 
val (head, args) = strip_comb lhs; 
9320  347 
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

348 
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

349 

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

352 
 dest_free _ = raise Match; 

353 

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 

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

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

358 
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

359 
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

360 
in 
4141  361 
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

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

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

364 
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

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

366 
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

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

368 
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

369 
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

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

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

373 

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

376 

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

380 

9332  381 
fun cycle_msg namess = "Cyclic dependency of constants:\n" ^ 
382 
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

383 

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

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

387 

388 

389 
fun check_defn sg overloaded ((deps, axms), def as (name, tm)) = 

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

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

391 
fun show_const (c, ty) = quote (Pretty.string_of (Pretty.block 
9280  392 
[Pretty.str (c ^ " ::"), Pretty.brk 1, Sign.pretty_typ sg ty])); 
3767
e2bb53d8dd26
moved theory stuff (add_defs etc.) here from drule.ML;
wenzelm
parents:
2979
diff
changeset

393 

9280  394 
fun def_txt c_ty = "Definition of " ^ show_const c_ty; 
3767
e2bb53d8dd26
moved theory stuff (add_defs etc.) here from drule.ML;
wenzelm
parents:
2979
diff
changeset

395 
fun show_defn c (dfn, ty') = show_const (c, ty') ^ " in " ^ dfn; 
e2bb53d8dd26
moved theory stuff (add_defs etc.) here from drule.ML;
wenzelm
parents:
2979
diff
changeset

396 
fun show_defns c = cat_lines o map (show_defn c); 
e2bb53d8dd26
moved theory stuff (add_defs etc.) here from drule.ML;
wenzelm
parents:
2979
diff
changeset

397 

9320  398 
val (c_ty as (c, ty), rhs) = dest_defn tm 
9280  399 
handle TERM (msg, _) => err_in_defn sg name msg; 
9320  400 
val c_decl = 
401 
(case Sign.const_type sg c of Some T => T 

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

403 

404 
val clashed = clash_defns c_ty axms; 

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

405 
in 
9320  406 
if not (null clashed) then 
407 
err_in_defn sg name (def_txt c_ty ^"\nclashes with "^ show_defns c clashed) 

408 
else 

409 
(case overloading sg c_decl ty of 

410 
NoOverloading => 

411 
(add_deps (c, Term.add_term_consts (rhs, [])) deps 

412 
handle Graph.CYCLES namess => err_in_defn sg name (cycle_msg namess), 

413 
def :: axms) 

414 
 Useless => 

415 
err_in_defn sg name (Library.setmp show_sorts true def_txt c_ty ^ 

416 
"\nimposes additional sort constraints on the declared type of the constant.") 

417 
 Plain => 

418 
(if not overloaded then 

419 
warning (def_txt c_ty ^ "\nis strictly less general than the declared type (see " 

420 
^ quote (Sign.full_name sg name) ^ ")") 

421 
else (); (deps, def :: axms))) 

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

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

423 

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

424 

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

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

426 

9320  427 
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

428 
let 
9320  429 
val Theory {sign, const_deps, axioms, oracles, parents, ancestors} = thy; 
430 
val all_axioms = flat (map (Symtab.dest o #axioms o rep_theory) (thy :: ancestors)); 

431 

432 
val axms = map (prep_axm sign) raw_axms; 

433 
val (const_deps', _) = foldl (check_defn sign overloaded) ((const_deps, all_axioms), axms); 

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

434 
in 
9320  435 
make_theory sign const_deps' axioms oracles parents ancestors 
436 
> add_axioms_i axms 

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

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

438 

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

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

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

441 

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

442 

3878  443 

3865  444 
(** additional theory data **) 
445 

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

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

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

3865  450 

451 

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

452 

6661  453 
(** merge theories **) (*exception ERROR*) 
4019  454 

455 
fun merge_sign (sg, thy) = 

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

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

459 
fun prep_ext_merge thys = 
3996  460 
if null thys then 
4019  461 
error "Merge: no parent theories" 
6188  462 
else if exists is_draft thys then 
4019  463 
error "Attempt to merge draft theories" 
3996  464 
else 
465 
let 

466 
val sign' = 

4019  467 
foldl merge_sign (sign_of (hd thys), tl thys) 
3996  468 
> Sign.prep_ext 
469 
> Sign.add_path "/"; 

3814  470 

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

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

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

474 

4488  475 
val axioms' = Symtab.empty; 
4019  476 

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

479 
Symtab.make (gen_distinct eq_ora 

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

481 
handle Symtab.DUPS names => err_dup_oras names; 

4019  482 

483 
val parents' = gen_distinct eq_thy thys; 

484 
val ancestors' = 

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

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

487 
make_theory sign' deps' axioms' oracles' parents' ancestors' 
3996  488 
end; 
1526  489 

3885  490 

1526  491 
end; 
492 

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

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

494 
open BasicTheory; 