package colibri2

You can search for identifiers within the package.

in-package search v0.2.0

Package contains no libraries

type t

An InvertedPath is a way to go from one subterm of patterns to substitution of triggers. It allows to know which nodes merge can create new substitutions for a pattern and how to find them. Cf Efficient E-matching + modifications

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 exec : 
  _ Colibri2_core.Egraph.t ->
  (Colibri2_core.Ground.Subst.S.t Trigger.M.t
   * Colibri2_core.Ground.Subst.S.t Callback.M.t) ->
  Colibri2_core.Node.t ->
  t ->
  Colibri2_core.Ground.Subst.S.t Trigger.M.t
  * Colibri2_core.Ground.Subst.S.t Callback.M.t

exec d acc substs n ip adds to acc new substitutions to the triggers that are obtained by the execution of the invertedpath

val add_callback : 
  Colibri2_core.Egraph.wt ->
  Pattern.t ->
  (Colibri2_core.Egraph.wt -> Colibri2_core.Ground.Subst.t -> unit) ->
  unit

add_callback d pat callback wait for the pattern to be matched

val add_trigger : Colibri2_core.Egraph.wt -> Trigger.t -> unit

add_trigger d trigger wait for the trigger to be matched

module HPP : Colibri2_core.Datastructure.Memo with type key := PP.t

val pp_ips : t HPP.t

The database of inverted path for each parent-parent pairs

module HPC : Colibri2_core.Datastructure.Memo with type key := PC.t

val pc_ips : t HPC.t

The database of inverted path for each parent-child pairs

module HPT : Colibri2_core.Datastructure.Memo with type key := PT.t

val pt_ips : t HPT.t

The database of inverted path for each parent-type, needed for variables present unique times

module HPN : Colibri2_core.Datastructure.Memo with type key := PN.t

val pn_ips : t HPN.t

The database of inverted path for each parent-node pairs