Skip to content

Commit

Permalink
wip
Browse files Browse the repository at this point in the history
  • Loading branch information
@gares
gares committed Sep 28, 2023
1 parent 1407081 commit bd21758
Show file tree
Hide file tree
Showing 7 changed files with 131 additions and 37 deletions.
9 changes: 8 additions & 1 deletion coq-builtin.elpi
View file
Original file line number Diff line number Diff line change
Expand Up @@ -52,6 +52,9 @@ type int int -> argument. % Eg. 1 -2.
type str string -> argument. % Eg. x "y" z.w. or any Coq keyword/symbol
type trm term -> argument. % Eg. (t).

% Extra arguments for tactics
type tac ltac-thunk -> argument.

% Extra arguments for commands. [Definition], [Axiom], [Record] and [Context]
% take precedence over the [str] argument above (when not "quoted").
%
Expand Down Expand Up @@ -1521,6 +1524,10 @@ external pred coq.strategy.get i:constant, o:conversion_strategy.

% -- Coq's tactics --------------------------------------------

% Ltac1 thunk
typeabbrev ltac1-thunk (ctype "ltac1-thunk").


% [coq.ltac.fail Level ...] Interrupts the Elpi program and calls Ltac's
% fail Level Msg, where Msg is the printing of the remaining arguments.
% Level can be left unspecified and defaults to 0
Expand All @@ -1540,7 +1547,7 @@ external pred coq.ltac.collect-goals i:term, o:list sealed-goal,

% [coq.ltac.call-ltac1 Tac G GL] Calls Ltac1 tactic named Tac on goal G
% (passing the arguments of G, see coq.ltac.call for a handy wrapper)
external pred coq.ltac.call-ltac1 i:string, i:goal, o:list sealed-goal.
external pred coq.ltac.call-ltac1 i:any, i:goal, o:list sealed-goal.

% [coq.ltac.id-free? ID G]
% Fails if ID is already used in G. Note that ids which are taken are
Expand Down
3 changes: 3 additions & 0 deletions elpi/coq-HOAS.elpi
View file
Original file line number Diff line number Diff line change
Expand Up @@ -37,6 +37,9 @@ type int int -> argument. % Eg. 1 -2.
type str string -> argument. % Eg. x "y" z.w. or any Coq keyword/symbol
type trm term -> argument. % Eg. (t).

% Extra arguments for tactics
type tac ltac-thunk -> argument.

% Extra arguments for commands. [Definition], [Axiom], [Record] and [Context]
% take precedence over the [str] argument above (when not "quoted").
%
Expand Down
62 changes: 51 additions & 11 deletions src/coq_elpi_arg_HOAS.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -407,27 +407,37 @@ type raw_ltac_term = Constrexpr.constr_expr
type glob_ltac_term = Glob_term.glob_constr
type top_ltac_term = Geninterp.interp_sign * Names.Id.t

type raw_ltac_thunk = Ltac_plugin.Tacexpr.raw_tactic_expr
type glob_ltac_thunk = Ltac_plugin.Tacexpr.glob_tactic_expr
type top_ltac_thunk = Geninterp.Val.t

type ltac_ty = Int | String | Term | List of ltac_ty

type ('a,'f) t =
| Int : int -> ('a,'f) t
| String : string -> ('a,'f) t
| Term : 'a -> ('a,'f) t
| LTac : ltac_ty * 'f -> ('a,'f) t
type ('a,'f,'t) t =
| Int : int -> ('a,'f,'t) t
| String : string -> ('a,'f,'t) t
| Term : 'a -> ('a,'f,'t) t
| LTac : ltac_ty * 'f -> ('a,'f,'t) t
| LTacThunk : 't -> ('a,'f,'t) t

type raw = (raw_term, raw_ltac_term) t
type glob = (glob_term, glob_ltac_term) t
type top = (top_term, top_ltac_term) t
type raw = (raw_term, raw_ltac_term, raw_ltac_thunk) t
type glob = (glob_term, glob_ltac_term, glob_ltac_thunk) t
type top = (top_term, top_ltac_term, top_ltac_thunk) t

let pr_raw_ltac_arg _ _ _ = Pp.str "TODO: pr_raw_ltac_arg"
let pr_glob_ltac_arg _ _ _ = Pp.str "TODO: pr_glob_ltac_arg"
let pr_top_ltac_arg _ _ _ = Pp.str "TODO: pr_top_ltac_arg"

let pr_arg f k x = match x with
let pr_raw_ltac_thunk _ _ _ = Pp.str "TODO: pr_raw_ltac_thunk"
let pr_glob_ltac_thunk _ _ _ = Pp.str "TODO: pr_glob_ltac_thunk"
let pr_top_ltac_thunk _ _ _ = Pp.str "TODO: pr_top_ltac_thunk"

let pr_arg f k t x = match x with
| Int n -> Pp.int n
| String s -> Pp.qstring s
| Term s -> f s
| LTac(_, s) -> k s
| LTacThunk s -> t s

let pr_glob_constr_and_expr env sigma = function
| (_, Some c) ->
Expand All @@ -441,22 +451,26 @@ let pp_raw env sigma : raw -> Pp.t =
pr_arg
(Ppconstr.pr_constr_expr env sigma)
(pr_raw_ltac_arg env sigma)
(pr_raw_ltac_thunk env sigma)

let pp_glob env sigma =
pr_arg
(pr_glob_constr_and_expr env sigma)
(pr_glob_ltac_arg env sigma)
(pr_glob_ltac_thunk env sigma)

let pp_top env sigma : top -> Pp.t =
pr_arg
((fun (_,x) -> pr_glob_constr_and_expr env sigma x))
(pr_top_ltac_arg env sigma)
(pr_top_ltac_thunk env sigma)

let glob glob_sign : raw -> _ * glob = function
| Int _ as x -> glob_sign, x
| String _ as x -> glob_sign, x
| Term t -> glob_sign, Term (intern_tactic_constr glob_sign t)
| LTac(ty,t) -> glob_sign, LTac (ty,fst @@ intern_tactic_constr glob_sign t)
| LTacThunk t -> glob_sign, LTacThunk (Ltac_plugin.Tacintern.glob_tactic t)

let subst mod_subst = function
| Int _ as x -> x
Expand All @@ -465,7 +479,9 @@ let subst mod_subst = function
Term (Ltac_plugin.Tacsubst.subst_glob_constr_and_expr mod_subst t)
| LTac(ty,t) ->
LTac(ty,(Detyping.subst_glob_constr (Global.env()) mod_subst t))

| LTacThunk t ->
LTacThunk (Ltac_plugin.Tacsubst.subst_tactic mod_subst t)

let interp return ist = function
| Int _ as x -> return x
| String _ as x -> return x
Expand All @@ -476,6 +492,7 @@ let interp return ist = function
| Glob_term.GVar id -> id
| _ -> assert false in
return @@ LTac(ty,(ist,id))
| LTacThunk t -> return @@ LTacThunk (Ltac_plugin.Tacinterp.Value.of_closure ist t)


let add_genarg tag pr_raw pr_glob pr_top glob subst interp =
Expand Down Expand Up @@ -636,6 +653,7 @@ let rec do_context_constr coq_ctx csts fields ~depth state =

let strc = E.Constants.declare_global_symbol "str"
let trmc = E.Constants.declare_global_symbol "trm"
let tacc = E.Constants.declare_global_symbol "tac"
let intc = E.Constants.declare_global_symbol "int"
let ctxc = E.Constants.declare_global_symbol "ctx-decl"

Expand Down Expand Up @@ -735,9 +753,23 @@ let rec in_elpi_ltac_arg ~depth ?calldepth coq_ctx hyps sigma state ty ist v =
with Taccoerce.CannotCoerceTo _ ->
raise (Taccoerce.CannotCoerceTo "a term")

let { CD.cin = of_ltac_thunk; isc = is_ltac_thunk; cout = to_ltac_thunk }, tac = CD.declare {
CD.name = "ltac1-thunk";
doc = "Ltac1 thunk";
pp = (fun fmt _ -> Format.fprintf fmt "<tactic>");
compare = (fun a b -> 0);
hash = (fun x -> Hashtbl.hash x);
hconsed = false;
constants = [];
}

let in_elpi_ltac_thunk ~depth ?calldepth coq_ctx hyps sigma state t =
state, [E.mkApp tacc (of_ltac_thunk t) []], []

let in_elpi_tac ~depth ?calldepth coq_ctx hyps sigma state x =
let open Tac in
match x with
| LTacThunk t -> in_elpi_ltac_thunk ~depth ?calldepth coq_ctx hyps sigma state t
| LTac(ty,(ist,id)) ->
let v = try Id.Map.find id ist.Geninterp.lfun with Not_found -> assert false in
begin try
Expand Down Expand Up @@ -828,7 +860,7 @@ let in_elpi_cmd ~depth ?calldepth coq_ctx state ~raw (x : Cmd.top) =
let sigma = get_sigma state in
in_elpi_elab_term_arg ~depth ?calldepth state coq_ctx hyps sigma ist glob_or_expr

type coq_arg = Cint of int | Cstr of string | Ctrm of EConstr.t
type coq_arg = Cint of int | Cstr of string | Ctrm of EConstr.t | Cltac of Geninterp.Val.t

let in_coq_arg ~depth proof_context constraints state t =
match E.look ~depth t with
Expand All @@ -845,5 +877,13 @@ let in_coq_arg ~depth proof_context constraints state t =
| E.App(c,t,[]) when c == trmc ->
let state, t, gls = lp2constr ~depth proof_context constraints state t in
state, Ctrm t, gls
| E.App(c,t,[]) when c == trmc ->
let state, t, gls = lp2constr ~depth proof_context constraints state t in
state, Ctrm t, gls
| E.App(c,t,[]) when c == tacc ->
begin match E.look ~depth t with
| E.CData c when is_ltac_thunk c -> state, Cltac (to_ltac_thunk c), []
| _ -> raise API.Conversion.(TypeErr (TyName"argument",depth,t))
end
| _ -> raise API.Conversion.(TypeErr (TyName"argument",depth,t))

27 changes: 18 additions & 9 deletions src/coq_elpi_arg_HOAS.mli
View file
Original file line number Diff line number Diff line change
Expand Up @@ -68,23 +68,32 @@ type raw_ltac_term = Constrexpr.constr_expr
type glob_ltac_term = Glob_term.glob_constr
type top_ltac_term = Geninterp.interp_sign * Names.Id.t

type raw_ltac_thunk = Ltac_plugin.Tacexpr.raw_tactic_expr
type glob_ltac_thunk = Ltac_plugin.Tacexpr.glob_tactic_expr
type top_ltac_thunk = Geninterp.Val.t

type ltac_ty = Int | String | Term | List of ltac_ty

type ('a,'f) t =
| Int : int -> ('a,'f) t
| String : string -> ('a,'f) t
| Term : 'a -> ('a,'f) t
| LTac : ltac_ty * 'f -> ('a,'f) t
type ('a,'f,'t) t =
| Int : int -> ('a,'f,'t) t
| String : string -> ('a,'f,'t) t
| Term : 'a -> ('a,'f,'t) t
| LTac : ltac_ty * 'f -> ('a,'f,'t) t
| LTacThunk : 't -> ('a,'f,'t) t

type raw = (raw_term, raw_ltac_term) t
type glob = (glob_term, glob_ltac_term) t
type top = (top_term, top_ltac_term) t
type raw = (raw_term, raw_ltac_term, raw_ltac_thunk) t
type glob = (glob_term, glob_ltac_term, glob_ltac_thunk) t
type top = (top_term, top_ltac_term, top_ltac_thunk) t

val subst : Mod_subst.substitution -> glob -> glob
val wit : (raw, glob, top) Genarg.genarg_type

end

val tac : Tac.top_ltac_thunk Elpi.API.Conversion.t
val is_ltac_thunk : Elpi.API.RawOpaqueData.t -> bool
val to_ltac_thunk : Elpi.API.RawOpaqueData.t -> Tac.top_ltac_thunk

(* for tactics *)
val in_elpi_tac :
depth:int -> ?calldepth:int ->
Expand Down Expand Up @@ -114,7 +123,7 @@ val in_elpi_cmd :
Cmd.top ->
Elpi.API.State.t * term * Elpi.API.Conversion.extra_goals

type coq_arg = Cint of int | Cstr of string | Ctrm of EConstr.t
type coq_arg = Cint of int | Cstr of string | Ctrm of EConstr.t | Cltac of Geninterp.Val.t

val in_coq_arg :
depth:int ->
Expand Down
11 changes: 11 additions & 0 deletions src/coq_elpi_arg_syntax.mlg
View file
Original file line number Diff line number Diff line change
Expand Up @@ -12,6 +12,8 @@ open Gramlib
open Pcoq.Constr
open Pcoq.Prim
open Pvernac.Vernac_
open Tacarg
open Pltac

module EA = Coq_elpi_arg_HOAS
module U = Coq_elpi_utils
Expand Down Expand Up @@ -169,6 +171,9 @@ let of_coq_definition ~loc ~atts name udecl def =
| Vernacexpr.ProveBody _ ->
CErrors.user_err ~loc Pp.(str"syntax error: missing Definition body")

let pr_tac env sigma _prc _prlc prtac c =
prtac env sigma (Constrexpr.LevelLe 0) c

}

GRAMMAR EXTEND Gram
Expand Down Expand Up @@ -258,6 +263,11 @@ GLOB_PRINTED BY { fun _ _ _ -> EA.Cmd.pp_glob env sigma }
| [ coq_kwd_or_symbol(x) ] -> { EA.Cmd.String x }
END

ARGUMENT EXTEND elpi_tactic_thunk
TYPED AS tactic
PRINTED BY { pr_tac env sigma }
| [ ltac_expr(c) ] -> { c }
END

ARGUMENT EXTEND elpi_tactic_arg
TYPED AS elpi_ftactic_arg
Expand All @@ -271,6 +281,7 @@ TYPED AS elpi_ftactic_arg
| [ "ltac_int_list" ":" "(" ident(t) ")" ] -> { EA.Tac.LTac(EA.Tac.List EA.Tac.Int, (CAst.make ~loc @@ Constrexpr.CRef (Libnames.qualid_of_string ~loc @@ Names.Id.to_string t,None))) }
| [ "ltac_term" ":" "(" ident(t) ")" ] -> { EA.Tac.LTac(EA.Tac.Term, CAst.make ~loc @@ Constrexpr.CRef (Libnames.qualid_of_string ~loc @@ Names.Id.to_string t,None)) }
| [ "ltac_term_list" ":" "(" ident(t) ")" ] -> { EA.Tac.LTac(EA.Tac.List EA.Tac.Term,(CAst.make ~loc @@ Constrexpr.CRef (Libnames.qualid_of_string ~loc @@ Names.Id.to_string t,None))) }
| [ "ltac_thunk" ":" "(" elpi_tactic_thunk(t) ")" ] -> { EA.Tac.LTacThunk t }
END

ARGUMENT EXTEND ltac_attributes
Expand Down
42 changes: 27 additions & 15 deletions src/coq_elpi_builtins.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3163,7 +3163,8 @@ is equivalent to Elpi Export TacName.|})))),
let tac_fixed_args = more_args |> List.map (function
| Coq_elpi_arg_HOAS.Cint n -> Coq_elpi_arg_HOAS.Tac.Int n
| Coq_elpi_arg_HOAS.Cstr s -> Coq_elpi_arg_HOAS.Tac.String s
| Coq_elpi_arg_HOAS.Ctrm t -> Coq_elpi_arg_HOAS.Tac.Term (Coq_elpi_utils.detype env sigma t,None)) in
| Coq_elpi_arg_HOAS.Ctrm t -> Coq_elpi_arg_HOAS.Tac.Term (Coq_elpi_utils.detype env sigma t,None)
| Coq_elpi_arg_HOAS.Cltac _ -> nYI "tactic notation with ltac argument") in
let abbrev_name = Coq_elpi_utils.string_split_on_char '.' name in
let tac_name = Coq_elpi_utils.string_split_on_char '.' tacname in
Lib.add_leaf @@ inAbbreviationForTactic { abbrev_name; tac_name; tac_fixed_args};
Expand Down Expand Up @@ -3555,6 +3556,8 @@ coq.reduction.lazy.whd_all X Y :-

LPDoc "-- Coq's tactics --------------------------------------------";

MLData Coq_elpi_arg_HOAS.tac;

MLCode(Pred("coq.ltac.fail",
In(B.unspec B.int,"Level",
VariadicIn(unit_ctx, !> B.any, "Interrupts the Elpi program and calls Ltac's fail Level Msg, where Msg is the printing of the remaining arguments. Level can be left unspecified and defaults to 0")),
Expand Down Expand Up @@ -3617,29 +3620,38 @@ fold_left over the terms, letin body comes before the type).
DocAbove);

MLCode(Pred("coq.ltac.call-ltac1",
In(B.string, "Tac",
In(B.any, "Tac",
CIn(goal, "G",
Out(list sealed_goal,"GL",
Full(raw_ctx, "Calls Ltac1 tactic named Tac on goal G (passing the arguments of G, see coq.ltac.call for a handy wrapper)")))),
(fun tac_name (proof_context,goal,tac_args) _ ~depth _ _ -> abstract__grab_global_env_keep_sigma "coq.ltac.call-ltac1" (fun state ->
(fun tac (proof_context,goal,tac_args) _ ~depth _ _ -> abstract__grab_global_env_keep_sigma "coq.ltac.call-ltac1" (fun state ->
let open Ltac_plugin in
let sigma = get_sigma state in
let tac_args = tac_args |> List.map (function
| Coq_elpi_arg_HOAS.Ctrm t -> Tacinterp.Value.of_constr t
| Coq_elpi_arg_HOAS.Cstr s -> Geninterp.(Val.inject (val_tag (Genarg.topwit Stdarg.wit_string))) s
| Coq_elpi_arg_HOAS.Cint i -> Tacinterp.Value.of_int i) in
| Coq_elpi_arg_HOAS.Cint i -> Tacinterp.Value.of_int i
| Coq_elpi_arg_HOAS.Cltac x -> x) in
let tactic =
let tac_name =
let q = Libnames.qualid_of_string tac_name in
try Tacenv.locate_tactic q
with Not_found ->
match Tacenv.locate_extended_all_tactic q with
| [x] -> x
| _::_::_ -> err Pp.(str"Ltac1 tactic " ++ str tac_name ++ str" is ambiguous, qualify the name")
| [] -> err Pp.(str"Ltac1 tactic " ++ str tac_name ++ str" not found") in
let tacref = Locus.ArgArg (Loc.tag @@ tac_name) in
let tacexpr = Tacexpr.(CAst.make @@ TacArg (TacCall (CAst.make @@ (tacref, [])))) in
let tac = Tacinterp.Value.of_closure (Tacinterp.default_ist ()) tacexpr in
let tac =
match E.look ~depth tac with
| E.CData s when API.RawOpaqueData.is_string s ->
let tac_name = API.RawOpaqueData.to_string s in
let tac_name =
let q = Libnames.qualid_of_string tac_name in
try Tacenv.locate_tactic q
with Not_found ->
match Tacenv.locate_extended_all_tactic q with
| [x] -> x
| _::_::_ -> err Pp.(str"Ltac1 tactic " ++ str tac_name ++ str" is ambiguous, qualify the name")
| [] -> err Pp.(str"Ltac1 tactic " ++ str tac_name ++ str" not found") in
let tacref = Locus.ArgArg (Loc.tag @@ tac_name) in
let tacexpr = Tacexpr.(CAst.make @@ TacArg (TacCall (CAst.make @@ (tacref, [])))) in
Tacinterp.Value.of_closure (Tacinterp.default_ist ()) tacexpr
| E.CData t when Coq_elpi_arg_HOAS.is_ltac_thunk t ->
Coq_elpi_arg_HOAS.to_ltac_thunk t
| _ -> assert false
in
Tacinterp.Value.apply tac tac_args in
let subgoals, sigma =
let open Proofview in let open Notations in
Expand Down
14 changes: 13 additions & 1 deletion tests/test_tactic.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -354,4 +354,16 @@ Section Test.
t2 (H = H). (* t2 called with a term containing H, works *)
t2 H. (* called just with H, fails *)
Abort.
End Test.
End Test.


Elpi Tactic app.
Elpi Accumulate lp:{{
solve (goal C R T P [tac F, tac X]) GL :-
coq.ltac.call-ltac1 F (goal C R T P [tac X]) GL.
}}.
Elpi Typecheck.
Ltac xx f := f.
Goal forall n, n + 1 = 1.

elpi app ltac_thunk:(let f x := x in f) ltac_thunk:( intro n ).

0 comments on commit bd21758

Please sign in to comment.