Module Ident

module Ident: sig .. end

Identifiers


Attributes

type attribute = private {
   attr_string : string;
   attr_tag : int;
}
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

Naming convention

type notation = 
| SNword of string
| SNinfix of string
| SNtight of string
| SNprefix of string
| SNget of string
| SNset of string
| SNupdate of string
| SNcut of string
| SNlcut of string
| SNrcut of string
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

Identifiers

type ident = private {
   id_string : string; (*

non-unique name

*)
   id_attrs : Sattr.t; (*

identifier attributes

*)
   id_loc : Loc.position option; (*

optional location

*)
   id_tag : Weakhtbl.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 : string;
   pre_attrs : Sattr.t;
   pre_loc : Loc.position option;
}

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

Name handling for ITP

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

General purpose attributes

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.

Attributes for handling counterexamples

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