diff options
Diffstat (limited to 'kernel/context.mli')
| -rw-r--r-- | kernel/context.mli | 151 |
1 files changed, 110 insertions, 41 deletions
diff --git a/kernel/context.mli b/kernel/context.mli index 1976e46d33..a69754cc29 100644 --- a/kernel/context.mli +++ b/kernel/context.mli @@ -26,21 +26,32 @@ open Names Individual declarations are then designated by de Bruijn indexes. *) module Rel : sig - (** Representation of {e local declarations}. - - [(name, None, typ)] represents a {e local assumption}. - - [(name, Some value, typ)] represents a {e local definition}. - *) module Declaration : sig - type t = Name.t * Constr.t option * Constr.t + (* local declaration *) + type t = LocalAssum of Name.t * Constr.t (* local assumption *) + | LocalDef of Name.t * Constr.t * Constr.t (* local definition *) - (** Map all terms in a given declaration. *) - val map : (Constr.t -> Constr.t) -> t -> t + (** Return the name bound by a given declaration. *) + val get_name : t -> Name.t - (** Reduce all terms in a given declaration to a single value. *) - val fold : (Constr.t -> 'a -> 'a) -> t -> 'a -> 'a + (** Return [Some value] for local-declarations and [None] for local-assumptions. *) + val get_value : t -> Constr.t option + + (** Return the type of the name bound by a given declaration. *) + val get_type : t -> Constr.t + + (** Set the name that is bound by a given declaration. *) + val set_name : Name.t -> t -> t + + (** Set the type of the bound variable in a given declaration. *) + val set_type : Constr.t -> t -> t + + (** Return [true] iff a given declaration is a local assumption. *) + val is_local_assum : t -> bool + + (** Return [true] iff a given declaration is a local definition. *) + val is_local_def : t -> bool (** Check whether any term in a given declaration satisfies a given predicate. *) val exists : (Constr.t -> bool) -> t -> bool @@ -50,6 +61,28 @@ sig (** Check whether the two given declarations are equal. *) val equal : t -> t -> bool + + (** Map the name bound by a given declaration. *) + val map_name : (Name.t -> Name.t) -> t -> t + + (** For local assumptions, this function returns the original local assumptions. + For local definitions, this function maps the value in the local definition. *) + val map_value : (Constr.t -> Constr.t) -> t -> t + + (** Map the type of the name bound by a given declaration. *) + val map_type : (Constr.t -> Constr.t) -> t -> t + + (** Map all terms in a given declaration. *) + val map_constr : (Constr.t -> Constr.t) -> t -> t + + (** Perform a given action on all terms in a given declaration. *) + val iter_constr : (Constr.t -> unit) -> t -> unit + + (** Reduce all terms in a given declaration to a single value. *) + val fold : (Constr.t -> 'a -> 'a) -> t -> 'a -> 'a + + val to_tuple : t -> Name.t * Constr.t option * Constr.t + val of_tuple : Name.t * Constr.t option * Constr.t -> t end (** Rel-context is represented as a list of declarations. @@ -63,6 +96,15 @@ sig (** Return a new rel-context enriched by with a given inner-most declaration. *) val add : Declaration.t -> t -> t + (** Return the number of {e local declarations} in a given context. *) + val length : t -> int + + (** Check whether given two rel-contexts are equal. *) + val equal : t -> t -> bool + + (** Return the number of {e local assumptions} in a given rel-context. *) + val nhyps : t -> int + (** Return a declaration designated by a given de Bruijn index. @raise Not_found if the designated de Bruijn index outside the range. *) val lookup : int -> t -> Declaration.t @@ -70,6 +112,9 @@ sig (** Map all terms in a given rel-context. *) val map : (Constr.t -> Constr.t) -> t -> t + (** Perform a given action on every declaration in a given rel-context. *) + val iter : (Constr.t -> unit) -> t -> unit + (** Reduce all terms in a given rel-context to a single value. Innermost declarations are processed first. *) val fold_inside : ('a -> Declaration.t -> 'a) -> init:'a -> t -> 'a @@ -78,15 +123,6 @@ sig Outermost declarations are processed first. *) val fold_outside : (Declaration.t -> 'a -> 'a) -> t -> init:'a -> 'a - (** Perform a given action on every declaration in a given rel-context. *) - val iter : (Constr.t -> unit) -> t -> unit - - (** Return the number of {e local declarations} in a given context. *) - val length : t -> int - - (** Return the number of {e local assumptions} in a given rel-context. *) - val nhyps : t -> int - (** Map a given rel-context to a list where each {e local assumption} is mapped to [true] and each {e local definition} is mapped to [false]. *) val to_tags : t -> bool list @@ -104,21 +140,32 @@ end Individual declarations are then designated by the identifiers they bind. *) module Named : sig - (** Representation of {e local declarations}. - - [(id, None, typ)] represents a {e local assumption}. - - [(id, Some value, typ)] represents a {e local definition}. - *) + (** Representation of {e local declarations}. *) module Declaration : sig - type t = Id.t * Constr.t option * Constr.t + type t = LocalAssum of Id.t * Constr.t + | LocalDef of Id.t * Constr.t * Constr.t - (** Map all terms in a given declaration. *) - val map : (Constr.t -> Constr.t) -> t -> t + (** Return the identifier bound by a given declaration. *) + val get_id : t -> Id.t - (** Reduce all terms in a given declaration to a single value. *) - val fold : (Constr.t -> 'a -> 'a) -> t -> 'a -> 'a + (** Return [Some value] for local-declarations and [None] for local-assumptions. *) + val get_value : t -> Constr.t option + + (** Return the type of the name bound by a given declaration. *) + val get_type : t -> Constr.t + + (** Set the identifier that is bound by a given declaration. *) + val set_id : Id.t -> t -> t + + (** Set the type of the bound variable in a given declaration. *) + val set_type : Constr.t -> t -> t + + (** Return [true] iff a given declaration is a local assumption. *) + val is_local_assum : t -> bool + + (** Return [true] iff a given declaration is a local definition. *) + val is_local_def : t -> bool (** Check whether any term in a given declaration satisfies a given predicate. *) val exists : (Constr.t -> bool) -> t -> bool @@ -128,6 +175,28 @@ sig (** Check whether the two given declarations are equal. *) val equal : t -> t -> bool + + (** Map the identifier bound by a given declaration. *) + val map_id : (Id.t -> Id.t) -> t -> t + + (** For local assumptions, this function returns the original local assumptions. + For local definitions, this function maps the value in the local definition. *) + val map_value : (Constr.t -> Constr.t) -> t -> t + + (** Map the type of the name bound by a given declaration. *) + val map_type : (Constr.t -> Constr.t) -> t -> t + + (** Map all terms in a given declaration. *) + val map_constr : (Constr.t -> Constr.t) -> t -> t + + (** Perform a given action on all terms in a given declaration. *) + val iter_constr : (Constr.t -> unit) -> t -> unit + + (** Reduce all terms in a given declaration to a single value. *) + val fold : (Constr.t -> 'a -> 'a) -> t -> 'a -> 'a + + val to_tuple : t -> Id.t * Constr.t option * Constr.t + val of_tuple : Id.t * Constr.t option * Constr.t -> t end (** Rel-context is represented as a list of declarations. @@ -141,13 +210,22 @@ sig (** Return a new rel-context enriched by with a given inner-most declaration. *) val add : Declaration.t -> t -> t + (** Return the number of {e local declarations} in a given named-context. *) + val length : t -> int + (** Return a declaration designated by an identifier of the variable bound in that declaration. @raise Not_found if the designated identifier is not bound in a given named-context. *) val lookup : Id.t -> t -> Declaration.t + (** Check whether given two rel-contexts are equal. *) + val equal : t -> t -> bool + (** Map all terms in a given named-context. *) val map : (Constr.t -> Constr.t) -> t -> t + (** Perform a given action on every declaration in a given named-context. *) + val iter : (Constr.t -> unit) -> t -> unit + (** Reduce all terms in a given named-context to a single value. Innermost declarations are processed first. *) val fold_inside : ('a -> Declaration.t -> 'a) -> init:'a -> t -> 'a @@ -156,15 +234,6 @@ sig Outermost declarations are processed first. *) val fold_outside : (Declaration.t -> 'a -> 'a) -> t -> init:'a -> 'a - (** Perform a given action on every declaration in a given named-context. *) - val iter : (Constr.t -> unit) -> t -> unit - - (** Return the number of {e local declarations} in a given named-context. *) - val length : t -> int - - (** Check whether given two named-contexts are equal. *) - val equal : t -> t -> bool - (** Return the set of all identifiers bound in a given named-context. *) val to_vars : t -> Id.Set.t @@ -180,7 +249,7 @@ sig module Declaration : sig type t = Id.t list * Constr.t option * Constr.t - val map : (Constr.t -> Constr.t) -> t -> t + val map_constr : (Constr.t -> Constr.t) -> t -> t end type t = Declaration.t list |