File ‹consts.ML›
signature CONSTS =
sig
val add_const_data: string * (term -> bool) -> theory -> theory
val detect_const: theory -> term -> string option
val detect_const_ctxt: Proof.context -> term -> string option
val is_const: theory -> term -> bool
val is_const_ctxt: Proof.context -> term -> bool
val neq_const: theory -> term * term -> bool
val neq_const_ctxt: Proof.context -> term * term -> bool
end;
structure Consts : CONSTS =
struct
structure Data = Theory_Data
(
type T = ((term -> bool) * serial) Symtab.table;
val empty = Symtab.empty;
val merge = Symtab.merge (eq_snd op =);
)
fun add_const_data (str, f) =
Data.map (Symtab.update_new (str, (f, serial ())))
fun detect_const thy t =
let
val data = Symtab.dest (Data.get thy)
in
get_first (fn (str, (f, _)) => if f t then SOME str else NONE) data
end
fun detect_const_ctxt ctxt t =
detect_const (Proof_Context.theory_of ctxt) t
fun is_const thy t =
is_some (detect_const thy t)
fun is_const_ctxt ctxt t =
is_const (Proof_Context.theory_of ctxt) t
fun neq_const thy (t1, t2) =
let
val ty1 = the (detect_const thy t1)
val ty2 = the (detect_const thy t2)
in
ty1 = ty2 andalso not (t1 aconv t2)
end
handle Option.Option => false
fun neq_const_ctxt ctxt (t1, t2) =
neq_const (Proof_Context.theory_of ctxt) (t1, t2)
end