ident.mli 8.11 KB
Newer Older
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
4
(*  Copyright 2010-2019   --   Inria - CNRS - Paris-Sud University  *)
5 6 7 8
(*                                                                  *)
(*  This software is distributed under the terms of the GNU Lesser  *)
(*  General Public License version 2.1, with the special exception  *)
(*  on linking described in file LICENSE.                           *)
9
(*                                                                  *)
10
(********************************************************************)
11

MARCHE Claude's avatar
MARCHE Claude committed
12 13
(** Identifiers *)

Andrei Paskevich's avatar
Andrei Paskevich committed
14
(** {2 Attributes} *)
MARCHE Claude's avatar
MARCHE Claude committed
15

Andrei Paskevich's avatar
Andrei Paskevich committed
16 17 18
type attribute = private {
  attr_string : string;
  attr_tag    : int;
Andrei Paskevich's avatar
Andrei Paskevich committed
19 20
}

Andrei Paskevich's avatar
Andrei Paskevich committed
21 22
module Mattr : Extmap.S with type key = attribute
module Sattr : Extset.S with module M = Mattr
23

Andrei Paskevich's avatar
Andrei Paskevich committed
24 25 26
val attr_compare : attribute -> attribute -> int
val attr_equal : attribute -> attribute -> bool
val attr_hash : attribute -> int
Andrei Paskevich's avatar
Andrei Paskevich committed
27

Andrei Paskevich's avatar
Andrei Paskevich committed
28
val create_attribute : string -> attribute
MARCHE Claude's avatar
MARCHE Claude committed
29

Andrei Paskevich's avatar
Andrei Paskevich committed
30
val list_attributes : unit -> string list
31

32 33 34
(** {2 Naming convention} *)

type notation =
35 36 37 38
  | SNword   of string  (* plus *)
  | SNinfix  of string  (* + *)
  | SNtight  of string  (* ! *)
  | SNprefix of string  (* -_ *)
39 40 41 42 43 44
  | SNget    of string  (* [] *)
  | SNset    of string  (* []<- *)
  | SNupdate of string  (* [<-] *)
  | SNcut    of string  (* [..] *)
  | SNlcut   of string  (* [.._] *)
  | SNrcut   of string  (* [_..] *)
45 46

val op_infix  : string -> string
47
val op_tight  : string -> string
48
val op_prefix : string -> string
49 50 51 52 53 54 55 56
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
57

58 59 60 61 62 63
val sn_decode : string -> notation
(* decode the string as a symbol name *)

val print_decoded : Format.formatter -> string -> unit
(* decode the string as a symbol name and pretty-print it *)

MARCHE Claude's avatar
MARCHE Claude committed
64
(** {2 Identifiers} *)
65 66

type ident = private {
Piotr Trojanek's avatar
Piotr Trojanek committed
67
  id_string : string;               (** non-unique name *)
Andrei Paskevich's avatar
Andrei Paskevich committed
68
  id_attrs  : Sattr.t;              (** identifier attributes *)
Piotr Trojanek's avatar
Piotr Trojanek committed
69 70
  id_loc    : Loc.position option;  (** optional location *)
  id_tag    : Weakhtbl.tag;         (** unique magical tag *)
71 72
}

73 74 75
module Mid : Extmap.S with type key = ident
module Sid : Extset.S with module M = Mid
module Hid : Exthtbl.S with type key = ident
76
module Wid : Weakhtbl.S with type key = ident
77

Andrei Paskevich's avatar
Andrei Paskevich committed
78
val id_compare : ident -> ident -> int
79
val id_equal : ident -> ident -> bool
Andrei Paskevich's avatar
Andrei Paskevich committed
80 81
val id_hash : ident -> int

Piotr Trojanek's avatar
Piotr Trojanek committed
82
(** a user-created type of unregistered identifiers *)
83 84
type preid = {
  pre_name  : string;
Andrei Paskevich's avatar
Andrei Paskevich committed
85
  pre_attrs : Sattr.t;
86 87
  pre_loc   : Loc.position option;
}
88

Piotr Trojanek's avatar
Piotr Trojanek committed
89
(** register a pre-ident (you should never use this function) *)
90
val id_register : preid -> ident
91

Piotr Trojanek's avatar
Piotr Trojanek committed
92
(** create a fresh pre-ident *)
Andrei Paskevich's avatar
Andrei Paskevich committed
93
val id_fresh : ?attrs:Sattr.t -> ?loc:Loc.position -> string -> preid
94

Piotr Trojanek's avatar
Piotr Trojanek committed
95
(** create a localized pre-ident *)
Andrei Paskevich's avatar
Andrei Paskevich committed
96
val id_user : ?attrs:Sattr.t -> string -> Loc.position -> preid
97

Andrei Paskevich's avatar
Andrei Paskevich committed
98 99
(** create a duplicate pre-ident with given attributes *)
val id_attr : ident -> Sattr.t -> preid
100

Piotr Trojanek's avatar
Piotr Trojanek committed
101
(** create a duplicate pre-ident *)
Andrei Paskevich's avatar
Andrei Paskevich committed
102
val id_clone : ?attrs:Sattr.t -> ident -> preid
103

Andrei Paskevich's avatar
Andrei Paskevich committed
104 105
(** create a derived pre-ident (inherit attributes and location) *)
val id_derive : ?attrs:Sattr.t -> string -> ident -> preid
106

107
(* DEPRECATED : retrieve preid name without registering *)
108
val preid_name : preid -> string
Francois Bobot's avatar
Francois Bobot committed
109

110 111
(** Unique persistent names for pretty printing *)

112
type ident_printer
113

114 115
val create_ident_printer :
  ?sanitizer : (string -> string) -> string list -> ident_printer
MARCHE Claude's avatar
MARCHE Claude committed
116
(** start a new printer with a sanitizing function and a blacklist *)
117

118 119 120 121 122 123 124
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.
*)

125 126
val id_unique :
  ident_printer -> ?sanitizer : (string -> string) -> ident -> string
127
(** use ident_printer to generate a unique name for ident
MARCHE Claude's avatar
MARCHE Claude committed
128
    an optional sanitizer is applied over the printer's sanitizer *)
129

130
val string_unique : ident_printer -> string -> string
MARCHE Claude's avatar
MARCHE Claude committed
131
(** Uniquify string *)
132

133 134 135 136
val known_id: ident_printer -> ident -> bool
(** Returns true if the printer already knows the id.
    false if it does not. *)

137
val forget_id : ident_printer -> ident -> unit
MARCHE Claude's avatar
MARCHE Claude committed
138
(** forget an ident *)
139

140
val forget_all : ident_printer -> unit
MARCHE Claude's avatar
MARCHE Claude committed
141
(** forget all idents *)
142

143 144 145
val sanitizer' : (char -> string) -> (char -> string) -> (char -> string) -> string -> string
(** generic sanitizer taking a separate encoder for the first and last letter *)

146
val sanitizer : (char -> string) -> (char -> string) -> string -> string
MARCHE Claude's avatar
MARCHE Claude committed
147 148 149
(** generic sanitizer taking a separate encoder for the first letter *)

(** various character encoders *)
150 151 152 153 154

val char_to_alpha : char -> string
val char_to_lalpha : char -> string
val char_to_ualpha : char -> string
val char_to_alnum : char -> string
155
val char_to_lalnum : char -> string
156
val char_to_alnumus : char -> string
157
val char_to_lalnumus : char -> string
158 159 160 161


(** {2 Name handling for ITP} *)

Andrei Paskevich's avatar
Andrei Paskevich committed
162 163
(* TODO: integrate this functionality into id_unique *)
val id_unique_attr :
164
  ident_printer -> ?sanitizer : (string -> string) -> ident -> string
Andrei Paskevich's avatar
Andrei Paskevich committed
165 166
(** 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 *)
167

DAILLER Sylvain's avatar
DAILLER Sylvain committed
168 169
val proxy_attr: attribute

Andrei Paskevich's avatar
Andrei Paskevich committed
170
(** {2 Attributes for handling counterexamples} *)
171

Andrei Paskevich's avatar
Andrei Paskevich committed
172 173
val model_projected_attr : attribute
val model_vc_post_attr : attribute
174

Andrei Paskevich's avatar
Andrei Paskevich committed
175 176
val has_a_model_attr : ident -> bool
(** [true] when [ident] has one of the attributes above *)
177

178 179 180 181 182
val relevant_for_counterexample: ident -> bool
(** [true] when [ident] is a constant value that should be used for
    counterexamples generation.
*)

183 184 185 186 187 188 189 190 191 192 193 194 195 196 197
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 extract_written_loc: attribute -> Loc.position option
(** Extract the location inside vc_written attribute. [None] if the attribute is
    ill-formed.
*)

Andrei Paskevich's avatar
Andrei Paskevich committed
198 199
val remove_model_attrs : attrs:Sattr.t -> Sattr.t
(** Remove the counter-example attributes from an attribute set *)
200

Andrei Paskevich's avatar
Andrei Paskevich committed
201
val create_model_trace_attr : string -> attribute
202

Andrei Paskevich's avatar
Andrei Paskevich committed
203
val is_model_trace_attr : attribute -> bool
204

Andrei Paskevich's avatar
Andrei Paskevich committed
205 206 207
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:*"]
208 209
    will be ["model_trace:*to_append"]. *)

Andrei Paskevich's avatar
Andrei Paskevich committed
210 211 212
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:*@*"]
213 214
    will be ["model_trace:*to_append@*"]. *)

Andrei Paskevich's avatar
Andrei Paskevich committed
215 216 217 218
val get_model_element_name : attrs:Sattr.t -> string
(** If attributes contain an attribute of the form ["model_trace:name@*"],
    return ["name"]. Raises [Not_found] if there is no attribute of
    the form ["model_trace:*"]. *)
219

220
val get_model_trace_string : name:string -> attrs:Sattr.t -> string
Andrei Paskevich's avatar
Andrei Paskevich committed
221 222 223
(** 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:*"]. *)
224

225 226 227 228 229 230 231
val compute_model_trace_field: ident option -> int -> Sattr.t
(** Take an optional projection name and the depths of its occurence 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 *)

Andrei Paskevich's avatar
Andrei Paskevich committed
232 233 234
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. *)