LAWS.bend source

LAWS.bend on the hub · documented module

import Baseimport ./lib.bend as DQ# empty is D{Nil, Nil}.law empty_is_d_nil:  for -a: Quant  for -A: Kind(a)  { DQ.Deque.empty(a, A) == DQ.D{Nil{}, Nil{}} : DQ.Deque<a, A> }# Empty has no front element.law peek_front_empty:  for -a: Quant  for -A: Kind(a)  { DQ.Deque.peek_front(a, A, DQ.Deque.empty(a, A)) == None{} : Maybe<a, A> }# Empty has no back element.law peek_back_empty:  for -a: Quant  for -A: Kind(a)  { DQ.Deque.peek_back(a, A, DQ.Deque.empty(a, A)) == None{} : Maybe<a, A> }# Empty pops from either end to None.law pop_front_empty:  for -a: Quant  for -A: Kind(a)  { DQ.Deque.pop_front(a, A, DQ.Deque.empty(a, A)) == None{} : Maybe<a, DQ.Deque.Pop<a, A>> }law pop_back_empty:  for -a: Quant  for -A: Kind(a)  { DQ.Deque.pop_back(a, A, DQ.Deque.empty(a, A)) == None{} : Maybe<a, DQ.Deque.Pop<a, A>> }law to_list_empty:  for -a: Quant  for -A: Kind(a)  { DQ.Deque.to_list(a, A, DQ.Deque.empty(a, A)) == Nil{} : List<a, A> }law length_empty:  for -a: Quant  for -A: Kind(a)  { DQ.Deque.length(a, A, DQ.Deque.empty(a, A)) == 0n : Nat }law is_empty_empty:  for -a: Quant  for -A: Kind(a)  { DQ.Deque.is_empty(a, A, DQ.Deque.empty(a, A)) == True{} : Bool }# Definitional characterization of the two-list order.law to_list_d:  for -a: Quant  for -A: Kind(a)  for f: List<a, A>  for r: List<a, A>  { DQ.Deque.to_list(a, A, DQ.D{f, r}) == List.append(a, A, f, List.reverse(a, A, r)) : List<a, A> }law length_d:  for -a: Quant  for -A: Kind(a)  for f: List<a, A>  for r: List<a, A>  {    DQ.Deque.length(a, A, DQ.D{f, r})      == Nat.add(List.length(a, A, f), List.length(a, A, r))    : Nat  }law from_list_d:  for -a: Quant  for -A: Kind(a)  for xs: List<a, A>  { DQ.Deque.from_list(a, A, xs) == DQ.D{xs, Nil{}} : DQ.Deque<a, A> }law from_list_empty:  for -a: Quant  for -A: Kind(a)  { DQ.Deque.from_list(a, A, Nil{}) == DQ.Deque.empty(a, A) : DQ.Deque<a, A> }law from_list_singleton_roundtrip:  for -a: Quant  for -A: Kind(a)  for x: A  { DQ.Deque.to_list(a, A, DQ.Deque.from_list(a, A, x <> Nil{})) == x <> Nil{} : List<a, A> }law push_front_d:  for -a: Quant  for -A: Kind(a)  for f: List<a, A>  for r: List<a, A>  for x: A  { DQ.Deque.push_front(a, A, DQ.D{f, r}, x) == DQ.D{x <> f, r} : DQ.Deque<a, A> }law push_back_d:  for -a: Quant  for -A: Kind(a)  for f: List<a, A>  for r: List<a, A>  for x: A  { DQ.Deque.push_back(a, A, DQ.D{f, r}, x) == DQ.D{f, x <> r} : DQ.Deque<a, A> }# Pushing at either end produces the same singleton order.law push_front_singleton:  for -a: Quant  for -A: Kind(a)  for x: A  { DQ.Deque.to_list(a, A, DQ.Deque.push_front(a, A, DQ.Deque.empty(a, A), x)) == x <> Nil{} : List<a, A> }law push_back_singleton:  for -a: Quant  for -A: Kind(a)  for x: A  { DQ.Deque.to_list(a, A, DQ.Deque.push_back(a, A, DQ.Deque.empty(a, A), x)) == x <> Nil{} : List<a, A> }law length_push_front_empty:  for -a: Quant  for -A: Kind(a)  for x: A  { DQ.Deque.length(a, A, DQ.Deque.push_front(a, A, DQ.Deque.empty(a, A), x)) == 1n : Nat }law length_push_back_empty:  for -a: Quant  for -A: Kind(a)  for x: A  { DQ.Deque.length(a, A, DQ.Deque.push_back(a, A, DQ.Deque.empty(a, A), x)) == 1n : Nat }law is_empty_push_front:  for -a: Quant  for -A: Kind(a)  for x: A  { DQ.Deque.is_empty(a, A, DQ.Deque.push_front(a, A, DQ.Deque.empty(a, A), x)) == False{} : Bool }law is_empty_push_back:  for -a: Quant  for -A: Kind(a)  for x: A  { DQ.Deque.is_empty(a, A, DQ.Deque.push_back(a, A, DQ.Deque.empty(a, A), x)) == False{} : Bool }law peek_front_push_front:  for -a: Quant  for -A: Kind(a)  for x: A  { DQ.Deque.peek_front(a, A, DQ.Deque.push_front(a, A, DQ.Deque.empty(a, A), x)) == Some{x} : Maybe<a, A> }law peek_back_push_back:  for -a: Quant  for -A: Kind(a)  for x: A  { DQ.Deque.peek_back(a, A, DQ.Deque.push_back(a, A, DQ.Deque.empty(a, A), x)) == Some{x} : Maybe<a, A> }law peek_front_push_back:  for -a: Quant  for -A: Kind(a)  for x: A  { DQ.Deque.peek_front(a, A, DQ.Deque.push_back(a, A, DQ.Deque.empty(a, A), x)) == Some{x} : Maybe<a, A> }law peek_back_push_front:  for -a: Quant  for -A: Kind(a)  for x: A  { DQ.Deque.peek_back(a, A, DQ.Deque.push_front(a, A, DQ.Deque.empty(a, A), x)) == Some{x} : Maybe<a, A> }# Singleton pops recover the value and an empty deque.law pop_front_push_front_empty:  for -a: Quant  for -A: Kind(a)  for x: A  { DQ.Deque.pop_front(a, A, DQ.Deque.push_front(a, A, DQ.Deque.empty(a, A), x)) == Some{DQ.P{x, DQ.Deque.empty(a, A)}} : Maybe<a, DQ.Deque.Pop<a, A>> }law pop_front_push_back_empty:  for -a: Quant  for -A: Kind(a)  for x: A  { DQ.Deque.pop_front(a, A, DQ.Deque.push_back(a, A, DQ.Deque.empty(a, A), x)) == Some{DQ.P{x, DQ.Deque.empty(a, A)}} : Maybe<a, DQ.Deque.Pop<a, A>> }law pop_back_push_back_empty:  for -a: Quant  for -A: Kind(a)  for x: A  { DQ.Deque.pop_back(a, A, DQ.Deque.push_back(a, A, DQ.Deque.empty(a, A), x)) == Some{DQ.P{x, DQ.Deque.empty(a, A)}} : Maybe<a, DQ.Deque.Pop<a, A>> }law pop_back_push_front_empty:  for -a: Quant  for -A: Kind(a)  for x: A  { DQ.Deque.pop_back(a, A, DQ.Deque.push_front(a, A, DQ.Deque.empty(a, A), x)) == Some{DQ.P{x, DQ.Deque.empty(a, A)}} : Maybe<a, DQ.Deque.Pop<a, A>> }law pop_front_cons:  for -a: Quant  for -A: Kind(a)  for h: A  for t: List<a, A>  for r: List<a, A>  {    DQ.Deque.pop_front(a, A, DQ.D{h <> t, r})      == Some{DQ.P{h, DQ.D{t, r}}}    : Maybe<a, DQ.Deque.Pop<a, A>>  }law pop_back_cons:  for -a: Quant  for -A: Kind(a)  for f: List<a, A>  for h: A  for t: List<a, A>  {    DQ.Deque.pop_back(a, A, DQ.D{f, h <> t})      == Some{DQ.P{h, DQ.D{f, t}}}    : Maybe<a, DQ.Deque.Pop<a, A>>  }law norm_front_cons:  for -a: Quant  for -A: Kind(a)  for h: A  for t: List<a, A>  for r: List<a, A>  { DQ.Deque.norm_front(a, A, DQ.D{h <> t, r}) == DQ.D{h <> t, r} : DQ.Deque<a, A> }law norm_back_cons:  for -a: Quant  for -A: Kind(a)  for f: List<a, A>  for h: A  for t: List<a, A>  { DQ.Deque.norm_back(a, A, DQ.D{f, h <> t}) == DQ.D{f, h <> t} : DQ.Deque<a, A> }law norm_front_rear_one:  for -a: Quant  for -A: Kind(a)  for x: A  { DQ.Deque.norm_front(a, A, DQ.D{Nil{}, x <> Nil{}}) == DQ.D{x <> Nil{}, Nil{}} : DQ.Deque<a, A> }law norm_back_front_one:  for -a: Quant  for -A: Kind(a)  for x: A  { DQ.Deque.norm_back(a, A, DQ.D{x <> Nil{}, Nil{}}) == DQ.D{Nil{}, x <> Nil{}} : DQ.Deque<a, A> }# push_front then push_back order.law to_list_front_then_back:  for -a: Quant  for -A: Kind(a)  for x: A  for y: A  {    DQ.Deque.to_list(a, A,      DQ.Deque.push_back(a, A, DQ.Deque.push_front(a, A, DQ.Deque.empty(a, A), x), y))      == x <> (y <> Nil{})    : List<a, A>  }