Copyright	(c) Artem Mavrin 2021
License	BSD3
Maintainer	artemvmavrin@gmail.com
Stability	experimental
Portability	POSIX
Safe Haskell	Safe
Language	Haskell2010

AutoProof.Internal.Utils.DList

Description

Simple difference list implementation. Difference lists are an abstraction that enables constant-time concatenation of lists using function composition. This is a generalization of the ShowS type.

See https://wiki.haskell.org/Difference_list.

Synopsis

type DList a = [a] -> [a]
fromList :: [a] -> DList a
toList :: DList a -> [a]
toSet :: Ord a => DList a -> Set a
cons :: a -> DList a -> DList a
empty :: DList a
singleton :: a -> DList a

Documentation

type DList a = [a] -> [a] Source #

Difference list. See https://wiki.haskell.org/Difference_list.

Difference lists are concatenated by function composition.

>>> d1 = fromList [1, 2, 3]
>>> d2 = fromList [4, 5, 6]
>>> d3 = fromList [7, 8, 9]
>>> toList (d1 . d2 . d3)
[1,2,3,4,5,6,7,8,9]

fromList :: [a] -> DList a Source #

Convert a list into a difference list.

toList :: DList a -> [a] Source #

Convert a difference list into a list.

toSet :: Ord a => DList a -> Set a Source #

Convert a difference list into a set.

cons :: a -> DList a -> DList a Source #

Prepend an element to a difference list.

>>> toList (cons 0 (fromList [1, 2, 3]))
[0,1,2,3]

empty :: DList a Source #

Empty difference list.

>>> (toList empty) :: [()]
[]

singleton :: a -> DList a Source #

Singleton difference list.

>>> toList $ (singleton 0) . (singleton 1)
[0,1]