A |
adjacency [Wstdlib.MakeSCC] |
|
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] |
|
B |
bad_instance [Theory] |
|
big_float [Pinterp_core.Value] |
|
binder [Ptree] |
|
binop [Term] |
|
blacklist [Printer] |
|
C |
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] |
|
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] |
|
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] |
|
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] |
|
cty [Ity] |
|
D |
data_decl [Decl] |
|
decl [Ptree] |
|
decl [Decl] |
|
decl_node [Decl] |
|
default_format [Number] |
|
delayed_format [Number] |
|
diff_decl [Trans] |
|
doc [Getopt] |
|
driver [Driver] |
|
E |
effekt [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] |
|
expr_id [Expr] |
|
expr_node [Expr] |
|
extension [Env] |
|
F |
family [Rc] |
A family of parameterized sections in a configuration file.
|
fformat [Env] |
|
field [Ptree] |
|
field [Pinterp_core.Value] |
|
field_info [Printer] |
|
file [Session_itp] |
|
fileID [Session_itp] |
|
filename [Env] |
|
filter_prover [Whyconf] |
|
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
|
G |
gen_strat [Strategy] |
|
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
|
H |
handler [Getopt] |
|
I |
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] |
|
instruction [Strategy] |
|
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] |
|
K |
key [Getopt] |
|
key [Exthtbl.Private] |
|
key [Weakhtbl.S] |
|
key [Extmap.S] |
The type of the map keys.
|
known_map [Pdecl] |
|
known_map [Decl] |
|
L |
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] |
|
M |
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] |
|
N |
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] |
|
O |
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] |
|
P |
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] |
|
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] |
|
proof_tree [Strategy] |
|
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] |
|
pvsymbol [Ity] |
|
Q |
qualid [Ptree] |
|
quant [Term] |
|
R |
rac [Pinterp_core] |
|
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] |
|
reg_branch [Expr] |
|
region [Ity] |
|
report [Controller_itp.Make] |
|
resource_limits [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] |
|
S |
section [Rc] |
A section in a configuration file.
|
session [Session_itp] |
|
sign [Mlmpfr_wrapper] |
|
simple_family [Rc] |
A family of sections without parameters.
|
source [Wstdlib.MakeSCC] |
|
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
|
strat [Strategy] |
|
strat_with_args [Strategy] |
|
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 |
t [Wstdlib.TaggedType] |
|
t [Wstdlib.OrderedHashedType] |
|
t [Weakhtbl.Weakey] |
|
t [Strategy] |
|
t [Rc] |
A parsed configuration file.
|
t [Exthtbl.Private] |
|
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] |
|
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] |
|
tysymbol [Ty] |
|
U |
update_info [Itp_communication] |
|
V |
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.
|
vertex [Wstdlib.MakeSCC] |
|
visibility [Ptree] |
|
vs_graph [Decl] |
|
vsymbol [Term] |
|
W |
warning_id [Loc] |
|
why_prover [Rac.Why] |
The configuration of the prover used for reducing terms in RAC
|
X |
xpost [Ptree] |
Exceptional postconditions
|
xsymbol [Ity] |
|