move string utilities from Util to Strings

Makefile.in

@@ -108,7 +108,7 @@ LIBGENERATED = src/util/config.ml src/util/rc.ml src/parser/lexer.ml \
 	       src/driver/driver_parser.mli src/driver/driver_parser.ml \
 	       src/driver/driver_lexer.ml src/session/xml.ml
 
-LIB_UTIL = config opt lists stdlib exn_printer pp debug loc print_tree \
+LIB_UTIL = config opt lists strings stdlib exn_printer pp debug loc print_tree \
 	   cmdline hashweak hashcons util warning sysutil rc plugin
 
 LIB_CORE = ident ty term pattern decl theory task pretty env trans printer

src/driver/autodetection.ml

@@ -466,10 +466,9 @@ let add_prover_binary config id path =
     (* Is a prover with this name and version already in config? *)
     let prover_id =
       if not (Mprover.mem p.prover provers) then p.prover else
-        let alt = get_altern id path in
-        let prover_id = { p.prover with
-          Wc.prover_altern =
-            Util.concat_non_empty " " [p.prover.Wc.prover_altern;alt] } in
+        let alt = match p.prover.Wc.prover_altern, get_altern id path with
+          | "", s -> s | s, "" -> s | s1, s2 -> s1 ^ " " ^ s2 in
+        let prover_id = { p.prover with Wc.prover_altern = alt } in
         find_prover_altern provers prover_id in
     let p = {p with prover = prover_id} in
     add_prover_with_uniq_id p provers in

src/driver/whyconf.ml

@@ -528,7 +528,7 @@ exception ProverAmbiguity of config * filter_prover * config_prover  Mprover.t
 exception ParseFilterProver of string
 
 let parse_filter_prover s =
-  let sl = Util.split_string_rev s ',' in
+  let sl = Strings.rev_split s ',' in
   (* reverse order *)
   match sl with
   | [name] -> mk_filter_prover name

src/printer/coq.ml

@@ -841,7 +841,9 @@ let print_task env pr thpr _blacklist realize ?old fmt task =
       match args with
       | [Theory.MAstr s1; Theory.MAstr s2] ->
         (* TODO: do not split string; in fact, do not even use a string argument *)
-        let f,id = let l = split_string_rev s1 '.' in List.rev (List.tl l),List.hd l in
+        let f,id =
+          let l = Strings.rev_split s1 '.' in
+          List.rev (List.tl l), List.hd l in
         let th = Env.find_theory env f id in
         Mid.add th.Theory.th_name (th, if s2 = "" then s1 else s2) mid
       | _ -> assert false

src/printer/pvs.ml

@@ -825,7 +825,8 @@ let print_task env pr thpr _blacklist realize ?old fmt task =
       match args with
       | [Theory.MAstr s1; Theory.MAstr s2] ->
         let f,id =
-          let l = split_string_rev s1 '.' in List.rev (List.tl l),List.hd l in
+          let l = Strings.rev_split s1 '.' in
+          List.rev (List.tl l), List.hd l in
         let th = Env.find_theory env f id in
         Mid.add th.Theory.th_name
           (th, (f, if s2 = "" then String.concat "." f else s2)) mid

src/util/strings.ml

+(********************************************************************)
+(*                                                                  *)
+(*  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.                           *)
+(*                                                                  *)
+(********************************************************************)
+
+(* useful function on string *)
+
+let rev_split s c =
+  let rec aux acc i =
+    try
+      let j = String.index_from s i c in
+      aux ((String.sub s i (j-i))::acc) (j + 1)
+    with Not_found -> (String.sub s i (String.length s - i))::acc
+      | Invalid_argument _ -> ""::acc in
+  aux [] 0
+
+let ends_with s suf =
+  let rec aux s suf suflen offset i =
+    i >= suflen || (s.[i + offset] = suf.[i]
+                   && aux s suf suflen offset (i+1)) in
+  let slen = String.length s in
+  let suflen = String.length suf in
+  slen >= suflen && aux s suf suflen (slen - suflen) 0
+
+let pad_right c s i =
+  let sl = String.length s in
+  if sl < i then
+    let p = String.create i in
+    String.blit s 0 p 0 sl;
+    String.fill p sl (i-sl) c;
+    p
+  else if sl > i
+  then String.sub s 0 i
+  else s
+

src/util/strings.mli

+(********************************************************************)
+(*                                                                  *)
+(*  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.                           *)
+(*                                                                  *)
+(********************************************************************)
+
+(* useful function on string *)
+
+val rev_split : string -> char -> string list
+
+val ends_with : string -> string -> bool
+(** test if a string ends with another *)
+
+val pad_right : char -> string -> int -> string
+(** chop or pad the given string on the right up to the given length *)
+

src/util/util.ml

@@ -45,46 +45,6 @@ let any_fn pr _ t = pr t && raise FoldSkip
 let ttrue _ = true
 let ffalse _ = false
 
-(* useful function on string *)
-let split_string_rev s c =
-  let rec aux acc i =
-    try
-      let j = String.index_from s i c in
-      aux ((String.sub s i (j-i))::acc) (j + 1)
-    with Not_found -> (String.sub s i (String.length s - i))::acc
-      | Invalid_argument _ -> ""::acc in
-  aux [] 0
-
-let ends_with s suf =
-  let rec aux s suf suflen offset i =
-    i >= suflen || (s.[i + offset] = suf.[i]
-                   && aux s suf suflen offset (i+1)) in
-  let slen = String.length s in
-  let suflen = String.length suf in
-  slen >= suflen && aux s suf suflen (slen - suflen) 0
-
-let padd_string c s i =
-  let sl = String.length s in
-  if sl < i then
-    let p = String.create i in
-    String.blit s 0 p 0 sl;
-    String.fill p sl (i-sl) c;
-    p
-  else if sl > i
-  then String.sub s 0 i
-  else s
-
-(** useful function on char *)
-let is_uppercase c = 'A' <= c && c <= 'Z'
-
-let concat_non_empty sep l =
-  String.concat sep (List.filter (fun s -> s <> "") l)
-
-(** useful function on char *)
-let count n =
-  let r = ref (n-1) in
-  fun _ -> incr r; !r
-
 (* Set and Map on ints and strings *)
 
 module Int  = struct

src/util/util.mli

@@ -48,24 +48,6 @@ val ffalse : 'a -> bool
 val ttrue : 'a -> bool
 (** [ttrue] constant function [true] *)
 
-(* useful function on string *)
-val split_string_rev : string -> char -> string list
-
-val ends_with : string -> string -> bool
-(** test if a string ends with another *)
-
-val padd_string : char -> string -> int -> string
-(** extract or padd the given string in order to have the given length *)
-
-val concat_non_empty : string -> string list -> string
-
-(* useful function on char *)
-val is_uppercase : char -> bool
-
-(* useful function on int *)
-val count : int -> ('a -> int)
-(** return the consecutie number from the first given *)
-
 (* Set and Map on ints and strings *)
 
 module Mint : Map.S with type key = int

src/why3bench/benchrc.ml

@@ -56,7 +56,7 @@ let read_tools absf wc map (name,section) =
   (* use *)
   let use = get_stringl ~default:[] section "use" in
   let load_use s =
-    let file,th = match Util.split_string_rev s '.' with
+    let file,th = match Strings.rev_split s '.' with
       | [] | [_] -> eprintf "Bad theory qualifier %s" s; exit 1
       | a::l -> List.rev l,a in
     Env.find_theory env file th,

src/why3session/why3session.ml

@@ -33,7 +33,7 @@ let print_usage () =
     exec_name
     (Pp.print_iter1 Array.iter Pp.newline
        (fun fmt e -> fprintf fmt "%s   @[<hov>%s@]"
-         (Util.padd_string ' ' e.cmd_name maxl) e.cmd_desc)) cmds;
+         (Strings.pad_right ' ' e.cmd_name maxl) e.cmd_desc)) cmds;
   Arg.usage (Arg.align Why3session_lib.common_options) "common options:";
   eprintf "@\nspecific command options: %s <command> -help@." exec_name;
   exit 1

src/why3session/why3session_html.ml

@@ -359,7 +359,7 @@ struct
     let basename = Filename.basename edited in
     try
       let suff,(cmd,suff_out) =
-        List.find (fun (s,_) -> ends_with basename s) !opt_pp in
+        List.find (fun (s,_) -> Strings.ends_with basename s) !opt_pp in
       let base =
         String.sub basename 0 (String.length basename - String.length suff) in
       let base_dst = (base^suff_out) in

src/why3session/why3session_lib.ml

@@ -94,7 +94,7 @@ let filter_prover = Stack.create ()
 
 let read_opt_prover s =
   try
-    let l = Util.split_string_rev s ',' in
+    let l = Strings.rev_split s ',' in
     match l with
     | [altern;version;name] when List.for_all (fun s -> s.[0] <> '^') l ->
       Prover {Whyconf.prover_name = name;