diff options
45 files changed, 602 insertions, 357 deletions
diff --git a/API/API.mli b/API/API.mli index 3bd047043a..04c69b025f 100644 --- a/API/API.mli +++ b/API/API.mli @@ -4661,6 +4661,7 @@ sig val pf_ids_set_of_hyps : 'a Proofview.Goal.t -> Names.Id.Set.t val pf_concl : 'a Proofview.Goal.t -> EConstr.types val pf_get_new_id : Names.Id.t -> 'a Proofview.Goal.t -> Names.Id.t + val pf_get_hyp : Names.Id.t -> 'a Proofview.Goal.t -> EConstr.named_declaration val pf_get_hyp_typ : Names.Id.t -> 'a Proofview.Goal.t -> EConstr.types val pf_get_type_of : 'a Proofview.Goal.t -> EConstr.constr -> EConstr.types val pf_global : Names.Id.t -> 'a Proofview.Goal.t -> Globnames.global_reference @@ -5813,8 +5814,11 @@ end module Stm : sig + type doc type state - val state_of_id : + + val get_doc : Feedback.doc_id -> doc + val state_of_id : doc:doc -> Stateid.t -> [ `Valid of state option | `Expired | `Error of exn ] end @@ -14,6 +14,13 @@ Tactics utility. The command "Set NativeCompute Profiling" enables profiling, and "Set NativeCompute Profile Filename" customizes the profile filename. +- The tactic "omega" is now aware of the bodies of context variables + such as "x := 5 : Z" (see bug #148). This could be disabled via + Unset Omega UseLocalDefs. +- The tactic "omega" is now aware of the bodies of context variables + such as "x := 5 : Z" (see bug #148). This could be disabled via + Unset Omega UseLocalDefs. +- The tactic "romega" is also aware now of the bodies of context variables. Changes from 8.7+beta2 to 8.7.0 =============================== diff --git a/configure.ml b/configure.ml index ca7979fa1b..a7acdf5320 100644 --- a/configure.ml +++ b/configure.ml @@ -206,7 +206,7 @@ let get_date () = let year = 1900+now.Unix.tm_year in let month = months.(now.Unix.tm_mon) in sprintf "%s %d" month year, - sprintf "%s %d %d %d:%d:%d" (String.sub month 0 3) now.Unix.tm_mday year + sprintf "%s %d %d %d:%02d:%02d" (String.sub month 0 3) now.Unix.tm_mday year now.Unix.tm_hour now.Unix.tm_min now.Unix.tm_sec let short_date, full_date = get_date () diff --git a/dev/ci/ci-iris-coq.sh b/dev/ci/ci-iris-coq.sh index 2d127ddc1b..c49b6ed9c9 100755 --- a/dev/ci/ci-iris-coq.sh +++ b/dev/ci/ci-iris-coq.sh @@ -9,17 +9,19 @@ Iris_CI_DIR=${CI_BUILD_DIR}/iris-coq install_ssreflect -# Setup Iris first, as it is needed to compute the dependencies +# Add or update the opam repo we need for dependency resolution +opam repo add iris-dev https://gitlab.mpi-sws.org/FP/opam-dev.git -p 0 || opam update iris-dev +# Setup Iris first, extract required version of std++ git_checkout ${Iris_CI_BRANCH} ${Iris_CI_GITURL} ${Iris_CI_DIR} -read -a IRIS_DEP < ${Iris_CI_DIR}/opam.pins +stdpp_VERSION=$(cat ${Iris_CI_DIR}/opam | fgrep coq-stdpp | egrep 'dev\.([0-9.-]+)' -o) -# Setup stdpp -stdpp_CI_GITURL=${IRIS_DEP[1]}.git -stdpp_CI_COMMIT=${IRIS_DEP[2]} - -git_checkout ${stdpp_CI_BRANCH} ${stdpp_CI_GITURL} ${stdpp_CI_DIR} ${stdpp_CI_COMMIT} +# Ask opam where to get this std++, separating at the # +stdpp_URL=$(opam show coq-stdpp.$stdpp_VERSION -f upstream-url) +read -a stdpp_URL_PARTS <<< $(echo $stdpp_URL | tr '#' ' ') +# Setup std++ +git_checkout ${stdpp_CI_BRANCH} ${stdpp_URL_PARTS[0]} ${stdpp_CI_DIR} ${stdpp_URL_PARTS[1]} ( cd ${stdpp_CI_DIR} && make && make install ) # Build iris now diff --git a/doc/faq/FAQ.tex b/doc/faq/FAQ.tex index 213fb03137..541d39501b 100644 --- a/doc/faq/FAQ.tex +++ b/doc/faq/FAQ.tex @@ -2413,15 +2413,14 @@ You can use {\tt coq\_tex}. \Question{How can I cite the {\Coq} reference manual?} -You can use this bibtex entry: +You can use this bibtex entry (to adapt to the appropriate version): \begin{verbatim} -@Manual{Coq:manual, - title = {The Coq proof assistant reference manual}, - author = {\mbox{The Coq development team}}, - organization = {LogiCal Project}, - note = {Version 8.2}, - year = {2009}, - url = "http://coq.inria.fr" +@manual{Coq:manual, + author = {{Coq} {Development} {Team}, The}, + title = {The {Coq} Proof Assistant Reference Manual, version 8.7}, + month = Oct, + year = {2017}, + url = {http://coq.inria.fr} } \end{verbatim} diff --git a/ide/coqOps.ml b/ide/coqOps.ml index 0dd08293c8..ded28a998e 100644 --- a/ide/coqOps.ml +++ b/ide/coqOps.ml @@ -422,7 +422,7 @@ object(self) let rec eat_feedback n = if n = 0 then true else let msg = Queue.pop feedbacks in - let id = msg.id in + let id = msg.span_id in let sentence = let finder _ state_id s = match state_id, id with diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml index f00b1e1421..7cbab56d44 100644 --- a/ide/ide_slave.ml +++ b/ide/ide_slave.ml @@ -76,10 +76,16 @@ let ide_cmd_checks ~id (loc,ast) = (** Interpretation (cf. [Ide_intf.interp]) *) +let ide_doc = ref None +let get_doc () = Option.get !ide_doc +let set_doc doc = ide_doc := Some doc + let add ((s,eid),(sid,verbose)) = + let doc = get_doc () in let pa = Pcoq.Gram.parsable (Stream.of_string s) in - let loc_ast = Stm.parse_sentence sid pa in - let newid, rc = Stm.add ~ontop:sid verbose loc_ast in + let loc_ast = Stm.parse_sentence ~doc sid pa in + let doc, newid, rc = Stm.add ~doc ~ontop:sid verbose loc_ast in + set_doc doc; let rc = match rc with `NewTip -> CSig.Inl () | `Unfocus id -> CSig.Inr id in ide_cmd_checks ~id:newid loc_ast; (* TODO: the "" parameter is a leftover of the times the protocol @@ -94,9 +100,10 @@ let add ((s,eid),(sid,verbose)) = newid, (rc, "") let edit_at id = - match Stm.edit_at id with - | `NewTip -> CSig.Inl () - | `Focus { Stm.start; stop; tip} -> CSig.Inr (start, (stop, tip)) + let doc = get_doc () in + match Stm.edit_at ~doc id with + | doc, `NewTip -> set_doc doc; CSig.Inl () + | doc, `Focus { Stm.start; stop; tip} -> set_doc doc; CSig.Inr (start, (stop, tip)) (* TODO: the "" parameter is a leftover of the times the protocol * used to include stderr/stdout output. @@ -109,12 +116,14 @@ let edit_at id = *) let query (route, (s,id)) = let pa = Pcoq.Gram.parsable (Stream.of_string s) in - Stm.query ~at:id ~route pa + let doc = get_doc () in + Stm.query ~at:id ~doc ~route pa let annotate phrase = + let doc = get_doc () in let (loc, ast) = let pa = Pcoq.Gram.parsable (Stream.of_string phrase) in - Stm.parse_sentence (Stm.get_current_state ()) pa + Stm.parse_sentence ~doc (Stm.get_current_state ~doc) pa in (* XXX: Width should be a parameter of annotate... *) Richpp.richpp_of_pp 78 (Ppvernac.pr_vernac ast) @@ -196,7 +205,8 @@ let export_pre_goals pgs = } let goals () = - Stm.finish (); + let doc = get_doc () in + set_doc @@ Stm.finish ~doc; try let pfts = Proof_global.give_me_the_proof () in Some (export_pre_goals (Proof.map_structured_proof pfts process_goal)) @@ -204,7 +214,8 @@ let goals () = let evars () = try - Stm.finish (); + let doc = get_doc () in + set_doc @@ Stm.finish ~doc; let pfts = Proof_global.give_me_the_proof () in let { Evd.it = all_goals ; sigma = sigma } = Proof.V82.subgoals pfts in let exl = Evar.Map.bindings (Evd.undefined_map sigma) in @@ -230,12 +241,17 @@ let hints () = (** Other API calls *) +let wait () = + let doc = get_doc () in + set_doc (Stm.wait ~doc) + let status force = (** We remove the initial part of the current [DirPath.t] (usually Top in an interactive session, cf "coqtop -top"), and display the other parts (opened sections and modules) *) - Stm.finish (); - if force then Stm.join (); + set_doc (Stm.finish ~doc:(get_doc ())); + if force then + set_doc (Stm.join ~doc:(get_doc ())); let path = let l = Names.DirPath.repr (Lib.cwd ()) in List.rev_map Names.Id.to_string l @@ -252,7 +268,7 @@ let status force = Interface.status_path = path; Interface.status_proofname = proof; Interface.status_allproofs = allproofs; - Interface.status_proofnum = Stm.current_proof_depth (); + Interface.status_proofnum = Stm.current_proof_depth ~doc:(get_doc ()); } let export_coq_object t = { @@ -356,22 +372,23 @@ let init = fun file -> if !initialized then anomaly (str "Already initialized.") else begin - let init_sid = Stm.get_current_state () in + let init_sid = Stm.get_current_state ~doc:(get_doc ()) in initialized := true; match file with | None -> init_sid | Some file -> let dir = Filename.dirname file in let open Loadpath in let open CUnix in - let initial_id, _ = + let doc, initial_id, _ = + let doc = get_doc () in if not (is_in_load_paths (physical_path_of_string dir)) then begin let pa = Pcoq.Gram.parsable (Stream.of_string (Printf.sprintf "Add LoadPath \"%s\". " dir)) in - let loc_ast = Stm.parse_sentence init_sid pa in - Stm.add false ~ontop:init_sid loc_ast - end else init_sid, `NewTip in + let loc_ast = Stm.parse_sentence ~doc init_sid pa in + Stm.add false ~doc ~ontop:init_sid loc_ast + end else doc, init_sid, `NewTip in if Filename.check_suffix file ".v" then Stm.set_compilation_hints file; - Stm.finish (); + set_doc (Stm.finish ~doc); initial_id end @@ -413,7 +430,7 @@ let eval_call c = Interface.quit = (fun () -> quit := true); Interface.init = interruptible init; Interface.about = interruptible about; - Interface.wait = interruptible Stm.wait; + Interface.wait = interruptible wait; Interface.interp = interruptible interp; Interface.handle_exn = handle_exn; Interface.stop_worker = Stm.stop_worker; @@ -449,7 +466,8 @@ let msg_format = ref (fun () -> Xmlprotocol.Richpp margin ) -let loop () = +let loop doc = + set_doc doc; init_signal_handler (); catch_break := false; let in_ch, out_ch = Spawned.get_channels () in diff --git a/ide/xmlprotocol.ml b/ide/xmlprotocol.ml index b452b0a13f..aaa24a2a95 100644 --- a/ide/xmlprotocol.ml +++ b/ide/xmlprotocol.ml @@ -939,7 +939,7 @@ let of_edit_or_state_id id = ["object","state"], of_stateid id let of_feedback msg = let content = of_feedback_content msg.contents in - let obj, id = of_edit_or_state_id msg.id in + let obj, id = of_edit_or_state_id msg.span_id in let route = string_of_int msg.route in Element ("feedback", obj @ ["route",route], [id;content]) @@ -947,8 +947,9 @@ let of_feedback msg_fmt = msg_format := msg_fmt; of_feedback let to_feedback xml = match xml with - | Element ("feedback", ["object","state";"route",route], [id;content]) -> { - id = to_stateid id; + | Element ("feedback", ["object","state";"route",route], [id;content]) -> { + doc_id = 0; + span_id = to_stateid id; route = int_of_string route; contents = to_feedback_content content } | x -> raise (Marshal_error("feedback",x)) diff --git a/vernac/discharge.ml b/interp/discharge.ml index 0e4bbd2993..0e4bbd2993 100644 --- a/vernac/discharge.ml +++ b/interp/discharge.ml diff --git a/vernac/discharge.mli b/interp/discharge.mli index c8c7e3b8b8..c8c7e3b8b8 100644 --- a/vernac/discharge.mli +++ b/interp/discharge.mli diff --git a/lib/feedback.ml b/lib/feedback.ml index 54d16a9be3..7a126363cc 100644 --- a/lib/feedback.ml +++ b/lib/feedback.ml @@ -15,6 +15,7 @@ type level = | Warning | Error +type doc_id = int type route_id = int type feedback_content = @@ -35,7 +36,8 @@ type feedback_content = | Message of level * Loc.t option * Pp.t type feedback = { - id : Stateid.t; + doc_id : doc_id; (* The document being concerned *) + span_id : Stateid.t; route : route_id; contents : feedback_content; } @@ -52,23 +54,27 @@ let add_feeder = let del_feeder fid = Hashtbl.remove feeders fid let default_route = 0 -let feedback_id = ref Stateid.dummy +let span_id = ref Stateid.dummy +let doc_id = ref 0 let feedback_route = ref default_route -let set_id_for_feedback ?(route=default_route) i = - feedback_id := i; feedback_route := route +let set_id_for_feedback ?(route=default_route) d i = + doc_id := d; + span_id := i; + feedback_route := route -let feedback ?id ?route what = +let feedback ?did ?id ?route what = let m = { contents = what; - route = Option.default !feedback_route route; - id = Option.default !feedback_id id; + route = Option.default !feedback_route route; + doc_id = Option.default !doc_id did; + span_id = Option.default !span_id id; } in Hashtbl.iter (fun _ f -> f m) feeders (* Logging messages *) let feedback_logger ?loc lvl msg = - feedback ~route:!feedback_route ~id:!feedback_id (Message (lvl, loc, msg)) + feedback ~route:!feedback_route ~id:!span_id (Message (lvl, loc, msg)) let msg_info ?loc x = feedback_logger ?loc Info x let msg_notice ?loc x = feedback_logger ?loc Notice x diff --git a/lib/feedback.mli b/lib/feedback.mli index 45a02d384a..73b84614f1 100644 --- a/lib/feedback.mli +++ b/lib/feedback.mli @@ -17,6 +17,9 @@ type level = | Error +(** Document unique identifier for serialization *) +type doc_id = int + (** Coq "semantic" infos obtained during execution *) type route_id = int @@ -43,7 +46,8 @@ type feedback_content = | Message of level * Loc.t option * Pp.t type feedback = { - id : Stateid.t; (* The document part concerned *) + doc_id : doc_id; (* The document being concerned *) + span_id : Stateid.t; (* The document part concerned *) route : route_id; (* Extra routing info *) contents : feedback_content; (* The payload *) } @@ -60,13 +64,13 @@ val add_feeder : (feedback -> unit) -> int (** [del_feeder fid] removes the feeder with id [fid] *) val del_feeder : int -> unit -(** [feedback ?id ?route fb] produces feedback fb, with [route] and - [id] set appropiatedly, if absent, it will use the defaults set by - [set_id_for_feedback] *) -val feedback : ?id:Stateid.t -> ?route:route_id -> feedback_content -> unit +(** [feedback ?did ?sid ?route fb] produces feedback [fb], with + [route] and [did, sid] set appropiatedly, if absent, it will use + the defaults set by [set_id_for_feedback] *) +val feedback : ?did:doc_id -> ?id:Stateid.t -> ?route:route_id -> feedback_content -> unit (** [set_id_for_feedback route id] Set the defaults for feedback *) -val set_id_for_feedback : ?route:route_id -> Stateid.t -> unit +val set_id_for_feedback : ?route:route_id -> doc_id -> Stateid.t -> unit (** {6 output functions} diff --git a/plugins/ltac/profile_ltac.ml b/plugins/ltac/profile_ltac.ml index 32494a8793..9ae8bfe65b 100644 --- a/plugins/ltac/profile_ltac.ml +++ b/plugins/ltac/profile_ltac.ml @@ -367,18 +367,30 @@ let do_profile s call_trace tac = let get_local_profiling_results () = List.hd Local.(!stack) -module SM = Map.Make(Stateid.Self) +(* We maintain our own cache of document data, given that the + semantics of the STM implies that synchronized state for opaque + proofs will be lost on QED. This provides some complications later + on as we will have to simulate going back on the document on our + own. *) +module DData = struct + type t = Feedback.doc_id * Stateid.t + let compare x y = Pervasives.compare x y +end + +module SM = Map.Make(DData) let data = ref SM.empty let _ = Feedback.(add_feeder (function - | { id = s; contents = Custom (_, "ltacprof_results", xml) } -> + | { doc_id = d; + span_id = s; + contents = Custom (_, "ltacprof_results", xml) } -> let results = to_ltacprof_results xml in let other_results = (* Multi success can cause this *) - try SM.find s !data + try SM.find (d,s) !data with Not_found -> empty_treenode root in - data := SM.add s (merge_roots results other_results) !data + data := SM.add (d,s) (merge_roots results other_results) !data | _ -> ())) let reset_profile () = @@ -388,7 +400,10 @@ let reset_profile () = (* ******************** *) let print_results_filter ~cutoff ~filter = - let valid id _ = Stm.state_of_id id <> `Expired in + (* The STM doesn't provide yet a proper document query and traversal + API, thus we need to re-check if some states are current anymore + (due to backtracking) using the `state_of_id` API. *) + let valid (did,id) _ = Stm.(state_of_id ~doc:(get_doc did) id) <> `Expired in data := SM.filter valid !data; let results = SM.fold (fun _ -> merge_roots ~disjoint:true) !data (empty_treenode root) in diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index fd791a9101..1809f0fcdb 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -1935,7 +1935,12 @@ let default_morphism sign m = let evars, mor = resolve_one_typeclass env (goalevars evars) morph in mor, proper_projection sigma mor morph +let warn_add_setoid_deprecated = + CWarnings.create ~name:"add-setoid" ~category:"deprecated" (fun () -> + Pp.(str "Add Setoid is deprecated, please use Add Parametric Relation.")) + let add_setoid global binders a aeq t n = + warn_add_setoid_deprecated ?loc:a.CAst.loc (); init_setoid (); let _lemma_refl = declare_instance_refl global binders a aeq n (mkappc "Seq_refl" [a;aeq;t]) in let _lemma_sym = declare_instance_sym global binders a aeq n (mkappc "Seq_sym" [a;aeq;t]) in @@ -1954,7 +1959,12 @@ let make_tactic name = let tacname = Qualid (Loc.tag tacpath) in TacArg (Loc.tag @@ TacCall (Loc.tag (tacname, []))) +let warn_add_morphism_deprecated = + CWarnings.create ~name:"add-morphism" ~category:"deprecated" (fun () -> + Pp.(str "Add Morphism f : id is deprecated, please use Add Morphism f with signature (...) as id")) + let add_morphism_infer glob m n = + warn_add_morphism_deprecated ?loc:m.CAst.loc (); init_setoid (); let poly = Flags.is_universe_polymorphism () in let instance_id = add_suffix n "_Proper" in diff --git a/plugins/micromega/EnvRing.v b/plugins/micromega/EnvRing.v index 56b3d480eb..ae4857a77c 100644 --- a/plugins/micromega/EnvRing.v +++ b/plugins/micromega/EnvRing.v @@ -56,10 +56,18 @@ Section MakeRingPol. Infix "?=!" := ceqb. Notation "[ x ]" := (phi x). (* Useful tactics *) - Add Morphism radd : radd_ext. exact (Radd_ext Reqe). Qed. - Add Morphism rmul : rmul_ext. exact (Rmul_ext Reqe). Qed. - Add Morphism ropp : ropp_ext. exact (Ropp_ext Reqe). Qed. - Add Morphism rsub : rsub_ext. exact (ARsub_ext Rsth Reqe ARth). Qed. + Add Morphism radd with signature (req ==> req ==> req) as radd_ext. + Proof. exact (Radd_ext Reqe). Qed. + + Add Morphism rmul with signature (req ==> req ==> req) as rmul_ext. + Proof. exact (Rmul_ext Reqe). Qed. + + Add Morphism ropp with signature (req ==> req) as ropp_ext. + Proof. exact (Ropp_ext Reqe). Qed. + + Add Morphism rsub with signature (req ==> req ==> req) as rsub_ext. + Proof. exact (ARsub_ext Rsth Reqe ARth). Qed. + Ltac rsimpl := gen_srewrite Rsth Reqe ARth. Ltac add_push := gen_add_push radd Rsth Reqe ARth. diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml index ae1a563bee..ff69ddefb8 100644 --- a/plugins/omega/coq_omega.ml +++ b/plugins/omega/coq_omega.ml @@ -50,6 +50,7 @@ let display_time_flag = ref false let display_system_flag = ref false let display_action_flag = ref false let old_style_flag = ref false +let letin_flag = ref true (* Should we reset all variable labels between two runs of omega ? *) @@ -100,6 +101,14 @@ let _ = optread = read reset_flag; optwrite = write reset_flag } +let _ = + declare_bool_option + { optdepr = false; + optname = "Omega takes advantage of context variables with body"; + optkey = ["Omega";"UseLocalDefs"]; + optread = read letin_flag; + optwrite = write letin_flag } + let intref, reset_all_references = let refs = ref [] in (fun n -> let r = ref n in refs := (r,n) :: !refs; r), @@ -376,16 +385,15 @@ let mk_var v = mkVar (Id.of_string v) let mk_plus t1 t2 = mkApp (Lazy.force coq_Zplus, [| t1; t2 |]) let mk_times t1 t2 = mkApp (Lazy.force coq_Zmult, [| t1; t2 |]) let mk_minus t1 t2 = mkApp (Lazy.force coq_Zminus, [| t1;t2 |]) -let mk_eq t1 t2 = mkApp (Lazy.force coq_eq, - [| Lazy.force coq_Z; t1; t2 |]) +let mk_gen_eq ty t1 t2 = mkApp (Lazy.force coq_eq, [| ty; t1; t2 |]) +let mk_eq t1 t2 = mk_gen_eq (Lazy.force coq_Z) t1 t2 let mk_le t1 t2 = mkApp (Lazy.force coq_Zle, [| t1; t2 |]) let mk_gt t1 t2 = mkApp (Lazy.force coq_Zgt, [| t1; t2 |]) let mk_inv t = mkApp (Lazy.force coq_Zopp, [| t |]) let mk_and t1 t2 = mkApp (Lazy.force coq_and, [| t1; t2 |]) let mk_or t1 t2 = mkApp (Lazy.force coq_or, [| t1; t2 |]) let mk_not t = mkApp (Lazy.force coq_not, [| t |]) -let mk_eq_rel t1 t2 = mkApp (Lazy.force coq_eq, - [| Lazy.force coq_comparison; t1; t2 |]) +let mk_eq_rel t1 t2 = mk_gen_eq (Lazy.force coq_comparison) t1 t2 let mk_inj t = mkApp (Lazy.force coq_Z_of_nat, [| t |]) let mk_integer n = @@ -1778,11 +1786,25 @@ let destructure_hyps = let type_of = Tacmach.New.pf_unsafe_type_of gl in let decidability = decidability gl in let pf_nf = pf_nf gl in - let rec loop = function - | [] -> (tclTHEN nat_inject coq_omega) - | decl::lit -> - let i = NamedDecl.get_id decl in - Proofview.tclEVARMAP >>= fun sigma -> + let rec loop = function + | [] -> (tclTHEN nat_inject coq_omega) + | LocalDef (i,body,typ) :: lit when !letin_flag -> + Proofview.tclEVARMAP >>= fun sigma -> + begin + try + match destructurate_type sigma (pf_nf typ) with + | Kapp(Nat,_) | Kapp(Z,_) -> + let hid = fresh_id Id.Set.empty (add_suffix i "_eqn") gl in + let hty = mk_gen_eq typ (mkVar i) body in + tclTHEN + (assert_by (Name hid) hty reflexivity) + (loop (LocalAssum (hid, hty) :: lit)) + | _ -> loop lit + with e when catchable_exception e -> loop lit + end + | decl :: lit -> (* variable without body (or !letin_flag isn't set) *) + let i = NamedDecl.get_id decl in + Proofview.tclEVARMAP >>= fun sigma -> begin try match destructurate_prop sigma (NamedDecl.get_type decl) with | Kapp(False,[]) -> elim_id i | Kapp((Zle|Zge|Zgt|Zlt|Zne),[t1;t2]) -> loop lit diff --git a/plugins/romega/const_omega.ml b/plugins/romega/const_omega.ml index 4ffbd5aa8b..c27ac2ea44 100644 --- a/plugins/romega/const_omega.ml +++ b/plugins/romega/const_omega.ml @@ -221,6 +221,7 @@ let mk_N = function module type Int = sig val typ : Term.constr Lazy.t + val is_int_typ : [ `NF ] Proofview.Goal.t -> Term.constr -> bool val plus : Term.constr Lazy.t val mult : Term.constr Lazy.t val opp : Term.constr Lazy.t @@ -287,12 +288,14 @@ let pf_nf gl c = EConstr.Unsafe.to_constr (Tacmach.New.pf_apply Tacred.simpl gl (EConstr.of_constr c)) +let is_int_typ gl t = + match destructurate (pf_nf gl t) with + | Kapp("Z",[]) -> true + | _ -> false + let parse_rel gl t = match destructurate t with - | Kapp("eq",[typ;t1;t2]) -> - (match destructurate (pf_nf gl typ) with - | Kapp("Z",[]) -> Req (t1,t2) - | _ -> Rother) + | Kapp("eq",[typ;t1;t2]) when is_int_typ gl typ -> Req (t1,t2) | Kapp("Zne",[t1;t2]) -> Rne (t1,t2) | Kapp("Z.le",[t1;t2]) -> Rle (t1,t2) | Kapp("Z.lt",[t1;t2]) -> Rlt (t1,t2) diff --git a/plugins/romega/const_omega.mli b/plugins/romega/const_omega.mli index a452b1a917..80e00e4e14 100644 --- a/plugins/romega/const_omega.mli +++ b/plugins/romega/const_omega.mli @@ -103,6 +103,8 @@ module type Int = sig (* the coq type of the numbers *) val typ : Term.constr Lazy.t + (* Is a constr expands to the type of these numbers *) + val is_int_typ : [ `NF ] Proofview.Goal.t -> Term.constr -> bool (* the operations on the numbers *) val plus : Term.constr Lazy.t val mult : Term.constr Lazy.t diff --git a/plugins/romega/refl_omega.ml b/plugins/romega/refl_omega.ml index 517df41d93..661485aeeb 100644 --- a/plugins/romega/refl_omega.ml +++ b/plugins/romega/refl_omega.ml @@ -547,22 +547,33 @@ let display_gl env t_concl t_lhyps = Printf.printf "REIFED PROBLEM\n\n"; Printf.printf " CONCL: %a\n" pprint t_concl; List.iter - (fun (i,t) -> Printf.printf " %s: %a\n" (Id.to_string i) pprint t) + (fun (i,_,t) -> Printf.printf " %s: %a\n" (Id.to_string i) pprint t) t_lhyps; print_env_reification env +type defined = Defined | Assumed + +let reify_hyp env gl i = + let open Context.Named.Declaration in + let ctxt = (false,[],i,[]) in + match Tacmach.New.pf_get_hyp i gl with + | LocalDef (_,d,t) when Z.is_int_typ gl (EConstr.Unsafe.to_constr t) -> + let d = EConstr.Unsafe.to_constr d in + let dummy = Lazy.force coq_True in + let p = mk_equation env ctxt dummy Eq (Term.mkVar i) d in + i,Defined,p + | LocalDef (_,_,t) | LocalAssum (_,t) -> + let t = EConstr.Unsafe.to_constr t in + let p = oproposition_of_constr env ctxt gl t in + i,Assumed,p + let reify_gl env gl = let concl = Tacmach.New.pf_concl gl in let concl = EConstr.Unsafe.to_constr concl in - let hyps = Tacmach.New.pf_hyps_types gl in - let hyps = List.map (fun (i,t) -> (i,EConstr.Unsafe.to_constr t)) hyps in - let t_concl = - oproposition_of_constr env (true,[],id_concl,[O_mono]) gl concl in - let t_lhyps = - List.map - (fun (i,t) -> i,oproposition_of_constr env (false,[],i,[]) gl t) - hyps - in + let hyps = Tacmach.New.pf_ids_of_hyps gl in + let ctxt_concl = (true,[],id_concl,[O_mono]) in + let t_concl = oproposition_of_constr env ctxt_concl gl concl in + let t_lhyps = List.map (reify_hyp env gl) hyps in let () = if !debug then display_gl env t_concl t_lhyps in t_concl, t_lhyps @@ -602,7 +613,7 @@ and destruct_neg_hyp eqns = function let rec destructurate_hyps = function | [] -> [[]] - | (i,t) :: l -> + | (i,_,t) :: l -> let l_syst1 = destruct_pos_hyp [] t in let l_syst2 = destructurate_hyps l in List.cartesian (@) l_syst1 l_syst2 @@ -673,6 +684,9 @@ let rec stated_in_tree = function | Tree(_,t1,t2) -> StateSet.union (stated_in_tree t1) (stated_in_tree t2) | Leaf s -> stated_in_trace s.s_trace +let mk_refl t = + EConstr.of_constr (app coq_refl_equal [|Lazy.force Z.typ; t|]) + let digest_stated_equations env tree = let do_equation st (vars,gens,eqns,ids) = (** We turn the definition of [v] @@ -684,9 +698,7 @@ let digest_stated_equations env tree = (** We then update the environment *) set_reified_atom st.st_var coq_v env; (** The term we'll introduce *) - let term_to_generalize = - EConstr.of_constr (app coq_refl_equal [|Lazy.force Z.typ; coq_v|]) - in + let term_to_generalize = mk_refl coq_v in (** Its representation as equation (but not reified yet, we lack the proper env to do that). *) let term_to_reify = (v_def,Oatom st.st_var) in @@ -954,18 +966,19 @@ let resolution unsafe env (reified_concl,reified_hyps) systems_list = display_solution_tree stdout solution_tree; print_newline() end; - (** Collect all hypotheses used in the solution tree *) + (** Collect all hypotheses and variables used in the solution tree *) let useful_equa_ids = equas_of_solution_tree solution_tree in - let equations = List.map (get_equation env) (IntSet.elements useful_equa_ids) - in - let hyps_of_eqns = - List.fold_left (fun s e -> Id.Set.add e.e_origin.o_hyp s) Id.Set.empty in - let hyps = hyps_of_eqns equations in - let useful_hypnames = Id.Set.elements (Id.Set.remove id_concl hyps) in - let useful_hyptypes = - List.map (fun id -> List.assoc_f Id.equal id reified_hyps) useful_hypnames + let useful_hypnames, useful_vars = + IntSet.fold + (fun i (hyps,vars) -> + let e = get_equation env i in + Id.Set.add e.e_origin.o_hyp hyps, + vars_of_equations [e] @@ vars) + useful_equa_ids + (Id.Set.empty, vars_of_prop reified_concl) in - let useful_vars = vars_of_equations equations @@ vars_of_prop reified_concl + let useful_hypnames = + Id.Set.elements (Id.Set.remove id_concl useful_hypnames) in (** Parts coming from equations introduced by omega: *) @@ -996,9 +1009,17 @@ let resolution unsafe env (reified_concl,reified_hyps) systems_list = let reified_concl = reified_of_proposition env reified_concl in let l_reified_terms = List.map - (fun p -> reified_of_proposition env (maximize_prop useful_equa_ids p)) - useful_hyptypes + (fun id -> + match Id.Map.find id reified_hyps with + | Defined,p -> + reified_of_proposition env p, mk_refl (Term.mkVar id) + | Assumed,p -> + reified_of_proposition env (maximize_prop useful_equa_ids p), + EConstr.mkVar id + | exception Not_found -> assert false) + useful_hypnames in + let l_reified_terms, l_reified_hypnames = List.split l_reified_terms in let env_props_reified = mk_plist env.props in let reified_goal = mk_list (Lazy.force coq_proposition) @@ -1007,14 +1028,14 @@ let resolution unsafe env (reified_concl,reified_hyps) systems_list = app coq_interp_sequent [| reified_concl;env_props_reified;reduced_term_env;reified_goal|] in + let mk_occ id = {o_hyp=id;o_path=[]} in let initial_context = - List.map (fun id -> CCHyp{o_hyp=id;o_path=[]}) useful_hypnames in + List.map (fun id -> CCHyp (mk_occ id)) useful_hypnames in let context = - CCHyp{o_hyp=id_concl;o_path=[]} :: hyp_stated_vars @ initial_context in + CCHyp (mk_occ id_concl) :: hyp_stated_vars @ initial_context in let decompose_tactic = decompose_tree env context solution_tree in - Tactics.generalize - (l_generalize_arg @ List.map EConstr.mkVar useful_hypnames) >> + Tactics.generalize (l_generalize_arg @ l_reified_hypnames) >> Tactics.convert_concl_no_check (EConstr.of_constr reified) Term.DEFAULTcast >> Tactics.apply (EConstr.of_constr (app coq_do_omega [|decompose_tactic|])) >> show_goal >> @@ -1034,13 +1055,16 @@ let total_reflexive_omega_tactic unsafe = rst_omega_var (); try let env = new_environment () in - let (concl,hyps) as reified_goal = reify_gl env gl in + let (concl,hyps) = reify_gl env gl in (* Register all atom indexes created during reification as omega vars *) set_omega_maxvar (pred (List.length env.terms)); - let full_reified_goal = (id_concl,Pnot concl) :: hyps in + let full_reified_goal = (id_concl,Assumed,Pnot concl) :: hyps in let systems_list = destructurate_hyps full_reified_goal in + let hyps = + List.fold_left (fun s (id,d,p) -> Id.Map.add id (d,p) s) Id.Map.empty hyps + in if !debug then display_systems systems_list; - resolution unsafe env reified_goal systems_list + resolution unsafe env (concl,hyps) systems_list with NO_CONTRADICTION -> CErrors.user_err Pp.(str "ROmega can't solve this system") end diff --git a/plugins/setoid_ring/Field_theory.v b/plugins/setoid_ring/Field_theory.v index 56b985aa34..88e2cb1da5 100644 --- a/plugins/setoid_ring/Field_theory.v +++ b/plugins/setoid_ring/Field_theory.v @@ -56,11 +56,16 @@ Let rI_neq_rO := AFth.(AF_1_neq_0). Let rdiv_def := AFth.(AFdiv_def). Let rinv_l := AFth.(AFinv_l). -Add Morphism radd : radd_ext. Proof. exact (Radd_ext Reqe). Qed. -Add Morphism rmul : rmul_ext. Proof. exact (Rmul_ext Reqe). Qed. -Add Morphism ropp : ropp_ext. Proof. exact (Ropp_ext Reqe). Qed. -Add Morphism rsub : rsub_ext. Proof. exact (ARsub_ext Rsth Reqe ARth). Qed. -Add Morphism rinv : rinv_ext. Proof. exact SRinv_ext. Qed. +Add Morphism radd with signature (req ==> req ==> req) as radd_ext. +Proof. exact (Radd_ext Reqe). Qed. +Add Morphism rmul with signature (req ==> req ==> req) as rmul_ext. +Proof. exact (Rmul_ext Reqe). Qed. +Add Morphism ropp with signature (req ==> req) as ropp_ext. +Proof. exact (Ropp_ext Reqe). Qed. +Add Morphism rsub with signature (req ==> req ==> req) as rsub_ext. +Proof. exact (ARsub_ext Rsth Reqe ARth). Qed. +Add Morphism rinv with signature (req ==> req) as rinv_ext. +Proof. exact SRinv_ext. Qed. Let eq_trans := Setoid.Seq_trans _ _ Rsth. Let eq_sym := Setoid.Seq_sym _ _ Rsth. @@ -1609,9 +1614,12 @@ Section Complete. Variable Rsth : Setoid_Theory R req. Add Setoid R req Rsth as R_setoid3. Variable Reqe : ring_eq_ext radd rmul ropp req. - Add Morphism radd : radd_ext3. exact (Radd_ext Reqe). Qed. - Add Morphism rmul : rmul_ext3. exact (Rmul_ext Reqe). Qed. - Add Morphism ropp : ropp_ext3. exact (Ropp_ext Reqe). Qed. + Add Morphism radd with signature (req ==> req ==> req) as radd_ext3. + Proof. exact (Radd_ext Reqe). Qed. + Add Morphism rmul with signature (req ==> req ==> req) as rmul_ext3. + Proof. exact (Rmul_ext Reqe). Qed. + Add Morphism ropp with signature (req ==> req) as ropp_ext3. + Proof. exact (Ropp_ext Reqe). Qed. Section AlmostField. diff --git a/plugins/setoid_ring/InitialRing.v b/plugins/setoid_ring/InitialRing.v index 98ffff4322..bd4e94687d 100644 --- a/plugins/setoid_ring/InitialRing.v +++ b/plugins/setoid_ring/InitialRing.v @@ -51,9 +51,12 @@ Section ZMORPHISM. Add Setoid R req Rsth as R_setoid3. Ltac rrefl := gen_reflexivity Rsth. Variable Reqe : ring_eq_ext radd rmul ropp req. - Add Morphism radd : radd_ext3. exact (Radd_ext Reqe). Qed. - Add Morphism rmul : rmul_ext3. exact (Rmul_ext Reqe). Qed. - Add Morphism ropp : ropp_ext3. exact (Ropp_ext Reqe). Qed. + Add Morphism radd with signature (req ==> req ==> req) as radd_ext3. + Proof. exact (Radd_ext Reqe). Qed. + Add Morphism rmul with signature (req ==> req ==> req) as rmul_ext3. + Proof. exact (Rmul_ext Reqe). Qed. + Add Morphism ropp with signature (req ==> req) as ropp_ext3. + Proof. exact (Ropp_ext Reqe). Qed. Fixpoint gen_phiPOS1 (p:positive) : R := match p with @@ -103,7 +106,8 @@ Section ZMORPHISM. Section ALMOST_RING. Variable ARth : almost_ring_theory 0 1 radd rmul rsub ropp req. - Add Morphism rsub : rsub_ext3. exact (ARsub_ext Rsth Reqe ARth). Qed. + Add Morphism rsub with signature (req ==> req ==> req) as rsub_ext3. + Proof. exact (ARsub_ext Rsth Reqe ARth). Qed. Ltac norm := gen_srewrite Rsth Reqe ARth. Ltac add_push := gen_add_push radd Rsth Reqe ARth. @@ -151,7 +155,8 @@ Section ZMORPHISM. Variable Rth : ring_theory 0 1 radd rmul rsub ropp req. Let ARth := Rth_ARth Rsth Reqe Rth. - Add Morphism rsub : rsub_ext4. exact (ARsub_ext Rsth Reqe ARth). Qed. + Add Morphism rsub with signature (req ==> req ==> req) as rsub_ext4. + Proof. exact (ARsub_ext Rsth Reqe ARth). Qed. Ltac norm := gen_srewrite Rsth Reqe ARth. Ltac add_push := gen_add_push radd Rsth Reqe ARth. @@ -265,8 +270,10 @@ Section NMORPHISM. Let rsub := (@SRsub R radd). Notation "x - y " := (rsub x y). Notation "- x" := (ropp x). Notation "x == y" := (req x y). - Add Morphism radd : radd_ext4. exact (Radd_ext Reqe). Qed. - Add Morphism rmul : rmul_ext4. exact (Rmul_ext Reqe). Qed. + Add Morphism radd with signature (req ==> req ==> req) as radd_ext4. + Proof. exact (Radd_ext Reqe). Qed. + Add Morphism rmul with signature (req ==> req ==> req) as rmul_ext4. + Proof. exact (Rmul_ext Reqe). Qed. Ltac norm := gen_srewrite_sr Rsth Reqe ARth. Definition gen_phiN1 x := @@ -377,12 +384,16 @@ Section NWORDMORPHISM. Add Setoid R req Rsth as R_setoid5. Ltac rrefl := gen_reflexivity Rsth. Variable Reqe : ring_eq_ext radd rmul ropp req. - Add Morphism radd : radd_ext5. exact (Radd_ext Reqe). Qed. - Add Morphism rmul : rmul_ext5. exact (Rmul_ext Reqe). Qed. - Add Morphism ropp : ropp_ext5. exact (Ropp_ext Reqe). Qed. + Add Morphism radd with signature (req ==> req ==> req) as radd_ext5. + Proof. exact (Radd_ext Reqe). Qed. + Add Morphism rmul with signature (req ==> req ==> req) as rmul_ext5. + Proof. exact (Rmul_ext Reqe). Qed. + Add Morphism ropp with signature (req ==> req) as ropp_ext5. + Proof. exact (Ropp_ext Reqe). Qed. Variable ARth : almost_ring_theory 0 1 radd rmul rsub ropp req. - Add Morphism rsub : rsub_ext7. exact (ARsub_ext Rsth Reqe ARth). Qed. + Add Morphism rsub with signature (req ==> req ==> req) as rsub_ext7. + Proof. exact (ARsub_ext Rsth Reqe ARth). Qed. Ltac norm := gen_srewrite Rsth Reqe ARth. Ltac add_push := gen_add_push radd Rsth Reqe ARth. @@ -557,10 +568,14 @@ Section GEN_DIV. (* Useful tactics *) Add Setoid R req Rsth as R_set1. Ltac rrefl := gen_reflexivity Rsth. - Add Morphism radd : radd_ext. exact (Radd_ext Reqe). Qed. - Add Morphism rmul : rmul_ext. exact (Rmul_ext Reqe). Qed. - Add Morphism ropp : ropp_ext. exact (Ropp_ext Reqe). Qed. - Add Morphism rsub : rsub_ext. exact (ARsub_ext Rsth Reqe ARth). Qed. + Add Morphism radd with signature (req ==> req ==> req) as radd_ext. + Proof. exact (Radd_ext Reqe). Qed. + Add Morphism rmul with signature (req ==> req ==> req) as rmul_ext. + Proof. exact (Rmul_ext Reqe). Qed. + Add Morphism ropp with signature (req ==> req) as ropp_ext. + Proof. exact (Ropp_ext Reqe). Qed. + Add Morphism rsub with signature (req ==> req ==> req) as rsub_ext. + Proof. exact (ARsub_ext Rsth Reqe ARth). Qed. Ltac rsimpl := gen_srewrite Rsth Reqe ARth. Definition triv_div x y := @@ -859,8 +874,3 @@ Ltac isZcst t := (* *) | _ => constr:(false) end. - - - - - diff --git a/plugins/setoid_ring/Ring_polynom.v b/plugins/setoid_ring/Ring_polynom.v index ac54d862c9..a94f8d8df6 100644 --- a/plugins/setoid_ring/Ring_polynom.v +++ b/plugins/setoid_ring/Ring_polynom.v @@ -59,10 +59,18 @@ Section MakeRingPol. Infix "?=!" := ceqb. Notation "[ x ]" := (phi x). (* Useful tactics *) - Add Morphism radd : radd_ext. exact (Radd_ext Reqe). Qed. - Add Morphism rmul : rmul_ext. exact (Rmul_ext Reqe). Qed. - Add Morphism ropp : ropp_ext. exact (Ropp_ext Reqe). Qed. - Add Morphism rsub : rsub_ext. exact (ARsub_ext Rsth Reqe ARth). Qed. + Add Morphism radd with signature (req ==> req ==> req) as radd_ext. + Proof. exact (Radd_ext Reqe). Qed. + + Add Morphism rmul with signature (req ==> req ==> req) as rmul_ext. + Proof. exact (Rmul_ext Reqe). Qed. + + Add Morphism ropp with signature (req ==> req) as ropp_ext. + Proof. exact (Ropp_ext Reqe). Qed. + + Add Morphism rsub with signature (req ==> req ==> req) as rsub_ext. + Proof. exact (ARsub_ext Rsth Reqe ARth). Qed. + Ltac rsimpl := gen_srewrite Rsth Reqe ARth. Ltac add_push := gen_add_push radd Rsth Reqe ARth. diff --git a/plugins/setoid_ring/Ring_theory.v b/plugins/setoid_ring/Ring_theory.v index 8dda5ecd34..335a68d70f 100644 --- a/plugins/setoid_ring/Ring_theory.v +++ b/plugins/setoid_ring/Ring_theory.v @@ -254,8 +254,12 @@ Section ALMOST_RING. Section SEMI_RING. Variable SReqe : sring_eq_ext radd rmul req. - Add Morphism radd : radd_ext1. exact (SRadd_ext SReqe). Qed. - Add Morphism rmul : rmul_ext1. exact (SRmul_ext SReqe). Qed. + Add Morphism radd with signature (req ==> req ==> req) as radd_ext1. + Proof. exact (SRadd_ext SReqe). Qed. + + Add Morphism rmul with signature (req ==> req ==> req) as rmul_ext1. + Proof. exact (SRmul_ext SReqe). Qed. + Variable SRth : semi_ring_theory 0 1 radd rmul req. (** Every semi ring can be seen as an almost ring, by taking : @@ -323,9 +327,15 @@ Section ALMOST_RING. Notation "- x" := (ropp x). Variable Reqe : ring_eq_ext radd rmul ropp req. - Add Morphism radd : radd_ext2. exact (Radd_ext Reqe). Qed. - Add Morphism rmul : rmul_ext2. exact (Rmul_ext Reqe). Qed. - Add Morphism ropp : ropp_ext2. exact (Ropp_ext Reqe). Qed. + + Add Morphism radd with signature (req ==> req ==> req) as radd_ext2. + Proof. exact (Radd_ext Reqe). Qed. + + Add Morphism rmul with signature (req ==> req ==> req) as rmul_ext2. + Proof. exact (Rmul_ext Reqe). Qed. + + Add Morphism ropp with signature (req ==> req) as ropp_ext2. + Proof. exact (Ropp_ext Reqe). Qed. Section RING. Variable Rth : ring_theory 0 1 radd rmul rsub ropp req. @@ -393,14 +403,25 @@ Section ALMOST_RING. Notation "?=!" := ceqb. Notation "[ x ]" := (phi x). Variable Csth : Equivalence ceq. Variable Ceqe : ring_eq_ext cadd cmul copp ceq. + Add Setoid C ceq Csth as C_setoid. - Add Morphism cadd : cadd_ext. exact (Radd_ext Ceqe). Qed. - Add Morphism cmul : cmul_ext. exact (Rmul_ext Ceqe). Qed. - Add Morphism copp : copp_ext. exact (Ropp_ext Ceqe). Qed. + + Add Morphism cadd with signature (ceq ==> ceq ==> ceq) as cadd_ext. + Proof. exact (Radd_ext Ceqe). Qed. + + Add Morphism cmul with signature (ceq ==> ceq ==> ceq) as cmul_ext. + Proof. exact (Rmul_ext Ceqe). Qed. + + Add Morphism copp with signature (ceq ==> ceq) as copp_ext. + Proof. exact (Ropp_ext Ceqe). Qed. + Variable Cth : ring_theory cO cI cadd cmul csub copp ceq. Variable Smorph : semi_morph 0 1 radd rmul req cO cI cadd cmul ceqb phi. Variable phi_ext : forall x y, ceq x y -> [x] == [y]. - Add Morphism phi : phi_ext1. exact phi_ext. Qed. + + Add Morphism phi with signature (ceq ==> req) as phi_ext1. + Proof. exact phi_ext. Qed. + Lemma Smorph_opp x : [-!x] == -[x]. Proof. rewrite <- (Rth.(Radd_0_l) [-!x]). diff --git a/stm/proofBlockDelimiter.ml b/stm/proofBlockDelimiter.ml index a4b35ad60f..b46556ea67 100644 --- a/stm/proofBlockDelimiter.ml +++ b/stm/proofBlockDelimiter.ml @@ -11,7 +11,7 @@ open Stm module Util : sig val simple_goal : Evd.evar_map -> Goal.goal -> Goal.goal list -> bool -val is_focused_goal_simple : Stateid.t -> [ `Simple of Goal.goal list | `Not ] +val is_focused_goal_simple : doc:Stm.doc -> Stateid.t -> [ `Simple of Goal.goal list | `Not ] type 'a until = [ `Stop | `Found of static_block_declaration | `Cont of 'a ] @@ -43,8 +43,8 @@ let simple_goal sigma g gs = Set.is_empty (evars_of_filtered_evar_info (nf_evar_info sigma evi)) && not (List.exists (Proofview.depends_on sigma g) gs) -let is_focused_goal_simple id = - match state_of_id id with +let is_focused_goal_simple ~doc id = + match state_of_id ~doc id with | `Expired | `Error _ | `Valid None -> `Not | `Valid (Some { proof }) -> let proof = Proof_global.proof_of_state proof in @@ -88,8 +88,8 @@ let static_bullet ({ entry_point; prev_node } as view) = | _ -> `Stop) entry_point | _ -> assert false -let dynamic_bullet { dynamic_switch = id; carry_on_data = b } = - match is_focused_goal_simple id with +let dynamic_bullet doc { dynamic_switch = id; carry_on_data = b } = + match is_focused_goal_simple ~doc id with | `Simple focused -> `ValidBlock { base_state = id; @@ -116,8 +116,8 @@ let static_curly_brace ({ entry_point; prev_node } as view) = `Cont (nesting + 1,node) | _ -> `Cont (nesting,node)) (-1, entry_point) -let dynamic_curly_brace { dynamic_switch = id } = - match is_focused_goal_simple id with +let dynamic_curly_brace doc { dynamic_switch = id } = + match is_focused_goal_simple ~doc id with | `Simple focused -> `ValidBlock { base_state = id; @@ -138,8 +138,8 @@ let static_par { entry_point; prev_node } = Some { block_stop = entry_point.id; block_start = pid; dynamic_switch = pid; carry_on_data = unit_val } -let dynamic_par { dynamic_switch = id } = - match is_focused_goal_simple id with +let dynamic_par doc { dynamic_switch = id } = + match is_focused_goal_simple ~doc id with | `Simple focused -> `ValidBlock { base_state = id; @@ -167,9 +167,9 @@ let static_indent ({ entry_point; prev_node } as view) = carry_on_data = of_vernac_expr_val entry_point.ast } ) last_tac -let dynamic_indent { dynamic_switch = id; carry_on_data = e } = +let dynamic_indent doc { dynamic_switch = id; carry_on_data = e } = Printf.eprintf "%s\n" (Stateid.to_string id); - match is_focused_goal_simple id with + match is_focused_goal_simple ~doc id with | `Simple [] -> `Leaks | `Simple focused -> let but_last = List.tl (List.rev focused) in diff --git a/stm/proofBlockDelimiter.mli b/stm/proofBlockDelimiter.mli index e23a1d1c18..5cff0a8a72 100644 --- a/stm/proofBlockDelimiter.mli +++ b/stm/proofBlockDelimiter.mli @@ -21,7 +21,7 @@ type). `Simple carries the list of focused goals. *) val simple_goal : Evd.evar_map -> Goal.goal -> Goal.goal list -> bool -val is_focused_goal_simple : Stateid.t -> [ `Simple of Goal.goal list | `Not ] +val is_focused_goal_simple : doc:Stm.doc -> Stateid.t -> [ `Simple of Goal.goal list | `Not ] type 'a until = [ `Stop | `Found of Stm.static_block_declaration | `Cont of 'a ] diff --git a/stm/proofworkertop.ml b/stm/proofworkertop.ml index 95012d984e..a27c6d6cd2 100644 --- a/stm/proofworkertop.ml +++ b/stm/proofworkertop.ml @@ -10,5 +10,5 @@ module W = AsyncTaskQueue.MakeWorker(Stm.ProofTask) let () = Coqtop.toploop_init := WorkerLoop.loop W.init_stdout -let () = Coqtop.toploop_run := W.main_loop +let () = Coqtop.toploop_run := (fun _ -> W.main_loop ()) diff --git a/stm/queryworkertop.ml b/stm/queryworkertop.ml index 85f0e6bfc1..ac7a270ac6 100644 --- a/stm/queryworkertop.ml +++ b/stm/queryworkertop.ml @@ -10,5 +10,5 @@ module W = AsyncTaskQueue.MakeWorker(Stm.QueryTask) let () = Coqtop.toploop_init := WorkerLoop.loop W.init_stdout -let () = Coqtop.toploop_run := W.main_loop +let () = Coqtop.toploop_run := (fun _ -> W.main_loop ()) diff --git a/stm/stm.ml b/stm/stm.ml index 2c5e9ed819..220ed9be4e 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -40,8 +40,8 @@ let state_ready, state_ready_hook = Hook.make let forward_feedback, forward_feedback_hook = let m = Mutex.create () in Hook.make ~default:(function - | { id = id; route; contents } -> - try Mutex.lock m; feedback ~id:id ~route contents; Mutex.unlock m + | { doc_id = did; span_id = id; route; contents } -> + try Mutex.lock m; feedback ~did ~id ~route contents; Mutex.unlock m with e -> Mutex.unlock m; raise e) () let unreachable_state, unreachable_state_hook = Hook.make @@ -254,6 +254,10 @@ type stm_doc_type = | VioDoc of Names.DirPath.t | Interactive of Names.DirPath.t +(* Dummy until we land the functional interp patch + fixed start_library *) +type doc = int +let dummy_doc : doc = 0 + (* Imperative wrap around VCS to obtain _the_ VCS that is the * representation of the document Coq is currently processing *) module VCS : sig @@ -270,7 +274,7 @@ module VCS : sig type vcs = (branch_type, transaction, vcs state_info, box) Vcs_.t - val init : stm_doc_type -> id -> unit + val init : stm_doc_type -> id -> doc (* val get_type : unit -> stm_doc_type *) val is_interactive : unit -> [`Yes | `No | `Shallow] val is_vio_doc : unit -> bool @@ -460,7 +464,8 @@ end = struct (* {{{ *) let init dt id = doc_type := dt; vcs := empty id; - vcs := set_info !vcs id (default_info ()) + vcs := set_info !vcs id (default_info ()); + dummy_doc (* let get_type () = !doc_type *) @@ -682,7 +687,7 @@ end = struct (* {{{ *) end (* }}} *) -let state_of_id id = +let state_of_id ~doc id = try match (VCS.get_info id).state with | Valid s -> `Valid (Some s) | Error (e,_) -> `Error e @@ -971,7 +976,7 @@ let stm_vernac_interp ?proof id ?route { verbose; loc; expr } = (* The Stm will gain the capability to interpret commmads affecting the whole document state, such as backtrack, etc... so we start to design the stm command interpreter now *) - set_id_for_feedback ?route id; + set_id_for_feedback ?route dummy_doc id; Aux_file.record_in_aux_set_at ?loc (); (* We need to check if a command should be filtered from * vernac_entries, as it cannot handle it. This should go away in @@ -1137,6 +1142,7 @@ end (* }}} *) let hints = ref Aux_file.empty_aux_file let set_compilation_hints file = hints := Aux_file.load_aux_file_for file + let get_hint_ctx loc = let s = Aux_file.get ?loc !hints "context_used" in match Str.split (Str.regexp ";") s with @@ -1191,7 +1197,7 @@ type recovery_action = { } type dynamic_block_error_recovery = - static_block_declaration -> [ `ValidBlock of recovery_action | `Leaks ] + doc -> static_block_declaration -> [ `ValidBlock of recovery_action | `Leaks ] let proof_block_delimiters = ref [] @@ -2132,7 +2138,7 @@ let known_state ?(redefine_qed=false) ~cache id = let decl, name = List.hd valid_boxes in try let _, dynamic_check = List.assoc name !proof_block_delimiters in - match dynamic_check decl with + match dynamic_check dummy_doc decl with | `Leaks -> Exninfo.iraise exn | `ValidBlock { base_state; goals_to_admit; recovery_command } -> begin let tac = @@ -2368,7 +2374,7 @@ type stm_init_options = { } let init { doc_type } = - VCS.init doc_type Stateid.initial; + let doc = VCS.init doc_type Stateid.initial in set_undo_classifier Backtrack.undo_vernac_classifier; (* we declare the library here XXX: *) State.define ~cache:`Yes (fun () -> ()) Stateid.initial; @@ -2386,35 +2392,39 @@ let init { doc_type } = async_proofs_workers_extra_env := Array.of_list (Str.split_delim (Str.regexp ";") (Str.replace_first env_opt "" env)) with Not_found -> () end; - end + end; + doc -let observe id = +let observe ~doc id = let vcs = VCS.backup () in try Reach.known_state ~cache:(VCS.is_interactive ()) id; - VCS.print () + VCS.print (); + doc with e -> let e = CErrors.push e in VCS.print (); VCS.restore vcs; Exninfo.iraise e -let finish () = +let finish ~doc = let head = VCS.current_branch () in - observe (VCS.get_branch_pos head); + let doc =observe ~doc (VCS.get_branch_pos head) in VCS.print (); (* EJGA: Setting here the proof state looks really wrong, and it hides true bugs cf bug #5363. Also, what happens with observe? *) (* Some commands may by side effect change the proof mode *) - match VCS.get_branch head with + (match VCS.get_branch head with | { VCS.kind = `Edit (mode,_,_,_,_) } -> Proof_global.activate_proof_mode mode [@ocaml.warning "-3"] | { VCS.kind = `Proof (mode, _) } -> Proof_global.activate_proof_mode mode [@ocaml.warning "-3"] | _ -> () + ); doc -let wait () = - finish (); +let wait ~doc = + let doc = finish ~doc in Slaves.wait_all_done (); - VCS.print () + VCS.print (); + doc let rec join_admitted_proofs id = if Stateid.equal id Stateid.initial then () else @@ -2425,17 +2435,17 @@ let rec join_admitted_proofs id = join_admitted_proofs view.next | _ -> join_admitted_proofs view.next -let join () = - wait (); +let join ~doc = + let doc = wait ~doc in stm_prerr_endline (fun () -> "Joining the environment"); Global.join_safe_environment (); stm_prerr_endline (fun () -> "Joining Admitted proofs"); join_admitted_proofs (VCS.get_branch_pos (VCS.current_branch ())); VCS.print (); - VCS.print () + doc let dump_snapshot () = Slaves.dump_snapshot (), RemoteCounter.snapshot () -type document = VCS.vcs + type tasks = int Slaves.tasks * RemoteCounter.remote_counters_status let check_task name (tasks,rcbackup) i = RemoteCounter.restore rcbackup; @@ -2502,12 +2512,13 @@ let handle_failure (e, info) vcs = VCS.print (); Exninfo.iraise (e, info) -let snapshot_vio ldir long_f_dot_vo = - finish (); +let snapshot_vio ~doc ldir long_f_dot_vo = + let doc = finish ~doc in if List.length (VCS.branches ()) > 1 then CErrors.user_err ~hdr:"stm" (str"Cannot dump a vio with open proofs"); Library.save_library_to ~todo:(dump_snapshot ()) ldir long_f_dot_vo - (Global.opaque_tables ()) + (Global.opaque_tables ()); + doc let reset_task_queue = Slaves.reset_task_queue @@ -2542,7 +2553,7 @@ let process_transaction ?(newtip=Stateid.fresh ()) (VCS.branches ()); VCS.checkout_shallowest_proof_branch (); VCS.commit id (Alias (oid,x)); - Backtrack.record (); if w == VtNow then finish (); `Ok + Backtrack.record (); if w == VtNow then ignore(finish ~doc:dummy_doc); `Ok | VtBack (false, id), VtNow -> stm_prerr_endline (fun () -> "undo to state " ^ Stateid.to_string id); Backtrack.backto id; @@ -2571,7 +2582,7 @@ let process_transaction ?(newtip=Stateid.fresh ()) then `SkipQueue else `MainQueue in VCS.commit id (mkTransCmd x [] false queue); - Backtrack.record (); if w == VtNow then finish (); `Ok + Backtrack.record (); if w == VtNow then ignore(finish ~doc:dummy_doc); `Ok | VtQuery (false,_), VtLater -> anomaly(str"classifier: VtQuery + VtLater must imply part_of_script.") @@ -2589,7 +2600,7 @@ let process_transaction ?(newtip=Stateid.fresh ()) VCS.merge id ~ours:(Fork (x, bname, guarantee, names)) head end; Proof_global.activate_proof_mode mode [@ocaml.warning "-3"]; - Backtrack.record (); if w == VtNow then finish (); `Ok + Backtrack.record (); if w == VtNow then ignore(finish ~doc:dummy_doc); `Ok | VtProofMode _, VtLater -> anomaly(str"VtProofMode must be executed VtNow.") | VtProofMode mode, VtNow -> @@ -2607,7 +2618,7 @@ let process_transaction ?(newtip=Stateid.fresh ()) (VCS.branches ()); VCS.checkout_shallowest_proof_branch (); Backtrack.record (); - finish (); + ignore(finish ~doc:dummy_doc); `Ok | VtProofStep { parallel; proof_block_detection = cblock }, w -> let id = VCS.new_node ~id:newtip () in @@ -2620,14 +2631,14 @@ let process_transaction ?(newtip=Stateid.fresh ()) If/when and UI will make something useful with this piece of info, detection should occur here. detect_proof_block id cblock; *) - Backtrack.record (); if w == VtNow then finish (); `Ok + Backtrack.record (); if w == VtNow then ignore(finish ~doc:dummy_doc); `Ok | VtQed keep, w -> let valid = VCS.get_branch_pos head in let rc = merge_proof_branch ~valid ~id:newtip x keep head in VCS.checkout_shallowest_proof_branch (); - Backtrack.record (); if w == VtNow then finish (); + Backtrack.record (); if w == VtNow then ignore(finish ~doc:dummy_doc); rc - + (* Side effect on all branches *) | VtUnknown, _ when expr = VernacToplevelControl Drop -> stm_vernac_interp (VCS.get_branch_pos head) x; `Ok @@ -2644,7 +2655,7 @@ let process_transaction ?(newtip=Stateid.fresh ()) | _ -> ReplayCommand x in VCS.propagate_sideff ~action; VCS.checkout_shallowest_proof_branch (); - Backtrack.record (); if w == VtNow then finish (); `Ok + Backtrack.record (); if w == VtNow then ignore(finish ~doc:dummy_doc); `Ok (* Unknown: we execute it, check for open goals and propagate sideeff *) | VtUnknown, VtNow -> @@ -2693,7 +2704,7 @@ let process_transaction ?(newtip=Stateid.fresh ()) let e = CErrors.push e in handle_failure e vcs -let get_ast id = +let get_ast ~doc id = match VCS.visit id with | { step = `Cmd { cast = { loc; expr } } } | { step = `Fork (({ loc; expr }, _, _, _), _) } @@ -2714,7 +2725,7 @@ let stop_worker n = Slaves.cancel_worker n *) exception End_of_input -let parse_sentence sid pa = +let parse_sentence ~doc sid pa = (* XXX: Should this restore the previous state? Using reach here to try to really get to the proper state makes the error resilience code fail *) @@ -2778,7 +2789,7 @@ let compute_indentation ?loc sid = Option.cata (fun loc -> eff_indent, len ) (0, 0) loc -let add ~ontop ?newtip verb (loc, ast) = +let add ~doc ~ontop ?newtip verb (loc, ast) = let cur_tip = VCS.cur_tip () in if not (Stateid.equal ontop cur_tip) then user_err ?loc ~hdr:"Stm.add" @@ -2791,10 +2802,10 @@ let add ~ontop ?newtip verb (loc, ast) = let clas = classify_vernac ast in let aast = { verbose = verb; indentation; strlen; loc; expr = ast } in match process_transaction ?newtip aast clas with - | `Ok -> VCS.cur_tip (), `NewTip - | `Unfocus qed_id -> qed_id, `Unfocus (VCS.cur_tip ()) + | `Ok -> doc, VCS.cur_tip (), `NewTip + | `Unfocus qed_id -> doc, qed_id, `Unfocus (VCS.cur_tip ()) -let set_perspective id_list = Slaves.set_perspective id_list +let set_perspective ~doc id_list = Slaves.set_perspective id_list type focus = { start : Stateid.t; @@ -2802,11 +2813,11 @@ type focus = { tip : Stateid.t } -let query ~at ~route s = +let query ~doc ~at ~route s = Future.purify (fun s -> - if Stateid.equal at Stateid.dummy then finish () + if Stateid.equal at Stateid.dummy then ignore(finish ~doc:dummy_doc) else Reach.known_state ~cache:`Yes at; - let loc, ast = parse_sentence at s in + let loc, ast = parse_sentence ~doc at s in let indentation, strlen = compute_indentation ?loc at in CWarnings.set_current_loc loc; let clas = classify_vernac ast in @@ -2818,7 +2829,7 @@ let query ~at ~route s = ignore(process_transaction aast (VtQuery (false, route), VtNow))) s -let edit_at id = +let edit_at ~doc id = if Stateid.equal id Stateid.dummy then anomaly(str"edit_at dummy.") else let vcs = VCS.backup () in let on_cur_branch id = @@ -2927,7 +2938,7 @@ let edit_at id = | false, None, None -> backto id None in VCS.print (); - rc + doc, rc with e -> let (e, info) = CErrors.push e in match Stateid.get info with @@ -2941,15 +2952,14 @@ let edit_at id = VCS.print (); Exninfo.iraise (e, info) -let backup () = VCS.backup () -let restore d = VCS.restore d +let get_current_state ~doc = VCS.cur_tip () -let get_current_state () = VCS.cur_tip () +let get_doc did = dummy_doc (*********************** TTY API (PG, coqtop, coqc) ***************************) (******************************************************************************) -let current_proof_depth () = +let current_proof_depth ~doc = let head = VCS.current_branch () in match VCS.get_branch head with | { VCS.kind = `Master } -> 0 @@ -2968,7 +2978,7 @@ let proofname b = match VCS.get_branch b with | { VCS.kind = (`Proof _| `Edit _) } -> Some b | _ -> None -let get_all_proof_names () = +let get_all_proof_names ~doc = List.map unmangle (CList.map_filter proofname (VCS.branches ())) (* Export hooks *) diff --git a/stm/stm.mli b/stm/stm.mli index ea8aecaed0..47963e5d81 100644 --- a/stm/stm.mli +++ b/stm/stm.mli @@ -28,11 +28,14 @@ type stm_init_options = { *) } -val init : stm_init_options -> unit +(** The type of a STM document *) +type doc + +val init : stm_init_options -> doc (* [parse_sentence sid pa] Reads a sentence from [pa] with parsing state [sid] Returns [End_of_input] if the stream ends *) -val parse_sentence : Stateid.t -> Pcoq.Gram.coq_parsable -> +val parse_sentence : doc:doc -> Stateid.t -> Pcoq.Gram.coq_parsable -> Vernacexpr.vernac_expr Loc.located (* Reminder: A parsable [pa] is constructed using @@ -46,14 +49,14 @@ exception End_of_input sync, but it will eventually call edit_at on the fly if needed. If [newtip] is provided, then the returned state id is guaranteed to be [newtip] *) -val add : ontop:Stateid.t -> ?newtip:Stateid.t -> +val add : doc:doc -> ontop:Stateid.t -> ?newtip:Stateid.t -> bool -> Vernacexpr.vernac_expr Loc.located -> - Stateid.t * [ `NewTip | `Unfocus of Stateid.t ] + doc * Stateid.t * [ `NewTip | `Unfocus of Stateid.t ] (* [query at ?report_with cmd] Executes [cmd] at a given state [at], throwing away side effects except messages. Feedback will be sent with [report_with], which defaults to the dummy state id *) -val query : +val query : doc:doc -> at:Stateid.t -> route:Feedback.route_id -> Pcoq.Gram.coq_parsable -> unit (* [edit_at id] is issued to change the editing zone. [`NewTip] is returned if @@ -66,27 +69,27 @@ val query : If Flags.async_proofs_full is set, then [id] is not [observe]d, else it is. *) type focus = { start : Stateid.t; stop : Stateid.t; tip : Stateid.t } -val edit_at : Stateid.t -> [ `NewTip | `Focus of focus ] +val edit_at : doc:doc -> Stateid.t -> doc * [ `NewTip | `Focus of focus ] (* Evaluates the tip of the current branch *) -val finish : unit -> unit +val finish : doc:doc -> doc (* Internal use (fake_ide) only, do not use *) -val wait : unit -> unit +val wait : doc:doc -> doc -val observe : Stateid.t -> unit +val observe : doc:doc -> Stateid.t -> doc val stop_worker : string -> unit (* Joins the entire document. Implies finish, but also checks proofs *) -val join : unit -> unit +val join : doc:doc -> doc (* Saves on the disk a .vio corresponding to the current status: - if the worker pool is empty, all tasks are saved - if the worker proof is not empty, then it waits until all workers are done with their current jobs and then dumps (or fails if one of the completed tasks is a failure) *) -val snapshot_vio : DirPath.t -> string -> unit +val snapshot_vio : doc:doc -> DirPath.t -> string -> doc (* Empties the task queue, can be used only if the worker pool is empty (E.g. * after having built a .vio in batch mode *) @@ -101,20 +104,16 @@ val finish_tasks : string -> tasks -> Library.seg_univ * Library.seg_proofs (* Id of the tip of the current branch *) -val get_current_state : unit -> Stateid.t +val get_current_state : doc:doc -> Stateid.t (* This returns the node at that position *) -val get_ast : Stateid.t -> (Vernacexpr.vernac_expr Loc.located) option +val get_ast : doc:doc -> Stateid.t -> (Vernacexpr.vernac_expr Loc.located) option (* Filename *) val set_compilation_hints : string -> unit (* Reorders the task queue putting forward what is in the perspective *) -val set_perspective : Stateid.t list -> unit - -type document -val backup : unit -> document -val restore : document -> unit +val set_perspective : doc:doc -> Stateid.t list -> unit (** workers **************************************************************** **) @@ -129,20 +128,20 @@ module QueryTask : AsyncTaskQueue.Task While checking a proof, if an error occurs in a (valid) block then processing can skip the entire block and go on to give feedback on the rest of the proof. - + static_block_detection and dynamic_block_validation are run when the closing block marker is parsed/executed respectively. - + static_block_detection is for example called when "}" is parsed and declares a block containing all proof steps between it and the matching "{". - + dynamic_block_validation is called when an error "crosses" the "}" statement. Depending on the nature of the goal focused by "{" the block may absorb the error or not. For example if the focused goal occurs in the type of another goal, then the block is leaky. Note that one can design proof commands that need no dynamic validation. - + Example of document: .. { tac1. tac2. } .. @@ -150,7 +149,7 @@ module QueryTask : AsyncTaskQueue.Task Corresponding DAG: .. (3) <-- { -- (4) <-- tac1 -- (5) <-- tac2 -- (6) <-- } -- (7) .. - + Declaration of block [-------------------------------------------] start = 5 the first state_id that could fail in the block @@ -190,7 +189,7 @@ type recovery_action = { } type dynamic_block_error_recovery = - static_block_declaration -> [ `ValidBlock of recovery_action | `Leaks ] + doc -> static_block_declaration -> [ `ValidBlock of recovery_action | `Leaks ] val register_proof_block_delimiter : Vernacexpr.proof_block_name -> @@ -219,9 +218,12 @@ type state = { proof : Proof_global.state; shallow : bool } -val state_of_id : + +val get_doc : Feedback.doc_id -> doc + +val state_of_id : doc:doc -> Stateid.t -> [ `Valid of state option | `Expired | `Error of exn ] (* Queries for backward compatibility *) -val current_proof_depth : unit -> int -val get_all_proof_names : unit -> Id.t list +val current_proof_depth : doc:doc -> int +val get_all_proof_names : doc:doc -> Id.t list diff --git a/stm/tacworkertop.ml b/stm/tacworkertop.ml index 186c8f8b7c..1716ac0c61 100644 --- a/stm/tacworkertop.ml +++ b/stm/tacworkertop.ml @@ -10,5 +10,5 @@ module W = AsyncTaskQueue.MakeWorker(Stm.TacTask) let () = Coqtop.toploop_init := WorkerLoop.loop W.init_stdout -let () = Coqtop.toploop_run := W.main_loop +let () = Coqtop.toploop_run := (fun _ -> W.main_loop ()) diff --git a/test-suite/bugs/closed/148.v b/test-suite/bugs/closed/148.v new file mode 100644 index 0000000000..6cafb9f0cd --- /dev/null +++ b/test-suite/bugs/closed/148.v @@ -0,0 +1,26 @@ +(** Omega is now aware of the bodies of context variables + (of type Z or nat). *) + +Require Import ZArith Omega. +Open Scope Z. + +Goal let x := 3 in x = 3. +intros. +omega. +Qed. + +Open Scope nat. + +Goal let x := 2 in x = 2. +intros. +omega. +Qed. + +(** NB: this could be disabled for compatibility reasons *) + +Unset Omega UseLocalDefs. + +Goal let x := 4 in x = 4. +intros. +Fail omega. +Abort. diff --git a/test-suite/success/ROmega4.v b/test-suite/success/ROmega4.v new file mode 100644 index 0000000000..58ae5b8fb8 --- /dev/null +++ b/test-suite/success/ROmega4.v @@ -0,0 +1,26 @@ +(** ROmega is now aware of the bodies of context variables + (of type Z or nat). + See also #148 for the corresponding improvement in Omega. +*) + +Require Import ZArith ROmega. +Open Scope Z. + +Goal let x := 3 in x = 3. +intros. +romega. +Qed. + +(** Example seen in #4132 + (actually solvable even if b isn't known to be 5) *) + +Lemma foo + (x y x' zxy zxy' z : Z) + (b := 5) + (Ry : - b <= y < b) + (Bx : x' <= b) + (H : - zxy' <= zxy) + (H' : zxy' <= x') : - b <= zxy. +Proof. +romega. +Qed. diff --git a/test-suite/success/setoid_test.v b/test-suite/success/setoid_test.v index 1f24ef2a6b..c8dfcd2cbf 100644 --- a/test-suite/success/setoid_test.v +++ b/test-suite/success/setoid_test.v @@ -33,7 +33,8 @@ Qed. Add Setoid set same setoid_set as setsetoid. -Add Morphism In : In_ext. +Add Morphism In with signature (eq ==> same ==> iff) as In_ext. +Proof. unfold same; intros a s t H; elim (H a); auto. Qed. @@ -50,10 +51,9 @@ simpl; right. apply (H2 H1). Qed. -Add Morphism Add : Add_ext. +Add Morphism Add with signature (eq ==> same ==> same) as Add_ext. split; apply add_aux. assumption. - rewrite H. reflexivity. Qed. @@ -90,7 +90,7 @@ Qed. Parameter P : set -> Prop. Parameter P_ext : forall s t : set, same s t -> P s -> P t. -Add Morphism P : P_extt. +Add Morphism P with signature (same ==> iff) as P_extt. intros; split; apply P_ext; (assumption || apply (Seq_sym _ _ setoid_set); assumption). Qed. @@ -113,7 +113,7 @@ Definition f: forall A : Set, A -> A := fun A x => x. Add Relation (id A) (rel A) as eq_rel. -Add Morphism (@f A) : f_morph. +Add Morphism (@f A) with signature (eq ==> eq) as f_morph. Proof. unfold rel, f. trivial. Qed. diff --git a/test-suite/success/setoid_test2.v b/test-suite/success/setoid_test2.v index 6baf79701a..79467e549c 100644 --- a/test-suite/success/setoid_test2.v +++ b/test-suite/success/setoid_test2.v @@ -134,8 +134,8 @@ Axiom SetoidS2 : Setoid_Theory S2 eqS2. Add Setoid S2 eqS2 SetoidS2 as S2setoid. Axiom f : S1 -> nat -> S2. -Add Morphism f : f_compat. Admitted. -Add Morphism f : f_compat2. Admitted. +Add Morphism f with signature (eqS1 ==> eq ==> eqS2) as f_compat. Admitted. +Add Morphism f with signature (eqS1 ==> eq ==> eqS2) as f_compat2. Admitted. Theorem test1: forall x y, (eqS1 x y) -> (eqS2 (f x 0) (f y 0)). intros. @@ -151,7 +151,7 @@ Theorem test1': forall x y, (eqS1 x y) -> (eqS2 (f x 0) (f y 0)). Qed. Axiom g : S1 -> S2 -> nat. -Add Morphism g : g_compat. Admitted. +Add Morphism g with signature (eqS1 ==> eqS2 ==> eq) as g_compat. Admitted. Axiom P : nat -> Prop. Theorem test2: @@ -190,13 +190,13 @@ Theorem test5: Qed. Axiom f_test6 : S2 -> Prop. -Add Morphism f_test6 : f_test6_compat. Admitted. +Add Morphism f_test6 with signature (eqS2 ==> iff) as f_test6_compat. Admitted. Axiom g_test6 : bool -> S2. -Add Morphism g_test6 : g_test6_compat. Admitted. +Add Morphism g_test6 with signature (eq ==> eqS2) as g_test6_compat. Admitted. Axiom h_test6 : S1 -> bool. -Add Morphism h_test6 : h_test6_compat. Admitted. +Add Morphism h_test6 with signature (eqS1 ==> eq) as h_test6_compat. Admitted. Theorem test6: forall E1 E2, (eqS1 E1 E2) -> (f_test6 (g_test6 (h_test6 E2))) -> @@ -223,7 +223,7 @@ Add Setoid S1_test8 eqS1_test8 SetoidS1_test8 as S1_test8setoid. Instance eqS1_test8_default : DefaultRelation eqS1_test8. Axiom f_test8 : S2 -> S1_test8. -Add Morphism f_test8 : f_compat_test8. Admitted. +Add Morphism f_test8 with signature (eqS2 ==> eqS1_test8) as f_compat_test8. Admitted. Axiom eqS1_test8': S1_test8 -> S1_test8 -> Prop. Axiom SetoidS1_test8' : Setoid_Theory S1_test8 eqS1_test8'. @@ -233,7 +233,7 @@ Add Setoid S1_test8 eqS1_test8' SetoidS1_test8' as S1_test8setoid'. (S1_test8, eqS1_test8'). However this does not happen and there is still no syntax for it ;-( *) Axiom g_test8 : S1_test8 -> S2. -Add Morphism g_test8 : g_compat_test8. Admitted. +Add Morphism g_test8 with signature (eqS1_test8 ==> eqS2) as g_compat_test8. Admitted. Theorem test8: forall x x': S2, (eqS2 x x') -> diff --git a/theories/Compat/Coq87.v b/theories/Compat/Coq87.v index 61e911678a..ef1737bf85 100644 --- a/theories/Compat/Coq87.v +++ b/theories/Compat/Coq87.v @@ -7,3 +7,11 @@ (************************************************************************) (** Compatibility file for making Coq act similar to Coq v8.7 *) + +(* In 8.7, omega wasn't taking advantage of local abbreviations, + see bug 148 and PR#768. For adjusting this flag, we're forced to + first dynlink the omega plugin, but we should avoid doing a full + "Require Omega", since it has some undesired effects (at least on hints) + and breaks at least fiat-crypto. *) +Declare ML Module "omega_plugin". +Unset Omega UseLocalDefs. diff --git a/theories/FSets/FSetProperties.v b/theories/FSets/FSetProperties.v index 25b042ca98..0041bfa1c4 100644 --- a/theories/FSets/FSetProperties.v +++ b/theories/FSets/FSetProperties.v @@ -762,7 +762,7 @@ Module WProperties_fun (Import E : DecidableType)(M : WSfun E). rewrite (cardinal_2 (s:=remove x s') (s':=s') (x:=x)); eauto with set. Qed. - Add Morphism cardinal : cardinal_m. + Add Morphism cardinal with signature (Equal ==> Logic.eq) as cardinal_m. Proof. exact Equal_cardinal. Qed. diff --git a/theories/QArith/Qreduction.v b/theories/QArith/Qreduction.v index 88e1298fbe..5d055b5474 100644 --- a/theories/QArith/Qreduction.v +++ b/theories/QArith/Qreduction.v @@ -101,7 +101,7 @@ Proof. - apply Qred_complete. Qed. -Add Morphism Qred : Qred_comp. +Add Morphism Qred with signature (Qeq ==> Qeq) as Qred_comp. Proof. intros. now rewrite !Qred_correct. Qed. @@ -125,19 +125,19 @@ Proof. intros; unfold Qminus'; apply Qred_correct; auto. Qed. -Add Morphism Qplus' : Qplus'_comp. +Add Morphism Qplus' with signature (Qeq ==> Qeq ==> Qeq) as Qplus'_comp. Proof. intros; unfold Qplus'. rewrite H, H0; auto with qarith. Qed. -Add Morphism Qmult' : Qmult'_comp. +Add Morphism Qmult' with signature (Qeq ==> Qeq ==> Qeq) as Qmult'_comp. Proof. intros; unfold Qmult'. rewrite H, H0; auto with qarith. Qed. -Add Morphism Qminus' : Qminus'_comp. +Add Morphism Qminus' with signature (Qeq ==> Qeq ==> Qeq) as Qminus'_comp. Proof. intros; unfold Qminus'. rewrite H, H0; auto with qarith. diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml index 8f676c656b..bf22c16cd3 100644 --- a/toplevel/coqinit.ml +++ b/toplevel/coqinit.ml @@ -27,12 +27,12 @@ let set_rcfile s = rcfile := s; rcfile_specified := true let load_rc = ref true let no_load_rc () = load_rc := false -let load_rcfile sid = +let load_rcfile doc sid = if !load_rc then try if !rcfile_specified then if CUnix.file_readable_p !rcfile then - Vernac.load_vernac ~verbosely:false ~interactive:false ~check:true sid !rcfile + Vernac.load_vernac ~verbosely:false ~interactive:false ~check:true doc sid !rcfile else raise (Sys_error ("Cannot read rcfile: "^ !rcfile)) else try @@ -43,8 +43,8 @@ let load_rcfile sid = Envars.home ~warn / "."^rcdefaultname^"."^Coq_config.version; Envars.home ~warn / "."^rcdefaultname ] in - Vernac.load_vernac ~verbosely:false ~interactive:false ~check:true sid inferedrc - with Not_found -> sid + Vernac.load_vernac ~verbosely:false ~interactive:false ~check:true doc sid inferedrc + with Not_found -> doc, sid (* Flags.if_verbose mSGNL (str ("No coqrc or coqrc."^Coq_config.version^ @@ -56,7 +56,7 @@ let load_rcfile sid = iraise reraise else (Flags.if_verbose Feedback.msg_info (str"Skipping rcfile loading."); - sid) + doc, sid) (* Recursively puts dir in the LoadPath if -nois was not passed *) let add_stdlib_path ~unix_path ~coq_root ~with_ml = diff --git a/toplevel/coqinit.mli b/toplevel/coqinit.mli index 1f7fd6ed95..2c275a00d3 100644 --- a/toplevel/coqinit.mli +++ b/toplevel/coqinit.mli @@ -13,7 +13,7 @@ val set_debug : unit -> unit val set_rcfile : string -> unit val no_load_rc : unit -> unit -val load_rcfile : Stateid.t -> Stateid.t +val load_rcfile : Stm.doc -> Stateid.t -> Stm.doc * Stateid.t val push_include : string -> Names.DirPath.t -> bool -> unit (** [push_include phys_path log_path implicit] *) diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml index 444bf8a8f7..c16e2751bc 100644 --- a/toplevel/coqloop.ml +++ b/toplevel/coqloop.ml @@ -17,7 +17,7 @@ let top_stderr x = * entered to be able to report errors without pretty-printing. *) type input_buffer = { - mutable prompt : unit -> string; + mutable prompt : Stm.doc -> string; mutable str : Bytes.t; (* buffer of already read characters *) mutable len : int; (* number of chars in the buffer *) mutable bols : int list; (* offsets in str of beginning of lines *) @@ -52,12 +52,12 @@ let emacs_prompt_endstring () = if !print_emacs then "</prompt>" else "" (* Read a char in an input channel, displaying a prompt at every beginning of line. *) -let prompt_char ic ibuf count = +let prompt_char doc ic ibuf count = let bol = match ibuf.bols with | ll::_ -> Int.equal ibuf.len ll | [] -> Int.equal ibuf.len 0 in - if bol && not !print_emacs then top_stderr (str (ibuf.prompt())); + if bol && not !print_emacs then top_stderr (str (ibuf.prompt doc)); try let c = input_char ic in if c == '\n' then ibuf.bols <- (ibuf.len+1) :: ibuf.bols; @@ -70,11 +70,11 @@ let prompt_char ic ibuf count = (* Reinitialize the char stream (after a Drop) *) -let reset_input_buffer ic ibuf = +let reset_input_buffer doc ic ibuf = ibuf.str <- Bytes.empty; ibuf.len <- 0; ibuf.bols <- []; - ibuf.tokens <- Pcoq.Gram.parsable (Stream.from (prompt_char ic ibuf)); + ibuf.tokens <- Pcoq.Gram.parsable (Stream.from (prompt_char doc ic ibuf)); ibuf.start <- 0 (* Functions to print underlined locations from an input buffer. *) @@ -201,10 +201,10 @@ let make_prompt () = "n |lem1|lem2|lem3| p < " *) -let make_emacs_prompt() = - let statnum = Stateid.to_string (Stm.get_current_state ()) in - let dpth = Stm.current_proof_depth() in - let pending = Stm.get_all_proof_names() in +let make_emacs_prompt doc = + let statnum = Stateid.to_string (Stm.get_current_state ~doc) in + let dpth = Stm.current_proof_depth ~doc in + let pending = Stm.get_all_proof_names ~doc in let pendingprompt = List.fold_left (fun acc x -> acc ^ (if CString.is_empty acc then "" else "|") ^ Names.Id.to_string x) @@ -217,10 +217,10 @@ let make_emacs_prompt() = * initialized when a vernac command is immediately followed by "\n", * or after a Drop. *) let top_buffer = - let pr() = + let pr doc = emacs_prompt_startstring() ^ make_prompt() - ^ make_emacs_prompt() + ^ make_emacs_prompt doc ^ emacs_prompt_endstring() in { prompt = pr; @@ -232,7 +232,7 @@ let top_buffer = let set_prompt prompt = top_buffer.prompt - <- (fun () -> + <- (fun doc -> emacs_prompt_startstring() ^ prompt () ^ emacs_prompt_endstring()) @@ -258,8 +258,8 @@ let rec discard_to_dot () = | Stm.End_of_input -> raise Stm.End_of_input | e when CErrors.noncritical e -> () -let read_sentence sid input = - try Stm.parse_sentence sid input +let read_sentence ~doc sid input = + try Stm.parse_sentence ~doc sid input with reraise -> let reraise = CErrors.push reraise in discard_to_dot (); @@ -300,19 +300,19 @@ let coqloop_feed (fb : Feedback.feedback) = let open Feedback in is caught and handled (i.e. not re-raised). *) -let do_vernac sid = +let do_vernac doc sid = top_stderr (fnl()); - if !print_emacs then top_stderr (str (top_buffer.prompt())); + if !print_emacs then top_stderr (str (top_buffer.prompt doc)); resynch_buffer top_buffer; try let input = (top_buffer.tokens, None) in - Vernac.process_expr sid (read_sentence sid (fst input)) + Vernac.process_expr doc sid (read_sentence ~doc sid (fst input)) with | Stm.End_of_input | CErrors.Quit -> top_stderr (fnl ()); raise CErrors.Quit | CErrors.Drop -> (* Last chance *) if Mltop.is_ocaml_top() then raise CErrors.Drop - else (Feedback.msg_error (str "There is no ML toplevel."); sid) + else (Feedback.msg_error (str "There is no ML toplevel."); doc, sid) (* Exception printing should be done by the feedback listener, however this is not yet ready so we rely on the exception for now. *) @@ -321,7 +321,7 @@ let do_vernac sid = let loc = Loc.get_loc info in let msg = CErrors.iprint (e, info) in TopErr.print_error_for_buffer ?loc Feedback.Error msg top_buffer; - sid + doc, sid (** Main coq loop : read vernacular expressions until Drop is entered. Ctrl-C is handled internally as Sys.Break instead of aborting Coq. @@ -337,18 +337,18 @@ let loop_flush_all () = Format.pp_print_flush !Topfmt.std_ft (); Format.pp_print_flush !Topfmt.err_ft () -let rec loop () = +let rec loop doc = Sys.catch_break true; try - reset_input_buffer stdin top_buffer; + reset_input_buffer doc stdin top_buffer; (* Be careful to keep this loop tail-recursive *) - let rec vernac_loop sid = - let nsid = do_vernac sid in + let rec vernac_loop doc sid = + let ndoc, nsid = do_vernac doc sid in loop_flush_all (); - vernac_loop nsid + vernac_loop ndoc nsid (* We recover the current stateid, threading from the caller is not possible due exceptions. *) - in vernac_loop (Stm.get_current_state ()) + in vernac_loop doc (Stm.get_current_state ~doc) with | CErrors.Drop -> () | CErrors.Quit -> exit 0 @@ -358,4 +358,4 @@ let rec loop () = fnl() ++ str"Please report" ++ strbrk" at " ++ str Coq_config.wwwbugtracker ++ str "."); - loop () + loop doc diff --git a/toplevel/coqloop.mli b/toplevel/coqloop.mli index 8eaa68914e..46dabf995d 100644 --- a/toplevel/coqloop.mli +++ b/toplevel/coqloop.mli @@ -15,7 +15,7 @@ val print_emacs : bool ref * entered to be able to report errors without pretty-printing. *) type input_buffer = { - mutable prompt : unit -> string; + mutable prompt : Stm.doc -> string; mutable str : Bytes.t; (** buffer of already read characters *) mutable len : int; (** number of chars in the buffer *) mutable bols : int list; (** offsets in str of begining of lines *) @@ -32,8 +32,8 @@ val coqloop_feed : Feedback.feedback -> unit (** Parse and execute one vernac command. *) -val do_vernac : Stateid.t -> Stateid.t +val do_vernac : Stm.doc -> Stateid.t -> Stm.doc * Stateid.t (** Main entry point of Coq: read and execute vernac commands. *) -val loop : unit -> unit +val loop : Stm.doc -> unit diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 0624c9bed8..9b58c9a654 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -81,14 +81,14 @@ let toploop_init = ref begin fun x -> let coqtop_init_feed = Coqloop.coqloop_feed (* Default toplevel loop *) -let console_toploop_run () = +let console_toploop_run doc = (* We initialize the console only if we run the toploop_run *) let tl_feed = Feedback.add_feeder Coqloop.coqloop_feed in if Dumpglob.dump () then begin Flags.if_verbose warning "Dumpglob cannot be used in interactive mode."; Dumpglob.noglob () end; - Coqloop.loop(); + Coqloop.loop doc; (* Initialise and launch the Ocaml toplevel *) Coqinit.init_ocaml_path(); Mltop.ocaml_toploop(); @@ -121,11 +121,6 @@ let print_memory_stat () = let _ = at_exit print_memory_stat (******************************************************************************) -(* Deprecated *) -(******************************************************************************) -let _remove_top_ml () = Mltop.remove () - -(******************************************************************************) (* Engagement *) (******************************************************************************) let impredicative_set = ref Declarations.PredicativeSet @@ -183,15 +178,15 @@ let load_vernacular_list = ref ([] : (string * bool) list) let add_load_vernacular verb s = load_vernacular_list := ((CUnix.make_suffix s ".v"),verb) :: !load_vernacular_list -let load_vernacular sid = +let load_vernacular doc sid = List.fold_left - (fun sid (f_in, verbosely) -> + (fun (doc,sid) (f_in, verbosely) -> let s = Loadpath.locate_file f_in in if !Flags.beautify then - Flags.with_option Flags.beautify_file (Vernac.load_vernac ~verbosely ~interactive:false ~check:true sid) f_in + Flags.with_option Flags.beautify_file (Vernac.load_vernac ~verbosely ~interactive:false ~check:true doc sid) f_in else - Vernac.load_vernac ~verbosely ~interactive:false ~check:true sid s) - sid (List.rev !load_vernacular_list) + Vernac.load_vernac ~verbosely ~interactive:false ~check:true doc sid s) + (doc, sid) (List.rev !load_vernacular_list) let load_vernacular_obj = ref ([] : string list) let add_vernac_obj s = load_vernacular_obj := s :: !load_vernacular_obj @@ -258,20 +253,20 @@ let add_compile verbose s = in compile_list := (verbose,s) :: !compile_list -let compile_file mode (verbosely,f_in) = +let compile_file mode doc (verbosely,f_in) = if !Flags.beautify then - Flags.with_option Flags.beautify_file (fun f_in -> Vernac.compile ~verbosely ~mode ~f_in ~f_out:None) f_in + Flags.with_option Flags.beautify_file (fun f_in -> Vernac.compile ~verbosely ~mode ~doc ~f_in ~f_out:None) f_in else - Vernac.compile ~verbosely ~mode ~f_in ~f_out:None + Vernac.compile ~verbosely ~mode ~doc ~f_in ~f_out:None -let compile_files () = +let compile_files doc = if !compile_list == [] then () else let init_state = States.freeze ~marshallable:`No in let mode = !compilation_mode in List.iter (fun vf -> States.unfreeze init_state; - compile_file mode vf) + compile_file mode doc vf) (List.rev !compile_list) (******************************************************************************) @@ -283,7 +278,8 @@ let add_vio_task f = set_batch_mode (); Flags.quiet := true; vio_tasks := f :: !vio_tasks -let check_vio_tasks () = + +let check_vio_tasks doc = let rc = List.fold_left (fun acc t -> Vio_checking.check_vio t && acc) true (List.rev !vio_tasks) in @@ -307,7 +303,7 @@ let set_vio_checking_j opt j = prerr_endline "setting the J variable like in 'make vio2vo J=3'"; exit 1 -let schedule_vio_checking () = +let schedule_vio_checking doc = if !vio_files <> [] && !vio_checking then Vio_checking.schedule_vio_checking !vio_files_j !vio_files @@ -649,7 +645,7 @@ let init_toplevel arglist = Sys.catch_break false; (* Ctrl-C is fatal during the initialisation *) let init_feeder = Feedback.add_feeder coqtop_init_feed in Lib.init(); - begin + let doc = begin try let extras = parse_args arglist in (* If we have been spawned by the Spawn module, this has to be done @@ -677,27 +673,29 @@ let init_toplevel arglist = then Declaremods.start_library !toplevel_name; load_vernac_obj (); require (); - Stm.(init { doc_type = Interactive Names.DirPath.empty }); - let sid = Coqinit.load_rcfile (Stm.get_current_state ()) in + let doc = Stm.(init { doc_type = Interactive Names.DirPath.empty }) in + let doc, sid = Coqinit.load_rcfile doc (Stm.get_current_state ~doc) in (* XXX: We ignore this for now, but should be threaded to the toplevels *) - let _sid = load_vernacular sid in - compile_files (); + let doc, _sid = load_vernacular doc sid in + compile_files doc; (* All these tasks use coqtop as a driver to invoke more coqtop, * they should be really orthogonal to coqtop. *) - schedule_vio_checking (); + schedule_vio_checking doc; schedule_vio_compilation (); - check_vio_tasks (); - outputstate () + check_vio_tasks doc; + outputstate (); + doc with any -> flush_all(); - let extra = - if !batch_mode && not Stateid.(equal (Stm.get_current_state ()) dummy) - then None - else Some (str "Error during initialization: ") + let extra = None + (* XXX: Must refine once Stm.init takes care of the start_library & friends *) + (* if !batch_mode && not Stateid.(equal (Stm.get_current_state ~doc) dummy) *) + (* then None *) + (* else Some (str "Error during initialization: ") *) in fatal_error ?extra any - end; + end in if !batch_mode then begin flush_all(); if !output_context then @@ -705,13 +703,14 @@ let init_toplevel arglist = Profile.print_profile (); exit 0 end; - Feedback.del_feeder init_feeder + Feedback.del_feeder init_feeder; + doc let start () = - let () = init_toplevel (List.tl (Array.to_list Sys.argv)) in + let doc = init_toplevel (List.tl (Array.to_list Sys.argv)) in (* In batch mode, Coqtop has already exited at this point. In interactive one, dump glob is nothing but garbage ... *) - !toploop_run (); + !toploop_run doc; exit 1 (* [Coqtop.start] will be called by the code produced by coqmktop *) diff --git a/toplevel/coqtop.mli b/toplevel/coqtop.mli index ac2be7e161..4c26a6ebcc 100644 --- a/toplevel/coqtop.mli +++ b/toplevel/coqtop.mli @@ -11,11 +11,11 @@ state, load the files given on the command line, load the resource file, produce the output state if any, and finally will launch [Coqloop.loop]. *) -val init_toplevel : string list -> unit +val init_toplevel : string list -> Stm.doc val start : unit -> unit (* For other toploops *) val toploop_init : (string list -> string list) ref -val toploop_run : (unit -> unit) ref +val toploop_run : (Stm.doc -> unit) ref diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index cb89dc8ff9..1e09a1c0d2 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -113,13 +113,13 @@ let vernac_error msg = (* Stm.End_of_input -> true *) (* | _ -> false *) -let rec interp_vernac ~check ~interactive sid (loc,com) = +let rec interp_vernac ~check ~interactive doc sid (loc,com) = let interp = function | VernacLoad (verbosely, fname) -> let fname = Envars.expand_path_macros ~warn:(fun x -> Feedback.msg_warning (str x)) fname in let fname = CUnix.make_suffix fname ".v" in let f = Loadpath.locate_file fname in - load_vernac ~verbosely ~check ~interactive sid f + load_vernac ~verbosely ~check ~interactive doc sid f | v -> (* XXX: We need to run this before add as the classification is @@ -137,7 +137,7 @@ let rec interp_vernac ~check ~interactive sid (loc,com) = in CWarnings.set_flags wflags; - let nsid, ntip = Stm.add ~ontop:sid (not !Flags.quiet) (loc,v) in + let doc, nsid, ntip = Stm.add ~doc ~ontop:sid (not !Flags.quiet) (loc,v) in (* Main STM interaction *) if ntip <> `NewTip then @@ -146,7 +146,7 @@ let rec interp_vernac ~check ~interactive sid (loc,com) = (* Due to bug #5363 we cannot use observe here as we should, it otherwise reveals bugs *) (* Stm.observe nsid; *) - if check then Stm.finish (); + let ndoc = if check then Stm.finish ~doc else doc in (* We could use a more refined criteria that depends on the vernac. For now we imitate the old approach and rely on the @@ -155,7 +155,7 @@ let rec interp_vernac ~check ~interactive sid (loc,com) = is_proof_step && Proof_global.there_are_pending_proofs () in if print_goals then Feedback.msg_notice (pr_open_cur_subgoals ()); - nsid + ndoc, nsid in try (* The -time option is only supported from console-based @@ -166,7 +166,7 @@ let rec interp_vernac ~check ~interactive sid (loc,com) = with reraise -> (* XXX: In non-interactive mode edit_at seems to do very weird things, so we better avoid it while we investigate *) - if interactive then ignore(Stm.edit_at sid); + if interactive then ignore(Stm.edit_at ~doc sid); let (reraise, info) = CErrors.push reraise in let info = begin match Loc.get_loc info with @@ -175,7 +175,7 @@ let rec interp_vernac ~check ~interactive sid (loc,com) = end in iraise (reraise, info) (* Load a vernac file. CErrors are annotated with file and location *) -and load_vernac ~verbosely ~check ~interactive sid file = +and load_vernac ~verbosely ~check ~interactive doc sid file = let ft_beautify, close_beautify = if !Flags.beautify_file then let chan_beautify = open_out (file^beautify_suffix) in @@ -187,12 +187,13 @@ and load_vernac ~verbosely ~check ~interactive sid file = let in_echo = if verbosely then Some (open_utf8_file_in file) else None in let in_pa = Pcoq.Gram.parsable ~file:(Loc.InFile file) (Stream.of_channel in_chan) in let rsid = ref sid in + let rdoc = ref doc in try (* we go out of the following infinite loop when a End_of_input is * raised, which means that we raised the end of the file being loaded *) while true do let loc, ast = - Stm.parse_sentence !rsid in_pa + Stm.parse_sentence ~doc:!rdoc !rsid in_pa (* If an error in parsing occurs, we propagate the exception so the caller of load_vernac will take care of it. However, in the future it could be possible that we want to handle @@ -216,10 +217,11 @@ and load_vernac ~verbosely ~check ~interactive sid file = Option.iter (vernac_echo ?loc) in_echo; checknav_simple (loc, ast); - let nsid = Flags.silently (interp_vernac ~check ~interactive !rsid) (loc, ast) in - rsid := nsid + let ndoc, nsid = Flags.silently (interp_vernac ~check ~interactive !rdoc !rsid) (loc, ast) in + rsid := nsid; + rdoc := ndoc done; - !rsid + !rdoc, !rsid with any -> (* whatever the exception *) let (e, info) = CErrors.push any in close_in in_chan; @@ -230,7 +232,7 @@ and load_vernac ~verbosely ~check ~interactive sid file = if !Flags.beautify then pr_new_syntax ~loc:(Loc.make_loc (max_int,max_int)) in_pa ft_beautify None; if !Flags.beautify_file then close_beautify (); - !rsid + !rdoc, !rsid | reraise -> if !Flags.beautify_file then close_beautify (); iraise (disable_drop e, info) @@ -242,9 +244,9 @@ and load_vernac ~verbosely ~check ~interactive sid file = of a new state label). An example of state-preserving command is one coming from the query panel of Coqide. *) -let process_expr sid loc_ast = +let process_expr doc sid loc_ast = checknav_deep loc_ast; - interp_vernac ~interactive:true ~check:true sid loc_ast + interp_vernac ~interactive:true ~check:true doc sid loc_ast let warn_file_no_extension = CWarnings.create ~name:"file-no-extension" ~category:"filesystem" @@ -284,7 +286,7 @@ let ensure_exists f = type compilation_mode = BuildVo | BuildVio | Vio2Vo (* Compile a vernac file *) -let compile ~verbosely ~mode ~f_in ~f_out= +let compile ~verbosely ~mode ~doc ~f_in ~f_out= let check_pending_proofs () = let pfs = Proof_global.get_all_proof_names () in if not (List.is_empty pfs) then @@ -310,8 +312,8 @@ let compile ~verbosely ~mode ~f_in ~f_out= Dumpglob.start_dump_glob ~vfile:long_f_dot_v ~vofile:long_f_dot_vo; Dumpglob.dump_string ("F" ^ Names.DirPath.to_string ldir ^ "\n"); let wall_clock1 = Unix.gettimeofday () in - let _ = load_vernac ~verbosely ~check:true ~interactive:false (Stm.get_current_state ()) long_f_dot_v in - Stm.join (); + let _ = load_vernac ~verbosely ~check:true ~interactive:false doc (Stm.get_current_state ~doc) long_f_dot_v in + let _doc = Stm.join ~doc in let wall_clock2 = Unix.gettimeofday () in check_pending_proofs (); Library.save_library_to ldir long_f_dot_vo (Global.opaque_tables ()); @@ -329,10 +331,10 @@ let compile ~verbosely ~mode ~f_in ~f_out= let ldir = Flags.verbosely Library.start_library long_f_dot_vio in Dumpglob.noglob (); Stm.set_compilation_hints long_f_dot_vio; - let _ = load_vernac ~verbosely ~check:false ~interactive:false (Stm.get_current_state ()) long_f_dot_v in - Stm.finish (); + let _ = load_vernac ~verbosely ~check:false ~interactive:false doc (Stm.get_current_state ~doc) long_f_dot_v in + let doc = Stm.finish ~doc in check_pending_proofs (); - Stm.snapshot_vio ldir long_f_dot_vio; + let _doc = Stm.snapshot_vio ~doc ldir long_f_dot_vio in Stm.reset_task_queue () | Vio2Vo -> let open Filename in @@ -343,7 +345,7 @@ let compile ~verbosely ~mode ~f_in ~f_out= let univs, proofs = Stm.finish_tasks lfdv univs disch proofs tasks in Library.save_library_raw lfdv sum lib univs proofs -let compile ~verbosely ~mode ~f_in ~f_out = +let compile ~verbosely ~mode ~doc ~f_in ~f_out = ignore(CoqworkmgrApi.get 1); - compile ~verbosely ~mode ~f_in ~f_out; + compile ~verbosely ~mode ~doc ~f_in ~f_out; CoqworkmgrApi.giveback 1 diff --git a/toplevel/vernac.mli b/toplevel/vernac.mli index 410dcf0d46..d3a45ce9de 100644 --- a/toplevel/vernac.mli +++ b/toplevel/vernac.mli @@ -12,14 +12,14 @@ expected to handle and print errors in form of exceptions, however care is taken so the state machine is left in a consistent state. *) -val process_expr : Stateid.t -> Vernacexpr.vernac_expr Loc.located -> Stateid.t +val process_expr : Stm.doc -> Stateid.t -> Vernacexpr.vernac_expr Loc.located -> Stm.doc * Stateid.t (** [load_vernac echo sid file] Loads [file] on top of [sid], will echo the commands if [echo] is set. Callers are expected to handle and print errors in form of exceptions. *) -val load_vernac : verbosely:bool -> check:bool -> interactive:bool -> Stateid.t -> string -> Stateid.t +val load_vernac : verbosely:bool -> check:bool -> interactive:bool -> Stm.doc -> Stateid.t -> string -> Stm.doc * Stateid.t type compilation_mode = BuildVo | BuildVio | Vio2Vo (** Compile a vernac file, (f is assumed without .v suffix) *) -val compile : verbosely:bool -> mode:compilation_mode -> f_in:string -> f_out:string option -> unit +val compile : verbosely:bool -> mode:compilation_mode -> doc:Stm.doc -> f_in:string -> f_out:string option -> unit |