From 3be2307af0f1316630b46078fd6b4367c283472d Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Mon, 3 Oct 2016 13:57:16 +0200 Subject: Remove if_then_else. Use tryif instead. if_then_else definition does not account for multi success tactics. tryif_then_else is a primitive tactical with the expected behavior. --- theories/FSets/FSetDecide.v | 19 +++++-------------- theories/MSets/MSetDecide.v | 19 +++++-------------- 2 files changed, 10 insertions(+), 28 deletions(-) diff --git a/theories/FSets/FSetDecide.v b/theories/FSets/FSetDecide.v index ad067eb3d8..1db6a71e81 100644 --- a/theories/FSets/FSetDecide.v +++ b/theories/FSets/FSetDecide.v @@ -357,17 +357,8 @@ the above form: | _ => idtac end. - (** [if t then t1 else t2] executes [t] and, if it does not - fail, then [t1] will be applied to all subgoals - produced. If [t] fails, then [t2] is executed. *) - Tactic Notation - "if" tactic(t) - "then" tactic(t1) - "else" tactic(t2) := - first [ t; first [ t1 | fail 2 ] | t2 ]. - Ltac abstract_term t := - if (is_var t) then fail "no need to abstract a variable" + tryif (is_var t) then fail "no need to abstract a variable" else (let x := fresh "x" in set (x := t) in *; try clearbody x). Ltac abstract_elements := @@ -478,11 +469,11 @@ the above form: repeat ( match goal with | H : context [ @Logic.eq ?T ?x ?y ] |- _ => - if (change T with E.t in H) then fail - else if (change T with t in H) then fail + tryif (change T with E.t in H) then fail + else tryif (change T with t in H) then fail else clear H | H : ?P |- _ => - if prop (FSet_Prop P) holds by + tryif prop (FSet_Prop P) holds by (auto 100 with FSet_Prop) then fail else clear H @@ -747,7 +738,7 @@ the above form: | H: (In ?x ?r) -> False |- (E.eq ?y ?x) -> False => contradict H; fsetdec_body | H: ?P -> False |- ?Q -> False => - if prop (FSet_elt_Prop P) holds by + tryif prop (FSet_elt_Prop P) holds by (auto 100 with FSet_Prop) then (contradict H; fsetdec_body) else fsetdec_body diff --git a/theories/MSets/MSetDecide.v b/theories/MSets/MSetDecide.v index f2555791b2..9c622fd786 100644 --- a/theories/MSets/MSetDecide.v +++ b/theories/MSets/MSetDecide.v @@ -357,17 +357,8 @@ the above form: | _ => idtac end. - (** [if t then t1 else t2] executes [t] and, if it does not - fail, then [t1] will be applied to all subgoals - produced. If [t] fails, then [t2] is executed. *) - Tactic Notation - "if" tactic(t) - "then" tactic(t1) - "else" tactic(t2) := - first [ t; first [ t1 | fail 2 ] | t2 ]. - Ltac abstract_term t := - if (is_var t) then fail "no need to abstract a variable" + tryif (is_var t) then fail "no need to abstract a variable" else (let x := fresh "x" in set (x := t) in *; try clearbody x). Ltac abstract_elements := @@ -478,11 +469,11 @@ the above form: repeat ( match goal with | H : context [ @Logic.eq ?T ?x ?y ] |- _ => - if (change T with E.t in H) then fail - else if (change T with t in H) then fail + tryif (change T with E.t in H) then fail + else tryif (change T with t in H) then fail else clear H | H : ?P |- _ => - if prop (MSet_Prop P) holds by + tryif prop (MSet_Prop P) holds by (auto 100 with MSet_Prop) then fail else clear H @@ -747,7 +738,7 @@ the above form: | H: (In ?x ?r) -> False |- (E.eq ?y ?x) -> False => contradict H; fsetdec_body | H: ?P -> False |- ?Q -> False => - if prop (MSet_elt_Prop P) holds by + tryif prop (MSet_elt_Prop P) holds by (auto 100 with MSet_Prop) then (contradict H; fsetdec_body) else fsetdec_body -- cgit v1.2.3 From d226adf01f20ea946bbeac4d4c5cde75a4d77f32 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Tue, 11 Oct 2016 11:57:46 +0200 Subject: Fix bug #5123: mark all shelved evars unresolvable Previously, some splipped through and were caught by unrelated calls to typeclass resolution. --- proofs/proof.ml | 9 ++++++++- proofs/proofview.ml | 36 ++++++++++++++++++++++-------------- proofs/proofview.mli | 8 ++++++-- test-suite/bugs/closed/5123.v | 31 +++++++++++++++++++++++++++++++ 4 files changed, 67 insertions(+), 17 deletions(-) create mode 100644 test-suite/bugs/closed/5123.v diff --git a/proofs/proof.ml b/proofs/proof.ml index 0489305aa7..1f094b3391 100644 --- a/proofs/proof.ml +++ b/proofs/proof.ml @@ -343,13 +343,20 @@ let run_tactic env tac pr = they to be marked as unresolvable. *) let undef l = List.filter (fun g -> Evd.is_undefined sigma g) l in let retrieved = undef (List.rev (Evd.future_goals sigma)) in - let shelf = (undef pr.shelf)@retrieved@(undef to_shelve) in + let to_shelve = undef to_shelve in + let shelf = (undef pr.shelf)@retrieved@to_shelve in let proofview = List.fold_left Proofview.Unsafe.mark_as_goal tacticced_proofview retrieved in + let proofview = + List.fold_left + Proofview.Unsafe.mark_as_unresolvable + proofview + to_shelve + in let given_up = pr.given_up@give_up in let proofview = Proofview.Unsafe.reset_future_goals proofview in { pr with proofview ; shelf ; given_up },(status,info_trace) diff --git a/proofs/proofview.ml b/proofs/proofview.ml index ae7e2b79a8..d166f46b23 100644 --- a/proofs/proofview.ml +++ b/proofs/proofview.ml @@ -642,6 +642,18 @@ let unshelve l p = let l = undefined p.solution l in { p with comb = p.comb@l } +let mark_in_evm ~goal evd content = + let info = Evd.find evd content in + let info = + if goal then + { info with Evd.evar_source = match info.Evd.evar_source with + | _, (Evar_kinds.VarInstance _ | Evar_kinds.GoalEvar) as x -> x + | loc,_ -> loc,Evar_kinds.GoalEvar } + else info + in + let info = Typeclasses.mark_unresolvable info in + Evd.add evd content info + let with_shelf tac = let open Proof in Pv.get >>= fun pv -> @@ -654,8 +666,11 @@ let with_shelf tac = let fgoals = Evd.future_goals solution in let pgoal = Evd.principal_future_goal solution in let sigma = Evd.restore_future_goals sigma fgoals pgoal in - Pv.set { npv with shelf; solution = sigma } >> - tclUNIT (CList.rev_append gls' gls, ans) + (* Ensure we mark and return only unsolved goals *) + let gls' = undefined sigma (CList.rev_append gls' gls) in + let sigma = CList.fold_left (mark_in_evm ~goal:false) sigma gls' in + let npv = { npv with shelf; solution = sigma } in + Pv.set npv >> tclUNIT (gls', ans) (** [goodmod p m] computes the representative of [p] modulo [m] in the interval [[0,m-1]].*) @@ -893,18 +908,11 @@ module Unsafe = struct let reset_future_goals p = { p with solution = Evd.reset_future_goals p.solution } - let mark_as_goal_evm evd content = - let info = Evd.find evd content in - let info = - { info with Evd.evar_source = match info.Evd.evar_source with - | _, (Evar_kinds.VarInstance _ | Evar_kinds.GoalEvar) as x -> x - | loc,_ -> loc,Evar_kinds.GoalEvar } - in - let info = Typeclasses.mark_unresolvable info in - Evd.add evd content info - let mark_as_goal p gl = - { p with solution = mark_as_goal_evm p.solution gl } + { p with solution = mark_in_evm ~goal:true p.solution gl } + + let mark_as_unresolvable p gl = + { p with solution = mark_in_evm ~goal:false p.solution gl } end @@ -1107,7 +1115,7 @@ struct let sigma = Evd.restore_future_goals sigma prev_future_goals prev_principal_goal in (** Select the goals *) let comb = undefined sigma (CList.rev evs) in - let sigma = CList.fold_left Unsafe.mark_as_goal_evm sigma comb in + let sigma = CList.fold_left (mark_in_evm ~goal:true) sigma comb in let open Proof in InfoL.leaf (Info.Tactic (fun () -> Pp.(hov 2 (str"simple refine"++spc()++ Hook.get pr_constrv env sigma c)))) >> Pv.modify (fun ps -> { ps with solution = sigma; comb; }) diff --git a/proofs/proofview.mli b/proofs/proofview.mli index 1a367f4eac..c8d96fe794 100644 --- a/proofs/proofview.mli +++ b/proofs/proofview.mli @@ -303,8 +303,9 @@ val guard_no_unifiable : unit tactic goals of p *) val unshelve : Goal.goal list -> proofview -> proofview -(** [with_shelf tac] executes [tac] and returns its result together with the set - of goals shelved by [tac]. The current shelf is unchanged. *) +(** [with_shelf tac] executes [tac] and returns its result together with + the set of goals shelved by [tac]. The current shelf is unchanged + and the returned list contains only unsolved goals. *) val with_shelf : 'a tactic -> (Goal.goal list * 'a) tactic (** If [n] is positive, [cycle n] puts the [n] first goal last. If [n] @@ -407,6 +408,9 @@ module Unsafe : sig (** Give an evar the status of a goal (changes its source location and makes it unresolvable for type classes. *) val mark_as_goal : proofview -> Evar.t -> proofview + + (** Make an evar unresolvable for type classes. *) + val mark_as_unresolvable : proofview -> Evar.t -> proofview end (** {7 Notations} *) diff --git a/test-suite/bugs/closed/5123.v b/test-suite/bugs/closed/5123.v new file mode 100644 index 0000000000..c171a10d10 --- /dev/null +++ b/test-suite/bugs/closed/5123.v @@ -0,0 +1,31 @@ +(* IN 8.5pl2 and 8.6 (4da2131), the following shows different typeclass resolution behaviors following an unshelve tactical vs. an Unshelve command: *) + +(*Pose an open constr to prevent immediate typeclass resolution in holes:*) +Tactic Notation "opose" open_constr(x) "as" ident(H) := pose x as H. + +Inductive vect A : nat -> Type := +| vnil : vect A 0 +| vcons : forall (h:A) (n:nat), vect A n -> vect A (S n). + +Class Eqdec A := eqdec : forall a b : A, {a=b}+{a<>b}. + +Require Bool. + +Instance Bool_eqdec : Eqdec bool := Bool.bool_dec. + +Context `{vect_sigT_eqdec : forall A : Type, Eqdec A -> Eqdec {a : nat & vect A a}}. + +Typeclasses eauto := debug. + +Goal True. + unshelve opose (@vect_sigT_eqdec _ _ _ _) as H. + all:cycle 2. + eapply existT. (*BUG: Why does this do typeclass resolution in the evar?*) +Abort. + +Goal True. + opose (@vect_sigT_eqdec _ _ _ _) as H. + Unshelve. + all:cycle 3. + eapply existT. (*This does no typeclass resultion, which is correct.*) +Abort. \ No newline at end of file -- cgit v1.2.3 From 2bcae5b7a22019718973f65cafd271f735d3d85b Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Tue, 11 Oct 2016 16:33:26 +0200 Subject: Fix test-suite file 5123 to fail in case of regression --- test-suite/bugs/closed/5123.v | 2 ++ 1 file changed, 2 insertions(+) diff --git a/test-suite/bugs/closed/5123.v b/test-suite/bugs/closed/5123.v index c171a10d10..bcde510ee6 100644 --- a/test-suite/bugs/closed/5123.v +++ b/test-suite/bugs/closed/5123.v @@ -21,6 +21,7 @@ Goal True. unshelve opose (@vect_sigT_eqdec _ _ _ _) as H. all:cycle 2. eapply existT. (*BUG: Why does this do typeclass resolution in the evar?*) + Focus 5. Abort. Goal True. @@ -28,4 +29,5 @@ Goal True. Unshelve. all:cycle 3. eapply existT. (*This does no typeclass resultion, which is correct.*) + Focus 5. Abort. \ No newline at end of file -- cgit v1.2.3 From 5dd690ee5975262d34d8dcc44191138c8d326f65 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 16 Jul 2016 16:24:59 +0200 Subject: Fixing a collision about the meta-variable ".." in recursive notations. This happens when recursive notations are used to define recursive notations. --- interp/constrintern.ml | 20 ++++++++------------ test-suite/success/Notations.v | 3 +++ 2 files changed, 11 insertions(+), 12 deletions(-) diff --git a/interp/constrintern.ml b/interp/constrintern.ml index f30d3cefad..478adf0115 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -517,27 +517,24 @@ let rec subordinate_letins letins = function | [] -> letins,[] -let rec subst_iterator y t = function - | GVar (_,id) as x -> if Id.equal id y then t else x - | x -> map_glob_constr (subst_iterator y t) x - let subst_aconstr_in_glob_constr loc intern (_,ntnvars as lvar) subst infos c = let (terms,termlists,binders) = subst in (* when called while defining a notation, avoid capturing the private binders of the expression by variables bound by the notation (see #3892) *) let avoid = Id.Map.domain ntnvars in - let rec aux (terms,binderopt as subst') (renaming,env) c = + let rec aux (terms,binderopt,terminopt as subst') (renaming,env) c = let subinfos = renaming,{env with tmp_scope = None} in match c with + | NVar id when Id.equal id ldots_var -> Option.get terminopt | NVar id -> subst_var subst' (renaming, env) id | NList (x,_,iter,terminator,lassoc) -> (try (* All elements of the list are in scopes (scopt,subscopes) *) let (l,(scopt,subscopes)) = Id.Map.find x termlists in - let termin = aux subst' subinfos terminator in + let termin = aux (terms,None,None) subinfos terminator in let fold a t = let nterms = Id.Map.add x (a, (scopt, subscopes)) terms in - subst_iterator ldots_var t (aux (nterms, binderopt) subinfos iter) + aux (nterms,None,Some t) subinfos iter in List.fold_right fold (if lassoc then List.rev l else l) termin with Not_found -> @@ -582,10 +579,9 @@ let subst_aconstr_in_glob_constr loc intern (_,ntnvars as lvar) subst infos c = let (bl,(scopt,subscopes)) = Id.Map.find x binders in let env,bl = List.fold_left (intern_local_binder_aux intern lvar) (env,[]) bl in let letins,bl = subordinate_letins [] bl in - let termin = aux subst' (renaming,env) terminator in + let termin = aux (terms,None,None) (renaming,env) terminator in let res = List.fold_left (fun t binder -> - subst_iterator ldots_var t - (aux (terms,Some(x,binder)) subinfos iter)) + aux (terms,Some(x,binder),Some t) subinfos iter) termin bl in make_letins letins res with Not_found -> @@ -610,7 +606,7 @@ let subst_aconstr_in_glob_constr loc intern (_,ntnvars as lvar) subst infos c = | t -> glob_constr_of_notation_constr_with_binders loc (traverse_binder subst avoid) (aux subst') subinfos t - and subst_var (terms, binderopt) (renaming, env) id = + and subst_var (terms, _binderopt, _terminopt) (renaming, env) id = (* subst remembers the delimiters stack in the interpretation *) (* of the notations *) try @@ -623,7 +619,7 @@ let subst_aconstr_in_glob_constr loc intern (_,ntnvars as lvar) subst infos c = with Not_found -> (* Happens for local notation joint with inductive/fixpoint defs *) GVar (loc,id) - in aux (terms,None) infos c + in aux (terms,None,None) infos c let split_by_type ids = List.fold_right (fun (x,(scl,typ)) (l1,l2,l3) -> diff --git a/test-suite/success/Notations.v b/test-suite/success/Notations.v index b72a067407..2f7c62972a 100644 --- a/test-suite/success/Notations.v +++ b/test-suite/success/Notations.v @@ -107,3 +107,6 @@ Notation traverse_var f l := (traverse (fun l => f l) l). Notation "'intros' x" := (S x) (at level 0). Goal True -> True. intros H. exact H. Qed. + +(* Check absence of collision on ".." in nested notations with ".." *) +Notation "[ a , .. , b ]" := (a, (.. (b,tt) ..)). -- cgit v1.2.3