Skip to content

Conversation

@nskh
Copy link
Collaborator

@nskh nskh commented Aug 19, 2025

Allows us to rewrite-check things like f(x) + 1 being equivalent to 1 + f(x); all we have to do is unpack function application. Even works when f, x have not been defined:
image

Closes #1842.

@nskh nskh requested review from Negabinary and Copilot August 19, 2025 18:11
Copy link
Contributor

Copilot AI left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Pull Request Overview

This PR enhances the rewrite checker to handle function application expressions, enabling equivalence checking for expressions like f(x) + 1 and 1 + f(x). The change allows the system to unpack and properly represent function applications even when the function and arguments are undefined.

  • Adds support for function application (Ap) pattern matching in the algebrite expression printer
  • Improves debugging output for unknown expression types with detailed logging
  • Updates a TODO comment attribution

Tip: Customize your code reviews with copilot-instructions.md. Create the file or learn how to get started.

print_endline(
"Algebrite rewrite checker received unknown value of type "
++ Exp.show(exp),
);
Copy link

Copilot AI Aug 19, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Adding debug output via print_endline in production code can clutter console output and may not be appropriate for all environments. Consider using a proper logging mechanism or making this conditional based on a debug flag.

Suggested change
);
if (debug) {
print_endline(
"Algebrite rewrite checker received unknown value of type "
++ Exp.show(exp),
);
};

Copilot uses AI. Check for mistakes.
@codecov
Copy link

codecov bot commented Aug 19, 2025

Codecov Report

❌ Patch coverage is 0% with 22 lines in your changes missing coverage. Please review.
✅ Project coverage is 50.68%. Comparing base (3636f8c) to head (c135936).

Files with missing lines Patch % Lines
src/web/app/editors/stepper/RewriteChecker.re 0.00% 22 Missing ⚠️
Additional details and impacted files
@@            Coverage Diff             @@
##              dev    #1877      +/-   ##
==========================================
- Coverage   50.79%   50.68%   -0.11%     
==========================================
  Files         204      204              
  Lines       21355    21376      +21     
==========================================
- Hits        10847    10835      -12     
- Misses      10508    10541      +33     
Files with missing lines Coverage Δ
src/web/app/editors/stepper/RewriteChecker.re 0.00% <0.00%> (ø)

... and 13 files with indirect coverage changes

🚀 New features to boost your workflow:
  • ❄️ Test Analytics: Detect flaky tests, report on failures, and find test suite problems.
  • 📦 JS Bundle Analysis: Save yourself from yourself by tracking and limiting bundle sizes in JS merges.

@Negabinary
Copy link
Contributor

Had a play with it; these are some examples I'd prefer if they gave the opposite answer

image image image image

@nskh
Copy link
Collaborator Author

nskh commented Sep 23, 2025

Fixed length (builtins) and list concat handling. Still working on the function stuff, we may need to chat about how to handle those generally.

@nskh nskh force-pushed the function-handling-in-algebrite branch from 9712ed2 to c135936 Compare September 23, 2025 00:22
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

Algebrite should treat arbitrary equal expressions as equal

3 participants