Expand description
Public language and compiler-facing APIs.
These parser, lowering, projection, and code-generation entry points are supported and covered by strict operational verification gates, but they are intentionally outside the current formal-verification claim. The current claim is scoped to the Lean models/theorems plus the theorem-defined Rust↔Lean runtime correspondence surface, not to Rust compiler-pipeline correctness.
Re-exports§
pub use ast::AgreementProfileDeclaration;pub use ast::Choreography;pub use ast::Condition;pub use ast::DslAnnotationEntry;pub use ast::EffectInterfaceDeclaration;pub use ast::ExecutionProfileDeclaration;pub use ast::GuestRuntimeDeclaration;pub use ast::LanguageTier;pub use ast::LanguageTierStatus;pub use ast::LocalType;pub use ast::MessageType;pub use ast::OperationAgreementAttachment;pub use ast::OperationDeclaration;pub use ast::Protocol;pub use ast::RegionDeclaration;pub use ast::Role;pub use ast::RoleSetDeclaration;pub use ast::TheoremPackDeclaration;pub use ast::TopologyDeclaration;pub use ast::TypeDeclaration;pub use compiler::codegen::generate_choreography_code;pub use compiler::codegen::generate_choreography_code_with_annotations;pub use compiler::codegen::generate_choreography_code_with_dynamic_roles;pub use compiler::codegen::generate_choreography_code_with_extensions;pub use compiler::codegen::generate_choreography_code_with_namespacing;pub use compiler::codegen::generate_helpers;pub use compiler::codegen::generate_role_implementations;pub use compiler::codegen::generate_session_type;pub use compiler::parser::choreography_macro;pub use compiler::parser::collect_dsl_lints;pub use compiler::parser::explain_lowering;pub use compiler::parser::parse_choreography;pub use compiler::parser::parse_choreography_file;pub use compiler::parser::parse_choreography_str;pub use compiler::parser::parse_choreography_str_with_extensions;pub use compiler::parser::parse_dsl;pub use compiler::parser::render_lsp_lint_diagnostics;pub use compiler::parser::ErrorSpan;pub use compiler::parser::LintDiagnostic;pub use compiler::parser::LintLevel;pub use compiler::parser::ParseError;pub use compiler::parser::DEFAULT_SOURCE_EXTENSION;pub use compiler::projection::project;pub use compiler::projection::ProjectionError;pub use effect_spec::generate_effect_interface_scaffold;pub use effect_spec::generated_effect_families;pub use effect_spec::GeneratedEffectBehavior;pub use effect_spec::GeneratedEffectFamily;pub use effect_spec::GeneratedEffectOperation;pub use effect_spec::GeneratedSimulationMetadata;pub use effect_spec::GeneratedSimulationMode;pub use extensions::CodegenContext;pub use extensions::ExtensionRegistry;pub use extensions::ExtensionValidationError;pub use extensions::GrammarExtension;pub use extensions::ParseContext;pub use extensions::ParseError as ExtensionParseError;pub use extensions::ProjectionContext;pub use extensions::ProtocolExtension;pub use extensions::StatementParser;pub use integration::collect_choreography_annotation_records;pub use integration::collect_protocol_annotation_records;pub use integration::compile_choreography;pub use integration::compile_choreography_ast;pub use integration::AnnotationScope;pub use integration::CompileArtifactsError;pub use integration::CompiledChoreography;pub use integration::ProtocolAnnotationRecord;
Modules§
- ast
- Abstract Syntax Tree for choreographic protocols
- compiler
- Compiler pipeline: parsing, layout, projection, and codegen.
- effect_
spec - Effect handler scaffolding and simulation metadata generation.
- extensions
- DSL Extension System for Telltale
- integration
- Integration-oriented helpers built on top of the shared choreography frontend.
Macros§
- register_
extension - Convenience macro for registering extensions