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, ProtocolAnnotation};
50pub use choreography::{
51    AgreementProfileDeclaration, ChildEffectAggregation, ChildEffectAggregationPolicy,
52    Choreography, EffectAuthorityClass, EffectContractDeclaration, EffectInterfaceDeclaration,
53    EffectOperationDeclaration, ExecutionProfileDeclaration, GuestRuntimeDeclaration, LanguageTier,
54    LanguageTierStatus, OperationAgreementAttachment, OperationDeclaration,
55    OperationParameterDeclaration, ProgressAttachment, RegionDeclaration, RoleSetDeclaration,
56    TheoremPackDeclaration, TopologyDeclaration, TypeConstructorDeclaration, TypeDeclaration,
57};
58pub use execution_hints::{
59    ChoreographyWithHints, ExecutionHints, ExecutionHintsBuilder, OperationHints, OperationPath,
60    OperationStep,
61};
62pub use global_type::GlobalType; // Extended GlobalType with DSL features
63pub use local_type::LocalType; // Extended LocalType for code generation
64pub use message::MessageType;
65pub use non_empty::{NonEmptyError, NonEmptyVec};
66pub use protocol::{
67    AuthorityBindingMode, AuthorityExpr, Branch, CaseBranch, CasePattern, ChoiceGuard,
68    CommitmentOutcome, Condition, Protocol,
69};
70pub use role::{
71    RangeExpr, Role, RoleBoundsChecker, RoleIndex, RoleParam, RoleRange, RoleValidationError,
72    RoleValidationResult, MAX_RANGE_COUNT, MAX_ROLE_COUNT, MAX_ROLE_INDEX,
73};
74pub use validation::ValidationError;
75
76// Re-export conversion utilities
77pub use convert::{
78    choreography_to_global, local_to_local_r, local_types_equivalent, protocol_to_global,
79    ConversionError, ConversionResult,
80};
telltale_language/ast/mod.rs

telltale_language/ast/
mod.rs
