aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--gramlib/gramext.ml72
-rw-r--r--gramlib/gramext.mli3
-rw-r--r--gramlib/grammar.ml99
-rw-r--r--gramlib/grammar.mli1
-rw-r--r--gramlib/plexing.ml4
-rw-r--r--gramlib/plexing.mli4
-rw-r--r--parsing/cLexer.ml1
-rw-r--r--vernac/attributes.ml19
-rw-r--r--vernac/attributes.mli17
-rw-r--r--vernac/vernacentries.ml40
10 files changed, 42 insertions, 218 deletions
diff --git a/gramlib/gramext.ml b/gramlib/gramext.ml
index c35c4bd18e..46c2688f05 100644
--- a/gramlib/gramext.ml
+++ b/gramlib/gramext.ml
@@ -8,7 +8,7 @@ type 'a parser_t = 'a Stream.t -> Obj.t
type 'te grammar =
{ gtokens : (Plexing.pattern, int ref) Hashtbl.t;
- mutable glexer : 'te Plexing.lexer }
+ glexer : 'te Plexing.lexer }
type 'te g_entry =
{ egram : 'te grammar;
@@ -52,7 +52,6 @@ type position =
| Last
| Before of string
| After of string
- | Like of string
| Level of string
let rec derive_eps =
@@ -154,27 +153,6 @@ let is_level_labelled n lev =
Some n1 -> n = n1
| None -> false
-let rec token_exists_in_level f lev =
- token_exists_in_tree f lev.lprefix || token_exists_in_tree f lev.lsuffix
-and token_exists_in_tree f =
- function
- Node n ->
- token_exists_in_symbol f n.node || token_exists_in_tree f n.brother ||
- token_exists_in_tree f n.son
- | LocAct (_, _) | DeadEnd -> false
-and token_exists_in_symbol f =
- function
- | Slist0 sy -> token_exists_in_symbol f sy
- | Slist0sep (sy, sep, _) ->
- token_exists_in_symbol f sy || token_exists_in_symbol f sep
- | Slist1 sy -> token_exists_in_symbol f sy
- | Slist1sep (sy, sep, _) ->
- token_exists_in_symbol f sy || token_exists_in_symbol f sep
- | Sopt sy -> token_exists_in_symbol f sy
- | Stoken tok -> f tok
- | Stree t -> token_exists_in_tree f t
- | Snterm _ | Snterml (_, _) | Snext | Sself -> false
-
let insert_level ~warning entry_name e1 symbols action slev =
match e1 with
true ->
@@ -265,58 +243,11 @@ let get_level ~warning entry position levs =
let (levs1, rlev, levs2) = get levs in lev :: levs1, rlev, levs2
in
get levs
- | Some (Like n) ->
- let f (tok, prm) = n = tok || n = prm in
- let rec get =
- function
- [] ->
- eprintf "No level with \"%s\" in entry \"%s\"\n" n entry.ename;
- flush stderr;
- failwith "Grammar.extend"
- | lev :: levs ->
- if token_exists_in_level f lev then [], change_lev ~warning lev n, levs
- else
- let (levs1, rlev, levs2) = get levs in lev :: levs1, rlev, levs2
- in
- get levs
| None ->
match levs with
lev :: levs -> [], change_lev ~warning lev "<top>", levs
| [] -> [], empty_lev, []
-let rec check_gram entry =
- function
- Snterm e ->
- if e.egram != entry.egram then
- begin
- eprintf "\
-Error: entries \"%s\" and \"%s\" do not belong to the same grammar.\n"
- entry.ename e.ename;
- flush stderr;
- failwith "Grammar.extend error"
- end
- | Snterml (e, _) ->
- if e.egram != entry.egram then
- begin
- eprintf "\
-Error: entries \"%s\" and \"%s\" do not belong to the same grammar.\n"
- entry.ename e.ename;
- flush stderr;
- failwith "Grammar.extend error"
- end
- | Slist0sep (s, t, _) -> check_gram entry t; check_gram entry s
- | Slist1sep (s, t, _) -> check_gram entry t; check_gram entry s
- | Slist0 s -> check_gram entry s
- | Slist1 s -> check_gram entry s
- | Sopt s -> check_gram entry s
- | Stree t -> tree_check_gram entry t
- | Snext | Sself | Stoken _ -> ()
-and tree_check_gram entry =
- function
- Node {node = n; brother = bro; son = son} ->
- check_gram entry n; tree_check_gram entry bro; tree_check_gram entry son
- | LocAct (_, _) | DeadEnd -> ()
-
let change_to_self entry =
function
Snterm e when e == entry -> Sself
@@ -373,7 +304,6 @@ let levels_of_rules ~warning entry position rules =
List.fold_left
(fun lev (symbols, action) ->
let symbols = List.map (change_to_self entry) symbols in
- List.iter (check_gram entry) symbols;
let (e1, symbols) = get_initial entry symbols in
insert_tokens entry.egram symbols;
insert_level ~warning entry.ename e1 symbols action lev)
diff --git a/gramlib/gramext.mli b/gramlib/gramext.mli
index ecb95ec61b..f1e294fb4c 100644
--- a/gramlib/gramext.mli
+++ b/gramlib/gramext.mli
@@ -6,7 +6,7 @@ type 'a parser_t = 'a Stream.t -> Obj.t
type 'te grammar =
{ gtokens : (Plexing.pattern, int ref) Hashtbl.t;
- mutable glexer : 'te Plexing.lexer }
+ glexer : 'te Plexing.lexer }
type 'te g_entry =
{ egram : 'te grammar;
@@ -50,7 +50,6 @@ type position =
| Last
| Before of string
| After of string
- | Like of string
| Level of string
val levels_of_rules : warning:(string -> unit) option ->
diff --git a/gramlib/grammar.ml b/gramlib/grammar.ml
index 8f7953b714..0ad11d075f 100644
--- a/gramlib/grammar.ml
+++ b/gramlib/grammar.ml
@@ -186,84 +186,6 @@ and name_of_tree_failed entry =
end
| DeadEnd | LocAct (_, _) -> "???"
-let search_tree_in_entry prev_symb tree =
- function
- Dlevels levels ->
- let rec search_levels =
- function
- [] -> tree
- | level :: levels ->
- match search_level level with
- Some tree -> tree
- | None -> search_levels levels
- and search_level level =
- match search_tree level.lsuffix with
- Some t -> Some (Node {node = Sself; son = t; brother = DeadEnd})
- | None -> search_tree level.lprefix
- and search_tree t =
- if tree <> DeadEnd && t == tree then Some t
- else
- match t with
- Node n ->
- begin match search_symbol n.node with
- Some symb ->
- Some (Node {node = symb; son = n.son; brother = DeadEnd})
- | None ->
- match search_tree n.son with
- Some t ->
- Some (Node {node = n.node; son = t; brother = DeadEnd})
- | None -> search_tree n.brother
- end
- | LocAct (_, _) | DeadEnd -> None
- and search_symbol symb =
- match symb with
- Snterm _ | Snterml (_, _) | Slist0 _ | Slist0sep (_, _, _) |
- Slist1 _ | Slist1sep (_, _, _) | Sopt _ | Stoken _ | Stree _
- when symb == prev_symb ->
- Some symb
- | Slist0 symb ->
- begin match search_symbol symb with
- Some symb -> Some (Slist0 symb)
- | None -> None
- end
- | Slist0sep (symb, sep, b) ->
- begin match search_symbol symb with
- Some symb -> Some (Slist0sep (symb, sep, b))
- | None ->
- match search_symbol sep with
- Some sep -> Some (Slist0sep (symb, sep, b))
- | None -> None
- end
- | Slist1 symb ->
- begin match search_symbol symb with
- Some symb -> Some (Slist1 symb)
- | None -> None
- end
- | Slist1sep (symb, sep, b) ->
- begin match search_symbol symb with
- Some symb -> Some (Slist1sep (symb, sep, b))
- | None ->
- match search_symbol sep with
- Some sep -> Some (Slist1sep (symb, sep, b))
- | None -> None
- end
- | Sopt symb ->
- begin match search_symbol symb with
- Some symb -> Some (Sopt symb)
- | None -> None
- end
- | Stree t ->
- begin match search_tree t with
- Some t -> Some (Stree t)
- | None -> None
- end
- | _ -> None
- in
- search_levels levels
- | Dparser _ -> tree
-
-let error_verbose = ref false
-
let tree_failed entry prev_symb_result prev_symb tree =
let txt = name_of_tree_failed entry tree in
let txt =
@@ -295,18 +217,6 @@ let tree_failed entry prev_symb_result prev_symb tree =
| Sopt _ | Stree _ -> txt ^ " expected"
| _ -> txt ^ " expected after " ^ name_of_symbol_failed entry prev_symb
in
- if !error_verbose then
- begin let tree = search_tree_in_entry prev_symb tree entry.edesc in
- let ppf = err_formatter in
- fprintf ppf "@[<v 0>@,";
- fprintf ppf "----------------------------------@,";
- fprintf ppf "Parse error in entry [%s], rule:@;<0 2>" entry.ename;
- fprintf ppf "@[";
- print_level ppf pp_force_newline (flatten_tree tree);
- fprintf ppf "@]@,";
- fprintf ppf "----------------------------------@,";
- fprintf ppf "@]@."
- end;
txt ^ " (in [" ^ entry.ename ^ "])"
let symb_failed entry prev_symb_result prev_symb symb =
@@ -374,11 +284,8 @@ let do_recover parser_of_tree entry nlevn alevn bp a s son
continue entry bp a s son (parser_of_tree entry nlevn alevn son)
strm__
-let strict_parsing = ref false
-
let recover parser_of_tree entry nlevn alevn bp a s son strm =
- if !strict_parsing then raise (Stream.Error (tree_failed entry a s son))
- else do_recover parser_of_tree entry nlevn alevn bp a s son strm
+ do_recover parser_of_tree entry nlevn alevn bp a s son strm
let token_count = ref 0
@@ -794,8 +701,6 @@ let tokens g con =
g.gtokens;
!list
-let glexer g = g.glexer
-
type 'te gen_parsable =
{ pa_chr_strm : char Stream.t;
pa_tok_strm : 'te Stream.t;
@@ -851,7 +756,6 @@ module type S =
type parsable
val parsable : char Stream.t -> parsable
val tokens : string -> (string * int) list
- val glexer : te Plexing.lexer
module Entry :
sig
type 'a e
@@ -906,7 +810,6 @@ module GMake (L : GLexerType) =
let (ts, lf) = L.lexer.Plexing.tok_func cs in
{pa_chr_strm = cs; pa_tok_strm = ts; pa_loc_func = lf}
let tokens = tokens gram
- let glexer = glexer gram
module Entry =
struct
type 'a e = te g_entry
diff --git a/gramlib/grammar.mli b/gramlib/grammar.mli
index 4b61286859..bde07ddc48 100644
--- a/gramlib/grammar.mli
+++ b/gramlib/grammar.mli
@@ -25,7 +25,6 @@ module type S =
type parsable
val parsable : char Stream.t -> parsable
val tokens : string -> (string * int) list
- val glexer : te Plexing.lexer
module Entry :
sig
type 'a e
diff --git a/gramlib/plexing.ml b/gramlib/plexing.ml
index 7b8618fd20..f99a3c2480 100644
--- a/gramlib/plexing.ml
+++ b/gramlib/plexing.ml
@@ -13,6 +13,6 @@ type 'te lexer =
{ tok_func : 'te lexer_func;
tok_using : pattern -> unit;
tok_removing : pattern -> unit;
- mutable tok_match : pattern -> 'te -> string;
+ tok_match : pattern -> 'te -> string;
tok_text : pattern -> string;
- mutable tok_comm : Loc.t list option }
+ }
diff --git a/gramlib/plexing.mli b/gramlib/plexing.mli
index 63c89dac28..eed4082e00 100644
--- a/gramlib/plexing.mli
+++ b/gramlib/plexing.mli
@@ -28,9 +28,9 @@ type 'te lexer =
{ tok_func : 'te lexer_func;
tok_using : pattern -> unit;
tok_removing : pattern -> unit;
- mutable tok_match : pattern -> 'te -> string;
+ tok_match : pattern -> 'te -> string;
tok_text : pattern -> string;
- mutable tok_comm : Loc.t list option }
+ }
and 'te lexer_func = char Stream.t -> 'te Stream.t * location_function
and location_function = int -> Loc.t
(** The type of a function giving the location of a token in the
diff --git a/parsing/cLexer.ml b/parsing/cLexer.ml
index c327f8aa43..c2b7fa117d 100644
--- a/parsing/cLexer.ml
+++ b/parsing/cLexer.ml
@@ -763,7 +763,6 @@ let lexer = {
| _ -> ());
Plexing.tok_removing = (fun _ -> ());
Plexing.tok_match = Tok.match_pattern;
- Plexing.tok_comm = None;
Plexing.tok_text = token_text }
(** Terminal symbols interpretation *)
diff --git a/vernac/attributes.ml b/vernac/attributes.ml
index 75ca027332..4f238f38e6 100644
--- a/vernac/attributes.ml
+++ b/vernac/attributes.ml
@@ -78,14 +78,6 @@ type deprecation = { since : string option ; note : string option }
let mk_deprecation ?(since=None) ?(note=None) () =
{ since ; note }
-type t = {
- locality : bool option;
- polymorphic : bool;
- template : bool option;
- program : bool;
- deprecated : deprecation option;
-}
-
let assert_empty k v =
if v <> VernacFlagEmpty
then user_err Pp.(str "Attribute " ++ str k ++ str " does not accept arguments")
@@ -181,10 +173,9 @@ let polymorphic_nowarn =
universe_transform ~warn_unqualified:false >>
qualify_attribute ukey polymorphic_base
-let universe_poly_template =
- let template = bool_attribute ~name:"Template" ~on:"template" ~off:"notemplate" in
+let template =
universe_transform ~warn_unqualified:true >>
- qualify_attribute ukey (polymorphic_base ++ template)
+ qualify_attribute ukey (bool_attribute ~name:"Template" ~on:"template" ~off:"notemplate")
let polymorphic =
universe_transform ~warn_unqualified:true >>
@@ -207,12 +198,6 @@ let deprecation_parser : deprecation key_parser = fun orig args ->
let deprecation = attribute_of_list ["deprecated",deprecation_parser]
-let attributes_of_flags f =
- let ((locality, deprecated), (polymorphic, template)), program =
- parse (locality ++ deprecation ++ universe_poly_template ++ program) f
- in
- { polymorphic; program; locality; template; deprecated }
-
let only_locality atts = parse locality atts
let only_polymorphism atts = parse polymorphic atts
diff --git a/vernac/attributes.mli b/vernac/attributes.mli
index c2dde4cbcc..6a32960a9d 100644
--- a/vernac/attributes.mli
+++ b/vernac/attributes.mli
@@ -49,28 +49,13 @@ val mk_deprecation : ?since: string option -> ?note: string option -> unit -> de
val polymorphic : bool attribute
val program : bool attribute
-val universe_poly_template : (bool * bool option) attribute
+val template : bool option attribute
val locality : bool option attribute
val deprecation : deprecation option attribute
val program_opt : bool option attribute
(** For internal use when messing with the global option. *)
-type t = {
- locality : bool option;
- polymorphic : bool;
- template : bool option;
- program : bool;
- deprecated : deprecation option;
-}
-(** Some attributes gathered in a adhoc record. Will probably be
- removed at some point. *)
-
-val attributes_of_flags : vernac_flags -> t
-(** Parse the attributes supported by type [t]. Errors on other
- attributes. Polymorphism and Program use the global flags as
- default values. *)
-
val only_locality : vernac_flags -> bool option
(** Parse attributes allowing only locality. *)
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 632df20592..f5d68a2199 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -52,6 +52,23 @@ let cl_of_qualid = function
let scope_class_of_qualid qid =
Notation.scope_class_of_class (cl_of_qualid qid)
+(** Standard attributes for definition-like commands. *)
+module DefAttributes = struct
+ type t = {
+ locality : bool option;
+ polymorphic : bool;
+ program : bool;
+ deprecated : deprecation option;
+ }
+
+ let parse f =
+ let open Attributes in
+ let ((locality, deprecated), polymorphic), program =
+ parse Notations.(locality ++ deprecation ++ polymorphic ++ program) f
+ in
+ { polymorphic; program; locality; deprecated }
+end
+
(*******************)
(* "Show" commands *)
@@ -509,7 +526,8 @@ let vernac_definition_hook p = function
| _ -> None
let vernac_definition ~atts discharge kind ({loc;v=id}, pl) def =
- let atts = attributes_of_flags atts in
+ let open DefAttributes in
+ let atts = parse atts in
let local = enforce_locality_exp atts.locality discharge in
let hook = vernac_definition_hook atts.polymorphic kind in
let () =
@@ -540,7 +558,8 @@ let vernac_definition ~atts discharge kind ({loc;v=id}, pl) def =
(local, atts.polymorphic, kind) pl bl red_option c typ_opt ?hook)
let vernac_start_proof ~atts kind l =
- let atts = attributes_of_flags atts in
+ let open DefAttributes in
+ let atts = parse atts in
let local = enforce_locality_exp atts.locality NoDischarge in
if Dumpglob.dump () then
List.iter (fun ((id, _), _) -> Dumpglob.dump_definition id false "prf") l;
@@ -558,7 +577,8 @@ let vernac_exact_proof c =
if not status then Feedback.feedback Feedback.AddedAxiom
let vernac_assumption ~atts discharge kind l nl =
- let atts = attributes_of_flags atts in
+ let open DefAttributes in
+ let atts = parse atts in
let local = enforce_locality_exp atts.locality discharge in
let global = local == Global in
let kind = local, atts.polymorphic, kind in
@@ -633,7 +653,9 @@ let extract_inductive_udecl (indl:(inductive_expr * decl_notation list) list) =
indicates whether the type is inductive, co-inductive or
neither. *)
let vernac_inductive ~atts cum lo finite indl =
- let atts = attributes_of_flags atts in
+ let open DefAttributes in
+ let atts, template = Attributes.(parse_with_extra template atts) in
+ let atts = parse atts in
let open Pp in
let udecl, indl = extract_inductive_udecl indl in
if Dumpglob.dump () then
@@ -658,7 +680,6 @@ let vernac_inductive ~atts cum lo finite indl =
| [ ( id , bl , c , Class _, Constructors [l]), [] ] -> Some (id, bl, c, l)
| _ -> None
in
- let template = atts.template in
if Option.has_some is_defclass then
(** Definitional class case *)
let (id, bl, c, l) = Option.get is_defclass in
@@ -729,7 +750,8 @@ let vernac_inductive ~atts cum lo finite indl =
*)
let vernac_fixpoint ~atts discharge l =
- let atts = attributes_of_flags atts in
+ let open DefAttributes in
+ let atts = parse atts in
let local = enforce_locality_exp atts.locality discharge in
if Dumpglob.dump () then
List.iter (fun (((lid,_), _, _, _, _), _) -> Dumpglob.dump_definition lid false "def") l;
@@ -742,7 +764,8 @@ let vernac_fixpoint ~atts discharge l =
do_fixpoint local atts.polymorphic l
let vernac_cofixpoint ~atts discharge l =
- let atts = attributes_of_flags atts in
+ let open DefAttributes in
+ let atts = parse atts in
let local = enforce_locality_exp atts.locality discharge in
if Dumpglob.dump () then
List.iter (fun (((lid,_), _, _, _), _) -> Dumpglob.dump_definition lid false "def") l;
@@ -983,7 +1006,8 @@ let vernac_identity_coercion ~atts id qids qidt =
(* Type classes *)
let vernac_instance ~atts abst sup inst props pri =
- let atts = attributes_of_flags atts in
+ let open DefAttributes in
+ let atts = parse atts in
let global = not (make_section_locality atts.locality) in
Dumpglob.dump_constraint (fst (pi1 inst)) false "inst";
let program_mode = Flags.is_program_mode () in
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-05 05:24:56 +0000