Agda 2.6.2 → 2.6.2.1

raw patch · 140 files changed

+5089/−5041 lines, 140 filesdep ~aesondep ~basedep ~bytestringPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

Dependency ranges changed: aeson, base, bytestring, directory, equivalence, hashable, hashtables, mtl, template-haskell, text, time, transformers

API changes (from Hackage documentation)

Files

• Agda.cabal +69/−79
• CHANGELOG.md +149/−1250
• LICENSE +13/−36
• README.md +0/−1
• doc/release-notes/2.6.2.md +1250/−0
• doc/user-manual.pdf binary
• src/agda-mode/Main.hs +27/−4
• src/data/Agda.css +0/−41
• src/data/JS/agda-rts.js +116/−110
• src/data/JS/biginteger.js +0/−1620
• src/data/JS/highlight-hover.js +0/−32
• src/data/MAlonzo/src/MAlonzo/RTE.hs +0/−3
• src/data/agda.sty +0/−712
• src/data/emacs-mode/agda-input.el +16/−0
• src/data/emacs-mode/agda2-mode-pkg.el +1/−1
• src/data/emacs-mode/agda2-mode.el +3/−3
• src/data/html/Agda.css +41/−0
• src/data/html/highlight-hover.js +32/−0
• src/data/latex/agda.sty +722/−0
• src/data/latex/postprocess-latex.pl +24/−0
• src/data/lib/prim/Agda/Builtin/Cubical/Id.agda +6/−0
• src/data/lib/prim/Agda/Builtin/Cubical/Sub.agda +3/−0
• src/data/lib/prim/Agda/Builtin/Reflection.agda +36/−0
• src/data/lib/prim/Agda/Builtin/Reflection/External.agda +2/−0
• src/data/lib/prim/Agda/Primitive/Cubical.agda +18/−0
• src/data/postprocess-latex.pl +0/−24
• src/full/Agda/Compiler/Common.hs +9/−0
• src/full/Agda/Compiler/JS/Compiler.hs +81/−66
• src/full/Agda/Compiler/MAlonzo/Compiler.hs +433/−172
• src/full/Agda/Compiler/MAlonzo/HaskellTypes.hs +59/−46
• src/full/Agda/Compiler/MAlonzo/Misc.hs +156/−49
• src/full/Agda/Compiler/MAlonzo/Pragmas.hs +16/−18
• src/full/Agda/Compiler/MAlonzo/Pretty.hs +17/−5
• src/full/Agda/Compiler/MAlonzo/Primitives.hs +69/−43
• src/full/Agda/Compiler/MAlonzo/Strict.hs +89/−0
• src/full/Agda/Compiler/ToTreeless.hs +1/−1
• src/full/Agda/Interaction/Base.hs +9/−3
• src/full/Agda/Interaction/BasicOps.hs +2/−2
• src/full/Agda/Interaction/EmacsTop.hs +8/−5
• src/full/Agda/Interaction/FindFile.hs +4/−1
• src/full/Agda/Interaction/Highlighting/FromAbstract.hs +0/−1
• src/full/Agda/Interaction/Highlighting/Generate.hs +1/−0
• src/full/Agda/Interaction/Highlighting/HTML/Base.hs +8/−2
• src/full/Agda/Interaction/Highlighting/JSON.hs +0/−1
• src/full/Agda/Interaction/Highlighting/LaTeX/Base.hs +99/−80
• src/full/Agda/Interaction/Imports.hs +29/−17
• src/full/Agda/Interaction/InteractionTop.hs +1/−1
• src/full/Agda/Interaction/JSON.hs +26/−6
• src/full/Agda/Interaction/JSONTop.hs +3/−3
• src/full/Agda/Interaction/Options/Base.hs +22/−9
• src/full/Agda/Interaction/Options/Warnings.hs +3/−0
• src/full/Agda/Interaction/Response.hs +9/−2
• src/full/Agda/Syntax/Abstract.hs +0/−6
• src/full/Agda/Syntax/Abstract/Name.hs +1/−1
• src/full/Agda/Syntax/Abstract/PatternSynonyms.hs +0/−1
• src/full/Agda/Syntax/Abstract/Views.hs +0/−4
• src/full/Agda/Syntax/Common.hs +44/−1
• src/full/Agda/Syntax/Concrete.hs +1/−1
• src/full/Agda/Syntax/Concrete/Attribute.hs +2/−2
• src/full/Agda/Syntax/Concrete/Definitions.hs +35/−30
• src/full/Agda/Syntax/Concrete/Definitions/Errors.hs +8/−0
• src/full/Agda/Syntax/Concrete/Definitions/Monad.hs +3/−1
• src/full/Agda/Syntax/Concrete/Definitions/Types.hs +24/−11
• src/full/Agda/Syntax/Concrete/Operators.hs +2/−2
• src/full/Agda/Syntax/Concrete/Pattern.hs +1/−1
• src/full/Agda/Syntax/Parser.hs +1/−1
• src/full/Agda/Syntax/Parser/LexActions.hs +1/−1
• src/full/Agda/Syntax/Parser/Lexer.x +38/−38
• src/full/Agda/Syntax/Parser/Literate.hs +30/−56
• src/full/Agda/Syntax/Parser/LookAhead.hs +46/−14
• src/full/Agda/Syntax/Parser/Parser.y +6/−8
• src/full/Agda/Syntax/Scope/Base.hs +1/−1
• src/full/Agda/Syntax/Translation/AbstractToConcrete.hs +2/−8
• src/full/Agda/Syntax/Translation/ConcreteToAbstract.hs +2/−6
• src/full/Agda/Syntax/Translation/InternalToAbstract.hs +0/−1
• src/full/Agda/Termination/RecCheck.hs +1/−1
• src/full/Agda/Termination/TermCheck.hs +1/−1
• src/full/Agda/TypeChecking/Abstract.hs +1/−1
• src/full/Agda/TypeChecking/CompiledClause/Match.hs +6/−1
• src/full/Agda/TypeChecking/Coverage.hs +4/−3
• src/full/Agda/TypeChecking/Errors.hs +5/−1
• src/full/Agda/TypeChecking/Errors.hs-boot +2/−1
• src/full/Agda/TypeChecking/Free.hs +8/−8
• src/full/Agda/TypeChecking/Generalize.hs +10/−10
• src/full/Agda/TypeChecking/IApplyConfluence.hs +7/−5
• src/full/Agda/TypeChecking/Implicit.hs +1/−1
• src/full/Agda/TypeChecking/Lock.hs +32/−21
• src/full/Agda/TypeChecking/MetaVars.hs +131/−19
• src/full/Agda/TypeChecking/MetaVars/Occurs.hs +21/−4
• src/full/Agda/TypeChecking/Monad/Base.hs +11/−7
• src/full/Agda/TypeChecking/Monad/Debug.hs-boot +5/−0
• src/full/Agda/TypeChecking/Monad/Options.hs +12/−0
• src/full/Agda/TypeChecking/Monad/Signature.hs +60/−2
• src/full/Agda/TypeChecking/Names.hs +2/−2
• src/full/Agda/TypeChecking/Positivity/Occurrence.hs +1/−1
• src/full/Agda/TypeChecking/Primitive.hs +1/−1
• src/full/Agda/TypeChecking/Primitive/Cubical.hs +40/−27
• src/full/Agda/TypeChecking/RecordPatterns.hs +1/−1
• src/full/Agda/TypeChecking/Records.hs +22/−13
• src/full/Agda/TypeChecking/Reduce.hs +16/−1
• src/full/Agda/TypeChecking/Reduce/Fast.hs +2/−0
• src/full/Agda/TypeChecking/Rewriting/NonLinMatch.hs +19/−6
• src/full/Agda/TypeChecking/Rewriting/NonLinPattern.hs +9/−2
• src/full/Agda/TypeChecking/Rules/Application.hs +22/−15
• src/full/Agda/TypeChecking/Rules/Builtin.hs +25/−23
• src/full/Agda/TypeChecking/Rules/Builtin/Coinduction.hs +7/−6
• src/full/Agda/TypeChecking/Rules/Data.hs +16/−13
• src/full/Agda/TypeChecking/Rules/Decl.hs +5/−4
• src/full/Agda/TypeChecking/Rules/Def.hs +35/−10
• src/full/Agda/TypeChecking/Rules/LHS.hs +16/−8
• src/full/Agda/TypeChecking/Rules/LHS/Unify.hs +6/−4
• src/full/Agda/TypeChecking/Rules/Record.hs +5/−5
• src/full/Agda/TypeChecking/Rules/Term.hs +12/−6
• src/full/Agda/TypeChecking/Serialise.hs +5/−3
• src/full/Agda/TypeChecking/Serialise/Instances/Common.hs +26/−6
• src/full/Agda/TypeChecking/Serialise/Instances/Errors.hs +2/−0
• src/full/Agda/TypeChecking/Serialise/Instances/Internal.hs +1/−1
• src/full/Agda/TypeChecking/SizedTypes/Syntax.hs +4/−1
• src/full/Agda/TypeChecking/SizedTypes/WarshallSolver.hs +9/−8
• src/full/Agda/TypeChecking/Sort.hs +4/−2
• src/full/Agda/TypeChecking/Substitute.hs +5/−4
• src/full/Agda/TypeChecking/Unquote.hs +5/−8
• src/full/Agda/Utils/Graph/AdjacencyMap/Unidirectional.hs +230/−8
• src/full/Agda/Utils/Haskell/Syntax.hs +4/−0
• src/full/Agda/Utils/List.hs +61/−16
• src/full/Agda/Utils/List1.hs +16/−5
• src/full/Agda/Utils/List1.hs-boot +5/−0
• src/full/Agda/Utils/Map.hs +5/−4
• src/full/Agda/Utils/Null.hs +7/−1
• src/full/Agda/Utils/Three.hs +0/−8
• src/full/Agda/Utils/Warshall.hs +3/−1
• stack-8.0.2.yaml +8/−0
• stack-8.10.5.yaml +0/−3
• stack-8.10.7.yaml +7/−0
• stack-8.2.2.yaml +7/−0
• stack-8.4.4.yaml +6/−0
• stack-8.6.5.yaml +5/−0
• stack-8.8.4.yaml +5/−0
• stack-9.0.1.yaml +13/−84
• stack-9.2.1.yaml +136/−0

@@ -1,12 +1,12 @@ name:            Agda-version:         2.6.2+version:         2.6.2.1 cabal-version:   >= 1.10 build-type:      Custom license:         OtherLicense license-file:    LICENSE copyright:       (c) 2005-2021 The Agda Team. author:          Ulf Norell and The Agda Team, see https://agda.readthedocs.io/en/latest/team.html-maintainer:      Ulf Norell <ulfn@chalmers.se>+maintainer:      The Agda Team homepage:        http://wiki.portal.chalmers.se/agda/ bug-reports:     https://github.com/agda/agda/issues category:        Dependent types@@ -39,11 +39,13 @@                     GHC == 8.4.4                     GHC == 8.6.5                     GHC == 8.8.4-                    GHC == 8.10.5+                    GHC == 8.10.7                     GHC == 9.0.1+                    GHC == 9.2.1  extra-source-files: CHANGELOG.md                     README.md+                    doc/release-notes/2.6.2.md                     doc/release-notes/2.6.1.3.md                     doc/release-notes/2.6.1.2.md                     doc/release-notes/2.6.1.1.md@@ -77,22 +79,24 @@                     doc/release-notes/2.2.2.md                     doc/release-notes/2.2.4.md                     doc/release-notes/2.2.0.md-                    doc/user-manual.pdf+-- Liang-Ting (2019-11-26): See Issues #4216+--                    doc/user-manual.pdf                     stack-8.0.2.yaml                     stack-8.2.2.yaml                     stack-8.4.4.yaml                     stack-8.6.5.yaml                     stack-8.8.4.yaml-                    stack-8.10.5.yaml+                    stack-8.10.7.yaml                     stack-9.0.1.yaml+                    stack-9.2.1.yaml  data-dir:           src/data-data-files:         Agda.css-                    agda.sty-                    emacs-mode/*.el+data-files:         emacs-mode/*.el+                    html/Agda.css+                    html/highlight-hover.js                     JS/agda-rts.js-                    JS/biginteger.js-                    JS/highlight-hover.js+                    latex/agda.sty+                    latex/postprocess-latex.pl                     lib/prim/Agda/Builtin/Bool.agda                     lib/prim/Agda/Builtin/Char.agda                     lib/prim/Agda/Builtin/Char/Properties.agda@@ -131,7 +135,6 @@                     lib/prim/Agda/Primitive/Cubical.agda                     MAlonzo/src/MAlonzo/*.hs                     MAlonzo/src/MAlonzo/RTE/*.hs-                    postprocess-latex.pl  source-repository head   type:     git@@ -140,7 +143,7 @@ source-repository this   type:     git   location: https://github.com/agda/agda.git-  tag:      v2.6.2+  tag:      v2.6.2.1  flag cpphs   default:     False@@ -165,9 +168,9 @@     Enable some expensive optimisations when compiling Agda.  custom-setup-  setup-depends:  base >= 4.9.0.0 && < 4.16-                , Cabal >= 1.24.0.0 && < 3.5-                , directory >= 1.2.6.1.2 && < 1.4+  setup-depends:  base >= 4.9.0.0 && < 4.17+                , Cabal >= 1.24.0.0 && < 3.7+                , directory >= 1.2.6.2 && < 1.4                 , filepath >= 1.4.1.0 && < 1.5                 , process >= 1.4.2.0 && < 1.7 @@ -201,10 +204,10 @@   if os(windows) && impl(ghc == 8.6.3)     buildable: False -  build-depends:  aeson >= 1.1.2.0 && < 1.6+  build-depends:  aeson >= 1.1.2.0 && < 2.1                 , array >= 0.5.1.1 && < 0.6                 , async >= 2.2 && < 2.3-                , base >= 4.9.0.0 && < 4.16+                , base >= 4.9.0.0 && < 4.17                 , binary >= 0.8.3.0 && < 0.9                 , blaze-html >= 0.8 && < 0.10                 , boxes >= 0.1.3 && < 0.2@@ -224,13 +227,13 @@                 -- hashable 1.2.0.10 makes library-test 10x                 -- slower. The issue was fixed in hashable 1.2.1.0.                 -- https://github.com/tibbe/hashable/issues/57.-                , hashable >= 1.2.1.0 && < 1.4+                , hashable >= 1.2.1.0 && < 1.5                 -- There is a "serious bug"                 -- (https://hackage.haskell.org/package/hashtables-1.2.0.2/changelog)                 -- in hashtables 1.2.0.0/1.2.0.1. This bug seems to                 -- have made Agda much slower (infinitely slower?) in                 -- some cases.-                , hashtables >= 1.2.0.2 && < 1.3+                , hashtables >= 1.2.0.2 && < 1.4                 , haskeline >= 0.7.2.3 && < 0.9                 -- monad-control-1.0.1.0 is the first to contain liftThrough                 , monad-control >= 1.0.1.0 && < 1.1@@ -247,10 +250,10 @@                 , split >= 0.2.0.0 && < 0.2.4                 , stm >= 2.4.4 && < 2.6                 , strict >= 0.3.2 && < 0.5-                , template-haskell >= 2.11.0.0 && < 2.18+                , template-haskell >= 2.11.0.0 && < 2.19                 , text >= 1.2.3.0 && < 1.3-                , time >= 1.6.0.1 && < 1.12-                , transformers == 0.5.*+                , time >= 1.6.0.1 && < 1.13+                , transformers >= 0.5 && < 0.7                 , unordered-containers >= 0.2.5.0 && < 0.3                 , uri-encode >= 1.5.0.4 && < 1.6                 , zlib == 0.6.*@@ -264,21 +267,6 @@   -- revisions on hackage, e.g. relaxing upper bounds.  This process   -- currently does not support revising conditionals. -  -- In hs-tags the mtl library must be compiled with the version of-  -- transformers shipped with GHC, so we use that version in Agda (see,-  -- for example, Issue #2983).-  if impl(ghc > 9.0.1)-    build-depends: transformers >= 0.5.6.2--  if impl(ghc >= 8.6.4) && impl(ghc <= 9.0.1)-    build-depends: transformers == 0.5.6.2--  if impl(ghc >= 8.4) && impl(ghc < 8.6.4)-    build-depends: transformers == 0.5.5.0--  if impl(ghc < 8.4)-    build-depends: transformers == 0.5.2.0-   -- ASR (2018-10-16).   -- text-1.2.3.0 required for supporting GHC 8.4.1, 8.4.2 and   -- 8.4.3. See Issue #3277.@@ -320,6 +308,7 @@                     Agda.Compiler.MAlonzo.Pragmas                     Agda.Compiler.MAlonzo.Pretty                     Agda.Compiler.MAlonzo.Primitives+                    Agda.Compiler.MAlonzo.Strict                     Agda.Compiler.ToTreeless                     Agda.Compiler.Treeless.AsPatterns                     Agda.Compiler.Treeless.Builtin@@ -659,6 +648,7 @@     ghc-options: -fprint-potential-instances                  -- Initially, we disable all the warnings.                  -w+                 -Wwarn                  -- This option must be the first one after disabling the                  -- warnings. See Issue #2094.                  -Wunrecognised-warning-flags@@ -691,34 +681,34 @@                  -Wwrong-do-bind   else     ghc-options: -fprint-potential-instances-                 -Werror=unrecognised-warning-flags-                 -Werror=deprecated-flags-                 -Werror=deriving-typeable-                 -Werror=dodgy-exports-                 -Werror=dodgy-foreign-imports-                 -Werror=dodgy-imports-                 -Werror=duplicate-exports-                 -Werror=empty-enumerations-                 -Werror=identities-                 -Werror=incomplete-patterns-                 -Werror=inline-rule-shadowing-                 -Werror=missing-fields-                 -Werror=missing-methods-                 -Werror=missing-pattern-synonym-signatures-                 -Werror=missing-signatures-                 -Werror=noncanonical-monad-instances-                 -Werror=noncanonical-monoid-instances-                 -Werror=overflowed-literals-                 -Werror=overlapping-patterns-                 -Werror=semigroup-                 -Werror=tabs-                 -Werror=typed-holes-                 -Werror=unrecognised-pragmas-                 -Werror=unticked-promoted-constructors-                 -Werror=unused-do-bind-                 -Werror=unused-foralls-                 -Werror=warnings-deprecations-                 -Werror=wrong-do-bind+                 -Wwarn=unrecognised-warning-flags+                 -Wwarn=deprecated-flags+                 -Wwarn=deriving-typeable+                 -Wwarn=dodgy-exports+                 -Wwarn=dodgy-foreign-imports+                 -Wwarn=dodgy-imports+                 -Wwarn=duplicate-exports+                 -Wwarn=empty-enumerations+                 -Wwarn=identities+                 -Wwarn=incomplete-patterns+                 -Wwarn=inline-rule-shadowing+                 -Wwarn=missing-fields+                 -Wwarn=missing-methods+                 -Wwarn=missing-pattern-synonym-signatures+                 -Wwarn=missing-signatures+                 -Wwarn=noncanonical-monad-instances+                 -Wwarn=noncanonical-monoid-instances+                 -Wwarn=overflowed-literals+                 -Wwarn=overlapping-patterns+                 -Wwarn=semigroup+                 -Wwarn=tabs+                 -Wwarn=typed-holes+                 -Wwarn=unrecognised-pragmas+                 -Wwarn=unticked-promoted-constructors+                 -Wwarn=unused-do-bind+                 -Wwarn=unused-foralls+                 -Wwarn=warnings-deprecations+                 -Wwarn=wrong-do-bind    -- NOTE: If adding or removing flags, also change `.ghci-8.2`   if impl(ghc >= 8.2)@@ -726,33 +716,33 @@                  -- ASR TODO (2017-07-23): `make haddock` fails when                  -- this flag is on.                  -- -Wmissing-home-modules-                 -Werror=simplifiable-class-constraints-                 -Werror=unbanged-strict-patterns+                 -Wwarn=simplifiable-class-constraints+                 -Wwarn=unbanged-strict-patterns    -- NOTE: If adding or removing flags, also change `.ghci-8.6`   if impl(ghc >= 8.6)-    ghc-options: -Werror=inaccessible-code-                 -Werror=star-binder-                 -Werror=star-is-type+    ghc-options: -Wwarn=inaccessible-code+                 -Wwarn=star-binder+                 -Wwarn=star-is-type    -- The following warning is an error in GHC >= 8.10.   if impl(ghc >= 8.6) && impl(ghc < 8.10)-    ghc-options: -Werror=implicit-kind-vars+    ghc-options: -Wwarn=implicit-kind-vars    -- NOTE: If adding or removing flags, also change `.ghci-8.8`   if impl(ghc >= 8.8)-    ghc-options: -Werror=missed-extra-shared-lib+    ghc-options: -Wwarn=missed-extra-shared-lib    -- NOTE: If adding or removing flags, also change `.ghci-8.10`   if impl(ghc >= 8.10)-    ghc-options: -Werror=deriving-defaults-                 -Werror=redundant-record-wildcards-                 -Werror=unused-packages-                 -Werror=unused-record-wildcards+    ghc-options: -Wwarn=deriving-defaults+                 -Wwarn=redundant-record-wildcards+                 -Wwarn=unused-packages+                 -Wwarn=unused-record-wildcards    -- NOTE: If adding or removing flags, also change `.ghci-9.0`   if impl(ghc >= 9.0)-    ghc-options: -Werror=invalid-haddock+    ghc-options: -Wwarn=invalid-haddock    default-language: Haskell2010 @@ -822,8 +812,8 @@   hs-source-dirs:   src/agda-mode   main-is:          Main.hs   other-modules:    Paths_Agda-  build-depends:    base >= 4.9.0.0 && < 4.16-                  , directory >= 1.2.6.1.2 && < 1.4+  build-depends:    base >= 4.9.0.0 && < 4.17+                  , directory >= 1.2.6.2 && < 1.4                   , filepath >= 1.4.1.0 && < 1.5                   , process >= 1.4.2.0 && < 1.7   default-language: Haskell2010

@@ -1,1250 +1,149 @@-Release notes for Agda version 2.6.2-====================================--Highlights-------------* Several improvements and bug-fixes related to [Run-time-  Irrelevance](https://agda.readthedocs.io/en/v2.6.2/language/runtime-irrelevance.html).--* Several improvements and bug-fixes related to the [JavaScript-  Backend](https://agda.readthedocs.io/en/v2.6.2/tools/compilers.html#javascript-backend).--* Added experimental support for [Guarded Cubical-  Agda](https://agda.readthedocs.io/en/v2.6.2/language/guarded-cubical.html).--* The [Primitive-  Sorts](https://agda.readthedocs.io/en/v2.6.2/language/built-ins.html#sorts)-  of Agda (`Set` and `Prop`) are no longer keywords and can be renamed-  when importing `Agda.Primitive`.--* Added native support for the [Inspect-  Idiom](https://agda.readthedocs.io/en/v2.6.2/language/with-abstraction.html#with-abstraction-equality).--* Added support for making [System-  Calls](https://agda.readthedocs.io/en/v2.6.2/language/reflection.html#system-calls)-  from the reflection API.--Installation and infrastructure----------------------------------* Added support for GHC 8.10.5 and 9.0.1.--* Some expensive optimisations are now off by default-  (see [#4521](https://github.com/agda/agda/issues/4521)).--  These optimisations can in some cases make Agda substantially-  faster, but they can also make the compilation of the Agda program-  take more time and space.--  The optimisations can be turned on manually (Cabal:-  `-foptimise-heavily`, Stack: `--flag Agda:optimise-heavily`). They-  are turned on (by default) when Agda is installed using `make-  install`.--  If the optimisations are turned on it might make sense to limit-  GHC's memory usage (using something like `--ghc-options="+RTS -M6G-  -RTS"`).--Pragmas and options----------------------* New option `--auto-inline` turns on automatic compile-time inlining-  of simple functions. This was previously enabled by default.--  Note that the absence of automatic inlining can make typechecking-  substantially slower.--  The new default has repercussions on termination checking, for instance-  (see [#4702](https://github.com/agda/agda/issues/4702)).-  The following formulation of `plus` termination checks with `--auto-inline`-  but not without:-  ```agda-  open import Agda.Builtin.Nat--  case_of_ : {A B : Set} → A → (A → B) → B-  case x of f = f x--  plus : Nat → Nat → Nat-  plus m n = case m of λ-     { zero    → n-     ; (suc m) → suc (plus m n)-     }-  ```-  In this particular case, we can work around the limitation of the-  termination checker with pragma `{-# INLINE case_of_ #-}`.--* New options `--qualified-instances` (default) and-  `--no-qualified-instances`. When `--no-qualified-instances` is-  enabled, Agda will only consider candidates for instance search that-  are in scope under an unqualified name (see-  [#4522](https://github.com/agda/agda/pull/4522)).--* New option `--call-by-name` turns off call-by-need evaluation at type-  checking time.--* New option `--highlight-occurrences` (off by default) enables the HTML-  backend to include a JavaScript file that highlights all occurrences of-  the mouse-hovered symbol (see-  [#4535](https://github.com/agda/agda/pull/4535)).--* New option `--no-import-sorts` disables the implicit `open-  import Agda.Primitive using (Set; Prop)` at the top of each file-  (see below).--* New option `--local-confluence-check` to restore the old behaviour-  of the `--confluence-check` flag (see below for the new behaviour).--* New primitive `primStringFromListInjective` internalising the fact that-  `primStringFromList` is an injective function. It is bound in-  `Agda.Builtin.String.Properties`.--* New option `--allow-exec` enables the use of system calls during-  type checking using the `AGDATCMEXECTC` builtin.--* New option `--show-identity-substitutions` shows all arguments of-  metavariables when pretty-printing a term, even if they amount to-  just applying all the variables in the context.--* The option `--rewriting` is now considered infective: if a module has-  `--rewriting` enabled, then all modules importing it must also have-  `--rewriting` enabled.--* New option `--no-double-check` (default), opposite of the existing-  `--double-check`.--* Due to several known soundness issues with sized types (see-  [#1201](https://github.com/agda/agda/issues/1201),-  [#1946](https://github.com/agda/agda/issues/1946),-  [#2820](https://github.com/agda/agda/issues/2820),-  [#3026](https://github.com/agda/agda/issues/3026)), the-  `--sized-types` flag can no longer be used while `--safe` is active.--* New option `--guarded` turns on the Guarded Cubical extension of Agda.--  See [Guarded Cubical](https://agda.readthedocs.io/en/v2.6.2/language/guarded-cubical.html)-  in the documentation for more.--* The flags `--guardedness` and `--sized-types` are no longer enabled-  by default.--Command-line interaction---------------------------* In the previous release, Agda exited with either status 0 when the-  program type checks successfully, or status 1 when encountering any-  kind of error.  Now Agda exits with status 42 for type errors, 71-  for errors in the commandline arguments, and 154 for impossible-  errors. Exit status 1 may be returned under other circumstances; for-  instance, an incomplete pattern matching, or an error generated by-  the Haskell runtime.  See PR-  [#4540](https://github.com/agda/agda/pull/4540).--Lexical syntax-----------------* Layout handling has been improved so that block starters can be-  stacked on the same line-  [#1145](https://github.com/agda/agda/issues/1145).--  If several layout blocks are started by layout keywords without line-  break in between (where line breaks inside block comments do not-  count), then those blocks indented *more* than the last block go-  passive, meaning they cannot be further extended by new statements.-  ```agda-    private module M where postulate-              A : Set                 -- module-block goes passive-              B : Set                 -- postulate-block can still be extended-            module N where            -- private-block can still be extended-  ```-  Previously, this was a parse error.--Language-----------* Inductive records without η-equality no longer support both matching-  on the record constructor and construction of record elements by-  copattern matching.  It has been discovered that the combination of-  both leads to loss of subject reduction, i.e., reduction does not-  preserve typing.  See issue-  [#4560](https://github.com/agda/agda/issues/4560).--  η-equality for a record can be turned off manually with directive-  `no-eta-equality` or command-line option `--no-eta-equality`, but it-  is also automatically turned off for some recursive records.  For-  records without η, matching on the record constructor is now off by-  default and construction by copattern matching is on.  If you want-  the converse, you can add the new record directive `pattern`.--  Example with record pattern:-  ```agda-  record N : Set where-    inductive-    no-eta-equality-    pattern-    field out : Maybe N--  pred : N → Maybe N-  pred record{ out = m } = m-  ```-  Example with record constructor and use of `;` instead of newline:-  ```agda-  record N : Set where-    inductive; no-eta-equality-    pattern; constructor inn-    field out : Maybe N--  pred : N → Maybe N-  pred (inn m) = m-  ```--* `Set` and `Prop` are no longer keywords but are now primitives-  defined in the module `Agda.Primitive`. They can be renamed when-  importing this module, for example:--  ```agda-  open import Agda.Primitive renaming (Set to Type)--  test : Type₁-  test = Type-  ```--  To preserve backwards compatibility, each top-level Agda module now-  starts with an implicit statement:--  ```agda-  open import Agda.Primitive using (Set; Prop)-  ```--  This implicit import can be disabled with the-  `--no-import-sorts` flag.--* Agda now has support for sorts `Setωᵢ` (alternative syntax: `Setωi`)-  for natural numbers `i`, where `Setω₀ = Setω`. These sorts form a-  second hierarchy `Setωᵢ : Setωᵢ₊₁` similar to the standard hierarchy-  of `Setᵢ`, but do not support universe polymorphism. It should not-  be necessary to refer to these sorts during normal usage of Agda,-  but they might be useful for defining reflection-based macros (see-  [#2119](https://github.com/agda/agda/issues/2119) and-  [#4585](https://github.com/agda/agda/issues/4585)).--* Changed the internal representation of literal strings: instead of using a-  linked list of characters (`String`), we are now using `Data.Text`. This-  should be a transparent change from the user's point of view: the backend-  was already packing these strings as text.--  Used this opportunity to introduce a `primStringUncons` primitive in-  `Agda.Builtin.String` (and to correspondingly add the-  `Agda.Builtin.Maybe` it needs).--* The option `--confluence-check` for rewrite rules has been given a-  new implementation that checks global confluence instead of local-  confluence. Concretely, it does so by enforcing two properties:--  1. For any two left-hand sides of the rewrite rules that overlap-     (either at the root position or at a subterm), the most general-     unifier of the two left-hand sides is again a left-hand side of a-     rewrite rule. For example, if there are two rules `suc m + n =-     suc (m + n)` and `m + suc n = suc (m + n)`, then there should-     also be a rule `suc m + suc n = suc (suc (m + n))`.--  2. Each rewrite rule should satisfy the *triangle property*: For any-     rewrite rule `u = w` and any single-step parallel unfolding `u =>-     v`, we should have another single-step parallel unfolding `v =>-     w`.--  The previous behaviour of the confluence checker that only ensures-  local confluence can be restored by using the-  `--local-confluence-check` flag.--* Binary integer literals with prefix `0b` (for instance,-  `0b11001001`) are now supported.--* Overloaded literals now require the conversion function (`fromNat`,-  `fromNeg`, or `fromString`) to be in scope *unqualified* to take-  effect.--  Previously, it was enough for the function to be in scope at all,-  which meant you couldn't import the corresponding builtin module-  without having overloaded literals turned on.--* Added `interleaved mutual` blocks where users can forward-declare-  function, record, and data types and interleave their-  definitions. These blocks are elaborated to more traditional mutual-  blocks by:--    - leaving the signatures where they are-    - grouping the clauses for a function together with the first of them-    - grouping the constructors for a datatype together with the first of them--  Example: two interleaved function definitions--  ```agda--  interleaved mutual--    -- Declarations:-    even : Nat → Bool-    odd  : Nat → Bool--    -- zero is even, not odd-    even zero = true-    odd  zero = false--    -- suc case: switch evenness on the predecessor-    even (suc n) = odd n-    odd  (suc n) = even n-  ```--  Other example: the definition of universe of types closed under the-  natural numbers and pairing:--  ```agda--  interleaved mutual--    -- Declaration of a product record, a universe of codes, and a decoding function-    record _×_ (A B : Set) : Set-    data U : Set-    El : U → Set--    -- We have a code for the type of natural numbers in our universe-    constructor `Nat : U-    El `Nat = Nat--    -- Btw we know how to pair values in a record-    record _×_ A B where-      constructor _,_-      inductive-      field fst : A; snd : B--    -- And we have a code for pairs in our universe-    constructor _`×_ : (A B : U) → U-    El (A `× B) = El A × El B-  ```--* Erased constructors (see-  [#4638](https://github.com/agda/agda/issues/4638)).--  Constructors can be marked as erased. Example:-  ```agda-    {-# OPTIONS --cubical --safe #-}--    open import Agda.Builtin.Cubical.Path-    open import Agda.Primitive--    private-      variable-        a   : Level-        A B : Set a--    Is-proposition : Set a → Set a-    Is-proposition A = (x y : A) → x ≡ y--    data ∥_∥ (A : Set a) : Set a where-      ∣_∣        : A → ∥ A ∥-      @0 trivial : Is-proposition ∥ A ∥--    rec : @0 Is-proposition B → (A → B) → ∥ A ∥ → B-    rec p f ∣ x ∣           = f x-    rec p f (trivial x y i) = p (rec p f x) (rec p f y) i-  ```-  In the code above the constructor `trivial` is only available at-  compile-time, whereas `∣_∣` is also available at run-time. Erased-  names can be used in bodies of clauses that match on `trivial`, if-  the match is done in a non-erased position, like in the final clause-  of `rec`. (Note that Cubical Agda programs still cannot be-  compiled.)--* Erased pattern-matching lambdas (see-  [#4525](https://github.com/agda/agda/issues/4525)).--  Regular pattern-matching lambdas are treated as non-erased-  function definitions. One can make a pattern-matching lambda erased-  by writing `@0` or `@erased` after the lambda:-  ```agda-  @0 _ : @0 Set → Set-  _ = λ @0 { A → A }--  @0 _ : @0 Set → Set-  _ = λ @erased where-    A → A-  ```--  The reflection machinery currently does not support erased-  pattern-matching lambdas (they are quoted as regular-  pattern-matching lambdas).--* New (?) rule for modalities of generalised variables-  (see [#5058](https://github.com/agda/agda/issues/5058)).--  The new rule is that generalisable variables get the modality that-  they are declared with, whereas other variables always get the-  default modality. (It is unclear what the old rule was, perhaps-  nothing was changed.)--* Private abstract type signatures can no longer see through abstract-  (see [#418](https://github.com/agda/agda/issues/418)).--  This means that abstract definitions no longer evaluate in *any*-  type signatures in the same module. Previously they evaluated in-  type signatures of definitions that were both private and abstract.--  It also means that metavariables in type signatures have to be-  solved locally, and cannot make use of information in the definition-  body, and that constructors of abstract datatypes are not in scope-  in type signatures.--* Type inference is disabled for abstract definitions (see-  [#418](https://github.com/agda/agda/issues/418)).--  This means that abstract definitions (inluding functions defined in-  `where` blocks of abstract definitions) need complete type-  signatures.--* One can now declare syntax with two name parts without any hole in-  between, and syntax without any holes.--  Examples:-  ```agda-  syntax Σ A (λ x → B) = [ x ∶ A ] × B-  syntax []            = [ ]-  ```--* Internalised the *inspect idiom* that allows users to abstract over-  an expression in a ``with`` clause while, at the same time,-  remembering the origin of the abstracted pattern via an equation.--  In the following example, abstracting over and then matching on the-  result of ``p x`` allows the first call to ``filter p (x ∷ xs)`` to-  reduce.--  In case the element ``x`` is kept, the second call to ``filter`` on-  the LHS then performs the same ``p x`` test. Because we have-  retained the proof that ``p x ≡ true`` in ``eq``, we are able to-  rewrite by this equality and get it to reduce too.--  This leads to just enough computation that we can finish the proof-  with an appeal to congruence and the induction hypothesis.--  ```agda-  filter-filter : ∀ p xs → filter p (filter p xs) ≡ filter p xs-  filter-filter p []       = refl-  filter-filter p (x ∷ xs) with p x in eq-  ... | false = filter-filter p xs -- easy-  ... | true -- second filter stuck on `p x`: rewrite by `eq`!-    rewrite eq = cong (x ∷_) (filter-filter p xs)-  ```--* As a consequence of the above extensions to `with`, lambdas and lets-  now need parentheses when appearing in a `with`. For instance,--  ```agda-  with-on-fun : Nat → Nat-  with-on-fun n with (λ m → m + n)  -- parentheses required!-  ... | f = f n-  ```--* It is now possible to add hiding and relevance annotations to `with`-  expressions. For example:--  ```agda-  module _ (A B : Set) (recompute : .B → .{{A}} → B) where--    _$_ : .(A → B) → .A → B-    f $ x with .{f} | .(f x) | .{{x}}-    ... | y = recompute y-  ```--Builtins------------ Primitive operations for floating-point numbers changed. The equalities now-  follow IEEE 754 equality, after unifying all NaNs. Primitive inequality was-  added:-  ```agda-  primFloatEquality   : Float -> Float -> Bool -- from primFloatNumericEquality-  primFloatLess       : Float -> Float -> Bool -- from primFloatNumericLess-  primFloatInequality : Float -> Float -> Bool -- new-  ```-  The “numeric” relations are now deprecated.--  There are several new predicates on floating-point numbers:-  ```agda-  primFloatIsInfinite     : Float -> Bool -- new-  primFloatIsNaN          : Float -> Bool -- new-  primFloatIsSafeInteger  : Float -> Bool -- new-  ```-  The `primFloatIsSafeInteger` function determines whether the value is a number-  that is a safe integer, i.e., is within the range where the arithmetic-  operations do not lose precision.--  The operations for conversion to integers (`primRound`, `primFloor`,-  and `primCeiling`) were renamed for consistency, and return a value-  of type `Maybe Int`, returning `nothing` for NaN and the infinities:-  ```agda-  primFloatRound   : Float → Maybe Int -- from primRound-  primFloatFloor   : Float → Maybe Int -- from primFloor-  primFloatCeiling : Float → Maybe Int -- from primCeiling-  ```--  There are several new conversions:-  ```agda-  primIntToFloat    : Int -> Float               -- new-  primFloatToRatio  : Float -> (Int × Nat)       -- new-  primRatioToFloat  : Int -> Nat -> Float        -- new-  primFloatDecode   : Float -> Maybe (Int × Int) -- new-  primFloatEncode   : Int -> Int -> Maybe Float  -- new-  ```-  The `primFloatDecode` function decodes a floating-point number f to a mantissa-  and exponent, such that `f = mantissa * 2 ^ exponent`, normalised such that-  the mantissa is the smallest possible number. The `primFloatEncode` function-  encodes a pair of a mantissa and exponent to a floating-point number.--  There are several new operations:-  ```agda-  primFloatPow        : Float -> Float -> Float -- new-  primFloatATan2      : Float -> Float -> Float -- from primATan2-  primFloatSinh       : Float -> Float          -- new-  primFloatCosh       : Float -> Float          -- new-  primFloatTanh       : Float -> Float          -- new-  primFloatASinh      : Float -> Float          -- new-  primFloatACosh      : Float -> Float          -- new-  primFloatATanh      : Float -> Float          -- new-  ```-  Furthermore, the following operations were renamed for consistency:-  ```agda-  primFloatExp        : Float -> Float          -- from primExp-  primFloatSin        : Float -> Float          -- from primSin-  primFloatLog        : Float -> Float          -- from primLog-  primFloatCos        : Float -> Float          -- from primCos-  primFloatTan        : Float -> Float          -- from primTan-  primFloatASin       : Float -> Float          -- from primASin-  primFloatACos       : Float -> Float          -- from primACos-  primFloatATan       : Float -> Float          -- from primATan-  ```--  All of these operations are implemented on the JavaScript backend.--- `primNatToChar` maps surrogate code points to the replacement character-  `'U+FFFD` and surrogate code points are disallowed in character literals--  [Surrogate code points](https://www.unicode.org/glossary/#surrogate_code_point)-  are characters in the range `U+D800` to `U+DFFF` and are reserved for use by-  UTF-16.--  The reason for this change is that strings are represented (at type-checking-  time and in the GHC backend) by Data.Text byte strings, which cannot-  represent surrogate code points and replaces them by `U+FFFD`. By doing the-  same for characters we can have `primStringFromList` be injective (witnessed-  by `Agda.Builtin.String.Properties.primStringFromListInjective`).---Reflection-------------- New operation in `TC` monad, similar to `quoteTC` but operating on-  types in `Setω`-  ```agda-  quoteωTC : ∀ {A : Setω} → A → TC Term-  ```-- `typeError` and `debugPrint` no longer inserts spaces around `termErr` and-  `nameErr` parts. They also do a better job of respecting line breaks in-  `strErr` parts.--- The reflection machinery now supports quantities in `Arg` (see-  [#5317](https://github.com/agda/agda/issues/5317)). The `ArgInfo`-  type has changed, and there are new types `Modality` and `Quantity`:-  ```agda-  data Quantity : Set where-    quantity-0 quantity-ω : Quantity--  {-# BUILTIN QUANTITY   Quantity   #-}-  {-# BUILTIN QUANTITY-0 quantity-0 #-}-  {-# BUILTIN QUANTITY-ω quantity-ω #-}--  data Modality : Set where-    modality : (r : Relevance) (q : Quantity) → Modality--  {-# BUILTIN MODALITY             Modality #-}-  {-# BUILTIN MODALITY-CONSTRUCTOR modality #-}--  data ArgInfo : Set where-    arg-info : (v : Visibility) (m : Modality) → ArgInfo-  ```--- The representation of reflected patterns and clauses has-  changed. Each clause now includes a telescope with the names and-  types of the pattern variables.--  ```agda-  data Clause where-    clause        : (tel : List (Σ String λ _ → Arg Type)) (ps : List (Arg Pattern)) (t : Term) → Clause-    absurd-clause : (tel : List (Σ String λ _ → Arg Type)) (ps : List (Arg Pattern)) → Clause-  ```--  These telescopes provide additional information on the types of-  pattern variables that was previously hard to reconstruct (see-  [#2151](https://github.com/agda/agda/issues/2151)). When unquoting a-  clause, the types in the clause telescope are currently ignored (but-  this is subject to change in the future).--  Three constructors of the `Pattern` datatype were also changed:--  * pattern variables now refer to a de Bruijn index (relative to the-    clause telescope) rather than a string,-  * absurd patterns take a de Bruijn index and are expected to be bound by the-    clause telescope,-  * dot patterns now include the actual dotted term.--  ```agda-  data Pattern where-    con    : (c : Name) (ps : List (Arg Pattern)) → Pattern-    dot    : (t : Term)    → Pattern   -- previously:   dot : Pattern-    var    : (x : Nat)     → Pattern   -- previously:   var : (x : String) → Pattern-    lit    : (l : Literal) → Pattern-    proj   : (f : Name)    → Pattern-    absurd : (x : Nat)     → Pattern-  ```--  It is likely that this change to the reflected syntax requires you-  to update reflection code written for previous versions of-  Agda. Here are some tips for updating your code:--  * When quoting a clause, you can recover the name of a pattern-    variable by looking up the given index in the clause-    telescope. The contents of dot patterns can safely be ignored-    (unless you have a use for them).--  * When creating a new clause for unquoting, you need to create a-    telescope for the types of the pattern variables. To get back the-    old behaviour of Agda, it is sufficient to set all the types of-    the pattern variables to `unknown`. So you can construct the-    telescope by listing the names of all pattern variables and absurd-    patterns together with their `ArgInfo`. Meanwhile, the pattern-    variables should be numbered in order to update them to the new-    representation. As for the telescope types, the contents of a-    `dot` pattern can safely be set to `unknown`.--- New operation in `TC` monad, `execTC`, which calls an external executable-  ```agda-  execTC : (exe : String) (args : List String) (stdIn : String)-         → TC (Σ Nat (λ _ → Σ String (λ _ → String)))-  ```-  The `execTC` builtin takes three arguments: the basename of the-  executable (e.g., `"echo"`), a list of arguments, and the contents-  of the standard input. It returns a triple, consisting of the exit-  code (as a natural number), the contents of the standard output, and-  the contents of the standard error.--  The builtin is only available when `--allow-exec` is passed. (Note-  that `--allow-exec` is incompatible with ``--safe``.) To make an-  executable available to Agda, add the absolute path on a new line in-  `~/.agda/executables`.--- Two new operations in the `TC` monad, `onlyReduceDefs` and-  `dontReduceDefs`:-  ```agda-  onlyReduceDefs : ∀ {a} {A : Set a} → List Name → TC A → TC A-  dontReduceDefs : ∀ {a} {A : Set a} → List Name → TC A → TC A-  ```-  These functions allow picking a specific set of functions that-  should (resp. should not) be reduced while executing the given `TC`-  computation.--  For example, the following macro unifies the current hole with the-  term `3 - 3`:-  ```agda-  macro₁ : Term -> TC ⊤-  macro₁ goal = do-    u   ← quoteTC ((1 + 2) - 3)-    u'  ← onlyReduceDefs (quote _+_ ∷ []) (normalise u)-    unify u' goal-  ```-- New operation in the `TC` monad, `withReconstructed`:-  ```agda-  withReconstructed : ∀ {a} {A : Set a} → TC A → TC A-  ```--  This function ensures reconstruction of hidden parameters-  after performing the `TC` computation.  For example, consider the-  following type and function:-  ```agda-  record RVec {a} (X : Set a) (n : Nat) : Set a where-    constructor vec-    field sel : Fin n → X--  test-rvec : Nat → RVec Nat 5-  test-rvec x = vec λ _ → x-  ```--  In the reflected syntax the body of the `test-rvec` would be represented-  as `con vec (unknown ∷ unknown ∷ unknown ∷ (lam _ x)`.  The use of-  `withReconstructed` replaces `unknown`s with the actual values:-  ```agda-  macro₂ : Name → Term → TC ⊤-  macro₂ n hole = do-    (function (clause tel ps t ∷ [])) ←-      withReconstructed (getDefinition n)-      where _ → quoteTC "ERROR" >>= unify hole-    quoteTC t >>= unify hole-  ```--- Three new constructors in the `Sort` datatype, `prop : Level →-  Sort`, `propLit : Nat → Sort`, and `inf : Nat → Sort`, representing-  the sorts `Prop ℓ`, `Propᵢ`, and `Setωᵢ`.--- Terms that belong to a type in `Prop` are no longer unquoted to-  `unknown` but to a proper `Term`. (See-  [#3553](https://github.com/agda/agda/issues/3553).)--Library management---------------------- `.agda-lib` files can now contain an extra field `flags:` with-  default flags for the library. Flags can be any flags that are-  accepted as part of an `{-# OPTIONS ... #-}` pragma. For example,-  file `my-library.agda-lib` with--  ```-  flags: --without-K-  ```--  will apply the `--without-K` flag to all Agda files in the current-  directory and (recursive) subdirectories that do not themselves-  contain an `.agda-lib` file.---Emacs mode-------------* New command prefix `C-u C-u C-u` for weak-head normalization. For instance,-  given--  ```agda-  downFrom : Nat → List Nat-  downFrom 0 = []-  downFrom (suc n) = n ∷ downFrom n-  ```--  `C-u C-u C-u C-c C-n downFrom 5` returns `4 ∷ downFrom 4`.--* New keyboard shortcut `C-c C-x C-i` for toggling display of-  irrelevant arguments.--* One can no longer use commands like `M-;` (`comment-dwim`) to-  uncomment block comments. In return one can use `M-;` to comment out-  pragmas. (See [#3329](https://github.com/agda/agda/issues/3329).)--JSON Interaction mode------------------------Changes have been made to the structure of error and warning-messages. The changes are summarized below. See-[#5052](https://github.com/agda/agda/issues/5052) for additional-details.--* The format of an error or warning was previously a bare string. Now, errors-  and warnings are represented by an object with a `"message"` key.--  This means that responses _previously_ structured like:--  ```json-  {"…": "…", "error": "Foo bar baz"}-  ```--  will now be structured:--  ```json-  {"…": "…", "error": {"message": "Foo bar baz"}}-  ```--  This applies directly to the `PostPonedCheckFunDef` response kind-  and `Error` info kind of the `DisplayInfo` response kind.--* The format of collections of errors or warnings, which previously were each-  represented by a single newline-joined string, has been updated to represent-  each warning or error individually in a list.--  That means that responses _previously_ structured like:--  ```json-  { "…": "…"-  , "errors": "Postulates overcooked\nAxioms too wiggly"-  , "warnings": "Something wrong\nSomething else\nwrong"-  }-  ```--  will now be structured:--  ```json-  { "…": "…"-  , "errors":-    [ { "message": "Postulates overcooked" }-    , { "message": "Axioms too wiggly" }-    ]-  , "warnings":-    [ { "message": "Something wrong" }-    , { "message": "Something else\nwrong" }-    ]-  }-  ```--  This applies to `CompilationOk`, `AllGoalsWarning`, and `Error` info-  kinds of the `DisplayInfo` response kind.--* The `Error` info kind of the `DisplayInfo` response kind has-  additionally been updated to distinguish warnings and errors.--  An example of the _previous_ format of a `DisplayInfo` response with-  an `Error` info kind was:-  ```json-  {-    "kind": "DisplayInfo",-    "info": {-      "kind": "Error",-      "message": "———— Error —————————————————————————————————————————————————\n/data/code/agda-test/Test.agda:2,1-9\nFailed to find source of module M in any of the following\nlocations:\n  /data/code/agda-test/M.agda\n  /data/code/agda-test/M.lagda\nwhen scope checking the declaration\n  import M\n\n———— Warning(s) ————————————————————————————————————————————\n/data/code/agda-test/Test.agda:3,1-10\nEmpty postulate block."-    }-  }-  ```--  The updated format is:-  ```json-  {-    "kind": "DisplayInfo",-    "info": {-      "kind": "Error",-      "error": {-        "message": "/data/code/agda-test/Test.agda:2,1-9\nFailed to find source of module M in any of the following\nlocations:\n  /data/code/agda-test/M.agda\n  /data/code/agda-test/M.lagda\nwhen scope checking the declaration\n  import M"-      },-      "warnings": [-        {-          "message": "/data/code/agda-test/Test.agda:3,1-10\nEmpty postulate block."-        }-      ]-    }-  }-  ```--Compiler backends -------------------- With option `--allow-unsolved-metas`, code with holes can be compiled.-  If a hole is reached at runtime, the compiled program crashes.-  See issue [#5103](https://github.com/agda/agda/issues/5103)--- Previously the GHC backend compiled at least one instance of Hinze's-  memoisation technique from ["Memo functions,-  polytypically!"](http://www.cs.ox.ac.uk/ralf.hinze/publications/index.html#P11)-  to reasonably efficient code. That is no longer the case (at least-  for that particular instance, see-  [#5153](https://github.com/agda/agda/issues/5153)).--LaTeX backend----------------- The spacing in comments is now preserved when generating LaTex files-  from literate Agda.  See-  [#5320](https://github.com/agda/agda/pull/5320) for more details.--HTML backend---------------- The named `id` attributes for local modules inside local modules are-  now different (see [#5335](https://github.com/agda/agda/pull/5320)).--  For instance, consider the following Agda file:-  ```agda-  module Top-level where--    module Inner where--      module Inside-inner where-  ```-  Previously one could link to the module `Inside-inner` using a URL-  that ended with `#Inside-inner`. Now one can use-  `#Inner.Inside-inner` instead.--JS backend-------------- Smaller local variable names in the generated JS code.--  Previously: `x0`, `x1`, `x2`, ...--  Now: `a`, `b`, `c`, ..., `z`, `a0`, `b0`, ..., `z0`, `a1`, `b1`, ...--- Improved indentation of generated JS code.--- More compact rendering of generated JS functions.--  Previously:-  ```js-  exports["N"]["suc"] = function (x0) {-      return function (x1) {-        return x1["suc"](x0);-      };-    };-  ```--  Now:-  ```js-  exports["N"]["suc"] = a => b => b["suc"](a);-  ```--- Irrelevant arguments are now erased in the generated JS code.--  Example Agda code:-  ```agda-  flip : {A B C : Set} -> (B -> A -> C) -> A -> B -> C-  flip f a b = f b a-  ```--  Previously generated JS code:-  ```js-  exports["flip"] = function (x0) {-      return function (x1) {-        return function (x2) {-          return function (x3) {-            return function (x4) {-              return function (x5) {-                return x3(x5)(x4);-              };-            };-          };-        };-      };-    };-  ```--  JS code generated now:-  ```js-  exports["flip"] = a => b => c => a(c)(b);-  ```--- Record fields are not stored separately (the fields are stored only-  in the constructor) in the generated JS code.--  Example Agda code:-  ```agda-  record Sigma (A : Set) (B : A -> Set) : Set where-    field-      fst : A-      snd : B fst-  ```--  Previously generated JS code (look at the `"fst"` and `"snd"` fields in the-  return value of `exports["Sigma"]["record"]`:-  ```js-  exports["Sigma"] = {};-  exports["Sigma"]["fst"] = function (x0) {-      return x0["record"]({-        "record": function (x1, x2) {-          return x1;-        }-      });-    };-  exports["Sigma"]["snd"] = function (x0) {-      return x0["record"]({-        "record": function (x1, x2) {-          return x2;-        }-      });-    };-  exports["Sigma"]["record"] = function (x0) {-      return function (x1) {-        return {-          "fst": x0,-          "record": function (x2) {-            return x2["record"](x0, x1);-          },-          "snd": x1-        };-      };-    };-  ```--  JS code generated now:-  ```js-  exports["Sigma"] = {};-  exports["Sigma"]["fst"] = a => a["record"]({"record": (b,c) => b});-  exports["Sigma"]["snd"] = a => a["record"]({"record": (b,c) => c});-  exports["Sigma"]["record"] = a => b => ({"record": c => c["record"](a,b)});-  ```--- `--js-optimize` flag has been added to the `agda` compiler.--  With `--js-optimize`, `agda` does not wrap records in JS objects.--  Example Agda code:-  ```agda-  record Sigma (A : Set) (B : A -> Set) : Set where-    field-      fst : A-      snd : B fst-  ```--  JS code generated without the `--js-optimize` flag:-  ```js-  exports["Sigma"] = {};-  exports["Sigma"]["fst"] = a => a["record"]({"record": (b,c) => b});-  exports["Sigma"]["snd"] = a => a["record"]({"record": (b,c) => c});-  exports["Sigma"]["record"] = a => b => ({"record": c => c["record"](a,b)});-  ```--  JS code generated with the `--js-optimize` flag:-  ```js-  exports["Sigma"] = {};-  exports["Sigma"]["fst"] = a => a((b,c) => b);-  exports["Sigma"]["snd"] = a => a((b,c) => c);-  exports["Sigma"]["record"] = a => b => c => c(a,b);-  ```--  With `--js-optimize`, `agda` uses JS arrays instead of JS objects.-  This is possible because constructor names are not relevant during the evaluation.--  Example Agda code:-  ```agda-  data Bool : Set where-    false : Bool-    true  : Bool--  not : Bool -> Bool-  not false = true-  not true  = false-  ```--  JS code generated without the `--js-optimize` flag:-  ```js-  exports["Bool"] = {};-  exports["Bool"]["false"] = a => a["false"]();-  exports["Bool"]["true"] = a => a["true"]();-  exports["not"] = a => a({-      "false": () => exports["Bool"]["true"],-      "true": () => exports["Bool"]["false"]-    });-  ```--  JS code generated with the `--js-optimize` flag:-  ```js-  exports["Bool"] = {};-  exports["Bool"]["false"] = a => a[0/* false */]();-  exports["Bool"]["true"] = a => a[1/* true */]();-  exports["not"] = a => a([-      /* false */() => exports["Bool"]["true"],-      /* true */() => exports["Bool"]["false"]-    ]);-  ```--  Note that comments are added to generated JS code to help human readers.--  Erased branches are replaced by `null` in the generated array.  If-  more than the half of branches are erased, the array is compressed-  to be a object like `{3: ..., 13: ...}`.--- `--js-minify` flag has been added to the `agda` compiler.--  With `--js-minify`, `agda` discards comments and whitespace in the-  generated JS code.---Agda as a library (API)--------------------------* The `SourceInfo` record has been renamed to `Source`, and the-  `sourceInfo` function to `parseSource`.--Other issues---------------For 2.6.2, the following issues were also closed (see [bug-tracker](https://github.com/agda/agda/issues)):--  -  [#418](https://github.com/agda/agda/issues/418): Unifier ignores presence of abstract keyword-  -  [#958](https://github.com/agda/agda/issues/958): Module application display forms in parameterised modules-  -  [#1145](https://github.com/agda/agda/issues/1145): Allow multiple layout keywords on the same line-  -  [#2151](https://github.com/agda/agda/issues/2151): Add TC primitive to check left-hand side-  -  [#2461](https://github.com/agda/agda/issues/2461): Support with in the presence of IApply patterns-  -  [#2858](https://github.com/agda/agda/issues/2858): Feature request: Interleaving mutually-defined functions & datatypes-  -  [#3000](https://github.com/agda/agda/issues/3000): Interaction: iterated give encounters internal error-  -  [#3118](https://github.com/agda/agda/issues/3118): Feature request: default flags in .agda-lib file-  -  [#3289](https://github.com/agda/agda/issues/3289): Postfix projections should not have hiding information-  -  [#3360](https://github.com/agda/agda/issues/3360): Make Emacs mode available as a normal package via MELPA-  -  [#3365](https://github.com/agda/agda/issues/3365): Update GitHub linguist syntax highlight file-  -  [#3398](https://github.com/agda/agda/issues/3398): With the option --allow-unsolved-metas, the unsolved metas are not shown, only yellow-  -  [#3422](https://github.com/agda/agda/issues/3422): Show names of instance candidates in error message-  -  [#3486](https://github.com/agda/agda/issues/3486): Elaborate-and-give shouldn't reduce solution-  -  [#3532](https://github.com/agda/agda/issues/3532): Refine does not work for functions with 10 arguments or more-  -  [#3538](https://github.com/agda/agda/issues/3538): Regression: Rewrite rule involving constructors rejected in parametrized module-  -  [#3588](https://github.com/agda/agda/issues/3588): Refine suggests overloaded constructor which is not in scope-  -  [#3627](https://github.com/agda/agda/issues/3627): Where-blocks of clauses with irrelevant projections can use irrelevant variables-  -  [#3644](https://github.com/agda/agda/issues/3644): Error message without position-  -  [#3672](https://github.com/agda/agda/issues/3672): Better error messages for generalize easter eggs-  -  [#3684](https://github.com/agda/agda/issues/3684): Make error about non-existent record field a warning?-  -  [#3734](https://github.com/agda/agda/issues/3734): WARNING_ON_USAGE is not raised for constructors-  -  [#3744](https://github.com/agda/agda/issues/3744): Internal error related to abstract-  -  [#3870](https://github.com/agda/agda/issues/3870): Internal error during instance search-  -  [#3926](https://github.com/agda/agda/issues/3926): Document the effect of `mutual` to the order of type checking-  -  [#3933](https://github.com/agda/agda/issues/3933): `import` can remove definitions from scope-  -  [#3961](https://github.com/agda/agda/issues/3961): Missing documentation for coverage checking-  -  [#4071](https://github.com/agda/agda/issues/4071): Ill-scoped code in error message-  -  [#4088](https://github.com/agda/agda/issues/4088): Strange scoping rules for irrefutable with, part 2-  -  [#4093](https://github.com/agda/agda/issues/4093): Make it possible to rename Set?-  -  [#4109](https://github.com/agda/agda/issues/4109): cannot declare data types in Setω-  -  [#4131](https://github.com/agda/agda/issues/4131): Record definition doesn't compile without a specific `let` binding-  -  [#4132](https://github.com/agda/agda/issues/4132): The regular expression for floats in the lexer is too liberal-  -  [#4135](https://github.com/agda/agda/issues/4135): Constructor disambiguation picks non-unique solution-  -  [#4157](https://github.com/agda/agda/issues/4157): Agda gets confused by multiple anonymous definitions in a single mutual block-  -  [#4160](https://github.com/agda/agda/issues/4160): Printing implicit lambdas with --show-implicit-  -  [#4161](https://github.com/agda/agda/issues/4161): An alternative solution for hGetContent error on Windows when non-English-  -  [#4166](https://github.com/agda/agda/issues/4166): Instances that are not in scope are candidates for instance resolution-  -  [#4208](https://github.com/agda/agda/issues/4208): Field named `_` in `genTel` record-  -  [#4252](https://github.com/agda/agda/issues/4252): Interaction ids get conflated after iterated give-  -  [#4265](https://github.com/agda/agda/issues/4265): Unsolved constraints when --no-syntactic-equality is used-  -  [#4280](https://github.com/agda/agda/issues/4280): Test case for #4169 fails in JS backend-  -  [#4291](https://github.com/agda/agda/issues/4291): Incorrect names can be generated for generalised variables-  -  [#4341](https://github.com/agda/agda/issues/4341): The documentation of inContext seems wrong.-  -  [#4350](https://github.com/agda/agda/issues/4350): Scoping bug with let open in telescope-  -  [#4365](https://github.com/agda/agda/issues/4365): Module fails to type check after parametrising it by postulates-  -  [#4400](https://github.com/agda/agda/issues/4400): TERMINATING pragma in where clause-  -  [#4425](https://github.com/agda/agda/issues/4425): [doc] What are .agdai files?-  -  [#4456](https://github.com/agda/agda/issues/4456): No error highlighting for error warnings?-  -  [#4458](https://github.com/agda/agda/issues/4458): The command agda2-measure-load-time is broken-  -  [#4481](https://github.com/agda/agda/issues/4481): Named implicit arguments do not behave the same in anonymous lambdas & definitions-  -  [#4482](https://github.com/agda/agda/issues/4482): "Unexpected implicit argument" should pinpoint exactly where the error starts-  -  [#4486](https://github.com/agda/agda/issues/4486): "did you mean" hint also for failing imports-  -  [#4491](https://github.com/agda/agda/issues/4491): Add a primitive for Data.Text's uncons-  -  [#4516](https://github.com/agda/agda/issues/4516): Internal error if files cannot be written to the directory for temporary files-  -  [#4518](https://github.com/agda/agda/issues/4518): Confusing error message if missing import-  -  [#4520](https://github.com/agda/agda/issues/4520): Better error for ambiguous BUILTIN [FROMNAT no longer working]-  -  [#4521](https://github.com/agda/agda/issues/4521): Massive increase in memory required to install Agda 2.6.1-  -  [#4526](https://github.com/agda/agda/issues/4526): Agda 2.6.1 bad performance: findProjectConfig slow in big directories-  -  [#4528](https://github.com/agda/agda/issues/4528): Internal error due to new forcing translation-  -  [#4530](https://github.com/agda/agda/issues/4530): Less normalization of goal types for instance search-  -  [#4534](https://github.com/agda/agda/issues/4534): [reflection] quote is not a defined name-  -  [#4536](https://github.com/agda/agda/issues/4536): co-pattern matching on empty record type removes body-  -  [#4538](https://github.com/agda/agda/issues/4538): changing the predefined precedence of an operator-  -  [#4543](https://github.com/agda/agda/issues/4543): Access violation on Windows on GHC 8.8.3, 8.8.4, 8.10.1 and 8.10.2-  -  [#4550](https://github.com/agda/agda/issues/4550): Documentation build: malformed code-block-  -  [#4556](https://github.com/agda/agda/issues/4556): [documentation] update hello world-  -  [#4557](https://github.com/agda/agda/issues/4557): activate github's discussions beta-  -  [#4560](https://github.com/agda/agda/issues/4560): Loss of canonicity with no-eta record and copatterns.-  -  [#4572](https://github.com/agda/agda/issues/4572): add PiSort and UnivSort to the documentation-  -  [#4576](https://github.com/agda/agda/issues/4576): quoteTC for Setω-  -  [#4580](https://github.com/agda/agda/issues/4580): No highlighting for pragmas FROMNAT, FROMNEG, FROMSTRING-  -  [#4583](https://github.com/agda/agda/issues/4583): QuickLaTeX backend does not highlight coinductive constructors as such-  -  [#4586](https://github.com/agda/agda/issues/4586): Better error message  for "Not a valid let declaration"-  -  [#4593](https://github.com/agda/agda/issues/4593): The blocking machinery seems to be broken-  -  [#4595](https://github.com/agda/agda/issues/4595): Should Setω be a type?-  -  [#4596](https://github.com/agda/agda/issues/4596): Improve pattern matching on records in telescopes-  -  [#4606](https://github.com/agda/agda/issues/4606): The combination of Cubical Agda with inductive families is logically inconsistent-  -  [#4610](https://github.com/agda/agda/issues/4610): Support Emacs 27.1-  -  [#4615](https://github.com/agda/agda/issues/4615): Enable --no-sort-comparison by default?-  -  [#4621](https://github.com/agda/agda/issues/4621): Make --rewriting infective-  -  [#4623](https://github.com/agda/agda/issues/4623): Empty where blocks should get dead code warnings-  -  [#4631](https://github.com/agda/agda/issues/4631): Non-linear patterns handled in a buggy way-  -  [#4637](https://github.com/agda/agda/issues/4637): recCon-NOT-PRINTED in termination error in connection to with-  -  [#4638](https://github.com/agda/agda/issues/4638): Erased constructors-  -  [#4649](https://github.com/agda/agda/issues/4649): Repair Agda's REPL (agda -I) to work with --safe flag-  -  [#4656](https://github.com/agda/agda/issues/4656): Function name not wrapped in `\AgdaFunction` in generated LaTeX-  -  [#4662](https://github.com/agda/agda/issues/4662): Current module contents-  -  [#4665](https://github.com/agda/agda/issues/4665): Documentation: add install instructions for stack-  -  [#4671](https://github.com/agda/agda/issues/4671): Weird error message on case-insensitive file systems-  -  [#4679](https://github.com/agda/agda/issues/4679): Cubical: giving seems to skip the boundary condition check for extended lambdas-  -  [#4681](https://github.com/agda/agda/issues/4681): Get rid of auto-inlining?-  -  [#4684](https://github.com/agda/agda/issues/4684): Type error due to --no-syntactic-equality-  -  [#4687](https://github.com/agda/agda/issues/4687): Instance search fails with two equal candidates-  -  [#4704](https://github.com/agda/agda/issues/4704): Case-split generates invalid code-  -  [#4707](https://github.com/agda/agda/issues/4707): Just warn when `using` directive has repetitions-  -  [#4721](https://github.com/agda/agda/issues/4721): de Bruijn index out of scope when using rewriting-  -  [#4727](https://github.com/agda/agda/issues/4727): Meta-variable solutions contain subterms with the wrong modality-  -  [#4735](https://github.com/agda/agda/issues/4735): primShowQName creates not-in-scope names-  -  [#4737](https://github.com/agda/agda/issues/4737): Turn error `Hiding ... has no effect` into a warning-  -  [#4750](https://github.com/agda/agda/issues/4750): Unification failure in 2.6.1 and the master branch-  -  [#4752](https://github.com/agda/agda/issues/4752): Panic on unbound variable with pattern synonym-  -  [#4768](https://github.com/agda/agda/issues/4768): De Bruijn index @0 in error "Not a finite domain"-  -  [#4769](https://github.com/agda/agda/issues/4769): mergeEqualPs ignores Name and ArgInfo of merged-in patterns-  -  [#4772](https://github.com/agda/agda/issues/4772): C-u C-u C-c C-? should show all goals normalized (Cmd_metas)-  -  [#4773](https://github.com/agda/agda/issues/4773): Missing does-not-export warning for `open` directive for parametrised module-  -  [#4775](https://github.com/agda/agda/issues/4775): Internal error when trying to use incorrect lambda syntax to pattern match-  -  [#4784](https://github.com/agda/agda/issues/4784): Make erasure compatible with univalence-  -  [#4795](https://github.com/agda/agda/issues/4795): Build "agda-tests" fails using dynamic linking-  -  [#4815](https://github.com/agda/agda/issues/4815): Current master fails compilation: binding for 'error' shadows the existing binding-  -  [#4828](https://github.com/agda/agda/issues/4828): Symlinks are incorrectly followed during compilation-  -  [#4833](https://github.com/agda/agda/issues/4833): Internal error: cannot type-check file-  -  [#4851](https://github.com/agda/agda/issues/4851): BUILTIN SIGMA and --type-in-type-  -  [#4852](https://github.com/agda/agda/issues/4852): First load the file-  -  [#4857](https://github.com/agda/agda/issues/4857): Instance argument is printed as explicit argument-  -  [#4869](https://github.com/agda/agda/issues/4869): Internal error at src/full/Agda/TypeChecking/Serialise/Instances/Internal.hs:147-  -  [#4880](https://github.com/agda/agda/issues/4880): Non-dependent, irrelevant, nameless arguments aren't accepted in arrows-  -  [#4882](https://github.com/agda/agda/issues/4882): Missing `reduce` in `literalStrategy`-  -  [#4888](https://github.com/agda/agda/issues/4888): "Illegal declaration(s) before top-level module" in Agda 2.6.1-  -  [#4909](https://github.com/agda/agda/issues/4909): Rewrite rule not accepted with --no-fast-reduce-  -  [#4924](https://github.com/agda/agda/issues/4924): Instance resolution loops infinitely even when an instance is available-  -  [#4925](https://github.com/agda/agda/issues/4925): Too aggressive literal overloading-  -  [#4928](https://github.com/agda/agda/issues/4928): Internal error checking cubical library-  -  [#4929](https://github.com/agda/agda/issues/4929): Regression in 2.6.1 connected to forcing translation (internal error)-  -  [#4944](https://github.com/agda/agda/issues/4944): Generalize: stuck on constraint ↑ i =< ↑ (↑ i) : Size-  -  [#4946](https://github.com/agda/agda/issues/4946): Size polarity brittle with generalization-  -  [#4949](https://github.com/agda/agda/issues/4949): Cubical: internal error in eta-expansion under constraints-  -  [#4950](https://github.com/agda/agda/issues/4950): Range too large in complaint about missing definitions-  -  [#4951](https://github.com/agda/agda/issues/4951): Data types in Setω are treated as non-fibrant-  -  [#4952](https://github.com/agda/agda/issues/4952): Incorrect HTML generated for renaming clause-  -  [#4962](https://github.com/agda/agda/issues/4962): JS backend: bugs involving "null"-  -  [#4967](https://github.com/agda/agda/issues/4967): Crazy bug when defining Ord instances for Int-  -  [#4970](https://github.com/agda/agda/issues/4970): `variable` use adds explicit argument-  -  [#4975](https://github.com/agda/agda/issues/4975): "no such meta variable" when calling `C-u C-c C-;`-  -  [#4982](https://github.com/agda/agda/issues/4982): Internal error related to Cubical Agda-  -  [#4986](https://github.com/agda/agda/issues/4986): Pattern matching allows you to turn `(x y : A) -> A` into `(@0 x y : A) -> A`-  -  [#4995](https://github.com/agda/agda/issues/4995): No Cycle should not look under lambdas.-  -  [#4998](https://github.com/agda/agda/issues/4998): Make case in clause with instance projection does not work-  -  [#4999](https://github.com/agda/agda/issues/4999): `primStringFromList` is not injective because of surrogate code points-  -  [#5002](https://github.com/agda/agda/issues/5002): Bad JavaScript generated-  -  [#5005](https://github.com/agda/agda/issues/5005): Add flag to print AGDA_DIR and exit-  -  [#5029](https://github.com/agda/agda/issues/5029): One can override --safe-  -  [#5033](https://github.com/agda/agda/issues/5033): Internal error related to @tick-  -  [#5048](https://github.com/agda/agda/issues/5048): Disturbing names in normalised reflected type-  -  [#5064](https://github.com/agda/agda/issues/5064): Give more information in error "Pattern matching on no-eta record types is by default not allowed"-  -  [#5065](https://github.com/agda/agda/issues/5065): The termination checker is too liberal-  -  [#5079](https://github.com/agda/agda/issues/5079): Deep pattern-matching is sometimes allowed for erased arguments-  -  [#5093](https://github.com/agda/agda/issues/5093): Weird instance propagation between parameterised modules-  -  [#5112](https://github.com/agda/agda/issues/5112): `make install-fix-whitespace` shouldn't use the `stack-X.Y.Z.yaml` files used for Agda-  -  [#5128](https://github.com/agda/agda/issues/5128): getDefinition sometimes loses patterns-  -  [#5133](https://github.com/agda/agda/issues/5133): Current master fails LaTeX-related tests-  -  [#5140](https://github.com/agda/agda/issues/5140): test/LaTeXAndHTML/succeed contains failing tests-  -  [#5146](https://github.com/agda/agda/issues/5146): v2.6.1.2 does not contain MAlonzo/RTE/Float.hs-  -  [#5161](https://github.com/agda/agda/issues/5161): No error location for error in imported module when .agdai file exists-  -  [#5167](https://github.com/agda/agda/issues/5167): Fix broken compatibility with agda-bench-  -  [#5168](https://github.com/agda/agda/issues/5168): User manual: Missing instructions for installing Agda from Hackage using stack-  -  [#5176](https://github.com/agda/agda/issues/5176): `mutual` is deprecated in doc-  -  [#5204](https://github.com/agda/agda/issues/5204): Investigate highlighting failures-  -  [#5205](https://github.com/agda/agda/issues/5205): acmart examples in (user-manual) fail to build with latest TeXLive-  -  [#5207](https://github.com/agda/agda/issues/5207): Agda generated code does not type-check with GHC 9.0-  -  [#5210](https://github.com/agda/agda/issues/5210): Internal error-  -  [#5230](https://github.com/agda/agda/issues/5230): When `stack.yaml` exists, `make` calls `stack`, even on `make debug`-  -  [#5231](https://github.com/agda/agda/issues/5231): Problems compiling hello-world.agda-  -  [#5237](https://github.com/agda/agda/issues/5237): `__IMPOSSIBLE__` from Agda.TypeChecking.Substitute-  -  [#5238](https://github.com/agda/agda/issues/5238): Rewrites are conjuring elements out of thin air-  -  [#5245](https://github.com/agda/agda/issues/5245): An infinite loop?-  -  [#5250](https://github.com/agda/agda/issues/5250): Change of warning options ignored-  -  [#5251](https://github.com/agda/agda/issues/5251): @0 annotation on lambda ignored-  -  [#5252](https://github.com/agda/agda/issues/5252): Internal error when case splitting pattern-lambda with higher rank type-  -  [#5286](https://github.com/agda/agda/issues/5286): Wrong error location with do notation and parse error in lhs-  -  [#5288](https://github.com/agda/agda/issues/5288): Very weird behaviour with compiled Data.Nat.Show.readMaybe-  -  [#5313](https://github.com/agda/agda/issues/5313): Documentation for internal level properties-  -  [#5314](https://github.com/agda/agda/issues/5314): Warn about abstract definitions without type signatures-  -  [#5317](https://github.com/agda/agda/issues/5317): The reflection machinery should support quantities-  -  [#5326](https://github.com/agda/agda/issues/5326): The highlighting code should be optimised-  -  [#5334](https://github.com/agda/agda/issues/5334): Meta-variable in constructor type busts interleaved mutual-  -  [#5335](https://github.com/agda/agda/issues/5335): Incorrect id attributes for local modules inside local modules-  -  [#5336](https://github.com/agda/agda/issues/5336): `data Foo constructor {cs : ts}` notation in `interleaved mutual`-  -  [#5339](https://github.com/agda/agda/issues/5339): `constructor` blocks do not tolerate overloading in same block-  -  [#5341](https://github.com/agda/agda/issues/5341): Do not make context variables non-erased-  -  [#5356](https://github.com/agda/agda/issues/5356): `interleaved mutual`: `data _ where` instead of `constructor`-  -  [#5358](https://github.com/agda/agda/issues/5358): tactic annotation on record field of function type drops domain in copattern definition-  -  [#5367](https://github.com/agda/agda/issues/5367): Parser regression involving `with` and `let`-  -  [#5370](https://github.com/agda/agda/issues/5370): Inconsistency in agda --help-  -  [#5375](https://github.com/agda/agda/issues/5375): Efficient conversion between interaction points and meta-variables-  -  [#5410](https://github.com/agda/agda/issues/5410): Module applications in where clauses of erased definitions yield non-erased code-  -  [#5419](https://github.com/agda/agda/issues/5419): Missing licences?-  -  [#5424](https://github.com/agda/agda/issues/5424): Internal error in v2.6.2 release candidate 1-  -  [#5434](https://github.com/agda/agda/issues/5434): The user manual's explanation of how erasure is checked for constructors does not match the implementation+Release notes for Agda version 2.6.2.1+======================================++Highlights+----------++* Agda 2.6.2.1 catches up to changes in the Haskell ecosystem+  (GHC 9.2.1, `aeson-2.0`, `hashable-1.4.`).++* Fixes some regressions introduced in 2.6.1:+  [#5283](https://github.com/agda/agda/issues/5283)+  [#5506](https://github.com/agda/agda/issues/5506)+  [#5610](https://github.com/agda/agda/issues/5610)++* Fixes some regressions introduced in 2.6.2:+  [#5508](https://github.com/agda/agda/issues/5508)+  [#5544](https://github.com/agda/agda/issues/5544)+  [#5565](https://github.com/agda/agda/issues/5565)+  [#5584](https://github.com/agda/agda/issues/5584)+  [#5620](https://github.com/agda/agda/issues/5620)+  [#5638](https://github.com/agda/agda/issues/5638)+  [#5657](https://github.com/agda/agda/issues/5657)++* Improvements to the compiler backends (see below).++* Feature preview: `--ghc-strict`.++Installation and infrastructure+-------------------------------++Agda 2.6.2.1 is expected to build with GHC versions 8.0 to 9.2.+It has been tested with the latest minor version releases of GHC for+each of these major versions:++  - 8.0.2+  - 8.2.2+  - 8.4.4+  - 8.6.5+  - 8.8.4+  - 8.10.7: Issue [#5539](https://github.com/agda/agda/issues/5539).+  - 9.0.1+  - 9.2.1:+    Issue [#5442](https://github.com/agda/agda/issues/5442),+    stackage issue [#6318](https://github.com/commercialhaskell/stackage/pull/6318).++Agda 2.6.2.1 has been adapted to recent changes in the Haskell ecosystem, including:++  - `Cabal-3.6.2`+  - `aeson-2.0`:+    Issue [#5593](https://github.com/agda/agda/issues/5593),+    stackage issue [#6217](https://github.com/commercialhaskell/stackage/issues/6217).+  - `hashable-1.4`:+    Stackage issue [#6268](https://github.com/commercialhaskell/stackage/issues/6268).+  - `transformers-0.6`++Compiler backends+-----------------++* Both the GHC and JS backends now refuse to compile code that uses+  `--cubical`.++* The new option `--ghc-strict-data`, which is inspired by the GHC+  language extension `StrictData`, makes the GHC backend compile+  inductive data and record constructors to constructors with strict+  arguments.++  This does not apply to certain builtin types—lists, the maybe type,+  and some types related to reflection—and might not apply to types+  with `COMPILE GHC … = data …` pragmas.++  This feature is experimental.++* The new option `--ghc-strict`, which is inspired by the GHC language+  extension `Strict`, makes the GHC backend generate mostly strict+  code.++  Functions might not be strict in unused arguments.++  Function definitions coming from `COMPILE GHC` pragmas are not+  affected.++  This flag implies `--ghc-strict-data`, and the exceptions of that+  flag applies to this flag as well.++  Note that this option requires the use of GHC 9 or later.++  This feature is experimental.++* JS backend now uses the native `BigInt` instead of the+  [biginteger.js](https://github.com/silentmatt/javascript-biginteger).+  Fixes [#4878](https://github.com/agda/agda/issues/4878).++LaTeX backend+-------------++* Files `agda.sty` and `postprocess-latex.pl` are now found in the `latex/`+  subdirectory of the Agda data directory (`agda --print-agda-dir`).++* `agda.sty` is now versioned (printed to the `.log` file by `latex`)+  (see [#5473](https://github.com/agda/agda/issues/5473)).++* Italics correction (inserted by `\textit` e.g. in `\AgdaBound`) now works,+  thanks to moving the `\textcolor` wrapping to the outside in `agda.sty`+  (see [#5471](https://github.com/agda/agda/issues/5471)).++List of closed issues+---------------------++For 2.6.2.1, the following issues were+[closed](https://github.com/agda/agda/issues?q=is%3Aissue+milestone%3A2.6.2.1+is%3Aclosed)+(see [bug tracker](https://github.com/agda/agda/issues)):++  - [#4878](https://github.com/agda/agda/issues/4878): Replace biginteger.js with native BigInt+  - [#5283](https://github.com/agda/agda/issues/5283): Tactic command runs forever+  - [#5291](https://github.com/agda/agda/issues/5291): `match` doesn't work for non-prefix-free cases+  - [#5302](https://github.com/agda/agda/issues/5302): building tests with cabal+  - [#5396](https://github.com/agda/agda/issues/5396): Internal error for rewriting without --confluence-check+  - [#5398](https://github.com/agda/agda/issues/5398): Problem with LaTeX code for multi-line comments with blank lines+  - [#5420](https://github.com/agda/agda/issues/5420): The JS backend generates incorrect code for Agda code that uses reflection+  - [#5421](https://github.com/agda/agda/issues/5421): The GHC backend generates incorrect code for Agda code that uses reflection+  - [#5431](https://github.com/agda/agda/issues/5431): --ghc-strict-data and --ghc-strict+  - [#5433](https://github.com/agda/agda/issues/5433): The JS backend "installs" highlight-hover.js+  - [#5440](https://github.com/agda/agda/issues/5440): (Re)Documenting `catchfilebetweentags` method of building latex files with Agda+  - [#5442](https://github.com/agda/agda/issues/5442): Support GHC 9.2+  - [#5463](https://github.com/agda/agda/issues/5463): Hole in the middle of a record is malformed+  - [#5465](https://github.com/agda/agda/issues/5465): Compilation of Parser.y depends on the locale on Debian too+  - [#5469](https://github.com/agda/agda/issues/5469): `onlyReduceDefs` should not prevent evaluation of macros+  - [#5470](https://github.com/agda/agda/issues/5470): Internal error when using `REWRITE` in `private` block+  - [#5471](https://github.com/agda/agda/issues/5471): LaTeX backend: italics correction+  - [#5473](https://github.com/agda/agda/issues/5473): agda.sty has no version+  - [#5478](https://github.com/agda/agda/issues/5478): Open goal inside record causes internal error (eta-contraction)+  - [#5481](https://github.com/agda/agda/issues/5481): Pattern-matching on records in Prop allows eliminating into Set+  - [#5489](https://github.com/agda/agda/issues/5489): C-c C-x C-a (abort) does not communicate well+  - [#5490](https://github.com/agda/agda/issues/5490): Why does abort (C-c C-x C-a) remove highlighting from the buffer?+  - [#5506](https://github.com/agda/agda/issues/5506): Agda panic: Pattern match failure+  - [#5508](https://github.com/agda/agda/issues/5508): Internal error typechecking non-terminating function on case-insensitive filesystem+  - [#5514](https://github.com/agda/agda/issues/5514): Support GHC 8.10.6+  - [#5531](https://github.com/agda/agda/issues/5531): Internal bug: TypeChecking/Sort+  - [#5532](https://github.com/agda/agda/issues/5532): "The module was successfully compiled" should mention with which backend+  - [#5539](https://github.com/agda/agda/issues/5539): Support GHC 8.10.7+  - [#5544](https://github.com/agda/agda/issues/5544): Internal error caused by addition of `Checkpoints` to `OpenThing`+  - [#5557](https://github.com/agda/agda/issues/5557): Allow Agda to output data files+  - [#5565](https://github.com/agda/agda/issues/5565): Internal error in Agda.TypeChecking.MetaVars+  - [#5593](https://github.com/agda/agda/issues/5593): Compilation failure with `aeson-2`+  - [#5602](https://github.com/agda/agda/issues/5602): The JS backend does not reduce constructor type signatures+  - [#5610](https://github.com/agda/agda/issues/5610): Panic when checking pragma BUILTIN SHARP+  - [#5620](https://github.com/agda/agda/issues/5620): Seemingly incorrect warning for abstract definition without type signature+  - [#5633](https://github.com/agda/agda/issues/5633): Case splitting inserts one with pattern too much (regression in 2.6.2)+  - [#5657](https://github.com/agda/agda/issues/5657): Internal error with postfix projection

@@ -4,19 +4,21 @@ and from Agdalight by Ulf Norell and Andreas Abel.  Agda 2 is currently actively developed mainly by Andreas Abel,-Guillaume Allais, Jesper Cockx, Nils Anders Danielsson, Philipp-Hausmann, Fredrik Nordvall Forsberg, Ulf Norell, Víctor López Juan,-Andrés Sicard-Ramírez, and Andrea Vezzosi.+Guillaume Allais, Liang-Ting Chen, Jesper Cockx, Matthew Daggitt, Nils+Anders Danielsson, Ulf Norell, Andrés Sicard-Ramírez, and Andrea+Vezzosi.  Further, Agda 2 has received contributions by, amongst others, Stevan Andjelkovic, Marcin Benke, Jean-Philippe Bernardy, Guillaume Brunerie,-James Chapman, Dominique Devriese, Péter Diviánszky, Olle Fredriksson,-Adam Gundry, Daniel Gustafsson, Kuen-Bang Hou (favonia), Patrik-Jansson, Alan Jeffrey, Wolfram Kahl, Wen Kokke, Fredrik Lindblad,-Francesco Mazzoli, Stefan Monnier, Darin Morrison, Guilhem Moulin,-Nicolas Pouillard, Nobuo Yamashita, Christian Sattler, Makoto-Takeyama and Tesla Ice Zhang.  The full list of contributors is-available at https://github.com/agda/agda/graphs/contributors+James Chapman, Dominique Devriese, Péter Diviánszky, Robert Estelle,+Olle Fredriksson, Adam Gundry, Daniel Gustafsson, Philipp Hausmann,+Alan Jeffrey, Wolfram Kahl, Wen Kokke, John Leo, Fredrik Lindblad,+Víctor López Juan, Ting-Gan Lua, Francesco Mazzoli, Stefan Monnier,+Guilhem Moulin, Fredrik Nordvall Forsberg, Nicolas Pouillard, Jonathan+Prieto, Christian Sattler, Makoto Takeyama, Noam Zeilberger, and Tesla+Ice Zhang.  The full list of contributors is available at+https://github.com/agda/agda/graphs/contributors or from the git+repository via ``git shortlog -sne``.  Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files (the@@ -71,7 +73,7 @@  ------------------------------------------------------------------------ -The file src/data/JS/highlight-hover.js (and the following licence+The file src/data/html/highlight-hover.js (and the following licence text?) seems to use the following licence:  Copyright 2002-2010, Simon Marlow.  All rights reserved.@@ -97,28 +99,3 @@ WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.----------------------------------------------------------------------------The file src/data/JS/biginteger.js (and the following licence text?)-seems to use the following licence:--Copyright (c) 2009 Matthew Crumley--Permission is hereby granted, free of charge, to any person obtaining a copy-of this software and associated documentation files (the "Software"), to deal-in the Software without restriction, including without limitation the rights-to use, copy, modify, merge, publish, distribute, sublicense, and/or sell-copies of the Software, and to permit persons to whom the Software is-furnished to do so, subject to the following conditions:--The above copyright notice and this permission notice shall be included in-all copies or substantial portions of the Software.--THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR-IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,-FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE-AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER-LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,-OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN-THE SOFTWARE.

@@ -3,7 +3,6 @@  [![Hackage version](https://img.shields.io/hackage/v/Agda.svg?label=Hackage)](http://hackage.haskell.org/package/Agda) [![Stackage version](https://www.stackage.org/package/Agda/badge/lts?label=Stackage)](https://www.stackage.org/package/Agda)-[![Travis Status](https://travis-ci.org/agda/agda.svg?branch=master)](https://travis-ci.org/agda/agda) [![Test](https://github.com/agda/agda/workflows/Build,%20Test,%20and%20Benchmark/badge.svg?branch=master)](https://github.com/agda/agda/actions?query=workflow%3A%22Build%2C+Test%2C+and+Benchmark%22) [![Stack Build Status via GH Actions](https://github.com/agda/agda/workflows/stack%20build/badge.svg)](https://github.com/agda/agda/actions?query=workflow%3A%22stack+build%22) [![Documentation Status](https://readthedocs.org/projects/agda/badge/?version=latest)](http://agda.readthedocs.io/en/latest/?badge=latest)

@@ -0,0 +1,1250 @@+Release notes for Agda version 2.6.2+====================================++Highlights+----------++* Several improvements and bug-fixes related to [Run-time+  Irrelevance](https://agda.readthedocs.io/en/v2.6.2/language/runtime-irrelevance.html).++* Several improvements and bug-fixes related to the [JavaScript+  Backend](https://agda.readthedocs.io/en/v2.6.2/tools/compilers.html#javascript-backend).++* Added experimental support for [Guarded Cubical+  Agda](https://agda.readthedocs.io/en/v2.6.2/language/guarded-cubical.html).++* The [Primitive+  Sorts](https://agda.readthedocs.io/en/v2.6.2/language/built-ins.html#sorts)+  of Agda (`Set` and `Prop`) are no longer keywords and can be renamed+  when importing `Agda.Primitive`.++* Added native support for the [Inspect+  Idiom](https://agda.readthedocs.io/en/v2.6.2/language/with-abstraction.html#with-abstraction-equality).++* Added support for making [System+  Calls](https://agda.readthedocs.io/en/v2.6.2/language/reflection.html#system-calls)+  from the reflection API.++Installation and infrastructure+-------------------------------++* Added support for GHC 8.10.5 and 9.0.1.++* Some expensive optimisations are now off by default+  (see [#4521](https://github.com/agda/agda/issues/4521)).++  These optimisations can in some cases make Agda substantially+  faster, but they can also make the compilation of the Agda program+  take more time and space.++  The optimisations can be turned on manually (Cabal:+  `-foptimise-heavily`, Stack: `--flag Agda:optimise-heavily`). They+  are turned on (by default) when Agda is installed using `make+  install`.++  If the optimisations are turned on it might make sense to limit+  GHC's memory usage (using something like `--ghc-options="+RTS -M6G+  -RTS"`).++Pragmas and options+-------------------++* New option `--auto-inline` turns on automatic compile-time inlining+  of simple functions. This was previously enabled by default.++  Note that the absence of automatic inlining can make typechecking+  substantially slower.++  The new default has repercussions on termination checking, for instance+  (see [#4702](https://github.com/agda/agda/issues/4702)).+  The following formulation of `plus` termination checks with `--auto-inline`+  but not without:+  ```agda+  open import Agda.Builtin.Nat++  case_of_ : {A B : Set} → A → (A → B) → B+  case x of f = f x++  plus : Nat → Nat → Nat+  plus m n = case m of λ+     { zero    → n+     ; (suc m) → suc (plus m n)+     }+  ```+  In this particular case, we can work around the limitation of the+  termination checker with pragma `{-# INLINE case_of_ #-}`.++* New options `--qualified-instances` (default) and+  `--no-qualified-instances`. When `--no-qualified-instances` is+  enabled, Agda will only consider candidates for instance search that+  are in scope under an unqualified name (see+  [#4522](https://github.com/agda/agda/pull/4522)).++* New option `--call-by-name` turns off call-by-need evaluation at type+  checking time.++* New option `--highlight-occurrences` (off by default) enables the HTML+  backend to include a JavaScript file that highlights all occurrences of+  the mouse-hovered symbol (see+  [#4535](https://github.com/agda/agda/pull/4535)).++* New option `--no-import-sorts` disables the implicit `open+  import Agda.Primitive using (Set; Prop)` at the top of each file+  (see below).++* New option `--local-confluence-check` to restore the old behaviour+  of the `--confluence-check` flag (see below for the new behaviour).++* New primitive `primStringFromListInjective` internalising the fact that+  `primStringFromList` is an injective function. It is bound in+  `Agda.Builtin.String.Properties`.++* New option `--allow-exec` enables the use of system calls during+  type checking using the `AGDATCMEXECTC` builtin.++* New option `--show-identity-substitutions` shows all arguments of+  metavariables when pretty-printing a term, even if they amount to+  just applying all the variables in the context.++* The option `--rewriting` is now considered infective: if a module has+  `--rewriting` enabled, then all modules importing it must also have+  `--rewriting` enabled.++* New option `--no-double-check` (default), opposite of the existing+  `--double-check`.++* Due to several known soundness issues with sized types (see+  [#1201](https://github.com/agda/agda/issues/1201),+  [#1946](https://github.com/agda/agda/issues/1946),+  [#2820](https://github.com/agda/agda/issues/2820),+  [#3026](https://github.com/agda/agda/issues/3026)), the+  `--sized-types` flag can no longer be used while `--safe` is active.++* New option `--guarded` turns on the Guarded Cubical extension of Agda.++  See [Guarded Cubical](https://agda.readthedocs.io/en/v2.6.2/language/guarded-cubical.html)+  in the documentation for more.++* The flags `--guardedness` and `--sized-types` are no longer enabled+  by default.++Command-line interaction+------------------------++* In the previous release, Agda exited with either status 0 when the+  program type checks successfully, or status 1 when encountering any+  kind of error.  Now Agda exits with status 42 for type errors, 71+  for errors in the commandline arguments, and 154 for impossible+  errors. Exit status 1 may be returned under other circumstances; for+  instance, an incomplete pattern matching, or an error generated by+  the Haskell runtime.  See PR+  [#4540](https://github.com/agda/agda/pull/4540).++Lexical syntax+--------------++* Layout handling has been improved so that block starters can be+  stacked on the same line+  [#1145](https://github.com/agda/agda/issues/1145).++  If several layout blocks are started by layout keywords without line+  break in between (where line breaks inside block comments do not+  count), then those blocks indented *more* than the last block go+  passive, meaning they cannot be further extended by new statements.+  ```agda+    private module M where postulate+              A : Set                 -- module-block goes passive+              B : Set                 -- postulate-block can still be extended+            module N where            -- private-block can still be extended+  ```+  Previously, this was a parse error.++Language+--------++* Inductive records without η-equality no longer support both matching+  on the record constructor and construction of record elements by+  copattern matching.  It has been discovered that the combination of+  both leads to loss of subject reduction, i.e., reduction does not+  preserve typing.  See issue+  [#4560](https://github.com/agda/agda/issues/4560).++  η-equality for a record can be turned off manually with directive+  `no-eta-equality` or command-line option `--no-eta-equality`, but it+  is also automatically turned off for some recursive records.  For+  records without η, matching on the record constructor is now off by+  default and construction by copattern matching is on.  If you want+  the converse, you can add the new record directive `pattern`.++  Example with record pattern:+  ```agda+  record N : Set where+    inductive+    no-eta-equality+    pattern+    field out : Maybe N++  pred : N → Maybe N+  pred record{ out = m } = m+  ```+  Example with record constructor and use of `;` instead of newline:+  ```agda+  record N : Set where+    inductive; no-eta-equality+    pattern; constructor inn+    field out : Maybe N++  pred : N → Maybe N+  pred (inn m) = m+  ```++* `Set` and `Prop` are no longer keywords but are now primitives+  defined in the module `Agda.Primitive`. They can be renamed when+  importing this module, for example:++  ```agda+  open import Agda.Primitive renaming (Set to Type)++  test : Type₁+  test = Type+  ```++  To preserve backwards compatibility, each top-level Agda module now+  starts with an implicit statement:++  ```agda+  open import Agda.Primitive using (Set; Prop)+  ```++  This implicit import can be disabled with the+  `--no-import-sorts` flag.++* Agda now has support for sorts `Setωᵢ` (alternative syntax: `Setωi`)+  for natural numbers `i`, where `Setω₀ = Setω`. These sorts form a+  second hierarchy `Setωᵢ : Setωᵢ₊₁` similar to the standard hierarchy+  of `Setᵢ`, but do not support universe polymorphism. It should not+  be necessary to refer to these sorts during normal usage of Agda,+  but they might be useful for defining reflection-based macros (see+  [#2119](https://github.com/agda/agda/issues/2119) and+  [#4585](https://github.com/agda/agda/issues/4585)).++* Changed the internal representation of literal strings: instead of using a+  linked list of characters (`String`), we are now using `Data.Text`. This+  should be a transparent change from the user's point of view: the backend+  was already packing these strings as text.++  Used this opportunity to introduce a `primStringUncons` primitive in+  `Agda.Builtin.String` (and to correspondingly add the+  `Agda.Builtin.Maybe` it needs).++* The option `--confluence-check` for rewrite rules has been given a+  new implementation that checks global confluence instead of local+  confluence. Concretely, it does so by enforcing two properties:++  1. For any two left-hand sides of the rewrite rules that overlap+     (either at the root position or at a subterm), the most general+     unifier of the two left-hand sides is again a left-hand side of a+     rewrite rule. For example, if there are two rules `suc m + n =+     suc (m + n)` and `m + suc n = suc (m + n)`, then there should+     also be a rule `suc m + suc n = suc (suc (m + n))`.++  2. Each rewrite rule should satisfy the *triangle property*: For any+     rewrite rule `u = w` and any single-step parallel unfolding `u =>+     v`, we should have another single-step parallel unfolding `v =>+     w`.++  The previous behaviour of the confluence checker that only ensures+  local confluence can be restored by using the+  `--local-confluence-check` flag.++* Binary integer literals with prefix `0b` (for instance,+  `0b11001001`) are now supported.++* Overloaded literals now require the conversion function (`fromNat`,+  `fromNeg`, or `fromString`) to be in scope *unqualified* to take+  effect.++  Previously, it was enough for the function to be in scope at all,+  which meant you couldn't import the corresponding builtin module+  without having overloaded literals turned on.++* Added `interleaved mutual` blocks where users can forward-declare+  function, record, and data types and interleave their+  definitions. These blocks are elaborated to more traditional mutual+  blocks by:++    - leaving the signatures where they are+    - grouping the clauses for a function together with the first of them+    - grouping the constructors for a datatype together with the first of them++  Example: two interleaved function definitions++  ```agda++  interleaved mutual++    -- Declarations:+    even : Nat → Bool+    odd  : Nat → Bool++    -- zero is even, not odd+    even zero = true+    odd  zero = false++    -- suc case: switch evenness on the predecessor+    even (suc n) = odd n+    odd  (suc n) = even n+  ```++  Other example: the definition of universe of types closed under the+  natural numbers and pairing:++  ```agda++  interleaved mutual++    -- Declaration of a product record, a universe of codes, and a decoding function+    record _×_ (A B : Set) : Set+    data U : Set+    El : U → Set++    -- We have a code for the type of natural numbers in our universe+    constructor `Nat : U+    El `Nat = Nat++    -- Btw we know how to pair values in a record+    record _×_ A B where+      constructor _,_+      inductive+      field fst : A; snd : B++    -- And we have a code for pairs in our universe+    constructor _`×_ : (A B : U) → U+    El (A `× B) = El A × El B+  ```++* Erased constructors (see+  [#4638](https://github.com/agda/agda/issues/4638)).++  Constructors can be marked as erased. Example:+  ```agda+    {-# OPTIONS --cubical --safe #-}++    open import Agda.Builtin.Cubical.Path+    open import Agda.Primitive++    private+      variable+        a   : Level+        A B : Set a++    Is-proposition : Set a → Set a+    Is-proposition A = (x y : A) → x ≡ y++    data ∥_∥ (A : Set a) : Set a where+      ∣_∣        : A → ∥ A ∥+      @0 trivial : Is-proposition ∥ A ∥++    rec : @0 Is-proposition B → (A → B) → ∥ A ∥ → B+    rec p f ∣ x ∣           = f x+    rec p f (trivial x y i) = p (rec p f x) (rec p f y) i+  ```+  In the code above the constructor `trivial` is only available at+  compile-time, whereas `∣_∣` is also available at run-time. Erased+  names can be used in bodies of clauses that match on `trivial`, if+  the match is done in a non-erased position, like in the final clause+  of `rec`. (Note that Cubical Agda programs still cannot be+  compiled.)++* Erased pattern-matching lambdas (see+  [#4525](https://github.com/agda/agda/issues/4525)).++  Regular pattern-matching lambdas are treated as non-erased+  function definitions. One can make a pattern-matching lambda erased+  by writing `@0` or `@erased` after the lambda:+  ```agda+  @0 _ : @0 Set → Set+  _ = λ @0 { A → A }++  @0 _ : @0 Set → Set+  _ = λ @erased where+    A → A+  ```++  The reflection machinery currently does not support erased+  pattern-matching lambdas (they are quoted as regular+  pattern-matching lambdas).++* New (?) rule for modalities of generalised variables+  (see [#5058](https://github.com/agda/agda/issues/5058)).++  The new rule is that generalisable variables get the modality that+  they are declared with, whereas other variables always get the+  default modality. (It is unclear what the old rule was, perhaps+  nothing was changed.)++* Private abstract type signatures can no longer see through abstract+  (see [#418](https://github.com/agda/agda/issues/418)).++  This means that abstract definitions no longer evaluate in *any*+  type signatures in the same module. Previously they evaluated in+  type signatures of definitions that were both private and abstract.++  It also means that metavariables in type signatures have to be+  solved locally, and cannot make use of information in the definition+  body, and that constructors of abstract datatypes are not in scope+  in type signatures.++* Type inference is disabled for abstract definitions (see+  [#418](https://github.com/agda/agda/issues/418)).++  This means that abstract definitions (inluding functions defined in+  `where` blocks of abstract definitions) need complete type+  signatures.++* One can now declare syntax with two name parts without any hole in+  between, and syntax without any holes.++  Examples:+  ```agda+  syntax Σ A (λ x → B) = [ x ∶ A ] × B+  syntax []            = [ ]+  ```++* Internalised the *inspect idiom* that allows users to abstract over+  an expression in a ``with`` clause while, at the same time,+  remembering the origin of the abstracted pattern via an equation.++  In the following example, abstracting over and then matching on the+  result of ``p x`` allows the first call to ``filter p (x ∷ xs)`` to+  reduce.++  In case the element ``x`` is kept, the second call to ``filter`` on+  the LHS then performs the same ``p x`` test. Because we have+  retained the proof that ``p x ≡ true`` in ``eq``, we are able to+  rewrite by this equality and get it to reduce too.++  This leads to just enough computation that we can finish the proof+  with an appeal to congruence and the induction hypothesis.++  ```agda+  filter-filter : ∀ p xs → filter p (filter p xs) ≡ filter p xs+  filter-filter p []       = refl+  filter-filter p (x ∷ xs) with p x in eq+  ... | false = filter-filter p xs -- easy+  ... | true -- second filter stuck on `p x`: rewrite by `eq`!+    rewrite eq = cong (x ∷_) (filter-filter p xs)+  ```++* As a consequence of the above extensions to `with`, lambdas and lets+  now need parentheses when appearing in a `with`. For instance,++  ```agda+  with-on-fun : Nat → Nat+  with-on-fun n with (λ m → m + n)  -- parentheses required!+  ... | f = f n+  ```++* It is now possible to add hiding and relevance annotations to `with`+  expressions. For example:++  ```agda+  module _ (A B : Set) (recompute : .B → .{{A}} → B) where++    _$_ : .(A → B) → .A → B+    f $ x with .{f} | .(f x) | .{{x}}+    ... | y = recompute y+  ```++Builtins+--------++- Primitive operations for floating-point numbers changed. The equalities now+  follow IEEE 754 equality, after unifying all NaNs. Primitive inequality was+  added:+  ```agda+  primFloatEquality   : Float -> Float -> Bool -- from primFloatNumericEquality+  primFloatLess       : Float -> Float -> Bool -- from primFloatNumericLess+  primFloatInequality : Float -> Float -> Bool -- new+  ```+  The “numeric” relations are now deprecated.++  There are several new predicates on floating-point numbers:+  ```agda+  primFloatIsInfinite     : Float -> Bool -- new+  primFloatIsNaN          : Float -> Bool -- new+  primFloatIsSafeInteger  : Float -> Bool -- new+  ```+  The `primFloatIsSafeInteger` function determines whether the value is a number+  that is a safe integer, i.e., is within the range where the arithmetic+  operations do not lose precision.++  The operations for conversion to integers (`primRound`, `primFloor`,+  and `primCeiling`) were renamed for consistency, and return a value+  of type `Maybe Int`, returning `nothing` for NaN and the infinities:+  ```agda+  primFloatRound   : Float → Maybe Int -- from primRound+  primFloatFloor   : Float → Maybe Int -- from primFloor+  primFloatCeiling : Float → Maybe Int -- from primCeiling+  ```++  There are several new conversions:+  ```agda+  primIntToFloat    : Int -> Float               -- new+  primFloatToRatio  : Float -> (Int × Nat)       -- new+  primRatioToFloat  : Int -> Nat -> Float        -- new+  primFloatDecode   : Float -> Maybe (Int × Int) -- new+  primFloatEncode   : Int -> Int -> Maybe Float  -- new+  ```+  The `primFloatDecode` function decodes a floating-point number f to a mantissa+  and exponent, such that `f = mantissa * 2 ^ exponent`, normalised such that+  the mantissa is the smallest possible number. The `primFloatEncode` function+  encodes a pair of a mantissa and exponent to a floating-point number.++  There are several new operations:+  ```agda+  primFloatPow        : Float -> Float -> Float -- new+  primFloatATan2      : Float -> Float -> Float -- from primATan2+  primFloatSinh       : Float -> Float          -- new+  primFloatCosh       : Float -> Float          -- new+  primFloatTanh       : Float -> Float          -- new+  primFloatASinh      : Float -> Float          -- new+  primFloatACosh      : Float -> Float          -- new+  primFloatATanh      : Float -> Float          -- new+  ```+  Furthermore, the following operations were renamed for consistency:+  ```agda+  primFloatExp        : Float -> Float          -- from primExp+  primFloatSin        : Float -> Float          -- from primSin+  primFloatLog        : Float -> Float          -- from primLog+  primFloatCos        : Float -> Float          -- from primCos+  primFloatTan        : Float -> Float          -- from primTan+  primFloatASin       : Float -> Float          -- from primASin+  primFloatACos       : Float -> Float          -- from primACos+  primFloatATan       : Float -> Float          -- from primATan+  ```++  All of these operations are implemented on the JavaScript backend.++- `primNatToChar` maps surrogate code points to the replacement character+  `'U+FFFD` and surrogate code points are disallowed in character literals++  [Surrogate code points](https://www.unicode.org/glossary/#surrogate_code_point)+  are characters in the range `U+D800` to `U+DFFF` and are reserved for use by+  UTF-16.++  The reason for this change is that strings are represented (at type-checking+  time and in the GHC backend) by Data.Text byte strings, which cannot+  represent surrogate code points and replaces them by `U+FFFD`. By doing the+  same for characters we can have `primStringFromList` be injective (witnessed+  by `Agda.Builtin.String.Properties.primStringFromListInjective`).+++Reflection+----------++- New operation in `TC` monad, similar to `quoteTC` but operating on+  types in `Setω`+  ```agda+  quoteωTC : ∀ {A : Setω} → A → TC Term+  ```+- `typeError` and `debugPrint` no longer inserts spaces around `termErr` and+  `nameErr` parts. They also do a better job of respecting line breaks in+  `strErr` parts.++- The reflection machinery now supports quantities in `Arg` (see+  [#5317](https://github.com/agda/agda/issues/5317)). The `ArgInfo`+  type has changed, and there are new types `Modality` and `Quantity`:+  ```agda+  data Quantity : Set where+    quantity-0 quantity-ω : Quantity++  {-# BUILTIN QUANTITY   Quantity   #-}+  {-# BUILTIN QUANTITY-0 quantity-0 #-}+  {-# BUILTIN QUANTITY-ω quantity-ω #-}++  data Modality : Set where+    modality : (r : Relevance) (q : Quantity) → Modality++  {-# BUILTIN MODALITY             Modality #-}+  {-# BUILTIN MODALITY-CONSTRUCTOR modality #-}++  data ArgInfo : Set where+    arg-info : (v : Visibility) (m : Modality) → ArgInfo+  ```++- The representation of reflected patterns and clauses has+  changed. Each clause now includes a telescope with the names and+  types of the pattern variables.++  ```agda+  data Clause where+    clause        : (tel : List (Σ String λ _ → Arg Type)) (ps : List (Arg Pattern)) (t : Term) → Clause+    absurd-clause : (tel : List (Σ String λ _ → Arg Type)) (ps : List (Arg Pattern)) → Clause+  ```++  These telescopes provide additional information on the types of+  pattern variables that was previously hard to reconstruct (see+  [#2151](https://github.com/agda/agda/issues/2151)). When unquoting a+  clause, the types in the clause telescope are currently ignored (but+  this is subject to change in the future).++  Three constructors of the `Pattern` datatype were also changed:++  * pattern variables now refer to a de Bruijn index (relative to the+    clause telescope) rather than a string,+  * absurd patterns take a de Bruijn index and are expected to be bound by the+    clause telescope,+  * dot patterns now include the actual dotted term.++  ```agda+  data Pattern where+    con    : (c : Name) (ps : List (Arg Pattern)) → Pattern+    dot    : (t : Term)    → Pattern   -- previously:   dot : Pattern+    var    : (x : Nat)     → Pattern   -- previously:   var : (x : String) → Pattern+    lit    : (l : Literal) → Pattern+    proj   : (f : Name)    → Pattern+    absurd : (x : Nat)     → Pattern+  ```++  It is likely that this change to the reflected syntax requires you+  to update reflection code written for previous versions of+  Agda. Here are some tips for updating your code:++  * When quoting a clause, you can recover the name of a pattern+    variable by looking up the given index in the clause+    telescope. The contents of dot patterns can safely be ignored+    (unless you have a use for them).++  * When creating a new clause for unquoting, you need to create a+    telescope for the types of the pattern variables. To get back the+    old behaviour of Agda, it is sufficient to set all the types of+    the pattern variables to `unknown`. So you can construct the+    telescope by listing the names of all pattern variables and absurd+    patterns together with their `ArgInfo`. Meanwhile, the pattern+    variables should be numbered in order to update them to the new+    representation. As for the telescope types, the contents of a+    `dot` pattern can safely be set to `unknown`.++- New operation in `TC` monad, `execTC`, which calls an external executable+  ```agda+  execTC : (exe : String) (args : List String) (stdIn : String)+         → TC (Σ Nat (λ _ → Σ String (λ _ → String)))+  ```+  The `execTC` builtin takes three arguments: the basename of the+  executable (e.g., `"echo"`), a list of arguments, and the contents+  of the standard input. It returns a triple, consisting of the exit+  code (as a natural number), the contents of the standard output, and+  the contents of the standard error.++  The builtin is only available when `--allow-exec` is passed. (Note+  that `--allow-exec` is incompatible with ``--safe``.) To make an+  executable available to Agda, add the absolute path on a new line in+  `~/.agda/executables`.++- Two new operations in the `TC` monad, `onlyReduceDefs` and+  `dontReduceDefs`:+  ```agda+  onlyReduceDefs : ∀ {a} {A : Set a} → List Name → TC A → TC A+  dontReduceDefs : ∀ {a} {A : Set a} → List Name → TC A → TC A+  ```+  These functions allow picking a specific set of functions that+  should (resp. should not) be reduced while executing the given `TC`+  computation.++  For example, the following macro unifies the current hole with the+  term `3 - 3`:+  ```agda+  macro₁ : Term -> TC ⊤+  macro₁ goal = do+    u   ← quoteTC ((1 + 2) - 3)+    u'  ← onlyReduceDefs (quote _+_ ∷ []) (normalise u)+    unify u' goal+  ```+- New operation in the `TC` monad, `withReconstructed`:+  ```agda+  withReconstructed : ∀ {a} {A : Set a} → TC A → TC A+  ```++  This function ensures reconstruction of hidden parameters+  after performing the `TC` computation.  For example, consider the+  following type and function:+  ```agda+  record RVec {a} (X : Set a) (n : Nat) : Set a where+    constructor vec+    field sel : Fin n → X++  test-rvec : Nat → RVec Nat 5+  test-rvec x = vec λ _ → x+  ```++  In the reflected syntax the body of the `test-rvec` would be represented+  as `con vec (unknown ∷ unknown ∷ unknown ∷ (lam _ x)`.  The use of+  `withReconstructed` replaces `unknown`s with the actual values:+  ```agda+  macro₂ : Name → Term → TC ⊤+  macro₂ n hole = do+    (function (clause tel ps t ∷ [])) ←+      withReconstructed (getDefinition n)+      where _ → quoteTC "ERROR" >>= unify hole+    quoteTC t >>= unify hole+  ```++- Three new constructors in the `Sort` datatype, `prop : Level →+  Sort`, `propLit : Nat → Sort`, and `inf : Nat → Sort`, representing+  the sorts `Prop ℓ`, `Propᵢ`, and `Setωᵢ`.++- Terms that belong to a type in `Prop` are no longer unquoted to+  `unknown` but to a proper `Term`. (See+  [#3553](https://github.com/agda/agda/issues/3553).)++Library management+------------------++- `.agda-lib` files can now contain an extra field `flags:` with+  default flags for the library. Flags can be any flags that are+  accepted as part of an `{-# OPTIONS ... #-}` pragma. For example,+  file `my-library.agda-lib` with++  ```+  flags: --without-K+  ```++  will apply the `--without-K` flag to all Agda files in the current+  directory and (recursive) subdirectories that do not themselves+  contain an `.agda-lib` file.+++Emacs mode+----------++* New command prefix `C-u C-u C-u` for weak-head normalization. For instance,+  given++  ```agda+  downFrom : Nat → List Nat+  downFrom 0 = []+  downFrom (suc n) = n ∷ downFrom n+  ```++  `C-u C-u C-u C-c C-n downFrom 5` returns `4 ∷ downFrom 4`.++* New keyboard shortcut `C-c C-x C-i` for toggling display of+  irrelevant arguments.++* One can no longer use commands like `M-;` (`comment-dwim`) to+  uncomment block comments. In return one can use `M-;` to comment out+  pragmas. (See [#3329](https://github.com/agda/agda/issues/3329).)++JSON Interaction mode+---------------------++Changes have been made to the structure of error and warning+messages. The changes are summarized below. See+[#5052](https://github.com/agda/agda/issues/5052) for additional+details.++* The format of an error or warning was previously a bare string. Now, errors+  and warnings are represented by an object with a `"message"` key.++  This means that responses _previously_ structured like:++  ```json+  {"…": "…", "error": "Foo bar baz"}+  ```++  will now be structured:++  ```json+  {"…": "…", "error": {"message": "Foo bar baz"}}+  ```++  This applies directly to the `PostPonedCheckFunDef` response kind+  and `Error` info kind of the `DisplayInfo` response kind.++* The format of collections of errors or warnings, which previously were each+  represented by a single newline-joined string, has been updated to represent+  each warning or error individually in a list.++  That means that responses _previously_ structured like:++  ```json+  { "…": "…"+  , "errors": "Postulates overcooked\nAxioms too wiggly"+  , "warnings": "Something wrong\nSomething else\nwrong"+  }+  ```++  will now be structured:++  ```json+  { "…": "…"+  , "errors":+    [ { "message": "Postulates overcooked" }+    , { "message": "Axioms too wiggly" }+    ]+  , "warnings":+    [ { "message": "Something wrong" }+    , { "message": "Something else\nwrong" }+    ]+  }+  ```++  This applies to `CompilationOk`, `AllGoalsWarning`, and `Error` info+  kinds of the `DisplayInfo` response kind.++* The `Error` info kind of the `DisplayInfo` response kind has+  additionally been updated to distinguish warnings and errors.++  An example of the _previous_ format of a `DisplayInfo` response with+  an `Error` info kind was:+  ```json+  {+    "kind": "DisplayInfo",+    "info": {+      "kind": "Error",+      "message": "———— Error —————————————————————————————————————————————————\n/data/code/agda-test/Test.agda:2,1-9\nFailed to find source of module M in any of the following\nlocations:\n  /data/code/agda-test/M.agda\n  /data/code/agda-test/M.lagda\nwhen scope checking the declaration\n  import M\n\n———— Warning(s) ————————————————————————————————————————————\n/data/code/agda-test/Test.agda:3,1-10\nEmpty postulate block."+    }+  }+  ```++  The updated format is:+  ```json+  {+    "kind": "DisplayInfo",+    "info": {+      "kind": "Error",+      "error": {+        "message": "/data/code/agda-test/Test.agda:2,1-9\nFailed to find source of module M in any of the following\nlocations:\n  /data/code/agda-test/M.agda\n  /data/code/agda-test/M.lagda\nwhen scope checking the declaration\n  import M"+      },+      "warnings": [+        {+          "message": "/data/code/agda-test/Test.agda:3,1-10\nEmpty postulate block."+        }+      ]+    }+  }+  ```++Compiler backends -----------------++- With option `--allow-unsolved-metas`, code with holes can be compiled.+  If a hole is reached at runtime, the compiled program crashes.+  See issue [#5103](https://github.com/agda/agda/issues/5103)++- Previously the GHC backend compiled at least one instance of Hinze's+  memoisation technique from ["Memo functions,+  polytypically!"](http://www.cs.ox.ac.uk/ralf.hinze/publications/index.html#P11)+  to reasonably efficient code. That is no longer the case (at least+  for that particular instance, see+  [#5153](https://github.com/agda/agda/issues/5153)).++LaTeX backend+-------------++- The spacing in comments is now preserved when generating LaTex files+  from literate Agda.  See+  [#5320](https://github.com/agda/agda/pull/5320) for more details.++HTML backend+------------++- The named `id` attributes for local modules inside local modules are+  now different (see [#5335](https://github.com/agda/agda/pull/5320)).++  For instance, consider the following Agda file:+  ```agda+  module Top-level where++    module Inner where++      module Inside-inner where+  ```+  Previously one could link to the module `Inside-inner` using a URL+  that ended with `#Inside-inner`. Now one can use+  `#Inner.Inside-inner` instead.++JS backend+----------++- Smaller local variable names in the generated JS code.++  Previously: `x0`, `x1`, `x2`, ...++  Now: `a`, `b`, `c`, ..., `z`, `a0`, `b0`, ..., `z0`, `a1`, `b1`, ...++- Improved indentation of generated JS code.++- More compact rendering of generated JS functions.++  Previously:+  ```js+  exports["N"]["suc"] = function (x0) {+      return function (x1) {+        return x1["suc"](x0);+      };+    };+  ```++  Now:+  ```js+  exports["N"]["suc"] = a => b => b["suc"](a);+  ```++- Irrelevant arguments are now erased in the generated JS code.++  Example Agda code:+  ```agda+  flip : {A B C : Set} -> (B -> A -> C) -> A -> B -> C+  flip f a b = f b a+  ```++  Previously generated JS code:+  ```js+  exports["flip"] = function (x0) {+      return function (x1) {+        return function (x2) {+          return function (x3) {+            return function (x4) {+              return function (x5) {+                return x3(x5)(x4);+              };+            };+          };+        };+      };+    };+  ```++  JS code generated now:+  ```js+  exports["flip"] = a => b => c => a(c)(b);+  ```++- Record fields are not stored separately (the fields are stored only+  in the constructor) in the generated JS code.++  Example Agda code:+  ```agda+  record Sigma (A : Set) (B : A -> Set) : Set where+    field+      fst : A+      snd : B fst+  ```++  Previously generated JS code (look at the `"fst"` and `"snd"` fields in the+  return value of `exports["Sigma"]["record"]`:+  ```js+  exports["Sigma"] = {};+  exports["Sigma"]["fst"] = function (x0) {+      return x0["record"]({+        "record": function (x1, x2) {+          return x1;+        }+      });+    };+  exports["Sigma"]["snd"] = function (x0) {+      return x0["record"]({+        "record": function (x1, x2) {+          return x2;+        }+      });+    };+  exports["Sigma"]["record"] = function (x0) {+      return function (x1) {+        return {+          "fst": x0,+          "record": function (x2) {+            return x2["record"](x0, x1);+          },+          "snd": x1+        };+      };+    };+  ```++  JS code generated now:+  ```js+  exports["Sigma"] = {};+  exports["Sigma"]["fst"] = a => a["record"]({"record": (b,c) => b});+  exports["Sigma"]["snd"] = a => a["record"]({"record": (b,c) => c});+  exports["Sigma"]["record"] = a => b => ({"record": c => c["record"](a,b)});+  ```++- `--js-optimize` flag has been added to the `agda` compiler.++  With `--js-optimize`, `agda` does not wrap records in JS objects.++  Example Agda code:+  ```agda+  record Sigma (A : Set) (B : A -> Set) : Set where+    field+      fst : A+      snd : B fst+  ```++  JS code generated without the `--js-optimize` flag:+  ```js+  exports["Sigma"] = {};+  exports["Sigma"]["fst"] = a => a["record"]({"record": (b,c) => b});+  exports["Sigma"]["snd"] = a => a["record"]({"record": (b,c) => c});+  exports["Sigma"]["record"] = a => b => ({"record": c => c["record"](a,b)});+  ```++  JS code generated with the `--js-optimize` flag:+  ```js+  exports["Sigma"] = {};+  exports["Sigma"]["fst"] = a => a((b,c) => b);+  exports["Sigma"]["snd"] = a => a((b,c) => c);+  exports["Sigma"]["record"] = a => b => c => c(a,b);+  ```++  With `--js-optimize`, `agda` uses JS arrays instead of JS objects.+  This is possible because constructor names are not relevant during the evaluation.++  Example Agda code:+  ```agda+  data Bool : Set where+    false : Bool+    true  : Bool++  not : Bool -> Bool+  not false = true+  not true  = false+  ```++  JS code generated without the `--js-optimize` flag:+  ```js+  exports["Bool"] = {};+  exports["Bool"]["false"] = a => a["false"]();+  exports["Bool"]["true"] = a => a["true"]();+  exports["not"] = a => a({+      "false": () => exports["Bool"]["true"],+      "true": () => exports["Bool"]["false"]+    });+  ```++  JS code generated with the `--js-optimize` flag:+  ```js+  exports["Bool"] = {};+  exports["Bool"]["false"] = a => a[0/* false */]();+  exports["Bool"]["true"] = a => a[1/* true */]();+  exports["not"] = a => a([+      /* false */() => exports["Bool"]["true"],+      /* true */() => exports["Bool"]["false"]+    ]);+  ```++  Note that comments are added to generated JS code to help human readers.++  Erased branches are replaced by `null` in the generated array.  If+  more than the half of branches are erased, the array is compressed+  to be a object like `{3: ..., 13: ...}`.++- `--js-minify` flag has been added to the `agda` compiler.++  With `--js-minify`, `agda` discards comments and whitespace in the+  generated JS code.+++Agda as a library (API)+-----------------------++* The `SourceInfo` record has been renamed to `Source`, and the+  `sourceInfo` function to `parseSource`.++Other issues+------------++For 2.6.2, the following issues were also closed (see [bug+tracker](https://github.com/agda/agda/issues)):++  -  [#418](https://github.com/agda/agda/issues/418): Unifier ignores presence of abstract keyword+  -  [#958](https://github.com/agda/agda/issues/958): Module application display forms in parameterised modules+  -  [#1145](https://github.com/agda/agda/issues/1145): Allow multiple layout keywords on the same line+  -  [#2151](https://github.com/agda/agda/issues/2151): Add TC primitive to check left-hand side+  -  [#2461](https://github.com/agda/agda/issues/2461): Support with in the presence of IApply patterns+  -  [#2858](https://github.com/agda/agda/issues/2858): Feature request: Interleaving mutually-defined functions & datatypes+  -  [#3000](https://github.com/agda/agda/issues/3000): Interaction: iterated give encounters internal error+  -  [#3118](https://github.com/agda/agda/issues/3118): Feature request: default flags in .agda-lib file+  -  [#3289](https://github.com/agda/agda/issues/3289): Postfix projections should not have hiding information+  -  [#3360](https://github.com/agda/agda/issues/3360): Make Emacs mode available as a normal package via MELPA+  -  [#3365](https://github.com/agda/agda/issues/3365): Update GitHub linguist syntax highlight file+  -  [#3398](https://github.com/agda/agda/issues/3398): With the option --allow-unsolved-metas, the unsolved metas are not shown, only yellow+  -  [#3422](https://github.com/agda/agda/issues/3422): Show names of instance candidates in error message+  -  [#3486](https://github.com/agda/agda/issues/3486): Elaborate-and-give shouldn't reduce solution+  -  [#3532](https://github.com/agda/agda/issues/3532): Refine does not work for functions with 10 arguments or more+  -  [#3538](https://github.com/agda/agda/issues/3538): Regression: Rewrite rule involving constructors rejected in parametrized module+  -  [#3588](https://github.com/agda/agda/issues/3588): Refine suggests overloaded constructor which is not in scope+  -  [#3627](https://github.com/agda/agda/issues/3627): Where-blocks of clauses with irrelevant projections can use irrelevant variables+  -  [#3644](https://github.com/agda/agda/issues/3644): Error message without position+  -  [#3672](https://github.com/agda/agda/issues/3672): Better error messages for generalize easter eggs+  -  [#3684](https://github.com/agda/agda/issues/3684): Make error about non-existent record field a warning?+  -  [#3734](https://github.com/agda/agda/issues/3734): WARNING_ON_USAGE is not raised for constructors+  -  [#3744](https://github.com/agda/agda/issues/3744): Internal error related to abstract+  -  [#3870](https://github.com/agda/agda/issues/3870): Internal error during instance search+  -  [#3926](https://github.com/agda/agda/issues/3926): Document the effect of `mutual` to the order of type checking+  -  [#3933](https://github.com/agda/agda/issues/3933): `import` can remove definitions from scope+  -  [#3961](https://github.com/agda/agda/issues/3961): Missing documentation for coverage checking+  -  [#4071](https://github.com/agda/agda/issues/4071): Ill-scoped code in error message+  -  [#4088](https://github.com/agda/agda/issues/4088): Strange scoping rules for irrefutable with, part 2+  -  [#4093](https://github.com/agda/agda/issues/4093): Make it possible to rename Set?+  -  [#4109](https://github.com/agda/agda/issues/4109): cannot declare data types in Setω+  -  [#4131](https://github.com/agda/agda/issues/4131): Record definition doesn't compile without a specific `let` binding+  -  [#4132](https://github.com/agda/agda/issues/4132): The regular expression for floats in the lexer is too liberal+  -  [#4135](https://github.com/agda/agda/issues/4135): Constructor disambiguation picks non-unique solution+  -  [#4157](https://github.com/agda/agda/issues/4157): Agda gets confused by multiple anonymous definitions in a single mutual block+  -  [#4160](https://github.com/agda/agda/issues/4160): Printing implicit lambdas with --show-implicit+  -  [#4161](https://github.com/agda/agda/issues/4161): An alternative solution for hGetContent error on Windows when non-English+  -  [#4166](https://github.com/agda/agda/issues/4166): Instances that are not in scope are candidates for instance resolution+  -  [#4208](https://github.com/agda/agda/issues/4208): Field named `_` in `genTel` record+  -  [#4252](https://github.com/agda/agda/issues/4252): Interaction ids get conflated after iterated give+  -  [#4265](https://github.com/agda/agda/issues/4265): Unsolved constraints when --no-syntactic-equality is used+  -  [#4280](https://github.com/agda/agda/issues/4280): Test case for #4169 fails in JS backend+  -  [#4291](https://github.com/agda/agda/issues/4291): Incorrect names can be generated for generalised variables+  -  [#4341](https://github.com/agda/agda/issues/4341): The documentation of inContext seems wrong.+  -  [#4350](https://github.com/agda/agda/issues/4350): Scoping bug with let open in telescope+  -  [#4365](https://github.com/agda/agda/issues/4365): Module fails to type check after parametrising it by postulates+  -  [#4400](https://github.com/agda/agda/issues/4400): TERMINATING pragma in where clause+  -  [#4425](https://github.com/agda/agda/issues/4425): [doc] What are .agdai files?+  -  [#4456](https://github.com/agda/agda/issues/4456): No error highlighting for error warnings?+  -  [#4458](https://github.com/agda/agda/issues/4458): The command agda2-measure-load-time is broken+  -  [#4481](https://github.com/agda/agda/issues/4481): Named implicit arguments do not behave the same in anonymous lambdas & definitions+  -  [#4482](https://github.com/agda/agda/issues/4482): "Unexpected implicit argument" should pinpoint exactly where the error starts+  -  [#4486](https://github.com/agda/agda/issues/4486): "did you mean" hint also for failing imports+  -  [#4491](https://github.com/agda/agda/issues/4491): Add a primitive for Data.Text's uncons+  -  [#4516](https://github.com/agda/agda/issues/4516): Internal error if files cannot be written to the directory for temporary files+  -  [#4518](https://github.com/agda/agda/issues/4518): Confusing error message if missing import+  -  [#4520](https://github.com/agda/agda/issues/4520): Better error for ambiguous BUILTIN [FROMNAT no longer working]+  -  [#4521](https://github.com/agda/agda/issues/4521): Massive increase in memory required to install Agda 2.6.1+  -  [#4526](https://github.com/agda/agda/issues/4526): Agda 2.6.1 bad performance: findProjectConfig slow in big directories+  -  [#4528](https://github.com/agda/agda/issues/4528): Internal error due to new forcing translation+  -  [#4530](https://github.com/agda/agda/issues/4530): Less normalization of goal types for instance search+  -  [#4534](https://github.com/agda/agda/issues/4534): [reflection] quote is not a defined name+  -  [#4536](https://github.com/agda/agda/issues/4536): co-pattern matching on empty record type removes body+  -  [#4538](https://github.com/agda/agda/issues/4538): changing the predefined precedence of an operator+  -  [#4543](https://github.com/agda/agda/issues/4543): Access violation on Windows on GHC 8.8.3, 8.8.4, 8.10.1 and 8.10.2+  -  [#4550](https://github.com/agda/agda/issues/4550): Documentation build: malformed code-block+  -  [#4556](https://github.com/agda/agda/issues/4556): [documentation] update hello world+  -  [#4557](https://github.com/agda/agda/issues/4557): activate github's discussions beta+  -  [#4560](https://github.com/agda/agda/issues/4560): Loss of canonicity with no-eta record and copatterns.+  -  [#4572](https://github.com/agda/agda/issues/4572): add PiSort and UnivSort to the documentation+  -  [#4576](https://github.com/agda/agda/issues/4576): quoteTC for Setω+  -  [#4580](https://github.com/agda/agda/issues/4580): No highlighting for pragmas FROMNAT, FROMNEG, FROMSTRING+  -  [#4583](https://github.com/agda/agda/issues/4583): QuickLaTeX backend does not highlight coinductive constructors as such+  -  [#4586](https://github.com/agda/agda/issues/4586): Better error message  for "Not a valid let declaration"+  -  [#4593](https://github.com/agda/agda/issues/4593): The blocking machinery seems to be broken+  -  [#4595](https://github.com/agda/agda/issues/4595): Should Setω be a type?+  -  [#4596](https://github.com/agda/agda/issues/4596): Improve pattern matching on records in telescopes+  -  [#4606](https://github.com/agda/agda/issues/4606): The combination of Cubical Agda with inductive families is logically inconsistent+  -  [#4610](https://github.com/agda/agda/issues/4610): Support Emacs 27.1+  -  [#4615](https://github.com/agda/agda/issues/4615): Enable --no-sort-comparison by default?+  -  [#4621](https://github.com/agda/agda/issues/4621): Make --rewriting infective+  -  [#4623](https://github.com/agda/agda/issues/4623): Empty where blocks should get dead code warnings+  -  [#4631](https://github.com/agda/agda/issues/4631): Non-linear patterns handled in a buggy way+  -  [#4637](https://github.com/agda/agda/issues/4637): recCon-NOT-PRINTED in termination error in connection to with+  -  [#4638](https://github.com/agda/agda/issues/4638): Erased constructors+  -  [#4649](https://github.com/agda/agda/issues/4649): Repair Agda's REPL (agda -I) to work with --safe flag+  -  [#4656](https://github.com/agda/agda/issues/4656): Function name not wrapped in `\AgdaFunction` in generated LaTeX+  -  [#4662](https://github.com/agda/agda/issues/4662): Current module contents+  -  [#4665](https://github.com/agda/agda/issues/4665): Documentation: add install instructions for stack+  -  [#4671](https://github.com/agda/agda/issues/4671): Weird error message on case-insensitive file systems+  -  [#4679](https://github.com/agda/agda/issues/4679): Cubical: giving seems to skip the boundary condition check for extended lambdas+  -  [#4681](https://github.com/agda/agda/issues/4681): Get rid of auto-inlining?+  -  [#4684](https://github.com/agda/agda/issues/4684): Type error due to --no-syntactic-equality+  -  [#4687](https://github.com/agda/agda/issues/4687): Instance search fails with two equal candidates+  -  [#4704](https://github.com/agda/agda/issues/4704): Case-split generates invalid code+  -  [#4707](https://github.com/agda/agda/issues/4707): Just warn when `using` directive has repetitions+  -  [#4721](https://github.com/agda/agda/issues/4721): de Bruijn index out of scope when using rewriting+  -  [#4727](https://github.com/agda/agda/issues/4727): Meta-variable solutions contain subterms with the wrong modality+  -  [#4735](https://github.com/agda/agda/issues/4735): primShowQName creates not-in-scope names+  -  [#4737](https://github.com/agda/agda/issues/4737): Turn error `Hiding ... has no effect` into a warning+  -  [#4750](https://github.com/agda/agda/issues/4750): Unification failure in 2.6.1 and the master branch+  -  [#4752](https://github.com/agda/agda/issues/4752): Panic on unbound variable with pattern synonym+  -  [#4768](https://github.com/agda/agda/issues/4768): De Bruijn index @0 in error "Not a finite domain"+  -  [#4769](https://github.com/agda/agda/issues/4769): mergeEqualPs ignores Name and ArgInfo of merged-in patterns+  -  [#4772](https://github.com/agda/agda/issues/4772): C-u C-u C-c C-? should show all goals normalized (Cmd_metas)+  -  [#4773](https://github.com/agda/agda/issues/4773): Missing does-not-export warning for `open` directive for parametrised module+  -  [#4775](https://github.com/agda/agda/issues/4775): Internal error when trying to use incorrect lambda syntax to pattern match+  -  [#4784](https://github.com/agda/agda/issues/4784): Make erasure compatible with univalence+  -  [#4795](https://github.com/agda/agda/issues/4795): Build "agda-tests" fails using dynamic linking+  -  [#4815](https://github.com/agda/agda/issues/4815): Current master fails compilation: binding for 'error' shadows the existing binding+  -  [#4828](https://github.com/agda/agda/issues/4828): Symlinks are incorrectly followed during compilation+  -  [#4833](https://github.com/agda/agda/issues/4833): Internal error: cannot type-check file+  -  [#4851](https://github.com/agda/agda/issues/4851): BUILTIN SIGMA and --type-in-type+  -  [#4852](https://github.com/agda/agda/issues/4852): First load the file+  -  [#4857](https://github.com/agda/agda/issues/4857): Instance argument is printed as explicit argument+  -  [#4869](https://github.com/agda/agda/issues/4869): Internal error at src/full/Agda/TypeChecking/Serialise/Instances/Internal.hs:147+  -  [#4880](https://github.com/agda/agda/issues/4880): Non-dependent, irrelevant, nameless arguments aren't accepted in arrows+  -  [#4882](https://github.com/agda/agda/issues/4882): Missing `reduce` in `literalStrategy`+  -  [#4888](https://github.com/agda/agda/issues/4888): "Illegal declaration(s) before top-level module" in Agda 2.6.1+  -  [#4909](https://github.com/agda/agda/issues/4909): Rewrite rule not accepted with --no-fast-reduce+  -  [#4924](https://github.com/agda/agda/issues/4924): Instance resolution loops infinitely even when an instance is available+  -  [#4925](https://github.com/agda/agda/issues/4925): Too aggressive literal overloading+  -  [#4928](https://github.com/agda/agda/issues/4928): Internal error checking cubical library+  -  [#4929](https://github.com/agda/agda/issues/4929): Regression in 2.6.1 connected to forcing translation (internal error)+  -  [#4944](https://github.com/agda/agda/issues/4944): Generalize: stuck on constraint ↑ i =< ↑ (↑ i) : Size+  -  [#4946](https://github.com/agda/agda/issues/4946): Size polarity brittle with generalization+  -  [#4949](https://github.com/agda/agda/issues/4949): Cubical: internal error in eta-expansion under constraints+  -  [#4950](https://github.com/agda/agda/issues/4950): Range too large in complaint about missing definitions+  -  [#4951](https://github.com/agda/agda/issues/4951): Data types in Setω are treated as non-fibrant+  -  [#4952](https://github.com/agda/agda/issues/4952): Incorrect HTML generated for renaming clause+  -  [#4962](https://github.com/agda/agda/issues/4962): JS backend: bugs involving "null"+  -  [#4967](https://github.com/agda/agda/issues/4967): Crazy bug when defining Ord instances for Int+  -  [#4970](https://github.com/agda/agda/issues/4970): `variable` use adds explicit argument+  -  [#4975](https://github.com/agda/agda/issues/4975): "no such meta variable" when calling `C-u C-c C-;`+  -  [#4982](https://github.com/agda/agda/issues/4982): Internal error related to Cubical Agda+  -  [#4986](https://github.com/agda/agda/issues/4986): Pattern matching allows you to turn `(x y : A) -> A` into `(@0 x y : A) -> A`+  -  [#4995](https://github.com/agda/agda/issues/4995): No Cycle should not look under lambdas.+  -  [#4998](https://github.com/agda/agda/issues/4998): Make case in clause with instance projection does not work+  -  [#4999](https://github.com/agda/agda/issues/4999): `primStringFromList` is not injective because of surrogate code points+  -  [#5002](https://github.com/agda/agda/issues/5002): Bad JavaScript generated+  -  [#5005](https://github.com/agda/agda/issues/5005): Add flag to print AGDA_DIR and exit+  -  [#5029](https://github.com/agda/agda/issues/5029): One can override --safe+  -  [#5033](https://github.com/agda/agda/issues/5033): Internal error related to @tick+  -  [#5048](https://github.com/agda/agda/issues/5048): Disturbing names in normalised reflected type+  -  [#5064](https://github.com/agda/agda/issues/5064): Give more information in error "Pattern matching on no-eta record types is by default not allowed"+  -  [#5065](https://github.com/agda/agda/issues/5065): The termination checker is too liberal+  -  [#5079](https://github.com/agda/agda/issues/5079): Deep pattern-matching is sometimes allowed for erased arguments+  -  [#5093](https://github.com/agda/agda/issues/5093): Weird instance propagation between parameterised modules+  -  [#5112](https://github.com/agda/agda/issues/5112): `make install-fix-whitespace` shouldn't use the `stack-X.Y.Z.yaml` files used for Agda+  -  [#5128](https://github.com/agda/agda/issues/5128): getDefinition sometimes loses patterns+  -  [#5133](https://github.com/agda/agda/issues/5133): Current master fails LaTeX-related tests+  -  [#5140](https://github.com/agda/agda/issues/5140): test/LaTeXAndHTML/succeed contains failing tests+  -  [#5146](https://github.com/agda/agda/issues/5146): v2.6.1.2 does not contain MAlonzo/RTE/Float.hs+  -  [#5161](https://github.com/agda/agda/issues/5161): No error location for error in imported module when .agdai file exists+  -  [#5167](https://github.com/agda/agda/issues/5167): Fix broken compatibility with agda-bench+  -  [#5168](https://github.com/agda/agda/issues/5168): User manual: Missing instructions for installing Agda from Hackage using stack+  -  [#5176](https://github.com/agda/agda/issues/5176): `mutual` is deprecated in doc+  -  [#5204](https://github.com/agda/agda/issues/5204): Investigate highlighting failures+  -  [#5205](https://github.com/agda/agda/issues/5205): acmart examples in (user-manual) fail to build with latest TeXLive+  -  [#5207](https://github.com/agda/agda/issues/5207): Agda generated code does not type-check with GHC 9.0+  -  [#5210](https://github.com/agda/agda/issues/5210): Internal error+  -  [#5230](https://github.com/agda/agda/issues/5230): When `stack.yaml` exists, `make` calls `stack`, even on `make debug`+  -  [#5231](https://github.com/agda/agda/issues/5231): Problems compiling hello-world.agda+  -  [#5237](https://github.com/agda/agda/issues/5237): `__IMPOSSIBLE__` from Agda.TypeChecking.Substitute+  -  [#5238](https://github.com/agda/agda/issues/5238): Rewrites are conjuring elements out of thin air+  -  [#5245](https://github.com/agda/agda/issues/5245): An infinite loop?+  -  [#5250](https://github.com/agda/agda/issues/5250): Change of warning options ignored+  -  [#5251](https://github.com/agda/agda/issues/5251): @0 annotation on lambda ignored+  -  [#5252](https://github.com/agda/agda/issues/5252): Internal error when case splitting pattern-lambda with higher rank type+  -  [#5286](https://github.com/agda/agda/issues/5286): Wrong error location with do notation and parse error in lhs+  -  [#5288](https://github.com/agda/agda/issues/5288): Very weird behaviour with compiled Data.Nat.Show.readMaybe+  -  [#5313](https://github.com/agda/agda/issues/5313): Documentation for internal level properties+  -  [#5314](https://github.com/agda/agda/issues/5314): Warn about abstract definitions without type signatures+  -  [#5317](https://github.com/agda/agda/issues/5317): The reflection machinery should support quantities+  -  [#5326](https://github.com/agda/agda/issues/5326): The highlighting code should be optimised+  -  [#5334](https://github.com/agda/agda/issues/5334): Meta-variable in constructor type busts interleaved mutual+  -  [#5335](https://github.com/agda/agda/issues/5335): Incorrect id attributes for local modules inside local modules+  -  [#5336](https://github.com/agda/agda/issues/5336): `data Foo constructor {cs : ts}` notation in `interleaved mutual`+  -  [#5339](https://github.com/agda/agda/issues/5339): `constructor` blocks do not tolerate overloading in same block+  -  [#5341](https://github.com/agda/agda/issues/5341): Do not make context variables non-erased+  -  [#5356](https://github.com/agda/agda/issues/5356): `interleaved mutual`: `data _ where` instead of `constructor`+  -  [#5358](https://github.com/agda/agda/issues/5358): tactic annotation on record field of function type drops domain in copattern definition+  -  [#5367](https://github.com/agda/agda/issues/5367): Parser regression involving `with` and `let`+  -  [#5370](https://github.com/agda/agda/issues/5370): Inconsistency in agda --help+  -  [#5375](https://github.com/agda/agda/issues/5375): Efficient conversion between interaction points and meta-variables+  -  [#5410](https://github.com/agda/agda/issues/5410): Module applications in where clauses of erased definitions yield non-erased code+  -  [#5419](https://github.com/agda/agda/issues/5419): Missing licences?+  -  [#5424](https://github.com/agda/agda/issues/5424): Internal error in v2.6.2 release candidate 1+  -  [#5434](https://github.com/agda/agda/issues/5434): The user manual's explanation of how erasure is checked for constructors does not match the implementation

binary file changed (1228011 → absent bytes)

@@ -1,13 +1,15 @@+{-# LANGUAGE ScopedTypeVariables #-}+ -- | A program which either tries to add setup code for Agda's Emacs -- mode to the users .emacs file, or provides information to Emacs -- about where the Emacs mode is installed.  module Main (main) where -import Control.Exception+import Control.Exception as E import Control.Monad import Data.Char-import Data.List+import Data.List (intercalate, isInfixOf) import Data.Maybe import Data.Version import Numeric@@ -16,6 +18,7 @@ import System.Exit import System.FilePath import System.IO+-- import System.IO.Error (isDoesNotExistError) import System.Process  import Paths_Agda (getDataDir, version)@@ -163,7 +166,7 @@   bracket (openTempFile tempDir "askEmacs")           (removeFile . fst) $ \(file, h) -> do     hClose h-    exit <- rawSystem "emacs"+    exit <- rawSystemWithDiagnostics "emacs"                       [ "--no-desktop", "-nw", "--no-splash"                           -- Andreas, 2014-01-11: ^ try a leaner startup of emacs                           -- Andreas, 2018-09-08: -nw instead of --no-window-system as some emacses do not support the long version@@ -182,6 +185,26 @@       -- prematurely.       return result +-- | Like 'rawSystem' but handles 'IOException' by printing diagnostics+-- (@PATH@) before 'exitFailure'.++rawSystemWithDiagnostics+  :: FilePath  -- ^ Command to run.+  -> [String]  -- ^ Arguments to command.+  -> IO ExitCode+rawSystemWithDiagnostics cmd args =+    rawSystem cmd args+  `E.catch` \ (e :: IOException) -> do+     informLn $ unwords [ "FAILED:", showCommandForUser cmd args ]+     informLn $ unwords [ "Exception:", show e ]+     -- The PATH might be useful in other exceptions, like "permission denied".+     -- when (isDoesNotExistError e) $ do+     path <- fromMaybe "(not found)" <$> findExecutable cmd+     informLn $ unwords [ "Executable", cmd, "at:", path ]+     informLn "PATH:"+     mapM_ (informLn . ("  - " ++)) =<< getSearchPath+     exitFailure+ -- | Escapes the string so that Emacs can parse it as an Elisp string.  escape :: FilePath -> FilePath@@ -225,7 +248,7 @@       exitFailure   where   compile dataDir f = do-    exit <- rawSystem "emacs" $+    exit <- rawSystemWithDiagnostics "emacs" $                       [ "--no-init-file", "--no-site-file"                       , "--directory", dataDir                       , "--batch"

@@ -1,41 +0,0 @@-/* Aspects. */-.Agda .Comment       { color: #B22222 }-.Agda .Background    {}-.Agda .Markup        { color: #000000 }-.Agda .Keyword       { color: #CD6600 }-.Agda .String        { color: #B22222 }-.Agda .Number        { color: #A020F0 }-.Agda .Symbol        { color: #404040 }-.Agda .PrimitiveType { color: #0000CD }-.Agda .Pragma        { color: black   }-.Agda .Operator      {}-.Agda .Hole          { background: #B4EEB4 }--/* NameKinds. */-.Agda .Bound                  { color: black   }-.Agda .Generalizable          { color: black   }-.Agda .InductiveConstructor   { color: #008B00 }-.Agda .CoinductiveConstructor { color: #8B7500 }-.Agda .Datatype               { color: #0000CD }-.Agda .Field                  { color: #EE1289 }-.Agda .Function               { color: #0000CD }-.Agda .Module                 { color: #A020F0 }-.Agda .Postulate              { color: #0000CD }-.Agda .Primitive              { color: #0000CD }-.Agda .Record                 { color: #0000CD }--/* OtherAspects. */-.Agda .DottedPattern        {}-.Agda .UnsolvedMeta         { color: black; background: yellow         }-.Agda .UnsolvedConstraint   { color: black; background: yellow         }-.Agda .TerminationProblem   { color: black; background: #FFA07A        }-.Agda .IncompletePattern    { color: black; background: #F5DEB3        }-.Agda .Error                { color: red;   text-decoration: underline }-.Agda .TypeChecks           { color: black; background: #ADD8E6        }-.Agda .Deadcode             { color: black; background: #808080        }-.Agda .ShadowingInTelescope { color: black; background: #808080        }--/* Standard attributes. */-.Agda a { text-decoration: none }-.Agda a[href]:hover { background-color: #B4EEB4 }-.Agda [href].hover-highlight { background-color: #B4EEB4; }

@@ -10,69 +10,62 @@ // which return Agda types like Maybe. These are never emitted by the compiler, // but can be used internally to define other prefixes. -const biginteger = require("biginteger");- // Integers-exports.primIntegerFromString = function(x) {-  return biginteger.BigInteger(x);-};-exports.primShowInteger = function(x) {-  return x.toString();-};-exports.uprimIntegerPlus = function(x,y) {-  return x.add(y);-};-exports.uprimIntegerMinus = function(x,y) {-  return x.subtract(y);-};-exports.uprimIntegerMultiply = function(x,y) {-  return x.multiply(y);-};-exports.uprimIntegerRem = function(x, y) {-  return x.remainder(y);-};-exports.uprimIntegerQuot = function(x, y) {-  return x.quotient(y);-};-exports.uprimIntegerEqual = function(x,y) {-  return x.compare(y) == 0;-};-exports.uprimIntegerGreaterOrEqualThan = function(x,y) {-  return x.compare(y) >= 0;-};-exports.uprimIntegerLessThan = function(x,y) {-  return x.compare(y) == -1;-}; +// primIntegerFromString : String -> Int+exports.primIntegerFromString = BigInt;++// primShowInteger : Int -> String+exports.primShowInteger = x => x.toString();++// uprimIntegerPlus : (Int, Int) -> Int+exports.uprimIntegerPlus = (x, y) => x + y;++// uprimIntegerMinus : (Int, Int) -> Int+exports.uprimIntegerMinus = (x, y) => x - y;++// uprimIntegerMultiply : (Int, Int) -> Int+exports.uprimIntegerMultiply = (x, y) => x * y;++// uprimIntegerRem : (Int, Int) -> Int+exports.uprimIntegerRem = (x, y) => x % y;++// uprimIntegerQuot : (Int, Int) -> Int+exports.uprimIntegerQuot = (x, y) => x / y;++// uprimIntegerEqual : (Int, Int) -> Bool+exports.uprimIntegerEqual = (x, y) => x === y;++// uprimIntegerGreaterOrEqualThan : (Int, Int) -> Bool+exports.uprimIntegerGreaterOrEqualThan = (x, y) => x >= y;++// uprimIntegerLessThan : (Int, Int) -> Bool+exports.uprimIntegerLessThan = (x, y) => x < y;+ // Words-const WORD64_MAX_VALUE = exports.primIntegerFromString("18446744073709552000");+const WORD64_MAX_VALUE = 18446744073709552000n; -exports.primWord64ToNat = function(x) {-    return x;-};-exports.primWord64FromNat = function(x) {-    return x.remainder(WORD64_MAX_VALUE);-};-exports.uprimWord64Plus = function(x, y) {-    return x.add(y).remainder(WORD64_MAX_VALUE);-};-exports.uprimWord64Minus = function(x, y) {-    return x.add(WORD64_MAX_VALUE).subtract(y).remainder(WORD64_MAX_VALUE);-};-exports.uprimWord64Multiply = function(x, y) {-    return x.multiply(y).remainder(WORD64_MAX_VALUE);-};+// primWord64ToNat : Word64 -> Nat+exports.primWord64ToNat = x => x; +// primWord64FromNat : Nat -> Word64+exports.primWord64FromNat = x => x % WORD64_MAX_VALUE;++// uprimWord64Plus : (Word64, Word64) -> Word64+exports.uprimWord64Plus = (x, y) => (x + y) % WORD64_MAX_VALUE;++// uprimWord64Minus : (Word64, Word64) -> Word64+exports.uprimWord64Minus = (x, y) => (x + WORD64_MAX_VALUE - y) % WORD64_MAX_VALUE;++// uprimWord64Multiply : (Word64, Word64) -> Word64+exports.uprimWord64Multiply = (x, y) => (x * y) % WORD64_MAX_VALUE;+ // Natural numbers-exports.primNatMinus = function(x) {-  return function(y) {-    var z = x.subtract(y);-    if (z.isNegative()) {-      return biginteger.ZERO;-    } else {-      return z;-    }-  };++// primNatMinus : Nat -> Nat -> Nat+exports.primNatMinus = x => y => {+  const z = x - y;+  return z < 0n ? 0n : z; };  // Floating-point numbers@@ -192,11 +185,11 @@   // These WORD64 values were obtained via `castDoubleToWord64` in Haskell:-const WORD64_NAN      = exports.primIntegerFromString("18444492273895866368");-const WORD64_POS_INF  = exports.primIntegerFromString("9218868437227405312");-const WORD64_NEG_INF  = exports.primIntegerFromString("18442240474082181120");-const WORD64_POS_ZERO = exports.primIntegerFromString("0");-const WORD64_NEG_ZERO = exports.primIntegerFromString("9223372036854775808");+const WORD64_NAN      = 18444492273895866368n;+const WORD64_POS_INF  = 9218868437227405312n;+const WORD64_NEG_INF  = 18442240474082181120n;+const WORD64_POS_ZERO = 0n;+const WORD64_NEG_ZERO = 9223372036854775808n;  exports.primFloatToWord64 = function(x) {     if (exports.primFloatIsNaN(x)) {@@ -223,32 +216,33 @@         sign = (sign === -1 ? "1" : "0");         mantissa = (mantissa.toString(2)).padStart(11, "0");         exponent = (mantissa.toString(2)).padStart(52, "0");-        return exports.primIntegerFromString(parseInt(-            sign + mantissa + exponent, 2).toString());+        return BigInt(parseInt(sign + mantissa + exponent, 2));     } }; -exports.primNatToFloat = function(x) {-    return x.valueOf();-};-exports.primIntToFloat = function(x) {-    return x.valueOf();-};-exports.primRatioToFloat = function(x) {-    return function(y) {-        return x.valueOf() / y.valueOf();-    };-};-exports.uprimFloatEncode = function(x, y) {-    var mantissa = x.valueOf();-    var exponent = y.valueOf();-    if (Number.isSafeInteger(mantissa) && -1024 <= exponent && exponent <= 1024) {-        return mantissa * (2 ** exponent);-    }-    else {-        return null;-    }+// primNatToFloat : Nat -> Float+exports.primNatToFloat = Number;++// primIntToFloat : Int -> Float+exports.primIntToFloat = Number;++// primRatioToFloat : Int -> Int -> Float+exports.primRatioToFloat = x => y => Number(x) / Number(y);++// uprimFloatEncode : (Int, Int) -> Maybe Float+exports.uprimFloatEncode = (x, y) => {+  const mantissa = Number(x);+  const exponent = Number(y);++  if (Number.isSafeInteger(mantissa) && -1024 <= exponent && exponent <= 1024) {+    return mantissa * (2 ** exponent);+  }++  else {+    return null;+  } };+ exports.primShowFloat = function(x) {     // See Issue #2192.     if (Number.isInteger(x)) {@@ -340,32 +334,44 @@     return Math.atanh(x); }; +// Cubical primitives.+exports.primIMin = x => y => x && y;+exports.primIMax = x => y => x || y;+exports.primINeg = x => !x;+exports.primPartial = _ => _ => x => x;+exports.primPartialP = _ => _ => x => x;+exports.primPOr = _ => i => _ => _ => x => y => i ? x : y;+exports.primComp = _ => _ => _ => _ => x => x;+exports.primTransp = _ => _ => _ => x => x;+exports.primHComp = _ => _ => _ => _ => x => x;+exports.primSubOut = _ => _ => _ => _ => x => x;+exports.prim_glueU = _ => _ => _ => _ => _ => x => x;+exports.prim_unglueU = _ => _ => _ => _ => x => x;+exports.primFaceForall = f => f(true) == true && f(false) == false;+exports.primDepIMin =+    i => f => i ? f({ "tt" : a => a["tt"]() }) : false;+exports.primIdFace = _ => _ => _ => _ => x => x["i"];+exports.primIdPath = _ => _ => _ => _ => x => x["p"];+exports.primIdJ = _ => _ => _ => _ => _ => x => _ => _ => x;+exports.primIdElim =+    _ => _ => _ => _ => _ => f => x => y => f(y["i"])(x)(y["p"]);+ // Other stuff-exports.primSeq = function(x, y) {-  return y;-};-exports.uprimQNameEquality = function(x,y) {-    return x["id"].compare(y["id"]) == 0 && x["moduleId"].compare(y["moduleId"]) == 0;-};-exports.primQNameEquality = function(x) {-    return function(y) {-        return exports.uprimQNameEquality(x, y);-    };-};-exports.primQNameLess = function(x) {-  return function(y) {-    switch (x["id"].compare(y["id"])) {-      case -1: return true;-      case  1: return false;-      default: return x["moduleId"].compare(y["moduleId"]) == -1;-    };-  };-};-exports.primShowQName = function(x) {-    return x["name"];-};-exports.primQNameFixity = function(x) {-    return x["fixity"];-}; +// primSeq : (X, Y) -> Y+exports.primSeq = (x, y) => y; +// uprimQNameEquality : (Name, Name) -> Bool+exports.uprimQNameEquality = (x, y) => x['id'] === y['id'] && x['moduleId'] === y['moduleId'];++// primQNameEquality : Name -> Name -> Bool+exports.primQNameEquality = x => y => exports.uprimQNameEquality(x, y);++// primQNameLess : Name -> Name -> Bool+exports.primQNameLess = x => y => x['id'] === y['id'] ? x['moduleId'] < y['moduleId'] : x['id'] < y['id'];++// primShowQName : Name -> String+exports.primShowQName = x => x['name'];++// primQNameFixity : Name -> Fixity+exports.primQNameFixity = x => x['fixity'];

@@ -1,1620 +0,0 @@-/*-	JavaScript BigInteger library version 0.9.1-	http://silentmatt.com/biginteger/--	Copyright (c) 2009 Matthew Crumley <email@matthewcrumley.com>-	Copyright (c) 2010,2011 by John Tobey <John.Tobey@gmail.com>-	Licensed under the MIT license.--	Support for arbitrary internal representation base was added by-	Vitaly Magerya.-*/--/*-	File: biginteger.js--	Exports:--		<BigInteger>-*/-(function(exports) {-"use strict";-/*-	Class: BigInteger-	An arbitrarily-large integer.--	<BigInteger> objects should be considered immutable. None of the "built-in"-	methods modify *this* or their arguments. All properties should be-	considered private.--	All the methods of <BigInteger> instances can be called "statically". The-	static versions are convenient if you don't already have a <BigInteger>-	object.--	As an example, these calls are equivalent.--	> BigInteger(4).multiply(5); // returns BigInteger(20);-	> BigInteger.multiply(4, 5); // returns BigInteger(20);--	> var a = 42;-	> var a = BigInteger.toJSValue("0b101010"); // Not completely useless...-*/--var CONSTRUCT = {}; // Unique token to call "private" version of constructor--/*-	Constructor: BigInteger()-	Convert a value to a <BigInteger>.--	Although <BigInteger()> is the constructor for <BigInteger> objects, it is-	best not to call it as a constructor. If *n* is a <BigInteger> object, it is-	simply returned as-is. Otherwise, <BigInteger()> is equivalent to <parse>-	without a radix argument.--	> var n0 = BigInteger();      // Same as <BigInteger.ZERO>-	> var n1 = BigInteger("123"); // Create a new <BigInteger> with value 123-	> var n2 = BigInteger(123);   // Create a new <BigInteger> with value 123-	> var n3 = BigInteger(n2);    // Return n2, unchanged--	The constructor form only takes an array and a sign. *n* must be an-	array of numbers in little-endian order, where each digit is between 0-	and BigInteger.base.  The second parameter sets the sign: -1 for-	negative, +1 for positive, or 0 for zero. The array is *not copied and-	may be modified*. If the array contains only zeros, the sign parameter-	is ignored and is forced to zero.--	> new BigInteger([5], -1): create a new BigInteger with value -5--	Parameters:--		n - Value to convert to a <BigInteger>.--	Returns:--		A <BigInteger> value.--	See Also:--		<parse>, <BigInteger>-*/-function BigInteger(n, s, token) {-	if (token !== CONSTRUCT) {-		if (n instanceof BigInteger) {-			return n;-		}-		else if (typeof n === "undefined") {-			return ZERO;-		}-		return BigInteger.parse(n);-	}--	n = n || [];  // Provide the nullary constructor for subclasses.-	while (n.length && !n[n.length - 1]) {-		--n.length;-	}-	this._d = n;-	this._s = n.length ? (s || 1) : 0;-}--BigInteger._construct = function(n, s) {-	return new BigInteger(n, s, CONSTRUCT);-};--// Base-10 speedup hacks in parse, toString, exp10 and log functions-// require base to be a power of 10. 10^7 is the largest such power-// that won't cause a precision loss when digits are multiplied.-var BigInteger_base = 10000000;-var BigInteger_base_log10 = 7;--BigInteger.base = BigInteger_base;-BigInteger.base_log10 = BigInteger_base_log10;--var ZERO = new BigInteger([], 0, CONSTRUCT);-// Constant: ZERO-// <BigInteger> 0.-BigInteger.ZERO = ZERO;--var ONE = new BigInteger([1], 1, CONSTRUCT);-// Constant: ONE-// <BigInteger> 1.-BigInteger.ONE = ONE;--var M_ONE = new BigInteger(ONE._d, -1, CONSTRUCT);-// Constant: M_ONE-// <BigInteger> -1.-BigInteger.M_ONE = M_ONE;--// Constant: _0-// Shortcut for <ZERO>.-BigInteger._0 = ZERO;--// Constant: _1-// Shortcut for <ONE>.-BigInteger._1 = ONE;--/*-	Constant: small-	Array of <BigIntegers> from 0 to 36.--	These are used internally for parsing, but useful when you need a "small"-	<BigInteger>.--	See Also:--		<ZERO>, <ONE>, <_0>, <_1>-*/-BigInteger.small = [-	ZERO,-	ONE,-	/* Assuming BigInteger_base > 36 */-	new BigInteger( [2], 1, CONSTRUCT),-	new BigInteger( [3], 1, CONSTRUCT),-	new BigInteger( [4], 1, CONSTRUCT),-	new BigInteger( [5], 1, CONSTRUCT),-	new BigInteger( [6], 1, CONSTRUCT),-	new BigInteger( [7], 1, CONSTRUCT),-	new BigInteger( [8], 1, CONSTRUCT),-	new BigInteger( [9], 1, CONSTRUCT),-	new BigInteger([10], 1, CONSTRUCT),-	new BigInteger([11], 1, CONSTRUCT),-	new BigInteger([12], 1, CONSTRUCT),-	new BigInteger([13], 1, CONSTRUCT),-	new BigInteger([14], 1, CONSTRUCT),-	new BigInteger([15], 1, CONSTRUCT),-	new BigInteger([16], 1, CONSTRUCT),-	new BigInteger([17], 1, CONSTRUCT),-	new BigInteger([18], 1, CONSTRUCT),-	new BigInteger([19], 1, CONSTRUCT),-	new BigInteger([20], 1, CONSTRUCT),-	new BigInteger([21], 1, CONSTRUCT),-	new BigInteger([22], 1, CONSTRUCT),-	new BigInteger([23], 1, CONSTRUCT),-	new BigInteger([24], 1, CONSTRUCT),-	new BigInteger([25], 1, CONSTRUCT),-	new BigInteger([26], 1, CONSTRUCT),-	new BigInteger([27], 1, CONSTRUCT),-	new BigInteger([28], 1, CONSTRUCT),-	new BigInteger([29], 1, CONSTRUCT),-	new BigInteger([30], 1, CONSTRUCT),-	new BigInteger([31], 1, CONSTRUCT),-	new BigInteger([32], 1, CONSTRUCT),-	new BigInteger([33], 1, CONSTRUCT),-	new BigInteger([34], 1, CONSTRUCT),-	new BigInteger([35], 1, CONSTRUCT),-	new BigInteger([36], 1, CONSTRUCT)-];--// Used for parsing/radix conversion-BigInteger.digits = "0123456789ABCDEFGHIJKLMNOPQRSTUVWXYZ".split("");--/*-	Method: toString-	Convert a <BigInteger> to a string.--	When *base* is greater than 10, letters are upper case.--	Parameters:--		base - Optional base to represent the number in (default is base 10).-		       Must be between 2 and 36 inclusive, or an Error will be thrown.--	Returns:--		The string representation of the <BigInteger>.-*/-BigInteger.prototype.toString = function(base) {-	base = +base || 10;-	if (base < 2 || base > 36) {-		throw new Error("illegal radix " + base + ".");-	}-	if (this._s === 0) {-		return "0";-	}-	if (base === 10) {-		var str = this._s < 0 ? "-" : "";-		str += this._d[this._d.length - 1].toString();-		for (var i = this._d.length - 2; i >= 0; i--) {-			var group = this._d[i].toString();-			while (group.length < BigInteger_base_log10) group = '0' + group;-			str += group;-		}-		return str;-	}-	else {-		var numerals = BigInteger.digits;-		base = BigInteger.small[base];-		var sign = this._s;--		var n = this.abs();-		var digits = [];-		var digit;--		while (n._s !== 0) {-			var divmod = n.divRem(base);-			n = divmod[0];-			digit = divmod[1];-			// TODO: This could be changed to unshift instead of reversing at the end.-			// Benchmark both to compare speeds.-			digits.push(numerals[digit.valueOf()]);-		}-		return (sign < 0 ? "-" : "") + digits.reverse().join("");-	}-};--// Verify strings for parsing-BigInteger.radixRegex = [-	/^$/,-	/^$/,-	/^[01]*$/,-	/^[012]*$/,-	/^[0-3]*$/,-	/^[0-4]*$/,-	/^[0-5]*$/,-	/^[0-6]*$/,-	/^[0-7]*$/,-	/^[0-8]*$/,-	/^[0-9]*$/,-	/^[0-9aA]*$/,-	/^[0-9abAB]*$/,-	/^[0-9abcABC]*$/,-	/^[0-9a-dA-D]*$/,-	/^[0-9a-eA-E]*$/,-	/^[0-9a-fA-F]*$/,-	/^[0-9a-gA-G]*$/,-	/^[0-9a-hA-H]*$/,-	/^[0-9a-iA-I]*$/,-	/^[0-9a-jA-J]*$/,-	/^[0-9a-kA-K]*$/,-	/^[0-9a-lA-L]*$/,-	/^[0-9a-mA-M]*$/,-	/^[0-9a-nA-N]*$/,-	/^[0-9a-oA-O]*$/,-	/^[0-9a-pA-P]*$/,-	/^[0-9a-qA-Q]*$/,-	/^[0-9a-rA-R]*$/,-	/^[0-9a-sA-S]*$/,-	/^[0-9a-tA-T]*$/,-	/^[0-9a-uA-U]*$/,-	/^[0-9a-vA-V]*$/,-	/^[0-9a-wA-W]*$/,-	/^[0-9a-xA-X]*$/,-	/^[0-9a-yA-Y]*$/,-	/^[0-9a-zA-Z]*$/-];--/*-	Function: parse-	Parse a string into a <BigInteger>.--	*base* is optional but, if provided, must be from 2 to 36 inclusive. If-	*base* is not provided, it will be guessed based on the leading characters-	of *s* as follows:--	- "0x" or "0X": *base* = 16-	- "0c" or "0C": *base* = 8-	- "0b" or "0B": *base* = 2-	- else: *base* = 10--	If no base is provided, or *base* is 10, the number can be in exponential-	form. For example, these are all valid:--	> BigInteger.parse("1e9");              // Same as "1000000000"-	> BigInteger.parse("1.234*10^3");       // Same as 1234-	> BigInteger.parse("56789 * 10 ** -2"); // Same as 567--	If any characters fall outside the range defined by the radix, an exception-	will be thrown.--	Parameters:--		s - The string to parse.-		base - Optional radix (default is to guess based on *s*).--	Returns:--		a <BigInteger> instance.-*/-BigInteger.parse = function(s, base) {-	// Expands a number in exponential form to decimal form.-	// expandExponential("-13.441*10^5") === "1344100";-	// expandExponential("1.12300e-1") === "0.112300";-	// expandExponential(1000000000000000000000000000000) === "1000000000000000000000000000000";-	function expandExponential(str) {-		str = str.replace(/\s*[*xX]\s*10\s*(\^|\*\*)\s*/, "e");--		return str.replace(/^([+\-])?(\d+)\.?(\d*)[eE]([+\-]?\d+)$/, function(x, s, n, f, c) {-			c = +c;-			var l = c < 0;-			var i = n.length + c;-			x = (l ? n : f).length;-			c = ((c = Math.abs(c)) >= x ? c - x + l : 0);-			var z = (new Array(c + 1)).join("0");-			var r = n + f;-			return (s || "") + (l ? r = z + r : r += z).substr(0, i += l ? z.length : 0) + (i < r.length ? "." + r.substr(i) : "");-		});-	}--	s = s.toString();-	if (typeof base === "undefined" || +base === 10) {-		s = expandExponential(s);-	}--	var prefixRE;-	if (typeof base === "undefined") {-		prefixRE = '0[xcb]';-	}-	else if (base == 16) {-		prefixRE = '0x';-	}-	else if (base == 8) {-		prefixRE = '0c';-	}-	else if (base == 2) {-		prefixRE = '0b';-	}-	else {-		prefixRE = '';-	}-	var parts = new RegExp('^([+\\-]?)(' + prefixRE + ')?([0-9a-z]*)(?:\\.\\d*)?$', 'i').exec(s);-	if (parts) {-		var sign = parts[1] || "+";-		var baseSection = parts[2] || "";-		var digits = parts[3] || "";--		if (typeof base === "undefined") {-			// Guess base-			if (baseSection === "0x" || baseSection === "0X") { // Hex-				base = 16;-			}-			else if (baseSection === "0c" || baseSection === "0C") { // Octal-				base = 8;-			}-			else if (baseSection === "0b" || baseSection === "0B") { // Binary-				base = 2;-			}-			else {-				base = 10;-			}-		}-		else if (base < 2 || base > 36) {-			throw new Error("Illegal radix " + base + ".");-		}--		base = +base;--		// Check for digits outside the range-		if (!(BigInteger.radixRegex[base].test(digits))) {-			throw new Error("Bad digit for radix " + base);-		}--		// Strip leading zeros, and convert to array-		digits = digits.replace(/^0+/, "").split("");-		if (digits.length === 0) {-			return ZERO;-		}--		// Get the sign (we know it's not zero)-		sign = (sign === "-") ? -1 : 1;--		// Optimize 10-		if (base == 10) {-			var d = [];-			while (digits.length >= BigInteger_base_log10) {-				d.push(parseInt(digits.splice(digits.length-BigInteger.base_log10, BigInteger.base_log10).join(''), 10));-			}-			d.push(parseInt(digits.join(''), 10));-			return new BigInteger(d, sign, CONSTRUCT);-		}--		// Do the conversion-		var d = ZERO;-		base = BigInteger.small[base];-		var small = BigInteger.small;-		for (var i = 0; i < digits.length; i++) {-			d = d.multiply(base).add(small[parseInt(digits[i], 36)]);-		}-		return new BigInteger(d._d, sign, CONSTRUCT);-	}-	else {-		throw new Error("Invalid BigInteger format: " + s);-	}-};--/*-	Function: add-	Add two <BigIntegers>.--	Parameters:--		n - The number to add to *this*. Will be converted to a <BigInteger>.--	Returns:--		The numbers added together.--	See Also:--		<subtract>, <multiply>, <quotient>, <next>-*/-BigInteger.prototype.add = function(n) {-	if (this._s === 0) {-		return BigInteger(n);-	}--	n = BigInteger(n);-	if (n._s === 0) {-		return this;-	}-	if (this._s !== n._s) {-		n = n.negate();-		return this.subtract(n);-	}--	var a = this._d;-	var b = n._d;-	var al = a.length;-	var bl = b.length;-	var sum = new Array(Math.max(al, bl) + 1);-	var size = Math.min(al, bl);-	var carry = 0;-	var digit;--	for (var i = 0; i < size; i++) {-		digit = a[i] + b[i] + carry;-		sum[i] = digit % BigInteger_base;-		carry = (digit / BigInteger_base) | 0;-	}-	if (bl > al) {-		a = b;-		al = bl;-	}-	for (i = size; carry && i < al; i++) {-		digit = a[i] + carry;-		sum[i] = digit % BigInteger_base;-		carry = (digit / BigInteger_base) | 0;-	}-	if (carry) {-		sum[i] = carry;-	}--	for ( ; i < al; i++) {-		sum[i] = a[i];-	}--	return new BigInteger(sum, this._s, CONSTRUCT);-};--/*-	Function: negate-	Get the additive inverse of a <BigInteger>.--	Returns:--		A <BigInteger> with the same magnatude, but with the opposite sign.--	See Also:--		<abs>-*/-BigInteger.prototype.negate = function() {-	return new BigInteger(this._d, (-this._s) | 0, CONSTRUCT);-};--/*-	Function: abs-	Get the absolute value of a <BigInteger>.--	Returns:--		A <BigInteger> with the same magnatude, but always positive (or zero).--	See Also:--		<negate>-*/-BigInteger.prototype.abs = function() {-	return (this._s < 0) ? this.negate() : this;-};--/*-	Function: subtract-	Subtract two <BigIntegers>.--	Parameters:--		n - The number to subtract from *this*. Will be converted to a <BigInteger>.--	Returns:--		The *n* subtracted from *this*.--	See Also:--		<add>, <multiply>, <quotient>, <prev>-*/-BigInteger.prototype.subtract = function(n) {-	if (this._s === 0) {-		return BigInteger(n).negate();-	}--	n = BigInteger(n);-	if (n._s === 0) {-		return this;-	}-	if (this._s !== n._s) {-		n = n.negate();-		return this.add(n);-	}--	var m = this;-	// negative - negative => -|a| - -|b| => -|a| + |b| => |b| - |a|-	if (this._s < 0) {-		m = new BigInteger(n._d, 1, CONSTRUCT);-		n = new BigInteger(this._d, 1, CONSTRUCT);-	}--	// Both are positive => a - b-	var sign = m.compareAbs(n);-	if (sign === 0) {-		return ZERO;-	}-	else if (sign < 0) {-		// swap m and n-		var t = n;-		n = m;-		m = t;-	}--	// a > b-	var a = m._d;-	var b = n._d;-	var al = a.length;-	var bl = b.length;-	var diff = new Array(al); // al >= bl since a > b-	var borrow = 0;-	var i;-	var digit;--	for (i = 0; i < bl; i++) {-		digit = a[i] - borrow - b[i];-		if (digit < 0) {-			digit += BigInteger_base;-			borrow = 1;-		}-		else {-			borrow = 0;-		}-		diff[i] = digit;-	}-	for (i = bl; i < al; i++) {-		digit = a[i] - borrow;-		if (digit < 0) {-			digit += BigInteger_base;-		}-		else {-			diff[i++] = digit;-			break;-		}-		diff[i] = digit;-	}-	for ( ; i < al; i++) {-		diff[i] = a[i];-	}--	return new BigInteger(diff, sign, CONSTRUCT);-};--(function() {-	function addOne(n, sign) {-		var a = n._d;-		var sum = a.slice();-		var carry = true;-		var i = 0;--		while (true) {-			var digit = (a[i] || 0) + 1;-			sum[i] = digit % BigInteger_base;-			if (digit <= BigInteger_base - 1) {-				break;-			}-			++i;-		}--		return new BigInteger(sum, sign, CONSTRUCT);-	}--	function subtractOne(n, sign) {-		var a = n._d;-		var sum = a.slice();-		var borrow = true;-		var i = 0;--		while (true) {-			var digit = (a[i] || 0) - 1;-			if (digit < 0) {-				sum[i] = digit + BigInteger_base;-			}-			else {-				sum[i] = digit;-				break;-			}-			++i;-		}--		return new BigInteger(sum, sign, CONSTRUCT);-	}--	/*-		Function: next-		Get the next <BigInteger> (add one).--		Returns:--			*this* + 1.--		See Also:--			<add>, <prev>-	*/-	BigInteger.prototype.next = function() {-		switch (this._s) {-		case 0:-			return ONE;-		case -1:-			return subtractOne(this, -1);-		// case 1:-		default:-			return addOne(this, 1);-		}-	};--	/*-		Function: prev-		Get the previous <BigInteger> (subtract one).--		Returns:--			*this* - 1.--		See Also:--			<next>, <subtract>-	*/-	BigInteger.prototype.prev = function() {-		switch (this._s) {-		case 0:-			return M_ONE;-		case -1:-			return addOne(this, -1);-		// case 1:-		default:-			return subtractOne(this, 1);-		}-	};-})();--/*-	Function: compareAbs-	Compare the absolute value of two <BigIntegers>.--	Calling <compareAbs> is faster than calling <abs> twice, then <compare>.--	Parameters:--		n - The number to compare to *this*. Will be converted to a <BigInteger>.--	Returns:--		-1, 0, or +1 if *|this|* is less than, equal to, or greater than *|n|*.--	See Also:--		<compare>, <abs>-*/-BigInteger.prototype.compareAbs = function(n) {-	if (this === n) {-		return 0;-	}--	if (!(n instanceof BigInteger)) {-		if (!isFinite(n)) {-			return(isNaN(n) ? n : -1);-		}-		n = BigInteger(n);-	}--	if (this._s === 0) {-		return (n._s !== 0) ? -1 : 0;-	}-	if (n._s === 0) {-		return 1;-	}--	var l = this._d.length;-	var nl = n._d.length;-	if (l < nl) {-		return -1;-	}-	else if (l > nl) {-		return 1;-	}--	var a = this._d;-	var b = n._d;-	for (var i = l-1; i >= 0; i--) {-		if (a[i] !== b[i]) {-			return a[i] < b[i] ? -1 : 1;-		}-	}--	return 0;-};--/*-	Function: compare-	Compare two <BigIntegers>.--	Parameters:--		n - The number to compare to *this*. Will be converted to a <BigInteger>.--	Returns:--		-1, 0, or +1 if *this* is less than, equal to, or greater than *n*.--	See Also:--		<compareAbs>, <isPositive>, <isNegative>, <isUnit>-*/-BigInteger.prototype.compare = function(n) {-	if (this === n) {-		return 0;-	}--	n = BigInteger(n);--	if (this._s === 0) {-		return -n._s;-	}--	if (this._s === n._s) { // both positive or both negative-		var cmp = this.compareAbs(n);-		return cmp * this._s;-	}-	else {-		return this._s;-	}-};--/*-	Function: isUnit-	Return true iff *this* is either 1 or -1.--	Returns:--		true if *this* compares equal to <BigInteger.ONE> or <BigInteger.M_ONE>.--	See Also:--		<isZero>, <isNegative>, <isPositive>, <compareAbs>, <compare>,-		<BigInteger.ONE>, <BigInteger.M_ONE>-*/-BigInteger.prototype.isUnit = function() {-	return this === ONE ||-		this === M_ONE ||-		(this._d.length === 1 && this._d[0] === 1);-};--/*-	Function: multiply-	Multiply two <BigIntegers>.--	Parameters:--		n - The number to multiply *this* by. Will be converted to a-		<BigInteger>.--	Returns:--		The numbers multiplied together.--	See Also:--		<add>, <subtract>, <quotient>, <square>-*/-BigInteger.prototype.multiply = function(n) {-	// TODO: Consider adding Karatsuba multiplication for large numbers-	if (this._s === 0) {-		return ZERO;-	}--	n = BigInteger(n);-	if (n._s === 0) {-		return ZERO;-	}-	if (this.isUnit()) {-		if (this._s < 0) {-			return n.negate();-		}-		return n;-	}-	if (n.isUnit()) {-		if (n._s < 0) {-			return this.negate();-		}-		return this;-	}-	if (this === n) {-		return this.square();-	}--	var r = (this._d.length >= n._d.length);-	var a = (r ? this : n)._d; // a will be longer than b-	var b = (r ? n : this)._d;-	var al = a.length;-	var bl = b.length;--	var pl = al + bl;-	var partial = new Array(pl);-	var i;-	for (i = 0; i < pl; i++) {-		partial[i] = 0;-	}--	for (i = 0; i < bl; i++) {-		var carry = 0;-		var bi = b[i];-		var jlimit = al + i;-		var digit;-		for (var j = i; j < jlimit; j++) {-			digit = partial[j] + bi * a[j - i] + carry;-			carry = (digit / BigInteger_base) | 0;-			partial[j] = (digit % BigInteger_base) | 0;-		}-		if (carry) {-			digit = partial[j] + carry;-			carry = (digit / BigInteger_base) | 0;-			partial[j] = digit % BigInteger_base;-		}-	}-	return new BigInteger(partial, this._s * n._s, CONSTRUCT);-};--// Multiply a BigInteger by a single-digit native number-// Assumes that this and n are >= 0-// This is not really intended to be used outside the library itself-BigInteger.prototype.multiplySingleDigit = function(n) {-	if (n === 0 || this._s === 0) {-		return ZERO;-	}-	if (n === 1) {-		return this;-	}--	var digit;-	if (this._d.length === 1) {-		digit = this._d[0] * n;-		if (digit >= BigInteger_base) {-			return new BigInteger([(digit % BigInteger_base)|0,-					(digit / BigInteger_base)|0], 1, CONSTRUCT);-		}-		return new BigInteger([digit], 1, CONSTRUCT);-	}--	if (n === 2) {-		return this.add(this);-	}-	if (this.isUnit()) {-		return new BigInteger([n], 1, CONSTRUCT);-	}--	var a = this._d;-	var al = a.length;--	var pl = al + 1;-	var partial = new Array(pl);-	for (var i = 0; i < pl; i++) {-		partial[i] = 0;-	}--	var carry = 0;-	for (var j = 0; j < al; j++) {-		digit = n * a[j] + carry;-		carry = (digit / BigInteger_base) | 0;-		partial[j] = (digit % BigInteger_base) | 0;-	}-	if (carry) {-		partial[j] = carry;-	}--	return new BigInteger(partial, 1, CONSTRUCT);-};--/*-	Function: square-	Multiply a <BigInteger> by itself.--	This is slightly faster than regular multiplication, since it removes the-	duplicated multiplcations.--	Returns:--		> this.multiply(this)--	See Also:-		<multiply>-*/-BigInteger.prototype.square = function() {-	// Normally, squaring a 10-digit number would take 100 multiplications.-	// Of these 10 are unique diagonals, of the remaining 90 (100-10), 45 are repeated.-	// This procedure saves (N*(N-1))/2 multiplications, (e.g., 45 of 100 multiplies).-	// Based on code by Gary Darby, Intellitech Systems Inc., www.DelphiForFun.org--	if (this._s === 0) {-		return ZERO;-	}-	if (this.isUnit()) {-		return ONE;-	}--	var digits = this._d;-	var length = digits.length;-	var imult1 = new Array(length + length + 1);-	var product, carry, k;-	var i;--	// Calculate diagonal-	for (i = 0; i < length; i++) {-		k = i * 2;-		product = digits[i] * digits[i];-		carry = (product / BigInteger_base) | 0;-		imult1[k] = product % BigInteger_base;-		imult1[k + 1] = carry;-	}--	// Calculate repeating part-	for (i = 0; i < length; i++) {-		carry = 0;-		k = i * 2 + 1;-		for (var j = i + 1; j < length; j++, k++) {-			product = digits[j] * digits[i] * 2 + imult1[k] + carry;-			carry = (product / BigInteger_base) | 0;-			imult1[k] = product % BigInteger_base;-		}-		k = length + i;-		var digit = carry + imult1[k];-		carry = (digit / BigInteger_base) | 0;-		imult1[k] = digit % BigInteger_base;-		imult1[k + 1] += carry;-	}--	return new BigInteger(imult1, 1, CONSTRUCT);-};--/*-	Function: quotient-	Divide two <BigIntegers> and truncate towards zero.--	<quotient> throws an exception if *n* is zero.--	Parameters:--		n - The number to divide *this* by. Will be converted to a <BigInteger>.--	Returns:--		The *this* / *n*, truncated to an integer.--	See Also:--		<add>, <subtract>, <multiply>, <divRem>, <remainder>-*/-BigInteger.prototype.quotient = function(n) {-	return this.divRem(n)[0];-};--/*-	Function: divide-	Deprecated synonym for <quotient>.-*/-BigInteger.prototype.divide = BigInteger.prototype.quotient;--/*-	Function: remainder-	Calculate the remainder of two <BigIntegers>.--	<remainder> throws an exception if *n* is zero.--	Parameters:--		n - The remainder after *this* is divided *this* by *n*. Will be-		    converted to a <BigInteger>.--	Returns:--		*this* % *n*.--	See Also:--		<divRem>, <quotient>-*/-BigInteger.prototype.remainder = function(n) {-	return this.divRem(n)[1];-};--/*-	Function: divRem-	Calculate the integer quotient and remainder of two <BigIntegers>.--	<divRem> throws an exception if *n* is zero.--	Parameters:--		n - The number to divide *this* by. Will be converted to a <BigInteger>.--	Returns:--		A two-element array containing the quotient and the remainder.--		> a.divRem(b)--		is exactly equivalent to--		> [a.quotient(b), a.remainder(b)]--		except it is faster, because they are calculated at the same time.--	See Also:--		<quotient>, <remainder>-*/-BigInteger.prototype.divRem = function(n) {-	n = BigInteger(n);-	if (n._s === 0) {-		throw new Error("Divide by zero");-	}-	if (this._s === 0) {-		return [ZERO, ZERO];-	}-	if (n._d.length === 1) {-		return this.divRemSmall(n._s * n._d[0]);-	}--	// Test for easy cases -- |n1| <= |n2|-	switch (this.compareAbs(n)) {-	case 0: // n1 == n2-		return [this._s === n._s ? ONE : M_ONE, ZERO];-	case -1: // |n1| < |n2|-		return [ZERO, this];-	}--	var sign = this._s * n._s;-	var a = n.abs();-	var b_digits = this._d;-	var b_index = b_digits.length;-	var digits = n._d.length;-	var quot = [];-	var guess;--	var part = new BigInteger([], 0, CONSTRUCT);--	while (b_index) {-		part._d.unshift(b_digits[--b_index]);-		part = new BigInteger(part._d, 1, CONSTRUCT);--		if (part.compareAbs(n) < 0) {-			quot.push(0);-			continue;-		}-		if (part._s === 0) {-			guess = 0;-		}-		else {-			var xlen = part._d.length, ylen = a._d.length;-			var highx = part._d[xlen-1]*BigInteger_base + part._d[xlen-2];-			var highy = a._d[ylen-1]*BigInteger_base + a._d[ylen-2];-			if (part._d.length > a._d.length) {-				// The length of part._d can either match a._d length,-				// or exceed it by one.-				highx = (highx+1)*BigInteger_base;-			}-			guess = Math.ceil(highx/highy);-		}-		do {-			var check = a.multiplySingleDigit(guess);-			if (check.compareAbs(part) <= 0) {-				break;-			}-			guess--;-		} while (guess);--		quot.push(guess);-		if (!guess) {-			continue;-		}-		var diff = part.subtract(check);-		part._d = diff._d.slice();-	}--	return [new BigInteger(quot.reverse(), sign, CONSTRUCT),-		   new BigInteger(part._d, this._s, CONSTRUCT)];-};--// Throws an exception if n is outside of (-BigInteger.base, -1] or-// [1, BigInteger.base).  It's not necessary to call this, since the-// other division functions will call it if they are able to.-BigInteger.prototype.divRemSmall = function(n) {-	var r;-	n = +n;-	if (n === 0) {-		throw new Error("Divide by zero");-	}--	var n_s = n < 0 ? -1 : 1;-	var sign = this._s * n_s;-	n = Math.abs(n);--	if (n < 1 || n >= BigInteger_base) {-		throw new Error("Argument out of range");-	}--	if (this._s === 0) {-		return [ZERO, ZERO];-	}--	if (n === 1 || n === -1) {-		return [(sign === 1) ? this.abs() : new BigInteger(this._d, sign, CONSTRUCT), ZERO];-	}--	// 2 <= n < BigInteger_base--	// divide a single digit by a single digit-	if (this._d.length === 1) {-		var q = new BigInteger([(this._d[0] / n) | 0], 1, CONSTRUCT);-		r = new BigInteger([(this._d[0] % n) | 0], 1, CONSTRUCT);-		if (sign < 0) {-			q = q.negate();-		}-		if (this._s < 0) {-			r = r.negate();-		}-		return [q, r];-	}--	var digits = this._d.slice();-	var quot = new Array(digits.length);-	var part = 0;-	var diff = 0;-	var i = 0;-	var guess;--	while (digits.length) {-		part = part * BigInteger_base + digits[digits.length - 1];-		if (part < n) {-			quot[i++] = 0;-			digits.pop();-			diff = BigInteger_base * diff + part;-			continue;-		}-		if (part === 0) {-			guess = 0;-		}-		else {-			guess = (part / n) | 0;-		}--		var check = n * guess;-		diff = part - check;-		quot[i++] = guess;-		if (!guess) {-			digits.pop();-			continue;-		}--		digits.pop();-		part = diff;-	}--	r = new BigInteger([diff], 1, CONSTRUCT);-	if (this._s < 0) {-		r = r.negate();-	}-	return [new BigInteger(quot.reverse(), sign, CONSTRUCT), r];-};--/*-	Function: isEven-	Return true iff *this* is divisible by two.--	Note that <BigInteger.ZERO> is even.--	Returns:--		true if *this* is even, false otherwise.--	See Also:--		<isOdd>-*/-BigInteger.prototype.isEven = function() {-	var digits = this._d;-	return this._s === 0 || digits.length === 0 || (digits[0] % 2) === 0;-};--/*-	Function: isOdd-	Return true iff *this* is not divisible by two.--	Returns:--		true if *this* is odd, false otherwise.--	See Also:--		<isEven>-*/-BigInteger.prototype.isOdd = function() {-	return !this.isEven();-};--/*-	Function: sign-	Get the sign of a <BigInteger>.--	Returns:--		* -1 if *this* < 0-		* 0 if *this* == 0-		* +1 if *this* > 0--	See Also:--		<isZero>, <isPositive>, <isNegative>, <compare>, <BigInteger.ZERO>-*/-BigInteger.prototype.sign = function() {-	return this._s;-};--/*-	Function: isPositive-	Return true iff *this* > 0.--	Returns:--		true if *this*.compare(<BigInteger.ZERO>) == 1.--	See Also:--		<sign>, <isZero>, <isNegative>, <isUnit>, <compare>, <BigInteger.ZERO>-*/-BigInteger.prototype.isPositive = function() {-	return this._s > 0;-};--/*-	Function: isNegative-	Return true iff *this* < 0.--	Returns:--		true if *this*.compare(<BigInteger.ZERO>) == -1.--	See Also:--		<sign>, <isPositive>, <isZero>, <isUnit>, <compare>, <BigInteger.ZERO>-*/-BigInteger.prototype.isNegative = function() {-	return this._s < 0;-};--/*-	Function: isZero-	Return true iff *this* == 0.--	Returns:--		true if *this*.compare(<BigInteger.ZERO>) == 0.--	See Also:--		<sign>, <isPositive>, <isNegative>, <isUnit>, <BigInteger.ZERO>-*/-BigInteger.prototype.isZero = function() {-	return this._s === 0;-};--/*-	Function: exp10-	Multiply a <BigInteger> by a power of 10.--	This is equivalent to, but faster than--	> if (n >= 0) {-	>     return this.multiply(BigInteger("1e" + n));-	> }-	> else { // n <= 0-	>     return this.quotient(BigInteger("1e" + -n));-	> }--	Parameters:--		n - The power of 10 to multiply *this* by. *n* is converted to a-		javascipt number and must be no greater than <BigInteger.MAX_EXP>-		(0x7FFFFFFF), or an exception will be thrown.--	Returns:--		*this* * (10 ** *n*), truncated to an integer if necessary.--	See Also:--		<pow>, <multiply>-*/-BigInteger.prototype.exp10 = function(n) {-	n = +n;-	if (n === 0) {-		return this;-	}-	if (Math.abs(n) > Number(MAX_EXP)) {-		throw new Error("exponent too large in BigInteger.exp10");-	}-	// Optimization for this == 0. This also keeps us from having to trim zeros in the positive n case-	if (this._s === 0) {-		return ZERO;-	}-	if (n > 0) {-		var k = new BigInteger(this._d.slice(), this._s, CONSTRUCT);--		for (; n >= BigInteger_base_log10; n -= BigInteger_base_log10) {-			k._d.unshift(0);-		}-		if (n == 0)-			return k;-		k._s = 1;-		k = k.multiplySingleDigit(Math.pow(10, n));-		return (this._s < 0 ? k.negate() : k);-	} else if (-n >= this._d.length*BigInteger_base_log10) {-		return ZERO;-	} else {-		var k = new BigInteger(this._d.slice(), this._s, CONSTRUCT);--		for (n = -n; n >= BigInteger_base_log10; n -= BigInteger_base_log10) {-			k._d.shift();-		}-		return (n == 0) ? k : k.divRemSmall(Math.pow(10, n))[0];-	}-};--/*-	Function: pow-	Raise a <BigInteger> to a power.--	In this implementation, 0**0 is 1.--	Parameters:--		n - The exponent to raise *this* by. *n* must be no greater than-		<BigInteger.MAX_EXP> (0x7FFFFFFF), or an exception will be thrown.--	Returns:--		*this* raised to the *nth* power.--	See Also:--		<modPow>-*/-BigInteger.prototype.pow = function(n) {-	if (this.isUnit()) {-		if (this._s > 0) {-			return this;-		}-		else {-			return BigInteger(n).isOdd() ? this : this.negate();-		}-	}--	n = BigInteger(n);-	if (n._s === 0) {-		return ONE;-	}-	else if (n._s < 0) {-		if (this._s === 0) {-			throw new Error("Divide by zero");-		}-		else {-			return ZERO;-		}-	}-	if (this._s === 0) {-		return ZERO;-	}-	if (n.isUnit()) {-		return this;-	}--	if (n.compareAbs(MAX_EXP) > 0) {-		throw new Error("exponent too large in BigInteger.pow");-	}-	var x = this;-	var aux = ONE;-	var two = BigInteger.small[2];--	while (n.isPositive()) {-		if (n.isOdd()) {-			aux = aux.multiply(x);-			if (n.isUnit()) {-				return aux;-			}-		}-		x = x.square();-		n = n.quotient(two);-	}--	return aux;-};--/*-	Function: modPow-	Raise a <BigInteger> to a power (mod m).--	Because it is reduced by a modulus, <modPow> is not limited by-	<BigInteger.MAX_EXP> like <pow>.--	Parameters:--		exponent - The exponent to raise *this* by. Must be positive.-		modulus - The modulus.--	Returns:--		*this* ^ *exponent* (mod *modulus*).--	See Also:--		<pow>, <mod>-*/-BigInteger.prototype.modPow = function(exponent, modulus) {-	var result = ONE;-	var base = this;--	while (exponent.isPositive()) {-		if (exponent.isOdd()) {-			result = result.multiply(base).remainder(modulus);-		}--		exponent = exponent.quotient(BigInteger.small[2]);-		if (exponent.isPositive()) {-			base = base.square().remainder(modulus);-		}-	}--	return result;-};--/*-	Function: log-	Get the natural logarithm of a <BigInteger> as a native JavaScript number.--	This is equivalent to--	> Math.log(this.toJSValue())--	but handles values outside of the native number range.--	Returns:--		log( *this* )--	See Also:--		<toJSValue>-*/-BigInteger.prototype.log = function() {-	switch (this._s) {-	case 0:	 return -Infinity;-	case -1: return NaN;-	default: // Fall through.-	}--	var l = this._d.length;--	if (l*BigInteger_base_log10 < 30) {-		return Math.log(this.valueOf());-	}--	var N = Math.ceil(30/BigInteger_base_log10);-	var firstNdigits = this._d.slice(l - N);-	return Math.log((new BigInteger(firstNdigits, 1, CONSTRUCT)).valueOf()) + (l - N) * Math.log(BigInteger_base);-};--/*-	Function: valueOf-	Convert a <BigInteger> to a native JavaScript integer.--	This is called automatically by JavaScipt to convert a <BigInteger> to a-	native value.--	Returns:--		> parseInt(this.toString(), 10)--	See Also:--		<toString>, <toJSValue>-*/-BigInteger.prototype.valueOf = function() {-	return parseInt(this.toString(), 10);-};--/*-	Function: toJSValue-	Convert a <BigInteger> to a native JavaScript integer.--	This is the same as valueOf, but more explicitly named.--	Returns:--		> parseInt(this.toString(), 10)--	See Also:--		<toString>, <valueOf>-*/-BigInteger.prototype.toJSValue = function() {-	return parseInt(this.toString(), 10);-};--var MAX_EXP = BigInteger(0x7FFFFFFF);-// Constant: MAX_EXP-// The largest exponent allowed in <pow> and <exp10> (0x7FFFFFFF or 2147483647).-BigInteger.MAX_EXP = MAX_EXP;--(function() {-	function makeUnary(fn) {-		return function(a) {-			return fn.call(BigInteger(a));-		};-	}--	function makeBinary(fn) {-		return function(a, b) {-			return fn.call(BigInteger(a), BigInteger(b));-		};-	}--	function makeTrinary(fn) {-		return function(a, b, c) {-			return fn.call(BigInteger(a), BigInteger(b), BigInteger(c));-		};-	}--	(function() {-		var i, fn;-		var unary = "toJSValue,isEven,isOdd,sign,isZero,isNegative,abs,isUnit,square,negate,isPositive,toString,next,prev,log".split(",");-		var binary = "compare,remainder,divRem,subtract,add,quotient,divide,multiply,pow,compareAbs".split(",");-		var trinary = ["modPow"];--		for (i = 0; i < unary.length; i++) {-			fn = unary[i];-			BigInteger[fn] = makeUnary(BigInteger.prototype[fn]);-		}--		for (i = 0; i < binary.length; i++) {-			fn = binary[i];-			BigInteger[fn] = makeBinary(BigInteger.prototype[fn]);-		}--		for (i = 0; i < trinary.length; i++) {-			fn = trinary[i];-			BigInteger[fn] = makeTrinary(BigInteger.prototype[fn]);-		}--		BigInteger.exp10 = function(x, n) {-			return BigInteger(x).exp10(n);-		};-	})();-})();--exports.BigInteger = BigInteger;-})(typeof exports !== 'undefined' ? exports : this);

@@ -1,32 +0,0 @@-// Copyright 2002-2010, Simon Marlow.  All rights reserved.-// https://github.com/haskell/haddock/blob/ghc-8.8/LICENSE-// Slightly modified by Tesla Ice Zhang--var highlight = function (on) {-  return function () {-    var links = document.getElementsByTagName('a');-    for (var i = 0; i < links.length; i++) {-      var that = links[i];--      if (this.href != that.href) {-        continue;-      }--      if (on) {-        that.classList.add("hover-highlight");-      } else {-        that.classList.remove("hover-highlight");-      }-    }-  }-};--window.onload = function () {-  var links = document.getElementsByTagName('a');-  for (var i = 0; i < links.length; i++) {-    var link = links[i];-    if (!link.hasAttribute("href")) continue;-    link.onmouseover = highlight(true);-    link.onmouseout = highlight(false);-  }-};

@@ -32,9 +32,6 @@ erased :: a erased = coe (\ _ -> erased) -mazIncompleteMatch :: String -> a-mazIncompleteMatch s = error ("Agda: incomplete pattern matching: " ++ s)- mazUnreachableError :: a mazUnreachableError = error ("Agda: unreachable code reached.") 

@@ -1,712 +0,0 @@-% -----------------------------------------------------------------------% Some useful commands when doing highlighting of Agda code in LaTeX.-% ------------------------------------------------------------------------\ProvidesPackage{agda}--\RequirePackage{ifxetex, ifluatex, xifthen, xcolor, polytable, etoolbox,-                calc, environ, xparse, xkeyval}--% https://tex.stackexchange.com/questions/47576/combining-ifxetex-and-ifluatex-with-the-logical-or-operation-\newif\ifxetexorluatex-\ifxetex-  \xetexorluatextrue-\else-  \ifluatex-    \xetexorluatextrue-  \else-    \xetexorluatexfalse-  \fi-\fi--% -----------------------------------------------------------------------% Options--\DeclareOption{bw}   {\newcommand{\AgdaColourScheme}{bw}}-\DeclareOption{conor}{\newcommand{\AgdaColourScheme}{conor}}--\newif\if@AgdaEnableReferences\@AgdaEnableReferencesfalse-\DeclareOption{references}{-  \@AgdaEnableReferencestrue-}--\newif\if@AgdaEnableLinks\@AgdaEnableLinksfalse-\DeclareOption{links}{-  \@AgdaEnableLinkstrue-}--\ProcessOptions\relax--% -----------------------------------------------------------------------% Font setup--\tracinglostchars=2 % If the font is missing some symbol, then say-                    % so in the compilation output.--% -----------------------------------------------------------------------% Colour schemes.--\providecommand{\AgdaColourScheme}{standard}--% -----------------------------------------------------------------------% References to code (needs additional post-processing of tex files to-% work, see wiki for details).--\if@AgdaEnableReferences-  \RequirePackage{catchfilebetweentags, xstring}-  \newcommand{\AgdaRef}[2][]{%-    \StrSubstitute{#2}{\_}{AgdaUnderscore}[\tmp]%-    \ifthenelse{\isempty{#1}}%-               {\ExecuteMetaData{AgdaTag-\tmp}}%-               {\ExecuteMetaData{#1}{AgdaTag-\tmp}}-  }-\fi--\providecommand{\AgdaRef}[2][]{#2}--% -----------------------------------------------------------------------% Links (only done if the option is passed and the user has loaded the-% hyperref package).--\if@AgdaEnableLinks-  \@ifpackageloaded{hyperref}{--    % List that holds added targets.-    \newcommand{\AgdaList}[0]{}--    \newtoggle{AgdaIsElem}-    \newcounter{AgdaIndex}-    \newcommand{\AgdaLookup}[3]{%-      \togglefalse{AgdaIsElem}%-      \setcounter{AgdaIndex}{0}%-      \renewcommand*{\do}[1]{%-      \ifstrequal{#1}{##1}%-        {\toggletrue{AgdaIsElem}\listbreak}%-        {\stepcounter{AgdaIndex}}}%-      \dolistloop{\AgdaList}%-      \iftoggle{AgdaIsElem}{#2}{#3}%-    }--    \newcommand*{\AgdaTargetHelper}[1]{%-      \AgdaLookup{#1}%-        {\PackageError{agda}{``#1'' used as target more than once}%-                            {Overloaded identifiers and links do not%-                             work well, consider using unique%-                             \MessageBreak identifiers instead.}%-        }%-        {\listadd{\AgdaList}{#1}%-         \hypertarget{Agda\theAgdaIndex}{}%-        }%-    }--    \newcommand{\AgdaTarget}[1]{\forcsvlist{\AgdaTargetHelper}{#1}}--    \newcommand{\AgdaLink}[1]{%-      \AgdaLookup{#1}%-        {\hyperlink{Agda\theAgdaIndex}{#1}}%-        {#1}%-    }-  }{\PackageError{agda}{Load the hyperref package before the agda package}{}}-\fi--\providecommand{\AgdaTarget}[1]{}-\providecommand{\AgdaLink}[1]{#1}--% -----------------------------------------------------------------------% Font styles.--\newcommand{\AgdaFontStyle}[1]{\textsf{#1}}-\ifthenelse{\equal{\AgdaColourScheme}{bw}}{-    \newcommand{\AgdaKeywordFontStyle}[1]{\underline{#1}}-}{-    \newcommand{\AgdaKeywordFontStyle}[1]{\textsf{#1}}-}-\newcommand{\AgdaStringFontStyle}[1]{\texttt{#1}}-\newcommand{\AgdaCommentFontStyle}[1]{\texttt{#1}}-\newcommand{\AgdaBoundFontStyle}[1]{\textit{#1}}--% -----------------------------------------------------------------------% Colours.--% -----------------------------------% The black and white colour scheme.-\ifthenelse{\equal{\AgdaColourScheme}{bw}}{--    % Aspect colours.-    \definecolor{AgdaComment}      {HTML}{000000}-    \definecolor{AgdaPragma}       {HTML}{000000}-    \definecolor{AgdaKeyword}      {HTML}{000000}-    \definecolor{AgdaString}       {HTML}{000000}-    \definecolor{AgdaNumber}       {HTML}{000000}-    \definecolor{AgdaSymbol}       {HTML}{000000}-    \definecolor{AgdaPrimitiveType}{HTML}{000000}--    % NameKind colours.-    \definecolor{AgdaBound}                 {HTML}{000000}-    \definecolor{AgdaGeneralizable}         {HTML}{000000}-    \definecolor{AgdaInductiveConstructor}  {HTML}{000000}-    \definecolor{AgdaCoinductiveConstructor}{HTML}{000000}-    \definecolor{AgdaDatatype}              {HTML}{000000}-    \definecolor{AgdaField}                 {HTML}{000000}-    \definecolor{AgdaFunction}              {HTML}{000000}-    \definecolor{AgdaMacro}                 {HTML}{000000}-    \definecolor{AgdaModule}                {HTML}{000000}-    \definecolor{AgdaPostulate}             {HTML}{000000}-    \definecolor{AgdaPrimitive}             {HTML}{000000}-    \definecolor{AgdaRecord}                {HTML}{000000}-    \definecolor{AgdaArgument}              {HTML}{000000}--    % Other aspect colours.-    \definecolor{AgdaDottedPattern}     {HTML}{000000}-    \definecolor{AgdaUnsolvedMeta}      {HTML}{D3D3D3}-    \definecolor{AgdaUnsolvedConstraint}{HTML}{D3D3D3}-    \definecolor{AgdaTerminationProblem}{HTML}{BEBEBE}-    \definecolor{AgdaIncompletePattern} {HTML}{D3D3D3}-    \definecolor{AgdaErrorWarning}      {HTML}{BEBEBE}-    \definecolor{AgdaError}             {HTML}{696969}--    % Misc.-    \definecolor{AgdaHole}              {HTML}{BEBEBE}--% -----------------------------------% Conor McBride's colour scheme.-}{ \ifthenelse{\equal{\AgdaColourScheme}{conor}}{--    % Aspect colours.-    \definecolor{AgdaComment}      {HTML}{B22222}-    \definecolor{AgdaPragma}       {HTML}{000000}-    \definecolor{AgdaKeyword}      {HTML}{000000}-    \definecolor{AgdaString}       {HTML}{000000}-    \definecolor{AgdaNumber}       {HTML}{000000}-    \definecolor{AgdaSymbol}       {HTML}{000000}-    \definecolor{AgdaPrimitiveType}{HTML}{0000CD}--    % NameKind colours.-    \definecolor{AgdaBound}                 {HTML}{A020F0}-    \definecolor{AgdaGeneralizable}         {HTML}{A020F0}-    \definecolor{AgdaInductiveConstructor}  {HTML}{8B0000}-    \definecolor{AgdaCoinductiveConstructor}{HTML}{8B0000}-    \definecolor{AgdaDatatype}              {HTML}{0000CD}-    \definecolor{AgdaField}                 {HTML}{8B0000}-    \definecolor{AgdaFunction}              {HTML}{006400}-    \definecolor{AgdaMacro}                 {HTML}{006400}-    \definecolor{AgdaModule}                {HTML}{006400}-    \definecolor{AgdaPostulate}             {HTML}{006400}-    \definecolor{AgdaPrimitive}             {HTML}{006400}-    \definecolor{AgdaRecord}                {HTML}{0000CD}-    \definecolor{AgdaArgument}              {HTML}{404040}--    % Other aspect colours.-    \definecolor{AgdaDottedPattern}     {HTML}{000000}-    \definecolor{AgdaUnsolvedMeta}      {HTML}{FFD700}-    \definecolor{AgdaUnsolvedConstraint}{HTML}{FFD700}-    \definecolor{AgdaTerminationProblem}{HTML}{FF0000}-    \definecolor{AgdaIncompletePattern} {HTML}{A020F0}-    \definecolor{AgdaErrorWarning}      {HTML}{FF0000}-    \definecolor{AgdaError}             {HTML}{F4A460}--    % Misc.-    \definecolor{AgdaHole}              {HTML}{9DFF9D}--% -----------------------------------% The standard colour scheme.-}{-    % Aspect colours.-    \definecolor{AgdaComment}      {HTML}{B22222}-    \definecolor{AgdaPragma}       {HTML}{000000}-    \definecolor{AgdaKeyword}      {HTML}{CD6600}-    \definecolor{AgdaString}       {HTML}{B22222}-    \definecolor{AgdaNumber}       {HTML}{A020F0}-    \definecolor{AgdaSymbol}       {HTML}{404040}-    \definecolor{AgdaPrimitiveType}{HTML}{0000CD}--    % NameKind colours.-    \definecolor{AgdaBound}                 {HTML}{000000}-    \definecolor{AgdaGeneralizable}         {HTML}{000000}-    \definecolor{AgdaInductiveConstructor}  {HTML}{008B00}-    \definecolor{AgdaCoinductiveConstructor}{HTML}{8B7500}-    \definecolor{AgdaDatatype}              {HTML}{0000CD}-    \definecolor{AgdaField}                 {HTML}{EE1289}-    \definecolor{AgdaFunction}              {HTML}{0000CD}-    \definecolor{AgdaMacro}                 {HTML}{458B74}-    \definecolor{AgdaModule}                {HTML}{A020F0}-    \definecolor{AgdaPostulate}             {HTML}{0000CD}-    \definecolor{AgdaPrimitive}             {HTML}{0000CD}-    \definecolor{AgdaRecord}                {HTML}{0000CD}-    \definecolor{AgdaArgument}              {HTML}{404040}--    % Other aspect colours.-    \definecolor{AgdaDottedPattern}     {HTML}{000000}-    \definecolor{AgdaUnsolvedMeta}      {HTML}{FFFF00}-    \definecolor{AgdaUnsolvedConstraint}{HTML}{FFFF00}-    \definecolor{AgdaTerminationProblem}{HTML}{FFA07A}-    \definecolor{AgdaIncompletePattern} {HTML}{F5DEB3}-    \definecolor{AgdaErrorWarning}      {HTML}{FFA07A}-    \definecolor{AgdaError}             {HTML}{FF0000}--    % Misc.-    \definecolor{AgdaHole}              {HTML}{9DFF9D}-}}--% -----------------------------------------------------------------------% Commands.--\newcommand{\AgdaNoSpaceMath}[1]-    {\begingroup\thickmuskip=0mu\medmuskip=0mu#1\endgroup}--% Aspect commands.-\newcommand{\AgdaComment}     [1]-    {\AgdaNoSpaceMath{\AgdaCommentFontStyle{\textcolor{AgdaComment}{#1}}}}-\newcommand{\AgdaPragma}      [1]-    {\AgdaNoSpaceMath{\AgdaCommentFontStyle{\textcolor{AgdaPragma}{#1}}}}-\newcommand{\AgdaKeyword}     [1]-    {\AgdaNoSpaceMath{\AgdaKeywordFontStyle{\textcolor{AgdaKeyword}{#1}}}}-\newcommand{\AgdaString}      [1]-    {\AgdaNoSpaceMath{\AgdaStringFontStyle{\textcolor{AgdaString}{#1}}}}-\newcommand{\AgdaNumber}      [1]-    {\AgdaNoSpaceMath{\AgdaFontStyle{\textcolor{AgdaNumber}{#1}}}}-\newcommand{\AgdaSymbol}      [1]-    {\AgdaNoSpaceMath{\AgdaFontStyle{\textcolor{AgdaSymbol}{#1}}}}-\newcommand{\AgdaPrimitiveType}[1]-    {\AgdaNoSpaceMath{\AgdaFontStyle{\textcolor{AgdaPrimitiveType}{#1}}}}-% Note that, in code generated by the LaTeX backend, \AgdaOperator is-% always applied to a NameKind command.-\newcommand{\AgdaOperator}    [1]{#1}--% NameKind commands.--% The user can control the typesetting of (certain) individual tokens-% by redefining the following command. The first argument is the token-% and the second argument the thing to be typeset (sometimes just the-% token, sometimes \AgdaLink{<the token>}). Example:-%-%   \usepackage{ifthen}-%-%   % Insert extra space before some tokens.-%   \DeclareRobustCommand{\AgdaFormat}[2]{%-%     \ifthenelse{-%       \equal{#1}{≡⟨} \OR-%       \equal{#1}{≡⟨⟩} \OR-%       \equal{#1}{∎}-%     }{\ }{}#2}-%-% Note the use of \DeclareRobustCommand.--\newcommand{\AgdaFormat}[2]{#2}--\newcommand{\AgdaBound}[1]-    {\AgdaNoSpaceMath{\AgdaBoundFontStyle{\textcolor{AgdaBound}{\AgdaFormat{#1}{#1}}}}}-\newcommand{\AgdaGeneralizable}[1]-    {\AgdaNoSpaceMath{\AgdaBoundFontStyle{\textcolor{AgdaGeneralizable}{\AgdaFormat{#1}{#1}}}}}-\newcommand{\AgdaInductiveConstructor}[1]-    {\AgdaNoSpaceMath{\AgdaFontStyle{\textcolor{AgdaInductiveConstructor}{\AgdaFormat{#1}{\AgdaLink{#1}}}}}}-\newcommand{\AgdaCoinductiveConstructor}[1]-    {\AgdaNoSpaceMath{\AgdaFontStyle{\textcolor{AgdaCoinductiveConstructor}{\AgdaFormat{#1}{\AgdaLink{#1}}}}}}-\newcommand{\AgdaDatatype}[1]-    {\AgdaNoSpaceMath{\AgdaFontStyle{\textcolor{AgdaDatatype}{\AgdaFormat{#1}{\AgdaLink{#1}}}}}}-\newcommand{\AgdaField}[1]-    {\AgdaNoSpaceMath{\AgdaFontStyle{\textcolor{AgdaField}{\AgdaFormat{#1}{\AgdaLink{#1}}}}}}-\newcommand{\AgdaFunction}[1]-    {\AgdaNoSpaceMath{\AgdaFontStyle{\textcolor{AgdaFunction}{\AgdaFormat{#1}{\AgdaLink{#1}}}}}}-\newcommand{\AgdaMacro}[1]-    {\AgdaNoSpaceMath{\AgdaFontStyle{\textcolor{AgdaMacro}{\AgdaFormat{#1}{\AgdaLink{#1}}}}}}-\newcommand{\AgdaModule}[1]-    {\AgdaNoSpaceMath{\AgdaFontStyle{\textcolor{AgdaModule}{\AgdaFormat{#1}{\AgdaLink{#1}}}}}}-\newcommand{\AgdaPostulate}[1]-    {\AgdaNoSpaceMath{\AgdaFontStyle{\textcolor{AgdaPostulate}{\AgdaFormat{#1}{\AgdaLink{#1}}}}}}-\newcommand{\AgdaPrimitive}[1]-    {\AgdaNoSpaceMath{\AgdaFontStyle{\textcolor{AgdaPrimitive}{\AgdaFormat{#1}{#1}}}}}-\newcommand{\AgdaRecord}[1]-    {\AgdaNoSpaceMath{\AgdaFontStyle{\textcolor{AgdaRecord}{\AgdaFormat{#1}{\AgdaLink{#1}}}}}}-\newcommand{\AgdaArgument}[1]-    {\AgdaNoSpaceMath{\AgdaBoundFontStyle{\textcolor{AgdaArgument}{\AgdaFormat{#1}{#1}}}}}--% Other aspect commands.-\newcommand{\AgdaFixityOp}          [1]{\AgdaNoSpaceMath{$#1$}}-\newcommand{\AgdaDottedPattern}     [1]{\textcolor{AgdaDottedPattern}{#1}}-\newcommand{\AgdaUnsolvedMeta}      [1]-    {\AgdaFontStyle{\colorbox{AgdaUnsolvedMeta}{#1}}}-\newcommand{\AgdaUnsolvedConstraint}[1]-    {\AgdaFontStyle{\colorbox{AgdaUnsolvedConstraint}{#1}}}-\newcommand{\AgdaTerminationProblem}[1]-    {\AgdaFontStyle{\colorbox{AgdaTerminationProblem}{#1}}}-\newcommand{\AgdaIncompletePattern} [1]{\colorbox{AgdaIncompletePattern}{#1}}-\newcommand{\AgdaErrorWarning}      [1]{\colorbox{AgdaErrorWarning}{#1}}-\newcommand{\AgdaError}             [1]-    {\AgdaFontStyle{\textcolor{AgdaError}{\underline{#1}}}}-\newcommand{\AgdaCatchallClause}    [1]{#1} % feel free to change this--% Used to hide code from LaTeX.-%-% Note that this macro has been deprecated in favour of giving the-% hide argument to the code environment.-\long\def\AgdaHide#1{\ignorespaces}--% Misc.-\newcommand{\AgdaHole}[1]{\colorbox{AgdaHole}{#1}}--% -----------------------------------------------------------------------% The code environment.--\newcommand{\AgdaCodeStyle}{}-% \newcommand{\AgdaCodeStyle}{\tiny}--\ifdefined\mathindent-  {}-\else-  \newdimen\mathindent\mathindent\leftmargini-\fi--% Adds the given amount of vertical space and starts a new line.-%-% The implementation comes from lhs2TeX's polycode.fmt, written by-% Andres Löh.-\newcommand{\Agda@NewlineWithVerticalSpace}[1]{%-  {\parskip=0pt\parindent=0pt\par\vskip #1\noindent}}--% Should there be space around code?-\newboolean{Agda@SpaceAroundCode}--% Use this command to avoid extra space around code blocks.-\newcommand{\AgdaNoSpaceAroundCode}{%-  \setboolean{Agda@SpaceAroundCode}{false}}--% Use this command to include extra space around code blocks.-\newcommand{\AgdaSpaceAroundCode}{%-  \setboolean{Agda@SpaceAroundCode}{true}}--% By default space is inserted around code blocks.-\AgdaSpaceAroundCode{}--% Sometimes one might want to break up a code block into multiple-% pieces, but keep code in different blocks aligned with respect to-% each other. Then one can use the AgdaAlign environment. Example-% usage:-%-%   \begin{AgdaAlign}-%   \begin{code}-%     code-%       code  (more code)-%   \end{code}-%   Explanation...-%   \begin{code}-%     aligned with "code"-%       code  (aligned with (more code))-%   \end{code}-%   \end{AgdaAlign}-%-% Note that AgdaAlign environments should not be nested.-%-% Sometimes one might also want to hide code in the middle of a code-% block. This can be accomplished in the following way:-%-%   \begin{AgdaAlign}-%   \begin{code}-%     visible-%   \end{code}-%   \begin{code}[hide]-%     hidden-%   \end{code}-%   \begin{code}-%     visible-%   \end{code}-%   \end{AgdaAlign}-%-% However, the result may be ugly: extra space is perhaps inserted-% around the code blocks.-%-% The AgdaSuppressSpace environment ensures that extra space is only-% inserted before the first code block, and after the last one (but-% not if \AgdaNoSpaceAroundCode{} is used). Example usage:-%-%   \begin{AgdaAlign}-%   \begin{code}-%     code-%       more code-%   \end{code}-%   Explanation...-%   \begin{AgdaSuppressSpace}-%   \begin{code}-%     aligned with "code"-%       aligned with "more code"-%   \end{code}-%   \begin{code}[hide]-%     hidden code-%   \end{code}-%   \begin{code}-%       also aligned with "more code"-%   \end{code}-%   \end{AgdaSuppressSpace}-%   \end{AgdaAlign}-%-% Note that AgdaSuppressSpace environments should not be nested.-%-% There is also a combined environment, AgdaMultiCode, that combines-% the effects of AgdaAlign and AgdaSuppressSpace.--% The number of the current/next code block (excluding hidden ones).-\newcounter{Agda@Current}-\setcounter{Agda@Current}{0}--% The number of the previous code block (excluding hidden ones), used-% locally in \Agda@SuppressEnd.-\newcounter{Agda@Previous}--% Is AgdaAlign active?-\newboolean{Agda@Align}-\setboolean{Agda@Align}{false}--% The number of the first code block (if any) in a given AgdaAlign-% environment.-\newcounter{Agda@AlignStart}--\newcommand{\Agda@AlignStart}{%-  \ifthenelse{\boolean{Agda@Align}}{%-    \PackageError{agda}{Nested AgdaAlign environments}{%-      AgdaAlign and AgdaMultiCode environments must not be-      nested.}}{%-    \setboolean{Agda@Align}{true}%-    \setcounter{Agda@AlignStart}{\value{Agda@Current}}}}--\newcommand{\Agda@AlignEnd}{\setboolean{Agda@Align}{false}}--\newenvironment{AgdaAlign}{%-  \Agda@AlignStart{}}{%-  \Agda@AlignEnd{}%-  \ignorespacesafterend}--% Is AgdaSuppressSpace active?-\newboolean{Agda@Suppress}-\setboolean{Agda@Suppress}{false}--% The number of the first code block (if any) in a given-% AgdaSuppressSpace environment.-\newcounter{Agda@SuppressStart}--% Does a "do not suppress space after" label exist for the current-% code block? (This boolean is used locally in the code environment's-% implementation.)-\newboolean{Agda@DoNotSuppressSpaceAfter}--\newcommand{\Agda@SuppressStart}{%-  \ifthenelse{\boolean{Agda@Suppress}}{%-    \PackageError{agda}{Nested AgdaSuppressSpace environments}{%-      AgdaSuppressSpace and AgdaMultiCode environments must not be-      nested.}}{%-    \setboolean{Agda@Suppress}{true}%-    \setcounter{Agda@SuppressStart}{\value{Agda@Current}}}}--% Marks the given code block as one that space should not be-% suppressed after (if AgdaSpaceAroundCode and AgdaSuppressSpace are-% both active).-\newcommand{\Agda@DoNotSuppressSpaceAfter}[1]{%-  % The use of labels is intended to ensure that LaTeX will provide a-  % warning if the document needs to be recompiled.-  \label{Agda@DoNotSuppressSpaceAfter@#1}}--\newcommand{\Agda@SuppressEnd}{%-  \ifthenelse{\value{Agda@SuppressStart} = \value{Agda@Current}}{}{%-    % Mark the previous code block in the .aux file.-    \setcounter{Agda@Previous}{\theAgda@Current-1}%-    \immediate\write\@auxout{%-      \noexpand\Agda@DoNotSuppressSpaceAfter{\theAgda@Previous}}}%-  \setboolean{Agda@Suppress}{false}}--\newenvironment{AgdaSuppressSpace}{%-  \Agda@SuppressStart{}}{%-  \Agda@SuppressEnd{}%-  \ignorespacesafterend}--\newenvironment{AgdaMultiCode}{%-  \Agda@AlignStart{}%-  \Agda@SuppressStart{}}{%-  \Agda@SuppressEnd{}%-  \Agda@AlignEnd{}%-  \ignorespacesafterend}--% Vertical space used for empty lines. By default \abovedisplayskip.-\newlength{\AgdaEmptySkip}-\setlength{\AgdaEmptySkip}{\abovedisplayskip}--% Extra space to be inserted for empty lines (the difference between-% \AgdaEmptySkip and \baselineskip). Used internally.-\newlength{\AgdaEmptyExtraSkip}--% Counter used for code numbers.-\newcounter{AgdaCodeNumber}-% Formats a code number.-\newcommand{\AgdaFormatCodeNumber}[1]{(#1)}--% A boolean used to handle the option number.-\newboolean{Agda@Number}-\setboolean{Agda@Number}{false}--% A boolean used to handle the option inline*. (For some reason the-% approach used for hide and inline does not work for inline*.)-\newboolean{Agda@InlineStar}-\setboolean{Agda@InlineStar}{false}--% Keys used by the code environment.-\define@boolkey[Agda]{code}{hide}[true]{}-\define@boolkey[Agda]{code}{inline}[true]{}-\define@boolkey[Agda]{code}{inline*}[true]{%-  \setboolean{Agda@InlineStar}{true}}-\define@key[Agda]{code}{number}[]{%-  \ifthenelse{\boolean{Agda@Number}}{}{%-    \setboolean{Agda@Number}{true}%-    % Increase the counter if this has not already been done.-    \refstepcounter{AgdaCodeNumber}}%-  % If the label is non-empty, set it. Note that it is possible to-  % give several labels for a single code listing.-  \ifthenelse{\equal{#1}{}}{}{\label{#1}}}--% The code environment.-%-% Options:-%-% * hide: The code is hidden. Other options are ignored.-%-% * number: Give the code an equation number.-%-% * number=l: Give the code an equation number and the label l. It is-%   possible to use this option several times with different labels.-%-% * inline/inline*: The code is inlined. In this case most of the-%   discussion above does not apply, alignment is not respected, and so-%   on. It is recommended to only use this option for a single line of-%   code, and to not use two consecutive spaces in this piece of code.-%-%   Note that this environment ignores spaces after its end. If a space-%   (\AgdaSpace{}) should be inserted after the inline code, use-%   inline*, otherwise use inline.-%-%   When this option is used number is ignored.-%-% The implementation is based on plainhscode in lhs2TeX's-% polycode.fmt, written by Andres Löh.-\NewEnviron{code}[1][]{%-  % Process the options. Complain about unknown options.-  \setkeys[Agda]{code}[number]{#1}%-  \ifAgda@code@hide%-    % Hide the code.-  \else%-  \ifAgda@code@inline%-    % Inline code.-    %-    % Make the polytable primitives emitted by the LaTeX backend-    % do nothing.-    \DeclareDocumentCommand{\>}{O{}O{}}{}%-    \DeclareDocumentCommand{\<}{O{}}{}%-    \AgdaCodeStyle\BODY%-  \else%-  \ifthenelse{\boolean{Agda@InlineStar}}{%-    % Inline code with space at the end.-    %-    \DeclareDocumentCommand{\>}{O{}O{}}{}%-    \DeclareDocumentCommand{\<}{O{}}{}%-    \AgdaCodeStyle\BODY\AgdaSpace{}}{%-    %-    % Displayed code.-    %-    % Conditionally emit space before the code block. Unconditionally-    % switch to a new line.-    \ifthenelse{\boolean{Agda@SpaceAroundCode} \and%-                \(\not \boolean{Agda@Suppress} \or%-                  \value{Agda@SuppressStart} = \value{Agda@Current}\)}{%-      \Agda@NewlineWithVerticalSpace{\abovedisplayskip}}{%-      \Agda@NewlineWithVerticalSpace{0pt}}%-    %-    % Check if numbers have been requested. If they have, then a side-    % effect of this call is that Agda@Number is set to true, the code-    % number counter is increased, and the label (if any) is set.-    \setkeys[Agda]{code}[hide,inline,inline*]{#1}%-    \ifthenelse{\boolean{Agda@Number}}{%-      % Equation numbers have been requested. Use a minipage, so that-      % there is room for the code number to the right, and the code-      % number becomes centered vertically.-      \begin{minipage}{%-          \linewidth-%-          \widthof{%-            \AgdaSpace{}%-            \AgdaFormatCodeNumber{\theAgdaCodeNumber}}}}{}%-    %-    % Indent the entire code block.-    \advance\leftskip\mathindent%-    %-    % The code's style can be customised.-    \AgdaCodeStyle%-    %-    % Used to control the height of empty lines.-    \setlength{\AgdaEmptyExtraSkip}{\AgdaEmptySkip - \baselineskip}%-    %-    % The environment used to handle indentation (of individual lines)-    % and alignment.-    \begin{pboxed}%-      %-      % Conditionally preserve alignment between code blocks.-      \ifthenelse{\boolean{Agda@Align}}{%-        \ifthenelse{\value{Agda@AlignStart} = \value{Agda@Current}}{%-          \savecolumns}{%-          \restorecolumns}}{}%-      %-      % The code.-      \BODY%-    \end{pboxed}%-    %-    \ifthenelse{\boolean{Agda@Number}}{%-      % Equation numbers have been requested.-      \end{minipage}%-      % Insert the code number to the right.-      \hfill \AgdaFormatCodeNumber{\theAgdaCodeNumber}}{}%-    %-    % Does the label Agda@DoNotSuppressAfter@<current code block-    % number> exist?-    \ifcsdef{r@Agda@DoNotSuppressSpaceAfter@\theAgda@Current}{%-      \setboolean{Agda@DoNotSuppressSpaceAfter}{true}}{%-      \setboolean{Agda@DoNotSuppressSpaceAfter}{false}}%-    %-    % Conditionally emit space after the code block. Unconditionally-    % switch to a new line.-    \ifthenelse{\boolean{Agda@SpaceAroundCode} \and%-                \(\not \boolean{Agda@Suppress} \or%-                  \boolean{Agda@DoNotSuppressSpaceAfter}\)}{%-      \Agda@NewlineWithVerticalSpace{\belowdisplayskip}}{%-      \Agda@NewlineWithVerticalSpace{0pt}}%-    %-    % Step the code block counter, but only for non-hidden code.-    \stepcounter{Agda@Current}}%-  \fi%-  \fi%-  % Reset Agda@Number and Agda@InlineStar.-  \setboolean{Agda@Number}{false}%-  \setboolean{Agda@InlineStar}{false}}--% Space inserted after tokens.-\newcommand{\AgdaSpace}{ }--% Space inserted to indent something.-\newcommand{\AgdaIndentSpace}{\AgdaSpace{}$\;\;$}--% Default column for polytable.-\defaultcolumn{@{}l@{\AgdaSpace{}}}--% \AgdaIndent expects a non-negative integer as its only argument.-% This integer should be the distance, in code blocks, to the thing-% relative to which the text is indented.-%-% The default implementation only indents if the thing that the text-% is indented relative to exists in the same code block or is wrapped-% in the same AgdaAlign or AgdaMultiCode environment.-\newcommand{\AgdaIndent}[1]{%-  \ifthenelse{#1 = 0-                \or-              \( \boolean{Agda@Align}-                   \and-                 \cnttest{\value{Agda@Current} - #1}{>=}{-                          \value{Agda@AlignStart}}-              \)}{\AgdaIndentSpace{}}{}}--% Underscores are typeset using \AgdaUnderscore{}.-\newcommand{\AgdaUnderscore}{\_}--\endinput

@@ -309,6 +309,8 @@   ("increment" . ("∆"))   ("inf"       . ("∞"))   ("&"         . ("⅋"))+  ("z;"        . ("⨟"))+  ("z:"        . ("⦂"))    ;; Circled operators. @@ -966,6 +968,12 @@   ;; ("_y" . ("y"))   ;; ("_z" . ("z")) +  ("_Gb" . ("ᵦ"))+  ("_Gg" . ("ᵧ"))+  ("_Gr" . ("ᵨ"))+  ("_Gf" . ("ᵩ"))+  ("_Gc" . ("ᵪ"))+   ("^a" . ("ᵃ"))   ("^b" . ("ᵇ"))   ("^c" . ("ᶜ"))@@ -1019,6 +1027,14 @@   ;; ("^X" . ("X"))   ;; ("^Y" . ("Y"))   ;; ("^Z" . ("Z"))++  ("^Gb" . ("ᵝ"))+  ("^Gg" . ("ᵞ"))+  ("^Gd" . ("ᵟ"))+  ("^Ge" . ("ᵋ"))+  ("^Gth" . ("ᶿ"))+  ("^Gf" . ("ᵠ"))+  ("^Gc" . ("ᵡ"))    ;; Some ISO8859-1 characters. 

@@ -1,3 +1,3 @@-(define-package "agda2-mode" "2.6.2"+(define-package "agda2-mode" "2.6.2.1"   "interactive development for Agda, a dependently typed functional programming language"   '((emacs "24.3") (annotation "1.0") (eri "1.0")))

@@ -28,7 +28,7 @@  ;;; Code: -(defvar agda2-version "2.6.2"+(defvar agda2-version "2.6.2.1"   "The version of the Agda mode. Note that the same version of the Agda executable must be used.") @@ -606,10 +606,10 @@                       "Cmd_abort"))  (defun agda2-abort-done ()-  "Removes annotations, resets certain variables.+  "Resets certain variables. Intended to be used by the backend if an abort command was successful."-  (agda2-remove-annotations)+  (agda2-info-action "*Aborted*" "Aborted." t)   (setq agda2-highlight-in-progress nil         agda2-last-responses        nil)) 

@@ -0,0 +1,41 @@+/* Aspects. */+.Agda .Comment       { color: #B22222 }+.Agda .Background    {}+.Agda .Markup        { color: #000000 }+.Agda .Keyword       { color: #CD6600 }+.Agda .String        { color: #B22222 }+.Agda .Number        { color: #A020F0 }+.Agda .Symbol        { color: #404040 }+.Agda .PrimitiveType { color: #0000CD }+.Agda .Pragma        { color: black   }+.Agda .Operator      {}+.Agda .Hole          { background: #B4EEB4 }++/* NameKinds. */+.Agda .Bound                  { color: black   }+.Agda .Generalizable          { color: black   }+.Agda .InductiveConstructor   { color: #008B00 }+.Agda .CoinductiveConstructor { color: #8B7500 }+.Agda .Datatype               { color: #0000CD }+.Agda .Field                  { color: #EE1289 }+.Agda .Function               { color: #0000CD }+.Agda .Module                 { color: #A020F0 }+.Agda .Postulate              { color: #0000CD }+.Agda .Primitive              { color: #0000CD }+.Agda .Record                 { color: #0000CD }++/* OtherAspects. */+.Agda .DottedPattern        {}+.Agda .UnsolvedMeta         { color: black; background: yellow         }+.Agda .UnsolvedConstraint   { color: black; background: yellow         }+.Agda .TerminationProblem   { color: black; background: #FFA07A        }+.Agda .IncompletePattern    { color: black; background: #F5DEB3        }+.Agda .Error                { color: red;   text-decoration: underline }+.Agda .TypeChecks           { color: black; background: #ADD8E6        }+.Agda .Deadcode             { color: black; background: #808080        }+.Agda .ShadowingInTelescope { color: black; background: #808080        }++/* Standard attributes. */+.Agda a { text-decoration: none }+.Agda a[href]:hover { background-color: #B4EEB4 }+.Agda [href].hover-highlight { background-color: #B4EEB4; }

@@ -0,0 +1,32 @@+// Copyright 2002-2010, Simon Marlow.  All rights reserved.+// https://github.com/haskell/haddock/blob/ghc-8.8/LICENSE+// Slightly modified by Tesla Ice Zhang++var highlight = function (on) {+  return function () {+    var links = document.getElementsByTagName('a');+    for (var i = 0; i < links.length; i++) {+      var that = links[i];++      if (this.href != that.href) {+        continue;+      }++      if (on) {+        that.classList.add("hover-highlight");+      } else {+        that.classList.remove("hover-highlight");+      }+    }+  }+};++window.onload = function () {+  var links = document.getElementsByTagName('a');+  for (var i = 0; i < links.length; i++) {+    var link = links[i];+    if (!link.hasAttribute("href")) continue;+    link.onmouseover = highlight(true);+    link.onmouseout = highlight(false);+  }+};

@@ -0,0 +1,722 @@+% ----------------------------------------------------------------------+% Some useful commands when doing highlighting of Agda code in LaTeX.+% ----------------------------------------------------------------------++% !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!+% !!! NOTE: when you make changes to this file, bump the date. !!!+% !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!+\ProvidesPackage{agda}+  [2021/07/14 version 2.6.2.1 Formatting LaTeX generated by Agda]++\RequirePackage{ifxetex, ifluatex, xifthen, xcolor, polytable, etoolbox,+                calc, environ, xparse, xkeyval}++% https://tex.stackexchange.com/questions/47576/combining-ifxetex-and-ifluatex-with-the-logical-or-operation+\newif\ifxetexorluatex+\ifxetex+  \xetexorluatextrue+\else+  \ifluatex+    \xetexorluatextrue+  \else+    \xetexorluatexfalse+  \fi+\fi++% ----------------------------------------------------------------------+% Options++\DeclareOption{bw}   {\newcommand{\AgdaColourScheme}{bw}}+\DeclareOption{conor}{\newcommand{\AgdaColourScheme}{conor}}++\newif\if@AgdaEnableReferences\@AgdaEnableReferencesfalse+\DeclareOption{references}{+  \@AgdaEnableReferencestrue+}++\newif\if@AgdaEnableLinks\@AgdaEnableLinksfalse+\DeclareOption{links}{+  \@AgdaEnableLinkstrue+}++\ProcessOptions\relax++% ----------------------------------------------------------------------+% Font setup++\tracinglostchars=2 % If the font is missing some symbol, then say+                    % so in the compilation output.++% ----------------------------------------------------------------------+% Colour schemes.++\providecommand{\AgdaColourScheme}{standard}++% ----------------------------------------------------------------------+% References to code (needs additional post-processing of tex files to+% work, see wiki for details).++\if@AgdaEnableReferences+  \RequirePackage{catchfilebetweentags, xstring}+  \newcommand{\AgdaRef}[2][]{%+    \StrSubstitute{#2}{\_}{AgdaUnderscore}[\tmp]%+    \ifthenelse{\isempty{#1}}%+               {\ExecuteMetaData{AgdaTag-\tmp}}%+               {\ExecuteMetaData{#1}{AgdaTag-\tmp}}+  }+\fi++\providecommand{\AgdaRef}[2][]{#2}++% ----------------------------------------------------------------------+% Links (only done if the option is passed and the user has loaded the+% hyperref package).++\if@AgdaEnableLinks+  \@ifpackageloaded{hyperref}{++    % List that holds added targets.+    \newcommand{\AgdaList}[0]{}++    \newtoggle{AgdaIsElem}+    \newcounter{AgdaIndex}+    \newcommand{\AgdaLookup}[3]{%+      \togglefalse{AgdaIsElem}%+      \setcounter{AgdaIndex}{0}%+      \renewcommand*{\do}[1]{%+      \ifstrequal{#1}{##1}%+        {\toggletrue{AgdaIsElem}\listbreak}%+        {\stepcounter{AgdaIndex}}}%+      \dolistloop{\AgdaList}%+      \iftoggle{AgdaIsElem}{#2}{#3}%+    }++    \newcommand*{\AgdaTargetHelper}[1]{%+      \AgdaLookup{#1}%+        {\PackageError{agda}{``#1'' used as target more than once}%+                            {Overloaded identifiers and links do not%+                             work well, consider using unique%+                             \MessageBreak identifiers instead.}%+        }%+        {\listadd{\AgdaList}{#1}%+         \hypertarget{Agda\theAgdaIndex}{}%+        }%+    }++    \newcommand{\AgdaTarget}[1]{\forcsvlist{\AgdaTargetHelper}{#1}}++    \newcommand{\AgdaLink}[1]{%+      \AgdaLookup{#1}%+        {\hyperlink{Agda\theAgdaIndex}{#1}}%+        {#1}%+    }+  }{\PackageError{agda}{Load the hyperref package before the agda package}{}}+\fi++\providecommand{\AgdaTarget}[1]{}+\providecommand{\AgdaLink}[1]{#1}++% ----------------------------------------------------------------------+% Font styles.++\newcommand{\AgdaFontStyle}[1]{\textsf{#1}}+\ifthenelse{\equal{\AgdaColourScheme}{bw}}{+    \newcommand{\AgdaKeywordFontStyle}[1]{\underline{#1}}+}{+    \newcommand{\AgdaKeywordFontStyle}[1]{\textsf{#1}}+}+\newcommand{\AgdaStringFontStyle}[1]{\texttt{#1}}+\newcommand{\AgdaCommentFontStyle}[1]{\texttt{#1}}+\newcommand{\AgdaBoundFontStyle}[1]{\textit{#1}}++% ----------------------------------------------------------------------+% Colours.++% ----------------------------------+% The black and white colour scheme.+\ifthenelse{\equal{\AgdaColourScheme}{bw}}{++    % Aspect colours.+    \definecolor{AgdaComment}      {HTML}{000000}+    \definecolor{AgdaPragma}       {HTML}{000000}+    \definecolor{AgdaKeyword}      {HTML}{000000}+    \definecolor{AgdaString}       {HTML}{000000}+    \definecolor{AgdaNumber}       {HTML}{000000}+    \definecolor{AgdaSymbol}       {HTML}{000000}+    \definecolor{AgdaPrimitiveType}{HTML}{000000}++    % NameKind colours.+    \definecolor{AgdaBound}                 {HTML}{000000}+    \definecolor{AgdaGeneralizable}         {HTML}{000000}+    \definecolor{AgdaInductiveConstructor}  {HTML}{000000}+    \definecolor{AgdaCoinductiveConstructor}{HTML}{000000}+    \definecolor{AgdaDatatype}              {HTML}{000000}+    \definecolor{AgdaField}                 {HTML}{000000}+    \definecolor{AgdaFunction}              {HTML}{000000}+    \definecolor{AgdaMacro}                 {HTML}{000000}+    \definecolor{AgdaModule}                {HTML}{000000}+    \definecolor{AgdaPostulate}             {HTML}{000000}+    \definecolor{AgdaPrimitive}             {HTML}{000000}+    \definecolor{AgdaRecord}                {HTML}{000000}+    \definecolor{AgdaArgument}              {HTML}{000000}++    % Other aspect colours.+    \definecolor{AgdaDottedPattern}     {HTML}{000000}+    \definecolor{AgdaUnsolvedMeta}      {HTML}{D3D3D3}+    \definecolor{AgdaUnsolvedConstraint}{HTML}{D3D3D3}+    \definecolor{AgdaTerminationProblem}{HTML}{BEBEBE}+    \definecolor{AgdaIncompletePattern} {HTML}{D3D3D3}+    \definecolor{AgdaErrorWarning}      {HTML}{BEBEBE}+    \definecolor{AgdaError}             {HTML}{696969}++    % Misc.+    \definecolor{AgdaHole}              {HTML}{BEBEBE}++% ----------------------------------+% Conor McBride's colour scheme.+}{ \ifthenelse{\equal{\AgdaColourScheme}{conor}}{++    % Aspect colours.+    \definecolor{AgdaComment}      {HTML}{B22222}+    \definecolor{AgdaPragma}       {HTML}{000000}+    \definecolor{AgdaKeyword}      {HTML}{000000}+    \definecolor{AgdaString}       {HTML}{000000}+    \definecolor{AgdaNumber}       {HTML}{000000}+    \definecolor{AgdaSymbol}       {HTML}{000000}+    \definecolor{AgdaPrimitiveType}{HTML}{0000CD}++    % NameKind colours.+    \definecolor{AgdaBound}                 {HTML}{A020F0}+    \definecolor{AgdaGeneralizable}         {HTML}{A020F0}+    \definecolor{AgdaInductiveConstructor}  {HTML}{8B0000}+    \definecolor{AgdaCoinductiveConstructor}{HTML}{8B0000}+    \definecolor{AgdaDatatype}              {HTML}{0000CD}+    \definecolor{AgdaField}                 {HTML}{8B0000}+    \definecolor{AgdaFunction}              {HTML}{006400}+    \definecolor{AgdaMacro}                 {HTML}{006400}+    \definecolor{AgdaModule}                {HTML}{006400}+    \definecolor{AgdaPostulate}             {HTML}{006400}+    \definecolor{AgdaPrimitive}             {HTML}{006400}+    \definecolor{AgdaRecord}                {HTML}{0000CD}+    \definecolor{AgdaArgument}              {HTML}{404040}++    % Other aspect colours.+    \definecolor{AgdaDottedPattern}     {HTML}{000000}+    \definecolor{AgdaUnsolvedMeta}      {HTML}{FFD700}+    \definecolor{AgdaUnsolvedConstraint}{HTML}{FFD700}+    \definecolor{AgdaTerminationProblem}{HTML}{FF0000}+    \definecolor{AgdaIncompletePattern} {HTML}{A020F0}+    \definecolor{AgdaErrorWarning}      {HTML}{FF0000}+    \definecolor{AgdaError}             {HTML}{F4A460}++    % Misc.+    \definecolor{AgdaHole}              {HTML}{9DFF9D}++% ----------------------------------+% The standard colour scheme.+}{+    % Aspect colours.+    \definecolor{AgdaComment}      {HTML}{B22222}+    \definecolor{AgdaPragma}       {HTML}{000000}+    \definecolor{AgdaKeyword}      {HTML}{CD6600}+    \definecolor{AgdaString}       {HTML}{B22222}+    \definecolor{AgdaNumber}       {HTML}{A020F0}+    \definecolor{AgdaSymbol}       {HTML}{404040}+    \definecolor{AgdaPrimitiveType}{HTML}{0000CD}++    % NameKind colours.+    \definecolor{AgdaBound}                 {HTML}{000000}+    \definecolor{AgdaGeneralizable}         {HTML}{000000}+    \definecolor{AgdaInductiveConstructor}  {HTML}{008B00}+    \definecolor{AgdaCoinductiveConstructor}{HTML}{8B7500}+    \definecolor{AgdaDatatype}              {HTML}{0000CD}+    \definecolor{AgdaField}                 {HTML}{EE1289}+    \definecolor{AgdaFunction}              {HTML}{0000CD}+    \definecolor{AgdaMacro}                 {HTML}{458B74}+    \definecolor{AgdaModule}                {HTML}{A020F0}+    \definecolor{AgdaPostulate}             {HTML}{0000CD}+    \definecolor{AgdaPrimitive}             {HTML}{0000CD}+    \definecolor{AgdaRecord}                {HTML}{0000CD}+    \definecolor{AgdaArgument}              {HTML}{404040}++    % Other aspect colours.+    \definecolor{AgdaDottedPattern}     {HTML}{000000}+    \definecolor{AgdaUnsolvedMeta}      {HTML}{FFFF00}+    \definecolor{AgdaUnsolvedConstraint}{HTML}{FFFF00}+    \definecolor{AgdaTerminationProblem}{HTML}{FFA07A}+    \definecolor{AgdaIncompletePattern} {HTML}{F5DEB3}+    \definecolor{AgdaErrorWarning}      {HTML}{FFA07A}+    \definecolor{AgdaError}             {HTML}{FF0000}++    % Misc.+    \definecolor{AgdaHole}              {HTML}{9DFF9D}+}}++% ----------------------------------------------------------------------+% Commands.++\newcommand{\AgdaNoSpaceMath}[1]+    {\begingroup\thickmuskip=0mu\medmuskip=0mu#1\endgroup}++% Aspect commands.+\newcommand{\AgdaComment}     [1]+    {\AgdaNoSpaceMath{\textcolor{AgdaComment}{\AgdaCommentFontStyle{#1}}}}+\newcommand{\AgdaPragma}      [1]+    {\AgdaNoSpaceMath{\textcolor{AgdaPragma}{\AgdaCommentFontStyle{#1}}}}+\newcommand{\AgdaKeyword}     [1]+    {\AgdaNoSpaceMath{\textcolor{AgdaKeyword}{\AgdaKeywordFontStyle{#1}}}}+\newcommand{\AgdaString}      [1]+    {\AgdaNoSpaceMath{\textcolor{AgdaString}{\AgdaStringFontStyle{#1}}}}+\newcommand{\AgdaNumber}      [1]+    {\AgdaNoSpaceMath{\textcolor{AgdaNumber}{\AgdaFontStyle{#1}}}}+\newcommand{\AgdaSymbol}      [1]+    {\AgdaNoSpaceMath{\textcolor{AgdaSymbol}{\AgdaFontStyle{#1}}}}+\newcommand{\AgdaPrimitiveType}[1]+    {\AgdaNoSpaceMath{\textcolor{AgdaPrimitiveType}{\AgdaFontStyle{#1}}}}+%% Andreas, 2021-07-14, issue #5471+%% To make italics correction \/ work, the font-style modifier+%% needs to be inside, in particular inside the \textcolor modifier,+%% as the \textcolor{} wrapping around something hides its content+%% to the logic that resolves \/ into a space or not.++% Note that, in code generated by the LaTeX backend, \AgdaOperator is+% always applied to a NameKind command.+\newcommand{\AgdaOperator}    [1]{#1}++% NameKind commands.++% The user can control the typesetting of (certain) individual tokens+% by redefining the following command. The first argument is the token+% and the second argument the thing to be typeset (sometimes just the+% token, sometimes \AgdaLink{<the token>}). Example:+%+%   \usepackage{ifthen}+%+%   % Insert extra space before some tokens.+%   \DeclareRobustCommand{\AgdaFormat}[2]{%+%     \ifthenelse{+%       \equal{#1}{≡⟨} \OR+%       \equal{#1}{≡⟨⟩} \OR+%       \equal{#1}{∎}+%     }{\ }{}#2}+%+% Note the use of \DeclareRobustCommand.++\newcommand{\AgdaFormat}[2]{#2}++\newcommand{\AgdaBound}[1]+    {\AgdaNoSpaceMath{\textcolor{AgdaBound}{\AgdaBoundFontStyle{\AgdaFormat{#1}{#1}}}}}+\newcommand{\AgdaGeneralizable}[1]+    {\AgdaNoSpaceMath{\textcolor{AgdaGeneralizable}{\AgdaBoundFontStyle{\AgdaFormat{#1}{#1}}}}}+\newcommand{\AgdaInductiveConstructor}[1]+    {\AgdaNoSpaceMath{\textcolor{AgdaInductiveConstructor}{\AgdaFontStyle{\AgdaFormat{#1}{\AgdaLink{#1}}}}}}+\newcommand{\AgdaCoinductiveConstructor}[1]+    {\AgdaNoSpaceMath{\textcolor{AgdaCoinductiveConstructor}{\AgdaFontStyle{\AgdaFormat{#1}{\AgdaLink{#1}}}}}}+\newcommand{\AgdaDatatype}[1]+    {\AgdaNoSpaceMath{\textcolor{AgdaDatatype}{\AgdaFontStyle{\AgdaFormat{#1}{\AgdaLink{#1}}}}}}+\newcommand{\AgdaField}[1]+    {\AgdaNoSpaceMath{\textcolor{AgdaField}{\AgdaFontStyle{\AgdaFormat{#1}{\AgdaLink{#1}}}}}}+\newcommand{\AgdaFunction}[1]+    {\AgdaNoSpaceMath{\textcolor{AgdaFunction}{\AgdaFontStyle{\AgdaFormat{#1}{\AgdaLink{#1}}}}}}+\newcommand{\AgdaMacro}[1]+    {\AgdaNoSpaceMath{\textcolor{AgdaMacro}{\AgdaFontStyle{\AgdaFormat{#1}{\AgdaLink{#1}}}}}}+\newcommand{\AgdaModule}[1]+    {\AgdaNoSpaceMath{\textcolor{AgdaModule}{\AgdaFontStyle{\AgdaFormat{#1}{\AgdaLink{#1}}}}}}+\newcommand{\AgdaPostulate}[1]+    {\AgdaNoSpaceMath{\textcolor{AgdaPostulate}{\AgdaFontStyle{\AgdaFormat{#1}{\AgdaLink{#1}}}}}}+\newcommand{\AgdaPrimitive}[1]+    {\AgdaNoSpaceMath{\textcolor{AgdaPrimitive}{\AgdaFontStyle{\AgdaFormat{#1}{#1}}}}}+\newcommand{\AgdaRecord}[1]+    {\AgdaNoSpaceMath{\textcolor{AgdaRecord}{\AgdaFontStyle{\AgdaFormat{#1}{\AgdaLink{#1}}}}}}+\newcommand{\AgdaArgument}[1]+    {\AgdaNoSpaceMath{\textcolor{AgdaArgument}{\AgdaBoundFontStyle{\AgdaFormat{#1}{#1}}}}}++% Other aspect commands.+\newcommand{\AgdaFixityOp}          [1]{\AgdaNoSpaceMath{$#1$}}+\newcommand{\AgdaDottedPattern}     [1]{\textcolor{AgdaDottedPattern}{#1}}+\newcommand{\AgdaUnsolvedMeta}      [1]+    {\AgdaFontStyle{\colorbox{AgdaUnsolvedMeta}{#1}}}+\newcommand{\AgdaUnsolvedConstraint}[1]+    {\AgdaFontStyle{\colorbox{AgdaUnsolvedConstraint}{#1}}}+\newcommand{\AgdaTerminationProblem}[1]+    {\AgdaFontStyle{\colorbox{AgdaTerminationProblem}{#1}}}+\newcommand{\AgdaIncompletePattern} [1]{\colorbox{AgdaIncompletePattern}{#1}}+\newcommand{\AgdaErrorWarning}      [1]{\colorbox{AgdaErrorWarning}{#1}}+\newcommand{\AgdaError}             [1]+    {\textcolor{AgdaError}{\AgdaFontStyle{\underline{#1}}}}+\newcommand{\AgdaCatchallClause}    [1]{#1} % feel free to change this++% Used to hide code from LaTeX.+%+% Note that this macro has been deprecated in favour of giving the+% hide argument to the code environment.+\long\def\AgdaHide#1{\ignorespaces}++% Misc.+\newcommand{\AgdaHole}[1]{\colorbox{AgdaHole}{#1}}++% ----------------------------------------------------------------------+% The code environment.++\newcommand{\AgdaCodeStyle}{}+% \newcommand{\AgdaCodeStyle}{\tiny}++\ifdefined\mathindent+  {}+\else+  \newdimen\mathindent\mathindent\leftmargini+\fi++% Adds the given amount of vertical space and starts a new line.+%+% The implementation comes from lhs2TeX's polycode.fmt, written by+% Andres Löh.+\newcommand{\Agda@NewlineWithVerticalSpace}[1]{%+  {\parskip=0pt\parindent=0pt\par\vskip #1\noindent}}++% Should there be space around code?+\newboolean{Agda@SpaceAroundCode}++% Use this command to avoid extra space around code blocks.+\newcommand{\AgdaNoSpaceAroundCode}{%+  \setboolean{Agda@SpaceAroundCode}{false}}++% Use this command to include extra space around code blocks.+\newcommand{\AgdaSpaceAroundCode}{%+  \setboolean{Agda@SpaceAroundCode}{true}}++% By default space is inserted around code blocks.+\AgdaSpaceAroundCode{}++% Sometimes one might want to break up a code block into multiple+% pieces, but keep code in different blocks aligned with respect to+% each other. Then one can use the AgdaAlign environment. Example+% usage:+%+%   \begin{AgdaAlign}+%   \begin{code}+%     code+%       code  (more code)+%   \end{code}+%   Explanation...+%   \begin{code}+%     aligned with "code"+%       code  (aligned with (more code))+%   \end{code}+%   \end{AgdaAlign}+%+% Note that AgdaAlign environments should not be nested.+%+% Sometimes one might also want to hide code in the middle of a code+% block. This can be accomplished in the following way:+%+%   \begin{AgdaAlign}+%   \begin{code}+%     visible+%   \end{code}+%   \begin{code}[hide]+%     hidden+%   \end{code}+%   \begin{code}+%     visible+%   \end{code}+%   \end{AgdaAlign}+%+% However, the result may be ugly: extra space is perhaps inserted+% around the code blocks.+%+% The AgdaSuppressSpace environment ensures that extra space is only+% inserted before the first code block, and after the last one (but+% not if \AgdaNoSpaceAroundCode{} is used). Example usage:+%+%   \begin{AgdaAlign}+%   \begin{code}+%     code+%       more code+%   \end{code}+%   Explanation...+%   \begin{AgdaSuppressSpace}+%   \begin{code}+%     aligned with "code"+%       aligned with "more code"+%   \end{code}+%   \begin{code}[hide]+%     hidden code+%   \end{code}+%   \begin{code}+%       also aligned with "more code"+%   \end{code}+%   \end{AgdaSuppressSpace}+%   \end{AgdaAlign}+%+% Note that AgdaSuppressSpace environments should not be nested.+%+% There is also a combined environment, AgdaMultiCode, that combines+% the effects of AgdaAlign and AgdaSuppressSpace.++% The number of the current/next code block (excluding hidden ones).+\newcounter{Agda@Current}+\setcounter{Agda@Current}{0}++% The number of the previous code block (excluding hidden ones), used+% locally in \Agda@SuppressEnd.+\newcounter{Agda@Previous}++% Is AgdaAlign active?+\newboolean{Agda@Align}+\setboolean{Agda@Align}{false}++% The number of the first code block (if any) in a given AgdaAlign+% environment.+\newcounter{Agda@AlignStart}++\newcommand{\Agda@AlignStart}{%+  \ifthenelse{\boolean{Agda@Align}}{%+    \PackageError{agda}{Nested AgdaAlign environments}{%+      AgdaAlign and AgdaMultiCode environments must not be+      nested.}}{%+    \setboolean{Agda@Align}{true}%+    \setcounter{Agda@AlignStart}{\value{Agda@Current}}}}++\newcommand{\Agda@AlignEnd}{\setboolean{Agda@Align}{false}}++\newenvironment{AgdaAlign}{%+  \Agda@AlignStart{}}{%+  \Agda@AlignEnd{}%+  \ignorespacesafterend}++% Is AgdaSuppressSpace active?+\newboolean{Agda@Suppress}+\setboolean{Agda@Suppress}{false}++% The number of the first code block (if any) in a given+% AgdaSuppressSpace environment.+\newcounter{Agda@SuppressStart}++% Does a "do not suppress space after" label exist for the current+% code block? (This boolean is used locally in the code environment's+% implementation.)+\newboolean{Agda@DoNotSuppressSpaceAfter}++\newcommand{\Agda@SuppressStart}{%+  \ifthenelse{\boolean{Agda@Suppress}}{%+    \PackageError{agda}{Nested AgdaSuppressSpace environments}{%+      AgdaSuppressSpace and AgdaMultiCode environments must not be+      nested.}}{%+    \setboolean{Agda@Suppress}{true}%+    \setcounter{Agda@SuppressStart}{\value{Agda@Current}}}}++% Marks the given code block as one that space should not be+% suppressed after (if AgdaSpaceAroundCode and AgdaSuppressSpace are+% both active).+\newcommand{\Agda@DoNotSuppressSpaceAfter}[1]{%+  % The use of labels is intended to ensure that LaTeX will provide a+  % warning if the document needs to be recompiled.+  \label{Agda@DoNotSuppressSpaceAfter@#1}}++\newcommand{\Agda@SuppressEnd}{%+  \ifthenelse{\value{Agda@SuppressStart} = \value{Agda@Current}}{}{%+    % Mark the previous code block in the .aux file.+    \setcounter{Agda@Previous}{\theAgda@Current-1}%+    \immediate\write\@auxout{%+      \noexpand\Agda@DoNotSuppressSpaceAfter{\theAgda@Previous}}}%+  \setboolean{Agda@Suppress}{false}}++\newenvironment{AgdaSuppressSpace}{%+  \Agda@SuppressStart{}}{%+  \Agda@SuppressEnd{}%+  \ignorespacesafterend}++\newenvironment{AgdaMultiCode}{%+  \Agda@AlignStart{}%+  \Agda@SuppressStart{}}{%+  \Agda@SuppressEnd{}%+  \Agda@AlignEnd{}%+  \ignorespacesafterend}++% Vertical space used for empty lines. By default \abovedisplayskip.+\newlength{\AgdaEmptySkip}+\setlength{\AgdaEmptySkip}{\abovedisplayskip}++% Extra space to be inserted for empty lines (the difference between+% \AgdaEmptySkip and \baselineskip). Used internally.+\newlength{\AgdaEmptyExtraSkip}++% Counter used for code numbers.+\newcounter{AgdaCodeNumber}+% Formats a code number.+\newcommand{\AgdaFormatCodeNumber}[1]{(#1)}++% A boolean used to handle the option number.+\newboolean{Agda@Number}+\setboolean{Agda@Number}{false}++% A boolean used to handle the option inline*. (For some reason the+% approach used for hide and inline does not work for inline*.)+\newboolean{Agda@InlineStar}+\setboolean{Agda@InlineStar}{false}++% Keys used by the code environment.+\define@boolkey[Agda]{code}{hide}[true]{}+\define@boolkey[Agda]{code}{inline}[true]{}+\define@boolkey[Agda]{code}{inline*}[true]{%+  \setboolean{Agda@InlineStar}{true}}+\define@key[Agda]{code}{number}[]{%+  \ifthenelse{\boolean{Agda@Number}}{}{%+    \setboolean{Agda@Number}{true}%+    % Increase the counter if this has not already been done.+    \refstepcounter{AgdaCodeNumber}}%+  % If the label is non-empty, set it. Note that it is possible to+  % give several labels for a single code listing.+  \ifthenelse{\equal{#1}{}}{}{\label{#1}}}++% The code environment.+%+% Options:+%+% * hide: The code is hidden. Other options are ignored.+%+% * number: Give the code an equation number.+%+% * number=l: Give the code an equation number and the label l. It is+%   possible to use this option several times with different labels.+%+% * inline/inline*: The code is inlined. In this case most of the+%   discussion above does not apply, alignment is not respected, and so+%   on. It is recommended to only use this option for a single line of+%   code, and to not use two consecutive spaces in this piece of code.+%+%   Note that this environment ignores spaces after its end. If a space+%   (\AgdaSpace{}) should be inserted after the inline code, use+%   inline*, otherwise use inline.+%+%   When this option is used number is ignored.+%+% The implementation is based on plainhscode in lhs2TeX's+% polycode.fmt, written by Andres Löh.+\NewEnviron{code}[1][]{%+  % Process the options. Complain about unknown options.+  \setkeys[Agda]{code}[number]{#1}%+  \ifAgda@code@hide%+    % Hide the code.+  \else%+  \ifAgda@code@inline%+    % Inline code.+    %+    % Make the polytable primitives emitted by the LaTeX backend+    % do nothing.+    \DeclareDocumentCommand{\>}{O{}O{}}{}%+    \DeclareDocumentCommand{\<}{O{}}{}%+    \AgdaCodeStyle\BODY%+  \else%+  \ifthenelse{\boolean{Agda@InlineStar}}{%+    % Inline code with space at the end.+    %+    \DeclareDocumentCommand{\>}{O{}O{}}{}%+    \DeclareDocumentCommand{\<}{O{}}{}%+    \AgdaCodeStyle\BODY\AgdaSpace{}}{%+    %+    % Displayed code.+    %+    % Conditionally emit space before the code block. Unconditionally+    % switch to a new line.+    \ifthenelse{\boolean{Agda@SpaceAroundCode} \and%+                \(\not \boolean{Agda@Suppress} \or%+                  \value{Agda@SuppressStart} = \value{Agda@Current}\)}{%+      \Agda@NewlineWithVerticalSpace{\abovedisplayskip}}{%+      \Agda@NewlineWithVerticalSpace{0pt}}%+    %+    % Check if numbers have been requested. If they have, then a side+    % effect of this call is that Agda@Number is set to true, the code+    % number counter is increased, and the label (if any) is set.+    \setkeys[Agda]{code}[hide,inline,inline*]{#1}%+    \ifthenelse{\boolean{Agda@Number}}{%+      % Equation numbers have been requested. Use a minipage, so that+      % there is room for the code number to the right, and the code+      % number becomes centered vertically.+      \begin{minipage}{%+          \linewidth-%+          \widthof{%+            \AgdaSpace{}%+            \AgdaFormatCodeNumber{\theAgdaCodeNumber}}}}{}%+    %+    % Indent the entire code block.+    \advance\leftskip\mathindent%+    %+    % The code's style can be customised.+    \AgdaCodeStyle%+    %+    % Used to control the height of empty lines.+    \setlength{\AgdaEmptyExtraSkip}{\AgdaEmptySkip - \baselineskip}%+    %+    % The environment used to handle indentation (of individual lines)+    % and alignment.+    \begin{pboxed}%+      %+      % Conditionally preserve alignment between code blocks.+      \ifthenelse{\boolean{Agda@Align}}{%+        \ifthenelse{\value{Agda@AlignStart} = \value{Agda@Current}}{%+          \savecolumns}{%+          \restorecolumns}}{}%+      %+      % The code.+      \BODY%+    \end{pboxed}%+    %+    \ifthenelse{\boolean{Agda@Number}}{%+      % Equation numbers have been requested.+      \end{minipage}%+      % Insert the code number to the right.+      \hfill \AgdaFormatCodeNumber{\theAgdaCodeNumber}}{}%+    %+    % Does the label Agda@DoNotSuppressAfter@<current code block+    % number> exist?+    \ifcsdef{r@Agda@DoNotSuppressSpaceAfter@\theAgda@Current}{%+      \setboolean{Agda@DoNotSuppressSpaceAfter}{true}}{%+      \setboolean{Agda@DoNotSuppressSpaceAfter}{false}}%+    %+    % Conditionally emit space after the code block. Unconditionally+    % switch to a new line.+    \ifthenelse{\boolean{Agda@SpaceAroundCode} \and%+                \(\not \boolean{Agda@Suppress} \or%+                  \boolean{Agda@DoNotSuppressSpaceAfter}\)}{%+      \Agda@NewlineWithVerticalSpace{\belowdisplayskip}}{%+      \Agda@NewlineWithVerticalSpace{0pt}}%+    %+    % Step the code block counter, but only for non-hidden code.+    \stepcounter{Agda@Current}}%+  \fi%+  \fi%+  % Reset Agda@Number and Agda@InlineStar.+  \setboolean{Agda@Number}{false}%+  \setboolean{Agda@InlineStar}{false}}++% Space inserted after tokens.+\newcommand{\AgdaSpace}{ }++% Space inserted to indent something.+\newcommand{\AgdaIndentSpace}{\AgdaSpace{}$\;\;$}++% Default column for polytable.+\defaultcolumn{@{}l@{\AgdaSpace{}}}++% \AgdaIndent expects a non-negative integer as its only argument.+% This integer should be the distance, in code blocks, to the thing+% relative to which the text is indented.+%+% The default implementation only indents if the thing that the text+% is indented relative to exists in the same code block or is wrapped+% in the same AgdaAlign or AgdaMultiCode environment.+\newcommand{\AgdaIndent}[1]{%+  \ifthenelse{#1 = 0+                \or+              \( \boolean{Agda@Align}+                   \and+                 \cnttest{\value{Agda@Current} - #1}{>=}{+                          \value{Agda@AlignStart}}+              \)}{\AgdaIndentSpace{}}{}}++% Underscores are typeset using \AgdaUnderscore{}.+\newcommand{\AgdaUnderscore}{\_}++\endinput

@@ -0,0 +1,24 @@+#!/usr/bin/env perl++use strict;+use warnings;++my $tag_prefix = "AgdaTag";+my $underscore = "AgdaUnderscore";+my $commands   = qr"(InductiveConstructor|CoinductiveConstructor\+                    |Datatype|Field|Function|Module|Postulate|Record)";++while (<>) {++  s|(\\Agda$commands)\{(.*?)\}++   | my $cmd = $1;+     my $arg = $3;+     my $tag = "$tag_prefix-$3" =~ s/\\_/$underscore/gr;++     $_ = "%\n%<*$tag>\n$cmd\{$arg\}%\n%</$tag>\n";+   |gxe;++  print;++}

@@ -13,6 +13,12 @@   {-# BUILTIN ID           Id       #-}   {-# BUILTIN CONID        conid    #-} +  -- Id x y is treated as a pair of I and x ≡ y, using "i" for the+  -- first component and "p" for the second.+  {-# COMPILE JS conid =+      _ => _ => _ => _ => i => p => { return { "i" : i, "p" : p } }+    #-}+   primitive     primDepIMin : _     primIdFace : ∀ {ℓ} {A : Set ℓ} {x y : A} → Id x y → I

@@ -12,5 +12,8 @@    {-# BUILTIN SUBIN inc #-} +  -- Sub A φ u is treated as A.+  {-# COMPILE JS inc = _ => _ => _ => x => x #-}+   primitive     primSubOut : ∀ {ℓ} {A : Set ℓ} {φ : I} {u : Partial φ A} → Sub _ φ u → A

@@ -349,3 +349,39 @@ {-# BUILTIN AGDATCMWITHRECONSPARAMS           withReconstructed          #-} {-# BUILTIN AGDATCMNOCONSTRAINTS              noConstraints              #-} {-# BUILTIN AGDATCMRUNSPECULATIVE             runSpeculative             #-}++-- All the TC primitives are compiled to functions that return+-- undefined, rather than just undefined, in an attempt to make sure+-- that code will run properly.+{-# COMPILE JS returnTC          = _ => _ => _ =>      undefined #-}+{-# COMPILE JS bindTC            = _ => _ => _ => _ =>+                                   _ => _ =>           undefined #-}+{-# COMPILE JS unify             = _ => _ =>           undefined #-}+{-# COMPILE JS typeError         = _ => _ => _ =>      undefined #-}+{-# COMPILE JS inferType         = _ =>                undefined #-}+{-# COMPILE JS checkType         = _ => _ =>           undefined #-}+{-# COMPILE JS normalise         = _ =>                undefined #-}+{-# COMPILE JS reduce            = _ =>                undefined #-}+{-# COMPILE JS catchTC           = _ => _ => _ => _ => undefined #-}+{-# COMPILE JS quoteTC           = _ => _ => _ =>      undefined #-}+{-# COMPILE JS unquoteTC         = _ => _ => _ =>      undefined #-}+{-# COMPILE JS quoteωTC          = _ => _ =>           undefined #-}+{-# COMPILE JS getContext        =                     undefined #-}+{-# COMPILE JS extendContext     = _ => _ => _ => _ => undefined #-}+{-# COMPILE JS inContext         = _ => _ => _ => _ => undefined #-}+{-# COMPILE JS freshName         = _ =>                undefined #-}+{-# COMPILE JS declareDef        = _ => _ =>           undefined #-}+{-# COMPILE JS declarePostulate  = _ => _ =>           undefined #-}+{-# COMPILE JS defineFun         = _ => _ =>           undefined #-}+{-# COMPILE JS getType           = _ =>                undefined #-}+{-# COMPILE JS getDefinition     = _ =>                undefined #-}+{-# COMPILE JS blockOnMeta       = _ => _ => _ =>      undefined #-}+{-# COMPILE JS commitTC          =                     undefined #-}+{-# COMPILE JS isMacro           = _ =>                undefined #-}+{-# COMPILE JS withNormalisation = _ => _ => _ => _ => undefined #-}+{-# COMPILE JS withReconstructed = _ => _ => _ =>      undefined #-}+{-# COMPILE JS debugPrint        = _ => _ => _ =>      undefined #-}+{-# COMPILE JS onlyReduceDefs    = _ => _ => _ => _ => undefined #-}+{-# COMPILE JS dontReduceDefs    = _ => _ => _ => _ => undefined #-}+{-# COMPILE JS noConstraints     = _ => _ => _ =>      undefined #-}+{-# COMPILE JS runSpeculative    = _ => _ => _ =>      undefined #-}

@@ -13,3 +13,5 @@          → TC (Σ Nat (λ _ → Σ String (λ _ → String)))  {-# BUILTIN AGDATCMEXEC execTC #-}++{-# COMPILE JS execTC = _ => _ => _ => undefined #-}

@@ -7,6 +7,10 @@ {-# BUILTIN IZERO    i0 #-} {-# BUILTIN IONE     i1 #-} +-- I is treated as the type of booleans.+{-# COMPILE JS i0 = false #-}+{-# COMPILE JS i1 = true  #-}+ infix  30 primINeg infixr 20 primIMin primIMax @@ -26,6 +30,15 @@ {-# BUILTIN ISONE1   IsOne1   #-} {-# BUILTIN ISONE2   IsOne2   #-} +-- IsOne i is treated as the unit type.+{-# COMPILE JS itIsOne = { "tt" : a => a["tt"]() } #-}+{-# COMPILE JS IsOne1 =+  _ => _ => _ => { return { "tt" : a => a["tt"]() } }+  #-}+{-# COMPILE JS IsOne2 =+  _ => _ => _ => { return { "tt" : a => a["tt"]() } }+  #-}+ -- Partial : ∀{ℓ} (i : I) (A : Set ℓ) → Set ℓ -- Partial i A = IsOne i → A @@ -36,6 +49,11 @@   isOneEmpty : ∀ {ℓ} {A : Partial i0 (Set ℓ)} → PartialP i0 A  {-# BUILTIN ISONEEMPTY isOneEmpty #-}++-- Partial i A and PartialP i A are treated as IsOne i → A.+{-# COMPILE JS isOneEmpty =+  _ => x => _ => x({ "tt" : a => a["tt"]() })+  #-}  primitive   primPOr : ∀ {ℓ} (i j : I) {A : Partial (primIMax i j) (Set ℓ)}

@@ -1,24 +0,0 @@-#!/usr/bin/env perl--use strict;-use warnings;--my $tag_prefix = "AgdaTag";-my $underscore = "AgdaUnderscore";-my $commands   = qr"(InductiveConstructor|CoinductiveConstructor\-                    |Datatype|Field|Function|Module|Postulate|Record)";--while (<>) {--  s|(\\Agda$commands)\{(.*?)\}--   | my $cmd = $1;-     my $arg = $3;-     my $tag = "$tag_prefix-$3" =~ s/\\_/$underscore/gr;--     $_ = "%\n%<*$tag>\n$cmd\{$arg\}%\n%</$tag>\n";-   |gxe;--  print;--}

@@ -16,6 +16,7 @@ import Control.Monad import Control.Monad.State +import Agda.Syntax.Common import qualified Agda.Syntax.Concrete.Name as C import Agda.Syntax.Internal as I @@ -146,6 +147,14 @@     -- We match on whether @["--no-main"]@ is one of the stored options.     when (["--no-main"] `elem` iFilePragmaOptions mainI) $       stPragmaOptions `modifyTCLens` \ o -> o { optCompileNoMain = True }++    -- Perhaps all pragma options from the top-level module should be+    -- made available to the compiler in a suitable way. Here are more+    -- hacks:+    when (any ("--cubical" `elem`) (iFilePragmaOptions mainI)) $+      stPragmaOptions `modifyTCLens` \ o -> o { optCubical = Just CFull }+    when (any ("--erased-cubical" `elem`) (iFilePragmaOptions mainI)) $+      stPragmaOptions `modifyTCLens` \ o -> o { optCubical = Just CErased }      setScope (iInsideScope mainI) -- so that compiler errors don't use overly qualified names     ignoreAbstractMode cont

@@ -34,7 +34,7 @@     mnameToList, qnameName, qnameModule, nameId ) import Agda.Syntax.Internal   ( Name, Type-  , arity, nameFixity, unDom )+  , nameFixity, unDom, telToList ) import Agda.Syntax.Literal       ( Literal(..) ) import Agda.Syntax.Treeless      ( ArgUsage(..), filterUsed ) import qualified Agda.Syntax.Treeless as T@@ -43,6 +43,7 @@ import Agda.TypeChecking.Reduce ( instantiateFull ) import Agda.TypeChecking.Substitute as TC ( TelV(..), raise, subst ) import Agda.TypeChecking.Pretty+import Agda.TypeChecking.Telescope ( telViewPath )  import Agda.Utils.FileName ( isNewerThan ) import Agda.Utils.Function ( iterate' )@@ -146,8 +147,18 @@ --- Top-level compilation ---  jsPreCompile :: JSOptions -> TCM JSOptions-jsPreCompile opts = return opts+jsPreCompile opts = do+  cubical <- optCubical <$> pragmaOptions+  let notSupported s =+        typeError $ GenericError $+          "Compilation of code that uses " ++ s ++ " is not supported."+  case cubical of+    Nothing      -> return ()+    Just CErased -> return ()+    Just CFull   -> notSupported "--cubical" +  return opts+ -- | After all modules have been compiled, copy RTE modules and verify compiled modules.  jsPostCompile :: JSOptions -> IsMain -> Map.Map ModuleName Module -> TCM ()@@ -192,10 +203,21 @@  --- Module compilation --- -type JSModuleEnv = Maybe CoinductionKit+data JSModuleEnv = JSModuleEnv+  { jsCoinductionKit :: Maybe CoinductionKit+  , jsCompile        :: Bool+    -- ^ Should this module be compiled?+  }  jsPreModule :: JSOptions -> IsMain -> ModuleName -> Maybe FilePath -> TCM (Recompile JSModuleEnv Module)-jsPreModule _opts _ m mifile = ifM uptodate noComp yesComp+jsPreModule _opts _ m mifile = do+  cubical <- optCubical <$> pragmaOptions+  let compile = case cubical of+        -- Code that uses --cubical is not compiled.+        Just CFull   -> False+        Just CErased -> True+        Nothing      -> True+  ifM uptodate noComp (yesComp compile)   where     uptodate = case mifile of       Nothing -> pure False@@ -209,11 +231,15 @@     -- A skipped module acts as a fake main module, to be skipped by --js-verify as well.     skippedModule = Module (jsMod m) mempty mempty (Just __IMPOSSIBLE__) -    yesComp = do+    yesComp compile = do       m   <- prettyShow <$> curMName       out <- outFile_       reportSLn "compile.js" 1 $ repl [m, ifileDesc, out] "Compiling <<0>> in <<1>> to <<2>>"-      Recompile <$> coinductionKit+      kit <- coinductionKit+      return $ Recompile $ JSModuleEnv+        { jsCoinductionKit = kit+        , jsCompile        = compile+        }  jsPostModule :: JSOptions -> JSModuleEnv -> IsMain -> ModuleName -> [Maybe Export] -> TCM Module jsPostModule opts _ isMain _ defs = do@@ -368,13 +394,18 @@     dropEquals = dropWhile $ \ c -> isSpace c || c == '='  definition' :: EnvWithOpts -> QName -> Definition -> Type -> JSQName -> TCM (Maybe Export)-definition' kit q d t ls = if not (usableModality d) then return Nothing else do+definition' kit q d t ls =+  if not (jsCompile (snd kit)) || not (usableModality d)+  then return Nothing+  else do   checkCompilerPragmas q   case theDef d of     -- coinduction-    Constructor{} | Just q == (nameOfSharp <$> snd kit) -> do+    Constructor{}+      | Just q == (nameOfSharp <$> jsCoinductionKit (snd kit)) -> do       return Nothing-    Function{} | Just q == (nameOfFlat <$> snd kit) -> do+    Function{}+      | Just q == (nameOfFlat <$> jsCoinductionKit (snd kit)) -> do       ret $ Lambda 1 $ Apply (Lookup (local 0) flatName) []      DataOrRecSig{} -> __IMPOSSIBLE__@@ -418,8 +449,12 @@           else Just $ Export ls funBody'      Primitive{primName = p}-      | p `Set.member` cubicalPrimitives ->-        typeError $ NotImplemented p+      | p == builtin_glueU ->+        -- The string prim^glueU is not a valid JS name.+        plainJS "agdaRTS.prim_glueU"+      | p == builtin_unglueU ->+        -- The string prim^unglueU is not a valid JS name.+        plainJS "agdaRTS.prim_unglueU"       | p `Set.member` primitives ->         plainJS $ "agdaRTS." ++ p       | Just e <- defJSDef d ->@@ -428,10 +463,6 @@         ret Undefined     PrimitiveSort{} -> return Nothing -    Datatype{ dataPathCons = _ : _ } -> do-      s <- render <$> prettyTCM q-      typeError $ NotImplemented $-        "Higher inductive types (" ++ s ++ ")"     Datatype{} -> do         computeErasedConstructorArgs q         ret emp@@ -441,7 +472,8 @@      Constructor{} | Just e <- defJSDef d -> plainJS e     Constructor{conData = p, conPars = nc} -> do-      let np = arity t - nc+      TelV tel _ <- telViewPath t+      let np = length (telToList tel) - nc       erased <- getErasedConArgs q       let nargs = np - length (filter id erased)           args = [ Local $ LocalId $ nargs - i | i <- [0 .. nargs-1] ]@@ -451,7 +483,7 @@         Record { recFields = flds } -> ret $ curriedLambda nargs $           if optJSOptimize (fst kit)             then Lambda 1 $ Apply (Local (LocalId 0)) args-            else Object $ Map.fromList [ (l, Lambda 1 $ Apply (Lookup (Local (LocalId 0)) l) args) ]+            else Object $ Map.singleton l $ Lambda 1 $ Apply (Lookup (Local (LocalId 0)) l) args         dt -> do           i <- index           ret $ curriedLambda (nargs + 1) $ Apply (Lookup (Local (LocalId 0)) i) args@@ -487,7 +519,8 @@           Datatype {} -> return (String "*")           Record {} -> return (String "*")           _ -> qname q-      T.TApp (T.TCon q) [x] | Just q == (nameOfSharp <$> snd kit) -> do+      T.TApp (T.TCon q) [x]+        | Just q == (nameOfSharp <$> jsCoinductionKit (snd kit)) -> do         x <- go x         let evalThunk = unlines               [ "function() {"@@ -498,7 +531,7 @@               , "  return result;"               , "}"               ]-        return $ Object $ Map.fromList+        return $ Object $ Map.fromListWith __IMPOSSIBLE__           [(flatName, PlainJS evalThunk)           ,(MemberId "__flat_helper", Lambda 0 x)]       T.TApp t' xs | Just f <- getDef t' -> do@@ -512,7 +545,8 @@             -- number of eta expanded args             etaN = length $ dropWhile (== ArgUsed) $ reverse $ drop given used -            args = filterUsed used $ xs ++ (T.TVar <$> downFrom etaN)+            args = filterUsed used $+                     raise etaN xs ++ (T.TVar <$> downFrom etaN)          curriedLambda etaN <$> (curriedApply <$> go (raise etaN t') <*> mapM go args) @@ -529,7 +563,7 @@         dt <- getConstInfo dt         alts' <- traverse (compileAlt kit) alts         let cs  = defConstructors $ theDef dt-            obj = Object $ Map.fromList [(snd x, y) | (x, y) <- alts']+            obj = Object $ Map.fromListWith __IMPOSSIBLE__ [(snd x, y) | (x, y) <- alts']             arr = mkArray [headWithDefault (mempty, Null) [(Comment s, y) | ((c', MemberId s), y) <- alts', c' == c] | c <- cs]         case (theDef dt, defJSDef dt) of           (_, Just e) -> do@@ -563,7 +597,8 @@      mkArray xs         | 2 * length (filter ((==Null) . snd) xs) <= length xs = Array xs-        | otherwise = Object $ Map.fromList [(MemberIndex i c, x) | (i, (c, x)) <- zip [0..] xs, x /= Null]+        | otherwise = Object $ Map.fromListWith __IMPOSSIBLE__+            [ (MemberIndex i c, x) | (i, (c, x)) <- zip [0..] xs, x /= Null ]  compilePrim :: T.TPrim -> Exp compilePrim p =@@ -637,7 +672,7 @@  litqname :: QName -> Exp litqname q =-  Object $ Map.fromList+  Object $ Map.fromListWith __IMPOSSIBLE__     [ (mem "id", Integer $ fromIntegral n)     , (mem "moduleId", Integer $ fromIntegral m)     , (mem "name", String $ T.pack $ prettyShow q)@@ -648,7 +683,7 @@     fx = theFixity $ nameFixity $ qnameName q      litfixity :: Fixity -> Exp-    litfixity fx = Object $ Map.fromList+    litfixity fx = Object $ Map.fromListWith __IMPOSSIBLE__       [ (mem "assoc", litAssoc $ fixityAssoc fx)       , (mem "prec", litPrec $ fixityLevel fx)] @@ -683,32 +718,12 @@   m <- curMName   outFile (jsMod m) --- | Cubical primitives that are (currently) not compiled.+-- | Primitives implemented in the JS Agda RTS. ----- TODO: Primitives that are neither part of this set nor of--- 'primitives', and for which 'defJSDef' does not return anything,--- are silently compiled to 'Undefined'. Thus, if a cubical primitive--- is by accident omitted from 'cubicalPrimitives', then programs that--- should be rejected are compiled to something which might not work--- as intended. A better approach might be to list exactly those+-- TODO: Primitives that are not part of this set, and for which+-- 'defJSDef' does not return anything, are silently compiled to+-- 'Undefined'. A better approach might be to list exactly those -- primitives which should be compiled to 'Undefined'.--cubicalPrimitives :: Set String-cubicalPrimitives = Set.fromList-  [ "primIMin"-  , "primIMax"-  , "primINeg"-  , "primPartial"-  , "primPartialP"-  , "primPFrom1"-  , "primPOr"-  , "primComp"-  , "primTransp"-  , "primHComp"-  , "primSubOut"-  ]---- | Primitives implemented in the JS Agda RTS. primitives :: Set String primitives = Set.fromList   [  "primShowInteger"@@ -822,25 +837,25 @@   -- , "primShowMeta"                -- missing   -- , "primMetaToNat"               -- missing   -- , "primMetaToNatInjective"      -- missing-  -- , "primIMin"                    -- missing-  -- , "primIMax"                    -- missing-  -- , "primINeg"                    -- missing-  -- , "primPOr"                     -- missing-  -- , "primComp"                    -- missing-  -- , builtinTrans                  -- missing-  -- , builtinHComp                  -- missing-  -- , "primIdJ"                     -- missing-  -- , "primPartial"                 -- missing-  -- , "primPartialP"                -- missing+  , builtinIMin+  , builtinIMax+  , builtinINeg+  , "primPartial"+  , "primPartialP"+  , builtinPOr+  , builtinComp+  , builtinTrans+  , builtinHComp+  , builtinSubOut+  , builtin_glueU+  , builtin_unglueU+  , builtinFaceForall+  , "primDepIMin"+  , "primIdFace"+  , "primIdPath"+  , "primIdJ"+  , builtinIdElim   -- , builtinGlue                   -- missing   -- , builtin_glue                  -- missing   -- , builtin_unglue                -- missing-  -- , builtinFaceForall             -- missing-  -- , "primDepIMin"                 -- missing-  -- , "primIdFace"                  -- missing-  -- , "primIdPath"                  -- missing-  -- , builtinIdElim                 -- missing-  -- , builtinSubOut                 -- missing-  -- , builtin_glueU                 -- missing-  -- , builtin_unglueU               -- missing   ]