Skip to content

Overview

The merc_typecheck crate type checks mCRL2 data specifications, following the definitions in Modeling and Analysis of Communicating Systems (Groote & Mousavi, MIT Press 2014). A type checker turns the loosely-structured syntax tree produced by the parser into a fully typed specification: it resolves every name, decides the sort of every expression, chooses between overloaded operators, and inserts the implicit coercions that the surface language leaves out (such as reading a natural number where a real number is expected).

Rather than performing all of this in one recursive traversal, merc splits type checking into a pipeline of phases, each with a well-defined input and output. The architecture is query-based in the style of the Rust compiler: each derived fact — the signature of a specification, the sort denoted by a declaration, the typing of an equation — is a memoized query on a shared TypeckContext, so phases pull their dependencies lazily and every fact is computed at most once. Cyclic definitions (a sort alias that refers to itself, say) are detected through the memoization table's lock state instead of running away into unbounded recursion.

Is the per-query memoization worth its complexity?

Not a settled question. Several passes already walk the full AST to perform other syntactic operations, so it is not yet clear how much the per-query memoization saves over simply recomputing facts during one of those existing traversals, versus what it costs in bookkeeping.

The entry point is DataSpecification::from_untyped, which takes the untyped merc_syntax AST produced by the parser and runs the phases below.

Overview

The guiding idea is a split representation. During type checking sorts are interned indices into a standalone arena, so equality is a single integer comparison and typings live in compact side tables keyed by expression id. Only the final lowering phase produces the maximally shared aterm representation that the rest of merc (merc_sabre, merc_explore) consumes.

Contents

This part of the documentation is split one page per pass, plus one page per specification kind built on top of them:

  • Sort & Name Resolution — Phase 0: sort name resolution, alias-cycle checks, and canonicalization.
  • Desugaring — Phase 1: structured sorts to constructors/recognisers/projections, built-in operators to applications.
  • Signature & Well-Typedness — Phase 2: the triple and Definition 15.1.7's well-typedness conditions.
  • The System-Defined Specification — Appendix B's standard data types, why they're checked apart from the user's own declarations, and how a system equation is type checked against a deliberately narrower, group-scoped view of the polymorphic built-ins.
  • Source Maps, Imports & Virtual Templates — the shared SourceMap byte-offset space, %import file composition, and how generated system-defined content gets real, renderable declaration spans.
  • Type Variables & Polymorphic Schemes — the type_var block, ResolvedSort::Var, and how a scheme like in: S # List(S) -> Bool is resolved once and instantiated fresh at every use site.
  • Sort Inference — Phase 3: the sort lattice, constraint generation, unification with subtyping, and the ranked backtracking search — the heart of the crate.
  • Lowering — Phase 4: emitting aterms, binary-aterm compatibility, and the known divergences from the mCRL2 toolset.

Specification kinds built on the pipeline above:

  • Specification Type Checking — how ProcessSpecification, PbesSpecification, and PresSpecification each build on the data checker, collecting their own declarations and then type checking every expression.
  • Span-Keyed Typing Info (LSP Support) — the TypingInfo API that exposes typing facts by source Span for editor tooling.