aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--.gitignore3
-rw-r--r--dune3
-rw-r--r--dune-project3
-rw-r--r--ltac2.opam18
-rw-r--r--opam/descr1
-rw-r--r--opam/opam17
-rw-r--r--src/dune6
-rw-r--r--src/g_ltac2.mlg17
-rw-r--r--src/tac2core.ml46
-rw-r--r--src/tac2entries.ml34
-rw-r--r--src/tac2entries.mli10
-rw-r--r--src/tac2tactics.ml1
-rw-r--r--theories/dune6
13 files changed, 90 insertions, 75 deletions
diff --git a/.gitignore b/.gitignore
index 50ed772be3..00e15f8daa 100644
--- a/.gitignore
+++ b/.gitignore
@@ -13,3 +13,6 @@ Makefile.coq.conf
*.a
*.aux
tests/*.log
+*.install
+_build
+.merlin
diff --git a/dune b/dune
new file mode 100644
index 0000000000..5dbc4db66a
--- /dev/null
+++ b/dune
@@ -0,0 +1,3 @@
+(env
+ (dev (flags :standard -rectypes))
+ (release (flags :standard -rectypes)))
diff --git a/dune-project b/dune-project
new file mode 100644
index 0000000000..8154e999de
--- /dev/null
+++ b/dune-project
@@ -0,0 +1,3 @@
+(lang dune 1.6)
+(using coq 0.1)
+(name ltac2)
diff --git a/ltac2.opam b/ltac2.opam
new file mode 100644
index 0000000000..47ceb882b1
--- /dev/null
+++ b/ltac2.opam
@@ -0,0 +1,18 @@
+synopsis: "A Tactic Language for Coq."
+description: "A Tactic Language for Coq."
+name: "coq-ltac2"
+opam-version: "2.0"
+maintainer: "Pierre-Marie Pédrot <pierre-marie.pedrot@irif.fr>"
+authors: "Pierre-Marie Pédrot <pierre-marie.pedrot@irif.fr>"
+homepage: "https://github.com/ppedrot/ltac2"
+dev-repo: "https://github.com/ppedrot/ltac2.git"
+bug-reports: "https://github.com/ppedrot/ltac2/issues"
+license: "LGPL 2.1"
+doc: "https://ppedrot.github.io/ltac2/doc"
+
+depends: [
+ "coq" { = "dev" }
+ "dune" { build & >= "1.9.0" }
+]
+
+build: [ "dune" "build" "-p" name "-j" jobs ]
diff --git a/opam/descr b/opam/descr
deleted file mode 100644
index 82463c4f45..0000000000
--- a/opam/descr
+++ /dev/null
@@ -1 +0,0 @@
-A tactic language for Coq.
diff --git a/opam/opam b/opam/opam
deleted file mode 100644
index e461b97942..0000000000
--- a/opam/opam
+++ /dev/null
@@ -1,17 +0,0 @@
-opam-version: "1.2"
-name: "coq-ltac2"
-version: "0.1"
-maintainer: "Pierre-Marie Pédrot <pierre-marie.pedrot@irif.fr>"
-author: "Pierre-Marie Pédrot <pierre-marie.pedrot@irif.fr>"
-license: "LGPL 2.1"
-homepage: "https://github.com/ppedrot/ltac2"
-dev-repo: "https://github.com/ppedrot/ltac2.git"
-bug-reports: "https://github.com/ppedrot/ltac2/issues"
-build: [
- [make "COQBIN=\"\"" "-j%{jobs}%"]
-]
-install: [make "install"]
-remove: [make "uninstall"]
-depends: [
- "coq" { = "dev" }
-]
diff --git a/src/dune b/src/dune
index 4a018adb9a..332f3644b0 100644
--- a/src/dune
+++ b/src/dune
@@ -1,8 +1,8 @@
(library
- (name ltac2)
- (public_name coq.plugins.ltac2)
+ (name ltac2_plugin)
+ (public_name ltac2.plugin)
(modules_without_implementation tac2expr tac2qexpr tac2types)
- (flags :standard -w -50)
+ (flags :standard -warn-error -9-27-50)
(libraries coq.plugins.firstorder))
(rule
diff --git a/src/g_ltac2.mlg b/src/g_ltac2.mlg
index 7b058a339a..fcf5d59ec9 100644
--- a/src/g_ltac2.mlg
+++ b/src/g_ltac2.mlg
@@ -831,7 +831,7 @@ let open Tok in
let (++) r s = Next (r, s) in
let rules = [
Rule (
- Stop ++ Aentry test_dollar_ident ++ Atoken (KEYWORD "$") ++ Aentry Prim.ident,
+ Stop ++ Aentry test_dollar_ident ++ Atoken (PKEYWORD "$") ++ Aentry Prim.ident,
begin fun id _ _ loc ->
let id = Loc.tag ~loc id in
let arg = Genarg.in_gen (Genarg.rawwit Tac2env.wit_ltac2_quotation) id in
@@ -840,7 +840,7 @@ let rules = [
);
Rule (
- Stop ++ Aentry test_ampersand_ident ++ Atoken (KEYWORD "&") ++ Aentry Prim.ident,
+ Stop ++ Aentry test_ampersand_ident ++ Atoken (PKEYWORD "&") ++ Aentry Prim.ident,
begin fun id _ _ loc ->
let tac = Tac2quote.of_exact_hyp ~loc (CAst.make ~loc id) in
let arg = Genarg.in_gen (Genarg.rawwit Tac2env.wit_ltac2) tac in
@@ -849,8 +849,8 @@ let rules = [
);
Rule (
- Stop ++ Atoken (IDENT "ltac2") ++ Atoken (KEYWORD ":") ++
- Atoken (KEYWORD "(") ++ Aentry tac2expr ++ Atoken (KEYWORD ")"),
+ Stop ++ Atoken (PIDENT (Some "ltac2")) ++ Atoken (PKEYWORD ":") ++
+ Atoken (PKEYWORD "(") ++ Aentry tac2expr ++ Atoken (PKEYWORD ")"),
begin fun _ tac _ _ _ loc ->
let arg = Genarg.in_gen (Genarg.rawwit Tac2env.wit_ltac2) tac in
CAst.make ~loc (CHole (None, Namegen.IntroAnonymous, Some arg))
@@ -890,8 +890,8 @@ let classify_ltac2 = function
}
VERNAC COMMAND EXTEND VernacDeclareTactic2Definition
-| #[ local = locality ] [ "Ltac2" ltac2_entry(e) ] => { classify_ltac2 e } -> {
- Tac2entries.register_struct ?local e
+| #[ local = locality ] ![proof] [ "Ltac2" ltac2_entry(e) ] => { classify_ltac2 e } -> {
+ fun ~pstate -> Tac2entries.register_struct ?local ~pstate e; pstate
}
END
@@ -914,10 +914,11 @@ open Vernacextend
}
VERNAC { tac2mode } EXTEND VernacLtac2
-| [ ltac2_expr(t) ltac_use_default(default) ] =>
+| ![proof] [ ltac2_expr(t) ltac_use_default(default) ] =>
{ classify_as_proofstep } -> {
(* let g = Option.default (Proof_global.get_default_goal_selector ()) g in *)
- Tac2entries.call ~default t
+ fun ~pstate ->
+ Option.map (fun pstate -> Tac2entries.call ~pstate ~default t) pstate
}
END
diff --git a/src/tac2core.ml b/src/tac2core.ml
index 15fd625650..a584933e00 100644
--- a/src/tac2core.ml
+++ b/src/tac2core.ml
@@ -979,6 +979,7 @@ let constr_flags () =
fail_evar = true;
expand_evars = true;
program_mode = false;
+ polymorphic = false;
}
let open_constr_no_classes_flags () =
@@ -989,6 +990,7 @@ let open_constr_no_classes_flags () =
fail_evar = false;
expand_evars = true;
program_mode = false;
+ polymorphic = false;
}
(** Embed all Ltac2 data into Values *)
@@ -1164,17 +1166,17 @@ let () =
(** Ltac2 in terms *)
let () =
- let interp ist env sigma concl tac =
+ let interp ist poly env sigma concl tac =
let ist = Tac2interp.get_env ist in
let tac = Proofview.tclIGNORE (Tac2interp.interp ist tac) in
- let name, poly = Id.of_string "ltac2", false in
+ let name, poly = Id.of_string "ltac2", poly in
let c, sigma = Pfedit.refine_by_tactic ~name ~poly env sigma concl tac in
(EConstr.of_constr c, sigma)
in
GlobEnv.register_constr_interp0 wit_ltac2 interp
let () =
- let interp ist env sigma concl id =
+ let interp ist poly env sigma concl id =
let ist = Tac2interp.get_env ist in
let c = Id.Map.find id ist.env_ist in
let c = Value.to_constr c in
@@ -1249,7 +1251,7 @@ open CAst
let () = add_scope "keyword" begin function
| [SexprStr {loc;v=s}] ->
- let scope = Extend.Atoken (Tok.KEYWORD s) in
+ let scope = Extend.Atoken (Tok.PKEYWORD s) in
Tac2entries.ScopeRule (scope, (fun _ -> q_unit))
| arg -> scope_fail "keyword" arg
end
@@ -1379,34 +1381,25 @@ let () = add_generic_scope "pattern" Pcoq.Constr.constr Tac2quote.wit_pattern
open Extend
exception SelfSymbol
-type 'a any_symbol = { any_symbol : 'r. ('r, 'a) symbol }
-
let rec generalize_symbol :
- type a s. (s, a) Extend.symbol -> a any_symbol = function
-| Atoken tok ->
- { any_symbol = Atoken tok }
-| Alist1 e ->
- let e = generalize_symbol e in
- { any_symbol = Alist1 e.any_symbol }
+ type a tr s. (s, tr, a) Extend.symbol -> (s, Extend.norec, a) Extend.symbol = function
+| Atoken tok -> Atoken tok
+| Alist1 e -> Alist1 (generalize_symbol e)
| Alist1sep (e, sep) ->
let e = generalize_symbol e in
let sep = generalize_symbol sep in
- { any_symbol = Alist1sep (e.any_symbol, sep.any_symbol) }
-| Alist0 e ->
- let e = generalize_symbol e in
- { any_symbol = Alist0 e.any_symbol }
+ Alist1sep (e, sep)
+| Alist0 e -> Alist0 (generalize_symbol e)
| Alist0sep (e, sep) ->
let e = generalize_symbol e in
let sep = generalize_symbol sep in
- { any_symbol = Alist0sep (e.any_symbol, sep.any_symbol) }
-| Aopt e ->
- let e = generalize_symbol e in
- { any_symbol = Aopt e.any_symbol }
+ Alist0sep (e, sep)
+| Aopt e -> Aopt (generalize_symbol e)
| Aself -> raise SelfSymbol
| Anext -> raise SelfSymbol
-| Aentry e -> { any_symbol = Aentry e }
-| Aentryl (e, l) -> { any_symbol = Aentryl (e, l) }
-| Arules r -> { any_symbol = Arules r }
+| Aentry e -> Aentry e
+| Aentryl (e, l) -> Aentryl (e, l)
+| Arules r -> Arules r
type _ converter =
| CvNil : (Loc.t -> raw_tacexpr) converter
@@ -1418,17 +1411,16 @@ let rec apply : type a. a converter -> raw_tacexpr list -> a = function
| CvCns (c, Some f) -> fun accu x -> apply c (f x :: accu)
type seqrule =
-| Seqrule : ('act, Loc.t -> raw_tacexpr) norec_rule * 'act converter -> seqrule
+| Seqrule : (Tac2expr.raw_tacexpr, Extend.norec, 'act, Loc.t -> raw_tacexpr) rule * 'act converter -> seqrule
let rec make_seq_rule = function
| [] ->
- let r = { norec_rule = Stop } in
- Seqrule (r, CvNil)
+ Seqrule (Stop, CvNil)
| tok :: rem ->
let Tac2entries.ScopeRule (scope, f) = Tac2entries.parse_scope tok in
let scope = generalize_symbol scope in
let Seqrule (r, c) = make_seq_rule rem in
- let r = { norec_rule = Next (r.norec_rule, scope.any_symbol) } in
+ let r = NextNoRec (r, scope) in
let f = match tok with
| SexprStr _ -> None (* Leave out mere strings *)
| _ -> Some f
diff --git a/src/tac2entries.ml b/src/tac2entries.ml
index b7ce363957..9fd01426de 100644
--- a/src/tac2entries.ml
+++ b/src/tac2entries.ml
@@ -514,7 +514,7 @@ type 'a token =
| TacNonTerm of Name.t * 'a
type scope_rule =
-| ScopeRule : (raw_tacexpr, 'a) Extend.symbol * ('a -> raw_tacexpr) -> scope_rule
+| ScopeRule : (raw_tacexpr, _, 'a) Extend.symbol * ('a -> raw_tacexpr) -> scope_rule
type scope_interpretation = sexpr list -> scope_rule
@@ -539,7 +539,7 @@ let parse_scope = function
CErrors.user_err ?loc (str "Unknown scope" ++ spc () ++ Names.Id.print id)
| SexprStr {v=str} ->
let v_unit = CAst.make @@ CTacCst (AbsKn (Tuple 0)) in
- ScopeRule (Extend.Atoken (Tok.IDENT str), (fun _ -> v_unit))
+ ScopeRule (Extend.Atoken (Tok.PIDENT (Some str)), (fun _ -> v_unit))
| tok ->
let loc = loc_of_token tok in
CErrors.user_err ?loc (str "Invalid parsing token")
@@ -567,7 +567,7 @@ type synext = {
type krule =
| KRule :
- (raw_tacexpr, 'act, Loc.t -> raw_tacexpr) Extend.rule *
+ (raw_tacexpr, _, 'act, Loc.t -> raw_tacexpr) Extend.rule *
((Loc.t -> (Name.t * raw_tacexpr) list -> raw_tacexpr) -> 'act) -> krule
let rec get_rule (tok : scope_rule token list) : krule = match tok with
@@ -739,19 +739,20 @@ let register_redefinition ?(local = false) qid e =
} in
Lib.add_anonymous_leaf (inTac2Redefinition def)
-let perform_eval e =
+let perform_eval ~pstate e =
let open Proofview.Notations in
let env = Global.env () in
let (e, ty) = Tac2intern.intern ~strict:false e in
let v = Tac2interp.interp Tac2interp.empty_environment e in
let selector, proof =
- try
- Goal_select.get_default_goal_selector (),
- Proof_global.give_me_the_proof ()
- with Proof_global.NoCurrentProof ->
+ match pstate with
+ | None ->
let sigma = Evd.from_env env in
let name, poly = Id.of_string "ltac2", false in
Goal_select.SelectAll, Proof.start ~name ~poly sigma []
+ | Some pstate ->
+ Goal_select.get_default_goal_selector (),
+ Proof_global.give_me_the_proof pstate
in
let v = match selector with
| Goal_select.SelectNth i -> Proofview.tclFOCUS i i v
@@ -773,13 +774,13 @@ let perform_eval e =
(** Toplevel entries *)
-let register_struct ?local str = match str with
+let register_struct ?local ~pstate str = match str with
| StrVal (mut, isrec, e) -> register_ltac ?local ~mut isrec e
| StrTyp (isrec, t) -> register_type ?local isrec t
| StrPrm (id, t, ml) -> register_primitive ?local id t ml
| StrSyn (tok, lev, e) -> register_notation ?local tok lev e
| StrMut (qid, e) -> register_redefinition ?local qid e
-| StrRun e -> perform_eval e
+| StrRun e -> perform_eval ~pstate e
(** Toplevel exception *)
@@ -860,8 +861,8 @@ let print_ltac qid =
(** Calling tactics *)
-let solve default tac =
- let status = Proof_global.with_current_proof begin fun etac p ->
+let solve ~pstate default tac =
+ let pstate, status = Proof_global.with_current_proof begin fun etac p ->
let with_end_tac = if default then Some etac else None in
let g = Goal_select.get_default_goal_selector () in
let (p, status) = Pfedit.solve g None tac ?with_end_tac p in
@@ -869,15 +870,16 @@ let solve default tac =
go back to the top of the prooftree *)
let p = Proof.maximal_unfocus Vernacentries.command_focus p in
p, status
- end in
- if not status then Feedback.feedback Feedback.AddedAxiom
+ end pstate in
+ if not status then Feedback.feedback Feedback.AddedAxiom;
+ pstate
-let call ~default e =
+let call ~pstate ~default e =
let loc = e.loc in
let (e, t) = intern ~strict:false e in
let () = check_unit ?loc t in
let tac = Tac2interp.interp Tac2interp.empty_environment e in
- solve default (Proofview.tclIGNORE tac)
+ solve ~pstate default (Proofview.tclIGNORE tac)
(** Primitive algebraic types than can't be defined Coq-side *)
diff --git a/src/tac2entries.mli b/src/tac2entries.mli
index f97e35fec0..d493192bb3 100644
--- a/src/tac2entries.mli
+++ b/src/tac2entries.mli
@@ -21,7 +21,11 @@ val register_type : ?local:bool -> rec_flag ->
val register_primitive : ?local:bool ->
Names.lident -> raw_typexpr -> ml_tactic_name -> unit
-val register_struct : ?local:bool -> strexpr -> unit
+val register_struct
+ : ?local:bool
+ -> pstate:Proof_global.t option
+ -> strexpr
+ -> unit
val register_notation : ?local:bool -> sexpr list -> int option ->
raw_tacexpr -> unit
@@ -29,7 +33,7 @@ val register_notation : ?local:bool -> sexpr list -> int option ->
(** {5 Notations} *)
type scope_rule =
-| ScopeRule : (raw_tacexpr, 'a) Extend.symbol * ('a -> raw_tacexpr) -> scope_rule
+| ScopeRule : (raw_tacexpr, _, 'a) Extend.symbol * ('a -> raw_tacexpr) -> scope_rule
type scope_interpretation = sexpr list -> scope_rule
@@ -46,7 +50,7 @@ val print_ltac : Libnames.qualid -> unit
(** {5 Eval loop} *)
(** Evaluate a tactic expression in the current environment *)
-val call : default:bool -> raw_tacexpr -> unit
+val call : pstate:Proof_global.t -> default:bool -> raw_tacexpr -> Proof_global.t
(** {5 Toplevel exceptions} *)
diff --git a/src/tac2tactics.ml b/src/tac2tactics.ml
index 5d9b14eab0..ce37a613b1 100644
--- a/src/tac2tactics.ml
+++ b/src/tac2tactics.ml
@@ -24,6 +24,7 @@ let tactic_infer_flags with_evar = {
Pretyping.fail_evar = not with_evar;
Pretyping.expand_evars = true;
Pretyping.program_mode = false;
+ Pretyping.polymorphic = false;
}
(** FIXME: export a better interface in Tactics *)
diff --git a/theories/dune b/theories/dune
new file mode 100644
index 0000000000..1fe3ba28fe
--- /dev/null
+++ b/theories/dune
@@ -0,0 +1,6 @@
+(coqlib
+ (name Ltac2) ; This determines the -R flag
+ (public_name ltac2.Ltac2)
+ (synopsis "Ltac 2 Plugin")
+ (libraries ltac2.plugin))
+
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-04 21:58:56 +0000