[Everything.agda is now generated automatically by darcs dist. Nils Anders Danielsson **20090423145120 Ignore-this: 5b63963c6ababe0d3320e1fb332d39b0 ] hunk ./Everything.agda 1 ------------------------------------------------------------------------- --- All library modules, along with short descriptions ------------------------------------------------------------------------- - --- Note that this module is automatically generated by the --- GenerateDocs program, and that core modules are not included. - -module Everything where - --- Definitions of algebraic structures like monoids and rings --- (packed in records together with setoids and operations) -import Algebra - --- Properties of functions, such as associativity and commutativity -import Algebra.FunctionProperties - --- Morphisms between algebraic structures -import Algebra.Morphism - --- Some defined operations (multiplication by natural number and --- exponentiation) -import Algebra.Operations - --- Some derivable properties -import Algebra.Props.AbelianGroup - --- Some derivable properties -import Algebra.Props.BooleanAlgebra - --- Some derivable properties -import Algebra.Props.DistributiveLattice - --- Some derivable properties -import Algebra.Props.Group - --- Some derivable properties -import Algebra.Props.Lattice - --- Some derivable properties -import Algebra.Props.Ring - --- Solver for commutative ring or semiring equalities -import Algebra.RingSolver - hiding (module AlmostCommutativeRing) -- To work around a bug in Agda 2.2.2. - --- Commutative semirings with some additional structure ("almost" --- commutative rings), used by the ring solver -import Algebra.RingSolver.AlmostCommutativeRing - --- Some boring lemmas used by the ring solver -import Algebra.RingSolver.Lemmas - --- Instantiates the ring solver with two copies of the same ring -import Algebra.RingSolver.Simple - --- Some algebraic structures (not packed up with setoids and --- operations) -import Algebra.Structures - --- Applicative functors -import Category.Applicative - --- Indexed applicative functors -import Category.Applicative.Indexed - --- Functors -import Category.Functor - --- Monads -import Category.Monad - --- A delimited continuation monad -import Category.Monad.Continuation - --- The identity monad -import Category.Monad.Identity - --- Indexed monads -import Category.Monad.Indexed - --- The partiality monad -import Category.Monad.Partiality - --- The state monad -import Category.Monad.State - --- Type used to make recursive arguments coinductive -import Coinduction - --- AVL trees -import Data.AVL - --- Finite maps with indexed keys and values, based on AVL trees -import Data.AVL.IndexedMap - --- Finite sets, based on AVL trees -import Data.AVL.Sets - --- A binary representation of natural numbers -import Data.Bin - --- Booleans -import Data.Bool - --- A bunch of properties -import Data.Bool.Properties - --- Showing booleans -import Data.Bool.Show - --- Bounded vectors -import Data.BoundedVec - --- Bounded vectors (inefficient, concrete implementation) -import Data.BoundedVec.Inefficient - --- Characters -import Data.Char - --- "Finite" sets indexed on coinductive "natural" numbers -import Data.Cofin - --- Coinductive lists -import Data.Colist - --- Coinductive "natural" numbers -import Data.Conat - --- Coinductive vectors -import Data.Covec - --- Lists with fast append -import Data.DifferenceList - --- Natural numbers with fast addition (for use together with --- DifferenceVec) -import Data.DifferenceNat - --- Vectors with fast append -import Data.DifferenceVec - --- Digits and digit expansions -import Data.Digit - --- Empty type -import Data.Empty - --- Empty type (in Set1) -import Data.Empty1 - --- Finite sets -import Data.Fin - --- Decision procedures for finite sets and subsets of finite sets -import Data.Fin.Dec - --- Properties related to Fin, and operations making use of these --- properties (or other properties not available in Data.Fin) -import Data.Fin.Props - --- Subsets of finite sets -import Data.Fin.Subset - --- Some properties about subsets -import Data.Fin.Subset.Props - --- Simple combinators working solely on and with functions -import Data.Function - --- Directed acyclic multigraphs -import Data.Graph.Acyclic - --- Integers -import Data.Integer - --- Lists -import Data.List - --- List equality -import Data.List.Equality - --- Non-empty lists -import Data.List.NonEmpty - --- Properties of non-empty lists -import Data.List.NonEmpty.Properties - --- List-related properties -import Data.List.Properties - --- Lists parameterised on things in Set1 -import Data.List1 - --- Finite maps, i.e. lookup tables (currently only some type --- signatures) -import Data.Map - --- The Maybe type -import Data.Maybe - --- Natural numbers -import Data.Nat - --- Coprimality -import Data.Nat.Coprimality - --- Integer division -import Data.Nat.DivMod - --- Divisibility -import Data.Nat.Divisibility - --- Greatest common divisor -import Data.Nat.GCD - --- A bunch of properties about natural number operations -import Data.Nat.Properties - --- Showing natural numbers -import Data.Nat.Show - --- Products -import Data.Product - --- Products implemented using records -import Data.Product.Record - --- Products (variants for Set1) -import Data.Product1 - --- Finite sets (currently only some type signatures) -import Data.Sets - --- Signs -import Data.Sign - --- The reflexive transitive closures of McBride, Norell and Jansson -import Data.Star - --- Bounded vectors (inefficient implementation) -import Data.Star.BoundedVec - --- Decorated star-lists -import Data.Star.Decoration - --- Environments (heterogeneous collections) -import Data.Star.Environment - --- Finite sets defined in terms of Data.Star -import Data.Star.Fin - --- Lists defined in terms of Data.Star -import Data.Star.List - --- Natural numbers defined in terms of Data.Star -import Data.Star.Nat - --- Pointers into star-lists -import Data.Star.Pointer - --- Some properties related to Data.Star -import Data.Star.Properties - --- Vectors defined in terms of Data.Star -import Data.Star.Vec - --- Streams -import Data.Stream - --- Strings -import Data.String - --- Sums (disjoint unions) -import Data.Sum - --- The unit type -import Data.Unit - --- The unit type (in Set1) -import Data.Unit1 - --- Vectors -import Data.Vec - --- Semi-heterogeneous vector equality -import Data.Vec.Equality - --- Code for converting Vec n A → B to and from n-ary functions -import Data.Vec.N-ary - --- Code for converting Vec₁ n A → B to and from n-ary functions -import Data.Vec.N-ary1 - --- Some Vec-related properties -import Data.Vec.Properties - --- Vectors parameterised on types in Set1 -import Data.Vec1 - --- Types used (only) when calling out to Haskell via the FFI -import Foreign.Haskell - --- IO -import IO - --- Primitive IO: simple bindings to Haskell types and functions -import IO.Primitive - --- An abstraction of various forms of recursion/induction -import Induction - --- Lexicographic induction -import Induction.Lexicographic - --- Various forms of induction for natural numbers -import Induction.Nat - --- Well-founded induction -import Induction.WellFounded - --- A variant of Induction for Set1 -import Induction1 - --- One form of induction for natural numbers -import Induction1.Nat - --- Well-founded induction -import Induction1.WellFounded - --- Properties of homogeneous binary relations -import Relation.Binary - --- Some properties imply others -import Relation.Binary.Consequences - --- Convenient syntax for equational reasoning -import Relation.Binary.EqReasoning - --- Many properties which hold for _∼_ also hold for flip₁ _∼_ -import Relation.Binary.Flip - --- (Some) function setoids -import Relation.Binary.FunctionLifting - --- Heterogeneous equality -import Relation.Binary.HeterogeneousEquality - --- Conversion of ≤ to <, along with a number of properties -import Relation.Binary.NonStrictToStrict - --- Many properties which hold for _∼_ also hold for _∼_ on₁ f -import Relation.Binary.On - --- Order morphisms -import Relation.Binary.OrderMorphism - --- Convenient syntax for "equational reasoning" using a partial order -import Relation.Binary.PartialOrderReasoning - --- Convenient syntax for "equational reasoning" using a preorder -import Relation.Binary.PreorderReasoning - --- Lexicographic products of binary relations -import Relation.Binary.Product.NonStrictLex - --- Pointwise products of binary relations -import Relation.Binary.Product.Pointwise - --- Lexicographic products of binary relations -import Relation.Binary.Product.StrictLex - --- Propositional (intensional) equality -import Relation.Binary.PropositionalEquality - --- Propositional equality -import Relation.Binary.PropositionalEquality1 - --- Properties satisfied by decidable total orders -import Relation.Binary.Props.DecTotalOrder - --- Properties satisfied by posets -import Relation.Binary.Props.Poset - --- Properties satisfied by strict partial orders -import Relation.Binary.Props.StrictPartialOrder - --- Properties satisfied by strict partial orders -import Relation.Binary.Props.StrictTotalOrder - --- Properties satisfied by total orders -import Relation.Binary.Props.TotalOrder - --- Helpers intended to ease the development of "tactics" which use --- proof by reflection -import Relation.Binary.Reflection - --- Some simple binary relations -import Relation.Binary.Simple - --- Convenient syntax for "equational reasoning" using a strict partial --- order -import Relation.Binary.StrictPartialOrderReasoning - --- Conversion of < to ≤, along with a number of properties -import Relation.Binary.StrictToNonStrict - --- Sums of binary relations -import Relation.Binary.Sum - --- Operations on nullary relations (like negation and decidability) -import Relation.Nullary - --- Operations on and properties of decidable relations -import Relation.Nullary.Decidable - --- Properties related to negation -import Relation.Nullary.Negation - --- Products of nullary relations -import Relation.Nullary.Product - --- Sums of nullary relations -import Relation.Nullary.Sum - --- A universe of proposition functors, along with some properties -import Relation.Nullary.Universe - --- Unary relations -import Relation.Unary - --- Unary relations (variant for Set1) -import Relation.Unary1 - --- Sizes for Agda's sized types -import Size rmfile ./Everything.agda hunk ./GenerateDocs.hs 3 --- This program requires that the filepath and process packages from +-- This program requires that the filepath and FileManip packages from hunk ./GenerateDocs.hs 6 -import Data.List +import qualified Data.List as List +import Control.Applicative hunk ./GenerateDocs.hs 12 -import System.Process +import System.FilePath.Find hunk ./GenerateDocs.hs 23 - header <- readFile headerFile - allFiles <- readProcess "darcs" ["show", "files"] "" - let modules = filter isLibraryModule $ sort $ lines allFiles + header <- readFile headerFile + modules <- filter isLibraryModule . List.sort <$> + find always + (extension ~~? ".agda" ||? extension ~~? ".lagda") + "." hunk ./GenerateDocs.hs 39 - , "This program has to be run from the library's base directory." + , "This program should be run in the base directory of a clean checkout of" + , "the library." hunk ./GenerateDocs.hs 65 - , (info, d2 : rest) <- span ("-- " `isPrefixOf`) ss + , (info, d2 : rest) <- span ("-- " `List.isPrefixOf`) ss changepref predist runhaskell GenerateDocs.hs