fix compilation with OCaml 4.12.0

src/ctrs/src/ctrs.mli

@@ -252,7 +252,7 @@ module type SORTDECLARATION = sig
   (** [to_string x] returns a string that represents [x]. *)
 end
 
-(** This module deals with sort declarations (combining input- and output sorts. *)
+(** This module deals with sort declarations (combining input- and output sorts). *)
 module Sortdeclaration : SORTDECLARATION with type sort = Sort.t
 
 (** {2 Module Specialdeclaration} *)
@@ -341,7 +341,7 @@ module type SPECIALDECLARATION = sig
   (** [to_string x] returns a string that represents [x]. *)
 end
 
-(** This module deals with polymorphic declarations, and declaratios with
+(** This module deals with polymorphic declarations, and declarations with
 variable arity.  Symbols with such a declaration should always be used in
 a combination with their currently active sort declaration. *)
 module Specialdeclaration : SPECIALDECLARATION

src/io/src/cleaner.ml

@@ -830,7 +830,7 @@ let group_symbols alf =
   let arrayable = Alphabet.arraysorts_of alf in
   let arrdata sort =
     let arrsort = Alphabet.array_sort sort alf in
-    let sortstring = String.uppercase (Sort.to_string sort) in
+    let sortstring = String.uppercase_ascii (Sort.to_string sort) in
     (arrsort, "  !ARRAY!" ^ sortstring ^ " : " ^ (Sort.to_string arrsort))
   in
   let extra_sorts = List.map arrdata arrayable in

src/smt/src/internalsolver.ml

@@ -226,7 +226,7 @@ let rec parse_iexp tr a e isparam = function
       try List.assoc fname tr
       with Not_found -> fname
     ) in
-    let name = String.lowercase name in
+    let name = String.lowercase_ascii name in
     (* recursion data *)
     let pargs = List.map (parse_exp tr a e isparam) args in
     let all_exps kind maker =
@@ -287,7 +287,7 @@ and parse_aexp tr a e isparam = function
       try List.assoc fname tr
       with Not_found -> fname
     ) in
-    let name = String.lowercase name in
+    let name = String.lowercase_ascii name in
     (* recursion data *)
     let pargs = List.map (parse_exp tr a e isparam) args in
     (* parse values *)
@@ -351,7 +351,7 @@ and parse_formula tr a e isparam = function
       try List.assoc fname tr
       with Not_found -> fname
     ) in
-    let name = String.lowercase name in
+    let name = String.lowercase_ascii name in
     (* recursion data *)
     let pargs = List.map (parse_exp tr a e isparam) args in
     let all_bools kind maker =
@@ -1793,7 +1793,7 @@ let rec translate_int ren tra a e isparam = function
       try List.assoc name ren
       with Not_found -> name
     ) in
-    let name = String.lowercase name in
+    let name = String.lowercase_ascii name in
     let newargs =
       if name = "ite" then []
       else List.map (translate_int ren tra a e isparam) args

src/util/src/argx.ml

@@ -43,6 +43,7 @@ type anon_fun = string -> unit
   | Tuple of spec list
   | Symbol of string list * (string -> unit)
   | Rest of (string -> unit)
+  | Rest_all of (string list -> unit)
   | Expand of (string -> string array)
  type usage_msg = string
 

src/util/src/isomorphism.ml

@@ -25,7 +25,6 @@ module type DOMAIN = sig
  type t
 
  val compare : t -> t -> int
- val copy : t -> t
  val fprintf : Format.formatter -> t -> unit
  val hash : t -> int
 end
@@ -83,9 +82,9 @@ module Make (D : DOMAIN) (R : RANGE) = struct
  let clear t = {domain = DH.clear_ t.domain; range = RH.clear_ t.range};;
 
  let copy t =
-  let add d r = DH.add_ (D.copy d) (R.copy r) in
+  let add d r = DH.add_ d r in
   let domain = DH.fold add t.domain (DH.create (DH.length t.domain)) in
-  let add r d = RH.add_ (R.copy r) (D.copy d) in
+  let add r d = RH.add_ r d in
   let range = RH.fold add t.range (RH.create (RH.length t.range)) in
   {domain = domain; range = range}
  ;;

src/util/src/listx.ml

@@ -57,7 +57,7 @@ module Set = struct
   else Node (l,v,r,(if hl >= hr then hl + 1 else hr + 1))
  ;;
 
- let rec add ?(c = compare) x = function
+ let rec add ?(c = Stdlib.compare) x = function
   | Empty -> Node (Empty,x,Empty,1)
   | Node (l,v,r,_) as t ->
    let n = c x v in
@@ -66,7 +66,7 @@ module Set = struct
    else bal l v (add ~c:c x r)
  ;;
 
- let rec mem ?(c = compare) x = function
+ let rec mem ?(c = Stdlib.compare) x = function
   | Empty -> false
   | Node (l,v,r,_) ->
    let n = c x v in n = 0 || mem ~c:c x (if n < 0 then l else r)
@@ -189,20 +189,20 @@ let drop_while p = snd <.> spani (const p);;
 let take n = fst <.> split_at n;;
 let take_while p = fst <.> spani (const p);;
 
-let rec group ?(c = compare) xs =
+let rec group ?(c = Stdlib.compare) xs =
  let f (x,xs,ys) y = if c x y = 0 then (x,y::xs,ys) else (y,[y],xs::ys) in
  if xs = [] then []
  else let (_,xs,ys) = foldl f (hd xs,[],[]) xs in rev (xs :: ys)
 ;;
 
-let group_fully ?(c = compare) xs = group ~c:c (sort c xs);;
+let group_fully ?(c = Stdlib.compare) xs = group ~c:c (sort c xs);;
 
 (* Constructors and Destructors *)
 let insert p e xs = let (hd,tl) = rev_split_at p xs in rev_append hd (e::tl);;
-let replace ?(c = compare) x y = map_tl (fun z -> if c x z = 0 then y else z);;
+let replace ?(c = Stdlib.compare) x y = map_tl (fun z -> if c x z = 0 then y else z);;
 let rev_concat xs = foldl (flip rev_append) [] xs;;
 let singleton x = [x];;
-let remove_all ?(c = compare) x = filter (fun y -> c x y <> 0);;
+let remove_all ?(c = Stdlib.compare) x = filter (fun y -> c x y <> 0);;
 
 let collapse ?(n = -1) xs = 
  let chunk_size = if n < 1 then 1 else (length xs + n - 1)/n in
@@ -215,15 +215,15 @@ let collapse ?(n = -1) xs =
  if chunk_size < 1 then [] else chunks xs
 ;;
 
-let remove ?(c = compare) x xs =
+let remove ?(c = Stdlib.compare) x xs =
  let rec remove acc = function
   | [] -> acc
   | y :: xs -> if c x y = 0 then rev_append xs acc else remove (y :: acc) xs
  in
  rev (remove [] xs)
 ;;
 
-let rec remove_equal ?(c = compare) xs ys = match (xs, ys) with
+let rec remove_equal ?(c = Stdlib.compare) xs ys = match (xs, ys) with
  | x :: us, y :: vs -> if c x y = 0 then remove_equal ~c:c us vs else (xs, ys)
  | _, _ -> (xs, ys)
 ;;
@@ -238,7 +238,7 @@ let for_alli p =
 ;;
 
 let existsi p = not <.> for_alli (fun i x -> not (p i x));;
-let mem ?(c = compare) x = exists (fun y -> c x y = 0);;
+let mem ?(c = Stdlib.compare) x = exists (fun y -> c x y = 0);;
 
 (* Search Functions *)
 let filteri p =
@@ -286,16 +286,16 @@ let rev_unzip xs = rev_unzip_with id xs;;
 let unzip xs = unzip_with id xs;;
 
 (* Assoctiation Lists *)
-let assoc ?(c = compare) x = snd <.> find (fun (y,_) -> c x y = 0);;
-let mem_assoc ?(c = compare) x = exists (fun (y,_) -> c x y = 0);;
+let assoc ?(c = Stdlib.compare) x = snd <.> find (fun (y,_) -> c x y = 0);;
+let mem_assoc ?(c = Stdlib.compare) x = exists (fun (y,_) -> c x y = 0);;
 
-let rec remove_assoc ?(c = compare) x = function
+let rec remove_assoc ?(c = Stdlib.compare) x = function
  | [] -> []
  | (y, z) :: xs -> if c x y = 0 then xs else (y, z) :: remove_assoc ~c:c x xs
 ;;
 
 (* Lists as Sets *)
-let union ?(c = compare) xs ys =
+let union ?(c = Stdlib.compare) xs ys =
  let (xs,ys) = foldl (fun (xs,ys) x -> (x::xs,remove_all x ys)) ([],ys) xs in
  rev (rev_append ys xs)
 ;;
@@ -319,27 +319,27 @@ let rev_times xs = flat_times (flip cons) [] xs;;
 let times xs = map_tl rev (rev_times xs);;
 let product xs = flat_product P.make xs;;
 let square xs = product xs xs;;
-let diff ?(c = compare) xs ys = filter (fun x -> not (mem ~c:c x ys)) xs;;
-let is_subset ?(c = compare) xs ys = for_all (flip (mem ~c:c) ys) xs;;
-let is_supset ?(c = compare) = flip (is_subset ~c:c);;
-let equal ?(c = compare) xs ys = is_subset ~c:c xs ys && is_subset ~c:c ys xs;;
-let intersect ?(c = compare) xs ys = filter (flip (mem ~c:c) ys) xs;;
+let diff ?(c = Stdlib.compare) xs ys = filter (fun x -> not (mem ~c:c x ys)) xs;;
+let is_subset ?(c = Stdlib.compare) xs ys = for_all (flip (mem ~c:c) ys) xs;;
+let is_supset ?(c = Stdlib.compare) = flip (is_subset ~c:c);;
+let equal ?(c = Stdlib.compare) xs ys = is_subset ~c:c xs ys && is_subset ~c:c ys xs;;
+let intersect ?(c = Stdlib.compare) xs ys = filter (flip (mem ~c:c) ys) xs;;
 
-let is_proper_subset ?(c = compare) xs ys =
+let is_proper_subset ?(c = Stdlib.compare) xs ys =
  is_subset ~c:c xs ys && not (is_subset ~c:c ys xs)
 ;;
 
-let unique ?(c = compare) xs =
+let unique ?(c = Stdlib.compare) xs =
  let mem = Set.mem ~c:c and add = Set.add ~c:c in
  let add (xs,s) x = if mem x s then (xs,s) else (x::xs,add x s) in
  rev (fst (foldl add ([],Set.empty) xs))
 ;;
 
-let sort_unique ?(c = compare) xs =
+let sort_unique ?(c = Stdlib.compare) xs =
   let rec uniquefy = function
     | [] | [_] as lst -> lst
     | x :: y :: lst ->
-      if compare x y = 0 then uniquefy (y :: lst)
+      if c x y = 0 then uniquefy (y :: lst)
       else x :: uniquefy (y :: lst)
   in
   uniquefy (sort c xs)
@@ -399,15 +399,15 @@ let rec implode f d = function
 (* Properties *)
 let is_empty xs = xs = [];;
 let is_singleton = function [_] -> true | _ -> false;;
-let is_prefix ?(c = compare) xs ys = fst (remove_equal ~c:c xs ys) = [];;
-let is_suffix ?(c = compare) xs ys = is_prefix ~c:c (rev xs) (rev ys);;
+let is_prefix ?(c = Stdlib.compare) xs ys = fst (remove_equal ~c:c xs ys) = [];;
+let is_suffix ?(c = Stdlib.compare) xs ys = is_prefix ~c:c (rev xs) (rev ys);;
 
-let is_proper_prefix ?(c = compare) xs ys =
+let is_proper_prefix ?(c = Stdlib.compare) xs ys =
  let (xs,ys) = remove_equal ~c:c xs ys in
  xs = [] && ys <> []
 ;;
 
-let is_proper_suffix ?(c = compare) xs ys =
+let is_proper_suffix ?(c = Stdlib.compare) xs ys =
  is_proper_prefix ~c:c (rev xs) (rev ys)
 ;;
 

src/util/src/prelude.ml

@@ -46,12 +46,12 @@ let swap x f = f x;;
 let read_channel ?(buff_size = 1024*1024) ch =
   let size = 4*1024 in
   let loop = ref true in
-  let buff = String.create size in
+  let buff = Bytes.create size in
   let res  = Buffer.create buff_size in
   while !loop do
     let n = input ch buff 0 size in
     if n = 0 then loop := false
-             else Buffer.add_substring res buff 0 n
+             else Buffer.add_subbytes res buff 0 n
   done;
   Buffer.contents res
 ;;

src/util/src/process.ml

@@ -32,7 +32,7 @@ let set_signals h = Sys.set_signal Sys.sigterm h; Sys.set_signal Sys.sigalrm h;;
 (* Parallel Evaluations *)
 let child t w f i =
  set_signals Sys.Signal_default;
- ignore (Unix.write w "sync" 0 4);
+ ignore (Unix.write w (Bytes.of_string "sync") 0 4);
  let t = Option.fold (max 0.001 <.> flip (-.) (Unix.gettimeofday ())) 0.0 t in
  if t <= 0.0015 && t >= 0.0005 then exit 0;
  let status = {Unix.it_interval = 0.0; Unix.it_value = t} in

src/util/src/stringx.ml

@@ -25,30 +25,25 @@ include String;;
 
 (*** MODULE TYPES *************************************************************)
 module type STRING = sig
- val blit : string -> int -> string -> int -> int -> unit
- val capitalize : string -> string
+ val capitalize_ascii : string -> string
  val compare: string -> string -> int
  val concat : string -> string list -> string
  val contains : string -> char -> bool
  val contains_from : string -> int -> char -> bool
- val copy : string -> string
- val create : int -> string
  val escaped : string -> string
- val fill : string -> int -> int -> char -> unit
  val get : string -> int -> char
  val index : string -> char -> int
  val index_from : string -> int -> char -> int
  val iter : (char -> unit) -> string -> unit
  val length : string -> int
- val lowercase : string -> string
+ val lowercase_ascii : string -> string
  val make : int -> char -> string
  val rcontains_from : string -> int -> char -> bool
  val rindex : string -> char -> int
  val rindex_from : string -> int -> char -> int
- val set : string -> int -> char -> unit
  val sub : string -> int -> int -> string
- val uppercase : string -> string
- val uncapitalize : string -> string
+ val uppercase_ascii : string -> string
+ val uncapitalize_ascii : string -> string
 end
 
 (*** FUNCTIONS ****************************************************************)

src/util/src/util.mli

@@ -137,6 +137,7 @@ module Arg : sig
    | Tuple of spec list
    | Symbol of string list * (string -> unit)
    | Rest of (string -> unit)
+   | Rest_all of (string list -> unit)
    | Expand of (string -> string array)
   type usage_msg = string
 
@@ -931,8 +932,6 @@ module Index : sig
   (** [compare s t] compares [s] and [t]. It must be guaranteed that
   [compare s t = 0] if [s] and [t] are equal, [compare s t < 0] if [s]
   is smaller than [t], and [compare s t > 0] if [s] is greater than [t]. *)
-  val copy : t -> t
-  (** [copy t] copies the value [t]. *)
   val fprintf : Format.formatter -> t -> unit
   (** [fprintf fmt t] prints [t] using the [OCaml] module [Format]. *)
   val hash : t -> int
@@ -953,8 +952,6 @@ module Index : sig
   (** [compare s t] compares [s] and [t]. It must be guaranteed that
   [compare s t = 0] if [s] and [t] are equal, [compare s t < 0] if [s]
   is smaller than [t], and [compare s t > 0] if [s] is greater than [t]. *)
-  val copy : t -> t
-  (** [copy t] copies the value [t]. *)
   val fprintf : Format.formatter -> t -> unit
   (** [fprintf fmt t] prints [t] using the [OCaml] module [Format]. *)
   val hash : t -> int
@@ -1353,8 +1350,6 @@ module Isomorphism : sig
   (** [compare s t] compares [s] and [t]. It must be guaranteed that
   [compare s t = 0] if [s] and [t] are equal, [compare s t < 0] if [s]
   is smaller than [t], and [compare s t > 0] if [s] is greater than [t]. *)
-  val copy : t -> t
-  (** [copy t] copies the value [t]. *)
   val fprintf : Format.formatter -> t -> unit
   (** [fprintf fmt t] prints [t] using the [OCaml] module [Format]. *)
   val hash : t -> int
@@ -3105,30 +3100,25 @@ module String : sig
 
  (*** MODULE TYPES ************************************************************)
  module type STRING = sig
-  val blit : t -> int -> t -> int -> int -> unit
-  val capitalize : t -> t
+  val capitalize_ascii : t -> t
   val compare: t -> t -> int
   val concat : t -> t list -> t
   val contains : t -> char -> bool
   val contains_from : t -> int -> char -> bool
-  val copy : t -> t
-  val create : int -> t
   val escaped : t -> t
-  val fill : t -> int -> int -> char -> unit
   val get : t -> int -> char
   val index : t -> char -> int
   val index_from : t -> int -> char -> int
   val iter : (char -> unit) -> t -> unit
   val length : t -> int
-  val lowercase : t -> t
+  val lowercase_ascii : t -> t
   val make : int -> char -> t
   val rcontains_from : t -> int -> char -> bool
   val rindex : t -> char -> int
   val rindex_from : t -> int -> char -> int
-  val set : t -> int -> char -> unit
   val sub : t -> int -> int -> t
-  val uppercase : t -> t
-  val uncapitalize : t -> t
+  val uppercase_ascii : t -> t
+  val uncapitalize_ascii : t -> t
  end
  (** This module type contains all standard [OCaml] functions provided by the
  module [String]. *)

src/util/src/xsltproc.ml

@@ -34,12 +34,12 @@ let write ch s = output_string ch s;flush ch;;
 
 let read ch =
   let loop = ref true in
-  let buff = String.create buff_size in
+  let buff = Bytes.create buff_size in
   let res  = Buffer.create(1024*1024) in
   while !loop do
     let n = input ch buff 0 buff_size in
     if n = 0 then loop := false
-             else Buffer.add_substring res buff 0 n
+             else Buffer.add_subbytes res buff 0 n
   done;
   Buffer.contents res
 ;;