telltale-language 17.0.0

Shared choreography frontend for Telltale DSL parsing, projection, and macro code generation
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81

//! Abstract Syntax Tree for choreographic protocols
//!
//! This module defines the core AST types used to represent choreographic protocols,
//! including global protocols, local (projected) types, roles, and messages.
//!
//! Core types (GlobalType, LocalTypeR, Label, PayloadSort) are re-exported from
//! `telltale-types` for Lean correspondence. Extended types (LocalType, Protocol)
//! are defined here for DSL-specific features.

/// Typed protocol annotations
pub mod annotation;

/// Choreography definitions (global protocols with metadata)
pub mod choreography;

/// Execution hints for code generation (deployment-level concerns)
pub mod execution_hints;

/// Conversion utilities between DSL types and theory types
pub mod convert;

/// Global types for multiparty session type protocols (extended, uses telltale-types)
pub mod global_type;

/// Local types resulting from projection (extended, uses telltale-types)
pub mod local_type;

/// Message type definitions
pub mod message;

/// Non-empty collection utilities
pub mod non_empty;

/// Protocol combinators (global protocol constructs)
pub mod protocol;

/// Role definitions
pub mod role;

/// Validation errors and utilities
pub mod validation;

// Re-export core types from telltale-types for Lean correspondence
pub use telltale_types::{
    Action, GlobalType as GlobalTypeCore, Label, LocalAction, LocalTypeR, PayloadSort,
};

// Re-export DSL-specific types
pub use annotation::{Annotations, DslAnnotationEntry, ProtocolAnnotation};
pub use choreography::{
    AgreementProfileDeclaration, AuthorityMetatheoryStatus, AuthorityMetatheoryTier,
    ChildEffectAggregation, ChildEffectAggregationPolicy, Choreography, EffectAuthorityClass,
    EffectContractDeclaration, EffectInterfaceDeclaration, EffectOperationDeclaration,
    ExecutionProfileDeclaration, GuestRuntimeDeclaration, LanguageTier, LanguageTierStatus,
    OperationAgreementAttachment, OperationDeclaration, OperationParameterDeclaration,
    ProgressAttachment, RegionDeclaration, RoleSetDeclaration, TheoremPackDeclaration,
    TopologyDeclaration, TypeConstructorDeclaration, TypeDeclaration,
};
pub use execution_hints::{
    ChoreographyWithHints, ExecutionHints, ExecutionHintsBuilder, OperationHints, OperationPath,
    OperationStep,
};
pub use global_type::GlobalType; // Extended GlobalType with DSL features
pub use local_type::LocalType; // Extended LocalType for code generation
pub use message::MessageType;
pub use non_empty::{NonEmptyError, NonEmptyVec};
pub use protocol::{
    AuthorityBindingMode, AuthorityExpr, Branch, CaseBranch, CasePattern, ChoiceGuard,
    CommitmentOutcome, Condition, Protocol,
};
pub use role::{
    RangeExpr, Role, RoleBoundsChecker, RoleIndex, RoleParam, RoleRange, RoleValidationError,
    RoleValidationResult, MAX_RANGE_COUNT, MAX_ROLE_COUNT, MAX_ROLE_INDEX,
};
pub use validation::ValidationError;

// Re-export conversion utilities
pub use convert::{
    choreography_to_global, local_to_local_r, local_types_equivalent, protocol_to_global,
    ConversionError, ConversionResult,
};