Module Imandra_surface.Event

Toplevel Events

type fun_kind =
| Fun_defined of {
is_macro : bool;
recursive : bool;
from_lambda : bool;
}
| Fun_builtin of Builtin.Fun.t
| Fun_opaque
type validation_strategy =
| VS_validate
| VS_validate_induct
| VS_no_validate
type validation_state =
| VS_ignore

no validation

| VS_waiting

not validated yet

| VS_ok of {
processing_time : float;
}

validated

type ext_solver_name = string
type fun_data = private {
f_name : Uid.t;
f_loc : Imandra_util.Iloc.t;
f_admission : admission option Stdlib.ref;
f_validate_strat : validation_strategy;
f_ty : Type.t;
f_is_param : bool;
f_args : Var.t list;
f_body : Term.t;
f_clique : Imandra_surface.Uid.Set.t;
f_kind : fun_kind;
f_size : int;
mutable f_validate : validation_state;
f_smt_decode : string option;
f_hints : apply_hint Hints.t;
f_enable : string list;
f_disable : string list;
f_doc : Imandra_document.Document.t option;
f_subs : fun_data list;
f_code : string option;
mutable f_proofs : Imandra_document.Document.t list;
}

Definition of a function

and apply_hint = {
apply_fun : fun_data;
}

A local function that has the same signature as the theorem

and admission = {
measure_fun : Uid.t option;

custom measure function

measured_subset : string list;
proved_sound : bool;
}

Justification for a function being well-defined. In particular we have information on its termination.

and pattern_head =
| PH_id of Uid.t
| PH_datatype_op
and rewrite_rule = {
rw_name : Uid.t;
rw_head : pattern_head;
rw_lhs : Term.fo_pattern;
rw_rhs : Term.t;
rw_guard : Term.t list;
rw_vars : Imandra_surface.Var.Set.t;
rw_triggers : Term.fo_pattern list;
rw_perm_restrict : bool;
}

guard ==> lhs=rhs

and instantiation_rule = {
rule_from : fun_data;
rule_triggers : trigger list;
rule_kind : instantiation_rule_kind;
}
and instantiation_rule_kind =
| IR_forward_chaining
| IR_generalization
and trigger = {
trigger_head : pattern_head;
trigger_patterns : Term.fo_pattern list;
trigger_rule : instantiation_rule lazy_t;
}
and elimination_rule = {
er_name : Uid.t;
er_guard : Term.t list;
er_lhs : Term.t;
er_rhs : Var.t;
er_dests : Term.fo_pattern list;
er_dest_tms : Term.t list;
}
type funs_syn = {
fss_rec : bool;
fss_data : (Term.Syn.pattern * Term.Syn.t) list;
}
type funs_data = private {
fs_loc : Imandra_util.Iloc.t;
fs_data : fun_data list;
fs_syn_data : funs_syn option;
}

Definition of a block of mutually recursive functions

type type_data = Type.def

Definition of a type

type types_data = private {
tys : type_data list;
count_funs : fun_data list;
}

Definition of a single type, or a block of mutually recursive types

type as_trigger =
| Trig_none
| Trig_anon
| Trig_named of int
| Trig_rw
type upto =
| Upto_steps of int
| Upto_bound of int
type cached_verify_result =
| VR_proved
| VR_proved_upto of upto
| VR_unknown
| VR_refuted of {
model_str : string;
code : Code_fragment.t list;
}
type thm_data = private {
thm_simplify : bool;
thm_nonlin : bool;
thm_rewriting : bool;
thm_perm_restrict : bool;
thm_fc : bool;
thm_elim : bool;
thm_gen : bool;
thm_otf : bool;
thm_triggers : (Term.t * as_trigger) list;
thm_is_axiom : bool;
mutable thm_res : cached_verify_result option;
mutable thm_as_rw : rewrite_rule list;
mutable thm_as_fc : instantiation_rule list;
mutable thm_as_elim : elimination_rule list;
mutable thm_as_gen : instantiation_rule list;
}

A theorem, entered with theorem foo x y = <formula using x,y>

type verify_data = private {
verify_simplify : bool;
verify_nonlin : bool;
verify_upto : upto option;
verify_is_instance : bool;
mutable verify_res : cached_verify_result option;
}

A verify (fun x y -> <formula using x,y>) event, for nameless theorems.

type mod_data = private {
mod_name : Uid.t;

Unique name of the module.

mod_loc : Imandra_util.Iloc.t;
mod_def : mod_def;

If the module is dynamic, its parsetree is stored for re-evaluation

mod_doc : Imandra_document.Document.t option;
mutable mod_processing_time : float option;
}

A module defined in logic mode

and mod_def =
| Mod_struct of {
events : t list;

List of events in the body of the module.

}
| Mod_alias of {
target_uid : Uid.t;
}

alias to this other module

and import_data = {
import_path : string;
import_evs : t list;
}
and t = private {
ev_spec : event_spec;
ev_time : float;
ev_in_prelude : bool;
}

A toplevel event

and event_spec =
| Function of funs_data
| Type of types_data
| Theorem of thm_data
| Axiom of thm_data
| Verify of verify_data
| Instance of verify_data
| Module of mod_data
| Install_dir of {
name : string;
doc : (Imandra_document.Document.t * Imandra_document.Document.t) option;
}
| Modify_state of modify_state_op
| Import of import_data
| Custom of {
name : string;
descr : string lazy_t;
}
and modify_state_op =
| Mod_enable of Uid.t
| Mod_disable of Uid.t
| Mod_trace of Uid.t
| Mod_untrace of Uid.t
| Mod_untrace_all
type event = t
val spec : t -> event_spec
val chash_physical : t Imandra_util.Chash.hasher

Hash of the Uids of this event. This is more of a "physical equality" style of hashing, where two isomorphic events that define distinct Uids have distinct hashes

val chash_content : t Imandra_util.Chash.hasher

Hash of content of this event. Two isomorphic events that have the exact same dependencies should have the same hash

val processing_time : t -> float

Total processing time for this event

module DB : sig ... end
module Snapshot : sig ... end
val get_fun_def : Uid.t -> fun_data

Find definition of the function

raises Not_found

if the function is not found

val get_fun_def_by_name : string -> fun_data

Find definition of the function

raises Undefined_function

if the function is not found

raises Error.Unsupported

if no function with this name exists

val f_doc : fun_data -> Imandra_document.Document.t option
val f_name : fun_data -> Uid.t
val f_as_var : fun_data -> Var.t
val f_as_term : fun_data -> Term.t
val follow_trivial_alias : fun_data -> fun_data

follow_trivial_alias f returns g if let f = g

val follow_trivial_alias_id : Uid.t -> Uid.t

Define new functions/types/modules, modify existing ones

type op =
| Op_define_event of event
| Op_set_validated of {
id : Uid.t;
processing_time : float;
}
| Op_set_ty_validated of {
id : Uid.t;
processing_time : float;
}
| Op_set_mod_validated of {
id : Uid.t;
processing_time : float;
}
| Op_add_rw of pattern_head * rewrite_rule
| Op_add_fc_trigger of pattern_head * trigger
| Op_add_elim of pattern_head * elimination_rule
| Op_add_gen_trigger of pattern_head * trigger
| Op_set_thm_as_rw of Uid.t * rewrite_rule list
| Op_set_thm_as_fc of Uid.t * instantiation_rule list
| Op_set_thm_as_elim of Uid.t * elimination_rule list
| Op_set_thm_as_gen of Uid.t * instantiation_rule
| Op_set_admission of Uid.t * admission
| Op_set_verify_res of Uid.t * cached_verify_result
| Op_modify_state of modify_state_op
| Op_add_proof of Uid.t * Imandra_document.Document.t
module Op : sig ... end

Helpers

val is_fun_defined : fun_data -> bool
val is_fun_builtin : fun_data -> bool
val mk_fun_data : name:Imandra_surface.Uid.Set.elt -> args:Var.t list -> ty:Type.t -> body:Term.t -> ?⁠doc:Imandra_document.Document.t -> ?⁠loc:Imandra_util.Iloc.t -> ?⁠clique:Imandra_surface.Uid.Set.t -> ?⁠is_param:bool -> ?⁠smt_decode:string -> ?⁠admission:admission option Stdlib.ref -> ?⁠validate:validation_state -> ?⁠validate_strat:validation_strategy -> ?⁠reuse_lambdas:bool -> ?⁠kind:fun_kind -> ?⁠hints:apply_hint Hints.t -> ?⁠enable:string list -> ?⁠disable:string list -> ?⁠code:string -> ?⁠subs:fun_data list -> unit -> fun_data

Smart constructor for building function definitions

val update_fun_data : ?⁠subs:fun_data list -> name:Uid.t -> body:Term.t -> fun_data -> fun_data
val mk_defined_kind : ?⁠is_macro:bool -> ?⁠from_lambda:bool -> recursive:bool -> unit -> fun_kind
val mk_funs_data : ?⁠loc:Imandra_util.Iloc.t -> ?⁠syn:funs_syn -> fun_data list -> funs_data
val mk_thm_data : ?⁠simplify:bool -> ?⁠nonlin:bool -> ?⁠rewriting:bool -> ?⁠perm_restrict:bool -> ?⁠fc:bool -> ?⁠elim:bool -> ?⁠gen:bool -> ?⁠otf:bool -> ?⁠triggers:(Term.t * as_trigger) list -> is_axiom:bool -> fun_data -> thm_data
val mk_verify_data : ?⁠simplify:bool -> ?⁠nonlin:bool -> ?⁠upto:upto -> is_instance:bool -> fun_data -> verify_data
val mk_mod_data : ?⁠loc:Imandra_util.Iloc.t -> ?⁠doc:Imandra_document.Document.t -> name:Uid.t -> mod_def -> mod_data
val mk_types_data : ?⁠count_funs:fun_data list -> type_data list -> types_data
val make : ?⁠in_prelude:bool -> event_spec -> t
val custom : string -> string lazy_t -> t
val import : path:string -> t list -> t
val fun_validated : fun_data -> bool
val is_defined : fun_data -> bool
val is_macro : fun_data -> bool
val recursive : fun_data -> bool
val get_rw : pattern_head -> rewrite_rule list
val get_fc : pattern_head -> trigger list
val get_elim : pattern_head -> elimination_rule list
val get_gen : pattern_head -> trigger list
val is_active : Uid.t -> bool
val rw_active : rewrite_rule -> bool
val ir_active : instantiation_rule -> bool
val elim_active : elimination_rule -> bool
val rw_traced : rewrite_rule -> bool
val ir_traced : instantiation_rule -> bool
val modify_state : modify_state_op -> unit
val enable : Uid.t -> unit
val disable : Uid.t -> unit
val enable_trace : Uid.t -> unit
val disable_trace : Uid.t -> unit
val disable_trace_all : unit -> unit
val traced : Uid.t -> bool
val names : t -> Uid.t list
val names_spec : event_spec -> Uid.t list
val locs : t -> Imandra_util.Iloc.t list
val depends_on : t -> Imandra_surface.Uid.Set.t
val walk_deps_dag : ?⁠exclude_prelude:bool -> Uid.t -> t list

recursive_deps f returns a topologically-sorted list of types and functions that f transitively depends on.

parameter exclude_prelude

if true (default true) do not return functions from the prelude

val walk_deps_dag_l : ?⁠exclude_prelude:bool -> Uid.t list -> t list

Similar to walk_deps_dag but for the dependencies of a set of symbols

val sub_events : t -> t list

Immediate sub-events

val exec_apply_hint : apply_hint list -> fun_data -> fun_data * bool

Enrich the predicate using the given apply hints, by adding them on the LHS of an implication.

returns

a pair (f', modified), where f = f' if not modified or 'f is the augmented version of f if modified

val print_fun : Stdlib.Format.formatter -> fun_data -> unit

Printer of function definition

val print_apply_hint : Stdlib.Format.formatter -> apply_hint -> unit
val print_trigger : Stdlib.Format.formatter -> trigger -> unit
val print_triggers : Stdlib.Format.formatter -> trigger list -> unit
val print_pattern_head : Stdlib.Format.formatter -> pattern_head -> unit
val print_rw : Stdlib.Format.formatter -> rewrite_rule -> unit
val print_ir : Stdlib.Format.formatter -> instantiation_rule -> unit
val print_elim : Stdlib.Format.formatter -> elimination_rule -> unit
val print_upto : Stdlib.Format.formatter -> upto -> unit
val print_upto_opt : Stdlib.Format.formatter -> upto option -> unit
val print_fss : Stdlib.Format.formatter -> funs_syn -> unit
val print_cached_verify_result : Stdlib.Format.formatter -> cached_verify_result -> unit
val map_spec : f:(event_spec -> event_spec) -> t -> t
module PH : sig ... end
val to_string_short : t -> string
val print_short : t CCFormat.printer
val to_doc : ?⁠body:bool -> t -> Imandra_document.Document.t
module Builtins : sig ... end
val with_enable_disable : enable:string list -> disable:string list -> ('a -> 'b) -> 'a -> 'b
module Iml : sig ... end