Source file util.ml

(************************************************************************)
(*         *      The Rocq Prover / The Rocq Development Team           *)
(*  v      *         Copyright INRIA, CNRS and contributors             *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

(* Mapping under pairs *)

let on_fst f (a,b) = (f a,b)
let on_snd f (a,b) = (a,f b)
let map_pair f (a,b) = (f a,f b)

(* Folding under pairs *)

let fold_fst f acc (a,b) = let acc, a = f acc a in acc, (a, b)
let fold_snd f acc (a,b) = let acc, b = f acc b in acc, (a, b)

(* Equality on pairs *)

let eq_pair eq1 eq2 (a,b) (a',b') = eq1 a a' && eq2 b b'

(* Mapping under triplets *)

let on_pi1 f (a,b,c) = (f a,b,c)
let on_pi2 f (a,b,c) = (a,f b,c)
let on_pi3 f (a,b,c) = (a,b,f c)

(* Projections from triplets *)

let pi1 (a,_,_) = a
let pi2 (_,a,_) = a
let pi3 (_,_,a) = a

(* Characters *)

let is_letter c = (c >= 'a' && c <= 'z') || (c >= 'A' && c <= 'Z')
let is_digit c = (c >= '0' && c <= '9')
let is_ident_tail c =
  is_letter c || is_digit c || c = '\'' || c = '_'
let is_blank = function
  | ' ' | '\r' | '\t' | '\n' -> true
  | _ -> false

module Empty =
struct
  type t = { abort : 'a. 'a }
  let abort (x : t) = x.abort
end

(* Strings *)

module String = CString

let subst_command_placeholder s t =
  let buff = Buffer.create (String.length s + String.length t) in
  let i = ref 0 in
  while (!i < String.length s) do
    if s.[!i] = '%' && !i+1 < String.length s && s.[!i+1] = 's'
    then (Buffer.add_string buff t;incr i)
    else Buffer.add_char buff s.[!i];
    incr i
  done;
  Buffer.contents buff

(* Lists *)

module List = CList

let (@) = CList.append

(* Arrays *)

module Array = CArray

(* Sets *)

module Set = CSet

(* Maps *)

module Map = CMap

(* Matrices *)

let matrix_transpose mat =
  List.fold_right (List.map2 (fun p c -> p::c)) mat
    (if List.is_empty mat then [] else List.map (fun _ -> []) (List.hd mat))

(* Functions *)

let identity x = x

(** Left-to-right function composition:

    [f1 %> f2] is [fun x -> f2 (f1 x)].

    [f1 %> f2 %> f3] is [fun x -> f3 (f2 (f1 x))].

    [f1 %> f2 %> f3 %> f4] is [fun x -> f4 (f3 (f2 (f1 x)))]

    etc.
*)
let (%>) f g x = g (f x)

let const x _ = x

let iterate =
  let rec iterate_f f n x =
    if n <= 0 then x else iterate_f f (pred n) (f x)
  in
  iterate_f

let repeat n f x =
  let rec loop i = if i <> 0 then (f x; loop (i - 1)) in loop n

let app_opt f x =
  match f with
  | Some f -> f x
  | None -> x

(* Delayed computations *)

type 'a delayed = unit -> 'a

let delayed_force f = f ()

(* finalize - Credit X.Leroy, D.Remy. , adapted to Coq's exn handling *)
let with_finally finally y =
  let acquire () = () in
  let release () = finally y in
  Memprof_coq.Masking.with_resource ~acquire () ~release

let try_finally f x finally y =
  let open Memprof_coq.Resource_bind in
  let& () = with_finally finally y in
  f x

let with_flag_value r =
  let acquire () = !r in
  let release r_val = r := r_val in
  Memprof_coq.Masking.with_resource ~acquire () ~release

let protect_ref ~scope r =
  let scope _ = scope () in
  with_flag_value ~scope r

let protect_state ~freeze ~unfreeze ~scope =
  let acquire () = freeze () in
  let release p_st = unfreeze p_st in
  let scope _ = scope () in
  Memprof_coq.Masking.with_resource ~acquire () ~release ~scope

let atomify f x =
  let acquire () = f x in
  let release _ = () in
  let scope r = r in
  Memprof_coq.Masking.with_resource ~acquire () ~release ~scope

(* Misc *)

type ('a, 'b) union = ('a, 'b) CSig.union = Inl of 'a | Inr of 'b
type 'a until = 'a CSig.until = Stop of 'a | Cont of 'a
type ('a, 'b) eq = ('a, 'b) CSig.eq = Refl : ('a, 'a) eq

let sym : type a b. (a, b) eq -> (b, a) eq = fun Refl -> Refl

module Union =
struct
  let map f g = function
    | Inl a -> Inl (f a)
    | Inr b -> Inr (g b)

  (** Lifting equality onto union types. *)
  let equal f g x y = match x, y with
    | Inl x, Inl y -> f x y
    | Inr x, Inr y -> g x y
    | _, _ -> false

  let fold_left f g a = function
    | Inl y -> f a y
    | Inr y -> g a y
end

module Compare = struct
  type list = [] | (::) : (('a -> 'a -> int) * 'a * 'a) * list -> list

  let rec compare = function
    | [] -> 0
    | (cmp,x,y) :: rest ->
      let c = cmp x y in
      if c <> 0 then c
      else compare rest

end

let map_union = Union.map

let open_utf8_file_in fname =
  let is_bom s =
    Int.equal (Char.code (Bytes.get s 0)) 0xEF &&
    Int.equal (Char.code (Bytes.get s 1)) 0xBB &&
    Int.equal (Char.code (Bytes.get s 2)) 0xBF
  in
  let in_chan = open_in fname in
  let s = Bytes.make 3 ' ' in
  if input in_chan s 0 3 < 3 || not (is_bom s) then seek_in in_chan 0;
  in_chan

(** A trick which can typically be used to store on the fly the
   computation of values in the "when" clause of a "match" then
   retrieve the evaluated result in the r.h.s of the clause *)

let set_temporary_memory () =
  let a = ref None in
  (fun x -> assert (!a = None); a := Some x; x),
  (fun () -> match !a with Some x -> x | None -> assert false)