colibri2 0.4 · OCaml Package

Pattern

type t =

| Var of {
1. var : Colibri2_core.Expr.Term.Var.t;
2. ty : Colibri2_core.Expr.Ty.t;
}
| App of F.t * Colibri2_core.Expr.Ty.t list * t Colibri2_popop_lib.IArray.t
| Node of Colibri2_core.Node.t

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

exception Unconvertible

val of_term_exn : 
  ?coercion:bool ->
  subst:Colibri2_core.Ground.Subst.t ->
  Colibri2_core.Expr.Term.t ->
  t

val init : Colibri2_core.Ground.Subst.S.t

Singleton set with the empty substitution, can be used as initial value for the following function. Ground.Subst.empty should not be used since the functions will do nothing

val match_ty : 
  Colibri2_core.Ground.Subst.S.t ->
  Colibri2_core.Ground.Ty.t ->
  Colibri2_core.Expr.Ty.t ->
  Colibri2_core.Ground.Subst.S.t

match_ty substs ty pat match the ty on pat for each substitution of substs

val match_term : 
  _ Colibri2_core.Egraph.t ->
  Colibri2_core.Ground.Subst.S.t ->
  Colibri2_core.Node.t ->
  t ->
  Colibri2_core.Ground.Subst.S.t

match_term d substs n pat match the node n on the pattern pat for each substitution. Each return substitution corresponds to one given as input.

val check_ty : 
  Colibri2_core.Ground.Subst.t ->
  Colibri2_core.Ground.Ty.t ->
  Colibri2_core.Expr.Ty.t ->
  bool

check_ty subst ty pat checks that the pattern pat substituted by subst is equal to ty

val check_term : 
  _ Colibri2_core.Egraph.t ->
  Colibri2_core.Ground.Subst.t ->
  Colibri2_core.Node.t ->
  t ->
  bool

check_term d subst n pat checks the pattern pat substituted by subst is equal by congruence of d to n

val check_term_exists : 
  _ Colibri2_core.Egraph.t ->
  Colibri2_core.Ground.Subst.t ->
  t ->
  Colibri2_core.Node.S.t

check_term_exists d subst pat return nodes that are equal to the pattern pat substituted by the substitution subst

val match_any_term : 
  _ Colibri2_core.Egraph.t ->
  Colibri2_core.Ground.Subst.S.t ->
  t ->
  Colibri2_core.Ground.Subst.S.t

match_any_term d subst pat match the pattern pat to all the nodes of d for each substitution. Each return substitution corresponds to one given as input.

val get_pps : t -> t list -> PP.t list Colibri2_core.Expr.Term.Var.M.t

get_pps pat pats return for each variables the parent-parent pairs between position in pat and position in pat or pats

val env_ground_by_apps : 
  Colibri2_core.Ground.t Colibri2_stdlib.Context.Push.t F.EnvApps.t

The set of ground terms sorted by their top function

module EnvTy : 
  Colibri2_core.Datastructure.Memo with type key := Colibri2_core.Ground.Ty.t

val env_node_by_ty : 
  Colibri2_core.Node.t Colibri2_stdlib.Context.Push.t EnvTy.t

The set of nodes sorted by their type. A node can have multiple types

val find_existing_app : 
  ?fg:('a Colibri2_core.Egraph.t -> Colibri2_core.Ground.t -> unit) ->
  'a Colibri2_core.Egraph.t ->
  Colibri2_core.Ground.Subst.t ->
  F.t ->
  Colibri2_core.Expr.ty list ->
  Colibri2_core.Node.S.t Colibri2_popop_lib.IArray.t ->
  Colibri2_core.Node.S.t

find_existing_app d s f tyl nodes_args find existing application of f with one of the nodes as arguments

package colibri2