necoherence - v0.2.0

necoherence/iteration

Types

ClosureOutcome

Closed outcome of a closure run.

pub type ClosureOutcome(t) {
  Fixpoint(result: List(t), position: Int)
  Violation(position: Int, current: List(t), produced: List(t))
  ClosureProjectionFailed(
    current: List(t),
    stopped: StageProjectionFailed,
  )
}

Constructors 

  • Fixpoint(result: List(t), position: Int)
  • Violation(position: Int, current: List(t), produced: List(t))
  • ClosureProjectionFailed(
  current: List(t),
  stopped: StageProjectionFailed,
)

ClosureReq

Input to a closure run: a monotone step declaration, its finite carrier, a seed subset, and the field names present on every round’s own input.

pub type ClosureReq(t) {
  ClosureReq(
    step: call.Immediate(ClosureState(t), List(t)),
    carrier: List(t),
    seed: List(t),
    step_fields: List(String),
  )
}

Constructors

ClosureState

Input to a closure’s step: the current accumulated subset of the carrier, given as a list with no meaningful order or duplication.

pub type ClosureState(t) {
  ClosureState(elements: List(t))
}

Constructors 

  • ClosureState(elements: List(t))

FoldOutcome

Closed outcome of a fold run.

pub type FoldOutcome(s) {
  FoldTrace(states: List(s))
  FoldStopped(states: List(s), stopped: StageProjectionFailed)
}

Constructors

FoldReq

Input to a fold run: a step declaration, its seed, how many rounds to run, and the field names present on every round’s own input.

pub type FoldReq(s) {
  FoldReq(
    step: call.Immediate(s, s),
    seed: s,
    count: Int,
    step_fields: List(String),
  )
}

Constructors 

  • FoldReq(
  step: call.Immediate(s, s),
  seed: s,
  count: Int,
  step_fields: List(String),
)

Measure

A round’s own progress measure, read from the step’s output.

pub type Measure =
  Int

RecurseOutcome

Closed outcome of a recurse run.

pub type RecurseOutcome(s) {
  RecurseSettled(value: s, steps: Int)
  RecurseDidNotDecrease(
    position: Int,
    state: s,
    measure: Int,
    previous_measure: Int,
  )
  RecurseProjectionFailed(
    last_state: s,
    stopped: StageProjectionFailed,
  )
}

Constructors 

  • RecurseSettled(value: s, steps: Int)
  • RecurseDidNotDecrease(
  position: Int,
  state: s,
  measure: Int,
  previous_measure: Int,
)
  • RecurseProjectionFailed(
  last_state: s,
  stopped: StageProjectionFailed,
)

RecurseReq

Input to a recurse run: a step declaration, its seed, and the field names present on every round’s own input.

pub type RecurseReq(s) {
  RecurseReq(
    step: call.Immediate(s, StepOutcome(s)),
    seed: s,
    step_fields: List(String),
  )
}

Constructors

StageProjectionFailed

Where, in a run of rounds, one round’s own projection failed.

pub type StageProjectionFailed {
  StageProjectionFailed(
    position: Int,
    failure: call.ProjectionFailed,
  )
}

Constructors

StepOutcome

Next state together with this round’s own measure toward termination, or the confirmed final state.

pub type StepOutcome(s) {
  Advance(state: s, measure: Int)
  Settled(state: s)
}

Constructors 

  • Advance(state: s, measure: Int)
  • Settled(state: s)

Values

closure 

pub fn closure(req: ClosureReq(t)) -> ClosureOutcome(t)

Call the step from the seed until the accumulated subset stops growing. Each round’s output must extend that round’s own input and stay within the carrier; either failing returns a declared outcome branch.

fold 

pub fn fold(req: FoldReq(s)) -> FoldOutcome(s)

Run the step through a call at most count times from the seed. Stops at the first round whose call fails to project and reports that round’s position; otherwise runs every round.

recurse 

pub fn recurse(req: RecurseReq(s)) -> RecurseOutcome(s)

Call the step from the seed until it settles. The first round sets the bound from its own reported measure; every later round must report a strictly smaller measure or the run stops early. A round whose call fails to project stops the run instead.

✨ Search Document