summaryrefslogtreecommitdiff
path: root/lib
diff options
context:
space:
mode:
Diffstat (limited to 'lib')
-rw-r--r--lib/bigint.ml4
-rw-r--r--lib/bigint.mli10
-rw-r--r--lib/bstack.ml75
-rw-r--r--lib/bstack.mli22
-rw-r--r--lib/compat.ml4271
-rw-r--r--lib/dnet.ml4
-rw-r--r--lib/dnet.mli42
-rw-r--r--lib/dyn.ml4
-rw-r--r--lib/dyn.mli6
-rw-r--r--lib/edit.ml134
-rw-r--r--lib/edit.mli63
-rw-r--r--lib/envars.ml75
-rw-r--r--lib/envars.mli14
-rw-r--r--lib/errors.ml68
-rw-r--r--lib/errors.mli41
-rw-r--r--lib/explore.ml4
-rw-r--r--lib/explore.mli12
-rw-r--r--lib/flags.ml39
-rw-r--r--lib/flags.mli39
-rw-r--r--lib/fmap.mli2
-rw-r--r--lib/gmap.ml3
-rw-r--r--lib/gmap.mli8
-rw-r--r--lib/gmapl.ml4
-rw-r--r--lib/gmapl.mli6
-rw-r--r--lib/gset.ml242
-rw-r--r--lib/gset.mli34
-rw-r--r--lib/hashcons.ml4
-rw-r--r--lib/hashcons.mli8
-rw-r--r--lib/hashtbl_alt.ml109
-rw-r--r--lib/hashtbl_alt.mli41
-rw-r--r--lib/heap.ml4
-rw-r--r--lib/heap.mli28
-rw-r--r--lib/lib.mllib14
-rw-r--r--lib/option.ml4
-rw-r--r--lib/option.mli4
-rw-r--r--lib/pp.ml413
-rw-r--r--lib/pp.mli35
-rw-r--r--lib/pp_control.ml34
-rw-r--r--lib/pp_control.mli19
-rw-r--r--lib/predicate.ml2
-rw-r--r--lib/predicate.mli38
-rw-r--r--lib/profile.ml8
-rw-r--r--lib/profile.mli32
-rw-r--r--lib/refutpat.ml433
-rw-r--r--lib/rtree.ml4
-rw-r--r--lib/rtree.mli37
-rw-r--r--lib/segmenttree.ml1
-rw-r--r--lib/segmenttree.mli2
-rw-r--r--lib/store.ml61
-rw-r--r--lib/store.mli25
-rw-r--r--lib/system.ml75
-rw-r--r--lib/system.mli25
-rw-r--r--lib/tlm.ml63
-rw-r--r--lib/tlm.mli32
-rw-r--r--lib/tries.ml2
-rw-r--r--lib/tries.mli4
-rw-r--r--lib/unionfind.ml115
-rw-r--r--lib/unionfind.mli57
-rw-r--r--lib/util.ml133
-rw-r--r--lib/util.mli146
-rw-r--r--lib/xml_lexer.mli44
-rw-r--r--lib/xml_lexer.mll299
-rw-r--r--lib/xml_parser.ml238
-rw-r--r--lib/xml_parser.mli104
-rw-r--r--lib/xml_utils.ml223
-rw-r--r--lib/xml_utils.mli93
66 files changed, 2249 insertions, 1190 deletions
diff --git a/lib/bigint.ml b/lib/bigint.ml
index f3808f14..ed854d7a 100644
--- a/lib/bigint.ml
+++ b/lib/bigint.ml
@@ -1,13 +1,11 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: bigint.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
-
(*i*)
open Pp
(*i*)
diff --git a/lib/bigint.mli b/lib/bigint.mli
index 9a890570..92a97bdc 100644
--- a/lib/bigint.mli
+++ b/lib/bigint.mli
@@ -1,18 +1,14 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: bigint.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
-(*i*)
open Pp
-(*i*)
-(* Arbitrary large integer numbers *)
+(** Arbitrary large integer numbers *)
type bigint
@@ -23,7 +19,7 @@ val zero : bigint
val one : bigint
val two : bigint
-val div2_with_rest : bigint -> bigint * bool (* true=odd; false=even *)
+val div2_with_rest : bigint -> bigint * bool (** true=odd; false=even *)
val add_1 : bigint -> bigint
val sub_1 : bigint -> bigint
val mult_2 : bigint -> bigint
diff --git a/lib/bstack.ml b/lib/bstack.ml
deleted file mode 100644
index 3d549427..00000000
--- a/lib/bstack.ml
+++ /dev/null
@@ -1,75 +0,0 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
-
-(* $Id: bstack.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
-
-(* 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}
-
-(*
-let set_depth bs n = bs.depth <- n
-*)
-
-let incr_pos bs =
- bs.pos <- if bs.pos = Array.length bs.stack - 1 then 0 else bs.pos + 1
-
-let incr_size bs =
- if bs.size < Array.length bs.stack then bs.size <- bs.size + 1
-
-let decr_pos bs =
- bs.pos <- if bs.pos = 0 then Array.length bs.stack - 1 else bs.pos - 1
-
-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 copying what is at new pos *)
- bs.stack.(oldpos) <- bs.stack.(bs.pos)
- end
-
-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)))
-
-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.depth
-
-let size bs = bs.size
diff --git a/lib/bstack.mli b/lib/bstack.mli
deleted file mode 100644
index 39a5202a..00000000
--- a/lib/bstack.mli
+++ /dev/null
@@ -1,22 +0,0 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
-
-(*i $Id: bstack.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
-(* Bounded stacks. If the depth is [None], then there is no depth limit. *)
-
-type 'a t
-
-val create : int -> 'a -> 'a t
-val push : 'a t -> 'a -> unit
-val app_push : 'a t -> ('a -> 'a) -> unit
-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 096320ed..8d8483b4 100644
--- a/lib/compat.ml4
+++ b/lib/compat.ml4
@@ -1,79 +1,242 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i camlp4use: "pa_macro.cmo" i*)
+(** Compatibility file depending on ocaml/camlp4 version *)
-(* Compatibility file depending on ocaml version *)
+(** Locations *)
-IFDEF OCAML309 THEN DEFINE OCAML308 END
+IFDEF CAMLP5 THEN
+
+module Loc = struct
+ include Ploc
+ exception Exc_located = Exc
+ let ghost = dummy
+ let merge = encl
+end
+
+let make_loc = Loc.make_unlined
+let unloc loc = (Loc.first_pos loc, Loc.last_pos loc)
+
+ELSE
+
+module Loc = Camlp4.PreCast.Loc
+
+let make_loc (start,stop) =
+ Loc.of_tuple ("", 0, 0, start, 0, 0, stop, false)
+let unloc loc = (Loc.start_off loc, Loc.stop_off loc)
+
+END
+
+(** Misc module emulation *)
+
+IFDEF CAMLP5 THEN
+
+module PcamlSig = struct end
+
+ELSE
+
+module PcamlSig = Camlp4.Sig
+module Ast = Camlp4.PreCast.Ast
+module Pcaml = Camlp4.PreCast.Syntax
+module MLast = Ast
+module Token = struct exception Error of string end
+
+END
+
+
+(** Grammar auxiliary types *)
+
+IFDEF CAMLP5 THEN
+type gram_assoc = Gramext.g_assoc = NonA | RightA | LeftA
+type gram_position = Gramext.position =
+ | First
+ | Last
+ | Before of string
+ | After of string
+ | Like of string (** dont use it, not in camlp4 *)
+ | Level of string
+ELSE
+type gram_assoc = PcamlSig.Grammar.assoc = NonA | RightA | LeftA
+type gram_position = PcamlSig.Grammar.position =
+ | First
+ | Last
+ | Before of string
+ | After of string
+ | Level of string
+END
+
+
+(** Signature of Lexer *)
+
+IFDEF CAMLP5 THEN
+
+module type LexerSig = sig
+ include Grammar.GLexerType with type te = Tok.t
+ module Error : sig
+ type t
+ exception E of t
+ val to_string : t -> string
+ end
+end
+
+ELSE
+
+module type LexerSig =
+ Camlp4.Sig.Lexer with module Loc = Loc and type Token.t = Tok.t
+
+END
+
+(** Signature and implementation of grammars *)
IFDEF CAMLP5 THEN
-module M = struct
-type loc = Stdpp.location
-let dummy_loc = Stdpp.dummy_loc
-let make_loc = Stdpp.make_loc
-let unloc loc = Stdpp.first_pos loc, Stdpp.last_pos loc
-let join_loc loc1 loc2 =
- if loc1 = dummy_loc or loc2 = dummy_loc then dummy_loc
- else Stdpp.encl_loc loc1 loc2
-type token = string*string
-type lexer = token Token.glexer
+
+module type GrammarSig = sig
+ include Grammar.S with type te = Tok.t
+ type 'a entry = 'a Entry.e
+ type internal_entry = Tok.t Gramext.g_entry
+ type symbol = Tok.t Gramext.g_symbol
+ type action = Gramext.g_action
+ type production_rule = symbol list * action
+ type single_extend_statment =
+ string option * gram_assoc option * production_rule list
+ type extend_statment =
+ gram_position option * single_extend_statment list
+ val action : 'a -> action
+ val entry_create : string -> 'a entry
+ val entry_parse : 'a entry -> parsable -> 'a
+ val entry_print : 'a entry -> unit
+ val srules' : production_rule list -> symbol
+ val parse_tokens_after_filter : 'a entry -> Tok.t Stream.t -> 'a
end
-ELSE IFDEF OCAML308 THEN
-module M = struct
-type loc = Token.flocation
-let dummy_loc = Token.dummy_loc
-let make_loc loc = Token.make_loc loc
-let unloc (b,e) =
- let loc = (b.Lexing.pos_cnum,e.Lexing.pos_cnum) in
- (* Ensure that we unpack a char location that was encoded as a line-col
- location by make_loc *)
-(* Gram.Entry.parse may send bad loc in 3.08, see caml-bugs #2954
- assert (dummy_loc = (b,e) or make_loc loc = (b,e));
-*)
- loc
-let join_loc loc1 loc2 =
- if loc1 = dummy_loc or loc2 = dummy_loc then dummy_loc
- else (fst loc1, snd loc2)
-type token = Token.t
-type lexer = Token.lexer
+
+module GrammarMake (L:LexerSig) : GrammarSig = struct
+ include Grammar.GMake (L)
+ type 'a entry = 'a Entry.e
+ type internal_entry = Tok.t Gramext.g_entry
+ type symbol = Tok.t Gramext.g_symbol
+ type action = Gramext.g_action
+ type production_rule = symbol list * action
+ type single_extend_statment =
+ string option * gram_assoc option * production_rule list
+ type extend_statment =
+ gram_position option * single_extend_statment list
+ let action = Gramext.action
+ let entry_create = Entry.create
+ let entry_parse = Entry.parse
+IFDEF CAMLP5_6_02_1 THEN
+ let entry_print x = Entry.print !Pp_control.std_ft x
+ELSE
+ let entry_print = Entry.print
+END
+ let srules' = Gramext.srules
+ let parse_tokens_after_filter = Entry.parse_token
end
+
ELSE
-module M = struct
-type loc = int * int
-let dummy_loc = (0,0)
-let make_loc x = x
-let unloc x = x
-let join_loc loc1 loc2 =
- if loc1 = dummy_loc or loc2 = dummy_loc then dummy_loc
- else (fst loc1, snd loc2)
-type token = Token.t
-type lexer = Token.lexer
+
+module type GrammarSig = sig
+ include Camlp4.Sig.Grammar.Static
+ with module Loc = Loc and type Token.t = Tok.t
+ type 'a entry = 'a Entry.t
+ type action = Action.t
+ type parsable
+ val parsable : char Stream.t -> parsable
+ val action : 'a -> action
+ val entry_create : string -> 'a entry
+ val entry_parse : 'a entry -> parsable -> 'a
+ val entry_print : 'a entry -> unit
+ val srules' : production_rule list -> symbol
+end
+
+module GrammarMake (L:LexerSig) : GrammarSig = struct
+ include Camlp4.Struct.Grammar.Static.Make (L)
+ type 'a entry = 'a Entry.t
+ type action = Action.t
+ type parsable = char Stream.t
+ let parsable s = s
+ let action = Action.mk
+ let entry_create = Entry.mk
+ let entry_parse e s = parse e (*FIXME*)Loc.ghost s
+ let entry_print x = Entry.print !Pp_control.std_ft x
+ let srules' = srules (entry_create "dummy")
end
+
END
+
+
+(** Misc functional adjustments *)
+
+(** - The lexer produces streams made of pairs in camlp4 *)
+
+let get_tok = IFDEF CAMLP5 THEN fun x -> x ELSE fst END
+
+(** - Gram.extend is more currified in camlp5 than in camlp4 *)
+
+IFDEF CAMLP5 THEN
+let maybe_curry f x y = f (x,y)
+let maybe_uncurry f (x,y) = f x y
+ELSE
+let maybe_curry f = f
+let maybe_uncurry f = f
+END
+
+(** Compatibility with camlp5 strict mode *)
+IFDEF CAMLP5 THEN
+ IFDEF STRICT THEN
+ let vala x = Ploc.VaVal x
+ ELSE
+ let vala x = x
+ END
+ELSE
+ let vala x = x
END
-type loc = M.loc
-let dummy_loc = M.dummy_loc
-let make_loc = M.make_loc
-let unloc = M.unloc
-let join_loc = M.join_loc
-type token = M.token
-type lexer = M.lexer
+(** Fix a quotation difference in [str_item] *)
+
+let declare_str_items loc l =
+IFDEF CAMLP5 THEN
+ MLast.StDcl (loc, vala l) (* correspond to <:str_item< declare $list:l'$ end >> *)
+ELSE
+ Ast.stSem_of_list l
+END
-IFDEF CAMLP5_6_00 THEN
+(** Quotation difference for match clauses *)
-let slist0sep x y = Gramext.Slist0sep (x, y, false)
-let slist1sep x y = Gramext.Slist1sep (x, y, false)
+let default_patt loc =
+ (<:patt< _ >>, vala None, <:expr< failwith "Extension: cannot occur" >>)
+
+IFDEF CAMLP5 THEN
+
+let make_fun loc cl =
+ let l = cl @ [default_patt loc] in
+ MLast.ExFun (loc, vala l) (* correspond to <:expr< fun [ $list:l$ ] >> *)
ELSE
-let slist0sep x y = Gramext.Slist0sep (x, y)
-let slist1sep x y = Gramext.Slist1sep (x, y)
+let make_fun loc cl =
+ let mk_when = function
+ | Some w -> w
+ | None -> Ast.ExNil loc
+ in
+ let mk_clause (patt,optwhen,expr) =
+ (* correspond to <:match_case< ... when ... -> ... >> *)
+ Ast.McArr (loc, patt, mk_when optwhen, expr) in
+ let init = mk_clause (default_patt loc) in
+ let add_clause x acc = Ast.McOr (loc, mk_clause x, acc) in
+ let l = List.fold_right add_clause cl init in
+ Ast.ExFun (loc,l) (* correspond to <:expr< fun [ $l$ ] >> *)
+
+END
+
+(** Explicit antiquotation $anti:... $ *)
+IFDEF CAMLP5 THEN
+let expl_anti loc e = <:expr< $anti:e$ >>
+ELSE
+let expl_anti _loc e = e (* FIXME: understand someday if we can do better *)
END
diff --git a/lib/dnet.ml b/lib/dnet.ml
index fe20ecac..0b09a16a 100644
--- a/lib/dnet.ml
+++ b/lib/dnet.ml
@@ -1,13 +1,11 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \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 =
diff --git a/lib/dnet.mli b/lib/dnet.mli
index eba2220b..ba0229d2 100644
--- a/lib/dnet.mli
+++ b/lib/dnet.mli
@@ -1,14 +1,12 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \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
+(** 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
@@ -43,27 +41,27 @@
*)
-(* datatype you want to build a dnet on *)
+(** datatype you want to build a dnet on *)
module type Datatype =
sig
- (* parametric datatype. ['a] is morally the recursive argument *)
+ (** parametric datatype. ['a] is morally the recursive argument *)
type 'a t
- (* non-recursive mapping of subterms *)
+ (** 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 *)
+ (** 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 *)
+ (** comparison of constructors *)
val compare : unit t -> unit t -> int
- (* for each constructor, is it not-parametric on 'a? *)
+ (** 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 *)
+ (** [choose f w] applies f on ONE of the subterms of w *)
val choose : ('a -> 'b) -> 'a t -> 'b
end
@@ -71,19 +69,19 @@ module type S =
sig
type t
- (* provided identifier type *)
+ (** provided identifier type *)
type ident
- (* provided metavariable type *)
+ (** provided metavariable type *)
type meta
- (* provided parametrized datastructure *)
+ (** provided parametrized datastructure *)
type 'a structure
- (* returned sets of solutions *)
+ (** returned sets of solutions *)
module Idset : Set.S with type elt=ident
- (* a pattern is a term where each node can be a unification
+ (** a pattern is a term where each node can be a unification
variable *)
type 'a pattern =
| Term of 'a
@@ -93,13 +91,13 @@ sig
val empty : t
- (* [add t w i] adds a new association (w,i) in 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. *)
+ (** [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
+ (** [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).
@@ -107,15 +105,15 @@ sig
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
+ (** [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 *)
+ (** 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 *)
+ (** apply a function on each identifier and node of terms in a dnet *)
val map : (ident -> ident) -> (unit structure -> unit structure) -> t -> t
end
diff --git a/lib/dyn.ml b/lib/dyn.ml
index 2748422a..a0109b60 100644
--- a/lib/dyn.ml
+++ b/lib/dyn.ml
@@ -1,13 +1,11 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: dyn.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
-
open Util
(* Dynamics, programmed with DANGER !!! *)
diff --git a/lib/dyn.mli b/lib/dyn.mli
index 0d36dbef..577d17d5 100644
--- a/lib/dyn.mli
+++ b/lib/dyn.mli
@@ -1,14 +1,12 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: dyn.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
-(* Dynamics. Use with extreme care. Not for kids. *)
+(** Dynamics. Use with extreme care. Not for kids. *)
type t
diff --git a/lib/edit.ml b/lib/edit.ml
deleted file mode 100644
index 882303a6..00000000
--- a/lib/edit.ml
+++ /dev/null
@@ -1,134 +0,0 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
-
-(* $Id: edit.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
-
-open Pp
-open Util
-
-type ('a,'b,'c) t = {
- mutable focus : 'a option;
- mutable last_focused_stk : 'a list;
- buf : ('a, 'b Bstack.t * 'c) Hashtbl.t }
-
-let empty () = {
- focus = None;
- last_focused_stk = [];
- buf = Hashtbl.create 17 }
-
-let focus e nd =
- if not (Hashtbl.mem e.buf nd) then invalid_arg "Edit.focus";
- begin match e.focus with
- | Some foc when foc <> nd ->
- e.last_focused_stk <- foc::(list_except foc e.last_focused_stk);
- | _ -> ()
- end;
- e.focus <- Some nd
-
-let unfocus e =
- match e.focus with
- | None -> invalid_arg "Edit.unfocus"
- | Some foc ->
- begin
- 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
- | f::_ -> Some f
-
-let restore_last_focus e =
- match e.last_focused_stk with
- | [] -> ()
- | f::_ -> focus e f
-
-let focusedp e =
- match e.focus with
- | None -> false
- | _ -> true
-
-let read e =
- match e.focus with
- | None -> None
- | Some d ->
- let (bs,c) = Hashtbl.find e.buf d in
- Some(d,Bstack.top bs,c)
-
-let mutate e f =
- match e.focus with
- | None -> invalid_arg "Edit.mutate"
- | Some d ->
- let (bs,c) = Hashtbl.find e.buf d in
- Bstack.app_push bs (f c)
-
-let rev_mutate e f =
- match e.focus with
- | None -> invalid_arg "Edit.rev_mutate"
- | Some d ->
- let (bs,c) = Hashtbl.find e.buf d in
- Bstack.app_repl bs (f c)
-
-let undo e n =
- match e.focus with
- | None -> invalid_arg "Edit.undo"
- | Some d ->
- let (bs,_) = Hashtbl.find e.buf d in
- if n >= Bstack.size bs then
- errorlabstrm "Edit.undo" (str"Undo stack exhausted");
- repeat n Bstack.pop bs
-
-(* Return the depth of the focused proof of [e] stack, this is used to
- put informations in coq prompt (in emacs mode). *)
-let depth e =
- match e.focus with
- | None -> invalid_arg "Edit.depth"
- | Some d ->
- let (bs,_) = Hashtbl.find e.buf d in
- Bstack.depth bs
-
-(* Undo focused proof of [e] to reach depth [n] *)
-let undo_todepth e n =
- match e.focus with
- | 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 ->
- let (bs,_) = Hashtbl.find e.buf d in
- let ucnt = Bstack.depth bs - n in
- if ucnt >= Bstack.size bs then
- errorlabstrm "Edit.undo_todepth" (str"Undo stack would be exhausted");
- repeat ucnt Bstack.pop bs
-
-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 usize b in
- Hashtbl.add e.buf d (bs,c)
-
-let delete e d =
- if not(Hashtbl.mem e.buf d) then
- errorlabstrm "Edit.delete" (str"No such editor");
- Hashtbl.remove e.buf d;
- e.last_focused_stk <- (list_except d e.last_focused_stk);
- match e.focus with
- | Some d' -> if d = d' then (e.focus <- None ; (restore_last_focus e))
- | None -> ()
-
-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 <- [];
- Hashtbl.clear e.buf
diff --git a/lib/edit.mli b/lib/edit.mli
deleted file mode 100644
index d3558716..00000000
--- a/lib/edit.mli
+++ /dev/null
@@ -1,63 +0,0 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
-
-(*i $Id: edit.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
-(* The type of editors.
- * An editor is a finite map, ['a -> 'b], which knows how to apply
- * modification functions to the value in the range, and how to
- * focus on a member of the range.
- * It also supports the notion of a limited-depth undo, and that certain
- * modification actions do not push onto the undo stack, since they are
- * reversible. *)
-
-type ('a,'b,'c) t
-
-val empty : unit -> ('a,'b,'c) t
-
-(* sets the focus to the specified domain element *)
-val focus : ('a,'b,'c) t -> 'a -> unit
-
-(* unsets the focus which must not already be unfocused *)
-val unfocus : ('a,'b,'c) t -> unit
-
-(* gives the last focused element or [None] if none *)
-val last_focused : ('a,'b,'c) t -> 'a option
-
-(* are we focused ? *)
-val focusedp : ('a,'b,'c) t -> bool
-
-(* If we are focused, then return the current domain,range pair. *)
-val read : ('a,'b,'c) t -> ('a * 'b * 'c) option
-
-(* mutates the currently-focused range element, pushing its
- * old value onto the undo stack
- *)
-val mutate : ('a,'b,'c) t -> ('c -> 'b -> 'b) -> unit
-
-(* mutates the currently-focused range element, in place. *)
-val rev_mutate : ('a,'b,'c) t -> ('c -> 'b -> 'b) -> unit
-
-(* Pops the specified number of elements off of the undo stack, *
- reinstating the last popped element. The undo stack is independently
- managed for each range element. *)
-val undo : ('a,'b,'c) t -> int -> unit
-
-val create : ('a,'b,'c) t -> 'a * 'b * 'c * int -> unit
-val delete : ('a,'b,'c) t -> 'a -> unit
-
-val dom : ('a,'b,'c) t -> 'a list
-
-val clear : ('a,'b,'c) t -> unit
-
-(* [depth e] Returns the depth of the focused proof stack of [e], this
- is used to put informations in coq prompt (in emacs mode). *)
-val depth : ('a,'b,'c) t -> int
-
-(* [undo_todepth e n] Undoes focused proof of [e] to reach depth [n] *)
-val undo_todepth : ('a,'b,'c) t -> int -> unit
diff --git a/lib/envars.ml b/lib/envars.ml
index f764576d..e5c93803 100644
--- a/lib/envars.ml
+++ b/lib/envars.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -9,39 +9,75 @@
(* This file gathers environment variables needed by Coq to run (such
as coqlib) *)
-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 coqbin =
+ System.canonical_path_name (Filename.dirname Sys.executable_name)
+
+(* The following only makes sense when executables are running from
+ source tree (e.g. during build or in local mode). *)
+let coqroot = Filename.dirname coqbin
(* On win32, we add coqbin to the PATH at launch-time (this used to be
done in a .bat script). *)
let _ =
if Coq_config.arch = "win32" then
- Unix.putenv "PATH" (coqbin() ^ ";" ^ System.getenv_else "PATH" "")
+ Unix.putenv "PATH" (coqbin ^ ";" ^ System.getenv_else "PATH" "")
+
+let reldir instdir testfile oth =
+ let rpath = if Coq_config.local then [] else instdir in
+ let out = List.fold_left Filename.concat coqroot rpath in
+ if Sys.file_exists (Filename.concat out testfile) then out else oth ()
let guess_coqlib () =
let file = "states/initial.coq" in
- if Sys.file_exists (Filename.concat Coq_config.coqlib file)
- then Coq_config.coqlib
- 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
- (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"
+ reldir (if Coq_config.arch = "win32" then ["lib"] else ["lib";"coq"]) file
+ (fun () ->
+ let coqlib = match Coq_config.coqlib with
+ | Some coqlib -> coqlib
+ | None -> coqroot
+ 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 () =
if !Flags.coqlib_spec then !Flags.coqlib else
- (if !Flags.boot then Coq_config.coqsrc else guess_coqlib ())
+ (if !Flags.boot then coqroot else guess_coqlib ())
+
+let docdir () =
+ reldir (if Coq_config.arch = "win32" then ["doc"] else ["share";"doc";"coq"]) "html" (fun () -> Coq_config.docdir)
let path_to_list p =
let sep = if Sys.os_type = "Win32" then ';' else ':' in
Util.split_string_at sep p
+let xdg_data_home =
+ Filename.concat
+ (System.getenv_else "XDG_DATA_HOME" (Filename.concat System.home ".local/share"))
+ "coq"
+
+let xdg_config_home =
+ Filename.concat
+ (System.getenv_else "XDG_CONFIG_HOME" (Filename.concat System.home ".config"))
+ "coq"
+
+let xdg_data_dirs =
+ try
+ List.map (fun dir -> Filename.concat dir "coq") (path_to_list (Sys.getenv "XDG_DATA_DIRS"))
+ with Not_found -> "/usr/local/share/coq" :: "/usr/share/coq"
+ :: (match Coq_config.datadir with |None -> [] |Some datadir -> [datadir])
+
+let xdg_dirs =
+ let dirs = xdg_data_home :: xdg_data_dirs
+ in
+ List.rev (List.filter Sys.file_exists dirs)
+
+let coqpath =
+ try
+ let path = Sys.getenv "COQPATH" in
+ List.rev (List.filter Sys.file_exists (path_to_list path))
+ with Not_found -> []
+
let rec which l f =
match l with
| [] -> raise Not_found
@@ -74,11 +110,12 @@ let camllib () =
let _,res = System.run_command (fun x -> x) (fun _ -> ()) com in
Util.strip res
-(* TODO : essayer aussi camlbin *)
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
+ try guess_camlp4bin () with _ -> let cb = camlbin () in
+ if Sys.file_exists (Filename.concat cb Coq_config.camlp4) then cb
+ else Coq_config.camlp4bin
let camlp4lib () =
if !Flags.boot
diff --git a/lib/envars.mli b/lib/envars.mli
index 05357b32..0c80492f 100644
--- a/lib/envars.mli
+++ b/lib/envars.mli
@@ -1,13 +1,23 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
+(** This file gathers environment variables needed by Coq to run (such
+ as coqlib) *)
+
val coqlib : unit -> string
-val coqbin : unit -> string
+val docdir : unit -> string
+val coqbin : string
+val coqroot : string
+(* coqpath is stored in reverse order, since that is the order it
+ * gets added to the searc path *)
+val xdg_config_home : string
+val xdg_dirs : string list
+val coqpath : string list
val camlbin : unit -> string
val camlp4bin : unit -> string
diff --git a/lib/errors.ml b/lib/errors.ml
new file mode 100644
index 00000000..3b5e6770
--- /dev/null
+++ b/lib/errors.ml
@@ -0,0 +1,68 @@
+(***********************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* \VV/ *************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(***********************************************************************)
+
+open Pp
+
+(* spiwack: it might be reasonable to decide and move the declarations
+ of Anomaly and so on to this module so as not to depend on Util. *)
+
+let handle_stack = ref []
+
+exception Unhandled
+
+let register_handler h = handle_stack := h::!handle_stack
+
+(** [print_gen] is a general exception printer which tries successively
+ all the handlers of a list, and finally a [bottom] handler if all
+ others have failed *)
+
+let rec print_gen bottom stk e =
+ match stk with
+ | [] -> bottom e
+ | h::stk' ->
+ try h e
+ with
+ | Unhandled -> print_gen bottom stk' e
+ | e' -> print_gen bottom stk' e'
+
+(** Only anomalies should reach the bottom of the handler stack.
+ In usual situation, the [handle_stack] is treated as it if was always
+ non-empty with [print_anomaly] as its bottom handler. *)
+
+let where s =
+ if !Flags.debug then str ("in "^s^":") ++ spc () else mt ()
+
+let raw_anomaly e = match e with
+ | Util.Anomaly (s,pps) -> where s ++ pps ++ str "."
+ | Assert_failure _ | Match_failure _ -> str (Printexc.to_string e ^ ".")
+ | _ -> str ("Uncaught exception " ^ Printexc.to_string e ^ ".")
+
+let print_anomaly askreport e =
+ if askreport then
+ hov 0 (str "Anomaly: " ++ raw_anomaly e ++ spc () ++ str "Please report.")
+ else
+ hov 0 (raw_anomaly e)
+
+(** The standard exception printer *)
+let print e = print_gen (print_anomaly true) !handle_stack e
+
+(** Same as [print], except that the "Please report" part of an anomaly
+ isn't printed (used in Ltac debugging). *)
+let print_no_report e = print_gen (print_anomaly false) !handle_stack e
+
+(** Same as [print], except that anomalies are not printed but re-raised
+ (used for the Fail command) *)
+let print_no_anomaly e = print_gen (fun e -> raise e) !handle_stack e
+
+(** Predefined handlers **)
+
+let _ = register_handler begin function
+ | Util.UserError(s,pps) -> hov 0 (str "Error: " ++ where s ++ pps)
+ | _ -> raise Unhandled
+end
+
diff --git a/lib/errors.mli b/lib/errors.mli
new file mode 100644
index 00000000..eb7fde8e
--- /dev/null
+++ b/lib/errors.mli
@@ -0,0 +1,41 @@
+(***********************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* \VV/ *************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(***********************************************************************)
+
+(** This modules implements basic manipulations of errors for use
+ throughout Coq's code. *)
+
+(** [register_handler h] registers [h] as a handler.
+ When an expression is printed with [print e], it
+ goes through all registered handles (the most
+ recent first) until a handle deals with it.
+
+ Handles signal that they don't deal with some exception
+ by raising [Unhandled].
+
+ Handles can raise exceptions themselves, in which
+ case, the exception is passed to the handles which
+ were registered before.
+
+ The exception that are considered anomalies should not be
+ handled by registered handlers.
+*)
+
+exception Unhandled
+
+val register_handler : (exn -> Pp.std_ppcmds) -> unit
+
+(** The standard exception printer *)
+val print : exn -> Pp.std_ppcmds
+
+(** Same as [print], except that the "Please report" part of an anomaly
+ isn't printed (used in Ltac debugging). *)
+val print_no_report : exn -> Pp.std_ppcmds
+
+(** Same as [print], except that anomalies are not printed but re-raised
+ (used for the Fail command) *)
+val print_no_anomaly : exn -> Pp.std_ppcmds
diff --git a/lib/explore.ml b/lib/explore.ml
index c40362c8..407bf1e9 100644
--- a/lib/explore.ml
+++ b/lib/explore.ml
@@ -1,13 +1,11 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: explore.ml 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
open Format
(*s Definition of a search problem. *)
diff --git a/lib/explore.mli b/lib/explore.mli
index e01f851c..e64459f1 100644
--- a/lib/explore.mli
+++ b/lib/explore.mli
@@ -1,16 +1,15 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: explore.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
+(** {6 Search strategies. } *)
-(*s Search strategies. *)
-
-(*s A search problem implements the following signature [SearchProblem].
+(** {6 ... } *)
+(** 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
empty list, then search from [s] is aborted; successors of [s] are
@@ -32,7 +31,8 @@ module type SearchProblem = sig
end
-(*s Functor [Make] returns some search functions given a search problem.
+(** {6 ... } *)
+(** Functor [Make] returns some search functions given a search problem.
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).
diff --git a/lib/flags.ml b/lib/flags.ml
index 6b68a8f2..470cf81f 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -1,13 +1,11 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: flags.ml 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
let with_option o f x =
let old = !o in o:=true;
try let r = f x in o := old; r
@@ -25,19 +23,22 @@ let batch_mode = ref false
let debug = ref false
let print_emacs = ref false
-let print_emacs_safechar = ref false
let term_quality = ref false
let xml_export = ref false
-let dont_load_proofs = ref false
+type load_proofs = Force | Lazy | Dont
+
+let load_proofs = ref Lazy
let raw_print = ref false
+let record_print = ref true
+
(* Compatibility mode *)
-type compat_version = V8_2
+type compat_version = V8_2 | V8_3
let compat_version = ref None
let version_strictly_greater v =
match !compat_version with None -> true | Some v' -> v'>v
@@ -86,12 +87,6 @@ let unsafe_set = ref Stringset.empty
let add_unsafe s = unsafe_set := Stringset.add s !unsafe_set
let is_unsafe s = Stringset.mem s !unsafe_set
-(* Flags for the virtual machine *)
-
-let boxed_definitions = ref true
-let set_boxed_definitions b = boxed_definitions := b
-let boxed_definitions _ = !boxed_definitions
-
(* Flags for external tools *)
let subst_command_placeholder s t =
@@ -120,9 +115,21 @@ let is_standard_doc_url url =
url = Coq_config.wwwrefman ||
url = wwwcompatprefix ^ String.sub Coq_config.wwwrefman n (n'-n)
+(* same as in System, but copied here because of dependencies *)
+let canonical_path_name p =
+ let current = Sys.getcwd () in
+ Sys.chdir p;
+ let result = Sys.getcwd () in
+ Sys.chdir current;
+ result
+
(* Options for changing coqlib *)
let coqlib_spec = ref false
-let coqlib = ref Coq_config.coqlib
+let coqlib = ref (
+ (* same as Envars.coqroot, but copied here because of dependencies *)
+ Filename.dirname
+ (canonical_path_name (Filename.dirname Sys.executable_name))
+)
(* Options for changing camlbin (used by coqmktop) *)
let camlbin_spec = ref false
@@ -132,3 +139,9 @@ let camlbin = ref Coq_config.camlbin
let camlp4bin_spec = ref false
let camlp4bin = ref Coq_config.camlp4bin
+(* Level of inlining during a functor application *)
+
+let default_inline_level = 100
+let inline_level = ref default_inline_level
+let set_inline_level = (:=) inline_level
+let get_inline_level () = !inline_level
diff --git a/lib/flags.mli b/lib/flags.mli
index f4325ce2..da43c867 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -1,14 +1,12 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: flags.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
-(* Global options of the system. *)
+(** Global options of the system. *)
val boot : bool ref
@@ -17,17 +15,18 @@ val batch_mode : bool ref
val debug : bool ref
val print_emacs : bool ref
-val print_emacs_safechar : bool ref
val term_quality : bool ref
val xml_export : bool ref
-val dont_load_proofs : bool ref
+type load_proofs = Force | Lazy | Dont
+val load_proofs : load_proofs ref
val raw_print : bool ref
+val record_print : bool ref
-type compat_version = V8_2
+type compat_version = V8_2 | V8_3
val compat_version : compat_version option ref
val version_strictly_greater : compat_version -> bool
val version_less_or_equal : compat_version -> bool
@@ -53,41 +52,41 @@ val if_warn : ('a -> unit) -> 'a -> unit
val hash_cons_proofs : bool ref
-(* Temporary activate an option (to activate option [o] on [f x y z],
+(** Temporary activate an option (to activate option [o] on [f x y z],
use [with_option o (f x y) z]) *)
val with_option : bool ref -> ('a -> 'b) -> 'a -> 'b
-(* Temporary deactivate an option *)
+(** Temporary deactivate an option *)
val without_option : bool ref -> ('a -> 'b) -> 'a -> 'b
-(* If [None], no limit *)
+(** If [None], no limit *)
val set_print_hyps_limit : int option -> unit
val print_hyps_limit : unit -> int option
val add_unsafe : string -> unit
val is_unsafe : string -> bool
-(* Options for the virtual machine *)
-
-val set_boxed_definitions : bool -> unit
-val boxed_definitions : unit -> bool
+(** Options for external tools *)
-(* Options for external tools *)
-
-(* Returns string format for default browser to use from Coq or CoqIDE *)
+(** 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 *)
+(** Substitute %s in the first chain by the second chain *)
val subst_command_placeholder : string -> string -> string
-(* Options for specifying where coq librairies reside *)
+(** Options for specifying where coq librairies reside *)
val coqlib_spec : bool ref
val coqlib : string ref
-(* Options for specifying where OCaml binaries reside *)
+(** Options for specifying where OCaml binaries reside *)
val camlbin_spec : bool ref
val camlbin : string ref
val camlp4bin_spec : bool ref
val camlp4bin : string ref
+
+(** Level of inlining during a functor application *)
+val set_inline_level : int -> unit
+val get_inline_level : unit -> int
+val default_inline_level : int
diff --git a/lib/fmap.mli b/lib/fmap.mli
index c323b055..2c8dedd7 100644
--- a/lib/fmap.mli
+++ b/lib/fmap.mli
@@ -14,7 +14,7 @@ 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. *)
+(** Additions with respect to ocaml standard library. *)
val dom : 'a t -> key list
val rng : 'a t -> 'a list
diff --git a/lib/gmap.ml b/lib/gmap.ml
index 3f979074..bc60a7fc 100644
--- a/lib/gmap.ml
+++ b/lib/gmap.ml
@@ -1,11 +1,10 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: gmap.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
(* 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 6da223d5..cdd6547c 100644
--- a/lib/gmap.mli
+++ b/lib/gmap.mli
@@ -1,14 +1,12 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: gmap.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
-(* Maps using the generic comparison function of ocaml. Same interface as
+(** Maps using the generic comparison function of ocaml. Same interface as
the module [Map] from the ocaml standard library. *)
type ('a,'b) t
@@ -23,7 +21,7 @@ val iter : ('a -> 'b -> unit) -> ('a,'b) t -> unit
val map : ('b -> 'c) -> ('a,'b) t -> ('a,'c) t
val fold : ('a -> 'b -> 'c -> 'c) -> ('a,'b) t -> 'c -> 'c
-(* Additions with respect to ocaml standard library. *)
+(** Additions with respect to ocaml standard library. *)
val dom : ('a,'b) t -> 'a list
val rng : ('a,'b) t -> 'b list
diff --git a/lib/gmapl.ml b/lib/gmapl.ml
index e8dc6295..a0040742 100644
--- a/lib/gmapl.ml
+++ b/lib/gmapl.ml
@@ -1,13 +1,11 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: gmapl.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
-
open Util
type ('a,'b) t = ('a,'b list) Gmap.t
diff --git a/lib/gmapl.mli b/lib/gmapl.mli
index f60aed5d..53a5d96f 100644
--- a/lib/gmapl.mli
+++ b/lib/gmapl.mli
@@ -1,14 +1,12 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: gmapl.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
-(* Maps from ['a] to lists of ['b]. *)
+(** Maps from ['a] to lists of ['b]. *)
type ('a,'b) t
diff --git a/lib/gset.ml b/lib/gset.ml
deleted file mode 100644
index 28b769af..00000000
--- a/lib/gset.ml
+++ /dev/null
@@ -1,242 +0,0 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
-
-(* $Id: gset.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
-
-(* Sets using the generic comparison function of ocaml. Code borrowed from
- the ocaml standard library. *)
-
- type 'a t = Empty | Node of 'a t * 'a * 'a 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 = Pervasives.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 = Pervasives.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 = Pervasives.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 = Pervasives.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 = Pervasives.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
diff --git a/lib/gset.mli b/lib/gset.mli
deleted file mode 100644
index 25e607f7..00000000
--- a/lib/gset.mli
+++ /dev/null
@@ -1,34 +0,0 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
-
-(*i $Id: gset.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
-(* Sets using the generic comparison function of ocaml. Same interface as
- the module [Set] from the ocaml standard library. *)
-
-type 'a t
-
-val empty : 'a t
-val is_empty : 'a t -> bool
-val mem : 'a -> 'a t -> bool
-val add : 'a -> 'a t -> 'a t
-val singleton : 'a -> 'a t
-val remove : 'a -> 'a t -> 'a t
-val union : 'a t -> 'a t -> 'a t
-val inter : 'a t -> 'a t -> 'a t
-val diff : 'a t -> 'a t -> 'a t
-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 -> 'b -> 'b) -> 'a t -> 'b -> 'b
-val cardinal : 'a t -> int
-val elements : 'a t -> 'a list
-val min_elt : 'a t -> 'a
-val max_elt : 'a t -> 'a
-val choose : 'a t -> 'a
diff --git a/lib/hashcons.ml b/lib/hashcons.ml
index 542ecde9..8ab718d5 100644
--- a/lib/hashcons.ml
+++ b/lib/hashcons.ml
@@ -1,13 +1,11 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: hashcons.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
-
(* Hash consing of datastructures *)
(* The generic hash-consing functions (does not use Obj) *)
diff --git a/lib/hashcons.mli b/lib/hashcons.mli
index 81c74aef..65b1e0e9 100644
--- a/lib/hashcons.mli
+++ b/lib/hashcons.mli
@@ -1,14 +1,12 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: hashcons.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
-(* Generic hash-consing. *)
+(** Generic hash-consing. *)
module type Comp =
sig
@@ -37,7 +35,7 @@ val recursive2_hcons :
(unit -> ('t1 -> 't1) * ('t2 -> 't2) * 'u2 -> 't2 -> 't2) ->
'u1 -> 'u2 -> ('t1 -> 't1) * ('t2 -> 't2)
-(* Declaring and reinitializing global hash-consing functions *)
+(** Declaring and reinitializing global hash-consing functions *)
val init : unit -> unit
val register_hcons : ('u -> 't -> 't) -> ('u -> 't -> 't)
diff --git a/lib/hashtbl_alt.ml b/lib/hashtbl_alt.ml
new file mode 100644
index 00000000..9e0f0dec
--- /dev/null
+++ b/lib/hashtbl_alt.ml
@@ -0,0 +1,109 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+(* The following module is a specialized version of [Hashtbl] that is
+ a better space saver. Actually, [Hashcons] instanciates [Hashtbl.t]
+ with [constr] used both as a key and as an image. Thus, in each
+ cell of the internal bucketlist, there are two representations of
+ the same value. In this implementation, there is only one.
+
+ Besides, the responsibility of computing the hash function is now
+ given to the caller, which makes possible the interleaving of the
+ hash key computation and the hash-consing. *)
+
+module type Hashtype = sig
+ type t
+ val equals : t -> t -> bool
+end
+
+module type S = sig
+ type elt
+ (* [may_add_and_get key constr] uses [key] to look for [constr]
+ in the hash table [H]. If [constr] is in [H], returns the
+ specific representation that is stored in [H]. Otherwise,
+ [constr] is stored in [H] and will be used as the canonical
+ representation of this value in the future. *)
+ val may_add_and_get : int -> elt -> elt
+end
+
+module Make (E : Hashtype) =
+ struct
+
+ type elt = E.t
+
+ type bucketlist = Empty | Cons of elt * int * bucketlist
+
+ let initial_size = 19991
+ let table_data = ref (Array.make initial_size Empty)
+ let table_size = ref 0
+
+ let resize () =
+ let odata = !table_data in
+ let osize = Array.length odata in
+ let nsize = min (2 * osize + 1) Sys.max_array_length in
+ if nsize <> osize then begin
+ let ndata = Array.create nsize Empty in
+ let rec insert_bucket = function
+ | Empty -> ()
+ | Cons (key, hash, rest) ->
+ let nidx = hash mod nsize in
+ ndata.(nidx) <- Cons (key, hash, ndata.(nidx));
+ insert_bucket rest
+ in
+ for i = 0 to osize - 1 do insert_bucket odata.(i) done;
+ table_data := ndata
+ end
+
+ let add hash key =
+ let odata = !table_data in
+ let osize = Array.length odata in
+ let i = hash mod osize in
+ odata.(i) <- Cons (key, hash, odata.(i));
+ incr table_size;
+ if !table_size > osize lsl 1 then resize ()
+
+ let find_rec hash key bucket =
+ let rec aux = function
+ | Empty ->
+ add hash key; key
+ | Cons (k, h, rest) ->
+ if hash == h && E.equals key k then k else aux rest
+ in
+ aux bucket
+
+ let may_add_and_get hash key =
+ let odata = !table_data in
+ match odata.(hash mod (Array.length odata)) with
+ | Empty -> add hash key; key
+ | Cons (k1, h1, rest1) ->
+ if hash == h1 && E.equals key k1 then k1 else
+ match rest1 with
+ | Empty -> add hash key; key
+ | Cons (k2, h2, rest2) ->
+ if hash == h2 && E.equals key k2 then k2 else
+ match rest2 with
+ | Empty -> add hash key; key
+ | Cons (k3, h3, rest3) ->
+ if hash == h2 && E.equals key k3 then k3
+ else find_rec hash key rest3
+
+end
+
+module Combine = struct
+ (* These are helper functions to combine the hash keys in a similar
+ way as [Hashtbl.hash] does. The constants [alpha] and [beta] must
+ be prime numbers. There were chosen empirically. Notice that the
+ problem of hashing trees is hard and there are plenty of study on
+ this topic. Therefore, there must be room for improvement here. *)
+ let alpha = 65599
+ let beta = 7
+ let combine x y = x * alpha + y
+ let combine3 x y z = combine x (combine y z)
+ let combine4 x y z t = combine x (combine3 y z t)
+ let combinesmall x y = beta * x + y
+end
diff --git a/lib/hashtbl_alt.mli b/lib/hashtbl_alt.mli
new file mode 100644
index 00000000..a22dbc28
--- /dev/null
+++ b/lib/hashtbl_alt.mli
@@ -0,0 +1,41 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+(* The following module is a specialized version of [Hashtbl] that is
+ a better space saver. Actually, [Hashcons] instanciates [Hashtbl.t]
+ with [constr] used both as a key and as an image. Thus, in each
+ cell of the internal bucketlist, there are two representations of
+ the same value. In this implementation, there is only one.
+
+ Besides, the responsibility of computing the hash function is now
+ given to the caller, which makes possible the interleaving of the
+ hash key computation and the hash-consing. *)
+
+module type Hashtype = sig
+ type t
+ val equals : t -> t -> bool
+end
+
+module type S = sig
+ type elt
+ (* [may_add_and_get key constr] uses [key] to look for [constr]
+ in the hash table [H]. If [constr] is in [H], returns the
+ specific representation that is stored in [H]. Otherwise,
+ [constr] is stored in [H] and will be used as the canonical
+ representation of this value in the future. *)
+ val may_add_and_get : int -> elt -> elt
+end
+
+module Make (E : Hashtype) : S with type elt = E.t
+
+module Combine : sig
+ val combine : int -> int -> int
+ val combinesmall : int -> int -> int
+ val combine3 : int -> int -> int -> int
+ val combine4 : int -> int -> int -> int -> int
+end
diff --git a/lib/heap.ml b/lib/heap.ml
index c61bccb9..f3326749 100644
--- a/lib/heap.ml
+++ b/lib/heap.ml
@@ -1,13 +1,11 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: heap.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
-
(*s Heaps *)
module type Ordered = sig
diff --git a/lib/heap.mli b/lib/heap.mli
index 3183e0ec..9cf23dd3 100644
--- a/lib/heap.mli
+++ b/lib/heap.mli
@@ -1,14 +1,12 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: heap.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
-(* Heaps *)
+(** Heaps *)
module type Ordered = sig
type t
@@ -17,29 +15,29 @@ end
module type S =sig
- (* Type of functional heaps *)
+ (** Type of functional heaps *)
type t
- (* Type of elements *)
+ (** Type of elements *)
type elt
- (* The empty heap *)
+ (** The empty heap *)
val empty : t
- (* [add x h] returns a new heap containing the elements of [h], plus [x];
- complexity $O(log(n))$ *)
+ (** [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)$ *)
+ (** [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
+ (** [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))$ *)
+ complexity {% $ %}O(log(n)){% $ %} *)
val remove : t -> t
- (* usual iterators and combinators; elements are presented in
+ (** usual iterators and combinators; elements are presented in
arbitrary order *)
val iter : (elt -> unit) -> t -> unit
@@ -49,6 +47,6 @@ end
exception EmptyHeap
-(*S Functional implementation. *)
+(** {6 Functional implementation. } *)
module Functional(X: Ordered) : S with type elt=X.t
diff --git a/lib/lib.mllib b/lib/lib.mllib
index 1743ce26..db79b5c2 100644
--- a/lib/lib.mllib
+++ b/lib/lib.mllib
@@ -1,3 +1,6 @@
+Xml_lexer
+Xml_parser
+Xml_utils
Pp_control
Pp
Compat
@@ -5,19 +8,16 @@ Flags
Segmenttree
Unicodetable
Util
+Errors
Bigint
Hashcons
Dyn
System
Envars
-Bstack
-Edit
-Gset
Gmap
Fset
Fmap
-Tlm
-tries
+Tries
Gmapl
Profile
Explore
@@ -26,4 +26,6 @@ Rtree
Heap
Option
Dnet
-
+Store
+Unionfind
+Hashtbl_alt
diff --git a/lib/option.ml b/lib/option.ml
index f4b1604f..c3fe9ce4 100644
--- a/lib/option.ml
+++ b/lib/option.ml
@@ -1,13 +1,11 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: option.ml 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
(** Module implementing basic combinators for OCaml option type.
It tries follow closely the style of OCaml standard library.
diff --git a/lib/option.mli b/lib/option.mli
index 1dc721fe..b9fd7d2f 100644
--- a/lib/option.mli
+++ b/lib/option.mli
@@ -1,13 +1,11 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: option.mli 14641 2011-11-06 11:59:10Z herbelin $ *)
-
(** Module implementing basic combinators for OCaml option type.
It tries follow closely the style of OCaml standard library.
diff --git a/lib/pp.ml4 b/lib/pp.ml4
index d02b5c4d..c602b403 100644
--- a/lib/pp.ml4
+++ b/lib/pp.ml4
@@ -1,13 +1,11 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: pp.ml4 14641 2011-11-06 11:59:10Z herbelin $ *)
-
open Pp_control
(* This should not be used outside of this file. Use
@@ -275,11 +273,6 @@ 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 ppcmds x = Ppdir_ppcmds x
-
(* Special chars for emacs, to detect warnings inside goal output *)
let emacs_warning_start_string = String.make 1 (Char.chr 254)
let emacs_warning_end_string = String.make 1 (Char.chr 255)
@@ -339,3 +332,7 @@ let msgnl x = msgnl_with !std_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
+
+let string_of_ppcmds c =
+ msg_with Format.str_formatter c;
+ Format.flush_str_formatter ()
diff --git a/lib/pp.mli b/lib/pp.mli
index 61b544e3..7070e3f5 100644
--- a/lib/pp.mli
+++ b/lib/pp.mli
@@ -1,30 +1,26 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: pp.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
-(*i*)
open Pp_control
-(*i*)
-(* Modify pretty printing functions behavior for emacs ouput (special
+(** Modify pretty printing functions behavior for emacs ouput (special
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. *)
+(** Pretty-printers. *)
type ppcmd
type std_ppcmds = ppcmd Stream.t
-(*s Formatting commands. *)
+(** {6 Formatting commands. } *)
val str : string -> std_ppcmds
val stras : int * string -> std_ppcmds
@@ -40,11 +36,11 @@ val ismt : std_ppcmds -> bool
val comment : int -> std_ppcmds
val comments : ((int * int) * string) list ref
-(*s Concatenation. *)
+(** {6 Concatenation. } *)
val (++) : std_ppcmds -> std_ppcmds -> std_ppcmds
-(*s Derived commands. *)
+(** {6 Derived commands. } *)
val spc : unit -> std_ppcmds
val cut : unit -> std_ppcmds
@@ -59,7 +55,7 @@ val strbrk : string -> std_ppcmds
val xmlescape : ppcmd -> ppcmd
-(*s Boxing commands. *)
+(** {6 Boxing commands. } *)
val h : int -> std_ppcmds -> std_ppcmds
val v : int -> std_ppcmds -> std_ppcmds
@@ -67,7 +63,7 @@ val hv : int -> std_ppcmds -> std_ppcmds
val hov : int -> std_ppcmds -> std_ppcmds
val t : std_ppcmds -> std_ppcmds
-(*s Opening and closing of boxes. *)
+(** {6 Opening and closing of boxes. } *)
val hb : int -> std_ppcmds
val vb : int -> std_ppcmds
@@ -77,7 +73,7 @@ val tb : unit -> std_ppcmds
val close : unit -> std_ppcmds
val tclose : unit -> std_ppcmds
-(*s Pretty-printing functions \emph{without flush}. *)
+(** {6 Pretty-printing functions {% \emph{%}without flush{% }%}. } *)
val pp_with : Format.formatter -> std_ppcmds -> unit
val ppnl_with : Format.formatter -> std_ppcmds -> unit
@@ -87,31 +83,34 @@ 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}. *)
+(** {6 Pretty-printing functions {% \emph{%}with flush{% }%}. } *)
val msg_with : Format.formatter -> std_ppcmds -> unit
val msgnl_with : Format.formatter -> std_ppcmds -> unit
-(*s The following functions are instances of the previous ones on
+(** {6 ... } *)
+(** The following functions are instances of the previous ones on
[std_ft] and [err_ft]. *)
-(*s Pretty-printing functions \emph{without flush} on [stdout] and [stderr]. *)
+(** {6 Pretty-printing functions {% \emph{%}without flush{% }%} on [stdout] and [stderr]. } *)
val pp : std_ppcmds -> unit
val ppnl : std_ppcmds -> unit
val pperr : std_ppcmds -> unit
val pperrnl : std_ppcmds -> unit
-val message : string -> unit (* = pPNL *)
+val message : string -> unit (** = pPNL *)
val warning : string -> unit
val warn : std_ppcmds -> unit
val pp_flush : unit -> unit
val flush_all: unit -> unit
-(*s Pretty-printing functions \emph{with flush} on [stdout] and [stderr]. *)
+(** {6 Pretty-printing functions {% \emph{%}with flush{% }%} on [stdout] and [stderr]. } *)
val msg : std_ppcmds -> unit
val msgnl : std_ppcmds -> unit
val msgerr : std_ppcmds -> unit
val msgerrnl : std_ppcmds -> unit
val msg_warning : std_ppcmds -> unit
+
+val string_of_ppcmds : std_ppcmds -> string
diff --git a/lib/pp_control.ml b/lib/pp_control.ml
index a7ad553b..cefd08c5 100644
--- a/lib/pp_control.ml
+++ b/lib/pp_control.ml
@@ -1,13 +1,11 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: pp_control.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
-
(* Parameters of pretty-printing *)
type pp_global_params = {
@@ -49,40 +47,18 @@ let get_gp ft =
max_depth = Format.pp_get_max_boxes ft ();
ellipsis = Format.pp_get_ellipsis_text ft () }
-
-(* Output functions of pretty-printing *)
-
-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 = {
- fp_output = stdout ;
- fp_output_function = output stdout;
- fp_flush_function = (fun () -> flush stdout) }
-
-let err_fp = {
- fp_output = stderr ;
- fp_output_function = output stderr;
- fp_flush_function = (fun () -> flush stderr) }
-
(* with_fp : 'a pp_formatter_params -> Format.formatter
* returns of formatter for given formatter functions *)
-let with_fp fp =
- let ft = Format.make_formatter fp.fp_output_function fp.fp_flush_function in
- Format.pp_set_formatter_out_channel ft fp.fp_output;
+let with_fp chan out_function flush_function =
+ let ft = Format.make_formatter out_function flush_function in
+ Format.pp_set_formatter_out_channel ft chan;
ft
(* Output on a channel ch *)
let with_output_to ch =
- let ft = with_fp { fp_output = ch ;
- fp_output_function = (output ch) ;
- fp_flush_function = (fun () -> flush ch) } in
+ let ft = with_fp ch (output ch) (fun () -> flush ch) in
set_gp ft deep_gp;
ft
diff --git a/lib/pp_control.mli b/lib/pp_control.mli
index bbc771d5..c66255f9 100644
--- a/lib/pp_control.mli
+++ b/lib/pp_control.mli
@@ -1,14 +1,12 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: pp_control.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
-(* Parameters of pretty-printing. *)
+(** Parameters of pretty-printing. *)
type pp_global_params = {
margin : int;
@@ -23,24 +21,15 @@ val set_dflt_gp : Format.formatter -> unit
val get_gp : Format.formatter -> pp_global_params
-(*s Output functions of pretty-printing. *)
-
-type 'a pp_formatter_params = {
- fp_output : out_channel;
- fp_output_function : string -> int -> int -> unit;
- fp_flush_function : unit -> unit }
-
-val std_fp : (int*string) pp_formatter_params
-val err_fp : (int*string) pp_formatter_params
+(** {6 Output functions of pretty-printing. } *)
-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 ref
val deep_ft : Format.formatter ref
-(*s For parametrization through vernacular. *)
+(** {6 For parametrization through vernacular. } *)
val set_depth_boxes : int option -> unit
val get_depth_boxes : unit -> int option
diff --git a/lib/predicate.ml b/lib/predicate.ml
index 506a87c9..e419aa6e 100644
--- a/lib/predicate.ml
+++ b/lib/predicate.ml
@@ -10,8 +10,6 @@
(* *)
(************************************************************************)
-(* $Id: predicate.ml 12337 2009-09-17 15:58:14Z glondu $ *)
-
(* Sets over ordered types *)
module type OrderedType =
diff --git a/lib/predicate.mli b/lib/predicate.mli
index 85596fea..bcc89e72 100644
--- a/lib/predicate.mli
+++ b/lib/predicate.mli
@@ -1,9 +1,7 @@
-(*i $Id: predicate.mli 6621 2005-01-21 17:24:37Z herbelin $ i*)
+(** Module [Pred]: sets over infinite ordered types with complement. *)
-(* Module [Pred]: sets over infinite ordered types with complement. *)
-
-(* This module implements the set data structure, given a total ordering
+(** This module implements the set data structure, given a total ordering
function over the set elements. All operations over sets
are purely applicative (no side-effects).
The implementation uses the Set library. *)
@@ -13,7 +11,7 @@ module type OrderedType =
type t
val compare: t -> t -> int
end
- (* The input signature of the functor [Pred.Make].
+ (** The input signature of the functor [Pred.Make].
[t] is the type of the set elements.
[compare] is a total ordering function over the set elements.
This is a two-argument function [f] such that
@@ -26,44 +24,44 @@ module type OrderedType =
module type S =
sig
type elt
- (* The type of the set elements. *)
+ (** The type of the set elements. *)
type t
- (* The type of sets. *)
+ (** The type of sets. *)
val empty: t
- (* The empty set. *)
+ (** The empty set. *)
val full: t
- (* The whole type. *)
+ (** The whole type. *)
val is_empty: t -> bool
- (* Test whether a set is empty or not. *)
+ (** Test whether a set is empty or not. *)
val is_full: t -> bool
- (* Test whether a set contains the whole type or not. *)
+ (** Test whether a set contains the whole type or not. *)
val mem: elt -> t -> bool
- (* [mem x s] tests whether [x] belongs to the set [s]. *)
+ (** [mem x s] tests whether [x] belongs to the set [s]. *)
val singleton: elt -> t
- (* [singleton x] returns the one-element set containing only [x]. *)
+ (** [singleton x] returns the one-element set containing only [x]. *)
val add: elt -> t -> t
- (* [add x s] returns a set containing all elements of [s],
+ (** [add x s] returns a set containing all elements of [s],
plus [x]. If [x] was already in [s], [s] is returned unchanged. *)
val remove: elt -> t -> t
- (* [remove x s] returns a set containing all elements of [s],
+ (** [remove x s] returns a set containing all elements of [s],
except [x]. If [x] was not in [s], [s] is returned unchanged. *)
val union: t -> t -> t
val inter: t -> t -> t
val diff: t -> t -> t
val complement: t -> t
- (* Union, intersection, difference and set complement. *)
+ (** Union, intersection, difference and set complement. *)
val equal: t -> t -> bool
- (* [equal s1 s2] tests whether the sets [s1] and [s2] are
+ (** [equal s1 s2] tests whether the sets [s1] and [s2] are
equal, that is, contain equal elements. *)
val subset: t -> t -> bool
- (* [subset s1 s2] tests whether the set [s1] is a subset of
+ (** [subset s1 s2] tests whether the set [s1] is a subset of
the set [s2]. *)
val elements: t -> bool * elt list
- (* Gives a finite representation of the predicate: if the
+ (** Gives a finite representation of the predicate: if the
boolean is false, then the predicate is given in extension.
if it is true, then the complement is given *)
end
module Make(Ord: OrderedType): (S with type elt = Ord.t)
- (* Functor building an implementation of the set structure
+ (** Functor building an implementation of the set structure
given a totally ordered type. *)
diff --git a/lib/profile.ml b/lib/profile.ml
index 95163a27..a6e2faa4 100644
--- a/lib/profile.ml
+++ b/lib/profile.ml
@@ -1,17 +1,12 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: profile.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
-
-open Gc
-
let word_length = Sys.word_size / 8
-let int_size = Sys.word_size - 1
let float_of_time t = float_of_int t /. 100.
let time_of_float f = int_of_float (f *. 100.)
@@ -354,7 +349,6 @@ let close_profile print =
end
| _ -> failwith "Inconsistency"
-let append_profile () = close_profile false
let print_profile () = close_profile true
let declare_profile name =
diff --git a/lib/profile.mli b/lib/profile.mli
index 208238e7..bd113687 100644
--- a/lib/profile.mli
+++ b/lib/profile.mli
@@ -1,20 +1,16 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: profile.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
+(** {6 This program is a small time and allocation profiler for Objective Caml } *)
-(*s This program is a small time and allocation profiler for Objective Caml *)
+(** Adapted from Christophe Raffalli *)
-(*i It requires the UNIX library *)
-
-(* Adapted from Christophe Raffalli *)
-
-(* To use it, link it with the program you want to profile.
+(** 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 :
@@ -106,23 +102,23 @@ val profile7 :
-> 'a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h
-(* Some utilities to compute the logical and physical sizes and depth
+(** Some utilities to compute the logical and physical sizes and depth
of ML objects *)
-(* Print logical size (in words) and depth of its argument *)
-(* This function does not disturb the heap *)
+(** Print logical size (in words) and depth of its argument
+ This function does not disturb the heap *)
val print_logical_stats : 'a -> unit
-(* Print physical size, logical size (in words) and depth of its argument *)
-(* This function allocates itself a lot (the same order of magnitude
+(** Print physical size, logical size (in words) and depth of its argument
+ This function allocates itself a lot (the same order of magnitude
as the physical size of its argument) *)
val print_stats : 'a -> unit
-(* Return logical size (first for strings, then for not strings),
- (in words) and depth of its argument *)
-(* This function allocates itself a lot *)
+(** Return logical size (first for strings, then for not strings),
+ (in words) and depth of its argument
+ This function allocates itself a lot *)
val obj_stats : 'a -> int * int * int
-(* Return physical size of its argument (string part and rest) *)
-(* This function allocates itself a lot *)
+(** Return physical size of its argument (string part and rest)
+ This function allocates itself a lot *)
val obj_shared_size : 'a -> int * int
diff --git a/lib/refutpat.ml4 b/lib/refutpat.ml4
deleted file mode 100644
index db25ce73..00000000
--- a/lib/refutpat.ml4
+++ /dev/null
@@ -1,33 +0,0 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
-(* \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 991ed25c..22d3d72b 100644
--- a/lib/rtree.ml
+++ b/lib/rtree.ml
@@ -1,13 +1,11 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: rtree.ml 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
open Util
diff --git a/lib/rtree.mli b/lib/rtree.mli
index 01fff68a..6695fc82 100644
--- a/lib/rtree.mli
+++ b/lib/rtree.mli
@@ -1,24 +1,22 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: rtree.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
-(* Type of regular tree with nodes labelled by values of type 'a *)
-(* The implementation uses de Bruijn indices, so binding capture
+(** 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 *)
+(** Building trees *)
-(* build a node given a label and the vector of sons *)
+(** build a node given a label and the vector of sons *)
val mk_node : 'a -> 'a t array -> 'a t
-(* Build mutually recursive 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
@@ -32,27 +30,29 @@ val mk_node : 'a -> 'a t array -> 'a t
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|]|]
+ 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
+(** [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 is_node : 'a t -> bool
-(* Destructors (recursive calls are expanded) *)
+
+(** Destructors (recursive calls are expanded) *)
val dest_node : 'a t -> 'a * 'a t array
-(* dest_param is not needed for closed trees (i.e. with no free variable) *)
+
+(** 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 *)
+(** Tells if a tree has an infinite branch *)
val is_infinite : 'a t -> bool
-(* [compare_rtree f t1 t2] compares t1 t2 (top-down).
+(** [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,
@@ -66,14 +66,15 @@ 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 *)
+(** Iterators *)
val map : ('a -> 'b) -> 'a t -> 'b t
-(* [(smartmap f t) == t] if [(f a) ==a ] for all nodes *)
+
+(** [(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 *)
+(** A rather simple minded pretty-printer *)
val pp_tree : ('a -> Pp.std_ppcmds) -> 'a t -> Pp.std_ppcmds
diff --git a/lib/segmenttree.ml b/lib/segmenttree.ml
index 2a7f9df0..9ce348a0 100644
--- a/lib/segmenttree.ml
+++ b/lib/segmenttree.ml
@@ -40,7 +40,6 @@ type domain =
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
diff --git a/lib/segmenttree.mli b/lib/segmenttree.mli
index 4aea13e9..3258537b 100644
--- a/lib/segmenttree.mli
+++ b/lib/segmenttree.mli
@@ -7,7 +7,7 @@
(** 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
+(** [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. *)
diff --git a/lib/store.ml b/lib/store.ml
new file mode 100644
index 00000000..bc1b335f
--- /dev/null
+++ b/lib/store.ml
@@ -0,0 +1,61 @@
+(***********************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* \VV/ *************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(***********************************************************************)
+
+(*** This module implements an "untyped store", in this particular case we
+ see it as an extensible record whose fields are left unspecified. ***)
+
+(* We give a short implementation of a universal type. This is mostly equivalent
+ to what is proposed by module Dyn.ml, except that it requires no explicit tag. *)
+module type Universal = sig
+ type t
+
+ type 'a etype = {
+ put : 'a -> t ;
+ get : t -> 'a option
+ }
+
+ val embed : unit -> 'a etype
+end
+
+(* We use a dynamic "name" allocator. But if we needed to serialise stores, we
+might want something static to avoid troubles with plugins order. *)
+
+let next =
+ let count = ref 0 in fun () ->
+ let n = !count in
+ incr count;
+ n
+
+type t = Obj.t Util.Intmap.t
+
+module Field = struct
+ type 'a field = {
+ set : 'a -> t -> t ;
+ get : t -> 'a option ;
+ remove : t -> t
+ }
+ type 'a t = 'a field
+end
+
+open Field
+
+let empty = Util.Intmap.empty
+
+let field () =
+ let fid = next () in
+ let set a s =
+ Util.Intmap.add fid (Obj.repr a) s
+ in
+ let get s =
+ try Some (Obj.obj (Util.Intmap.find fid s))
+ with _ -> None
+ in
+ let remove s =
+ Util.Intmap.remove fid s
+ in
+ { set = set ; get = get ; remove = remove }
diff --git a/lib/store.mli b/lib/store.mli
new file mode 100644
index 00000000..5df0c99a
--- /dev/null
+++ b/lib/store.mli
@@ -0,0 +1,25 @@
+(***********************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* \VV/ *************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(***********************************************************************)
+
+(*** This module implements an "untyped store", in this particular case we
+ see it as an extensible record whose fields are left unspecified. ***)
+
+type t
+
+module Field : sig
+ type 'a field = {
+ set : 'a -> t -> t ;
+ get : t -> 'a option ;
+ remove : t -> t
+ }
+ type 'a t = 'a field
+end
+
+val empty : t
+
+val field : unit -> 'a Field.field
diff --git a/lib/system.ml b/lib/system.ml
index 94a57792..7d54e2c3 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -1,12 +1,12 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: system.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
+(* $Id$ *)
open Pp
open Util
@@ -33,7 +33,7 @@ let home =
try Sys.getenv "USERPROFILE" with Not_found ->
warning ("Cannot determine user home directory, using '.' .");
flush_all ();
- "."
+ Filename.current_dir_name
let safe_getenv n = safe_getenv_def n ("$"^n)
@@ -72,20 +72,49 @@ type load_path = physical_path list
let physical_path_of_string s = s
let string_of_physical_path p = p
+(*
+ * Split a path into a list of directories. A one-liner with Str, but Coq
+ * doesn't seem to use this library at all, so here is a slighly longer version.
+ *)
+
+let lpath_from_path path path_separator =
+ let n = String.length path in
+ let rec aux i l =
+ 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
+ aux (j+1) (dir::l)
+ else
+ l
+ in List.rev (aux 0 [])
+
(* Hints to partially detects if two paths refer to the same repertory *)
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
- remove_path_dot (String.sub p n (String.length p - n))
+ let l = String.length p in
+ if l > n && String.sub p 0 n = curdir then
+ let n' =
+ let sl = String.length Filename.dir_sep in
+ let i = ref n in
+ while !i <= l - sl && String.sub p !i sl = Filename.dir_sep do i := !i + sl done; !i in
+ remove_path_dot (String.sub p n' (l - n'))
else
p
let strip_path p =
let cwd = Filename.concat (Sys.getcwd ()) "" in (* Unix: "`pwd`/" *)
let n = String.length cwd in
- if String.length p > n && String.sub p 0 n = cwd then
- remove_path_dot (String.sub p n (String.length p - n))
+ let l = String.length p in
+ if l > n && String.sub p 0 n = cwd then
+ let n' =
+ let sl = String.length Filename.dir_sep in
+ let i = ref n in
+ while !i <= l - sl && String.sub p !i sl = Filename.dir_sep do i := !i + sl done; !i in
+ remove_path_dot (String.sub p n' (l - n'))
else
remove_path_dot p
@@ -179,6 +208,14 @@ let is_in_path lpath filename =
try ignore (where_in_path ~warn:false lpath filename); true
with Not_found -> false
+let path_separator = if Sys.os_type = "Unix" then ':' else ';'
+
+let is_in_system_path filename =
+ let path = try Sys.getenv "PATH"
+ with Not_found -> error "system variable PATH not found" in
+ let lpath = lpath_from_path path path_separator in
+ is_in_path lpath filename
+
let make_suffix name suffix =
if Filename.check_suffix name suffix then name else (name ^ suffix)
@@ -300,34 +337,10 @@ let run_command converter f c =
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 t = times () in
- (t.tms_utime, t.tms_stime)
-
let get_time () =
let t = times () in
(time(), t.tms_utime, t.tms_stime)
diff --git a/lib/system.mli b/lib/system.mli
index 6998085c..fae7fd1e 100644
--- a/lib/system.mli
+++ b/lib/system.mli
@@ -1,18 +1,19 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: system.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
+(** System utilities *)
-(*s Files and load paths. Load path entries remember the original root
+(** {6 Files and load paths} *)
+
+(** Load path entries remember the original root
given by the user. For efficiency, we keep the full path (field
[directory]), the root path and the path relative to the root. *)
-
type physical_path = string
type load_path = physical_path list
@@ -22,6 +23,7 @@ val exclude_search_in_dirname : string -> unit
val all_subdirs : unix_path:string -> (physical_path * string list) list
val is_in_path : load_path -> string -> bool
+val is_in_system_path : string -> bool
val where_in_path : ?warn:bool -> load_path -> string -> physical_path * string
val physical_path_of_string : string -> physical_path
@@ -39,7 +41,8 @@ val exists_dir : string -> bool
val find_file_in_path :
?warn:bool -> load_path -> string -> physical_path * string
-(*s Generic input and output functions, parameterized by a magic number
+(** {6 I/O functions } *)
+(** Generic input and output functions, parameterized by a magic number
and a suffix. The intern functions raise the exception [Bad_magic_number]
when the check fails, with the full file name. *)
@@ -56,11 +59,12 @@ val extern_intern : ?warn:bool -> int -> string ->
val with_magic_number_check : ('a -> 'b) -> 'a -> 'b
-(*s Sending/receiving once with external executable *)
+(** {6 Sending/receiving once with external executable } *)
val connect : (out_channel -> unit) -> (in_channel -> 'a) -> string -> 'a
-(*s [run_command converter f com] launches command [com], and returns
+(** {6 Executing commands } *)
+(** [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] *)
@@ -68,13 +72,10 @@ val connect : (out_channel -> unit) -> (in_channel -> 'a) -> string -> 'a
val run_command : (string -> string) -> (string -> unit) -> string ->
Unix.process_status * string
-val search_exe_in_path : string -> string option
-
-(*s Time stamps. *)
+(** {6 Time stamps.} *)
type time
-val process_time : unit -> float * float
val get_time : unit -> time
-val time_difference : time -> time -> float (* in seconds *)
+val time_difference : time -> time -> float (** in seconds *)
val fmt_time_difference : time -> time -> Pp.std_ppcmds
diff --git a/lib/tlm.ml b/lib/tlm.ml
deleted file mode 100644
index 17d337c8..00000000
--- a/lib/tlm.ml
+++ /dev/null
@@ -1,63 +0,0 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
-
-(* $Id: tlm.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
-
-type ('a,'b) t = Node of 'b Gset.t * ('a, ('a,'b) t) Gmap.t
-
-let empty = Node (Gset.empty, Gmap.empty)
-
-let map (Node (_,m)) lbl = Gmap.find lbl m
-
-let xtract (Node (hereset,_)) = Gset.elements hereset
-
-let dom (Node (_,m)) = Gmap.dom m
-
-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
- m
- else
- Gmap.add lbl (Node (Gset.empty,Gmap.empty)) m
-
-let cleanse_arcs (Node (hereset,m)) =
- 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
- 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 rec apprec pfx (Node(hereset,m)) =
- 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
- 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)) (Gset.elements hereset))::
- (List.map (fun (l,tm) -> torec (l::pfx) tm) (Gmap.to_list m)))
- in
- torec [] tlm
diff --git a/lib/tlm.mli b/lib/tlm.mli
deleted file mode 100644
index 9042281f..00000000
--- a/lib/tlm.mli
+++ /dev/null
@@ -1,32 +0,0 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
-
-(*i $Id: tlm.mli 14641 2011-11-06 11:59:10Z herbelin $ 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]. *)
-
-type ('a,'b) t
-
-val empty : ('a,'b) t
-
-(* Work on labels, not on paths. *)
-
-val map : ('a,'b) t -> 'a -> ('a,'b) t
-val xtract : ('a,'b) t -> 'b list
-val dom : ('a,'b) t -> 'a list
-val in_dom : ('a,'b) t -> 'a -> bool
-
-(* Work on paths, not on labels. *)
-
-val add : ('a,'b) t -> 'a list * 'b -> ('a,'b) t
-val rmv : ('a,'b) t -> ('a list * 'b) -> ('a,'b) t
-
-val app : (('a list * 'b) -> unit) -> ('a,'b) t -> unit
-val to_list : ('a,'b) t -> ('a list * 'b) list
-
diff --git a/lib/tries.ml b/lib/tries.ml
index 2540bd1e..e7fe8a66 100644
--- a/lib/tries.ml
+++ b/lib/tries.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/lib/tries.mli b/lib/tries.mli
index 342c81ec..8e837677 100644
--- a/lib/tries.mli
+++ b/lib/tries.mli
@@ -12,7 +12,7 @@ sig
val empty : t
- (* Work on labels, not on paths. *)
+ (** Work on labels, not on paths. *)
val map : t -> Y.t -> t
@@ -22,7 +22,7 @@ sig
val in_dom : t -> Y.t -> bool
- (* Work on paths, not on labels. *)
+ (** Work on paths, not on labels. *)
val add : t -> Y.t list * X.t -> t
diff --git a/lib/unionfind.ml b/lib/unionfind.ml
new file mode 100644
index 00000000..b05f8de0
--- /dev/null
+++ b/lib/unionfind.ml
@@ -0,0 +1,115 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+(** An imperative implementation of partitions via Union-Find *)
+
+(** Paths are compressed imperatively at each lookup of a
+ canonical representative. Each union also modifies in-place
+ the partition structure.
+
+ Nota: For the moment we use Pervasive's comparison for
+ choosing the smallest object as representative. This could
+ be made more generic.
+*)
+
+
+
+module type PartitionSig = sig
+
+ (** The type of elements in the partition *)
+ type elt
+
+ (** A set structure over elements *)
+ type set
+
+ (** The type of partitions *)
+ type t
+
+ (** Initialise an empty partition *)
+ val create : unit -> t
+
+ (** Add (in place) an element in the partition, or do nothing
+ if the element is already in the partition. *)
+ val add : elt -> t -> unit
+
+ (** Find the canonical representative of an element.
+ Raise [not_found] if the element isn't known yet. *)
+ val find : elt -> t -> elt
+
+ (** Merge (in place) the equivalence classes of two elements.
+ This will add the elements in the partition if necessary. *)
+ val union : elt -> elt -> t -> unit
+
+ (** Merge (in place) the equivalence classes of many elements. *)
+ val union_set : set -> t -> unit
+
+ (** Listing the different components of the partition *)
+ val partition : t -> set list
+
+end
+
+module Make (S:Set.S)(M:Map.S with type key = S.elt) = struct
+
+ type elt = S.elt
+ type set = S.t
+
+ type node =
+ | Canon of set
+ | Equiv of elt
+
+ type t = node ref M.t ref
+
+ let create () = ref (M.empty : node ref M.t)
+
+ let fresh x p =
+ let node = ref (Canon (S.singleton x)) in
+ p := M.add x node !p;
+ x, node
+
+ let rec lookup x p =
+ let node = M.find x !p in
+ match !node with
+ | Canon _ -> x, node
+ | Equiv y ->
+ let ((z,_) as res) = lookup y p in
+ if not (z == y) then node := Equiv z;
+ res
+
+ let add x p = if not (M.mem x !p) then ignore (fresh x p)
+
+ let find x p = fst (lookup x p)
+
+ let canonical x p = try lookup x p with Not_found -> fresh x p
+
+ let union x y p =
+ let ((x,_) as xcan) = canonical x p in
+ let ((y,_) as ycan) = canonical y p in
+ if x = y then ()
+ else
+ let xcan, ycan = if x < y then xcan, ycan else ycan, xcan in
+ let x,xnode = xcan and y,ynode = ycan in
+ match !xnode, !ynode with
+ | Canon lx, Canon ly ->
+ xnode := Canon (S.union lx ly);
+ ynode := Equiv x;
+ | _ -> assert false
+
+ let union_set s p =
+ try
+ let x = S.min_elt s in
+ S.iter (fun y -> union x y p) s
+ with Not_found -> ()
+
+ let partition p =
+ List.rev (M.fold
+ (fun x node acc -> match !node with
+ | Equiv _ -> acc
+ | Canon lx -> lx::acc)
+ !p [])
+
+end
diff --git a/lib/unionfind.mli b/lib/unionfind.mli
new file mode 100644
index 00000000..07ee7c2b
--- /dev/null
+++ b/lib/unionfind.mli
@@ -0,0 +1,57 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+(** An imperative implementation of partitions via Union-Find *)
+
+(** Paths are compressed imperatively at each lookup of a
+ canonical representative. Each union also modifies in-place
+ the partition structure.
+
+ Nota: for the moment we use Pervasive's comparison for
+ choosing the smallest object as representative. This could
+ be made more generic.
+*)
+
+module type PartitionSig = sig
+
+ (** The type of elements in the partition *)
+ type elt
+
+ (** A set structure over elements *)
+ type set
+
+ (** The type of partitions *)
+ type t
+
+ (** Initialise an empty partition *)
+ val create : unit -> t
+
+ (** Add (in place) an element in the partition, or do nothing
+ if the element is already in the partition. *)
+ val add : elt -> t -> unit
+
+ (** Find the canonical representative of an element.
+ Raise [not_found] if the element isn't known yet. *)
+ val find : elt -> t -> elt
+
+ (** Merge (in place) the equivalence classes of two elements.
+ This will add the elements in the partition if necessary. *)
+ val union : elt -> elt -> t -> unit
+
+ (** Merge (in place) the equivalence classes of many elements. *)
+ val union_set : set -> t -> unit
+
+ (** Listing the different components of the partition *)
+ val partition : t -> set list
+
+end
+
+module Make :
+ functor (S:Set.S) ->
+ functor (M:Map.S with type key = S.elt) ->
+ PartitionSig with type elt = S.elt and type set = S.t
diff --git a/lib/util.ml b/lib/util.ml
index 9a8c724f..287dd371 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -6,9 +6,8 @@
(* * GNU Lesser General Public License Version 2.1 *)
(***********************************************************************)
-(* $Id: util.ml 13492 2010-10-04 21:20:01Z herbelin $ *)
-
open Pp
+open Compat
(* Errors *)
@@ -17,11 +16,9 @@ let anomaly string = raise (Anomaly(string, str string))
let anomalylabstrm string pps = raise (Anomaly(string,pps))
exception UserError of string * std_ppcmds (* User errors *)
-let error string = raise (UserError(string, str string))
+let error string = raise (UserError("_", 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))
@@ -29,17 +26,17 @@ let todo s = prerr_string ("TODO: "^s^"\n")
exception Timeout
-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
+type loc = Loc.t
+let dummy_loc = Loc.ghost
+let join_loc = Loc.merge
+let make_loc = make_loc
+let unloc = unloc
(* 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 anomaly_loc (loc,s,strm) = Loc.raise loc (Anomaly (s,strm))
+let user_err_loc (loc,s,strm) = Loc.raise loc (UserError (s,strm))
+let invalid_arg_loc (loc,s) = Loc.raise loc (Invalid_argument s)
let located_fold_left f x (_,a) = f x a
let located_iter2 f (_,a) (_,b) = f a b
@@ -54,6 +51,7 @@ 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)
+let map_pair f (a,b) = (f a,f b)
(* Mapping under pairs *)
@@ -402,6 +400,13 @@ let rec list_compare cmp l1 l2 =
| 0 -> list_compare cmp l1 l2
| c -> c)
+let rec list_equal cmp l1 l2 =
+ match l1, l2 with
+ | [], [] -> true
+ | x1 :: l1, x2 :: l2 ->
+ cmp x1 x2 && list_equal cmp l1 l2
+ | _ -> false
+
let list_intersect l1 l2 =
List.filter (fun x -> List.mem x l2) l1
@@ -425,24 +430,21 @@ let list_subtract 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 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
- chop_aux [] (n,l)
-
let list_tabulate f len =
let rec tabrec n =
if n = len then [] else (f n)::(tabrec (n+1))
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_addn n v =
+ let rec aux n l =
+ if n = 0 then l
+ else aux (pred n) (v::l)
+ in
+ if n < 0 then invalid_arg "list_addn"
+ else aux n
+
+let list_make n v = list_addn n v []
let list_assign l n e =
let rec assrec stk = function
@@ -497,6 +499,24 @@ let list_map4 f l1 l2 l3 l4 =
in
map (l1,l2,l3,l4)
+let rec list_smartfilter f l = match l with
+ [] -> l
+ | h::tl ->
+ let tl' = list_smartfilter f tl in
+ if f h then
+ if tl' == tl then l
+ else h :: tl'
+ else tl'
+
+let list_index_f f x =
+ let rec index_x n = function
+ | y::l -> if f x y then n else index_x (succ n) l
+ | [] -> raise Not_found
+ in
+ index_x 1
+
+let list_index0_f f x l = list_index_f f x l - 1
+
let list_index x =
let rec index_x n = function
| y::l -> if x = y then n else index_x (succ n) l
@@ -584,6 +604,10 @@ let rec list_remove_assoc_in_triple x = function
| [] -> []
| (y,_,_ as z)::l -> if x = y then l else z::list_remove_assoc_in_triple x l
+let rec list_assoc_snd_in_triple x = function
+ [] -> raise Not_found
+ | (a,b,_)::l -> if compare a x = 0 then b else list_assoc_snd_in_triple x l
+
let list_add_set x l = if List.mem x l then l else x::l
let list_eq_set l1 l2 =
@@ -676,6 +700,14 @@ let rec list_map_filter f = function
let l' = list_map_filter f l in
match f x with None -> l' | Some y -> y::l'
+let list_map_filter_i f =
+ let rec aux i = function
+ | [] -> []
+ | x::l ->
+ let l' = aux (succ i) l in
+ match f i x with None -> l' | Some y -> y::l'
+ in aux 0
+
let list_subset l1 l2 =
let t2 = Hashtbl.create 151 in
List.iter (fun x -> Hashtbl.add t2 x ()) l2;
@@ -685,15 +717,17 @@ let list_subset l1 l2 =
in
look l1
-(* [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_chop 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_chop n l =
+ let rec chop_aux i acc = function
+ | tl when i=0 -> (List.rev acc, tl)
+ | h::t -> chop_aux (pred i) (h::acc) t
+ | [] -> failwith "list_chop"
+ in
+ chop_aux n [] 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].
@@ -757,9 +791,6 @@ let rec list_skipn n l = match n,l with
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 rec prefrec = function
| (h1::t1, h2::t2) -> h1 = h2 && prefrec (t1,t2)
@@ -815,6 +846,10 @@ let list_fold_map' f l e =
let list_map_assoc f = List.map (fun (x,a) -> (x,f a))
+let rec list_assoc_f f a = function
+ | (x, e) :: xs -> if f a x then e else list_assoc_f f a xs
+ | [] -> raise Not_found
+
(* Specification:
- =p= is set equality (double inclusion)
- f such that \forall l acc, (f l acc) =p= append (f l []) acc
@@ -878,6 +913,12 @@ let array_compare item_cmp v1 v2 =
else cmp (i-1) in
cmp (Array.length v1 - 1)
+let array_equal cmp t1 t2 =
+ Array.length t1 = Array.length t2 &&
+ let rec aux i =
+ (i = Array.length t1) || (cmp t1.(i) t2.(i) && aux (i + 1))
+ in aux 0
+
let array_exists f v =
let rec exrec = function
| -1 -> false
@@ -998,6 +1039,15 @@ let array_fold_left2_i f a v1 v2 =
if Array.length v2 <> lv1 then invalid_arg "array_fold_left2";
fold a 0
+let array_fold_left3 f a v1 v2 v3 =
+ let lv1 = Array.length v1 in
+ let rec fold a n =
+ if n >= lv1 then a else fold (f a v1.(n) v2.(n) v3.(n)) (succ n)
+ in
+ if Array.length v2 <> lv1 || Array.length v3 <> lv1 then
+ invalid_arg "array_fold_left2";
+ fold a 0
+
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)
@@ -1167,6 +1217,15 @@ let array_rev_to_list a =
if i >= Array.length a then res else tolist (i+1) (a.(i) :: res) in
tolist 0 []
+(* Stream *)
+
+let stream_nth n st =
+ try List.nth (Stream.npeek (n+1) st) n
+ with Failure _ -> raise Stream.Failure
+
+let stream_njunk n st =
+ for i = 1 to n do Stream.junk st done
+
(* Matrices *)
let matrix_transpose mat =
diff --git a/lib/util.mli b/lib/util.mli
index e5b5f8c6..1fec2295 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -1,21 +1,19 @@
-(***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
-(* \VV/ *************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(***********************************************************************)
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
-(*i $Id: util.mli 13492 2010-10-04 21:20:01Z herbelin $ i*)
-
-(*i*)
open Pp
-(*i*)
+open Compat
-(* This module contains numerous utility functions on strings, lists,
+(** This module contains numerous utility functions on strings, lists,
arrays, etc. *)
-(*s Errors. [Anomaly] is used for system errors and [UserError] for the
+(** {6 ... } *)
+(** Errors. [Anomaly] is used for system errors and [UserError] for the
user's ones. *)
exception Anomaly of string * std_ppcmds
@@ -29,9 +27,7 @@ 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
+(** [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 *)
@@ -39,57 +35,59 @@ val todo : string -> unit
exception Timeout
-type loc = Compat.loc
+type loc = Loc.t
type 'a located = loc * 'a
val unloc : loc -> int * int
val make_loc : int * int -> loc
val dummy_loc : loc
+val join_loc : loc -> loc -> loc
+
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
val down_located : ('a -> 'b) -> 'a located -> 'b
-(* Like [Exc_located], but specifies the outermost file read, the
+(** Like [Exc_located], but specifies the outermost file read, the
input buffer associated to the location of the error (or the module name
if boolean is true), and the error itself. *)
exception Error_in_file of string * (bool * string * loc) * exn
-(* Mapping under pairs *)
+(** Mapping under pairs *)
val on_fst : ('a -> 'b) -> 'a * 'c -> 'b * 'c
val on_snd : ('a -> 'b) -> 'c * 'a -> 'c * 'b
+val map_pair : ('a -> 'b) -> 'a * 'a -> 'b * 'b
-(* Going down pairs *)
+(** Going down pairs *)
val down_fst : ('a -> 'b) -> 'a * 'c -> 'b
val down_snd : ('a -> 'b) -> 'c * 'a -> 'b
-(* Mapping under triple *)
+(** 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 *)
+(** {6 Projections from triplets } *)
val pi1 : 'a * 'b * 'c -> 'a
val pi2 : 'a * 'b * 'c -> 'b
val pi3 : 'a * 'b * 'c -> 'c
-(*s Chars. *)
+(** {6 Chars. } *)
val is_letter : char -> bool
val is_digit : char -> bool
val is_ident_tail : char -> bool
val is_blank : char -> bool
-(*s Strings. *)
+(** {6 Strings. } *)
val explode : string -> string list
val implode : string list -> string
@@ -116,9 +114,10 @@ val check_ident_soft : string -> unit
val lowercase_first_char_utf8 : string -> string
val ascii_of_ident : string -> string
-(*s Lists. *)
+(** {6 Lists. } *)
val list_compare : ('a -> 'a -> int) -> 'a list -> 'a list -> int
+val list_equal : ('a -> 'a -> bool) -> 'a list -> 'a list -> bool
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
@@ -126,8 +125,8 @@ val list_union : 'a list -> 'a list -> 'a list
val list_unionq : 'a list -> 'a list -> 'a list
val list_subtract : 'a list -> 'a list -> 'a list
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)]] *)
+
+(** [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
@@ -135,7 +134,9 @@ 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
+val list_map_filter_i : (int -> '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
val list_map_left : ('a -> 'b) -> 'a list -> 'b list
@@ -148,12 +149,21 @@ 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) *)
+
+(** [list_smartfilter f [a1...an] = List.filter f [a1...an]] but if for all i
+ [f ai = true], then [list_smartfilter f l==l] *)
+val list_smartfilter : ('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_index_f : ('a -> 'a -> bool) -> '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 *)
+
+(** [list_index0] behaves as [list_index] except that it starts counting at 0 *)
val list_index0 : 'a -> 'a list -> int
+val list_index0_f : ('a -> 'a -> bool) -> '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
@@ -166,15 +176,18 @@ val list_except : 'a -> 'a list -> 'a list
val list_remove : 'a -> 'a list -> 'a list
val list_remove_first : 'a -> 'a list -> 'a list
val list_remove_assoc_in_triple : 'a -> ('a * 'b * 'c) list -> ('a * 'b * 'c) list
+val list_assoc_snd_in_triple : 'a -> ('a * 'b * 'c) list -> 'b
val list_for_all2eq : ('a -> 'b -> bool) -> 'a list -> 'b list -> bool
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: *)
+
+(** 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 : int -> 'a list -> 'a list*'a list
+val list_chop : int -> 'a list -> 'a list * 'a list
+(* former [list_split_at] was a duplicate of [list_chop] *)
val list_split_when : ('a -> bool) -> 'a list -> 'a list * 'a list
val list_split_by : ('a -> bool) -> 'a list -> 'a list * 'a list
val list_split3 : ('a * 'b * 'c) list -> 'a list * 'b list * 'c list
@@ -186,28 +199,36 @@ 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] *)
+
+(** [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)] *)
+
+(** [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 *)
+
+(** 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
-(* [list_fold_map f e_0 [l_1...l_n] = e_n,[k_1...k_n]]
+
+(** [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 (**),
+val list_assoc_f : ('a -> 'a -> bool) -> 'a -> ('a * 'b) list -> 'b
+
+(** 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]] *)
+
+(** 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_combine3 : 'a list -> 'b list -> 'c list -> ('a * 'b * 'c) list
@@ -219,9 +240,10 @@ val list_cartesians_filter :
val list_union_map : ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b
-(*s Arrays. *)
+(** {6 Arrays. } *)
val array_compare : ('a -> 'a -> int) -> 'a array -> 'a array -> int
+val array_equal : ('a -> 'a -> bool) -> 'a array -> 'a array -> bool
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
@@ -243,6 +265,8 @@ val array_fold_right2 :
('a -> 'b -> 'c -> 'c) -> 'a array -> 'b array -> 'c -> 'c
val array_fold_left2 :
('a -> 'b -> 'c -> 'a) -> 'a -> 'b array -> 'c array -> 'a
+val array_fold_left3 :
+ ('a -> 'b -> 'c -> 'd -> 'a) -> 'a -> 'b array -> 'c array -> 'd array -> 'a
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
@@ -268,11 +292,16 @@ 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 *)
+(** {6 Streams. } *)
+
+val stream_nth : int -> 'a Stream.t -> 'a
+val stream_njunk : int -> 'a Stream.t -> unit
+
+(** {6 Matrices. } *)
val matrix_transpose : 'a list list -> 'a list list
-(*s Functions. *)
+(** {6 Functions. } *)
val identity : 'a -> 'a
val compose : ('a -> 'b) -> ('c -> 'a) -> 'c -> 'b
@@ -302,12 +331,12 @@ val intmap_inv : 'a Intmap.t -> 'a -> int list
val interval : int -> int -> int list
-(* In [map_succeed f l] an element [a] is removed if [f a] raises *)
-(* [Failure _] otherwise behaves as [List.map f l] *)
+(** In [map_succeed f l] an element [a] is removed if [f a] raises
+ [Failure _] otherwise behaves as [List.map f l] *)
val map_succeed : ('a -> 'b) -> 'a list -> 'b list
-(*s Pretty-printing. *)
+(** {6 Pretty-printing. } *)
val pr_spc : unit -> std_ppcmds
val pr_fnl : unit -> std_ppcmds
@@ -322,7 +351,8 @@ 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
-(* unlike all other functions below, [prlist] works lazily.
+
+(** 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 :
@@ -339,34 +369,36 @@ val pr_located : ('a -> std_ppcmds) -> 'a located -> std_ppcmds
val pr_sequence : ('a -> std_ppcmds) -> 'a list -> std_ppcmds
val surround : std_ppcmds -> std_ppcmds
-(*s Memoization. *)
+(** {6 Memoization. } *)
-(* General comments on memoization:
+(** General comments on memoization:
- cache is created whenever the function is supplied (because of
ML's polymorphic value restriction).
- cache is never flushed (unless the memoized fun is GC'd)
- *)
-(* One cell memory: memorizes only the last call *)
+
+ One cell memory: memorizes only the last call *)
val memo1_1 : ('a -> 'b) -> ('a -> 'b)
val memo1_2 : ('a -> 'b -> 'c) -> ('a -> 'b -> 'c)
-(* with custom equality (used to deal with various arities) *)
+
+(** with custom equality (used to deal with various arities) *)
val memo1_eq : ('a -> 'a -> bool) -> ('a -> 'b) -> ('a -> 'b)
-(* Memorizes the last [n] distinct calls. Efficient only for small [n]. *)
+(** Memorizes the last [n] distinct calls. Efficient only for small [n]. *)
val memon_eq : ('a -> 'a -> bool) -> int -> ('a -> 'b) -> ('a -> 'b)
-(*s Size of an ocaml value (in words, bytes and kilobytes). *)
+(** {6 Size of an ocaml value (in words, bytes and kilobytes). } *)
val size_w : 'a -> int
val size_b : 'a -> int
val size_kb : 'a -> int
-(*s Total size of the allocated ocaml heap. *)
+(** {6 Total size of the allocated ocaml heap. } *)
val heap_size : unit -> int
val heap_size_kb : unit -> int
-(*s Coq interruption: set the following boolean reference to interrupt Coq
+(** {6 ... } *)
+(** Coq interruption: set the following boolean reference to interrupt Coq
(it eventually raises [Break], simulating a Ctrl-C) *)
val interrupt : bool ref
diff --git a/lib/xml_lexer.mli b/lib/xml_lexer.mli
new file mode 100644
index 00000000..a1ca0576
--- /dev/null
+++ b/lib/xml_lexer.mli
@@ -0,0 +1,44 @@
+(*
+ * Xml Light, an small Xml parser/printer with DTD support.
+ * Copyright (C) 2003 Nicolas Cannasse (ncannasse@motion-twin.com)
+ *
+ * This library is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU Lesser General Public
+ * License as published by the Free Software Foundation; either
+ * version 2.1 of the License, or (at your option) any later version.
+ *
+ * This library is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
+ * Lesser General Public License for more details.
+ *
+ * You should have received a copy of the GNU Lesser General Public
+ * License along with this library; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA
+ *)
+
+type error =
+ | EUnterminatedComment
+ | EUnterminatedString
+ | EIdentExpected
+ | ECloseExpected
+ | ENodeExpected
+ | EAttributeNameExpected
+ | EAttributeValueExpected
+ | EUnterminatedEntity
+
+exception Error of error
+
+type token =
+ | Tag of string * (string * string) list * bool
+ | PCData of string
+ | Endtag of string
+ | Eof
+
+type pos = int * int * int * int
+
+val init : Lexing.lexbuf -> unit
+val close : Lexing.lexbuf -> unit
+val token : Lexing.lexbuf -> token
+val pos : Lexing.lexbuf -> pos
+val restore : pos -> unit \ No newline at end of file
diff --git a/lib/xml_lexer.mll b/lib/xml_lexer.mll
new file mode 100644
index 00000000..2be4bf98
--- /dev/null
+++ b/lib/xml_lexer.mll
@@ -0,0 +1,299 @@
+{(*
+ * Xml Light, an small Xml parser/printer with DTD support.
+ * Copyright (C) 2003 Nicolas Cannasse (ncannasse@motion-twin.com)
+ *
+ * This library is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU Lesser General Public
+ * License as published by the Free Software Foundation; either
+ * version 2.1 of the License, or (at your option) any later version.
+ *
+ * This library is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
+ * Lesser General Public License for more details.
+ *
+ * You should have received a copy of the GNU Lesser General Public
+ * License along with this library; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA
+ *)
+
+open Lexing
+
+type error =
+ | EUnterminatedComment
+ | EUnterminatedString
+ | EIdentExpected
+ | ECloseExpected
+ | ENodeExpected
+ | EAttributeNameExpected
+ | EAttributeValueExpected
+ | EUnterminatedEntity
+
+exception Error of error
+
+type pos = int * int * int * int
+
+type token =
+ | Tag of string * (string * string) list * bool
+ | PCData of string
+ | Endtag of string
+ | Eof
+
+let last_pos = ref 0
+and current_line = ref 0
+and current_line_start = ref 0
+
+let tmp = Buffer.create 200
+
+let idents = Hashtbl.create 0
+
+let _ = begin
+ Hashtbl.add idents "gt;" ">";
+ Hashtbl.add idents "lt;" "<";
+ Hashtbl.add idents "amp;" "&";
+ Hashtbl.add idents "apos;" "'";
+ Hashtbl.add idents "quot;" "\"";
+end
+
+let init lexbuf =
+ current_line := 1;
+ current_line_start := lexeme_start lexbuf;
+ last_pos := !current_line_start
+
+let close lexbuf =
+ Buffer.reset tmp
+
+let pos lexbuf =
+ !current_line , !current_line_start ,
+ !last_pos ,
+ lexeme_start lexbuf
+
+let restore (cl,cls,lp,_) =
+ current_line := cl;
+ current_line_start := cls;
+ last_pos := lp
+
+let newline lexbuf =
+ incr current_line;
+ last_pos := lexeme_end lexbuf;
+ current_line_start := !last_pos
+
+let error lexbuf e =
+ last_pos := lexeme_start lexbuf;
+ raise (Error e)
+
+}
+
+let newline = ['\n']
+let break = ['\r']
+let space = [' ' '\t']
+let identchar = ['A'-'Z' 'a'-'z' '_' '0'-'9' ':' '-']
+let entitychar = ['A'-'Z' 'a'-'z']
+let pcchar = [^ '\r' '\n' '<' '>' '&']
+
+rule token = parse
+ | newline | (newline break) | break
+ {
+ newline lexbuf;
+ PCData "\n"
+ }
+ | "<!--"
+ {
+ last_pos := lexeme_start lexbuf;
+ comment lexbuf;
+ token lexbuf
+ }
+ | "<?"
+ {
+ last_pos := lexeme_start lexbuf;
+ header lexbuf;
+ token lexbuf;
+ }
+ | '<' space* '/' space*
+ {
+ last_pos := lexeme_start lexbuf;
+ let tag = ident_name lexbuf in
+ ignore_spaces lexbuf;
+ close_tag lexbuf;
+ Endtag tag
+ }
+ | '<' space*
+ {
+ last_pos := lexeme_start lexbuf;
+ let tag = ident_name lexbuf in
+ ignore_spaces lexbuf;
+ let attribs, closed = attributes lexbuf in
+ Tag(tag, attribs, closed)
+ }
+ | "&#"
+ {
+ last_pos := lexeme_start lexbuf;
+ Buffer.reset tmp;
+ Buffer.add_string tmp (lexeme lexbuf);
+ PCData (pcdata lexbuf)
+ }
+ | '&'
+ {
+ last_pos := lexeme_start lexbuf;
+ Buffer.reset tmp;
+ Buffer.add_string tmp (entity lexbuf);
+ PCData (pcdata lexbuf)
+ }
+ | pcchar+
+ {
+ last_pos := lexeme_start lexbuf;
+ Buffer.reset tmp;
+ Buffer.add_string tmp (lexeme lexbuf);
+ PCData (pcdata lexbuf)
+ }
+ | eof { Eof }
+ | _
+ { error lexbuf ENodeExpected }
+
+and ignore_spaces = parse
+ | newline | (newline break) | break
+ {
+ newline lexbuf;
+ ignore_spaces lexbuf
+ }
+ | space +
+ { ignore_spaces lexbuf }
+ | ""
+ { () }
+
+and comment = parse
+ | newline | (newline break) | break
+ {
+ newline lexbuf;
+ comment lexbuf
+ }
+ | "-->"
+ { () }
+ | eof
+ { raise (Error EUnterminatedComment) }
+ | _
+ { comment lexbuf }
+
+and header = parse
+ | newline | (newline break) | break
+ {
+ newline lexbuf;
+ header lexbuf
+ }
+ | "?>"
+ { () }
+ | eof
+ { error lexbuf ECloseExpected }
+ | _
+ { header lexbuf }
+
+and pcdata = parse
+ | pcchar+
+ {
+ Buffer.add_string tmp (lexeme lexbuf);
+ pcdata lexbuf
+ }
+ | "&#"
+ {
+ Buffer.add_string tmp (lexeme lexbuf);
+ pcdata lexbuf;
+ }
+ | '&'
+ {
+ Buffer.add_string tmp (entity lexbuf);
+ pcdata lexbuf
+ }
+ | ""
+ { Buffer.contents tmp }
+
+and entity = parse
+ | entitychar+ ';'
+ {
+ let ident = lexeme lexbuf in
+ try
+ Hashtbl.find idents (String.lowercase ident)
+ with
+ Not_found -> "&" ^ ident
+ }
+ | _ | eof
+ { raise (Error EUnterminatedEntity) }
+
+and ident_name = parse
+ | identchar+
+ { lexeme lexbuf }
+ | _ | eof
+ { error lexbuf EIdentExpected }
+
+and close_tag = parse
+ | '>'
+ { () }
+ | _ | eof
+ { error lexbuf ECloseExpected }
+
+and attributes = parse
+ | '>'
+ { [], false }
+ | "/>"
+ { [], true }
+ | "" (* do not read a char ! *)
+ {
+ let key = attribute lexbuf in
+ let data = attribute_data lexbuf in
+ ignore_spaces lexbuf;
+ let others, closed = attributes lexbuf in
+ (key, data) :: others, closed
+ }
+
+and attribute = parse
+ | identchar+
+ { lexeme lexbuf }
+ | _ | eof
+ { error lexbuf EAttributeNameExpected }
+
+and attribute_data = parse
+ | space* '=' space* '"'
+ {
+ Buffer.reset tmp;
+ last_pos := lexeme_end lexbuf;
+ dq_string lexbuf
+ }
+ | space* '=' space* '\''
+ {
+ Buffer.reset tmp;
+ last_pos := lexeme_end lexbuf;
+ q_string lexbuf
+ }
+ | _ | eof
+ { error lexbuf EAttributeValueExpected }
+
+and dq_string = parse
+ | '"'
+ { Buffer.contents tmp }
+ | '\\' [ '"' '\\' ]
+ {
+ Buffer.add_char tmp (lexeme_char lexbuf 1);
+ dq_string lexbuf
+ }
+ | eof
+ { raise (Error EUnterminatedString) }
+ | _
+ {
+ Buffer.add_char tmp (lexeme_char lexbuf 0);
+ dq_string lexbuf
+ }
+
+and q_string = parse
+ | '\''
+ { Buffer.contents tmp }
+ | '\\' [ '\'' '\\' ]
+ {
+ Buffer.add_char tmp (lexeme_char lexbuf 1);
+ q_string lexbuf
+ }
+ | eof
+ { raise (Error EUnterminatedString) }
+ | _
+ {
+ Buffer.add_char tmp (lexeme_char lexbuf 0);
+ q_string lexbuf
+ }
diff --git a/lib/xml_parser.ml b/lib/xml_parser.ml
new file mode 100644
index 00000000..bf931d75
--- /dev/null
+++ b/lib/xml_parser.ml
@@ -0,0 +1,238 @@
+(*
+ * Xml Light, an small Xml parser/printer with DTD support.
+ * Copyright (C) 2003 Nicolas Cannasse (ncannasse@motion-twin.com)
+ * Copyright (C) 2003 Jacques Garrigue
+ *
+ * This library is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU Lesser General Public
+ * License as published by the Free Software Foundation; either
+ * version 2.1 of the License, or (at your option) any later version.
+ *
+ * This library is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
+ * Lesser General Public License for more details.
+ *
+ * You should have received a copy of the GNU Lesser General Public
+ * License along with this library; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA
+ *)
+
+open Printf
+
+type xml =
+ | Element of (string * (string * string) list * xml list)
+ | PCData of string
+
+type error_pos = {
+ eline : int;
+ eline_start : int;
+ emin : int;
+ emax : int;
+}
+
+type error_msg =
+ | UnterminatedComment
+ | UnterminatedString
+ | UnterminatedEntity
+ | IdentExpected
+ | CloseExpected
+ | NodeExpected
+ | AttributeNameExpected
+ | AttributeValueExpected
+ | EndOfTagExpected of string
+ | EOFExpected
+
+type error = error_msg * error_pos
+
+exception Error of error
+
+exception File_not_found of string
+
+type t = {
+ mutable check_eof : bool;
+ mutable concat_pcdata : bool;
+}
+
+type source =
+ | SFile of string
+ | SChannel of in_channel
+ | SString of string
+ | SLexbuf of Lexing.lexbuf
+
+type state = {
+ source : Lexing.lexbuf;
+ stack : Xml_lexer.token Stack.t;
+ xparser : t;
+}
+
+exception Internal_error of error_msg
+exception NoMoreData
+
+let xml_error = ref (fun _ -> assert false)
+let file_not_found = ref (fun _ -> assert false)
+
+let is_blank s =
+ let len = String.length s in
+ let break = ref true in
+ let i = ref 0 in
+ while !break && !i < len do
+ let c = s.[!i] in
+ (* no '\r' because we replaced them in the lexer *)
+ if c = ' ' || c = '\n' || c = '\t' then incr i
+ else break := false
+ done;
+ !i = len
+
+let _raises e f =
+ xml_error := e;
+ file_not_found := f
+
+let make () =
+ {
+ check_eof = true;
+ concat_pcdata = true;
+ }
+
+let check_eof p v = p.check_eof <- v
+let concat_pcdata p v = p.concat_pcdata <- v
+
+let pop s =
+ try
+ Stack.pop s.stack
+ with
+ Stack.Empty ->
+ Xml_lexer.token s.source
+
+let push t s =
+ Stack.push t s.stack
+
+let canonicalize l =
+ let has_elt = List.exists (function Element _ -> true | _ -> false) l in
+ if has_elt then List.filter (function PCData s -> not (is_blank s) | _ -> true) l
+ else l
+
+let rec read_node s =
+ match pop s with
+ | Xml_lexer.PCData s -> PCData s
+ | Xml_lexer.Tag (tag, attr, true) -> Element (tag, attr, [])
+ | Xml_lexer.Tag (tag, attr, false) ->
+ let elements = read_elems ~tag s in
+ Element (tag, attr, canonicalize elements)
+ | t ->
+ push t s;
+ raise NoMoreData
+and
+ read_elems ?tag s =
+ let elems = ref [] in
+ (try
+ while true do
+ let node = read_node s in
+ match node, !elems with
+ | PCData c , (PCData c2) :: q ->
+ elems := PCData (c2 ^ c) :: q
+ | _, l ->
+ elems := node :: l
+ done
+ with
+ NoMoreData -> ());
+ match pop s with
+ | Xml_lexer.Endtag s when Some s = tag -> List.rev !elems
+ | Xml_lexer.Eof when tag = None -> List.rev !elems
+ | t ->
+ match tag with
+ | None -> raise (Internal_error EOFExpected)
+ | Some s -> raise (Internal_error (EndOfTagExpected s))
+
+let rec read_xml s =
+ let node = read_node s in
+ match node with
+ | Element _ -> node
+ | PCData c ->
+ if is_blank c then read_xml s
+ else raise (Xml_lexer.Error Xml_lexer.ENodeExpected)
+
+let convert = function
+ | Xml_lexer.EUnterminatedComment -> UnterminatedComment
+ | Xml_lexer.EUnterminatedString -> UnterminatedString
+ | Xml_lexer.EIdentExpected -> IdentExpected
+ | Xml_lexer.ECloseExpected -> CloseExpected
+ | Xml_lexer.ENodeExpected -> NodeExpected
+ | Xml_lexer.EAttributeNameExpected -> AttributeNameExpected
+ | Xml_lexer.EAttributeValueExpected -> AttributeValueExpected
+ | Xml_lexer.EUnterminatedEntity -> UnterminatedEntity
+
+let do_parse xparser source =
+ try
+ Xml_lexer.init source;
+ let s = { source = source; xparser = xparser; stack = Stack.create(); } in
+ let x = read_xml s in
+ if xparser.check_eof && pop s <> Xml_lexer.Eof then raise (Internal_error EOFExpected);
+ Xml_lexer.close source;
+ x
+ with
+ | NoMoreData ->
+ Xml_lexer.close source;
+ raise (!xml_error NodeExpected source)
+ | Internal_error e ->
+ Xml_lexer.close source;
+ raise (!xml_error e source)
+ | Xml_lexer.Error e ->
+ Xml_lexer.close source;
+ raise (!xml_error (convert e) source)
+
+let parse p = function
+ | SChannel ch -> do_parse p (Lexing.from_channel ch)
+ | SString str -> do_parse p (Lexing.from_string str)
+ | SLexbuf lex -> do_parse p lex
+ | SFile fname ->
+ let ch = (try open_in fname with Sys_error _ -> raise (!file_not_found fname)) in
+ try
+ let x = do_parse p (Lexing.from_channel ch) in
+ close_in ch;
+ x
+ with
+ e ->
+ close_in ch;
+ raise e
+
+
+let error_msg = function
+ | UnterminatedComment -> "Unterminated comment"
+ | UnterminatedString -> "Unterminated string"
+ | UnterminatedEntity -> "Unterminated entity"
+ | IdentExpected -> "Ident expected"
+ | CloseExpected -> "Element close expected"
+ | NodeExpected -> "Xml node expected"
+ | AttributeNameExpected -> "Attribute name expected"
+ | AttributeValueExpected -> "Attribute value expected"
+ | EndOfTagExpected tag -> sprintf "End of tag expected : '%s'" tag
+ | EOFExpected -> "End of file expected"
+
+let error (msg,pos) =
+ if pos.emin = pos.emax then
+ sprintf "%s line %d character %d" (error_msg msg) pos.eline (pos.emin - pos.eline_start)
+ else
+ sprintf "%s line %d characters %d-%d" (error_msg msg) pos.eline (pos.emin - pos.eline_start) (pos.emax - pos.eline_start)
+
+let line e = e.eline
+
+let range e =
+ e.emin - e.eline_start , e.emax - e.eline_start
+
+let abs_range e =
+ e.emin , e.emax
+
+let pos source =
+ let line, lstart, min, max = Xml_lexer.pos source in
+ {
+ eline = line;
+ eline_start = lstart;
+ emin = min;
+ emax = max;
+ }
+
+let () = _raises (fun x p ->
+ (* local cast : Xml.error_msg -> error_msg *)
+ Error (x, pos p))
+ (fun f -> File_not_found f)
diff --git a/lib/xml_parser.mli b/lib/xml_parser.mli
new file mode 100644
index 00000000..a3e8aa4a
--- /dev/null
+++ b/lib/xml_parser.mli
@@ -0,0 +1,104 @@
+(*
+ * Xml Light, an small Xml parser/printer with DTD support.
+ * Copyright (C) 2003 Nicolas Cannasse (ncannasse@motion-twin.com)
+ *
+ * This library is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU Lesser General Public
+ * License as published by the Free Software Foundation; either
+ * version 2.1 of the License, or (at your option) any later version.
+ *
+ * This library is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
+ * Lesser General Public License for more details.
+ *
+ * You should have received a copy of the GNU Lesser General Public
+ * License along with this library; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA
+ *)
+
+(** Xml Light Parser
+
+ While basic parsing functions can be used in the {!Xml} module, this module
+ is providing a way to create, configure and run an Xml parser.
+
+*)
+
+
+(** An Xml node is either
+ [Element (tag-name, attributes, children)] or [PCData text] *)
+type xml =
+ | Element of (string * (string * string) list * xml list)
+ | PCData of string
+
+(** Abstract type for an Xml parser. *)
+type t
+
+(** {6:exc Xml Exceptions} *)
+
+(** Several exceptions can be raised when parsing an Xml document : {ul
+ {li {!Xml.Error} is raised when an xml parsing error occurs. the
+ {!Xml.error_msg} tells you which error occured during parsing
+ and the {!Xml.error_pos} can be used to retreive the document
+ location where the error occured at.}
+ {li {!Xml.File_not_found} is raised when and error occured while
+ opening a file with the {!Xml.parse_file} function.
+ }
+ *)
+
+type error_pos
+
+type error_msg =
+ | UnterminatedComment
+ | UnterminatedString
+ | UnterminatedEntity
+ | IdentExpected
+ | CloseExpected
+ | NodeExpected
+ | AttributeNameExpected
+ | AttributeValueExpected
+ | EndOfTagExpected of string
+ | EOFExpected
+
+type error = error_msg * error_pos
+
+exception Error of error
+
+exception File_not_found of string
+
+(** Get a full error message from an Xml error. *)
+val error : error -> string
+
+(** Get the Xml error message as a string. *)
+val error_msg : error_msg -> string
+
+(** Get the line the error occured at. *)
+val line : error_pos -> int
+
+(** Get the relative character range (in current line) the error occured at.*)
+val range : error_pos -> int * int
+
+(** Get the absolute character range the error occured at. *)
+val abs_range : error_pos -> int * int
+
+val pos : Lexing.lexbuf -> error_pos
+
+(** Several kind of resources can contain Xml documents. *)
+type source =
+ | SFile of string
+ | SChannel of in_channel
+ | SString of string
+ | SLexbuf of Lexing.lexbuf
+
+(** This function returns a new parser with default options. *)
+val make : unit -> t
+
+(** When a Xml document is parsed, the parser will check that the end of the
+ document is reached, so for example parsing ["<A/><B/>"] will fail instead
+ of returning only the A element. You can turn off this check by setting
+ [check_eof] to [false] {i (by default, check_eof is true)}. *)
+val check_eof : t -> bool -> unit
+
+(** Once the parser is configurated, you can run the parser on a any kind
+ of xml document source to parse its contents into an Xml data structure. *)
+val parse : t -> source -> xml
diff --git a/lib/xml_utils.ml b/lib/xml_utils.ml
new file mode 100644
index 00000000..31003586
--- /dev/null
+++ b/lib/xml_utils.ml
@@ -0,0 +1,223 @@
+(*
+ * Xml Light, an small Xml parser/printer with DTD support.
+ * Copyright (C) 2003 Nicolas Cannasse (ncannasse@motion-twin.com)
+ *
+ * This library is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU Lesser General Public
+ * License as published by the Free Software Foundation; either
+ * version 2.1 of the License, or (at your option) any later version.
+ *
+ * This library is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
+ * Lesser General Public License for more details.
+ *
+ * You should have received a copy of the GNU Lesser General Public
+ * License along with this library; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA
+ *)
+
+open Printf
+open Xml_parser
+
+exception Not_element of xml
+exception Not_pcdata of xml
+exception No_attribute of string
+
+let default_parser = Xml_parser.make()
+
+let parse (p:Xml_parser.t) (source:Xml_parser.source) =
+ (* local cast Xml.xml -> xml *)
+ (Obj.magic Xml_parser.parse p source : xml)
+
+let parse_in ch = parse default_parser (Xml_parser.SChannel ch)
+let parse_string str = parse default_parser (Xml_parser.SString str)
+
+let parse_file f = parse default_parser (Xml_parser.SFile f)
+
+let tag = function
+ | Element (tag,_,_) -> tag
+ | x -> raise (Not_element x)
+
+let pcdata = function
+ | PCData text -> text
+ | x -> raise (Not_pcdata x)
+
+let attribs = function
+ | Element (_,attr,_) -> attr
+ | x -> raise (Not_element x)
+
+let attrib x att =
+ match x with
+ | Element (_,attr,_) ->
+ (try
+ let att = String.lowercase att in
+ snd (List.find (fun (n,_) -> String.lowercase n = att) attr)
+ with
+ Not_found ->
+ raise (No_attribute att))
+ | x ->
+ raise (Not_element x)
+
+let children = function
+ | Element (_,_,clist) -> clist
+ | x -> raise (Not_element x)
+
+(*let enum = function
+ | Element (_,_,clist) -> List.to_enum clist
+ | x -> raise (Not_element x)
+*)
+
+let iter f = function
+ | Element (_,_,clist) -> List.iter f clist
+ | x -> raise (Not_element x)
+
+let map f = function
+ | Element (_,_,clist) -> List.map f clist
+ | x -> raise (Not_element x)
+
+let fold f v = function
+ | Element (_,_,clist) -> List.fold_left f v clist
+ | x -> raise (Not_element x)
+
+let tmp = Buffer.create 200
+
+let buffer_pcdata text =
+ let l = String.length text in
+ for p = 0 to l-1 do
+ match text.[p] with
+ | '>' -> Buffer.add_string tmp "&gt;"
+ | '<' -> Buffer.add_string tmp "&lt;"
+ | '&' ->
+ if p < l-1 && text.[p+1] = '#' then
+ Buffer.add_char tmp '&'
+ else
+ Buffer.add_string tmp "&amp;"
+ | '\'' -> Buffer.add_string tmp "&apos;"
+ | '"' -> Buffer.add_string tmp "&quot;"
+ | c -> Buffer.add_char tmp c
+ done
+
+let print_pcdata chan text =
+ let l = String.length text in
+ for p = 0 to l-1 do
+ match text.[p] with
+ | '>' -> Printf.fprintf chan "&gt;"
+ | '<' -> Printf.fprintf chan "&lt;"
+ | '&' ->
+ if p < l-1 && text.[p+1] = '#' then
+ Printf.fprintf chan "&"
+ else
+ Printf.fprintf chan "&amp;"
+ | '\'' -> Printf.fprintf chan "&apos;"
+ | '"' -> Printf.fprintf chan "&quot;"
+ | c -> Printf.fprintf chan "%c" c
+ done
+
+let buffer_attr (n,v) =
+ Buffer.add_char tmp ' ';
+ Buffer.add_string tmp n;
+ Buffer.add_string tmp "=\"";
+ let l = String.length v in
+ for p = 0 to l-1 do
+ match v.[p] with
+ | '\\' -> Buffer.add_string tmp "\\\\"
+ | '"' -> Buffer.add_string tmp "\\\""
+ | c -> Buffer.add_char tmp c
+ done;
+ Buffer.add_char tmp '"'
+
+let rec print_attr chan (n, v) =
+ Printf.fprintf chan " %s=\"" n;
+ let l = String.length v in
+ for p = 0 to l-1 do
+ match v.[p] with
+ | '\\' -> Printf.fprintf chan "\\\\"
+ | '"' -> Printf.fprintf chan "\\\""
+ | c -> Printf.fprintf chan "%c" c
+ done;
+ Printf.fprintf chan "\""
+
+let print_attrs chan l = List.iter (print_attr chan) l
+
+let rec print_xml chan = function
+| Element (tag, alist, []) ->
+ Printf.fprintf chan "<%s%a/>" tag print_attrs alist;
+| Element (tag, alist, l) ->
+ Printf.fprintf chan "<%s%a>%a</%s>" tag print_attrs alist
+ (fun chan -> List.iter (print_xml chan)) l tag
+| PCData text ->
+ print_pcdata chan text
+
+let to_string x =
+ let pcdata = ref false in
+ let rec loop = function
+ | Element (tag,alist,[]) ->
+ Buffer.add_char tmp '<';
+ Buffer.add_string tmp tag;
+ List.iter buffer_attr alist;
+ Buffer.add_string tmp "/>";
+ pcdata := false;
+ | Element (tag,alist,l) ->
+ Buffer.add_char tmp '<';
+ Buffer.add_string tmp tag;
+ List.iter buffer_attr alist;
+ Buffer.add_char tmp '>';
+ pcdata := false;
+ List.iter loop l;
+ Buffer.add_string tmp "</";
+ Buffer.add_string tmp tag;
+ Buffer.add_char tmp '>';
+ pcdata := false;
+ | PCData text ->
+ if !pcdata then Buffer.add_char tmp ' ';
+ buffer_pcdata text;
+ pcdata := true;
+ in
+ Buffer.reset tmp;
+ loop x;
+ let s = Buffer.contents tmp in
+ Buffer.reset tmp;
+ s
+
+let to_string_fmt x =
+ let rec loop ?(newl=false) tab = function
+ | Element (tag,alist,[]) ->
+ Buffer.add_string tmp tab;
+ Buffer.add_char tmp '<';
+ Buffer.add_string tmp tag;
+ List.iter buffer_attr alist;
+ Buffer.add_string tmp "/>";
+ if newl then Buffer.add_char tmp '\n';
+ | Element (tag,alist,[PCData text]) ->
+ Buffer.add_string tmp tab;
+ Buffer.add_char tmp '<';
+ Buffer.add_string tmp tag;
+ List.iter buffer_attr alist;
+ Buffer.add_string tmp ">";
+ buffer_pcdata text;
+ Buffer.add_string tmp "</";
+ Buffer.add_string tmp tag;
+ Buffer.add_char tmp '>';
+ if newl then Buffer.add_char tmp '\n';
+ | Element (tag,alist,l) ->
+ Buffer.add_string tmp tab;
+ Buffer.add_char tmp '<';
+ Buffer.add_string tmp tag;
+ List.iter buffer_attr alist;
+ Buffer.add_string tmp ">\n";
+ List.iter (loop ~newl:true (tab^" ")) l;
+ Buffer.add_string tmp tab;
+ Buffer.add_string tmp "</";
+ Buffer.add_string tmp tag;
+ Buffer.add_char tmp '>';
+ if newl then Buffer.add_char tmp '\n';
+ | PCData text ->
+ buffer_pcdata text;
+ if newl then Buffer.add_char tmp '\n';
+ in
+ Buffer.reset tmp;
+ loop "" x;
+ let s = Buffer.contents tmp in
+ Buffer.reset tmp;
+ s
diff --git a/lib/xml_utils.mli b/lib/xml_utils.mli
new file mode 100644
index 00000000..4a4a1309
--- /dev/null
+++ b/lib/xml_utils.mli
@@ -0,0 +1,93 @@
+(*
+ * Xml Light, an small Xml parser/printer with DTD support.
+ * Copyright (C) 2003 Nicolas Cannasse (ncannasse@motion-twin.com)
+ *
+ * This library is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU Lesser General Public
+ * License as published by the Free Software Foundation; either
+ * version 2.1 of the License, or (at your option) any later version.
+ *
+ * This library is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
+ * Lesser General Public License for more details.
+ *
+ * You should have received a copy of the GNU Lesser General Public
+ * License along with this library; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA
+ *)
+
+(** Xml Light
+
+ Xml Light is a minimal Xml parser & printer for OCaml.
+ It provide few functions to parse a basic Xml document into
+ an OCaml data structure and to print back the data structures
+ to an Xml document.
+
+ Xml Light has also support for {b DTD} (Document Type Definition).
+
+ {i (c)Copyright 2002-2003 Nicolas Cannasse}
+*)
+
+open Xml_parser
+
+(** {6 Xml Functions} *)
+
+exception Not_element of xml
+exception Not_pcdata of xml
+exception No_attribute of string
+
+(** [tag xdata] returns the tag value of the xml node.
+ Raise {!Xml.Not_element} if the xml is not an element *)
+val tag : xml -> string
+
+(** [pcdata xdata] returns the PCData value of the xml node.
+ Raise {!Xml.Not_pcdata} if the xml is not a PCData *)
+val pcdata : xml -> string
+
+(** [attribs xdata] returns the attribute list of the xml node.
+ First string if the attribute name, second string is attribute value.
+ Raise {!Xml.Not_element} if the xml is not an element *)
+val attribs : xml -> (string * string) list
+
+(** [attrib xdata "href"] returns the value of the ["href"]
+ attribute of the xml node (attribute matching is case-insensitive).
+ Raise {!Xml.No_attribute} if the attribute does not exists in the node's
+ attribute list
+ Raise {!Xml.Not_element} if the xml is not an element *)
+val attrib : xml -> string -> string
+
+(** [children xdata] returns the children list of the xml node
+ Raise {!Xml.Not_element} if the xml is not an element *)
+val children : xml -> xml list
+
+(*** [enum xdata] returns the children enumeration of the xml node
+ Raise {!Xml.Not_element} if the xml is not an element *)
+(* val enum : xml -> xml Enum.t *)
+
+(** [iter f xdata] calls f on all children of the xml node.
+ Raise {!Xml.Not_element} if the xml is not an element *)
+val iter : (xml -> unit) -> xml -> unit
+
+(** [map f xdata] is equivalent to [List.map f (Xml.children xdata)]
+ Raise {!Xml.Not_element} if the xml is not an element *)
+val map : (xml -> 'a) -> xml -> 'a list
+
+(** [fold f init xdata] is equivalent to
+ [List.fold_left f init (Xml.children xdata)]
+ Raise {!Xml.Not_element} if the xml is not an element *)
+val fold : ('a -> xml -> 'a) -> 'a -> xml -> 'a
+
+(** {6 Xml Printing} *)
+
+(** Print the xml data structure to a channel into a compact xml string (without
+ any user-readable formating ). *)
+val print_xml : out_channel -> xml -> unit
+
+(** Print the xml data structure into a compact xml string (without
+ any user-readable formating ). *)
+val to_string : xml -> string
+
+(** Print the xml data structure into an user-readable string with
+ tabs and lines break between different nodes. *)
+val to_string_fmt : xml -> string