summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorAndresSicardRamirez <>2019-05-17 23:02:00 (GMT)
committerhdiff <hdiff@hdiff.luite.com>2019-05-17 23:02:00 (GMT)
commit31d1cd473230453a02cdc340259f2372df397b2f (patch)
treee247584ea14ad464674fec464c7c79a4f9abeb0d
parent87e5acbc1486d2241581cd8a65d02919c1a8616e (diff)
version 2.6.0.1HEAD2.6.0.1master
-rw-r--r--Agda.cabal74
-rw-r--r--CHANGELOG.md44
-rw-r--r--Setup.hs4
-rw-r--r--dist/build/Agda/Syntax/Parser/Parser.hs407
-rw-r--r--doc/user-manual.pdfbin872344 -> 872824 bytes
-rw-r--r--src/data/MAlonzo/src/MAlonzo/RTE.hs10
-rw-r--r--src/data/emacs-mode/agda2-mode-pkg.el2
-rw-r--r--src/data/emacs-mode/agda2-mode.el2
-rw-r--r--src/data/lib/prim/Agda/Builtin/Word/Properties.agda10
-rw-r--r--src/full/Agda/Compiler/Backend.hs8
-rw-r--r--src/full/Agda/Compiler/Common.hs1
-rw-r--r--src/full/Agda/Compiler/JS/Compiler.hs4
-rw-r--r--src/full/Agda/Compiler/MAlonzo/Compiler.hs23
-rw-r--r--src/full/Agda/Compiler/MAlonzo/Pragmas.hs10
-rw-r--r--src/full/Agda/Compiler/MAlonzo/Primitives.hs40
-rw-r--r--src/full/Agda/Interaction/BasicOps.hs7
-rw-r--r--src/full/Agda/Interaction/Highlighting/Generate.hs15
-rw-r--r--src/full/Agda/Interaction/InteractionTop.hs11
-rw-r--r--src/full/Agda/Interaction/Options/Lenses.hs1
-rw-r--r--src/full/Agda/Syntax/Internal.hs6
-rw-r--r--src/full/Agda/TypeChecking/Conversion.hs10
-rw-r--r--src/full/Agda/TypeChecking/Coverage.hs19
-rw-r--r--src/full/Agda/TypeChecking/Empty.hs26
-rw-r--r--src/full/Agda/TypeChecking/Empty.hs-boot3
-rw-r--r--src/full/Agda/TypeChecking/Errors.hs11
-rw-r--r--src/full/Agda/TypeChecking/Generalize.hs14
-rw-r--r--src/full/Agda/TypeChecking/IApplyConfluence.hs17
-rw-r--r--src/full/Agda/TypeChecking/InstanceArguments.hs3
-rw-r--r--src/full/Agda/TypeChecking/MetaVars/Occurs.hs14
-rw-r--r--src/full/Agda/TypeChecking/Monad/Base.hs6
-rw-r--r--src/full/Agda/TypeChecking/Monad/Builtin.hs2
-rw-r--r--src/full/Agda/TypeChecking/Monad/MetaVars.hs64
-rw-r--r--src/full/Agda/TypeChecking/Monad/Signature.hs2
-rw-r--r--src/full/Agda/TypeChecking/Monad/Signature.hs-boot2
-rw-r--r--src/full/Agda/TypeChecking/Names.hs22
-rw-r--r--src/full/Agda/TypeChecking/Primitive.hs30
-rw-r--r--src/full/Agda/TypeChecking/Records.hs70
-rw-r--r--src/full/Agda/TypeChecking/Reduce.hs3
-rw-r--r--src/full/Agda/TypeChecking/Rewriting.hs12
-rw-r--r--src/full/Agda/TypeChecking/Rewriting/NonLinMatch.hs6
-rw-r--r--src/full/Agda/TypeChecking/Rules/Data.hs142
-rw-r--r--src/full/Agda/TypeChecking/Rules/LHS/ProblemRest.hs4
-rw-r--r--src/full/Agda/TypeChecking/Rules/Record.hs18
-rw-r--r--src/full/Agda/TypeChecking/Rules/Term.hs36
-rw-r--r--src/full/Agda/TypeChecking/Serialise/Instances/Errors.hs1
-rw-r--r--src/full/Agda/TypeChecking/SizedTypes/Solve.hs3
-rw-r--r--src/full/Agda/TypeChecking/Telescope.hs6
-rw-r--r--src/full/Agda/Utils/Singleton.hs4
-rw-r--r--stack-8.6.4.yaml20
-rw-r--r--stack-8.6.5.yaml9
50 files changed, 504 insertions, 754 deletions
diff --git a/Agda.cabal b/Agda.cabal
index 1d157c8..c4d63c1 100644
--- a/Agda.cabal
+++ b/Agda.cabal
@@ -1,5 +1,5 @@
name: Agda
-version: 2.6.0
+version: 2.6.0.1
cabal-version: >= 1.10
build-type: Custom
license: OtherLicense
@@ -37,7 +37,8 @@ tested-with: GHC == 7.10.3
GHC == 8.0.2
GHC == 8.2.2
GHC == 8.4.4
- GHC == 8.6.4
+ GHC == 8.6.5
+
extra-source-files: CHANGELOG.md
README.md
doc/user-manual.pdf
@@ -46,7 +47,7 @@ extra-source-files: CHANGELOG.md
stack-8.0.2.yaml
stack-8.2.2.yaml
stack-8.4.4.yaml
- stack-8.6.4.yaml
+ stack-8.6.5.yaml
data-dir: src/data
data-files: Agda.css
@@ -82,6 +83,7 @@ data-files: Agda.css
lib/prim/Agda/Builtin/TrustMe.agda
lib/prim/Agda/Builtin/Unit.agda
lib/prim/Agda/Builtin/Word.agda
+ lib/prim/Agda/Builtin/Word/Properties.agda
lib/prim/Agda/Primitive.agda
lib/prim/Agda/Primitive/Cubical.agda
MAlonzo/src/MAlonzo/*.hs
@@ -94,7 +96,7 @@ source-repository head
source-repository this
type: git
location: https://github.com/agda/agda.git
- tag: v2.6.0
+ tag: v2.6.0.1
flag cpphs
default: False
@@ -225,7 +227,7 @@ library
-- ASR (2018-09-14). We add the dependency on the filemanip library
-- due to Issue #3225.
- if impl(ghc >= 7.10) && impl(ghc < 8.0)
+ if impl(ghc < 8.0)
build-depends: transformers == 0.4.2.0
, filemanip >= 0.3.6.2 && < 0.4
@@ -576,33 +578,32 @@ library
if impl(ghc >= 8.0)
ghc-options: -Wunrecognised-warning-flags
- if impl(ghc >= 7.10)
- ghc-options: -fwarn-deprecated-flags
- -fwarn-deriving-typeable
- -fwarn-dodgy-exports
- -fwarn-dodgy-foreign-imports
- -fwarn-dodgy-imports
- -fwarn-duplicate-exports
- -fwarn-empty-enumerations
- -fwarn-hi-shadowing
- -fwarn-identities
- -fwarn-incomplete-patterns
- -fwarn-inline-rule-shadowing
- -fwarn-missing-fields
- -fwarn-missing-methods
- -fwarn-missing-signatures
- -fwarn-tabs
- -fwarn-typed-holes
- -fwarn-overflowed-literals
- -fwarn-overlapping-patterns
- -fwarn-unrecognised-pragmas
- -fwarn-unticked-promoted-constructors
- -fwarn-unused-do-bind
- -fwarn-warnings-deprecations
- -fwarn-wrong-do-bind
+ ghc-options: -fwarn-deprecated-flags
+ -fwarn-deriving-typeable
+ -fwarn-dodgy-exports
+ -fwarn-dodgy-foreign-imports
+ -fwarn-dodgy-imports
+ -fwarn-duplicate-exports
+ -fwarn-empty-enumerations
+ -fwarn-hi-shadowing
+ -fwarn-identities
+ -fwarn-incomplete-patterns
+ -fwarn-inline-rule-shadowing
+ -fwarn-missing-fields
+ -fwarn-missing-methods
+ -fwarn-missing-signatures
+ -fwarn-tabs
+ -fwarn-typed-holes
+ -fwarn-overflowed-literals
+ -fwarn-overlapping-patterns
+ -fwarn-unrecognised-pragmas
+ -fwarn-unticked-promoted-constructors
+ -fwarn-unused-do-bind
+ -fwarn-warnings-deprecations
+ -fwarn-wrong-do-bind
-- These options will be removed in GHC 8.0.1.
- if impl(ghc >= 7.10) && impl(ghc < 8.0)
+ if impl(ghc < 8.0)
ghc-options: -fwarn-context-quantification
-fwarn-duplicate-constraints
-fwarn-pointless-pragmas
@@ -663,13 +664,12 @@ executable agda
-- except for the prelude.
, base >= 4.8.0.0 && < 6
default-language: Haskell2010
- if impl(ghc >= 7)
- -- If someone installs Agda with the setuid bit set, then the
- -- presence of +RTS may be a security problem (see GHC bug #3910).
- -- However, we sometimes recommend people to use +RTS to control
- -- Agda's memory usage, so we want this functionality enabled by
- -- default.
- ghc-options: -rtsopts
+ -- If someone installs Agda with the setuid bit set, then the
+ -- presence of +RTS may be a security problem (see GHC bug #3910).
+ -- However, we sometimes recommend people to use +RTS to control
+ -- Agda's memory usage, so we want this functionality enabled by
+ -- default.
+ ghc-options: -rtsopts
executable agda-mode
hs-source-dirs: src/agda-mode
diff --git a/CHANGELOG.md b/CHANGELOG.md
index c72a896..03ba878 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,3 +1,26 @@
+Release notes for Agda version 2.6.0.1
+======================================
+
+Installation and infrastructure
+-------------------------------
+
+* Added support for GHC 8.6.5.
+
+List of all closed issues
+-------------------------
+
+For 2.6.0.1, the following issues have been closed
+(see [bug tracker](https://github.com/agda/agda/issues)):
+
+ - [#3685](https://github.com/agda/agda/issues/3685): Support GHC 8.6.5
+ - [#3692](https://github.com/agda/agda/issues/3692): Omission of absurd patterns in automatically added absurd clauses causes too optimistic polarity.
+ - [#3694](https://github.com/agda/agda/issues/3694): Importing Agda.Builtin.Size in one module affects another module
+ - [#3696](https://github.com/agda/agda/issues/3696): Make `AgdaAny` polykinded?
+ - [#3697](https://github.com/agda/agda/issues/3697): Panic when checking non-Setω data definitions with --type-in-type
+ - [#3701](https://github.com/agda/agda/issues/3701): [ re agda/agda-stdlib#710 ] toNat for machine words is injective
+ - [#3731](https://github.com/agda/agda/issues/3731): GHC backend thinks that a constructor called 'main' is the main program
+ - [#3742](https://github.com/agda/agda/issues/3742): Strange error message for code that combines mutual and abstract
+
Release notes for Agda version 2.6.0
====================================
@@ -5,18 +28,18 @@ Highlights
----------
* Added support for [Cubical
- Agda](https://agda.readthedocs.io/en/latest/language/cubical.html)
+ Agda](https://agda.readthedocs.io/en/v2.6.0/language/cubical.html)
which adds new features such as univalence and higher inductive
types to Agda.
* Added support for ML-style [automatic generalization of
- variables](https://agda.readthedocs.io/en/latest/language/generalization-of-declared-variables.html).
+ variables](https://agda.readthedocs.io/en/v2.6.0/language/generalization-of-declared-variables.html).
* Added a new sort ``Prop`` of [definitionally proof-irrelevant
- propositions](https://agda.readthedocs.io/en/latest/language/prop.html).
+ propositions](https://agda.readthedocs.io/en/v2.6.0/language/prop.html).
* The implementation of [instance
- search](https://agda.readthedocs.io/en/latest/language/instance-arguments.html)
+ search](https://agda.readthedocs.io/en/v2.6.0/language/instance-arguments.html)
got a major overhaul and no longer supports overlapping instances
(unless enabled by a flag).
@@ -59,7 +82,7 @@ Syntax
-- _∘_ : {Γ Δ Θ : Con} → Sub Θ Δ → Sub Γ Θ → Sub Γ Δ
```
- See the [user manual](https://agda.readthedocs.io/en/latest/language/generalization-of-declared-variables.html)
+ See the [user manual](https://agda.readthedocs.io/en/v2.6.0/language/generalization-of-declared-variables.html)
for more details.
* Data type and record definitions separated from their type signatures can no
@@ -145,14 +168,14 @@ Type checking
univalence and higher inductive types. Option `--cubical` enables
the cubical mode, and cubical primitives are defined in the module
`Agda.Primitive.Cubical`. See the [user
- manual](https://agda.readthedocs.io/en/latest/language/cubical.html)
+ manual](https://agda.readthedocs.io/en/v2.6.0/language/cubical.html)
for more info.
* Agda now supports the new sort ``Prop`` of [definitionally
proof-irrelevant propositions](https://hal.inria.fr/hal-01859964).
Option `--prop` enables the `Prop` universe but is off by default.
Option `--no-prop` disables the `Prop` universe. See the [user
- manual](https://agda.readthedocs.io/en/latest/language/prop.html)
+ manual](https://agda.readthedocs.io/en/v2.6.0/language/prop.html)
for more details.
In the absense of `Prop`, the sort `Set` is the lowest sort, thus,
@@ -299,7 +322,6 @@ Instance search
Reflection
----------
-
* New TC primitive `noConstraints` [Issue
[#2351](https://github.com/agda/agda/issues/2351)]:
@@ -483,7 +505,7 @@ Pragmas and options
{-# COMPILED_JS f e #-}
```
- See the [user manual](https://agda.readthedocs.io/en/latest/language/foreign-function-interface.html)
+ See the [user manual](https://agda.readthedocs.io/en/v2.6.0/language/foreign-function-interface.html)
for how to use the `COMPILE` and `FOREIGN` pragmas that replaced these in Agda 2.5.
### New warnings
@@ -3194,7 +3216,7 @@ Language
```
This change fixes an inconsistency, see [Issue [#2169](https://github.com/agda/agda/issues/2169)].
- For further detail see the [user manual](http://agda.readthedocs.io/en/latest/language/built-ins.html#floats).
+ For further detail see the [user manual](http://agda.readthedocs.io/en/v2.5.2/language/built-ins.html#floats).
- Floats now have only one `NaN` value. This is necessary
for proper Float support in the JavaScript backend,
@@ -3850,7 +3872,7 @@ Documentation
-------------
* There is now an official Agda User Manual:
- http://agda.readthedocs.org/en/stable/
+ https://agda.readthedocs.io/
Installation and infrastructure
-------------------------------
diff --git a/Setup.hs b/Setup.hs
index a211e81..910c8fe 100644
--- a/Setup.hs
+++ b/Setup.hs
@@ -8,7 +8,7 @@ import Distribution.PackageDescription
-- ASR (2019-01-10): The Cabal macro @MIN_VERSION_Cabal@ is avaliable
-- from Cabal_>_1.24 so this macro is not supported with the
-- "standard" GHC 7.10.3 which is shipped with Cabal 1.22.5.0.
-#if __GLASGOW_HASKELL__ > 710
+#if __GLASGOW_HASKELL__ >= 800
#if MIN_VERSION_Cabal(2,3,0)
import Distribution.System ( buildPlatform )
#endif
@@ -84,7 +84,7 @@ agdaExeExtension :: String
-- ASR (2019-01-10): The Cabal macro @MIN_VERSION_Cabal@ is avaliable
-- from Cabal_>_1.24 so this macro is not supported with the
-- "standard" GHC 7.10.3 which is shipped with Cabal 1.22.5.0.
-#if __GLASGOW_HASKELL__ > 710
+#if __GLASGOW_HASKELL__ >= 800
#if MIN_VERSION_Cabal(2,3,0)
agdaExeExtension = exeExtension buildPlatform
#else
diff --git a/dist/build/Agda/Syntax/Parser/Parser.hs b/dist/build/Agda/Syntax/Parser/Parser.hs
index f7eef54..df53cae 100644
--- a/dist/build/Agda/Syntax/Parser/Parser.hs
+++ b/dist/build/Agda/Syntax/Parser/Parser.hs
@@ -7659,8 +7659,7 @@ errorConflictingAttributes as = parseErrorRange as $
{-# LINE 10 "<command-line>" #-}
-{-# LINE 1 "/usr/local/stow/ghc-8.6.5-rc1/lib/ghc-8.6.4.20190406/include/ghcversion.h" #-}
-
+{-# LINE 1 "/usr/local/stow/ghc-8.6.5/lib/ghc-8.6.5/include/ghcversion.h" #-}
@@ -7677,409 +7676,7 @@ errorConflictingAttributes as = parseErrorRange as $
{-# LINE 10 "<command-line>" #-}
-{-# LINE 1 "/tmp/ghc23210_0/ghc_2.h" #-}
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
+{-# LINE 1 "/tmp/ghc31894_0/ghc_2.h" #-}
diff --git a/doc/user-manual.pdf b/doc/user-manual.pdf
index 72a24e8..cc7df7e 100644
--- a/doc/user-manual.pdf
+++ b/doc/user-manual.pdf
Binary files differ
diff --git a/src/data/MAlonzo/src/MAlonzo/RTE.hs b/src/data/MAlonzo/src/MAlonzo/RTE.hs
index f775444..955f1e9 100644
--- a/src/data/MAlonzo/src/MAlonzo/RTE.hs
+++ b/src/data/MAlonzo/src/MAlonzo/RTE.hs
@@ -1,8 +1,10 @@
-{-# LANGUAGE CPP #-}
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE PolyKinds #-}
+
module MAlonzo.RTE where
import Unsafe.Coerce
-#if __GLASGOW_HASKELL__ >= 802
+#if __GLASGOW_HASKELL__ >= 800
import qualified GHC.Exts as GHC (Any)
#else
import qualified GHC.Prim as GHC (Any)
@@ -147,5 +149,5 @@ lt64 = (<)
-- Support for musical coinduction.
-data Inf a = Sharp { flat :: a }
-type Infinity level a = Inf a
+data Inf a = Sharp { flat :: a }
+type Infinity (level :: *) a = Inf a
diff --git a/src/data/emacs-mode/agda2-mode-pkg.el b/src/data/emacs-mode/agda2-mode-pkg.el
index d7aa224..6bfc66c 100644
--- a/src/data/emacs-mode/agda2-mode-pkg.el
+++ b/src/data/emacs-mode/agda2-mode-pkg.el
@@ -1,2 +1,2 @@
-(define-package "agda2-mode" "2.6.0"
+(define-package "agda2-mode" "2.6.0.1"
"interactive development for Agda, a dependently typed functional programming language")
diff --git a/src/data/emacs-mode/agda2-mode.el b/src/data/emacs-mode/agda2-mode.el
index aafdfa4..7172993 100644
--- a/src/data/emacs-mode/agda2-mode.el
+++ b/src/data/emacs-mode/agda2-mode.el
@@ -10,7 +10,7 @@
;;; Code:
-(defvar agda2-version "2.6.0"
+(defvar agda2-version "2.6.0.1"
"The version of the Agda mode.
Note that the same version of the Agda executable must be used.")
diff --git a/src/data/lib/prim/Agda/Builtin/Word/Properties.agda b/src/data/lib/prim/Agda/Builtin/Word/Properties.agda
new file mode 100644
index 0000000..365b4fd
--- /dev/null
+++ b/src/data/lib/prim/Agda/Builtin/Word/Properties.agda
@@ -0,0 +1,10 @@
+{-# OPTIONS --without-K --safe --no-sized-types --no-guardedness #-}
+
+module Agda.Builtin.Word.Properties where
+
+open import Agda.Builtin.Word
+open import Agda.Builtin.Equality
+
+primitive
+
+ primWord64ToNatInjective : ∀ a b → primWord64ToNat a ≡ primWord64ToNat b → a ≡ b
diff --git a/src/full/Agda/Compiler/Backend.hs b/src/full/Agda/Compiler/Backend.hs
index 542cc28..8957229 100644
--- a/src/full/Agda/Compiler/Backend.hs
+++ b/src/full/Agda/Compiler/Backend.hs
@@ -82,7 +82,7 @@ data Backend' opts env menv mod def = Backend'
-- required.
, postModule :: env -> menv -> IsMain -> ModuleName -> [def] -> TCM mod
-- ^ Called after all definitions of a module has been compiled.
- , compileDef :: env -> menv -> Definition -> TCM def
+ , compileDef :: env -> menv -> IsMain -> Definition -> TCM def
-- ^ Compile a single definition.
, scopeCheckingSuffices :: Bool
-- ^ True if the backend works if @--only-scope-checking@ is used.
@@ -201,8 +201,8 @@ compileModule backend env isMain i = do
Skip m -> return m
Recompile menv -> do
defs <- map snd . sortDefs <$> curDefs
- res <- mapM (compileDef' backend env menv <=< instantiateFull) defs
+ res <- mapM (compileDef' backend env menv isMain <=< instantiateFull) defs
postModule backend env menv isMain (iModuleName i) res
-compileDef' :: Backend' opts env menv mod def -> env -> menv -> Definition -> TCM def
-compileDef' backend env menv def = setCurrentRange (defName def) $ compileDef backend env menv def
+compileDef' :: Backend' opts env menv mod def -> env -> menv -> IsMain -> Definition -> TCM def
+compileDef' backend env menv isMain def = setCurrentRange (defName def) $ compileDef backend env menv isMain def
diff --git a/src/full/Agda/Compiler/Common.hs b/src/full/Agda/Compiler/Common.hs
index 4a75814..4dd2e85 100644
--- a/src/full/Agda/Compiler/Common.hs
+++ b/src/full/Agda/Compiler/Common.hs
@@ -44,6 +44,7 @@ import Agda.Utils.Impossible
data IsMain = IsMain | NotMain
deriving (Eq, Show)
+-- | Conjunctive semigroup ('NotMain' is absorbing).
instance Semigroup IsMain where
NotMain <> _ = NotMain
_ <> NotMain = NotMain
diff --git a/src/full/Agda/Compiler/JS/Compiler.hs b/src/full/Agda/Compiler/JS/Compiler.hs
index c591a46..ff3cf53 100644
--- a/src/full/Agda/Compiler/JS/Compiler.hs
+++ b/src/full/Agda/Compiler/JS/Compiler.hs
@@ -151,8 +151,8 @@ jsPostModule _ _ isMain _ defs = do
IsMain -> Just $ Apply (Lookup Self $ MemberId "main") [Lambda 1 emp]
NotMain -> Nothing
-jsCompileDef :: JSOptions -> JSModuleEnv -> Definition -> TCM (Maybe Export)
-jsCompileDef _ kit def = definition kit (defName def, def)
+jsCompileDef :: JSOptions -> JSModuleEnv -> IsMain -> Definition -> TCM (Maybe Export)
+jsCompileDef _ kit _isMain def = definition kit (defName def, def)
--------------------------------------------------
-- Naming
diff --git a/src/full/Agda/Compiler/MAlonzo/Compiler.hs b/src/full/Agda/Compiler/MAlonzo/Compiler.hs
index 698d2d8..07042e9 100644
--- a/src/full/Agda/Compiler/MAlonzo/Compiler.hs
+++ b/src/full/Agda/Compiler/MAlonzo/Compiler.hs
@@ -181,7 +181,7 @@ ghcPostModule _ _ _ _ defs = do
(map fakeDecl (hsImps ++ code) ++ concat defs)
hasMainFunction <$> curIF
-ghcCompileDef :: GHCOptions -> GHCModuleEnv -> Definition -> TCM [HS.Decl]
+ghcCompileDef :: GHCOptions -> GHCModuleEnv -> IsMain -> Definition -> TCM [HS.Decl]
ghcCompileDef _ = definition
-- Compilation ------------------------------------------------------------
@@ -224,16 +224,16 @@ imports = (hsImps ++) <$> imps where
-- Main compiling clauses
--------------------------------------------------
-definition :: GHCModuleEnv -> Definition -> TCM [HS.Decl]
+definition :: GHCModuleEnv -> IsMain -> Definition -> TCM [HS.Decl]
-- ignore irrelevant definitions
{- Andreas, 2012-10-02: Invariant no longer holds
definition kit (Defn NonStrict _ _ _ _ _ _ _ _) = __IMPOSSIBLE__
-}
-definition env Defn{defArgInfo = info, defName = q} | not $ usableModality info = do
+definition _env _isMain Defn{defArgInfo = info, defName = q} | not $ usableModality info = do
reportSDoc "compile.ghc.definition" 10 $
"Not compiling" <+> prettyTCM q <> "."
return []
-definition env Defn{defName = q, defType = ty, theDef = d} = do
+definition env isMain def@Defn{defName = q, defType = ty, theDef = d} = do
reportSDoc "compile.ghc.definition" 10 $ vcat
[ "Compiling" <+> prettyTCM q <> ":"
, nest 2 $ text (show d)
@@ -243,7 +243,7 @@ definition env Defn{defName = q, defType = ty, theDef = d} = do
mlist <- getBuiltinName builtinList
minf <- getBuiltinName builtinInf
mflat <- getBuiltinName builtinFlat
- checkTypeOfMain q ty $ do
+ checkTypeOfMain isMain q def $ do
infodecl q <$> case d of
_ | Just HsDefn{} <- pragma, Just q == mflat ->
@@ -314,12 +314,19 @@ definition env Defn{defName = q, defType = ty, theDef = d} = do
Function{} -> function pragma $ functionViaTreeless q
Datatype{ dataPars = np, dataIxs = ni, dataClause = cl, dataCons = cs }
- | Just (HsData r ty hsCons) <- pragma -> setCurrentRange r $ do
+ | Just hsdata@(HsData r ty hsCons) <- pragma -> setCurrentRange r $ do
+ reportSDoc "compile.ghc.definition" 40 $ hsep $
+ [ "Compiling data type with COMPILE pragma ...", pretty hsdata ]
computeErasedConstructorArgs q
ccscov <- constructorCoverageCode q (np + ni) cs ty hsCons
cds <- mapM compiledcondecl cs
- return $ tvaldecl q (dataInduction d) (np + ni) [] (Just __IMPOSSIBLE__) ++
- [compiledTypeSynonym q ty np] ++ cds ++ ccscov
+ let result = concat $
+ [ tvaldecl q (dataInduction d) (np + ni) [] (Just __IMPOSSIBLE__)
+ , [ compiledTypeSynonym q ty np ]
+ , cds
+ , ccscov
+ ]
+ return result
Datatype{ dataPars = np, dataIxs = ni, dataClause = cl,
dataCons = cs, dataInduction = ind } -> do
computeErasedConstructorArgs q
diff --git a/src/full/Agda/Compiler/MAlonzo/Pragmas.hs b/src/full/Agda/Compiler/MAlonzo/Pragmas.hs
index 8395ca9..05ec807 100644
--- a/src/full/Agda/Compiler/MAlonzo/Pragmas.hs
+++ b/src/full/Agda/Compiler/MAlonzo/Pragmas.hs
@@ -47,6 +47,16 @@ instance HasRange HaskellPragma where
getRange (HsData r _ _) = r
getRange (HsExport r _) = r
+instance Pretty HaskellPragma where
+ pretty = \case
+ HsDefn _r hsCode -> equals <+> text hsCode
+ HsType _r hsType -> equals <+> text hsType
+ HsData _r hsType hsCons -> hsep $
+ [ equals, "data", text hsType
+ , parens $ hsep $ map text $ List.intersperse "|" hsCons
+ ]
+ HsExport _r hsCode -> "as" <+> text hsCode
+
-- Syntax for Haskell pragmas:
-- HsDefn CODE "= CODE"
-- HsType TYPE "= type TYPE"
diff --git a/src/full/Agda/Compiler/MAlonzo/Primitives.hs b/src/full/Agda/Compiler/MAlonzo/Primitives.hs
index f3a5b64..e7ecc07 100644
--- a/src/full/Agda/Compiler/MAlonzo/Primitives.hs
+++ b/src/full/Agda/Compiler/MAlonzo/Primitives.hs
@@ -5,7 +5,7 @@ module Agda.Compiler.MAlonzo.Primitives where
import Control.Monad.State
import Data.Char
import qualified Data.List as List
-import Data.Map as M
+import qualified Data.Map as Map
import Data.Maybe
import Agda.Compiler.Common
@@ -26,29 +26,46 @@ import Agda.Utils.Either
import Agda.Utils.Except
import Agda.Utils.Lens
import Agda.Utils.Monad
+import Agda.Utils.Pretty (prettyShow)
import qualified Agda.Utils.HashMap as HMap
import qualified Agda.Utils.Haskell.Syntax as HS
#include "undefined.h"
import Agda.Utils.Impossible
-isMainFunction :: QName -> Bool
-isMainFunction q = "main" == show (nameConcrete $ qnameName q)
+-- Andreas, 2019-04-29, issue #3731: exclude certain kinds of names, like constructors.
+-- TODO: Also only consider top-level definition (not buried inside a module).
+isMainFunction :: QName -> Defn -> Bool
+isMainFunction q = \case
+ Axiom{} -> perhaps
+ Function{ funProjection = Nothing } -> perhaps
+ Function{ funProjection = Just{} } -> no
+ AbstractDefn{} -> no
+ GeneralizableVar{} -> no
+ DataOrRecSig{} -> no
+ Datatype{} -> no
+ Record{} -> no
+ Constructor{} -> no
+ Primitive{} -> no
+ where
+ perhaps = "main" == prettyShow (nameConcrete $ qnameName q) -- ignores the qualification!?
+ no = False
hasMainFunction :: Interface -> IsMain
hasMainFunction i
- | List.any isMainFunction names = IsMain
- | otherwise = NotMain
+ | List.any (\ (x, def) -> isMainFunction x $ theDef def) names = IsMain
+ | otherwise = NotMain
where
- names = HMap.keys $ iSignature i ^. sigDefinitions
+ names = HMap.toList $ iSignature i ^. sigDefinitions
-- | Check that the main function has type IO a, for some a.
-checkTypeOfMain :: QName -> Type -> TCM [HS.Decl] -> TCM [HS.Decl]
-checkTypeOfMain q ty ret
- | not (isMainFunction q) = ret
+checkTypeOfMain :: IsMain -> QName -> Definition -> TCM [HS.Decl] -> TCM [HS.Decl]
+checkTypeOfMain NotMain q def ret = ret
+checkTypeOfMain IsMain q def ret
+ | not (isMainFunction q $ theDef def) = ret
| otherwise = do
Def io _ <- primIO
- ty <- normalise ty
+ ty <- normalise $ defType def
case unEl ty of
Def d _ | d == io -> (mainAlias :) <$> ret
_ -> do
@@ -115,7 +132,7 @@ importsForPrim =
xForPrim :: [(String, TCM [a])] -> TCM [a]
xForPrim table = do
qs <- HMap.keys <$> curDefs
- bs <- toList <$> getsTC stBuiltinThings
+ bs <- Map.toList <$> getsTC stBuiltinThings
let getName (Builtin (Def q _)) = q
getName (Builtin (Con q _ _)) = conName q
getName (Builtin (Lam _ b)) = getName (Builtin $ unAbs b)
@@ -162,6 +179,7 @@ primBody s = maybe unimplemented (fromRight (hsVarUQ . HS.Ident) <$>) $
-- Machine word functions
, "primWord64ToNat" |-> return "MAlonzo.RTE.word64ToNat"
, "primWord64FromNat" |-> return "MAlonzo.RTE.word64FromNat"
+ , "primWord64ToNatInjective" |-> return "erased"
-- Floating point functions
, "primNatToFloat" |-> return "(fromIntegral :: Integer -> Double)"
diff --git a/src/full/Agda/Interaction/BasicOps.hs b/src/full/Agda/Interaction/BasicOps.hs
index 8080eb1..ddcd6e3 100644
--- a/src/full/Agda/Interaction/BasicOps.hs
+++ b/src/full/Agda/Interaction/BasicOps.hs
@@ -551,8 +551,11 @@ instance (ToConcrete a c, ToConcrete b d) =>
toConcrete (OfType' e t) = OfType' <$> toConcrete e <*> toConcreteCtx TopCtx t
getConstraints :: TCM [OutputForm C.Expr C.Expr]
-getConstraints = liftTCM $ do
- cs <- M.getAllConstraints
+getConstraints = getConstraints' $ const True
+
+getConstraints' :: (ProblemConstraint -> Bool) -> TCM [OutputForm C.Expr C.Expr]
+getConstraints' f = liftTCM $ do
+ cs <- filter f <$> M.getAllConstraints
cs <- forM cs $ \c -> do
cl <- reify c
enterClosure cl abstractToConcrete_
diff --git a/src/full/Agda/Interaction/Highlighting/Generate.hs b/src/full/Agda/Interaction/Highlighting/Generate.hs
index c5d2644..cfae19c 100644
--- a/src/full/Agda/Interaction/Highlighting/Generate.hs
+++ b/src/full/Agda/Interaction/Highlighting/Generate.hs
@@ -665,8 +665,19 @@ warningHighlighting w = case tcWarning w of
UselessAbstract{} -> deadcodeHighlighting $ P.getRange w
UselessInstance{} -> deadcodeHighlighting $ P.getRange w
UselessPrivate{} -> deadcodeHighlighting $ P.getRange w
- _ -> mempty -- TODO: explore highlighting opportunities here!
-
+ -- TODO: explore highlighting opportunities here!
+ EmptyPrimitive{} -> mempty
+ InvalidCatchallPragma{} -> mempty
+ InvalidNoPositivityCheckPragma{} -> mempty
+ InvalidNoUniverseCheckPragma{} -> mempty
+ InvalidTerminationCheckPragma{} -> mempty
+ MissingDefinitions{} -> mempty
+ PolarityPragmasButNotPostulates{} -> mempty
+ PragmaNoTerminationCheck{} -> mempty
+ PragmaCompiled{} -> mempty
+ UnknownFixityInMixfixDecl{} -> mempty
+ UnknownNamesInFixityDecl{} -> mempty
+ UnknownNamesInPolarityPragmas{} -> mempty
-- | Generate syntax highlighting for termination errors.
diff --git a/src/full/Agda/Interaction/InteractionTop.hs b/src/full/Agda/Interaction/InteractionTop.hs
index 49dd7cb..92b2bc1 100644
--- a/src/full/Agda/Interaction/InteractionTop.hs
+++ b/src/full/Agda/Interaction/InteractionTop.hs
@@ -42,6 +42,7 @@ import qualified Agda.TypeChecking.Monad as TM
import qualified Agda.TypeChecking.Pretty as TCP
import Agda.TypeChecking.Rules.Term (checkExpr, isType_)
import Agda.TypeChecking.Errors
+import Agda.TypeChecking.MetaVars.Mention
import Agda.Syntax.Fixity
import Agda.Syntax.Position
@@ -1485,12 +1486,18 @@ cmd_goal_type_context_and doc norm ii _ _ = display_info . Info_GoalType =<< do
lift $ do
goal <- B.withInteractionId ii $ prettyTypeOfMeta norm ii
ctx <- prettyContext norm True ii
- return $ vcat
+ m <- lookupInteractionId ii
+ constr <- vcat . map pretty <$> B.getConstraints' (mentionsMeta m)
+ let constrDoc = ifNull constr [] $ \constr ->
+ [ text $ delimiter "Constraints"
+ , constr
+ ]
+ return $ vcat $
[ "Goal:" <+> goal
, doc
, text (replicate 60 '\x2014')
, ctx
- ]
+ ] ++ constrDoc
-- | Shows all the top-level names in the given module, along with
-- their types.
diff --git a/src/full/Agda/Interaction/Options/Lenses.hs b/src/full/Agda/Interaction/Options/Lenses.hs
index 353dda9..dd3daf5 100644
--- a/src/full/Agda/Interaction/Options/Lenses.hs
+++ b/src/full/Agda/Interaction/Options/Lenses.hs
@@ -167,6 +167,7 @@ builtinModulesWithSafePostulates =
, "Agda" </> "Builtin" </> "String" </> "Properties.agda"
, "Agda" </> "Builtin" </> "Unit.agda"
, "Agda" </> "Builtin" </> "Word.agda"
+ , "Agda" </> "Builtin" </> "Word" </> "Properties.agda"
])
-- | These builtins may not use postulates under --safe. They are not
diff --git a/src/full/Agda/Syntax/Internal.hs b/src/full/Agda/Syntax/Internal.hs
index 13276fe..f4788d3 100644
--- a/src/full/Agda/Syntax/Internal.hs
+++ b/src/full/Agda/Syntax/Internal.hs
@@ -489,6 +489,10 @@ namedVarP x = Named named $ varP x
namedDBVarP :: Int -> PatVarName -> Named_ DeBruijnPattern
namedDBVarP m = (fmap . fmap) (\x -> DBPatVar x m) . namedVarP
+-- | Make an absurd pattern with the given de Bruijn index.
+absurdP :: Int -> DeBruijnPattern
+absurdP = VarP PatOAbsurd . DBPatVar absurdPatternName
+
-- | The @ConPatternInfo@ states whether the constructor belongs to
-- a record type (@Just@) or data type (@Nothing@).
-- In the former case, the @PatOrigin@ says whether the record pattern
@@ -859,7 +863,7 @@ telFromList :: ListTel -> Telescope
telFromList = telFromList' id
-- | Convert a telescope to its list form.
-telToList :: Telescope -> ListTel
+telToList :: Tele (Dom t) -> [Dom (ArgName,t)]
telToList EmptyTel = []
telToList (ExtendTel arg (Abs x tel)) = fmap (x,) arg : telToList tel
telToList (ExtendTel _ NoAbs{} ) = __IMPOSSIBLE__
diff --git a/src/full/Agda/TypeChecking/Conversion.hs b/src/full/Agda/TypeChecking/Conversion.hs
index d21ace6..48c7e85 100644
--- a/src/full/Agda/TypeChecking/Conversion.hs
+++ b/src/full/Agda/TypeChecking/Conversion.hs
@@ -12,10 +12,6 @@ import qualified Data.Map as Map
import qualified Data.Set as Set
import qualified Data.IntSet as IntSet
-#if __GLASGOW_HASKELL__ <= 708
-import Data.Traversable ( traverse )
-#endif
-
import Agda.Syntax.Abstract.Views (isSet)
import Agda.Syntax.Common
import Agda.Syntax.Internal
@@ -1459,9 +1455,9 @@ equalLevel' a b = do
hasMeta ClosedLevel{} = False
hasMeta (Plus _ MetaLevel{}) = True
- hasMeta (Plus _ (BlockedLevel _ v)) = not $ null $ allMetas v
- hasMeta (Plus _ (NeutralLevel _ v)) = not $ null $ allMetas v
- hasMeta (Plus _ (UnreducedLevel v)) = not $ null $ allMetas v
+ hasMeta (Plus _ (BlockedLevel _ v)) = isJust $ firstMeta v
+ hasMeta (Plus _ (NeutralLevel _ v)) = isJust $ firstMeta v
+ hasMeta (Plus _ (UnreducedLevel v)) = isJust $ firstMeta v
isThisMeta x (Plus _ (MetaLevel y _)) = x == y
isThisMeta _ _ = False
diff --git a/src/full/Agda/TypeChecking/Coverage.hs b/src/full/Agda/TypeChecking/Coverage.hs
index e7398c9..5b25db1 100644
--- a/src/full/Agda/TypeChecking/Coverage.hs
+++ b/src/full/Agda/TypeChecking/Coverage.hs
@@ -55,7 +55,7 @@ import Agda.TypeChecking.Coverage.SplitTree
import Agda.TypeChecking.Conversion (tryConversion, equalType, equalTermOnFace)
import Agda.TypeChecking.Datatypes (getConForm)
-import {-# SOURCE #-} Agda.TypeChecking.Empty ( isEmptyTel, isEmptyType )
+import {-# SOURCE #-} Agda.TypeChecking.Empty ( checkEmptyTel, isEmptyTel, isEmptyType )
import Agda.TypeChecking.Free
import Agda.TypeChecking.Irrelevance
import Agda.TypeChecking.Patterns.Internal (dotPatternsToPatterns)
@@ -225,13 +225,21 @@ coverageCheck f t cs = do
-- filter out the missing clauses that are absurd.
pss <- flip filterM pss $ \(tel,ps) ->
- ifNotM (isEmptyTel tel) (return True) $ do
+ -- Andreas, 2019-04-13, issue #3692: when adding missing absurd
+ -- clauses, also put the absurd pattern in.
+ caseEitherM (checkEmptyTel noRange tel) (\ _ -> return True) $ \ l -> do
+ -- Now, @l@ is the first type in @tel@ (counting from 0=leftmost)
+ -- which is empty. Turn it into a de Bruijn index @i@.
+ let i = size tel - 1 - l
+ -- Build a substitution mapping this pattern variable to the absurd pattern.
+ let sub = inplaceS i $ absurdP i
+ -- ifNotM (isEmptyTel tel) (return True) $ do
-- Jesper, 2018-11-28, Issue #3407: if the clause is absurd,
-- add the appropriate absurd clause to the definition.
let cl = Clause { clauseLHSRange = noRange
, clauseFullRange = noRange
, clauseTel = tel
- , namedClausePats = ps
+ , namedClausePats = applySubst sub ps
, clauseBody = Nothing
, clauseType = Nothing
, clauseCatchall = False
@@ -241,6 +249,11 @@ coverageCheck f t cs = do
sep [ "adding missing absurd clause"
, nest 2 $ prettyTCM $ QNamed f cl
]
+ reportSDoc "tc.cover.missing" 80 $ inTopContext $ vcat
+ [ "l = " <+> pretty l
+ , "i = " <+> pretty i
+ , "cl = " <+> pretty (QNamed f cl)
+ ]
addClauses f [cl]
return False
diff --git a/src/full/Agda/TypeChecking/Empty.hs b/src/full/Agda/TypeChecking/Empty.hs
index 9527f16..1e0392c 100644
--- a/src/full/Agda/TypeChecking/Empty.hs
+++ b/src/full/Agda/TypeChecking/Empty.hs
@@ -1,9 +1,5 @@
-module Agda.TypeChecking.Empty
- ( isEmptyType
- , isEmptyTel
- , ensureEmptyType
- ) where
+module Agda.TypeChecking.Empty where
import Control.Monad.Except
@@ -94,11 +90,15 @@ checkEmptyType range t = do
-- If t is a record type, see if any of the field types is empty
Right (r, pars, def) -> do
if recEtaEquality def == NoEta then return $ Left Fail else do
- checkEmptyTel range $ recTel def `apply` pars
-
-checkEmptyTel :: Range -> Telescope -> TCM (Either ErrorNonEmpty ())
-checkEmptyTel r EmptyTel = return $ Left Fail
-checkEmptyTel r (ExtendTel dom tel) = orEitherM
- [ checkEmptyType r (unDom dom)
- , underAbstraction dom tel (checkEmptyTel r)
- ]
+ void <$> do checkEmptyTel range $ recTel def `apply` pars
+
+-- | Check whether one of the types in the given telescope is constructor-less
+-- and if yes, return its index in the telescope (0 = leftmost).
+checkEmptyTel :: Range -> Telescope -> TCM (Either ErrorNonEmpty Int)
+checkEmptyTel r = loop 0
+ where
+ loop i EmptyTel = return $ Left Fail
+ loop i (ExtendTel dom tel) = orEitherM
+ [ (i <$) <$> checkEmptyType r (unDom dom)
+ , underAbstraction dom tel $ loop (succ i)
+ ]
diff --git a/src/full/Agda/TypeChecking/Empty.hs-boot b/src/full/Agda/TypeChecking/Empty.hs-boot
index 8234bb7..d82cde1 100644
--- a/src/full/Agda/TypeChecking/Empty.hs-boot
+++ b/src/full/Agda/TypeChecking/Empty.hs-boot
@@ -5,7 +5,10 @@ import Agda.TypeChecking.Monad (TCM)
import Agda.Syntax.Internal (Type, Telescope)
import Agda.Syntax.Position (Range)
+data ErrorNonEmpty
+
isEmptyType :: Type -> TCM Bool
isEmptyTel :: Telescope -> TCM Bool
ensureEmptyType :: Range -> Type -> TCM ()
+checkEmptyTel :: Range -> Telescope -> TCM (Either ErrorNonEmpty Int)
diff --git a/src/full/Agda/TypeChecking/Errors.hs b/src/full/Agda/TypeChecking/Errors.hs
index c9e92e3..7db3aa7 100644
--- a/src/full/Agda/TypeChecking/Errors.hs
+++ b/src/full/Agda/TypeChecking/Errors.hs
@@ -452,7 +452,6 @@ errorString err = case err of
ShouldEndInApplicationOfTheDatatype{} -> "ShouldEndInApplicationOfTheDatatype"
SplitError{} -> "SplitError"
ImpossibleConstructor{} -> "ImpossibleConstructor"
- TooFewFields{} -> "TooFewFields"
TooManyFields{} -> "TooManyFields"
TooManyPolarities{} -> "TooManyPolarities"
SplitOnIrrelevant{} -> "SplitOnIrrelevant"
@@ -797,13 +796,11 @@ instance PrettyTCM TypeError where
NotLeqSort s1 s2 -> fsep $
[prettyTCM s1] ++ pwords "is not less or equal than" ++ [prettyTCM s2]
- TooFewFields r xs -> fsep $
- pwords "Missing fields" ++ punctuate comma (map pretty xs) ++
- pwords "in an element of the record" ++ [prettyTCM r]
-
- TooManyFields r xs -> fsep $
+ TooManyFields r missing xs -> fsep $
pwords "The record type" ++ [prettyTCM r] ++
- pwords "does not have the fields" ++ punctuate comma (map pretty xs)
+ pwords "does not have the fields" ++ punctuate comma (map pretty xs) ++
+ if null missing then [] else
+ pwords "but it would have the fields" ++ punctuate comma (map pretty missing)
DuplicateConstructors xs -> fsep $
pwords "Duplicate constructors" ++ punctuate comma (map pretty xs) ++
diff --git a/src/full/Agda/TypeChecking/Generalize.hs b/src/full/Agda/TypeChecking/Generalize.hs
index 8604e5b..0efdeb5 100644
--- a/src/full/Agda/TypeChecking/Generalize.hs
+++ b/src/full/Agda/TypeChecking/Generalize.hs
@@ -14,6 +14,7 @@ import qualified Data.Set as Set
import Data.Map (Map)
import qualified Data.Map as Map
import Data.List (nub, partition, init, sortBy)
+import Data.Monoid
import Data.Function (on)
import Data.Traversable
@@ -48,6 +49,7 @@ import Agda.Utils.Lens
import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Utils.Size
+import Agda.Utils.Singleton
import Agda.Utils.Permutation
import qualified Agda.Utils.Graph.TopSort as Graph
@@ -212,7 +214,7 @@ computeGeneralization genRecMeta nameMap allmetas = postponeInstanceConstraints
case mvInstantiation mv of
InstV _ v -> do
parentName <- getMetaNameSuggestion x
- metas <- filterM canGeneralize . allMetas =<< instantiateFull v
+ metas <- filterM canGeneralize . allMetasList =<< instantiateFull v
let suggestNames i [] = return ()
suggestNames i (m : ms) = do
name <- getMetaNameSuggestion m
@@ -546,7 +548,7 @@ pruneUnsolvedMetas genRecName genRecCon genTel genRecFields interactionPoints is
_ -> err
telList = telToList genTel
names = map (fst . unDom) telList
- late = map (fst . unDom) $ filter (elem x . allMetas) telList
+ late = map (fst . unDom) $ filter (getAny . allMetas (Any . (== x))) telList
projs (Proj _ q)
| elem q genRecFields = Set.fromList [x | Just x <- [getGeneralizedFieldName q]]
projs _ = Set.empty
@@ -691,9 +693,10 @@ createGenValue x = setCurrentRange x $ do
-- | Sort metas in dependency order.
sortMetas :: [MetaId] -> TCM [MetaId]
sortMetas metas = do
- metaGraph <- fmap concat $ forM metas $ \ m -> do
- deps <- nub . filter (`elem` metas) . allMetas <$> getType m
- return [ (m, m') | m' <- deps ]
+ metaGraph <- concat <$> do
+ forM metas $ \ m -> do
+ deps <- allMetas (\ m' -> if m' `elem` metas then singleton m' else mempty) <$> getType m
+ return [ (m, m') | m' <- Set.toList deps ]
caseMaybe (Graph.topSort metas metaGraph)
(typeError GeneralizeCyclicDependency)
@@ -804,4 +807,3 @@ fillInGenRecordDetails name con fields recTy fieldTel = do
r { theDef = (theDef r) { recTel = fullTel } }
where
setType q ty = modifyGlobalDefinition q $ \ d -> d { defType = ty }
-
diff --git a/src/full/Agda/TypeChecking/IApplyConfluence.hs b/src/full/Agda/TypeChecking/IApplyConfluence.hs
index e1754b6..de8df6c 100644
--- a/src/full/Agda/TypeChecking/IApplyConfluence.hs
+++ b/src/full/Agda/TypeChecking/IApplyConfluence.hs
@@ -30,30 +30,13 @@ import Agda.TypeChecking.Primitive hiding (Nat)
import Agda.TypeChecking.Primitive.Cubical
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Monad.Builtin
-
--- import Agda.TypeChecking.Rules.LHS (checkSortOfSplitVar)
--- import Agda.TypeChecking.Rules.LHS.Problem (allFlexVars)
--- import Agda.TypeChecking.Rules.LHS.Unify
-
--- import Agda.TypeChecking.Coverage.Match
--- import Agda.TypeChecking.Coverage.SplitTree
-
import Agda.TypeChecking.Conversion (tryConversion, equalType, equalTermOnFace)
--- import Agda.TypeChecking.Datatypes (getConForm)
--- import {-# SOURCE #-} Agda.TypeChecking.Empty (isEmptyTel)
--- import Agda.TypeChecking.Free
--- import Agda.TypeChecking.Irrelevance
--- import Agda.TypeChecking.Patterns.Internal (dotPatternsToPatterns)
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Records
import Agda.TypeChecking.Telescope
import Agda.TypeChecking.Telescope.Path
--- import Agda.TypeChecking.MetaVars
--- import Agda.TypeChecking.Warnings
-
--- import Agda.Interaction.Options
import Agda.Utils.Either
import Agda.Utils.Except
diff --git a/src/full/Agda/TypeChecking/InstanceArguments.hs b/src/full/Agda/TypeChecking/InstanceArguments.hs
index 8b186bf..39a7f15 100644
--- a/src/full/Agda/TypeChecking/InstanceArguments.hs
+++ b/src/full/Agda/TypeChecking/InstanceArguments.hs
@@ -20,6 +20,7 @@ import qualified Data.Map as Map
import qualified Data.Set as Set
import qualified Data.List as List
import Data.Function (on)
+import Data.Monoid hiding ((<>))
import Agda.Interaction.Options (optOverlappingInstances)
@@ -342,7 +343,7 @@ dropSameCandidates :: MetaId -> [(Candidate, Term, Type, a)] -> TCM [(Candidate,
dropSameCandidates m cands0 = verboseBracket "tc.instance" 30 "dropSameCandidates" $ do
metas <- getMetaVariableSet
-- Does `it` have any metas in the initial meta variable store?
- let freshMetas = any ((`IntSet.notMember` metas) . metaId) . allMetas
+ let freshMetas = getAny . allMetas (Any . (`IntSet.notMember` metas) . metaId)
-- Take overlappable candidates into account
let cands =
diff --git a/src/full/Agda/TypeChecking/MetaVars/Occurs.hs b/src/full/Agda/TypeChecking/MetaVars/Occurs.hs
index 314403e..06624e8 100644
--- a/src/full/Agda/TypeChecking/MetaVars/Occurs.hs
+++ b/src/full/Agda/TypeChecking/MetaVars/Occurs.hs
@@ -366,7 +366,14 @@ instance Occurs QName where
metaOccurs m d = whenM (defNeedsChecking d) $ do
tallyDef d
reportSLn "tc.meta.occurs" 30 $ "Checking for occurrences in " ++ show d
- metaOccurs m . theDef =<< ignoreAbstractMode (getConstInfo d)
+ metaOccursQName m d
+
+metaOccursQName :: MetaId -> QName -> TCM ()
+metaOccursQName m x = metaOccurs m . theDef =<< do
+ ignoreAbstractMode $ getConstInfo x
+ -- Andreas, 2019-05-03, issue #3742:
+ -- ignoreAbstractMode necessary, as abstract
+ -- constructors are also called up.
instance Occurs Defn where
occurs red ctx m xs def = __IMPOSSIBLE__
@@ -376,9 +383,8 @@ instance Occurs Defn where
metaOccurs m Function{ funClauses = cls } = metaOccurs m cls
-- since a datatype is isomorphic to the sum of its constructor types
-- we check the constructor types
- metaOccurs m Datatype{ dataCons = cs } = mapM_ mocc cs
- where mocc c = metaOccurs m . defType =<< getConstInfo c
- metaOccurs m Record{ recConHead = c } = metaOccurs m . defType =<< getConstInfo (conName c)
+ metaOccurs m Datatype{ dataCons = cs } = mapM_ (metaOccursQName m) cs
+ metaOccurs m Record{ recConHead = c } = metaOccursQName m $ conName c
metaOccurs m Constructor{} = return ()
metaOccurs m Primitive{} = return ()
metaOccurs m AbstractDefn{} = __IMPOSSIBLE__
diff --git a/src/full/Agda/TypeChecking/Monad/Base.hs b/src/full/Agda/TypeChecking/Monad/Base.hs
index 8066c05..ceb222f 100644
--- a/src/full/Agda/TypeChecking/Monad/Base.hs
+++ b/src/full/Agda/TypeChecking/Monad/Base.hs
@@ -3046,8 +3046,8 @@ data TypeError
| BuiltinInParameterisedModule String
| IllegalLetInTelescope C.TypedBinding
| NoRHSRequiresAbsurdPattern [NamedArg A.Pattern]
- | TooFewFields QName [C.Name]
- | TooManyFields QName [C.Name]
+ | TooManyFields QName [C.Name] [C.Name]
+ -- ^ Record type, fields not supplied by user, non-fields not supplied.
| DuplicateFields [C.Name]
| DuplicateConstructors [C.Name]
| WithOnFreeVariable A.Expr Term
@@ -3612,7 +3612,7 @@ instance MonadIO m => Monad (TCMT m) where
return = pure
(>>=) = bindTCMT
(>>) = (*>)
-#if __GLASGOW_HASKELL__ == 710
+#if __GLASGOW_HASKELL__ < 800
fail = internalError
#else
fail = Fail.fail
diff --git a/src/full/Agda/TypeChecking/Monad/Builtin.hs b/src/full/Agda/TypeChecking/Monad/Builtin.hs
index 9db01f9..d9e8682 100644
--- a/src/full/Agda/TypeChecking/Monad/Builtin.hs
+++ b/src/full/Agda/TypeChecking/Monad/Builtin.hs
@@ -35,7 +35,7 @@ import Agda.Utils.Impossible
class ( Functor m
, Applicative m
-#if __GLASGOW_HASKELL__ == 710
+#if __GLASGOW_HASKELL__ < 800
, Monad m
#else
, Fail.MonadFail m
diff --git a/src/full/Agda/TypeChecking/Monad/MetaVars.hs b/src/full/Agda/TypeChecking/Monad/MetaVars.hs
index 4d97150..5db93a6 100644
--- a/src/full/Agda/TypeChecking/Monad/MetaVars.hs
+++ b/src/full/Agda/TypeChecking/Monad/MetaVars.hs
@@ -19,6 +19,7 @@ import qualified Data.Map as Map
import Data.Set (Set)
import qualified Data.Set as Set
import qualified Data.Foldable as Fold
+import Data.Monoid
import Agda.Syntax.Common
import Agda.Syntax.Internal
@@ -43,6 +44,7 @@ import Agda.Utils.Null
import Agda.Utils.Permutation
import Agda.Utils.Pretty (prettyShow)
import Agda.Utils.Tuple
+import Agda.Utils.Singleton
import Agda.Utils.Size
import qualified Agda.Utils.Maybe.Strict as Strict
@@ -172,33 +174,67 @@ isInstantiatedMeta' m = do
-- | Returns every meta-variable occurrence in the given type, except
-- for those in 'Sort's.
-allMetas :: TermLike a => a -> [MetaId]
-allMetas = foldTerm metas
+allMetas :: (TermLike a, Monoid m) => (MetaId -> m) -> a -> m
+allMetas singl = foldTerm metas
where
- metas (MetaV m _) = [m]
+ metas (MetaV m _) = singl m
metas (Level l) = levelMetas l
- metas _ = []
+ metas _ = mempty
- levelMetas (Max as) = concatMap plusLevelMetas as
+ levelMetas (Max as) = foldMap plusLevelMetas as
- plusLevelMetas ClosedLevel{} = []
+ plusLevelMetas ClosedLevel{} = mempty
plusLevelMetas (Plus _ l) = levelAtomMetas l
- levelAtomMetas (MetaLevel m _) = [m]
- levelAtomMetas _ = []
+ levelAtomMetas (MetaLevel m _) = singl m
+ levelAtomMetas _ = mempty
+
+-- | Returns 'allMetas' in a list.
+-- @allMetasList = allMetas (:[])@.
+--
+-- Note: this resulting list is computed via difference lists.
+-- Thus, use this function if you actually need the whole list of metas.
+-- Otherwise, use 'allMetas' with a suitable monoid.
+allMetasList :: TermLike a => a -> [MetaId]
+allMetasList t = allMetas singleton t `appEndo` []
+
+-- | 'True' if thing contains no metas.
+-- @noMetas = null . allMetasList@.
+noMetas :: TermLike a => a -> Bool
+noMetas = getAll . allMetas (\ _m -> All False)
+
+-- | Returns the first meta it find in the thing, if any.
+-- @firstMeta == headMaybe . allMetasList@.
+firstMeta :: TermLike a => a -> Maybe MetaId
+firstMeta = getFirst . allMetas (First . Just)
-- | Returns all metavariables in a constraint. Slightly complicated by the
-- fact that blocked terms are represented by two meta variables. To find the
-- second one we need to look up the meta listeners for the one in the
-- UnBlock constraint.
constraintMetas :: Constraint -> TCM (Set MetaId)
-constraintMetas c = Set.union (Set.fromList $ allMetas c) <$> metas c
+constraintMetas c = metas c
where
- -- Dig out constraint-specific meta vars
- metas (UnBlock x) = Set.insert x . Set.unions <$> (mapM listenerMetas =<< getMetaListeners x)
- metas (Guarded c _) = metas c
- metas (UnquoteTactic (Just x) _ _ _) = return $ Set.singleton x
- metas _ = return Set.empty
+ -- We don't use allMetas here since some constraints should not stop us from generalizing. For
+ -- instance CheckSizeLtSat (see #3694). We also have to check meta listeners to get metas of
+ -- UnBlock constraints.
+ metas c = case c of
+ ValueCmp _ t u v -> return $ allMetas Set.singleton (t, u, v)
+ ValueCmpOnFace _ p t u v -> return $ allMetas Set.singleton (p, t, u, v)
+ ElimCmp _ _ t u es es' -> return $ allMetas Set.singleton (t, u, es, es')
+ TypeCmp _ t t' -> return $ allMetas Set.singleton (t, t')
+ LevelCmp _ l l' -> return $ allMetas Set.singleton (l, l')
+ UnquoteTactic m t h g -> return $ Set.fromList [x | Just x <- [m]] `Set.union` allMetas Set.singleton (t, h, g)
+ Guarded c _ -> metas c
+ TelCmp _ _ _ tel1 tel2 -> return $ allMetas Set.singleton (tel1, tel2)
+ SortCmp _ s1 s2 -> return $ allMetas Set.singleton (s1, s2)
+ UnBlock x -> Set.insert x . Set.unions <$> (mapM listenerMetas =<< getMetaListeners x)
+ FindInstance{} -> return mempty -- v Ignore these constraints
+ IsEmpty{} -> return mempty
+ CheckFunDef{} -> return mempty
+ CheckSizeLtSat{} -> return mempty
+ HasBiggerSort{} -> return mempty
+ HasPTSRule{} -> return mempty
-- For blocked constant twin variables
listenerMetas EtaExpand{} = return Set.empty
diff --git a/src/full/Agda/TypeChecking/Monad/Signature.hs b/src/full/Agda/TypeChecking/Monad/Signature.hs
index 4bf3499..556fd4d 100644
--- a/src/full/Agda/TypeChecking/Monad/Signature.hs
+++ b/src/full/Agda/TypeChecking/Monad/Signature.hs
@@ -636,7 +636,7 @@ sigError f a = \case
class ( Functor m
, Applicative m
-#if __GLASGOW_HASKELL__ == 710
+#if __GLASGOW_HASKELL__ < 800
, Monad m
#else
, Fail.MonadFail m
diff --git a/src/full/Agda/TypeChecking/Monad/Signature.hs-boot b/src/full/Agda/TypeChecking/Monad/Signature.hs-boot
index 143ad1f..3abe29a 100644
--- a/src/full/Agda/TypeChecking/Monad/Signature.hs-boot
+++ b/src/full/Agda/TypeChecking/Monad/Signature.hs-boot
@@ -23,7 +23,7 @@ data SigError = SigUnknown String | SigAbstract
class ( Functor m
, Applicative m
-#if __GLASGOW_HASKELL__ == 710
+#if __GLASGOW_HASKELL__ < 800
, Monad m
#else
, Fail.MonadFail m
diff --git a/src/full/Agda/TypeChecking/Names.hs b/src/full/Agda/TypeChecking/Names.hs
index 004fa47..531d068 100644
--- a/src/full/Agda/TypeChecking/Names.hs
+++ b/src/full/Agda/TypeChecking/Names.hs
@@ -130,12 +130,7 @@ cl' = pure
cl :: Monad m => m a -> NamesT m a
cl = lift
-open :: ( Monad m
-#if __GLASGOW_HASKELL__ <= 708
- , Applicative m
-#endif
- , Subst t a
- ) => a -> NamesT m (NamesT m a)
+open :: (Monad m, Subst t a) => a -> NamesT m (NamesT m a)
open a = do
ctx <- NamesT ask
pure $ inCxt ctx a
@@ -146,9 +141,6 @@ bind' n f = do
(NamesT . local (n:) . unName $ f (inCxt (n:cxt) (deBruijnVar 0)))
bind :: ( Monad m
-#if __GLASGOW_HASKELL__ <= 708
- , Functor m
-#endif
, Subst t' b
, DeBruijn b
, Subst t a
@@ -157,11 +149,7 @@ bind :: ( Monad m
ArgName -> (NamesT m b -> NamesT m a) -> NamesT m (Abs a)
bind n f = Abs n <$> bind' n f
-#if __GLASGOW_HASKELL__ <= 708
-glam :: (Functor m, Monad m)
-#else
glam :: Monad m
-#endif
=> ArgInfo -> ArgName -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
glam info n f = Lam info <$> bind n f
@@ -170,18 +158,10 @@ glamN :: (Functor m, Monad m) =>
glamN [] f = f $ pure []
glamN (Arg i n:ns) f = glam i n $ \ x -> glamN ns (\ xs -> f ((:) <$> (Arg i <$> x) <*> xs))
-#if __GLASGOW_HASKELL__ <= 708
-lam :: (Functor m, Monad m)
-#else
lam :: Monad m
-#endif
=> ArgName -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
lam n f = glam defaultArgInfo n f
-#if __GLASGOW_HASKELL__ <= 708
-ilam :: (Functor m, Monad m)
-#else
ilam :: Monad m
-#endif
=> ArgName -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
ilam n f = glam (setRelevance Irrelevant defaultArgInfo) n f
diff --git a/src/full/Agda/TypeChecking/Primitive.hs b/src/full/Agda/TypeChecking/Primitive.hs
index 7298a3d..5e7f749 100644
--- a/src/full/Agda/TypeChecking/Primitive.hs
+++ b/src/full/Agda/TypeChecking/Primitive.hs
@@ -28,6 +28,7 @@ import qualified Data.Map as Map
import Data.Set (Set)
import qualified Data.Set as Set
import Data.Maybe
+import Data.Monoid
import Data.Traversable (traverse)
import Data.Monoid (mempty)
import Data.Word
@@ -59,15 +60,16 @@ import Agda.TypeChecking.Pretty () -- instances only
import Agda.TypeChecking.Names
import Agda.TypeChecking.Warnings
+import Agda.Utils.Float
import Agda.Utils.Functor
import Agda.Utils.List
import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Utils.Pretty (pretty, prettyShow)
+import Agda.Utils.Singleton
import Agda.Utils.Size
import Agda.Utils.String ( Str(Str), unStr )
import Agda.Utils.Tuple
-import Agda.Utils.Float
#include "undefined.h"
import Agda.Utils.Impossible
@@ -1583,6 +1585,13 @@ primStringToListInjective = do
toList <- primFunName <$> getPrimitive "primStringToList"
mkPrimInjective string chars toList
+primWord64ToNatInjective :: TCM PrimitiveImpl
+primWord64ToNatInjective = do
+ word <- primType (undefined :: Word64)
+ nat <- primType (undefined :: Nat)
+ toNat <- primFunName <$> getPrimitive "primWord64ToNat"
+ mkPrimInjective word nat toNat
+
getRefl :: TCM (Arg Term -> Term)
getRefl = do
-- BUILTIN REFL maybe a constructor with one (the principal) argument or only parameters.
@@ -1750,11 +1759,11 @@ mkPrimFun1TCM mt f = do
return $ PrimImpl t $ primFun __IMPOSSIBLE__ 1 $ \ts ->
case ts of
[v] ->
- redBind (toA v) (\v' -> [v']) $ \x -> do
+ redBind (toA v) singleton $ \ x -> do
b <- f x
- case allMetas b of
- (m:_) -> return $ NoReduction [reduced (Blocked m v)]
- [] -> redReturn =<< fromB b
+ case firstMeta b of
+ Just m -> return $ NoReduction [reduced (Blocked m v)]
+ Nothing -> redReturn =<< fromB b
_ -> __IMPOSSIBLE__
-- Tying the knot
@@ -1767,8 +1776,7 @@ mkPrimFun1 f = do
return $ PrimImpl t $ primFun __IMPOSSIBLE__ 1 $ \ts ->
case ts of
[v] ->
- redBind (toA v)
- (\v' -> [v']) $ \x ->
+ redBind (toA v) singleton $ \ x ->
redReturn $ fromB $ f x
_ -> __IMPOSSIBLE__
@@ -1874,12 +1882,7 @@ pPi' n phi b = toFinitePi <$> nPi' n (elInf $ cl (liftTCM primIsOne) <@> phi) b
toFinitePi (El s (Pi d b)) = El s $ Pi (setRelevance Irrelevant $ d { domFinite = True }) b
toFinitePi _ = __IMPOSSIBLE__
-#if __GLASGOW_HASKELL__ <= 708
-el' :: (Functor m, Applicative m, Monad m)
-#else
-el' :: Monad m
-#endif
- => m Term -> m Term -> m Type
+el' :: Monad m => m Term -> m Term -> m Type
el' l a = El <$> (tmSort <$> l) <*> a
elInf :: Functor m => m Term -> m Type
@@ -2004,6 +2007,7 @@ primitiveFunctions = Map.fromList
-- Machine words
, "primWord64ToNat" |-> mkPrimFun1 (fromIntegral :: Word64 -> Nat)
, "primWord64FromNat" |-> mkPrimFun1 (fromIntegral :: Nat -> Word64)
+ , "primWord64ToNatInjective" |-> primWord64ToNatInjective
-- Level functions
, "primLevelZero" |-> mkPrimLevelZero
diff --git a/src/full/Agda/TypeChecking/Records.hs b/src/full/Agda/TypeChecking/Records.hs
index 52358a0..7b51310 100644
--- a/src/full/Agda/TypeChecking/Records.hs
+++ b/src/full/Agda/TypeChecking/Records.hs
@@ -52,64 +52,62 @@ mkCon :: ConHead -> ConInfo -> Args -> Term
mkCon h info args = Con h info (map Apply args)
-- | Order the fields of a record construction.
--- Use the second argument for missing fields.
-orderFields :: QName -> a -> [C.Name] -> [(C.Name, a)] -> TCM [a]
-orderFields r def xs fs = do
- unlessNull (ys List.\\ List.nub ys) $ typeError . DuplicateFields . List.nub
- unlessNull (ys List.\\ xs) $ typeError . TooManyFields r
- -- shouldBeNull (xs List.\\ ys) $ TooFewFields r
- return $ order xs fs
+orderFields
+ :: forall a
+ . QName -- ^ Name of record type (for error message).
+ -> (Arg C.Name -> a) -- ^ How to fill a missing field.
+ -> [Arg C.Name] -- ^ Field names of the record type.
+ -> [(C.Name, a)] -- ^ Provided fields with content in the record expression.
+ -> TCM [a] -- ^ Content arranged in official order.
+orderFields r fill axs fs = do
+ reportSDoc "tc.record" 30 $ vcat
+ [ "orderFields"
+ , " official fields: " <+> sep (map pretty xs)
+ , " provided fields: " <+> sep (map pretty ys)
+ ]
+ unlessNull duplicate $ typeError . DuplicateFields . List.nub
+ unlessNull alien $ typeError . TooManyFields r missing
+ return $ for axs $ \ ax -> fromMaybe (fill ax) $ lookup (unArg ax) fs
where
- ys = map fst fs
-
- -- invariant: the first list contains at least the fields of the second list
- order [] [] = []
- order [] _ = __IMPOSSIBLE__
- order (x : xs) ys = case lookup x (assocHoles ys) of
- Just (e, ys') -> e : order xs ys'
- Nothing -> def : order xs ys
-
- assocHoles xs = [ (x, (v, xs')) | ((x, v), xs') <- holes xs ]
+ xs = map unArg axs -- official fields (accord. record type)
+ ys = map fst fs -- provided fields
+ duplicate = ys List.\\ List.nub ys -- duplicate fields
+ alien = ys List.\\ xs -- spurious fields
+ missing = xs List.\\ ys -- missing fields
-- | A record field assignment @record{xs = es}@ might not mention all
-- visible fields. @insertMissingFields@ inserts placeholders for
-- the missing visible fields and returns the values in order
-- of the fields in the record declaration.
insertMissingFields
- :: QName -- ^ Name of record type (for error reporting).
+ :: forall a
+ . QName -- ^ Name of record type (for error reporting).
-> (C.Name -> a) -- ^ Function to generate a placeholder for missing visible field.
-> [FieldAssignment' a] -- ^ Given fields.
-> [Arg C.Name] -- ^ All record field names with 'ArgInfo'.
-> TCM [NamedArg a] -- ^ Given fields enriched by placeholders for missing explicit fields.
insertMissingFields r placeholder fs axs = do
-- Compute the list of given fields, decorated with the ArgInfo from the record def.
- let arg x e =
- case [ a | a <- axs, unArg a == x ] of
- [a] -> nameIfHidden a e <$ a
- _ -> defaultNamedArg e -- we only end up here if the field names are bad
+ let arg x e = caseMaybe (List.find ((x ==) . unArg) axs) (defaultNamedArg e) $ \ a ->
+ nameIfHidden a e <$ a
givenFields = [ (x, Just $ arg x e) | FieldAssignment x e <- fs ]
- -- Compute a list of p[aceholders for the missing visible fields.
- let missingExplicits =
- [ (x, Just $ setOrigin Inserted $ nameIfHidden a . placeholder <$> a)
- | a <- filter visible axs
- , let x = unArg a
- , x `notElem` map (view nameFieldA) fs
- ]
- -- In es omitted explicit fields are replaced by placeholders
- -- (from missingExplicits). Omitted implicit or instance fields
+
+ -- Omitted explicit fields are filled in with placeholders.
+ -- Omitted implicit or instance fields
-- are still left out and inserted later by checkArguments_.
- catMaybes <$> do
- -- Default value @Nothing@ will only be used for missing hidden fields.
- -- These can be ignored as they will be inserted by @checkArguments_@.
- orderFields r Nothing (map unArg axs) $ givenFields ++ missingExplicits
+ catMaybes <$> orderFields r fill axs givenFields
where
+ fill :: Arg C.Name -> Maybe (NamedArg a)
+ fill ax
+ | visible ax = Just $ setOrigin Inserted $ unnamed . placeholder <$> ax
+ | otherwise = Nothing
-- Andreas, 2017-04-13, issue #2494
-- We need to put the field names as argument names for hidden arguments.
-- Otherwise, insertImplicit does not do the right thing.
nameIfHidden :: Arg C.Name -> c -> Named_ c
nameIfHidden ax
| visible ax = unnamed
- | otherwise = named (Ranged (getRange ax) $ prettyShow $ unArg ax)
+ | otherwise = named $ Ranged (getRange ax) $ prettyShow $ unArg ax
-- | The name of the module corresponding to a record.
recordModule :: QName -> ModuleName
diff --git a/src/full/Agda/TypeChecking/Reduce.hs b/src/full/Agda/TypeChecking/Reduce.hs
index 7d97598..62765e1 100644
--- a/src/full/Agda/TypeChecking/Reduce.hs
+++ b/src/full/Agda/TypeChecking/Reduce.hs
@@ -11,6 +11,7 @@ import qualified Data.List as List
import Data.List ((\\))
import Data.Maybe
import Data.Map (Map)
+import Data.Monoid
import Data.Traversable
import Data.Hashable
@@ -80,7 +81,7 @@ isFullyInstantiatedMeta :: MetaId -> TCM Bool
isFullyInstantiatedMeta m = do
mv <- TCM.lookupMeta m
case mvInstantiation mv of
- InstV _tel v -> null . allMetas <$> instantiateFull v
+ InstV _tel v -> noMetas <$> instantiateFull v
_ -> return False
-- | Instantiate something.
diff --git a/src/full/Agda/TypeChecking/Rewriting.hs b/src/full/Agda/TypeChecking/Rewriting.hs
index 156ed23..4a922fc 100644
--- a/src/full/Agda/TypeChecking/Rewriting.hs
+++ b/src/full/Agda/TypeChecking/Rewriting.hs
@@ -207,8 +207,8 @@ addRewriteRule q = do
gamma1 <- instantiateFull gamma1
let gamma = gamma0 `abstract` gamma1
- unless (null $ allMetas (telToList gamma1)) $ do
- reportSDoc "rewriting" 30 $ "metas in gamma1: " <+> text (show $ allMetas $ telToList gamma1)
+ unless (noMetas (telToList gamma1)) $ do
+ reportSDoc "rewriting" 30 $ "metas in gamma1: " <+> text (show $ allMetasList $ telToList gamma1)
failureMetas
-- 2017-06-18, Jesper: Unfold inlined definitions on the LHS.
@@ -236,10 +236,10 @@ addRewriteRule q = do
checkNoLhsReduction f es
- unless (null $ allMetas (es, rhs, b)) $ do
- reportSDoc "rewriting" 30 $ "metas in lhs: " <+> text (show $ allMetas es)
- reportSDoc "rewriting" 30 $ "metas in rhs: " <+> text (show $ allMetas rhs)
- reportSDoc "rewriting" 30 $ "metas in b : " <+> text (show $ allMetas b)
+ unless (noMetas (es, rhs, b)) $ do
+ reportSDoc "rewriting" 30 $ "metas in lhs: " <+> text (show $ allMetasList es)
+ reportSDoc "rewriting" 30 $ "metas in rhs: " <+> text (show $ allMetasList rhs)
+ reportSDoc "rewriting" 30 $ "metas in b : " <+> text (show $ allMetasList b)
failureMetas
ps <- patternFrom Relevant 0 (t , Def f []) es
diff --git a/src/full/Agda/TypeChecking/Rewriting/NonLinMatch.hs b/src/full/Agda/TypeChecking/Rewriting/NonLinMatch.hs
index 1459ec4..effbb93 100644
--- a/src/full/Agda/TypeChecking/Rewriting/NonLinMatch.hs
+++ b/src/full/Agda/TypeChecking/Rewriting/NonLinMatch.hs
@@ -31,6 +31,7 @@ import Debug.Trace
import System.IO.Unsafe
import Data.Maybe
+import Data.Monoid
import Data.Traversable (Traversable,traverse)
import Data.IntMap (IntMap)
import qualified Data.IntMap as IntMap
@@ -528,10 +529,9 @@ equal :: (MonadReduce m, HasConstInfo m)
equal u v = do
(u, v) <- etaContract =<< normalise (u, v)
let ok = u == v
- metas = allMetas (u, v)
- block = caseMaybe (headMaybe metas)
+ block = caseMaybe (firstMeta (u, v))
(NotBlocked ReallyNotBlocked ())
- (\m -> Blocked m ())
+ (\ m -> Blocked m ())
if ok then return Nothing else do
traceSDoc "rewriting.match" 10 (sep
[ "mismatch between " <+> prettyTCM u
diff --git a/src/full/Agda/TypeChecking/Rules/Data.hs b/src/full/Agda/TypeChecking/Rules/Data.hs
index 3ea684c..db90234 100644
--- a/src/full/Agda/TypeChecking/Rules/Data.hs
+++ b/src/full/Agda/TypeChecking/Rules/Data.hs
@@ -1,5 +1,6 @@
{-# LANGUAGE CPP #-}
{-# LANGUAGE MultiWayIf #-}
+{-# LANGUAGE NondecreasingIndentation #-}
module Agda.TypeChecking.Rules.Data where
@@ -7,6 +8,8 @@ import Control.Monad
import Data.List (genericTake)
import Data.Maybe (fromMaybe, catMaybes, isJust)
+import Control.Monad.Trans.Maybe
+import Control.Monad.Trans
import Data.Set (Set)
import qualified Data.Set as Set
@@ -341,10 +344,9 @@ defineCompData d con params names fsT t boundary = do
, builtinPOr
, builtinItIsOne
]
- sortsOk <- sortOk t `and2M` allM (map unDom (flattenTel fsT)) sortOkField
- if not sortsOk || not (all isJust required) then return $ emptyCompKit else do
+ if not (all isJust required) then return $ emptyCompKit else do
hcomp <- whenDefined (null boundary) [builtinHComp,builtinTrans] (defineTranspOrHCompD DoHComp d con params names fsT t boundary)
- transp <- whenDefined True [builtinTrans] (defineTranspOrHCompD DoTransp d con params names fsT t boundary)
+ transp <- whenDefined True [builtinTrans] (defineTranspOrHCompD DoTransp d con params names fsT t boundary)
return $ CompKit
{ nameOfTransp = transp
, nameOfHComp = hcomp
@@ -355,10 +357,12 @@ defineCompData d con params names fsT t boundary = do
withArgInfo tel = zipWith Arg (map domInfo . telToList $ tel)
defineTranspOrHCompD cmd d con params names fsT t boundary
= do
- ((theName, gamma , ty, _cl_types , bodies), theSub) <-
- (case cmd of DoTransp -> defineTranspForFields' (guard (not $ null boundary) >> (Just $ Con con ConOSystem $ teleElims fsT boundary))
- ; DoHComp -> defineHCompForFields)
- (\ t p -> apply (Def p []) [argN t]) d params fsT (map argN names) t
+ let project = (\ t p -> apply (Def p []) [argN t])
+ stuff <- defineTranspOrHCompForFields cmd
+ (guard (not $ null boundary) >> (Just $ Con con ConOSystem $ teleElims fsT boundary))
+ project d params fsT (map argN names) t
+ caseMaybe stuff (return Nothing) $ \ ((theName, gamma , ty, _cl_types , bodies), theSub) -> do
+
iz <- primIZero
body <- do
case cmd of
@@ -538,18 +542,6 @@ defineCompData d con params names fsT t boundary = do
xs <- mapM getTerm' xs
if all isJust xs then m else return Nothing
- sortOk :: Type -> TCM Bool
- sortOk a = reduce (getSort a) >>= \case
- Type{} -> return True
- _ -> return False
-
- sortOkField :: Type -> TCM Bool
- sortOkField a = reduce (getSort a) >>= \case
- Type{} -> return True
- -- fields might be elements of the interval
- Inf -> return True
- _ -> return False
-
-- Andrea: TODO handle Irrelevant fields somehow.
defineProjections :: QName -- datatype name
-> ConHead
@@ -607,29 +599,88 @@ freshAbstractQName'_ :: String -> TCM QName
freshAbstractQName'_ s = freshAbstractQName noFixity' (C.Name noRange C.InScope [C.Id $ s])
-defineTranspForFields
- :: (Term -> QName -> Term) -- ^ how to apply a "projection" to a term
+-- * Special cases of Type
+-----------------------------------------------------------
+
+-- | A @Type@ with sort @Type l@
+-- Such a type supports both hcomp and transp.
+data LType = LEl Level Term deriving (Eq,Show)
+
+fromLType :: LType -> Type
+fromLType (LEl l t) = El (Type l) t
+
+lTypeLevel :: LType -> Level
+lTypeLevel (LEl l t) = l
+
+toLType :: MonadReduce m => Type -> m (Maybe LType)
+toLType ty = do
+ sort <- reduce $ getSort ty
+ case sort of
+ Type l -> return $ Just $ LEl l (unEl ty)
+ _ -> return $ Nothing
+
+instance Subst Term LType where
+ applySubst rho (LEl l t) = LEl (applySubst rho l) (applySubst rho t)
+
+-- | A @Type@ that either has sort @Type l@ or is a closed definition.
+-- Such a type supports some version of transp.
+-- In particular we want to allow the Interval as a @ClosedType@.
+data CType = ClosedType QName | LType LType deriving (Eq,Show)
+
+fromCType :: CType -> Type
+fromCType (ClosedType q) = El Inf (Def q [])
+fromCType (LType t) = fromLType t
+
+toCType :: MonadReduce m => Type -> m (Maybe CType)
+toCType ty = do
+ sort <- reduce $ getSort ty
+ case sort of
+ Type l -> return $ Just $ LType (LEl l (unEl ty))
+ Inf -> do
+ t <- reduce (unEl ty)
+ case t of
+ Def q [] -> return $ Just $ ClosedType q
+ _ -> return $ Nothing
+ _ -> return $ Nothing
+
+instance Subst Term CType where
+ applySubst rho t@ClosedType{} = t
+ applySubst rho (LType t) = LType $ applySubst rho t
+
+
+defineTranspOrHCompForFields
+ :: TranspOrHComp
+ -> (Maybe Term) -- ^ PathCons, Δ.Φ ⊢ u : R δ
+ -> (Term -> QName -> Term) -- ^ how to apply a "projection" to a term
-> QName -- ^ some name, e.g. record name
-> Telescope -- ^ param types Δ
-> Telescope -- ^ fields' types Δ ⊢ Φ
-> [Arg QName] -- ^ fields' names
-> Type -- ^ record type Δ ⊢ T
- -> TCM ((QName, Telescope, Type, [Dom Type], [Term]), Substitution)
-defineTranspForFields = defineTranspForFields' Nothing
+ -> TCM (Maybe ((QName, Telescope, Type, [Dom Type], [Term]), Substitution))
+defineTranspOrHCompForFields cmd pathCons project name params fsT fns rect =
+ case cmd of
+ DoTransp -> runMaybeT $ do
+ fsT' <- traverse (traverse (MaybeT . toCType)) fsT
+ lift $ defineTranspForFields pathCons project name params fsT' fns rect
+ DoHComp -> runMaybeT $ do
+ fsT' <- traverse (traverse (MaybeT . toLType)) fsT
+ rect' <- MaybeT $ toLType rect
+ lift $ defineHCompForFields project name params fsT' fns rect'
-- invariant: resulting tel Γ is such that Γ = ... , (φ : I), (a0 : ...)
-- where a0 has type matching the arguments of primTrans.
-defineTranspForFields'
- :: (Maybe Term) -- ^ PathCons, Δ.Φ ⊢ u : R δ
+defineTranspForFields
+ :: (Maybe Term) -- ^ PathCons, Δ.Φ ⊢ u : R δ
-> (Term -> QName -> Term) -- ^ how to apply a "projection" to a term
-> QName -- ^ some name, e.g. record name
-> Telescope -- ^ param types Δ
- -> Telescope -- ^ fields' types Δ ⊢ Φ
+ -> Tele (Dom CType) -- ^ fields' types Δ ⊢ Φ
-> [Arg QName] -- ^ fields' names
-> Type -- ^ record type Δ ⊢ T
-> TCM ((QName, Telescope, Type, [Dom Type], [Term]), Substitution)
-defineTranspForFields' pathCons applyProj name params fsT fns rect = do
+defineTranspForFields pathCons applyProj name params fsT fns rect = do
interval <- elInf primInterval
let deltaI = expTelescope interval params
iz <- primIZero
@@ -703,7 +754,7 @@ defineTranspForFields' pathCons applyProj name params fsT fns rect = do
(tel,theta,the_phi,the_u0, the_fields) =
case pathCons of
-- (δ : Δ).Φ ⊢ u : R δ
- Just u -> (abstract gamma' (d0 `applySubst` fsT) -- Ξ = δ : Δ^I, φ : F, _ : Φ[δ i0]
+ Just u -> (abstract gamma' (d0 `applySubst` fmap (fmap fromCType) fsT) -- Ξ = δ : Δ^I, φ : F, _ : Φ[δ i0]
, (liftS (size fsT) d0 `applySubst` u) `consS` raiseS (size fsT)
, raise (size fsT) (var 0)
, (liftS (size fsT) d0 `applySubst` u)
@@ -719,11 +770,11 @@ defineTranspForFields' pathCons applyProj name params fsT fns rect = do
-- .. ⊢ field : filled_ty' i0
mkBody (field, filled_ty') = do
let
- filled_ty = lam_i $ (unEl . unDom) filled_ty'
+ filled_ty = lam_i $ (unEl . fromCType . unDom) filled_ty'
-- Γ ⊢ l : I -> Level of filled_ty
- sort <- reduce $ getSort $ unDom filled_ty'
- case sort of
- Type l -> do
+ -- sort <- reduce $ getSort $ unDom filled_ty'
+ case unDom filled_ty' of
+ LType (LEl l _) -> do
let lvl = lam_i $ Level l
return $ runNames [] $ do
lvl <- open lvl
@@ -732,11 +783,10 @@ defineTranspForFields' pathCons applyProj name params fsT fns rect = do
<@> phi
<@> field
-- interval arg
- Inf ->
+ ClosedType{} ->
return $ runNames [] $ do
[field] <- mapM open [field]
field
- _ -> __IMPOSSIBLE__
let
-- ' Ξ , i : I ⊢ τ = [(\ j → δ (i ∧ j)), φ ∨ ~ i, u] : Ξ
@@ -765,7 +815,7 @@ defineTranspForFields' pathCons applyProj name params fsT fns rect = do
let
-- Ξ, i : I ⊢ ... : Δ.Φ
theSubst = reverse (tau `applySubst` bodys) ++# (liftS 1 (raiseS (size tel - size deltaI)) `composeS` sub params)
- return $ ((theName, tel, theta `applySubst` rtype, clause_types, bodys), theSubst)
+ return $ ((theName, tel, theta `applySubst` rtype, map (fmap fromCType) clause_types, bodys), theSubst)
where
-- record type in 'exponentiated' context
-- (params : Δ^I), i : I |- T[params i]
@@ -789,9 +839,9 @@ defineHCompForFields
:: (Term -> QName -> Term) -- ^ how to apply a "projection" to a term
-> QName -- ^ some name, e.g. record name
-> Telescope -- ^ param types Δ
- -> Telescope -- ^ fields' types Δ ⊢ Φ
+ -> Tele (Dom LType) -- ^ fields' types Δ ⊢ Φ
-> [Arg QName] -- ^ fields' names
- -> Type -- ^ record type (δ : Δ) ⊢ R[δ]
+ -> LType -- ^ record type (δ : Δ) ⊢ R[δ]
-> TCM ((QName, Telescope, Type, [Dom Type], [Term]),Substitution)
defineHCompForFields applyProj name params fsT fns rect = do
interval <- elInf primInterval
@@ -816,14 +866,14 @@ defineHCompForFields applyProj name params fsT fns rect = do
reportSLn "hcomp.rec" 5 $ ("Generated name: " ++ show theName ++ " " ++ showQNameId theName)
theType <- (abstract delta <$>) $ runNamesT [] $ do
- rect <- open rect
+ rect <- open $ fromLType rect
nPi' "phi" (elInf $ cl primInterval) $ \ phi ->
(nPi' "i" (elInf $ cl primInterval) $ \ i ->
pPi' "o" phi $ \ _ -> rect) -->
rect --> rect
reportSDoc "hcomp.rec" 20 $ prettyTCM theType
- reportSDoc "hcomp.rec" 60 $ text $ "sort = " ++ show (getSort rect)
+ reportSDoc "hcomp.rec" 60 $ text $ "sort = " ++ show (lTypeLevel rect)
noMutualBlock $ addConstant theName $ (defaultDefn defaultArgInfo theName theType
(emptyFunction { funTerminates = Just True }))
@@ -835,7 +885,7 @@ defineHCompForFields applyProj name params fsT fns rect = do
let -- Γ ⊢ R δ
drect_gamma = raiseS (size gamma - size delta) `applySubst` rect
- reportSDoc "hcomp.rec" 60 $ text $ "sort = " ++ show (getSort drect_gamma)
+ reportSDoc "hcomp.rec" 60 $ text $ "sort = " ++ show (lTypeLevel drect_gamma)
let
@@ -851,8 +901,8 @@ defineHCompForFields applyProj name params fsT fns rect = do
-- ' (δ, φ, u, u0) : Γ ⊢ fillR Γ : (i : I) → rtype[ δ ↦ (\ j → δ (i ∧ j))]
fillTerm = runNames [] $ do
- rect <- open $ unEl drect_gamma
- lvl <- open . (\ (Type l) -> Level l) $ getSort drect_gamma
+ rect <- open . unEl . fromLType $ drect_gamma
+ lvl <- open . Level . lTypeLevel $ drect_gamma
params <- mapM open $ take (size delta) $ teleArgs gamma
[phi,w,w0] <- mapM open [the_phi,the_u,the_u0]
-- (δ : Δ, φ : I, w : .., w0 : R δ) ⊢
@@ -903,9 +953,9 @@ defineHCompForFields applyProj name params fsT fns rect = do
mkBody (fname, filled_ty') = do
let
proj t = (`applyProj` unArg fname) <$> t
- filled_ty = Lam defaultArgInfo (Abs "i" $ (unEl . unDom) filled_ty')
+ filled_ty = Lam defaultArgInfo (Abs "i" $ (unEl . fromLType . unDom) filled_ty')
-- Γ ⊢ l : I -> Level of filled_ty
- Type l <- reduce $ getSort $ unDom filled_ty'
+ l <- reduce $ lTypeLevel $ unDom filled_ty'
let lvl = Lam defaultArgInfo (Abs "i" $ Level l)
return $ runNames [] $ do
lvl <- open lvl
@@ -918,10 +968,10 @@ defineHCompForFields applyProj name params fsT fns rect = do
(lam "i" $ \ i -> lam "o" $ \ o -> proj $ w <@> i <@> o) -- TODO wait for phi = 1
(proj w0)
- reportSDoc "hcomp.rec" 60 $ text $ "filled_types sorts:" ++ show (map (getSort . unDom) filled_types)
+ reportSDoc "hcomp.rec" 60 $ text $ "filled_types sorts:" ++ show (map (getSort . fromLType . unDom) filled_types)
bodys <- mapM mkBody (zip fns filled_types)
- return $ ((theName, gamma, rtype, clause_types, bodys),IdS)
+ return $ ((theName, gamma, rtype, map (fmap fromLType) clause_types, bodys),IdS)
getGeneralizedParameters :: Set Name -> QName -> TCM [Maybe Name]
diff --git a/src/full/Agda/TypeChecking/Rules/LHS/ProblemRest.hs b/src/full/Agda/TypeChecking/Rules/LHS/ProblemRest.hs
index b58ae9f..440af1a 100644
--- a/src/full/Agda/TypeChecking/Rules/LHS/ProblemRest.hs
+++ b/src/full/Agda/TypeChecking/Rules/LHS/ProblemRest.hs
@@ -3,10 +3,6 @@
module Agda.TypeChecking.Rules.LHS.ProblemRest where
-#if __GLASGOW_HASKELL__ <= 708
-import Data.Functor ( (<$), (<$>) )
-#endif
-
import Control.Arrow (first, second)
import Control.Monad
diff --git a/src/full/Agda/TypeChecking/Rules/Record.hs b/src/full/Agda/TypeChecking/Rules/Record.hs
index e948459..79f2e6e 100644
--- a/src/full/Agda/TypeChecking/Rules/Record.hs
+++ b/src/full/Agda/TypeChecking/Rules/Record.hs
@@ -1,4 +1,5 @@
{-# LANGUAGE CPP #-}
+{-# LANGUAGE NondecreasingIndentation #-}
module Agda.TypeChecking.Rules.Record where
@@ -35,7 +36,7 @@ import Agda.TypeChecking.CompiledClause (hasProjectionPatterns)
import Agda.TypeChecking.CompiledClause.Compile
import Agda.TypeChecking.Rules.Data ( getGeneralizedParameters, bindGeneralizedParameters, bindParameters, fitsIn, forceSort,
- defineCompData, defineTranspForFields, defineHCompForFields )
+ defineCompData, defineTranspOrHCompForFields )
import Agda.TypeChecking.Rules.Term ( isType_ )
import {-# SOURCE #-} Agda.TypeChecking.Rules.Decl (checkDecl)
@@ -374,9 +375,8 @@ defineCompKitR name params fsT fns rect = do
]
reportSDoc "tc.rec.cxt" 30 $ prettyTCM params
reportSDoc "tc.rec.cxt" 30 $ prettyTCM fsT
- reportSDoc "tc.rec.cxt" 30 $ text $ show rect
- sortsOk <- allM (rect : map unDom (flattenTel fsT)) sortOk
- if not $ sortsOk && all isJust required then return $ emptyCompKit else do
+ reportSDoc "tc.rec.cxt" 30 $ pretty rect
+ if not $ all isJust required then return $ emptyCompKit else do
transp <- whenDefined [builtinTrans] (defineTranspOrHCompR DoTransp name params fsT fns rect)
hcomp <- whenDefined [builtinTrans,builtinHComp] (defineTranspOrHCompR DoHComp name params fsT fns rect)
return $ CompKit
@@ -387,10 +387,6 @@ defineCompKitR name params fsT fns rect = do
whenDefined xs m = do
xs <- mapM getTerm' xs
if all isJust xs then m else return Nothing
- sortOk :: Type -> TCM Bool
- sortOk a = reduce (getSort a) >>= \case
- Type{} -> return True
- _ -> return False
defineTranspOrHCompR ::
@@ -402,10 +398,10 @@ defineTranspOrHCompR ::
-> Type -- ^ record type Δ ⊢ T
-> TCM (Maybe QName)
defineTranspOrHCompR cmd name params fsT fns rect = do
- (theName, gamma, rtype, clause_types, bodies) <- fst <$>
- (case cmd of DoTransp -> defineTranspForFields; DoHComp -> defineHCompForFields)
- (\ t fn -> t `applyE` [Proj ProjSystem fn]) name params fsT fns rect
+ let project = (\ t fn -> t `applyE` [Proj ProjSystem fn])
+ stuff <- fmap fst <$> defineTranspOrHCompForFields cmd Nothing project name params fsT fns rect
+ caseMaybe stuff (return Nothing) $ \ (theName, gamma, rtype, clause_types, bodies) -> do
-- phi = 1 clause
c' <- do
io <- primIOne
diff --git a/src/full/Agda/TypeChecking/Rules/Term.hs b/src/full/Agda/TypeChecking/Rules/Term.hs
index d5304e4..280dcaa 100644
--- a/src/full/Agda/TypeChecking/Rules/Term.hs
+++ b/src/full/Agda/TypeChecking/Rules/Term.hs
@@ -553,9 +553,9 @@ checkAbsurdLambda cmp i h e t = do
case unEl t' of
Pi dom@(Dom{domInfo = info', unDom = a}) b
| not (sameHiding h info') -> typeError $ WrongHidingInLambda t'
- | not (null $ allMetas a) ->
+ | not (noMetas a) ->
postponeTypeCheckingProblem (CheckExpr cmp e t') $
- null . allMetas <$> instantiateFull a
+ noMetas <$> instantiateFull a
| otherwise -> blockTerm t' $ do
ensureEmptyType (getRange i) a
-- Add helper function
@@ -578,7 +578,7 @@ checkAbsurdLambda cmp i h e t = do
{ clauseLHSRange = getRange e
, clauseFullRange = getRange e
, clauseTel = telFromList [fmap (absurdPatternName,) dom]
- , namedClausePats = [Arg info' $ Named (Just $ unranged $ absName b) $ VarP PatOAbsurd (DBPatVar absurdPatternName 0)]
+ , namedClausePats = [Arg info' $ Named (Just $ unranged $ absName b) $ absurdP 0]
, clauseBody = Nothing
, clauseType = Just $ setRelevance rel $ defaultArg $ absBody b
, clauseCatchall = False
@@ -682,7 +682,7 @@ catchIlltypedPatternBlockedOnMeta m handle = do
-- (seems to archieve a bit along @normalize@, but how much??).
problem <- reduce =<< instantiateFull (flattenTel tel, us, vs)
-- over-approximating the set of metas actually blocking unification
- return $ listToMaybe $ allMetas problem
+ return $ firstMeta problem
SplitError (NotADatatype aClosure) ->
enterClosure aClosure $ \ a -> isBlockedType a
@@ -892,8 +892,9 @@ checkRecordUpdate cmp ei recexpr fs e t = do
-- to their counterpart in the record type definition.
disambiguateRecordFields (map _nameFieldA fs) (map unArg projs)
- xs <- map unArg <$> getRecordFieldNames r
- es <- orderFields r Nothing xs $ map (\ (FieldAssignment x e) -> (x, Just e)) fs
+ axs <- getRecordFieldNames r
+ let xs = map unArg axs
+ es <- orderFields r (\ _ -> Nothing) axs $ map (\ (FieldAssignment x e) -> (x, Just e)) fs
let es' = zipWith (replaceFields name ei) projs es
checkExpr' cmp (A.Rec ei [ Left (FieldAssignment x e) | (x, Just e) <- zip xs es' ]) t
@@ -1194,36 +1195,33 @@ checkExpr' cmp e t0 =
doQuoteTerm :: Comparison -> Term -> Type -> TCM Term
doQuoteTerm cmp et t = do
et' <- etaContract =<< instantiateFull et
- let metas = allMetas et'
- case metas of
- _:_ -> postponeTypeCheckingProblem (DoQuoteTerm cmp et t) $ andM $ map isInstantiatedMeta metas
+ case allMetasList et' of
[] -> do
q <- quoteTerm et'
ty <- el primAgdaTerm
coerce cmp q ty t
+ metas -> postponeTypeCheckingProblem (DoQuoteTerm cmp et t) $ andM $ map isInstantiatedMeta metas
-- | Checking `quoteGoal` (deprecated)
quoteGoal :: Type -> TCM (Either [MetaId] Term)
quoteGoal t = do
t' <- etaContract =<< instantiateFull t
- let metas = allMetas t'
- case metas of
- _:_ -> return $ Left metas
+ case allMetasList t' of
[] -> do
quotedGoal <- quoteTerm (unEl t')
return $ Right quotedGoal
+ metas -> return $ Left metas
-- | Checking `quoteContext` (deprecated)
quoteContext :: TCM (Either [MetaId] Term)
quoteContext = do
contextTypes <- map (fmap snd) <$> getContext
contextTypes <- etaContract =<< instantiateFull contextTypes
- let metas = allMetas contextTypes
- case metas of
- _:_ -> return $ Left metas
+ case allMetasList contextTypes of
[] -> do
quotedContext <- buildList <*> mapM quoteDom contextTypes
return $ Right quotedContext
+ metas -> return $ Left metas
-- | Unquote a TCM computation in a given hole.
unquoteM :: A.Expr -> Term -> Type -> TCM ()
@@ -1242,10 +1240,10 @@ unquoteTactic tac hole goal = do
mi <- lookupMeta' x
(r, meta) <- case mi of
Nothing -> do -- fresh meta: need to block on something else!
- otherMetas <- allMetas <$> instantiateFull goal
- case otherMetas of
- [] -> return (noRange, Nothing) -- Nothing to block on, leave it yellow. Alternative: fail.
- x:_ -> return (noRange, Just x) -- range?
+ (noRange,) . firstMeta <$> instantiateFull goal
+ -- Remark:
+ -- Nothing: Nothing to block on, leave it yellow. Alternative: fail.
+ -- Just x: range?
Just mi -> return (getRange mi, Just x)
setCurrentRange r $
addConstraint (UnquoteTactic meta tac hole goal)
diff --git a/src/full/Agda/TypeChecking/Serialise/Instances/Errors.hs b/src/full/Agda/TypeChecking/Serialise/Instances/Errors.hs
index d440e0b..6de30f7 100644
--- a/src/full/Agda/TypeChecking/Serialise/Instances/Errors.hs
+++ b/src/full/Agda/TypeChecking/Serialise/Instances/Errors.hs
@@ -102,6 +102,7 @@ instance EmbPrj Warning where
valu [19, a, b] = valuN CoInfectiveImport a b
valu [20, a] = valuN InstanceNoOutputTypeName a
valu [21, a] = valuN InstanceArgWithExplicitArg a
+ valu [22] = valuN WrongInstanceDeclaration
valu _ = malformed
instance EmbPrj DeclarationWarning where
diff --git a/src/full/Agda/TypeChecking/SizedTypes/Solve.hs b/src/full/Agda/TypeChecking/SizedTypes/Solve.hs
index 51af5e6..6622365 100644
--- a/src/full/Agda/TypeChecking/SizedTypes/Solve.hs
+++ b/src/full/Agda/TypeChecking/SizedTypes/Solve.hs
@@ -102,6 +102,7 @@ import Agda.Utils.Monad
import Agda.Utils.Null
import Agda.Utils.Pretty (Pretty, prettyShow)
import qualified Agda.Utils.Pretty as P
+import Agda.Utils.Singleton
import Agda.Utils.Size
import Agda.Utils.Tuple
import qualified Agda.Utils.VarSet as VarSet
@@ -145,7 +146,7 @@ solveSizeConstraints flag = do
-- @allMetas@ does not reduce or instantiate;
-- this is why we require the size constraints to be normalised.
return (cl, map metaId . Set.toList $
- sizeMetaSet `Set.intersection` Set.fromList (allMetas c))
+ sizeMetaSet `Set.intersection` allMetas singleton c)
-- Now, some constraints may have no metas (clcs), the others have at least one (othercs).
let classify :: (a, [b]) -> Either a (a, NonemptyList b)
diff --git a/src/full/Agda/TypeChecking/Telescope.hs b/src/full/Agda/TypeChecking/Telescope.hs
index f6954b7..fdbbef4 100644
--- a/src/full/Agda/TypeChecking/Telescope.hs
+++ b/src/full/Agda/TypeChecking/Telescope.hs
@@ -38,10 +38,12 @@ import qualified Agda.Utils.VarSet as VarSet
import Agda.Utils.Impossible
-- | Flatten telescope: (Γ : Tel) -> [Type Γ]
-flattenTel :: Telescope -> [Dom Type]
+flattenTel :: Subst t a => Tele (Dom a) -> [Dom a]
flattenTel EmptyTel = []
flattenTel (ExtendTel a tel) = raise (size tel + 1) a : flattenTel (absBody tel)
+{-# SPECIALIZE flattenTel :: Telescope -> [Dom Type] #-}
+
-- | Order a flattened telescope in the correct dependeny order: Γ ->
-- Permutation (Γ -> Γ~)
--
@@ -77,7 +79,7 @@ teleNames = map (fst . unDom) . telToList
teleArgNames :: Telescope -> [Arg ArgName]
teleArgNames = map (argFromDom . fmap fst) . telToList
-teleArgs :: (DeBruijn a) => Telescope -> [Arg a]
+teleArgs :: (DeBruijn a) => Tele (Dom t) -> [Arg a]
teleArgs tel =
[ Arg info (deBruijnVar i)
| (i, Dom {domInfo = info, unDom = (n,_)}) <- zip (downFrom $ size l) l ]
diff --git a/src/full/Agda/Utils/Singleton.hs b/src/full/Agda/Utils/Singleton.hs
index edc0af0..d15a989 100644
--- a/src/full/Agda/Utils/Singleton.hs
+++ b/src/full/Agda/Utils/Singleton.hs
@@ -5,6 +5,8 @@
module Agda.Utils.Singleton where
+import Data.Monoid (Endo(..))
+
import Data.Hashable (Hashable)
import Data.HashMap.Strict (HashMap)
import qualified Data.HashMap.Strict as HashMap
@@ -30,6 +32,8 @@ class Singleton el coll | coll -> el where
instance Singleton a (Maybe a) where singleton = Just
instance Singleton a [a] where singleton = (:[])
+instance Singleton a ([a] -> [a]) where singleton = (:)
+instance Singleton a (Endo [a]) where singleton = Endo . (:)
instance Singleton a (NonemptyList a)
where singleton = (:! [])
instance Singleton a (Seq a) where singleton = Seq.singleton
diff --git a/stack-8.6.4.yaml b/stack-8.6.4.yaml
deleted file mode 100644
index 457da56..0000000
--- a/stack-8.6.4.yaml
+++ /dev/null
@@ -1,20 +0,0 @@
-resolver: lts-13.16
-
-extra-deps:
-- EdisonCore-1.3.2.1
-- data-hash-0.2.0.1
-- equivalence-0.3.4
-- geniplate-mirror-0.7.6
-- EdisonAPI-1.3.1
-- STMonadTrans-0.4.3
-
-flags:
- time-locale-compat:
- old-locale: false
-
- transformers-compat:
- five-three: true
-
-# Local packages, usually specified by relative directory name
-packages:
-- '.'
diff --git a/stack-8.6.5.yaml b/stack-8.6.5.yaml
new file mode 100644
index 0000000..4b6c77a
--- /dev/null
+++ b/stack-8.6.5.yaml
@@ -0,0 +1,9 @@
+resolver: lts-13.21
+
+extra-deps:
+- EdisonCore-1.3.2.1
+- data-hash-0.2.0.1
+- equivalence-0.3.4
+- geniplate-mirror-0.7.6
+- EdisonAPI-1.3.1
+- STMonadTrans-0.4.3