From bd21758d276cbd71efb335af63ec40e7a92730d2 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 28 Sep 2023 21:14:55 +0200 Subject: [PATCH] wip --- coq-builtin.elpi | 9 +++++- elpi/coq-HOAS.elpi | 3 ++ src/coq_elpi_arg_HOAS.ml | 62 ++++++++++++++++++++++++++++++------- src/coq_elpi_arg_HOAS.mli | 27 ++++++++++------ src/coq_elpi_arg_syntax.mlg | 11 +++++++ src/coq_elpi_builtins.ml | 42 ++++++++++++++++--------- tests/test_tactic.v | 14 ++++++++- 7 files changed, 131 insertions(+), 37 deletions(-) diff --git a/coq-builtin.elpi b/coq-builtin.elpi index f8008b533..d1a7b0d70 100644 --- a/coq-builtin.elpi +++ b/coq-builtin.elpi @@ -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"). % @@ -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 @@ -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 diff --git a/elpi/coq-HOAS.elpi b/elpi/coq-HOAS.elpi index 272635bcc..94e69496c 100644 --- a/elpi/coq-HOAS.elpi +++ b/elpi/coq-HOAS.elpi @@ -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"). % diff --git a/src/coq_elpi_arg_HOAS.ml b/src/coq_elpi_arg_HOAS.ml index 83875d7f1..a21c76548 100644 --- a/src/coq_elpi_arg_HOAS.ml +++ b/src/coq_elpi_arg_HOAS.ml @@ -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) -> @@ -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 @@ -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 @@ -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 = @@ -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" @@ -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 ""); + 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 @@ -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 @@ -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)) diff --git a/src/coq_elpi_arg_HOAS.mli b/src/coq_elpi_arg_HOAS.mli index 09a08a4c6..5613d56aa 100644 --- a/src/coq_elpi_arg_HOAS.mli +++ b/src/coq_elpi_arg_HOAS.mli @@ -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 -> @@ -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 -> diff --git a/src/coq_elpi_arg_syntax.mlg b/src/coq_elpi_arg_syntax.mlg index 334c87c0f..9ba911d6e 100644 --- a/src/coq_elpi_arg_syntax.mlg +++ b/src/coq_elpi_arg_syntax.mlg @@ -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 @@ -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 @@ -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 @@ -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 diff --git a/src/coq_elpi_builtins.ml b/src/coq_elpi_builtins.ml index 8e9c74e0a..4a46b5f42 100644 --- a/src/coq_elpi_builtins.ml +++ b/src/coq_elpi_builtins.ml @@ -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}; @@ -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")), @@ -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 diff --git a/tests/test_tactic.v b/tests/test_tactic.v index cbece1f77..02716e414 100644 --- a/tests/test_tactic.v +++ b/tests/test_tactic.v @@ -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. \ No newline at end of file +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 ). \ No newline at end of file