Made type checking fully polymorphic - #134
Open
mlaveaux wants to merge 19 commits into
Open
Conversation
* Will be used to tell polymorphic type variables apart from ordinary sort references.
…sistent, avoids scopes in several later passes.
mlaveaux
commented
Sep 8, 2026
| //! Rewrites every sort-position [`SortExpressionKind::Reference`] naming one of a | ||
| //! specification's own `type_var` declarations into a [`SortExpressionKind::TypeVar`]. | ||
| //! | ||
| //! This runs as part of parsing (see the `type_var`-handling call sites in `consume.rs`), before |
Collaborator
Author
There was a problem hiding this comment.
Clean up these comments
mlaveaux
commented
Sep 8, 2026
| /// aliases, constructor, map and equation-variable sorts, and binder sorts inside equation bodies | ||
| /// (a quantifier, lambda, or set/bag comprehension). A no-op when the spec declares no type | ||
| /// variables. | ||
| pub(crate) fn bind_type_vars(spec: &mut UntypedDataSpecification) { |
Collaborator
Author
There was a problem hiding this comment.
This might be called resolve in other places, make it consistent
mlaveaux
commented
Sep 8, 2026
| fn with_binder_scope<T>( | ||
| &mut self, | ||
| variables: &'a [IdDecl], | ||
| f: impl FnOnce(&mut Self, &[ResolvedSortId]) -> Result<T, GenFailure>, |
Collaborator
Author
There was a problem hiding this comment.
Remove this inline impl
mlaveaux
commented
Sep 8, 2026
| /// the shadowing done inline for a comprehension's single bound variable. | ||
| /// Used by `lambda` and `forall`/`exists`, which declare their variables' | ||
| /// sorts, unlike a `whr` binding whose sort follows from its right-hand side. | ||
| /// binder sort, see [Self::binder_sort]) and registers it in `self.declared_sorts`, by each |
Collaborator
Author
There was a problem hiding this comment.
This comment seems weird, what scope, we just have resolved all
mlaveaux
commented
Sep 8, 2026
| // variables per occurrence, mirroring mCRL2's polymorphic symbol | ||
| // table; Phase-4 lowering recovers the concrete operation from the | ||
| // name and the inferred sort. | ||
| for scheme in self.builtin_schemes.clone().get(name).into_iter().flatten() { |
mlaveaux
commented
Sep 8, 2026
| /// Instantiates the leaves of a `Product` domain spine in declaration | ||
| /// order, the template counterpart of `resolve_function_domain`. | ||
| fn template_domain( | ||
| /// A fresh instance of a scheme's already-*interned* sort: every bound |
mlaveaux
commented
Sep 8, 2026
| /// comment), parenthesized when it is itself an arrow (matching how a `map`/`cons` declaration's | ||
| /// own function sort is parenthesized in this same file's header). | ||
| /// | ||
| /// `cursor` walks `typing.sorts`/`typing.spans` (both `ExprId`-indexed) one entry per recursive |
Collaborator
Author
There was a problem hiding this comment.
This seems to be some weird dependency
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Previously there were all kinds of special cases for polymorphic containers. This branch focusses on introducing proper syntax (now called type_var) for the type variables.
Also added source_map and import statements, these are also used to include the system defined and generated sorts, such that errors can be reported on them.
The next step is to clean up all special cases in type inference.