(***********************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* = '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 let abort (x : t) = assert false end (* Strings *) module String : CString.ExtS = 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.ExtS = CList let (@) = CList.append (* Arrays *) module Array : CArray.ExtS = CArray (* Sets *) module Set = CSet (* Maps *) module Map = CMap (* Stacks *) module Stack = CStack (* 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 (** Function composition: the mathematical [∘] operator. So [g % f] is a synonym for [fun x -> g (f x)]. Also because [%] is right-associative, [h % g % f] means [fun x -> h (g (f x))]. *) let (%) f g x = f (g 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 (* Stream *) let stream_nth n st = try List.nth (Stream.npeek (n+1) st) n with Failure _ -> raise Stream.Failure let stream_njunk n st = repeat n Stream.junk st (* Delayed computations *) type 'a delayed = unit -> 'a let delayed_force f = f () (* 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 map_union f g = function | Inl a -> Inl (f a) | Inr b -> Inr (g b) type iexn = Exninfo.iexn 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 in let in_chan = open_in fname in let s = " " in if input in_chan s 0 3 < 3 || not (is_bom s) then seek_in in_chan 0; in_chan