references.mbt

///|
/// A symbolic variable that names a value produced by an earlier command.
///
/// Generated command programs are built before the real system is executed, so
/// they cannot contain concrete handles, ids, references, file descriptors, or
/// other runtime values. `Var` is the stable placeholder that lets later
/// symbolic commands refer to a value that will only be known after replay.
pub(all) struct Var {
  id : Int
} derive(Eq, Hash, Debug)

///|
/// Formats a symbolic variable using the short form that appears in generated
/// command traces.
pub fn Var::to_string(self : Var) -> String {
  "v\{self.id}"
}

///|
/// A reference that is either symbolic during generation/shrinking or concrete
/// during execution.
///
/// This mirrors the `quickcheck-state-machine` split between symbolic
/// references used in generated programs and concrete references returned by the
/// implementation under test. User command types usually contain `Ref[V]`
/// whenever a command needs to point at a resource created by an earlier
/// command.
pub(all) enum Ref[V] {
  // Placeholder generated by `mock` before the system exists.
  Symbolic(Var)
  // Runtime value obtained from the actual response and stored in the
  // execution `Environment`.
  Concrete(V)
} derive(Eq, Debug)

///|
/// Deterministic source of fresh symbolic variables for mock responses.
///
/// `GenSym` is threaded through generation and shrink validation so that a
/// regenerated prefix allocates the same sequence of symbolic variables. That
/// determinism is what makes command dependencies shrink safely.
pub(all) struct GenSym {
  mut next : Int
} derive(Eq, Debug)

///|
/// Creates a fresh symbolic-variable supply starting at `v0`.
pub fn GenSym::new() -> GenSym {
  { next: 0 }
}

///|
/// Allocates one variable and returns the advanced supply.
pub fn GenSym::fresh(self : GenSym) -> (Var, GenSym) {
  let fresh_var = Var::{ id: self.next }
  self.next = self.next + 1
  (fresh_var, self)
}