bynk_check/
store_write.rs

1//! #2194/#2195: recognising a write to an agent's own state, shared by the
2//! sequence diagram (state-write notes) and the agent state model.
3//!
4//! Syntactic by design (agent-state-views track §3.3): the checker's resolved
5//! `Callee` table is not retained for the IDE, so a store operation is
6//! recognised from the AST against the agent's `store` fields and the
7//! store-op registry's `mutates` flag, with local shadowing respected.
8
9use std::collections::HashMap;
10
11use crate::store_ops;
12use bynk_syntax::ast::*;
13
14/// A mutating store operation on one of the agent's own fields:
15/// `field.method(args)`.
16pub struct StoreWrite<'a> {
17    pub field: &'a Ident,
18    pub method: &'a Ident,
19    pub args: &'a [Expr],
20}
21
22/// `expr` as a mutating store operation, when its receiver is a bare name
23/// that is one of the agent's store fields (`store`: name → kind head), not
24/// shadowed by a name in `bound`, and its method is one the registry marks as
25/// mutating for that field's kind. `None` for a read, a query, any other call,
26/// or a shadowed name.
27pub fn store_write<'a>(
28    store: &HashMap<String, String>,
29    bound: &[String],
30    expr: &'a Expr,
31) -> Option<StoreWrite<'a>> {
32    let ExprKind::MethodCall {
33        receiver,
34        method,
35        args,
36        ..
37    } = &expr.kind
38    else {
39        return None;
40    };
41    let ExprKind::Ident(field) = &receiver.kind else {
42        return None;
43    };
44    let head = store.get(&field.name)?;
45    if bound.contains(&field.name) || !store_ops::is_mutating(head, &method.name) {
46        return None;
47    }
48    Some(StoreWrite {
49        field,
50        method,
51        args,
52    })
53}
54
55/// The agent's store fields as name → kind head (`"Map"`, `"Cell"`, …).
56pub fn store_kinds(agent: &AgentDecl) -> HashMap<String, String> {
57    agent
58        .store_fields
59        .iter()
60        .map(|f| (f.name.name.clone(), f.kind.head.name.clone()))
61        .collect()
62}
bynk_check/store_write.rs

bynk_check/
store_write.rs
