diff options
Diffstat (limited to 'grammar/vernacextend.mlp')
| -rw-r--r-- | grammar/vernacextend.mlp | 192 |
1 files changed, 192 insertions, 0 deletions
diff --git a/grammar/vernacextend.mlp b/grammar/vernacextend.mlp new file mode 100644 index 00000000..04b117fb --- /dev/null +++ b/grammar/vernacextend.mlp @@ -0,0 +1,192 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(** Implementation of the VERNAC EXTEND macro. *) + +open Q_util +open Argextend +open Tacextend +open GramCompat + +type rule = { + r_head : string option; + (** The first terminal grammar token *) + 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 : unit option; + (** Whether this entry is deprecated *) +} + +let rec make_let e = function + | [] -> e + | ExtNonTerminal (g, 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 + <:expr< let $lid:p$ = Genarg.out_gen $make_rawwit loc t$ $lid:p$ in $e$ >> + | _::l -> make_let e l + +let make_clause { r_patt = pt; r_branch = e; } = + (make_patt pt, + vala None, + make_let e pt) + +(* To avoid warnings *) +let mk_ignore c pt = + let fold accu = function + | ExtNonTerminal (_, p) -> p :: accu + | _ -> accu + in + let names = List.fold_left fold [] pt in + let fold accu id = <:expr< let _ = $lid:id$ in $accu$ >> in + let names = List.fold_left fold <:expr< () >> names in + <:expr< do { let _ = $names$ in $c$ } >> + +let make_clause_classifier cg s { r_patt = pt; r_class = c; } = + match c ,cg with + | Some c, _ -> + (make_patt pt, + vala None, + make_let (mk_ignore c pt) pt) + | None, Some cg -> + (make_patt pt, + vala None, + <:expr< fun () -> $cg$ $str:s$ >>) + | None, None -> prerr_endline + (("Vernac entry \""^s^"\" misses a classifier. "^ + "A classifier is a function that returns an expression "^ + "of type vernac_classification (see Vernacexpr). You can: ") ^ + "- " ^ ( + ("Use '... EXTEND "^s^" CLASSIFIED AS QUERY ...' if the "^ + "new vernacular command does not alter the system state;"))^ "\n" ^ + "- " ^ ( + ("Use '... EXTEND "^s^" CLASSIFIED AS SIDEFF ...' if the "^ + "new vernacular command alters the system state but not the "^ + "parser nor it starts a proof or ends one;"))^ "\n" ^ + "- " ^ ( + ("Use '... EXTEND "^s^" CLASSIFIED BY f ...' to specify "^ + "a global function f. The function f will be called passing "^ + "\""^s^"\" as the only argument;")) ^ "\n" ^ + "- " ^ ( + "Add a specific classifier in each clause using the syntax:" + ^ "\n" ^("'[...] => [ f ] -> [...]'. "))^ "\n" ^ + ("Specific classifiers have precedence over global "^ + "classifiers. Only one classifier is called.") ^ "\n"); + (make_patt pt, + vala None, + <:expr< fun () -> (Vernacexpr.VtUnknown, Vernacexpr.VtNow) >>) + +let make_fun_clauses loc s l = + let map c = + let depr = match c.r_depr with + | None -> false + | Some () -> true + in + let cl = GramCompat.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 + mlexpr_of_list (fun x -> x) cl + +let make_prod_item = function + | ExtTerminal s -> <:expr< Egramml.GramTerminal $str:s$ >> + | ExtNonTerminal (g, id) -> + 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 mlexpr_of_clause cl = + let mkexpr { r_head = a; r_patt = b; } = match a with + | None -> mlexpr_of_list make_prod_item b + | Some a -> mlexpr_of_list make_prod_item (ExtTerminal a :: b) + in + mlexpr_of_list mkexpr cl + +let declare_command loc s c nt cl = + let se = mlexpr_of_string s in + let gl = mlexpr_of_clause cl in + let funcl = make_fun_clauses loc s cl in + let classl = make_fun_classifiers loc s c cl in + declare_str_items loc + [ <:str_item< do { + CList.iteri (fun i (depr, f) -> Vernacinterp.vinterp_add depr ($se$, i) f) $funcl$; + CList.iteri (fun i f -> Vernac_classifier.declare_vernac_classifier ($se$, i) f) $classl$; + CList.iteri (fun i r -> Egramml.extend_vernac_command_grammar ($se$, i) $nt$ r) $gl$; + } >> ] + +open Pcaml +open PcamlSig (* necessary for camlp4 *) + +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"; 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 $str: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: + [ [ "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. *) + 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 + { 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 + { r_head = None; r_patt = l; r_class = c; r_branch = b; r_depr = d; } + ] ] + ; + classifier: + [ [ "=>"; "["; c = Pcaml.expr; "]" -> <:expr< fun () -> $c$>> ] ] + ; + args: + [ [ e = LIDENT; "("; s = LIDENT; ")" -> + let e = parse_user_entry e "" in + ExtNonTerminal (e, s) + | e = LIDENT; "("; s = LIDENT; ","; sep = STRING; ")" -> + let e = parse_user_entry e sep in + ExtNonTerminal (e, s) + | s = STRING -> + ExtTerminal s + ] ] + ; + END +;; |