Something went wrong. Try again.
forked from coq/coq
Something went wrong. Try again.
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222(************************************************************************)(* * 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,_,_) = alet pi2 (_,a,_) = alet 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 (* See https://ocaml.org/manual/emptyvariants.html *) type t = | let abort (x : t) = match x with _ -> .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 'btype 'a until = 'a CSig.until = Stop of 'a | Cont of 'atype ('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 yend
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)