From 3f04bd0a74575d93b2a5c1dfff2bd5a364bfac59 Mon Sep 17 00:00:00 2001
From: Pierre Roux
Date: Thu, 3 Sep 2020 13:10:00 +0200
Subject: Add functions Smartlocate.global_{constant,constructor}

---
 interp/smartlocate.ml  | 38 +++++++++++++++++++++++++++++++++-----
 interp/smartlocate.mli | 12 ++++++++++++
 2 files changed, 45 insertions(+), 5 deletions(-)

(limited to 'interp')

diff --git a/interp/smartlocate.ml b/interp/smartlocate.ml
index 33d8aa6064..46baa00c74 100644
--- a/interp/smartlocate.ml
+++ b/interp/smartlocate.ml
@@ -50,6 +50,16 @@ let locate_global_with_alias ?(head=false) qid =
     user_err ?loc:qid.CAst.loc (pr_qualid qid ++
       str " is bound to a notation that does not denote a reference.")
 
+let global_constant_with_alias qid  =
+  try match locate_global_with_alias qid with
+  | Names.GlobRef.ConstRef c -> c
+  | ref ->
+      user_err ?loc:qid.CAst.loc ~hdr:"global_inductive"
+        (pr_qualid qid ++ spc () ++ str "is not a reference to a constant.")
+  with Not_found as exn ->
+    let _, info = Exninfo.capture exn in
+    Nametab.error_global_not_found ~info qid
+
 let global_inductive_with_alias qid  =
   try match locate_global_with_alias qid with
   | Names.GlobRef.IndRef ind -> ind
@@ -60,6 +70,16 @@ let global_inductive_with_alias qid  =
     let _, info = Exninfo.capture exn in
     Nametab.error_global_not_found ~info qid
 
+let global_constructor_with_alias qid  =
+  try match locate_global_with_alias qid with
+  | Names.GlobRef.ConstructRef c -> c
+  | ref ->
+      user_err ?loc:qid.CAst.loc ~hdr:"global_inductive"
+        (pr_qualid qid ++ spc () ++ str "is not a constructor of an inductive type.")
+  with Not_found as exn ->
+    let _, info = Exninfo.capture exn in
+    Nametab.error_global_not_found ~info qid
+
 let global_with_alias ?head qid =
   try locate_global_with_alias ?head qid
   with Not_found as exn ->
@@ -72,9 +92,17 @@ let smart_global ?(head = false) = let open Constrexpr in CAst.with_loc_val (fun
   | ByNotation (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
+let smart_global_kind f dest is = let open Constrexpr in CAst.with_loc_val (fun ?loc -> function
+  | AN r -> f r
   | ByNotation (ntn,sc) ->
-    destIndRef
-      (Notation.interp_notation_as_global_reference ?loc ~head:false isIndRef ntn sc))
+    dest
+      (Notation.interp_notation_as_global_reference ?loc ~head:false is ntn sc))
+
+let smart_global_constant =
+  smart_global_kind global_constant_with_alias destConstRef isConstRef
+
+let smart_global_inductive =
+  smart_global_kind global_inductive_with_alias destIndRef isIndRef
+
+let smart_global_constructor =
+  smart_global_kind global_constructor_with_alias destConstructRef isConstructRef
diff --git a/interp/smartlocate.mli b/interp/smartlocate.mli
index 9b24a62086..26f2a4f36d 100644
--- a/interp/smartlocate.mli
+++ b/interp/smartlocate.mli
@@ -28,11 +28,23 @@ val global_of_extended_global : extended_global_reference -> GlobRef.t
     a reference. *)
 val global_with_alias : ?head:bool -> qualid -> GlobRef.t
 
+(** The same for constants *)
+val global_constant_with_alias : qualid -> Constant.t
+
 (** The same for inductive types *)
 val global_inductive_with_alias : qualid -> inductive
 
+(** The same for constructors of an inductive type *)
+val global_constructor_with_alias : qualid -> constructor
+
 (** Locate a reference taking into account notations and "aliases" *)
 val smart_global : ?head:bool -> qualid Constrexpr.or_by_notation -> GlobRef.t
 
+(** The same for constants *)
+val smart_global_constant : qualid Constrexpr.or_by_notation -> Constant.t
+
 (** The same for inductive types *)
 val smart_global_inductive : qualid Constrexpr.or_by_notation -> inductive
+
+(** The same for constructors of an inductive type *)
+val smart_global_constructor : qualid Constrexpr.or_by_notation -> constructor
-- 
cgit v1.2.3