From 7a9708cd03e40bd9becb68d8e702be65d4992819 Mon Sep 17 00:00:00 2001 From: vgross Date: Thu, 19 Nov 2009 12:48:32 +0000 Subject: Refactoring of coqide backtrack code, with the intent to put everything into coqtop. Also, some cleaning in ide/gtk_parsing.ml. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12537 85f007b7-540e-0410-9357-904b9bb8a0f7 --- ide/coq.ml | 73 +++++++++++++++++------------------------- ide/coq.mli | 25 ++++++++++++--- ide/coqide.ml | 93 +++++++++++++++++++++++++++++------------------------- ide/gtk_parsing.ml | 67 --------------------------------------- 4 files changed, 100 insertions(+), 158 deletions(-) (limited to 'ide') diff --git a/ide/coq.ml b/ide/coq.ml index bf1140552..6018cc07e 100644 --- a/ide/coq.ml +++ b/ide/coq.ml @@ -340,21 +340,41 @@ let is_vernac_goal_printing_command com = List.mem GoalStartingCommand attribute or List.mem SolveCommand attribute -type undo_info = identifier list * int - -let undo_info () = Pfedit.get_all_proof_names (), Pfedit.current_proof_depth() - type reset_mark = Libnames.object_name -type reset_info = reset_mark * undo_info * bool ref +type reset_info = { + state : reset_mark; + pending : identifier list; + pf_depth : int; + mutable segment : bool; +} let compute_reset_info () = - (match Lib.has_top_frozen_state () with + match Lib.has_top_frozen_state () with | Some st -> - prerr_endline ("On top of state "^Libnames.string_of_path (fst st)); - st + { state = st; + pending = Pfedit.get_all_proof_names (); + pf_depth = Pfedit.current_proof_depth (); + segment = true; } | None -> - failwith "FATAL ERROR: NO RESET"), undo_info(), ref true + failwith "FATAL ERROR: NO RESET" + +type backtrack = + | BacktrackToNextActiveMark + | BacktrackToMark of reset_mark + | NoBacktrack + +type undo_cmds = { + n : int; + a : int; + b : backtrack; + p : int; + l : (identifier list * int); +} + +let init_undo u = + { n = 0; a = 0; b = NoBacktrack; p = 0; + l = (Pfedit.get_all_proof_names u,Pfedit.current_proof_depth u) } let reset_initial () = prerr_endline "Reset initial called"; flush stderr; @@ -410,41 +430,6 @@ let interp_and_replace s = let msg = read_stdout () in result,msg -type bktk_info = { start : GText.mark; - stop : GText.mark; - state_num : int; - pending_proofs : string list; - proof_stack_depth : int; -} - -let record_interp cmd_stk start_of_sentence end_of_sentence (sn,pp,psd) = - Stack.push { start = start_of_sentence; - stop = end_of_sentence; - state_num = sn; - pending_proofs = pp; - proof_stack_depth = psd; - } cmd_stk - -let backtrack cmd_stack stop_cond = - if Stack.is_empty cmd_stack then - reset_initial () (* reset coq *) - else try - let current = Stack.top cmd_stack in - while not (stop_cond (Stack.top cmd_stack).stop) do - ignore (Stack.pop cmd_stack) - done; - let target = Stack.top cmd_stack in - if current != target then - let rst = target.state_num in - let undo = target.proof_stack_depth in - let abrt = List.fold_left - (fun acc e -> if List.mem e target.pending_proofs then acc else succ acc) - 0 current.pending_proofs - in - raw_interp (Printf.sprintf "Backtrack %d %d %d.\n" rst undo abrt) - else () - with Stack.Empty -> reset_initial () (* might as well reset coq ... *) - type tried_tactic = | Interrupted | Success of int (* nb of goals after *) diff --git a/ide/coq.mli b/ide/coq.mli index c2f96a1fe..a03528f81 100644 --- a/ide/coq.mli +++ b/ide/coq.mli @@ -31,13 +31,30 @@ val printing_state : printing_state type reset_mark -type undo_info = identifier list * int +type reset_info = { + state : reset_mark; + pending : identifier list; + pf_depth : int; + mutable segment : bool; +} -val undo_info : unit -> undo_info +val compute_reset_info : unit -> reset_info -type reset_info = reset_mark * undo_info * bool ref +type backtrack = + | BacktrackToNextActiveMark + | BacktrackToMark of reset_mark + | NoBacktrack + +type undo_cmds = { + n : int; + a : int; + b : backtrack; + p : int; + l : (identifier list * int); +} + +val init_undo : unit -> undo_cmds -val compute_reset_info : unit -> reset_info val reset_initial : unit -> unit val reset_to : reset_mark -> unit val reset_to_mod : identifier -> unit diff --git a/ide/coqide.ml b/ide/coqide.ml index 90673b67f..a22e4b4df 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -175,11 +175,12 @@ let cb = GData.clipboard Gdk.Atom.primary exception Size of int -let update_on_end_of_segment cmd_stk id = - let lookup_section = function - | { reset_info = _,_,r } -> r := false - in - try Stack.iter lookup_section cmd_stk with Exit -> () +(* when pushing a segment end, all the previous sentences have their segment + * boolean turned to false, causing backtrack to such sentences to be a + * BackTrackToNextActiveMark *) +let update_on_end_of_segment cmd_stk = let lookup_section item = + item.reset_info.segment <- false in try Stack.iter lookup_section cmd_stk with + Exit -> () let push_phrase cmd_stk reset_info start_of_phrase_mark end_of_phrase_mark ast = let x = {start = start_of_phrase_mark; @@ -189,9 +190,9 @@ let push_phrase cmd_stk reset_info start_of_phrase_mark end_of_phrase_mark ast = } in begin match snd ast with - | VernacEndSegment (_,id) -> + | VernacEndSegment _ -> prerr_endline "Updating on end of segment 1"; - update_on_end_of_segment cmd_stk id + update_on_end_of_segment cmd_stk | _ -> () end; Stack.push x cmd_stk @@ -201,52 +202,59 @@ let repush_phrase cmd_stk reset_info x = let x = { x with reset_info = reset_info } in begin match snd x.ast with - | VernacEndSegment (_,id) -> + | VernacEndSegment _ -> prerr_endline "Updating on end of segment 2"; - update_on_end_of_segment cmd_stk id + update_on_end_of_segment cmd_stk | _ -> () end; Stack.push x cmd_stk -type backtrack = -| BacktrackToNextActiveMark -| BacktrackToMark of reset_mark -| NoBacktrack - -let add_undo = function (n,a,b,p,l as x) -> if p = 0 then (n+1,a,b,p,l) else x -let add_abort = function - | (n,a,b,0,l) -> (0,a+1,b,0,l) - | (n,a,b,p,l) -> (n,a,b,p-1,l) -let add_qed q (n,a,b,p,l as x) = - if q = 0 then x else (n,a,BacktrackToNextActiveMark,p+q,l) -let add_backtrack (n,a,b,p,l) b' = (n,a,b',p,l) - -let update_proofs (n,a,b,p,(cur_lems,ntacsteps)) (prev_lems,prev_ntacsteps) = +(* called ($ntacsteps - $prev_ntacsteps) times *) +let add_undo x = + if x.p = 0 then { x with n = x.n + 1 } else x + +(* called $openproofs times *) +let add_abort x = + if x.p = 0 then (* *) + { x with n = 0; a = x.a + 1 } + else (* there was a closed proof between S+ and S0, and now there is an open proof between S0 and S- *) + { x with p = x.p - 1 } + +(* called at each update_proof call *) +let add_qed q x = + if q = 0 then (* no closed proofs *) + x + else (* closed proofs *) + { x with b = BacktrackToNextActiveMark; p = x.p + q } + +let add_backtrack x b' = + { x with b = b' } + +let update_proofs x (prev_lems,prev_ntacsteps) = + let (cur_lems,ntacsteps) = x.l in let ncommon = List.length (Util.list_intersect cur_lems prev_lems) in let openproofs = List.length cur_lems - ncommon in let closedproofs = List.length prev_lems - ncommon in - let undos = (n,a,b,p,(prev_lems,prev_ntacsteps)) in + let undos = { x with l = (prev_lems,prev_ntacsteps) } in let undos = add_qed closedproofs (Util.iterate add_abort openproofs undos) in Util.iterate add_undo (ntacsteps - prev_ntacsteps) undos let pop_command cmd_stk undos t = - let (state_info,undo_info,section_info) = t.reset_info in + let t = t.reset_info in + let (state_info,undo_info,section_info) = (t.state,(t.pending,t.pf_depth),t.segment) in let undos = - if !section_info then + if section_info then (* segment ouvert, on saute directement au bon état *) let undos = update_proofs undos undo_info in add_backtrack undos (BacktrackToMark state_info) - else + else (* segment fermé, il faut sauter au debut du segment *) begin prerr_endline "In section"; - (* An object inside a closed section *) - add_backtrack undos BacktrackToNextActiveMark + (* XXX - all the way to the bottom of the stack *) + add_backtrack undos BacktrackToNextActiveMark end in ignore (Stack.pop cmd_stk); undos - -(* appelle Pfedit.delete_current_proof a fois - * utiliser Vernacentries.vernac_abort a la place ? *) let apply_aborts a = if a <> 0 then prerr_endline ("Applying "^string_of_int a^" aborts"); try Util.repeat a Pfedit.delete_current_proof () @@ -254,8 +262,6 @@ let apply_aborts a = exception UndoStackExhausted -(* appelle Pfedit.undo n fois - * utiliser vernac_undo ? *) let apply_tactic_undo n = if n<>0 then (prerr_endline ("Applying "^string_of_int n^" undos"); @@ -267,15 +273,17 @@ let apply_reset = function | NoBacktrack -> () | BacktrackToNextActiveMark -> assert false -let rec apply_undos cmd_stk (n,a,b,p,l as undos) = - if p = 0 & b <> BacktrackToNextActiveMark then +(* XXX - in its current form, it goes all the way to the bottom of the stack. *) +let rec apply_undos cmd_stk undos = + if undos.p = 0 & undos.b <> BacktrackToNextActiveMark then + (* pas de preuve fermée et dans un segment ouvert *) begin - apply_aborts a; + apply_aborts undos.a; try - apply_tactic_undo n; - apply_reset b + apply_tactic_undo undos.n; + apply_reset undos.b with UndoStackExhausted -> - apply_undos cmd_stk (n,0,BacktrackToNextActiveMark,p,l) + apply_undos cmd_stk { undos with a = 0; b = BacktrackToNextActiveMark } end else (* re-synchronize Coq to the current state of the stack *) @@ -1274,7 +1282,7 @@ object(self) else done_smthg, undos in - let undos = (0,0,NoBacktrack,0,undo_info()) in + let undos = Coq.init_undo () in let done_smthg, undos = pop_commands false undos in prerr_endline "Popped commands"; if done_smthg then @@ -1344,7 +1352,7 @@ object(self) self#show_goals; self#clear_message in - let undo = pop_command cmd_stack (0,0,NoBacktrack,0,undo_info()) last_command in + let undo = pop_command cmd_stack (Coq.init_undo ()) last_command in apply_undos cmd_stack undo; sync update_input () with @@ -1909,7 +1917,6 @@ let main files = input_buffer#place_cursor input_buffer#start_iter; prerr_endline ("Loading: switch to view "^ string_of_int index); session_notebook#goto_page index; - prerr_endline "Loading: highlight"; input_buffer#set_modified false; prerr_endline "Loading: clear undo"; session.script#clear_undo; diff --git a/ide/gtk_parsing.ml b/ide/gtk_parsing.ml index e92a345e3..ffb8c8d59 100644 --- a/ide/gtk_parsing.ml +++ b/ide/gtk_parsing.ml @@ -107,70 +107,3 @@ let rec complete_forward w (it:GText.iter) = else Some (stop,stop,ne) else complete_forward w stop - -let find_comment_end (start:GText.iter) = - let rec find_nested_comment (search_start:GText.iter) (search_end:GText.iter) (comment_end:GText.iter) = - match (search_start#forward_search ~limit:search_end "(*"),(comment_end#forward_search "*)") with - | None,_ -> comment_end - | Some _, None -> raise Not_found - | Some (_,next_search_start),Some (next_search_end,next_comment_end) -> - find_nested_comment next_search_start next_search_end next_comment_end - in - match start#forward_search "*)" with - | None -> raise Not_found - | Some (search_end,comment_end) -> find_nested_comment start search_end comment_end - - -let rec find_string_end (start:GText.iter) = - let dblquote = int_of_char '"' in - let rec escaped_dblquote c = - (c#char = dblquote) && not (escaped_dblquote c#backward_char) - in - match start#forward_search "\"" with - | None -> raise Not_found - | Some (stop,next_start) -> - if escaped_dblquote stop#backward_char - then find_string_end next_start - else next_start - - -let rec find_next_sentence (from:GText.iter) = - match (from#forward_search ".") with - | None -> raise Not_found - | Some (non_vernac_search_end,next_sentence) -> - match from#forward_search ~limit:non_vernac_search_end "(*",from#forward_search ~limit:non_vernac_search_end "\"" with - | None,None -> - if Glib.Unichar.isspace next_sentence#char || next_sentence#compare next_sentence#forward_char == 0 - then next_sentence else find_next_sentence next_sentence - | None,Some (_,string_search_start) -> find_next_sentence (find_string_end string_search_start) - | Some (_,comment_search_start),None -> find_next_sentence (find_comment_end comment_search_start) - | Some (_,comment_search_start),Some (_,string_search_start) -> - find_next_sentence ( - if comment_search_start#compare string_search_start < 0 - then find_comment_end comment_search_start - else find_string_end string_search_start) - - -let find_nearest_forward (cursor:GText.iter) targets = - let fold_targets acc target = - match cursor#forward_search target,acc with - | Some (t_start,_),Some nearest when (t_start#compare nearest < 0) -> Some t_start - | Some (t_start,_),None -> Some t_start - | _ -> acc - in - match List.fold_left fold_targets None targets with - | None -> raise Not_found - | Some nearest -> nearest - - -let find_nearest_backward (cursor:GText.iter) targets = - let fold_targets acc target = - match cursor#backward_search target,acc with - | Some (t_start,_),Some nearest when (t_start#compare nearest > 0) -> Some t_start - | Some (t_start,_),None -> Some t_start - | _ -> acc - in - match List.fold_left fold_targets None targets with - | None -> raise Not_found - | Some nearest -> nearest - -- cgit v1.2.3