ShotDs.Util.TermTraversal (shot_ds v1.0.2)

Copy Markdown View Source

Utilities for efficiently traversing and transforming Hol term DAGs.

Summary

Functions

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

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

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

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, cache \\ %{})

@spec fold_term(ShotDs.Data.Term.term_id(), (ShotDs.Data.Term.t(), [a] -> a), map()) ::
  {:ok, {a, map()}} | 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.

Returns a tuple {:ok, {result, final_cache}} or {:error, reason}.

fold_term!(term_id, fold_fn, cache \\ %{})

@spec fold_term!(ShotDs.Data.Term.term_id(), (ShotDs.Data.Term.t(), [a] -> a), map()) ::
  {a, map()}
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.

Returns a tuple {result, final_cache}.

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.

Returns a tuple {:ok, {result_id, final_cache}} or {:error, reason}.

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.

Returns a tuple {result_id, final_cache}.