~/bend-docscommunity

src/sorted.bend checks

raw source on the hub · import 0x5f97f469d15c04a181dae0e4e64e1d3d/src/sorted.bend as Sorted

2 imports
import Base
import ./class.bend as C

Laws

law insert_from.go provedsource · line 59 · raw

@-A:Data -> @-o:0x5f97f469d15c04a181dae0e4e64e1d3d/src/class.Ord<A> -> @-lo:A -> @-x:A -> @-h:A -> @-t:List<&2, A> -> @-rec:(@_:Unit -> List<&2, A>) -> @s:from(A, o, lo, h <> t) -> @lx:0x5f97f469d15c04a181dae0e4e64e1d3d/src/class.Ord.R(A, o, lo, x) -> @ih:(@_:from(A, o, h, t) -> @_:0x5f97f469d15c04a181dae0e4e64e1d3d/src/class.Ord.R(A, o, h, x) -> from(A, o, h, rec(Unit{}))) -> @c:Or(0x5f97f469d15c04a181dae0e4e64e1d3d/src/class.Ord.R(A, o, x, h), 0x5f97f469d15c04a181dae0e4e64e1d3d/src/class.Ord.R(A, o, h, x)) -> from(A, o, lo, insert.go(A, o, x, h, t, rec, c))

law insert_from provedsource · line 81 · raw

@-A:Data -> @-o:0x5f97f469d15c04a181dae0e4e64e1d3d/src/class.Ord<A> -> @+x:A -> @xs:List<&2, A> -> @-lo:A -> @_:from(A, o, lo, xs) -> @_:0x5f97f469d15c04a181dae0e4e64e1d3d/src/class.Ord.R(A, o, lo, x) -> from(A, o, lo, insert(A, o, x, xs))

law insert_sorted.go provedsource · line 97 · raw

@-A:Data -> @-o:0x5f97f469d15c04a181dae0e4e64e1d3d/src/class.Ord<A> -> @-x:A -> @-h:A -> @-t:List<&2, A> -> @-rec:(@_:Unit -> List<&2, A>) -> @s:from(A, o, h, t) -> @ih:(@_:from(A, o, h, t) -> @_:0x5f97f469d15c04a181dae0e4e64e1d3d/src/class.Ord.R(A, o, h, x) -> from(A, o, h, rec(Unit{}))) -> @c:Or(0x5f97f469d15c04a181dae0e4e64e1d3d/src/class.Ord.R(A, o, x, h), 0x5f97f469d15c04a181dae0e4e64e1d3d/src/class.Ord.R(A, o, h, x)) -> Sorted(A, o, insert.go(A, o, x, h, t, rec, c))

law insert_sorted provedsource · line 116 · raw

@-A:Data -> @-o:0x5f97f469d15c04a181dae0e4e64e1d3d/src/class.Ord<A> -> @+x:A -> @xs:List<&2, A> -> @_:Sorted(A, o, xs) -> Sorted(A, o, insert(A, o, x, xs))

law sort_sorted provedsource · line 132 · raw

@-A:Data -> @-o:0x5f97f469d15c04a181dae0e4e64e1d3d/src/class.Ord<A> -> @xs:List<&2, A> -> Sorted(A, o, sort(A, o, xs))

sort's output is sorted.

law bump_swap provedsource · line 152 · raw

@a:Bool -> @b:Bool -> @-n:Nat -> {bump(a, bump(b, n)) == bump(b, bump(a, n)) : Nat}

law insert_count.go provedsource · line 177 · raw

@-A:Data -> @-eq:(@_:A -> @_:A -> Bool) -> @-o:0x5f97f469d15c04a181dae0e4e64e1d3d/src/class.Ord<A> -> @+y:A -> @+x:A -> @+h:A -> @+t:List<&2, A> -> @-rec:(@_:Unit -> List<&2, A>) -> @ih:{bump(eq(y, x), count(A, eq, y, t)) == count(A, eq, y, rec(Unit{})) : Nat} -> @c:Or(0x5f97f469d15c04a181dae0e4e64e1d3d/src/class.Ord.R(A, o, x, h), 0x5f97f469d15c04a181dae0e4e64e1d3d/src/class.Ord.R(A, o, h, x)) -> {bump(eq(y, x), count(A, eq, y, h <> t)) == count(A, eq, y, insert.go(A, o, x, h, t, rec, c)) : Nat}

law insert_count provedsource · line 198 · raw

@-A:Data -> @-o:0x5f97f469d15c04a181dae0e4e64e1d3d/src/class.Ord<A> -> @-eq:(@_:A -> @_:A -> Bool) -> @+y:A -> @+x:A -> @xs:List<&2, A> -> {bump(eq(y, x), count(A, eq, y, xs)) == count(A, eq, y, insert(A, o, x, xs)) : Nat}

law sort_count provedsource · line 216 · raw

@-A:Data -> @-o:0x5f97f469d15c04a181dae0e4e64e1d3d/src/class.Ord<A> -> @-eq:(@_:A -> @_:A -> Bool) -> @+y:A -> @xs:List<&2, A> -> {count(A, eq, y, xs) == count(A, eq, y, sort(A, o, xs)) : Nat}

sort keeps every element's count.

Definitions

def insert.go source · line 35 · raw

@-A:Data -> @-o:0x5f97f469d15c04a181dae0e4e64e1d3d/src/class.Ord<A> -> @x:A -> @h:A -> @t:List<&2, A> -> @rec:(@_:Unit -> List<&2, A>) -> @c:Or(0x5f97f469d15c04a181dae0e4e64e1d3d/src/class.Ord.R(A, o, x, h), 0x5f97f469d15c04a181dae0e4e64e1d3d/src/class.Ord.R(A, o, h, x)) -> List<&2, A>

insert's step after comparing x with h. The recursive insert is passed as a thunk so that the x-first branch does not run it.

def bump source · line 145 · raw

@b:Bool -> @n:Nat -> Nat

Templates

template from source · line 18 · raw

@-A:Data -> @-o:0x5f97f469d15c04a181dae0e4e64e1d3d/src/class.Ord<A> -> @lo:A -> @xs:List<&2, A> -> Type

every element is at least lo, and the list ascends

template Sorted source · line 26 · raw

@-A:Data -> @-o:0x5f97f469d15c04a181dae0e4e64e1d3d/src/class.Ord<A> -> @xs:List<&2, A> -> Type

the list ascends

template insert source · line 42 · raw

@-A:Data -> @-o:0x5f97f469d15c04a181dae0e4e64e1d3d/src/class.Ord<A> -> @+x:A -> @xs:List<&2, A> -> List<&2, A>

template sort source · line 49 · raw

@-A:Data -> @-o:0x5f97f469d15c04a181dae0e4e64e1d3d/src/class.Ord<A> -> @xs:List<&2, A> -> List<&2, A>

template count source · line 170 · raw

@-A:Data -> @-eq:(@_:A -> @_:A -> Bool) -> @+y:A -> @xs:List<&2, A> -> Nat

how many elements of xs ~eq calls equal to y