hydra.rewriting module
Core rewrite and fold combinators for terms and types.
- hydra.rewriting.apply_inside_type_lambdas_and_annotations(f: Callable[[Term], Term], term0: Term) Term
Apply a term-level function inside any leading type lambdas.
- hydra.rewriting.fold_over_term(order: TraversalOrder, fld: Callable[[T0, Term], T0], b0: T0, term: Term) T0
Fold over a term, traversing its subterms in the specified order.
- hydra.rewriting.fold_over_type(order: TraversalOrder, fld: Callable[[T0, Type], T0], b0: T0, typ: Type) T0
Fold over a type, traversing its subtypes in the specified order.
- hydra.rewriting.fold_term_with_graph_and_path(f: Callable[[Callable[[T0, Term], T0], Sequence[SubtermStep], Graph, T0, Term], T0], cx0: Graph, val0: T0, term0: Term) T0
Fold over a term to produce a value, with both Graph and accessor path tracked. Like rewriteAndFoldTermWithGraphAndPath, but only folds without rewriting. The Graph is automatically updated when descending into lambdas, lets, and type lambdas.
- hydra.rewriting.map_beneath_type_annotations(f: Callable[[Type], Type], t: Type) Type
Apply a transformation to the first type beneath a chain of annotations.
- hydra.rewriting.rewrite_and_fold_term(f: Callable[[Callable[[T0, Term], tuple[T0, Term]], T0, Term], tuple[T0, Term]], term0: T0, v1: Term) tuple[T0, Term]
Rewrite a term, and at the same time, fold a function over it, accumulating a value.
- hydra.rewriting.rewrite_and_fold_term_with_graph(f: Callable[[Callable[[T0, Term], tuple[T0, Term]], Graph, T0, Term], tuple[T0, Term]], cx0: Graph, val0: T0, term0: Term) tuple[T0, Term]
Rewrite a term while folding to produce a value, with Graph updated as we descend into subterms. Combines the features of rewriteAndFoldTerm and rewriteTermWithGraph. The user function f receives a recurse function that handles subterm traversal and Graph management.
- hydra.rewriting.rewrite_and_fold_term_with_graph_and_path(f: Callable[[Callable[[T0, Term], tuple[T0, Term]], Sequence[SubtermStep], Graph, T0, Term], tuple[T0, Term]], cx0: Graph, val0: T0, term0: Term) tuple[T0, Term]
Rewrite a term while folding to produce a value, with both Graph and accessor path tracked. The path is a list of SubtermSteps representing the position from the root to the current term. Combines the features of rewriteAndFoldTermWithPath and Graph tracking. The Graph is automatically updated when descending into lambdas, lets, and type lambdas.
- hydra.rewriting.rewrite_and_fold_term_with_path(f: Callable[[Callable[[Sequence[SubtermStep], T0, Term], tuple[T0, Term]], Sequence[SubtermStep], T0, Term], tuple[T0, Term]], term0: T0, v1: Term) tuple[T0, Term]
Rewrite a term with path tracking, and fold a function over it, accumulating a value. The path is a list of SubtermSteps from root to current position.
- hydra.rewriting.rewrite_term(f: Callable[[Callable[[Term], Term], Term], Term], term0: Term) Term
Rewrite a term with a custom transformation function. The function receives a recursive walker and the current term and decides whether to recurse, replace, or both.
- hydra.rewriting.rewrite_term_m(f: Callable[[Callable[[Term], object], Term], object], term0: Term) object
Either-based term rewriting with custom transformation function.
- hydra.rewriting.rewrite_term_with_context(f: Callable[[Callable[[T0, Term], Term], T0, Term], Term], cx0: T0, term0: Term) Term
A variant of rewriteTerm which allows a context (e.g. a TypeContext) to be passed down to all subterms during rewriting.
- hydra.rewriting.rewrite_term_with_context_m(f: Callable[[Callable[[T0, Term], object], T0, Term], object], cx0: T0, term0: Term) object
Either-based variant of rewriteTermWithContextM which allows a context (e.g. a TypeContext) to be passed down to all subterms during rewriting.
- hydra.rewriting.rewrite_term_with_graph(f: Callable[[Callable[[Term], T0], Graph, Term], T0], cx0: Graph, term0: Term) T0
Rewrite a term with the help of a Graph which is updated as we descend into subterms.
- hydra.rewriting.rewrite_type(f: Callable[[Callable[[Type], Type], Type], Type], typ0: Type) Type
Rewrite a type with a custom transformation function. The function receives a recursive walker and the current type and decides whether to recurse, replace, or both.
- hydra.rewriting.rewrite_type_m(f: Callable[[Callable[[Type], object], Type], object], typ0: Type) object
Either-based type rewriting.
- hydra.rewriting.subterms_with_steps(v1: Term) Sequence[tuple[SubtermStep, Term]]
Find the children of a given term.
- hydra.rewriting.subtypes_with_steps(v1: Type) Sequence[tuple[SubtypeStep, Type]]
Find the children of a given type expression, each paired with the step by which it is reached.