ident.mli 5.86 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 32 33 34 35 36 37 38 39 40 41 42 43 44 45
(** {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
46
(** {2 Identifiers} *)
47 48

type ident = private {
Piotr Trojanek's avatar
Piotr Trojanek committed
49 50 51 52
  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 *)
53 54
}

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

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

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

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

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

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

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

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

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

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

92 93
(** Unique persistent names for pretty printing *)

94
type ident_printer
95

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

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

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

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

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

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

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

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

(** various character encoders *)
125 126 127 128 129

val char_to_alpha : char -> string
val char_to_lalpha : char -> string
val char_to_ualpha : char -> string
val char_to_alnum : char -> string
130
val char_to_lalnum : char -> string
131
val char_to_alnumus : char -> string
132
val char_to_lalnumus : char -> string
133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179


(** {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} *)

val model_label: label

val has_model_label: ident -> bool

val remove_model_labels : labels : Slab.t -> Slab.t
(** Returns a copy of labels without labels ["model"] and ["model_projected"]. *)

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. *)