improved naive unification

[kevinyeeeee]

Improved naive unification, which now allows for arbitrary variable names in target code

• functions now use holes for local variables
• lhs now called pat, and added PHole constructor for pats
• For statements now take in a pat as an index

unify now threads substitutions made so far through the program, checking that holes with the same name are matched to the same exprs each time.

This means solver now works for many target programs, and we are now even able to synthesize sum(mul(x,y)!

[justinlubin]

This is brilliant, thank you so much! I look through all the files and I have no improvements to suggest!

Could you resolve the git` conflicts with the main branch? (i.e., merge the main branch into your branch, then resolve the conflicts, then push the commit to your branch.) Then I'll merge in this pull request and we'll be good to go! Thank you again!