summaryrefslogtreecommitdiff
path: root/parsing/vernacextend.ml4
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <samuel.mimram@ens-lyon.org>2004-07-28 21:54:47 +0000
committerGravatar Samuel Mimram <samuel.mimram@ens-lyon.org>2004-07-28 21:54:47 +0000
commit6b649aba925b6f7462da07599fe67ebb12a3460e (patch)
tree43656bcaa51164548f3fa14e5b10de5ef1088574 /parsing/vernacextend.ml4
Imported Upstream version 8.0pl1upstream/8.0pl1
Diffstat (limited to 'parsing/vernacextend.ml4')
-rw-r--r--parsing/vernacextend.ml4162
1 files changed, 162 insertions, 0 deletions
diff --git a/parsing/vernacextend.ml4 b/parsing/vernacextend.ml4
new file mode 100644
index 00000000..bdc1ea66
--- /dev/null
+++ b/parsing/vernacextend.ml4
@@ -0,0 +1,162 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+(* $Id: vernacextend.ml4,v 1.5.2.2 2004/07/16 19:30:42 herbelin Exp $ *)
+
+open Genarg
+open Q_util
+open Q_coqast
+open Ast
+open Argextend
+
+let join_loc (deb1,_) (_,fin2) = (deb1,fin2)
+let loc = Util.dummy_loc
+let default_loc = <:expr< Util.dummy_loc >>
+
+type grammar_tactic_production_expr =
+ | VernacTerm of string
+ | VernacNonTerm of Util.loc * Genarg.argument_type * MLast.expr * string option
+let rec make_patt = function
+ | [] -> <:patt< [] >>
+ | VernacNonTerm(_,_,_,Some p)::l ->
+ <:patt< [ $lid:p$ :: $make_patt l$ ] >>
+ | _::l -> make_patt l
+
+let rec make_when loc = function
+ | [] -> <:expr< True >>
+ | VernacNonTerm(loc',t,_,Some p)::l ->
+ let l = make_when loc l in
+ let loc = join_loc loc' loc in
+ let t = mlexpr_of_argtype loc' t in
+ <:expr< Genarg.genarg_tag $lid:p$ = $t$ && $l$ >>
+ | _::l -> make_when loc l
+
+let rec make_let e = function
+ | [] -> e
+ | VernacNonTerm(loc,t,_,Some p)::l ->
+ 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 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, w, make_let e pt)::l
+
+let rec extract_signature = function
+ | [] -> []
+ | VernacNonTerm (_,t,_,_) :: l -> t :: extract_signature l
+ | _::l -> extract_signature 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_clauses s l =
+ check_unicity s l;
+ let default =
+ (<:patt< _ >>,None,<:expr< failwith "Vernac extension: cannot occur" >>) in
+ List.fold_right (add_clause s) l [default]
+
+let rec make_fun e = function
+ | [] -> e
+ | VernacNonTerm(loc,_,_,Some p)::l ->
+ <:expr< fun $lid:p$ -> $make_fun e l$ >>
+ | _::l -> make_fun e l
+
+let mlexpr_of_grammar_production = function
+ | VernacTerm s ->
+ <:expr< Egrammar.TacTerm $mlexpr_of_string s$ >>
+ | VernacNonTerm (loc,nt,g,sopt) ->
+ <:expr< Egrammar.TacNonTerm $default_loc$ ($g$,$mlexpr_of_argtype loc nt$) $mlexpr_of_option mlexpr_of_string sopt$ >>
+
+let mlexpr_of_clause =
+ mlexpr_of_list
+ (fun (a,b,c) ->
+ (mlexpr_of_pair
+ mlexpr_of_string
+ (mlexpr_of_list mlexpr_of_grammar_production)
+ (a,b)))
+
+let declare_command loc s cl =
+ let gl = mlexpr_of_clause cl in
+ let icl = make_clauses s cl in
+ <:str_item<
+ declare
+ open Pcoq;
+ 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
+ >>
+
+open Vernacexpr
+open Pcoq
+
+let rec interp_entry_name loc s =
+ let l = String.length s in
+ if l > 8 & String.sub s 0 3 = "ne_" & String.sub s (l-5) 5 = "_list" then
+ let t, g = interp_entry_name loc (String.sub s 3 (l-8)) in
+ List1ArgType t, <:expr< Gramext.Slist1 $g$ >>
+ else if l > 5 & String.sub s (l-5) 5 = "_list" then
+ let t, g = interp_entry_name loc (String.sub s 0 (l-5)) in
+ List0ArgType t, <:expr< Gramext.Slist0 $g$ >>
+ else if l > 4 & String.sub s (l-4) 4 = "_opt" then
+ let t, g = interp_entry_name loc (String.sub s 0 (l-4)) in
+ OptArgType t, <:expr< Gramext.Sopt $g$ >>
+ else
+ let t, se =
+ match Pcoq.entry_type (Pcoq.get_univ "prim") s with
+ | Some _ as x -> x, <:expr< Prim. $lid:s$ >>
+ | None ->
+ match Pcoq.entry_type (Pcoq.get_univ "constr") s with
+ | Some _ as x -> x, <:expr< Constr. $lid:s$ >>
+ | None ->
+ match Pcoq.entry_type (Pcoq.get_univ "tactic") s with
+ | Some _ as x -> x, <:expr< Tactic. $lid:s$ >>
+ | None -> None, <:expr< $lid:s$ >> in
+ let t =
+ match t with
+ | Some t -> t
+ | None ->
+(* Pp.warning_with Pp_control.err_ft
+ ("Unknown primitive grammar entry: "^s);*)
+ ExtraArgType s
+ in t, <:expr< Gramext.Snterm (Pcoq.Gram.Entry.obj $se$) >>
+
+open Pcaml
+
+EXTEND
+ GLOBAL: str_item;
+ str_item:
+ [ [ "VERNAC"; "COMMAND"; "EXTEND"; s = UIDENT;
+ OPT "|"; l = LIST1 rule SEP "|";
+ "END" ->
+ declare_command loc s l ] ]
+ ;
+ 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$ >>)
+ ] ]
+ ;
+ args:
+ [ [ e = LIDENT; "("; s = LIDENT; ")" ->
+ let t, g = interp_entry_name loc e in
+ VernacNonTerm (loc, t, g, Some s)
+ | s = STRING ->
+ VernacTerm s
+ ] ]
+ ;
+ END
+;;