diff options
Diffstat (limited to 'grammar/vernacextend.mlp')
-rw-r--r-- | grammar/vernacextend.mlp | 93 |
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 ] ] |