package coq

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

Source file syntax_def.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
(************************************************************************)
(*         *   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

(* Syntactic definitions. *)

type syndef =
  { syndef_pattern : interpretation;
    syndef_onlyparsing : bool;
    syndef_deprecation : Deprecation.t option;
    syndef_also_in_cases_pattern : bool;
  }

let syntax_table =
  Summary.ref (KNmap.empty : syndef KNmap.t)
    ~name:"SYNDEFS"

let add_syntax_constant kn syndef =
  syntax_table := KNmap.add kn syndef !syntax_table

let load_syntax_constant i ((sp,kn),(_local,syndef)) =
  if Nametab.exists_cci sp then
    user_err ~hdr:"cache_syntax_constant"
      (Id.print (basename sp) ++ str " already exists");
  add_syntax_constant kn syndef;
  Nametab.push_syndef (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_syntax_constant i ((sp,kn),(_local,syndef)) =
  let pat = syndef.syndef_pattern in
  if not (Int.equal i 1 && is_alias_of_already_visible_name sp pat) then begin
    Nametab.push_syndef (Nametab.Exactly i) sp kn;
    if not syndef.syndef_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:syndef.syndef_also_in_cases_pattern (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,syndef)) =
  let syndef_pattern = Notation_ops.subst_interpretation subst syndef.syndef_pattern in
  (local, { syndef with syndef_pattern })

let classify_syntax_constant (local,_ as o) =
  if local then Dispose else Substitute o

let filtered_open_syntax_constant f i ((_,kn),_ as o) =
  let in_f = match f with
    | Unfiltered -> true
    | Names ns -> Globnames.(ExtRefSet.mem (SynDef kn) ns)
  in
  if in_f then open_syntax_constant i o

let in_syntax_constant : (bool * syndef) -> obj =
  declare_object {(default_object "SYNDEF") with
    cache_function = cache_syntax_constant;
    load_function = load_syntax_constant;
    open_function = filtered_open_syntax_constant;
    subst_function = subst_syntax_constant;
    classify_function = classify_syntax_constant }

let declare_syntactic_definition ~local ?(also_in_cases_pattern=true) deprecation id ~onlyparsing pat =
  let syndef =
    { syndef_pattern = pat;
      syndef_onlyparsing = onlyparsing;
      syndef_deprecation = deprecation;
      syndef_also_in_cases_pattern = also_in_cases_pattern;
    }
  in
  let _ = add_leaf id (in_syntax_constant (local,syndef)) in ()

let pr_syndef kn = pr_qualid (Nametab.shortest_qualid_of_syndef Id.Set.empty kn)

let warn_deprecated_syntactic_definition =
  Deprecation.create_warning ~object_name:"Notation" ~warning_name:"deprecated-syntactic-definition"
    pr_syndef

let search_syntactic_definition ?loc kn =
  let syndef = KNmap.find kn !syntax_table in
  Option.iter (fun d -> warn_deprecated_syntactic_definition ?loc (kn,d)) syndef.syndef_deprecation;
  syndef.syndef_pattern

let search_filtered_syntactic_definition ?loc filter kn =
  let syndef = KNmap.find kn !syntax_table in
  let res = filter syndef.syndef_pattern in
  if Option.has_some res then
    Option.iter (fun d -> warn_deprecated_syntactic_definition ?loc (kn,d)) syndef.syndef_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