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

(* Reserved names *)

open CErrors
open Util
open Pp
open Names
open Nameops
open Notation_term
open Notation_ops

type key =
  | RefKey of GlobRef.t
  | Oth

(** TODO: share code from Notation *)

let canonize_key env k = match k with
| Oth -> Oth
| RefKey gr ->
  let gr' = Environ.QGlobRef.canonize env gr in
  if gr' == gr then k else RefKey gr'

let mkRefKey env gr =
  RefKey (Environ.QGlobRef.canonize env gr)

let key_compare k1 k2 = match k1, k2 with
| RefKey gr1, RefKey gr2 -> GlobRef.UserOrd.compare gr1 gr2
| RefKey _, Oth -> -1
| Oth, RefKey _ -> 1
| Oth, Oth -> 0

module KeyOrd = struct type t = key let compare = key_compare end
module KeyMap = Map.Make(KeyOrd)

module ReservedSet :
sig
  type t
  val empty : t
  val add : (Id.t * notation_constr) -> t -> t
  val find : (Id.t -> notation_constr -> bool) -> t -> Id.t * notation_constr
end =
struct
  type t = (Id.t * notation_constr) list

  let empty = []

  let rec mem id c = function
  | [] -> false
  | (id', c') :: l ->
    if c == c' && Id.equal id id' then true else mem id c l

  let add p l =
    let (id, c) = p in
    if mem id c l then l else p :: l

  let rec find f = function
  | [] -> raise Not_found
  | (id, c) as p :: l -> if f id c then p else find f l
end


let keymap_add env key data map =
  let key = canonize_key env key in
  let old = try KeyMap.find key map with Not_found -> ReservedSet.empty in
  KeyMap.add key (ReservedSet.add data old) map

let reserve_table = Summary.ref Id.Map.empty ~name:"reserved-type"
let reserve_revtable = Summary.ref KeyMap.empty ~name:"reserved-type-rev"

let notation_constr_key env = function (* Rem: NApp(NRef ref,[]) stands for @ref *)
  | NApp (NRef (ref,_),args) -> mkRefKey env ref, Some (List.length args)
  | NList (_,_,NApp (NRef (ref,_),args),_,_)
  | NBinderList (_,_,NApp (NRef (ref,_),args),_,_) -> mkRefKey env ref, Some (List.length args)
  | NRef (ref,_) -> mkRefKey env ref, None
  | _ -> Oth, None

let add_reserved_type env (id,t) =
  let key = fst (notation_constr_key env t) in
  reserve_table := Id.Map.add id t !reserve_table;
  reserve_revtable := keymap_add env key (id, t) !reserve_revtable

let declare_reserved_type_binding env {CAst.loc;v=id} t =
  if not (Id.equal id (root_of_id id)) then
    user_err ?loc
      ((Id.print id ++ str
      " is not reservable: it must have no trailing digits, quote, or _."));
  begin try
    let _ = Id.Map.find id !reserve_table in
    user_err ?loc
    ((Id.print id ++ str " is already bound to a type."))
  with Not_found -> () end;
  add_reserved_type env (id,t)

let declare_reserved_type idl t =
  let env = Global.env () in
  List.iter (fun id -> declare_reserved_type_binding env id t) (List.rev idl)

let find_reserved_type id = Id.Map.find (root_of_id id) !reserve_table

let constr_key env c =
  try mkRefKey env (fst @@ Constr.destRef (fst (Constr.decompose_app c)))
  with Constr.DestKO -> Oth

let revert_reserved_type t =
  try
    let env = Global.env () in
    let t = EConstr.Unsafe.to_constr t in
    let reserved = KeyMap.find (constr_key env t) !reserve_revtable in
    let t = EConstr.of_constr t in
    let evd = Evd.from_env env in
    let t = Detyping.detype Detyping.Now Id.Set.empty env evd t in
    (* pedrot: if [Notation_ops.match_notation_constr] may raise [Failure _]
        then I've introduced a bug... *)
    let filter _ pat =
      try
        let _ = match_notation_constr ~print_univ:false t ~vars:Id.Set.empty ([], pat) in
        true
      with No_match -> false
    in
    let (id, _) = ReservedSet.find filter reserved in
    Name id
  with Not_found | Failure _ -> Anonymous

let _ = Namegen.set_reserved_typed_name revert_reserved_type