Nameops.Name
include module type of struct include Names.Name end
Representation and operations on identifiers that are allowed to be anonymous (i.e. "_" in concrete syntax).
type t = Names.Name.t =
| Anonymous | (* anonymous identifier *) |
| Name of Names.Id.t | (* non-anonymous identifier *) |
val mk_name : Names.Id.t -> t
constructor
val is_anonymous : t -> bool
Return true
iff a given name is Anonymous
.
val is_name : t -> bool
Return true
iff a given name is Name _
.
val hash : t -> int
Hash over names.
val fold_left : ('a -> Names.Id.t -> 'a) -> 'a -> Names.Name.t -> 'a
fold_left f na a
is f id a
if na
is Name id
, and a
otherwise.
val fold_right : (Names.Id.t -> 'a -> 'a) -> Names.Name.t -> 'a -> 'a
fold_right f a na
is f a id
if na
is Name id
, and a
otherwise.
val iter : (Names.Id.t -> unit) -> Names.Name.t -> unit
iter f na
does f id
if na
equals Name id
, nothing otherwise.
val map : (Names.Id.t -> Names.Id.t) -> Names.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 -> Names.Id.t -> 'a * Names.Id.t) -> 'a -> Names.Name.t -> 'a * Names.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 : (Names.Id.t -> 'a -> Names.Id.t * 'a) -> Names.Name.t -> 'a -> Names.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 : Names.Name.t -> Names.Id.t
get_id
associates id
to Name id
.
val pick : Names.Name.t -> Names.Name.t -> Names.Name.t
pick na na'
returns Anonymous
if both names are Anonymous
. Pick one of na
or na'
otherwise.
val pick_annot : (Names.Name.t, 'r) Context.pbinder_annot -> (Names.Name.t, 'r) Context.pbinder_annot -> (Names.Name.t, 'r) Context.pbinder_annot
val cons : Names.Name.t -> Names.Id.t list -> Names.Id.t list
cons na l
returns id::l
if na
is Name id
and l
otherwise.
val to_option : Names.Name.t -> Names.Id.t option
to_option Anonymous
is None
and to_option (Name id)
is Some id