diff options
Diffstat (limited to 'grammar/vernacextend.mlp')
| -rw-r--r-- | grammar/vernacextend.mlp | 115 |
1 files changed, 0 insertions, 115 deletions
diff --git a/grammar/vernacextend.mlp b/grammar/vernacextend.mlp deleted file mode 100644 index d44eeef670..0000000000 --- a/grammar/vernacextend.mlp +++ /dev/null @@ -1,115 +0,0 @@ -(************************************************************************) -(* * 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 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -(** Implementation of the VERNAC EXTEND macro. *) - -open Q_util -open Argextend - -type rule = { - r_patt : extend_token list; - (** The remaining tokens of the parsing rule *) - r_class : MLast.expr option; - (** An optional classifier for the STM *) - r_branch : MLast.expr; - (** The action performed by this rule. *) - r_depr : bool; - (** Whether this entry is deprecated *) -} - -let rec mlexpr_of_clause = function -| [] -> <:expr< Vernacextend.TyNil >> -| ExtTerminal s :: cl -> <:expr< Vernacextend.TyTerminal ($str:s$, $mlexpr_of_clause cl$) >> -| ExtNonTerminal (g, id) :: cl -> - <:expr< Vernacextend.TyNonTerminal ($mlexpr_of_symbol g$, $mlexpr_of_clause cl$) >> - -let make_rule r = - let ty = mlexpr_of_clause r.r_patt in - let cmd = binders_of_tokens r.r_branch r.r_patt in - let make_classifier c = binders_of_tokens c r.r_patt in - let classif = mlexpr_of_option make_classifier r.r_class in - <:expr< Vernacextend.TyML ($mlexpr_of_bool r.r_depr$, $ty$, $cmd$, $classif$) >> - -let declare_command loc s c nt cl = - let se = mlexpr_of_string s in - let c = mlexpr_of_option (fun x -> x) c in - let rules = mlexpr_of_list make_rule cl in - declare_str_items loc - [ <:str_item< Vernacextend.vernac_extend ?{ classifier = $c$ } ~{ command = $se$ } ?{ entry = $nt$ } $rules$ >> ] - -open Pcaml - -EXTEND - GLOBAL: str_item; - str_item: - [ [ "VERNAC"; "COMMAND"; "EXTEND"; s = UIDENT; c = OPT classification; - 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" -> - declare_command loc s c <:expr<Some $lid:nt$>> l - | "DECLARE"; "PLUGIN"; name = STRING -> - declare_str_items loc [ - <:str_item< value __coq_plugin_name = $str:name$ >>; - <:str_item< value _ = Mltop.add_known_module __coq_plugin_name >>; - ] - ] ] - ; - classification: - [ [ "CLASSIFIED"; "BY"; c = LIDENT -> <:expr< $lid:c$ >> - | "CLASSIFIED"; "AS"; "SIDEFF" -> - <:expr< fun _ -> Vernac_classifier.classify_as_sideeff >> - | "CLASSIFIED"; "AS"; "QUERY" -> - <:expr< fun _ -> Vernac_classifier.classify_as_query >> - ] ] - ; - deprecation: - [ [ -> false | "DEPRECATED" -> true ] ] - ; - rule: - [ [ "["; OPT "-"; l = LIST1 args; "]"; - d = deprecation; c = OPT classifier; "->"; "["; e = Pcaml.expr; "]" -> - let b = <:expr< fun ~{atts} ~{st} -> ( let () = $e$ in st ) >> in - { r_patt = l; r_class = c; r_branch = b; r_depr = d; } - ] ] - ; - (** The [OPT "-"] argument serves no purpose nowadays, it is left here for - backward compatibility. *) - fun_rule: - [ [ "["; OPT "-"; l = LIST1 args; "]"; - d = deprecation; c = OPT classifier; "->"; "["; e = Pcaml.expr; "]" -> - { r_patt = l; r_class = c; r_branch = e; r_depr = d; } - ] ] - ; - classifier: - [ [ "=>"; "["; c = Pcaml.expr; "]" -> <:expr< $c$>> ] ] - ; - args: - [ [ e = LIDENT; "("; s = LIDENT; ")" -> - let e = parse_user_entry e "" in - ExtNonTerminal (e, Some s) - | e = LIDENT; "("; s = LIDENT; ","; sep = STRING; ")" -> - let e = parse_user_entry e sep in - ExtNonTerminal (e, Some s) - | e = LIDENT -> - let e = parse_user_entry e "" in - ExtNonTerminal (e, None) - | s = STRING -> - ExtTerminal s - ] ] - ; - END -;; |