aboutsummaryrefslogtreecommitdiffhomepage
path: root/engine/nameops.mli
blob: 0fec8a925d0bb6b09f2aebdf79e203e91e285bed (plain)
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
135
136
137
138
(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017     *)
(*   \VV/  **************************************************************)
(*    //   *      This file is distributed under the terms of the       *)
(*         *       GNU Lesser General Public License Version 2.1        *)
(************************************************************************)

open Names

(** Identifiers and names *)

val make_ident : string -> int option -> Id.t
val repr_ident : Id.t -> string * int option

val atompart_of_id : Id.t -> string  (** remove trailing digits *)
val root_of_id : Id.t -> Id.t (** remove trailing digits, ' and _ *)

val add_suffix : Id.t -> string -> Id.t
val add_prefix : string -> Id.t -> Id.t

(** Below, by {i subscript} we mean a suffix composed solely from (decimal) digits. *)

val has_subscript       : Id.t -> bool

val increment_subscript : Id.t -> Id.t
(** Return the same identifier as the original one but whose {i subscript} is incremented.
    If the original identifier does not have a suffix, [0] is appended to it.

    Example mappings:

    [bar]   ↦ [bar0]

    [bar0]  ↦ [bar1]

    [bar00] ↦ [bar01]

    [bar1]  ↦ [bar2]

    [bar01] ↦ [bar01]

    [bar9]  ↦ [bar10]

    [bar09] ↦ [bar10]

    [bar99] ↦ [bar100]
*)

val forget_subscript    : Id.t -> Id.t

module Name : sig

  include module type of struct include Names.Name end

  exception IsAnonymous

  val fold_left : ('a -> Id.t -> 'a) -> 'a -> Name.t -> 'a
  (** [fold_left f na a] is [f id a] if [na] is [Name id], and [a] otherwise. *)

  val fold_right : (Id.t -> 'a -> 'a) -> Name.t -> 'a -> 'a
  (** [fold_right f a na] is [f a id] if [na] is [Name id], and [a] otherwise. *)

  val iter : (Id.t -> unit) -> Name.t -> unit
  (** [iter f na] does [f id] if [na] equals [Name id], nothing otherwise. *)

  val map : (Id.t -> Id.t) -> Name.t -> t
  (** [map f na] is [Anonymous] if [na] is [Anonymous] and [Name (f id)] if [na] is [Name id]. *)

  val fold_left_map : ('a -> Id.t -> 'a * Id.t) -> 'a -> Name.t -> 'a * Name.t
  (** [fold_left_map f a na] is [a',Name id'] when [na] is [Name id] and [f a id] is [(a',id')].
      It is [a,Anonymous] otherwise. *)

  val fold_right_map : (Id.t -> 'a -> Id.t * 'a) -> Name.t -> 'a -> Name.t * 'a
  (** [fold_right_map f na a] is [Name id',a'] when [na] is [Name id] and [f id a] is [(id',a')].
      It is [Anonymous,a] otherwise. *)

  val get_id : Name.t -> Id.t
  (** [get_id] associates [id] to [Name id]. @raise IsAnonymous otherwise. *)

  val pick : Name.t -> Name.t -> Name.t
  (** [pick na na'] returns [Anonymous] if both names are [Anonymous].
      Pick one of [na] or [na'] otherwise. *)

  val cons : Name.t -> Id.t list -> Id.t list
  (** [cons na l] returns [id::l] if [na] is [Name id] and [l] otherwise. *)

  val to_option : Name.t -> Id.t option
  (** [to_option Anonymous] is [None] and [to_option (Name id)] is [Some id] *)

end

(** Metavariables *)
val pr_meta : Constr.metavariable -> Pp.t
val string_of_meta : Constr.metavariable -> string

val out_name : Name.t -> Id.t
[@@ocaml.deprecated "Same as [Name.get_id]"]

val name_fold : (Id.t -> 'a -> 'a) -> Name.t -> 'a -> 'a
[@@ocaml.deprecated "Same as [Name.fold_right]"]

val name_iter : (Id.t -> unit) -> Name.t -> unit
[@@ocaml.deprecated "Same as [Name.iter]"]

val name_app : (Id.t -> Id.t) -> Name.t -> Name.t
[@@ocaml.deprecated "Same as [Name.map]"]

val name_fold_map : ('a -> Id.t -> 'a * Id.t) -> 'a -> Name.t -> 'a * Name.t
[@@ocaml.deprecated "Same as [Name.fold_left_map]"]

val name_max : Name.t -> Name.t -> Name.t
[@@ocaml.deprecated "Same as [Name.pick]"]

val name_cons : Name.t -> Id.t list -> Id.t list
[@@ocaml.deprecated "Same as [Name.cons]"]

val pr_name : Name.t -> Pp.t
[@@ocaml.deprecated "Same as [Name.print]"]

val pr_id : Id.t -> Pp.t
[@@ocaml.deprecated "Same as [Names.Id.print]"]

val pr_lab : Label.t -> Pp.t
[@@ocaml.deprecated "Same as [Names.Label.print]"]

(** Deprecated stuff to libnames *)
val default_library : DirPath.t
[@@ocaml.deprecated "Same as [Libnames.default_library]"]

val coq_root : module_ident (** "Coq" *)
[@@ocaml.deprecated "Same as [Libnames.coq_root]"]

val coq_string : string (** "Coq" *)
[@@ocaml.deprecated "Same as [Libnames.coq_string]"]

val default_root_prefix : DirPath.t
[@@ocaml.deprecated "Same as [Libnames.default_root_prefix]"]