diff options
47 files changed, 409 insertions, 260 deletions
diff --git a/.travis.yml b/.travis.yml index d35b7a8422..72ce17a09f 100644 --- a/.travis.yml +++ b/.travis.yml @@ -22,6 +22,7 @@ env: - NJOBS=2 # system is == 4.02.3 - COMPILER="system" + - CAMLP5_VER="6.14" # Main test suites matrix: - TEST_TARGET="test-suite" COMPILER="4.02.3+32bit" @@ -81,6 +82,7 @@ matrix: - env: - TEST_TARGET="test-suite" - COMPILER="4.04.0" + - CAMLP5_VER="6.17" - EXTRA_CONF="-coqide opt -with-doc yes" - EXTRA_OPAM="lablgtk-extras hevea" addons: @@ -106,8 +108,8 @@ matrix: install: - opam init -j ${NJOBS} --compiler=${COMPILER} -n -y - eval $(opam config env) -- opam config var root -- opam install -j ${NJOBS} -y camlp5 ocamlfind ${EXTRA_OPAM} +- opam config list +- opam install -j ${NJOBS} -y camlp5.${CAMLP5_VER} ocamlfind ${EXTRA_OPAM} - opam list script: @@ -1,53 +0,0 @@ -Langage: - -Distribution: - -Environnement: - -- Porter SearchIsos - -Noyau: - -Tactic: - -- Que contradiction raisonne a isomorphisme pres de False - -Vernac: - -- Print / Print Proof en fait identiques ; Print ne devrait pas afficher - les constantes opaques (devrait afficher qqchose comme <opaque>) - -Theories: - -- Rendre transparent tous les theoremes prouvant {A}+{B} -- Faire demarrer PolyList.nth a` l'indice 0 - Renommer l'actuel nth en nth1 ?? - -Doc: - -- Mettre à jour les messages d'erreurs de Discriminate/Simplify_eq/Injection -- Documenter le filtrage sur les types inductifs avec let-ins (dont la - compatibilite V6) - -- Ajouter let dans les règles du CIC - -> FAIT, mais reste a documenter le let dans les inductifs - et les champs manifestes dans les Record -- revoir le chapitre sur les tactiques utilisateur -- faut-il mieux spécifier la sémantique de Simpl (??) - -- Préciser la clarification syntaxique de IntroPattern -- preciser que Goal vient en dernier dans une clause pattern list et - qu'il doit apparaitre si il y a un "in" - -- Omega Time debranche mais Omega System et Omega Action remarchent ? -- Ajout "Replace in" (mais TODO) -- Syntaxe Conditional tac Rewrite marche, à documenter -- Documenter Dependent Rewrite et CutRewrite ? -- Ajouter les motifs sous-termes de ltac - -- ajouter doc de GenFixpoint (mais avant: changer syntaxe) (J. Forest ou Pierre C.) -- mettre à jour la doc de induction (arguments multiples) (Pierre C.) -- mettre à jour la doc de functional induction/scheme (J. Forest ou Pierre C.) ---> mettre à jour le CHANGES (vers la ligne 72) - - diff --git a/dev/doc/econstr.md b/dev/doc/econstr.md new file mode 100644 index 0000000000..bb17e8fb62 --- /dev/null +++ b/dev/doc/econstr.md @@ -0,0 +1,129 @@ +# Evar-insensitive terms (EConstr) + +Evar-insensitive terms were introduced in 8.7, following +[CEP #10](https://github.com/coq/ceps/blob/master/text/010-econstr.md). We will +not recap the motivations in this document and rather summarize the code changes +to perform. + +## Overview + +The essential datastructures are defined in +[the `EConstr` module](/engine/eConstr.mli) module. It defines +the tactic counterparts of kernel data structures such as terms +(`EConstr.constr`), universes (`EConstr.ESorts.t`) and contexts +(`EConstr.*_context`). + +The main difference with kernel-side types is that observing them requires +an evar-map at hand in order to normalize evars on the fly. The basic primitive +to observe an `EConstr.t` is the following function: +``` +val kind : Evd.evar_map -> t -> (t, t, ESorts.t, EInstance.t) Constr.kind_of_term +(** Same as {!Constr.kind} except that it expands evars and normalizes + universes on the fly. *) +``` + +Essentially, each time it sees an evar which happens to be defined in the +provided evar-map, it replaces it with the corresponding body and carries on. + +Due to universe unification occuring at the tactic level, the same goes for +universe instances and sorts. See the `ESort` and `EInstance` modules in +`EConstr`. + +This normalization is critical for the soundness of tactics. Before EConstr, a +lot of bugs were lurking in the code base, a few still are (most notably in +meta-based unification) and failure to respect the guidelines thereafter may +result in nasal demons. + +## Transition path + +### Types + +As a rule of thumb, all functions living at the tactic level should manipulate +`EConstr.t` instead of `Constr.t`, and similarly for the other data structures. + +To ease the transition, the `EConstr` module defines a handful of aliases to +shadow the type names from the kernel. + +It is recommended to perform the following replacement in headers. +```ocaml +(** Kernel types. You may remove the two following opens if you want. Beware + that [kind_of_term] needs to be in scope if you use [EConstr.kind] so that + you may still need to open one of the two. *) +open Term +open Constr +(** Tactic types. Open this after to shadow kernel types. *) +open EConstr +``` + +Note that the `EConstr` module also redefines a `Vars` submodule. + +### Evar-map-passing + +All functions deconstructing an econstr need to take an evar-map as a parameter. +Therefore, you need to pass one as an argument virtually everywhere. + +In the Coq source code, it is recommended to take the evar-map as a first +argument called `sigma`, except if the function also takes an environment in +which case it is passed second. Namely, the two typical instances are: +```ocaml +let foo sigma c = mycode +val foo : Evd.evar_map -> EConstr.t -> Foo.t + +let bar env sigma c = mycode +val bar : Environ.env -> Evd.evar_map -> EConstr.t -> Bar.t +``` + +The EConstr API makes the code much more sensitive to evar-maps, because a +lot of now useless normalizations were removed. Thus one should be cautious of +**not** dropping the evar-map when it has been updated, and should rather stick +to a strict state-passing discipline. Unsound primitives like +`Typing.unsafe_type_of` are also a known source of problems, so you should +replace them with the corresponding evar-map-returning function and thread it +properly. + +### Functions + +Many functions from `Constr` and `Term` are redefined to work on econstr in +the `EConstr` module, so that it is often enough to perform the `open` as +described above to replace them. Their type may differ though, because they now +need access to an evar-map. A lot of econstr-manipulating functions are also +defined in [`Termops`](/engine/termops.mli). + +Functions manipulating tactic terms and kernel terms share the same name if they +are the equivalent one of the other. Do not hesitate to grep Coq mli files to +find the equivalent of a function you want to port if it is neither in `EConstr` +nor in `Termops` (this should be very rare). + +### Conversion + +Sometimes you do not have any other choice than calling kernel-side functions +on terms, and conversely to turn a kernel term into a tactic term. + +There are two functions to do so. +* `EConstr.of_constr` turns kernel terms into tactic terms. It is currently +the physical identity, and thus O(1), but this may change in the future. +* `EConstr.to_constr` turns tactic terms into kernel terms. It performs a +full-blown normalization of the given term, which is O(n) and potentially +costly. + +For performance reasons, avoiding to jump back and forth between kernel and +tactic terms is recommended. + +There are also a few unsafe conversion functions that take advantage of the +fact that `EConstr.t` is internally the same as `Constr.t`. Namely, +`EConstr.Unsafe.to_constr` is the physical identity. It should **not** be used +in typical code and is instead provided for efficiency **when you know what you +are doing**. Either use it to reimplement low-level functions that happen to +be insensitive externally, or use it to provide backward compatibility with +broken code that relies on evar-sensitivity. **Do not use it because it is +easier than stuffing evar-maps everywhere.** You've been warned. + +## Notes + +The EConstr branch fixed a lot of eisenbugs linked to lack of normalization +everywhere, most notably in unification. It may also have introduced a few, so +if you see a change in behaviour *that looks like a bug*, please report it. +Obviously, unification is not specified, so it's hard to tell apart, but still. + +Efficiency has been affected as well. We now pay an overhead when observing a +term, but at the same time a lot of costly upfront normalizations were removed. diff --git a/engine/proofview.ml b/engine/proofview.ml index 9c264439be..f054038e9c 100644 --- a/engine/proofview.ml +++ b/engine/proofview.ml @@ -1020,11 +1020,11 @@ module Goal = struct let assume (gl : ('a, 'r) t) = (gl :> ([ `NF ], 'r) t) - let env { env=env } = env - let sigma { sigma=sigma } = Sigma.Unsafe.of_evar_map sigma - let hyps { env=env } = EConstr.named_context env - let concl { concl=concl } = concl - let extra { sigma=sigma; self=self } = goal_extra sigma self + let env {env} = env + let sigma {sigma} = Sigma.Unsafe.of_evar_map sigma + let hyps {env} = EConstr.named_context env + let concl {concl} = concl + let extra {sigma; self} = goal_extra sigma self let gmake_with info env sigma goal = { env = Environ.reset_with_named_context (Evd.evar_filtered_hyps info) env ; @@ -1040,7 +1040,7 @@ module Goal = struct let nf_enter f = InfoL.tag (Info.Dispatch) begin iter_goal begin fun goal -> - Env.get >>= fun env -> + tclENV >>= fun env -> tclEVARMAP >>= fun sigma -> try let (gl, sigma) = nf_gmake env sigma goal in diff --git a/ide/coqOps.ml b/ide/coqOps.ml index eb97755fa6..222b9eed9f 100644 --- a/ide/coqOps.ml +++ b/ide/coqOps.ml @@ -366,6 +366,9 @@ object(self) (* This method is intended to perform stateless commands *) method raw_coq_query phrase = + let sid = try Document.tip document + with Document.Empty -> Stateid.initial + in let action = log "raw_coq_query starting now" in let display_error s = if not (validate s) then @@ -373,11 +376,10 @@ object(self) else messages#add s; in let query = - Coq.query (phrase,Stateid.dummy) in + Coq.query (phrase,sid) in let next = function | Fail (_, _, err) -> display_error err; Coq.return () - | Good msg -> - messages#add_string msg; Coq.return () + | Good msg -> Coq.return () in Coq.bind (Coq.seq action query) next @@ -414,12 +416,9 @@ object(self) buffer#apply_tag Tags.Script.tooltip ~start ~stop; add_tooltip sentence pre post markup - method private is_dummy_id id = Stateid.equal id Stateid.dummy - method private enqueue_feedback msg = - (* Minilib.log ("Feedback received: " ^ Xml_printer.to_string_fmt (Xmlprotocol.of_feedback msg)); *) - let id = msg.id in - if self#is_dummy_id id then () else Queue.add msg feedbacks + (* Minilib.log ("Feedback received: " ^ Xml_printer.to_string_fmt Xmlprotocol.(of_feedback Ppcmds msg)); *) + Queue.add msg feedbacks method private process_feedback () = let rec eat_feedback n = @@ -433,41 +432,41 @@ object(self) | _ -> None in try Some (Doc.find_map document finder) with Not_found -> None in - let log_pp s state_id = + let log_pp ?id s= Minilib.log_pp Pp.(seq - [str "Feedback "; s; str " on "; - str (Stateid.to_string (Option.default Stateid.dummy state_id))]) in - let log s state_id = log_pp (Pp.str s) state_id in + [str "Feedback "; s; pr_opt (fun id -> str " on " ++ str (Stateid.to_string id)) id]) + in + let log ?id s = log_pp ?id (Pp.str s) in begin match msg.contents, sentence with | AddedAxiom, Some (id,sentence) -> - log "AddedAxiom" id; + log ?id "AddedAxiom"; remove_flag sentence `PROCESSING; remove_flag sentence `ERROR; add_flag sentence `UNSAFE; self#mark_as_needed sentence | Processed, Some (id,sentence) -> - log "Processed" id; + log ?id "Processed" ; remove_flag sentence `PROCESSING; self#mark_as_needed sentence | ProcessingIn _, Some (id,sentence) -> - log "ProcessingIn" id; + log ?id "ProcessingIn"; add_flag sentence `PROCESSING; self#mark_as_needed sentence | Incomplete, Some (id, sentence) -> - log "Incomplete" id; + log ?id "Incomplete"; add_flag sentence `INCOMPLETE; self#mark_as_needed sentence | Complete, Some (id, sentence) -> - log "Complete" id; + log ?id "Complete"; remove_flag sentence `INCOMPLETE; self#mark_as_needed sentence | GlobRef(loc, filepath, modpath, ident, ty), Some (id,sentence) -> - log "GlobRef" id; + log ?id "GlobRef"; self#attach_tooltip ~loc sentence (Printf.sprintf "%s %s %s" filepath ident ty) | Message(Error, loc, msg), Some (id,sentence) -> let uloc = Option.default Loc.ghost loc in - log_pp Pp.(str "ErrorMsg" ++ msg) id; + log_pp ?id Pp.(str "ErrorMsg" ++ msg); remove_flag sentence `PROCESSING; let rmsg = Pp.string_of_ppcmds msg in add_flag sentence (`ERROR (uloc, rmsg)); @@ -476,22 +475,24 @@ object(self) self#position_tag_at_sentence ?loc Tags.Script.error sentence | Message(Warning, loc, msg), Some (id,sentence) -> let uloc = Option.default Loc.ghost loc in - log_pp Pp.(str "WarningMsg" ++ msg) id; + log_pp ?id Pp.(str "WarningMsg" ++ msg); let rmsg = Pp.string_of_ppcmds msg in add_flag sentence (`WARNING (uloc, rmsg)); self#attach_tooltip sentence ?loc rmsg; self#position_tag_at_sentence ?loc Tags.Script.warning sentence; messages#push Warning msg | Message(lvl, loc, msg), Some (id,sentence) -> - log_pp Pp.(str "Msg" ++ msg) id; + log_pp ?id Pp.(str "Msg" ++ msg); + messages#push lvl msg + | Message(lvl, loc, msg), None -> + log_pp Pp.(str "Msg" ++ msg); messages#push lvl msg | InProgress n, _ -> if n < 0 then processed <- processed + abs n else to_process <- to_process + n | WorkerStatus(id,status), _ -> - log "WorkerStatus" None; + log "WorkerStatus"; slaves_status <- CString.Map.add id status slaves_status - | _ -> if sentence <> None then Minilib.log "Unsupported feedback message" else if Doc.is_empty document then () @@ -500,7 +501,7 @@ object(self) match id, Doc.tip document with | id1, id2 when Stateid.newer_than id2 id1 -> () | _ -> Queue.add msg feedbacks - with Doc.Empty | Invalid_argument _ -> Queue.add msg feedbacks + with Doc.Empty | Invalid_argument _ -> Queue.add msg feedbacks end; eat_feedback (n-1) in diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml index 4b95e983d6..bf86db08ff 100644 --- a/ide/ide_slave.ml +++ b/ide/ide_slave.ml @@ -63,25 +63,26 @@ let is_known_option cmd = match cmd with (** Check whether a command is forbidden in the IDE *) -let ide_cmd_checks (loc,ast) = +let ide_cmd_checks ~id (loc,ast) = let user_error s = CErrors.user_err ~loc ~hdr:"CoqIde" (str s) in + let warn msg = Feedback.(feedback ~id (Message (Warning, Some loc, strbrk msg))) in if is_debug ast then user_error "Debug mode not available in the IDE"; if is_known_option ast then - Feedback.msg_warning ~loc (strbrk "Set this option from the IDE menu instead"); + warn "Set this option from the IDE menu instead"; if is_navigation_vernac ast || is_undo ast then - Feedback.msg_warning ~loc (strbrk "Use IDE navigation instead"); + warn "Use IDE navigation instead"; if is_query ast then - Feedback.msg_warning ~loc (strbrk "Query commands should not be inserted in scripts") + warn "Query commands should not be inserted in scripts" (** Interpretation (cf. [Ide_intf.interp]) *) let add ((s,eid),(sid,verbose)) = let pa = Pcoq.Gram.parsable (Stream.of_string s) in let loc_ast = Stm.parse_sentence sid pa in - ide_cmd_checks loc_ast; let newid, rc = Stm.add ~ontop:sid verbose loc_ast in let rc = match rc with `NewTip -> CSig.Inl () | `Unfocus id -> CSig.Inr id in + ide_cmd_checks newid loc_ast; (* TODO: the "" parameter is a leftover of the times the protocol * used to include stderr/stdout output. * diff --git a/ide/session.ml b/ide/session.ml index fc6340d283..6262820e7b 100644 --- a/ide/session.ml +++ b/ide/session.ml @@ -386,12 +386,12 @@ let create file coqtop_args = let proof = create_proof () in let messages = create_messages () in let segment = new Wg_Segment.segment () in - let command = new Wg_Command.command_window basename coqtop in let finder = new Wg_Find.finder basename (script :> GText.view) in let fops = new FileOps.fileops (buffer :> GText.buffer) file reset in let _ = fops#update_stats in let cops = new CoqOps.coqops script proof messages segment coqtop (fun () -> fops#filename) in + let command = new Wg_Command.command_window basename coqtop cops in let errpage = create_errpage script in let jobpage = create_jobpage coqtop cops in let _ = set_buffer_handlers (buffer :> GText.buffer) script cops coqtop in diff --git a/ide/texmacspp.ml b/ide/texmacspp.ml index e787e48bf1..e20704b7fb 100644 --- a/ide/texmacspp.ml +++ b/ide/texmacspp.ml @@ -504,7 +504,6 @@ let rec tmpp v loc = xmlApply loc (Element("timeout",["val",string_of_int s],[]) :: [tmpp e loc]) | VernacFail e -> xmlApply loc (Element("fail",[],[]) :: [tmpp e loc]) - | VernacError _ -> xmlWithLoc loc "error" [] [] (* Syntax *) | VernacSyntaxExtension (_, ((_, name), sml)) -> diff --git a/ide/wg_Command.ml b/ide/wg_Command.ml index 47dad8f196..3fcb7ce49e 100644 --- a/ide/wg_Command.ml +++ b/ide/wg_Command.ml @@ -8,7 +8,7 @@ open Preferences -class command_window name coqtop = +class command_window name coqtop coqops = let frame = Wg_Detachable.detachable ~title:(Printf.sprintf "Query pane (%s)" name) () in let _ = frame#hide in @@ -26,6 +26,11 @@ object(self) val notebook = notebook + (* We need access to coqops in order to place queries in the proper + document stint. This should remove access from this module to the + low-level Coq one. *) + val coqops = coqops + method pack_in (f : GObj.widget -> unit) = f frame#coerce val mutable new_page : GObj.widget = (GMisc.label ())#coerce @@ -101,7 +106,10 @@ object(self) else com ^ " " ^ arg ^" . " in let process = - Coq.bind (Coq.query (phrase,Stateid.dummy)) (function + (* We need to adapt this to route_id and redirect to the result buffer below *) + coqops#raw_coq_query phrase + (* + Coq.bind (Coq.query (phrase,sid)) (function | Interface.Fail (_,l,str) -> let width = Ideutils.textview_width result in Ideutils.insert_xml result#buffer (Richpp.richpp_of_pp width str); @@ -111,6 +119,7 @@ object(self) result#buffer#insert res; notebook#set_page ~tab_label:(new_tab_lbl arg) frame#coerce; Coq.return ()) + *) in result#buffer#set_text ("Result for command " ^ phrase ^ ":\n"); Coq.try_grab coqtop process ignore diff --git a/ide/wg_Command.mli b/ide/wg_Command.mli index fa50ba5fdd..341322be1b 100644 --- a/ide/wg_Command.mli +++ b/ide/wg_Command.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -class command_window : string -> Coq.coqtop -> +class command_window : string -> Coq.coqtop -> CoqOps.coqops -> object method new_query : ?command:string -> ?term:string -> unit -> unit method pack_in : (GObj.widget -> unit) -> unit diff --git a/interp/coqlib.mli b/interp/coqlib.mli index 5ba26d8286..1facb47e1e 100644 --- a/interp/coqlib.mli +++ b/interp/coqlib.mli @@ -19,7 +19,7 @@ open Util (** [find_reference caller_message [dir;subdir;...] s] returns a global reference to the name dir.subdir.(...).s; the corresponding module must have been required or in the process of being compiled so that - it must be used lazyly; it raises an anomaly with the given message + it must be used lazily; it raises an anomaly with the given message if not found *) type message = string diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli index 25d3c705f4..f018d59e6b 100644 --- a/intf/vernacexpr.mli +++ b/intf/vernacexpr.mli @@ -71,7 +71,7 @@ type printable = | PrintScopes | PrintScope of string | PrintVisibility of string option - | PrintAbout of reference or_by_notation*int option + | PrintAbout of reference or_by_notation * goal_selector option | PrintImplicit of reference or_by_notation | PrintAssumptions of bool * bool * reference or_by_notation | PrintStrategy of reference or_by_notation option @@ -316,7 +316,6 @@ type vernac_expr = | VernacRedirect of string * vernac_expr located | VernacTimeout of int * vernac_expr | VernacFail of vernac_expr - | VernacError of exn (* always fails *) (* Syntax *) | VernacSyntaxExtension of @@ -436,11 +435,11 @@ type vernac_expr = | VernacRemoveOption of Goptions.option_name * option_ref_value list | VernacMemOption of Goptions.option_name * option_ref_value list | VernacPrintOption of Goptions.option_name - | VernacCheckMayEval of Genredexpr.raw_red_expr option * int option * constr_expr + | VernacCheckMayEval of Genredexpr.raw_red_expr option * goal_selector option * constr_expr | VernacGlobalCheck of constr_expr | VernacDeclareReduction of string * Genredexpr.raw_red_expr | VernacPrint of printable - | VernacSearch of searchable * int option * search_restriction + | VernacSearch of searchable * goal_selector option * search_restriction | VernacLocate of locatable | VernacRegister of lident * register_kind | VernacComments of comment list diff --git a/kernel/context.mli b/kernel/context.mli index 0c666a25d9..24e69ebd6e 100644 --- a/kernel/context.mli +++ b/kernel/context.mli @@ -214,7 +214,7 @@ sig val to_rel_decl : ('c, 't) pt -> ('c, 't) Rel.Declaration.pt end - (** Rel-context is represented as a list of declarations. + (** Named-context is represented as a list of declarations. Inner-most declarations are at the beginning of the list. Outer-most declarations are at the end of the list. *) type ('constr, 'types) pt = ('constr, 'types) Declaration.pt list @@ -223,7 +223,7 @@ sig (** empty named-context *) val empty : ('c, 't) pt - (** Return a new rel-context enriched by with a given inner-most declaration. *) + (** Return a new named-context enriched by with a given inner-most declaration. *) val add : ('c, 't) Declaration.pt -> ('c, 't) pt -> ('c, 't) pt (** Return the number of {e local declarations} in a given named-context. *) @@ -233,7 +233,7 @@ sig @raise Not_found if the designated identifier is not bound in a given named-context. *) val lookup : Id.t -> ('c, 't) pt -> ('c, 't) Declaration.pt - (** Check whether given two rel-contexts are equal. *) + (** Check whether given two named-contexts are equal. *) val equal : ('c -> 'c -> bool) -> ('c, 'c) pt -> ('c, 'c) pt -> bool (** Map all terms in a given named-context. *) @@ -253,8 +253,8 @@ sig (** Return the set of all identifiers bound in a given named-context. *) val to_vars : ('c, 't) pt -> Id.Set.t - (** [instance_from_named_context Ω] builds an instance [args] such - that [Ω ⊢ args:Ω] where [Ω] is a named context and with the local + (** [to_instance Ω] builds an instance [args] such + that [Ω ⊢ args:Ω] where [Ω] is a named-context and with the local definitions of [Ω] skipped. Example: for [id1:T,id2:=c,id3:U], it gives [Var id1, Var id3]. All [idj] are supposed distinct. *) val to_instance : (Id.t -> 'r) -> ('c, 't) pt -> 'r list diff --git a/kernel/declarations.mli b/kernel/declarations.mli index 7821ea20ff..71e228b19c 100644 --- a/kernel/declarations.mli +++ b/kernel/declarations.mli @@ -77,7 +77,7 @@ type typing_flags = { } (* some contraints are in constant_constraints, some other may be in - * the OpaueDef *) + * the OpaqueDef *) type constant_body = { const_hyps : Context.Named.t; (** New: younger hyp at top *) const_body : constant_def; diff --git a/kernel/names.ml b/kernel/names.ml index ee8d838da1..5c10badbec 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -162,21 +162,8 @@ module DirPath = struct type t = module_ident list - let rec compare (p1 : t) (p2 : t) = - if p1 == p2 then 0 - else begin match p1, p2 with - | [], [] -> 0 - | [], _ -> -1 - | _, [] -> 1 - | id1 :: p1, id2 :: p2 -> - let c = Id.compare id1 id2 in - if Int.equal c 0 then compare p1 p2 else c - end - - let rec equal p1 p2 = p1 == p2 || match p1, p2 with - | [], [] -> true - | id1 :: p1, id2 :: p2 -> Id.equal id1 id2 && equal p1 p2 - | _ -> false + let compare = List.compare Id.compare + let equal = List.equal Id.equal let rec hash accu = function | [] -> accu @@ -191,7 +178,7 @@ struct let empty = [] - let is_empty d = match d with [] -> true | _ -> false + let is_empty = List.is_empty let to_string = function | [] -> "<>" diff --git a/kernel/pre_env.ml b/kernel/pre_env.ml index d14a254d32..48d7ee9ec3 100644 --- a/kernel/pre_env.ml +++ b/kernel/pre_env.ml @@ -68,8 +68,8 @@ type named_context_val = { } type env = { - env_globals : globals; - env_named_context : named_context_val; + env_globals : globals; (* globals = constants + inductive types + modules + module-types *) + env_named_context : named_context_val; (* section variables *) env_rel_context : Context.Rel.t; env_rel_val : lazy_val list; env_nb_rel : int; @@ -161,19 +161,7 @@ let map_named_val f ctxt = else { env_named_ctx = ctx; env_named_map = map } let push_named d env = -(* if not (env.env_rel_context = []) then raise (ASSERT env.env_rel_context); - assert (env.env_rel_context = []); *) - { env_globals = env.env_globals; - env_named_context = push_named_context_val d env.env_named_context; - env_rel_context = env.env_rel_context; - env_rel_val = env.env_rel_val; - env_nb_rel = env.env_nb_rel; - env_stratification = env.env_stratification; - env_typing_flags = env.env_typing_flags; - env_conv_oracle = env.env_conv_oracle; - retroknowledge = env.retroknowledge; - indirect_pterms = env.indirect_pterms; - } + {env with env_named_context = push_named_context_val d env.env_named_context} let lookup_named id env = fst (Id.Map.find id env.env_named_context.env_named_map) diff --git a/lib/flags.ml b/lib/flags.ml index d87d9e7295..00f515b5a6 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -143,16 +143,16 @@ let beautify = ref false let beautify_file = ref false (* Silent / Verbose *) -let silent = ref false -let make_silent flag = silent := flag; () -let is_silent () = !silent -let is_verbose () = not !silent +let quiet = ref false +let silently f x = with_option quiet f x +let verbosely f x = without_option quiet f x -let silently f x = with_option silent f x -let verbosely f x = without_option silent f x +let if_silent f x = if !quiet then f x +let if_verbose f x = if not !quiet then f x -let if_silent f x = if !silent then f x -let if_verbose f x = if not !silent then f x +let make_silent flag = quiet := flag +let is_silent () = !quiet +let is_verbose () = not !quiet let auto_intros = ref true let make_auto_intros flag = auto_intros := flag diff --git a/lib/flags.mli b/lib/flags.mli index c5c4a15aaa..0b00ac13c2 100644 --- a/lib/flags.mli +++ b/lib/flags.mli @@ -85,16 +85,22 @@ val pr_version : compat_version -> string val beautify : bool ref val beautify_file : bool ref -(* Silent/verbose, both actually controlled by a single flag so they - are mutually exclusive *) -val make_silent : bool -> unit -val is_silent : unit -> bool -val is_verbose : unit -> bool +(* Coq quiet mode. Note that normal mode is called "verbose" here, + whereas [quiet] supresses normal output such as goals in coqtop *) +val quiet : bool ref val silently : ('a -> 'b) -> 'a -> 'b val verbosely : ('a -> 'b) -> 'a -> 'b val if_silent : ('a -> unit) -> 'a -> unit val if_verbose : ('a -> unit) -> 'a -> unit +(* Deprecated *) +val make_silent : bool -> unit +[@@ocaml.deprecated "Please use Flags.quiet"] +val is_silent : unit -> bool +[@@ocaml.deprecated "Please use Flags.quiet"] +val is_verbose : unit -> bool +[@@ocaml.deprecated "Please use Flags.quiet"] + (* Miscellaneus flags for vernac *) val make_auto_intros : bool -> unit val is_auto_intros : unit -> bool diff --git a/library/loadpath.ml b/library/loadpath.ml index d03c6c5553..529b9502b0 100644 --- a/library/loadpath.ml +++ b/library/loadpath.ml @@ -113,5 +113,5 @@ let expand_path ?root dir = let locate_file fname = let paths = List.map physical !load_paths in let _,longfname = - System.find_file_in_path ~warn:(Flags.is_verbose()) paths fname in + System.find_file_in_path ~warn:(not !Flags.quiet) paths fname in longfname diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 4fd316119f..011565d86a 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -40,7 +40,6 @@ let def_body = Gram.entry_create "vernac:def_body" let decl_notation = Gram.entry_create "vernac:decl_notation" let record_field = Gram.entry_create "vernac:record_field" let of_type_with_opt_coercion = Gram.entry_create "vernac:of_type_with_opt_coercion" -let subgoal_command = Gram.entry_create "proof_mode:subgoal_command" let instance_name = Gram.entry_create "vernac:instance_name" let section_subset_expr = Gram.entry_create "vernac:section_subset_expr" @@ -53,7 +52,7 @@ let make_bullet s = | _ -> assert false GEXTEND Gram - GLOBAL: vernac gallina_ext noedit_mode subprf subgoal_command; + GLOBAL: vernac gallina_ext noedit_mode subprf; vernac: FIRST [ [ IDENT "Time"; c = located_vernac -> VernacTime c | IDENT "Redirect"; s = ne_string; c = located_vernac -> VernacRedirect (s, c) @@ -92,7 +91,7 @@ GEXTEND Gram [ [ prfcom = command_entry -> prfcom ] ] ; noedit_mode: - [ [ c = subgoal_command -> c None] ] + [ [ c = query_command -> c None] ] ; subprf: @@ -102,15 +101,6 @@ GEXTEND Gram ] ] ; - subgoal_command: - [ [ c = query_command; "." -> - begin function - | Some (SelectNth g) -> c (Some g) - | None -> c None - | _ -> - VernacError (UserError (None,str"Typing and evaluation commands, cannot be used with the \"all:\" selector.")) - end ] ] - ; located_vernac: [ [ v = vernac -> !@loc, v ] ] ; @@ -918,29 +908,30 @@ GEXTEND Gram VernacRemoveOption ([table], v) ]] ; query_command: (* TODO: rapprocher Eval et Check *) - [ [ IDENT "Eval"; r = red_expr; "in"; c = lconstr -> + [ [ IDENT "Eval"; r = red_expr; "in"; c = lconstr; "." -> fun g -> VernacCheckMayEval (Some r, g, c) - | IDENT "Compute"; c = lconstr -> + | IDENT "Compute"; c = lconstr; "." -> fun g -> VernacCheckMayEval (Some (Genredexpr.CbvVm None), g, c) - | IDENT "Check"; c = lconstr -> + | IDENT "Check"; c = lconstr; "." -> fun g -> VernacCheckMayEval (None, g, c) (* Searching the environment *) - | IDENT "About"; qid = smart_global -> + | IDENT "About"; qid = smart_global; "." -> fun g -> VernacPrint (PrintAbout (qid,g)) - | IDENT "SearchHead"; c = constr_pattern; l = in_or_out_modules -> + | IDENT "SearchHead"; c = constr_pattern; l = in_or_out_modules; "." -> fun g -> VernacSearch (SearchHead c,g, l) - | IDENT "SearchPattern"; c = constr_pattern; l = in_or_out_modules -> + | IDENT "SearchPattern"; c = constr_pattern; l = in_or_out_modules; "." -> fun g -> VernacSearch (SearchPattern c,g, l) - | IDENT "SearchRewrite"; c = constr_pattern; l = in_or_out_modules -> + | IDENT "SearchRewrite"; c = constr_pattern; l = in_or_out_modules; "." -> fun g -> VernacSearch (SearchRewrite c,g, l) - | IDENT "Search"; s = searchabout_query; l = searchabout_queries -> + | IDENT "Search"; s = searchabout_query; l = searchabout_queries; "." -> let (sl,m) = l in fun g -> VernacSearch (SearchAbout (s::sl),g, m) (* compatibility: SearchAbout *) - | IDENT "SearchAbout"; s = searchabout_query; l = searchabout_queries -> + | IDENT "SearchAbout"; s = searchabout_query; l = searchabout_queries; "." -> fun g -> let (sl,m) = l in VernacSearch (SearchAbout (s::sl),g, m) (* compatibility: SearchAbout with "[ ... ]" *) | IDENT "SearchAbout"; "["; sl = LIST1 searchabout_query; "]"; - l = in_or_out_modules -> fun g -> VernacSearch (SearchAbout sl,g, l) + l = in_or_out_modules; "." -> + fun g -> VernacSearch (SearchAbout sl,g, l) ] ] ; printable: diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml index 92d249e535..dad98e2e98 100644 --- a/parsing/pcoq.ml +++ b/parsing/pcoq.ml @@ -211,7 +211,7 @@ let camlp4_verbosity silent f x = f x; warning_verbose := a -let camlp4_verbose f x = camlp4_verbosity (Flags.is_verbose ()) f x +let camlp4_verbose f x = camlp4_verbosity (not !Flags.quiet) f x (** Grammar extensions *) diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 48c0f5f04c..8dae17d69e 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -299,7 +299,7 @@ let change_eq env sigma hyp_id (context:rel_context) x t end_of_type = Can be safely replaced by the next comment for Ocaml >= 3.08.4 *) let sub = Int.Map.bindings sub in - List.fold_left (fun end_of_type (i,t) -> lift 1 (substnl [t] (i-1) end_of_type)) + List.fold_left (fun end_of_type (i,t) -> liftn 1 i (substnl [t] (i-1) end_of_type)) end_of_type_with_pop sub in @@ -1401,8 +1401,8 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam let prove_with_tcc tcc_lemma_constr eqs : tactic = match !tcc_lemma_constr with - | None -> anomaly (Pp.str "No tcc proof !!") - | Some lemma -> + | Undefined -> anomaly (Pp.str "No tcc proof !!") + | Value lemma -> fun gls -> (* let hid = next_ident_away_in_goal h_id (pf_ids_of_hyps gls) in *) (* let ids = hid::pf_ids_of_hyps gls in *) @@ -1420,7 +1420,7 @@ let prove_with_tcc tcc_lemma_constr eqs : tactic = Proofview.V82.of_tactic (Eauto.gen_eauto (false,5) [] (Some [])) ] gls - + | Not_needed -> tclIDTAC let backtrack_eqs_until_hrec hrec eqs : tactic = fun gls -> @@ -1599,8 +1599,9 @@ let prove_principle_for_gen let args_ids = List.map (get_name %> Nameops.out_name) princ_info.args in let lemma = match !tcc_lemma_ref with - | None -> error "No tcc proof !!" - | Some lemma -> EConstr.of_constr lemma + | Undefined -> error "No tcc proof !!" + | Value lemma -> EConstr.of_constr lemma + | Not_needed -> EConstr.of_constr (Coqlib.build_coq_I ()) in (* let rec list_diff del_list check_list = *) (* match del_list with *) diff --git a/plugins/funind/functional_principles_proofs.mli b/plugins/funind/functional_principles_proofs.mli index 769d726d70..7ddc84d015 100644 --- a/plugins/funind/functional_principles_proofs.mli +++ b/plugins/funind/functional_principles_proofs.mli @@ -9,7 +9,7 @@ val prove_princ_for_struct : val prove_principle_for_gen : constant*constant*constant -> (* name of the function, the functional and the fixpoint equation *) - constr option ref -> (* a pointer to the obligation proofs lemma *) + Indfun_common.tcc_lemma_value ref -> (* a pointer to the obligation proofs lemma *) bool -> (* is that function uses measure *) int -> (* the number of recursive argument *) EConstr.types -> (* the type of the recursive argument *) diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index 20da12f395..7b0d7d27d7 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -543,3 +543,8 @@ let prodn n env b = (* compose_prod [xn:Tn;..;x1:T1] b = (x1:T1)..(xn:Tn)b *) let compose_prod l b = prodn (List.length l) l b + +type tcc_lemma_value = + | Undefined + | Value of Constr.constr + | Not_needed diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli index 5c3e73e9d7..5ef8f05bb7 100644 --- a/plugins/funind/indfun_common.mli +++ b/plugins/funind/indfun_common.mli @@ -119,3 +119,8 @@ val decompose_lam_n : Evd.evar_map -> int -> EConstr.t -> (Names.Name.t * EConstr.t) list * EConstr.t val compose_lam : (Names.Name.t * EConstr.t) list -> EConstr.t -> EConstr.t val compose_prod : (Names.Name.t * EConstr.t) list -> EConstr.t -> EConstr.t + +type tcc_lemma_value = + | Undefined + | Value of Constr.constr + | Not_needed diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 5460d6fb73..1e405d2c90 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -45,12 +45,6 @@ open Indfun_common open Sigma.Notations open Context.Rel.Declaration -let local_assum (na, t) = - LocalAssum (na, EConstr.Unsafe.to_constr t) - -let local_def (na, b, t) = - LocalDef (na, EConstr.Unsafe.to_constr b, EConstr.Unsafe.to_constr t) - (* Ugly things which should not be here *) let coq_constant m s = @@ -1323,7 +1317,7 @@ let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decomp | _ -> anomaly ~label:"equation_lemma" (Pp.str "not a constant") in let lemma = mkConst (Names.Constant.make1 (Lib.make_kn na)) in - ref_ := Some (EConstr.Unsafe.to_constr lemma); + ref_ := Value (EConstr.Unsafe.to_constr lemma); let lid = ref [] in let h_num = ref (-1) in let env = Global.env () in @@ -1411,7 +1405,7 @@ let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decomp let com_terminate tcc_lemma_name - (tcc_lemma_ref : Constr.t option ref) + tcc_lemma_ref is_mes fonctional_ref input_type @@ -1440,6 +1434,7 @@ let com_terminate (new_goal_type); with Failure "empty list of subgoals!" -> (* a non recursive function declared with measure ! *) + tcc_lemma_ref := Not_needed; defined () @@ -1515,7 +1510,6 @@ let (com_eqn : int -> Id.t -> (* Pp.msgnl (str "eqn finished"); *) );; - let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num eq generate_induction_principle using_lemmas : unit = let open Term in @@ -1561,7 +1555,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num in let evm = Evd.from_ctx evuctx in let tcc_lemma_name = add_suffix function_name "_tcc" in - let tcc_lemma_constr = ref None in + let tcc_lemma_constr = ref Undefined in (* let _ = Pp.msgnl (str "relation := " ++ Printer.pr_lconstr_env env_with_pre_rec_args relation) in *) let hook _ _ = let term_ref = Nametab.locate (qualid_of_ident term_id) in @@ -1590,8 +1584,8 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num and eq_ref = destConst (constr_of_global eq_ref) in generate_induction_principle f_ref tcc_lemma_constr functional_ref eq_ref rec_arg_num (EConstr.of_constr rec_arg_type) (nb_prod evm (EConstr.of_constr res)) (EConstr.of_constr relation); - if Flags.is_verbose () - then msgnl (h 1 (Ppconstr.pr_id function_name ++ + Flags.if_verbose + msgnl (h 1 (Ppconstr.pr_id function_name ++ spc () ++ str"is defined" )++ fnl () ++ h 1 (Ppconstr.pr_id equation_id ++ spc () ++ str"is defined" ) diff --git a/plugins/funind/recdef.mli b/plugins/funind/recdef.mli index 9c1081b9d2..80f02e01c4 100644 --- a/plugins/funind/recdef.mli +++ b/plugins/funind/recdef.mli @@ -13,7 +13,7 @@ bool -> Constrexpr.constr_expr -> Constrexpr.constr_expr -> int -> Constrexpr.constr_expr -> (Term.pconstant -> - Term.constr option ref -> + Indfun_common.tcc_lemma_value ref -> Term.pconstant -> Term.pconstant -> int -> EConstr.types -> int -> EConstr.constr -> 'a) -> Constrexpr.constr_expr list -> unit diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4 index ece0adb071..ca5d198c23 100644 --- a/plugins/ltac/g_ltac.ml4 +++ b/plugins/ltac/g_ltac.ml4 @@ -335,7 +335,7 @@ GEXTEND Gram | IDENT "all"; ":" -> SelectAll ] ] ; tactic_mode: - [ [ g = OPT toplevel_selector; tac = G_vernac.subgoal_command -> tac g ] ] + [ [ g = OPT toplevel_selector; tac = G_vernac.query_command -> tac g ] ] ; command: [ [ IDENT "Proof"; "with"; ta = Pltac.tactic; diff --git a/pretyping/classops.ml b/pretyping/classops.ml index 632ba0d9cd..e9b3d197bc 100644 --- a/pretyping/classops.ml +++ b/pretyping/classops.ml @@ -388,7 +388,7 @@ let add_coercion_in_graph (ic,source,target) = old_inheritance_graph end; let is_ambig = match !ambig_paths with [] -> false | _ -> true in - if is_ambig && is_verbose () then + if is_ambig && not !quiet then Feedback.msg_info (message_ambig !ambig_paths) type coercion = { diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml index 2eff1936f4..b16d044956 100644 --- a/pretyping/patternops.ml +++ b/pretyping/patternops.ml @@ -220,6 +220,8 @@ let instantiate_pattern env sigma lvar c = ctx in let c = substl inst c in + (** FIXME: Stupid workaround to pattern_of_constr being evar sensitive *) + let c = Evarutil.nf_evar sigma c in pattern_of_constr env sigma (EConstr.Unsafe.to_constr c) with Not_found (* List.index failed *) -> let vars = diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index cfc2e48d11..e4a87739b1 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -107,7 +107,7 @@ open Decl_kinds | SearchString (s,sc) -> qs s ++ pr_opt (fun sc -> str "%" ++ str sc) sc let pr_search a gopt b pr_p = - pr_opt (fun g -> int g ++ str ":"++ spc()) gopt + pr_opt (fun g -> Proof_global.pr_goal_selector g ++ str ":"++ spc()) gopt ++ match a with | SearchHead c -> keyword "SearchHead" ++ spc() ++ pr_p c ++ pr_in_out_modules b @@ -497,7 +497,7 @@ open Decl_kinds | PrintVisibility s -> keyword "Print Visibility" ++ pr_opt str s | PrintAbout (qid,gopt) -> - pr_opt (fun g -> int g ++ str ":"++ spc()) gopt + pr_opt (fun g -> Proof_global.pr_goal_selector g ++ str ":"++ spc()) gopt ++ keyword "About" ++ spc() ++ pr_smart_global qid | PrintImplicit qid -> keyword "Print Implicit" ++ spc() ++ pr_smart_global qid @@ -619,8 +619,6 @@ open Decl_kinds return (keyword "Timeout " ++ int n ++ spc() ++ pr_vernac_body v) | VernacFail v -> return (keyword "Fail" ++ spc() ++ pr_vernac_body v) - | VernacError _ -> - return (keyword "No-parsing-rule for VernacError") (* Syntax *) | VernacOpenCloseScope (_,(opening,sc)) -> @@ -1140,7 +1138,8 @@ open Decl_kinds spc() ++ keyword "in" ++ spc () ++ pr_lconstr c) | None -> hov 2 (keyword "Check" ++ spc() ++ pr_lconstr c) in - let pr_i = match io with None -> mt () | Some i -> int i ++ str ": " in + let pr_i = match io with None -> mt () + | Some i -> Proof_global.pr_goal_selector i ++ str ": " in return (pr_i ++ pr_mayeval r c) | VernacGlobalCheck c -> return (hov 2 (keyword "Type" ++ pr_constrarg c)) @@ -1222,7 +1221,7 @@ open Decl_kinds | Egramml.GramTerminal s :: rl, cl -> str s :: aux rl cl | [], [] -> [] | _ -> assert false in - hov 1 (pr_sequence (fun x -> x) (aux rl cl)) + hov 1 (pr_sequence identity (aux rl cl)) with Not_found -> hov 1 (str "TODO(" ++ str (fst s) ++ spc () ++ prlist_with_sep sep pr_arg cl ++ str ")") diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index e4cba6f07d..5f4a7766f3 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -88,7 +88,7 @@ type proof_terminator = proof_ending -> unit type closed_proof = proof_object * proof_terminator type pstate = { - pid : Id.t; + pid : Id.t; (* the name of the theorem whose proof is being constructed *) terminator : proof_terminator CEphemeron.key; endline_tactic : Genarg.glob_generic_argument option; section_vars : Context.Named.t option; @@ -671,16 +671,18 @@ let _ = let default_goal_selector = ref (Vernacexpr.SelectNth 1) let get_default_goal_selector () = !default_goal_selector -let print_range_selector (i, j) = - if i = j then string_of_int i - else string_of_int i ^ "-" ^ string_of_int j +let pr_range_selector (i, j) = + if i = j then int i + else int i ++ str "-" ++ int j -let print_goal_selector = function - | Vernacexpr.SelectAll -> "all" - | Vernacexpr.SelectNth i -> string_of_int i - | Vernacexpr.SelectList l -> "[" ^ - String.concat ", " (List.map print_range_selector l) ^ "]" - | Vernacexpr.SelectId id -> Id.to_string id +let pr_goal_selector = function + | Vernacexpr.SelectAll -> str "all" + | Vernacexpr.SelectNth i -> int i + | Vernacexpr.SelectList l -> + str "[" + ++ prlist_with_sep pr_comma pr_range_selector l + ++ str "]" + | Vernacexpr.SelectId id -> Id.print id let parse_goal_selector = function | "all" -> Vernacexpr.SelectAll @@ -699,7 +701,10 @@ let _ = optdepr = false; optname = "default goal selector" ; optkey = ["Default";"Goal";"Selector"] ; - optread = begin fun () -> print_goal_selector !default_goal_selector end; + optread = begin fun () -> + string_of_ppcmds + (pr_goal_selector !default_goal_selector) + end; optwrite = begin fun n -> default_goal_selector := parse_goal_selector n end diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli index 3b2cc6b23b..6bb6f5e2cb 100644 --- a/proofs/proof_global.mli +++ b/proofs/proof_global.mli @@ -198,6 +198,7 @@ end (* *) (**********************************************************) +val pr_goal_selector : Vernacexpr.goal_selector -> Pp.std_ppcmds val get_default_goal_selector : unit -> Vernacexpr.goal_selector module V82 : sig diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index fb6adaec5f..c4f392f201 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -202,8 +202,7 @@ let rec classify_vernac e = (* What are these? *) | VernacToplevelControl _ | VernacRestoreState _ - | VernacWriteState _ - | VernacError _ -> VtUnknown, VtNow + | VernacWriteState _ -> VtUnknown, VtNow (* Plugins should classify their commands *) | VernacExtend (s,l) -> try List.assoc s !classifiers l () diff --git a/stm/workerLoop.ml b/stm/workerLoop.ml index 50b42512cb..86ef59dc30 100644 --- a/stm/workerLoop.ml +++ b/stm/workerLoop.ml @@ -13,7 +13,7 @@ let rec parse = function let loop init args = let args = parse args in - Flags.make_silent true; + Flags.quiet := true; init (); CoqworkmgrApi.init !Flags.async_proofs_worker_priority; args diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index ea19660931..df222eed80 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -590,7 +590,7 @@ let make_resolve_hyp env sigma st flags only_classes pri decl = info.Vernacexpr.hint_pattern } in make_resolves env sigma ~name:(PathHints path) - (true,false,Flags.is_verbose()) info false + (true,false,not !Flags.quiet) info false (IsConstr (EConstr.of_constr c,Univ.ContextSet.empty))) hints) else [] diff --git a/tactics/hints.ml b/tactics/hints.ml index 77ed4330c1..bcc068d3da 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -1160,7 +1160,7 @@ let add_resolves env sigma clist local dbnames = (fun dbname -> let r = List.flatten (List.map (fun (pri, poly, hnf, path, gr) -> - make_resolves env sigma (true,hnf,Flags.is_verbose()) + make_resolves env sigma (true,hnf,not !Flags.quiet) pri poly ~name:path gr) clist) in let hint = make_hint ~local dbname (AddHints r) in diff --git a/test-suite/bugs/closed/4306.v b/test-suite/bugs/closed/4306.v new file mode 100644 index 0000000000..4aef5bb95e --- /dev/null +++ b/test-suite/bugs/closed/4306.v @@ -0,0 +1,32 @@ +Require Import List. +Require Import Arith. +Require Import Recdef. +Require Import Omega. + +Function foo (xys : (list nat * list nat)) {measure (fun xys => length (fst xys) + length (snd xys))} : list nat := + match xys with + | (nil, _) => snd xys + | (_, nil) => fst xys + | (x :: xs', y :: ys') => match Compare_dec.nat_compare x y with + | Lt => x :: foo (xs', y :: ys') + | Eq => x :: foo (xs', ys') + | Gt => y :: foo (x :: xs', ys') + end + end. +Proof. + intros; simpl; omega. + intros; simpl; omega. + intros; simpl; omega. +Qed. + +Function bar (xys : (list nat * list nat)) {measure (fun xys => length (fst xys) + length (snd xys))} : list nat := + let (xs, ys) := xys in + match (xs, ys) with + | (nil, _) => ys + | (_, nil) => xs + | (x :: xs', y :: ys') => match Compare_dec.nat_compare x y with + | Lt => x :: foo (xs', ys) + | Eq => x :: foo (xs', ys') + | Gt => y :: foo (xs, ys') + end + end.
\ No newline at end of file diff --git a/test-suite/bugs/closed/5476.v b/test-suite/bugs/closed/5476.v new file mode 100644 index 0000000000..b2d9d943bc --- /dev/null +++ b/test-suite/bugs/closed/5476.v @@ -0,0 +1,28 @@ +Require Setoid. + +Goal forall (P : Prop) (T : Type) (m m' : T) (T0 T1 : Type) (P2 : forall _ : +Prop, Prop) + (P0 : Set) (x0 : P0) (P1 : forall (_ : P0) (_ : T), Prop) + (P3 : forall (_ : forall (_ : P0) (_ : T0) (_ : Prop), Prop) (_ : +T) (_ : Prop), Prop) + (o : forall _ : P0, option T1) + (_ : P3 + (fun (k : P0) (_ : T0) (_ : Prop) => + match o k return Prop with + | Some _ => True + | None => False + end) m' P) (_ : P2 (P1 x0 m)) + (_ : forall (f : forall (_ : P0) (_ : T0) (_ : Prop), Prop) (m1 m2 +: T) + (k : P0) (e : T0) (_ : P2 (P1 k m1)), iff (P3 f m2 P) +(f k e (P3 f m1 P))), False. +Proof. + intros ???????????? H0 H H1. + rewrite H1 in H0; eauto with nocore. + { lazymatch goal with + | H : match ?X with _ => _ end |- _ + => first [ lazymatch goal with + | [ H' : context[X] |- _ ] => idtac H + end + | fail 1 "could not find" X ] + end. diff --git a/test-suite/output/Search.out b/test-suite/output/Search.out index 81fda176ec..7446c17d98 100644 --- a/test-suite/output/Search.out +++ b/test-suite/output/Search.out @@ -98,6 +98,14 @@ h: n <> newdef n h': newdef n <> n h: n <> newdef n h: n <> newdef n +h: n <> newdef n +h': newdef n <> n +The command has indeed failed with message: +No such goal. +The command has indeed failed with message: +Query commands only support the single numbered goal selector. +The command has indeed failed with message: +Query commands only support the single numbered goal selector. h: P n h': ~ P n h: P n diff --git a/test-suite/output/Search.v b/test-suite/output/Search.v index 2a0f0b407c..82096f29bf 100644 --- a/test-suite/output/Search.v +++ b/test-suite/output/Search.v @@ -10,11 +10,19 @@ Search (@eq _ _ _) true -false "prop" -"intro". (* andb_prop *) Definition newdef := fun x:nat => x. Goal forall n:nat, n <> newdef n -> newdef n <> n -> False. - intros n h h'. + cut False. + intros _ n h h'. Search n. (* search hypothesis *) Search newdef. (* search hypothesis *) Search ( _ <> newdef _). (* search hypothesis, pattern *) Search ( _ <> newdef _) -"h'". (* search hypothesis, pattern *) + + 1:Search newdef. + 2:Search newdef. + + Fail 3:Search newdef. + Fail 1-2:Search newdef. + Fail all:Search newdef. Abort. Goal forall n (P:nat -> Prop), P n -> ~P n -> False. diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index a4dcefcbde..f5f43ff66f 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -215,7 +215,7 @@ let glob_opt = ref false let add_compile verbose s = set_batch_mode (); - Flags.make_silent true; + Flags.quiet := true; if not !glob_opt then Dumpglob.dump_to_dotglob (); (** make the file name explicit; needed not to break up Coq loadpath stuff. *) let s = @@ -384,7 +384,7 @@ let vio_tasks = ref [] let add_vio_task f = set_batch_mode (); - Flags.make_silent true; + Flags.quiet := true; vio_tasks := f :: !vio_tasks let check_vio_tasks () = @@ -398,7 +398,7 @@ let vio_files_j = ref 0 let vio_checking = ref false let add_vio_file f = set_batch_mode (); - Flags.make_silent true; + Flags.quiet := true; vio_files := f :: !vio_files let set_vio_checking_j opt j = @@ -563,7 +563,7 @@ let parse_args arglist = |"-output-context" -> output_context := true |"-profile-ltac" -> Flags.profile_ltac := true |"-q" -> no_load_rc () - |"-quiet"|"-silent" -> Flags.make_silent true; Flags.make_warn false + |"-quiet"|"-silent" -> Flags.quiet := true; Flags.make_warn false |"-quick" -> Flags.compilation_mode := BuildVio |"-list-tags" -> print_tags := true |"-time" -> Flags.time := true diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index 84330b88ac..3359a16721 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -116,7 +116,7 @@ let rec interp_vernac sid po (loc,com) = load_vernac verbosely sid f | v -> try - let nsid, ntip = Stm.add sid (Flags.is_verbose()) (loc,v) in + let nsid, ntip = Stm.add sid (not !Flags.quiet) (loc,v) in (* Main STM interaction *) if ntip <> `NewTip then @@ -128,7 +128,7 @@ let rec interp_vernac sid po (loc,com) = (* We could use a more refined criteria that depends on the vernac. For now we imitate the old approach. *) - let hide_goals = !Flags.batch_mode || is_query v || + let hide_goals = !Flags.batch_mode || is_query v || !Flags.quiet || not (Proof_global.there_are_pending_proofs ()) in if not hide_goals then Feedback.msg_notice (pr_open_cur_subgoals ()); diff --git a/vernac/command.ml b/vernac/command.ml index 5ec708446d..45ff579552 100644 --- a/vernac/command.ml +++ b/vernac/command.ml @@ -234,7 +234,7 @@ match local with let _ = declare_variable ident decl in let () = assumption_message ident in let () = - if is_verbose () && Pfedit.refining () then + if not !Flags.quiet && Pfedit.refining () then Feedback.msg_info (str"Variable" ++ spc () ++ pr_id ident ++ strbrk " is not visible from current goals") in diff --git a/vernac/mltop.ml b/vernac/mltop.ml index 2396cf04a4..056ffca5c8 100644 --- a/vernac/mltop.ml +++ b/vernac/mltop.ml @@ -138,7 +138,7 @@ let dir_ml_load s = match !load with | WithTop _ -> ml_load s | WithoutTop -> - let warn = Flags.is_verbose() in + let warn = not !Flags.quiet in let _,gname = find_file_in_path ~warn !coq_mlpath_copy s in ml_load gname @@ -365,7 +365,7 @@ let trigger_ml_object verb cache reinit ?path name = else begin let file = file_of_name (Option.default name path) in let path = - if_verbose_load (verb && is_verbose ()) load_ml_object name ?path file in + if_verbose_load (verb && not !quiet) load_ml_object name ?path file in add_loaded_module name (Some path); if cache then perform_cache_obj name end diff --git a/vernac/topfmt.ml b/vernac/topfmt.ml index a4acd3f24e..c25dd55fb7 100644 --- a/vernac/topfmt.ml +++ b/vernac/topfmt.ml @@ -112,26 +112,23 @@ let msgnl_with ?pre_hdr fmt strm = pp_with fmt (strm ++ fnl ()); Format.pp_print_flush fmt () -(* XXX: This is really painful! *) module Emacs = struct (* Special chars for emacs, to detect warnings inside goal output *) - let emacs_quote_start = String.make 1 (Char.chr 254) - let emacs_quote_end = String.make 1 (Char.chr 255) + let quote_warning_start = "<warning>" + let quote_warning_end = "</warning>" - let emacs_quote_err g = - hov 0 (str emacs_quote_start ++ g ++ str emacs_quote_end) + let quote_info_start = "<infomsg>" + let quote_info_end = "</infomsg>" - let emacs_quote_info_start = "<infomsg>" - let emacs_quote_info_end = "</infomsg>" + let quote_emacs q_start q_end msg = + hov 0 (seq [str q_start; brk(0,0); msg; brk(0,0); str q_end]) - let emacs_quote_info g = - hov 0 (str emacs_quote_info_start++ brk(0,0) ++ g ++ brk(0,0) ++ str emacs_quote_info_end) + let quote_warning = quote_emacs quote_warning_start quote_warning_end + let quote_info = quote_emacs quote_info_start quote_info_end end -open Emacs - let dbg_hdr = tag Tag.debug (str "Debug:") ++ spc () let info_hdr = mt () let warn_hdr = tag Tag.warning (str "Warning:") ++ spc () @@ -144,13 +141,13 @@ let make_body quoter info ?pre_hdr s = (* The empty quoter *) let noq x = x (* Generic logger *) -let gen_logger dbg err ?pre_hdr level msg = match level with +let gen_logger dbg warn ?pre_hdr level msg = match level with | Debug -> msgnl_with !std_ft (make_body dbg dbg_hdr ?pre_hdr msg) | Info -> msgnl_with !std_ft (make_body dbg info_hdr ?pre_hdr msg) | Notice -> msgnl_with !std_ft (make_body noq info_hdr ?pre_hdr msg) | Warning -> Flags.if_warn (fun () -> - msgnl_with !err_ft (make_body err warn_hdr ?pre_hdr msg)) () - | Error -> msgnl_with !err_ft (make_body err err_hdr ?pre_hdr msg) + msgnl_with !err_ft (make_body warn warn_hdr ?pre_hdr msg)) () + | Error -> msgnl_with !err_ft (make_body noq err_hdr ?pre_hdr msg) (** Standard loggers *) @@ -261,7 +258,7 @@ let init_color_output () = - Warning/Error: emacs_quote_err - Notice: unquoted *) -let emacs_logger = gen_logger emacs_quote_info emacs_quote_err +let emacs_logger = gen_logger Emacs.quote_info Emacs.quote_warning (* Output to file, used only in extraction so a candidate for removal *) let ft_logger old_logger ft ?loc level mesg = diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 92b1a59562..0a5a000fec 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -780,7 +780,7 @@ let vernac_require from import qidl = in let locate (loc, qid) = try - let warn = Flags.is_verbose () in + let warn = not !Flags.quiet in let (_, dir, f) = Library.locate_qualified_library ?root ~warn qid in (dir, f) with @@ -1232,8 +1232,8 @@ let _ = optdepr = false; optname = "silent"; optkey = ["Silent"]; - optread = is_silent; - optwrite = make_silent } + optread = (fun () -> !Flags.quiet); + optwrite = ((:=) Flags.quiet) } let _ = declare_bool_option @@ -1533,7 +1533,14 @@ let get_current_context_of_args = function | Some n -> get_goal_context n | None -> get_current_context () -let vernac_check_may_eval redexp glopt rc = +let query_command_selector ~loc = function + | None -> None + | Some (SelectNth n) -> Some n + | _ -> user_err ~loc ~hdr:"query_command_selector" + (str "Query commands only support the single numbered goal selector.") + +let vernac_check_may_eval ~loc redexp glopt rc = + let glopt = query_command_selector ~loc glopt in let (sigma, env) = get_current_context_of_args glopt in let sigma', c = interp_open_constr env sigma rc in let c = EConstr.Unsafe.to_constr c in @@ -1595,9 +1602,10 @@ exception NoHyp (* Printing "About" information of a hypothesis of the current goal. We only print the type and a small statement to this comes from the goal. Precondition: there must be at least one current goal. *) -let print_about_hyp_globs ref_or_by_not glnumopt = +let print_about_hyp_globs ~loc ref_or_by_not glopt = let open Context.Named.Declaration in try + let glnumopt = query_command_selector ~loc glopt in let gl,id = match glnumopt,ref_or_by_not with | None,AN (Ident (_loc,id)) -> (* goal number not given, catch any failure *) @@ -1605,8 +1613,8 @@ let print_about_hyp_globs ref_or_by_not glnumopt = | Some n,AN (Ident (_loc,id)) -> (* goal number given, catch if wong *) (try get_nth_goal n,id with - Failure _ -> user_err ~hdr:"print_about_hyp_globs" - (str "No such goal: " ++ int n ++ str ".")) + Failure _ -> user_err ~loc ~hdr:"print_about_hyp_globs" + (str "No such goal: " ++ int n ++ str ".")) | _ , _ -> raise NoHyp in let hyps = pf_hyps gl in let decl = Context.Named.lookup id hyps in @@ -1619,7 +1627,7 @@ let print_about_hyp_globs ref_or_by_not glnumopt = | NoHyp | Not_found -> print_about ref_or_by_not -let vernac_print = let open Feedback in function +let vernac_print ~loc = let open Feedback in function | PrintTables -> msg_notice (print_tables ()) | PrintFullContext-> msg_notice (print_full_context_typ ()) | PrintSectionContext qid -> msg_notice (print_sec_context_typ qid) @@ -1664,7 +1672,7 @@ let vernac_print = let open Feedback in function | PrintVisibility s -> msg_notice (Notation.pr_visibility (Constrextern.without_symbols pr_lglob_constr) s) | PrintAbout (ref_or_by_not,glnumopt) -> - msg_notice (print_about_hyp_globs ref_or_by_not glnumopt) + msg_notice (print_about_hyp_globs ~loc ref_or_by_not glnumopt) | PrintImplicit qid -> dump_global qid; msg_notice (print_impargs qid) | PrintAssumptions (o,t,r) -> @@ -1729,7 +1737,8 @@ let _ = optread = (fun () -> !search_output_name_only); optwrite = (:=) search_output_name_only } -let vernac_search s gopt r = +let vernac_search ~loc s gopt r = + let gopt = query_command_selector ~loc gopt in let r = interp_search_restriction r in let env,gopt = match gopt with | None -> @@ -1935,9 +1944,6 @@ let interp ?proof ~loc locality poly c = | VernacBack _ -> anomaly (str "VernacBack not handled by Stm") | VernacBackTo _ -> anomaly (str "VernacBackTo not handled by Stm") - (* Horrible Hack that should die. *) - | VernacError e -> raise e - (* This one is possible to handle here *) | VernacAbort id -> CErrors.user_err (str "Abort cannot be used through the Load command") @@ -2039,11 +2045,11 @@ let interp ?proof ~loc locality poly c = | VernacAddOption (key,v) -> vernac_add_option key v | VernacMemOption (key,v) -> vernac_mem_option key v | VernacPrintOption key -> vernac_print_option key - | VernacCheckMayEval (r,g,c) -> vernac_check_may_eval r g c + | VernacCheckMayEval (r,g,c) -> vernac_check_may_eval ~loc r g c | VernacDeclareReduction (s,r) -> vernac_declare_reduction locality s r | VernacGlobalCheck c -> vernac_global_check c - | VernacPrint p -> vernac_print p - | VernacSearch (s,g,r) -> vernac_search s g r + | VernacPrint p -> vernac_print ~loc p + | VernacSearch (s,g,r) -> vernac_search ~loc s g r | VernacLocate l -> vernac_locate l | VernacRegister (id, r) -> vernac_register id r | VernacComments l -> if_verbose Feedback.msg_info (str "Comments ok\n") @@ -2173,7 +2179,7 @@ let with_fail b f = | HasNotFailed -> user_err ~hdr:"Fail" (str "The command has not failed!") | HasFailed msg -> - if is_verbose () || !test_mode || !ide_slave then Feedback.msg_info + if not !Flags.quiet || !test_mode || !ide_slave then Feedback.msg_info (str "The command has indeed failed with message:" ++ fnl () ++ msg) | _ -> assert false end |