README.Data

------------------------------------------------------------------------
-- The Agda standard library
--
-- An explanation about how data types are laid out in the standard
-- library.
------------------------------------------------------------------------

{-# OPTIONS --sized-types --guardedness #-}

module README.Data where

-- The top-level folder `Data` contains all the definitions of datatypes
-- and their associated properties.

-- Datatypes can broadly split into two categories
--   i) "Basic" datatypes which do not take other datatypes as generic
--      arguments (Nat, String, Fin, Bool, Char etc.)
--   ii) "Container" datatypes which take other generic datatypes as
--   arguments, (List, Vec, Sum, Product, Maybe, AVL trees etc.)

------------------------------------------------------------------------
-- Basic datatypes
------------------------------------------------------------------------

-- Basic datatypes are usually organised as follows:


-- 1. A `Base` module which either contains the definition of the
-- datatype or reimports it from the builtin modules, along with common
-- functions, operations and relations over elements of the datatype.

import Data.Nat.Base
import Data.Integer.Base
import Data.Char.Base
import Data.String.Base
import Data.Bool.Base

-- Commonly these modules don't need to be imported directly as their
-- contents is re-exported by the top level module (see below).


-- 2. A `Properties` module which contains the basic properties of the
-- functions, operations and relations contained in the base module.

import Data.Nat.Properties
import Data.Integer.Properties
import Data.Char.Properties
import Data.String.Properties
import Data.Bool.Properties


-- 3. A top-level module which re-exports the contents of the base
-- module as well as various queries (i.e. decidability proofs) from the
-- properties file.

import Data.Nat
import Data.Integer
import Data.Char
import Data.String
import Data.Bool


-- 4. A `Solver` module (for those datatypes that have an algebraic solver)
-- which can be used to automatically solve equalities over the basic datatype.

import Data.Nat.Solver
import Data.Integer.Solver
import Data.Bool.Solver


-- 5. More complex operations and relations are commonly found in their
-- own module beneath the top-level directory. For example:

import Data.Nat.DivMod
import Data.Integer.Coprimality

-- Note that eventually there is a plan to re-organise the library to
-- have the top-level module export a far wider range of properties and
-- additional operations in order to minimise the number of imports
-- needed. Currently it is necessary to import each of these separately
-- however.

------------------------------------------------------------------------
-- Container datatypes
------------------------------------------------------------------------

-- 1. As with basic datatypes, a `Base` module which contains the
-- definition of the datatype, along with common functions and
-- operations over that data. Unlike basic datatypes, the `Base` module
-- for container datatypes does not export any relations or predicates
-- over the datatype (see the `Relation` section below).

import Data.List.Base
import Data.Maybe.Base
import Data.Sum.Base

-- Commonly these modules don't need to be imported directly as their
-- contents is re-exported by the top level module (see below).


-- 2. As with basic datatypes, a `Properties` module which contains the
-- basic properties of the functions, operations and contained in the
-- base module.

import Data.List.Properties
import Data.Maybe.Properties
import Data.Sum.Properties


-- 3. As with basic datatypes, a top-level module which re-exports the
-- contents of the base module. In some cases this may also contain
-- additional functions which could not be placed into the corresponding
-- Base module because of cyclic dependencies.

import Data.List
import Data.Maybe
import Data.Sum


-- 4. A `Relation.Binary` folder where binary relations over the datatypes
-- are stored. Because relations over container datatypes often depend on
-- relations over the parameter datatype, this differs from basic datatypes
-- where the binary relations are usually defined in the `Base` module, e.g.
-- equality over the type `List A` depends on equality over type `A`.

-- For example the `Pointwise` relation that takes a relation over the
-- underlying type A and lifts it to the container parameterised can be found
-- as follows:

import Data.List.Relation.Binary.Pointwise
import Data.Maybe.Relation.Binary.Pointwise
import Data.Sum.Relation.Binary.Pointwise

-- Another useful subfolder in the `Data.X.Relation.Binary` folders is the
-- `Data.X.Relation.Binary.Equality` folder which contains various forms of
-- equality over the datatype.


-- 5. A `Relation.Unary` folder where unary relations, or predicates,
-- over the datatypes are stored. These can be viewed as properties
-- over a single list.

-- For example a common, useful example is `Data.X.Relation.Unary.Any`
-- that contains the types of proofs that at least one element in the
-- container satisfies some predicate/property.

import Data.List.Relation.Unary.Any
import Data.Vec.Relation.Unary.Any
import Data.Maybe.Relation.Unary.Any

-- Alternatively the `Data.X.Relation.Unary.All` module contains the
-- type of proofs that all elements in the container satisfy some
-- property.

import Data.List.Relation.Unary.All
import Data.Vec.Relation.Unary.All
import Data.Maybe.Relation.Unary.All


-- 6. An `Effectful` module/folder that contains effectful
-- interpretations of the datatype.

import Data.List.Effectful
import Data.Maybe.Effectful
import Data.Sum.Effectful.Left
import Data.Sum.Effectful.Right


-- 7. A `Function` folder that contains lifting of various types of
-- functions (e.g. injections, surjections, bijections, inverses) to
-- the datatype.

import Data.Sum.Function.Propositional
import Data.Sum.Function.Setoid
import Data.Product.Function.Dependent.Propositional
import Data.Product.Function.Dependent.Setoid


------------------------------------------------------------------------
-- Full list of documentation for the Data folder
------------------------------------------------------------------------

-- Some examples showing where the natural numbers/integers and some
-- related operations and properties are defined, and how they can be
-- used:

import README.Data.Nat
import README.Data.Nat.Induction

import README.Data.Integer

-- Some examples showing how the AVL tree module can be used.

import README.Data.Tree.AVL

-- Some examples showing how List module can be used.

import README.Data.List

-- Some examples showing how the Fresh list can be used.

import README.Data.List.Fresh

-- Example of an encoding of record types with manifest fields and "with".

import README.Data.Record

-- Example use case for a trie: a wee generic lexer

import README.Data.Trie.NonDependent

-- Examples of equational reasoning about vectors of non-definitionally
-- equal lengths.

import README.Data.Vec.Relation.Binary.Equality.Cast

-- Examples how (indexed) containers and constructions over them (free
-- monad, least fixed point, etc.) can be used

import README.Data.Container.FreeMonad
import README.Data.Container.Indexed.VectorExample
import README.Data.Container.Indexed.MultiSortedAlgebraExample

-- Wrapping n-ary relations into a record definition so type-inference
-- remembers the things being related.

import README.Data.Wrap

-- Specifying the default value a function's argument should take if it
-- is not passed explicitly.

import README.Data.Default