Crate stitch_core
source ·Modules
Macros
A macro to easily create a
Language.this macros defines two lazy static variables PRIMS and FUNCS
this macro is used at the start of a DSL function to load arguments out of their args vec
this macro is used at the start of a DSL function to load arguments out of their args vec
Make a test function
Structs
an argument to an abstraction.
id is the main field here, we can use
it to lookup the corresponding tree using egraph[id]A simple
CostFunction that counts maximum ast depth.A simple
CostFunction that counts total ast size.A
RewriteScheduler that implements exponentional rule backoff.Bottom-up synthesis
Args for compression step
the complete result of a single step of compression, this is a somewhat expensive data structure
to create.
A
Condition that checks if two terms are equivalent.This is the multithread data locked during the critical section of the algorithm.
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).
The analysis data associated with each Lambda node
Result of
Analysis::merge indicating which of the inputs
are different from the merged result.An equivalence class of enodes.
A data structure to keep track of equalities between expressions.
A data structure representing an explanation that two terms are equivalent.
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 finished invention
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.The heap item used for heap-based worklists. Holds a pattern
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.the cost of a program, where
app and lam cost 1, programs costs nothing,
ivar and var and prim cost 100.depth of a program. For example a leaf is depth 1.
A rewrite that searches for the lefthand side and applies the righthand side.
The result of searching a
Searcher over one eclass.All the data shared among threads, mostly read-only
except for the mutexes
A very simple
RewriteScheduler that runs every rewrite every
time.Various tracking stats
An interned string.
A simple language used for testing.
Top-down synthesis
Used for debugging tracking information
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.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
The language of
Patterns.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.
a strategy for choosing which hole to expand next in a partial pattern
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.An error type for failures when attempting to parse an s-expression as a
RecExpr<L>.Error returned by
Runner when it stops.int
[Term(“int”,None)]
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
A node in an ZPath
Ord: Func < Body < Arg
Constants
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.
Traits
Support
&str and String, you can use "text".red() and s.red() for s:StringA condition to check in a
ConditionalApplier.A cost function that can be used by an
Extractor.The key trait that defines a domain
A trait for parsing e-nodes. This is implemented automatically by
define_language!.A marker that defines acceptable children types for
define_language!.Functions
convenience function for equality assertions
convenience function for asserting that something executes to what you’d expect
Multistep compression. See
compression_step if you’d just like to do a single step of compression.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
same as Itertools::counts() but returns an FxHashMap instead of a HashMap
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.
like extract() but works on nodes
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.
replaces upward refs to 0 with negative ivar
Replace the ivars in an expr based on an i32->Expr map
Replace the ivars in an expr based on an i32->Expr map
A utility for implementing
Analysis::merge
when the Data type has a total ordering.
This will take the maximum of the two values.A utility for implementing
Analysis::merge
when the Data type has a total ordering.
This will take the minimum of the two values.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
convenience function for returning arguments from a DSL function
print some info about a Vec of programs
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.Same as
rewrite_with_invention but operates on an egraph instead of an Expr.Same as
rewrite_with_invention but for multiple inventions, rewriting with one after another in order, compounding on each otherSame as
rewrite_with_invention_egraph but for multiple inventions, rewriting with one after another in order, compounding on each otherDoes debruijn index shifting of a subtree, incrementing all Vars by the given amount
provides a timestamp as a string in a format you can use for file/folder names: YYYY-MM-DD_HH-MM-SS
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 Definitions
env[i] is the value at $i
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.cache for shift()
Explanation trees are the compact representation showing
how one term can be rewritten to another.
“zipper id” each unique zipper gets referred to by its zipper id
a list of znodes, representing a path through a tree (a zipper)