diff options
45 files changed, 462 insertions, 213 deletions
diff --git a/Makefile.dev b/Makefile.dev index d9db7055f..8c1812da1 100644 --- a/Makefile.dev +++ b/Makefile.dev @@ -164,7 +164,7 @@ noreal: unicode logic arith bool zarith qarith lists sets fsets \ .PHONY: init theories-light noreal .PHONY: logic arith bool narith zarith qarith lists strings sets .PHONY: fsets relations wellfounded reals setoids sorting numbers -.PHONY: msets mmaps compat +.PHONY: msets mmaps compat parith classes program unicode structures vectors ################ ### 4) plugins diff --git a/doc/refman/Micromega.tex b/doc/refman/Micromega.tex index 1efed6ef7..4daf98f87 100644 --- a/doc/refman/Micromega.tex +++ b/doc/refman/Micromega.tex @@ -4,16 +4,19 @@ \asection{Short description of the tactics} -\tacindex{psatz} \tacindex{lra} +\tacindex{psatz} \tacindex{lra} \tacindex{lia} \tacindex{nia} \tacindex{nra} \label{sec:psatz-hurry} The {\tt Psatz} module ({\tt Require Import Psatz.}) gives access to several tactics for solving arithmetic goals over {\tt Z}, {\tt Q}, and {\tt R}:\footnote{Support for {\tt nat} and {\tt N} is obtained by - pre-processing the goal with the {\tt zify} tactic.} + pre-processing the goal with the {\tt zify} tactic.}. +It also possible to get the tactics for integers by a {\tt Require Import Lia}, rationals {\tt Require Import Lqa} +and reals {\tt Require Import Lra}. \begin{itemize} \item {\tt lia} is a decision procedure for linear integer arithmetic (see Section~\ref{sec:lia}); \item {\tt nia} is an incomplete proof procedure for integer non-linear arithmetic (see Section~\ref{sec:nia}); -\item {\tt lra} is a decision procedure for linear (real or rational) arithmetic goals (see Section~\ref{sec:lra}); +\item {\tt lra} is a decision procedure for linear (real or rational) arithmetic (see Section~\ref{sec:lra}); +\item {\tt nra} is an incomplete proof procedure for non-linear (real or rational) arithmetic (see Section~\ref{sec:nra}); \item {\tt psatz D n} where {\tt D} is {\tt Z} or {\tt Q} or {\tt R}, and {\tt n} is an optional integer limiting the proof search depth is is an incomplete proof procedure for non-linear arithmetic. It is based on @@ -114,36 +117,6 @@ The deductive power of {\tt lra} is the combined deductive power of {\tt ring\_s % There is also an overlap with the {\tt field} tactic {\emph e.g.}, {\tt x = 10 * x / 10} is solved by {\tt lra}. -\asection{{\tt psatz}: a proof procedure for non-linear arithmetic} -\label{sec:psatz} -The {\tt psatz} tactic explores the $\mathit{Cone}$ by increasing degrees -- hence the depth parameter $n$. -In theory, such a proof search is complete -- if the goal is provable the search eventually stops. -Unfortunately, the external oracle is using numeric (approximate) optimization techniques that might miss a -refutation. - -To illustrate the working of the tactic, consider we wish to prove the following Coq goal. -\begin{coq_eval} -Require Import ZArith Psatz. -Open Scope Z_scope. -\end{coq_eval} -\begin{coq_example*} -Goal forall x, -x^2 >= 0 -> x - 1 >= 0 -> False. -\end{coq_example*} -\begin{coq_eval} -intro x; psatz Z 2. -\end{coq_eval} -Such a goal is solved by {\tt intro x; psatz Z 2}. The oracle returns the -cone expression $2 \times (\mathbf{x-1}) + (\mathbf{x-1}) \times -(\mathbf{x-1}) + \mathbf{-x^2}$ (polynomial hypotheses are printed in -bold). By construction, this expression belongs to $\mathit{Cone}(\{-x^2, -x -1\})$. Moreover, by running {\tt ring} we obtain $-1$. By -Theorem~\ref{thm:psatz}, the goal is valid. -% - -%% \paragraph{The {\tt sos} tactic} -- where {\tt sos} stands for \emph{sum of squares} -- tries to prove that a -%% single polynomial $p$ is positive by expressing it as a sum of squares \emph{i.e.,} $\sum_{i\in S} p_i^2$. -%% This amounts to searching for $p$ in the cone without generators \emph{i.e.}, $Cone(\{\})$. -% \asection{{\tt lia}: a tactic for linear integer arithmetic} \tacindex{lia} @@ -219,22 +192,61 @@ Our current oracle tries to find an expression $e$ with a small range $[c_1,c_2] We generate $c_2 - c_1$ subgoals which contexts are enriched with an equation $e = i$ for $i \in [c_1,c_2]$ and recursively search for a proof. -\asection{{\tt nia}: a proof procedure for non-linear integer arithmetic} -\tacindex{nia} -\label{sec:nia} -The {\tt nia} tactic is an {\emph experimental} proof procedure for non-linear integer arithmetic. + +\asection{{\tt nra}: a proof procedure for non-linear arithmetic} +\tacindex{nra} +\label{sec:nra} +The {\tt nra} tactic is an {\emph experimental} proof procedure for non-linear arithmetic. % The tactic performs a limited amount of non-linear reasoning before running the -linear prover of {\tt lia}. +linear prover of {\tt lra}. This pre-processing does the following: \begin{itemize} \item If the context contains an arithmetic expression of the form $e[x^2]$ where $x$ is a monomial, the context is enriched with $x^2\ge 0$; \item For all pairs of hypotheses $e_1\ge 0$, $e_2 \ge 0$, the context is enriched with $e_1 \times e_2 \ge 0$. \end{itemize} -After pre-processing, the linear prover of {\tt lia} searches for a proof +After this pre-processing, the linear prover of {\tt lra} searches for a proof by abstracting monomials by variables. +\asection{{\tt nia}: a proof procedure for non-linear integer arithmetic} +\tacindex{nia} +\label{sec:nia} +The {\tt nia} tactic is a proof procedure for non-linear integer arithmetic. +% +It performs a pre-processing similar to {\tt nra}. The obtained goal is solved using the linear integer prover {\tt lia}. + +\asection{{\tt psatz}: a proof procedure for non-linear arithmetic} +\label{sec:psatz} +The {\tt psatz} tactic explores the $\mathit{Cone}$ by increasing degrees -- hence the depth parameter $n$. +In theory, such a proof search is complete -- if the goal is provable the search eventually stops. +Unfortunately, the external oracle is using numeric (approximate) optimization techniques that might miss a +refutation. + +To illustrate the working of the tactic, consider we wish to prove the following Coq goal. +\begin{coq_eval} +Require Import ZArith Psatz. +Open Scope Z_scope. +\end{coq_eval} +\begin{coq_example*} +Goal forall x, -x^2 >= 0 -> x - 1 >= 0 -> False. +\end{coq_example*} +\begin{coq_eval} +intro x; psatz Z 2. +\end{coq_eval} +Such a goal is solved by {\tt intro x; psatz Z 2}. The oracle returns the +cone expression $2 \times (\mathbf{x-1}) + (\mathbf{x-1}) \times +(\mathbf{x-1}) + \mathbf{-x^2}$ (polynomial hypotheses are printed in +bold). By construction, this expression belongs to $\mathit{Cone}(\{-x^2, +x -1\})$. Moreover, by running {\tt ring} we obtain $-1$. By +Theorem~\ref{thm:psatz}, the goal is valid. +% + +%% \paragraph{The {\tt sos} tactic} -- where {\tt sos} stands for \emph{sum of squares} -- tries to prove that a +%% single polynomial $p$ is positive by expressing it as a sum of squares \emph{i.e.,} $\sum_{i\in S} p_i^2$. +%% This amounts to searching for $p$ in the cone without generators \emph{i.e.}, $Cone(\{\})$. +% + %%% Local Variables: diff --git a/engine/evd.mli b/engine/evd.mli index 942414511..b47b389d1 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -98,11 +98,12 @@ type evar_info = { (** Optional content of the evar. *) evar_filter : Filter.t; (** Boolean mask over {!evar_hyps}. Should have the same length. - TODO: document me more. *) + When filtered out, the corresponding variable is not allowed to occur + in the solution *) evar_source : Evar_kinds.t located; (** Information about the evar. *) evar_candidates : constr list option; - (** TODO: document this *) + (** List of possible solutions when known that it is a finite list *) evar_extra : Store.t (** Extra store, used for clever hacks. *) } diff --git a/ide/coqOps.ml b/ide/coqOps.ml index 50b3f2c0a..5b6bad349 100644 --- a/ide/coqOps.ml +++ b/ide/coqOps.ml @@ -785,7 +785,6 @@ object(self) method private handle_failure_aux ?(move_insert=false) (safe_id, (loc : (int * int) option), msg) = - messages#clear; messages#push Feedback.Error msg; ignore(self#process_feedback ()); if Stateid.equal safe_id Stateid.dummy then Coq.lift (fun () -> ()) diff --git a/ide/ideutils.ml b/ide/ideutils.ml index fe69be9e4..06a132732 100644 --- a/ide/ideutils.ml +++ b/ide/ideutils.ml @@ -46,23 +46,37 @@ let xml_to_string xml = let () = iter (Richpp.repr xml) in Buffer.contents buf -let translate s = s - -let insert_xml ?(tags = []) (buf : #GText.buffer_skel) msg = +let insert_with_tags (buf : #GText.buffer_skel) mark rmark tags text = + (** FIXME: LablGTK2 does not export the C insert_with_tags function, so that + it has to reimplement its own helper function. Unluckily, it relies on + a slow algorithm, so that we have to have our own quicker version here. + Alas, it is still much slower than the native version... *) + if CList.is_empty tags then buf#insert ~iter:(buf#get_iter_at_mark mark) text + else + let it = buf#get_iter_at_mark mark in + let () = buf#move_mark rmark ~where:it in + let () = buf#insert ~iter:(buf#get_iter_at_mark mark) text in + let start = buf#get_iter_at_mark mark in + let stop = buf#get_iter_at_mark rmark in + let iter tag = buf#apply_tag tag start stop in + List.iter iter tags + +let insert_xml ?(mark = `INSERT) ?(tags = []) (buf : #GText.buffer_skel) msg = let open Xml_datatype in let tag name = - let name = translate name in match GtkText.TagTable.lookup buf#tag_table name with | None -> raise Not_found | Some tag -> new GText.tag tag in + let rmark = `MARK (buf#create_mark buf#start_iter) in let rec insert tags = function - | PCData s -> buf#insert ~tags:(List.rev tags) s + | PCData s -> insert_with_tags buf mark rmark tags s | Element (t, _, children) -> let tags = try tag t :: tags with Not_found -> tags in List.iter (fun xml -> insert tags xml) children in - insert tags (Richpp.repr msg) + let () = try insert tags (Richpp.repr msg) with _ -> () in + buf#delete_mark rmark let set_location = ref (function s -> failwith "not ready") diff --git a/ide/ideutils.mli b/ide/ideutils.mli index 491e8e823..e32a4d9e3 100644 --- a/ide/ideutils.mli +++ b/ide/ideutils.mli @@ -54,7 +54,7 @@ val flash_info : ?delay:int -> string -> unit val xml_to_string : Richpp.richpp -> string -val insert_xml : ?tags:GText.tag list -> +val insert_xml : ?mark:GText.mark -> ?tags:GText.tag list -> #GText.buffer_skel -> Richpp.richpp -> unit val set_location : (string -> unit) ref diff --git a/ide/preferences.ml b/ide/preferences.ml index 3241a962d..64327d74f 100644 --- a/ide/preferences.ml +++ b/ide/preferences.ml @@ -33,6 +33,7 @@ type obj = { } let preferences : obj Util.String.Map.t ref = ref Util.String.Map.empty +let unknown_preferences : string list Util.String.Map.t ref = ref Util.String.Map.empty class type ['a] repr = object @@ -617,19 +618,19 @@ let save_pref () = then Unix.mkdir (Minilib.coqide_config_home ()) 0o700; let () = try GtkData.AccelMap.save accel_file with _ -> () in let add = Util.String.Map.add in - let (++) x f = f x in let fold key obj accu = add key (obj.get ()) accu in - - (Util.String.Map.fold fold !preferences Util.String.Map.empty) ++ - Config_lexer.print_file pref_file + let prefs = Util.String.Map.fold fold !preferences Util.String.Map.empty in + let prefs = Util.String.Map.fold Util.String.Map.add !unknown_preferences prefs in + Config_lexer.print_file pref_file prefs let load_pref () = let () = try GtkData.AccelMap.load loaded_accel_file with _ -> () in let m = Config_lexer.load_file loaded_pref_file in let iter name v = - try (Util.String.Map.find name !preferences).set v - with _ -> () + if Util.String.Map.mem name !preferences then + try (Util.String.Map.find name !preferences).set v with _ -> () + else unknown_preferences := Util.String.Map.add name v !unknown_preferences in Util.String.Map.iter iter m diff --git a/ide/wg_MessageView.ml b/ide/wg_MessageView.ml index 758f383d6..0330b8eff 100644 --- a/ide/wg_MessageView.ml +++ b/ide/wg_MessageView.ml @@ -43,6 +43,7 @@ let message_view () : message_view = ~tag_table:Tags.Message.table () in let text_buffer = new GText.buffer buffer#as_buffer in + let mark = buffer#create_mark ~left_gravity:false buffer#start_iter in let box = GPack.vbox () in let scroll = GBin.scrolled_window ~vpolicy:`AUTOMATIC ~hpolicy:`AUTOMATIC ~packing:(box#pack ~expand:true) () in @@ -69,7 +70,8 @@ let message_view () : message_view = new message_view_signals_impl box#as_widget push method clear = - buffer#set_text "" + buffer#set_text ""; + buffer#move_mark (`MARK mark) ~where:buffer#start_iter method push level msg = let tags = match level with @@ -83,8 +85,9 @@ let message_view () : message_view = | Xml_datatype.Element (_, _, children) -> List.exists non_empty children in if non_empty (Richpp.repr msg) then begin - Ideutils.insert_xml buffer ~tags msg; - buffer#insert (*~tags*) "\n"; + let mark = `MARK mark in + Ideutils.insert_xml ~mark buffer ~tags msg; + buffer#insert ~iter:(buffer#get_iter_at_mark mark) "\n"; push#call (level, msg) end diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index f3e0682bd..fcb4a345e 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -124,6 +124,14 @@ let rec cases_pattern_fold_map loc g e = function let e',patl' = List.fold_map (cases_pattern_fold_map loc g) e patl in e', PatCstr (loc,cstr,patl',na') +let subst_binder_type_vars l = function + | Evar_kinds.BinderType (Name id) as e -> + let id = + try match Id.List.assoc id l with GVar(_,id') -> id' | _ -> id + with Not_found -> id in + Evar_kinds.BinderType (Name id) + | e -> e + let rec subst_glob_vars l = function | GVar (_,id) as r -> (try Id.List.assoc id l with Not_found -> r) | GProd (loc,Name id,bk,t,c) -> @@ -136,6 +144,7 @@ let rec subst_glob_vars l = function try match Id.List.assoc id l with GVar(_,id') -> id' | _ -> id with Not_found -> id in GLambda (loc,Name id,bk,subst_glob_vars l t,subst_glob_vars l c) + | GHole (loc,x,naming,arg) -> GHole (loc,subst_binder_type_vars l x,naming,arg) | r -> map_glob_constr (subst_glob_vars l) r (* assume: id is not binding *) let ldots_var = Id.of_string ".." @@ -1128,13 +1137,15 @@ let match_notation_constr u c (metas,pat) = List.fold_right (fun (x,(scl,typ)) (terms',termlists',binders') -> match typ with | NtnTypeConstr -> - ((Id.List.assoc x terms, scl)::terms',termlists',binders') + let term = try Id.List.assoc x terms with Not_found -> raise No_match in + ((term, scl)::terms',termlists',binders') | NtnTypeOnlyBinder -> ((find_binder x, scl)::terms',termlists',binders') | NtnTypeConstrList -> (terms',(Id.List.assoc x termlists,scl)::termlists',binders') | NtnTypeBinderList -> - (terms',termlists',(Id.List.assoc x binderlists,scl)::binders')) + let bl = try Id.List.assoc x binderlists with Not_found -> raise No_match in + (terms',termlists',(bl, scl)::binders')) metas ([],[],[]) (* Matching cases pattern *) diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli index 156e00368..ed44704df 100644 --- a/intf/vernacexpr.mli +++ b/intf/vernacexpr.mli @@ -106,7 +106,7 @@ type showable = | ShowTree | ShowProofNames | ShowIntros of bool - | ShowMatch of lident + | ShowMatch of reference | ShowThesis type comment = diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml index 3864df6c9..ef4b50130 100644 --- a/kernel/nativecode.ml +++ b/kernel/nativecode.ml @@ -1929,13 +1929,15 @@ let compile_constant env sigma prefix ~interactive con cb = arg|]))):: [Glet(gn, mkMLlam [|c_uid|] code)], Linked prefix -let loaded_native_files = ref ([] : string list) +module StringOrd = struct type t = string let compare = String.compare end +module StringSet = Set.Make(StringOrd) -let is_loaded_native_file s = String.List.mem s !loaded_native_files +let loaded_native_files = ref StringSet.empty + +let is_loaded_native_file s = StringSet.mem s !loaded_native_files let register_native_file s = - if not (is_loaded_native_file s) then - loaded_native_files := s :: !loaded_native_files + loaded_native_files := StringSet.add s !loaded_native_files let is_code_loaded ~interactive name = match !name with diff --git a/library/library.ml b/library/library.ml index 12090183a..d44f796a7 100644 --- a/library/library.ml +++ b/library/library.ml @@ -452,13 +452,13 @@ let intern_from_file f = module DPMap = Map.Make(DirPath) let rec intern_library (needed, contents) (dir, f) from = - Feedback.feedback(Feedback.FileDependency (from, DirPath.to_string dir)); (* Look if in the current logical environment *) try (find_library dir).libsum_digests, (needed, contents) with Not_found -> (* Look if already listed and consequently its dependencies too *) try (DPMap.find dir contents).library_digests, (needed, contents) with Not_found -> + Feedback.feedback(Feedback.FileDependency (from, DirPath.to_string dir)); (* [dir] is an absolute name which matches [f] which must be in loadpath *) let f = match f with Some f -> f | None -> try_locate_absolute_library dir in let m = intern_from_file f in @@ -468,16 +468,18 @@ let rec intern_library (needed, contents) (dir, f) from = pr_dirpath m.library_name ++ spc () ++ str "and not library" ++ spc() ++ pr_dirpath dir); Feedback.feedback (Feedback.FileLoaded(DirPath.to_string dir, f)); - m.library_digests, intern_library_deps (needed, contents) dir m (Some f) + m.library_digests, intern_library_deps (needed, contents) dir m f and intern_library_deps libs dir m from = let needed, contents = Array.fold_left (intern_mandatory_library dir from) libs m.library_deps in (dir :: needed, DPMap.add dir m contents ) and intern_mandatory_library caller from libs (dir,d) = - let digest, libs = intern_library libs (dir, None) from in + let digest, libs = intern_library libs (dir, None) (Some from) in if not (Safe_typing.digest_match ~actual:digest ~required:d) then - errorlabstrm "" (str "Compiled library " ++ pr_dirpath caller ++ str ".vo makes inconsistent assumptions over library " ++ pr_dirpath dir); + errorlabstrm "" (str "Compiled library " ++ pr_dirpath caller ++ + str " (in file " ++ str from ++ str ") makes inconsistent assumptions \ + over library " ++ pr_dirpath dir); libs let rec_intern_library libs (dir, f) = @@ -551,12 +553,20 @@ let in_require : require_obj -> obj = let (f_xml_require, xml_require) = Hook.make ~default:ignore () +let warn_require_in_module = + CWarnings.create ~name:"require-in-module" ~category:"deprecated" + (fun () -> strbrk "Require inside a module is" ++ + strbrk " deprecated and strongly discouraged. " ++ + strbrk "You can Require a module at toplevel " ++ + strbrk "and optionally Import it inside another one.") + let require_library_from_dirpath modrefl export = let needed, contents = List.fold_left rec_intern_library ([], DPMap.empty) modrefl in let needed = List.rev_map (fun dir -> DPMap.find dir contents) needed in let modrefl = List.map fst modrefl in if Lib.is_module_or_modtype () then begin + warn_require_in_module (); add_anonymous_leaf (in_require (needed,modrefl,None)); Option.iter (fun exp -> add_anonymous_leaf (in_import_library (modrefl,exp))) diff --git a/ltac/extratactics.ml4 b/ltac/extratactics.ml4 index be47293fc..e50b0520b 100644 --- a/ltac/extratactics.ml4 +++ b/ltac/extratactics.ml4 @@ -816,9 +816,11 @@ END TACTIC EXTEND is_evar | [ "is_evar" constr(x) ] -> - [ match kind_of_term x with + [ Proofview.tclBIND Proofview.tclEVARMAP begin fun sigma -> + match Evarutil.kind_of_term_upto sigma x with | Evar _ -> Proofview.tclUNIT () | _ -> Tacticals.New.tclFAIL 0 (str "Not an evar") + end ] END diff --git a/ltac/rewrite.ml b/ltac/rewrite.ml index 09454f3e8..153ca5bf5 100644 --- a/ltac/rewrite.ml +++ b/ltac/rewrite.ml @@ -1564,6 +1564,10 @@ let newfail n s = let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause = let open Proofview.Notations in + (** For compatibility *) + let beta_red _ sigma c = Reductionops.nf_betaiota sigma c in + let beta = Tactics.reduct_in_concl (beta_red, DEFAULTcast) in + let beta_hyp id = Tactics.reduct_in_hyp beta_red (id, InHyp) in let treat sigma res = match res with | None -> newfail 0 (str "Nothing to rewrite") @@ -1575,12 +1579,17 @@ let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause = let gls = List.rev (Evd.fold_undefined fold undef []) in match clause, prf with | Some id, Some p -> - let tac = Refine.refine ~unsafe:false { run = fun h -> Sigma (p, h, Sigma.refl) } <*> Proofview.Unsafe.tclNEWGOALS gls in + let tac = Tacticals.New.tclTHENLIST [ + Refine.refine ~unsafe:false { run = fun h -> Sigma.here p h }; + beta_hyp id; + Proofview.Unsafe.tclNEWGOALS gls; + ] in Proofview.Unsafe.tclEVARS undef <*> assert_replacing id newt tac | Some id, None -> Proofview.Unsafe.tclEVARS undef <*> - convert_hyp_no_check (LocalAssum (id, newt)) + convert_hyp_no_check (LocalAssum (id, newt)) <*> + beta_hyp id | None, Some p -> Proofview.Unsafe.tclEVARS undef <*> Proofview.Goal.enter { enter = begin fun gl -> @@ -1595,12 +1604,6 @@ let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause = Proofview.Unsafe.tclEVARS undef <*> convert_concl_no_check newt DEFAULTcast in - let beta_red _ sigma c = Reductionops.nf_betaiota sigma c in - let beta = Tactics.reduct_in_concl (beta_red, DEFAULTcast) in - let opt_beta = match clause with - | None -> Proofview.tclUNIT () - | Some id -> Tactics.reduct_in_hyp beta_red (id, InHyp) - in Proofview.Goal.nf_enter { enter = begin fun gl -> let concl = Proofview.Goal.concl gl in let env = Proofview.Goal.env gl in @@ -1625,7 +1628,7 @@ let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause = let sigma = match origsigma with None -> sigma | Some sigma -> sigma in treat sigma res <*> (** For compatibility *) - beta <*> opt_beta <*> Proofview.shelve_unifiable + beta <*> Proofview.shelve_unifiable with | PretypeError (env, evd, (UnsatisfiableConstraints _ as e)) -> raise (RewriteFailure (Himsg.explain_pretype_error env evd e)) diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml index aa7e096a9..8b2e1ee1a 100644 --- a/ltac/tacinterp.ml +++ b/ltac/tacinterp.ml @@ -1813,13 +1813,10 @@ and interp_atomic ist tac : unit Proofview.tactic = (* Conversion *) | TacReduce (r,cl) -> - (* spiwack: until the tactic is in the monad *) - Proofview.Trace.name_tactic (fun () -> Pp.str"<reduce>") begin Proofview.Goal.nf_s_enter { s_enter = begin fun gl -> let (sigma,r_interp) = interp_red_expr ist (pf_env gl) (project gl) r in Sigma.Unsafe.of_pair (Tactics.reduce r_interp (interp_clause ist (pf_env gl) (project gl) cl), sigma) end } - end | TacChange (None,c,cl) -> (* spiwack: until the tactic is in the monad *) Proofview.Trace.name_tactic (fun () -> Pp.str"<change>") begin diff --git a/parsing/cLexer.ml4 b/parsing/cLexer.ml4 index 2acccfdf5..bec891f7f 100644 --- a/parsing/cLexer.ml4 +++ b/parsing/cLexer.ml4 @@ -103,6 +103,9 @@ open Error let current_file = ref "" +let get_current_file () = + !current_file + let set_current_file ~fname = current_file := fname diff --git a/parsing/cLexer.mli b/parsing/cLexer.mli index d99ba3557..3b4891d9a 100644 --- a/parsing/cLexer.mli +++ b/parsing/cLexer.mli @@ -17,7 +17,13 @@ type location_table val location_table : unit -> location_table val restore_location_table : location_table -> unit -(** [set_current_file fname] sets the filename in locations emitted by the lexer *) + +(** [get_current_file fname] returns the filename used in locations emitted by + the lexer *) +val get_current_file : unit -> string + +(** [set_current_file fname] sets the filename used in locations emitted by the + lexer *) val set_current_file : fname:string -> unit val check_ident : string -> unit diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4 index b0ff8b64f..1e3c4b880 100644 --- a/parsing/g_proofs.ml4 +++ b/parsing/g_proofs.ml4 @@ -88,7 +88,7 @@ GEXTEND Gram | IDENT "Show"; IDENT "Proof" -> VernacShow ShowProof | IDENT "Show"; IDENT "Intro" -> VernacShow (ShowIntros false) | IDENT "Show"; IDENT "Intros" -> VernacShow (ShowIntros true) - | IDENT "Show"; IDENT "Match"; id = identref -> VernacShow (ShowMatch id) + | IDENT "Show"; IDENT "Match"; id = reference -> VernacShow (ShowMatch id) | IDENT "Show"; IDENT "Thesis" -> VernacShow ShowThesis | IDENT "Guarded" -> VernacCheckGuard (* Hints for Auto and EAuto *) diff --git a/plugins/micromega/Lia.v b/plugins/micromega/Lia.v index 52bf5ed3d..6974f8d99 100644 --- a/plugins/micromega/Lia.v +++ b/plugins/micromega/Lia.v @@ -8,7 +8,7 @@ (* *) (* Micromega: A reflexive tactic using the Positivstellensatz *) (* *) -(* Frédéric Besson (Irisa/Inria) 2013 *) +(* Frédéric Besson (Irisa/Inria) 2013-2016 *) (* *) (************************************************************************) @@ -19,24 +19,24 @@ Require Import VarMap. Require Coq.micromega.Tauto. Declare ML Module "micromega_plugin". + Ltac preprocess := zify ; unfold Z.succ in * ; unfold Z.pred in *. -Ltac lia := - preprocess; - xlia ; - abstract ( - intros __wit __varmap __ff ; - change (Tauto.eval_f (Zeval_formula (@find Z Z0 __varmap)) __ff) ; - apply (ZTautoChecker_sound __ff __wit); vm_cast_no_check (eq_refl true)). - -Ltac nia := - preprocess; - xnlia ; - abstract ( - intros __wit __varmap __ff ; - change (Tauto.eval_f (Zeval_formula (@find Z Z0 __varmap)) __ff) ; - apply (ZTautoChecker_sound __ff __wit); vm_cast_no_check (eq_refl true)). +Ltac zchange := + intros __wit __varmap __ff ; + change (Tauto.eval_f (Zeval_formula (@find Z Z0 __varmap)) __ff) ; + apply (ZTautoChecker_sound __ff __wit). + +Ltac zchecker_no_abstract := zchange ; vm_compute ; reflexivity. + +Ltac zchecker_abstract := abstract (zchange ; vm_cast_no_check (eq_refl true)). + +Ltac zchecker := zchecker_abstract || zchecker_no_abstract . + +Ltac lia := preprocess; xlia ; zchecker. + +Ltac nia := preprocess; xnlia ; zchecker. (* Local Variables: *) diff --git a/plugins/micromega/Lqa.v b/plugins/micromega/Lqa.v new file mode 100644 index 000000000..e3414b849 --- /dev/null +++ b/plugins/micromega/Lqa.v @@ -0,0 +1,54 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) +(* *) +(* Micromega: A reflexive tactic using the Positivstellensatz *) +(* *) +(* Frédéric Besson (Irisa/Inria) 2016 *) +(* *) +(************************************************************************) + +Require Import QMicromega. +Require Import QArith. +Require Import RingMicromega. +Require Import VarMap. +Require Coq.micromega.Tauto. +Declare ML Module "micromega_plugin". + +Ltac rchange := + intros __wit __varmap __ff ; + change (Tauto.eval_f (Qeval_formula (@find Q 0%Q __varmap)) __ff) ; + apply (QTautoChecker_sound __ff __wit). + +Ltac rchecker_no_abstract := rchange ; vm_compute ; reflexivity. +Ltac rchecker_abstract := abstract (rchange ; vm_cast_no_check (eq_refl true)). + +Ltac rchecker := (rchecker_abstract || rchecker_no_abstract). + +(** Here, lra stands for linear rational arithmetic *) +Ltac lra := lra_Q ; rchecker. + +(** Here, nra stands for non-linear rational arithmetic *) +Ltac nra := xnqa ; rchecker. + +Ltac xpsatz dom d := + let tac := lazymatch dom with + | Q => + (sos_Q || psatz_Q d) ; + (* If csdp is not installed, the previous step might not produce any + progress: the rest of the tactical will then fail. Hence the 'try'. *) + try rchecker + | _ => fail "Unsupported domain" + end in tac. + +Tactic Notation "psatz" constr(dom) int_or_var(n) := xpsatz dom n. +Tactic Notation "psatz" constr(dom) := xpsatz dom ltac:(-1). + + +(* Local Variables: *) +(* coding: utf-8 *) +(* End: *) diff --git a/plugins/micromega/Lra.v b/plugins/micromega/Lra.v new file mode 100644 index 000000000..4d9cf22dd --- /dev/null +++ b/plugins/micromega/Lra.v @@ -0,0 +1,55 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) +(* *) +(* Micromega: A reflexive tactic using the Positivstellensatz *) +(* *) +(* Frédéric Besson (Irisa/Inria) 2016 *) +(* *) +(************************************************************************) + +Require Import RMicromega. +Require Import QMicromega. +Require Import Rdefinitions. +Require Import RingMicromega. +Require Import VarMap. +Require Coq.micromega.Tauto. +Declare ML Module "micromega_plugin". + +Ltac rchange := + intros __wit __varmap __ff ; + change (Tauto.eval_f (Reval_formula (@find R 0%R __varmap)) __ff) ; + apply (RTautoChecker_sound __ff __wit). + +Ltac rchecker_no_abstract := rchange ; vm_compute ; reflexivity. +Ltac rchecker_abstract := abstract (rchange ; vm_cast_no_check (eq_refl true)). + +Ltac rchecker := rchecker_abstract || rchecker_no_abstract. + +(** Here, lra stands for linear real arithmetic *) +Ltac lra := unfold Rdiv in * ; lra_R ; rchecker. + +(** Here, nra stands for non-linear real arithmetic *) +Ltac nra := unfold Rdiv in * ; xnra ; rchecker. + +Ltac xpsatz dom d := + let tac := lazymatch dom with + | R => + (sos_R || psatz_R d) ; + (* If csdp is not installed, the previous step might not produce any + progress: the rest of the tactical will then fail. Hence the 'try'. *) + try rchecker + | _ => fail "Unsupported domain" + end in tac. + +Tactic Notation "psatz" constr(dom) int_or_var(n) := xpsatz dom n. +Tactic Notation "psatz" constr(dom) := xpsatz dom ltac:(-1). + + +(* Local Variables: *) +(* coding: utf-8 *) +(* End: *) diff --git a/plugins/micromega/Psatz.v b/plugins/micromega/Psatz.v index fafd8a5f2..c81c025a5 100644 --- a/plugins/micromega/Psatz.v +++ b/plugins/micromega/Psatz.v @@ -8,7 +8,7 @@ (* *) (* Micromega: A reflexive tactic using the Positivstellensatz *) (* *) -(* Frédéric Besson (Irisa/Inria) 2006-2008 *) +(* Frédéric Besson (Irisa/Inria) 2006-2016 *) (* *) (************************************************************************) @@ -21,50 +21,30 @@ Require Import Rdefinitions. Require Import RingMicromega. Require Import VarMap. Require Coq.micromega.Tauto. -Declare ML Module "micromega_plugin". +Require Lia. +Require Lra. +Require Lqa. -Ltac preprocess := - zify ; unfold Z.succ in * ; unfold Z.pred in *. +Declare ML Module "micromega_plugin". -Ltac lia := - preprocess; - xlia ; - abstract ( - intros __wit __varmap __ff ; - change (Tauto.eval_f (Zeval_formula (@find Z Z0 __varmap)) __ff) ; - apply (ZTautoChecker_sound __ff __wit); vm_cast_no_check (eq_refl true)). +Ltac lia := Lia.lia. -Ltac nia := - preprocess; - xnlia ; - abstract ( - intros __wit __varmap __ff ; - change (Tauto.eval_f (Zeval_formula (@find Z Z0 __varmap)) __ff) ; - apply (ZTautoChecker_sound __ff __wit); vm_cast_no_check (eq_refl true)). +Ltac nia := Lia.nia. Ltac xpsatz dom d := let tac := lazymatch dom with | Z => - (sos_Z || psatz_Z d) ; - abstract( - intros __wit __varmap __ff ; - change (Tauto.eval_f (Zeval_formula (@find Z Z0 __varmap)) __ff) ; - apply (ZTautoChecker_sound __ff __wit); vm_cast_no_check (eq_refl true)) + (sos_Z || psatz_Z d) ; Lia.zchecker | R => (sos_R || psatz_R d) ; (* If csdp is not installed, the previous step might not produce any progress: the rest of the tactical will then fail. Hence the 'try'. *) - try (abstract(intros __wit __varmap __ff ; - change (Tauto.eval_f (Reval_formula (@find R 0%R __varmap)) __ff) ; - apply (RTautoChecker_sound __ff __wit); vm_cast_no_check (eq_refl true))) - | Q => - (sos_Q || psatz_Q d) ; + try Lra.rchecker + | Q => (sos_Q || psatz_Q d) ; (* If csdp is not installed, the previous step might not produce any progress: the rest of the tactical will then fail. Hence the 'try'. *) - try (abstract(intros __wit __varmap __ff ; - change (Tauto.eval_f (Qeval_formula (@find Q 0%Q __varmap)) __ff) ; - apply (QTautoChecker_sound __ff __wit); vm_cast_no_check (eq_refl true))) + try Lqa.rchecker | _ => fail "Unsupported domain" end in tac. @@ -73,22 +53,9 @@ Tactic Notation "psatz" constr(dom) := xpsatz dom ltac:(-1). Ltac psatzl dom := let tac := lazymatch dom with - | Z => lia - | Q => - psatzl_Q ; - (* If csdp is not installed, the previous step might not produce any - progress: the rest of the tactical will then fail. Hence the 'try'. *) - try (abstract(intros __wit __varmap __ff ; - change (Tauto.eval_f (Qeval_formula (@find Q 0%Q __varmap)) __ff) ; - apply (QTautoChecker_sound __ff __wit); vm_cast_no_check (eq_refl true))) - | R => - unfold Rdiv in * ; - psatzl_R ; - (* If csdp is not installed, the previous step might not produce any - progress: the rest of the tactical will then fail. Hence the 'try'. *) - try abstract((intros __wit __varmap __ff ; - change (Tauto.eval_f (Reval_formula (@find R 0%R __varmap)) __ff) ; - apply (RTautoChecker_sound __ff __wit); vm_cast_no_check (eq_refl true))) + | Z => Lia.lia + | Q => Lqa.lra + | R => Lra.lra | _ => fail "Unsupported domain" end in tac. @@ -97,13 +64,7 @@ Ltac lra := first [ psatzl R | psatzl Q ]. Ltac nra := - unfold Rdiv in * ; - xnra ; - abstract - (intros __wit __varmap __ff ; - change (Tauto.eval_f (Reval_formula (@find R 0%R __varmap)) __ff) ; - apply (RTautoChecker_sound __ff __wit); vm_compute ; reflexivity). - + first [ Lra.nra | Lqa.nra ]. (* Local Variables: *) diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml index b8e5e66ca..faf3b3e69 100644 --- a/plugins/micromega/coq_micromega.ml +++ b/plugins/micromega/coq_micromega.ml @@ -1437,7 +1437,36 @@ let rcst_domain_spec = lazy { open Proofview.Notations - +(** Naive topological sort of constr according to the subterm-ordering *) + +(* An element is minimal x is minimal w.r.t y if + x <= y or (x and y are incomparable) *) + +let is_min le x y = + if le x y then true + else if le y x then false else true + +let is_minimal le l c = List.for_all (is_min le c) l + +let find_rem p l = + let rec xfind_rem acc l = + match l with + | [] -> (None, acc) + | x :: l -> if p x then (Some x, acc @ l) + else xfind_rem (x::acc) l in + xfind_rem [] l + +let find_minimal le l = find_rem (is_minimal le l) l + +let rec mk_topo_order le l = + match find_minimal le l with + | (None , _) -> [] + | (Some v,l') -> v :: (mk_topo_order le l') + + +let topo_sort_constr l = mk_topo_order Termops.dependent l + + (** * Instanciate the current Coq goal with a Micromega formula, a varmap, and a * witness. @@ -1464,7 +1493,7 @@ let micromega_order_change spec cert cert_typ env ff (*: unit Proofview.tactic* ] (Tacmach.pf_concl gl)) ; - Tactics.generalize env ; + Tactics.generalize (topo_sort_constr env) ; Tacticals.New.tclTHENLIST (List.map (fun id -> (Tactics.introduction id)) ids) ] end } @@ -1774,7 +1803,7 @@ let micromega_order_changer cert env ff = ("__wit", cert, cert_typ) ] (Tacmach.pf_concl gl))); - Tactics.generalize env ; + Tactics.generalize (topo_sort_constr env) ; Tacticals.New.tclTHENLIST (List.map (fun id -> (Tactics.introduction id)) ids) ] end } @@ -1851,7 +1880,7 @@ module Cache = PHashtable(struct let hash = Hashtbl.hash end) -let csdp_cache = "csdp.cache" +let csdp_cache = ".csdp.cache" (** * Build the command to call csdpcert, and launch it. This in turn will call @@ -1997,9 +2026,9 @@ module CacheQ = PHashtable(struct let hash = Hashtbl.hash end) -let memo_zlinear_prover = CacheZ.memo "lia.cache" (fun ((ce,b),s) -> lift_pexpr_prover (Certificate.lia ce b) s) -let memo_nlia = CacheZ.memo "nlia.cache" (fun ((ce,b),s) -> lift_pexpr_prover (Certificate.nlia ce b) s) -let memo_nra = CacheQ.memo "nra.cache" (fun (o,s) -> lift_pexpr_prover (Certificate.nlinear_prover o) s) +let memo_zlinear_prover = CacheZ.memo ".lia.cache" (fun ((ce,b),s) -> lift_pexpr_prover (Certificate.lia ce b) s) +let memo_nlia = CacheZ.memo ".nia.cache" (fun ((ce,b),s) -> lift_pexpr_prover (Certificate.nlia ce b) s) +let memo_nra = CacheQ.memo ".nra.cache" (fun (o,s) -> lift_pexpr_prover (Certificate.nlinear_prover o) s) @@ -2064,7 +2093,6 @@ let non_linear_prover_Z str o = { pp_f = fun o x -> pp_pol pp_z o (fst x) } - let linear_Z = { name = "lia"; get_option = get_lia_option; @@ -2100,11 +2128,7 @@ let tauto_lia ff = * solvers *) -let psatzl_Z = - micromega_gen parse_zarith Mc.negate Mc.normalise Mc.zunsat Mc.zdeduce zz_domain_spec - [ linear_Z ] - -let psatzl_Q = +let lra_Q = micromega_gen parse_qarith Mc.qnegate Mc.qnormalise Mc.qunsat Mc.qdeduce qq_domain_spec [ linear_prover_Q ] @@ -2112,7 +2136,7 @@ let psatz_Q i = micromega_gen parse_qarith Mc.qnegate Mc.qnormalise Mc.qunsat Mc.qdeduce qq_domain_spec [ non_linear_prover_Q "real_nonlinear_prover" (Some i) ] -let psatzl_R = +let lra_R = micromega_genr [ linear_prover_R ] let psatz_R i = @@ -2136,21 +2160,21 @@ let sos_R = micromega_genr [ non_linear_prover_R "pure_sos" None ] -let xlia = - try - micromega_gen parse_zarith Mc.negate Mc.normalise Mc.zunsat Mc.zdeduce zz_domain_spec +let xlia = micromega_gen parse_zarith Mc.negate Mc.normalise Mc.zunsat Mc.zdeduce zz_domain_spec [ linear_Z ] - with reraise -> (*Printexc.print_backtrace stdout ;*) raise reraise let xnlia = - try micromega_gen parse_zarith Mc.negate Mc.normalise Mc.zunsat Mc.zdeduce zz_domain_spec [ nlinear_Z ] - with reraise -> (*Printexc.print_backtrace stdout ;*) raise reraise let nra = micromega_genr [ nlinear_prover_R ] +let nqa = + micromega_gen parse_qarith Mc.qnegate Mc.qnormalise Mc.qunsat Mc.qdeduce qq_domain_spec + [ nlinear_prover_R ] + + (* Local Variables: *) (* coding: utf-8 *) diff --git a/plugins/micromega/g_micromega.ml4 b/plugins/micromega/g_micromega.ml4 index e6b5cc60d..974dcee87 100644 --- a/plugins/micromega/g_micromega.ml4 +++ b/plugins/micromega/g_micromega.ml4 @@ -37,6 +37,12 @@ TACTIC EXTEND NRA [ "xnra" ] -> [ (Coq_micromega.nra)] END +TACTIC EXTEND NQA +[ "xnqa" ] -> [ (Coq_micromega.nqa)] +END + + + TACTIC EXTEND Sos_Z | [ "sos_Z" ] -> [ (Coq_micromega.sos_Z) ] END @@ -50,11 +56,11 @@ TACTIC EXTEND Sos_R END TACTIC EXTEND LRA_Q -[ "psatzl_Q" ] -> [ (Coq_micromega.psatzl_Q) ] +[ "lra_Q" ] -> [ (Coq_micromega.lra_Q) ] END TACTIC EXTEND LRA_R -[ "psatzl_R" ] -> [ (Coq_micromega.psatzl_R) ] +[ "lra_R" ] -> [ (Coq_micromega.lra_R) ] END TACTIC EXTEND PsatzR diff --git a/plugins/micromega/vo.itarget b/plugins/micromega/vo.itarget index bf6a1a7db..cb4b2b8a5 100644 --- a/plugins/micromega/vo.itarget +++ b/plugins/micromega/vo.itarget @@ -10,4 +10,6 @@ Tauto.vo VarMap.vo ZCoeff.vo ZMicromega.vo -Lia.vo
\ No newline at end of file +Lia.vo +Lqa.vo +Lra.vo
\ No newline at end of file diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index 935e2d076..a00e4bab3 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -793,6 +793,22 @@ end let do_not_tag _ x = x +let split_token tag s = + let len = String.length s in + let rec parse_string off i = + if Int.equal i len then + if Int.equal off i then mt () else tag (str (String.sub s off (i - off))) + else if s.[i] == ' ' then + if Int.equal off i then parse_space 1 (succ i) + else tag (str (String.sub s off (i - off))) ++ parse_space 1 (succ i) + else parse_string off (succ i) + and parse_space spc i = + if Int.equal i len then str (String.make spc ' ') + else if s.[i] == ' ' then parse_space (succ spc) (succ i) + else str (String.make spc ' ') ++ parse_string i (succ i) + in + parse_string 0 0 + (** Instantiating Make with tagging functions that only add style information. *) include Make (struct @@ -801,7 +817,7 @@ include Make (struct let tag_evar = tag Tag.evar let tag_type = tag Tag.univ let tag_unparsing = function - | UnpTerminal s -> tag Tag.notation + | UnpTerminal s -> fun _ -> split_token (fun pp -> tag Tag.notation pp) s | _ -> do_not_tag () let tag_constr_expr = do_not_tag let tag_path = tag Tag.path diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 0d47b34df..40ce28dc0 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -591,7 +591,7 @@ module Make | ShowTree -> keyword "Show Tree" | ShowProofNames -> keyword "Show Conjectures" | ShowIntros b -> keyword "Show " ++ (if b then keyword "Intros" else keyword "Intro") - | ShowMatch id -> keyword "Show Match " ++ pr_lident id + | ShowMatch id -> keyword "Show Match " ++ pr_reference id | ShowThesis -> keyword "Show Thesis" in return (pr_showable s) diff --git a/proofs/refine.ml b/proofs/refine.ml index 139862b8f..28952b9a7 100644 --- a/proofs/refine.ml +++ b/proofs/refine.ml @@ -93,7 +93,7 @@ let refine ?(unsafe = true) f = Proofview.Goal.enter { enter = begin fun gl -> (** Select the goals *) let comb = CList.map_filter (Proofview.Unsafe.advance sigma) (CList.rev evs) in let sigma = CList.fold_left Proofview.Unsafe.mark_as_goal sigma comb in - let trace () = Pp.(hov 2 (str"refine"++spc()++ Hook.get pr_constrv env sigma c)) in + let trace () = Pp.(hov 2 (str"simple refine"++spc()++ Hook.get pr_constrv env sigma c)) in Proofview.Trace.name_tactic trace (Proofview.tclUNIT ()) >>= fun () -> Proofview.Unsafe.tclEVARS sigma >>= fun () -> Proofview.Unsafe.tclSETGOALS comb diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml index 73a90f611..2d1f725ef 100644 --- a/stm/asyncTaskQueue.ml +++ b/stm/asyncTaskQueue.ml @@ -229,10 +229,8 @@ module Make(T : Task) = struct | (Die | TQueue.BeingDestroyed) -> giveback_exec_token (); kill proc; exit () | Sys_error _ | Invalid_argument _ | End_of_file -> - giveback_exec_token (); T.on_task_cancellation_or_expiration_or_slave_death !last_task; - kill proc; - exit () + giveback_exec_token (); kill proc; exit () end module Pool = WorkerPool.Make(Model) diff --git a/stm/lemmas.ml b/stm/lemmas.ml index 5e4e34114..cf4143dbb 100644 --- a/stm/lemmas.ml +++ b/stm/lemmas.ml @@ -482,6 +482,18 @@ let start_proof_com kind thms hook = (* Saving a proof *) +let keep_admitted_vars = ref true + +let _ = + let open Goptions in + declare_bool_option + { optsync = true; + optdepr = false; + optname = "keep section variables in admitted proofs"; + optkey = ["Keep"; "Admitted"; "Variables"]; + optread = (fun () -> !keep_admitted_vars); + optwrite = (fun b -> keep_admitted_vars := b) } + let save_proof ?proof = function | Vernacexpr.Admitted -> let pe = @@ -495,7 +507,8 @@ let save_proof ?proof = function error "Admitted requires an explicit statement"; let typ = Option.get const_entry_type in let ctx = Evd.evar_context_universe_context (fst universes) in - Admitted(id, k, (const_entry_secctx, pi2 k, (typ, ctx), None), universes) + let sec_vars = if !keep_admitted_vars then const_entry_secctx else None in + Admitted(id, k, (sec_vars, pi2 k, (typ, ctx), None), universes) | None -> let pftree = Pfedit.get_pftreestate () in let id, k, typ = Pfedit.current_proof_statement () in @@ -504,7 +517,8 @@ let save_proof ?proof = function let pproofs, _univs = Proof_global.return_proof ~allow_partial:true () in let sec_vars = - match Pfedit.get_used_variables(), pproofs with + if not !keep_admitted_vars then None + else match Pfedit.get_used_variables(), pproofs with | Some _ as x, _ -> x | None, (pproof, _) :: _ -> let env = Global.env () in diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 1672b7bd1..f9f8e8715 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -1500,9 +1500,11 @@ let head_of_constr h c = let c = head_of_constr c in letin_tac None (Name h) c None Locusops.allHyps -let not_evar c = match kind_of_term c with -| Evar _ -> Tacticals.New.tclFAIL 0 (str"Evar") -| _ -> Proofview.tclUNIT () +let not_evar c = + Proofview.tclEVARMAP >>= fun sigma -> + match Evarutil.kind_of_term_upto sigma c with + | Evar _ -> Tacticals.New.tclFAIL 0 (str"Evar") + | _ -> Proofview.tclUNIT () let is_ground c gl = if Evarutil.is_ground_term (project gl) c then tclIDTAC gl diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 7519339ca..b54624f89 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -871,14 +871,17 @@ let reduction_clause redexp cl = (None, bind_red_expr_occurrences occs nbcl redexp)) cl let reduce redexp cl = + let trace () = Pp.(hov 2 (Pptactic.pr_atomic_tactic (Global.env()) (TacReduce (redexp,cl)))) in + Proofview.Trace.name_tactic trace begin Proofview.Goal.enter { enter = begin fun gl -> - let cl = concrete_clause_of (fun () -> Tacmach.New.pf_ids_of_hyps gl) cl in - let redexps = reduction_clause redexp cl in + let cl' = concrete_clause_of (fun () -> Tacmach.New.pf_ids_of_hyps gl) cl in + let redexps = reduction_clause redexp cl' in let check = match redexp with Fold _ | Pattern _ -> true | _ -> false in Tacticals.New.tclMAP (fun (where,redexp) -> e_reduct_option ~check (Redexpr.reduction_of_red_expr (Tacmach.New.pf_env gl) redexp) where) redexps end } + end (* Unfolding occurrences of a constant *) @@ -4945,7 +4948,7 @@ module New = struct let reduce_after_refine = reduce (Lazy {rBeta=true;rMatch=true;rFix=true;rCofix=true;rZeta=false;rDelta=false;rConst=[]}) - {onhyps=None; concl_occs=AllOccurrences } + {onhyps=Some []; concl_occs=AllOccurrences } let refine ?unsafe c = Refine.refine ?unsafe c <*> diff --git a/test-suite/.csdp.cache b/test-suite/.csdp.cache Binary files differnew file mode 100644 index 000000000..75dd38fde --- /dev/null +++ b/test-suite/.csdp.cache diff --git a/test-suite/bugs/closed/3920.v b/test-suite/bugs/closed/3920.v new file mode 100644 index 000000000..a4adb23cc --- /dev/null +++ b/test-suite/bugs/closed/3920.v @@ -0,0 +1,7 @@ +Require Import Setoid. +Axiom P : nat -> Prop. +Axiom P_or : forall x y, P (x + y) <-> P x \/ P y. +Lemma foo (H : P 3) : False. +eapply or_introl in H. +erewrite <- P_or in H. +(* Error: No such hypothesis: H *) diff --git a/test-suite/bugs/closed/4764.v b/test-suite/bugs/closed/4764.v new file mode 100644 index 000000000..e545cc1b7 --- /dev/null +++ b/test-suite/bugs/closed/4764.v @@ -0,0 +1,5 @@ +Notation prop_fun x y := (fun (x : Prop) => y). +Definition foo := fun (p : Prop) => p. +Definition bar := fun (_ : Prop) => O. +Print foo. +Print bar. diff --git a/test-suite/bugs/closed/4893.v b/test-suite/bugs/closed/4893.v new file mode 100644 index 000000000..9a35bcf95 --- /dev/null +++ b/test-suite/bugs/closed/4893.v @@ -0,0 +1,4 @@ +Goal True. +evar (P: Prop). +assert (H : P); [|subst P]; [exact I|]. +let T := type of H in not_evar T. diff --git a/test-suite/bugs/closed/5043.v b/test-suite/bugs/closed/5043.v new file mode 100644 index 000000000..4e6a0f878 --- /dev/null +++ b/test-suite/bugs/closed/5043.v @@ -0,0 +1,8 @@ +Unset Keep Admitted Variables. + +Section a. + Context (x : Type). + Definition foo : Type. + Admitted. +End a. +Check foo : Type. diff --git a/test-suite/csdp.cache b/test-suite/csdp.cache Binary files differdeleted file mode 100644 index 8e5708cf0..000000000 --- a/test-suite/csdp.cache +++ /dev/null diff --git a/test-suite/micromega/qexample.v b/test-suite/micromega/qexample.v index 47e6005b9..d001e8f7f 100644 --- a/test-suite/micromega/qexample.v +++ b/test-suite/micromega/qexample.v @@ -6,32 +6,29 @@ (* *) (************************************************************************) -Require Import Psatz. +Require Import Lqa. Require Import QArith. Lemma plus_minus : forall x y, 0 == x + y -> 0 == x -y -> 0 == x /\ 0 == y. Proof. intros. - psatzl Q. + lra. Qed. - - - (* Other (simple) examples *) Open Scope Q_scope. Lemma binomial : forall x y:Q, ((x+y)^2 == x^2 + (2 # 1) *x*y + y^2). Proof. intros. - psatzl Q. + lra. Qed. Lemma hol_light19 : forall m n, (2 # 1) * m + n == (n + m) + m. Proof. - intros ; psatzl Q. + intros ; lra. Qed. Open Scope Z_scope. Open Scope Q_scope. @@ -60,7 +57,11 @@ Lemma vcgen_25 : forall (( 1# 1) == (-2 # 1) * i + it). Proof. intros. - psatzl Q. + lra. +Qed. + +Goal forall x : Q, x * x >= 0. + intro; nra. Qed. Goal forall x, -x^2 >= 0 -> x - 1 >= 0 -> False. diff --git a/test-suite/micromega/rexample.v b/test-suite/micromega/rexample.v index 2eed7e951..89c08c770 100644 --- a/test-suite/micromega/rexample.v +++ b/test-suite/micromega/rexample.v @@ -6,7 +6,7 @@ (* *) (************************************************************************) -Require Import Psatz. +Require Import Lra. Require Import Reals. Open Scope R_scope. @@ -15,7 +15,7 @@ Lemma yplus_minus : forall x y, 0 = x + y -> 0 = x -y -> 0 = x /\ 0 = y. Proof. intros. - psatzl R. + lra. Qed. (* Other (simple) examples *) @@ -23,13 +23,13 @@ Qed. Lemma binomial : forall x y, ((x+y)^2 = x^2 + 2 *x*y + y^2). Proof. intros. - psatzl R. + lra. Qed. Lemma hol_light19 : forall m n, 2 * m + n = (n + m) + m. Proof. - intros ; psatzl R. + intros ; lra. Qed. @@ -57,7 +57,7 @@ Lemma vcgen_25 : forall (( 1 ) = (-2 ) * i + it). Proof. intros. - psatzl R. + lra. Qed. Goal forall x, -x^2 >= 0 -> x - 1 >= 0 -> False. @@ -72,5 +72,5 @@ Proof. Qed. Lemma l1 : forall x y z : R, Rabs (x - z) <= Rabs (x - y) + Rabs (y - z). -intros; split_Rabs; psatzl R. +intros; split_Rabs; lra. Qed.
\ No newline at end of file diff --git a/test-suite/micromega/zomicron.v b/test-suite/micromega/zomicron.v index 0ec1dbfbc..1f148becc 100644 --- a/test-suite/micromega/zomicron.v +++ b/test-suite/micromega/zomicron.v @@ -33,4 +33,13 @@ Lemma compact_proof : forall z, Proof. intros. lia. -Qed.
\ No newline at end of file +Qed. + +Lemma dummy_ex : exists (x:Z), x = x. +Proof. + eexists. + lia. + Unshelve. + exact Z0. +Qed. +
\ No newline at end of file diff --git a/test-suite/output/PatternsInBinders.v b/test-suite/output/PatternsInBinders.v index b5c91e347..fff86d6fa 100644 --- a/test-suite/output/PatternsInBinders.v +++ b/test-suite/output/PatternsInBinders.v @@ -1,3 +1,5 @@ +Require Coq.Unicode.Utf8. + (** The purpose of this file is to test printing of the destructive patterns used in binders ([fun] and [forall]). *) @@ -37,7 +39,7 @@ End WithParameters. (** Some test involving unicode notations. *) Module WithUnicode. - Require Import Coq.Unicode.Utf8. + Import Coq.Unicode.Utf8. Check λ '((x,y) : A*B), (y,x). Check ∀ '(x,y), swap (x,y) = (y,x). diff --git a/theories/Compat/Coq84.v b/theories/Compat/Coq84.v index 21b78b533..8ae1a9195 100644 --- a/theories/Compat/Coq84.v +++ b/theories/Compat/Coq84.v @@ -76,3 +76,7 @@ Require Coq.Lists.List. Require Coq.Vectors.VectorDef. Notation " [ x ; .. ; y ] " := (cons x .. (cons y nil) ..) : list_scope. Notation " [ x ; .. ; y ] " := (VectorDef.cons _ x _ .. (VectorDef.cons _ y _ (nil _)) ..) : vector_scope. + +(** In 8.4, the statement of admitted lemmas did not depend on the section + variables. *) +Unset Keep Admitted Variables. diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index 6dba2c51e..de3d14483 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -81,7 +81,6 @@ let open_file_twice_if verbosely longfname = let in_chan = open_utf8_file_in longfname in let verb_ch = if verbosely then Some (open_utf8_file_in longfname) else None in - CLexer.set_current_file longfname; let po = Pcoq.Gram.parsable (Stream.of_channel in_chan) in (in_chan, longfname, (po, verb_ch)) @@ -190,6 +189,8 @@ let rec vernac_com checknav (loc,com) = let fname = CUnix.make_suffix fname ".v" in let f = Loadpath.locate_file fname in let st = save_translator_coqdoc () in + let old_lexer_file = CLexer.get_current_file () in + CLexer.set_current_file f; if !Flags.beautify_file then begin chan_beautify := open_out (f^beautify_suffix); @@ -199,9 +200,11 @@ let rec vernac_com checknav (loc,com) = try Flags.silently (read_vernac_file verbosely) f; restore_translator_coqdoc st; + CLexer.set_current_file old_lexer_file; with reraise -> let reraise = CErrors.push reraise in restore_translator_coqdoc st; + CLexer.set_current_file old_lexer_file; iraise reraise end @@ -271,12 +274,16 @@ let (f_xml_end_library, xml_end_library) = Hook.make ~default:ignore () let load_vernac verb file = chan_beautify := if !Flags.beautify_file then open_out (file^beautify_suffix) else stdout; + let old_lexer_file = CLexer.get_current_file () in try + CLexer.set_current_file file; Flags.silently (read_vernac_file verb) file; if !Flags.beautify_file then close_out !chan_beautify; + CLexer.set_current_file old_lexer_file; with any -> let (e, info) = CErrors.push any in if !Flags.beautify_file then close_out !chan_beautify; + CLexer.set_current_file old_lexer_file; iraise (disable_drop e, info) let warn_file_no_extension = diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 40c7c7010..10bbdc358 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -122,9 +122,7 @@ let show_intro all = [Not_found] is raised if the given string isn't the qualid of a known inductive type. *) -let make_cases s = - let qualified_name = Libnames.qualid_of_string s in - let glob_ref = Nametab.locate qualified_name in +let make_cases_aux glob_ref = match glob_ref with | Globnames.IndRef i -> let {Declarations.mind_nparams = np} @@ -144,11 +142,16 @@ let make_cases s = carr tarr [] | _ -> raise Not_found +let make_cases s = + let qualified_name = Libnames.qualid_of_string s in + let glob_ref = Nametab.locate qualified_name in + make_cases_aux glob_ref + (** Textual display of a generic "match" template *) let show_match id = let patterns = - try make_cases (Id.to_string (snd id)) + try make_cases_aux (Nametab.global id) with Not_found -> error "Unknown inductive type." in let pr_branch l = |