Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Atomics, improve lisa.fol.FOL's logic and simplify it #194

Merged
merged 20 commits into from
Dec 2, 2023

Conversation

SimonGuilloud
Copy link
Collaborator

The PR does a few things:

  • Rename old and poor traits and classes in the kernel's FOL and front's FOL, following the realization the the word I was looking for is exactly "Atomics". For example, "SchematicVarOrPredLabel" --> "SchematicAtomicLabel". This does not change any functionality.
  • Fixed the logic in the front's FOL. Labels were contravariant in their type parameters when they should not be; This was necessary for fixing some classes extending labels twice, itself following some other workarround. This as all been fixed. Moreover, apply paterns on Variables, Constants, Terms and Formulas should be much cleaner and logical. The cost was to carry a little bit more type parameters, but it's well worth it.
  • Removed the match type for T *** N, which was used to obtain function application with arbitrary but fixed number of parameters given by N. Instead, T**N is now always a sequence at runtime, hidden behind an opaque type. Function application with N arguments is obtained through extension methods (one for each N, not one for each implementation of (T ** N) |-> S). That's a bit less general, but more flexible and possibly more efficient.
  • Generally refactored the Common.scala file, ensuring uniformity across definitions. Uses less top-notch, scala-specific features and should be a bit more stable and easier to understand.

Copy link
Member

@sankalpgambhir sankalpgambhir left a comment

Choose a reason for hiding this comment

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

Looks good.

Just out of curiosity, do you notice a significant change in compile times with a move to hard coded arities over the previous generic framework?

@SimonGuilloud SimonGuilloud merged commit 7005950 into epfl-lara:main Dec 2, 2023
1 check passed
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.

2 participants