diff options
Diffstat (limited to 'lib')
55 files changed, 4547 insertions, 766 deletions
diff --git a/lib/bigint.ml b/lib/bigint.ml index 7671b0fc..f505bbe1 100644 --- a/lib/bigint.ml +++ b/lib/bigint.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: bigint.ml 9821 2007-05-11 17:00:58Z aspiwack $ *) +(* $Id$ *) (*i*) open Pp @@ -19,8 +19,8 @@ open Pp (* An integer is canonically represented as an array of k-digits blocs. 0 is represented by the empty array and -1 by the singleton [|-1|]. - The first bloc is in the range ]0;10^k[ for positive numbers. - The first bloc is in the range ]-10^k;-1[ for negative ones. + The first bloc is in the range ]0;10^k[ for positive numbers. + The first bloc is in the range ]-10^k;-1[ for negative ones. All other blocs are numbers in the range [0;10^k[. Negative numbers are represented using 2's complementation. For instance, @@ -78,7 +78,7 @@ let normalize_neg n = if Array.length n' = 0 then [|-1|] else (n'.(0) <- n'.(0) - base; n') let rec normalize n = - if Array.length n = 0 then n else + if Array.length n = 0 then n else if n.(0) = -1 then normalize_neg n else normalize_pos n let neg m = @@ -167,8 +167,6 @@ let less_than m n = (Array.length m = Array.length n && less_than_same_size m n 0 0)) let equal m n = (m = n) - -let less_or_equal_than m n = equal m n or less_than m n let less_than_shift_pos k m n = (Array.length m - k < Array.length n) @@ -194,7 +192,7 @@ let euclid m d = if is_strictly_neg m then (-1),neg m else 1,Array.copy m in let isnegd, d = if is_strictly_neg d then (-1),neg d else 1,d in if d = zero then raise Division_by_zero; - let q,r = + let q,r = if less_than m d then (zero,m) else let ql = Array.length m - Array.length d in let q = Array.create (ql+1) 0 in @@ -202,7 +200,7 @@ let euclid m d = while not (less_than_shift_pos !i m d) do if m.(!i)=0 then incr i else if can_divide !i m d 0 then begin - let v = + let v = if Array.length d > 1 && d.(0) <> m.(!i) then (m.(!i) * base + m.(!i+1)) / (d.(0) * base + d.(1) + 1) else @@ -234,11 +232,11 @@ let of_string s = let r = (String.length s - !d) mod size in let h = String.sub s (!d) r in if !d = String.length s - 1 && isneg && h="1" then neg_one else - let e = if h<>"" then 1 else 0 in + let e = if h<>"" then 1 else 0 in let l = (String.length s - !d) / size in let a = Array.create (l + e + n) 0 in if isneg then begin - a.(0) <- (-1); + a.(0) <- (-1); let carry = ref 0 in for i=l downto 1 do let v = int_of_string (String.sub s ((i-1)*size + !d +r) size)+ !carry in @@ -298,7 +296,7 @@ let app_pair f (m, n) = (f m, f n) let add m n = - if Obj.is_int m & Obj.is_int n + if Obj.is_int m & Obj.is_int n then big_of_int (coerce_to_int m + coerce_to_int n) else big_of_ints (add (ints_of_z m) (ints_of_z n)) @@ -313,8 +311,8 @@ let mult m n = else big_of_ints (mult (ints_of_z m) (ints_of_z n)) let euclid m n = - if Obj.is_int m & Obj.is_int n - then app_pair big_of_int + if Obj.is_int m & Obj.is_int n + then app_pair big_of_int (coerce_to_int m / coerce_to_int n, coerce_to_int m mod coerce_to_int n) else app_pair big_of_ints (euclid (ints_of_z m) (ints_of_z n)) @@ -335,9 +333,7 @@ let one = big_of_int 1 let sub_1 n = sub n one let add_1 n = add n one let two = big_of_int 2 -let neg_two = big_of_int (-2) let mult_2 n = add n n -let is_zero n = n=zero let div2_with_rest n = let (q,b) = euclid n two in @@ -364,12 +360,12 @@ let pow = let (quo,rem) = div2_with_rest m in pow_aux ((* [if m mod 2 = 1]*) - if rem then + if rem then mult n odd_rest else odd_rest ) (* quo = [m/2] *) - (mult n n) quo + (mult n n) quo in pow_aux one @@ -397,7 +393,7 @@ let check () = let s = Printf.sprintf "%30s" (to_string n) in let s' = Printf.sprintf "% 30.0f" (round n') in if s <> s' then Printf.printf "%s: %s <> %s\n" op s s' in -List.iter (fun a -> List.iter (fun b -> +List.iter (fun a -> List.iter (fun b -> let n = of_string a and m = of_string b in let n' = float_of_string a and m' = float_of_string b in let a = add n m and a' = n' +. m' in diff --git a/lib/bigint.mli b/lib/bigint.mli index f6d3da7b..69b035c4 100644 --- a/lib/bigint.mli +++ b/lib/bigint.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: bigint.mli 9821 2007-05-11 17:00:58Z aspiwack $ i*) +(*i $Id$ i*) (*i*) open Pp diff --git a/lib/bstack.ml b/lib/bstack.ml index 35bbf32b..4191ccdb 100644 --- a/lib/bstack.ml +++ b/lib/bstack.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: bstack.ml 10441 2008-01-15 16:37:46Z lmamane $ *) +(* $Id$ *) (* Queues of a given length *) @@ -47,10 +47,10 @@ let push bs e = incr_size bs; bs.depth <- bs.depth + 1; bs.stack.(bs.pos) <- e - + let pop bs = if bs.size > 1 then begin - bs.size <- bs.size - 1; + bs.size <- bs.size - 1; bs.depth <- bs.depth - 1; let oldpos = bs.pos in decr_pos bs; @@ -61,7 +61,7 @@ let pop bs = let top bs = if bs.size >= 1 then bs.stack.(bs.pos) else error "Nothing on the stack" - + let app_push bs f = if bs.size = 0 then error "Nothing on the stack" else push bs (f (bs.stack.(bs.pos))) diff --git a/lib/bstack.mli b/lib/bstack.mli index ca2b5f02..cef8e1d9 100644 --- a/lib/bstack.mli +++ b/lib/bstack.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: bstack.mli 10441 2008-01-15 16:37:46Z lmamane $ i*) +(*i $Id$ i*) (* Bounded stacks. If the depth is [None], then there is no depth limit. *) diff --git a/lib/compat.ml4 b/lib/compat.ml4 index 40cffadb..7566624b 100644 --- a/lib/compat.ml4 +++ b/lib/compat.ml4 @@ -12,8 +12,8 @@ IFDEF OCAML309 THEN DEFINE OCAML308 END -IFDEF CAMLP5 THEN -module M = struct +IFDEF CAMLP5 THEN +module M = struct type loc = Stdpp.location let dummy_loc = Stdpp.dummy_loc let make_loc = Stdpp.make_loc @@ -23,7 +23,6 @@ let join_loc loc1 loc2 = else Stdpp.encl_loc loc1 loc2 type token = string*string type lexer = token Token.glexer -let using l x = l.Token.tok_using x end ELSE IFDEF OCAML308 THEN module M = struct @@ -40,12 +39,11 @@ let unloc (b,e) = loc let join_loc loc1 loc2 = if loc1 = dummy_loc or loc2 = dummy_loc then dummy_loc - else (fst loc1, snd loc2) + else (fst loc1, snd loc2) type token = Token.t type lexer = Token.lexer -let using l x = l.Token.using x end -ELSE +ELSE module M = struct type loc = int * int let dummy_loc = (0,0) @@ -56,7 +54,6 @@ let join_loc loc1 loc2 = else (fst loc1, snd loc2) type token = Token.t type lexer = Token.lexer -let using l x = l.Token.using x end END END @@ -68,4 +65,3 @@ let unloc = M.unloc let join_loc = M.join_loc type token = M.token type lexer = M.lexer -let using = M.using diff --git a/lib/dnet.ml b/lib/dnet.ml new file mode 100644 index 00000000..f7b36929 --- /dev/null +++ b/lib/dnet.ml @@ -0,0 +1,295 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* $Id:$ *) + +(* Generic dnet implementation over non-recursive types *) + +module type Datatype = +sig + type 'a t + val map : ('a -> 'b) -> 'a t -> 'b t + val map2 : ('a -> 'b -> 'c) -> 'a t -> 'b t -> 'c t + val fold : ('a -> 'b -> 'a) -> 'a -> 'b t -> 'a + val fold2 : ('a -> 'b -> 'c -> 'a) -> 'a -> 'b t -> 'c t -> 'a + val compare : unit t -> unit t -> int + val terminal : 'a t -> bool + val choose : ('a -> 'b) -> 'a t -> 'b +end + +module type S = +sig + type t + type ident + type meta + type 'a structure + module Idset : Set.S with type elt=ident + type 'a pattern = + | Term of 'a + | Meta of meta + type term_pattern = ('a structure) pattern as 'a + val empty : t + val add : t -> term_pattern -> ident -> t + val find_all : t -> Idset.t + val fold_pattern : + ('a -> (Idset.t * meta * t) -> 'a) -> 'a -> term_pattern -> t -> Idset.t option * 'a + val find_match : term_pattern -> t -> Idset.t + val inter : t -> t -> t + val union : t -> t -> t + val map : (ident -> ident) -> (unit structure -> unit structure) -> t -> t +end + +module Make = + functor (T:Datatype) -> + functor (Ident:Set.OrderedType) -> + functor (Meta:Set.OrderedType) -> +struct + + type ident = Ident.t + type meta = Meta.t + + type 'a pattern = + | Term of 'a + | Meta of meta + + type 'a structure = 'a T.t + + module Idset = Set.Make(Ident) + module Mmap = Map.Make(Meta) + module Tmap = Map.Make(struct type t = unit structure + let compare = T.compare end) + + type term_pattern = term_pattern structure pattern + type idset = Idset.t + + + + (* we store identifiers at the leaf of the dnet *) + type node = + | Node of t structure + | Terminal of t structure * idset + + (* at each node, we have a bunch of nodes (actually a map between + the bare node and a subnet) and a bunch of metavariables *) + and t = Nodes of node Tmap.t * idset Mmap.t + + let empty : t = Nodes (Tmap.empty, Mmap.empty) + + (* the head of a data is of type unit structure *) + let head w = T.map (fun c -> ()) w + + (* given a node of the net and a word, returns the subnet with the + same head as the word (with the rest of the nodes) *) + let split l (w:'a structure) : node * node Tmap.t = + let elt : node = Tmap.find (head w) l in + (elt, Tmap.remove (head w) l) + + let select l w = Tmap.find (head w) l + + let rec add (Nodes (t,m):t) (w:term_pattern) (id:ident) : t = + match w with Term w -> + ( try + let (n,tl) = split t w in + let new_node = match n with + | Terminal (e,is) -> Terminal (e,Idset.add id is) + | Node e -> Node (T.map2 (fun t p -> add t p id) e w) in + Nodes ((Tmap.add (head w) new_node tl), m) + with Not_found -> + let new_content = T.map (fun p -> add empty p id) w in + let new_node = + if T.terminal w then + Terminal (new_content, Idset.singleton id) + else Node new_content in + Nodes ((Tmap.add (head w) new_node t), m) ) + | Meta i -> + let m = + try Mmap.add i (Idset.add id (Mmap.find i m)) m + with Not_found -> Mmap.add i (Idset.singleton id) m in + Nodes (t, m) + + let add t w id = add t w id + + let rec find_all (Nodes (t,m)) : idset = + Idset.union + (Mmap.fold (fun _ -> Idset.union) m Idset.empty) + (Tmap.fold + ( fun _ n acc -> + let s2 = match n with + | Terminal (_,is) -> is + | Node e -> T.choose find_all e in + Idset.union acc s2 + ) t Idset.empty) + +(* (\* optimization hack: Not_found is catched in fold_pattern *\) *) +(* let fast_inter s1 s2 = *) +(* if Idset.is_empty s1 || Idset.is_empty s2 then raise Not_found *) +(* else Idset.inter s1 s2 *) + +(* let option_any2 f s1 s2 = match s1,s2 with *) +(* | Some s1, Some s2 -> f s1 s2 *) +(* | (Some s, _ | _, Some s) -> s *) +(* | _ -> raise Not_found *) + +(* let fold_pattern ?(complete=true) f acc pat dn = *) +(* let deferred = ref [] in *) +(* let leafs,metas = ref None, ref None in *) +(* let leaf s = leafs := match !leafs with *) +(* | None -> Some s *) +(* | Some s' -> Some (fast_inter s s') in *) +(* let meta s = metas := match !metas with *) +(* | None -> Some s *) +(* | Some s' -> Some (Idset.union s s') in *) +(* let defer c = deferred := c::!deferred in *) +(* let rec fp_rec (p:term_pattern) (Nodes(t,m) as dn:t) = *) +(* Mmap.iter (fun _ -> meta) m; (\* TODO: gérer patterns nonlin ici *\) *) +(* match p with *) +(* | Meta m -> defer (m,dn) *) +(* | Term w -> *) +(* try match select t w with *) +(* | Terminal (_,is) -> leaf is *) +(* | Node e -> *) +(* if complete then T.fold2 (fun _ -> fp_rec) () w e else *) +(* if T.fold2 *) +(* (fun b p dn -> match p with *) +(* | Term _ -> fp_rec p dn; false *) +(* | Meta _ -> b *) +(* ) true w e *) +(* then T.choose (T.choose fp_rec w) e *) +(* with Not_found -> *) +(* if Mmap.is_empty m then raise Not_found else () *) +(* in try *) +(* fp_rec pat dn; *) +(* (try Some (option_any2 Idset.union !leafs !metas) with Not_found -> None), *) +(* List.fold_left (fun acc (m,dn) -> f m dn acc) acc !deferred *) +(* with Not_found -> None,acc *) + + (* Sets with a neutral element for inter *) + module OSet (S:Set.S) = struct + type t = S.t option + let union s1 s2 = match s1,s2 with + | (None, _ | _, None) -> None + | Some a, Some b -> Some (S.union a b) + let inter s1 s2 = match s1,s2 with + | (None, a | a, None) -> a + | Some a, Some b -> Some (S.inter a b) + let is_empty = function + | None -> false + | Some s -> S.is_empty s + (* optimization hack: Not_found is catched in fold_pattern *) + let fast_inter s1 s2 = + if is_empty s1 || is_empty s2 then raise Not_found + else let r = inter s1 s2 in + if is_empty r then raise Not_found else r + let full = None + let empty = Some S.empty + end + + module OIdset = OSet(Idset) + + let fold_pattern ?(complete=true) f acc pat dn = + let deferred = ref [] in + let defer c = deferred := c::!deferred in + + let rec fp_rec metas p (Nodes(t,m) as dn:t) = + (* TODO gérer les dnets non-linéaires *) + let metas = Mmap.fold (fun _ -> Idset.union) m metas in + match p with + | Meta m -> defer (metas,m,dn); OIdset.full + | Term w -> + let curm = Mmap.fold (fun _ -> Idset.union) m Idset.empty in + try match select t w with + | Terminal (_,is) -> Some (Idset.union curm is) + | Node e -> + let ids = if complete then T.fold2 + (fun acc w e -> + OIdset.fast_inter acc (fp_rec metas w e) + ) OIdset.full w e + else + let (all_metas, res) = T.fold2 + (fun (b,acc) w e -> match w with + | Term _ -> false, OIdset.fast_inter acc (fp_rec metas w e) + | Meta _ -> b, acc + ) (true,OIdset.full) w e in + if all_metas then T.choose (T.choose (fp_rec metas) w) e + else res in + OIdset.union ids (Some curm) + with Not_found -> + if Idset.is_empty metas then raise Not_found else Some curm in + let cand = + try fp_rec Idset.empty pat dn + with Not_found -> OIdset.empty in + let res = List.fold_left f acc !deferred in + cand, res + + (* intersection of two dnets. keep only the common pairs *) + let rec inter (t1:t) (t2:t) : t = + let inter_map f (Nodes (t1,m1):t) (Nodes (t2,m2):t) : t = + Nodes + (Tmap.fold + ( fun k e acc -> + try Tmap.add k (f e (Tmap.find k t2)) acc + with Not_found -> acc + ) t1 Tmap.empty, + Mmap.fold + ( fun m s acc -> + try Mmap.add m (Idset.inter s (Mmap.find m m2)) acc + with Not_found -> acc + ) m1 Mmap.empty + ) in + inter_map + (fun n1 n2 -> match n1,n2 with + | Terminal (e1,s1), Terminal (_,s2) -> Terminal (e1,Idset.inter s1 s2) + | Node e1, Node e2 -> Node (T.map2 inter e1 e2) + | _ -> assert false + ) t1 t2 + + let rec union (t1:t) (t2:t) : t = + let union_map f (Nodes (t1,m1):t) (Nodes (t2,m2):t) : t = + Nodes + (Tmap.fold + ( fun k e acc -> + try Tmap.add k (f e (Tmap.find k acc)) acc + with Not_found -> Tmap.add k e acc + ) t1 t2, + Mmap.fold + ( fun m s acc -> + try Mmap.add m (Idset.inter s (Mmap.find m acc)) acc + with Not_found -> Mmap.add m s acc + ) m1 m2 + ) in + union_map + (fun n1 n2 -> match n1,n2 with + | Terminal (e1,s1), Terminal (_,s2) -> Terminal (e1,Idset.union s1 s2) + | Node e1, Node e2 -> Node (T.map2 union e1 e2) + | _ -> assert false + ) t1 t2 + + let find_match (p:term_pattern) (t:t) : idset = + let metas = ref Mmap.empty in + let (mset,lset) = fold_pattern ~complete:false + (fun acc (mset,m,t) -> + let all = OIdset.fast_inter acc + (Some(let t = try inter t (Mmap.find m !metas) with Not_found -> t in + metas := Mmap.add m t !metas; + find_all t)) in + OIdset.union (Some mset) all + ) None p t in + Option.get (OIdset.inter mset lset) + + let fold_pattern f acc p dn = fold_pattern ~complete:true f acc p dn + + let idset_map f is = Idset.fold (fun e acc -> Idset.add (f e) acc) is Idset.empty + let tmap_map f g m = Tmap.fold (fun k e acc -> Tmap.add (f k) (g e) acc) m Tmap.empty + + let rec map sidset sterm (Nodes (t,m)) : t = + let snode = function + | Terminal (e,is) -> Terminal (e,idset_map sidset is) + | Node e -> Node (T.map (map sidset sterm) e) in + Nodes (tmap_map sterm snode t, Mmap.map (idset_map sidset) m) + +end diff --git a/lib/dnet.mli b/lib/dnet.mli new file mode 100644 index 00000000..61998d63 --- /dev/null +++ b/lib/dnet.mli @@ -0,0 +1,128 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* $Id:$ *) + +(* Generic discrimination net implementation over recursive + types. This module implements a association data structure similar + to tries but working on any types (not just lists). It is a term + indexing datastructure, a generalization of the discrimination nets + described for example in W.W.McCune, 1992, related also to + generalized tries [Hinze, 2000]. + + You can add pairs of (term,identifier) into a dnet, where the + identifier is *unique*, and search terms in a dnet filtering a + given pattern (retrievial of instances). It returns all identifiers + associated with terms matching the pattern. It also works the other + way around : You provide a set of patterns and a term, and it + returns all patterns which the term matches (retrievial of + generalizations). That's why you provide *patterns* everywhere. + + Warning 1: Full unification doesn't work as for now. Make sure the + set of metavariables in the structure and in the queries are + distincts, or you'll get unexpected behaviours. + + Warning 2: This structure is perfect, i.e. the set of candidates + returned is equal to the set of solutions. Beware of DeBruijn + shifts and sorts subtyping though (which makes the comparison not + symmetric, see term_dnet.ml). + + The complexity of the search is (almost) the depth of the term. + + To use it, you have to provide a module (Datatype) with the datatype + parametrized on the recursive argument. example: + + type btree = type 'a btree0 = + | Leaf ===> | Leaf + | Node of btree * btree | Node of 'a * 'a + +*) + +(* datatype you want to build a dnet on *) +module type Datatype = +sig + (* parametric datatype. ['a] is morally the recursive argument *) + type 'a t + + (* non-recursive mapping of subterms *) + val map : ('a -> 'b) -> 'a t -> 'b t + val map2 : ('a -> 'b -> 'c) -> 'a t -> 'b t -> 'c t + + (* non-recursive folding of subterms *) + val fold : ('a -> 'b -> 'a) -> 'a -> 'b t -> 'a + val fold2 : ('a -> 'b -> 'c -> 'a) -> 'a -> 'b t -> 'c t -> 'a + + (* comparison of constructors *) + val compare : unit t -> unit t -> int + + (* for each constructor, is it not-parametric on 'a? *) + val terminal : 'a t -> bool + + (* [choose f w] applies f on ONE of the subterms of w *) + val choose : ('a -> 'b) -> 'a t -> 'b +end + +module type S = +sig + type t + + (* provided identifier type *) + type ident + + (* provided metavariable type *) + type meta + + (* provided parametrized datastructure *) + type 'a structure + + (* returned sets of solutions *) + module Idset : Set.S with type elt=ident + + (* a pattern is a term where each node can be a unification + variable *) + type 'a pattern = + | Term of 'a + | Meta of meta + + type term_pattern = 'a structure pattern as 'a + + val empty : t + + (* [add t w i] adds a new association (w,i) in t. *) + val add : t -> term_pattern -> ident -> t + + (* [find_all t] returns all identifiers contained in t. *) + val find_all : t -> Idset.t + + (* [fold_pattern f acc p dn] folds f on each meta of p, passing the + meta and the sub-dnet under it. The result includes: + - Some set if identifiers were gathered on the leafs of the term + - None if the pattern contains no leaf (only Metas at the leafs). + *) + val fold_pattern : + ('a -> (Idset.t * meta * t) -> 'a) -> 'a -> term_pattern -> t -> Idset.t option * 'a + + (* [find_match p t] returns identifiers of all terms matching p in + t. *) + val find_match : term_pattern -> t -> Idset.t + + (* set operations on dnets *) + val inter : t -> t -> t + val union : t -> t -> t + + (* apply a function on each identifier and node of terms in a dnet *) + val map : (ident -> ident) -> (unit structure -> unit structure) -> t -> t +end + +module Make : + functor (T:Datatype) -> + functor (Ident:Set.OrderedType) -> + functor (Meta:Set.OrderedType) -> + S with type ident = Ident.t + and type meta = Meta.t + and type 'a structure = 'a T.t @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: dyn.ml 5920 2004-07-16 20:01:26Z herbelin $ *) +(* $Id$ *) open Util @@ -17,7 +17,7 @@ type t = string * Obj.t let dyntab = ref ([] : string list) let create s = - if List.mem s !dyntab then + if List.mem s !dyntab then anomaly ("Dyn.create: already declared dynamic " ^ s); dyntab := s :: !dyntab; ((fun v -> (s,Obj.repr v)), diff --git a/lib/dyn.mli b/lib/dyn.mli index 86a1560a..1149612f 100644 --- a/lib/dyn.mli +++ b/lib/dyn.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: dyn.mli 5920 2004-07-16 20:01:26Z herbelin $ i*) +(*i $Id$ i*) (* Dynamics. Use with extreme care. Not for kids. *) diff --git a/lib/edit.ml b/lib/edit.ml index 380abfd8..fd870a21 100644 --- a/lib/edit.ml +++ b/lib/edit.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: edit.ml 10441 2008-01-15 16:37:46Z lmamane $ *) +(* $Id$ *) open Pp open Util @@ -16,7 +16,7 @@ type ('a,'b,'c) t = { mutable last_focused_stk : 'a list; buf : ('a, 'b Bstack.t * 'c) Hashtbl.t } -let empty () = { +let empty () = { focus = None; last_focused_stk = []; buf = Hashtbl.create 17 } @@ -38,7 +38,7 @@ let unfocus e = e.last_focused_stk <- foc::(list_except foc e.last_focused_stk); e.focus <- None end - + let last_focused e = match e.last_focused_stk with | [] -> None @@ -48,7 +48,7 @@ let restore_last_focus e = match e.last_focused_stk with | [] -> () | f::_ -> focus e f - + let focusedp e = match e.focus with | None -> false @@ -96,8 +96,8 @@ let depth e = (* Undo focused proof of [e] to reach depth [n] *) let undo_todepth e n = match e.focus with - | None -> - if n <> 0 + | None -> + if n <> 0 then errorlabstrm "Edit.undo_todepth" (str"No proof in progress") else () (* if there is no proof in progress, then n must be zero *) | Some d -> @@ -109,7 +109,7 @@ let undo_todepth e n = let create e (d,b,c,usize) = if Hashtbl.mem e.buf d then - errorlabstrm "Edit.create" + errorlabstrm "Edit.create" (str"Already editing something of that name"); let bs = Bstack.create usize b in Hashtbl.add e.buf d (bs,c) @@ -123,11 +123,11 @@ let delete e d = | Some d' -> if d = d' then (e.focus <- None ; (restore_last_focus e)) | None -> () -let dom e = +let dom e = let l = ref [] in Hashtbl.iter (fun x _ -> l := x :: !l) e.buf; !l - + let clear e = e.focus <- None; e.last_focused_stk <- []; diff --git a/lib/edit.mli b/lib/edit.mli index ab82c1f9..d13d9c6f 100644 --- a/lib/edit.mli +++ b/lib/edit.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: edit.mli 6947 2005-04-20 16:18:41Z coq $ i*) +(*i $Id$ i*) (* The type of editors. * An editor is a finite map, ['a -> 'b], which knows how to apply diff --git a/lib/envars.ml b/lib/envars.ml index d700ffe1..2e680ad0 100644 --- a/lib/envars.ml +++ b/lib/envars.ml @@ -9,77 +9,77 @@ (* This file gathers environment variables needed by Coq to run (such as coqlib) *) -let coqbin () = +let coqbin () = if !Flags.boot || Coq_config.local then Filename.concat Coq_config.coqsrc "bin" else System.canonical_path_name (Filename.dirname Sys.executable_name) -let guess_coqlib () = +let guess_coqlib () = let file = "states/initial.coq" in - if Sys.file_exists (Filename.concat Coq_config.coqlib file) + if Sys.file_exists (Filename.concat Coq_config.coqlib file) then Coq_config.coqlib - else + else let coqbin = System.canonical_path_name (Filename.dirname Sys.executable_name) in let prefix = Filename.dirname coqbin in - let rpath = if Coq_config.local then [] else + let rpath = if Coq_config.local then [] else (if Coq_config.arch = "win32" then ["lib"] else ["lib";"coq"]) in let coqlib = List.fold_left Filename.concat prefix rpath in if Sys.file_exists (Filename.concat coqlib file) then coqlib else Util.error "cannot guess a path for Coq libraries; please use -coqlib option" - -let coqlib () = + +let coqlib () = if !Flags.coqlib_spec then !Flags.coqlib else (if !Flags.boot then Coq_config.coqsrc else guess_coqlib ()) let path_to_list p = let sep = if Sys.os_type = "Win32" then ';' else ':' in - Util.split_string_at sep p + Util.split_string_at sep p let rec which l f = match l with | [] -> raise Not_found - | p :: tl -> - if Sys.file_exists (Filename.concat p f) - then p + | p :: tl -> + if Sys.file_exists (Filename.concat p f) + then p else which tl f - -let guess_camlbin () = - let path = try Sys.getenv "PATH" with _ -> raise Not_found in + +let guess_camlbin () = + let path = try Sys.getenv "PATH" with _ -> raise Not_found in let lpath = path_to_list path in which lpath "ocamlc" -let guess_camlp4bin () = - let path = try Sys.getenv "PATH" with _ -> raise Not_found in +let guess_camlp4bin () = + let path = try Sys.getenv "PATH" with _ -> raise Not_found in let lpath = path_to_list path in which lpath Coq_config.camlp4 -let camlbin () = +let camlbin () = if !Flags.camlbin_spec then !Flags.camlbin else if !Flags.boot then Coq_config.camlbin else try guess_camlbin () with _ -> Coq_config.camlbin -let camllib () = +let camllib () = if !Flags.boot then Coq_config.camllib - else - let camlbin = camlbin () in + else + let camlbin = camlbin () in let com = (Filename.concat camlbin "ocamlc") ^ " -where" in let _,res = System.run_command (fun x -> x) (fun _ -> ()) com in Util.strip res (* TODO : essayer aussi camlbin *) -let camlp4bin () = +let camlp4bin () = if !Flags.camlp4bin_spec then !Flags.camlp4bin else if !Flags.boot then Coq_config.camlp4bin else try guess_camlp4bin () with _ -> Coq_config.camlp4bin -let camlp4lib () = +let camlp4lib () = if !Flags.boot then Coq_config.camlp4lib - else - let camlp4bin = camlp4bin () in + else + let camlp4bin = camlp4bin () in let com = (Filename.concat camlp4bin Coq_config.camlp4) ^ " -where" in let _,res = System.run_command (fun x -> x) (fun _ -> ()) com in Util.strip res - + diff --git a/lib/explore.ml b/lib/explore.ml index 7e6de0c4..76049509 100644 --- a/lib/explore.ml +++ b/lib/explore.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: explore.ml 6066 2004-09-06 22:54:50Z barras $ i*) +(*i $Id$ i*) open Format @@ -23,7 +23,7 @@ module Make = functor(S : SearchProblem) -> struct type position = int list - let pp_position p = + let pp_position p = let rec pp_rec = function | [] -> () | [i] -> printf "%d" i @@ -33,21 +33,21 @@ module Make = functor(S : SearchProblem) -> struct (*s Depth first search. *) - let rec depth_first s = + let rec depth_first s = if S.success s then s else depth_first_many (S.branching s) and depth_first_many = function | [] -> raise Not_found | [s] -> depth_first s | s :: l -> try depth_first s with Not_found -> depth_first_many l - let debug_depth_first s = + let debug_depth_first s = let rec explore p s = pp_position p; S.pp s; if S.success s then s else explore_many 1 p (S.branching s) and explore_many i p = function | [] -> raise Not_found | [s] -> explore (i::p) s - | s :: l -> + | s :: l -> try explore (i::p) s with Not_found -> explore_many (succ i) p l in explore [1] s @@ -66,7 +66,7 @@ module Make = functor(S : SearchProblem) -> struct | h, x::t -> x, (h,t) | h, [] -> match List.rev h with x::t -> x, ([],t) | [] -> raise Empty - let breadth_first s = + let breadth_first s = let rec explore q = let (s, q') = try pop q with Empty -> raise Not_found in enqueue q' (S.branching s) @@ -76,15 +76,15 @@ module Make = functor(S : SearchProblem) -> struct in enqueue empty [s] - let debug_breadth_first s = + let debug_breadth_first s = let rec explore q = - let ((p,s), q') = try pop q with Empty -> raise Not_found in + let ((p,s), q') = try pop q with Empty -> raise Not_found in enqueue 1 p q' (S.branching s) and enqueue i p q = function - | [] -> + | [] -> explore q | s :: l -> - let ps = i::p in + let ps = i::p in pp_position ps; S.pp s; if S.success s then s else enqueue (succ i) p (push (ps,s) q) l in diff --git a/lib/explore.mli b/lib/explore.mli index 07f95e8a..e29f2795 100644 --- a/lib/explore.mli +++ b/lib/explore.mli @@ -6,18 +6,18 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: explore.mli 5920 2004-07-16 20:01:26Z herbelin $ i*) +(*i $Id$ i*) (*s Search strategies. *) (*s A search problem implements the following signature [SearchProblem]. [state] is the type of states of the search tree. - [branching] is the branching function; if [branching s] returns an + [branching] is the branching function; if [branching s] returns an empty list, then search from [s] is aborted; successors of [s] are recursively searched in the order they appear in the list. - [success] determines whether a given state is a success. + [success] determines whether a given state is a success. - [pp] is a pretty-printer for states used in debugging versions of the + [pp] is a pretty-printer for states used in debugging versions of the search functions. *) module type SearchProblem = sig @@ -33,7 +33,7 @@ module type SearchProblem = sig end (*s Functor [Make] returns some search functions given a search problem. - Search functions raise [Not_found] if no success is found. + Search functions raise [Not_found] if no success is found. States are always visited in the order they appear in the output of [branching] (whatever the search method is). Debugging versions of the search functions print the position of the diff --git a/lib/flags.ml b/lib/flags.ml index 928912e6..12d25c54 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: flags.ml 11801 2009-01-18 20:11:41Z herbelin $ i*) +(*i $Id$ i*) let with_option o f x = let old = !o in o:=true; @@ -37,6 +37,14 @@ let raw_print = ref false let unicode_syntax = ref false +(* Compatibility mode *) + +type compat_version = V8_2 +let compat_version = ref None +let version_strictly_greater v = + match !compat_version with None -> true | Some v' -> v'>v +let version_less_or_equal v = not (version_strictly_greater v) + (* Translate *) let beautify = ref false let make_beautify f = beautify := f @@ -55,6 +63,10 @@ let verbosely f x = without_option silent f x let if_silent f x = if !silent then f x let if_verbose f x = if not !silent then f x +let auto_intros = ref true +let make_auto_intros flag = auto_intros := flag +let is_auto_intros () = version_strictly_greater V8_2 && !auto_intros + let hash_cons_proofs = ref true let warn = ref true @@ -80,8 +92,8 @@ let is_unsafe s = Stringset.mem s !unsafe_set let boxed_definitions = ref true let set_boxed_definitions b = boxed_definitions := b -let boxed_definitions _ = !boxed_definitions - +let boxed_definitions _ = !boxed_definitions + (* Flags for external tools *) let subst_command_placeholder s t = @@ -102,6 +114,15 @@ let browser_cmd_fmt = with Not_found -> Coq_config.browser +let is_standard_doc_url url = + let wwwcompatprefix = "http://www.lix.polytechnique.fr/coq/" in + let wwwprefix = "http://coq.inria.fr/" in + let n = String.length wwwprefix in + let n' = String.length Coq_config.wwwrefman in + url = Coq_config.localwwwrefman || + url = Coq_config.wwwrefman || + url = wwwcompatprefix ^ String.sub Coq_config.wwwrefman n (n'-n) + (* Options for changing coqlib *) let coqlib_spec = ref false let coqlib = ref Coq_config.coqlib diff --git a/lib/flags.mli b/lib/flags.mli index c5903285..50ba923b 100644 --- a/lib/flags.mli +++ b/lib/flags.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: flags.mli 11801 2009-01-18 20:11:41Z herbelin $ i*) +(*i $Id$ i*) (* Global options of the system. *) @@ -29,6 +29,11 @@ val raw_print : bool ref val unicode_syntax : bool ref +type compat_version = V8_2 +val compat_version : compat_version option ref +val version_strictly_greater : compat_version -> bool +val version_less_or_equal : compat_version -> bool + val beautify : bool ref val make_beautify : bool -> unit val do_beautify : unit -> bool @@ -42,6 +47,9 @@ val verbosely : ('a -> 'b) -> 'a -> 'b val if_silent : ('a -> unit) -> 'a -> unit val if_verbose : ('a -> unit) -> 'a -> unit +val make_auto_intros : bool -> unit +val is_auto_intros : unit -> bool + val make_warn : bool -> unit val if_warn : ('a -> unit) -> 'a -> unit @@ -70,7 +78,9 @@ val boxed_definitions : unit -> bool (* Returns string format for default browser to use from Coq or CoqIDE *) val browser_cmd_fmt : string - + +val is_standard_doc_url : string -> bool + (* Substitute %s in the first chain by the second chain *) val subst_command_placeholder : string -> string -> string diff --git a/lib/fmap.ml b/lib/fmap.ml new file mode 100644 index 00000000..8ca56fe7 --- /dev/null +++ b/lib/fmap.ml @@ -0,0 +1,133 @@ + +module Make = functor (X:Map.OrderedType) -> struct + type key = X.t + type 'a t = + Empty + | Node of 'a t * key * 'a * 'a t * int + + let empty = Empty + + let is_empty = function Empty -> true | _ -> false + + let height = function + Empty -> 0 + | Node(_,_,_,_,h) -> h + + let create l x d r = + let hl = height l and hr = height r in + Node(l, x, d, r, (if hl >= hr then hl + 1 else hr + 1)) + + let bal l x d r = + let hl = match l with Empty -> 0 | Node(_,_,_,_,h) -> h in + let hr = match r with Empty -> 0 | Node(_,_,_,_,h) -> h in + if hl > hr + 2 then begin + match l with + Empty -> invalid_arg "Map.bal" + | Node(ll, lv, ld, lr, _) -> + if height ll >= height lr then + create ll lv ld (create lr x d r) + else begin + match lr with + Empty -> invalid_arg "Map.bal" + | Node(lrl, lrv, lrd, lrr, _)-> + create (create ll lv ld lrl) lrv lrd (create lrr x d r) + end + end else if hr > hl + 2 then begin + match r with + Empty -> invalid_arg "Map.bal" + | Node(rl, rv, rd, rr, _) -> + if height rr >= height rl then + create (create l x d rl) rv rd rr + else begin + match rl with + Empty -> invalid_arg "Map.bal" + | Node(rll, rlv, rld, rlr, _) -> + create (create l x d rll) rlv rld (create rlr rv rd rr) + end + end else + Node(l, x, d, r, (if hl >= hr then hl + 1 else hr + 1)) + + let rec add x data = function + Empty -> + Node(Empty, x, data, Empty, 1) + | Node(l, v, d, r, h) -> + let c = X.compare x v in + if c = 0 then + Node(l, x, data, r, h) + else if c < 0 then + bal (add x data l) v d r + else + bal l v d (add x data r) + + let rec find x = function + Empty -> + raise Not_found + | Node(l, v, d, r, _) -> + let c = X.compare x v in + if c = 0 then d + else find x (if c < 0 then l else r) + + let rec mem x = function + Empty -> + false + | Node(l, v, d, r, _) -> + let c = X.compare x v in + c = 0 || mem x (if c < 0 then l else r) + + let rec min_binding = function + Empty -> raise Not_found + | Node(Empty, x, d, r, _) -> (x, d) + | Node(l, x, d, r, _) -> min_binding l + + let rec remove_min_binding = function + Empty -> invalid_arg "Map.remove_min_elt" + | Node(Empty, x, d, r, _) -> r + | Node(l, x, d, r, _) -> bal (remove_min_binding l) x d r + + let merge t1 t2 = + match (t1, t2) with + (Empty, t) -> t + | (t, Empty) -> t + | (_, _) -> + let (x, d) = min_binding t2 in + bal t1 x d (remove_min_binding t2) + + let rec remove x = function + Empty -> + Empty + | Node(l, v, d, r, h) -> + let c = X.compare x v in + if c = 0 then + merge l r + else if c < 0 then + bal (remove x l) v d r + else + bal l v d (remove x r) + + let rec iter f = function + Empty -> () + | Node(l, v, d, r, _) -> + iter f l; f v d; iter f r + + let rec map f = function + Empty -> Empty + | Node(l, v, d, r, h) -> Node(map f l, v, f d, map f r, h) + + (* Maintien de fold_right par compatibilité (changé en fold_left dans + ocaml-3.09.0) *) + + let rec fold f m accu = + match m with + Empty -> accu + | Node(l, v, d, r, _) -> + fold f l (f v d (fold f r accu)) + +(* Added with respect to ocaml standard library. *) + + let dom m = fold (fun x _ acc -> x::acc) m [] + + let rng m = fold (fun _ y acc -> y::acc) m [] + + let to_list m = fold (fun x y acc -> (x,y)::acc) m [] + +end diff --git a/lib/fmap.mli b/lib/fmap.mli new file mode 100644 index 00000000..c323b055 --- /dev/null +++ b/lib/fmap.mli @@ -0,0 +1,23 @@ + +module Make : functor (X : Map.OrderedType) -> +sig + type key = X.t + type 'a t + +val empty : 'a t +val is_empty : 'a t -> bool +val add : key -> 'a -> 'a t -> 'a t +val find : key -> 'a t -> 'a +val remove : key -> 'a t -> 'a t +val mem : key -> 'a t -> bool +val iter : (key -> 'a -> unit) -> 'a t -> unit +val map : ('a -> 'b) -> 'a t -> 'b t +val fold : (key -> 'a -> 'c -> 'c) -> 'a t -> 'c -> 'c + +(* Additions with respect to ocaml standard library. *) + +val dom : 'a t -> key list +val rng : 'a t -> 'a list +val to_list : 'a t -> (key * 'a) list +end + diff --git a/lib/fset.ml b/lib/fset.ml new file mode 100644 index 00000000..567feaa7 --- /dev/null +++ b/lib/fset.ml @@ -0,0 +1,235 @@ +module Make = functor (X : Set.OrderedType) -> +struct + + type elt = X.t + type t = Empty | Node of t * elt * t * int + + + (* Sets are represented by balanced binary trees (the heights of the + children differ by at most 2 *) + + let height = function + Empty -> 0 + | Node(_, _, _, h) -> h + + (* Creates a new node with left son l, value x and right son r. + l and r must be balanced and | height l - height r | <= 2. + Inline expansion of height for better speed. *) + + let create l x r = + let hl = match l with Empty -> 0 | Node(_,_,_,h) -> h in + let hr = match r with Empty -> 0 | Node(_,_,_,h) -> h in + Node(l, x, r, (if hl >= hr then hl + 1 else hr + 1)) + + (* Same as create, but performs one step of rebalancing if necessary. + Assumes l and r balanced. + Inline expansion of create for better speed in the most frequent case + where no rebalancing is required. *) + + let bal l x r = + let hl = match l with Empty -> 0 | Node(_,_,_,h) -> h in + let hr = match r with Empty -> 0 | Node(_,_,_,h) -> h in + if hl > hr + 2 then begin + match l with + Empty -> invalid_arg "Set.bal" + | Node(ll, lv, lr, _) -> + if height ll >= height lr then + create ll lv (create lr x r) + else begin + match lr with + Empty -> invalid_arg "Set.bal" + | Node(lrl, lrv, lrr, _)-> + create (create ll lv lrl) lrv (create lrr x r) + end + end else if hr > hl + 2 then begin + match r with + Empty -> invalid_arg "Set.bal" + | Node(rl, rv, rr, _) -> + if height rr >= height rl then + create (create l x rl) rv rr + else begin + match rl with + Empty -> invalid_arg "Set.bal" + | Node(rll, rlv, rlr, _) -> + create (create l x rll) rlv (create rlr rv rr) + end + end else + Node(l, x, r, (if hl >= hr then hl + 1 else hr + 1)) + + (* Same as bal, but repeat rebalancing until the final result + is balanced. *) + + let rec join l x r = + match bal l x r with + Empty -> invalid_arg "Set.join" + | Node(l', x', r', _) as t' -> + let d = height l' - height r' in + if d < -2 or d > 2 then join l' x' r' else t' + + (* Merge two trees l and r into one. + All elements of l must precede the elements of r. + Assumes | height l - height r | <= 2. *) + + let rec merge t1 t2 = + match (t1, t2) with + (Empty, t) -> t + | (t, Empty) -> t + | (Node(l1, v1, r1, h1), Node(l2, v2, r2, h2)) -> + bal l1 v1 (bal (merge r1 l2) v2 r2) + + (* Same as merge, but does not assume anything about l and r. *) + + let rec concat t1 t2 = + match (t1, t2) with + (Empty, t) -> t + | (t, Empty) -> t + | (Node(l1, v1, r1, h1), Node(l2, v2, r2, h2)) -> + join l1 v1 (join (concat r1 l2) v2 r2) + + (* Splitting *) + + let rec split x = function + Empty -> + (Empty, None, Empty) + | Node(l, v, r, _) -> + let c = X.compare x v in + if c = 0 then (l, Some v, r) + else if c < 0 then + let (ll, vl, rl) = split x l in (ll, vl, join rl v r) + else + let (lr, vr, rr) = split x r in (join l v lr, vr, rr) + + (* Implementation of the set operations *) + + let empty = Empty + + let is_empty = function Empty -> true | _ -> false + + let rec mem x = function + Empty -> false + | Node(l, v, r, _) -> + let c = X.compare x v in + c = 0 || mem x (if c < 0 then l else r) + + let rec add x = function + Empty -> Node(Empty, x, Empty, 1) + | Node(l, v, r, _) as t -> + let c = X.compare x v in + if c = 0 then t else + if c < 0 then bal (add x l) v r else bal l v (add x r) + + let singleton x = Node(Empty, x, Empty, 1) + + let rec remove x = function + Empty -> Empty + | Node(l, v, r, _) -> + let c = X.compare x v in + if c = 0 then merge l r else + if c < 0 then bal (remove x l) v r else bal l v (remove x r) + + let rec union s1 s2 = + match (s1, s2) with + (Empty, t2) -> t2 + | (t1, Empty) -> t1 + | (Node(l1, v1, r1, h1), Node(l2, v2, r2, h2)) -> + if h1 >= h2 then + if h2 = 1 then add v2 s1 else begin + let (l2, _, r2) = split v1 s2 in + join (union l1 l2) v1 (union r1 r2) + end + else + if h1 = 1 then add v1 s2 else begin + let (l1, _, r1) = split v2 s1 in + join (union l1 l2) v2 (union r1 r2) + end + + let rec inter s1 s2 = + match (s1, s2) with + (Empty, t2) -> Empty + | (t1, Empty) -> Empty + | (Node(l1, v1, r1, _), t2) -> + match split v1 t2 with + (l2, None, r2) -> + concat (inter l1 l2) (inter r1 r2) + | (l2, Some _, r2) -> + join (inter l1 l2) v1 (inter r1 r2) + + let rec diff s1 s2 = + match (s1, s2) with + (Empty, t2) -> Empty + | (t1, Empty) -> t1 + | (Node(l1, v1, r1, _), t2) -> + match split v1 t2 with + (l2, None, r2) -> + join (diff l1 l2) v1 (diff r1 r2) + | (l2, Some _, r2) -> + concat (diff l1 l2) (diff r1 r2) + + let rec compare_aux l1 l2 = + match (l1, l2) with + ([], []) -> 0 + | ([], _) -> -1 + | (_, []) -> 1 + | (Empty :: t1, Empty :: t2) -> + compare_aux t1 t2 + | (Node(Empty, v1, r1, _) :: t1, Node(Empty, v2, r2, _) :: t2) -> + let c = compare v1 v2 in + if c <> 0 then c else compare_aux (r1::t1) (r2::t2) + | (Node(l1, v1, r1, _) :: t1, t2) -> + compare_aux (l1 :: Node(Empty, v1, r1, 0) :: t1) t2 + | (t1, Node(l2, v2, r2, _) :: t2) -> + compare_aux t1 (l2 :: Node(Empty, v2, r2, 0) :: t2) + + let compare s1 s2 = + compare_aux [s1] [s2] + + let equal s1 s2 = + compare s1 s2 = 0 + + let rec subset s1 s2 = + match (s1, s2) with + Empty, _ -> + true + | _, Empty -> + false + | Node (l1, v1, r1, _), (Node (l2, v2, r2, _) as t2) -> + let c = X.compare v1 v2 in + if c = 0 then + subset l1 l2 && subset r1 r2 + else if c < 0 then + subset (Node (l1, v1, Empty, 0)) l2 && subset r1 t2 + else + subset (Node (Empty, v1, r1, 0)) r2 && subset l1 t2 + + let rec iter f = function + Empty -> () + | Node(l, v, r, _) -> iter f l; f v; iter f r + + let rec fold f s accu = + match s with + Empty -> accu + | Node(l, v, r, _) -> fold f l (f v (fold f r accu)) + + let rec cardinal = function + Empty -> 0 + | Node(l, v, r, _) -> cardinal l + 1 + cardinal r + + let rec elements_aux accu = function + Empty -> accu + | Node(l, v, r, _) -> elements_aux (v :: elements_aux accu r) l + + let elements s = + elements_aux [] s + + let rec min_elt = function + Empty -> raise Not_found + | Node(Empty, v, r, _) -> v + | Node(l, v, r, _) -> min_elt l + + let rec max_elt = function + Empty -> raise Not_found + | Node(l, v, Empty, _) -> v + | Node(l, v, r, _) -> max_elt r + + let choose = min_elt +end diff --git a/lib/fset.mli b/lib/fset.mli new file mode 100644 index 00000000..b1751d0b --- /dev/null +++ b/lib/fset.mli @@ -0,0 +1,25 @@ +module Make : functor (X : Set.OrderedType) -> +sig + type elt = X.t + type t + +val empty : t +val is_empty : t -> bool +val mem : elt -> t -> bool +val add : elt -> t -> t +val singleton : elt -> t +val remove : elt -> t -> t +val union : t -> t -> t +val inter : t -> t -> t +val diff : t -> t -> t +val compare : t -> t -> int +val equal : t -> t -> bool +val subset : t -> t -> bool +val iter : ( elt -> unit) -> t -> unit +val fold : (elt -> 'b -> 'b) -> t -> 'b -> 'b +val cardinal : t -> int +val elements : t -> elt list +val min_elt : t -> elt +val max_elt : t -> elt +val choose : t -> elt +end diff --git a/lib/gmap.ml b/lib/gmap.ml index 7a4cb56e..0c498fe7 100644 --- a/lib/gmap.ml +++ b/lib/gmap.ml @@ -5,7 +5,7 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: gmap.ml 10250 2007-10-23 15:02:23Z aspiwack $ *) +(* $Id$ *) (* Maps using the generic comparison function of ocaml. Code borrowed from the ocaml standard library (Copyright 1996, INRIA). *) diff --git a/lib/gmap.mli b/lib/gmap.mli index 5186cff4..ac1a9922 100644 --- a/lib/gmap.mli +++ b/lib/gmap.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: gmap.mli 10250 2007-10-23 15:02:23Z aspiwack $ i*) +(*i $Id$ i*) (* Maps using the generic comparison function of ocaml. Same interface as the module [Map] from the ocaml standard library. *) diff --git a/lib/gmapl.ml b/lib/gmapl.ml index 0974909d..cec10d64 100644 --- a/lib/gmapl.ml +++ b/lib/gmapl.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: gmapl.ml 7780 2006-01-03 20:33:53Z herbelin $ *) +(* $Id$ *) open Util @@ -32,4 +32,4 @@ let remove x y m = let l = Gmap.find x m in Gmap.add x (if List.mem y l then list_subtract l [y] else l) m - + diff --git a/lib/gmapl.mli b/lib/gmapl.mli index db8f4358..5a5c9a2a 100644 --- a/lib/gmapl.mli +++ b/lib/gmapl.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: gmapl.mli 5920 2004-07-16 20:01:26Z herbelin $ i*) +(*i $Id$ i*) (* Maps from ['a] to lists of ['b]. *) diff --git a/lib/gset.ml b/lib/gset.ml index e90386a0..d39cb23f 100644 --- a/lib/gset.ml +++ b/lib/gset.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: gset.ml 5920 2004-07-16 20:01:26Z herbelin $ *) +(* $Id$ *) (* Sets using the generic comparison function of ocaml. Code borrowed from the ocaml standard library. *) diff --git a/lib/gset.mli b/lib/gset.mli index 5c794381..78fc61e1 100644 --- a/lib/gset.mli +++ b/lib/gset.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: gset.mli 10840 2008-04-23 21:29:34Z herbelin $ i*) +(*i $Id$ i*) (* Sets using the generic comparison function of ocaml. Same interface as the module [Set] from the ocaml standard library. *) diff --git a/lib/hashcons.ml b/lib/hashcons.ml index 50be0ec4..921a4ed5 100644 --- a/lib/hashcons.ml +++ b/lib/hashcons.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: hashcons.ml 5920 2004-07-16 20:01:26Z herbelin $ *) +(* $Id$ *) (* Hash consing of datastructures *) @@ -19,7 +19,7 @@ * the hash-consing functions u provides. * [equal] is a comparison function. It is allowed to use physical equality * on the sub-terms hash-consed by the hash_sub function. - * [hash] is the hash function given to the Hashtbl.Make function + * [hash] is the hash function given to the Hashtbl.Make function * * Note that this module type coerces to the argument of Hashtbl.Make. *) @@ -106,7 +106,7 @@ let recursive_loop_hcons h u = let rec hrec visited x = if List.memq x visited then x else hc (hrec (x::visited),u) x - in + in hrec [] (* For 2 mutually recursive types *) @@ -164,7 +164,7 @@ let comp_obj o1 o2 = else false else o1=o2 -let hash_obj hrec o = +let hash_obj hrec o = begin if tuple_p o then let n = Obj.size o in diff --git a/lib/hashcons.mli b/lib/hashcons.mli index f1e55ba1..243368d0 100644 --- a/lib/hashcons.mli +++ b/lib/hashcons.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: hashcons.mli 5920 2004-07-16 20:01:26Z herbelin $ i*) +(*i $Id$ i*) (* Generic hash-consing. *) diff --git a/lib/heap.ml b/lib/heap.ml index 92aa0070..7ddb4a72 100644 --- a/lib/heap.ml +++ b/lib/heap.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: heap.ml 5920 2004-07-16 20:01:26Z herbelin $ *) +(* $Id$ *) (*s Heaps *) @@ -16,35 +16,35 @@ module type Ordered = sig end module type S =sig - + (* Type of functional heaps *) type t (* Type of elements *) type elt - + (* The empty heap *) val empty : t - + (* [add x h] returns a new heap containing the elements of [h], plus [x]; complexity $O(log(n))$ *) val add : elt -> t -> t - + (* [maximum h] returns the maximum element of [h]; raises [EmptyHeap] when [h] is empty; complexity $O(1)$ *) val maximum : t -> elt - + (* [remove h] returns a new heap containing the elements of [h], except - the maximum of [h]; raises [EmptyHeap] when [h] is empty; - complexity $O(log(n))$ *) + the maximum of [h]; raises [EmptyHeap] when [h] is empty; + complexity $O(log(n))$ *) val remove : t -> t - + (* usual iterators and combinators; elements are presented in arbitrary order *) val iter : (elt -> unit) -> t -> unit - + val fold : (elt -> 'a -> 'a) -> t -> 'a -> 'a - + end exception EmptyHeap @@ -54,9 +54,9 @@ exception EmptyHeap module Functional(X : Ordered) = struct (* Heaps are encoded as complete binary trees, i.e., binary trees - which are full expect, may be, on the bottom level where it is filled - from the left. - These trees also enjoy the heap property, namely the value of any node + which are full expect, may be, on the bottom level where it is filled + from the left. + These trees also enjoy the heap property, namely the value of any node is greater or equal than those of its left and right subtrees. There are 4 kinds of complete binary trees, denoted by 4 constructors: @@ -68,7 +68,7 @@ module Functional(X : Ordered) = struct and [PFP] for a partial tree with a full left subtree and a partial right subtree. *) - type t = + type t = | Empty | FFF of t * X.t * t (* full (full, full) *) | PPF of t * X.t * t (* partial (partial, full) *) @@ -78,7 +78,7 @@ module Functional(X : Ordered) = struct type elt = X.t let empty = Empty - + (* smart constructors for insertion *) let p_f l x r = match l with | Empty | FFF _ -> PFF (l, x, r) @@ -89,7 +89,7 @@ module Functional(X : Ordered) = struct | r -> PFP (l, x, r) let rec add x = function - | Empty -> + | Empty -> FFF (Empty, x, Empty) (* insertion to the left *) | FFF (l, y, r) | PPF (l, y, r) -> @@ -113,9 +113,9 @@ module Functional(X : Ordered) = struct | r -> PFP (l, x, r) let rec remove = function - | Empty -> + | Empty -> raise EmptyHeap - | FFF (Empty, _, Empty) -> + | FFF (Empty, _, Empty) -> Empty | PFF (l, _, Empty) -> l @@ -124,30 +124,30 @@ module Functional(X : Ordered) = struct let xl = maximum l in let xr = maximum r in let l' = remove l in - if X.compare xl xr >= 0 then - p_f l' xl r - else + if X.compare xl xr >= 0 then + p_f l' xl r + else p_f l' xr (add xl (remove r)) (* remove on the right *) | FFF (l, x, r) | PFP (l, x, r) -> let xl = maximum l in let xr = maximum r in let r' = remove r in - if X.compare xl xr > 0 then + if X.compare xl xr > 0 then pf_ (add xr (remove l)) xl r' - else + else pf_ l xr r' let rec iter f = function - | Empty -> + | Empty -> () - | FFF (l, x, r) | PPF (l, x, r) | PFF (l, x, r) | PFP (l, x, r) -> + | FFF (l, x, r) | PPF (l, x, r) | PFF (l, x, r) | PFP (l, x, r) -> iter f l; f x; iter f r let rec fold f h x0 = match h with - | Empty -> + | Empty -> x0 - | FFF (l, x, r) | PPF (l, x, r) | PFF (l, x, r) | PFP (l, x, r) -> + | FFF (l, x, r) | PPF (l, x, r) | PFF (l, x, r) | PFP (l, x, r) -> fold f l (fold f r (f x x0)) end diff --git a/lib/heap.mli b/lib/heap.mli index d351edd0..777e356d 100644 --- a/lib/heap.mli +++ b/lib/heap.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: heap.mli 6621 2005-01-21 17:24:37Z herbelin $ i*) +(*i $Id$ i*) (* Heaps *) @@ -16,35 +16,35 @@ module type Ordered = sig end module type S =sig - + (* Type of functional heaps *) type t (* Type of elements *) type elt - + (* The empty heap *) val empty : t - + (* [add x h] returns a new heap containing the elements of [h], plus [x]; complexity $O(log(n))$ *) val add : elt -> t -> t - + (* [maximum h] returns the maximum element of [h]; raises [EmptyHeap] when [h] is empty; complexity $O(1)$ *) val maximum : t -> elt - + (* [remove h] returns a new heap containing the elements of [h], except - the maximum of [h]; raises [EmptyHeap] when [h] is empty; - complexity $O(log(n))$ *) + the maximum of [h]; raises [EmptyHeap] when [h] is empty; + complexity $O(log(n))$ *) val remove : t -> t - + (* usual iterators and combinators; elements are presented in arbitrary order *) val iter : (elt -> unit) -> t -> unit - + val fold : (elt -> 'a -> 'a) -> t -> 'a -> 'a - + end exception EmptyHeap diff --git a/lib/lib.mllib b/lib/lib.mllib new file mode 100644 index 00000000..1743ce26 --- /dev/null +++ b/lib/lib.mllib @@ -0,0 +1,29 @@ +Pp_control +Pp +Compat +Flags +Segmenttree +Unicodetable +Util +Bigint +Hashcons +Dyn +System +Envars +Bstack +Edit +Gset +Gmap +Fset +Fmap +Tlm +tries +Gmapl +Profile +Explore +Predicate +Rtree +Heap +Option +Dnet + diff --git a/lib/option.ml b/lib/option.ml index 85efdd44..942fff48 100644 --- a/lib/option.ml +++ b/lib/option.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: option.ml 11576 2008-11-10 19:13:15Z msozeau $ i*) +(*i $Id$ i*) (** Module implementing basic combinators for OCaml option type. It tries follow closely the style of OCaml standard library. @@ -20,7 +20,7 @@ let has_some = function | None -> false | _ -> true - + exception IsNone (** [get x] returns [y] where [x] is [Some y]. It raises IsNone @@ -34,11 +34,11 @@ let make x = Some x (** [init b x] returns [Some x] if [b] is [true] and [None] otherwise. *) let init b x = - if b then + if b then Some x else None - + (** [flatten x] is [Some y] if [x] is [Some (Some y)] and [None] otherwise. *) let flatten = function @@ -48,7 +48,7 @@ let flatten = function (** {6 "Iterators"} ***) -(** [iter f x] executes [f y] if [x] equals [Some y]. It does nothing +(** [iter f x] executes [f y] if [x] equals [Some y]. It does nothing otherwise. *) let iter f = function | Some y -> f y @@ -60,7 +60,7 @@ exception Heterogeneous (** [iter2 f x y] executes [f z w] if [x] equals [Some z] and [y] equals [Some w]. It does nothing if both [x] and [y] are [None]. And raises [Heterogeneous] otherwise. *) -let iter2 f x y = +let iter2 f x y = match x,y with | Some z, Some w -> f z w | None,None -> () @@ -92,11 +92,17 @@ let fold_left2 f a x y = | _ -> raise Heterogeneous (** [fold_right f x a] is [f y a] if [x] is [Some y], and [a] otherwise. *) -let fold_right f x a = +let fold_right f x a = match x with | Some y -> f y a | _ -> a +(** [fold_map f a x] is [a, f y] if [x] is [Some y], and [a] otherwise. *) +let fold_map f a x = + match x with + | Some y -> let a, z = f a y in a, Some z + | _ -> a, None + (** [cata f a x] is [a] if [x] is [None] and [f y] if [x] is [Some y]. *) let cata f a = function | Some c -> f c @@ -112,20 +118,20 @@ let default a = function (** [lift f x] is the same as [map f x]. *) let lift = map -(** [lift_right f a x] is [Some (f a y)] if [x] is [Some y], and +(** [lift_right f a x] is [Some (f a y)] if [x] is [Some y], and [None] otherwise. *) let lift_right f a = function | Some y -> Some (f a y) | _ -> None -(** [lift_left f x a] is [Some (f y a)] if [x] is [Some y], and +(** [lift_left f x a] is [Some (f y a)] if [x] is [Some y], and [None] otherwise. *) let lift_left f x a = match x with | Some y -> Some (f y a) | _ -> None -(** [lift2 f x y] is [Some (f z w)] if [x] equals [Some z] and [y] equals +(** [lift2 f x y] is [Some (f z w)] if [x] equals [Some z] and [y] equals [Some w]. It is [None] otherwise. *) let lift2 f x y = match x,y with @@ -137,18 +143,18 @@ let lift2 f x y = (** {6 Operations with Lists} *) module List = - struct + struct (** [List.cons x l] equals [y::l] if [x] is [Some y] and [l] otherwise. *) let cons x l = match x with | Some y -> y::l | _ -> l - + (** [List.flatten l] is the list of all the [y]s such that [l] contains [Some y] (in the same order). *) let rec flatten = function | x::l -> cons x (flatten l) - | [] -> [] + | [] -> [] end @@ -157,8 +163,8 @@ end module Misc = struct - (** [Misc.compare f x y] lifts the equality predicate [f] to - option types. That is, if both [x] and [y] are [None] then + (** [Misc.compare f x y] lifts the equality predicate [f] to + option types. That is, if both [x] and [y] are [None] then it returns [true], if they are bothe [Some _] then [f] is called. Otherwise it returns [false]. *) let compare f x y = diff --git a/lib/option.mli b/lib/option.mli index 6fa89098..ef2e311a 100644 --- a/lib/option.mli +++ b/lib/option.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: option.mli 11576 2008-11-10 19:13:15Z msozeau $ *) +(* $Id$ *) (** Module implementing basic combinators for OCaml option type. It tries follow closely the style of OCaml standard library. @@ -18,7 +18,7 @@ (** [has_some x] is [true] if [x] is of the form [Some y] and [false] otherwise. *) val has_some : 'a option -> bool - + exception IsNone (** [get x] returns [y] where [x] is [Some y]. It raises IsNone @@ -37,7 +37,7 @@ val flatten : 'a option option -> 'a option (** {6 "Iterators"} ***) -(** [iter f x] executes [f y] if [x] equals [Some y]. It does nothing +(** [iter f x] executes [f y] if [x] equals [Some y]. It does nothing otherwise. *) val iter : ('a -> unit) -> 'a option -> unit @@ -66,6 +66,9 @@ val fold_left2 : ('a -> 'b -> 'c -> 'a) -> 'a -> 'b option -> 'c option -> 'a (** [fold_right f x a] is [f y a] if [x] is [Some y], and [a] otherwise. *) val fold_right : ('a -> 'b -> 'b) -> 'a option -> 'b -> 'b +(** [fold_map f a x] is [a, f y] if [x] is [Some y], and [a] otherwise. *) +val fold_map : ('a -> 'b -> 'a * 'c) -> 'a -> 'b option -> 'a * 'c option + (** [cata e f x] is [e] if [x] is [None] and [f a] if [x] is [Some a] *) val cata : ('a -> 'b) -> 'b -> 'a option -> 'b @@ -77,15 +80,15 @@ val default : 'a -> 'a option -> 'a (** [lift] is the same as {!map}. *) val lift : ('a -> 'b) -> 'a option -> 'b option -(** [lift_right f a x] is [Some (f a y)] if [x] is [Some y], and +(** [lift_right f a x] is [Some (f a y)] if [x] is [Some y], and [None] otherwise. *) val lift_right : ('a -> 'b -> 'c) -> 'a -> 'b option -> 'c option -(** [lift_left f x a] is [Some (f y a)] if [x] is [Some y], and +(** [lift_left f x a] is [Some (f y a)] if [x] is [Some y], and [None] otherwise. *) val lift_left : ('a -> 'b -> 'c) -> 'a option -> 'b -> 'c option -(** [lift2 f x y] is [Some (f z w)] if [x] equals [Some z] and [y] equals +(** [lift2 f x y] is [Some (f z w)] if [x] equals [Some z] and [y] equals [Some w]. It is [None] otherwise. *) val lift2 : ('a -> 'b -> 'c) -> 'a option -> 'b option -> 'c option @@ -105,8 +108,8 @@ end (** {6 Miscelaneous Primitives} *) module Misc : sig - (** [Misc.compare f x y] lifts the equality predicate [f] to - option types. That is, if both [x] and [y] are [None] then + (** [Misc.compare f x y] lifts the equality predicate [f] to + option types. That is, if both [x] and [y] are [None] then it returns [true], if they are bothe [Some _] then [f] is called. Otherwise it returns [false]. *) val compare : ('a -> 'a -> bool) -> 'a option -> 'a option -> bool @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: pp.ml4 10803 2008-04-16 09:30:05Z cek $ *) +(* $Id$ *) open Pp_control @@ -19,7 +19,7 @@ let print_emacs = ref false let make_pp_emacs() = print_emacs:=true let make_pp_nonemacs() = print_emacs:=false -(* The different kinds of blocks are: +(* The different kinds of blocks are: \begin{description} \item[hbox:] Horizontal block no line breaking; \item[vbox:] Vertical block each break leads to a new line; @@ -31,9 +31,9 @@ let make_pp_nonemacs() = print_emacs:=false (except if no mark yet on the reste of the line) \end{description} *) - + let comments = ref [] - + let rec split_com comacc acc pos = function [] -> comments := List.rev acc; comacc | ((b,e),c as com)::coms -> @@ -132,7 +132,7 @@ let real r = str (string_of_float r) let bool b = str (string_of_bool b) let strbrk s = let rec aux p n = - if n < String.length s then + if n < String.length s then if s.[n] = ' ' then if p=n then [< spc (); aux (n+1) (n+1) >] else [< str (String.sub s p (n-p)); spc (); aux (n+1) (n+1) >] @@ -224,13 +224,13 @@ let rec pr_com ft s = | None -> () (* pretty printing functions *) -let pp_dirs ft = +let pp_dirs ft = let pp_open_box = function | Pp_hbox n -> Format.pp_open_hbox ft () | Pp_vbox n -> Format.pp_open_vbox ft n | Pp_hvbox n -> Format.pp_open_hvbox ft n | Pp_hovbox n -> Format.pp_open_hovbox ft n - | Pp_tbox -> Format.pp_open_tbox ft () + | Pp_tbox -> Format.pp_open_tbox ft () in let rec pp_cmd = function | Ppcmd_print(n,s) -> @@ -264,12 +264,12 @@ let pp_dirs ft = | Ppdir_ppcmds cmdstream -> Stream.iter pp_cmd cmdstream | Ppdir_print_newline -> com_brk ft; Format.pp_print_newline ft () - | Ppdir_print_flush -> Format.pp_print_flush ft () + | Ppdir_print_flush -> Format.pp_print_flush ft () in fun dirstream -> - try + try Stream.iter pp_dir dirstream; com_brk ft - with + with | e -> Format.pp_print_flush ft () ; raise e @@ -284,10 +284,10 @@ let ppcmds x = Ppdir_ppcmds x let emacs_warning_start_string = String.make 1 (Char.chr 254) let emacs_warning_end_string = String.make 1 (Char.chr 255) -let warnstart() = +let warnstart() = if not !print_emacs then mt() else str emacs_warning_start_string -let warnend() = +let warnend() = if not !print_emacs then mt() else str emacs_warning_end_string let warnbody strm = @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: pp.mli 10803 2008-04-16 09:30:05Z cek $ i*) +(*i $Id$ i*) (*i*) open Pp_control @@ -85,7 +85,7 @@ val warning_with : Format.formatter -> string -> unit val warn_with : Format.formatter -> std_ppcmds -> unit val pp_flush_with : Format.formatter -> unit -> unit -val set_warning_function : (Format.formatter -> std_ppcmds -> unit) -> unit +val set_warning_function : (Format.formatter -> std_ppcmds -> unit) -> unit (*s Pretty-printing functions \emph{with flush}. *) diff --git a/lib/pp_control.ml b/lib/pp_control.ml index 7aa05975..ecc54649 100644 --- a/lib/pp_control.ml +++ b/lib/pp_control.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: pp_control.ml 10917 2008-05-10 16:35:46Z herbelin $ *) +(* $Id$ *) (* Parameters of pretty-printing *) @@ -18,7 +18,7 @@ type pp_global_params = { (* Default parameters of pretty-printing *) -let dflt_gp = { +let dflt_gp = { margin = 78; max_indent = 50; max_depth = 50; @@ -26,7 +26,7 @@ let dflt_gp = { (* A deeper pretty-printer to print proof scripts *) -let deep_gp = { +let deep_gp = { margin = 78; max_indent = 50; max_depth = 10000; @@ -35,13 +35,13 @@ let deep_gp = { (* set_gp : Format.formatter -> pp_global_params -> unit * set the parameters of a formatter *) -let set_gp ft gp = +let set_gp ft gp = Format.pp_set_margin ft gp.margin ; Format.pp_set_max_indent ft gp.max_indent ; Format.pp_set_max_boxes ft gp.max_depth ; Format.pp_set_ellipsis_text ft gp.ellipsis -let set_dflt_gp ft = set_gp ft dflt_gp +let set_dflt_gp ft = set_gp ft dflt_gp let get_gp ft = { margin = Format.pp_get_margin ft (); @@ -56,7 +56,7 @@ type 'a pp_formatter_params = { fp_output : out_channel ; fp_output_function : string -> int -> int -> unit ; fp_flush_function : unit -> unit } - + (* Output functions for stdout and stderr *) let std_fp = { @@ -69,7 +69,7 @@ let err_fp = { fp_output_function = output stderr; fp_flush_function = (fun () -> flush stderr) } -(* with_fp : 'a pp_formatter_params -> Format.formatter +(* with_fp : 'a pp_formatter_params -> Format.formatter * returns of formatter for given formatter functions *) let with_fp fp = @@ -83,7 +83,7 @@ let with_output_to ch = let ft = with_fp { fp_output = ch ; fp_output_function = (output ch) ; fp_flush_function = (fun () -> flush ch) } in - set_gp ft deep_gp; + set_gp ft deep_gp; ft let std_ft = ref Format.std_formatter @@ -105,5 +105,7 @@ let set_depth_boxes v = let get_margin () = Some (Format.pp_get_margin !std_ft ()) let set_margin v = - Format.pp_set_margin !std_ft (match v with None -> default_margin | Some v -> v) + let v = match v with None -> default_margin | Some v -> v in + Format.pp_set_margin !std_ft v; + Format.pp_set_margin !deep_ft v diff --git a/lib/pp_control.mli b/lib/pp_control.mli index f245d942..5c481b89 100644 --- a/lib/pp_control.mli +++ b/lib/pp_control.mli @@ -6,11 +6,11 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: pp_control.mli 10917 2008-05-10 16:35:46Z herbelin $ i*) +(*i $Id$ i*) (* Parameters of pretty-printing. *) -type pp_global_params = { +type pp_global_params = { margin : int; max_indent : int; max_depth : int; @@ -25,7 +25,7 @@ val get_gp : Format.formatter -> pp_global_params (*s Output functions of pretty-printing. *) -type 'a pp_formatter_params = { +type 'a pp_formatter_params = { fp_output : out_channel; fp_output_function : string -> int -> int -> unit; fp_flush_function : unit -> unit } diff --git a/lib/predicate.ml b/lib/predicate.ml index 93b74463..af66c0f2 100644 --- a/lib/predicate.ml +++ b/lib/predicate.ml @@ -10,7 +10,7 @@ (* *) (************************************************************************) -(* $Id: predicate.ml 5920 2004-07-16 20:01:26Z herbelin $ *) +(* $Id$ *) (* Sets over ordered types *) @@ -44,7 +44,7 @@ module type S = module Make(Ord: OrderedType) = struct module EltSet = Set.Make(Ord) - + (* when bool is false, the denoted set is the complement of the given set *) type elt = Ord.t diff --git a/lib/predicate.mli b/lib/predicate.mli index 85596fea..41d5399b 100644 --- a/lib/predicate.mli +++ b/lib/predicate.mli @@ -1,5 +1,5 @@ -(*i $Id: predicate.mli 6621 2005-01-21 17:24:37Z herbelin $ i*) +(*i $Id$ i*) (* Module [Pred]: sets over infinite ordered types with complement. *) diff --git a/lib/profile.ml b/lib/profile.ml index dd7e977e..7bf71d0b 100644 --- a/lib/profile.ml +++ b/lib/profile.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: profile.ml 7538 2005-11-08 17:14:52Z herbelin $ *) +(* $Id$ *) open Gc @@ -17,8 +17,7 @@ let float_of_time t = float_of_int t /. 100. let time_of_float f = int_of_float (f *. 100.) let get_time () = - let {Unix.tms_utime = ut;Unix.tms_stime = st} = Unix.times () in - time_of_float (ut +. st) + time_of_float (Sys.time ()) (* Since ocaml 3.01, gc statistics are in float *) let get_alloc () = @@ -113,12 +112,12 @@ let ajoute_to_list ((name,n) as e) l = with Not_found -> e::l let magic = 1249 - + let merge_profile filename (curr_table, curr_outside, curr_total as new_data) = let (old_table, old_outside, old_total) = - try + try let c = open_in filename in - if input_binary_int c <> magic + if input_binary_int c <> magic then Printf.printf "Incompatible recording file: %s\n" filename; let old_data = input_value c in close_in c; @@ -134,7 +133,7 @@ let merge_profile filename (curr_table, curr_outside, curr_total as new_data) = begin (try let c = - open_out_gen + open_out_gen [Open_creat;Open_wronly;Open_trunc;Open_binary] 0o644 filename in output_binary_int c magic; output_value c updated_data; @@ -157,7 +156,10 @@ let merge_profile filename (curr_table, curr_outside, curr_total as new_data) = (* Unix measure of time is approximative and shoitt delays are often unperceivable; therefore, total times are measured in one (big) step to avoid rounding errors and to get the best possible - approximation *) + approximation. + Note: Sys.time is the same as: + Unix.(let x = times () in x.tms_utime +. x.tms_stime) + *) (* ---------- start profile for f1 @@ -186,7 +188,7 @@ overheadA| ... real 2' | ... ---------- end 2nd f2 overheadC| ... - ---------- [2'w2] 2nd call to get_time for 2nd f2 + ---------- [2'w2] 2nd call to get_time for 2nd f2 overheadD| ... ---------- end profile for f2 real 1 | ... @@ -242,7 +244,7 @@ let time_overhead_A_D () = ajoute_totalloc p (e.totalloc-.totalloc0); p.intcount <- p.intcount + e.intcount - intcount0 + 1; p.immcount <- p.immcount + 1; - if not (p==e) then + if not (p==e) then (match !dummy_stack with [] -> assert false | _::s -> stack := s); dummy_last_alloc := get_alloc () done; @@ -279,7 +281,7 @@ let compute_alloc lo = lo /. (float_of_int word_length) let format_profile (table, outside, total) = print_newline (); - Printf.printf + Printf.printf "%-23s %9s %9s %10s %10s %10s\n" "Function name" "Own time" "Tot. time" "Own alloc" "Tot. alloc" "Calls "; let l = Sort.list (fun (_,{tottime=p}) (_,{tottime=p'}) -> p > p') table in @@ -293,7 +295,7 @@ let format_profile (table, outside, total) = e.owncount e.intcount) l; Printf.printf "%-23s %9.2f %9.2f %10.0f %10.0f %6d\n" - "others" + "others" (float_of_time outside.owntime) (float_of_time outside.tottime) (compute_alloc outside.ownalloc) (compute_alloc outside.totalloc) @@ -305,7 +307,7 @@ let format_profile (table, outside, total) = (compute_alloc total.ownalloc) (compute_alloc total.totalloc); Printf.printf - "Time in seconds and allocation in words (1 word = %d bytes)\n" + "Time in seconds and allocation in words (1 word = %d bytes)\n" word_length let recording_file = ref "" @@ -319,7 +321,7 @@ let adjust_time ov_bc ov_ad e = tottime = e.tottime - int_of_float (abcd_all +. bc_imm); owntime = e.owntime - int_of_float (ad_imm +. bc_imm) } -let close_profile print = +let close_profile print = let dw = spent_alloc () in let t = get_time () in match !stack with @@ -390,7 +392,7 @@ let profile1 e f a = ajoute_totalloc p (e.totalloc -. totalloc0); p.intcount <- p.intcount + e.intcount - intcount0 + 1; p.immcount <- p.immcount + 1; - if not (p==e) then + if not (p==e) then (match !stack with [] -> assert false | _::s -> stack := s); last_alloc := get_alloc (); r @@ -404,7 +406,7 @@ let profile1 e f a = ajoute_totalloc p (e.totalloc -. totalloc0); p.intcount <- p.intcount + e.intcount - intcount0 + 1; p.immcount <- p.immcount + 1; - if not (p==e) then + if not (p==e) then (match !stack with [] -> assert false | _::s -> stack := s); last_alloc := get_alloc (); raise exn @@ -432,7 +434,7 @@ let profile2 e f a b = ajoute_totalloc p (e.totalloc -. totalloc0); p.intcount <- p.intcount + e.intcount - intcount0 + 1; p.immcount <- p.immcount + 1; - if not (p==e) then + if not (p==e) then (match !stack with [] -> assert false | _::s -> stack := s); last_alloc := get_alloc (); r @@ -446,7 +448,7 @@ let profile2 e f a b = ajoute_totalloc p (e.totalloc -. totalloc0); p.intcount <- p.intcount + e.intcount - intcount0 + 1; p.immcount <- p.immcount + 1; - if not (p==e) then + if not (p==e) then (match !stack with [] -> assert false | _::s -> stack := s); last_alloc := get_alloc (); raise exn @@ -474,7 +476,7 @@ let profile3 e f a b c = ajoute_totalloc p (e.totalloc -. totalloc0); p.intcount <- p.intcount + e.intcount - intcount0 + 1; p.immcount <- p.immcount + 1; - if not (p==e) then + if not (p==e) then (match !stack with [] -> assert false | _::s -> stack := s); last_alloc := get_alloc (); r @@ -488,7 +490,7 @@ let profile3 e f a b c = ajoute_totalloc p (e.totalloc -. totalloc0); p.intcount <- p.intcount + e.intcount - intcount0 + 1; p.immcount <- p.immcount + 1; - if not (p==e) then + if not (p==e) then (match !stack with [] -> assert false | _::s -> stack := s); last_alloc := get_alloc (); raise exn @@ -516,7 +518,7 @@ let profile4 e f a b c d = ajoute_totalloc p (e.totalloc -. totalloc0); p.intcount <- p.intcount + e.intcount - intcount0 + 1; p.immcount <- p.immcount + 1; - if not (p==e) then + if not (p==e) then (match !stack with [] -> assert false | _::s -> stack := s); last_alloc := get_alloc (); r @@ -530,7 +532,7 @@ let profile4 e f a b c d = ajoute_totalloc p (e.totalloc -. totalloc0); p.intcount <- p.intcount + e.intcount - intcount0 + 1; p.immcount <- p.immcount + 1; - if not (p==e) then + if not (p==e) then (match !stack with [] -> assert false | _::s -> stack := s); last_alloc := get_alloc (); raise exn @@ -558,7 +560,7 @@ let profile5 e f a b c d g = ajoute_totalloc p (e.totalloc -. totalloc0); p.intcount <- p.intcount + e.intcount - intcount0 + 1; p.immcount <- p.immcount + 1; - if not (p==e) then + if not (p==e) then (match !stack with [] -> assert false | _::s -> stack := s); last_alloc := get_alloc (); r @@ -572,7 +574,7 @@ let profile5 e f a b c d g = ajoute_totalloc p (e.totalloc -. totalloc0); p.intcount <- p.intcount + e.intcount - intcount0 + 1; p.immcount <- p.immcount + 1; - if not (p==e) then + if not (p==e) then (match !stack with [] -> assert false | _::s -> stack := s); last_alloc := get_alloc (); raise exn @@ -600,7 +602,7 @@ let profile6 e f a b c d g h = ajoute_totalloc p (e.totalloc -. totalloc0); p.intcount <- p.intcount + e.intcount - intcount0 + 1; p.immcount <- p.immcount + 1; - if not (p==e) then + if not (p==e) then (match !stack with [] -> assert false | _::s -> stack := s); last_alloc := get_alloc (); r @@ -614,7 +616,7 @@ let profile6 e f a b c d g h = ajoute_totalloc p (e.totalloc -. totalloc0); p.intcount <- p.intcount + e.intcount - intcount0 + 1; p.immcount <- p.immcount + 1; - if not (p==e) then + if not (p==e) then (match !stack with [] -> assert false | _::s -> stack := s); last_alloc := get_alloc (); raise exn @@ -642,7 +644,7 @@ let profile7 e f a b c d g h i = ajoute_totalloc p (e.totalloc -. totalloc0); p.intcount <- p.intcount + e.intcount - intcount0 + 1; p.immcount <- p.immcount + 1; - if not (p==e) then + if not (p==e) then (match !stack with [] -> assert false | _::s -> stack := s); last_alloc := get_alloc (); r @@ -656,7 +658,7 @@ let profile7 e f a b c d g h i = ajoute_totalloc p (e.totalloc -. totalloc0); p.intcount <- p.intcount + e.intcount - intcount0 + 1; p.immcount <- p.immcount + 1; - if not (p==e) then + if not (p==e) then (match !stack with [] -> assert false | _::s -> stack := s); last_alloc := get_alloc (); raise exn @@ -664,22 +666,20 @@ let profile7 e f a b c d g h i = (* Some utilities to compute the logical and physical sizes and depth of ML objects *) -open Obj - let c = ref 0 let s = ref 0 let b = ref 0 let m = ref 0 let rec obj_stats d t = - if is_int t then m := max d !m - else if tag t >= no_scan_tag then - if tag t = string_tag then - (c := !c + size t; b := !b + 1; m := max d !m) - else if tag t = double_tag then + if Obj.is_int t then m := max d !m + else if Obj.tag t >= Obj.no_scan_tag then + if Obj.tag t = Obj.string_tag then + (c := !c + Obj.size t; b := !b + 1; m := max d !m) + else if Obj.tag t = Obj.double_tag then (s := !s + 2; b := !b + 1; m := max d !m) - else if tag t = double_array_tag then - (s := !s + 2 * size t; b := !b + 1; m := max d !m) + else if Obj.tag t = Obj.double_array_tag then + (s := !s + 2 * Obj.size t; b := !b + 1; m := max d !m) else (b := !b + 1; m := max d !m) else let n = Obj.size t in @@ -687,7 +687,7 @@ let rec obj_stats d t = block_stats (d + 1) (n - 1) t and block_stats d i t = - if i >= 0 then (obj_stats d (field t i); block_stats d (i-1) t) + if i >= 0 then (obj_stats d (Obj.field t i); block_stats d (i-1) t) let obj_stats a = c := 0; s:= 0; b:= 0; m:= 0; @@ -695,24 +695,24 @@ let obj_stats a = (!c, !s + !b, !m) module H = Hashtbl.Make( - struct - type t = Obj.t - let equal = (==) - let hash o = Hashtbl.hash (magic o : int) + struct + type t = Obj.t + let equal = (==) + let hash o = Hashtbl.hash (Obj.magic o : int) end) let tbl = H.create 13 let rec obj_shared_size s t = - if is_int t then s + if Obj.is_int t then s else if H.mem tbl t then s else begin H.add tbl t (); let n = Obj.size t in - if tag t >= no_scan_tag then - if tag t = string_tag then (c := !c + n; s + 1) - else if tag t = double_tag then s + 3 - else if tag t = double_array_tag then s + 2 * n + 1 + if Obj.tag t >= Obj.no_scan_tag then + if Obj.tag t = Obj.string_tag then (c := !c + n; s + 1) + else if Obj.tag t = Obj.double_tag then s + 3 + else if Obj.tag t = Obj.double_array_tag then s + 2 * n + 1 else s + 1 else block_shared_size (s + n + 1) (n - 1) t @@ -720,7 +720,7 @@ let rec obj_shared_size s t = and block_shared_size s i t = if i < 0 then s - else block_shared_size (obj_shared_size s (field t i)) (i-1) t + else block_shared_size (obj_shared_size s (Obj.field t i)) (i-1) t let obj_shared_size a = H.clear tbl; diff --git a/lib/profile.mli b/lib/profile.mli index 0937e9e3..9466ad30 100644 --- a/lib/profile.mli +++ b/lib/profile.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: profile.mli 6621 2005-01-21 17:24:37Z herbelin $ i*) +(*i $Id$ i*) (*s This program is a small time and allocation profiler for Objective Caml *) @@ -14,8 +14,7 @@ (* Adapted from Christophe Raffalli *) -(* To use it, link it with the program you want to profile (do not forget -"-cclib -lunix -custom unix.cma" among the link options). +(* To use it, link it with the program you want to profile. To trace a function "f" you first need to get a key for it by using : @@ -49,7 +48,7 @@ let g = profile gkey g';; Before the program quits, you should call "print_profile ();;". It produces a result of the following kind: -Function name Own time Total time Own alloc Tot. alloc Calls +Function name Own time Total time Own alloc Tot. alloc Calls f 0.28 0.47 116 116 5 4 h 0.19 0.19 0 0 4 0 g 0.00 0.00 0 0 0 0 @@ -65,7 +64,7 @@ Est. overhead/total 0.00 0.47 2752 3260 the number of calls to profiled functions inside the scope of the current function -Remarks: +Remarks: - If a function has a polymorphic type, you need to supply it with at least one argument as in "let f a = profile1 fkey f a;;" (instead of @@ -103,7 +102,7 @@ val profile6 : -> 'a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g val profile7 : profile_key -> - ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h) + ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h) -> 'a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h diff --git a/lib/refutpat.ml4 b/lib/refutpat.ml4 new file mode 100644 index 00000000..7c6801a8 --- /dev/null +++ b/lib/refutpat.ml4 @@ -0,0 +1,33 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(*i camlp4use: "pa_extend.cmo q_MLast.cmo" i*) + +open Pcaml + +(** * Non-irrefutable patterns + + This small camlp4 extension creates a "let*" variant of the "let" + syntax that allow the use of a non-exhaustive pattern. The typical + usage is: + + let* x::l = foo in ... + + when foo is already known to be non-empty. This way, no warnings by ocamlc. + A Failure is raised if the pattern doesn't match the expression. +*) + + +EXTEND + expr: + [[ "let"; "*"; p = patt; "="; e1 = expr; "in"; e2 = expr -> + <:expr< match $e1$ with + [ $p$ -> $e2$ + | _ -> failwith "Refutable pattern failed" + ] >> ]]; +END diff --git a/lib/rtree.ml b/lib/rtree.ml index 4742a90d..ec50e556 100644 --- a/lib/rtree.ml +++ b/lib/rtree.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: rtree.ml 10690 2008-03-18 13:30:04Z barras $ i*) +(*i $Id$ i*) open Util @@ -53,7 +53,7 @@ let rec subst_rtree_rec depth sub = function let subst_rtree sub t = subst_rtree_rec 0 [|sub|] t -(* To avoid looping, we must check that every body introduces a node +(* To avoid looping, we must check that every body introduces a node or a parameter *) let rec expand = function | Rec(j,defs) -> @@ -81,17 +81,17 @@ the last one should be accepted *) (* Tree destructors, expanding loops when necessary *) -let dest_param t = +let dest_param t = match expand t with Param (i,j) -> (i,j) | _ -> failwith "Rtree.dest_param" -let dest_node t = +let dest_node t = match expand t with Node (l,sons) -> (l,sons) | _ -> failwith "Rtree.dest_node" -let is_node t = +let is_node t = match expand t with Node _ -> true | _ -> false @@ -104,13 +104,13 @@ let rec map f t = match t with let rec smartmap f t = match t with Param _ -> t - | Node (a,sons) -> + | Node (a,sons) -> let a'=f a and sons' = Util.array_smartmap (map f) sons in if a'==a && sons'==sons then t else Node (a',sons') - | Rec(j,defs) -> + | Rec(j,defs) -> let defs' = Util.array_smartmap (map f) defs in if defs'==defs then t @@ -175,11 +175,11 @@ let rec pp_tree prl t = | Node(lab,[||]) -> hov 2 (str"("++prl lab++str")") | Node(lab,v) -> hov 2 (str"("++prl lab++str","++brk(1,0)++ - Util.prvect_with_sep Util.pr_coma (pp_tree prl) v++str")") + Util.prvect_with_sep Util.pr_comma (pp_tree prl) v++str")") | Rec(i,v) -> if Array.length v = 0 then str"Rec{}" else if Array.length v = 1 then hov 2 (str"Rec{"++pp_tree prl v.(0)++str"}") else hov 2 (str"Rec{"++int i++str","++brk(1,0)++ - Util.prvect_with_sep Util.pr_coma (pp_tree prl) v++str"}") + Util.prvect_with_sep Util.pr_comma (pp_tree prl) v++str"}") diff --git a/lib/rtree.mli b/lib/rtree.mli index b61e6965..de5a9aa3 100644 --- a/lib/rtree.mli +++ b/lib/rtree.mli @@ -6,12 +6,12 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: rtree.mli 10690 2008-03-18 13:30:04Z barras $ i*) +(*i $Id$ i*) (* Type of regular tree with nodes labelled by values of type 'a *) (* The implementation uses de Bruijn indices, so binding capture is avoided by the lift operator (see example below) *) -type 'a t +type 'a t (* Building trees *) @@ -40,7 +40,7 @@ val mk_rec_calls : int -> 'a t array val mk_rec : 'a t array -> 'a t array (* [lift k t] increases of [k] the free parameters of [t]. Needed - to avoid captures when a tree appears under [mk_rec] *) + to avoid captures when a tree appears under [mk_rec] *) val lift : int -> 'a t -> 'a t val is_node : 'a t -> bool diff --git a/lib/segmenttree.ml b/lib/segmenttree.ml new file mode 100644 index 00000000..2a7f9df0 --- /dev/null +++ b/lib/segmenttree.ml @@ -0,0 +1,131 @@ +(** This module is a very simple implementation of "segment trees". + + A segment tree of type ['a t] represents a mapping from a union of + disjoint segments to some values of type 'a. +*) + +(** Misc. functions. *) +let list_iteri f l = + let rec loop i = function + | [] -> () + | x :: xs -> f i x; loop (i + 1) xs + in + loop 0 l + +let log2 x = log x /. log 2. + +let log2n x = int_of_float (ceil (log2 (float_of_int x))) + +(** We focus on integers but this module can be generalized. *) +type elt = int + +(** A value of type [domain] is interpreted differently given its position + in the tree. On internal nodes, a domain represents the set of + integers which are _not_ in the set of keys handled by the tree. On + leaves, a domain represents the st of integers which are in the set of + keys. *) +type domain = + (** On internal nodes, a domain [Interval (a, b)] represents + the interval [a + 1; b - 1]. On leaves, it represents [a; b]. + We always have [a] <= [b]. *) + | Interval of elt * elt + (** On internal node or root, a domain [Universe] represents all + the integers. When the tree is not a trivial root, + [Universe] has no interpretation on leaves. (The lookup + function should never reach the leaves.) *) + | Universe + +(** We use an array to store the almost complete tree. This array + contains at least one element. *) +type 'a t = (domain * 'a option) array + +(** The root is the first item of the array. *) +let is_root i = (i = 0) + +(** Standard layout for left child. *) +let left_child i = 2 * i + 1 + +(** Standard layout for right child. *) +let right_child i = 2 * i + 2 + +(** Extract the annotation of a node, be it internal or a leaf. *) +let value_of i t = match t.(i) with (_, Some x) -> x | _ -> raise Not_found + +(** Initialize the array to store [n] leaves. *) +let create n init = + Array.make (1 lsl (log2n n + 1) - 1) init + +(** Make a complete interval tree from a list of disjoint segments. + Precondition : the segments must be sorted. *) +let make segments = + let nsegments = List.length segments in + let tree = create nsegments (Universe, None) in + let leaves_offset = (1 lsl (log2n nsegments)) - 1 in + + (** The algorithm proceeds in two steps using an intermediate tree + to store minimum and maximum of each subtree as annotation of + the node. *) + + (** We start from leaves: the last level of the tree is initialized + with the given segments... *) + list_iteri + (fun i ((start, stop), value) -> + let k = leaves_offset + i in + let i = Interval (start, stop) in + tree.(k) <- (i, Some i)) + segments; + (** ... the remaining leaves are initialized with neutral information. *) + for k = leaves_offset + nsegments to Array.length tree -1 do + tree.(k) <- (Universe, Some Universe) + done; + + (** We traverse the tree bottom-up and compute the interval and + annotation associated to each node from the annotations of its + children. *) + for k = leaves_offset - 1 downto 0 do + let node, annotation = + match value_of (left_child k) tree, value_of (right_child k) tree with + | Interval (left_min, left_max), Interval (right_min, right_max) -> + (Interval (left_max, right_min), Interval (left_min, right_max)) + | Interval (min, max), Universe -> + (Interval (max, max), Interval (min, max)) + | Universe, Universe -> Universe, Universe + | Universe, _ -> assert false + in + tree.(k) <- (node, Some annotation) + done; + + (** Finally, annotation are replaced with the image related to each leaf. *) + let final_tree = + Array.mapi (fun i (segment, value) -> (segment, None)) tree + in + list_iteri + (fun i ((start, stop), value) -> + final_tree.(leaves_offset + i) + <- (Interval (start, stop), Some value)) + segments; + final_tree + +(** [lookup k t] looks for an image for key [k] in the interval tree [t]. + Raise [Not_found] if it fails. *) +let lookup k t = + let i = ref 0 in + while (snd t.(!i) = None) do + match fst t.(!i) with + | Interval (start, stop) -> + if k <= start then i := left_child !i + else if k >= stop then i:= right_child !i + else raise Not_found + | Universe -> raise Not_found + done; + match fst t.(!i) with + | Interval (start, stop) -> + if k >= start && k <= stop then + match snd t.(!i) with + | Some v -> v + | None -> assert false + else + raise Not_found + | Universe -> assert false + + diff --git a/lib/segmenttree.mli b/lib/segmenttree.mli new file mode 100644 index 00000000..4aea13e9 --- /dev/null +++ b/lib/segmenttree.mli @@ -0,0 +1,20 @@ +(** This module is a very simple implementation of "segment trees". + + A segment tree of type ['a t] represents a mapping from a union of + disjoint segments to some values of type 'a. +*) + +(** A mapping from a union of disjoint segments to some values of type ['a]. *) +type 'a t + +(** [make [(i1, j1), v1; (i2, j2), v2; ...] creates a mapping that + associates to every integer [x] the value [v1] if [i1 <= x <= j1], + [v2] if [i2 <= x <= j2], and so one. + Precondition: the segments must be sorted. *) +val make : ((int * int) * 'a) list -> 'a t + +(** [lookup k t] looks for an image for key [k] in the interval tree [t]. + Raise [Not_found] if it fails. *) +val lookup : int -> 'a t -> 'a + + diff --git a/lib/system.ml b/lib/system.ml index 3fa32ef8..6eb4e751 100644 --- a/lib/system.ml +++ b/lib/system.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: system.ml 13175 2010-06-22 06:28:37Z herbelin $ *) +(* $Id$ *) open Pp open Util @@ -15,7 +15,7 @@ open Unix (* Expanding shell variables and home-directories *) let safe_getenv_def var def = - try + try Sys.getenv var with Not_found -> warning ("Environment variable "^var^" not found: using '"^def^"' ."); @@ -38,7 +38,7 @@ let rec expand_macros s i = let l = String.length s in if i=l then s else match s.[i] with - | '$' -> + | '$' -> let n = expand_atom s (i+1) in let v = safe_getenv (String.sub s (i+1) (n-i-1)) in let s = (String.sub s 0 i)^v^(String.sub s n (l-n)) in @@ -64,7 +64,7 @@ let physical_path_of_string s = s let string_of_physical_path p = p (* Hints to partially detects if two paths refer to the same repertory *) -let rec remove_path_dot p = +let rec remove_path_dot p = let curdir = Filename.concat Filename.current_dir_name "" in (* Unix: "./" *) let n = String.length curdir in if String.length p > n && String.sub p 0 n = curdir then @@ -82,7 +82,7 @@ let strip_path p = let canonical_path_name p = let current = Sys.getcwd () in - try + try Sys.chdir p; let p' = Sys.getcwd () in Sys.chdir current; @@ -100,7 +100,7 @@ let skipped_dirnames = ref ["CVS"; "_darcs"] let exclude_search_in_dirname f = skipped_dirnames := f :: !skipped_dirnames -let ok_dirname f = +let ok_dirname f = f <> "" && f.[0] <> '.' && not (List.mem f !skipped_dirnames) && try ignore (check_ident f); true with _ -> false @@ -114,7 +114,7 @@ let all_subdirs ~unix_path:root = let f = readdir dirh in if ok_dirname f then let file = Filename.concat dir f in - try + try if (stat file).st_kind = S_DIR then begin let newrel = rel@[f] in add file newrel; @@ -132,14 +132,14 @@ let where_in_path ?(warn=true) path filename = let rec search = function | lpe :: rem -> let f = Filename.concat lpe filename in - if Sys.file_exists f + if Sys.file_exists f then (lpe,f) :: search rem else search rem | [] -> [] in let rec check_and_warn l = match l with | [] -> raise Not_found - | (lpe, f) :: l' -> + | (lpe, f) :: l' -> if warn & l' <> [] then msg_warning (str filename ++ str " has been found in" ++ spc () ++ @@ -159,11 +159,11 @@ let find_file_in_path ?(warn=true) paths filename = else errorlabstrm "System.find_file_in_path" (hov 0 (str "Can't find file" ++ spc () ++ str filename)) - else + else try where_in_path ~warn paths filename with Not_found -> errorlabstrm "System.find_file_in_path" - (hov 0 (str "Can't find file" ++ spc () ++ str filename ++ spc () ++ + (hov 0 (str "Can't find file" ++ spc () ++ str filename ++ spc () ++ str "on loadpath")) let is_in_path lpath filename = @@ -192,40 +192,40 @@ let marshal_in ch = exception Bad_magic_number of string let raw_extern_intern magic suffix = - let extern_state name = + let extern_state name = let filename = make_suffix name suffix in let channel = open_trapping_failure filename in output_binary_int channel magic; filename,channel - and intern_state filename = + and intern_state filename = let channel = open_in_bin filename in if input_binary_int channel <> magic then raise (Bad_magic_number filename); channel - in + in (extern_state,intern_state) let extern_intern ?(warn=true) magic suffix = let (raw_extern,raw_intern) = raw_extern_intern magic suffix in - let extern_state name val_0 = + let extern_state name val_0 = try let (filename,channel) = raw_extern name in try marshal_out channel val_0; close_out channel - with e -> + with e -> begin try_remove filename; raise e end with Sys_error s -> error ("System error: " ^ s) - and intern_state paths name = + and intern_state paths name = try let _,filename = find_file_in_path ~warn paths (make_suffix name suffix) in let channel = raw_intern filename in let v = marshal_in channel in - close_in channel; + close_in channel; v - with Sys_error s -> + with Sys_error s -> error("System error: " ^ s) - in + in (extern_state,intern_state) let with_magic_number_check f a = @@ -244,14 +244,14 @@ let connect writefun readfun com = let ch_to_in,ch_to_out = try open_in tmp_to, open_out tmp_to with Sys_error s -> error ("Cannot set connection to "^com^"("^s^")") in - let ch_from_in,ch_from_out = + let ch_from_in,ch_from_out = try open_in tmp_from, open_out tmp_from with Sys_error s -> - close_out ch_to_out; close_in ch_to_in; + close_out ch_to_out; close_in ch_to_in; error ("Cannot set connection from "^com^"("^s^")") in writefun ch_to_out; close_out ch_to_out; - let pid = + let pid = let ch_to' = Unix.descr_of_in_channel ch_to_in in let ch_from' = Unix.descr_of_out_channel ch_from_out in try Unix.create_process com [|com|] ch_to' ch_from' Unix.stdout @@ -279,32 +279,52 @@ let run_command converter f c = let n = ref 0 in let ne = ref 0 in - while n:= input cin buff 0 127 ; ne := input cerr buffe 0 127 ; + while n:= input cin buff 0 127 ; ne := input cerr buffe 0 127 ; !n+ !ne <> 0 - do - let r = converter (String.sub buff 0 !n) in + do + let r = converter (String.sub buff 0 !n) in f r; Buffer.add_string result r; - let r = converter (String.sub buffe 0 !ne) in + let r = converter (String.sub buffe 0 !ne) in f r; - Buffer.add_string result r + Buffer.add_string result r done; (Unix.close_process_full (cin,cout,cerr), Buffer.contents result) +let path_separator = if Sys.os_type = "Unix" then ':' else ';' + +let search_exe_in_path exe = + try + let path = Sys.getenv "PATH" in + let n = String.length path in + let rec aux i = + if i < n then + let j = + try String.index_from path i path_separator + with Not_found -> n + in + let dir = String.sub path i (j-i) in + let exe = Filename.concat dir exe in + if Sys.file_exists exe then Some exe else aux (i+1) + else + None + in aux 0 + with Not_found -> None + (* Time stamps. *) type time = float * float * float -let process_time () = +let process_time () = let t = times () in (t.tms_utime, t.tms_stime) -let get_time () = +let get_time () = let t = times () in (time(), t.tms_utime, t.tms_stime) let time_difference (t1,_,_) (t2,_,_) = t2 -. t1 - + let fmt_time_difference (startreal,ustart,sstart) (stopreal,ustop,sstop) = real (stopreal -. startreal) ++ str " secs " ++ str "(" ++ diff --git a/lib/system.mli b/lib/system.mli index 426a00df..2b8057f8 100644 --- a/lib/system.mli +++ b/lib/system.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: system.mli 13175 2010-06-22 06:28:37Z herbelin $ i*) +(*i $Id$ i*) (*s Files and load paths. Load path entries remember the original root given by the user. For efficiency, we keep the full path (field @@ -48,26 +48,28 @@ val marshal_in : in_channel -> 'a exception Bad_magic_number of string -val raw_extern_intern : int -> string -> +val raw_extern_intern : int -> string -> (string -> string * out_channel) * (string -> in_channel) -val extern_intern : ?warn:bool -> int -> string -> +val extern_intern : ?warn:bool -> int -> string -> (string -> 'a -> unit) * (load_path -> string -> 'a) val with_magic_number_check : ('a -> 'b) -> 'a -> 'b (*s Sending/receiving once with external executable *) -val connect : (out_channel -> unit) -> (in_channel -> 'a) -> string -> 'a +val connect : (out_channel -> unit) -> (in_channel -> 'a) -> string -> 'a (*s [run_command converter f com] launches command [com], and returns the contents of stdout and stderr that have been processed with [converter]; the processed contents of stdout and stderr is also passed to [f] *) -val run_command : (string -> string) -> (string -> unit) -> string -> +val run_command : (string -> string) -> (string -> unit) -> string -> Unix.process_status * string +val search_exe_in_path : string -> string option + (*s Time stamps. *) type time @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: tlm.ml 5920 2004-07-16 20:01:26Z herbelin $ *) +(* $Id$ *) type ('a,'b) t = Node of 'b Gset.t * ('a, ('a,'b) t) Gmap.t @@ -23,41 +23,41 @@ let in_dom (Node (_,m)) lbl = Gmap.mem lbl m let is_empty_node (Node(a,b)) = (Gset.elements a = []) & (Gmap.to_list b = []) let assure_arc m lbl = - if Gmap.mem lbl m then + if Gmap.mem lbl m then m - else + else Gmap.add lbl (Node (Gset.empty,Gmap.empty)) m let cleanse_arcs (Node (hereset,m)) = - let l = Gmap.rng m in + let l = Gmap.rng m in Node(hereset, if List.for_all is_empty_node l then Gmap.empty else m) let rec at_path f (Node (hereset,m)) = function - | [] -> + | [] -> cleanse_arcs (Node(f hereset,m)) | h::t -> - let m = assure_arc m h in + let m = assure_arc m h in cleanse_arcs (Node(hereset, Gmap.add h (at_path f (Gmap.find h m) t) m)) let add tm (path,v) = at_path (fun hereset -> Gset.add v hereset) tm path - + let rmv tm (path,v) = at_path (fun hereset -> Gset.remove v hereset) tm path -let app f tlm = +let app f tlm = let rec apprec pfx (Node(hereset,m)) = - let path = List.rev pfx in + let path = List.rev pfx in Gset.iter (fun v -> f(path,v)) hereset; Gmap.iter (fun l tm -> apprec (l::pfx) tm) m - in + in apprec [] tlm - -let to_list tlm = + +let to_list tlm = let rec torec pfx (Node(hereset,m)) = - let path = List.rev pfx in + let path = List.rev pfx in List.flatten((List.map (fun v -> (path,v)) (Gset.elements hereset)):: (List.map (fun (l,tm) -> torec (l::pfx) tm) (Gmap.to_list m))) - in + in torec [] tlm diff --git a/lib/tlm.mli b/lib/tlm.mli index 982bb5ed..54eb1759 100644 --- a/lib/tlm.mli +++ b/lib/tlm.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: tlm.mli 5920 2004-07-16 20:01:26Z herbelin $ i*) +(*i $Id$ i*) (* Tries. This module implements a data structure [('a,'b) t] mapping lists of values of type ['a] to sets (as lists) of values of type ['b]. *) diff --git a/lib/tries.ml b/lib/tries.ml new file mode 100644 index 00000000..fdde344c --- /dev/null +++ b/lib/tries.ml @@ -0,0 +1,78 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + + + +module Make = + functor (X : Set.OrderedType) -> + functor (Y : Map.OrderedType) -> +struct + module T_dom = Fset.Make(X) + module T_codom = Fmap.Make(Y) + + type t = Node of T_dom.t * t T_codom.t + + let codom_to_list m = T_codom.fold (fun x y l -> (x,y)::l) m [] + + let codom_rng m = T_codom.fold (fun _ y acc -> y::acc) m [] + + let codom_dom m = T_codom.fold (fun x _ acc -> x::acc) m [] + + let empty = Node (T_dom.empty, T_codom.empty) + + let map (Node (_,m)) lbl = T_codom.find lbl m + + let xtract (Node (hereset,_)) = T_dom.elements hereset + + let dom (Node (_,m)) = codom_dom m + + let in_dom (Node (_,m)) lbl = T_codom.mem lbl m + + let is_empty_node (Node(a,b)) = (T_dom.elements a = []) & (codom_to_list b = []) + +let assure_arc m lbl = + if T_codom.mem lbl m then + m + else + T_codom.add lbl (Node (T_dom.empty,T_codom.empty)) m + +let cleanse_arcs (Node (hereset,m)) = + let l = codom_rng m in + Node(hereset, if List.for_all is_empty_node l then T_codom.empty else m) + +let rec at_path f (Node (hereset,m)) = function + | [] -> + cleanse_arcs (Node(f hereset,m)) + | h::t -> + let m = assure_arc m h in + cleanse_arcs (Node(hereset, + T_codom.add h (at_path f (T_codom.find h m) t) m)) + +let add tm (path,v) = + at_path (fun hereset -> T_dom.add v hereset) tm path + +let rmv tm (path,v) = + at_path (fun hereset -> T_dom.remove v hereset) tm path + +let app f tlm = + let rec apprec pfx (Node(hereset,m)) = + let path = List.rev pfx in + T_dom.iter (fun v -> f(path,v)) hereset; + T_codom.iter (fun l tm -> apprec (l::pfx) tm) m + in + apprec [] tlm + +let to_list tlm = + let rec torec pfx (Node(hereset,m)) = + let path = List.rev pfx in + List.flatten((List.map (fun v -> (path,v)) (T_dom.elements hereset)):: + (List.map (fun (l,tm) -> torec (l::pfx) tm) (codom_to_list m))) + in + torec [] tlm + +end diff --git a/lib/tries.mli b/lib/tries.mli new file mode 100644 index 00000000..342c81ec --- /dev/null +++ b/lib/tries.mli @@ -0,0 +1,34 @@ + + + + + +module Make : + functor (X : Set.OrderedType) -> + functor (Y : Map.OrderedType) -> +sig + + type t + + val empty : t + + (* Work on labels, not on paths. *) + + val map : t -> Y.t -> t + + val xtract : t -> X.t list + + val dom : t -> Y.t list + + val in_dom : t -> Y.t -> bool + + (* Work on paths, not on labels. *) + + val add : t -> Y.t list * X.t -> t + + val rmv : t -> Y.t list * X.t -> t + + val app : ((Y.t list * X.t) -> unit) -> t -> unit + + val to_list : t -> (Y.t list * X.t) list +end diff --git a/lib/unicodetable.ml b/lib/unicodetable.ml new file mode 100644 index 00000000..f4e978d6 --- /dev/null +++ b/lib/unicodetable.ml @@ -0,0 +1,2619 @@ + +(** Unicode tables generated from Camomile. *) + +(* Letter, Uppercase *) +let lu = [ + (0x00041,0x0005A); + (0x000C0,0x000D6); + (0x000D8,0x000DE); + (0x00100,0x00100); + (0x00102,0x00102); + (0x00104,0x00104); + (0x00106,0x00106); + (0x00108,0x00108); + (0x0010A,0x0010A); + (0x0010C,0x0010C); + (0x0010E,0x0010E); + (0x00110,0x00110); + (0x00112,0x00112); + (0x00114,0x00114); + (0x00116,0x00116); + (0x00118,0x00118); + (0x0011A,0x0011A); + (0x0011C,0x0011C); + (0x0011E,0x0011E); + (0x00120,0x00120); + (0x00122,0x00122); + (0x00124,0x00124); + (0x00126,0x00126); + (0x00128,0x00128); + (0x0012A,0x0012A); + (0x0012C,0x0012C); + (0x0012E,0x0012E); + (0x00130,0x00130); + (0x00132,0x00132); + (0x00134,0x00134); + (0x00136,0x00136); + (0x00139,0x00139); + (0x0013B,0x0013B); + (0x0013D,0x0013D); + (0x0013F,0x0013F); + (0x00141,0x00141); + (0x00143,0x00143); + (0x00145,0x00145); + (0x00147,0x00147); + (0x0014A,0x0014A); + (0x0014C,0x0014C); + (0x0014E,0x0014E); + (0x00150,0x00150); + (0x00152,0x00152); + (0x00154,0x00154); + (0x00156,0x00156); + (0x00158,0x00158); + (0x0015A,0x0015A); + (0x0015C,0x0015C); + (0x0015E,0x0015E); + (0x00160,0x00160); + (0x00162,0x00162); + (0x00164,0x00164); + (0x00166,0x00166); + (0x00168,0x00168); + (0x0016A,0x0016A); + (0x0016C,0x0016C); + (0x0016E,0x0016E); + (0x00170,0x00170); + (0x00172,0x00172); + (0x00174,0x00174); + (0x00176,0x00176); + (0x00178,0x00179); + (0x0017B,0x0017B); + (0x0017D,0x0017D); + (0x00181,0x00182); + (0x00184,0x00184); + (0x00186,0x00187); + (0x00189,0x0018B); + (0x0018E,0x00191); + (0x00193,0x00194); + (0x00196,0x00198); + (0x0019C,0x0019D); + (0x0019F,0x001A0); + (0x001A2,0x001A2); + (0x001A4,0x001A4); + (0x001A6,0x001A7); + (0x001A9,0x001A9); + (0x001AC,0x001AC); + (0x001AE,0x001AF); + (0x001B1,0x001B3); + (0x001B5,0x001B5); + (0x001B7,0x001B8); + (0x001BC,0x001BC); + (0x001C4,0x001C4); + (0x001C7,0x001C7); + (0x001CA,0x001CA); + (0x001CD,0x001CD); + (0x001CF,0x001CF); + (0x001D1,0x001D1); + (0x001D3,0x001D3); + (0x001D5,0x001D5); + (0x001D7,0x001D7); + (0x001D9,0x001D9); + (0x001DB,0x001DB); + (0x001DE,0x001DE); + (0x001E0,0x001E0); + (0x001E2,0x001E2); + (0x001E4,0x001E4); + (0x001E6,0x001E6); + (0x001E8,0x001E8); + (0x001EA,0x001EA); + (0x001EC,0x001EC); + (0x001EE,0x001EE); + (0x001F1,0x001F1); + (0x001F4,0x001F4); + (0x001F6,0x001F8); + (0x001FA,0x001FA); + (0x001FC,0x001FC); + (0x001FE,0x001FE); + (0x00200,0x00200); + (0x00202,0x00202); + (0x00204,0x00204); + (0x00206,0x00206); + (0x00208,0x00208); + (0x0020A,0x0020A); + (0x0020C,0x0020C); + (0x0020E,0x0020E); + (0x00210,0x00210); + (0x00212,0x00212); + (0x00214,0x00214); + (0x00216,0x00216); + (0x00218,0x00218); + (0x0021A,0x0021A); + (0x0021C,0x0021C); + (0x0021E,0x0021E); + (0x00220,0x00220); + (0x00222,0x00222); + (0x00224,0x00224); + (0x00226,0x00226); + (0x00228,0x00228); + (0x0022A,0x0022A); + (0x0022C,0x0022C); + (0x0022E,0x0022E); + (0x00230,0x00230); + (0x00232,0x00232); + (0x00386,0x00386); + (0x00388,0x0038A); + (0x0038C,0x0038C); + (0x0038E,0x0038F); + (0x00391,0x003A1); + (0x003A3,0x003AB); + (0x003D2,0x003D4); + (0x003D8,0x003D8); + (0x003DA,0x003DA); + (0x003DC,0x003DC); + (0x003DE,0x003DE); + (0x003E0,0x003E0); + (0x003E2,0x003E2); + (0x003E4,0x003E4); + (0x003E6,0x003E6); + (0x003E8,0x003E8); + (0x003EA,0x003EA); + (0x003EC,0x003EC); + (0x003EE,0x003EE); + (0x003F4,0x003F4); + (0x00400,0x0042F); + (0x00460,0x00460); + (0x00462,0x00462); + (0x00464,0x00464); + (0x00466,0x00466); + (0x00468,0x00468); + (0x0046A,0x0046A); + (0x0046C,0x0046C); + (0x0046E,0x0046E); + (0x00470,0x00470); + (0x00472,0x00472); + (0x00474,0x00474); + (0x00476,0x00476); + (0x00478,0x00478); + (0x0047A,0x0047A); + (0x0047C,0x0047C); + (0x0047E,0x0047E); + (0x00480,0x00480); + (0x0048A,0x0048A); + (0x0048C,0x0048C); + (0x0048E,0x0048E); + (0x00490,0x00490); + (0x00492,0x00492); + (0x00494,0x00494); + (0x00496,0x00496); + (0x00498,0x00498); + (0x0049A,0x0049A); + (0x0049C,0x0049C); + (0x0049E,0x0049E); + (0x004A0,0x004A0); + (0x004A2,0x004A2); + (0x004A4,0x004A4); + (0x004A6,0x004A6); + (0x004A8,0x004A8); + (0x004AA,0x004AA); + (0x004AC,0x004AC); + (0x004AE,0x004AE); + (0x004B0,0x004B0); + (0x004B2,0x004B2); + (0x004B4,0x004B4); + (0x004B6,0x004B6); + (0x004B8,0x004B8); + (0x004BA,0x004BA); + (0x004BC,0x004BC); + (0x004BE,0x004BE); + (0x004C0,0x004C1); + (0x004C3,0x004C3); + (0x004C5,0x004C5); + (0x004C7,0x004C7); + (0x004C9,0x004C9); + (0x004CB,0x004CB); + (0x004CD,0x004CD); + (0x004D0,0x004D0); + (0x004D2,0x004D2); + (0x004D4,0x004D4); + (0x004D6,0x004D6); + (0x004D8,0x004D8); + (0x004DA,0x004DA); + (0x004DC,0x004DC); + (0x004DE,0x004DE); + (0x004E0,0x004E0); + (0x004E2,0x004E2); + (0x004E4,0x004E4); + (0x004E6,0x004E6); + (0x004E8,0x004E8); + (0x004EA,0x004EA); + (0x004EC,0x004EC); + (0x004EE,0x004EE); + (0x004F0,0x004F0); + (0x004F2,0x004F2); + (0x004F4,0x004F4); + (0x004F8,0x004F8); + (0x00500,0x00500); + (0x00502,0x00502); + (0x00504,0x00504); + (0x00506,0x00506); + (0x00508,0x00508); + (0x0050A,0x0050A); + (0x0050C,0x0050C); + (0x0050E,0x0050E); + (0x00531,0x00556); + (0x010A0,0x010C5); + (0x01E00,0x01E00); + (0x01E02,0x01E02); + (0x01E04,0x01E04); + (0x01E06,0x01E06); + (0x01E08,0x01E08); + (0x01E0A,0x01E0A); + (0x01E0C,0x01E0C); + (0x01E0E,0x01E0E); + (0x01E10,0x01E10); + (0x01E12,0x01E12); + (0x01E14,0x01E14); + (0x01E16,0x01E16); + (0x01E18,0x01E18); + (0x01E1A,0x01E1A); + (0x01E1C,0x01E1C); + (0x01E1E,0x01E1E); + (0x01E20,0x01E20); + (0x01E22,0x01E22); + (0x01E24,0x01E24); + (0x01E26,0x01E26); + (0x01E28,0x01E28); + (0x01E2A,0x01E2A); + (0x01E2C,0x01E2C); + (0x01E2E,0x01E2E); + (0x01E30,0x01E30); + (0x01E32,0x01E32); + (0x01E34,0x01E34); + (0x01E36,0x01E36); + (0x01E38,0x01E38); + (0x01E3A,0x01E3A); + (0x01E3C,0x01E3C); + (0x01E3E,0x01E3E); + (0x01E40,0x01E40); + (0x01E42,0x01E42); + (0x01E44,0x01E44); + (0x01E46,0x01E46); + (0x01E48,0x01E48); + (0x01E4A,0x01E4A); + (0x01E4C,0x01E4C); + (0x01E4E,0x01E4E); + (0x01E50,0x01E50); + (0x01E52,0x01E52); + (0x01E54,0x01E54); + (0x01E56,0x01E56); + (0x01E58,0x01E58); + (0x01E5A,0x01E5A); + (0x01E5C,0x01E5C); + (0x01E5E,0x01E5E); + (0x01E60,0x01E60); + (0x01E62,0x01E62); + (0x01E64,0x01E64); + (0x01E66,0x01E66); + (0x01E68,0x01E68); + (0x01E6A,0x01E6A); + (0x01E6C,0x01E6C); + (0x01E6E,0x01E6E); + (0x01E70,0x01E70); + (0x01E72,0x01E72); + (0x01E74,0x01E74); + (0x01E76,0x01E76); + (0x01E78,0x01E78); + (0x01E7A,0x01E7A); + (0x01E7C,0x01E7C); + (0x01E7E,0x01E7E); + (0x01E80,0x01E80); + (0x01E82,0x01E82); + (0x01E84,0x01E84); + (0x01E86,0x01E86); + (0x01E88,0x01E88); + (0x01E8A,0x01E8A); + (0x01E8C,0x01E8C); + (0x01E8E,0x01E8E); + (0x01E90,0x01E90); + (0x01E92,0x01E92); + (0x01E94,0x01E94); + (0x01EA0,0x01EA0); + (0x01EA2,0x01EA2); + (0x01EA4,0x01EA4); + (0x01EA6,0x01EA6); + (0x01EA8,0x01EA8); + (0x01EAA,0x01EAA); + (0x01EAC,0x01EAC); + (0x01EAE,0x01EAE); + (0x01EB0,0x01EB0); + (0x01EB2,0x01EB2); + (0x01EB4,0x01EB4); + (0x01EB6,0x01EB6); + (0x01EB8,0x01EB8); + (0x01EBA,0x01EBA); + (0x01EBC,0x01EBC); + (0x01EBE,0x01EBE); + (0x01EC0,0x01EC0); + (0x01EC2,0x01EC2); + (0x01EC4,0x01EC4); + (0x01EC6,0x01EC6); + (0x01EC8,0x01EC8); + (0x01ECA,0x01ECA); + (0x01ECC,0x01ECC); + (0x01ECE,0x01ECE); + (0x01ED0,0x01ED0); + (0x01ED2,0x01ED2); + (0x01ED4,0x01ED4); + (0x01ED6,0x01ED6); + (0x01ED8,0x01ED8); + (0x01EDA,0x01EDA); + (0x01EDC,0x01EDC); + (0x01EDE,0x01EDE); + (0x01EE0,0x01EE0); + (0x01EE2,0x01EE2); + (0x01EE4,0x01EE4); + (0x01EE6,0x01EE6); + (0x01EE8,0x01EE8); + (0x01EEA,0x01EEA); + (0x01EEC,0x01EEC); + (0x01EEE,0x01EEE); + (0x01EF0,0x01EF0); + (0x01EF2,0x01EF2); + (0x01EF4,0x01EF4); + (0x01EF6,0x01EF6); + (0x01EF8,0x01EF8); + (0x01F08,0x01F0F); + (0x01F18,0x01F1D); + (0x01F28,0x01F2F); + (0x01F38,0x01F3F); + (0x01F48,0x01F4D); + (0x01F59,0x01F59); + (0x01F5B,0x01F5B); + (0x01F5D,0x01F5D); + (0x01F5F,0x01F5F); + (0x01F68,0x01F6F); + (0x01FB8,0x01FBB); + (0x01FC8,0x01FCB); + (0x01FD8,0x01FDB); + (0x01FE8,0x01FEC); + (0x01FF8,0x01FFB); + (0x02102,0x02102); + (0x02107,0x02107); + (0x0210B,0x0210D); + (0x02110,0x02112); + (0x02115,0x02115); + (0x02119,0x0211D); + (0x02124,0x02124); + (0x02126,0x02126); + (0x02128,0x02128); + (0x0212A,0x0212D); + (0x02130,0x02131); + (0x02133,0x02133); + (0x0213E,0x0213F); + (0x02145,0x02145); + (0x0FF21,0x0FF3A); + (0x10400,0x10425); + (0x1D400,0x1D419); + (0x1D434,0x1D44D); + (0x1D468,0x1D481); + (0x1D49C,0x1D49C); + (0x1D49E,0x1D49F); + (0x1D4A2,0x1D4A2); + (0x1D4A5,0x1D4A6); + (0x1D4A9,0x1D4AC); + (0x1D4AE,0x1D4B5); + (0x1D4D0,0x1D4E9); + (0x1D504,0x1D505); + (0x1D507,0x1D50A); + (0x1D50D,0x1D514); + (0x1D516,0x1D51C); + (0x1D538,0x1D539); + (0x1D53B,0x1D53E); + (0x1D540,0x1D544); + (0x1D546,0x1D546); + (0x1D54A,0x1D550); + (0x1D56C,0x1D585); + (0x1D5A0,0x1D5B9); + (0x1D5D4,0x1D5ED); + (0x1D608,0x1D621); + (0x1D63C,0x1D655); + (0x1D670,0x1D689); + (0x1D6A8,0x1D6C0); + (0x1D6E2,0x1D6FA); + (0x1D71C,0x1D734); + (0x1D756,0x1D76E); + (0x1D790,0x1D7A8) +] +(* Letter, Lowercase *) +let ll = [ + (0x00061,0x0007A); + (0x000AA,0x000AA); + (0x000B5,0x000B5); + (0x000BA,0x000BA); + (0x000DF,0x000F6); + (0x000F8,0x000FF); + (0x00101,0x00101); + (0x00103,0x00103); + (0x00105,0x00105); + (0x00107,0x00107); + (0x00109,0x00109); + (0x0010B,0x0010B); + (0x0010D,0x0010D); + (0x0010F,0x0010F); + (0x00111,0x00111); + (0x00113,0x00113); + (0x00115,0x00115); + (0x00117,0x00117); + (0x00119,0x00119); + (0x0011B,0x0011B); + (0x0011D,0x0011D); + (0x0011F,0x0011F); + (0x00121,0x00121); + (0x00123,0x00123); + (0x00125,0x00125); + (0x00127,0x00127); + (0x00129,0x00129); + (0x0012B,0x0012B); + (0x0012D,0x0012D); + (0x0012F,0x0012F); + (0x00131,0x00131); + (0x00133,0x00133); + (0x00135,0x00135); + (0x00137,0x00138); + (0x0013A,0x0013A); + (0x0013C,0x0013C); + (0x0013E,0x0013E); + (0x00140,0x00140); + (0x00142,0x00142); + (0x00144,0x00144); + (0x00146,0x00146); + (0x00148,0x00149); + (0x0014B,0x0014B); + (0x0014D,0x0014D); + (0x0014F,0x0014F); + (0x00151,0x00151); + (0x00153,0x00153); + (0x00155,0x00155); + (0x00157,0x00157); + (0x00159,0x00159); + (0x0015B,0x0015B); + (0x0015D,0x0015D); + (0x0015F,0x0015F); + (0x00161,0x00161); + (0x00163,0x00163); + (0x00165,0x00165); + (0x00167,0x00167); + (0x00169,0x00169); + (0x0016B,0x0016B); + (0x0016D,0x0016D); + (0x0016F,0x0016F); + (0x00171,0x00171); + (0x00173,0x00173); + (0x00175,0x00175); + (0x00177,0x00177); + (0x0017A,0x0017A); + (0x0017C,0x0017C); + (0x0017E,0x00180); + (0x00183,0x00183); + (0x00185,0x00185); + (0x00188,0x00188); + (0x0018C,0x0018D); + (0x00192,0x00192); + (0x00195,0x00195); + (0x00199,0x0019B); + (0x0019E,0x0019E); + (0x001A1,0x001A1); + (0x001A3,0x001A3); + (0x001A5,0x001A5); + (0x001A8,0x001A8); + (0x001AA,0x001AB); + (0x001AD,0x001AD); + (0x001B0,0x001B0); + (0x001B4,0x001B4); + (0x001B6,0x001B6); + (0x001B9,0x001BA); + (0x001BD,0x001BF); + (0x001C6,0x001C6); + (0x001C9,0x001C9); + (0x001CC,0x001CC); + (0x001CE,0x001CE); + (0x001D0,0x001D0); + (0x001D2,0x001D2); + (0x001D4,0x001D4); + (0x001D6,0x001D6); + (0x001D8,0x001D8); + (0x001DA,0x001DA); + (0x001DC,0x001DD); + (0x001DF,0x001DF); + (0x001E1,0x001E1); + (0x001E3,0x001E3); + (0x001E5,0x001E5); + (0x001E7,0x001E7); + (0x001E9,0x001E9); + (0x001EB,0x001EB); + (0x001ED,0x001ED); + (0x001EF,0x001F0); + (0x001F3,0x001F3); + (0x001F5,0x001F5); + (0x001F9,0x001F9); + (0x001FB,0x001FB); + (0x001FD,0x001FD); + (0x001FF,0x001FF); + (0x00201,0x00201); + (0x00203,0x00203); + (0x00205,0x00205); + (0x00207,0x00207); + (0x00209,0x00209); + (0x0020B,0x0020B); + (0x0020D,0x0020D); + (0x0020F,0x0020F); + (0x00211,0x00211); + (0x00213,0x00213); + (0x00215,0x00215); + (0x00217,0x00217); + (0x00219,0x00219); + (0x0021B,0x0021B); + (0x0021D,0x0021D); + (0x0021F,0x0021F); + (0x00223,0x00223); + (0x00225,0x00225); + (0x00227,0x00227); + (0x00229,0x00229); + (0x0022B,0x0022B); + (0x0022D,0x0022D); + (0x0022F,0x0022F); + (0x00231,0x00231); + (0x00233,0x00233); + (0x00250,0x002AD); + (0x00390,0x00390); + (0x003AC,0x003CE); + (0x003D0,0x003D1); + (0x003D5,0x003D7); + (0x003D9,0x003D9); + (0x003DB,0x003DB); + (0x003DD,0x003DD); + (0x003DF,0x003DF); + (0x003E1,0x003E1); + (0x003E3,0x003E3); + (0x003E5,0x003E5); + (0x003E7,0x003E7); + (0x003E9,0x003E9); + (0x003EB,0x003EB); + (0x003ED,0x003ED); + (0x003EF,0x003F3); + (0x003F5,0x003F5); + (0x00430,0x0045F); + (0x00461,0x00461); + (0x00463,0x00463); + (0x00465,0x00465); + (0x00467,0x00467); + (0x00469,0x00469); + (0x0046B,0x0046B); + (0x0046D,0x0046D); + (0x0046F,0x0046F); + (0x00471,0x00471); + (0x00473,0x00473); + (0x00475,0x00475); + (0x00477,0x00477); + (0x00479,0x00479); + (0x0047B,0x0047B); + (0x0047D,0x0047D); + (0x0047F,0x0047F); + (0x00481,0x00481); + (0x0048B,0x0048B); + (0x0048D,0x0048D); + (0x0048F,0x0048F); + (0x00491,0x00491); + (0x00493,0x00493); + (0x00495,0x00495); + (0x00497,0x00497); + (0x00499,0x00499); + (0x0049B,0x0049B); + (0x0049D,0x0049D); + (0x0049F,0x0049F); + (0x004A1,0x004A1); + (0x004A3,0x004A3); + (0x004A5,0x004A5); + (0x004A7,0x004A7); + (0x004A9,0x004A9); + (0x004AB,0x004AB); + (0x004AD,0x004AD); + (0x004AF,0x004AF); + (0x004B1,0x004B1); + (0x004B3,0x004B3); + (0x004B5,0x004B5); + (0x004B7,0x004B7); + (0x004B9,0x004B9); + (0x004BB,0x004BB); + (0x004BD,0x004BD); + (0x004BF,0x004BF); + (0x004C2,0x004C2); + (0x004C4,0x004C4); + (0x004C6,0x004C6); + (0x004C8,0x004C8); + (0x004CA,0x004CA); + (0x004CC,0x004CC); + (0x004CE,0x004CE); + (0x004D1,0x004D1); + (0x004D3,0x004D3); + (0x004D5,0x004D5); + (0x004D7,0x004D7); + (0x004D9,0x004D9); + (0x004DB,0x004DB); + (0x004DD,0x004DD); + (0x004DF,0x004DF); + (0x004E1,0x004E1); + (0x004E3,0x004E3); + (0x004E5,0x004E5); + (0x004E7,0x004E7); + (0x004E9,0x004E9); + (0x004EB,0x004EB); + (0x004ED,0x004ED); + (0x004EF,0x004EF); + (0x004F1,0x004F1); + (0x004F3,0x004F3); + (0x004F5,0x004F5); + (0x004F9,0x004F9); + (0x00501,0x00501); + (0x00503,0x00503); + (0x00505,0x00505); + (0x00507,0x00507); + (0x00509,0x00509); + (0x0050B,0x0050B); + (0x0050D,0x0050D); + (0x0050F,0x0050F); + (0x00561,0x00587); + (0x01E01,0x01E01); + (0x01E03,0x01E03); + (0x01E05,0x01E05); + (0x01E07,0x01E07); + (0x01E09,0x01E09); + (0x01E0B,0x01E0B); + (0x01E0D,0x01E0D); + (0x01E0F,0x01E0F); + (0x01E11,0x01E11); + (0x01E13,0x01E13); + (0x01E15,0x01E15); + (0x01E17,0x01E17); + (0x01E19,0x01E19); + (0x01E1B,0x01E1B); + (0x01E1D,0x01E1D); + (0x01E1F,0x01E1F); + (0x01E21,0x01E21); + (0x01E23,0x01E23); + (0x01E25,0x01E25); + (0x01E27,0x01E27); + (0x01E29,0x01E29); + (0x01E2B,0x01E2B); + (0x01E2D,0x01E2D); + (0x01E2F,0x01E2F); + (0x01E31,0x01E31); + (0x01E33,0x01E33); + (0x01E35,0x01E35); + (0x01E37,0x01E37); + (0x01E39,0x01E39); + (0x01E3B,0x01E3B); + (0x01E3D,0x01E3D); + (0x01E3F,0x01E3F); + (0x01E41,0x01E41); + (0x01E43,0x01E43); + (0x01E45,0x01E45); + (0x01E47,0x01E47); + (0x01E49,0x01E49); + (0x01E4B,0x01E4B); + (0x01E4D,0x01E4D); + (0x01E4F,0x01E4F); + (0x01E51,0x01E51); + (0x01E53,0x01E53); + (0x01E55,0x01E55); + (0x01E57,0x01E57); + (0x01E59,0x01E59); + (0x01E5B,0x01E5B); + (0x01E5D,0x01E5D); + (0x01E5F,0x01E5F); + (0x01E61,0x01E61); + (0x01E63,0x01E63); + (0x01E65,0x01E65); + (0x01E67,0x01E67); + (0x01E69,0x01E69); + (0x01E6B,0x01E6B); + (0x01E6D,0x01E6D); + (0x01E6F,0x01E6F); + (0x01E71,0x01E71); + (0x01E73,0x01E73); + (0x01E75,0x01E75); + (0x01E77,0x01E77); + (0x01E79,0x01E79); + (0x01E7B,0x01E7B); + (0x01E7D,0x01E7D); + (0x01E7F,0x01E7F); + (0x01E81,0x01E81); + (0x01E83,0x01E83); + (0x01E85,0x01E85); + (0x01E87,0x01E87); + (0x01E89,0x01E89); + (0x01E8B,0x01E8B); + (0x01E8D,0x01E8D); + (0x01E8F,0x01E8F); + (0x01E91,0x01E91); + (0x01E93,0x01E93); + (0x01E95,0x01E9B); + (0x01EA1,0x01EA1); + (0x01EA3,0x01EA3); + (0x01EA5,0x01EA5); + (0x01EA7,0x01EA7); + (0x01EA9,0x01EA9); + (0x01EAB,0x01EAB); + (0x01EAD,0x01EAD); + (0x01EAF,0x01EAF); + (0x01EB1,0x01EB1); + (0x01EB3,0x01EB3); + (0x01EB5,0x01EB5); + (0x01EB7,0x01EB7); + (0x01EB9,0x01EB9); + (0x01EBB,0x01EBB); + (0x01EBD,0x01EBD); + (0x01EBF,0x01EBF); + (0x01EC1,0x01EC1); + (0x01EC3,0x01EC3); + (0x01EC5,0x01EC5); + (0x01EC7,0x01EC7); + (0x01EC9,0x01EC9); + (0x01ECB,0x01ECB); + (0x01ECD,0x01ECD); + (0x01ECF,0x01ECF); + (0x01ED1,0x01ED1); + (0x01ED3,0x01ED3); + (0x01ED5,0x01ED5); + (0x01ED7,0x01ED7); + (0x01ED9,0x01ED9); + (0x01EDB,0x01EDB); + (0x01EDD,0x01EDD); + (0x01EDF,0x01EDF); + (0x01EE1,0x01EE1); + (0x01EE3,0x01EE3); + (0x01EE5,0x01EE5); + (0x01EE7,0x01EE7); + (0x01EE9,0x01EE9); + (0x01EEB,0x01EEB); + (0x01EED,0x01EED); + (0x01EEF,0x01EEF); + (0x01EF1,0x01EF1); + (0x01EF3,0x01EF3); + (0x01EF5,0x01EF5); + (0x01EF7,0x01EF7); + (0x01EF9,0x01EF9); + (0x01F00,0x01F07); + (0x01F10,0x01F15); + (0x01F20,0x01F27); + (0x01F30,0x01F37); + (0x01F40,0x01F45); + (0x01F50,0x01F57); + (0x01F60,0x01F67); + (0x01F70,0x01F7D); + (0x01F80,0x01F87); + (0x01F90,0x01F97); + (0x01FA0,0x01FA7); + (0x01FB0,0x01FB4); + (0x01FB6,0x01FB7); + (0x01FBE,0x01FBE); + (0x01FC2,0x01FC4); + (0x01FC6,0x01FC7); + (0x01FD0,0x01FD3); + (0x01FD6,0x01FD7); + (0x01FE0,0x01FE7); + (0x01FF2,0x01FF4); + (0x01FF6,0x01FF7); + (0x02071,0x02071); + (0x0207F,0x0207F); + (0x0210A,0x0210A); + (0x0210E,0x0210F); + (0x02113,0x02113); + (0x0212F,0x0212F); + (0x02134,0x02134); + (0x02139,0x02139); + (0x0213D,0x0213D); + (0x02146,0x02149); + (0x0FB00,0x0FB06); + (0x0FB13,0x0FB17); + (0x0FF41,0x0FF5A); + (0x10428,0x1044D); + (0x1D41A,0x1D433); + (0x1D44E,0x1D454); + (0x1D456,0x1D467); + (0x1D482,0x1D49B); + (0x1D4B6,0x1D4B9); + (0x1D4BB,0x1D4BB); + (0x1D4BD,0x1D4C0); + (0x1D4C2,0x1D4C3); + (0x1D4C5,0x1D4CF); + (0x1D4EA,0x1D503); + (0x1D51E,0x1D537); + (0x1D552,0x1D56B); + (0x1D586,0x1D59F); + (0x1D5BA,0x1D5D3); + (0x1D5EE,0x1D607); + (0x1D622,0x1D63B); + (0x1D656,0x1D66F); + (0x1D68A,0x1D6A3); + (0x1D6C2,0x1D6DA); + (0x1D6DC,0x1D6E1); + (0x1D6FC,0x1D714); + (0x1D716,0x1D71B); + (0x1D736,0x1D74E); + (0x1D750,0x1D755); + (0x1D770,0x1D788); + (0x1D78A,0x1D78F); + (0x1D7AA,0x1D7C2); + (0x1D7C4,0x1D7C9) +] +(* Letter, Titlecase *) +let lt = [ + (0x001C5,0x001C5); + (0x001C8,0x001C8); + (0x001CB,0x001CB); + (0x001F2,0x001F2); + (0x01F88,0x01F8F); + (0x01F98,0x01F9F); + (0x01FA8,0x01FAF); + (0x01FBC,0x01FBC); + (0x01FCC,0x01FCC); + (0x01FFC,0x01FFC) +] +(* Mark, Non-Spacing *) +let mn = [ + (0x00300,0x0034F); + (0x00360,0x0036F); + (0x00483,0x00486); + (0x00591,0x005A1); + (0x005A3,0x005B9); + (0x005BB,0x005BD); + (0x005BF,0x005BF); + (0x005C1,0x005C2); + (0x005C4,0x005C4); + (0x0064B,0x00655); + (0x00670,0x00670); + (0x006D6,0x006DC); + (0x006DF,0x006E4); + (0x006E7,0x006E8); + (0x006EA,0x006ED); + (0x00711,0x00711); + (0x00730,0x0074A); + (0x007A6,0x007B0); + (0x00901,0x00902); + (0x0093C,0x0093C); + (0x00941,0x00948); + (0x0094D,0x0094D); + (0x00951,0x00954); + (0x00962,0x00963); + (0x00981,0x00981); + (0x009BC,0x009BC); + (0x009C1,0x009C4); + (0x009CD,0x009CD); + (0x009E2,0x009E3); + (0x00A02,0x00A02); + (0x00A3C,0x00A3C); + (0x00A41,0x00A42); + (0x00A47,0x00A48); + (0x00A4B,0x00A4D); + (0x00A70,0x00A71); + (0x00A81,0x00A82); + (0x00ABC,0x00ABC); + (0x00AC1,0x00AC5); + (0x00AC7,0x00AC8); + (0x00ACD,0x00ACD); + (0x00B01,0x00B01); + (0x00B3C,0x00B3C); + (0x00B3F,0x00B3F); + (0x00B41,0x00B43); + (0x00B4D,0x00B4D); + (0x00B56,0x00B56); + (0x00B82,0x00B82); + (0x00BC0,0x00BC0); + (0x00BCD,0x00BCD); + (0x00C3E,0x00C40); + (0x00C46,0x00C48); + (0x00C4A,0x00C4D); + (0x00C55,0x00C56); + (0x00CBF,0x00CBF); + (0x00CC6,0x00CC6); + (0x00CCC,0x00CCD); + (0x00D41,0x00D43); + (0x00D4D,0x00D4D); + (0x00DCA,0x00DCA); + (0x00DD2,0x00DD4); + (0x00DD6,0x00DD6); + (0x00E31,0x00E31); + (0x00E34,0x00E3A); + (0x00E47,0x00E4E); + (0x00EB1,0x00EB1); + (0x00EB4,0x00EB9); + (0x00EBB,0x00EBC); + (0x00EC8,0x00ECD); + (0x00F18,0x00F19); + (0x00F35,0x00F35); + (0x00F37,0x00F37); + (0x00F39,0x00F39); + (0x00F71,0x00F7E); + (0x00F80,0x00F84); + (0x00F86,0x00F87); + (0x00F90,0x00F97); + (0x00F99,0x00FBC); + (0x00FC6,0x00FC6); + (0x0102D,0x01030); + (0x01032,0x01032); + (0x01036,0x01037); + (0x01039,0x01039); + (0x01058,0x01059); + (0x01712,0x01714); + (0x01732,0x01734); + (0x01752,0x01753); + (0x01772,0x01773); + (0x017B7,0x017BD); + (0x017C6,0x017C6); + (0x017C9,0x017D3); + (0x0180B,0x0180D); + (0x018A9,0x018A9); + (0x020D0,0x020DC); + (0x020E1,0x020E1); + (0x020E5,0x020EA); + (0x0302A,0x0302F); + (0x03099,0x0309A); + (0x0FB1E,0x0FB1E); + (0x0FE00,0x0FE0F); + (0x0FE20,0x0FE23); + (0x1D167,0x1D169); + (0x1D17B,0x1D182); + (0x1D185,0x1D18B); + (0x1D1AA,0x1D1AD) +] +(* Mark, Spacing Combining *) +let mc = [ + (0x00903,0x00903); + (0x0093E,0x00940); + (0x00949,0x0094C); + (0x00982,0x00983); + (0x009BE,0x009C0); + (0x009C7,0x009C8); + (0x009CB,0x009CC); + (0x009D7,0x009D7); + (0x00A3E,0x00A40); + (0x00A83,0x00A83); + (0x00ABE,0x00AC0); + (0x00AC9,0x00AC9); + (0x00ACB,0x00ACC); + (0x00B02,0x00B03); + (0x00B3E,0x00B3E); + (0x00B40,0x00B40); + (0x00B47,0x00B48); + (0x00B4B,0x00B4C); + (0x00B57,0x00B57); + (0x00BBE,0x00BBF); + (0x00BC1,0x00BC2); + (0x00BC6,0x00BC8); + (0x00BCA,0x00BCC); + (0x00BD7,0x00BD7); + (0x00C01,0x00C03); + (0x00C41,0x00C44); + (0x00C82,0x00C83); + (0x00CBE,0x00CBE); + (0x00CC0,0x00CC4); + (0x00CC7,0x00CC8); + (0x00CCA,0x00CCB); + (0x00CD5,0x00CD6); + (0x00D02,0x00D03); + (0x00D3E,0x00D40); + (0x00D46,0x00D48); + (0x00D4A,0x00D4C); + (0x00D57,0x00D57); + (0x00D82,0x00D83); + (0x00DCF,0x00DD1); + (0x00DD8,0x00DDF); + (0x00DF2,0x00DF3); + (0x00F3E,0x00F3F); + (0x00F7F,0x00F7F); + (0x0102C,0x0102C); + (0x01031,0x01031); + (0x01038,0x01038); + (0x01056,0x01057); + (0x017B4,0x017B6); + (0x017BE,0x017C5); + (0x017C7,0x017C8); + (0x1D165,0x1D166); + (0x1D16D,0x1D172) +] +(* Mark, Enclosing *) +let me = [ + (0x00488,0x00489); + (0x006DE,0x006DE); + (0x020DD,0x020E0); + (0x020E2,0x020E4) +] +(* Number, Decimal Digit *) +let nd = [ + (0x00030,0x00039); + (0x00660,0x00669); + (0x006F0,0x006F9); + (0x00966,0x0096F); + (0x009E6,0x009EF); + (0x00A66,0x00A6F); + (0x00AE6,0x00AEF); + (0x00B66,0x00B6F); + (0x00BE7,0x00BEF); + (0x00C66,0x00C6F); + (0x00CE6,0x00CEF); + (0x00D66,0x00D6F); + (0x00E50,0x00E59); + (0x00ED0,0x00ED9); + (0x00F20,0x00F29); + (0x01040,0x01049); + (0x01369,0x01371); + (0x017E0,0x017E9); + (0x01810,0x01819); + (0x0FF10,0x0FF19); + (0x1D7CE,0x1D7FF) +] +(* Number, Letter *) +let nl = [ + (0x016EE,0x016F0); + (0x02160,0x02183); + (0x03007,0x03007); + (0x03021,0x03029); + (0x03038,0x0303A); + (0x1034A,0x1034A) +] +(* Number, Other *) +let no = [ + (0x000B2,0x000B3); + (0x000B9,0x000B9); + (0x000BC,0x000BE); + (0x009F4,0x009F9); + (0x00BF0,0x00BF2); + (0x00F2A,0x00F33); + (0x01372,0x0137C); + (0x02070,0x02070); + (0x02074,0x02079); + (0x02080,0x02089); + (0x02153,0x0215F); + (0x02460,0x0249B); + (0x024EA,0x024FE); + (0x02776,0x02793); + (0x03192,0x03195); + (0x03220,0x03229); + (0x03251,0x0325F); + (0x03280,0x03289); + (0x032B1,0x032BF); + (0x10320,0x10323) +] +(* Separator, Space *) +let zs = [ + (0x00020,0x00020); + (0x000A0,0x000A0); + (0x01680,0x01680); + (0x02000,0x0200B); + (0x0202F,0x0202F); + (0x0205F,0x0205F); + (0x03000,0x03000) +] +(* Separator, Line *) +let zl = [ + (0x02028,0x02028) +] +(* Separator, Paragraph *) +let zp = [ + (0x02029,0x02029) +] +(* Other, Control *) +let cc = [ + (0x00000,0x0001F); + (0x0007F,0x0009F) +] +(* Other, Format *) +let cf = [ + (0x006DD,0x006DD); + (0x0070F,0x0070F); + (0x0180E,0x0180E); + (0x0200C,0x0200F); + (0x0202A,0x0202E); + (0x02060,0x02063); + (0x0206A,0x0206F); + (0x0FEFF,0x0FEFF); + (0x0FFF9,0x0FFFB); + (0x1D173,0x1D17A); + (0xE0001,0xE0001); + (0xE0020,0xE007F) +] +(* Other, Surrogate *) +let cs = [ + (0x0D800,0x0DEFE); + (0x0DFFF,0x0DFFF) +] +(* Other, Private Use *) +let co = [ + (0x0E000,0x0F8FF) +] +(* Other, Not Assigned *) +let cn = [ + (0x00221,0x00221); + (0x00234,0x0024F); + (0x002AE,0x002AF); + (0x002EF,0x002FF); + (0x00350,0x0035F); + (0x00370,0x00373); + (0x00376,0x00379); + (0x0037B,0x0037D); + (0x0037F,0x00383); + (0x0038B,0x0038B); + (0x0038D,0x0038D); + (0x003A2,0x003A2); + (0x003CF,0x003CF); + (0x003F7,0x003FF); + (0x00487,0x00487); + (0x004CF,0x004CF); + (0x004F6,0x004F7); + (0x004FA,0x004FF); + (0x00510,0x00530); + (0x00557,0x00558); + (0x00560,0x00560); + (0x00588,0x00588); + (0x0058B,0x00590); + (0x005A2,0x005A2); + (0x005BA,0x005BA); + (0x005C5,0x005CF); + (0x005EB,0x005EF); + (0x005F5,0x0060B); + (0x0060D,0x0061A); + (0x0061C,0x0061E); + (0x00620,0x00620); + (0x0063B,0x0063F); + (0x00656,0x0065F); + (0x006EE,0x006EF); + (0x006FF,0x006FF); + (0x0070E,0x0070E); + (0x0072D,0x0072F); + (0x0074B,0x0077F); + (0x007B2,0x00900); + (0x00904,0x00904); + (0x0093A,0x0093B); + (0x0094E,0x0094F); + (0x00955,0x00957); + (0x00971,0x00980); + (0x00984,0x00984); + (0x0098D,0x0098E); + (0x00991,0x00992); + (0x009A9,0x009A9); + (0x009B1,0x009B1); + (0x009B3,0x009B5); + (0x009BA,0x009BB); + (0x009BD,0x009BD); + (0x009C5,0x009C6); + (0x009C9,0x009CA); + (0x009CE,0x009D6); + (0x009D8,0x009DB); + (0x009DE,0x009DE); + (0x009E4,0x009E5); + (0x009FB,0x00A01); + (0x00A03,0x00A04); + (0x00A0B,0x00A0E); + (0x00A11,0x00A12); + (0x00A29,0x00A29); + (0x00A31,0x00A31); + (0x00A34,0x00A34); + (0x00A37,0x00A37); + (0x00A3A,0x00A3B); + (0x00A3D,0x00A3D); + (0x00A43,0x00A46); + (0x00A49,0x00A4A); + (0x00A4E,0x00A58); + (0x00A5D,0x00A5D); + (0x00A5F,0x00A65); + (0x00A75,0x00A80); + (0x00A84,0x00A84); + (0x00A8C,0x00A8C); + (0x00A8E,0x00A8E); + (0x00A92,0x00A92); + (0x00AA9,0x00AA9); + (0x00AB1,0x00AB1); + (0x00AB4,0x00AB4); + (0x00ABA,0x00ABB); + (0x00AC6,0x00AC6); + (0x00ACA,0x00ACA); + (0x00ACE,0x00ACF); + (0x00AD1,0x00ADF); + (0x00AE1,0x00AE5); + (0x00AF0,0x00B00); + (0x00B04,0x00B04); + (0x00B0D,0x00B0E); + (0x00B11,0x00B12); + (0x00B29,0x00B29); + (0x00B31,0x00B31); + (0x00B34,0x00B35); + (0x00B3A,0x00B3B); + (0x00B44,0x00B46); + (0x00B49,0x00B4A); + (0x00B4E,0x00B55); + (0x00B58,0x00B5B); + (0x00B5E,0x00B5E); + (0x00B62,0x00B65); + (0x00B71,0x00B81); + (0x00B84,0x00B84); + (0x00B8B,0x00B8D); + (0x00B91,0x00B91); + (0x00B96,0x00B98); + (0x00B9B,0x00B9B); + (0x00B9D,0x00B9D); + (0x00BA0,0x00BA2); + (0x00BA5,0x00BA7); + (0x00BAB,0x00BAD); + (0x00BB6,0x00BB6); + (0x00BBA,0x00BBD); + (0x00BC3,0x00BC5); + (0x00BC9,0x00BC9); + (0x00BCE,0x00BD6); + (0x00BD8,0x00BE6); + (0x00BF3,0x00C00); + (0x00C04,0x00C04); + (0x00C0D,0x00C0D); + (0x00C11,0x00C11); + (0x00C29,0x00C29); + (0x00C34,0x00C34); + (0x00C3A,0x00C3D); + (0x00C45,0x00C45); + (0x00C49,0x00C49); + (0x00C4E,0x00C54); + (0x00C57,0x00C5F); + (0x00C62,0x00C65); + (0x00C70,0x00C81); + (0x00C84,0x00C84); + (0x00C8D,0x00C8D); + (0x00C91,0x00C91); + (0x00CA9,0x00CA9); + (0x00CB4,0x00CB4); + (0x00CBA,0x00CBD); + (0x00CC5,0x00CC5); + (0x00CC9,0x00CC9); + (0x00CCE,0x00CD4); + (0x00CD7,0x00CDD); + (0x00CDF,0x00CDF); + (0x00CE2,0x00CE5); + (0x00CF0,0x00D01); + (0x00D04,0x00D04); + (0x00D0D,0x00D0D); + (0x00D11,0x00D11); + (0x00D29,0x00D29); + (0x00D3A,0x00D3D); + (0x00D44,0x00D45); + (0x00D49,0x00D49); + (0x00D4E,0x00D56); + (0x00D58,0x00D5F); + (0x00D62,0x00D65); + (0x00D70,0x00D81); + (0x00D84,0x00D84); + (0x00D97,0x00D99); + (0x00DB2,0x00DB2); + (0x00DBC,0x00DBC); + (0x00DBE,0x00DBF); + (0x00DC7,0x00DC9); + (0x00DCB,0x00DCE); + (0x00DD5,0x00DD5); + (0x00DD7,0x00DD7); + (0x00DE0,0x00DF1); + (0x00DF5,0x00E00); + (0x00E3B,0x00E3E); + (0x00E5C,0x00E80); + (0x00E83,0x00E83); + (0x00E85,0x00E86); + (0x00E89,0x00E89); + (0x00E8B,0x00E8C); + (0x00E8E,0x00E93); + (0x00E98,0x00E98); + (0x00EA0,0x00EA0); + (0x00EA4,0x00EA4); + (0x00EA6,0x00EA6); + (0x00EA8,0x00EA9); + (0x00EAC,0x00EAC); + (0x00EBA,0x00EBA); + (0x00EBE,0x00EBF); + (0x00EC5,0x00EC5); + (0x00EC7,0x00EC7); + (0x00ECE,0x00ECF); + (0x00EDA,0x00EDB); + (0x00EDE,0x00EFF); + (0x00F48,0x00F48); + (0x00F6B,0x00F70); + (0x00F8C,0x00F8F); + (0x00F98,0x00F98); + (0x00FBD,0x00FBD); + (0x00FCD,0x00FCE); + (0x00FD0,0x00FFF); + (0x01022,0x01022); + (0x01028,0x01028); + (0x0102B,0x0102B); + (0x01033,0x01035); + (0x0103A,0x0103F); + (0x0105A,0x0109F); + (0x010C6,0x010CF); + (0x010F9,0x010FA); + (0x010FC,0x010FF); + (0x0115A,0x0115E); + (0x011A3,0x011A7); + (0x011FA,0x011FF); + (0x01207,0x01207); + (0x01247,0x01247); + (0x01249,0x01249); + (0x0124E,0x0124F); + (0x01257,0x01257); + (0x01259,0x01259); + (0x0125E,0x0125F); + (0x01287,0x01287); + (0x01289,0x01289); + (0x0128E,0x0128F); + (0x012AF,0x012AF); + (0x012B1,0x012B1); + (0x012B6,0x012B7); + (0x012BF,0x012BF); + (0x012C1,0x012C1); + (0x012C6,0x012C7); + (0x012CF,0x012CF); + (0x012D7,0x012D7); + (0x012EF,0x012EF); + (0x0130F,0x0130F); + (0x01311,0x01311); + (0x01316,0x01317); + (0x0131F,0x0131F); + (0x01347,0x01347); + (0x0135B,0x01360); + (0x0137D,0x0139F); + (0x013F5,0x01400); + (0x01677,0x0167F); + (0x0169D,0x0169F); + (0x016F1,0x016FF); + (0x0170D,0x0170D); + (0x01715,0x0171F); + (0x01737,0x0173F); + (0x01754,0x0175F); + (0x0176D,0x0176D); + (0x01771,0x01771); + (0x01774,0x0177F); + (0x017DD,0x017DF); + (0x017EA,0x017FF); + (0x0180F,0x0180F); + (0x0181A,0x0181F); + (0x01878,0x0187F); + (0x018AA,0x01DFF); + (0x01E9C,0x01E9F); + (0x01EFA,0x01EFF); + (0x01F16,0x01F17); + (0x01F1E,0x01F1F); + (0x01F46,0x01F47); + (0x01F4E,0x01F4F); + (0x01F58,0x01F58); + (0x01F5A,0x01F5A); + (0x01F5C,0x01F5C); + (0x01F5E,0x01F5E); + (0x01F7E,0x01F7F); + (0x01FB5,0x01FB5); + (0x01FC5,0x01FC5); + (0x01FD4,0x01FD5); + (0x01FDC,0x01FDC); + (0x01FF0,0x01FF1); + (0x01FF5,0x01FF5); + (0x01FFF,0x01FFF); + (0x02053,0x02056); + (0x02058,0x0205E); + (0x02064,0x02069); + (0x02072,0x02073); + (0x0208F,0x0209F); + (0x020B2,0x020CF); + (0x020EB,0x020FF); + (0x0213B,0x0213C); + (0x0214C,0x02152); + (0x02184,0x0218F); + (0x023CF,0x023FF); + (0x02427,0x0243F); + (0x0244B,0x0245F); + (0x024FF,0x024FF); + (0x02614,0x02615); + (0x02618,0x02618); + (0x0267E,0x0267F); + (0x0268A,0x02700); + (0x02705,0x02705); + (0x0270A,0x0270B); + (0x02728,0x02728); + (0x0274C,0x0274C); + (0x0274E,0x0274E); + (0x02753,0x02755); + (0x02757,0x02757); + (0x0275F,0x02760); + (0x02795,0x02797); + (0x027B0,0x027B0); + (0x027BF,0x027CF); + (0x027EC,0x027EF); + (0x02B00,0x02E7F); + (0x02E9A,0x02E9A); + (0x02EF4,0x02EFF); + (0x02FD6,0x02FEF); + (0x02FFC,0x02FFF); + (0x03040,0x03040); + (0x03097,0x03098); + (0x03100,0x03104); + (0x0312D,0x03130); + (0x0318F,0x0318F); + (0x031B8,0x031EF); + (0x0321D,0x0321F); + (0x03244,0x03250); + (0x0327C,0x0327E); + (0x032CC,0x032CF); + (0x032FF,0x032FF); + (0x03377,0x0337A); + (0x033DE,0x033DF); + (0x033FF,0x033FF); + (0x04DB6,0x04DFF); + (0x09FA6,0x09FFF); + (0x0A48D,0x0A48F); + (0x0A4C7,0x0ABFF); + (0x0D7A4,0x0D7FF); + (0x0DEFF,0x0DFFE); + (0x0FA2E,0x0FA2F); + (0x0FA6B,0x0FAFF); + (0x0FB07,0x0FB12); + (0x0FB18,0x0FB1C); + (0x0FB37,0x0FB37); + (0x0FB3D,0x0FB3D); + (0x0FB3F,0x0FB3F); + (0x0FB42,0x0FB42); + (0x0FB45,0x0FB45); + (0x0FBB2,0x0FBD2); + (0x0FD40,0x0FD4F); + (0x0FD90,0x0FD91); + (0x0FDC8,0x0FDEF); + (0x0FDFD,0x0FDFF); + (0x0FE10,0x0FE1F); + (0x0FE24,0x0FE2F); + (0x0FE47,0x0FE48); + (0x0FE53,0x0FE53); + (0x0FE67,0x0FE67); + (0x0FE6C,0x0FE6F); + (0x0FE75,0x0FE75); + (0x0FEFD,0x0FEFE); + (0x0FF00,0x0FF00); + (0x0FFBF,0x0FFC1); + (0x0FFC8,0x0FFC9); + (0x0FFD0,0x0FFD1); + (0x0FFD8,0x0FFD9); + (0x0FFDD,0x0FFDF); + (0x0FFE7,0x0FFE7); + (0x0FFEF,0x0FFF8); + (0x0FFFE,0x102FF); + (0x1031F,0x1031F); + (0x10324,0x1032F); + (0x1034B,0x103FF); + (0x10426,0x10427); + (0x1044E,0x1CFFF); + (0x1D0F6,0x1D0FF); + (0x1D127,0x1D129); + (0x1D1DE,0x1D3FF); + (0x1D455,0x1D455); + (0x1D49D,0x1D49D); + (0x1D4A0,0x1D4A1); + (0x1D4A3,0x1D4A4); + (0x1D4A7,0x1D4A8); + (0x1D4AD,0x1D4AD); + (0x1D4BA,0x1D4BA); + (0x1D4BC,0x1D4BC); + (0x1D4C1,0x1D4C1); + (0x1D4C4,0x1D4C4); + (0x1D506,0x1D506); + (0x1D50B,0x1D50C); + (0x1D515,0x1D515); + (0x1D51D,0x1D51D); + (0x1D53A,0x1D53A); + (0x1D53F,0x1D53F); + (0x1D545,0x1D545); + (0x1D547,0x1D549); + (0x1D551,0x1D551); + (0x1D6A4,0x1D6A7); + (0x1D7CA,0x1D7CD); + (0x1D800,0x1FFFF); + (0x2A6D7,0x2F7FF); + (0x2FA1E,0xE0000); + (0xE0002,0xE001F); + (0xE0080,0x7FFFFFFF) +] +(* Letter, Modifier *) +let lm = [ + (0x002B0,0x002B8); + (0x002BB,0x002C1); + (0x002D0,0x002D1); + (0x002E0,0x002E4); + (0x002EE,0x002EE); + (0x0037A,0x0037A); + (0x00559,0x00559); + (0x00640,0x00640); + (0x006E5,0x006E6); + (0x00E46,0x00E46); + (0x00EC6,0x00EC6); + (0x017D7,0x017D7); + (0x01843,0x01843); + (0x03005,0x03005); + (0x03031,0x03035); + (0x0303B,0x0303B); + (0x0309D,0x0309E); + (0x030FC,0x030FE); + (0x0FF70,0x0FF70); + (0x0FF9E,0x0FF9F) +] +(* Letter, Other *) +let lo = [ + (0x001BB,0x001BB); + (0x001C0,0x001C3); + (0x005D0,0x005EA); + (0x005F0,0x005F2); + (0x00621,0x0063A); + (0x00641,0x0064A); + (0x0066E,0x0066F); + (0x00671,0x006D3); + (0x006D5,0x006D5); + (0x006FA,0x006FC); + (0x00710,0x00710); + (0x00712,0x0072C); + (0x00780,0x007A5); + (0x007B1,0x007B1); + (0x00905,0x00939); + (0x0093D,0x0093D); + (0x00950,0x00950); + (0x00958,0x00961); + (0x00985,0x0098C); + (0x0098F,0x00990); + (0x00993,0x009A8); + (0x009AA,0x009B0); + (0x009B2,0x009B2); + (0x009B6,0x009B9); + (0x009DC,0x009DD); + (0x009DF,0x009E1); + (0x009F0,0x009F1); + (0x00A05,0x00A0A); + (0x00A0F,0x00A10); + (0x00A13,0x00A28); + (0x00A2A,0x00A30); + (0x00A32,0x00A33); + (0x00A35,0x00A36); + (0x00A38,0x00A39); + (0x00A59,0x00A5C); + (0x00A5E,0x00A5E); + (0x00A72,0x00A74); + (0x00A85,0x00A8B); + (0x00A8D,0x00A8D); + (0x00A8F,0x00A91); + (0x00A93,0x00AA8); + (0x00AAA,0x00AB0); + (0x00AB2,0x00AB3); + (0x00AB5,0x00AB9); + (0x00ABD,0x00ABD); + (0x00AD0,0x00AD0); + (0x00AE0,0x00AE0); + (0x00B05,0x00B0C); + (0x00B0F,0x00B10); + (0x00B13,0x00B28); + (0x00B2A,0x00B30); + (0x00B32,0x00B33); + (0x00B36,0x00B39); + (0x00B3D,0x00B3D); + (0x00B5C,0x00B5D); + (0x00B5F,0x00B61); + (0x00B83,0x00B83); + (0x00B85,0x00B8A); + (0x00B8E,0x00B90); + (0x00B92,0x00B95); + (0x00B99,0x00B9A); + (0x00B9C,0x00B9C); + (0x00B9E,0x00B9F); + (0x00BA3,0x00BA4); + (0x00BA8,0x00BAA); + (0x00BAE,0x00BB5); + (0x00BB7,0x00BB9); + (0x00C05,0x00C0C); + (0x00C0E,0x00C10); + (0x00C12,0x00C28); + (0x00C2A,0x00C33); + (0x00C35,0x00C39); + (0x00C60,0x00C61); + (0x00C85,0x00C8C); + (0x00C8E,0x00C90); + (0x00C92,0x00CA8); + (0x00CAA,0x00CB3); + (0x00CB5,0x00CB9); + (0x00CDE,0x00CDE); + (0x00CE0,0x00CE1); + (0x00D05,0x00D0C); + (0x00D0E,0x00D10); + (0x00D12,0x00D28); + (0x00D2A,0x00D39); + (0x00D60,0x00D61); + (0x00D85,0x00D96); + (0x00D9A,0x00DB1); + (0x00DB3,0x00DBB); + (0x00DBD,0x00DBD); + (0x00DC0,0x00DC6); + (0x00E01,0x00E30); + (0x00E32,0x00E33); + (0x00E40,0x00E45); + (0x00E81,0x00E82); + (0x00E84,0x00E84); + (0x00E87,0x00E88); + (0x00E8A,0x00E8A); + (0x00E8D,0x00E8D); + (0x00E94,0x00E97); + (0x00E99,0x00E9F); + (0x00EA1,0x00EA3); + (0x00EA5,0x00EA5); + (0x00EA7,0x00EA7); + (0x00EAA,0x00EAB); + (0x00EAD,0x00EB0); + (0x00EB2,0x00EB3); + (0x00EBD,0x00EBD); + (0x00EC0,0x00EC4); + (0x00EDC,0x00EDD); + (0x00F00,0x00F00); + (0x00F40,0x00F47); + (0x00F49,0x00F6A); + (0x00F88,0x00F8B); + (0x01000,0x01021); + (0x01023,0x01027); + (0x01029,0x0102A); + (0x01050,0x01055); + (0x010D0,0x010F8); + (0x01100,0x01159); + (0x0115F,0x011A2); + (0x011A8,0x011F9); + (0x01200,0x01206); + (0x01208,0x01246); + (0x01248,0x01248); + (0x0124A,0x0124D); + (0x01250,0x01256); + (0x01258,0x01258); + (0x0125A,0x0125D); + (0x01260,0x01286); + (0x01288,0x01288); + (0x0128A,0x0128D); + (0x01290,0x012AE); + (0x012B0,0x012B0); + (0x012B2,0x012B5); + (0x012B8,0x012BE); + (0x012C0,0x012C0); + (0x012C2,0x012C5); + (0x012C8,0x012CE); + (0x012D0,0x012D6); + (0x012D8,0x012EE); + (0x012F0,0x0130E); + (0x01310,0x01310); + (0x01312,0x01315); + (0x01318,0x0131E); + (0x01320,0x01346); + (0x01348,0x0135A); + (0x013A0,0x013F4); + (0x01401,0x0166C); + (0x0166F,0x01676); + (0x01681,0x0169A); + (0x016A0,0x016EA); + (0x01700,0x0170C); + (0x0170E,0x01711); + (0x01720,0x01731); + (0x01740,0x01751); + (0x01760,0x0176C); + (0x0176E,0x01770); + (0x01780,0x017B3); + (0x017DC,0x017DC); + (0x01820,0x01842); + (0x01844,0x01877); + (0x01880,0x018A8); + (0x02135,0x02138); + (0x03006,0x03006); + (0x0303C,0x0303C); + (0x03041,0x03096); + (0x0309F,0x0309F); + (0x030A1,0x030FA); + (0x030FF,0x030FF); + (0x03105,0x0312C); + (0x03131,0x0318E); + (0x031A0,0x031B7); + (0x031F0,0x031FF); + (0x03400,0x04DB5); + (0x04E00,0x09FA5); + (0x0A000,0x0A48C); + (0x0AC00,0x0D7A3); + (0x0F900,0x0FA2D); + (0x0FA30,0x0FA6A); + (0x0FB1D,0x0FB1D); + (0x0FB1F,0x0FB28); + (0x0FB2A,0x0FB36); + (0x0FB38,0x0FB3C); + (0x0FB3E,0x0FB3E); + (0x0FB40,0x0FB41); + (0x0FB43,0x0FB44); + (0x0FB46,0x0FBB1); + (0x0FBD3,0x0FD3D); + (0x0FD50,0x0FD8F); + (0x0FD92,0x0FDC7); + (0x0FDF0,0x0FDFB); + (0x0FE70,0x0FE74); + (0x0FE76,0x0FEFC); + (0x0FF66,0x0FF6F); + (0x0FF71,0x0FF9D); + (0x0FFA0,0x0FFBE); + (0x0FFC2,0x0FFC7); + (0x0FFCA,0x0FFCF); + (0x0FFD2,0x0FFD7); + (0x0FFDA,0x0FFDC); + (0x10300,0x1031E); + (0x10330,0x10349); + (0x20000,0x2A6D6); + (0x2F800,0x2FA1D) +] +(* Punctuation, Connector *) +let pc = [ + (0x0005F,0x0005F); + (0x0203F,0x02040); + (0x030FB,0x030FB); + (0x0FE33,0x0FE34); + (0x0FE4D,0x0FE4F); + (0x0FF3F,0x0FF3F); + (0x0FF65,0x0FF65) +] +(* Punctuation, Dash *) +let pd = [ + (0x0002D,0x0002D); + (0x000AD,0x000AD); + (0x0058A,0x0058A); + (0x01806,0x01806); + (0x02010,0x02015); + (0x0301C,0x0301C); + (0x03030,0x03030); + (0x030A0,0x030A0); + (0x0FE31,0x0FE32); + (0x0FE58,0x0FE58); + (0x0FE63,0x0FE63); + (0x0FF0D,0x0FF0D) +] +(* Punctuation, Open *) +let ps = [ + (0x00028,0x00028); + (0x0005B,0x0005B); + (0x0007B,0x0007B); + (0x00F3A,0x00F3A); + (0x00F3C,0x00F3C); + (0x0169B,0x0169B); + (0x0201A,0x0201A); + (0x0201E,0x0201E); + (0x02045,0x02045); + (0x0207D,0x0207D); + (0x0208D,0x0208D); + (0x02329,0x02329); + (0x023B4,0x023B4); + (0x02768,0x02768); + (0x0276A,0x0276A); + (0x0276C,0x0276C); + (0x0276E,0x0276E); + (0x02770,0x02770); + (0x02772,0x02772); + (0x02774,0x02774); + (0x027E6,0x027E6); + (0x027E8,0x027E8); + (0x027EA,0x027EA); + (0x02983,0x02983); + (0x02985,0x02985); + (0x02987,0x02987); + (0x02989,0x02989); + (0x0298B,0x0298B); + (0x0298D,0x0298D); + (0x0298F,0x0298F); + (0x02991,0x02991); + (0x02993,0x02993); + (0x02995,0x02995); + (0x02997,0x02997); + (0x029D8,0x029D8); + (0x029DA,0x029DA); + (0x029FC,0x029FC); + (0x03008,0x03008); + (0x0300A,0x0300A); + (0x0300C,0x0300C); + (0x0300E,0x0300E); + (0x03010,0x03010); + (0x03014,0x03014); + (0x03016,0x03016); + (0x03018,0x03018); + (0x0301A,0x0301A); + (0x0301D,0x0301D); + (0x0FD3E,0x0FD3E); + (0x0FE35,0x0FE35); + (0x0FE37,0x0FE37); + (0x0FE39,0x0FE39); + (0x0FE3B,0x0FE3B); + (0x0FE3D,0x0FE3D); + (0x0FE3F,0x0FE3F); + (0x0FE41,0x0FE41); + (0x0FE43,0x0FE43); + (0x0FE59,0x0FE59); + (0x0FE5B,0x0FE5B); + (0x0FE5D,0x0FE5D); + (0x0FF08,0x0FF08); + (0x0FF3B,0x0FF3B); + (0x0FF5B,0x0FF5B); + (0x0FF5F,0x0FF5F); + (0x0FF62,0x0FF62) +] +(* Punctuation, Close *) +let pe = [ + (0x00029,0x00029); + (0x0005D,0x0005D); + (0x0007D,0x0007D); + (0x00F3B,0x00F3B); + (0x00F3D,0x00F3D); + (0x0169C,0x0169C); + (0x02046,0x02046); + (0x0207E,0x0207E); + (0x0208E,0x0208E); + (0x0232A,0x0232A); + (0x023B5,0x023B5); + (0x02769,0x02769); + (0x0276B,0x0276B); + (0x0276D,0x0276D); + (0x0276F,0x0276F); + (0x02771,0x02771); + (0x02773,0x02773); + (0x02775,0x02775); + (0x027E7,0x027E7); + (0x027E9,0x027E9); + (0x027EB,0x027EB); + (0x02984,0x02984); + (0x02986,0x02986); + (0x02988,0x02988); + (0x0298A,0x0298A); + (0x0298C,0x0298C); + (0x0298E,0x0298E); + (0x02990,0x02990); + (0x02992,0x02992); + (0x02994,0x02994); + (0x02996,0x02996); + (0x02998,0x02998); + (0x029D9,0x029D9); + (0x029DB,0x029DB); + (0x029FD,0x029FD); + (0x03009,0x03009); + (0x0300B,0x0300B); + (0x0300D,0x0300D); + (0x0300F,0x0300F); + (0x03011,0x03011); + (0x03015,0x03015); + (0x03017,0x03017); + (0x03019,0x03019); + (0x0301B,0x0301B); + (0x0301E,0x0301F); + (0x0FD3F,0x0FD3F); + (0x0FE36,0x0FE36); + (0x0FE38,0x0FE38); + (0x0FE3A,0x0FE3A); + (0x0FE3C,0x0FE3C); + (0x0FE3E,0x0FE3E); + (0x0FE40,0x0FE40); + (0x0FE42,0x0FE42); + (0x0FE44,0x0FE44); + (0x0FE5A,0x0FE5A); + (0x0FE5C,0x0FE5C); + (0x0FE5E,0x0FE5E); + (0x0FF09,0x0FF09); + (0x0FF3D,0x0FF3D); + (0x0FF5D,0x0FF5D); + (0x0FF60,0x0FF60); + (0x0FF63,0x0FF63) +] +(* Punctuation, Initial quote *) +let pi = [ + (0x000AB,0x000AB); + (0x02018,0x02018); + (0x0201B,0x0201C); + (0x0201F,0x0201F); + (0x02039,0x02039) +] +(* Punctuation, Final quote *) +let pf = [ + (0x000BB,0x000BB); + (0x02019,0x02019); + (0x0201D,0x0201D); + (0x0203A,0x0203A) +] +(* Punctuation, Other *) +let po = [ + (0x00021,0x00023); + (0x00025,0x00027); + (0x0002A,0x0002A); + (0x0002C,0x0002C); + (0x0002E,0x0002F); + (0x0003A,0x0003B); + (0x0003F,0x00040); + (0x0005C,0x0005C); + (0x000A1,0x000A1); + (0x000B7,0x000B7); + (0x000BF,0x000BF); + (0x0037E,0x0037E); + (0x00387,0x00387); + (0x0055A,0x0055F); + (0x00589,0x00589); + (0x005BE,0x005BE); + (0x005C0,0x005C0); + (0x005C3,0x005C3); + (0x005F3,0x005F4); + (0x0060C,0x0060C); + (0x0061B,0x0061B); + (0x0061F,0x0061F); + (0x0066A,0x0066D); + (0x006D4,0x006D4); + (0x00700,0x0070D); + (0x00964,0x00965); + (0x00970,0x00970); + (0x00DF4,0x00DF4); + (0x00E4F,0x00E4F); + (0x00E5A,0x00E5B); + (0x00F04,0x00F12); + (0x00F85,0x00F85); + (0x0104A,0x0104F); + (0x010FB,0x010FB); + (0x01361,0x01368); + (0x0166D,0x0166E); + (0x016EB,0x016ED); + (0x01735,0x01736); + (0x017D4,0x017D6); + (0x017D8,0x017DA); + (0x01800,0x01805); + (0x01807,0x0180A); + (0x02016,0x02017); + (0x02020,0x02027); + (0x02030,0x02038); + (0x0203B,0x0203E); + (0x02041,0x02043); + (0x02047,0x02051); + (0x02057,0x02057); + (0x023B6,0x023B6); + (0x03001,0x03003); + (0x0303D,0x0303D); + (0x0FE30,0x0FE30); + (0x0FE45,0x0FE46); + (0x0FE49,0x0FE4C); + (0x0FE50,0x0FE52); + (0x0FE54,0x0FE57); + (0x0FE5F,0x0FE61); + (0x0FE68,0x0FE68); + (0x0FE6A,0x0FE6B); + (0x0FF01,0x0FF03); + (0x0FF05,0x0FF07); + (0x0FF0A,0x0FF0A); + (0x0FF0C,0x0FF0C); + (0x0FF0E,0x0FF0F); + (0x0FF1A,0x0FF1B); + (0x0FF1F,0x0FF20); + (0x0FF3C,0x0FF3C); + (0x0FF61,0x0FF61); + (0x0FF64,0x0FF64) +] +(* Symbol, Math *) +let sm = [ + (0x0002B,0x0002B); + (0x0003C,0x0003E); + (0x0007C,0x0007C); + (0x0007E,0x0007E); + (0x000AC,0x000AC); + (0x000B1,0x000B1); + (0x000D7,0x000D7); + (0x000F7,0x000F7); + (0x003F6,0x003F6); + (0x02044,0x02044); + (0x02052,0x02052); + (0x0207A,0x0207C); + (0x0208A,0x0208C); + (0x02140,0x02144); + (0x0214B,0x0214B); + (0x02190,0x02194); + (0x0219A,0x0219B); + (0x021A0,0x021A0); + (0x021A3,0x021A3); + (0x021A6,0x021A6); + (0x021AE,0x021AE); + (0x021CE,0x021CF); + (0x021D2,0x021D2); + (0x021D4,0x021D4); + (0x021F4,0x022FF); + (0x02308,0x0230B); + (0x02320,0x02321); + (0x0237C,0x0237C); + (0x0239B,0x023B3); + (0x025B7,0x025B7); + (0x025C1,0x025C1); + (0x025F8,0x025FF); + (0x0266F,0x0266F); + (0x027D0,0x027E5); + (0x027F0,0x027FF); + (0x02900,0x02982); + (0x02999,0x029D7); + (0x029DC,0x029FB); + (0x029FE,0x02AFF); + (0x0FB29,0x0FB29); + (0x0FE62,0x0FE62); + (0x0FE64,0x0FE66); + (0x0FF0B,0x0FF0B); + (0x0FF1C,0x0FF1E); + (0x0FF5C,0x0FF5C); + (0x0FF5E,0x0FF5E); + (0x0FFE2,0x0FFE2); + (0x0FFE9,0x0FFEC); + (0x1D6C1,0x1D6C1); + (0x1D6DB,0x1D6DB); + (0x1D6FB,0x1D6FB); + (0x1D715,0x1D715); + (0x1D735,0x1D735); + (0x1D74F,0x1D74F); + (0x1D76F,0x1D76F); + (0x1D789,0x1D789); + (0x1D7A9,0x1D7A9); + (0x1D7C3,0x1D7C3) +] +(* Symbol, Currency *) +let sc = [ + (0x00024,0x00024); + (0x000A2,0x000A5); + (0x009F2,0x009F3); + (0x00E3F,0x00E3F); + (0x017DB,0x017DB); + (0x020A0,0x020B1); + (0x0FDFC,0x0FDFC); + (0x0FE69,0x0FE69); + (0x0FF04,0x0FF04); + (0x0FFE0,0x0FFE1); + (0x0FFE5,0x0FFE6) +] +(* Symbol, Modifier *) +let sk = [ + (0x0005E,0x0005E); + (0x00060,0x00060); + (0x000A8,0x000A8); + (0x000AF,0x000AF); + (0x000B4,0x000B4); + (0x000B8,0x000B8); + (0x002B9,0x002BA); + (0x002C2,0x002CF); + (0x002D2,0x002DF); + (0x002E5,0x002ED); + (0x00374,0x00375); + (0x00384,0x00385); + (0x01FBD,0x01FBD); + (0x01FBF,0x01FC1); + (0x01FCD,0x01FCF); + (0x01FDD,0x01FDF); + (0x01FED,0x01FEF); + (0x01FFD,0x01FFE); + (0x0309B,0x0309C); + (0x0FF3E,0x0FF3E); + (0x0FF40,0x0FF40); + (0x0FFE3,0x0FFE3) +] +(* Symbol, Other *) +let so = [ + (0x000A6,0x000A7); + (0x000A9,0x000A9); + (0x000AE,0x000AE); + (0x000B0,0x000B0); + (0x000B6,0x000B6); + (0x00482,0x00482); + (0x006E9,0x006E9); + (0x006FD,0x006FE); + (0x009FA,0x009FA); + (0x00B70,0x00B70); + (0x00F01,0x00F03); + (0x00F13,0x00F17); + (0x00F1A,0x00F1F); + (0x00F34,0x00F34); + (0x00F36,0x00F36); + (0x00F38,0x00F38); + (0x00FBE,0x00FC5); + (0x00FC7,0x00FCC); + (0x00FCF,0x00FCF); + (0x02100,0x02101); + (0x02103,0x02106); + (0x02108,0x02109); + (0x02114,0x02114); + (0x02116,0x02118); + (0x0211E,0x02123); + (0x02125,0x02125); + (0x02127,0x02127); + (0x02129,0x02129); + (0x0212E,0x0212E); + (0x02132,0x02132); + (0x0213A,0x0213A); + (0x0214A,0x0214A); + (0x02195,0x02199); + (0x0219C,0x0219F); + (0x021A1,0x021A2); + (0x021A4,0x021A5); + (0x021A7,0x021AD); + (0x021AF,0x021CD); + (0x021D0,0x021D1); + (0x021D3,0x021D3); + (0x021D5,0x021F3); + (0x02300,0x02307); + (0x0230C,0x0231F); + (0x02322,0x02328); + (0x0232B,0x0237B); + (0x0237D,0x0239A); + (0x023B7,0x023CE); + (0x02400,0x02426); + (0x02440,0x0244A); + (0x0249C,0x024E9); + (0x02500,0x025B6); + (0x025B8,0x025C0); + (0x025C2,0x025F7); + (0x02600,0x02613); + (0x02616,0x02617); + (0x02619,0x0266E); + (0x02670,0x0267D); + (0x02680,0x02689); + (0x02701,0x02704); + (0x02706,0x02709); + (0x0270C,0x02727); + (0x02729,0x0274B); + (0x0274D,0x0274D); + (0x0274F,0x02752); + (0x02756,0x02756); + (0x02758,0x0275E); + (0x02761,0x02767); + (0x02794,0x02794); + (0x02798,0x027AF); + (0x027B1,0x027BE); + (0x02800,0x028FF); + (0x02E80,0x02E99); + (0x02E9B,0x02EF3); + (0x02F00,0x02FD5); + (0x02FF0,0x02FFB); + (0x03004,0x03004); + (0x03012,0x03013); + (0x03020,0x03020); + (0x03036,0x03037); + (0x0303E,0x0303F); + (0x03190,0x03191); + (0x03196,0x0319F); + (0x03200,0x0321C); + (0x0322A,0x03243); + (0x03260,0x0327B); + (0x0327F,0x0327F); + (0x0328A,0x032B0); + (0x032C0,0x032CB); + (0x032D0,0x032FE); + (0x03300,0x03376); + (0x0337B,0x033DD); + (0x033E0,0x033FE); + (0x0A490,0x0A4C6); + (0x0FFE4,0x0FFE4); + (0x0FFE8,0x0FFE8); + (0x0FFED,0x0FFEE); + (0x0FFFC,0x0FFFD); + (0x1D000,0x1D0F5); + (0x1D100,0x1D126); + (0x1D12A,0x1D164); + (0x1D16A,0x1D16C); + (0x1D183,0x1D184); + (0x1D18C,0x1D1A9); + (0x1D1AE,0x1D1DD) +] + +(* Conversion to lower case. *) +let to_lower = [ + (0x00041,0x0005A), `Delta (32); + (0x000C0,0x000D6), `Delta (32); + (0x000D8,0x000DE), `Delta (32); + (0x00100,0x00100), `Abs (0x00101); + (0x00102,0x00102), `Abs (0x00103); + (0x00104,0x00104), `Abs (0x00105); + (0x00106,0x00106), `Abs (0x00107); + (0x00108,0x00108), `Abs (0x00109); + (0x0010A,0x0010A), `Abs (0x0010B); + (0x0010C,0x0010C), `Abs (0x0010D); + (0x0010E,0x0010E), `Abs (0x0010F); + (0x00110,0x00110), `Abs (0x00111); + (0x00112,0x00112), `Abs (0x00113); + (0x00114,0x00114), `Abs (0x00115); + (0x00116,0x00116), `Abs (0x00117); + (0x00118,0x00118), `Abs (0x00119); + (0x0011A,0x0011A), `Abs (0x0011B); + (0x0011C,0x0011C), `Abs (0x0011D); + (0x0011E,0x0011E), `Abs (0x0011F); + (0x00120,0x00120), `Abs (0x00121); + (0x00122,0x00122), `Abs (0x00123); + (0x00124,0x00124), `Abs (0x00125); + (0x00126,0x00126), `Abs (0x00127); + (0x00128,0x00128), `Abs (0x00129); + (0x0012A,0x0012A), `Abs (0x0012B); + (0x0012C,0x0012C), `Abs (0x0012D); + (0x0012E,0x0012E), `Abs (0x0012F); + (0x00130,0x00130), `Abs (0x00069); + (0x00132,0x00132), `Abs (0x00133); + (0x00134,0x00134), `Abs (0x00135); + (0x00136,0x00136), `Abs (0x00137); + (0x00139,0x00139), `Abs (0x0013A); + (0x0013B,0x0013B), `Abs (0x0013C); + (0x0013D,0x0013D), `Abs (0x0013E); + (0x0013F,0x0013F), `Abs (0x00140); + (0x00141,0x00141), `Abs (0x00142); + (0x00143,0x00143), `Abs (0x00144); + (0x00145,0x00145), `Abs (0x00146); + (0x00147,0x00147), `Abs (0x00148); + (0x0014A,0x0014A), `Abs (0x0014B); + (0x0014C,0x0014C), `Abs (0x0014D); + (0x0014E,0x0014E), `Abs (0x0014F); + (0x00150,0x00150), `Abs (0x00151); + (0x00152,0x00152), `Abs (0x00153); + (0x00154,0x00154), `Abs (0x00155); + (0x00156,0x00156), `Abs (0x00157); + (0x00158,0x00158), `Abs (0x00159); + (0x0015A,0x0015A), `Abs (0x0015B); + (0x0015C,0x0015C), `Abs (0x0015D); + (0x0015E,0x0015E), `Abs (0x0015F); + (0x00160,0x00160), `Abs (0x00161); + (0x00162,0x00162), `Abs (0x00163); + (0x00164,0x00164), `Abs (0x00165); + (0x00166,0x00166), `Abs (0x00167); + (0x00168,0x00168), `Abs (0x00169); + (0x0016A,0x0016A), `Abs (0x0016B); + (0x0016C,0x0016C), `Abs (0x0016D); + (0x0016E,0x0016E), `Abs (0x0016F); + (0x00170,0x00170), `Abs (0x00171); + (0x00172,0x00172), `Abs (0x00173); + (0x00174,0x00174), `Abs (0x00175); + (0x00176,0x00176), `Abs (0x00177); + (0x00178,0x00178), `Abs (0x000FF); + (0x00179,0x00179), `Abs (0x0017A); + (0x0017B,0x0017B), `Abs (0x0017C); + (0x0017D,0x0017D), `Abs (0x0017E); + (0x00181,0x00181), `Abs (0x00253); + (0x00182,0x00182), `Abs (0x00183); + (0x00184,0x00184), `Abs (0x00185); + (0x00186,0x00186), `Abs (0x00254); + (0x00187,0x00187), `Abs (0x00188); + (0x00189,0x0018A), `Delta (205); + (0x0018B,0x0018B), `Abs (0x0018C); + (0x0018E,0x0018E), `Abs (0x001DD); + (0x0018F,0x0018F), `Abs (0x00259); + (0x00190,0x00190), `Abs (0x0025B); + (0x00191,0x00191), `Abs (0x00192); + (0x00193,0x00193), `Abs (0x00260); + (0x00194,0x00194), `Abs (0x00263); + (0x00196,0x00196), `Abs (0x00269); + (0x00197,0x00197), `Abs (0x00268); + (0x00198,0x00198), `Abs (0x00199); + (0x0019C,0x0019C), `Abs (0x0026F); + (0x0019D,0x0019D), `Abs (0x00272); + (0x0019F,0x0019F), `Abs (0x00275); + (0x001A0,0x001A0), `Abs (0x001A1); + (0x001A2,0x001A2), `Abs (0x001A3); + (0x001A4,0x001A4), `Abs (0x001A5); + (0x001A6,0x001A6), `Abs (0x00280); + (0x001A7,0x001A7), `Abs (0x001A8); + (0x001A9,0x001A9), `Abs (0x00283); + (0x001AC,0x001AC), `Abs (0x001AD); + (0x001AE,0x001AE), `Abs (0x00288); + (0x001AF,0x001AF), `Abs (0x001B0); + (0x001B1,0x001B2), `Delta (217); + (0x001B3,0x001B3), `Abs (0x001B4); + (0x001B5,0x001B5), `Abs (0x001B6); + (0x001B7,0x001B7), `Abs (0x00292); + (0x001B8,0x001B8), `Abs (0x001B9); + (0x001BC,0x001BC), `Abs (0x001BD); + (0x001C4,0x001C4), `Abs (0x001C6); + (0x001C7,0x001C7), `Abs (0x001C9); + (0x001CA,0x001CA), `Abs (0x001CC); + (0x001CD,0x001CD), `Abs (0x001CE); + (0x001CF,0x001CF), `Abs (0x001D0); + (0x001D1,0x001D1), `Abs (0x001D2); + (0x001D3,0x001D3), `Abs (0x001D4); + (0x001D5,0x001D5), `Abs (0x001D6); + (0x001D7,0x001D7), `Abs (0x001D8); + (0x001D9,0x001D9), `Abs (0x001DA); + (0x001DB,0x001DB), `Abs (0x001DC); + (0x001DE,0x001DE), `Abs (0x001DF); + (0x001E0,0x001E0), `Abs (0x001E1); + (0x001E2,0x001E2), `Abs (0x001E3); + (0x001E4,0x001E4), `Abs (0x001E5); + (0x001E6,0x001E6), `Abs (0x001E7); + (0x001E8,0x001E8), `Abs (0x001E9); + (0x001EA,0x001EA), `Abs (0x001EB); + (0x001EC,0x001EC), `Abs (0x001ED); + (0x001EE,0x001EE), `Abs (0x001EF); + (0x001F1,0x001F1), `Abs (0x001F3); + (0x001F4,0x001F4), `Abs (0x001F5); + (0x001F6,0x001F6), `Abs (0x00195); + (0x001F7,0x001F7), `Abs (0x001BF); + (0x001F8,0x001F8), `Abs (0x001F9); + (0x001FA,0x001FA), `Abs (0x001FB); + (0x001FC,0x001FC), `Abs (0x001FD); + (0x001FE,0x001FE), `Abs (0x001FF); + (0x00200,0x00200), `Abs (0x00201); + (0x00202,0x00202), `Abs (0x00203); + (0x00204,0x00204), `Abs (0x00205); + (0x00206,0x00206), `Abs (0x00207); + (0x00208,0x00208), `Abs (0x00209); + (0x0020A,0x0020A), `Abs (0x0020B); + (0x0020C,0x0020C), `Abs (0x0020D); + (0x0020E,0x0020E), `Abs (0x0020F); + (0x00210,0x00210), `Abs (0x00211); + (0x00212,0x00212), `Abs (0x00213); + (0x00214,0x00214), `Abs (0x00215); + (0x00216,0x00216), `Abs (0x00217); + (0x00218,0x00218), `Abs (0x00219); + (0x0021A,0x0021A), `Abs (0x0021B); + (0x0021C,0x0021C), `Abs (0x0021D); + (0x0021E,0x0021E), `Abs (0x0021F); + (0x00220,0x00220), `Abs (0x0019E); + (0x00222,0x00222), `Abs (0x00223); + (0x00224,0x00224), `Abs (0x00225); + (0x00226,0x00226), `Abs (0x00227); + (0x00228,0x00228), `Abs (0x00229); + (0x0022A,0x0022A), `Abs (0x0022B); + (0x0022C,0x0022C), `Abs (0x0022D); + (0x0022E,0x0022E), `Abs (0x0022F); + (0x00230,0x00230), `Abs (0x00231); + (0x00232,0x00232), `Abs (0x00233); + (0x00386,0x00386), `Abs (0x003AC); + (0x00388,0x0038A), `Delta (37); + (0x0038C,0x0038C), `Abs (0x003CC); + (0x0038E,0x0038F), `Delta (63); + (0x00391,0x003A1), `Delta (32); + (0x003A3,0x003AB), `Delta (32); + (0x003D8,0x003D8), `Abs (0x003D9); + (0x003DA,0x003DA), `Abs (0x003DB); + (0x003DC,0x003DC), `Abs (0x003DD); + (0x003DE,0x003DE), `Abs (0x003DF); + (0x003E0,0x003E0), `Abs (0x003E1); + (0x003E2,0x003E2), `Abs (0x003E3); + (0x003E4,0x003E4), `Abs (0x003E5); + (0x003E6,0x003E6), `Abs (0x003E7); + (0x003E8,0x003E8), `Abs (0x003E9); + (0x003EA,0x003EA), `Abs (0x003EB); + (0x003EC,0x003EC), `Abs (0x003ED); + (0x003EE,0x003EE), `Abs (0x003EF); + (0x003F4,0x003F4), `Abs (0x003B8); + (0x00400,0x0040F), `Delta (80); + (0x00410,0x0042F), `Delta (32); + (0x00460,0x00460), `Abs (0x00461); + (0x00462,0x00462), `Abs (0x00463); + (0x00464,0x00464), `Abs (0x00465); + (0x00466,0x00466), `Abs (0x00467); + (0x00468,0x00468), `Abs (0x00469); + (0x0046A,0x0046A), `Abs (0x0046B); + (0x0046C,0x0046C), `Abs (0x0046D); + (0x0046E,0x0046E), `Abs (0x0046F); + (0x00470,0x00470), `Abs (0x00471); + (0x00472,0x00472), `Abs (0x00473); + (0x00474,0x00474), `Abs (0x00475); + (0x00476,0x00476), `Abs (0x00477); + (0x00478,0x00478), `Abs (0x00479); + (0x0047A,0x0047A), `Abs (0x0047B); + (0x0047C,0x0047C), `Abs (0x0047D); + (0x0047E,0x0047E), `Abs (0x0047F); + (0x00480,0x00480), `Abs (0x00481); + (0x0048A,0x0048A), `Abs (0x0048B); + (0x0048C,0x0048C), `Abs (0x0048D); + (0x0048E,0x0048E), `Abs (0x0048F); + (0x00490,0x00490), `Abs (0x00491); + (0x00492,0x00492), `Abs (0x00493); + (0x00494,0x00494), `Abs (0x00495); + (0x00496,0x00496), `Abs (0x00497); + (0x00498,0x00498), `Abs (0x00499); + (0x0049A,0x0049A), `Abs (0x0049B); + (0x0049C,0x0049C), `Abs (0x0049D); + (0x0049E,0x0049E), `Abs (0x0049F); + (0x004A0,0x004A0), `Abs (0x004A1); + (0x004A2,0x004A2), `Abs (0x004A3); + (0x004A4,0x004A4), `Abs (0x004A5); + (0x004A6,0x004A6), `Abs (0x004A7); + (0x004A8,0x004A8), `Abs (0x004A9); + (0x004AA,0x004AA), `Abs (0x004AB); + (0x004AC,0x004AC), `Abs (0x004AD); + (0x004AE,0x004AE), `Abs (0x004AF); + (0x004B0,0x004B0), `Abs (0x004B1); + (0x004B2,0x004B2), `Abs (0x004B3); + (0x004B4,0x004B4), `Abs (0x004B5); + (0x004B6,0x004B6), `Abs (0x004B7); + (0x004B8,0x004B8), `Abs (0x004B9); + (0x004BA,0x004BA), `Abs (0x004BB); + (0x004BC,0x004BC), `Abs (0x004BD); + (0x004BE,0x004BE), `Abs (0x004BF); + (0x004C1,0x004C1), `Abs (0x004C2); + (0x004C3,0x004C3), `Abs (0x004C4); + (0x004C5,0x004C5), `Abs (0x004C6); + (0x004C7,0x004C7), `Abs (0x004C8); + (0x004C9,0x004C9), `Abs (0x004CA); + (0x004CB,0x004CB), `Abs (0x004CC); + (0x004CD,0x004CD), `Abs (0x004CE); + (0x004D0,0x004D0), `Abs (0x004D1); + (0x004D2,0x004D2), `Abs (0x004D3); + (0x004D4,0x004D4), `Abs (0x004D5); + (0x004D6,0x004D6), `Abs (0x004D7); + (0x004D8,0x004D8), `Abs (0x004D9); + (0x004DA,0x004DA), `Abs (0x004DB); + (0x004DC,0x004DC), `Abs (0x004DD); + (0x004DE,0x004DE), `Abs (0x004DF); + (0x004E0,0x004E0), `Abs (0x004E1); + (0x004E2,0x004E2), `Abs (0x004E3); + (0x004E4,0x004E4), `Abs (0x004E5); + (0x004E6,0x004E6), `Abs (0x004E7); + (0x004E8,0x004E8), `Abs (0x004E9); + (0x004EA,0x004EA), `Abs (0x004EB); + (0x004EC,0x004EC), `Abs (0x004ED); + (0x004EE,0x004EE), `Abs (0x004EF); + (0x004F0,0x004F0), `Abs (0x004F1); + (0x004F2,0x004F2), `Abs (0x004F3); + (0x004F4,0x004F4), `Abs (0x004F5); + (0x004F8,0x004F8), `Abs (0x004F9); + (0x00500,0x00500), `Abs (0x00501); + (0x00502,0x00502), `Abs (0x00503); + (0x00504,0x00504), `Abs (0x00505); + (0x00506,0x00506), `Abs (0x00507); + (0x00508,0x00508), `Abs (0x00509); + (0x0050A,0x0050A), `Abs (0x0050B); + (0x0050C,0x0050C), `Abs (0x0050D); + (0x0050E,0x0050E), `Abs (0x0050F); + (0x00531,0x00556), `Delta (48); + (0x01E00,0x01E00), `Abs (0x01E01); + (0x01E02,0x01E02), `Abs (0x01E03); + (0x01E04,0x01E04), `Abs (0x01E05); + (0x01E06,0x01E06), `Abs (0x01E07); + (0x01E08,0x01E08), `Abs (0x01E09); + (0x01E0A,0x01E0A), `Abs (0x01E0B); + (0x01E0C,0x01E0C), `Abs (0x01E0D); + (0x01E0E,0x01E0E), `Abs (0x01E0F); + (0x01E10,0x01E10), `Abs (0x01E11); + (0x01E12,0x01E12), `Abs (0x01E13); + (0x01E14,0x01E14), `Abs (0x01E15); + (0x01E16,0x01E16), `Abs (0x01E17); + (0x01E18,0x01E18), `Abs (0x01E19); + (0x01E1A,0x01E1A), `Abs (0x01E1B); + (0x01E1C,0x01E1C), `Abs (0x01E1D); + (0x01E1E,0x01E1E), `Abs (0x01E1F); + (0x01E20,0x01E20), `Abs (0x01E21); + (0x01E22,0x01E22), `Abs (0x01E23); + (0x01E24,0x01E24), `Abs (0x01E25); + (0x01E26,0x01E26), `Abs (0x01E27); + (0x01E28,0x01E28), `Abs (0x01E29); + (0x01E2A,0x01E2A), `Abs (0x01E2B); + (0x01E2C,0x01E2C), `Abs (0x01E2D); + (0x01E2E,0x01E2E), `Abs (0x01E2F); + (0x01E30,0x01E30), `Abs (0x01E31); + (0x01E32,0x01E32), `Abs (0x01E33); + (0x01E34,0x01E34), `Abs (0x01E35); + (0x01E36,0x01E36), `Abs (0x01E37); + (0x01E38,0x01E38), `Abs (0x01E39); + (0x01E3A,0x01E3A), `Abs (0x01E3B); + (0x01E3C,0x01E3C), `Abs (0x01E3D); + (0x01E3E,0x01E3E), `Abs (0x01E3F); + (0x01E40,0x01E40), `Abs (0x01E41); + (0x01E42,0x01E42), `Abs (0x01E43); + (0x01E44,0x01E44), `Abs (0x01E45); + (0x01E46,0x01E46), `Abs (0x01E47); + (0x01E48,0x01E48), `Abs (0x01E49); + (0x01E4A,0x01E4A), `Abs (0x01E4B); + (0x01E4C,0x01E4C), `Abs (0x01E4D); + (0x01E4E,0x01E4E), `Abs (0x01E4F); + (0x01E50,0x01E50), `Abs (0x01E51); + (0x01E52,0x01E52), `Abs (0x01E53); + (0x01E54,0x01E54), `Abs (0x01E55); + (0x01E56,0x01E56), `Abs (0x01E57); + (0x01E58,0x01E58), `Abs (0x01E59); + (0x01E5A,0x01E5A), `Abs (0x01E5B); + (0x01E5C,0x01E5C), `Abs (0x01E5D); + (0x01E5E,0x01E5E), `Abs (0x01E5F); + (0x01E60,0x01E60), `Abs (0x01E61); + (0x01E62,0x01E62), `Abs (0x01E63); + (0x01E64,0x01E64), `Abs (0x01E65); + (0x01E66,0x01E66), `Abs (0x01E67); + (0x01E68,0x01E68), `Abs (0x01E69); + (0x01E6A,0x01E6A), `Abs (0x01E6B); + (0x01E6C,0x01E6C), `Abs (0x01E6D); + (0x01E6E,0x01E6E), `Abs (0x01E6F); + (0x01E70,0x01E70), `Abs (0x01E71); + (0x01E72,0x01E72), `Abs (0x01E73); + (0x01E74,0x01E74), `Abs (0x01E75); + (0x01E76,0x01E76), `Abs (0x01E77); + (0x01E78,0x01E78), `Abs (0x01E79); + (0x01E7A,0x01E7A), `Abs (0x01E7B); + (0x01E7C,0x01E7C), `Abs (0x01E7D); + (0x01E7E,0x01E7E), `Abs (0x01E7F); + (0x01E80,0x01E80), `Abs (0x01E81); + (0x01E82,0x01E82), `Abs (0x01E83); + (0x01E84,0x01E84), `Abs (0x01E85); + (0x01E86,0x01E86), `Abs (0x01E87); + (0x01E88,0x01E88), `Abs (0x01E89); + (0x01E8A,0x01E8A), `Abs (0x01E8B); + (0x01E8C,0x01E8C), `Abs (0x01E8D); + (0x01E8E,0x01E8E), `Abs (0x01E8F); + (0x01E90,0x01E90), `Abs (0x01E91); + (0x01E92,0x01E92), `Abs (0x01E93); + (0x01E94,0x01E94), `Abs (0x01E95); + (0x01EA0,0x01EA0), `Abs (0x01EA1); + (0x01EA2,0x01EA2), `Abs (0x01EA3); + (0x01EA4,0x01EA4), `Abs (0x01EA5); + (0x01EA6,0x01EA6), `Abs (0x01EA7); + (0x01EA8,0x01EA8), `Abs (0x01EA9); + (0x01EAA,0x01EAA), `Abs (0x01EAB); + (0x01EAC,0x01EAC), `Abs (0x01EAD); + (0x01EAE,0x01EAE), `Abs (0x01EAF); + (0x01EB0,0x01EB0), `Abs (0x01EB1); + (0x01EB2,0x01EB2), `Abs (0x01EB3); + (0x01EB4,0x01EB4), `Abs (0x01EB5); + (0x01EB6,0x01EB6), `Abs (0x01EB7); + (0x01EB8,0x01EB8), `Abs (0x01EB9); + (0x01EBA,0x01EBA), `Abs (0x01EBB); + (0x01EBC,0x01EBC), `Abs (0x01EBD); + (0x01EBE,0x01EBE), `Abs (0x01EBF); + (0x01EC0,0x01EC0), `Abs (0x01EC1); + (0x01EC2,0x01EC2), `Abs (0x01EC3); + (0x01EC4,0x01EC4), `Abs (0x01EC5); + (0x01EC6,0x01EC6), `Abs (0x01EC7); + (0x01EC8,0x01EC8), `Abs (0x01EC9); + (0x01ECA,0x01ECA), `Abs (0x01ECB); + (0x01ECC,0x01ECC), `Abs (0x01ECD); + (0x01ECE,0x01ECE), `Abs (0x01ECF); + (0x01ED0,0x01ED0), `Abs (0x01ED1); + (0x01ED2,0x01ED2), `Abs (0x01ED3); + (0x01ED4,0x01ED4), `Abs (0x01ED5); + (0x01ED6,0x01ED6), `Abs (0x01ED7); + (0x01ED8,0x01ED8), `Abs (0x01ED9); + (0x01EDA,0x01EDA), `Abs (0x01EDB); + (0x01EDC,0x01EDC), `Abs (0x01EDD); + (0x01EDE,0x01EDE), `Abs (0x01EDF); + (0x01EE0,0x01EE0), `Abs (0x01EE1); + (0x01EE2,0x01EE2), `Abs (0x01EE3); + (0x01EE4,0x01EE4), `Abs (0x01EE5); + (0x01EE6,0x01EE6), `Abs (0x01EE7); + (0x01EE8,0x01EE8), `Abs (0x01EE9); + (0x01EEA,0x01EEA), `Abs (0x01EEB); + (0x01EEC,0x01EEC), `Abs (0x01EED); + (0x01EEE,0x01EEE), `Abs (0x01EEF); + (0x01EF0,0x01EF0), `Abs (0x01EF1); + (0x01EF2,0x01EF2), `Abs (0x01EF3); + (0x01EF4,0x01EF4), `Abs (0x01EF5); + (0x01EF6,0x01EF6), `Abs (0x01EF7); + (0x01EF8,0x01EF8), `Abs (0x01EF9); + (0x01F08,0x01F0F), `Delta (-8); + (0x01F18,0x01F1D), `Delta (-8); + (0x01F28,0x01F2F), `Delta (-8); + (0x01F38,0x01F3F), `Delta (-8); + (0x01F48,0x01F4D), `Delta (-8); + (0x01F59,0x01F59), `Abs (0x01F51); + (0x01F5B,0x01F5B), `Abs (0x01F53); + (0x01F5D,0x01F5D), `Abs (0x01F55); + (0x01F5F,0x01F5F), `Abs (0x01F57); + (0x01F68,0x01F6F), `Delta (-8); + (0x01FB8,0x01FB9), `Delta (-8); + (0x01FBA,0x01FBB), `Delta (-74); + (0x01FC8,0x01FCB), `Delta (-86); + (0x01FD8,0x01FD9), `Delta (-8); + (0x01FDA,0x01FDB), `Delta (-100); + (0x01FE8,0x01FE9), `Delta (-8); + (0x01FEA,0x01FEB), `Delta (-112); + (0x01FEC,0x01FEC), `Abs (0x01FE5); + (0x01FF8,0x01FF9), `Delta (-128); + (0x01FFA,0x01FFB), `Delta (-126); + (0x02126,0x02126), `Abs (0x003C9); + (0x0212A,0x0212A), `Abs (0x0006B); + (0x0212B,0x0212B), `Abs (0x000E5); + (0x0FF21,0x0FF3A), `Delta (32); + (0x10400,0x10425), `Delta (40); + (0x001C5,0x001C5), `Abs (0x001C6); + (0x001C8,0x001C8), `Abs (0x001C9); + (0x001CB,0x001CB), `Abs (0x001CC); + (0x001F2,0x001F2), `Abs (0x001F3); + (0x01F88,0x01F8F), `Delta (-8); + (0x01F98,0x01F9F), `Delta (-8); + (0x01FA8,0x01FAF), `Delta (-8); + (0x01FBC,0x01FBC), `Abs (0x01FB3); + (0x01FCC,0x01FCC), `Abs (0x01FC3); + (0x01FFC,0x01FFC), `Abs (0x01FF3); + (0x02160,0x0216F), `Delta (16) +] + diff --git a/lib/util.ml b/lib/util.ml index 0d6e7ff2..6d04c3c2 100644 --- a/lib/util.ml +++ b/lib/util.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* $Id: util.ml 13200 2010-06-25 22:36:25Z letouzey $ *) +(* $Id$ *) open Pp @@ -20,8 +20,15 @@ exception UserError of string * std_ppcmds (* User errors *) let error string = raise (UserError(string, str string)) let errorlabstrm l pps = raise (UserError(l,pps)) +exception AnomalyOnError of string * exn + +exception AlreadyDeclared of std_ppcmds (* for already declared Schemes *) +let alreadydeclared pps = raise (AlreadyDeclared(pps)) + let todo s = prerr_string ("TODO: "^s^"\n") +exception Timeout + type loc = Compat.loc let dummy_loc = Compat.dummy_loc let unloc = Compat.unloc @@ -34,7 +41,7 @@ let anomaly_loc (loc,s,strm) = Stdpp.raise_with_loc loc (Anomaly (s,strm)) let user_err_loc (loc,s,strm) = Stdpp.raise_with_loc loc (UserError (s,strm)) let invalid_arg_loc (loc,s) = Stdpp.raise_with_loc loc (Invalid_argument s) -let located_fold_left f x (_,a) = f x a +let located_fold_left f x (_,a) = f x a let located_iter2 f (_,a) (_,b) = f a b (* Like Exc_located, but specifies the outermost file read, the filename @@ -47,6 +54,12 @@ exception Error_in_file of string * (bool * string * loc) * exn let on_fst f (a,b) = (f a,b) let on_snd f (a,b) = (a,f b) +(* Mapping under pairs *) + +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 @@ -65,13 +78,13 @@ let is_blank = function (* Strings *) -let explode s = +let explode s = let rec explode_rec n = if n >= String.length s then [] - else + else String.make 1 (String.get s n) :: explode_rec (succ n) - in + in explode_rec 0 let implode sl = String.concat "" sl @@ -91,16 +104,20 @@ let strip s = let a = lstrip_rec 0 and b = rstrip_rec (n-1) in String.sub s a (b-a+1) +let drop_simple_quotes s = + let n = String.length s in + if n > 2 & s.[0] = '\'' & s.[n-1] = '\'' then String.sub s 1 (n-2) else s + (* substring searching... *) (* gdzie = where, co = what *) (* gdzie=gdzie(string) gl=gdzie(length) gi=gdzie(index) *) -let rec is_sub gdzie gl gi co cl ci = +let rec is_sub gdzie gl gi co cl ci = (ci>=cl) || - ((String.unsafe_get gdzie gi = String.unsafe_get co ci) && + ((String.unsafe_get gdzie gi = String.unsafe_get co ci) && (is_sub gdzie gl (gi+1) co cl (ci+1))) -let rec raw_str_index i gdzie l c co cl = +let rec raw_str_index i gdzie l c co cl = (* First adapt to ocaml 3.11 new semantics of index_from *) if (i+cl > l) then raise Not_found; (* Then proceed as in ocaml < 3.11 *) @@ -108,7 +125,7 @@ let rec raw_str_index i gdzie l c co cl = if (i'+cl <= l) && (is_sub gdzie l i' co cl 0) then i' else raw_str_index (i'+1) gdzie l c co cl -let string_index_from gdzie i co = +let string_index_from gdzie i co = if co="" then i else raw_str_index i gdzie (String.length gdzie) (String.unsafe_get co 0) co (String.length co) @@ -130,7 +147,7 @@ let ordinal n = let split_string_at c s = let len = String.length s in let rec split n = - try + try let pos = String.index_from s n c in let dir = String.sub s n (pos-n) in dir :: split (succ pos) @@ -153,138 +170,105 @@ type utf8_status = UnicodeLetter | UnicodeIdentPart | UnicodeSymbol exception UnsupportedUtf8 -let classify_unicode unicode = - match unicode land 0x1F000 with - | 0x0 -> - begin match unicode with - (* utf-8 Basic Latin underscore *) - | x when x = 0x005F -> UnicodeLetter - (* utf-8 Basic Latin letters *) - | x when 0x0041 <= x & x <= 0x005A -> UnicodeLetter - | x when 0x0061 <= x & x <= 0x007A -> UnicodeLetter - (* utf-8 Basic Latin digits and quote *) - | x when 0x0030 <= x & x <= 0x0039 or x = 0x0027 -> UnicodeIdentPart - (* utf-8 Basic Latin symbols *) - | x when x <= 0x007F -> UnicodeSymbol - (* utf-8 Latin-1 non breaking space U00A0 *) - | 0x00A0 -> UnicodeLetter - (* utf-8 Latin-1 symbols U00A1-00BF *) - | x when 0x00A0 <= x & x <= 0x00BF -> UnicodeSymbol - (* utf-8 Latin-1 letters U00C0-00D6 *) - | x when 0x00C0 <= x & x <= 0x00D6 -> UnicodeLetter - (* utf-8 Latin-1 symbol U00D7 *) - | 0x00D7 -> UnicodeSymbol - (* utf-8 Latin-1 letters U00D8-00F6 *) - | x when 0x00D8 <= x & x <= 0x00F6 -> UnicodeLetter - (* utf-8 Latin-1 symbol U00F7 *) - | 0x00F7 -> UnicodeSymbol - (* utf-8 Latin-1 letters U00F8-00FF *) - | x when 0x00F8 <= x & x <= 0x00FF -> UnicodeLetter - (* utf-8 Latin Extended A U0100-017F and Latin Extended B U0180-U0241 *) - | x when 0x0100 <= x & x <= 0x0241 -> UnicodeLetter - (* utf-8 Phonetic letters U0250-02AF *) - | x when 0x0250 <= x & x <= 0x02AF -> UnicodeLetter - (* utf-8 what do to with diacritics U0300-U036F ? *) - (* utf-8 Greek letters U0380-03FF *) - | x when 0x0380 <= x & x <= 0x03FF -> UnicodeLetter - (* utf-8 Cyrillic letters U0400-0481 *) - | x when 0x0400 <= x & x <= 0x0481 -> UnicodeLetter - (* utf-8 Cyrillic symbol U0482 *) - | 0x0482 -> UnicodeSymbol - (* utf-8 what do to with diacritics U0483-U0489 \ U0487 ? *) - (* utf-8 Cyrillic letters U048A-U4F9 (Warning: 04CF) *) - | x when 0x048A <= x & x <= 0x04F9 -> UnicodeLetter - (* utf-8 Cyrillic supplement letters U0500-U050F *) - | x when 0x0500 <= x & x <= 0x050F -> UnicodeLetter - (* utf-8 Hebrew letters U05D0-05EA *) - | x when 0x05D0 <= x & x <= 0x05EA -> UnicodeLetter - (* utf-8 Arabic letters U0621-064A *) - | x when 0x0621 <= x & x <= 0x064A -> UnicodeLetter - (* utf-8 Arabic supplement letters U0750-076D *) - | x when 0x0750 <= x & x <= 0x076D -> UnicodeLetter - | _ -> raise UnsupportedUtf8 - end - | 0x1000 -> - begin match unicode with - (* utf-8 Georgian U10A0-10FF (has holes) *) - | x when 0x10A0 <= x & x <= 0x10FF -> UnicodeLetter - (* utf-8 Hangul Jamo U1100-11FF (has holes) *) - | x when 0x1100 <= x & x <= 0x11FF -> UnicodeLetter - (* utf-8 Latin additional letters U1E00-1E9B and U1EA0-1EF9 *) - | x when 0x1E00 <= x & x <= 0x1E9B -> UnicodeLetter - | x when 0x1EA0 <= x & x <= 0x1EF9 -> UnicodeLetter - | _ -> raise UnsupportedUtf8 - end - | 0x2000 -> - begin match unicode with - (* utf-8 general punctuation U2080-2089 *) - (* Hyphens *) - | x when 0x2010 <= x & x <= 0x2011 -> UnicodeLetter - (* Dashes and other symbols *) - | x when 0x2012 <= x & x <= 0x2027 -> UnicodeSymbol - (* Per mille and per ten thousand signs *) - | x when 0x2030 <= x & x <= 0x2031 -> UnicodeSymbol - (* Prime letters *) - | x when 0x2032 <= x & x <= 0x2034 or x = 0x2057 -> UnicodeIdentPart - (* Miscellaneous punctuation *) - | x when 0x2039 <= x & x <= 0x2056 -> UnicodeSymbol - | x when 0x2058 <= x & x <= 0x205E -> UnicodeSymbol - (* Invisible mathematical operators *) - | x when 0x2061 <= x & x <= 0x2063 -> UnicodeSymbol - (* utf-8 superscript U2070-207C *) - | x when 0x2070 <= x & x <= 0x207C -> UnicodeSymbol - (* utf-8 subscript U2080-2089 *) - | x when 0x2080 <= x & x <= 0x2089 -> UnicodeIdentPart - (* utf-8 letter-like U2100-214F *) - | x when 0x2100 <= x & x <= 0x214F -> UnicodeLetter - (* utf-8 number-forms U2153-2183 *) - | x when 0x2153 <= x & x <= 0x2183 -> UnicodeSymbol - (* utf-8 arrows A U2190-21FF *) - (* utf-8 mathematical operators U2200-22FF *) - (* utf-8 miscellaneous technical U2300-23FF *) - | x when 0x2190 <= x & x <= 0x23FF -> UnicodeSymbol - (* utf-8 box drawing U2500-257F has ceiling, etc. *) - (* utf-8 block elements U2580-259F *) - (* utf-8 geom. shapes U25A0-25FF (has triangles, losange, etc) *) - (* utf-8 miscellaneous symbols U2600-26FF *) - | x when 0x2500 <= x & x <= 0x26FF -> UnicodeSymbol - (* utf-8 arrows B U2900-297F *) - | x when 0x2900 <= x & x <= 0x297F -> UnicodeSymbol - (* utf-8 mathematical operators U2A00-2AFF *) - | x when 0x2A00 <= x & x <= 0x2AFF -> UnicodeSymbol - (* utf-8 bold symbols U2768-U2775 *) - | x when 0x2768 <= x & x <= 0x2775 -> UnicodeSymbol - (* utf-8 arrows and brackets U27E0-U27FF *) - | x when 0x27E0 <= x & x <= 0x27FF -> UnicodeSymbol - (* utf-8 brackets, braces and parentheses *) - | x when 0x2980 <= x & x <= 0x29FF -> UnicodeSymbol - (* utf-8 miscellaneous including double-plus U29F0-U29FF *) - | x when 0x29F0 <= x & x <= 0x29FF -> UnicodeSymbol - | _ -> raise UnsupportedUtf8 - end - | _ -> - begin match unicode with - (* utf-8 CJC Symbols and Punctuation *) - | x when 0x3008 <= x & x <= 0x3020 -> UnicodeSymbol - (* utf-8 Hiragana U3040-309F and Katakana U30A0-30FF *) - | x when 0x3040 <= x & x <= 0x30FF -> UnicodeLetter - (* utf-8 Unified CJK Ideographs U4E00-9FA5 *) - | x when 0x4E00 <= x & x <= 0x9FA5 -> UnicodeLetter - (* utf-8 Hangul syllables UAC00-D7AF *) - | x when 0xAC00 <= x & x <= 0xD7AF -> UnicodeLetter - (* utf-8 Gothic U10330-1034A *) - | x when 0x10330 <= x & x <= 0x1034A -> UnicodeLetter - (* utf-8 Math Alphanumeric Symbols U1D400-1D7FF (letters) (has holes) *) - | x when 0x1D400 <= x & x <= 0x1D7CB -> UnicodeLetter - (* utf-8 Math Alphanumeric Symbols U1D400-1D7FF (digits) *) - | x when 0x1D7CE <= x & x <= 0x1D7FF -> UnicodeIdentPart - | _ -> raise UnsupportedUtf8 - end +(* The following table stores classes of Unicode characters that + are used by the lexer. There are 3 different classes so 2 bits are + allocated for each character. We only use 16 bits over the 31 bits + to simplify the masking process. (This choice seems to be a good + trade-off between speed and space after some benchmarks.) *) + +(* A 256ko table, initially filled with zeros. *) +let table = Array.create (1 lsl 17) 0 + +(* Associate a 2-bit pattern to each status at position [i]. + Only the 3 lowest bits of [i] are taken into account to + define the position of the pattern in the word. + Notice that pattern "00" means "undefined". *) +let mask i = function + | UnicodeLetter -> 1 lsl ((i land 7) lsl 1) (* 01 *) + | UnicodeIdentPart -> 2 lsl ((i land 7) lsl 1) (* 10 *) + | UnicodeSymbol -> 3 lsl ((i land 7) lsl 1) (* 11 *) + +(* Helper to reset 2 bits in a word. *) +let reset_mask i = + lnot (3 lsl ((i land 7) lsl 1)) + +(* Initialize the lookup table from a list of segments, assigning + a status to every character of each segment. The order of these + assignments is relevant: it is possible to assign status [s] to + a segment [(c1, c2)] and later assign [s'] to [c] even if [c] is + between [c1] and [c2]. *) +let mk_lookup_table_from_unicode_tables_for status tables = + List.iter + (List.iter + (fun (c1, c2) -> + for i = c1 to c2 do + table.(i lsr 3) <- + (table.(i lsr 3) land (reset_mask i)) lor (mask i status) + done)) + tables + +(* Look up into the table and interpret the found pattern. *) +let lookup x = + let v = (table.(x lsr 3) lsr ((x land 7) lsl 1)) land 3 in + if v = 1 then UnicodeLetter + else if v = 2 then UnicodeIdentPart + else if v = 3 then UnicodeSymbol + else raise UnsupportedUtf8 + +(* [classify_unicode] discriminates between 3 different kinds of + symbols based on the standard unicode classification (extracted from + Camomile). *) +let classify_unicode = + let single c = [ (c, c) ] in + (* General tables. *) + mk_lookup_table_from_unicode_tables_for UnicodeSymbol + [ + Unicodetable.sm; (* Symbol, maths. *) + Unicodetable.sc; (* Symbol, currency. *) + Unicodetable.so; (* Symbol, modifier. *) + Unicodetable.pd; (* Punctation, dash. *) + Unicodetable.pc; (* Punctation, connector. *) + Unicodetable.pe; (* Punctation, open. *) + Unicodetable.ps; (* Punctation, close. *) + Unicodetable.pi; (* Punctation, initial quote. *) + Unicodetable.pf; (* Punctation, final quote. *) + Unicodetable.po; (* Punctation, other. *) + ]; + mk_lookup_table_from_unicode_tables_for UnicodeLetter + [ + Unicodetable.lu; (* Letter, uppercase. *) + Unicodetable.ll; (* Letter, lowercase. *) + Unicodetable.lt; (* Letter, titlecase. *) + Unicodetable.lo; (* Letter, others. *) + ]; + mk_lookup_table_from_unicode_tables_for UnicodeIdentPart + [ + Unicodetable.nd; (* Number, decimal digits. *) + Unicodetable.nl; (* Number, letter. *) + Unicodetable.no; (* Number, other. *) + ]; + (* Exceptions (from a previous version of this function). *) + mk_lookup_table_from_unicode_tables_for UnicodeSymbol + [ + single 0x000B2; (* Squared. *) + single 0x0002E; (* Dot. *) + ]; + mk_lookup_table_from_unicode_tables_for UnicodeLetter + [ + single 0x005F; (* Underscore. *) + single 0x00A0; (* Non breaking space. *) + ]; + mk_lookup_table_from_unicode_tables_for UnicodeIdentPart + [ + single 0x0027; (* Special space. *) + ]; + (* Lookup *) + lookup exception End_of_input let utf8_of_unicode n = - if n < 128 then + if n < 128 then String.make 1 (Char.chr n) else if n < 2048 then let s = String.make 2 (Char.chr (128 + n mod 64)) in @@ -294,18 +278,18 @@ let utf8_of_unicode n = end else if n < 65536 then let s = String.make 3 (Char.chr (128 + n mod 64)) in - begin + begin s.[1] <- Char.chr (128 + (n / 64) mod 64); - s.[0] <- Char.chr (224 + n / 4096); + s.[0] <- Char.chr (224 + n / 4096); s end else let s = String.make 4 (Char.chr (128 + n mod 64)) in - begin + begin s.[2] <- Char.chr (128 + (n / 64) mod 64); s.[1] <- Char.chr (128 + (n / 4096) mod 64); s.[0] <- Char.chr (240 + n / 262144); - s + s end let next_utf8 s i = @@ -358,7 +342,7 @@ let check_ident_gen handle s = i := !i + j done with End_of_input -> () - with + with | End_of_input -> error "The empty string is not an identifier." | UnsupportedUtf8 -> error (s^": unsupported character in utf8 sequence.") | Invalid_argument _ -> error (s^": invalid utf8 sequence.") @@ -366,127 +350,21 @@ let check_ident_gen handle s = let check_ident_soft = check_ident_gen warning let check_ident = check_ident_gen error -let lowercase_unicode s unicode = - match unicode land 0x1F000 with - | 0x0 -> - begin match unicode with - (* utf-8 Basic Latin underscore *) - | x when x = 0x005F -> x - (* utf-8 Basic Latin letters *) - | x when 0x0041 <= x & x <= 0x005A -> x + 32 - | x when 0x0061 <= x & x <= 0x007A -> x - (* utf-8 Latin-1 non breaking space U00A0 *) - | 0x00A0 as x -> x - (* utf-8 Latin-1 letters U00C0-00D6 *) - | x when 0x00C0 <= x & x <= 0x00D6 -> x + 32 - (* utf-8 Latin-1 letters U00D8-00F6 *) - | x when 0x00D8 <= x & x <= 0x00DE -> x + 32 - | x when 0x00E0 <= x & x <= 0x00F6 -> x - (* utf-8 Latin-1 letters U00F8-00FF *) - | x when 0x00F8 <= x & x <= 0x00FF -> x - (* utf-8 Latin Extended A U0100-017F and Latin Extended B U0180-U0241 *) - | x when 0x0100 <= x & x <= 0x017F -> - if x mod 2 = 1 then x else x + 1 - | x when 0x0180 <= x & x <= 0x0241 -> - warning ("Unable to decide which lowercase letter to map to "^s); x - (* utf-8 Phonetic letters U0250-02AF *) - | x when 0x0250 <= x & x <= 0x02AF -> x - (* utf-8 what do to with diacritics U0300-U036F ? *) - (* utf-8 Greek letters U0380-03FF *) - | x when 0x0380 <= x & x <= 0x0385 -> x - | 0x0386 -> 0x03AC - | x when 0x0388 <= x & x <= 0x038A -> x + 37 - | 0x038C -> 0x03CC - | x when 0x038E <= x & x <= 0x038F -> x + 63 - | x when 0x0390 <= x & x <= 0x03AB & x <> 0x03A2 -> x + 32 - (* utf-8 Greek lowercase letters U03B0-03CE *) - | x when 0x03AC <= x & x <= 0x03CE -> x - | x when 0x03CF <= x & x <= 0x03FF -> - warning ("Unable to decide which lowercase letter to map to "^s); x - (* utf-8 Cyrillic letters U0400-0481 *) - | x when 0x0400 <= x & x <= 0x040F -> x + 80 - | x when 0x0410 <= x & x <= 0x042F -> x + 32 - | x when 0x0430 <= x & x <= 0x045F -> x - | x when 0x0460 <= x & x <= 0x0481 -> - if x mod 2 = 1 then x else x + 1 - (* utf-8 Cyrillic letters U048A-U4F9 (Warning: 04CF) *) - | x when 0x048A <= x & x <= 0x04F9 & x <> 0x04CF -> - if x mod 2 = 1 then x else x + 1 - (* utf-8 Cyrillic supplement letters U0500-U050F *) - | x when 0x0500 <= x & x <= 0x050F -> - if x mod 2 = 1 then x else x + 1 - (* utf-8 Hebrew letters U05D0-05EA *) - | x when 0x05D0 <= x & x <= 0x05EA -> x - (* utf-8 Arabic letters U0621-064A *) - | x when 0x0621 <= x & x <= 0x064A -> x - (* utf-8 Arabic supplement letters U0750-076D *) - | x when 0x0750 <= x & x <= 0x076D -> x - | _ -> raise UnsupportedUtf8 - end - | 0x1000 -> - begin match unicode with - (* utf-8 Georgian U10A0-10FF (has holes) *) - | x when 0x10A0 <= x & x <= 0x10FF -> x - (* utf-8 Hangul Jamo U1100-11FF (has holes) *) - | x when 0x1100 <= x & x <= 0x11FF -> x - (* utf-8 Latin additional letters U1E00-1E9B and U1EA0-1EF9 *) - | x when 0x1E00 <= x & x <= 0x1E95 -> - if x mod 2 = 1 then x else x + 1 - | x when 0x1E96 <= x & x <= 0x1E9B -> x - | x when 0x1EA0 <= x & x <= 0x1EF9 -> - if x mod 2 = 1 then x else x + 1 - | _ -> raise UnsupportedUtf8 - end - | 0x2000 -> - begin match unicode with - (* utf-8 general punctuation U2080-2089 *) - (* Hyphens *) - | x when 0x2010 <= x & x <= 0x2011 -> x - (* utf-8 letter-like U2100-214F *) - | 0x2102 (* double-struck C *) -> Char.code 'x' - | 0x2115 (* double-struck N *) -> Char.code 'n' - | 0x2119 (* double-struck P *) -> Char.code 'x' - | 0x211A (* double-struck Q *) -> Char.code 'x' - | 0x211D (* double-struck R *) -> Char.code 'r' - | 0x2124 (* double-struck Z *) -> Char.code 'x' - | x when 0x2100 <= x & x <= 0x214F -> - warning ("Unable to decide which lowercase letter to map to "^s); x - | _ -> raise UnsupportedUtf8 - end - | _ -> - begin match unicode with - (* utf-8 Hiragana U3040-309F and Katakana U30A0-30FF *) - | x when 0x3040 <= x & x <= 0x30FF -> x - (* utf-8 Unified CJK Ideographs U4E00-9FA5 *) - | x when 0x4E00 <= x & x <= 0x9FA5 -> x - (* utf-8 Hangul syllables UAC00-D7AF *) - | x when 0xAC00 <= x & x <= 0xD7AF -> x - (* utf-8 Gothic U10330-1034A *) - | x when 0x10330 <= x & x <= 0x1034A -> x - (* utf-8 Math Alphanumeric Symbols U1D400-1D7FF (letters) (has holes) *) - | x when 0x1D6A8 <= x & x <= 0x1D7C9 -> - let a = (x - 0x1D6A8) mod 58 in - if a <= 16 or (18 <= a & a <= 24) - then x + 26 (* all but nabla and theta symbol *) - else x - | x when 0x1D538 <= x & x <= 0x1D56B -> - (* Use ordinary lowercase in both small and capital double-struck *) - (x - 0x1D538) mod 26 + Char.code 'a' - | x when 0x1D468 <= x & x <= 0x1D6A3 -> (* General case *) - if (x - 0x1D400 / 26) mod 2 = 0 then x + 26 else x - | x when 0x1D400 <= x & x <= 0x1D7CB -> (* fallback *) - x - (* utf-8 Math Alphanumeric Symbols U1D400-1D7FF (digits) *) - | x when 0x1D7CE <= x & x <= 0x1D7FF -> x - | _ -> raise UnsupportedUtf8 - end +let lowercase_unicode = + let tree = Segmenttree.make Unicodetable.to_lower in + fun unicode -> + try + match Segmenttree.lookup unicode tree with + | `Abs c -> c + | `Delta d -> unicode + d + with Not_found -> unicode let lowercase_first_char_utf8 s = assert (s <> ""); let j, n = next_utf8 s 0 in - utf8_of_unicode (lowercase_unicode (String.sub s 0 j) n) + utf8_of_unicode (lowercase_unicode n) -(* For extraction, we need to encode unicode character into ascii ones *) +(** For extraction, we need to encode unicode character into ascii ones *) let ascii_of_ident s = let check_ascii s = @@ -499,50 +377,60 @@ let ascii_of_ident s = begin try while true do let j, n = next_utf8 s !i in out := - if n >= 128 - then Printf.sprintf "%s__U%04x_" !out n - else Printf.sprintf "%s%c" !out s.[!i]; + if n >= 128 + then Printf.sprintf "%s__U%04x_" !out n + else Printf.sprintf "%s%c" !out s.[!i]; i := !i + j done with End_of_input -> () end; !out (* Lists *) -let list_intersect l1 l2 = +let rec list_compare cmp l1 l2 = + match l1,l2 with + [], [] -> 0 + | _::_, [] -> 1 + | [], _::_ -> -1 + | x1::l1, x2::l2 -> + (match cmp x1 x2 with + | 0 -> list_compare cmp l1 l2 + | c -> c) + +let list_intersect l1 l2 = List.filter (fun x -> List.mem x l2) l1 -let list_union l1 l2 = +let list_union l1 l2 = let rec urec = function | [] -> l2 | a::l -> if List.mem a l2 then urec l else a::urec l - in + in urec l1 -let list_unionq l1 l2 = +let list_unionq l1 l2 = let rec urec = function | [] -> l2 | a::l -> if List.memq a l2 then urec l else a::urec l - in + in urec l1 let list_subtract l1 l2 = if l2 = [] then l1 else List.filter (fun x -> not (List.mem x l2)) l1 -let list_subtractq l1 l2 = +let list_subtractq l1 l2 = if l2 = [] then l1 else List.filter (fun x -> not (List.memq x l2)) l1 -let list_chop n l = +let list_chop n l = let rec chop_aux acc = function | (0, l2) -> (List.rev acc, l2) | (n, (h::t)) -> chop_aux (h::acc) (pred n, t) | (_, []) -> failwith "list_chop" - in + in chop_aux [] (n,l) -let list_tabulate f len = +let list_tabulate f len = let rec tabrec n = if n = len then [] else (f n)::(tabrec (n+1)) - in + in tabrec 0 let rec list_make n v = @@ -550,41 +438,41 @@ let rec list_make n v = else if n < 0 then invalid_arg "list_make" else v::list_make (n-1) v -let list_assign l n e = +let list_assign l n e = let rec assrec stk = function | ((h::t), 0) -> List.rev_append stk (e::t) | ((h::t), n) -> assrec (h::stk) (t, n-1) | ([], _) -> failwith "list_assign" - in + in assrec [] (l,n) let rec list_smartmap f l = match l with [] -> l - | h::tl -> + | h::tl -> let h' = f h and tl' = list_smartmap f tl in if h'==h && tl'==tl then l else h'::tl' let list_map_left f = (* ensures the order in case of side-effects *) let rec map_rec = function - | [] -> [] + | [] -> [] | x::l -> let v = f x in v :: map_rec l - in + in map_rec -let list_map_i f = +let list_map_i f = let rec map_i_rec i = function - | [] -> [] + | [] -> [] | x::l -> let v = f i x in v :: map_i_rec (i+1) l - in + in map_i_rec -let list_map2_i f i l1 l2 = +let list_map2_i f i l1 l2 = let rec map_i i = function | ([], []) -> [] | ((h1::t1), (h2::t2)) -> let v = f i h1 h2 in v :: map_i (succ i) (t1,t2) | (_, _) -> invalid_arg "map2_i" - in + in map_i i (l1,l2) let list_map3 f l1 l2 l3 = @@ -592,7 +480,7 @@ let list_map3 f l1 l2 l3 = | ([], [], []) -> [] | ((h1::t1), (h2::t2), (h3::t3)) -> let v = f h1 h2 h3 in v::map (t1,t2,t3) | (_, _, _) -> invalid_arg "map3" - in + in map (l1,l2,l3) let list_map4 f l1 l2 l3 l4 = @@ -600,41 +488,41 @@ let list_map4 f l1 l2 l3 l4 = | ([], [], [], []) -> [] | ((h1::t1), (h2::t2), (h3::t3), (h4::t4)) -> let v = f h1 h2 h3 h4 in v::map (t1,t2,t3,t4) | (_, _, _, _) -> invalid_arg "map4" - in + in map (l1,l2,l3,l4) -let list_index x = +let list_index x = let rec index_x n = function | y::l -> if x = y then n else index_x (succ n) l | [] -> raise Not_found - in + in index_x 1 -let list_index0 x l = list_index x l - 1 +let list_index0 x l = list_index x l - 1 -let list_unique_index x = +let list_unique_index x = let rec index_x n = function - | y::l -> - if x = y then + | y::l -> + if x = y then if List.mem x l then raise Not_found - else n + else n else index_x (succ n) l - | [] -> raise Not_found + | [] -> raise Not_found in index_x 1 let list_fold_right_i f i l = let rec it_list_f i l a = match l with | [] -> a | b::l -> f (i-1) b (it_list_f (i-1) l a) - in + in it_list_f (List.length l + i) l -let list_fold_left_i f = +let list_fold_left_i f = let rec it_list_f i a = function - | [] -> a + | [] -> a | b::l -> it_list_f (i+1) (f i a b) l - in - it_list_f + in + it_list_f let rec list_fold_left3 f accu l1 l2 l3 = match (l1, l2, l3) with @@ -665,16 +553,16 @@ let list_iter3 f l1 l2 l3 = | ([], [], []) -> () | ((h1::t1), (h2::t2), (h3::t3)) -> f h1 h2 h3; iter (t1,t2,t3) | (_, _, _) -> invalid_arg "map3" - in + in iter (l1,l2,l3) let list_iter_i f l = list_fold_left_i (fun i _ x -> f i x) 0 () l -let list_for_all_i p = +let list_for_all_i p = let rec for_all_p i = function - | [] -> true + | [] -> true | a::l -> p i a && for_all_p (i+1) l - in + in for_all_p let list_except x l = List.filter (fun y -> not (x = y)) l @@ -698,32 +586,33 @@ let list_eq_set l1 l2 = | a::l2 -> aux (list_remove_first a l1) l2 in try aux l1 l2 with Not_found -> false -let list_for_all2eq f l1 l2 = try List.for_all2 f l1 l2 with Failure _ -> false +let list_for_all2eq f l1 l2 = + try List.for_all2 f l1 l2 with Invalid_argument _ -> false -let list_map_i f = - let rec map_i_rec i = function - | [] -> [] - | x::l -> let v = f i x in v::map_i_rec (i+1) l - in - map_i_rec +let list_filter_i p = + let rec filter_i_rec i = function + | [] -> [] + | x::l -> let l' = filter_i_rec (succ i) l in if p i x then x::l' else l' + in + filter_i_rec 0 let rec list_sep_last = function | [] -> failwith "sep_last" | hd::[] -> (hd,[]) | hd::tl -> let (l,tl) = list_sep_last tl in (l,hd::tl) -let list_try_find_i f = +let list_try_find_i f = let rec try_find_f n = function | [] -> failwith "try_find_i" | h::t -> try f n h with Failure _ -> try_find_f (n+1) t - in + in try_find_f -let list_try_find f = +let list_try_find f = let rec try_find_f = function | [] -> failwith "try_find" | h::t -> try f h with Failure _ -> try_find_f t - in + in try_find_f let list_uniquize l = @@ -737,12 +626,12 @@ let list_uniquize l = | [] -> List.rev acc in aux [] l -let rec list_distinct l = +let rec list_distinct l = let visited = Hashtbl.create 23 in let rec loop = function | h::t -> if Hashtbl.mem visited h then false - else + else begin Hashtbl.add visited h h; loop t @@ -755,10 +644,10 @@ let rec list_merge_uniq cmp l1 l2 = | [], l2 -> l2 | l1, [] -> l1 | h1 :: t1, h2 :: t2 -> - let c = cmp h1 h2 in - if c = 0 + let c = cmp h1 h2 in + if c = 0 then h1 :: list_merge_uniq cmp t1 t2 - else if c <= 0 + else if c <= 0 then h1 :: list_merge_uniq cmp t1 l2 else h2 :: list_merge_uniq cmp l1 t2 @@ -787,24 +676,29 @@ let list_subset l1 l2 = let rec look = function | [] -> true | x::ll -> try Hashtbl.find t2 x; look ll with Not_found -> false - in + in look l1 -let list_split_at p = - let rec split_at_loop x y = - match y with - | [] -> ([],[]) - | (a::l) -> if (p a) then (List.rev x,y) else split_at_loop (a::x) l - in - split_at_loop [] - -let list_split_by p = - let rec split_loop = function - | [] -> ([],[]) - | (a::l) -> - let (l1,l2) = split_loop l in if (p a) then (a::l1,l2) else (l1,a::l2) - in - split_loop +(* [list_split_at i l] splits [l] into two lists [(l1,l2)] such that [l1++l2=l] + and [l1] has length [i]. + It raises [Failure] when [i] is negative or greater than the length of [l] *) +let list_split_at index l = + let rec aux i acc = function + tl when i = index -> (List.rev acc), tl + | hd :: tl -> aux (succ i) (hd :: acc) tl + | [] -> failwith "list_split_at: Invalid argument" + in aux 0 [] l + +(* [list_split_when p l] splits [l] into two lists [(l1,a::l2)] such that + [l1++(a::l2)=l], [p a=true] and [p b = false] for every element [b] of [l1]. + If there is no such [a], then it returns [(l,[])] instead *) +let list_split_when p = + let rec split_when_loop x y = + match y with + | [] -> (List.rev x,[]) + | (a::l) -> if (p a) then (List.rev x,y) else split_when_loop (a::x) l + in + split_when_loop [] let rec list_split3 = function | [] -> ([], [], []) @@ -824,7 +718,7 @@ let list_firstn n l = | (0, l) -> List.rev acc | (n, (h::t)) -> aux (h::acc) (pred n, t) | _ -> failwith "firstn" - in + in aux [] (n,l) let rec list_last = function @@ -839,20 +733,23 @@ let list_lastn n l = in if len < n then failwith "lastn" else aux len l -let rec list_skipn n l = match n,l with - | 0, _ -> l - | _, [] -> failwith "list_fromn" +let rec list_skipn n l = match n,l with + | 0, _ -> l + | _, [] -> failwith "list_skipn" | n, _::l -> list_skipn (pred n) l -let rec list_addn n x l = +let rec list_skipn_at_least n l = + try list_skipn n l with Failure _ -> [] + +let rec list_addn n x l = if n = 0 then l else x :: (list_addn (pred n) x l) -let list_prefix_of prefl l = +let list_prefix_of prefl l = let rec prefrec = function | (h1::t1, h2::t2) -> h1 = h2 && prefrec (t1,t2) | ([], _) -> true | (_, _) -> false - in + in prefrec (prefl,l) let list_drop_prefix p l = @@ -860,7 +757,7 @@ let list_drop_prefix p l = let rec list_drop_prefix_rec = function | ([], tl) -> Some tl | (_, []) -> None - | (h1::tp, h2::tl) -> + | (h1::tp, h2::tl) -> if h1 = h2 then list_drop_prefix_rec (tp,tl) else None in match list_drop_prefix_rec (p,l) with @@ -876,7 +773,7 @@ let list_share_tails l1 l2 = let rec shr_rev acc = function | ((x1::l1), (x2::l2)) when x1 == x2 -> shr_rev (x1::acc) (l1,l2) | (l1,l2) -> (List.rev l1, List.rev l2, acc) - in + in shr_rev [] (List.rev l1, List.rev l2) let rec list_fold_map f e = function @@ -887,10 +784,10 @@ let rec list_fold_map f e = function e'',h'::t' (* (* tail-recursive version of the above function *) -let list_fold_map f e l = - let g (e,b') h = +let list_fold_map f e l = + let g (e,b') h = let (e',h') = f e h in - (e',h'::b') + (e',h'::b') in let (e',lrev) = List.fold_left g (e,[]) l in (e',List.rev lrev) @@ -914,17 +811,17 @@ let list_union_map f l acc = acc l -(* A generic cartesian product: for any operator (**), - [list_cartesian (**) [x1;x2] [y1;y2] = [x1**y1; x1**y2; x2**y1; x2**y1]], +(* A generic cartesian product: for any operator (**), + [list_cartesian (**) [x1;x2] [y1;y2] = [x1**y1; x1**y2; x2**y1; x2**y1]], and so on if there are more elements in the lists. *) -let rec list_cartesian op l1 l2 = +let rec list_cartesian op l1 l2 = list_map_append (fun x -> List.map (op x) l2) l1 -(* [list_cartesians] is an n-ary cartesian product: it iterates +(* [list_cartesians] is an n-ary cartesian product: it iterates [list_cartesian] over a list of lists. *) -let list_cartesians op init ll = +let list_cartesians op init ll = List.fold_right (list_cartesian op) ll [init] (* list_combinations [[a;b];[c;d]] gives [[a;c];[a;d];[b;c];[b;d]] *) @@ -933,12 +830,12 @@ let list_combinations l = list_cartesians (fun x l -> x::l) [] l (* Keep only those products that do not return None *) -let rec list_cartesian_filter op l1 l2 = +let rec list_cartesian_filter op l1 l2 = list_map_append (fun x -> list_map_filter (op x) l2) l1 (* Keep only those products that do not return None *) -let rec list_cartesians_filter op init ll = +let rec list_cartesians_filter op init ll = List.fold_right (list_cartesian_filter op) ll [init] (* Drop the last element of a list *) @@ -947,57 +844,76 @@ let rec list_drop_last = function [] -> assert false | hd :: [] -> [] | hd :: tl (* Arrays *) -let array_exists f v = +let array_compare item_cmp v1 v2 = + let c = compare (Array.length v1) (Array.length v2) in + if c<>0 then c else + let rec cmp = function + -1 -> 0 + | i -> + let c' = item_cmp v1.(i) v2.(i) in + if c'<>0 then c' + else cmp (i-1) in + cmp (Array.length v1 - 1) + +let array_exists f v = let rec exrec = function | -1 -> false | n -> (f v.(n)) || (exrec (n-1)) - in - exrec ((Array.length v)-1) + in + exrec ((Array.length v)-1) -let array_for_all f v = +let array_for_all f v = let rec allrec = function | -1 -> true | n -> (f v.(n)) && (allrec (n-1)) - in - allrec ((Array.length v)-1) + in + allrec ((Array.length v)-1) let array_for_all2 f v1 v2 = let rec allrec = function | -1 -> true | n -> (f v1.(n) v2.(n)) && (allrec (n-1)) - in + in let lv1 = Array.length v1 in - lv1 = Array.length v2 && allrec (pred lv1) + lv1 = Array.length v2 && allrec (pred lv1) let array_for_all3 f v1 v2 v3 = let rec allrec = function | -1 -> true | n -> (f v1.(n) v2.(n) v3.(n)) && (allrec (n-1)) - in + in let lv1 = Array.length v1 in - lv1 = Array.length v2 && lv1 = Array.length v3 && allrec (pred lv1) + lv1 = Array.length v2 && lv1 = Array.length v3 && allrec (pred lv1) let array_for_all4 f v1 v2 v3 v4 = let rec allrec = function | -1 -> true | n -> (f v1.(n) v2.(n) v3.(n) v4.(n)) && (allrec (n-1)) - in + in let lv1 = Array.length v1 in lv1 = Array.length v2 && lv1 = Array.length v3 && lv1 = Array.length v4 && - allrec (pred lv1) + allrec (pred lv1) -let array_for_all_i f i v = - let rec allrec i n = n = Array.length v || f i v.(n) && allrec (i+1) (n+1) in +let array_for_all_i f i v = + let rec allrec i n = n = Array.length v || f i v.(n) && allrec (i+1) (n+1) in allrec i 0 -let array_hd v = +exception Found of int + +let array_find_i (pred: int -> 'a -> bool) (arr: 'a array) : int option = + try + for i=0 to Array.length arr - 1 do if pred i (arr.(i)) then raise (Found i) done; + None + with Found i -> Some i + +let array_hd v = match Array.length v with | 0 -> failwith "array_hd" | _ -> v.(0) -let array_tl v = +let array_tl v = match Array.length v with | 0 -> failwith "array_tl" | n -> Array.sub v 1 (pred n) @@ -1009,12 +925,12 @@ let array_last v = let array_cons e v = Array.append [|e|] v -let array_rev t = +let array_rev t = let n=Array.length t in - if n <=0 then () + if n <=0 then () else let tmp=ref t.(0) in - for i=0 to pred (n/2) do + for i=0 to pred (n/2) do tmp:=t.((pred n)-i); t.((pred n)-i)<- t.(i); t.(i)<- !tmp @@ -1045,7 +961,7 @@ let array_fold_right2 f v1 v2 a = let array_fold_left2 f a v1 v2 = let lv1 = Array.length v1 in - let rec fold a n = + let rec fold a n = if n >= lv1 then a else fold (f a v1.(n) v2.(n)) (succ n) in if Array.length v2 <> lv1 then invalid_arg "array_fold_left2"; @@ -1053,25 +969,25 @@ let array_fold_left2 f a v1 v2 = let array_fold_left2_i f a v1 v2 = let lv1 = Array.length v1 in - let rec fold a n = + let rec fold a n = if n >= lv1 then a else fold (f n a v1.(n) v2.(n)) (succ n) in if Array.length v2 <> lv1 then invalid_arg "array_fold_left2"; fold a 0 -let array_fold_left_from n f a v = +let array_fold_left_from n f a v = let rec fold a n = if n >= Array.length v then a else fold (f a v.(n)) (succ n) - in + in fold a n -let array_fold_right_from n f v a = +let array_fold_right_from n f v a = let rec fold n = if n >= Array.length v then a else f v.(n) (fold (succ n)) - in + in fold n -let array_app_tl v l = +let array_app_tl v l = if Array.length v = 0 then invalid_arg "array_app_tl"; array_fold_right_from 1 (fun e l -> e::l) v l @@ -1091,9 +1007,9 @@ exception Local of int (* If none of the elements is changed by f we return ar itself. The for loop looks for the first such an element. - If found it is temporarily stored in a ref and the new array is produced, + If found it is temporarily stored in a ref and the new array is produced, but f is not re-applied to elements that are already checked *) -let array_smartmap f ar = +let array_smartmap f ar = let ar_size = Array.length ar in let aux = ref None in try @@ -1107,10 +1023,10 @@ let array_smartmap f ar = done; ar with - Local i -> - let copy j = - if j<i then ar.(j) - else if j=i then + Local i -> + let copy j = + if j<i then ar.(j) + else if j=i then match !aux with Some a' -> a' | None -> failwith "Error" else f (ar.(j)) in @@ -1118,8 +1034,8 @@ let array_smartmap f ar = let array_map2 f v1 v2 = if Array.length v1 <> Array.length v2 then invalid_arg "array_map2"; - if Array.length v1 == 0 then - [| |] + if Array.length v1 == 0 then + [| |] else begin let res = Array.create (Array.length v1) (f v1.(0) v2.(0)) in for i = 1 to pred (Array.length v1) do @@ -1130,8 +1046,8 @@ let array_map2 f v1 v2 = let array_map2_i f v1 v2 = if Array.length v1 <> Array.length v2 then invalid_arg "array_map2"; - if Array.length v1 == 0 then - [| |] + if Array.length v1 == 0 then + [| |] else begin let res = Array.create (Array.length v1) (f 0 v1.(0) v2.(0)) in for i = 1 to pred (Array.length v1) do @@ -1143,8 +1059,8 @@ let array_map2_i f v1 v2 = let array_map3 f v1 v2 v3 = if Array.length v1 <> Array.length v2 || Array.length v1 <> Array.length v3 then invalid_arg "array_map3"; - if Array.length v1 == 0 then - [| |] + if Array.length v1 == 0 then + [| |] else begin let res = Array.create (Array.length v1) (f v1.(0) v2.(0) v3.(0)) in for i = 1 to pred (Array.length v1) do @@ -1185,7 +1101,7 @@ let pure_functional = false let array_fold_map' f v e = if pure_functional then let (l,e) = - Array.fold_right + Array.fold_right (fun x (l,e) -> let (y,e) = f x e in (y::l,e)) v ([],e) in (Array.of_list l,e) @@ -1201,8 +1117,8 @@ let array_fold_map f e v = let array_fold_map2' f v1 v2 e = let e' = ref e in - let v' = - array_map2 (fun x1 x2 -> let (y,e) = f x1 x2 !e' in e' := e; y) v1 v2 + let v' = + array_map2 (fun x1 x2 -> let (y,e) = f x1 x2 !e' in e' := e; y) v1 v2 in (v',!e') @@ -1223,6 +1139,11 @@ let array_union_map f a acc = acc a +let array_rev_to_list a = + let rec tolist i res = + if i >= Array.length a then res else tolist (i+1) (a.(i) :: res) in + tolist 0 [] + (* Matrices *) let matrix_transpose mat = @@ -1235,10 +1156,12 @@ let identity x = x let compose f g x = f (g x) -let iterate f = +let const x _ = x + +let iterate f = let rec iterate_f n x = if n <= 0 then x else iterate_f (pred n) (f x) - in + in iterate_f let repeat n f x = @@ -1247,7 +1170,7 @@ let repeat n f x = let iterate_for a b f x = let rec iterate i v = if i > b then v else iterate (succ i) (f i v) in iterate a x - + (* Misc *) type ('a,'b) union = Inl of 'a | Inr of 'b @@ -1263,27 +1186,27 @@ let intmap_to_list m = Intmap.fold (fun n v l -> (n,v)::l) m [] let intmap_inv m b = Intmap.fold (fun n v l -> if v = b then n::l else l) m [] -let interval n m = +let interval n m = let rec interval_n (l,m) = if n > m then l else interval_n (m::l,pred m) - in + in interval_n ([],m) -let map_succeed f = - let rec map_f = function +let map_succeed f = + let rec map_f = function | [] -> [] | h::t -> try (let x = f h in x :: map_f t) with Failure _ -> map_f t - in - map_f + in + map_f (* Pretty-printing *) - + let pr_spc = spc let pr_fnl = fnl let pr_int = int let pr_str = str -let pr_coma () = str "," ++ spc () +let pr_comma () = str "," ++ spc () let pr_semicolon () = str ";" ++ spc () let pr_bar () = str "|" ++ spc () let pr_arg pr x = spc () ++ pr x @@ -1294,7 +1217,7 @@ let nth n = str (ordinal n) (* [prlist pr [a ; ... ; c]] outputs [pr a ++ ... ++ pr c] *) -let rec prlist elem l = match l with +let rec prlist elem l = match l with | [] -> mt () | h::t -> Stream.lapp (fun () -> elem h) (prlist elem t) @@ -1302,7 +1225,7 @@ let rec prlist elem l = match l with if a strict behavior is needed, use [prlist_strict] instead. evaluation is done from left to right. *) -let rec prlist_strict elem l = match l with +let rec prlist_strict elem l = match l with | [] -> mt () | h::t -> let e = elem h in let r = prlist_strict elem t in e++r @@ -1326,22 +1249,22 @@ let rec pr_sequence elem = function let e = elem h and r = pr_sequence elem t in if e = mt () then r else e ++ spc () ++ r -(* [pr_enum pr [a ; b ; ... ; c]] outputs +(* [pr_enum pr [a ; b ; ... ; c]] outputs [pr a ++ str "," ++ pr b ++ str "," ++ ... ++ str "and" ++ pr c] *) let pr_enum pr l = let c,l' = list_sep_last l in - prlist_with_sep pr_coma pr l' ++ + prlist_with_sep pr_comma pr l' ++ (if l'<>[] then str " and" ++ spc () else mt()) ++ pr c let pr_vertical_list pr = function | [] -> str "none" ++ fnl () | l -> fnl () ++ str " " ++ hov 0 (prlist_with_sep pr_fnl pr l) ++ fnl () - + let prvecti elem v = let n = Array.length v in let rec pr i = - if i = 0 then + if i = 0 then elem 0 v.(0) else let r = pr (i-1) and e = elem i v.(i) in r ++ e @@ -1353,10 +1276,10 @@ let prvecti elem v = let prvect_with_sep sep elem v = let rec pr n = - if n = 0 then + if n = 0 then elem v.(0) - else - let r = pr (n-1) and s = sep() and e = elem v.(n) in + else + let r = pr (n-1) and s = sep() and e = elem v.(n) in r ++ s ++ e in let n = Array.length v in @@ -1410,64 +1333,62 @@ let memon_eq eq n f = (*s Size of ocaml values. *) module Size = struct - - open Obj (*s Pointers already visited are stored in a hash-table, where comparisons are done using physical equality. *) module H = Hashtbl.Make( - struct - type t = Obj.t - let equal = (==) - let hash o = Hashtbl.hash (magic o : int) + struct + type t = Obj.t + let equal = (==) + let hash o = Hashtbl.hash (Obj.magic o : int) end) - + let node_table = (H.create 257 : unit H.t) - + let in_table o = try H.find node_table o; true with Not_found -> false - + let add_in_table o = H.add node_table o () - + let reset_table () = H.clear node_table - + (*s Objects are traversed recursively, as soon as their tags are less than [no_scan_tag]. [count] records the numbers of words already visited. *) - let size_of_double = size (repr 1.0) - + let size_of_double = Obj.size (Obj.repr 1.0) + let count = ref 0 - + let rec traverse t = if not (in_table t) then begin add_in_table t; - if is_block t then begin - let n = size t in - let tag = tag t in - if tag < no_scan_tag then begin + if Obj.is_block t then begin + let n = Obj.size t in + let tag = Obj.tag t in + if tag < Obj.no_scan_tag then begin count := !count + 1 + n; for i = 0 to n - 1 do - let f = field t i in - if is_block f then traverse f + let f = Obj.field t i in + if Obj.is_block f then traverse f done - end else if tag = string_tag then - count := !count + 1 + n - else if tag = double_tag then + end else if tag = Obj.string_tag then + count := !count + 1 + n + else if tag = Obj.double_tag then count := !count + size_of_double - else if tag = double_array_tag then - count := !count + 1 + size_of_double * n + else if tag = Obj.double_array_tag then + count := !count + 1 + size_of_double * n else incr count end end - + (*s Sizes of objects in words and in bytes. The size in bytes is computed system-independently according to [Sys.word_size]. *) let size_w o = reset_table (); count := 0; - traverse (repr o); + traverse (Obj.repr o); !count let size_b o = (size_w o) * (Sys.word_size / 8) @@ -1493,6 +1414,5 @@ let heap_size_kb () = (heap_size () + 1023) / 1024 (*s interruption *) let interrupt = ref false -let check_for_interrupt () = +let check_for_interrupt () = if !interrupt then begin interrupt := false; raise Sys.Break end - diff --git a/lib/util.mli b/lib/util.mli index 97bda074..cd8e3135 100644 --- a/lib/util.mli +++ b/lib/util.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(*i $Id: util.mli 13200 2010-06-25 22:36:25Z letouzey $ i*) +(*i $Id$ i*) (*i*) open Pp @@ -26,12 +26,19 @@ exception UserError of string * std_ppcmds val error : string -> 'a val errorlabstrm : string -> std_ppcmds -> 'a +exception AlreadyDeclared of std_ppcmds +val alreadydeclared : std_ppcmds -> 'a + +exception AnomalyOnError of string * exn + (* [todo] is for running of an incomplete code its implementation is "do nothing" (or print a message), but this function should not be used in a released code *) val todo : string -> unit +exception Timeout + type loc = Compat.loc type 'a located = loc * 'a @@ -57,6 +64,12 @@ exception Error_in_file of string * (bool * string * loc) * exn val on_fst : ('a -> 'b) -> 'a * 'c -> 'b * 'c val on_snd : ('a -> 'b) -> 'c * 'a -> 'c * 'b +(* Mapping under triple *) + +val on_pi1 : ('a -> 'b) -> 'a * 'c * 'd -> 'b * 'c * 'd +val on_pi2 : ('a -> 'b) -> 'c * 'a * 'd -> 'c * 'b * 'd +val on_pi3 : ('a -> 'b) -> 'c * 'd * 'a -> 'c * 'd * 'b + (*s Projections from triplets *) val pi1 : 'a * 'b * 'c -> 'a @@ -75,6 +88,7 @@ val is_blank : char -> bool val explode : string -> string list val implode : string list -> string val strip : string -> string +val drop_simple_quotes : string -> string val string_index_from : string -> int -> string -> int val string_string_contains : where:string -> what:string -> bool val plural : int -> string -> string @@ -98,6 +112,7 @@ val ascii_of_ident : string -> string (*s Lists. *) +val list_compare : ('a -> 'a -> int) -> 'a list -> 'a list -> int val list_add_set : 'a -> 'a list -> 'a list val list_eq_set : 'a list -> 'a list -> bool val list_intersect : 'a list -> 'a list -> 'a list @@ -119,16 +134,18 @@ val list_map_filter : ('a -> 'b option) -> 'a list -> 'b list val list_smartmap : ('a -> 'a) -> 'a list -> 'a list val list_map_left : ('a -> 'b) -> 'a list -> 'b list val list_map_i : (int -> 'a -> 'b) -> int -> 'a list -> 'b list -val list_map2_i : +val list_map2_i : (int -> 'a -> 'b -> 'c) -> int -> 'a list -> 'b list -> 'c list val list_map3 : ('a -> 'b -> 'c -> 'd) -> 'a list -> 'b list -> 'c list -> 'd list val list_map4 : ('a -> 'b -> 'c -> 'd -> 'e) -> 'a list -> 'b list -> 'c list -> 'd list -> 'e list +val list_filter_i : + (int -> 'a -> bool) -> 'a list -> 'a list (* [list_index] returns the 1st index of an element in a list (counting from 1) *) val list_index : 'a -> 'a list -> int (* [list_unique_index x l] returns [Not_found] if [x] doesn't occur exactly once *) -val list_unique_index : 'a -> 'a list -> int +val list_unique_index : 'a -> 'a list -> int (* [list_index0] behaves as [list_index] except that it starts counting at 0 *) val list_index0 : 'a -> 'a list -> int val list_iter3 : ('a -> 'b -> 'c -> unit) -> 'a list -> 'b list -> 'c list -> unit @@ -151,16 +168,18 @@ val list_uniquize : 'a list -> 'a list (* merges two sorted lists and preserves the uniqueness property: *) val list_merge_uniq : ('a -> 'a -> int) -> 'a list -> 'a list -> 'a list val list_subset : 'a list -> 'a list -> bool -val list_split_at : ('a -> bool) -> 'a list -> 'a list * 'a list -val list_split_by : ('a -> bool) -> 'a list -> 'a list * 'a list +val list_split_at : int -> 'a list -> 'a list*'a list +val list_split_when : ('a -> bool) -> 'a list -> 'a list * 'a list val list_split3 : ('a * 'b * 'c) list -> 'a list * 'b list * 'c list val list_partition_by : ('a -> 'a -> bool) -> 'a list -> 'a list list val list_firstn : int -> 'a list -> 'a list val list_last : 'a list -> 'a val list_lastn : int -> 'a list -> 'a list -val list_skipn : int -> 'a list -> 'a list +val list_skipn : int -> 'a list -> 'a list +val list_skipn_at_least : int -> 'a list -> 'a list val list_addn : int -> 'a -> 'a list -> 'a list val list_prefix_of : 'a list -> 'a list -> bool +(* [list_drop_prefix p l] returns [t] if [l=p++t] else return [l] *) val list_drop_prefix : 'a list -> 'a list -> 'a list val list_drop_last : 'a list -> 'a list (* [map_append f [x1; ...; xn]] returns [(f x1)@(f x2)@...@(f xn)] *) @@ -174,11 +193,11 @@ val list_share_tails : 'a list -> 'a list -> 'a list * 'a list * 'a list val list_fold_map : ('a -> 'b -> 'a * 'c) -> 'a -> 'b list -> 'a * 'c list val list_fold_map' : ('b -> 'a -> 'c * 'a) -> 'b list -> 'a -> 'c list * 'a val list_map_assoc : ('a -> 'b) -> ('c * 'a) list -> ('c * 'b) list -(* A generic cartesian product: for any operator (**), - [list_cartesian (**) [x1;x2] [y1;y2] = [x1**y1; x1**y2; x2**y1; x2**y1]], +(* A generic cartesian product: for any operator (**), + [list_cartesian (**) [x1;x2] [y1;y2] = [x1**y1; x1**y2; x2**y1; x2**y1]], and so on if there are more elements in the lists. *) val list_cartesian : ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list -(* [list_cartesians] is an n-ary cartesian product: it iterates +(* [list_cartesians] is an n-ary cartesian product: it iterates [list_cartesian] over a list of lists. *) val list_cartesians : ('a -> 'b -> 'b) -> 'b -> 'a list list -> 'b list (* list_combinations [[a;b];[c;d]] returns [[a;c];[a;d];[b;c];[b;d]] *) @@ -193,6 +212,7 @@ val list_union_map : ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b (*s Arrays. *) +val array_compare : ('a -> 'a -> int) -> 'a array -> 'a array -> int val array_exists : ('a -> bool) -> 'a array -> bool val array_for_all : ('a -> bool) -> 'a array -> bool val array_for_all2 : ('a -> 'b -> bool) -> 'a array -> 'b array -> bool @@ -201,19 +221,20 @@ val array_for_all3 : ('a -> 'b -> 'c -> bool) -> val array_for_all4 : ('a -> 'b -> 'c -> 'd -> bool) -> 'a array -> 'b array -> 'c array -> 'd array -> bool val array_for_all_i : (int -> 'a -> bool) -> int -> 'a array -> bool +val array_find_i : (int -> 'a -> bool) -> 'a array -> int option val array_hd : 'a array -> 'a val array_tl : 'a array -> 'a array val array_last : 'a array -> 'a val array_cons : 'a -> 'a array -> 'a array val array_rev : 'a array -> unit -val array_fold_right_i : +val array_fold_right_i : (int -> 'b -> 'a -> 'a) -> 'b array -> 'a -> 'a val array_fold_left_i : (int -> 'a -> 'b -> 'a) -> 'a -> 'b array -> 'a val array_fold_right2 : ('a -> 'b -> 'c -> 'c) -> 'a array -> 'b array -> 'c -> 'c -val array_fold_left2 : +val array_fold_left2 : ('a -> 'b -> 'c -> 'a) -> 'a -> 'b array -> 'c array -> 'a -val array_fold_left2_i : +val array_fold_left2_i : (int -> 'a -> 'b -> 'c -> 'a) -> 'a -> 'b array -> 'c array -> 'a val array_fold_left_from : int -> ('a -> 'b -> 'a) -> 'a -> 'b array -> 'a val array_fold_right_from : int -> ('a -> 'b -> 'b) -> 'a array -> 'b -> 'b @@ -224,7 +245,7 @@ val array_chop : int -> 'a array -> 'a array * 'a array val array_smartmap : ('a -> 'a) -> 'a array -> 'a array val array_map2 : ('a -> 'b -> 'c) -> 'a array -> 'b array -> 'c array val array_map2_i : (int -> 'a -> 'b -> 'c) -> 'a array -> 'b array -> 'c array -val array_map3 : +val array_map3 : ('a -> 'b -> 'c -> 'd) -> 'a array -> 'b array -> 'c array -> 'd array val array_map_left : ('a -> 'b) -> 'a array -> 'b array val array_map_left_pair : ('a -> 'b) -> 'a array -> ('c -> 'd) -> 'c array -> @@ -236,6 +257,7 @@ val array_fold_map2' : ('a -> 'b -> 'c -> 'd * 'c) -> 'a array -> 'b array -> 'c -> 'd array * 'c val array_distinct : 'a array -> bool val array_union_map : ('a -> 'b -> 'b) -> 'a array -> 'b -> 'b +val array_rev_to_list : 'a array -> 'a list (*s Matrices *) @@ -245,6 +267,7 @@ val matrix_transpose : 'a list list -> 'a list list val identity : 'a -> 'a val compose : ('a -> 'b) -> ('c -> 'a) -> 'c -> 'b +val const : 'a -> 'b -> 'a val iterate : ('a -> 'a) -> int -> 'a -> 'a val repeat : int -> ('a -> unit) -> 'a -> unit val iterate_for : int -> int -> (int -> 'a -> 'a) -> 'a -> 'a @@ -275,7 +298,7 @@ val pr_spc : unit -> std_ppcmds val pr_fnl : unit -> std_ppcmds val pr_int : int -> std_ppcmds val pr_str : string -> std_ppcmds -val pr_coma : unit -> std_ppcmds +val pr_comma : unit -> std_ppcmds val pr_semicolon : unit -> std_ppcmds val pr_bar : unit -> std_ppcmds val pr_arg : ('a -> std_ppcmds) -> 'a -> std_ppcmds |