telltale_language/ast/
mod.rs

1//! Abstract Syntax Tree for choreographic protocols
2//!
3//! This module defines the core AST types used to represent choreographic protocols,
4//! including global protocols, local (projected) types, roles, and messages.
5//!
6//! Core types (GlobalType, LocalTypeR, Label, PayloadSort) are re-exported from
7//! `telltale-types` for Lean correspondence. Extended types (LocalType, Protocol)
8//! are defined here for DSL-specific features.
9
10/// Typed protocol annotations
11pub mod annotation;
12
13/// Choreography definitions (global protocols with metadata)
14pub mod choreography;
15
16/// Execution hints for code generation (deployment-level concerns)
17pub mod execution_hints;
18
19/// Conversion utilities between DSL types and theory types
20pub mod convert;
21
22/// Global types for multiparty session type protocols (extended, uses telltale-types)
23pub mod global_type;
24
25/// Local types resulting from projection (extended, uses telltale-types)
26pub mod local_type;
27
28/// Message type definitions
29pub mod message;
30
31/// Non-empty collection utilities
32pub mod non_empty;
33
34/// Protocol combinators (global protocol constructs)
35pub mod protocol;
36
37/// Role definitions
38pub mod role;
39
40/// Validation errors and utilities
41pub mod validation;
42
43// Re-export core types from telltale-types for Lean correspondence
44pub use telltale_types::{
45    Action, GlobalType as GlobalTypeCore, Label, LocalAction, LocalTypeR, PayloadSort,
46};
47
48// Re-export DSL-specific types
49pub use annotation::{Annotations, DslAnnotationEntry, ProtocolAnnotation};
50pub use choreography::{
51    AgreementProfileDeclaration, AuthorityMetatheoryStatus, AuthorityMetatheoryTier,
52    ChildEffectAggregation, ChildEffectAggregationPolicy, Choreography, EffectAuthorityClass,
53    EffectContractDeclaration, EffectInterfaceDeclaration, EffectOperationDeclaration,
54    ExecutionProfileDeclaration, GuestRuntimeDeclaration, LanguageTier, LanguageTierStatus,
55    OperationAgreementAttachment, OperationDeclaration, OperationParameterDeclaration,
56    ProgressAttachment, RegionDeclaration, RoleSetDeclaration, TheoremPackDeclaration,
57    TopologyDeclaration, TypeConstructorDeclaration, TypeDeclaration,
58};
59pub use execution_hints::{
60    ChoreographyWithHints, ExecutionHints, ExecutionHintsBuilder, OperationHints, OperationPath,
61    OperationStep,
62};
63pub use global_type::GlobalType; // Extended GlobalType with DSL features
64pub use local_type::LocalType; // Extended LocalType for code generation
65pub use message::MessageType;
66pub use non_empty::{NonEmptyError, NonEmptyVec};
67pub use protocol::{
68    AuthorityBindingMode, AuthorityExpr, Branch, CaseBranch, CasePattern, ChoiceGuard,
69    CommitmentOutcome, Condition, Protocol,
70};
71pub use role::{
72    RangeExpr, Role, RoleBoundsChecker, RoleIndex, RoleParam, RoleRange, RoleValidationError,
73    RoleValidationResult, MAX_RANGE_COUNT, MAX_ROLE_COUNT, MAX_ROLE_INDEX,
74};
75pub use validation::ValidationError;
76
77// Re-export conversion utilities
78pub use convert::{
79    choreography_to_global, local_to_local_r, local_types_equivalent, protocol_to_global,
80    ConversionError, ConversionResult,
81};
telltale_language/ast/mod.rs

telltale_language/ast/
mod.rs
