package term-indexing

  1. Overview
  2. Docs
Term indexing library

Install 

dune-project
 Dependency

github.com Readme Changelog MIT License Edit opam file Versions (1)

Authors

  1. I
    Ilias Garnier

Maintainers

  1. I
    igarnier@protonmail.com

Sources

0.0.1.tar.gz
md5=9ba5dcf909fde539e173daf8f13abffd
sha512=e84fb1104c420db346181416a1e95e60aeb1b757ed7456a6028a6dfd5096bb7888af7c1ad6ea1acb25e99318e86d1f75c82a072bbdc3ba8218e5b16778199dfe

doc/term-indexing/Term_indexing/Term/Make_hash_consed/index.html

Module Term.Make_hash_consedSource

The following functor instantiates a module to manipulate hash-consed terms over the signature P, using an implementation of persistent maps given by M.

Parameters

module P : Intf.Signature
module M : Intf.Map with type key = int

Signature

include Intf.Term_core with type prim = P.t with type t = P.t term
Sourcetype prim = P.t

The type of primitives, i.e. the symbols. Each value of type prim has a definite arity.

Sourcetype t = P.t term

The type of terms

type var := int
Sourceval pp_sexp : Format.formatter -> t -> unit

Pretty-printing of terms in s-exp format.

Sourceval prim : prim -> t array -> t

prim p ts constructs a term with head equal to p and subterms equal to ts

Raises Invalid_argument if the length of ts does not match the arity of p.

Sourceval var : var -> t

var v construcst a variable v

Sourceval destruct : (prim -> t array -> 'a) -> (var -> 'a) -> t -> 'a

destruct t ifprim ifvar performs case analysis on the term t

Sourceval is_var : t -> var option

is_var t is equal to var v if equal t (var v) or None if it is not the case

Sourceval fold : (t -> Path.t -> 'b -> 'b) -> 'b -> t -> 'b

fold f acc term folds f over the subterms of t

Sourceval get_subterm_fwd : t -> Path.forward -> t

get_subterm_fwd t fpth is the subterm of t at position defined by the forward path fpth.

Raises Get_subterm_oob if the path is out of bounds.

Sourcetype 'a var_map = 'a M.t

The type of polymorphic maps indexed by variables

include Intf.Hashed with type t := t
Sourceval compare : t -> t -> int

compare is a total order.

Sourceval equal : t -> t -> bool

equal s1 s2 tests whether s1 and s2 are equal.

Sourceval hash : t -> int

hash s is a hash of s.

Sourceval pp : Format.formatter -> t -> unit

pp fmt s prints a representation of s to the formatter fmt.

type var := int
Sourceval ub : t -> Int_option.t

ub t is an upper bound on the absolute value of variables contained in t. Equal to Int_option.none if t does not contain variables.

Sourceval map_variables : (int -> t) -> t -> t

map_variables f t replaces all variables var i present in t by f i.

Sourceval get_subterm : t -> Path.t -> t

get_subterm t pth is the subterm of t at position defined by the path pth.

Raise Get_subterm_oob if the path is out of bounds.

Sourceval subst : term:t -> path:Path.t -> (t -> t) -> t

subst ~term ~path f replaces the subterm of term at position path by f (get_subterm term path).

Sourceval fold_variables : (var -> Path.t -> 'b -> 'b) -> 'b -> t -> 'b

fold_variables f acc t folds f over the variables of t

Sourceval canon : t -> (unit -> var) -> var var_map * t

canon t gen canonicalizes the term t using the variable generator gen. Returns the canonicalized term as well as a map from old to canonicalized variables.

Sourceval uid : t -> int

uid t returns a unique integer attached to t. It is guaranteed that if two terms have the same uid, they are equal.