diff options
Diffstat (limited to 'parsing/vernacextend.ml4')
| -rw-r--r-- | parsing/vernacextend.ml4 | 105 |
1 files changed, 0 insertions, 105 deletions
diff --git a/parsing/vernacextend.ml4 b/parsing/vernacextend.ml4 deleted file mode 100644 index 1df5fbbd..00000000 --- a/parsing/vernacextend.ml4 +++ /dev/null @@ -1,105 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(*i camlp4deps: "tools/compat5b.cmo" i*) - -open Util -open Genarg -open Q_util -open Q_coqast -open Argextend -open Tacextend -open Pcoq -open Egrammar -open Compat - -let rec make_let e = function - | [] -> e - | GramNonTerminal(loc,t,_,Some p)::l -> - let p = Names.string_of_id p in - let loc = join_loc 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 check_unicity s l = - let l' = List.map (fun (_,l,_) -> extract_signature l) l in - if not (Util.list_distinct l') then - Pp.warning_with !Pp_control.err_ft - ("Two distinct rules of entry "^s^" have the same\n"^ - "non-terminals in the same order: put them in distinct vernac entries") - -let make_clause (_,pt,e) = - (make_patt pt, - vala (Some (make_when (MLast.loc_of_expr e) pt)), - make_let e pt) - -let make_fun_clauses loc s l = - check_unicity s l; - Compat.make_fun loc (List.map make_clause l) - -let mlexpr_of_clause = - mlexpr_of_list - (fun (a,b,c) -> mlexpr_of_list make_prod_item - (Option.List.cons (Option.map (fun a -> GramTerminal a) a) b)) - -let declare_command loc s 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 - declare_str_items loc - [ <:str_item< do { - try Vernacinterp.vinterp_add $se$ $funcl$ - with [ e when Errors.noncritical e -> - Pp.msg_warning - (Stream.iapp - (Pp.str ("Exception in vernac extend " ^ $se$ ^": ")) - (Errors.print e)) ]; - Egrammar.extend_vernac_command_grammar $se$ $nt$ $gl$ - } >> ] - -open Pcaml -open PcamlSig - -EXTEND - GLOBAL: str_item; - str_item: - [ [ "VERNAC"; "COMMAND"; "EXTEND"; s = UIDENT; - OPT "|"; l = LIST1 rule SEP "|"; - "END" -> - declare_command loc s <:expr<None>> l - | "VERNAC"; nt = LIDENT ; "EXTEND"; s = UIDENT; - OPT "|"; l = LIST1 rule SEP "|"; - "END" -> - declare_command loc s <:expr<Some $lid:nt$>> l ] ] - ; - (* 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; "]"; "->"; "["; e = Pcaml.expr; "]" - -> - if s = "" then Util.user_err_loc (loc,"",Pp.str"Command name is empty."); - (Some s,l,<:expr< fun () -> $e$ >>) - | "[" ; "-" ; l = LIST1 args ; "]" ; "->" ; "[" ; e = Pcaml.expr ; "]" -> - (None,l,<:expr< fun () -> $e$ >>) - ] ] - ; - args: - [ [ e = LIDENT; "("; s = LIDENT; ")" -> - let t, g = interp_entry_name false None e "" in - GramNonTerminal (loc, t, g, Some (Names.id_of_string s)) - | e = LIDENT; "("; s = LIDENT; ","; sep = STRING; ")" -> - let t, g = interp_entry_name false None e sep in - GramNonTerminal (loc, t, g, Some (Names.id_of_string s)) - | s = STRING -> - GramTerminal s - ] ] - ; - END -;; |