diff options
Diffstat (limited to 'kernel/context.mli')
| -rw-r--r-- | kernel/context.mli | 47 |
1 files changed, 38 insertions, 9 deletions
diff --git a/kernel/context.mli b/kernel/context.mli index 8acae73680..7b67e54ba4 100644 --- a/kernel/context.mli +++ b/kernel/context.mli @@ -24,6 +24,27 @@ open Names +type 'a binder_annot = { binder_name : 'a; binder_relevance : Sorts.relevance } +val eq_annot : ('a -> 'a -> bool) -> 'a binder_annot -> 'a binder_annot -> bool + +val hash_annot : ('a -> int) -> 'a binder_annot -> int + +val map_annot : ('a -> 'b) -> 'a binder_annot -> 'b binder_annot + +val make_annot : 'a -> Sorts.relevance -> 'a binder_annot + +val binder_name : 'a binder_annot -> 'a +val binder_relevance : 'a binder_annot -> Sorts.relevance + +val annotR : 'a -> 'a binder_annot +(** Always Relevant *) + +val nameR : Id.t -> Name.t binder_annot +(** Relevant + Name *) + +val anonR : Name.t binder_annot +(** Relevant + Anonymous *) + (** Representation of contexts that can capture anonymous as well as non-anonymous variables. Individual declarations are then designated by de Bruijn indexes. *) module Rel : @@ -32,8 +53,10 @@ sig sig (* local declaration *) type ('constr, 'types) pt = - | LocalAssum of Name.t * 'types (** name, type *) - | LocalDef of Name.t * 'constr * 'types (** name, value, type *) + | LocalAssum of Name.t binder_annot * 'types (** name, type *) + | LocalDef of Name.t binder_annot * 'constr * 'types (** name, value, type *) + + val get_annot : _ pt -> Name.t binder_annot (** Return the name bound by a given declaration. *) val get_name : ('c, 't) pt -> Name.t @@ -44,6 +67,8 @@ sig (** Return the type of the name bound by a given declaration. *) val get_type : ('c, 't) pt -> 't + val get_relevance : ('c, 't) pt -> Sorts.relevance + (** Set the name that is bound by a given declaration. *) val set_name : Name.t -> ('c, 't) pt -> ('c, 't) pt @@ -87,7 +112,7 @@ sig (** Reduce all terms in a given declaration to a single value. *) val fold_constr : ('c -> 'a -> 'a) -> ('c, 'c) pt -> 'a -> 'a - val to_tuple : ('c, 't) pt -> Name.t * 'c option * 't + val to_tuple : ('c, 't) pt -> Name.t binder_annot * 'c option * 't (** Turn [LocalDef] into [LocalAssum], identity otherwise. *) val drop_body : ('c, 't) pt -> ('c, 't) pt @@ -156,8 +181,10 @@ sig module Declaration : sig type ('constr, 'types) pt = - | LocalAssum of Id.t * 'types (** identifier, type *) - | LocalDef of Id.t * 'constr * 'types (** identifier, value, type *) + | LocalAssum of Id.t binder_annot * 'types (** identifier, type *) + | LocalDef of Id.t binder_annot * 'constr * 'types (** identifier, value, type *) + + val get_annot : _ pt -> Id.t binder_annot (** Return the identifier bound by a given declaration. *) val get_id : ('c, 't) pt -> Id.t @@ -168,6 +195,8 @@ sig (** Return the type of the name bound by a given declaration. *) val get_type : ('c, 't) pt -> 't + val get_relevance : ('c, 't) pt -> Sorts.relevance + (** Set the identifier that is bound by a given declaration. *) val set_id : Id.t -> ('c, 't) pt -> ('c, 't) pt @@ -208,8 +237,8 @@ sig (** Reduce all terms in a given declaration to a single value. *) val fold_constr : ('c -> 'a -> 'a) -> ('c, 'c) pt -> 'a -> 'a - val to_tuple : ('c, 't) pt -> Id.t * 'c option * 't - val of_tuple : Id.t * 'c option * 't -> ('c, 't) pt + val to_tuple : ('c, 't) pt -> Id.t binder_annot * 'c option * 't + val of_tuple : Id.t binder_annot * 'c option * 't -> ('c, 't) pt (** Turn [LocalDef] into [LocalAssum], identity otherwise. *) val drop_body : ('c, 't) pt -> ('c, 't) pt @@ -276,8 +305,8 @@ sig module Declaration : sig type ('constr, 'types) pt = - | LocalAssum of Id.t list * 'types - | LocalDef of Id.t list * 'constr * 'types + | LocalAssum of Id.t binder_annot list * 'types + | LocalDef of Id.t binder_annot list * 'constr * 'types val map_constr : ('c -> 'c) -> ('c, 'c) pt -> ('c, 'c) pt val of_named_decl : ('c, 't) Named.Declaration.pt -> ('c, 't) pt |