Added various parts of the well typedness checks#82
Open
mlaveaux wants to merge 19 commits into
Open
Conversation
There was a problem hiding this comment.
Pull request overview
This PR introduces an initial merc_typecheck crate that starts implementing well-typedness checks for data specifications (non-emptiness, name resolution, standard/basic sort rules, and alias-cycle detection), and extends the syntax AST/visitors to support resolved sort references and flattened function sorts.
Changes:
- Add
merc_typecheckcrate with name resolution, alias-cycle detection, non-emptiness checking, and standard/basic sort specification helpers. - Extend
merc_syntaxsort AST withDefId,Resolvedsort references, andFlattenedFunction, updating visitors/builders/display accordingly. - Wire the new crate into the workspace and dependents; add small utilities/tests in
merc_collections.
Reviewed changes
Copilot reviewed 18 out of 19 changed files in this pull request and generated 9 comments.
Show a summary per file
| File | Description |
|---|---|
| crates/typecheck/src/standard_sorts.rs | Generates/instantiates standard/basic sort data specs and helper replacements. |
| crates/typecheck/src/non_empty.rs | Adds syntactic non-emptiness checking and a regression test. |
| crates/typecheck/src/name_resolution.rs | Implements initial sort name resolution to DefIds. |
| crates/typecheck/src/lib.rs | Exposes the new typecheck modules. |
| crates/typecheck/src/is_well_typed.rs | Adds well-typedness checks and defines WellTypedError plus tests. |
| crates/typecheck/src/is_finite.rs | Adds a finiteness predicate for sorts. |
| crates/typecheck/src/data_specification.rs | Adds a DataSpecification::from_untyped pipeline (flatten, resolve, cycle-check, well-typed checks). |
| crates/typecheck/src/alias.rs | Adds alias-cycle detection via SCC decomposition plus tests. |
| crates/typecheck/Cargo.toml | Declares the new merc_typecheck crate. |
| crates/syntax/src/visitor.rs | Updates sort-expression visiting APIs and adds traversal support for new sort variants. |
| crates/syntax/src/syntax_tree_display.rs | Adds display for Resolved and FlattenedFunction. |
| crates/syntax/src/syntax_tree.rs | Renames DeclId → DefId and adds Resolved/FlattenedFunction to SortExpression. |
| crates/syntax/src/consume.rs | Minor parsing code style adjustment. |
| crates/syntax/src/builder.rs | Generalizes apply_sort_expression error type and supports new sort variants. |
| crates/sabre/Cargo.toml | Adds dependency on merc_typecheck. |
| crates/collections/src/indexed_set.rs | Adds IndexedSet::get_unchecked. |
| crates/collections/src/block_partition.rs | Updates docs, removes a debug assert in is_empty, and adjusts tests. |
| Cargo.toml | Adds crates/typecheck to workspace members and workspace dependencies. |
| Cargo.lock | Adds the new merc_typecheck package entry and dependency edges. |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
75fc011 to
419b5f9
Compare
…s not yet very efficient.
…his is not technically unsafe, but could result in use after free.
f9d3d39 to
b5e92d1
Compare
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.
Implemented so far: