Module LogtkDBEnv

module LogtkDBEnv: sig .. end

De Bruijn environments



type +'a t 
An environment that maps De Bruijn indices to values of type 'a.
val empty : 'a t
Empty environment
val is_empty : 'a t -> bool
Are there bindings?
val make : int -> 'a t
Empty environment of the given size
val singleton : 'a -> 'a t
Single binding
val push : 'a t -> 'a -> 'a t
Create a new environment, when entering a scope, where the De Bruijn index 0 is bound to the given value
val push_none : 'a t -> 'a t
Create a new environment, when entering a scope, where the De Bruijn index 0 is bound to nothing.
val push_none_multiple : 'a t -> int -> 'a t
Call push_none n times (after we've entered n scopes, for instances)
val pop : 'a t -> 'a t
Exit a scope, removing the top binding.
Raises Invalid_argument if the env is empty
val size : 'a t -> int
Number of scopes (number of times LogtkDBEnv.push or LogtkDBEnv.push_none were called to produce the given environement)
val find : 'a t -> int -> 'a option
Find to which value the given De Bruijn index is bound to, or return None
val find_exn : 'a t -> int -> 'a
Unsafe version of LogtkDBEnv.find.
Raises Failure if the index is not bound within env
val mem : 'a t -> int -> bool
mem env i returns true iff find env i returns Some _ rather than None, ie. whether the i-th De Bruijn variable is bound within env
val set : 'a t -> int -> 'a -> 'a t
Set the n-th variable to the given objects.
Raises Invalid_argument if the index isn't in the range 0... size-1
val num_bindings : 'a t -> int
How many variables are actually bound?
val map : ('a -> 'b) -> 'a t -> 'b t
Map bound objects to other bound objects
val of_list : (int * 'a) list -> 'a t
Map indices to objects