vertep_core/lib.rs
1//! Chart IR, validation and the pure SCXML step kernel for Vertep.
2//!
3//! `vertep-core` is `no_std` with `alloc` and has no I/O, no async and no clock: every
4//! interaction with the outside world is an effect returned by the step function.
5//!
6//! The pipeline is: build or read a [`ir::Chart`], give anonymous states identifiers with
7//! [`identity::assign_generated_ids`], compile it with [`compile::CompiledChart::new`] (which runs
8//! [`validate::validate`]), pick the datamodel with [`null::create_datamodel`], then call
9//! [`session::start`] once and [`session::step`] for every input. Wrap the datamodel in a
10//! [`tape::TapeDatamodel`] to record the answer tape for the Lean oracle.
11//!
12//! @tg: implements:: [[decisions#IR is the hub]]
13//! @tg: implements:: [[decisions#SCXML semantics are normative]]
14//! @tg: implements:: [[decisions#No-std core and tokio shell]]
15//! @tg: implements:: [[decisions#Pluggable datamodel]]
16
17#![cfg_attr(not(feature = "std"), no_std)]
18
19extern crate alloc;
20
21#[cfg(doctest)]
22#[doc = include_str!("../README.md")]
23struct ReadmeDoctests;
24
25pub mod bitset;
26pub mod compile;
27pub mod datamodel;
28pub mod identity;
29pub mod ir;
30pub mod kernel;
31pub mod null;
32pub mod order;
33pub mod session;
34pub mod tape;
35pub mod trace;
36pub mod types;
37pub mod validate;
38
39#[cfg(test)]
40mod tests;