package colibri2

You can search for identifiers within the package.

in-package search v0.2.0

Package contains no libraries

type t

Normalizable terms

val name : string

include Colibri2_popop_lib.Popop_stdlib.Datatype with type t := t

include Colibri2_popop_lib.Popop_stdlib.OrderedHashedType with type t := t

val equal : t -> t -> bool

val pp : t Colibri2_popop_lib.Pp.pp

val hash_fold_t : t Base.Hash.folder

module M : Colibri2_popop_lib.Map_intf.PMap with type key = t

module S : 
  Colibri2_popop_lib.Map_intf.Set
    with type 'a M.t = 'a M.t
     and type M.key = M.key

module H : Colibri2_popop_lib.Exthtbl.Hashtbl.S with type key = t

include Base.Hashtbl.Key.S with type t := t

val compare : t Base__Ppx_compare_lib.compare

val sexp_of_t : t -> Sexplib0.Sexp.t

val hash : t -> int

val of_one_node : _ Colibri2_core.Egraph.t -> Colibri2_core.Node.t -> t

Build a value that represent one node

val is_one_node : t -> Colibri2_core.Node.t option

Test if a value represents one node

val subst : t -> Colibri2_core.Node.t -> t -> t option

subst p n q substitute n by q in p, if n is not in p None is returned, otherwise the substitution is returned

val normalize : t -> f:(Colibri2_core.Node.t -> t) -> t

norm p ~f normalize p using f

type data

An abstract type to avoid translating the map to sets in nodes

val nodes : t -> data Colibri2_core.Node.M.t

nodes t returns the node which are present in t

type info

Additional information useful for solving the equation

val info : _ Colibri2_core.Egraph.t -> t -> info

info d t returns the information for the given normalized term

val attach_info_change : 
  Colibri2_core.Egraph.wt ->
  (Colibri2_core.Egraph.rt ->
    Colibri2_core.Node.t ->
    Colibri2_core.Events.enqueue) ->
  unit

attach_info_change f should call the given function when information used for the computation of info changed. All unsolved equation which contains, nodes t, the given node will be looked again.

val solve : info -> info -> t solve_with_unsolved

solve t1 t2 solve the equation t1 = t2 by returning a substitution. Return Unsolved if the equation can't be yet solved

val set : 
  Colibri2_core.Egraph.wt ->
  Colibri2_core.Node.t ->
  old_:t ->
  new_:t ->
  unit

Called a new term equal to this node is found