Skip to content

Commit a93953f

Browse files
garesgares
committed
coq.ltac.call-mltac
1 parent 63c47a6 commit a93953f

File tree

4 files changed

+136
-27
lines changed

4 files changed

+136
-27
lines changed

‎Changelog.md‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -11,6 +11,8 @@
1111
first class in Rocq 10
1212
- Rename `coq.env.section`, use `coq.env.section-variables`
1313
- New `coq.env.section-contents` listing the contents of sections.
14+
- New `coq.ltac.call-mltac` to call code defined via `TACTIC EXTEND` directives
15+
in OCaml.
1416

1517
# [3.2.0] 19/09/2025
1618

‎builtin-doc/coq-builtin.elpi‎

Lines changed: 26 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -755,8 +755,8 @@ external func coq.env.module-type modtypath -> list id.
755755
external func coq.env.section-variables -> list constant.
756756

757757
% [coq.env.section-contents GlobalObjects] lists the global objects that are
758-
% defined withing the current section
759-
external func coq.env.section-contents -> list gref.
758+
% defined withing the open sections. Inner section first.
759+
external func coq.env.section-contents -> list (list gref).
760760

761761
% Deprecated, use coq.env.section-variables
762762
func coq.env.section -> list constant.
@@ -1646,6 +1646,30 @@ external type coq.ltac.fail int -> variadic any (func).
16461646
external func coq.ltac.collect-goals term -> list sealed-goal,
16471647
list sealed-goal.
16481648

1649+
% [coq.ltac.call-mltac PluginName BlockName BlockIndex G GL] Calls OCaml
1650+
% code bound via TACTIC EXTEND. For example the
1651+
% OCaml code for lia looks like:
1652+
%
1653+
% DECLARE PLUGIN "rocq-runtime.plugins.micromega"
1654+
% ...
1655+
% TACTIC EXTEND Lia
1656+
% | [ "xlia" tactic(t) ] -> { Coq_micromega.xlia
1657+
% (Tacinterp.tactic_of_value ist t) }
1658+
% END
1659+
%
1660+
% In order to call the code between curly braces one has to run
1661+
%
1662+
% coq.ltac.call-mltac "rocq-runtime.plugins.micromega" "Lia" 0 G GL
1663+
%
1664+
% Note that each TACTIC EXTEND block can have many entries and their
1665+
% numbering
1666+
% starts from 0. Also, each block has a name, "Lia" in this case.
1667+
%
1668+
% Supported attributes:
1669+
% - @no-tc! (default false, do not infer typeclasses)
1670+
external func coq.ltac.call-mltac string, string, int,
1671+
goal -> list sealed-goal.
1672+
16491673
% [coq.ltac.call-ltac1 Tac G GL] Calls Ltac1 tactic Tac on goal G (passing
16501674
% the arguments of G, see coq.ltac.call for a handy wrapper).
16511675
% Tac can either be a string (the tactic name), or a value

‎src/rocq_elpi_builtins.ml‎

Lines changed: 74 additions & 25 deletions
Original file line numberDiff line numberDiff line change
@@ -1561,6 +1561,32 @@ let apply_proof ~name ~poly env tac pf =
15611561
pv
15621562
[%%endif]
15631563

1564+
let call_tactic ~depth state ~no_tc proof_context goal tactic =
1565+
let sigma = get_sigma state in
1566+
let sigma, subgoals =
1567+
let open Proofview in let open Notations in
1568+
let focused_tac =
1569+
Unsafe.tclSETGOALS [with_empty_state goal] <*> tactic in
1570+
with_no_tc ~no_tc (fun sigma ->
1571+
let _, pv = init sigma [] in
1572+
let pv =
1573+
let vernac_state = Vernacstate.freeze_full_state () in
1574+
try
1575+
let rc = apply_proof ~name:(Id.of_string "elpi") ~poly:default_polyflags proof_context.env focused_tac pv in
1576+
let pstate = Vernacstate.Stm.pstate (Vernacstate.freeze_full_state ()) in
1577+
let vernac_state = Vernacstate.Stm.set_pstate vernac_state pstate in
1578+
Vernacstate.unfreeze_full_state vernac_state;
1579+
rc
1580+
with e when CErrors.noncritical e && false ->
1581+
Vernacstate.unfreeze_full_state vernac_state;
1582+
raise Pred.No_clause
1583+
in
1584+
let subgoals, sigma = proofview pv in
1585+
sigma, subgoals)
1586+
sigma in
1587+
Declare.Internal.export_side_effects (Evd.eval_side_effects sigma);
1588+
let state, assignments = set_current_sigma ~depth state sigma in
1589+
state, subgoals, assignments
15641590

15651591
[%%if coq = "9.0"]
15661592
let section_close_section x =
@@ -4060,6 +4086,52 @@ fold_left over the terms, letin body comes before the type).
40604086
)),
40614087
DocAbove);
40624088

4089+
MLCode(Pred("coq.ltac.call-mltac",
4090+
In(B.string, "PluginName",
4091+
In(B.string, "BlockName",
4092+
In(B.int, "BlockIndex",
4093+
CIn(goal, "G",
4094+
Out(list sealed_goal,"GL",
4095+
Full(raw_ctx, {|Calls OCaml code bound via TACTIC EXTEND. For example the
4096+
OCaml code for lia looks like:
4097+
4098+
DECLARE PLUGIN "rocq-runtime.plugins.micromega"
4099+
...
4100+
TACTIC EXTEND Lia
4101+
| [ "xlia" tactic(t) ] -> { Coq_micromega.xlia (Tacinterp.tactic_of_value ist t) }
4102+
END
4103+
4104+
In order to call the code between curly braces one has to run
4105+
4106+
coq.ltac.call-mltac "rocq-runtime.plugins.micromega" "Lia" 0 G GL
4107+
4108+
Note that each TACTIC EXTEND block can have many entries and their numbering
4109+
starts from 0. Also, each block has a name, "Lia" in this case.
4110+
4111+
Supported attributes:
4112+
- @no-tc! (default false, do not infer typeclasses)|})))))),
4113+
(fun plugin block index (proof_context,goal,tac_args) _ ~depth _ _ -> abstract__grab_global_env_keep_sigma "coq.ltac.call-ltac1" (fun state ->
4114+
let no_tc = if proof_context.options.no_tc = Some true then true else false in
4115+
let open Ltac_plugin in
4116+
4117+
let tac_args = tac_args |> List.map (function
4118+
| Rocq_elpi_arg_HOAS.Ctrm t -> Tacinterp.Value.of_constr t
4119+
| Rocq_elpi_arg_HOAS.Cstr s -> Geninterp.(Val.inject (val_tag (Genarg.topwit Stdarg.wit_string))) s
4120+
| Rocq_elpi_arg_HOAS.Cint i -> Tacinterp.Value.of_int i
4121+
| Rocq_elpi_arg_HOAS.CLtac1 x -> Geninterp.(Val.inject (val_tag (Topwit Ltac_plugin.Tacarg.wit_tactic))) x) in
4122+
let tactic =
4123+
let tacname = Tacexpr.{ mltac_name = { mltac_plugin = plugin; mltac_tactic = block; }; mltac_index = index } in
4124+
Tacenv.interp_ml_tactic tacname tac_args (Tacinterp.default_ist ()) in
4125+
4126+
let state, subgoals, assignments =
4127+
call_tactic ~depth state ~no_tc proof_context goal tactic in
4128+
4129+
(* universe constraints fixed by the code above*)
4130+
Univ.ContextSet.empty, state, !: subgoals, assignments
4131+
))),
4132+
DocAbove);
4133+
4134+
40634135
MLCode(Pred("coq.ltac.call-ltac1",
40644136
In(B.any, "Tac",
40654137
CIn(goal, "G",
@@ -4079,7 +4151,6 @@ Supported attributes:
40794151
(fun tac (proof_context,goal,tac_args) _ ~depth _ _ -> abstract__grab_global_env_keep_sigma "coq.ltac.call-ltac1" (fun state ->
40804152
let no_tc = if proof_context.options.no_tc = Some true then true else false in
40814153
let open Ltac_plugin in
4082-
let sigma = get_sigma state in
40834154

40844155
let tac_args = tac_args |> List.map (function
40854156
| Rocq_elpi_arg_HOAS.Ctrm t -> Tacinterp.Value.of_constr t
@@ -4107,31 +4178,9 @@ Supported attributes:
41074178
| _ -> U.type_error ("coq.ltac.call-ltac1: string or ltac1-tactic are expected as the tactic to call")
41084179
in
41094180
Tacinterp.Value.apply tac tac_args in
4110-
let sigma, subgoals =
4111-
let open Proofview in let open Notations in
4112-
let focused_tac =
4113-
Unsafe.tclSETGOALS [with_empty_state goal] <*> tactic in
4114-
with_no_tc ~no_tc (fun sigma ->
4115-
let _, pv = init sigma [] in
4116-
let pv =
4117-
let vernac_state = Vernacstate.freeze_full_state () in
4118-
try
4119-
let rc = apply_proof ~name:(Id.of_string "elpi") ~poly:default_polyflags proof_context.env focused_tac pv in
4120-
let pstate = Vernacstate.Stm.pstate (Vernacstate.freeze_full_state ()) in
4121-
let vernac_state = Vernacstate.Stm.set_pstate vernac_state pstate in
4122-
Vernacstate.unfreeze_full_state vernac_state;
4123-
rc
4124-
with e when CErrors.noncritical e ->
4125-
Vernacstate.unfreeze_full_state vernac_state;
4126-
raise Pred.No_clause
4127-
in
4128-
let subgoals, sigma = proofview pv in
4129-
sigma, subgoals)
4130-
sigma in
4131-
4132-
Declare.Internal.export_side_effects (Evd.eval_side_effects sigma);
41334181

4134-
let state, assignments = set_current_sigma ~depth state sigma in
4182+
let state, subgoals, assignments =
4183+
call_tactic ~depth state ~no_tc proof_context goal tactic in
41354184

41364185
(* universe constraints fixed by the code above*)
41374186
Univ.ContextSet.empty, state, !: subgoals, assignments

‎tests-stdlib/test_ring.v‎

Lines changed: 34 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,34 @@
1+
From elpi Require Import elpi.
2+
From Stdlib Require Import ZArith Lia.
3+
4+
(* we test we can call ML tactics *)
5+
6+
Elpi Tactic xlia.
7+
Elpi Accumulate lp:{{
8+
solve G GL :- coq.ltac.call-mltac "rocq-runtime.plugins.micromega" "Lia" 0 G GL.
9+
}}.
10+
Tactic Notation "mylia" :=
11+
Zify.zify; elpi xlia ltac_tactic:(zchecker).
12+
13+
Open Scope Z.
14+
15+
Goal 0 = 0 :> Z.
16+
mylia.
17+
Qed.
18+
19+
From Stdlib Require Import Ring.
20+
21+
Ltac xx rl :=
22+
let G := Get_goal in
23+
ring_lookup (PackRing Ring_simplify) [] rl G.
24+
25+
Elpi Tactic test.
26+
Elpi Accumulate lp:{{
27+
solve (goal C R T E []) GL :- coq.ltac.call-ltac1 "xx" (goal C R T E [trm {{ 0 + 0 }}]) GL.
28+
}}.
29+
30+
Goal forall f, 0 = f (0 + 0) :> Z.
31+
intro f.
32+
elpi test.
33+
match goal with |- 0 = f 0 => idtac end.
34+
Abort.

0 commit comments

Comments
 (0)