diff options
30 files changed, 403 insertions, 312 deletions
diff --git a/dev/bench/gitlab-bench.yml b/dev/bench/gitlab-bench.yml index a2207081f4..4275e3d121 100644 --- a/dev/bench/gitlab-bench.yml +++ b/dev/bench/gitlab-bench.yml @@ -28,5 +28,10 @@ bench: paths: - _bench/html/**/*.v.html - _bench/logs + - _bench/files.listing + - _bench/opam.NEW/**/*.log + - _bench/opam.NEW/**/*.timing + - _bench/opam.OLD/**/*.log + - _bench/opam.OLD/**/*.timing when: always expire_in: 1 year diff --git a/dev/bench/gitlab.sh b/dev/bench/gitlab.sh index 38b4e25bde..7625e4e7f7 100755 --- a/dev/bench/gitlab.sh +++ b/dev/bench/gitlab.sh @@ -12,6 +12,9 @@ r='\033[0m' # reset (all attributes off) b='\033[1m' # bold u='\033[4m' # underline nl=$'\n' +bt='`' # backtick +start_code_block='```' +end_code_block='```' number_of_processors=$(cat /proc/cpuinfo | grep '^processor *' | wc -l) @@ -36,6 +39,7 @@ echo $PWD #check_variable "BUILD_URL" #check_variable "JOB_NAME" #check_variable "JENKINS_URL" +check_variable "CI_JOB_URL" check_variable "coq_pr_number" check_variable "coq_pr_comment_id" check_variable "new_ocaml_switch" @@ -61,8 +65,9 @@ else exit 1 fi -mkdir -p "_bench" -working_dir="$PWD/_bench" +bench_dirname="_bench" +mkdir -p "${bench_dirname}" +working_dir="$PWD/${bench_dirname}" log_dir=$working_dir/logs mkdir "$log_dir" @@ -109,6 +114,15 @@ else exit 1 fi +if which du > /dev/null; then + : +else + echo > /dev/stderr + echo "ERROR: \"du\" program is not available." > /dev/stderr + echo > /dev/stderr + exit 1 +fi + if [ ! -e "$working_dir" ]; then echo > /dev/stderr echo "ERROR: \"$working_dir\" does not exist." > /dev/stderr @@ -146,22 +160,31 @@ function coqbot_update_comment() { if [ ! -z "${coq_pr_number}" ]; then comment_text="" + artifact_text="" if [ -z "${is_done}" ]; then comment_text="in progress, " + artifact_text="eventually " else comment_text="" + artifact_text="" fi - comment_text="Benchmarking ${comment_text}log available [here](${BUILD_URL}/console), workspace available [here](${JENKINS_URL}/view/benchmarking/job/${JOB_NAME}/ws/${BUILD_ID})" + comment_text="Benchmarking ${comment_text}log available [here](${CI_JOB_URL}) ([raw log here](${CI_JOB_URL}/raw)), artifacts ${artifact_text}available for [download](${CI_JOB_URL}/artifacts/download) and [browsing](${CI_JOB_URL}/artifacts/browse)" if [ ! -z "${comment_body}" ]; then - comment_text="${comment_text}${nl}"'```'"${nl}${comment_body}${nl}"'```' + comment_text="${comment_text}${nl}${start_code_block}${nl}${comment_body}${nl}${end_code_block}" fi if [ ! -z "${uninstallable_packages}" ]; then comment_text="${comment_text}${nl}The following packages failed to install: ${uninstallable_packages}" fi + comment_text="${comment_text}${nl}${nl}<details><summary>Old Coq version ${old_coq_commit}</summary>" + comment_text="${comment_text}${nl}${nl}${start_code_block}${nl}$(git log -n 1 "${old_coq_commit}")${nl}${end_code_block}${nl}</details>" + comment_text="${comment_text}${nl}${nl}<details><summary>New Coq version ${new_coq_commit}</summary>" + comment_text="${comment_text}${nl}${nl}${start_code_block}${nl}$(git log -n 1 "${new_coq_commit}")${nl}${end_code_block}${nl}</details>" + comment_text="${comment_text}${nl}${nl}[Diff: ${bt}${old_coq_commit}..${new_coq_commit}${bt}](https://github.com/coq/coq/compare/${old_coq_commit}..${new_coq_commit})" + # if there's a comment id, we update the comment while we're # in progress; otherwise, we wait until the end to post a new # comment @@ -416,6 +439,11 @@ for coq_opam_package in $sorted_coq_opam_packages; do done done +# Since we do not upload all files, store a list of the files +# available so that if we at some point want to tweak which files we +# upload, we'll know which ones are available for upload +du -ha "$working_dir" > "$working_dir/files.listing" + # The following directories in $working_dir are no longer used: # # - coq, opam.OLD, opam.NEW @@ -430,7 +458,7 @@ done # # The next script processes all these files and prints results in a table. -echo "INFO: workspace = https://ci.inria.fr/coq/view/benchmarking/job/$JOB_NAME/ws/$BUILD_ID" +echo "INFO: workspace = ${CI_JOB_URL}/artifacts/browse/${bench_dirname}" # Print the final results. if [ -z "$installable_coq_opam_packages" ]; then @@ -444,7 +472,7 @@ else rendered_results="$($program_path/render_results "$log_dir" $num_of_iterations $new_coq_commit_long $old_coq_commit_long 0 user_time_pdiff $installable_coq_opam_packages)" echo "${rendered_results}" - echo "INFO: per line timing: https://ci.inria.fr/coq/job/$JOB_NAME/ws/$BUILD_ID/html/" + echo "INFO: per line timing: ${CI_JOB_URL}/artifacts/browse/${bench_dirname}/html/" cd "$coq_dir" echo INFO: Old Coq version diff --git a/dev/ci/user-overlays/12968-maximedenes-delay-frozen-evarconv.sh b/dev/ci/user-overlays/12968-maximedenes-delay-frozen-evarconv.sh new file mode 100644 index 0000000000..ee75944a52 --- /dev/null +++ b/dev/ci/user-overlays/12968-maximedenes-delay-frozen-evarconv.sh @@ -0,0 +1,6 @@ +if [ "$CI_PULL_REQUEST" = "12968" ] || [ "$CI_BRANCH" = "delay-frozen-evarconv" ]; then + + equations_CI_REF=delay-frozen-evarconv + equations_CI_GITURL=https://github.com/maximedenes/Coq-Equations + +fi diff --git a/doc/sphinx/addendum/micromega.rst b/doc/sphinx/addendum/micromega.rst index d7e4c9c804..070e899c9d 100644 --- a/doc/sphinx/addendum/micromega.rst +++ b/doc/sphinx/addendum/micromega.rst @@ -180,7 +180,7 @@ are a way to take into account the discreteness of :math:`\mathbb{Z}` by roundin Let :math:`p` be an integer and :math:`c` a rational constant. Then :math:`p \ge c \rightarrow p \ge \lceil{c}\rceil`. -For instance, from 2 x = 1 we can deduce +For instance, from :math:`2 x = 1` we can deduce + :math:`x \ge 1/2` whose cut plane is :math:`x \ge \lceil{1/2}\rceil = 1`; + :math:`x \le 1/2` whose cut plane is :math:`x \le \lfloor{1/2}\rfloor = 0`. diff --git a/engine/namegen.ml b/engine/namegen.ml index fb9f6db0ea..f398f29f41 100644 --- a/engine/namegen.ml +++ b/engine/namegen.ml @@ -273,8 +273,8 @@ let visible_ids sigma (nenv, c) = accu := (gseen, vseen, ids) | Rel p -> let (gseen, vseen, ids) = !accu in - if p > n && not (Int.Set.mem p vseen) then - let vseen = Int.Set.add p vseen in + if p > n && not (Int.Set.mem (p - n) vseen) then + let vseen = Int.Set.add (p - n) vseen in let name = try Some (List.nth nenv (p - n - 1)) with Invalid_argument _ | Failure _ -> @@ -290,7 +290,7 @@ let visible_ids sigma (nenv, c) = accu := (gseen, vseen, ids) | _ -> EConstr.iter_with_binders sigma succ visible_ids n c in - let () = visible_ids 1 c in + let () = visible_ids 1 c in (* n = 1 to count the binder to rename *) let (_, _, ids) = !accu in ids @@ -416,6 +416,8 @@ let next_name_away_for_default_printing sigma env_t na avoid = *) type renaming_flags = + (* The term is the body of a binder and the environment excludes this binder *) + (* so, there is a missing binder in the environment *) | RenamingForCasesPattern of (Name.t list * constr) | RenamingForGoal | RenamingElsewhereFor of (Name.t list * constr) diff --git a/kernel/uGraph.ml b/kernel/uGraph.ml index 927db9e9e6..52e93a9e22 100644 --- a/kernel/uGraph.ml +++ b/kernel/uGraph.ml @@ -142,6 +142,12 @@ let enforce_leq_alg u v g = | Inl x -> x | Inr e -> raise e +let enforce_leq_alg u v g = + match Universe.is_sprop u, Universe.is_sprop v with + | true, true -> Constraint.empty, g + | true, false | false, true -> raise (UniverseInconsistency (Le, u, v, None)) + | false, false -> enforce_leq_alg u v g + (* sanity check wrapper *) let enforce_leq_alg u v g = let _,g as cg = enforce_leq_alg u v g in diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index fb149071c9..a1dbf9a439 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -546,7 +546,7 @@ let rewrite_core_unif_flags = { Unification.check_applied_meta_types = true; Unification.use_pattern_unification = true; Unification.use_meta_bound_pattern_unification = true; - Unification.allowed_evars = Unification.AllowAll; + Unification.allowed_evars = Evarsolve.AllowedEvars.all; Unification.restrict_conv_on_strict_subterms = false; Unification.modulo_betaiota = false; Unification.modulo_eta = true; diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 489e8de602..61453ff214 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -40,7 +40,7 @@ let default_transparent_state env = TransparentState.full let default_flags_of ?(subterm_ts=TransparentState.empty) ts = { modulo_betaiota = true; open_ts = ts; closed_ts = ts; subterm_ts; - frozen_evars = Evar.Set.empty; with_cs = true; + allowed_evars = AllowedEvars.all; with_cs = true; allow_K_at_toplevel = true } let default_flags env = @@ -118,8 +118,6 @@ type flex_kind_of_term = | MaybeFlexible of EConstr.t (* reducible but not necessarily reduced *) | Flexible of EConstr.existential -let is_frozen flags (evk, _) = Evar.Set.mem evk flags.frozen_evars - let flex_kind_of_term flags env evd c sk = match EConstr.kind evd c with | LetIn _ | Rel _ | Const _ | Var _ | Proj _ -> @@ -128,8 +126,7 @@ let flex_kind_of_term flags env evd c sk = if flags.modulo_betaiota then MaybeFlexible c else Rigid | Evar ev -> - if is_frozen flags ev then Rigid - else Flexible ev + if is_evar_allowed flags (fst ev) then Flexible ev else Rigid | Lambda _ | Prod _ | Sort _ | Ind _ | Construct _ | CoFix _ | Int _ | Float _ | Array _ -> Rigid | Meta _ -> Rigid | Fix _ -> Rigid (* happens when the fixpoint is partially applied *) @@ -192,11 +189,11 @@ let occur_rigidly flags env evd (evk,_) t = | Rigid _ as res -> res | Normal b -> Reducible | Reducible -> Reducible) - | Evar (evk',l as ev) -> + | Evar (evk',l) -> if Evar.equal evk evk' then Rigid true - else if is_frozen flags ev then - Rigid (List.exists (fun x -> rigid_normal_occ (aux x)) l) - else Reducible + else if is_evar_allowed flags evk' then + Reducible + else Rigid (List.exists (fun x -> rigid_normal_occ (aux x)) l) | Cast (p, _, _) -> aux p | Lambda (na, t, b) -> aux b | LetIn (na, _, _, b) -> aux b @@ -458,7 +455,7 @@ let conv_fun f flags on_types = let typefn env evd pbty term1 term2 = let flags = { (default_flags env) with with_cs = flags.with_cs; - frozen_evars = flags.frozen_evars } + allowed_evars = flags.allowed_evars } in f flags env evd pbty term1 term2 in let termfn env evd pbty term1 term2 = @@ -500,7 +497,7 @@ let rec evar_conv_x flags env evd pbty term1 term2 = (whd_nored_state env evd (term2,Stack.empty)) in begin match EConstr.kind evd term1, EConstr.kind evd term2 with - | Evar ev, _ when Evd.is_undefined evd (fst ev) && not (is_frozen flags ev) -> + | Evar ev, _ when Evd.is_undefined evd (fst ev) && is_evar_allowed flags (fst ev) -> (match solve_simple_eqn (conv_fun evar_conv_x) flags env evd (position_problem true pbty,ev,term2) with | UnifFailure (_,(OccurCheck _ | NotClean _)) -> @@ -511,7 +508,7 @@ let rec evar_conv_x flags env evd pbty term1 term2 = Miller patterns *) default () | x -> x) - | _, Evar ev when Evd.is_undefined evd (fst ev) && not (is_frozen flags ev) -> + | _, Evar ev when Evd.is_undefined evd (fst ev) && is_evar_allowed flags (fst ev) -> (match solve_simple_eqn (conv_fun evar_conv_x) flags env evd (position_problem false pbty,ev,term1) with | UnifFailure (_, (OccurCheck _ | NotClean _)) -> @@ -1206,14 +1203,14 @@ type occurrences_selection = let default_occurrence_selection = Unspecified Abstraction.Imitate -let default_occurrence_test ~frozen_evars ts _ origsigma _ env sigma _ c pat = - let flags = { (default_flags_of ~subterm_ts:ts ts) with frozen_evars } in +let default_occurrence_test ~allowed_evars ts _ origsigma _ env sigma _ c pat = + let flags = { (default_flags_of ~subterm_ts:ts ts) with allowed_evars } in match evar_conv_x flags env sigma CONV c pat with | Success sigma -> true, sigma | UnifFailure _ -> false, sigma -let default_occurrences_selection ?(frozen_evars=Evar.Set.empty) ts n = - (default_occurrence_test ~frozen_evars ts, +let default_occurrences_selection ?(allowed_evars=AllowedEvars.all) ts n = + (default_occurrence_test ~allowed_evars ts, List.init n (fun _ -> default_occurrence_selection)) let apply_on_subterm env evd fixedref f test c t = @@ -1554,7 +1551,7 @@ let second_order_matching_with_args flags env evd with_ho pbty ev l t = if with_ho then let evd,ev = evar_absorb_arguments env evd ev (Array.to_list l) in let argoccs = default_evar_selection flags evd ev in - let test = default_occurrence_test ~frozen_evars:flags.frozen_evars flags.subterm_ts in + let test = default_occurrence_test ~allowed_evars:flags.allowed_evars flags.subterm_ts in let evd, b = try second_order_matching flags env evd ev (test,argoccs) t with PretypeError (_, _, NoOccurrenceFound _) -> evd, false @@ -1582,8 +1579,8 @@ let apply_conversion_problem_heuristic flags env evd with_ho pbty t1 t2 = Termops.Internal.print_constr_env env evd t2 ++ cut ())) in let app_empty = Array.is_empty l1 && Array.is_empty l2 in match EConstr.kind evd term1, EConstr.kind evd term2 with - | Evar (evk1,args1 as ev1), (Rel _|Var _) when app_empty - && not (is_frozen flags ev1) + | Evar (evk1,args1), (Rel _|Var _) when app_empty + && is_evar_allowed flags evk1 && List.for_all (fun a -> EConstr.eq_constr evd a term2 || isEvar evd a) (remove_instance_local_defs evd evk1 args1) -> (* The typical kind of constraint coming from pattern-matching return @@ -1593,8 +1590,8 @@ let apply_conversion_problem_heuristic flags env evd with_ho pbty t1 t2 = | None -> let reason = ProblemBeyondCapabilities in UnifFailure (evd, CannotSolveConstraint ((pbty,env,t1,t2),reason))) - | (Rel _|Var _), Evar (evk2,args2 as ev2) when app_empty - && not (is_frozen flags ev2) + | (Rel _|Var _), Evar (evk2,args2) when app_empty + && is_evar_allowed flags evk2 && List.for_all (fun a -> EConstr.eq_constr evd a term1 || isEvar evd a) (remove_instance_local_defs evd evk2 args2) -> (* The typical kind of constraint coming from pattern-matching return @@ -1620,24 +1617,24 @@ let apply_conversion_problem_heuristic flags env evd with_ho pbty t1 t2 = (evar_define evar_unify flags ~choose:true) evar_unify flags env evd (position_problem true pbty) ev1 ev2) - | Evar ev1,_ when not (is_frozen flags ev1) && Array.length l1 <= Array.length l2 -> + | Evar ev1,_ when is_evar_allowed flags (fst ev1) && Array.length l1 <= Array.length l2 -> (* On "?n t1 .. tn = u u1 .. u(n+p)", try first-order unification *) (* and otherwise second-order matching *) ise_try evd [(fun evd -> first_order_unification flags env evd (ev1,l1) appr2); (fun evd -> second_order_matching_with_args flags env evd with_ho pbty ev1 l1 t2)] - | _,Evar ev2 when not (is_frozen flags ev2) && Array.length l2 <= Array.length l1 -> + | _,Evar ev2 when is_evar_allowed flags (fst ev2) && Array.length l2 <= Array.length l1 -> (* On "u u1 .. u(n+p) = ?n t1 .. tn", try first-order unification *) (* and otherwise second-order matching *) ise_try evd [(fun evd -> first_order_unification flags env evd (ev2,l2) appr1); (fun evd -> second_order_matching_with_args flags env evd with_ho pbty ev2 l2 t1)] - | Evar ev1,_ when not (is_frozen flags ev1) -> + | Evar ev1,_ when is_evar_allowed flags (fst ev1) -> (* Try second-order pattern-matching *) second_order_matching_with_args flags env evd with_ho pbty ev1 l1 t2 - | _,Evar ev2 when not (is_frozen flags ev2) -> + | _,Evar ev2 when is_evar_allowed flags (fst ev2) -> (* Try second-order pattern-matching *) second_order_matching_with_args flags env evd with_ho pbty ev2 l2 t1 | _ -> diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli index 767a173131..a5a8d1f916 100644 --- a/pretyping/evarconv.mli +++ b/pretyping/evarconv.mli @@ -105,11 +105,11 @@ val default_occurrence_selection : occurrence_selection type occurrences_selection = occurrence_match_test * occurrence_selection list -val default_occurrence_test : frozen_evars:Evar.Set.t -> TransparentState.t -> occurrence_match_test +val default_occurrence_test : allowed_evars:Evarsolve.AllowedEvars.t -> TransparentState.t -> occurrence_match_test (** [default_occurrence_selection n] Gives the default test and occurrences for [n] arguments *) -val default_occurrences_selection : ?frozen_evars:Evar.Set.t (* By default, none *) -> +val default_occurrences_selection : ?allowed_evars:Evarsolve.AllowedEvars.t (* By default, all *) -> TransparentState.t -> int -> occurrences_selection val second_order_matching : unify_flags -> env -> evar_map -> diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index 989fb05c3d..4d5715a391 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -25,14 +25,43 @@ open Reductionops open Evarutil open Pretype_errors +module AllowedEvars = struct + + type t = + | AllowAll + | AllowFun of (Evar.t -> bool) * Evar.Set.t + + let mem allowed evk = + match allowed with + | AllowAll -> true + | AllowFun (f,except) -> f evk && not (Evar.Set.mem evk except) + + let remove evk = function + | AllowAll -> AllowFun ((fun _ -> true), Evar.Set.singleton evk) + | AllowFun (f,except) -> AllowFun (f, Evar.Set.add evk except) + + let all = AllowAll + + let except evars = + AllowFun ((fun _ -> true), evars) + + let from_pred f = + AllowFun (f, Evar.Set.empty) + +end + type unify_flags = { modulo_betaiota: bool; open_ts : TransparentState.t; closed_ts : TransparentState.t; subterm_ts : TransparentState.t; - frozen_evars : Evar.Set.t; + allowed_evars : AllowedEvars.t; allow_K_at_toplevel : bool; - with_cs : bool } + with_cs : bool +} + +let is_evar_allowed flags evk = + AllowedEvars.mem flags.allowed_evars evk type unification_kind = | TypeUnification @@ -1307,24 +1336,24 @@ let preferred_orientation evd evk1 evk2 = let solve_evar_evar_aux force f unify flags env evd pbty (evk1,args1 as ev1) (evk2,args2 as ev2) = let aliases = make_alias_map env evd in - let frozen_ev1 = Evar.Set.mem evk1 flags.frozen_evars in - let frozen_ev2 = Evar.Set.mem evk2 flags.frozen_evars in + let allowed_ev1 = is_evar_allowed flags evk1 in + let allowed_ev2 = is_evar_allowed flags evk2 in if preferred_orientation evd evk1 evk2 then - try if not frozen_ev1 then + try if allowed_ev1 then solve_evar_evar_l2r force f unify flags env evd aliases (opp_problem pbty) ev2 ev1 else raise (CannotProject (evd,ev2)) with CannotProject (evd,ev2) -> - try if not frozen_ev2 then + try if allowed_ev2 then solve_evar_evar_l2r force f unify flags env evd aliases pbty ev1 ev2 else raise (CannotProject (evd,ev1)) with CannotProject (evd,ev1) -> add_conv_oriented_pb ~tail:true (pbty,env,mkEvar ev1,mkEvar ev2) evd else - try if not frozen_ev2 then + try if allowed_ev2 then solve_evar_evar_l2r force f unify flags env evd aliases pbty ev1 ev2 else raise (CannotProject (evd,ev1)) with CannotProject (evd,ev1) -> - try if not frozen_ev1 then + try if allowed_ev1 then solve_evar_evar_l2r force f unify flags env evd aliases (opp_problem pbty) ev2 ev1 else raise (CannotProject (evd,ev2)) with CannotProject (evd,ev2) -> @@ -1390,15 +1419,15 @@ let solve_refl ?(can_drop=false) unify flags env evd pbty evk argsv1 argsv2 = let candidates = filter_candidates evd evk untypedfilter NoUpdate in let filter = closure_of_filter evd evk untypedfilter in let evd',ev1 = restrict_applied_evar evd (evk,argsv1) filter candidates in - let frozen = Evar.Set.mem evk flags.frozen_evars in - if Evar.equal (fst ev1) evk && (frozen || can_drop) then + let allowed = is_evar_allowed flags evk in + if Evar.equal (fst ev1) evk && (not allowed || can_drop) then (* No refinement needed *) evd' else (* either progress, or not allowed to drop, e.g. to preserve possibly *) (* informative equations such as ?e[x:=?y]=?e[x:=?y'] where we don't know *) (* if e can depend on x until ?y is not resolved, or, conversely, we *) (* don't know if ?y has to be unified with ?y, until e is resolved *) - if frozen then + if not allowed then (* We cannot prune a frozen evar *) add_conv_oriented_pb (pbty,env,mkEvar (evk, argsv1),mkEvar (evk,argsv2)) evd else @@ -1455,7 +1484,8 @@ let occur_evar_upto_types sigma n c = let instantiate_evar unify flags env evd evk body = (* Check instance freezing the evar to be defined, as checking could involve the same evar definition problem again otherwise *) - let flags = { flags with frozen_evars = Evar.Set.add evk flags.frozen_evars } in + let allowed_evars = AllowedEvars.remove evk flags.allowed_evars in + let flags = { flags with allowed_evars } in let evd' = check_evar_instance unify flags env evd evk body in Evd.define evk body evd' diff --git a/pretyping/evarsolve.mli b/pretyping/evarsolve.mli index 3fb80432ad..8ff2d7fc63 100644 --- a/pretyping/evarsolve.mli +++ b/pretyping/evarsolve.mli @@ -16,6 +16,28 @@ type alias val of_alias : alias -> EConstr.t +module AllowedEvars : sig + + type t + (** Represents the set of evars that can be defined by the pretyper *) + + val all : t + (** All evars can be defined *) + + val mem : t -> Evar.t -> bool + (** [mem allowed evk] is true iff evk can be defined *) + + val from_pred : (Evar.t -> bool) -> t + (** [from_pred p] means evars satisfying p can be defined *) + + val except : Evar.Set.t -> t + (** [except evars] means all evars can be defined except the ones in [evars] *) + + val remove : Evar.t -> t -> t + (** [remove evk allowed] removes [evk] from the set of evars allowed by [allowed] *) + +end + type unify_flags = { modulo_betaiota : bool; (* Enable beta-iota reductions during unification *) @@ -26,8 +48,8 @@ type unify_flags = { subterm_ts : TransparentState.t; (* Enable delta reduction according to subterm_ts for selection of subterms during higher-order unifications. *) - frozen_evars : Evar.Set.t; - (* Frozen evars are treated like rigid variables during unification: they can not be instantiated. *) + allowed_evars : AllowedEvars.t; + (* Disallowed evars are treated like rigid variables during unification: they can not be instantiated. *) allow_K_at_toplevel : bool; (* During higher-order unifications, allow to produce K-redexes: i.e. to produce an abstraction for an unused argument *) @@ -41,6 +63,8 @@ type unification_result = val is_success : unification_result -> bool +val is_evar_allowed : unify_flags -> Evar.t -> bool + (** Replace the vars and rels that are aliases to other vars and rels by their representative that is most ancient in the context *) val expand_vars_in_term : env -> evar_map -> constr -> constr diff --git a/pretyping/unification.ml b/pretyping/unification.ml index a26c981cb9..207a03d80f 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -252,10 +252,6 @@ let unify_r2l x = x let sort_eqns = unify_r2l *) -type allowed_evars = -| AllowAll -| AllowFun of (Evar.t -> bool) - type core_unify_flags = { modulo_conv_on_closed_terms : TransparentState.t option; (* What this flag controls was activated with all constants transparent, *) @@ -289,7 +285,7 @@ type core_unify_flags = { (* This allowed for instance to unify "forall x:?A, ?B x" with "A' -> B'" *) (* when ?B is a Meta. *) - allowed_evars : allowed_evars; + allowed_evars : AllowedEvars.t; (* Evars that are allowed to be instantiated *) (* Useful e.g. for autorewrite *) @@ -341,7 +337,7 @@ let default_core_unify_flags () = check_applied_meta_types = true; use_pattern_unification = true; use_meta_bound_pattern_unification = true; - allowed_evars = AllowAll; + allowed_evars = AllowedEvars.all; restrict_conv_on_strict_subterms = false; modulo_betaiota = true; modulo_eta = true; @@ -421,7 +417,7 @@ let default_no_delta_unify_flags ts = let allow_new_evars sigma = let undefined = Evd.undefined_map sigma in - AllowFun (fun evk -> not (Evar.Map.mem evk undefined)) + AllowedEvars.from_pred (fun evk -> not (Evar.Map.mem evk undefined)) (* Default flags for looking for subterms in elimination tactics *) (* Not used in practice at the current date, to the exception of *) @@ -604,9 +600,8 @@ let do_reduce ts (env, nb) sigma c = Stack.zip sigma (whd_betaiota_deltazeta_for_iota_state ts env sigma (c, Stack.empty)) -let is_evar_allowed flags evk = match flags.allowed_evars with -| AllowAll -> true -| AllowFun f -> f evk +let is_evar_allowed flags evk = + AllowedEvars.mem flags.allowed_evars evk let isAllowedEvar sigma flags c = match EConstr.kind sigma c with | Evar (evk,_) -> is_evar_allowed flags evk diff --git a/pretyping/unification.mli b/pretyping/unification.mli index f9a969a253..5462e09359 100644 --- a/pretyping/unification.mli +++ b/pretyping/unification.mli @@ -13,10 +13,6 @@ open EConstr open Environ open Evd -type allowed_evars = -| AllowAll -| AllowFun of (Evar.t -> bool) - type core_unify_flags = { modulo_conv_on_closed_terms : TransparentState.t option; use_metas_eagerly_in_conv_on_closed_terms : bool; @@ -26,7 +22,7 @@ type core_unify_flags = { check_applied_meta_types : bool; use_pattern_unification : bool; use_meta_bound_pattern_unification : bool; - allowed_evars : allowed_evars; + allowed_evars : Evarsolve.AllowedEvars.t; restrict_conv_on_strict_subterms : bool; modulo_betaiota : bool; modulo_eta : bool; diff --git a/proofs/clenv.ml b/proofs/clenv.ml index db76d08736..8e3cab70ea 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -673,7 +673,7 @@ let fail_quick_core_unif_flags = { check_applied_meta_types = false; use_pattern_unification = false; use_meta_bound_pattern_unification = true; (* ? *) - allowed_evars = AllowAll; + allowed_evars = Evarsolve.AllowedEvars.all; restrict_conv_on_strict_subterms = false; (* ? *) modulo_betaiota = false; modulo_eta = true; diff --git a/tactics/auto.ml b/tactics/auto.ml index 784322679f..369508c2a3 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -47,7 +47,7 @@ let auto_core_unif_flags_of st1 st2 = { check_applied_meta_types = false; use_pattern_unification = false; use_meta_bound_pattern_unification = true; - allowed_evars = AllowAll; + allowed_evars = Evarsolve.AllowedEvars.all; restrict_conv_on_strict_subterms = false; (* Compat *) modulo_betaiota = false; modulo_eta = true; diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index d969dea19e..96cbbf0ba8 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -134,7 +134,7 @@ let auto_core_unif_flags st allowed_evars = { modulo_eta = false; } -let auto_unif_flags ?(allowed_evars = AllowAll) st = +let auto_unif_flags ?(allowed_evars = Evarsolve.AllowedEvars.all) st = let fl = auto_core_unif_flags st allowed_evars in { core_unify_flags = fl; merge_unify_flags = fl; @@ -307,10 +307,10 @@ and e_my_find_search db_list local_db secvars hdc complete only_classes env sigm if cl.cl_strict then let undefined = lazy (Evarutil.undefined_evars_of_term sigma concl) in let allowed evk = not (Evar.Set.mem evk (Lazy.force undefined)) in - AllowFun allowed - else AllowAll - | _ -> AllowAll - with e when CErrors.noncritical e -> AllowAll + Evarsolve.AllowedEvars.from_pred allowed + else Evarsolve.AllowedEvars.all + | _ -> Evarsolve.AllowedEvars.all + with e when CErrors.noncritical e -> Evarsolve.AllowedEvars.all in let tac_of_hint = fun (flags, h) -> diff --git a/tactics/elim.ml b/tactics/elim.ml index 274ebc9f60..852ad626e1 100644 --- a/tactics/elim.ml +++ b/tactics/elim.ml @@ -10,33 +10,145 @@ open Util open Names +open Constr open Termops open EConstr open Inductiveops open Hipattern open Tacmach.New open Tacticals.New +open Clenv open Tactics open Proofview.Notations +type branch_args = { + ity : pinductive; (* the type we were eliminating on *) + branchnum : int; (* the branch number *) + nassums : int; (* number of assumptions/letin to be introduced *) + branchsign : bool list; (* the signature of the branch. + true=assumption, false=let-in *) + branchnames : Tactypes.intro_patterns} + module NamedDecl = Context.Named.Declaration +(* Find the right elimination suffix corresponding to the sort of the goal *) +(* c should be of type A1->.. An->B with B an inductive definition *) +let general_elim_then_using mk_elim + rec_flag allnames tac predicate ind (c, t) = + let open Pp in + Proofview.Goal.enter begin fun gl -> + let sigma, elim = mk_elim ind gl in + let ind = on_snd (fun u -> EInstance.kind sigma u) ind in + Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma) + (Proofview.Goal.enter begin fun gl -> + let indclause = mk_clenv_from gl (c, t) in + (* applying elimination_scheme just a little modified *) + let elimclause = mk_clenv_from gl (elim,Tacmach.New.pf_get_type_of gl elim) in + let indmv = + match EConstr.kind elimclause.evd (last_arg elimclause.evd elimclause.templval.Evd.rebus) with + | Meta mv -> mv + | _ -> CErrors.anomaly (str"elimination.") + in + let pmv = + let p, _ = decompose_app elimclause.evd elimclause.templtyp.Evd.rebus in + match EConstr.kind elimclause.evd p with + | Meta p -> p + | _ -> + let name_elim = + match EConstr.kind sigma elim with + | Const _ | Var _ -> str " " ++ Printer.pr_econstr_env (pf_env gl) sigma elim + | _ -> mt () + in + CErrors.user_err ~hdr:"Tacticals.general_elim_then_using" + (str "The elimination combinator " ++ name_elim ++ str " is unknown.") + in + let elimclause' = clenv_fchain ~with_univs:false indmv elimclause indclause in + let branchsigns = Tacticals.compute_constructor_signatures ~rec_flag ind in + let brnames = Tacticals.compute_induction_names false branchsigns allnames in + let flags = Unification.elim_flags () in + let elimclause' = + match predicate with + | None -> elimclause' + | Some p -> clenv_unify ~flags Reduction.CONV (mkMeta pmv) p elimclause' + in + let after_tac i = + let ba = { branchsign = branchsigns.(i); + branchnames = brnames.(i); + nassums = List.length branchsigns.(i); + branchnum = i+1; + ity = ind; } + in + tac ba + in + let branchtacs = List.init (Array.length branchsigns) after_tac in + Proofview.tclTHEN + (Clenv.res_pf ~flags elimclause') + (Proofview.tclEXTEND [] tclIDTAC branchtacs) + end) end + +(* computing the case/elim combinators *) + +let gl_make_elim ind = begin fun gl -> + let env = Proofview.Goal.env gl in + let gr = Indrec.lookup_eliminator env (fst ind) (elimination_sort_of_goal gl) in + let (sigma, c) = pf_apply Evd.fresh_global gl gr in + (sigma, c) +end + +let gl_make_case dep (ind, u) = begin fun gl -> + let sigma = project gl in + let u = EInstance.kind (project gl) u in + let (sigma, r) = Indrec.build_case_analysis_scheme (pf_env gl) sigma (ind, u) dep + (elimination_sort_of_goal gl) + in + (sigma, EConstr.of_constr r) +end + +let make_elim_branch_assumptions ba hyps = + let assums = + try List.rev (List.firstn ba.nassums hyps) + with Failure _ -> CErrors.anomaly (Pp.str "make_elim_branch_assumptions.") in + assums + +let elim_on_ba tac ba = + Proofview.Goal.enter begin fun gl -> + let branches = make_elim_branch_assumptions ba (Proofview.Goal.hyps gl) in + tac branches + end + +let elimination_then tac c = + let open Declarations in + Proofview.Goal.enter begin fun gl -> + let (ind,t) = pf_reduce_to_quantified_ind gl (pf_get_type_of gl c) in + let isrec,mkelim = + match (Global.lookup_mind (fst (fst ind))).mind_record with + | NotRecord -> true,gl_make_elim + | FakeRecord | PrimRecord _ -> false,gl_make_case true + in + general_elim_then_using mkelim isrec None tac None ind (c, t) + end + (* Supposed to be called without as clause *) let introElimAssumsThen tac ba = - assert (ba.Tacticals.branchnames == []); - let introElimAssums = tclDO ba.Tacticals.nassums intro in + assert (ba.branchnames == []); + let introElimAssums = tclDO ba.nassums intro in (tclTHEN introElimAssums (elim_on_ba tac ba)) (* Supposed to be called with a non-recursive scheme *) let introCaseAssumsThen with_evars tac ba = - let n1 = List.length ba.Tacticals.branchsign in - let n2 = List.length ba.Tacticals.branchnames in + let n1 = List.length ba.branchsign in + let n2 = List.length ba.branchnames in let (l1,l2),l3 = - if n1 < n2 then List.chop n1 ba.Tacticals.branchnames, [] - else (ba.Tacticals.branchnames, []), List.make (n1-n2) false in + if n1 < n2 then List.chop n1 ba.branchnames, [] + else (ba.branchnames, []), List.make (n1-n2) false in let introCaseAssums = tclTHEN (intro_patterns with_evars l1) (intros_clearing l3) in - (tclTHEN introCaseAssums (case_on_ba (tac l2) ba)) + (tclTHEN introCaseAssums (elim_on_ba (tac l2) ba)) + +let case_tac dep names tac elim ind c = + let mkcase = gl_make_case dep in + let tac = introCaseAssumsThen false (* ApplyOn not supported by inversion *) tac in + general_elim_then_using mkcase false names tac (Some elim) ind c (* The following tactic Decompose repeatedly applies the elimination(s) rule(s) of the types satisfying the predicate @@ -68,7 +180,7 @@ and general_decompose_aux recognizer id = (fun bas -> tclTHEN (clear [id]) (tclMAP (general_decompose_on_hyp recognizer) - (ids_of_named_context bas.Tacticals.assums)))) + (ids_of_named_context bas)))) id (* We should add a COMPLETE to be sure that the created hypothesis @@ -136,7 +248,7 @@ let induction_trailer abs_i abs_j bargs = let idty = pf_get_type_of gl (mkVar id) in let fvty = global_vars (pf_env gl) (project gl) idty in let possible_bring_hyps = - (List.tl (nLastDecls gl (abs_j - abs_i))) @ bargs.Tacticals.assums + (List.tl (nLastDecls gl (abs_j - abs_i))) @ bargs in let (hyps,_) = List.fold_left diff --git a/tactics/elim.mli b/tactics/elim.mli index e89855a050..4c5cdc8a31 100644 --- a/tactics/elim.mli +++ b/tactics/elim.mli @@ -10,14 +10,13 @@ open Names open EConstr -open Tacticals open Tactypes (** Eliminations tactics. *) -val introCaseAssumsThen : Tactics.evars_flag -> - (intro_patterns -> branch_assumptions -> unit Proofview.tactic) -> - branch_args -> unit Proofview.tactic +val case_tac : bool -> or_and_intro_pattern option -> + (intro_patterns -> named_context -> unit Proofview.tactic) -> + constr -> inductive * EInstance.t -> constr * types -> unit Proofview.tactic val h_decompose : inductive list -> constr -> unit Proofview.tactic val h_decompose_or : constr -> unit Proofview.tactic diff --git a/tactics/equality.ml b/tactics/equality.ml index b4def7bb51..535725b11d 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -105,7 +105,7 @@ let rewrite_core_unif_flags = { check_applied_meta_types = true; use_pattern_unification = true; use_meta_bound_pattern_unification = true; - allowed_evars = AllowAll; + allowed_evars = Evarsolve.AllowedEvars.all; restrict_conv_on_strict_subterms = false; modulo_betaiota = false; modulo_eta = true; @@ -130,7 +130,7 @@ let freeze_initial_evars sigma flags clause = if Evar.Map.mem evk initial then false else Evar.Set.mem evk (Lazy.force newevars) in - let allowed_evars = AllowFun allowed in + let allowed_evars = Evarsolve.AllowedEvars.from_pred allowed in {flags with core_unify_flags = {flags.core_unify_flags with allowed_evars}; merge_unify_flags = {flags.merge_unify_flags with allowed_evars}; @@ -187,7 +187,7 @@ let rewrite_conv_closed_core_unif_flags = { use_meta_bound_pattern_unification = true; - allowed_evars = AllowAll; + allowed_evars = Evarsolve.AllowedEvars.all; restrict_conv_on_strict_subterms = false; modulo_betaiota = false; @@ -221,7 +221,7 @@ let rewrite_keyed_core_unif_flags = { use_meta_bound_pattern_unification = true; - allowed_evars = AllowAll; + allowed_evars = Evarsolve.AllowedEvars.all; restrict_conv_on_strict_subterms = false; modulo_betaiota = true; @@ -1013,6 +1013,12 @@ let discrimination_pf e (t,t1,t2) discriminator lbeq to_kind = Proofview.tclUNIT (applist (eq_elim, [t;t1;mkNamedLambda (make_annot e Sorts.Relevant) t discriminator;i;t2])) +type equality = { + eq_data : (coq_eq_data * (EConstr.t * EConstr.t * EConstr.t)); + (* equality data + A : Type, t1 : A, t2 : A *) + eq_clenv : clausenv; + (* clause [M : R A t1 t2] where [R] is the equality from above *) +} let eq_baseid = Id.of_string "e" @@ -1025,7 +1031,7 @@ let apply_on_clause (f,t) clause = | _ -> user_err (str "Ill-formed clause applicator.")) in clenv_fchain ~with_univs:false argmv f_clause clause -let discr_positions env sigma (lbeq,eqn,(t,t1,t2)) eq_clause cpath dirn = +let discr_positions env sigma { eq_data = (lbeq,(t,t1,t2)); eq_clenv = eq_clause } cpath dirn = build_coq_True () >>= fun true_0 -> build_coq_False () >>= fun false_0 -> let false_ty = Retyping.get_type_of env sigma false_0 in @@ -1043,13 +1049,14 @@ let discr_positions env sigma (lbeq,eqn,(t,t1,t2)) eq_clause cpath dirn = in discriminator >>= fun discriminator -> discrimination_pf e (t,t1,t2) discriminator lbeq false_kind >>= fun pf -> - let pf_ty = mkArrow eqn Sorts.Relevant false_0 in + let pf_ty = mkArrow (clenv_type eq_clause) Sorts.Relevant false_0 in let absurd_clause = apply_on_clause (pf,pf_ty) eq_clause in let pf = Clenv.clenv_value_cast_meta absurd_clause in tclTHENS (assert_after Anonymous false_0) [onLastHypId gen_absurdity; (Logic.refiner ~check:true EConstr.Unsafe.(to_constr pf))] -let discrEq (lbeq,_,(t,t1,t2) as u) eq_clause = +let discrEq eq = + let { eq_data = (_, (_, t1, t2)); eq_clenv = eq_clause } = eq in let sigma = eq_clause.evd in Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in @@ -1058,7 +1065,7 @@ let discrEq (lbeq,_,(t,t1,t2) as u) eq_clause = let info = Exninfo.reify () in tclZEROMSG ~info (str"Not a discriminable equality.") | Inl (cpath, (_,dirn), _) -> - discr_positions env sigma u eq_clause cpath dirn + discr_positions env sigma eq cpath dirn end let onEquality with_evars tac (c,lbindc) = @@ -1071,9 +1078,10 @@ let onEquality with_evars tac (c,lbindc) = let eqn = clenv_type eq_clause' in (* FIXME evar leak *) let (eq,u,eq_args) = pf_apply find_this_eq_data_decompose gl eqn in + let eq = { eq_data = (eq, eq_args); eq_clenv = eq_clause' } in tclTHEN (Proofview.Unsafe.tclEVARS eq_clause'.evd) - (tac (eq,eqn,eq_args) eq_clause') + (tac eq) end let onNegatedEquality with_evars tac = @@ -1385,7 +1393,8 @@ let simplify_args env sigma t = | eq, [t1;c1;t2;c2] -> applist (eq,[t1;simpl env sigma c1;t2;simpl env sigma c2]) | _ -> t -let inject_at_positions env sigma l2r (eq,_,(t,t1,t2)) eq_clause posns tac = +let inject_at_positions env sigma l2r eq posns tac = + let { eq_data = (eq, (t,t1,t2)); eq_clenv = eq_clause } = eq in let e = next_ident_away eq_baseid (vars_of_env env) in let e_env = push_named (LocalAssum (make_annot e Sorts.Relevant,t)) env in let evdref = ref sigma in @@ -1422,7 +1431,8 @@ let () = CErrors.register_handler (function | NothingToInject -> Some (Pp.str "Nothing to inject.") | _ -> None) -let injEqThen keep_proofs tac l2r (eq,_,(t,t1,t2) as u) eq_clause = +let injEqThen keep_proofs tac l2r eql = + let { eq_data = (eq, (t,t1,t2)); eq_clenv = eq_clause } = eql in let sigma = eq_clause.evd in let env = eq_clause.env in match find_positions env sigma ~keep_proofs ~no_discr:true t1 t2 with @@ -1437,7 +1447,7 @@ let injEqThen keep_proofs tac l2r (eq,_,(t,t1,t2) as u) eq_clause = | Inr [([],_,_)] -> Proofview.tclZERO NothingToInject | Inr posns -> - inject_at_positions env sigma l2r u eq_clause posns + inject_at_positions env sigma l2r eql posns (tac (clenv_value eq_clause)) let get_previous_hyp_position id gl = @@ -1491,17 +1501,18 @@ let simpleInjClause flags with_evars = function let injConcl flags = injClause flags None false None let injHyp flags clear_flag id = injClause flags None false (Some (clear_flag,ElimOnIdent CAst.(make id))) -let decompEqThen keep_proofs ntac (lbeq,_,(t,t1,t2) as u) clause = +let decompEqThen keep_proofs ntac eq = + let { eq_data = (_, (_,t1,t2) as u); eq_clenv = clause } = eq in Proofview.Goal.enter begin fun gl -> let sigma = clause.evd in let env = Proofview.Goal.env gl in match find_positions env sigma ~keep_proofs ~no_discr:false t1 t2 with | Inl (cpath, (_,dirn), _) -> - discr_positions env sigma u clause cpath dirn + discr_positions env sigma eq cpath dirn | Inr [] -> (* Change: do not fail, simplify clear this trivial hyp *) ntac (clenv_value clause) 0 | Inr posns -> - inject_at_positions env sigma true u clause posns + inject_at_positions env sigma true eq posns (ntac (clenv_value clause)) end @@ -1513,10 +1524,11 @@ let dEq ~keep_proofs with_evars = dEqThen ~keep_proofs with_evars (fun clear_flag c x -> (apply_clear_request clear_flag (use_clear_hyp_by_default ()) c)) -let intro_decomp_eq tac data (c, t) = +let intro_decomp_eq tac (eq, _, data) (c, t) = Proofview.Goal.enter begin fun gl -> let cl = pf_apply make_clenv_binding gl (c, t) NoBindings in - decompEqThen !keep_proof_equalities_for_injection (fun _ -> tac) data cl + let eq = { eq_data = (eq, data); eq_clenv = cl } in + decompEqThen !keep_proof_equalities_for_injection (fun _ -> tac) eq end let () = declare_intro_decomp_eq intro_decomp_eq diff --git a/tactics/hints.ml b/tactics/hints.ml index db4b23705f..355cea8fa8 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -837,7 +837,7 @@ let make_exact_entry env sigma info ~poly ?(name=PathAny) (c, cty, ctx) = db = None; secvars; code = with_uid (Give_exact (c, cty, ctx, poly)); }) -let make_apply_entry env sigma (eapply,hnf,verbose) info ~poly ?(name=PathAny) (c, cty, ctx) = +let make_apply_entry env sigma hnf info ~poly ?(name=PathAny) (c, cty, ctx) = let cty = if hnf then hnf_constr env sigma cty else cty in match EConstr.kind sigma cty with | Prod _ -> @@ -862,25 +862,11 @@ let make_apply_entry env sigma (eapply,hnf,verbose) info ~poly ?(name=PathAny) ( db = None; secvars; code = with_uid (Res_pf(c,cty,ctx,poly)); }) - else begin - if not eapply then failwith "make_apply_entry"; - if verbose then begin - let variables = str (CString.plural nmiss "variable") in - Feedback.msg_info ( - strbrk "The hint " ++ - pr_leconstr_env env sigma' c ++ - strbrk " will only be used by eauto, because applying " ++ - pr_leconstr_env env sigma' c ++ - strbrk " would leave " ++ variables ++ Pp.spc () ++ - Pp.prlist_with_sep Pp.pr_comma Name.print (List.map (Evd.meta_name ce.evd) miss) ++ - strbrk " as unresolved existential " ++ variables ++ str "." - ) - end; + else (Some hd, { pri; pat = Some pat; name; db = None; secvars; code = with_uid (ERes_pf(c,cty,ctx,poly)); }) - end | _ -> failwith "make_apply_entry" (* flags is (e,h,v) with e=true if eapply and h=true if hnf and v=true if verbose @@ -916,19 +902,25 @@ let fresh_global_or_constr env sigma poly cr = (c, Univ.ContextSet.empty) end -let make_resolves env sigma flags info ~check ~poly ?name cr = +let make_resolves env sigma (eapply, hnf) info ~check ~poly ?name cr = let c, ctx = fresh_global_or_constr env sigma poly cr in let cty = Retyping.get_type_of env sigma c in let try_apply f = - try Some (f (c, cty, ctx)) with Failure _ -> None in + try + let (_, hint) as ans = f (c, cty, ctx) in + match hint.code.obj with + | ERes_pf _ -> if not eapply then None else Some ans + | _ -> Some ans + with Failure _ -> None + in let ents = List.map_filter try_apply [make_exact_entry env sigma info ~poly ?name; - make_apply_entry env sigma flags info ~poly ?name] + make_apply_entry env sigma hnf info ~poly ?name] in if check && List.is_empty ents then user_err ~hdr:"Hint" (pr_leconstr_env env sigma c ++ spc() ++ - (if pi1 flags then str"cannot be used as a hint." + (if eapply then str"cannot be used as a hint." else str "can be used as a hint only for eauto.")); ents @@ -937,7 +929,7 @@ let make_resolve_hyp env sigma decl = let hname = NamedDecl.get_id decl in let c = mkVar hname in try - [make_apply_entry env sigma (true, true, false) empty_hint_info ~poly:false + [make_apply_entry env sigma true empty_hint_info ~poly:false ~name:(PathHints [GlobRef.VarRef hname]) (c, NamedDecl.get_type decl, Univ.ContextSet.empty)] with @@ -1223,9 +1215,28 @@ let add_resolves env sigma clist ~local ~superglobal dbnames = (fun dbname -> let r = List.flatten (List.map (fun (pri, poly, hnf, path, gr) -> - make_resolves env sigma (true,hnf,not !Flags.quiet) + make_resolves env sigma (true, hnf) pri ~check:true ~poly ~name:path gr) clist) in + let check (_, hint) = match hint.code.obj with + | ERes_pf (c, cty, ctx, _) -> + let sigma' = Evd.merge_context_set univ_flexible sigma ctx in + let ce = mk_clenv_from_env env sigma' None (c,cty) in + let miss = clenv_missing ce in + let nmiss = List.length miss in + let variables = str (CString.plural nmiss "variable") in + Feedback.msg_info ( + strbrk "The hint " ++ + pr_leconstr_env env sigma' c ++ + strbrk " will only be used by eauto, because applying " ++ + pr_leconstr_env env sigma' c ++ + strbrk " would leave " ++ variables ++ Pp.spc () ++ + Pp.prlist_with_sep Pp.pr_comma Name.print (List.map (Evd.meta_name ce.evd) miss) ++ + strbrk " as unresolved existential " ++ variables ++ str "." + ) + | _ -> () + in + let () = if not !Flags.quiet then List.iter check r in let hint = make_hint ~local dbname (AddHints { superglobal; hints = r }) in Lib.add_anonymous_leaf (inAutoHint hint)) dbnames @@ -1375,10 +1386,10 @@ let expand_constructor_hints env sigma lems = let constructor_hints env sigma eapply lems = let lems = expand_constructor_hints env sigma lems in List.map_append (fun (poly, lem) -> - make_resolves env sigma (eapply,true,false) empty_hint_info ~check:true ~poly lem) lems + make_resolves env sigma (eapply, true) empty_hint_info ~check:true ~poly lem) lems let make_resolves env sigma info ~check ~poly ?name hint = - make_resolves env sigma (true, false, false) info ~check ~poly ?name hint + make_resolves env sigma (true, false) info ~check ~poly ?name hint let make_local_hint_db env sigma ts eapply lems = let map c = c env sigma in diff --git a/tactics/inv.ml b/tactics/inv.ml index 4b94dd0e72..f77b52b931 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -409,7 +409,7 @@ let nLastDecls i tac = let rewrite_equations as_mode othin neqns names ba = Proofview.Goal.enter begin fun gl -> - let (depids,nodepids) = split_dep_and_nodep ba.Tacticals.assums gl in + let (depids,nodepids) = split_dep_and_nodep ba gl in let first_eq = ref Logic.MoveLast in let avoid = if as_mode then Id.Set.of_list (List.map NamedDecl.get_id nodepids) else Id.Set.empty in match othin with @@ -474,13 +474,12 @@ let raw_inversion inv_kind id status names = let (elim_predicate, args) = make_inv_predicate env evdref indf realargs id status concl in let sigma = !evdref in - let (cut_concl,case_tac) = - if status != NoDep && (local_occur_var sigma id concl) then - Reductionops.beta_applist sigma (elim_predicate, realargs@[c]), - case_then_using + let dep = status != NoDep && (local_occur_var sigma id concl) in + let cut_concl = + if dep then + Reductionops.beta_applist sigma (elim_predicate, realargs@[c]) else - Reductionops.beta_applist sigma (elim_predicate, realargs), - case_nodep_then_using + Reductionops.beta_applist sigma (elim_predicate, realargs) in let refined id = let prf = mkApp (mkVar id, args) in @@ -491,10 +490,7 @@ let raw_inversion inv_kind id status names = tclTHEN (Proofview.Unsafe.tclEVARS sigma) (tclTHENS (assert_before Anonymous cut_concl) - [case_tac names - (introCaseAssumsThen false (* ApplyOn not supported by inversion *) - (rewrite_equations_tac as_mode inv_kind id neqns)) - (Some elim_predicate) ind (c,t); + [case_tac dep names (rewrite_equations_tac as_mode inv_kind id neqns) elim_predicate ind (c,t); onLastHypId (fun id -> tclTHEN (refined id) reflexivity)]) end diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index ec770e2473..fc099f643d 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -14,10 +14,8 @@ open Util open Names open Constr open EConstr -open Termops open Declarations open Tacmach -open Clenv open Tactypes module RelDecl = Context.Rel.Declaration @@ -335,18 +333,6 @@ let ifOnHyp pred tac1 tac2 id gl = used to keep track of some information about the ``branches'' of the elimination. *) -type branch_args = { - ity : pinductive; (* the type we were eliminating on *) - branchnum : int; (* the branch number *) - nassums : int; (* number of assumptions/letin to be introduced *) - branchsign : bool list; (* the signature of the branch. - true=assumption, false=let-in *) - branchnames : intro_patterns} - -type branch_assumptions = { - ba : branch_args; (* the branch args *) - assums : named_context} (* the list of assumptions introduced *) - let fix_empty_or_and_pattern nv l = (* 1- The syntax does not distinguish between "[ ]" for one clause with no names and "[ ]" for no clause at all *) @@ -401,15 +387,13 @@ let get_and_check_or_and_pattern_gen ?loc check_and names branchsigns = let get_and_check_or_and_pattern ?loc = get_and_check_or_and_pattern_gen ?loc true -let compute_induction_names_gen check_and branchletsigns = function +let compute_induction_names check_and branchletsigns = function | None -> Array.make (Array.length branchletsigns) [] | Some {CAst.loc;v=names} -> let names = fix_empty_or_and_pattern (Array.length branchletsigns) names in get_and_check_or_and_pattern_gen check_and ?loc names branchletsigns -let compute_induction_names = compute_induction_names_gen true - (* Compute the let-in signature of case analysis or standard induction scheme *) let compute_constructor_signatures ~rec_flag ((_,k as ity),u) = let rec analrec c recargs = @@ -844,60 +828,6 @@ module New = struct tclMAP tac (Locusops.simple_clause_of (fun () -> hyps) cl) end - (* Find the right elimination suffix corresponding to the sort of the goal *) - (* c should be of type A1->.. An->B with B an inductive definition *) - let general_elim_then_using mk_elim - rec_flag allnames tac predicate ind (c, t) = - Proofview.Goal.enter begin fun gl -> - let sigma, elim = mk_elim ind gl in - let ind = on_snd (fun u -> EInstance.kind sigma u) ind in - Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma) - (Proofview.Goal.enter begin fun gl -> - let indclause = mk_clenv_from gl (c, t) in - (* applying elimination_scheme just a little modified *) - let elimclause = mk_clenv_from gl (elim,Tacmach.New.pf_get_type_of gl elim) in - let indmv = - match EConstr.kind elimclause.evd (last_arg elimclause.evd elimclause.templval.Evd.rebus) with - | Meta mv -> mv - | _ -> anomaly (str"elimination.") - in - let pmv = - let p, _ = decompose_app elimclause.evd elimclause.templtyp.Evd.rebus in - match EConstr.kind elimclause.evd p with - | Meta p -> p - | _ -> - let name_elim = - match EConstr.kind sigma elim with - | Const _ | Var _ -> str " " ++ Printer.pr_econstr_env (pf_env gl) sigma elim - | _ -> mt () - in - user_err ~hdr:"Tacticals.general_elim_then_using" - (str "The elimination combinator " ++ name_elim ++ str " is unknown.") - in - let elimclause' = clenv_fchain ~with_univs:false indmv elimclause indclause in - let branchsigns = compute_constructor_signatures ~rec_flag ind in - let brnames = compute_induction_names_gen false branchsigns allnames in - let flags = Unification.elim_flags () in - let elimclause' = - match predicate with - | None -> elimclause' - | Some p -> clenv_unify ~flags Reduction.CONV (mkMeta pmv) p elimclause' - in - let after_tac i = - let ba = { branchsign = branchsigns.(i); - branchnames = brnames.(i); - nassums = List.length branchsigns.(i); - branchnum = i+1; - ity = ind; } - in - tac ba - in - let branchtacs = List.init (Array.length branchsigns) after_tac in - Proofview.tclTHEN - (Clenv.res_pf ~flags elimclause') - (Proofview.tclEXTEND [] tclIDTAC branchtacs) - end) end - let elimination_sort_of_goal gl = (* Retyping will expand evars anyway. *) let c = Proofview.Goal.concl gl in @@ -912,68 +842,6 @@ module New = struct | None -> elimination_sort_of_goal gl | Some id -> elimination_sort_of_hyp id gl - (* computing the case/elim combinators *) - - let gl_make_elim ind = begin fun gl -> - let env = Proofview.Goal.env gl in - let gr = Indrec.lookup_eliminator env (fst ind) (elimination_sort_of_goal gl) in - let (sigma, c) = pf_apply Evd.fresh_global gl gr in - (sigma, c) - end - - let gl_make_case_dep (ind, u) = begin fun gl -> - let sigma = project gl in - let u = EInstance.kind (project gl) u in - let (sigma, r) = Indrec.build_case_analysis_scheme (pf_env gl) sigma (ind, u) true - (elimination_sort_of_goal gl) - in - (sigma, EConstr.of_constr r) - end - - let gl_make_case_nodep (ind, u) = begin fun gl -> - let sigma = project gl in - let u = EInstance.kind sigma u in - let (sigma, r) = Indrec.build_case_analysis_scheme (pf_env gl) sigma (ind, u) false - (elimination_sort_of_goal gl) - in - (sigma, EConstr.of_constr r) - end - - let make_elim_branch_assumptions ba hyps = - let assums = - try List.rev (List.firstn ba.nassums hyps) - with Failure _ -> anomaly (Pp.str "make_elim_branch_assumptions.") in - { ba = ba; assums = assums } - - let elim_on_ba tac ba = - Proofview.Goal.enter begin fun gl -> - let branches = make_elim_branch_assumptions ba (Proofview.Goal.hyps gl) in - tac branches - end - - let case_on_ba tac ba = - Proofview.Goal.enter begin fun gl -> - let branches = make_elim_branch_assumptions ba (Proofview.Goal.hyps gl) in - tac branches - end - - let elimination_then tac c = - Proofview.Goal.enter begin fun gl -> - let (ind,t) = pf_reduce_to_quantified_ind gl (pf_get_type_of gl c) in - let isrec,mkelim = - match (Global.lookup_mind (fst (fst ind))).mind_record with - | NotRecord -> true,gl_make_elim - | FakeRecord | PrimRecord _ -> false,gl_make_case_dep - in - general_elim_then_using mkelim isrec None tac None ind (c, t) - end - - let case_then_using = - general_elim_then_using gl_make_case_dep false - - let case_nodep_then_using = - general_elim_then_using gl_make_case_nodep false - let pf_constr_of_global ref = Proofview.tclEVARMAP >>= fun sigma -> Proofview.tclENV >>= fun env -> diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli index 48a06e6e1d..bfead34b3b 100644 --- a/tactics/tacticals.mli +++ b/tactics/tacticals.mli @@ -9,7 +9,6 @@ (************************************************************************) open Names -open Constr open EConstr open Evd open Locus @@ -94,18 +93,6 @@ val onClauseLR : (Id.t option -> tactic) -> clause -> tactic (** {6 Elimination tacticals. } *) -type branch_args = private { - ity : pinductive; (** the type we were eliminating on *) - branchnum : int; (** the branch number *) - nassums : int; (** number of assumptions/letin to be introduced *) - branchsign : bool list; (** the signature of the branch. - true=assumption, false=let-in *) - branchnames : intro_patterns} - -type branch_assumptions = private { - ba : branch_args; (** the branch args *) - assums : named_context} (** the list of assumptions introduced *) - (** [get_and_check_or_and_pattern loc pats branchsign] returns an appropriate error message if |pats| <> |branchsign|; extends them if no pattern is given for let-ins in the case of a conjunctive pattern *) @@ -122,7 +109,7 @@ val compute_constructor_signatures : rec_flag:bool -> inductive * 'a -> bool lis (** Useful for [as intro_pattern] modifier *) val compute_induction_names : - bool list array -> or_and_intro_pattern option -> intro_patterns array + bool -> bool list array -> or_and_intro_pattern option -> intro_patterns array val elimination_sort_of_goal : Goal.goal sigma -> Sorts.family val elimination_sort_of_hyp : Id.t -> Goal.goal sigma -> Sorts.family @@ -249,20 +236,5 @@ module New : sig val elimination_sort_of_hyp : Id.t -> Proofview.Goal.t -> Sorts.family val elimination_sort_of_clause : Id.t option -> Proofview.Goal.t -> Sorts.family - val elimination_then : - (branch_args -> unit Proofview.tactic) -> - constr -> unit Proofview.tactic - - val case_then_using : - or_and_intro_pattern option -> (branch_args -> unit Proofview.tactic) -> - constr option -> inductive * EInstance.t -> constr * types -> unit Proofview.tactic - - val case_nodep_then_using : - or_and_intro_pattern option -> (branch_args -> unit Proofview.tactic) -> - constr option -> inductive * EInstance.t -> constr * types -> unit Proofview.tactic - - val elim_on_ba : (branch_assumptions -> unit Proofview.tactic) -> branch_args -> unit Proofview.tactic - val case_on_ba : (branch_assumptions -> unit Proofview.tactic) -> branch_args -> unit Proofview.tactic - val pf_constr_of_global : GlobRef.t -> constr Proofview.tactic end diff --git a/tactics/tactics.ml b/tactics/tactics.ml index eb7b7e363f..5f7e35d205 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -2330,7 +2330,7 @@ let intro_decomp_eq ?loc l thin tac id = let env = Proofview.Goal.env gl in let sigma = Proofview.Goal.sigma gl in let sigma, t = Typing.type_of env sigma c in - let _,t = reduce_to_quantified_ind env sigma t in + let _,t = reduce_to_atomic_ind env sigma t in match my_find_eq_data_decompose env sigma t with | Some (eq,u,eq_args) -> !intro_decomp_eq_function @@ -4397,7 +4397,7 @@ let apply_induction_in_context with_evars hyp0 inhyps elim indvars names induct_ let branchletsigns = let f (_,is_not_let,_,_) = is_not_let in Array.map (fun (_,l) -> List.map f l) indsign in - let names = compute_induction_names branchletsigns names in + let names = compute_induction_names true branchletsigns names in Array.iter (check_name_unicity env toclear []) names; let tac = (if isrec then Tacticals.New.tclTHENFIRSTn else Tacticals.New.tclTHENLASTn) diff --git a/test-suite/bugs/closed/bug_12909.v b/test-suite/bugs/closed/bug_12909.v new file mode 100644 index 0000000000..fafb6a418f --- /dev/null +++ b/test-suite/bugs/closed/bug_12909.v @@ -0,0 +1,8 @@ +Module Type T. +Axiom A : Type. +End T. + +Module M. + Axiom A : SProp. +End M. +Fail Module N <: T := M. diff --git a/test-suite/output/bug_12887.out b/test-suite/output/bug_12887.out new file mode 100644 index 0000000000..5ea7722bc6 --- /dev/null +++ b/test-suite/output/bug_12887.out @@ -0,0 +1,10 @@ +The command has indeed failed with message: +Cannot infer this placeholder of type "Type" in +environment: +Functor : (Type -> Type) -> Type +F : Type -> Type +fmap : forall A B : Type, (A -> B) -> F A -> F B +The command has indeed failed with message: +Cannot infer an existential variable of type "nat" in +environment: +R : nat -> Type diff --git a/test-suite/output/bug_12887.v b/test-suite/output/bug_12887.v new file mode 100644 index 0000000000..4208c3e8e9 --- /dev/null +++ b/test-suite/output/bug_12887.v @@ -0,0 +1,10 @@ +Arguments id {_} _. + +Fail Record Functor (F : Type -> Type) := { + fmap : forall A B, (A -> B) -> F A -> F B; + fmap_identity : fmap _ _ id = id; +}. + +Fail Inductive R (x:nat) := { y : R ltac:(clear x) }. + +Inductive R (x:nat) := { y : bool; z : R _ }. diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml index 673124296d..452de69b1d 100644 --- a/vernac/comInductive.ml +++ b/vernac/comInductive.ml @@ -451,7 +451,7 @@ let interp_params env udecl uparamsl paramsl = do the unification. [env_ar_par] is [uparams; inds; params] *) -let maybe_unify_params_in env_ar_par sigma ~ninds ~nparams c = +let maybe_unify_params_in env_ar_par sigma ~ninds ~nparams ~binders:k c = let is_ind sigma k c = match EConstr.kind sigma c with | Constr.Rel n -> (* env is [uparams; inds; params; k other things] *) @@ -462,14 +462,18 @@ let maybe_unify_params_in env_ar_par sigma ~ninds ~nparams c = | Constr.App (h,args) when is_ind sigma k h -> Array.fold_left_i (fun i sigma arg -> if i >= nparams || not (EConstr.isEvar sigma arg) then sigma - else Evarconv.unify_delay env sigma arg (EConstr.mkRel (k+nparams-i))) + else begin try Evarconv.unify_delay env sigma arg (EConstr.mkRel (k+nparams-i)) + with Evarconv.UnableToUnify _ -> + (* ignore errors, we will get a "Cannot infer ..." error instead *) + sigma + end) sigma args | _ -> Termops.fold_constr_with_full_binders sigma (fun d (env,k) -> EConstr.push_rel d env, k+1) aux envk sigma c in - aux (env_ar_par,0) sigma c + aux (env_ar_par,k) sigma c let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) notations ~cumulative ~poly ~private_ind finite = check_all_names_different indl; @@ -527,7 +531,7 @@ let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) not let sigma = List.fold_left (fun sigma (_,ctyps,_) -> List.fold_left (fun sigma ctyp -> - maybe_unify_params_in env_ar_params sigma ~ninds ~nparams ctyp) + maybe_unify_params_in env_ar_params sigma ~ninds ~nparams ~binders:0 ctyp) sigma ctyps) sigma constructors in diff --git a/vernac/comInductive.mli b/vernac/comInductive.mli index 9c876787a3..91e8f609d5 100644 --- a/vernac/comInductive.mli +++ b/vernac/comInductive.mli @@ -81,8 +81,8 @@ val template_polymorphism_candidate monomorphic universe context that can be made parametric in its conclusion sort, if one is given. *) -val maybe_unify_params_in : Environ.env -> Evd.evar_map -> ninds:int -> nparams:int +val maybe_unify_params_in : Environ.env -> Evd.evar_map -> ninds:int -> nparams:int -> binders:int -> EConstr.t -> Evd.evar_map (** [nparams] is the number of parameters which aren't treated as uniform, ie the length of params (including letins) where the env - is [uniform params, inductives, params]. *) + is [uniform params, inductives, params, binders]. *) diff --git a/vernac/record.ml b/vernac/record.ml index d0036e40f9..bd5b71cd6b 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -81,12 +81,12 @@ let interp_fields_evars env sigma ~ninds ~nparams impls_env nots l = (EConstr.push_rel d env, sigma, impl :: uimpls, d::params, impls)) (env, sigma, [], [], impls_env) nots l in - let _, sigma = Context.Rel.fold_outside ~init:(env,sigma) (fun f (env,sigma) -> + let _, _, sigma = Context.Rel.fold_outside ~init:(env,0,sigma) (fun f (env,k,sigma) -> let sigma = RelDecl.fold_constr (fun c sigma -> - ComInductive.maybe_unify_params_in env sigma ~ninds ~nparams c) + ComInductive.maybe_unify_params_in env sigma ~ninds ~nparams ~binders:k c) f sigma in - EConstr.push_rel f env, sigma) + EConstr.push_rel f env, k+1, sigma) newfs in sigma, (impls, newfs) |