term-indexing 0.0.1 (latest)

Term indexing.

type prim = P.t

prim is the type of primitive symbols used in terms.

type term = Term.t

term is the type of first-order terms.

type subst = Subst.t

subst is the type of substitutions, i.e. finite functions from variables to term.

type var := int

type internal_term

internal_term is the internal representation of terms in the index.

Due to the details of the implementation, it might be the case that the result of querying the index is a term containing cycle. This might occur if for instance the querying term contains variables overlapping the terms contained in the index.

The type internal_term is also used to represent substitutions.

val is_cyclic : internal_term -> bool

is_cyclic term checks whether a term contains a cycle or not.

val to_term : internal_term -> term

to_term term creates a new term representing the internal term term.

Raises Invalid_argument if term contains a cycle.

val get_subst : internal_term -> subst

get_subst term extracts a substitution out of term

val reduce : 
  (prim -> 'a array -> 'a) ->
  (var -> internal_term option -> 'a) ->
  internal_term ->
  'a

reduce fprim fvar term reduces term by recursively applying fprim on primitives applications and fvar on variables. If the variable is associated to a term in a substitution, the term is passed to fvar as Some term.

val destruct : 
  (prim -> internal_term array -> 'a) ->
  (var -> internal_term option -> 'a) ->
  internal_term ->
  'a

destruct ifprim ifvar t performs case analysis on the term t

val pp_internal_term : internal_term Fmt.t

type 'a t

'a t is the type of term indexes mapping terms to values of type 'a.

val pp : 'a Fmt.t -> 'a t Fmt.t

pp pp_val allows to pretty-print values of type 'a t given pp_val, a pretty-printer for values of type 'a.

val create : unit -> 'a t

create () creates an empty index.

The worst-case complexity of all operations below is proportional to the size of the index. Practical complexity depends heavily on the term distribution but should be much better.

val insert : term -> 'a -> 'a t -> unit

insert term v index associates the value v to term in index.

val update : term -> ('a option -> 'a) -> 'a t -> unit

update term f index associates the value f None to term if term is not already in index, or f (Some v) if v is already bound to term.

val iter : (term -> 'a -> unit) -> 'a t -> unit

iter f index iterates f on all bindings of index.

val iter_unifiable : (term -> 'a -> unit) -> 'a t -> term -> unit

iter_unfiable f index query applies f on all terms unifiable with query.

val iter_specialize : (term -> 'a -> unit) -> 'a t -> term -> unit

iter_specialize f index query applies f on all terms specializing query.

val iter_generalize : (term -> 'a -> unit) -> 'a t -> term -> unit

iter_generalize f index query applies f on all terms generalizing query.

The transient variants below are more efficient but must be used with care. The lifetime of the internal_terms ends when each call to the closure returns. Do not keep pointers to those internal_terms.

val iter_transient : (internal_term -> 'a -> unit) -> 'a t -> unit

iter_transient f index iterates f on all bindings of index. Note that the lifetime of the internal_term passed to f ends when f returns.

val iter_unifiable_transient : 
  (internal_term -> 'a -> unit) ->
  'a t ->
  term ->
  unit

iter_unfiable_transient f index query applies f on all terms unifiable with query. Note that the lifetime of the internal_term passed to f ends when f returns.

val iter_specialize_transient : 
  (internal_term -> 'a -> unit) ->
  'a t ->
  term ->
  unit

iter_specialize_transient f index query applies f on all terms specializing query. Note that the lifetime of the internal_term passed to f ends when f returns.

val iter_generalize_transient : 
  (internal_term -> 'a -> unit) ->
  'a t ->
  term ->
  unit

iter_generalize_transient f index query applies f on all terms generalizing query. Note that the lifetime of the internal_term passed to f ends when f returns.

package term-indexing