tla_eval/
value.rs

1use std::collections::{BTreeMap, BTreeSet};
2use std::fmt;
3
4/// A TLA+ value.
5///
6/// Sequences, records and functions are all functions in TLA+, and the same
7/// value must not have two representations or equality would depend on how it
8/// was written. [`Value::function`] is the only way to build one, and it picks
9/// the representation from the domain: `1..n` gives a sequence, all-string
10/// gives a record, anything else stays a general function.
11#[derive(Debug, Clone, PartialEq, Eq, PartialOrd, Ord)]
12pub enum Value {
13    Bool(bool),
14    Int(i64),
15    Str(String),
16    Seq(Vec<Value>),
17    Set(BTreeSet<Value>),
18    Record(BTreeMap<String, Value>),
19    Func(BTreeMap<Value, Value>),
20    /// A set too large to enumerate. Membership is decidable; iteration is not.
21    Infinite(Infinite),
22}
23
24#[derive(Debug, Clone, PartialEq, Eq, PartialOrd, Ord)]
25pub enum Infinite {
26    Nat,
27    Int,
28    Strings,
29    /// `Seq(S)` — every finite sequence over `S`.
30    Sequences(Box<Value>),
31}
32
33/// A length or cardinality as a TLA+ integer. No collection can hold more than
34/// `isize::MAX` elements, so this never loses information.
35pub(crate) fn count(n: usize) -> i64 {
36    i64::try_from(n).expect("no collection exceeds isize::MAX elements")
37}
38
39impl Value {
40    pub fn set(items: impl IntoIterator<Item = Value>) -> Value {
41        Value::Set(items.into_iter().collect())
42    }
43
44    pub fn string(s: impl Into<String>) -> Value {
45        Value::Str(s.into())
46    }
47
48    pub fn interval(lo: i64, hi: i64) -> Value {
49        Value::Set((lo..=hi).map(Value::Int).collect())
50    }
51
52    pub fn record(fields: impl IntoIterator<Item = (String, Value)>) -> Value {
53        Value::Record(fields.into_iter().collect())
54    }
55
56    /// Build a function, choosing the representation its domain implies.
57    pub fn function(entries: BTreeMap<Value, Value>) -> Value {
58        if entries.is_empty() {
59            return Value::Seq(Vec::new());
60        }
61        if entries
62            .keys()
63            .enumerate()
64            .all(|(i, k)| matches!(k, Value::Int(n) if *n == count(i) + 1))
65        {
66            return Value::Seq(entries.into_values().collect());
67        }
68        if entries.keys().all(|k| matches!(k, Value::Str(_))) {
69            return Value::Record(
70                entries
71                    .into_iter()
72                    .map(|(k, v)| match k {
73                        Value::Str(s) => (s, v),
74                        _ => unreachable!("keys checked to be strings"),
75                    })
76                    .collect(),
77            );
78        }
79        Value::Func(entries)
80    }
81
82    /// The function's graph, for values that are functions.
83    pub fn entries(&self) -> Option<BTreeMap<Value, Value>> {
84        match self {
85            Value::Seq(items) => Some(
86                items
87                    .iter()
88                    .enumerate()
89                    .map(|(i, v)| (Value::Int(count(i) + 1), v.clone()))
90                    .collect(),
91            ),
92            Value::Record(fields) => Some(
93                fields
94                    .iter()
95                    .map(|(k, v)| (Value::Str(k.clone()), v.clone()))
96                    .collect(),
97            ),
98            Value::Func(map) => Some(map.clone()),
99            _ => None,
100        }
101    }
102
103    pub fn domain(&self) -> Option<BTreeSet<Value>> {
104        match self {
105            Value::Seq(items) => Some((1..=count(items.len())).map(Value::Int).collect()),
106            Value::Record(fields) => Some(fields.keys().cloned().map(Value::Str).collect()),
107            Value::Func(map) => Some(map.keys().cloned().collect()),
108            _ => None,
109        }
110    }
111
112    pub fn apply(&self, key: &Value) -> Option<Value> {
113        match (self, key) {
114            (Value::Seq(items), Value::Int(i)) => usize::try_from(*i)
115                .ok()?
116                .checked_sub(1)
117                .and_then(|i| items.get(i).cloned()),
118            (Value::Record(fields), Value::Str(k)) => fields.get(k).cloned(),
119            (Value::Func(map), k) => map.get(k).cloned(),
120            _ => None,
121        }
122    }
123
124    pub fn type_name(&self) -> &'static str {
125        match self {
126            Value::Bool(_) => "a boolean",
127            Value::Int(_) => "an integer",
128            Value::Str(_) => "a string",
129            Value::Seq(_) => "a sequence",
130            Value::Set(_) | Value::Infinite(_) => "a set",
131            Value::Record(_) => "a record",
132            Value::Func(_) => "a function",
133        }
134    }
135
136    pub fn is_set(&self) -> bool {
137        matches!(self, Value::Set(_) | Value::Infinite(_))
138    }
139}
140
141impl fmt::Display for Value {
142    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
143        match self {
144            Value::Bool(b) => f.write_str(if *b { "TRUE" } else { "FALSE" }),
145            Value::Int(n) => write!(f, "{n}"),
146            Value::Str(s) => write!(f, "{s:?}"),
147            Value::Seq(items) => write!(f, "<<{}>>", join(items.iter())),
148            Value::Set(items) => write!(f, "{{{}}}", join(items.iter())),
149            Value::Record(fields) => {
150                let body: Vec<String> =
151                    fields.iter().map(|(k, v)| format!("{k} |-> {v}")).collect();
152                write!(f, "[{}]", body.join(", "))
153            }
154            Value::Func(map) => {
155                let body: Vec<String> = map.iter().map(|(k, v)| format!("{k} :> {v}")).collect();
156                write!(f, "({})", body.join(" @@ "))
157            }
158            Value::Infinite(Infinite::Nat) => f.write_str("Nat"),
159            Value::Infinite(Infinite::Int) => f.write_str("Int"),
160            Value::Infinite(Infinite::Strings) => f.write_str("STRING"),
161            Value::Infinite(Infinite::Sequences(s)) => write!(f, "Seq({s})"),
162        }
163    }
164}
165
166fn join<'a>(items: impl Iterator<Item = &'a Value>) -> String {
167    items
168        .map(ToString::to_string)
169        .collect::<Vec<_>>()
170        .join(", ")
171}
tla_eval/value.rs

tla_eval/
value.rs
