From d0a9edabf59a858625d11516cdb230d223a77aeb Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Tue, 31 May 2016 12:14:55 +0200 Subject: Yet another Makefile reform : a unique phase without nasty make tricks We're back to a unique build phase (as before e372b72), but without relying on the awkward include-deps-failed-lets-retry feature of make. Since PMP has made grammar/ self-contained, we could now build grammar.cma in a rather straightforward way, no need for a specific sub-call to $(MAKE) for that. The dependencies between files of grammar/ are stated explicitely, since .d files aren't fully available initially. Some Makefile simplifications, for instance remove the CAMLP4DEPS shell horror. Instead, we generalize the use of two different filename extensions : - a .mlp do not need grammar.cma (they are in grammar/ and tools/compat5*.mlp) - a .ml4 is now always preprocessed with grammar.cma (and q_constr.cmo), except coqide_main.ml4 and its specific rule Note that we do not generate .ml4.d anymore (thanks to the .mlp vs. .ml4 dichotomy) --- grammar/vernacextend.mlp | 198 +++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 198 insertions(+) create mode 100644 grammar/vernacextend.mlp (limited to 'grammar/vernacextend.mlp') diff --git a/grammar/vernacextend.mlp b/grammar/vernacextend.mlp new file mode 100644 index 000000000..fa8610fb9 --- /dev/null +++ b/grammar/vernacextend.mlp @@ -0,0 +1,198 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* 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 { + try 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$ } + with [ e when Errors.noncritical e -> + Pp.msg_warning + (Pp.app + (Pp.str ("Exception in vernac extend " ^ $se$ ^": ")) + (Errors.print e)) ]; + 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> l + | "VERNAC"; nt = LIDENT ; "EXTEND"; s = UIDENT; c = OPT classification; + OPT "|"; l = LIST1 rule SEP "|"; + "END" -> + declare_command loc s c <:expr> 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 +;; -- cgit v1.2.3