package coq

  1. Overview
  2. Docs
package coq
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

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
(************************************************************************)
(*         *   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
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct