Update eggify.jl for 2.0

[jakevossen5]

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 #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 means p.head should probably be p.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 with Metatheory.jl wants to take a crack at it I would appreciate it!

[0x0f0f0f]

It's out of date! Sorry. I should update it. Original author is @philzook58 . Maybe phil could help

[jakevossen5]

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

[0x0f0f0f]

It would be nice to have eggify as a method dispatching on <:AbstractRule types, Vector{<:AbstractRule} and on <:AbstractPat types

[0x0f0f0f]

Needs an update for 2.0