mutate

mutate-decl ::= attribute* 'pub'? 'mutate' Ident '(' param-list ')' ('->' TypeExpr)?
                '{' mutate-body '}'
mutate-body ::= ('require' '{' expr (',' …)* '}')?
                stmt*
                ('return' expr ';')?
stmt        ::= 'let' Ident (':' TypeExpr)? '=' expr ';'
             |  'match' expr '{' arm (',' …)* '}'
             |  insert-stmt | update-stmt | delete-stmt | upsert-stmt
             |  'detach' 'delete' expr ';'                                  // ‡ refused, OE1353
             |  emit-stmt
             |  'for' Ident 'in' expr '{' stmt* '}'
             |  'if' expr '{' stmt* '}' ('else' '{' stmt* '}')?
             |  expr ';'
insert-stmt ::= 'insert' TypeExpr '{' field-init-list '}' ';'              // typed-literal insert
             |  'insert' Ident ':' TypeExpr '{' field-init-list '}' ';'   // ‡ named typed-literal — OE0001
             |  'insert' Ident 'into' expr ';'                             // insert binding into collection
             |  'insert' predicate-call '{' field-init-list '}' ';'        // relation insert with body
             |  'insert' predicate-call ';'                                // relation insert, no body
update-stmt ::= 'update' (Ident | pattern) 'set' '{' field-assign (',' …)* '}' ('where' expr)? ';'
field-assign ::= Ident ('=' | '+=' | '-=') expr
delete-stmt ::= 'delete' predicate-call ';'                                // delete iof(…) / delete Rel(…)
             |  'delete' (Ident | pattern) ('where' expr)? ';'             // ‡ entity / bulk delete — OE0001
upsert-stmt ::= 'upsert' pattern ('as' Ident)? upsert-clause+ ';'          // ‡ refused, OE1352
upsert-clause ::= 'on' 'insert' '{' field-assign (',' …)* '}'
               |  'on' 'update' '{' field-assign (',' …)* '}'
emit-stmt   ::= 'emit' Ident '{' expr '}' ';'

pub mutate sign_lease(t: Person, p: Property, rent: Money, term_days: Nat) -> Lease {
    require { rent > 0, term_days > 0 }
    let l = insert Lease(t, p) {
        monthly_rent: rent,
        start:        today(),
        end:          today() + term_days.days,
        status:       Pending,
    };
    emit AuditLog { LeaseSigned { lease: l, at: now() } };
    return l;
}

pub mutate hire_or_raise(p: Person, o: Organization, salary: Money) {
    upsert p.works_at(o) as emp
        on insert { emp.start_date = now(), emp.salary = salary }
        on update { emp.salary = salary };
}

pub mutate rebrand(old: String, new: String) {
    update c: Company set { name = new } where c.name == old;
}

An update of a bound target writes its mut fields directly. The ('where' expr)? filter (and the bulk/pattern target forms it implies, as in rebrand above) is refused at ox check / ox build (OE1318), never silently dropped.

The grammar shapes marked ‡ are loud refusals, not silent no-ops. Named typed-literal insert (insert l: Lease { … }; use let l = insert Lease { … } instead) and entity/bulk delete of a bound target or pattern with an optional where refuse with OE0001 — only delete predicate-call (delete iof(…) / delete Rel(…)) is admitted. detach delete refuses with OE1353 and upsert with OE1352.

The rebrand example assumes name is declared mut on Company. Per struct and enum — language built-ins (data declarations), fields are immutable post-construction unless explicitly marked mut:

pub type Company {
    #[intrinsic] founded: Date,    // construction-required; not updatable
    mut name: String,              // updatable via `update`-stmt
}

update-stmt admits writes only to mut fields. A field-assign targeting a non-mut field is rejected with OE0820 UpdateImmutableField. The elaborator validates each field-assign against the entity’s field-decl mut flag; rejection surfaces at build time, not at mutation invocation.

Field updates lower to append-only event pairs on the underlying property axiom (Storage layer): a retract event for the prior value and an assert event for the new. The proposition’s logical identity is the (entity_id, property_id) pair; the value is what changes. Bitemporal queries reconstruct prior values per Temporal substrate.

Mutations are transactional within the body; the kernel may reject mutations that violate refinement, consistency policy, or stratification — rejection surfaces to the caller as Result<T, Diagnostic> from the host runtime.

Dynamic reclassification — insert iof / delete iof. Because iof is a first-class predicate (Reflection), mutate bodies can dynamically classify and declassify entities by inserting or deleting iof tuples through the existing insert predicate-call / delete predicate-call forms:

pub mutate enrol(p: Person) {
    insert iof(p, Student);                  // p is now a Student
}

pub mutate expel(s: Student) {
    delete iof(s, Student);                  // s is no longer a Student
}

The single-type insert iof(x, T) / delete iof(x, T) forms above classify and declassify an entity, subject to the gates below. Inserting an iof tuple over a relation concept — insert iof((p, into), EnrolledAt) for a named relation EnrolledAt — refuses: the tuple-argument form parse-refuses with OE0001 rather than silently doing nothing.

The substrate enforces two constraints on insert iof(x, T):

1. Refinement gate (enforced). If T carries a defined refinement iff { … } (Refinement) — for example, pub type ExtinctSpecies <: BirdSpecies iff { self.numberOfLivingInstances == 0 } — the predicate is the substrate’s source of truth for membership: the modeler updates the underlying state (here, numberOfLivingInstances) and the substrate derives the iof classification automatically, so explicit insert iof(x, ExtinctSpecies) emits OE0211 IofInsertOnDefined and the mutation is rejected. If instead T carries a primitive refinement where { … }, membership is conferred by assertion, so insert iof(x, T) is permitted — but the predicate is a necessary invariant: an x that positively violates it (definite false, World assumptions (CWA / OWA)) is rejected with OE0668 RefinementInvariantViolated. The same invariant is checked when a primitive-where member is created by construction (insert T { … }) or when an update writes a field the predicate reads.
2. Modifier gates (enforced — RFD 0027 D6). Re-classification is governed by the ontology-neutral fixed modifier on the target’s introducing metatype (metatype), never by any axis name: insert iof(x, T) / delete iof(x, T) where T is fixed-introduced is refused with OE0234 FixedReclassification — classification under such types is decided at construction (insert <T> { … } remains legal; construction is not re-classification). Admission is the absence of fixed: dynamic classification is the default, and a vocabulary opts its rigid metatypes into the restriction explicitly (pub fixed metatype kind = { … };) — an axis assignment like rigidity::anti_rigid is inert user vocabulary and grants nothing by itself. Likewise insert iof(x, T) against an abstract type — a direct instance — is refused with OE0233 AbstractTypeConstruct; non-abstract subtypes are unaffected. Both gates fire at ox check / ox build where the target is statically known and at the runtime write path otherwise, rejecting the whole mutation atomically. The membership-constancy theorem (Argon.Runtime.ModifierGates.runMutation_fixed_iof_constant) is what grounds static modal discharge over fixed-introduced types (Modal operators).
3. Compatibility gate. x’s existing classification chain must include some supertype that T specializes (e.g. Student <: Person requires x: Person).

After insert iof(x, T), the entity x is classified under both its prior types and T. After delete iof(x, T), x is no longer classified under T but retains all other classifications. The substrate maintains a single global iof relation; insert/delete operate transactionally.

Bitemporal mutation forms. Per the temporal substrate (Temporal substrate, Effective-dating: valid time and the two as_of axes), an insert may carry an explicit valid-time at <date> qualifier — the assertion’s valid time begins on that civil day (RP-004 mutate). This form executes: the write threads the date onto the event’s bitemporal extent, and an as_of <#date#> query reads it back.

pub type T;
pub mutate enact(x: T, effective: Date) {
    insert iof(x, T);              // [VT: now → ∞]  [TT: now → ∞]  — atemporal default
    insert iof(x, T) at effective; // [VT: effective → ∞]            — effective-dated
}

The window form during [t1, t2], the since open-interval form, and a valid-time-qualified delete (bitemporal retraction — closing a valid-time interval rather than opening one) refuse loudly (OE1330) rather than silently applying at all valid times:

pub type T;
pub mutate retro(x: T) {
    insert iof(x, T) during #2020-09-01#;   // window VT
}

Explicit erasure — forget. For compliance scenarios (GDPR right-to-erasure, sensitive-data redaction), forget removes the underlying tuple including its bitemporal history:

forget x;                                               // bound individual; capability-gated

Only the bound-individual form forget <expr> is admitted; the forget iof(x, T) and bulk forget … where … shapes refuse with OE0001.

forget is capability-gated at the source level: a mutate body containing forget refuses to build (OE0730 ForgetWithoutCapability) unless the enclosing mutate declaration grants #[allow_forget]. Cascading derived facts are revised via DRed overdelete.

Reasserting a tuple after retraction produces distinct VT intervals on the underlying store — the substrate does not coalesce on adjacent boundaries. Historical retract/reassert is queryable via audit projections.

Body semantics

A mutate body lowers to the Operation IR and runs with all-or-nothing atomic commit: a failed require guard, or any error, emits nothing (RFD 0015). require preconditions, let bindings, typed-literal entity construction with system-minted identity, projection navigation (a.b.c) over committed state, collection inserts (insert … into …) with for iteration, sum / count aggregate guards over comprehensions, index projection (coll[i]), and effectful if/else (control flow is expression-valued; branches are blocks) all execute, returning the body’s tail value.

match in bodies. A value-position match (a let RHS, an update … set value, a tail / return value, or a require guard) matches over constant patterns (payloadless enum constants, literals, or-patterns, _; Pattern matching) and desugars to the same IfExpr chain a value if uses, with exhaustiveness enforced at ox check (OE0203). A statement-position match (arms running effects — the BPMN-gateway dispatch match d { Disposition::Clean => { update … }, Disposition::BreaksFound => { insert … }, _ => {} }) lowers to a right-nested Operation::If chain over the arm blocks’ operations (RFD 0015 Amendment 2): the same ordered first-match semantics, constant-pattern subset, and OE0203 exhaustiveness as the value desugar; arm blocks and if branches admit the full mutate statement set at any nesting depth. upsert, emit, and detach delete in a body refuse by name rather than dying generic or doing nothing silently: emit with OE1318, upsert with OE1352, and detach delete with OE1353.

Mutate-body arithmetic is exact (RFD 0016 / RFD 0029): require guards and let / field expressions route through one canonical evaluation core — pure-Int operands stay checked integers (overflow is a loud error, never a wrap), and any Real / Decimal / Money operand promotes to an exact rational (/ is the field operation, no truncation), so 0.1 + 0.2 == 0.3 holds exactly in a mutate body where it would fail in f64.

Reads see committed state. A body’s projections (a.b.c) read the store as committed before the mutation; a body does not observe its own not-yet-committed constructions. One consequence: constructing a collection-valued field and then insert … into that same field in a single body does not compose (the append seeds from committed state).