221 |
221 |
222 |
222 |
223 |
223 |
224 (** add constant definitions **) |
224 (** add constant definitions **) |
225 |
225 |
226 (* overloading *) |
226 (* check_overloading *) |
227 |
227 |
228 datatype overloading = Clean | Implicit | Useless; |
228 fun check_overloading thy overloaded (c, T) = |
229 |
229 let |
230 fun overloading thy overloaded declT defT = |
230 val declT = |
231 let |
231 (case Sign.const_constraint thy c of |
232 val defT' = Logic.incr_tvar (maxidx_of_typ declT + 1) (Type.varifyT defT); |
232 NONE => error ("Undeclared constant " ^ quote c) |
|
233 | SOME declT => declT); |
|
234 val T' = Type.varifyT T; |
|
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; |
233 in |
240 in |
234 if Sign.typ_instance thy (declT, defT') then Clean |
241 if Sign.typ_instance thy (declT, T') then () |
235 else if Sign.typ_instance thy (Type.strip_sorts declT, Type.strip_sorts defT') then Useless |
242 else if Type.raw_instance (declT, T') then |
236 else if overloaded then Clean |
243 error (Library.setmp show_sorts true |
237 else Implicit |
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) |
238 end; |
248 end; |
239 |
249 |
240 |
250 |
241 (* dest_def *) |
251 (* dest_def *) |
242 |
252 |
277 end; |
287 end; |
278 |
288 |
279 |
289 |
280 (* check_def *) |
290 (* check_def *) |
281 |
291 |
282 fun pretty_const pp (c, T) = |
|
283 [Pretty.str c, Pretty.str " ::", Pretty.brk 1, |
|
284 Pretty.quote (Pretty.typ pp (Type.freeze_type T))]; |
|
285 |
|
286 fun check_def thy overloaded (bname, tm) defs = |
292 fun check_def thy overloaded (bname, tm) defs = |
287 let |
293 let |
288 val pp = Sign.pp thy; |
294 val pp = Sign.pp thy; |
289 fun prt_const (c, T) = |
295 fun prt_const (c, T) = |
290 [Pretty.str c, Pretty.str " ::", Pretty.brk 1, |
296 [Pretty.str c, Pretty.str " ::", Pretty.brk 1, |
291 Pretty.quote (Pretty.typ pp (Type.freeze_type T))]; |
297 Pretty.quote (Pretty.typ pp (Type.freeze_type T))]; |
292 fun string_of_def const txt = |
298 fun declared (c, _) = (c, Sign.the_const_type thy c); |
293 [Pretty.block (Pretty.str "Definition of " :: pretty_const pp const), Pretty.str txt] |
299 |
294 |> Pretty.chunks |> Pretty.string_of; |
300 val _ = no_vars pp tm; |
295 |
301 val (const, rhs) = dest_def pp tm handle TERM (msg, _) => error msg; |
296 fun typed_const c = (c, Sign.the_const_type thy c); |
302 val rhs_consts = fold_aterms (fn Const const => insert (op =) const | _ => I) rhs []; |
297 |
303 val _ = check_overloading thy overloaded const; |
298 val ((c, defT), rhs) = dest_def pp tm handle TERM (msg, _) => error msg; |
|
299 val rhs_consts = Term.term_constsT rhs; |
|
300 val declT = Sign.the_const_type thy c; |
|
301 val _ = |
|
302 (case overloading thy overloaded declT defT of |
|
303 Clean => () |
|
304 | Implicit => warning (string_of_def (c, defT) |
|
305 ("is strictly less general than the declared type (see " ^ quote bname ^ ")")) |
|
306 | Useless => error (Library.setmp show_sorts true (string_of_def (c, defT)) |
|
307 "imposes additional sort constraints on the declared type of the constant")); |
|
308 in |
304 in |
309 defs |> Defs.declare (typed_const c) |> fold (Defs.declare o typed_const o #1) rhs_consts |
305 defs |
310 |> Defs.define pp (c, defT) (Sign.full_name thy bname) rhs_consts |
306 |> Defs.declare (declared const) |
|
307 |> fold (Defs.declare o declared) rhs_consts |
|
308 |> Defs.define pp const (Sign.full_name thy bname) rhs_consts |
311 end |
309 end |
312 handle ERROR => error (Pretty.string_of (Pretty.block |
310 handle ERROR => error (Pretty.string_of (Pretty.block |
313 [Pretty.str ("The error(s) above occurred in definition " ^ quote bname ^ ":"), |
311 [Pretty.str ("The error(s) above occurred in definition " ^ quote bname ^ ":"), |
314 Pretty.fbrk, Pretty.quote (Pretty.term (Sign.pp thy) tm)])); |
312 Pretty.fbrk, Pretty.quote (Pretty.term (Sign.pp thy) tm)])); |
315 |
313 |
337 |
335 |
338 local |
336 local |
339 |
337 |
340 fun gen_add_finals prep_term overloaded raw_terms thy = |
338 fun gen_add_finals prep_term overloaded raw_terms thy = |
341 let |
339 let |
|
340 val pp = Sign.pp thy; |
342 fun finalize tm finals = |
341 fun finalize tm finals = |
343 let |
342 let |
344 fun err msg = raise TERM (msg, [tm]); (* FIXME error!? *) |
343 val _ = no_vars pp tm; |
345 val (c, defT) = |
344 val const as (c, _) = |
346 (case tm of Const x => x |
345 (case tm of Const x => x |
347 | Free _ => err "Attempt to finalize variable (or undeclared constant)" |
346 | Free _ => error "Attempt to finalize variable (or undeclared constant)" |
348 | _ => err "Attempt to finalize non-constant term"); |
347 | _ => error "Attempt to finalize non-constant term") |
349 val declT = Sign.the_const_type thy c |
348 |> check_overloading thy overloaded; |
350 handle TYPE (msg, _, _) => err msg; |
349 in finals |> Defs.declare (c, Sign.the_const_type thy c) |> Defs.finalize const end; |
351 val _ = (* FIXME unify messages with defs *) |
|
352 (case overloading thy overloaded declT defT of |
|
353 Clean => () |
|
354 | Implicit => warning ("Finalizing " ^ quote c ^ |
|
355 " at a strictly less general type than declared") |
|
356 | Useless => err "Sort constraints stronger than declared"); |
|
357 in finals |> Defs.declare (c, declT) |> Defs.finalize (c, defT) end; |
|
358 in thy |> map_defs (fold finalize (map (prep_term thy) raw_terms)) end; |
350 in thy |> map_defs (fold finalize (map (prep_term thy) raw_terms)) end; |
359 |
351 |
360 fun read_term thy = Sign.simple_read_term thy TypeInfer.logicT; |
352 fun read_term thy = Sign.simple_read_term thy TypeInfer.logicT; |
361 fun cert_term thy = #1 o Sign.certify_term (Sign.pp thy) thy; |
353 fun cert_term thy = #1 o Sign.certify_term (Sign.pp thy) thy; |
362 |
354 |