summaryrefslogtreecommitdiff
path: root/lib
diff options
context:
space:
mode:
Diffstat (limited to 'lib')
-rw-r--r--lib/bigint.ml25
-rw-r--r--lib/bigint.mli4
-rw-r--r--lib/bstack.ml18
-rw-r--r--lib/bstack.mli3
-rw-r--r--lib/compat.ml410
-rw-r--r--lib/edit.ml13
-rw-r--r--lib/flags.ml (renamed from lib/options.ml)38
-rw-r--r--lib/flags.mli (renamed from lib/options.mli)14
-rw-r--r--lib/gmap.ml4
-rw-r--r--lib/gmap.mli3
-rw-r--r--lib/gset.mli4
-rw-r--r--lib/option.ml165
-rw-r--r--lib/option.mli112
-rw-r--r--lib/pp.ml4116
-rw-r--r--lib/pp.mli10
-rw-r--r--lib/pp_control.ml9
-rw-r--r--lib/pp_control.mli6
-rw-r--r--lib/rtree.ml168
-rw-r--r--lib/rtree.mli61
-rw-r--r--lib/system.ml32
-rw-r--r--lib/system.mli2
-rw-r--r--lib/util.ml540
-rw-r--r--lib/util.mli69
23 files changed, 1185 insertions, 241 deletions
diff --git a/lib/bigint.ml b/lib/bigint.ml
index 5bcceb5c..7671b0fc 100644
--- a/lib/bigint.ml
+++ b/lib/bigint.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: bigint.ml 7305 2005-08-19 19:51:02Z letouzey $ *)
+(* $Id: bigint.ml 9821 2007-05-11 17:00:58Z aspiwack $ *)
(*i*)
open Pp
@@ -350,6 +350,29 @@ let is_pos_or_zero n = is_pos_or_zero (ints_of_z n)
let pr_bigint n = str (to_string n)
+(* spiwack: computes n^m *)
+(* The basic idea of the algorithm is that n^(2m) = (n^2)^m *)
+(* In practice the algorithm performs :
+ k*n^0 = k
+ k*n^(2m) = k*(n*n)^m
+ k*n^(2m+1) = (n*k)*(n*n)^m *)
+let pow =
+ let rec pow_aux odd_rest n m = (* odd_rest is the k from above *)
+ if is_neg_or_zero m then
+ odd_rest
+ else
+ let (quo,rem) = div2_with_rest m in
+ pow_aux
+ ((* [if m mod 2 = 1]*)
+ if rem then
+ mult n odd_rest
+ else
+ odd_rest )
+ (* quo = [m/2] *)
+ (mult n n) quo
+ in
+ pow_aux one
+
(* Testing suite *)
let check () =
diff --git a/lib/bigint.mli b/lib/bigint.mli
index 7a835a49..f6d3da7b 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 6616 2005-01-21 17:18:23Z herbelin $ i*)
+(*i $Id: bigint.mli 9821 2007-05-11 17:00:58Z aspiwack $ i*)
(*i*)
open Pp
@@ -42,4 +42,6 @@ val is_pos_or_zero : bigint -> bool
val is_neg_or_zero : bigint -> bool
val neg : bigint -> bigint
+val pow : bigint -> bigint -> bigint
+
val pr_bigint : bigint -> std_ppcmds
diff --git a/lib/bstack.ml b/lib/bstack.ml
index b86dccf9..35bbf32b 100644
--- a/lib/bstack.ml
+++ b/lib/bstack.ml
@@ -6,19 +6,27 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: bstack.ml 5920 2004-07-16 20:01:26Z herbelin $ *)
+(* $Id: bstack.ml 10441 2008-01-15 16:37:46Z lmamane $ *)
(* Queues of a given length *)
open Util
+(* - size is the count of elements actually in the queue
+ - depth is the the amount of elements pushed in the queue (and not popped)
+ in particular, depth >= size always and depth > size if the queue overflowed
+ (and forgot older elements)
+ *)
+
type 'a t = {mutable pos : int;
mutable size : int;
+ mutable depth : int;
stack : 'a array}
let create depth e =
{pos = 0;
size = 1;
+ depth = 1;
stack = Array.create depth e}
(*
@@ -37,14 +45,16 @@ let decr_pos bs =
let push bs e =
incr_pos bs;
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.depth <- bs.depth - 1;
let oldpos = bs.pos in
decr_pos bs;
- (* Release the memory at oldpos, by coyping what is at new pos *)
+ (* Release the memory at oldpos, by copying what is at new pos *)
bs.stack.(oldpos) <- bs.stack.(bs.pos)
end
@@ -60,4 +70,6 @@ let app_repl bs f =
if bs.size = 0 then error "Nothing on the stack"
else bs.stack.(bs.pos) <- f (bs.stack.(bs.pos))
-let depth bs = bs.size
+let depth bs = bs.depth
+
+let size bs = bs.size
diff --git a/lib/bstack.mli b/lib/bstack.mli
index f018d155..ca2b5f02 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 5920 2004-07-16 20:01:26Z herbelin $ i*)
+(*i $Id: bstack.mli 10441 2008-01-15 16:37:46Z lmamane $ i*)
(* Bounded stacks. If the depth is [None], then there is no depth limit. *)
@@ -19,3 +19,4 @@ val app_repl : 'a t -> ('a -> 'a) -> unit
val pop : 'a t -> unit
val top : 'a t -> 'a
val depth : 'a t -> int
+val size : 'a t -> int
diff --git a/lib/compat.ml4 b/lib/compat.ml4
index 372d2be3..40cffadb 100644
--- a/lib/compat.ml4
+++ b/lib/compat.ml4
@@ -6,13 +6,13 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* Compatibility file depending on ocaml version *)
+(*i camlp4use: "pa_macro.cmo" i*)
-(* type loc is different in 3.08 *)
+(* Compatibility file depending on ocaml version *)
IFDEF OCAML309 THEN DEFINE OCAML308 END
-IFDEF CAMLP5 THEN
+IFDEF CAMLP5 THEN
module M = struct
type loc = Stdpp.location
let dummy_loc = Stdpp.dummy_loc
@@ -45,7 +45,7 @@ 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)
@@ -63,8 +63,8 @@ END
type loc = M.loc
let dummy_loc = M.dummy_loc
-let unloc = M.unloc
let make_loc = M.make_loc
+let unloc = M.unloc
let join_loc = M.join_loc
type token = M.token
type lexer = M.lexer
diff --git a/lib/edit.ml b/lib/edit.ml
index 03420992..380abfd8 100644
--- a/lib/edit.ml
+++ b/lib/edit.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: edit.ml 6947 2005-04-20 16:18:41Z coq $ *)
+(* $Id: edit.ml 10441 2008-01-15 16:37:46Z lmamane $ *)
open Pp
open Util
@@ -80,7 +80,7 @@ let undo e n =
| None -> invalid_arg "Edit.undo"
| Some d ->
let (bs,_) = Hashtbl.find e.buf d in
- if Bstack.depth bs = 1 & n > 0 then
+ if n >= Bstack.size bs then
errorlabstrm "Edit.undo" (str"Undo stack exhausted");
repeat n Bstack.pop bs
@@ -102,15 +102,16 @@ let undo_todepth e n =
else () (* if there is no proof in progress, then n must be zero *)
| Some d ->
let (bs,_) = Hashtbl.find e.buf d in
- if Bstack.depth bs < n then
+ let ucnt = Bstack.depth bs - n in
+ if ucnt >= Bstack.size bs then
errorlabstrm "Edit.undo_todepth" (str"Undo stack would be exhausted");
- repeat (Bstack.depth bs - n) Bstack.pop bs
+ repeat ucnt Bstack.pop bs
-let create e (d,b,c,udepth) =
+let create e (d,b,c,usize) =
if Hashtbl.mem e.buf d then
errorlabstrm "Edit.create"
(str"Already editing something of that name");
- let bs = Bstack.create udepth b in
+ let bs = Bstack.create usize b in
Hashtbl.add e.buf d (bs,c)
let delete e d =
diff --git a/lib/options.ml b/lib/flags.ml
index 53a7e9cf..de971c7c 100644
--- a/lib/options.ml
+++ b/lib/flags.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: options.ml 10105 2007-08-30 16:53:32Z herbelin $ *)
+(*i $Id: flags.ml 11077 2008-06-09 11:26:32Z herbelin $ i*)
open Util
@@ -32,6 +32,8 @@ let dont_load_proofs = ref false
let raw_print = ref false
+let unicode_syntax = ref false
+
(* Translate *)
let translate = ref false
let make_translate f = translate := f
@@ -63,6 +65,10 @@ let if_verbose f x = if not !silent then f x
let hash_cons_proofs = ref true
+let warn = ref true
+let make_warn flag = warn := flag; ()
+let if_warn f x = if !warn then f x
+
(* The number of printed hypothesis in a goal *)
let print_hyps_limit = ref (None : int option)
@@ -96,29 +102,31 @@ let dump_it () =
let _ = at_exit dump_it
-(* Options for the virtual machine *)
+(* Flags.for the virtual machine *)
let boxed_definitions = ref true
let set_boxed_definitions b = boxed_definitions := b
let boxed_definitions _ = !boxed_definitions
-(* Options for external tools *)
+(* Flags.for external tools *)
+
+let subst_command_placeholder s t =
+ let buff = Buffer.create (String.length s + String.length t) in
+ let i = ref 0 in
+ while (!i < String.length s) do
+ if s.[!i] = '%' & !i+1 < String.length s & s.[!i+1] = 's'
+ then (Buffer.add_string buff t;incr i)
+ else Buffer.add_char buff s.[!i];
+ incr i
+ done;
+ Buffer.contents buff
let browser_cmd_fmt =
try
let coq_netscape_remote_var = "COQREMOTEBROWSER" in
- let coq_netscape_remote = Sys.getenv coq_netscape_remote_var in
- let i = Util.string_index_from coq_netscape_remote 0 "%s" in
- let pre = String.sub coq_netscape_remote 0 i in
- let post = String.sub coq_netscape_remote (i + 2)
- (String.length coq_netscape_remote - (i + 2)) in
- if Util.string_string_contains ~where:post ~what:"%s" then
- error ("The environment variable \"" ^
- coq_netscape_remote_var ^
- "\" must contain exactly one placeholder \"%s\".")
- else pre,post
+ Sys.getenv coq_netscape_remote_var
with
Not_found ->
if Sys.os_type = "Win32"
- then "C:\\PROGRA~1\\INTERN~1\\IEXPLORE ", ""
- else "firefox -remote \"OpenURL(", ")\""
+ then "C:\\PROGRA~1\\INTERN~1\\IEXPLORE %s"
+ else "firefox -remote \"OpenURL(%s,new-tab)\" || firefox %s &"
diff --git a/lib/options.mli b/lib/flags.mli
index 30d585fb..1fcae990 100644
--- a/lib/options.mli
+++ b/lib/flags.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: options.mli 9191 2006-09-29 15:45:42Z courtieu $ i*)
+(*i $Id: flags.mli 10921 2008-05-12 12:27:25Z msozeau $ i*)
(* Global options of the system. *)
@@ -27,6 +27,8 @@ val dont_load_proofs : bool ref
val raw_print : bool ref
+val unicode_syntax : bool ref
+
val translate : bool ref
val make_translate : bool -> unit
val do_translate : unit -> bool
@@ -40,6 +42,9 @@ val silently : ('a -> 'b) -> 'a -> 'b
val if_silent : ('a -> unit) -> 'a -> unit
val if_verbose : ('a -> unit) -> 'a -> unit
+val make_warn : bool -> unit
+val if_warn : ('a -> unit) -> 'a -> unit
+
val hash_cons_proofs : bool ref
(* Temporary activate an option ('c must be an atomic type) *)
@@ -65,7 +70,8 @@ val boxed_definitions : unit -> bool
(* Options for external tools *)
-(* Returns head and tail of printf string format *)
-(* ocaml doesn't allow not applied formats *)
-val browser_cmd_fmt : string * string
+(* Returns string format for default browser to use from Coq or CoqIDE *)
+val browser_cmd_fmt : string
+(* Substitute %s in the first chain by the second chain *)
+val subst_command_placeholder : string -> string -> string
diff --git a/lib/gmap.ml b/lib/gmap.ml
index 884305d9..7a4cb56e 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 7925 2006-01-24 23:20:39Z herbelin $ *)
+(* $Id: gmap.ml 10250 2007-10-23 15:02:23Z aspiwack $ *)
(* Maps using the generic comparison function of ocaml. Code borrowed from
the ocaml standard library (Copyright 1996, INRIA). *)
@@ -16,6 +16,8 @@
let empty = Empty
+ let is_empty = function Empty -> true | _ -> false
+
let height = function
Empty -> 0
| Node(_,_,_,_,h) -> h
diff --git a/lib/gmap.mli b/lib/gmap.mli
index 79958fab..5186cff4 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 5920 2004-07-16 20:01:26Z herbelin $ i*)
+(*i $Id: gmap.mli 10250 2007-10-23 15:02:23Z aspiwack $ i*)
(* Maps using the generic comparison function of ocaml. Same interface as
the module [Map] from the ocaml standard library. *)
@@ -14,6 +14,7 @@
type ('a,'b) t
val empty : ('a,'b) t
+val is_empty : ('a,'b) t -> bool
val add : 'a -> 'b -> ('a,'b) t -> ('a,'b) t
val find : 'a -> ('a,'b) t -> 'b
val remove : 'a -> ('a,'b) t -> ('a,'b) t
diff --git a/lib/gset.mli b/lib/gset.mli
index 0f14368f..5c794381 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 5920 2004-07-16 20:01:26Z herbelin $ i*)
+(*i $Id: gset.mli 10840 2008-04-23 21:29:34Z herbelin $ i*)
(* Sets using the generic comparison function of ocaml. Same interface as
the module [Set] from the ocaml standard library. *)
@@ -26,7 +26,7 @@ val compare : 'a t -> 'a t -> int
val equal : 'a t -> 'a t -> bool
val subset : 'a t -> 'a t -> bool
val iter : ('a -> unit) -> 'a t -> unit
-val fold : ('a -> 'a -> 'a) -> 'a t -> 'a -> 'a
+val fold : ('a -> 'b -> 'b) -> 'a t -> 'b -> 'b
val cardinal : 'a t -> int
val elements : 'a t -> 'a list
val min_elt : 'a t -> 'a
diff --git a/lib/option.ml b/lib/option.ml
new file mode 100644
index 00000000..34749b8c
--- /dev/null
+++ b/lib/option.ml
@@ -0,0 +1,165 @@
+(************************************************************************)
+(* 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 $Id: option.ml 10739 2008-04-01 14:45:20Z herbelin $ i*)
+
+(** Module implementing basic combinators for OCaml option type.
+ It tries follow closely the style of OCaml standard library.
+
+ Actually, some operations have the same name as [List] ones:
+ they actually are similar considering ['a option] as a type
+ of lists with at most one element. *)
+
+(** [has_some x] is [true] if [x] is of the form [Some y] and [false]
+ otherwise. *)
+let has_some = function
+ | None -> false
+ | _ -> true
+
+exception IsNone
+
+(** [get x] returns [y] where [x] is [Some y]. It raises IsNone
+ if [x] equals [None]. *)
+let get = function
+ | Some y -> y
+ | _ -> raise IsNone
+
+(** [make x] returns [Some x]. *)
+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
+ Some x
+ else
+ None
+
+
+(** [flatten x] is [Some y] if [x] is [Some (Some y)] and [None] otherwise. *)
+let flatten = function
+ | Some (Some y) -> Some y
+ | _ -> None
+
+
+(** {6 "Iterators"} ***)
+
+(** [iter f x] executes [f y] if [x] equals [Some y]. It does nothing
+ otherwise. *)
+let iter f = function
+ | Some y -> f y
+ | _ -> ()
+
+
+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 =
+ match x,y with
+ | Some z, Some w -> f z w
+ | None,None -> ()
+ | _,_ -> raise Heterogeneous
+
+(** [map f x] is [None] if [x] is [None] and [Some (f y)] if [x] is [Some y]. *)
+let map f = function
+ | Some y -> Some (f y)
+ | _ -> None
+
+(** [smartmap f x] does the same as [map f x] except that it tries to share
+ some memory. *)
+let smartmap f = function
+ | Some y as x -> let y' = f y in if y' == y then x else Some y'
+ | _ -> None
+
+(** [fold_left f a x] is [f a y] if [x] is [Some y], and [a] otherwise. *)
+let fold_left f a = function
+ | Some y -> f a y
+ | _ -> a
+
+(** [fold_left2 f a x y] is [f z w] if [x] is [Some z] and [y] is [Some w].
+ It is [a] if both [x] and [y] are [None]. Otherwise it raises
+ [Heterogeneous]. *)
+let fold_left2 f a x y =
+ match x,y with
+ | Some x, Some y -> f a x y
+ | None, None -> a
+ | _ -> 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 =
+ match x with
+ | Some y -> f y a
+ | _ -> a
+
+
+(** {6 More Specific operations} ***)
+
+(** [default a x] is [y] if [x] is [Some y] and [a] otherwise. *)
+let default a = function
+ | Some y -> y
+ | _ -> a
+
+(** [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
+ [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
+ [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
+ [Some w]. It is [None] otherwise. *)
+let lift2 f x y =
+ match x,y with
+ | Some z, Some w -> Some (f z w)
+ | _,_ -> None
+
+
+
+(** {6 Operations with Lists} *)
+
+module List =
+ 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
+
+
+
+(** {6 Miscelaneous Primitives} *)
+
+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
+ it returns [true], if they are bothe [Some _] then
+ [f] is called. Otherwise it returns [false]. *)
+ let compare f x y =
+ match x,y with
+ | None, None -> true
+ | Some z, Some w -> f z w
+ | _,_ -> false
+end
diff --git a/lib/option.mli b/lib/option.mli
new file mode 100644
index 00000000..d9c18d88
--- /dev/null
+++ b/lib/option.mli
@@ -0,0 +1,112 @@
+(************************************************************************)
+(* 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: option.mli 10739 2008-04-01 14:45:20Z herbelin $ *)
+
+(** Module implementing basic combinators for OCaml option type.
+ It tries follow closely the style of OCaml standard library.
+
+ Actually, some operations have the same name as [List] ones:
+ they actually are similar considering ['a option] as a type
+ of lists with at most one element. *)
+
+(** [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
+ if [x] equals [None]. *)
+val get : 'a option -> 'a
+
+(** [make x] returns [Some x]. *)
+val make : 'a -> 'a option
+
+(** [init b x] returns [Some x] if [b] is [true] and [None] otherwise. *)
+val init : bool -> 'a -> 'a option
+
+(** [flatten x] is [Some y] if [x] is [Some (Some y)] and [None] otherwise. *)
+val flatten : 'a option option -> 'a option
+
+
+(** {6 "Iterators"} ***)
+
+(** [iter f x] executes [f y] if [x] equals [Some y]. It does nothing
+ otherwise. *)
+val iter : ('a -> unit) -> 'a option -> unit
+
+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. *)
+val iter2 : ('a -> 'b -> unit) -> 'a option -> 'b option -> unit
+
+(** [map f x] is [None] if [x] is [None] and [Some (f y)] if [x] is [Some y]. *)
+val map : ('a -> 'b) -> 'a option -> 'b option
+
+(** [smartmap f x] does the same as [map f x] except that it tries to share
+ some memory. *)
+val smartmap : ('a -> 'a) -> 'a option -> 'a option
+
+(** [fold_left f a x] is [f a y] if [x] is [Some y], and [a] otherwise. *)
+val fold_left : ('b -> 'a -> 'b) -> 'b -> 'a option -> 'b
+
+(** [fold_left2 f a x y] is [f z w] if [x] is [Some z] and [y] is [Some w].
+ It is [a] if both [x] and [y] are [None]. Otherwise it raises
+ [Heterogeneous]. *)
+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
+
+
+(** {6 More Specific Operations} ***)
+
+(** [default a x] is [y] if [x] is [Some y] and [a] otherwise. *)
+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
+ [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
+ [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
+ [Some w]. It is [None] otherwise. *)
+val lift2 : ('a -> 'b -> 'c) -> 'a option -> 'b option -> 'c option
+
+
+(** {6 Operations with Lists} *)
+
+module List : sig
+ (** [List.cons x l] equals [y::l] if [x] is [Some y] and [l] otherwise. *)
+ val cons : 'a option -> 'a list -> 'a list
+
+ (** [List.flatten l] is the list of all the [y]s such that [l] contains
+ [Some y] (in the same order). *)
+ val flatten : 'a option list -> 'a list
+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
+ 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
+end
+
diff --git a/lib/pp.ml4 b/lib/pp.ml4
index 88efc5f2..616302ac 100644
--- a/lib/pp.ml4
+++ b/lib/pp.ml4
@@ -6,17 +6,18 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: pp.ml4 8747 2006-04-27 16:00:49Z courtieu $ *)
+(* $Id: pp.ml4 10803 2008-04-16 09:30:05Z cek $ *)
open Pp_control
(* This should not be used outside of this file. Use
- Options.print_emacs instead. This one is updated when reading
+ Flags.print_emacs instead. This one is updated when reading
command line options. This was the only way to make [Pp] depend on
- an option without creating a circularity: [Options] -> [Util] ->
- [Pp] -> [Options] *)
+ an option without creating a circularity: [Flags. -> [Util] ->
+ [Pp] -> [Flags. *)
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:
\begin{description}
@@ -129,19 +130,17 @@ let align () = [< 'Ppcmd_print_break (0,0) >]
let int n = str (string_of_int n)
let real r = str (string_of_float r)
let bool b = str (string_of_bool b)
-
-(* In new syntax only double quote char is escaped by repeating it *)
-let rec escape_string s =
- let rec escape_at s i =
- if i<0 then s
- else if s.[i] == '"' then
- let s' = String.sub s 0 i^"\""^String.sub s i (String.length s - i) in
- escape_at s' (i-1)
- else escape_at s (i-1) in
- escape_at s (String.length s - 1)
-
-let qstring s = str ("\""^escape_string s^"\"")
-let qs = qstring
+let strbrk s =
+ let rec aux p n =
+ 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) >]
+ else aux p (n+1)
+ else if p=n then [< >] else [< str (String.sub s p (n-p)) >]
+ in aux 0 0
+
+let ismt s = try let _ = Stream.empty s in true with Stream.Failure -> false
(* boxing commands *)
let h n s = [< 'Ppcmd_box(Pp_hbox n,s) >]
@@ -161,6 +160,41 @@ let tclose () = [< 'Ppcmd_close_tbox >]
let (++) = Stream.iapp
+(* In new syntax only double quote char is escaped by repeating it *)
+let rec escape_string s =
+ let rec escape_at s i =
+ if i<0 then s
+ else if s.[i] == '"' then
+ let s' = String.sub s 0 i^"\""^String.sub s i (String.length s - i) in
+ escape_at s' (i-1)
+ else escape_at s (i-1) in
+ escape_at s (String.length s - 1)
+
+let qstring s = str ("\""^escape_string s^"\"")
+let qs = qstring
+let quote s = h 0 (str "\"" ++ s ++ str "\"")
+
+let rec xmlescape ppcmd =
+ let rec escape what withwhat (len, str) =
+ try
+ let pos = String.index str what in
+ let (tlen, tail) =
+ escape what withwhat ((len - pos - 1),
+ (String.sub str (pos + 1) (len - pos - 1)))
+ in
+ (pos + tlen + String.length withwhat, String.sub str 0 pos ^ withwhat ^ tail)
+ with Not_found -> (len, str)
+ in
+ match ppcmd with
+ | Ppcmd_print (len, str) ->
+ Ppcmd_print (escape '"' "&quot;"
+ (escape '<' "&lt;" (escape '&' "&amp;" (len, str))))
+ (* In XML we always print whole content so we can npeek the whole stream *)
+ | Ppcmd_box (x, str) -> Ppcmd_box (x, Stream.of_list
+ (List.map xmlescape (Stream.npeek max_int str)))
+ | x -> x
+
+
(* This flag tells if the last printed comment ends with a newline, to
avoid empty lines *)
let com_eol = ref false
@@ -242,7 +276,7 @@ let pp_dirs ft =
(* pretty print on stdout and stderr *)
let pp_std_dirs = pp_dirs !std_ft
-let pp_err_dirs = pp_dirs err_ft
+let pp_err_dirs = pp_dirs !err_ft
let ppcmds x = Ppdir_ppcmds x
@@ -251,11 +285,13 @@ let emacs_warning_start_string = String.make 1 (Char.chr 254)
let emacs_warning_end_string = String.make 1 (Char.chr 255)
let warnstart() =
- if not !print_emacs then str "" else str emacs_warning_start_string
+ if not !print_emacs then mt() else str emacs_warning_start_string
let warnend() =
- if not !print_emacs then str "" else str emacs_warning_end_string
-
+ if not !print_emacs then mt() else str emacs_warning_end_string
+
+let warnbody strm =
+ [< warnstart() ; hov 0 (str "Warning: " ++ strm) ; warnend() >]
(* pretty printing functions WITHOUT FLUSH *)
let pp_with ft strm =
@@ -264,15 +300,17 @@ let pp_with ft strm =
let ppnl_with ft strm =
pp_dirs ft [< 'Ppdir_ppcmds [< strm ; 'Ppcmd_force_newline >] >]
-let warning_with ft string =
- ppnl_with ft [< warnstart() ; str "Warning: " ; str string ; warnend() >]
+let default_warn_with ft strm = ppnl_with ft (warnbody strm)
+
+let pp_warn_with = ref default_warn_with
-let warn_with ft pps =
- ppnl_with ft [< warnstart() ; str "Warning: " ; pps ; warnend() >]
+let set_warning_function pp_warn = pp_warn_with := pp_warn
-let pp_flush_with ft =
- Format.pp_print_flush ft
+let warn_with ft strm = !pp_warn_with ft strm
+let warning_with ft string = warn_with ft (str string)
+
+let pp_flush_with ft = Format.pp_print_flush ft
(* pretty printing functions WITH FLUSH *)
let msg_with ft strm =
@@ -281,25 +319,23 @@ let msg_with ft strm =
let msgnl_with ft strm =
pp_dirs ft [< 'Ppdir_ppcmds strm ; 'Ppdir_print_newline >]
-let msg_warning_with ft strm=
- pp_dirs ft [< 'Ppdir_ppcmds [< warnstart() ; str "Warning: "; strm ; warnend() >];
- 'Ppdir_print_newline >]
-
+let msg_warning_with ft strm =
+ msgnl_with ft (warnbody strm)
(* pretty printing functions WITHOUT FLUSH *)
-let pp x = pp_with !std_ft x
+let pp x = pp_with !std_ft x
let ppnl x = ppnl_with !std_ft x
-let pperr = pp_with err_ft
-let pperrnl = ppnl_with err_ft
-let message s = ppnl (str s)
-let warning x = warning_with err_ft x
-let warn x = warn_with err_ft x
+let pperr x = pp_with !err_ft x
+let pperrnl x = ppnl_with !err_ft x
+let message s = ppnl (str s)
+let warning x = warning_with !err_ft x
+let warn x = warn_with !err_ft x
let pp_flush x = Format.pp_print_flush !std_ft x
let flush_all() = flush stderr; flush stdout; pp_flush()
(* pretty printing functions WITH FLUSH *)
let msg x = msg_with !std_ft x
let msgnl x = msgnl_with !std_ft x
-let msgerr = msg_with err_ft
-let msgerrnl = msgnl_with err_ft
-let msg_warning x = msg_warning_with err_ft x
+let msgerr x = msg_with !err_ft x
+let msgerrnl x = msgnl_with !err_ft x
+let msg_warning x = msg_warning_with !err_ft x
diff --git a/lib/pp.mli b/lib/pp.mli
index e240fd2d..85b8345d 100644
--- a/lib/pp.mli
+++ b/lib/pp.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: pp.mli 8748 2006-04-27 16:01:26Z courtieu $ i*)
+(*i $Id: pp.mli 10803 2008-04-16 09:30:05Z cek $ i*)
(*i*)
open Pp_control
@@ -16,6 +16,7 @@ open Pp_control
chars inserted at some places). This function should called once in
module [Options], that's all. *)
val make_pp_emacs:unit -> unit
+val make_pp_nonemacs:unit -> unit
(* Pretty-printers. *)
@@ -34,6 +35,7 @@ val fnl : unit -> std_ppcmds
val pifb : unit -> std_ppcmds
val ws : int -> std_ppcmds
val mt : unit -> std_ppcmds
+val ismt : std_ppcmds -> bool
val comment : int -> std_ppcmds
val comments : ((int * int) * string) list ref
@@ -52,6 +54,10 @@ val real : float -> std_ppcmds
val bool : bool -> std_ppcmds
val qstring : string -> std_ppcmds
val qs : string -> std_ppcmds
+val quote : std_ppcmds -> std_ppcmds
+val strbrk : string -> std_ppcmds
+
+val xmlescape : ppcmd -> ppcmd
(*s Boxing commands. *)
@@ -79,6 +85,8 @@ 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
+
(*s Pretty-printing functions \emph{with flush}. *)
val msg_with : Format.formatter -> std_ppcmds -> unit
diff --git a/lib/pp_control.ml b/lib/pp_control.ml
index 7632d736..7aa05975 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 5920 2004-07-16 20:01:26Z herbelin $ *)
+(* $Id: pp_control.ml 10917 2008-05-10 16:35:46Z herbelin $ *)
(* Parameters of pretty-printing *)
@@ -89,10 +89,11 @@ let with_output_to ch =
let std_ft = ref Format.std_formatter
let _ = set_dflt_gp !std_ft
-let err_ft = with_output_to stderr
+let err_ft = ref Format.err_formatter
+let _ = set_gp !err_ft deep_gp
-let deep_ft = with_output_to stdout
-let _ = set_gp deep_ft deep_gp
+let deep_ft = ref (with_output_to stdout)
+let _ = set_gp !deep_ft deep_gp
(* For parametrization through vernacular *)
let default = Format.pp_get_max_boxes !std_ft ()
diff --git a/lib/pp_control.mli b/lib/pp_control.mli
index 7e25e561..f245d942 100644
--- a/lib/pp_control.mli
+++ b/lib/pp_control.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: pp_control.mli 5920 2004-07-16 20:01:26Z herbelin $ i*)
+(*i $Id: pp_control.mli 10917 2008-05-10 16:35:46Z herbelin $ i*)
(* Parameters of pretty-printing. *)
@@ -37,8 +37,8 @@ val with_fp : 'a pp_formatter_params -> Format.formatter
val with_output_to : out_channel -> Format.formatter
val std_ft : Format.formatter ref
-val err_ft : Format.formatter
-val deep_ft : Format.formatter
+val err_ft : Format.formatter ref
+val deep_ft : Format.formatter ref
(*s For parametrization through vernacular. *)
diff --git a/lib/rtree.ml b/lib/rtree.ml
index ab689be1..4742a90d 100644
--- a/lib/rtree.ml
+++ b/lib/rtree.ml
@@ -6,11 +6,15 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: rtree.ml 8648 2006-03-18 15:37:14Z herbelin $ i*)
+(*i $Id: rtree.ml 10690 2008-03-18 13:30:04Z barras $ i*)
+
+open Util
(* Type of regular trees:
- Param denotes tree variables (like de Bruijn indices)
+ the first int is the depth of the occurrence, and the second int
+ is the index in the array of trees introduced at that depth
- Node denotes the usual tree node, labelled with 'a
- Rec(j,v1..vn) introduces infinite tree. It denotes
v(j+1) with parameters 0..n-1 replaced by
@@ -19,55 +23,87 @@
current Rec node (as usual in de Bruijn binding system)
*)
type 'a t =
- Param of int
+ Param of int * int
| Node of 'a * 'a t array
| Rec of int * 'a t array
(* Building trees *)
-let mk_param i = Param i
+let mk_rec_calls i = Array.init i (fun j -> Param(0,j))
let mk_node lab sons = Node (lab, sons)
-(* Given a vector of n bodies, builds the n mutual recursive trees.
- Recursive calls are made with parameters 0 to n-1. We check
- the bodies actually build something by checking it is not
- directly one of the parameters 0 to n-1. *)
-let mk_rec defs =
- Array.mapi
- (fun i d ->
- (match d with
- Param k when k < Array.length defs -> failwith "invalid rec call"
- | _ -> ());
- Rec(i,defs))
- defs
-
(* The usual lift operation *)
let rec lift_rtree_rec depth n = function
- Param i -> if i < depth then Param i else Param (i+n)
+ Param (i,j) as t -> if i < depth then t else Param (i+n,j)
| Node (l,sons) -> Node (l,Array.map (lift_rtree_rec depth n) sons)
| Rec(j,defs) ->
- Rec(j, Array.map (lift_rtree_rec (depth+Array.length defs) n) defs)
+ Rec(j, Array.map (lift_rtree_rec (depth+1) n) defs)
let lift n t = if n=0 then t else lift_rtree_rec 0 n t
(* The usual subst operation *)
let rec subst_rtree_rec depth sub = function
- Param i ->
- if i < depth then Param i
- else if i-depth < Array.length sub then lift depth sub.(i-depth)
- else Param (i-Array.length sub)
+ Param (i,j) as t ->
+ if i < depth then t
+ else if i-depth < Array.length sub then
+ lift depth sub.(i-depth).(j)
+ else Param (i-Array.length sub,j)
| Node (l,sons) -> Node (l,Array.map (subst_rtree_rec depth sub) sons)
| Rec(j,defs) ->
- Rec(j, Array.map (subst_rtree_rec (depth+Array.length defs) sub) defs)
+ Rec(j, Array.map (subst_rtree_rec (depth+1) sub) defs)
+
+let subst_rtree sub t = subst_rtree_rec 0 [|sub|] t
+
+(* To avoid looping, we must check that every body introduces a node
+ or a parameter *)
+let rec expand = function
+ | Rec(j,defs) ->
+ let sub = Array.init (Array.length defs) (fun i -> Rec(i,defs)) in
+ expand (subst_rtree sub defs.(j))
+ | t -> t
+
+(* Given a vector of n bodies, builds the n mutual recursive trees.
+ Recursive calls are made with parameters (0,0) to (0,n-1). We check
+ the bodies actually build something by checking it is not
+ directly one of the parameters of depth 0. Some care is taken to
+ accept definitions like rec X=Y and Y=f(X,Y) *)
+let mk_rec defs =
+ let rec check histo d =
+ match expand d with
+ Param(0,j) when List.mem j histo -> failwith "invalid rec call"
+ | Param(0,j) -> check (j::histo) defs.(j)
+ | _ -> () in
+ Array.mapi (fun i d -> check [i] d; Rec(i,defs)) defs
+(*
+let v(i,j) = lift i (mk_rec_calls(j+1)).(j);;
+let r = (mk_rec[|(mk_rec[|v(1,0)|]).(0)|]).(0);;
+let r = mk_rec[|v(0,1);v(1,0)|];;
+the last one should be accepted
+*)
+
+(* Tree destructors, expanding loops when necessary *)
+let dest_param t =
+ match expand t with
+ Param (i,j) -> (i,j)
+ | _ -> failwith "Rtree.dest_param"
+
+let dest_node t =
+ match expand t with
+ Node (l,sons) -> (l,sons)
+ | _ -> failwith "Rtree.dest_node"
+
+let is_node t =
+ match expand t with
+ Node _ -> true
+ | _ -> false
-let subst_rtree sub t = subst_rtree_rec 0 sub t
let rec map f t = match t with
- Param i -> Param i
+ Param(i,j) -> Param(i,j)
| Node (a,sons) -> Node (f a, Array.map (map f) sons)
| Rec(j,defs) -> Rec (j, Array.map (map f) defs)
let rec smartmap f t = match t with
- Param i -> t
+ Param _ -> t
| Node (a,sons) ->
let a'=f a and sons' = Util.array_smartmap (map f) sons in
if a'==a && sons'==sons then
@@ -81,43 +117,61 @@ let rec smartmap f t = match t with
else
Rec(j,defs')
-(* To avoid looping, we must check that every body introduces a node
- or a parameter *)
-let rec expand_rtree = function
- | Rec(j,defs) ->
- let sub = Array.init (Array.length defs) (fun i -> Rec(i,defs)) in
- expand_rtree (subst_rtree sub defs.(j))
- | t -> t
-
-(* Tree destructors, expanding loops when necessary *)
-let dest_param t =
- match expand_rtree t with
- Param i -> i
- | _ -> failwith "dest_param"
-
-let dest_node t =
- match expand_rtree t with
- Node (l,sons) -> (l,sons)
- | _ -> failwith "dest_node"
-
-(* Tests if a given tree is infinite or not. It proceeds *)
-let rec is_infinite = function
- Param i -> i = (-1)
- | Node(_,sons) -> Util.array_exists is_infinite sons
- | Rec(j,defs) ->
- let newdefs =
- Array.mapi (fun i def -> if i=j then Param (-1) else def) defs in
- let sub =
- Array.init (Array.length defs)
- (fun i -> if i=j then Param (-1) else Rec(i,newdefs)) in
- is_infinite (subst_rtree sub defs.(j))
+(* Fixpoint operator on trees:
+ f is the body of the fixpoint. Arguments passed to f are:
+ - a boolean telling if the subtree has already been seen
+ - the current subtree
+ - a function to make recursive calls on subtrees
+ *)
+let fold f t =
+ let rec fold histo t =
+ let seen = List.mem t histo in
+ let nhisto = if not seen then t::histo else histo in
+ f seen (expand t) (fold nhisto) in
+ fold [] t
+
+
+(* Tests if a given tree is infinite, i.e. has an branch of infinte length. *)
+let is_infinite t = fold
+ (fun seen t is_inf ->
+ seen ||
+ (match t with
+ Node(_,v) -> array_exists is_inf v
+ | Param _ -> false
+ | _ -> assert false))
+ t
+
+let fold2 f t x =
+ let rec fold histo t x =
+ let seen = List.mem (t,x) histo in
+ let nhisto = if not seen then (t,x)::histo else histo in
+ f seen (expand t) x (fold nhisto) in
+ fold [] t x
+
+let compare_rtree f = fold2
+ (fun seen t1 t2 cmp ->
+ seen ||
+ let b = f t1 t2 in
+ if b < 0 then false
+ else if b > 0 then true
+ else match expand t1, expand t2 with
+ Node(_,v1), Node(_,v2) when Array.length v1 = Array.length v2 ->
+ array_for_all2 cmp v1 v2
+ | _ -> false)
+
+let eq_rtree cmp t1 t2 =
+ t1 == t2 || t1=t2 ||
+ compare_rtree
+ (fun t1 t2 ->
+ if cmp (fst(dest_node t1)) (fst(dest_node t2)) then 0
+ else (-1)) t1 t2
(* Pretty-print a tree (not so pretty) *)
open Pp
let rec pp_tree prl t =
match t with
- Param k -> str"#"++int k
+ Param (i,j) -> str"#"++int i++str","++int j
| Node(lab,[||]) -> hov 2 (str"("++prl lab++str")")
| Node(lab,v) ->
hov 2 (str"("++prl lab++str","++brk(1,0)++
diff --git a/lib/rtree.mli b/lib/rtree.mli
index 7be96652..b61e6965 100644
--- a/lib/rtree.mli
+++ b/lib/rtree.mli
@@ -6,35 +6,74 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: rtree.mli 7493 2005-11-02 22:12:16Z mohring $ i*)
+(*i $Id: rtree.mli 10690 2008-03-18 13:30:04Z barras $ 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
(* Building trees *)
-(* build a recursive call *)
-val mk_param : int -> 'a t
+
(* build a node given a label and the vector of sons *)
val mk_node : 'a -> 'a t array -> 'a t
-(* build mutually dependent trees *)
+
+(* Build mutually recursive trees:
+ X_1 = f_1(X_1,..,X_n) ... X_n = f_n(X_1,..,X_n)
+ is obtained by the following pseudo-code
+ let vx = mk_rec_calls n in
+ let [|x_1;..;x_n|] =
+ mk_rec[|f_1(vx.(0),..,vx.(n-1);..;f_n(vx.(0),..,vx.(n-1))|]
+
+ First example: build rec X = a(X,Y) and Y = b(X,Y,Y)
+ let [|vx;vy|] = mk_rec_calls 2 in
+ let [|x;y|] = mk_rec [|mk_node a [|vx;vy|]; mk_node b [|vx;vy;vy|]|]
+
+ Another example: nested recursive trees rec Y = b(rec X = a(X,Y),Y,Y)
+ let [|vy|] = mk_rec_calls 1 in
+ let [|vx|] = mk_rec_calls 1 in
+ let [|x|] = mk_rec[|mk_node a [|vx;lift 1 vy|]
+ let [|y|] = mk_rec[|mk_node b [|x;vy;vy|]|]
+ (note the lift to avoid
+ *)
+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] *)
val lift : int -> 'a t -> 'a t
-val map : ('a -> 'b) -> 'a t -> 'b t
-
-(* [(smartmap f t) == t] if [(f a) ==a ] for all nodes *)
-val smartmap : ('a -> 'a) -> 'a t -> 'a t
-
+val is_node : 'a t -> bool
(* Destructors (recursive calls are expanded) *)
-val dest_param : 'a t -> int
val dest_node : 'a t -> 'a * 'a t array
+(* dest_param is not needed for closed trees (i.e. with no free variable) *)
+val dest_param : 'a t -> int * int
(* Tells if a tree has an infinite branch *)
val is_infinite : 'a t -> bool
+(* [compare_rtree f t1 t2] compares t1 t2 (top-down).
+ f is called on each node: if the result is negative then the
+ traversal ends on false, it is is positive then deeper nodes are
+ not examined, and the traversal continues on respective siblings,
+ and if it is 0, then the traversal continues on sons, pairwise.
+ In this latter case, if the nodes do not have the same number of
+ sons, then the traversal ends on false.
+ In case of loop, the traversal is successful and it resumes on
+ siblings.
+ *)
+val compare_rtree : ('a t -> 'b t -> int) -> 'a t -> 'b t -> bool
+
+val eq_rtree : ('a -> 'a -> bool) -> 'a t -> 'a t -> bool
+
+(* Iterators *)
+
+val map : ('a -> 'b) -> 'a t -> 'b t
+(* [(smartmap f t) == t] if [(f a) ==a ] for all nodes *)
+val smartmap : ('a -> 'a) -> 'a t -> 'a t
+val fold : (bool -> 'a t -> ('a t -> 'b) -> 'b) -> 'a t -> 'b
+val fold2 :
+ (bool -> 'a t -> 'b -> ('a t -> 'b -> 'c) -> 'c) -> 'a t -> 'b -> 'c
+
(* A rather simple minded pretty-printer *)
val pp_tree : ('a -> Pp.std_ppcmds) -> 'a t -> Pp.std_ppcmds
diff --git a/lib/system.ml b/lib/system.ml
index c92e87f1..aa71ddfa 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: system.ml 9397 2006-11-21 21:50:54Z herbelin $ *)
+(* $Id: system.ml 10437 2008-01-11 14:50:44Z bertot $ *)
open Pp
open Util
@@ -98,15 +98,31 @@ let all_subdirs ~unix_path:root =
List.rev !l
let where_in_path path filename =
- let rec search = function
+ let rec search acc = function
| lpe :: rem ->
let f = Filename.concat lpe filename in
- if Sys.file_exists f then (lpe,f) else search rem
- | [] ->
- raise Not_found
+ if Sys.file_exists f
+ then (search ((lpe,f)::acc) rem)
+ else search acc rem
+ | [] -> acc in
+ let rec check_and_warn cont acc l =
+ match l with
+ | [] -> if cont then assert false else raise Not_found
+ | [ (lpe, f) ] ->
+ if cont then begin
+ warning (acc ^ (string_of_physical_path lpe) ^ " ]");
+ warning ("Loading " ^ f)
+ end;
+ (lpe, f)
+ | (lpe, f) :: l' ->
+ if cont then
+ check_and_warn true (acc ^ (string_of_physical_path lpe) ^ "; ") l'
+ else
+ check_and_warn true
+ (filename ^ " has been found in [ " ^ (string_of_physical_path lpe) ^ "; ") l'
in
- search path
-
+ check_and_warn false "" (search [] path)
+
let find_file_in_path paths filename =
if not (Filename.is_implicit filename) then
let root = Filename.dirname filename in
@@ -199,7 +215,7 @@ let connect writefun readfun com =
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 [||] ch_to' ch_from' Unix.stdout
+ try Unix.create_process com [|com|] ch_to' ch_from' Unix.stdout
with Unix.Unix_error (err,_,_) ->
close_in ch_to_in; close_in ch_from_in; close_out ch_from_out;
unlink tmp_from; unlink tmp_to;
diff --git a/lib/system.mli b/lib/system.mli
index a58308a8..6d535464 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 9397 2006-11-21 21:50:54Z herbelin $ i*)
+(*i $Id: system.mli 9398 2006-11-21 21:51:18Z herbelin $ 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
diff --git a/lib/util.ml b/lib/util.ml
index 16d73430..9fa92f94 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(***********************************************************************)
-(* $Id: util.ml 10185 2007-10-06 18:05:13Z herbelin $ *)
+(* $Id: util.ml 11083 2008-06-09 22:08:14Z herbelin $ *)
open Pp
@@ -26,19 +26,27 @@ type loc = Compat.loc
let dummy_loc = Compat.dummy_loc
let unloc = Compat.unloc
let make_loc = Compat.make_loc
+let join_loc = Compat.join_loc
(* raising located exceptions *)
type 'a located = loc * 'a
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 join_loc = Compat.join_loc
+
+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
associated to the location of the error, and the error itself. *)
exception Error_in_file of string * (bool * string * loc) * exn
+(* Mapping under pairs *)
+
+let on_fst f (a,b) = (f a,b)
+let on_snd f (a,b) = (a,f b)
+
(* Projections from triplets *)
let pi1 (a,_,_) = a
@@ -47,15 +55,8 @@ let pi3 (_,_,a) = a
(* Characters *)
-let is_letter c =
- (c >= 'a' && c <= 'z') or
- (c >= 'A' && c <= 'Z') or
- (c >= '\248' && c <= '\255') or
- (c >= '\192' && c <= '\214') or
- (c >= '\216' && c <= '\246')
-
+let is_letter c = (c >= 'a' && c <= 'z') or (c >= 'A' && c <= 'Z')
let is_digit c = (c >= '0' && c <= '9')
-
let is_ident_tail c =
is_letter c or is_digit c or c = '\'' or c = '_'
@@ -99,6 +100,10 @@ let string_string_contains ~where ~what =
let plural n s = if n>1 then s^"s" else s
+let ordinal n =
+ let s = match n mod 10 with 1 -> "st" | 2 -> "nd" | 3 -> "rd" | _ -> "th" in
+ string_of_int n ^ s
+
(* string parsing *)
let parse_loadpath s =
@@ -119,9 +124,329 @@ module Stringset = Set.Make(struct type t = string let compare = compare end)
module Stringmap = Map.Make(struct type t = string let compare = compare end)
-(* Lists *)
+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 <= 0x299F -> 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 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
-let list_add_set x l = if List.mem x l then l else x::l
+exception End_of_input
+
+let utf8_of_unicode n =
+ 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
+ begin
+ s.[0] <- Char.chr (192 + n / 64);
+ s
+ end
+ else if n < 65536 then
+ let s = String.make 3 (Char.chr (128 + n mod 64)) in
+ begin
+ s.[1] <- Char.chr (128 + (n / 64) mod 64);
+ s.[0] <- Char.chr (224 + n / 4096);
+ s
+ end
+ else
+ let s = String.make 4 (Char.chr (128 + n mod 64)) in
+ 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
+ end
+
+let next_utf8 s i =
+ let err () = invalid_arg "utf8" in
+ let l = String.length s - i in
+ if l = 0 then raise End_of_input
+ else let a = Char.code s.[i] in if a <= 0x7F then
+ 1, a
+ else if a land 0x40 = 0 or l = 1 then err ()
+ else let b = Char.code s.[i+1] in if b land 0xC0 <> 0x80 then err ()
+ else if a land 0x20 = 0 then
+ 2, (a land 0x1F) lsl 6 + (b land 0x3F)
+ else if l = 2 then err ()
+ else let c = Char.code s.[i+2] in if c land 0xC0 <> 0x80 then err ()
+ else if a land 0x10 = 0 then
+ 3, (a land 0x0F) lsl 12 + (b land 0x3F) lsl 6 + (c land 0x3F)
+ else if l = 3 then err ()
+ else let d = Char.code s.[i+3] in if d land 0xC0 <> 0x80 then err ()
+ else if a land 0x08 = 0 then
+ 4, (a land 0x07) lsl 18 + (b land 0x3F) lsl 12 +
+ (c land 0x3F) lsl 6 + (d land 0x3F)
+ else err ()
+
+(* Check the well-formedness of an identifier *)
+
+let check_ident s =
+ let i = ref 0 in
+ if s <> ".." then try
+ let j, n = next_utf8 s 0 in
+ match classify_unicode n with
+ | UnicodeLetter ->
+ i := !i + j;
+ begin try
+ while true do
+ let j, n = next_utf8 s !i in
+ match classify_unicode n with
+ | UnicodeLetter | UnicodeIdentPart -> i := !i + j
+ | _ -> error
+ ("invalid character "^(String.sub s !i j)^" in identifier "^s)
+ done
+ with End_of_input -> () end
+ | _ -> error (s^": an identifier should start with a letter")
+ 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")
+
+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_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)
+
+(* Lists *)
let list_intersect l1 l2 =
List.filter (fun x -> List.mem x l2) l1
@@ -160,6 +485,11 @@ let list_tabulate f len =
in
tabrec 0
+let rec list_make n v =
+ if n = 0 then []
+ else if n < 0 then invalid_arg "list_make"
+ else v::list_make (n-1) v
+
let list_assign l n e =
let rec assrec stk = function
| ((h::t), 0) -> List.rev_append stk (e::t)
@@ -205,6 +535,14 @@ let list_map3 f l1 l2 l3 =
in
map (l1,l2,l3)
+let list_map4 f l1 l2 l3 l4 =
+ let rec map = function
+ | ([], [], [], []) -> []
+ | ((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
+ map (l1,l2,l3,l4)
+
let list_index x =
let rec index_x n = function
| y::l -> if x = y then n else index_x (succ n) l
@@ -212,6 +550,8 @@ let list_index x =
in
index_x 1
+let list_index0 x l = list_index x l - 1
+
let list_unique_index x =
let rec index_x n = function
| y::l ->
@@ -222,6 +562,13 @@ let list_unique_index x =
| [] -> 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
+ it_list_f (List.length l + i) l
+
let list_fold_left_i f =
let rec it_list_f i a = function
| [] -> a
@@ -247,6 +594,14 @@ let rec list_fold_right_and_left f l hd =
| a::l -> let hd = aux (a::tl) l in f hd a tl
in aux [] l
+let list_iter3 f l1 l2 l3 =
+ let rec iter = function
+ | ([], [], []) -> ()
+ | ((h1::t1), (h2::t2), (h3::t3)) -> f h1 h2 h3; iter (t1,t2,t3)
+ | (_, _, _) -> invalid_arg "map3"
+ 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 =
@@ -265,6 +620,8 @@ let rec list_remove_first a = function
| b::l -> b::list_remove_first a l
| [] -> raise Not_found
+let list_add_set x l = if List.mem x l then l else x::l
+
let list_eq_set l1 l2 =
let rec aux l1 = function
| [] -> l1 = []
@@ -300,14 +657,46 @@ let list_try_find f =
try_find_f
let list_uniquize l =
+ let visited = Hashtbl.create 23 in
let rec aux acc = function
- | [] -> List.rev acc
- | h::t -> if List.mem h acc then aux acc t else aux (h::acc) t
+ | h::t -> if Hashtbl.mem visited h then aux acc t else
+ begin
+ Hashtbl.add visited h h;
+ aux (h::acc) t
+ end
+ | [] -> List.rev acc
in aux [] l
-let rec list_distinct = function
- | h::t -> (not (List.mem h t)) && list_distinct t
- | _ -> true
+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
+ begin
+ Hashtbl.add visited h h;
+ loop t
+ end
+ | [] -> true
+ in loop l
+
+let rec list_merge_uniq cmp l1 l2 =
+ match l1, l2 with
+ | [], l2 -> l2
+ | l1, [] -> l1
+ | h1 :: t1, h2 :: t2 ->
+ let c = cmp h1 h2 in
+ if c = 0
+ then h1 :: list_merge_uniq cmp t1 t2
+ else if c <= 0
+ then h1 :: list_merge_uniq cmp t1 l2
+ else h2 :: list_merge_uniq cmp l1 t2
+
+let rec list_duplicates = function
+ | [] -> []
+ | x::l ->
+ let l' = list_duplicates l in
+ if List.mem x l then list_add_set x l' else l'
let rec list_filter2 f = function
| [], [] as p -> p
@@ -316,6 +705,12 @@ let rec list_filter2 f = function
if f d l then d::dp', l::lp' else p
| _ -> invalid_arg "list_filter2"
+let rec list_map_filter f = function
+ | [] -> []
+ | x::l ->
+ let l' = list_map_filter f l in
+ match f x with None -> l' | Some y -> y::l'
+
let list_subset l1 l2 =
let t2 = Hashtbl.create 151 in
List.iter (fun x -> Hashtbl.add t2 x ()) l2;
@@ -338,6 +733,14 @@ let rec list_split3 = function
| (x,y,z)::l ->
let (rx, ry, rz) = list_split3 l in (x::rx, y::ry, z::rz)
+let rec list_insert_in_class f a = function
+ | [] -> [[a]]
+ | (b::_ as l)::classes when f a b -> (a::l)::classes
+ | l::classes -> l :: list_insert_in_class f a classes
+
+let list_partition_by f l =
+ List.fold_right (list_insert_in_class f) l []
+
let list_firstn n l =
let rec aux acc = function
| (0, l) -> List.rev acc
@@ -363,6 +766,9 @@ let rec list_skipn n l = match n,l with
| _, [] -> failwith "list_fromn"
| n, _::l -> list_skipn (pred n) l
+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 rec prefrec = function
| (h1::t1, h2::t2) -> h1 = h2 && prefrec (t1,t2)
@@ -384,6 +790,7 @@ let list_drop_prefix p l =
| None -> l
let list_map_append f l = List.flatten (List.map f l)
+let list_join_map = list_map_append (* Alias *)
let list_map_append2 f l1 l2 = List.flatten (List.map2 f l1 l2)
@@ -394,8 +801,6 @@ let list_share_tails l1 l2 =
in
shr_rev [] (List.rev l1, List.rev l2)
-let list_join_map f l = List.flatten (List.map f l)
-
let rec list_fold_map f e = function
| [] -> (e,[])
| h::t ->
@@ -419,6 +824,35 @@ let list_fold_map' f l e =
let list_map_assoc f = List.map (fun (x,a) -> (x,f a))
+(* Specification:
+ - =p= is set equality (double inclusion)
+ - f such that \forall l acc, (f l acc) =p= append (f l []) acc
+ - let g = fun x -> f x [] in
+ - union_map f l acc =p= append (flatten (map g l)) acc
+ *)
+let list_union_map f l acc =
+ List.fold_left
+ (fun x y -> f y x)
+ acc
+ l
+
+(* 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 =
+ list_map_append (fun x -> List.map (op x) l2) l1
+
+(* [list_cartesians] is an n-ary cartesian product: it iterates
+ [list_cartesian] over a list of lists. *)
+
+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]] *)
+
+let list_combinations l = list_cartesians (fun x l -> x::l) [] l
+
(* Arrays *)
let array_exists f v =
@@ -645,6 +1079,11 @@ let array_map_left_pair f a g b =
r, s
end
+let array_iter2 f v1 v2 =
+ let n = Array.length v1 in
+ if Array.length v2 <> n then invalid_arg "array_iter2"
+ else for i = 0 to n - 1 do f v1.(i) v2.(i) done
+
let pure_functional = false
let array_fold_map' f v e =
@@ -659,6 +1098,11 @@ else
let v' = Array.map (fun x -> let (y,e) = f x !e' in e' := e; y) v in
(v',!e')
+let array_fold_map f e v =
+ let e' = ref e in
+ let v' = Array.map (fun x -> let (e,y) = f !e' x in e' := e; y) v in
+ (!e',v')
+
let array_fold_map2' f v1 v2 e =
let e' = ref e in
let v' =
@@ -677,6 +1121,12 @@ let array_distinct v =
with Exit ->
false
+let array_union_map f a acc =
+ Array.fold_left
+ (fun x y -> f y x)
+ acc
+ a
+
(* Matrices *)
let matrix_transpose mat =
@@ -723,44 +1173,6 @@ let interval n m =
in
interval_n ([],m)
-let in_some x = Some x
-
-let out_some = function
- | Some x -> x
- | None -> failwith "out_some"
-
-let option_map f = function
- | None -> None
- | Some x -> Some (f x)
-
-let option_cons a l = match a with
- | Some x -> x::l
- | None -> l
-
-let option_fold_left2 f e a b = match (a,b) with
- | Some x, Some y -> f e x y
- | _ -> e
-
-let option_fold_left f e a = match a with
- | Some x -> f e x
- | _ -> e
-
-let option_fold_right f a e = match a with
- | Some x -> f x e
- | _ -> e
-
-let option_compare f a b = match (a,b) with
- | None, None -> true
- | Some a', Some b' -> f a' b'
- | _ -> failwith "option_compare"
-
-let option_iter f = function
- | None -> ()
- | Some x -> f x
-
-let option_smartmap f a = match a with
- | None -> a
- | Some x -> let x' = f x in if x'==x then a else Some x'
let map_succeed f =
let rec map_f = function
@@ -780,15 +1192,21 @@ let pr_semicolon () = str ";" ++ spc ()
let pr_bar () = str "|" ++ spc ()
let pr_arg pr x = spc () ++ pr x
let pr_opt pr = function None -> mt () | Some x -> pr_arg pr x
+let pr_opt_no_spc pr = function None -> mt () | Some x -> pr x
-let pr_ord n =
- let suff = match n mod 10 with 1 -> "st" | 2 -> "nd" | _ -> "th" in
- int n ++ str suff
+let nth n = str (ordinal n)
let rec prlist elem l = match l with
| [] -> mt ()
| h::t -> Stream.lapp (fun () -> elem h) (prlist elem t)
+(* unlike all other functions below, [prlist] works lazily.
+ if a strict behavior is needed, use [prlist_strict] instead. *)
+
+let rec prlist_strict elem l = match l with
+ | [] -> mt ()
+ | h::t -> (elem h)++(prlist_strict elem t)
+
let rec prlist_with_sep sep elem l = match l with
| [] -> mt ()
| [h] -> elem h
@@ -821,6 +1239,8 @@ let prvect_with_sep sep elem v =
let n = Array.length v in
if n = 0 then mt () else pr (n - 1)
+let prvect elem v = prvect_with_sep mt elem v
+
let surround p = hov 1 (str"(" ++ p ++ str")")
(*s Size of ocaml values. *)
diff --git a/lib/util.mli b/lib/util.mli
index cc44a677..7807bbbd 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 9766 2007-04-13 13:26:28Z herbelin $ i*)
+(*i $Id: util.mli 11083 2008-06-09 22:08:14Z herbelin $ i*)
(*i*)
open Pp
@@ -43,6 +43,8 @@ val anomaly_loc : loc * string * std_ppcmds -> 'a
val user_err_loc : loc * string * std_ppcmds -> 'a
val invalid_arg_loc : loc * string -> 'a
val join_loc : loc -> loc -> loc
+val located_fold_left : ('a -> 'b -> 'a) -> 'a -> 'b located -> 'a
+val located_iter2 : ('a -> 'b -> unit) -> 'a located -> 'b located -> unit
(* Like [Exc_located], but specifies the outermost file read, the
input buffer associated to the location of the error (or the module name
@@ -50,6 +52,11 @@ val join_loc : loc -> loc -> loc
exception Error_in_file of string * (bool * string * loc) * exn
+(* Mapping under pairs *)
+
+val on_fst : ('a -> 'b) -> 'a * 'c -> 'b * 'c
+val on_snd : ('a -> 'b) -> 'c * 'a -> 'c * 'b
+
(*s Projections from triplets *)
val pi1 : 'a * 'b * 'c -> 'a
@@ -69,12 +76,21 @@ val implode : string list -> string
val string_index_from : string -> int -> string -> int
val string_string_contains : where:string -> what:string -> bool
val plural : int -> string -> string
+val ordinal : int -> string
val parse_loadpath : string -> string list
module Stringset : Set.S with type elt = string
module Stringmap : Map.S with type key = string
+type utf8_status = UnicodeLetter | UnicodeIdentPart | UnicodeSymbol
+
+exception UnsupportedUtf8
+
+val classify_unicode : int -> utf8_status
+val check_ident : string -> unit
+val lowercase_first_char_utf8 : string -> string
+
(*s Lists. *)
val list_add_set : 'a -> 'a list -> 'a list
@@ -87,10 +103,12 @@ val list_subtractq : 'a list -> 'a list -> 'a list
val list_chop : int -> 'a list -> 'a list * 'a list
(* [list_tabulate f n] builds [[f 0; ...; f (n-1)]] *)
val list_tabulate : (int -> 'a) -> int -> 'a list
+val list_make : int -> 'a -> 'a list
val list_assign : 'a list -> int -> 'a -> 'a list
val list_distinct : 'a list -> bool
+val list_duplicates : 'a list -> 'a list
val list_filter2 : ('a -> 'b -> bool) -> 'a list * 'b list -> 'a list * 'b list
-
+val list_map_filter : ('a -> 'b option) -> 'a list -> 'b list
(* [list_smartmap f [a1...an] = List.map f [a1...an]] but if for all i
[ f ai == ai], then [list_smartmap f l==l] *)
val list_smartmap : ('a -> 'a) -> 'a list -> 'a list
@@ -100,10 +118,17 @@ 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
+(* [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
+(* [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
val list_iter_i : (int -> 'a -> unit) -> 'a list -> unit
+val list_fold_right_i : (int -> 'a -> 'b -> 'b) -> int -> 'a list -> 'b -> 'b
val list_fold_left_i : (int -> 'a -> 'b -> 'a) -> int -> 'a -> 'b list -> 'a
val list_fold_right_and_left :
('a -> 'b -> 'b list -> 'a) -> 'b list -> 'a -> 'a
@@ -116,26 +141,41 @@ val list_sep_last : 'a list -> 'a * 'a list
val list_try_find_i : (int -> 'a -> 'b) -> int -> 'a list -> 'b
val list_try_find : ('a -> 'b) -> 'a list -> 'b
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_splitby : ('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_addn : int -> 'a -> 'a list -> 'a list
val list_prefix_of : 'a list -> 'a list -> bool
val list_drop_prefix : 'a list -> 'a list -> 'a list
(* [map_append f [x1; ...; xn]] returns [(f x1)@(f x2)@...@(f xn)] *)
val list_map_append : ('a -> 'b list) -> 'a list -> 'b list
+val list_join_map : ('a -> 'b list) -> 'a list -> 'b list
(* raises [Invalid_argument] if the two lists don't have the same length *)
val list_map_append2 : ('a -> 'b -> 'c list) -> 'a list -> 'b list -> 'c list
val list_share_tails : 'a list -> 'a list -> 'a list * 'a list * 'a list
-val list_join_map : ('a -> 'b list) -> 'a list -> 'b list
(* [list_fold_map f e_0 [l_1...l_n] = e_n,[k_1...k_n]]
where [(e_i,k_i)=f e_{i-1} l_i] *)
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]],
+ 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_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]] *)
+val list_combinations : 'a list list -> 'a list list
+
+val list_union_map : ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b
(*s Arrays. *)
@@ -174,10 +214,13 @@ val array_map3 :
val array_map_left : ('a -> 'b) -> 'a array -> 'b array
val array_map_left_pair : ('a -> 'b) -> 'a array -> ('c -> 'd) -> 'c array ->
'b array * 'd array
+val array_iter2 : ('a -> 'b -> unit) -> 'a array -> 'b array -> unit
val array_fold_map' : ('a -> 'c -> 'b * 'c) -> 'a array -> 'c -> 'b array * 'c
+val array_fold_map : ('a -> 'b -> 'a * 'c) -> 'a -> 'b array -> 'a * 'c array
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
(*s Matrices *)
@@ -205,17 +248,6 @@ val intmap_inv : 'a Intmap.t -> 'a -> int list
val interval : int -> int -> int list
-val in_some : 'a -> 'a option
-val out_some : 'a option -> 'a
-val option_map : ('a -> 'b) -> 'a option -> 'b option
-val option_cons : 'a option -> 'a list -> 'a list
-val option_fold_right : ('a -> 'b -> 'b) -> 'a option -> 'b -> 'b
-val option_fold_left : ('a -> 'b -> 'a) -> 'a -> 'b option -> 'a
-val option_fold_left2 : ('a -> 'b -> 'c -> 'a) -> 'a -> 'b option ->
- 'c option -> 'a
-val option_iter : ('a -> unit) -> 'a option -> unit
-val option_compare : ('a -> 'b -> bool) -> 'a option -> 'b option -> bool
-val option_smartmap : ('a -> 'a) -> 'a option -> 'a option
(* In [map_succeed f l] an element [a] is removed if [f a] raises *)
(* [Failure _] otherwise behaves as [List.map f l] *)
@@ -231,14 +263,19 @@ val pr_str : string -> std_ppcmds
val pr_coma : unit -> std_ppcmds
val pr_semicolon : unit -> std_ppcmds
val pr_bar : unit -> std_ppcmds
-val pr_ord : int -> std_ppcmds
val pr_arg : ('a -> std_ppcmds) -> 'a -> std_ppcmds
val pr_opt : ('a -> std_ppcmds) -> 'a option -> std_ppcmds
+val pr_opt_no_spc : ('a -> std_ppcmds) -> 'a option -> std_ppcmds
+val nth : int -> std_ppcmds
val prlist : ('a -> std_ppcmds) -> 'a list -> std_ppcmds
-val prvecti : (int -> 'a -> std_ppcmds) -> 'a array -> std_ppcmds
+(* unlike all other functions below, [prlist] works lazily.
+ if a strict behavior is needed, use [prlist_strict] instead. *)
+val prlist_strict : ('a -> std_ppcmds) -> 'a list -> std_ppcmds
val prlist_with_sep :
(unit -> std_ppcmds) -> ('b -> std_ppcmds) -> 'b list -> std_ppcmds
+val prvect : ('a -> std_ppcmds) -> 'a array -> std_ppcmds
+val prvecti : (int -> 'a -> std_ppcmds) -> 'a array -> std_ppcmds
val prvect_with_sep :
(unit -> std_ppcmds) -> ('b -> std_ppcmds) -> 'b array -> std_ppcmds
val pr_vertical_list : ('b -> std_ppcmds) -> 'b list -> std_ppcmds
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-26 21:42:33 +0000