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