ident.ml 7.59 KB
Newer Older
Andrei Paskevich's avatar
Andrei Paskevich committed
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
4
(*  Copyright 2010-2015   --   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

François Bobot's avatar
François Bobot committed
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
let is_model_trace_label label =
48
  Strings.has_prefix "model_trace:" label.lab_string
49

50
let get_model_trace_label ~labels =
51 52
  Slab.choose (Slab.filter is_model_trace_label labels)

53 54
let transform_model_trace_label labels trans_fun =
  try
55
    let trace_label = get_model_trace_label ~labels in
56 57 58 59 60 61 62
    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 =
63
    let splitted = Strings.bounded_split '@' lab_str 2 in
64 65 66 67 68 69 70 71 72 73
    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 =
74
  let trace_label = get_model_trace_label ~labels in
75
  let splitted1 = Strings.bounded_split ':' trace_label.lab_string 2 in
76 77 78
  match splitted1 with
  | [_; content] ->
    begin
79
      let splitted2 = Strings.bounded_split '@' content 2 in
80 81 82 83 84
      match splitted2 with
      | [el_name; _] -> el_name
      | [el_name] -> el_name
      | _ -> raise Not_found
    end;
85
  | [_] -> ""
86 87
  | _ -> assert false

88 89
let get_model_trace_string ~labels =
  let tl = get_model_trace_label ~labels in
90
  let splitted = Strings.bounded_split ':' tl.lab_string 2 in
91 92 93 94
  match splitted with
  | [_; t_str] -> t_str
  | _ -> ""

95

96 97 98
(** Identifiers *)

type ident = {
99
  id_string : string;               (* non-unique name *)
100
  id_label  : Slab.t;               (* identifier labels *)
101
  id_loc    : Loc.position option;  (* optional location *)
Andrei Paskevich's avatar
Andrei Paskevich committed
102
  id_tag    : Weakhtbl.tag;         (* unique magical tag *)
103 104
}

105
module Id = MakeMSHW (struct
106
  type t = ident
107 108 109 110 111 112
  let tag id = id.id_tag
end)

module Sid = Id.S
module Mid = Id.M
module Hid = Id.H
113
module Wid = Id.W
114

115 116 117 118 119
type preid = {
  pre_name  : string;
  pre_label : Slab.t;
  pre_loc   : Loc.position option;
}
120

121
let id_equal : ident -> ident -> bool = (==)
Andrei Paskevich's avatar
Andrei Paskevich committed
122
let id_hash id = Weakhtbl.tag_hash id.id_tag
Andrei Paskevich's avatar
Andrei Paskevich committed
123
let id_compare id1 id2 = Pervasives.compare (id_hash id1) (id_hash id2)
124

Andrei Paskevich's avatar
Andrei Paskevich committed
125
(* constructors *)
126

127 128 129 130 131 132
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);
}
133

134
let create_ident name labels loc = {
135 136 137
  pre_name  = name;
  pre_label = labels;
  pre_loc   = loc;
138 139
}

140
let id_fresh ?(label = Slab.empty) ?loc nm =
141
  create_ident nm label loc
Andrei Paskevich's avatar
Andrei Paskevich committed
142

143
let id_user ?(label = Slab.empty) nm loc =
144
  create_ident nm label (Some loc)
145

146 147 148
let id_lab label id =
  create_ident id.id_string label id.id_loc

149 150 151
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
152

153 154 155
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
156

157
let preid_name id = id.pre_name
158

159 160
(** Unique names for pretty printing *)

161
type ident_printer = {
162
  indices   : int Hstr.t;
Andrei Paskevich's avatar
Andrei Paskevich committed
163
  values    : string Hid.t;
164 165 166
  sanitizer : string -> string;
  blacklist : string list;
}
167 168

let find_unique indices name =
169
  let specname ind = name ^ string_of_int ind in
170
  let testname ind = Hstr.mem indices (specname ind) in
171 172 173 174 175 176
  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
177
  let name = try
178 179
    let ind = fetch (succ (Hstr.find indices name)) in
    Hstr.replace indices name ind;
180
    specname ind
181
  with Not_found -> name in
182
  Hstr.replace indices name 0;
183
  name
184

185 186
let reserve indices name = ignore (find_unique indices name)

187 188
let same x = x

189
let create_ident_printer ?(sanitizer = same) sl =
190
  let indices = Hstr.create 1997 in
191 192
  List.iter (reserve indices) sl;
  { indices   = indices;
Andrei Paskevich's avatar
Andrei Paskevich committed
193
    values    = Hid.create 1997;
194 195
    sanitizer = sanitizer;
    blacklist = sl }
196

197
let id_unique printer ?(sanitizer = same) id =
198
  try
Andrei Paskevich's avatar
Andrei Paskevich committed
199
    Hid.find printer.values id
200
  with Not_found ->
201
    let name = sanitizer (printer.sanitizer id.id_string) in
202
    let name = find_unique printer.indices name in
Andrei Paskevich's avatar
Andrei Paskevich committed
203
    Hid.replace printer.values id name;
204 205
    name

206
let string_unique printer s = find_unique printer.indices s
207

208
let forget_id printer id =
209
  try
Andrei Paskevich's avatar
Andrei Paskevich committed
210
    let name = Hid.find printer.values id in
211
    Hstr.remove printer.indices name;
Andrei Paskevich's avatar
Andrei Paskevich committed
212
    Hid.remove printer.values id
213 214
  with Not_found -> ()

215
let forget_all printer =
Andrei Paskevich's avatar
Andrei Paskevich committed
216
  Hid.clear printer.values;
217
  Hstr.clear printer.indices;
218
  List.iter (reserve printer.indices) printer.blacklist
219

220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237
(** 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
238
  | '9' -> "nn" | '\n' -> "br" |  _  -> "zz"
239 240 241 242 243 244 245

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

246 247 248
let char_to_lalnum c =
  match c with '0'..'9' -> String.make 1 c | _ -> char_to_lalpha c

249 250 251
let char_to_alnumus c =
  match c with '_' | ' ' -> "_" | _ -> char_to_alnum c

252 253 254
let char_to_lalnumus c =
  match c with '_' | ' ' -> "_" | _ -> char_to_lalnum c

255
let sanitizer' head rest last n =
256
  let lst = ref [] in
257 258 259 260
  let code i c = lst :=
    (if i = 0 then head
     else if i = String.length n - 1 then last
     else rest) c :: !lst in
261
  let n = if n = "" then "zilch" else n in
262 263 264 265
  String.iteri code n;
  String.concat "" (List.rev !lst)

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