telltale_language/
lib.rs

1#![allow(
2    clippy::missing_errors_doc,
3    clippy::missing_panics_doc,
4    clippy::must_use_candidate
5)]
6#![cfg_attr(not(test), deny(clippy::unwrap_used, clippy::expect_used))]
7
8//! Public language and compiler-facing APIs.
9//!
10//! These parser, lowering, projection, and code-generation entry points are
11//! supported and covered by strict operational verification gates, but they are
12//! intentionally outside the current formal-verification claim. The current
13//! claim is scoped to the Lean models/theorems plus the theorem-defined Rust↔Lean
14//! runtime correspondence surface, not to Rust compiler-pipeline correctness.
15
16pub mod ast;
17pub mod compiler;
18pub mod effect_spec;
19pub mod extensions;
20pub mod integration;
21mod module_codegen;
22
23pub use ast::{
24    AgreementProfileDeclaration, Choreography, Condition, DslAnnotationEntry,
25    EffectInterfaceDeclaration, ExecutionProfileDeclaration, GuestRuntimeDeclaration, LanguageTier,
26    LanguageTierStatus, LocalType, MessageType, OperationAgreementAttachment, OperationDeclaration,
27    Protocol, RegionDeclaration, Role, RoleSetDeclaration, TheoremPackDeclaration,
28    TopologyDeclaration, TypeDeclaration,
29};
30pub use compiler::codegen::{
31    generate_choreography_code, generate_choreography_code_with_annotations,
32    generate_choreography_code_with_dynamic_roles, generate_choreography_code_with_extensions,
33    generate_choreography_code_with_namespacing, generate_helpers, generate_role_implementations,
34    generate_session_type,
35};
36pub use compiler::parser::{
37    choreography_macro, collect_dsl_lints, explain_lowering, parse_choreography,
38    parse_choreography_file, parse_choreography_str, parse_choreography_str_with_extensions,
39    parse_dsl, render_lsp_lint_diagnostics, ErrorSpan, LintDiagnostic, LintLevel, ParseError,
40    DEFAULT_SOURCE_EXTENSION,
41};
42pub use compiler::projection::{project, ProjectionError};
43pub use effect_spec::{
44    generate_effect_interface_scaffold, generated_effect_families, GeneratedEffectBehavior,
45    GeneratedEffectFamily, GeneratedEffectOperation, GeneratedSimulationMetadata,
46    GeneratedSimulationMode,
47};
48pub use extensions::{
49    CodegenContext, ExtensionRegistry, ExtensionValidationError, GrammarExtension, ParseContext,
50    ParseError as ExtensionParseError, ProjectionContext, ProtocolExtension, StatementParser,
51};
52pub use integration::{
53    collect_choreography_annotation_records, collect_protocol_annotation_records,
54    compile_choreography, compile_choreography_ast, AnnotationScope, CompileArtifactsError,
55    CompiledChoreography, ProtocolAnnotationRecord,
56};
57pub use module_codegen::generate_protocol_module;
telltale_language/lib.rs

telltale_language/
lib.rs
