ident.mli 6.14 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 *)

MARCHE Claude's avatar
MARCHE Claude committed
14 15
(** {2 Labels} *)

Andrei Paskevich's avatar
Andrei Paskevich committed
16 17 18 19 20
type label = private {
  lab_string : string;
  lab_tag    : int;
}

21 22
module Mlab : Extmap.S with type key = label
module Slab : Extset.S with module M = Mlab
23

Andrei Paskevich's avatar
Andrei Paskevich committed
24
val lab_compare : label -> label -> int
Andrei Paskevich's avatar
Andrei Paskevich committed
25
val lab_equal : label -> label -> bool
Andrei Paskevich's avatar
Andrei Paskevich committed
26
val lab_hash : label -> int
Andrei Paskevich's avatar
Andrei Paskevich committed
27 28

val create_label : string -> label
MARCHE Claude's avatar
MARCHE Claude committed
29

30 31
val list_label: unit -> string list

32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47
(** {2 Naming convention } *)

val infix: string -> string
(** Apply the naming convention for infix operator (+) *)

val prefix: string -> string
(** Apply the naming convention for prefix operator *)

val mixfix: string -> string
(** Apply the naming convention for mixfix operator *)

val kind_of_fix: string -> [ `None
                           | `Prefix of string
                           | `Infix  of string
                           | `Mixfix of string ]

MARCHE Claude's avatar
MARCHE Claude committed
48
(** {2 Identifiers} *)
49 50

type ident = private {
Piotr Trojanek's avatar
Piotr Trojanek committed
51 52 53 54
  id_string : string;               (** non-unique name *)
  id_label  : Slab.t;               (** identifier labels *)
  id_loc    : Loc.position option;  (** optional location *)
  id_tag    : Weakhtbl.tag;         (** unique magical tag *)
55 56
}

57 58 59
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
60
module Wid : Weakhtbl.S with type key = ident
61

Andrei Paskevich's avatar
Andrei Paskevich committed
62
val id_compare : ident -> ident -> int
63
val id_equal : ident -> ident -> bool
Andrei Paskevich's avatar
Andrei Paskevich committed
64 65
val id_hash : ident -> int

Piotr Trojanek's avatar
Piotr Trojanek committed
66
(** a user-created type of unregistered identifiers *)
67 68 69 70 71
type preid = {
  pre_name  : string;
  pre_label : Slab.t;
  pre_loc   : Loc.position option;
}
72

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

Piotr Trojanek's avatar
Piotr Trojanek committed
76
(** create a fresh pre-ident *)
77
val id_fresh : ?label:Slab.t -> ?loc:Loc.position -> string -> preid
78

Piotr Trojanek's avatar
Piotr Trojanek committed
79
(** create a localized pre-ident *)
80
val id_user : ?label:Slab.t -> string -> Loc.position -> preid
81

Piotr Trojanek's avatar
Piotr Trojanek committed
82
(** create a duplicate pre-ident with given labels *)
83 84
val id_lab : Slab.t -> ident -> preid

Piotr Trojanek's avatar
Piotr Trojanek committed
85
(** create a duplicate pre-ident *)
86
val id_clone : ?label:Slab.t -> ident -> preid
87

Piotr Trojanek's avatar
Piotr Trojanek committed
88
(** create a derived pre-ident (inherit labels and location) *)
89
val id_derive : ?label:Slab.t -> string -> ident -> preid
90

91
(* DEPRECATED : retrieve preid name without registering *)
92
val preid_name : preid -> string
Francois Bobot's avatar
Francois Bobot committed
93

94 95
(** Unique persistent names for pretty printing *)

96
type ident_printer
97

98 99
val create_ident_printer :
  ?sanitizer : (string -> string) -> string list -> ident_printer
MARCHE Claude's avatar
MARCHE Claude committed
100
(** start a new printer with a sanitizing function and a blacklist *)
101

102 103
val id_unique :
  ident_printer -> ?sanitizer : (string -> string) -> ident -> string
104
(** use ident_printer to generate a unique name for ident
MARCHE Claude's avatar
MARCHE Claude committed
105
    an optional sanitizer is applied over the printer's sanitizer *)
106

107
val string_unique : ident_printer -> string -> string
MARCHE Claude's avatar
MARCHE Claude committed
108
(** Uniquify string *)
109

110 111 112 113
val known_id: ident_printer -> ident -> bool
(** Returns true if the printer already knows the id.
    false if it does not. *)

114
val forget_id : ident_printer -> ident -> unit
MARCHE Claude's avatar
MARCHE Claude committed
115
(** forget an ident *)
116

117
val forget_all : ident_printer -> unit
MARCHE Claude's avatar
MARCHE Claude committed
118
(** forget all idents *)
119

120 121 122
val sanitizer' : (char -> string) -> (char -> string) -> (char -> string) -> string -> string
(** generic sanitizer taking a separate encoder for the first and last letter *)

123
val sanitizer : (char -> string) -> (char -> string) -> string -> string
MARCHE Claude's avatar
MARCHE Claude committed
124 125 126
(** generic sanitizer taking a separate encoder for the first letter *)

(** various character encoders *)
127 128 129 130 131

val char_to_alpha : char -> string
val char_to_lalpha : char -> string
val char_to_ualpha : char -> string
val char_to_alnum : char -> string
132
val char_to_lalnum : char -> string
133
val char_to_alnumus : char -> string
134
val char_to_lalnumus : char -> string
135 136 137 138 139 140 141 142 143 144 145 146 147


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

val id_unique_label :
  ident_printer -> ?sanitizer : (string -> string) -> ident -> string
(** Do the same as id_unique except that it tries first to
   use the "name:" label to generate the name instead of id.id_string *)



(** {2 labels for handling counterexamples} *)

148 149 150 151
val model_label : label
val model_projected_label : label
val model_vc_label : label
val model_vc_post_label : label
152

153 154
val has_a_model_label : ident -> bool
(** [true] when [ident] has one of the labels above. *)
155 156

val remove_model_labels : labels : Slab.t -> Slab.t
157 158 159 160 161
(** Returns a copy of labels without [model_label] and [model_projected_label]. *)

val create_model_trace_label : string -> label

val is_model_trace_label : label -> bool
162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189

val append_to_model_trace_label : labels : Slab.t ->
  to_append : string ->
  Slab.t
(** The returned set of labels will contain the same set of labels
    as argument labels except that a label of the form ["model_trace:*"]
    will be ["model_trace:*to_append"]. *)

val append_to_model_element_name : labels : Slab.t ->
  to_append : string ->
  Slab.t
(** The returned set of labels will contain the same set of labels
    as argument labels except that a label of the form ["model_trace:*@*"]
    will be ["model_trace:*to_append@*"]. *)

val get_model_element_name : labels : Slab.t -> string
(** If labels contain a label of the form ["model_trace:name@*"],
    return ["name"].
    Throws [Not_found] if there is no label of the form ["model_trace:*"]. *)

val get_model_trace_string : labels : Slab.t -> string
(** If labels contain a label of the form ["model_trace:mt_string"],
    return ["mt_string"].
    Throws [Not_found] if there is no label of the form ["model_trace:*"]. *)

val get_model_trace_label : labels : Slab.t -> Slab.elt
(** Return a label of the form ["model_trace:*"].
    Throws [Not_found] if there is no such label. *)