diff options
| author | Sean Whitton <spwhitton@spwhitton.name> | 2016-06-10 17:28:53 +0900 |
|---|---|---|
| committer | Sean Whitton <spwhitton@spwhitton.name> | 2016-06-10 17:28:53 +0900 |
| commit | 4b8a7e1e9640da64fd17a74ebc176909a3aea944 (patch) | |
| tree | 9b85ed495daeb8968d8cd9f7abd45a8244e341b1 | |
| parent | 22d7b46b012db080c7e94b064eef55fc25b31eac (diff) | |
Imported Upstream version 0.12
63 files changed, 468 insertions, 613 deletions
diff --git a/.dropbox_uploader.enc b/.dropbox_uploader.enc new file mode 100644 index 0000000..8dc5135 --- /dev/null +++ b/.dropbox_uploader.enc @@ -0,0 +1 @@ +$ %7 "6_TXNݤPp~ *'O^6<W)aQ Ak_ 9c -)hfF ה9C>_[AYo@o%67 4ugT%";Bv`R fo
\ No newline at end of file @@ -1,11 +1,14 @@ # Keep this file in alphabetic order please! +*~ .*.swp *.agdai *.agda.el *.lagda.el *.hi *.o +*.tix +*.vim dist Everything.agda html diff --git a/.travis.yml b/.travis.yml index 9cb6122..98571a2 100644 --- a/.travis.yml +++ b/.travis.yml @@ -1,3 +1,52 @@ +language: haskell branches: only: - - master + - master + +before_install: + # Decrypting the dropbox credentials + - openssl aes-256-cbc -K $encrypted_3f6e0f4132ed_key -iv $encrypted_3f6e0f4132ed_iv -in .dropbox_uploader.enc -out .dropbox_uploader -d + - cp .dropbox_uploader $HOME/ + +install: + # Installing the dropbox download script + - cd $HOME + - curl "https://raw.githubusercontent.com/andreafabrizi/Dropbox-Uploader/master/dropbox_uploader.sh" -o dropbox_uploader.sh + - chmod +x dropbox_uploader.sh + # downloading the last (latest?) tarball and installing agda + - AGDATAR=$(./dropbox_uploader.sh list | tail -n 1 | sed 's/^.*\(Agda.*\)$/\1/') + - ./dropbox_uploader.sh download $AGDATAR . + - tar -xzvf $AGDATAR + - cd $( basename $AGDATAR .tar.gz ) + - sudo ./deploy.sh + # generating Everything.agda + - cabal install filemanip + - cd $HOME/build/agda/agda-stdlib + - runghc GenerateEverything.hs + +script: + # generating index.agda + - ./index.sh + # building the docs + - agda -i . -i src/ --html src/index.agda + # moving everything at the root + - mv html/* . + +after_success: + # uploading to gh-pages + - git init + - git config --global user.name "Travis CI bot" + - 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 add -f \*.html + - git commit -m "Automatic HTML update via Travis" + - git push -q upstream HEAD:gh-pages &>/dev/null + +notifications: + email: false + +# Github token +env: + global: + secure: f0GRSKTlAw6FdrvkI8LjP5ZhwcGBltJ1t5+nxipqfoR3VczMxcNgXD7bdwtUojFYR48jMs2W+LxEoJcuSH4bsdCeoSfpZ0nU424MDajGh0wuhAbSYKQXPWjFOxwMgC23sCySKhDAZiqN/Wd6orwV1p5JhuJkSCHdVeyUp+hLvIw= @@ -1,21 +1,18 @@ ------------------------------------------------------------------------ --- Release notes for Agda standard library version 0.11 +-- Release notes for Agda standard library version 0.12 ------------------------------------------------------------------------ -The library has been tested using Agda version 2.4.2.4. +The library has been tested using Agda version 2.5.1. -Note that no guarantees are made about backwards or forwards -compatibility, the library is still at an experimental stage. +Important changes since 0.11: -If you want to compile the library using the MAlonzo compiler, then -you should first install some supporting Haskell code, for instance as -follows: +* Added support for GHC 8.0.1. - cd ffi - cabal install +------------------------------------------------------------------------ +-- Release notes for Agda standard library version 0.11 +------------------------------------------------------------------------ -Currently the library does not support the Epic or JavaScript compiler -backends. +The library has been tested using Agda version 2.4.2.4. Important changes since 0.10: @@ -38,19 +35,6 @@ Important changes since 0.10: The library has been tested using Agda version 2.4.2.3. -Note that no guarantees are made about backwards or forwards -compatibility, the library is still at an experimental stage. - -If you want to compile the library using the MAlonzo compiler, then -you should first install some supporting Haskell code, for instance as -follows: - - cd ffi - cabal install - -Currently the library does not support the Epic or JavaScript compiler -backends. - Important changes since 0.9: * Renamed Data.Unit.Core to Data.Unit.NonEta @@ -180,25 +164,15 @@ Important changes since 0.9: * The fixity of Relation.Unary._~ was changed from the default to infix 10. +* Turned on η-equality for Record.Record, removed Record.Signature′ + and Record.Record′. + ------------------------------------------------------------------------ -- Release notes for Agda standard library version 0.9 ------------------------------------------------------------------------ The library has been tested using Agda version 2.4.2.1. -Note that no guarantees are made about backwards or forwards -compatibility, the library is still at an experimental stage. - -If you want to compile the library using the MAlonzo compiler, then -you should first install some supporting Haskell code, for instance as -follows: - - cd ffi - cabal install - -Currently the library does not support the Epic or JavaScript compiler -backends. - Important changes since 0.8.1: * Data.List.NonEmpty @@ -228,19 +202,6 @@ Important changes since 0.8.1: The library has been tested using Agda version 2.4.2. -Note that no guarantees are made about backwards or forwards -compatibility, the library is still at an experimental stage. - -If you want to compile the library using the MAlonzo compiler, then -you should first install some supporting Haskell code, for instance as -follows: - - cd ffi - cabal install - -Currently the library does not support the Epic or JavaScript compiler -backends. - Important changes since 0.8: * Reflection API @@ -266,19 +227,6 @@ http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Libraries.StandardLibrary. The library has been tested using Agda version 2.4.0. -Note that no guarantees are made about backwards or forwards -compatibility, the library is still at an experimental stage. - -If you want to compile the library using the MAlonzo compiler, then -you should first install some supporting Haskell code, for instance as -follows: - - cd ffi - cabal install - -Currently the library does not support the Epic or JavaScript compiler -backends. - ------------------------------------------------------------------------ Version 0.7 ------------------------------------------------------------------------ @@ -288,20 +236,7 @@ http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Libraries.StandardLibrary. The library has been tested using Agda version 2.3.2. -Note that no guarantees are made about backwards or forwards -compatibility, the library is still at an experimental stage. - -If you want to compile the library using the MAlonzo compiler, then -you should first install some supporting Haskell code, for instance as -follows: - - cd ffi - cabal install - -Currently the library does not support the Epic or JavaScript compiler -backends. - -------------------------------------------------------------------- +------------------------------------------------------------------------ Version 0.6 ------------------------------------------------------------------------ @@ -310,19 +245,6 @@ http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Libraries.StandardLibrary. The library has been tested using Agda version 2.3.0. -Note that no guarantees are made about backwards or forwards -compatibility, the library is still at an experimental stage. - -If you want to compile the library using the MAlonzo compiler, then -you should first install some supporting Haskell code, for instance as -follows: - - cd ffi - cabal install - -Currently the library does not support the Epic or JavaScript compiler -backends. - ------------------------------------------------------------------------ Version 0.5 ------------------------------------------------------------------------ @@ -332,9 +254,6 @@ http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Libraries.StandardLibrary. The library has been tested using Agda version 2.2.10. -Note that no guarantees are made about backwards or forwards -compatibility, the library is still at an experimental stage. - ------------------------------------------------------------------------ Version 0.4 ------------------------------------------------------------------------ @@ -344,9 +263,6 @@ http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Libraries.StandardLibrary. The library has been tested using Agda version 2.2.8. -Note that no guarantees are made about backwards or forwards -compatibility, the library is still at an experimental stage. - ------------------------------------------------------------------------ Version 0.3 ------------------------------------------------------------------------ @@ -356,9 +272,6 @@ http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Libraries.StandardLibrary. The library has been tested using Agda version 2.2.6. -Note that no guarantees are made about backwards or forwards -compatibility, the library is still at an experimental stage. - ------------------------------------------------------------------------ Version 0.2 ------------------------------------------------------------------------ @@ -368,11 +281,8 @@ http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Libraries.StandardLibrary. The library has been tested using Agda version 2.2.4. -Note that no guarantees are made about backwards or forwards -compatibility, the library is still at an experimental stage. - -Note also that the library sources are now located in the -sub-directory lib-<version>/src of the installation tarball. +Note that the library sources are now located in the sub-directory +lib-<version>/src of the installation tarball. ------------------------------------------------------------------------ Version 0.1 @@ -382,6 +292,3 @@ Version 0.1 of the "standard" library has now been released, see http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Libraries.StandardLibrary. The library has been tested using Agda version 2.2.2. - -Note that no guarantees are made about backwards or forwards -compatibility, the library is still at an experimental stage. diff --git a/GNUmakefile b/GNUmakefile index 542aea1..2916a1b 100644 --- a/GNUmakefile +++ b/GNUmakefile @@ -4,17 +4,13 @@ test: Everything.agda fix-agda-whitespace --check $(AGDA) -i. -isrc README.agda -setup: Everything.agda agda-lib-ffi +setup: Everything.agda .PHONY: Everything.agda Everything.agda: cabal clean && cabal install GenerateEverything -.PHONY: agda-lib-ffi -agda-lib-ffi: - cd ffi && cabal clean && cabal install - .PHONY: listings listings: Everything.agda $(AGDA) -i. -isrc --html README.agda -v0 diff --git a/GenerateEverything.hs b/GenerateEverything.hs index dbd42ef..25c14d6 100644 --- a/GenerateEverything.hs +++ b/GenerateEverything.hs @@ -48,8 +48,9 @@ usage = unlines isLibraryModule :: FilePath -> Bool isLibraryModule f = - takeExtension f `elem` [".agda", ".lagda"] && - dropExtension (takeFileName f) /= "Core" + takeExtension f `elem` [".agda", ".lagda"] + && dropExtension (takeFileName f) /= "Core" + && dropExtension (takeFileName f) /= "index" -- | Reads a module and extracts the header. @@ -0,0 +1,31 @@ + +* Where to commit changes: + + CURRENT_AGDA = current released Agda version, e.g. 2.4.2.5 + AGDA_MAINT = Agda maintenance version, e.g. 2.4.2.6 + + A. Your change is independent of Agda + + 1. Push your commit in the CURRENT_AGDA branch + 2. Merge the CURRENT_AGDA branch into the AGDA_MAINT branch + 3. Merge the AGDA_MAINT branch into the master branch + + B. Your change is due to a change in the AGDA_MAINT version of Agda + + 1. Push your commit in the AGDA_MAINT branch + 2. Merge the AGDA_MAINT branch into the master branch + + C. Your change is due to a change in the master version of Agda + + 1. Push your commit in the master branch + + This scheme should guarantee that: + + a. the stdlib CURRENT_AGDA branch always builds with the current + released Agda version, + + b. the stdlib AGDA_MAINT branch always build with the Agda maint + branch and + + c. the stdlib master branch always builds with the Agda master + branch. @@ -1,4 +1,4 @@ -Copyright (c) 2007-2015 Nils Anders Danielsson, Ulf Norell, Shin-Cheng +Copyright (c) 2007-2016 Nils Anders Danielsson, Ulf Norell, Shin-Cheng Mu, 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 diff --git a/README.agda b/README.agda index 8e4d0ed..aa9669f 100644 --- a/README.agda +++ b/README.agda @@ -1,7 +1,7 @@ module README where ------------------------------------------------------------------------ --- The Agda standard library, version 0.11 +-- The Agda standard library, version 0.12 -- -- Author: Nils Anders Danielsson, with contributions from Andreas -- Abel, Stevan Andjelkovic, Jean-Philippe Bernardy, Peter Berry, @@ -14,25 +14,17 @@ module README where -- anonymous contributors. -- ---------------------------------------------------------------------- --- This version of the library has been tested using Agda 2.4.2.4. +-- This version of the library has been tested using Agda 2.5.1. -- Note that no guarantees are currently made about forwards or -- backwards compatibility, the library is still at an experimental -- stage. --- To make use of the library, add the path to the library’s root --- directory (src) to the Agda search path, either using the --- --include-path flag or by customising the Emacs mode variable --- agda2-include-dirs (M-x customize-group RET agda2 RET). +-- The library comes with a .agda-lib file, for use with the library +-- management system. --- To compile the library using the MAlonzo compiler you first need to --- install some supporting Haskell code, for instance as follows: --- --- cd ffi --- cabal install --- --- Currently the library does not support the Epic or JavaScript --- compiler backends. +-- 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 @@ -274,6 +266,11 @@ import README.Record import README.Case +-- An example showing how the free monad construction on containers can be +-- used + +import README.Container.FreeMonad + ------------------------------------------------------------------------ -- Core modules ------------------------------------------------------------------------ diff --git a/README/Container/FreeMonad.agda b/README/Container/FreeMonad.agda index 4263658..c7b3eec 100644 --- a/README/Container/FreeMonad.agda +++ b/README/Container/FreeMonad.agda @@ -55,7 +55,7 @@ runState (sup (inj₁ x) _) = λ s → x , s runState (sup (inj₂ (inj₁ _)) k) = λ s → runState (k s) s runState (sup (inj₂ (inj₂ s)) k) = λ _ → runState (k _) s -test : runState prog 0 ≡ true , 1 +test : runState prog 0 ≡ (true , 1) test = refl -- It should be noted that @State S ⋆ X@ is not the state monad. If we diff --git a/doc/release-notes/future.txt b/doc/release-notes/future.txt new file mode 100644 index 0000000..fb3cf36 --- /dev/null +++ b/doc/release-notes/future.txt @@ -0,0 +1,30 @@ +NOTE: Put drafts of release notes here that might be included in some +future release. Don't remove this message please! +------------------------------------------------------------------------------ + +* Support for the UHC backend has been added. + +* The tri⟶irr function has been made more general. + +* The field <-resp-≈ has been removed from the IsStrictTotalOrder + record. The property can be derived (see the new lemma + Relation.Binary.Consequences.trans∧tri⟶resp≈), and is available from + the IsStrictTotalOrder record module. + +* Various changes required by changes in Agda (see Agda CHANGELOG): + + ** Hiding some modules in import directives after fixing #836. + + ** Removed COMPILED_DATA for Bool.Base.agda. + + ** Removed the IRRAXIOM built-in from Irrelevance.agda + + ** Added BUILTIN bindings in Data/Integer.agda + + ** IO FFI calls work with the now Data.Text-backed String builtins. + + ** Added parentheses for fixing operators and sections parsing. + + ** Added BUILTIN binding in Data/Unit.agda. + + ** Various changes in Reflection.agda diff --git a/ffi/Data/FFI.hs b/ffi/Data/FFI.hs deleted file mode 100644 index 6c8bf54..0000000 --- a/ffi/Data/FFI.hs +++ /dev/null @@ -1,11 +0,0 @@ -{-# LANGUAGE EmptyDataDecls #-} - -module Data.FFI where - -type AgdaList a b = [b] -type AgdaMaybe a b = Maybe b -type AgdaEither a b c d = Either c d - -data AgdaEmpty - -data AgdaStream a = Cons a (AgdaStream a) diff --git a/ffi/IO/FFI.hs b/ffi/IO/FFI.hs deleted file mode 100644 index 7db128a..0000000 --- a/ffi/IO/FFI.hs +++ /dev/null @@ -1,18 +0,0 @@ -module IO.FFI where - -import Control.Exception (bracketOnError) -import System.IO - (openFile, IOMode(ReadMode), hClose, hFileSize, hGetContents) - --- | A variant of IO with an extra dummy type parameter. - -type AgdaIO a b = IO b - --- | Reads a finite file. Raises an exception if the file path refers --- to a non-physical file (like @/dev/zero@). - -readFiniteFile :: FilePath -> IO String -readFiniteFile f = do - h <- openFile f ReadMode - bracketOnError (return ()) (\_ -> hClose h) (\_ -> hFileSize h) - hGetContents h diff --git a/ffi/Setup.hs b/ffi/Setup.hs deleted file mode 100644 index e8ef27d..0000000 --- a/ffi/Setup.hs +++ /dev/null @@ -1,3 +0,0 @@ -import Distribution.Simple - -main = defaultMain diff --git a/ffi/agda-lib-ffi.cabal b/ffi/agda-lib-ffi.cabal deleted file mode 100644 index 5cd6e8e..0000000 --- a/ffi/agda-lib-ffi.cabal +++ /dev/null @@ -1,11 +0,0 @@ -name: agda-lib-ffi -version: 0.11 -cabal-version: >= 1.8 -build-type: Simple -description: Auxiliary Haskell code used by Agda's standard library. -tested-with: GHC == 7.8.4 - -library - build-depends: base >= 4.6.0.1 && < 4.9 - exposed-modules: Data.FFI - IO.FFI diff --git a/index.sh b/index.sh new file mode 100755 index 0000000..05ccc0b --- /dev/null +++ b/index.sh @@ -0,0 +1,3 @@ +for i in $( find src -name "*.agda" | grep -v "index.agda" | sed 's/src\/\(.*\)\.agda/\1/' | sed 's/\//\./g' | sort ); do + echo "import $i" >> src/index.agda; +done @@ -1,20 +1,20 @@ name: lib -version: 0.11 +version: 0.12 cabal-version: >= 1.8 build-type: Simple description: Helper programs. license: MIT -tested-with: GHC == 7.8.4 +tested-with: GHC == 7.10.3 executable GenerateEverything hs-source-dirs: . main-is: GenerateEverything.hs - build-depends: base >= 4.6.0.1 && < 4.9 + build-depends: base >= 4.6.0.1 && < 4.10 , filemanip >= 0.3.6.2 && < 0.4 , filepath >= 1.3.0.1 && < 1.5 executable AllNonAsciiChars hs-source-dirs: . main-is: AllNonAsciiChars.hs - build-depends: base >= 4.6.0.1 && < 4.9 + build-depends: base >= 4.6.0.1 && < 4.10 , filemanip >= 0.3.6.2 && < 0.4 diff --git a/notes/stdlib-releases.txt b/notes/stdlib-releases.txt index b885d27..086f99f 100644 --- a/notes/stdlib-releases.txt +++ b/notes/stdlib-releases.txt @@ -16,18 +16,10 @@ procedure can be followed: * Update the lib.cabal version to X.Y. -* Update the ffi/agda-lib-ffi.cabal version to X.Y. - * Ensure that the library type-checks using Agda A.B.C: make test -* Ensure that the auxiliary Haskell code used by the library builds - properly (with the versions of GHC supported by Agda A.B.C if - possible): - - make agda-lib-ffi - * If necessary, copy the contents of notes/future-version.txt to CHANGELOG. Remove the contents from notes/future-version.txt diff --git a/src/Coinduction.agda b/src/Coinduction.agda index 9587fbb..25f0de7 100644 --- a/src/Coinduction.agda +++ b/src/Coinduction.agda @@ -6,21 +6,7 @@ module Coinduction where -import Level - ------------------------------------------------------------------------- --- A type used to make recursive arguments coinductive - -infix 1000 ♯_ - -postulate - ∞ : ∀ {a} (A : Set a) → Set a - ♯_ : ∀ {a} {A : Set a} → A → ∞ A - ♭ : ∀ {a} {A : Set a} → ∞ A → A - -{-# BUILTIN INFINITY ∞ #-} -{-# BUILTIN SHARP ♯_ #-} -{-# BUILTIN FLAT ♭ #-} +open import Agda.Builtin.Coinduction public ------------------------------------------------------------------------ -- Rec, a type which is analogous to the Rec type constructor used in diff --git a/src/Data/Bin.agda b/src/Data/Bin.agda index abc1776..3a05a0e 100644 --- a/src/Data/Bin.agda +++ b/src/Data/Bin.agda @@ -186,7 +186,6 @@ strictTotalOrder = record { isEquivalence = PropEq.isEquivalence ; trans = <-trans ; compare = compare - ; <-resp-≈ = PropEq.resp₂ _<_ } } diff --git a/src/Data/Bool/Base.agda b/src/Data/Bool/Base.agda index 5a8b601..2208199 100644 --- a/src/Data/Bool/Base.agda +++ b/src/Data/Bool/Base.agda @@ -17,19 +17,7 @@ infix 0 if_then_else_ ------------------------------------------------------------------------ -- The boolean type -data Bool : Set where - true : Bool - false : Bool - -{-# BUILTIN BOOL Bool #-} -{-# BUILTIN TRUE true #-} -{-# BUILTIN FALSE false #-} - -{-# COMPILED_DATA Bool Bool True False #-} - -{-# COMPILED_JS Bool function (x,v) { return ((x)? v["true"]() : v["false"]()); } #-} -{-# COMPILED_JS true true #-} -{-# COMPILED_JS false false #-} +open import Agda.Builtin.Bool public ------------------------------------------------------------------------ -- Some operations diff --git a/src/Data/Char/Base.agda b/src/Data/Char/Base.agda index 361d6d3..ba1aa55 100644 --- a/src/Data/Char/Base.agda +++ b/src/Data/Char/Base.agda @@ -17,10 +17,8 @@ open import Data.Char.Core using (Char) public ------------------------------------------------------------------------ -- Primitive operations -primitive - primCharToNat : Char → ℕ - primCharEquality : Char → Char → Bool - primShowChar : Char → String +open import Agda.Builtin.Char public using (primCharToNat; primCharEquality) +open import Agda.Builtin.String public using (primShowChar) show : Char → String show = primShowChar diff --git a/src/Data/Char/Core.agda b/src/Data/Char/Core.agda index 0a0d1e6..a31c435 100644 --- a/src/Data/Char/Core.agda +++ b/src/Data/Char/Core.agda @@ -9,8 +9,4 @@ module Data.Char.Core where ------------------------------------------------------------------------ -- The type -postulate - Char : Set - -{-# BUILTIN CHAR Char #-} -{-# COMPILED_TYPE Char Char #-} +open import Agda.Builtin.Char public using (Char) diff --git a/src/Data/Colist.agda b/src/Data/Colist.agda index 8da5feb..a458171 100644 --- a/src/Data/Colist.agda +++ b/src/Data/Colist.agda @@ -43,8 +43,9 @@ data Colist {a} (A : Set a) : Set a where [] : Colist A _∷_ : (x : A) (xs : ∞ (Colist A)) → Colist A -{-# IMPORT Data.FFI #-} -{-# COMPILED_DATA Colist Data.FFI.AgdaList [] (:) #-} +{-# HASKELL type AgdaColist a b = [b] #-} +{-# COMPILED_DATA Colist MAlonzo.Code.Data.Colist.AgdaColist [] (:) #-} +{-# COMPILED_DATA_UHC Colist __LIST__ __NIL__ __CONS__ #-} data Any {a p} {A : Set a} (P : A → Set p) : Colist A → Set (a ⊔ p) where diff --git a/src/Data/Empty.agda b/src/Data/Empty.agda index b32d11b..5c1fd5d 100644 --- a/src/Data/Empty.agda +++ b/src/Data/Empty.agda @@ -10,8 +10,8 @@ open import Level data ⊥ : Set where -{-# IMPORT Data.FFI #-} -{-# COMPILED_DATA ⊥ Data.FFI.AgdaEmpty #-} +{-# HASKELL data AgdaEmpty #-} +{-# COMPILED_DATA ⊥ MAlonzo.Code.Data.Empty.AgdaEmpty #-} ⊥-elim : ∀ {w} {Whatever : Set w} → ⊥ → Whatever ⊥-elim () diff --git a/src/Data/Fin/Properties.agda b/src/Data/Fin/Properties.agda index 38cb28d..756a113 100644 --- a/src/Data/Fin/Properties.agda +++ b/src/Data/Fin/Properties.agda @@ -50,7 +50,6 @@ strictTotalOrder n = record { isEquivalence = P.isEquivalence ; trans = N.<-trans ; compare = cmp - ; <-resp-≈ = P.resp₂ _<_ } } where diff --git a/src/Data/Float.agda b/src/Data/Float.agda index d0eeb33..77af9ce 100644 --- a/src/Data/Float.agda +++ b/src/Data/Float.agda @@ -13,14 +13,8 @@ open import Relation.Binary.PropositionalEquality as PropEq using (_≡_) open import Relation.Binary.PropositionalEquality.TrustMe open import Data.String.Base using (String) -postulate - Float : Set - -{-# BUILTIN FLOAT Float #-} - -primitive - primFloatEquality : Float → Float → Bool - primShowFloat : Float → String +open import Agda.Builtin.Float public + using ( Float; primFloatEquality; primShowFloat ) show : Float → String show = primShowFloat diff --git a/src/Data/Integer.agda b/src/Data/Integer.agda index 3502ca0..db30cc8 100644 --- a/src/Data/Integer.agda +++ b/src/Data/Integer.agda @@ -112,7 +112,7 @@ decTotalOrder = record antisym : Antisymmetric _≡_ _≤_ antisym -≤+ () antisym (-≤- n≤m) (-≤- m≤n) = cong -[1+_] $ ℕO.antisym m≤n n≤m - antisym (+≤+ m≤n) (+≤+ n≤m) = cong +_ $ ℕO.antisym m≤n n≤m + antisym (+≤+ m≤n) (+≤+ n≤m) = cong (+_) $ ℕO.antisym m≤n n≤m total : Total _≤_ total (-[1+ m ]) (-[1+ n ]) = [ inj₂ ∘′ -≤- , inj₁ ∘′ -≤- ]′ $ ℕO.total m n diff --git a/src/Data/Integer/Base.agda b/src/Data/Integer/Base.agda index fb417ba..8894f16 100644 --- a/src/Data/Integer/Base.agda +++ b/src/Data/Integer/Base.agda @@ -15,7 +15,7 @@ open import Relation.Binary open import Relation.Binary.Core using (_≡_; refl) -- Importing Core here ^^^ to keep a small import list -infix 8 +_ -_ +infix 8 -_ infixl 7 _*_ _⊓_ infixl 6 _+_ _-_ _⊖_ _⊔_ infix 4 _≤_ @@ -25,9 +25,11 @@ infix 4 _≤_ -- Integers. -data ℤ : Set where - -[1+_] : (n : ℕ) → ℤ -- -[1+ n ] stands for - (1 + n). - +_ : (n : ℕ) → ℤ -- + n stands for n. +open import Agda.Builtin.Int public + using () + renaming ( Int to ℤ + ; negsuc to -[1+_] -- -[1+ n ] stands for - (1 + n). + ; pos to +_ ) -- + n stands for n. ------------------------------------------------------------------------ -- Conversions diff --git a/src/Data/Integer/Properties.agda b/src/Data/Integer/Properties.agda index 9f1d821..485907c 100644 --- a/src/Data/Integer/Properties.agda +++ b/src/Data/Integer/Properties.agda @@ -16,6 +16,7 @@ import Data.Integer.Addition.Properties as Add import Data.Integer.Multiplication.Properties as Mul open import Data.Nat using (ℕ; suc; zero; _∸_; _≤?_; _<_; _≥_; _≱_; s≤s; z≤n; ≤-pred) + hiding (module ℕ) renaming (_+_ to _ℕ+_; _*_ to _ℕ*_) open import Data.Nat.Properties as ℕ using (_*-mono_) open import Data.Product using (proj₁; proj₂; _,_) @@ -216,13 +217,13 @@ private | proj₂ +-identity (sign y S* sign x ◃ ∣ y ∣ ℕ* ∣ x ∣) = refl - distribʳ -[1+ a ] -[1+ b ] -[1+ c ] = cong +_ $ + distribʳ -[1+ a ] -[1+ b ] -[1+ c ] = cong (+_) $ solve 3 (λ a b c → (con 2 :+ b :+ c) :* (con 1 :+ a) := (con 1 :+ b) :* (con 1 :+ a) :+ (con 1 :+ c) :* (con 1 :+ a)) refl a b c - distribʳ (+ suc a) (+ suc b) (+ suc c) = cong +_ $ + distribʳ (+ suc a) (+ suc b) (+ suc c) = cong (+_) $ solve 3 (λ a b c → (con 1 :+ b :+ (con 1 :+ c)) :* (con 1 :+ a) := (con 1 :+ b) :* (con 1 :+ a) :+ (con 1 :+ c) :* (con 1 :+ a)) @@ -360,9 +361,9 @@ cancel-*-right i j .(s ◃ suc n) ≢0 eq | s ◂ suc n cancel-*-+-right-≤ : ∀ m n o → m * + suc o ≤ n * + suc o → m ≤ n cancel-*-+-right-≤ (-[1+ m ]) (-[1+ n ]) o (-≤- n≤m) = -≤- (≤-pred (ℕ.cancel-*-right-≤ (suc n) (suc m) o (s≤s n≤m))) -cancel-*-+-right-≤ ℤ.-[1+ _ ] (+ _) _ _ = -≤+ -cancel-*-+-right-≤ (+ 0) ℤ.-[1+ _ ] _ () -cancel-*-+-right-≤ (+ suc _) ℤ.-[1+ _ ] _ () +cancel-*-+-right-≤ -[1+ _ ] (+ _) _ _ = -≤+ +cancel-*-+-right-≤ (+ 0) -[1+ _ ] _ () +cancel-*-+-right-≤ (+ suc _) -[1+ _ ] _ () cancel-*-+-right-≤ (+ 0) (+ 0) _ _ = +≤+ z≤n cancel-*-+-right-≤ (+ 0) (+ suc _) _ _ = +≤+ z≤n cancel-*-+-right-≤ (+ suc _) (+ 0) _ (+≤+ ()) diff --git a/src/Data/List/Base.agda b/src/Data/List/Base.agda index 69ea3b5..dd082c5 100644 --- a/src/Data/List/Base.agda +++ b/src/Data/List/Base.agda @@ -13,21 +13,11 @@ open import Data.Maybe.Base using (Maybe; nothing; just) open import Data.Product as Prod using (_×_; _,_) open import Function -infixr 5 _∷_ - ------------------------------------------------------------------------ -- Types -data List {a} (A : Set a) : Set a where - [] : List A - _∷_ : (x : A) (xs : List A) → List A - -{-# BUILTIN LIST List #-} -{-# BUILTIN NIL [] #-} -{-# BUILTIN CONS _∷_ #-} - -{-# IMPORT Data.FFI #-} -{-# COMPILED_DATA List Data.FFI.AgdaList [] (:) #-} +open import Agda.Builtin.List public + using (List; []; _∷_) ------------------------------------------------------------------------ -- Some operations diff --git a/src/Data/Maybe/Base.agda b/src/Data/Maybe/Base.agda index 06e72c6..7f8e78a 100644 --- a/src/Data/Maybe/Base.agda +++ b/src/Data/Maybe/Base.agda @@ -14,8 +14,8 @@ data Maybe {a} (A : Set a) : Set a where just : (x : A) → Maybe A nothing : Maybe A -{-# IMPORT Data.FFI #-} -{-# COMPILED_DATA Maybe Data.FFI.AgdaMaybe Just Nothing #-} +{-# HASKELL type AgdaMaybe a b = Maybe b #-} +{-# COMPILED_DATA Maybe MAlonzo.Code.Data.Maybe.Base.AgdaMaybe Just Nothing #-} ------------------------------------------------------------------------ -- Some operations diff --git a/src/Data/Nat/Base.agda b/src/Data/Nat/Base.agda index 1e485c9..7199a5c 100644 --- a/src/Data/Nat/Base.agda +++ b/src/Data/Nat/Base.agda @@ -19,38 +19,15 @@ infix 4 _≤_ _<_ _≥_ _>_ _≰_ _≮_ _≱_ _≯_ ------------------------------------------------------------------------ -- The types -data ℕ : Set where - zero : ℕ - suc : (n : ℕ) → ℕ +open import Agda.Builtin.Nat public + using ( zero; suc; _+_; _*_ ) + renaming ( Nat to ℕ + ; _-_ to _∸_ ) data _≤_ : Rel ℕ Level.zero where z≤n : ∀ {n} → zero ≤ n s≤s : ∀ {m n} (m≤n : m ≤ n) → suc m ≤ suc n -{-# BUILTIN NATURAL ℕ #-} - -infixl 6 _+_ _∸_ -infixl 7 _*_ - -_+_ : ℕ → ℕ → ℕ -zero + n = n -suc m + n = suc (m + n) - -{-# BUILTIN NATPLUS _+_ #-} - -_∸_ : ℕ → ℕ → ℕ -m ∸ zero = m -zero ∸ suc n = zero -suc m ∸ suc n = m ∸ n - -{-# BUILTIN NATMINUS _∸_ #-} - -_*_ : ℕ → ℕ → ℕ -zero * n = zero -suc m * n = n + m * n - -{-# BUILTIN NATTIMES _*_ #-} - _<_ : Rel ℕ Level.zero m < n = suc m ≤ n diff --git a/src/Data/Nat/DivMod.agda b/src/Data/Nat/DivMod.agda index 0fcd457..b76f60f 100644 --- a/src/Data/Nat/DivMod.agda +++ b/src/Data/Nat/DivMod.agda @@ -16,6 +16,8 @@ open import Relation.Binary.PropositionalEquality as P using (_≡_) import Relation.Binary.PropositionalEquality.TrustMe as TrustMe using (erase) +open import Agda.Builtin.Nat using ( div-helper; mod-helper ) + open NatP.SemiringSolver open P.≡-Reasoning open Nat.≤-Reasoning @@ -34,15 +36,6 @@ record DivMod (dividend divisor : ℕ) : Set where -- Integer division. -private - - div-helper : ℕ → ℕ → ℕ → ℕ → ℕ - div-helper acc s zero n = acc - div-helper acc s (suc d) zero = div-helper (suc acc) s d s - div-helper acc s (suc d) (suc n) = div-helper acc s d n - - {-# BUILTIN NATDIVSUCAUX div-helper #-} - _div_ : (dividend divisor : ℕ) {≢0 : False (divisor ≟ 0)} → ℕ (d div 0) {} (d div suc s) = div-helper 0 s d s @@ -50,14 +43,6 @@ _div_ : (dividend divisor : ℕ) {≢0 : False (divisor ≟ 0)} → ℕ -- The remainder after integer division. private - - mod-helper : ℕ → ℕ → ℕ → ℕ → ℕ - mod-helper acc s zero n = acc - mod-helper acc s (suc d) zero = mod-helper zero s d s - mod-helper acc s (suc d) (suc n) = mod-helper (suc acc) s d n - - {-# BUILTIN NATMODSUCAUX mod-helper #-} - -- The remainder is not too large. mod-lemma : (acc d n : ℕ) → diff --git a/src/Data/Nat/GCD.agda b/src/Data/Nat/GCD.agda index de7382c..d78b0e5 100644 --- a/src/Data/Nat/GCD.agda +++ b/src/Data/Nat/GCD.agda @@ -69,7 +69,7 @@ module GCD where greatest′ : ∀ {d′} → d′ ∣ n × d′ ∣ n + k → d′ ∣ d greatest′ (d₁ , d₂) = GCD.greatest g (d₁ , ∣-∸ d₂ d₁) -open GCD public using (GCD) +open GCD public using (GCD) hiding (module GCD) ------------------------------------------------------------------------ -- Calculating the gcd @@ -119,7 +119,7 @@ module Bézout where step {d} (-+ .x .(x ⊕ i) eq) | less x i = -+ (2 * x ⊕ i) (x ⊕ i) (lem₆ d x eq) step {d} {n} (-+ .(y ⊕ i) .y eq) | greater y i = -+ (2 * y ⊕ i) y (lem₇ d y n eq) - open Identity public using (Identity; +-; -+) + open Identity public using (Identity; +-; -+) hiding (module Identity) module Lemma where @@ -148,7 +148,7 @@ module Bézout where stepʳ : ∀ {n k} → Lemma (suc k) n → Lemma (suc (n + k)) n stepʳ = sym ∘ stepˡ ∘ sym - open Lemma public using (Lemma; result) + open Lemma public using (Lemma; result) hiding (module Lemma) -- Bézout's lemma proved using some variant of the extended -- Euclidean algorithm. diff --git a/src/Data/Nat/LCM.agda b/src/Data/Nat/LCM.agda index bb4917a..7292123 100644 --- a/src/Data/Nat/LCM.agda +++ b/src/Data/Nat/LCM.agda @@ -47,7 +47,7 @@ module LCM where unique d₁ d₂ = P.antisym (LCM.least d₁ (LCM.commonMultiple d₂)) (LCM.least d₂ (LCM.commonMultiple d₁)) -open LCM public using (LCM) +open LCM public using (LCM) hiding (module LCM) ------------------------------------------------------------------------ -- Calculating the lcm diff --git a/src/Data/Nat/Properties.agda b/src/Data/Nat/Properties.agda index 6bbb73c..b74a3a5 100644 --- a/src/Data/Nat/Properties.agda +++ b/src/Data/Nat/Properties.agda @@ -375,7 +375,6 @@ strictTotalOrder = record { isEquivalence = PropEq.isEquivalence ; trans = <-trans ; compare = cmp - ; <-resp-≈ = PropEq.resp₂ _<_ } } where diff --git a/src/Data/Stream.agda b/src/Data/Stream.agda index 20fe7da..dcad1f8 100644 --- a/src/Data/Stream.agda +++ b/src/Data/Stream.agda @@ -21,8 +21,8 @@ infixr 5 _∷_ data Stream (A : Set) : Set where _∷_ : (x : A) (xs : ∞ (Stream A)) → Stream A -{-# IMPORT Data.FFI #-} -{-# COMPILED_DATA Stream Data.FFI.AgdaStream Data.FFI.Cons #-} +{-# HASKELL data AgdaStream a = Cons a (AgdaStream a) #-} +{-# COMPILED_DATA Stream MAlonzo.Code.Data.Stream.AgdaStream MAlonzo.Code.Data.Stream.Cons #-} ------------------------------------------------------------------------ -- Some operations diff --git a/src/Data/String/Base.agda b/src/Data/String/Base.agda index bc15358..90b9a43 100644 --- a/src/Data/String/Base.agda +++ b/src/Data/String/Base.agda @@ -13,23 +13,15 @@ open import Relation.Binary.Core using (_≡_) open import Relation.Binary.PropositionalEquality.TrustMe using (trustMe) ------------------------------------------------------------------------ --- The type - -postulate - String : Set - -{-# BUILTIN STRING String #-} -{-# COMPILED_TYPE String String #-} - ------------------------------------------------------------------------- --- Primitive operations - -primitive - primStringAppend : String → String → String - primStringToList : String → List Char - primStringFromList : List Char → String - primStringEquality : String → String → Bool - primShowString : String → String +-- From Agda.Builtin + +open import Agda.Builtin.String public + using ( String + ; primStringAppend + ; primStringToList + ; primStringFromList + ; primStringEquality + ; primShowString ) ------------------------------------------------------------------------ -- Operations diff --git a/src/Data/Sum.agda b/src/Data/Sum.agda index 7f39bdd..3942c7f 100644 --- a/src/Data/Sum.agda +++ b/src/Data/Sum.agda @@ -19,8 +19,8 @@ data _⊎_ {a b} (A : Set a) (B : Set b) : Set (a ⊔ b) where inj₁ : (x : A) → A ⊎ B inj₂ : (y : B) → A ⊎ B -{-# IMPORT Data.FFI #-} -{-# COMPILED_DATA _⊎_ Data.FFI.AgdaEither Left Right #-} +{-# HASKELL type AgdaEither a b c d = Either c d #-} +{-# COMPILED_DATA _⊎_ MAlonzo.Code.Data.Sum.AgdaEither Left Right #-} ------------------------------------------------------------------------ -- Functions diff --git a/src/Data/Unit/Base.agda b/src/Data/Unit/Base.agda index f7cb84d..e3b7de8 100644 --- a/src/Data/Unit/Base.agda +++ b/src/Data/Unit/Base.agda @@ -10,7 +10,6 @@ module Data.Unit.Base where -- Note that the name of this type is "\top", not T. -record ⊤ : Set where - constructor tt +open import Agda.Builtin.Unit public using (⊤; tt) record _≤_ (x y : ⊤) : Set where diff --git a/src/Data/Vec/N-ary.agda b/src/Data/Vec/N-ary.agda index c6b49c1..32386a2 100644 --- a/src/Data/Vec/N-ary.agda +++ b/src/Data/Vec/N-ary.agda @@ -48,6 +48,8 @@ f $ⁿ (x ∷ xs) = f x $ⁿ xs N-ary n A (Set ℓ) → Set (N-ary-level a ℓ n) ∀ⁿ zero P = P ∀ⁿ (suc n) P = ∀ x → ∀ⁿ n (P x) +{- Normalising is very slow for this function for some reason... -} +{-# NO_SMASHING ∀ⁿ #-} -- Universal quantifier with implicit (hidden) arguments. diff --git a/src/Foreign/Haskell.agda b/src/Foreign/Haskell.agda index e0c462a..1a88fb4 100644 --- a/src/Foreign/Haskell.agda +++ b/src/Foreign/Haskell.agda @@ -12,3 +12,4 @@ data Unit : Set where unit : Unit {-# COMPILED_DATA Unit () () #-} +{-# COMPILED_DATA_UHC Unit __UNIT__ __UNIT__ #-} diff --git a/src/IO/Primitive.agda b/src/IO/Primitive.agda index dcd7462..b6a33fc 100644 --- a/src/IO/Primitive.agda +++ b/src/IO/Primitive.agda @@ -13,12 +13,7 @@ open import Foreign.Haskell ------------------------------------------------------------------------ -- The IO monad -postulate - IO : ∀ {ℓ} → Set ℓ → Set ℓ - -{-# IMPORT IO.FFI #-} -{-# COMPILED_TYPE IO IO.FFI.AgdaIO #-} -{-# BUILTIN IO IO #-} +open import Agda.Builtin.IO public using (IO) infixl 1 _>>=_ @@ -28,6 +23,8 @@ postulate {-# COMPILED return (\_ _ -> return) #-} {-# COMPILED _>>=_ (\_ _ _ _ -> (>>=)) #-} +{-# COMPILED_UHC return (\_ _ x -> UHC.Agda.Builtins.primReturn x) #-} +{-# COMPILED_UHC _>>=_ (\_ _ _ _ x y -> UHC.Agda.Builtins.primBind x y) #-} ------------------------------------------------------------------------ -- Simple lazy IO @@ -41,6 +38,11 @@ postulate -- the locale. For older versions of the library (going back to at -- least version 3) the functions use ISO-8859-1. +{-# IMPORT Data.Text #-} +{-# IMPORT Data.Text.IO #-} +{-# IMPORT System.IO #-} +{-# IMPORT Control.Exception #-} + postulate getContents : IO Costring readFile : String → IO Costring @@ -54,10 +56,26 @@ postulate readFiniteFile : String → IO String -{-# COMPILED getContents getContents #-} -{-# COMPILED readFile readFile #-} -{-# COMPILED writeFile writeFile #-} -{-# COMPILED appendFile appendFile #-} -{-# COMPILED putStr putStr #-} -{-# COMPILED putStrLn putStrLn #-} -{-# COMPILED readFiniteFile IO.FFI.readFiniteFile #-} +{-# HASKELL + readFiniteFile :: Data.Text.Text -> IO Data.Text.Text + readFiniteFile f = do + h <- System.IO.openFile (Data.Text.unpack f) System.IO.ReadMode + Control.Exception.bracketOnError (return ()) (\_ -> System.IO.hClose h) + (\_ -> System.IO.hFileSize h) + Data.Text.IO.hGetContents h +#-} + +{-# COMPILED getContents getContents #-} +{-# COMPILED readFile (readFile . Data.Text.unpack) #-} +{-# COMPILED writeFile (\x -> writeFile (Data.Text.unpack x)) #-} +{-# COMPILED appendFile (\x -> appendFile (Data.Text.unpack x)) #-} +{-# COMPILED putStr putStr #-} +{-# COMPILED putStrLn putStrLn #-} +{-# COMPILED readFiniteFile readFiniteFile #-} +{-# COMPILED_UHC getContents (UHC.Agda.Builtins.primGetContents) #-} +{-# COMPILED_UHC readFile (UHC.Agda.Builtins.primReadFile) #-} +{-# COMPILED_UHC writeFile (UHC.Agda.Builtins.primWriteFile) #-} +{-# COMPILED_UHC appendFile (UHC.Agda.Builtins.primAppendFile) #-} +{-# COMPILED_UHC putStr (UHC.Agda.Builtins.primPutStr) #-} +{-# COMPILED_UHC putStrLn (UHC.Agda.Builtins.primPutStrLn) #-} +{-# COMPILED_UHC readFiniteFile (UHC.Agda.Builtins.primReadFiniteFile) #-} diff --git a/src/Irrelevance.agda b/src/Irrelevance.agda index 2a39b84..31fb54a 100644 --- a/src/Irrelevance.agda +++ b/src/Irrelevance.agda @@ -7,14 +7,3 @@ module Irrelevance where import Level - ------------------------------------------------------------------------- --- The irrelevance axiom - --- There is no guarantee that this axiom is sound. Use it at your own --- risk. - -postulate - .irrelevance-axiom : ∀ {a} {A : Set a} → .A → A - -{-# BUILTIN IRRAXIOM irrelevance-axiom #-} diff --git a/src/Record.agda b/src/Record.agda index 1181db7..1929f90 100644 --- a/src/Record.agda +++ b/src/Record.agda @@ -63,6 +63,7 @@ mutual -- inferred from a value of type Record Sig. record Record {s} (Sig : Signature s) : Set s where + eta-equality inductive constructor rec field fun : Record-fun Sig @@ -72,10 +73,6 @@ mutual Record-fun (Sig , ℓ ∶ A) = Σ (Record Sig) A Record-fun (Sig , ℓ ≔ a) = Manifest-Σ (Record Sig) a --- Eta-equality is enabled for Record. - -{-# ETA Record #-} - ------------------------------------------------------------------------ -- Labels diff --git a/src/Reflection.agda b/src/Reflection.agda index 5446271..2c79980 100644 --- a/src/Reflection.agda +++ b/src/Reflection.agda @@ -6,6 +6,7 @@ module Reflection where +open import Data.Unit.Base using (⊤) open import Data.Bool.Base using (Bool; false; true) open import Data.List.Base using (List); open Data.List.Base.List open import Data.Nat using (ℕ) renaming (_≟_ to _≟-ℕ_) @@ -22,18 +23,14 @@ open import Relation.Nullary hiding (module Dec) open import Relation.Nullary.Decidable as Dec open import Relation.Nullary.Product +import Agda.Builtin.Reflection as Builtin + ------------------------------------------------------------------------ -- Names -- Names. -postulate Name : Set - -{-# BUILTIN QNAME Name #-} - -private - primitive - primQNameEquality : Name → Name → Bool +open Builtin public using (Name) -- Equality of names is decidable. @@ -42,7 +39,7 @@ infix 4 _==_ _≟-Name_ private _==_ : Name → Name → Bool - _==_ = primQNameEquality + _==_ = Builtin.primQNameEquality _≟-Name_ : Decidable {A = Name} _≡_ s₁ ≟-Name s₂ with s₁ == s₂ @@ -52,40 +49,50 @@ s₁ ≟-Name s₂ with s₁ == s₂ -- Names can be shown. +showName : Name → String +showName = Builtin.primShowQName + +------------------------------------------------------------------------ +-- Metavariables + +-- Metavariables. + +open Builtin public using (Meta) + +-- Equality of metavariables is decidable. + +infix 4 _==-Meta_ _≟-Meta_ + private - primitive - primShowQName : Name → String -showName : Name → String -showName = primShowQName + _==-Meta_ : Meta → Meta → Bool + _==-Meta_ = Builtin.primMetaEquality + +_≟-Meta_ : Decidable {A = Meta} _≡_ +s₁ ≟-Meta s₂ with s₁ ==-Meta s₂ +... | true = yes trustMe +... | false = no whatever + where postulate whatever : _ + +-- Metas can be shown. + +showMeta : Meta → String +showMeta = Builtin.primShowMeta ------------------------------------------------------------------------ -- Terms -- Is the argument visible (explicit), hidden (implicit), or an -- instance argument? - -data Visibility : Set where - visible hidden instance′ : Visibility - -{-# BUILTIN HIDING Visibility #-} -{-# BUILTIN VISIBLE visible #-} -{-# BUILTIN HIDDEN hidden #-} -{-# BUILTIN INSTANCE instance′ #-} +open Builtin public using (Visibility; visible; hidden; instance′) -- Arguments can be relevant or irrelevant. - -data Relevance : Set where - relevant irrelevant : Relevance - -{-# BUILTIN RELEVANCE Relevance #-} -{-# BUILTIN RELEVANT relevant #-} -{-# BUILTIN IRRELEVANT irrelevant #-} +open Builtin public using (Relevance; relevant; irrelevant) -- Arguments. - -data Arg-info : Set where - arg-info : (v : Visibility) (r : Relevance) → Arg-info +open Builtin public + renaming ( ArgInfo to Arg-info ) + using ( arg-info ) visibility : Arg-info → Visibility visibility (arg-info v _) = v @@ -93,142 +100,39 @@ visibility (arg-info v _) = v relevance : Arg-info → Relevance relevance (arg-info _ r) = r -data Arg (A : Set) : Set where - arg : (i : Arg-info) (x : A) → Arg A - -{-# BUILTIN ARGINFO Arg-info #-} -{-# BUILTIN ARGARGINFO arg-info #-} -{-# BUILTIN ARG Arg #-} -{-# BUILTIN ARGARG arg #-} +open Builtin public using (Arg; arg) +open Builtin public using (Abs; abs) -- Literals. -data Literal : Set where - nat : ℕ → Literal - float : Float → Literal - char : Char → Literal - string : String → Literal - name : Name → Literal +open Builtin public using (Literal; nat; float; char; string; name; meta) -{-# BUILTIN AGDALITERAL Literal #-} -{-# BUILTIN AGDALITNAT nat #-} -{-# BUILTIN AGDALITFLOAT float #-} -{-# BUILTIN AGDALITCHAR char #-} -{-# BUILTIN AGDALITSTRING string #-} -{-# BUILTIN AGDALITQNAME name #-} +-- Patterns. + +open Builtin public using (Pattern; con; dot; var; lit; proj; absurd) -- Terms. -mutual - data Term : Set where - -- Variable applied to arguments. - var : (x : ℕ) (args : List (Arg Term)) → Term - -- Constructor applied to arguments. - con : (c : Name) (args : List (Arg Term)) → Term - -- Identifier applied to arguments. - def : (f : Name) (args : List (Arg Term)) → Term - -- Different kinds of λ-abstraction. - lam : (v : Visibility) (t : Term) → Term - -- Pattern matching λ-abstraction. - pat-lam : (cs : List Clause) (args : List (Arg Term)) → Term - -- Pi-type. - pi : (t₁ : Arg Type) (t₂ : Type) → Term - -- A sort. - sort : Sort → Term - -- A literal. - lit : Literal → Term - -- Anything else. - unknown : Term - - data Type : Set where - el : (s : Sort) (t : Term) → Type - - data Sort : Set where - -- A Set of a given (possibly neutral) level. - set : (t : Term) → Sort - -- A Set of a given concrete level. - lit : (n : ℕ) → Sort - -- Anything else. - unknown : Sort - - data Pattern : Set where - con : Name → List (Arg Pattern) → Pattern - dot : Pattern - var : Pattern - lit : Literal → Pattern - proj : Name → Pattern - absurd : Pattern - - data Clause : Set where - clause : List (Arg Pattern) → Term → Clause - absurd-clause : List (Arg Pattern) → Clause - -{-# BUILTIN AGDASORT Sort #-} -{-# BUILTIN AGDATYPE Type #-} -{-# BUILTIN AGDATERM Term #-} -{-# BUILTIN AGDAPATTERN Pattern #-} -{-# BUILTIN AGDACLAUSE Clause #-} - -{-# BUILTIN AGDATERMVAR var #-} -{-# BUILTIN AGDATERMCON con #-} -{-# BUILTIN AGDATERMDEF def #-} -{-# BUILTIN AGDATERMLAM lam #-} -{-# BUILTIN AGDATERMEXTLAM pat-lam #-} -{-# BUILTIN AGDATERMPI pi #-} -{-# BUILTIN AGDATERMSORT sort #-} -{-# BUILTIN AGDATERMLIT lit #-} -{-# BUILTIN AGDATERMUNSUPPORTED unknown #-} -{-# BUILTIN AGDATYPEEL el #-} -{-# BUILTIN AGDASORTSET set #-} -{-# BUILTIN AGDASORTLIT lit #-} -{-# BUILTIN AGDASORTUNSUPPORTED unknown #-} - -{-# BUILTIN AGDAPATCON con #-} -{-# BUILTIN AGDAPATDOT dot #-} -{-# BUILTIN AGDAPATVAR var #-} -{-# BUILTIN AGDAPATLIT lit #-} -{-# BUILTIN AGDAPATPROJ proj #-} -{-# BUILTIN AGDAPATABSURD absurd #-} - -{-# BUILTIN AGDACLAUSECLAUSE clause #-} -{-# BUILTIN AGDACLAUSEABSURD absurd-clause #-} +open Builtin public + using ( Type; Term; var; con; def; lam; pat-lam; pi; lit; meta; unknown + ; Sort; set + ; Clause; clause; absurd-clause ) + renaming ( agda-sort to sort ) + +Clauses = List Clause ------------------------------------------------------------------------ -- Definitions --- Function definition. -data FunctionDef : Set where - fun-def : Type → List Clause → FunctionDef - -{-# BUILTIN AGDAFUNDEF FunctionDef #-} -{-# BUILTIN AGDAFUNDEFCON fun-def #-} - -postulate - -- Data type definition. - Data-type : Set - -- Record type definition. - Record : Set - -{-# BUILTIN AGDADATADEF Data-type #-} -{-# BUILTIN AGDARECORDDEF Record #-} - --- Definitions. - -data Definition : Set where - function : FunctionDef → Definition - data-type : Data-type → Definition - record′ : Record → Definition - constructor′ : Definition - axiom : Definition - primitive′ : Definition - -{-# BUILTIN AGDADEFINITION Definition #-} -{-# BUILTIN AGDADEFINITIONFUNDEF function #-} -{-# BUILTIN AGDADEFINITIONDATADEF data-type #-} -{-# BUILTIN AGDADEFINITIONRECORDDEF record′ #-} -{-# BUILTIN AGDADEFINITIONDATACONSTRUCTOR constructor′ #-} -{-# BUILTIN AGDADEFINITIONPOSTULATE axiom #-} -{-# BUILTIN AGDADEFINITIONPRIMITIVE primitive′ #-} +open Builtin public + using ( Definition + ; function + ; data-type + ; axiom + ) + renaming ( record-type to record′ + ; data-cons to constructor′ + ; prim-fun to primitive′ ) showLiteral : Literal → String showLiteral (nat x) = showNat x @@ -236,27 +140,23 @@ showLiteral (float x) = showFloat x showLiteral (char x) = showChar x showLiteral (string x) = showString x showLiteral (name x) = showName x +showLiteral (meta x) = showMeta x -private - primitive - primQNameType : Name → Type - primQNameDefinition : Name → Definition - primDataConstructors : Data-type → List Name - --- The type of the thing with the given name. - -type : Name → Type -type = primQNameType - --- The definition of the thing with the given name. +------------------------------------------------------------------------ +-- Type checking monad -definition : Name → Definition -definition = primQNameDefinition +-- Type errors +open Builtin public using (ErrorPart; strErr; termErr; nameErr) --- The constructors of the given data type. +-- The monad +open Builtin public + using ( TC; returnTC; bindTC; unify; typeError; inferType; checkType + ; normalise; catchTC; getContext; extendContext; inContext + ; freshName; declareDef; defineFun; getType; getDefinition + ; blockOnMeta; quoteTC; unquoteTC ) -constructors : Data-type → List Name -constructors = primDataConstructors +newMeta : Type → TC Term +newMeta = checkType unknown ------------------------------------------------------------------------ -- Term equality is decidable @@ -279,6 +179,12 @@ private arg₂ : ∀ {A i i′} {x x′ : A} → arg i x ≡ arg i′ x′ → x ≡ x′ arg₂ refl = refl + abs₁ : ∀ {A i i′} {x x′ : A} → abs i x ≡ abs i′ x′ → i ≡ i′ + abs₁ refl = refl + + abs₂ : ∀ {A i i′} {x x′ : A} → abs i x ≡ abs i′ x′ → x ≡ x′ + abs₂ refl = refl + arg-info₁ : ∀ {v v′ r r′} → arg-info v r ≡ arg-info v′ r′ → v ≡ v′ arg-info₁ refl = refl @@ -309,6 +215,12 @@ private def₂ : ∀ {f f′ args args′} → def f args ≡ def f′ args′ → args ≡ args′ def₂ refl = refl + meta₁ : ∀ {x x′ args args′} → Term.meta x args ≡ meta x′ args′ → x ≡ x′ + meta₁ refl = refl + + meta₂ : ∀ {x x′ args args′} → Term.meta x args ≡ meta x′ args′ → args ≡ args′ + meta₂ refl = refl + lam₁ : ∀ {v v′ t t′} → lam v t ≡ lam v′ t′ → v ≡ v′ lam₁ refl = refl @@ -339,6 +251,9 @@ private pcon₂ : ∀ {c c′ args args′} → Pattern.con c args ≡ con c′ args′ → args ≡ args′ pcon₂ refl = refl + pvar : ∀ {x y} → Pattern.var x ≡ var y → x ≡ y + pvar refl = refl + plit₁ : ∀ {x y} → Pattern.lit x ≡ lit y → x ≡ y plit₁ refl = refl @@ -351,12 +266,6 @@ private slit₁ : ∀ {x y} → Sort.lit x ≡ lit y → x ≡ y slit₁ refl = refl - el₁ : ∀ {s s′ t t′} → el s t ≡ el s′ t′ → s ≡ s′ - el₁ refl = refl - - el₂ : ∀ {s s′ t t′} → el s t ≡ el s′ t′ → t ≡ t′ - el₂ refl = refl - nat₁ : ∀ {x y} → nat x ≡ nat y → x ≡ y nat₁ refl = refl @@ -372,6 +281,9 @@ private name₁ : ∀ {x y} → name x ≡ name y → x ≡ y name₁ refl = refl + lmeta₁ : ∀ {x y} → Literal.meta x ≡ meta y → x ≡ y + lmeta₁ refl = refl + clause₁ : ∀ {ps ps′ b b′} → clause ps b ≡ clause ps′ b′ → ps ≡ ps′ clause₁ refl = refl @@ -381,9 +293,9 @@ private absurd-clause₁ : ∀ {ps ps′} → absurd-clause ps ≡ absurd-clause ps′ → ps ≡ ps′ absurd-clause₁ refl = refl -infix 4 _≟-Visibility_ _≟-Relevance_ _≟-Arg-info_ _≟-Lit_ - _≟-ArgTerm_ _≟-ArgType_ _≟-ArgPattern_ _≟-Args_ - _≟-Clause_ _≟-Clauses_ _≟-Pattern_ _≟-ArgPatterns_ _≟_ _≟-Type_ +infix 4 _≟-Visibility_ _≟-Relevance_ _≟-Arg-info_ _≟-Lit_ _≟-AbsTerm_ + _≟-AbsType_ _≟-ArgTerm_ _≟-ArgType_ _≟-ArgPattern_ _≟-Args_ + _≟-Clause_ _≟-Clauses_ _≟-Pattern_ _≟-ArgPatterns_ _≟_ _≟-Sort_ _≟-Visibility_ : Decidable (_≡_ {A = Visibility}) @@ -415,28 +327,51 @@ nat x ≟-Lit float x₁ = no (λ ()) nat x ≟-Lit char x₁ = no (λ ()) nat x ≟-Lit string x₁ = no (λ ()) nat x ≟-Lit name x₁ = no (λ ()) +nat x ≟-Lit meta x₁ = no (λ ()) float x ≟-Lit nat x₁ = no (λ ()) float x ≟-Lit float x₁ = Dec.map′ (cong float) float₁ (x ≟f x₁) float x ≟-Lit char x₁ = no (λ ()) float x ≟-Lit string x₁ = no (λ ()) float x ≟-Lit name x₁ = no (λ ()) +float x ≟-Lit meta x₁ = no (λ ()) char x ≟-Lit nat x₁ = no (λ ()) char x ≟-Lit float x₁ = no (λ ()) char x ≟-Lit char x₁ = Dec.map′ (cong char) char₁ (x ≟c x₁) char x ≟-Lit string x₁ = no (λ ()) char x ≟-Lit name x₁ = no (λ ()) +char x ≟-Lit meta x₁ = no (λ ()) string x ≟-Lit nat x₁ = no (λ ()) string x ≟-Lit float x₁ = no (λ ()) string x ≟-Lit char x₁ = no (λ ()) string x ≟-Lit string x₁ = Dec.map′ (cong string) string₁ (x ≟s x₁) string x ≟-Lit name x₁ = no (λ ()) +string x ≟-Lit meta x₁ = no (λ ()) name x ≟-Lit nat x₁ = no (λ ()) name x ≟-Lit float x₁ = no (λ ()) name x ≟-Lit char x₁ = no (λ ()) name x ≟-Lit string x₁ = no (λ ()) name x ≟-Lit name x₁ = Dec.map′ (cong name) name₁ (x ≟-Name x₁) +name x ≟-Lit meta x₁ = no (λ ()) +meta x ≟-Lit nat x₁ = no (λ ()) +meta x ≟-Lit float x₁ = no (λ ()) +meta x ≟-Lit char x₁ = no (λ ()) +meta x ≟-Lit string x₁ = no (λ ()) +meta x ≟-Lit name x₁ = no (λ ()) +meta x ≟-Lit meta x₁ = Dec.map′ (cong meta) lmeta₁ (x ≟-Meta x₁) mutual + _≟-AbsTerm_ : Decidable (_≡_ {A = Abs Term}) + abs s a ≟-AbsTerm abs s′ a′ = + Dec.map′ (cong₂′ abs) + < abs₁ , abs₂ > + (s ≟s s′ ×-dec a ≟ a′) + + _≟-AbsType_ : Decidable (_≡_ {A = Abs Type}) + abs s a ≟-AbsType abs s′ a′ = + Dec.map′ (cong₂′ abs) + < abs₁ , abs₂ > + (s ≟s s′ ×-dec a ≟ a′) + _≟-ArgTerm_ : Decidable (_≡_ {A = Arg Term}) arg i a ≟-ArgTerm arg i′ a′ = Dec.map′ (cong₂′ arg) @@ -447,7 +382,7 @@ mutual arg i a ≟-ArgType arg i′ a′ = Dec.map′ (cong₂′ arg) < arg₁ , arg₂ > - (i ≟-Arg-info i′ ×-dec a ≟-Type a′) + (i ≟-Arg-info i′ ×-dec a ≟ a′) _≟-ArgPattern_ : Decidable (_≡_ {A = Arg Pattern}) arg i a ≟-ArgPattern arg i′ a′ = @@ -467,7 +402,7 @@ mutual clause _ _ ≟-Clause absurd-clause _ = no λ() absurd-clause _ ≟-Clause clause _ _ = no λ() - _≟-Clauses_ : Decidable (_≡_ {A = List Clause}) + _≟-Clauses_ : Decidable (_≡_ {A = Clauses}) [] ≟-Clauses [] = yes refl (x ∷ xs) ≟-Clauses (y ∷ ys) = Dec.map′ (cong₂′ _∷_) < cons₁ , cons₂ > (x ≟-Clause y ×-dec xs ≟-Clauses ys) [] ≟-Clauses (_ ∷ _) = no λ() @@ -476,37 +411,37 @@ mutual _≟-Pattern_ : Decidable (_≡_ {A = Pattern}) con c ps ≟-Pattern con c′ ps′ = Dec.map′ (cong₂′ con) < pcon₁ , pcon₂ > (c ≟-Name c′ ×-dec ps ≟-ArgPatterns ps′) con x x₁ ≟-Pattern dot = no (λ ()) - con x x₁ ≟-Pattern var = no (λ ()) + con x x₁ ≟-Pattern var x₂ = no (λ ()) con x x₁ ≟-Pattern lit x₂ = no (λ ()) con x x₁ ≟-Pattern proj x₂ = no (λ ()) con x x₁ ≟-Pattern absurd = no (λ ()) dot ≟-Pattern con x x₁ = no (λ ()) dot ≟-Pattern dot = yes refl - dot ≟-Pattern var = no (λ ()) + dot ≟-Pattern var x = no (λ ()) dot ≟-Pattern lit x = no (λ ()) dot ≟-Pattern proj x = no (λ ()) dot ≟-Pattern absurd = no (λ ()) - var ≟-Pattern con x x₁ = no (λ ()) - var ≟-Pattern dot = no (λ ()) - var ≟-Pattern var = yes refl - var ≟-Pattern lit x = no (λ ()) - var ≟-Pattern proj x = no (λ ()) - var ≟-Pattern absurd = no (λ ()) + var s ≟-Pattern con x x₁ = no (λ ()) + var s ≟-Pattern dot = no (λ ()) + var s ≟-Pattern var s′ = Dec.map′ (cong var) pvar (s ≟s s′) + var s ≟-Pattern lit x = no (λ ()) + var s ≟-Pattern proj x = no (λ ()) + var s ≟-Pattern absurd = no (λ ()) lit x ≟-Pattern con x₁ x₂ = no (λ ()) lit x ≟-Pattern dot = no (λ ()) - lit x ≟-Pattern var = no (λ ()) + lit x ≟-Pattern var _ = no (λ ()) lit l ≟-Pattern lit l′ = Dec.map′ (cong lit) plit₁ (l ≟-Lit l′) lit x ≟-Pattern proj x₁ = no (λ ()) lit x ≟-Pattern absurd = no (λ ()) proj x ≟-Pattern con x₁ x₂ = no (λ ()) proj x ≟-Pattern dot = no (λ ()) - proj x ≟-Pattern var = no (λ ()) + proj x ≟-Pattern var _ = no (λ ()) proj x ≟-Pattern lit x₁ = no (λ ()) proj x ≟-Pattern proj x₁ = Dec.map′ (cong proj) pproj₁ (x ≟-Name x₁) proj x ≟-Pattern absurd = no (λ ()) absurd ≟-Pattern con x x₁ = no (λ ()) absurd ≟-Pattern dot = no (λ ()) - absurd ≟-Pattern var = no (λ ()) + absurd ≟-Pattern var _ = no (λ ()) absurd ≟-Pattern lit x = no (λ ()) absurd ≟-Pattern proj x = no (λ ()) absurd ≟-Pattern absurd = yes refl @@ -521,10 +456,11 @@ mutual var x args ≟ var x′ args′ = Dec.map′ (cong₂′ var) < var₁ , var₂ > (x ≟-ℕ x′ ×-dec args ≟-Args args′) con c args ≟ con c′ args′ = Dec.map′ (cong₂′ con) < con₁ , con₂ > (c ≟-Name c′ ×-dec args ≟-Args args′) def f args ≟ def f′ args′ = Dec.map′ (cong₂′ def) < def₁ , def₂ > (f ≟-Name f′ ×-dec args ≟-Args args′) - lam v t ≟ lam v′ t′ = Dec.map′ (cong₂′ lam) < lam₁ , lam₂ > (v ≟-Visibility v′ ×-dec t ≟ t′) + meta x args ≟ meta x′ args′ = Dec.map′ (cong₂′ meta) < meta₁ , meta₂ > (x ≟-Meta x′ ×-dec args ≟-Args args′) + lam v t ≟ lam v′ t′ = Dec.map′ (cong₂′ lam) < lam₁ , lam₂ > (v ≟-Visibility v′ ×-dec t ≟-AbsTerm t′) pat-lam cs args ≟ pat-lam cs′ args′ = Dec.map′ (cong₂′ pat-lam) < pat-lam₁ , pat-lam₂ > (cs ≟-Clauses cs′ ×-dec args ≟-Args args′) - pi t₁ t₂ ≟ pi t₁′ t₂′ = Dec.map′ (cong₂′ pi) < pi₁ , pi₂ > (t₁ ≟-ArgType t₁′ ×-dec t₂ ≟-Type t₂′) + pi t₁ t₂ ≟ pi t₁′ t₂′ = Dec.map′ (cong₂′ pi) < pi₁ , pi₂ > (t₁ ≟-ArgType t₁′ ×-dec t₂ ≟-AbsType t₂′) sort s ≟ sort s′ = Dec.map′ (cong sort) sort₁ (s ≟-Sort s′) lit l ≟ lit l′ = Dec.map′ (cong lit) lit₁ (l ≟-Lit l′) unknown ≟ unknown = yes refl @@ -535,6 +471,7 @@ mutual var x args ≟ pi t₁ t₂ = no λ() var x args ≟ sort _ = no λ() var x args ≟ lit _ = no λ() + var x args ≟ meta _ _ = no λ() var x args ≟ unknown = no λ() con c args ≟ var x args′ = no λ() con c args ≟ def f args′ = no λ() @@ -542,6 +479,7 @@ mutual con c args ≟ pi t₁ t₂ = no λ() con c args ≟ sort _ = no λ() con c args ≟ lit _ = no λ() + con c args ≟ meta _ _ = no λ() con c args ≟ unknown = no λ() def f args ≟ var x args′ = no λ() def f args ≟ con c args′ = no λ() @@ -549,6 +487,7 @@ mutual def f args ≟ pi t₁ t₂ = no λ() def f args ≟ sort _ = no λ() def f args ≟ lit _ = no λ() + def f args ≟ meta _ _ = no λ() def f args ≟ unknown = no λ() lam v t ≟ var x args = no λ() lam v t ≟ con c args = no λ() @@ -556,6 +495,7 @@ mutual lam v t ≟ pi t₁ t₂ = no λ() lam v t ≟ sort _ = no λ() lam v t ≟ lit _ = no λ() + lam v t ≟ meta _ _ = no λ() lam v t ≟ unknown = no λ() pi t₁ t₂ ≟ var x args = no λ() pi t₁ t₂ ≟ con c args = no λ() @@ -563,6 +503,7 @@ mutual pi t₁ t₂ ≟ lam v t = no λ() pi t₁ t₂ ≟ sort _ = no λ() pi t₁ t₂ ≟ lit _ = no λ() + pi t₁ t₂ ≟ meta _ _ = no λ() pi t₁ t₂ ≟ unknown = no λ() sort _ ≟ var x args = no λ() sort _ ≟ con c args = no λ() @@ -570,6 +511,7 @@ mutual sort _ ≟ lam v t = no λ() sort _ ≟ pi t₁ t₂ = no λ() sort _ ≟ lit _ = no λ() + sort _ ≟ meta _ _ = no λ() sort _ ≟ unknown = no λ() lit _ ≟ var x args = no λ() lit _ ≟ con c args = no λ() @@ -577,7 +519,16 @@ mutual lit _ ≟ lam v t = no λ() lit _ ≟ pi t₁ t₂ = no λ() lit _ ≟ sort _ = no λ() + lit _ ≟ meta _ _ = no λ() lit _ ≟ unknown = no λ() + meta _ _ ≟ var x args = no λ() + meta _ _ ≟ con c args = no λ() + meta _ _ ≟ def f args = no λ() + meta _ _ ≟ lam v t = no λ() + meta _ _ ≟ pi t₁ t₂ = no λ() + meta _ _ ≟ sort _ = no λ() + meta _ _ ≟ lit _ = no λ() + meta _ _ ≟ unknown = no λ() unknown ≟ var x args = no λ() unknown ≟ con c args = no λ() unknown ≟ def f args = no λ() @@ -585,6 +536,7 @@ mutual unknown ≟ pi t₁ t₂ = no λ() unknown ≟ sort _ = no λ() unknown ≟ lit _ = no λ() + unknown ≟ meta _ _ = no λ() pat-lam _ _ ≟ var x args = no λ() pat-lam _ _ ≟ con c args = no λ() pat-lam _ _ ≟ def f args = no λ() @@ -592,6 +544,7 @@ mutual pat-lam _ _ ≟ pi t₁ t₂ = no λ() pat-lam _ _ ≟ sort _ = no λ() pat-lam _ _ ≟ lit _ = no λ() + pat-lam _ _ ≟ meta _ _ = no λ() pat-lam _ _ ≟ unknown = no λ() var x args ≟ pat-lam _ _ = no λ() con c args ≟ pat-lam _ _ = no λ() @@ -600,11 +553,9 @@ mutual pi t₁ t₂ ≟ pat-lam _ _ = no λ() sort _ ≟ pat-lam _ _ = no λ() lit _ ≟ pat-lam _ _ = no λ() + meta _ _ ≟ pat-lam _ _ = no λ() unknown ≟ pat-lam _ _ = no λ() - _≟-Type_ : Decidable (_≡_ {A = Type}) - el s t ≟-Type el s′ t′ = Dec.map′ (cong₂′ el) < el₁ , el₂ > (s ≟-Sort s′ ×-dec t ≟ t′) - _≟-Sort_ : Decidable (_≡_ {A = Sort}) set t ≟-Sort set t′ = Dec.map′ (cong set) set₁ (t ≟ t′) lit n ≟-Sort lit n′ = Dec.map′ (cong lit) slit₁ (n ≟-ℕ n′) diff --git a/src/Relation/Binary.agda b/src/Relation/Binary.agda index 27fc8e0..54fef09 100644 --- a/src/Relation/Binary.agda +++ b/src/Relation/Binary.agda @@ -358,7 +358,6 @@ record IsStrictTotalOrder {a ℓ₁ ℓ₂} {A : Set a} isEquivalence : IsEquivalence _≈_ trans : Transitive _<_ compare : Trichotomous _≈_ _<_ - <-resp-≈ : _<_ Respects₂ _≈_ infix 4 _≟_ _<?_ @@ -376,10 +375,13 @@ record IsStrictTotalOrder {a ℓ₁ ℓ₂} {A : Set a} module Eq = IsDecEquivalence isDecEquivalence + <-resp-≈ : _<_ Respects₂ _≈_ + <-resp-≈ = trans∧tri⟶resp≈ Eq.sym Eq.trans trans compare + isStrictPartialOrder : IsStrictPartialOrder _≈_ _<_ isStrictPartialOrder = record { isEquivalence = isEquivalence - ; irrefl = tri⟶irr <-resp-≈ Eq.sym compare + ; irrefl = tri⟶irr compare ; trans = trans ; <-resp-≈ = <-resp-≈ } diff --git a/src/Relation/Binary/Consequences.agda b/src/Relation/Binary/Consequences.agda index 91ef677..4b0f071 100644 --- a/src/Relation/Binary/Consequences.agda +++ b/src/Relation/Binary/Consequences.agda @@ -85,9 +85,34 @@ tri⟶asym tri {x} {y} x<y x>y with tri x y tri⟶irr : ∀ {a ℓ₁ ℓ₂} {A : Set a} {_≈_ : Rel A ℓ₁} {_<_ : Rel A ℓ₂} → - _<_ Respects₂ _≈_ → Symmetric _≈_ → Trichotomous _≈_ _<_ → Irreflexive _≈_ _<_ -tri⟶irr resp sym tri = asym⟶irr resp sym (tri⟶asym tri) +tri⟶irr {_≈_ = _≈_} {_<_} compare = irr + where + irr : ∀ {x y} → x ≈ y → ¬ (x < y) + irr {x} {y} x≈y x<y with compare x y + ... | tri< _ x≉y y≮x = x≉y x≈y + ... | tri> x≮y x≉y y<x = x≉y x≈y + ... | tri≈ x≮y _ y≮x = x≮y x<y + +trans∧tri⟶resp≈ : + ∀ {a ℓ₁ ℓ₂} {A : Set a} {_≈_ : Rel A ℓ₁} {_<_ : Rel A ℓ₂} → + Symmetric _≈_ → Transitive _≈_ → + Transitive _<_ → Trichotomous _≈_ _<_ → + _<_ Respects₂ _≈_ +trans∧tri⟶resp≈ {_≈_ = _≈_} {_<_} sym trans <-trans tri = + respʳ , respˡ + where + respʳ : ∀ {x y z} → y ≈ z → x < y → x < z + respʳ {x} {z = z} y≈z x<y with tri x z + ... | tri< x<z _ _ = x<z + ... | tri≈ _ x≈z _ = ⊥-elim (tri⟶irr tri (trans x≈z (sym y≈z)) x<y) + ... | tri> _ _ z<x = ⊥-elim (tri⟶irr tri (sym y≈z) (<-trans z<x x<y)) + + respˡ : ∀ {z x y} → x ≈ y → x < z → y < z + respˡ {z} {y = y} x≈y x<z with tri y z + ... | tri< y<z _ _ = y<z + ... | tri≈ _ y≈z _ = ⊥-elim (tri⟶irr tri (trans x≈y y≈z) x<z) + ... | tri> _ _ z<y = ⊥-elim (tri⟶irr tri x≈y (<-trans x<z z<y)) tri⟶dec≈ : ∀ {a ℓ₁ ℓ₂} {A : Set a} {_≈_ : Rel A ℓ₁} {_<_ : Rel A ℓ₂} → diff --git a/src/Relation/Binary/Core.agda b/src/Relation/Binary/Core.agda index 89880ad..8b927f8 100644 --- a/src/Relation/Binary/Core.agda +++ b/src/Relation/Binary/Core.agda @@ -139,21 +139,11 @@ record NonEmpty {a b ℓ} {A : Set a} {B : Set b} -- refl defined in IsEquivalence below. The module is opened publicly -- at the end of this file. -private - module Dummy where +import Agda.Builtin.Equality as Dummy - infix 4 _≡_ _≢_ - - data _≡_ {a} {A : Set a} (x : A) : A → Set a where - refl : x ≡ x - - {-# BUILTIN EQUALITY _≡_ #-} - {-# BUILTIN REFL refl #-} - - -- Nonequality. - - _≢_ : ∀ {a} {A : Set a} → A → A → Set a - x ≢ y = ¬ x ≡ y +infix 4 _≢_ +_≢_ : ∀ {a} {A : Set a} → A → A → Set a +x ≢ y = ¬ x Dummy.≡ y ------------------------------------------------------------------------ -- Equivalence relations diff --git a/src/Relation/Binary/EqReasoning.agda b/src/Relation/Binary/EqReasoning.agda index cee1043..394cb50 100644 --- a/src/Relation/Binary/EqReasoning.agda +++ b/src/Relation/Binary/EqReasoning.agda @@ -19,10 +19,8 @@ -- 0 -- ∎ --- Note that some modules contain generalised versions of specific --- instantiations of this module. For instance, the module ≡-Reasoning --- in Relation.Binary.PropositionalEquality is recommended for --- equational reasoning when the underlying equality is +-- Module ≡-Reasoning in Relation.Binary.PropositionalEquality +-- is recommended for equational reasoning when the underlying equality is -- Relation.Binary.PropositionalEquality._≡_. open import Relation.Binary diff --git a/src/Relation/Binary/Flip.agda b/src/Relation/Binary/Flip.agda index 9d52c36..79644e5 100644 --- a/src/Relation/Binary/Flip.agda +++ b/src/Relation/Binary/Flip.agda @@ -184,7 +184,6 @@ isStrictTotalOrder {≈ = ≈} {<} sto = record { isEquivalence = isEquivalence Sto.isEquivalence ; trans = transitive < Sto.trans ; compare = trichotomous ≈ < Sto.compare - ; <-resp-≈ = respects₂ < ≈ Sto.Eq.sym Sto.<-resp-≈ } where module Sto = IsStrictTotalOrder sto diff --git a/src/Relation/Binary/List/StrictLex.agda b/src/Relation/Binary/List/StrictLex.agda index f9eaddd..9bf21ad 100644 --- a/src/Relation/Binary/List/StrictLex.agda +++ b/src/Relation/Binary/List/StrictLex.agda @@ -238,7 +238,7 @@ module _ {A : Set} where { isPartialOrder = ≤-isPartialOrder (record { isEquivalence = isEquivalence - ; irrefl = tri⟶irr <-resp-≈ Eq.sym compare + ; irrefl = tri⟶irr compare ; trans = trans ; <-resp-≈ = <-resp-≈ }) @@ -271,7 +271,6 @@ module _ {A : Set} where { isEquivalence = Pointwise.isEquivalence isEquivalence ; trans = transitive isEquivalence <-resp-≈ trans ; compare = <-compare Eq.sym compare - ; <-resp-≈ = respects₂ isEquivalence <-resp-≈ } where open IsStrictTotalOrder sto -- "Packages" (e.g. preorders) can also be handled. diff --git a/src/Relation/Binary/NonStrictToStrict.agda b/src/Relation/Binary/NonStrictToStrict.agda index 73e2eed..cd67ba1 100644 --- a/src/Relation/Binary/NonStrictToStrict.agda +++ b/src/Relation/Binary/NonStrictToStrict.agda @@ -97,7 +97,6 @@ isTotalOrder⟶isStrictTotalOrder dec-≈ tot = record { isEquivalence = TO.isEquivalence ; trans = trans TO.isPartialOrder ; compare = trichotomous TO.Eq.sym dec-≈ TO.antisym TO.total - ; <-resp-≈ = <-resp-≈ TO.isEquivalence TO.≤-resp-≈ } where module TO = IsTotalOrder tot isDecTotalOrder⟶isStrictTotalOrder : diff --git a/src/Relation/Binary/On.agda b/src/Relation/Binary/On.agda index 67180c2..6ec98e5 100644 --- a/src/Relation/Binary/On.agda +++ b/src/Relation/Binary/On.agda @@ -138,7 +138,6 @@ module _ {a b} {A : Set a} {B : Set b} (f : B → A) where { isEquivalence = isEquivalence Sto.isEquivalence ; trans = transitive < Sto.trans ; compare = trichotomous ≈ < Sto.compare - ; <-resp-≈ = respects₂ < ≈ Sto.<-resp-≈ } where module Sto = IsStrictTotalOrder sto diff --git a/src/Relation/Binary/Product/StrictLex.agda b/src/Relation/Binary/Product/StrictLex.agda index 92c2a12..72203be 100644 --- a/src/Relation/Binary/Product/StrictLex.agda +++ b/src/Relation/Binary/Product/StrictLex.agda @@ -243,9 +243,6 @@ module _ {a₁ a₂ ℓ₁ ℓ₂} {A₁ : Set a₁} {A₂ : Set a₂} where {_≤₂_ = _<₂_} (trans spo₂) {x} {y} {z} ; compare = ×-compare (Eq.sym spo₁) (compare spo₁) (compare spo₂) - ; <-resp-≈ = ×-≈-respects₂ (isEquivalence spo₁) - (<-resp-≈ spo₁) - (<-resp-≈ spo₂) } where open IsStrictTotalOrder diff --git a/src/Relation/Binary/Properties/DecTotalOrder.agda b/src/Relation/Binary/Properties/DecTotalOrder.agda index 13673c0..5b25739 100644 --- a/src/Relation/Binary/Properties/DecTotalOrder.agda +++ b/src/Relation/Binary/Properties/DecTotalOrder.agda @@ -19,7 +19,6 @@ strictTotalOrder = record { isEquivalence = isEquivalence ; trans = trans isPartialOrder ; compare = trichotomous Eq.sym _≟_ antisym total - ; <-resp-≈ = <-resp-≈ isEquivalence ≤-resp-≈ } } diff --git a/src/Relation/Binary/PropositionalEquality.agda b/src/Relation/Binary/PropositionalEquality.agda index 1f3a207..4299d70 100644 --- a/src/Relation/Binary/PropositionalEquality.agda +++ b/src/Relation/Binary/PropositionalEquality.agda @@ -175,23 +175,31 @@ inspect f x = [ refl ] ------------------------------------------------------------------------ -- Convenient syntax for equational reasoning -import Relation.Binary.EqReasoning as EqR +-- This is special instance of Relation.Binary.EqReasoning. +-- Rather than instantiating the latter with (setoid A), +-- we reimplement equation chains from scratch +-- since then goals are printed much more readably. --- Relation.Binary.EqReasoning is more convenient to use with _≡_ if --- the combinators take the type argument (a) as a hidden argument, --- instead of being locked to a fixed type at module instantiation --- time. +module ≡-Reasoning {a} {A : Set a} where -module ≡-Reasoning where - module _ {a} {A : Set a} where - open EqR (setoid A) public - hiding (_≡⟨_⟩_) renaming (_≈⟨_⟩_ to _≡⟨_⟩_) + infix 3 _∎ + infixr 2 _≡⟨⟩_ _≡⟨_⟩_ _≅⟨_⟩_ + infix 1 begin_ - infixr 2 _≅⟨_⟩_ + begin_ : ∀{x y : A} → x ≡ y → x ≡ y + begin_ x≡y = x≡y - _≅⟨_⟩_ : ∀ {a} {A : Set a} (x : A) {y z : A} → - x ≅ y → y IsRelatedTo z → x IsRelatedTo z - _ ≅⟨ x≅y ⟩ y≡z = _ ≡⟨ H.≅-to-≡ x≅y ⟩ y≡z + _≡⟨⟩_ : ∀ (x {y} : A) → x ≡ y → x ≡ y + _ ≡⟨⟩ x≡y = x≡y + + _≡⟨_⟩_ : ∀ (x {y z} : A) → x ≡ y → y ≡ z → x ≡ z + _ ≡⟨ x≡y ⟩ y≡z = trans x≡y y≡z + + _≅⟨_⟩_ : ∀ (x {y z} : A) → x ≅ y → y ≡ z → x ≡ z + _ ≅⟨ x≅y ⟩ y≡z = trans (H.≅-to-≡ x≅y) y≡z + + _∎ : ∀ (x : A) → x ≡ x + _∎ _ = refl ------------------------------------------------------------------------ -- Functional extensionality diff --git a/src/Relation/Binary/PropositionalEquality/TrustMe.agda b/src/Relation/Binary/PropositionalEquality/TrustMe.agda index 91801d6..5235862 100644 --- a/src/Relation/Binary/PropositionalEquality/TrustMe.agda +++ b/src/Relation/Binary/PropositionalEquality/TrustMe.agda @@ -8,9 +8,7 @@ module Relation.Binary.PropositionalEquality.TrustMe where open import Relation.Binary.Core using (_≡_) -private - primitive - primTrustMe : ∀ {a} {A : Set a} {x y : A} → x ≡ y +open import Agda.Builtin.TrustMe -- trustMe {x = x} {y = y} evaluates to refl if x and y are -- definitionally equal. diff --git a/src/Relation/Binary/Sum.agda b/src/Relation/Binary/Sum.agda index c754776..ee389b7 100644 --- a/src/Relation/Binary/Sum.agda +++ b/src/Relation/Binary/Sum.agda @@ -321,7 +321,6 @@ module _ {a₁ a₂} {A₁ : Set a₁} {A₂ : Set a₂} where isEquivalence sto₂ ; trans = trans sto₁ ⊎-transitive trans sto₂ ; compare = compare sto₁ ⊎-<-trichotomous compare sto₂ - ; <-resp-≈ = <-resp-≈ sto₁ ⊎-≈-respects₂ <-resp-≈ sto₂ } where open IsStrictTotalOrder diff --git a/src/Size.agda b/src/Size.agda index caf5ead..243c799 100644 --- a/src/Size.agda +++ b/src/Size.agda @@ -6,8 +6,9 @@ module Size where -{-# BUILTIN SIZEUNIV SizeUniv #-} -- sort SizeUniv -{-# BUILTIN SIZE Size #-} -- Size : SizeUniv -{-# BUILTIN SIZELT Size<_ #-} -- Size<_ : Size → SizeUniv -{-# BUILTIN SIZESUC ↑_ #-} -- ↑_ : Size → Size -{-# BUILTIN SIZEINF ∞ #-} -- ∞ : Size +open import Agda.Builtin.Size public + renaming ( SizeU to SizeUniv ) -- sort SizeUniv + using ( Size -- Size : SizeUniv + ; Size<_ -- Size<_ : Size → SizeUniv + ; ↑_ ) -- ↑_ : Size → Size + renaming ( ω to ∞ ) -- ∞ : Size diff --git a/src/index.agda b/src/index.agda new file mode 100644 index 0000000..4acb132 --- /dev/null +++ b/src/index.agda @@ -0,0 +1,9 @@ +module index where + +-- You probably want to start with this module: +import README + +-- For a brief presentation of every single module, head over to +import Everything + +-- Otherwise, here is an exhaustive, stern list of all the available modules: diff --git a/standard-library.agda-lib b/standard-library.agda-lib new file mode 100644 index 0000000..626387c --- /dev/null +++ b/standard-library.agda-lib @@ -0,0 +1,2 @@ +name: standard-library +include: src |