Merge PR#608: Allow Ltac2 as a plugin

16 files changed, 132 insertions, 43 deletions

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 3b3dccc99..c7078cf2a 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -69,6 +69,7 @@ type internalization_env =
 type ltac_sign = {
   ltac_vars : Id.Set.t;
   ltac_bound : Id.Set.t;
+  ltac_extra : Genintern.Store.t;
 }
 
 let interning_grammar = ref false
@@ -1733,12 +1734,14 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
         | Some gen ->
           let (ltacvars, ntnvars) = lvar in
           let ntnvars = Id.Map.domain ntnvars in
+          let extra = ltacvars.ltac_extra in
           let lvars = Id.Set.union ltacvars.ltac_bound ltacvars.ltac_vars in
           let lvars = Id.Set.union lvars ntnvars in
-          let lvars = Id.Set.union lvars env.ids in
+          let ltacvars = Id.Set.union lvars env.ids in
           let ist = {
-            Genintern.ltacvars = lvars;
-            genv = globalenv;
+            Genintern.genv = globalenv;
+            ltacvars;
+            extra;
           } in
           let (_, glb) = Genintern.generic_intern ist gen in
           Some glb
@@ -1937,6 +1940,7 @@ let scope_of_type_kind = function
 let empty_ltac_sign = {
   ltac_vars = Id.Set.empty;
   ltac_bound = Id.Set.empty;
+  ltac_extra = Genintern.Store.empty;
 }
 
 let intern_gen kind env
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index fdd50c6a1..644cafe57 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -70,6 +70,8 @@ type ltac_sign = {
   (** Variables of Ltac which may be bound to a term *)
   ltac_bound : Id.Set.t;
   (** Other variables of Ltac *)
+  ltac_extra : Genintern.Store.t;
+  (** Arbitrary payload *)
 }
 
 val empty_ltac_sign : ltac_sign
diff --git a/interp/genintern.ml b/interp/genintern.ml
index be7abfa99..e443824bd 100644
--- a/interp/genintern.ml
+++ b/interp/genintern.ml
@@ -10,9 +10,19 @@ open Names
 open Mod_subst
 open Genarg
 
+module Store = Store.Make(struct end)
+
 type glob_sign = {
   ltacvars : Id.Set.t;
-  genv : Environ.env }
+  genv : Environ.env;
+  extra : Store.t;
+}
+
+let empty_glob_sign env = {
+  ltacvars = Id.Set.empty;
+  genv = env;
+  extra = Store.empty;
+}
 
 type ('raw, 'glb) intern_fun = glob_sign -> 'raw -> glob_sign * 'glb
 type 'glb subst_fun = substitution -> 'glb -> 'glb
diff --git a/interp/genintern.mli b/interp/genintern.mli
index 4b0354be3..658caa08c 100644
--- a/interp/genintern.mli
+++ b/interp/genintern.mli
@@ -10,9 +10,15 @@ open Names
 open Mod_subst
 open Genarg
 
+module Store : Store.S
+
 type glob_sign = {
   ltacvars : Id.Set.t;
-  genv : Environ.env }
+  genv : Environ.env;
+  extra : Store.t;
+}
+
+val empty_glob_sign : Environ.env -> glob_sign
 
 (** {5 Internalization functions} *)
 
diff --git a/library/nametab.mli b/library/nametab.mli
index d20c399b6..095ac4f9d 100644
--- a/library/nametab.mli
+++ b/library/nametab.mli
@@ -173,3 +173,38 @@ val shortest_qualid_of_tactic : ltac_constant -> qualid
 
 val extended_locate : qualid -> extended_global_reference (*= locate_extended *)
 val absolute_reference : full_path -> global_reference (** = global_of_path *)
+
+(** {5 Generic name handling} *)
+
+(** NOT FOR PUBLIC USE YET. Plugin writers, please do not rely on this API. *)
+
+module type UserName = sig
+  type t
+  val equal : t -> t -> bool
+  val to_string : t -> string
+  val repr : t -> Id.t * module_ident list
+end
+
+module type EqualityType =
+sig
+  type t
+  val equal : t -> t -> bool
+end
+
+module type NAMETREE = sig
+  type elt
+  type t
+  type user_name
+
+  val empty : t
+  val push : visibility -> user_name -> elt -> t -> t
+  val locate : qualid -> t -> elt
+  val find : user_name -> t -> elt
+  val exists : user_name -> t -> bool
+  val user_name : qualid -> t -> user_name
+  val shortest_qualid : Id.Set.t -> user_name -> t -> qualid
+  val find_prefixes : qualid -> t -> elt list
+end
+
+module Make (U : UserName) (E : EqualityType) :
+  NAMETREE with type user_name = U.t and type elt = E.t
diff --git a/plugins/ltac/g_obligations.ml4 b/plugins/ltac/g_obligations.ml4
index 7d4075836..4dceb0331 100644
--- a/plugins/ltac/g_obligations.ml4
+++ b/plugins/ltac/g_obligations.ml4
@@ -31,7 +31,7 @@ let () =
   Obligations.default_tactic := tac
 
 let with_tac f tac =
-  let env = { Genintern.genv = Global.env (); ltacvars = Names.Id.Set.empty } in
+  let env = Genintern.empty_glob_sign (Global.env ()) in
   let tac = match tac with
   | None -> None
   | Some tac ->
diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml
index da7f11472..6c7eb8c89 100644
--- a/plugins/ltac/tacintern.ml
+++ b/plugins/ltac/tacintern.ml
@@ -39,13 +39,12 @@ let error_tactic_expected ?loc =
 type glob_sign = Genintern.glob_sign = {
   ltacvars : Id.Set.t;
      (* ltac variables and the subset of vars introduced by Intro/Let/... *)
-  genv : Environ.env }
+  genv : Environ.env;
+  extra : Genintern.Store.t;
+}
 
-let fully_empty_glob_sign =
-  { ltacvars = Id.Set.empty; genv = Environ.empty_env }
-
-let make_empty_glob_sign () =
-  { fully_empty_glob_sign with genv = Global.env () }
+let fully_empty_glob_sign = Genintern.empty_glob_sign Environ.empty_env
+let make_empty_glob_sign () = Genintern.empty_glob_sign (Global.env ())
 
 (* We have identifier <| global_reference <| constr *)
 
@@ -190,12 +189,13 @@ let intern_binding_name ist x =
      and if a term w/o ltac vars, check the name is indeed quantified *)
   x
 
-let intern_constr_gen allow_patvar isarity {ltacvars=lfun; genv=env} c =
+let intern_constr_gen allow_patvar isarity {ltacvars=lfun; genv=env; extra} c =
   let warn = if !strict_check then fun x -> x else Constrintern.for_grammar in
   let scope = if isarity then Pretyping.IsType else Pretyping.WithoutTypeConstraint in
   let ltacvars = {
     Constrintern.ltac_vars = lfun;
     ltac_bound = Id.Set.empty;
+    ltac_extra = extra;
   } in
   let c' =
     warn (Constrintern.intern_gen scope ~allow_patvar ~ltacvars env) c
@@ -311,6 +311,7 @@ let intern_constr_pattern ist ~as_type ~ltacvars pc =
   let ltacvars = {
     Constrintern.ltac_vars = ltacvars;
     ltac_bound = Id.Set.empty;
+    ltac_extra = ist.extra;
   } in
   let metas,pat = Constrintern.intern_constr_pattern
     ist.genv ~as_type ~ltacvars pc
@@ -342,7 +343,11 @@ let intern_typed_pattern_or_ref_with_occurrences ist (l,p) =
       let r = match r with
       | AN r -> r
       | _ -> Qualid (loc,qualid_of_path (path_of_global (smart_global r))) in
-      let sign = { Constrintern.ltac_vars = ist.ltacvars; Constrintern.ltac_bound = Id.Set.empty } in
+      let sign = {
+        Constrintern.ltac_vars = ist.ltacvars;
+        ltac_bound = Id.Set.empty;
+        ltac_extra = ist.extra;
+      } in
       let c = Constrintern.interp_reference sign r in
       match c.CAst.v with
       | GRef (r,None) ->
@@ -706,8 +711,7 @@ let glob_tactic_env l env x =
   let ltacvars =
     List.fold_left (fun accu x -> Id.Set.add x accu) Id.Set.empty l in
   Flags.with_option strict_check
-  (intern_pure_tactic
-    { ltacvars; genv = env })
+  (intern_pure_tactic { (Genintern.empty_glob_sign env) with ltacvars })
     x
 
 let split_ltac_fun = function
diff --git a/plugins/ltac/tacintern.mli b/plugins/ltac/tacintern.mli
index 71ca354fa..8ad52ca02 100644
--- a/plugins/ltac/tacintern.mli
+++ b/plugins/ltac/tacintern.mli
@@ -18,7 +18,9 @@ open Misctypes
 
 type glob_sign = Genintern.glob_sign = {
   ltacvars : Id.Set.t;
-  genv : Environ.env }
+  genv : Environ.env;
+  extra : Genintern.Store.t;
+}
 
 val fully_empty_glob_sign : glob_sign
 
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 8a10a4d76..8ed65c5d9 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -585,6 +585,7 @@ let interp_uconstr ist env sigma = function
       let ltacvars = {
         Constrintern.ltac_vars = Id.(Set.union (Map.domain typed) (Map.domain untyped));
         ltac_bound = Id.Map.domain ist.lfun;
+        ltac_extra = Genintern.Store.empty;
       } in
       { closure ; term =  intern_gen WithoutTypeConstraint ~ltacvars env ce }
 
@@ -612,6 +613,7 @@ let interp_gen kind ist allow_patvar flags env sigma (c,ce) =
       let ltacvars = {
         ltac_vars = constr_context;
         ltac_bound = Id.Map.domain ist.lfun;
+        ltac_extra = Genintern.Store.empty;
       } in
       let kind_for_intern =
         match kind with OfType _ -> WithoutTypeConstraint | _ -> kind in
@@ -1964,8 +1966,7 @@ let interp_tac_gen lfun avoid_ids debug t =
   let ist = { lfun = lfun; extra = extra } in
   let ltacvars = Id.Map.domain lfun in
   interp_tactic ist
-    (intern_pure_tactic {
-      ltacvars; genv = env } t)
+    (intern_pure_tactic { (Genintern.empty_glob_sign env) with ltacvars } t)
   end }
 
 let interp t = interp_tac_gen Id.Map.empty [] (get_debug()) t
@@ -1974,7 +1975,7 @@ let interp t = interp_tac_gen Id.Map.empty [] (get_debug()) t
 (* [global] means that [t] should be internalized outside of goals. *)
 let hide_interp global t ot =
   let hide_interp env =
-    let ist = { ltacvars = Id.Set.empty; genv = env } in
+    let ist = Genintern.empty_glob_sign env in
     let te = intern_pure_tactic ist t in
     let t = eval_tactic te in
     match ot with
@@ -2097,17 +2098,13 @@ let interp_redexp env sigma r =
 (* Backwarding recursive needs of tactic glob/interp/eval functions *)
 
 let _ =
-  let eval ty env sigma lfun arg =
+  let eval lfun env sigma ty tac =
     let ist = { lfun = lfun; extra = TacStore.empty; } in
-    if Genarg.has_type arg (glbwit wit_tactic) then
-      let tac = Genarg.out_gen (glbwit wit_tactic) arg in
-      let tac = interp_tactic ist tac in
-      let (c, sigma) = Pfedit.refine_by_tactic env sigma ty tac in
-      (EConstr.of_constr c, sigma)
-    else
-      failwith "not a tactic"
+    let tac = interp_tactic ist tac in
+    let (c, sigma) = Pfedit.refine_by_tactic env sigma ty tac in
+    (EConstr.of_constr c, sigma)
   in
-  Hook.set Pretyping.genarg_interp_hook eval
+  Pretyping.register_constr_interp0 wit_tactic eval
 
 (** Used in tactic extension **)
 
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 75fda97b8..e72394fa2 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -564,7 +564,17 @@ let new_type_evar env evdref loc =
   evdref := Sigma.to_evar_map sigma;
   e
 
-let (f_genarg_interp, genarg_interp_hook) = Hook.make ()
+module ConstrInterpObj =
+struct
+  type ('r, 'g, 't) obj =
+    unbound_ltac_var_map -> env -> evar_map -> types -> 'g -> constr * evar_map
+  let name = "constr_interp"
+  let default _ = None
+end
+
+module ConstrInterp = Genarg.Register(ConstrInterpObj)
+
+let register_constr_interp0 = ConstrInterp.register0
 
 (* [pretype tycon env evdref lvar lmeta cstr] attempts to type [cstr] *)
 (* in environment [env], with existential variables [evdref] and *)
@@ -625,8 +635,11 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
         | Some ty -> ty
         | None ->
           new_type_evar env evdref loc in
+      let open Genarg in
       let ist = lvar.ltac_genargs in
-      let (c, sigma) = Hook.get f_genarg_interp ty env.ExtraEnv.env !evdref ist arg in
+      let GenArg (Glbwit tag, arg) = arg in
+      let interp = ConstrInterp.obj tag in
+      let (c, sigma) = interp ist env.ExtraEnv.env !evdref ty arg in
       let () = evdref := sigma in
       { uj_val = c; uj_type = ty }
 
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index 79fafcf1a..dcacd0720 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -163,6 +163,6 @@ val ise_pretype_gen :
 val interp_sort : ?loc:Loc.t -> evar_map -> glob_sort -> evar_map * sorts
 val interp_elimination_sort : glob_sort -> sorts_family
 
-val genarg_interp_hook :
-  (types -> env -> evar_map -> unbound_ltac_var_map ->
-    Genarg.glob_generic_argument -> constr * evar_map) Hook.t
+val register_constr_interp0 :
+  ('r, 'g, 't) Genarg.genarg_type ->
+    (unbound_ltac_var_map -> env -> evar_map -> types -> 'g -> constr * evar_map) -> unit
diff --git a/proofs/refine.ml b/proofs/refine.ml
index d423a658a..63ae41075 100644
--- a/proofs/refine.ml
+++ b/proofs/refine.ml
@@ -70,8 +70,7 @@ let add_side_effect env = function
 let add_side_effects env effects =
   List.fold_left (fun env eff -> add_side_effect env eff) env effects
 
-let make_refine_enter ?(unsafe = true) f =
-  { enter = fun gl ->
+let generic_refine ?(unsafe = true) f gl =
   let gl = Proofview.Goal.assume gl in
   let sigma = Proofview.Goal.sigma gl in
   let sigma = Sigma.to_evar_map sigma in
@@ -82,7 +81,10 @@ let make_refine_enter ?(unsafe = true) f =
   let prev_future_goals = Evd.future_goals sigma in
   let prev_principal_goal = Evd.principal_future_goal sigma in
   (** Create the refinement term *)
-  let ((v,c), sigma) = Sigma.run (Evd.reset_future_goals sigma) f in
+  Proofview.Unsafe.tclEVARS (Evd.reset_future_goals sigma) >>= fun () ->
+  f >>= fun (v, c) ->
+  Proofview.tclEVARMAP >>= fun sigma ->
+  Proofview.V82.wrap_exceptions begin fun () ->
   let evs = Evd.future_goals sigma in
   let evkmain = Evd.principal_future_goal sigma in
   (** Redo the effects in sigma in the monad's env *)
@@ -122,7 +124,18 @@ let make_refine_enter ?(unsafe = true) f =
   Proofview.Unsafe.tclEVARS sigma <*>
   Proofview.Unsafe.tclSETGOALS comb <*>
   Proofview.tclUNIT v
-  }
+  end
+
+let lift c =
+  Proofview.tclEVARMAP >>= fun sigma ->
+  Proofview.V82.wrap_exceptions begin fun () ->
+  let Sigma (c, sigma, _) = c.run (Sigma.Unsafe.of_evar_map sigma) in
+  Proofview.Unsafe.tclEVARS (Sigma.to_evar_map sigma) >>= fun () ->
+  Proofview.tclUNIT c
+  end
+
+let make_refine_enter ?unsafe f =
+  { enter = fun gl -> generic_refine ?unsafe (lift f) gl }
 
 let refine_one ?(unsafe = true) f =
   Proofview.Goal.enter_one (make_refine_enter ~unsafe f)
diff --git a/proofs/refine.mli b/proofs/refine.mli
index 1a254d578..5098f246a 100644
--- a/proofs/refine.mli
+++ b/proofs/refine.mli
@@ -31,7 +31,11 @@ val refine : ?unsafe:bool -> EConstr.t Sigma.run -> unit tactic
     type-checked beforehand. *)
 
 val refine_one : ?unsafe:bool -> ('a * EConstr.t) Sigma.run -> 'a tactic
-(** A generalization of [refine] which assumes exactly one goal under focus *)
+(** A variant of [refine] which assumes exactly one goal under focus *)
+
+val generic_refine : ?unsafe:bool -> ('a * EConstr.t) tactic ->
+  ([ `NF ], 'r) Proofview.Goal.t -> 'a tactic
+(** The general version of refine. *)
 
 (** {7 Helper functions} *)
 
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index 68f72d7ae..de544fe5f 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -271,7 +271,7 @@ let add_rew_rules base lrul =
   let counter = ref 0 in
   let env = Global.env () in
   let sigma = Evd.from_env env in
-  let ist = { Genintern.ltacvars = Id.Set.empty; genv = Global.env () } in
+  let ist = Genintern.empty_glob_sign (Global.env ()) in
   let intern tac = snd (Genintern.generic_intern ist tac) in
   let lrul =
     List.fold_left
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 0c796b886..e6edae7ef 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -1316,7 +1316,7 @@ let interp_hints poly =
       let pat =	Option.map fp patcom in
       let l = match pat with None -> [] | Some (l, _) -> l in
       let ltacvars = List.fold_left (fun accu x -> Id.Set.add x accu) Id.Set.empty l in
-      let env = Genintern.({ genv = env; ltacvars }) in
+      let env = Genintern.({ (empty_glob_sign env) with ltacvars }) in
       let _, tacexp = Genintern.generic_intern env tacexp in
       HintsExternEntry ({ hint_priority = Some pri; hint_pattern = pat }, tacexp)
 
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index f75e04383..a08c79c40 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -843,8 +843,7 @@ let focus_command_cond = Proof.no_cond command_focus
 let vernac_solve_existential = instantiate_nth_evar_com
 
 let vernac_set_end_tac tac =
-  let open Genintern in
-  let env = { genv = Global.env (); ltacvars = Id.Set.empty } in
+  let env = Genintern.empty_glob_sign (Global.env ()) in
   let _, tac = Genintern.generic_intern env tac in
   if not (refining ()) then
     error "Unknown command of the non proof-editing mode.";