diff options
Diffstat (limited to 'parsing/vernacextend.ml4')
| -rw-r--r-- | parsing/vernacextend.ml4 | 60 |
1 files changed, 32 insertions, 28 deletions
diff --git a/parsing/vernacextend.ml4 b/parsing/vernacextend.ml4 index 3f60aafa..88a75079 100644 --- a/parsing/vernacextend.ml4 +++ b/parsing/vernacextend.ml4 @@ -1,14 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i camlp4use: "pa_extend.cmo q_MLast.cmo" i*) - -(* $Id: vernacextend.ml4 14641 2011-11-06 11:59:10Z herbelin $ *) +(*i camlp4deps: "tools/compat5b.cmo" i*) open Util open Genarg @@ -18,6 +16,7 @@ open Argextend open Tacextend open Pcoq open Egrammar +open Compat let rec make_let e = function | [] -> e @@ -28,11 +27,6 @@ let rec make_let e = function <:expr< let $lid:p$ = Genarg.out_gen $make_rawwit loc t$ $lid:p$ in $e$ >> | _::l -> make_let e l -let add_clause s (_,pt,e) l = - let p = make_patt pt in - let w = Some (make_when (MLast.loc_of_expr e) pt) in - (p, <:vala<w>>, make_let e pt)::l - let check_unicity s l = let l' = List.map (fun (_,l,_) -> extract_signature l) l in if not (Util.list_distinct l') then @@ -40,31 +34,32 @@ let check_unicity s l = ("Two distinct rules of entry "^s^" have the same\n"^ "non-terminals in the same order: put them in distinct vernac entries") -let make_clauses s l = +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; - let default = - (<:patt< _ >>,<:vala<None>>, - <:expr< failwith "Vernac extension: cannot occur" >>) in - List.fold_right (add_clause s) l [default] + 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 (GramTerminal a::b)) + (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 cl = +let declare_command loc s nt cl = let gl = mlexpr_of_clause cl in - let icl = make_clauses s cl in - <:str_item< - declare - open Pcoq; - open Extrawit; - try Vernacinterp.vinterp_add $mlexpr_of_string s$ (fun [ $list:icl$ ]) - with e -> Pp.pp (Cerrors.explain_exn e); - Egrammar.extend_vernac_command_grammar $mlexpr_of_string s$ $gl$; - end - >> + let funcl = make_fun_clauses loc s cl in + declare_str_items loc + [ <:str_item< do { + try Vernacinterp.vinterp_add $mlexpr_of_string s$ $funcl$ + with e -> Pp.pp (Errors.print e); + Egrammar.extend_vernac_command_grammar $mlexpr_of_string s$ $nt$ $gl$ + } >> ] open Pcaml +open PcamlSig EXTEND GLOBAL: str_item; @@ -72,13 +67,22 @@ EXTEND [ [ "VERNAC"; "COMMAND"; "EXTEND"; s = UIDENT; OPT "|"; l = LIST1 rule SEP "|"; "END" -> - declare_command loc s l ] ] + 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."); - (s,l,<:expr< fun () -> $e$ >>) + (Some s,l,<:expr< fun () -> $e$ >>) + | "[" ; "-" ; l = LIST1 args ; "]" ; "->" ; "[" ; e = Pcaml.expr ; "]" -> + (None,l,<:expr< fun () -> $e$ >>) ] ] ; args: |