aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--grammar/argextend.ml440
-rw-r--r--grammar/q_util.ml44
-rw-r--r--grammar/q_util.mli4
-rw-r--r--grammar/tacextend.ml465
-rw-r--r--grammar/vernacextend.ml421
5 files changed, 66 insertions, 68 deletions
diff --git a/grammar/argextend.ml4 b/grammar/argextend.ml4
index 677daebfb..89a1cd8b8 100644
--- a/grammar/argextend.ml4
+++ b/grammar/argextend.ml4
@@ -45,7 +45,7 @@ let make_topwit loc arg = <:expr< Genarg.topwit $make_wit loc arg$ >>
let has_extraarg l =
let check = function
- | GramNonTerminal(_, t, _, _) ->
+ | ExtNonTerminal(EntryName (t, _), _) ->
begin match Genarg.unquote t with
| ExtraArgType _ -> true
| _ -> false
@@ -74,7 +74,7 @@ let rec get_empty_entry : type s a. (s, a) entry_key -> _ = function
let statically_known_possibly_empty s (prods,_) =
List.for_all (function
- | GramNonTerminal(_,t,e,_) ->
+ | ExtNonTerminal(EntryName (t, e), _) ->
begin match Genarg.unquote t with
| ExtraArgType s' ->
(* For ExtraArg we don't know (we'll have to test dynamically) *)
@@ -83,26 +83,26 @@ let statically_known_possibly_empty s (prods,_) =
| _ ->
is_possibly_empty e
end
- | GramTerminal _ ->
+ | ExtTerminal _ ->
(* This consumes a token for sure *) false)
prods
let possibly_empty_subentries loc (prods,act) =
- let bind_name p v e = match p with
- | None -> e
- | Some id ->
- let s = Names.Id.to_string id in <:expr< let $lid:s$ = $v$ in $e$ >> in
+ let bind_name id v e =
+ let s = Names.Id.to_string id in
+ <:expr< let $lid:s$ = $v$ in $e$ >>
+ in
let rec aux = function
| [] -> <:expr< let loc = $default_loc$ in let _ = loc in $act$ >>
- | GramNonTerminal(_,_,e,p) :: tl when is_possibly_empty e ->
- bind_name p (get_empty_entry e) (aux tl)
- | GramNonTerminal(_,t,_,p) :: tl ->
+ | ExtNonTerminal(EntryName (_, e), id) :: tl when is_possibly_empty e ->
+ bind_name id (get_empty_entry e) (aux tl)
+ | ExtNonTerminal(EntryName (t, _), id) :: tl ->
let t = match Genarg.unquote t with
| ExtraArgType _ as t -> t
| _ -> assert false
in
(* We check at runtime if extraarg s parses "epsilon" *)
- let s = match p with None -> "_" | Some id -> Names.Id.to_string id in
+ let s = Names.Id.to_string id in
<:expr< let $lid:s$ = match Genarg.default_empty_value $make_wit loc t$ with
[ None -> raise Exit
| Some v -> v ] in $aux tl$ >>
@@ -135,20 +135,20 @@ let make_possibly_empty_subentries loc s cl =
let make_act loc act pil =
let rec make = function
| [] -> <:expr< (fun loc -> $act$) >>
- | GramNonTerminal (_,t,_,Some p) :: tl ->
+ | ExtNonTerminal (EntryName (t, _), p) :: tl ->
let t = Genarg.unquote t in
let p = Names.Id.to_string p in
<:expr<
(fun $lid:p$ ->
let _ = Genarg.in_gen $make_rawwit loc t$ $lid:p$ in $make tl$)
>>
- | (GramTerminal _ | GramNonTerminal (_,_,_,None)) :: tl ->
+ | ExtTerminal _ :: tl ->
<:expr< (fun _ -> $make tl$) >> in
make (List.rev pil)
let make_prod_item = function
- | GramTerminal s -> <:expr< Pcoq.Atoken (Lexer.terminal $mlexpr_of_string s$) >>
- | GramNonTerminal (_,_,g,_) -> mlexpr_of_prod_entry_key g
+ | ExtTerminal s -> <:expr< Pcoq.Atoken (Lexer.terminal $mlexpr_of_string s$) >>
+ | ExtNonTerminal (EntryName (_, g), _) -> mlexpr_of_prod_entry_key g
let rec make_prod = function
| [] -> <:expr< Extend.Stop >>
@@ -315,15 +315,15 @@ EXTEND
;
genarg:
[ [ e = LIDENT; "("; s = LIDENT; ")" ->
- let EntryName (t, g) = interp_entry_name false TgAny e "" in
- GramNonTerminal (!@loc, t, g, Some (Names.Id.of_string s))
+ let entry = interp_entry_name false TgAny e "" in
+ ExtNonTerminal (entry, Names.Id.of_string s)
| e = LIDENT; "("; s = LIDENT; ","; sep = STRING; ")" ->
- let EntryName (t, g) = interp_entry_name false TgAny e sep in
- GramNonTerminal (!@loc, t, g, Some (Names.Id.of_string s))
+ let entry = interp_entry_name false TgAny e sep in
+ ExtNonTerminal (entry, Names.Id.of_string s)
| s = STRING ->
if String.length s > 0 && Util.is_letter s.[0] then
Lexer.add_keyword s;
- GramTerminal s
+ ExtTerminal s
] ]
;
entry_name:
diff --git a/grammar/q_util.ml4 b/grammar/q_util.ml4
index 76113ad50..4c1f25941 100644
--- a/grammar/q_util.ml4
+++ b/grammar/q_util.ml4
@@ -10,6 +10,10 @@
open Compat
+type extend_token =
+| ExtTerminal of string
+| ExtNonTerminal of unit Pcoq.entry_name * Names.Id.t
+
let mlexpr_of_list f l =
List.fold_right
(fun e1 e2 ->
diff --git a/grammar/q_util.mli b/grammar/q_util.mli
index d01fb1e9a..d9359de1e 100644
--- a/grammar/q_util.mli
+++ b/grammar/q_util.mli
@@ -8,6 +8,10 @@
open Compat (* necessary for camlp4 *)
+type extend_token =
+| ExtTerminal of string
+| ExtNonTerminal of unit Pcoq.entry_name * Names.Id.t
+
val mlexpr_of_list : ('a -> MLast.expr) -> 'a list -> MLast.expr
val mlexpr_of_pair :
diff --git a/grammar/tacextend.ml4 b/grammar/tacextend.ml4
index 01828267b..6069f4b4b 100644
--- a/grammar/tacextend.ml4
+++ b/grammar/tacextend.ml4
@@ -27,29 +27,26 @@ let plugin_name = <:expr< __coq_plugin_name >>
let rec make_patt = function
| [] -> <:patt< [] >>
- | GramNonTerminal(loc',_,_,Some p)::l ->
+ | ExtNonTerminal (_, p) :: l ->
let p = Names.Id.to_string p in
<:patt< [ $lid:p$ :: $make_patt l$ ] >>
| _::l -> make_patt l
let rec make_when loc = function
| [] -> <:expr< True >>
- | GramNonTerminal(loc',t,_,Some p)::l ->
- let loc' = of_coqloc loc' in
+ | ExtNonTerminal (EntryName (t, _), p) :: l ->
let p = Names.Id.to_string p in
let l = make_when loc l in
- let loc = CompatLoc.merge loc' loc in
- let t = mlexpr_of_argtype loc' (Genarg.unquote t) in
+ let t = mlexpr_of_argtype loc (Genarg.unquote t) in
<:expr< Genarg.argument_type_eq (Genarg.genarg_tag $lid:p$) $t$ && $l$ >>
| _::l -> make_when loc l
let rec make_let raw e = function
| [] -> <:expr< fun $lid:"ist"$ -> $e$ >>
- | GramNonTerminal(loc,t,_,Some p)::l ->
+ | ExtNonTerminal (EntryName (t, _), p) :: l ->
let t = Genarg.unquote t in
- let loc = of_coqloc loc in
let p = Names.Id.to_string p in
- let loc = CompatLoc.merge loc (MLast.loc_of_expr e) in
+ let loc = MLast.loc_of_expr e in
let e = make_let raw e l in
let v =
if raw then <:expr< Genarg.out_gen $make_rawwit loc t$ $lid:p$ >>
@@ -59,7 +56,7 @@ let rec make_let raw e = function
let rec extract_signature = function
| [] -> []
- | GramNonTerminal (_,t,_,_) :: l -> Genarg.unquote t :: extract_signature l
+ | ExtNonTerminal (EntryName (t, _), _) :: l -> Genarg.unquote t :: extract_signature l
| _::l -> extract_signature l
@@ -83,37 +80,32 @@ let make_fun_clauses loc s l =
let rec make_args = function
| [] -> <:expr< [] >>
- | GramNonTerminal(loc,t,_,Some p)::l ->
+ | ExtNonTerminal (EntryName (t, _), p) :: l ->
let t = Genarg.unquote t in
- let loc = of_coqloc loc in
let p = Names.Id.to_string p in
<:expr< [ Genarg.in_gen $make_topwit loc t$ $lid:p$ :: $make_args l$ ] >>
| _::l -> make_args l
let mlexpr_terminals_of_grammar_tactic_prod_item_expr = function
- | GramTerminal s -> <:expr< Some $mlexpr_of_string s$ >>
- | GramNonTerminal (loc,nt,_,sopt) ->
- let loc = of_coqloc loc in <:expr< None >>
+ | ExtTerminal s -> <:expr< Some $mlexpr_of_string s$ >>
+ | ExtNonTerminal _ -> <:expr< None >>
let make_prod_item = function
- | GramTerminal s -> <:expr< Egramml.GramTerminal $str:s$ >>
- | GramNonTerminal (loc,nt,g,sopt) ->
- let loc = of_coqloc loc in
+ | ExtTerminal s -> <:expr< Egramml.GramTerminal $str:s$ >>
+ | ExtNonTerminal (EntryName (nt, g), id) ->
let nt = Genarg.unquote nt in
<:expr< Egramml.GramNonTerminal $default_loc$ $make_rawwit loc nt$
- $mlexpr_of_prod_entry_key g$ $mlexpr_of_option mlexpr_of_ident sopt$ >>
+ $mlexpr_of_prod_entry_key g$ (Some $mlexpr_of_ident id$) >>
let mlexpr_of_clause cl =
mlexpr_of_list (fun (a,_,b) -> mlexpr_of_list make_prod_item a) cl
let rec make_tags loc = function
| [] -> <:expr< [] >>
- | GramNonTerminal(loc',t,_,Some p)::l ->
- let loc' = of_coqloc loc' in
+ | ExtNonTerminal (EntryName (t, _), p) :: l ->
let l = make_tags loc l in
- let loc = CompatLoc.merge loc' loc in
let t = Genarg.unquote t in
- let t = mlexpr_of_argtype loc' t in
+ let t = mlexpr_of_argtype loc t in
<:expr< [ $t$ :: $l$ ] >>
| _::l -> make_tags loc l
@@ -127,7 +119,7 @@ let make_one_printing_rule (pt,_,e) =
let make_printing_rule r = mlexpr_of_list make_one_printing_rule r
let make_empty_check = function
-| GramNonTerminal(_, t, e, _)->
+| ExtNonTerminal (EntryName (t, e), _)->
let t = Genarg.unquote t in
let is_extra = match t with ExtraArgType _ -> true | _ -> false in
if is_possibly_empty e || is_extra then
@@ -143,16 +135,16 @@ let make_empty_check = function
else
(* This does not parse epsilon (this Exit is static time) *)
raise Exit
-| GramTerminal _ ->
+| ExtTerminal _ ->
(* Idem *)
raise Exit
let rec possibly_atomic loc = function
| [] -> []
-| ((GramNonTerminal _ :: _ | []), _, _) :: rem ->
+| ((ExtNonTerminal _ :: _ | []), _, _) :: rem ->
(** This is not parsed by the TACTIC EXTEND rules *)
assert false
-| (GramTerminal s :: prods, _, _) :: rem ->
+| (ExtTerminal s :: prods, _, _) :: rem ->
let entry =
try
let l = List.map make_empty_check prods in
@@ -164,8 +156,8 @@ let rec possibly_atomic loc = function
(** Special treatment of constr entries *)
let is_constr_gram = function
-| GramTerminal _ -> false
-| GramNonTerminal (_, _, e, _) ->
+| ExtTerminal _ -> false
+| ExtNonTerminal (EntryName (_, e), _) ->
match e with
| Aentry e ->
begin match Entry.repr e with
@@ -175,12 +167,11 @@ let is_constr_gram = function
| _ -> false
let make_var = function
- | GramNonTerminal(loc',_,_,Some p) -> Some p
- | GramNonTerminal(loc',_,_,None) -> Some (Id.of_string "_")
+ | ExtNonTerminal (_, p) -> Some p
| _ -> assert false
let declare_tactic loc s c cl = match cl with
-| [(GramTerminal name) :: rem, _, tac] when List.for_all is_constr_gram rem ->
+| [(ExtTerminal name) :: rem, _, tac] when List.for_all is_constr_gram rem ->
(** The extension is only made of a name followed by constr entries: we do not
add any grammar nor printing rule and add it as a true Ltac definition. *)
let patt = make_patt rem in
@@ -258,7 +249,7 @@ EXTEND
c = OPT [ "=>"; "["; c = Pcaml.expr; "]" -> c ];
"->"; "["; e = Pcaml.expr; "]" ->
(match l with
- | GramNonTerminal _ :: _ ->
+ | ExtNonTerminal _ :: _ ->
(* En attendant la syntaxe de tacticielles *)
failwith "Tactic syntax must start with an identifier"
| _ -> (l,c,e))
@@ -266,14 +257,14 @@ EXTEND
;
tacargs:
[ [ e = LIDENT; "("; s = LIDENT; ")" ->
- let EntryName (t, g) = interp_entry_name false TgAny e "" in
- GramNonTerminal (!@loc, t, g, Some (Names.Id.of_string s))
+ let entry = interp_entry_name false TgAny e "" in
+ ExtNonTerminal (entry, Names.Id.of_string s)
| e = LIDENT; "("; s = LIDENT; ","; sep = STRING; ")" ->
- let EntryName (t, g) = interp_entry_name false TgAny e sep in
- GramNonTerminal (!@loc, t, g, Some (Names.Id.of_string s))
+ let entry = interp_entry_name false TgAny e sep in
+ ExtNonTerminal (entry, Names.Id.of_string s)
| s = STRING ->
if String.is_empty s then Errors.user_err_loc (!@loc,"",Pp.str "Empty terminal.");
- GramTerminal s
+ ExtTerminal s
] ]
;
tac_name:
diff --git a/grammar/vernacextend.ml4 b/grammar/vernacextend.ml4
index 54638556d..8de59e5cd 100644
--- a/grammar/vernacextend.ml4
+++ b/grammar/vernacextend.ml4
@@ -22,7 +22,7 @@ open Compat
type rule = {
r_head : string option;
(** The first terminal grammar token *)
- r_patt : Vernacexpr.vernac_expr grammar_prod_item list;
+ r_patt : extend_token list;
(** The remaining tokens of the parsing rule *)
r_class : MLast.expr option;
(** An optional classifier for the STM *)
@@ -34,11 +34,10 @@ type rule = {
let rec make_let e = function
| [] -> e
- | GramNonTerminal(loc,t,_,Some p)::l ->
+ | ExtNonTerminal (EntryName (t, _), p) :: l ->
let t = Genarg.unquote t in
- let loc = of_coqloc loc in
let p = Names.Id.to_string p in
- let loc = CompatLoc.merge loc (MLast.loc_of_expr e) 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
@@ -51,7 +50,7 @@ let make_clause { r_patt = pt; r_branch = e; } =
(* To avoid warnings *)
let mk_ignore c pt =
let names = CList.map_filter (function
- | GramNonTerminal(_,_,_,Some p) -> Some (Names.Id.to_string p)
+ | ExtNonTerminal (_, p) -> Some (Names.Id.to_string p)
| _ -> None) pt in
let fold accu id = <:expr< let _ = $lid:id$ in $accu$ >> in
let names = List.fold_left fold <:expr< () >> names in
@@ -109,7 +108,7 @@ let make_fun_classifiers loc s c l =
let mlexpr_of_clause =
mlexpr_of_list
(fun { r_head = a; r_patt = b; } -> mlexpr_of_list make_prod_item
- (Option.List.cons (Option.map (fun a -> GramTerminal a) a) b))
+ (Option.List.cons (Option.map (fun a -> ExtTerminal a) a) b))
let declare_command loc s c nt cl =
let se = mlexpr_of_string s in
@@ -182,13 +181,13 @@ EXTEND
;
args:
[ [ e = LIDENT; "("; s = LIDENT; ")" ->
- let EntryName (t, g) = interp_entry_name false TgAny e "" in
- GramNonTerminal (!@loc, t, g, Some (Names.Id.of_string s))
+ let entry = interp_entry_name false TgAny e "" in
+ ExtNonTerminal (entry, Names.Id.of_string s)
| e = LIDENT; "("; s = LIDENT; ","; sep = STRING; ")" ->
- let EntryName (t, g) = interp_entry_name false TgAny e sep in
- GramNonTerminal (!@loc, t, g, Some (Names.Id.of_string s))
+ let entry = interp_entry_name false TgAny e sep in
+ ExtNonTerminal (entry, Names.Id.of_string s)
| s = STRING ->
- GramTerminal s
+ ExtTerminal s
] ]
;
END
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-20 00:18:29 +0000