diff options
59 files changed, 403 insertions, 420 deletions
diff --git a/dev/ci/user-overlays/08893-herbelin-master+moving-evars-of-term-on-econstr.sh b/dev/ci/user-overlays/08893-herbelin-master+moving-evars-of-term-on-econstr.sh new file mode 100644 index 0000000000..dc39ea5ef0 --- /dev/null +++ b/dev/ci/user-overlays/08893-herbelin-master+moving-evars-of-term-on-econstr.sh @@ -0,0 +1,7 @@ +if [ "$CI_PULL_REQUEST" = "8893" ] || [ "$CI_BRANCH" = "master+moving-evars-of-term-on-econstr" ]; then + + equations_CI_BRANCH=master+fix-evars_of_term-pr8893 + equations_CI_REF=master+fix-evars_of_term-pr8893 + equations_CI_GITURL=https://github.com/herbelin/Coq-Equations + +fi diff --git a/dev/ci/user-overlays/10125-SkySkimmer-run_tactic_gen.sh b/dev/ci/user-overlays/10125-SkySkimmer-run_tactic_gen.sh new file mode 100644 index 0000000000..4032b1c6b5 --- /dev/null +++ b/dev/ci/user-overlays/10125-SkySkimmer-run_tactic_gen.sh @@ -0,0 +1,6 @@ +if [ "$CI_PULL_REQUEST" = "10125" ] || [ "$CI_BRANCH" = "run_tactic_gen" ]; then + + paramcoq_CI_REF=run_tactic_gen + paramcoq_CI_GITURL=https://github.com/SkySkimmer/paramcoq + +fi diff --git a/dev/ci/user-overlays/10135-maximedenes-detype-anonymous.sh b/dev/ci/user-overlays/10135-maximedenes-detype-anonymous.sh new file mode 100644 index 0000000000..bc8aa33565 --- /dev/null +++ b/dev/ci/user-overlays/10135-maximedenes-detype-anonymous.sh @@ -0,0 +1,6 @@ +if [ "$CI_PULL_REQUEST" = "10135" ] || [ "$CI_BRANCH" = "detype-anonymous" ]; then + + unicoq_CI_REF=detype-anonymous + unicoq_CI_GITURL=https://github.com/maximedenes/unicoq + +fi diff --git a/dev/include_printers b/dev/include_printers index 90088e40bf..d077075eeb 100644 --- a/dev/include_printers +++ b/dev/include_printers @@ -11,6 +11,7 @@ #install_printer (* universes *) ppuniverses;; #install_printer (* univ level *) ppuni_level;; #install_printer (* univ context *) ppuniverse_context;; +#install_printer (* univ context *) ppaucontext;; #install_printer (* univ context future *) ppuniverse_context_future;; #install_printer (* univ context set *) ppuniverse_context_set;; #install_printer (* univ set *) ppuniverse_set;; diff --git a/dev/top_printers.dbg b/dev/top_printers.dbg index a6ecec7e33..82f2e79549 100644 --- a/dev/top_printers.dbg +++ b/dev/top_printers.dbg @@ -62,6 +62,7 @@ install_printer Top_printers.ppuni_level install_printer Top_printers.ppuniverse_set install_printer Top_printers.ppuniverse_instance install_printer Top_printers.ppuniverse_context +install_printer Top_printers.ppaucontext install_printer Top_printers.ppuniverse_context_set install_printer Top_printers.ppuniverse_subst install_printer Top_printers.ppuniverse_opt_subst diff --git a/dev/top_printers.ml b/dev/top_printers.ml index 816316487c..2859b56cbe 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -27,7 +27,6 @@ open Clenv let _ = Detyping.print_evar_arguments := true let _ = Detyping.print_universes := true let _ = Goptions.set_bool_option_value ["Printing";"Matching"] false -let _ = Detyping.set_detype_anonymous (fun ?loc _ -> raise Not_found) (* std_ppcmds *) let pp x = Pp.pp_with !Topfmt.std_ft x @@ -236,6 +235,15 @@ let ppnamedcontextval e = let sigma = Evd.from_env env in pp (pr_named_context env sigma (named_context_of_val e)) +let ppaucontext auctx = + let nas = AUContext.names auctx in + let prlev l = match Level.var_index l with + | Some n -> Name.print nas.(n) + | None -> prlev l + in + pp (pr_universe_context prlev (AUContext.repr auctx)) + + let ppenv e = pp (str "[" ++ pr_named_context_of e Evd.empty ++ str "]" ++ spc() ++ str "[" ++ pr_rel_context e Evd.empty (rel_context e) ++ str "]") diff --git a/dev/top_printers.mli b/dev/top_printers.mli index cb32d2294c..2aa1808322 100644 --- a/dev/top_printers.mli +++ b/dev/top_printers.mli @@ -137,6 +137,7 @@ val prlev : Univ.Level.t -> Pp.t (* with global names (does this work?) *) val ppuniverse_set : Univ.LSet.t -> unit val ppuniverse_instance : Univ.Instance.t -> unit val ppuniverse_context : Univ.UContext.t -> unit +val ppaucontext : Univ.AUContext.t -> unit val ppuniverse_context_set : Univ.ContextSet.t -> unit val ppuniverse_subst : Univ.universe_subst -> unit val ppuniverse_opt_subst : UnivSubst.universe_opt_subst -> unit diff --git a/doc/changelog/03-notations/10061-print-custom-grammar.rst b/doc/changelog/03-notations/10061-print-custom-grammar.rst deleted file mode 100644 index 8786c7ce6b..0000000000 --- a/doc/changelog/03-notations/10061-print-custom-grammar.rst +++ /dev/null @@ -1,4 +0,0 @@ -- Allow inspecting custom grammar entries by :cmd:`Print Custom Grammar` - (`#10061 <https://github.com/coq/coq/pull/10061>`_, - fixes `#9681 <http://github.com/coq/coq/pull/9681>`_, - by Jasper Hugunin, review by Pierre-Marie Pédrot and Hugo Herbelin). diff --git a/doc/changelog/04-tactics/09996-hint-mode.rst b/doc/changelog/04-tactics/09996-hint-mode.rst deleted file mode 100644 index 06e9059b45..0000000000 --- a/doc/changelog/04-tactics/09996-hint-mode.rst +++ /dev/null @@ -1,5 +0,0 @@ -- Modes are now taken into account by :tacn:`typeclasses eauto` for - local hypotheses - (`#9996 <https://github.com/coq/coq/pull/9996>`_, - fixes `#5752 <https://github.com/coq/coq/issues/5752>`_, - by Maxime Dénès, review by Pierre-Marie Pédrot). diff --git a/doc/changelog/04-tactics/10059-change-no-check.rst b/doc/changelog/04-tactics/10059-change-no-check.rst deleted file mode 100644 index 987b2a8ccd..0000000000 --- a/doc/changelog/04-tactics/10059-change-no-check.rst +++ /dev/null @@ -1,7 +0,0 @@ -- New variant :tacn:`change_no_check` of :tacn:`change`, usable as a - documented replacement of :tacn:`convert_concl_no_check` - (`#10012 <https://github.com/coq/coq/pull/10012>`_, - `#10017 <https://github.com/coq/coq/pull/10017>`_, - `#10053 <https://github.com/coq/coq/pull/10053>`_, and - `#10059 <https://github.com/coq/coq/pull/10059>`_, - by Hugo Herbelin and Paolo G. Giarrusso). diff --git a/doc/changelog/06-ssreflect/09995-notations.rst b/doc/changelog/06-ssreflect/09995-notations.rst deleted file mode 100644 index 3dfc45242d..0000000000 --- a/doc/changelog/06-ssreflect/09995-notations.rst +++ /dev/null @@ -1,8 +0,0 @@ -- `inE` now expands `y \in r x` when `r` is a `simpl_rel`. - New `{pred T}` notation for a `pred T` alias in the `pred_sort` coercion - class, simplified `predType` interface: `pred_class` and `mkPredType` - deprecated, `{pred T}` and `PredType` should be used instead. - `if c return t then ...` now expects `c` to be a variable bound in `t`. - New `nonPropType` interface matching types that do _not_ have sort `Prop`. - New `relpre R f` definition for the preimage of a relation R under f - (`#9995 <https://github.com/coq/coq/pull/9995>`_, by Georges Gonthier). diff --git a/doc/changelog/10-standard-library/09984-pairusualdecidabletypefull.rst b/doc/changelog/10-standard-library/09984-pairusualdecidabletypefull.rst deleted file mode 100644 index 732c088f45..0000000000 --- a/doc/changelog/10-standard-library/09984-pairusualdecidabletypefull.rst +++ /dev/null @@ -1,3 +0,0 @@ -- Added :g:`Coq.Structures.EqualitiesFacts.PairUsualDecidableTypeFull` - (`#9984 <https://github.com/coq/coq/pull/9984>`_, - by Jean-Christophe Léchenet and Oliver Nash). diff --git a/doc/changelog/12-misc/09964-changes.rst b/doc/changelog/12-misc/09964-changes.rst deleted file mode 100644 index dd873cfdd5..0000000000 --- a/doc/changelog/12-misc/09964-changes.rst +++ /dev/null @@ -1,14 +0,0 @@ -- Changelog has been moved from a specific file `CHANGES.md` to the - reference manual; former Credits chapter of the reference manual has - been split in two parts: a History chapter which was enriched with - additional historical information about Coq versions 1 to 5, and a - Changes chapter which was enriched with the content formerly in - `CHANGES.md` and `COMPATIBILITY` - (`#9133 <https://github.com/coq/coq/pull/9133>`_, - `#9668 <https://github.com/coq/coq/pull/9668>`_, - `#9939 <https://github.com/coq/coq/pull/9939>`_, - `#9964 <https://github.com/coq/coq/pull/9964>`_, - and `#10085 <https://github.com/coq/coq/pull/10085>`_, - by Théo Zimmermann, - with help and ideas from Emilio Jesús Gallego Arias, Gaëtan - Gilbert, Clément Pit-Claudel, Matthieu Sozeau, and Enrico Tassi). diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index 574b943a78..cca3b2e06b 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -355,6 +355,11 @@ Other changes in 8.10+beta1 that will do it automatically, using the output of ``coqc`` (`#8638 <https://github.com/coq/coq/pull/8638>`_, by Jason Gross). + - Allow inspecting custom grammar entries by :cmd:`Print Custom Grammar` + (`#10061 <https://github.com/coq/coq/pull/10061>`_, + fixes `#9681 <http://github.com/coq/coq/pull/9681>`_, + by Jasper Hugunin, review by Pierre-Marie Pédrot and Hugo Herbelin). + - The `quote plugin <https://coq.inria.fr/distrib/V8.9.0/refman/proof-engine/detailed-tactic-examples.html#quote>`_ was removed. If some users are interested in maintaining this plugin @@ -400,7 +405,32 @@ Other changes in 8.10+beta1 closes `#7632 <https://github.com/coq/coq/issues/7632>`_, by Théo Zimmermann). - - SSReflect clear discipline made consistent across the entire proof language. + - Modes are now taken into account by :tacn:`typeclasses eauto` for + local hypotheses + (`#9996 <https://github.com/coq/coq/pull/9996>`_, + fixes `#5752 <https://github.com/coq/coq/issues/5752>`_, + by Maxime Dénès, review by Pierre-Marie Pédrot). + + - New variant :tacn:`change_no_check` of :tacn:`change`, usable as a + documented replacement of :tacn:`convert_concl_no_check` + (`#10012 <https://github.com/coq/coq/pull/10012>`_, + `#10017 <https://github.com/coq/coq/pull/10017>`_, + `#10053 <https://github.com/coq/coq/pull/10053>`_, and + `#10059 <https://github.com/coq/coq/pull/10059>`_, + by Hugo Herbelin and Paolo G. Giarrusso). + + - The simplified value returned by :tacn:`field_simplify` is not + always a fraction anymore. When the denominator is :g:`1`, it + returns :g:`x` while previously it was returning :g:`x/1`. This + change could break codes that were post-processing application of + :tacn:`field_simplify` to get rid of these :g:`x/1` + (`#9854 <https://github.com/coq/coq/pull/9854>`_, + by Laurent Théry, + with help from Michael Soegtrop, Maxime Dénès, and Vincent Laporte). + +- SSReflect: + + - Clear discipline made consistent across the entire proof language. Whenever a clear switch `{x..}` comes immediately before an existing proof context entry (used as a view, as a rewrite rule or as name for a new context entry) then such entry is cleared too. @@ -414,6 +444,15 @@ Other changes in 8.10+beta1 (`#9341 <https://github.com/coq/coq/pull/9341>`_, by Enrico Tassi). + - `inE` now expands `y \in r x` when `r` is a `simpl_rel`. + New `{pred T}` notation for a `pred T` alias in the `pred_sort` coercion + class, simplified `predType` interface: `pred_class` and `mkPredType` + deprecated, `{pred T}` and `PredType` should be used instead. + `if c return t then ...` now expects `c` to be a variable bound in `t`. + New `nonPropType` interface matching types that do _not_ have sort `Prop`. + New `relpre R f` definition for the preimage of a relation R under f + (`#9995 <https://github.com/coq/coq/pull/9995>`_, by Georges Gonthier). + - Vernacular commands: - Binders for an :cmd:`Instance` now act more like binders for a :cmd:`Theorem`. @@ -535,10 +574,28 @@ Other changes in 8.10+beta1 `fset` database (`#9725 <https://github.com/coq/coq/pull/9725>`_, by Frédéric Besson). + - Added :g:`Coq.Structures.EqualitiesFacts.PairUsualDecidableTypeFull` + (`#9984 <https://github.com/coq/coq/pull/9984>`_, + by Jean-Christophe Léchenet and Oliver Nash). + - Some error messages that show problems with a pair of non-matching values will now highlight the differences (`#8669 <https://github.com/coq/coq/pull/8669>`_, by Jim Fehrle). +- Changelog has been moved from a specific file `CHANGES.md` to the + reference manual; former Credits chapter of the reference manual has + been split in two parts: a History chapter which was enriched with + additional historical information about Coq versions 1 to 5, and a + Changes chapter which was enriched with the content formerly in + `CHANGES.md` and `COMPATIBILITY` + (`#9133 <https://github.com/coq/coq/pull/9133>`_, + `#9668 <https://github.com/coq/coq/pull/9668>`_, + `#9939 <https://github.com/coq/coq/pull/9939>`_, + `#9964 <https://github.com/coq/coq/pull/9964>`_, + and `#10085 <https://github.com/coq/coq/pull/10085>`_, + by Théo Zimmermann, + with help and ideas from Emilio Jesús Gallego Arias, Gaëtan + Gilbert, Clément Pit-Claudel, Matthieu Sozeau, and Enrico Tassi). Version 8.9 ----------- diff --git a/engine/evarutil.ml b/engine/evarutil.ml index be0318fbde..0a5bba39b9 100644 --- a/engine/evarutil.ml +++ b/engine/evarutil.ml @@ -656,26 +656,26 @@ let clear_hyps2_in_evi env sigma hyps t concl ids = (* spiwack: a few functions to gather evars on which goals depend. *) let queue_set q is_dependent set = Evar.Set.iter (fun a -> Queue.push (is_dependent,a) q) set -let queue_term q is_dependent c = - queue_set q is_dependent (evars_of_term (EConstr.Unsafe.to_constr c)) +let queue_term evm q is_dependent c = + queue_set q is_dependent (evars_of_term evm c) let process_dependent_evar q acc evm is_dependent e = let evi = Evd.find evm e in (* Queues evars appearing in the types of the goal (conclusion, then hypotheses), they are all dependent. *) - queue_term q true evi.evar_concl; + queue_term evm q true evi.evar_concl; List.iter begin fun decl -> let open NamedDecl in - queue_term q true (NamedDecl.get_type decl); + queue_term evm q true (NamedDecl.get_type decl); match decl with | LocalAssum _ -> () - | LocalDef (_,b,_) -> queue_term q true b + | LocalDef (_,b,_) -> queue_term evm q true b end (EConstr.named_context_of_val evi.evar_hyps); match evi.evar_body with | Evar_empty -> if is_dependent then Evar.Map.add e None acc else acc | Evar_defined b -> - let subevars = evars_of_term (EConstr.Unsafe.to_constr b) in + let subevars = evars_of_term evm b in (* evars appearing in the definition of an evar [e] are marked as dependent when [e] is dependent itself: if [e] is a non-dependent goal, then, unless they are reach from another @@ -795,7 +795,7 @@ let filtered_undefined_evars_of_evar_info ?cache sigma evi = in let accu = match evi.evar_body with | Evar_empty -> Evar.Set.empty - | Evar_defined b -> evars_of_term (EConstr.Unsafe.to_constr b) + | Evar_defined b -> evars_of_term sigma b in let accu = Evar.Set.union (undefined_evars_of_term sigma evi.evar_concl) accu in let ctxt = EConstr.Unsafe.to_named_context (evar_filtered_context evi) in diff --git a/engine/evd.ml b/engine/evd.ml index d37b49e2dc..0f10a380d3 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -823,33 +823,6 @@ let loc_of_conv_pb evd (pbty,env,t1,t2) = | Evar (evk2,_) -> fst (evar_source evk2 evd) | _ -> None -(** The following functions return the set of evars immediately - contained in the object *) - -(* excluding defined evars *) - -let evars_of_term c = - let rec evrec acc c = - match kind c with - | Evar (n, l) -> Evar.Set.add n (Array.fold_left evrec acc l) - | _ -> Constr.fold evrec acc c - in - evrec Evar.Set.empty c - -let evars_of_named_context nc = - Context.Named.fold_outside - (NamedDecl.fold_constr (fun constr s -> Evar.Set.union s (evars_of_term constr))) - nc - ~init:Evar.Set.empty - -let evars_of_filtered_evar_info evi = - Evar.Set.union (evars_of_term evi.evar_concl) - (Evar.Set.union - (match evi.evar_body with - | Evar_empty -> Evar.Set.empty - | Evar_defined b -> evars_of_term b) - (evars_of_named_context (evar_filtered_context evi))) - (**********************************************************) (* Sort variables *) @@ -1404,3 +1377,30 @@ module MiniEConstr = struct let to_rel_decl sigma d = Context.Rel.Declaration.map_constr (to_constr sigma) d end + +(** The following functions return the set of evars immediately + contained in the object *) + +(* excluding defined evars *) + +let evars_of_term evd c = + let rec evrec acc c = + match MiniEConstr.kind evd c with + | Evar (n, l) -> Evar.Set.add n (Array.fold_left evrec acc l) + | _ -> Constr.fold evrec acc c + in + evrec Evar.Set.empty c + +let evars_of_named_context evd nc = + Context.Named.fold_outside + (NamedDecl.fold_constr (fun constr s -> Evar.Set.union s (evars_of_term evd constr))) + nc + ~init:Evar.Set.empty + +let evars_of_filtered_evar_info evd evi = + Evar.Set.union (evars_of_term evd evi.evar_concl) + (Evar.Set.union + (match evi.evar_body with + | Evar_empty -> Evar.Set.empty + | Evar_defined b -> evars_of_term evd b) + (evars_of_named_context evd (evar_filtered_context evi))) diff --git a/engine/evd.mli b/engine/evd.mli index 29235050b0..587a1de044 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -491,16 +491,15 @@ val extract_changed_conv_pbs : evar_map -> val extract_all_conv_pbs : evar_map -> evar_map * evar_constraint list val loc_of_conv_pb : evar_map -> evar_constraint -> Loc.t option -(** The following functions return the set of evars immediately - contained in the object; need the term to be evar-normal otherwise - defined evars are returned too. *) +(** The following functions return the set of undefined evars + contained in the object. *) -val evars_of_term : constr -> Evar.Set.t +val evars_of_term : evar_map -> econstr -> Evar.Set.t (** including evars in instances of evars *) -val evars_of_named_context : (econstr, etypes) Context.Named.pt -> Evar.Set.t +val evars_of_named_context : evar_map -> (econstr, etypes) Context.Named.pt -> Evar.Set.t -val evars_of_filtered_evar_info : evar_info -> Evar.Set.t +val evars_of_filtered_evar_info : evar_map -> evar_info -> Evar.Set.t (** Metas *) val meta_list : evar_map -> (metavariable * clbinding) list diff --git a/engine/proofview.ml b/engine/proofview.ml index ecea637947..1fd8b5d50e 100644 --- a/engine/proofview.ml +++ b/engine/proofview.ml @@ -641,7 +641,7 @@ let shelve_goals l = [sigma]. *) let depends_on sigma src tgt = let evi = Evd.find sigma tgt in - Evar.Set.mem src (Evd.evars_of_filtered_evar_info (Evarutil.nf_evar_info sigma evi)) + Evar.Set.mem src (Evd.evars_of_filtered_evar_info sigma (Evarutil.nf_evar_info sigma evi)) let unifiable_delayed g l = CList.exists (fun (tgt, lazy evs) -> not (Evar.equal g tgt) && Evar.Set.mem g evs) l @@ -1251,9 +1251,9 @@ module V82 = struct let goals = CList.map (fun (t,_) -> fst (Constr.destEvar (EConstr.Unsafe.to_constr t))) initial in { Evd.it = goals ; sigma=solution; } - let top_evars initial = + let top_evars initial { solution=sigma; } = let evars_of_initial (c,_) = - Evar.Set.elements (Evd.evars_of_term (EConstr.Unsafe.to_constr c)) + Evar.Set.elements (Evd.evars_of_term sigma c) in CList.flatten (CList.map evars_of_initial initial) diff --git a/engine/proofview.mli b/engine/proofview.mli index 92f8b86df5..b7ff3ac432 100644 --- a/engine/proofview.mli +++ b/engine/proofview.mli @@ -595,7 +595,7 @@ module V82 : sig val top_goals : entry -> proofview -> Evar.t list Evd.sigma (* returns the existential variable used to start the proof *) - val top_evars : entry -> Evar.t list + val top_evars : entry -> proofview -> Evar.t list (* Caution: this function loses quite a bit of information. It should be avoided as much as possible. It should work as diff --git a/engine/termops.ml b/engine/termops.ml index 8a6bd17948..fcacb53ac4 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -187,7 +187,7 @@ let compute_evar_dependency_graph sigma = in match evar_body evi with | Evar_empty -> acc - | Evar_defined c -> Evar.Set.fold fold_ev (evars_of_term (EConstr.Unsafe.to_constr c)) acc + | Evar_defined c -> Evar.Set.fold fold_ev (evars_of_term sigma c) acc in Evd.fold fold sigma EvMap.empty diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c index 1b348ae777..4b45608ae5 100644 --- a/kernel/byterun/coq_interp.c +++ b/kernel/byterun/coq_interp.c @@ -97,7 +97,8 @@ if (sp - num_args < coq_stack_threshold) { \ several architectures. */ -#if defined(__GNUC__) && !defined(DEBUG) +#if defined(__GNUC__) && !defined(DEBUG) && !defined(__INTEL_COMPILER) \ + && !defined(__llvm__) #ifdef __mips__ #define PC_REG asm("$16") #define SP_REG asm("$17") @@ -126,7 +127,7 @@ if (sp - num_args < coq_stack_threshold) { \ #define SP_REG asm("%edi") #define ACCU_REG #endif -#if defined(PPC) || defined(_POWER) || defined(_IBMR2) +#if defined(__ppc__) || defined(__ppc64__) #define PC_REG asm("26") #define SP_REG asm("27") #define ACCU_REG asm("28") @@ -141,8 +142,9 @@ if (sp - num_args < coq_stack_threshold) { \ #define SP_REG asm("a4") #define ACCU_REG asm("d7") #endif -#if defined(__arm__) && !defined(__thumb2__) -#define PC_REG asm("r9") +/* OCaml PR#4953: these specific registers not available in Thumb mode */ +#if defined(__arm__) && !defined(__thumb__) +#define PC_REG asm("r6") #define SP_REG asm("r8") #define ACCU_REG asm("r7") #endif @@ -152,6 +154,17 @@ if (sp - num_args < coq_stack_threshold) { \ #define ACCU_REG asm("38") #define JUMPTBL_BASE_REG asm("39") #endif +#ifdef __x86_64__ +#define PC_REG asm("%r15") +#define SP_REG asm("%r14") +#define ACCU_REG asm("%r13") +#endif +#ifdef __aarch64__ +#define PC_REG asm("%x19") +#define SP_REG asm("%x20") +#define ACCU_REG asm("%x21") +#define JUMPTBL_BASE_REG asm("%x22") +#endif #endif #define CheckInt1() do{ \ diff --git a/kernel/entries.ml b/kernel/entries.ml index a3d32267a7..adb3f6bd29 100644 --- a/kernel/entries.ml +++ b/kernel/entries.ml @@ -108,21 +108,7 @@ type module_entry = | MExpr of module_params_entry * module_struct_entry * module_struct_entry option - -type seff_env = - [ `Nothing - (* The proof term and its universes. - Same as the constant_body's but not in an ephemeron *) - | `Opaque of Constr.t * Univ.ContextSet.t ] - (** Not used by the kernel. *) type side_effect_role = | Subproof | Schema of inductive * string - -type side_eff = { - seff_constant : Constant.t; - seff_body : Declarations.constant_body; - seff_env : seff_env; - seff_role : side_effect_role; -} diff --git a/kernel/modops.ml b/kernel/modops.ml index 4f992d3972..4fdd7ab334 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -608,11 +608,7 @@ let clean_bounded_mod_expr sign = (** {6 Stm machinery } *) let join_constant_body except otab cb = match cb.const_body with - | OpaqueDef o -> - (match Opaqueproof.uuid_opaque otab o with - | Some uuid when not(Future.UUIDSet.mem uuid except) -> - Opaqueproof.join_opaque otab o - | _ -> ()) + | OpaqueDef o -> Opaqueproof.join_opaque ~except otab o | _ -> () let join_structure except otab s = diff --git a/kernel/opaqueproof.ml b/kernel/opaqueproof.ml index 303cb06c55..57059300b8 100644 --- a/kernel/opaqueproof.ml +++ b/kernel/opaqueproof.ml @@ -87,19 +87,18 @@ let discharge_direct_opaque ~cook_constr ci = function | Direct (d,cu) -> Direct (ci::d,Future.chain cu (fun (c, u) -> cook_constr c, u)) -let join_opaque { opaque_val = prfs; opaque_dir = odp; _ } = function - | Direct (_,cu) -> ignore(Future.join cu) +let join except cu = match except with +| None -> ignore (Future.join cu) +| Some except -> + if Future.UUIDSet.mem (Future.uuid cu) except then () + else ignore (Future.join cu) + +let join_opaque ?except { opaque_val = prfs; opaque_dir = odp; _ } = function + | Direct (_,cu) -> join except cu | Indirect (_,dp,i) -> if DirPath.equal dp odp then let fp = snd (Int.Map.find i prfs) in - ignore(Future.join fp) - -let uuid_opaque { opaque_val = prfs; opaque_dir = odp; _ } = function - | Direct (_,cu) -> Some (Future.uuid cu) - | Indirect (_,dp,i) -> - if DirPath.equal dp odp - then Some (Future.uuid (snd (Int.Map.find i prfs))) - else None + join except fp let force_proof { opaque_val = prfs; opaque_dir = odp; _ } = function | Direct (_,cu) -> @@ -128,16 +127,6 @@ let get_constraints { opaque_val = prfs; opaque_dir = odp; _ } = function then Some(Future.chain (snd (Int.Map.find i prfs)) snd) else !get_univ dp i -let get_proof { opaque_val = prfs; opaque_dir = odp; _ } = function - | Direct (_,cu) -> Future.chain cu fst - | Indirect (l,dp,i) -> - let pt = - if DirPath.equal dp odp - then Future.chain (snd (Int.Map.find i prfs)) fst - else !get_opaque dp i in - Future.chain pt (fun c -> - force_constr (List.fold_right subst_substituted l (from_val c))) - module FMap = Future.UUIDMap let a_constr = Future.from_val (mkRel 1) diff --git a/kernel/opaqueproof.mli b/kernel/opaqueproof.mli index 5ea6da649b..d47c0bbb3c 100644 --- a/kernel/opaqueproof.mli +++ b/kernel/opaqueproof.mli @@ -39,7 +39,6 @@ val turn_indirect : DirPath.t -> opaque -> opaquetab -> opaque * opaquetab indirect opaque accessor configured below. *) val force_proof : opaquetab -> opaque -> constr val force_constraints : opaquetab -> opaque -> Univ.ContextSet.t -val get_proof : opaquetab -> opaque -> constr Future.computation val get_constraints : opaquetab -> opaque -> Univ.ContextSet.t Future.computation option @@ -60,8 +59,7 @@ type cooking_info = { val discharge_direct_opaque : cook_constr:(constr -> constr) -> cooking_info -> opaque -> opaque -val uuid_opaque : opaquetab -> opaque -> Future.UUID.t option -val join_opaque : opaquetab -> opaque -> unit +val join_opaque : ?except:Future.UUIDSet.t -> opaquetab -> opaque -> unit val dump : opaquetab -> Constr.t Future.computation array * diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 673f025c75..75375812c0 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -228,6 +228,12 @@ let check_engagement env expected_impredicative_set = (** {6 Stm machinery } *) +type seff_env = + [ `Nothing + (* The proof term and its universes. + Same as the constant_body's but not in an ephemeron *) + | `Opaque of Constr.t * Univ.ContextSet.t ] + let get_opaque_body env cbo = match cbo.const_body with | Undef _ -> assert false @@ -240,7 +246,10 @@ let get_opaque_body env cbo = type side_effect = { from_env : Declarations.structure_body CEphemeron.key; - eff : Entries.side_eff list; + seff_constant : Constant.t; + seff_body : Declarations.constant_body; + seff_env : seff_env; + seff_role : Entries.side_effect_role; } module SideEffects : @@ -254,11 +263,9 @@ end = struct module SeffOrd = struct -open Entries type t = side_effect let compare e1 e2 = - let cmp e1 e2 = Constant.CanOrd.compare e1.seff_constant e2.seff_constant in - List.compare cmp e1.eff e2.eff + Constant.CanOrd.compare e1.seff_constant e2.seff_constant end module SeffSet = Set.Make(SeffOrd) @@ -279,37 +286,37 @@ end type private_constants = SideEffects.t let side_effects_of_private_constants l = - let ans = List.rev (SideEffects.repr l) in - List.map_append (fun { eff; _ } -> eff) ans + List.rev (SideEffects.repr l) + +let push_private_constants env eff = + let eff = side_effects_of_private_constants eff in + let add_if_undefined env eff = + try ignore(Environ.lookup_constant eff.seff_constant env); env + with Not_found -> Environ.add_constant eff.seff_constant eff.seff_body env + in + List.fold_left add_if_undefined env eff let empty_private_constants = SideEffects.empty -let add_private mb eff effs = - let from_env = CEphemeron.create mb in - SideEffects.add { eff; from_env } effs let concat_private = SideEffects.concat -let make_eff env cst r = - let open Entries in +let private_constant env role cst = + (** The constant must be the last entry of the safe environment *) + let () = match env.revstruct with + | (lbl, SFBconst _) :: _ -> assert (Label.equal lbl (Constant.label cst)) + | _ -> assert false + in + let from_env = CEphemeron.create env.revstruct in let cbo = Environ.lookup_constant cst env.env in - { + let eff = { + from_env = from_env; seff_constant = cst; seff_body = cbo; seff_env = get_opaque_body env.env cbo; - seff_role = r; - } - -let private_con_of_con env c = - let open Entries in - let eff = [make_eff env c Subproof] in - add_private env.revstruct eff empty_private_constants - -let private_con_of_scheme ~kind env cl = - let open Entries in - let eff = List.map (fun (i, c) -> make_eff env c (Schema (i, kind))) cl in - add_private env.revstruct eff empty_private_constants + seff_role = role; + } in + SideEffects.add eff empty_private_constants let universes_of_private eff = - let open Entries in let fold acc eff = let acc = match eff.seff_env with | `Nothing -> acc @@ -588,22 +595,17 @@ let add_constant_aux ~in_section senv (kn, cb) = let mk_pure_proof c = (c, Univ.ContextSet.empty), SideEffects.empty let inline_side_effects env body side_eff = - let open Entries in let open Constr in (** First step: remove the constants that are still in the environment *) - let filter { eff = se; from_env = mb } = - let map e = (e.seff_constant, e.seff_body, e.seff_env) in - let cbl = List.map map se in - let not_exists (c,_,_) = - try ignore(Environ.lookup_constant c env); false - with Not_found -> true in - let cbl = List.filter not_exists cbl in - (cbl, mb) + let filter e = + let cb = (e.seff_constant, e.seff_body, e.seff_env) in + try ignore (Environ.lookup_constant e.seff_constant env); None + with Not_found -> Some (cb, e.from_env) in (* CAVEAT: we assure that most recent effects come first *) - let side_eff = List.map filter (SideEffects.repr side_eff) in - let sigs = List.rev_map (fun (cbl, mb) -> mb, List.length cbl) side_eff in - let side_eff = List.fold_left (fun accu (cbl, _) -> cbl @ accu) [] side_eff in + let side_eff = List.map_filter filter (SideEffects.repr side_eff) in + let sigs = List.rev_map (fun (_, mb) -> mb) side_eff in + let side_eff = List.fold_left (fun accu (cb, _) -> cb :: accu) [] side_eff in let side_eff = List.rev side_eff in (** Most recent side-effects first in side_eff *) if List.is_empty side_eff then (body, Univ.ContextSet.empty, sigs) @@ -675,24 +677,22 @@ let inline_private_constants_in_definition_entry env ce = let inline_private_constants_in_constr env body side_eff = pi1 (inline_side_effects env body side_eff) -let rec is_nth_suffix n l suf = - if Int.equal n 0 then l == suf - else match l with - | [] -> false - | _ :: l -> is_nth_suffix (pred n) l suf +let is_suffix l suf = match l with +| [] -> false +| _ :: l -> l == suf (* Given the list of signatures of side effects, checks if they match. * I.e. if they are ordered descendants of the current revstruct. Returns the number of effects that can be trusted. *) let check_signatures curmb sl = - let is_direct_ancestor accu (mb, how_many) = + let is_direct_ancestor accu mb = match accu with | None -> None | Some (n, curmb) -> try let mb = CEphemeron.get mb in - if is_nth_suffix how_many mb curmb - then Some (n + how_many, mb) + if is_suffix mb curmb + then Some (n + 1, mb) else None with CEphemeron.InvalidKey -> None in let sl = List.fold_left is_direct_ancestor (Some (0, curmb)) sl in @@ -725,7 +725,6 @@ let constant_entry_of_side_effect cb u = const_entry_inline_code = cb.const_inline_code } let turn_direct orig = - let open Entries in let cb = orig.seff_body in if Declareops.is_opaque cb then let p = match orig.seff_env with @@ -738,7 +737,6 @@ let turn_direct orig = else orig let export_eff eff = - let open Entries in (eff.seff_constant, eff.seff_body, eff.seff_role) let export_side_effects mb env c = @@ -751,10 +749,9 @@ let export_side_effects mb env c = let not_exists e = try ignore(Environ.lookup_constant e.seff_constant env); false with Not_found -> true in - let aux (acc,sl) { eff = se; from_env = mb } = - let cbl = List.filter not_exists se in - if List.is_empty cbl then acc, sl - else cbl :: acc, (mb,List.length cbl) :: sl in + let aux (acc,sl) e = + if not (not_exists e) then acc, sl + else e :: acc, e.from_env :: sl in let seff, signatures = List.fold_left aux ([],[]) (SideEffects.repr eff) in let trusted = check_signatures mb signatures in let push_seff env eff = @@ -772,10 +769,9 @@ let export_side_effects mb env c = let rec translate_seff sl seff acc env = match seff with | [] -> List.rev acc, ce - | cbs :: rest -> + | eff :: rest -> if Int.equal sl 0 then - let env, cbs = - List.fold_left (fun (env,cbs) eff -> + let env, cb = let { seff_constant = kn; seff_body = ocb; seff_env = u ; _ } = eff in let ce = constant_entry_of_side_effect ocb u in let cb = Term_typing.translate_constant Term_typing.Pure env kn ce in @@ -783,15 +779,14 @@ let export_side_effects mb env c = seff_body = cb; seff_env = `Nothing; } in - (push_seff env eff, export_eff eff :: cbs)) - (env,[]) cbs in - translate_seff 0 rest (cbs @ acc) env + (push_seff env eff, export_eff eff) + in + translate_seff 0 rest (cb :: acc) env else - let cbs_len = List.length cbs in - let cbs = List.map turn_direct cbs in - let env = List.fold_left push_seff env cbs in - let ecbs = List.map export_eff cbs in - translate_seff (sl - cbs_len) rest (ecbs @ acc) env + let cb = turn_direct eff in + let env = push_seff env cb in + let ecb = export_eff cb in + translate_seff (sl - 1) rest (ecb :: acc) env in translate_seff trusted seff [] env diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index 46c97c1fb8..d6c7022cf5 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -43,18 +43,13 @@ type 'a safe_transformer = safe_environment -> 'a * safe_environment type private_constants -val side_effects_of_private_constants : - private_constants -> Entries.side_eff list -(** Return the list of individual side-effects in the order of their - creation. *) - val empty_private_constants : private_constants val concat_private : private_constants -> private_constants -> private_constants (** [concat_private e1 e2] adds the constants of [e1] to [e2], i.e. constants in [e1] must be more recent than those of [e2]. *) -val private_con_of_con : safe_environment -> Constant.t -> private_constants -val private_con_of_scheme : kind:string -> safe_environment -> (inductive * Constant.t) list -> private_constants +val private_constant : safe_environment -> Entries.side_effect_role -> Constant.t -> private_constants +(** Constant must be the last definition of the safe_environment. *) val mk_pure_proof : Constr.constr -> private_constants Entries.proof_output val inline_private_constants_in_constr : @@ -62,6 +57,9 @@ val inline_private_constants_in_constr : val inline_private_constants_in_definition_entry : Environ.env -> private_constants Entries.definition_entry -> unit Entries.definition_entry +val push_private_constants : Environ.env -> private_constants -> Environ.env +(** Push the constants in the environment if not already there. *) + val universes_of_private : private_constants -> Univ.ContextSet.t list val is_curmod_library : safe_environment -> bool diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml index 4425e41652..4769c2dc53 100644 --- a/plugins/derive/derive.ml +++ b/plugins/derive/derive.ml @@ -102,6 +102,7 @@ let start_deriving f suchthat lemma = let terminator = Proof_global.make_terminator terminator in let pstate = Proof_global.start_dependent_proof ~ontop:None lemma kind goals terminator in - fst @@ Proof_global.with_current_proof begin fun _ p -> - Proof.run_tactic env Proofview.(tclFOCUS 1 2 shelve) p + Proof_global.simple_with_current_proof begin fun _ p -> + let p,_,() = Proof.run_tactic env Proofview.(tclFOCUS 1 2 shelve) p in + p end pstate diff --git a/plugins/ssr/ssrview.ml b/plugins/ssr/ssrview.ml index 075ebf006a..0a5c85f4ab 100644 --- a/plugins/ssr/ssrview.ml +++ b/plugins/ssr/ssrview.ml @@ -290,7 +290,7 @@ let finalize_view s0 ?(simple_types=true) p = Goal.enter_one ~__LOC__ begin fun g -> let env = Goal.env g in let sigma = Goal.sigma g in - let evars_of_p = Evd.evars_of_term (EConstr.to_constr ~abort_on_undefined_evars:false sigma p) in + let evars_of_p = Evd.evars_of_term sigma p in let filter x _ = Evar.Set.mem x evars_of_p in let sigma = Typeclasses.resolve_typeclasses ~fail:false ~filter env sigma in let p = Reductionops.nf_evar sigma p in @@ -307,7 +307,7 @@ Goal.enter_one ~__LOC__ begin fun g -> let und0 = (* Unassigned evars in the initial goal *) let sigma0 = Tacmach.project s0 in let g0info = Evd.find sigma0 (Tacmach.sig_it s0) in - let g0 = Evd.evars_of_filtered_evar_info g0info in + let g0 = Evd.evars_of_filtered_evar_info sigma0 g0info in List.filter (fun k -> Evar.Set.mem k g0) (List.map fst (Evar.Map.bindings (Evd.undefined_map sigma0))) in let rigid = rigid_of und0 in diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml index 4e0866a0c5..adbcfb8f3b 100644 --- a/plugins/ssrmatching/ssrmatching.ml +++ b/plugins/ssrmatching/ssrmatching.ml @@ -529,8 +529,8 @@ exception FoundUnif of (evar_map * UState.t * tpattern) (* Note: we don't update env as we descend into the term, as the primitive *) (* unification procedure always rejects subterms with bound variables. *) -let dont_impact_evars_in cl = - let evs_in_cl = Evd.evars_of_term cl in +let dont_impact_evars_in sigma0 cl = + let evs_in_cl = Evd.evars_of_term sigma0 cl in fun sigma -> Evar.Set.for_all (fun k -> try let _ = Evd.find_undefined sigma k in true with Not_found -> false) evs_in_cl @@ -544,7 +544,7 @@ let dont_impact_evars_in cl = (* - w_unify expands let-in (zeta conversion) eagerly, whereas we want to *) (* match a head let rigidly. *) let match_upats_FO upats env sigma0 ise orig_c = - let dont_impact_evars = dont_impact_evars_in orig_c in + let dont_impact_evars = dont_impact_evars_in sigma0 (EConstr.of_constr orig_c) in let rec loop c = let f, a = splay_app ise c in let i0 = ref (-1) in let fpats = @@ -586,7 +586,7 @@ let match_upats_FO upats env sigma0 ise orig_c = let match_upats_HO ~on_instance upats env sigma0 ise c = - let dont_impact_evars = dont_impact_evars_in c in + let dont_impact_evars = dont_impact_evars_in sigma0 (EConstr.of_constr c) in let it_did_match = ref false in let failed_because_of_TC = ref false in let rec aux upats env sigma0 ise c = diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 062e3ca8b2..82726eccf0 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -708,9 +708,6 @@ type binder_kind = BProd | BLambda | BLetIn (**********************************************************************) (* Main detyping function *) -let detype_anonymous = ref (fun ?loc n -> anomaly ~label:"detype" (Pp.str "index to an anonymous variable.")) -let set_detype_anonymous f = detype_anonymous := f - let detype_level sigma l = let l = hack_qualid_of_univ_level sigma l in GType (UNamed l) @@ -732,11 +729,13 @@ and detype_r d flags avoid env sigma t = match EConstr.kind sigma (collapse_appl sigma t) with | Rel n -> (try match lookup_name_of_rel n (fst env) with - | Name id -> GVar id - | Anonymous -> GVar (!detype_anonymous n) + | Name id -> GVar id + | Anonymous -> + let s = "_ANONYMOUS_REL_"^(string_of_int n) in + GVar (Id.of_string s) with Not_found -> - let s = "_UNBOUND_REL_"^(string_of_int n) - in GVar (Id.of_string s)) + let s = "_UNBOUND_REL_"^(string_of_int n) + in GVar (Id.of_string s)) | Meta n -> (* Meta in constr are not user-parsable and are mapped to Evar *) if n = Constr_matching.special_meta then diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli index 1a8e97efb8..00b0578a52 100644 --- a/pretyping/detyping.mli +++ b/pretyping/detyping.mli @@ -68,9 +68,6 @@ val detype_closed_glob : ?lax:bool -> bool -> Id.Set.t -> env -> evar_map -> clo val lookup_name_as_displayed : env -> evar_map -> constr -> Id.t -> int option val lookup_index_as_renamed : env -> evar_map -> constr -> int -> int option -(* XXX: This is a hack and should go away *) -val set_detype_anonymous : (?loc:Loc.t -> int -> Id.t) -> unit - val force_wildcard : unit -> bool val synthetize_type : unit -> bool diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index 4f36354f79..52e15f466f 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -98,7 +98,7 @@ let solve ?with_end_tac gi info_lvl tac pr = else tac in let env = Global.env () in - let (p,(status,info)) = Proof.run_tactic env tac pr in + let (p,(status,info),()) = Proof.run_tactic env tac pr in let env = Global.env () in let sigma = Evd.from_env env in let () = @@ -161,7 +161,7 @@ let refine_by_tactic ~name ~poly env sigma ty tac = let prev_future_goals = save_future_goals sigma in (* Start a proof *) let prf = Proof.start ~name ~poly sigma [env, ty] in - let (prf, _) = + let (prf, _, ()) = try Proof.run_tactic env tac prf with Logic_monad.TacticFailure e as src -> (* Catch the inner error of the monad tactic *) diff --git a/proofs/proof.ml b/proofs/proof.ml index 778d98b2cd..09e4e898fe 100644 --- a/proofs/proof.ml +++ b/proofs/proof.ml @@ -372,7 +372,7 @@ let run_tactic env tac pr = let sp = pr.proofview in let undef sigma l = List.filter (fun g -> Evd.is_undefined sigma g) l in let tac = - tac >>= fun () -> + tac >>= fun result -> Proofview.tclEVARMAP >>= fun sigma -> (* Already solved goals are not to be counted as shelved. Nor are they to be marked as unresolvable. *) @@ -383,10 +383,10 @@ let run_tactic env tac pr = CErrors.anomaly Pp.(str "Evars generated outside of proof engine (e.g. V82, clear, ...) are not supposed to be explicitly given up."); let sigma = Proofview.Unsafe.mark_as_goals sigma retrieved in Proofview.Unsafe.tclEVARS sigma >>= fun () -> - Proofview.tclUNIT retrieved + Proofview.tclUNIT (result,retrieved) in let { name; poly } = pr in - let (retrieved,proofview,(status,to_shelve,give_up),info_trace) = + let ((result,retrieved),proofview,(status,to_shelve,give_up),info_trace) = Proofview.apply ~name ~poly env tac sp in let sigma = Proofview.return proofview in @@ -400,7 +400,7 @@ let run_tactic env tac pr = in let given_up = pr.given_up@give_up in let proofview = Proofview.Unsafe.reset_future_goals proofview in - { pr with proofview ; shelf ; given_up },(status,info_trace) + { pr with proofview ; shelf ; given_up },(status,info_trace),result (*** Commands ***) @@ -425,7 +425,7 @@ module V82 = struct { Evd.it=List.hd gls ; sigma=sigma; } let top_evars p = - Proofview.V82.top_evars p.entry + Proofview.V82.top_evars p.entry p.proofview let grab_evars p = if not (is_done p) then diff --git a/proofs/proof.mli b/proofs/proof.mli index 1f4748141a..248b9d921e 100644 --- a/proofs/proof.mli +++ b/proofs/proof.mli @@ -172,7 +172,7 @@ val no_focused_goal : t -> bool used. In which case it is [false]. *) val run_tactic : Environ.env - -> unit Proofview.tactic -> t -> t * (bool*Proofview_monad.Info.tree) + -> 'a Proofview.tactic -> t -> t * (bool*Proofview_monad.Info.tree) * 'a val maximal_unfocus : 'a focus_kind -> t -> t diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index 08b98d702a..40ae4acc88 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -345,6 +345,6 @@ let update_global_env (pf : t) = with_current_proof (fun _ p -> Proof.in_proof p (fun sigma -> let tac = Proofview.Unsafe.tclEVARS (Evd.update_sigma_env sigma (Global.env ())) in - let (p,(status,info)) = Proof.run_tactic (Global.env ()) tac p in + let (p,(status,info),()) = Proof.run_tactic (Global.env ()) tac p in (p, ()))) pf in res diff --git a/proofs/refine.ml b/proofs/refine.ml index 06e6b89df1..4a9404aa96 100644 --- a/proofs/refine.ml +++ b/proofs/refine.ml @@ -44,17 +44,6 @@ let typecheck_evar ev env sigma = let sigma, _ = Typing.sort_of env sigma (Evd.evar_concl info) in sigma -(* Get the side-effect's constant declarations to update the monad's - * environmnent *) -let add_if_undefined env eff = - let open Entries in - try ignore(Environ.lookup_constant eff.seff_constant env); env - with Not_found -> Environ.add_constant eff.seff_constant eff.seff_body env - -(* Add the side effects to the monad's environment, if not already done. *) -let add_side_effects env eff = - List.fold_left add_if_undefined env eff - let generic_refine ~typecheck f gl = let sigma = Proofview.Goal.sigma gl in let env = Proofview.Goal.env gl in @@ -71,8 +60,7 @@ let generic_refine ~typecheck f gl = let evs = Evd.save_future_goals sigma in (* Redo the effects in sigma in the monad's env *) let privates_csts = Evd.eval_side_effects sigma in - let sideff = Safe_typing.side_effects_of_private_constants privates_csts in - let env = add_side_effects env sideff in + let env = Safe_typing.push_private_constants env privates_csts in (* Check that the introduced evars are well-typed *) let fold accu ev = typecheck_evar ev env accu in let sigma = if typecheck then Evd.fold_future_goals fold sigma evs else sigma in diff --git a/stm/proofBlockDelimiter.ml b/stm/proofBlockDelimiter.ml index 2b32838964..04f10e7399 100644 --- a/stm/proofBlockDelimiter.ml +++ b/stm/proofBlockDelimiter.ml @@ -41,8 +41,8 @@ let simple_goal sigma g gs = let open Evd in let open Evarutil in let evi = Evd.find sigma g in - Set.is_empty (evars_of_term (EConstr.Unsafe.to_constr evi.evar_concl)) && - Set.is_empty (evars_of_filtered_evar_info (nf_evar_info sigma evi)) && + Set.is_empty (evars_of_term sigma evi.evar_concl) && + Set.is_empty (evars_of_filtered_evar_info sigma (nf_evar_info sigma evi)) && not (List.exists (Proofview.depends_on sigma g) gs) let is_focused_goal_simple ~doc id = diff --git a/stm/stm.ml b/stm/stm.ml index 3eb6d03529..21618bc044 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -2085,8 +2085,8 @@ end = struct (* {{{ *) let st = Vernacstate.freeze_interp_state ~marshallable:false in stm_fail ~st fail (fun () -> (if time then System.with_time ~batch ~header:(Pp.mt ()) else (fun x -> x)) (fun () -> - ignore(TaskQueue.with_n_workers nworkers (fun queue -> - PG_compat.with_current_proof (fun _ p -> + TaskQueue.with_n_workers nworkers (fun queue -> + PG_compat.simple_with_current_proof (fun _ p -> let Proof.{goals} = Proof.data p in let open TacTask in let res = CList.map_i (fun i g -> @@ -2131,7 +2131,8 @@ end = struct (* {{{ *) if solve then Tacticals.New.tclSOLVE [] else tclUNIT () end) in - Proof.run_tactic (Global.env()) assign_tac p)))) ()) + let p,_,() = Proof.run_tactic (Global.env()) assign_tac p in + p))) ()) end (* }}} *) diff --git a/tactics/abstract.ml b/tactics/abstract.ml index 7a61deba0c..499152f39a 100644 --- a/tactics/abstract.ml +++ b/tactics/abstract.ml @@ -174,7 +174,7 @@ let cache_term_by_tactic_then ~opaque ~name_op ?(goal_type=None) tac tacK = let lem = mkConstU (cst, inst) in let evd = Evd.set_universe_context evd ectx in let open Safe_typing in - let eff = private_con_of_con (Global.safe_env ()) cst in + let eff = private_constant (Global.safe_env ()) Entries.Subproof cst in let effs = concat_private eff Entries.(snd (Future.force const.const_entry_body)) in let solve = diff --git a/tactics/equality.ml b/tactics/equality.ml index f049f8c568..45a4799ea1 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -417,7 +417,7 @@ let leibniz_rewrite_ebindings_clause cls lft2rgt tac c t l with_evars frzevars d find_elim hdcncl lft2rgt dep cls (Some t) >>= fun elim -> general_elim_clause with_evars frzevars tac cls c t l (match lft2rgt with None -> false | Some b -> b) - {elimindex = None; elimbody = (elim,NoBindings); elimrename = None} + {elimindex = None; elimbody = (elim,NoBindings) } end let adjust_rewriting_direction args lft2rgt = diff --git a/tactics/ind_tables.ml b/tactics/ind_tables.ml index 16829482e5..e95778a90d 100644 --- a/tactics/ind_tables.ml +++ b/tactics/ind_tables.ml @@ -147,9 +147,10 @@ let define_individual_scheme_base kind suff f mode idopt (mind,i as ind) = | Some id -> id | None -> add_suffix mib.mind_packets.(i).mind_typename suff in let const = define mode id c (Declareops.inductive_is_polymorphic mib) ctx in + let role = Entries.Schema (ind, kind) in + let neff = Safe_typing.private_constant (Global.safe_env ()) role const in declare_scheme kind [|ind,const|]; - const, Safe_typing.concat_private - (Safe_typing.private_con_of_scheme ~kind (Global.safe_env()) [ind,const]) eff + const, Safe_typing.concat_private neff eff let define_individual_scheme kind mode names (mind,i as ind) = match Hashtbl.find scheme_object_table kind with @@ -163,15 +164,16 @@ let define_mutual_scheme_base kind suff f mode names mind = let ids = Array.init (Array.length mib.mind_packets) (fun i -> try Int.List.assoc i names with Not_found -> add_suffix mib.mind_packets.(i).mind_typename suff) in - let consts = Array.map2 (fun id cl -> - define mode id cl (Declareops.inductive_is_polymorphic mib) ctx) ids cl in + let fold i effs id cl = + let cst = define mode id cl (Declareops.inductive_is_polymorphic mib) ctx in + let role = Entries.Schema ((mind, i), kind)in + let neff = Safe_typing.private_constant (Global.safe_env ()) role cst in + (Safe_typing.concat_private neff effs, cst) + in + let (eff, consts) = Array.fold_left2_map_i fold eff ids cl in let schemes = Array.mapi (fun i cst -> ((mind,i),cst)) consts in declare_scheme kind schemes; - consts, - Safe_typing.concat_private - (Safe_typing.private_con_of_scheme - ~kind (Global.safe_env()) (Array.to_list schemes)) - eff + consts, eff let define_mutual_scheme kind mode names mind = match Hashtbl.find scheme_object_table kind with diff --git a/tactics/leminv.ml b/tactics/leminv.ml index 4aa4d13e1e..6efa1ece9c 100644 --- a/tactics/leminv.ml +++ b/tactics/leminv.ml @@ -204,10 +204,7 @@ let inversion_scheme ~name ~poly env sigma t sort dep_option inv_op = (str"Computed inversion goal was not closed in initial signature."); *) let pf = Proof.start ~name ~poly (Evd.from_ctx (evar_universe_context sigma)) [invEnv,invGoal] in - let pf = - fst (Proof.run_tactic env ( - tclTHEN intro (onLastHypId inv_op)) pf) - in + let pf, _, () = Proof.run_tactic env (tclTHEN intro (onLastHypId inv_op)) pf in let pfterm = List.hd (Proof.partial_proof pf) in let global_named_context = Global.named_context_val () in let ownSign = ref begin diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 806c955591..2bdfc85d6d 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1302,14 +1302,11 @@ let do_replace id = function [Ti] and the first one (resp last one) being [G] whose hypothesis [id] is replaced by P using the proof given by [tac] *) -let clenv_refine_in ?(sidecond_first=false) with_evars ?(with_classes=true) - targetid id sigma0 clenv tac = +let clenv_refine_in with_evars targetid id sigma0 clenv tac = let clenv = Clenvtac.clenv_pose_dependent_evars ~with_evars clenv in let clenv = - if with_classes then { clenv with evd = Typeclasses.resolve_typeclasses ~fail:(not with_evars) clenv.env clenv.evd } - else clenv in let new_hyp_typ = clenv_type clenv in if not with_evars then check_unresolved_evars_of_metas sigma0 clenv; @@ -1321,11 +1318,7 @@ let clenv_refine_in ?(sidecond_first=false) with_evars ?(with_classes=true) let with_clear = do_replace (Some id) naming in Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS (clear_metas clenv.evd)) - (if sidecond_first then - Tacticals.New.tclTHENFIRST - (assert_before_then_gen with_clear naming new_hyp_typ tac) exact_tac - else - Tacticals.New.tclTHENLAST + (Tacticals.New.tclTHENLAST (assert_after_then_gen with_clear naming new_hyp_typ tac) exact_tac) (********************************************) @@ -1360,22 +1353,25 @@ let rec contract_letin_in_lam_header sigma c = | LetIn (x,b,t,c) -> contract_letin_in_lam_header sigma (subst1 b c) | _ -> c -let elimination_clause_scheme with_evars ?(with_classes=true) ?(flags=elim_flags ()) - rename i (elim, elimty, bindings) indclause = - Proofview.Goal.enter begin fun gl -> - let env = Proofview.Goal.env gl in - let sigma = Tacmach.New.project gl in - let elim = contract_letin_in_lam_header sigma elim in - let elimclause = make_clenv_binding env sigma (elim, elimty) bindings in - let indmv = - (match EConstr.kind sigma (nth_arg sigma i elimclause.templval.rebus) with - | Meta mv -> mv - | _ -> user_err ~hdr:"elimination_clause" - (str "The type of elimination clause is not well-formed.")) +let elimination_in_clause_scheme env sigma with_evars ~flags + id hypmv elimclause = + let hyp = mkVar id in + let hyp_typ = Retyping.get_type_of env sigma hyp in + let hypclause = mk_clenv_from_env env sigma (Some 0) (hyp, hyp_typ) in + let elimclause'' = + (* The evarmap of elimclause is assumed to be an extension of hypclause, so + we do not need to merge the universes coming from hypclause. *) + try clenv_fchain ~with_univs:false ~flags hypmv elimclause hypclause + with PretypeError (env,evd,NoOccurrenceFound (op,_)) -> + (* Set the hypothesis name in the message *) + raise (PretypeError (env,evd,NoOccurrenceFound (op,Some id))) in - let elimclause' = clenv_fchain ~flags indmv elimclause indclause in - Clenvtac.res_pf elimclause' ~with_evars ~with_classes ~flags - end + let new_hyp_typ = clenv_type elimclause'' in + if EConstr.eq_constr sigma hyp_typ new_hyp_typ then + user_err ~hdr:"general_rewrite_in" + (str "Nothing to rewrite in " ++ Id.print id ++ str"."); + clenv_refine_in with_evars id id sigma elimclause'' + (fun id -> Proofview.tclUNIT ()) (* * Elimination tactic with bindings and using an arbitrary @@ -1387,11 +1383,10 @@ let elimination_clause_scheme with_evars ?(with_classes=true) ?(flags=elim_flags type eliminator = { elimindex : int option; (* None = find it automatically *) - elimrename : (bool * int array) option; (** None = don't rename Prop hyps with H-names *) elimbody : EConstr.constr with_bindings } -let general_elim_clause_gen elimtac indclause elim = +let general_elim_clause with_evars flags where indclause elim = Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Tacmach.New.project gl in @@ -1399,7 +1394,27 @@ let general_elim_clause_gen elimtac indclause elim = let elimt = Retyping.get_type_of env sigma elimc in let i = match elim.elimindex with None -> index_of_ind_arg sigma elimt | Some i -> i in - elimtac elim.elimrename i (elimc, elimt, lbindelimc) indclause + let elimc = contract_letin_in_lam_header sigma elimc in + let elimclause = make_clenv_binding env sigma (elimc, elimt) lbindelimc in + let indmv = + (match EConstr.kind sigma (nth_arg sigma i elimclause.templval.rebus) with + | Meta mv -> mv + | _ -> user_err ~hdr:"elimination_clause" + (str "The type of elimination clause is not well-formed.")) + in + match where with + | None -> + let elimclause = clenv_fchain ~flags indmv elimclause indclause in + Clenvtac.res_pf elimclause ~with_evars ~with_classes:true ~flags + | Some id -> + let hypmv = + match List.remove Int.equal indmv (clenv_independent elimclause) with + | [a] -> a + | _ -> user_err ~hdr:"elimination_clause" + (str "The type of elimination clause is not well-formed.") + in + let elimclause = clenv_fchain ~flags indmv elimclause indclause in + elimination_in_clause_scheme env sigma with_evars ~flags id hypmv elimclause end let general_elim with_evars clear_flag (c, lbindc) elim = @@ -1408,12 +1423,12 @@ let general_elim with_evars clear_flag (c, lbindc) elim = let sigma = Tacmach.New.project gl in let ct = Retyping.get_type_of env sigma c in let t = try snd (reduce_to_quantified_ind env sigma ct) with UserError _ -> ct in - let elimtac = elimination_clause_scheme with_evars in let indclause = make_clenv_binding env sigma (c, t) lbindc in let sigma = meta_merge sigma (clear_metas indclause.evd) in + let flags = elim_flags () in Proofview.Unsafe.tclEVARS sigma <*> Tacticals.New.tclTHEN - (general_elim_clause_gen elimtac indclause elim) + (general_elim_clause with_evars flags None indclause elim) (apply_clear_request clear_flag (use_clear_hyp_by_default ()) c) end @@ -1436,8 +1451,7 @@ let general_case_analysis_in_context with_evars clear_flag (c,lbindc) = let elim = EConstr.of_constr elim in Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma) (general_elim with_evars clear_flag (c,lbindc) - {elimindex = None; elimbody = (elim,NoBindings); - elimrename = Some (false, constructors_nrealdecls env (fst mind))}) + {elimindex = None; elimbody = (elim,NoBindings); }) end let general_case_analysis with_evars clear_flag (c,lbindc as cx) = @@ -1468,8 +1482,7 @@ let find_eliminator c gl = let ((ind,u),t) = Tacmach.New.pf_reduce_to_quantified_ind gl (Tacmach.New.pf_unsafe_type_of gl c) in if is_nonrec ind then raise IsNonrec; let evd, c = find_ind_eliminator ind (Tacticals.New.elimination_sort_of_goal gl) gl in - evd, {elimindex = None; elimbody = (c,NoBindings); - elimrename = Some (true, constructors_nrealdecls (Global.env()) ind)} + evd, { elimindex = None; elimbody = (c,NoBindings) } let default_elim with_evars clear_flag (c,_ as cx) = Proofview.tclORELSE @@ -1489,7 +1502,7 @@ let default_elim with_evars clear_flag (c,_ as cx) = let elim_in_context with_evars clear_flag c = function | Some elim -> general_elim with_evars clear_flag c - {elimindex = Some (-1); elimbody = elim; elimrename = None} + { elimindex = Some (-1); elimbody = elim } | None -> default_elim with_evars clear_flag c let elim with_evars clear_flag (c,lbindc as cx) elim = @@ -1515,48 +1528,6 @@ let simplest_elim c = default_elim false None (c,NoBindings) (e.g. it could replace id:A->B->C by id:C, knowing A/\B) *) -let clenv_fchain_in id ?(flags=elim_flags ()) mv elimclause hypclause = - (* The evarmap of elimclause is assumed to be an extension of hypclause, so - we do not need to merge the universes coming from hypclause. *) - try clenv_fchain ~with_univs:false ~flags mv elimclause hypclause - with PretypeError (env,evd,NoOccurrenceFound (op,_)) -> - (* Set the hypothesis name in the message *) - raise (PretypeError (env,evd,NoOccurrenceFound (op,Some id))) - -let elimination_in_clause_scheme with_evars ?(flags=elim_flags ()) - id rename i (elim, elimty, bindings) indclause = - Proofview.Goal.enter begin fun gl -> - let env = Proofview.Goal.env gl in - let sigma = Tacmach.New.project gl in - let elim = contract_letin_in_lam_header sigma elim in - let elimclause = make_clenv_binding env sigma (elim, elimty) bindings in - let indmv = destMeta sigma (nth_arg sigma i elimclause.templval.rebus) in - let hypmv = - match List.remove Int.equal indmv (clenv_independent elimclause) with - | [a] -> a - | _ -> user_err ~hdr:"elimination_clause" - (str "The type of elimination clause is not well-formed.") - in - let elimclause' = clenv_fchain ~flags indmv elimclause indclause in - let hyp = mkVar id in - let hyp_typ = Retyping.get_type_of env sigma hyp in - let hypclause = mk_clenv_from_env env sigma (Some 0) (hyp, hyp_typ) in - let elimclause'' = clenv_fchain_in id ~flags hypmv elimclause' hypclause in - let new_hyp_typ = clenv_type elimclause'' in - if EConstr.eq_constr sigma hyp_typ new_hyp_typ then - user_err ~hdr:"general_rewrite_in" - (str "Nothing to rewrite in " ++ Id.print id ++ str"."); - clenv_refine_in with_evars id id sigma elimclause'' - (fun id -> Proofview.tclUNIT ()) - end - -let general_elim_clause with_evars flags id c e = - let elim = match id with - | None -> elimination_clause_scheme with_evars ~with_classes:true ~flags - | Some id -> elimination_in_clause_scheme with_evars ~flags id - in - general_elim_clause_gen elim c e - (* Apply a tactic below the products of the conclusion of a lemma *) type conjunction_status = @@ -1828,7 +1799,7 @@ let apply_in_once_main flags innerclause env sigma (loc,d,lbind) = in aux (make_clenv_binding env sigma (d,thm) lbind) -let apply_in_once ?(respect_opaque = false) sidecond_first with_delta +let apply_in_once ?(respect_opaque = false) with_delta with_destruct with_evars naming id (clear_flag,{ CAst.loc; v= d,lbind}) tac = let open Context.Rel.Declaration in Proofview.Goal.enter begin fun gl -> @@ -1849,7 +1820,7 @@ let apply_in_once ?(respect_opaque = false) sidecond_first with_delta if with_delta then default_unify_flags () else default_no_delta_unify_flags ts in try let clause = apply_in_once_main flags innerclause env sigma (loc,c,lbind) in - clenv_refine_in ~sidecond_first with_evars targetid id sigma clause + clenv_refine_in with_evars targetid id sigma clause (fun id -> Tacticals.New.tclTHENLIST [ apply_clear_request clear_flag false c; @@ -1866,14 +1837,14 @@ let apply_in_once ?(respect_opaque = false) sidecond_first with_delta aux [] with_destruct d end -let apply_in_delayed_once ?(respect_opaque = false) sidecond_first with_delta +let apply_in_delayed_once ?(respect_opaque = false) with_delta with_destruct with_evars naming id (clear_flag,{CAst.loc;v=f}) tac = Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Tacmach.New.project gl in let (sigma, c) = f env sigma in Tacticals.New.tclWITHHOLES with_evars - (apply_in_once ~respect_opaque sidecond_first with_delta with_destruct with_evars + (apply_in_once ~respect_opaque with_delta with_destruct with_evars naming id (clear_flag,CAst.(make ?loc c)) tac) sigma end @@ -2493,7 +2464,7 @@ and intro_pattern_action ?loc with_evars b style pat thin destopt tac id = clear [id] in let f env sigma = let (sigma, c) = f env sigma in (sigma,(c, NoBindings)) in - apply_in_delayed_once false true true with_evars naming id (None,CAst.make ?loc:loc' f) + apply_in_delayed_once true true with_evars naming id (None,CAst.make ?loc:loc' f) (fun id -> Tacticals.New.tclTHENLIST [doclear; tac_ipat id; tac thin None []]) and prepare_intros ?loc with_evars dft destopt = function @@ -2561,10 +2532,10 @@ let assert_as first hd ipat t = (* apply in as *) -let general_apply_in ?(respect_opaque=false) sidecond_first with_delta +let general_apply_in ?(respect_opaque=false) with_delta with_destruct with_evars id lemmas ipat = let tac (naming,lemma) tac id = - apply_in_delayed_once ~respect_opaque sidecond_first with_delta + apply_in_delayed_once ~respect_opaque with_delta with_destruct with_evars naming id lemma tac in Proofview.Goal.enter begin fun gl -> let destopt = @@ -2593,10 +2564,10 @@ let general_apply_in ?(respect_opaque=false) sidecond_first with_delta let apply_in simple with_evars id lemmas ipat = let lemmas = List.map (fun (k,{CAst.loc;v=l}) -> k, CAst.make ?loc (fun _ sigma -> (sigma,l))) lemmas in - general_apply_in false simple simple with_evars id lemmas ipat + general_apply_in simple simple with_evars id lemmas ipat let apply_delayed_in simple with_evars id lemmas ipat = - general_apply_in ~respect_opaque:true false simple simple with_evars id lemmas ipat + general_apply_in ~respect_opaque:true simple simple with_evars id lemmas ipat (*****************************) (* Tactics abstracting terms *) @@ -4183,7 +4154,7 @@ let find_induction_type isrec elim hyp0 gl = let scheme = compute_elim_sig sigma ~elimc elimt in if Option.is_empty scheme.indarg then error "Cannot find induction type"; let indsign = compute_scheme_signature evd scheme hyp0 ind_guess in - let elim = ({elimindex = Some(-1); elimbody = elimc; elimrename = None},elimt) in + let elim = ({ elimindex = Some(-1); elimbody = elimc },elimt) in scheme, ElimUsing (elim,indsign) in match scheme.indref with @@ -4210,10 +4181,7 @@ let get_eliminator elim dep s gl = | ElimOver (isrec,id) -> let evd, (elimc,elimt),_ as elims = guess_elim isrec dep s id gl in let _, (l, s) = compute_elim_signature elims id in - let branchlengthes = List.map (fun d -> assert (RelDecl.is_local_assum d); pi1 (decompose_prod_letin (Tacmach.New.project gl) (RelDecl.get_type d))) - (List.rev s.branches) - in - evd, isrec, ({elimindex = None; elimbody = elimc; elimrename = Some (isrec,Array.of_list branchlengthes)}, elimt), l + evd, isrec, ({ elimindex = None; elimbody = elimc }, elimt), l (* Instantiate all meta variables of elimclause using lid, some elts of lid are parameters (first ones), the other are @@ -4257,7 +4225,7 @@ let recolle_clenv i params args elimclause gl = let induction_tac with_evars params indvars elim = Proofview.Goal.enter begin fun gl -> let sigma = Tacmach.New.project gl in - let ({elimindex=i;elimbody=(elimc,lbindelimc);elimrename=rename},elimt) = elim in + let ({ elimindex=i;elimbody=(elimc,lbindelimc) },elimt) = elim in let i = match i with None -> index_of_ind_arg sigma elimt | Some i -> i in (* elimclause contains this: (elimc ?i ?j ?k...?l) *) let elimc = contract_letin_in_lam_header sigma elimc in @@ -4362,7 +4330,7 @@ let induction_without_atomization isrec with_evars elim names lid = (* FIXME: Tester ca avec un principe dependant et non-dependant *) induction_tac with_evars params realindvars elim; ] in - let elim = ElimUsing (({elimindex = Some (-1); elimbody = Option.get scheme.elimc; elimrename = None}, scheme.elimt), indsign) in + let elim = ElimUsing (({ elimindex = Some (-1); elimbody = Option.get scheme.elimc }, scheme.elimt), indsign) in apply_induction_in_context with_evars None [] elim indvars names induct_tac end diff --git a/tactics/tactics.mli b/tactics/tactics.mli index 9eb8196280..32c64bacf6 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -282,7 +282,6 @@ val compute_elim_sig : evar_map -> ?elimc:constr with_bindings -> types -> elim_ (** elim principle with the index of its inductive arg *) type eliminator = { elimindex : int option; (** None = find it automatically *) - elimrename : (bool * int array) option; (** None = don't rename Prop hyps with H-names *) elimbody : constr with_bindings } diff --git a/test-suite/bugs/closed/bug_10026.v b/test-suite/bugs/closed/bug_10026.v new file mode 100644 index 0000000000..0d3142d0f2 --- /dev/null +++ b/test-suite/bugs/closed/bug_10026.v @@ -0,0 +1,3 @@ +Require Import Coq.Lists.List. +Set Debug RAKAM. +Check fun _ => fold_right (fun A B => prod A B) unit _. diff --git a/test-suite/bugs/opened/bug_3754.v b/test-suite/bugs/closed/bug_3754.v index 18820b1a4c..7031cbf132 100644 --- a/test-suite/bugs/opened/bug_3754.v +++ b/test-suite/bugs/closed/bug_3754.v @@ -281,5 +281,7 @@ Defined. (factor2 fact)). rewrite <- ap_p_pp; rewrite_moveL_Mp_p. Set Debug Tactic Unification. - Fail rewrite (concat_Ap ff2). + rewrite (concat_Ap ff2). Abort. + +End Factorization. diff --git a/user-contrib/Ltac2/Constr.v b/user-contrib/Ltac2/Constr.v index d8d222730e..1701bf4365 100644 --- a/user-contrib/Ltac2/Constr.v +++ b/user-contrib/Ltac2/Constr.v @@ -38,6 +38,7 @@ Ltac2 Type kind := [ | Fix (int array, int, ident option array, constr array, constr array) | CoFix (int, ident option array, constr array, constr array) | Proj (projection, constr) +| Uint63 (uint63) ]. Ltac2 @ external kind : constr -> kind := "ltac2" "constr_kind". diff --git a/user-contrib/Ltac2/Init.v b/user-contrib/Ltac2/Init.v index 16e7d7a6f9..dc1690bdfb 100644 --- a/user-contrib/Ltac2/Init.v +++ b/user-contrib/Ltac2/Init.v @@ -14,6 +14,7 @@ Ltac2 Type int. Ltac2 Type string. Ltac2 Type char. Ltac2 Type ident. +Ltac2 Type uint63. (** Constr-specific built-in types *) Ltac2 Type meta. diff --git a/user-contrib/Ltac2/tac2core.ml b/user-contrib/Ltac2/tac2core.ml index d7e7b91ee6..da8600109e 100644 --- a/user-contrib/Ltac2/tac2core.ml +++ b/user-contrib/Ltac2/tac2core.ml @@ -424,8 +424,8 @@ let () = define1 "constr_kind" constr begin fun c -> Value.of_ext Value.val_projection p; Value.of_constr c; |] - | Int _ -> - assert false + | Int n -> + v_blk 17 [|Value.of_uint63 n|] end end @@ -503,6 +503,9 @@ let () = define1 "constr_make" valexpr begin fun knd -> let p = Value.to_ext Value.val_projection p in let c = Value.to_constr c in EConstr.mkProj (p, c) + | (17, [|n|]) -> + let n = Value.to_uint63 n in + EConstr.mkInt n | _ -> assert false in return (Value.of_constr c) diff --git a/user-contrib/Ltac2/tac2entries.ml b/user-contrib/Ltac2/tac2entries.ml index 9fd01426de..254c2e5086 100644 --- a/user-contrib/Ltac2/tac2entries.ml +++ b/user-contrib/Ltac2/tac2entries.ml @@ -740,7 +740,6 @@ let register_redefinition ?(local = false) qid e = Lib.add_anonymous_leaf (inTac2Redefinition def) let perform_eval ~pstate e = - let open Proofview.Notations in let env = Global.env () in let (e, ty) = Tac2intern.intern ~strict:false e in let v = Tac2interp.interp Tac2interp.empty_environment e in @@ -761,12 +760,8 @@ let perform_eval ~pstate e = | Goal_select.SelectAll -> v | Goal_select.SelectAlreadyFocused -> assert false (* TODO **) in - (* HACK: the API doesn't allow to return a value *) - let ans = ref None in - let tac = (v >>= fun r -> ans := Some r; Proofview.tclUNIT ()) in - let (proof, _) = Proof.run_tactic (Global.env ()) tac proof in + let (proof, _, ans) = Proof.run_tactic (Global.env ()) v proof in let sigma = Proof.in_proof proof (fun sigma -> sigma) in - let ans = match !ans with None -> assert false | Some r -> r in let name = int_name () in Feedback.msg_notice (str "- : " ++ pr_glbtype name (snd ty) ++ spc () ++ str "=" ++ spc () ++ diff --git a/user-contrib/Ltac2/tac2ffi.ml b/user-contrib/Ltac2/tac2ffi.ml index e3127ab9df..1043d25a75 100644 --- a/user-contrib/Ltac2/tac2ffi.ml +++ b/user-contrib/Ltac2/tac2ffi.ml @@ -30,6 +30,8 @@ type valexpr = (** Open constructors *) | ValExt : 'a Tac2dyn.Val.tag * 'a -> valexpr (** Arbitrary data *) +| ValUint63 of Uint63.t + (** Primitive integers *) and closure = MLTactic : (valexpr, 'v) arity0 * 'v -> closure @@ -47,21 +49,21 @@ type t = valexpr let is_int = function | ValInt _ -> true -| ValBlk _ | ValStr _ | ValCls _ | ValOpn _ | ValExt _ -> false +| ValBlk _ | ValStr _ | ValCls _ | ValOpn _ | ValExt _ | ValUint63 _ -> false let tag v = match v with | ValBlk (n, _) -> n -| ValInt _ | ValStr _ | ValCls _ | ValOpn _ | ValExt _ -> +| ValInt _ | ValStr _ | ValCls _ | ValOpn _ | ValExt _ | ValUint63 _ -> CErrors.anomaly (Pp.str "Unexpected value shape") let field v n = match v with | ValBlk (_, v) -> v.(n) -| ValInt _ | ValStr _ | ValCls _ | ValOpn _ | ValExt _ -> +| ValInt _ | ValStr _ | ValCls _ | ValOpn _ | ValExt _ | ValUint63 _ -> CErrors.anomaly (Pp.str "Unexpected value shape") let set_field v n w = match v with | ValBlk (_, v) -> v.(n) <- w -| ValInt _ | ValStr _ | ValCls _ | ValOpn _ | ValExt _ -> +| ValInt _ | ValStr _ | ValCls _ | ValOpn _ | ValExt _ | ValUint63 _ -> CErrors.anomaly (Pp.str "Unexpected value shape") let make_block tag v = ValBlk (tag, v) @@ -192,7 +194,7 @@ let of_closure cls = ValCls cls let to_closure = function | ValCls cls -> cls -| ValExt _ | ValInt _ | ValBlk _ | ValStr _ | ValOpn _ -> assert false +| ValExt _ | ValInt _ | ValBlk _ | ValStr _ | ValOpn _ | ValUint63 _ -> assert false let closure = { r_of = of_closure; @@ -318,6 +320,17 @@ let open_ = { r_id = false; } +let of_uint63 n = ValUint63 n +let to_uint63 = function +| ValUint63 n -> n +| _ -> assert false + +let uint63 = { + r_of = of_uint63; + r_to = to_uint63; + r_id = false; +} + let of_constant c = of_ext val_constant c let to_constant c = to_ext val_constant c let constant = repr_ext val_constant diff --git a/user-contrib/Ltac2/tac2ffi.mli b/user-contrib/Ltac2/tac2ffi.mli index bfc93d99e6..f8581061a0 100644 --- a/user-contrib/Ltac2/tac2ffi.mli +++ b/user-contrib/Ltac2/tac2ffi.mli @@ -28,6 +28,8 @@ type valexpr = (** Open constructors *) | ValExt : 'a Tac2dyn.Val.tag * 'a -> valexpr (** Arbitrary data *) +| ValUint63 of Uint63.t + (** Primitive integers *) type 'a arity @@ -143,6 +145,10 @@ val of_open : KerName.t * valexpr array -> valexpr val to_open : valexpr -> KerName.t * valexpr array val open_ : (KerName.t * valexpr array) repr +val of_uint63 : Uint63.t -> valexpr +val to_uint63 : valexpr -> Uint63.t +val uint63 : Uint63.t repr + type ('a, 'b) fun1 val app_fun1 : ('a, 'b) fun1 -> 'a repr -> 'b repr -> 'a -> 'b Proofview.tactic diff --git a/vernac/classes.ml b/vernac/classes.ml index 9f233a2551..ece9fc8937 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -374,6 +374,7 @@ let declare_instance_open ~pstate env sigma ?hook ~tac ~program_mode ~global ~po let obls, constr, typ = match term with | Some t -> + let termtype = EConstr.of_constr termtype in let obls, _, constr, typ = Obligations.eterm_obligations env id sigma 0 t termtype in obls, Some constr, typ @@ -400,7 +401,7 @@ let declare_instance_open ~pstate env sigma ?hook ~tac ~program_mode ~global ~po if not (Option.is_empty term) then let init_refine = Tacticals.New.tclTHENLIST [ - Refine.refine ~typecheck:false (fun sigma -> (sigma,EConstr.of_constr (Option.get term))); + Refine.refine ~typecheck:false (fun sigma -> (sigma, Option.get term)); Proofview.Unsafe.tclNEWGOALS (CList.map Proofview.with_empty_state gls); Tactics.New.reduce_after_refine; ] @@ -497,10 +498,10 @@ let do_instance ~pstate env env' sigma ?hook ~refine ~tac ~global ~poly ~program (* Check that the type is free of evars now. *) Pretyping.check_evars env (Evd.from_env env) sigma termtype; let termtype = to_constr sigma termtype in - let term = Option.map (to_constr ~abort_on_undefined_evars:false sigma) term in let pstate = if not (Evd.has_undefined sigma) && not (Option.is_empty props) then - (declare_instance_constant k pri global imps ?hook id decl poly sigma (Option.get term) termtype; + let term = to_constr sigma (Option.get term) in + (declare_instance_constant k pri global imps ?hook id decl poly sigma term termtype; None) else if program_mode || refine || Option.is_empty props then declare_instance_open ~pstate env sigma ?hook ~tac ~program_mode ~global ~poly k id pri imps decl (List.map RelDecl.get_name ctx) term termtype diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml index 12df3215ad..d2c986fe5c 100644 --- a/vernac/comDefinition.ml +++ b/vernac/comDefinition.ml @@ -88,11 +88,12 @@ let do_definition ~ontop ~program_mode ?hook ident k univdecl bl red_option c ct let (c,ctx), sideff = Future.force ce.const_entry_body in assert(Safe_typing.empty_private_constants = sideff); assert(Univ.ContextSet.is_empty ctx); + Obligations.check_evars env evd; + let c = EConstr.of_constr c in let typ = match ce.const_entry_type with - | Some t -> t - | None -> EConstr.to_constr ~abort_on_undefined_evars:false evd (Retyping.get_type_of env evd (EConstr.of_constr c)) + | Some t -> EConstr.of_constr t + | None -> Retyping.get_type_of env evd c in - Obligations.check_evars env evd; let obls, _, c, cty = Obligations.eterm_obligations env ident evd 0 c typ in diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml index 20a2db7ca2..69e2a209eb 100644 --- a/vernac/comProgramFixpoint.ml +++ b/vernac/comProgramFixpoint.ml @@ -230,12 +230,9 @@ let build_wellfounded (recname,pl,bl,arityc,body) poly r measure notation = in (* XXX: Capturing sigma here... bad bad *) let hook = Lemmas.mk_hook (hook sigma) in - (* XXX: Grounding non-ground terms here... bad bad *) - let fullcoqc = EConstr.to_constr ~abort_on_undefined_evars:false sigma def in - let fullctyp = EConstr.to_constr ~abort_on_undefined_evars:false sigma typ in Obligations.check_evars env sigma; let evars, _, evars_def, evars_typ = - Obligations.eterm_obligations env recname sigma 0 fullcoqc fullctyp + Obligations.eterm_obligations env recname sigma 0 def typ in let ctx = Evd.evar_universe_context sigma in ignore(Obligations.add_definition recname ~term:evars_def ~univdecl:decl @@ -246,7 +243,7 @@ let out_def = function | None -> user_err Pp.(str "Program Fixpoint needs defined bodies.") let collect_evars_of_term evd c ty = - let evars = Evar.Set.union (Evd.evars_of_term c) (Evd.evars_of_term ty) in + let evars = Evar.Set.union (Evd.evars_of_term evd c) (Evd.evars_of_term evd ty) in Evar.Set.fold (fun ev acc -> Evd.add acc ev (Evd.find_undefined evd ev)) evars (Evd.from_ctx (Evd.evar_universe_context evd)) @@ -262,17 +259,13 @@ let do_program_recursive local poly fixkind fixl ntns = let evd = nf_evar_map_undefined evd in let collect_evars id def typ imps = (* Generalize by the recursive prototypes *) - let def = - EConstr.to_constr ~abort_on_undefined_evars:false evd (Termops.it_mkNamedLambda_or_LetIn def rec_sign) - and typ = - (* Worrying... *) - EConstr.to_constr ~abort_on_undefined_evars:false evd (Termops.it_mkNamedProd_or_LetIn typ rec_sign) - in + let def = nf_evar evd (Termops.it_mkNamedLambda_or_LetIn def rec_sign) in + let typ = nf_evar evd (Termops.it_mkNamedProd_or_LetIn typ rec_sign) in let evm = collect_evars_of_term evd def typ in let evars, _, def, typ = Obligations.eterm_obligations env id evm - (List.length rec_sign) def typ - in (id, def, typ, imps, evars) + (List.length rec_sign) def typ in + (id, def, typ, imps, evars) in let (fixnames,fixrs,fixdefs,fixtypes) = fix in let fiximps = List.map pi2 info in diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index 1c7cc5e636..317cf487cc 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -75,13 +75,7 @@ let adjust_guardness_conditions const = function List.interval 0 (List.length ((lam_assum c)))) lemma_guard (Array.to_list fixdefs) in *) - let fold env eff = - try - let _ = Environ.lookup_constant eff.seff_constant env in - env - with Not_found -> Environ.add_constant eff.seff_constant eff.seff_body env - in - let env = List.fold_left fold env (Safe_typing.side_effects_of_private_constants eff) in + let env = Safe_typing.push_private_constants env eff in let indexes = search_guard env possible_indexes fixdecls in @@ -395,10 +389,10 @@ let start_proof_with_initialization ~ontop ?hook kind sigma decl recguard thms s maybe_declare_manual_implicits false ref imps; call_hook ?hook ctx [] strength ref) thms_data in let pstate = start_proof ~ontop id ~pl:decl kind sigma t ~hook ~compute_guard:guard in - let pstate, _ = Proof_global.with_current_proof (fun _ p -> + let pstate = Proof_global.simple_with_current_proof (fun _ p -> match init_tac with - | None -> p,(true,[]) - | Some tac -> Proof.run_tactic Global.(env ()) tac p) pstate in + | None -> p + | Some tac -> pi1 @@ Proof.run_tactic Global.(env ()) tac p) pstate in pstate let start_proof_com ~program_mode ~ontop ?inference_hook ?hook kind thms = diff --git a/vernac/obligations.ml b/vernac/obligations.ml index 1b1c618dc7..f768278dd7 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -39,7 +39,7 @@ let check_evars env evm = type oblinfo = { ev_name: int * Id.t; - ev_hyps: Constr.named_context; + ev_hyps: EConstr.named_context; ev_status: bool * Evar_kinds.obligation_definition_status; ev_chop: int option; ev_src: Evar_kinds.t Loc.located; @@ -50,11 +50,11 @@ type oblinfo = (** Substitute evar references in t using de Bruijn indices, where n binders were passed through. *) -let subst_evar_constr evs n idf t = +let subst_evar_constr evm evs n idf t = let seen = ref Int.Set.empty in let transparent = ref Id.Set.empty in let evar_info id = List.assoc_f Evar.equal id evs in - let rec substrec (depth, fixrels) c = match Constr.kind c with + let rec substrec (depth, fixrels) c = match EConstr.kind evm c with | Evar (k, args) -> let { ev_name = (id, idstr) ; ev_hyps = hyps ; ev_chop = chop } = @@ -84,18 +84,18 @@ let subst_evar_constr evs n idf t = in aux hyps args [] in if List.exists - (fun x -> match Constr.kind x with + (fun x -> match EConstr.kind evm x with | Rel n -> Int.List.mem n fixrels | _ -> false) args then transparent := Id.Set.add idstr !transparent; - mkApp (idf idstr, Array.of_list args) + EConstr.mkApp (idf idstr, Array.of_list args) | Fix _ -> - Constr.map_with_binders succfix substrec (depth, 1 :: fixrels) c - | _ -> Constr.map_with_binders succfix substrec (depth, fixrels) c + EConstr.map_with_binders evm succfix substrec (depth, 1 :: fixrels) c + | _ -> EConstr.map_with_binders evm succfix substrec (depth, fixrels) c in let t' = substrec (0, []) t in - t', !seen, !transparent + EConstr.to_constr evm t', !seen, !transparent (** Substitute variable references in t using de Bruijn indices, @@ -112,18 +112,18 @@ let subst_vars acc n t = to a product : forall H1 : t1, ..., forall Hn : tn, concl. Changes evars and hypothesis references to variable references. *) -let etype_of_evar evs hyps concl = +let etype_of_evar evm evs hyps concl = let open Context.Named.Declaration in let rec aux acc n = function decl :: tl -> - let t', s, trans = subst_evar_constr evs n mkVar (NamedDecl.get_type decl) in + let t', s, trans = subst_evar_constr evm evs n EConstr.mkVar (NamedDecl.get_type decl) in let t'' = subst_vars acc 0 t' in let rest, s', trans' = aux (NamedDecl.get_id decl :: acc) (succ n) tl in let s' = Int.Set.union s s' in let trans' = Id.Set.union trans trans' in (match decl with | LocalDef (id,c,_) -> - let c', s'', trans'' = subst_evar_constr evs n mkVar c in + let c', s'', trans'' = subst_evar_constr evm evs n EConstr.mkVar c in let c' = subst_vars acc 0 c' in mkNamedProd_or_LetIn (LocalDef (id, c', t'')) rest, Int.Set.union s'' s', @@ -131,7 +131,7 @@ let etype_of_evar evs hyps concl = | LocalAssum (id,_) -> mkNamedProd_or_LetIn (LocalAssum (id, t'')) rest, s', trans') | [] -> - let t', s, trans = subst_evar_constr evs n mkVar concl in + let t', s, trans = subst_evar_constr evm evs n EConstr.mkVar concl in subst_vars acc 0 t', s, trans in aux [] 0 (List.rev hyps) @@ -151,7 +151,7 @@ let evar_dependencies evm oev = let one_step deps = Evar.Set.fold (fun ev s -> let evi = Evd.find evm ev in - let deps' = evars_of_filtered_evar_info evi in + let deps' = evars_of_filtered_evar_info evm evi in if Evar.Set.mem oev deps' then invalid_arg ("Ill-formed evar map: cycle detected for evar " ^ Pp.string_of_ppcmds @@ Evar.print oev) else Evar.Set.union deps' s) @@ -209,9 +209,7 @@ let eterm_obligations env name evm fs ?status t ty = (fun (id, (n, nstr), ev) l -> let hyps = Evd.evar_filtered_context ev in let hyps = trunc_named_context nc_len hyps in - let hyps = EConstr.Unsafe.to_named_context hyps in - let concl = EConstr.Unsafe.to_constr ev.evar_concl in - let evtyp, deps, transp = etype_of_evar l hyps concl in + let evtyp, deps, transp = etype_of_evar evm l hyps ev.evar_concl in let evtyp, hyps, chop = match chop_product fs evtyp with | Some t -> t, trunc_named_context fs hyps, fs @@ -237,9 +235,9 @@ let eterm_obligations env name evm fs ?status t ty = evn [] in let t', _, transparent = (* Substitute evar refs in the term by variables *) - subst_evar_constr evts 0 mkVar t + subst_evar_constr evm evts 0 EConstr.mkVar t in - let ty, _, _ = subst_evar_constr evts 0 mkVar ty in + let ty, _, _ = subst_evar_constr evm evts 0 EConstr.mkVar ty in let evars = List.map (fun (ev, info) -> let { ev_name = (_, name); ev_status = force_status, status; @@ -252,7 +250,7 @@ let eterm_obligations env name evm fs ?status t ty = in name, typ, src, (force_status, status), deps, tac) evts in let evnames = List.map (fun (ev, info) -> ev, snd info.ev_name) evts in - let evmap f c = pi1 (subst_evar_constr evts 0 f c) in + let evmap f c = pi1 (subst_evar_constr evm evts 0 f c) in Array.of_list (List.rev evars), (evnames, evmap), t', ty let hide_obligation () = diff --git a/vernac/obligations.mli b/vernac/obligations.mli index d25daeed9c..9214ddd4b9 100644 --- a/vernac/obligations.mli +++ b/vernac/obligations.mli @@ -26,14 +26,14 @@ val sort_dependencies : (Evar.t * evar_info * Evar.Set.t) list -> (Evar.t * evar (* env, id, evars, number of function prototypes to try to clear from evars contexts, object and type *) val eterm_obligations : env -> Id.t -> evar_map -> int -> - ?status:Evar_kinds.obligation_definition_status -> constr -> types -> + ?status:Evar_kinds.obligation_definition_status -> EConstr.constr -> EConstr.types -> (Id.t * types * Evar_kinds.t Loc.located * (bool * Evar_kinds.obligation_definition_status) * Int.Set.t * unit Proofview.tactic option) array (* Existential key, obl. name, type as product, location of the original evar, associated tactic, status and dependencies as indexes into the array *) - * ((Evar.t * Id.t) list * ((Id.t -> constr) -> constr -> constr)) * + * ((Evar.t * Id.t) list * ((Id.t -> EConstr.constr) -> EConstr.constr -> constr)) * constr * types (* Translations from existential identifiers to obligation identifiers and for terms with existentials to closed terms, given a |