package term-tools

You can search for identifiers within the package.

in-package search v0.2.0

package term-tools

term-tools
- Term_tools
  - Int_option
  - Intf
    
    Hashed
    
    Map
    
    Pattern
    
    Signature
    
    Subst
    
    Term
    
    Term_core
    
    Unification
    
    Zipper
  - Make
    
    P
    
    Pattern
    
    Subst
    
    Term
    
    Term_graph
    
    Pattern
    
    Zipper
    
    Unification
    
    Zipper
  - Pattern
    
    Make
    
    P
    
    T
    
    Z
    
    Make_raw
    
    P
    
    T
    
    Z
    
    Make_with_hash_consing
    
    P
    
    T
    
    Z
  - Subst
    
    Make
    
    M
    
    P
    
    T
  - Term
    
    Default_map
    
    Make_hash_consed
    
    M
    
    P
  - Zipper
    
    Make
    
    P
    
    T
    
    Make_gen
    
    P
    
    S
    
    T
    
    Make_stateful
    
    P
    
    S
    
    T
    
    Zipper_impl

Legend:
Library
Module
Module type
Parameter
Class
Class type

type prim = P.t

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

type t = P.t Term.term

The type of terms

type var := int

include Intf.Hashed with type t := t

val compare : t -> t -> int

compare is a total order.

val equal : t -> t -> bool

equal s1 s2 tests whether s1 and s2 are equal.

val hash : t -> int

hash s is a hash of s.

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 ifprim ifvar t performs case analysis on the term t

val destruct2 : 
  (prim -> t array -> prim -> t array -> 'a) ->
  (prim -> t array -> int -> 'a) ->
  (int -> prim -> t array -> 'a) ->
  (int -> int -> 'a) ->
  t ->
  t ->
  'a

destruct2 fpp fpv fvp fvv t1 t2 performs case analysis on a pair of terms t1, t2

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 is_ground : t -> bool

is_ground t is true if and only if t does not contain any variable.

val get_subterm : t -> int list -> t

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

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

fold f acc t folds f over the subterms of t