diff options
author | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-09-06 17:18:44 +0000 |
---|---|---|
committer | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-09-06 17:18:44 +0000 |
commit | ba524ddfaabc80b31a439544de46c40366565ae8 (patch) | |
tree | ff4350bc4ec7e225be1b6f9eeb5af83b45ab7f36 | |
parent | ab7377de0a913ca6218bc7377fab33b8018f8f59 (diff) |
Moving Searchstack to CStack, and normalizing names a bit.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16765 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r-- | Makefile.common | 2 | ||||
-rw-r--r-- | checker/check.mllib | 1 | ||||
-rw-r--r-- | dev/printers.mllib | 1 | ||||
-rw-r--r-- | grammar/grammar.mllib | 1 | ||||
-rw-r--r-- | ide/coqOps.ml | 47 | ||||
-rw-r--r-- | lib/cSig.mli (renamed from lib/searchstack.mli) | 20 | ||||
-rw-r--r-- | lib/cStack.ml (renamed from lib/searchstack.ml) | 20 | ||||
-rw-r--r-- | lib/cStack.mli | 58 | ||||
-rw-r--r-- | lib/clib.mllib | 1 | ||||
-rw-r--r-- | lib/lib.mllib | 1 | ||||
-rw-r--r-- | lib/util.ml | 7 | ||||
-rw-r--r-- | lib/util.mli | 10 | ||||
-rw-r--r-- | toplevel/stm.ml | 31 |
13 files changed, 137 insertions, 63 deletions
diff --git a/Makefile.common b/Makefile.common index 1845f7164..8aaf8fceb 100644 --- a/Makefile.common +++ b/Makefile.common @@ -208,7 +208,7 @@ endif LINKCMO:=$(CORECMA) $(STATICPLUGINS) LINKCMX:=$(CORECMA:.cma=.cmxa) $(STATICPLUGINS:.cma=.cmxa) -IDEDEPS:=lib/clib.cma lib/xml_lexer.cmo lib/xml_parser.cmo lib/xml_printer.cmo lib/searchstack.cmo +IDEDEPS:=lib/clib.cma lib/xml_lexer.cmo lib/xml_parser.cmo lib/xml_printer.cmo IDECMA:=ide/ide.cma LINKIDE:=$(IDEDEPS) $(IDECMA) ide/coqide_main.ml diff --git a/checker/check.mllib b/checker/check.mllib index 31d2e005f..759be8729 100644 --- a/checker/check.mllib +++ b/checker/check.mllib @@ -21,6 +21,7 @@ CObj CList CString CArray +CStack Util Future CUnix diff --git a/dev/printers.mllib b/dev/printers.mllib index 090536cc3..8e99b5247 100644 --- a/dev/printers.mllib +++ b/dev/printers.mllib @@ -23,6 +23,7 @@ CObj CList CString CArray +CStack Util Bigint Dyn diff --git a/grammar/grammar.mllib b/grammar/grammar.mllib index b1eb01f4f..50c1cfa6a 100644 --- a/grammar/grammar.mllib +++ b/grammar/grammar.mllib @@ -18,6 +18,7 @@ Hashcons CList CString CArray +CStack Util Bigint Predicate diff --git a/ide/coqOps.ml b/ide/coqOps.ml index 1ca949b52..cb90c0ff0 100644 --- a/ide/coqOps.ml +++ b/ide/coqOps.ml @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Util open Coq open Ideutils open Interface @@ -100,7 +101,7 @@ object(self) val proof = _pv val messages = _mv - val cmd_stack = Searchstack.create () + val cmd_stack = Stack.create () val mutable initial_state = Stateid.initial @@ -232,12 +233,12 @@ object(self) let msg = Queue.pop feedbacks in let id = msg.id in let sentence = - let finder () s = + let finder s = match s.state_id, id with - | Some id', State id when id = id' -> `Stop s - | _, Edit id when id = s.edit_id -> `Stop s - | _ -> `Cont () in - try Some (Searchstack.find finder () cmd_stack) + | Some id', State id when id = id' -> Some s + | _, Edit id when id = s.edit_id -> Some s + | _ -> None in + try Some (Stack.find_map finder cmd_stack) with Not_found -> None in let log s sentence = Minilib.log ("Feedback " ^ s ^ " on " ^ Stateid.to_string @@ -268,9 +269,9 @@ object(self) self#position_error_tag_at_sentence sentence (Some (Loc.unloc loc)) | _ -> if sentence <> None then Minilib.log "Unsupported feedback message" - else if Searchstack.is_empty cmd_stack then () + else if Stack.is_empty cmd_stack then () else - match id, (Searchstack.top cmd_stack).state_id with + match id, (Stack.top cmd_stack).state_id with | Edit _, _ -> () | State id1, Some id2 when Stateid.newer_than id2 id1 -> () | _ -> Queue.add msg feedbacks (* Put back into the queue *) @@ -341,7 +342,7 @@ object(self) else let sentence = Queue.pop queue in add_flag sentence `PROCESSING; - Searchstack.push sentence cmd_stack; + Stack.push sentence cmd_stack; if List.mem `COMMENT sentence.flags then let () = remove_flag sentence `PROCESSING in let () = self#commit_queue_transaction sentence in @@ -361,7 +362,7 @@ object(self) assign_state_id sentence id; commit_and_continue msg | Fail (id, loc, msg) -> - let sentence = Searchstack.pop cmd_stack in + let sentence = Stack.pop cmd_stack in self#process_interp_error queue sentence loc msg id in Coq.bind query next @@ -398,12 +399,12 @@ object(self) let finder (n, found, zone) ({ start; stop; state_id } as sentence) = let found = found || until n state_id start stop in match found, state_id with - | true, Some id -> `Stop (n, id, Some sentence, zone) - | _ -> `Cont (n + 1, found, sentence :: zone) in - try Searchstack.find finder (0, false, []) cmd_stack + | true, Some id -> Stop (n, id, Some sentence, zone) + | _ -> Next (n + 1, found, sentence :: zone) in + try Stack.seek finder (0, false, []) cmd_stack with Not_found -> - Searchstack.length cmd_stack, initial_state, - None, List.rev (Searchstack.to_list cmd_stack) + Stack.length cmd_stack, initial_state, + None, List.rev (Stack.to_list cmd_stack) (** Wrapper around the raw undo command *) method private backtrack_until ?(move_insert=true) until = @@ -414,7 +415,7 @@ object(self) if move_insert then buffer#place_cursor ~where:self#get_start_of_input; self#show_goals in let cleanup n l = - for i = 1 to n do ignore(Searchstack.pop cmd_stack) done; + for i = 1 to n do ignore(Stack.pop cmd_stack) done; if l <> [] then begin let start = buffer#get_iter_at_mark (CList.hd l).start in let stop = buffer#get_iter_at_mark (CList.last l).stop in @@ -448,12 +449,12 @@ object(self) messages#push Error msg; ignore(self#process_feedback ()); let safe_flags s = s.flags = [ `UNSAFE ] || s.flags = [] in - let find_last_safe_id () s = + let find_last_safe_id s = match s.state_id with - | Some id when safe_flags s -> `Stop id | _ -> `Cont () in + | Some id -> safe_flags s | None -> false in try - let last_safe_id = Searchstack.find find_last_safe_id () cmd_stack in - self#backtrack_until (fun _ id _ _ -> id = Some last_safe_id) + let last_safe = Stack.find find_last_safe_id cmd_stack in + self#backtrack_until (fun _ id _ _ -> id = last_safe.state_id) with Not_found -> self#backtrack_until (fun _ id _ _ -> id = Some safe_id) method backtrack_last_phrase = @@ -494,7 +495,7 @@ object(self) ~start:(`MARK (buffer#create_mark start)) ~stop:(`MARK (buffer#create_mark stop)) [] in - Searchstack.push sentence cmd_stack; + Stack.push sentence cmd_stack; messages#clear; self#show_goals in @@ -528,8 +529,8 @@ object(self) let action () = if why = Coq.Unexpected then warning "Coqtop died badly. Resetting."; (* clear the stack *) - while not (Searchstack.is_empty cmd_stack) do - let phrase = Searchstack.pop cmd_stack in + while not (Stack.is_empty cmd_stack) do + let phrase = Stack.pop cmd_stack in buffer#delete_mark phrase.start; buffer#delete_mark phrase.stop done; diff --git a/lib/searchstack.mli b/lib/cSig.mli index 6c81a2a9c..4858d16c3 100644 --- a/lib/searchstack.mli +++ b/lib/cSig.mli @@ -6,20 +6,10 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -type 'a t -type ('a,'b) search = [ `Stop of 'b | `Cont of 'a ] +(** Missing pervasive types from OCaml stdlib *) -val create : unit -> 'a t -val push : 'a -> 'a t -> unit -val find : ('c -> 'a -> ('c, 'b) search) -> 'c -> 'a t -> 'b -val is_empty : 'a t -> bool -val iter : ('a -> unit) -> 'a t -> unit -val clear : 'a t -> unit -val length : 'a t -> int +type ('a, 'b) union = Inl of 'a | Inr of 'b +(** Union type *) -(* may raise Stack.Empty *) -val pop : 'a t -> 'a -val top : 'a t -> 'a - -(* Extra *) -val to_list : 'a t -> 'a list +type ('a, 'b) seek = Stop of 'a | Next of 'b +(** Type isomorphic to union used for browsable structures. *) diff --git a/lib/searchstack.ml b/lib/cStack.ml index 8d160e572..e0a3733f6 100644 --- a/lib/searchstack.ml +++ b/lib/cStack.ml @@ -6,18 +6,28 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open CSig + +exception Empty = Stack.Empty + type 'a t = 'a list ref -type ('a,'b) search = [ `Stop of 'b | `Cont of 'a ] let create () = ref [] let push x l = l := x :: !l let pop l = match !l with [] -> raise Stack.Empty | x::xs -> l := xs; x let top l = match !l with [] -> raise Stack.Empty | x::_ -> x -let find f i l = - let rec aux i = function +let find f l = List.find f !l +let find_map f l = + let rec aux = function + | [] -> raise Not_found + | x :: xs -> match f x with None -> aux xs | Some i -> i + in + aux !l +let seek f accu l = + let rec aux accu = function | [] -> raise Not_found - | x::xs -> match f i x with `Stop x -> x | `Cont i -> aux i xs in - aux i !l + | x :: xs -> match f accu x with Stop x -> x | Next i -> aux accu xs in + aux accu !l let is_empty l = match !l with [] -> true | _ -> false let iter f l = List.iter f !l let clear l = l := [] diff --git a/lib/cStack.mli b/lib/cStack.mli new file mode 100644 index 000000000..edca85448 --- /dev/null +++ b/lib/cStack.mli @@ -0,0 +1,58 @@ +(************************************************************************) +(* 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 *) +(************************************************************************) + +(** Extended interface for OCaml stacks. *) + +open CSig + +type 'a t + +exception Empty +(** Alias for Stack.Empty. *) + +val create : unit -> 'a t +(** Create an empty stack. *) + +val push : 'a -> 'a t -> unit +(** Add an element to a stack. *) + +val find : ('a -> bool) -> 'a t -> 'a +(** Find the first element satisfying the predicate. + @raise Not_found it there is none. *) + +val find_map : ('a -> 'b option) -> 'a t -> 'b +(** Find the first element that returns [Some _]. + @raise Not_found it there is none. *) + +val seek : ('c -> 'a -> ('b, 'c) seek) -> 'c -> 'a t -> 'b +(** Find the first element that returns [Some _]. + @raise Not_found it there is none. *) + +val is_empty : 'a t -> bool +(** Whether a stack is empty. *) + +val iter : ('a -> unit) -> 'a t -> unit +(** Iterate a function over elements, from the last added one. *) + +val clear : 'a t -> unit +(** Empty a stack. *) + +val length : 'a t -> int +(** Length of a stack. *) + +val pop : 'a t -> 'a +(** Remove and returns the first element of the stack. + @raise Empty if empty. *) + +val top : 'a t -> 'a +(** Remove the first element of the stack without modifying it. + @raise Empty if empty. *) + +val to_list : 'a t -> 'a list +(** Convert to a list. *) + diff --git a/lib/clib.mllib b/lib/clib.mllib index 30821492e..833182bce 100644 --- a/lib/clib.mllib +++ b/lib/clib.mllib @@ -19,6 +19,7 @@ CObj CList CString CArray +CStack Util Loc Flags diff --git a/lib/lib.mllib b/lib/lib.mllib index 9f29613d1..f45c34610 100644 --- a/lib/lib.mllib +++ b/lib/lib.mllib @@ -2,7 +2,6 @@ Xml_lexer Xml_parser Xml_printer Errors -Searchstack Bigint Dyn Segmenttree diff --git a/lib/util.ml b/lib/util.ml index b7364cbc5..2db11131d 100644 --- a/lib/util.ml +++ b/lib/util.ml @@ -69,6 +69,10 @@ module Array : CArray.ExtS = CArray module Map = CMap +(* Stacks *) + +module Stack = CStack + (* Matrices *) let matrix_transpose mat = @@ -118,7 +122,8 @@ let delayed_force f = f () (* Misc *) -type ('a,'b) union = Inl of 'a | Inr of 'b +type ('a, 'b) union = ('a, 'b) CSig.union = Inl of 'a | Inr of 'b +type ('a, 'b) seek = ('a, 'b) CSig.seek = Stop of 'a | Next of 'b (*s interruption *) diff --git a/lib/util.mli b/lib/util.mli index 72217fd0e..8dec93e30 100644 --- a/lib/util.mli +++ b/lib/util.mli @@ -63,6 +63,10 @@ module Array : CArray.ExtS module Map : module type of CMap +(** {6 Stacks.} *) + +module Stack : module type of CStack + (** {6 Streams. } *) val stream_nth : int -> 'a Stream.t -> 'a @@ -90,7 +94,11 @@ val delayed_force : 'a delayed -> 'a (** {6 Misc. } *) -type ('a, 'b) union = Inl of 'a | Inr of 'b +type ('a, 'b) union = ('a, 'b) CSig.union = Inl of 'a | Inr of 'b +(** Union type *) + +type ('a, 'b) seek = ('a, 'b) CSig.seek = Stop of 'a | Next of 'b +(** Type isomorphic to union used for browsable structures. *) (** {6 ... } *) (** Coq interruption: set the following boolean reference to interrupt Coq diff --git a/toplevel/stm.ml b/toplevel/stm.ml index bae2a58fe..1bade01bb 100644 --- a/toplevel/stm.ml +++ b/toplevel/stm.ml @@ -941,7 +941,7 @@ module Backtrack : sig end = struct (* {{{ *) - module S = Searchstack + module S = Stack type hystory_elt = { id : Stateid.t ; @@ -981,8 +981,7 @@ end = struct (* {{{ *) let branches_of id = try - let s = S.find (fun n s -> - if Stateid.equal s.id id then `Stop s else `Cont ()) () history in + let s = S.find (fun s -> Stateid.equal s.id id) history in Vcs_.branches s.vcs with Not_found -> assert false @@ -994,19 +993,19 @@ end = struct (* {{{ *) (str"Reset not implemented for automatically generated constants"); (try let s = - S.find (fun b s -> - if b then `Stop s else `Cont (List.mem name s.label)) + S.seek (fun b s -> + if b then Stop s else Next (List.mem name s.label)) false history in VtStm (VtBack s.id, true), VtNow with Not_found -> VtStm (VtBack (S.top history).id, true), VtNow) | VernacBack n -> - let s = S.find (fun n s -> - if Int.equal n 0 then `Stop s else `Cont (n-1)) n history in + let s = S.seek (fun n s -> + if Int.equal n 0 then Stop s else Next (n-1)) n history in VtStm (VtBack s.id, true), VtNow | VernacUndo n -> - let s = S.find (fun n s -> - if Int.equal n 0 then `Stop s else `Cont (n-1)) n history in + let s = S.seek (fun n s -> + if Int.equal n 0 then Stop s else Next (n-1)) n history in VtStm (VtBack s.id, true), VtLater | VernacUndoTo _ | VernacRestart as e -> @@ -1014,16 +1013,16 @@ end = struct (* {{{ *) let vcs = (S.top history).vcs in let cb, _ = Vcs_aux.find_proof_at_depth vcs (Vcs_aux.proof_nesting vcs) in - let n = S.find (fun n { vcs } -> - if List.mem cb (Vcs_.branches vcs) then `Cont (n+1) else `Stop n) + let n = S.seek (fun n { vcs } -> + if List.mem cb (Vcs_.branches vcs) then Next (n+1) else Stop n) 0 history in - let s = S.find (fun n s -> - if Int.equal n 0 then `Stop s else `Cont (n-1)) (n-m-1) history in + let s = S.seek (fun n s -> + if Int.equal n 0 then Stop s else Next (n-1)) (n-m-1) history in VtStm (VtBack s.id, true), VtLater | VernacAbortAll -> - let s = S.find (fun () s -> - match Vcs_.branches s.vcs with [_] -> `Stop s | _ -> `Cont ()) - () history in + let s = S.find (fun s -> + match Vcs_.branches s.vcs with [_] -> true | _ -> false) + history in VtStm (VtBack s.id, true), VtLater | VernacBacktrack (id,_,_) | VernacBackTo id -> |