ShotDs.Util.TermTraversal (shot_ds v1.0.0)

Copy Markdown View Source

Utilities for efficiently traversing and transforming Hol term DAGs.

Summary

Functions

fold_term(term_id, fold_fn)

A bottom-up fold combinator for reducing a term DAG into a single value.

fold_term!(term_id, fold_fn)

A bottom-up fold combinator for reducing a term DAG into a single value, erroring out if it encounters an invalid ID.

map_term(term_id, env, update_env, transform, short_circuit \\ fn _, _ -> false end, cache \\ %{})

A bottom-up map combinator on term DAGs for transforming term DAGs with environment passing and efficient caching.

map_term!(term_id, env, update_env, transform, short_circuit \\ fn _, _ -> false end, cache \\ %{})

A bottom-up map combinator on term DAGs for transforming term DAGs with environment passing and efficient caching, erroring out if it encounters an invalid ID.

Functions

fold_term(term_id, fold_fn)

@spec fold_term(ShotDs.Data.Term.term_id(), (ShotDs.Data.Term.t(), [a] -> a)) ::
  {:ok, a} | ShotDs.Stt.TermFactory.lookup_error_t()
when a: var

A bottom-up fold combinator for reducing a term DAG into a single value.

This combinator visits the leaves of the term graph first, applies the fold_fn, and propagates the computed result up to the parent terms.

Note

Unlike map_term, this basic fold does not implement DAG caching out of the box, so it will traverse shared subterms multiple times. It is best suited for lightweight reduction or formatting tasks.

fold_term!(term_id, fold_fn)

@spec fold_term!(ShotDs.Data.Term.term_id(), (ShotDs.Data.Term.t(), [a] -> a)) :: a
when a: var

A bottom-up fold combinator for reducing a term DAG into a single value, erroring out if it encounters an invalid ID.

This combinator visits the leaves of the term graph first, applies the fold_fn, and propagates the computed result up to the parent terms.

Note

Unlike map_term, this basic fold does not implement DAG caching out of the box, so it will traverse shared subterms multiple times. It is best suited for lightweight reduction or formatting tasks.

map_term(term_id, env, update_env, transform, short_circuit \\ fn _, _ -> false end, cache \\ %{})

@spec map_term(
  term_id :: ShotDs.Data.Term.term_id(),
  env :: a,
  update_env :: (ShotDs.Data.Term.t(), a -> a),
  transform :: (ShotDs.Data.Term.t(), [ShotDs.Data.Term.term_id()], a, map() ->
                  {{:ok, ShotDs.Data.Term.term_id()}
                   | ShotDs.Stt.TermFactory.lookup_error_t(), map()}),
  short_circuit :: (ShotDs.Data.Term.t(), a -> boolean()),
  cache :: map()
) ::
  {:ok, {ShotDs.Data.Term.term_id(), map()}}
  | ShotDs.Stt.TermFactory.lookup_error_t()

A bottom-up map combinator on term DAGs for transforming term DAGs with environment passing and efficient caching.

This function traverses a term and its arguments recursively. It evaluates in a post-order fashion (bottom-up), meaning the arguments of a term are mapped before the term itself is transformed. It uses a cache to memoize visits, ensuring that shared subterms are only processed once per unique environment.

map_term!(term_id, env, update_env, transform, short_circuit \\ fn _, _ -> false end, cache \\ %{})

@spec map_term!(
  term_id :: ShotDs.Data.Term.term_id(),
  env :: a,
  update_env :: (ShotDs.Data.Term.t(), a -> a),
  transform :: (ShotDs.Data.Term.t(), [ShotDs.Data.Term.term_id()], a, map() ->
                  {ShotDs.Data.Term.term_id(), map()}),
  short_circuit :: (ShotDs.Data.Term.t(), a -> boolean()),
  cache :: map()
) :: {ShotDs.Data.Term.term_id(), map()}

A bottom-up map combinator on term DAGs for transforming term DAGs with environment passing and efficient caching, erroring out if it encounters an invalid ID.

This function traverses a term and its arguments recursively. It evaluates in a post-order fashion (bottom-up), meaning the arguments of a term are mapped before the term itself is transformed. It uses a cache to memoize visits, ensuring that shared subterms are only processed once per unique environment.