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

WIP: get rid of module rec and functors by moving many types into types.ml #576

Draft
wants to merge 3 commits into
base: next
Choose a base branch
from

Conversation

lefessan
Copy link
Member

@lefessan lefessan commented Apr 15, 2023

Currently, the code of alt-ergo is hard to enter because it is a huge recursive mess, where all theories are functors with a Sig.SHOSTAK interface and they are all gathered together in the shostak.ml using a big module rec.

This patch is probably not intented to be merged at any point, but it might be interesting as it simplifies the code by removing this use of functors and module rec :

  • Types from symbols.ml, expr.ml and all theories are gathered together in a file types.ml (which makes it easier to understand what they are ...)
  • A shostak_pre.ml file exposes shostak.ml functions before they are available, to allow a huge recursion between modules. It exposes a set of refs, which are set from the shostak.ml file at the end.
  • Most of the changes are replacements of scopes changes to use Types instead of Symbols or Expr.

@lefessan lefessan marked this pull request as draft April 17, 2023 11:40
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.

1 participant