From b5e92420ed7df63d910d792832d498e06d40c78b Mon Sep 17 00:00:00 2001 From: Maurice Laveaux Date: Wed, 11 Mar 2026 18:51:04 +0100 Subject: [PATCH 01/18] Started a crate for typechecking --- Cargo.lock | 10 ++++++++++ Cargo.toml | 1 + crates/sabre/Cargo.toml | 1 + crates/typecheck/Cargo.toml | 15 +++++++++++++++ 4 files changed, 27 insertions(+) create mode 100644 crates/typecheck/Cargo.toml diff --git a/Cargo.lock b/Cargo.lock index df83e7441..348e098c8 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -1285,6 +1285,7 @@ dependencies = [ "merc_aterm", "merc_data", "merc_syntax", + "merc_typecheck", "merc_utilities", "rand", "rustc-hash 2.1.2", @@ -1358,6 +1359,15 @@ dependencies = [ "winapi", ] +[[package]] +name = "merc_typecheck" +version = "1.0.0" +dependencies = [ + "indoc", + "merc_syntax", + "merc_utilities", +] + [[package]] name = "merc_unsafety" version = "2.0.0" diff --git a/Cargo.toml b/Cargo.toml index a4d8efbeb..2ed21ebc4 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -40,6 +40,7 @@ members = [ "crates/symbolic", "crates/syntax", "crates/tools", + "crates/typecheck", "crates/unsafety", "crates/utilities", "crates/vpg", diff --git a/crates/sabre/Cargo.toml b/crates/sabre/Cargo.toml index 3b9746c46..dada16e0d 100644 --- a/crates/sabre/Cargo.toml +++ b/crates/sabre/Cargo.toml @@ -16,6 +16,7 @@ version.workspace = true merc_aterm.workspace = true merc_data.workspace = true merc_syntax.workspace = true +merc_typecheck.workspace = true merc_utilities.workspace = true rustc-hash.workspace = true diff --git a/crates/typecheck/Cargo.toml b/crates/typecheck/Cargo.toml new file mode 100644 index 000000000..d55e4739a --- /dev/null +++ b/crates/typecheck/Cargo.toml @@ -0,0 +1,15 @@ +[package] +name = "merc_typecheck" + +edition.workspace = true +homepage.workspace = true +license.workspace = true +repository.workspace = true +rust-version.workspace = true +version.workspace = true + +[dependencies] +indoc.workspace = true + +merc_syntax.workspace = true +merc_utilities.workspace = true \ No newline at end of file From 9523a17262a8f3c6f2f1bdc5d9110a65b47f3b4a Mon Sep 17 00:00:00 2001 From: Maurice Laveaux Date: Wed, 11 Mar 2026 18:53:53 +0100 Subject: [PATCH 02/18] Smaller changes --- crates/syntax/src/builder.rs | 2 ++ crates/syntax/src/syntax_tree.rs | 8 ++++---- 2 files changed, 6 insertions(+), 4 deletions(-) diff --git a/crates/syntax/src/builder.rs b/crates/syntax/src/builder.rs index 33feb9dc7..770f8ee9d 100644 --- a/crates/syntax/src/builder.rs +++ b/crates/syntax/src/builder.rs @@ -17,6 +17,7 @@ where apply_statefrm_rec(formula, &mut function) } +///// Applies the given function recursively to the sort expression. pub fn apply_sort_expression(sort_expr: SortExpression, mut function: F) -> Result where F: FnMut(&SortExpression) -> Result, MercError>, @@ -164,6 +165,7 @@ where } } +/// See [`apply_sort_expression`]. fn apply_sort_expression_rec(sort_expr: SortExpression, apply: &mut F) -> Result where F: FnMut(&SortExpression) -> Result, MercError>, diff --git a/crates/syntax/src/syntax_tree.rs b/crates/syntax/src/syntax_tree.rs index b2cae02f8..ccc1098c0 100644 --- a/crates/syntax/src/syntax_tree.rs +++ b/crates/syntax/src/syntax_tree.rs @@ -3,10 +3,10 @@ use std::hash::Hash; use merc_utilities::TagIndex; /// A unique type for declarations. -pub struct DeclTag; +pub struct DefTag; /// The index type for a label. -pub type DeclId = TagIndex; +pub type DefId = TagIndex; /// A complete mCRL2 process specification. #[derive(Debug, Default, Eq, PartialEq, Hash)] @@ -106,7 +106,7 @@ pub struct IdDecl { /// Source location information pub span: Span, /// Unique ID assigned to this declaration during name resolution. - pub id: Option, + pub id: Option, } impl IdDecl { @@ -183,7 +183,7 @@ pub struct SortDecl { /// Where the sort is defined pub span: Span, /// Unique ID assigned to this declaration during name resolution. - pub id: Option, + pub id: Option, } impl SortDecl { From 03f892f22587a78f38f6012beebce263dd62deda Mon Sep 17 00:00:00 2001 From: Maurice Laveaux Date: Thu, 12 Mar 2026 20:35:44 +0100 Subject: [PATCH 03/18] Added FlattenedFunction to simply further analysis --- crates/syntax/src/builder.rs | 13 ++++++++++++- crates/syntax/src/syntax_tree.rs | 7 +++++++ crates/syntax/src/syntax_tree_display.rs | 7 ++++++- crates/syntax/src/visitor.rs | 9 ++++++++- 4 files changed, 33 insertions(+), 3 deletions(-) diff --git a/crates/syntax/src/builder.rs b/crates/syntax/src/builder.rs index 770f8ee9d..2f7852074 100644 --- a/crates/syntax/src/builder.rs +++ b/crates/syntax/src/builder.rs @@ -205,7 +205,18 @@ where let inner = apply_sort_expression_rec(*sort_expression, apply)?; Ok(SortExpression::Complex(complex_sort, Box::new(inner))) } - SortExpression::Reference(_) | SortExpression::Simple(_) => { + SortExpression::FlattenedFunction { domain, range } => { + let domain = domain + .into_iter() + .map(|sort| apply_sort_expression_rec(sort, apply)) + .collect::, _>>()?; + let range = apply_sort_expression_rec(*range, apply)?; + Ok(SortExpression::FlattenedFunction { + domain, + range: Box::new(range), + }) + } + SortExpression::Reference(_) | SortExpression::Simple(_) | SortExpression::Resolved(_, _) => { // Ignored Ok(sort_expr) } diff --git a/crates/syntax/src/syntax_tree.rs b/crates/syntax/src/syntax_tree.rs index ccc1098c0..e3dc5f86b 100644 --- a/crates/syntax/src/syntax_tree.rs +++ b/crates/syntax/src/syntax_tree.rs @@ -143,6 +143,13 @@ pub enum SortExpression { Simple(Sort), /// Parameterized complex sort Complex(ComplexSort, Box), + /// Resolved reference to a sort after name resolution + Resolved(String, DefId), + /// Function sort (A_0 # ... # A_n -> B) after flattening (performed during name resolution) + FlattenedFunction { + domain: Vec, + range: Box, + }, } /// Constructor declaration diff --git a/crates/syntax/src/syntax_tree_display.rs b/crates/syntax/src/syntax_tree_display.rs index 5ec503760..2c96a26a7 100644 --- a/crates/syntax/src/syntax_tree_display.rs +++ b/crates/syntax/src/syntax_tree_display.rs @@ -340,13 +340,18 @@ impl fmt::Display for SortExpression { match self { SortExpression::Product { lhs, rhs } => write!(f, "({lhs} # {rhs})"), SortExpression::Function { domain, range } => write!(f, "({domain} -> {range})"), - SortExpression::Reference(ident) => write!(f, "{ident}"), + SortExpression::Reference(name) => write!(f, "{name}"), SortExpression::Simple(sort) => write!(f, "{sort}"), SortExpression::Complex(complex, inner) => write!(f, "{complex}({inner})"), SortExpression::Struct { inner } => { write!(f, "struct ")?; write!(f, "{}", inner.iter().format(" | ")) } + SortExpression::Resolved(name, _id) => write!(f, "{name}"), + SortExpression::FlattenedFunction { domain, range } => { + let domain = domain.iter().format(" # "); + write!(f, "({domain} -> {range})") + } } } } diff --git a/crates/syntax/src/visitor.rs b/crates/syntax/src/visitor.rs index f8f1d7ace..16fceca93 100644 --- a/crates/syntax/src/visitor.rs +++ b/crates/syntax/src/visitor.rs @@ -75,6 +75,7 @@ where Ok(None) } +/// See [`visit_sort_expr`]. fn visit_sort_expr_rec(sort_expr: &SortExpression, function: &mut F) -> Result, MercError> where F: FnMut(&SortExpression) -> Result, MercError>, @@ -103,7 +104,13 @@ where SortExpression::Complex(_complex_sort, sort_expression) => { visit_sort_expr_rec(sort_expression, function)?; } - SortExpression::Reference(_) | SortExpression::Simple(_) => {} + SortExpression::FlattenedFunction { domain, range } => { + for domain_sort in domain { + visit_sort_expr_rec(domain_sort, function)?; + } + visit_sort_expr_rec(range, function)?; + } + SortExpression::Reference(_) | SortExpression::Simple(_) | SortExpression::Resolved(_, _)=> {} } // The visitor did not break the traversal. From 0fcc187e84b4ebc7091398e2ca49269421497647 Mon Sep 17 00:00:00 2001 From: Maurice Laveaux Date: Sat, 14 Mar 2026 12:00:50 +0100 Subject: [PATCH 04/18] Implemented name resolution for sorts --- crates/typecheck/src/name_resolution.rs | 75 +++++++++++++++++++++++++ 1 file changed, 75 insertions(+) create mode 100644 crates/typecheck/src/name_resolution.rs diff --git a/crates/typecheck/src/name_resolution.rs b/crates/typecheck/src/name_resolution.rs new file mode 100644 index 000000000..a4d1941f5 --- /dev/null +++ b/crates/typecheck/src/name_resolution.rs @@ -0,0 +1,75 @@ +use merc_collections::IndexedSet; +use merc_syntax::DefId; +use merc_syntax::SortExpression; +use merc_syntax::UntypedDataSpecification; +use merc_syntax::apply_sort_expression; + +use crate::WellTypedError; + +/// Ensure that all DefIds in the data specification are resolved. Returns an +/// indexed set that indicates the mapping from sort identifiers to their +/// DefIds. +pub fn resolve_names(spec: &mut UntypedDataSpecification) -> Result, WellTypedError> { + // Every sort declaration should have a unique name. + let mut sorts = IndexedSet::new(); + + // Assign unique IDs to all sort declarations + for (i, sort) in spec.sort_declarations.iter_mut().enumerate() { + sort.id = Some(DefId::new(i)); + + if !sorts.insert(sort.identifier.clone()).1 { + return Err(WellTypedError::DuplicateSortDeclaration { + sort: sort.identifier.clone(), + }); + } + } + + // Resolve all sorts. + map_sorts_in_spec(spec, |sort| resolve_sort_id(sort, &sorts))?; + + Ok(sorts) +} + +// Apply a mapping function to every sort in the specification. +pub fn map_sorts_in_spec(spec: &mut UntypedDataSpecification, mut f: F) -> Result<(), E> +where + F: FnMut(&SortExpression) -> Result, +{ + for sort in &mut spec.sort_declarations { + if let Some(expr) = &sort.expr { + // Only apply to type aliases. + sort.expr = Some(f(expr)?); + } + } + + for constructor in &mut spec.constructor_declarations { + constructor.sort = f(&constructor.sort)?; + } + + for map in &mut spec.map_declarations { + map.sort = f(&map.sort)?; + } + + for equation in &mut spec.equation_declarations { + for var in &mut equation.variables { + var.sort = f(&var.sort)?; + } + } + + Ok(()) +} + +/// Replaces sort references of `identifier` in `sort` by the given `result_sort`. +fn resolve_sort_id(sort: &SortExpression, resolved: &IndexedSet) -> Result { + apply_sort_expression(sort.clone(), |expr| { + if let SortExpression::Reference(name) = expr { + if let Some(id) = resolved.index(name) { + return Ok(Some(SortExpression::Resolved(name.clone(), DefId::new(*id)))); + } + + return Err(WellTypedError::UndefinedSort { sort: name.clone() }); + } + + Ok(None) + }) +} \ No newline at end of file From be5c3ec16cead4554162a796d9194e4246a22235 Mon Sep 17 00:00:00 2001 From: Maurice Laveaux Date: Sat, 14 Mar 2026 12:01:14 +0100 Subject: [PATCH 05/18] Generalised apply_sort_expression to return any error type --- crates/syntax/src/builder.rs | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/crates/syntax/src/builder.rs b/crates/syntax/src/builder.rs index 2f7852074..1c17d8501 100644 --- a/crates/syntax/src/builder.rs +++ b/crates/syntax/src/builder.rs @@ -18,9 +18,9 @@ where } ///// Applies the given function recursively to the sort expression. -pub fn apply_sort_expression(sort_expr: SortExpression, mut function: F) -> Result +pub fn apply_sort_expression(sort_expr: SortExpression, mut function: F) -> Result where - F: FnMut(&SortExpression) -> Result, MercError>, + F: FnMut(&SortExpression) -> Result, E>, { apply_sort_expression_rec(sort_expr, &mut function) } @@ -166,9 +166,9 @@ where } /// See [`apply_sort_expression`]. -fn apply_sort_expression_rec(sort_expr: SortExpression, apply: &mut F) -> Result +fn apply_sort_expression_rec(sort_expr: SortExpression, apply: &mut F) -> Result where - F: FnMut(&SortExpression) -> Result, MercError>, + F: FnMut(&SortExpression) -> Result, E>, { if let Some(sort_expr) = apply(&sort_expr)? { // A substitution was made, return the new sort expression. From 3c82b92b0dd5c2ed72cfe59aa9a96fb6727a688f Mon Sep 17 00:00:00 2001 From: Maurice Laveaux Date: Sat, 14 Mar 2026 12:01:47 +0100 Subject: [PATCH 06/18] Moved the DataSpecification to this crate, and added a few well_typed checks. --- crates/typecheck/src/data_specification.rs | 98 ++++++++++++++++++++++ 1 file changed, 98 insertions(+) create mode 100644 crates/typecheck/src/data_specification.rs diff --git a/crates/typecheck/src/data_specification.rs b/crates/typecheck/src/data_specification.rs new file mode 100644 index 000000000..05b91ade5 --- /dev/null +++ b/crates/typecheck/src/data_specification.rs @@ -0,0 +1,98 @@ +use std::collections::HashMap; +use std::convert::Infallible; + +use merc_syntax::DefId; +use merc_syntax::EqnSpec; +use merc_syntax::IdDecl; +use merc_syntax::SortExpression; +use merc_syntax::UntypedDataSpecification; +use merc_syntax::apply_sort_expression; + +use crate::WellTypedError; +use crate::basic_sort_data_specification; +use crate::is_well_typed; +use crate::map_sorts_in_spec; +use crate::resolve_names; + +/// A type checked and well-typed data specification. +pub struct DataSpecification { + pub sort_declarations: HashMap, Vec)>, +} + +impl DataSpecification { + /// Create a completed well-typed data specification from an untyped data specification. + pub fn from_untyped(mut spec: UntypedDataSpecification) -> Result { + map_sorts_in_spec(&mut spec, |sort| -> Result<_, Infallible> { + Ok(flatten_function_sorts(sort)) + }) + .expect("The inner function never fails"); + + let _sorts = resolve_names(&mut spec)?; + + is_well_typed(&spec)?; + + // Obtain the definitions for all basic sort. + let _basic_sort_spec = basic_sort_data_specification().map_err(|e| WellTypedError::Custom(e))?; + + // Add all the occurring standard sorts to the specification. + + Ok(Self { + sort_declarations: HashMap::new(), // TODO: Fill this in with the actual sort declarations. + }) + } +} + +/// Returns the target sort of a sort expression, i.e. the range of a function +/// sort, or the sort itself if it is not a function sort. +pub fn target_sort(sort: &SortExpression) -> &SortExpression { + debug_assert!( + !matches!(sort, SortExpression::Function { .. }), + "target_sort should only be called on non-function sorts or flattened function sorts" + ); + + if let SortExpression::FlattenedFunction { domain: _, range } = sort { + range + } else { + sort + } +} + +/// Returns the arguments of a function sort, requires that function sorts are flattened. +pub fn argument_sorts(sort: &SortExpression) -> &Vec { + if let SortExpression::FlattenedFunction { domain, range: _ } = sort { + domain + } else { + unreachable!("argument_sorts should only be called on function sorts") + } +} + +/// Replaces sort references of `identifier` in `sort` by the given `result_sort`. +fn flatten_function_sorts(sort: &SortExpression) -> SortExpression { + apply_sort_expression(sort.clone(), |expr| -> Result<_, Infallible>{ + if let SortExpression::Function { domain, range } = expr { + let mut flattened_domain = Vec::new(); + flatten_function_domain_rec(domain, &mut flattened_domain); + + return Ok(Some(SortExpression::FlattenedFunction { + domain: flattened_domain, + range: range.clone(), + })); + } + + Ok(None) + }) + .expect("flatten_function_sorts should not fail") +} + +/// Flattens a function sort of the form ((A_0 # A_1) # ... # A_n) -> B into a +/// sort of the form A_0 # A_1 # ... # A_n -> B, where B is the original range +/// of the function. +fn flatten_function_domain_rec(sort: &SortExpression, domain: &mut Vec) { + match sort { + SortExpression::Product { lhs, rhs } => { + flatten_function_domain_rec(lhs, domain); + flatten_function_domain_rec(rhs, domain); + } + _ => domain.push(sort.clone()), + } +} From 3840025bae8d380e71945e7722a6a484b86335b0 Mon Sep 17 00:00:00 2001 From: Maurice Laveaux Date: Sat, 14 Mar 2026 12:02:21 +0100 Subject: [PATCH 07/18] Added the check for whether a sort is syntactically non-empty. This is not yet very efficient. --- crates/typecheck/src/non_empty.rs | 83 +++++++++++++++++++++++++++++++ 1 file changed, 83 insertions(+) create mode 100644 crates/typecheck/src/non_empty.rs diff --git a/crates/typecheck/src/non_empty.rs b/crates/typecheck/src/non_empty.rs new file mode 100644 index 000000000..8cce89944 --- /dev/null +++ b/crates/typecheck/src/non_empty.rs @@ -0,0 +1,83 @@ +use std::collections::HashSet; + +use merc_syntax::DefId; +use merc_syntax::IdDecl; +use merc_syntax::SortExpression; +use merc_syntax::UntypedDataSpecification; + +use crate::argument_sorts; +use crate::target_sort; + +/// Returns true iff the sort is syntactically non-empty, i.e., there is at +/// least one constructor for the target sort that has a non-empty sort. +pub fn is_nonempty_sort(sort: &str, spec: &UntypedDataSpecification) -> bool { + debug_assert!( + spec.sort_declarations.iter().any(|id| id.id.is_some()), + "The sorts must be resolved" + ); + + let sort_id = spec + .sort_declarations + .iter() + .find(|id| id.identifier == sort) + .expect("The sort should be declared") + .id + .unwrap(); + + let mut seen = HashSet::new(); + is_nonempty_sort_rec(sort_id, &spec.constructor_declarations, &mut seen) +} + +/// The recursive definition of non-emptiness. +fn is_nonempty_sort_rec(sort: DefId, constructors: &Vec, seen: &mut HashSet) -> bool { + if seen.contains(&sort) { + return false; // We have already seen this sort, so we have a cycle. + } + + for constructor in constructors.iter().filter(|id| { + if let SortExpression::Resolved(_, id) = target_sort(&id.sort) { + *id == sort + } else { + unreachable!("The target sort of a constructor should always be a reference sort, but is not for {:?}", id.sort) + } + }) { + if argument_sorts(&constructor.sort).is_empty() { + return true; // We have found a constructor with no arguments, so the sort is non-empty. + } + + seen.insert(sort); // Mark the current sort as seen to avoid cycles. + + if argument_sorts(&constructor.sort).iter().all(|_arg| true) { + return true; // All argument sorts are non-empty, so the sort is non-empty. + } + + seen.remove(&sort); // Unmark the current sort as seen to allow other paths to explore it. + } + + true +} + +#[cfg(test)] +mod tests { + use merc_syntax::UntypedDataSpecification; + + use crate::DataSpecification; + use crate::WellTypedError; + + #[test] + fn test_empty_data_spec() { + let spec = UntypedDataSpecification::parse( + " + sort D; + cons f: D -> D; + ", + ) + .unwrap(); + + match DataSpecification::from_untyped(spec) { + Err(WellTypedError::EmptySort { sort }) if sort == "D" => {}, + Err(other) => panic!("{:?}", other), + _ => panic!("Excepted from_untyped to fail"), + } + } +} From b86d24025d6dd4718aa7782d92c90219d97ed2a4 Mon Sep 17 00:00:00 2001 From: Maurice Laveaux Date: Sat, 14 Mar 2026 12:02:39 +0100 Subject: [PATCH 08/18] Added a helper to determine whether a sort is certainly finite --- crates/typecheck/src/is_finite.rs | 24 ++++++++++++++++++++++++ 1 file changed, 24 insertions(+) create mode 100644 crates/typecheck/src/is_finite.rs diff --git a/crates/typecheck/src/is_finite.rs b/crates/typecheck/src/is_finite.rs new file mode 100644 index 000000000..28b66c9c5 --- /dev/null +++ b/crates/typecheck/src/is_finite.rs @@ -0,0 +1,24 @@ +use merc_syntax::ComplexSort; +use merc_syntax::SortExpression; + +/// Returns true iff the sort is finite. +pub fn is_finite(sort: &SortExpression) -> bool { + match sort { + SortExpression::Product { lhs, rhs } => is_finite(lhs) && is_finite(rhs), + SortExpression::Function { domain, range: _ } => is_finite(domain), + SortExpression::Struct { inner } => inner + .iter() + .all(|decl| decl.args.iter().all(|(_, sort)| is_finite(sort))), + SortExpression::Simple(sort) => match sort { + merc_syntax::Sort::Bool => true, + _ => false, // All number sorts are infinite. + }, + SortExpression::Complex(complex_sort, sort_expression) => { + (*complex_sort == ComplexSort::Set || *complex_sort == ComplexSort::FSet) && is_finite(sort_expression) + } + SortExpression::FlattenedFunction { domain, range: _ } => domain.iter().all(|sort| is_finite(sort)), + SortExpression::Reference(_) | SortExpression::Resolved(_, _) => { + unreachable!("is_finite should not be called on reference sorts") + } + } +} From 7177afde33106cf7c591f349ca114fe17e2ce625 Mon Sep 17 00:00:00 2001 From: Maurice Laveaux Date: Sat, 14 Mar 2026 12:02:55 +0100 Subject: [PATCH 09/18] Added a few of the basic well typeness checks --- crates/typecheck/src/is_well_typed.rs | 123 ++++++++++++++++++++++++++ 1 file changed, 123 insertions(+) create mode 100644 crates/typecheck/src/is_well_typed.rs diff --git a/crates/typecheck/src/is_well_typed.rs b/crates/typecheck/src/is_well_typed.rs new file mode 100644 index 000000000..2475c86be --- /dev/null +++ b/crates/typecheck/src/is_well_typed.rs @@ -0,0 +1,123 @@ +use thiserror::Error; + +use merc_syntax::SortExpression; +use merc_syntax::UntypedDataSpecification; +use merc_utilities::MercError; + +use crate::is_nonempty_sort; +use crate::target_sort; + +/// Checks if a signature is well-typed, i.e. it satisfies the conditions of 15.1.7. +pub fn is_well_typed(spec: &UntypedDataSpecification) -> Result<(), WellTypedError> { + are_constructors_and_mappings_disjoint(spec)?; + + // Check that there are no constructors defined for the basic sorts. + for constructor in &spec.constructor_declarations { + let sort = target_sort(&constructor.sort); + + // There are not more constructors for basic sorts. + if is_basic_sort(sort) { + return Err(WellTypedError::ConstructorForBasicSort { + constructor: constructor.identifier.clone(), + sort: sort.to_string(), + } + .into()); + } + + // Function sorts are not constructor sorts + if matches!(sort, SortExpression::Function { domain: _, range: _ }) { + return Err(WellTypedError::ConstructorForFunctionSort { + constructor: constructor.identifier.clone(), + sort: sort.to_string(), + }); + } + } + + // Check that all sorts are syntactically non-empty. + for sort in &spec.sort_declarations { + if is_nonempty_sort(&sort.identifier, spec) { + return Err(WellTypedError::EmptySort { + sort: sort.identifier.clone(), + }); + } + } + + + Ok(()) +} + +#[derive(Debug, Error)] +pub enum WellTypedError { + #[error("Constructor '{}' and mapping '{}' have the same identifier", constructor, map)] + ConstructorAndMappingConflict { constructor: String, map: String }, + + #[error( + "Constructors cannot be defined for basic sorts, but constructor '{}' is defined for sort '{}'", + constructor, + sort + )] + ConstructorForBasicSort { constructor: String, sort: String }, + + #[error( + "Constructors cannot be defined for function sorts, but constructor '{}' is defined for sort '{}'", + constructor, + sort + )] + ConstructorForFunctionSort { constructor: String, sort: String }, + + #[error("Sort '{}' is syntactically empty", sort)] + EmptySort { sort: String }, + + // These are name resolution errors, but we include them here to avoid having to define a separate error type for name resolution. + #[error("Duplicate sort declaration: '{}'", sort)] + DuplicateSortDeclaration { sort: String }, + + #[error("Undefined sort: '{}'", sort)] + UndefinedSort { sort: String }, + + #[error("Error: '{}'", 0)] + Custom(MercError), +} + +/// Checks that the constructors and mappings are disjoint, i.e. that no identifier is both a constructor and a mapping. +fn are_constructors_and_mappings_disjoint(spec: &UntypedDataSpecification) -> Result<(), WellTypedError> { + for constructor in &spec.constructor_declarations { + if let Some(map) = spec + .map_declarations + .iter() + .find(|map| map.identifier == constructor.identifier && map.sort == constructor.sort) + { + return Err(WellTypedError::ConstructorAndMappingConflict { + constructor: constructor.identifier.clone(), + map: map.identifier.clone(), + }); + } + } + + Ok(()) +} + +/// The set of basic sorts `BS` are exactly the sorts Bool, Pos, Int, Nat, and Real. Definition 15.1.2. +fn is_basic_sort(sort: &SortExpression) -> bool { + matches!(sort, SortExpression::Simple(_)) +} + +#[cfg(test)] +mod tests { + use merc_syntax::UntypedDataSpecification; + + use crate::DataSpecification; + + #[test] + fn test_well_typed_spec() { + let spec = UntypedDataSpecification::parse( + " + sort D; + cons f: D -> Nat; + ", + ) + .unwrap(); + + let _typed_spec = DataSpecification::from_untyped(spec).unwrap(); + } +} From b7f61ac06a7a2991840a54e930f2177502b1f93b Mon Sep 17 00:00:00 2001 From: Maurice Laveaux Date: Sat, 14 Mar 2026 12:03:10 +0100 Subject: [PATCH 10/18] Added the lib.rs for the typecheck crate --- crates/typecheck/src/lib.rs | 15 +++++++++++++++ 1 file changed, 15 insertions(+) create mode 100644 crates/typecheck/src/lib.rs diff --git a/crates/typecheck/src/lib.rs b/crates/typecheck/src/lib.rs new file mode 100644 index 000000000..a391accdc --- /dev/null +++ b/crates/typecheck/src/lib.rs @@ -0,0 +1,15 @@ +mod alias; +mod data_specification; +mod is_finite; +mod is_well_typed; +mod name_resolution; +mod non_empty; +mod standard_sorts; + +pub use alias::*; +pub use data_specification::*; +pub use is_finite::*; +pub use is_well_typed::*; +pub use name_resolution::*; +pub use non_empty::*; +pub use standard_sorts::*; From ee1aaef1c7e733f06cec55972178b2bd1efe2a6e Mon Sep 17 00:00:00 2001 From: Maurice Laveaux Date: Sat, 14 Mar 2026 12:08:53 +0100 Subject: [PATCH 11/18] Added the standard sorts, and reading the spec files. --- crates/typecheck/src/standard_sorts.rs | 145 +++++++++++++++++++++++++ 1 file changed, 145 insertions(+) create mode 100644 crates/typecheck/src/standard_sorts.rs diff --git a/crates/typecheck/src/standard_sorts.rs b/crates/typecheck/src/standard_sorts.rs new file mode 100644 index 000000000..ac9dba82a --- /dev/null +++ b/crates/typecheck/src/standard_sorts.rs @@ -0,0 +1,145 @@ +use std::convert::Infallible; + +use indoc::formatdoc; + +use merc_syntax::ComplexSort; +use merc_syntax::SortExpression; +use merc_syntax::UntypedDataSpecification; +use merc_syntax::apply_sort_expression; +use merc_utilities::MercError; + +/// Returns a standard data specification containing the standard sorts and their associated constructors, mappings, and equations. +pub fn basic_sort_data_specification() -> Result { + let mut result = UntypedDataSpecification::default(); + + // Append the relevant specifications for the sorts that are present in the specification. + result.merge(&UntypedDataSpecification::parse(include_str!( + "../../syntax/spec/bool.mcrl2" + ))?); + result.merge(&UntypedDataSpecification::parse(include_str!( + "../../syntax/spec/pos.mcrl2" + ))?); + result.merge(&UntypedDataSpecification::parse(include_str!( + "../../syntax/spec/int.mcrl2" + ))?); + result.merge(&UntypedDataSpecification::parse(include_str!( + "../../syntax/spec/nat.mcrl2" + ))?); + result.merge(&UntypedDataSpecification::parse(include_str!( + "../../syntax/spec/real.mcrl2" + ))?); + + Ok(result) +} + +/// Constructs a data specification for a standard sort; +pub fn standard_sort(sort: &SortExpression) -> Result { + if let SortExpression::Complex(complex, sort) = sort { + let text = match complex { + ComplexSort::List => include_str!("../../syntax/spec/list.mcrl2"), + ComplexSort::Set => include_str!("../../syntax/spec/set.mcrl2"), + ComplexSort::FSet => include_str!("../../syntax/spec/fset.mcrl2"), + ComplexSort::Bag => include_str!("../../syntax/spec/bag.mcrl2"), + ComplexSort::FBag => include_str!("../../syntax/spec/fbag.mcrl2"), + }; + + let spec = UntypedDataSpecification::parse(text)?; + + Ok(replace_sort(&spec, "S", sort)) + } else if let SortExpression::Function { domain, range } = sort { + let text = include_str!("../../syntax/spec/function_update.mcrl2"); + + let spec = UntypedDataSpecification::parse(text)?; + + // In the specification we define the function S -> T. + let spec = replace_sort(&spec, "S", domain); + let spec = replace_sort(&spec, "T", range); + + Ok(spec) + } else { + unreachable!("The given sort {} is not a standard sort", sort); + } +} + +/// Replaces the given identifier by the given sort expression in the given data +/// specification. +/// +/// # Details +/// +/// This function can be used to instantiate polymorphic types, for example, +/// replacing identifier `S` in the specification for `List(S)` by `Nat` to get +/// a specification for `List(Nat)`. +fn replace_sort(spec: &UntypedDataSpecification, identifier: &str, sort: &SortExpression) -> UntypedDataSpecification { + let mut result = spec.clone(); + + for constructor in &mut result.constructor_declarations { + constructor.sort = replace_sort_expression(&constructor.sort, identifier, sort); + } + + for map in &mut result.map_declarations { + map.sort = replace_sort_expression(&map.sort, identifier, sort); + } + + for equation in &mut result.equation_declarations { + for var in &mut equation.variables { + var.sort = replace_sort_expression(&var.sort, identifier, sort); + } + } + + result +} + +/// Replaces sort references of `identifier` in `sort` by the given `result_sort`. +fn replace_sort_expression(sort: &SortExpression, identifier: &str, result_sort: &SortExpression) -> SortExpression { + apply_sort_expression(sort.clone(), |expr| -> Result, Infallible> { + if let SortExpression::Reference(id) = expr { + if id == identifier { + return Ok(Some(result_sort.clone())); + } + } + + Ok(None) + }).unwrap() +} + +/// Generate a data specification for any sort based on the rules in Appendix `B`. +pub fn basic_spec(sort: &str) -> Result { + Ok(UntypedDataSpecification::parse(&formatdoc! {" + map ==, !=, <, <=, >=, >: {sort} # {sort} -> Bool; + if: Bool # {sort} # {sort} -> {sort}; + + var x, y: {sort}; + b: Bool; + + eqm x == x = true; + x != y = !(x == y); + if(true, x, y) = x; + if(false, x, y) = y; + if(b, x, y) = if (b, x, y); + if(x == y, x, y) = y; + x < x = false; + x <= x = true; + x > y = y < x; + x >= y = y <= x; + "})?) +} + +/// Generates a data specification for a structured sort, the rules are given in Appendix `B.10`. +pub fn structured_sort_spec( + name: &str, + structured_sort: &SortExpression, +) -> Result { + if let SortExpression::Struct { inner: _ } = structured_sort { + let name = format!("Struct{}", name); + + let spec = formatdoc!( + "sort {name} + + " + ); + + UntypedDataSpecification::parse(&spec) + } else { + unreachable!("structure_sort_spec should only be called on structured sorts"); + } +} From a116743965ca083943f98534bcb89f4989d3a660 Mon Sep 17 00:00:00 2001 From: Maurice Laveaux Date: Sat, 14 Mar 2026 13:22:44 +0100 Subject: [PATCH 12/18] Added an Infallible variant of visit_sort_expr. --- crates/syntax/src/builder.rs | 2 +- crates/syntax/src/visitor.rs | 20 ++++++++++++++++---- 2 files changed, 17 insertions(+), 5 deletions(-) diff --git a/crates/syntax/src/builder.rs b/crates/syntax/src/builder.rs index 1c17d8501..e16561feb 100644 --- a/crates/syntax/src/builder.rs +++ b/crates/syntax/src/builder.rs @@ -17,7 +17,7 @@ where apply_statefrm_rec(formula, &mut function) } -///// Applies the given function recursively to the sort expression. +/// Applies the given function recursively to the sort expression. pub fn apply_sort_expression(sort_expr: SortExpression, mut function: F) -> Result where F: FnMut(&SortExpression) -> Result, E>, diff --git a/crates/syntax/src/visitor.rs b/crates/syntax/src/visitor.rs index 16fceca93..a059afe51 100644 --- a/crates/syntax/src/visitor.rs +++ b/crates/syntax/src/visitor.rs @@ -1,3 +1,4 @@ +use std::convert::Infallible; use std::ops::ControlFlow; use merc_utilities::MercError; @@ -20,9 +21,20 @@ where visit_statefrm_rec(formula, &mut visitor) } -pub fn visit_sort_expr(sort_expr: &SortExpression, mut visitor: F) -> Result, MercError> +/// Visits all sort expressions in the sort expression. +pub fn visit_sort_expr(sort_expr: &SortExpression, mut visitor: F) -> Option where - F: FnMut(&SortExpression) -> Result, MercError>, + F: FnMut(&SortExpression) -> ControlFlow, +{ + try_visit_sort_expr(sort_expr, |sort_expr| -> Result<_, Infallible> { + Ok(visitor(sort_expr)) + }).expect("Inner function does not fail") +} + +/// Visits all sort expressions in the sort expression, allowing the visitor to return an error. +pub fn try_visit_sort_expr(sort_expr: &SortExpression, mut visitor: F) -> Result, E> +where + F: FnMut(&SortExpression) -> Result, E>, { visit_sort_expr_rec(sort_expr, &mut visitor) } @@ -76,9 +88,9 @@ where } /// See [`visit_sort_expr`]. -fn visit_sort_expr_rec(sort_expr: &SortExpression, function: &mut F) -> Result, MercError> +fn visit_sort_expr_rec(sort_expr: &SortExpression, function: &mut F) -> Result, E> where - F: FnMut(&SortExpression) -> Result, MercError>, + F: FnMut(&SortExpression) -> Result, E>, { if let ControlFlow::Break(result) = function(sort_expr)? { // The visitor requested to break the traversal. From 4fb4092a7f20bb99e31bbccacb9fc7b409551537 Mon Sep 17 00:00:00 2001 From: Maurice Laveaux Date: Sat, 14 Mar 2026 13:22:53 +0100 Subject: [PATCH 13/18] Detect alias loops. --- crates/typecheck/src/alias.rs | 101 ++++++++++++++++++++++++++++++++++ 1 file changed, 101 insertions(+) create mode 100644 crates/typecheck/src/alias.rs diff --git a/crates/typecheck/src/alias.rs b/crates/typecheck/src/alias.rs new file mode 100644 index 000000000..eca8aaf4a --- /dev/null +++ b/crates/typecheck/src/alias.rs @@ -0,0 +1,101 @@ +use std::collections::HashMap; +use std::ops::ControlFlow; + +use merc_collections::BlockIndex; +use merc_collections::BlockPartition; +use merc_collections::Graph; +use merc_collections::scc_decomposition; +use merc_syntax::DefId; +use merc_syntax::SortExpression; +use merc_syntax::UntypedDataSpecification; +use merc_syntax::visit_sort_expr; +use merc_utilities::TagIndex; + +/// Returns true iff there is a cycle in the alias declarations. +pub fn has_alias_cycle(spec: &UntypedDataSpecification) -> Result<(), Vec> { + // A mapping that keeps track of the relation between sorts. + let mut mapping: HashMap> = HashMap::new(); + + for sort_decl in &spec.sort_declarations { + if let Some(alias) = &sort_decl.expr { + let mut visited = Vec::new(); + + visit_sort_expr::<(), _>(alias, |sort| { + if let SortExpression::Resolved(_, id) = sort { + visited.push(*id); + } + + ControlFlow::Continue(()) + }); + + mapping.insert(sort_decl.id.expect("Name must have been resolved"), visited); + } + } + + let scc_partition = BlockPartition::<()>::from_indexed_partition(&scc_decomposition(&SortGraph { mapping }, |_, _, _| true)); + + for block in (0..scc_partition.len()).map(BlockIndex::new) { + if scc_partition.block(block).len() > 1 { + return Err(scc_partition.iter_block(block).map(|id| DefId::new(id)).collect()); + } + } + Ok(()) +} + +/// A graph structure representing the alias declarations in a data +/// specification. The vertices are the sorts, and there is an edge from sort A +/// to sort B if B is contained in the alias of A, i.e. `A -> B` if `A = List(B)`. +struct SortGraph { + mapping: HashMap>, +} + +/// A unique type for the sorts. +pub struct SortTag; + +/// The index type for a sort. +pub type SortIndex = TagIndex; + +impl Graph for SortGraph { + type VertexIndex = SortIndex; + + type LabelIndex = (); + + fn num_of_vertices(&self) -> usize { + self.mapping.len() + } + + fn iter_vertices(&self) -> impl Iterator { + self.mapping.keys().map(|id| SortIndex::new(**id)) + } + + fn outgoing_edges( + &self, + _vertex: Self::VertexIndex, + ) -> impl Iterator { + self.mapping + .get(&DefId::new(*_vertex)) + .expect("Vertex must be in the graph") + .iter() + .map(|id| ((), SortIndex::new(**id))) + } +} + +#[cfg(test)] +mod tests { + use merc_syntax::UntypedDataSpecification; + + use crate::{DataSpecification, WellTypedError}; + + #[test] + fn test_trivial_alias_cycle() { + let spec = UntypedDataSpecification::parse("sort S = T; + T = U; + U = S;").unwrap(); + + match DataSpecification::from_untyped(spec) { + Err(WellTypedError::AliasCycle { sorts }) if sorts == vec!["S".to_string(), "T".to_string(), "U".to_string()] => {}, + Err(other) => panic!("Unexpected error {:?}", other), + _ => panic!("Expected from_untyped to fail"), + } + } +} From 1e7dd4aec43b736d82a10eca09c331575f33a64e Mon Sep 17 00:00:00 2001 From: Maurice Laveaux Date: Sat, 14 Mar 2026 13:35:07 +0100 Subject: [PATCH 14/18] Small changes, added more error types. --- crates/typecheck/Cargo.toml | 2 ++ crates/typecheck/src/data_specification.rs | 14 ++++++++++++-- crates/typecheck/src/is_well_typed.rs | 9 ++++++--- crates/typecheck/src/non_empty.rs | 4 ++-- 4 files changed, 22 insertions(+), 7 deletions(-) diff --git a/crates/typecheck/Cargo.toml b/crates/typecheck/Cargo.toml index d55e4739a..34435a84d 100644 --- a/crates/typecheck/Cargo.toml +++ b/crates/typecheck/Cargo.toml @@ -10,6 +10,8 @@ version.workspace = true [dependencies] indoc.workspace = true +thiserror.workspace = true +merc_collections.workspace = true merc_syntax.workspace = true merc_utilities.workspace = true \ No newline at end of file diff --git a/crates/typecheck/src/data_specification.rs b/crates/typecheck/src/data_specification.rs index 05b91ade5..ba395a1f6 100644 --- a/crates/typecheck/src/data_specification.rs +++ b/crates/typecheck/src/data_specification.rs @@ -10,6 +10,7 @@ use merc_syntax::apply_sort_expression; use crate::WellTypedError; use crate::basic_sort_data_specification; +use crate::has_alias_cycle; use crate::is_well_typed; use crate::map_sorts_in_spec; use crate::resolve_names; @@ -27,7 +28,16 @@ impl DataSpecification { }) .expect("The inner function never fails"); - let _sorts = resolve_names(&mut spec)?; + let sorts = resolve_names(&mut spec)?; + + has_alias_cycle(&spec).map_err(|cycle| WellTypedError::AliasCycle { + sorts: cycle + .iter() + .map(|id| { + sorts.get_unchecked(**id).expect("The sort should be declared").clone() + }) + .collect(), + })?; is_well_typed(&spec)?; @@ -68,7 +78,7 @@ pub fn argument_sorts(sort: &SortExpression) -> &Vec { /// Replaces sort references of `identifier` in `sort` by the given `result_sort`. fn flatten_function_sorts(sort: &SortExpression) -> SortExpression { - apply_sort_expression(sort.clone(), |expr| -> Result<_, Infallible>{ + apply_sort_expression(sort.clone(), |expr| -> Result<_, Infallible> { if let SortExpression::Function { domain, range } = expr { let mut flattened_domain = Vec::new(); flatten_function_domain_rec(domain, &mut flattened_domain); diff --git a/crates/typecheck/src/is_well_typed.rs b/crates/typecheck/src/is_well_typed.rs index 2475c86be..9a69b30dd 100644 --- a/crates/typecheck/src/is_well_typed.rs +++ b/crates/typecheck/src/is_well_typed.rs @@ -68,15 +68,18 @@ pub enum WellTypedError { #[error("Sort '{}' is syntactically empty", sort)] EmptySort { sort: String }, + #[error("Alias cycle detected: {:?}", sorts)] + AliasCycle { sorts: Vec }, + + #[error("Error: '{}'", 0)] + Custom(MercError), + // These are name resolution errors, but we include them here to avoid having to define a separate error type for name resolution. #[error("Duplicate sort declaration: '{}'", sort)] DuplicateSortDeclaration { sort: String }, #[error("Undefined sort: '{}'", sort)] UndefinedSort { sort: String }, - - #[error("Error: '{}'", 0)] - Custom(MercError), } /// Checks that the constructors and mappings are disjoint, i.e. that no identifier is both a constructor and a mapping. diff --git a/crates/typecheck/src/non_empty.rs b/crates/typecheck/src/non_empty.rs index 8cce89944..c3870e818 100644 --- a/crates/typecheck/src/non_empty.rs +++ b/crates/typecheck/src/non_empty.rs @@ -76,8 +76,8 @@ mod tests { match DataSpecification::from_untyped(spec) { Err(WellTypedError::EmptySort { sort }) if sort == "D" => {}, - Err(other) => panic!("{:?}", other), - _ => panic!("Excepted from_untyped to fail"), + Err(other) => panic!("Unexpected {:?}", other), + _ => panic!("Unexpected from_untyped to fail"), } } } From 357dc687a97881d360f1432f55aa1e301e31f550 Mon Sep 17 00:00:00 2001 From: Maurice Laveaux Date: Sat, 14 Mar 2026 15:20:40 +0100 Subject: [PATCH 15/18] Fixed some tests. --- Cargo.lock | 2 ++ crates/collections/src/block_partition.rs | 4 ++++ crates/typecheck/src/is_well_typed.rs | 8 ++++++-- 3 files changed, 12 insertions(+), 2 deletions(-) diff --git a/Cargo.lock b/Cargo.lock index 348e098c8..ebae5ae49 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -1364,8 +1364,10 @@ name = "merc_typecheck" version = "1.0.0" dependencies = [ "indoc", + "merc_collections", "merc_syntax", "merc_utilities", + "thiserror", ] [[package]] diff --git a/crates/collections/src/block_partition.rs b/crates/collections/src/block_partition.rs index 13f257267..67e343627 100644 --- a/crates/collections/src/block_partition.rs +++ b/crates/collections/src/block_partition.rs @@ -31,6 +31,10 @@ impl BlockPartition { impl BlockPartition { /// Create a block partition from an indexed partition. + /// + /// This function creates a new partition that is dense, i.e. it does not + /// contain empty blocks, and the blocks are indexed from 0 to n-1 even if the + /// indexed partition is sparse. pub fn from_indexed_partition(partition: &IndexedPartition) -> Self { let mut blocks = vec![Block::new_empty(); partition.num_of_blocks()]; let num_of_blocks = partition.iter().count(); diff --git a/crates/typecheck/src/is_well_typed.rs b/crates/typecheck/src/is_well_typed.rs index 9a69b30dd..0e7e12bd0 100644 --- a/crates/typecheck/src/is_well_typed.rs +++ b/crates/typecheck/src/is_well_typed.rs @@ -109,7 +109,7 @@ fn is_basic_sort(sort: &SortExpression) -> bool { mod tests { use merc_syntax::UntypedDataSpecification; - use crate::DataSpecification; + use crate::{DataSpecification, WellTypedError}; #[test] fn test_well_typed_spec() { @@ -121,6 +121,10 @@ mod tests { ) .unwrap(); - let _typed_spec = DataSpecification::from_untyped(spec).unwrap(); + match DataSpecification::from_untyped(spec) { + Err(WellTypedError::ConstructorForBasicSort { constructor, sort }) if constructor == "f" && sort == "Nat" => {}, + Err(other) => panic!("Unexpected error {:?}", other), + _ => panic!("Expected from_untyped to fail"), + } } } From c4aa8642a1246c035933f2892134c72e27f8c136 Mon Sep 17 00:00:00 2001 From: Maurice Laveaux Date: Thu, 2 Apr 2026 11:54:07 +0200 Subject: [PATCH 16/18] Fixed several suggestions in the typecheck functions --- crates/collections/src/block_partition.rs | 15 +++++++++++---- crates/collections/src/compressed_vec.rs | 5 +++-- crates/collections/src/indexed_set.rs | 1 - crates/typecheck/src/alias.rs | 16 ++++++++++------ crates/typecheck/src/is_well_typed.rs | 4 ++-- crates/typecheck/src/non_empty.rs | 7 +++++-- crates/typecheck/src/standard_sorts.rs | 2 +- crates/unsafety/src/protection_set.rs | 4 ++-- 8 files changed, 34 insertions(+), 20 deletions(-) diff --git a/crates/collections/src/block_partition.rs b/crates/collections/src/block_partition.rs index 67e343627..694695533 100644 --- a/crates/collections/src/block_partition.rs +++ b/crates/collections/src/block_partition.rs @@ -31,7 +31,7 @@ impl BlockPartition { impl BlockPartition { /// Create a block partition from an indexed partition. - /// + /// /// This function creates a new partition that is dense, i.e. it does not /// contain empty blocks, and the blocks are indexed from 0 to n-1 even if the /// indexed partition is sparse. @@ -259,9 +259,11 @@ impl Iterator for BlockIter<'_> { mod tests { use merc_utilities::random_test; use rand::RngExt; - use rand::seq::IteratorRandom; - - use super::*; + + use super::BlockIndex; + use super::BlockPartition; + use super::IndexedPartition; + use super::trace; #[test] fn test_simple_block_partition() { @@ -306,6 +308,11 @@ mod tests { expected_block, "Block {block} contains elements from different indexed-partition blocks" ); + assert_eq!( + partition.block(element), + expected_block, + "Block {block} contains elements from different indexed-partition blocks" + ); } } }) diff --git a/crates/collections/src/compressed_vec.rs b/crates/collections/src/compressed_vec.rs index de25afd6b..4b4fb9d4b 100644 --- a/crates/collections/src/compressed_vec.rs +++ b/crates/collections/src/compressed_vec.rs @@ -484,14 +484,15 @@ impl CompressedEntry for TagIndex { #[cfg(test)] mod tests { - use super::*; - use rand::RngExt; use rand::distr::Uniform; use rand::seq::SliceRandom; use merc_utilities::random_test; + use super::ByteCompressedVec; + use super::CompressedEntry; + #[test] fn test_index_bytevector() { let mut vec = ByteCompressedVec::new(); diff --git a/crates/collections/src/indexed_set.rs b/crates/collections/src/indexed_set.rs index b15191cb1..08a8a6c9c 100644 --- a/crates/collections/src/indexed_set.rs +++ b/crates/collections/src/indexed_set.rs @@ -448,7 +448,6 @@ impl<'a, T, S> IntoIterator for &'a IndexedSet { #[cfg(test)] mod tests { use std::collections::HashMap; - use rand::RngExt; use merc_utilities::random_test; diff --git a/crates/typecheck/src/alias.rs b/crates/typecheck/src/alias.rs index eca8aaf4a..bff5f86f1 100644 --- a/crates/typecheck/src/alias.rs +++ b/crates/typecheck/src/alias.rs @@ -61,21 +61,25 @@ impl Graph for SortGraph { type LabelIndex = (); fn num_of_vertices(&self) -> usize { - self.mapping.len() + self.mapping + .keys() + .map(|id| **id) + .max() + .map_or(0, |max_id| max_id + 1) } fn iter_vertices(&self) -> impl Iterator { - self.mapping.keys().map(|id| SortIndex::new(**id)) + (0..self.num_of_vertices()).map(SortIndex::new) } fn outgoing_edges( &self, - _vertex: Self::VertexIndex, + vertex: Self::VertexIndex, ) -> impl Iterator { self.mapping - .get(&DefId::new(*_vertex)) - .expect("Vertex must be in the graph") - .iter() + .get(&DefId::new(*vertex)) + .into_iter() + .flat_map(|targets| targets.iter()) .map(|id| ((), SortIndex::new(**id))) } } diff --git a/crates/typecheck/src/is_well_typed.rs b/crates/typecheck/src/is_well_typed.rs index 0e7e12bd0..868d82512 100644 --- a/crates/typecheck/src/is_well_typed.rs +++ b/crates/typecheck/src/is_well_typed.rs @@ -35,7 +35,7 @@ pub fn is_well_typed(spec: &UntypedDataSpecification) -> Result<(), WellTypedErr // Check that all sorts are syntactically non-empty. for sort in &spec.sort_declarations { - if is_nonempty_sort(&sort.identifier, spec) { + if !is_nonempty_sort(&sort.identifier, spec) { return Err(WellTypedError::EmptySort { sort: sort.identifier.clone(), }); @@ -88,7 +88,7 @@ fn are_constructors_and_mappings_disjoint(spec: &UntypedDataSpecification) -> Re if let Some(map) = spec .map_declarations .iter() - .find(|map| map.identifier == constructor.identifier && map.sort == constructor.sort) + .find(|map| map.identifier == constructor.identifier) { return Err(WellTypedError::ConstructorAndMappingConflict { constructor: constructor.identifier.clone(), diff --git a/crates/typecheck/src/non_empty.rs b/crates/typecheck/src/non_empty.rs index c3870e818..4c293f088 100644 --- a/crates/typecheck/src/non_empty.rs +++ b/crates/typecheck/src/non_empty.rs @@ -47,14 +47,17 @@ fn is_nonempty_sort_rec(sort: DefId, constructors: &Vec, seen: &mut Hash seen.insert(sort); // Mark the current sort as seen to avoid cycles. - if argument_sorts(&constructor.sort).iter().all(|_arg| true) { + if argument_sorts(&constructor.sort).iter().all(|arg| match arg { + SortExpression::Resolved(_, id) => is_nonempty_sort_rec(*id, constructors, seen), + _ => true, + }) { return true; // All argument sorts are non-empty, so the sort is non-empty. } seen.remove(&sort); // Unmark the current sort as seen to allow other paths to explore it. } - true + false } #[cfg(test)] diff --git a/crates/typecheck/src/standard_sorts.rs b/crates/typecheck/src/standard_sorts.rs index ac9dba82a..2641ccb74 100644 --- a/crates/typecheck/src/standard_sorts.rs +++ b/crates/typecheck/src/standard_sorts.rs @@ -140,6 +140,6 @@ pub fn structured_sort_spec( UntypedDataSpecification::parse(&spec) } else { - unreachable!("structure_sort_spec should only be called on structured sorts"); + unreachable!("structured_sort_spec should only be called on structured sorts"); } } diff --git a/crates/unsafety/src/protection_set.rs b/crates/unsafety/src/protection_set.rs index ba0d5203c..024a985a1 100644 --- a/crates/unsafety/src/protection_set.rs +++ b/crates/unsafety/src/protection_set.rs @@ -310,8 +310,8 @@ mod tests { use merc_utilities::random_test; use merc_utilities::test_logger; - use crate::ProtectionIndex; - use crate::ProtectionSet; + use super::ProtectionIndex; + use super::ProtectionSet; #[test] #[cfg_attr(miri, ignore)] From 4f5f99a7ebe20aac25db0df107d4adecc0e8d0e5 Mon Sep 17 00:00:00 2001 From: Maurice Laveaux Date: Thu, 2 Apr 2026 11:54:27 +0200 Subject: [PATCH 17/18] Check for duplicated transitions in labelled transition systems. --- crates/lts/src/labelled_transition_system.rs | 21 ++++++++++++++++++++ 1 file changed, 21 insertions(+) diff --git a/crates/lts/src/labelled_transition_system.rs b/crates/lts/src/labelled_transition_system.rs index fdd9050c0..f8d48758f 100644 --- a/crates/lts/src/labelled_transition_system.rs +++ b/crates/lts/src/labelled_transition_system.rs @@ -1,6 +1,7 @@ #![forbid(unsafe_code)] use std::collections::HashMap; +use std::collections::HashSet; use std::fmt; use merc_collections::ByteCompressedVec; @@ -412,6 +413,26 @@ impl LabelledTransitionSystem