Add a type of untyped term to Ltac's value.

It is meant to avoid intermediary retyping when a term is built in Ltac. See #3218.

The implementation makes a small modification in Constrintern: now the main internalisation function can take an extra substitution from Ltac variables to glob_constr and will apply the substitution during the internalisation.

5 files changed, 64 insertions, 5 deletions

diff --git a/tactics/taccoerce.ml b/tactics/taccoerce.ml
index 95c6b6bfbf..2c36398ed8 100644
--- a/tactics/taccoerce.ml
+++ b/tactics/taccoerce.ml
@@ -46,6 +46,14 @@ let to_constr v =
     match vars with [] -> Some c | _ -> None
   else None
 
+let of_uconstr c = in_gen (topwit wit_uconstr) c
+
+let to_uconstr v =
+  let v = normalize v in
+  if has_type v (topwit wit_uconstr) then
+    Some (out_gen (topwit wit_uconstr) v)
+  else None
+
 let of_int i = in_gen (topwit wit_int) i
 
 let to_int v =
@@ -139,6 +147,14 @@ let coerce_to_constr env v =
     (try [], constr_of_id env id with Not_found -> fail ())
   else fail ()
 
+let coerce_to_uconstr env v =
+  let v = Value.normalize v in
+  let fail () = raise (CannotCoerceTo "an untyped term") in
+  if has_type v (topwit wit_uconstr) then
+    out_gen (topwit wit_uconstr) v
+  else
+    fail ()
+
 let coerce_to_closed_constr env v =
   let ids,c = coerce_to_constr env v in
   let () = if not (List.is_empty ids) then raise (CannotCoerceTo "a term") in
diff --git a/tactics/taccoerce.mli b/tactics/taccoerce.mli
index 75f45e7316..b4c0283c92 100644
--- a/tactics/taccoerce.mli
+++ b/tactics/taccoerce.mli
@@ -37,6 +37,8 @@ sig
 
   val of_constr : constr -> t
   val to_constr : t -> constr option
+  val of_uconstr : Glob_term.glob_constr -> t
+  val to_uconstr : t -> Glob_term.glob_constr option
   val of_int : int -> t
   val to_int : t -> int option
   val to_list : t -> t list option
@@ -56,6 +58,8 @@ val coerce_to_int : Value.t -> int
 
 val coerce_to_constr : Environ.env -> Value.t -> constr_under_binders
 
+val coerce_to_uconstr : Environ.env -> Value.t -> Glob_term.glob_constr
+
 val coerce_to_closed_constr : Environ.env -> Value.t -> constr
 
 val coerce_to_evaluable_ref :
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml
index c624a38d1a..44b695e219 100644
--- a/tactics/tacintern.ml
+++ b/tactics/tacintern.ml
@@ -245,7 +245,7 @@ let intern_binding_name ist x =
 let intern_constr_gen allow_patvar isarity {ltacvars=lfun; genv=env} 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 = (lfun, Id.Set.empty) in
+  let ltacvars = (lfun, Id.Set.empty,Id.Map.empty) in
   let c' =
     warn (Constrintern.intern_gen scope ~allow_patvar ~ltacvars env) c
   in
@@ -318,7 +318,7 @@ let intern_flag ist red =
 let intern_constr_with_occurrences ist (l,c) = (l,intern_constr ist c)
 
 let intern_constr_pattern ist ~as_type ~ltacvars pc =
-  let ltacvars = ltacvars, Id.Set.empty in
+  let ltacvars = ltacvars, Id.Set.empty,Id.Map.empty in
   let metas,pat = Constrintern.intern_constr_pattern
     ist.genv ~as_type ~ltacvars pc
   in
@@ -631,7 +631,7 @@ and intern_tactic_as_arg loc onlytac ist a =
   | TacCall _ | TacExternal _ | Reference _
   | TacDynamic _ | TacGeneric _ as a -> TacArg (loc,a)
   | Tacexp a -> a
-  | ConstrMayEval _ | TacFreshId _ as a ->
+  | ConstrMayEval _ | UConstr _ | TacFreshId _ as a ->
       if onlytac then error_tactic_expected loc else TacArg (loc,a)
   | MetaIdArg _ -> assert false
 
@@ -646,6 +646,7 @@ and intern_tactic_fun ist (var,body) =
 and intern_tacarg strict onlytac ist = function
   | Reference r -> intern_non_tactic_reference strict ist r
   | ConstrMayEval c -> ConstrMayEval (intern_constr_may_eval ist c)
+  | UConstr c -> UConstr (intern_constr ist c)
   | MetaIdArg (loc,istac,s) ->
       (* $id can occur in Grammar tactic... *)
       let id = Id.of_string s in
@@ -786,6 +787,9 @@ let () =
   Genintern.register_intern0 wit_tactic (lift intern_tactic_or_tacarg);
   Genintern.register_intern0 wit_sort (fun ist s -> (ist, s))
 
+let () =
+  Genintern.register_intern0 wit_uconstr (fun ist c -> (ist,intern_constr ist c))
+
 (***************************************************************************)
 (* Backwarding recursive needs of tactic glob/interp/eval functions *)
 
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index b83775b93a..cb63d53dd7 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -453,6 +453,29 @@ let interp_fresh_id ist env l =
       Id.of_string s in
   Tactics.fresh_id_in_env avoid id env
 
+
+
+(* Extract the uconstr list from lfun *)
+let extract_ltac_uconstr_values ist env =
+  let fold id v accu =
+    try
+      let c = coerce_to_uconstr env v in
+      Id.Map.add id c accu
+    with CannotCoerceTo _ -> accu
+  in
+  Id.Map.fold fold ist.lfun Id.Map.empty
+
+(** Significantly simpler than [interp_constr], to interpret an
+    untyped constr, it suffices to substitute any bound Ltac variables
+    while redoint internalisation. *)
+let interp_uconstr ist env = function
+  | (c,None) -> c
+  | (_,Some ce) ->
+      let ltacvars = extract_ltac_uconstr_values ist env in
+      let bndvars = Id.Map.domain ist.lfun in
+      let ltacdata = (Id.Set.empty, bndvars , ltacvars) in
+      intern_gen WithoutTypeConstraint ~ltacvars:ltacdata env ce
+
 let interp_gen kind ist allow_patvar flags env sigma (c,ce) =
   let constrvars = extract_ltac_constr_values ist env in
   let vars = (constrvars, ist.lfun) in
@@ -464,7 +487,7 @@ let interp_gen kind ist allow_patvar flags env sigma (c,ce) =
   | Some c ->
       let ltacvars = Id.Map.domain constrvars in
       let bndvars = Id.Map.domain ist.lfun in
-      let ltacdata = (ltacvars, bndvars) in
+      let ltacdata = (ltacvars, bndvars,Id.Map.empty) in
       intern_gen kind ~allow_patvar ~ltacvars:ltacdata env c
   in
   let trace =
@@ -1090,6 +1113,11 @@ and interp_tacarg ist arg : typed_generic_argument GTac.t =
         Proofview.V82.tclEVARS sigma <*>
         GTac.return (Value.of_constr c_interp)
       end
+  | UConstr c ->
+      GTac.raw_enter begin fun gl ->
+        let env = Proofview.Goal.env gl in
+        GTac.return (Value.of_uconstr (interp_uconstr ist env c))
+      end
   | MetaIdArg (loc,_,id) -> assert false
   | TacCall (loc,r,[]) ->
       interp_ltac_reference loc true ist r
@@ -2024,6 +2052,11 @@ let () =
   in
   Geninterp.register_interp0 wit_tactic interp
 
+let () =
+  Geninterp.register_interp0 wit_uconstr (fun ist gl c ->
+     project gl , interp_uconstr ist (pf_env gl) c
+  )
+
 (***************************************************************************)
 (* Other entry points *)
 
diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml
index 0d8923d5ba..0872f8bbf6 100644
--- a/tactics/tacsubst.ml
+++ b/tactics/tacsubst.ml
@@ -254,6 +254,7 @@ and subst_tactic_fun subst (var,body) = (var,subst_tactic subst body)
 and subst_tacarg subst = function
   | Reference r -> Reference (subst_reference subst r)
   | ConstrMayEval c -> ConstrMayEval (subst_raw_may_eval subst c)
+  | UConstr c -> UConstr (subst_glob_constr subst c)
   | MetaIdArg (_loc,_,_) -> assert false
   | TacCall (_loc,f,l) ->
       TacCall (_loc, subst_reference subst f, List.map (subst_tacarg subst) l)
@@ -320,6 +321,7 @@ let () =
   Genintern.register_subst0 wit_intro_pattern (fun _ v -> v);
   Genintern.register_subst0 wit_tactic subst_tactic;
   Genintern.register_subst0 wit_sort (fun _ v -> v);
-  Genintern.register_subst0 wit_clause_dft_concl (fun _ v -> v)
+  Genintern.register_subst0 wit_clause_dft_concl (fun _ v -> v);
+  Genintern.register_subst0 wit_uconstr (fun subst c -> subst_glob_constr subst c)
 
 let _ = Hook.set Auto.extern_subst_tactic subst_tactic