wit_tactic top type is tacvalue

plugins/firstorder/g_ground.mlg

@@ -61,7 +61,7 @@ let gen_ground_tac ist taco ids bases =
   Proofview.Goal.enter begin fun gl ->
       let solver=
         match taco with
-        | Some tac -> tactic_of_value ist tac
+        | Some tac -> tactic_of_tacvalue ist tac
         | None-> default_solver ()
       in
       let startseq k =

plugins/ltac/extraargs.mlg

@@ -266,11 +266,15 @@ let pr_by_arg_tac env sigma _prc _prlc prtac opt_c =
     | None -> mt ()
     | Some t -> hov 2 (str "by" ++ spc () ++ prtac env sigma (Constrexpr.LevelLe 3) t)
 
+let top_pr_by_arg_tac env sigma prc prlc _prtac opt_c =
+  pr_by_arg_tac env sigma prc prlc (fun env _ _ t -> Pptactic.pr_tacvalue env t) opt_c
 }
 
 ARGUMENT EXTEND by_arg_tac
   TYPED AS tactic option
-  PRINTED BY { pr_by_arg_tac env sigma }
+  PRINTED BY { top_pr_by_arg_tac env sigma }
+  RAW_PRINTED BY { pr_by_arg_tac env sigma }
+  GLOB_PRINTED BY { pr_by_arg_tac env sigma }
 | [ "by" tactic3(c) ] -> { Some c }
 | [ ] -> { None }
 END

plugins/ltac/extraargs.mli

@@ -57,7 +57,7 @@ val by_arg_tac : Tacexpr.raw_tactic_expr option Procq.Entry.t
 val wit_by_arg_tac :
   (raw_tactic_expr option,
   glob_tactic_expr option,
-  Geninterp.Val.t option) Genarg.genarg_type
+  Tacarg.tacvalue option) Genarg.genarg_type
 
 val pr_by_arg_tac :
   Environ.env -> Evd.evar_map ->

plugins/ltac/extratactics.mlg

@@ -31,7 +31,7 @@ DECLARE PLUGIN "rocq-runtime.plugins.ltac"
 
 TACTIC EXTEND assert_succeeds
 | [ "assert_succeeds" tactic3(tac) ]
-  -> { Internals.assert_succeeds (Tacinterp.tactic_of_value ist tac) }
+  -> { Internals.assert_succeeds (Tacinterp.tactic_of_tacvalue ist tac) }
 END
 
 TACTIC EXTEND replace
@@ -179,24 +179,24 @@ TACTIC EXTEND autorewrite
     { auto_multi_rewrite  l ( cl) }
 | [ "autorewrite" "with" ne_preident_list(l) clause(cl) "using" tactic(t) ] ->
     {
-      auto_multi_rewrite_with (Tacinterp.tactic_of_value ist t) l cl
+      auto_multi_rewrite_with (Tacinterp.tactic_of_tacvalue ist t) l cl
    }
 END
 
 TACTIC EXTEND autorewrite_star
 | [ "autorewrite" "*" "with" ne_preident_list(l) clause(cl) ] ->
     { auto_multi_rewrite ~conds:AllMatches l cl }
 | [ "autorewrite" "*" "with" ne_preident_list(l) clause(cl) "using" tactic(t) ] ->
-  { auto_multi_rewrite_with ~conds:AllMatches (Tacinterp.tactic_of_value ist t) l cl }
+  { auto_multi_rewrite_with ~conds:AllMatches (Tacinterp.tactic_of_tacvalue ist t) l cl }
 END
 
 (**********************************************************************)
 (* Rewrite star                                                       *)
 
 {
 
-let rewrite_star ist clause orient occs c (tac : Geninterp.Val.t option) =
-  let tac' = Option.map (fun t -> Tacinterp.tactic_of_value ist t, FirstSolved) tac in
+let rewrite_star ist clause orient occs c (tac : Tacarg.tacvalue option) =
+  let tac' = Option.map (fun t -> Tacinterp.tactic_of_tacvalue ist t, FirstSolved) tac in
   Internals.with_delayed_uconstr ist c
     (fun c -> general_rewrite ~where:clause ~l2r:orient occs ?tac:tac' ~freeze:true ~dep:true ~with_evars:true (c,NoBindings))
 
@@ -420,12 +420,12 @@ let add_transitivity_lemma left lem =
 (* Vernacular syntax *)
 
 TACTIC EXTEND stepl
-| ["stepl" constr(c) "by" tactic(tac) ] -> { step true c (Tacinterp.tactic_of_value ist tac) }
+| ["stepl" constr(c) "by" tactic(tac) ] -> { step true c (Tacinterp.tactic_of_tacvalue ist tac) }
 | ["stepl" constr(c) ] -> { step true c (Proofview.tclUNIT ()) }
 END
 
 TACTIC EXTEND stepr
-| ["stepr" constr(c) "by" tactic(tac) ] -> { step false c (Tacinterp.tactic_of_value ist tac) }
+| ["stepr" constr(c) "by" tactic(tac) ] -> { step false c (Tacinterp.tactic_of_tacvalue ist tac) }
 | ["stepr" constr(c) ] -> { step false c (Proofview.tclUNIT ()) }
 END
 
@@ -472,9 +472,9 @@ END
 
 TACTIC EXTEND transparent_abstract
 | [ "transparent_abstract" tactic3(t) ] -> { Proofview.Goal.enter begin fun gl ->
-    Abstract.tclABSTRACT ~opaque:false None (Tacinterp.tactic_of_value ist t) end; }
+    Abstract.tclABSTRACT ~opaque:false None (Tacinterp.tactic_of_tacvalue ist t) end; }
 | [ "transparent_abstract" tactic3(t) "using" ident(id) ] -> { Proofview.Goal.enter begin fun gl ->
-    Abstract.tclABSTRACT ~opaque:false (Some id) (Tacinterp.tactic_of_value ist t) end; }
+    Abstract.tclABSTRACT ~opaque:false (Some id) (Tacinterp.tactic_of_tacvalue ist t) end; }
 END
 
 (* ********************************************************************* *)
@@ -683,6 +683,6 @@ END
 
 TACTIC EXTEND with_strategy
 | [ "with_strategy" strategy_level_or_var(v) "[" ne_smart_global_list(q) "]" tactic3(tac) ] -> {
-  with_set_strategy [(v, q)] (Tacinterp.tactic_of_value ist tac)
+  with_set_strategy [(v, q)] (Tacinterp.tactic_of_tacvalue ist tac)
 }
 END

plugins/ltac/internals.ml

@@ -53,7 +53,7 @@ let with_delayed_uconstr ist c tac =
 
 let replace_in_clause_maybe_by ist dir_opt c1 c2 cl tac =
   with_delayed_uconstr ist c1
-  (fun c1 -> Equality.replace_in_clause_maybe_by dir_opt c1 c2 cl (Option.map (Tacinterp.tactic_of_value ist) tac))
+  (fun c1 -> Equality.replace_in_clause_maybe_by dir_opt c1 c2 cl (Option.map (Tacinterp.tactic_of_tacvalue ist) tac))
 
 let replace_term ist dir_opt c cl =
   with_delayed_uconstr ist c (fun c -> Equality.replace_term dir_opt c cl)
@@ -163,7 +163,7 @@ let is_const x =
     | _ -> Tacticals.tclFAIL (Pp.str "not a constant")
 
 let unshelve ist t =
-  Proofview.with_shelf (Tacinterp.tactic_of_value ist t) >>= fun (gls, ()) ->
+  Proofview.with_shelf (Tacinterp.tactic_of_tacvalue ist t) >>= fun (gls, ()) ->
   let gls = List.map Proofview.with_empty_state gls in
   Proofview.Unsafe.tclGETGOALS >>= fun ogls ->
   Proofview.Unsafe.tclSETGOALS (gls @ ogls)

plugins/ltac/internals.mli

@@ -30,7 +30,7 @@ val with_delayed_uconstr : Tacinterp.interp_sign ->
   closed_glob_constr -> (EConstr.constr -> unit tactic) -> unit tactic
 val replace_in_clause_maybe_by : Tacinterp.interp_sign -> bool option ->
   closed_glob_constr -> EConstr.constr ->
-  Locus.clause -> Tacinterp.Value.t option -> unit tactic
+  Locus.clause -> Tacarg.tacvalue option -> unit tactic
 val replace_term : Tacinterp.interp_sign -> bool option -> closed_glob_constr ->
   Locus.clause -> unit tactic
 
@@ -51,7 +51,7 @@ val is_constructor : EConstr.t -> unit tactic
 val is_proj : EConstr.t -> unit tactic
 val is_const : EConstr.t -> unit tactic
 
-val unshelve : Tacinterp.interp_sign -> Tacinterp.Value.t -> unit tactic
+val unshelve : Tacinterp.interp_sign -> Tacarg.tacvalue -> unit tactic
 
 val decompose : EConstr.t list -> EConstr.t -> unit tactic
 

plugins/ltac/pptactic.ml

@@ -91,7 +91,7 @@ type 'a extra_genarg_printer =
   Environ.env -> Evd.evar_map ->
   (Environ.env -> Evd.evar_map -> EConstr.constr -> Pp.t) ->
   (Environ.env -> Evd.evar_map -> EConstr.constr -> Pp.t) ->
-  (Environ.env -> Evd.evar_map -> entry_relative_level -> Val.t -> Pp.t) ->
+  (Environ.env -> Evd.evar_map -> entry_relative_level -> tacvalue -> Pp.t) ->
   'a -> Pp.t
 
 type 'a raw_extra_genarg_printer_with_level =
@@ -112,7 +112,7 @@ type 'a extra_genarg_printer_with_level =
   Environ.env -> Evd.evar_map ->
   (Environ.env -> Evd.evar_map -> EConstr.constr -> Pp.t) ->
   (Environ.env -> Evd.evar_map -> EConstr.constr -> Pp.t) ->
-  (Environ.env -> Evd.evar_map -> entry_relative_level -> Val.t -> Pp.t) ->
+  (Environ.env -> Evd.evar_map -> entry_relative_level -> tacvalue -> Pp.t) ->
   entry_relative_level -> 'a -> Pp.t
 
 let string_of_genarg_arg (ArgumentType arg) =
@@ -1400,9 +1400,14 @@ let () =
   register_basic_print0 Stdarg.wit_pre_ident str str str;
   register_basic_print0 Stdarg.wit_string qstring qstring qstring
 
+let pr_tacvalue_ref = ref (fun _ _ : Pp.t -> assert false)
+
+let pr_tacvalue env v = !pr_tacvalue_ref env v
+
 let () =
   let printer env sigma _ _ prtac = prtac env sigma in
-  declare_extra_genarg_pprule_with_level wit_tactic printer printer printer
+  let top_print env sigma _ _ _ _ v = pr_tacvalue env v in
+  declare_extra_genarg_pprule_with_level wit_tactic printer printer top_print
   ltop (LevelLe 0)
 
 let () =
@@ -1435,3 +1440,7 @@ let () =
   in
   Gentactic.register_print wit_ltac (printer pr_raw_tactic_level)
     (printer (fun env _sigma n x -> pr_glob_tactic_level env n x))
+
+module Internal = struct
+  let pr_tacvalue_ref = pr_tacvalue_ref
+end

plugins/ltac/pptactic.mli

@@ -42,7 +42,7 @@ type 'a extra_genarg_printer =
   Environ.env -> Evd.evar_map ->
   (Environ.env -> Evd.evar_map -> EConstr.constr -> Pp.t) ->
   (Environ.env -> Evd.evar_map -> EConstr.constr -> Pp.t) ->
-  (Environ.env -> Evd.evar_map -> entry_relative_level -> Val.t -> Pp.t) ->
+  (Environ.env -> Evd.evar_map -> entry_relative_level -> Tacarg.tacvalue -> Pp.t) ->
   'a -> Pp.t
 
 type 'a raw_extra_genarg_printer_with_level =
@@ -63,7 +63,7 @@ type 'a extra_genarg_printer_with_level =
   Environ.env -> Evd.evar_map ->
   (Environ.env -> Evd.evar_map -> EConstr.constr -> Pp.t) ->
   (Environ.env -> Evd.evar_map -> EConstr.constr -> Pp.t) ->
-  (Environ.env -> Evd.evar_map -> entry_relative_level -> Val.t -> Pp.t) ->
+  (Environ.env -> Evd.evar_map -> entry_relative_level -> Tacarg.tacvalue -> Pp.t) ->
   entry_relative_level -> 'a -> Pp.t
 
 val declare_extra_genarg_pprule :
@@ -155,6 +155,8 @@ val pr_match_rule : bool -> ('a -> Pp.t) -> ('b -> Pp.t) ->
 
 val pr_value : entry_relative_level -> Val.t -> Pp.t
 
+val pr_tacvalue : env -> Tacarg.tacvalue -> Pp.t
+
 val pp_ltac_call_kind : ltac_call_kind -> Pp.t
 
 val ltop : entry_relative_level
@@ -163,3 +165,7 @@ val make_constr_printer : (env -> Evd.evar_map -> entry_relative_level -> 'a ->
   'a Genprint.top_printer
 
 val ssr_loaded : unit -> bool
+
+module Internal : sig
+  val pr_tacvalue_ref : (env -> Tacarg.tacvalue -> Pp.t) ref
+end

plugins/ltac/tacarg.ml

@@ -27,7 +27,10 @@ let wit_open_constr_with_bindings = make0 "open_constr_with_bindings"
 let wit_bindings = make0 "bindings"
 let wit_quantified_hypothesis = wit_quant_hyp
 
-let wit_tactic : (raw_tactic_expr, glob_tactic_expr, Val.t) genarg_type =
+(* we can put ocaml closures (through geninterp vals) in tacvalues so no need to be marshallable *)
+type tacvalue = ..
+
+let wit_tactic : (raw_tactic_expr, glob_tactic_expr, tacvalue) genarg_type =
   make0 "tactic"
 
 let wit_ltac_in_term = GenConstr.create "ltac_in_term"
@@ -36,3 +39,18 @@ let wit_ltac = Gentactic.make "ltac"
 
 let wit_destruction_arg =
   make0 "destruction_arg"
+
+module Internal = struct
+  let defined_tacvalue = ref false
+
+  let define_tacvalue (type a) () =
+    assert (not !defined_tacvalue);
+    defined_tacvalue := true;
+    let module M = (struct type tacvalue += V of a end) in
+    let of_v x = M.V x in
+    let to_v = function
+      | M.V x -> x
+      | _ -> assert false
+    in
+    of_v, to_v
+end

plugins/ltac/tacarg.mli

@@ -42,7 +42,9 @@ val wit_quantified_hypothesis : quantified_hypothesis uniform_genarg_type
 
 (** Generic arguments based on Ltac. *)
 
-val wit_tactic : (raw_tactic_expr, glob_tactic_expr, Geninterp.Val.t) genarg_type
+type tacvalue
+
+val wit_tactic : (raw_tactic_expr, glob_tactic_expr, tacvalue) genarg_type
 
 val wit_ltac_in_term : (raw_tactic_expr, Names.Id.Set.t * glob_tactic_expr) GenConstr.tag
 
@@ -56,3 +58,8 @@ val wit_destruction_arg :
    glob_constr_and_expr with_bindings Tactics.destruction_arg,
    delayed_open_constr_with_bindings Tactics.destruction_arg) genarg_type
 
+module Internal : sig
+
+  val define_tacvalue : unit -> ('a -> tacvalue) * (tacvalue -> 'a)
+
+end

plugins/ltac/taccoerce.ml

@@ -43,34 +43,6 @@ let pr_value env v =
   | TopPrinterNeedsContextAndLevel { default_already_surrounded; printer } ->
      pr_with_env (fun env sigma -> printer env sigma default_already_surrounded)
 
-(** Abstract application, to print ltac functions *)
-type appl =
-  | UnnamedAppl (** For generic applications: nothing is printed *)
-  | GlbAppl of (Names.KerName.t * Val.t list) list
-       (** For calls to global constants, some may alias other. *)
-
-(* Values for interpretation *)
-type tacvalue =
-  | VFun of
-      appl *
-      Tacexpr.ltac_trace *
-      Loc.t option * (* when executing a global Ltac function: the location where this function was called *)
-      Val.t Id.Map.t * (* closure *)
-      Name.t list * (* binders *)
-      Tacexpr.glob_tactic_expr (* body *)
-  | VRec of Val.t Id.Map.t ref * Tacexpr.glob_tactic_expr
-
-let tacvalue_tag : tacvalue Val.typ =
-  let tag = Val.create "tacvalue" in
-  let pr = function
-    | VFun (a,_,loc,ids,l,tac) ->
-      let tac = if List.is_empty l then tac else CAst.make ?loc @@ Tacexpr.TacFun (l,tac) in
-      let pr_env env sigma = if Id.Map.is_empty ids then mt () else cut () ++ str "where" ++ Id.Map.fold (fun id c pp -> cut () ++ Id.print id ++ str " := " ++ pr_value (Some (env,sigma)) c ++ pp) ids (mt ()) in
-      Genprint.TopPrinterNeedsContext (fun env sigma -> v 0 (hov 0 (Pptactic.pr_glob_tactic env tac) ++ pr_env env sigma))
-    | _ -> Genprint.TopPrinterBasic (fun _ -> str "<tactic closure>") in
-  let () = Genprint.register_val_print0 tag pr in
-  tag
-
 let constr_context_tag : Constr_matching.context Val.typ =
   let tag = Val.create "constr_context" in
   let pr env sigma lev c : Pp.t = Printer.pr_econstr_n_env env sigma lev (Constr_matching.repr_context c) in
@@ -109,6 +81,8 @@ struct
 
 type t = Val.t
 
+let tacvalue_tag = val_tag (topwit wit_tactic)
+
 let of_tacvalue v = Val.Dyn (tacvalue_tag, v)
 
 let to_tacvalue v = prj tacvalue_tag v

plugins/ltac/taccoerce.mli

@@ -21,17 +21,6 @@ open Tactypes
 exception CannotCoerceTo of string
 (** Exception raised whenever a coercion failed. *)
 
-(** Abstract application, to print ltac functions *)
-type appl =
-  | UnnamedAppl (** For generic applications: nothing is printed *)
-  | GlbAppl of (Names.KerName.t * Val.t list) list
-       (** For calls to global constants, some may alias other. *)
-
-type tacvalue =
-  | VFun of appl * Tacexpr.ltac_trace * Loc.t option * Val.t Id.Map.t *
-      Name.t list * Tacexpr.glob_tactic_expr
-  | VRec of Val.t Id.Map.t ref * Tacexpr.glob_tactic_expr
-
 (** {5 High-level access to values}
 
   The [of_*] functions cast a given argument into a value. The [to_*] do the
@@ -43,8 +32,8 @@ module Value :
 sig
   type t = Val.t
 
-  val of_tacvalue : tacvalue -> t
-  val to_tacvalue : t -> tacvalue option
+  val of_tacvalue : Tacarg.tacvalue -> t
+  val to_tacvalue : t -> Tacarg.tacvalue option
   val of_constr : constr -> t
   val to_constr : t -> constr option
   val of_uconstr : Ltac_pretype.closed_glob_constr -> t