.gitattributes

+.travis.yml merge=ours

.gitignore

@@ -13,4 +13,6 @@
 dist
 Everything.agda
 EverythingSafe.agda
+EverythingSafeGuardedness.agda
+EverythingSafeSizedTypes.agda
 html

.travis.yml

@@ -2,11 +2,9 @@ language: c
 branches:
   only:
   - master
-  - travis
+  - experimental
 
-sudo: enabled
-
-dist: trusty
+dist: xenial
 
 cache:
   directories:
@@ -14,14 +12,12 @@ cache:
 
 matrix:
   include:
-    - env: TEST=MAIN GHC_VER=8.0.2 BUILD=CABAL CABAL_VER=1.24
+    - env: TEST=MAIN GHC_VER=8.4.4 BUILD=CABAL CABAL_VER=2.2
       addons:
         apt:
           packages:
-            - alex-3.1.7
-            - cabal-install-1.24
-            - ghc-8.0.2
-            - happy-1.19.5
+            - cabal-install-2.2
+            - ghc-8.4.4
           sources:
             - hvr-ghc
 
@@ -32,9 +28,10 @@ install:
   - cabal update
   - sed -i 's/^jobs:/-- jobs:/' $HOME/.cabal/config
   # checking whether .ghc is still valid
-  - cabal install --only-dependencies --dry -v agda > $HOME/installplan.txt
+  - cabal install alex happy
+  - cabal install --only-dependencies --dry -v > $HOME/installplan.txt
   - sed -i -e '1,/^Resolving /d' $HOME/installplan.txt; cat $HOME/installplan.txt
-  - touch $HOME/.cabsnap/intallplan.txt
+  - touch $HOME/.cabsnap/installplan.txt
   - mkdir -p $HOME/.cabsnap/ghc $HOME/.cabsnap/lib $HOME/.cabsnap/share $HOME/.cabsnap/bin
   - if diff -u $HOME/.cabsnap/installplan.txt $HOME/installplan.txt;
     then
@@ -48,7 +45,7 @@ install:
       mkdir -p $HOME/.ghc $HOME/.cabal/lib $HOME/.cabal/share $HOME/.cabal/bin;
     fi
   - cabal install cpphs
-  - cabal install agda
+  - cabal install Agda
   # snapshot package-db on cache miss
   - echo "snapshotting package-db to build-cache";
     mkdir $HOME/.cabsnap;
@@ -66,19 +63,25 @@ install:
   # setting up travis-specific scripts and files
   - cp travis/* .
 
+before_script:
+  - export RTS_OPTIONS="+RTS -M2.5G -H2.5G -A128M -RTS"
+
 script:
   # generating index.agda
   - ./index.sh
   # detecting whitespace violations
   - make check-whitespace
+  # expose the value of RTS_OPTIONS
+  - echo $RTS_OPTIONS
   # checking safe modules build with --safe
-  # - agda -i . -i src/ --safe safe.agda
+  - agda $RTS_OPTIONS -i . -i src/ --safe EverythingSafeGuardedness.agda
+  - agda $RTS_OPTIONS -i . -i src/ --safe EverythingSafeSizedTypes.agda
   # detecting basic compilation errors
-  - agda -i . -i src/ -c --no-main Everything.agda
+  - agda $RTS_OPTIONS -i . -i src/ -c --no-main Everything.agda
   # building the docs
-  - agda -i . -i src/ --html safe.agda
-  - agda -i . -i src/ --html index.agda
-  # moving everything at the root
+  - agda $RTS_OPTIONS -i . -i src/ --html safe.agda
+  - agda $RTS_OPTIONS -i . -i src/ --html index.agda
+  # moving everything to the doc directory
   - mv html/* .
 
 after_success:
@@ -88,6 +91,7 @@ after_success:
   - git config --global user.email "travis-ci-bot@travis.fake"
   - git remote add upstream https://$GH_TOKEN@github.com/agda/agda-stdlib.git &>/dev/null
   - git fetch upstream && git reset upstream/gh-pages
+  - git checkout HEAD -- v0.16/ v0.17/ v1.0/ experimental/
   - git add -f \*.html
   - git commit -m "Automatic HTML update via Travis"
   - if [ "$TRAVIS_PULL_REQUEST" = "false" ] && [ "$TRAVIS_BRANCH" = "master" ];

CHANGELOG/v1.0.1.md

+Version 1.0.1
+=============
+
+The library has been tested using Agda version 2.6.0.
+
+Important changes since 1.0:
+
+* Fixed unsolved metas in `Relation.Binary.Reasoning.MultiSetoid` and
+  added missing combinator `_≈˘⟨_⟩_`.

GNUmakefile

-AGDA=agda
+AGDA_EXEC=agda
+RTS_OPTIONS=+RTS -M2.5G -H2.5G -A128M -RTS
+AGDA=$(AGDA_EXEC) $(RTS_OPTIONS)
 
 # Before running `make test` the `fix-agda-whitespace` program should
 # be installed:

GenerateEverything.hs

 {-# LANGUAGE PatternGuards #-}
 
-import qualified Data.List as List
 import Control.Applicative
+
+import qualified Data.List as List
+
 import System.Environment
-import System.IO
 import System.Exit
 import System.FilePath
 import System.FilePath.Find
+import System.IO
 
 headerFile     = "Header"
 allOutputFile  = "Everything"
 safeOutputFile = "EverythingSafe"
 srcDir         = "src"
 
+---------------------------------------------------------------------------
+-- Files with a special status
+
+-- | Checks whether a module is declared (un)safe
+
 unsafeModules :: [FilePath]
 unsafeModules = map toAgdaFilePath
-  [ "Data.Char.Unsafe"
+  [ "Codata.Musical.Cofin"
+  , "Codata.Musical.Colist"
+  , "Codata.Musical.Colist.Infinite-merge"
+  , "Codata.Musical.Conat"
+  , "Codata.Musical.Costring"
+  , "Codata.Musical.Covec"
+  , "Codata.Musical.M"
+  , "Codata.Musical.Stream"
+  , "Data.Char.Unsafe"
   , "Data.Float.Unsafe"
   , "Data.Nat.Unsafe"
   , "Data.Nat.DivMod.Unsafe"
   , "Data.String.Unsafe"
   , "Data.Word.Unsafe"
+  , "Debug.Trace"
+  , "Foreign.Haskell"
+  , "Foreign.Haskell.Maybe"
+  , "Foreign.Haskell.Pair"
   , "IO"
   , "IO.Primitive"
   , "Reflection"
@@ -34,6 +53,166 @@ unsafeModules = map toAgdaFilePath
     , ".agda"
     ]
 
+isUnsafeModule :: FilePath -> Bool
+isUnsafeModule =
+  -- GA 2019-02-24: it is crucial to use an anonymous lambda
+  -- here so that `unsafeModules` is shared between all calls
+  -- to `isUnsafeModule`.
+  \ fp -> unqualifiedModuleName fp == "Unsafe"
+       || fp `elem` unsafeModules
+
+-- | Checks whether a module is declared as using K
+
+isWithKModule :: FilePath -> Bool
+isWithKModule =
+  -- GA 2019-02-24: it is crucial to use an anonymous lambda
+  -- here so that `withKModules` is shared between all calls
+  -- to `isWithKModule`.
+  \ fp -> unqualifiedModuleName fp == "WithK"
+       || fp `elem` withKModules
+
+  where
+
+  withKModules :: [FilePath]
+  withKModules = map modToFile
+    [ "Axiom.Extensionality.Heterogeneous"
+    , "Data.Char.Unsafe"
+    , "Data.Float.Unsafe"
+    , "Data.Nat.Unsafe"
+    , "Data.Nat.DivMod.Unsafe"
+    , "Data.Star.BoundedVec"
+    , "Data.Star.Decoration"
+    , "Data.Star.Environment"
+    , "Data.Star.Fin"
+    , "Data.Star.Pointer"
+    , "Data.Star.Vec"
+    , "Data.String.Unsafe"
+    , "Data.Word.Unsafe"
+    , "Reflection"
+    , "Relation.Binary.HeterogeneousEquality"
+    , "Relation.Binary.HeterogeneousEquality.Core"
+    , "Relation.Binary.HeterogeneousEquality.Quotients.Examples"
+    , "Relation.Binary.HeterogeneousEquality.Quotients"
+    , "Relation.Binary.PropositionalEquality.TrustMe"
+    ]
+
+unqualifiedModuleName :: FilePath -> String
+unqualifiedModuleName = dropExtension . takeFileName
+
+-- | Returns 'True' for all Agda files except for core modules.
+
+isLibraryModule :: FilePath -> Bool
+isLibraryModule f =
+  takeExtension f `elem` [".agda", ".lagda"]
+  && unqualifiedModuleName f /= "Core"
+
+
+---------------------------------------------------------------------------
+-- Analysing library files
+
+-- | Extracting the header.
+
+-- It needs to have the form:
+-- ------------------------------------------------------------------------
+-- -- The Agda standard library
+-- --
+-- -- Description of the module
+-- ------------------------------------------------------------------------
+
+extractHeader :: FilePath -> [String] -> [String]
+extractHeader mod = extract
+  where
+  delimiter = all (== '-')
+
+  extract (d1 : "-- The Agda standard library" : "--" : ss)
+    | delimiter d1
+    , (info, d2 : rest) <- span ("-- " `List.isPrefixOf`) ss
+    , delimiter d2
+    = info
+  extract (d1 : _)
+    | not (delimiter d1)
+    , last d1 == '\r'
+    = error $ mod ++ " contains \\r, probably due to git misconfiguration; maybe set autocrf to input?"
+  extract _ = error $ unwords [ mod ++ " is malformed."
+                              , "It needs to have a module header."
+                              , "Please see other existing files or consult HACKING.md."
+                              ]
+
+-- | A crude classifier looking for lines containing options & trying to guess
+--   whether the safe file is using either @--guardedness@ or @--sized-types@
+
+data Safety = Unsafe | Safe | SafeGuardedness | SafeSizedTypes
+  deriving (Eq)
+
+classify :: FilePath -> [String] -> Safety
+classify fp ls
+  -- We start with sanity checks
+  | isUnsafe && safe          = error $ fp ++ contradiction "unsafe" "safe"
+  | not (isUnsafe || safe)    = error $ fp ++ uncategorized "unsafe" "safe"
+  | isWithK && withoutK       = error $ fp ++ contradiction "as relying on K" "without-K"
+  | isWithK && not withK      = error $ fp ++ missingWithK
+  | not (isWithK || withoutK) = error $ fp ++ uncategorized "as relying on K" "without-K"
+  -- And then perform the actual classification
+  | isUnsafe                  = Unsafe
+  | guardedness               = SafeGuardedness
+  | sizedtypes                = SafeSizedTypes
+  | safe                      = Safe
+  -- We know that @not (isUnsafe || safe)@, all cases are covered
+  | otherwise                 = error "IMPOSSIBLE"
+
+  where
+
+    -- based on declarations
+    isWithK  = isWithKModule fp
+    isUnsafe = isUnsafeModule fp
+
+    -- based on detected OPTIONS
+    guardedness = option "--guardedness"
+    sizedtypes  = option "--sized-types"
+    safe        = option "--safe"
+    withK       = option "--with-K"
+    withoutK    = option "--without-K"
+
+    -- GA 2019-02-24: note that we do not reprocess the whole module for every
+    -- option check: the shared @options@ definition ensures we only inspect a
+    -- handful of lines (at most one, ideally)
+    option str = let detect = List.isSubsequenceOf ["{-#", "OPTIONS", str, "#-}"]
+                  in not $ null $ filter detect options
+    options    = words <$> filter (List.isInfixOf "OPTIONS") ls
+
+    -- formatting error messages
+    contradiction d o = unwords
+      [ " is declared", d, "but uses the", "--" ++ o, "option." ]
+    uncategorized d o = unwords
+      [ " is not declared", d, "but not using the", "--" ++ o, "option either." ]
+
+    missingWithK = " is declared as relying on K but not using the --with-K option."
+
+-- | Analyse a file: extracting header and classifying it.
+
+data LibraryFile = LibraryFile
+  { filepath   :: FilePath -- ^ FilePath of the source file
+  , header     :: [String] -- ^ All lines in the headers are already prefixed with \"-- \".
+  , safety     :: Safety   -- ^ Safety options used by the module
+  }
+
+analyse :: FilePath -> IO LibraryFile
+analyse fp = do
+  ls <- lines <$> readFileUTF8 fp
+  return $ LibraryFile
+    { filepath   = fp
+    , header     = extractHeader fp ls
+    , safety     = classify fp ls
+    }
+
+---------------------------------------------------------------------------
+-- Collecting all non-Core library files, analysing them and generating
+-- 4 files:
+-- Everything.agda                 all the modules
+-- EverythingSafe.agda             all the safe modules (may be incompatible)
+-- EverythingSafeGuardedness.agda  all the safe modules using --guardedness
+-- EverythingSafeSizedTypes.agda   all the safe modules using --sized-types
+
 main = do
   args <- getArgs
   case args of
@@ -45,21 +224,37 @@ main = do
                find always
                     (extension ==? ".agda" ||? extension ==? ".lagda")
                     srcDir
-  headers <- mapM extractHeader modules
+  libraryfiles <- mapM analyse modules
 
   let mkModule str = "module " ++ str ++ " where"
-  let content = zip modules headers
 
   writeFileUTF8 (allOutputFile ++ ".agda") $
     unlines [ header
             , mkModule allOutputFile
-            , format content
+            , format libraryfiles
             ]
 
   writeFileUTF8 (safeOutputFile ++ ".agda") $
     unlines [ header
+            , "{-# OPTIONS --guardedness --sized-types #-}\n"
             , mkModule safeOutputFile
-            , format $ filter ((`notElem` unsafeModules) . fst) content
+            , format $ filter ((Unsafe /=) . safety) libraryfiles
+            ]
+
+  let safeGuardednessOutputFile = safeOutputFile ++ "Guardedness"
+  writeFileUTF8 (safeGuardednessOutputFile ++ ".agda") $
+    unlines [ header
+            , "{-# OPTIONS --safe --guardedness #-}\n"
+            , mkModule safeGuardednessOutputFile
+            , format $ filter ((SafeGuardedness ==) . safety) libraryfiles
+            ]
+
+  let safeSizedTypesOutputFile = safeOutputFile ++ "SizedTypes"
+  writeFileUTF8 (safeSizedTypesOutputFile ++ ".agda") $
+    unlines [ header
+            , "{-# OPTIONS --safe --sized-types #-}\n"
+            , mkModule safeSizedTypesOutputFile
+            , format $ filter ((SafeSizedTypes ==) . safety) libraryfiles
             ]
 
 -- | Usage info.
@@ -78,43 +273,16 @@ usage = unlines
   , "with the file " ++ headerFile ++ " inserted verbatim at the beginning."
   ]
 
--- | Returns 'True' for all Agda files except for core modules.
-
-isLibraryModule :: FilePath -> Bool
-isLibraryModule f =
-  takeExtension f `elem` [".agda", ".lagda"]
-  && dropExtension (takeFileName f) /= "Core"
-
--- | Reads a module and extracts the header.
-
-extractHeader :: FilePath -> IO [String]
-extractHeader mod = fmap (extract . lines) $ readFileUTF8 mod
-  where
-  delimiter = all (== '-')
-
-  extract (d1 : "-- The Agda standard library" : "--" : ss)
-    | delimiter d1
-    , (info, d2 : rest) <- span ("-- " `List.isPrefixOf`) ss
-    , delimiter d2
-    = info
-  extract (d1 : _)
-    | not (delimiter d1)
-    , last d1 == '\r'
-    = error $ mod ++ " contains \\r, probably due to git misconfiguration; maybe set autocrf to input?"
-  extract _ = error $ mod ++ " is malformed. It is required to have a module header. Please see other existing files or consult HACKING.md."
 
 -- | Formats the extracted module information.
 
-format :: [(FilePath, [String])]
-          -- ^ Pairs of module names and headers. All lines in the
-          -- headers are already prefixed with \"-- \".
-       -> String
+format :: [LibraryFile] -> String
 format = unlines . concat . map fmt
   where
-  fmt (mod, header) = "" : header ++ ["import " ++ fileToMod mod]
+  fmt lf = "" : header lf ++ ["import " ++ fileToMod (filepath lf)]
 
--- | Translates a file name to the corresponding module name. It is
--- assumed that the file name corresponds to an Agda module under
+-- | Translates back and forth between a file name and the corresponding module
+--   name. We assume that the file name corresponds to an Agda module under
 --   'srcDir'.
 
 fileToMod :: FilePath -> String
@@ -123,6 +291,12 @@ fileToMod = map slashToDot . dropExtension . makeRelative srcDir
   slashToDot c | isPathSeparator c = '.'
                | otherwise         = c
 
+modToFile :: String -> FilePath
+modToFile name = concat [ srcDir, [pathSeparator], map dotToSlash name, ".agda" ]
+  where
+  dotToSlash c | c == '.'  = pathSeparator
+               | otherwise = c
+
 -- | A variant of 'readFile' which uses the 'utf8' encoding.
 
 readFileUTF8 :: FilePath -> IO String

HACKING.md

@@ -11,48 +11,58 @@ How to make changes
 
 ### Fork and download the repository
 
-1. Create a fork by clicking `Fork` button at the top right of the [repository](https://github.com/agda/agda-stdlib).
+1. Create a fork by clicking `Fork` button at the top right of the
+   [repository](https://github.com/agda/agda-stdlib).
 
-2. If you are on a Mac, make sure that your git options has `autocrlf` set to `input`.  This can be done by executing
+2. If you are on a Mac, make sure that your git options has `autocrlf`
+   set  to `input`.  This can be done by executing
    ```
    git config --global core.autocrlf input
    ```
-   If you are on Windows, make sure that your editor can deal with Unix format files.
+   If you are on Windows, make sure that your editor can deal with Unix
+   format files.
 
-3. On the command line, and in a suitable folder, download your fork by running the command
+3. On the command line, and in a suitable folder, download your fork by
+   running the command
    ```
    git clone https://github.com/USER_NAME/agda-stdlib agda-stdlib-fork
    ```
 
-   where `USER_NAME` is your Git username. The folder `agda-stdlib-fork` should now contain a copy of the standard library.
+   where `USER_NAME` is your Git username. The folder `agda-stdlib-fork`
+   should now contain a copy of the standard library.
 
-4. Enter the folder `agda-stdlib-fork` and choose the correct branch of the library to make your changes on by running the
-   command
+4. Enter the folder `agda-stdlib-fork` and choose the correct branch of
+   the library to make your changes on by running the command
    ```
    git checkout X
    ```
-   where `X` should be `master` if your changes are compatible with the current released version of Agda, and `experimental`
-   if your changes require the development version of Agda.
+   where `X` should be `master` if your changes are compatible with the
+   current released version of Agda, and `experimental` if your changes
+   require the development version of Agda.
 
 ### Make your changes
 
-5. Make your proposed changes. Please try to obey existing conventions in the library.
-   See `agda-stdlib-fork/notes/style-guide.md` for a selection of the most important ones.
+5. Make your proposed changes. Please try to obey existing conventions
+   in the library. See `agda-stdlib-fork/notes/style-guide.md` for a
+   selection of the most important ones.
 
 6. Document your changes in `agda-stdlib-fork/CHANGELOG.md`.
 
-7. Ensure your changes are compatible with the rest of the library by running the commands
+7. Ensure your changes are compatible with the rest of the library by
+   running the commands
    ```
    make clean
    make test
    ```
-   inside the `agda-stdlib-fork` folder. Continue to correct any bugs thrown up until the tests are passed.
+   inside the `agda-stdlib-fork` folder. Continue to correct any bugs
+   thrown up until the tests are passed.
 
-   Your proposed changes MUST pass these tests. Note that the tests require the use of a tool called
-   `fix-agda-whitespace`. See the instructions at the end of this file for how to install this.
+   Your proposed changes MUST pass these tests. Note that the tests
+   require the use of a tool called `fix-agda-whitespace`. See the
+   instructions at the end of this file for how to install this.
 
-   If you are creating new modules, please make sure you are having a proper header,
-   and a brief description of what the module is for, e.g.
+   If you are creating new modules, please make sure you are having a
+   proper header, and a brief description of what the module is for, e.g.
    ```
    ------------------------------------------------------------------------
    -- The Agda standard library
@@ -61,10 +71,23 @@ How to make changes
    ------------------------------------------------------------------------
    ```
 
+   If possible, each module should use the options `--safe` and `--without-K`. You
+   can achieve this by placing the following pragma under the header and before
+   any other line of code (including the module name):
+   ```
+   {-# OPTIONS --without-K --safe #-}
+   ```
+
+   If a module cannot be made safe or needs the `--with-K` option then it should be
+   split into a module which is compatible with these options and an auxiliary
+   one which will:
+   * Either be called `SOME/PATH/Unsafe.agda` or `SOME/PATH/WithK.agda`
+   * Or explicitly declared as either unsafe or needing K in `GenerateEverything.hs`
 
 ### Upload your changes
 
-8. Use the `git add` command to add the files you have changed to your proposed commit.
+8. Use the `git add X` command to add changes to file `X` to the commit,
+   or `git add .` to add all the changed files.
 
 9. Run the command:
    ```
@@ -76,17 +99,35 @@ How to make changes
    ```
    git push
    ```
-11. Go to your fork on Github at `https://github.com/USER_NAME/agda-stdlib` and click the green `Compare & pull request` button to open a pull request.
 
-12. The standard library maintainers will then be made aware of your requested changes and should be in touch soon.
+11. Go to your fork on Github at `https://github.com/USER_NAME/agda-stdlib`
+        and follow the [official Git instructions](https://help.github.com/en/articles/creating-a-pull-request-from-a-fork)
+        to open a pull request to the main standard library repository.
+
+12. The library maintainers will then be made aware of your requested
+        changes and should be in touch soon.
+
+How to enforce whitespace policies
+----------------------------------
 
-Installing `fix-agda-whitespace`
---------------------------------
+### Installing fix-agda-whitespace
 
-This tool is kept in the main agda repository. It can be installed by following these instructions:
+This tool is kept in the main agda repository. It can be installed by
+following these instructions:
    ```
    git clone https://github.com/agda/agda
    cd agda/src/fix-agda-whitespace
    cabal install
    ```
 
+### Adding fix-agda-whitespace as a pre-commit hook
+
+You can add the following code to the file `.git/hooks/pre-commit` to
+get git to run fix-agda-whitespace before each `git commit` and ensure
+you are never committing anything with a whitespace violation:
+
+   ```
+   #!/bin/sh
+
+   fix-agda-whitespace --check
+   ```

LICENCE

-Copyright (c) 2007-2018 Nils Anders Danielsson, Ulf Norell, Shin-Cheng
+Copyright (c) 2007-2019 Nils Anders Danielsson, Ulf Norell, Shin-Cheng
 Mu, Bradley Hardy, Samuel Bronson, Dan Doel, Patrik Jansson,
 Liang-Ting Chen, Jean-Philippe Bernardy, Andrés Sicard-Ramírez,
 Nicolas Pouillard, Darin Morrison, Peter Berry, Daniel Brown,
 Simon Foster, Dominique Devriese, Andreas Abel, Alcatel-Lucent,
 Eric Mertens, Joachim Breitner, Liyang Hu, Noam Zeilberger, Érdi Gergő,
 Stevan Andjelkovic, Helmut Grohne, Guilhem Moulin, Noriyuki Ohkawa,
-Evgeny Kotelnikov, James Chapman, Wen Kokke, Matthew Daggitt, Jason Hu
+Evgeny Kotelnikov, James Chapman, Wen Kokke, Matthew Daggitt, Jason Hu,
+Sandro Stucki, Milo Turner, Zack Grannan, Lex van der Stoep
 and some anonymous contributors.
 
 Permission is hereby granted, free of charge, to any person obtaining a

README.agda

 module README where
 
 ------------------------------------------------------------------------
--- The Agda standard library, version 0.17
+-- The Agda standard library, version 1.1
 --
--- Authors: Nils Anders Danielsson, with contributions from Andreas
--- Abel, Stevan Andjelkovic, Jean-Philippe Bernardy, Peter Berry,
--- Bradley Hardy Joachim Breitner, Samuel Bronson, Daniel Brown,
--- James Chapman, Liang-Ting Chen, Matthew Daggitt, Dominique Devriese,
--- Dan Doel, Érdi Gergő, Helmut Grohne, Simon Foster, Liyang Hu,
--- Jason Hu, Patrik Jansson, Alan Jeffrey, Wen Kokke, Evgeny Kotelnikov,
--- Sergei Meshveliani, Eric Mertens, Darin Morrison, Guilhem Moulin,
--- Shin-Cheng Mu, Ulf Norell, Noriyuki Ohkawa, Nicolas Pouillard,
--- Andrés Sicard-Ramírez, Noam Zeilberger and some anonymous
--- contributors.
+-- Authors: Nils Anders Danielsson, Matthew Daggitt, Guillaume Allais
+-- with contributions from Andreas Abel, Stevan Andjelkovic,
+-- Jean-Philippe Bernardy, Peter Berry, Bradley Hardy Joachim Breitner,
+-- Samuel Bronson, Daniel Brown, James Chapman, Liang-Ting Chen,
+-- Dominique Devriese, Dan Doel, Érdi Gergő, Zack Grannan,
+-- Helmut Grohne, Simon Foster, Liyang Hu, Jason Hu, Patrik Jansson,
+-- Alan Jeffrey, Wen Kokke, Evgeny Kotelnikov, Sergei Meshveliani,
+-- Eric Mertens, Darin Morrison, Guilhem Moulin, Shin-Cheng Mu,
+-- Ulf Norell, Noriyuki Ohkawa, Nicolas Pouillard,
+-- Andrés Sicard-Ramírez, Lex van der Stoep, Sandro Stucki, Milo Turner,
+-- Noam Zeilberger and other anonymous contributors.
 ------------------------------------------------------------------------
 
--- This version of the library has been tested using Agda 2.5.4.1.
-
--- Note that no guarantees are currently made about forwards or
--- backwards compatibility, the library is still at an experimental
--- stage.
+-- This version of the library has been tested using Agda 2.6.0.1.
 
 -- The library comes with a .agda-lib file, for use with the library
 -- management system.
@@ -27,13 +24,6 @@ module README where
 -- Currently the library does not support the JavaScript compiler
 -- backend.
 
--- Contributions to this library are welcome (but to avoid wasted work
--- it is suggested that you discuss large changes before implementing
--- them). Please send contributions in the form of git pull requests,
--- patch bundles or ask for commmit rights to the repository.  It is
--- appreciated if every patch contains a single, complete change, and
--- if the coding style used in the library is adhered to.
-
 ------------------------------------------------------------------------
 -- Module hierarchy
 ------------------------------------------------------------------------
@@ -46,39 +36,56 @@ module README where
 --     properties needed to specify these structures (associativity,
 --     commutativity, etc.), and operations on and proofs about the
 --     structures.
+
+-- • Axiom
+--     Types and consequences of various additional axioms not
+--     necessarily included in Agda, e.g. uniqueness of identity
+--     proofs, function extensionality and excluded middle.
+
+import README.Axiom
+
 -- • Category
 --     Category theory-inspired idioms used to structure functional
 --     programs (functors and monads, for instance).
+
 -- • Codata
 --     Coinductive data types and properties. There are two different
 --     approaches taken. The `Codata` folder contains the new more
 --     standard approach using sized types. The `Codata.Musical`
 --     folder contains modules using the old musical notation.
+
 -- • Data
 --     Data types and properties.
+
+import README.Data
+
 -- • Function
 --     Combinators and properties related to functions.
+
 -- • Foreign
 --     Related to the foreign function interface.
+
 -- • Induction
 --     A general framework for induction (includes lexicographic and
 --     well-founded induction).
+
 -- • IO
 --     Input/output-related functions.
+
 -- • Level
 --     Universe levels.
--- • Record
---     An encoding of record types with manifest fields and "with".
+
 -- • Reflection
 --     Support for reflection.
+
 -- • Relation
 --     Properties of and proofs about relations.
+
 -- • Size
 --     Sizes used by the sized types mechanism.
+
 -- • Strict
 --     Provides access to the builtins relating to strictness.
--- • Universe
---     A definition of universes.
 
 ------------------------------------------------------------------------
 -- A selection of useful library modules
@@ -120,7 +127,7 @@ import Category.Monad        -- Monads.
 import Relation.Binary.PropositionalEquality
 
 -- Convenient syntax for "equational reasoning" using a preorder:
-import Relation.Binary.PreorderReasoning
+import Relation.Binary.Reasoning.Preorder
 
 -- Solver for commutative ring or semiring equalities:
 import Algebra.Solver.Ring
@@ -145,7 +152,7 @@ import Induction
 import Induction.WellFounded
 
 -- Various forms of induction for natural numbers:
-import Induction.Nat
+import Data.Nat.Induction
 
 -- • Support for coinduction
 
@@ -184,7 +191,7 @@ import IO
 --
 --     open IsSemigroup isSemigroup public
 --
--- Note here that open IsSemigroup isSemigroup public ensures that the
+-- Note here that `open IsSemigroup isSemigroup public` ensures that the
 -- fields of the isSemigroup record can be accessed directly; this
 -- technique enables the user of an IsMonoid record to use underlying
 -- records without having to manually open an entire record hierarchy.
@@ -210,7 +217,7 @@ import IO
 -- in IsPreorder.
 
 -- Records packing up properties with the corresponding operations,
--- sets, etc. are sometimes also defined:
+-- sets, etc. are also defined:
 --
 --   record Semigroup : Set₁ where
 --     infixl 7 _∙_
@@ -255,34 +262,33 @@ import IO
 -- More documentation
 ------------------------------------------------------------------------
 
--- Some examples showing where the natural numbers/integers and some
--- related operations and properties are defined, and how they can be
--- used:
+-- Some examples showing how the case expression can be used.
 
-import README.Nat
-import README.Integer
+import README.Case
 
--- Some examples showing how the AVL tree module can be used.
+-- Some examples showing how combinators can be used to emulate
+-- "functional reasoning"
 
-import README.AVL
+import README.Function.Reasoning
 
--- An example showing how the Record module can be used.
+-- An example showing how to use the debug tracing mechanism to inspect
+-- the behaviour of compiled Agda programs.
 
-import README.Record
+import README.Debug.Trace
 
--- An example showing how the case expression can be used.
+-- An exploration of the generic programs acting on n-ary functions and
+-- n-ary heterogeneous products
 
-import README.Case
+import README.Nary
 
--- An example showing how the free monad construction on containers can be
--- used
+-- Explaining the inspect idiom: use case, equivalent handwritten
+-- auxiliary definitions, and implementation details.
 
-import README.Container.FreeMonad
+import README.Inspect
 
--- Some examples showing how combinators can be used to emulate
--- "functional reasoning"
+-- Explaining string formats and the behaviour of printf
 
-import README.Function.Reasoning
+import README.Text
 
 ------------------------------------------------------------------------
 -- Core modules

README.md

@@ -6,74 +6,48 @@ write both programs and proofs. While we always try and write efficient
 code, we prioritise ease of proof over type-checking and normalisation
 performance. If computational performance is important to you, then
 perhaps try [agda-prelude](https://github.com/UlfNorell/agda-prelude)
-instead. You can browse the library source code in glorious clickable
-html [here](https://agda.github.io/agda-stdlib/README.html).
+instead.
 
-## Quick installation instructions
+If you're looking to find your way around the library, its structure
+is described in the [README.agda](https://github.com/agda/agda-stdlib/tree/master/README.agda)
+and the associated [README folder](https://github.com/agda/agda-stdlib/tree/master/README).
+You can browse the library source code in glorious clickable html
+[here](https://agda.github.io/agda-stdlib/README.html).
 
-Use version v0.17 of the standard library with Agda 2.5.4.1.
+## Installation instructions
 
-Install it as follows. Say you are in directory `$HERE` (replace appropriately).
-```
-  git clone https://github.com/agda/agda-stdlib.git
-  cd agda-stdlib
-  git checkout v0.17
-  cabal install
-```
-The last comment is optional, omit it if you are lacking [cabal](https://www.haskell.org/cabal/).
+See the instructions [here](https://github.com/agda/agda-stdlib/blob/master/notes/installation-guide.md)
+for how to install version 1.1 of the standard library.
 
-Register it by adding the following line to `$HOME/.agda/libraries`:
-```
-  $HERE/agda-stdlib/standard-library.agda-lib
-```
-
-To use the standard library in you project `$PROJECT`, put a file
-`$PROJECT.agda-lib` file in the project root containing:
-```
-  depend: standard-library
-  include: $DIRS
-```
-where `$DIRS` is a list of directories where Agda
-searches for modules, for instance `.` (just the project root).
-
-If you want to refer to the standard library in all your
-projects, add the following line to `$HOME/.agda/defaults`
-```
-  standard-library
-```
-
-Find the full story at [readthedocs](http://agda.readthedocs.io/en/latest/tools/package-system.html).
-
-## Contributing to the library
-
-If you would like to suggest improvements, feel free to use the `Issues` tab.
-If you would like to make improvements yourself, follow the instructions in
-[HACKING](https://github.com/agda/agda-stdlib/blob/master/HACKING.md).
-
-## Non-standard versions of Agda
+#### Old versions of Agda
 
 If you're using an old version of Agda, you can download the corresponding version
 of the standard library on the [Agda wiki](http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Libraries.StandardLibrary).
 
+#### Development version of Agda
+
 If you're using a development version of Agda rather than the latest official release
 you should use the `experimental` branch of the standard library rather than `master`.
 The `experimental` branch contains non-backwards compatible patches for upcoming
 changes to the language.
 
-## Type-checking with the `--safe` flag
+## Type-checking with flags
+
+#### The `--safe` flag
+
+Most of the library can be type-checked using the `--safe` flag. Please consult
+[GenerateEverything.hs](https://github.com/agda/agda-stdlib/blob/master/GenerateEverything.hs#L23)
+for a full list of modules that use unsafe features.
+
+#### The `--without-k` flag
 
-After the next full release of Agda, most of the library will be able to
-be type-checked with the `--safe` flag. Only the following modules are
-not compatible:
-```
-  Data.Char.Unsafe
-  Data.Float.Unsafe
-  Data.Nat.Unsafe
-  Data.Nat.DivMod.Unsafe
-  Data.String.Unsafe
-  Data.Word.Unsafe
-  IO
-  IO.Primitives
-  Reflection
-  Relation.Binary.PropositionalEquality.TrustMe
-```
+Most of the library can be type-checked using the `--without-k` flag. Please consult
+[GenerateEverything.hs](https://github.com/agda/agda-stdlib/blob/master/GenerateEverything.hs#L74)
+for a full list of modules that use axiom K.
+
+## Contributing to the library
+
+If you would like to suggest improvements, feel free to use the `Issues` tab.
+Even better if you would like to make the improvements yourself, we have instructions
+in [HACKING](https://github.com/agda/agda-stdlib/blob/master/HACKING.md) to help
+you get started.

README/Axiom.agda

+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- An explanation about the `Axiom` modules.
+------------------------------------------------------------------------
+
+module README.Axiom where
+
+open import Level using (Level)
+
+private variable ℓ : Level
+
+------------------------------------------------------------------------
+-- Introduction
+
+-- Several rules that are used without thought in written mathematics
+-- cannot be proved in Agda. The modules in the `Axiom` folder
+-- provide types expressing some of these rules that users may want to
+-- use even when they're not provable in Agda.
+
+------------------------------------------------------------------------
+-- Example: law of excluded middle
+
+-- In classical logic the law of excluded middle states that for any
+-- proposition `P` either `P` or `¬P` must hold. This is impossible
+-- to prove in Agda because Agda is a constructive system and so any
+-- proof of the excluded middle would have to build a term of either
+-- type `P` or `¬P`. This is clearly impossible without any knowledge
+-- of what proposition `P` is.
+
+-- The types for which `P` or `¬P` holds is called `Dec P` in the
+-- standard library (short for `Decidable`).
+
+open import Relation.Nullary using (Dec)
+
+-- The type of the proof of saying that excluded middle holds for
+-- all types at universe level ℓ is therefore:
+--
+--   ExcludedMiddle ℓ = ∀ {P : Set ℓ} → Dec P
+--
+-- and this type is exactly the one found in `Axiom.ExcludedMiddle`:
+
+open import Axiom.ExcludedMiddle
+
+-- There are two different ways that the axiom can be introduced into
+-- your Agda development. The first option is to postulate it:
+
+postulate excludedMiddle : ExcludedMiddle ℓ
+
+-- This has the advantage that it only needs to be postulated once
+-- and it can then be imported into many different modules as with any
+-- other proof. The downside is that the resulting Agda code will no
+-- longer type check under the --safe flag.
+
+-- The second approach is to pass it as a module parameter:
+
+module Proof (excludedMiddle : ExcludedMiddle ℓ) where
+
+-- The advantage of this approach is that the resulting Agda
+-- development can still be type checked under the --safe flag.
+-- Intuitively the reason for this is that when postulating it
+-- you are telling Agda that excluded middle does hold (which is clearly
+-- untrue as discussed above). In contrast when passing it as a module
+-- parameter you are telling Agda that **if** excluded middle was true
+-- then the following proofs would hold, which is logically valid.
+
+-- The disadvantage of this approach is that it is now necessary to
+-- include the excluded middle assumption as a parameter in every module
+-- that you want to use it in. Additionally the modules can never
+-- be fully instantiated (without postulating excluded middle).
+
+------------------------------------------------------------------------
+-- Other axioms
+
+-- Double negation elimination
+--   (∀ P → ¬ ¬ P → P)
+
+import Axiom.DoubleNegationElimination
+
+-- Function extensionality
+--   (∀ f g → (∀ x → f x ≡ g x) → f ≡ g)
+
+import Axiom.Extensionality.Propositional
+import Axiom.Extensionality.Heterogeneous
+
+-- Uniqueness of identity proofs (UIP)
+--  (∀ x y (p q : x ≡ y) → p ≡ q)
+
+import Axiom.UniquenessOfIdentityProofs