diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/bstack.ml | 75 | ||||
| -rw-r--r-- | lib/bstack.mli | 22 | ||||
| -rw-r--r-- | lib/edit.ml | 134 | ||||
| -rw-r--r-- | lib/edit.mli | 63 | ||||
| -rw-r--r-- | lib/lib.mllib | 4 | ||||
| -rw-r--r-- | lib/store.ml | 63 | ||||
| -rw-r--r-- | lib/store.mli | 27 |
7 files changed, 91 insertions, 297 deletions
diff --git a/lib/bstack.ml b/lib/bstack.ml deleted file mode 100644 index 4191ccdb15..0000000000 --- a/lib/bstack.ml +++ /dev/null @@ -1,75 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(* $Id$ *) - -(* 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 cef8e1d9e5..0000000000 --- a/lib/bstack.mli +++ /dev/null @@ -1,22 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(*i $Id$ 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/edit.ml b/lib/edit.ml deleted file mode 100644 index fd870a21ba..0000000000 --- a/lib/edit.ml +++ /dev/null @@ -1,134 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(* $Id$ *) - -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 d13d9c6f69..0000000000 --- a/lib/edit.mli +++ /dev/null @@ -1,63 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(*i $Id$ 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/lib.mllib b/lib/lib.mllib index 1743ce26ca..86d29c4be6 100644 --- a/lib/lib.mllib +++ b/lib/lib.mllib @@ -10,8 +10,6 @@ Hashcons Dyn System Envars -Bstack -Edit Gset Gmap Fset @@ -26,4 +24,4 @@ Rtree Heap Option Dnet - +Store diff --git a/lib/store.ml b/lib/store.ml new file mode 100644 index 0000000000..8f1309531e --- /dev/null +++ b/lib/store.ml @@ -0,0 +1,63 @@ +(***********************************************************************) +(* 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 *) +(***********************************************************************) + +(* $Id$ *) + +(*** 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 0000000000..0caeb2abba --- /dev/null +++ b/lib/store.mli @@ -0,0 +1,27 @@ +(***********************************************************************) +(* 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 *) +(***********************************************************************) + +(* $Id$ *) + +(*** 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 |