panproto_gat/
alg_struct.rs

1//! Algebraic struct types for theories.
2//!
3//! An `AlgStruct` declares a record type within a theory, with named
4//! fields typed by the theory's sorts. This enables schemas to be
5//! modeled as algebraic objects within the theory framework.
6
7use std::sync::Arc;
8
9use serde::{Deserialize, Serialize};
10
11/// An algebraic struct type declared within a theory.
12#[derive(Debug, Clone, PartialEq, Eq, Hash, Serialize, Deserialize)]
13pub struct AlgStruct {
14    /// The struct type name.
15    pub name: Arc<str>,
16    /// Type parameters.
17    pub params: Vec<StructParam>,
18    /// Named fields.
19    pub fields: Vec<StructField>,
20}
21
22/// A type parameter of an algebraic struct.
23#[derive(Debug, Clone, PartialEq, Eq, Hash, Serialize, Deserialize)]
24pub struct StructParam {
25    /// The parameter name.
26    pub name: Arc<str>,
27    /// The sort this parameter ranges over.
28    pub sort: Arc<str>,
29}
30
31/// A field of an algebraic struct.
32#[derive(Debug, Clone, PartialEq, Eq, Hash, Serialize, Deserialize)]
33pub struct StructField {
34    /// The field name.
35    pub name: Arc<str>,
36    /// The sort of values in this field.
37    pub sort: Arc<str>,
38    /// Whether this field is optional.
39    pub optional: bool,
40}
41
42impl AlgStruct {
43    /// Create a new algebraic struct with the given name and no parameters or fields.
44    #[must_use]
45    pub fn new(name: impl Into<Arc<str>>) -> Self {
46        Self {
47            name: name.into(),
48            params: Vec::new(),
49            fields: Vec::new(),
50        }
51    }
52
53    /// Add a type parameter.
54    #[must_use]
55    pub fn with_param(mut self, name: impl Into<Arc<str>>, sort: impl Into<Arc<str>>) -> Self {
56        self.params.push(StructParam {
57            name: name.into(),
58            sort: sort.into(),
59        });
60        self
61    }
62
63    /// Add a required field.
64    #[must_use]
65    pub fn with_field(mut self, name: impl Into<Arc<str>>, sort: impl Into<Arc<str>>) -> Self {
66        self.fields.push(StructField {
67            name: name.into(),
68            sort: sort.into(),
69            optional: false,
70        });
71        self
72    }
73
74    /// Add an optional field.
75    #[must_use]
76    pub fn with_optional_field(
77        mut self,
78        name: impl Into<Arc<str>>,
79        sort: impl Into<Arc<str>>,
80    ) -> Self {
81        self.fields.push(StructField {
82            name: name.into(),
83            sort: sort.into(),
84            optional: true,
85        });
86        self
87    }
88
89    /// Return the number of required (non-optional) fields.
90    #[must_use]
91    pub fn required_field_count(&self) -> usize {
92        self.fields.iter().filter(|f| !f.optional).count()
93    }
94}
95
96#[cfg(test)]
97#[allow(clippy::unwrap_used, clippy::expect_used)]
98mod tests {
99    use super::*;
100
101    #[test]
102    fn build_struct_with_builder() {
103        let s = AlgStruct::new("Person")
104            .with_param("T", "Type")
105            .with_field("name", "string")
106            .with_field("age", "int")
107            .with_optional_field("email", "string");
108
109        assert_eq!(&*s.name, "Person");
110        assert_eq!(s.params.len(), 1);
111        assert_eq!(s.fields.len(), 3);
112        assert_eq!(s.required_field_count(), 2);
113    }
114
115    #[test]
116    fn empty_struct() {
117        let s = AlgStruct::new("Unit");
118        assert!(s.params.is_empty());
119        assert!(s.fields.is_empty());
120        assert_eq!(s.required_field_count(), 0);
121    }
122
123    /// An `AlgStruct` whose fields share names with its declared
124    /// parameters is plain data: construction does not register
125    /// anything globally, so name overlap is inert and round-trips
126    /// through serde unchanged.
127    #[test]
128    fn alg_struct_with_name_overlap_between_fields_and_params_is_inert() {
129        // Shape deliberately chosen to make every identifier coincide:
130        // a struct named "Self" with a param "Self" : Type and two
131        // fields that reuse the param name and the struct name.
132        let s = AlgStruct::new("Self")
133            .with_param("Self", "Type")
134            .with_field("Self", "Type")
135            .with_field("value", "Self");
136        assert_eq!(&*s.name, "Self");
137        assert_eq!(s.params.len(), 1);
138        assert_eq!(s.fields.len(), 2);
139
140        // Round-trip survives the clash without panic.
141        let json = serde_json::to_string(&s).expect("serialize");
142        let back: AlgStruct = serde_json::from_str(&json).expect("deserialize");
143        assert_eq!(s, back);
144    }
145
146    #[test]
147    fn serialization_round_trip() {
148        let s = AlgStruct::new("Pair")
149            .with_param("A", "Sort")
150            .with_param("B", "Sort")
151            .with_field("fst", "A")
152            .with_field("snd", "B");
153
154        let json = serde_json::to_string(&s).expect("serialize");
155        let deserialized: AlgStruct = serde_json::from_str(&json).expect("deserialize");
156        assert_eq!(s, deserialized);
157    }
158}
panproto_gat/alg_struct.rs

panproto_gat/
alg_struct.rs
