From 9fec60111a49960a01ffdd863d69fea57960edc5 Mon Sep 17 00:00:00 2001 From: herbelin Date: Sat, 24 May 2008 14:32:25 +0000 Subject: - Prise en compte des frozen state de Coq autant que possible pour améliorer l'efficacité du undo. Restent les Qed et les End dont le undo peut nécessiter de rejouer un segment arbitrairement complexe (pour le undo du Qed, il faudrait typiquement que Coq se souvienne de l'entrelacement de déclarations et de tactiques). - Code mort concernant les mots-clés dans coq.ml. MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10982 85f007b7-540e-0410-9357-904b9bb8a0f7 --- ide/coq.ml | 127 +++++++++++++++++++++++--------------------------------- ide/coq.mli | 30 +++++++------ ide/coqide.ml | 75 ++++++++++++++++++++------------- library/lib.ml | 15 +++++++ library/lib.mli | 3 ++ 5 files changed, 135 insertions(+), 115 deletions(-) diff --git a/ide/coq.ml b/ide/coq.ml index 4e0150918..17f80b0ec 100644 --- a/ide/coq.ml +++ b/ide/coq.ml @@ -271,6 +271,57 @@ let is_vernac_state_preserving_command com = let is_vernac_tactic_command com = List.mem SolveCommand (attribute_of_vernac_command com) +type reset_mark = + | ResetToId of Names.identifier + | ResetToState of Libnames.object_name + +type reset_info = + | NoReset + | ResetAtDecl of reset_mark * bool ref + | ResetAtSegmentStart of Names.identifier * bool ref + | ResetAtFrozenState of Libnames.object_name * bool ref + +let reset_mark id = match Lib.has_top_frozen_state () with + | Some sp -> ResetToState sp + | None -> ResetToId id + +let compute_reset_info = function + | VernacBeginSection id + | VernacDefineModule (_,id, _, _, _) + | VernacDeclareModule (_,id, _, _) + | VernacDeclareModuleType (id, _, _) -> + ResetAtSegmentStart (snd id, ref true) + + | VernacDefinition (_, (_,id), DefineBody _, _) + | VernacAssumption (_,_ ,(_,((_,id)::_,_))::_) + | VernacInductive (_, (((_,id),_,_,_),_) :: _) -> + ResetAtDecl (reset_mark id, ref true) + + | VernacDefinition (_, (_,id), ProveBody _, _) + | VernacStartTheoremProof (_, [Some (_,id), _], _, _) -> + ResetAtDecl (reset_mark id, ref false) + + | VernacEndProof _ -> NoReset + | _ -> match Lib.has_top_frozen_state () with + | Some sp -> ResetAtFrozenState (sp, ref true) + | None -> NoReset + +let reset_initial () = + prerr_endline "Reset initial called"; flush stderr; + Vernacentries.abort_refine Lib.reset_initial () + +let reset_to = function + | ResetToId id -> + prerr_endline ("Reset called with "^(string_of_id id)); + Vernacentries.abort_refine Lib.reset_name (Util.dummy_loc,id) + | ResetToState sp -> + Vernacentries.abort_refine Lib.reset_to_state sp + +let reset_to_mod id = + prerr_endline ("Reset called to Mod/Sect with "^(string_of_id id)); + Vernacentries.abort_refine Lib.reset_mod (Util.dummy_loc,id) + + let interp verbosely s = prerr_endline "Starting interp..."; prerr_endline s; @@ -291,10 +342,11 @@ let interp verbosely s = if not (is_vernac_goal_printing_command vernac) then (* Verbose if in small step forward and not a tactic *) Flags.make_silent (not verbosely); + let reset_info = compute_reset_info vernac in Vernac.raw_do_vernac (Pcoq.Gram.parsable (Stream.of_string s)); Flags.make_silent true; prerr_endline ("...Done with interp of : "^s); - last + reset_info,last let interp_and_replace s = let result = interp false s in @@ -425,79 +477,6 @@ let print_no_goal () = msg (Printer.pr_subgoals (Decl_mode.get_end_command pfts) sigma gls) -type word_class = Normal | Kwd | Reserved - - -let kwd = [(* "Compile";"Inductive";"Qed";"Type";"end";"Axiom"; - "Definition";"Load";"Quit";"Variable";"in";"Cases";"FixPoint"; - "Parameter";"Set";"of";"CoFixpoint";"Grammar";"Proof";"Syntax"; - "using";"CoInductive";"Hypothesis";"Prop";"Theorem"; - *) - "Add"; "AddPath"; "Axiom"; "Chapter"; "CoFixpoint"; - "CoInductive"; "Defined"; "Definition"; - "End"; "Export"; "Fact"; "Fix"; "Fixpoint"; "Global"; "Grammar"; "Hint"; - "Hypothesis"; "Immediate"; "Implicits"; "Import"; "Inductive"; - "Infix"; "Lemma"; "Load"; "Local"; - "Match"; "Module"; "Module Type"; - "Mutual"; "Parameter"; "Print"; "Proof"; "Qed"; - "Record"; "Recursive"; "Remark"; "Require"; "Save"; "Scheme"; - "Section"; "Show"; "Syntactic"; "Syntax"; "Tactic"; "Theorem"; - "Unset"; "Variable"; "Variables"; -] - -let reserved = [] - -module SHashtbl = - Hashtbl.Make - (struct - type t = string - let equal = ( = ) - let hash = Hashtbl.hash - end) - - -let word_tbl = SHashtbl.create 37 -let _ = - List.iter (fun w -> SHashtbl.add word_tbl w Kwd) kwd; - List.iter (fun w -> SHashtbl.add word_tbl w Reserved) reserved - -let word_class s = - try - SHashtbl.find word_tbl s - with Not_found -> Normal - -type reset_info = - | NoReset - | ResetAtDecl of Names.identifier * bool ref - | ResetAtSegmentStart of Names.identifier * bool ref - -let compute_reset_info = function - | VernacBeginSection id - | VernacDefineModule (_,id, _, _, _) - | VernacDeclareModule (_,id, _, _) - | VernacDeclareModuleType (id, _, _) -> - ResetAtSegmentStart (snd id, ref true) - | VernacDefinition (_, (_,id), DefineBody _, _) - | VernacAssumption (_,_ ,(_,((_,id)::_,_))::_) - | VernacInductive (_, (((_,id),_,_,_),_) :: _) -> - ResetAtDecl (id, ref true) - | VernacDefinition (_, (_,id), ProveBody _, _) - | VernacStartTheoremProof (_, [Some (_,id), _], _, _) -> - ResetAtDecl (id, ref false) - | _ -> NoReset - -let reset_initial () = - prerr_endline "Reset initial called"; flush stderr; - Vernacentries.abort_refine Lib.reset_initial () - -let reset_to id = - prerr_endline ("Reset called with "^(string_of_id id)); - Vernacentries.abort_refine Lib.reset_name (Util.dummy_loc,id) -let reset_to_mod id = - prerr_endline ("Reset called to Mod/Sect with "^(string_of_id id)); - Vernacentries.abort_refine Lib.reset_mod (Util.dummy_loc,id) - - let hyp_menu (env, sigma, ((coqident,ident),_,ast),(s,pr_ast)) = [("clear "^ident),("clear "^ident^"."); diff --git a/ide/coq.mli b/ide/coq.mli index 9c8e27320..5ded2b573 100644 --- a/ide/coq.mli +++ b/ide/coq.mli @@ -15,10 +15,26 @@ open Evd val version : unit -> string +type reset_mark = + | ResetToId of Names.identifier + | ResetToState of Libnames.object_name + +type reset_info = + | NoReset + | ResetAtDecl of reset_mark * bool ref + | ResetAtSegmentStart of Names.identifier * bool ref + | ResetAtFrozenState of Libnames.object_name * bool ref + +val compute_reset_info : Vernacexpr.vernac_expr -> reset_info +val reset_initial : unit -> unit +val reset_to : reset_mark -> unit +val reset_to_mod : identifier -> unit + val init : unit -> string list -val interp : bool -> string -> Util.loc * Vernacexpr.vernac_expr +val interp : bool -> string -> reset_info * (Util.loc * Vernacexpr.vernac_expr) val interp_last : Util.loc * Vernacexpr.vernac_expr -> unit -val interp_and_replace : string -> (Util.loc * Vernacexpr.vernac_expr) * string +val interp_and_replace : string -> + (reset_info * (Util.loc * Vernacexpr.vernac_expr)) * string val is_vernac_tactic_command : Vernacexpr.vernac_expr -> bool val is_vernac_state_preserving_command : Vernacexpr.vernac_expr -> bool @@ -42,16 +58,6 @@ val print_no_goal : unit -> string val process_exn : exn -> string*(Util.loc option) -type reset_info = - | NoReset - | ResetAtDecl of Names.identifier * bool ref - | ResetAtSegmentStart of Names.identifier * bool ref - -val compute_reset_info : Vernacexpr.vernac_expr -> reset_info -val reset_initial : unit -> unit -val reset_to : identifier -> unit -val reset_to_mod : identifier -> unit - val hyp_menu : hyp -> (string * string) list val concl_menu : concl -> (string * string) list diff --git a/ide/coqide.ml b/ide/coqide.ml index 7cfeb694d..4e5223b02 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -159,7 +159,7 @@ object('self) method activate : unit -> unit method active_keypress_handler : GdkEvent.Key.t -> bool method backtrack_to : GText.iter -> unit - method backtrack_to_no_lock : GText.iter -> Names.identifier option -> unit + method backtrack_to_no_lock : GText.iter -> reset_mark option -> unit method clear_message : unit method deactivate : unit -> unit method disconnected_keypress_handler : GdkEvent.Key.t -> bool @@ -182,7 +182,8 @@ object('self) method reset_initial : unit method send_to_coq : bool -> bool -> string -> - bool -> bool -> bool -> (bool*(Util.loc * Vernacexpr.vernac_expr)) option + bool -> bool -> bool -> + (bool*(reset_info*(Util.loc * Vernacexpr.vernac_expr))) option method set_message : string -> unit method show_pm_goal : unit method show_goals : unit @@ -502,6 +503,9 @@ let is_empty () = Stack.is_empty processed_stack let update_on_end_of_proof () = let lookup_lemma = function + | { reset_info = ResetAtFrozenState (_, r) } -> + prerr_endline "Toggling Frozen State info to false"; + r := false | { reset_info = ResetAtDecl (_, r) } -> if not !r then begin prerr_endline "Toggling Reset info to true"; @@ -521,15 +525,16 @@ let update_on_end_of_segment id = | { reset_info = ResetAtSegmentStart (id', r) } when id = id' -> raise Exit | { reset_info = ResetAtSegmentStart (_, r) } -> r := false | { reset_info = ResetAtDecl (_, r) } -> r := false + | { reset_info = ResetAtFrozenState (_, r) } -> r := false | _ -> () in try Stack.iter lookup_section processed_stack with Exit -> () -let push_phrase start_of_phrase_mark end_of_phrase_mark ast = +let push_phrase reset_info start_of_phrase_mark end_of_phrase_mark ast = let x = {start = start_of_phrase_mark; stop = end_of_phrase_mark; ast = ast; - reset_info = Coq.compute_reset_info (snd ast) + reset_info = reset_info } in begin match snd ast with @@ -540,8 +545,8 @@ let push_phrase start_of_phrase_mark end_of_phrase_mark ast = push x -let repush_phrase x = - let x = { x with reset_info = Coq.compute_reset_info (snd x.ast) } in +let repush_phrase reset_info x = + let x = { x with reset_info = reset_info } in begin match snd x.ast with | VernacEndProof (Proved (_, None)) -> update_on_end_of_proof () @@ -1143,7 +1148,7 @@ object(self) input_view#set_editable true; !pop_info (); end in - let mark_processed complete (start,stop) ast = + let mark_processed reset_info complete (start,stop) ast = let b = input_buffer in b#move_mark ~where:stop (`NAME "start_of_input"); b#apply_tag_by_name @@ -1155,7 +1160,8 @@ object(self) end; let start_of_phrase_mark = `MARK (b#create_mark start) in let end_of_phrase_mark = `MARK (b#create_mark stop) in - push_phrase + push_phrase + reset_info start_of_phrase_mark end_of_phrase_mark ast; if display_goals then self#show_goals; @@ -1165,14 +1171,14 @@ object(self) None -> false | Some (loc,phrase) -> (match self#send_to_coq verbosely false phrase true true true with - | Some (complete,ast) -> - sync (mark_processed complete) loc ast; true + | Some (complete,(reset_info,ast)) -> + sync (mark_processed reset_info complete) loc ast; true | None -> sync remove_tag loc; false) end method insert_this_phrase_on_success show_output show_msg localize coqphrase insertphrase = - let mark_processed complete ast = + let mark_processed reset_info complete ast = let stop = self#get_start_of_input in if stop#starts_line then input_buffer#insert ~iter:stop insertphrase @@ -1185,7 +1191,7 @@ object(self) input_buffer#place_cursor stop; let start_of_phrase_mark = `MARK (input_buffer#create_mark start) in let end_of_phrase_mark = `MARK (input_buffer#create_mark stop) in - push_phrase start_of_phrase_mark end_of_phrase_mark ast; + push_phrase reset_info start_of_phrase_mark end_of_phrase_mark ast; self#show_goals; (*Auto insert save on success... try (match Coq.get_current_goals () with @@ -1206,13 +1212,15 @@ object(self) `MARK (input_buffer#create_mark start) in let end_of_phrase_mark = `MARK (input_buffer#create_mark stop) in - push_phrase start_of_phrase_mark end_of_phrase_mark ast + push_phrase + reset_info start_of_phrase_mark end_of_phrase_mark ast end | None -> ()) | _ -> ()) with _ -> ()*) in match self#send_to_coq false false coqphrase show_output show_msg localize with - | Some (complete,ast) -> sync (mark_processed complete) ast; true + | Some (complete,(reset_info,ast)) -> + sync (mark_processed reset_info complete) ast; true | None -> sync (fun _ -> self#insert_message ("Unsuccessfully tried: "^coqphrase)) @@ -1284,28 +1292,35 @@ object(self) begin match t.reset_info with | ResetAtSegmentStart (id, {contents=true}) -> reset_to_mod id - | ResetAtDecl (id, {contents=true}) -> + | ResetAtFrozenState (sp, {contents=true}) -> if inproof then - (prerr_endline ("Skipping "^Names.string_of_id id); - synchro (Some id) inproof) + synchro (Some (ResetToState sp)) inproof else - reset_to (Option.default id oldest_decl_in_middle_of_proof) - | ResetAtDecl (id, {contents=false}) -> + reset_to (ResetToState sp) + | ResetAtDecl (mark, {contents=true}) -> + if inproof then + synchro (Some mark) inproof + else + reset_to + (Option.default mark oldest_decl_in_middle_of_proof) + | ResetAtDecl (mark, {contents=false}) -> if inproof then if oldest_decl_in_middle_of_proof = None then - synchro None false + match mark with + | ResetToId _ -> synchro None false + | ResetToState _ -> reset_to mark else (* reset oldest decl found before theorem started what *) (* resets back just before the proof was started *) reset_to (Option.get oldest_decl_in_middle_of_proof) else - (prerr_endline ("Skipping "^Names.string_of_id id); - synchro (Some id) inproof) + synchro (Some mark) inproof | _ -> synchro oldest_decl_in_middle_of_proof inproof end; + let reset_info = Coq.compute_reset_info (snd t.ast) in interp_last t.ast; - repush_phrase t + repush_phrase reset_info t end in let add_undo t = match t with | Some n -> Some (succ n) | None -> None @@ -1400,23 +1415,25 @@ Please restart and report NOW."; in begin match last_command with | {ast=_,com} when is_vernac_tactic_command com -> -prerr_endline "TACT"; begin try Pfedit.undo 1; ignore (pop ()); sync update_input () with _ -> self#backtrack_to_no_lock start None end + | {reset_info=ResetAtFrozenState (sp, {contents=true})} -> + ignore (pop ()); + Lib.reset_to_state sp; + sync update_input () | {reset_info=ResetAtSegmentStart (id, {contents=true})} -> -prerr_endline "SEG"; ignore (pop ()); reset_to_mod id; sync update_input () - | {reset_info=ResetAtDecl (id, {contents=true})} -> + | {reset_info=ResetAtDecl (mark, {contents=true})} -> if Pfedit.refining () then - self#backtrack_to_no_lock start (Some id) + self#backtrack_to_no_lock start (Some mark) else - (ignore (pop ()); reset_to id; sync update_input ()) - | {reset_info=ResetAtDecl (id,{contents=false})} -> + (ignore (pop ()); reset_to mark; sync update_input ()) + | {reset_info=ResetAtDecl (_, {contents=false})} -> ignore (pop ()); (try Pfedit.delete_current_proof () diff --git a/library/lib.ml b/library/lib.ml index ae1a41ca1..5e22c4d22 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -584,6 +584,13 @@ let recache_context ctx = let is_frozen_state = function (_,FrozenState _) -> true | _ -> false +let has_top_frozen_state () = + let rec aux = function + | (sp, FrozenState _)::_ -> Some sp + | (sp, Leaf o)::t when object_tag o = "DOT" -> aux t + | _ -> None + in aux !lib_stk + let set_lib_stk new_lib_stk = lib_stk := new_lib_stk; recalc_path_prefix (); @@ -603,6 +610,14 @@ let reset_to_gen test = let reset_to sp = reset_to_gen (fun x -> (fst x) = sp) +let reset_to_state sp = + let (_,eq,before) = split_lib sp in + (* if eq a frozen state, we'll reset to it *) + match eq with + | [_,FrozenState f] -> lib_stk := eq@before; unfreeze_summaries f + | _ -> error "Not a frozen state" + + (* LEM: TODO * We will need to muck with frozen states in after, too! * Not only FrozenState, but also those embedded in Opened(Section|Module|Modtype) diff --git a/library/lib.mli b/library/lib.mli index da8ace048..f3fa9a4b3 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -145,6 +145,9 @@ val reset_to : object_name -> unit val reset_name : identifier located -> unit val remove_name : identifier located -> unit val reset_mod : identifier located -> unit +val reset_to_state : object_name -> unit + +val has_top_frozen_state : unit -> object_name option (* [back n] resets to the place corresponding to the $n$-th call of [mark_end_of_command] (counting backwards) *) -- cgit v1.2.3