From ac03def19c547f082422110a1e56e74ed5b3a634 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Fri, 27 Feb 2026 16:02:09 +0100 Subject: [PATCH 1/2] wit_tactic top type is tacvalue --- plugins/firstorder/g_ground.mlg | 2 +- plugins/ltac/extraargs.mlg | 6 +- plugins/ltac/extraargs.mli | 2 +- plugins/ltac/extratactics.mlg | 20 ++-- plugins/ltac/internals.ml | 4 +- plugins/ltac/internals.mli | 4 +- plugins/ltac/pptactic.ml | 22 +++- plugins/ltac/pptactic.mli | 6 +- plugins/ltac/tacarg.ml | 15 ++- plugins/ltac/tacarg.mli | 14 ++- plugins/ltac/taccoerce.ml | 30 +---- plugins/ltac/taccoerce.mli | 15 +-- plugins/ltac/tacinterp.ml | 113 +++++++++--------- plugins/ltac/tacinterp.mli | 5 +- plugins/ltac/tauto.ml | 4 + plugins/micromega/g_micromega.mlg | 24 ++-- plugins/micromega/zify.ml | 2 +- plugins/micromega/zify.mli | 2 +- plugins/ring/ring.ml | 4 +- plugins/ring/ring.mli | 4 +- plugins/ssr/ssrcommon.ml | 2 +- plugins/ssr/ssrcommon.mli | 2 +- plugins/ssr/ssrfwd.mli | 8 +- plugins/ssr/ssrparser.mli | 26 ++-- plugins/ssr/ssrtacs.mli | 2 +- plugins/ssr/ssrtacticals.mli | 10 +- test-suite/output/InvalidDisjunctiveIntro.out | 6 +- test-suite/output/bug6404.out | 3 +- 28 files changed, 186 insertions(+), 171 deletions(-) diff --git a/plugins/firstorder/g_ground.mlg b/plugins/firstorder/g_ground.mlg index 59e8a377387b..a460d01f3a9f 100644 --- a/plugins/firstorder/g_ground.mlg +++ b/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 = diff --git a/plugins/ltac/extraargs.mlg b/plugins/ltac/extraargs.mlg index 01b22b8b24cf..cb386946c156 100644 --- a/plugins/ltac/extraargs.mlg +++ b/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 diff --git a/plugins/ltac/extraargs.mli b/plugins/ltac/extraargs.mli index 91af7c80d7ab..27592b63f9a4 100644 --- a/plugins/ltac/extraargs.mli +++ b/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 -> diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg index b62c553dbfbe..b499395c3100 100644 --- a/plugins/ltac/extratactics.mlg +++ b/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,7 +179,7 @@ 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 @@ -187,7 +187,7 @@ 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 (**********************************************************************) @@ -195,8 +195,8 @@ END { -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 diff --git a/plugins/ltac/internals.ml b/plugins/ltac/internals.ml index bab239eed096..d9ecd6cc259a 100644 --- a/plugins/ltac/internals.ml +++ b/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) diff --git a/plugins/ltac/internals.mli b/plugins/ltac/internals.mli index 4bd96aba258f..009901c9bf4c 100644 --- a/plugins/ltac/internals.mli +++ b/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 diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index 22e0aea6f7d9..05dc9b021639 100644 --- a/plugins/ltac/pptactic.ml +++ b/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,25 @@ let () = register_basic_print0 Stdarg.wit_pre_ident str str str; register_basic_print0 Stdarg.wit_string qstring qstring qstring +let pr_tacvalue env = function + | VFun (a,_,loc,ids,l,tac) -> + let open Pp in + let tac = if List.is_empty l then tac else CAst.make ?loc @@ Tacexpr.TacFun (l,tac) in + let pr_env env = + 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 ltop c ++ pp) + ids (mt ()) + in + v 0 (hov 0 (pr_glob_tactic env tac) ++ pr_env env) + | VRec _ -> str "" + 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 _ _ _ _ = pr_tacvalue env in + declare_extra_genarg_pprule_with_level wit_tactic printer printer top_print ltop (LevelLe 0) let () = diff --git a/plugins/ltac/pptactic.mli b/plugins/ltac/pptactic.mli index a93dfb56324a..9300abee9b7d 100644 --- a/plugins/ltac/pptactic.mli +++ b/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 diff --git a/plugins/ltac/tacarg.ml b/plugins/ltac/tacarg.ml index ac98e78cacb1..36ccf600dfe9 100644 --- a/plugins/ltac/tacarg.ml +++ b/plugins/ltac/tacarg.ml @@ -13,6 +13,7 @@ open Genarg open Geninterp open Tacexpr +open Names let make0 ?dyn name = let wit = Genarg.make0 name in @@ -27,7 +28,19 @@ 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 = + +(** Abstract application, to print ltac functions *) +type appl = + | UnnamedAppl (** For generic applications: nothing is printed *) + | GlbAppl of (Names.KerName.t * Geninterp.Val.t list) list + (** For calls to global constants, some may alias other. *) + +type tacvalue = + | VFun of appl * ltac_trace * Loc.t option * Geninterp.Val.t Id.Map.t * + Name.t list * glob_tactic_expr + | VRec of Geninterp.Val.t Id.Map.t ref * glob_tactic_expr + +let wit_tactic : (raw_tactic_expr, glob_tactic_expr, tacvalue) genarg_type = make0 "tactic" let wit_ltac_in_term = GenConstr.create "ltac_in_term" diff --git a/plugins/ltac/tacarg.mli b/plugins/ltac/tacarg.mli index cac63bb86dc5..c7db853396b4 100644 --- a/plugins/ltac/tacarg.mli +++ b/plugins/ltac/tacarg.mli @@ -14,6 +14,7 @@ open Constrexpr open Genintern open Tactypes open Tacexpr +open Names (** Tactic related witnesses, could also live in tactics/ if other users *) @@ -42,7 +43,18 @@ 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 +(** Abstract application, to print ltac functions *) +type appl = + | UnnamedAppl (** For generic applications: nothing is printed *) + | GlbAppl of (Names.KerName.t * Geninterp.Val.t list) list + (** For calls to global constants, some may alias other. *) + +type tacvalue = + | VFun of appl * ltac_trace * Loc.t option * Geninterp.Val.t Id.Map.t * + Name.t list * glob_tactic_expr + | VRec of Geninterp.Val.t Id.Map.t ref * glob_tactic_expr + +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 diff --git a/plugins/ltac/taccoerce.ml b/plugins/ltac/taccoerce.ml index feef6ed741bd..e7f1a914e234 100644 --- a/plugins/ltac/taccoerce.ml +++ b/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 "") 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 diff --git a/plugins/ltac/taccoerce.mli b/plugins/ltac/taccoerce.mli index b15637a262a9..90baac82f5bb 100644 --- a/plugins/ltac/taccoerce.mli +++ b/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 diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index 36dc70975291..081923137718 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -1445,59 +1445,8 @@ and interp_app loc ist fv largs : Val.t Ftactic.t = (* Gives the tactic corresponding to the tactic value *) and tactic_of_value ist vle = match to_tacvalue vle with - | Some vle -> - begin match vle with - | VFun (appl,trace,loc,lfun,[],t) -> - Proofview.tclProofInfo [@ocaml.warning "-3"] >>= fun (_name, poly) -> - let ist = { - lfun = lfun; - poly; - (* todo: debug stack needs "trace" but that gives incorrect results for profiling - Couldn't figure out how to make them play together. Currently no way both can - be enabled. Perhaps profiling should be redesigned as suggested in profile_ltac.mli *) - extra = TacStore.set ist.extra f_trace (if Profile_tactic.get_profiling() then ([],[]) else trace); } in - let tac = name_if_glob appl (eval_tactic_ist ist t) in - let (stack, _) = trace in - do_profile stack (catch_error_tac_loc loc stack tac) - | VFun (appl,(stack,_),loc,vmap,vars,_) -> - let tactic_nm = - match appl with - UnnamedAppl -> "An unnamed user-defined tactic" - | GlbAppl apps -> - let nms = List.map (fun (kn,_) -> string_of_qualid (Tacenv.shortest_qualid_of_tactic kn)) apps in - match nms with - [] -> assert false - | kn::_ -> "The user-defined tactic \"" ^ kn ^ "\"" (* TODO: when do we not have a singleton? *) - in - let numargs = List.length vars in - let givenargs = - List.map (fun (arg,_) -> Names.Id.to_string arg) (Names.Id.Map.bindings vmap) in - let numgiven = List.length givenargs in - let info = Exninfo.reify () in - catch_error_tac stack @@ - Tacticals.tclZEROMSG ~info - Pp.(str tactic_nm ++ str " was not fully applied:" ++ spc() ++ - str "There is a missing argument for variable" ++ spc() ++ Name.print (List.hd vars) ++ - (if numargs > 1 then - spc() ++ str "and " ++ int (numargs - 1) ++ - str " more" - else mt()) ++ pr_comma() ++ - (match numgiven with - | 0 -> - str "no arguments at all were provided." - | 1 -> - str "1 argument was provided." - | _ -> - int numgiven ++ str " arguments were provided.")) - | VRec _ -> - let info = Exninfo.reify () in - Tacticals.tclZEROMSG ~info (str "A fully applied tactic is expected.") - end + | Some vle -> tactic_of_tacvalue ist vle | None -> - if has_type vle (topwit wit_tactic) then - let tac = out_gen (topwit wit_tactic) vle in - tactic_of_value ist tac - else let name = let Dyn (t, _) = vle in Val.repr t @@ -1505,6 +1454,53 @@ and tactic_of_value ist vle = let info = Exninfo.reify () in Tacticals.tclZEROMSG ~info (str "Expression does not evaluate to a tactic (got a " ++ str name ++ str ").") +and tactic_of_tacvalue ist = function + | VFun (appl,trace,loc,lfun,[],t) -> + Proofview.tclProofInfo [@ocaml.warning "-3"] >>= fun (_name, poly) -> + let ist = { + lfun = lfun; + poly; + (* todo: debug stack needs "trace" but that gives incorrect results for profiling + Couldn't figure out how to make them play together. Currently no way both can + be enabled. Perhaps profiling should be redesigned as suggested in profile_ltac.mli *) + extra = TacStore.set ist.extra f_trace (if Profile_tactic.get_profiling() then ([],[]) else trace); } in + let tac = name_if_glob appl (eval_tactic_ist ist t) in + let (stack, _) = trace in + do_profile stack (catch_error_tac_loc loc stack tac) + | VFun (appl,(stack,_),loc,vmap,vars,_) -> + let tactic_nm = + match appl with + UnnamedAppl -> "An unnamed user-defined tactic" + | GlbAppl apps -> + let nms = List.map (fun (kn,_) -> string_of_qualid (Tacenv.shortest_qualid_of_tactic kn)) apps in + match nms with + [] -> assert false + | kn::_ -> "The user-defined tactic \"" ^ kn ^ "\"" (* TODO: when do we not have a singleton? *) + in + let numargs = List.length vars in + let givenargs = + List.map (fun (arg,_) -> Names.Id.to_string arg) (Names.Id.Map.bindings vmap) in + let numgiven = List.length givenargs in + let info = Exninfo.reify () in + catch_error_tac stack @@ + Tacticals.tclZEROMSG ~info + Pp.(str tactic_nm ++ str " was not fully applied:" ++ spc() ++ + str "There is a missing argument for variable" ++ spc() ++ Name.print (List.hd vars) ++ + (if numargs > 1 then + spc() ++ str "and " ++ int (numargs - 1) ++ + str " more" + else mt()) ++ pr_comma() ++ + (match numgiven with + | 0 -> + str "no arguments at all were provided." + | 1 -> + str "1 argument was provided." + | _ -> + int numgiven ++ str " arguments were provided.")) + | VRec _ -> + let info = Exninfo.reify () in + Tacticals.tclZEROMSG ~info (str "A fully applied tactic is expected.") + (* Interprets the clauses of a recursive LetIn *) and interp_letrec ist llc u = Proofview.tclUNIT () >>= fun () -> (* delay for the effects of [lref], just in case. *) @@ -2003,8 +1999,11 @@ module Value = struct include Taccoerce.Value + let closure ist tac = + VFun (UnnamedAppl, extract_trace ist, None, ist.lfun, [], tac) + let of_closure ist tac = - let closure = VFun (UnnamedAppl, extract_trace ist, None, ist.lfun, [], tac) in + let closure = closure ist tac in of_tacvalue closure let apply_expr f args = @@ -2014,17 +2013,17 @@ module Value = struct (succ i, x :: vars, Id.Map.add id arg lfun) in let (_, args, lfun) = List.fold_right fold args (0, [], Id.Map.empty) in - let lfun = Id.Map.add (Id.of_string "F") f lfun in + let lfun = Id.Map.add (Id.of_string "F") (of_tacvalue f) lfun in let ist = { (default_ist ()) with lfun = lfun; } in ist, CAst.make @@ TacArg (TacCall (CAst.make (ArgVar CAst.(make @@ Id.of_string "F"),args))) (** Apply toplevel tactic values *) - let apply (f : value) (args: value list) = + let apply f (args: value list) = let ist, tac = apply_expr f args in eval_tactic_ist ist tac - let apply_val (f : value) (args: value list) = + let apply_val f (args: value list) = let ist, tac = apply_expr f args in val_interp ist tac @@ -2156,7 +2155,7 @@ let () = () let () = - let interp ist tac = Ftactic.return (Value.of_closure ist tac) in + let interp ist tac = Ftactic.return (Value.closure ist tac) in register_interp0 wit_tactic interp let () = diff --git a/plugins/ltac/tacinterp.mli b/plugins/ltac/tacinterp.mli index 6342c33a2ae7..961670613336 100644 --- a/plugins/ltac/tacinterp.mli +++ b/plugins/ltac/tacinterp.mli @@ -36,8 +36,8 @@ sig val to_list : t -> t list option val of_closure : interp_sign -> glob_tactic_expr -> t val cast : 'a typed_abstract_argument_type -> Geninterp.Val.t -> 'a - val apply : t -> t list -> unit Proofview.tactic - val apply_val : t -> t list -> t Ftactic.t + val apply : Tacarg.tacvalue -> t list -> unit Proofview.tactic + val apply_val : Tacarg.tacvalue -> t list -> t Ftactic.t end (** Values for interpretation *) @@ -118,6 +118,7 @@ val eval_tactic_ist : interp_sign -> glob_tactic_expr -> unit Proofview.tactic (** Same as [eval_tactic], but with the provided [interp_sign]. *) val tactic_of_value : interp_sign -> Value.t -> unit Proofview.tactic +val tactic_of_tacvalue : interp_sign -> Tacarg.tacvalue -> unit Proofview.tactic (** Globalization + interpretation *) diff --git a/plugins/ltac/tauto.ml b/plugins/ltac/tauto.ml index f0e590b2f29e..174c090b0d17 100644 --- a/plugins/ltac/tauto.ml +++ b/plugins/ltac/tauto.ml @@ -244,6 +244,10 @@ let val_of_id id = let find_cut _ ist = let k = Id.Map.find (Names.Id.of_string "k") ist.lfun in + let k = match Taccoerce.Value.to_tacvalue k with + | Some k -> k + | None -> CErrors.user_err Pp.(str "Argument to find_cut should be a tactic.") + in Proofview.Goal.enter begin fun gl -> let sigma = Proofview.Goal.sigma gl in let hyps0 = Proofview.Goal.hyps gl in diff --git a/plugins/micromega/g_micromega.mlg b/plugins/micromega/g_micromega.mlg index 1f530ad038dc..522590e6019b 100644 --- a/plugins/micromega/g_micromega.mlg +++ b/plugins/micromega/g_micromega.mlg @@ -27,7 +27,7 @@ open Tacarg DECLARE PLUGIN "rocq-runtime.plugins.micromega" TACTIC EXTEND Lra_Q -| [ "xlra_Q" tactic(t) ] -> { Coq_micromega.xlra_Q (Tacinterp.tactic_of_value ist t) } +| [ "xlra_Q" tactic(t) ] -> { Coq_micromega.xlra_Q (Tacinterp.tactic_of_tacvalue ist t) } END TACTIC EXTEND Lra_wit_Q @@ -35,11 +35,11 @@ TACTIC EXTEND Lra_wit_Q END TACTIC EXTEND Lra_R -| [ "xlra_R" tactic(t) ] -> { Coq_micromega.xlra_R (Tacinterp.tactic_of_value ist t) } +| [ "xlra_R" tactic(t) ] -> { Coq_micromega.xlra_R (Tacinterp.tactic_of_tacvalue ist t) } END TACTIC EXTEND Lia -| [ "xlia" tactic(t) ] -> { Coq_micromega.xlia (Tacinterp.tactic_of_value ist t) } +| [ "xlia" tactic(t) ] -> { Coq_micromega.xlia (Tacinterp.tactic_of_tacvalue ist t) } END TACTIC EXTEND Lia_wit @@ -47,7 +47,7 @@ TACTIC EXTEND Lia_wit END TACTIC EXTEND Nra_Q -| [ "xnra_Q" tactic(t) ] -> { Coq_micromega.xnra_Q (Tacinterp.tactic_of_value ist t) } +| [ "xnra_Q" tactic(t) ] -> { Coq_micromega.xnra_Q (Tacinterp.tactic_of_tacvalue ist t) } END TACTIC EXTEND Nra_wit_Q @@ -55,11 +55,11 @@ TACTIC EXTEND Nra_wit_Q END TACTIC EXTEND Nra_R -| [ "xnra_R" tactic(t) ] -> { Coq_micromega.xnra_R (Tacinterp.tactic_of_value ist t) } +| [ "xnra_R" tactic(t) ] -> { Coq_micromega.xnra_R (Tacinterp.tactic_of_tacvalue ist t) } END TACTIC EXTEND Nia -| [ "xnia" tactic(t) ] -> { Coq_micromega.xnia (Tacinterp.tactic_of_value ist t) } +| [ "xnia" tactic(t) ] -> { Coq_micromega.xnia (Tacinterp.tactic_of_tacvalue ist t) } END TACTIC EXTEND Nia_wit @@ -67,7 +67,7 @@ TACTIC EXTEND Nia_wit END TACTIC EXTEND Sos_Z -| [ "xsos_Z" tactic(t) ] -> { Coq_micromega.xsos_Z (Tacinterp.tactic_of_value ist t) } +| [ "xsos_Z" tactic(t) ] -> { Coq_micromega.xsos_Z (Tacinterp.tactic_of_tacvalue ist t) } END TACTIC EXTEND Sos_wit_Z @@ -75,7 +75,7 @@ TACTIC EXTEND Sos_wit_Z END TACTIC EXTEND Sos_Q -| [ "xsos_Q" tactic(t) ] -> { Coq_micromega.xsos_Q (Tacinterp.tactic_of_value ist t) } +| [ "xsos_Q" tactic(t) ] -> { Coq_micromega.xsos_Q (Tacinterp.tactic_of_tacvalue ist t) } END TACTIC EXTEND Sos_wit_Q @@ -83,12 +83,12 @@ TACTIC EXTEND Sos_wit_Q END TACTIC EXTEND Sos_R -| [ "xsos_R" tactic(t) ] -> { Coq_micromega.xsos_R (Tacinterp.tactic_of_value ist t) } +| [ "xsos_R" tactic(t) ] -> { Coq_micromega.xsos_R (Tacinterp.tactic_of_tacvalue ist t) } END TACTIC EXTEND Psatz_Z | [ "xpsatz_Z" nat_or_var(i) tactic(t) ] -> - { Coq_micromega.xpsatz_Z i (Tacinterp.tactic_of_value ist t) } + { Coq_micromega.xpsatz_Z i (Tacinterp.tactic_of_tacvalue ist t) } END TACTIC EXTEND Psatz_wit_Z @@ -97,7 +97,7 @@ END TACTIC EXTEND Psatz_Q | [ "xpsatz_Q" nat_or_var(i) tactic(t) ] -> - { Coq_micromega.xpsatz_Q i (Tacinterp.tactic_of_value ist t) } + { Coq_micromega.xpsatz_Q i (Tacinterp.tactic_of_tacvalue ist t) } END TACTIC EXTEND Psatz_wit_Q @@ -106,7 +106,7 @@ END TACTIC EXTEND Psatz_R | [ "xpsatz_R" nat_or_var(i) tactic(t) ] -> - { Coq_micromega.xpsatz_R i (Tacinterp.tactic_of_value ist t) } + { Coq_micromega.xpsatz_R i (Tacinterp.tactic_of_tacvalue ist t) } END VERNAC COMMAND EXTEND ShowLiaProfile CLASSIFIED AS QUERY diff --git a/plugins/micromega/zify.ml b/plugins/micromega/zify.ml index 77a4efdd0746..c5f259e08378 100644 --- a/plugins/micromega/zify.ml +++ b/plugins/micromega/zify.ml @@ -1432,7 +1432,7 @@ let iter_let_aux tac = init_cache (); Tacticals.tclMAP (do_let tac) sign) -let iter_let (tac : Ltac_plugin.Tacinterp.Value.t) = +let iter_let (tac : Ltac_plugin.Tacarg.tacvalue) = iter_let_aux (fun (id : Names.Id.t) t ty -> Ltac_plugin.Tacinterp.Value.apply tac [ Ltac_plugin.Tacinterp.Value.of_constr (EConstr.mkVar id) diff --git a/plugins/micromega/zify.mli b/plugins/micromega/zify.mli index 30ae2100ccc5..57b3444bcf98 100644 --- a/plugins/micromega/zify.mli +++ b/plugins/micromega/zify.mli @@ -29,5 +29,5 @@ module Saturate : S val zify_tac : unit Proofview.tactic val saturate : unit Proofview.tactic val iter_specs : unit Proofview.tactic -val iter_let : Ltac_plugin.Tacinterp.Value.t -> unit Proofview.tactic +val iter_let : Ltac_plugin.Tacarg.tacvalue -> unit Proofview.tactic val elim_let : unit Proofview.tactic diff --git a/plugins/ring/ring.ml b/plugins/ring/ring.ml index 16f4634155ab..942585fd0be6 100644 --- a/plugins/ring/ring.ml +++ b/plugins/ring/ring.ml @@ -688,7 +688,7 @@ let ltac_ring_structure e = [req;sth;ext;morph;th;cst_tac;pow_tac; lemma1;lemma2;pretac;posttac] -let ring_lookup (f : Value.t) lH rl t = +let ring_lookup f lH rl t = Proofview.Goal.enter begin fun gl -> let sigma = Proofview.Goal.sigma gl in let env = Proofview.Goal.env gl in @@ -967,7 +967,7 @@ let ltac_field_structure e = [req;cst_tac;pow_tac;field_ok;field_simpl_ok;field_simpl_eq_ok; field_simpl_eq_in_ok;cond_ok;pretac;posttac] -let field_lookup (f : Value.t) lH rl t = +let field_lookup f lH rl t = Proofview.Goal.enter begin fun gl -> let sigma = Proofview.Goal.sigma gl in let env = Proofview.Goal.env gl in diff --git a/plugins/ring/ring.mli b/plugins/ring/ring.mli index 0b946d9fe188..fc8f0e043b5f 100644 --- a/plugins/ring/ring.mli +++ b/plugins/ring/ring.mli @@ -25,7 +25,7 @@ val add_theory : val print_rings : unit -> unit val ring_lookup : - Geninterp.Val.t -> + Ltac_plugin.Tacarg.tacvalue -> constr list -> constr list -> constr -> unit Proofview.tactic @@ -37,6 +37,6 @@ val add_field_theory : val print_fields : unit -> unit val field_lookup : - Geninterp.Val.t -> + Ltac_plugin.Tacarg.tacvalue -> constr list -> constr list -> constr -> unit Proofview.tactic diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml index 12b5fad7dab0..6478d08f4f43 100644 --- a/plugins/ssr/ssrcommon.ml +++ b/plugins/ssr/ssrcommon.ml @@ -357,7 +357,7 @@ let red_product_skip_id env sigma c = match EConstr.kind sigma c with | App(hd,args) when Array.length args = 1 && is_id_constr sigma hd -> args.(0) | _ -> match Tacred.red_product env sigma c with Some c -> c | None -> c -let ssrevaltac ist gtac = Tacinterp.tactic_of_value ist gtac +let ssrevaltac ist gtac = Tacinterp.tactic_of_tacvalue ist gtac (** Open term to lambda-term coercion *)(* {{{ ************************************) diff --git a/plugins/ssr/ssrcommon.mli b/plugins/ssr/ssrcommon.mli index 979ae0985678..eb0de8cda3d8 100644 --- a/plugins/ssr/ssrcommon.mli +++ b/plugins/ssr/ssrcommon.mli @@ -157,7 +157,7 @@ val nbargs_open_constr : Environ.env -> Evd.evar_map * EConstr.t -> int val pf_nbargs : Environ.env -> Evd.evar_map -> EConstr.t -> int val ssrevaltac : - Tacinterp.interp_sign -> Tacinterp.Value.t -> unit Proofview.tactic + Tacinterp.interp_sign -> Tacarg.tacvalue -> unit Proofview.tactic val convert_concl_no_check : EConstr.t -> unit Proofview.tactic val convert_concl : check:bool -> EConstr.t -> unit Proofview.tactic diff --git a/plugins/ssr/ssrfwd.mli b/plugins/ssr/ssrfwd.mli index dd13cc5a1ff3..82b18b657d08 100644 --- a/plugins/ssr/ssrfwd.mli +++ b/plugins/ssr/ssrfwd.mli @@ -25,7 +25,7 @@ val havetac : ist -> ((((Ssrast.ssrclear option * Ssrast.ssripat list) * Ssrast.ssripats) * Ssrast.ssripats) * (((Ssrast.ssrfwdkind * 'a) * ast_closure_term) * - (bool * Tacinterp.Value.t option list))) -> + (bool * Tacarg.tacvalue option list))) -> bool -> bool -> unit Proofview.tactic @@ -44,7 +44,7 @@ val wlogtac : list * ('c * ast_closure_term) -> - Ltac_plugin.Tacinterp.Value.t Ssrast.ssrhint -> + Tacarg.tacvalue Ssrast.ssrhint -> bool -> [< `Gen of Names.Id.t option option | `NoGen > `NoGen ] -> unit Proofview.tactic @@ -55,7 +55,7 @@ val sufftac : Ssrast.ssripat list) * (('a * ast_closure_term) * - (bool * Tacinterp.Value.t option list)) -> + (bool * Tacarg.tacvalue option list)) -> unit Proofview.tactic (* pad_intro (by default false) indicates whether the intro-pattern @@ -67,7 +67,7 @@ val undertac : ?pad_intro:bool -> Ltac_plugin.Tacinterp.interp_sign -> Ssrast.ssripats option -> Ssrequality.ssrrwarg -> - Ltac_plugin.Tacinterp.Value.t Ssrast.ssrhint -> unit Proofview.tactic + Tacarg.tacvalue Ssrast.ssrhint -> unit Proofview.tactic val overtac : unit Proofview.tactic diff --git a/plugins/ssr/ssrparser.mli b/plugins/ssr/ssrparser.mli index 8a69a80558d7..a1d177156e4a 100644 --- a/plugins/ssr/ssrparser.mli +++ b/plugins/ssr/ssrparser.mli @@ -13,12 +13,12 @@ open Ltac_plugin val ssrtacarg : Tacexpr.raw_tactic_expr Procq.Entry.t -val wit_ssrtacarg : (Tacexpr.raw_tactic_expr, Tacexpr.glob_tactic_expr, Geninterp.Val.t) Genarg.genarg_type +val wit_ssrtacarg : (Tacexpr.raw_tactic_expr, Tacexpr.glob_tactic_expr, Tacarg.tacvalue) Genarg.genarg_type val pr_ssrtacarg : Environ.env -> Evd.evar_map -> 'a -> 'b -> (Environ.env -> Evd.evar_map -> Constrexpr.entry_relative_level -> 'c) -> 'c val ssrtclarg : Tacexpr.raw_tactic_expr Procq.Entry.t -val wit_ssrtclarg : (Tacexpr.raw_tactic_expr, Tacexpr.glob_tactic_expr, Geninterp.Val.t) Genarg.genarg_type +val wit_ssrtclarg : (Tacexpr.raw_tactic_expr, Tacexpr.glob_tactic_expr, Tacarg.tacvalue) Genarg.genarg_type val pr_ssrtclarg : Environ.env -> Evd.evar_map -> 'a -> 'b -> (Environ.env -> Evd.evar_map -> Constrexpr.entry_relative_level -> 'c -> 'd) -> 'c -> 'd @@ -31,28 +31,28 @@ open Ssrast type ssrfwdview = ast_closure_term list -val wit_ssrseqarg : (Tacexpr.raw_tactic_expr ssrseqarg, Tacexpr.glob_tactic_expr ssrseqarg, Geninterp.Val.t ssrseqarg) Genarg.genarg_type +val wit_ssrseqarg : (Tacexpr.raw_tactic_expr ssrseqarg, Tacexpr.glob_tactic_expr ssrseqarg, Tacarg.tacvalue ssrseqarg) Genarg.genarg_type val wit_ssrintros_ne : ssripats Genarg.uniform_genarg_type val wit_ssrintrosarg : (Tacexpr.raw_tactic_expr * ssripats, Tacexpr.glob_tactic_expr * ssripats, - Geninterp.Val.t * ssripats) Genarg.genarg_type + Tacarg.tacvalue * ssripats) Genarg.genarg_type val wit_ssripatrep : ssripat Genarg.uniform_genarg_type val wit_ssrclauses : clauses Genarg.uniform_genarg_type val wit_ssrhavefwdwbinders : (Tacexpr.raw_tactic_expr fwdbinders, Tacexpr.glob_tactic_expr fwdbinders, - Tacinterp.Value.t fwdbinders) Genarg.genarg_type + Tacarg.tacvalue fwdbinders) Genarg.genarg_type val wit_ssrhintarg : (Tacexpr.raw_tactic_expr ssrhint, Tacexpr.glob_tactic_expr ssrhint, - Tacinterp.Value.t ssrhint) Genarg.genarg_type + Tacarg.tacvalue ssrhint) Genarg.genarg_type val wit_ssrhint3arg : (Tacexpr.raw_tactic_expr ssrhint, Tacexpr.glob_tactic_expr ssrhint, - Tacinterp.Value.t ssrhint) Genarg.genarg_type + Tacarg.tacvalue ssrhint) Genarg.genarg_type val wit_ssrfwdid : Names.Id.t Genarg.uniform_genarg_type @@ -62,12 +62,12 @@ val wit_ssrsetfwd : val wit_ssrdoarg : (Tacexpr.raw_tactic_expr ssrdoarg, Tacexpr.glob_tactic_expr ssrdoarg, - Tacinterp.Value.t ssrdoarg) Genarg.genarg_type + Tacarg.tacvalue ssrdoarg) Genarg.genarg_type val wit_ssrhint : (Tacexpr.raw_tactic_expr ssrhint, Tacexpr.glob_tactic_expr ssrhint, - Tacinterp.Value.t ssrhint) Genarg.genarg_type + Tacarg.tacvalue ssrhint) Genarg.genarg_type val ssrhpats : ssrhpats Procq.Entry.t val wit_ssrhpats : ssrhpats Genarg.uniform_genarg_type @@ -79,7 +79,7 @@ val wit_ssrposefwd : (ssrfwdfmt * ast_closure_term) Genarg.uniform_genarg_type val wit_ssrhavefwd : ((ssrfwdfmt * ast_closure_term) * Tacexpr.raw_tactic_expr ssrhint , (ssrfwdfmt * ast_closure_term) * Tacexpr.glob_tactic_expr ssrhint - , (ssrfwdfmt * ast_closure_term) * Geninterp.Val.t ssrhint) + , (ssrfwdfmt * ast_closure_term) * Tacarg.tacvalue ssrhint) Genarg.genarg_type val wit_ssrrpat : ssripat Genarg.uniform_genarg_type @@ -267,13 +267,13 @@ val wit_ssrmult_ne : (int * ssrmmod) Genarg.uniform_genarg_type val wit_ssrortacarg : (Tacexpr.raw_tactic_expr ssrhint, bool * Ltac_plugin.Tacexpr.glob_tactic_expr option list, - bool * Geninterp.Val.t option list) + bool * Tacarg.tacvalue option list) Genarg.genarg_type val wit_ssrortacs : (Tacexpr.raw_tactic_expr option list, Tacexpr.glob_tactic_expr option list, - Geninterp.Val.t option list) + Tacarg.tacvalue option list) Genarg.genarg_type val wit_ssrsimpl_ne : @@ -282,4 +282,4 @@ val wit_ssrsimpl_ne : val wit_ssrstruct : Names.Id.t option Genarg.uniform_genarg_type val wit_ssrtac3arg : - (Tacexpr.raw_tactic_expr, Tacexpr.glob_tactic_expr, Geninterp.Val.t) Genarg.genarg_type + (Tacexpr.raw_tactic_expr, Tacexpr.glob_tactic_expr, Tacarg.tacvalue) Genarg.genarg_type diff --git a/plugins/ssr/ssrtacs.mli b/plugins/ssr/ssrtacs.mli index 57cd2e1b3b97..4069c40ae277 100644 --- a/plugins/ssr/ssrtacs.mli +++ b/plugins/ssr/ssrtacs.mli @@ -17,7 +17,7 @@ val wit_ssrseqdir : ssrdir Genarg.uniform_genarg_type val wit_ssrsufffwd : (Tacexpr.raw_tactic_expr ffwbinders, Tacexpr.glob_tactic_expr ffwbinders, - Geninterp.Val.t ffwbinders) Genarg.genarg_type + Tacarg.tacvalue ffwbinders) Genarg.genarg_type val wit_ssrcasearg : (cpattern ssragens) ssrmovearg Genarg.uniform_genarg_type val wit_ssrmovearg : (cpattern ssragens) ssrmovearg Genarg.uniform_genarg_type diff --git a/plugins/ssr/ssrtacticals.mli b/plugins/ssr/ssrtacticals.mli index 0ab1980ed026..0928ee8e87b7 100644 --- a/plugins/ssr/ssrtacticals.mli +++ b/plugins/ssr/ssrtacticals.mli @@ -15,11 +15,11 @@ open Ssrmatching_plugin val tclSEQAT : Tacinterp.interp_sign -> - Tacinterp.Value.t -> + Tacarg.tacvalue -> Ssrast.ssrdir -> int Locus.or_var * - (('a * Tacinterp.Value.t option list) * - Tacinterp.Value.t option) -> + (('a * Tacarg.tacvalue option list) * + Tacarg.tacvalue option) -> unit Proofview.tactic val tclCLAUSES : @@ -33,12 +33,12 @@ val tclCLAUSES : val hinttac : Tacinterp.interp_sign -> - bool -> bool * Tacinterp.Value.t option list -> unit Proofview.tactic + bool -> bool * Tacarg.tacvalue option list -> unit Proofview.tactic val ssrdotac : Tacinterp.interp_sign -> ((int Locus.or_var * Ssrast.ssrmmod) * - (bool * Tacinterp.Value.t option list)) * + (bool * Tacarg.tacvalue option list)) * ((Ssrast.ssrhyps * ((Ssrast.ssrhyp_or_id * string) * Ssrmatching.cpattern option) diff --git a/test-suite/output/InvalidDisjunctiveIntro.out b/test-suite/output/InvalidDisjunctiveIntro.out index 277062e50c3b..361aac6f2365 100644 --- a/test-suite/output/InvalidDisjunctiveIntro.out +++ b/test-suite/output/InvalidDisjunctiveIntro.out @@ -12,12 +12,12 @@ The command has indeed failed with message: Cannot coerce to a disjunctive/conjunctive pattern. File "./output/InvalidDisjunctiveIntro.v", line 10, characters 32-33: The command has indeed failed with message: -Ltac variable H is bound to idtac of type tacvalue which cannot be coerced to +Ltac variable H is bound to idtac of type tactic which cannot be coerced to an introduction pattern. File "./output/InvalidDisjunctiveIntro.v", line 13, characters 2-52: The command has indeed failed with message: Disjunctive/conjunctive introduction pattern expected. File "./output/InvalidDisjunctiveIntro.v", line 15, characters 50-52: The command has indeed failed with message: -Ltac variable H' is bound to idtac of type tacvalue which cannot be coerced -to an introduction pattern. +Ltac variable H' is bound to idtac of type tactic which cannot be coerced to +an introduction pattern. diff --git a/test-suite/output/bug6404.out b/test-suite/output/bug6404.out index 9940f3202091..b57b9934e88f 100644 --- a/test-suite/output/bug6404.out +++ b/test-suite/output/bug6404.out @@ -3,5 +3,6 @@ The command has indeed failed with message: The term "I" has type "True" which should be Set, Prop or Type. In nested Ltac calls to "c", "abs", "transparent_abstract (tactic3)", -"b", "a", "pose (I : I)" and "(I : I)", last term evaluation failed. +"$1" (bound to b ltac:(())), "b", "a", "pose (I : I)" and +"(I : I)", last term evaluation failed. From b6528af8fedf60f247a4de422b7800717ef5373a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Thu, 5 Mar 2026 17:49:28 +0100 Subject: [PATCH 2/2] Hide definition of tacvalue in tacinterp --- plugins/ltac/pptactic.ml | 23 +++++------- plugins/ltac/pptactic.mli | 4 +++ plugins/ltac/tacarg.ml | 29 +++++++++------- plugins/ltac/tacarg.mli | 17 ++++----- plugins/ltac/tacinterp.ml | 73 +++++++++++++++++++++++++++++---------- 5 files changed, 89 insertions(+), 57 deletions(-) diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index 05dc9b021639..46a68fa762e7 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -1400,24 +1400,13 @@ let () = register_basic_print0 Stdarg.wit_pre_ident str str str; register_basic_print0 Stdarg.wit_string qstring qstring qstring -let pr_tacvalue env = function - | VFun (a,_,loc,ids,l,tac) -> - let open Pp in - let tac = if List.is_empty l then tac else CAst.make ?loc @@ Tacexpr.TacFun (l,tac) in - let pr_env env = - 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 ltop c ++ pp) - ids (mt ()) - in - v 0 (hov 0 (pr_glob_tactic env tac) ++ pr_env env) - | VRec _ -> str "" +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 - let top_print env sigma _ _ _ _ = pr_tacvalue env in + 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) @@ -1451,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 diff --git a/plugins/ltac/pptactic.mli b/plugins/ltac/pptactic.mli index 9300abee9b7d..0f7602d255bb 100644 --- a/plugins/ltac/pptactic.mli +++ b/plugins/ltac/pptactic.mli @@ -165,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 diff --git a/plugins/ltac/tacarg.ml b/plugins/ltac/tacarg.ml index 36ccf600dfe9..aaf285cef808 100644 --- a/plugins/ltac/tacarg.ml +++ b/plugins/ltac/tacarg.ml @@ -13,7 +13,6 @@ open Genarg open Geninterp open Tacexpr -open Names let make0 ?dyn name = let wit = Genarg.make0 name in @@ -28,17 +27,8 @@ let wit_open_constr_with_bindings = make0 "open_constr_with_bindings" let wit_bindings = make0 "bindings" let wit_quantified_hypothesis = wit_quant_hyp - -(** Abstract application, to print ltac functions *) -type appl = - | UnnamedAppl (** For generic applications: nothing is printed *) - | GlbAppl of (Names.KerName.t * Geninterp.Val.t list) list - (** For calls to global constants, some may alias other. *) - -type tacvalue = - | VFun of appl * ltac_trace * Loc.t option * Geninterp.Val.t Id.Map.t * - Name.t list * glob_tactic_expr - | VRec of Geninterp.Val.t Id.Map.t ref * glob_tactic_expr +(* 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" @@ -49,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 diff --git a/plugins/ltac/tacarg.mli b/plugins/ltac/tacarg.mli index c7db853396b4..680a515abd3e 100644 --- a/plugins/ltac/tacarg.mli +++ b/plugins/ltac/tacarg.mli @@ -14,7 +14,6 @@ open Constrexpr open Genintern open Tactypes open Tacexpr -open Names (** Tactic related witnesses, could also live in tactics/ if other users *) @@ -43,16 +42,7 @@ val wit_quantified_hypothesis : quantified_hypothesis uniform_genarg_type (** Generic arguments based on Ltac. *) -(** Abstract application, to print ltac functions *) -type appl = - | UnnamedAppl (** For generic applications: nothing is printed *) - | GlbAppl of (Names.KerName.t * Geninterp.Val.t list) list - (** For calls to global constants, some may alias other. *) - -type tacvalue = - | VFun of appl * ltac_trace * Loc.t option * Geninterp.Val.t Id.Map.t * - Name.t list * glob_tactic_expr - | VRec of Geninterp.Val.t Id.Map.t ref * glob_tactic_expr +type tacvalue val wit_tactic : (raw_tactic_expr, glob_tactic_expr, tacvalue) genarg_type @@ -68,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 diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index 081923137718..8fca7cb9910d 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -42,6 +42,17 @@ open Ltac_pretype module TacStore = Tacenv.TacStore +(** Abstract application, to print ltac functions *) +type appl = + | UnnamedAppl (** For generic applications: nothing is printed *) + | GlbAppl of (Names.KerName.t * Geninterp.Val.t list) list + (** For calls to global constants, some may alias other. *) + +type tacvalue_v = + | VFun of appl * ltac_trace * Loc.t option * Geninterp.Val.t Id.Map.t * + Name.t list * glob_tactic_expr + | VRec of Geninterp.Val.t Id.Map.t ref * glob_tactic_expr + (* Signature for interpretation: val_interp and interpretation functions *) type interp_sign = Tacenv.interp_sign = { lfun : Geninterp.Val.t Id.Map.t @@ -138,6 +149,30 @@ let combine_appl appl1 appl2 = let of_tacvalue = Value.of_tacvalue let to_tacvalue = Value.to_tacvalue +let (of_tacvalue_v : tacvalue_v -> tacvalue), to_tacvalue_v = Tacarg.Internal.define_tacvalue () + +let pr_tacvalue env v = match to_tacvalue_v v with + | VFun (a,_,loc,ids,l,tac) -> + let open Pp in + let tac = if List.is_empty l then tac else CAst.make ?loc @@ Tacexpr.TacFun (l,tac) in + let pr_env env = + if Id.Map.is_empty ids then mt () + else + cut () ++ str "where" ++ + Id.Map.fold (fun id c pp -> + cut () ++ Id.print id ++ str " := " ++ Pptactic.pr_value Pptactic.ltop c ++ pp) + ids (mt ()) + in + v 0 (hov 0 (Pptactic.pr_glob_tactic env tac) ++ pr_env env) + | VRec _ -> str "" + +let () = + Pptactic.Internal.pr_tacvalue_ref := fun env v -> + pr_tacvalue env v + +let to_tacvalue_val v = Option.map to_tacvalue_v @@ to_tacvalue v +let of_tacvalue_val v = of_tacvalue @@ of_tacvalue_v v + (* Debug reference *) let debug = ref DebugOff @@ -154,9 +189,9 @@ let is_traced () = (** More naming applications *) let name_vfun appl vle = - match to_tacvalue vle with + match to_tacvalue_val vle with | Some (VFun (appl0,trace,loc,lfun,vars,t)) -> - of_tacvalue (VFun (combine_appl appl0 appl,trace,loc,lfun,vars,t)) + of_tacvalue_val (VFun (combine_appl appl0 appl,trace,loc,lfun,vars,t)) | Some (VRec _) | None -> vle let f_avoid_ids : Id.Set.t TacStore.field = TacStore.field "f_avoid_ids" @@ -261,7 +296,7 @@ let pr_closure env ist body = let pr_inspect env expr result = let pp_expr = Pptactic.pr_glob_tactic env expr in let pp_result = - match to_tacvalue result with + match to_tacvalue_val result with | Some (VFun (_, _, _, ist, ul, b)) -> let body = if List.is_empty ul then b else CAst.make (TacFun (ul, b)) in str "a closure with body " ++ fnl() ++ pr_closure env ist body @@ -286,7 +321,7 @@ let push_trace call ist = else [],[] let propagate_trace ist loc id v = - match to_tacvalue v with + match to_tacvalue_val v with | None -> Proofview.tclUNIT v | Some tacv -> match tacv with @@ -299,12 +334,12 @@ let propagate_trace ist loc id v = let t = if List.is_empty it then b else CAst.make (TacFun (it,b)) in let trace = push_trace(loc,LtacVarCall (kn,id,t)) ist in let ans = VFun (appl,trace,loc,lfun,it,b) in - Proofview.tclUNIT (of_tacvalue ans) + Proofview.tclUNIT (of_tacvalue_val ans) | VRec _ -> Proofview.tclUNIT v let append_trace trace v = - match to_tacvalue v with - | Some (VFun (appl,trace',loc,lfun,it,b)) -> of_tacvalue (VFun (appl,trace',loc,lfun,it,b)) + match to_tacvalue_val v with + | Some (VFun (appl,trace',loc,lfun,it,b)) -> of_tacvalue_val (VFun (appl,trace',loc,lfun,it,b)) | _ -> v (* Dynamically check that an argument is a tactic *) @@ -312,8 +347,8 @@ let coerce_to_tactic loc id v = let fail () = user_err ?loc (str "Variable " ++ Id.print id ++ str " should be bound to a tactic.") in - match to_tacvalue v with - | Some (VFun (appl,trace,_,lfun,it,b)) -> of_tacvalue (VFun (appl,trace,loc,lfun,it,b)) + match to_tacvalue_val v with + | Some (VFun (appl,trace,_,lfun,it,b)) -> of_tacvalue_val (VFun (appl,trace,loc,lfun,it,b)) | _ -> fail () let intro_pattern_of_ident id = CAst.make @@ IntroNaming (IntroIdentifier id) @@ -1151,7 +1186,7 @@ let rec val_interp ist ?(appl=UnnamedAppl) (tac:glob_tactic_expr) : Val.t Ftacti let value_interp ist = match tac2 with | TacFun (it, body) -> - Ftactic.return (of_tacvalue (VFun (UnnamedAppl, extract_trace ist, extract_loc ist, ist.lfun, it, body))) + Ftactic.return (of_tacvalue_val (VFun (UnnamedAppl, extract_trace ist, extract_loc ist, ist.lfun, it, body))) | TacLetIn (true,l,u) -> interp_letrec ist l u | TacLetIn (false,l,u) -> interp_letin ist l u | TacMatchGoal (lz,lr,lmr) -> interp_match_goal ist lz lr lmr @@ -1159,7 +1194,7 @@ let rec val_interp ist ?(appl=UnnamedAppl) (tac:glob_tactic_expr) : Val.t Ftacti | TacArg v -> interp_tacarg ist v | _ -> (* Delayed evaluation *) - Ftactic.return (of_tacvalue (VFun (UnnamedAppl, extract_trace ist, extract_loc ist, ist.lfun, [], tac))) + Ftactic.return (of_tacvalue_val (VFun (UnnamedAppl, extract_trace ist, extract_loc ist, ist.lfun, [], tac))) in let open Ftactic in Control.check_for_interrupt (); @@ -1305,7 +1340,7 @@ and eval_tactic_ist ist tac : unit Proofview.tactic = Ftactic.run args tac and force_vrec ist v : Val.t Ftactic.t = - match to_tacvalue v with + match to_tacvalue_val v with | Some (VRec (lfun,body)) -> val_interp {ist with lfun = !lfun} body | _ -> Ftactic.return v @@ -1385,7 +1420,7 @@ and interp_tacarg ist arg : Val.t Ftactic.t = and interp_app loc ist fv largs : Val.t Ftactic.t = Proofview.tclProofInfo [@ocaml.warning "-3"] >>= fun (_name, poly) -> let (>>=) = Ftactic.bind in - match to_tacvalue fv with + match to_tacvalue_val fv with | None | Some (VRec _) -> Tacticals.tclZEROMSG (str "Illegal tactic application.") (* if var=[] and body has been delayed by val_interp, then body is not a tactic that expects arguments. @@ -1432,7 +1467,7 @@ and interp_app loc ist fv largs : Val.t Ftactic.t = end <*> if List.is_empty lval then Ftactic.return v else interp_app loc ist v lval else - Ftactic.return (of_tacvalue (VFun(push_appl appl largs,trace,loc,newlfun,lvar,body))) + Ftactic.return (of_tacvalue_val (VFun(push_appl appl largs,trace,loc,newlfun,lvar,body))) | Some (VFun(appl,trace,_,olfun,[],body)) -> let extra_args = List.length largs in let info = Exninfo.reify () in @@ -1454,7 +1489,7 @@ and tactic_of_value ist vle = let info = Exninfo.reify () in Tacticals.tclZEROMSG ~info (str "Expression does not evaluate to a tactic (got a " ++ str name ++ str ").") -and tactic_of_tacvalue ist = function +and tactic_of_tacvalue ist v = match to_tacvalue_v v with | VFun (appl,trace,loc,lfun,[],t) -> Proofview.tclProofInfo [@ocaml.warning "-3"] >>= fun (_name, poly) -> let ist = { @@ -1506,7 +1541,7 @@ and interp_letrec ist llc u = Proofview.tclUNIT () >>= fun () -> (* delay for the effects of [lref], just in case. *) let lref = ref ist.lfun in let fold accu ({v=na}, b) = - let v = of_tacvalue (VRec (lref, CAst.make (TacArg b))) in + let v = of_tacvalue_val (VRec (lref, CAst.make (TacArg b))) in Name.fold_right (fun id -> Id.Map.add id v) na accu in let lfun = List.fold_left fold ist.lfun llc in @@ -1536,7 +1571,7 @@ and interp_match_success ist { Tactic_matching.subst ; context ; terms ; lhs } = let lfun = extend_values_with_bindings subst (lctxt +++ hyp_subst +++ ist.lfun) in let ist = { ist with lfun } in val_interp ist lhs >>= fun v -> - match to_tacvalue v with + match to_tacvalue_val v with | Some (VFun (appl,trace,loc,lfun,[],t)) -> let ist = { lfun = lfun @@ -1547,7 +1582,7 @@ and interp_match_success ist { Tactic_matching.subst ; context ; terms ; lhs } = let dummy = VFun (appl, extract_trace ist, loc, Id.Map.empty, [], CAst.make (TacId [])) in let (stack, _) = trace in - catch_error_tac stack (tac <*> Ftactic.return (of_tacvalue dummy)) + catch_error_tac stack (tac <*> Ftactic.return (of_tacvalue_val dummy)) | _ -> Ftactic.return v @@ -2000,7 +2035,7 @@ module Value = struct include Taccoerce.Value let closure ist tac = - VFun (UnnamedAppl, extract_trace ist, None, ist.lfun, [], tac) + of_tacvalue_v @@ VFun (UnnamedAppl, extract_trace ist, None, ist.lfun, [], tac) let of_closure ist tac = let closure = closure ist tac in