aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--contrib/interface/xlate.ml2
-rw-r--r--parsing/g_basevernac.ml48
-rw-r--r--toplevel/metasyntax.ml40
-rw-r--r--toplevel/metasyntax.mli4
-rw-r--r--toplevel/vernacentries.ml2
-rw-r--r--toplevel/vernacexpr.ml2
6 files changed, 36 insertions, 22 deletions
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 57e7189a7..6358a3e59 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -1932,7 +1932,7 @@ let xlate_vernac =
| VernacSyntaxExtension _ -> xlate_error "Syntax Extension not implemented"
- | VernacInfix (str_assoc, n, str, id, None) ->
+ | VernacInfix (str_assoc, n, str, id, false, None) ->
CT_infix (
(match str_assoc with
| Some Gramext.LeftA -> CT_lefta
diff --git a/parsing/g_basevernac.ml4 b/parsing/g_basevernac.ml4
index 24499fb2d..9ef698ad1 100644
--- a/parsing/g_basevernac.ml4
+++ b/parsing/g_basevernac.ml4
@@ -232,8 +232,12 @@ GEXTEND Gram
| IDENT "Arguments"; IDENT "Scope"; qid = global;
"["; scl = LIST0 opt_scope; "]" -> VernacArgumentsScope (qid,scl)
- | IDENT "Infix"; a = entry_prec; n = natural; op = STRING; p = global;
- sc = OPT [ ":"; sc = IDENT -> sc ] -> VernacInfix (a,n,op,p,sc)
+ | IDENT "Infix"; a = entry_prec; n = OPT natural; op = STRING;
+ p = global;
+ modl = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ];
+ sc = OPT [ ":"; sc = IDENT -> sc ] ->
+ let (a,n,b) = Metasyntax.interp_infix_modifiers a n modl in
+ VernacInfix (a,n,op,p,b,sc)
| IDENT "Distfix"; a = entry_prec; n = natural; s = STRING; p = global;
sc = OPT [ ":"; sc = IDENT -> sc ] -> VernacDistfix (a,n,s,p,sc)
| IDENT "Notation"; s = IDENT; ":="; c = constr ->
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index e527fafd8..564fc48d8 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -441,12 +441,11 @@ let (inSyntaxExtension, outSyntaxExtension) =
classify_function = (fun (_,o) -> Substitute o);
export_function = (fun x -> Some x)}
-let interp_syntax_modifiers =
+let interp_modifiers a n =
let onlyparsing = ref false in
let rec interp assoc level etyps = function
| [] ->
let n = match level with None -> 1 | Some n -> n in
- let assoc = match assoc with None -> Some Gramext.NonA | a -> a in
(assoc,n,etyps,!onlyparsing)
| SetEntryType (s,typ) :: l ->
let id = id_of_string s in
@@ -471,7 +470,21 @@ let interp_syntax_modifiers =
| SetOnlyParsing :: l ->
onlyparsing := true;
interp assoc level etyps l
- in interp None None []
+ in interp a n []
+
+(* Infix defaults to LEFTA (cf doc) *)
+let interp_infix_modifiers a n l =
+ let (assoc,n,t,b) = interp_modifiers a n l in
+ if t <> [] then
+ error "explicit entry level or type unexpected in infix notation";
+ let assoc = match assoc with None -> Some Gramext.LeftA | a -> a in
+ (assoc,n,b)
+
+(* Notation defaults to NONA *)
+let interp_notation_modifiers modl =
+ let (assoc,n,t,b) = interp_modifiers None None modl in
+ let assoc = match assoc with None -> Some Gramext.NonA | a -> a in
+ (assoc,n,t,b)
(* 2nd list of types has priority *)
let rec merge_entry_types etyps' = function
@@ -503,7 +516,7 @@ let recompute_assoc typs =
| _ -> Some Gramext.NonA
let add_syntax_extension df modifiers =
- let (assoc,n,etyps,onlyparse) = interp_syntax_modifiers modifiers in
+ let (assoc,n,etyps,onlyparse) = interp_notation_modifiers modifiers in
let (typs,symbs) =
find_symbols
(n,BorderProd(true,assoc)) (10,InternalProd) (n,BorderProd(false,assoc))
@@ -576,8 +589,7 @@ let make_old_pp_rule n symbols typs r ntn scope vars =
let rule_name = ntn^"_"^scope^"_notation" in
make_syntax_rule n rule_name symbols typs ast ntn scope
-let add_notation_in_scope df a modifiers sc toks =
- let (assoc,n,etyps,onlyparse) = interp_syntax_modifiers modifiers in
+let add_notation_in_scope df a (assoc,n,etyps,onlyparse) sc toks =
let scope = match sc with None -> Symbols.default_scope | Some sc -> sc in
let (typs,symbols) =
find_symbols
@@ -613,7 +625,7 @@ let add_notation df a modifiers sc =
let ident = id_of_string (strip x) in
Syntax_def.declare_syntactic_definition ident (interp_aconstr a)
| _ ->
- add_notation_in_scope df a modifiers sc toks
+ add_notation_in_scope df a (interp_notation_modifiers modifiers) sc toks
(* TODO add boxes information in the expression *)
@@ -636,12 +648,10 @@ let add_distfix assoc n df r sc =
let (vars,l) = rename "x" [] 1 (split df) in
let df = String.concat " " l in
let a = mkAppC (mkRefC r, vars) in
- let assoc = match assoc with
- | None -> [SetAssoc Gramext.LeftA]
- | Some a -> [SetAssoc a] in
- add_notation df a (SetLevel n :: assoc) sc
+ let assoc = match assoc with None -> Gramext.LeftA | Some a -> a in
+ add_notation_in_scope df a (Some assoc,n,[],false) sc (split df)
-let add_infix assoc n inf pr sc =
+let add_infix assoc n inf pr onlyparse sc =
(* let pr = Astterm.globalize_qualid pr in*)
(* check the precedence *)
if n<1 or n>10 then
@@ -654,10 +664,8 @@ let add_infix assoc n inf pr sc =
*)
let metas = [inject_var "x"; inject_var "y"] in
let a = mkAppC (mkRefC pr,metas) in
- let assoc = match assoc with
- | None -> [SetAssoc Gramext.LeftA]
- | Some a -> [SetAssoc a] in
- add_notation ("x "^(quote inf)^" y") a (SetLevel n :: assoc) sc
+ let df = "x "^(quote inf)^" y" in
+ add_notation_in_scope df a (assoc,n,[],onlyparse) sc (split df)
(* Delimiters *)
let load_delimiters _ (_,(scope,dlm)) =
diff --git a/toplevel/metasyntax.mli b/toplevel/metasyntax.mli
index a63d1dea9..08a4d3c06 100644
--- a/toplevel/metasyntax.mli
+++ b/toplevel/metasyntax.mli
@@ -29,7 +29,7 @@ val add_tactic_grammar :
(string * (string * grammar_production list) * raw_tactic_expr) list -> unit
val add_infix :
- grammar_associativity -> precedence -> string -> reference
+ grammar_associativity -> precedence -> string -> reference -> bool
-> scope_name option -> unit
val add_distfix :
grammar_associativity -> precedence -> string -> reference
@@ -43,3 +43,5 @@ val add_syntax_extension : string -> syntax_modifier list -> unit
val print_grammar : string -> string -> unit
+val interp_infix_modifiers : Gramext.g_assoc option -> int option ->
+ syntax_modifier list -> Gramext.g_assoc option * int * bool
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 35ef1e620..0a3e28c6c 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1014,7 +1014,7 @@ let interp c = match c with
| VernacDelimiters (sc,lr) -> vernac_delimiters sc lr
| VernacOpenScope sc -> vernac_open_scope sc
| VernacArgumentsScope (qid,scl) -> vernac_arguments_scope qid scl
- | VernacInfix (assoc,n,inf,qid,sc) -> vernac_infix assoc n inf qid sc
+ | VernacInfix (assoc,n,inf,qid,b,sc) -> vernac_infix assoc n inf qid b sc
| VernacDistfix (assoc,n,inf,qid,sc) -> vernac_distfix assoc n inf qid sc
| VernacNotation (inf,c,pl,sc) -> vernac_notation inf c pl sc
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index 6076184b8..36c277b95 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -158,7 +158,7 @@ type vernac_expr =
| VernacDelimiters of scope_name * string
| VernacArgumentsScope of reference * scope_name option list
| VernacInfix of
- grammar_associativity * precedence * string * reference *
+ grammar_associativity * precedence * string * reference * bool *
scope_name option
| VernacDistfix of
grammar_associativity * precedence * string * reference *
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-09 02:24:00 +0000