Introducing a quotation for global references.

8 files changed, 67 insertions, 17 deletions

diff --git a/src/g_ltac2.ml4 b/src/g_ltac2.ml4
index e5847119e1..c70f1e882d 100644
--- a/src/g_ltac2.ml4
+++ b/src/g_ltac2.ml4
@@ -65,6 +65,7 @@ let tac2mode = Gram.entry_create "vernac:ltac2_command"
 let inj_wit wit loc x = CTacExt (loc, Genarg.in_gen (Genarg.rawwit wit) x)
 let inj_open_constr loc c = inj_wit Stdarg.wit_open_constr loc c
 let inj_pattern loc c = inj_wit Tac2env.wit_pattern loc c
+let inj_reference loc c = inj_wit Tac2env.wit_reference loc c
 
 let pattern_of_qualid loc id =
   if Tac2env.is_constructor (snd id) then CPatRef (loc, RelId id, [])
@@ -157,6 +158,7 @@ GEXTEND Gram
       | IDENT "open_constr"; ":"; "("; c = Constr.lconstr; ")" -> Tac2quote.of_open_constr c
       | IDENT "ident"; ":"; "("; c = lident; ")" -> Tac2quote.of_ident c
       | IDENT "pattern"; ":"; "("; c = Constr.lconstr_pattern; ")" -> inj_pattern !@loc c
+      | IDENT "reference"; ":"; "("; c = globref; ")" -> inj_reference !@loc c
     ] ]
   ;
   let_clause:
@@ -300,6 +302,11 @@ GEXTEND Gram
   lident:
     [ [ id = Prim.ident -> Loc.tag ~loc:!@loc id ] ]
   ;
+  globref:
+    [ [ "&"; id = Prim.ident -> Libnames.Ident (Loc.tag ~loc:!@loc id)
+      | qid = Prim.qualid -> Libnames.Qualid qid
+    ] ]
+  ;
 END
 
 (** Quotation scopes used by notations *)
diff --git a/src/tac2core.ml b/src/tac2core.ml
index bec1761120..303d62a30d 100644
--- a/src/tac2core.ml
+++ b/src/tac2core.ml
@@ -689,7 +689,7 @@ let interp_constr flags ist (c, _) =
   Proofview.V82.wrap_exceptions begin fun () ->
     let ist = to_lvar ist in
     let (sigma, c) = understand_ltac flags env sigma ist WithoutTypeConstraint c in
-    let c = Val.Dyn (Value.val_constr, c) in
+    let c = ValExt (Val.Dyn (Value.val_constr, c)) in
     Proofview.Unsafe.tclEVARS sigma >>= fun () ->
     Proofview.tclUNIT c
   end
@@ -712,7 +712,7 @@ let () =
   define_ml_object Stdarg.wit_open_constr obj
 
 let () =
-  let interp _ id = return (Val.Dyn (Value.val_ident, id)) in
+  let interp _ id = return (ValExt (Val.Dyn (Value.val_ident, id))) in
   let obj = {
     ml_type = t_ident;
     ml_interp = interp;
@@ -720,7 +720,7 @@ let () =
   define_ml_object Stdarg.wit_ident obj
 
 let () =
-  let interp _ c = return (Val.Dyn (Value.val_pattern, c)) in
+  let interp _ c = return (ValExt (Val.Dyn (Value.val_pattern, c))) in
   let obj = {
     ml_type = t_pattern;
     ml_interp = interp;
@@ -728,6 +728,14 @@ let () =
   define_ml_object Tac2env.wit_pattern obj
 
 let () =
+  let interp _ gr = return (Value.of_reference gr) in
+  let obj = {
+    ml_type = t_pattern;
+    ml_interp = interp;
+  } in
+  define_ml_object Tac2env.wit_reference obj
+
+let () =
   let interp ist env sigma concl tac =
     let fold id (Val.Dyn (tag, v)) (accu : environment) : environment =
       match Val.eq tag val_valexpr with
@@ -754,6 +762,25 @@ let () =
   let subst s c = Patternops.subst_pattern s c in
   Genintern.register_subst0 wit_pattern subst
 
+(** References *)
+
+let () =
+  let intern ist qid = match qid with
+  | Libnames.Ident (_, id) -> ist, Globnames.VarRef id
+  | Libnames.Qualid (loc, qid) ->
+    let gr =
+      try Nametab.locate qid
+      with Not_found ->
+        Nametab.error_global_not_found ?loc qid
+    in
+    ist, gr
+  in
+  Genintern.register_intern0 wit_reference intern
+
+let () =
+  let subst s c = Globnames.subst_global_reference s c in
+  Genintern.register_subst0 wit_reference subst
+
 (** Built-in notation scopes *)
 
 let add_scope s f =
diff --git a/src/tac2env.ml b/src/tac2env.ml
index ac2bd5fc23..65276ec57f 100644
--- a/src/tac2env.ml
+++ b/src/tac2env.ml
@@ -246,7 +246,7 @@ let shortest_qualid_of_projection kn =
 
 type 'a ml_object = {
   ml_type : type_constant;
-  ml_interp : environment -> 'a -> Geninterp.Val.t Proofview.tactic;
+  ml_interp : environment -> 'a -> valexpr Proofview.tactic;
 }
 
 module MLTypeObj =
@@ -271,8 +271,9 @@ let std_prefix =
 
 (** Generic arguments *)
 
-let wit_ltac2 = Genarg.make0 "ltac2"
+let wit_ltac2 = Genarg.make0 "ltac2:value"
 let wit_pattern = Genarg.make0 "ltac2:pattern"
+let wit_reference = Genarg.make0 "ltac2:reference"
 
 let is_constructor qid =
   let (_, id) = repr_qualid qid in
diff --git a/src/tac2env.mli b/src/tac2env.mli
index e4cc8387c5..20bf24d19d 100644
--- a/src/tac2env.mli
+++ b/src/tac2env.mli
@@ -100,7 +100,7 @@ val interp_primitive : ml_tactic_name -> ml_tactic
 
 type 'a ml_object = {
   ml_type : type_constant;
-  ml_interp : environment -> 'a -> Geninterp.Val.t Proofview.tactic;
+  ml_interp : environment -> 'a -> valexpr Proofview.tactic;
 }
 
 val define_ml_object : ('a, 'b, 'c) genarg_type -> 'b ml_object -> unit
@@ -118,7 +118,12 @@ val std_prefix : ModPath.t
 
 val wit_ltac2 : (raw_tacexpr, glb_tacexpr, Util.Empty.t) genarg_type
 
-val wit_pattern : (Constrexpr.constr_expr, Pattern.constr_pattern, Pattern.constr_pattern) genarg_type
+val wit_pattern : (Constrexpr.constr_expr, Pattern.constr_pattern, Util.Empty.t) genarg_type
+
+val wit_reference : (reference, Globnames.global_reference, Util.Empty.t) genarg_type
+(** Beware, at the raw level, [Qualid [id]] has not the same meaning as
+    [Ident id]. The first is an unqualified global reference, the second is
+    the dynamic reference to id. *)
 
 (** {5 Helper functions} *)
 
diff --git a/src/tac2ffi.ml b/src/tac2ffi.ml
index 49b49d92fd..b506a578b1 100644
--- a/src/tac2ffi.ml
+++ b/src/tac2ffi.ml
@@ -7,6 +7,7 @@
 (************************************************************************)
 
 open Util
+open Globnames
 open Genarg
 open Geninterp
 open Tac2expr
@@ -125,3 +126,16 @@ let to_array f = function
 
 let of_constant c = of_ext val_constant c
 let to_constant c = to_ext val_constant c
+
+let of_reference = function
+| VarRef id -> ValBlk (0, [| of_ident id |])
+| ConstRef cst -> ValBlk (1, [| of_constant cst |])
+| IndRef ind -> ValBlk (2, [| of_ext val_inductive ind |])
+| ConstructRef cstr -> ValBlk (3, [| of_ext val_constructor cstr |])
+
+let to_reference = function
+| ValBlk (0, [| id |]) -> VarRef (to_ident id)
+| ValBlk (1, [| cst |]) -> ConstRef (to_constant cst)
+| ValBlk (2, [| ind |]) -> IndRef (to_ext val_inductive ind)
+| ValBlk (3, [| cstr |]) -> ConstructRef (to_ext val_constructor cstr)
+| _ -> assert false
diff --git a/src/tac2ffi.mli b/src/tac2ffi.mli
index b69ca9a382..71d90ba940 100644
--- a/src/tac2ffi.mli
+++ b/src/tac2ffi.mli
@@ -62,6 +62,9 @@ val to_pp : valexpr -> Pp.t
 val of_constant : Constant.t -> valexpr
 val to_constant : valexpr -> Constant.t
 
+val of_reference : Globnames.global_reference -> valexpr
+val to_reference : valexpr -> Globnames.global_reference
+
 val of_ext : 'a Val.typ -> 'a -> valexpr
 val to_ext : 'a Val.typ -> valexpr -> 'a
 
diff --git a/src/tac2interp.ml b/src/tac2interp.ml
index 664b7de3d6..d3bc79957b 100644
--- a/src/tac2interp.ml
+++ b/src/tac2interp.ml
@@ -105,7 +105,7 @@ let rec interp ist = function
 | GTacExt e ->
   let GenArg (Glbwit tag, e) = e in
   let tpe = Tac2env.interp_ml_object tag in
-  tpe.Tac2env.ml_interp ist e >>= fun e -> return (ValExt e)
+  tpe.Tac2env.ml_interp ist e
 
 and interp_app f args = match f with
 | ValCls { clos_env = ist; clos_var = ids; clos_exp = e } ->
diff --git a/src/tac2stdlib.ml b/src/tac2stdlib.ml
index d3430213b4..eccaf95ab3 100644
--- a/src/tac2stdlib.ml
+++ b/src/tac2stdlib.ml
@@ -71,13 +71,6 @@ let to_clause = function
   { onhyps = hyps; concl_occs = to_occurrences to_int_or_var concl; }
 | _ -> assert false
 
-let to_reference = function
-| ValBlk (0, [| id |]) -> VarRef (Value.to_ident id)
-| ValBlk (1, [| cst |]) -> ConstRef (Value.to_constant cst)
-| ValBlk (2, [| ind |]) -> IndRef (Value.to_ext Value.val_inductive ind)
-| ValBlk (3, [| cstr |]) -> ConstructRef (Value.to_ext Value.val_constructor cstr)
-| _ -> assert false
-
 let to_red_flag = function
 | ValBlk (0, [| beta; iota; fix; cofix; zeta; delta; const |]) ->
   {
@@ -87,7 +80,7 @@ let to_red_flag = function
     rCofix = Value.to_bool cofix;
     rZeta = Value.to_bool zeta;
     rDelta = Value.to_bool delta;
-    rConst = Value.to_list to_reference const;
+    rConst = Value.to_list Value.to_reference const;
   }
 | _ -> assert false
 
@@ -329,7 +322,7 @@ let () = define_prim2 "tac_lazy" begin fun flags cl ->
 end
 
 let () = define_prim2 "tac_unfold" begin fun refs cl ->
-  let map v = to_pair to_reference (fun occ -> to_occurrences to_int_or_var occ) v in
+  let map v = to_pair Value.to_reference (fun occ -> to_occurrences to_int_or_var occ) v in
   let refs = Value.to_list map refs in
   let cl = to_clause cl in
   Tac2tactics.unfold refs cl