Closed keltono closed 11 months ago
Apologies for the slow work, I started the PR right before midterms began (my mistake!), but I (believe I) have addressed all of the issues except for not emitting color codes by default for log files, which I will finish by the end of the day. Let me know if there's anything else.
I think everything is ready to go for merging!
This is the culmination of the work I mostly did 2 summers ago and have been finishing up since when I could. The code is (I would say) well commented, and is mostly contained within
src/edu.umn.cs.melt.copper.compiletime/src/main/java/edu/umn/cs/melt/copper/compiletime/auxiliary/counterexample
. The way that the code is organized and the scope of the project made this feel like a reasonable way to do things --- if need be the code could be messaged into a builder/checker/dumper, but this doesn't feel like the correct abstraction.After some time I decided to restrict the scope of the algorithm to only produce non-unified counterexamples, i.e examples that may not have the exact same tokens. Getting this always is (of course) undecidable in general, and the algorithm presented in the literature is massively complex slow, and very brittle to changes. I think it would be essentially unmaintainable without significant reworking of the core algorithm.
Let me know if they're any questions or concerns with anything. I've added Lucas and August as reviewers, let me know if I should do something else or if the review/merge process should be done in a particular way. CC @ericvanwyk @krame505 @schwerdf .