equal
deleted
inserted
replaced
47 val merge_refs: theory_ref * theory_ref -> theory_ref (*exception TERM*) |
47 val merge_refs: theory_ref * theory_ref -> theory_ref (*exception TERM*) |
48 val requires: theory -> string -> string -> unit |
48 val requires: theory -> string -> string -> unit |
49 val assert_super: theory -> theory -> theory |
49 val assert_super: theory -> theory -> theory |
50 val add_axioms: (bstring * string) list -> theory -> theory |
50 val add_axioms: (bstring * string) list -> theory -> theory |
51 val add_axioms_i: (bstring * term) list -> theory -> theory |
51 val add_axioms_i: (bstring * term) list -> theory -> theory |
52 val add_defs: bool -> (bstring * string) list -> theory -> theory |
52 val add_defs: bool -> bool -> (bstring * string) list -> theory -> theory |
53 val add_defs_i: bool -> (bstring * term) list -> theory -> theory |
53 val add_defs_i: bool -> bool -> (bstring * term) list -> theory -> theory |
54 val add_finals: bool -> string list -> theory -> theory |
54 val add_finals: bool -> string list -> theory -> theory |
55 val add_finals_i: bool -> term list -> theory -> theory |
55 val add_finals_i: bool -> term list -> theory -> theory |
56 val add_oracle: bstring * (theory * Object.T -> term) -> theory -> theory |
56 val add_oracle: bstring * (theory * Object.T -> term) -> theory -> theory |
57 end |
57 end |
58 |
58 |
252 end; |
252 end; |
253 |
253 |
254 |
254 |
255 (* check_def *) |
255 (* check_def *) |
256 |
256 |
257 fun check_def thy overloaded (bname, tm) defs = |
257 fun check_def thy unchecked overloaded (bname, tm) defs = |
258 let |
258 let |
259 val pp = Sign.pp thy; |
259 val pp = Sign.pp thy; |
260 fun prt_const (c, T) = |
260 fun prt_const (c, T) = |
261 [Pretty.str c, Pretty.str " ::", Pretty.brk 1, |
261 [Pretty.str c, Pretty.str " ::", Pretty.brk 1, |
262 Pretty.quote (Pretty.typ pp (Type.freeze_type T))]; |
262 Pretty.quote (Pretty.typ pp (Type.freeze_type T))]; |
264 val name = Sign.full_name thy bname; |
264 val name = Sign.full_name thy bname; |
265 val (lhs_const, rhs) = Sign.cert_def pp tm; |
265 val (lhs_const, rhs) = Sign.cert_def pp tm; |
266 val rhs_consts = fold_aterms (fn Const const => insert (op =) const | _ => I) rhs []; |
266 val rhs_consts = fold_aterms (fn Const const => insert (op =) const | _ => I) rhs []; |
267 val _ = check_overloading thy overloaded lhs_const; |
267 val _ = check_overloading thy overloaded lhs_const; |
268 in |
268 in |
269 defs |> Defs.define (Sign.const_typargs thy) true (Context.theory_name thy) |
269 defs |> Defs.define (Sign.const_typargs thy) unchecked true (Context.theory_name thy) |
270 name (prep_const thy lhs_const) (map (prep_const thy) rhs_consts) |
270 name (prep_const thy lhs_const) (map (prep_const thy) rhs_consts) |
271 end |
271 end |
272 handle ERROR msg => cat_error msg (Pretty.string_of (Pretty.block |
272 handle ERROR msg => cat_error msg (Pretty.string_of (Pretty.block |
273 [Pretty.str ("The error(s) above occurred in definition " ^ quote bname ^ ":"), |
273 [Pretty.str ("The error(s) above occurred in definition " ^ quote bname ^ ":"), |
274 Pretty.fbrk, Pretty.quote (Pretty.term (Sign.pp thy) tm)])); |
274 Pretty.fbrk, Pretty.quote (Pretty.term (Sign.pp thy) tm)])); |
276 |
276 |
277 (* add_defs(_i) *) |
277 (* add_defs(_i) *) |
278 |
278 |
279 local |
279 local |
280 |
280 |
281 fun gen_add_defs prep_axm overloaded raw_axms thy = |
281 fun gen_add_defs prep_axm unchecked overloaded raw_axms thy = |
282 let val axms = map (prep_axm thy) raw_axms in |
282 let val axms = map (prep_axm thy) raw_axms in |
283 thy |
283 thy |
284 |> map_defs (fold (check_def thy overloaded) axms) |
284 |> map_defs (fold (check_def thy unchecked overloaded) axms) |
285 |> add_axioms_i axms |
285 |> add_axioms_i axms |
286 end; |
286 end; |
287 |
287 |
288 in |
288 in |
289 |
289 |
300 fun gen_add_finals prep_term overloaded args thy = |
300 fun gen_add_finals prep_term overloaded args thy = |
301 let |
301 let |
302 fun const_of (Const const) = const |
302 fun const_of (Const const) = const |
303 | const_of (Free _) = error "Attempt to finalize variable (or undeclared constant)" |
303 | const_of (Free _) = error "Attempt to finalize variable (or undeclared constant)" |
304 | const_of _ = error "Attempt to finalize non-constant term"; |
304 | const_of _ = error "Attempt to finalize non-constant term"; |
305 fun specify (c, T) = Defs.define (Sign.const_typargs thy) false (Context.theory_name thy) |
305 fun specify (c, T) = Defs.define (Sign.const_typargs thy) false false (Context.theory_name thy) |
306 (c ^ " axiom") (prep_const thy (c, T)) []; |
306 (c ^ " axiom") (prep_const thy (c, T)) []; |
307 val finalize = specify o check_overloading thy overloaded o |
307 val finalize = specify o check_overloading thy overloaded o |
308 const_of o Sign.no_vars (Sign.pp thy) o prep_term thy; |
308 const_of o Sign.no_vars (Sign.pp thy) o prep_term thy; |
309 in thy |> map_defs (fold finalize args) end; |
309 in thy |> map_defs (fold finalize args) end; |
310 |
310 |