diff --git a/Agda.cabal b/Agda.cabal --- a/Agda.cabal +++ b/Agda.cabal @@ -1,10 +1,10 @@ name: Agda -version: 2.6.2.1 +version: 2.6.2.2 cabal-version: >= 1.10 build-type: Custom license: OtherLicense license-file: LICENSE -copyright: (c) 2005-2021 The Agda Team. +copyright: (c) 2005-2022 The Agda Team. author: Ulf Norell and The Agda Team, see https://agda.readthedocs.io/en/latest/team.html maintainer: The Agda Team homepage: http://wiki.portal.chalmers.se/agda/ @@ -24,7 +24,7 @@ theory, a foundational system for constructive mathematics developed by the Swedish logician Per Martin-Löf. It has many similarities with other proof assistants based on dependent types, - such as Coq, Epigram and NuPRL. + such as Coq, Idris, Lean and NuPRL. . This package includes both a command-line program (agda) and an Emacs mode. If you want to use the Emacs mode you can set it up by @@ -41,10 +41,13 @@ GHC == 8.8.4 GHC == 8.10.7 GHC == 9.0.1 + GHC == 9.0.2 GHC == 9.2.1 + GHC == 9.2.2 extra-source-files: CHANGELOG.md README.md + doc/release-notes/2.6.2.1.md doc/release-notes/2.6.2.md doc/release-notes/2.6.1.3.md doc/release-notes/2.6.1.2.md @@ -88,7 +91,9 @@ stack-8.8.4.yaml stack-8.10.7.yaml stack-9.0.1.yaml + stack-9.0.2.yaml stack-9.2.1.yaml + stack-9.2.2.yaml data-dir: src/data data-files: emacs-mode/*.el @@ -143,7 +148,7 @@ source-repository this type: git location: https://github.com/agda/agda.git - tag: v2.6.2.1 + tag: v2.6.2.2 flag cpphs default: False @@ -219,7 +224,7 @@ , deepseq >= 1.4.2.0 && < 1.5 , directory >= 1.2.6.2 && < 1.4 , edit-distance >= 0.2.1.2 && < 0.3 - , equivalence >= 0.3.2 && < 0.4 + , equivalence >= 0.3.2 && < 0.5 -- exceptions-0.8 instead of 0.10 because of stack , exceptions >= 0.8 && < 0.11 , filepath >= 1.4.1.0 && < 1.5 @@ -237,11 +242,9 @@ , 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 - -- mtl-2.1 contains a severe bug. - -- -- mtl >= 2.2 && < 2.2.1 doesn't export Control.Monad.Except. -- Need mtl 2.2.2 for export of Control.Monad.IdentityT (ghc 8.2.2+) - , mtl >= 2.2.1 && < 2.3 + , mtl >= 2.2.1 && < 2.4 , murmur-hash >= 0.1 && < 0.2 , parallel >= 3.2.2.0 && < 3.3 , pretty >= 1.1.3.3 && < 1.2 @@ -251,13 +254,19 @@ , stm >= 2.4.4 && < 2.6 , strict >= 0.3.2 && < 0.5 , template-haskell >= 2.11.0.0 && < 2.19 - , text >= 1.2.3.0 && < 1.3 + , text >= 1.2.3.0 && < 2.1 , 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.* + -- Andreas, 2022-02-02, issue #5659: + -- Build failure with transformers-0.6.0.{0,1,2} and GHC 8.6. + -- Transformers-0.6.0.3 might restored GHC 8.6 buildability. + if impl(ghc == 8.6.*) + build-depends: transformers < 0.6 || >= 0.6.0.3 + -- Andreas, 2021-03-10: -- All packages we depend upon should be mentioned in an unconditional -- build-depends field, but additional restrictions on their @@ -793,8 +802,8 @@ -- GHC 8.2.1 RC1). -- Nothing is used from the following package, - -- except for the prelude. - , base >= 4.9.0.0 && < 6 + -- except for the Prelude. + , base default-language: Haskell2010 -- If someone installs Agda with the setuid bit set, then the -- presence of +RTS may be a security problem (see GHC bug #3910). diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,149 +1,109 @@ -Release notes for Agda version 2.6.2.1 +Release notes for Agda version 2.6.2.2 ====================================== Highlights ---------- -* Agda 2.6.2.1 catches up to changes in the Haskell ecosystem - (GHC 9.2.1, `aeson-2.0`, `hashable-1.4.`). +* Agda 2.6.2.2 catches up to changes in the Haskell ecosystem + (`bytestring-0.11.2.0`, `mtl-2.3-rc3/4`, `text-icu-0.8.0.1`, + stackage `lts-19.0` and `nightly`). +* Fixes inconsistency [#5838](https://github.com/agda/agda/issues/5838) + in `--cubical`. + * 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) + - [#5809](https://github.com/agda/agda/issues/5809): + internal error with `--irrelevant-projections`. + * 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). + - [#5705](https://github.com/agda/agda/issues/5705) and + [#5706](https://github.com/agda/agda/issues/5706): + inconsistency from universe level `Int` overflow. -* Feature preview: `--ghc-strict`. + - [#5784](https://github.com/agda/agda/issues/5784): + `primEraseEquality` does not compute. -Installation and infrastructure -------------------------------- + - [#5805](https://github.com/agda/agda/issues/5805): + internal error involving holes and `with`. -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: + - [#5819](https://github.com/agda/agda/issues/5819): + internal error when reducing in termination checker. - - 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). +* Other + [fixes](https://github.com/agda/agda/issues?q=is%3Aissue+milestone%3A2.6.2.2+is%3Aclosed) + and improvements (see below). -Agda 2.6.2.1 has been adapted to recent changes in the Haskell ecosystem, including: +Installation and infrastructure +------------------------------- - - `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` +Agda supports GHC versions 8.0.2 to 9.2.2. -Compiler backends ------------------ +* UTF-8 encoding is now used for the `libraries` and `executables` + configuration files (issue + [#5741](https://github.com/agda/agda/issues/5741)). -* Both the GHC and JS backends now refuse to compile code that uses - `--cubical`. +Language +-------- -* 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. +* `macro` definitions can now be used even when they are declared as erased + (PR [#5744](https://github.com/agda/agda/pull/5744)). + For example, this is now accepted: + ```agda + macro + @0 trivial : Term → TC ⊤ + trivial = unify (con (quote refl) []) - 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. + test : 42 ≡ 42 + test = trivial + ``` - This feature is experimental. +* Fixed inconsistent `--cubical` reductions for `transp`: + issue [#5838](https://github.com/agda/agda/issues/5838). -* The new option `--ghc-strict`, which is inspired by the GHC language - extension `Strict`, makes the GHC backend generate mostly strict - code. +* Fixed issues with reflection: - Functions might not be strict in unused arguments. + - [#5762](https://github.com/agda/agda/issues/5762): + do not eagerly check existence of commands in `executables` file. - Function definitions coming from `COMPILE GHC` pragmas are not - affected. + - [#5695](https://github.com/agda/agda/issues/5695): + fix `elaborate-and-give` interaction command. - This flag implies `--ghc-strict-data`, and the exceptions of that - flag applies to this flag as well. + - [#5700](https://github.com/agda/agda/issues/5700): + scope of metas created during macro expansion. - Note that this option requires the use of GHC 9 or later. + - [#5712](https://github.com/agda/agda/issues/5712): + internal error with tactics on record fields of function type. - This feature is experimental. +* Fixed issues with instance search: -* 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). + - [#5583](https://github.com/agda/agda/issues/5583): + constructor instances from parameterized modules. -LaTeX backend -------------- + - [#5787](https://github.com/agda/agda/issues/5787): + erased instance arguments. -* Files `agda.sty` and `postprocess-latex.pl` are now found in the `latex/` - subdirectory of the Agda data directory (`agda --print-agda-dir`). +* Fixed issue [#5683](https://github.com/agda/agda/issues/5683) with + generalization in `let`. -* `agda.sty` is now versioned (printed to the `.log` file by `latex`) - (see [#5473](https://github.com/agda/agda/issues/5473)). +Compiler backends +----------------- -* 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)). +* `.hs` files generated by the GHC backend now switch off the + `warn-overlapping-patterns` warning (issue + [#5758](https://github.com/agda/agda/issues/5758)). -List of closed issues ---------------------- +* The GHC backend now calls `ghc` with environment setting + `GHC_CHARENC=UTF-8` (issue + [#5742](https://github.com/agda/agda/issues/5742)). -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)): +Performance +----------- - - [#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 +* Better caching of interfaces + (issue [#2767](https://github.com/agda/agda/issues/2767)). + +* Various performance improvements concerning meta-variables: + issue [#5388](https://github.com/agda/agda/issues/5388) + and PR [#5733](https://github.com/agda/agda/pull/5733). diff --git a/LICENSE b/LICENSE --- a/LICENSE +++ b/LICENSE @@ -1,4 +1,4 @@ -Copyright (c) 2005-2021 remains with the authors. +Copyright (c) 2005-2022 remains with the authors. Agda 2 was originally written by Ulf Norell, partially based on code from Agda 1 by Catarina Coquand and Makoto Takeyama, and from Agdalight by Ulf Norell and Andreas Abel. diff --git a/doc/release-notes/2.6.2.1.md b/doc/release-notes/2.6.2.1.md new file mode 100644 --- /dev/null +++ b/doc/release-notes/2.6.2.1.md @@ -0,0 +1,149 @@ +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 diff --git a/src/data/emacs-mode/agda2-mode-pkg.el b/src/data/emacs-mode/agda2-mode-pkg.el --- a/src/data/emacs-mode/agda2-mode-pkg.el +++ b/src/data/emacs-mode/agda2-mode-pkg.el @@ -1,3 +1,3 @@ -(define-package "agda2-mode" "2.6.2.1" +(define-package "agda2-mode" "2.6.2.2" "interactive development for Agda, a dependently typed functional programming language" '((emacs "24.3") (annotation "1.0") (eri "1.0"))) diff --git a/src/data/emacs-mode/agda2-mode.el b/src/data/emacs-mode/agda2-mode.el --- a/src/data/emacs-mode/agda2-mode.el +++ b/src/data/emacs-mode/agda2-mode.el @@ -28,7 +28,7 @@ ;;; Code: -(defvar agda2-version "2.6.2.1" +(defvar agda2-version "2.6.2.2" "The version of the Agda mode. Note that the same version of the Agda executable must be used.") diff --git a/src/data/latex/agda.sty b/src/data/latex/agda.sty --- a/src/data/latex/agda.sty +++ b/src/data/latex/agda.sty @@ -6,7 +6,7 @@ % !!! 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] + [2021/07/14 version 2.6.2.2 Formatting LaTeX generated by Agda] \RequirePackage{ifxetex, ifluatex, xifthen, xcolor, polytable, etoolbox, calc, environ, xparse, xkeyval} diff --git a/src/data/lib/prim/Agda/Builtin/Cubical/HCompU.agda b/src/data/lib/prim/Agda/Builtin/Cubical/HCompU.agda --- a/src/data/lib/prim/Agda/Builtin/Cubical/HCompU.agda +++ b/src/data/lib/prim/Agda/Builtin/Cubical/HCompU.agda @@ -1,4 +1,4 @@ -{-# OPTIONS --cubical --safe --no-sized-types --no-guardedness +{-# OPTIONS --erased-cubical --safe --no-sized-types --no-guardedness --no-subtyping #-} module Agda.Builtin.Cubical.HCompU where diff --git a/src/data/lib/prim/Agda/Builtin/Cubical/Id.agda b/src/data/lib/prim/Agda/Builtin/Cubical/Id.agda --- a/src/data/lib/prim/Agda/Builtin/Cubical/Id.agda +++ b/src/data/lib/prim/Agda/Builtin/Cubical/Id.agda @@ -1,4 +1,4 @@ -{-# OPTIONS --cubical --safe --no-sized-types --no-guardedness +{-# OPTIONS --erased-cubical --safe --no-sized-types --no-guardedness --no-subtyping #-} module Agda.Builtin.Cubical.Id where diff --git a/src/data/lib/prim/Agda/Builtin/Cubical/Path.agda b/src/data/lib/prim/Agda/Builtin/Cubical/Path.agda --- a/src/data/lib/prim/Agda/Builtin/Cubical/Path.agda +++ b/src/data/lib/prim/Agda/Builtin/Cubical/Path.agda @@ -1,4 +1,4 @@ -{-# OPTIONS --cubical --safe --no-sized-types --no-guardedness +{-# OPTIONS --erased-cubical --safe --no-sized-types --no-guardedness --no-subtyping #-} module Agda.Builtin.Cubical.Path where diff --git a/src/data/lib/prim/Agda/Builtin/Cubical/Sub.agda b/src/data/lib/prim/Agda/Builtin/Cubical/Sub.agda --- a/src/data/lib/prim/Agda/Builtin/Cubical/Sub.agda +++ b/src/data/lib/prim/Agda/Builtin/Cubical/Sub.agda @@ -1,4 +1,4 @@ -{-# OPTIONS --cubical --safe --no-sized-types --no-guardedness +{-# OPTIONS --erased-cubical --safe --no-sized-types --no-guardedness --no-subtyping #-} module Agda.Builtin.Cubical.Sub where diff --git a/src/data/lib/prim/Agda/Primitive/Cubical.agda b/src/data/lib/prim/Agda/Primitive/Cubical.agda --- a/src/data/lib/prim/Agda/Primitive/Cubical.agda +++ b/src/data/lib/prim/Agda/Primitive/Cubical.agda @@ -1,4 +1,4 @@ -{-# OPTIONS --cubical --no-subtyping #-} +{-# OPTIONS --erased-cubical --no-subtyping #-} module Agda.Primitive.Cubical where diff --git a/src/full/Agda/Auto/Auto.hs b/src/full/Agda/Auto/Auto.hs --- a/src/full/Agda/Auto/Auto.hs +++ b/src/full/Agda/Auto/Auto.hs @@ -7,7 +7,9 @@ import Prelude hiding (null) +import Control.Monad ( filterM, forM, guard, join, when ) import Control.Monad.Except +import Control.Monad.IO.Class ( MonadIO(..) ) import Control.Monad.State import qualified Data.List as List diff --git a/src/full/Agda/Auto/CaseSplit.hs b/src/full/Agda/Auto/CaseSplit.hs --- a/src/full/Agda/Auto/CaseSplit.hs +++ b/src/full/Agda/Auto/CaseSplit.hs @@ -1,6 +1,12 @@ module Agda.Auto.CaseSplit where +import Control.Monad.State as St hiding (lift) +import Control.Monad.Reader as Rd hiding (lift) +import qualified Control.Monad.State as St +import Control.Monad.IO.Class ( MonadIO(..) ) + +import Data.Function import Data.IORef import Data.Tuple (swap) import Data.List (elemIndex) @@ -8,10 +14,6 @@ import Data.Monoid ((<>), Sum(..)) import qualified Data.Set as Set import qualified Data.IntMap as IntMap -import Control.Monad.State as St hiding (lift) -import Control.Monad.Reader as Rd hiding (lift) -import qualified Control.Monad.State as St -import Data.Function import Agda.Syntax.Common (Hiding(..)) import Agda.Auto.NarrowingSearch diff --git a/src/full/Agda/Auto/Convert.hs b/src/full/Agda/Auto/Convert.hs --- a/src/full/Agda/Auto/Convert.hs +++ b/src/full/Agda/Auto/Convert.hs @@ -1,7 +1,9 @@ module Agda.Auto.Convert where +import Control.Monad ( when ) import Control.Monad.Except +import Control.Monad.IO.Class ( MonadIO(..) ) import Control.Monad.State import Data.Bifunctor (first) diff --git a/src/full/Agda/Auto/NarrowingSearch.hs b/src/full/Agda/Auto/NarrowingSearch.hs --- a/src/full/Agda/Auto/NarrowingSearch.hs +++ b/src/full/Agda/Auto/NarrowingSearch.hs @@ -1,9 +1,12 @@ module Agda.Auto.NarrowingSearch where +import Control.Monad ( foldM, when ) +import Control.Monad.State ( MonadState(..), modify, StateT, evalStateT, runStateT ) +import Control.Monad.Trans ( lift ) + import Data.IORef hiding (writeIORef, modifyIORef) import qualified Data.IORef as NoUndo (writeIORef, modifyIORef) -import Control.Monad.State import Agda.Utils.Impossible import Agda.Utils.Empty diff --git a/src/full/Agda/Compiler/Backend.hs b/src/full/Agda/Compiler/Backend.hs --- a/src/full/Agda/Compiler/Backend.hs +++ b/src/full/Agda/Compiler/Backend.hs @@ -22,7 +22,8 @@ ) where import Control.DeepSeq -import Control.Monad.State +import Control.Monad ( (<=<) ) +import Control.Monad.Trans ( lift ) import Control.Monad.Trans.Maybe import qualified Data.List as List diff --git a/src/full/Agda/Compiler/CallCompiler.hs b/src/full/Agda/Compiler/CallCompiler.hs --- a/src/full/Agda/Compiler/CallCompiler.hs +++ b/src/full/Agda/Compiler/CallCompiler.hs @@ -32,10 +32,13 @@ -- ^ The path to the compiler -> [String] -- ^ Command-line arguments. + -> Maybe TextEncoding + -- ^ Use the given text encoding, if any, when reading the output + -- from the process (stdout and stderr). -> TCM () -callCompiler doCall cmd args = +callCompiler doCall cmd args enc = if doCall then do - merrors <- callCompiler' cmd args + merrors <- callCompiler' cmd args enc case merrors of Nothing -> return () Just errors -> typeError (CompilationError errors) @@ -49,8 +52,11 @@ -- ^ The path to the compiler -> [String] -- ^ Command-line arguments. + -> Maybe TextEncoding + -- ^ Use the given text encoding, if any, when reading the output + -- from the process (stdout and stderr). -> TCM (Maybe String) -callCompiler' cmd args = do +callCompiler' cmd args enc = do reportSLn "compile.cmd" 1 $ "Calling: " ++ unwords (cmd : args) (_, out, err, p) <- liftIO $ createProcess @@ -65,6 +71,9 @@ Just out -> forkTCM $ do -- The handle should be in text mode. liftIO $ hSetBinaryMode out False + case enc of + Nothing -> return () + Just enc -> liftIO $ hSetEncoding out enc progressInfo <- liftIO $ hGetContents out mapM_ (reportSLn "compile.output" 1) $ lines progressInfo @@ -73,6 +82,9 @@ Just err -> do -- The handle should be in text mode. hSetBinaryMode err False + case enc of + Nothing -> return () + Just enc -> liftIO $ hSetEncoding err enc hGetContents err exitcode <- liftIO $ do diff --git a/src/full/Agda/Compiler/MAlonzo/Compiler.hs b/src/full/Agda/Compiler/MAlonzo/Compiler.hs --- a/src/full/Agda/Compiler/MAlonzo/Compiler.hs +++ b/src/full/Agda/Compiler/MAlonzo/Compiler.hs @@ -3,9 +3,12 @@ import Control.Arrow (second) import Control.DeepSeq -import Control.Monad.Except (throwError) -import Control.Monad.Reader -import Control.Monad.Writer hiding ((<>)) +import Control.Monad +import Control.Monad.Except ( throwError ) +import Control.Monad.IO.Class ( MonadIO(..) ) +import Control.Monad.Reader ( MonadReader(..), asks, ReaderT, runReaderT, withReaderT) +import Control.Monad.Trans ( lift ) +import Control.Monad.Writer ( MonadWriter(..), WriterT, runWriterT ) import qualified Data.HashSet as HashSet import qualified Data.List as List @@ -24,7 +27,9 @@ import qualified Agda.Utils.Haskell.Syntax as HS import System.Directory (createDirectoryIfMissing) +import System.Environment (setEnv) import System.FilePath hiding (normalise) +import System.IO (utf8) import Agda.Compiler.CallCompiler import Agda.Compiler.Common @@ -68,6 +73,7 @@ import Agda.Utils.Maybe import Agda.Utils.Monad import Agda.Utils.Pretty (prettyShow, render) +import Agda.Utils.Singleton import qualified Agda.Utils.IO.UTF8 as UTF8 import Agda.Utils.String @@ -1207,7 +1213,16 @@ -- Note that GHC assumes that sources use ASCII or UTF-8. out <- snd <$> outFileAndDir m strict <- optGhcStrict <$> askGhcOpts - let p = HS.LanguagePragma $ List.map HS.Ident $ + let languagePragmas = + List.map (HS.LanguagePragma . singleton . HS.Ident) $ + List.sort $ + [ "QualifiedDo" | strict ] ++ + -- If --ghc-strict is used, then the language extension + -- QualifiedDo is activated. At the time of writing no + -- code is generated that depends on this extension + -- (except for the pragmas), but --ghc-strict is broken + -- with at least some versions of GHC prior to version 9, + -- and QualifiedDo was introduced with GHC 9. [ "BangPatterns" , "EmptyDataDecls" , "EmptyCase" @@ -1217,22 +1232,23 @@ , "RankNTypes" , "PatternSynonyms" , "OverloadedStrings" - ] ++ - -- If --ghc-strict is used, then the language extension - -- QualifiedDo is activated. At the time of writing no - -- code is generated that depends on this extension - -- (except for the pragmas), but --ghc-strict is broken - -- with at least some versions of GHC prior to version 9, - -- and QualifiedDo was introduced with GHC 9. - if strict - then ["QualifiedDo"] - else [] + ] + let ghcOptions = + List.map HS.OtherPragma + [ "" -- to separate from LANGUAGE pragmas + , "{-# OPTIONS_GHC -Wno-overlapping-patterns #-}" + -- Andreas, 2022-01-26, issue #5758: + -- Place this in generated file rather than + -- passing it only when calling GHC from within Agda. + -- This will silence the warning for the Agda-generated .hs + -- files while it can be on for other .hs files in the same + -- project. (E.g., when using cabal/stack to compile.) + ] liftIO $ UTF8.writeFile out $ (++ "\n") $ prettyPrint $ -- TODO: It might make sense to skip bang patterns for the unused -- arguments of the "non-stripped" functions. - (if strict then makeStrict else id) $ - HS.Module m (p : ps) imp ds - where + applyWhen strict makeStrict $ + HS.Module m (concat [languagePragmas, ghcOptions, ps]) imp ds outFileAndDir :: MonadGHCIO m => HS.ModuleName -> m (FilePath, FilePath) outFileAndDir m = do @@ -1257,9 +1273,7 @@ opts <- askGhcOpts hsmod <- prettyPrint <$> curHsMod agdaMod <- curAgdaMod - let outputName = case mnameToList agdaMod of - [] -> __IMPOSSIBLE__ - m:ms -> last1 m ms + let outputName = lastWithDefault __IMPOSSIBLE__ $ mnameToList agdaMod (mdir, fp) <- curOutFileAndDir let ghcopts = optGhcFlags opts @@ -1282,14 +1296,15 @@ [ fp , "--make" , "-fwarn-incomplete-patterns" - , "-fno-warn-overlapping-patterns" ] args = overridableArgs ++ ghcopts ++ otherArgs let ghcBin = optGhcBin opts + -- Make GHC use UTF-8 when writing to stdout and stderr. + liftIO $ setEnv "GHC_CHARENC" "UTF-8" -- Note: Some versions of GHC use stderr for progress reports. For -- those versions of GHC we don't print any progress information -- unless an error is encountered. let doCall = optGhcCallGhc opts - liftTCM $ callCompiler doCall ghcBin args + liftTCM $ callCompiler doCall ghcBin args (Just utf8) diff --git a/src/full/Agda/Compiler/MAlonzo/Pretty.hs b/src/full/Agda/Compiler/MAlonzo/Pretty.hs --- a/src/full/Agda/Compiler/MAlonzo/Pretty.hs +++ b/src/full/Agda/Compiler/MAlonzo/Pretty.hs @@ -17,12 +17,15 @@ instance Pretty HS.Module where pretty (HS.Module m pragmas imps decls) = - vcat [ vcat $ map pretty pragmas - , "module" <+> pretty m <+> "where" - , "" - , vcat $ map pretty imps - , "" - , vcat $ map pretty decls ] + vcat $ concat + [ map pretty pragmas + , [ "" | not $ null pragmas ] + , [ "module" <+> pretty m <+> "where" ] + , [ "" ] + , map pretty imps + , [ "" ] + , map pretty decls + ] instance Pretty HS.ModulePragma where pretty (HS.LanguagePragma ps) = diff --git a/src/full/Agda/Compiler/ToTreeless.hs b/src/full/Agda/Compiler/ToTreeless.hs --- a/src/full/Agda/Compiler/ToTreeless.hs +++ b/src/full/Agda/Compiler/ToTreeless.hs @@ -4,8 +4,10 @@ , closedTermToTreeless ) where -import Control.Arrow (first) -import Control.Monad.Reader +import Control.Arrow ( first ) +import Control.Monad ( filterM, foldM, forM, zipWithM ) +import Control.Monad.Reader ( MonadReader(..), asks, ReaderT, runReaderT ) +import Control.Monad.Trans ( lift ) import Data.Maybe import Data.Map (Map) @@ -479,6 +481,7 @@ recConFromProj :: QName -> TCM I.ConHead recConFromProj q = do caseMaybeM (isProjection q) __IMPOSSIBLE__ $ \ proj -> do + -- Get the record type name @d@ from the projection. let d = unArg $ projFromType proj getRecordConstructor d diff --git a/src/full/Agda/Compiler/Treeless/Simplify.hs b/src/full/Agda/Compiler/Treeless/Simplify.hs --- a/src/full/Agda/Compiler/Treeless/Simplify.hs +++ b/src/full/Agda/Compiler/Treeless/Simplify.hs @@ -1,7 +1,8 @@ module Agda.Compiler.Treeless.Simplify (simplifyTTerm) where -import Control.Arrow (second, (***)) -import Control.Monad.Reader +import Control.Arrow ( (***), second ) +import Control.Monad ( (>=>), guard ) +import Control.Monad.Reader ( MonadReader(..), asks, Reader, runReader ) import qualified Data.List as List import Agda.Syntax.Treeless diff --git a/src/full/Agda/Interaction/AgdaTop.hs b/src/full/Agda/Interaction/AgdaTop.hs --- a/src/full/Agda/Interaction/AgdaTop.hs +++ b/src/full/Agda/Interaction/AgdaTop.hs @@ -2,7 +2,11 @@ ( repl ) where -import Control.Monad.State +import Control.Monad ( unless ) +import Control.Monad.IO.Class ( MonadIO(..) ) +import Control.Monad.State ( evalStateT, runStateT ) +import Control.Monad.Trans ( lift ) + import Data.Char import Data.Maybe import System.IO diff --git a/src/full/Agda/Interaction/Base.hs b/src/full/Agda/Interaction/Base.hs --- a/src/full/Agda/Interaction/Base.hs +++ b/src/full/Agda/Interaction/Base.hs @@ -5,6 +5,8 @@ import Control.Concurrent.STM.TChan import Control.Concurrent.STM.TVar + +import Control.Monad ( mplus, liftM2, liftM4 ) import Control.Monad.Except import Control.Monad.Identity import Control.Monad.State diff --git a/src/full/Agda/Interaction/BasicOps.hs b/src/full/Agda/Interaction/BasicOps.hs --- a/src/full/Agda/Interaction/BasicOps.hs +++ b/src/full/Agda/Interaction/BasicOps.hs @@ -6,7 +6,8 @@ import Prelude hiding (null) -import Control.Arrow (first) +import Control.Arrow ( first ) +import Control.Monad ( (>=>), forM, guard ) import Control.Monad.Except import Control.Monad.Reader import Control.Monad.State @@ -112,63 +113,61 @@ withMetaInfo mi $ concreteToAbstract (clScope mi) e -giveExpr :: UseForce -> Maybe InteractionId -> MetaId -> Expr -> TCM () --- When translator from internal to abstract is given, this function might return --- the expression returned by the type checker. +-- Type check the given expression and assign its value to the meta +-- Precondition: we are in the context where the given meta was created. +giveExpr :: UseForce -> Maybe InteractionId -> MetaId -> Expr -> TCM Term giveExpr force mii mi e = do mv <- lookupMeta mi - -- In the context (incl. signature) of the meta variable, - -- type check expression and assign meta - withMetaInfo (getMetaInfo mv) $ do - let t = case mvJudgement mv of - IsSort{} -> __IMPOSSIBLE__ - HasType _ _ t -> t - reportSDoc "interaction.give" 20 $ - "give: meta type =" TP.<+> prettyTCM t - -- Here, we must be in the same context where the meta was created. - -- Thus, we can safely apply its type to the context variables. - ctx <- getContextArgs - t' <- t `piApplyM` permute (takeP (length ctx) $ mvPermutation mv) ctx - traceCall (CheckExprCall CmpLeq e t') $ do - reportSDoc "interaction.give" 20 $ do - a <- asksTC envAbstractMode - TP.hsep - [ TP.text ("give(" ++ show a ++ "): instantiated meta type =") - , prettyTCM t' - ] - -- Andreas, 2020-05-27 AIM XXXII, issue #4679 - -- Clear envMutualBlock since cubical only executes - -- certain checks (checkIApplyConfluence) for an extended lambda - -- when not in a mutual block. - v <- locallyTC eMutualBlock (const Nothing) $ - checkExpr e t' - case mvInstantiation mv of + let t = case mvJudgement mv of + IsSort{} -> __IMPOSSIBLE__ + HasType _ _ t -> t + reportSDoc "interaction.give" 20 $ + "give: meta type =" TP.<+> prettyTCM t + -- Here, we must be in the same context where the meta was created. + -- Thus, we can safely apply its type to the context variables. + ctx <- getContextArgs + t' <- t `piApplyM` permute (takeP (length ctx) $ mvPermutation mv) ctx + traceCall (CheckExprCall CmpLeq e t') $ do + reportSDoc "interaction.give" 20 $ do + a <- asksTC envAbstractMode + TP.hsep + [ TP.text ("give(" ++ show a ++ "): instantiated meta type =") + , prettyTCM t' + ] + -- Andreas, 2020-05-27 AIM XXXII, issue #4679 + -- Clear envMutualBlock since cubical only executes + -- certain checks (checkIApplyConfluence) for an extended lambda + -- when not in a mutual block. + v <- locallyTC eMutualBlock (const Nothing) $ + checkExpr e t' + case mvInstantiation mv of - InstV{} -> unlessM ((Irrelevant ==) <$> asksTC getRelevance) $ do - v' <- instantiate $ MetaV mi $ map Apply ctx - reportSDoc "interaction.give" 20 $ TP.sep - [ "meta was already set to value v' = " TP.<+> prettyTCM v' - , "now comparing it to given value v = " TP.<+> prettyTCM v - , "in context " TP.<+> inTopContext (prettyTCM ctx) - ] - equalTerm t' v v' + InstV{} -> unlessM ((Irrelevant ==) <$> asksTC getRelevance) $ do + v' <- instantiate $ MetaV mi $ map Apply ctx + reportSDoc "interaction.give" 20 $ TP.sep + [ "meta was already set to value v' = " TP.<+> prettyTCM v' + , "now comparing it to given value v = " TP.<+> prettyTCM v + , "in context " TP.<+> inTopContext (prettyTCM ctx) + ] + equalTerm t' v v' - _ -> do -- updateMeta mi v - reportSLn "interaction.give" 20 "give: meta unassigned, assigning..." - args <- getContextArgs - nowSolvingConstraints $ assign DirEq mi args v (AsTermsOf t') + _ -> do -- updateMeta mi v + reportSLn "interaction.give" 20 "give: meta unassigned, assigning..." + args <- getContextArgs + nowSolvingConstraints $ assign DirEq mi args v (AsTermsOf t') - reportSDoc "interaction.give" 20 $ "give: meta variable updated!" - unless (force == WithForce) $ redoChecks mii - wakeupConstraints mi - solveSizeConstraints DontDefaultToInfty - cubical <- isJust . optCubical <$> pragmaOptions - -- don't double check with cubical, because it gets in the way too often. - unless (cubical || force == WithForce) $ do - -- Double check. - reportSDoc "interaction.give" 20 $ "give: double checking" - vfull <- instantiateFull v - checkInternal vfull CmpLeq t' + reportSDoc "interaction.give" 20 $ "give: meta variable updated!" + unless (force == WithForce) $ redoChecks mii + wakeupConstraints mi + solveSizeConstraints DontDefaultToInfty + cubical <- isJust . optCubical <$> pragmaOptions + -- don't double check with cubical, because it gets in the way too often. + unless (cubical || force == WithForce) $ do + -- Double check. + reportSDoc "interaction.give" 20 $ "give: double checking" + vfull <- instantiateFull v + checkInternal vfull CmpLeq t' + return v -- | After a give, redo termination etc. checks for function which was complemented. redoChecks :: Maybe InteractionId -> TCM () @@ -202,7 +201,8 @@ reportSDoc "interaction.give" 10 $ "giving expression" TP.<+> prettyTCM e reportSDoc "interaction.give" 50 $ TP.text $ show $ deepUnscope e -- Try to give mi := e - do setMetaOccursCheck mi DontRunMetaOccursCheck -- #589, #2710: Allow giving recursive solutions. + _ <- withInteractionId ii $ do + setMetaOccursCheck mi DontRunMetaOccursCheck -- #589, #2710: Allow giving recursive solutions. giveExpr force (Just ii) mi e `catchError` \ case -- Turn PatternErr into proper error: @@ -212,6 +212,32 @@ removeInteractionPoint ii return e +-- | Try to fill hole by elaborated expression. +elaborate_give + :: Rewrite -- ^ Normalise result? + -> UseForce -- ^ Skip safety checks? + -> InteractionId -- ^ Hole. + -> Maybe Range + -> Expr -- ^ The expression to give. + -> TCM Expr -- ^ If successful, return the elaborated expression. +elaborate_give norm force ii mr e = withInteractionId ii $ do + -- if Range is given, update the range of the interaction meta + mi <- lookupInteractionId ii + whenJust mr $ updateMetaVarRange mi + reportSDoc "interaction.give" 10 $ "giving expression" TP.<+> prettyTCM e + reportSDoc "interaction.give" 50 $ TP.text $ show $ deepUnscope e + -- Try to give mi := e + v <- withInteractionId ii $ do + setMetaOccursCheck mi DontRunMetaOccursCheck -- #589, #2710: Allow giving recursive solutions. + locallyTC eCurrentlyElaborating (const True) $ + giveExpr force (Just ii) mi e + `catchError` \ case + -- Turn PatternErr into proper error: + PatternErr{} -> typeError . GenericDocError =<< do + withInteractionId ii $ "Failed to give" TP.<+> prettyTCM e + err -> throwError err + nv <- normalForm norm v + locallyTC ePrintMetasBare (const True) $ reify nv -- | Try to refine hole by expression @e@. -- @@ -454,6 +480,7 @@ reify (CheckMetaInst m) = do t <- jMetaType . mvJudgement <$> lookupMeta m OfType <$> reify (MetaV m []) <*> reify t + reify (CheckType t) = JustType <$> reify t reify (UsableAtModality mod t) = UsableAtMod mod <$> reify t instance (Pretty a, Pretty b) => Pretty (OutputForm a b) where @@ -618,6 +645,7 @@ HasPTSRule a b -> Nothing UnquoteTactic{} -> Nothing CheckMetaInst{} -> Nothing + CheckType t -> isMeta (unEl t) CheckLockedVars t _ _ _ -> isMeta t UsableAtModality _ t -> isMeta t @@ -1002,16 +1030,6 @@ mi <- getMetaInfo <$> lookupMeta m withMetaInfo mi $ typeInCurrent norm e - -withInteractionId :: InteractionId -> TCM a -> TCM a -withInteractionId i ret = do - m <- lookupInteractionId i - withMetaId m ret - -withMetaId :: MetaId -> TCM a -> TCM a -withMetaId m ret = do - mv <- lookupMeta m - withMetaInfo' mv ret -- | The intro tactic. -- diff --git a/src/full/Agda/Interaction/CommandLine.hs b/src/full/Agda/Interaction/CommandLine.hs --- a/src/full/Agda/Interaction/CommandLine.hs +++ b/src/full/Agda/Interaction/CommandLine.hs @@ -3,7 +3,9 @@ ( runInteractionLoop ) where +import Control.Monad import Control.Monad.Except +import Control.Monad.IO.Class ( MonadIO(..) ) import Control.Monad.State import Control.Monad.Reader diff --git a/src/full/Agda/Interaction/EmacsTop.hs b/src/full/Agda/Interaction/EmacsTop.hs --- a/src/full/Agda/Interaction/EmacsTop.hs +++ b/src/full/Agda/Interaction/EmacsTop.hs @@ -7,7 +7,11 @@ , prettyTypeOfMeta ) where -import Control.Monad.State hiding (state) +import Control.Monad +import Control.Monad.IO.Class ( MonadIO(..) ) +import Control.Monad.State ( evalStateT ) +import Control.Monad.Trans ( lift ) + import qualified Data.List as List import Agda.Syntax.Common @@ -194,7 +198,7 @@ Info_GoalSpecific ii kind -> lispifyGoalSpecificDisplayInfo ii kind lispifyGoalSpecificDisplayInfo :: InteractionId -> GoalDisplayInfo -> TCM [Lisp String] -lispifyGoalSpecificDisplayInfo ii kind = localTCState $ B.withInteractionId ii $ +lispifyGoalSpecificDisplayInfo ii kind = localTCState $ withInteractionId ii $ case kind of Goal_HelperFunction helperType -> do doc <- inTopContext $ prettyATop helperType diff --git a/src/full/Agda/Interaction/FindFile.hs b/src/full/Agda/Interaction/FindFile.hs --- a/src/full/Agda/Interaction/FindFile.hs +++ b/src/full/Agda/Interaction/FindFile.hs @@ -39,7 +39,8 @@ import Agda.TypeChecking.Monad.Base import Agda.TypeChecking.Monad.Benchmark (billTo) import qualified Agda.TypeChecking.Monad.Benchmark as Bench -import Agda.TypeChecking.Monad.Options (getIncludeDirs, libToTCM) +import {-# SOURCE #-} Agda.TypeChecking.Monad.Options + (getIncludeDirs, libToTCM) import Agda.TypeChecking.Warnings (runPM) import Agda.Version ( version ) diff --git a/src/full/Agda/Interaction/Highlighting/Dot/Backend.hs b/src/full/Agda/Interaction/Highlighting/Dot/Backend.hs --- a/src/full/Agda/Interaction/Highlighting/Dot/Backend.hs +++ b/src/full/Agda/Interaction/Highlighting/Dot/Backend.hs @@ -10,12 +10,13 @@ ) import Control.Monad.Except - ( MonadIO - , ExceptT + ( ExceptT , runExceptT , MonadError(throwError) ) - +import Control.Monad.IO.Class + ( MonadIO(..) + ) import Control.DeepSeq import Data.Map ( Map ) diff --git a/src/full/Agda/Interaction/Highlighting/Dot/Base.hs b/src/full/Agda/Interaction/Highlighting/Dot/Base.hs --- a/src/full/Agda/Interaction/Highlighting/Dot/Base.hs +++ b/src/full/Agda/Interaction/Highlighting/Dot/Base.hs @@ -9,8 +9,10 @@ , Env(..) ) where -import Control.Monad.Reader -import Control.Monad.State +import Control.Monad (liftM2, when) +import Control.Monad.IO.Class (MonadIO(..)) +import Control.Monad.Reader (ReaderT, runReaderT, ask) +import Control.Monad.State (State, execState, get, modify, put) import qualified Data.Map as M import Data.Map(Map) diff --git a/src/full/Agda/Interaction/Highlighting/FromAbstract.hs b/src/full/Agda/Interaction/Highlighting/FromAbstract.hs --- a/src/full/Agda/Interaction/Highlighting/FromAbstract.hs +++ b/src/full/Agda/Interaction/Highlighting/FromAbstract.hs @@ -13,7 +13,8 @@ import Prelude hiding (null) import Control.Applicative -import Control.Monad.Reader +import Control.Monad ( (<=<) ) +import Control.Monad.Reader ( MonadReader(..), asks, Reader, runReader ) import qualified Data.Map as Map import Data.Maybe diff --git a/src/full/Agda/Interaction/Highlighting/LaTeX/Base.hs b/src/full/Agda/Interaction/Highlighting/LaTeX/Base.hs --- a/src/full/Agda/Interaction/Highlighting/LaTeX/Base.hs +++ b/src/full/Agda/Interaction/Highlighting/LaTeX/Base.hs @@ -29,10 +29,13 @@ import Control.Monad (forM_, mapM_, unless, when) import Control.Monad.Trans.Reader as R ( ReaderT(runReaderT)) import Control.Monad.RWS.Strict - ( MonadIO(..), RWST(runRWST) + ( RWST(runRWST) , MonadReader(..), asks , MonadState(..), gets, modify , lift, tell + ) +import Control.Monad.IO.Class + ( MonadIO(..) ) import System.Directory diff --git a/src/full/Agda/Interaction/Imports.hs b/src/full/Agda/Interaction/Imports.hs --- a/src/full/Agda/Interaction/Imports.hs +++ b/src/full/Agda/Interaction/Imports.hs @@ -24,7 +24,9 @@ import Prelude hiding (null) +import Control.Monad ( forM, forM_, void ) import Control.Monad.Except +import Control.Monad.IO.Class ( MonadIO(..) ) import Control.Monad.State import Control.Monad.Trans.Maybe import qualified Control.Exception as E @@ -1194,7 +1196,9 @@ let builtin' = Map.mapWithKey (\ x b -> (x,) . primFunName <$> b) builtin warnings <- getAllWarnings AllWarnings reportSLn "import.iface" 7 " instantiating all meta variables" - i <- instantiateFull Interface + -- Note that the meta-variables in the definitions in "sig" have + -- already been instantiated (by eliminateDeadCode). + i <- instantiateFullExceptForDefinitions Interface { iSourceHash = hashText source , iSource = source , iFileType = fileType diff --git a/src/full/Agda/Interaction/InteractionTop.hs b/src/full/Agda/Interaction/InteractionTop.hs --- a/src/full/Agda/Interaction/InteractionTop.hs +++ b/src/full/Agda/Interaction/InteractionTop.hs @@ -13,12 +13,16 @@ import Control.Concurrent.Async import Control.Concurrent.STM.TChan import Control.Concurrent.STM.TVar -import qualified Control.Exception as E -import Control.Monad.Except -import Control.Monad.Identity -import Control.Monad.Reader -import Control.Monad.State hiding (state) + +import qualified Control.Exception as E + +import Control.Monad +import Control.Monad.Except ( MonadError(..), ExceptT(..), runExceptT ) +import Control.Monad.IO.Class ( MonadIO(..) ) +import Control.Monad.Fail ( MonadFail ) +import Control.Monad.State ( MonadState(..), gets, modify, runStateT ) import Control.Monad.STM +import Control.Monad.Trans ( lift ) import qualified Data.Char as Char import Data.Function @@ -662,7 +666,7 @@ interpret (Cmd_intro pmLambda ii rng _) = do ss <- lift $ B.introTactic pmLambda ii - liftCommandMT (B.withInteractionId ii) $ case ss of + liftCommandMT (withInteractionId ii) $ case ss of [] -> do display_info $ Info_Intro_NotFound [s] -> give_gen WithoutForce ii rng s Intro @@ -728,27 +732,18 @@ interpret (Cmd_helper_function norm ii rng s) = do -- Create type of application of new helper function that would solve the goal. - helperType <- liftLocalState $ B.withInteractionId ii $ inTopContext $ B.metaHelperType norm ii rng s + helperType <- liftLocalState $ withInteractionId ii $ inTopContext $ B.metaHelperType norm ii rng s display_info $ Info_GoalSpecific ii (Goal_HelperFunction helperType) interpret (Cmd_infer norm ii rng s) = do - expr <- liftLocalState $ B.withInteractionId ii $ B.typeInMeta ii norm =<< B.parseExprIn ii rng s + expr <- liftLocalState $ withInteractionId ii $ B.typeInMeta ii norm =<< B.parseExprIn ii rng s display_info $ Info_GoalSpecific ii (Goal_InferredType expr) interpret (Cmd_goal_type norm ii _ _) = display_info $ Info_GoalSpecific ii (Goal_CurrentGoal norm) -interpret (Cmd_elaborate_give norm ii rng s) = do - have <- liftLocalState $ B.withInteractionId ii $ do - expr <- B.parseExprIn ii rng s - goal <- B.typeOfMeta AsIs ii - term <- case goal of - OfType _ ty -> checkExpr expr =<< isType_ ty - _ -> __IMPOSSIBLE__ - nf <- B.normalForm norm term - txt <- localTC (\ e -> e { envPrintMetasBare = True }) (TCP.prettyTCM nf) - return $ show txt - give_gen WithoutForce ii rng have ElaborateGive +interpret (Cmd_elaborate_give norm ii rng s) = + give_gen WithoutForce ii rng s $ ElaborateGive norm interpret (Cmd_goal_type_context norm ii rng s) = cmd_goal_type_context_and GoalOnly norm ii rng s @@ -761,13 +756,13 @@ then return GoalOnly else do typ <- liftLocalState - $ B.withInteractionId ii + $ withInteractionId ii $ B.typeInMeta ii norm =<< B.parseExprIn ii rng s return (GoalAndHave typ) cmd_goal_type_context_and aux norm ii rng s interpret (Cmd_goal_type_context_check norm ii rng s) = do - term <- liftLocalState $ B.withInteractionId ii $ do + term <- liftLocalState $ withInteractionId ii $ do expr <- B.parseExprIn ii rng s goal <- B.typeOfMeta AsIs ii term <- case goal of @@ -777,17 +772,17 @@ cmd_goal_type_context_and (GoalAndElaboration term) norm ii rng s interpret (Cmd_show_module_contents norm ii rng s) = - liftCommandMT (B.withInteractionId ii) $ showModuleContents norm rng s + liftCommandMT (withInteractionId ii) $ showModuleContents norm rng s interpret (Cmd_why_in_scope_toplevel s) = atTopLevel $ whyInScope s interpret (Cmd_why_in_scope ii _range s) = - liftCommandMT (B.withInteractionId ii) $ whyInScope s + liftCommandMT (withInteractionId ii) $ whyInScope s interpret (Cmd_make_case ii rng s) = do (f, casectxt, cs) <- lift $ makeCase ii rng s - liftCommandMT (B.withInteractionId ii) $ do + liftCommandMT (withInteractionId ii) $ do tel <- lift $ lookupSection (qnameModule f) -- don't shadow the names in this telescope unicode <- getsTC $ optUseUnicode . getPragmaOptions pcs :: [Doc] <- lift $ inTopContext $ addContext tel $ mapM prettyA cs @@ -830,7 +825,7 @@ interpret (Cmd_compute cmode ii rng s) = do expr <- liftLocalState $ do e <- B.parseExprIn ii rng $ B.computeWrapInput cmode s - B.withInteractionId ii $ applyWhen (B.computeIgnoreAbstract cmode) ignoreAbstractMode $ B.evalInCurrent cmode e + withInteractionId ii $ applyWhen (B.computeIgnoreAbstract cmode) ignoreAbstractMode $ B.evalInCurrent cmode e display_info $ Info_GoalSpecific ii (Goal_NormalForm cmode expr) interpret Cmd_show_version = display_info Info_Version @@ -950,7 +945,7 @@ --------------------------------------------------------------------------- -- Giving, refining. -data GiveRefine = Give | Refine | Intro | ElaborateGive +data GiveRefine = Give | Refine | Intro | ElaborateGive Rewrite deriving (Eq, Show) -- | A "give"-like action (give, refine, etc). @@ -970,28 +965,28 @@ -> CommandM () give_gen force ii rng s0 giveRefine = do let s = trim s0 - lift $ reportSLn "interaction.give" 20 $ "give_gen " ++ s + reportSLn "interaction.give" 20 $ "give_gen " ++ s -- Andreas, 2015-02-26 if string is empty do nothing rather -- than giving a parse error. unless (null s) $ do let give_ref = case giveRefine of - Give -> B.give - Refine -> B.refine - Intro -> B.refine - ElaborateGive -> B.give + Give -> B.give + Refine -> B.refine + Intro -> B.refine + ElaborateGive norm -> B.elaborate_give norm -- save scope of the interaction point (for printing the given expr. later) - scope <- lift $ getInteractionScope ii + scope <- getInteractionScope ii -- parse string and "give", obtaining an abstract expression -- and newly created interaction points - (time, (ae, ae0, iis)) <- maybeTimed $ lift $ do + (time, (ae, ae0, iis)) <- maybeTimed $ do -- Issue 3000: mark the current hole as solved before giving, to avoid confusing it with potential -- new interaction points introduced by the give. removeInteractionPoint ii mis <- getInteractionPoints reportSLn "interaction.give" 30 $ "interaction points before = " ++ show mis - given <- B.parseExprIn ii rng s - ae <- give_ref force ii Nothing given + given <- lift $ B.parseExprIn ii rng s + ae <- lift $ give_ref force ii Nothing given mis' <- getInteractionPoints reportSLn "interaction.give" 30 $ "interaction points after = " ++ show mis' return (ae, given, mis' List.\\ mis) @@ -999,11 +994,11 @@ insertOldInteractionScope ii scope -- sort the new interaction points and put them into the state -- in replacement of the old interaction point - iis' <- lift $ sortInteractionPoints iis + iis' <- sortInteractionPoints iis modifyTheInteractionPoints $ replace ii iis' -- print abstract expr - ce <- lift $ abstractToConcreteScope scope ae - lift $ reportS "interaction.give" 30 + ce <- abstractToConcreteScope scope ae + reportS "interaction.give" 30 [ "ce = " ++ show ce , "scopePrecedence = " ++ show (scope ^. scopePrecedence) ] @@ -1016,22 +1011,22 @@ -- WRONG: let literally = (giveRefine == Give || null iis) && rng /= noRange -- Ulf, 2015-03-30, if we're doing intro we can't do literal give since -- there is nothing in the hole (issue 1892). - let literally = giveRefine /= Intro && giveRefine /= ElaborateGive && ae == ae0 && rng /= noRange + let literally = (giveRefine == Give || giveRefine == Refine) && ae == ae0 && rng /= noRange -- Ulf, 2014-01-24: This works for give since we're highlighting the string -- that's already in the buffer. Doing it before the give action means that -- the highlighting is moved together with the text when the hole goes away. -- To make it work for refine we'd have to adjust the ranges. - when literally $ lift $ do + when literally $ do l <- asksTC envHighlightingLevel - when (l /= None) $ do + when (l /= None) $ lift $ do printHighlightingInfo KeepHighlighting =<< generateTokenInfoFromString rng s highlightExpr ae putResponse $ Resp_GiveAction ii $ mkNewTxt literally ce - lift $ reportSLn "interaction.give" 30 $ "putResponse GiveAction passed" + reportSLn "interaction.give" 30 $ "putResponse GiveAction passed" -- display new goal set (if not measuring time) maybe (interpret $ Cmd_metas AsIs) (display_info . Info_Time) time - lift $ reportSLn "interaction.give" 30 $ "interpret Cmd_metas passed" + reportSLn "interaction.give" 30 $ "interpret Cmd_metas passed" where -- Substitutes xs for x in ys. replace x xs ys = concatMap (\ y -> if y == x then xs else [y]) ys @@ -1054,7 +1049,9 @@ -- | Sorts interaction points based on their ranges. -sortInteractionPoints :: [InteractionId] -> TCM [InteractionId] +sortInteractionPoints + :: (MonadInteractionPoints m, MonadError TCErr m, MonadFail m) + => [InteractionId] -> m [InteractionId] sortInteractionPoints is = map fst . List.sortBy (compare `on` snd) <$> do forM is $ \ i -> do diff --git a/src/full/Agda/Interaction/JSONTop.hs b/src/full/Agda/Interaction/JSONTop.hs --- a/src/full/Agda/Interaction/JSONTop.hs +++ b/src/full/Agda/Interaction/JSONTop.hs @@ -1,8 +1,10 @@ module Agda.Interaction.JSONTop ( jsonREPL ) where -import Control.Monad.State +import Control.Monad ( (<=<), forM ) +import Control.Monad.IO.Class ( MonadIO(..) ) + import Data.ByteString.Lazy (ByteString) import qualified Data.ByteString.Lazy.Char8 as BS import qualified Data.Text as T @@ -20,13 +22,13 @@ import Agda.Syntax.Common import qualified Agda.Syntax.Concrete as C import Agda.Syntax.Concrete.Name (NameInScope(..), Name) -import Agda.Syntax.Internal (telToList, Dom'(..), Dom, MetaId(..), ProblemId(..), Blocker(..)) -import Agda.Syntax.Position (Range, rangeIntervals, Interval'(..), Position'(..)) +import Agda.Syntax.Internal (telToList, Dom'(..), Dom, MetaId(..), ProblemId(..), Blocker(..), alwaysUnblock) +import Agda.Syntax.Position (Range, rangeIntervals, Interval'(..), Position'(..), noRange) import Agda.VersionCommit import Agda.TypeChecking.Errors (getAllWarningsOfTCErr) -import Agda.TypeChecking.Monad (Comparison(..), inTopContext, TCM, TCErr, TCWarning, NamedMeta(..)) -import Agda.TypeChecking.Monad.MetaVars (getInteractionRange, getMetaRange) +import Agda.TypeChecking.Monad (Comparison(..), inTopContext, TCM, TCErr, TCWarning, NamedMeta(..), withInteractionId) +import Agda.TypeChecking.Monad.MetaVars (getInteractionRange, getMetaRange, withMetaId) import Agda.TypeChecking.Pretty (PrettyTCM(..), prettyTCM) -- borrowed from EmacsTop, for temporarily serialising stuff import Agda.TypeChecking.Pretty.Warning (filterTCWarnings) @@ -113,7 +115,7 @@ , "range" #= intervalsTCM ] where - nameTCM = encodeShow <$> B.withMetaId (nmid m) (prettyATop m) + nameTCM = encodeShow <$> withMetaId (nmid m) (prettyATop m) intervalsTCM = toJSON <$> getMetaRange (nmid m) instance EncodeTCM GiveResult where @@ -241,7 +243,7 @@ [ "range" @= range , "problems" @= problems , "unblocker" @= unblock - , "constraint" #= encodeOC (pure . encodeShow) (pure . encodeShow) oc + , "constraint" #= encodeOC (pure . encodePretty) (pure . encodePretty) oc ] instance EncodeTCM Blocker where @@ -260,7 +262,7 @@ [ "constraints" #= forM constraints encodeTCM ] encodeTCM (Info_AllGoalsWarnings (vis, invis) wes) = kind "AllGoalsWarnings" - [ "visibleGoals" #= forM vis (encodeOC encodeTCM encodePrettyTCM) + [ "visibleGoals" #= forM vis (\i -> withInteractionId (B.outputFormId $ OutputForm noRange [] alwaysUnblock i) $ encodeOC encodeTCM encodePrettyTCM i) , "invisibleGoals" #= forM invis (encodeOC encodeTCM encodePrettyTCM) , "warnings" #= encodeTCM (filterTCWarnings (tcWarnings wes)) , "errors" #= encodeTCM (filterTCWarnings (nonFatalErrors wes)) @@ -323,7 +325,7 @@ ] encodeTCM (Info_GoalSpecific ii info) = kind "GoalSpecific" [ "interactionPoint" @= ii - , "goalInfo" #= encodeGoalSpecific ii info + , "goalInfo" #= withInteractionId ii (encodeGoalSpecific ii info) ] instance EncodeTCM GoalTypeAux where diff --git a/src/full/Agda/Interaction/Library.hs b/src/full/Agda/Interaction/Library.hs --- a/src/full/Agda/Interaction/Library.hs +++ b/src/full/Agda/Interaction/Library.hs @@ -38,10 +38,12 @@ , findLib' ) where -import Control.Arrow ( first , second ) +import Control.Arrow ( first , second ) +import Control.Monad ( filterM, forM ) import Control.Monad.Except import Control.Monad.State import Control.Monad.Writer +import Control.Monad.IO.Class ( MonadIO(..) ) import Data.Char import Data.Data ( Data ) @@ -65,6 +67,7 @@ import Agda.Utils.FileName import Agda.Utils.Functor ( (<&>) ) import Agda.Utils.IO ( catchIO ) +import qualified Agda.Utils.IO.UTF8 as UTF8 import Agda.Utils.List import Agda.Utils.List1 ( List1 ) import qualified Agda.Utils.List1 as List1 @@ -257,7 +260,7 @@ agdaDir <- liftIO getAgdaAppDir let file = agdaDir defaultsFile ifNotM (liftIO $ doesFileExist file) (return []) $ {-else-} do - ls <- liftIO $ map snd . stripCommentLines <$> readFile file + ls <- liftIO $ map snd . stripCommentLines <$> UTF8.readFile file return $ concatMap splitCommas ls `catchIO` \ e -> do raiseErrors' [ OtherError $ unlines ["Failed to read defaults file.", show e] ] @@ -301,7 +304,7 @@ Left err -> raiseErrors' [OtherError err] >> return [] Right file -> do if not (lfExists file) then return [] else do - ls <- liftIO $ stripCommentLines <$> readFile (lfPath file) + ls <- liftIO $ stripCommentLines <$> UTF8.readFile (lfPath file) files <- liftIO $ sequence [ (i, ) <$> expandEnvironmentVariables s | (i, s) <- ls ] parseLibFiles (Just file) $ nubOn snd files `catchIO` \ e -> do @@ -370,7 +373,7 @@ getTrustedExecutables = mkLibM [] $ do file <- liftIO getExecutablesFile if not (efExists file) then return Map.empty else do - es <- liftIO $ stripCommentLines <$> readFile (efPath file) + es <- liftIO $ stripCommentLines <$> UTF8.readFile (efPath file) files <- liftIO $ sequence [ (i, ) <$> expandEnvironmentVariables s | (i, s) <- es ] tmp <- parseExecutablesFile file $ nubOn snd files return tmp @@ -387,26 +390,12 @@ parseExecutablesFile ef files = fmap (Map.fromList . catMaybes) . forM files $ \(ln, fp) -> do - -- Check if the executable exists. - fpExists <- liftIO $ doesFileExist fp - if not fpExists - then do warnings' [ExeNotFound ef fp] - return Nothing - else do - - -- Check if the executable is executable. - fpPerms <- liftIO $ getPermissions fp - if not (executable fpPerms) - then do warnings' [ExeNotExecutable ef fp] - return Nothing - else do - - -- Compute canonical executable name and absolute filepath. - let strExeName = takeFileName fp - let strExeName' = fromMaybe strExeName $ stripExtension exeExtension strExeName - let txtExeName = T.pack strExeName' - exePath <- liftIO $ makeAbsolute fp - return $ Just (txtExeName, exePath) + -- Compute canonical executable name and absolute filepath. + let strExeName = takeFileName fp + let strExeName' = fromMaybe strExeName $ stripExtension exeExtension strExeName + let txtExeName = T.pack strExeName' + exePath <- liftIO $ makeAbsolute fp + return $ Just (txtExeName, exePath) ------------------------------------------------------------------------ -- * Resolving library names to include pathes diff --git a/src/full/Agda/Interaction/Library/Base.hs b/src/full/Agda/Interaction/Library/Base.hs --- a/src/full/Agda/Interaction/Library/Base.hs +++ b/src/full/Agda/Interaction/Library/Base.hs @@ -7,6 +7,7 @@ import Control.Monad.Except import Control.Monad.State import Control.Monad.Writer +import Control.Monad.IO.Class ( MonadIO(..) ) import Data.Char ( isDigit ) import Data.Data ( Data ) @@ -124,18 +125,12 @@ -- | Library Warnings. data LibWarning' = UnknownField String - | ExeNotFound ExecutablesFile FilePath - -- ^ Raised when a trusted executable can not be found. - | ExeNotExecutable ExecutablesFile FilePath - -- ^ Raised when a trusted executable does not have the executable permission. deriving (Show, Data, Generic) data LibError = LibError (Maybe LibPositionInfo) LibError' libraryWarningName :: LibWarning -> WarningName libraryWarningName (LibWarning c (UnknownField{})) = LibUnknownField_ -libraryWarningName (LibWarning c (ExeNotFound{})) = ExeNotFoundWarning_ -libraryWarningName (LibWarning c (ExeNotExecutable{})) = ExeNotExecutableWarning_ -- | Collected errors while processing library files. -- @@ -261,8 +256,6 @@ instance Pretty LibWarning' where pretty (UnknownField s) = text $ "Unknown field '" ++ s ++ "'" - pretty (ExeNotFound file exe) = text $ "Executable '" ++ exe ++ "' not found." - pretty (ExeNotExecutable file exe) = text $ "Executable '" ++ exe ++ "' not executable." ------------------------------------------------------------------------ -- NFData instances diff --git a/src/full/Agda/Interaction/Library/Parse.hs b/src/full/Agda/Interaction/Library/Parse.hs --- a/src/full/Agda/Interaction/Library/Parse.hs +++ b/src/full/Agda/Interaction/Library/Parse.hs @@ -41,6 +41,7 @@ import Agda.Utils.Applicative import Agda.Utils.IO ( catchIO ) +import qualified Agda.Utils.IO.UTF8 as UTF8 import Agda.Utils.Lens import Agda.Utils.List ( duplicates ) import Agda.Utils.String ( ltrim ) @@ -109,7 +110,7 @@ -- parseLibFile :: FilePath -> IO (P AgdaLibFile) parseLibFile file = - (fmap setPath . parseLib <$> readFile file) `catchIO` \e -> + (fmap setPath . parseLib <$> UTF8.readFile file) `catchIO` \e -> return $ throwError $ unlines [ "Failed to read library file " ++ file ++ "." , "Reason: " ++ show e diff --git a/src/full/Agda/Interaction/MakeCase.hs b/src/full/Agda/Interaction/MakeCase.hs --- a/src/full/Agda/Interaction/MakeCase.hs +++ b/src/full/Agda/Interaction/MakeCase.hs @@ -324,7 +324,7 @@ -- we need to print them postfix. let postProjInExtLam = applyWhen (isJust casectxt) $ withPragmaOptions $ \ opt -> opt { optPostfixProjections = True } - (piTel, sc) <- insertTrailingArgs $ clauseToSplitClause clause + (piTel, sc) <- insertTrailingArgs False $ clauseToSplitClause clause -- Andreas, 2015-05-05 If we introduced new function arguments -- do not split on result. This might be more what the user wants. -- To split on result, he can then C-c C-c again. diff --git a/src/full/Agda/Interaction/Options/Base.hs b/src/full/Agda/Interaction/Options/Base.hs --- a/src/full/Agda/Interaction/Options/Base.hs +++ b/src/full/Agda/Interaction/Options/Base.hs @@ -91,6 +91,7 @@ , optInputFile :: Maybe FilePath , optIncludePaths :: [FilePath] , optAbsoluteIncludePaths :: [AbsolutePath] + -- ^ The list should not contain duplicates. , optLibraries :: [LibName] , optOverrideLibrariesFile :: Maybe FilePath -- ^ Use this (if Just) instead of .agda/libraries @@ -709,7 +710,6 @@ cubicalFlag :: Cubical -- ^ Which variant of Cubical Agda? -> Flag PragmaOptions -cubicalFlag CErased _ = throwError "--erased-cubical is not available." cubicalFlag variant o = do let withoutK = optWithoutK o return $ o { optCubical = Just variant diff --git a/src/full/Agda/Interaction/Options/Lenses.hs b/src/full/Agda/Interaction/Options/Lenses.hs --- a/src/full/Agda/Interaction/Options/Lenses.hs +++ b/src/full/Agda/Interaction/Options/Lenses.hs @@ -6,7 +6,7 @@ module Agda.Interaction.Options.Lenses where -import Control.Monad.State +import Control.Monad.IO.Class ( MonadIO(..) ) import Data.Set (Set) import qualified Data.Set as Set diff --git a/src/full/Agda/Interaction/Options/Warnings.hs b/src/full/Agda/Interaction/Options/Warnings.hs --- a/src/full/Agda/Interaction/Options/Warnings.hs +++ b/src/full/Agda/Interaction/Options/Warnings.hs @@ -150,8 +150,6 @@ , RewriteMaybeNonConfluent_ , RewriteAmbiguousRules_ , RewriteMissingRule_ - , ExeNotFoundWarning_ - , ExeNotExecutableWarning_ ] allWarnings :: Set WarningName @@ -268,9 +266,6 @@ -- Record field warnings | DuplicateFieldsWarning_ | TooManyFieldsWarning_ - -- System call warnings - | ExeNotFoundWarning_ - | ExeNotExecutableWarning_ deriving (Eq, Ord, Show, Read, Enum, Bounded, Generic) instance NFData WarningName @@ -425,6 +420,3 @@ -- Record field warnings DuplicateFieldsWarning_ -> "Record expression with duplicate field names." TooManyFieldsWarning_ -> "Record expression with invalid field names." - -- System call warnings - ExeNotFoundWarning_ -> "Trusted executable cannot be found." - ExeNotExecutableWarning_ -> "Trusted executable does not have permission to execute." diff --git a/src/full/Agda/Main.hs b/src/full/Agda/Main.hs --- a/src/full/Agda/Main.hs +++ b/src/full/Agda/Main.hs @@ -5,7 +5,9 @@ import Prelude hiding (null) -import Control.Monad.Except +import Control.Monad ( void ) +import Control.Monad.Except ( MonadError(..), ExceptT(..), runExceptT ) +import Control.Monad.IO.Class ( MonadIO(..) ) import qualified Data.List as List import Data.Maybe diff --git a/src/full/Agda/Syntax/Abstract/Pattern.hs b/src/full/Agda/Syntax/Abstract/Pattern.hs --- a/src/full/Agda/Syntax/Abstract/Pattern.hs +++ b/src/full/Agda/Syntax/Abstract/Pattern.hs @@ -7,9 +7,10 @@ import Prelude hiding (null) -import Control.Arrow ((***), second) -import Control.Monad.Identity -import Control.Applicative (liftA2) +import Control.Arrow ( (***), second ) +import Control.Monad ( (>=>) ) +import Control.Monad.Identity ( Identity(..), runIdentity ) +import Control.Applicative ( liftA2 ) import Data.Maybe diff --git a/src/full/Agda/Syntax/Abstract/PatternSynonyms.hs b/src/full/Agda/Syntax/Abstract/PatternSynonyms.hs --- a/src/full/Agda/Syntax/Abstract/PatternSynonyms.hs +++ b/src/full/Agda/Syntax/Abstract/PatternSynonyms.hs @@ -8,8 +8,9 @@ , mergePatternSynDefs ) where -import Control.Applicative ( Alternative(empty) ) -import Control.Monad.Writer hiding (forM) +import Control.Applicative ( Alternative(empty) ) +import Control.Monad ( foldM, guard, zipWithM, zipWithM_ ) +import Control.Monad.Writer ( MonadWriter(..), WriterT, execWriterT ) import Data.Map (Map) import qualified Data.Map as Map diff --git a/src/full/Agda/Syntax/Concrete/Definitions.hs b/src/full/Agda/Syntax/Concrete/Definitions.hs --- a/src/full/Agda/Syntax/Concrete/Definitions.hs +++ b/src/full/Agda/Syntax/Concrete/Definitions.hs @@ -54,8 +54,10 @@ import Prelude hiding (null) -import Control.Monad.Except -import Control.Monad.State +import Control.Monad ( forM, guard, unless, void, when ) +import Control.Monad.Except ( ) +import Control.Monad.State ( MonadState(..), gets, StateT, runStateT ) +import Control.Monad.Trans ( lift ) import Data.Bifunctor import Data.Data (Data) diff --git a/src/full/Agda/Syntax/Concrete/Definitions/Monad.hs b/src/full/Agda/Syntax/Concrete/Definitions/Monad.hs --- a/src/full/Agda/Syntax/Concrete/Definitions/Monad.hs +++ b/src/full/Agda/Syntax/Concrete/Definitions/Monad.hs @@ -1,7 +1,8 @@ module Agda.Syntax.Concrete.Definitions.Monad where -import Control.Monad.Except -import Control.Monad.State +import Control.Monad ( unless ) +import Control.Monad.Except ( MonadError(..), ExceptT, runExceptT ) +import Control.Monad.State ( MonadState(..), modify, State, runState ) import Data.Bifunctor (second) import Data.Map (Map) diff --git a/src/full/Agda/Syntax/Concrete/Pattern.hs b/src/full/Agda/Syntax/Concrete/Pattern.hs --- a/src/full/Agda/Syntax/Concrete/Pattern.hs +++ b/src/full/Agda/Syntax/Concrete/Pattern.hs @@ -5,8 +5,10 @@ import Control.Applicative ( liftA2 ) import Control.Arrow ( first ) +import Control.Monad ( (>=>) ) import Control.Monad.Identity -import Control.Monad.Writer + +import Data.Monoid ( Any(..), Endo(..), Sum(..) ) import Agda.Syntax.Common import Agda.Syntax.Concrete diff --git a/src/full/Agda/Syntax/Internal.hs b/src/full/Agda/Syntax/Internal.hs --- a/src/full/Agda/Syntax/Internal.hs +++ b/src/full/Agda/Syntax/Internal.hs @@ -221,7 +221,10 @@ -- The @String@ typically describes the location where we create this dummy, -- but can contain other information as well. -- The second field accumulates eliminations in case we - -- apply a dummy term to more of them. + -- apply a dummy term to more of them. Dummy terms should never be used in places + -- where they can affect type checking, so syntactic checks are free to ignore the + -- eliminators, which are only there to ease debugging when a dummy term incorrectly + -- leaks into a relevant position. deriving (Data, Show) type ConInfo = ConOrigin diff --git a/src/full/Agda/Syntax/Internal/Pattern.hs b/src/full/Agda/Syntax/Internal/Pattern.hs --- a/src/full/Agda/Syntax/Internal/Pattern.hs +++ b/src/full/Agda/Syntax/Internal/Pattern.hs @@ -1,8 +1,9 @@ module Agda.Syntax.Internal.Pattern where -import Control.Arrow (second) -import Control.Monad.State +import Control.Arrow ( second ) +import Control.Monad ( (>=>), forM ) +import Control.Monad.State ( MonadState(..), State, evalState ) import Data.Maybe import Data.Monoid diff --git a/src/full/Agda/Syntax/Parser.hs b/src/full/Agda/Syntax/Parser.hs --- a/src/full/Agda/Syntax/Parser.hs +++ b/src/full/Agda/Syntax/Parser.hs @@ -24,8 +24,10 @@ ) where import Control.Exception +import Control.Monad ( forM_ ) import Control.Monad.Except import Control.Monad.State +import Control.Monad.IO.Class ( MonadIO(..) ) import Data.Bifunctor import qualified Data.List as List diff --git a/src/full/Agda/Syntax/Parser/Lexer.x b/src/full/Agda/Syntax/Parser/Lexer.x --- a/src/full/Agda/Syntax/Parser/Lexer.x +++ b/src/full/Agda/Syntax/Parser/Lexer.x @@ -37,9 +37,8 @@ } --- Unicode is not handled by the following regular expressions. --- Instead, unicode characters are translated to 7-bit ASCII --- by Agda.Syntax.Parser.LexActions.foolAlex in a preprocessing pass. +-- Note that the regular expressions should not use non-ASCII +-- characters, see Agda.Syntax.Parser.Alex.alexGetByte. $digit = 0-9 $hexdigit = [ $digit a-f A-F ] diff --git a/src/full/Agda/Syntax/Scope/Monad.hs b/src/full/Agda/Syntax/Scope/Monad.hs --- a/src/full/Agda/Syntax/Scope/Monad.hs +++ b/src/full/Agda/Syntax/Scope/Monad.hs @@ -10,7 +10,6 @@ import Control.Arrow ((***)) import Control.Monad import Control.Monad.Except -import Control.Monad.Writer hiding ((<>)) import Control.Monad.State import Data.Either ( partitionEithers ) @@ -253,6 +252,18 @@ printLocals 10 "bound variables:" modifyScope_ $ setVarsToBind [] +annotateDecls :: ReadTCState m => m [A.Declaration] -> m A.Declaration +annotateDecls m = do + ds <- m + s <- getScope + return $ A.ScopedDecl s ds + +annotateExpr :: ReadTCState m => m A.Expr -> m A.Expr +annotateExpr m = do + e <- m + s <- getScope + return $ A.ScopedExpr s e + --------------------------------------------------------------------------- -- * Names --------------------------------------------------------------------------- @@ -387,8 +398,8 @@ fromConcreteSuffix = \case Nothing -> Nothing Just C.Prime{} -> Nothing - Just (C.Index i) -> Just $ A.Suffix $ toInteger i - Just (C.Subscript i) -> Just $ A.Suffix $ toInteger i + Just (C.Index i) -> Just $ A.Suffix i + Just (C.Subscript i) -> Just $ A.Suffix i -- | Test if a given abstract name can appear with a suffix. Currently -- only true for the names of builtin sorts @Set@ and @Prop@. diff --git a/src/full/Agda/Syntax/Translation/AbstractToConcrete.hs b/src/full/Agda/Syntax/Translation/AbstractToConcrete.hs --- a/src/full/Agda/Syntax/Translation/AbstractToConcrete.hs +++ b/src/full/Agda/Syntax/Translation/AbstractToConcrete.hs @@ -26,10 +26,11 @@ import Prelude hiding (null) -import Control.Arrow ((&&&), first) -import Control.Monad.Except -import Control.Monad.Reader -import Control.Monad.State +import Control.Arrow ( (&&&), first ) +import Control.Monad ( (<=<), forM, forM_, guard, liftM2 ) +import Control.Monad.Except ( runExceptT ) +import Control.Monad.Reader ( MonadReader(..), asks, runReaderT ) +import Control.Monad.State ( StateT(..), runStateT ) import qualified Control.Monad.Fail as Fail diff --git a/src/full/Agda/Syntax/Translation/ConcreteToAbstract.hs b/src/full/Agda/Syntax/Translation/ConcreteToAbstract.hs --- a/src/full/Agda/Syntax/Translation/ConcreteToAbstract.hs +++ b/src/full/Agda/Syntax/Translation/ConcreteToAbstract.hs @@ -19,9 +19,9 @@ import Prelude hiding ( null ) -import Control.Applicative hiding ( empty ) -import Control.Monad.Except -import Control.Monad.Reader +import Control.Monad ( (<=<), foldM, forM, forM_, zipWithM, zipWithM_ ) +import Control.Applicative ( liftA2, liftA3 ) +import Control.Monad.Except ( MonadError(..) ) import Data.Bifunctor import Data.Foldable (traverse_) @@ -126,18 +126,6 @@ --annotateDecl :: ScopeM A.Declaration -> ScopeM A.Declaration --annotateDecl m = annotateDecls $ (:[]) <$> m -annotateDecls :: ScopeM [A.Declaration] -> ScopeM A.Declaration -annotateDecls m = do - ds <- m - s <- getScope - return $ ScopedDecl s ds - -annotateExpr :: ScopeM A.Expr -> ScopeM A.Expr -annotateExpr m = do - e <- m - s <- getScope - return $ ScopedExpr s e - -- | Make sure that there are no dot patterns (called on pattern synonyms). noDotorEqPattern :: String -> A.Pattern' e -> ScopeM (A.Pattern' Void) noDotorEqPattern err = dot @@ -2102,13 +2090,19 @@ unGeneralized (A.ScopedExpr si e) = A.ScopedExpr si <$> unGeneralized e unGeneralized t = (mempty, t) +alreadyGeneralizing :: ScopeM Bool +alreadyGeneralizing = isJust <$> useTC stGeneralizedVars + collectGeneralizables :: ScopeM a -> ScopeM (Set I.QName, a) -collectGeneralizables m = bracket_ open close $ do - a <- m - s <- useTC stGeneralizedVars - case s of - Nothing -> __IMPOSSIBLE__ - Just s -> return (s, a) +collectGeneralizables m = + -- #5683: No nested generalization + ifM alreadyGeneralizing ((Set.empty,) <$> m) $ + {-else-} bracket_ open close $ do + a <- m + s <- useTC stGeneralizedVars + case s of + Nothing -> __IMPOSSIBLE__ + Just s -> return (s, a) where open = do gvs <- useTC stGeneralizedVars diff --git a/src/full/Agda/Syntax/Translation/InternalToAbstract.hs b/src/full/Agda/Syntax/Translation/InternalToAbstract.hs --- a/src/full/Agda/Syntax/Translation/InternalToAbstract.hs +++ b/src/full/Agda/Syntax/Translation/InternalToAbstract.hs @@ -23,9 +23,9 @@ import Prelude hiding (null) -import Control.Applicative (liftA2) -import Control.Arrow ((&&&)) -import Control.Monad.State +import Control.Applicative ( liftA2 ) +import Control.Arrow ( (&&&) ) +import Control.Monad ( filterM, forM ) import qualified Data.List as List import qualified Data.Map as Map diff --git a/src/full/Agda/Syntax/Translation/ReflectedToAbstract.hs b/src/full/Agda/Syntax/Translation/ReflectedToAbstract.hs --- a/src/full/Agda/Syntax/Translation/ReflectedToAbstract.hs +++ b/src/full/Agda/Syntax/Translation/ReflectedToAbstract.hs @@ -2,9 +2,10 @@ module Agda.Syntax.Translation.ReflectedToAbstract where -import Control.Arrow ( (***) ) -import Control.Monad.Except -import Control.Monad.Reader +import Control.Arrow ( (***) ) +import Control.Monad ( foldM ) +import Control.Monad.Except ( MonadError ) +import Control.Monad.Reader ( MonadReader(..), asks, reader, runReaderT ) import Data.Maybe import Data.Set (Set) @@ -118,7 +119,7 @@ , HasConstInfo m ) => r -> m (AbsOfRef r) toAbstractWithoutImplicit x = do - xs <- getContextNames + xs <- killRange <$> getContextNames let ctx = zip xs $ repeat R.Unknown runReaderT (toAbstract x) ctx @@ -190,10 +191,17 @@ return $ A.Pi exprNoRange (singleton a) b R.Sort s -> toAbstract s R.Lit l -> toAbstract l - R.Meta x es -> toAbstract (A.Underscore info, es) - where info = emptyMetaInfo{ metaNumber = Just x } - R.Unknown -> return $ Underscore emptyMetaInfo + R.Meta x es -> do + info <- mkMetaInfo + let info' = info{ metaNumber = Just x } + toAbstract (A.Underscore info', es) + R.Unknown -> Underscore <$> mkMetaInfo +mkMetaInfo :: ReadTCState m => m MetaInfo +mkMetaInfo = do + scope <- getScope + return $ emptyMetaInfo { metaScope = scope } + mkDef :: HasConstInfo m => QName -> m A.Expr mkDef f = ifM (isMacro . theDef <$> getConstInfo f) @@ -231,7 +239,7 @@ PropS x -> mkApp (A.Def propName) <$> toAbstract x PropLitS x -> return $ A.Def' propName $ A.Suffix x InfS x -> return $ A.Def' infName $ A.Suffix x - UnknownS -> return $ mkApp (A.Def setName) $ Underscore emptyMetaInfo + UnknownS -> mkApp (A.Def setName) . Underscore <$> mkMetaInfo instance ToAbstract R.Pattern where type AbsOfRef R.Pattern = A.Pattern diff --git a/src/full/Agda/Termination/Monad.hs b/src/full/Agda/Termination/Monad.hs --- a/src/full/Agda/Termination/Monad.hs +++ b/src/full/Agda/Termination/Monad.hs @@ -13,6 +13,8 @@ import qualified Control.Monad.Fail as Fail +import Control.Monad ( forM ) +import Control.Monad.IO.Class ( MonadIO(..) ) import Control.Monad.Except import Control.Monad.Reader diff --git a/src/full/Agda/Termination/RecCheck.hs b/src/full/Agda/Termination/RecCheck.hs --- a/src/full/Agda/Termination/RecCheck.hs +++ b/src/full/Agda/Termination/RecCheck.hs @@ -57,7 +57,7 @@ let nonRec = mapMaybe (\case{ AcyclicSCC x -> Just x ; _ -> Nothing}) sccs let recs = mapMaybe (\case{ CyclicSCC xs -> Just xs; _ -> Nothing}) sccs - reportSLn "rec.graph" 20 $ show graph + reportSLn "rec.graph" 60 $ show graph -- Mark all non-recursive functions and their clauses as such. mapM_ markNonRecursive nonRec diff --git a/src/full/Agda/Termination/TermCheck.hs b/src/full/Agda/Termination/TermCheck.hs --- a/src/full/Agda/Termination/TermCheck.hs +++ b/src/full/Agda/Termination/TermCheck.hs @@ -18,8 +18,8 @@ import Prelude hiding ( null ) -import Control.Applicative (liftA2) -import Control.Monad.Reader +import Control.Applicative ( liftA2 ) +import Control.Monad ( (<=<), filterM, forM, forM_, zipWithM ) import Data.Foldable (toList) import qualified Data.List as List @@ -549,7 +549,7 @@ termToDBP :: Term -> TerM DeBruijnPattern termToDBP t = ifNotM terGetUseDotPatterns (return unusedVar) $ {- else -} do - termToPattern =<< do liftTCM $ stripAllProjections t + termToPattern =<< do liftTCM $ stripAllProjections =<< normalise t -- | Convert a term (from a dot pattern) to a pattern for the purposes of the termination checker. -- @@ -570,7 +570,7 @@ -- termToPattern t = unnamed <$> termToPattern t instance TermToPattern Term DeBruijnPattern where - termToPattern t = liftTCM (reduce t >>= constructorForm) >>= \case + termToPattern t = liftTCM (constructorForm t) >>= \case -- Constructors. Con c _ args -> ConP c noConPatternInfo . map (fmap unnamed) <$> termToPattern (fromMaybe __IMPOSSIBLE__ $ allApplyElims args) Def s [Apply arg] -> do @@ -604,7 +604,7 @@ , nest 2 $ "ps =" <+> do addContext tel $ prettyTCMPatternList ps ] forM' body $ \ v -> addContext tel $ do - -- TODO: combine the following two traversals. + -- TODO: combine the following two traversals, avoid full normalisation. -- Parse dot patterns as patterns as far as possible. ps <- postTraversePatternM parseDotP ps -- Blank out coconstructors. diff --git a/src/full/Agda/TypeChecking/CheckInternal.hs b/src/full/Agda/TypeChecking/CheckInternal.hs --- a/src/full/Agda/TypeChecking/CheckInternal.hs +++ b/src/full/Agda/TypeChecking/CheckInternal.hs @@ -56,7 +56,7 @@ -- | Entry point for e.g. checking WithFunctionType. checkType :: (MonadCheckInternal m) => Type -> m () -checkType t = do +checkType t = catchConstraint (CheckType t) $ do inferred <- checkType' t equalSort (getSort t) inferred @@ -343,8 +343,8 @@ -- | Infer possibly projection-like function application inferDef' :: (MonadCheckInternal m) => QName -> Arg Term -> Elims -> m Type inferDef' f a es = do - isProj <- isProjection f - case isProj of + -- Andreas, 2022-03-07, issue #5809: don't drop parameters of irrelevant projections. + isRelevantProjection f >>= \case Just Projection{ projIndex = n } | n > 0 -> do let self = unArg a b <- infer self diff --git a/src/full/Agda/TypeChecking/Constraints.hs b/src/full/Agda/TypeChecking/Constraints.hs --- a/src/full/Agda/TypeChecking/Constraints.hs +++ b/src/full/Agda/TypeChecking/Constraints.hs @@ -32,6 +32,7 @@ import {-# SOURCE #-} Agda.TypeChecking.MetaVars import {-# SOURCE #-} Agda.TypeChecking.Empty import {-# SOURCE #-} Agda.TypeChecking.Lock +import {-# SOURCE #-} Agda.TypeChecking.CheckInternal ( checkType ) import Agda.Utils.CallStack ( withCurrentCallStack ) import Agda.Utils.Functor @@ -296,6 +297,7 @@ solveConstraint_ (HasBiggerSort a) = hasBiggerSort a solveConstraint_ (HasPTSRule a b) = hasPTSRule a b solveConstraint_ (CheckMetaInst m) = checkMetaInst m +solveConstraint_ (CheckType t) = checkType t solveConstraint_ (UsableAtModality mod t) = usableAtModality mod t checkTypeCheckingProblem :: TypeCheckingProblem -> TCM Term diff --git a/src/full/Agda/TypeChecking/Conversion.hs b/src/full/Agda/TypeChecking/Conversion.hs --- a/src/full/Agda/TypeChecking/Conversion.hs +++ b/src/full/Agda/TypeChecking/Conversion.hs @@ -193,8 +193,10 @@ (Def f es, Def f' es') | f == f' -> ifNotM (optFirstOrder <$> pragmaOptions) fallback $ {- else -} unlessSubtyping $ do def <- getConstInfo f - -- We do not shortcut projection-likes - if isJust $ isProjection_ (theDef def) then fallback else do + -- We do not shortcut projection-likes, + -- Andreas, 2022-03-07, issue #5809: + -- but irrelevant projections since they are applied to their parameters. + if isJust $ isRelevantProjection_ def then fallback else do pol <- getPolarity' cmp f compareElims pol [] (defType def) (Def f []) es es' `orelse` fallback _ -> fallback @@ -393,8 +395,8 @@ def <- getConstInfo f -- To compute the type @a@ of a projection-like @f@, -- we have to infer the type of its first argument. - if projectionArgs (theDef def) <= 0 then return $ defType def else do - -- Find an first argument to @f@. + if projectionArgs def <= 0 then return $ defType def else do + -- Find a first argument to @f@. let arg = case (es, es') of (Apply arg : _, _) -> arg (_, Apply arg : _) -> arg diff --git a/src/full/Agda/TypeChecking/Coverage.hs b/src/full/Agda/TypeChecking/Coverage.hs --- a/src/full/Agda/TypeChecking/Coverage.hs +++ b/src/full/Agda/TypeChecking/Coverage.hs @@ -297,7 +297,7 @@ ] ] -- Jesper, 2019-10: introduce trailing arguments (see #3828) - (_ , sc') <- insertTrailingArgs sc + (_ , sc') <- insertTrailingArgs True sc CoverResult { coverMissingClauses = missing } <- cover f cs sc' return $ null missing -- Andreas, 2019-08-08 and 2020-02-11 @@ -517,16 +517,24 @@ -- blocked on arguments that are not yet introduced: -- we must split on a variable so that the target type becomes a pi type - trySplitRes (BlockedOnApply IsApply) finalSplit splitError cont - | finalSplit = __IMPOSSIBLE__ -- already ruled out by lhs checker - | otherwise = cont + trySplitRes (BlockedOnApply IsApply) finalSplit splitError cont = do + -- Andreas, 2021-12-31, issue #5712. + -- If there is a tactic to solve the clause, we might not have inserted + -- trailing args (due to #5358). Now we force it! + (tel, sc') <- insertTrailingArgs True sc + if null tel then + if finalSplit then __IMPOSSIBLE__ -- already ruled out by lhs checker + else cont + else cover f cs sc' + -- ...or it was an IApply pattern, so we might just need to introduce the variable now. trySplitRes (BlockedOnApply IsIApply) finalSplit splitError cont = do - caseMaybeM (splitResultPath f sc) fallback $ (cover f cs . snd) <=< insertTrailingArgs + caseMaybeM (splitResultPath f sc) fallback $ (cover f cs . snd) <=< insertTrailingArgs False where fallback | finalSplit = __IMPOSSIBLE__ -- already ruled out by lhs checker? | otherwise = cont + -- blocked on result but there are catchalls: -- try regular splits if there are any, or else throw an error, -- this is nicer than continuing and reporting unreachable clauses @@ -546,7 +554,7 @@ Right (Covering n scs) -> do -- If result splitting was successful, continue coverage checking. (projs, results) <- unzip <$> do - mapM (traverseF $ cover f cs <=< (snd <.> insertTrailingArgs)) scs + mapM (traverseF $ cover f cs <=< (snd <.> insertTrailingArgs False)) scs -- OR: -- forM scs $ \ (proj, sc') -> (proj,) <$> do -- cover f cs =<< do @@ -970,11 +978,14 @@ -- | Add more patterns to split clause if the target type is a function type. -- Returns the domains of the function type (if any). -insertTrailingArgs :: SplitClause -> TCM (Telescope, SplitClause) -insertTrailingArgs sc@SClause{ scTel = sctel, scPats = ps, scSubst = sigma, scCheckpoints = cps, scTarget = target } = do +insertTrailingArgs + :: Bool -- ^ Force insertion even when there is a 'domTactic'? + -> SplitClause + -> TCM (Telescope, SplitClause) +insertTrailingArgs force sc@SClause{ scTel = sctel, scPats = ps, scSubst = sigma, scCheckpoints = cps, scTarget = target } = do let fallback = return (empty, sc) caseMaybe target fallback $ \ a -> do - if isJust (domTactic a) then fallback else do + if isJust (domTactic a) && not force then fallback else do (TelV tel b) <- telViewUpTo (-1) $ unDom a reportSDoc "tc.cover.target" 15 $ sep [ "target type telescope: " <+> do @@ -990,7 +1001,7 @@ sctel' = telFromList $ telToList (raise n sctel) ++ telToList tel -- Dot patterns in @ps@ need to be raised! (Issue 1298) ps' = applySubst (raiseS n) ps ++ xs - newTarget = Just $ a $> b + newTarget = Just $ (if not (null tel) then a{ domTactic = Nothing } else a) $> b sc' = SClause { scTel = sctel' , scPats = ps' @@ -1455,7 +1466,7 @@ ns <- case inserttrailing of DontInsertTrailing -> return ns DoInsertTrailing -> lift $ forM ns $ \(con,sc) -> - (con,) . snd <$> insertTrailingArgs sc + (con,) . snd <$> insertTrailingArgs False sc mHCompName <- getPrimitiveName' builtinHComp withoutK <- collapseDefault . optWithoutK <$> pragmaOptions diff --git a/src/full/Agda/TypeChecking/Datatypes.hs b/src/full/Agda/TypeChecking/Datatypes.hs --- a/src/full/Agda/TypeChecking/Datatypes.hs +++ b/src/full/Agda/TypeChecking/Datatypes.hs @@ -1,7 +1,8 @@ module Agda.TypeChecking.Datatypes where -import Control.Monad.Except +import Control.Monad ( filterM ) +import Control.Monad.Except ( MonadError(..), ExceptT(..), runExceptT ) import Data.Maybe (fromMaybe) diff --git a/src/full/Agda/TypeChecking/Empty.hs b/src/full/Agda/TypeChecking/Empty.hs --- a/src/full/Agda/TypeChecking/Empty.hs +++ b/src/full/Agda/TypeChecking/Empty.hs @@ -6,7 +6,8 @@ , checkEmptyTel ) where -import Control.Monad.Except +import Control.Monad ( void ) +import Control.Monad.Except ( MonadError(..) ) import Data.Semigroup import qualified Data.Set as Set diff --git a/src/full/Agda/TypeChecking/Free/Lazy.hs b/src/full/Agda/TypeChecking/Free/Lazy.hs --- a/src/full/Agda/TypeChecking/Free/Lazy.hs +++ b/src/full/Agda/TypeChecking/Free/Lazy.hs @@ -60,8 +60,8 @@ module Agda.TypeChecking.Free.Lazy where import Control.Applicative hiding (empty) -import Control.Monad.Reader - +import Control.Monad ( guard ) +import Control.Monad.Reader ( MonadReader(..), asks, ReaderT, Reader, runReader ) import Data.IntMap (IntMap) import qualified Data.IntMap as IntMap diff --git a/src/full/Agda/TypeChecking/Generalize.hs b/src/full/Agda/TypeChecking/Generalize.hs --- a/src/full/Agda/TypeChecking/Generalize.hs +++ b/src/full/Agda/TypeChecking/Generalize.hs @@ -10,7 +10,7 @@ import Control.Monad import Control.Monad.Except -import Data.IntSet (IntSet) +import qualified Data.IntMap as IntMap import qualified Data.IntSet as IntSet import Data.Set (Set) import qualified Data.Set as Set @@ -127,7 +127,8 @@ return (genTelNames, t', userdata) -- | Create metas for the generalizable variables and run the type check action. -createMetasAndTypeCheck :: Set QName -> TCM a -> TCM (a, Map MetaId QName, IntSet) +createMetasAndTypeCheck :: + Set QName -> TCM a -> TCM (a, Map MetaId QName, MetaStore) createMetasAndTypeCheck s typecheckAction = do ((namedMetas, x), allmetas) <- metasCreatedBy $ do (metamap, genvals) <- createGenValues s @@ -150,13 +151,15 @@ -- generalized. Called in the context extended with the telescope record variable (whose type is -- the first argument). Returns the telescope of generalized variables and a substitution from -- this telescope to the current context. -computeGeneralization :: Type -> Map MetaId name -> IntSet -> TCM (Telescope, [Maybe name], Substitution) +computeGeneralization :: + Type -> Map MetaId name -> MetaStore -> + TCM (Telescope, [Maybe name], Substitution) computeGeneralization genRecMeta nameMap allmetas = postponeInstanceConstraints $ do reportSDoc "tc.generalize" 10 $ "computing generalization for type" <+> prettyTCM genRecMeta -- Pair metas with their metaInfo - mvs <- mapM ((\ x -> (x,) <$> lookupMeta x) . MetaId) $ IntSet.toList allmetas + mvs <- mapM ((\ x -> (x,) <$> lookupMeta x) . MetaId) $ IntMap.keys allmetas -- Issue 4727: filter out metavariables that were created before the -- current checkpoint, since they are too old to be generalized. @@ -317,7 +320,7 @@ -- Now we need to prune the unsolved metas to make sure they respect the new -- dependencies (#3672). Also update interaction points to point to pruned metas. let inscope (ii, InteractionPoint{ipMeta = Just x}) - | IntSet.member (metaId x) allmetas = Just (x, ii) + | IntMap.member (metaId x) allmetas = Just (x, ii) inscope _ = Nothing ips <- Map.fromDistinctAscList . mapMaybe inscope . fst . BiMap.toDistinctAscendingLists <$> useTC stInteractionPoints pruneUnsolvedMetas genRecName genRecCon genTel genRecFields ips shouldGeneralize allSortedMetas diff --git a/src/full/Agda/TypeChecking/Implicit.hs b/src/full/Agda/TypeChecking/Implicit.hs --- a/src/full/Agda/TypeChecking/Implicit.hs +++ b/src/full/Agda/TypeChecking/Implicit.hs @@ -120,7 +120,8 @@ return $ makeInstance info (_, v) <- newMetaArg info' x CmpLeq a - whenJust tac $ \ tac -> liftTCM $ unquoteTactic tac v a + whenJust tac $ \ tac -> liftTCM $ + applyModalityToContext info $ unquoteTactic tac v a let narg = Arg info (Named (Just $ WithOrigin Inserted $ unranged x) v) mapFst (narg :) <$> implicitNamedArgs (n-1) expand (absApp b v) _ -> return ([], t0') diff --git a/src/full/Agda/TypeChecking/InstanceArguments.hs b/src/full/Agda/TypeChecking/InstanceArguments.hs --- a/src/full/Agda/TypeChecking/InstanceArguments.hs +++ b/src/full/Agda/TypeChecking/InstanceArguments.hs @@ -7,9 +7,11 @@ , postponeInstanceConstraints ) where -import Control.Monad.Except -import Control.Monad.Reader -import qualified Data.IntSet as IntSet +import Control.Monad ( forM ) +import Control.Monad.Except ( MonadError(..) ) +import Control.Monad.Trans ( lift ) + +import qualified Data.IntMap as IntMap import qualified Data.Map as Map import qualified Data.Set as Set import qualified Data.List as List @@ -84,7 +86,6 @@ vars = [ Candidate LocalCandidate x t (isOverlappable info) | (x, Dom{domInfo = info, unDom = (_, t)}) <- varsAndRaisedTypes , isInstance info - , usableModality info ] -- {{}}-fields of variables are also candidates @@ -356,9 +357,9 @@ -- This is sufficient to reduce the list to a singleton should all be equal. dropSameCandidates :: MetaId -> [(Candidate, Term, a)] -> TCM [(Candidate, Term, a)] dropSameCandidates m cands0 = verboseBracket "tc.instance" 30 "dropSameCandidates" $ do - metas <- getMetaVariableSet + metas <- getMetaStore -- Does `it` have any metas in the initial meta variable store? - let freshMetas = getAny . allMetas (Any . (`IntSet.notMember` metas) . metaId) + let freshMetas = getAny . allMetas (Any . (`IntMap.notMember` metas) . metaId) -- Take overlappable candidates into account let cands = @@ -582,7 +583,8 @@ Constructor {conPars = n} -> return $ Con c ci (map Apply $ drop n vs) _ -> __IMPOSSIBLE__ Def f [] -> do - mp <- isProjection f + -- Andreas, 2022-03-07, issue #5809: don't drop parameters of irrelevant projections. + mp <- isRelevantProjection f case mp of Just Projection{projIndex = n} -> do case drop n vs of diff --git a/src/full/Agda/TypeChecking/Irrelevance.hs b/src/full/Agda/TypeChecking/Irrelevance.hs --- a/src/full/Agda/TypeChecking/Irrelevance.hs +++ b/src/full/Agda/TypeChecking/Irrelevance.hs @@ -118,13 +118,12 @@ -- as argument. workOnTypes' :: (MonadTCEnv m) => Bool -> m a -> m a workOnTypes' experimental - = modifyContextInfo (mapRelevance f) + = (if experimental + then modifyContextInfo (mapRelevance irrToNonStrict) + else id) . applyQuantityToContext zeroQuantity . typeLevelReductions . localTC (\ e -> e { envWorkingOnTypes = True }) - where - f | experimental = irrToNonStrict - | otherwise = id -- | (Conditionally) wake up irrelevant variables and make them relevant. -- For instance, diff --git a/src/full/Agda/TypeChecking/Level/Solve.hs b/src/full/Agda/TypeChecking/Level/Solve.hs --- a/src/full/Agda/TypeChecking/Level/Solve.hs +++ b/src/full/Agda/TypeChecking/Level/Solve.hs @@ -5,8 +5,7 @@ import Control.Monad import Control.Monad.Except -import qualified Data.IntSet as IntSet -import Data.IntSet (IntSet) +import qualified Data.IntMap as IntMap import Data.Maybe import Agda.Interaction.Options @@ -32,8 +31,8 @@ defaultLevelsToZero newMetas return result -defaultLevelsToZero :: forall m. (PureTCM m, MonadMetaSolver m) => IntSet -> m () -defaultLevelsToZero xs = loop =<< openLevelMetas (map MetaId $ IntSet.elems xs) +defaultLevelsToZero :: forall m. (PureTCM m, MonadMetaSolver m) => MetaStore -> m () +defaultLevelsToZero xs = loop =<< openLevelMetas (map MetaId $ IntMap.keys xs) where loop :: [MetaId] -> m () loop xs = do diff --git a/src/full/Agda/TypeChecking/Lock.hs b/src/full/Agda/TypeChecking/Lock.hs --- a/src/full/Agda/TypeChecking/Lock.hs +++ b/src/full/Agda/TypeChecking/Lock.hs @@ -7,7 +7,7 @@ ) where -import Control.Monad.Reader +import Control.Monad ( filterM, forM, forM_ ) import qualified Data.IntMap as IMap import qualified Data.IntSet as ISet diff --git a/src/full/Agda/TypeChecking/MetaVars.hs b/src/full/Agda/TypeChecking/MetaVars.hs --- a/src/full/Agda/TypeChecking/MetaVars.hs +++ b/src/full/Agda/TypeChecking/MetaVars.hs @@ -5,8 +5,9 @@ import Prelude hiding (null) -import Control.Monad.Except -import Control.Monad.Reader +import Control.Monad ( foldM, forM, forM_, liftM2, void ) +import Control.Monad.Except ( MonadError(..), ExceptT, runExceptT ) +import Control.Monad.Trans ( lift ) import Data.Function import qualified Data.IntMap as IntMap diff --git a/src/full/Agda/TypeChecking/MetaVars/Mention.hs b/src/full/Agda/TypeChecking/MetaVars/Mention.hs --- a/src/full/Agda/TypeChecking/MetaVars/Mention.hs +++ b/src/full/Agda/TypeChecking/MetaVars/Mention.hs @@ -118,6 +118,7 @@ HasPTSRule a b -> mm (a, b) UnquoteTactic tac hole goal -> False CheckMetaInst m -> True -- TODO + CheckType t -> mm t CheckLockedVars a b c d -> mm ((a, b), (c, d)) UsableAtModality mod t -> mm t where diff --git a/src/full/Agda/TypeChecking/Monad/Base.hs b/src/full/Agda/TypeChecking/Monad/Base.hs --- a/src/full/Agda/TypeChecking/Monad/Base.hs +++ b/src/full/Agda/TypeChecking/Monad/Base.hs @@ -15,14 +15,16 @@ import qualified Control.Monad.Fail as Fail +import Control.Monad ( void ) import Control.Monad.Except -import Control.Monad.State -import Control.Monad.Reader -import Control.Monad.Writer hiding ((<>)) +import Control.Monad.IO.Class ( MonadIO(..) ) +import Control.Monad.State ( MonadState(..), modify, StateT(..), runStateT ) +import Control.Monad.Reader ( MonadReader(..), ReaderT(..), runReaderT ) +import Control.Monad.Writer ( WriterT ) import Control.Monad.Trans ( MonadTrans(..), lift ) import Control.Monad.Trans.Control ( MonadTransControl(..), liftThrough ) -import Control.Monad.Trans.Identity -import Control.Monad.Trans.Maybe +import Control.Monad.Trans.Identity ( IdentityT(..), runIdentityT ) +import Control.Monad.Trans.Maybe ( MaybeT(..) ) import Control.Parallel ( pseq ) @@ -1002,6 +1004,11 @@ iFullHash :: Interface -> Hash iFullHash i = combineHashes $ iSourceHash i : List.map snd (iImportedModules i) +-- | A lens for the 'iSignature' field of the 'Interface' type. + +intSignature :: Lens' Signature Interface +intSignature f i = f (iSignature i) <&> \s -> i { iSignature = s } + --------------------------------------------------------------------------- -- ** Closure --------------------------------------------------------------------------- @@ -1065,6 +1072,7 @@ | HasBiggerSort Sort | HasPTSRule (Dom Type) (Abs Sort) | CheckMetaInst MetaId + | CheckType Type | UnBlock MetaId -- ^ Meta created for a term blocked by a postponed type checking problem or unsolved -- constraints. The 'MetaInstantiation' for the meta (when unsolved) is either 'BlockedConst' @@ -1114,6 +1122,7 @@ CheckLockedVars a b c d -> freeVars' ((a,b),(c,d)) UnquoteTactic t h g -> freeVars' (t, (h, g)) CheckMetaInst m -> mempty + CheckType t -> freeVars' t UsableAtModality mod t -> freeVars' t instance TermLike Constraint where @@ -1133,6 +1142,7 @@ HasBiggerSort s -> foldTerm f s HasPTSRule a s -> foldTerm f (a, Sort <$> s) CheckMetaInst m -> mempty + CheckType t -> foldTerm f t UsableAtModality m t -> foldTerm f t traverseTermM f c = __IMPOSSIBLE__ -- Not yet implemented @@ -1280,7 +1290,10 @@ , mvInstantiation :: MetaInstantiation , mvListeners :: Set Listener -- ^ meta variables scheduled for eta-expansion but blocked by this one , mvFrozen :: Frozen -- ^ are we past the point where we can instantiate this meta variable? - , mvTwin :: Maybe MetaId -- ^ @Just m@ means this meta will be equated to @m@ when the latter is unblocked. See @blockedTermOnProblem@. + , mvTwin :: Maybe MetaId + -- ^ @Just m@ means that this meta-variable will be + -- equated to @m@ when the latter is unblocked. See + -- 'Agda.TypeChecking.MetaVars.blockTermOnProblem'. } deriving Generic @@ -2907,6 +2920,9 @@ , envConflComputingOverlap :: Bool -- ^ Are we currently computing the overlap between -- two rewrite rules for the purpose of confluence checking? + , envCurrentlyElaborating :: Bool + -- ^ Are we currently in the process of executing an + -- elaborate-and-give interactive command? } deriving (Generic) @@ -2966,6 +2982,7 @@ , envGeneralizedVars = Map.empty , envActiveBackendName = Nothing , envConflComputingOverlap = False + , envCurrentlyElaborating = False } class LensTCEnv a where @@ -3106,6 +3123,9 @@ ePrintDomainFreePi :: Lens' Bool TCEnv ePrintDomainFreePi f e = f (envPrintDomainFreePi e) <&> \ x -> e { envPrintDomainFreePi = x } +ePrintMetasBare :: Lens' Bool TCEnv +ePrintMetasBare f e = f (envPrintMetasBare e) <&> \ x -> e { envPrintMetasBare = x } + eInsideDotPattern :: Lens' Bool TCEnv eInsideDotPattern f e = f (envInsideDotPattern e) <&> \ x -> e { envInsideDotPattern = x } @@ -3142,6 +3162,9 @@ eConflComputingOverlap :: Lens' Bool TCEnv eConflComputingOverlap f e = f (envConflComputingOverlap e) <&> \ x -> e { envConflComputingOverlap = x } +eCurrentlyElaborating :: Lens' Bool TCEnv +eCurrentlyElaborating f e = f (envCurrentlyElaborating e) <&> \ x -> e { envCurrentlyElaborating = x } + --------------------------------------------------------------------------- -- ** Context --------------------------------------------------------------------------- @@ -4195,38 +4218,45 @@ -- [1] When compiled with -auto-all and run with -p: roughly 750% -- faster for one example. -returnTCMT :: MonadIO m => a -> TCMT m a -returnTCMT = \x -> TCM $ \_ _ -> return x +returnTCMT :: Applicative m => a -> TCMT m a +returnTCMT = \x -> TCM $ \_ _ -> pure x {-# INLINE returnTCMT #-} -bindTCMT :: MonadIO m => TCMT m a -> (a -> TCMT m b) -> TCMT m b +bindTCMT :: Monad m => TCMT m a -> (a -> TCMT m b) -> TCMT m b bindTCMT = \(TCM m) k -> TCM $ \r e -> m r e >>= \x -> unTCM (k x) r e {-# INLINE bindTCMT #-} -thenTCMT :: MonadIO m => TCMT m a -> TCMT m b -> TCMT m b -thenTCMT = \(TCM m1) (TCM m2) -> TCM $ \r e -> m1 r e >> m2 r e +thenTCMT :: Applicative m => TCMT m a -> TCMT m b -> TCMT m b +thenTCMT = \(TCM m1) (TCM m2) -> TCM $ \r e -> m1 r e *> m2 r e {-# INLINE thenTCMT #-} -instance MonadIO m => Functor (TCMT m) where +instance Functor m => Functor (TCMT m) where fmap = fmapTCMT -fmapTCMT :: MonadIO m => (a -> b) -> TCMT m a -> TCMT m b +fmapTCMT :: Functor m => (a -> b) -> TCMT m a -> TCMT m b fmapTCMT = \f (TCM m) -> TCM $ \r e -> fmap f (m r e) {-# INLINE fmapTCMT #-} -instance MonadIO m => Applicative (TCMT m) where +instance Applicative m => Applicative (TCMT m) where pure = returnTCMT (<*>) = apTCMT -apTCMT :: MonadIO m => TCMT m (a -> b) -> TCMT m a -> TCMT m b -apTCMT = \(TCM mf) (TCM m) -> TCM $ \r e -> ap (mf r e) (m r e) +apTCMT :: Applicative m => TCMT m (a -> b) -> TCMT m a -> TCMT m b +apTCMT = \(TCM mf) (TCM m) -> TCM $ \r e -> mf r e <*> m r e {-# INLINE apTCMT #-} instance MonadTrans TCMT where lift m = TCM $ \_ _ -> m -- We want a special monad implementation of fail. +#if __GLASGOW_HASKELL__ < 808 instance MonadIO m => Monad (TCMT m) where +#else +-- Andreas, 2022-02-02, issue #5659: +-- @transformers-0.6@ requires exactly a @Monad@ superclass constraint here +-- if we want @instance MonadTrans TCMT@. +instance Monad m => Monad (TCMT m) where +#endif return = pure (>>=) = bindTCMT (>>) = (*>) diff --git a/src/full/Agda/TypeChecking/Monad/Base.hs-boot b/src/full/Agda/TypeChecking/Monad/Base.hs-boot --- a/src/full/Agda/TypeChecking/Monad/Base.hs-boot +++ b/src/full/Agda/TypeChecking/Monad/Base.hs-boot @@ -1,3 +1,5 @@ +{-# LANGUAGE CPP #-} + module Agda.TypeChecking.Monad.Base where import Control.Monad.IO.Class (MonadIO) @@ -26,10 +28,18 @@ data TCState newtype TCMT m a = TCM { unTCM :: IORef TCState -> TCEnv -> m a } -instance MonadIO m => Applicative (TCMT m) -instance MonadIO m => Functor (TCMT m) -instance MonadIO m => Monad (TCMT m) +instance Applicative m => Applicative (TCMT m) +instance Functor m => Functor (TCMT m) instance MonadIO m => MonadIO (TCMT m) + +#if __GLASGOW_HASKELL__ < 808 +instance MonadIO m => Monad (TCMT m) where +#else +-- Andreas, 2022-02-02, issue #5659: +-- @transformers-0.6@ requires exactly a @Monad@ superclass constraint here +-- if we want @instance MonadTrans TCMT@. +instance Monad m => Monad (TCMT m) where +#endif type TCM = TCMT IO diff --git a/src/full/Agda/TypeChecking/Monad/Builtin.hs b/src/full/Agda/TypeChecking/Monad/Builtin.hs --- a/src/full/Agda/TypeChecking/Monad/Builtin.hs +++ b/src/full/Agda/TypeChecking/Monad/Builtin.hs @@ -6,7 +6,9 @@ import qualified Control.Monad.Fail as Fail +import Control.Monad ( liftM2, void ) import Control.Monad.Except +import Control.Monad.IO.Class ( MonadIO(..) ) import Control.Monad.Reader import Control.Monad.State import Control.Monad.Trans.Identity (IdentityT) diff --git a/src/full/Agda/TypeChecking/Monad/Builtin.hs-boot b/src/full/Agda/TypeChecking/Monad/Builtin.hs-boot --- a/src/full/Agda/TypeChecking/Monad/Builtin.hs-boot +++ b/src/full/Agda/TypeChecking/Monad/Builtin.hs-boot @@ -1,9 +1,11 @@ module Agda.TypeChecking.Monad.Builtin where -import Control.Monad.Reader -import Control.Monad.State +import Control.Monad.IO.Class ( MonadIO ) +import Control.Monad.Reader ( ReaderT ) +import Control.Monad.State ( StateT ) import Control.Monad.Trans.Identity ( IdentityT ) +import Control.Monad.Trans ( MonadTrans, lift ) import qualified Control.Monad.Fail as Fail diff --git a/src/full/Agda/TypeChecking/Monad/Constraints.hs b/src/full/Agda/TypeChecking/Monad/Constraints.hs --- a/src/full/Agda/TypeChecking/Monad/Constraints.hs +++ b/src/full/Agda/TypeChecking/Monad/Constraints.hs @@ -210,6 +210,7 @@ CheckFunDef{} -> True UnquoteTactic{} -> True CheckMetaInst{} -> True + CheckType{} -> True CheckLockedVars{} -> True UsableAtModality{} -> True diff --git a/src/full/Agda/TypeChecking/Monad/Context.hs b/src/full/Agda/TypeChecking/Monad/Context.hs --- a/src/full/Agda/TypeChecking/Monad/Context.hs +++ b/src/full/Agda/TypeChecking/Monad/Context.hs @@ -1,6 +1,7 @@ module Agda.TypeChecking.Monad.Context where +import Control.Monad ( (<=<), forM, when ) import Control.Monad.Except import Control.Monad.Reader import Control.Monad.State diff --git a/src/full/Agda/TypeChecking/Monad/Debug.hs b/src/full/Agda/TypeChecking/Monad/Debug.hs --- a/src/full/Agda/TypeChecking/Monad/Debug.hs +++ b/src/full/Agda/TypeChecking/Monad/Debug.hs @@ -6,6 +6,8 @@ import qualified Control.Exception as E import qualified Control.DeepSeq as DeepSeq (force) + +import Control.Monad.IO.Class ( MonadIO(..) ) import Control.Monad.Except import Control.Monad.Reader import Control.Monad.State diff --git a/src/full/Agda/TypeChecking/Monad/Imports.hs b/src/full/Agda/TypeChecking/Monad/Imports.hs --- a/src/full/Agda/TypeChecking/Monad/Imports.hs +++ b/src/full/Agda/TypeChecking/Monad/Imports.hs @@ -19,9 +19,8 @@ , withImportPath ) where -import Control.Arrow ( (***) ) -import Control.Monad.State - +import Control.Arrow ( (***) ) +import Control.Monad ( when ) import Data.Set (Set) import qualified Data.Map as Map diff --git a/src/full/Agda/TypeChecking/Monad/MetaVars.hs b/src/full/Agda/TypeChecking/Monad/MetaVars.hs --- a/src/full/Agda/TypeChecking/Monad/MetaVars.hs +++ b/src/full/Agda/TypeChecking/Monad/MetaVars.hs @@ -4,6 +4,9 @@ import Prelude hiding (null) +import Control.DeepSeq + +import Control.Monad ( (<=<), guard ) import Control.Monad.Except import Control.Monad.State import Control.Monad.Trans.Identity ( IdentityT ) @@ -127,12 +130,17 @@ modifyMetaStore f = stMetaStore `modifyTCLens` f -- | Run a computation and record which new metas it created. -metasCreatedBy :: ReadTCState m => m a -> m (a, IntSet) +metasCreatedBy :: ReadTCState m => m a -> m (a, MetaStore) metasCreatedBy m = do - before <- IntMap.keysSet <$> useTC stMetaStore - a <- m - after <- IntMap.keysSet <$> useTC stMetaStore - return (a, after IntSet.\\ before) + -- Compute largestMeta strictly to avoid leaking memory. + !largestMeta <- force . fmap fst . IntMap.lookupMax <$> + useTC stMetaStore + a <- m + ms <- useTC stMetaStore + let createdMetas = case largestMeta of + Nothing -> ms + Just largestMeta -> snd $ IntMap.split largestMeta ms + return (a, createdMetas) -- | Lookup a meta variable. lookupMeta' :: ReadTCState m => MetaId -> m (Maybe MetaVariable) @@ -272,6 +280,7 @@ HasBiggerSort{} -> return mempty HasPTSRule{} -> return mempty CheckMetaInst x -> return mempty + CheckType t -> return $ allMetas Set.singleton t CheckLockedVars a b c d -> return $ allMetas Set.singleton (a, b, c, d) UsableAtModality{} -> return mempty where @@ -518,33 +527,37 @@ getMetaRange :: (MonadFail m, ReadTCState m) => MetaId -> m Range getMetaRange = getRange <.> lookupMeta -getInteractionScope :: InteractionId -> TCM ScopeInfo +getInteractionScope + :: (MonadFail m, ReadTCState m, MonadError TCErr m, MonadTCEnv m) + => InteractionId -> m ScopeInfo getInteractionScope = getMetaScope <.> lookupMeta <=< lookupInteractionId -withMetaInfo' :: MetaVariable -> TCM a -> TCM a +withMetaInfo' :: (MonadTCEnv m, ReadTCState m, MonadTrace m) => MetaVariable -> m a -> m a withMetaInfo' mv = withMetaInfo (miClosRange $ mvInfo mv) -withMetaInfo :: Closure Range -> TCM a -> TCM a +withMetaInfo :: (MonadTCEnv m, ReadTCState m, MonadTrace m) => Closure Range -> m a -> m a withMetaInfo mI cont = enterClosure mI $ \ r -> setCurrentRange r cont -getMetaVariableSet :: ReadTCState m => m IntSet -getMetaVariableSet = IntMap.keysSet <$> getMetaStore +withInteractionId + :: (MonadFail m, ReadTCState m, MonadError TCErr m, MonadTCEnv m, MonadTrace m) + => InteractionId -> m a -> m a +withInteractionId i ret = do + m <- lookupInteractionId i + withMetaId m ret +withMetaId + :: (MonadFail m, MonadTCEnv m, ReadTCState m, MonadTrace m) + => MetaId -> m a -> m a +withMetaId m ret = do + mv <- lookupMeta m + withMetaInfo' mv ret + getMetaVariables :: ReadTCState m => (MetaVariable -> Bool) -> m [MetaId] getMetaVariables p = do store <- getMetaStore return [ MetaId i | (i, mv) <- IntMap.assocs store, p mv ] -getInstantiatedMetas :: ReadTCState m => m [MetaId] -getInstantiatedMetas = getMetaVariables (isInst . mvInstantiation) - where - isInst Open = False - isInst OpenInstance = False - isInst BlockedConst{} = False - isInst PostponedTypeCheckingProblem{} = False - isInst InstV{} = True - getOpenMetas :: ReadTCState m => m [MetaId] getOpenMetas = getMetaVariables (isOpenMeta . mvInstantiation) @@ -578,41 +591,31 @@ -- * Freezing and unfreezing metas. --------------------------------------------------------------------------- --- | Freeze all so far unfrozen metas for the duration of the given computation. -withFreezeMetas :: TCM a -> TCM a -withFreezeMetas cont = do - ms <- Set.fromList <$> freezeMetas - x <- cont - unfreezeMetas' (`Set.member` ms) - return x - --- | Freeze all meta variables and return the list of metas that got frozen. -freezeMetas :: TCM [MetaId] -freezeMetas = freezeMetas' $ const True - --- | Freeze some meta variables and return the list of metas that got frozen. -freezeMetas' :: (MetaId -> Bool) -> TCM [MetaId] -freezeMetas' p = execWriterT $ modifyTCLensM stMetaStore $ IntMap.traverseWithKey (freeze . MetaId) +-- | Freeze the given meta-variables and return those that were not +-- already frozen. +freezeMetas :: MetaStore -> TCM IntSet +freezeMetas ms = + execWriterT $ + modifyTCLensM stMetaStore $ + execStateT (mapM_ freeze $ IntMap.keys ms) where - freeze :: Monad m => MetaId -> MetaVariable -> WriterT [MetaId] m MetaVariable - freeze m mvar - | p m && mvFrozen mvar /= Frozen = do - tell [m] - return $ mvar { mvFrozen = Frozen } - | otherwise = return mvar + freeze :: Monad m => Int -> StateT MetaStore (WriterT IntSet m) () + freeze m = do + store <- get + case IntMap.lookup m store of + Just mvar + | mvFrozen mvar /= Frozen -> do + lift $ tell (IntSet.singleton m) + put $ IntMap.insert m (mvar { mvFrozen = Frozen }) store + | otherwise -> return () + Nothing -> __IMPOSSIBLE__ -- | Thaw all meta variables. unfreezeMetas :: TCM () -unfreezeMetas = unfreezeMetas' $ const True - --- | Thaw some metas, as indicated by the passed condition. -unfreezeMetas' :: (MetaId -> Bool) -> TCM () -unfreezeMetas' cond = modifyMetaStore $ IntMap.mapWithKey $ unfreeze . MetaId +unfreezeMetas = modifyMetaStore $ IntMap.map unfreeze where - unfreeze :: MetaId -> MetaVariable -> MetaVariable - unfreeze m mvar - | cond m = mvar { mvFrozen = Instantiable } - | otherwise = mvar + unfreeze :: MetaVariable -> MetaVariable + unfreeze mvar = mvar { mvFrozen = Instantiable } isFrozen :: (MonadFail m, ReadTCState m) => MetaId -> m Bool isFrozen x = do diff --git a/src/full/Agda/TypeChecking/Monad/Options.hs b/src/full/Agda/TypeChecking/Monad/Options.hs --- a/src/full/Agda/TypeChecking/Monad/Options.hs +++ b/src/full/Agda/TypeChecking/Monad/Options.hs @@ -1,30 +1,44 @@ module Agda.TypeChecking.Monad.Options where -import Control.Arrow ( (&&&) ) +import Control.Arrow ( (&&&) ) +import Control.Monad ( unless, when ) +import Control.Monad.IO.Class ( MonadIO(..) ) import Control.Monad.Except import Control.Monad.Reader import Control.Monad.State import Control.Monad.Writer +import qualified Data.Graph as Graph +import Data.List (sort) import Data.Maybe +import Data.Map (Map) +import qualified Data.Map as Map import System.Directory import System.FilePath import Agda.Syntax.Common +import Agda.Syntax.Concrete (TopLevelModuleName) +import qualified Agda.Syntax.Concrete as C +import qualified Agda.Syntax.Abstract as A import Agda.TypeChecking.Monad.Debug (reportSDoc) import Agda.TypeChecking.Warnings import Agda.TypeChecking.Monad.Base +import Agda.TypeChecking.Monad.Imports import Agda.TypeChecking.Monad.State import Agda.TypeChecking.Monad.Benchmark +import Agda.Interaction.FindFile import Agda.Interaction.Options import qualified Agda.Interaction.Options.Lenses as Lens import Agda.Interaction.Library import Agda.Utils.FileName import Agda.Utils.Functor +import qualified Agda.Utils.Graph.AdjacencyMap.Unidirectional as G +import Agda.Utils.List import Agda.Utils.Maybe import Agda.Utils.Pretty +import Agda.Utils.Tuple import Agda.Utils.WithDefault import Agda.Utils.Impossible @@ -180,8 +194,9 @@ -- | Makes the given directories absolute and stores them as include -- directories. -- --- If the include directories change, then the state is reset (completely, --- except for the include directories and 'stInteractionOutputCallback'). +-- If the include directories change, then the state is reset +-- (completely, except for the include directories and some other +-- things). -- -- An empty list is interpreted as @["."]@. @@ -204,7 +219,7 @@ -- We add the default dir at the end, since it is then -- printed last in error messages. -- Might also be useful to overwrite default imports... - incs <- return $ incs ++ [primdir] + incs <- return $ nubOn id $ incs ++ [primdir] reportSDoc "setIncludeDirs" 10 $ return $ vcat [ "Old include directories:" @@ -226,18 +241,97 @@ -- up in a situation in which we use the contents of the file -- "old-path/M.agda", when the user actually meant -- "new-path/M.agda". - when (oldIncs /= incs) $ do + when (sort oldIncs /= sort incs) $ do ho <- getInteractionOutputCallback tcWarnings <- useTC stTCWarnings -- restore already generated warnings projectConfs <- useTC stProjectConfigs -- restore cached project configs & .agda-lib agdaLibFiles <- useTC stAgdaLibFiles -- files, since they use absolute paths + decodedModules <- getDecodedModules + (keptDecodedModules, modFile) <- modulesToKeep incs decodedModules resetAllState setTCLens stTCWarnings tcWarnings setTCLens stProjectConfigs projectConfs setTCLens stAgdaLibFiles agdaLibFiles setInteractionOutputCallback ho + setDecodedModules keptDecodedModules + setTCLens stModuleToSource modFile Lens.putAbsoluteIncludePaths incs + where + -- A decoded module is kept if its top-level module name is resolved + -- to the same absolute path using the old and the new include + -- directories, and the same applies to all dependencies. + -- + -- File system accesses are cached using the ModuleToSource data + -- structure: For the old include directories this should mean that + -- the file system is not accessed, but the file system is accessed + -- for the new include directories, and certain changes to the file + -- system could lead to interfaces being discarded. A new + -- ModuleToSource structure, constructed using the new include + -- directories, is returned. + modulesToKeep + :: [AbsolutePath] -- New include directories. + -> DecodedModules -- Old decoded modules. + -> TCM (DecodedModules, ModuleToSource) + modulesToKeep incs old = process Map.empty Map.empty modules + where + -- A graph with one node per module in old, and an edge from m to + -- n if the module corresponding to m imports the module + -- corresponding to n. + dependencyGraph :: G.Graph A.ModuleName () + dependencyGraph = + G.fromNodes + [ iModuleName $ miInterface m + | m <- Map.elems old + ] + `G.union` + G.fromEdges + [ G.Edge + { source = iModuleName $ miInterface m + , target = d + , label = () + } + | m <- Map.elems old + , (d, _) <- iImportedModules $ miInterface m + ] + + -- All the modules from old, sorted so that all of a module's + -- dependencies precede it in the list. + modules :: [ModuleInfo] + modules = + map (\case + Graph.CyclicSCC{} -> + -- Agda does not allow cycles in the dependency graph. + __IMPOSSIBLE__ + Graph.AcyclicSCC m -> + case Map.lookup (A.toTopLevelModuleName m) old of + Just m -> m + Nothing -> __IMPOSSIBLE__) $ + G.sccs' dependencyGraph + + process :: + Map A.ModuleName ModuleInfo -> ModuleToSource -> [ModuleInfo] -> + TCM (DecodedModules, ModuleToSource) + process !keep !modFile [] = return + ( Map.fromList $ + map (mapFst A.toTopLevelModuleName) $ + Map.toList keep + , modFile + ) + process keep modFile (m : ms) = do + let deps = map fst $ iImportedModules $ miInterface m + depsKept = all (`Map.member` keep) deps + (keep, modFile) <- + if not depsKept then return (keep, modFile) else do + let n = iModuleName $ miInterface m + t = A.toTopLevelModuleName n + oldF <- findFile' t + (newF, modFile) <- liftIO $ findFile'' incs t modFile + return $ case (oldF, newF) of + (Right f1, Right f2) | f1 == f2 -> + (Map.insert n m keep, modFile) + _ -> (keep, modFile) + process keep modFile ms isPropEnabled :: HasOptions m => m Bool isPropEnabled = optProp <$> pragmaOptions diff --git a/src/full/Agda/TypeChecking/Monad/Options.hs-boot b/src/full/Agda/TypeChecking/Monad/Options.hs-boot new file mode 100644 --- /dev/null +++ b/src/full/Agda/TypeChecking/Monad/Options.hs-boot @@ -0,0 +1,9 @@ +module Agda.TypeChecking.Monad.Options where + +import Agda.Interaction.Library.Base +import Agda.Interaction.Options.HasOptions +import Agda.TypeChecking.Monad.Base +import Agda.Utils.FileName + +libToTCM :: LibM a -> TCM a +getIncludeDirs :: HasOptions m => m [AbsolutePath] diff --git a/src/full/Agda/TypeChecking/Monad/Signature.hs b/src/full/Agda/TypeChecking/Monad/Signature.hs --- a/src/full/Agda/TypeChecking/Monad/Signature.hs +++ b/src/full/Agda/TypeChecking/Monad/Signature.hs @@ -6,13 +6,14 @@ import qualified Control.Monad.Fail as Fail -import Control.Arrow (first, second) -import Control.Monad.Except -import Control.Monad.State -import Control.Monad.Reader -import Control.Monad.Writer hiding ((<>)) -import Control.Monad.Trans.Maybe -import Control.Monad.Trans.Identity +import Control.Arrow ( first, second ) +import Control.Monad.Except ( ExceptT ) +import Control.Monad.State ( StateT ) +import Control.Monad.Reader ( ReaderT ) +import Control.Monad.Writer ( WriterT ) +import Control.Monad.Trans.Maybe ( MaybeT ) +import Control.Monad.Trans.Identity ( IdentityT ) +import Control.Monad.Trans ( MonadTrans, lift ) import Data.Foldable (for_) import qualified Data.List as List @@ -265,8 +266,8 @@ addDisplayForms :: QName -> TCM () addDisplayForms x = do reportSDoc "tc.display.section" 20 $ "Computing display forms for" <+> pretty x - def <- theDef <$> getConstInfo x - let v = case def of + def <- getConstInfo x + let v = case theDef def of Constructor{conSrcCon = h} -> Con h{ conName = x } ConOSystem [] _ -> Def x [] @@ -441,7 +442,10 @@ -- Issue1238: the copied def should be an 'instance' if the original -- def is one. Skip constructors since the original constructor will -- still work as an instance. - unless isCon $ whenJust inst $ \ c -> addNamedInstance y c + -- Issue5583: Don't skip constructures, because the original constructor doesn't always + -- work. For instance if it's only available in an anonymous module generated by + -- `open import M args`. + whenJust inst $ \ c -> addNamedInstance y c -- Set display form for the old name if it's not a constructor. {- BREAKS fail/Issue478 -- Andreas, 2012-10-20 and if we are not an anonymous module @@ -1221,7 +1225,7 @@ Axiom{} -> 0 DataOrRecSig{} -> 0 GeneralizableVar{} -> 0 - def@Function{} -> projectionArgs def + def@Function{} -> projectionArgs d Datatype {dataPars = _} -> 0 -- not dropped Record {recPars = _} -> 0 -- not dropped Constructor{conPars = n} -> n @@ -1240,6 +1244,15 @@ Function { funProjection = result } -> result _ -> Nothing +-- | Is it the name of a non-irrelevant record projection? +{-# SPECIALIZE isProjection :: QName -> TCM (Maybe Projection) #-} +isRelevantProjection :: HasConstInfo m => QName -> m (Maybe Projection) +isRelevantProjection qn = isRelevantProjection_ <$> getConstInfo qn + +isRelevantProjection_ :: Definition -> Maybe Projection +isRelevantProjection_ def = + if isIrrelevant def then Nothing else isProjection_ $ theDef def + -- | Is it a function marked STATIC? isStaticFun :: Defn -> Bool isStaticFun = (^. funStatic) @@ -1256,20 +1269,21 @@ (projIndex isP > 0) && isJust (projProper isP) -- | Number of dropped initial arguments of a projection(-like) function. -projectionArgs :: Defn -> Int -projectionArgs = maybe 0 (max 0 . pred . projIndex) . isProjection_ +projectionArgs :: Definition -> Int +projectionArgs = maybe 0 (max 0 . pred . projIndex) . isRelevantProjection_ -- | Check whether a definition uses copatterns. usesCopatterns :: (HasConstInfo m) => QName -> m Bool usesCopatterns q = defCopatternLHS <$> getConstInfo q -- | Apply a function @f@ to its first argument, producing the proper --- postfix projection if @f@ is a projection. +-- postfix projection if @f@ is a projection which is not irrelevant. applyDef :: (HasConstInfo m) => ProjOrigin -> QName -> Arg Term -> m Term applyDef o f a = do let fallback = return $ Def f [Apply a] - caseMaybeM (isProjection f) fallback $ \ isP -> do + -- Andreas, 2022-03-07, issue #5809: don't drop parameters of irrelevant projections. + caseMaybeM (isRelevantProjection f) fallback $ \ isP -> do if projIndex isP <= 0 then fallback else do -- Get the original projection, if existing. if isNothing (projProper isP) then fallback else do diff --git a/src/full/Agda/TypeChecking/Monad/State.hs b/src/full/Agda/TypeChecking/Monad/State.hs --- a/src/full/Agda/TypeChecking/Monad/State.hs +++ b/src/full/Agda/TypeChecking/Monad/State.hs @@ -5,7 +5,7 @@ import qualified Control.Exception as E -import Control.Monad.State (void) +import Control.Monad (void) import Control.Monad.Trans (MonadIO, liftIO) import Data.Maybe diff --git a/src/full/Agda/TypeChecking/Names.hs b/src/full/Agda/TypeChecking/Names.hs --- a/src/full/Agda/TypeChecking/Names.hs +++ b/src/full/Agda/TypeChecking/Names.hs @@ -22,11 +22,14 @@ -- Control.Monad.Fail import is redundant since GHC 8.8.1 import Control.Monad.Fail (MonadFail) -import Control.Monad.Except -import Control.Monad.Reader -import Control.Monad.State +import Control.Monad ( liftM2, unless ) +import Control.Monad.Except ( MonadError ) +import Control.Monad.IO.Class ( MonadIO(..) ) +import Control.Monad.Reader ( MonadReader(..), ReaderT, runReaderT ) +import Control.Monad.State ( MonadState ) +import Control.Monad.Trans ( MonadTrans, lift ) -import Data.List (isSuffixOf) +import Data.List ( isSuffixOf ) import Agda.Syntax.Common hiding (Nat) import Agda.Syntax.Internal diff --git a/src/full/Agda/TypeChecking/Polarity.hs b/src/full/Agda/TypeChecking/Polarity.hs --- a/src/full/Agda/TypeChecking/Polarity.hs +++ b/src/full/Agda/TypeChecking/Polarity.hs @@ -11,10 +11,10 @@ , polFromOcc ) where -import Control.Monad.State +import Control.Monad ( forM_, zipWithM ) import Data.Maybe -import Data.Semigroup (Semigroup(..)) +import Data.Semigroup ( Semigroup(..) ) import Agda.Syntax.Abstract.Name import Agda.Syntax.Common diff --git a/src/full/Agda/TypeChecking/Positivity.hs b/src/full/Agda/TypeChecking/Positivity.hs --- a/src/full/Agda/TypeChecking/Positivity.hs +++ b/src/full/Agda/TypeChecking/Positivity.hs @@ -6,7 +6,8 @@ import Control.Applicative hiding (empty) import Control.DeepSeq -import Control.Monad.Reader +import Control.Monad ( forM_, guard, liftM2 ) +import Control.Monad.Reader ( MonadReader(..), asks, Reader, runReader ) import Data.Either import qualified Data.Foldable as Fold @@ -260,13 +261,15 @@ getDefArity :: Definition -> TCM Int getDefArity def = do - let dropped = case theDef def of - defn@Function{} -> projectionArgs defn - _ -> 0 - -- TODO: instantiateFull followed by arity could perhaps be - -- optimised, presumably the instantiation can be performed - -- lazily. - subtract dropped . arity <$> instantiateFull (defType def) + subtract (projectionArgs def) <$> arity' (defType def) + where + -- A variant of "\t -> arity <$> instantiateFull t". + arity' :: Type -> TCM Int + arity' t = do + t <- instantiate t + case unEl t of + Pi _ t -> succ <$> arity' (unAbs t) + _ -> return 0 -- Computing occurrences -------------------------------------------------- diff --git a/src/full/Agda/TypeChecking/Pretty/Constraint.hs b/src/full/Agda/TypeChecking/Pretty/Constraint.hs --- a/src/full/Agda/TypeChecking/Pretty/Constraint.hs +++ b/src/full/Agda/TypeChecking/Pretty/Constraint.hs @@ -132,6 +132,8 @@ case mvJudgement m of HasType{ jMetaType = t } -> prettyTCM x <+> ":" <+> prettyTCM t IsSort{} -> prettyTCM x <+> "is a sort" + CheckType t -> + prettyTCM t <+> "is a well-formed type" CheckLockedVars t ty lk lk_ty -> do "Lock" <+> prettyTCM lk <+> "|-" <+> prettyTCMCtx TopCtx t <+> ":" <+> prettyTCM ty UsableAtModality mod t -> "Is usable at" <+> prettyTCM mod <+> ":" <+> prettyTCM t diff --git a/src/full/Agda/TypeChecking/Primitive.hs b/src/full/Agda/TypeChecking/Primitive.hs --- a/src/full/Agda/TypeChecking/Primitive.hs +++ b/src/full/Agda/TypeChecking/Primitive.hs @@ -547,12 +547,7 @@ -- and the conversion checker for eliminations does not -- like this. -- We can only do untyped equality, e.g., by normalisation. - -- Jesper, 2020-04-04: We reduce rather than normalise for - -- efficiency reasons. In general this is weaker but it is - -- equivalent at base types. A stronger version of - -- primEraseEquality (using type-directed conversion) may be - -- implemented using --rewriting. - (u', v') <- reduce' (u, v) + (u', v') <- normalise' (u, v) if u' == v' then redReturn $ refl u else return $ NoReduction $ map notReduced ts diff --git a/src/full/Agda/TypeChecking/Primitive/Cubical.hs b/src/full/Agda/TypeChecking/Primitive/Cubical.hs --- a/src/full/Agda/TypeChecking/Primitive/Cubical.hs +++ b/src/full/Agda/TypeChecking/Primitive/Cubical.hs @@ -461,6 +461,8 @@ -> FamilyOrNot (Arg Term, Arg Term, Arg Term, Arg Term, Arg Term, Arg Term) -> m Term +-- ... |- psi, u0 +-- ..., i |- la, lb, bA, phi, bT, e unglueTranspGlue psi u0 (IsFam (la, lb, bA, phi, bT, e)) = do let localUse = builtinTrans ++ " for " ++ builtinGlue @@ -496,21 +498,31 @@ <@> (imax phi (ineg i)) <@> u0 [psi,u0] <- mapM (open . unArg) [psi,u0] + + -- glue1 t a = glue la[i1/i] lb[i1/i] bA[i1/i] phi[i1/i] bT[i1/i] e[i1/i] t a glue1 <- do g <- open $ (tglue `apply`) . map ((setHiding Hidden) . (subst 0 io)) $ [la, lb, bA, phi, bT, e] return $ \ t a -> g <@> t <@> a - unglue0 <- do - ug <- open $ (tunglue `apply`) . map ((setHiding Hidden) . (subst 0 iz)) $ [la, lb, bA, phi, bT, e] - return $ \ a -> ug <@> a + [la, lb, bA, phi, bT, e] <- mapM (\ a -> open . runNames [] $ lam "i" (const (pure $ unArg a))) [la, lb, bA, phi, bT, e] + + -- Andreas, 2022-03-24, fixing #5838 + -- Following the updated note + -- + -- Simon Huber, A Cubical Type Theory for Higher Inductive Types + -- https://simhu.github.io/misc/hcomp.pdf (February 2022) + -- + -- See: https://github.com/agda/agda/issues/5755#issuecomment-1043797776 + + -- unglue_u0 i = unglue la[i/i] lb[i/i] bA[i/i] phi[i/i] bT[i/i] e[i/i] u0 + let unglue_u0 i = + foldl (<#>) (pure tunglue) (map (<@> i) [la, lb, bA, phi, bT, e]) <@> u0 + view <- intervalView' - -- phi1 <- view <$> (reduce =<< (phi <@> pure io)) - -- if not $ (isIOne phi1) then return Nothing else Just <$> do let tf i o = transpFill lb (lam "i" $ \ i -> bT <@> i <..> o) psi u0 i t1 o = tf (pure io) o - a0 = unglue0 u0 -- compute "forall. phi" forallphi = pure tForall <@> phi @@ -522,14 +534,14 @@ <@> psi <@> forallphi <@> ilam "o" (\ a -> bA <@> i) - <@> ilam "o" (\ _ -> a0) + <@> ilam "o" (\ _ -> unglue_u0 i) <@> ilam "o" (\ o -> pure tEFun <#> (lb <@> i) <#> (la <@> i) <#> (bT <@> i <..> o) <#> (bA <@> i) <@> (e <@> i <..> o) <@> (tf i o))) - a0 + (unglue_u0 (pure iz)) max l l' = pure tLMax <@> l <@> l' sigCon x y = pure (Con (sigmaCon kit) ConOSystem []) <@> x <@> y @@ -642,6 +654,9 @@ case tpos of Head -> t1 (pure tItIsOne) Eliminated -> a1 + +-- ... |- psi, u0 +-- ..., i |- la, lb, bA, phi, bT, e compGlue DoTransp psi Nothing u0 (IsFam (la, lb, bA, phi, bT, e)) tpos = do let localUse = builtinTrans ++ " for " ++ builtinGlue @@ -677,20 +692,32 @@ <@> (imax phi (ineg i)) <@> u0 [psi,u0] <- mapM (open . unArg) [psi,u0] + + -- glue1 t a = glue la[i1/i] lb[i1/i] bA[i1/i] phi[i1/i] bT[i1/i] e[i1/i] t a glue1 <- do g <- open $ (tglue `apply`) . map ((setHiding Hidden) . (subst 0 io)) $ [la, lb, bA, phi, bT, e] return $ \ t a -> g <@> t <@> a - unglue0 <- do - ug <- open $ (tunglue `apply`) . map ((setHiding Hidden) . (subst 0 iz)) $ [la, lb, bA, phi, bT, e] - return $ \ a -> ug <@> a + [la, lb, bA, phi, bT, e] <- mapM (\ a -> open . runNames [] $ lam "i" (const (pure $ unArg a))) [la, lb, bA, phi, bT, e] + + -- Andreas, 2022-03-24, fixing #5838 + -- Following the updated note + -- + -- Simon Huber, A Cubical Type Theory for Higher Inductive Types + -- https://simhu.github.io/misc/hcomp.pdf (February 2022) + -- + -- See: https://github.com/agda/agda/issues/5755#issuecomment-1043797776 + + -- unglue_u0 i = unglue la[i/i] lb[i/i] bA[i/i] phi[i/i] bT[i/i] e[i/e] u0 + let unglue_u0 i = + foldl (<#>) (pure tunglue) (map (<@> i) [la, lb, bA, phi, bT, e]) <@> u0 + view <- intervalView' ifM (headStop tpos (phi <@> pure io)) (return Nothing) $ Just <$> do let tf i o = transpFill lb (lam "i" $ \ i -> bT <@> i <..> o) psi u0 i t1 o = tf (pure io) o - a0 = unglue0 u0 -- compute "forall. phi" forallphi = pure tForall <@> phi @@ -701,15 +728,15 @@ (lam "i" $ \ i -> pure tPOr <#> (la <@> i) <@> psi <@> forallphi - <@> ilam "o" (\ a -> bA <@> i) - <@> ilam "o" (\ _ -> a0) + <@> ilam "o" (\ _ -> bA <@> i) + <@> ilam "o" (\ _ -> unglue_u0 i) <@> ilam "o" (\ o -> pure tEFun <#> (lb <@> i) <#> (la <@> i) <#> (bT <@> i <..> o) <#> (bA <@> i) <@> (e <@> i <..> o) <@> (tf i o))) - a0 + (unglue_u0 (pure iz)) max l l' = pure tLMax <@> l <@> l' sigCon x y = pure (Con (sigmaCon kit) ConOSystem []) <@> x <@> y @@ -864,21 +891,33 @@ let bAS = pure tSubIn <#> (pure tLSuc <@> la) <#> (Sort . tmSort <$> la) <#> phi <@> bA g <- (open =<<) $ pure tglue <#> la <#> phi <#> bT <#> bAS return $ \ t a -> g <@> t <@> a - unglue0 <- do - tunglue <- cl $ getTermLocal builtin_unglueU - [la, phi, bT, bA] <- mapM (open . unArg . subst 0 iz) $ [la, phi, bT, bA] - let bAS = pure tSubIn <#> (pure tLSuc <@> la) <#> (Sort . tmSort <$> la) <#> phi <@> bA - ug <- (open =<<) $ pure tunglue <#> la <#> phi <#> bT <#> bAS - return $ \ a -> ug <@> a + [la, phi, bT, bA] <- mapM (\ a -> open . runNames [] $ lam "i" (const (pure $ unArg a))) [la, phi, bT, bA] + -- Andreas, 2022-03-25, issue #5838. + -- Port the fix of @unglueTranspGlue@ and @compGlue DoTransp@ + -- also to @compHCompU DoTransp@, as suggested by Tom Jack and Anders Mörtberg. + -- We define @unglue_u0 i@ that is first used with @i@ and then with @i0@. + -- The original code used it only with @i0@. + tunglue <- cl $ getTermLocal builtin_unglueU + let bAS i = + pure tSubIn <#> (pure tLSuc <@> (la <@> i)) + <#> (Sort . tmSort <$> (la <@> i)) + <#> (phi <@> i) + <@> (bA <@> i) + let unglue_u0 i = + pure tunglue <#> (la <@> i) + <#> (phi <@> i) + <#> (bT <@> i) + <#> bAS i + <@> u0 + ifM (headStop tpos (phi <@> pure io)) (return Nothing) $ Just <$> do let lb = la tf i o = transpFill lb (lam "i" $ \ i -> bT <@> i <@> pure io <..> o) psi u0 i t1 o = tf (pure io) o - a0 = unglue0 u0 -- compute "forall. phi" forallphi = pure tForall <@> phi @@ -889,12 +928,12 @@ (lam "i" $ \ i -> pure tPOr <#> (la <@> i) <@> psi <@> forallphi - <@> ilam "o" (\ a -> bA <@> i) - <@> ilam "o" (\ _ -> a0) + <@> ilam "o" (\ _ -> bA <@> i) + <@> ilam "o" (\ _ -> unglue_u0 i) <@> ilam "o" (\ o -> transp (la <@> i) (\ j -> bT <@> i <@> ineg j <..> o) (tf i o))) - a0 + (unglue_u0 (pure iz)) w i o = lam "x" $ transp (la <@> i) diff --git a/src/full/Agda/TypeChecking/ProjectionLike.hs b/src/full/Agda/TypeChecking/ProjectionLike.hs --- a/src/full/Agda/TypeChecking/ProjectionLike.hs +++ b/src/full/Agda/TypeChecking/ProjectionLike.hs @@ -87,7 +87,7 @@ import Agda.Utils.Impossible --- | View for a @Def f (Apply a : es)@ where @isProjection f@. +-- | View for a @Def f (Apply a : es)@ where @isRelevantProjection f@. -- Used for projection-like @f@s. data ProjectionView = ProjectionView @@ -117,7 +117,7 @@ projView v = do let fallback = return $ NoProjection v case v of - Def f es -> caseMaybeM (isProjection f) fallback $ \ isP -> do + Def f es -> caseMaybeM (isRelevantProjection f) fallback $ \ isP -> do if projIndex isP <= 0 then fallback else do case es of [] -> return $ LoneProjectionLike f $ projArgInfo isP @@ -226,6 +226,8 @@ -- Thus, an application of @f@ waiting for a projection -- can be stuck even when the principal argument is a constructor. -- +-- g. @f@ cannot be an irrelevant definition (Andreas, 2022-03-07, #5809), +-- as those are not reduced. -- -- For internal reasons: -- @@ -247,7 +249,9 @@ [ "Checking for projection likeness " , prettyTCM x <+> " : " <+> prettyTCM t ] - case theDef defn of + if isIrrelevant defn then + reportSDoc "tc.proj.like" 30 $ " projection-like functions cannot be irrelevant" + else case theDef defn of Function{funClauses = cls} | any (isNothing . clauseBody) cls -> reportSLn "tc.proj.like" 30 $ " projection-like functions cannot have absurd clauses" diff --git a/src/full/Agda/TypeChecking/ReconstructParameters.hs b/src/full/Agda/TypeChecking/ReconstructParameters.hs --- a/src/full/Agda/TypeChecking/ReconstructParameters.hs +++ b/src/full/Agda/TypeChecking/ReconstructParameters.hs @@ -24,6 +24,7 @@ import Agda.Utils.Size import Agda.Utils.Either +import Agda.Utils.Function (applyWhen) import Agda.Utils.Impossible @@ -162,23 +163,18 @@ applyWithoutReversing _ _ = __IMPOSSIBLE__ mapHide (El _ (Pi a b)) (p:tl) = - case argInfoHiding (domInfo a) of - Hidden -> (hideAndRelParams p):(mapHide (unAbs b) tl) - _ -> p:(mapHide (unAbs b) tl) + applyWhen (getHiding a == Hidden) hideAndRelParams p : mapHide (unAbs b) tl mapHide t l = l dropParameters :: TermLike a => a -> TCM a -dropParameters = traverseTermM dropPars - where - dropPars v = - case v of +dropParameters = traverseTermM $ + \case Con c ci vs -> do Constructor{ conData = d } <- theDef <$> getConstInfo (conName c) Just n <- defParameters <$> getConstInfo d return $ Con c ci $ drop n vs - Def f vs -> do - isProj <- isProjection f - case isProj of + v@(Def f vs) -> do + isRelevantProjection f >>= \case Nothing -> return v Just pr -> return $ applyE (projDropPars pr ProjSystem) vs - _ -> return v + v -> return v diff --git a/src/full/Agda/TypeChecking/RecordPatterns.hs b/src/full/Agda/TypeChecking/RecordPatterns.hs --- a/src/full/Agda/TypeChecking/RecordPatterns.hs +++ b/src/full/Agda/TypeChecking/RecordPatterns.hs @@ -9,10 +9,13 @@ , recordPatternToProjections ) where -import Control.Arrow (first, second) -import Control.Monad.Fix -import Control.Monad.Reader -import Control.Monad.State +import Control.Arrow ( first, second ) +import Control.Monad ( forM, unless, when, zipWithM ) +import Control.Monad.Fix ( mfix ) +import Control.Monad.IO.Class ( MonadIO(..) ) +import Control.Monad.Reader ( MonadReader(..), ReaderT(..), runReaderT ) +import Control.Monad.State ( MonadState(..), StateT(..), runStateT ) +import Control.Monad.Trans ( lift ) import qualified Data.List as List import Data.Maybe diff --git a/src/full/Agda/TypeChecking/Reduce.hs b/src/full/Agda/TypeChecking/Reduce.hs --- a/src/full/Agda/TypeChecking/Reduce.hs +++ b/src/full/Agda/TypeChecking/Reduce.hs @@ -2,7 +2,7 @@ module Agda.TypeChecking.Reduce where -import Control.Monad.Reader +import Control.Monad ( (>=>), void ) import Data.Maybe import Data.Map (Map) @@ -232,6 +232,7 @@ CheckLockedVars <$> instantiate' a <*> instantiate' b <*> instantiate' c <*> instantiate' d instantiate' (UnquoteTactic t h g) = UnquoteTactic <$> instantiate' t <*> instantiate' h <*> instantiate' g instantiate' c@CheckMetaInst{} = return c + instantiate' (CheckType t) = CheckType <$> instantiate' t instantiate' (UsableAtModality mod t) = UsableAtModality mod <$> instantiate' t instance Instantiate CompareAs where @@ -555,12 +556,14 @@ -- (i.e., those that failed the termination check) -- and delayed definitions -- are not unfolded unless explicitly permitted. - dontUnfold = - (defNonterminating info && SmallSet.notMember NonTerminatingReductions allowed) - || (defTerminationUnconfirmed info && SmallSet.notMember UnconfirmedReductions allowed) - || (defDelayed info == Delayed && not unfoldDelayed) - || prp == Right True || isIrrelevant (defArgInfo info) - || not defOk + dontUnfold = or + [ defNonterminating info && SmallSet.notMember NonTerminatingReductions allowed + , defTerminationUnconfirmed info && SmallSet.notMember UnconfirmedReductions allowed + , defDelayed info == Delayed && not unfoldDelayed + , prp == Right True + , isIrrelevant info + , not defOk + ] copatterns = defCopatternLHS info case def of Constructor{conSrcCon = c} -> do @@ -573,12 +576,20 @@ cls (defCompiled info) rewr else noReduction $ notBlocked v PrimitiveSort{ primSort = s } -> yesReduction NoSimplification $ Sort s `applyE` es + _ -> do - if (RecursiveReductions `SmallSet.member` allowed) || - (isJust (isProjection_ def) && ProjectionReductions `SmallSet.member` allowed) || -- includes projection-like - (isInlineFun def && InlineReductions `SmallSet.member` allowed) || - (definitelyNonRecursive_ def && copatterns && CopatternReductions `SmallSet.member` allowed) || - (definitelyNonRecursive_ def && FunctionReductions `SmallSet.member` allowed) + if or + [ RecursiveReductions `SmallSet.member` allowed + , isJust (isProjection_ def) && ProjectionReductions `SmallSet.member` allowed + -- Includes projection-like and irrelevant projections. + -- Note: irrelevant projections lead to @dontUnfold@ and + -- so are not actually unfolded. + , isInlineFun def && InlineReductions `SmallSet.member` allowed + , definitelyNonRecursive_ def && or + [ copatterns && CopatternReductions `SmallSet.member` allowed + , FunctionReductions `SmallSet.member` allowed + ] + ] then reduceNormalE v0 f (map notReduced es) dontUnfold (defClauses info) (defCompiled info) rewr @@ -830,6 +841,7 @@ reduce' (CheckLockedVars a b c d) = CheckLockedVars <$> reduce' a <*> reduce' b <*> reduce' c <*> reduce' d reduce' c@CheckMetaInst{} = return c + reduce' (CheckType t) = CheckType <$> reduce' t reduce' (UsableAtModality mod t) = UsableAtModality mod <$> reduce' t instance Reduce CompareAs where @@ -994,6 +1006,7 @@ simplify' (CheckLockedVars a b c d) = CheckLockedVars <$> simplify' a <*> simplify' b <*> simplify' c <*> simplify' d simplify' c@CheckMetaInst{} = return c + simplify' (CheckType t) = CheckType <$> simplify' t simplify' (UsableAtModality mod t) = UsableAtModality mod <$> simplify' t instance Simplify CompareAs where @@ -1173,6 +1186,7 @@ normalise' (CheckLockedVars a b c d) = CheckLockedVars <$> normalise' a <*> normalise' b <*> normalise' c <*> normalise' d normalise' c@CheckMetaInst{} = return c + normalise' (CheckType t) = CheckType <$> normalise' t normalise' (UsableAtModality mod t) = UsableAtModality mod <$> normalise' t instance Normalise CompareAs where @@ -1405,6 +1419,7 @@ CheckLockedVars a b c d -> CheckLockedVars <$> instantiateFull' a <*> instantiateFull' b <*> instantiateFull' c <*> instantiateFull' d c@CheckMetaInst{} -> return c + CheckType t -> CheckType <$> instantiateFull' t UsableAtModality mod t -> UsableAtModality mod <$> instantiateFull' t instance InstantiateFull CompareAs where @@ -1532,24 +1547,44 @@ <*> return ell instance InstantiateFull Interface where - instantiateFull' (Interface h s ft ms mod scope inside - sig display userwarn importwarn b foreignCode - highlighting libPragmas filePragmas usedOpts patsyns - warnings partialdefs) = - Interface h s ft ms mod scope inside - <$> instantiateFull' sig - <*> instantiateFull' display - <*> return userwarn - <*> return importwarn - <*> instantiateFull' b - <*> return foreignCode - <*> return highlighting - <*> return libPragmas - <*> return filePragmas - <*> return usedOpts - <*> return patsyns - <*> return warnings - <*> return partialdefs + instantiateFull' i = do + defs <- instantiateFull' (i ^. intSignature . sigDefinitions) + instantiateFullExceptForDefinitions' + (set (intSignature . sigDefinitions) defs i) + +-- | Instantiates everything except for definitions in the signature. + +instantiateFullExceptForDefinitions' :: Interface -> ReduceM Interface +instantiateFullExceptForDefinitions' + (Interface h s ft ms mod scope inside sig display userwarn importwarn + b foreignCode highlighting libPragmas filePragmas usedOpts patsyns + warnings partialdefs) = + Interface h s ft ms mod scope inside + <$> ((\s r -> Sig { _sigSections = s + , _sigDefinitions = sig ^. sigDefinitions + , _sigRewriteRules = r + }) + <$> instantiateFull' (sig ^. sigSections) + <*> instantiateFull' (sig ^. sigRewriteRules)) + <*> instantiateFull' display + <*> return userwarn + <*> return importwarn + <*> instantiateFull' b + <*> return foreignCode + <*> return highlighting + <*> return libPragmas + <*> return filePragmas + <*> return usedOpts + <*> return patsyns + <*> return warnings + <*> return partialdefs + +-- | Instantiates everything except for definitions in the signature. + +instantiateFullExceptForDefinitions :: + MonadReduce m => Interface -> m Interface +instantiateFullExceptForDefinitions = + liftReduce . instantiateFullExceptForDefinitions' instance InstantiateFull a => InstantiateFull (Builtin a) where instantiateFull' (Builtin t) = Builtin <$> instantiateFull' t diff --git a/src/full/Agda/TypeChecking/Reduce/Fast.hs b/src/full/Agda/TypeChecking/Reduce/Fast.hs --- a/src/full/Agda/TypeChecking/Reduce/Fast.hs +++ b/src/full/Agda/TypeChecking/Reduce/Fast.hs @@ -502,9 +502,11 @@ -- | In most cases pointers that we dereference do not contain black holes. derefPointer_ :: Pointer s -> ST s (Closure s) -derefPointer_ ptr = do - Thunk cl <- derefPointer ptr - return cl +derefPointer_ ptr = + derefPointer ptr <&> \case + Thunk cl -> cl + BlackHole -> __IMPOSSIBLE__ + -- | Only use for debug printing! unsafeDerefPointer :: Pointer s -> Thunk (Closure s) diff --git a/src/full/Agda/TypeChecking/Reduce/Monad.hs b/src/full/Agda/TypeChecking/Reduce/Monad.hs --- a/src/full/Agda/TypeChecking/Reduce/Monad.hs +++ b/src/full/Agda/TypeChecking/Reduce/Monad.hs @@ -10,7 +10,7 @@ import Prelude hiding (null) -import Control.Monad.Reader +import Control.Monad ( liftM2 ) import qualified Data.Map as Map import Data.Maybe diff --git a/src/full/Agda/TypeChecking/Rewriting/NonLinMatch.hs b/src/full/Agda/TypeChecking/Rewriting/NonLinMatch.hs --- a/src/full/Agda/TypeChecking/Rewriting/NonLinMatch.hs +++ b/src/full/Agda/TypeChecking/Rewriting/NonLinMatch.hs @@ -22,9 +22,10 @@ import Prelude hiding (null, sequence) -import Control.Applicative (Alternative) -import Control.Monad.Except -import Control.Monad.State +import Control.Applicative ( Alternative ) +import Control.Monad ( void ) +import Control.Monad.Except ( MonadError(..), ExceptT, runExceptT ) +import Control.Monad.State ( MonadState, StateT, runStateT ) import qualified Control.Monad.Fail as Fail diff --git a/src/full/Agda/TypeChecking/Rewriting/NonLinPattern.hs b/src/full/Agda/TypeChecking/Rewriting/NonLinPattern.hs --- a/src/full/Agda/TypeChecking/Rewriting/NonLinPattern.hs +++ b/src/full/Agda/TypeChecking/Rewriting/NonLinPattern.hs @@ -6,7 +6,8 @@ module Agda.TypeChecking.Rewriting.NonLinPattern where -import Control.Monad.Reader +import Control.Monad ( (>=>), forM ) +import Control.Monad.Reader ( asks ) import Data.IntSet (IntSet) import qualified Data.IntSet as IntSet diff --git a/src/full/Agda/TypeChecking/Rules/Application.hs b/src/full/Agda/TypeChecking/Rules/Application.hs --- a/src/full/Agda/TypeChecking/Rules/Application.hs +++ b/src/full/Agda/TypeChecking/Rules/Application.hs @@ -10,7 +10,8 @@ import Prelude hiding ( null ) -import Control.Applicative ((<|>)) +import Control.Applicative ( (<|>) ) +import Control.Monad ( forM, forM_, guard, liftM2 ) import Control.Monad.Except import Control.Monad.Trans import Control.Monad.Trans.Maybe @@ -262,7 +263,8 @@ inferHeadDef :: ProjOrigin -> QName -> TCM (Elims -> Term, Type) inferHeadDef o x = do - proj <- isProjection x + -- Andreas, 2022-03-07, issue #5809: don't drop parameters of irrelevant projections. + proj <- isRelevantProjection x rel <- getRelevance . defArgInfo <$> getConstInfo x let app = case proj of diff --git a/src/full/Agda/TypeChecking/Rules/Decl.hs b/src/full/Agda/TypeChecking/Rules/Decl.hs --- a/src/full/Agda/TypeChecking/Rules/Decl.hs +++ b/src/full/Agda/TypeChecking/Rules/Decl.hs @@ -9,9 +9,10 @@ import Data.Either (partitionEithers) import qualified Data.Foldable as Fold +import qualified Data.IntMap as IntMap +import qualified Data.IntSet as IntSet import Data.Maybe import qualified Data.Set as Set -import qualified Data.IntSet as IntSet import Data.Set (Set) import Agda.Interaction.Highlighting.Generate @@ -213,7 +214,7 @@ A.Generalize{} -> pure () _ -> do reportSLn "tc.decl" 20 $ "Freezing all metas." - void $ freezeMetas' $ \ (MetaId x) -> IntSet.member x metas + void $ freezeMetas metas theMutualChecks @@ -335,7 +336,8 @@ lzero <- primLevelZero let vArg = defaultArg hArg = setHiding Hidden . vArg - m <- checkExpr e $ El (mkType 0) $ apply tcm [hArg lzero, vArg unit] + m <- applyQuantityToContext zeroQuantity $ + checkExpr e $ El (mkType 0) $ apply tcm [hArg lzero, vArg unit] res <- runUnquoteM $ tell xs >> evalTCM m case res of Left err -> typeError $ UnquoteFailed err @@ -522,10 +524,10 @@ (a, ms) <- metasCreatedBy m reportSLn "tc.decl" 20 $ "Attempting to solve constraints before freezing." wakeupConstraints_ -- solve emptiness and instance constraints - xs <- freezeMetas' $ (`IntSet.member` ms) . metaId + xs <- freezeMetas ms reportSDoc "tc.decl.ax" 20 $ vcat - [ "Abstract type signature produced new metas: " <+> sep (map prettyTCM $ IntSet.toList ms) - , "We froze the following ones of these: " <+> sep (map prettyTCM xs) + [ "Abstract type signature produced new metas: " <+> sep (map prettyTCM $ IntMap.keys ms) + , "We froze the following ones of these: " <+> sep (map prettyTCM $ IntSet.toList xs) ] return a diff --git a/src/full/Agda/TypeChecking/Rules/Def.hs b/src/full/Agda/TypeChecking/Rules/Def.hs --- a/src/full/Agda/TypeChecking/Rules/Def.hs +++ b/src/full/Agda/TypeChecking/Rules/Def.hs @@ -4,8 +4,8 @@ import Prelude hiding ( null ) -import Control.Monad.Except -import Control.Monad.State +import Control.Monad ( forM, forM_ ) +import Control.Monad.Except ( MonadError(..) ) import Data.Bifunctor import Data.Function diff --git a/src/full/Agda/TypeChecking/Rules/LHS.hs b/src/full/Agda/TypeChecking/Rules/LHS.hs --- a/src/full/Agda/TypeChecking/Rules/LHS.hs +++ b/src/full/Agda/TypeChecking/Rules/LHS.hs @@ -18,7 +18,7 @@ import Control.Monad import Control.Monad.Except import Control.Monad.Reader -import Control.Monad.Writer hiding ((<>)) +import Control.Monad.Writer ( MonadWriter(..), runWriterT ) import Control.Monad.Trans.Maybe import Data.IntSet (IntSet) diff --git a/src/full/Agda/TypeChecking/Rules/LHS/Problem.hs b/src/full/Agda/TypeChecking/Rules/LHS/Problem.hs --- a/src/full/Agda/TypeChecking/Rules/LHS/Problem.hs +++ b/src/full/Agda/TypeChecking/Rules/LHS/Problem.hs @@ -11,8 +11,9 @@ import Prelude hiding (null) -import Control.Arrow ( (***) ) -import Control.Monad.Writer hiding ((<>)) +import Control.Arrow ( (***) ) +import Control.Monad ( zipWithM ) +import Control.Monad.Writer ( MonadWriter(..), Writer, runWriter ) import Data.Functor (($>)) import Data.IntMap (IntMap) diff --git a/src/full/Agda/TypeChecking/Rules/LHS/Unify.hs b/src/full/Agda/TypeChecking/Rules/LHS/Unify.hs --- a/src/full/Agda/TypeChecking/Rules/LHS/Unify.hs +++ b/src/full/Agda/TypeChecking/Rules/LHS/Unify.hs @@ -1206,10 +1206,12 @@ -- Jesper, Andreas, 2018-10-17: the quantity of the equation is morally -- always @Quantity0@, since the indices of the data type are runtime erased. -- Thus, we need not change the quantity of the solution. + envmod <- viewTC eModality let eqrel = getRelevance dom eqmod = getModality dom varmod = getModality dom' mod = applyUnless (NonStrict `moreRelevant` eqrel) (setRelevance eqrel) + $ applyUnless (usableQuantity envmod) (setQuantity zeroQuantity) $ varmod reportSDoc "tc.lhs.unify" 65 $ text $ "Equation modality: " ++ show (getModality dom) reportSDoc "tc.lhs.unify" 65 $ text $ "Variable modality: " ++ show varmod diff --git a/src/full/Agda/TypeChecking/Rules/Term.hs b/src/full/Agda/TypeChecking/Rules/Term.hs --- a/src/full/Agda/TypeChecking/Rules/Term.hs +++ b/src/full/Agda/TypeChecking/Rules/Term.hs @@ -4,6 +4,7 @@ import Prelude hiding ( null ) +import Control.Monad ( (<=<), forM ) import Control.Monad.Except import Control.Monad.Reader @@ -1346,7 +1347,8 @@ -- | Unquote a TCM computation in a given hole. unquoteM :: A.Expr -> Term -> Type -> TCM () unquoteM tacA hole holeType = do - tac <- checkExpr tacA =<< (el primAgdaTerm --> el (primAgdaTCM <#> primLevelZero <@> primUnit)) + tac <- applyQuantityToContext zeroQuantity $ + checkExpr tacA =<< (el primAgdaTerm --> el (primAgdaTCM <#> primLevelZero <@> primUnit)) inFreshModuleIfFreeParams $ unquoteTactic tac hole holeType -- | Run a tactic `tac : Term → TC ⊤` in a hole (second argument) of the type @@ -1624,7 +1626,7 @@ -- #4131: Only DontExpandLast if no user written type signature let check | getOrigin info == Inserted = checkDontExpandLast | otherwise = checkExpr' - t <- isType_ t + t <- workOnTypes $ isType_ t v <- applyModalityToContext info $ check CmpLeq e t addLetBinding info (A.unBind x) v t ret diff --git a/src/full/Agda/TypeChecking/Serialise.hs b/src/full/Agda/TypeChecking/Serialise.hs --- a/src/full/Agda/TypeChecking/Serialise.hs +++ b/src/full/Agda/TypeChecking/Serialise.hs @@ -23,6 +23,8 @@ ) where +import Prelude hiding ( null ) + import System.Directory ( createDirectoryIfMissing ) import System.FilePath ( takeDirectory ) @@ -31,12 +33,14 @@ import qualified Control.Exception as E import Control.Monad import Control.Monad.Except +import Control.Monad.IO.Class ( MonadIO(..) ) import Control.Monad.Reader import Control.Monad.State.Strict import Data.Array.IArray import Data.Word -import qualified Data.ByteString.Builder as L +import Data.ByteString.Lazy ( ByteString ) +import Data.ByteString.Builder ( byteString, toLazyByteString ) import qualified Data.ByteString.Lazy as L import qualified Data.HashTable.IO as H import qualified Data.Map as Map @@ -66,6 +70,7 @@ import Agda.Utils.FileName (canonicalizeAbsolutePath) import Agda.Utils.Hash import Agda.Utils.IORef +import Agda.Utils.Null import Agda.Utils.Impossible @@ -74,15 +79,15 @@ -- 32-bit machines). Word64 does not have these problems. currentInterfaceVersion :: Word64 -currentInterfaceVersion = 20210514 * 10 + 1 +currentInterfaceVersion = 20220211 * 10 + 0 -- | The result of 'encode' and 'encodeInterface'. data Encoded = Encoded - { uncompressed :: L.ByteString + { uncompressed :: ByteString -- ^ The uncompressed bytestring, without hashes and the interface -- version. - , compressed :: L.ByteString + , compressed :: ByteString -- ^ The compressed bytestring. } @@ -135,7 +140,7 @@ } cbits <- Bench.billTo [ Bench.Serialization, Bench.Compress ] $ return $!! G.compressWith compressParams bits1 - let x = B.encode currentInterfaceVersion `L.append` cbits + let x = B.encode currentInterfaceVersion <> cbits return (Encoded { uncompressed = bits1, compressed = x }) where l h = List.map fst . List.sortBy (compare `on` snd) <$> H.toList h @@ -152,7 +157,7 @@ tickN (kind ++ " (reused)") $ fromIntegral reused #endif --- encode :: EmbPrj a => a -> TCM L.ByteString +-- encode :: EmbPrj a => a -> TCM ByteString -- encode a = do -- fileMod <- sourceToModule -- (x, shared, total) <- liftIO $ do @@ -160,7 +165,7 @@ -- root <- runReaderT (icode a) newD -- nL <- l nD; sL <- l sD; iL <- l iD; dL <- l dD -- (shared, total) <- readIORef stats --- return (B.encode currentInterfaceVersion `L.append` +-- return (B.encode currentInterfaceVersion <> -- G.compress (B.encode (root, nL, sL, iL, dL)), shared, total) -- verboseS "profile.sharing" 10 $ do -- tickN "pointers (reused)" $ fromIntegral shared @@ -174,7 +179,7 @@ -- -- Returns 'Nothing' if a decoding error is encountered. -decode :: EmbPrj a => L.ByteString -> TCM (Maybe a) +decode :: EmbPrj a => ByteString -> TCM (Maybe a) decode s = do mf <- useTC stModuleToSource incs <- getIncludeDirs @@ -186,7 +191,7 @@ (mf, r) <- liftIO $ E.handle (\(E.ErrorCall s) -> noResult s) $ do ((r, nL, ltL, stL, bL, iL, dL), s, _) <- return $ runGetState B.get s 0 - if s /= L.empty + if not (null s) then noResult "Garbage at end." else do @@ -226,9 +231,9 @@ encodeInterface :: Interface -> TCM Encoded encodeInterface i = do r <- encode i - return (r { compressed = L.append hashes (compressed r) }) + return r{ compressed = hashes <> compressed r } where - hashes :: L.ByteString + hashes :: ByteString hashes = B.runPut $ B.put (iSourceHash i) >> B.put (iFullHash i) -- | Encodes an interface. To ensure relocatability file paths in @@ -237,7 +242,7 @@ -- An uncompressed bytestring corresponding to the encoded interface -- is returned. -encodeFile :: FilePath -> Interface -> TCM L.ByteString +encodeFile :: FilePath -> Interface -> TCM ByteString encodeFile f i = do r <- encodeInterface i liftIO $ createDirectoryIfMissing True (takeDirectory f) @@ -249,7 +254,7 @@ -- Returns 'Nothing' if the file does not start with the right magic -- number or some other decoding error is encountered. -decodeInterface :: L.ByteString -> TCM (Maybe Interface) +decodeInterface :: ByteString -> TCM (Maybe Interface) decodeInterface s = do -- Note that runGetState and the decompression code below can raise @@ -264,10 +269,10 @@ if ver /= currentInterfaceVersion then Left "Wrong interface version." else Right $ - L.toLazyByteString $ + toLazyByteString $ Z.foldDecompressStreamWithInput - (\s -> (L.byteString s <>)) - (\s -> if L.null s + (\s -> (byteString s <>)) + (\s -> if null s then mempty else error "Garbage at end.") (\err -> error (show err)) @@ -281,7 +286,7 @@ "Error when decoding interface file: " ++ err return Nothing -decodeHashes :: L.ByteString -> Maybe (Hash, Hash) +decodeHashes :: ByteString -> Maybe (Hash, Hash) decodeHashes s | L.length s < 16 = Nothing | otherwise = Just $ B.runGet getH $ L.take 16 s diff --git a/src/full/Agda/TypeChecking/Serialise/Base.hs b/src/full/Agda/TypeChecking/Serialise/Base.hs --- a/src/full/Agda/TypeChecking/Serialise/Base.hs +++ b/src/full/Agda/TypeChecking/Serialise/Base.hs @@ -9,6 +9,7 @@ import Control.Monad.Catch (catchAll) import Control.Monad.Except +import Control.Monad.IO.Class ( MonadIO(..) ) import Control.Monad.Reader import Control.Monad.State.Strict (StateT, gets) diff --git a/src/full/Agda/TypeChecking/Serialise/Instances/Common.hs b/src/full/Agda/TypeChecking/Serialise/Instances/Common.hs --- a/src/full/Agda/TypeChecking/Serialise/Instances/Common.hs +++ b/src/full/Agda/TypeChecking/Serialise/Instances/Common.hs @@ -3,10 +3,11 @@ module Agda.TypeChecking.Serialise.Instances.Common (SerialisedRange(..)) where -import Control.Monad.Except -import Control.Monad.Reader -import Control.Monad.State.Strict (gets, modify) - +import Control.Monad ( (<=<) ) +import Control.Monad.IO.Class ( MonadIO(..) ) +import Control.Monad.Except ( MonadError(..) ) +import Control.Monad.Reader ( MonadReader(..), asks ) +import Control.Monad.State.Strict ( gets, modify ) import Data.Array.IArray import Data.Word diff --git a/src/full/Agda/TypeChecking/Serialise/Instances/Errors.hs b/src/full/Agda/TypeChecking/Serialise/Instances/Errors.hs --- a/src/full/Agda/TypeChecking/Serialise/Instances/Errors.hs +++ b/src/full/Agda/TypeChecking/Serialise/Instances/Errors.hs @@ -239,13 +239,9 @@ instance EmbPrj LibWarning' where icod_ = \case UnknownField a -> icodeN 0 UnknownField a - ExeNotFound a b -> icodeN 1 ExeNotFound a b - ExeNotExecutable a b -> icodeN 2 ExeNotExecutable a b value = vcase $ \case [0, a] -> valuN UnknownField a - [1, a, b] -> valuN ExeNotFound a b - [2, a, b] -> valuN ExeNotExecutable a b _ -> malformed instance EmbPrj ExecutablesFile where diff --git a/src/full/Agda/TypeChecking/SizedTypes.hs b/src/full/Agda/TypeChecking/SizedTypes.hs --- a/src/full/Agda/TypeChecking/SizedTypes.hs +++ b/src/full/Agda/TypeChecking/SizedTypes.hs @@ -4,8 +4,9 @@ import Prelude hiding (null) -import Control.Monad.Except -import Control.Monad.Writer +import Control.Monad +import Control.Monad.Except ( MonadError(..) ) +import Control.Monad.Writer ( MonadWriter(..), WriterT(..), runWriterT ) import qualified Data.Foldable as Fold import qualified Data.List as List diff --git a/src/full/Agda/TypeChecking/Substitute.hs b/src/full/Agda/TypeChecking/Substitute.hs --- a/src/full/Agda/TypeChecking/Substitute.hs +++ b/src/full/Agda/TypeChecking/Substitute.hs @@ -993,6 +993,7 @@ CheckLockedVars a b c d -> CheckLockedVars (rf a) (rf b) (rf c) (rf d) UnquoteTactic t h g -> UnquoteTactic (rf t) (rf h) (rf g) CheckMetaInst m -> CheckMetaInst m + CheckType t -> CheckType (rf t) UsableAtModality mod m -> UsableAtModality mod (rf m) where rf :: forall a. TermSubst a => a -> a diff --git a/src/full/Agda/TypeChecking/SyntacticEquality.hs b/src/full/Agda/TypeChecking/SyntacticEquality.hs --- a/src/full/Agda/TypeChecking/SyntacticEquality.hs +++ b/src/full/Agda/TypeChecking/SyntacticEquality.hs @@ -9,10 +9,12 @@ module Agda.TypeChecking.SyntacticEquality (SynEq, checkSyntacticEquality) where -import Control.Arrow ((***)) -import Control.Monad.State +import Control.Arrow ( (***) ) +import Control.Monad ( zipWithM ) +import Control.Monad.State ( MonadState(..), StateT, runStateT ) +import Control.Monad.Trans ( lift ) -import Agda.Interaction.Options (optSyntacticEquality) +import Agda.Interaction.Options ( optSyntacticEquality ) import Agda.Syntax.Common import Agda.Syntax.Internal diff --git a/src/full/Agda/TypeChecking/Unquote.hs b/src/full/Agda/TypeChecking/Unquote.hs --- a/src/full/Agda/TypeChecking/Unquote.hs +++ b/src/full/Agda/TypeChecking/Unquote.hs @@ -1,11 +1,14 @@ module Agda.TypeChecking.Unquote where -import Control.Arrow (first, second) -import Control.Monad.Except -import Control.Monad.Reader -import Control.Monad.State -import Control.Monad.Writer hiding ((<>)) +import Control.Arrow ( first, second, (&&&) ) +import Control.Monad ( (<=<) ) +import Control.Monad.Except ( MonadError(..), ExceptT(..), runExceptT ) +import Control.Monad.IO.Class ( MonadIO(..) ) +import Control.Monad.Reader ( ReaderT(..), runReaderT ) +import Control.Monad.State ( gets, modify, StateT(..), runStateT ) +import Control.Monad.Writer ( MonadWriter(..), WriterT(..), runWriterT ) +import Control.Monad.Trans ( lift ) import Data.Char import Data.Map (Map) @@ -17,6 +20,7 @@ import qualified Data.Text as T import Data.Word +import System.Directory (doesFileExist, getPermissions, executable) import System.Process ( readProcessWithExitCode ) import System.Exit ( ExitCode(..) ) @@ -658,6 +662,8 @@ tcFreshName :: Text -> TCM Term tcFreshName s = do + whenM (viewTC eCurrentlyElaborating) $ + typeError $ GenericError "Not supported: declaring new names from an edit-time macro" m <- currentModule quoteName . qualify m <$> freshName_ (T.unpack s) @@ -963,8 +969,13 @@ requireAllowExec exes <- optTrustedExecutables <$> commandLineOptions case Map.lookup exe exes of - Nothing -> raiseExeNotFound exe exes + Nothing -> raiseExeNotTrusted exe exes Just fp -> do + -- Check that the executable exists. + unlessM (liftIO $ doesFileExist fp) $ raiseExeNotFound exe fp + -- Check that the executable is executable. + unlessM (liftIO $ executable <$> getPermissions fp) $ raiseExeNotExecutable exe fp + let strArgs = T.unpack <$> args let strStdIn = T.unpack stdIn (datExitCode, strStdOut, strStdErr) <- lift $ readProcessWithExitCode fp strArgs strStdIn @@ -976,8 +987,16 @@ -- | Raise an error if the trusted executable cannot be found. -- -raiseExeNotFound :: ExeName -> Map ExeName FilePath -> TCM a -raiseExeNotFound exe exes = genericDocError =<< do +raiseExeNotTrusted :: ExeName -> Map ExeName FilePath -> TCM a +raiseExeNotTrusted exe exes = genericDocError =<< do vcat . map pretty $ ("Could not find '" ++ T.unpack exe ++ "' in list of trusted executables:") : [ " - " ++ T.unpack exe | exe <- Map.keys exes ] + +raiseExeNotFound :: ExeName -> FilePath -> TCM a +raiseExeNotFound exe fp = genericDocError =<< do + text $ "Could not find file '" ++ fp ++ "' for trusted executable " ++ T.unpack exe + +raiseExeNotExecutable :: ExeName -> FilePath -> TCM a +raiseExeNotExecutable exe fp = genericDocError =<< do + text $ "File '" ++ fp ++ "' for trusted executable" ++ T.unpack exe ++ " does not have permission to execute" diff --git a/src/full/Agda/Utils/Benchmark.hs b/src/full/Agda/Utils/Benchmark.hs --- a/src/full/Agda/Utils/Benchmark.hs +++ b/src/full/Agda/Utils/Benchmark.hs @@ -12,6 +12,7 @@ import Control.Monad.Reader import Control.Monad.Writer import Control.Monad.State +import Control.Monad.IO.Class ( MonadIO(..) ) import Data.Function diff --git a/src/full/Agda/Utils/Graph/AdjacencyMap/Unidirectional.hs b/src/full/Agda/Utils/Graph/AdjacencyMap/Unidirectional.hs --- a/src/full/Agda/Utils/Graph/AdjacencyMap/Unidirectional.hs +++ b/src/full/Agda/Utils/Graph/AdjacencyMap/Unidirectional.hs @@ -377,7 +377,7 @@ -- occur in both graphs (labels from the first graph are given as the -- first argument to the function). -- --- Time complexity: /O(n₁ log (n₂/n₁ + 1) + e₁ log e₂/, where /n₁/ is +-- Time complexity: /O(n₁ log (n₂/n₁ + 1) + e₁ log e₂)/, where /n₁/ is -- the number of nodes in the graph with the smallest number of nodes -- and /n₂/ is the number of nodes in the other graph, and /e₁/ is the -- number of edges in the graph with the smallest number of edges and diff --git a/src/full/Agda/Utils/IO/Directory.hs b/src/full/Agda/Utils/IO/Directory.hs --- a/src/full/Agda/Utils/IO/Directory.hs +++ b/src/full/Agda/Utils/IO/Directory.hs @@ -4,7 +4,10 @@ where import Control.Monad -import Control.Monad.Writer +import Control.Monad.Writer ( WriterT, execWriterT, tell ) +import Control.Monad.Trans ( lift ) + +import Data.Monoid ( Endo(Endo, appEndo) ) import System.Directory import System.FilePath diff --git a/src/full/Agda/Utils/IO/UTF8.hs b/src/full/Agda/Utils/IO/UTF8.hs --- a/src/full/Agda/Utils/IO/UTF8.hs +++ b/src/full/Agda/Utils/IO/UTF8.hs @@ -2,6 +2,7 @@ module Agda.Utils.IO.UTF8 ( readTextFile + , Agda.Utils.IO.UTF8.readFile , Agda.Utils.IO.UTF8.writeFile , writeTextToFile ) where @@ -40,6 +41,15 @@ IO.NewlineMode { IO.inputNL = IO.CRLF, IO.outputNL = IO.LF } IO.hSetEncoding h IO.utf8 T.hGetContents h + +-- | Reads a UTF8-encoded text file and converts many character +-- sequences which may be interpreted as line or paragraph separators +-- into '\n'. + +readFile :: FilePath -> IO String +readFile f = do + s <- readTextFile f + return $ T.unpack s -- | Writes a UTF8-encoded text file. The native convention for line -- endings is used. diff --git a/src/full/Agda/Utils/ListT.hs b/src/full/Agda/Utils/ListT.hs --- a/src/full/Agda/Utils/ListT.hs +++ b/src/full/Agda/Utils/ListT.hs @@ -15,6 +15,7 @@ import Control.Monad.Fail as Fail import Control.Monad.Reader import Control.Monad.State +import Control.Monad.IO.Class ( MonadIO(..) ) #if !(MIN_VERSION_base(4,11,0)) import Data.Semigroup (Semigroup(..)) diff --git a/src/full/Agda/Utils/Monad.hs b/src/full/Agda/Utils/Monad.hs --- a/src/full/Agda/Utils/Monad.hs +++ b/src/full/Agda/Utils/Monad.hs @@ -7,9 +7,10 @@ ) where -import Control.Applicative (liftA2) -import Control.Monad.Except -import Control.Monad.State +import Control.Applicative ( liftA2 ) +import Control.Monad ( MonadPlus(..), guard, unless, when ) +import Control.Monad.Except ( MonadError(catchError, throwError) ) +import Control.Monad.State ( MonadState(get, put) ) import Data.Traversable as Trav hiding (for, sequence) import Data.Foldable as Fold diff --git a/src/full/Agda/Utils/Null.hs b/src/full/Agda/Utils/Null.hs --- a/src/full/Agda/Utils/Null.hs +++ b/src/full/Agda/Utils/Null.hs @@ -11,8 +11,8 @@ import Control.Monad.Reader import Control.Monad.State -import Data.ByteString.Char8 (ByteString) -import qualified Data.ByteString.Char8 as ByteString +import qualified Data.ByteString.Char8 as ByteStringChar8 +import qualified Data.ByteString.Lazy as ByteStringLazy import Data.HashMap.Strict (HashMap) import qualified Data.HashMap.Strict as HashMap @@ -64,9 +64,13 @@ empty = (empty, empty, empty, empty) null (a,b,c,d) = null a && null b && null c && null d -instance Null ByteString where - empty = ByteString.empty - null = ByteString.null +instance Null ByteStringChar8.ByteString where + empty = ByteStringChar8.empty + null = ByteStringChar8.null + +instance Null ByteStringLazy.ByteString where + empty = ByteStringLazy.empty + null = ByteStringLazy.null instance Null Text where empty = Text.empty diff --git a/src/full/Agda/Utils/Suffix.hs b/src/full/Agda/Utils/Suffix.hs --- a/src/full/Agda/Utils/Suffix.hs +++ b/src/full/Agda/Utils/Suffix.hs @@ -2,6 +2,7 @@ module Agda.Utils.Suffix where import Data.Char +import qualified Data.List as List import Agda.Utils.Impossible @@ -37,12 +38,11 @@ -- | Classification of identifier variants. data Suffix - = Prime Int -- ^ Identifier ends in @Int@ many primes. - | Index Int -- ^ Identifier ends in number @Int@ (ordinary digits). - | Subscript Int -- ^ Identifier ends in number @Int@ (subscript digits). + = Prime Integer -- ^ Identifier ends in @Integer@ many primes. + | Index Integer -- ^ Identifier ends in number @Integer@ (ordinary digits). + | Subscript Integer -- ^ Identifier ends in number @Integer@ (subscript digits). --- | Increase the suffix by one. If no suffix yet, put a subscript @1@ --- unless users do not want us to use any unicode. +-- | Increase the suffix by one. nextSuffix :: Suffix -> Suffix nextSuffix (Prime i) = Prime $ i + 1 @@ -53,17 +53,27 @@ suffixView :: String -> (String, Maybe Suffix) suffixView s - | (ps@(_:_), s') <- span (=='\'') rs = (reverse s', Just $ Prime $ length ps) + | (ps@(_:_), s') <- span (=='\'') rs = (reverse s', Just $ Prime $ List.genericLength ps) | (ns@(_:_), s') <- span isDigit rs = (reverse s', Just $ Index $ read $ reverse ns) | (ns@(_:_), s') <- span isSubscriptDigit rs = (reverse s', Just $ Subscript $ read $ map fromSubscriptDigit $ reverse ns) | otherwise = (s, Nothing) where rs = reverse s +-- Note: suffixView could be implemented using spanEnd, but the implementation using reverse +-- looks more efficient, since the reversal is only done once. +-- +-- suffixView :: String -> (String, Maybe Suffix) +-- suffixView s +-- | (s', ps@(_:_)) <- spanEnd (=='\'') s = (s', Just $ Prime $ length ps) +-- | (s', ns@(_:_)) <- spanEnd isDigit s = (s', Just $ Index $ read ns) +-- | (s', ns@(_:_)) <- spanEnd isSubscriptDigit s = (s', Just $ Subscript $ read $ map fromSubscriptDigit ns) +-- | otherwise = (s, Nothing) + -- | Print suffix. renderSuffix :: Suffix -> String -renderSuffix (Prime n) = replicate n '\'' +renderSuffix (Prime n) = List.genericReplicate n '\'' renderSuffix (Index i) = show i renderSuffix (Subscript i) = map toSubscriptDigit (show i) diff --git a/src/full/Agda/Utils/Update.hs b/src/full/Agda/Utils/Update.hs --- a/src/full/Agda/Utils/Update.hs +++ b/src/full/Agda/Utils/Update.hs @@ -25,8 +25,9 @@ -- NB: Control.Monad.Trans.Identity is already exported by Control.Monad.Identity -- since version mtl 2.2.2, but this needs at least ghc 8.2.2 import Control.Monad.Trans.Identity -import Control.Monad.Writer.Strict +import Control.Monad.Writer.Strict ( MonadWriter(..), Writer, WriterT, mapWriterT, runWriterT ) +import Data.Monoid ( Any(..) ) import Agda.Utils.Tuple diff --git a/stack-8.10.7.yaml b/stack-8.10.7.yaml --- a/stack-8.10.7.yaml +++ b/stack-8.10.7.yaml @@ -1,4 +1,4 @@ -resolver: lts-18.10 +resolver: lts-18.22 compiler: ghc-8.10.7 compiler-check: match-exact diff --git a/stack-9.0.1.yaml b/stack-9.0.1.yaml --- a/stack-9.0.1.yaml +++ b/stack-9.0.1.yaml @@ -1,4 +1,4 @@ -resolver: nightly-2021-11-12 +resolver: nightly-2022-01-06 compiler: ghc-9.0.1 compiler-check: match-exact @@ -7,6 +7,9 @@ # happy-1.21.0 is deprecated, but currently in nightly # (commercialhaskell/stackage#6294) - happy-1.20.0 +# Andreas, 2022-02-07 +# On Windows, we install the latest ICU (v69), which is only supported from text-icu >= 0.8 +- text-icu-0.8.0 flags: transformers-compat: diff --git a/stack-9.0.2.yaml b/stack-9.0.2.yaml new file mode 100644 --- /dev/null +++ b/stack-9.0.2.yaml @@ -0,0 +1,7 @@ +resolver: lts-19.0 +compiler: ghc-9.0.2 +compiler-check: match-exact + +# Local packages, usually specified by relative directory name +packages: +- '.' diff --git a/stack-9.2.1.yaml b/stack-9.2.1.yaml --- a/stack-9.2.1.yaml +++ b/stack-9.2.1.yaml @@ -71,7 +71,7 @@ - process-extras-0.7.4 - random-1.2.1 - regex-base-0.94.0.1 -- regex-posix-0.96.0.0 +- regex-posix-0.96.0.1 - regex-tdfa-1.3.1.1 - safe-0.3.19 - scientific-0.3.7.0 @@ -89,7 +89,7 @@ - temporary-1.3 - test-framework-0.8.2.0 - test-framework-hunit-0.3.0.2 -- text-icu-0.7.1.0 +- text-icu-0.8.0.1 - text-short-0.1.4 - th-abstraction-0.4.3.0 - th-compat-0.1.3 diff --git a/stack-9.2.2.yaml b/stack-9.2.2.yaml new file mode 100644 --- /dev/null +++ b/stack-9.2.2.yaml @@ -0,0 +1,6 @@ +resolver: nightly-2022-03-26 +compiler: ghc-9.2.2 +compiler-check: match-exact + +packages: +- '.'