LAWS.bend source

LAWS.bend on the hub · documented module

import Baseimport ./lib.bend as Q# to_list(empty) is Nil.law to_list_empty:  for -a: Quant  for -A: Kind(a)  { Q.Queue.to_list(a, A, Q.Queue.empty(a, A)) == Nil{} : List<a, A> }# empty is Q{Nil, Nil}.law empty_is_q_nil:  for -a: Quant  for -A: Kind(a)  { Q.Queue.empty(a, A) == Q.Q{Nil{}, Nil{}} : Q.Queue<a, A> }# to_list unfolds to front ++ reverse(rear).law to_list_q:  for -a: Quant  for -A: Kind(a)  for f: List<a, A>  for r: List<a, A>  { Q.Queue.to_list(a, A, Q.Q{f, r}) == List.append(a, A, f, List.reverse(a, A, r)) : List<a, A> }# Enqueue on empty yields a singleton list in FIFO order.law to_list_enqueue_empty:  for -a: Quant  for -A: Kind(a)  for x: A  { Q.Queue.to_list(a, A, Q.Queue.enqueue(a, A, Q.Queue.empty(a, A), x)) == x <> Nil{} : List<a, A> }# enqueue(empty, x) puts x on the rear.law enqueue_empty:  for -a: Quant  for -A: Kind(a)  for x: A  { Q.Queue.enqueue(a, A, Q.Queue.empty(a, A), x) == Q.Q{Nil{}, x <> Nil{}} : Q.Queue<a, A> }# enqueue preserves front and conses onto rear.law enqueue_q:  for -a: Quant  for -A: Kind(a)  for f: List<a, A>  for r: List<a, A>  for x: A  { Q.Queue.enqueue(a, A, Q.Q{f, r}, x) == Q.Q{f, x <> r} : Q.Queue<a, A> }# dequeue(enqueue(empty, x)) recovers x and an empty rest.law dequeue_enqueue_empty:  for -a: Quant  for -A: Kind(a)  for x: A  {    Q.Queue.dequeue(a, A, Q.Queue.enqueue(a, A, Q.Queue.empty(a, A), x))      == Some{Q.HD{x, Q.Queue.empty(a, A)}}    : Maybe<a, Q.Queue.Deq<a, A>>  }# dequeue with nonempty front recovers head without rotating.law dequeue_front_cons:  for -a: Quant  for -A: Kind(a)  for h: A  for t: List<a, A>  for r: List<a, A>  {    Q.Queue.dequeue(a, A, Q.Q{h <> t, r})      == Some{Q.HD{h, Q.Q{t, r}}}    : Maybe<a, Q.Queue.Deq<a, A>>  }# dequeue(from_list(h <> t)) recovers h.law dequeue_from_cons:  for -a: Quant  for -A: Kind(a)  for h: A  for t: List<a, A>  {    Q.Queue.dequeue(a, A, Q.Queue.from_list(a, A, h <> t))      == Some{Q.HD{h, Q.Q{t, Nil{}}}}    : Maybe<a, Q.Queue.Deq<a, A>>  }# peek(empty) is None.law peek_empty:  for -a: Quant  for -A: Kind(a)  { Q.Queue.peek(a, A, Q.Queue.empty(a, A)) == None{} : Maybe<a, A> }# peek(enqueue(empty, x)) recovers x.law peek_enqueue_empty:  for -a: Quant  for -A: Kind(a)  for x: A  { Q.Queue.peek(a, A, Q.Queue.enqueue(a, A, Q.Queue.empty(a, A), x)) == Some{x} : Maybe<a, A> }# peek(from_list(h <> t)) recovers h.law peek_from_cons:  for -a: Quant  for -A: Kind(a)  for h: A  for t: List<a, A>  { Q.Queue.peek(a, A, Q.Queue.from_list(a, A, h <> t)) == Some{h} : Maybe<a, A> }# length(empty) is 0.law length_empty:  for -a: Quant  for -A: Kind(a)  { Q.Queue.length(a, A, Q.Queue.empty(a, A)) == 0n : Nat }# length(Q{f,r}) is |f| + |r|.law length_q:  for -a: Quant  for -A: Kind(a)  for f: List<a, A>  for r: List<a, A>  {    Q.Queue.length(a, A, Q.Q{f, r})      == Nat.add(List.length(a, A, f), List.length(a, A, r))    : Nat  }# length after enqueue on a concrete Q{f,r}: |f| + Succ(|r|).law length_enqueue:  for -a: Quant  for -A: Kind(a)  for f: List<a, A>  for r: List<a, A>  for x: A  {    Q.Queue.length(a, A, Q.Queue.enqueue(a, A, Q.Q{f, r}, x))      == Nat.add(List.length(a, A, f), 1n+List.length(a, A, r))    : Nat  }# length(enqueue(empty, x)) is 1.law length_enqueue_empty:  for -a: Quant  for -A: Kind(a)  for x: A  { Q.Queue.length(a, A, Q.Queue.enqueue(a, A, Q.Queue.empty(a, A), x)) == 1n : Nat }# Definitional characterization of length(from_list(xs)).law length_from_list_def:  for -a: Quant  for -A: Kind(a)  for xs: List<a, A>  {    Q.Queue.length(a, A, Q.Queue.from_list(a, A, xs))      == Nat.add(List.length(a, A, xs), List.length(a, A, Nil{}))    : Nat  }# from_list puts the whole list in front.law from_list_q:  for -a: Quant  for -A: Kind(a)  for xs: List<a, A>  { Q.Queue.from_list(a, A, xs) == Q.Q{xs, Nil{}} : Q.Queue<a, A> }# Definitional characterization of to_list(from_list(xs)).law to_list_from_list_def:  for -a: Quant  for -A: Kind(a)  for xs: List<a, A>  {    Q.Queue.to_list(a, A, Q.Queue.from_list(a, A, xs))      == List.append(a, A, xs, List.reverse(a, A, Nil{}))    : List<a, A>  }# dequeue(empty) is None.law dequeue_empty:  for -a: Quant  for -A: Kind(a)  { Q.Queue.dequeue(a, A, Q.Queue.empty(a, A)) == None{} : Maybe<a, Q.Queue.Deq<a, A>> }# is_empty(empty) is true.law is_empty_empty:  for -a: Quant  for -A: Kind(a)  { Q.Queue.is_empty(a, A, Q.Queue.empty(a, A)) == True{} : Bool }# is_empty(enqueue(empty, x)) is false.law is_empty_enqueue_empty:  for -a: Quant  for -A: Kind(a)  for x: A  { Q.Queue.is_empty(a, A, Q.Queue.enqueue(a, A, Q.Queue.empty(a, A), x)) == False{} : Bool }# is_empty with nonempty front is false.law is_empty_front_cons:  for -a: Quant  for -A: Kind(a)  for h: A  for t: List<a, A>  for r: List<a, A>  { Q.Queue.is_empty(a, A, Q.Q{h <> t, r}) == False{} : Bool }# is_empty(from_list(Nil)) is true.law is_empty_from_nil:  for -a: Quant  for -A: Kind(a)  { Q.Queue.is_empty(a, A, Q.Queue.from_list(a, A, Nil{})) == True{} : Bool }# is_empty(from_list(h <> t)) is false.law is_empty_from_cons:  for -a: Quant  for -A: Kind(a)  for h: A  for t: List<a, A>  { Q.Queue.is_empty(a, A, Q.Queue.from_list(a, A, h <> t)) == False{} : Bool }# norm(empty) is empty.law norm_empty:  for -a: Quant  for -A: Kind(a)  { Q.Queue.norm(a, A, Q.Queue.empty(a, A)) == Q.Q{Nil{}, Nil{}} : Q.Queue<a, A> }# norm with nonempty front is identity.law norm_front_cons:  for -a: Quant  for -A: Kind(a)  for h: A  for t: List<a, A>  for r: List<a, A>  { Q.Queue.norm(a, A, Q.Q{h <> t, r}) == Q.Q{h <> t, r} : Q.Queue<a, A> }# norm rotates a singleton rear into front.law norm_rear_singleton:  for -a: Quant  for -A: Kind(a)  for x: A  { Q.Queue.norm(a, A, Q.Q{Nil{}, x <> Nil{}}) == Q.Q{x <> Nil{}, Nil{}} : Q.Queue<a, A> }