LAWS.bend source

LAWS.bend on the hub · documented module

import Baseimport ./lib.bend as P# empty is P{Nil}.law empty_is_p_nil:  { P.Prio.empty() == P.P{Nil{}} : P.Prio }# to_list(empty) is Nil.law to_list_empty:  { P.Prio.to_list(P.Prio.empty()) == Nil{} : List<&2, U32> }# to_list(P{xs}) exposes the list.law to_list_p:  for xs: List<&2, U32>  { P.Prio.to_list(P.P{xs}) == xs : List<&2, U32> }# push(empty, x) stores the singleton list.law to_list_push_empty:  for x: U32  { P.Prio.to_list(P.Prio.push(P.Prio.empty(), x)) == x <> Nil{} : List<&2, U32> }# peek_min(empty) is None.law peek_empty:  { P.Prio.peek_min(P.Prio.empty()) == None{} : Maybe<&2, U32> }# peek_min(push(empty, x)) is x.law peek_push_empty:  for x: U32  { P.Prio.peek_min(P.Prio.push(P.Prio.empty(), x)) == Some{x} : Maybe<&2, U32> }# peek_min on a concrete Cons recovers the head (min when sorted).law peek_p_cons:  for h: U32  for t: List<&2, U32>  { P.Prio.peek_min(P.P{h <> t}) == Some{h} : Maybe<&2, U32> }# pop_min(empty) is None.law pop_empty:  { P.Prio.pop_min(P.Prio.empty()) == None{} : Maybe<&2, P.Prio.Pop> }# pop_min(push(empty, x)) returns x and empty.law pop_push_empty:  for x: U32  {    P.Prio.pop_min(P.Prio.push(P.Prio.empty(), x))      == Some{P.PP{x, P.Prio.empty()}}    : Maybe<&2, P.Prio.Pop>  }# pop_min on Cons recovers head/rest.law pop_p_cons:  for h: U32  for t: List<&2, U32>  { P.Prio.pop_min(P.P{h <> t}) == Some{P.PP{h, P.P{t}}} : Maybe<&2, P.Prio.Pop> }# size(empty) is 0.law size_empty:  { P.Prio.size(P.Prio.empty()) == 0n : Nat }# size(P{xs}) is List.length(xs).law size_p:  for xs: List<&2, U32>  { P.Prio.size(P.P{xs}) == List.length(&2, U32, xs) : Nat }# size(push(empty, x)) is 1.law size_push_empty:  for x: U32  { P.Prio.size(P.Prio.push(P.Prio.empty(), x)) == 1n : Nat }# is_empty(empty) is True.law is_empty_empty:  { P.Prio.is_empty(P.Prio.empty()) == True{} : Bool }law is_empty_p_nil:  { P.Prio.is_empty(P.P{Nil{}}) == True{} : Bool }law is_empty_p_cons:  for h: U32  for t: List<&2, U32>  { P.Prio.is_empty(P.P{h <> t}) == False{} : Bool }law is_empty_push:  for x: U32  { P.Prio.is_empty(P.Prio.push(P.Prio.empty(), x)) == False{} : Bool }# from_list(Nil) is empty.law from_list_empty:  { P.Prio.from_list(Nil{}) == P.Prio.empty() : P.Prio }# from_list(singleton) is the singleton bag.law from_list_singleton:  for x: U32  { P.Prio.from_list(x <> Nil{}) == P.Prio.push(P.Prio.empty(), x) : P.Prio }# insert into Nil yields singleton.law insert_nil:  for x: U32  { P.Prio.insert(Nil{}, x) == x <> Nil{} : List<&2, U32> }# Concrete ordering: push 2 then 1 sorts ascending.law push_two_ordered:  {    P.Prio.to_list(P.Prio.push(P.Prio.push(P.Prio.empty(), 2), 1))      == 1 <> (2 <> Nil{})    : List<&2, U32>  }# Concrete ordering: push 1 then 2 stays ascending.law push_two_same_order:  {    P.Prio.to_list(P.Prio.push(P.Prio.push(P.Prio.empty(), 1), 2))      == 1 <> (2 <> Nil{})    : List<&2, U32>  }# peek_min of two pushed values is the smaller.law peek_two_min:  {    P.Prio.peek_min(P.Prio.push(P.Prio.push(P.Prio.empty(), 5), 3))      == Some{3}    : Maybe<&2, U32>  }# size after two pushes is 2.law size_two:  {    P.Prio.size(P.Prio.push(P.Prio.push(P.Prio.empty(), 1), 2))      == 2n    : Nat  }# from_list sorts into nondecreasing order (concrete).law from_list_two:  {    P.Prio.to_list(P.Prio.from_list(2 <> (1 <> Nil{})))      == 1 <> (2 <> Nil{})    : List<&2, U32>  }