Skip to content

Commit

Permalink
Fixes #17985: Error on level of notation variable set more than once.
Browse files Browse the repository at this point in the history
In practice, it is enough to simplify the code for setting levels
thanks to the pre-parsing of the main entry in 359cac9.

Also, we reset the syntax modifiers in the natural order after having
parsed the non-syntax modifiers.
  • Loading branch information
herbelin committed Aug 29, 2023
1 parent e78e90d commit d9683e1
Show file tree
Hide file tree
Showing 3 changed files with 16 additions and 14 deletions.
3 changes: 3 additions & 0 deletions test-suite/output/wish_17985.out
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
File "./output/bug_17985.v", line 2, characters 75-91:
The command has indeed failed with message:
B is already assigned to an entry or constr level.
2 changes: 2 additions & 0 deletions test-suite/output/wish_17985.v
Original file line number Diff line number Diff line change
@@ -0,0 +1,2 @@
(* Do not accept B to be declared twice *)
Fail Reserved Notation "'<<<' A '>>>' e '<<<' B '>>>'" (A, B at level 200, e, B at level 55).
25 changes: 11 additions & 14 deletions vernac/metasyntax.ml
Original file line number Diff line number Diff line change
Expand Up @@ -981,24 +981,24 @@ let check_entry_type = function
| ETIdent | ETGlobal | ETBigint | ETName | ETBinder _-> ()

let interp_modifiers entry modl = let open NotationMods in
let rec interp subtyps acc = function
| [] -> subtyps, acc
let rec interp acc = function
| [] -> acc
| CAst.{loc;v} :: l -> match v with
| SetEntryType (s,typ) ->
let id = Id.of_string s in
check_entry_type typ;
if Id.List.mem_assoc id acc.etyps then
user_err ?loc
(str s ++ str " is already assigned to an entry or constr level.");
interp subtyps { acc with etyps = (id,typ) :: acc.etyps; } l
interp { acc with etyps = (id,typ) :: acc.etyps; } l
| SetItemLevel ([],bko,n) ->
interp subtyps acc l
interp acc l
| SetItemLevel (s::idl,bko,n) ->
let id = Id.of_string s in
if Id.List.mem_assoc id acc.etyps then
user_err ?loc
(str s ++ str " is already assigned to an entry or constr level.");
interp ((id,bko,n)::subtyps) acc ((CAst.make ?loc @@ SetItemLevel (idl,bko,n))::l)
interp { acc with etyps = (id,ETConstr (entry,bko,n)) :: acc.etyps } ((CAst.make ?loc @@ SetItemLevel (idl,bko,n))::l)
| SetLevel n ->
(match entry with
| InCustomEntry s ->
Expand All @@ -1012,24 +1012,20 @@ let interp_modifiers entry modl = let open NotationMods in
| InConstrEntry ->
if acc.level <> None then
user_err ?loc (str "A level is already assigned.");
interp subtyps { acc with level = Some n; } l)
interp { acc with level = Some n; } l)
| SetCustomEntry (s,Some n) ->
(* Note: name of entry already registered in interp_non_syntax_modifiers *)
if acc.level <> None then
user_err ?loc (str ("isolated \"at level " ^ string_of_int (Option.get acc.level) ^ "\" unexpected."));
interp subtyps { acc with level = Some n } l
interp { acc with level = Some n } l
| SetAssoc a ->
if not (Option.is_empty acc.assoc) then user_err ?loc Pp.(str "An associativity is given more than once.");
interp subtyps { acc with assoc = Some a; } l
interp { acc with assoc = Some a; } l
| SetOnlyParsing | SetOnlyPrinting | SetCustomEntry (_,None) | SetFormat _ | SetItemScope _ ->
(* interpreted in interp_non_syntax_modifiers *)
assert false
in
let subtyps, mods = interp [] default modl in
(* interpret item levels wrt to main entry *)
let extra_etyps = List.map (fun (id,bko,n) -> (id,ETConstr (entry,bko,n))) subtyps in
(* Temporary hack: "ETName false" (i.e. "ident" in deprecation phase) means "ETIdent" for custom entries *)
{ mods with etyps = extra_etyps@mods.etyps }
interp default modl

let check_useless_entry_types recvars mainvars etyps =
let vars = let (l1,l2) = List.split recvars in l1@l2@mainvars in
Expand Down Expand Up @@ -1115,7 +1111,8 @@ let interp_non_syntax_modifiers ~reserved ~infix ~abbrev deprecation mods =
entry = InConstrEntry; format = None; itemscopes = []
}
in
List.fold_left set (main_data,[]) mods
let main_data, rest = List.fold_left set (main_data,[]) mods in
main_data, List.rev rest

(* Compute precedences from modifiers (or find default ones) *)

Expand Down

0 comments on commit d9683e1

Please sign in to comment.