diff options
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/egramcoq.ml | 12 | ||||
| -rw-r--r-- | vernac/g_vernac.mlg | 1 | ||||
| -rw-r--r-- | vernac/himsg.ml | 16 | ||||
| -rw-r--r-- | vernac/metasyntax.ml | 360 | ||||
| -rw-r--r-- | vernac/ppvernac.ml | 1 | ||||
| -rw-r--r-- | vernac/prettyp.ml | 6 |
6 files changed, 231 insertions, 165 deletions
diff --git a/vernac/egramcoq.ml b/vernac/egramcoq.ml index 5e98f5ddc0..72e6d41969 100644 --- a/vernac/egramcoq.ml +++ b/vernac/egramcoq.ml @@ -249,7 +249,6 @@ type (_, _) entry = | TTName : ('self, lname) entry | TTReference : ('self, qualid) entry | TTBigint : ('self, string) entry -| TTString : ('self, string) entry | TTConstr : notation_entry * prod_info * 'r target -> ('r, 'r) entry | TTConstrList : notation_entry * prod_info * string Tok.p list * 'r target -> ('r, 'r list) entry | TTPattern : int -> ('self, cases_pattern_expr) entry @@ -370,14 +369,12 @@ let symbol_of_entry : type s r. _ -> _ -> (s, r) entry -> (s, r) mayrec_symbol = | TTName -> MayRecNo (Aentry Prim.name) | TTOpenBinderList -> MayRecNo (Aentry Constr.open_binders) | TTBigint -> MayRecNo (Aentry Prim.bigint) -| TTString -> MayRecNo (Aentry Prim.string) | TTReference -> MayRecNo (Aentry Constr.global) let interp_entry forpat e = match e with | ETProdName -> TTAny TTName | ETProdReference -> TTAny TTReference | ETProdBigint -> TTAny TTBigint -| ETProdString -> TTAny TTString | ETProdConstr (s,p) -> TTAny (TTConstr (s, p, forpat)) | ETProdPattern p -> TTAny (TTPattern p) | ETProdConstrList (s, p, tkl) -> TTAny (TTConstrList (s, p, tkl, forpat)) @@ -417,11 +414,6 @@ match e with | ForConstr -> push_constr subst (CAst.make @@ CPrim (Numeral (SPlus,NumTok.int v))) | ForPattern -> push_constr subst (CAst.make @@ CPatPrim (Numeral (SPlus,NumTok.int v))) end -| TTString -> - begin match forpat with - | ForConstr -> push_constr subst (CAst.make @@ CPrim (String v)) - | ForPattern -> push_constr subst (CAst.make @@ CPatPrim (String v)) - end | TTReference -> begin match forpat with | ForConstr -> push_constr subst (CAst.make @@ CRef (v, None)) @@ -537,10 +529,10 @@ let rec pure_sublevels' assoc from forpat level = function let make_act : type r. r target -> _ -> r gen_eval = function | ForConstr -> fun notation loc env -> let env = (env.constrs, env.constrlists, env.binders, env.binderlists) in - CAst.make ~loc @@ CNotation (notation, env) + CAst.make ~loc @@ CNotation (None, notation, env) | ForPattern -> fun notation loc env -> let env = (env.constrs, env.constrlists) in - CAst.make ~loc @@ CPatNotation (notation, env, []) + CAst.make ~loc @@ CPatNotation (None, notation, env, []) let extend_constr state forpat ng = let custom,n,_,_ = ng.notgram_level in diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg index 882be6449d..d597707d12 100644 --- a/vernac/g_vernac.mlg +++ b/vernac/g_vernac.mlg @@ -1235,7 +1235,6 @@ GRAMMAR EXTEND Gram syntax_extension_type: [ [ IDENT "ident" -> { ETIdent } | IDENT "global" -> { ETGlobal } | IDENT "bigint" -> { ETBigint } - | IDENT "string" -> { ETString } | IDENT "binder" -> { ETBinder true } | IDENT "constr" -> { ETConstr (InConstrEntry,None,DefaultLevel) } | IDENT "constr"; n = at_level_opt; b = OPT constr_as_binder_kind -> { ETConstr (InConstrEntry,b,n) } diff --git a/vernac/himsg.ml b/vernac/himsg.ml index dfc4631572..f6f6c4f1eb 100644 --- a/vernac/himsg.ml +++ b/vernac/himsg.ml @@ -324,11 +324,8 @@ let explain_unification_error env sigma p1 p2 = function strbrk ": cannot ensure that " ++ t ++ strbrk " is a subtype of " ++ u] | UnifUnivInconsistency p -> - if !Constrextern.print_universes then - [str "universe inconsistency: " ++ - Univ.explain_universe_inconsistency (Termops.pr_evd_level sigma) p] - else - [str "universe inconsistency"] + [str "universe inconsistency: " ++ + Univ.explain_universe_inconsistency (Termops.pr_evd_level sigma) p] | CannotSolveConstraint ((pb,env,t,u),e) -> let env = make_all_name_different env sigma in (strbrk "cannot satisfy constraint " ++ pr_leconstr_env env sigma t ++ @@ -1375,13 +1372,8 @@ let _ = CErrors.register_handler explain_exn_default let rec vernac_interp_error_handler = function | Univ.UniverseInconsistency i -> - let msg = - if !Constrextern.print_universes then - str "." ++ spc() ++ - Univ.explain_universe_inconsistency UnivNames.pr_with_global_universes i - else - mt() in - str "Universe inconsistency" ++ msg ++ str "." + str "Universe inconsistency." ++ spc() ++ + Univ.explain_universe_inconsistency UnivNames.pr_with_global_universes i ++ str "." | TypeError(ctx,te) -> let te = map_ptype_error EConstr.of_constr te in explain_type_error ctx Evd.empty te diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml index d39ee60c25..afff0347f5 100644 --- a/vernac/metasyntax.ml +++ b/vernac/metasyntax.ml @@ -286,32 +286,30 @@ let pr_notation_entry = function | InConstrEntry -> str "constr" | InCustomEntry s -> str "custom " ++ str s -let prec_assoc = let open Gramlib.Gramext in function - | RightA -> (L,E) - | LeftA -> (E,L) - | NonA -> (L,L) - let precedence_of_position_and_level from_level = function - | NumLevel n, BorderProd (_,None) -> n, Prec n | NumLevel n, BorderProd (b,Some a) -> - n, let (lp,rp) = prec_assoc a in if b == Left then lp else rp - | NumLevel n, InternalProd -> n, Prec n - | NextLevel, _ -> from_level, L - | DefaultLevel, _ -> - (* Fake value, waiting for PR#5 at herbelin's fork *) 200, - Any + (let open Gramlib.Gramext in + match a, b with + | RightA, Left -> LevelLt n + | RightA, Right -> LevelLe n + | LeftA, Left -> LevelLe n + | LeftA, Right -> LevelLt n + | NonA, _ -> LevelLt n) + | NumLevel n, _ -> LevelLe n + | NextLevel, _ -> LevelLt from_level + | DefaultLevel, _ -> LevelSome (** Computing precedences of subentries for parsing *) let precedence_of_entry_type (from_custom,from_level) = function | ETConstr (custom,_,x) when notation_entry_eq custom from_custom -> precedence_of_position_and_level from_level x - | ETConstr (custom,_,(NumLevel n,_)) -> n, Prec n + | ETConstr (custom,_,(NumLevel n,_)) -> LevelLe n | ETConstr (custom,_,(NextLevel,_)) -> user_err (strbrk "\"next level\" is only for sub-expressions in the same entry as where the notation is (" ++ quote (pr_notation_entry custom) ++ strbrk " is different from " ++ quote (pr_notation_entry from_custom) ++ str ").") - | ETPattern (_,n) -> let n = match n with None -> 0 | Some n -> n in n, Prec n - | _ -> 0, E (* should not matter *) + | ETPattern (_,n) -> let n = match n with None -> 0 | Some n -> n in LevelLe n + | _ -> LevelSome (* should not matter *) (** Computing precedences for future insertion of parentheses at the time of printing using hard-wired constr levels *) @@ -320,14 +318,14 @@ let unparsing_precedence_of_entry_type from_level = function (* Possible insertion of parentheses at printing time to deal with precedence in a constr entry is managed using [prec_less] in [ppconstr.ml] *) - snd (precedence_of_position_and_level from_level x) + precedence_of_position_and_level from_level x | ETConstr (custom,_,_) -> (* Precedence of printing for a custom entry is managed using explicit insertion of entry coercions at the time of building a [constr_expr] *) - Any - | ETPattern (_,n) -> (* in constr *) Prec (match n with Some n -> n | None -> 0) - | _ -> Any (* should not matter *) + LevelSome + | ETPattern (_,n) -> (* in constr *) LevelLe (match n with Some n -> n | None -> 0) + | _ -> LevelSome (* should not matter *) (* Some breaking examples *) (* "x = y" : "x /1 = y" (breaks before any symbol) *) @@ -396,12 +394,12 @@ let unparsing_metavar i from typs = let x = List.nth typs (i-1) in let prec = unparsing_precedence_of_entry_type from x in match x with - | ETConstr _ | ETGlobal | ETBigint | ETString -> - UnpMetaVar (i,prec) + | ETConstr _ | ETGlobal | ETBigint -> + UnpMetaVar prec | ETPattern _ -> - UnpBinderMetaVar (i,prec) + UnpBinderMetaVar prec | ETIdent -> - UnpBinderMetaVar (i,prec) + UnpBinderMetaVar prec | ETBinder isopen -> assert false @@ -455,10 +453,10 @@ let make_hunks etyps symbols from_level = (* We add NonTerminal for simulation but remove it afterwards *) else make true sl in let hunk = match typ with - | ETConstr _ -> UnpListMetaVar (i,prec,List.map snd sl') + | ETConstr _ -> UnpListMetaVar (prec,List.map snd sl') | ETBinder isopen -> check_open_binder isopen sl m; - UnpBinderListMetaVar (i,isopen,List.map snd sl') + UnpBinderListMetaVar (isopen,List.map snd sl') | _ -> assert false in (None, hunk) :: make_with_space b prods @@ -597,10 +595,10 @@ let hunks_of_format (from_level,(vars,typs)) symfmt = if not (List.is_empty sl) then error_format ?loc:(find_prod_list_loc loc_slfmt fmt) (); let symbs, l = aux (symbs,rfmt) in let hunk = match typ with - | ETConstr _ -> UnpListMetaVar (i,prec,slfmt) + | ETConstr _ -> UnpListMetaVar (prec,slfmt) | ETBinder isopen -> check_open_binder isopen sl m; - UnpBinderListMetaVar (i,isopen,slfmt) + UnpBinderListMetaVar (isopen,slfmt) | _ -> assert false in symbs, hunk :: l | symbs, (_,UnpBox (a,b)) :: fmt -> @@ -686,7 +684,6 @@ let prod_entry_type = function | ETIdent -> ETProdName | ETGlobal -> ETProdReference | ETBigint -> ETProdBigint - | ETString -> ETProdString | ETBinder _ -> assert false (* See check_binder_type *) | ETConstr (s,_,p) -> ETProdConstr (s,p) | ETPattern (_,n) -> ETProdPattern (match n with None -> 0 | Some n -> n) @@ -746,15 +743,11 @@ let recompute_assoc typs = let open Gramlib.Gramext in let pr_arg_level from (lev,typ) = let pplev = function - | (n,L) when Int.equal n from -> str "at next level" - | (n,E) -> str "at level " ++ int n - | (n,L) -> str "at level below " ++ int n - | (n,Prec m) when Int.equal m n -> str "at level " ++ int n - | (n,_) -> str "Unknown level" in - Ppvernac.pr_set_entry_type (fun _ -> (*TO CHECK*) mt()) typ ++ - (match typ with - | ETConstr _ | ETPattern _ -> spc () ++ pplev lev - | _ -> mt ()) + | LevelLt n when Int.equal n from -> spc () ++ str "at next level" + | LevelLe n -> spc () ++ str "at level " ++ int n + | LevelLt n -> spc () ++ str "at level below " ++ int n + | LevelSome -> mt () in + Ppvernac.pr_set_entry_type (fun _ -> (*TO CHECK*) mt()) typ ++ pplev lev let pr_level ntn (from,fromlevel,args,typs) = (match from with InConstrEntry -> mt () | InCustomEntry s -> str "in " ++ str s ++ spc()) ++ @@ -776,43 +769,97 @@ let error_parsing_incompatible_level ntn ntn' oldprec prec = spc() ++ str "while it is now required to be" ++ spc() ++ pr_level ntn prec ++ str ".") -type syntax_extension = { +let warn_incompatible_format = + CWarnings.create ~name:"notation-incompatible-format" ~category:"parsing" + (fun (specific,ntn) -> + let head,scope = match specific with + | None -> str "Notation", mt () + | Some LastLonelyNotation -> str "Lonely notation", mt () + | Some (NotationInScope sc) -> str "Notation", strbrk (" in scope " ^ sc) in + head ++ spc () ++ pr_notation ntn ++ + strbrk " was already defined with a different format" ++ scope ++ str ".") + +type syntax_parsing_extension = { synext_level : Notation_gram.level; synext_notation : notation; - synext_notgram : notation_grammar; - synext_unparsing : unparsing list; + synext_notgram : notation_grammar option; +} + +type syntax_printing_extension = { + synext_reserved : bool; + synext_unparsing : unparsing_rule; synext_extra : (string * string) list; } -type syntax_extension_obj = locality_flag * syntax_extension +let generic_format_to_declare ntn {synext_unparsing = (rules,_); synext_extra = extra_rules } = + try + let (generic_rules,_),reserved,generic_extra_rules = + Ppextend.find_generic_notation_printing_rule ntn in + if reserved && + (not (List.for_all2eq unparsing_eq rules generic_rules) + || extra_rules <> generic_extra_rules) + then + (warn_incompatible_format (None,ntn); true) + else + false + with Not_found -> true + +let check_reserved_format ntn = function + | None -> () + | Some sy_pp_rules -> let _ = generic_format_to_declare ntn sy_pp_rules in () + +let specific_format_to_declare (specific,ntn as specific_ntn) + {synext_unparsing = (rules,_); synext_extra = extra_rules } = + try + let (specific_rules,_),specific_extra_rules = + Ppextend.find_specific_notation_printing_rule specific_ntn in + if not (List.for_all2eq unparsing_eq rules specific_rules) + || extra_rules <> specific_extra_rules then + (warn_incompatible_format (Some specific,ntn); true) + else false + with Not_found -> true + +type syntax_extension_obj = + locality_flag * (syntax_parsing_extension * syntax_printing_extension option) let check_and_extend_constr_grammar ntn rule = try let ntn_for_grammar = rule.notgram_notation in if notation_eq ntn ntn_for_grammar then raise Not_found; let prec = rule.notgram_level in - let oldprec = Notgram_ops.level_of_notation ntn_for_grammar in - if not (Notgram_ops.level_eq prec oldprec) then error_parsing_incompatible_level ntn ntn_for_grammar oldprec prec; + let oldparsing,oldprec = Notgram_ops.level_of_notation ntn_for_grammar in + if not (Notgram_ops.level_eq prec oldprec) && oldparsing <> None then error_parsing_incompatible_level ntn ntn_for_grammar oldprec prec; + if oldparsing = None then raise Not_found with Not_found -> Egramcoq.extend_constr_grammar rule -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 = Notgram_ops.level_of_notation ~onlyprint ntn in - if not (Notgram_ops.level_eq prec oldprec) then error_incompatible_level ntn oldprec prec; - with Not_found -> - begin - (* Reserve the notation level *) - Notgram_ops.declare_notation_level ntn prec ~onlyprint; - (* Declare the parsing rule *) - if not onlyprint then List.iter (check_and_extend_constr_grammar ntn) se.synext_notgram.notgram_rules; - (* Declare the notation rule *) - declare_notation_rule ntn - ~extra:se.synext_extra (se.synext_unparsing, let (_,lev,_,_) = prec in lev) se.synext_notgram - end +let cache_one_syntax_extension (pa_se,pp_se) = + let ntn = pa_se.synext_notation in + let prec = pa_se.synext_level in + (* Check and ensure that the level and the precomputed parsing rule is declared *) + let oldparsing = + try + let oldparsing,oldprec = Notgram_ops.level_of_notation ntn in + if not (Notgram_ops.level_eq prec oldprec) && (oldparsing <> None || pa_se.synext_notgram = None) then error_incompatible_level ntn oldprec prec; + oldparsing + with Not_found -> + (* Declare the level and the precomputed parsing rule *) + let _ = Notgram_ops.declare_notation_level ntn pa_se.synext_notgram prec in + None in + (* Declare the parsing rule *) + begin match oldparsing, pa_se.synext_notgram with + | None, Some grams -> List.iter (check_and_extend_constr_grammar ntn) grams + | _ -> (* The grammars rules are canonically derived from the string and the precedence*) () + end; + (* Printing *) + match pp_se with + | None -> () + | Some pp_se -> + (* Check compatibility of format in case of two Reserved Notation *) + (* and declare or redeclare printing rule *) + if generic_format_to_declare ntn pp_se then + declare_generic_notation_printing_rules ntn + ~extra:pp_se.synext_extra ~reserved:pp_se.synext_reserved pp_se.synext_unparsing let cache_syntax_extension (_, (_, sy)) = cache_one_syntax_extension sy @@ -821,11 +868,11 @@ let subst_parsing_rule subst x = x let subst_printing_rule subst x = x -let subst_syntax_extension (subst, (local, sy)) = - (local, { sy with - synext_notgram = { sy.synext_notgram with notgram_rules = List.map (subst_parsing_rule subst) sy.synext_notgram.notgram_rules }; - synext_unparsing = subst_printing_rule subst sy.synext_unparsing; - }) +let subst_syntax_extension (subst, (local, (pa_sy,pp_sy))) = + (local, ({ pa_sy with + synext_notgram = Option.map (List.map (subst_parsing_rule subst)) pa_sy.synext_notgram }, + Option.map (fun pp_sy -> {pp_sy with synext_unparsing = subst_printing_rule subst pp_sy.synext_unparsing}) pp_sy) + ) let classify_syntax_definition (local, _ as o) = if local then Dispose else Substitute o @@ -990,7 +1037,7 @@ let set_entry_type from n etyps (x,typ) = | ETConstr (s,bko,n), InternalProd -> ETConstr (s,bko,(n,InternalProd)) | ETPattern (b,n), _ -> ETPattern (b,n) - | (ETIdent | ETBigint | ETString | ETGlobal | ETBinder _ as x), _ -> x + | (ETIdent | ETBigint | ETGlobal | ETBinder _ as x), _ -> x with Not_found -> ETConstr (from,None,(make_lev n from,typ)) in (x,typ) @@ -1012,7 +1059,7 @@ let join_auxiliary_recursive_types recvars etyps = let internalization_type_of_entry_type = function | ETBinder _ -> NtnInternTypeOnlyBinder - | ETConstr _ | ETBigint | ETString | ETGlobal + | ETConstr _ | ETBigint | ETGlobal | ETIdent | ETPattern _ -> NtnInternTypeAny let set_internalization_type typs = @@ -1034,7 +1081,7 @@ let make_interpretation_type isrec isonlybinding = function (* Others *) | ETIdent -> NtnTypeBinder NtnParsedAsIdent | ETPattern (ppstrict,_) -> NtnTypeBinder (NtnParsedAsPattern ppstrict) (* Parsed as ident/pattern, primarily interpreted as binder; maybe strict at printing *) - | ETBigint | ETString | ETGlobal -> NtnTypeConstr + | ETBigint | ETGlobal -> NtnTypeConstr | ETBinder _ -> if isrec then NtnTypeBinderList else anomaly Pp.(str "Type binder is only for use in recursive notations for binders.") @@ -1098,8 +1145,6 @@ type entry_coercion_kind = | IsEntryCoercion of notation_entry_level | IsEntryGlobal of string * int | IsEntryIdent of string * int - | IsEntryNumeral of string * int - | IsEntryString of string * int let is_coercion = function | Some (custom,n,_,[e]) -> @@ -1111,8 +1156,6 @@ let is_coercion = function else Some (IsEntryCoercion subentry) | ETGlobal, InCustomEntry s -> Some (IsEntryGlobal (s,n)) | ETIdent, InCustomEntry s -> Some (IsEntryIdent (s,n)) - | ETBigint, InCustomEntry s -> Some (IsEntryNumeral (s,n)) - | ETString, InCustomEntry s -> Some (IsEntryString (s,n)) | _ -> None) | Some _ -> assert false | None -> None @@ -1154,10 +1197,10 @@ let find_precedence custom lev etyps symbols onlyprint = user_err Pp.(str "The level of the leftmost non-terminal cannot be changed.") in (try match List.assoc x etyps, custom with | ETConstr (s,_,(NumLevel _ | NextLevel)), s' when s = s' -> test () - | (ETIdent | ETBigint | ETString | ETGlobal), _ -> + | (ETIdent | ETBigint | ETGlobal), _ -> begin match lev with | None -> - ([Feedback.msg_info ?loc:None ,strbrk "Setting notation at level 0."],0) + ([fun () -> Flags.if_verbose (Feedback.msg_info ?loc:None) (strbrk "Setting notation at level 0.")],0) | Some 0 -> ([],0) | _ -> @@ -1174,7 +1217,7 @@ let find_precedence custom lev etyps symbols onlyprint = else [],Option.get lev) | Some (Terminal _) when last_is_terminal () -> if Option.is_empty lev then - ([Feedback.msg_info ?loc:None ,strbrk "Setting notation at level 0."], 0) + ([fun () -> Flags.if_verbose (Feedback.msg_info ?loc:None) (strbrk "Setting notation at level 0.")], 0) else [],Option.get lev | Some _ -> if Option.is_empty lev then user_err Pp.(str "Cannot determine the level."); @@ -1227,7 +1270,7 @@ module SynData = struct extra : (string * string) list; (* XXX: Callback to printing, must remove *) - msgs : ((Pp.t -> unit) * Pp.t) list; + msgs : (unit -> unit) list; (* Fields for internalization *) recvars : (Id.t * Id.t) list; @@ -1325,15 +1368,19 @@ let compute_syntax_data ~local deprecation df modifiers = not_data = sy_fulldata; } +let warn_only_parsing_reserved_notation = + CWarnings.create ~name:"irrelevant-reserved-notation-only-parsing" ~category:"parsing" + (fun () -> strbrk "The only parsing modifier has no effect in Reserved Notation.") + let compute_pure_syntax_data ~local df mods = let open SynData in let sd = compute_syntax_data ~local None df mods in - let msgs = - if sd.only_parsing then - (Feedback.msg_warning ?loc:None, - strbrk "The only parsing modifier has no effect in Reserved Notation.")::sd.msgs - else sd.msgs in - { sd with msgs } + if sd.only_parsing + then + let msgs = (fun () -> warn_only_parsing_reserved_notation ?loc:None ())::sd.msgs in + { sd with msgs; only_parsing = false } + else + sd (**********************************************************************) (* Registration of notations interpretation *) @@ -1347,6 +1394,7 @@ type notation_obj = { notobj_onlyprint : bool; notobj_deprecation : Deprecation.t option; notobj_notation : notation * notation_location; + notobj_specific_pp_rules : syntax_printing_extension option; } let load_notation_common silently_define_scope_if_undefined _ (_, nobj) = @@ -1363,26 +1411,35 @@ let load_notation = load_notation_common true let open_notation i (_, nobj) = - let scope = nobj.notobj_scope in - let (ntn, df) = nobj.notobj_notation in - let pat = nobj.notobj_interp in - let onlyprint = nobj.notobj_onlyprint in - let deprecation = nobj.notobj_deprecation in - let fresh = not (Notation.exists_notation_in_scope scope ntn onlyprint pat) in - if Int.equal i 1 && fresh then begin - (* Declare the interpretation *) - let () = Notation.declare_notation_interpretation ntn scope pat df ~onlyprint deprecation in - (* Declare the uninterpretation *) - if not nobj.notobj_onlyparse then - Notation.declare_uninterpretation (NotationRule (scope, ntn)) pat; - (* Declare a possible coercion *) - (match nobj.notobj_coercion with - | Some (IsEntryCoercion entry) -> Notation.declare_entry_coercion ntn entry - | Some (IsEntryGlobal (entry,n)) -> Notation.declare_custom_entry_has_global entry n - | Some (IsEntryIdent (entry,n)) -> Notation.declare_custom_entry_has_ident entry n - | Some (IsEntryNumeral (entry,n)) -> Notation.declare_custom_entry_has_numeral entry n - | Some (IsEntryString (entry,n)) -> Notation.declare_custom_entry_has_string entry n - | None -> ()) + if Int.equal i 1 then begin + let scope = nobj.notobj_scope in + let (ntn, df) = nobj.notobj_notation in + let pat = nobj.notobj_interp in + let onlyprint = nobj.notobj_onlyprint in + let deprecation = nobj.notobj_deprecation in + let specific = match scope with None -> LastLonelyNotation | Some sc -> NotationInScope sc in + let specific_ntn = (specific,ntn) in + let fresh = not (Notation.exists_notation_in_scope scope ntn onlyprint pat) in + if fresh then begin + (* Declare the interpretation *) + let () = Notation.declare_notation_interpretation ntn scope pat df ~onlyprint deprecation in + (* Declare the uninterpretation *) + if not nobj.notobj_onlyparse then + Notation.declare_uninterpretation (NotationRule specific_ntn) pat; + (* Declare a possible coercion *) + (match nobj.notobj_coercion with + | Some (IsEntryCoercion entry) -> Notation.declare_entry_coercion specific_ntn entry + | Some (IsEntryGlobal (entry,n)) -> Notation.declare_custom_entry_has_global entry n + | Some (IsEntryIdent (entry,n)) -> Notation.declare_custom_entry_has_ident entry n + | None -> ()) + end; + (* Declare specific format if any *) + match nobj.notobj_specific_pp_rules with + | Some pp_sy -> + if specific_format_to_declare specific_ntn pp_sy then + Ppextend.declare_specific_notation_printing_rules + specific_ntn ~extra:pp_sy.synext_extra pp_sy.synext_unparsing + | None -> () end let cache_notation o = @@ -1424,23 +1481,30 @@ let with_syntax_protection f x = exception NoSyntaxRule let recover_notation_syntax ntn = - try - let prec = Notgram_ops.level_of_notation ~onlyprint:true ntn (* Be as little restrictive as possible *) in - let pp_rule,_ = find_notation_printing_rule ntn in - let pp_extra_rules = find_notation_extra_printing_rules ntn in - let pa_rule = 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; - } - with Not_found -> - raise NoSyntaxRule + let pa = + try + let pa_rule,prec = Notgram_ops.level_of_notation ntn in + { synext_level = prec; + synext_notation = ntn; + synext_notgram = pa_rule } + with Not_found -> + raise NoSyntaxRule in + let pp = + try + let pp_rule,reserved,pp_extra_rules = find_generic_notation_printing_rule ntn in + Some { + synext_reserved = reserved; + synext_unparsing = pp_rule; + synext_extra = pp_extra_rules; + } + with Not_found -> None in + pa,pp let recover_squash_syntax sy = - let sq = recover_notation_syntax (InConstrEntrySomeLevel,"{ _ }") in - sy :: sq.synext_notgram.notgram_rules + let sq,_ = recover_notation_syntax (InConstrEntrySomeLevel,"{ _ }") in + match sq.synext_notgram with + | Some gram -> sy :: gram + | None -> raise NoSyntaxRule (**********************************************************************) (* Main entry point for building parsing and printing rules *) @@ -1471,16 +1535,28 @@ let make_pp_rule level (typs,symbols) fmt = | Some fmt -> hunks_of_format (level, List.split typs) (symbols, parse_format fmt) -(* let make_syntax_rules i_typs (ntn,prec,need_squash) sy_data fmt extra onlyprint compat = *) -let make_syntax_rules (sd : SynData.syn_data) = let open SynData in +let make_parsing_rules (sd : SynData.syn_data) = let open SynData in let ntn_for_grammar, prec_for_grammar, need_squash = sd.not_data in - let custom,level,_,_ = sd.level in - let pa_rule = make_pa_rule prec_for_grammar sd.pa_syntax_data ntn_for_grammar need_squash in - let pp_rule = make_pp_rule level sd.pp_syntax_data sd.format in { + let pa_rule = + if sd.only_printing then None + else Some (make_pa_rule prec_for_grammar sd.pa_syntax_data ntn_for_grammar need_squash) + in { synext_level = sd.level; synext_notation = fst sd.info; - synext_notgram = { notgram_onlyprinting = sd.only_printing; notgram_rules = pa_rule }; - synext_unparsing = pp_rule; + synext_notgram = pa_rule; + } + +let warn_irrelevant_format = + CWarnings.create ~name:"irrelevant-format-only-parsing" ~category:"parsing" + (fun () -> str "The format modifier is irrelevant for only parsing rules.") + +let make_printing_rules reserved (sd : SynData.syn_data) = let open SynData in + let custom,level,_,_ = sd.level in + let pp_rule = make_pp_rule level sd.pp_syntax_data sd.format in + if sd.only_parsing then (if sd.format <> None then warn_irrelevant_format (); None) + else Some { + synext_reserved = reserved; + synext_unparsing = (pp_rule,level); synext_extra = sd.extra; } @@ -1494,9 +1570,10 @@ let to_map l = let add_notation_in_scope ~local deprecation df env c mods scope = let open SynData in let sd = compute_syntax_data ~local deprecation df mods in - (* Prepare the interpretation *) (* Prepare the parsing and printing rules *) - let sy_rules = make_syntax_rules sd in + let sy_pa_rules = make_parsing_rules sd in + let sy_pp_rules = make_printing_rules false sd in + (* Prepare the interpretation *) let i_vars = make_internalization_vars sd.recvars sd.mainvars sd.intern_typs in let nenv = { ninterp_var_type = to_map i_vars; @@ -1516,24 +1593,29 @@ let add_notation_in_scope ~local deprecation df env c mods scope = notobj_onlyprint = sd.only_printing; notobj_deprecation = sd.deprecation; notobj_notation = sd.info; + notobj_specific_pp_rules = sy_pp_rules; } in + let gen_sy_pp_rules = + if Ppextend.has_generic_notation_printing_rule (fst sd.info) then None + else sy_pp_rules (* We use the format of this notation as the default *) in + let _ = check_reserved_format (fst sd.info) sy_pp_rules in (* Ready to change the global state *) - Flags.if_verbose (List.iter (fun (f,x) -> f x)) sd.msgs; - Lib.add_anonymous_leaf (inSyntaxExtension (local, sy_rules)); + List.iter (fun f -> f ()) sd.msgs; + Lib.add_anonymous_leaf (inSyntaxExtension (local, (sy_pa_rules,gen_sy_pp_rules))); Lib.add_anonymous_leaf (inNotation notation); sd.info let add_notation_interpretation_core ~local df env ?(impls=empty_internalization_env) c scope onlyparse onlyprint deprecation = let (recvars,mainvars,symbs) = analyze_notation_tokens ~onlyprint df in (* Recover types of variables and pa/pp rules; redeclare them if needed *) - let level, i_typs, onlyprint = if not (is_numeral symbs) then begin - let sy = recover_notation_syntax (make_notation_key InConstrEntrySomeLevel symbs) in + let level, i_typs, onlyprint, pp_sy = if not (is_numeral symbs) then begin + let (pa_sy,pp_sy as sy) = recover_notation_syntax (make_notation_key InConstrEntrySomeLevel symbs) in let () = Lib.add_anonymous_leaf (inSyntaxExtension (local,sy)) in (* If the only printing flag has been explicitly requested, put it back *) - let onlyprint = onlyprint || sy.synext_notgram.notgram_onlyprinting in - let _,_,_,typs = sy.synext_level in - Some sy.synext_level, typs, onlyprint - end else None, [], false in + let onlyprint = onlyprint || pa_sy.synext_notgram = None in + let _,_,_,typs = pa_sy.synext_level in + Some pa_sy.synext_level, typs, onlyprint, pp_sy + end else None, [], false, None in (* Declare interpretation *) let path = (Lib.library_dp(), Lib.current_dirpath true) in let df' = (make_notation_key InConstrEntrySomeLevel symbs, (path,df)) in @@ -1556,6 +1638,7 @@ let add_notation_interpretation_core ~local df env ?(impls=empty_internalization notobj_onlyprint = onlyprint; notobj_deprecation = deprecation; notobj_notation = df'; + notobj_specific_pp_rules = pp_sy; } in Lib.add_anonymous_leaf (inNotation notation); df' @@ -1563,10 +1646,11 @@ let add_notation_interpretation_core ~local df env ?(impls=empty_internalization (* Notations without interpretation (Reserved Notation) *) let add_syntax_extension ~local ({CAst.loc;v=df},mods) = let open SynData in - let psd = compute_pure_syntax_data ~local df mods in - let sy_rules = make_syntax_rules {psd with deprecation = None} in - Flags.if_verbose (List.iter (fun (f,x) -> f x)) psd.msgs; - Lib.add_anonymous_leaf (inSyntaxExtension(local,sy_rules)) + let psd = {(compute_pure_syntax_data ~local df mods) with deprecation = None} in + let pa_rules = make_parsing_rules psd in + let pp_rules = make_printing_rules true psd in + List.iter (fun f -> f ()) psd.msgs; + Lib.add_anonymous_leaf (inSyntaxExtension(local,(pa_rules,pp_rules))) (* Notations with only interpretation *) diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml index c6ba4e2c29..314c423f65 100644 --- a/vernac/ppvernac.ml +++ b/vernac/ppvernac.ml @@ -126,7 +126,6 @@ open Pputils | ETPattern (b,n) -> pr_strict b ++ str"pattern" ++ pr_at_level (level_of_pattern_level n) | ETConstr (s,bko,lev) -> pr_notation_entry s ++ pr lev ++ pr_opt pr_constr_as_binder_kind bko | ETBigint -> str "bigint" - | ETString -> str "string" | ETBinder true -> str "binder" | ETBinder false -> str "closed binder" diff --git a/vernac/prettyp.ml b/vernac/prettyp.ml index 32c438c724..cdd93db884 100644 --- a/vernac/prettyp.ml +++ b/vernac/prettyp.ml @@ -547,7 +547,7 @@ let print_located_qualid ref = print_located_qualid "object" LocAny ref (**** Gallina layer *****) let gallina_print_typed_value_in_env env sigma (trm,typ) = - (pr_leconstr_env env sigma trm ++ fnl () ++ + (pr_leconstr_env ~inctx:true env sigma trm ++ fnl () ++ str " : " ++ pr_letype_env env sigma typ) (* To be improved; the type should be used to provide the types in the @@ -556,7 +556,7 @@ let gallina_print_typed_value_in_env env sigma (trm,typ) = synthesizes the type nat of the abstraction on u *) let print_named_def env sigma name body typ = - let pbody = pr_lconstr_env env sigma body in + let pbody = pr_lconstr_env ~inctx:true env sigma body in let ptyp = pr_ltype_env env sigma typ in let pbody = if Constr.isCast body then surround pbody else pbody in (str "*** [" ++ str name ++ str " " ++ @@ -598,7 +598,7 @@ let gallina_print_section_variable env sigma id = with_line_skip (print_name_infos (GlobRef.VarRef id)) let print_body env evd = function - | Some c -> pr_lconstr_env env evd c + | Some c -> pr_lconstr_env ~inctx:true env evd c | None -> (str"<no body>") let print_typed_body env evd (val_0,typ) = |