Added various parts of the well typedness checks

Cargo.toml

@@ -42,6 +42,7 @@ members = [
     "crates/symbolic",
     "crates/syntax",
     "crates/tools",
+    "crates/typecheck",
     "crates/unsafety",
     "crates/utilities",
     "crates/vpg",
@@ -132,16 +133,17 @@ merc_ldd = { version = "3.0", path = "crates/ldd" }
 merc_lts = { version = "2.0", path = "crates/lts" }
 merc_macros = { version = "2.0", path = "crates/macros" }
 merc_number = { version = "2.0", path = "crates/number" }
-merc_refinement = { version = "2.0", path = "crates/refinement" }
 merc_rec-tests = { path = "crates/rec-tests" }
 merc_reduction = { version = "2.0", path = "crates/reduction" }
+merc_refinement = { version = "2.0", path = "crates/refinement" }
 merc_sabre = { version = "2.0", path = "crates/sabre" }
 merc_sabre-compiling = { path = "crates/sabre_compiling" }
 merc_sabre-ffi = { path = "crates/sabre_compiling/sabre_ffi" }
 merc_sharedmutex = { version = "2.0", path = "crates/sharedmutex" }
 merc_symbolic = { version = "3.0", path = "crates/symbolic", features = ["clap"] }
 merc_syntax = { version = "2.0", path = "crates/syntax" }
 merc_tools = { path = "crates/tools" }
+merc_typecheck = { path = "crates/typecheck" }
 merc_unsafety = { version = "2.0", path = "crates/unsafety" }
 merc_utilities = { version = "3.0", path = "crates/utilities" }
 merc_vpg = { path = "crates/vpg", features = ["clap"] }

crates/collections/src/block_partition.rs

@@ -31,6 +31,10 @@ impl<A: Clone + fmt::Debug + Default> BlockPartition<A> {
 
 impl<A: Clone + fmt::Debug + Default> BlockPartition<A> {
     /// 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();
@@ -253,11 +257,15 @@ impl Iterator for BlockIter<'_> {
 
 #[cfg(test)]
 mod tests {
-    use merc_utilities::random_test;
     use rand::RngExt;
     use rand::seq::IteratorRandom;
 
-    use super::*;
+    use merc_utilities::random_test;
+
+    use super::BlockIndex;
+    use super::BlockPartition;
+    use super::IndexedPartition;
+    use super::trace;
 
     #[test]
     fn test_simple_block_partition() {
@@ -302,6 +310,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"
+                    );
                 }
             }
         })

crates/collections/src/compressed_vec.rs

@@ -484,14 +484,15 @@ impl<T: CompressedEntry + Copy, Tag> CompressedEntry for TagIndex<T, Tag> {
 
 #[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();

crates/collections/src/indexed_set.rs

@@ -382,9 +382,8 @@ impl<'a, T, S> IntoIterator for &'a IndexedSet<T, S> {
 
 #[cfg(test)]
 mod tests {
-    use std::collections::HashMap;
-
     use rand::RngExt;
+    use std::collections::HashMap;
 
     use merc_utilities::random_test;
 

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<Label: TransitionLabel> LabelledTransitionSystem<Label> {
                 num_states
             );
         }
+
+        for state in 0..num_states {
+            let start = self.states.index(state);
+            let end = self.states.index(state + 1);
+            let mut seen = HashSet::with_capacity(end.saturating_sub(start));
+
+            for i in start..end {
+                let edge = (
+                    self.transition_labels.index(i).value(),
+                    self.transition_to.index(i).value(),
+                );
+
+                debug_assert!(
+                    seen.insert(edge),
+                    "state {state} has duplicate outgoing transition with label {} to state {}",
+                    edge.0,
+                    edge.1
+                );
+            }
+        }
     }
 
     /// Returns metrics about the LTS.

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

crates/syntax/src/builder.rs

@@ -17,9 +17,10 @@ where
     apply_statefrm_rec(formula, &mut function)
 }
 
-pub fn apply_sort_expression<F>(sort_expr: SortExpression, mut function: F) -> Result<SortExpression, MercError>
+/// Applies the given function recursively to the sort expression.
+pub fn apply_sort_expression<E, F>(sort_expr: SortExpression, mut function: F) -> Result<SortExpression, E>
 where
-    F: FnMut(&SortExpression) -> Result<Option<SortExpression>, MercError>,
+    F: FnMut(&SortExpression) -> Result<Option<SortExpression>, E>,
 {
     apply_sort_expression_rec(sort_expr, &mut function)
 }
@@ -164,9 +165,10 @@ where
     }
 }
 
-fn apply_sort_expression_rec<F>(sort_expr: SortExpression, apply: &mut F) -> Result<SortExpression, MercError>
+/// See [`apply_sort_expression`].
+fn apply_sort_expression_rec<E, F>(sort_expr: SortExpression, apply: &mut F) -> Result<SortExpression, E>
 where
-    F: FnMut(&SortExpression) -> Result<Option<SortExpression>, MercError>,
+    F: FnMut(&SortExpression) -> Result<Option<SortExpression>, E>,
 {
     if let Some(sort_expr) = apply(&sort_expr)? {
         // A substitution was made, return the new sort expression.
@@ -203,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::<Result<Vec<SortExpression>, _>>()?;
+            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)
         }

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<usize, DeclTag>;
+pub type DefId = TagIndex<usize, DefTag>;
 
 /// 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<DeclId>,
+    pub id: Option<DefId>,
 }
 
 impl IdDecl {
@@ -143,6 +143,13 @@ pub enum SortExpression {
     Simple(Sort),
     /// Parameterized complex sort
     Complex(ComplexSort, Box<SortExpression>),
+    /// 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<SortExpression>,
+        range: Box<SortExpression>,
+    },
 }
 
 /// Constructor declaration
@@ -183,7 +190,7 @@ pub struct SortDecl {
     /// Where the sort is defined
     pub span: Span,
     /// Unique ID assigned to this declaration during name resolution.
-    pub id: Option<DeclId>,
+    pub id: Option<DefId>,
 }
 
 impl SortDecl {

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})")
+            }
         }
     }
 }

crates/syntax/src/visitor.rs

@@ -1,3 +1,4 @@
+use std::convert::Infallible;
 use std::ops::ControlFlow;
 
 use merc_utilities::MercError;
@@ -20,9 +21,21 @@ where
     visit_statefrm_rec(formula, &mut visitor)
 }
 
-pub fn visit_sort_expr<T, F>(sort_expr: &SortExpression, mut visitor: F) -> Result<Option<T>, MercError>
+/// Visits all sort expressions in the sort expression.
+pub fn visit_sort_expr<T, F>(sort_expr: &SortExpression, mut visitor: F) -> Option<T>
 where
-    F: FnMut(&SortExpression) -> Result<ControlFlow<T>, MercError>,
+    F: FnMut(&SortExpression) -> ControlFlow<T>,
+{
+    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<E, T, F>(sort_expr: &SortExpression, mut visitor: F) -> Result<Option<T>, E>
+where
+    F: FnMut(&SortExpression) -> Result<ControlFlow<T>, E>,
 {
     visit_sort_expr_rec(sort_expr, &mut visitor)
 }
@@ -75,9 +88,10 @@ where
     Ok(None)
 }
 
-fn visit_sort_expr_rec<T, F>(sort_expr: &SortExpression, function: &mut F) -> Result<Option<T>, MercError>
+/// See [`visit_sort_expr`].
+fn visit_sort_expr_rec<E, T, F>(sort_expr: &SortExpression, function: &mut F) -> Result<Option<T>, E>
 where
-    F: FnMut(&SortExpression) -> Result<ControlFlow<T>, MercError>,
+    F: FnMut(&SortExpression) -> Result<ControlFlow<T>, E>,
 {
     if let ControlFlow::Break(result) = function(sort_expr)? {
         // The visitor requested to break the traversal.
@@ -103,7 +117,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.

crates/typecheck/Cargo.toml

@@ -0,0 +1,17 @@
+[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
+thiserror.workspace = true
+
+merc_collections.workspace = true
+merc_syntax.workspace = true
+merc_utilities.workspace = true