package logtk

  1. Overview
  2. Docs
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module Logtk.DBEnvSource

De Bruijn environments

An environment is used to map De Bruijn indices to objects (or nothing).

This is low level and should be used with a lot of care (it's mostly used in InnerTerm.view.DB and a lot of coffee or aspiring at hand.

Sourcetype +'a t

An environment that maps De Bruijn indices to values of type 'a.

Sourceval empty : 'a t

Empty environment

Sourceval is_empty : 'a t -> bool

Are there bindings?

Sourceval make : int -> 'a t

Empty environment of the given size

Sourceval singleton : 'a -> 'a t

Single binding

Sourceval 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

Sourceval push_l_same_order : 'a t -> 'a list -> 'a t

push_l_same_order env l builds env l0 :: l1 :: … :: env

Sourceval push_l_rev : 'a t -> 'a list -> 'a t

push_l_rev env l builds env l(n-1) :: … :: l1 :: l0 :: env

Sourceval push_none : 'a t -> 'a t

Create a new environment, when entering a scope, where the De Bruijn index 0 is bound to nothing.

Sourceval push_none_multiple : 'a t -> int -> 'a t

Call push_none n times (after we've entered n scopes, for instances)

Sourceval pop : 'a t -> 'a t

Exit a scope, removing the top binding.

Sourceval pop_many : 'a t -> int -> 'a t

pop_many env n calls pop env n times

Sourceval size : 'a t -> int

Number of scopes (number of times push or push_none were called to produce the given environment)

Sourceval find : 'a t -> int -> 'a option

Find to which value the given De Bruijn index is bound to, or return None

Sourceval find_exn : 'a t -> int -> 'a

Unsafe version of find.

  • raises Failure

    if the index is not bound within env

Sourceval mem : _ 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

Sourceval set : 'a t -> int -> 'a -> 'a t

Set the n-th variable to the given objects.

Sourceval num_bindings : _ t -> int

How many variables are actually bound?

Sourceval map : ('a -> 'b) -> 'a t -> 'b t

Map bound objects to other bound objects

Sourceval filteri : (int -> 'a -> bool) -> 'a t -> 'a t
Sourceval of_list : (int * 'a) list -> 'a t

Map indices to objects

Sourceval to_list : 'a t -> 'a option list

List of underlying elements

Sourceval to_list_i : 'a t -> (int * 'a) option list

List of underlying elements

include Interfaces.PRINT1 with type 'a t := 'a t
Sourceval to_string : 'a CCFormat.printer -> 'a t -> string
OCaml

Innovation. Community. Security.