Source file `abbreviation.ml`

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
131
132
133
134
(************************************************************************)
(*         *   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
open Notationextern

(* Abbreviations. *)

type abbreviation =
  { abbrev_pattern : interpretation;
    abbrev_onlyparsing : bool;
    abbrev_deprecation : Deprecation.t option;
    abbrev_also_in_cases_pattern : bool;
    abbrev_activated : bool; (* Not really necessary in practice *)
  }

let abbrev_table =
  Summary.ref (KNmap.empty : (full_path * abbreviation) KNmap.t)
    ~name:"ABBREVIATIONS"

let add_abbreviation kn sp abbrev =
  abbrev_table := KNmap.add kn (sp,abbrev) !abbrev_table

let toggle_abbreviation ~on ~use kn =
  let sp, data = KNmap.find kn !abbrev_table in
  if data.abbrev_activated != on then
    begin
      abbrev_table := KNmap.add kn (sp, {data with abbrev_activated = on}) !abbrev_table;
      match use with
      | OnlyPrinting -> ()
      | OnlyParsing | ParsingAndPrinting ->
         if on then
           begin
             Nametab.push_abbreviation (Nametab.Until 1) sp kn;
             Nametab.push_abbreviation (Nametab.Exactly 1) sp kn
           end
         else
           Nametab.remove_abbreviation sp kn
    end

let toggle_abbreviations ~on ~use filter =
  KNmap.fold (fun kn (sp,abbrev) () ->
      if abbrev.abbrev_activated != on && filter sp abbrev.abbrev_pattern then toggle_abbreviation ~on ~use kn)
  !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 sp 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 *)
      Notationextern.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;
      abbrev_activated = true;
    }
  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

(* Remark: do not check for activation (if not activated, it is already not supposed to be located) *)
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