aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--contrib/interface/xlate.ml6
-rw-r--r--interp/symbols.ml8
-rw-r--r--interp/syntax_def.ml18
-rw-r--r--interp/syntax_def.mli3
-rw-r--r--parsing/g_basevernac.ml428
-rw-r--r--parsing/g_vernac.ml42
-rw-r--r--parsing/g_vernacnew.ml429
7 files changed, 55 insertions, 39 deletions
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 1fe718f0e..07deebf4a 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -1606,7 +1606,7 @@ let xlate_vernac =
| VernacSyntaxExtension _ -> xlate_error "Syntax Extension not implemented"
- | VernacInfix (str_assoc, n, str, id, false, _, None) ->
+ | VernacInfix (false,str_assoc, n, str, id, false, _, None) ->
CT_infix (
(match str_assoc with
| Some Gramext.LeftA -> CT_lefta
@@ -1614,7 +1614,7 @@ let xlate_vernac =
| Some Gramext.NonA -> CT_nona
| None -> CT_coerce_NONE_to_ASSOC CT_none),
CT_int n, CT_string str, loc_qualid_to_ct_ID id)
- | VernacInfix _ -> xlate_error "TODO: handle scopes"
+ | VernacInfix _ -> xlate_error "TODO: handle scopes and locality"
| VernacGrammar _ -> xlate_error "GRAMMAR not implemented"
| VernacCoercion (s, id1, id2, id3) ->
let id_opt = CT_coerce_NONE_to_IDENTITY_OPT CT_none in
@@ -1664,7 +1664,7 @@ let xlate_vernac =
VernacSetOption (_, _)|VernacUnsetOption _|
VernacHintDestruct (_, _, _, _, _)|VernacBack _|VernacRestoreState _|
VernacWriteState _|VernacSolveExistential (_, _)|VernacCanonical _|
- VernacImport (_, _)|VernacExactProof _|VernacDistfix (_, _, _, _, _)|
+ VernacImport (_, _)|VernacExactProof _|VernacDistfix _|
VernacTacticGrammar _|VernacVar _|VernacTime _|VernacProof _)
-> xlate_error "TODO: vernac"
diff --git a/interp/symbols.ml b/interp/symbols.ml
index 30e139236..0c988f315 100644
--- a/interp/symbols.ml
+++ b/interp/symbols.ml
@@ -293,7 +293,7 @@ let exists_notation prec nt =
!scope_map false
(* Exportation of scopes *)
-let cache_scope (_,(exp,sc)) =
+let cache_scope (_,(local,sc)) =
check_scope sc;
scope_stack := sc :: !scope_stack
@@ -301,7 +301,9 @@ let subst_scope (_,subst,sc) = sc
open Libobject
-let classify_scope (_,(exp,_ as o)) = if exp then Substitute o else Dispose
+let classify_scope (_,(local,_ as o)) = if local then Dispose else Substitute o
+
+let export_scope (local,_ as x) = if local then None else Some x
let (inScope,outScope) =
declare_object {(default_object "SCOPE") with
@@ -309,7 +311,7 @@ let (inScope,outScope) =
open_function = (fun i o -> if i=1 then cache_scope o);
subst_function = subst_scope;
classify_function = classify_scope;
- export_function = (fun (exp,_ as x) -> if exp then Some x else None) }
+ export_function = export_scope }
let open_scope sc = Lib.add_anonymous_leaf (inScope sc)
diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml
index d24ac4673..69094507d 100644
--- a/interp/syntax_def.ml
+++ b/interp/syntax_def.ml
@@ -31,7 +31,7 @@ let _ = Summary.declare_summary
let add_syntax_constant kn c =
syntax_table := KNmap.add kn c !syntax_table
-let load_syntax_constant i ((sp,kn),(c,onlyparse)) =
+let load_syntax_constant i ((sp,kn),(local,c,onlyparse)) =
if Nametab.exists_cci sp then
errorlabstrm "cache_syntax_constant"
(pr_id (basename sp) ++ str " already exists");
@@ -46,10 +46,14 @@ let open_syntax_constant i ((sp,kn),c) =
let cache_syntax_constant d =
load_syntax_constant 1 d
-let subst_syntax_constant ((sp,kn),subst,(c,onlyparse)) =
- (subst_aconstr subst c,onlyparse)
+let subst_syntax_constant ((sp,kn),subst,(local,c,onlyparse)) =
+ (local,subst_aconstr subst c,onlyparse)
-let classify_syntax_constant (_,c) = Substitute c
+let classify_syntax_constant (_,(local,_,_ as o)) =
+ if local then Dispose else Substitute o
+
+let export_syntax_constant (local,_,_ as o) =
+ if local then None else Some o
let (in_syntax_constant, out_syntax_constant) =
declare_object {(default_object "SYNTAXCONSTANT") with
@@ -58,10 +62,10 @@ let (in_syntax_constant, out_syntax_constant) =
open_function = open_syntax_constant;
subst_function = subst_syntax_constant;
classify_function = classify_syntax_constant;
- export_function = (fun x -> Some x) }
+ export_function = export_syntax_constant }
-let declare_syntactic_definition id onlyparse c =
- let _ = add_leaf id (in_syntax_constant (c,onlyparse)) in ()
+let declare_syntactic_definition local id onlyparse c =
+ let _ = add_leaf id (in_syntax_constant (local,c,onlyparse)) in ()
let rec set_loc loc _ a =
map_aconstr_with_binders_loc loc (fun id e -> (id,e)) (set_loc loc) () a
diff --git a/interp/syntax_def.mli b/interp/syntax_def.mli
index 87c3e7512..9083158ac 100644
--- a/interp/syntax_def.mli
+++ b/interp/syntax_def.mli
@@ -16,7 +16,8 @@ open Rawterm
(* Syntactic definitions. *)
-val declare_syntactic_definition : identifier -> bool -> aconstr -> unit
+val declare_syntactic_definition : bool -> identifier -> bool -> aconstr
+ -> unit
val search_syntactic_definition : loc -> kernel_name -> rawconstr
diff --git a/parsing/g_basevernac.ml4 b/parsing/g_basevernac.ml4
index 3d9753783..3db24bcd1 100644
--- a/parsing/g_basevernac.ml4
+++ b/parsing/g_basevernac.ml4
@@ -241,12 +241,12 @@ GEXTEND Gram
| IDENT "Syntax"; u = univ; el = LIST1 syntax_entry SEP ";" ->
VernacSyntax (u,el)
- | IDENT "Uninterpreted"; IDENT "Notation"; s = STRING;
+ | IDENT "Uninterpreted"; IDENT "Notation"; local = locality; s = STRING;
l = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ]
- -> VernacSyntaxExtension (s,l)
+ -> VernacSyntaxExtension (local,s,l)
- | IDENT "Open"; exp = [IDENT "Local" -> false | -> true]; IDENT "Scope";
- sc = IDENT -> VernacOpenScope (exp,sc)
+ | IDENT "Open"; local = locality; IDENT "Scope";
+ sc = IDENT -> VernacOpenScope (local,sc)
| IDENT "Delimits"; IDENT "Scope"; sc = IDENT; "with"; key = IDENT ->
VernacDelimiters (sc,key)
@@ -254,7 +254,7 @@ GEXTEND Gram
| IDENT "Arguments"; IDENT "Scope"; qid = global;
"["; scl = LIST0 opt_scope; "]" -> VernacArgumentsScope (qid,scl)
- | IDENT "Infix"; a = entry_prec; n = OPT natural;
+ | IDENT "Infix"; local = locality; a = entry_prec; n = OPT natural;
op = STRING;
p = global;
modl = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ];
@@ -277,12 +277,13 @@ GEXTEND Gram
let (a8,n8,_) =
Metasyntax.interp_infix_modifiers a nv8 mv8 in
let v8 = Some(a8,n8,op8) in
- VernacInfix (ai,ni,op,p,b,v8,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 ->
- VernacNotation ("'"^s^"'",c,[],None,None)
- | IDENT "Notation"; s = STRING; ":="; c = constr;
+ VernacInfix (local,ai,ni,op,p,b,v8,sc)
+ | IDENT "Distfix"; local = locality; a = entry_prec; n = natural;
+ s = STRING; p = global; sc = OPT [ ":"; sc = IDENT -> sc ] ->
+ VernacDistfix (local,a,n,s,p,sc)
+ | IDENT "Notation"; local = locality; s = IDENT; ":="; c = constr ->
+ VernacNotation (local,"'"^s^"'",c,[],None,None)
+ | IDENT "Notation"; local = locality; s = STRING; ":="; c = constr;
modl = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ];
sc = OPT [ ":"; sc = IDENT -> sc ];
(s8,mv8) =
@@ -295,12 +296,15 @@ GEXTEND Gram
let mv8 = match mv8 with
Some mv8 -> mv8
| _ -> List.map map_modl modl in
- VernacNotation (s,c,modl,Some(s8,mv8),sc)
+ VernacNotation (local,s,c,modl,Some(s8,mv8),sc)
(* "Print" "Grammar" should be here but is in "command" entry in order
to factorize with other "Print"-based vernac entries *)
] ]
;
+ locality:
+ [ [ IDENT "Local" -> true | -> false ] ]
+ ;
syntax_modifier:
[ [ x = IDENT; IDENT "at"; IDENT "level"; n = natural ->
SetItemLevel ([x],n)
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index cb02b082e..2d1fcdd30 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -419,7 +419,7 @@ GEXTEND Gram
let l = list_tabulate (fun _ -> (CHole (loc),None)) n in
CApp (loc,c,l)
| None -> c in
- VernacNotation ("'"^id^"'",c,[],None,None)
+ VernacNotation (false,"'"^id^"'",c,[],None,None)
| IDENT "Implicits"; qid = global; "["; l = LIST0 natural; "]" ->
VernacDeclareImplicits (qid,Some l)
| IDENT "Implicits"; qid = global -> VernacDeclareImplicits (qid,None)
diff --git a/parsing/g_vernacnew.ml4 b/parsing/g_vernacnew.ml4
index 0ad8caaaa..0e9e8dabb 100644
--- a/parsing/g_vernacnew.ml4
+++ b/parsing/g_vernacnew.ml4
@@ -411,6 +411,7 @@ GEXTEND Gram
VernacCoercion (Global, qid, s, t)
(* Implicit *)
+(* Obsolete
| IDENT "Syntactic"; IDENT "Definition"; id = IDENT; ":="; c = lconstr;
n = OPT [ "|"; n = natural -> n ] ->
let c = match n with
@@ -418,7 +419,8 @@ GEXTEND Gram
let l = list_tabulate (fun _ -> (CHole (loc),None)) n in
CApp (loc,c,l)
| None -> c in
- VernacNotation ("'"^id^"'",c,[],None,None)
+ VernacNotation (false,"'"^id^"'",c,[],None,None)
+*)
| IDENT "Implicits"; qid = global; "["; l = LIST0 natural; "]" ->
VernacDeclareImplicits (qid,Some l)
| IDENT "Implicits"; qid = global -> VernacDeclareImplicits (qid,None)
@@ -648,8 +650,8 @@ GEXTEND Gram
GLOBAL: syntax;
syntax:
- [ [ IDENT "Open"; exp = [IDENT "Local" -> false | -> true]; IDENT "Scope";
- sc = IDENT -> VernacOpenScope (exp,sc)
+ [ [ IDENT "Open"; local = locality; IDENT "Scope"; sc = IDENT ->
+ VernacOpenScope (local,sc)
| IDENT "Delimits"; IDENT "Scope"; sc = IDENT; "with"; key = IDENT ->
VernacDelimiters (sc,key)
@@ -657,18 +659,18 @@ GEXTEND Gram
| IDENT "Arguments"; IDENT "Scope"; qid = global;
"["; scl = LIST0 opt_scope; "]" -> VernacArgumentsScope (qid,scl)
- | IDENT "Infix"; a = entry_prec; n = OPT natural; op = STRING;
- p = global;
+ | IDENT "Infix"; local = locality; 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,None,sc)
- | IDENT "Notation"; s = IDENT; ":="; c = constr ->
- VernacNotation ("'"^s^"'",c,[],None,None)
- | IDENT "Notation"; s = STRING; ":="; c = constr;
+ VernacInfix (local,a,n,op,p,b,None,sc)
+ | IDENT "Notation"; local = locality; s = IDENT; ":="; c = constr ->
+ VernacNotation (local,"'"^s^"'",c,[],None,None)
+ | IDENT "Notation"; local = locality; s = STRING; ":="; c = constr;
modl = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ];
sc = OPT [ ":"; sc = IDENT -> sc ] ->
- VernacNotation (s,c,modl,None,sc)
+ VernacNotation (local,s,c,modl,None,sc)
| IDENT "Grammar"; IDENT "tactic"; IDENT "simple_tactic";
OPT [ ":"; IDENT "tactic" ]; ":=";
@@ -682,14 +684,17 @@ GEXTEND Gram
| IDENT "Syntax"; u = univ; el = LIST1 syntax_entry SEP "," ->
VernacSyntax (u,el)
- | IDENT "Uninterpreted"; IDENT "Notation"; s = STRING;
+ | IDENT "Uninterpreted"; IDENT "Notation"; local = locality; s = STRING;
l = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ]
- -> VernacSyntaxExtension (s,l)
+ -> VernacSyntaxExtension (local,s,l)
(* "Print" "Grammar" should be here but is in "command" entry in order
to factorize with other "Print"-based vernac entries *)
] ]
;
+ locality:
+ [ [ IDENT "Local" -> true | -> false ] ]
+ ;
univ:
[ [ univ = IDENT ->
set_default_action_parser (parser_type_from_name univ); univ ] ]
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-03 14:54:50 +0000