aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--parsing/extend.ml3
-rw-r--r--parsing/notgram_ops.ml3
-rw-r--r--vernac/egramcoq.ml22
-rw-r--r--vernac/g_vernac.mlg19
-rw-r--r--vernac/metasyntax.ml19
-rw-r--r--vernac/ppvernac.ml18
-rw-r--r--vernac/vernacexpr.ml2
7 files changed, 47 insertions, 39 deletions
diff --git a/parsing/extend.ml b/parsing/extend.ml
index dcdaa25c33..848861238a 100644
--- a/parsing/extend.ml
+++ b/parsing/extend.ml
@@ -21,6 +21,7 @@ type production_position =
type production_level =
| NextLevel
| NumLevel of int
+ | DefaultLevel (** Interpreted differently at the border or inside a rule *)
(** User-level types used to tell how to parse or interpret of the non-terminal *)
@@ -40,7 +41,7 @@ type constr_entry_key =
(** Entries used in productions, vernac side (e.g. "x bigint" or "x ident") *)
type simple_constr_prod_entry_key =
- production_level option constr_entry_key_gen
+ production_level constr_entry_key_gen
(** Entries used in productions (in right-hand-side of grammar rules), to parse non-terminals *)
diff --git a/parsing/notgram_ops.ml b/parsing/notgram_ops.ml
index 009dafdb13..a5ade43295 100644
--- a/parsing/notgram_ops.ml
+++ b/parsing/notgram_ops.ml
@@ -48,7 +48,8 @@ let production_position_eq pp1 pp2 = match (pp1,pp2) with
let production_level_eq l1 l2 = match (l1,l2) with
| NextLevel, NextLevel -> true
| NumLevel n1, NumLevel n2 -> Int.equal n1 n2
-| (NextLevel | NumLevel _), _ -> false
+| DefaultLevel, DefaultLevel -> true
+| (NextLevel | NumLevel _ | DefaultLevel), _ -> false
let constr_entry_key_eq eq v1 v2 = match v1, v2 with
| ETIdent, ETIdent -> true
diff --git a/vernac/egramcoq.ml b/vernac/egramcoq.ml
index 2b6b18e058..1c1b59e397 100644
--- a/vernac/egramcoq.ml
+++ b/vernac/egramcoq.ml
@@ -208,29 +208,33 @@ let assoc_eq al ar =
Some None = NEXT
Some (Some (n,cur)) = constr LEVEL n *)
let adjust_level custom assoc (custom',from) p = let open Gramlib.Gramext in match p with
-(* If in a different grammar, no other choice than denoting it by absolute level *)
+(* If a level in a different grammar, no other choice than denoting it by absolute level *)
| (NumLevel n,_) when not (Notation.notation_entry_eq custom custom') -> Some (Some n)
+(* If a default level in a different grammar, the entry name is ok *)
+ | (DefaultLevel,InternalProd) ->
+ if Notation.notation_entry_eq custom InConstrEntry then Some (Some 200) else None
+ | (DefaultLevel,BorderProd _) when not (Notation.notation_entry_eq custom custom') -> None
(* Associativity is None means force the level *)
| (NumLevel n,BorderProd (_,None)) -> Some (Some n)
+ | (DefaultLevel,BorderProd (_,None)) -> assert false
(* Compute production name on the right side *)
(* If NonA or LeftA on the right-hand side, set to NEXT *)
- | (NumLevel n,BorderProd (Right,Some (NonA|LeftA))) ->
+ | ((NumLevel _ | DefaultLevel),BorderProd (Right,Some (NonA|LeftA))) ->
Some None
(* If RightA on the right-hand side, set to the explicit (current) level *)
| (NumLevel n,BorderProd (Right,Some RightA)) ->
Some (Some n)
+ | (DefaultLevel,BorderProd (Right,Some RightA)) ->
+ Some (Some from)
(* Compute production name on the left side *)
(* If NonA on the left-hand side, adopt the current assoc ?? *)
- | (NumLevel n,BorderProd (Left,Some NonA)) -> None
+ | ((NumLevel _ | DefaultLevel),BorderProd (Left,Some NonA)) -> None
(* If the expected assoc is the current one, set to SELF *)
- | (NumLevel n,BorderProd (Left,Some a)) when assoc_eq a (camlp5_assoc assoc) ->
+ | ((NumLevel _ | DefaultLevel),BorderProd (Left,Some a)) when assoc_eq a (camlp5_assoc assoc) ->
None
(* Otherwise, force the level, n or n-1, according to expected assoc *)
- | (NumLevel n,BorderProd (Left,Some a)) ->
- begin match a with
- | LeftA -> Some (Some n)
- | _ -> Some None
- end
+ | (NumLevel n,BorderProd (Left,Some LeftA)) -> Some (Some n)
+ | ((NumLevel _ | DefaultLevel),BorderProd (Left,Some _)) -> Some None
(* None means NEXT *)
| (NextLevel,_) -> assert (Notation.notation_entry_eq custom custom'); Some None
(* Compute production name elsewhere *)
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index 74249301d7..ac2341ac8d 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -1224,11 +1224,11 @@ GRAMMAR EXTEND Gram
| { CAst.v = k }, Some s -> SetFormat(k,s)
| s, None -> SetFormat ("text",s) end }
| x = IDENT; ","; l = LIST1 [id = IDENT -> { id } ] SEP ","; "at";
- lev = level -> { SetItemLevel (x::l,None,Some lev) }
- | x = IDENT; "at"; lev = level -> { SetItemLevel ([x],None,Some lev) }
+ lev = level -> { SetItemLevel (x::l,None,lev) }
+ | x = IDENT; "at"; lev = level -> { SetItemLevel ([x],None,lev) }
| x = IDENT; "at"; lev = level; b = constr_as_binder_kind ->
- { SetItemLevel ([x],Some b,Some lev) }
- | x = IDENT; b = constr_as_binder_kind -> { SetItemLevel ([x],Some b,None) }
+ { SetItemLevel ([x],Some b,lev) }
+ | x = IDENT; b = constr_as_binder_kind -> { SetItemLevel ([x],Some b,DefaultLevel) }
| x = IDENT; typ = syntax_extension_type -> { SetEntryType (x,typ) }
] ]
;
@@ -1236,19 +1236,20 @@ GRAMMAR EXTEND Gram
[ [ IDENT "ident" -> { ETIdent } | IDENT "global" -> { ETGlobal }
| IDENT "bigint" -> { ETBigint }
| IDENT "binder" -> { ETBinder true }
- | IDENT "constr" -> { ETConstr (InConstrEntry,None,None) }
- | IDENT "constr"; n = OPT at_level; b = OPT constr_as_binder_kind -> { ETConstr (InConstrEntry,b,n) }
+ | IDENT "constr" -> { ETConstr (InConstrEntry,None,DefaultLevel) }
+ | IDENT "constr"; n = at_level_opt; b = OPT constr_as_binder_kind -> { ETConstr (InConstrEntry,b,n) }
| IDENT "pattern" -> { ETPattern (false,None) }
| IDENT "pattern"; "at"; IDENT "level"; n = natural -> { ETPattern (false,Some n) }
| IDENT "strict"; IDENT "pattern" -> { ETPattern (true,None) }
| IDENT "strict"; IDENT "pattern"; "at"; IDENT "level"; n = natural -> { ETPattern (true,Some n) }
| IDENT "closed"; IDENT "binder" -> { ETBinder false }
- | IDENT "custom"; x = IDENT; n = OPT at_level; b = OPT constr_as_binder_kind ->
+ | IDENT "custom"; x = IDENT; n = at_level_opt; b = OPT constr_as_binder_kind ->
{ ETConstr (InCustomEntry x,b,n) }
] ]
;
- at_level:
- [ [ "at"; n = level -> { n } ] ]
+ at_level_opt:
+ [ [ "at"; n = level -> { n }
+ | -> { DefaultLevel } ] ]
;
constr_as_binder_kind:
[ [ "as"; IDENT "ident" -> { Notation_term.AsIdent }
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index c8c2376155..1e46d35ed7 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -297,6 +297,9 @@ let precedence_of_position_and_level from_level = function
n, let (lp,rp) = prec_assoc a in if b == Left then lp else rp
| NumLevel n, InternalProd -> n, Prec n
| NextLevel, _ -> from_level, L
+ | DefaultLevel, _ ->
+ (* Fake value, waiting for PR#5 at herbelin's fork *) 200,
+ Any
(** Computing precedences of subentries for parsing *)
let precedence_of_entry_type (from_custom,from_level) = function
@@ -981,17 +984,17 @@ let set_entry_type from n etyps (x,typ) =
str " cannot be inferred. It must be given explicitly.") in
let typ = try
match List.assoc x etyps, typ with
- | ETConstr (s,bko,Some n), BorderProd (left,_) ->
- ETConstr (s,bko,(n,BorderProd (left,None)))
- | ETConstr (s,bko,Some n), InternalProd ->
- ETConstr (s,bko,(n,InternalProd))
- | ETPattern (b,n), _ -> ETPattern (b,n)
- | (ETIdent | ETBigint | ETGlobal | ETBinder _ as x), _ -> x
- | ETConstr (s,bko,None), _ ->
+ | ETConstr (s,bko,DefaultLevel), _ ->
if notation_entry_eq from s then ETConstr (s,bko,(make_lev n s,typ))
else if s = InConstrEntry then ETConstr (s,bko,(make_lev 200 s,typ)) else
user_err (strbrk "level of subentry " ++ quote (pr_notation_entry s) ++
str " cannot be inferred. It must be given explicitly.")
+ | ETConstr (s,bko,n), BorderProd (left,_) ->
+ ETConstr (s,bko,(n,BorderProd (left,None)))
+ | ETConstr (s,bko,n), InternalProd ->
+ ETConstr (s,bko,(n,InternalProd))
+ | ETPattern (b,n), _ -> ETPattern (b,n)
+ | (ETIdent | ETBigint | ETGlobal | ETBinder _ as x), _ -> x
with Not_found ->
ETConstr (from,None,(make_lev n from,typ))
in (x,typ)
@@ -1150,7 +1153,7 @@ let find_precedence custom lev etyps symbols onlyprint =
else
user_err Pp.(str "The level of the leftmost non-terminal cannot be changed.") in
(try match List.assoc x etyps, custom with
- | ETConstr (s,_,Some _), s' when s = s' -> test ()
+ | ETConstr (s,_,(NumLevel _ | NextLevel)), s' when s = s' -> test ()
| (ETIdent | ETBigint | ETGlobal), _ ->
begin match lev with
| None ->
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml
index 6240120cb0..f4918caeff 100644
--- a/vernac/ppvernac.ml
+++ b/vernac/ppvernac.ml
@@ -107,8 +107,11 @@ open Pputils
| InCustomEntry s -> keyword "custom" ++ spc () ++ str s
let pr_at_level = function
- | NumLevel n -> keyword "at" ++ spc () ++ keyword "level" ++ spc () ++ int n
- | NextLevel -> keyword "at" ++ spc () ++ keyword "next" ++ spc () ++ keyword "level"
+ | NumLevel n -> spc () ++ keyword "at" ++ spc () ++ keyword "level" ++ spc () ++ int n
+ | NextLevel -> spc () ++ keyword "at" ++ spc () ++ keyword "next" ++ spc () ++ keyword "level"
+ | DefaultLevel -> mt ()
+
+ let level_of_pattern_level = function None -> DefaultLevel | Some n -> NumLevel n
let pr_constr_as_binder_kind = let open Notation_term in function
| AsIdent -> spc () ++ keyword "as ident"
@@ -120,19 +123,14 @@ open Pputils
let pr_set_entry_type pr = function
| ETIdent -> str"ident"
| ETGlobal -> str"global"
- | ETPattern (b,None) -> pr_strict b ++ str"pattern"
- | ETPattern (b,Some n) -> pr_strict b ++ str"pattern" ++ spc () ++ pr_at_level (NumLevel n)
+ | ETPattern (b,n) -> pr_strict b ++ str"pattern" ++ pr_at_level (level_of_pattern_level n)
| ETConstr (s,bko,lev) -> pr_notation_entry s ++ pr lev ++ pr_opt pr_constr_as_binder_kind bko
| ETBigint -> str "bigint"
| ETBinder true -> str "binder"
| ETBinder false -> str "closed binder"
- let pr_at_level_opt = function
- | None -> mt ()
- | Some n -> spc () ++ pr_at_level n
-
let pr_set_simple_entry_type =
- pr_set_entry_type pr_at_level_opt
+ pr_set_entry_type pr_at_level
let pr_comment pr_c = function
| CommentConstr c -> pr_c c
@@ -402,7 +400,7 @@ let string_of_theorem_kind = let open Decls in function
let pr_syntax_modifier = let open Gramlib.Gramext in function
| SetItemLevel (l,bko,n) ->
- prlist_with_sep sep_v2 str l ++ spc () ++ pr_at_level_opt n ++
+ prlist_with_sep sep_v2 str l ++ spc () ++ pr_at_level n ++
pr_opt pr_constr_as_binder_kind bko
| SetLevel n -> pr_at_level (NumLevel n)
| SetCustomEntry (s,n) -> keyword "in" ++ spc() ++ keyword "custom" ++ spc() ++ str s ++ (match n with None -> mt () | Some n -> pr_at_level (NumLevel n))
diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml
index 8ead56dfdf..3610240634 100644
--- a/vernac/vernacexpr.ml
+++ b/vernac/vernacexpr.ml
@@ -177,7 +177,7 @@ type proof_expr =
ident_decl * (local_binder_expr list * constr_expr)
type syntax_modifier =
- | SetItemLevel of string list * Notation_term.constr_as_binder_kind option * Extend.production_level option
+ | SetItemLevel of string list * Notation_term.constr_as_binder_kind option * Extend.production_level
| SetLevel of int
| SetCustomEntry of string * int option
| SetAssoc of Gramlib.Gramext.g_assoc
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 18:59:40 +0000