Implemented an experimental type checker - #122
Open
mlaveaux wants to merge 94 commits into
Open
Conversation
…yields all non empty sorts
…and rejecting conflicting ones; add tests for new behavior.
…y becomes &&(x, y).
…he untyped data specification
MatchGoal::partition previously handed back each partition's announcement positions, and derive_transition used those to decide whether a freshly discovered subtree position should merge into an existing partition. pos_comparable treats an empty position as comparable to anything, and root-anchored goals have an empty announcement position, so any partition containing one absorbed every subsequent fresh subtree without bound and the automaton construction never reached a fixpoint. Goals reaching this code are always unchanged/reduced (never completed), so their obligations are never empty even when the announcement position is. Deriving the merge-candidate positions from each partition's remaining obligations instead of its announcement positions keeps merging tied to genuinely overlapping work and restores termination.
- Introduced `SystemEquationGroup` to encapsulate generated content and its equation range. - Modified `build_system_defined_specification` and `extend_system_with_inferred_sorts` to return both the merged specification and the associated `SystemEquationGroup`s. - Enhanced `resolve_system_signature_full` to resolve declarations by groups, ensuring proper handling of constructors and mappings. - Updated `validate_system_binder_sorts` to recursively resolve sorts for binder variables in equations. - Added tests to verify the correctness of signature resolution and ensure that equations are validated against their respective binder sorts.
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
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.
This is a continuation of the previous type checker that only performed some minor well typedness checks. These have been extended, and additional passes for the type checking using unification and lowering to aterms have been implemented.