removed superfluous use of Str.split

src/driver/whyconf.ml

@@ -200,7 +200,7 @@ let loadpath m =
 (*
     eprintf "[Info] loadpath set using WHY3LOADPATH='%s'@." d;
 *)
-    Str.split (Str.regexp ":") d
+    Strings.split ':' d
   with Not_found -> m.loadpath
 
 let timelimit m = m.timelimit
@@ -607,7 +607,7 @@ exception ProverAmbiguity of config * filter_prover * config_prover  Mprover.t
 exception ParseFilterProver of string
 
 let parse_filter_prover s =
-  let sl = Strings.rev_split s ',' in
+  let sl = Strings.rev_split ',' s in
   (* reverse order *)
   match sl with
   | [name] -> mk_filter_prover name

src/ide/gmain.ml

@@ -1588,7 +1588,7 @@ let run_factory = new GMenu.factory run_menu ~accel_group
 
 let eval const result =
   let msg =
-    match Str.split (Str.regexp "\\.") const with
+    match Strings.split '.' const with
       | [f;m;i] ->
         begin
           let e = env_session () in

src/printer/coq.ml

@@ -926,7 +926,7 @@ let print_task printer_args realize ?old fmt task =
       | [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 = Strings.rev_split s1 '.' in
+          let l = Strings.rev_split '.' s1 in
           List.rev (List.tl l), List.hd l in
         let th = Env.find_theory printer_args.env f id in
         Mid.add th.Theory.th_name (th, if s2 = "" then s1 else s2) mid

src/printer/isabelle.ml

@@ -429,7 +429,7 @@ let print_task printer_args realize fmt task =
       match args with
       | [Theory.MAstr s1; Theory.MAstr _] ->
         let f,id =
-          let l = Strings.rev_split s1 '.' in
+          let l = Strings.rev_split '.' s1 in
           List.rev (List.tl l), List.hd l in
         let th = Env.find_theory printer_args.env f id in
         Mid.add th.Theory.th_name (th, s1) mid

src/printer/pvs.ml

@@ -827,7 +827,7 @@ let print_task printer_args realize ?old fmt task =
       match args with
       | [Theory.MAstr s1; Theory.MAstr s2] ->
         let f,id =
-          let l = Strings.rev_split s1 '.' in
+          let l = Strings.rev_split '.' s1 in
           List.rev (List.tl l), List.hd l in
         let th = Env.find_theory printer_args.env f id in
         Mid.add th.Theory.th_name

src/session/session_scheduler.ml

@@ -928,7 +928,7 @@ let convert_unknown_prover =
   exception SyntaxError of string
 
   let parse_instr env max s =
-    match Strings.split s ' ' with
+    match Strings.split ' ' s with
       | [] -> raise (SyntaxError "unexpected empty instruction")
       | ["g";n] ->
         let g =

src/tools/why3contraption.ml

@@ -38,9 +38,8 @@ let add_opt_file x =
   Queue.push (Some x, tlist) opt_queue;
   opt_input := Some tlist
 
-let add_opt_theory =
-  let rdot = (Str.regexp "\\.") in fun x ->
-  let l = Str.split rdot x in
+let add_opt_theory x =
+  let l = Strings.split '.' x in
   let p, t = match List.rev l with
     | t::p -> List.rev p, t
     | _ -> assert false
@@ -71,7 +70,7 @@ let add_opt_goal x = match !opt_theory with
       eprintf "Option '-G'/'--goal' requires a theory.@.";
       exit 1
   | Some glist ->
-      let l = Str.split (Str.regexp "\\.") x in
+      let l = Strings.split '.' x in
       Queue.push (x, l) glist
 
 let add_opt_eval x = match !opt_theory_eval with
@@ -79,7 +78,7 @@ let add_opt_eval x = match !opt_theory_eval with
       eprintf "Option '--eval' requires a theory.@.";
       exit 1
   | Some elist ->
-      let l = Str.split (Str.regexp "\\.") x in
+      let l = Strings.split '.' x in
       Queue.push (x, l) elist
 
 let add_opt_exec x = Queue.push x opt_exec
@@ -563,7 +562,7 @@ let do_exec env fname cin exec =
     let mm, _thm = Mlw_main.read_channel lib [] fname cin in
     let do_exec x =
       let mid,name =
-        match Str.split (Str.regexp "\\.") x with
+        match Strings.split '.' x with
           | [m;i] -> m,i
           | _ ->
             Format.eprintf

src/tools/why3execute.ml

@@ -20,10 +20,9 @@ let usage_msg = sprintf
 let opt_file = ref None
 let opt_exec = Queue.create ()
 
-let add_opt =
-  let rdot = Str.regexp "\\." in fun x ->
+let add_opt x =
   if !opt_file = None then opt_file := Some x else
-  match Str.split rdot x with
+  match Strings.split '.' x with
   | [m;i] -> Queue.push (m,i) opt_exec
   | _ ->
     Format.eprintf "extra arguments must be of the form 'module.ident'@.";

src/tools/why3extract.ml

@@ -27,9 +27,8 @@ let add_opt_file x =
   Queue.push (Some x, tlist) opt_queue;
   opt_input := Some tlist
 
-let add_opt_theory =
-  let rdot = (Str.regexp "\\.") in fun x ->
-  let l = Str.split rdot x in
+let add_opt_theory x =
+  let l = Strings.split '.' x in
   let p, t = match List.rev l with
     | t::p -> List.rev p, t
     | _ -> assert false

src/tools/why3prove.ml

@@ -33,9 +33,8 @@ let add_opt_file x =
   Queue.push (Some x, tlist) opt_queue;
   opt_input := Some tlist
 
-let add_opt_theory =
-  let rdot = (Str.regexp "\\.") in fun x ->
-  let l = Str.split rdot x in
+let add_opt_theory x =
+  let l = Strings.split '.' x in
   let p, t = match List.rev l with
     | t::p -> List.rev p, t
     | _ -> assert false
@@ -64,7 +63,7 @@ let add_opt_goal x = match !opt_theory with
       eprintf "Option '-G'/'--goal' requires a theory.@.";
       exit 1
   | Some glist ->
-      let l = Str.split (Str.regexp "\\.") x in
+      let l = Strings.split '.' x in
       Queue.push (x, l) glist
 
 let add_opt_trans x = opt_trans := x::!opt_trans

src/tools/why3realize.ml

@@ -24,9 +24,8 @@ let add_opt_file _ =
     Use option -L if the containing files are not in the default loadpath.@.";
   exit 1
 
-let add_opt_theory =
-  let rdot = (Str.regexp "\\.") in fun x ->
-  let l = Str.split rdot x in
+let add_opt_theory x =
+  let l = Strings.split '.' x in
   let p, t = match List.rev l with
     | t::p -> List.rev p, t
     | _ -> assert false

src/util/strings.ml

@@ -11,7 +11,7 @@
 
 (* useful function on string *)
 
-let rev_split s c =
+let rev_split c s =
   let rec aux acc i =
     try
       let j = String.index_from s i c in
@@ -20,7 +20,7 @@ let rev_split s c =
       | Invalid_argument _ -> ""::acc in
   aux [] 0
 
-let split s c = List.rev (rev_split s c)
+let split c s = List.rev (rev_split c s)
 
 let ends_with s suf =
   let rec aux s suf suflen offset i =

src/util/strings.mli

@@ -11,9 +11,9 @@
 
 (** Useful functions on string *)
 
-val rev_split : string -> char -> string list
+val rev_split : char -> string -> string list
 
-val split : string -> char -> string list
+val split : char -> string -> string list
 
 val ends_with : string -> string -> bool
 (** test if a string ends with another *)

src/why3session/why3session_latex.ml

@@ -426,15 +426,14 @@ let element_latex_stat_file f n table dir e =
 
 let element_latex_stat files n table dir e =
   eprintf "Element %s@." e;
-  let re_dot = Str.regexp "\\." in
-  match Str.split re_dot e with
+  match Strings.split '.' e with
     | [] -> ()
     | f :: r ->
       let found = ref false in
       S.PHstr.iter
         (fun fname file ->
           let fname = Filename.basename fname in
-          let fname = List.hd (Str.split re_dot fname) in
+          let fname = List.hd (Strings.split '.' fname) in
           if fname = f then
             begin
               found := true;

src/why3session/why3session_lib.ml

@@ -87,7 +87,7 @@ let filter_prover = Stack.create ()
 
 let read_opt_prover s =
   try
-    let l = Strings.rev_split 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;