module Ident:sig
..end
Identifiers
type
attribute = private {
|
attr_string : |
|
attr_tag : |
}
module Mattr:Extmap.S
with type key = attribute
module Sattr:Extset.S
with module M = Mattr
val attr_compare : attribute -> attribute -> int
val attr_equal : attribute -> attribute -> bool
val attr_hash : attribute -> int
val create_attribute : string -> attribute
val list_attributes : unit -> string list
type
notation =
| |
SNword of |
| |
SNinfix of |
| |
SNtight of |
| |
SNprefix of |
| |
SNget of |
| |
SNset of |
| |
SNupdate of |
| |
SNcut of |
| |
SNlcut of |
| |
SNrcut of |
val op_infix : string -> string
val op_tight : string -> string
val op_prefix : string -> string
val op_get : string -> string
val op_set : string -> string
val op_update : string -> string
val op_cut : string -> string
val op_lcut : string -> string
val op_rcut : string -> string
val op_equ : string
val op_neq : string
val sn_decode : string -> notation
val print_decoded : Stdlib.Format.formatter -> string -> unit
type
ident = private {
|
id_string : |
(* | non-unique name | *) |
|
id_attrs : |
(* | identifier attributes | *) |
|
id_loc : |
(* | optional location | *) |
|
id_tag : |
(* | unique magical tag | *) |
}
module Mid:Extmap.S
with type key = ident
module Sid:Extset.S
with module M = Mid
module Hid:Exthtbl.S
with type key = ident
module Wid:Weakhtbl.S
with type key = ident
val id_compare : ident -> ident -> int
val id_equal : ident -> ident -> bool
val id_hash : ident -> int
type
preid = {
|
pre_name : |
|
pre_attrs : |
|
pre_loc : |
}
a user-created type of unregistered identifiers
val id_register : preid -> ident
register a pre-ident (you should never use this function)
val id_fresh : ?attrs:Sattr.t -> ?loc:Loc.position -> string -> preid
create a fresh pre-ident
val id_user : ?attrs:Sattr.t -> string -> Loc.position -> preid
create a localized pre-ident
val id_attr : ident -> Sattr.t -> preid
create a duplicate pre-ident with given attributes
val id_clone : ?loc:Loc.position -> ?attrs:Sattr.t -> ident -> preid
create a duplicate pre-ident
val id_derive : ?attrs:Sattr.t -> string -> ident -> preid
create a derived pre-ident (inherit attributes and location)
val preid_name : preid -> string
Unique persistent names for pretty printing
type
ident_printer
val create_ident_printer : ?sanitizer:(string -> string) -> string list -> ident_printer
start a new printer with a sanitizing function and a blacklist
val duplicate_ident_printer : ident_printer -> ident_printer
This is used to avoid editing the current (mutable) printer when raising exception or printing information messages for the user. This should be avoided for any other usage including display of the whole task.
val id_unique : ident_printer -> ?sanitizer:(string -> string) -> ident -> string
use ident_printer to generate a unique name for ident an optional sanitizer is applied over the printer's sanitizer
val string_unique : ident_printer -> string -> string
Uniquify string
val known_id : ident_printer -> ident -> bool
Returns true if the printer already knows the id. false if it does not.
val forget_id : ident_printer -> ident -> unit
forget an ident
val forget_all : ident_printer -> unit
forget all idents
val sanitizer' : (char -> string) -> (char -> string) -> (char -> string) -> string -> string
generic sanitizer taking a separate encoder for the first and last letter
val sanitizer : (char -> string) -> (char -> string) -> string -> string
generic sanitizer taking a separate encoder for the first letter
various character encoders
val char_to_alpha : char -> string
val char_to_lalpha : char -> string
val char_to_ualpha : char -> string
val char_to_alnum : char -> string
val char_to_lalnum : char -> string
val char_to_alnumus : char -> string
val char_to_lalnumus : char -> string
val id_unique_attr : ident_printer -> ?sanitizer:(string -> string) -> ident -> string
Do the same as id_unique except that it tries first to use the "name:" attribute to generate the name instead of id.id_string
val proxy_attr : attribute
val useraxiom_attr : attribute
val funlit : attribute
val is_field_id_attr : attribute
indicates that the related ident is a field name, and its applications should be printed in dotted notation
val builtin_attr : attribute
indicates that the related ident comes from a builtin of the language, for instance the builtin `ref` in WhyML. This is useful when filtering functions that are listed as potential culprits in counterexamples
val eid_attribute_prefix : string
the prefix string for expression identifiers in attributes
val is_eid_attr : attribute -> bool
is_eid_attr a
tells whether a
is an expression identifier attribute.
val get_eid_attr : Sattr.t -> int option
get_eid_attr s
searches in the set s
an attribute defining an
expression identifier, as prefixed by eid_attribute_prefix
.
val model_projected_attr : attribute
val model_vc_post_attr : attribute
val has_a_model_attr : ident -> bool
true
when ident
has one of the attributes above
val relevant_for_counterexample : ident -> bool
true
when ident
is a constant value that should be used for
counterexamples generation.
val create_written_attr : Loc.position -> attribute
The vc_written attribute is built during VC generation: it is used to track the location of the creation of variables. Those variables can have several creation locations with SP algorithm. These attribute-locations are used by counterexamples. The form is the following: "vc:written:line:start_column:end_column:file_name" file_name is at the end for easier parsing (file_name can contain ":")
val get_written_loc : attribute -> Loc.position option
Get the location inside vc_written attribute. None
if the attribute is
ill-formed.
val create_call_result_attr : Loc.position -> attribute
A call result attribute on a counterexample model element marks the result of a call at the given location
val get_call_result_loc : attribute -> Loc.position option
Get the call result location from an attribute.
val has_rac_assume : Sattr.t -> bool
Check if the attributes contain [@RAC:assume]
. When a program annotation
is a conjunction, conjuncts marked by this annotation are added to the
preconditions when checking the programannotation during giant-step RAC.
val search_attribute_value : (attribute -> 'a option) -> Sattr.t -> 'a option
search_attribute_value f attrs
applies f to the attributes in attr
and
returns the first inhabited result, if any, or None
otherwise.
val remove_model_attrs : attrs:Sattr.t -> Sattr.t
Remove the counter-example attributes from an attribute set
val create_model_trace_attr : string -> attribute
val is_model_trace_attr : attribute -> bool
val append_to_model_trace_attr : attrs:Sattr.t -> to_append:string -> Sattr.t
The returned set of attributes will contain the same set of attributes
as argument attrs except that an attribute of the form "model_trace:*"
will be "model_trace:*to_append"
.
val append_to_model_element_name : attrs:Sattr.t -> to_append:string -> Sattr.t
The returned set of attributes will contain the same set of attributes
as argument attrs except that an attribute of the form "model_trace:*@*"
will be "model_trace:*to_append@*"
.
val get_model_element_name : attrs:Sattr.t -> string
If attributes contain an attribute of the form
"model_trace:name(@...)?"
, return "name"
. Everything after
'@'
is ignored. Raises Not_found
if there is no attribute of
the form "model_trace:..."
.
val get_model_trace_string : name:string -> attrs:Sattr.t -> string
If attrs contain an attribute of the form "model_trace:mt_string"
,
return "mt_string"
. Raises Not_found
if there is no attribute of
the form "model_trace:*"
.
val get_element_name : attrs:Sattr.t -> string option
val suffix_attr_name : attrs:Sattr.t -> string -> Sattr.t
Add a suffix to all "name" attributes of attrs
val compute_model_trace_field : ident option -> int -> Sattr.t
Take an optional projection name and the depths of its occurrence and return the built field attribute associated
val extract_field : attribute -> (int * string) option
Take an attribute and extract its depth, name if it was a field attribute
("field:depth:field_name"
)
val get_model_trace_attr : attrs:Sattr.t -> attribute
Return an attribute of the form "model_trace:*"
.
Raises Not_found
if there is no such attribute.
val get_hyp_name : attrs:Sattr.t -> string option
If attrs contains an attribute of the form "hyp_name:<s>"
returns
Some <s>
or None
if no attribute have this form
val unused_suffix : string
Suffix for unused variables kept for counterexample generation
val unused_attr : attribute
attribute for unused variables kept for counterexample generation