metamon/relation

Named two-argument predicates used by metamorphic relations.

A Relation(b) answers “do these two outputs satisfy the constraint?”. The name is surfaced in failure reports so the user immediately sees which property broke.

Types

Relation

</>

A named two-argument predicate over outputs.

pub type Relation(b) {
  Relation(name: String, holds: fn(b, b) -> Bool)
}

Constructors

Relation(name: String, holds: fn(b, b) -> Bool)

A relation across an arbitrary number of follow-up outputs. holds(outputs) receives the source output as outputs[0] and the i-th follow-up output as outputs[i + 1]. Used by metamon.forall_morph_n for MRs that compare more than two outputs (e.g. f(x), f(T1(x)), f(T2(x)) are pairwise equal).

pub type RelationN(b) {
  RelationN(name: String, holds: fn(List(b)) -> Bool)
}

Constructors

RelationN(name: String, holds: fn(List(b)) -> Bool)

Values

all_equal

</>

pub fn all_equal() -> RelationN(b)

All elements of the input list are equal under structural ==. Trivially True for lists of length 0 or 1.

and

</>

pub fn and(r1: Relation(b), r2: Relation(b)) -> Relation(b)

Both r1 and r2 must hold.

approximately

</>

pub fn approximately(epsilon: Float) -> Relation(Float)

Floats within epsilon of each other.

Panics at construction if epsilon is negative. A negative epsilon would silently yield a degenerate “always false” relation (the absolute difference is always non-negative, so diff <=. epsilon can never hold). Failing visibly on a sign mistake matches the project’s posture for malformed numeric inputs in Range.constant, Range.linear, etc.

equal

</>

pub fn equal() -> Relation(a)

Equality (Gleam’s structural ==).

equivalent_under

</>

pub fn equivalent_under(
  via: fn(b) -> c,
  name: String,
) -> Relation(b)

Equality after a shared normalisation step. Useful for “equal modulo whitespace / key order / formatting”.

implies

</>

pub fn implies(
  antecedent: fn(b, b) -> Bool,
  inner: Relation(b),
) -> Relation(b)

Conditional relation: if antecedent(left, right) is True, the inner relation must hold. Otherwise the relation is trivially satisfied.

invert

</>

pub fn invert(r: Relation(b)) -> Relation(b)

Negate a relation.

monotone

</>

pub fn monotone(cmp: fn(a, a) -> order.Order) -> Relation(a)

cmp(left, right) returns Lt or Eq (i.e. left ≤ right).

n_new

</>

pub fn n_new(
  name: String,
  holds: fn(List(b)) -> Bool,
) -> RelationN(b)

Construct an N-ary relation directly.

new

</>

pub fn new(name: String, holds: fn(b, b) -> Bool) -> Relation(b)

Construct a relation from a name and a binary predicate.

not_equal

</>

pub fn not_equal() -> Relation(a)

Inequality.

or

</>

pub fn or(r1: Relation(b), r2: Relation(b)) -> Relation(b)

At least one of r1 and r2 must hold.

pairwise

</>

pub fn pairwise(r: Relation(b)) -> RelationN(b)

Lift a binary Relation(b) to an N-ary relation by checking it pairwise: every consecutive pair (items[i], items[i+1]) must satisfy r. For name == "equal" this gives a chain of equal values; for monotone it gives a sorted chain.

permutation_of

</>

pub fn permutation_of() -> Relation(List(a))

Two lists are permutations of each other (same multiset).

rename

</>

pub fn rename(r: Relation(b), name: String) -> Relation(b)

Override a relation’s name.

set_subset_of

</>

pub fn set_subset_of() -> Relation(List(a))

Set subset: every element of left is contained somewhere in right, ignoring multiplicity. set_subset_of([1, 1], [1]) is True because the only distinct value 1 is present.

For the multiset interpretation that requires distinct matches per occurrence, use subset_of() instead.

subset_of

</>

pub fn subset_of() -> Relation(List(a))

Multiset subset: every element of left is matched against a distinct element of right (one-to-one, by structural equality). subset_of([1, 1], [1]) is False; subset_of([1, 1], [1, 1, 2]) is True. This matches the semantics of permutation_of (which is also multiset-based).

For the set-style interpretation that ignores multiplicity, use set_subset_of() instead.