1
(************************************************************************)
2
(* v * The Coq Proof Assistant / The Coq Development Team *)
3
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
4
(* \VV/ **************************************************************)
5
(* // * This file is distributed under the terms of the *)
6
(* * GNU Lesser General Public License Version 2.1 *)
7
(************************************************************************)
9
(*i camlp4use: "pa_extend.cmo q_MLast.cmo" i*)
11
(* $Id: vernacextend.ml4 11622 2008-11-23 08:45:56Z herbelin $ *)
19
let loc = Util.dummy_loc
20
let default_loc = <:expr< Util.dummy_loc >>
22
type grammar_tactic_production_expr =
23
| VernacTerm of string
24
| VernacNonTerm of Util.loc * Genarg.argument_type * MLast.expr * string option
25
let rec make_patt = function
27
| VernacNonTerm(_,_,_,Some p)::l ->
28
<:patt< [ $lid:p$ :: $make_patt l$ ] >>
31
let rec make_when loc = function
32
| [] -> <:expr< True >>
33
| VernacNonTerm(loc',t,_,Some p)::l ->
34
let l = make_when loc l in
35
let loc = join_loc loc' loc in
36
let t = mlexpr_of_argtype loc' t in
37
<:expr< Genarg.genarg_tag $lid:p$ = $t$ && $l$ >>
38
| _::l -> make_when loc l
40
let rec make_let e = function
42
| VernacNonTerm(loc,t,_,Some p)::l ->
43
let loc = join_loc loc (MLast.loc_of_expr e) in
44
let e = make_let e l in
45
<:expr< let $lid:p$ = Genarg.out_gen $make_rawwit loc t$ $lid:p$ in $e$ >>
46
| _::l -> make_let e l
48
let add_clause s (_,pt,e) l =
49
let p = make_patt pt in
50
let w = Some (make_when (MLast.loc_of_expr e) pt) in
51
(p, w, make_let e pt)::l
53
let rec extract_signature = function
55
| VernacNonTerm (_,t,_,_) :: l -> t :: extract_signature l
56
| _::l -> extract_signature l
58
let check_unicity s l =
59
let l' = List.map (fun (_,l,_) -> extract_signature l) l in
60
if not (Util.list_distinct l') then
61
Pp.warning_with !Pp_control.err_ft
62
("Two distinct rules of entry "^s^" have the same\n"^
63
"non-terminals in the same order: put them in distinct vernac entries")
65
let make_clauses s l =
68
(<:patt< _ >>,None,<:expr< failwith "Vernac extension: cannot occur" >>) in
69
List.fold_right (add_clause s) l [default]
71
let rec make_fun e = function
73
| VernacNonTerm(loc,_,_,Some p)::l ->
74
<:expr< fun $lid:p$ -> $make_fun e l$ >>
75
| _::l -> make_fun e l
77
let mlexpr_of_grammar_production = function
79
<:expr< Egrammar.TacTerm $mlexpr_of_string s$ >>
80
| VernacNonTerm (loc,nt,g,sopt) ->
81
<:expr< Egrammar.TacNonTerm $default_loc$ ($g$,$mlexpr_of_argtype loc nt$) $mlexpr_of_option mlexpr_of_string sopt$ >>
83
let mlexpr_of_clause =
86
mlexpr_of_list mlexpr_of_grammar_production (VernacTerm a::b))
88
let declare_command loc s cl =
89
let gl = mlexpr_of_clause cl in
90
let icl = make_clauses s cl in
94
try Vernacinterp.vinterp_add $mlexpr_of_string s$ (fun [ $list:icl$ ])
95
with e -> Pp.pp (Cerrors.explain_exn e);
96
Egrammar.extend_vernac_command_grammar $mlexpr_of_string s$ $gl$;
105
[ [ "VERNAC"; "COMMAND"; "EXTEND"; s = UIDENT;
106
OPT "|"; l = LIST1 rule SEP "|";
108
declare_command loc s l ] ]
111
[ [ "["; s = STRING; l = LIST0 args; "]"; "->"; "["; e = Pcaml.expr; "]"
113
if s = "" then Util.user_err_loc (loc,"",Pp.str"Command name is empty.");
114
(s,l,<:expr< fun () -> $e$ >>)
118
[ [ e = LIDENT; "("; s = LIDENT; ")" ->
119
let t, g = Q_util.interp_entry_name loc e "" in
120
VernacNonTerm (loc, t, g, Some s)
121
| e = LIDENT; "("; s = LIDENT; ","; sep = STRING; ")" ->
122
let t, g = Q_util.interp_entry_name loc e sep in
123
VernacNonTerm (loc, t, g, Some s)