Index of types

any [Session_itp]
any_pp [Pretty]
arg [Getopt]
assertion_kind [Expr]
assign [Expr]
attr [Ptree]

attributes, with a specific case for a source location

attribute [Ident]
bad_instance [Theory]
big_float [Pinterp_core.Value]
binder [Ptree]
binop [Term]
blacklist [Printer]
call_set [Decl]
cexp [Expr]
cexp_node [Expr]
check_term [Pinterp_core]

A function of type check_term comprises a RAC engine.

check_value [Pinterp_core]
classification [Check_ce]

The result of a classification based on normal and giant-step RAC execution is comprised of a verdict itself and the log of the relevant execution.

clone_map [Task]
clone_subst [Ptree]

The possible "clone" substitution elements

cmptr [Util]

A comparator for values of type 'a *

cntr_ctx [Pinterp_core]

A contradiction context carries all necessary information about a contradiction (with snapshot'ed values).

color [Itp_communication]

Used to give colors to the parts of the source code that corresponds to the following property in the current task.

compare [Util]
compute_term [Pinterp_core]

Reduce a term (for RAC or for computing ghost expressions).

concrete_syntax_binop [Model_parser]

Binary operators

concrete_syntax_bv [Model_parser]


concrete_syntax_constant [Model_parser]


concrete_syntax_float [Model_parser]
concrete_syntax_float_value [Model_parser]


concrete_syntax_frac [Model_parser]


concrete_syntax_fun [Model_parser]

Function arguments and body

concrete_syntax_funlit [Model_parser]

Function literal value

concrete_syntax_funlit_elts [Model_parser]
concrete_syntax_int [Model_parser]


concrete_syntax_quant [Model_parser]


concrete_syntax_real [Model_parser]
concrete_syntax_term [Model_parser]

Concrete term

config [Whyconf]

A configuration linked to an rc file.

config_editor [Whyconf]
config_param [Itp_communication]
config_prover [Whyconf]
config_strategy [Whyconf]
constructor [Decl]

constructor symbol with the list of projections

controller [Controller_itp]
ctx [Pinterp]

The execution context

cty [Ity]
data_decl [Decl]
decl [Ptree]

top-level declarations

decl [Decl]
decl_node [Decl]
default_format [Number]
delayed_format [Number]
diff_decl [Trans]
doc [Getopt]
driver [Driver]
effect [Ity]
elt [Extset.S]

The type of set elements.

enumeration [Extmap.S]

enumeration: zipper style

env [Pinterp_core]

The parts of the execution environment in Pinterp which are relevant for Rac.

env [Env]
exec_log [Pinterp_core.Log]
exec_mode [Pinterp_core.Log]
exn_branch [Ptree]

An exception match branch

exn_branch [Expr]
expr [Ptree]

Expressions, equipped with a source location

expr [Expr]
expr_desc [Ptree]

Expression kinds

expr_id [Expr]
expr_node [Expr]
extension [Env]
family [Rc]

A family of parameterized sections in a configuration file.

fformat [Env]
field [Ptree]

record fields

field [Pinterp_core.Value]
field_info [Printer]
file [Session_itp]
fileID [Session_itp]
filename [Env]
filter_prover [Whyconf]

filter prover

flag [Debug]
flag_trans [Trans]
float_format [Number]
float_mode [Pinterp_core.Value]
fold [Util]
fold2 [Util]
foldd [Util]
for_bounds [Expr]
for_direction [Expr]
format_parser [Env]

(fn : 'a format_parser) env path file ch parses the in_channel ch and returns the language-specific contents of type 'a.

formatted [Pp]

formatted: string which is formatted "@ " allow to cut the line if too long

formatter [Pp]
frac_real_format [Number]
fundef [Ptree]

Local function definition

gentrans [Trans]
ghost [Ptree]
global_information [Itp_communication]

Global information known when server process has started and that can be shared with the IDE through communication

handler [Getopt]
ide_request [Itp_communication]
ident [Ptree]

identifiers, with attributes and a source location

ident [Ident]
ident_printer [Ident]
ind_decl [Ptree]

A single declaration of an inductive predicate

ind_decl [Decl]
ind_list [Decl]
ind_sign [Decl]
int_constant [Number]
int_literal_kind [Number]
int_range [Number]
int_value [Number]
integer_format [Number]
interface [Printer]
interface_export_map [Printer]
interface_map [Printer]
invariant [Ptree]
invariant [Expr]
its_defn [Pdecl]
its_flag [Ity]
ity [Ity]
ity_node [Ity]
ity_subst [Ity]
itysymbol [Ity]
key [Getopt]
key [Exthtbl.Private]
key [Weakhtbl.S]
key [Extmap.S]

The type of the map keys.

known_map [Pdecl]
known_map [Decl]
language [Env]
let_defn [Expr]
log_entry [Pinterp_core.Log]
log_entry_desc [Pinterp_core.Log]
log_uc [Pinterp_core.Log]
logic_decl [Ptree]

A single declaration of a function or predicate

logic_decl [Decl]
ls_defn [Decl]
lsymbol [Term]
main [Whyconf]
mask [Ity]
message_notification [Itp_communication]
meta [Theory]
meta_arg [Theory]
meta_arg_type [Theory]
meta_decl [Pdecl]
meta_map [Task]
metarg [Ptree]

Arguments of "meta" declarations

mlw_file [Ptree]
mlw_file [Pmodule]
mod_inst [Pmodule]
mod_unit [Pmodule]
model [Model_parser]
model_element [Model_parser]

Counter-example model elements.

model_element_kind [Model_parser]
model_parser [Model_parser]

Parses the input string (i.e.

mpfr_float [Mlmpfr_wrapper]
mpfr_rnd_t [Mlmpfr_wrapper]
namespace [Theory]
namespace [Pmodule]
naming_table [Trans]

In order to interpret, that is type, string arguments as symbols or terms, a transformation may need a naming_table.

next_unproved_node_strat [Itp_communication]
node_ID [Itp_communication]
node_type [Itp_communication]
notation [Ident]
notification [Itp_communication]
notifier [Session_itp]
number_support [Number]
oneway [Ity]
opt [Getopt]
oracle [Pinterp_core]

An oracle provides values during execution in Pinterp for program parameters and during giant steps.

oracle_quant_var [Rac]

An oracle to get all-quantified variables during RAC.

overload [Pmodule]
param [Ptree]

parameter as 4-uple (loc,id,ghost,type) to represent "ghost? id? : type".

pat_desc [Ptree]
pat_ghost [Expr]
pathname [Env]
pattern [Term]
pattern [Ptree]

Patterns, equipped with a source location

pattern_node [Term]
pdecl [Pdecl]
pdecl_node [Pdecl]
pmodule [Pmodule]
pmodule_uc [Pmodule]
position [Loc]
post [Ptree]

Normal postconditions

post [Ity]
pp [Pp]
pre [Ptree]


pre [Ity]
pre_pattern [Expr]
preid [Ident]

a user-created type of unregistered identifiers

prelude [Printer]
prelude_export_map [Printer]
prelude_map [Printer]
premises [Pinterp_core]

The premises during RAC, i.e.

printer [Printer]

A printer receives a printer_args which is created from the information contained in the driver file.

printer_args [Printer]
printers [Mlw_printer]

The marked printer potentially adds the marker, the closed printer adds parentheses to the potentially marked node

printing_info [Printer]

The printing info is collected while printing a task to trace back elements in the output of the printer to elements in the task and the AST.

prog_pattern [Expr]
prog_symbol [Pmodule]
proofAttemptID [Session_itp]
proofNodeID [Session_itp]
proof_attempt_node [Session_itp]
proof_attempt_status [Controller_itp]
proof_parent [Session_itp]
prop_decl [Decl]
prop_kind [Decl]
prover [Whyconf]

record of necessary data for a given external prover

prover_answer [Call_provers]
prover_call [Call_provers]

Type that represents a single prover run

prover_result [Call_provers]
prover_result_parser [Call_provers]
prover_update [Call_provers]
prover_upgrade_policy [Whyconf]
prsymbol [Decl]
pty [Ptree]

type expressions

pvsymbol [Ity]
qualid [Ptree]

qualified identifiers

quant [Term]
rac [Pinterp_core]

RAC is defined by a single function Pinterp_core.check_term.

rac_result [Check_ce]
rac_result_state [Check_ce]

The result state of a RAC execution

raw_model_parser [Model_parser]
rc_value [Rc]
real_constant [Number]
real_format [Number]
real_literal_kind [Number]
real_value [Number]
rec_defn [Expr]
reg_branch [Ptree]

A regular match branch

reg_branch [Expr]
region [Ity]
report [Controller_itp.Make]
resource_limit [Call_provers]
result [Pinterp]

An execution may terminate normally, with an exception, or with an irreducible expression.

rs_kind [Expr]
rs_logic [Expr]
rsymbol [Expr]
section [Rc]

A section in a configuration file.

session [Session_itp]
sign [Mlmpfr_wrapper]
simple_family [Rc]

A family of sections without parameters.

spec [Ptree]


spec [Loc.Args]
spec [Debug.Args]
stat [Debug]
state [Ptree_helpers.F]
stepregexp [Call_provers]

The type of precompiled regular expressions for parsing of steps

strategy [Itp_communication]
strategy_from_rac [Check_ce]

Type of strategies to select a model from the RAC execution results.

strategy_status [Controller_itp]
symbol [Args_wrapper]
symbol_map [Theory]
syntax [Pretty]
syntax_map [Printer]
t [Wstdlib.TaggedType]
t [Wstdlib.OrderedHashedType]
t [Weakhtbl.Weakey]
t [Rc]

A parsed configuration file.

t [Exthtbl.Private]

Private Hashtbl

t [Weakhtbl.S]
t [Extset.S]

The type of sets of type elt.

t [Extmap.S]

The type of maps from type key to type 'a.

t [Coercion]

a set of coercions

t [BigInt]
tag [Weakhtbl]
task [Task]
task_hd [Task]
tdecl [Theory]
tdecl_node [Theory]
tdecl_set [Task]
term [Term]
term [Ptree]

Terms, equipped with a source location

term_bound [Term]
term_branch [Term]
term_desc [Ptree]
term_node [Term]
term_quant [Term]
th_inst [Theory]
theory [Theory]
theory [Session_itp]
theory_uc [Theory]

theories under constructions

timeregexp [Call_provers]

The type of precompiled regular expressions for time parsing

tlist [Trans]
trans [Trans]
transID [Session_itp]
trans_typ [Args_wrapper]
trans_with_args [Trans]
trans_with_args_l [Trans]
transformation [Itp_communication]
transformation_status [Controller_itp]
trigger [Term]
tvsymbol [Ty]
ty [Ty]
ty_node [Ty]
type_decl [Ptree]
type_def [Ty]
type_def [Ptree]

Type definition body

tysymbol [Ty]
update_info [Itp_communication]
value [Pinterp_core.Value]
value_desc [Pinterp_core.Value]
value_or_invalid [Pinterp_core.Log]
variant [Ptree]

Variant for both loops and recursive functions.

variant [Expr]

tau * (tau -> tau -> prop)

verdict [Check_ce]

Verdict of the classification.

visibility [Ptree]
vs_graph [Decl]
vsymbol [Term]
warning_id [Loc]

warning identifiers

why_prover [Rac.Why]

The configuration of the prover used for reducing terms in RAC

xpost [Ptree]

Exceptional postconditions

xsymbol [Ity]