equal
deleted
inserted
replaced
28 val at_end: (theory -> theory option) -> theory -> theory |
28 val at_end: (theory -> theory option) -> theory -> theory |
29 val begin_theory: string -> theory list -> theory |
29 val begin_theory: string -> theory list -> theory |
30 val end_theory: theory -> theory |
30 val end_theory: theory -> theory |
31 val add_axiom: binding * term -> theory -> theory |
31 val add_axiom: binding * term -> theory -> theory |
32 val add_deps: string -> string * typ -> (string * typ) list -> theory -> theory |
32 val add_deps: string -> string * typ -> (string * typ) list -> theory -> theory |
33 val add_defs_i: bool -> bool -> (binding * term) list -> theory -> theory |
33 val add_def: bool -> bool -> binding * term -> theory -> theory |
34 val add_defs: bool -> bool -> (binding * string) list -> theory -> theory |
|
35 val add_finals_i: bool -> term list -> theory -> theory |
34 val add_finals_i: bool -> term list -> theory -> theory |
36 val add_finals: bool -> string list -> theory -> theory |
35 val add_finals: bool -> string list -> theory -> theory |
37 val specify_const: (binding * typ) * mixfix -> theory -> term * theory |
36 val specify_const: (binding * typ) * mixfix -> theory -> term * theory |
38 end |
37 end |
39 |
38 |
149 fun end_theory thy = |
148 fun end_theory thy = |
150 thy |> apply_wrappers (end_wrappers thy) |> Context.finish_thy; |
149 thy |> apply_wrappers (end_wrappers thy) |> Context.finish_thy; |
151 |
150 |
152 |
151 |
153 |
152 |
154 (** add axioms **) |
153 (** primitive specifications **) |
155 |
154 |
156 (* prepare axioms *) |
155 (* raw axioms *) |
157 |
156 |
158 fun cert_axm thy (b, raw_tm) = |
157 fun cert_axm thy (b, raw_tm) = |
159 let |
158 let |
160 val t = Sign.cert_prop thy raw_tm |
159 val t = Sign.cert_prop thy raw_tm |
161 handle TYPE (msg, _, _) => error msg |
160 handle TYPE (msg, _, _) => error msg |
163 in |
162 in |
164 Term.no_dummy_patterns t handle TERM (msg, _) => error msg; |
163 Term.no_dummy_patterns t handle TERM (msg, _) => error msg; |
165 (b, Sign.no_vars (Syntax.pp_global thy) t) |
164 (b, Sign.no_vars (Syntax.pp_global thy) t) |
166 end; |
165 end; |
167 |
166 |
168 fun read_axm thy (b, str) = |
|
169 cert_axm thy (b, Syntax.read_prop_global thy str) handle ERROR msg => |
|
170 cat_error msg ("The error(s) above occurred in axiom " ^ quote (Binding.str_of b)); |
|
171 |
|
172 |
|
173 (* add_axiom *) |
|
174 |
|
175 fun add_axiom raw_axm thy = thy |> map_axioms (fn axioms => |
167 fun add_axiom raw_axm thy = thy |> map_axioms (fn axioms => |
176 let |
168 let |
177 val axm = apsnd Logic.varify_global (cert_axm thy raw_axm); |
169 val axm = apsnd Logic.varify_global (cert_axm thy raw_axm); |
178 val (_, axioms') = Name_Space.define true (Sign.naming_of thy) axm axioms; |
170 val (_, axioms') = Name_Space.define true (Sign.naming_of thy) axm axioms; |
179 in axioms' end); |
171 in axioms' end); |
180 |
172 |
181 |
|
182 |
|
183 (** add constant definitions **) |
|
184 |
173 |
185 (* dependencies *) |
174 (* dependencies *) |
186 |
175 |
187 fun dependencies thy unchecked def description lhs rhs = |
176 fun dependencies thy unchecked def description lhs rhs = |
188 let |
177 let |
211 fun specify_const decl thy = |
200 fun specify_const decl thy = |
212 let val (t as Const const, thy') = Sign.declare_const decl thy |
201 let val (t as Const const, thy') = Sign.declare_const decl thy |
213 in (t, add_deps "" const [] thy') end; |
202 in (t, add_deps "" const [] thy') end; |
214 |
203 |
215 |
204 |
216 (* check_overloading *) |
205 (* overloading *) |
217 |
206 |
218 fun check_overloading thy overloaded (c, T) = |
207 fun check_overloading thy overloaded (c, T) = |
219 let |
208 let |
220 val declT = Sign.the_const_constraint thy c |
209 val declT = Sign.the_const_constraint thy c |
221 handle TYPE (msg, _, _) => error msg; |
210 handle TYPE (msg, _, _) => error msg; |
234 else warning (message "is strictly less general than the declared type"); |
223 else warning (message "is strictly less general than the declared type"); |
235 (c, T) |
224 (c, T) |
236 end; |
225 end; |
237 |
226 |
238 |
227 |
239 (* check_def *) |
228 (* definitional axioms *) |
|
229 |
|
230 local |
240 |
231 |
241 fun check_def thy unchecked overloaded (b, tm) defs = |
232 fun check_def thy unchecked overloaded (b, tm) defs = |
242 let |
233 let |
243 val ctxt = ProofContext.init thy; |
234 val ctxt = ProofContext.init thy; |
244 val name = Sign.full_name thy b; |
235 val name = Sign.full_name thy b; |
248 in defs |> dependencies thy unchecked (SOME name) name lhs_const rhs_consts end |
239 in defs |> dependencies thy unchecked (SOME name) name lhs_const rhs_consts end |
249 handle ERROR msg => cat_error msg (Pretty.string_of (Pretty.block |
240 handle ERROR msg => cat_error msg (Pretty.string_of (Pretty.block |
250 [Pretty.str ("The error(s) above occurred in definition " ^ quote (Binding.str_of b) ^ ":"), |
241 [Pretty.str ("The error(s) above occurred in definition " ^ quote (Binding.str_of b) ^ ":"), |
251 Pretty.fbrk, Pretty.quote (Syntax.pretty_term_global thy tm)])); |
242 Pretty.fbrk, Pretty.quote (Syntax.pretty_term_global thy tm)])); |
252 |
243 |
253 |
244 in |
254 (* add_defs(_i) *) |
245 |
255 |
246 fun add_def unchecked overloaded raw_axm thy = |
256 local |
247 let val axm = cert_axm thy raw_axm in |
257 |
|
258 fun gen_add_defs prep_axm unchecked overloaded raw_axms thy = |
|
259 let val axms = map (prep_axm thy) raw_axms in |
|
260 thy |
248 thy |
261 |> map_defs (fold (check_def thy unchecked overloaded) axms) |
249 |> map_defs (check_def thy unchecked overloaded axm) |
262 |> fold add_axiom axms |
250 |> add_axiom axm |
263 end; |
251 end; |
264 |
|
265 in |
|
266 |
|
267 val add_defs_i = gen_add_defs cert_axm; |
|
268 val add_defs = gen_add_defs read_axm; |
|
269 |
252 |
270 end; |
253 end; |
271 |
254 |
272 |
255 |
273 (* add_finals(_i) *) |
256 (* add_finals(_i) *) |