diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-09-09 22:13:08 +0200 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-09-10 00:16:20 +0200 |
commit | edfa5e986a25eb7a0719d20b43a618cb5bd4cd95 (patch) | |
tree | e7af11e344a99b2496d22d2bc100f493bd701b96 | |
parent | 0dd3f0d34873dcd126be8ec48724a310214f38ac (diff) |
VernacExtend does not dispatch on type anymore.
-rw-r--r-- | dev/top_printers.ml | 16 | ||||
-rw-r--r-- | grammar/vernacextend.ml4 | 22 | ||||
-rw-r--r-- | intf/vernacexpr.mli | 4 | ||||
-rw-r--r-- | parsing/egramml.ml | 12 | ||||
-rw-r--r-- | parsing/egramml.mli | 7 | ||||
-rw-r--r-- | printing/ppvernac.ml | 18 | ||||
-rw-r--r-- | stm/vernac_classifier.ml | 4 | ||||
-rw-r--r-- | stm/vernac_classifier.mli | 2 | ||||
-rw-r--r-- | toplevel/vernacinterp.ml | 8 | ||||
-rw-r--r-- | toplevel/vernacinterp.mli | 6 |
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 |