From a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 27 Dec 2016 16:53:30 +0100 Subject: Imported Upstream version 8.6 --- toplevel/metasyntax.ml | 416 ++++++++++++++++++++----------------------------- 1 file changed, 168 insertions(+), 248 deletions(-) (limited to 'toplevel/metasyntax.ml') 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 @@ -42,161 +41,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 *) @@ -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 -- cgit v1.2.3