diff options
author | 2012-01-12 16:08:29 +0100 | |
---|---|---|
committer | 2012-01-12 16:08:29 +0100 | |
commit | 23a6061a81ffa0c214d521287b6af0a31bfa22f0 (patch) | |
tree | f1ca9ba9240b98b8695a9f1870e56602734cf97c /lib | |
parent | de109d8c0c68f569b907e6e24271f259ba28888e (diff) | |
parent | 39efc41237ec906226a3a53d7396d51173495204 (diff) |
Merge commit 'upstream/8.4_beta+dfsg' into experimental/master
Diffstat (limited to 'lib')
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 @@ -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. @@ -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 () @@ -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 ">" + | '<' -> Buffer.add_string tmp "<" + | '&' -> + if p < l-1 && text.[p+1] = '#' then + Buffer.add_char tmp '&' + else + Buffer.add_string tmp "&" + | '\'' -> Buffer.add_string tmp "'" + | '"' -> Buffer.add_string tmp """ + | 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 ">" + | '<' -> Printf.fprintf chan "<" + | '&' -> + if p < l-1 && text.[p+1] = '#' then + Printf.fprintf chan "&" + else + Printf.fprintf chan "&" + | '\'' -> Printf.fprintf chan "'" + | '"' -> Printf.fprintf chan """ + | 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 |