ident.ml 7.79 KB
Newer Older
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
4
(*  Copyright 2010-2015   --   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

12
open Stdlib
13

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

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

21
module Lab = MakeMSH (struct
22 23 24 25 26 27 28
  type t = label
  let tag lab = lab.lab_tag
end)

module Slab = Lab.S
module Mlab = Lab.M

Andrei Paskevich's avatar
Andrei Paskevich committed
29 30 31 32 33 34 35 36 37 38 39 40 41
module Hslab = Hashcons.Make (struct
  type t = label
  let equal lab1 lab2 = lab1.lab_string = lab2.lab_string
  let hash lab = Hashtbl.hash lab.lab_string
  let tag n lab = { lab with lab_tag = n }
end)

let create_label s = Hslab.hashcons {
  lab_string = s;
  lab_tag    = -1
}

let lab_equal : label -> label -> bool = (==)
Andrei Paskevich's avatar
Andrei Paskevich committed
42 43
let lab_hash lab = lab.lab_tag
let lab_compare l1 l2 = Pervasives.compare l1.lab_tag l2.lab_tag
MARCHE Claude's avatar
MARCHE Claude committed
44

45 46
(* functions for working with counterexample model labels *)

47 48 49 50 51 52
let model_proj_label = create_label "model_projected"
let model_label = create_label "model"

let remove_model_labels ~labels =
  Slab.filter (fun l -> (l <> model_label) && (l <> model_proj_label) ) labels

53
let is_model_trace_label label =
54
  Strings.has_prefix "model_trace:" label.lab_string
55

56
let get_model_trace_label ~labels =
57 58
  Slab.choose (Slab.filter is_model_trace_label labels)

59 60
let transform_model_trace_label labels trans_fun =
  try
61
    let trace_label = get_model_trace_label ~labels in
62 63 64 65 66 67 68
    let labels_without_trace = Slab.remove trace_label labels in
    let new_trace_label = create_label (trans_fun trace_label.lab_string) in
    Slab.add new_trace_label labels_without_trace
  with Not_found -> labels

let append_to_model_element_name ~labels ~to_append =
  let trans lab_str =
69
    let splitted = Strings.bounded_split '@' lab_str 2 in
70 71 72 73 74 75 76 77 78 79
    match splitted with
    | [before; after] -> before ^ to_append ^ "@" ^ after
    | _ -> lab_str^to_append in
  transform_model_trace_label labels trans

let append_to_model_trace_label ~labels ~to_append =
    let trans lab_str = lab_str ^ to_append in
    transform_model_trace_label labels trans

let get_model_element_name ~labels =
80
  let trace_label = get_model_trace_label ~labels in
81
  let splitted1 = Strings.bounded_split ':' trace_label.lab_string 2 in
82 83 84
  match splitted1 with
  | [_; content] ->
    begin
85
      let splitted2 = Strings.bounded_split '@' content 2 in
86 87 88 89 90
      match splitted2 with
      | [el_name; _] -> el_name
      | [el_name] -> el_name
      | _ -> raise Not_found
    end;
91
  | [_] -> ""
92 93
  | _ -> assert false

94 95
let get_model_trace_string ~labels =
  let tl = get_model_trace_label ~labels in
96
  let splitted = Strings.bounded_split ':' tl.lab_string 2 in
97 98 99 100
  match splitted with
  | [_; t_str] -> t_str
  | _ -> ""

101

102 103 104
(** Identifiers *)

type ident = {
105
  id_string : string;               (* non-unique name *)
106
  id_label  : Slab.t;               (* identifier labels *)
107
  id_loc    : Loc.position option;  (* optional location *)
108
  id_tag    : Weakhtbl.tag;         (* unique magical tag *)
109 110
}

111
module Id = MakeMSHW (struct
112
  type t = ident
113 114 115 116 117 118
  let tag id = id.id_tag
end)

module Sid = Id.S
module Mid = Id.M
module Hid = Id.H
119
module Wid = Id.W
120

121 122 123 124 125
type preid = {
  pre_name  : string;
  pre_label : Slab.t;
  pre_loc   : Loc.position option;
}
126

127
let id_equal : ident -> ident -> bool = (==)
128
let id_hash id = Weakhtbl.tag_hash id.id_tag
Andrei Paskevich's avatar
Andrei Paskevich committed
129
let id_compare id1 id2 = Pervasives.compare (id_hash id1) (id_hash id2)
130

Andrei Paskevich's avatar
Andrei Paskevich committed
131
(* constructors *)
132

133 134 135 136 137 138
let id_register = let r = ref 0 in fun id -> {
  id_string = id.pre_name;
  id_label  = id.pre_label;
  id_loc    = id.pre_loc;
  id_tag    = (incr r; Weakhtbl.create_tag !r);
}
139

140
let create_ident name labels loc = {
141 142 143
  pre_name  = name;
  pre_label = labels;
  pre_loc   = loc;
144 145
}

146
let id_fresh ?(label = Slab.empty) ?loc nm =
147
  create_ident nm label loc
Andrei Paskevich's avatar
Andrei Paskevich committed
148

149
let id_user ?(label = Slab.empty) nm loc =
150
  create_ident nm label (Some loc)
151

152 153 154
let id_lab label id =
  create_ident id.id_string label id.id_loc

155 156 157
let id_clone ?(label = Slab.empty) id =
  let ll = Slab.union label id.id_label in
  create_ident id.id_string ll id.id_loc
158

159 160 161
let id_derive ?(label = Slab.empty) nm id =
  let ll = Slab.union label id.id_label in
  create_ident nm ll id.id_loc
Francois Bobot's avatar
Francois Bobot committed
162

163
let preid_name id = id.pre_name
164

165 166
(** Unique names for pretty printing *)

167
type ident_printer = {
168
  indices   : int Hstr.t;
Andrei Paskevich's avatar
Andrei Paskevich committed
169
  values    : string Hid.t;
170 171 172
  sanitizer : string -> string;
  blacklist : string list;
}
173 174

let find_unique indices name =
175
  let specname ind = name ^ string_of_int ind in
176
  let testname ind = Hstr.mem indices (specname ind) in
177 178 179 180 181 182
  let rec advance ind =
    if testname ind then advance (succ ind) else ind in
  let rec retreat ind =
    if ind = 1 || testname (pred ind) then ind else retreat (pred ind) in
  let fetch ind =
    if testname ind then advance (succ ind) else retreat ind in
183
  let name = try
184 185
    let ind = fetch (succ (Hstr.find indices name)) in
    Hstr.replace indices name ind;
186
    specname ind
187
  with Not_found -> name in
188
  Hstr.replace indices name 0;
189
  name
190

191 192
let reserve indices name = ignore (find_unique indices name)

193 194
let same x = x

195
let create_ident_printer ?(sanitizer = same) sl =
196
  let indices = Hstr.create 1997 in
197 198
  List.iter (reserve indices) sl;
  { indices   = indices;
Andrei Paskevich's avatar
Andrei Paskevich committed
199
    values    = Hid.create 1997;
200 201
    sanitizer = sanitizer;
    blacklist = sl }
202

203
let id_unique printer ?(sanitizer = same) id =
204
  try
Andrei Paskevich's avatar
Andrei Paskevich committed
205
    Hid.find printer.values id
206
  with Not_found ->
207
    let name = sanitizer (printer.sanitizer id.id_string) in
208
    let name = find_unique printer.indices name in
Andrei Paskevich's avatar
Andrei Paskevich committed
209
    Hid.replace printer.values id name;
210 211
    name

212
let string_unique printer s = find_unique printer.indices s
213

214
let forget_id printer id =
215
  try
Andrei Paskevich's avatar
Andrei Paskevich committed
216
    let name = Hid.find printer.values id in
217
    Hstr.remove printer.indices name;
Andrei Paskevich's avatar
Andrei Paskevich committed
218
    Hid.remove printer.values id
219 220
  with Not_found -> ()

221
let forget_all printer =
Andrei Paskevich's avatar
Andrei Paskevich committed
222
  Hid.clear printer.values;
223
  Hstr.clear printer.indices;
224
  List.iter (reserve printer.indices) printer.blacklist
225

226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243
(** Sanitizers *)

let char_to_alpha c = match c with
  | 'a'..'z' | 'A'..'Z' -> String.make 1 c
  | ' ' -> "sp" | '_'  -> "us" | '#' -> "sh"
  | '`' -> "bq" | '~'  -> "tl" | '!' -> "ex"
  | '@' -> "at" | '$'  -> "dl" | '%' -> "pc"
  | '^' -> "cf" | '&'  -> "et" | '*' -> "as"
  | '(' -> "lp" | ')'  -> "rp" | '-' -> "mn"
  | '+' -> "pl" | '='  -> "eq" | '[' -> "lb"
  | ']' -> "rb" | '{'  -> "lc" | '}' -> "rc"
  | ':' -> "cl" | '\'' -> "qt" | '"' -> "dq"
  | '<' -> "ls" | '>'  -> "gt" | '/' -> "sl"
  | '?' -> "qu" | '\\' -> "bs" | '|' -> "br"
  | ';' -> "sc" | ','  -> "cm" | '.' -> "dt"
  | '0' -> "zr" | '1'  -> "un" | '2' -> "du"
  | '3' -> "tr" | '4'  -> "qr" | '5' -> "qn"
  | '6' -> "sx" | '7'  -> "st" | '8' -> "oc"
Andrei Paskevich's avatar
Andrei Paskevich committed
244
  | '9' -> "nn" | '\n' -> "br" |  _  -> "zz"
245 246 247 248 249 250 251

let char_to_lalpha c = String.uncapitalize (char_to_alpha c)
let char_to_ualpha c = String.capitalize (char_to_alpha c)

let char_to_alnum c =
  match c with '0'..'9' -> String.make 1 c | _ -> char_to_alpha c

252 253 254
let char_to_lalnum c =
  match c with '0'..'9' -> String.make 1 c | _ -> char_to_lalpha c

255 256 257
let char_to_alnumus c =
  match c with '_' | ' ' -> "_" | _ -> char_to_alnum c

258 259 260
let char_to_lalnumus c =
  match c with '_' | ' ' -> "_" | _ -> char_to_lalnum c

261
let sanitizer' head rest last n =
262
  let lst = ref [] in
263 264 265 266
  let code i c = lst :=
    (if i = 0 then head
     else if i = String.length n - 1 then last
     else rest) c :: !lst in
267
  let n = if n = "" then "zilch" else n in
268 269 270 271
  String.iteri code n;
  String.concat "" (List.rev !lst)

let sanitizer head rest n = sanitizer' head rest rest n