LAWS.bend source

LAWS.bend on the hub · documented module

import Baseimport ./lib.bend as S# to_list(empty) is Nil.law to_list_empty:  for -a: Quant  for -A: Kind(a)  { S.Stack.to_list(a, A, S.Stack.empty(a, A)) == Nil{} : List<a, A> }# empty is S{Nil}.law empty_is_s_nil:  for -a: Quant  for -A: Kind(a)  { S.Stack.empty(a, A) == S.S{Nil{}} : S.Stack<a, A> }# to_list(S{xs}) exposes the underlying list.law to_list_s:  for -a: Quant  for -A: Kind(a)  for xs: List<a, A>  { S.Stack.to_list(a, A, S.S{xs}) == xs : List<a, A> }# push places the new value at the list head.law to_list_push:  for -a: Quant  for -A: Kind(a)  for xs: List<a, A>  for x: A  { S.Stack.to_list(a, A, S.Stack.push(a, A, S.S{xs}, x)) == x <> xs : List<a, A> }# push(empty, x) is S{x <> Nil}.law push_empty:  for -a: Quant  for -A: Kind(a)  for x: A  { S.Stack.push(a, A, S.Stack.empty(a, A), x) == S.S{x <> Nil{}} : S.Stack<a, A> }# pop(push(empty, x)) recovers x and an empty rest.law pop_push_empty:  for -a: Quant  for -A: Kind(a)  for x: A  {    S.Stack.pop(a, A, S.Stack.push(a, A, S.Stack.empty(a, A), x))      == Some{S.HD{x, S.Stack.empty(a, A)}}    : Maybe<a, S.Stack.Pop<a, A>>  }# pop(push(s, x)) recovers x and s.law pop_push:  for -a: Quant  for -A: Kind(a)  for xs: List<a, A>  for x: A  {    S.Stack.pop(a, A, S.Stack.push(a, A, S.S{xs}, x))      == Some{S.HD{x, S.S{xs}}}    : Maybe<a, S.Stack.Pop<a, A>>  }# pop on a concrete Cons recovers head/rest.law pop_s_cons:  for -a: Quant  for -A: Kind(a)  for h: A  for t: List<a, A>  { S.Stack.pop(a, A, S.S{h <> t}) == Some{S.HD{h, S.S{t}}} : Maybe<a, S.Stack.Pop<a, A>> }# peek(push(s, x)) recovers x.law peek_push:  for -a: Quant  for -A: Kind(a)  for xs: List<a, A>  for x: A  { S.Stack.peek(a, A, S.Stack.push(a, A, S.S{xs}, x)) == Some{x} : Maybe<a, A> }# peek(push(empty, x)) recovers x.law peek_push_empty:  for -a: Quant  for -A: Kind(a)  for x: A  { S.Stack.peek(a, A, S.Stack.push(a, A, S.Stack.empty(a, A), x)) == Some{x} : Maybe<a, A> }# peek on Cons recovers head.law peek_s_cons:  for -a: Quant  for -A: Kind(a)  for h: A  for t: List<a, A>  { S.Stack.peek(a, A, S.S{h <> t}) == Some{h} : Maybe<a, A> }# is_empty(empty) is true.law is_empty_empty:  for -a: Quant  for -A: Kind(a)  { S.Stack.is_empty(a, A, S.Stack.empty(a, A)) == True{} : Bool }# is_empty(S{Nil}) is true.law is_empty_s_nil:  for -a: Quant  for -A: Kind(a)  { S.Stack.is_empty(a, A, S.S{Nil{}}) == True{} : Bool }# is_empty after push is false.law is_empty_push:  for -a: Quant  for -A: Kind(a)  for xs: List<a, A>  for x: A  { S.Stack.is_empty(a, A, S.Stack.push(a, A, S.S{xs}, x)) == False{} : Bool }# is_empty(S{h <> t}) is false.law is_empty_s_cons:  for -a: Quant  for -A: Kind(a)  for h: A  for t: List<a, A>  { S.Stack.is_empty(a, A, S.S{h <> t}) == False{} : Bool }# length(empty) is 0.law length_empty:  for -a: Quant  for -A: Kind(a)  { S.Stack.length(a, A, S.Stack.empty(a, A)) == 0n : Nat }# length(S{xs}) is List.length(xs).law length_s:  for -a: Quant  for -A: Kind(a)  for xs: List<a, A>  { S.Stack.length(a, A, S.S{xs}) == List.length(a, A, xs) : Nat }# length after push is one plus the prior list length.law length_push:  for -a: Quant  for -A: Kind(a)  for xs: List<a, A>  for x: A  {    S.Stack.length(a, A, S.Stack.push(a, A, S.S{xs}, x))      == 1n+List.length(a, A, xs)    : Nat  }# length(push(empty, x)) is 1.law length_push_empty:  for -a: Quant  for -A: Kind(a)  for x: A  { S.Stack.length(a, A, S.Stack.push(a, A, S.Stack.empty(a, A), x)) == 1n : Nat }# from_list puts the list directly in stack order.law from_list_s:  for -a: Quant  for -A: Kind(a)  for xs: List<a, A>  { S.Stack.from_list(a, A, xs) == S.S{xs} : S.Stack<a, A> }# to_list ∘ from_list is identity on lists.law to_list_from_list:  for -a: Quant  for -A: Kind(a)  for xs: List<a, A>  { S.Stack.to_list(a, A, S.Stack.from_list(a, A, xs)) == xs : List<a, A> }# from_list ∘ to_list is identity on stacks.law from_list_to_list:  for -a: Quant  for -A: Kind(a)  for xs: List<a, A>  { S.Stack.from_list(a, A, S.Stack.to_list(a, A, S.S{xs})) == S.S{xs} : S.Stack<a, A> }# from_list(Nil) roundtrips to empty via to_list.law to_list_from_empty:  for -a: Quant  for -A: Kind(a)  { S.Stack.to_list(a, A, S.Stack.from_list(a, A, Nil{})) == Nil{} : List<a, A> }# pop(empty) is None.law pop_empty:  for -a: Quant  for -A: Kind(a)  { S.Stack.pop(a, A, S.Stack.empty(a, A)) == None{} : Maybe<a, S.Stack.Pop<a, A>> }# peek(empty) is None.law peek_empty:  for -a: Quant  for -A: Kind(a)  { S.Stack.peek(a, A, S.Stack.empty(a, A)) == None{} : Maybe<a, A> }