aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--API/API.mli3
-rw-r--r--dev/ci/user-overlays/06197-ejgallego-plugins+remove_locality_hack.sh4
-rw-r--r--dev/top_printers.ml4
-rw-r--r--grammar/vernacextend.mlp23
-rw-r--r--plugins/firstorder/g_ground.ml411
-rw-r--r--plugins/ltac/extratactics.ml438
-rw-r--r--plugins/ltac/g_auto.ml415
-rw-r--r--plugins/ltac/g_ltac.ml418
-rw-r--r--plugins/ltac/g_obligations.ml412
-rw-r--r--plugins/ltac/g_rewrite.ml427
-rw-r--r--plugins/ltac/rewrite.ml4
-rw-r--r--plugins/ltac/rewrite.mli2
-rw-r--r--plugins/ssr/ssrvernac.ml411
-rw-r--r--vernac/locality.ml20
-rw-r--r--vernac/locality.mli8
-rw-r--r--vernac/vernacinterp.ml5
16 files changed, 117 insertions, 88 deletions
diff --git a/API/API.mli b/API/API.mli
index f56509a70..275185fa7 100644
--- a/API/API.mli
+++ b/API/API.mli
@@ -5837,9 +5837,6 @@ end
module Locality :
sig
val make_section_locality : bool option -> bool
- module LocalityFixme : sig
- val consume : unit -> bool option
- end
val make_module_locality : bool option -> bool
end
diff --git a/dev/ci/user-overlays/06197-ejgallego-plugins+remove_locality_hack.sh b/dev/ci/user-overlays/06197-ejgallego-plugins+remove_locality_hack.sh
new file mode 100644
index 000000000..c9f1272be
--- /dev/null
+++ b/dev/ci/user-overlays/06197-ejgallego-plugins+remove_locality_hack.sh
@@ -0,0 +1,4 @@
+if [ "$TRAVIS_PULL_REQUEST" = "6197" ] || [ "$TRAVIS_BRANCH" = "plugins+remove_locality_hack" ]; then
+ ltac2_CI_BRANCH=localityfixyou
+ ltac2_CI_GITURL=https://github.com/ejgallego/ltac2.git
+fi
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 0f496d3b9..9ebb0360a 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -509,7 +509,7 @@ let _ =
(function
[c] when genarg_tag c = unquote (topwit wit_constr) && true ->
let c = out_gen (rawwit wit_constr) c in
- (fun _ st -> in_current_context constr_display c; st)
+ (fun ~atts ~st -> in_current_context constr_display c; st)
| _ -> failwith "Vernac extension: cannot occur")
with
e -> pp (CErrors.print e)
@@ -525,7 +525,7 @@ let _ =
(function
[c] when genarg_tag c = unquote (topwit wit_constr) && true ->
let c = out_gen (rawwit wit_constr) c in
- (fun _ st -> in_current_context print_pure_constr c; st)
+ (fun ~atts ~st -> in_current_context print_pure_constr c; st)
| _ -> failwith "Vernac extension: cannot occur")
with
e -> pp (CErrors.print e)
diff --git a/grammar/vernacextend.mlp b/grammar/vernacextend.mlp
index ae8fe4da2..5bc8f1504 100644
--- a/grammar/vernacextend.mlp
+++ b/grammar/vernacextend.mlp
@@ -136,6 +136,10 @@ EXTEND
OPT "|"; l = LIST1 rule SEP "|";
"END" ->
declare_command loc s c <:expr<None>> l
+ | "VERNAC"; "COMMAND"; "FUNCTIONAL"; "EXTEND"; s = UIDENT; c = OPT classification;
+ OPT "|"; l = LIST1 fun_rule SEP "|";
+ "END" ->
+ declare_command loc s c <:expr<None>> l
| "VERNAC"; nt = LIDENT ; "EXTEND"; s = UIDENT; c = OPT classification;
OPT "|"; l = LIST1 rule SEP "|";
"END" ->
@@ -162,13 +166,6 @@ EXTEND
(which otherwise could have been another argument) is not passed
to the VernacExtend interpreter function to discriminate between
the clauses. *)
-
- (* ejga: Due to the LocalityFixme abomination we cannot eta-expand
- [e] as we'd like to, so we need to use the below mess with [fun
- st -> st].
-
- At some point We should solve the mess and extend
- vernacextend.mlp with locality info. *)
rule:
[ [ "["; s = STRING; l = LIST0 args; "]";
d = OPT deprecation; c = OPT classifier; "->"; "["; e = Pcaml.expr; "]" ->
@@ -181,6 +178,18 @@ EXTEND
{ r_head = None; r_patt = l; r_class = c; r_branch = b; r_depr = d; }
] ]
;
+ fun_rule:
+ [ [ "["; s = STRING; l = LIST0 args; "]";
+ d = OPT deprecation; c = OPT classifier; "->"; "["; e = Pcaml.expr; "]" ->
+ let () = if s = "" then failwith "Command name is empty." in
+ let b = <:expr< $e$ >> in
+ { r_head = Some s; r_patt = l; r_class = c; r_branch = b; r_depr = d; }
+ | "[" ; "-" ; l = LIST1 args ; "]" ;
+ d = OPT deprecation; c = OPT classifier; "->"; "["; e = Pcaml.expr; "]" ->
+ let b = <:expr< $e$ >> in
+ { r_head = None; r_patt = l; r_class = c; r_branch = b; r_depr = d; }
+ ] ]
+ ;
classifier:
[ [ "=>"; "["; c = Pcaml.expr; "]" -> <:expr< fun loc -> $c$>> ] ]
;
diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4
index 1e7da3250..938bec25b 100644
--- a/plugins/firstorder/g_ground.ml4
+++ b/plugins/firstorder/g_ground.ml4
@@ -65,11 +65,14 @@ let default_intuition_tac =
let (set_default_solver, default_solver, print_default_solver) =
Tactic_option.declare_tactic_option ~default:default_intuition_tac "Firstorder default solver"
-VERNAC COMMAND EXTEND Firstorder_Set_Solver CLASSIFIED AS SIDEFF
+VERNAC COMMAND FUNCTIONAL EXTEND Firstorder_Set_Solver CLASSIFIED AS SIDEFF
| [ "Set" "Firstorder" "Solver" tactic(t) ] -> [
- set_default_solver
- (Locality.make_section_locality (Locality.LocalityFixme.consume ()))
- (Tacintern.glob_tactic t) ]
+ fun ~atts ~st -> let open Vernacinterp in
+ set_default_solver
+ (Locality.make_section_locality atts.locality)
+ (Tacintern.glob_tactic t);
+ st
+ ]
END
VERNAC COMMAND EXTEND Firstorder_Print_Solver CLASSIFIED AS QUERY
diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4
index 4b1555e55..578ebd6f7 100644
--- a/plugins/ltac/extratactics.ml4
+++ b/plugins/ltac/extratactics.ml4
@@ -319,24 +319,44 @@ let project_hint pri l2r r =
let info = {Vernacexpr.hint_priority = pri; hint_pattern = None} in
(info,false,true,Hints.PathAny, Hints.IsGlobRef (Globnames.ConstRef c))
-let add_hints_iff l2r lc n bl =
- let l = Locality.LocalityFixme.consume () in
- Hints.add_hints (Locality.make_module_locality l) bl
+let add_hints_iff ?locality l2r lc n bl =
+ Hints.add_hints (Locality.make_module_locality locality) bl
(Hints.HintsResolveEntry (List.map (project_hint n l2r) lc))
-VERNAC COMMAND EXTEND HintResolveIffLR CLASSIFIED AS SIDEFF
+VERNAC COMMAND FUNCTIONAL EXTEND HintResolveIffLR CLASSIFIED AS SIDEFF
[ "Hint" "Resolve" "->" ne_global_list(lc) natural_opt(n)
":" preident_list(bl) ] ->
- [ add_hints_iff true lc n bl ]
+ [ fun ~atts ~st -> begin
+ let open Vernacinterp in
+ add_hints_iff ?locality:atts.locality true lc n bl;
+ st
+ end
+ ]
| [ "Hint" "Resolve" "->" ne_global_list(lc) natural_opt(n) ] ->
- [ add_hints_iff true lc n ["core"] ]
+ [ fun ~atts ~st -> begin
+ let open Vernacinterp in
+ add_hints_iff ?locality:atts.locality true lc n ["core"];
+ st
+ end
+ ]
END
-VERNAC COMMAND EXTEND HintResolveIffRL CLASSIFIED AS SIDEFF
+
+VERNAC COMMAND FUNCTIONAL EXTEND HintResolveIffRL CLASSIFIED AS SIDEFF
[ "Hint" "Resolve" "<-" ne_global_list(lc) natural_opt(n)
":" preident_list(bl) ] ->
- [ add_hints_iff false lc n bl ]
+ [ fun ~atts ~st -> begin
+ let open Vernacinterp in
+ add_hints_iff ?locality:atts.locality false lc n bl;
+ st
+ end
+ ]
| [ "Hint" "Resolve" "<-" ne_global_list(lc) natural_opt(n) ] ->
- [ add_hints_iff false lc n ["core"] ]
+ [ fun ~atts ~st -> begin
+ let open Vernacinterp in
+ add_hints_iff ?locality:atts.locality false lc n ["core"];
+ st
+ end
+ ]
END
(**********************************************************************)
diff --git a/plugins/ltac/g_auto.ml4 b/plugins/ltac/g_auto.ml4
index 84e79d8ab..90a44708f 100644
--- a/plugins/ltac/g_auto.ml4
+++ b/plugins/ltac/g_auto.ml4
@@ -190,7 +190,7 @@ END
let pr_hints_path prc prx pry c = Hints.pp_hints_path c
let pr_pre_hints_path prc prx pry c = Hints.pp_hints_path_gen Libnames.pr_reference c
let glob_hints_path ist = Hints.glob_hints_path
-
+
ARGUMENT EXTEND hints_path
PRINTED BY pr_hints_path
@@ -214,10 +214,15 @@ ARGUMENT EXTEND opthints
| [ ] -> [ None ]
END
-VERNAC COMMAND EXTEND HintCut CLASSIFIED AS SIDEFF
+VERNAC COMMAND FUNCTIONAL EXTEND HintCut CLASSIFIED AS SIDEFF
| [ "Hint" "Cut" "[" hints_path(p) "]" opthints(dbnames) ] -> [
- let entry = Hints.HintsCutEntry (Hints.glob_hints_path p) in
- Hints.add_hints (Locality.make_section_locality (Locality.LocalityFixme.consume ()))
- (match dbnames with None -> ["core"] | Some l -> l) entry ]
+ fun ~atts ~st -> begin
+ let open Vernacinterp in
+ let entry = Hints.HintsCutEntry (Hints.glob_hints_path p) in
+ Hints.add_hints (Locality.make_section_locality atts.locality)
+ (match dbnames with None -> ["core"] | Some l -> l) entry;
+ st
+ end
+ ]
END
diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4
index 116152568..34fea6175 100644
--- a/plugins/ltac/g_ltac.ml4
+++ b/plugins/ltac/g_ltac.ml4
@@ -469,13 +469,13 @@ VERNAC ARGUMENT EXTEND ltac_production_item PRINTED BY pr_ltac_production_item
[ Tacentries.TacNonTerm (Loc.tag ~loc ((Id.to_string nt, None), None)) ]
END
-VERNAC COMMAND EXTEND VernacTacticNotation
+VERNAC COMMAND FUNCTIONAL EXTEND VernacTacticNotation
| [ "Tactic" "Notation" ltac_tactic_level_opt(n) ne_ltac_production_item_list(r) ":=" tactic(e) ] =>
[ VtUnknown, VtNow ] ->
- [
- let l = Locality.LocalityFixme.consume () in
- let n = Option.default 0 n in
- Tacentries.add_tactic_notation (Locality.make_module_locality l) n r e
+ [ fun ~atts ~st -> let open Vernacinterp in
+ let n = Option.default 0 n in
+ Tacentries.add_tactic_notation (Locality.make_module_locality atts.locality) n r e;
+ st
]
END
@@ -512,15 +512,15 @@ PRINTED BY pr_tacdef_body
| [ tacdef_body(t) ] -> [ t ]
END
-VERNAC COMMAND EXTEND VernacDeclareTacticDefinition
+VERNAC COMMAND FUNCTIONAL EXTEND VernacDeclareTacticDefinition
| [ "Ltac" ne_ltac_tacdef_body_list_sep(l, "with") ] => [
VtSideff (List.map (function
| TacticDefinition ((_,r),_) -> r
| TacticRedefinition (Ident (_,r),_) -> r
| TacticRedefinition (Qualid (_,q),_) -> snd(repr_qualid q)) l), VtLater
- ] -> [
- let lc = Locality.LocalityFixme.consume () in
- Tacentries.register_ltac (Locality.make_module_locality lc) l
+ ] -> [ fun ~atts ~st -> let open Vernacinterp in
+ Tacentries.register_ltac (Locality.make_module_locality atts.locality) l;
+ st
]
END
diff --git a/plugins/ltac/g_obligations.ml4 b/plugins/ltac/g_obligations.ml4
index fea9e837b..f6cc3833a 100644
--- a/plugins/ltac/g_obligations.ml4
+++ b/plugins/ltac/g_obligations.ml4
@@ -123,11 +123,15 @@ VERNAC COMMAND EXTEND Admit_Obligations CLASSIFIED AS SIDEFF
| [ "Admit" "Obligations" ] -> [ admit_obligations None ]
END
-VERNAC COMMAND EXTEND Set_Solver CLASSIFIED AS SIDEFF
+VERNAC COMMAND FUNCTIONAL EXTEND Set_Solver CLASSIFIED AS SIDEFF
| [ "Obligation" "Tactic" ":=" tactic(t) ] -> [
- set_default_tactic
- (Locality.make_section_locality (Locality.LocalityFixme.consume ()))
- (Tacintern.glob_tactic t) ]
+ fun ~atts ~st -> begin
+ let open Vernacinterp in
+ set_default_tactic
+ (Locality.make_section_locality atts.locality)
+ (Tacintern.glob_tactic t);
+ st
+ end]
END
open Pp
diff --git a/plugins/ltac/g_rewrite.ml4 b/plugins/ltac/g_rewrite.ml4
index 91abe1019..ea1808a25 100644
--- a/plugins/ltac/g_rewrite.ml4
+++ b/plugins/ltac/g_rewrite.ml4
@@ -243,22 +243,37 @@ VERNAC COMMAND EXTEND AddParametricRelation3 CLASSIFIED AS SIDEFF
[ declare_relation ~binders:b a aeq n None None (Some lemma3) ]
END
-VERNAC COMMAND EXTEND AddSetoid1 CLASSIFIED AS SIDEFF
+VERNAC COMMAND FUNCTIONAL EXTEND AddSetoid1 CLASSIFIED AS SIDEFF
[ "Add" "Setoid" constr(a) constr(aeq) constr(t) "as" ident(n) ] ->
- [ add_setoid (not (Locality.make_section_locality (Locality.LocalityFixme.consume ()))) [] a aeq t n ]
+ [ fun ~atts ~st -> let open Vernacinterp in
+ add_setoid (not (Locality.make_section_locality atts.locality)) [] a aeq t n;
+ st
+ ]
| [ "Add" "Parametric" "Setoid" binders(binders) ":" constr(a) constr(aeq) constr(t) "as" ident(n) ] ->
- [ add_setoid (not (Locality.make_section_locality (Locality.LocalityFixme.consume ()))) binders a aeq t n ]
+ [ fun ~atts ~st -> let open Vernacinterp in
+ add_setoid (not (Locality.make_section_locality atts.locality)) binders a aeq t n;
+ st
+ ]
| [ "Add" "Morphism" constr(m) ":" ident(n) ]
(* This command may or may not open a goal *)
=> [ Vernacexpr.VtUnknown, Vernacexpr.VtNow ]
- -> [ add_morphism_infer (not (Locality.make_section_locality (Locality.LocalityFixme.consume ()))) m n ]
+ -> [ fun ~atts ~st -> let open Vernacinterp in
+ add_morphism_infer (not (Locality.make_section_locality atts.locality)) m n;
+ st
+ ]
| [ "Add" "Morphism" constr(m) "with" "signature" lconstr(s) "as" ident(n) ]
=> [ Vernacexpr.(VtStartProof("Classic",GuaranteesOpacity,[n]), VtLater) ]
- -> [ add_morphism (not (Locality.make_section_locality (Locality.LocalityFixme.consume ()))) [] m s n ]
+ -> [ fun ~atts ~st -> let open Vernacinterp in
+ add_morphism (not (Locality.make_section_locality atts.locality)) [] m s n;
+ st
+ ]
| [ "Add" "Parametric" "Morphism" binders(binders) ":" constr(m)
"with" "signature" lconstr(s) "as" ident(n) ]
=> [ Vernacexpr.(VtStartProof("Classic",GuaranteesOpacity,[n]), VtLater) ]
- -> [ add_morphism (not (Locality.make_section_locality (Locality.LocalityFixme.consume ()))) binders m s n ]
+ -> [ fun ~atts ~st -> let open Vernacinterp in
+ add_morphism (not (Locality.make_section_locality atts.locality)) binders m s n;
+ st
+ ]
END
TACTIC EXTEND setoid_symmetry
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index c63492d1b..14b0742a7 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -1800,9 +1800,9 @@ let declare_instance_trans global binders a aeq n lemma =
in anew_instance global binders instance
[(Ident (Loc.tag @@ Id.of_string "transitivity"),lemma)]
-let declare_relation ?(binders=[]) a aeq n refl symm trans =
+let declare_relation ?locality ?(binders=[]) a aeq n refl symm trans =
init_setoid ();
- let global = not (Locality.make_section_locality (Locality.LocalityFixme.consume ())) in
+ let global = not (Locality.make_section_locality locality) in
let instance = declare_instance a aeq (add_suffix n "_relation") "Coq.Classes.RelationClasses.RewriteRelation"
in ignore(anew_instance global binders instance []);
match (refl,symm,trans) with
diff --git a/plugins/ltac/rewrite.mli b/plugins/ltac/rewrite.mli
index 1306c590b..17e7244b3 100644
--- a/plugins/ltac/rewrite.mli
+++ b/plugins/ltac/rewrite.mli
@@ -75,7 +75,7 @@ val cl_rewrite_clause :
val is_applied_rewrite_relation :
env -> evar_map -> rel_context -> constr -> types option
-val declare_relation :
+val declare_relation : ?locality:bool ->
?binders:local_binder_expr list -> constr_expr -> constr_expr -> Id.t ->
constr_expr option -> constr_expr option -> constr_expr option -> unit
diff --git a/plugins/ssr/ssrvernac.ml4 b/plugins/ssr/ssrvernac.ml4
index cd614fee9..7385ed84c 100644
--- a/plugins/ssr/ssrvernac.ml4
+++ b/plugins/ssr/ssrvernac.ml4
@@ -158,11 +158,14 @@ let declare_one_prenex_implicit locality f =
| impls ->
Impargs.declare_manual_implicits locality fref ~enriching:false [impls]
-VERNAC COMMAND EXTEND Ssrpreneximplicits CLASSIFIED AS SIDEFF
+VERNAC COMMAND FUNCTIONAL EXTEND Ssrpreneximplicits CLASSIFIED AS SIDEFF
| [ "Prenex" "Implicits" ne_global_list(fl) ]
- -> [ let locality =
- Locality.make_section_locality (Locality.LocalityFixme.consume ()) in
- List.iter (declare_one_prenex_implicit locality) fl ]
+ -> [ fun ~atts ~st ->
+ let open Vernacinterp in
+ let locality = Locality.make_section_locality atts.locality in
+ List.iter (declare_one_prenex_implicit locality) fl;
+ st
+ ]
END
(* Vernac grammar visibility patch *)
diff --git a/vernac/locality.ml b/vernac/locality.ml
index 054a451a4..681b1ab20 100644
--- a/vernac/locality.ml
+++ b/vernac/locality.ml
@@ -6,22 +6,12 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open Pp
-
(** * Managing locality *)
let local_of_bool = function
| true -> Decl_kinds.Local
| false -> Decl_kinds.Global
-let check_locality locality_flag =
- match locality_flag with
- | Some b ->
- let s = if b then "Local" else "Global" in
- CErrors.user_err ~hdr:"Locality.check_locality"
- (str "This command does not support the \"" ++ str s ++ str "\" prefix.")
- | None -> ()
-
(** Extracting the locality flag *)
(* Commands which supported an inlined Local flag *)
@@ -95,13 +85,3 @@ let make_module_locality = function
let enforce_module_locality locality_flag local =
make_module_locality (enforce_locality_full locality_flag local)
-
-module LocalityFixme = struct
- let locality = ref None
- let set l = locality := l
- let consume () =
- let l = !locality in
- locality := None;
- l
- let assert_consumed () = check_locality !locality
-end
diff --git a/vernac/locality.mli b/vernac/locality.mli
index c1c45d6b0..bef66d8bc 100644
--- a/vernac/locality.mli
+++ b/vernac/locality.mli
@@ -41,11 +41,3 @@ val enforce_section_locality : bool option -> bool -> bool
val make_module_locality : bool option -> bool
val enforce_module_locality : bool option -> bool -> bool
-
-(* This is the old imperative interface that is still used for
- * VernacExtend vernaculars. Time permitting this could be trashed too *)
-module LocalityFixme : sig
- val set : bool option -> unit
- val consume : unit -> bool option
- val assert_consumed : unit -> unit
-end
diff --git a/vernac/vernacinterp.ml b/vernac/vernacinterp.ml
index 725436fef..47dec1958 100644
--- a/vernac/vernacinterp.ml
+++ b/vernac/vernacinterp.ml
@@ -74,11 +74,8 @@ let call ?locality ?loc (opn,converted_args) =
phase := "Checking arguments";
let hunk = callback converted_args in
phase := "Executing command";
- Locality.LocalityFixme.set locality;
let atts = { loc; locality } in
- let res = hunk ~atts in
- Locality.LocalityFixme.assert_consumed ();
- res
+ hunk ~atts
with
| Drop -> raise Drop
| reraise ->
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-17 02:07:55 +0000