aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--dev/top_printers.ml16
-rw-r--r--grammar/vernacextend.ml422
-rw-r--r--intf/vernacexpr.mli4
-rw-r--r--parsing/egramml.ml12
-rw-r--r--parsing/egramml.mli7
-rw-r--r--printing/ppvernac.ml18
-rw-r--r--stm/vernac_classifier.ml4
-rw-r--r--stm/vernac_classifier.mli2
-rw-r--r--toplevel/vernacinterp.ml8
-rw-r--r--toplevel/vernacinterp.mli6
10 files changed, 45 insertions, 54 deletions
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 15f35b775..56c71d88f 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -476,7 +476,7 @@ open Egramml
let _ =
try
- Vernacinterp.vinterp_add "PrintConstr"
+ Vernacinterp.vinterp_add ("PrintConstr", 0)
(function
[c] when genarg_tag c = ConstrArgType && true ->
let c = out_gen (rawwit wit_constr) c in
@@ -485,15 +485,15 @@ let _ =
with
e -> Pp.pp (Errors.print e)
let _ =
- extend_vernac_command_grammar "PrintConstr" None
- [[GramTerminal "PrintConstr";
+ extend_vernac_command_grammar ("PrintConstr", 0) None
+ [GramTerminal "PrintConstr";
GramNonTerminal
(Loc.ghost,ConstrArgType,Aentry ("constr","constr"),
- Some (Names.Id.of_string "c"))]]
+ Some (Names.Id.of_string "c"))]
let _ =
try
- Vernacinterp.vinterp_add "PrintPureConstr"
+ Vernacinterp.vinterp_add ("PrintPureConstr", 0)
(function
[c] when genarg_tag c = ConstrArgType && true ->
let c = out_gen (rawwit wit_constr) c in
@@ -502,11 +502,11 @@ let _ =
with
e -> Pp.pp (Errors.print e)
let _ =
- extend_vernac_command_grammar "PrintPureConstr" None
- [[GramTerminal "PrintPureConstr";
+ extend_vernac_command_grammar ("PrintPureConstr", 0) None
+ [GramTerminal "PrintPureConstr";
GramNonTerminal
(Loc.ghost,ConstrArgType,Aentry ("constr","constr"),
- Some (Names.Id.of_string "c"))]]
+ Some (Names.Id.of_string "c"))]
(* Setting printer of unbound global reference *)
open Names
diff --git a/grammar/vernacextend.ml4 b/grammar/vernacextend.ml4
index 3a9991633..bda262a98 100644
--- a/grammar/vernacextend.ml4
+++ b/grammar/vernacextend.ml4
@@ -27,13 +27,6 @@ let rec make_let e = function
<:expr< let $lid:p$ = Genarg.out_gen $make_rawwit loc t$ $lid:p$ in $e$ >>
| _::l -> make_let e l
-let check_unicity s l =
- let l' = List.map (fun (_,l,_,_) -> extract_signature l) l in
- if not (Util.List.distinct l') then
- msg_warning
- (strbrk ("Two distinct rules of entry "^s^" have the same "^
- "non-terminals in the same order: put them in distinct vernac entries"))
-
let make_clause (_,pt,_,e) =
(make_patt pt,
vala (Some (make_when (MLast.loc_of_expr e) pt)),
@@ -83,11 +76,12 @@ let make_clause_classifier cg s (_,pt,c,_) =
<:expr< fun () -> (Vernacexpr.VtUnknown, Vernacexpr.VtNow) >>)
let make_fun_clauses loc s l =
- check_unicity s l;
- Compat.make_fun loc (List.map make_clause l)
+ let cl = List.map (fun c -> Compat.make_fun loc [make_clause c]) l in
+ mlexpr_of_list (fun x -> x) cl
let make_fun_classifiers loc s c l =
- Compat.make_fun loc (List.map (make_clause_classifier c s) l)
+ let cl = List.map (fun x -> Compat.make_fun loc [make_clause_classifier c s x]) l in
+ mlexpr_of_list (fun x -> x) cl
let mlexpr_of_clause =
mlexpr_of_list
@@ -101,15 +95,15 @@ let declare_command loc s c nt cl =
let classl = make_fun_classifiers loc s c cl in
declare_str_items loc
[ <:str_item< do {
- try do {
- Vernacinterp.vinterp_add $se$ $funcl$;
- Vernac_classifier.declare_vernac_classifier $se$ $classl$ }
+ try do {
+ CList.iteri (fun i f -> Vernacinterp.vinterp_add ($se$, i) f) $funcl$;
+ CList.iteri (fun i f -> Vernac_classifier.declare_vernac_classifier ($se$, i) f) $classl$ }
with [ e when Errors.noncritical e ->
Pp.msg_warning
(Pp.app
(Pp.str ("Exception in vernac extend " ^ $se$ ^": "))
(Errors.print e)) ];
- Egramml.extend_vernac_command_grammar $se$ $nt$ $gl$
+ CList.iteri (fun i r -> Egramml.extend_vernac_command_grammar ($se$, i) $nt$ r) $gl$;
} >> ]
open Pcaml
diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli
index 5bf83e2c1..b784bc433 100644
--- a/intf/vernacexpr.mli
+++ b/intf/vernacexpr.mli
@@ -223,6 +223,8 @@ type section_subset_expr =
type section_subset_descr = SsAll | SsType | SsExpr of section_subset_expr
+type extend_name = string * int
+
(* This type allows registering the inlining of constants in native compiler.
It will be extended with primitive inductive types and operators *)
type register_kind =
@@ -427,7 +429,7 @@ type vernac_expr =
| VernacToplevelControl of exn
(* For extension *)
- | VernacExtend of string * Genarg.raw_generic_argument list
+ | VernacExtend of extend_name * Genarg.raw_generic_argument list
(* Flags *)
| VernacProgram of vernac_expr
diff --git a/parsing/egramml.ml b/parsing/egramml.ml
index 51dda2664..e7c5c4a48 100644
--- a/parsing/egramml.ml
+++ b/parsing/egramml.ml
@@ -6,6 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
+open Util
open Compat
open Names
open Pcoq
@@ -45,11 +46,18 @@ let make_rule mkact pt =
(** Vernac grammar extensions *)
let vernac_exts = ref []
-let get_extend_vernac_grammars () = !vernac_exts
+
+let get_extend_vernac_rule (s, i) =
+ try
+ let find ((name, j), _) = String.equal name s && Int.equal i j in
+ let (_, rules) = List.find find !vernac_exts in
+ rules
+ with
+ | Failure _ -> raise Not_found
let extend_vernac_command_grammar s nt gl =
let nt = Option.default Vernac_.command nt in
vernac_exts := (s,gl) :: !vernac_exts;
let mkact loc l = VernacExtend (s,List.map snd l) in
- let rules = List.map (make_rule mkact) gl in
+ let rules = [make_rule mkact gl] in
maybe_uncurry (Gram.extend nt) (None,[(None, None, List.rev rules)])
diff --git a/parsing/egramml.mli b/parsing/egramml.mli
index 9e2c29b98..97bfbf682 100644
--- a/parsing/egramml.mli
+++ b/parsing/egramml.mli
@@ -17,11 +17,10 @@ type grammar_prod_item =
Pcoq.prod_entry_key * Names.Id.t option
val extend_vernac_command_grammar :
- string -> Vernacexpr.vernac_expr Pcoq.Gram.entry option ->
- grammar_prod_item list list -> unit
+ Vernacexpr.extend_name -> Vernacexpr.vernac_expr Pcoq.Gram.entry option ->
+ grammar_prod_item list -> unit
-val get_extend_vernac_grammars :
- unit -> (string * grammar_prod_item list list) list
+val get_extend_vernac_rule : Vernacexpr.extend_name -> grammar_prod_item list
(** Utility function reused in Egramcoq : *)
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 5ef7eb710..930166524 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -67,17 +67,6 @@ let pr_gen t =
pr_constr_expr
pr_reference t
-let rec extract_signature = function
- | [] -> []
- | Egramml.GramNonTerminal (_,t,_,_) :: l -> t :: extract_signature l
- | _::l -> extract_signature l
-
-let rec match_vernac_rule tys = function
- [] -> raise Not_found
- | pargs::rls ->
- if List.equal Genarg.argument_type_eq (extract_signature pargs) tys then pargs
- else match_vernac_rule tys rls
-
let sep = fun _ -> spc()
let sep_v2 = fun _ -> str"," ++ spc()
@@ -972,10 +961,9 @@ and pr_vernac_list l =
and pr_extend s cl =
let pr_arg a =
try pr_gen a
- with Failure _ -> str ("<error in "^s^">") in
+ with Failure _ -> str ("<error in "^fst s^">") in
try
- let rls = String.List.assoc s (Egramml.get_extend_vernac_grammars()) in
- let rl = match_vernac_rule (List.map Genarg.genarg_tag cl) rls in
+ let rl = Egramml.get_extend_vernac_rule s in
let start,rl,cl =
match rl with
| Egramml.GramTerminal s :: rl -> str s, rl, cl
@@ -991,7 +979,7 @@ and pr_extend s cl =
(start,cl) rl in
hov 1 pp
with Not_found ->
- hov 1 (str ("TODO("^s) ++ prlist_with_sep sep pr_arg cl ++ str ")")
+ hov 1 (str ("TODO("^fst s) ++ prlist_with_sep sep pr_arg cl ++ str ")")
in pr_vernac
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index 6ad1294fc..794fabc91 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -37,7 +37,7 @@ let string_of_vernac_classification (t,w) =
let classifiers = ref []
let declare_vernac_classifier
- (s : string)
+ (s : Vernacexpr.extend_name)
(f : Genarg.raw_generic_argument list -> unit -> vernac_classification)
=
classifiers := !classifiers @ [s,f]
@@ -201,7 +201,7 @@ let rec classify_vernac e =
(* Plugins should classify their commands *)
| VernacExtend (s,l) ->
try List.assoc s !classifiers l ()
- with Not_found -> anomaly(str"No classifier for"++spc()++str s)
+ with Not_found -> anomaly(str"No classifier for"++spc()++str (fst s))
and classify_vernac_list = function
(* spiwack: It would be better to define a monoid on classifiers.
So that the classifier of the list would be the composition of
diff --git a/stm/vernac_classifier.mli b/stm/vernac_classifier.mli
index bc0c0c2b3..329c90198 100644
--- a/stm/vernac_classifier.mli
+++ b/stm/vernac_classifier.mli
@@ -16,7 +16,7 @@ val classify_vernac : vernac_expr -> vernac_classification
(** Install a vernacular classifier for VernacExtend *)
val declare_vernac_classifier :
- string -> (raw_generic_argument list -> unit -> vernac_classification) -> unit
+ Vernacexpr.extend_name -> (raw_generic_argument list -> unit -> vernac_classification) -> unit
(** Set by Stm *)
val set_undo_classifier : (vernac_expr -> vernac_classification) -> unit
diff --git a/toplevel/vernacinterp.ml b/toplevel/vernacinterp.ml
index 2753a3367..31d1c641c 100644
--- a/toplevel/vernacinterp.ml
+++ b/toplevel/vernacinterp.ml
@@ -12,14 +12,14 @@ open Errors
(* Table of vernac entries *)
let vernac_tab =
(Hashtbl.create 51 :
- (string, Genarg.raw_generic_argument list -> unit -> unit) Hashtbl.t)
+ (Vernacexpr.extend_name, (Genarg.raw_generic_argument list -> unit -> unit)) Hashtbl.t)
let vinterp_add s f =
try
Hashtbl.add vernac_tab s f
with Failure _ ->
errorlabstrm "vinterp_add"
- (str"Cannot add the vernac command " ++ str s ++ str" twice.")
+ (str"Cannot add the vernac command " ++ str (fst s) ++ str" twice.")
let overwriting_vinterp_add s f =
begin
@@ -32,9 +32,9 @@ let overwriting_vinterp_add s f =
let vinterp_map s =
try
Hashtbl.find vernac_tab s
- with Not_found ->
+ with Failure _ | Not_found ->
errorlabstrm "Vernac Interpreter"
- (str"Cannot find vernac command " ++ str s ++ str".")
+ (str"Cannot find vernac command " ++ str (fst s) ++ str".")
let vinterp_init () = Hashtbl.clear vernac_tab
diff --git a/toplevel/vernacinterp.mli b/toplevel/vernacinterp.mli
index 3cbbbf05e..33920ec70 100644
--- a/toplevel/vernacinterp.mli
+++ b/toplevel/vernacinterp.mli
@@ -8,9 +8,9 @@
(** Interpretation of extended vernac phrases. *)
-val vinterp_add : string -> (Genarg.raw_generic_argument list -> unit -> unit) -> unit
+val vinterp_add : Vernacexpr.extend_name -> (Genarg.raw_generic_argument list -> unit -> unit) -> unit
val overwriting_vinterp_add :
- string -> (Genarg.raw_generic_argument list -> unit -> unit) -> unit
+ Vernacexpr.extend_name -> (Genarg.raw_generic_argument list -> unit -> unit) -> unit
val vinterp_init : unit -> unit
-val call : ?locality:bool -> string * Genarg.raw_generic_argument list -> unit
+val call : ?locality:bool -> Vernacexpr.extend_name * Genarg.raw_generic_argument list -> unit
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-12 06:32:40 +0000