summaryrefslogtreecommitdiff
path: root/toplevel
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2012-06-04 12:29:12 +0200
committerGravatar Stephane Glondu <steph@glondu.net>2012-06-04 12:29:12 +0200
commit676cc7a1dcf1634005c67f76f17390cc8fe44f00 (patch)
treef26ec3bc41f1b7ea54e6c7b39e3262e74e97faba /toplevel
parentff61c7f8b0cbe6f0173720e08a63142a3146cc53 (diff)
parent86535d84cc3cffeee1dcd8545343f234e7285530 (diff)
Merge tag 'upstream/8.4_gamma0+really8.4beta2+dfsg' into experimental/master
Upstream version 8.4~gamma0+really8.4beta2+dfsg
Diffstat (limited to 'toplevel')
-rw-r--r--toplevel/backtrack.ml225
-rw-r--r--toplevel/backtrack.mli93
-rw-r--r--toplevel/class.ml2
-rw-r--r--toplevel/classes.ml9
-rw-r--r--toplevel/command.ml36
-rw-r--r--toplevel/coqtop.ml11
-rw-r--r--toplevel/himsg.ml16
-rw-r--r--toplevel/ide_intf.ml120
-rw-r--r--toplevel/ide_intf.mli26
-rw-r--r--toplevel/ide_slave.ml436
-rw-r--r--toplevel/interface.mli47
-rw-r--r--toplevel/metasyntax.ml12
-rw-r--r--toplevel/metasyntax.mli2
-rw-r--r--toplevel/mltop.ml423
-rw-r--r--toplevel/mltop.mli10
-rw-r--r--toplevel/record.ml6
-rw-r--r--toplevel/search.mli2
-rw-r--r--toplevel/toplevel.ml3
-rw-r--r--toplevel/toplevel.mllib1
-rw-r--r--toplevel/vernac.ml65
-rw-r--r--toplevel/vernac.mli9
-rw-r--r--toplevel/vernacentries.ml198
-rw-r--r--toplevel/vernacentries.mli31
-rw-r--r--toplevel/vernacexpr.ml28
24 files changed, 964 insertions, 447 deletions
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 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+open Names
+open Vernacexpr
+
+(** Command history stack
+
+ We maintain a stack of the past states of the system. Each
+ successfully interpreted command adds an [info] element
+ to this stack, storing what were the (label / current proof / ...)
+ just _after_ the interpretation of this command.
+
+ - A label is just an integer, starting from Lib.first_command_label
+ initially, and incremented at each new successful command.
+ - If some proofs are opened, we have their number in [nproofs],
+ the name of the current proof in [prfname], the current depth in
+ [prfdepth].
+ - Otherwise, [nproofs = 0], [prfname = None], [prfdepth = 0]
+ - The text of the command is stored (for Show Script currently).
+ - A command can be tagged later as non-"reachable" when the current proof
+ at the time of this command has been ended by Qed/Abort/Restart,
+ meaning we can't backtrack there.
+*)
+
+type info = {
+ label : int;
+ nproofs : int;
+ prfname : identifier option;
+ prfdepth : int;
+ cmd : vernac_expr;
+ mutable reachable : bool;
+}
+
+let history : info Stack.t = Stack.create ()
+
+(** For debug purpose, a dump of the history *)
+
+let dump_history () =
+ let l = ref [] in
+ Stack.iter (fun i -> 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 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+(** Command history stack
+
+ We maintain a stack of the past states of the system after each
+ (non-state-preserving) interpreted commands
+*)
+
+(** [mark_command ast] marks the end of a command:
+ - it stores a frozen state and a end of command in the Lib stack,
+ - it stores the current state information in the command history
+ stack *)
+
+val mark_command : Vernacexpr.vernac_expr -> 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
@@ -986,6 +986,18 @@ let inNotation : notation_obj -> obj =
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 *)
let contract_notation ntn =
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 *)
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-20 09:48:28 +0000