aboutsummaryrefslogtreecommitdiff
path: root/plugins/ltac
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/ltac')
-rw-r--r--plugins/ltac/evar_tactics.ml32
-rw-r--r--plugins/ltac/extraargs.mlg54
-rw-r--r--plugins/ltac/extraargs.mli4
-rw-r--r--plugins/ltac/extratactics.mlg8
-rw-r--r--plugins/ltac/g_class.mlg15
-rw-r--r--plugins/ltac/g_ltac.mlg6
-rw-r--r--plugins/ltac/g_tactic.mlg3
-rw-r--r--plugins/ltac/pptactic.ml2
-rw-r--r--plugins/ltac/profile_ltac.ml108
-rw-r--r--plugins/ltac/rewrite.ml18
-rw-r--r--plugins/ltac/taccoerce.ml7
-rw-r--r--plugins/ltac/tacentries.ml105
-rw-r--r--plugins/ltac/tacentries.mli19
-rw-r--r--plugins/ltac/tacintern.ml83
-rw-r--r--plugins/ltac/tacinterp.ml50
-rw-r--r--plugins/ltac/tacinterp.mli1
-rw-r--r--plugins/ltac/tacsubst.ml1
17 files changed, 383 insertions, 133 deletions
diff --git a/plugins/ltac/evar_tactics.ml b/plugins/ltac/evar_tactics.ml
index 17a7121a3f..f867a47c08 100644
--- a/plugins/ltac/evar_tactics.ml
+++ b/plugins/ltac/evar_tactics.ml
@@ -14,10 +14,7 @@ open Constr
open Context
open CErrors
open Evar_refiner
-open Tacmach
open Tacexpr
-open Refiner
-open Evd
open Locus
open Context.Named.Declaration
open Ltac_pretype
@@ -26,7 +23,11 @@ module NamedDecl = Context.Named.Declaration
(* The instantiate tactic *)
-let instantiate_evar evk (ist,rawc) env sigma =
+let instantiate_evar evk (ist,rawc) =
+ let open Proofview.Notations in
+ Proofview.tclENV >>= fun env ->
+ Proofview.Goal.enter begin fun gl ->
+ let sigma = Proofview.Goal.sigma gl in
let evi = Evd.find sigma evk in
let filtered = Evd.evar_filtered_env env evi in
let constrvars = Tacinterp.extract_ltac_constr_values ist filtered in
@@ -37,7 +38,8 @@ let instantiate_evar evk (ist,rawc) env sigma =
ltac_genargs = ist.Geninterp.lfun;
} in
let sigma' = w_refine (evk,evi) (lvar ,rawc) env sigma in
- tclEVARS sigma'
+ Proofview.Unsafe.tclEVARS sigma'
+ end
let evar_list sigma c =
let rec evrec acc c =
@@ -47,14 +49,15 @@ let evar_list sigma c =
evrec [] c
let instantiate_tac n c ido =
- Proofview.V82.tactic begin fun gl ->
- let env = Global.env () in
- let sigma = gl.sigma in
+ Proofview.Goal.enter begin fun gl ->
+ let sigma = Proofview.Goal.sigma gl in
+ let env = Proofview.Goal.env gl in
+ let concl = Proofview.Goal.concl gl in
let evl =
match ido with
- ConclLocation () -> evar_list sigma (pf_concl gl)
+ ConclLocation () -> evar_list sigma concl
| HypLocation (id,hloc) ->
- let decl = Environ.lookup_named id (pf_env gl) in
+ let decl = Environ.lookup_named id env in
match hloc with
InHyp ->
(match decl with
@@ -70,17 +73,16 @@ let instantiate_tac n c ido =
user_err Pp.(str "Not enough uninstantiated existential variables.");
if n <= 0 then user_err Pp.(str "Incorrect existential variable index.");
let evk,_ = List.nth evl (n-1) in
- instantiate_evar evk c env sigma gl
+ instantiate_evar evk c
end
let instantiate_tac_by_name id c =
- Proofview.V82.tactic begin fun gl ->
- let env = Global.env () in
- let sigma = gl.sigma in
+ Proofview.Goal.enter begin fun gl ->
+ let sigma = Proofview.Goal.sigma gl in
let evk =
try Evd.evar_key id sigma
with Not_found -> user_err Pp.(str "Unknown existential variable.") in
- instantiate_evar evk c env sigma gl
+ instantiate_evar evk c
end
let let_evar name typ =
diff --git a/plugins/ltac/extraargs.mlg b/plugins/ltac/extraargs.mlg
index c4731e5c34..eb53fd45d0 100644
--- a/plugins/ltac/extraargs.mlg
+++ b/plugins/ltac/extraargs.mlg
@@ -31,6 +31,8 @@ let create_generic_quotation name e wit =
let () = create_generic_quotation "integer" Pcoq.Prim.integer Stdarg.wit_int
let () = create_generic_quotation "string" Pcoq.Prim.string Stdarg.wit_string
+let () = create_generic_quotation "smart_global" Pcoq.Prim.smart_global Stdarg.wit_smart_global
+
let () = create_generic_quotation "ident" Pcoq.Prim.ident Stdarg.wit_ident
let () = create_generic_quotation "reference" Pcoq.Prim.reference Stdarg.wit_ref
let () = create_generic_quotation "uconstr" Pcoq.Constr.lconstr Stdarg.wit_uconstr
@@ -342,3 +344,55 @@ let pr_lpar_id_colon _ _ _ _ = mt ()
ARGUMENT EXTEND test_lpar_id_colon TYPED AS unit PRINTED BY { pr_lpar_id_colon }
| [ local_test_lpar_id_colon(x) ] -> { () }
END
+
+{
+
+(* Work around a limitation of the macro system *)
+let strategy_level0 = Pcoq.Prim.strategy_level
+
+let pr_strategy _ _ _ v = Conv_oracle.pr_level v
+
+}
+
+ARGUMENT EXTEND strategy_level PRINTED BY { pr_strategy }
+| [ strategy_level0(n) ] -> { n }
+END
+
+{
+
+let intern_strategy ist v = match v with
+| ArgVar id -> ArgVar (Tacintern.intern_hyp ist id)
+| ArgArg v -> ArgArg v
+
+let subst_strategy _ v = v
+
+let interp_strategy ist gl = function
+| ArgArg n -> gl.Evd.sigma, n
+| ArgVar { CAst.v = id; CAst.loc } ->
+ let v =
+ try Id.Map.find id ist.lfun
+ with Not_found ->
+ CErrors.user_err ?loc
+ (str "Unbound variable " ++ Id.print id ++ str".")
+ in
+ let v =
+ try Tacinterp.Value.cast (Genarg.topwit wit_strategy_level) v
+ with CErrors.UserError _ -> Taccoerce.error_ltac_variable ?loc id None v "a strategy_level"
+ in
+ gl.Evd.sigma, v
+
+let pr_loc_strategy _ _ _ v = Pputils.pr_or_var Conv_oracle.pr_level v
+
+}
+
+ARGUMENT EXTEND strategy_level_or_var
+ TYPED AS strategy_level
+ PRINTED BY { pr_strategy }
+ INTERPRETED BY { interp_strategy }
+ GLOBALIZED BY { intern_strategy }
+ SUBSTITUTED BY { subst_strategy }
+ RAW_PRINTED BY { pr_loc_strategy }
+ GLOB_PRINTED BY { pr_loc_strategy }
+| [ strategy_level(n) ] -> { ArgArg n }
+| [ identref(id) ] -> { ArgVar id }
+END
diff --git a/plugins/ltac/extraargs.mli b/plugins/ltac/extraargs.mli
index fbdb7c0032..e52bf55f71 100644
--- a/plugins/ltac/extraargs.mli
+++ b/plugins/ltac/extraargs.mli
@@ -78,3 +78,7 @@ val wit_in_clause :
(lident Locus.clause_expr,
lident Locus.clause_expr,
Id.t Locus.clause_expr) Genarg.genarg_type
+
+val wit_strategy_level : Conv_oracle.level Genarg.uniform_genarg_type
+
+val wit_strategy_level_or_var : (Conv_oracle.level Locus.or_var, Conv_oracle.level Locus.or_var, Conv_oracle.level) Genarg.genarg_type
diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg
index 0bad3cbe5b..ffb597d4cb 100644
--- a/plugins/ltac/extratactics.mlg
+++ b/plugins/ltac/extratactics.mlg
@@ -1119,3 +1119,11 @@ let tclOPTIMIZE_HEAP =
TACTIC EXTEND optimize_heap
| [ "optimize_heap" ] -> { tclOPTIMIZE_HEAP }
END
+
+(** Tactic analogous to [Strategy] vernacular *)
+
+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)
+}
+END
diff --git a/plugins/ltac/g_class.mlg b/plugins/ltac/g_class.mlg
index 0f0341f123..81e745b714 100644
--- a/plugins/ltac/g_class.mlg
+++ b/plugins/ltac/g_class.mlg
@@ -54,16 +54,23 @@ END
{
+let pr_search_strategy_name _prc _prlc _prt = function
+ | Dfs -> Pp.str "dfs"
+ | Bfs -> Pp.str "bfs"
+
let pr_search_strategy _prc _prlc _prt = function
- | Some Dfs -> Pp.str "dfs"
- | Some Bfs -> Pp.str "bfs"
+ | Some s -> pr_search_strategy_name _prc _prlc _prt s
| None -> Pp.mt ()
}
+ARGUMENT EXTEND eauto_search_strategy_name PRINTED BY { pr_search_strategy_name }
+| [ "bfs" ] -> { Bfs }
+| [ "dfs" ] -> { Dfs }
+END
+
ARGUMENT EXTEND eauto_search_strategy PRINTED BY { pr_search_strategy }
-| [ "(bfs)" ] -> { Some Bfs }
-| [ "(dfs)" ] -> { Some Dfs }
+| [ "(" eauto_search_strategy_name(s) ")" ] -> { Some s }
| [ ] -> { None }
END
diff --git a/plugins/ltac/g_ltac.mlg b/plugins/ltac/g_ltac.mlg
index 5baa23b3e9..0e661543db 100644
--- a/plugins/ltac/g_ltac.mlg
+++ b/plugins/ltac/g_ltac.mlg
@@ -216,8 +216,8 @@ GRAMMAR EXTEND Gram
;
match_key:
[ [ "match" -> { Once }
- | "lazymatch" -> { Select }
- | "multimatch" -> { General } ] ]
+ | IDENT "lazymatch" -> { Select }
+ | IDENT "multimatch" -> { General } ] ]
;
input_fun:
[ [ "_" -> { Name.Anonymous }
@@ -342,7 +342,7 @@ GRAMMAR EXTEND Gram
hint:
[ [ IDENT "Extern"; n = natural; c = OPT Constr.constr_pattern ; "=>";
tac = Pltac.tactic ->
- { ComHints.HintsExtern (n,c, in_tac tac) } ] ]
+ { Vernacexpr.HintsExtern (n,c, in_tac tac) } ] ]
;
operconstr: LEVEL "0"
[ [ IDENT "ltac"; ":"; "("; tac = Pltac.tactic_expr; ")" ->
diff --git a/plugins/ltac/g_tactic.mlg b/plugins/ltac/g_tactic.mlg
index 6a158bde17..e51b1f051d 100644
--- a/plugins/ltac/g_tactic.mlg
+++ b/plugins/ltac/g_tactic.mlg
@@ -30,9 +30,6 @@ open Pcoq
let all_with delta = Redops.make_red_flag [FBeta;FMatch;FFix;FCofix;FZeta;delta]
-let tactic_kw = [ "->"; "<-" ; "by" ]
-let _ = List.iter CLexer.add_keyword tactic_kw
-
let err () = raise Stream.Failure
(* Hack to parse "(x:=t)" as an explicit argument without conflicts with the *)
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index 09f1fc371a..d74e981c6d 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -1325,6 +1325,8 @@ let () =
register_basic_print0 wit_int_or_var (pr_or_var int) (pr_or_var int) int;
register_basic_print0 wit_ref
pr_qualid (pr_or_var (pr_located pr_global)) pr_global;
+ register_basic_print0 wit_smart_global
+ (pr_or_by_notation pr_qualid) (pr_or_var (pr_located pr_global)) pr_global;
register_basic_print0 wit_ident pr_id pr_id pr_id;
register_basic_print0 wit_var pr_lident pr_lident pr_id;
register_print0 wit_intropattern pr_raw_intro_pattern pr_glob_intro_pattern pr_intro_pattern_env [@warning "-3"];
diff --git a/plugins/ltac/profile_ltac.ml b/plugins/ltac/profile_ltac.ml
index 14fab251d0..0dbf16a821 100644
--- a/plugins/ltac/profile_ltac.ml
+++ b/plugins/ltac/profile_ltac.ml
@@ -25,27 +25,20 @@ let is_profiling = Flags.profile_ltac
let set_profiling b = is_profiling := b
let get_profiling () = !is_profiling
-(** LtacProf cannot yet handle backtracking into multi-success tactics.
- To properly support this, we'd have to somehow recreate our location in the
- call-stack, and stop/restart the intervening timers. This is tricky and
- possibly expensive, so instead we currently just emit a warning that
- profiling results will be off. *)
-let encountered_multi_success_backtracking = ref false
-
-let warn_profile_backtracking =
- CWarnings.create ~name:"profile-backtracking" ~category:"ltac"
- (fun () -> strbrk "Ltac Profiler cannot yet handle backtracking \
- into multi-success tactics; profiling results may be wildly inaccurate.")
-
-let warn_encountered_multi_success_backtracking () =
- if !encountered_multi_success_backtracking then
- warn_profile_backtracking ()
-
-let encounter_multi_success_backtracking () =
- if not !encountered_multi_success_backtracking
+let encountered_invalid_stack_no_self = ref false
+
+let warn_invalid_stack_no_self =
+ CWarnings.create ~name:"profile-invalid-stack-no-self" ~category:"ltac"
+ (fun () -> strbrk
+ "Ltac Profiler encountered an invalid stack (no self \
+ node). This can happen if you reset the profile during \
+ tactic execution.")
+
+let encounter_invalid_stack_no_self () =
+ if not !encountered_invalid_stack_no_self
then begin
- encountered_multi_success_backtracking := true;
- warn_encountered_multi_success_backtracking ()
+ encountered_invalid_stack_no_self := true;
+ warn_invalid_stack_no_self ()
end
@@ -76,8 +69,7 @@ module Local = Summary.Local
let stack = Local.ref ~name:"LtacProf-stack" [empty_treenode root]
let reset_profile_tmp () =
- Local.(stack := [empty_treenode root]);
- encountered_multi_success_backtracking := false
+ Local.(stack := [empty_treenode root])
(* ************** XML Serialization ********************* *)
@@ -218,7 +210,6 @@ let to_string ~filter ?(cutoff=0.0) node =
cumulate tree;
!global
in
- warn_encountered_multi_success_backtracking ();
let filter s n = filter s && (all_total <= 0.0 || n /. all_total >= cutoff /. 100.0) in
let msg =
h 0 (str "total time: " ++ padl 11 (format_sec (all_total))) ++
@@ -296,13 +287,15 @@ let exit_tactic ~count_call start_time c =
match Local.(!stack) with
| [] | [_] ->
(* oops, our stack is invalid *)
- encounter_multi_success_backtracking ();
+ encounter_invalid_stack_no_self ();
reset_profile_tmp ()
| node :: (parent :: rest as full_stack) ->
let name = string_of_call c in
if not (String.equal name node.name) then
(* oops, our stack is invalid *)
- encounter_multi_success_backtracking ();
+ CErrors.anomaly
+ (Pp.strbrk "Ltac Profiler encountered an invalid stack (wrong self node) \
+ likely due to backtracking into multi-success tactics.");
let node = { node with
total = node.total +. diff;
local = node.local +. diff;
@@ -332,38 +325,56 @@ let exit_tactic ~count_call start_time c =
(* Calls are over, we reset the stack and send back data *)
if rest == [] && get_profiling () then begin
assert(String.equal root parent.name);
+ encountered_invalid_stack_no_self := false;
reset_profile_tmp ();
feedback_results parent
end
-let tclFINALLY tac (finally : unit Proofview.tactic) =
+(** [tclWRAPFINALLY before tac finally] runs [before] before each
+ entry-point of [tac] and passes the result of [before] to
+ [finally], which is then run at each exit-point of [tac],
+ regardless of whether it succeeds or fails. Said another way, if
+ [tac] succeeds, then it behaves as [before >>= fun v -> tac >>= fun
+ ret -> finally v <*> tclUNIT ret]; otherwise, if [tac] fails with
+ [e], it behaves as [before >>= fun v -> finally v <*> tclZERO
+ e]. *)
+let rec tclWRAPFINALLY before tac finally =
+ let open Proofview in
let open Proofview.Notations in
- Proofview.tclIFCATCH
- tac
- (fun v -> finally <*> Proofview.tclUNIT v)
- (fun (exn, info) -> finally <*> Proofview.tclZERO ~info exn)
+ before >>= fun v -> tclCASE tac >>= function
+ | Fail (e, info) -> finally v >>= fun () -> tclZERO ~info e
+ | Next (ret, tac') -> tclOR
+ (finally v >>= fun () -> tclUNIT ret)
+ (fun e -> tclWRAPFINALLY before (tac' e) finally)
let do_profile s call_trace ?(count_call=true) tac =
let open Proofview.Notations in
- Proofview.tclLIFT (Proofview.NonLogical.make (fun () ->
- if !is_profiling then
- match call_trace, Local.(!stack) with
- | (_, c) :: _, parent :: rest ->
- let name = string_of_call c in
- let node = get_child name parent in
- Local.(stack := node :: parent :: rest);
- Some (time ())
- | _ :: _, [] -> assert false
- | _ -> None
- else None)) >>= function
- | Some start_time ->
- tclFINALLY
- tac
+ (* We do an early check to [is_profiling] so that we save the
+ overhead of [tclWRAPFINALLY] when profiling is not set
+ *)
+ Proofview.tclLIFT (Proofview.NonLogical.make (fun () -> !is_profiling)) >>= function
+ | false -> tac
+ | true ->
+ tclWRAPFINALLY
(Proofview.tclLIFT (Proofview.NonLogical.make (fun () ->
- (match call_trace with
- | (_, c) :: _ -> exit_tactic ~count_call start_time c
- | [] -> ()))))
- | None -> tac
+ if !is_profiling then
+ match call_trace, Local.(!stack) with
+ | (_, c) :: _, parent :: rest ->
+ let name = string_of_call c in
+ let node = get_child name parent in
+ Local.(stack := node :: parent :: rest);
+ Some (time ())
+ | _ :: _, [] -> assert false
+ | _ -> None
+ else None)))
+ tac
+ (function
+ | Some start_time ->
+ (Proofview.tclLIFT (Proofview.NonLogical.make (fun () ->
+ (match call_trace with
+ | (_, c) :: _ -> exit_tactic ~count_call start_time c
+ | [] -> ()))))
+ | None -> Proofview.tclUNIT ())
(* ************** Accumulation of data from workers ************************* *)
@@ -396,6 +407,7 @@ let _ =
| _ -> ()))
let reset_profile () =
+ encountered_invalid_stack_no_self := false;
reset_profile_tmp ();
data := SM.empty
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 3834b21a14..d6b2a17882 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -478,7 +478,7 @@ let error_no_relation () = user_err Pp.(str "Cannot find a relation to rewrite."
let rec decompose_app_rel env evd t =
(* Head normalize for compatibility with the old meta mechanism *)
- let t = Reductionops.whd_betaiota evd t in
+ let t = Reductionops.whd_betaiota env evd t in
match EConstr.kind evd t with
| App (f, [||]) -> assert false
| App (f, [|arg|]) ->
@@ -711,7 +711,7 @@ let unify_eqn (car, rel, prf, c1, c2, holes, sort) l2r flags env (sigma, cstrs)
let sigma = Typeclasses.resolve_typeclasses ~filter:(no_constraints cstrs)
~fail:true env sigma in
let evd = solve_remaining_by env sigma holes by in
- let nf c = Reductionops.nf_evar evd (Reductionops.nf_meta evd c) in
+ let nf c = Reductionops.nf_evar evd (Reductionops.nf_meta env evd c) in
let c1 = nf c1 and c2 = nf c2
and rew_car = nf car and rel = nf rel
and prf = nf prf in
@@ -971,7 +971,7 @@ let unfold_match env sigma sk app =
| App (f', args) when Constant.equal (fst (destConst sigma f')) sk ->
let v = Environ.constant_value_in (Global.env ()) (sk,Univ.Instance.empty)(*FIXME*) in
let v = EConstr.of_constr v in
- Reductionops.whd_beta sigma (mkApp (v, args))
+ Reductionops.whd_beta env sigma (mkApp (v, args))
| _ -> app
let is_rew_cast = function RewCast _ -> true | _ -> false
@@ -1894,10 +1894,10 @@ let declare_projection name instance_id r =
in it_mkProd_or_LetIn ccl ctx
in
let types = Some (it_mkProd_or_LetIn typ ctx) in
- let kind, opaque, scope = Decls.(IsDefinition Definition), false, DeclareDef.Global Declare.ImportDefaultBehavior in
+ let kind, opaque, scope = Decls.(IsDefinition Definition), false, Declare.Global Declare.ImportDefaultBehavior in
let impargs, udecl = [], UState.default_univ_decl in
let _r : GlobRef.t =
- DeclareDef.declare_definition ~name ~scope ~kind ~opaque ~impargs ~udecl ~poly ~types ~body sigma
+ Declare.declare_definition ~name ~scope ~kind ~opaque ~impargs ~udecl ~poly ~types ~body sigma
in ()
let build_morphism_signature env sigma m =
@@ -1961,10 +1961,10 @@ let add_morphism_as_parameter atts m n : unit =
let env = Global.env () in
let evd = Evd.from_env env in
let poly = atts.polymorphic in
- let kind, opaque, scope = Decls.(IsAssumption Logical), false, DeclareDef.Global Declare.ImportDefaultBehavior in
+ let kind, opaque, scope = Decls.(IsAssumption Logical), false, Declare.Global Declare.ImportDefaultBehavior in
let impargs, udecl = [], UState.default_univ_decl in
let evd, types = build_morphism_signature env evd m in
- let evd, pe = DeclareDef.prepare_parameter ~poly ~udecl ~types evd in
+ let evd, pe = Declare.prepare_parameter ~poly ~udecl ~types evd in
let cst = Declare.declare_constant ~name:instance_id ~kind (Declare.ParameterEntry pe) in
let cst = GlobRef.ConstRef cst in
Classes.add_instance
@@ -1981,7 +1981,7 @@ let add_morphism_interactive atts m n : Lemmas.t =
let poly = atts.polymorphic in
let kind = Decls.(IsDefinition Instance) in
let tac = make_tactic "Coq.Classes.SetoidTactics.add_morphism_tactic" in
- let hook { DeclareDef.Hook.S.dref; _ } = dref |> function
+ let hook { Declare.Hook.S.dref; _ } = dref |> function
| GlobRef.ConstRef cst ->
Classes.add_instance (Classes.mk_instance
(PropGlobal.proper_class env evd) Hints.empty_hint_info
@@ -1989,7 +1989,7 @@ let add_morphism_interactive atts m n : Lemmas.t =
declare_projection n instance_id (GlobRef.ConstRef cst)
| _ -> assert false
in
- let hook = DeclareDef.Hook.make hook in
+ let hook = Declare.Hook.make hook in
let info = Lemmas.Info.make ~hook ~kind () in
Flags.silently
(fun () ->
diff --git a/plugins/ltac/taccoerce.ml b/plugins/ltac/taccoerce.ml
index 04d85ed390..91d26519b8 100644
--- a/plugins/ltac/taccoerce.ml
+++ b/plugins/ltac/taccoerce.ml
@@ -293,6 +293,13 @@ let coerce_to_evaluable_ref env sigma v =
| VarRef var -> EvalVarRef var
| ConstRef c -> EvalConstRef c
| IndRef _ | ConstructRef _ -> fail ()
+ else if has_type v (topwit wit_smart_global) then
+ let open GlobRef in
+ let r = out_gen (topwit wit_smart_global) v in
+ match r with
+ | VarRef var -> EvalVarRef var
+ | ConstRef c -> EvalConstRef c
+ | IndRef _ | ConstructRef _ -> fail ()
else
match Value.to_constr v with
| Some c when isConst sigma c -> EvalConstRef (fst (destConst sigma c))
diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml
index 9910796d9c..e6c59f446d 100644
--- a/plugins/ltac/tacentries.ml
+++ b/plugins/ltac/tacentries.ml
@@ -683,6 +683,111 @@ let tactic_extend plugin_name tacname ~level ?deprecation sign =
Tacenv.register_ml_tactic ml_tactic_name @@ Array.of_list (List.map eval sign);
Mltop.declare_cache_obj obj plugin_name
+type (_, 'a) ml_ty_sig =
+| MLTyNil : ('a, 'a) ml_ty_sig
+| MLTyArg : ('r, 'a) ml_ty_sig -> (Geninterp.Val.t -> 'r, 'a) ml_ty_sig
+
+let rec ml_sig_len : type r a. (r, a) ml_ty_sig -> int = function
+| MLTyNil -> 0
+| MLTyArg sign -> 1 + ml_sig_len sign
+
+let rec cast_ml : type r a. (r, a) ml_ty_sig -> r -> Geninterp.Val.t list -> a =
+ fun sign f ->
+ match sign with
+ | MLTyNil ->
+ begin function
+ | [] -> f
+ | _ :: _ -> CErrors.anomaly (str "Arity mismatch")
+ end
+ | MLTyArg sign ->
+ function
+ | [] -> CErrors.anomaly (str "Arity mismatch")
+ | arg :: args -> cast_ml sign (f arg) args
+
+let ml_tactic_extend ~plugin ~name ~local ?deprecation sign tac =
+ let open Tacexpr in
+ let tac args _ = cast_ml sign tac args in
+ let ml_tactic_name = { mltac_tactic = name; mltac_plugin = plugin } in
+ let ml = { mltac_name = ml_tactic_name; mltac_index = 0 } in
+ let len = ml_sig_len sign in
+ let args = List.init len (fun i -> Id.of_string (Printf.sprintf "arg%i" i)) in
+ let vars = List.map (fun id -> Name id) args in
+ let args = List.map (fun id -> Reference (Locus.ArgVar (CAst.make id))) args in
+ let body = Tacexpr.TacFun (vars, Tacexpr.TacML (CAst.make (ml, args))) in
+ let id = Names.Id.of_string name in
+ let obj () = Tacenv.register_ltac true local id body ?deprecation in
+ let () = Tacenv.register_ml_tactic ml_tactic_name [|tac|] in
+ Mltop.declare_cache_obj obj plugin
+
+module MLName =
+struct
+ open Tacexpr
+ type t = ml_tactic_name
+ let compare tac1 tac2 =
+ let c = String.compare tac1.mltac_tactic tac2.mltac_tactic in
+ if c = 0 then String.compare tac1.mltac_plugin tac2.mltac_plugin
+ else c
+end
+
+module MLTacMap = Map.Make(MLName)
+
+let ml_table : (Geninterp.Val.t list -> Geninterp.Val.t Ftactic.t) MLTacMap.t ref = ref MLTacMap.empty
+
+type ml_ltac_val = {
+ tacval_tac : Tacexpr.ml_tactic_name;
+ tacval_var : Id.t list;
+}
+
+let in_tacval =
+(* This is a hack to emulate value-returning ML-implemented tactics in Ltac.
+ We use a dummy generic argument to work around the limitations of the Ltac
+ runtime. Indeed, the TacML node needs to return unit values, since it is
+ considered a "tactic" in the runtime. Changing it to allow arbitrary values
+ would require to toggle this status, and thus to make it a "value" node.
+ This would in turn create too much backwards incompatibility. Instead, we
+ piggy back on the TacGeneric node, which by construction is used to return
+ values.
+
+ The trick is to represent a n-ary application of a ML function as a generic
+ argument. We store in the node the name of the tactic and its arity, while
+ giving canonical names to the bound variables of the closure. This trick is
+ already performed in several external developments for specific calls, we
+ make it here generic. The argument should not be used for other purposes, so
+ we only export the registering functions.
+ *)
+ let wit : (Empty.t, ml_ltac_val, Geninterp.Val.t) Genarg.genarg_type =
+ Genarg.create_arg "ltac:val"
+ in
+ (* No need to internalize this ever *)
+ let intern_fun _ e = Empty.abort e in
+ let subst_fun s v = v in
+ let () = Genintern.register_intern0 wit intern_fun in
+ let () = Genintern.register_subst0 wit subst_fun in
+ (* No need to register a value tag for it via register_val0 since we will
+ never access this genarg directly. *)
+ let interp_fun ist tac =
+ let args = List.map (fun id -> Id.Map.get id ist.Geninterp.lfun) tac.tacval_var in
+ let tac = MLTacMap.get tac.tacval_tac !ml_table in
+ tac args
+ in
+ let () = Geninterp.register_interp0 wit interp_fun in
+ (fun v -> Genarg.in_gen (Genarg.Glbwit wit) v)
+
+
+let ml_val_tactic_extend ~plugin ~name ~local ?deprecation sign tac =
+ let open Tacexpr in
+ let tac args = cast_ml sign tac args in
+ let ml_tactic_name = { mltac_tactic = name; mltac_plugin = plugin } in
+ let len = ml_sig_len sign in
+ let vars = List.init len (fun i -> Id.of_string (Printf.sprintf "arg%i" i)) in
+ let body = TacGeneric (in_tacval { tacval_tac = ml_tactic_name; tacval_var = vars }) in
+ let vars = List.map (fun id -> Name id) vars in
+ let body = Tacexpr.TacFun (vars, Tacexpr.TacArg (CAst.make body)) in
+ let id = Names.Id.of_string name in
+ let obj () = Tacenv.register_ltac true local id body ?deprecation in
+ let () = assert (not @@ MLTacMap.mem ml_tactic_name !ml_table) in
+ let () = ml_table := MLTacMap.add ml_tactic_name tac !ml_table in
+ Mltop.declare_cache_obj obj plugin
(** ARGUMENT EXTEND *)
diff --git a/plugins/ltac/tacentries.mli b/plugins/ltac/tacentries.mli
index ce38431a18..6ee3ce091b 100644
--- a/plugins/ltac/tacentries.mli
+++ b/plugins/ltac/tacentries.mli
@@ -69,6 +69,25 @@ val print_ltacs : unit -> unit
val print_located_tactic : Libnames.qualid -> unit
(** Display the absolute name of a tactic. *)
+(** {5 Low-level registering of tactics} *)
+
+type (_, 'a) ml_ty_sig =
+| MLTyNil : ('a, 'a) ml_ty_sig
+| MLTyArg : ('r, 'a) ml_ty_sig -> (Geninterp.Val.t -> 'r, 'a) ml_ty_sig
+
+val ml_tactic_extend : plugin:string -> name:string -> local:locality_flag ->
+ ?deprecation:Deprecation.t -> ('r, unit Proofview.tactic) ml_ty_sig -> 'r -> unit
+(** Helper function to define directly an Ltac function in OCaml without any
+ associated parsing rule nor further shenanigans. The Ltac function will be
+ defined as [name] in the Coq file that loads the ML plugin where this
+ function is called. It will have the arity given by the [ml_ty_sig]
+ argument. *)
+
+val ml_val_tactic_extend : plugin:string -> name:string -> local:locality_flag ->
+ ?deprecation:Deprecation.t -> ('r, Geninterp.Val.t Ftactic.t) ml_ty_sig -> 'r -> unit
+(** Same as {!ml_tactic_extend} but the function can return an argument
+ instead. *)
+
(** {5 TACTIC EXTEND} *)
type _ ty_sig =
diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml
index 597c3fdaac..53dc518bd3 100644
--- a/plugins/ltac/tacintern.ml
+++ b/plugins/ltac/tacintern.ml
@@ -14,7 +14,6 @@ open CAst
open Pattern
open Genredexpr
open Glob_term
-open Tacred
open Util
open Names
open Libnames
@@ -95,9 +94,16 @@ let intern_string_or_var = intern_or_var (fun (s : string) -> s)
let intern_global_reference ist qid =
if qualid_is_ident qid && find_var (qualid_basename qid) ist then
ArgVar (make ?loc:qid.CAst.loc @@ qualid_basename qid)
- else
- try ArgArg (qid.CAst.loc,locate_global_with_alias qid)
- with Not_found -> Nametab.error_global_not_found qid
+ else if qualid_is_ident qid && find_hyp (qualid_basename qid) ist then
+ let id = qualid_basename qid in
+ ArgArg (qid.CAst.loc, GlobRef.VarRef id)
+ else match locate_global_with_alias ~head:true qid with
+ | r -> ArgArg (qid.CAst.loc, r)
+ | exception Not_found ->
+ if not !strict_check && qualid_is_ident qid then
+ let id = qualid_basename qid in
+ ArgArg (qid.CAst.loc, GlobRef.VarRef id)
+ else Nametab.error_global_not_found qid
let intern_ltac_variable ist qid =
if qualid_is_ident qid && find_var (qualid_basename qid) ist then
@@ -287,38 +293,42 @@ let intern_destruction_arg ist = function
else
clear,ElimOnIdent (make ?loc id)
-let short_name = function
- | {v=AN qid} when qualid_is_ident qid && not !strict_check ->
+let short_name qid =
+ if qualid_is_ident qid && not !strict_check then
Some (make ?loc:qid.CAst.loc @@ qualid_basename qid)
- | _ -> None
-
-let intern_evaluable_global_reference ist qid =
- try evaluable_of_global_reference ist.genv (locate_global_with_alias ~head:true qid)
- with Not_found ->
- if qualid_is_ident qid && not !strict_check then EvalVarRef (qualid_basename qid)
- else Nametab.error_global_not_found qid
+ else None
+
+let evalref_of_globref ?loc ?short = function
+ | GlobRef.ConstRef cst -> ArgArg (EvalConstRef cst, short)
+ | GlobRef.VarRef id -> ArgArg (EvalVarRef id, short)
+ | r ->
+ let tpe = match r with
+ | GlobRef.IndRef _ -> "inductive"
+ | GlobRef.ConstructRef _ -> "constructor"
+ | (GlobRef.VarRef _ | GlobRef.ConstRef _) -> assert false
+ in
+ user_err ?loc (str "Cannot turn" ++ spc () ++ str tpe ++ spc () ++
+ Nametab.pr_global_env Id.Set.empty r ++ spc () ++
+ str "into an evaluable reference.")
+
+let intern_evaluable ist = function
+ | {v=AN qid} ->
+ begin match intern_global_reference ist qid with
+ | ArgVar _ as v -> v
+ | ArgArg (loc, r) ->
+ let short = short_name qid in
+ evalref_of_globref ?loc ?short r
+ end
+ | {v=ByNotation (ntn,sc);loc} ->
+ let check = GlobRef.(function ConstRef _ | VarRef _ -> true | _ -> false) in
+ let r = Notation.interp_notation_as_global_reference ?loc ~head:true check ntn sc in
+ evalref_of_globref ?loc r
-let intern_evaluable_reference_or_by_notation ist = function
- | {v=AN r} -> intern_evaluable_global_reference ist r
+let intern_smart_global ist = function
+ | {v=AN r} -> intern_global_reference ist r
| {v=ByNotation (ntn,sc);loc} ->
- evaluable_of_global_reference ist.genv
- (Notation.interp_notation_as_global_reference ?loc
- GlobRef.(function ConstRef _ | VarRef _ -> true | _ -> false) ntn sc)
-
-(* Globalize a reduction expression *)
-let intern_evaluable ist r =
- let f ist r =
- let e = intern_evaluable_reference_or_by_notation ist r in
- let na = short_name r in
- ArgArg (e,na)
- in
- match r with
- | {v=AN qid} when qualid_is_ident qid && find_var (qualid_basename qid) ist ->
- ArgVar (make ?loc:qid.CAst.loc @@ qualid_basename qid)
- | {v=AN qid} when qualid_is_ident qid && not !strict_check && find_hyp (qualid_basename qid) ist ->
- let id = qualid_basename qid in
- ArgArg (EvalVarRef id, Some (make ?loc:qid.CAst.loc id))
- | _ -> f ist r
+ ArgArg (loc, (Notation.interp_notation_as_global_reference ?loc ~head:true
+ GlobRef.(function ConstRef _ | VarRef _ -> true | _ -> false) ntn sc))
let intern_unfold ist (l,qid) = (l,intern_evaluable ist qid)
@@ -380,10 +390,10 @@ let intern_typed_pattern_or_ref_with_occurrences ist (l,p) =
let c = Constrintern.interp_reference sign r in
match DAst.get c with
| GRef (r,None) ->
- Inl (ArgArg (evaluable_of_global_reference ist.genv r,None))
+ Inl (evalref_of_globref r)
| GVar id ->
- let r = evaluable_of_global_reference ist.genv (GlobRef.VarRef id) in
- Inl (ArgArg (r,None))
+ let r = evalref_of_globref (GlobRef.VarRef id) in
+ Inl r
| _ ->
let bound_names = Glob_ops.bound_glob_vars c in
Inr (bound_names,(c,None),dummy_pat) in
@@ -813,6 +823,7 @@ let intern_ltac ist tac =
let () =
Genintern.register_intern0 wit_int_or_var (lift intern_int_or_var);
+ Genintern.register_intern0 wit_smart_global (lift intern_smart_global);
Genintern.register_intern0 wit_ref (lift intern_global_reference);
Genintern.register_intern0 wit_pre_ident (fun ist c -> (ist,c));
Genintern.register_intern0 wit_ident intern_ident';
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index dda7f0742c..6d350ade8d 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -162,17 +162,27 @@ let catching_error call_trace fail (e, info) =
fail located_exc
end
-let catch_error call_trace f x =
+let update_loc ?loc (e, info) =
+ (e, Option.cata (Loc.add_loc info) info loc)
+
+let catch_error ?loc call_trace f x =
try f x
with e when CErrors.noncritical e ->
let e = Exninfo.capture e in
+ let e = update_loc ?loc e in
catching_error call_trace Exninfo.iraise e
-let wrap_error tac k =
- if is_traced () then Proofview.tclORELSE tac k else tac
+let catch_error_loc ?loc tac =
+ Proofview.tclOR tac (fun exn ->
+ let (e, info) = update_loc ?loc exn in
+ Proofview.tclZERO ~info e)
+
+let wrap_error ?loc tac k =
+ if is_traced () then Proofview.tclORELSE tac k
+ else catch_error_loc ?loc tac
-let catch_error_tac call_trace tac =
- wrap_error
+let catch_error_tac ?loc call_trace tac =
+ wrap_error ?loc
tac
(catching_error call_trace (fun (e, info) -> Proofview.tclZERO ~info e))
@@ -535,9 +545,10 @@ let interp_gen kind ist pattern_mode flags env sigma c =
ltac_idents = constrvars.idents;
ltac_genargs = ist.lfun;
} in
- let trace = push_trace (loc_of_glob_constr term,LtacConstrInterp (term,vars)) ist in
+ let loc = loc_of_glob_constr term in
+ let trace = push_trace (loc,LtacConstrInterp (term,vars)) ist in
let (evd,c) =
- catch_error trace (understand_ltac flags env sigma vars kind) term
+ catch_error ?loc trace (understand_ltac flags env sigma vars kind) term
in
(* spiwack: to avoid unnecessary modifications of tacinterp, as this
function already use effect, I call [run] hoping it doesn't mess
@@ -1059,7 +1070,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
let call = LtacAtomCall t in
let trace = push_trace(loc,call) ist in
Profile_ltac.do_profile "eval_tactic:2" trace
- (catch_error_tac trace (interp_atomic ist t))
+ (catch_error_tac ?loc trace (interp_atomic ist t))
| TacFun _ | TacLetIn _ | TacMatchGoal _ | TacMatch _ -> interp_tactic ist tac
| TacId [] -> Proofview.tclLIFT (db_breakpoint (curr_debug ist) [])
| TacId s ->
@@ -1087,7 +1098,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
| TacShowHyps tac ->
Proofview.V82.tactic begin
tclSHOWHYPS (Proofview.V82.of_tactic (interp_tactic ist tac))
- end
+ end [@ocaml.warning "-3"]
| TacAbstract (t,ido) ->
let call = LtacMLCall tac in
let trace = push_trace(None,call) ist in
@@ -1149,7 +1160,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
; poly
; extra = TacStore.set ist.extra f_trace trace } in
val_interp ist alias.Tacenv.alias_body >>= fun v ->
- Ftactic.lift (tactic_of_value ist v)
+ Ftactic.lift (catch_error_loc ?loc (tactic_of_value ist v))
in
let tac =
Ftactic.with_env interp_vars >>= fun (env, lr) ->
@@ -1175,7 +1186,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
let args = Ftactic.List.map_right (fun a -> interp_tacarg ist a) l in
let tac args =
let name _ _ = Pptactic.pr_extend (fun v -> print_top_val () v) 0 opn args in
- Proofview.Trace.name_tactic name (catch_error_tac trace (tac args ist))
+ Proofview.Trace.name_tactic name (catch_error_tac ?loc trace (tac args ist))
in
Ftactic.run args tac
@@ -1278,7 +1289,7 @@ and interp_app loc ist fv largs : Val.t Ftactic.t =
; extra = TacStore.set ist.extra f_trace []
} in
Profile_ltac.do_profile "interp_app" trace ~count_call:false
- (catch_error_tac trace (val_interp ist body)) >>= fun v ->
+ (catch_error_tac ?loc trace (val_interp ist body)) >>= fun v ->
Ftactic.return (name_vfun (push_appl appl largs) v)
end
begin fun (e, info) ->
@@ -1895,8 +1906,7 @@ module Value = struct
let closure = VFun (UnnamedAppl,extract_trace ist, ist.lfun, [], tac) in
of_tacvalue closure
- (** Apply toplevel tactic values *)
- let apply (f : value) (args: value list) =
+ let apply_expr f args =
let fold arg (i, vars, lfun) =
let id = Id.of_string ("x" ^ string_of_int i) in
let x = Reference (ArgVar CAst.(make id)) in
@@ -1905,9 +1915,18 @@ module Value = struct
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 ist = { (default_ist ()) with lfun = lfun; } in
- let tac = TacArg(CAst.make @@ TacCall (CAst.make (ArgVar CAst.(make @@ Id.of_string "F"),args))) in
+ ist, TacArg(CAst.make @@ TacCall (CAst.make (ArgVar CAst.(make @@ Id.of_string "F"),args)))
+
+
+ (** Apply toplevel tactic values *)
+ let apply (f : value) (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 ist, tac = apply_expr f args in
+ val_interp ist tac
+
end
(* globalization + interpretation *)
@@ -2014,6 +2033,7 @@ let interp_pre_ident ist env sigma s =
let () =
register_interp0 wit_int_or_var (fun ist n -> Ftactic.return (interp_int_or_var ist n));
+ register_interp0 wit_smart_global (lift interp_reference);
register_interp0 wit_ref (lift interp_reference);
register_interp0 wit_pre_ident (lift interp_pre_ident);
register_interp0 wit_ident (lift interp_ident);
diff --git a/plugins/ltac/tacinterp.mli b/plugins/ltac/tacinterp.mli
index ce34356a37..cbb17bf0fa 100644
--- a/plugins/ltac/tacinterp.mli
+++ b/plugins/ltac/tacinterp.mli
@@ -29,6 +29,7 @@ sig
val of_closure : Geninterp.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
end
(** Values for interpretation *)
diff --git a/plugins/ltac/tacsubst.ml b/plugins/ltac/tacsubst.ml
index 600c30b403..ed298b7e66 100644
--- a/plugins/ltac/tacsubst.ml
+++ b/plugins/ltac/tacsubst.ml
@@ -280,6 +280,7 @@ and subst_genarg subst (GenArg (Glbwit wit, x)) =
let () =
Genintern.register_subst0 wit_int_or_var (fun _ v -> v);
Genintern.register_subst0 wit_ref subst_global_reference;
+ Genintern.register_subst0 wit_smart_global subst_global_reference;
Genintern.register_subst0 wit_pre_ident (fun _ v -> v);
Genintern.register_subst0 wit_ident (fun _ v -> v);
Genintern.register_subst0 wit_var (fun _ v -> v);
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-30 10:22:02 +0000