Crate stitch_core

Source

Modules§

compression
domains
egraphs
formats
rewriting
tutorials
A Guide-level Explanation of egg
util

Macros§

define_language
A macro to easily create a Language.
define_semantics
this macros defines two lazy static variables PRIMS and FUNCS
dsl_entries
dsl_entries_lookup_gen
fn_ptr_entries
load_args
this macro is used at the start of a DSL function to load arguments out of their args vec
load_args_lazy
this macro is used at the start of a DSL function to load arguments out of their args vec
rewrite
A macro to easily make Rewrites.
test_fn
Make a test function

Structs§

Arg
an argument to an abstraction. id is the main field here, we can use it to lookup the corresponding tree using egraph[id]
ArrowIter
ArrowIterTypeRef
AstDepth
A simple CostFunction that counts maximum ast depth.
AstSize
A simple CostFunction that counts total ast size.
BackoffScheduler
A RewriteScheduler that implements exponentional rule backoff.
BottomUpConfig
Bottom-up synthesis
CompressionStepConfig
Args for compression step
CompressionStepResult
the complete result of a single step of compression, this is a somewhat expensive data structure to create.
ConditionEqual
A Condition that checks if two terms are equivalent.
ConditionalApplier
An Applier that checks a Condition before applying.
Context
CriticalMultithreadData
This is the multithread data locked during the critical section of the algorithm.
CurriedFn
Wraps a DSL function in a struct that manages currying of the arguments which are fed in one at a time through .apply(). Example: the “+” primitive evaluates to a CurriedFn with arity 2 and empty partial_args. The expression (app + 3) evals to a CurriedFn with vec![3] as the partial_args. The expression (app (app + 3) 4) will evaluate to 7 (since .apply() will fill the last argument, notice that all arguments are filled, and return the result).
DSL
DSLEntry
Data
The analysis data associated with each Lambda node
DidMerge
Result of Analysis::merge indicating which of the inputs are different from the merged result.
Dot
A wrapper for an EGraph that can output GraphViz for visualization.
EClass
An equivalence class of enodes.
EGraph
A data structure to keep track of equalities between expressions.
Evaluator
Expansion
Explanation
A data structure representing an explanation that two terms are equivalent.
Expr
An untyped lambda calculus expression, much like egg::RecExpr but with a public nodes field and many attached functions. See Lambda for details on the individual nodes.
Extractor
Extracting a single RecExpr from an EGraph.
FinishedPattern
A finished invention
FlatTerm
A single term in an flattened explanation. After the first term in a FlatExplanation, each term will be annotated with exactly one backward_rule or one forward_rule. This can appear in children FlatTerms, indicating that the child is being rewritten.
Found
FoundExpr
FromOpError
A generic error for failing to parse an operator. This is the error type used by define_language! for FromOp::Error, and is a sensible choice when implementing FromOp manually.
HeapItem
The heap item used for heap-based worklists. Holds a pattern
Hole
IO
Id
A key to identify EClasses within an EGraph.
Input
Invention
At the end of the day we convert our Inventions into InventionExprs to make them standalone without needing to carry the EGraph around to figure out what the body Id points to.
Iteration
Data generated by running a Runner one iteration.
LambdaAnalysis
LazyVal
OrigamiModel
This wraps a model to make it behave roughly like the DreamCoder enumerator, which when it detects a fixpoint operator it give it 0% probability for using it lower in the program. Specifically what original DC does is it forces the program to start with (lam (fix $0 ??)), then after the fact it may strip away that fix() operator if the function var was never used in the body of the lambda. For us fix_flip() is the DC style fixpoint operator, and we set fix() to P=0 as it’s really just necessary internally to implement fix_flip(). In our case, we dont force it to start with a fix_flip() but instead let that just be the usual distribution for the toplevel operator, but then if we ever try to expand into a fix_flip() and we’re not at the top level then we set P=0 immediately. Furthermore since the first argument of fix is always $0 we modify probabilities to force that too.
PartialExpr
Pattern
A Pattern is a partial invention with holes. The simplest pattern is the single hole ?? which matches at all nodes in the program set. From this single hole in a top-down manner we grow more complex patterns like (+ ?? ??) and (+ 3 (* ?? ??)). Expanding a hole in a pattern always results in a pattern that matches at a subset of the places that the original pattern matched.
ProgramCost
the cost of a program, where app and lam cost 1, programs costs nothing, ivar and var and prim cost 100.
ProgramDepth
depth of a program. For example a leaf is depth 1.
RGB
RawTypeRef
RecExpr
A recursive expression from a user-defined Language.
Report
A report containing data about an entire Runner run.
Rewrite
A rewrite that searches for the lefthand side and applies the righthand side.
Runner
Faciliates running rewrites over an EGraph.
SaveState
SearchMatches
The result of searching a Searcher over one eclass.
SharedData
All the data shared among threads, mostly read-only except for the mutexes
SimpleScheduler
A very simple RewriteScheduler that runs every rewrite every time.
Stats
Various tracking stats
Subst
A substitition mapping Vars to eclass Ids.
Symbol
An interned string.
SymbolLang
A simple language used for testing.
Task
TermArgIter
TopDownConfig
Top-down synthesis
Tracking
Used for debugging tracking information
TreeTerm
An explanation for a term and its equivalent children. Each child is a proof transforming the initial child into the final child term. The initial term is given by taking each first sub-term in each child_proofs recursivly. The final term is given by all of the final terms in each child_proofs.
TypeRef
TypeSet
UniformModel
UtilityCalculation
Var
A variable for use in Patterns or Substs.
WorklistItem
ZIdExtension
tells you which zid if any you would get if you extended the depth (of whatever the current zid is) with any of these znodes.

Enums§

Color
ENodeOrVar
The language of Patterns.
ExpandsTo
The child-ignoring value of a node in the original set of programs. This tells us what the hole will expand into at this node.
HoleChoice
a strategy for choosing which hole to expand next in a partial pattern
InputFormat
Lambda
A node of an untyped lambda calculus expression compatible with egg but also used more widely throughout this crate. Note that there is no domain associated with this object. This makes it easy to run compression on domains that don’t have semantics yet, makes it easy to add new prims (eg learned functions), etc. You’ll have to specify a domain when you execute the expression, type check it, etc, but you can easily do that at the time through generics on those functions.
LazyValSource
Prod
RecExprParseError
An error type for failures when attempting to parse an s-expression as a RecExpr<L>.
StopReason
Error returned by Runner when it stops.
TNode
int [Term(“int”,None)]
Type
UnifyErr
Val
a value can either be some domain specific value Dom(D) like an Int, or it can be a primitive function or partially applied primitive function like + or (+ 2) or it can be a lambda function with some captured env like (lam (* $1 $0)) where $1 may have been captured from the surrounding code and this whole object may now be passed around
ZNode
A node in an ZPath Ord: Func < Body < Arg

Constants§

COST_NONTERMINAL
nonterminals (“app” and “lam”) cost 1/100th of a terminal (“var”, “ivar”, “prim”). This is because nonterminals can be autofilled based on the type of the hole you’re filling during most search methods.
COST_TERMINAL
SENTINEL

Traits§

Analysis
Arbitrary data associated with an EClass.
Applier
The righthand side of a Rewrite.
Colorful
Support &str and String, you can use "text".red() and s.red() for s:String
Condition
A condition to check in a ConditionalApplier.
CostFunction
A cost function that can be used by an Extractor.
Domain
The key trait that defines a domain
FromOp
A trait for parsing e-nodes. This is implemented automatically by define_language!.
FromVal
IterationData
Custom data to inject into the Iterations recorded by a Runner
Language
Trait that defines a Language whose terms will be in the EGraph.
LanguageChildren
A marker that defines acceptable children types for define_language!.
ProbabilisticModel
RewriteScheduler
A way to customize how a Runner runs Rewrites.
Searcher
The lefthand side of a Rewrite.

Functions§

add_expansions
arg_ivars_to_vars
assert_eq_val
convenience function for equality assertions
assert_error
assert_execution
convenience function for asserting that something executes to what you’d expect
associate_tasks
bottom_up
compression
Multistep compression. See compression_step if you’d just like to do a single step of compression.
compression_factor
compression_step
Takes a set of programs as an Expr with Programs as its root, and does one full step of compresison. Returns the top Inventions and the Expr rewritten under that invention along with other useful info in CompressionStepResult The number of inventions returned is based on cfg.inv_candidates
counts_ahash
same as Itertools::counts() but returns an FxHashMap instead of a HashMap
dc_inv_str
egraph_info
extract
convert an egraph Id to an Expr. Assumes one node per class (just picks the first node). Note that this could cause an infinite loop if the egraph didnt just have a single node in a class and instead the first node had a self loop.
extract_enode
like extract() but works on nodes
group_by_key
Takes a SORTED vector of copyable items and a key function and groups adjacent equal-key items into subvectors, returning the vector of these subvectors.
insert_arg_ivars
replaces upward refs to 0 with negative ivar
is_descendant
ivar_replace
Replace the ivars in an expr based on an i32->Expr map
ivar_to_dc
Replace the ivars in an expr based on an i32->Expr map
merge_max
A utility for implementing Analysis::merge when the Data type has a total ordering. This will take the maximum of the two values.
merge_min
A utility for implementing Analysis::merge when the Data type has a total ordering. This will take the minimum of the two values.
num_paths_to_node
Returns a vec from node id to number of places that node is used in the tree. Essentially this just follows all paths down from the root and logs how many times it encounters each node
ok
convenience function for returning arguments from a DSL function
programs_info
print some info about a Vec of programs
recursive_var_mod
This is a helper function for implementing various recursive operations that only modify Var or IVar constructs (use ivars=true to run this on all ivars). Just provide a function that you want to call on each Var to determine what to replace it with. The function signature should be (actual_idx, depth, which_upward_ref, egraph) -> Option<Id>.
replace_prim_with
rewrite_fast
rewrite_with_invention
Rewrite root using an invention inv. This will use inventions everywhere as long as it decreases the cost. It will account for the fact that using an invention in a child could prevent the use of the invention in the parent - it will always do whatever gives the lowest cost.
rewrite_with_invention_egraph
Same as rewrite_with_invention but operates on an egraph instead of an Expr.
rewrite_with_inventions
Same as rewrite_with_invention but for multiple inventions, rewriting with one after another in order, compounding on each other
rewrite_with_inventions_egraph
Same as rewrite_with_invention_egraph but for multiple inventions, rewriting with one after another in order, compounding on each other
save
shift
Does debruijn index shifting of a subtree, incrementing all Vars by the given amount
timestamp
provides a timestamp as a string in a format you can use for file/folder names: YYYY-MM-DD_HH-MM-SS
top_down_inplace
topological_ordering
does a child first traversal of the egraph and returns a Vec in that order. Notably an Id will never show up twice (if it showed up earlier it wont show up again). Assumes no cycles in the EGraph. Note that I’m pretty usre this will just return 0,1,2,3,… since due to structural hashing that is a topological ordering

Type Aliases§

DSLFn
EGraph
Env
env[i] is the value at $i
FlatExplanation
FlatExplanation are the simpler, expanded representation showing one term being rewritten to another. Each step contains a full FlatTerm. Each flat term is connected to the previous by exactly one rewrite.
PatternAst
A RecExpr that represents a Pattern.
RecVarModCache
cache for shift()
TreeExplanation
Explanation trees are the compact representation showing how one term can be rewritten to another.
UnifyResult
VError
VResult
ZId
“zipper id” each unique zipper gets referred to by its zipper id
Zip
a list of znodes, representing a path through a tree (a zipper)