colibri2 0.4 (latest) · OCaml Package

module Subst : sig ... end

module Ty : sig ... end

type s = {

app : Expr.Term.Const.t;
tyargs : Ty.t list;
args : Node.t Colibri2_popop_lib.IArray.t;
ty : Ty.t;

}

module Term : Colibri2_popop_lib.Popop_stdlib.Datatype with type t = s

include Colibri2_popop_lib.Popop_stdlib.Datatype

include Colibri2_popop_lib.Popop_stdlib.OrderedHashedType

type 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 node : t -> Node.t

Return a class from a thterm

val sem : t -> s

Return the sem from a thterm

val index : s -> t

Return a theory term from the user type

val thterm : t -> ThTerm.t

val of_thterm : ThTerm.t -> t option

Return the user type if the ThTerm belongs to this module

val coerce_thterm : ThTerm.t -> t

Return the user type. Raise if the ThTerm does not belong to this module

val convert : ?subst:Subst.t -> _ Egraph.t -> Expr.Term.t -> Node.t

val apply : 
  _ Egraph.t ->
  Expr.Term.Const.t ->
  Ty.t list ->
  Node.t Colibri2_popop_lib.IArray.t ->
  s

val init : Egraph.wt -> unit

val register_converter : Egraph.wt -> (Egraph.wt -> t -> unit) -> unit

val tys : _ Egraph.t -> Node.t -> Ty.S.t

val add_ty : Egraph.wt -> Node.t -> Ty.t -> unit

module Defs : sig ... end

module ClosedQuantifier : sig ... end

module NotTotallyApplied : sig ... end

val convert_and_iter : 
  ('a -> t -> unit) ->
  ('a -> ClosedQuantifier.t -> unit) ->
  ('a -> NotTotallyApplied.t -> unit) ->
  'a ->
  Subst.t ->
  Expr.Term.t ->
  Node.t

Iter on the new ground terms when converting, bottom_up

val convert_one_app : 
  Subst.t ->
  'a Egraph.t ->
  Expr.term ->
  Expr.ty list ->
  Node.t Colibri2_popop_lib.IArray.t ->
  Expr.ty ->
  Node.t

val convert_one_cst : 
  Subst.t ->
  'a Egraph.t ->
  Dolmen_std.Expr.term_cst ->
  Node.t

val convert_one_binder : 
  Subst.t ->
  'a Egraph.t ->
  Expr.binder ->
  Expr.term ->
  Expr.ty ->
  Node.t

val convert_one_app_and_iter : 
  'a ->
  Expr.term ->
  Expr.ty list ->
  Node.t Colibri2_popop_lib.IArray.t ->
  Expr.ty ->
  Subst.t ->
  ('a -> t -> unit) ->
  ('a -> ClosedQuantifier.t -> unit) ->
  ('a -> NotTotallyApplied.t -> unit) ->
  Node.t

val convert_one_cst_and_iter : 
  'a ->
  Expr.term_cst ->
  Subst.t ->
  ('a -> t -> unit) ->
  ('a -> NotTotallyApplied.t -> unit) ->
  Node.t

val convert_one_binder_and_iter : 
  'a ->
  Expr.binder ->
  Expr.term ->
  Expr.ty ->
  Subst.t ->
  ('a -> ClosedQuantifier.t -> unit) ->
  ('a -> NotTotallyApplied.t -> unit) ->
  Node.t

val convert_let_seq : 
  Subst.t ->
  'a ->
  (Dolmen_std.Expr.term_var * Expr.term) list ->
  Expr.term ->
  ('a -> Subst.t -> Expr.term -> Node.t) ->
  Node.t

val convert_let_par : 
  Subst.t ->
  'a ->
  (Dolmen_std.Expr.term_var * Expr.term) list ->
  Expr.term ->
  ('a -> Subst.t -> Expr.term -> Node.t) ->
  Node.t

package colibri2