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
125
126
127
128
129
130
|
(************************************************************************)
(* 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 allow_compat_notations = ref true
let verbose_compat_notations = ref false
let is_verbose_compat () =
!verbose_compat_notations || not !allow_compat_notations
let verbose_compat kn def = function
| Some v when is_verbose_compat () && Flags.version_strictly_greater v ->
let act =
if !verbose_compat_notations then msg_warning else errorlabstrm ""
in
let pp_def = match def with
| [], NRef r -> str " is " ++ pr_global_env Id.Set.empty r
| _ -> str " is a compatibility notation"
in
let since = str " since Coq > " ++ str (Flags.pr_version v) ++ str "." in
act (pr_syndef kn ++ pp_def ++ since)
| _ -> ()
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) }
let set_compat_notations =
declare_bool_option
{ optsync = true;
optdepr = false;
optname = "accept compatibility notations";
optkey = ["Compat"; "Notations"];
optread = (fun () -> !allow_compat_notations);
optwrite = ((:=) allow_compat_notations) }
|
