From 61dc740ed1c3780cccaec00d059a28f0d31d0052 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Mon, 4 Jun 2012 12:07:52 +0200 Subject: Imported Upstream version 8.4~gamma0+really8.4beta2 --- toplevel/backtrack.ml | 225 +++++++++++++++++++++++ toplevel/backtrack.mli | 93 ++++++++++ toplevel/class.ml | 2 +- toplevel/classes.ml | 9 +- toplevel/command.ml | 36 ++-- toplevel/coqtop.ml | 11 +- toplevel/himsg.ml | 16 +- toplevel/ide_intf.ml | 120 ++++++++++++- toplevel/ide_intf.mli | 26 +++ toplevel/ide_slave.ml | 436 ++++++++++++++++----------------------------- toplevel/interface.mli | 47 +++-- toplevel/metasyntax.ml | 12 ++ toplevel/metasyntax.mli | 2 + toplevel/mltop.ml4 | 23 ++- toplevel/mltop.mli | 10 ++ toplevel/record.ml | 6 +- toplevel/search.mli | 2 + toplevel/toplevel.ml | 3 - toplevel/toplevel.mllib | 1 + toplevel/vernac.ml | 65 ++++--- toplevel/vernac.mli | 9 +- toplevel/vernacentries.ml | 198 +++++++++++++------- toplevel/vernacentries.mli | 31 ++-- toplevel/vernacexpr.ml | 28 ++- 24 files changed, 964 insertions(+), 447 deletions(-) create mode 100644 toplevel/backtrack.ml create mode 100644 toplevel/backtrack.mli (limited to 'toplevel') diff --git a/toplevel/backtrack.ml b/toplevel/backtrack.ml new file mode 100644 index 00000000..24a056d7 --- /dev/null +++ b/toplevel/backtrack.ml @@ -0,0 +1,225 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* l:=i::!l) history; + !l + +(** Basic manipulation of the command history stack *) + +exception Invalid + +let pop () = ignore (Stack.pop history) + +let npop n = + (* Since our history stack always contains an initial entry, + it's invalid to try to completely empty it *) + if n < 0 || n >= Stack.length history then raise Invalid + else for i = 1 to n do pop () done + +let top () = + try Stack.top history with Stack.Empty -> raise Invalid + +(** Search the history stack for a suitable location. We perform first + a non-destructive search: in case of search failure, the stack is + unchanged. *) + +exception Found of info + +let search test = + try + Stack.iter (fun i -> if test i then raise (Found i)) history; + raise Invalid + with Found i -> + while i != Stack.top history do pop () done + +(** Register the end of a command and store the current state *) + +let mark_command ast = + Lib.add_frozen_state(); + Lib.mark_end_of_command(); + Stack.push + { label = Lib.current_command_label (); + nproofs = List.length (Pfedit.get_all_proof_names ()); + prfname = (try Some (Pfedit.get_current_proof_name ()) with _ -> None); + prfdepth = max 0 (Pfedit.current_proof_depth ()); + reachable = true; + cmd = ast } + history + +(** Backtrack by aborting [naborts] proofs, then setting proof-depth back to + [pnum] and finally going to state number [snum]. *) + +let raw_backtrack snum pnum naborts = + for i = 1 to naborts do Pfedit.delete_current_proof () done; + Pfedit.undo_todepth pnum; + Lib.reset_label snum + +(** Re-sync the state of the system (label, proofs) with the top + of the history stack. We may end on some earlier state to avoid + re-opening proofs. This function will return the final label + and the number of extra backtracking steps performed. *) + +let sync nb_opened_proofs = + (* Backtrack by enough additional steps to avoid re-opening proofs. + Typically, when a Qed has been crossed, we backtrack to the proof start. + NB: We cannot reach the empty stack, since the first entry in the + stack has no opened proofs and is tagged as reachable. + *) + let extra = ref 0 in + while not (top()).reachable do incr extra; pop () done; + let target = top () + in + (* Now the opened proofs at target is a subset of the opened proofs before + the backtrack, we simply abort the extra proofs (if any). + NB: It is critical here that proofs are nested in a regular way + (i.e. no more Resume or Suspend commands as earlier). This way, we can + simply count the extra proofs to abort instead of taking care of their + names. + *) + let naborts = nb_opened_proofs - target.nproofs in + (* We are now ready to do a low-level backtrack *) + raw_backtrack target.label target.prfdepth naborts; + (target.label, !extra) + +(** Backtracking by a certain number of (non-state-preserving) commands. + This is used by Coqide. + It may actually undo more commands than asked : for instance instead + of jumping back in the middle of a finished proof, we jump back before + this proof. The number of extra backtracked command is returned at + the end. *) + +let back count = + if count = 0 then 0 + else + let nb_opened_proofs = List.length (Pfedit.get_all_proof_names ()) in + npop count; + snd (sync nb_opened_proofs) + +(** Backtracking to a certain state number, and reset proofs accordingly. + We may end on some earlier state if needed to avoid re-opening proofs. + Return the final state number. *) + +let backto snum = + if snum = Lib.current_command_label () then snum + else + let nb_opened_proofs = List.length (Pfedit.get_all_proof_names ()) in + search (fun i -> i.label = snum); + fst (sync nb_opened_proofs) + +(** Old [Backtrack] code with corresponding update of the history stack. + [Backtrack] is now deprecated (in favor of [BackTo]) but is kept for + compatibility with ProofGeneral. It's completely up to ProofGeneral + to decide where to go and how to adapt proofs. Note that the choices + of ProofGeneral are currently not always perfect (for instance when + backtracking an Undo). *) + +let backtrack snum pnum naborts = + raw_backtrack snum pnum naborts; + search (fun i -> i.label = snum) + +(** [reset_initial] resets the system and clears the command history + stack, only pushing back the initial entry. It should be equivalent + to [backto Lib.first_command_label], but sligthly more efficient. *) + +let reset_initial () = + let init_label = Lib.first_command_label in + if Lib.current_command_label () = init_label then () + else begin + Pfedit.delete_all_proofs (); + Lib.reset_label init_label; + Stack.clear history; + Stack.push + { label = init_label; + nproofs = 0; + prfname = None; + prfdepth = 0; + reachable = true; + cmd = VernacNop } + history + end + +(** Reset to the last known state just before defining [id] *) + +let reset_name id = + let lbl = + try Lib.label_before_name id with Not_found -> raise Invalid + in + ignore (backto lbl) + +(** When a proof is ended (via either Qed/Admitted/Restart/Abort), + old proof steps should be marked differently to avoid jumping back + to them: + - either this proof isn't there anymore in the proof engine + - either it's there but it's a more recent attempt after a Restart, + so we shouldn't mix the two. + We also mark as unreachable the proof steps cancelled via a Undo. *) + +let mark_unreachable ?(after=0) prf_lst = + let fix i = match i.prfname with + | None -> raise Not_found (* stop hacking the history outside of proofs *) + | Some p -> + if List.mem p prf_lst && i.prfdepth > after + then i.reachable <- false + in + try Stack.iter fix history with Not_found -> () + +(** Parse the history stack for printing the script of a proof *) + +let get_script prf = + let script = ref [] in + let select i = match i.prfname with + | None -> raise Not_found + | Some p when p=prf && i.reachable -> script := i :: !script + | _ -> () + in + (try Stack.iter select history with Not_found -> ()); + (* Get rid of intermediate commands which don't grow the depth *) + let rec filter n = function + | [] -> [] + | {prfdepth=d; cmd=c}::l when n < d -> c :: filter d l + | {prfdepth=d}::l -> filter d l + in + (* initial proof depth (after entering the lemma statement) is 1 *) + filter 1 !script diff --git a/toplevel/backtrack.mli b/toplevel/backtrack.mli new file mode 100644 index 00000000..3fde5b11 --- /dev/null +++ b/toplevel/backtrack.mli @@ -0,0 +1,93 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* unit + +(** The [Invalid] exception is raised when one of the following function + tries to empty the history stack, or reach an unknown states, etc. + The stack is preserved in these cases. *) + +exception Invalid + +(** Nota Bene: it is critical for the following functions that proofs + are nested in a regular way (i.e. no more Resume or Suspend commands + as earlier). *) + +(** Backtracking by a certain number of (non-state-preserving) commands. + This is used by Coqide. + It may actually undo more commands than asked : for instance instead + of jumping back in the middle of a finished proof, we jump back before + this proof. The number of extra backtracked command is returned at + the end. *) + +val back : int -> int + +(** Backtracking to a certain state number, and reset proofs accordingly. + We may end on some earlier state if needed to avoid re-opening proofs. + Return the state number on which we finally end. *) + +val backto : int -> int + +(** Old [Backtrack] code with corresponding update of the history stack. + [Backtrack] is now deprecated (in favor of [BackTo]) but is kept for + compatibility with ProofGeneral. It's completely up to ProofGeneral + to decide where to go and how to adapt proofs. Note that the choices + of ProofGeneral are currently not always perfect (for instance when + backtracking an Undo). *) + +val backtrack : int -> int -> int -> unit + +(** [reset_initial] resets the system and clears the command history + stack, only pushing back the initial entry. It should be equivalent + to [backto Lib.first_command_label], but sligthly more efficient. *) + +val reset_initial : unit -> unit + +(** Reset to the last known state just before defining [id] *) + +val reset_name : Names.identifier Util.located -> unit + +(** When a proof is ended (via either Qed/Admitted/Restart/Abort), + old proof steps should be marked differently to avoid jumping back + to them: + - either this proof isn't there anymore in the proof engine + - either a proof with the same name is there, but it's a more recent + attempt after a Restart/Abort, we shouldn't mix the two. + We also mark as unreachable the proof steps cancelled via a Undo. +*) + +val mark_unreachable : ?after:int -> Names.identifier list -> unit + +(** Parse the history stack for printing the script of a proof *) + +val get_script : Names.identifier -> Vernacexpr.vernac_expr list + + +(** For debug purpose, a dump of the history *) + +type info = { + label : int; + nproofs : int; + prfname : Names.identifier option; + prfdepth : int; + cmd : Vernacexpr.vernac_expr; + mutable reachable : bool; +} + +val dump_history : unit -> info list diff --git a/toplevel/class.ml b/toplevel/class.ml index ebaa19b6..c328cc91 100644 --- a/toplevel/class.ml +++ b/toplevel/class.ml @@ -255,7 +255,7 @@ let add_new_coercion_core coef stre source target isid = in check_source (Some cls); if not (uniform_cond (llp-ind) lvs) then - raise (CoercionError NotUniform); + warning (Pp.string_of_ppcmds (explain_coercion_error coef NotUniform)); let clt = try get_target tg ind diff --git a/toplevel/classes.ml b/toplevel/classes.ml index 1e83e4b8..18f12582 100644 --- a/toplevel/classes.ml +++ b/toplevel/classes.ml @@ -252,6 +252,14 @@ let new_instance ?(abstract=false) ?(global=false) ctx (instid, bk, cl) props let term = Termops.it_mkLambda_or_LetIn def ctx in Some term, termtype in + let _ = + evars := Evarutil.nf_evar_map !evars; + evars := Typeclasses.resolve_typeclasses ~filter:Typeclasses.no_goals ~fail:true + env !evars; + (* Try resolving fields that are typeclasses automatically. *) + evars := Typeclasses.resolve_typeclasses ~filter:Typeclasses.all_evars ~fail:false + env !evars + in let termtype = Evarutil.nf_evar !evars termtype in let term = Option.map (Evarutil.nf_evar !evars) term in let evm = undefined_evars !evars in @@ -259,7 +267,6 @@ let new_instance ?(abstract=false) ?(global=false) ctx (instid, bk, cl) props if Evd.is_empty evm && term <> None then declare_instance_constant k pri global imps ?hook id (Option.get term) termtype else begin - evars := Typeclasses.resolve_typeclasses ~onlyargs:true ~fail:true env !evars; let kind = Decl_kinds.Global, Decl_kinds.DefinitionBody Decl_kinds.Instance in Flags.silently (fun () -> Lemmas.start_proof id kind termtype (fun _ -> instance_hook k pri global imps ?hook); diff --git a/toplevel/command.ml b/toplevel/command.ml index eca53ae7..dfb1a1b5 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -87,7 +87,11 @@ let interp_definition bl red_option c ctypopt = let typ = nf_evar !evdref (it_mkProd_or_LetIn ty ctx) in check_evars env Evd.empty !evdref body; check_evars env Evd.empty !evdref typ; - imps1@(Impargs.lift_implicits nb_args imps2), + (* Check that all implicit arguments inferable from the term is inferable from the type *) + if not (try List.for_all (fun (key,va) -> List.assoc key impsty = va) imps2 with Not_found -> false) + then warn (str "Implicit arguments declaration relies on type." ++ + spc () ++ str "The term declares more implicits than the type here."); + imps1@(Impargs.lift_implicits nb_args impsty), { const_entry_body = body; const_entry_secctx = None; const_entry_type = Some typ; @@ -250,7 +254,7 @@ let interp_mutual_inductive (paramsl,indl) notations finite = let mldatas = List.map2 (mk_mltype_data evdref env_params params) arities indnames in let constructors = - States.with_state_protection (fun () -> + Metasyntax.with_syntax_protection (fun () -> (* Temporary declaration of notations and scopes *) List.iter (Metasyntax.set_notation_for_interpretation impls) notations; (* Interpret the constructor types *) @@ -259,7 +263,7 @@ let interp_mutual_inductive (paramsl,indl) notations finite = (* Instantiate evars and check all are resolved *) let evd = consider_remaining_unif_problems env_params !evdref in - let evd = Typeclasses.resolve_typeclasses ~onlyargs:false ~fail:true env_params evd in + let evd = Typeclasses.resolve_typeclasses ~filter:(Typeclasses.no_goals) ~fail:true env_params evd in let sigma = evd in let constructors = List.map (fun (idl,cl,impsl) -> (idl,List.map (nf_evar sigma) cl,impsl)) constructors in let ctx_params = Sign.map_rel_context (nf_evar sigma) ctx_params in @@ -459,12 +463,12 @@ type structured_fixpoint_expr = { let interp_fix_context evdref env isfix fix = let before, after = if isfix then split_at_annot fix.fix_binders fix.fix_annot else [], fix.fix_binders in let impl_env, ((env', ctx), imps) = interp_context_evars evdref env before in - let _, ((env'', ctx'), imps') = interp_context_evars ~impl_env evdref env' after in + let impl_env', ((env'', ctx'), imps') = interp_context_evars ~impl_env evdref env' after in let annot = Option.map (fun _ -> List.length (assums_of_rel_context ctx)) fix.fix_annot in - ((env'', ctx' @ ctx), imps @ imps', annot) - -let interp_fix_ccl evdref (env,_) fix = - interp_type_evars evdref env fix.fix_type + ((env'', ctx' @ ctx), (impl_env',imps @ imps'), annot) + +let interp_fix_ccl evdref impls (env,_) fix = + interp_type_evars_impls ~impls ~evdref ~fail_evar:false env fix.fix_type let interp_fix_body evdref env_rec impls (_,ctx) fix ccl = Option.map (fun body -> @@ -514,11 +518,15 @@ let interp_recursive isfix fixl notations = (* Interp arities allowing for unresolved types *) let evdref = ref Evd.empty in - let fixctxs, fiximps, fixannots = + let fixctxs, fiximppairs, fixannots = list_split3 (List.map (interp_fix_context evdref env isfix) fixl) in - let fixccls = List.map2 (interp_fix_ccl evdref) fixctxs fixl in + let fixctximpenvs, fixctximps = List.split fiximppairs in + let fixccls,fixcclimps = List.split (list_map3 (interp_fix_ccl evdref) fixctximpenvs fixctxs fixl) in let fixtypes = List.map2 build_fix_type fixctxs fixccls in let fixtypes = List.map (nf_evar !evdref) fixtypes in + let fiximps = list_map3 + (fun ctximps cclimps (_,ctx) -> ctximps@(Impargs.lift_implicits (List.length ctx) cclimps)) + fixctximps fixcclimps fixctxs in let env_rec = push_named_types env fixnames fixtypes in (* Get interpretation metadatas *) @@ -526,9 +534,11 @@ let interp_recursive isfix fixl notations = (* Interp bodies with rollback because temp use of notations/implicit *) let fixdefs = - States.with_state_protection (fun () -> + Metasyntax.with_syntax_protection (fun () -> List.iter (Metasyntax.set_notation_for_interpretation impls) notations; - list_map3 (interp_fix_body evdref env_rec impls) fixctxs fixl fixccls) + list_map4 + (fun fixctximpenv -> interp_fix_body evdref env_rec (Idmap.fold Idmap.add fixctximpenv impls)) + fixctximpenvs fixctxs fixl fixccls) () in (* Instantiate evars and check all are resolved *) @@ -536,7 +546,7 @@ let interp_recursive isfix fixl notations = let fixdefs = List.map (Option.map (nf_evar evd)) fixdefs in let fixtypes = List.map (nf_evar evd) fixtypes in let fixctxnames = List.map (fun (_,ctx) -> List.map pi1 ctx) fixctxs in - let evd = Typeclasses.resolve_typeclasses ~onlyargs:false ~fail:true env evd in + let evd = Typeclasses.resolve_typeclasses ~filter:Typeclasses.no_goals ~fail:true env evd in List.iter (Option.iter (check_evars env_rec Evd.empty evd)) fixdefs; List.iter (check_evars env Evd.empty evd) fixtypes; if not (List.mem None fixdefs) then begin diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 76e9c2fe..a60e0d82 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -247,10 +247,13 @@ let parse_args arglist = | "-compat" :: [] -> usage () | "-vm" :: rem -> use_vm := true; parse rem - | "-emacs" :: rem -> Flags.print_emacs := true; Pp.make_pp_emacs(); parse rem + | "-emacs" :: rem -> + Flags.print_emacs := true; Pp.make_pp_emacs(); + Vernacentries.qed_display_script := false; + parse rem | "-emacs-U" :: rem -> warning "Obsolete option \"-emacs-U\", use -emacs instead."; - Flags.print_emacs := true; Pp.make_pp_emacs(); parse rem + parse ("-emacs" :: rem) | "-unicode" :: rem -> add_require "Utf8_core"; parse rem @@ -326,6 +329,7 @@ let init arglist = if_verbose print_header (); init_load_path (); inputstate (); + Mltop.init_known_plugins (); set_vm_opt (); engage (); if (not !batch_mode|| !compile_list=[]) && Global.env_is_empty() then @@ -349,7 +353,8 @@ let init arglist = Pp.ppnl (with_option raw_print Prettyp.print_full_pure_context ()); Profile.print_profile (); exit 0); - Lib.declare_initial_state () + (* We initialize the command history stack with a first entry *) + Backtrack.mark_command Vernacexpr.VernacNop let init_toplevel = init diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index 1bd68014..958e3dcb 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -31,7 +31,6 @@ open Evd let pr_lconstr c = quote (pr_lconstr c) let pr_lconstr_env e c = quote (pr_lconstr_env e c) -let pr_lconstr_env_at_top e c = quote (pr_lconstr_env_at_top e c) let pr_ljudge_env e c = let v,t = pr_ljudge_env e c in (quote v,quote t) let pr_db env i = @@ -696,8 +695,14 @@ let explain_no_instance env (_,id) l = str "applied to arguments" ++ spc () ++ prlist_with_sep pr_spc (pr_lconstr_env env) l +let is_goal_evar evi = match evi.evar_source with (_, GoalEvar) -> true | _ -> false + let pr_constraints printenv env evm = let evm = Evd.undefined_evars (Evarutil.nf_evar_map_undefined evm) in + let evm = fold_undefined + (fun ev evi evm' -> + if is_goal_evar evi then Evd.remove evm' ev else evm') evm evm + in let l = Evd.to_list evm in let (ev, evi) = List.hd l in if List.for_all (fun (ev', evi') -> @@ -819,8 +824,12 @@ let error_ill_formed_constructor env id c v nparams nargs = else mt()) ++ str "." +let pr_ltype_using_barendregt_convention_env env c = + (* Use goal_concl_style as an approximation of Barendregt's convention (?) *) + quote (pr_goal_concl_style_env env c) + let error_bad_ind_parameters env c n v1 v2 = - let pc = pr_lconstr_env_at_top env c in + let pc = pr_ltype_using_barendregt_convention_env env c in let pv1 = pr_lconstr_env env v1 in let pv2 = pr_lconstr_env env v2 in str "Last occurrence of " ++ pv2 ++ str " must have " ++ pv1 ++ @@ -978,7 +987,8 @@ let explain_pattern_matching_error env = function let explain_reduction_tactic_error = function | Tacred.InvalidAbstraction (env,c,(env',e)) -> - str "The abstracted term" ++ spc () ++ pr_lconstr_env_at_top env c ++ + str "The abstracted term" ++ spc () ++ + quote (pr_goal_concl_style_env env c) ++ spc () ++ str "is not well typed." ++ fnl () ++ explain_type_error env' Evd.empty e diff --git a/toplevel/ide_intf.ml b/toplevel/ide_intf.ml index fc8ffa25..9ba3d8b4 100644 --- a/toplevel/ide_intf.ml +++ b/toplevel/ide_intf.ml @@ -6,6 +6,12 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +(** Protocol version of this file. This is the date of the last modification. *) + +(** WARNING: TO BE UPDATED WHEN MODIFIED! *) + +let protocol_version = "20120511" + (** * Interface of calls to Coq by CoqIde *) open Xml_parser @@ -22,10 +28,32 @@ type 'a call = | Evars | Hints | Status + | Search of search_flags | GetOptions | SetOptions of (option_name * option_value) list | InLoadPath of string | MkCases of string + | Quit + | About + +(** The structure that coqtop should implement *) + +type handler = { + interp : raw * verbose * string -> string; + rewind : int -> int; + goals : unit -> goals option; + evars : unit -> evar list option; + hints : unit -> (hint list * hint) option; + status : unit -> status; + search : search_flags -> search_answer list; + get_options : unit -> (option_name * option_state) list; + set_options : (option_name * option_value) list -> unit; + inloadpath : string -> bool; + mkcases : string -> string list list; + quit : unit -> unit; + about : unit -> coq_info; + handle_exn : exn -> location * string; +} (** The actual calls *) @@ -35,10 +63,12 @@ let goals : goals option call = Goal let evars : evar list option call = Evars let hints : (hint list * hint) option call = Hints let status : status call = Status +let search flags : search_answer list call = Search flags let get_options : (option_name * option_state) list call = GetOptions let set_options l : unit call = SetOptions l let inloadpath s : bool call = InLoadPath s let mkcases s : string list list call = MkCases s +let quit : unit call = Quit (** * Coq answers to CoqIde *) @@ -51,10 +81,13 @@ let abstract_eval_call handler c = | Evars -> Obj.magic (handler.evars () : evar list option) | Hints -> Obj.magic (handler.hints () : (hint list * hint) option) | Status -> Obj.magic (handler.status () : status) + | Search flags -> Obj.magic (handler.search flags : search_answer list) | GetOptions -> Obj.magic (handler.get_options () : (option_name * option_state) list) | SetOptions opts -> Obj.magic (handler.set_options opts : unit) | InLoadPath s -> Obj.magic (handler.inloadpath s : bool) | MkCases s -> Obj.magic (handler.mkcases s : string list list) + | Quit -> Obj.magic (handler.quit () : unit) + | About -> Obj.magic (handler.about () : coq_info) in Good res with e -> let (l, str) = handler.handle_exn e in @@ -178,6 +211,44 @@ let to_option_state = function } | _ -> raise Marshal_error +let of_search_constraint = function +| Name_Pattern s -> + constructor "search_constraint" "name_pattern" [of_string s] +| Type_Pattern s -> + constructor "search_constraint" "type_pattern" [of_string s] +| SubType_Pattern s -> + constructor "search_constraint" "subtype_pattern" [of_string s] +| In_Module m -> + constructor "search_constraint" "in_module" [of_list of_string m] +| Include_Blacklist -> + constructor "search_constraint" "include_blacklist" [] + +let to_search_constraint xml = do_match xml "search_constraint" + (fun s args -> match s with + | "name_pattern" -> Name_Pattern (to_string (singleton args)) + | "type_pattern" -> Type_Pattern (to_string (singleton args)) + | "subtype_pattern" -> SubType_Pattern (to_string (singleton args)) + | "in_module" -> In_Module (to_list to_string (singleton args)) + | "include_blacklist" -> Include_Blacklist + | _ -> raise Marshal_error) + +let of_search_answer ans = + let path = of_list of_string ans.search_answer_full_path in + let name = of_string ans.search_answer_base_name in + let tpe = of_string ans.search_answer_type in + Element ("search_answer", [], [path; name; tpe]) + +let to_search_answer = function +| Element ("search_answer", [], [path; name; tpe]) -> + let path = to_list to_string path in + let name = to_string name in + let tpe = to_string tpe in { + search_answer_full_path = path; + search_answer_base_name = name; + search_answer_type = tpe; + } +| _ -> raise Marshal_error + let of_value f = function | Good x -> Element ("value", ["val", "good"], [f x]) | Fail (loc, msg) -> @@ -218,6 +289,9 @@ let of_call = function Element ("call", ["val", "hints"], []) | Status -> Element ("call", ["val", "status"], []) +| Search flags -> + let args = List.map (of_pair of_search_constraint of_bool) flags in + Element ("call", ["val", "search"], args) | GetOptions -> Element ("call", ["val", "getoptions"], []) | SetOptions opts -> @@ -227,6 +301,10 @@ let of_call = function Element ("call", ["val", "inloadpath"], [PCData file]) | MkCases ind -> Element ("call", ["val", "mkcases"], [PCData ind]) +| Quit -> + Element ("call", ["val", "quit"], []) +| About -> + Element ("call", ["val", "about"], []) let to_call = function | Element ("call", attrs, l) -> @@ -242,6 +320,9 @@ let to_call = function | "goal" -> Goal | "evars" -> Evars | "status" -> Status + | "search" -> + let args = List.map (to_pair to_search_constraint to_bool) l in + Search args | "getoptions" -> GetOptions | "setoptions" -> let args = List.map (to_pair (to_list to_string) to_option_value) l in @@ -249,6 +330,8 @@ let to_call = function | "inloadpath" -> InLoadPath (raw_string l) | "mkcases" -> MkCases (raw_string l) | "hints" -> Hints + | "quit" -> Quit + | "about" -> About | _ -> raise Marshal_error end | _ -> raise Marshal_error @@ -275,13 +358,15 @@ let to_evar = function let of_goal g = let hyp = of_list of_string g.goal_hyp in let ccl = of_string g.goal_ccl in - Element ("goal", [], [hyp; ccl]) + let id = of_string g.goal_id in + Element ("goal", [], [id; hyp; ccl]) let to_goal = function -| Element ("goal", [], [hyp; ccl]) -> +| Element ("goal", [], [id; hyp; ccl]) -> let hyp = to_list to_string hyp in let ccl = to_string ccl in - { goal_hyp = hyp; goal_ccl = ccl } + let id = to_string id in + { goal_hyp = hyp; goal_ccl = ccl; goal_id = id; } | _ -> raise Marshal_error let of_goals g = @@ -296,6 +381,23 @@ let to_goals = function { fg_goals = fg; bg_goals = bg; } | _ -> raise Marshal_error +let of_coq_info info = + let version = of_string info.coqtop_version in + let protocol = of_string info.protocol_version in + let release = of_string info.release_date in + let compile = of_string info.compile_date in + Element ("coq_info", [], [version; protocol; release; compile]) + +let to_coq_info = function +| Element ("coq_info", [], [version; protocol; release; compile]) -> + { + coqtop_version = to_string version; + protocol_version = to_string protocol; + release_date = to_string release; + compile_date = to_string compile; + } +| _ -> raise Marshal_error + let of_hints = let of_hint = of_list (of_pair of_string of_string) in of_option (of_pair (of_list of_hint) of_hint) @@ -308,10 +410,13 @@ let of_answer (q : 'a call) (r : 'a value) = | Evars -> Obj.magic (of_option (of_list of_evar) : evar list option -> xml) | Hints -> Obj.magic (of_hints : (hint list * hint) option -> xml) | Status -> Obj.magic (of_status : status -> xml) + | Search _ -> Obj.magic (of_list of_search_answer : search_answer list -> xml) | GetOptions -> Obj.magic (of_list (of_pair (of_list of_string) of_option_state) : (option_name * option_state) list -> xml) | SetOptions _ -> Obj.magic (fun _ -> Element ("unit", [], [])) | InLoadPath _ -> Obj.magic (of_bool : bool -> xml) | MkCases _ -> Obj.magic (of_list (of_list of_string) : string list list -> xml) + | Quit -> Obj.magic (fun _ -> Element ("unit", [], [])) + | About -> Obj.magic (of_coq_info : coq_info -> xml) in of_value convert r @@ -331,6 +436,8 @@ let to_answer xml = | "evar" -> Obj.magic (to_evar elt : evar) | "option_value" -> Obj.magic (to_option_value elt : option_value) | "option_state" -> Obj.magic (to_option_state elt : option_state) + | "coq_info" -> Obj.magic (to_coq_info elt : coq_info) + | "search_answer" -> Obj.magic (to_search_answer elt : search_answer) | _ -> raise Marshal_error end | _ -> raise Marshal_error @@ -370,10 +477,13 @@ let pr_call = function | Evars -> "EVARS" | Hints -> "HINTS" | Status -> "STATUS" + | Search _ -> "SEARCH" | GetOptions -> "GETOPTIONS" | SetOptions l -> "SETOPTIONS" ^ " [" ^ pr_setoptions l ^ "]" | InLoadPath s -> "INLOADPATH "^s | MkCases s -> "MKCASES "^s + | Quit -> "QUIT" + | About -> "ABOUT" let pr_value_gen pr = function | Good v -> "GOOD " ^ pr v @@ -428,7 +538,11 @@ let pr_full_value call value = | Evars -> pr_value_gen pr_evars (Obj.magic value : evar list option value) | Hints -> pr_value value | Status -> pr_value_gen pr_status (Obj.magic value : status value) + | Search _ -> pr_value value | GetOptions -> pr_value_gen pr_getoptions (Obj.magic value : (option_name * option_state) list value) | SetOptions _ -> pr_value value | InLoadPath s -> pr_value_gen pr_bool (Obj.magic value : bool value) | MkCases s -> pr_value_gen pr_mkcases (Obj.magic value : string list list value) + | Quit -> pr_value value + | About -> pr_value value + diff --git a/toplevel/ide_intf.mli b/toplevel/ide_intf.mli index 69204da1..deee50e5 100644 --- a/toplevel/ide_intf.mli +++ b/toplevel/ide_intf.mli @@ -65,8 +65,34 @@ val get_options : (option_name * option_state) list call to check that everything is correct. *) val set_options : (option_name * option_value) list -> unit call +(** Quit gracefully the interpreter. *) +val quit : unit call + +(** The structure that coqtop should implement *) + +type handler = { + interp : raw * verbose * string -> string; + rewind : int -> int; + goals : unit -> goals option; + evars : unit -> evar list option; + hints : unit -> (hint list * hint) option; + status : unit -> status; + search : search_flags -> search_answer list; + get_options : unit -> (option_name * option_state) list; + set_options : (option_name * option_value) list -> unit; + inloadpath : string -> bool; + mkcases : string -> string list list; + quit : unit -> unit; + about : unit -> coq_info; + handle_exn : exn -> location * string; +} + val abstract_eval_call : handler -> 'a call -> 'a value +(** * Protocol version *) + +val protocol_version : string + (** * XML data marshalling *) exception Marshal_error diff --git a/toplevel/ide_slave.ml b/toplevel/ide_slave.ml index 42ecb75b..93ad052c 100644 --- a/toplevel/ide_slave.ml +++ b/toplevel/ide_slave.ml @@ -20,12 +20,6 @@ open Namegen the only one using this mode, but we try here to be as generic as possible, so this may change in the future... *) - -(** Comment the next line for displaying some more debug messages *) - -let prerr_endline _ = () - - (** Signal handling: we postpone ^C during input and output phases, but make it directly raise a Sys.Break during evaluation of the request. *) @@ -59,6 +53,8 @@ let init_stdout,read_stdout = let r = Buffer.contents out_buff in Buffer.clear out_buff; r) +let pr_debug s = + if !Flags.debug then Printf.eprintf "[pid %d] %s\n%!" (Unix.getpid ()) s (** Categories of commands *) @@ -73,202 +69,29 @@ let coqide_known_option table = List.mem table [ ["Printing";"Existential";"Instances"]; ["Printing";"Universes"]] -type command_attribute = - NavigationCommand | QueryCommand | DebugCommand | KnownOptionCommand - | OtherStatePreservingCommand | GoalStartingCommand | SolveCommand - | ProofEndingCommand - -let rec attribute_of_vernac_command = function - (* Control *) - | VernacTime com -> attribute_of_vernac_command com - | VernacTimeout(_,com) -> attribute_of_vernac_command com - | VernacFail com -> attribute_of_vernac_command com - | VernacList _ -> [] (* unsupported *) - | VernacLoad _ -> [] - - (* Syntax *) - | VernacTacticNotation _ -> [] - | VernacSyntaxExtension _ -> [] - | VernacDelimiters _ -> [] - | VernacBindScope _ -> [] - | VernacOpenCloseScope _ -> [] - | VernacArgumentsScope _ -> [] - | VernacInfix _ -> [] - | VernacNotation _ -> [] - - (* Gallina *) - | VernacDefinition (_,_,DefineBody _,_) -> [] - | VernacDefinition (_,_,ProveBody _,_) -> [GoalStartingCommand] - | VernacStartTheoremProof _ -> [GoalStartingCommand] - | VernacEndProof _ -> [ProofEndingCommand] - | VernacExactProof _ -> [ProofEndingCommand] - - | VernacAssumption _ -> [] - | VernacInductive _ -> [] - | VernacFixpoint _ -> [] - | VernacCoFixpoint _ -> [] - | VernacScheme _ -> [] - | VernacCombinedScheme _ -> [] - - (* Modules *) - | VernacDeclareModule _ -> [] - | VernacDefineModule _ -> [] - | VernacDeclareModuleType _ -> [] - | VernacInclude _ -> [] - - (* Gallina extensions *) - | VernacBeginSection _ -> [] - | VernacEndSegment _ -> [] - | VernacRequire _ -> [] - | VernacImport _ -> [] - | VernacCanonical _ -> [] - | VernacCoercion _ -> [] - | VernacIdentityCoercion _ -> [] - - (* Type classes *) - | VernacInstance _ -> [] - | VernacContext _ -> [] - | VernacDeclareInstances _ -> [] - | VernacDeclareClass _ -> [] - - (* Solving *) - | VernacSolve _ -> [SolveCommand] - | VernacSolveExistential _ -> [SolveCommand] - - (* Auxiliary file and library management *) - | VernacRequireFrom _ -> [] - | VernacAddLoadPath _ -> [] - | VernacRemoveLoadPath _ -> [] - | VernacAddMLPath _ -> [] - | VernacDeclareMLModule _ -> [] - | VernacChdir o -> - (* TODO: [Chdir d] is currently not undo-able (not stored in coq state). - But if we register [Chdir] in the state, loading [initial.coq] will - wrongly cd to the compile-time directory at each coqtop launch. *) - if o = None then [QueryCommand] else [] - - (* State management *) - | VernacWriteState _ -> [] - | VernacRestoreState _ -> [] - - (* Resetting *) - | VernacRemoveName _ -> [NavigationCommand] - | VernacResetName _ -> [NavigationCommand] - | VernacResetInitial -> [NavigationCommand] - | VernacBack _ -> [NavigationCommand] - | VernacBackTo _ -> [NavigationCommand] - - (* Commands *) - | VernacDeclareTacticDefinition _ -> [] - | VernacCreateHintDb _ -> [] - | VernacRemoveHints _ -> [] - | VernacHints _ -> [] - | VernacSyntacticDefinition _ -> [] - | VernacDeclareImplicits _ -> [] - | VernacArguments _ -> [] - | VernacDeclareReduction _ -> [] - | VernacReserve _ -> [] - | VernacGeneralizable _ -> [] - | VernacSetOpacity _ -> [] - | VernacSetOption (_,["Ltac";"Debug"], _) -> [DebugCommand] - | VernacSetOption (_,o,BoolValue true) | VernacUnsetOption (_,o) -> - if coqide_known_option o then [KnownOptionCommand] else [] - | VernacSetOption _ -> [] - | VernacRemoveOption _ -> [] - | VernacAddOption _ -> [] - | VernacMemOption _ -> [QueryCommand] - - | VernacPrintOption _ -> [QueryCommand] - | VernacCheckMayEval _ -> [QueryCommand] - | VernacGlobalCheck _ -> [QueryCommand] - | VernacPrint _ -> [QueryCommand] - | VernacSearch _ -> [QueryCommand] - | VernacLocate _ -> [QueryCommand] - - | VernacComments _ -> [OtherStatePreservingCommand] - | VernacNop -> [OtherStatePreservingCommand] - - (* Proof management *) - | VernacGoal _ -> [GoalStartingCommand] - - | VernacAbort _ -> [] - | VernacAbortAll -> [NavigationCommand] - | VernacRestart -> [NavigationCommand] - | VernacSuspend -> [NavigationCommand] - | VernacResume _ -> [NavigationCommand] - | VernacUndo _ -> [NavigationCommand] - | VernacUndoTo _ -> [NavigationCommand] - | VernacBacktrack _ -> [NavigationCommand] - - | VernacFocus _ -> [SolveCommand] - | VernacUnfocus -> [SolveCommand] - | VernacShow _ -> [OtherStatePreservingCommand] - | VernacCheckGuard -> [OtherStatePreservingCommand] - | VernacProof (None, None) -> [OtherStatePreservingCommand] - | VernacProof _ -> [] - - | VernacProofMode _ -> [] - | VernacBullet _ -> [SolveCommand] - | VernacSubproof _ -> [SolveCommand] - | VernacEndSubproof -> [SolveCommand] - - (* Toplevel control *) - | VernacToplevelControl _ -> [] - - (* Extensions *) - | VernacExtend ("Subtac_Obligations", _) -> [GoalStartingCommand] - | VernacExtend _ -> [] - -let is_vernac_navigation_command com = - List.mem NavigationCommand (attribute_of_vernac_command com) - -let is_vernac_query_command com = - List.mem QueryCommand (attribute_of_vernac_command com) - -let is_vernac_known_option_command com = - List.mem KnownOptionCommand (attribute_of_vernac_command com) - -let is_vernac_debug_command com = - List.mem DebugCommand (attribute_of_vernac_command com) - -let is_vernac_goal_printing_command com = - let attribute = attribute_of_vernac_command com in - List.mem GoalStartingCommand attribute or - List.mem SolveCommand attribute - -let is_vernac_state_preserving_command com = - let attribute = attribute_of_vernac_command com in - List.mem OtherStatePreservingCommand attribute or - List.mem QueryCommand attribute - -let is_vernac_tactic_command com = - List.mem SolveCommand (attribute_of_vernac_command com) - -let is_vernac_proof_ending_command com = - List.mem ProofEndingCommand (attribute_of_vernac_command com) - - -(** Command history stack - - We maintain a stack of the past states of the system. Each - successfully interpreted command adds a [reset_info] element - to this stack, storing what were the (label / open proofs / - current proof depth) just _before_ the interpretation of this - command. A label is just an integer (cf. BackTo and Bactrack - vernac commands). -*) - -type reset_info = { label : int; proofs : identifier list; depth : int } - -let com_stk = Stack.create () - -let compute_reset_info () = - { label = Lib.current_command_label (); - proofs = Pfedit.get_all_proof_names (); - depth = max 0 (Pfedit.current_proof_depth ()) } - - -(** Interpretation (cf. [Ide_intf.interp]) *) +let is_known_option cmd = match cmd with + | VernacSetOption (_,o,BoolValue true) + | VernacUnsetOption (_,o) -> coqide_known_option o + | _ -> false + +let is_debug cmd = match cmd with + | VernacSetOption (_,["Ltac";"Debug"], _) -> true + | _ -> false + +let is_query cmd = match cmd with + | VernacChdir None + | VernacMemOption _ + | VernacPrintOption _ + | VernacCheckMayEval _ + | VernacGlobalCheck _ + | VernacPrint _ + | VernacSearch _ + | VernacLocate _ -> true + | _ -> false + +let is_undo cmd = match cmd with + | VernacUndo _ | VernacUndoTo _ -> true + | _ -> false (** Check whether a command is forbidden by CoqIDE *) @@ -276,82 +99,28 @@ let coqide_cmd_checks (loc,ast) = let user_error s = raise (Loc.Exc_located (loc, Util.UserError ("CoqIde", str s))) in - if is_vernac_debug_command ast then + if is_debug ast then user_error "Debug mode not available within CoqIDE"; - if is_vernac_navigation_command ast then - user_error "Use CoqIDE navigation instead"; - if is_vernac_known_option_command ast then + if is_known_option ast then user_error "Use CoqIDE display menu instead"; - if is_vernac_query_command ast then + if is_navigation_vernac ast then + user_error "Use CoqIDE navigation instead"; + if is_undo ast then + msgerrnl (str "Warning: rather use CoqIDE navigation instead"); + if is_query ast then msgerrnl (str "Warning: query commands should not be inserted in scripts") -let raw_eval_expr = Vernac.eval_expr - -let eval_expr loc_ast = - let rewind_info = compute_reset_info () in - raw_eval_expr loc_ast; - Stack.push rewind_info com_stk +(** Interpretation (cf. [Ide_intf.interp]) *) let interp (raw,verbosely,s) = - if not raw then (prerr_endline "Starting interp..."; prerr_endline s); let pa = Pcoq.Gram.parsable (Stream.of_string s) in let loc_ast = Vernac.parse_sentence (pa,None) in if not raw then coqide_cmd_checks loc_ast; - (* We run tactics silently, since we will query the goal state later. - Otherwise, we honor the IDE verbosity flag. *) - Flags.make_silent - (is_vernac_goal_printing_command (snd loc_ast) || not verbosely); - if raw then raw_eval_expr loc_ast else eval_expr loc_ast; + Flags.make_silent (not verbosely); + Vernac.eval_expr ~preserving:raw loc_ast; Flags.make_silent true; - if not raw then prerr_endline ("...Done with interp of : "^s); read_stdout () - -(** Backtracking (cf. [Ide_intf.rewind]). - We now rely on the [Backtrack] command just as ProofGeneral. *) - -let rewind count = - if count = 0 then 0 - else - let current_proofs = Pfedit.get_all_proof_names () - in - (* 1) First, let's pop the history stack exactly [count] times. - NB: Normally, the IDE will not rewind by more than the numbers - of already interpreted commands, hence no risk of [Stack.Empty]. - *) - let initial_target = - for i = 1 to count - 1 do ignore (Stack.pop com_stk) done; - Stack.pop com_stk - in - (* 2) Backtrack by enough additional steps to avoid re-opening proofs. - Typically, when a Qed has been crossed, we backtrack to the proof start. - NB: We cannot reach the empty stack, since the oldest [reset_info] - in the history cannot have opened proofs. - *) - let already_opened p = List.mem p current_proofs in - let rec extra_back n target = - if List.for_all already_opened target.proofs then n,target - else extra_back (n+1) (Stack.pop com_stk) - in - let extra_count, target = extra_back 0 initial_target - in - (* 3) Now that [target.proofs] is a subset of the opened proofs before - the rewind, we simply abort the extra proofs (if any). - NB: It is critical here that proofs are nested in a regular way - (i.e. no Resume or Suspend, as enforced above). This way, we can simply - count the extra proofs to abort instead of taking care of their names. - *) - let naborts = List.length current_proofs - List.length target.proofs - in - (* 4) We are now ready to call [Backtrack] *) - prerr_endline ("Rewind to state "^string_of_int target.label^ - ", proof depth "^string_of_int target.depth^ - ", num of aborts "^string_of_int naborts); - Vernacentries.vernac_backtrack target.label target.depth naborts; - Lib.mark_end_of_command (); (* We've short-circuited Vernac.eval_expr *) - extra_count - - (** Goal display *) let hyp_next_tac sigma env (id,_,ast) = @@ -404,16 +173,17 @@ let concl_next_tac sigma concl = let process_goal sigma g = let env = Goal.V82.env sigma g in + let id = Goal.uid g in let ccl = let norm_constr = Reductionops.nf_evar sigma (Goal.V82.concl sigma g) in - string_of_ppcmds (pr_ltype_env_at_top env norm_constr) in + string_of_ppcmds (pr_goal_concl_style_env env norm_constr) in let process_hyp h_env d acc = let d = Term.map_named_declaration (Reductionops.nf_evar sigma) d in (string_of_ppcmds (pr_var_decl h_env d)) :: acc in (* (string_of_ppcmds (pr_var_decl h_env d), hyp_next_tac sigma h_env d)::acc in *) let hyps = List.rev (Environ.fold_named_context process_hyp env ~init: []) in - { Interface.goal_hyp = hyps; Interface.goal_ccl = ccl } + { Interface.goal_hyp = hyps; Interface.goal_ccl = ccl; Interface.goal_id = id; } (* hyps,(ccl,concl_next_tac sigma g)) *) let goals () = @@ -472,6 +242,82 @@ let status () = in { Interface.status_path = path; Interface.status_proofname = proof } +(** This should be elsewhere... *) +let search flags = + let env = Global.env () in + let rec extract_flags name tpe subtpe mods blacklist = function + | [] -> (name, tpe, subtpe, mods, blacklist) + | (Interface.Name_Pattern s, b) :: l -> + let regexp = + try Str.regexp s + with _ -> Util.error ("Invalid regexp: " ^ s) + in + extract_flags ((regexp, b) :: name) tpe subtpe mods blacklist l + | (Interface.Type_Pattern s, b) :: l -> + let constr = Pcoq.parse_string Pcoq.Constr.lconstr_pattern s in + let (_, pat) = Constrintern.intern_constr_pattern Evd.empty env constr in + extract_flags name ((pat, b) :: tpe) subtpe mods blacklist l + | (Interface.SubType_Pattern s, b) :: l -> + let constr = Pcoq.parse_string Pcoq.Constr.lconstr_pattern s in + let (_, pat) = Constrintern.intern_constr_pattern Evd.empty env constr in + extract_flags name tpe ((pat, b) :: subtpe) mods blacklist l + | (Interface.In_Module m, b) :: l -> + let path = String.concat "." m in + let m = Pcoq.parse_string Pcoq.Constr.global path in + let (_, qid) = Libnames.qualid_of_reference m in + let id = + try Nametab.full_name_module qid + with Not_found -> + Util.error ("Module " ^ path ^ " not found.") + in + extract_flags name tpe subtpe ((id, b) :: mods) blacklist l + | (Interface.Include_Blacklist, b) :: l -> + extract_flags name tpe subtpe mods b l + in + let (name, tpe, subtpe, mods, blacklist) = + extract_flags [] [] [] [] false flags + in + let filter_function ref env constr = + let id = Names.string_of_id (Nametab.basename_of_global ref) in + let path = Libnames.dirpath (Nametab.path_of_global ref) in + let toggle x b = if x then b else not b in + let match_name (regexp, flag) = + toggle (Str.string_match regexp id 0) flag + in + let match_type (pat, flag) = + toggle (Matching.is_matching pat constr) flag + in + let match_subtype (pat, flag) = + toggle (Matching.is_matching_appsubterm ~closed:false pat constr) flag + in + let match_module (mdl, flag) = + toggle (Libnames.is_dirpath_prefix_of mdl path) flag + in + let in_blacklist = + blacklist || (Search.filter_blacklist ref env constr) + in + List.for_all match_name name && + List.for_all match_type tpe && + List.for_all match_subtype subtpe && + List.for_all match_module mods && in_blacklist + in + let ans = ref [] in + let print_function ref env constr = + let name = Names.string_of_id (Nametab.basename_of_global ref) in + let make_path = Names.string_of_id in + let path = + List.rev_map make_path (Names.repr_dirpath (Nametab.dirpath_of_global ref)) + in + let answer = { + Interface.search_answer_full_path = path; + Interface.search_answer_base_name = name; + Interface.search_answer_type = string_of_ppcmds (pr_lconstr_env env constr); + } in + ans := answer :: !ans; + in + let () = Search.gen_filtered_search filter_function print_function in + !ans + let get_options () = let table = Goptions.get_tables () in let fold key state accu = (key, state) :: accu in @@ -485,13 +331,31 @@ let set_options options = in List.iter iter options +let about () = { + Interface.coqtop_version = Coq_config.version; + Interface.protocol_version = Ide_intf.protocol_version; + Interface.release_date = Coq_config.date; + Interface.compile_date = Coq_config.compile_date; +} + (** Grouping all call handlers together + error handling *) +exception Quit + let eval_call c = let rec handle_exn e = catch_break := false; - let pr_exn e = string_of_ppcmds (Errors.print e) in + let pr_exn e = (read_stdout ())^("\n"^(string_of_ppcmds (Errors.print e))) in match e with + | Quit -> + (* Here we do send an acknowledgement message to prove everything went + OK. *) + let dummy = Interface.Good () in + let xml_answer = Ide_intf.of_answer Ide_intf.quit dummy in + let () = Xml_utils.print_xml !orig_stdout xml_answer in + let () = flush !orig_stdout in + let () = pr_debug "Exiting gracefully." in + exit 0 | Vernacexpr.Drop -> None, "Drop is not allowed by coqide!" | Vernacexpr.Quit -> None, "Quit is not allowed by coqide!" | Vernac.DuringCommandInterp (_,inner) -> handle_exn inner @@ -508,17 +372,20 @@ let eval_call c = r in let handler = { - Interface.interp = interruptible interp; - Interface.rewind = interruptible rewind; - Interface.goals = interruptible goals; - Interface.evars = interruptible evars; - Interface.hints = interruptible hints; - Interface.status = interruptible status; - Interface.inloadpath = interruptible inloadpath; - Interface.get_options = interruptible get_options; - Interface.set_options = interruptible set_options; - Interface.mkcases = interruptible Vernacentries.make_cases; - Interface.handle_exn = handle_exn; } + Ide_intf.interp = interruptible interp; + Ide_intf.rewind = interruptible Backtrack.back; + Ide_intf.goals = interruptible goals; + Ide_intf.evars = interruptible evars; + Ide_intf.hints = interruptible hints; + Ide_intf.status = interruptible status; + Ide_intf.search = interruptible search; + Ide_intf.inloadpath = interruptible inloadpath; + Ide_intf.get_options = interruptible get_options; + Ide_intf.set_options = interruptible set_options; + Ide_intf.mkcases = interruptible Vernacentries.make_cases; + Ide_intf.quit = (fun () -> raise Quit); + Ide_intf.about = interruptible about; + Ide_intf.handle_exn = handle_exn; } in (* If the messages of last command are still there, we remove them *) ignore (read_stdout ()); @@ -534,9 +401,6 @@ let eval_call c = between coqtop and ide. With marshalling, reading an answer to a different request could hang the ide... *) -let pr_debug s = - if !Flags.debug then Printf.eprintf "[pid %d] %s\n%!" (Unix.getpid ()) s - let fail err = Ide_intf.of_value (fun _ -> assert false) (Interface.Fail (None, err)) @@ -545,9 +409,9 @@ let loop () = let () = Xml_parser.check_eof p false in init_signal_handler (); catch_break := false; - (* ensure we have a command separator object (DOT) so that the first - command can be reseted. *) - Lib.mark_end_of_command(); + (* We'll handle goal fetching and display in our own way *) + Vernacentries.enable_goal_printing := false; + Vernacentries.qed_display_script := false; try while true do let xml_answer = diff --git a/toplevel/interface.mli b/toplevel/interface.mli index e1410f5b..f3374ab4 100644 --- a/toplevel/interface.mli +++ b/toplevel/interface.mli @@ -15,6 +15,8 @@ type verbose = bool (** The type of coqtop goals *) type goal = { + goal_id : string; + (** Unique goal identifier *) goal_hyp : string list; (** List of hypotheses *) goal_ccl : string; @@ -62,6 +64,35 @@ type option_state = Goptionstyp.option_state = { (** The current value of the option *) } +type search_constraint = +(** Whether the name satisfies a regexp (uses Ocaml Str syntax) *) +| Name_Pattern of string +(** Whether the object type satisfies a pattern *) +| Type_Pattern of string +(** Whether some subtype of object type satisfies a pattern *) +| SubType_Pattern of string +(** Whether the object pertains to a module *) +| In_Module of string list +(** Bypass the Search blacklist *) +| Include_Blacklist + +(** A list of search constraints; the boolean flag is set to [false] whenever + the flag should be negated. *) +type search_flags = (search_constraint * bool) list + +type search_answer = { + search_answer_full_path : string list; + search_answer_base_name : string; + search_answer_type : string; +} + +type coq_info = { + coqtop_version : string; + protocol_version : string; + release_date : string; + compile_date : string; +} + (** * Coq answers to CoqIde *) type location = (int * int) option (* start and end of the error *) @@ -69,19 +100,3 @@ type location = (int * int) option (* start and end of the error *) type 'a value = | Good of 'a | Fail of (location * string) - -(** * The structure that coqtop should implement *) - -type handler = { - interp : raw * verbose * string -> string; - rewind : int -> int; - goals : unit -> goals option; - evars : unit -> evar list option; - hints : unit -> (hint list * hint) option; - status : unit -> status; - get_options : unit -> (option_name * option_state) list; - set_options : (option_name * option_value) list -> unit; - inloadpath : string -> bool; - mkcases : string -> string list list; - handle_exn : exn -> location * string; -} diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index 6a4d7251..cdeff601 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -985,6 +985,18 @@ let inNotation : notation_obj -> obj = load_function = load_notation; classify_function = classify_notation} +(**********************************************************************) + +let with_lib_stk_protection f x = + let fs = Lib.freeze () in + try let a = f x in Lib.unfreeze fs; a + with e -> Lib.unfreeze fs; raise e + +let with_syntax_protection f x = + with_lib_stk_protection + (with_grammar_rule_protection + (with_notation_protection f)) x + (**********************************************************************) (* Recovering existing syntax *) diff --git a/toplevel/metasyntax.mli b/toplevel/metasyntax.mli index 4ee1310a..32568854 100644 --- a/toplevel/metasyntax.mli +++ b/toplevel/metasyntax.mli @@ -61,3 +61,5 @@ val add_syntactic_definition : identifier -> identifier list * constr_expr -> val print_grammar : string -> unit val check_infix_modifiers : syntax_modifier list -> unit + +val with_syntax_protection : ('a -> 'b) -> 'a -> 'b diff --git a/toplevel/mltop.ml4 b/toplevel/mltop.ml4 index ff3ce8a0..025c972f 100644 --- a/toplevel/mltop.ml4 +++ b/toplevel/mltop.ml4 @@ -235,9 +235,24 @@ let add_known_module mname = let module_is_known mname = Stringset.mem (String.capitalize mname) !known_loaded_modules +let known_loaded_plugins = ref Stringmap.empty + +let init_ml_object mname = + try Stringmap.find mname !known_loaded_plugins () + with Not_found -> () + let load_ml_object mname fname= dir_ml_load fname; - add_known_module mname + add_known_module mname; + init_ml_object mname + +let add_known_plugin init name = + let name = String.capitalize name in + add_known_module name; + known_loaded_plugins := Stringmap.add name init !known_loaded_plugins + +let init_known_plugins () = + Stringmap.iter (fun _ f -> f()) !known_loaded_plugins (* Summary of declared ML Modules *) @@ -260,7 +275,8 @@ let unfreeze_ml_modules x = load_ml_object mname fname else errorlabstrm "Mltop.unfreeze_ml_modules" - (str"Loading of ML object file forbidden in a native Coq."); + (str"Loading of ML object file forbidden in a native Coq.") + else init_ml_object mname; add_loaded_module mname) x @@ -290,7 +306,8 @@ let cache_ml_module_object (_,{mnames=mnames}) = raise e else (if_verbose msgnl (str" failed]"); - error ("Dynamic link not supported (module "^name^")"))) + error ("Dynamic link not supported (module "^name^")")) + else init_ml_object mname) mnames let classify_ml_module_object ({mlocal=mlocal} as o) = diff --git a/toplevel/mltop.mli b/toplevel/mltop.mli index 1e9c3b03..99b96ed7 100644 --- a/toplevel/mltop.mli +++ b/toplevel/mltop.mli @@ -51,6 +51,16 @@ val add_known_module : string -> unit val module_is_known : string -> bool val load_ml_object : string -> string -> unit +(* Declare a plugin and its initialization function. + * A plugin is just an ML module with an initialization function. + * Adding a known plugin implies adding it as a known ML module. + * The initialization function is granted to be called after Coq is fully + * bootstrapped, even if the plugin is statically linked with the toplevel *) +val add_known_plugin : (unit -> unit) -> string -> unit + +(* Calls all initialization functions in a non-specified order *) +val init_known_plugins : unit -> unit + (** Summary of Declared ML Modules *) val get_loaded_modules : unit -> string list val add_loaded_module : string -> unit diff --git a/toplevel/record.ml b/toplevel/record.ml index 86849cbb..0c55861f 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -81,8 +81,8 @@ let typecheck_params_and_fields id t ps nots fs = let newps = Evarutil.nf_rel_context_evar sigma newps in let newfs = Evarutil.nf_rel_context_evar sigma newfs in let ce t = Evarutil.check_evars env0 Evd.empty evars t in - List.iter (fun (n, b, t) -> Option.iter ce b; ce t) newps; - List.iter (fun (n, b, t) -> Option.iter ce b; ce t) newfs; + List.iter (fun (n, b, t) -> Option.iter ce b; ce t) (List.rev newps); + List.iter (fun (n, b, t) -> Option.iter ce b; ce t) (List.rev newfs); imps, newps, impls, newfs let degenerate_decl (na,b,t) = @@ -263,7 +263,7 @@ let declare_structure finite infer id idbuild paramimpls params arity fieldimpls begin match finite with | BiFinite -> if Termops.dependent (mkRel (nparams+1)) (it_mkProd_or_LetIn mkProp fields) then - error "Records declared with the keyword Record or Structure cannot be recursive. Maybe you meant to define an Inductive or CoInductive record." + error "Records declared with the keyword Record or Structure cannot be recursive. You can, however, define recursive records using the Inductive or CoInductive command." | _ -> () end; let mie = diff --git a/toplevel/search.mli b/toplevel/search.mli index d2d5c538..95827d54 100644 --- a/toplevel/search.mli +++ b/toplevel/search.mli @@ -33,6 +33,8 @@ val search_about : val filter_by_module_from_list : dir_path list * bool -> global_reference -> env -> 'a -> bool +val filter_blacklist : global_reference -> env -> constr -> bool + (** raw search functions can be used for various extensions. They are also used for pcoq. *) val gen_filtered_search : (global_reference -> env -> constr -> bool) -> diff --git a/toplevel/toplevel.ml b/toplevel/toplevel.ml index 699fd12f..8514872b 100644 --- a/toplevel/toplevel.ml +++ b/toplevel/toplevel.ml @@ -367,9 +367,6 @@ let do_vernac () = let rec loop () = Sys.catch_break true; - (* ensure we have a command separator object (DOT) so that the first - command can be reseted. *) - Lib.mark_end_of_command(); try reset_input_buffer stdin top_buffer; while true do do_vernac() done diff --git a/toplevel/toplevel.mllib b/toplevel/toplevel.mllib index 8b03e938..e1e349a6 100644 --- a/toplevel/toplevel.mllib +++ b/toplevel/toplevel.mllib @@ -13,6 +13,7 @@ Command Classes Record Ppvernac +Backtrack Vernacinterp Mltop Vernacentries diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index 84e20f5e..ed20fc60 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -51,6 +51,8 @@ let real_error = function | Error_in_file (_, _, e) -> e | e -> e +let user_error loc s = Util.user_err_loc (loc,"_",str s) + (** Timeout handling *) (** A global default timeout, controled by option "Set Default Timeout n". @@ -97,6 +99,18 @@ let restore_timeout = function (* restore handler *) Sys.set_signal Sys.sigalrm psh + +(* Open an utf-8 encoded file and skip the byte-order mark if any *) + +let open_utf8_file_in fname = + let is_bom s = + Char.code s.[0] = 0xEF && Char.code s.[1] = 0xBB && Char.code s.[2] = 0xBF + in + let in_chan = open_in fname in + let s = " " in + if input in_chan s 0 3 < 3 || not (is_bom s) then seek_in in_chan 0; + in_chan + (* Opening and closing a channel. Open it twice when verbose: the first channel is used to read the commands, and the second one to print them. Note: we could use only one thanks to seek_in, but seeking on and on in @@ -106,8 +120,9 @@ let open_file_twice_if verbosely fname = let paths = Library.get_load_paths () in let _,longfname = find_file_in_path ~warn:(Flags.is_verbose()) paths fname in - let in_chan = open_in longfname in - let verb_ch = if verbosely then Some (open_in longfname) else None in + let in_chan = open_utf8_file_in longfname in + let verb_ch = + if verbosely then Some (open_utf8_file_in longfname) else None in let po = Pcoq.Gram.parsable (Stream.of_channel in_chan) in (in_chan, longfname, (po, verb_ch)) @@ -166,7 +181,7 @@ let pr_new_syntax loc ocom = States.unfreeze fs; Format.set_formatter_out_channel stdout -let rec vernac_com interpfun (loc,com) = +let rec vernac_com interpfun checknav (loc,com) = let rec interp = function | VernacLoad (verbosely, fname) -> let fname = expand_path_macros fname in @@ -204,9 +219,13 @@ let rec vernac_com interpfun (loc,com) = | VernacList l -> List.iter (fun (_,v) -> interp v) l + | v when !just_parsing -> () + | VernacFail v -> - if not !just_parsing then begin try - interp v; raise HasNotFailed + begin try + (* If the command actually works, ignore its effects on the state *) + States.with_state_protection + (fun v -> interp v; raise HasNotFailed) v with e -> match real_error e with | HasNotFailed -> errorlabstrm "Fail" (str "The command has not failed !") @@ -219,22 +238,17 @@ let rec vernac_com interpfun (loc,com) = end | VernacTime v -> - if not !just_parsing then begin let tstart = System.get_time() in interp v; let tend = System.get_time() in msgnl (str"Finished transaction in " ++ System.fmt_time_difference tstart tend) - end | VernacTimeout(n,v) -> - if not !just_parsing then begin current_timeout := Some n; interp v - end | v -> - if not !just_parsing then let psh = default_set_timeout () in try States.with_heavy_rollback interpfun @@ -243,6 +257,7 @@ let rec vernac_com interpfun (loc,com) = with e -> restore_timeout psh; raise e in try + checknav loc com; current_timeout := !default_timeout; if do_beautify () then pr_new_syntax loc (Some com); interp com @@ -256,13 +271,17 @@ and read_vernac_file verbosely s = if verbosely then Vernacentries.interp else Flags.silently Vernacentries.interp in + let checknav loc cmd = + if is_navigation_vernac cmd then + user_error loc "Navigation commands forbidden in files" + in let (in_chan, fname, input) = open_file_twice_if verbosely s in try (* we go out of the following infinite loop when a End_of_input is * raised, which means that we raised the end of the file being loaded *) while true do - vernac_com interpfun (parse_sentence input); + vernac_com interpfun checknav (parse_sentence input); pp_flush () done with e -> (* whatever the exception *) @@ -273,15 +292,21 @@ and read_vernac_file verbosely s = if do_beautify () then pr_new_syntax (make_loc (max_int,max_int)) None | _ -> raise_with_file fname e +(** [eval_expr : ?preserving:bool -> Pp.loc * Vernacexpr.vernac_expr -> unit] + It executes one vernacular command. By default the command is + considered as non-state-preserving, in which case we add it to the + Backtrack stack (triggering a save of a frozen state and the generation + of a new state label). An example of state-preserving command is one coming + from the query panel of Coqide. *) -(* eval_expr : Util.loc * Vernacexpr.vernac_expr -> unit - * execute one vernacular command. Marks the end of the command in the lib_stk - * with a new label to make vernac undoing easier. Also freeze state to speed up - * backtracking. *) -let eval_expr last = - vernac_com Vernacentries.interp last; - Lib.add_frozen_state(); - Lib.mark_end_of_command() +let checknav loc ast = + if is_deep_navigation_vernac ast then + user_error loc "Navigation commands forbidden in nested commands" + +let eval_expr ?(preserving=false) loc_ast = + vernac_com Vernacentries.interp checknav loc_ast; + if not preserving && not (is_navigation_vernac (snd loc_ast)) then + Backtrack.mark_command (snd loc_ast) (* raw_do_vernac : Pcoq.Gram.parsable -> unit * vernac_step . parse_sentence *) @@ -317,5 +342,3 @@ let compile verbosely f = if !Flags.xml_export then !xml_end_library (); Dumpglob.end_dump_glob (); Library.save_library_to ldir (long_f_dot_v ^ "o") - - diff --git a/toplevel/vernac.mli b/toplevel/vernac.mli index d89e90d0..bcfe9b71 100644 --- a/toplevel/vernac.mli +++ b/toplevel/vernac.mli @@ -21,7 +21,14 @@ exception DuringCommandInterp of Util.loc * exn exception End_of_input val just_parsing : bool ref -val eval_expr : Util.loc * Vernacexpr.vernac_expr -> unit + +(** [eval_expr] executes one vernacular command. By default the command is + considered as non-state-preserving, in which case we add it to the + Backtrack stack (triggering a save of a frozen state and the generation + of a new state label). An example of state-preserving command is one coming + from the query panel of Coqide. *) + +val eval_expr : ?preserving:bool -> Util.loc * Vernacexpr.vernac_expr -> unit val raw_do_vernac : Pcoq.Gram.parsable -> unit (** Set XML hooks *) diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 5787feb0..2324e3e9 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -73,8 +73,9 @@ let show_node () = () let show_script () = - (* spiwack: show_script is currently not working *) - () + let prf = Pfedit.get_current_proof_name () in + let cmds = Backtrack.get_script prf in + msgnl (Util.prlist_with_sep Pp.fnl Ppvernac.pr_vernac cmds) let show_thesis () = msgnl (anomaly "TODO" ) @@ -91,7 +92,16 @@ let show_prooftree () = (* Spiwack: proof tree is currently not working *) () -let print_subgoals () = if_verbose (fun () -> msg (pr_open_subgoals ())) () +let enable_goal_printing = ref true + +let print_subgoals () = + if !enable_goal_printing && is_verbose () + then msg (pr_open_subgoals ()) + +let try_print_subgoals () = + Pp.flush_all(); + try print_subgoals () with Proof_global.NoCurrentProof | UserError _ -> () + (* Simulate the Intro(s) tactic *) @@ -341,7 +351,7 @@ let vernac_definition (local,k) (loc,id as lid) def hook = | None -> None | Some r -> let (evc,env)= get_current_context () in - Some (interp_redexp env evc r) in + Some (snd (interp_redexp env evc r)) in let ce,imps = interp_definition bl red_option c typ_opt in declare_definition id (local,k) ce imps hook) @@ -357,14 +367,21 @@ let vernac_start_proof kind l lettop hook = (str "Let declarations can only be used in proof editing mode."); start_proof_and_print (Global, Proof kind) l hook +let qed_display_script = ref true + let vernac_end_proof = function - | Admitted -> admit () + | Admitted -> + Backtrack.mark_unreachable [Pfedit.get_current_proof_name ()]; + admit () | Proved (is_opaque,idopt) -> - if not !Flags.print_emacs then if_verbose show_script (); - match idopt with + let prf = Pfedit.get_current_proof_name () in + if is_verbose () && !qed_display_script then (show_script (); msg (fnl())); + begin match idopt with | None -> save_named is_opaque | Some ((_,id),None) -> save_anonymous is_opaque id | Some ((_,id),Some kind) -> save_anonymous_with_strength kind is_opaque id + end; + Backtrack.mark_unreachable [prf] (* A stupid macro that should be replaced by ``Exact c. Save.'' all along the theories [??] *) @@ -723,28 +740,14 @@ let vernac_chdir = function (********************) (* State management *) -let abort_refine f x = - if Pfedit.refining() then delete_all_proofs (); - f x - (* used to be: error "Must save or abort current goal first" *) - -let vernac_write_state file = abort_refine States.extern_state file - -let vernac_restore_state file = abort_refine States.intern_state file - - -(*************) -(* Resetting *) - -let vernac_reset_name id = abort_refine Lib.reset_name id +let vernac_write_state file = + Pfedit.delete_all_proofs (); + States.extern_state file -let vernac_reset_initial () = abort_refine Lib.reset_initial () +let vernac_restore_state file = + Pfedit.delete_all_proofs (); + States.intern_state file -let vernac_back n = Lib.back n - -let vernac_backto n = Lib.reset_label n - -(* see also [vernac_backtrack] which combines undoing and resetting *) (************) (* Commands *) @@ -772,8 +775,10 @@ let vernac_declare_implicits local r = function (List.map (List.map (fun (ex,b,f) -> ex, (b,true,f))) imps) let vernac_declare_arguments local r l nargs flags = + let extra_scope_flag = List.mem `ExtraScopes flags in let names = List.map (List.map (fun (id, _,_,_,_) -> id)) l in let names, rest = List.hd names, List.tl names in + let scopes = List.map (List.map (fun (_,_, s, _,_) -> s)) l in if List.exists ((<>) names) rest then error "All arguments lists must declare the same names."; if not (Util.list_distinct (List.filter ((<>) Anonymous) names)) then @@ -782,14 +787,26 @@ let vernac_declare_arguments local r l nargs flags = let inf_names = Impargs.compute_implicits_names (Global.env()) (Global.type_of_global sr) in let string_of_name = function Anonymous -> "_" | Name id -> string_of_id id in - let rec check li ld = match li, ld with - | [], [] -> () - | [], x::_ -> error ("Extra argument " ^ string_of_name x ^ ".") - | l, [] -> error ("The following arguments are not declared: " ^ + let rec check li ld ls = match li, ld, ls with + | [], [], [] -> () + | [], Anonymous::ld, (Some _)::ls when extra_scope_flag -> check li ld ls + | [], _::_, (Some _)::ls when extra_scope_flag -> + error "Extra notation scopes can be set on anonymous arguments only" + | [], x::_, _ -> error ("Extra argument " ^ string_of_name x ^ ".") + | l, [], _ -> error ("The following arguments are not declared: " ^ (String.concat ", " (List.map string_of_name l)) ^ ".") - | _::li, _::ld -> check li ld in + | _::li, _::ld, _::ls -> check li ld ls + | _ -> assert false in if l <> [[]] then - List.iter (fun l -> check inf_names l) (names :: rest); + List.iter2 (fun l -> check inf_names l) (names :: rest) scopes; + (* we take extra scopes apart, and we check they are consistent *) + let l, scopes = + let scopes, rest = List.hd scopes, List.tl scopes in + if List.exists (List.exists ((<>) None)) rest then + error "Notation scopes can be given only once"; + if not extra_scope_flag then l, scopes else + let l, _ = List.split (List.map (list_chop (List.length inf_names)) l) in + l, scopes in (* we interpret _ as the inferred names *) let l = if l = [[]] then l else let name_anons = function @@ -822,10 +839,10 @@ let vernac_declare_arguments local r l nargs flags = let l = List.hd l in let some_implicits_specified = implicits <> [[]] in let scopes = List.map (function - | (_,_, None,_,_) -> None - | (_,_, Some (o, k), _,_) -> + | None -> None + | Some (o, k) -> try Some(ignore(Notation.find_scope k); k) - with _ -> Some (Notation.find_delimiters_scope o k)) l in + with _ -> Some (Notation.find_delimiters_scope o k)) scopes in let some_scopes_specified = List.exists ((<>) None) scopes in let rargs = Util.list_map_filter (function (n, true) -> Some n | _ -> None) @@ -952,6 +969,7 @@ let _ = optkey = ["Printing";"Existential";"Instances"]; optread = (fun () -> !Constrextern.print_evar_arguments); optwrite = (:=) Constrextern.print_evar_arguments } + let _ = declare_bool_option { optsync = true; @@ -1095,6 +1113,15 @@ let _ = optread = (fun () -> get_debug () <> Tactic_debug.DebugOff); optwrite = vernac_debug } +let _ = + declare_bool_option + { optsync = true; + optdepr = false; + optname = "explicitly parsing implicit arguments"; + optkey = ["Parsing";"Explicit"]; + optread = (fun () -> !Constrintern.parsing_explicit); + optwrite = (fun b -> Constrintern.parsing_explicit := b) } + let vernac_set_opacity local str = let glob_ref r = match smart_global r with @@ -1150,6 +1177,7 @@ let vernac_check_may_eval redexp glopt rc = let module P = Pretype_errors in let (sigma, env) = get_current_context_of_args glopt in let sigma', c = interp_open_constr sigma env rc in + let sigma' = Evarconv.consider_remaining_unif_problems env sigma' in let j = try Evarutil.check_evars env sigma sigma' c; @@ -1162,13 +1190,14 @@ let vernac_check_may_eval redexp glopt rc = if !pcoq <> None then (Option.get !pcoq).print_check env j else msg (print_judgment env j) | Some r -> - let redfun = fst (reduction_of_red_expr (interp_redexp env sigma' r)) in + let (sigma',r_interp) = interp_redexp env sigma' r in + let redfun = fst (reduction_of_red_expr r_interp) in if !pcoq <> None then (Option.get !pcoq).print_eval redfun env sigma' rc j else msg (print_eval redfun env sigma' rc j) let vernac_declare_reduction locality s r = - declare_red_expr locality s (interp_redexp (Global.env()) Evd.empty r) + declare_red_expr locality s (snd (interp_redexp (Global.env()) Evd.empty r)) (* The same but avoiding the current goal context if any *) let vernac_global_check c = @@ -1286,15 +1315,54 @@ let vernac_locate = function | LocateTactic qid -> print_located_tactic qid | LocateFile f -> locate_file f +(****************) +(* Backtracking *) + +(** NB: these commands are now forbidden in non-interactive use, + e.g. inside VernacLoad, VernacList, ... *) + +let vernac_backto lbl = + try + let lbl' = Backtrack.backto lbl in + if lbl <> lbl' then + Pp.msg_warning + (str "Actually back to state "++ Pp.int lbl' ++ str "."); + try_print_subgoals () + with Backtrack.Invalid -> error "Invalid backtrack." + +let vernac_back n = + try + let extra = Backtrack.back n in + if extra <> 0 then + Pp.msg_warning + (str "Actually back by " ++ Pp.int (extra+n) ++ str " steps."); + try_print_subgoals () + with Backtrack.Invalid -> error "Invalid backtrack." + +let vernac_reset_name id = + try Backtrack.reset_name id; try_print_subgoals () + with Backtrack.Invalid -> error "Invalid Reset." + +let vernac_reset_initial () = Backtrack.reset_initial () + +(* For compatibility with ProofGeneral: *) + +let vernac_backtrack snum pnum naborts = + Backtrack.backtrack snum pnum naborts; + try_print_subgoals () + + (********************) (* Proof management *) let vernac_abort = function | None -> + Backtrack.mark_unreachable [Pfedit.get_current_proof_name ()]; delete_current_proof (); if_verbose message "Current goal aborted"; if !pcoq <> None then (Option.get !pcoq).abort "" | Some id -> + Backtrack.mark_unreachable [snd id]; delete_proof id; let s = string_of_id (snd id) in if_verbose message ("Goal "^s^" aborted"); @@ -1302,49 +1370,45 @@ let vernac_abort = function let vernac_abort_all () = if refining() then begin + Backtrack.mark_unreachable (Pfedit.get_all_proof_names ()); delete_all_proofs (); message "Current goals aborted" end else error "No proof-editing in progress." -let vernac_restart () = restart_proof(); print_subgoals () - - (* Proof switching *) - -let vernac_suspend = suspend_proof - -let vernac_resume = function - | None -> resume_last_proof () - | Some id -> resume_proof id +let vernac_restart () = + Backtrack.mark_unreachable [Pfedit.get_current_proof_name ()]; + restart_proof(); print_subgoals () let vernac_undo n = - undo n; - print_subgoals () - -(* backtrack with [naborts] abort, then undo_todepth to [pnum], then - back-to state number [snum]. This allows to backtrack proofs and - state with one command (easier for proofgeneral). *) -let vernac_backtrack snum pnum naborts = - for i = 1 to naborts do vernac_abort None done; - undo_todepth pnum; - vernac_backto snum; - Pp.flush_all(); - (* there may be no proof in progress, even if no abort *) - (try print_subgoals () with Proof_global.NoCurrentProof | UserError _ -> ()) + let d = Pfedit.current_proof_depth () - n in + Backtrack.mark_unreachable ~after:d [Pfedit.get_current_proof_name ()]; + Pfedit.undo n; print_subgoals () +let vernac_undoto n = + Backtrack.mark_unreachable ~after:n [Pfedit.get_current_proof_name ()]; + Pfedit.undo_todepth n; + print_subgoals () let vernac_focus gln = let p = Proof_global.give_me_the_proof () in - match gln with - | None -> Proof.focus focus_command_cond () 1 p; print_subgoals () - | Some n -> Proof.focus focus_command_cond () n p; print_subgoals () - + let n = match gln with None -> 1 | Some n -> n in + Proof.focus focus_command_cond () n p; print_subgoals () (* Unfocuses one step in the focus stack. *) let vernac_unfocus () = let p = Proof_global.give_me_the_proof () in Proof.unfocus command_focus p; print_subgoals () +(* Checks that a proof is fully unfocused. Raises an error if not. *) +let vernac_unfocused () = + let p = Proof_global.give_me_the_proof () in + if Proof.unfocused p then + msg (str"The proof is indeed fully unfocused.") + else + error "The proof is not fully unfocused." + + (* BeginSubproof / EndSubproof. BeginSubproof (vernac_subproof) focuses on the first goal, or the goal given as argument. @@ -1483,7 +1547,6 @@ let interp c = match c with | VernacRestoreState s -> vernac_restore_state s (* Resetting *) - | VernacRemoveName id -> Lib.remove_name id | VernacResetName id -> vernac_reset_name id | VernacResetInitial -> vernac_reset_initial () | VernacBack n -> vernac_back n @@ -1520,13 +1583,12 @@ let interp c = match c with | VernacAbort id -> vernac_abort id | VernacAbortAll -> vernac_abort_all () | VernacRestart -> vernac_restart () - | VernacSuspend -> vernac_suspend () - | VernacResume id -> vernac_resume id | VernacUndo n -> vernac_undo n - | VernacUndoTo n -> undo_todepth n + | VernacUndoTo n -> vernac_undoto n | VernacBacktrack (snum,pnum,naborts) -> vernac_backtrack snum pnum naborts | VernacFocus n -> vernac_focus n | VernacUnfocus -> vernac_unfocus () + | VernacUnfocused -> vernac_unfocused () | VernacBullet b -> vernac_bullet b | VernacSubproof n -> vernac_subproof n | VernacEndSubproof -> vernac_end_subproof () diff --git a/toplevel/vernacentries.mli b/toplevel/vernacentries.mli index 8fb6f466..a9d384ea 100644 --- a/toplevel/vernacentries.mli +++ b/toplevel/vernacentries.mli @@ -23,13 +23,6 @@ val show_node : unit -> unit in the context of the current goal, as for instance in pcoq *) val get_current_context_of_args : int option -> Evd.evar_map * Environ.env -(*i - -(** this function is used to analyse the extra arguments in search commands. - It is used in pcoq. *) (*i anciennement: inside_outside i*) -val interp_search_restriction : search_restriction -> dir_path list * bool -i*) - type pcoq_hook = { start_proof : unit -> unit; solve : int -> unit; @@ -44,21 +37,27 @@ type pcoq_hook = { val set_pcoq_hook : pcoq_hook -> unit -(** This function makes sure that the function given in argument is preceded - by a command aborting all proofs if necessary. - It is used in pcoq. *) -val abort_refine : ('a -> unit) -> 'a -> unit;; +(** The main interpretation function of vernacular expressions *) val interp : Vernacexpr.vernac_expr -> unit -val vernac_reset_name : identifier Util.located -> unit +(** Print subgoals when the verbose flag is on. + Meant to be used inside vernac commands from plugins. *) -val vernac_backtrack : int -> int -> int -> unit - -(* Print subgoals when the verbose flag is on. Meant to be used inside - vernac commands from plugins. *) val print_subgoals : unit -> unit +(** The printing of goals via [print_subgoals] or during + [interp] can be controlled by the following flag. + Used for instance by coqide, since it has its own + goal-fetching mechanism. *) + +val enable_goal_printing : bool ref + +(** Should Qed try to display the proof script ? + True by default, but false in ProofGeneral and coqIDE *) + +val qed_display_script : bool ref + (** Prepare a "match" template for a given inductive type. For each branch of the match, we list the constructor name followed by enough pattern variables. diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml index 850bc111..d9f15337 100644 --- a/toplevel/vernacexpr.ml +++ b/toplevel/vernacexpr.ml @@ -114,8 +114,6 @@ type hints_expr = | HintsTransparency of reference list * bool | HintsConstructors of reference list | HintsExtern of int * constr_expr option * raw_tactic_expr - | HintsDestruct of identifier * - int * (bool,unit) location * constr_expr * raw_tactic_expr type search_restriction = | SearchInside of reference list @@ -300,7 +298,6 @@ type vernac_expr = | VernacRestoreState of string (* Resetting *) - | VernacRemoveName of lident | VernacResetName of lident | VernacResetInitial | VernacBack of int @@ -318,7 +315,7 @@ type vernac_expr = (explicitation * bool * bool) list list | VernacArguments of locality_flag * reference or_by_notation * ((name * bool * (loc * string) option * bool * bool) list) list * - int * [ `SimplDontExposeCase | `SimplNeverUnfold | `Rename + int * [ `SimplDontExposeCase | `SimplNeverUnfold | `Rename | `ExtraScopes | `ClearImplicits | `ClearScopes | `DefaultImplicits ] list | VernacArgumentsScope of locality_flag * reference or_by_notation * scope_name option list @@ -346,13 +343,12 @@ type vernac_expr = | VernacAbort of lident option | VernacAbortAll | VernacRestart - | VernacSuspend - | VernacResume of lident option | VernacUndo of int | VernacUndoTo of int | VernacBacktrack of int*int*int | VernacFocus of int option | VernacUnfocus + | VernacUnfocused | VernacBullet of bullet | VernacSubproof of int option | VernacEndSubproof @@ -368,6 +364,26 @@ type vernac_expr = and located_vernac_expr = loc * vernac_expr + +(** Categories of [vernac_expr] *) + +let rec strip_vernac = function + | VernacTime c | VernacTimeout(_,c) | VernacFail c -> strip_vernac c + | c -> c (* TODO: what about VernacList ? *) + +let rec is_navigation_vernac = function + | VernacResetInitial + | VernacResetName _ + | VernacBacktrack _ + | VernacBackTo _ + | VernacBack _ -> true + | c -> is_deep_navigation_vernac c + +and is_deep_navigation_vernac = function + | VernacTime c | VernacTimeout (_,c) | VernacFail c -> is_navigation_vernac c + | VernacList l -> List.exists (fun (_,c) -> is_navigation_vernac c) l + | _ -> false + (* Locating errors raised just after the dot is parsed but before the interpretation phase *) -- cgit v1.2.3