Module Event.DB

Database of definitions. Use with care

type t
val fun_id_of_str : ?⁠loc:Imandra_util.Iloc.t -> ?⁠db:t -> string -> Uid.t

Find the unique ID of the function with the given (qualified) name.

raises Error.Unsupported

if no such function is found

val mod_id_of_str : ?⁠loc:Imandra_util.Iloc.t -> ?⁠db:t -> string -> Uid.t

Find the unique ID of the module with the given (qualified) name.

raises Error.Unsupported

if no such module is found

val thm_id_of_str : ?⁠loc:Imandra_util.Iloc.t -> ?⁠db:t -> string -> Uid.t

Find the unique ID of the theorem with the given (qualified) name.

raises Error.Unsupported

if no such theorem is found

val ty_id_of_str : ?⁠loc:Imandra_util.Iloc.t -> ?⁠db:t -> string -> Uid.t
val fun_or_thm_id_of_str : ?⁠loc:Imandra_util.Iloc.t -> ?⁠db:t -> string -> Uid.t
val fun_mod_id_of_str : ?⁠loc:Imandra_util.Iloc.t -> ?⁠db:t -> string -> Uid.t

Find the unique ID of the function or module with the given (qualified) name. Whether we look for a function or module depends on lexical properties of the name (is the unqualified part of the name capitalized?)

raises Error.Unsupported

if no such function/module is found

val mem_fun : ?⁠db:t -> Uid.t -> bool

Is this function defined?

val mem_thm : ?⁠db:t -> Uid.t -> bool

Is this theorem defined?

val mem_ty : ?⁠db:t -> Uid.t -> bool
val fun_exists : ?⁠db:t -> string -> bool

Is there a function with this name?

val ty_exists : ?⁠db:t -> string -> bool

Is there a type with this name?

val count_fun_of_ty : ?⁠db:t -> Uid.t -> fun_data option

count_fun_of_ty ty returns the function for mapping values of this type to ordinals, if one is defined.

val find_fun : ?⁠db:t -> Uid.t -> fun_data

Find definition of the function with given unique ID

raises Not_found

if the definition is not found

val find_ty : ?⁠db:t -> Uid.t -> type_data
val find_mod : ?⁠db:t -> Uid.t -> mod_data

Find definition of the module with given unique ID

raises Not_found

if the definition is not found

val mod_exists : ?⁠db:t -> string -> bool

Is there a module with this name?

val mem_mod : ?⁠db:t -> Uid.t -> bool
val find_fun_by_name : ?⁠db:t -> string -> fun_data
val find_thm_by_name : ?⁠db:t -> string -> thm_data
val find_mod_by_name : ?⁠db:t -> string -> mod_data
val find_ty_by_name : ?⁠db:t -> string -> type_data
val find_thm : ?⁠db:t -> Uid.t -> thm_data
val thm_exists : ?⁠db:t -> string -> bool
val find : ?⁠db:t -> Uid.t -> event

Find module/function definition from its ID

raises Not_found

if the definition is not found

val find_short : ?⁠db:t -> Short_uid.t -> Uid.t option
val find_short_exn : ?⁠db:t -> Short_uid.t -> Uid.t
val chash : ?⁠db:t -> unit -> Imandra_util.Chash.t

Hash of the DB as a logical theory, including enabled/disabled symbols, rw rules, etc.

val disabled_list : ?⁠db:t -> unit -> Uid.t list
val is_fun_active : ?⁠db:t -> Uid.t -> bool

Is a function currently active (`enabled')?

val cur_ : unit -> t