Open jakevossen5 opened 2 years ago
It's out of date! Sorry. I should update it. Original author is @philzook58 . Maybe phil could help
No worries! I made some changes and it is working for my use case right now, though it should probably be put through some more intense examples.
I will paste the script here, if you think it looks pretty good then let me know and I can make a PR (and maybe try to add it to a test suite so this doesn't happen again). It has some limitations, like no multi-line scripts, but seems to do the same thing as the original script did.
using Metatheory
using Metatheory: cleanast
using Metatheory.EGraphs
using Metatheory.Library
to_sexpr_pattern(p::PatVar) = "?$(p.name)"
function to_sexpr_pattern(p::PatTerm)
e1 = join([p.operation ; to_sexpr_pattern.(p.args)], ' ')
"($e1)"
end
to_sexpr_pattern(e::Symbol) = e
to_sexpr_pattern(e::Int64) = e
to_sexpr_pattern(e::Expr) = "($(join(to_sexpr_pattern.(e.args),' ')))"
function eggify(rules)
egg_rules = []
for rule in rules
l = to_sexpr_pattern(rule.left)
r = to_sexpr_pattern(rule.right)
if rule isa SymbolicRule
push!(egg_rules,"\tvec![rw!( \"$(rule.left) => $(rule.right)\" ; \"$l\" => \"$r\" )]")
elseif rule isa EqualityRule
push!(egg_rules,"\trw!( \"$(rule.left) == $(rule.right)\" ; \"$l\" <=> \"$r\" )")
else
println("Unsupported Rewrite Mode")
@assert false
end
end
return join(egg_rules, ",\n")
end
function rust_code(theory, query, params=SaturationParams())
"""
use egg::{*, rewrite as rw};
fn main() {
let rules : &[Rewrite<SymbolLang, ()>] = &vec![
$(eggify(theory))
].concat();
let start = "$(to_sexpr_pattern(cleanast(query)))".parse().unwrap();
let runner = Runner::default().with_expr(&start)
// More options here https://docs.rs/egg/0.6.0/egg/struct.Runner.html
.with_iter_limit($(params.timeout))
.with_node_limit($(params.enodelimit))
.run(rules);
runner.print_report();
let extractor = Extractor::new(&runner.egraph, AstSize);
let (best_cost, best_expr) = extractor.find_best(runner.roots[0]);
println!("best cost: {}, best expr {}", best_cost, best_expr);
}
"""
end
It would be nice to have eggify
as a method dispatching on <:AbstractRule
types, Vector{<:AbstractRule}
and on <:AbstractPat
types
Needs an update for 2.0
I have been trying to run
eggify.jl
found here but have been running into some issues, as it looks like some things have been renamed, mostly from https://github.com/JuliaSymbolics/Metatheory.jl/pull/77.First time I ran I got the error
LoadError: UndefVarError: PatLiteral not defined
If I delete that, I get
LoadError: type PatTerm has no field head
. So that meansp.head
should probably bep.operation
? Not sure. I am going to mess around with it a bit to see if I can get something to work, but if someone more familiar withMetatheory.jl
wants to take a crack at it I would appreciate it!