metamon - v0.1.0

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)

RelationN

</>

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.

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.

subset_of

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

left is a sub-multiset of right.

✨ Search Document