summaryrefslogtreecommitdiff
path: root/grammar/vernacextend.mlp
diff options
context:
space:
mode:
Diffstat (limited to 'grammar/vernacextend.mlp')
-rw-r--r--grammar/vernacextend.mlp93
1 files changed, 64 insertions, 29 deletions
diff --git a/grammar/vernacextend.mlp b/grammar/vernacextend.mlp
index 04b117fb..a2872d07 100644
--- a/grammar/vernacextend.mlp
+++ b/grammar/vernacextend.mlp
@@ -1,17 +1,17 @@
(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
(** Implementation of the VERNAC EXTEND macro. *)
open Q_util
open Argextend
-open Tacextend
-open GramCompat
type rule = {
r_head : string option;
@@ -26,9 +26,24 @@ type rule = {
(** Whether this entry is deprecated *)
}
+(** Quotation difference for match clauses *)
+
+let default_patt loc =
+ (<:patt< _ >>, ploc_vala None, <:expr< failwith "Extension: cannot occur" >>)
+
+let make_fun loc cl =
+ let l = cl @ [default_patt loc] in
+ MLast.ExFun (loc, ploc_vala l) (* correspond to <:expr< fun [ $list:l$ ] >> *)
+
+let rec make_patt = function
+ | [] -> <:patt< [] >>
+ | ExtNonTerminal (_, Some p) :: l ->
+ <:patt< [ $lid:p$ :: $make_patt l$ ] >>
+ | _::l -> make_patt l
+
let rec make_let e = function
| [] -> e
- | ExtNonTerminal (g, p) :: l ->
+ | ExtNonTerminal (g, Some p) :: l ->
let t = type_of_user_symbol g in
let loc = MLast.loc_of_expr e in
let e = make_let e l in
@@ -37,13 +52,13 @@ let rec make_let e = function
let make_clause { r_patt = pt; r_branch = e; } =
(make_patt pt,
- vala None,
+ ploc_vala None,
make_let e pt)
(* To avoid warnings *)
let mk_ignore c pt =
let fold accu = function
- | ExtNonTerminal (_, p) -> p :: accu
+ | ExtNonTerminal (_, Some p) -> p :: accu
| _ -> accu
in
let names = List.fold_left fold [] pt in
@@ -55,12 +70,12 @@ let make_clause_classifier cg s { r_patt = pt; r_class = c; } =
match c ,cg with
| Some c, _ ->
(make_patt pt,
- vala None,
+ ploc_vala None,
make_let (mk_ignore c pt) pt)
| None, Some cg ->
(make_patt pt,
- vala None,
- <:expr< fun () -> $cg$ $str:s$ >>)
+ ploc_vala None,
+ <:expr< fun loc -> $cg$ $str:s$ >>)
| None, None -> prerr_endline
(("Vernac entry \""^s^"\" misses a classifier. "^
"A classifier is a function that returns an expression "^
@@ -82,8 +97,8 @@ let make_clause_classifier cg s { r_patt = pt; r_class = c; } =
("Specific classifiers have precedence over global "^
"classifiers. Only one classifier is called.") ^ "\n");
(make_patt pt,
- vala None,
- <:expr< fun () -> (Vernacexpr.VtUnknown, Vernacexpr.VtNow) >>)
+ ploc_vala None,
+ <:expr< fun () -> ( CErrors.anomaly (Pp.str "No classification given for command " ^ s ) ) >>)
let make_fun_clauses loc s l =
let map c =
@@ -91,22 +106,23 @@ let make_fun_clauses loc s l =
| None -> false
| Some () -> true
in
- let cl = GramCompat.make_fun loc [make_clause c] in
+ let cl = make_fun loc [make_clause c] in
<:expr< ($mlexpr_of_bool depr$, $cl$)>>
in
mlexpr_of_list map l
let make_fun_classifiers loc s c l =
- let cl = List.map (fun x -> GramCompat.make_fun loc [make_clause_classifier c s x]) l in
+ let cl = List.map (fun x -> make_fun loc [make_clause_classifier c s x]) l in
mlexpr_of_list (fun x -> x) cl
let make_prod_item = function
| ExtTerminal s -> <:expr< Egramml.GramTerminal $str:s$ >>
- | ExtNonTerminal (g, id) ->
+ | ExtNonTerminal (g, ido) ->
let nt = type_of_user_symbol g in
let base s = <:expr< Pcoq.genarg_grammar ($mk_extraarg loc s$) >> in
- <:expr< Egramml.GramNonTerminal $default_loc$ $make_rawwit loc nt$
- $mlexpr_of_prod_entry_key base g$ >>
+ let typ = match ido with None -> None | Some _ -> Some nt in
+ <:expr< Egramml.GramNonTerminal ( Loc.tag ( $mlexpr_of_option (make_rawwit loc) typ$ ,
+ $mlexpr_of_prod_entry_key base g$ ) ) >>
let mlexpr_of_clause cl =
let mkexpr { r_head = a; r_patt = b; } = match a with
@@ -128,7 +144,6 @@ let declare_command loc s c nt cl =
} >> ]
open Pcaml
-open PcamlSig (* necessary for camlp4 *)
EXTEND
GLOBAL: str_item;
@@ -137,6 +152,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" ->
@@ -144,7 +163,7 @@ EXTEND
| "DECLARE"; "PLUGIN"; name = STRING ->
declare_str_items loc [
<:str_item< value __coq_plugin_name = $str:name$ >>;
- <:str_item< value _ = Mltop.add_known_module $str:name$ >>;
+ <:str_item< value _ = Mltop.add_known_module __coq_plugin_name >>;
]
] ]
;
@@ -159,31 +178,47 @@ EXTEND
deprecation:
[ [ "DEPRECATED" -> () ] ]
;
- (* spiwack: comment-by-guessing: it seems that the isolated string (which
- otherwise could have been another argument) is not passed to the
- VernacExtend interpreter function to discriminate between the clauses. *)
+ (* spiwack: comment-by-guessing: it seems that the isolated string
+ (which otherwise could have been another argument) is not passed
+ to the VernacExtend interpreter function to discriminate between
+ the clauses. *)
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< fun () -> $e$ >> in
+ let b = <:expr< fun ~{atts} ~{st} -> ( let () = $e$ in st ) >> 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< fun ~{atts} ~{st} -> ( let () = $e$ in st ) >> in
+ { 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< fun () -> $e$ >> in
+ 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 () -> $c$>> ] ]
+ [ [ "=>"; "["; c = Pcaml.expr; "]" -> <:expr< fun loc -> $c$>> ] ]
;
args:
[ [ e = LIDENT; "("; s = LIDENT; ")" ->
let e = parse_user_entry e "" in
- ExtNonTerminal (e, s)
+ ExtNonTerminal (e, Some s)
| e = LIDENT; "("; s = LIDENT; ","; sep = STRING; ")" ->
let e = parse_user_entry e sep in
- ExtNonTerminal (e, s)
+ ExtNonTerminal (e, Some s)
+ | e = LIDENT ->
+ let e = parse_user_entry e "" in
+ ExtNonTerminal (e, None)
| s = STRING ->
ExtTerminal s
] ]
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-07 17:53:17 +0000