diff options
51 files changed, 483 insertions, 220 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index fcf6413be3..7c3489de42 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -284,6 +284,9 @@ ci-coquelicot: <<: *ci-template-vars EXTRA_PACKAGES: "$TIMING_PACKAGES autoconf" +ci-equations: + <<: *ci-template + ci-geocoq: <<: *ci-template allow_failure: true diff --git a/.travis.yml b/.travis.yml index 3ebfbefd20..1f6bb11e0e 100644 --- a/.travis.yml +++ b/.travis.yml @@ -50,6 +50,7 @@ env: - TEST_TARGET="ci-compcert TIMED=1" - TEST_TARGET="ci-coq-dpdgraph" EXTRA_OPAM="ocamlgraph" - TEST_TARGET="ci-coquelicot TIMED=1" + - TEST_TARGET="ci-equations TIMED=1" - TEST_TARGET="ci-geocoq TIMED=1" - TEST_TARGET="ci-fiat-crypto TIMED=1" - TEST_TARGET="ci-fiat-parsers TIMED=1" diff --git a/API/API.ml b/API/API.ml index f588fe193a..78d9c0c26e 100644 --- a/API/API.ml +++ b/API/API.ml @@ -275,6 +275,7 @@ module Command = Command module Classes = Classes (* module Record *) (* module Assumptions *) +module Vernacstate = Vernacstate module Vernacinterp = Vernacinterp module Mltop = Mltop module Topfmt = Topfmt diff --git a/API/API.mli b/API/API.mli index 44d02ce2b9..51671fc3d2 100644 --- a/API/API.mli +++ b/API/API.mli @@ -4650,16 +4650,23 @@ sig type proof type 'a focus_kind + val proof : proof -> + Goal.goal list * (Goal.goal list * Goal.goal list) list * + Goal.goal list * Goal.goal list * Evd.evar_map + val run_tactic : Environ.env -> unit Proofview.tactic -> proof -> proof * (bool * Proofview_monad.Info.tree) val unshelve : proof -> proof val maximal_unfocus : 'a focus_kind -> proof -> proof val pr_proof : proof -> Pp.t + module V82 : sig val grab_evars : proof -> proof val subgoals : proof -> Goal.goal list Evd.sigma + [@@ocaml.deprecated "Use the first and fifth argument of [Proof.proof]"] + end end @@ -5934,14 +5941,30 @@ sig Names.Id.t end +module Vernacstate : +sig + + type t = { (* TODO: inline records in OCaml 4.03 *) + system : States.state; (* summary + libstack *) + proof : Proof_global.state; (* proof state *) + shallow : bool (* is the state trimmed down (libstack) *) + } + + (* XXX: This should not be exported *) + val freeze_interp_state : Summary.marshallable -> t + val unfreeze_interp_state : t -> unit + +end + module Vernacinterp : sig + type deprecation = bool - type vernac_command = Genarg.raw_generic_argument list -> Loc.t option -> unit + type vernac_command = + Genarg.raw_generic_argument list -> Loc.t option -> Vernacstate.t -> Vernacstate.t - val vinterp_add : deprecation -> Vernacexpr.extend_name -> - vernac_command -> unit + val vinterp_add : deprecation -> Vernacexpr.extend_name -> vernac_command -> unit end @@ -5963,15 +5986,6 @@ end module Vernacentries : sig - type interp_state = { (* TODO: inline records in OCaml 4.03 *) - system : States.state; (* summary + libstack *) - proof : Proof_global.state; (* proof state *) - shallow : bool (* is the state trimmed down (libstack) *) - } - - val freeze_interp_state : Summary.marshallable -> interp_state - val unfreeze_interp_state : interp_state -> unit - val dump_global : Libnames.reference Misctypes.or_by_notation -> unit val interp_redexp_hook : (Environ.env -> Evd.evar_map -> Genredexpr.raw_red_expr -> Evd.evar_map * Redexpr.red_expr) Hook.t @@ -6003,7 +6017,7 @@ sig val get_doc : Feedback.doc_id -> doc val state_of_id : doc:doc -> - Stateid.t -> [ `Valid of Vernacentries.interp_state option | `Expired | `Error of exn ] + Stateid.t -> [ `Valid of Vernacstate.t option | `Expired | `Error of exn ] end (************************************************************************) diff --git a/Makefile.build b/Makefile.build index 991942bf0a..39b793d2bb 100644 --- a/Makefile.build +++ b/Makefile.build @@ -734,8 +734,8 @@ $(MICROMEGAV:.v=.vo) $(MICROMEGAV:.v=.glob) : $(MICROMEGAV) theories/Init/Prelud $(SHOW)'COQC $<' $(HIDE)rm -f $*.glob $(HIDE)$(BOOTCOQC) $< | sed -e '$$d' > $(MICROMEGAGEN) - $(HIDE)cmp -s $(MICROMEGAML) $(MICROMEGAGEN) || \ - echo "Warning: $(MICROMEGAML) and the code generated by $(MICROMEGAV) differ !" + $(HIDE)diff -u --strip-trailing-cr $(MICROMEGAML) $(MICROMEGAGEN) || \ + (2>&1 echo "Error: $(MICROMEGAML) and the code generated by $(MICROMEGAV) differ !" && false) # The general rule for building .vo files : diff --git a/Makefile.ci b/Makefile.ci index 0b2cbb6637..a17d4ddf75 100644 --- a/Makefile.ci +++ b/Makefile.ci @@ -5,6 +5,7 @@ CI_TARGETS=ci-all \ ci-coq-dpdgraph \ ci-coquelicot \ ci-cpdt \ + ci-equations \ ci-fiat-crypto \ ci-fiat-parsers \ ci-flocq \ diff --git a/Makefile.install b/Makefile.install index 55229deb96..b590aad549 100644 --- a/Makefile.install +++ b/Makefile.install @@ -144,7 +144,7 @@ install-coq-manpages: install-emacs: $(MKDIR) $(FULLEMACSLIB) - $(INSTALLLIB) tools/gallina-db.el tools/coq-font-lock.el tools/gallina-syntax.el tools/gallina.el tools/coq-inferior.el $(FULLEMACSLIB) + $(INSTALLLIB) tools/gallina-db.el tools/coq-font-lock.el tools/gallina-syntax.el tools/gallina.el tools/inferior-coq.el $(FULLEMACSLIB) # command to update TeX' kpathsea database #UPDATETEX = $(MKTEXLSR) /usr/share/texmf /var/spool/texmf $(BASETEXDIR) > /dev/null diff --git a/dev/base_include b/dev/base_include index 0c2bdb9a25..1da5e3ed18 100644 --- a/dev/base_include +++ b/dev/base_include @@ -230,7 +230,7 @@ let pf_e gl s = let _ = Flags.in_debugger := false let _ = Flags.in_toplevel := true let _ = Constrextern.set_extern_reference - (fun ?loc _ r -> Libnames.Qualid (loc,Nametab.shortest_qualid_of_global Idset.empty r));; + (fun ?loc _ r -> Libnames.Qualid (loc,Nametab.shortest_qualid_of_global Id.Set.empty r));; let go () = Coqloop.loop Option.(get !Coqtop.drop_last_doc) diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh index cb1493d6aa..168a34e6e4 100644 --- a/dev/ci/ci-basic-overlay.sh +++ b/dev/ci/ci-basic-overlay.sh @@ -135,3 +135,9 @@ ######################################################################## : ${bignums_CI_BRANCH:=master} : ${bignums_CI_GITURL:=https://github.com/coq/bignums.git} + +######################################################################## +# Equations +######################################################################## +: ${Equations_CI_BRANCH:=8.8+alpha} +: ${Equations_CI_GITURL:=https://github.com/mattam82/Coq-Equations.git} diff --git a/dev/ci/ci-equations.sh b/dev/ci/ci-equations.sh new file mode 100755 index 0000000000..f7470463d9 --- /dev/null +++ b/dev/ci/ci-equations.sh @@ -0,0 +1,10 @@ +#!/usr/bin/env bash + +ci_dir="$(dirname "$0")" +source ${ci_dir}/ci-common.sh + +Equations_CI_DIR=${CI_BUILD_DIR}/Equations + +git_checkout ${Equations_CI_BRANCH} ${Equations_CI_GITURL} ${Equations_CI_DIR} + +( cd ${Equations_CI_DIR} && coq_makefile -f _CoqProject -o Makefile && make -j ${NJOBS} && make -j ${NJOBS} test-suite && make -j ${NJOBS} examples && make install) diff --git a/dev/top_printers.ml b/dev/top_printers.ml index b4c8ae33ca..5b09436c26 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -508,7 +508,7 @@ let _ = (function [c] when genarg_tag c = unquote (topwit wit_constr) && true -> let c = out_gen (rawwit wit_constr) c in - (fun _ -> in_current_context constr_display c) + (fun _ st -> in_current_context constr_display c; st) | _ -> failwith "Vernac extension: cannot occur") with e -> pp (CErrors.print e) @@ -524,7 +524,7 @@ let _ = (function [c] when genarg_tag c = unquote (topwit wit_constr) && true -> let c = out_gen (rawwit wit_constr) c in - (fun _ -> in_current_context print_pure_constr c) + (fun _ st -> in_current_context print_pure_constr c; st) | _ -> failwith "Vernac extension: cannot occur") with e -> pp (CErrors.print e) diff --git a/doc/refman/RefMan-uti.tex b/doc/refman/RefMan-uti.tex index 8f846f2f59..c411db1001 100644 --- a/doc/refman/RefMan-uti.tex +++ b/doc/refman/RefMan-uti.tex @@ -467,7 +467,7 @@ the \Coq\ language, and also a rudimentary indentation facility: \end{itemize} An inferior mode to run \Coq\ under Emacs, by Marco Maggesi, is also -included in the distribution, in file \texttt{coq-inferior.el}. +included in the distribution, in file \texttt{inferior-coq.el}. Instructions to use it are contained in this file. \subsection[{\ProofGeneral}]{{\ProofGeneral}\index{Proof General@{\ProofGeneral}}} diff --git a/engine/proofview.mli b/engine/proofview.mli index 0379d4b493..7f7acf8745 100644 --- a/engine/proofview.mli +++ b/engine/proofview.mli @@ -563,6 +563,7 @@ module V82 : sig (* Returns the open goals of the proofview together with the evar_map to interpret them. *) val goals : proofview -> Evar.t list Evd.sigma + [@@ocaml.deprecated "Use [Proofview.proofview]"] val top_goals : entry -> proofview -> Evar.t list Evd.sigma diff --git a/grammar/vernacextend.mlp b/grammar/vernacextend.mlp index 874712124c..12308bedef 100644 --- a/grammar/vernacextend.mlp +++ b/grammar/vernacextend.mlp @@ -158,18 +158,26 @@ EXTEND deprecation: [ [ "DEPRECATED" -> () ] ] ; - (* spiwack: comment-by-guessing: it seems that the isolated string (which - otherwise could have been another argument) is not passed to the - VernacExtend interpreter function to discriminate between the clauses. *) + (* spiwack: comment-by-guessing: it seems that the isolated string + (which otherwise could have been another argument) is not passed + to the VernacExtend interpreter function to discriminate between + the clauses. *) + + (* ejga: Due to the LocalityFixme abomination we cannot eta-expand + [e] as we'd like to, so we need to use the below mess with [fun + st -> st]. + + At some point We should solve the mess and extend + vernacextend.mlp with locality info. *) rule: [ [ "["; s = STRING; l = LIST0 args; "]"; d = OPT deprecation; c = OPT classifier; "->"; "["; e = Pcaml.expr; "]" -> let () = if s = "" then failwith "Command name is empty." in - let b = <:expr< fun loc -> $e$ >> in + let b = <:expr< fun loc -> ( let () = $e$ in fun st -> st ) >> in { r_head = Some s; r_patt = l; r_class = c; r_branch = b; r_depr = d; } | "[" ; "-" ; l = LIST1 args ; "]" ; d = OPT deprecation; c = OPT classifier; "->"; "["; e = Pcaml.expr; "]" -> - let b = <:expr< fun loc -> $e$ >> in + let b = <:expr< fun loc -> ( let () = $e$ in fun st -> st ) >> in { r_head = None; r_patt = l; r_class = c; r_branch = b; r_depr = d; } ] ] ; diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml index 7cbab56d44..cfc0e09a0c 100644 --- a/ide/ide_slave.ml +++ b/ide/ide_slave.ml @@ -217,7 +217,7 @@ let evars () = 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 all_goals, _, _, _, sigma = Proof.proof pfts in let exl = Evar.Map.bindings (Evd.undefined_map sigma) in let map_evar ev = { Interface.evar_info = string_of_ppcmds (pr_evar sigma ev); } in let el = List.map map_evar exl in @@ -227,7 +227,7 @@ let evars () = let hints () = try let pfts = Proof_global.give_me_the_proof () in - let { Evd.it = all_goals ; sigma = sigma } = Proof.V82.subgoals pfts in + let all_goals, _, _, _, sigma = Proof.proof pfts in match all_goals with | [] -> None | g :: _ -> diff --git a/interp/constrextern.ml b/interp/constrextern.ml index a92f974813..e1df24f717 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -184,18 +184,8 @@ let with_universes f = Flags.with_option print_universes f let with_meta_as_hole f = Flags.with_option print_meta_as_hole f let without_symbols f = Flags.with_option print_no_symbol f -(* XXX: Where to put this in the library? Util maybe? *) -let protect_ref r nf f x = - let old_ref = !r in - r := nf !r; - try let res = f x in r := old_ref; res - with reraise -> - let reraise = Backtrace.add_backtrace reraise in - r := old_ref; - Exninfo.iraise reraise - let without_specific_symbols l = - protect_ref inactive_notations_table + Flags.with_modified_ref inactive_notations_table (fun tbl -> IRuleSet.(union (of_list l) tbl)) (**********************************************************************) diff --git a/interp/constrintern.ml b/interp/constrintern.ml index ee3e11f8a5..977146b2fe 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -533,8 +533,9 @@ let traverse_binder (terms,_,_ as subst) avoid (renaming,env) = function | Name id -> try (* Binders bound in the notation are considered first-order objects *) - let _,na = coerce_to_name (fst (Id.Map.find id terms)) in - (renaming,{env with ids = Name.fold_right Id.Set.add na env.ids}), na + let _,na as locna = coerce_to_name (fst (Id.Map.find id terms)) in + let env = push_name_env Id.Map.empty (Variable,[],[],[]) env locna in + (renaming,env), na with Not_found -> (* Binders not bound in the notation do not capture variables *) (* outside the notation (i.e. in the substitution) *) @@ -746,7 +747,14 @@ let gvar (loc, id) us = match us with str " cannot have a universe instance") let intern_var genv (ltacvars,ntnvars) namedctx loc id us = - (* Is [id] an inductive type potentially with implicit *) + (* Is [id] a notation variable *) + if Id.Map.mem id ntnvars then + begin + if not (Id.Map.mem id genv.impls) then set_var_scope ?loc id true genv ntnvars; + gvar (loc,id) us, [], [], [] + end + else + (* Is [id] registered with implicit arguments *) try let ty,expl_impls,impls,argsc = Id.Map.find id genv.impls in let expl_impls = List.map @@ -759,12 +767,8 @@ let intern_var genv (ltacvars,ntnvars) namedctx loc id us = if Id.Set.mem id genv.ids || Id.Set.mem id ltacvars.ltac_vars then gvar (loc,id) us, [], [], [] - (* Is [id] a notation variable *) - else if Id.Map.mem id ntnvars - then - (set_var_scope ?loc id true genv ntnvars; gvar (loc,id) us, [], [], []) - (* Is [id] the special variable for recursive notations *) else if Id.equal id ldots_var + (* Is [id] the special variable for recursive notations? *) then if Id.Map.is_empty ntnvars then error_ldots_var ?loc else gvar (loc,id) us, [], [], [] diff --git a/lib/flags.ml b/lib/flags.ml index 323b5492dd..ddc8f84825 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -6,13 +6,17 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -let with_option o f x = - let old = !o in o:=true; - try let r = f x in if !o = true then o := old; r - with reraise -> - let reraise = Backtrace.add_backtrace reraise in - let () = o := old in - Exninfo.iraise reraise +let with_modified_ref r nf f x = + let old_ref = !r in r := nf !r; + try let res = f x in r := old_ref; res + with reraise -> + let reraise = Backtrace.add_backtrace reraise in + r := old_ref; + Exninfo.iraise reraise + +let with_option o f x = with_modified_ref o (fun _ -> true) f x +let without_option o f x = with_modified_ref o (fun _ -> false) f x +let with_extra_values o l f x = with_modified_ref o (fun ol -> ol@l) f x let with_options ol f x = let vl = List.map (!) ol in @@ -25,22 +29,6 @@ let with_options ol f x = let () = List.iter2 (:=) ol vl in Exninfo.iraise reraise -let without_option o f x = - let old = !o in o:=false; - try let r = f x in if !o = false then o := old; r - with reraise -> - let reraise = Backtrace.add_backtrace reraise in - let () = o := old in - Exninfo.iraise reraise - -let with_extra_values o l f x = - let old = !o in o:=old@l; - try let r = f x in o := old; r - with reraise -> - let reraise = Backtrace.add_backtrace reraise in - let () = o := old in - Exninfo.iraise reraise - let boot = ref false let record_aux_file = ref false diff --git a/lib/flags.mli b/lib/flags.mli index 0ff3e0a81d..c4afb83186 100644 --- a/lib/flags.mli +++ b/lib/flags.mli @@ -110,6 +110,15 @@ val warn : bool ref val make_warn : bool -> unit val if_warn : ('a -> unit) -> 'a -> unit +(** [with_modified_ref r nf f x] Temporarily modify a reference in the + call to [f x] . Be very careful with these functions, it is very + easy to fall in the typical problem with effects: + + with_modified_ref r nf f x y != with_modified_ref r nf (f x) y + +*) +val with_modified_ref : 'c ref -> ('c -> 'c) -> ('a -> 'b) -> 'a -> 'b + (** Temporarily activate an option (to activate option [o] on [f x y z], use [with_option o (f x y) z]) *) val with_option : bool ref -> ('a -> 'b) -> 'a -> 'b diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index e9102e9c82..61d207b953 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -550,11 +550,11 @@ type tcc_lemma_value = | Value of constr | Not_needed -(* We only "purify" on exceptions *) +(* We only "purify" on exceptions. XXX: What is this doing here? *) let funind_purify f x = - let st = Vernacentries.freeze_interp_state `No in + let st = Vernacstate.freeze_interp_state `No in try f x with e -> let e = CErrors.push e in - Vernacentries.unfreeze_interp_state st; + Vernacstate.unfreeze_interp_state st; Exninfo.iraise e diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 2fdc3bc37e..b8d41d539b 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -1225,8 +1225,8 @@ let whole_start (concl_tac:tactic) nb_args is_mes func input_type relation rec_a let get_current_subgoals_types () = let p = Proof_global.give_me_the_proof () in - let { Evd.it=sgs ; sigma=sigma } = Proof.V82.subgoals p in - sigma, List.map (Goal.V82.abstract_type sigma) sgs + let sgs,_,_,_,sigma = Proof.proof p in + sigma, List.map (Goal.V82.abstract_type sigma) sgs exception EmptySubgoals let build_and_l sigma l = diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index 38460c669f..3f885f8baa 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -84,6 +84,14 @@ type 'a extra_genarg_printer = (tolerability -> Val.t -> Pp.t) -> 'a -> Pp.t +let string_of_genarg_arg (ArgumentType arg) = + let rec aux : type a b c. (a, b, c) genarg_type -> string = function + | ListArg t -> aux t ^ "_list" + | OptArg t -> aux t ^ "_opt" + | PairArg (t1, t2) -> assert false (* No parsing/printing rule for it *) + | ExtraArg s -> ArgT.repr s in + aux arg + let keyword x = tag_keyword (str x) let primitive x = tag_primitive (str x) @@ -536,15 +544,24 @@ let pr_goal_selector ~toplevel s = let pr_funvar n = spc () ++ Name.print n - let pr_let_clause k pr (na,(bl,t)) = + let pr_let_clause k pr_gen pr_arg (na,(bl,t)) = + let pr = function + | TacGeneric arg -> + let name = string_of_genarg_arg (genarg_tag arg) in + if name = "unit" || name = "int" then + (* Hard-wired parsing rules *) + pr_gen arg + else + str name ++ str ":" ++ surround (pr_gen arg) + | _ -> pr_arg (TacArg (Loc.tag t)) in hov 0 (keyword k ++ spc () ++ pr_lname na ++ prlist pr_funvar bl ++ - str " :=" ++ brk (1,1) ++ pr (TacArg (Loc.tag t))) + str " :=" ++ brk (1,1) ++ pr t) - let pr_let_clauses recflag pr = function + let pr_let_clauses recflag pr_gen pr = function | hd::tl -> hv 0 - (pr_let_clause (if recflag then "let rec" else "let") pr hd ++ - prlist (fun t -> spc () ++ pr_let_clause "with" pr t) tl) + (pr_let_clause (if recflag then "let rec" else "let") pr_gen pr hd ++ + prlist (fun t -> spc () ++ pr_let_clause "with" pr_gen pr t) tl) | [] -> anomaly (Pp.str "LetIn must declare at least one binding.") let pr_seq_body pr tl = @@ -858,7 +875,7 @@ let pr_goal_selector ~toplevel s = let llc = List.map (fun (id,t) -> (id,extract_binders t)) llc in v 0 (hv 0 ( - pr_let_clauses recflag (pr_tac ltop) llc + pr_let_clauses recflag pr.pr_generic (pr_tac ltop) llc ++ spc () ++ keyword "in" ) ++ fnl () ++ pr_tac (llet,E) u), llet @@ -1003,7 +1020,7 @@ let pr_goal_selector ~toplevel s = | TacAtom (loc,t) -> pr_with_comments ?loc (hov 1 (pr_atom pr strip_prod_binders tag_atom t)), ltatom | TacArg(_,Tacexp e) -> - pr.pr_tactic (latom,E) e, latom + pr_tac inherited e, latom | TacArg(_,ConstrMayEval (ConstrTerm c)) -> keyword "constr:" ++ pr.pr_constr c, latom | TacArg(_,ConstrMayEval c) -> @@ -1250,8 +1267,8 @@ let () = ; Genprint.register_print0 wit_constr - Ppconstr.pr_constr_expr - (fun (c, _) -> Printer.pr_glob_constr c) + Ppconstr.pr_lconstr_expr + (fun (c, _) -> Printer.pr_lglob_constr c) (make_constr_printer Printer.pr_econstr_n_env) ; Genprint.register_print0 diff --git a/plugins/micromega/micromega.ml b/plugins/micromega/micromega.ml index 7da4a3b829..52c6ef983d 100644 --- a/plugins/micromega/micromega.ml +++ b/plugins/micromega/micromega.ml @@ -981,8 +981,8 @@ let rec or_cnf unsat deduce f f' = (** val and_cnf : 'a1 cnf -> 'a1 cnf -> 'a1 cnf **) -let and_cnf f1 f2 = - app f1 f2 +let and_cnf = + app (** val xcnf : ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> ('a1 -> 'a2 cnf) -> ('a1 @@ -1204,22 +1204,22 @@ type 't formula = { flhs : 't pExpr; fop : op2; frhs : 't pExpr } 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pExpr -> 'a1 pol **) -let norm cO cI cplus ctimes cminus copp ceqb = - norm_aux cO cI cplus ctimes cminus copp ceqb +let norm = + norm_aux (** val psub0 : 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pol -> 'a1 pol -> 'a1 pol **) -let psub0 cO cplus cminus copp ceqb = - psub cO cplus cminus copp ceqb +let psub0 = + psub (** val padd0 : 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pol -> 'a1 pol -> 'a1 pol **) -let padd0 cO cplus ceqb = - padd cO cplus ceqb +let padd0 = + padd (** val xnormalise : 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml index 3a2eac7e79..95de969260 100644 --- a/pretyping/cbv.ml +++ b/pretyping/cbv.ml @@ -208,25 +208,32 @@ and reify_value = function (* reduction under binders *) | STACK (n,v,stk) -> lift n (reify_stack (reify_value v) stk) | CBN(t,env) -> - t - (* map_constr_with_binders subs_lift (cbv_norm_term) env t *) - | LAM (n,ctxt,b,env) -> - List.fold_left (fun c (n,t) -> mkLambda (n, t, c)) b ctxt + apply_env env t + | LAM (k,ctxt,b,env) -> + apply_env env @@ + List.fold_left (fun c (n,t) -> + mkLambda (n, t, c)) b ctxt | FIXP ((lij,(names,lty,bds)),env,args) -> - mkApp - (mkFix (lij, - (names, - lty, - bds)), - Array.map reify_value args) + let fix = mkFix (lij, (names, lty, bds)) in + mkApp (apply_env env fix, Array.map reify_value args) | COFIXP ((j,(names,lty,bds)),env,args) -> - mkApp - (mkCoFix (j, - (names,lty,bds)), - Array.map reify_value args) + let cofix = mkCoFix (j, (names,lty,bds)) in + mkApp (apply_env env cofix, Array.map reify_value args) | CONSTR (c,args) -> mkApp(mkConstructU c, Array.map reify_value args) +and apply_env env t = + match kind t with + | Rel i -> + begin match expand_rel i env with + | Inl (k, v) -> + reify_value (shift_value k v) + | Inr (k,_) -> + mkRel k + end + | _ -> + map_with_binders subs_lift apply_env env t + (* The main recursive functions * * Go under applications and cases/projections (pushed in the stack), @@ -290,7 +297,10 @@ let rec norm_head info env t stack = | Evar ev -> (match evar_value info.infos.i_cache ev with Some c -> norm_head info env c stack - | None -> (VAL(0, t), stack)) + | None -> + let e, xs = ev in + let xs' = Array.map (apply_env env) xs in + (VAL(0, mkEvar (e,xs')), stack)) (* non-neutral cases *) | Lambda _ -> diff --git a/printing/printer.ml b/printing/printer.ml index 075b03b7d1..ba31b72d6c 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -828,7 +828,7 @@ let pr_open_subgoals ?(proof=Proof_global.give_me_the_proof ()) () = let pr_nth_open_subgoal n = let pf = Proof_global.give_me_the_proof () in - let { it=gls ; sigma=sigma } = Proof.V82.subgoals pf in + let gls,_,_,_,sigma = Proof.proof pf in pr_subgoal n sigma gls let pr_goal_by_id id = diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index 2d4aba17cb..c526ae000a 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -51,9 +51,8 @@ end let get_nth_V82_goal i = let p = Proof_global.give_me_the_proof () in - let { it=goals ; sigma = sigma; } = Proof.V82.subgoals p in - try - { it=(List.nth goals (i-1)) ; sigma=sigma; } + let goals,_,_,_,sigma = Proof.proof p in + try { it = List.nth goals (i-1) ; sigma } with Failure _ -> raise NoSuchGoal let get_goal_context_gen i = diff --git a/proofs/proof.ml b/proofs/proof.ml index e24d57f088..413b5fdd7e 100644 --- a/proofs/proof.ml +++ b/proofs/proof.ml @@ -163,6 +163,7 @@ let map_structured_proof pfts process_goal: 'a pre_goals = let rec unroll_focus pv = function | (_,_,ctx)::stk -> unroll_focus (Proofview.unfocus ctx pv) stk | [] -> pv + (* spiwack: a proof is considered completed even if its still focused, if the focus doesn't hide any goal. Unfocusing is handled in {!return}. *) @@ -391,10 +392,12 @@ let pr_proof p = (*** Compatibility layer with <=v8.2 ***) module V82 = struct let subgoals p = - Proofview.V82.goals p.proofview + let it, sigma = Proofview.proofview p.proofview in + Evd.{ it; sigma } let background_subgoals p = - Proofview.V82.goals (unroll_focus p.proofview p.focus_stack) + let it, sigma = Proofview.proofview (unroll_focus p.proofview p.focus_stack) in + Evd.{ it; sigma } let top_goal p = let { Evd.it=gls ; sigma=sigma; } = diff --git a/proofs/proof.mli b/proofs/proof.mli index 48aed8225e..5756d06b64 100644 --- a/proofs/proof.mli +++ b/proofs/proof.mli @@ -65,7 +65,6 @@ val map_structured_proof : proof -> (Evd.evar_map -> Goal.goal -> 'a) -> ('a pre (*** General proof functions ***) - val start : Evd.evar_map -> (Environ.env * EConstr.types) list -> proof val dependent_start : Proofview.telescope -> proof val initial_goals : proof -> (EConstr.constr * EConstr.types) list @@ -187,6 +186,7 @@ val pr_proof : proof -> Pp.t (*** Compatibility layer with <=v8.2 ***) module V82 : sig val subgoals : proof -> Goal.goal list Evd.sigma + [@@ocaml.deprecated "Use the first and fifth argument of [Proof.proof]"] (* All the subgoals of the proof, including those which are not focused. *) val background_subgoals : proof -> Goal.goal list Evd.sigma diff --git a/stm/proofBlockDelimiter.ml b/stm/proofBlockDelimiter.ml index 01b75e4964..77642946cd 100644 --- a/stm/proofBlockDelimiter.ml +++ b/stm/proofBlockDelimiter.ml @@ -46,7 +46,7 @@ let simple_goal sigma g gs = let is_focused_goal_simple ~doc id = match state_of_id ~doc id with | `Expired | `Error _ | `Valid None -> `Not - | `Valid (Some { Vernacentries.proof }) -> + | `Valid (Some { Vernacstate.proof }) -> let proof = Proof_global.proof_of_state proof in let focused, r1, r2, r3, sigma = Proof.proof proof in let rest = List.(flatten (map (fun (x,y) -> x @ y) r1)) @ r2 @ r3 in diff --git a/stm/stm.ml b/stm/stm.ml index b394c3a135..864fff9e0b 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -25,14 +25,14 @@ open Vernacexpr (* Protect against state changes *) let stm_purify f x = - let st = Vernacentries.freeze_interp_state `No in + let st = Vernacstate.freeze_interp_state `No in try let res = f x in - Vernacentries.unfreeze_interp_state st; + Vernacstate.unfreeze_interp_state st; res with e -> let e = CErrors.push e in - Vernacentries.unfreeze_interp_state st; + Vernacstate.unfreeze_interp_state st; Exninfo.iraise e let execution_error ?loc state_id msg = @@ -165,7 +165,7 @@ let summary_pstate = [ Evarutil.meta_counter_summary_name; type cached_state = | Empty | Error of Exninfo.iexn - | Valid of Vernacentries.interp_state + | Valid of Vernacstate.t type branch = Vcs_.Branch.t * branch_type Vcs_.branch_info type backup = { mine : branch; others : branch list } @@ -735,16 +735,16 @@ module State : sig val exn_on : Stateid.t -> valid:Stateid.t -> Exninfo.iexn -> Exninfo.iexn (* to send states across worker/master *) - val get_cached : Stateid.t -> Vernacentries.interp_state - val same_env : Vernacentries.interp_state -> Vernacentries.interp_state -> bool + val get_cached : Stateid.t -> Vernacstate.t + val same_env : Vernacstate.t -> Vernacstate.t -> bool type proof_part type partial_state = - [ `Full of Vernacentries.interp_state + [ `Full of Vernacstate.t | `ProofOnly of Stateid.t * proof_part ] - val proof_part_of_frozen : Vernacentries.interp_state -> proof_part + val proof_part_of_frozen : Vernacstate.t -> proof_part val assign : Stateid.t -> partial_state -> unit (* Handlers for initial state, prior to document creation. *) @@ -757,8 +757,6 @@ module State : sig end = struct (* {{{ *) - open Vernacentries - (* cur_id holds Stateid.dummy in case the last attempt to define a state * failed, so the global state may contain garbage *) let cur_id = ref Stateid.dummy @@ -768,15 +766,15 @@ end = struct (* {{{ *) Proof_global.state * Summary.frozen_bits (* only meta counters *) type partial_state = - [ `Full of Vernacentries.interp_state + [ `Full of Vernacstate.t | `ProofOnly of Stateid.t * proof_part ] - let proof_part_of_frozen { Vernacentries.proof; system } = + let proof_part_of_frozen { Vernacstate.proof; system } = proof, Summary.project_summary (States.summary_of_state system) summary_pstate let freeze marshallable id = - VCS.set_state id (Valid (Vernacentries.freeze_interp_state marshallable)) + VCS.set_state id (Valid (Vernacstate.freeze_interp_state marshallable)) let freeze_invalid id iexn = VCS.set_state id (Error iexn) @@ -800,7 +798,7 @@ end = struct (* {{{ *) let install_cached id = match VCS.get_info id with | { state = Valid s } -> - Vernacentries.unfreeze_interp_state s; + Vernacstate.unfreeze_interp_state s; cur_id := id | { state = Error ie } -> @@ -819,6 +817,7 @@ end = struct (* {{{ *) with VCS.Expired -> anomaly Pp.(str "not a cached state (expired).") let assign id what = + let open Vernacstate in if VCS.get_state id <> Empty then () else try match what with | `Full s -> @@ -826,7 +825,7 @@ end = struct (* {{{ *) try let prev = (VCS.visit id).next in if is_cached_and_valid prev - then { s with Vernacentries.proof = + then { s with proof = Proof_global.copy_terminators ~src:(get_cached prev).proof ~tgt:s.proof } else s @@ -854,7 +853,7 @@ end = struct (* {{{ *) execution_error ?loc id (iprint (e, info)); (e, Stateid.add info ~valid id) - let same_env { system = s1 } { system = s2 } = + let same_env { Vernacstate.system = s1 } { Vernacstate.system = s2 } = let s1 = States.summary_of_state s1 in let e1 = Summary.project_summary s1 [Global.global_env_summary_name] in let s2 = States.summary_of_state s2 in @@ -902,11 +901,11 @@ end = struct (* {{{ *) let init_state = ref None let register_root_state () = - init_state := Some (Vernacentries.freeze_interp_state `No) + init_state := Some (Vernacstate.freeze_interp_state `No) let restore_root_state () = cur_id := Stateid.dummy; - Vernacentries.unfreeze_interp_state (Option.get !init_state); + Vernacstate.unfreeze_interp_state (Option.get !init_state); end (* }}} *) @@ -1001,7 +1000,7 @@ end (* Wrapper for Vernacentries.interp to set the feedback id *) (* It is currently called 19 times, this number should be certainly reduced... *) -let stm_vernac_interp ?proof ?route id st { verbose; loc; expr } : Vernacentries.interp_state = +let stm_vernac_interp ?proof ?route id st { verbose; loc; expr } : Vernacstate.t = (* 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 *) @@ -1437,19 +1436,19 @@ end = struct (* {{{ *) * a bad fixpoint *) let fix_exn = Future.fix_exn_of future_proof in (* STATE: We use the current installed imperative state *) - let st = Vernacentries.freeze_interp_state `No in + let st = Vernacstate.freeze_interp_state `No in if not drop then begin let checked_proof = Future.chain future_proof (fun p -> (* Unfortunately close_future_proof and friends are not pure so we need to set the state manually here *) - Vernacentries.unfreeze_interp_state st; + Vernacstate.unfreeze_interp_state st; let pobject, _ = Proof_global.close_future_proof ~feedback_id:stop (Future.from_val ~fix_exn p) in let terminator = (* The one sent by master is an InvalidKey *) Lemmas.(standard_proof_terminator [] (mk_hook (fun _ _ -> ()))) in - let st = Vernacentries.freeze_interp_state `No in + let st = Vernacstate.freeze_interp_state `No in stm_vernac_interp stop ~proof:(pobject, terminator) st { verbose = false; loc; indentation = 0; strlen = 0; @@ -1457,7 +1456,7 @@ end = struct (* {{{ *) ignore(Future.join checked_proof); end; (* STATE: Restore the state XXX: handle exn *) - Vernacentries.unfreeze_interp_state st; + Vernacstate.unfreeze_interp_state st; RespBuiltProof(proof,time) with | e when CErrors.noncritical e || e = Stack_overflow -> @@ -1598,7 +1597,7 @@ end = struct (* {{{ *) * => takes nothing from the itermediate states. *) (* STATE We use the state resulting from reaching start. *) - let st = Vernacentries.freeze_interp_state `No in + let st = Vernacstate.freeze_interp_state `No in ignore(stm_vernac_interp stop ~proof st { verbose = false; loc; indentation = 0; strlen = 0; expr = (VernacEndProof (Proved (Opaque,None))) }); @@ -1855,7 +1854,7 @@ end = struct (* {{{ *) * => captures state id in a future closure, which will discard execution state but for the proof + univs. *) - let st = Vernacentries.freeze_interp_state `No in + let st = Vernacstate.freeze_interp_state `No in ignore(stm_vernac_interp r_state_fb st ast); let _,_,_,_,sigma = Proof.proof (Proof_global.give_me_the_proof ()) in match Evd.(evar_body (find sigma r_goal)) with @@ -1895,7 +1894,7 @@ end = struct (* {{{ *) | VernacRedirect (_,(_,e)) -> find ~time ~fail e | VernacFail e -> find ~time ~fail:true e | e -> e, time, fail in find ~time:false ~fail:false e in - let st = Vernacentries.freeze_interp_state `No in + let st = Vernacstate.freeze_interp_state `No in Vernacentries.with_fail st fail (fun () -> (if time then System.with_time !Flags.time else (fun x -> x)) (fun () -> ignore(TaskQueue.with_n_workers nworkers (fun queue -> @@ -1989,7 +1988,7 @@ end = struct (* {{{ *) VCS.print (); Reach.known_state ~cache:`No r_where; (* STATE *) - let st = Vernacentries.freeze_interp_state `No in + let st = Vernacstate.freeze_interp_state `No in try (* STATE SPEC: * - start: r_where @@ -2065,6 +2064,7 @@ let collect_proof keep cur hd brkind id = | id :: _ -> Names.Id.to_string id in let loc = (snd cur).loc in let rec is_defined_expr = function + | VernacEndProof (Proved (Transparent,_)) -> true | VernacTime (_, e) -> is_defined_expr e | VernacRedirect (_, (_, e)) -> is_defined_expr e | VernacTimeout (_, e) -> is_defined_expr e @@ -2203,7 +2203,7 @@ let known_state ?(redefine_qed=false) ~cache id = Proofview.give_up else Proofview.tclUNIT () end in match (VCS.get_info base_state).state with - | Valid { Vernacentries.proof } -> + | Valid { Vernacstate.proof } -> Proof_global.unfreeze proof; Proof_global.with_current_proof (fun _ p -> feedback ~id:id Feedback.AddedAxiom; @@ -2213,7 +2213,7 @@ let known_state ?(redefine_qed=false) ~cache id = * - end : maybe after recovery command. *) (* STATE: We use an updated state with proof *) - let st = Vernacentries.freeze_interp_state `No in + let st = Vernacstate.freeze_interp_state `No in Option.iter (fun expr -> ignore(stm_vernac_interp id st { verbose = true; loc = None; expr; indentation = 0; strlen = 0 } )) @@ -2293,7 +2293,7 @@ let known_state ?(redefine_qed=false) ~cache id = resilient_tactic id cblock (fun () -> reach view.next; (* State resulting from reach *) - let st = Vernacentries.freeze_interp_state `No in + let st = Vernacstate.freeze_interp_state `No in ignore(stm_vernac_interp id st x) ); if eff then update_global_env () @@ -2303,13 +2303,13 @@ let known_state ?(redefine_qed=false) ~cache id = | Flags.APon | Flags.APonLazy -> resilient_command reach view.next | Flags.APoff -> reach view.next); - let st = Vernacentries.freeze_interp_state `No in + let st = Vernacstate.freeze_interp_state `No in ignore(stm_vernac_interp id st x); if eff then update_global_env () ), (if eff then `Yes else cache), true | `Fork ((x,_,_,_), None) -> (fun () -> resilient_command reach view.next; - let st = Vernacentries.freeze_interp_state `No in + let st = Vernacstate.freeze_interp_state `No in ignore(stm_vernac_interp id st x); wall_clock_last_fork := Unix.gettimeofday () ), `Yes, true @@ -2318,7 +2318,7 @@ let known_state ?(redefine_qed=false) ~cache id = reach view.next; (try - let st = Vernacentries.freeze_interp_state `No in + let st = Vernacstate.freeze_interp_state `No in ignore(stm_vernac_interp id st x); with e when CErrors.noncritical e -> let (e, info) = CErrors.push e in @@ -2369,7 +2369,7 @@ let known_state ?(redefine_qed=false) ~cache id = Proof_global.close_future_proof ~feedback_id:id fp in if not delegate then ignore(Future.compute fp); reach view.next; - let st = Vernacentries.freeze_interp_state `No in + let st = Vernacstate.freeze_interp_state `No in ignore(stm_vernac_interp id ~proof st x); feedback ~id:id Incomplete | { VCS.kind = `Master }, _ -> assert false @@ -2378,7 +2378,7 @@ let known_state ?(redefine_qed=false) ~cache id = ), (if redefine_qed then `No else `Yes), true | `Sync (name, `Immediate) -> (fun () -> reach eop; - let st = Vernacentries.freeze_interp_state `No in + let st = Vernacstate.freeze_interp_state `No in ignore(stm_vernac_interp id st x); Proof_global.discard_all () ), `Yes, true @@ -2401,7 +2401,7 @@ let known_state ?(redefine_qed=false) ~cache id = if keep != VtKeepAsAxiom then reach view.next; let wall_clock2 = Unix.gettimeofday () in - let st = Vernacentries.freeze_interp_state `No in + let st = Vernacstate.freeze_interp_state `No in ignore(stm_vernac_interp id ?proof st x); let wall_clock3 = Unix.gettimeofday () in Aux_file.record_in_aux_at ?loc:x.loc "proof_check_time" @@ -2419,7 +2419,7 @@ let known_state ?(redefine_qed=false) ~cache id = aux (collect_proof keep (view.next, x) brname brinfo eop) | `Sideff (ReplayCommand x,_) -> (fun () -> reach view.next; - let st = Vernacentries.freeze_interp_state `No in + let st = Vernacstate.freeze_interp_state `No in ignore(stm_vernac_interp id st x); update_global_env () ), cache, true @@ -2688,7 +2688,7 @@ let process_transaction ?(newtip=Stateid.fresh ()) ?(part_of_script=true) | VtQuery (false,route), VtNow -> let query_sid = VCS.cur_tip () in (try - let st = Vernacentries.freeze_interp_state `No in + let st = Vernacstate.freeze_interp_state `No in ignore(stm_vernac_interp ~route query_sid st x) with e -> let e = CErrors.push e in @@ -2762,7 +2762,7 @@ let process_transaction ?(newtip=Stateid.fresh ()) ?(part_of_script=true) (* Side effect on all branches *) | VtUnknown, _ when expr = VernacToplevelControl Drop -> - let st = Vernacentries.freeze_interp_state `No in + let st = Vernacstate.freeze_interp_state `No in ignore(stm_vernac_interp (VCS.get_branch_pos head) st x); `Ok @@ -2790,7 +2790,7 @@ let process_transaction ?(newtip=Stateid.fresh ()) ?(part_of_script=true) VCS.checkout VCS.Branch.master; let mid = VCS.get_branch_pos VCS.Branch.master in let _st' = Reach.known_state ~cache:(VCS.is_interactive ()) mid in - let st = Vernacentries.freeze_interp_state `No in + let st = Vernacstate.freeze_interp_state `No in ignore(stm_vernac_interp id st x); (* Vernac x may or may not start a proof *) if not in_proof && Proof_global.there_are_pending_proofs () then diff --git a/stm/stm.mli b/stm/stm.mli index 31f4599d36..9fd35a0d38 100644 --- a/stm/stm.mli +++ b/stm/stm.mli @@ -220,7 +220,7 @@ val forward_feedback_hook : (Feedback.feedback -> unit) Hook.t val get_doc : Feedback.doc_id -> doc val state_of_id : doc:doc -> - Stateid.t -> [ `Valid of Vernacentries.interp_state option | `Expired | `Error of exn ] + Stateid.t -> [ `Valid of Vernacstate.t option | `Expired | `Error of exn ] (* Queries for backward compatibility *) val current_proof_depth : doc:doc -> int diff --git a/tactics/hints.ml b/tactics/hints.ml index c7c53b3930..99be1846cb 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -1467,11 +1467,11 @@ let pr_hint_term sigma cl = (* print all hints that apply to the concl of the current goal *) let pr_applicable_hint () = let pts = Proof_global.give_me_the_proof () in - let glss = Proof.V82.subgoals pts in - match glss.Evd.it with + let glss,_,_,_,sigma = Proof.proof pts in + match glss with | [] -> CErrors.user_err Pp.(str "No focused goal.") | g::_ -> - pr_hint_term glss.Evd.sigma (Goal.V82.concl glss.Evd.sigma g) + pr_hint_term sigma (Goal.V82.concl sigma g) let pp_hint_mode = function | ModeInput -> str"+" diff --git a/tactics/leminv.ml b/tactics/leminv.ml index cc9d98f6fe..62f3866de9 100644 --- a/tactics/leminv.ml +++ b/tactics/leminv.ml @@ -215,7 +215,7 @@ let inversion_scheme env sigma t sort dep_option inv_op = invEnv ~init:Context.Named.empty end in let avoid = ref Id.Set.empty in - let { sigma=sigma } = Proof.V82.subgoals pf in + let _,_,_,_,sigma = Proof.proof pf in let sigma = Evd.nf_constraints sigma in let rec fill_holes c = match EConstr.kind sigma c with diff --git a/test-suite/bugs/closed/5761.v b/test-suite/bugs/closed/5761.v new file mode 100644 index 0000000000..6f28d1981a --- /dev/null +++ b/test-suite/bugs/closed/5761.v @@ -0,0 +1,126 @@ +Set Primitive Projections. +Record mix := { a : nat ; b : a = a ; c : nat ; d : a = c ; e : nat ; f : nat }. +Ltac strip_args T ctor := + lazymatch type of ctor with + | context[T] + => match eval cbv beta in ctor with + | ?ctor _ => strip_args T ctor + | _ => ctor + end + end. +Ltac get_ctor T := + let full_ctor := constr:(ltac:(let x := fresh in intro x; econstructor; apply +x) : T -> T) in + let ctor := constr:(fun x : T => ltac:(let v := strip_args T (full_ctor x) in +exact v)) in + lazymatch ctor with + | fun _ => ?ctor => ctor + end. +Ltac uncurry_domain f := + lazymatch type of f with + | forall (a : ?A) (b : @ ?B a), _ + => uncurry_domain (fun ab : { a : A & B a } => f (projT1 ab) (projT2 ab)) + | _ => eval cbv beta in f + end. +Ltac get_of_sigma T := + let ctor := get_ctor T in + uncurry_domain ctor. +Ltac repeat_existT := + lazymatch goal with + | [ |- sigT _ ] => simple refine (existT _ _ _); [ repeat_existT | shelve ] + | _ => shelve + end. + Ltac prove_to_of_sigma_goal of_sigma := + let v := fresh "v" in + simple refine (exist _ _ (fun v => _ : id _ (of_sigma v) = v)); + try unfold of_sigma; + [ intro v; destruct v; repeat_existT + | cbv beta; + repeat match goal with + | [ |- context[projT2 ?k] ] + => let x := fresh "x" in + is_var k; + destruct k as [k x]; cbn [projT1 projT2] + end; + unfold id; reflexivity ]. +Ltac prove_to_of_sigma of_sigma := + constr:( + ltac:(prove_to_of_sigma_goal of_sigma) + : { to_sigma : _ | forall v, id to_sigma (of_sigma v) = v }). +Ltac get_to_sigma_gen of_sigma := + let v := prove_to_of_sigma of_sigma in + eval hnf in (proj1_sig v). +Ltac get_to_sigma T := + let of_sigma := get_of_sigma T in + get_to_sigma_gen of_sigma. +Definition to_sigma := ltac:(let v := get_to_sigma mix in exact v). +(* Error: +In nested Ltac calls to "get_to_sigma", "get_to_sigma_gen", +"prove_to_of_sigma", +"(_ : {to_sigma : _ | forall v, id to_sigma (of_sigma v) = v})" (with +of_sigma:=fun + ab : {_ + : {_ + : {ab : {_ : {a : nat & a = a} & nat} & + projT1 (projT1 ab) = projT2 ab} & nat} & nat} => + {| + a := projT1 (projT1 (projT1 (projT1 (projT1 ab)))); + b := projT2 (projT1 (projT1 (projT1 (projT1 ab)))); + c := projT2 (projT1 (projT1 (projT1 ab))); + d := projT2 (projT1 (projT1 ab)); + e := projT2 (projT1 ab); + f := projT2 ab |}) and "prove_to_of_sigma_goal", last call failed. +Anomaly "Uncaught exception Not_found." Please report at +http://coq.inria.fr/bugs/. +frame @ file "toplevel/coqtop.ml", line 640, characters 6-22 +frame @ file "list.ml", line 73, characters 12-15 +frame @ file "toplevel/vernac.ml", line 344, characters 2-13 +frame @ file "toplevel/vernac.ml", line 308, characters 14-75 +raise @ file "lib/exninfo.ml", line 63, characters 8-15 +frame @ file "lib/flags.ml", line 141, characters 19-40 +raise @ file "lib/exninfo.ml", line 63, characters 8-15 +frame @ file "lib/flags.ml", line 11, characters 15-18 +raise @ file "lib/exninfo.ml", line 63, characters 8-15 +frame @ file "toplevel/vernac.ml", line 167, characters 6-16 +frame @ file "toplevel/vernac.ml", line 151, characters 26-39 +frame @ file "stm/stm.ml", line 2365, characters 2-35 +raise @ file "lib/exninfo.ml", line 63, characters 8-15 +frame @ file "stm/stm.ml", line 2355, characters 4-48 +frame @ file "stm/stm.ml", line 2321, characters 4-100 +raise @ file "lib/exninfo.ml", line 63, characters 8-15 +frame @ file "stm/stm.ml", line 832, characters 6-10 +frame @ file "stm/stm.ml", line 2206, characters 10-32 +raise @ file "lib/exninfo.ml", line 63, characters 8-15 +frame @ file "stm/stm.ml", line 975, characters 8-81 +raise @ file "lib/exninfo.ml", line 63, characters 8-15 +frame @ file "vernac/vernacentries.ml", line 2216, characters 10-389 +frame @ file "lib/flags.ml", line 141, characters 19-40 +raise @ file "lib/exninfo.ml", line 63, characters 8-15 +frame @ file "lib/flags.ml", line 11, characters 15-18 +frame @ file "vernac/command.ml", line 150, characters 4-56 +frame @ file "interp/constrintern.ml", line 2046, characters 2-73 +frame @ file "pretyping/pretyping.ml", line 1194, characters 19-77 +frame @ file "pretyping/pretyping.ml", line 1155, characters 8-72 +frame @ file "pretyping/pretyping.ml", line 628, characters 23-65 +frame @ file "plugins/ltac/tacinterp.ml", line 2095, characters 21-61 +frame @ file "proofs/pfedit.ml", line 178, characters 6-22 +raise @ file "lib/exninfo.ml", line 63, characters 8-15 +frame @ file "proofs/pfedit.ml", line 174, characters 8-36 +frame @ file "proofs/proof.ml", line 351, characters 4-30 +raise @ file "lib/exninfo.ml", line 63, characters 8-15 +frame @ file "engine/proofview.ml", line 1222, characters 8-12 +frame @ file "plugins/ltac/tacinterp.ml", line 2020, characters 19-36 +frame @ file "plugins/ltac/tacinterp.ml", line 618, characters 4-70 +raise @ file "lib/exninfo.ml", line 63, characters 8-15 +frame @ file "plugins/ltac/tacinterp.ml", line 214, characters 6-9 +frame @ file "pretyping/pretyping.ml", line 1198, characters 19-62 +frame @ file "pretyping/pretyping.ml", line 1155, characters 8-72 +raise @ unknown +frame @ file "pretyping/pretyping.ml", line 628, characters 23-65 +frame @ file "plugins/ltac/tacinterp.ml", line 2095, characters 21-61 +frame @ file "proofs/pfedit.ml", line 178, characters 6-22 +raise @ file "lib/exninfo.ml", line 63, characters 8-15 +frame @ file "proofs/pfedit.ml", line 174, characters 8-36 +frame @ file "proofs/proof.ml", line 351, characters 4-30 +raise @ file "lib/exninfo.ml", line 63, characters 8-15 + *) diff --git a/test-suite/bugs/closed/5762.v b/test-suite/bugs/closed/5762.v index edd5c8d73d..55d36bd722 100644 --- a/test-suite/bugs/closed/5762.v +++ b/test-suite/bugs/closed/5762.v @@ -26,3 +26,9 @@ Reserved Notation "%% a" (at level 70). Record R := {g : forall {A} (a:A), a=a where "%% x" := (g x); k : %% 0 = eq_refl}. + +(* An extra example *) + +Module A. +Inductive I {A:Type} := C : # 0 -> I where "# I" := (I = I) : I_scope. +End A. diff --git a/test-suite/bugs/closed/gh6165.v b/test-suite/bugs/closed/gh6165.v new file mode 100644 index 0000000000..b87a7caaf2 --- /dev/null +++ b/test-suite/bugs/closed/gh6165.v @@ -0,0 +1,5 @@ +(* -*- mode: coq; coq-prog-args: ("-quick") -*- *) + +Goal True. + abstract exact I. +Timeout 1 Defined. diff --git a/test-suite/coq-makefile/timing/run.sh b/test-suite/coq-makefile/timing/run.sh index 7e0baaa8f2..2428da7316 100755 --- a/test-suite/coq-makefile/timing/run.sh +++ b/test-suite/coq-makefile/timing/run.sh @@ -41,6 +41,9 @@ for ext in "" .desired; do done done for file in time-of-build-before.log time-of-build-after.log time-of-build-both.log; do + echo "cat $file" + cat "$file" + echo diff -u $file.desired.processed $file.processed || exit $? done @@ -56,6 +59,13 @@ make all TIMING=after -j2 || exit $? find ../per-file-before/ -name "*.before-timing" -exec 'cp' '{}' './' ';' make all.timing.diff -j2 || exit $? +echo "cat A.v.before-timing" +cat A.v.before-timing +echo +echo "cat A.v.after-timing" +cat A.v.after-timing +echo +echo "cat A.v.timing.diff" cat A.v.timing.diff echo diff --git a/test-suite/coqdoc/links.html.out b/test-suite/coqdoc/links.html.out index 70cbe50657..5e4b676c2f 100644 --- a/test-suite/coqdoc/links.html.out +++ b/test-suite/coqdoc/links.html.out @@ -76,7 +76,7 @@ Various checks for coqdoc <br/> <span class="id" title="keyword">Inductive</span> <a name="eq"><span class="id" title="inductive">eq</span></a> (<span class="id" title="var">A</span>:<span class="id" title="keyword">Type</span>) (<span class="id" title="var">x</span>:<a class="idref" href="Coqdoc.links.html#A"><span class="id" title="variable">A</span></a>) : <span class="id" title="var">A</span> <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <span class="id" title="keyword">Prop</span> := <a name="eq_refl"><span class="id" title="constructor">eq_refl</span></a> : <a class="idref" href="Coqdoc.links.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Coqdoc.links.html#8f9364556521ebb498093f28eea2240f"><span class="id" title="notation">=</span></a> <a class="idref" href="Coqdoc.links.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Coqdoc.links.html#8f9364556521ebb498093f28eea2240f"><span class="id" title="notation">:></span></a><a class="idref" href="Coqdoc.links.html#A"><span class="id" title="variable">A</span></a><br/> <br/> -<span class="id" title="keyword">where</span> <a name="8f9364556521ebb498093f28eea2240f"><span class="id" title="notation">"</span></a>x = y :> A" := (@<a class="idref" href="Coqdoc.links.html#eq"><span class="id" title="inductive">eq</span></a> <a class="idref" href="Coqdoc.links.html#A"><span class="id" title="variable">A</span></a> <a class="idref" href="Coqdoc.links.html#x"><span class="id" title="variable">x</span></a> <span class="id" title="var">y</span>) : <span class="id" title="var">type_scope</span>.<br/> +<span class="id" title="keyword">where</span> <a name="8f9364556521ebb498093f28eea2240f"><span class="id" title="notation">"</span></a>x = y :> A" := (@<a class="idref" href="Coqdoc.links.html#eq"><span class="id" title="inductive">eq</span></a> <span class="id" title="var">A</span> <span class="id" title="var">x</span> <span class="id" title="var">y</span>) : <span class="id" title="var">type_scope</span>.<br/> <br/> <span class="id" title="keyword">Definition</span> <a name="eq0"><span class="id" title="definition">eq0</span></a> := 0 <a class="idref" href="Coqdoc.links.html#8f9364556521ebb498093f28eea2240f"><span class="id" title="notation">=</span></a> 0 <a class="idref" href="Coqdoc.links.html#8f9364556521ebb498093f28eea2240f"><span class="id" title="notation">:></span></a> <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>.<br/> diff --git a/test-suite/coqdoc/links.tex.out b/test-suite/coqdoc/links.tex.out index 7d93189ae2..f42db99dc2 100644 --- a/test-suite/coqdoc/links.tex.out +++ b/test-suite/coqdoc/links.tex.out @@ -69,7 +69,7 @@ Various checks for coqdoc \coqdocnoindent \coqdoceol \coqdocnoindent -\coqdockw{where} \coqdef{Coqdoc.links.:type scope:x '=' x ':>' x}{"}{"}x = y :> A" := (@\coqref{Coqdoc.links.eq}{\coqdocinductive{eq}} \coqdocvariable{A} \coqdocvariable{x} \coqdocvar{y}) : \coqdocvar{type\_scope}.\coqdoceol +\coqdockw{where} \coqdef{Coqdoc.links.:type scope:x '=' x ':>' x}{"}{"}x = y :> A" := (@\coqref{Coqdoc.links.eq}{\coqdocinductive{eq}} \coqdocvar{A} \coqdocvar{x} \coqdocvar{y}) : \coqdocvar{type\_scope}.\coqdoceol \coqdocemptyline \coqdocnoindent \coqdockw{Definition} \coqdef{Coqdoc.links.eq0}{eq0}{\coqdocdefinition{eq0}} := 0 \coqref{Coqdoc.links.:type scope:x '=' x ':>' x}{\coqdocnotation{=}} 0 \coqref{Coqdoc.links.:type scope:x '=' x ':>' x}{\coqdocnotation{:>}} \coqexternalref{nat}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocinductive{nat}}.\coqdoceol diff --git a/test-suite/output/ltac.out b/test-suite/output/ltac.out index 35c3057d84..c5d58ec1ec 100644 --- a/test-suite/output/ltac.out +++ b/test-suite/output/ltac.out @@ -31,3 +31,10 @@ nat nat 0 0 +Ltac foo := + let x := intros ** in + let y := intros -> in + let v := constr:(nil) in + let w := () in + let z := 1 in + pose v diff --git a/test-suite/output/ltac.v b/test-suite/output/ltac.v index 76c37625aa..6adbe95dd5 100644 --- a/test-suite/output/ltac.v +++ b/test-suite/output/ltac.v @@ -57,3 +57,14 @@ match goal with |- ?x*?y => idtac x end. match goal with H: context [?x*?y] |- _ => idtac x end. match goal with |- context [?x*?y] => idtac x end. Abort. + +(* Check printing of let in Ltac and Tactic Notation *) + +Ltac foo := + let x := intros in + let y := intros -> in + let v := constr:(@ nil True) in + let w := () in + let z := 1 in + pose v. +Print Ltac foo. diff --git a/test-suite/success/Notations2.v b/test-suite/success/Notations2.v index 9505a56e3f..e86b3edb83 100644 --- a/test-suite/success/Notations2.v +++ b/test-suite/success/Notations2.v @@ -90,3 +90,9 @@ Check fun A (x :prod' bool A) => match x with #### 0 y 0 => 2 | _ => 1 end. Notation "##### x" := (pair' x) (at level 0, x at level 1). Check ##### 0 _ 0%bool 0%bool : prod' bool bool. Check fun A (x :prod' bool A) => match x with ##### 0 _ y 0%bool => 2 | _ => 1 end. + +(* 10. Check computation of binding variable through other notations *) +(* i should be detected as binding variable and the scopes not being checked *) + +Notation "'FUNNAT' i => t" := (fun i : nat => i = t) (at level 200). +Notation "'Funnat' i => t" := (FUNNAT i => t + i%nat) (at level 200). diff --git a/tools/coq-inferior.el b/tools/inferior-coq.el index b79d97d66e..b79d97d66e 100644 --- a/tools/coq-inferior.el +++ b/tools/inferior-coq.el diff --git a/vernac/command.ml b/vernac/command.ml index 0232d7376c..fd0027c408 100644 --- a/vernac/command.ml +++ b/vernac/command.ml @@ -550,12 +550,13 @@ let interp_mutual_inductive (paramsl,indl) notations cum poly prv finite = lift_implicits (Context.Rel.nhyps ctx_params) impls) arities in let arities = List.map pi1 arities and aritypoly = List.map pi2 arities in let impls = compute_internalization_env env0 ~impls (Inductive (params,true)) indnames fullarities indimpls in + let ntn_impls = compute_internalization_env env0 (Inductive (params,true)) indnames fullarities indimpls in let mldatas = List.map2 (mk_mltype_data evdref env_params params) arities indnames in let constructors = Metasyntax.with_syntax_protection (fun () -> (* Temporary declaration of notations and scopes *) - List.iter (Metasyntax.set_notation_for_interpretation env_params impls) notations; + List.iter (Metasyntax.set_notation_for_interpretation env_params ntn_impls) notations; (* Interpret the constructor types *) List.map3 (interp_cstrs env_ar_params evdref impls) mldatas arities indl) () in diff --git a/vernac/vernac.mllib b/vernac/vernac.mllib index 850902d6ba..8673155e28 100644 --- a/vernac/vernac.mllib +++ b/vernac/vernac.mllib @@ -15,6 +15,7 @@ Command Classes Record Assumptions +Vernacstate Vernacinterp Mltop Topfmt diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 5bcb3b1e15..c00b107cfe 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -62,14 +62,12 @@ let show_proof () = let show_top_evars () = (* spiwack: new as of Feb. 2010: shows goal evars in addition to non-goal evars. *) let pfts = Proof_global.give_me_the_proof () in - let gls = Proof.V82.subgoals pfts in - let sigma = gls.Evd.sigma in + let gls,_,_,_,sigma = Proof.proof pfts in Feedback.msg_notice (pr_evars_int sigma 1 (Evd.undefined_map sigma)) let show_universes () = let pfts = Proof_global.give_me_the_proof () in - let gls = Proof.V82.subgoals pfts in - let sigma = gls.Evd.sigma in + let gls,_,_,_,sigma = Proof.proof pfts in let ctx = Evd.universe_context_set (Evd.nf_constraints sigma) in Feedback.msg_notice (Termops.pr_evar_universe_context (Evd.evar_universe_context sigma)); Feedback.msg_notice (str"Normalized constraints: " ++ Univ.pr_universe_context_set (Termops.pr_evd_level sigma) ctx) @@ -78,7 +76,7 @@ let show_universes () = let show_intro all = let open EConstr in let pf = Proof_global.give_me_the_proof() in - let {Evd.it=gls ; sigma=sigma; } = Proof.V82.subgoals pf in + let gls,_,_,_,sigma = Proof.proof pf in if not (List.is_empty gls) then begin let gl = {Evd.it=List.hd gls ; sigma = sigma; } in let l,_= decompose_prod_assum sigma (Termops.strip_outer_cast sigma (pf_concl gl)) in @@ -1601,7 +1599,7 @@ let vernac_global_check c = let get_nth_goal n = let pf = Proof_global.give_me_the_proof() in - let {Evd.it=gls ; sigma=sigma; } = Proof.V82.subgoals pf in + let gls,_,_,_,sigma = Proof.proof pf in let gl = {Evd.it=List.nth gls (n-1) ; sigma = sigma; } in gl @@ -1909,7 +1907,7 @@ let vernac_load interp fname = * is the outdated/deprecated "Local" attribute of some vernacular commands * still parsed as the obsolete_locality grammar entry for retrocompatibility. * loc is the Loc.t of the vernacular command being interpreted. *) -let interp ?proof ?loc locality poly c = +let interp ?proof ?loc locality poly st c = vernac_pperr_endline (fun () -> str "interpreting: " ++ Ppvernac.pr_vernac c); match c with (* The below vernac are candidates for removal from the main type @@ -2069,7 +2067,10 @@ let interp ?proof ?loc locality poly c = | VernacProofMode mn -> Proof_global.set_proof_mode mn [@ocaml.warning "-3"] (* Extensions *) - | VernacExtend (opn,args) -> Vernacinterp.call ?locality ?loc (opn,args) + | VernacExtend (opn,args) -> + (* XXX: Here we are returning the state! :) *) + let _st : Vernacstate.t = Vernacinterp.call ?locality ?loc (opn,args) st in + () (* Vernaculars that take a locality flag *) let check_vernac_supports_locality c l = @@ -2147,28 +2148,6 @@ let locate_if_not_already ?loc (e, info) = exception HasNotFailed exception HasFailed of Pp.t -type interp_state = { (* TODO: inline records in OCaml 4.03 *) - system : States.state; (* summary + libstack *) - proof : Proof_global.state; (* proof state *) - shallow : bool (* is the state trimmed down (libstack) *) -} - -let s_cache = ref (States.freeze ~marshallable:`No) -let s_proof = ref (Proof_global.freeze ~marshallable:`No) - -let invalidate_cache () = - s_cache := Obj.magic 0; - s_proof := Obj.magic 0 - -let freeze_interp_state marshallable = - { system = (s_cache := States.freeze ~marshallable; !s_cache); - proof = (s_proof := Proof_global.freeze ~marshallable; !s_proof); - shallow = marshallable = `Shallow } - -let unfreeze_interp_state { system; proof } = - if (!s_cache != system) then (s_cache := system; States.unfreeze system); - if (!s_proof != proof) then (s_proof := proof; Proof_global.unfreeze proof) - (* XXX STATE: this type hints that restoring the state should be the caller's responsibility *) let with_fail st b f = @@ -2187,8 +2166,8 @@ let with_fail st b f = (ExplainErr.process_vernac_interp_error ~allow_uncaught:false e))) with e when CErrors.noncritical e -> (* Restore the previous state XXX Careful here with the cache! *) - invalidate_cache (); - unfreeze_interp_state st; + Vernacstate.invalidate_cache (); + Vernacstate.unfreeze_interp_state st; let (e, _) = CErrors.push e in match e with | HasNotFailed -> @@ -2230,8 +2209,8 @@ let interp ?(verbosely=true) ?proof st (loc,c) = try vernac_timeout begin fun () -> if verbosely - then Flags.verbosely (interp ?proof ?loc locality poly) c - else Flags.silently (interp ?proof ?loc locality poly) c; + then Flags.verbosely (interp ?proof ?loc locality poly st) c + else Flags.silently (interp ?proof ?loc locality poly st) c; if orig_program_mode || not !Flags.program_mode || isprogcmd then Flags.program_mode := orig_program_mode; ignore (Flags.use_polymorphic_flag ()) @@ -2252,7 +2231,9 @@ let interp ?(verbosely=true) ?proof st (loc,c) = if verbosely then Flags.verbosely (aux false) c else aux false c +(* XXX: There is a bug here in case of an exception, see @gares + comments on the PR *) let interp ?verbosely ?proof st cmd = - unfreeze_interp_state st; + Vernacstate.unfreeze_interp_state st; interp ?verbosely ?proof st cmd; - freeze_interp_state `No + Vernacstate.freeze_interp_state `No diff --git a/vernac/vernacentries.mli b/vernac/vernacentries.mli index 56635c8011..67001bc24e 100644 --- a/vernac/vernacentries.mli +++ b/vernac/vernacentries.mli @@ -14,21 +14,11 @@ val dump_global : Libnames.reference or_by_notation -> unit val vernac_require : Libnames.reference option -> bool option -> Libnames.reference list -> unit -type interp_state = { (* TODO: inline records in OCaml 4.03 *) - system : States.state; (* summary + libstack *) - proof : Proof_global.state; (* proof state *) - shallow : bool (* is the state trimmed down (libstack) *) -} - -val freeze_interp_state : Summary.marshallable -> interp_state -val unfreeze_interp_state : interp_state -> unit - (** The main interpretation function of vernacular expressions *) val interp : ?verbosely:bool -> ?proof:Proof_global.closed_proof -> - interp_state -> - Vernacexpr.vernac_expr Loc.located -> interp_state + Vernacstate.t -> Vernacexpr.vernac_expr Loc.located -> Vernacstate.t (** Prepare a "match" template for a given inductive type. For each branch of the match, we list the constructor name @@ -40,7 +30,7 @@ val make_cases : string -> string list list (* XXX STATE: this type hints that restoring the state should be the caller's responsibility *) -val with_fail : interp_state -> bool -> (unit -> unit) -> unit +val with_fail : Vernacstate.t -> bool -> (unit -> unit) -> unit val command_focus : unit Proof.focus_kind diff --git a/vernac/vernacinterp.ml b/vernac/vernacinterp.ml index 41fee6bd08..1d024386e2 100644 --- a/vernac/vernacinterp.ml +++ b/vernac/vernacinterp.ml @@ -11,11 +11,12 @@ open Pp open CErrors type deprecation = bool -type vernac_command = Genarg.raw_generic_argument list -> Loc.t option -> unit +type vernac_command = Genarg.raw_generic_argument list -> Loc.t option -> + Vernacstate.t -> Vernacstate.t (* Table of vernac entries *) let vernac_tab = - (Hashtbl.create 51 : + (Hashtbl.create 211 : (Vernacexpr.extend_name, deprecation * vernac_command) Hashtbl.t) let vinterp_add depr s f = @@ -66,8 +67,9 @@ let call ?locality ?loc (opn,converted_args) = let hunk = callback converted_args in phase := "Executing command"; Locality.LocalityFixme.set locality; - hunk loc; - Locality.LocalityFixme.assert_consumed() + let res = hunk loc in + Locality.LocalityFixme.assert_consumed (); + res with | Drop -> raise Drop | reraise -> diff --git a/vernac/vernacinterp.mli b/vernac/vernacinterp.mli index 84370fdc29..1c66b1c045 100644 --- a/vernac/vernacinterp.mli +++ b/vernac/vernacinterp.mli @@ -9,12 +9,16 @@ (** Interpretation of extended vernac phrases. *) type deprecation = bool -type vernac_command = Genarg.raw_generic_argument list -> Loc.t option -> unit -val vinterp_add : deprecation -> Vernacexpr.extend_name -> - vernac_command -> unit -val overwriting_vinterp_add : - Vernacexpr.extend_name -> vernac_command -> unit +type vernac_command = Genarg.raw_generic_argument list -> Loc.t option -> + Vernacstate.t -> Vernacstate.t + +val vinterp_add : deprecation -> Vernacexpr.extend_name -> vernac_command -> unit + +val overwriting_vinterp_add : Vernacexpr.extend_name -> vernac_command -> unit val vinterp_init : unit -> unit -val call : ?locality:bool -> ?loc:Loc.t -> Vernacexpr.extend_name * Genarg.raw_generic_argument list -> unit + +val call : ?locality:bool -> ?loc:Loc.t -> + Vernacexpr.extend_name * Genarg.raw_generic_argument list -> + Vernacstate.t -> Vernacstate.t diff --git a/vernac/vernacstate.ml b/vernac/vernacstate.ml new file mode 100644 index 0000000000..9802a03cad --- /dev/null +++ b/vernac/vernacstate.ml @@ -0,0 +1,29 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +type t = { (* TODO: inline records in OCaml 4.03 *) + system : States.state; (* summary + libstack *) + proof : Proof_global.state; (* proof state *) + shallow : bool (* is the state trimmed down (libstack) *) +} + +let s_cache = ref (States.freeze ~marshallable:`No) +let s_proof = ref (Proof_global.freeze ~marshallable:`No) + +let invalidate_cache () = + s_cache := Obj.magic 0; + s_proof := Obj.magic 0 + +let freeze_interp_state marshallable = + { system = (s_cache := States.freeze ~marshallable; !s_cache); + proof = (s_proof := Proof_global.freeze ~marshallable; !s_proof); + shallow = marshallable = `Shallow } + +let unfreeze_interp_state { system; proof } = + if (!s_cache != system) then (s_cache := system; States.unfreeze system); + if (!s_proof != proof) then (s_proof := proof; Proof_global.unfreeze proof) diff --git a/vernac/vernacstate.mli b/vernac/vernacstate.mli new file mode 100644 index 0000000000..63a5b3b1eb --- /dev/null +++ b/vernac/vernacstate.mli @@ -0,0 +1,19 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +type t = { (* TODO: inline records in OCaml 4.03 *) + system : States.state; (* summary + libstack *) + proof : Proof_global.state; (* proof state *) + shallow : bool (* is the state trimmed down (libstack) *) +} + +val freeze_interp_state : Summary.marshallable -> t +val unfreeze_interp_state : t -> unit + +(* WARNING: Do not use, it will go away in future releases *) +val invalidate_cache : unit -> unit |