diff options
Diffstat (limited to 'lib/util.ml')
| -rw-r--r-- | lib/util.ml | 49 |
1 files changed, 33 insertions, 16 deletions
diff --git a/lib/util.ml b/lib/util.ml index 009dfbe1..7d7d380b 100644 --- a/lib/util.ml +++ b/lib/util.ml @@ -1,10 +1,12 @@ -(***********************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) -(* \VV/ *************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(***********************************************************************) +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \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 *) @@ -87,13 +89,17 @@ let matrix_transpose mat = let identity x = x -(** Function composition: the mathematical [∘] operator. +(** Left-to-right function composition: + + [f1 %> f2] is [fun x -> f2 (f1 x)]. - So [g % f] is a synonym for [fun x -> g (f x)]. + [f1 %> f2 %> f3] is [fun x -> f3 (f2 (f1 x))]. - Also because [%] is right-associative, [h % g % f] means [fun x -> h (g (f x))]. - *) -let (%) f g x = f (g 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 @@ -132,6 +138,8 @@ 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 @@ -157,11 +165,20 @@ let iraise = Exninfo.iraise let open_utf8_file_in fname = let is_bom s = - Int.equal (Char.code s.[0]) 0xEF && - Int.equal (Char.code s.[1]) 0xBB && - Int.equal (Char.code s.[2]) 0xBF + 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 = " " 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) |