1 (* Copyright (C) 2000, HELM Team.
3 * This file is part of HELM, an Hypertextual, Electronic
4 * Library of Mathematics, developed at the Computer Science
5 * Department, University of Bologna, Italy.
7 * HELM is free software; you can redistribute it and/or
8 * modify it under the terms of the GNU General Public License
9 * as published by the Free Software Foundation; either version 2
10 * of the License, or (at your option) any later version.
12 * HELM is distributed in the hope that it will be useful,
13 * but WITHOUT ANY WARRANTY; without even the implied warranty of
14 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
15 * GNU General Public License for more details.
17 * You should have received a copy of the GNU General Public License
18 * along with HELM; if not, write to the Free Software
19 * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
22 * For details, see the HELM World-Wide-Web page,
23 * http://cs.unibo.it/helm/.
26 (* AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
29 (* time handling ***********************************************************)
31 type time = float * float
34 (Sys.time (), Unix.time ())
36 let stop_time (s0, u0) =
37 let s1 = Sys.time () in
38 let u1 = Unix.time () in
39 Printf.sprintf "%.2fs,%.2fs" (s1 -. s0) (u1 -. u0)
41 (* operations on lists *****************************************************)
43 type 'a comparison = Lt
47 let list_join f l1 l2 =
48 let rec aux = function
51 | ((h1 :: t1) as v1), ((h2 :: t2) as v2) -> begin
53 | Lt -> h1 :: aux (t1, v2)
54 | Gt -> h2 :: aux (v1, t2)
55 | Eq h -> h :: aux (t1, t2)
59 let list_meet f l1 l2 =
60 let rec aux = function
63 | ((h1 :: t1) as v1), ((h2 :: t2) as v2) -> begin
67 | Eq h -> h :: aux (t1, t2)
71 let rec flat_list out f s = function
74 | a :: tail -> f a; out s; flat_list out f s tail
76 let rec add_assoc ap = function
78 | head :: tail when fst head = fst ap -> ap :: tail
79 | head :: tail -> head :: add_assoc ap tail
81 (* int of string ************************************************************)
89 let l = String.length s in
91 if i = l then End else
93 | ' ' | '\t' | '\r' | 'n' -> Space
94 | '0' .. '9' -> Figure (Char.code s.[i] - Char.code '0')
97 let rec aux i xv = match get_t i, xv with
99 | End, None -> raise (Failure "int_of_string")
101 | Space, xv -> aux (succ i) xv
102 | Figure f, None -> aux (succ i) (Some f)
103 | Figure f, Some v -> aux (succ i) (Some (10 * v + f))