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

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