author  wenzelm 
Sun, 20 Mar 2011 22:47:08 +0100  
changeset 42016  3b6826b3ed37 
parent 39134  917b4b6ba3d2 
child 42360  da8817d01e7c 
permissions  rwrr 
1526  1 
(* Title: Pure/theory.ML 
2 
Author: Lawrence C Paulson and Markus Wenzel 

3 

28290  4 
Logical theory content: axioms, definitions, and begin/end wrappers. 
1526  5 
*) 
16291  6 

26668
65023d4fd226
removed obsolete SIGN_THEORY  no name aliases in structure Theory;
wenzelm
parents:
26631
diff
changeset

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

8 
sig 
16443
82a116532e3e
type theory, theory_ref, exception THEORY and related operations imported from Context;
wenzelm
parents:
16369
diff
changeset

9 
val eq_thy: theory * theory > bool 
3996  10 
val subthy: theory * theory > bool 
24666  11 
val assert_super: theory > theory > theory 
22684  12 
val parents_of: theory > theory list 
13 
val ancestors_of: theory > theory list 

24666  14 
val check_thy: theory > theory_ref 
15 
val deref: theory_ref > theory 

16 
val merge: theory * theory > theory 

17 
val merge_refs: theory_ref * theory_ref > theory_ref 

18 
val merge_list: theory list > theory 

16495  19 
val checkpoint: theory > theory 
20 
val copy: theory > theory 

24666  21 
val requires: theory > string > string > unit 
33095
bbd52d2f8696
renamed NameSpace to Name_Space  also to emphasize its subtle change in semantics;
wenzelm
parents:
33092
diff
changeset

22 
val axiom_space: theory > Name_Space.T 
22684  23 
val axiom_table: theory > term Symtab.table 
16339  24 
val axioms_of: theory > (string * term) list 
25 
val all_axioms_of: theory > (string * term) list 

24666  26 
val defs_of: theory > Defs.T 
27 
val at_begin: (theory > theory option) > theory > theory 

28 
val at_end: (theory > theory option) > theory > theory 

29 
val begin_theory: string > theory list > theory 

30 
val end_theory: theory > theory 

35857
28e73b3e7b6c
replaced Theory.add_axioms(_i) by more primitive Theory.add_axiom;
wenzelm
parents:
35845
diff
changeset

31 
val add_axiom: binding * term > theory > theory 
19708
a508bde37a81
added add_deps, which actually records dependencies of consts (unlike add_finals);
wenzelm
parents:
19700
diff
changeset

32 
val add_deps: string > string * typ > (string * typ) list > theory > theory 
35985
0bbf0d2348f9
moved Drule.forall_intr_frees to Thm.forall_intr_frees (in more_thm.ML, which is loaded before pure_thy.ML);
wenzelm
parents:
35857
diff
changeset

33 
val add_def: bool > bool > binding * term > theory > theory 
29581  34 
val add_finals_i: bool > term list > theory > theory 
16443
82a116532e3e
type theory, theory_ref, exception THEORY and related operations imported from Context;
wenzelm
parents:
16369
diff
changeset

35 
val add_finals: bool > string list > theory > theory 
33173
b8ca12f6681a
eliminated obsolete tags for types/consts  now handled via name space, in strongly typed fashion;
wenzelm
parents:
33168
diff
changeset

36 
val specify_const: (binding * typ) * mixfix > theory > term * theory 
16495  37 
end 
1526  38 

24666  39 
structure Theory: THEORY = 
16443
82a116532e3e
type theory, theory_ref, exception THEORY and related operations imported from Context;
wenzelm
parents:
16369
diff
changeset

40 
struct 
82a116532e3e
type theory, theory_ref, exception THEORY and related operations imported from Context;
wenzelm
parents:
16369
diff
changeset

41 

19708
a508bde37a81
added add_deps, which actually records dependencies of consts (unlike add_finals);
wenzelm
parents:
19700
diff
changeset

42 

24666  43 
(** theory context operations **) 
16443
82a116532e3e
type theory, theory_ref, exception THEORY and related operations imported from Context;
wenzelm
parents:
16369
diff
changeset

44 

82a116532e3e
type theory, theory_ref, exception THEORY and related operations imported from Context;
wenzelm
parents:
16369
diff
changeset

45 
val eq_thy = Context.eq_thy; 
82a116532e3e
type theory, theory_ref, exception THEORY and related operations imported from Context;
wenzelm
parents:
16369
diff
changeset

46 
val subthy = Context.subthy; 
1526  47 

24626
85eceef2edc7
introduced generic concepts for theory interpretators
haftmann
parents:
24199
diff
changeset

48 
fun assert_super thy1 thy2 = 
85eceef2edc7
introduced generic concepts for theory interpretators
haftmann
parents:
24199
diff
changeset

49 
if subthy (thy1, thy2) then thy2 
85eceef2edc7
introduced generic concepts for theory interpretators
haftmann
parents:
24199
diff
changeset

50 
else raise THEORY ("Not a super theory", [thy1, thy2]); 
85eceef2edc7
introduced generic concepts for theory interpretators
haftmann
parents:
24199
diff
changeset

51 

16443
82a116532e3e
type theory, theory_ref, exception THEORY and related operations imported from Context;
wenzelm
parents:
16369
diff
changeset

52 
val parents_of = Context.parents_of; 
82a116532e3e
type theory, theory_ref, exception THEORY and related operations imported from Context;
wenzelm
parents:
16369
diff
changeset

53 
val ancestors_of = Context.ancestors_of; 
82a116532e3e
type theory, theory_ref, exception THEORY and related operations imported from Context;
wenzelm
parents:
16369
diff
changeset

54 

24137
8d7896398147
replaced Theory.self_ref by Theory.check_thy, which now produces a checked ref;
wenzelm
parents:
23655
diff
changeset

55 
val check_thy = Context.check_thy; 
16443
82a116532e3e
type theory, theory_ref, exception THEORY and related operations imported from Context;
wenzelm
parents:
16369
diff
changeset

56 
val deref = Context.deref; 
24666  57 

16443
82a116532e3e
type theory, theory_ref, exception THEORY and related operations imported from Context;
wenzelm
parents:
16369
diff
changeset

58 
val merge = Context.merge; 
82a116532e3e
type theory, theory_ref, exception THEORY and related operations imported from Context;
wenzelm
parents:
16369
diff
changeset

59 
val merge_refs = Context.merge_refs; 
82a116532e3e
type theory, theory_ref, exception THEORY and related operations imported from Context;
wenzelm
parents:
16369
diff
changeset

60 

23600  61 
fun merge_list [] = raise THEORY ("Empty merge of theories", []) 
21608  62 
 merge_list (thy :: thys) = Library.foldl merge (thy, thys); 
63 

16495  64 
val checkpoint = Context.checkpoint_thy; 
65 
val copy = Context.copy_thy; 

66 

24666  67 
fun requires thy name what = 
29092  68 
if exists (fn thy' => Context.theory_name thy' = name) (thy :: ancestors_of thy) then () 
24666  69 
else error ("Require theory " ^ quote name ^ " as an ancestor for " ^ what); 
70 

71 

72 

25059  73 
(** datatype thy **) 
24666  74 

75 
type wrapper = (theory > theory option) * stamp; 

76 

77 
fun apply_wrappers (wrappers: wrapper list) = 

25059  78 
perhaps (perhaps_loop (perhaps_apply (map fst wrappers))); 
24666  79 

80 
datatype thy = Thy of 

33095
bbd52d2f8696
renamed NameSpace to Name_Space  also to emphasize its subtle change in semantics;
wenzelm
parents:
33092
diff
changeset

81 
{axioms: term Name_Space.table, 
24666  82 
defs: Defs.T, 
83 
wrappers: wrapper list * wrapper list}; 

84 

28290  85 
fun make_thy (axioms, defs, wrappers) = Thy {axioms = axioms, defs = defs, wrappers = wrappers}; 
24666  86 

42016  87 
structure Thy = Theory_Data_PP 
24666  88 
( 
89 
type T = thy; 

33159  90 
val empty_axioms = Name_Space.empty_table "axiom" : term Name_Space.table; 
33096  91 
val empty = make_thy (empty_axioms, Defs.empty, ([], [])); 
24666  92 

33096  93 
fun extend (Thy {axioms = _, defs, wrappers}) = make_thy (empty_axioms, defs, wrappers); 
24666  94 

95 
fun merge pp (thy1, thy2) = 

96 
let 

28290  97 
val Thy {axioms = _, defs = defs1, wrappers = (bgs1, ens1)} = thy1; 
98 
val Thy {axioms = _, defs = defs2, wrappers = (bgs2, ens2)} = thy2; 

24666  99 

33096  100 
val axioms' = empty_axioms; 
24666  101 
val defs' = Defs.merge pp (defs1, defs2); 
102 
val bgs' = Library.merge (eq_snd op =) (bgs1, bgs2); 

103 
val ens' = Library.merge (eq_snd op =) (ens1, ens2); 

28290  104 
in make_thy (axioms', defs', (bgs', ens')) end; 
24666  105 
); 
106 

42016  107 
fun rep_theory thy = Thy.get thy > (fn Thy args => args); 
24666  108 

42016  109 
fun map_thy f = Thy.map (fn (Thy {axioms, defs, wrappers}) => 
28290  110 
make_thy (f (axioms, defs, wrappers))); 
24666  111 

112 

28290  113 
fun map_axioms f = map_thy (fn (axioms, defs, wrappers) => (f axioms, defs, wrappers)); 
114 
fun map_defs f = map_thy (fn (axioms, defs, wrappers) => (axioms, f defs, wrappers)); 

115 
fun map_wrappers f = map_thy (fn (axioms, defs, wrappers) => (axioms, defs, f wrappers)); 

24666  116 

117 

118 
(* basic operations *) 

119 

120 
val axiom_space = #1 o #axioms o rep_theory; 

121 
val axiom_table = #2 o #axioms o rep_theory; 

122 

123 
val axioms_of = Symtab.dest o #2 o #axioms o rep_theory; 

124 
fun all_axioms_of thy = maps axioms_of (thy :: ancestors_of thy); 

125 

126 
val defs_of = #defs o rep_theory; 

127 

128 

129 
(* begin/end theory *) 

130 

131 
val begin_wrappers = rev o #1 o #wrappers o rep_theory; 

132 
val end_wrappers = rev o #2 o #wrappers o rep_theory; 

133 

134 
fun at_begin f = map_wrappers (apfst (cons (f, stamp ()))); 

135 
fun at_end f = map_wrappers (apsnd (cons (f, stamp ()))); 

136 

137 
fun begin_theory name imports = 

138 
let 

26939
1035c89b4c02
moved global pretty/string_of functions from Sign to Syntax;
wenzelm
parents:
26668
diff
changeset

139 
val thy = Context.begin_thy Syntax.pp_global name imports; 
24666  140 
val wrappers = begin_wrappers thy; 
33168  141 
in 
142 
thy 

143 
> Sign.local_path 

144 
> Sign.map_naming (Name_Space.set_theory_name name) 

145 
> apply_wrappers wrappers 

146 
end; 

24666  147 

148 
fun end_theory thy = 

149 
thy > apply_wrappers (end_wrappers thy) > Context.finish_thy; 

150 

16443
82a116532e3e
type theory, theory_ref, exception THEORY and related operations imported from Context;
wenzelm
parents:
16369
diff
changeset

151 

3996  152 

35985
0bbf0d2348f9
moved Drule.forall_intr_frees to Thm.forall_intr_frees (in more_thm.ML, which is loaded before pure_thy.ML);
wenzelm
parents:
35857
diff
changeset

153 
(** primitive specifications **) 
3814  154 

35985
0bbf0d2348f9
moved Drule.forall_intr_frees to Thm.forall_intr_frees (in more_thm.ML, which is loaded before pure_thy.ML);
wenzelm
parents:
35857
diff
changeset

155 
(* raw axioms *) 
1526  156 

29581  157 
fun cert_axm thy (b, raw_tm) = 
1526  158 
let 
32789
d89327de0b3c
removed redundant Sign.certify_prop, use Sign.cert_prop instead;
wenzelm
parents:
30466
diff
changeset

159 
val t = Sign.cert_prop thy raw_tm 
2979  160 
handle TYPE (msg, _, _) => error msg 
16291  161 
 TERM (msg, _) => error msg; 
35987
7c728daf4876
disallow sort constraints in primitive Theory.add_axiom/add_def  handled in Thm.add_axiom/add_def;
wenzelm
parents:
35985
diff
changeset

162 
val _ = Term.no_dummy_patterns t handle TERM (msg, _) => error msg; 
7c728daf4876
disallow sort constraints in primitive Theory.add_axiom/add_def  handled in Thm.add_axiom/add_def;
wenzelm
parents:
35985
diff
changeset

163 

39134
917b4b6ba3d2
turned show_sorts/show_types into proper configuration options;
wenzelm
parents:
39133
diff
changeset

164 
val ctxt = Syntax.init_pretty_global thy 
917b4b6ba3d2
turned show_sorts/show_types into proper configuration options;
wenzelm
parents:
39133
diff
changeset

165 
> Config.put show_sorts true; 
35987
7c728daf4876
disallow sort constraints in primitive Theory.add_axiom/add_def  handled in Thm.add_axiom/add_def;
wenzelm
parents:
35985
diff
changeset

166 
val bad_sorts = 
7c728daf4876
disallow sort constraints in primitive Theory.add_axiom/add_def  handled in Thm.add_axiom/add_def;
wenzelm
parents:
35985
diff
changeset

167 
rev ((fold_types o fold_atyps_sorts) (fn (_, []) => I  (T, _) => insert (op =) T) t []); 
7c728daf4876
disallow sort constraints in primitive Theory.add_axiom/add_def  handled in Thm.add_axiom/add_def;
wenzelm
parents:
35985
diff
changeset

168 
val _ = null bad_sorts orelse 
7c728daf4876
disallow sort constraints in primitive Theory.add_axiom/add_def  handled in Thm.add_axiom/add_def;
wenzelm
parents:
35985
diff
changeset

169 
error ("Illegal sort constraints in primitive specification: " ^ 
39134
917b4b6ba3d2
turned show_sorts/show_types into proper configuration options;
wenzelm
parents:
39133
diff
changeset

170 
commas (map (Syntax.string_of_typ ctxt) bad_sorts)); 
1526  171 
in 
39133
70d3915c92f0
pretty printing: prefer regular Proof.context over Pretty.pp, which is mostly for special bootstrap purposes involving theory merge, for example;
wenzelm
parents:
36610
diff
changeset

172 
(b, Sign.no_vars (Syntax.init_pretty_global thy) t) 
35987
7c728daf4876
disallow sort constraints in primitive Theory.add_axiom/add_def  handled in Thm.add_axiom/add_def;
wenzelm
parents:
35985
diff
changeset

173 
end handle ERROR msg => 
7c728daf4876
disallow sort constraints in primitive Theory.add_axiom/add_def  handled in Thm.add_axiom/add_def;
wenzelm
parents:
35985
diff
changeset

174 
cat_error msg ("The error(s) above occurred in axiom " ^ quote (Binding.str_of b)); 
1526  175 

35857
28e73b3e7b6c
replaced Theory.add_axioms(_i) by more primitive Theory.add_axiom;
wenzelm
parents:
35845
diff
changeset

176 
fun add_axiom raw_axm thy = thy > map_axioms (fn axioms => 
1526  177 
let 
35857
28e73b3e7b6c
replaced Theory.add_axioms(_i) by more primitive Theory.add_axiom;
wenzelm
parents:
35845
diff
changeset

178 
val axm = apsnd Logic.varify_global (cert_axm thy raw_axm); 
28e73b3e7b6c
replaced Theory.add_axioms(_i) by more primitive Theory.add_axiom;
wenzelm
parents:
35845
diff
changeset

179 
val (_, axioms') = Name_Space.define true (Sign.naming_of thy) axm axioms; 
16443
82a116532e3e
type theory, theory_ref, exception THEORY and related operations imported from Context;
wenzelm
parents:
16369
diff
changeset

180 
in axioms' end); 
1526  181 

182 

19708
a508bde37a81
added add_deps, which actually records dependencies of consts (unlike add_finals);
wenzelm
parents:
19700
diff
changeset

183 
(* dependencies *) 
a508bde37a81
added add_deps, which actually records dependencies of consts (unlike add_finals);
wenzelm
parents:
19700
diff
changeset

184 

33701
9dd1079cec3a
primitive defs: clarified def (axiom name) vs. description;
wenzelm
parents:
33173
diff
changeset

185 
fun dependencies thy unchecked def description lhs rhs = 
19708
a508bde37a81
added add_deps, which actually records dependencies of consts (unlike add_finals);
wenzelm
parents:
19700
diff
changeset

186 
let 
39133
70d3915c92f0
pretty printing: prefer regular Proof.context over Pretty.pp, which is mostly for special bootstrap purposes involving theory merge, for example;
wenzelm
parents:
36610
diff
changeset

187 
val ctxt = Syntax.init_pretty_global thy; 
19708
a508bde37a81
added add_deps, which actually records dependencies of consts (unlike add_finals);
wenzelm
parents:
19700
diff
changeset

188 
val consts = Sign.consts_of thy; 
19727  189 
fun prep const = 
39133
70d3915c92f0
pretty printing: prefer regular Proof.context over Pretty.pp, which is mostly for special bootstrap purposes involving theory merge, for example;
wenzelm
parents:
36610
diff
changeset

190 
let val Const (c, T) = Sign.no_vars ctxt (Const const) 
35845
e5980f0ad025
renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
wenzelm
parents:
34259
diff
changeset

191 
in (c, Consts.typargs consts (c, Logic.varifyT_global T)) end; 
19708
a508bde37a81
added add_deps, which actually records dependencies of consts (unlike add_finals);
wenzelm
parents:
19700
diff
changeset

192 

a508bde37a81
added add_deps, which actually records dependencies of consts (unlike add_finals);
wenzelm
parents:
19700
diff
changeset

193 
val lhs_vars = Term.add_tfreesT (#2 lhs) []; 
a508bde37a81
added add_deps, which actually records dependencies of consts (unlike add_finals);
wenzelm
parents:
19700
diff
changeset

194 
val rhs_extras = fold (#2 #> Term.fold_atyps (fn TFree v => 
a508bde37a81
added add_deps, which actually records dependencies of consts (unlike add_finals);
wenzelm
parents:
19700
diff
changeset

195 
if member (op =) lhs_vars v then I else insert (op =) v  _ => I)) rhs []; 
a508bde37a81
added add_deps, which actually records dependencies of consts (unlike add_finals);
wenzelm
parents:
19700
diff
changeset

196 
val _ = 
a508bde37a81
added add_deps, which actually records dependencies of consts (unlike add_finals);
wenzelm
parents:
19700
diff
changeset

197 
if null rhs_extras then () 
a508bde37a81
added add_deps, which actually records dependencies of consts (unlike add_finals);
wenzelm
parents:
19700
diff
changeset

198 
else error ("Specification depends on extra type variables: " ^ 
39133
70d3915c92f0
pretty printing: prefer regular Proof.context over Pretty.pp, which is mostly for special bootstrap purposes involving theory merge, for example;
wenzelm
parents:
36610
diff
changeset

199 
commas_quote (map (Syntax.string_of_typ ctxt o TFree) rhs_extras) ^ 
33701
9dd1079cec3a
primitive defs: clarified def (axiom name) vs. description;
wenzelm
parents:
33173
diff
changeset

200 
"\nThe error(s) above occurred in " ^ quote description); 
39133
70d3915c92f0
pretty printing: prefer regular Proof.context over Pretty.pp, which is mostly for special bootstrap purposes involving theory merge, for example;
wenzelm
parents:
36610
diff
changeset

201 
in Defs.define (Syntax.pp ctxt) unchecked def description (prep lhs) (map prep rhs) end; 
19708
a508bde37a81
added add_deps, which actually records dependencies of consts (unlike add_finals);
wenzelm
parents:
19700
diff
changeset

202 

a508bde37a81
added add_deps, which actually records dependencies of consts (unlike add_finals);
wenzelm
parents:
19700
diff
changeset

203 
fun add_deps a raw_lhs raw_rhs thy = 
a508bde37a81
added add_deps, which actually records dependencies of consts (unlike add_finals);
wenzelm
parents:
19700
diff
changeset

204 
let 
a508bde37a81
added add_deps, which actually records dependencies of consts (unlike add_finals);
wenzelm
parents:
19700
diff
changeset

205 
val lhs :: rhs = map (dest_Const o Sign.cert_term thy o Const) (raw_lhs :: raw_rhs); 
33701
9dd1079cec3a
primitive defs: clarified def (axiom name) vs. description;
wenzelm
parents:
33173
diff
changeset

206 
val description = if a = "" then #1 lhs ^ " axiom" else a; 
9dd1079cec3a
primitive defs: clarified def (axiom name) vs. description;
wenzelm
parents:
33173
diff
changeset

207 
in thy > map_defs (dependencies thy false NONE description lhs rhs) end; 
17706  208 

33173
b8ca12f6681a
eliminated obsolete tags for types/consts  now handled via name space, in strongly typed fashion;
wenzelm
parents:
33168
diff
changeset

209 
fun specify_const decl thy = 
b8ca12f6681a
eliminated obsolete tags for types/consts  now handled via name space, in strongly typed fashion;
wenzelm
parents:
33168
diff
changeset

210 
let val (t as Const const, thy') = Sign.declare_const decl thy 
28112
691993ef6abe
simplified specify_const: canonical args, global deps;
wenzelm
parents:
28017
diff
changeset

211 
in (t, add_deps "" const [] thy') end; 
25017  212 

17706  213 

35985
0bbf0d2348f9
moved Drule.forall_intr_frees to Thm.forall_intr_frees (in more_thm.ML, which is loaded before pure_thy.ML);
wenzelm
parents:
35857
diff
changeset

214 
(* overloading *) 
9280  215 

16944  216 
fun check_overloading thy overloaded (c, T) = 
16291  217 
let 
24763  218 
val declT = Sign.the_const_constraint thy c 
219 
handle TYPE (msg, _, _) => error msg; 

35845
e5980f0ad025
renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
wenzelm
parents:
34259
diff
changeset

220 
val T' = Logic.varifyT_global T; 
16944  221 

39134
917b4b6ba3d2
turned show_sorts/show_types into proper configuration options;
wenzelm
parents:
39133
diff
changeset

222 
val ctxt = Syntax.init_pretty_global thy; 
917b4b6ba3d2
turned show_sorts/show_types into proper configuration options;
wenzelm
parents:
39133
diff
changeset

223 
fun message sorts txt = 
16944  224 
[Pretty.block [Pretty.str "Specification of constant ", 
39134
917b4b6ba3d2
turned show_sorts/show_types into proper configuration options;
wenzelm
parents:
39133
diff
changeset

225 
Pretty.str c, Pretty.str " ::", Pretty.brk 1, 
917b4b6ba3d2
turned show_sorts/show_types into proper configuration options;
wenzelm
parents:
39133
diff
changeset

226 
Pretty.quote (Syntax.pretty_typ (Config.put show_sorts sorts ctxt) T)], 
16944  227 
Pretty.str txt] > Pretty.chunks > Pretty.string_of; 
16291  228 
in 
16944  229 
if Sign.typ_instance thy (declT, T') then () 
230 
else if Type.raw_instance (declT, T') then 

39134
917b4b6ba3d2
turned show_sorts/show_types into proper configuration options;
wenzelm
parents:
39133
diff
changeset

231 
error (message true "imposes additional sort constraints on the constant declaration") 
16944  232 
else if overloaded then () 
39134
917b4b6ba3d2
turned show_sorts/show_types into proper configuration options;
wenzelm
parents:
39133
diff
changeset

233 
else warning (message false "is strictly less general than the declared type") 
9280  234 
end; 
235 

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

236 

35985
0bbf0d2348f9
moved Drule.forall_intr_frees to Thm.forall_intr_frees (in more_thm.ML, which is loaded before pure_thy.ML);
wenzelm
parents:
35857
diff
changeset

237 
(* definitional axioms *) 
0bbf0d2348f9
moved Drule.forall_intr_frees to Thm.forall_intr_frees (in more_thm.ML, which is loaded before pure_thy.ML);
wenzelm
parents:
35857
diff
changeset

238 

0bbf0d2348f9
moved Drule.forall_intr_frees to Thm.forall_intr_frees (in more_thm.ML, which is loaded before pure_thy.ML);
wenzelm
parents:
35857
diff
changeset

239 
local 
16291  240 

29581  241 
fun check_def thy unchecked overloaded (b, tm) defs = 
16291  242 
let 
36610
bafd82950e24
renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
wenzelm
parents:
35988
diff
changeset

243 
val ctxt = ProofContext.init_global thy; 
29581  244 
val name = Sign.full_name thy b; 
35988
76ca601c941e
disallow premises in primitive Theory.add_def  handle in Thm.add_def;
wenzelm
parents:
35987
diff
changeset

245 
val ((lhs, rhs), _) = Primitive_Defs.dest_def ctxt Term.is_Const (K false) (K false) tm 
76ca601c941e
disallow premises in primitive Theory.add_def  handle in Thm.add_def;
wenzelm
parents:
35987
diff
changeset

246 
handle TERM (msg, _) => error msg; 
76ca601c941e
disallow premises in primitive Theory.add_def  handle in Thm.add_def;
wenzelm
parents:
35987
diff
changeset

247 
val lhs_const = Term.dest_Const (Term.head_of lhs); 
16944  248 
val rhs_consts = fold_aterms (fn Const const => insert (op =) const  _ => I) rhs []; 
18943  249 
val _ = check_overloading thy overloaded lhs_const; 
33701
9dd1079cec3a
primitive defs: clarified def (axiom name) vs. description;
wenzelm
parents:
33173
diff
changeset

250 
in defs > dependencies thy unchecked (SOME name) name lhs_const rhs_consts end 
18678  251 
handle ERROR msg => cat_error msg (Pretty.string_of (Pretty.block 
30218  252 
[Pretty.str ("The error(s) above occurred in definition " ^ quote (Binding.str_of b) ^ ":"), 
26939
1035c89b4c02
moved global pretty/string_of functions from Sign to Syntax;
wenzelm
parents:
26668
diff
changeset

253 
Pretty.fbrk, Pretty.quote (Syntax.pretty_term_global thy tm)])); 
3767
e2bb53d8dd26
moved theory stuff (add_defs etc.) here from drule.ML;
wenzelm
parents:
2979
diff
changeset

254 

16291  255 
in 
256 

35985
0bbf0d2348f9
moved Drule.forall_intr_frees to Thm.forall_intr_frees (in more_thm.ML, which is loaded before pure_thy.ML);
wenzelm
parents:
35857
diff
changeset

257 
fun add_def unchecked overloaded raw_axm thy = 
0bbf0d2348f9
moved Drule.forall_intr_frees to Thm.forall_intr_frees (in more_thm.ML, which is loaded before pure_thy.ML);
wenzelm
parents:
35857
diff
changeset

258 
let val axm = cert_axm thy raw_axm in 
0bbf0d2348f9
moved Drule.forall_intr_frees to Thm.forall_intr_frees (in more_thm.ML, which is loaded before pure_thy.ML);
wenzelm
parents:
35857
diff
changeset

259 
thy 
0bbf0d2348f9
moved Drule.forall_intr_frees to Thm.forall_intr_frees (in more_thm.ML, which is loaded before pure_thy.ML);
wenzelm
parents:
35857
diff
changeset

260 
> map_defs (check_def thy unchecked overloaded axm) 
0bbf0d2348f9
moved Drule.forall_intr_frees to Thm.forall_intr_frees (in more_thm.ML, which is loaded before pure_thy.ML);
wenzelm
parents:
35857
diff
changeset

261 
> add_axiom axm 
0bbf0d2348f9
moved Drule.forall_intr_frees to Thm.forall_intr_frees (in more_thm.ML, which is loaded before pure_thy.ML);
wenzelm
parents:
35857
diff
changeset

262 
end; 
16291  263 

264 
end; 

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

265 

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

266 

16443
82a116532e3e
type theory, theory_ref, exception THEORY and related operations imported from Context;
wenzelm
parents:
16369
diff
changeset

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

268 

16291  269 
local 
270 

17706  271 
fun gen_add_finals prep_term overloaded args thy = 
14223
0ee05eef881b
Added support for making constants final, that is, ensuring that no
skalberg
parents:
14204
diff
changeset

272 
let 
17706  273 
fun const_of (Const const) = const 
274 
 const_of (Free _) = error "Attempt to finalize variable (or undeclared constant)" 

275 
 const_of _ = error "Attempt to finalize nonconstant term"; 

33701
9dd1079cec3a
primitive defs: clarified def (axiom name) vs. description;
wenzelm
parents:
33173
diff
changeset

276 
fun specify (c, T) = dependencies thy false NONE (c ^ " axiom") (c, T) []; 
39134
917b4b6ba3d2
turned show_sorts/show_types into proper configuration options;
wenzelm
parents:
39133
diff
changeset

277 
val finalize = specify o tap (check_overloading thy overloaded) o const_of o 
24708  278 
Sign.cert_term thy o prep_term thy; 
17706  279 
in thy > map_defs (fold finalize args) end; 
16291  280 

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

281 
in 
16291  282 

29581  283 
val add_finals_i = gen_add_finals (K I); 
24708  284 
val add_finals = gen_add_finals Syntax.read_term_global; 
16291  285 

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

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

287 

1526  288 
end; 