diff options
29 files changed, 412 insertions, 137 deletions
diff --git a/doc/changelog/04-tactics/12146-master+fix10812-subst-failure-section-variables.rst b/doc/changelog/04-tactics/12146-master+fix10812-subst-failure-section-variables.rst new file mode 100644 index 0000000000..055006d3b4 --- /dev/null +++ b/doc/changelog/04-tactics/12146-master+fix10812-subst-failure-section-variables.rst @@ -0,0 +1,9 @@ +- **Changed:** + Tactic :tacn:`subst` :n:`@ident` now fails over a section variable which is + indirectly dependent in the goal; the incompatibility can generally + be fixed by first clearing the hypotheses causing an indirect + dependency, as reported by the error message, or by using :tacn:`rewrite` :n:`in *` + instead; similarly, :tacn:`subst` has no more effect on such variables + (`#12146 <https://github.com/coq/coq/pull/12146>`_, + by Hugo Herbelin; fixes `#10812 <https://github.com/coq/coq/pull/10812>`_; + fixes `#12139 <https://github.com/coq/coq/pull/12139>`_). diff --git a/doc/changelog/04-tactics/12223-master+fix12152-locating-error-atomic-level.rst b/doc/changelog/04-tactics/12223-master+fix12152-locating-error-atomic-level.rst new file mode 100644 index 0000000000..dc438f151e --- /dev/null +++ b/doc/changelog/04-tactics/12223-master+fix12152-locating-error-atomic-level.rst @@ -0,0 +1,6 @@ +- **Fixed:** + Loss of location of some tactic errors + (`#12223 <https://github.com/coq/coq/pull/12223>`_, + by Hugo Herbelin; fixes + `#12152 <https://github.com/coq/coq/pull/12152>`_ and + `#12255 <https://github.com/coq/coq/pull/12255>`_). diff --git a/doc/changelog/05-tactic-language/11503-ltac2-rebind-with-value.rst b/doc/changelog/05-tactic-language/11503-ltac2-rebind-with-value.rst new file mode 100644 index 0000000000..0dd0fed4e2 --- /dev/null +++ b/doc/changelog/05-tactic-language/11503-ltac2-rebind-with-value.rst @@ -0,0 +1,6 @@ +- **Added:** + The Ltac2 rebinding command :cmd:`Ltac2 Set` has been extended with the ability to + give a name to the old value so as to be able to reuse it inside the + new one + (`#11503 <https://github.com/coq/coq/pull/11503>`_, + by Pierre-Marie Pédrot). diff --git a/doc/changelog/10-standard-library/12008-ollibs-bool.rst b/doc/changelog/10-standard-library/12008-ollibs-bool.rst index 7c10d261a7..42e5eb96eb 100644 --- a/doc/changelog/10-standard-library/12008-ollibs-bool.rst +++ b/doc/changelog/10-standard-library/12008-ollibs-bool.rst @@ -1,5 +1,5 @@ - **Added:** - Order relations ``ltb`` and ``compareb`` added in ``Bool.Bool``. + Order relations ``lt`` and ``compare`` added in ``Bool.Bool``. Order properties for ``bool`` added in ``Bool.BoolOrder`` as well as two modules ``Bool_as_OT`` and ``Bool_as_DT`` in ``Structures.OrdersEx`` (`#12008 <https://github.com/coq/coq/pull/12008>`_, by Olivier Laurent). diff --git a/doc/changelog/10-standard-library/12162-bool-leb.rst b/doc/changelog/10-standard-library/12162-bool-leb.rst new file mode 100644 index 0000000000..6a4070a82e --- /dev/null +++ b/doc/changelog/10-standard-library/12162-bool-leb.rst @@ -0,0 +1,4 @@ +- **Deprecated:** + ``Bool.leb`` in favor of ``Bool.le``. The definition of ``Bool.le`` is made local to avoid conflicts with ``Nat.le``. As a consequence, previous calls to ``leb`` based on importing ``Bool`` should now be qualified into ``Bool.le`` even if ``Bool`` is imported. + (`#12162 <https://github.com/coq/coq/pull/12162>`_, + by Olivier Laurent). diff --git a/doc/sphinx/proof-engine/ltac2.rst b/doc/sphinx/proof-engine/ltac2.rst index 35062e0057..1e35160205 100644 --- a/doc/sphinx/proof-engine/ltac2.rst +++ b/doc/sphinx/proof-engine/ltac2.rst @@ -213,25 +213,63 @@ There is dedicated syntax for list and array literals. Ltac Definitions ~~~~~~~~~~~~~~~~ -.. cmd:: Ltac2 {? mutable} {? rec} @lident := @ltac2_term +.. cmd:: Ltac2 {? mutable} {? rec} @lident := @ltac2_value :name: Ltac2 This command defines a new global Ltac2 value. - For semantic reasons, the body of the Ltac2 definition must be a syntactical - value, that is, a function, a constant or a pure constructor recursively applied to - values. + The body of an Ltac2 definition is required to be a syntactical value + that is, a function, a constant, a pure constructor recursively applied to + values or a (non-recursive) let binding of a value in a value. + + .. productionlist:: coq + ltac2_value: fun `ltac2_var` => `ltac2_term` + : `ltac2_qualid` + : `ltac2_constructor` `ltac2_value` ... `ltac2_value` + : `ltac2_var` + : let `ltac2_var` := `ltac2_value` in `ltac2_value` If ``rec`` is set, the tactic is expanded into a recursive binding. If ``mutable`` is set, the definition can be redefined at a later stage (see below). -.. cmd:: Ltac2 Set @qualid := @ltac2_term +.. cmd:: Ltac2 Set @qualid {? as @lident} := @ltac2_term :name: Ltac2 Set This command redefines a previous ``mutable`` definition. Mutable definitions act like dynamic binding, i.e. at runtime, the last defined value for this entry is chosen. This is useful for global flags and the like. + The previous value of the binding can be optionally accessed using the `as` + binding syntax. + + .. example:: Dynamic nature of mutable cells + + .. coqtop:: all + + Ltac2 mutable x := true. + Ltac2 y := x. + Ltac2 Eval y. + Ltac2 Set x := false. + Ltac2 Eval y. + + .. example:: Interaction with recursive calls + + + .. coqtop:: all + + Ltac2 mutable rec f b := match b with true => 0 | _ => f true end. + Ltac2 Set f := fun b => + match b with true => 1 | _ => f true end. + Ltac2 Eval (f false). + Ltac2 Set f as oldf := fun b => + match b with true => 2 | _ => oldf false end. + Ltac2 Eval (f false). + + In the definition, the `f` in the body is resolved statically + because the definition is marked recursive. In the first re-definition, + the `f` in the body is resolved dynamically. This is witnessed by + the second re-definition. + Reduction ~~~~~~~~~ diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index bc2168411b..439f7fb9f6 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -2832,6 +2832,11 @@ simply :g:`t=u` dropping the implicit type of :g:`t` and :g:`u`. If :n:`@ident` is a local definition of the form :n:`@ident := t`, it is also unfolded and cleared. + If :n:`@ident` is a section variable it is expected to have no + indirect occurrences in the goal, i.e. that no global declarations + implicitly depending on the section variable must be present in the + goal. + .. note:: + When several hypotheses have the form :n:`@ident = t` or :n:`t = @ident`, the first one is used. @@ -2845,9 +2850,11 @@ simply :g:`t=u` dropping the implicit type of :g:`t` and :g:`u`. .. tacv:: subst - This applies subst repeatedly from top to bottom to all identifiers of the + This applies :tacn:`subst` repeatedly from top to bottom to all hypotheses of the context for which an equality of the form :n:`@ident = t` or :n:`t = @ident` - or :n:`@ident := t` exists, with :n:`@ident` not occurring in ``t``. + or :n:`@ident := t` exists, with :n:`@ident` not occurring in + ``t`` and :n:`@ident` not a section variable with indirect + dependencies in the goal. .. flag:: Regular Subst Tactic @@ -2873,6 +2880,15 @@ simply :g:`t=u` dropping the implicit type of :g:`t` and :g:`u`. hypotheses, which without the flag it may break. default. + .. exn:: Cannot find any non-recursive equality over :n:`@ident`. + :undocumented: + + .. exn:: Section variable :n:`@ident` occurs implicitly in global declaration :n:`@qualid` present in hypothesis :n:`@ident`. + Section variable :n:`@ident` occurs implicitly in global declaration :n:`@qualid` present in the conclusion. + + Raised when the variable is a section variable with indirect + dependencies in the goal. + .. tacn:: stepl @term :name: stepl diff --git a/engine/termops.ml b/engine/termops.ml index 6d779e6a35..c51e753d46 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -803,23 +803,29 @@ let occur_evar sigma n c = let occur_in_global env id constr = let vars = vars_of_global env constr in - if Id.Set.mem id vars then raise Occur + Id.Set.mem id vars let occur_var env sigma id c = let rec occur_rec c = match EConstr.destRef sigma c with - | gr, _ -> occur_in_global env id gr + | gr, _ -> if occur_in_global env id gr then raise Occur | exception DestKO -> EConstr.iter sigma occur_rec c in try occur_rec c; false with Occur -> true +exception OccurInGlobal of GlobRef.t + +let occur_var_indirectly env sigma id c = + let var = GlobRef.VarRef id in + let rec occur_rec c = + match EConstr.destRef sigma c with + | gr, _ -> if not (GlobRef.equal gr var) && occur_in_global env id gr then raise (OccurInGlobal gr) + | exception DestKO -> EConstr.iter sigma occur_rec c + in + try occur_rec c; None with OccurInGlobal gr -> Some gr + let occur_var_in_decl env sigma hyp decl = - let open NamedDecl in - match decl with - | LocalAssum (_,typ) -> occur_var env sigma hyp typ - | LocalDef (_, body, typ) -> - occur_var env sigma hyp typ || - occur_var env sigma hyp body + NamedDecl.exists (occur_var env sigma hyp) decl let local_occur_var sigma id c = let rec occur c = match EConstr.kind sigma c with @@ -828,6 +834,9 @@ let local_occur_var sigma id c = in try occur c; false with Occur -> true +let local_occur_var_in_decl sigma hyp decl = + NamedDecl.exists (local_occur_var sigma hyp) decl + (* returns the list of free debruijn indices in a term *) let free_rels sigma m = diff --git a/engine/termops.mli b/engine/termops.mli index 4e77aa9b3b..709fa361a9 100644 --- a/engine/termops.mli +++ b/engine/termops.mli @@ -92,12 +92,14 @@ val occur_meta_or_existential : Evd.evar_map -> constr -> bool val occur_metavariable : Evd.evar_map -> metavariable -> constr -> bool val occur_evar : Evd.evar_map -> Evar.t -> constr -> bool val occur_var : env -> Evd.evar_map -> Id.t -> constr -> bool +val occur_var_indirectly : env -> Evd.evar_map -> Id.t -> constr -> GlobRef.t option val occur_var_in_decl : env -> Evd.evar_map -> Id.t -> named_declaration -> bool (** As {!occur_var} but assume the identifier not to be a section variable *) val local_occur_var : Evd.evar_map -> Id.t -> constr -> bool +val local_occur_var_in_decl : Evd.evar_map -> Id.t -> named_declaration -> bool val free_rels : Evd.evar_map -> constr -> Int.Set.t diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index 5ae0b2efd7..6d350ade8d 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -162,17 +162,27 @@ let catching_error call_trace fail (e, info) = fail located_exc end -let catch_error call_trace f x = +let update_loc ?loc (e, info) = + (e, Option.cata (Loc.add_loc info) info loc) + +let catch_error ?loc call_trace f x = try f x with e when CErrors.noncritical e -> let e = Exninfo.capture e in + let e = update_loc ?loc e in catching_error call_trace Exninfo.iraise e -let wrap_error tac k = - if is_traced () then Proofview.tclORELSE tac k else tac +let catch_error_loc ?loc tac = + Proofview.tclOR tac (fun exn -> + let (e, info) = update_loc ?loc exn in + Proofview.tclZERO ~info e) + +let wrap_error ?loc tac k = + if is_traced () then Proofview.tclORELSE tac k + else catch_error_loc ?loc tac -let catch_error_tac call_trace tac = - wrap_error +let catch_error_tac ?loc call_trace tac = + wrap_error ?loc tac (catching_error call_trace (fun (e, info) -> Proofview.tclZERO ~info e)) @@ -535,9 +545,10 @@ let interp_gen kind ist pattern_mode flags env sigma c = ltac_idents = constrvars.idents; ltac_genargs = ist.lfun; } in - let trace = push_trace (loc_of_glob_constr term,LtacConstrInterp (term,vars)) ist in + let loc = loc_of_glob_constr term in + let trace = push_trace (loc,LtacConstrInterp (term,vars)) ist in let (evd,c) = - catch_error trace (understand_ltac flags env sigma vars kind) term + catch_error ?loc trace (understand_ltac flags env sigma vars kind) term in (* spiwack: to avoid unnecessary modifications of tacinterp, as this function already use effect, I call [run] hoping it doesn't mess @@ -1059,7 +1070,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with let call = LtacAtomCall t in let trace = push_trace(loc,call) ist in Profile_ltac.do_profile "eval_tactic:2" trace - (catch_error_tac trace (interp_atomic ist t)) + (catch_error_tac ?loc trace (interp_atomic ist t)) | TacFun _ | TacLetIn _ | TacMatchGoal _ | TacMatch _ -> interp_tactic ist tac | TacId [] -> Proofview.tclLIFT (db_breakpoint (curr_debug ist) []) | TacId s -> @@ -1149,7 +1160,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with ; poly ; extra = TacStore.set ist.extra f_trace trace } in val_interp ist alias.Tacenv.alias_body >>= fun v -> - Ftactic.lift (tactic_of_value ist v) + Ftactic.lift (catch_error_loc ?loc (tactic_of_value ist v)) in let tac = Ftactic.with_env interp_vars >>= fun (env, lr) -> @@ -1175,7 +1186,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with let args = Ftactic.List.map_right (fun a -> interp_tacarg ist a) l in let tac args = let name _ _ = Pptactic.pr_extend (fun v -> print_top_val () v) 0 opn args in - Proofview.Trace.name_tactic name (catch_error_tac trace (tac args ist)) + Proofview.Trace.name_tactic name (catch_error_tac ?loc trace (tac args ist)) in Ftactic.run args tac @@ -1278,7 +1289,7 @@ and interp_app loc ist fv largs : Val.t Ftactic.t = ; extra = TacStore.set ist.extra f_trace [] } in Profile_ltac.do_profile "interp_app" trace ~count_call:false - (catch_error_tac trace (val_interp ist body)) >>= fun v -> + (catch_error_tac ?loc trace (val_interp ist body)) >>= fun v -> Ftactic.return (name_vfun (push_appl appl largs) v) end begin fun (e, info) -> diff --git a/tactics/equality.ml b/tactics/equality.ml index e1d34af13e..b92a65d767 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -1707,12 +1707,42 @@ let is_eq_x gl x d = with Constr_matching.PatternMatchingFailure -> () +exception FoundDepInGlobal of Id.t option * GlobRef.t + +let test_non_indirectly_dependent_section_variable gl x = + let env = Proofview.Goal.env gl in + let sigma = Tacmach.New.project gl in + let hyps = Proofview.Goal.hyps gl in + let concl = Proofview.Goal.concl gl in + List.iter (fun decl -> + NamedDecl.iter_constr (fun c -> + match occur_var_indirectly env sigma x c with + | Some gr -> raise (FoundDepInGlobal (Some (NamedDecl.get_id decl), gr)) + | None -> ()) decl) hyps; + match occur_var_indirectly env sigma x concl with + | Some gr -> raise (FoundDepInGlobal (None, gr)) + | None -> () + +let check_non_indirectly_dependent_section_variable gl x = + try test_non_indirectly_dependent_section_variable gl x + with FoundDepInGlobal (pos,gr) -> + let where = match pos with + | Some id -> str "hypothesis " ++ Id.print id + | None -> str "the conclusion of the goal" in + user_err ~hdr:"Subst" + (strbrk "Section variable " ++ Id.print x ++ + strbrk " occurs implicitly in global declaration " ++ Printer.pr_global gr ++ + strbrk " present in " ++ where ++ strbrk ".") + +let is_non_indirectly_dependent_section_variable gl z = + try test_non_indirectly_dependent_section_variable gl z; true + with FoundDepInGlobal (pos,gr) -> false + (* Rewrite "hyp:x=rhs" or "hyp:rhs=x" (if dir=false) everywhere and erase hyp and x; proceed by generalizing all dep hyps *) let subst_one dep_proof_ok x (hyp,rhs,dir) = Proofview.Goal.enter begin fun gl -> - let env = Proofview.Goal.env gl in let sigma = Tacmach.New.project gl in let hyps = Proofview.Goal.hyps gl in let concl = Proofview.Goal.concl gl in @@ -1721,7 +1751,7 @@ let subst_one dep_proof_ok x (hyp,rhs,dir) = List.rev (pi3 (List.fold_right (fun dcl (dest,deps,allhyps) -> let id = NamedDecl.get_id dcl in if not (Id.equal id hyp) - && List.exists (fun y -> occur_var_in_decl env sigma y dcl) deps + && List.exists (fun y -> local_occur_var_in_decl sigma y dcl) deps then let id_dest = if !regular_subst_tactic then dest else MoveLast in (dest,id::deps,(id_dest,id)::allhyps) @@ -1730,7 +1760,7 @@ let subst_one dep_proof_ok x (hyp,rhs,dir) = hyps (MoveBefore x,[x],[]))) in (* In practice, no dep hyps before x, so MoveBefore x is good enough *) (* Decides if x appears in conclusion *) - let depconcl = occur_var env sigma x concl in + let depconcl = local_occur_var sigma x concl in let need_rewrite = not (List.is_empty dephyps) || depconcl in tclTHENLIST ((if need_rewrite then @@ -1761,6 +1791,8 @@ let subst_one_var dep_proof_ok x = (str "Cannot find any non-recursive equality over " ++ Id.print x ++ str".") with FoundHyp res -> res in + if is_section_variable x then + check_non_indirectly_dependent_section_variable gl x; subst_one dep_proof_ok x res end @@ -1794,53 +1826,37 @@ let subst_all ?(flags=default_subst_tactic_flags) () = if !regular_subst_tactic then - (* First step: find hypotheses to treat in linear time *) - let find_equations gl = - let env = Proofview.Goal.env gl in - let sigma = project gl in - let find_eq_data_decompose = pf_apply find_eq_data_decompose gl in - let select_equation_name decl = + (* Find hypotheses to treat in linear time *) + let process hyp = + Proofview.Goal.enter begin fun gl -> + let env = Proofview.Goal.env gl in + let sigma = project gl in + let c = pf_get_hyp hyp gl |> NamedDecl.get_type in try - let lbeq,u,(_,x,y) = find_eq_data_decompose (NamedDecl.get_type decl) in + let lbeq,u,(_,x,y) = pf_apply find_eq_data_decompose gl c in let u = EInstance.kind sigma u in let eq = Constr.mkRef (lbeq.eq,u) in if flags.only_leibniz then restrict_to_eq_and_identity eq; match EConstr.kind sigma x, EConstr.kind sigma y with - | Var z, _ when not (is_evaluable env (EvalVarRef z)) -> - Some (NamedDecl.get_id decl) - | _, Var z when not (is_evaluable env (EvalVarRef z)) -> - Some (NamedDecl.get_id decl) + | Var x, Var y when Id.equal x y -> + Proofview.tclUNIT () + | Var x', _ when not (Termops.local_occur_var sigma x' y) && + not (is_evaluable env (EvalVarRef x')) && + is_non_indirectly_dependent_section_variable gl x' -> + subst_one flags.rewrite_dependent_proof x' (hyp,y,true) + | _, Var y' when not (Termops.local_occur_var sigma y' x) && + not (is_evaluable env (EvalVarRef y')) && + is_non_indirectly_dependent_section_variable gl y' -> + subst_one flags.rewrite_dependent_proof y' (hyp,x,false) | _ -> - None - with Constr_matching.PatternMatchingFailure -> None + Proofview.tclUNIT () + with Constr_matching.PatternMatchingFailure -> + Proofview.tclUNIT () + end in - let hyps = Proofview.Goal.hyps gl in - List.rev (List.map_filter select_equation_name hyps) - in - - (* Second step: treat equations *) - let process hyp = Proofview.Goal.enter begin fun gl -> - let sigma = project gl in - let env = Proofview.Goal.env gl in - let find_eq_data_decompose = pf_apply find_eq_data_decompose gl in - let c = pf_get_hyp hyp gl |> NamedDecl.get_type in - let _,_,(_,x,y) = find_eq_data_decompose c in - (* J.F.: added to prevent failure on goal containing x=x as an hyp *) - if EConstr.eq_constr sigma x y then Proofview.tclUNIT () else - match EConstr.kind sigma x, EConstr.kind sigma y with - | Var x', _ when not (Termops.local_occur_var sigma x' y) && not (is_evaluable env (EvalVarRef x')) -> - subst_one flags.rewrite_dependent_proof x' (hyp,y,true) - | _, Var y' when not (Termops.local_occur_var sigma y' x) && not (is_evaluable env (EvalVarRef y')) -> - subst_one flags.rewrite_dependent_proof y' (hyp,x,false) - | _ -> - Proofview.tclUNIT () + tclMAP process (List.rev (List.map NamedDecl.get_id (Proofview.Goal.hyps gl))) end - in - Proofview.Goal.enter begin fun gl -> - let ids = find_equations gl in - tclMAP process ids - end else diff --git a/test-suite/bugs/closed/bug_10812.v b/test-suite/bugs/closed/bug_10812.v new file mode 100644 index 0000000000..68f3814781 --- /dev/null +++ b/test-suite/bugs/closed/bug_10812.v @@ -0,0 +1,28 @@ +(* subst with indirectly dependent section variables *) + +Section A. + +Variable a:nat. +Definition b := a. + +Goal a=1 -> a+a=1 -> b=1. +intros. +Fail subst a. (* was working; we make it failing *) +rewrite H in H0. +discriminate. +Qed. + +Goal a=1 -> a+a=1 -> b=1. +intros. +subst. (* should not apply to a *) +rewrite H in H0. +discriminate. +Qed. + +Goal forall t, a=t -> b=t. +intros. +subst. +reflexivity. +Qed. + +End A. diff --git a/test-suite/ltac2/rebind.v b/test-suite/ltac2/rebind.v index e1c20a2059..7b3a460c8c 100644 --- a/test-suite/ltac2/rebind.v +++ b/test-suite/ltac2/rebind.v @@ -15,6 +15,39 @@ Fail foo (). constructor. Qed. + +(** Bindings are dynamic *) + +Ltac2 Type rec nat := [O | S (nat)]. + +Ltac2 rec nat_eq n m := + match n with + | O => match m with | O => true | S _ => false end + | S n => match m with | O => false | S m => nat_eq n m end + end. + +Ltac2 Type exn ::= [ Assertion_failed ]. + +Ltac2 assert_eq n m := + match nat_eq n m with + | true => () + | false => Control.throw Assertion_failed end. + +Ltac2 mutable x := O. +Ltac2 y := x. +Ltac2 Eval (assert_eq y O). +Ltac2 Set x := (S O). +Ltac2 Eval (assert_eq y (S O)). + +Ltac2 mutable quw := fun (n : nat) => O. +Ltac2 Set quw := fun n => + match n with + | O => O + | S n => S (S (quw n)) + end. + +Ltac2 Eval (quw (S (S O))). + (** Not the right type *) Fail Ltac2 Set foo := 0. @@ -25,10 +58,46 @@ Fail Ltac2 Set bar := fun _ => (). (** Subtype check *) -Ltac2 mutable rec f x := f x. +Ltac2 rec h x := h x. +Ltac2 mutable f x := h x. Fail Ltac2 Set f := fun x => x. Ltac2 mutable g x := x. +Ltac2 Set g := h. + +(** Rebinding with old values *) + + + +Ltac2 mutable qux n := S n. + +Ltac2 Set qux as self := fun n => self (self n). + +Ltac2 Eval assert_eq (qux O) (S (S O)). + +Ltac2 mutable quz := O. + +Ltac2 Set quz as self := S self. + +Ltac2 Eval (assert_eq quz (S O)). + +Ltac2 rec addn n := + match n with + | O => fun m => m + | S n => fun m => S (addn n m) + + end. +Ltac2 mutable rec quy n := + match n with + | O => S O + | S n => S (quy n) + end. -Ltac2 Set g := f. +Ltac2 Set quy as self := fun n => + match n with + | O => O + | S n => addn (self n) (quy n) + end. +Ltac2 Eval (assert_eq (quy (S (S O))) (S (S (S O)))). +Ltac2 Eval (assert_eq (quy (S (S (S O)))) (S (S (S (S (S (S O))))))). diff --git a/test-suite/output/ErrorLocation_12152_1.out b/test-suite/output/ErrorLocation_12152_1.out new file mode 100644 index 0000000000..b7b600d53d --- /dev/null +++ b/test-suite/output/ErrorLocation_12152_1.out @@ -0,0 +1,3 @@ +File "stdin", line 3, characters 0-7: +Error: No product even after head-reduction. + diff --git a/test-suite/output/ErrorLocation_12152_1.v b/test-suite/output/ErrorLocation_12152_1.v new file mode 100644 index 0000000000..e63ab1cd48 --- /dev/null +++ b/test-suite/output/ErrorLocation_12152_1.v @@ -0,0 +1,3 @@ +(* Reported in #12152 *) +Goal True. +intro H; auto. diff --git a/test-suite/output/ErrorLocation_12152_2.out b/test-suite/output/ErrorLocation_12152_2.out new file mode 100644 index 0000000000..bdfd0a050f --- /dev/null +++ b/test-suite/output/ErrorLocation_12152_2.out @@ -0,0 +1,3 @@ +File "stdin", line 3, characters 0-8: +Error: No product even after head-reduction. + diff --git a/test-suite/output/ErrorLocation_12152_2.v b/test-suite/output/ErrorLocation_12152_2.v new file mode 100644 index 0000000000..5df6bec939 --- /dev/null +++ b/test-suite/output/ErrorLocation_12152_2.v @@ -0,0 +1,3 @@ +(* Reported in #12152 *) +Goal True. +intros H; auto. diff --git a/test-suite/output/ErrorLocation_12255.out b/test-suite/output/ErrorLocation_12255.out new file mode 100644 index 0000000000..ed5e183427 --- /dev/null +++ b/test-suite/output/ErrorLocation_12255.out @@ -0,0 +1,4 @@ +File "stdin", line 4, characters 0-16: +Error: Ltac variable x is bound to i > 0 which cannot be coerced to +an evaluable reference. + diff --git a/test-suite/output/ErrorLocation_12255.v b/test-suite/output/ErrorLocation_12255.v new file mode 100644 index 0000000000..347424b2fc --- /dev/null +++ b/test-suite/output/ErrorLocation_12255.v @@ -0,0 +1,4 @@ +Ltac can_unfold x := let b := eval cbv delta [x] in x in idtac. +Definition i := O. +Goal False. +can_unfold (i>0). diff --git a/theories/Bool/Bool.v b/theories/Bool/Bool.v index 57cc8c4e90..d70978fabe 100644 --- a/theories/Bool/Bool.v +++ b/theories/Bool/Bool.v @@ -82,34 +82,39 @@ Qed. (** * Order on booleans *) (************************) -Definition leb (b1 b2:bool) := +#[ local ] Definition le (b1 b2:bool) := match b1 with | true => b2 = true | false => True end. -Hint Unfold leb: bool. +Hint Unfold le: bool. -Lemma leb_implb : forall b1 b2, leb b1 b2 <-> implb b1 b2 = true. +Lemma le_implb : forall b1 b2, le b1 b2 <-> implb b1 b2 = true. Proof. destr_bool; intuition. Qed. -Definition ltb (b1 b2:bool) := +#[deprecated(since="8.12",note="Use Bool.le instead.")] +Notation leb := le (only parsing). +#[deprecated(since="8.12",note="Use Bool.le_implb instead.")] +Notation leb_implb := le_implb (only parsing). + +#[ local ] Definition lt (b1 b2:bool) := match b1 with | true => False | false => b2 = true end. -Hint Unfold ltb: bool. +Hint Unfold lt: bool. -Definition compareb (b1 b2 : bool) := +#[ local ] Definition compare (b1 b2 : bool) := match b1, b2 with | false, true => Lt | true, false => Gt | _, _ => Eq end. -Lemma compareb_spec : forall b1 b2, - CompareSpec (b1 = b2) (ltb b1 b2) (ltb b2 b1) (compareb b1 b2). +Lemma compare_spec : forall b1 b2, + CompareSpec (b1 = b2) (lt b1 b2) (lt b2 b1) (compare b1 b2). Proof. destr_bool; auto. Qed. @@ -935,8 +940,8 @@ Defined. (** Notations *) Module BoolNotations. -Infix "<=" := leb : bool_scope. -Infix "<" := ltb : bool_scope. -Infix "?=" := compareb (at level 70) : bool_scope. +Infix "<=" := le : bool_scope. +Infix "<" := lt : bool_scope. +Infix "?=" := compare (at level 70) : bool_scope. Infix "=?" := eqb (at level 70) : bool_scope. End BoolNotations. diff --git a/theories/Bool/BoolOrder.v b/theories/Bool/BoolOrder.v index 61aab607a9..aaa7321bfc 100644 --- a/theories/Bool/BoolOrder.v +++ b/theories/Bool/BoolOrder.v @@ -14,69 +14,65 @@ Require Export Bool. Require Import Orders. - -Local Notation le := Bool.leb. -Local Notation lt := Bool.ltb. -Local Notation compare := Bool.compareb. -Local Notation compare_spec := Bool.compareb_spec. +Import BoolNotations. (** * Order [le] *) -Lemma le_refl : forall b, le b b. +Lemma le_refl : forall b, b <= b. Proof. destr_bool. Qed. Lemma le_trans : forall b1 b2 b3, - le b1 b2 -> le b2 b3 -> le b1 b3. + b1 <= b2 -> b2 <= b3 -> b1 <= b3. Proof. destr_bool. Qed. -Lemma le_true : forall b, le b true. +Lemma le_true : forall b, b <= true. Proof. destr_bool. Qed. -Lemma false_le : forall b, le false b. +Lemma false_le : forall b, false <= b. Proof. intros; constructor. Qed. -Instance le_compat : Proper (eq ==> eq ==> iff) le. +Instance le_compat : Proper (eq ==> eq ==> iff) Bool.le. Proof. intuition. Qed. (** * Strict order [lt] *) -Lemma lt_irrefl : forall b, ~ lt b b. +Lemma lt_irrefl : forall b, ~ b < b. Proof. destr_bool; auto. Qed. Lemma lt_trans : forall b1 b2 b3, - lt b1 b2 -> lt b2 b3 -> lt b1 b3. + b1 < b2 -> b2 < b3 -> b1 < b3. Proof. destr_bool; auto. Qed. -Instance lt_compat : Proper (eq ==> eq ==> iff) lt. +Instance lt_compat : Proper (eq ==> eq ==> iff) Bool.lt. Proof. intuition. Qed. -Lemma lt_trichotomy : forall b1 b2, { lt b1 b2 } + { b1 = b2 } + { lt b2 b1 }. +Lemma lt_trichotomy : forall b1 b2, { b1 < b2 } + { b1 = b2 } + { b2 < b1 }. Proof. destr_bool; auto. Qed. -Lemma lt_total : forall b1 b2, lt b1 b2 \/ b1 = b2 \/ lt b2 b1. +Lemma lt_total : forall b1 b2, b1 < b2 \/ b1 = b2 \/ b2 < b1. Proof. destr_bool; auto. Qed. -Lemma lt_le_incl : forall b1 b2, lt b1 b2 -> le b1 b2. +Lemma lt_le_incl : forall b1 b2, b1 < b2 -> b1 <= b2. Proof. destr_bool; auto. Qed. -Lemma le_lteq_dec : forall b1 b2, le b1 b2 -> { lt b1 b2 } + { b1 = b2 }. +Lemma le_lteq_dec : forall b1 b2, b1 <= b2 -> { b1 < b2 } + { b1 = b2 }. Proof. destr_bool; auto. Qed. -Lemma le_lteq : forall b1 b2, le b1 b2 <-> lt b1 b2 \/ b1 = b2. +Lemma le_lteq : forall b1 b2, b1 <= b2 <-> b1 < b2 \/ b1 = b2. Proof. destr_bool; intuition. Qed. (** * Order structures *) (* Class structure *) -Instance le_preorder : PreOrder le. +Instance le_preorder : PreOrder Bool.le. Proof. split. - intros b; apply le_refl. - intros b1 b2 b3; apply le_trans. Qed. -Instance lt_strorder : StrictOrder lt. +Instance lt_strorder : StrictOrder Bool.lt. Proof. split. - intros b; apply lt_irrefl. @@ -88,13 +84,13 @@ Module BoolOrd <: UsualDecidableTypeFull <: OrderedTypeFull <: TotalOrder. Definition t := bool. Definition eq := @eq bool. Definition eq_equiv := @eq_equivalence bool. - Definition lt := lt. + Definition lt := Bool.lt. Definition lt_strorder := lt_strorder. Definition lt_compat := lt_compat. - Definition le := le. + Definition le := Bool.le. Definition le_lteq := le_lteq. Definition lt_total := lt_total. - Definition compare := compare. + Definition compare := Bool.compare. Definition compare_spec := compare_spec. Definition eq_dec := bool_dec. Definition eq_refl := @eq_Reflexive bool. diff --git a/theories/Sets/Uniset.v b/theories/Sets/Uniset.v index 31e8cf463e..474b417e8e 100644 --- a/theories/Sets/Uniset.v +++ b/theories/Sets/Uniset.v @@ -44,18 +44,18 @@ Definition In (s:uniset) (a:A) : Prop := charac s a = true. Hint Unfold In : core. (** uniset inclusion *) -Definition incl (s1 s2:uniset) := forall a:A, leb (charac s1 a) (charac s2 a). +Definition incl (s1 s2:uniset) := forall a:A, Bool.le (charac s1 a) (charac s2 a). Hint Unfold incl : core. (** uniset equality *) Definition seq (s1 s2:uniset) := forall a:A, charac s1 a = charac s2 a. Hint Unfold seq : core. -Lemma leb_refl : forall b:bool, leb b b. +Lemma le_refl : forall b, Bool.le b b. Proof. destruct b; simpl; auto. Qed. -Hint Resolve leb_refl : core. +Hint Resolve le_refl : core. Lemma incl_left : forall s1 s2:uniset, seq s1 s2 -> incl s1 s2. Proof. diff --git a/theories/Sorting/Permutation.v b/theories/Sorting/Permutation.v index 1dd9285412..026cf32ceb 100644 --- a/theories/Sorting/Permutation.v +++ b/theories/Sorting/Permutation.v @@ -273,8 +273,8 @@ Proof. exact Permutation_length. Qed. -Instance Permutation_Forall (P : A -> Prop) : - Proper ((@Permutation A) ==> Basics.impl) (Forall P). +Global Instance Permutation_Forall (P : A -> Prop) : + Proper ((@Permutation A) ==> Basics.impl) (Forall P) | 10. Proof. intros l1 l2 HP. induction HP; intro HF; auto. @@ -283,8 +283,8 @@ Proof. inversion_clear HF2; auto. Qed. -Instance Permutation_Exists (P : A -> Prop) : - Proper ((@Permutation A) ==> Basics.impl) (Exists P). +Global Instance Permutation_Exists (P : A -> Prop) : + Proper ((@Permutation A) ==> Basics.impl) (Exists P) | 10. Proof. intros l1 l2 HP. induction HP; intro HF; auto. @@ -581,8 +581,8 @@ Proof. now contradiction (Hf x). Qed. -Instance Permutation_flat_map (g : A -> list B) : - Proper ((@Permutation A) ==> (@Permutation B)) (flat_map g). +Global Instance Permutation_flat_map (g : A -> list B) : + Proper ((@Permutation A) ==> (@Permutation B)) (flat_map g) | 10. Proof. intros l1; induction l1; intros l2 HP. - now apply Permutation_nil in HP; subst. @@ -773,7 +773,7 @@ Qed. End Permutation_alt. -Instance Permutation_list_sum : Proper (@Permutation nat ==> eq) list_sum. +Instance Permutation_list_sum : Proper (@Permutation nat ==> eq) list_sum | 10. Proof. intros l1 l2 HP; induction HP; simpl; intuition. - rewrite 2 (Nat.add_comm x). @@ -781,7 +781,7 @@ Proof. - now transitivity (list_sum l'). Qed. -Instance Permutation_list_max : Proper (@Permutation nat ==> eq) list_max. +Instance Permutation_list_max : Proper (@Permutation nat ==> eq) list_max | 10. Proof. intros l1 l2 HP; induction HP; simpl; intuition. - rewrite 2 (Nat.max_comm x). @@ -806,7 +806,7 @@ Proof. now apply (perm_t_trans IHHP2). Qed. -Instance Permutation_transp_equiv : Equivalence Permutation_transp. +Global Instance Permutation_transp_equiv : Equivalence Permutation_transp | 100. Proof. split. - intros l; apply perm_t_refl. diff --git a/user-contrib/Ltac2/g_ltac2.mlg b/user-contrib/Ltac2/g_ltac2.mlg index 13c4d667a0..8979170026 100644 --- a/user-contrib/Ltac2/g_ltac2.mlg +++ b/user-contrib/Ltac2/g_ltac2.mlg @@ -289,7 +289,7 @@ GRAMMAR EXTEND Gram ] ] ; tac2def_mut: - [ [ "Set"; qid = Prim.qualid; ":="; e = tac2expr -> { StrMut (qid, e) } ] ] + [ [ "Set"; qid = Prim.qualid; old = OPT [ "as"; id = locident -> { id } ]; ":="; e = tac2expr -> { StrMut (qid, old, e) } ] ] ; tac2typ_knd: [ [ t = tac2type -> { CTydDef (Some t) } diff --git a/user-contrib/Ltac2/tac2entries.ml b/user-contrib/Ltac2/tac2entries.ml index 28e877491e..987cd8c1b8 100644 --- a/user-contrib/Ltac2/tac2entries.ml +++ b/user-contrib/Ltac2/tac2entries.ml @@ -336,7 +336,7 @@ let register_ltac ?(local = false) ?(mut = false) isrec tactics = if isrec then inline_rec_tactic tactics else tactics in let map ({loc;v=id}, e) = - let (e, t) = intern ~strict:true e in + let (e, t) = intern ~strict:true [] e in let () = if not (is_value e) then user_err ?loc (str "Tactic definition must be a syntactical value") @@ -728,19 +728,26 @@ let register_notation ?(local = false) tkn lev body = match tkn, lev with type redefinition = { redef_kn : ltac_constant; redef_body : glb_tacexpr; + redef_old : Id.t option; } let perform_redefinition (_, redef) = let kn = redef.redef_kn in let data = Tac2env.interp_global kn in - let data = { data with Tac2env.gdata_expr = redef.redef_body } in + let body = match redef.redef_old with + | None -> redef.redef_body + | Some id -> + (* Rebind the old value with a let-binding *) + GTacLet (false, [Name id, data.Tac2env.gdata_expr], redef.redef_body) + in + let data = { data with Tac2env.gdata_expr = body } in Tac2env.define_global kn data let subst_redefinition (subst, redef) = let kn = Mod_subst.subst_kn subst redef.redef_kn in let body = Tac2intern.subst_expr subst redef.redef_body in if kn == redef.redef_kn && body == redef.redef_body then redef - else { redef_kn = kn; redef_body = body } + else { redef_kn = kn; redef_body = body; redef_old = redef.redef_old } let classify_redefinition o = Substitute o @@ -751,7 +758,7 @@ let inTac2Redefinition : redefinition -> obj = subst_function = subst_redefinition; classify_function = classify_redefinition } -let register_redefinition ?(local = false) qid e = +let register_redefinition ?(local = false) qid old e = let kn = try Tac2env.locate_ltac qid with Not_found -> user_err ?loc:qid.CAst.loc (str "Unknown tactic " ++ pr_qualid qid) @@ -766,7 +773,11 @@ let register_redefinition ?(local = false) qid e = if not (data.Tac2env.gdata_mutable) then user_err ?loc:qid.CAst.loc (str "The tactic " ++ pr_qualid qid ++ str " is not declared as mutable") in - let (e, t) = intern ~strict:true e in + let ctx = match old with + | None -> [] + | Some { CAst.v = id } -> [id, data.Tac2env.gdata_type] + in + let (e, t) = intern ~strict:true ctx e in let () = if not (is_value e) then user_err ?loc:qid.CAst.loc (str "Tactic definition must be a syntactical value") @@ -777,15 +788,17 @@ let register_redefinition ?(local = false) qid e = user_err ?loc:qid.CAst.loc (str "Type " ++ pr_glbtype name (snd t) ++ str " is not a subtype of " ++ pr_glbtype name (snd data.Tac2env.gdata_type)) in + let old = Option.map (fun { CAst.v = id } -> id) old in let def = { redef_kn = kn; redef_body = e; + redef_old = old; } in Lib.add_anonymous_leaf (inTac2Redefinition def) let perform_eval ~pstate e = let env = Global.env () in - let (e, ty) = Tac2intern.intern ~strict:false e in + let (e, ty) = Tac2intern.intern ~strict:false [] e in let v = Tac2interp.interp Tac2interp.empty_environment e in let selector, proof = match pstate with @@ -818,7 +831,7 @@ let register_struct ?local str = match str with | StrTyp (isrec, t) -> register_type ?local isrec t | StrPrm (id, t, ml) -> register_primitive ?local id t ml | StrSyn (tok, lev, e) -> register_notation ?local tok lev e -| StrMut (qid, e) -> register_redefinition ?local qid e +| StrMut (qid, old, e) -> register_redefinition ?local qid old e (** Toplevel exception *) @@ -913,7 +926,7 @@ let solve ~pstate default tac = let call ~pstate ~default e = let loc = e.loc in - let (e, t) = intern ~strict:false e in + let (e, t) = intern ~strict:false [] e in let () = check_unit ?loc t in let tac = Tac2interp.interp Tac2interp.empty_environment e in solve ~pstate default (Proofview.tclIGNORE tac) diff --git a/user-contrib/Ltac2/tac2expr.mli b/user-contrib/Ltac2/tac2expr.mli index a95d8cc49f..548655f561 100644 --- a/user-contrib/Ltac2/tac2expr.mli +++ b/user-contrib/Ltac2/tac2expr.mli @@ -168,7 +168,7 @@ type strexpr = (** External definition *) | StrSyn of sexpr list * int option * raw_tacexpr (** Syntactic extensions *) -| StrMut of qualid * raw_tacexpr +| StrMut of qualid * Names.lident option * raw_tacexpr (** Redefinition of mutable globals *) (** {5 Dynamic semantics} *) diff --git a/user-contrib/Ltac2/tac2intern.ml b/user-contrib/Ltac2/tac2intern.ml index a4f385d432..797f72702d 100644 --- a/user-contrib/Ltac2/tac2intern.ml +++ b/user-contrib/Ltac2/tac2intern.ml @@ -396,11 +396,13 @@ let is_pure_constructor kn = let rec is_value = function | GTacAtm (AtmInt _) | GTacVar _ | GTacRef _ | GTacFun _ -> true -| GTacAtm (AtmStr _) | GTacApp _ | GTacLet _ -> false +| GTacAtm (AtmStr _) | GTacApp _ | GTacLet (true, _, _) -> false | GTacCst (Tuple _, _, el) -> List.for_all is_value el | GTacCst (_, _, []) -> true | GTacOpn (_, el) -> List.for_all is_value el | GTacCst (Other kn, _, el) -> is_pure_constructor kn && List.for_all is_value el +| GTacLet (false, bnd, e) -> + is_value e && List.for_all (fun (_, e) -> is_value e) bnd | GTacCse _ | GTacPrj _ | GTacSet _ | GTacExt _ | GTacPrm _ | GTacWth _ -> false @@ -458,6 +460,10 @@ let monomorphic (t : UF.elt glb_typexpr) : mix_type_scheme = let subst id = GTypVar (GVar id) in (0, subst_type subst t) +let polymorphic ((n, t) : type_scheme) : mix_type_scheme = + let subst id = GTypVar (LVar id) in + (n, subst_type subst t) + let warn_not_unit = CWarnings.create ~name:"not-unit" ~category:"ltac" (fun () -> strbrk "The following expression should have type unit.") @@ -1138,9 +1144,13 @@ let normalize env (count, vars) (t : UF.elt glb_typexpr) = in subst_type subst t -let intern ~strict e = +type context = (Id.t * type_scheme) list + +let intern ~strict ctx e = let env = empty_env () in let env = if strict then env else { env with env_str = false } in + let fold accu (id, t) = push_name (Name id) (polymorphic t) accu in + let env = List.fold_left fold env ctx in let (e, t) = intern_rec env e in let count = ref 0 in let vars = ref UF.Map.empty in diff --git a/user-contrib/Ltac2/tac2intern.mli b/user-contrib/Ltac2/tac2intern.mli index 8b09ecbcf7..ed251d6201 100644 --- a/user-contrib/Ltac2/tac2intern.mli +++ b/user-contrib/Ltac2/tac2intern.mli @@ -12,7 +12,9 @@ open Names open Mod_subst open Tac2expr -val intern : strict:bool -> raw_tacexpr -> glb_tacexpr * type_scheme +type context = (Id.t * type_scheme) list + +val intern : strict:bool -> context -> raw_tacexpr -> glb_tacexpr * type_scheme val intern_typedef : (KerName.t * int) Id.Map.t -> raw_quant_typedef -> glb_quant_typedef val intern_open_type : raw_typexpr -> type_scheme diff --git a/user-contrib/Ltac2/tac2interp.ml b/user-contrib/Ltac2/tac2interp.ml index 54f2da0621..ed783afce7 100644 --- a/user-contrib/Ltac2/tac2interp.ml +++ b/user-contrib/Ltac2/tac2interp.ml @@ -86,7 +86,7 @@ let rec interp (ist : environment) = function | GTacVar id -> return (get_var ist id) | GTacRef kn -> let data = get_ref ist kn in - return (eval_pure (Some kn) data) + return (eval_pure Id.Map.empty (Some kn) data) | GTacFun (ids, e) -> let cls = { clos_ref = None; clos_env = ist.env_ist; clos_var = ids; clos_exp = e } in let f = interp_app cls in @@ -187,26 +187,41 @@ and interp_set ist e p r = let () = Valexpr.set_field e p r in return (Valexpr.make_int 0) -and eval_pure kn = function +and eval_pure bnd kn = function +| GTacVar id -> Id.Map.get id bnd | GTacAtm (AtmInt n) -> Valexpr.make_int n | GTacRef kn -> let { Tac2env.gdata_expr = e } = try Tac2env.interp_global kn with Not_found -> assert false in - eval_pure (Some kn) e + eval_pure bnd (Some kn) e | GTacFun (na, e) -> - let cls = { clos_ref = kn; clos_env = Id.Map.empty; clos_var = na; clos_exp = e } in + let cls = { clos_ref = kn; clos_env = bnd; clos_var = na; clos_exp = e } in let f = interp_app cls in Tac2ffi.of_closure f | GTacCst (_, n, []) -> Valexpr.make_int n -| GTacCst (_, n, el) -> Valexpr.make_block n (Array.map_of_list eval_unnamed el) -| GTacOpn (kn, el) -> Tac2ffi.of_open (kn, Array.map_of_list eval_unnamed el) -| GTacAtm (AtmStr _) | GTacLet _ | GTacVar _ | GTacSet _ +| GTacCst (_, n, el) -> Valexpr.make_block n (eval_pure_args bnd el) +| GTacOpn (kn, el) -> Tac2ffi.of_open (kn, eval_pure_args bnd el) +| GTacLet (isrec, vals, body) -> + let () = assert (not isrec) in + let fold accu (na, e) = match na with + | Anonymous -> + (* No need to evaluate, we know this is a value *) + accu + | Name id -> + let v = eval_pure bnd None e in + Id.Map.add id v accu + in + let bnd = List.fold_left fold bnd vals in + eval_pure bnd kn body +| GTacAtm (AtmStr _) | GTacSet _ | GTacApp _ | GTacCse _ | GTacPrj _ | GTacPrm _ | GTacExt _ | GTacWth _ -> anomaly (Pp.str "Term is not a syntactical value") -and eval_unnamed e = eval_pure None e +and eval_pure_args bnd args = + let map e = eval_pure bnd None e in + Array.map_of_list map args (** Cross-boundary hacks. *) |