diff options
| -rw-r--r-- | interp/notation.ml | 33 | ||||
| -rw-r--r-- | interp/notation.mli | 2 | ||||
| -rw-r--r-- | toplevel/metasyntax.ml | 28 |
3 files changed, 42 insertions, 21 deletions
diff --git a/interp/notation.ml b/interp/notation.ml index 7ad104d036..e777e5c24e 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -44,8 +44,14 @@ type level = precedence * tolerability list type delimiters = string type notation_location = (DirPath.t * DirPath.t) * string +type notation_data = { + not_interp : interpretation; + not_location : notation_location; + not_onlyprinting : bool; +} + type scope = { - notations: (interpretation * notation_location) String.Map.t; + notations: notation_data String.Map.t; delimiters: delimiters option } @@ -380,7 +386,7 @@ let level_of_notation ntn = (* The mapping between notations and their interpretation *) -let declare_notation_interpretation ntn scopt pat df = +let declare_notation_interpretation ntn scopt pat df ~onlyprint = let scope = match scopt with Some s -> s | None -> default_scope in let sc = find_scope scope in let () = @@ -390,7 +396,12 @@ let declare_notation_interpretation ntn scopt pat df = | Some _ -> str " in scope " ++ str scope in Feedback.msg_warning (str "Notation " ++ str ntn ++ str " was already used" ++ which_scope) in - let sc = { sc with notations = String.Map.add ntn (pat,df) sc.notations } in + let notdata = { + not_interp = pat; + not_location = df; + not_onlyprinting = onlyprint; + } in + let sc = { sc with notations = String.Map.add ntn notdata sc.notations } in let () = scope_map := String.Map.add scope sc !scope_map in begin match scopt with | None -> scope_stack := SingleNotation ntn :: !scope_stack @@ -415,7 +426,9 @@ let rec find_interpretation ntn find = function find_interpretation ntn find scopes let find_notation ntn sc = - String.Map.find ntn (find_scope sc).notations + let n = String.Map.find ntn (find_scope sc).notations in + let () = if n.not_onlyprinting then raise Not_found in + (n.not_interp, n.not_location) let notation_of_prim_token = function | Numeral n when is_pos_or_zero n -> to_string n @@ -547,8 +560,8 @@ let exists_notation_in_scope scopt ntn r = let scope = match scopt with Some s -> s | None -> default_scope in try let sc = String.Map.find scope !scope_map in - let (r',_) = String.Map.find ntn sc.notations in - interpretation_eq r' r + let n = String.Map.find ntn sc.notations in + interpretation_eq n.not_interp r with Not_found -> false let isNVar_or_NHole = function NVar _ | NHole _ -> true | _ -> false @@ -805,7 +818,7 @@ let pr_named_scope prglob scope sc = ++ fnl () ++ pr_scope_classes scope ++ String.Map.fold - (fun ntn ((_,r),(_,df)) strm -> + (fun ntn { not_interp = (_, r); not_location = (_, df) } strm -> pr_notation_info prglob df r ++ fnl () ++ strm) sc.notations (mt ()) @@ -849,7 +862,7 @@ let browse_notation strict ntn map = let l = String.Map.fold (fun scope_name sc -> - String.Map.fold (fun ntn ((_,r),df) l -> + String.Map.fold (fun ntn { not_interp = (_, r); not_location = df } l -> if find ntn then (ntn,(scope_name,r,df))::l else l) sc.notations) map [] in List.sort (fun x y -> String.compare (fst x) (fst y)) l @@ -915,7 +928,7 @@ let locate_notation prglob ntn scope = let collect_notation_in_scope scope sc known = assert (not (String.equal scope default_scope)); String.Map.fold - (fun ntn ((_,r),(_,df)) (l,known as acc) -> + (fun ntn { not_interp = (_, r); not_location = (_, df) } (l,known as acc) -> if String.List.mem ntn known then acc else ((df,r)::l,ntn::known)) sc.notations ([],known) @@ -931,7 +944,7 @@ let collect_notations stack = | SingleNotation ntn -> if String.List.mem ntn knownntn then (all,knownntn) else - let ((_,r),(_,df)) = + let { not_interp = (_, r); not_location = (_, df) } = String.Map.find ntn (find_scope default_scope).notations in let all' = match all with | (s,lonelyntn)::rest when String.equal s default_scope -> diff --git a/interp/notation.mli b/interp/notation.mli index a85dc50f2f..b47e1975e3 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -109,7 +109,7 @@ type interp_rule = | SynDefRule of kernel_name val declare_notation_interpretation : notation -> scope_name option -> - interpretation -> notation_location -> unit + interpretation -> notation_location -> onlyprint:bool -> unit val declare_uninterpretation : interp_rule -> interpretation -> unit diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index 8d20bf3d14..586d9f1cf8 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -1006,6 +1006,7 @@ type notation_obj = { notobj_scope : scope_name option; notobj_interp : interpretation; notobj_onlyparse : bool; + notobj_onlyprint : bool; notobj_notation : notation * notation_location; } @@ -1018,7 +1019,8 @@ let open_notation i (_, nobj) = let pat = nobj.notobj_interp in if Int.equal i 1 && not (Notation.exists_notation_in_scope scope ntn pat) 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 @@ -1098,7 +1100,7 @@ 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 *) @@ -1163,6 +1165,7 @@ let add_notation_in_scope local df c mods scope = notobj_interp = (List.map_filter map i_vars, ac); (** Order is important here! *) notobj_onlyparse = onlyparse; + notobj_onlyprint = onlyprint; notobj_notation = df'; } in (* Ready to change the global state *) @@ -1171,14 +1174,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 = 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 @@ -1198,6 +1204,7 @@ let add_notation_interpretation_core local df ?(impls=empty_internalization_env) notobj_interp = (List.map_filter map i_vars, ac); (** Order is important here! *) notobj_onlyparse = onlyparse; + notobj_onlyprint = onlyprint; notobj_notation = df'; } in Lib.add_anonymous_leaf (inNotation notation); @@ -1214,12 +1221,12 @@ let add_syntax_extension local ((loc,df),mods) = (* 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 in Dumpglob.dump_notation (loc,df') sc true let set_notation_for_interpretation impls ((_,df),c,sc) = (try ignore - (silently (fun () -> add_notation_interpretation_core false df ~impls c sc false) ()); + (silently (fun () -> add_notation_interpretation_core false df ~impls c sc false false) ()); 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 @@ -1231,7 +1238,8 @@ 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 + try add_notation_interpretation_core local df c sc onlyparse onlyprint with NoSyntaxRule -> (* Try to determine a default syntax rule *) add_notation_in_scope local df c modifiers sc |