ident.mli 6.6 KB
Newer Older
Andrei Paskevich's avatar
Andrei Paskevich committed
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
4
(*  Copyright 2010-2018   --   Inria - CNRS - Paris-Sud University  *)
Andrei Paskevich's avatar
Andrei Paskevich committed
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
(*                                                                  *)
Andrei Paskevich's avatar
Andrei Paskevich committed
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 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66
(** {2 Naming convention} *)

type notation =
  | SNword   of string
  | SNinfix  of string
  | SNprefix of string
  | SNget  (* [] *)
  | SNset  (* []<- *)
  | SNupd  (* [<-] *)
  | SNcut  (* [..] *)
  | SNlcut (* [.._] *)
  | SNrcut (* [_..] *)

val sn_encode : notation -> string
(* encode the symbol name as a string *)

val sn_decode : string -> notation
(* decode the string as a symbol name *)

val str_decode : string -> string
(* decode the string as a symbol name and pretty-print it *)

(* specialized encoders *)

val op_infix  : string -> string
val op_prefix : string -> string

val op_equ  : string
val op_neq  : string
val op_get  : string
val op_set  : string
val op_upd  : string
val op_cut  : string
val op_lcut : string
val op_rcut : string
67

MARCHE Claude's avatar
MARCHE Claude committed
68
(** {2 Identifiers} *)
69 70

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

77 78 79
module Mid : Extmap.S with type key = ident
module Sid : Extset.S with module M = Mid
module Hid : Exthtbl.S with type key = ident
Andrei Paskevich's avatar
Andrei Paskevich committed
80
module Wid : Weakhtbl.S with type key = ident
81

Andrei Paskevich's avatar
Andrei Paskevich committed
82
val id_compare : ident -> ident -> int
83
val id_equal : ident -> ident -> bool
Andrei Paskevich's avatar
Andrei Paskevich committed
84 85
val id_hash : ident -> int

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

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

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

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

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

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

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

111
(* DEPRECATED : retrieve preid name without registering *)
112
val preid_name : preid -> string
Francois Bobot's avatar
Francois Bobot committed
113

114 115
(** Unique persistent names for pretty printing *)

116
type ident_printer
117

118 119
val create_ident_printer :
  ?sanitizer : (string -> string) -> string list -> ident_printer
MARCHE Claude's avatar
MARCHE Claude committed
120
(** start a new printer with a sanitizing function and a blacklist *)
121

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

127
val string_unique : ident_printer -> string -> string
MARCHE Claude's avatar
MARCHE Claude committed
128
(** Uniquify string *)
129

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

134
val forget_id : ident_printer -> ident -> unit
MARCHE Claude's avatar
MARCHE Claude committed
135
(** forget an ident *)
136

137
val forget_all : ident_printer -> unit
MARCHE Claude's avatar
MARCHE Claude committed
138
(** forget all idents *)
139

140 141 142
val sanitizer' : (char -> string) -> (char -> string) -> (char -> string) -> string -> string
(** generic sanitizer taking a separate encoder for the first and last letter *)

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

(** various character encoders *)
147 148 149 150 151

val char_to_alpha : char -> string
val char_to_lalpha : char -> string
val char_to_ualpha : char -> string
val char_to_alnum : char -> string
152
val char_to_lalnum : char -> string
153
val char_to_alnumus : char -> string
154
val char_to_lalnumus : char -> string
155 156 157 158


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

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

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

Andrei Paskevich's avatar
Andrei Paskevich committed
167
val model_projected_attr : attribute
168

Andrei Paskevich's avatar
Andrei Paskevich committed
169 170 171
val model_vc_attr : attribute
val model_vc_post_attr : attribute
val model_vc_havoc_attr : attribute
172

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

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

Andrei Paskevich's avatar
Andrei Paskevich committed
179
val create_model_trace_attr : string -> attribute
180

Andrei Paskevich's avatar
Andrei Paskevich committed
181
val is_model_trace_attr : attribute -> bool
182

Andrei Paskevich's avatar
Andrei Paskevich committed
183 184 185
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:*"]
186 187
    will be ["model_trace:*to_append"]. *)

Andrei Paskevich's avatar
Andrei Paskevich committed
188 189 190
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:*@*"]
191 192
    will be ["model_trace:*to_append@*"]. *)

Andrei Paskevich's avatar
Andrei Paskevich committed
193 194 195 196
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:*"]. *)
197

Andrei Paskevich's avatar
Andrei Paskevich committed
198 199 200 201
val get_model_trace_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:*"]. *)
202

Andrei Paskevich's avatar
Andrei Paskevich committed
203 204 205
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. *)