package term-indexing

  1. Overview
  2. Docs

Term_core specifies the core types and operations related to first-order terms.

type prim

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

type t

The type of terms

type var := int
val pp : Format.formatter -> t -> unit

Pretty-printing of terms.

val pp_sexp : Format.formatter -> t -> unit

Pretty-printing of terms in s-exp format.

val 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.

val var : var -> t

var v construcst a variable v

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

destruct t ifprim ifvar performs case analysis on the term t

val 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

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

fold f acc term folds f over the subterms of t

val 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.

OCaml

Innovation. Community. Security.