ident.ml 5.82 KB
Newer Older
Andrei Paskevich's avatar
Andrei Paskevich committed
1 2 3 4 5 6 7 8 9 10
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
(*  Copyright 2010-2012   --   INRIA - CNRS - Paris-Sud University  *)
(*                                                                  *)
(*  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.                           *)
(*                                                                  *)
(********************************************************************)
11

François Bobot's avatar
François Bobot committed
12
open Stdlib
13 14
open Util

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

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

22 23 24 25 26 27 28 29
module Lab = StructMake (struct
  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
30 31 32 33 34 35 36 37 38 39 40 41 42 43 44
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 = (==)

let lab_hash (lab : label) = lab.lab_tag
MARCHE Claude's avatar
MARCHE Claude committed
45

46 47 48
(** Identifiers *)

type ident = {
49
  id_string : string;               (* non-unique name *)
50
  id_label  : Slab.t;               (* identifier labels *)
51 52
  id_loc    : Loc.position option;  (* optional location *)
  id_tag    : Hashweak.tag;         (* unique magical tag *)
53 54
}

Andrei Paskevich's avatar
Andrei Paskevich committed
55
module Id = WeakStructMake (struct
56
  type t = ident
57 58 59 60 61 62
  let tag id = id.id_tag
end)

module Sid = Id.S
module Mid = Id.M
module Hid = Id.H
63
module Wid = Id.W
64

65 66
type preid = ident

67
let id_equal : ident -> ident -> bool = (==)
68

Andrei Paskevich's avatar
Andrei Paskevich committed
69
let id_hash id = Hashweak.tag_hash id.id_tag
70

Andrei Paskevich's avatar
Andrei Paskevich committed
71
(* constructors *)
72

Andrei Paskevich's avatar
Andrei Paskevich committed
73 74
let id_register = let r = ref 0 in fun id ->
  { id with id_tag = (incr r; Hashweak.create_tag !r) }
75

76
let create_ident name labels loc = {
77
  id_string = name;
Andrei Paskevich's avatar
Andrei Paskevich committed
78
  id_label  = labels;
79
  id_loc    = loc;
Andrei Paskevich's avatar
Andrei Paskevich committed
80
  id_tag    = Hashweak.dummy_tag;
81 82
}

83
let id_fresh ?(label = Slab.empty) ?loc nm =
84
  create_ident nm label loc
Andrei Paskevich's avatar
Andrei Paskevich committed
85

86
let id_user ?(label = Slab.empty) nm loc =
87
  create_ident nm label (Some loc)
88

89 90 91
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
92

93 94 95
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
96

97 98
let preid_name id = id.id_string

99 100
(** Unique names for pretty printing *)

101
type ident_printer = {
102
  indices   : int Hstr.t;
Andrei Paskevich's avatar
Andrei Paskevich committed
103
  values    : string Hid.t;
104 105 106
  sanitizer : string -> string;
  blacklist : string list;
}
107 108

let find_unique indices name =
109
  let specname ind = name ^ string_of_int ind in
110
  let testname ind = Hstr.mem indices (specname ind) in
111 112 113 114 115 116
  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
117
  let name = try
118 119
    let ind = fetch (succ (Hstr.find indices name)) in
    Hstr.replace indices name ind;
120
    specname ind
121
  with Not_found -> name in
122
  Hstr.replace indices name 0;
123
  name
124

125 126
let reserve indices name = ignore (find_unique indices name)

127 128
let same x = x

129
let create_ident_printer ?(sanitizer = same) sl =
130
  let indices = Hstr.create 1997 in
131 132
  List.iter (reserve indices) sl;
  { indices   = indices;
Andrei Paskevich's avatar
Andrei Paskevich committed
133
    values    = Hid.create 1997;
134 135
    sanitizer = sanitizer;
    blacklist = sl }
136

137
let id_unique printer ?(sanitizer = same) id =
138
  try
Andrei Paskevich's avatar
Andrei Paskevich committed
139
    Hid.find printer.values id
140
  with Not_found ->
141
    let name = sanitizer (printer.sanitizer id.id_string) in
142
    let name = find_unique printer.indices name in
Andrei Paskevich's avatar
Andrei Paskevich committed
143
    Hid.replace printer.values id name;
144 145
    name

146
let string_unique printer s = find_unique printer.indices s
147

148
let forget_id printer id =
149
  try
Andrei Paskevich's avatar
Andrei Paskevich committed
150
    let name = Hid.find printer.values id in
151
    Hstr.remove printer.indices name;
Andrei Paskevich's avatar
Andrei Paskevich committed
152
    Hid.remove printer.values id
153 154
  with Not_found -> ()

155
let forget_all printer =
Andrei Paskevich's avatar
Andrei Paskevich committed
156
  Hid.clear printer.values;
157
  Hstr.clear printer.indices;
158
  List.iter (reserve printer.indices) printer.blacklist
159

160 161
(** Sanitizers *)

162
let unsanitizable = Debug.register_info_flag "unsanitizable"
163
  ~desc:"About@ the@ sanitazing@ during@ the@ pretty-printing."
164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180

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"
181 182 183 184
  | '9' -> "nn" | '\n' -> "br"
  | _ ->
    Debug.dprintf unsanitizable "Unsanitizable : '%c' can't be sanitized@." c;
    "zz"
185 186 187 188 189 190 191

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

192 193 194
let char_to_lalnum c =
  match c with '0'..'9' -> String.make 1 c | _ -> char_to_lalpha c

195 196 197
let char_to_alnumus c =
  match c with '_' | ' ' -> "_" | _ -> char_to_alnum c

198 199 200
let char_to_lalnumus c =
  match c with '_' | ' ' -> "_" | _ -> char_to_lalnum c

201 202 203 204 205 206 207 208
let sanitizer head rest n =
  let lst = ref [] in
  let code c = lst := rest c :: !lst in
  let n = if n = "" then "zilch" else n in
  String.iter code n;
  let rst = List.tl (List.rev !lst) in
  let cs = head (String.get n 0) :: rst in
  String.concat "" cs