aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--toplevel/command.ml2
-rw-r--r--toplevel/metasyntax.ml59
-rw-r--r--toplevel/metasyntax.mli9
-rw-r--r--toplevel/vernacentries.ml13
-rw-r--r--toplevel/vernacexpr.ml10
-rw-r--r--translate/ppvernacnew.ml30
6 files changed, 73 insertions, 50 deletions
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 6c33b3783..ed77973c2 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -122,7 +122,7 @@ let declare_definition ident local bl red_option c typopt =
let syntax_definition ident c =
let c = snd (interp_aconstr [] c) in
let onlyparse = !Options.v7_only in
- Syntax_def.declare_syntactic_definition ident onlyparse c;
+ Syntax_def.declare_syntactic_definition false ident onlyparse c;
if_verbose message ((string_of_id ident) ^ " is now a syntax macro")
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index fa0310c00..c5a0c7a92 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -470,7 +470,7 @@ let make_pp_rule symbols typs =
(**************************************************************************)
(* Syntax extenstion: common parsing/printing rules and no interpretation *)
-let cache_syntax_extension (_,(prec,ntn,gr,se)) =
+let cache_syntax_extension (_,(_,prec,ntn,gr,se)) =
if not (Symbols.exists_notation prec ntn) then begin
Egrammar.extend_grammar (Egrammar.Notation gr);
if se<>None then
@@ -481,18 +481,24 @@ let subst_notation_grammar subst x = x
let subst_printing_rule subst x = x
-let subst_syntax_extension (_,subst,(prec,ntn,gr,se)) =
- (prec,ntn,
+let subst_syntax_extension (_,subst,(local,prec,ntn,gr,se)) =
+ (local,prec,ntn,
subst_notation_grammar subst gr,
option_app (subst_printing_rule subst) se)
+let classify_syntax_definition (_,(local,_,_,_,_ as o)) =
+ if local then Dispose else Substitute o
+
+let export_syntax_definition (local,_,_,_,_ as o) =
+ if local then None else Some o
+
let (inSyntaxExtension, outSyntaxExtension) =
declare_object {(default_object "SYNTAX-EXTENSION") with
open_function = (fun i o -> if i=1 then cache_syntax_extension o);
cache_function = cache_syntax_extension;
subst_function = subst_syntax_extension;
- classify_function = (fun (_,o) -> Substitute o);
- export_function = (fun x -> Some x)}
+ classify_function = classify_syntax_definition;
+ export_function = export_syntax_definition}
let interp_modifiers a n =
let onlyparsing = ref false in
@@ -568,7 +574,7 @@ let recompute_assoc typs =
| _, Some Gramext.RightA -> Some Gramext.RightA
| _ -> None
-let add_syntax_extension df modifiers =
+let add_syntax_extension local df modifiers =
let (assoc,n,etyps,onlyparse) = interp_notation_modifiers modifiers in
let inner = if !Options.v7 then (10,InternalProd) else
(200,InternalProd) in
@@ -581,17 +587,18 @@ let add_syntax_extension df modifiers =
let (prec,notation) = make_symbolic n symbs typs in
let gram_rule = make_grammar_rule n assoc typs symbs notation in
let pp_rule = if onlyparse then None else Some (make_pp_rule typs symbs) in
- Lib.add_anonymous_leaf (inSyntaxExtension(prec,notation,gram_rule,pp_rule))
+ Lib.add_anonymous_leaf
+ (inSyntaxExtension(local,prec,notation,gram_rule,pp_rule))
(**********************************************************************)
(* Distfix, Infix, Notations *)
(* A notation comes with a grammar rule, a pretty-printing rule, an
identifiying pattern called notation and an associated scope *)
-let load_notation _ (_,(_,prec,ntn,scope,pat,onlyparse,_)) =
+let load_notation _ (_,(_,_,prec,ntn,scope,pat,onlyparse,_)) =
Symbols.declare_scope scope
-let open_notation i (_,(oldse,prec,ntn,scope,pat,onlyparse,df)) =
+let open_notation i (_,(_,oldse,prec,ntn,scope,pat,onlyparse,df)) =
(*print_string ("Open notation "^ntn^" at "^string_of_int (fst prec)^"\n");*)
if i=1 then begin
let b = Symbols.exists_notation_in_scope scope prec ntn pat in
@@ -609,21 +616,27 @@ let cache_notation o =
load_notation 1 o;
open_notation 1 o
-let subst_notation (_,subst,(oldse,prec,ntn,scope,(metas,pat),b,df)) =
- (option_app
+let subst_notation (_,subst,(lc,oldse,prec,ntn,scope,(metas,pat),b,df)) =
+ (lc,option_app
(list_smartmap (Extend.subst_syntax_entry Ast.subst_astpat subst)) oldse,
prec,ntn,
scope,
(metas,subst_aconstr subst pat), b, df)
+let classify_notation (_,(local,_,_,_,_,_,_,_ as o)) =
+ if local then Dispose else Substitute o
+
+let export_notation (local,_,_,_,_,_,_,_ as o) =
+ if local then None else Some o
+
let (inNotation, outNotation) =
declare_object {(default_object "NOTATION") with
open_function = open_notation;
cache_function = cache_notation;
subst_function = subst_notation;
load_function = load_notation;
- classify_function = (fun (_,o) -> Substitute o);
- export_function = (fun x -> Some x)}
+ classify_function = classify_notation;
+ export_function = export_notation}
(* For old ast printer *)
let rec reify_meta_ast vars = function
@@ -645,7 +658,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 c (assoc,n,etyps,onlyparse) omodv8 sc toks =
+let add_notation_in_scope local df c (assoc,n,etyps,onlyparse) omodv8 sc toks =
let onlyparse = onlyparse or !Options.v7_only in
let scope = match sc with None -> Symbols.default_scope | Some sc -> sc in
let inner =
@@ -678,7 +691,7 @@ let add_notation_in_scope df c (assoc,n,etyps,onlyparse) omodv8 sc toks =
if onlyparse then None
else Some (make_pp_rule pptyps ppsymbols) in
Lib.add_anonymous_leaf
- (inSyntaxExtension(ppprec,notation,gram_rule,pp_rule));
+ (inSyntaxExtension(local,ppprec,notation,gram_rule,pp_rule));
let old_pp_rule =
if onlyparse then None
else
@@ -688,9 +701,9 @@ let add_notation_in_scope df c (assoc,n,etyps,onlyparse) omodv8 sc toks =
(* Declare the interpretation *)
let vars = List.map (fun id -> id,[] (* insert the right scope *)) vars in
Lib.add_anonymous_leaf
- (inNotation(old_pp_rule,ppprec,notation,scope,a,onlyparse,df))
+ (inNotation(local,old_pp_rule,ppprec,notation,scope,a,onlyparse,df))
-let add_notation df a modifiers mv8 sc =
+let add_notation local df a modifiers mv8 sc =
let toks = split df in
match toks with
| [String x] when quote(strip x) = x
@@ -699,9 +712,9 @@ let add_notation df a modifiers mv8 sc =
let ident = id_of_string (strip x) in
let c = snd (interp_aconstr [] a) in
let onlyparse = !Options.v7_only or modifiers = [SetOnlyParsing] in
- Syntax_def.declare_syntactic_definition ident onlyparse c
+ Syntax_def.declare_syntactic_definition local ident onlyparse c
| _ ->
- add_notation_in_scope
+ add_notation_in_scope local
df a (interp_notation_modifiers modifiers)
(option_app (fun (s8,ml8) ->
let toks8 = split s8 in
@@ -725,15 +738,15 @@ let rec rename x vars n = function
| WhiteSpace _::l ->
rename x vars n l
-let add_distfix assoc n df r sc =
+let add_distfix local assoc n df r sc =
(* "x" cannot clash since r is globalized (included section vars) *)
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 -> Gramext.LeftA | Some a -> a in
- add_notation_in_scope df a (Some assoc,n,[],false) None sc (split df)
+ add_notation_in_scope local df a (Some assoc,n,[],false) None sc (split df)
-let add_infix assoc n inf pr onlyparse mv8 sc =
+let add_infix local assoc n inf pr onlyparse mv8 sc =
(* let pr = Astterm.globalize_qualid pr in*)
(* check the precedence *)
if !Options.v7 & (n<1 or n>10) then
@@ -751,7 +764,7 @@ let add_infix assoc n inf pr onlyparse mv8 sc =
None -> Some(split df,(assoc,n*10,[],false))
| Some(a8,n8,s8) ->
Some(split ("x "^quote s8^" y"),(a8,n8,[],false)) in
- add_notation_in_scope df a (assoc,n,[],onlyparse) mv8 sc (split df)
+ add_notation_in_scope local df a (assoc,n,[],onlyparse) mv8 sc (split df)
(* Delimiters *)
let load_delimiters _ (_,(scope,dlm)) =
diff --git a/toplevel/metasyntax.mli b/toplevel/metasyntax.mli
index 0c84a3ead..92f79680e 100644
--- a/toplevel/metasyntax.mli
+++ b/toplevel/metasyntax.mli
@@ -28,20 +28,21 @@ val add_token_obj : string -> unit
val add_tactic_grammar :
(string * (string * grammar_production list) * raw_tactic_expr) list -> unit
-val add_infix :
+val add_infix : locality_flag ->
grammar_associativity -> precedence -> string -> reference -> bool ->
(grammar_associativity * precedence * string) option ->
scope_name option -> unit
-val add_distfix :
+val add_distfix : locality_flag ->
grammar_associativity -> precedence -> string -> reference
-> scope_name option -> unit
val add_delimiters : scope_name -> string -> unit
-val add_notation : string -> constr_expr
+val add_notation : locality_flag -> string -> constr_expr
-> syntax_modifier list -> (string * syntax_modifier list) option
-> scope_name option -> unit
-val add_syntax_extension : string -> syntax_modifier list -> unit
+val add_syntax_extension : locality_flag -> string -> syntax_modifier list
+ -> unit
val print_grammar : string -> string -> unit
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index d536be9bd..9b11e6879 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1139,15 +1139,16 @@ let interp c = match c with
| VernacSyntax (whatfor,sel) -> vernac_syntax whatfor sel
| VernacTacticGrammar al -> Metasyntax.add_tactic_grammar al
| VernacGrammar (univ,al) -> vernac_grammar univ al
- | VernacSyntaxExtension (s,l) -> vernac_syntax_extension s l
+ | VernacSyntaxExtension (local,s,l) -> vernac_syntax_extension local s l
| 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,b,mv8,sc) ->
- vernac_infix assoc n inf qid b mv8 sc
- | VernacDistfix (assoc,n,inf,qid,sc) -> vernac_distfix assoc n inf qid sc
- | VernacNotation (inf,c,pl,mv8,sc) ->
- vernac_notation inf c pl mv8 sc
+ | VernacInfix (local,assoc,n,inf,qid,b,mv8,sc) ->
+ vernac_infix local assoc n inf qid b mv8 sc
+ | VernacDistfix (local,assoc,n,inf,qid,sc) ->
+ vernac_distfix local assoc n inf qid sc
+ | VernacNotation (local,inf,c,pl,mv8,sc) ->
+ vernac_notation local inf c pl mv8 sc
(* Gallina *)
| VernacDefinition (k,id,d,f,_) -> vernac_definition k id d f
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index 171238eb8..99ce8b34e 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -150,19 +150,19 @@ type vernac_expr =
| VernacTacticGrammar of
(string * (string * grammar_production list) * raw_tactic_expr) list
| VernacSyntax of string * raw_syntax_entry list
- | VernacSyntaxExtension of string * syntax_modifier list
- | VernacDistfix of
+ | VernacSyntaxExtension of locality_flag * string * syntax_modifier list
+ | VernacDistfix of locality_flag *
grammar_associativity * precedence * string * reference *
scope_name option
- | VernacOpenScope of (export_flag * scope_name)
+ | VernacOpenScope of (locality_flag * scope_name)
| VernacDelimiters of scope_name * string
| VernacArgumentsScope of reference * scope_name option list
- | VernacInfix of
+ | VernacInfix of locality_flag *
grammar_associativity * precedence * string * reference * bool *
(grammar_associativity * precedence * string) option *
scope_name option
| VernacNotation of
- string * constr_expr * syntax_modifier list *
+ locality_flag * string * constr_expr * syntax_modifier list *
(string * syntax_modifier list) option * scope_name option
(* Gallina *)
diff --git a/translate/ppvernacnew.ml b/translate/ppvernacnew.ml
index aa264293b..1b2428a9d 100644
--- a/translate/ppvernacnew.ml
+++ b/translate/ppvernacnew.ml
@@ -70,9 +70,9 @@ let pr_ne_sep sep pr = function
| l -> sep() ++ pr l
let pr_entry_prec = function
- | Some Gramext.LeftA -> spc() ++ str"LEFTA"
- | Some Gramext.RightA -> spc() ++ str"RIGHTA"
- | Some Gramext.NonA -> spc() ++ str"NONA"
+ | Some Gramext.LeftA -> str"LEFTA "
+ | Some Gramext.RightA -> str"RIGHTA "
+ | Some Gramext.NonA -> str"NONA "
| None -> mt()
let pr_set_entry_type = function
@@ -108,6 +108,8 @@ let pr_search a b pr_c = match a with
| SearchRewrite c -> str"SearchRewrite" ++ spc() ++ pr_c c ++ spc() ++ pr_in_out_modules b
| SearchAbout qid -> str"SearchAbout" ++ spc() ++ pr_reference qid ++ spc() ++ pr_in_out_modules b
+let pr_locality local = if local then str "Local " else str ""
+
let pr_class_rawexpr = function
| FunClass -> str"FUNCLASS"
| SortClass -> str"SORTCLASS"
@@ -416,8 +418,8 @@ let rec pr_vernac = function
| VernacTacticGrammar l -> hov 1 (str"Grammar tactic simple_tactic :=" ++ spc() ++ prlist_with_sep (fun _ -> brk(1,1) ++ str"|") pr_grammar_tactic_rule l) (***)
| VernacSyntax (u,el) -> hov 1 (str"Syntax " ++ str u ++ spc() ++
prlist_with_sep sep_v2 pr_syntax_entry el) (***)
- | VernacOpenScope (exp,sc) ->
- str ("Open "^(if exp then "" else "Local ")^"Scope") ++ spc() ++ str sc
+ | VernacOpenScope (local,sc) ->
+ str "Open " ++ pr_locality local ++ str "Scope" ++ spc() ++ str sc
| VernacDelimiters (sc,key) ->
str"Delimits Scope" ++ spc () ++ str sc ++
spc() ++ str "with " ++ str key
@@ -425,21 +427,24 @@ let rec pr_vernac = function
| None -> str"_"
| Some sc -> str sc in
str"Arguments Scope" ++ spc() ++ pr_reference q ++ spc() ++ str"[" ++ prlist_with_sep sep pr_opt_scope scl ++ str"]"
- | VernacInfix (a,p,s,q,_,ov8,sn) -> (* A Verifier *)
+ | VernacInfix (local,a,p,s,q,_,ov8,sn) -> (* A Verifier *)
let (a,p,s) = match ov8 with
Some mv8 -> mv8
| None -> (a,p,s) in
- hov 0 (str"Infix" ++ pr_entry_prec a ++ pr_intarg p ++ spc() ++ qs s ++ spc() ++ pr_reference q ++ (match sn with
+ hov 0 (str"Infix " ++ pr_locality local ++ pr_entry_prec a ++ int p
+ ++ spc() ++ qs s ++ spc() ++ pr_reference q ++ (match sn with
| None -> mt()
| Some sc -> spc() ++ str":" ++ spc() ++ str sc))
- | VernacDistfix (a,p,s,q,sn) -> hov 0 (str"Distfix" ++ pr_entry_prec a ++ pr_intarg p ++ spc() ++ qs s ++ spc() ++ pr_reference q ++ (match sn with
+ | VernacDistfix (local,a,p,s,q,sn) ->
+ hov 0 (str"Distfix " ++ pr_locality local ++ pr_entry_prec a ++ int p
+ ++ spc() ++ qs s ++ spc() ++ pr_reference q ++ (match sn with
| None -> mt()
| Some sc -> spc() ++ str":" ++ spc() ++ str sc))
- | VernacNotation (s,c,l,mv8,opt) ->
+ | VernacNotation (local,s,c,l,mv8,opt) ->
let (s,l) = match mv8 with
None -> (s,l)
| Some ml -> ml in
- hov 2( str"Notation" ++ spc() ++ qs s ++
+ hov 2( str"Notation" ++ spc() ++ pr_locality local ++ qs s ++
str " :=" ++ pr_constrarg c ++
(match l with
| [] -> mt()
@@ -448,7 +453,10 @@ let rec pr_vernac = function
(match opt with
| None -> mt()
| Some sc -> str" :" ++ spc() ++ str sc))
- | VernacSyntaxExtension (a,b) -> str"Uninterpreted Notation" ++ spc() ++ qs a ++ (match b with | [] -> mt() | _ as l -> str"(" ++ prlist_with_sep sep_v2 pr_syntax_modifier l ++ str")")
+ | VernacSyntaxExtension (local,a,b) ->
+ str"Uninterpreted Notation" ++ spc() ++ pr_locality local ++ qs a ++
+ (match b with | [] -> mt() | _ as l ->
+ str"(" ++ prlist_with_sep sep_v2 pr_syntax_modifier l ++ str")")
(* Gallina *)
| VernacDefinition (d,id,b,f,e) -> (* A verifier... *)
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-28 19:13:17 +0000