Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
94 commits
Select commit Hold shift + click to select a range
a28d402
Updated oxidd to the latest version
mlaveaux Jul 10, 2026
50de3ca
Fixed an issue in the sort expr precedence rules
mlaveaux Jul 11, 2026
c6ba242
Added example tests for type checking
mlaveaux Jul 11, 2026
7830098
Changed nonempty sort check to be a simply fixpoint computation that …
mlaveaux Jul 11, 2026
8d20574
Implement desugaring of struct sorts
mlaveaux Jul 11, 2026
215ac5c
Enhance name resolution by deduplicating identical sort declarations …
mlaveaux Jul 11, 2026
d057894
Moved sort signature generation to desugar step
mlaveaux Jul 11, 2026
bb8d79f
Improved the alias detection, added a visitor that can deal with cont…
mlaveaux Jul 11, 2026
699de08
Added tests for the context visitor
mlaveaux Jul 11, 2026
50bd88c
Added the various passes to the data specification from_untyped
mlaveaux Jul 11, 2026
efc5296
Formatting
mlaveaux Jul 11, 2026
fb9ec4b
Extended the well typedness checks
mlaveaux Jul 11, 2026
54971ba
Added various tests from the mCRL2 toolset as well
mlaveaux Jul 11, 2026
4293164
Implement signature resolution and overload handling in type checking
mlaveaux Jul 11, 2026
cd680e4
Add support for binder sort resolution in type checking
mlaveaux Jul 11, 2026
16084b3
Add ena dependency and implement unification logic for type checking
mlaveaux Jul 11, 2026
ce9da95
Refactor is_finite function visibility
mlaveaux Jul 11, 2026
8fd42d1
Added a step to lower AST nodes into a plain application, i.e., x && …
mlaveaux Jul 12, 2026
da01f7e
Added apply function for data expressions
mlaveaux Jul 12, 2026
3be69d0
Added various debug statements
mlaveaux Jul 12, 2026
2fc04f0
Find all system defined sorts and add their standard definitions to t…
mlaveaux Jul 12, 2026
78f95b1
Add ResolvedSort and SortInterner implementations for type system
mlaveaux Jul 12, 2026
31f1c42
Added the alias normalisation pass
mlaveaux Jul 12, 2026
cd23f8b
Implement TypeckContext and QueryCache for type-checking queries
mlaveaux Jul 12, 2026
5648e80
Wire in all the new modules
mlaveaux Jul 12, 2026
24f7351
Added another test
mlaveaux Jul 12, 2026
b9489f9
Implement type inference, calling the unification of all expression t…
mlaveaux Jul 12, 2026
37a0e2b
Add system resolution for type-checking with internal sort names
mlaveaux Jul 12, 2026
4b06d17
Implement sort resolution for declarations and expressions in type-ch…
mlaveaux Jul 12, 2026
e930d1f
Added visitor for data expression, parse system specs only once
mlaveaux Jul 12, 2026
f7b3bd1
Added parsing of mCRL2 specification to merc-rewrite
mlaveaux Jul 12, 2026
cc9446e
Added the ena dependency
mlaveaux Jul 12, 2026
815daf7
Add fixed-arity term creation methods to ATermStorage and GlobalTermP…
mlaveaux Jul 12, 2026
dbd79f8
Refactor IdDecl to support generic ID types and update related specif…
mlaveaux Jul 12, 2026
dbb320e
Use IDs instead of more fragile offsets for the resolution
mlaveaux Jul 12, 2026
ec7d2a4
Replaced visitors
mlaveaux Jul 12, 2026
d6af8e8
Added additional tests
mlaveaux Jul 12, 2026
23a88f7
Typecheck binders
mlaveaux Jul 12, 2026
cbe4acb
Update example tests and inference tests for improved coverage
mlaveaux Jul 13, 2026
2f959b3
Implement system specification checker for well-formedness validation
mlaveaux Jul 13, 2026
1b73de2
Enhance type checking by implementing binder sort hoisting and numeri…
mlaveaux Jul 13, 2026
d99a48b
Refactor data specification handling: replace DataSpecification with …
mlaveaux Jul 13, 2026
bdefe26
Started to lowering of the type checked data specification into the M…
mlaveaux Jul 13, 2026
3e5143a
Moved passes into various submodules in merc_typecheck
mlaveaux Jul 13, 2026
f8d4a6c
Clarify documentation on thread-local destructors and safety in ATerm…
mlaveaux Jul 13, 2026
40fa088
Removed unused product_lts module, this can be replaced by combine
mlaveaux Jul 13, 2026
0b6e531
Added lowering of various binders
mlaveaux Jul 14, 2026
9969b29
Added unification for various empty sets/bags by selecting a default …
mlaveaux Jul 14, 2026
5083420
Refactor sort resolution to default free element sorts to Bool and up…
mlaveaux Jul 14, 2026
00483ad
Refactor type-checking context and improve sort resolution
mlaveaux Jul 14, 2026
7f66d86
Introduced an EqnVarId for name resolution of equation spec variables.
mlaveaux Jul 15, 2026
b9ee083
Mark all public symbols in merc_data explicitly
mlaveaux Jul 15, 2026
eefaf0d
Extended the lowering, and ran formatting
mlaveaux Jul 15, 2026
8bcd506
Marked items pub(crate) in the mcrl2 crate
mlaveaux Jul 15, 2026
f977811
Convert between mcrl2 and merc aterms
mlaveaux Jul 15, 2026
7746942
Added lowering tests
mlaveaux Jul 15, 2026
776e587
Implement join constraints for shared free variables in type inference.
mlaveaux Jul 15, 2026
18d6f55
Removed references from documentation to the mcrl2 source code
mlaveaux Jul 15, 2026
17bc303
Updated various comments
mlaveaux Jul 16, 2026
8f9c4c0
Added explicit exports for the merc_syntax crate.
mlaveaux Jul 16, 2026
da88c05
Added spans to the DataExpr AST
mlaveaux Jul 17, 2026
daee680
Added rendering of spans
mlaveaux Jul 17, 2026
475ee7f
Added assertions for missing system equations
mlaveaux Jul 17, 2026
9aa9b90
Added the machine number specifications
mlaveaux Jul 17, 2026
f1cddf2
Wire up a conversion from Mcrl2DataSpecification to a RewriteSpecific…
mlaveaux Jul 17, 2026
e6b91cb
Added the machine word compiled rules
mlaveaux Jul 18, 2026
78f886f
Added spans to all the syntax tree nodes
mlaveaux Jul 18, 2026
f14a8c6
Added lowering of the machine words
mlaveaux Jul 18, 2026
787a818
Ran formatting, updated the buildt in operators for all equations
mlaveaux Jul 18, 2026
40a1a2b
Added a missing export
mlaveaux Jul 18, 2026
d68326a
Ensure that the Term variant is also marked properly
mlaveaux Jul 20, 2026
abee276
Added the binary and machine word encodings, and their operations
mlaveaux Jul 20, 2026
cc1c1fb
Add the machine numbers to the set automaton construction
mlaveaux Jul 20, 2026
1d325eb
Updated various comments
mlaveaux Jul 21, 2026
922ebb4
Renamed to TypeCheckContext
mlaveaux Jul 24, 2026
90ab8ed
Added a check command for data specifications to the rewrite CLI
mlaveaux Jul 24, 2026
e9ef3e0
Renamed to mcrl2_lowering
mlaveaux Jul 24, 2026
558a6ac
Started README
mlaveaux Jul 24, 2026
8cd360b
Fixed display for sort expressions
mlaveaux Jul 24, 2026
45f1a26
Added printing of Mcrl2DataSpecification
mlaveaux Jul 24, 2026
154e2e4
Removed resolve_sort, and use the query directly instead of storing t…
mlaveaux Jul 24, 2026
9fcc9c0
Removed checks from is_well_typed that build_signature already did
mlaveaux Jul 24, 2026
95fc887
Smaller formatting fixes
mlaveaux Jul 24, 2026
b394c1c
Moved builtins to a central place.
mlaveaux Jul 25, 2026
77de69a
Added span information to all well typedness errors.
mlaveaux Jul 25, 2026
b9f7610
Made the query cache closure based to avoid the unlock.
mlaveaux Jul 25, 2026
a671cbb
Fix set automaton partition merging to use obligation positions
mlaveaux Aug 4, 2026
8948e67
Refactor system signature resolution and grouping
mlaveaux Aug 5, 2026
caa20f9
Disabled the local patched mCRL2-sys
mlaveaux Aug 5, 2026
d1e87ca
Renamed a variable
mlaveaux Aug 7, 2026
5e1954b
Merge main into feature/typecheck
mlaveaux Aug 10, 2026
a01a725
Updated upstream, and fixed compilation. Added lowering tests.
mlaveaux Aug 10, 2026
23c1093
Added type checking for individual data expressions
mlaveaux Aug 10, 2026
9fcd727
Applied formatting
mlaveaux Aug 10, 2026
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
17 changes: 17 additions & 0 deletions Cargo.lock

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

1 change: 1 addition & 0 deletions Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -70,6 +70,7 @@ clap = { version = "4.6", features = ["derive"] }
core_affinity2 = "0.15"
dashmap = { version = "7.0.0-rc2", features = ["inline-more"] }
delegate = "0.13"
ena = "0.14"
env_logger = { version = "0.11", features = ["kv"] }
equivalent = "1.0"
hashbrown = "0.17"
Expand Down
20 changes: 11 additions & 9 deletions crates/aterm/src/aterm.rs
Original file line number Diff line number Diff line change
Expand Up @@ -228,17 +228,19 @@ impl fmt::Debug for ATermRef<'_> {
/// # Safety
///
/// Note that terms use thread-local state for their protection mechanism, so
/// [ATerm] is not [Send]. Terms should not be dropped after the thread that
/// created them has exited, because the order in which thread-local destructors
/// run is undefined and dropping a term after `THREAD_TERM_POOL` is gone panics.
/// For this purpose one can wrap terms kept in thread-local storage in
/// `ManuallyDrop` to simply never drop them.
/// [ATerm] is not [Send]. Moreover, this means that terms cannot be stored in
/// thread-local storage themselves, or at least must be destroyed before the
/// thread exits, because the order in which thread-local destructors are called
/// is undefined, and as such a term could be destroyed after the thread-local
/// term pool is destroyed, leading to undefined behavior.
///
/// Read-only inspection of a term after its originating thread has exited
/// remains memory-safe: any roots still protected at thread teardown are adopted
/// into a global orphan set (deduplicated), so their storage is not reclaimed.
/// For this purpose one can use `ManuallyDrop` to simply never drop thread
/// local terms, since exiting the thread will clean up the protection sets
/// anyway.
///
/// If you need to send a term across threads, use [ATermSend] instead.
/// We do not mark term access as unsafe, since that would make their use
/// cumbersome. An alternative would be to require `THREAD_TERM_POOL.with(|tp|
/// ...)` around every access, but that would be very verbose.
pub struct ATerm {
term: ATermRef<'static>,

Expand Down
107 changes: 84 additions & 23 deletions crates/aterm/src/storage/aterm_storage.rs
Original file line number Diff line number Diff line change
Expand Up @@ -45,6 +45,10 @@ const INITIAL_CAPACITY: usize = 1024;
/// The number of terms stored in every block of the fixed-size storage.
const BLOCK_SIZE: usize = 1024;

/// The largest arity stored in the fixed-size tables; larger terms go into the
/// dynamically sized `terms` storage.
pub(crate) const MAX_FIXED_ARITY: usize = 7;

impl ATermStorage {
/// Creates a new, empty storage.
pub(crate) fn new() -> Self {
Expand Down Expand Up @@ -80,13 +84,76 @@ impl ATermStorage {
"The number of arguments does not match the arity of the symbol"
);

if symbol.arity() <= MAX_FIXED_ARITY {
return self.insert_fixed(symbol, args);
}

let shared_term = SharedTermLookup {
symbol: SymbolRef::from_symbol(symbol),
arguments: args,
};

unsafe {
self.terms
.insert_equiv_dst(&shared_term, SharedTerm::length_for(&shared_term), |ptr, key| {
SharedTerm::construct(ptr, key)
})
}
}

/// Inserts a term whose arity is at most [MAX_FIXED_ARITY] into the corresponding fixed-size
/// storage, building the `SharedTermFixed<N>` key straight from the argument slice.
///
/// Taking the arguments as a generic `T: Term` slice lets callers pass the terms they already
/// have (e.g. the input slice of [crate::ATerm::with_args]) without first materialising an
/// intermediate `ATermRef` buffer.
pub(crate) fn insert_fixed<'a, 'b, 'c, 'd, S, T>(
&self,
symbol: &'b S,
args: &[T],
) -> (StablePointer<SharedTerm>, bool)
where
S: Symb<'a, 'b>,
T: Term<'c, 'd>,
{
debug_assert_eq!(
symbol.arity(),
args.len(),
"The number of arguments does not match the arity of the symbol"
);

// SAFETY: the copied argument indices are stored inside the inserted term, and the
// GC marks the arguments of every live term, so each argument stays in the pool at
// least as long as the term referencing it; the copies are dropped when the term
// itself is reclaimed.
let arg = |i: usize| unsafe { args[i].shared().copy() };
self.insert_fixed_iter(symbol, args.iter().map(|arg| unsafe { arg.shared().copy() }))
}

/// Inserts a term whose arity is at most [MAX_FIXED_ARITY], pulling the argument indices
/// straight from the iterator. Counterpart of [Self::insert_fixed] for callers that only
/// have an iterator and would otherwise round-trip through an intermediate buffer.
///
/// The caller produces the `ATermIndex` copies (an unsafe operation) and thereby
/// guarantees they stay valid until the inserted term takes ownership of them.
///
/// # Panics
///
/// Panics when the iterator yields fewer items than the arity of the symbol.
pub(crate) fn insert_fixed_iter<'a, 'b, S, I>(
&self,
symbol: &'b S,
mut args: I,
) -> (StablePointer<SharedTerm>, bool)
where
S: Symb<'a, 'b>,
I: Iterator<Item = ATermIndex>,
{
let mut arg = || {
args.next()
.expect("The iterator yields fewer arguments than the arity of the symbol")
};

match symbol.arity() {
let result = match symbol.arity() {
0 => {
let (result, inserted) = self.terms_0.insert(SharedTermFixed {
symbol: SymbolRef::from_symbol(symbol),
Expand All @@ -97,66 +164,60 @@ impl ATermStorage {
1 => {
let (result, inserted) = self.terms_1.insert(SharedTermFixed {
symbol: SymbolRef::from_symbol(symbol),
args: [arg(0)],
args: [arg()],
});
unsafe { (cast_to_shared_term_ptr(&result, 1), inserted) }
}
2 => {
let (result, inserted) = self.terms_2.insert(SharedTermFixed {
symbol: SymbolRef::from_symbol(symbol),
args: [arg(0), arg(1)],
args: [arg(), arg()],
});
unsafe { (cast_to_shared_term_ptr(&result, 2), inserted) }
}
3 => {
let (result, inserted) = self.terms_3.insert(SharedTermFixed {
symbol: SymbolRef::from_symbol(symbol),
args: [arg(0), arg(1), arg(2)],
args: [arg(), arg(), arg()],
});
unsafe { (cast_to_shared_term_ptr(&result, 3), inserted) }
}
4 => {
let (result, inserted) = self.terms_4.insert(SharedTermFixed {
symbol: SymbolRef::from_symbol(symbol),
args: [arg(0), arg(1), arg(2), arg(3)],
args: [arg(), arg(), arg(), arg()],
});
unsafe { (cast_to_shared_term_ptr(&result, 4), inserted) }
}
5 => {
let (result, inserted) = self.terms_5.insert(SharedTermFixed {
symbol: SymbolRef::from_symbol(symbol),
args: [arg(0), arg(1), arg(2), arg(3), arg(4)],
args: [arg(), arg(), arg(), arg(), arg()],
});
unsafe { (cast_to_shared_term_ptr(&result, 5), inserted) }
}
6 => {
let (result, inserted) = self.terms_6.insert(SharedTermFixed {
symbol: SymbolRef::from_symbol(symbol),
args: [arg(0), arg(1), arg(2), arg(3), arg(4), arg(5)],
args: [arg(), arg(), arg(), arg(), arg(), arg()],
});
unsafe { (cast_to_shared_term_ptr(&result, 6), inserted) }
}
7 => {
let (result, inserted) = self.terms_7.insert(SharedTermFixed {
symbol: SymbolRef::from_symbol(symbol),
args: [arg(0), arg(1), arg(2), arg(3), arg(4), arg(5), arg(6)],
args: [arg(), arg(), arg(), arg(), arg(), arg(), arg()],
});
unsafe { (cast_to_shared_term_ptr(&result, 7), inserted) }
}
_ => {
let shared_term = SharedTermLookup {
symbol: SymbolRef::from_symbol(symbol),
arguments: args,
};

unsafe {
self.terms
.insert_equiv_dst(&shared_term, SharedTerm::length_for(&shared_term), |ptr, key| {
SharedTerm::construct(ptr, key)
})
}
}
}
arity => unreachable!("insert_fixed_iter called with arity {arity} > {MAX_FIXED_ARITY}"),
};

debug_assert!(
args.next().is_none(),
"The iterator yields more arguments than the arity of the symbol"
);
result
}

/// Inserts an integer term into the storage, returning a pointer to the stored term
Expand Down
5 changes: 2 additions & 3 deletions crates/aterm/src/storage/gc_mutex.rs
Original file line number Diff line number Diff line change
Expand Up @@ -10,12 +10,11 @@ use crate::storage::THREAD_TERM_POOL;
/// the [super::GlobalTermPool] for the duration of the guard's lifetime.
/// Returns a [GcMutexGuard] on access.
///
/// # Safety
/// # Panics
///
/// The `GcMutex` returns guards that are tied to the thread-local storage of
/// [crate::storage::THREAD_TERM_POOL]. This means that the guard must be
/// dropped before this thread-local storage is dropped. Otherwise
/// use-after-free will occur, which is undefined behaviour.
/// dropped before this thread-local storage is dropped, or it will panic.
pub(crate) struct GcMutex<T> {
inner: UnsafeCell<T>,
}
Expand Down
32 changes: 32 additions & 0 deletions crates/aterm/src/storage/global_aterm_pool.rs
Original file line number Diff line number Diff line change
Expand Up @@ -155,6 +155,38 @@ impl GlobalTermPool {
self.terms.insert(symbol, args)
}

/// Create a term of arity at most [crate::storage::aterm_storage::MAX_FIXED_ARITY] directly
/// from the given argument slice, without an intermediate `ATermRef` buffer.
///
/// Crate-private: the returned pointer is unprotected, see [Self::create_int].
pub(crate) fn create_term_fixed<'a, 'b, 'c, 'd, S, T>(
&self,
symbol: &'b S,
args: &[T],
) -> (StablePointer<SharedTerm>, bool)
where
S: Symb<'a, 'b>,
T: Term<'c, 'd>,
{
self.terms.insert_fixed(symbol, args)
}

/// Create a term of arity at most [crate::storage::aterm_storage::MAX_FIXED_ARITY] straight
/// from an iterator over argument indices, see [Self::create_term_fixed].
///
/// Crate-private: the returned pointer is unprotected, see [Self::create_int].
pub(crate) fn create_term_fixed_iter<'a, 'b, S, I>(
&self,
symbol: &'b S,
args: I,
) -> (StablePointer<SharedTerm>, bool)
where
S: Symb<'a, 'b>,
I: Iterator<Item = ATermIndex>,
{
self.terms.insert_fixed_iter(symbol, args)
}

/// Create a function symbol
///
/// Crate-private: `protect` receives an unprotected index, see [Self::create_int].
Expand Down
Loading
Loading