1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
open Errors
open Util
open Pp
open Names
open Libnames
open Notation_term
open Libobject
open Lib
open Nameops
open Nametab
(* Syntactic definitions. *)
type version = Flags.compat_version option
let syntax_table =
Summary.ref (KNmap.empty : (interpretation*version) KNmap.t)
~name:"SYNTAXCONSTANT"
let add_syntax_constant kn c onlyparse =
syntax_table := KNmap.add kn (c,onlyparse) !syntax_table
let load_syntax_constant i ((sp,kn),(_,pat,onlyparse)) =
if Nametab.exists_cci sp then
errorlabstrm "cache_syntax_constant"
(pr_id (basename sp) ++ str " already exists");
add_syntax_constant kn pat onlyparse;
Nametab.push_syndef (Nametab.Until i) sp kn
let is_alias_of_already_visible_name sp = function
| _,NRef ref ->
let (dir,id) = repr_qualid (shortest_qualid_of_global Id.Set.empty ref) in
DirPath.is_empty dir && Id.equal id (basename sp)
| _ ->
false
let open_syntax_constant i ((sp,kn),(_,pat,onlyparse)) =
if not (is_alias_of_already_visible_name sp pat) then begin
Nametab.push_syndef (Nametab.Exactly i) sp kn;
match onlyparse with
| None ->
(* Redeclare it to be used as (short) name in case an other (distfix)
notation was declared inbetween *)
Notation.declare_uninterpretation (Notation.SynDefRule kn) pat
| _ -> ()
end
let cache_syntax_constant d =
load_syntax_constant 1 d;
open_syntax_constant 1 d
let subst_syntax_constant (subst,(local,pat,onlyparse)) =
(local,Notation_ops.subst_interpretation subst pat,onlyparse)
let classify_syntax_constant (local,_,_ as o) =
if local then Dispose else Substitute o
let in_syntax_constant
: bool * interpretation * Flags.compat_version option -> obj =
declare_object {(default_object "SYNTAXCONSTANT") with
cache_function = cache_syntax_constant;
load_function = load_syntax_constant;
open_function = open_syntax_constant;
subst_function = subst_syntax_constant;
classify_function = classify_syntax_constant }
type syndef_interpretation = (Id.t * subscopes) list * notation_constr
(* Coercions to the general format of notation that also supports
variables bound to list of expressions *)
let in_pat (ids,ac) = (List.map (fun (id,sc) -> (id,(sc,NtnTypeConstr))) ids,ac)
let out_pat (ids,ac) = (List.map (fun (id,(sc,typ)) -> (id,sc)) ids,ac)
let declare_syntactic_definition local id onlyparse pat =
let _ = add_leaf id (in_syntax_constant (local,in_pat pat,onlyparse)) in ()
let pr_syndef kn = pr_qualid (shortest_qualid_of_syndef Id.Set.empty kn)
let verbose_compat_notations = ref true
let is_verbose_compat () =
!verbose_compat_notations
let pr_compat_warning (kn, def, v) =
let pp_def = match def with
| [], NRef r -> spc () ++ str "is" ++ spc () ++ pr_global_env Id.Set.empty r
| _ -> strbrk " is a compatibility notation"
in
let since = strbrk " since Coq > " ++ str (Flags.pr_version v) ++ str "." in
pr_syndef kn ++ pp_def ++ since
let warn_compatibility_notation =
CWarnings.create ~name:"compatibility-notation"
~category:"deprecated" pr_compat_warning
let verbose_compat kn def = function
| Some v when is_verbose_compat () && Flags.version_strictly_greater v ->
warn_compatibility_notation (kn, def, v)
| _ -> ()
let search_syntactic_definition kn =
let pat,v = KNmap.find kn !syntax_table in
let def = out_pat pat in
verbose_compat kn def v;
def
open Goptions
let set_verbose_compat_notations =
declare_bool_option
{ optsync = true;
optdepr = false;
optname = "verbose compatibility notations";
optkey = ["Verbose";"Compat";"Notations"];
optread = (fun () -> !verbose_compat_notations);
optwrite = ((:=) verbose_compat_notations) }
|
