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
|
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
(* v * Copyright INRIA, CNRS and contributors *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
open Pp
open CErrors
open Names
open Libnames
open Libobject
open Lib
open Notation_term
(* Abbreviations. *)
type abbreviation =
{ abbrev_pattern : interpretation;
abbrev_onlyparsing : bool;
abbrev_deprecation : Deprecation.t option;
abbrev_also_in_cases_pattern : bool;
}
let abbrev_table =
Summary.ref (KNmap.empty : abbreviation KNmap.t)
~name:"ABBREVIATIONS"
let add_abbreviation kn abbrev =
abbrev_table := KNmap.add kn abbrev !abbrev_table
let load_abbreviation i ((sp,kn),(_local,abbrev)) =
if Nametab.exists_cci sp then
user_err
(Id.print (basename sp) ++ str " already exists.");
add_abbreviation kn abbrev;
Nametab.push_abbreviation (Nametab.Until i) sp kn
let is_alias_of_already_visible_name sp = function
| _,NRef (ref,_) ->
let (dir,id) = repr_qualid (Nametab.shortest_qualid_of_global Id.Set.empty ref) in
DirPath.is_empty dir && Id.equal id (basename sp)
| _ ->
false
let open_abbreviation i ((sp,kn),(_local,abbrev)) =
let pat = abbrev.abbrev_pattern in
if not (Int.equal i 1 && is_alias_of_already_visible_name sp pat) then begin
Nametab.push_abbreviation (Nametab.Exactly i) sp kn;
if not abbrev.abbrev_onlyparsing then
(* Redeclare it to be used as (short) name in case an other (distfix)
notation was declared in between *)
Notation.declare_uninterpretation ~also_in_cases_pattern:abbrev.abbrev_also_in_cases_pattern (AbbrevRule kn) pat
end
let import_abbreviation i sp kn =
let abbrev = KNmap.get kn !abbrev_table in
open_abbreviation i ((sp,kn),(false,abbrev))
let cache_abbreviation d =
load_abbreviation 1 d;
open_abbreviation 1 d
let subst_abbreviation (subst,(local,abbrev)) =
let abbrev_pattern = Notation_ops.subst_interpretation subst abbrev.abbrev_pattern in
(local, { abbrev with abbrev_pattern })
let classify_abbreviation (local,_) =
if local then Dispose else Substitute
let inAbbreviation : Id.t -> (bool * abbreviation) -> obj =
declare_named_object {(default_object "ABBREVIATION") with
cache_function = cache_abbreviation;
load_function = load_abbreviation;
open_function = simple_open open_abbreviation;
subst_function = subst_abbreviation;
classify_function = classify_abbreviation }
let declare_abbreviation ~local ?(also_in_cases_pattern=true) deprecation id ~onlyparsing pat =
let abbrev =
{ abbrev_pattern = pat;
abbrev_onlyparsing = onlyparsing;
abbrev_deprecation = deprecation;
abbrev_also_in_cases_pattern = also_in_cases_pattern;
}
in
add_leaf (inAbbreviation id (local,abbrev))
let pr_abbreviation kn = pr_qualid (Nametab.shortest_qualid_of_abbreviation Id.Set.empty kn)
let warn_deprecated_abbreviation =
Deprecation.create_warning ~object_name:"Notation" ~warning_name:"deprecated-syntactic-definition"
pr_abbreviation
let search_abbreviation ?loc kn =
let abbrev = KNmap.find kn !abbrev_table in
Option.iter (fun d -> warn_deprecated_abbreviation ?loc (kn,d)) abbrev.abbrev_deprecation;
abbrev.abbrev_pattern
let search_filtered_abbreviation ?loc filter kn =
let abbrev = KNmap.find kn !abbrev_table in
let res = filter abbrev.abbrev_pattern in
if Option.has_some res then
Option.iter (fun d -> warn_deprecated_abbreviation ?loc (kn,d)) abbrev.abbrev_deprecation;
res
|
