summaryrefslogtreecommitdiff
path: root/toplevel/metasyntax.ml
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel/metasyntax.ml')
-rw-r--r--toplevel/metasyntax.ml416
1 files changed, 168 insertions, 248 deletions
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index ae82b64e..008d5cf9 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -8,7 +8,7 @@
open Pp
open Flags
-open Errors
+open CErrors
open Util
open Names
open Constrexpr
@@ -23,7 +23,6 @@ open Vernacexpr
open Pcoq
open Libnames
open Tok
-open Egramml
open Egramcoq
open Notation
open Nameops
@@ -31,7 +30,7 @@ open Nameops
(**********************************************************************)
(* Tokens *)
-let cache_token (_,s) = Lexer.add_keyword s
+let cache_token (_,s) = CLexer.add_keyword s
let inToken : string -> obj =
declare_object {(default_object "TOKEN") with
@@ -43,161 +42,6 @@ let inToken : string -> obj =
let add_token_obj s = Lib.add_anonymous_leaf (inToken s)
(**********************************************************************)
-(* Tactic Notation *)
-
-let interp_prod_item lev = function
- | TacTerm s -> GramTerminal s
- | TacNonTerm (loc, nt, po) ->
- let sep = match po with Some (_,sep) -> sep | _ -> "" in
- let (etyp, e) = interp_entry_name true (Some lev) nt sep in
- GramNonTerminal (loc, etyp, e, Option.map fst po)
-
-let make_terminal_status = function
- | GramTerminal s -> Some s
- | GramNonTerminal _ -> None
-
-let rec make_tags = function
- | GramTerminal s :: l -> make_tags l
- | GramNonTerminal (loc, etyp, _, po) :: l -> etyp :: make_tags l
- | [] -> []
-
-let make_fresh_key =
- let id = Summary.ref ~name:"TACTIC-NOTATION-COUNTER" 0 in
- fun () ->
- let cur = incr id; !id in
- let lbl = Id.of_string ("_" ^ string_of_int cur) in
- let kn = Lib.make_kn lbl in
- let (mp, dir, _) = KerName.repr kn in
- (** We embed the full path of the kernel name in the label so that the
- identifier should be unique. This ensures that including two modules
- together won't confuse the corresponding labels. *)
- let lbl = Id.of_string_soft (Printf.sprintf "%s#%s#%i"
- (ModPath.to_string mp) (DirPath.to_string dir) cur)
- in
- KerName.make mp dir (Label.of_id lbl)
-
-type tactic_grammar_obj = {
- tacobj_key : KerName.t;
- tacobj_local : locality_flag;
- tacobj_tacgram : tactic_grammar;
- tacobj_tacpp : Pptactic.pp_tactic;
- tacobj_body : Tacexpr.glob_tactic_expr
-}
-
-let check_key key =
- if Tacenv.check_alias key then
- error "Conflicting tactic notations keys. This can happen when including \
- twice the same module."
-
-let cache_tactic_notation (_, tobj) =
- let key = tobj.tacobj_key in
- let () = check_key key in
- Tacenv.register_alias key tobj.tacobj_body;
- Egramcoq.extend_tactic_grammar key tobj.tacobj_tacgram;
- Pptactic.declare_notation_tactic_pprule key tobj.tacobj_tacpp
-
-let open_tactic_notation i (_, tobj) =
- let key = tobj.tacobj_key in
- if Int.equal i 1 && not tobj.tacobj_local then
- Egramcoq.extend_tactic_grammar key tobj.tacobj_tacgram
-
-let load_tactic_notation i (_, tobj) =
- let key = tobj.tacobj_key in
- let () = check_key key in
- (** Only add the printing and interpretation rules. *)
- Tacenv.register_alias key tobj.tacobj_body;
- Pptactic.declare_notation_tactic_pprule key tobj.tacobj_tacpp;
- if Int.equal i 1 && not tobj.tacobj_local then
- Egramcoq.extend_tactic_grammar key tobj.tacobj_tacgram
-
-let subst_tactic_notation (subst, tobj) =
- { tobj with
- tacobj_key = Mod_subst.subst_kn subst tobj.tacobj_key;
- tacobj_body = Tacsubst.subst_tactic subst tobj.tacobj_body;
- }
-
-let classify_tactic_notation tacobj = Substitute tacobj
-
-let inTacticGrammar : tactic_grammar_obj -> obj =
- declare_object {(default_object "TacticGrammar") with
- open_function = open_tactic_notation;
- load_function = load_tactic_notation;
- cache_function = cache_tactic_notation;
- subst_function = subst_tactic_notation;
- classify_function = classify_tactic_notation}
-
-let cons_production_parameter l = function
- | GramTerminal _ -> l
- | GramNonTerminal (_,_,_,ido) -> Option.List.cons ido l
-
-let add_tactic_notation (local,n,prods,e) =
- let prods = List.map (interp_prod_item n) prods in
- let tags = make_tags prods in
- let pprule = {
- Pptactic.pptac_args = tags;
- pptac_prods = (n, List.map make_terminal_status prods);
- } in
- let ids = List.fold_left cons_production_parameter [] prods in
- let tac = Tacintern.glob_tactic_env ids (Global.env()) e in
- let parule = {
- tacgram_level = n;
- tacgram_prods = prods;
- } in
- let tacobj = {
- tacobj_key = make_fresh_key ();
- tacobj_local = local;
- tacobj_tacgram = parule;
- tacobj_tacpp = pprule;
- tacobj_body = tac;
- } in
- Lib.add_anonymous_leaf (inTacticGrammar tacobj)
-
-(**********************************************************************)
-(* ML Tactic entries *)
-
-type atomic_entry = string * Genarg.glob_generic_argument list option
-
-type ml_tactic_grammar_obj = {
- mltacobj_name : Tacexpr.ml_tactic_name;
- (** ML-side unique name *)
- mltacobj_prod : grammar_prod_item list list;
- (** Grammar rules generating the ML tactic. *)
-}
-
-(** ML tactic notations whose use can be restricted to an identifier are added
- as true Ltac entries. *)
-let extend_atomic_tactic name entries =
- let add_atomic (id, args) = match args with
- | None -> ()
- | Some args ->
- let body = Tacexpr.TacML (Loc.ghost, name, args) in
- Tacenv.register_ltac false false (Names.Id.of_string id) body
- in
- List.iter add_atomic entries
-
-let cache_ml_tactic_notation (_, obj) =
- extend_ml_tactic_grammar obj.mltacobj_name obj.mltacobj_prod
-
-let open_ml_tactic_notation i obj =
- if Int.equal i 1 then cache_ml_tactic_notation obj
-
-let inMLTacticGrammar : ml_tactic_grammar_obj -> obj =
- declare_object { (default_object "MLTacticGrammar") with
- open_function = open_ml_tactic_notation;
- cache_function = cache_ml_tactic_notation;
- classify_function = (fun o -> Substitute o);
- subst_function = (fun (_, o) -> o);
- }
-
-let add_ml_tactic_notation name prods atomic =
- let obj = {
- mltacobj_name = name;
- mltacobj_prod = prods;
- } in
- Lib.add_anonymous_leaf (inMLTacticGrammar obj);
- extend_atomic_tactic name atomic
-
-(**********************************************************************)
(* Printing grammar entries *)
let entry_buf = Buffer.create 64
@@ -340,7 +184,7 @@ let parse_format ((loc, str) : lstring) =
else
error "Empty format."
with reraise ->
- let (e, info) = Errors.push reraise in
+ let (e, info) = CErrors.push reraise in
let info = Loc.add_loc info loc in
iraise (e, info)
@@ -428,7 +272,7 @@ let rec interp_list_parser hd = function
(* To protect alphabetic tokens and quotes from being seen as variables *)
let quote_notation_token x =
let n = String.length x in
- let norm = Lexer.is_ident x in
+ let norm = CLexer.is_ident x in
if (n > 0 && norm) || (n > 2 && x.[0] == '\'') then "'"^x^"'"
else x
@@ -436,7 +280,7 @@ let rec raw_analyze_notation_tokens = function
| [] -> []
| String ".." :: sl -> NonTerminal ldots_var :: raw_analyze_notation_tokens sl
| String "_" :: _ -> error "_ must be quoted."
- | String x :: sl when Lexer.is_ident x ->
+ | String x :: sl when CLexer.is_ident x ->
NonTerminal (Names.Id.of_string x) :: raw_analyze_notation_tokens sl
| String s :: sl ->
Terminal (String.drop_simple_quotes s) :: raw_analyze_notation_tokens sl
@@ -540,10 +384,15 @@ let add_break_if_none n = function
| l -> UnpCut (PpBrk(n,0)) :: l
let check_open_binder isopen sl m =
+ let pr_token = function
+ | Terminal s -> str s
+ | Break n -> str "␣"
+ | _ -> assert false
+ in
if isopen && not (List.is_empty sl) then
errorlabstrm "" (str "as " ++ pr_id m ++
str " is a non-closed binder, no such \"" ++
- prlist_with_sep spc (function Terminal s -> str s | _ -> assert false) sl
+ prlist_with_sep spc pr_token sl
++ strbrk "\" is allowed to occur.")
(* Heuristics for building default printing rules *)
@@ -719,8 +568,8 @@ let is_not_small_constr = function
let rec define_keywords_aux = function
| GramConstrNonTerminal(e,Some _) as n1 :: GramConstrTerminal(IDENT k) :: l
when is_not_small_constr e ->
- Flags.if_verbose msg_info (str "Identifier '" ++ str k ++ str "' now a keyword");
- Lexer.add_keyword k;
+ Flags.if_verbose Feedback.msg_info (str "Identifier '" ++ str k ++ str "' now a keyword");
+ CLexer.add_keyword k;
n1 :: GramConstrTerminal(KEYWORD k) :: define_keywords_aux l
| n :: l -> n :: define_keywords_aux l
| [] -> []
@@ -728,8 +577,8 @@ let rec define_keywords_aux = function
(* Ensure that IDENT articulation terminal symbols are keywords *)
let define_keywords = function
| GramConstrTerminal(IDENT k)::l ->
- Flags.if_verbose msg_info (str "Identifier '" ++ str k ++ str "' now a keyword");
- Lexer.add_keyword k;
+ Flags.if_verbose Feedback.msg_info (str "Identifier '" ++ str k ++ str "' now a keyword");
+ CLexer.add_keyword k;
GramConstrTerminal(KEYWORD k) :: define_keywords_aux l
| l -> define_keywords_aux l
@@ -758,12 +607,12 @@ let make_production etyps symbols =
let typ = List.assoc m etyps in
distribute [GramConstrNonTerminal (typ, Some m)] ll
| Terminal s ->
- distribute [GramConstrTerminal (Lexer.terminal s)] ll
+ distribute [GramConstrTerminal (CLexer.terminal s)] ll
| Break _ ->
ll
| SProdList (x,sl) ->
let tkl = List.flatten
- (List.map (function Terminal s -> [Lexer.terminal s]
+ (List.map (function Terminal s -> [CLexer.terminal s]
| Break _ -> []
| _ -> anomaly (Pp.str "Found a non terminal token in recursive notation separator")) sl) in
match List.assoc x etyps with
@@ -824,24 +673,32 @@ type syntax_extension = {
synext_notgram : notation_grammar;
synext_unparsing : unparsing list;
synext_extra : (string * string) list;
+ synext_compat : Flags.compat_version option;
}
+let is_active_compat = function
+| None -> true
+| Some v -> 0 <= Flags.version_compare v !Flags.compat_version
+
type syntax_extension_obj = locality_flag * syntax_extension list
let cache_one_syntax_extension se =
let ntn = se.synext_notation in
let prec = se.synext_level in
+ let onlyprint = se.synext_notgram.notgram_onlyprinting in
try
let oldprec = Notation.level_of_notation ntn in
if not (Notation.level_eq prec oldprec) then error_incompatible_level ntn oldprec prec
with Not_found ->
- (* Reserve the notation level *)
- Notation.declare_notation_level ntn prec;
- (* Declare the parsing rule *)
- Egramcoq.extend_constr_grammar prec se.synext_notgram;
- (* Declare the printing rule *)
- Notation.declare_notation_printing_rule ntn
- ~extra:se.synext_extra (se.synext_unparsing, fst prec)
+ if is_active_compat se.synext_compat then begin
+ (* Reserve the notation level *)
+ Notation.declare_notation_level ntn prec;
+ (* Declare the parsing rule *)
+ if not onlyprint then Egramcoq.extend_constr_grammar prec se.synext_notgram;
+ (* Declare the notation rule *)
+ Notation.declare_notation_rule ntn
+ ~extra:se.synext_extra (se.synext_unparsing, fst prec) se.synext_notgram
+ end
let cache_syntax_extension (_, (_, sy)) =
List.iter cache_one_syntax_extension sy
@@ -874,9 +731,11 @@ let inSyntaxExtension : syntax_extension_obj -> obj =
let interp_modifiers modl =
let onlyparsing = ref false in
+ let onlyprinting = ref false in
+ let compat = ref None in
let rec interp assoc level etyps format extra = function
| [] ->
- (assoc,level,etyps,!onlyparsing,format,extra)
+ (assoc,level,etyps,!onlyparsing,!onlyprinting,!compat,format,extra)
| SetEntryType (s,typ) :: l ->
let id = Id.of_string s in
if Id.List.mem_assoc id etyps then
@@ -898,9 +757,15 @@ let interp_modifiers modl =
| SetAssoc a :: l ->
if not (Option.is_empty assoc) then error"An associativity is given more than once.";
interp (Some a) level etyps format extra l
- | SetOnlyParsing _ :: l ->
+ | SetOnlyParsing :: l ->
onlyparsing := true;
interp assoc level etyps format extra l
+ | SetOnlyPrinting :: l ->
+ onlyprinting := true;
+ interp assoc level etyps format extra l
+ | SetCompatVersion v :: l ->
+ compat := Some v;
+ interp assoc level etyps format extra l
| SetFormat ("text",s) :: l ->
if not (Option.is_empty format) then error "A format is given more than once.";
interp assoc level etyps (Some s) extra l
@@ -909,7 +774,7 @@ let interp_modifiers modl =
in interp None None [] None [] modl
let check_infix_modifiers modifiers =
- let (assoc,level,t,b,fmt,extra) = interp_modifiers modifiers in
+ let (_, _, t, _, _, _, _, _) = interp_modifiers modifiers in
if not (List.is_empty t) then
error "Explicit entry level or type unexpected in infix notation."
@@ -920,13 +785,25 @@ let check_useless_entry_types recvars mainvars etyps =
(pr_id x ++ str " is unbound in the notation.")
| _ -> ()
-let no_syntax_modifiers = function
- | [] | [SetOnlyParsing _] -> true
- | _ -> false
+let not_a_syntax_modifier = function
+| SetOnlyParsing -> true
+| SetOnlyPrinting -> true
+| SetCompatVersion _ -> true
+| _ -> false
-let is_only_parsing = function
- | [SetOnlyParsing _] -> true
- | _ -> false
+let no_syntax_modifiers mods = List.for_all not_a_syntax_modifier mods
+
+let is_only_parsing mods =
+ let test = function SetOnlyParsing -> true | _ -> false in
+ List.exists test mods
+
+let is_only_printing mods =
+ let test = function SetOnlyPrinting -> true | _ -> false in
+ List.exists test mods
+
+let get_compat_version mods =
+ let test = function SetCompatVersion v -> Some v | _ -> None in
+ try Some (List.find_map test mods) with Not_found -> None
(* Compute precedences from modifiers (or find default ones) *)
@@ -973,11 +850,12 @@ let make_internalization_vars recvars mainvars typs =
let extratyps = List.map (fun (x,y) -> (y,List.assoc x maintyps)) recvars in
maintyps @ extratyps
-let make_interpretation_type isrec = function
+let make_interpretation_type isrec isonlybinding = function
| NtnInternTypeConstr when isrec -> NtnTypeConstrList
- | NtnInternTypeConstr | NtnInternTypeIdent -> NtnTypeConstr
+ | NtnInternTypeConstr | NtnInternTypeIdent ->
+ if isonlybinding then NtnTypeOnlyBinder else NtnTypeConstr
| NtnInternTypeBinder when isrec -> NtnTypeBinderList
- | NtnInternTypeBinder -> error "Type not allowed in recursive notation."
+ | NtnInternTypeBinder -> error "Type binder is only for use in recursive notations for binders."
let make_interpretation_vars recvars allvars =
let eq_subscope (sc1, l1) (sc2, l2) =
@@ -985,45 +863,65 @@ let make_interpretation_vars recvars allvars =
List.equal String.equal l1 l2
in
let check (x, y) =
- let (scope1, _) = Id.Map.find x allvars in
- let (scope2, _) = Id.Map.find y allvars in
+ let (_,scope1, _) = Id.Map.find x allvars in
+ let (_,scope2, _) = Id.Map.find y allvars in
if not (eq_subscope scope1 scope2) then error_not_same_scope x y
in
let () = List.iter check recvars in
let useless_recvars = List.map snd recvars in
let mainvars =
Id.Map.filter (fun x _ -> not (Id.List.mem x useless_recvars)) allvars in
- Id.Map.mapi (fun x (sc, typ) ->
- (sc, make_interpretation_type (Id.List.mem_assoc x recvars) typ)) mainvars
+ Id.Map.mapi (fun x (isonlybinding, sc, typ) ->
+ (sc, make_interpretation_type (Id.List.mem_assoc x recvars) isonlybinding typ)) mainvars
let check_rule_productivity l =
- if List.for_all (function NonTerminal _ -> true | _ -> false) l then
+ if List.for_all (function NonTerminal _ | Break _ -> true | _ -> false) l then
error "A notation must include at least one symbol.";
if (match l with SProdList _ :: _ -> true | _ -> false) then
error "A recursive notation must start with at least one symbol."
-let is_not_printable onlyparse noninjective = function
+let warn_notation_bound_to_variable =
+ CWarnings.create ~name:"notation-bound-to-variable" ~category:"parsing"
+ (fun () ->
+ strbrk "This notation will not be used for printing as it is bound to a single variable.")
+
+let warn_non_reversible_notation =
+ CWarnings.create ~name:"non-reversible-notation" ~category:"parsing"
+ (fun () ->
+ strbrk "This notation will not be used for printing as it is not reversible.")
+
+let is_not_printable onlyparse nonreversible = function
| NVar _ ->
- let () = if not onlyparse then
- msg_warning (strbrk "This notation will not be used for printing as it is bound to a single variable.")
- in
+ if not onlyparse then warn_notation_bound_to_variable ();
true
| _ ->
- if not onlyparse && noninjective then
- let () = msg_warning (strbrk "This notation will not be used for printing as it is not reversible.") in
- true
+ if not onlyparse && nonreversible then
+ (warn_non_reversible_notation (); true)
else onlyparse
let find_precedence lev etyps symbols =
- match symbols with
- | NonTerminal x :: _ ->
+ let first_symbol =
+ let rec aux = function
+ | Break _ :: t -> aux t
+ | h :: t -> h
+ | [] -> assert false (* rule is known to be productive *) in
+ aux symbols in
+ let last_is_terminal () =
+ let rec aux b = function
+ | Break _ :: t -> aux b t
+ | Terminal _ :: t -> aux true t
+ | _ :: t -> aux false t
+ | [] -> b in
+ aux false symbols in
+ match first_symbol with
+ | NonTerminal x ->
(try match List.assoc x etyps with
| ETConstr _ ->
error "The level of the leftmost non-terminal cannot be changed."
| ETName | ETBigint | ETReference ->
begin match lev with
| None ->
- ([msg_info,strbrk "Setting notation at level 0."],0)
+ ([Feedback.msg_info ?loc:None ,strbrk "Setting notation at level 0."],0)
| Some 0 ->
([],0)
| _ ->
@@ -1039,11 +937,9 @@ let find_precedence lev etyps symbols =
if Option.is_empty lev then
error "A left-recursive notation must have an explicit level."
else [],Option.get lev)
- | Terminal _ ::l when
- (match List.last symbols with Terminal _ -> true |_ -> false)
- ->
+ | Terminal _ when last_is_terminal () ->
if Option.is_empty lev then
- ([msg_info,strbrk "Setting notation at level 0."], 0)
+ ([Feedback.msg_info ?loc:None ,strbrk "Setting notation at level 0."], 0)
else [],Option.get lev
| _ ->
if Option.is_empty lev then error "Cannot determine the level.";
@@ -1055,6 +951,10 @@ let check_curly_brackets_notation_exists () =
error "Notations involving patterns of the form \"{ _ }\" are treated \n\
specially and require that the notation \"{ _ }\" is already reserved."
+let warn_skip_spaces_curly =
+ CWarnings.create ~name:"skip-spaces-curly" ~category:"parsing"
+ (fun () ->strbrk "Skipping spaces inside curly brackets")
+
(* Remove patterns of the form "{ _ }", unless it is the "{ _ }" notation *)
let remove_curly_brackets l =
let rec skip_break acc = function
@@ -1069,9 +969,10 @@ let remove_curly_brackets l =
let br',next' = skip_break [] l' in
(match next' with
| Terminal "}" as t2 :: l'' as l1 ->
- if not (List.equal Notation.symbol_eq l l0) || not (List.equal Notation.symbol_eq l' l1) then
- msg_warning (strbrk "Skipping spaces inside curly brackets");
- if deb && List.is_empty l'' then [t1;x;t2] else begin
+ if not (List.equal Notation.symbol_eq l l0) ||
+ not (List.equal Notation.symbol_eq l' l1) then
+ warn_skip_spaces_curly ();
+ if deb && List.is_empty l'' then [t1;x;t2] else begin
check_curly_brackets_notation_exists ();
x :: aux false l''
end
@@ -1081,7 +982,7 @@ let remove_curly_brackets l =
in aux true l
let compute_syntax_data df modifiers =
- let (assoc,n,etyps,onlyparse,fmt,extra) = interp_modifiers modifiers in
+ let (assoc,n,etyps,onlyparse,onlyprint,compat,fmt,extra) = interp_modifiers modifiers in
let assoc = match assoc with None -> (* default *) Some NonA | a -> a in
let toks = split_notation_string df in
let (recvars,mainvars,symbols) = analyze_notation_tokens toks in
@@ -1107,18 +1008,18 @@ let compute_syntax_data df modifiers =
let sy_data = (n,sy_typs,symbols',fmt) in
let sy_fulldata = (i_typs,ntn_for_grammar,prec,need_squash,sy_data) in
let df' = ((Lib.library_dp(),Lib.current_dirpath true),df) in
- let i_data = (onlyparse,recvars,mainvars,(ntn_for_interp,df')) in
+ let i_data = (onlyparse,onlyprint,compat,recvars,mainvars,(ntn_for_interp,df')) in
(* Return relevant data for interpretation and for parsing/printing *)
(msgs,i_data,i_typs,sy_fulldata,extra)
let compute_pure_syntax_data df mods =
- let (msgs,(onlyparse,_,_,_),_,sy_data,extra) = compute_syntax_data df mods in
+ let (msgs,(onlyparse,onlyprint,_,_,_,_),_,sy_data,extra) = compute_syntax_data df mods in
let msgs =
if onlyparse then
- (msg_warning,
+ (Feedback.msg_warning ?loc:None,
strbrk "The only parsing modifier has no effect in Reserved Notation.")::msgs
else msgs in
- msgs, sy_data, extra
+ msgs, sy_data, extra, onlyprint
(**********************************************************************)
(* Registration of notations interpretation *)
@@ -1128,6 +1029,8 @@ type notation_obj = {
notobj_scope : scope_name option;
notobj_interp : interpretation;
notobj_onlyparse : bool;
+ notobj_onlyprint : bool;
+ notobj_compat : Flags.compat_version option;
notobj_notation : notation * notation_location;
}
@@ -1138,9 +1041,12 @@ let open_notation i (_, nobj) =
let scope = nobj.notobj_scope in
let (ntn, df) = nobj.notobj_notation in
let pat = nobj.notobj_interp in
- if Int.equal i 1 && not (Notation.exists_notation_in_scope scope ntn pat) then begin
+ let fresh = not (Notation.exists_notation_in_scope scope ntn pat) in
+ let active = is_active_compat nobj.notobj_compat in
+ if Int.equal i 1 && fresh && active then begin
(* Declare the interpretation *)
- Notation.declare_notation_interpretation ntn scope pat df;
+ let onlyprint = nobj.notobj_onlyprint in
+ let () = Notation.declare_notation_interpretation ntn scope pat df ~onlyprint in
(* Declare the uninterpretation *)
if not nobj.notobj_onlyparse then
Notation.declare_uninterpretation (NotationRule (scope, ntn)) pat
@@ -1170,7 +1076,7 @@ let with_lib_stk_protection f x =
let fs = Lib.freeze `No in
try let a = f x in Lib.unfreeze fs; a
with reraise ->
- let reraise = Errors.push reraise in
+ let reraise = CErrors.push reraise in
let () = Lib.unfreeze fs in
iraise reraise
@@ -1187,7 +1093,10 @@ let contract_notation ntn =
let rec aux ntn i =
if i <= String.length ntn - 5 then
let ntn' =
- if String.is_sub "{ _ }" ntn i then
+ if String.is_sub "{ _ }" ntn i &&
+ (i = 0 || ntn.[i-1] = ' ') &&
+ (i = String.length ntn - 5 || ntn.[i+5] = ' ')
+ then
String.sub ntn 0 i ^ "_" ^
String.sub ntn (i+5) (String.length ntn -i-5)
else ntn in
@@ -1202,12 +1111,14 @@ let recover_syntax ntn =
let prec = Notation.level_of_notation ntn in
let pp_rule,_ = Notation.find_notation_printing_rule ntn in
let pp_extra_rules = Notation.find_notation_extra_printing_rules ntn in
- let pa_rule = Egramcoq.recover_constr_grammar ntn prec in
+ let pa_rule = Notation.find_notation_parsing_rules ntn in
{ synext_level = prec;
synext_notation = ntn;
synext_notgram = pa_rule;
synext_unparsing = pp_rule;
- synext_extra = pp_extra_rules }
+ synext_extra = pp_extra_rules;
+ synext_compat = None;
+ }
with Not_found ->
raise NoSyntaxRule
@@ -1220,27 +1131,29 @@ let recover_notation_syntax rawntn =
let sy = recover_syntax ntn in
let need_squash = not (String.equal ntn rawntn) in
let rules = if need_squash then recover_squash_syntax sy else [sy] in
- sy.synext_notgram.notgram_typs, rules
+ sy.synext_notgram.notgram_typs, rules, sy.synext_notgram.notgram_onlyprinting
(**********************************************************************)
(* Main entry point for building parsing and printing rules *)
-let make_pa_rule i_typs (n,typs,symbols,_) ntn =
+let make_pa_rule i_typs (n,typs,symbols,_) ntn onlyprint =
let assoc = recompute_assoc typs in
let prod = make_production typs symbols in
{ notgram_level = n;
notgram_assoc = assoc;
notgram_notation = ntn;
notgram_prods = prod;
- notgram_typs = i_typs; }
+ notgram_typs = i_typs;
+ notgram_onlyprinting = onlyprint;
+ }
let make_pp_rule (n,typs,symbols,fmt) =
match fmt with
| None -> [UnpBox (PpHOVB 0, make_hunks typs symbols n)]
| Some fmt -> hunks_of_format (n, List.split typs) (symbols, parse_format fmt)
-let make_syntax_rules (i_typs,ntn,prec,need_squash,sy_data) extra =
- let pa_rule = make_pa_rule i_typs sy_data ntn in
+let make_syntax_rules (i_typs,ntn,prec,need_squash,sy_data) extra onlyprint compat =
+ let pa_rule = make_pa_rule i_typs sy_data ntn onlyprint in
let pp_rule = make_pp_rule sy_data in
let sy = {
synext_level = prec;
@@ -1248,6 +1161,7 @@ let make_syntax_rules (i_typs,ntn,prec,need_squash,sy_data) extra =
synext_notgram = pa_rule;
synext_unparsing = pp_rule;
synext_extra = extra;
+ synext_compat = compat;
} in
(* By construction, the rule for "{ _ }" is declared, but we need to
redeclare it because the file where it is declared needs not be open
@@ -1263,26 +1177,27 @@ let to_map l =
let add_notation_in_scope local df c mods scope =
let (msgs,i_data,i_typs,sy_data,extra) = compute_syntax_data df mods in
- (* Prepare the parsing and printing rules *)
- let sy_rules = make_syntax_rules sy_data extra in
(* Prepare the interpretation *)
- let (onlyparse, recvars,mainvars, df') = i_data in
+ let (onlyparse, onlyprint, compat, recvars,mainvars, df') = i_data in
+ (* Prepare the parsing and printing rules *)
+ let sy_rules = make_syntax_rules sy_data extra onlyprint compat in
let i_vars = make_internalization_vars recvars mainvars i_typs in
let nenv = {
ninterp_var_type = to_map i_vars;
ninterp_rec_vars = to_map recvars;
- ninterp_only_parse = false;
} in
- let (acvars, ac) = interp_notation_constr nenv c in
+ let (acvars, ac, reversible) = interp_notation_constr nenv c in
let interp = make_interpretation_vars recvars acvars in
let map (x, _) = try Some (x, Id.Map.find x interp) with Not_found -> None in
- let onlyparse = is_not_printable onlyparse nenv.ninterp_only_parse ac in
+ let onlyparse = is_not_printable onlyparse (not reversible) ac in
let notation = {
notobj_local = local;
notobj_scope = scope;
notobj_interp = (List.map_filter map i_vars, ac);
(** Order is important here! *)
notobj_onlyparse = onlyparse;
+ notobj_onlyprint = onlyprint;
+ notobj_compat = compat;
notobj_notation = df';
} in
(* Ready to change the global state *)
@@ -1291,14 +1206,17 @@ let add_notation_in_scope local df c mods scope =
Lib.add_anonymous_leaf (inNotation notation);
df'
-let add_notation_interpretation_core local df ?(impls=empty_internalization_env) c scope onlyparse =
+let add_notation_interpretation_core local df ?(impls=empty_internalization_env) c scope onlyparse onlyprint compat =
let dfs = split_notation_string df in
let (recvars,mainvars,symbs) = analyze_notation_tokens dfs in
(* Recover types of variables and pa/pp rules; redeclare them if needed *)
- let i_typs = if not (is_numeral symbs) then begin
- let i_typs,sy_rules = recover_notation_syntax (make_notation_key symbs) in
- Lib.add_anonymous_leaf (inSyntaxExtension (local,sy_rules)); i_typs
- end else [] in
+ let i_typs, onlyprint = if not (is_numeral symbs) then begin
+ let i_typs,sy_rules,onlyprint' = recover_notation_syntax (make_notation_key symbs) in
+ let () = Lib.add_anonymous_leaf (inSyntaxExtension (local,sy_rules)) in
+ (** If the only printing flag has been explicitly requested, put it back *)
+ let onlyprint = onlyprint || onlyprint' in
+ i_typs, onlyprint
+ end else [], false in
(* Declare interpretation *)
let path = (Lib.library_dp(),Lib.current_dirpath true) in
let df' = (make_notation_key symbs,(path,df)) in
@@ -1306,18 +1224,19 @@ let add_notation_interpretation_core local df ?(impls=empty_internalization_env)
let nenv = {
ninterp_var_type = to_map i_vars;
ninterp_rec_vars = to_map recvars;
- ninterp_only_parse = false;
} in
- let (acvars, ac) = interp_notation_constr ~impls nenv c in
+ let (acvars, ac, reversible) = interp_notation_constr ~impls nenv c in
let interp = make_interpretation_vars recvars acvars in
let map (x, _) = try Some (x, Id.Map.find x interp) with Not_found -> None in
- let onlyparse = is_not_printable onlyparse nenv.ninterp_only_parse ac in
+ let onlyparse = is_not_printable onlyparse (not reversible) ac in
let notation = {
notobj_local = local;
notobj_scope = scope;
notobj_interp = (List.map_filter map i_vars, ac);
(** Order is important here! *)
notobj_onlyparse = onlyparse;
+ notobj_onlyprint = onlyprint;
+ notobj_compat = compat;
notobj_notation = df';
} in
Lib.add_anonymous_leaf (inNotation notation);
@@ -1326,20 +1245,20 @@ let add_notation_interpretation_core local df ?(impls=empty_internalization_env)
(* Notations without interpretation (Reserved Notation) *)
let add_syntax_extension local ((loc,df),mods) =
- let msgs, sy_data, extra = compute_pure_syntax_data df mods in
- let sy_rules = make_syntax_rules sy_data extra in
+ let msgs, sy_data, extra, onlyprint = compute_pure_syntax_data df mods in
+ let sy_rules = make_syntax_rules sy_data extra onlyprint None in
Flags.if_verbose (List.iter (fun (f,x) -> f x)) msgs;
Lib.add_anonymous_leaf (inSyntaxExtension(local,sy_rules))
(* Notations with only interpretation *)
let add_notation_interpretation ((loc,df),c,sc) =
- let df' = add_notation_interpretation_core false df c sc false in
+ let df' = add_notation_interpretation_core false df c sc false false None in
Dumpglob.dump_notation (loc,df') sc true
let set_notation_for_interpretation impls ((_,df),c,sc) =
(try ignore
- (silently (add_notation_interpretation_core false df ~impls c sc) false);
+ (silently (fun () -> add_notation_interpretation_core false df ~impls c sc false false None) ());
with NoSyntaxRule ->
error "Parsing rule for this notation has to be previously declared.");
Option.iter (fun sc -> Notation.open_close_scope (false,true,sc)) sc
@@ -1351,7 +1270,9 @@ let add_notation local c ((loc,df),modifiers) sc =
if no_syntax_modifiers modifiers then
(* No syntax data: try to rely on a previously declared rule *)
let onlyparse = is_only_parsing modifiers in
- try add_notation_interpretation_core local df c sc onlyparse
+ let onlyprint = is_only_printing modifiers in
+ let compat = get_compat_version modifiers in
+ try add_notation_interpretation_core local df c sc onlyparse onlyprint compat
with NoSyntaxRule ->
(* Try to determine a default syntax rule *)
add_notation_in_scope local df c modifiers sc
@@ -1444,11 +1365,10 @@ let add_syntactic_definition ident (vars,c) local onlyparse =
let nenv = {
ninterp_var_type = i_vars;
ninterp_rec_vars = Id.Map.empty;
- ninterp_only_parse = false;
} in
- let nvars, pat = interp_notation_constr nenv c in
- let () = nonprintable := nenv.ninterp_only_parse in
- let map id = let (sc, _) = Id.Map.find id nvars in (id, sc) in
+ let nvars, pat, reversible = interp_notation_constr nenv c in
+ let () = nonprintable := not reversible in
+ let map id = let (_,sc,_) = Id.Map.find id nvars in (id, sc) in
List.map map vars, pat
in
let onlyparse = match onlyparse with
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-06 09:06:25 +0000