Added various parts of the well typedness checks#82
Added various parts of the well typedness checks#82mlaveaux wants to merge 18 commits intoMERCorg:mainfrom
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.
| let name = format!("Struct{}", name); | ||
|
|
||
| let spec = formatdoc!( | ||
| "sort {name} | ||
|
|
||
| " | ||
| ); | ||
|
|
||
| UntypedDataSpecification::parse(&spec) | ||
| } else { |
There was a problem hiding this comment.
structured_sort_spec generates a sort declaration string without a terminating semicolon (e.g., sort StructX), which is unlikely to be accepted by the mCRL2 parser (other sort decls use sort D;). This will make UntypedDataSpecification::parse(&spec) fail at runtime for structured sorts; include the semicolon and any required body per the expected grammar.
…s not yet very efficient.
…his is not technically unsafe, but could result in use after free.
75fc011 to
419b5f9
Compare
Implemented so far: