author  haftmann 
Thu, 24 May 2007 08:37:37 +0200  
changeset 23086  12320f6e2523 
parent 22846  fb79144af9a3 
child 23600  5a5332e1351b 
permissions  rwrr 
1526  1 
(* Title: Pure/theory.ML 
2 
ID: $Id$ 

3 
Author: Lawrence C Paulson and Markus Wenzel 

4 

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

5 
Logical theory content: axioms, definitions, oracles. 
1526  6 
*) 
16291  7 

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

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

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

10 
val eq_thy: theory * theory > bool 
3996  11 
val subthy: theory * theory > bool 
3767
e2bb53d8dd26
moved theory stuff (add_defs etc.) here from drule.ML;
wenzelm
parents:
2979
diff
changeset

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

13 

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

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

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

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

17 
include SIGN_THEORY 
22684  18 
val parents_of: theory > theory list 
19 
val ancestors_of: theory > theory list 

16495  20 
val begin_theory: string > theory list > theory 
21 
val end_theory: theory > theory 

22 
val checkpoint: theory > theory 

23 
val copy: theory > theory 

22684  24 
val rep_theory: theory > 
25 
{axioms: term NameSpace.table, 

26 
defs: Defs.T, 

27 
oracles: ((theory * Object.T > term) * stamp) NameSpace.table} 

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

28 
val axiom_space: theory > NameSpace.T 
22684  29 
val axiom_table: theory > term Symtab.table 
16443
82a116532e3e
type theory, theory_ref, exception THEORY and related operations imported from Context;
wenzelm
parents:
16369
diff
changeset

30 
val oracle_space: theory > NameSpace.T 
22684  31 
val oracle_table: theory > ((theory * Object.T > term) * stamp) Symtab.table 
16339  32 
val axioms_of: theory > (string * term) list 
33 
val all_axioms_of: theory > (string * term) list 

17706  34 
val defs_of : theory > Defs.T 
16443
82a116532e3e
type theory, theory_ref, exception THEORY and related operations imported from Context;
wenzelm
parents:
16369
diff
changeset

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

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

37 
val merge: theory * theory > theory (*exception TERM*) 
82a116532e3e
type theory, theory_ref, exception THEORY and related operations imported from Context;
wenzelm
parents:
16369
diff
changeset

38 
val merge_refs: theory_ref * theory_ref > theory_ref (*exception TERM*) 
21608  39 
val merge_list: theory list > theory (*exception TERM*) 
16443
82a116532e3e
type theory, theory_ref, exception THEORY and related operations imported from Context;
wenzelm
parents:
16369
diff
changeset

40 
val requires: theory > string > string > unit 
82a116532e3e
type theory, theory_ref, exception THEORY and related operations imported from Context;
wenzelm
parents:
16369
diff
changeset

41 
val assert_super: theory > theory > theory 
22684  42 
val cert_axm: theory > string * term > string * term 
43 
val read_axm: theory > string * string > string * term 

3996  44 
val add_axioms: (bstring * string) list > theory > theory 
45 
val add_axioms_i: (bstring * term) list > theory > theory 

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

46 
val add_deps: string > string * typ > (string * typ) list > theory > theory 
19630  47 
val add_defs: bool > bool > (bstring * string) list > theory > theory 
48 
val add_defs_i: bool > bool > (bstring * term) list > theory > theory 

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

49 
val add_finals: bool > string list > theory > theory 
82a116532e3e
type theory, theory_ref, exception THEORY and related operations imported from Context;
wenzelm
parents:
16369
diff
changeset

50 
val add_finals_i: bool > term list > theory > theory 
82a116532e3e
type theory, theory_ref, exception THEORY and related operations imported from Context;
wenzelm
parents:
16369
diff
changeset

51 
val add_oracle: bstring * (theory * Object.T > term) > theory > theory 
16495  52 
end 
1526  53 

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

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

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

56 

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

57 

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

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

59 

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

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

61 

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

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

63 
val subthy = Context.subthy; 
1526  64 

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

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

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

67 

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

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

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

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

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

72 

21608  73 
fun merge_list [] = raise TERM ("Empty merge of theories", []) 
74 
 merge_list (thy :: thys) = Library.foldl merge (thy, thys); 

75 

16495  76 
val begin_theory = Sign.local_path oo Context.begin_thy Sign.pp; 
77 
val end_theory = Context.finish_thy; 

78 
val checkpoint = Context.checkpoint_thy; 

79 
val copy = Context.copy_thy; 

80 

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

81 

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

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

83 

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

84 
structure SignTheory: SIGN_THEORY = Sign; 
82a116532e3e
type theory, theory_ref, exception THEORY and related operations imported from Context;
wenzelm
parents:
16369
diff
changeset

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

86 

2206  87 

3996  88 

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

89 
(** datatype thy **) 
82a116532e3e
type theory, theory_ref, exception THEORY and related operations imported from Context;
wenzelm
parents:
16369
diff
changeset

90 

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

91 
datatype thy = Thy of 
82a116532e3e
type theory, theory_ref, exception THEORY and related operations imported from Context;
wenzelm
parents:
16369
diff
changeset

92 
{axioms: term NameSpace.table, 
17706  93 
defs: Defs.T, 
16443
82a116532e3e
type theory, theory_ref, exception THEORY and related operations imported from Context;
wenzelm
parents:
16369
diff
changeset

94 
oracles: ((theory * Object.T > term) * stamp) NameSpace.table}; 
82a116532e3e
type theory, theory_ref, exception THEORY and related operations imported from Context;
wenzelm
parents:
16369
diff
changeset

95 

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

96 
fun make_thy (axioms, defs, oracles) = 
82a116532e3e
type theory, theory_ref, exception THEORY and related operations imported from Context;
wenzelm
parents:
16369
diff
changeset

97 
Thy {axioms = axioms, defs = defs, oracles = oracles}; 
1526  98 

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

99 
fun err_dup_axms dups = error ("Duplicate axiom(s): " ^ commas_quote dups); 
82a116532e3e
type theory, theory_ref, exception THEORY and related operations imported from Context;
wenzelm
parents:
16369
diff
changeset

100 
fun err_dup_oras dups = error ("Duplicate oracle(s): " ^ commas_quote dups); 
3996  101 

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

102 
structure ThyData = TheoryDataFun 
22846  103 
( 
16443
82a116532e3e
type theory, theory_ref, exception THEORY and related operations imported from Context;
wenzelm
parents:
16369
diff
changeset

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

105 
val empty = make_thy (NameSpace.empty_table, Defs.empty, NameSpace.empty_table); 
82a116532e3e
type theory, theory_ref, exception THEORY and related operations imported from Context;
wenzelm
parents:
16369
diff
changeset

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

107 

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

108 
fun extend (Thy {axioms, defs, oracles}) = make_thy (NameSpace.empty_table, defs, oracles); 
82a116532e3e
type theory, theory_ref, exception THEORY and related operations imported from Context;
wenzelm
parents:
16369
diff
changeset

109 

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

110 
fun merge pp (thy1, thy2) = 
82a116532e3e
type theory, theory_ref, exception THEORY and related operations imported from Context;
wenzelm
parents:
16369
diff
changeset

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

112 
val Thy {axioms = _, defs = defs1, oracles = oracles1} = thy1; 
82a116532e3e
type theory, theory_ref, exception THEORY and related operations imported from Context;
wenzelm
parents:
16369
diff
changeset

113 
val Thy {axioms = _, defs = defs2, oracles = oracles2} = thy2; 
1526  114 

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

115 
val axioms = NameSpace.empty_table; 
19693  116 
val defs = Defs.merge pp (defs1, defs2); 
17496  117 
val oracles = NameSpace.merge_tables (eq_snd (op =)) (oracles1, oracles2) 
16443
82a116532e3e
type theory, theory_ref, exception THEORY and related operations imported from Context;
wenzelm
parents:
16369
diff
changeset

118 
handle Symtab.DUPS dups => err_dup_oras dups; 
82a116532e3e
type theory, theory_ref, exception THEORY and related operations imported from Context;
wenzelm
parents:
16369
diff
changeset

119 
in make_thy (axioms, defs, oracles) end; 
22846  120 
); 
16443
82a116532e3e
type theory, theory_ref, exception THEORY and related operations imported from Context;
wenzelm
parents:
16369
diff
changeset

121 

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

122 
fun rep_theory thy = ThyData.get thy > (fn Thy args => args); 
82a116532e3e
type theory, theory_ref, exception THEORY and related operations imported from Context;
wenzelm
parents:
16369
diff
changeset

123 

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

124 
fun map_thy f = ThyData.map (fn (Thy {axioms, defs, oracles}) => 
82a116532e3e
type theory, theory_ref, exception THEORY and related operations imported from Context;
wenzelm
parents:
16369
diff
changeset

125 
make_thy (f (axioms, defs, oracles))); 
82a116532e3e
type theory, theory_ref, exception THEORY and related operations imported from Context;
wenzelm
parents:
16369
diff
changeset

126 

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

127 
fun map_axioms f = map_thy (fn (axioms, defs, oracles) => (f axioms, defs, oracles)); 
82a116532e3e
type theory, theory_ref, exception THEORY and related operations imported from Context;
wenzelm
parents:
16369
diff
changeset

128 
fun map_defs f = map_thy (fn (axioms, defs, oracles) => (axioms, f defs, oracles)); 
82a116532e3e
type theory, theory_ref, exception THEORY and related operations imported from Context;
wenzelm
parents:
16369
diff
changeset

129 
fun map_oracles f = map_thy (fn (axioms, defs, oracles) => (axioms, defs, f oracles)); 
82a116532e3e
type theory, theory_ref, exception THEORY and related operations imported from Context;
wenzelm
parents:
16369
diff
changeset

130 

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

131 

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

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

133 

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

134 
val axiom_space = #1 o #axioms o rep_theory; 
22684  135 
val axiom_table = #2 o #axioms o rep_theory; 
136 

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

137 
val oracle_space = #1 o #oracles o rep_theory; 
22684  138 
val oracle_table = #2 o #oracles o rep_theory; 
3996  139 

16339  140 
val axioms_of = Symtab.dest o #2 o #axioms o rep_theory; 
19482
9f11af8f7ef9
tuned basic list operators (flat, maps, map_filter);
wenzelm
parents:
19428
diff
changeset

141 
fun all_axioms_of thy = maps axioms_of (thy :: ancestors_of thy); 
16339  142 

16803  143 
val defs_of = #defs o rep_theory; 
16743
21dbff595bf6
1) all theorems in Orderings can now be given as a parameter
obua
parents:
16600
diff
changeset

144 

4970  145 
fun requires thy name what = 
16443
82a116532e3e
type theory, theory_ref, exception THEORY and related operations imported from Context;
wenzelm
parents:
16369
diff
changeset

146 
if Context.exists_name name thy then () 
4846  147 
else error ("Require theory " ^ quote name ^ " as an ancestor for " ^ what); 
1526  148 

6369  149 
fun assert_super thy1 thy2 = 
150 
if subthy (thy1, thy2) then thy2 

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

152 

3996  153 

6311  154 

3814  155 
(** add axioms **) 
156 

1526  157 
(* prepare axioms *) 
158 

18678  159 
fun err_in_axm msg name = 
160 
cat_error msg ("The error(s) above occurred in axiom " ^ quote name); 

1526  161 

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

162 
fun cert_axm thy (name, raw_tm) = 
1526  163 
let 
18968
52639ad19a96
adapted Sign.infer_types(_simult), Sign.certify_term/prop;
wenzelm
parents:
18943
diff
changeset

164 
val (t, T, _) = Sign.certify_prop thy raw_tm 
2979  165 
handle TYPE (msg, _, _) => error msg 
16291  166 
 TERM (msg, _) => error msg; 
1526  167 
in 
9537  168 
Term.no_dummy_patterns t handle TERM (msg, _) => error msg; 
18968
52639ad19a96
adapted Sign.infer_types(_simult), Sign.certify_term/prop;
wenzelm
parents:
18943
diff
changeset

169 
(name, Sign.no_vars (Sign.pp thy) t) 
9629  170 
end; 
1526  171 

22684  172 
fun read_axm thy (name, str) = 
22689  173 
cert_axm thy (name, Sign.read_prop thy str) 
174 
handle ERROR msg => err_in_axm msg name; 

1526  175 

176 

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

177 
(* add_axioms(_i) *) 
1526  178 

16291  179 
local 
180 

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

181 
fun gen_add_axioms prep_axm raw_axms thy = thy > map_axioms (fn axioms => 
1526  182 
let 
16991  183 
val axms = map (apsnd (Compress.term thy o Logic.varify) o prep_axm thy) raw_axms; 
23086  184 
val axioms' = NameSpace.extend_table (Sign.naming_of thy) axms axioms 
16443
82a116532e3e
type theory, theory_ref, exception THEORY and related operations imported from Context;
wenzelm
parents:
16369
diff
changeset

185 
handle Symtab.DUPS dups => err_dup_axms dups; 
82a116532e3e
type theory, theory_ref, exception THEORY and related operations imported from Context;
wenzelm
parents:
16369
diff
changeset

186 
in axioms' end); 
1526  187 

16291  188 
in 
189 

190 
val add_axioms = gen_add_axioms read_axm; 

191 
val add_axioms_i = gen_add_axioms cert_axm; 

192 

193 
end; 

1526  194 

195 

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

196 

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

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

198 

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

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

200 

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

201 
fun dependencies thy unchecked is_def name lhs rhs = 
a508bde37a81
added add_deps, which actually records dependencies of consts (unlike add_finals);
wenzelm
parents:
19700
diff
changeset

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

203 
val pp = Sign.pp thy; 
a508bde37a81
added add_deps, which actually records dependencies of consts (unlike add_finals);
wenzelm
parents:
19700
diff
changeset

204 
val consts = Sign.consts_of thy; 
19727  205 
fun prep const = 
206 
let val Const (c, T) = Sign.no_vars pp (Const const) 

19806  207 
in (c, Consts.typargs consts (c, Compress.typ thy (Logic.varifyT T))) end; 
19708
a508bde37a81
added add_deps, which actually records dependencies of consts (unlike add_finals);
wenzelm
parents:
19700
diff
changeset

208 

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

209 
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

210 
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

211 
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

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

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

214 
else error ("Specification depends on extra type variables: " ^ 
a508bde37a81
added add_deps, which actually records dependencies of consts (unlike add_finals);
wenzelm
parents:
19700
diff
changeset

215 
commas_quote (map (Pretty.string_of_typ pp o TFree) rhs_extras) ^ 
a508bde37a81
added add_deps, which actually records dependencies of consts (unlike add_finals);
wenzelm
parents:
19700
diff
changeset

216 
"\nThe error(s) above occurred in " ^ quote name); 
19727  217 
in Defs.define pp unchecked is_def (Context.theory_name thy) name (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

218 

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

219 
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

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

221 
val lhs :: rhs = map (dest_Const o Sign.cert_term thy o Const) (raw_lhs :: raw_rhs); 
a508bde37a81
added add_deps, which actually records dependencies of consts (unlike add_finals);
wenzelm
parents:
19700
diff
changeset

222 
val name = if a = "" then (#1 lhs ^ " axiom") else a; 
a508bde37a81
added add_deps, which actually records dependencies of consts (unlike add_finals);
wenzelm
parents:
19700
diff
changeset

223 
in thy > map_defs (dependencies thy false false name lhs rhs) end; 
17706  224 

225 

16944  226 
(* check_overloading *) 
9280  227 

16944  228 
fun check_overloading thy overloaded (c, T) = 
16291  229 
let 
16944  230 
val declT = 
231 
(case Sign.const_constraint thy c of 

232 
NONE => error ("Undeclared constant " ^ quote c) 

233 
 SOME declT => declT); 

19806  234 
val T' = Logic.varifyT T; 
16944  235 

236 
fun message txt = 

237 
[Pretty.block [Pretty.str "Specification of constant ", 

238 
Pretty.str c, Pretty.str " ::", Pretty.brk 1, Pretty.quote (Sign.pretty_typ thy T)], 

239 
Pretty.str txt] > Pretty.chunks > Pretty.string_of; 

16291  240 
in 
16944  241 
if Sign.typ_instance thy (declT, T') then () 
242 
else if Type.raw_instance (declT, T') then 

243 
error (Library.setmp show_sorts true 

244 
message "imposes additional sort constraints on the constant declaration") 

245 
else if overloaded then () 

246 
else warning (message "is strictly less general than the declared type"); 

247 
(c, T) 

9280  248 
end; 
249 

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

250 

16291  251 
(* check_def *) 
252 

19630  253 
fun check_def thy unchecked overloaded (bname, tm) defs = 
16291  254 
let 
17706  255 
val name = Sign.full_name thy bname; 
19693  256 
val (lhs_const, rhs) = Sign.cert_def (Sign.pp thy) tm; 
16944  257 
val rhs_consts = fold_aterms (fn Const const => insert (op =) const  _ => I) rhs []; 
18943  258 
val _ = check_overloading thy overloaded lhs_const; 
19708
a508bde37a81
added add_deps, which actually records dependencies of consts (unlike add_finals);
wenzelm
parents:
19700
diff
changeset

259 
in defs > dependencies thy unchecked true name lhs_const rhs_consts end 
18678  260 
handle ERROR msg => cat_error msg (Pretty.string_of (Pretty.block 
16883  261 
[Pretty.str ("The error(s) above occurred in definition " ^ quote bname ^ ":"), 
19693  262 
Pretty.fbrk, Pretty.quote (Sign.pretty_term thy tm)])); 
3767
e2bb53d8dd26
moved theory stuff (add_defs etc.) here from drule.ML;
wenzelm
parents:
2979
diff
changeset

263 

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

264 

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

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

266 

16291  267 
local 
9320  268 

19630  269 
fun gen_add_defs prep_axm unchecked overloaded raw_axms thy = 
16443
82a116532e3e
type theory, theory_ref, exception THEORY and related operations imported from Context;
wenzelm
parents:
16369
diff
changeset

270 
let val axms = map (prep_axm thy) raw_axms in 
82a116532e3e
type theory, theory_ref, exception THEORY and related operations imported from Context;
wenzelm
parents:
16369
diff
changeset

271 
thy 
19630  272 
> map_defs (fold (check_def thy unchecked overloaded) axms) 
9320  273 
> add_axioms_i axms 
3767
e2bb53d8dd26
moved theory stuff (add_defs etc.) here from drule.ML;
wenzelm
parents:
2979
diff
changeset

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

275 

16291  276 
in 
277 

278 
val add_defs_i = gen_add_defs cert_axm; 

279 
val add_defs = gen_add_defs read_axm; 

280 

281 
end; 

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

282 

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

283 

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

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

285 

16291  286 
local 
287 

17706  288 
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

289 
let 
17706  290 
fun const_of (Const const) = const 
291 
 const_of (Free _) = error "Attempt to finalize variable (or undeclared constant)" 

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

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

293 
fun specify (c, T) = dependencies thy false false (c ^ " axiom") (c, T) []; 
a508bde37a81
added add_deps, which actually records dependencies of consts (unlike add_finals);
wenzelm
parents:
19700
diff
changeset

294 
val finalize = specify o check_overloading thy overloaded o const_of o prep_term thy; 
17706  295 
in thy > map_defs (fold finalize args) end; 
16291  296 

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

297 
in 
16291  298 

17706  299 
val add_finals = gen_add_finals Sign.read_term; 
300 
val add_finals_i = gen_add_finals Sign.cert_term; 

16291  301 

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

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

303 

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

304 

3878  305 

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

306 
(** add oracle **) 
3814  307 

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

308 
fun add_oracle (bname, oracle) thy = thy > map_oracles (fn oracles => 
23086  309 
NameSpace.extend_table (Sign.naming_of thy) [(bname, (oracle, stamp ()))] oracles 
16443
82a116532e3e
type theory, theory_ref, exception THEORY and related operations imported from Context;
wenzelm
parents:
16369
diff
changeset

310 
handle Symtab.DUPS dups => err_dup_oras dups); 
3885  311 

1526  312 
end; 
313 

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

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

315 
open BasicTheory; 