diff options
| -rw-r--r-- | ide/coq.ml | 127 | ||||
| -rw-r--r-- | ide/coq.mli | 30 | ||||
| -rw-r--r-- | ide/coqide.ml | 75 | ||||
| -rw-r--r-- | library/lib.ml | 15 | ||||
| -rw-r--r-- | 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) *) |