Merge PR #12256: Move the static check of evaluability in unfold tact…

…ic to runtime.

Reviewed-by: herbelin

doc/changelog/04-tactics/12256-unfold-dyn-check.rst

@@ -0,0 +1,4 @@
+- **Changed:**
+  The check that unfold arguments were indeed unfoldable has been moved to runtime
+  (`#12256 <https://github.com/coq/coq/pull/12256>`_,
+  by Pierre-Marie Pédrot).

doc/sphinx/proof-engine/tactics.rst

@@ -3393,26 +3393,14 @@ the conversion in hypotheses :n:`{+ @ident}`.
    never unfolded by tactics like :tacn:`simpl` and :tacn:`cbn` or to
    ensure that unfolding does not fail.
 
-   .. note::
-
-      This tactic unfortunately does not yet play well with tactic
-      internalization, resulting in interpretation-time errors when
-      you try to use it directly with opaque identifiers, as seen in
-      the first (failing) use of :tacn:`with_strategy` in the
-      following example.  This can be worked around by binding the
-      identifier to an |Ltac| variable, and this issue should
-      disappear in a future version of |Coq|; see `#12179
-      <https://github.com/coq/coq/issues/12179>`_.
-
    .. example::
 
       .. coqtop:: all reset abort
 
          Opaque id.
          Goal id 10 = 10.
          Fail unfold id.
-         Fail with_strategy transparent [id] unfold id.
-         let id' := id in with_strategy transparent [id] unfold id'.
+         with_strategy transparent [id] unfold id.
 
    .. warning::
 

interp/notation.ml

@@ -1809,10 +1809,10 @@ let browse_notation strict ntn map =
       map [] in
   List.sort (fun x y -> String.compare (snd (fst x)) (snd (fst y))) l
 
-let global_reference_of_notation test (ntn,(sc,c,_)) =
+let global_reference_of_notation ~head test (ntn,(sc,c,_)) =
   match c with
   | NRef ref when test ref -> Some (ntn,sc,ref)
-  | NApp (NRef ref, l) when List.for_all isNVar_or_NHole l && test ref ->
+  | NApp (NRef ref, l) when head || List.for_all isNVar_or_NHole l && test ref ->
       Some (ntn,sc,ref)
   | _ -> None
 
@@ -1824,14 +1824,14 @@ let error_notation_not_reference ?loc ntn =
    (str "Unable to interpret " ++ quote (str ntn) ++
     str " as a reference.")
 
-let interp_notation_as_global_reference ?loc test ntn sc =
+let interp_notation_as_global_reference ?loc ~head test ntn sc =
   let scopes = match sc with
   | Some sc ->
       let scope = find_scope (find_delimiters_scope sc) in
       String.Map.add sc scope String.Map.empty
   | None -> !scope_map in
   let ntns = browse_notation true ntn scopes in
-  let refs = List.map (global_reference_of_notation test) ntns in
+  let refs = List.map (global_reference_of_notation ~head test) ntns in
   match Option.List.flatten refs with
   | [_,_,ref] -> ref
   | [] -> error_notation_not_reference ?loc ntn

interp/notation.mli

@@ -245,7 +245,8 @@ val availability_of_notation : specific_notation -> subscopes ->
 
 (** {6 Miscellaneous} *)
 
-val interp_notation_as_global_reference : ?loc:Loc.t -> (GlobRef.t -> bool) ->
+(** If head is true, also allows applied global references. *)
+val interp_notation_as_global_reference : ?loc:Loc.t -> head:bool -> (GlobRef.t -> bool) ->
       notation_key -> delimiters option -> GlobRef.t
 
 (** Checks for already existing notations *)

interp/smartlocate.ml

@@ -62,15 +62,15 @@ let global_with_alias ?head qid =
   try locate_global_with_alias ?head qid
   with Not_found -> Nametab.error_global_not_found qid
 
-let smart_global ?head = let open Constrexpr in CAst.with_loc_val (fun ?loc -> function
+let smart_global ?(head = false) = let open Constrexpr in CAst.with_loc_val (fun ?loc -> function
   | AN r ->
-    global_with_alias ?head r
+    global_with_alias ~head r
   | ByNotation (ntn,sc) ->
-    Notation.interp_notation_as_global_reference ?loc (fun _ -> true) ntn sc)
+    Notation.interp_notation_as_global_reference ?loc ~head (fun _ -> true) ntn sc)
 
 let smart_global_inductive = let open Constrexpr in CAst.with_loc_val (fun ?loc -> function
   | AN r ->
     global_inductive_with_alias r
   | ByNotation (ntn,sc) ->
     destIndRef
-      (Notation.interp_notation_as_global_reference ?loc isIndRef ntn sc))
+      (Notation.interp_notation_as_global_reference ?loc ~head:false isIndRef ntn sc))

plugins/ltac/tacintern.ml

@@ -14,7 +14,6 @@ open CAst
 open Pattern
 open Genredexpr
 open Glob_term
-open Tacred
 open Util
 open Names
 open Libnames
@@ -98,7 +97,7 @@ let intern_global_reference ist qid =
   else if qualid_is_ident qid && find_hyp (qualid_basename qid) ist then
     let id = qualid_basename qid in
     ArgArg (qid.CAst.loc, GlobRef.VarRef id)
-  else match locate_global_with_alias qid with
+  else match locate_global_with_alias ~head:true qid with
   | r -> ArgArg (qid.CAst.loc, r)
   | exception Not_found ->
     if not !strict_check && qualid_is_ident qid then
@@ -294,45 +293,43 @@ let intern_destruction_arg ist = function
       else
         clear,ElimOnIdent (make ?loc id)
 
-let short_name = function
-  | {v=AN qid} when qualid_is_ident qid && not !strict_check ->
+let short_name qid =
+  if qualid_is_ident qid && not !strict_check then
     Some (make ?loc:qid.CAst.loc @@ qualid_basename qid)
-  | _ -> None
-
-let intern_evaluable_global_reference ist qid =
-  try evaluable_of_global_reference ist.genv (locate_global_with_alias ~head:true qid)
-  with Not_found ->
-  if qualid_is_ident qid && not !strict_check then EvalVarRef (qualid_basename qid)
-  else Nametab.error_global_not_found qid
-
-let intern_evaluable_reference_or_by_notation ist = function
-  | {v=AN r} -> intern_evaluable_global_reference ist r
+  else None
+
+let evalref_of_globref ?loc ?short = function
+  | GlobRef.ConstRef cst -> ArgArg (EvalConstRef cst, short)
+  | GlobRef.VarRef id -> ArgArg (EvalVarRef id, short)
+  | r ->
+    let tpe = match r with
+    | GlobRef.IndRef _ -> "inductive"
+    | GlobRef.ConstructRef _ -> "constructor"
+    | (GlobRef.VarRef _ | GlobRef.ConstRef _) -> assert false
+    in
+    user_err ?loc (str "Cannot turn" ++ spc () ++ str tpe ++ spc () ++
+      Nametab.pr_global_env Id.Set.empty r ++ spc () ++
+      str "into an evaluable reference.")
+
+let intern_evaluable ist = function
+  | {v=AN qid} ->
+    begin match intern_global_reference ist qid with
+    | ArgVar _ as v -> v
+    | ArgArg (loc, r) ->
+      let short = short_name qid in
+      evalref_of_globref ?loc ?short r
+    end
   | {v=ByNotation (ntn,sc);loc} ->
-      evaluable_of_global_reference ist.genv
-      (Notation.interp_notation_as_global_reference ?loc
-        GlobRef.(function ConstRef _ | VarRef _ -> true | _ -> false) ntn sc)
+    let check = GlobRef.(function ConstRef _ | VarRef _ -> true | _ -> false) in
+    let r = Notation.interp_notation_as_global_reference ?loc ~head:true check ntn sc in
+    evalref_of_globref ?loc r
 
 let intern_smart_global ist = function
   | {v=AN r} -> intern_global_reference ist r
   | {v=ByNotation (ntn,sc);loc} ->
-      ArgArg (loc, (Notation.interp_notation_as_global_reference ?loc
+      ArgArg (loc, (Notation.interp_notation_as_global_reference ?loc ~head:true
         GlobRef.(function ConstRef _ | VarRef _ -> true | _ -> false) ntn sc))
 
-(* Globalize a reduction expression *)
-let intern_evaluable ist r =
-  let f ist r =
-    let e = intern_evaluable_reference_or_by_notation ist r in
-    let na = short_name r in
-    ArgArg (e,na)
-  in
-  match r with
-  | {v=AN qid} when qualid_is_ident qid && find_var (qualid_basename qid) ist ->
-    ArgVar (make ?loc:qid.CAst.loc @@ qualid_basename qid)
-  | {v=AN qid} when qualid_is_ident qid && not !strict_check && find_hyp (qualid_basename qid) ist ->
-    let id = qualid_basename qid in
-      ArgArg (EvalVarRef id, Some (make ?loc:qid.CAst.loc id))
-  | _ -> f ist r
-
 let intern_unfold ist (l,qid) = (l,intern_evaluable ist qid)
 
 let intern_flag ist red =
@@ -393,10 +390,10 @@ let intern_typed_pattern_or_ref_with_occurrences ist (l,p) =
       let c = Constrintern.interp_reference sign r in
       match DAst.get c with
       | GRef (r,None) ->
-          Inl (ArgArg (evaluable_of_global_reference ist.genv r,None))
+          Inl (evalref_of_globref r)
       | GVar id ->
-          let r = evaluable_of_global_reference ist.genv (GlobRef.VarRef id) in
-          Inl (ArgArg (r,None))
+          let r = evalref_of_globref (GlobRef.VarRef id) in
+          Inl r
       | _ ->
           let bound_names = Glob_ops.bound_glob_vars c in
           Inr (bound_names,(c,None),dummy_pat) in

test-suite/bugs/closed/bug_11727.v

@@ -0,0 +1,8 @@
+Tactic Notation "myunfold" reference(x) := unfold x.
+Notation idnat := (@id nat).
+Goal let n := 0 in idnat n = 0.
+Proof.
+  intro n.
+  myunfold idnat.
+  myunfold n.
+Abort.

test-suite/bugs/closed/bug_4925.v

@@ -0,0 +1,6 @@
+Axiom a: bool.
+
+Goal a = true.
+Proof.
+try unfold a.
+Abort.

test-suite/bugs/closed/bug_5159.v

@@ -0,0 +1,12 @@
+Axiom foo : Type.
+Definition bar := 1.
+Definition bar' := Eval cbv -[bar] in bar.
+Declare Reduction red' := cbv -[bar].
+Opaque bar.
+Definition bar'' := Eval red' in bar.
+Declare Reduction red'' := cbv -[bar]. (* Error: Cannot coerce bar to an
+evaluable reference. *)
+Definition bar''' := Eval cbv -[bar] in bar. (* Error: Cannot coerce bar to an
+evaluable reference. *)
+Definition foo' := Eval cbv -[foo] in foo. (* Error: Cannot coerce foo to an
+evaluable reference. *)

test-suite/bugs/closed/bug_5764.v

@@ -0,0 +1,7 @@
+Module Type A.
+Parameter a : nat.
+End A.
+
+Module B (mA : A).
+Ltac cbv_a := cbv [mA.a].
+End B.

test-suite/success/with_strategy.v

@@ -195,8 +195,8 @@ Opaque F.id.
 
 Goal F.id 0 = F.id 0.
   Fail unfold F.id.
-  (* This should work, but it fails with "Cannot coerce F.id to an evaluable reference." *)
-  Fail F.with_transparent_id ltac:(progress unfold F.id).
+  F.with_transparent_id ltac:(progress unfold F.id).
+  Undo.
   F.with_transparent_id ltac:(let x := constr:(@F.id) in progress unfold x).
 Abort.
 
@@ -212,8 +212,8 @@ Opaque F2.id.
 
 Goal F2.id 0 = F2.id 0.
   Fail unfold F2.id.
-  (* This should work, but it fails with "Cannot coerce F2.id to an evaluable reference." *)
-  Fail F2.with_transparent_id ltac:(progress unfold F2.id).
+  F2.with_transparent_id ltac:(progress unfold F2.id).
+  Undo.
   F2.with_transparent_id ltac:(let x := constr:(@F2.id) in progress unfold x).
 Abort.
 

vernac/prettyp.ml

@@ -906,7 +906,7 @@ let print_name env sigma na udecl =
   match na with
   | {loc; v=Constrexpr.ByNotation (ntn,sc)} ->
     print_any_name env sigma
-      (Term (Notation.interp_notation_as_global_reference ?loc (fun _ -> true)
+      (Term (Notation.interp_notation_as_global_reference ?loc ~head:false (fun _ -> true)
                ntn sc))
       udecl
   | {loc; v=Constrexpr.AN ref} ->
@@ -960,7 +960,7 @@ let print_about env sigma na udecl =
   match na with
   | {loc;v=Constrexpr.ByNotation (ntn,sc)} ->
       print_about_any ?loc env sigma
-        (Term (Notation.interp_notation_as_global_reference ?loc (fun _ -> true)
+        (Term (Notation.interp_notation_as_global_reference ?loc ~head:false (fun _ -> true)
                ntn sc)) udecl
   | {loc;v=Constrexpr.AN ref} ->
       print_about_any ?loc env sigma (locate_any_name ref) udecl

vernac/vernacentries.ml

@@ -1785,7 +1785,7 @@ let interp_search_about_item env sigma =
       try
         let ref =
           Notation.interp_notation_as_global_reference
-            (fun _ -> true) s sc in
+            ~head:false (fun _ -> true) s sc in
         GlobSearchSubPattern (Pattern.PRef ref)
       with UserError _ ->
         user_err ~hdr:"interp_search_about_item"