src/utilities/stringTools.ml

   1
   2 (** FIXME: document here *)
   3
   4 type t = string
   5
   6 let compare = String.compare
   7
   8
   9 module Set = struct
  10   include Set.Make (String)
  11   let of_list l =
  12     let f res e = add e res in
  13     List.fold_left f empty l
  14   let unionl l = List.fold_left union empty l
  15 end
  16
  17
  18 module Map = Map.Make (String)
  19
  20
  21 module Gen = struct
  22
  23   type universe = { prefix : string ; mutable next : int }
  24
  25   let added_suffix = "_"
  26
  27   let is_prefix prefix s =
  28     let l = String.length prefix in
  29     (String.length s >= l) && (String.sub s 0 l = prefix)
  30
  31   let has_prefix set prefix =
  32     let f s b = b || (is_prefix prefix s) in
  33     Set.fold f set false
  34
  35   let fresh_prefix set prefix =
  36     let rec aux prefix =
  37       if has_prefix set prefix then aux (prefix ^ added_suffix)
  38       else prefix in
  39     aux prefix
  40
  41
  42   let new_universe s = { prefix = s ; next = 0 }
  43
  44   let fresh u =
  45     let s = u.prefix ^ (string_of_int u.next) in
  46     u.next <- u.next + 1 ;
  47     s
  48
  49 end
  50
  51 let make_unique set =
  52   let set_ref = ref set in
  53   let unique s =
  54     let res = Gen.fresh_prefix !set_ref s in
  55     set_ref := Set.add res !set_ref ;
  56     res in
  57   unique
  58
  59 let make_fresh set prefix =
  60   let fresh_prefix = Gen.fresh_prefix set prefix in
  61   let universe = Gen.new_universe fresh_prefix in
  62   (fun () -> Gen.fresh universe)
  63
  64 let dummy = ""