fastbreak/model/
spec.rs

1//! Compiled specification model
2//!
3//! This module defines the fully resolved specification model that is ready
4//! for code generation, documentation, and verification.
5
6use crate::ast::{Attribute, AttributeArg};
7use crate::semantic::{ActionInfo, EnumInfo, RelationInfo, StateInfo, StructInfo, Type};
8use crate::Span;
9use indexmap::IndexMap;
10use smol_str::SmolStr;
11use std::sync::Arc;
12
13/// A compiled attribute
14#[derive(Debug, Clone)]
15pub struct CompiledAttribute {
16    /// Attribute name
17    pub name: SmolStr,
18    /// Attribute arguments
19    pub args: Vec<CompiledAttributeArg>,
20}
21
22/// A compiled attribute argument
23#[derive(Debug, Clone)]
24pub enum CompiledAttributeArg {
25    /// String value
26    String(SmolStr),
27    /// Identifier value
28    Ident(SmolStr),
29    /// Integer value
30    Int(i64),
31}
32
33impl CompiledAttribute {
34    /// Create from AST `Attribute`
35    #[must_use]
36    pub fn from_ast(attr: &Attribute) -> Self {
37        Self {
38            name: attr.name.name.clone(),
39            args: attr.args.iter().map(CompiledAttributeArg::from_ast).collect(),
40        }
41    }
42
43    /// Get the first argument as a string if it exists
44    #[must_use]
45    pub fn first_arg_string(&self) -> Option<&str> {
46        self.args.first().and_then(|arg| match arg {
47            CompiledAttributeArg::String(s) | CompiledAttributeArg::Ident(s) => Some(s.as_str()),
48            CompiledAttributeArg::Int(_) => None,
49        })
50    }
51}
52
53impl CompiledAttributeArg {
54    /// Create from AST `AttributeArg`
55    #[must_use]
56    pub fn from_ast(arg: &AttributeArg) -> Self {
57        match arg {
58            AttributeArg::String(s, _) => CompiledAttributeArg::String(s.clone()),
59            AttributeArg::Ident(ident) => CompiledAttributeArg::Ident(ident.name.clone()),
60            AttributeArg::Int(n, _) => CompiledAttributeArg::Int(*n),
61        }
62    }
63}
64
65impl std::fmt::Display for CompiledAttributeArg {
66    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
67        match self {
68            CompiledAttributeArg::String(s) => write!(f, "\"{s}\""),
69            CompiledAttributeArg::Ident(s) => write!(f, "{s}"),
70            CompiledAttributeArg::Int(n) => write!(f, "{n}"),
71        }
72    }
73}
74
75/// A fully compiled and resolved specification
76#[derive(Debug, Clone)]
77pub struct CompiledSpec {
78    /// Module name (if any)
79    pub module: Option<SmolStr>,
80    /// Imports from other modules
81    pub imports: Vec<Import>,
82    /// User-defined struct types
83    pub structs: IndexMap<SmolStr, CompiledStruct>,
84    /// Type aliases (e.g., `type PositiveInt = Int where self > 0`)
85    pub type_aliases: IndexMap<SmolStr, CompiledTypeAlias>,
86    /// User-defined enum types
87    pub enums: IndexMap<SmolStr, CompiledEnum>,
88    /// State definitions
89    pub states: IndexMap<SmolStr, CompiledState>,
90    /// Action definitions
91    pub actions: IndexMap<SmolStr, CompiledAction>,
92    /// Relation definitions
93    pub relations: IndexMap<SmolStr, CompiledRelation>,
94    /// Scenario definitions
95    pub scenarios: Vec<CompiledScenario>,
96    /// Property definitions
97    pub properties: Vec<CompiledProperty>,
98    /// Quality requirements (non-functional requirements)
99    pub qualities: Vec<CompiledQuality>,
100}
101
102impl CompiledSpec {
103    /// Create a new empty compiled specification
104    #[must_use]
105    pub fn new() -> Self {
106        Self {
107            module: None,
108            imports: Vec::new(),
109            structs: IndexMap::new(),
110            type_aliases: IndexMap::new(),
111            enums: IndexMap::new(),
112            states: IndexMap::new(),
113            actions: IndexMap::new(),
114            relations: IndexMap::new(),
115            scenarios: Vec::new(),
116            properties: Vec::new(),
117            qualities: Vec::new(),
118        }
119    }
120
121    /// Check if the specification is empty
122    #[must_use]
123    pub fn is_empty(&self) -> bool {
124        self.structs.is_empty()
125            && self.type_aliases.is_empty()
126            && self.enums.is_empty()
127            && self.states.is_empty()
128            && self.actions.is_empty()
129            && self.relations.is_empty()
130            && self.scenarios.is_empty()
131            && self.properties.is_empty()
132            && self.qualities.is_empty()
133    }
134
135    /// Get the total number of definitions
136    #[must_use]
137    pub fn definition_count(&self) -> usize {
138        self.structs.len()
139            + self.type_aliases.len()
140            + self.enums.len()
141            + self.states.len()
142            + self.actions.len()
143            + self.relations.len()
144    }
145}
146
147impl Default for CompiledSpec {
148    fn default() -> Self {
149        Self::new()
150    }
151}
152
153/// An import statement
154#[derive(Debug, Clone)]
155pub struct Import {
156    /// The module path being imported
157    pub path: Vec<SmolStr>,
158    /// Specific items being imported (empty means import all)
159    pub items: Vec<SmolStr>,
160    /// Source span
161    pub span: Span,
162}
163
164/// A compiled struct type
165#[derive(Debug, Clone)]
166pub struct CompiledStruct {
167    /// Struct name
168    pub name: SmolStr,
169    /// Type parameters
170    pub type_params: Vec<SmolStr>,
171    /// Fields with their resolved types
172    pub fields: IndexMap<SmolStr, Type>,
173    /// Refinement predicate (optional)
174    pub refinement: Option<Arc<crate::ast::Expr>>,
175    /// Attributes
176    pub attributes: Vec<CompiledAttribute>,
177    /// Documentation comment
178    pub doc: Option<String>,
179    /// Source span
180    pub span: Span,
181}
182
183/// A compiled type alias
184#[derive(Debug, Clone)]
185pub struct CompiledTypeAlias {
186    /// Alias name
187    pub name: SmolStr,
188    /// Type parameters
189    pub type_params: Vec<SmolStr>,
190    /// The underlying base type
191    pub base: Type,
192    /// Refinement predicate (optional)
193    pub refinement: Option<Arc<crate::ast::Expr>>,
194    /// Attributes
195    pub attributes: Vec<CompiledAttribute>,
196    /// Documentation comment
197    pub doc: Option<String>,
198    /// Source span
199    pub span: Span,
200}
201
202impl CompiledStruct {
203    /// Create from semantic `StructInfo`
204    #[must_use]
205    pub fn from_info(
206        info: &StructInfo,
207        refinement: Option<Arc<crate::ast::Expr>>,
208        attributes: Vec<CompiledAttribute>,
209        span: Span,
210    ) -> Self {
211        Self {
212            name: info.id.name.clone(),
213            type_params: info.type_params.clone(),
214            fields: info.fields.clone(),
215            refinement,
216            attributes,
217            doc: None,
218            span,
219        }
220    }
221}
222
223/// A compiled enum type
224#[derive(Debug, Clone)]
225pub struct CompiledEnum {
226    /// Enum name
227    pub name: SmolStr,
228    /// Type parameters
229    pub type_params: Vec<SmolStr>,
230    /// Variants
231    pub variants: IndexMap<SmolStr, CompiledVariant>,
232    /// Attributes
233    pub attributes: Vec<CompiledAttribute>,
234    /// Documentation comment
235    pub doc: Option<String>,
236    /// Source span
237    pub span: Span,
238}
239
240impl CompiledEnum {
241    /// Create from semantic `EnumInfo`
242    #[must_use]
243    pub fn from_info(info: &EnumInfo, attributes: Vec<CompiledAttribute>, span: Span) -> Self {
244        let variants = info
245            .variants
246            .iter()
247            .map(|(name, v)| {
248                (
249                    name.clone(),
250                    CompiledVariant {
251                        name: v.name.clone(),
252                        fields: v.fields.clone(),
253                        is_tuple: v.is_tuple,
254                    },
255                )
256            })
257            .collect();
258
259        Self {
260            name: info.id.name.clone(),
261            type_params: info.type_params.clone(),
262            variants,
263            attributes,
264            doc: None,
265            span,
266        }
267    }
268}
269
270/// A compiled enum variant
271#[derive(Debug, Clone)]
272pub struct CompiledVariant {
273    /// Variant name
274    pub name: SmolStr,
275    /// Fields (named or positional)
276    pub fields: IndexMap<SmolStr, Type>,
277    /// Whether this is a tuple variant
278    pub is_tuple: bool,
279}
280
281impl CompiledVariant {
282    /// Check if this is a unit variant (no fields)
283    #[must_use]
284    pub fn is_unit(&self) -> bool {
285        self.fields.is_empty()
286    }
287}
288
289/// A compiled state definition
290#[derive(Debug, Clone)]
291pub struct CompiledState {
292    /// State name
293    pub name: SmolStr,
294    /// State fields with their resolved types
295    pub fields: IndexMap<SmolStr, Type>,
296    /// State invariants
297    pub invariants: Vec<CompiledInvariant>,
298    /// Attributes
299    pub attributes: Vec<CompiledAttribute>,
300    /// Documentation comment
301    pub doc: Option<String>,
302    /// Source span
303    pub span: Span,
304}
305
306impl CompiledState {
307    /// Create from semantic `StateInfo`
308    #[must_use]
309    pub fn from_info(info: &StateInfo, attributes: Vec<CompiledAttribute>, span: Span) -> Self {
310        Self {
311            name: info.name.clone(),
312            fields: info.fields.clone(),
313            invariants: Vec::new(),
314            attributes,
315            doc: None,
316            span,
317        }
318    }
319}
320
321/// A compiled invariant
322#[derive(Debug, Clone)]
323pub struct CompiledInvariant {
324    /// Invariant name/description
325    pub name: Option<String>,
326    /// The invariant expression (stored as AST for now)
327    pub expr: Arc<crate::ast::Expr>,
328    /// Source span
329    pub span: Span,
330}
331
332/// A compiled action definition
333#[derive(Debug, Clone)]
334pub struct CompiledAction {
335    /// Action name
336    pub name: SmolStr,
337    /// Parameters with their types
338    pub params: IndexMap<SmolStr, Type>,
339    /// Return type
340    pub return_type: Type,
341    /// Preconditions (requires clauses)
342    pub requires: Vec<CompiledContract>,
343    /// Postconditions (ensures clauses)
344    pub ensures: Vec<CompiledContract>,
345    /// Attributes
346    pub attributes: Vec<CompiledAttribute>,
347    /// Documentation comment
348    pub doc: Option<String>,
349    /// Source span
350    pub span: Span,
351}
352
353impl CompiledAction {
354    /// Create from semantic `ActionInfo`
355    #[must_use]
356    pub fn from_info(info: &ActionInfo, attributes: Vec<CompiledAttribute>, span: Span) -> Self {
357        Self {
358            name: info.name.clone(),
359            params: info.params.clone(),
360            return_type: info.return_type.clone(),
361            requires: Vec::new(),
362            ensures: Vec::new(),
363            attributes,
364            doc: None,
365            span,
366        }
367    }
368}
369
370/// A compiled contract (requires/ensures clause)
371#[derive(Debug, Clone)]
372pub struct CompiledContract {
373    /// The contract expression
374    pub expr: Arc<crate::ast::Expr>,
375    /// Source span
376    pub span: Span,
377}
378
379/// A compiled relation definition
380#[derive(Debug, Clone)]
381pub struct CompiledRelation {
382    /// Relation name
383    pub name: SmolStr,
384    /// Source type
385    pub source: Type,
386    /// Target type
387    pub target: Type,
388    /// Relation properties
389    pub properties: Vec<RelationProperty>,
390    /// Attributes
391    pub attributes: Vec<CompiledAttribute>,
392    /// Documentation comment
393    pub doc: Option<String>,
394    /// Source span
395    pub span: Span,
396}
397
398impl CompiledRelation {
399    /// Create from semantic `RelationInfo`
400    #[must_use]
401    pub fn from_info(info: &RelationInfo, attributes: Vec<CompiledAttribute>, span: Span) -> Self {
402        Self {
403            name: info.name.clone(),
404            source: info.source.clone(),
405            target: info.target.clone(),
406            properties: Vec::new(),
407            attributes,
408            doc: None,
409            span,
410        }
411    }
412}
413
414/// A relation property constraint
415#[derive(Debug, Clone, Copy, PartialEq, Eq)]
416pub enum RelationProperty {
417    /// The relation is symmetric (a->b implies b->a)
418    Symmetric,
419    /// The relation is reflexive (a->a for all a)
420    Reflexive,
421    /// The relation is irreflexive (never a->a)
422    Irreflexive,
423    /// The relation is transitive (a->b and b->c implies a->c)
424    Transitive,
425    /// The relation is antisymmetric (a->b and b->a implies a=b)
426    Antisymmetric,
427}
428
429/// A compiled scenario
430#[derive(Debug, Clone)]
431pub struct CompiledScenario {
432    /// Scenario name/description
433    pub name: String,
434    /// Given clauses (initial state setup)
435    pub given: Vec<CompiledGiven>,
436    /// When clauses (actions to perform)
437    pub when: Vec<CompiledWhen>,
438    /// Then clauses (expected outcomes)
439    pub then: Vec<CompiledThen>,
440    /// Alternative flows (error cases, extensions)
441    pub alternatives: Vec<CompiledAlternative>,
442    /// Attributes
443    pub attributes: Vec<CompiledAttribute>,
444    /// Documentation comment
445    pub doc: Option<String>,
446    /// Source span
447    pub span: Span,
448}
449
450/// A compiled alternative flow
451#[derive(Debug, Clone)]
452pub struct CompiledAlternative {
453    /// Alternative name/description
454    pub name: String,
455    /// Condition that triggers this alternative (optional)
456    pub condition: Option<Arc<crate::ast::Expr>>,
457    /// Additional given bindings (optional, extends base)
458    pub given: Option<CompiledGiven>,
459    /// Different when clause (optional, replaces base)
460    pub when: Option<CompiledWhen>,
461    /// Expected outcome (required)
462    pub then: CompiledThen,
463    /// Attributes
464    pub attributes: Vec<CompiledAttribute>,
465    /// Source span
466    pub span: Span,
467}
468
469/// A compiled given clause
470#[derive(Debug, Clone)]
471pub struct CompiledGiven {
472    /// Assignments in the given clause
473    pub assignments: Vec<CompiledAssignment>,
474    /// Source span
475    pub span: Span,
476}
477
478/// A compiled when clause
479#[derive(Debug, Clone)]
480pub struct CompiledWhen {
481    /// Actions/expressions in the when clause
482    pub actions: Vec<CompiledWhenAction>,
483    /// Source span
484    pub span: Span,
485}
486
487/// An action in a when clause
488#[derive(Debug, Clone)]
489pub struct CompiledWhenAction {
490    /// Optional result binding
491    pub binding: Option<SmolStr>,
492    /// The action expression
493    pub expr: Arc<crate::ast::Expr>,
494    /// Source span
495    pub span: Span,
496}
497
498/// A compiled then clause
499#[derive(Debug, Clone)]
500pub struct CompiledThen {
501    /// Assertions in the then clause
502    pub assertions: Vec<CompiledAssertion>,
503    /// Source span
504    pub span: Span,
505}
506
507/// An assignment in a given clause
508#[derive(Debug, Clone)]
509pub struct CompiledAssignment {
510    /// The variable being assigned
511    pub name: SmolStr,
512    /// The value expression
513    pub value: Arc<crate::ast::Expr>,
514    /// Source span
515    pub span: Span,
516}
517
518/// An assertion in a then clause
519#[derive(Debug, Clone)]
520pub struct CompiledAssertion {
521    /// The assertion expression
522    pub expr: Arc<crate::ast::Expr>,
523    /// Source span
524    pub span: Span,
525}
526
527/// A compiled property
528#[derive(Debug, Clone)]
529pub struct CompiledProperty {
530    /// Property name/description
531    pub name: String,
532    /// The property expression
533    pub expr: Arc<crate::ast::Expr>,
534    /// Temporal operator (if any)
535    pub temporal: Option<TemporalOp>,
536    /// Attributes
537    pub attributes: Vec<CompiledAttribute>,
538    /// Documentation comment
539    pub doc: Option<String>,
540    /// Source span
541    pub span: Span,
542}
543
544/// Temporal operators for properties
545#[derive(Debug, Clone, Copy, PartialEq, Eq)]
546pub enum TemporalOp {
547    /// The property always holds
548    Always,
549    /// The property eventually holds
550    Eventually,
551    /// The property holds until another property holds
552    Until,
553    /// The property holds in the next state
554    Next,
555}
556
557/// A compiled quality requirement (non-functional requirement)
558#[derive(Debug, Clone)]
559pub struct CompiledQuality {
560    /// Quality category (performance, reliability, etc.)
561    pub category: QualityCategory,
562    /// Description/name of the quality requirement
563    pub description: SmolStr,
564    /// Metric being measured
565    pub metric: SmolStr,
566    /// Target value as formatted string
567    pub target: String,
568    /// Additional properties
569    pub properties: Vec<CompiledQualityProperty>,
570    /// Attributes
571    pub attributes: Vec<CompiledAttribute>,
572    /// Source span
573    pub span: Span,
574}
575
576/// Quality category
577#[derive(Debug, Clone, Copy, PartialEq, Eq)]
578pub enum QualityCategory {
579    /// Performance requirements (latency, throughput)
580    Performance,
581    /// Reliability requirements (uptime, MTBF)
582    Reliability,
583    /// Security requirements (encryption, authentication)
584    Security,
585    /// Usability requirements (accessibility, learnability)
586    Usability,
587    /// Scalability requirements (capacity, elasticity)
588    Scalability,
589    /// Maintainability requirements (testability, modularity)
590    Maintainability,
591}
592
593impl std::fmt::Display for QualityCategory {
594    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
595        match self {
596            QualityCategory::Performance => write!(f, "Performance"),
597            QualityCategory::Reliability => write!(f, "Reliability"),
598            QualityCategory::Security => write!(f, "Security"),
599            QualityCategory::Usability => write!(f, "Usability"),
600            QualityCategory::Scalability => write!(f, "Scalability"),
601            QualityCategory::Maintainability => write!(f, "Maintainability"),
602        }
603    }
604}
605
606/// Additional property for a quality requirement
607#[derive(Debug, Clone)]
608pub struct CompiledQualityProperty {
609    /// Property name
610    pub name: SmolStr,
611    /// Property value as formatted string
612    pub value: String,
613}
fastbreak/model/spec.rs

fastbreak/model/
spec.rs
