[Pkg-haskell-commits] [SCM] Packaging for Agda branch, upstream, updated. upstream/2.3.2.1
Iain Lane
laney at debian.org
Sun Jun 16 12:29:46 UTC 2013
The following commit has been merged in the upstream branch:
commit bfeeaa533d985e7a6d656da71a60c836ed9d8787
Author: Iain Lane <laney at debian.org>
Date: Sun Jun 16 13:07:25 2013 +0100
Imported Upstream version 2.3.2.1
diff --git a/Agda.cabal b/Agda.cabal
index d5e35bf..de6b235 100644
--- a/Agda.cabal
+++ b/Agda.cabal
@@ -1,5 +1,5 @@
name: Agda
-version: 2.3.2
+version: 2.3.2.1
cabal-version: >= 1.8
build-type: Simple
license: OtherLicense
@@ -32,7 +32,7 @@ description:
Note that the Agda library does not follow the package versioning
policy, because it is not intended to be used by third-party
packages.
-tested-with: GHC == 7.6.1
+tested-with: GHC == 7.6.3
extra-source-files: src/full/Agda/undefined.h
README
doc/release-notes/*.txt
@@ -51,7 +51,7 @@ source-repository head
source-repository this
type: darcs
location: http://code.haskell.org/Agda/
- tag: 2.3.2
+ tag: 2.3.2.1
flag epic
default: False
@@ -65,11 +65,12 @@ library
build-depends: epic >= 0.1.13 && < 0.10
if os(windows)
- build-depends: Win32 == 2.2.*
+ build-depends: Win32 >= 2.2 && < 2.4
build-depends: base >= 4.2 && < 4.7,
- mtl >= 2.0 && < 2.2,
- QuickCheck >= 2.3 && < 2.6,
+ -- mtl-2.1 contains a severe bug
+ mtl >= 2.0 && < 2.1 || >= 2.1.1 && < 2.2,
+ QuickCheck >= 2.3 && < 2.7,
haskell-src-exts >= 1.9.6 && < 1.14,
containers >= 0.1 && < 0.6,
unordered-containers == 0.2.*,
@@ -82,7 +83,7 @@ library
process >= 1.0.1.0 && < 1.2,
haskeline >= 0.6.3.2 && < 0.8,
xhtml == 3000.2.*,
- hashable >= 1.1.2.3 && < 1.2,
+ hashable >= 1.1.2.3 && < 1.3,
hashtables == 1.0.*,
geniplate >= 0.6.0.3 && < 0.7,
parallel < 3.3,
@@ -347,7 +348,7 @@ library
executable agda
hs-source-dirs: src/main
main-is: Main.hs
- build-depends: Agda == 2.3.2,
+ build-depends: Agda == 2.3.2.1,
-- Nothing is used from the following package, except
-- for the prelude.
base >= 3 && < 6
diff --git a/dist/build/Agda/Syntax/Parser/Lexer.hs b/dist/build/Agda/Syntax/Parser/Lexer.hs
index 1436d16..101c533 100644
--- a/dist/build/Agda/Syntax/Parser/Lexer.hs
+++ b/dist/build/Agda/Syntax/Parser/Lexer.hs
@@ -61,7 +61,7 @@ alex_check = AlexA# "\xff\xff\x0a\x00\x0b\x00\x0c\x00\x0d\x00\x7d\x00\x2d\x00\x2
alex_deflt :: AlexAddr
alex_deflt = AlexA# "\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\x8e\x00\x48\x00\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\x27\x00\x27\x00\x29\x00\x29\x00\xff\xff\x2b\x00\x2b\x00\x2d\x00\x2d\x00\x32\x00\x32\x00\x35\x00\x35\x00\x38\x00\x38\x00\x3d\x00\x3d\x00\xff\xff\xad\x00\xad\x00\xad\x00\x8e\x00\x8e\x00\x8e\x00\x48\x00\x48\x00\x48\x00\x3e\x00\xff\xff\x3e\x00\x3e\x00\x3e\x00\xff\xff\x48\x00\x48\x00\x48\x00\x48\x00\x48\x00\x48\x00\x48\x00\x48\x00\x48\x00\x48\x00\x48\x00\x48\x00\x48\x00\x48\x00\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\x8e\x00\x8e\x00\x8e\x00\x8e\x00\x8e\x00\x8e\x00\x8e\x00\x8e\x00\x8e\x00\x8e\x00\x8e\x00\x8e\x00\x8e\x00\x8e\x00\x8e\x00\x8e\x00\x8e\x00\x8e\x00\x8e\x00\x8e\x00\x8e\x00\x8e\x00\x8e\x00\x8e\x00\x8e\x00\x8e\x00\x8e\x00\x8e\x00\x8e\x00\x8e\x00\x8e\x00\x8e\x00\x8e\x00\x8e\x00\x8e\x00\x8e\x00\x8e\x00\x8e\x00\x8e\x00\x8e\x00\x8e\x00\x8e\x00\x8e\x00\x8e\x00\x8e\x00\x8e\x00\x8e\x00\x8e\x00\x8e\x00\x8e\x00\x8e\x00\x8e\x00\x8e\x00\x8e\x00\x8e\x00\x8e\x00\x8e\x00\x8e\x00\x8e\x00\x8e\x00\x8e\x00\x8e\x00\x8e\x00\x8e\x00\x8e\x00\x8e\x00\x8e\x00\x8e\x00\x8e\x00\x8e\x00\x8e\x00\x8e\x00\x8e\x00\x8e\x00\x8e\x00\x8e\x00\x8e\x00\x8e\x00\x8e\x00\x8e\x00\x8e\x00\x8e\x00\x8e\x00\x8e\x00\x8e\x00\x8e\x00\x8e\x00\x8e\x00\x8e\x00\xff\xff\xff\xff\xad\x00\xb1\x00\xad\x00\xb1\x00\xb1\x00\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff"#
-alex_accept = listArray (0::Int,408) [[],[(AlexAccPred (alex_action_30) ( not' eof ))],[],[(AlexAcc (alex_action_33))],[],[(AlexAcc (alex_action_32))],[],[(AlexAccPred (alex_action_4) ( eof ))],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[(AlexAccSkip)],[(AlexAccPred (alex_action_0) (alexRightContext 58)),(AlexAccPred (alex_action_1) ( keepComments )),(AlexAccSkip)],[(AlexAccPred (alex_action_1) ( keepComments )),(AlexAccSkip)],[(AlexAccPred (alex_action_1) ( keepComments )),(AlexAccSkip)],[(AlexAccPred (alex_action_1) ( keepComments )),(AlexAccSkip)],[(AlexAccPred (alex_action_1) ( keepComments )),(AlexAccSkip)],[(AlexAccPred (alex_action_1) ( keepComments )),(AlexAccSkip)],[(AlexAccPred (alex_action_1) ( keepComments )),(AlexAccSkip)],[(AlexAccPred (alex_action_1) ( keepComments )),(AlexAccSkip)],[(AlexAccPred (alex_action_1) ( keepComments )),(AlexAccSkip)],[(AlexAccPred (alex_action_1) ( keepComments )),(AlexAccSkip)],[(AlexAccPred (alex_action_1) ( keepComments )),(AlexAccSkip)],[(AlexAccPred (alex_action_1) ( keepComments )),(AlexAccSkip)],[(AlexAccPred (alex_action_1) ( keepComments )),(AlexAccSkip)],[(AlexAccPred (alex_action_1) ( keepComments )),(AlexAccSkip)],[(AlexAccSkip)],[(AlexAccPred (alex_action_5) ( inState code ))],[(AlexAccSkip)],[(AlexAccSkip)],[(AlexAcc (alex_action_8))],[(AlexAcc (alex_action_9))],[(AlexAcc (alex_action_10))],[(AlexAcc (alex_action_11))],[(AlexAcc (alex_action_12))],[(AlexAcc (alex_action_13))],[(AlexAcc (alex_action_14))],[(AlexAcc (alex_action_15))],[(AlexAcc (alex_action_16))],[(AlexAcc (alex_action_17))],[(AlexAcc (alex_action_18))],[(AlexAcc (alex_action_19))],[(AlexAcc (alex_action_20))],[(AlexAcc (alex_action_21))],[(AlexAcc (alex_action_22))],[(AlexAcc (alex_action_23))],[(AlexAcc (alex_action_24))],[(AlexAcc (alex_action_24))],[(AlexAcc (alex_action_24))],[(AlexAcc (alex_action_24))],[(AlexAcc (alex_action_24))],[(AlexAcc (alex_action_24))],[(AlexAcc (alex_action_24))],[(AlexAcc (alex_action_24))],[(AlexAcc (alex_action_24))],[(AlexAcc (alex_action_24))],[(AlexAcc (alex_action_24))],[(AlexAcc (alex_action_24))],[(AlexAcc (alex_action_24))],[(AlexAcc (alex_action_24))],[(AlexAcc (alex_action_24))],[(AlexAcc (alex_action_24))],[(AlexAcc (alex_action_24))],[(AlexAcc (alex_action_24))],[(AlexAcc (alex_action_24))],[(AlexAcc (alex_action_24))],[(AlexAcc (alex_action_24))],[(AlexAcc (alex_action_24))],[(AlexAcc (alex_action_24))],[(AlexAcc (alex_action_24))],[(AlexAcc (alex_action_24))],[(AlexAcc (alex_action_24))],[(AlexAcc (alex_action_24))],[(AlexAcc (alex_action_24))],[(AlexAcc (alex_action_24))],[(AlexAcc (alex_action_24))],[(AlexAcc (alex_action_24))],[(AlexAcc (alex_action_24))],[(AlexAcc (alex_action_24))],[(AlexAcc (alex_action_24))],[(AlexAcc (alex_action_24))],[(AlexAcc (alex_action_24))],[(AlexAcc (alex_action_24))],[(AlexAcc (alex_action_24))],[(AlexAcc (alex_action_24))],[(AlexAcc (alex_action_24))],[(AlexAcc (alex_action_24))],[(AlexAcc (alex_action_24))],[(AlexAcc (alex_action_24))],[(AlexAcc (alex_action_24))],[(AlexAcc (alex_action_24))],[(AlexAcc (alex_action_24))],[(AlexAcc (alex_action_24))],[(AlexAcc (alex_action_24))],[(AlexAcc (alex_action_24))],[(AlexAcc (alex_action_24))],[(AlexAcc (alex_action_24))],[(AlexAcc (alex_action_24))],[(AlexAcc (alex_action_24))],[(AlexAcc (alex_action_24))],[(AlexAcc (alex_action_24))],[(AlexAcc (alex_action_24))],[(AlexAcc (alex_action_24))],[(AlexAcc (alex_action_24))],[(AlexAcc (alex_action_24))],[(AlexAcc (alex_action_24))],[(AlexAcc (alex_action_24))],[(AlexAcc (alex_action_24))],[(AlexAcc (alex_action_24))],[(AlexAcc (alex_action_24))],[(AlexAcc (alex_action_24))],[(AlexAcc (alex_action_24))],[(AlexAcc (alex_action_24))],[(AlexAcc (alex_action_24))],[(AlexAcc (alex_action_24))],[(AlexAcc (alex_action_24))],[(AlexAcc (alex_action_24))],[(AlexAcc (alex_action_24))],[(AlexAcc (alex_action_24))],[(AlexAcc (alex_action_24))],[(AlexAccPred (alex_action_25) ( not' (followedBy '#') ))],[(AlexAccPred (alex_action_25) ( not' (followedBy '#') ))],[(AlexAccPred (alex_action_26) ( keepComments .&&. (followedBy '\n' .||. eof) )),(AlexAccSkipPred ( followedBy '\n' .||. eof ))],[(AlexAccPred (alex_action_26) ( keepComments .&&. (followedBy '\n' .||. eof) )),(AlexAccSkipPred ( followedBy '\n' .||. eof ))],[(AlexAccPred (alex_action_26) ( keepComments .&&. (followedBy '\n' .||. eof) )),(AlexAccSkipPred ( followedBy '\n' .||. eof ))],[(AlexAccPred (alex_action_26) ( keepComments .&&. (followedBy '\n' .||. eof) )),(AlexAccSkipPred ( followedBy '\n' .||. eof ))],[(AlexAccPred (alex_action_26) ( keepComments .&&. (followedBy '\n' .||. eof) )),(AlexAccSkipPred ( followedBy '\n' .||. eof )),(AlexAcc (alex_action_94))],[(AlexAcc (alex_action_28))],[(AlexAccSkip)],[(AlexAccSkip)],[(AlexAcc (alex_action_34))],[(AlexAcc (alex_action_35))],[(AlexAcc (alex_action_36))],[(AlexAcc (alex_action_37))],[(AlexAcc (alex_action_38))],[(AlexAcc (alex_action_39))],[(AlexAcc (alex_action_40))],[(AlexAcc (alex_action_41))],[(AlexAcc (alex_action_42))],[(AlexAcc (alex_action_43))],[(AlexAcc (alex_action_44))],[(AlexAcc (alex_action_45))],[(AlexAcc (alex_action_46))],[(AlexAcc (alex_action_47))],[(AlexAcc (alex_action_48))],[(AlexAcc (alex_action_49))],[(AlexAcc (alex_action_50))],[(AlexAcc (alex_action_51))],[(AlexAcc (alex_action_52))],[(AlexAcc (alex_action_53))],[(AlexAcc (alex_action_54))],[(AlexAcc (alex_action_55))],[(AlexAcc (alex_action_56))],[(AlexAcc (alex_action_57))],[(AlexAcc (alex_action_58))],[(AlexAcc (alex_action_59))],[(AlexAcc (alex_action_60))],[(AlexAcc (alex_action_60))],[(AlexAcc (alex_action_60))],[(AlexAcc (alex_action_61))],[(AlexAcc (alex_action_62))],[(AlexAcc (alex_action_63))],[(AlexAcc (alex_action_64))],[(AlexAcc (alex_action_65))],[(AlexAcc (alex_action_66))],[(AlexAcc (alex_action_67))],[(AlexAcc (alex_action_68))],[(AlexAcc (alex_action_69))],[(AlexAcc (alex_action_70))],[(AlexAcc (alex_action_71))],[(AlexAcc (alex_action_72))],[(AlexAcc (alex_action_73))],[(AlexAcc (alex_action_74))],[(AlexAcc (alex_action_75))],[(AlexAcc (alex_action_76))],[(AlexAcc (alex_action_77))],[(AlexAcc (alex_action_78))],[(AlexAcc (alex_action_79))],[(AlexAcc (alex_action_80))],[(AlexAcc (alex_action_81))],[(AlexAcc (alex_action_82))],[(AlexAcc (alex_action_83))],[(AlexAcc (alex_action_84))],[(AlexAcc (alex_action_85))],[(AlexAcc (alex_action_86))],[(AlexAccPred (alex_action_87) (alexRightContext 59))],[(AlexAcc (alex_action_88))],[(AlexAcc (alex_action_89))],[(AlexAcc (alex_action_90))],[(AlexAcc (alex_action_91))],[(AlexAcc (alex_action_92))],[(AlexAcc (alex_action_92))],[(AlexAcc (alex_action_92))],[(AlexAcc (alex_action_92))],[(AlexAcc (alex_action_92))],[(AlexAcc (alex_action_93))],[(AlexAcc (alex_action_93))],[(AlexAcc (alex_action_93))],[(AlexAcc (alex_action_93))],[(AlexAcc (alex_action_93))],[(AlexAcc (alex_action_93))],[(AlexAcc (alex_action_93))],[(AlexAcc (alex_action_93))],[(AlexAcc (alex_action_94))],[(AlexAcc (alex_action_94))],[(AlexAcc (alex_action_94))],[(AlexAcc (alex_action_94))],[(AlexAcc (alex_action_94))],[(AlexAcc (alex_action_94))],[(AlexAcc (alex_action_94))],[(AlexAcc (alex_action_94))],[(AlexAcc (alex_action_94))],[(AlexAcc (alex_action_94))],[(AlexAcc (alex_action_94))],[(AlexAcc (alex_action_94))],[(AlexAcc (alex_action_94))],[(AlexAcc (alex_action_94))],[(AlexAcc (alex_action_94))],[(AlexAcc (alex_action_94))],[(AlexAcc (alex_action_94))],[(AlexAcc (alex_action_94))],[(AlexAcc (alex_action_94))],[(AlexAcc (alex_action_94))],[(AlexAcc (alex_action_94))],[(AlexAcc (alex_action_94))],[(AlexAcc (alex_action_94))],[(AlexAcc (alex_action_94))],[(AlexAcc (alex_action_94))],[(AlexAcc (alex_action_94))],[(AlexAcc (alex_action_94))],[(AlexAcc (alex_action_94))],[(AlexAcc (alex_action_94))],[(AlexAcc (alex_action_94))],[(AlexAcc (alex_action_94))],[(AlexAcc (alex_action_94))],[(AlexAcc (alex_action_94))],[(AlexAcc (alex_action_94))],[(AlexAcc (alex_action_94))],[(AlexAcc (alex_action_94))],[(AlexAcc (alex_action_94))],[(AlexAcc (alex_action_94))],[(AlexAcc (alex_action_94))],[(AlexAcc (alex_action_94))],[(AlexAcc (alex_action_94))],[(AlexAcc (alex_action_94))],[(AlexAcc (alex_action_94))],[(AlexAcc (alex_action_94))],[(AlexAcc (alex_action_94))],[(AlexAcc (alex_action_94))],[(AlexAcc (alex_action_94))],[(AlexAcc (alex_action_94))],[(AlexAcc (alex_action_94))],[(AlexAcc (alex_action_94))],[(AlexAcc (alex_action_94))],[(AlexAcc (alex_action_94))],[(AlexAcc (alex_action_94))],[(AlexAcc (alex_action_94))],[(AlexAcc (alex_action_94))],[(AlexAcc (alex_action_94))],[(AlexAcc (alex_action_94))],[(AlexAcc (alex_action_94))],[(AlexAcc (alex_action_94))],[(AlexAcc (alex_action_94))],[(AlexAcc (alex_action_94))],[(AlexAcc (alex_action_94))],[(AlexAcc (alex_action_94))],[(AlexAcc (alex_action_94))],[(AlexAcc (alex_action_94))],[(AlexAcc (alex_action_94))],[(AlexAcc (alex_action_94))],[(AlexAcc (alex_action_94))],[(AlexAcc (alex_action_94))],[(AlexAcc (alex_action_94))],[(AlexAcc (alex_action_94))],[(AlexAcc (alex_action_94))],[(AlexAcc (alex_action_94))],[(AlexAcc (alex_action_94))],[(AlexAcc (alex_action_94))],[(AlexAcc (alex_action_94))],[(AlexAcc (alex_action_94))],[(AlexAcc (alex_action_94))],[(AlexAcc (alex_action_94))],[(AlexAcc (alex_action_94))],[(AlexAcc (alex_action_94))],[(AlexAcc (alex_action_94))],[(AlexAcc (alex_action_94))],[(AlexAcc (alex_action_94))],[(AlexAcc (alex_action_94))],[(AlexAcc (alex_action_94))],[(AlexAcc (alex_action_94))],[(AlexAcc (alex_action_94))],[(AlexAcc (alex_action_94))],[(AlexAcc (alex_action_94))],[(AlexAcc (alex_action_94))],[(AlexAcc (alex_action_94))],[(AlexAcc (alex_action_94))],[(AlexAcc (alex_action_94))],[(AlexAcc (alex_action_94))],[(AlexAcc (alex_action_94))],[(AlexAcc (alex_action_94))],[(AlexAcc (alex_action_94))],[(AlexAcc (alex_action_94))],[(AlexAcc (alex_action_94))],[(AlexAcc (alex_action_94))],[(AlexAcc (alex_action_94))],[(AlexAcc (alex_action_94))],[(AlexAcc (alex_action_94))],[(AlexAcc (alex_action_94))],[(AlexAcc (alex_action_94))],[(AlexAcc (alex_action_94))],[(AlexAcc (alex_action_94))],[(AlexAcc (alex_action_94))],[(AlexAcc (alex_action_94))],[(AlexAcc (alex_action_94))],[(AlexAcc (alex_action_94))],[(AlexAcc (alex_action_94))],[(AlexAcc (alex_action_94))],[(AlexAcc (alex_action_94))],[(AlexAcc (alex_action_94))],[(AlexAcc (alex_action_94))],[(AlexAcc (alex_action_94))],[(AlexAcc (alex_action_94))],[(AlexAcc (alex_action_94))],[(AlexAcc (alex_action_94))],[(AlexAcc (alex_action_94))],[(AlexAcc (alex_action_94))],[(AlexAcc (alex_action_94))],[(AlexAcc (alex_action_94))],[(AlexAcc (alex_action_94))],[(AlexAcc (alex_action_94))],[(AlexAcc (alex_action_94))],[(AlexAcc (alex_action_94))],[(AlexAcc (alex_action_94))],[(AlexAcc (alex_action_94))],[(AlexAcc (alex_action_94))],[(AlexAcc (alex_action_94))],[(AlexAcc (alex_action_94))],[(AlexAcc (alex_action_94))],[(AlexAcc (alex_action_94))],[(AlexAcc (alex_action_94))],[(AlexAcc (alex_action_94))],[(AlexAcc (alex_action_94))],[(AlexAcc (alex_action_94))],[(AlexAcc (alex_action_94))],[(AlexAcc (alex_action_94))],[(AlexAcc (alex_action_94))],[(AlexAcc (alex_action_94))],[(AlexAcc (alex_action_94))],[(AlexAcc (alex_action_94))],[(AlexAcc (alex_action_94))],[(AlexAcc (alex_action_94))],[(AlexAcc (alex_action_94))],[(AlexAcc (alex_action_94))],[(AlexAcc (alex_action_94))],[(AlexAcc (alex_action_94))],[(AlexAcc (alex_action_94))],[(AlexAcc (alex_action_94))],[(AlexAcc (alex_action_94))]]
+alex_accept = listArray (0::Int,408) [AlexAccNone,AlexAccPred (alex_action_30) ( not' eof )(AlexAccNone),AlexAccNone,AlexAcc (alex_action_33),AlexAccNone,AlexAcc (alex_action_32),AlexAccNone,AlexAccPred (alex_action_4) ( eof )(AlexAccNone),AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccNone,AlexAccSkip,AlexAccPred (alex_action_0) (alexRightContext 58)(AlexAccPred (alex_action_1) ( keepComments )(AlexAccSkip)),AlexAccPred (alex_action_1) ( keepComments )(AlexAccSkip),AlexAccPred (alex_action_1) ( keepComments )(AlexAccSkip),AlexAccPred (alex_action_1) ( keepComments )(AlexAccSkip),AlexAccPred (alex_action_1) ( keepComments )(AlexAccSkip),AlexAccPred (alex_action_1) ( keepComments )(AlexAccSkip),AlexAccPred (alex_action_1) ( keepComments )(AlexAccSkip),AlexAccPred (alex_action_1) ( keepComments )(AlexAccSkip),AlexAccPred (alex_action_1) ( keepComments )(AlexAccSkip),AlexAccPred (alex_action_1) ( keepComments )(AlexAccSkip),AlexAccPred (alex_action_1) ( keepComments )(AlexAccSkip),AlexAccPred (alex_action_1) ( keepComments )(AlexAccSkip),AlexAccPred (alex_action_1) ( keepComments )(AlexAccSkip),AlexAccPred (alex_action_1) ( keepComments )(AlexAccSkip),AlexAccSkip,AlexAccPred (alex_action_5) ( inState code )(AlexAccNone),AlexAccSkip,AlexAccSkip,AlexAcc (alex_action_8),AlexAcc (alex_action_9),AlexAcc (alex_action_10),AlexAcc (alex_action_11),AlexAcc (alex_action_12),AlexAcc (alex_action_13),AlexAcc (alex_action_14),AlexAcc (alex_action_15),AlexAcc (alex_action_16),AlexAcc (alex_action_17),AlexAcc (alex_action_18),AlexAcc (alex_action_19),AlexAcc (alex_action_20),AlexAcc (alex_action_21),AlexAcc (alex_action_22),AlexAcc (alex_action_23),AlexAcc (alex_action_24),AlexAcc (alex_action_24),AlexAcc (alex_action_24),AlexAcc (alex_action_24),AlexAcc (alex_action_24),AlexAcc (alex_action_24),AlexAcc (alex_action_24),AlexAcc (alex_action_24),AlexAcc (alex_action_24),AlexAcc (alex_action_24),AlexAcc (alex_action_24),AlexAcc (alex_action_24),AlexAcc (alex_action_24),AlexAcc (alex_action_24),AlexAcc (alex_action_24),AlexAcc (alex_action_24),AlexAcc (alex_action_24),AlexAcc (alex_action_24),AlexAcc (alex_action_24),AlexAcc (alex_action_24),AlexAcc (alex_action_24),AlexAcc (alex_action_24),AlexAcc (alex_action_24),AlexAcc (alex_action_24),AlexAcc (alex_action_24),AlexAcc (alex_action_24),AlexAcc (alex_action_24),AlexAcc (alex_action_24),AlexAcc (alex_action_24),AlexAcc (alex_action_24),AlexAcc (alex_action_24),AlexAcc (alex_action_24),AlexAcc (alex_action_24),AlexAcc (alex_action_24),AlexAcc (alex_action_24),AlexAcc (alex_action_24),AlexAcc (alex_action_24),AlexAcc (alex_action_24),AlexAcc (alex_action_24),AlexAcc (alex_action_24),AlexAcc (alex_action_24),AlexAcc (alex_action_24),AlexAcc (alex_action_24),AlexAcc (alex_action_24),AlexAcc (alex_action_24),AlexAcc (alex_action_24),AlexAcc (alex_action_24),AlexAcc (alex_action_24),AlexAcc (alex_action_24),AlexAcc (alex_action_24),AlexAcc (alex_action_24),AlexAcc (alex_action_24),AlexAcc (alex_action_24),AlexAcc (alex_action_24),AlexAcc (alex_action_24),AlexAcc (alex_action_24),AlexAcc (alex_action_24),AlexAcc (alex_action_24),AlexAcc (alex_action_24),AlexAcc (alex_action_24),AlexAcc (alex_action_24),AlexAcc (alex_action_24),AlexAcc (alex_action_24),AlexAcc (alex_action_24),AlexAcc (alex_action_24),AlexAcc (alex_action_24),AlexAcc (alex_action_24),AlexAcc (alex_action_24),AlexAcc (alex_action_24),AlexAcc (alex_action_24),AlexAcc (alex_action_24),AlexAcc (alex_action_24),AlexAcc (alex_action_24),AlexAcc (alex_action_24),AlexAccPred (alex_action_25) ( not' (followedBy '#') )(AlexAccNone),AlexAccPred (alex_action_25) ( not' (followedBy '#') )(AlexAccNone),AlexAccPred (alex_action_26) ( keepComments .&&. (followedBy '\n' .||. eof) )(AlexAccSkipPred ( followedBy '\n' .||. eof )(AlexAccNone)),AlexAccPred (alex_action_26) ( keepComments .&&. (followedBy '\n' .||. eof) )(AlexAccSkipPred ( followedBy '\n' .||. eof )(AlexAccNone)),AlexAccPred (alex_action_26) ( keepComments .&&. (followedBy '\n' .||. eof) )(AlexAccSkipPred ( followedBy '\n' .||. eof )(AlexAccNone)),AlexAccPred (alex_action_26) ( keepComments .&&. (followedBy '\n' .||. eof) )(AlexAccSkipPred ( followedBy '\n' .||. eof )(AlexAccNone)),AlexAccPred (alex_action_26) ( keepComments .&&. (followedBy '\n' .||. eof) )(AlexAccSkipPred ( followedBy '\n' .||. eof )(AlexAcc (alex_action_94))),AlexAcc (alex_action_28),AlexAccSkip,AlexAccSkip,AlexAcc (alex_action_34),AlexAcc (alex_action_35),AlexAcc (alex_action_36),AlexAcc (alex_action_37),AlexAcc (alex_action_38),AlexAcc (alex_action_39),AlexAcc (alex_action_40),AlexAcc (alex_action_41),AlexAcc (alex_action_42),AlexAcc (alex_action_43),AlexAcc (alex_action_44),AlexAcc (alex_action_45),AlexAcc (alex_action_46),AlexAcc (alex_action_47),AlexAcc (alex_action_48),AlexAcc (alex_action_49),AlexAcc (alex_action_50),AlexAcc (alex_action_51),AlexAcc (alex_action_52),AlexAcc (alex_action_53),AlexAcc (alex_action_54),AlexAcc (alex_action_55),AlexAcc (alex_action_56),AlexAcc (alex_action_57),AlexAcc (alex_action_58),AlexAcc (alex_action_59),AlexAcc (alex_action_60),AlexAcc (alex_action_60),AlexAcc (alex_action_60),AlexAcc (alex_action_61),AlexAcc (alex_action_62),AlexAcc (alex_action_63),AlexAcc (alex_action_64),AlexAcc (alex_action_65),AlexAcc (alex_action_66),AlexAcc (alex_action_67),AlexAcc (alex_action_68),AlexAcc (alex_action_69),AlexAcc (alex_action_70),AlexAcc (alex_action_71),AlexAcc (alex_action_72),AlexAcc (alex_action_73),AlexAcc (alex_action_74),AlexAcc (alex_action_75),AlexAcc (alex_action_76),AlexAcc (alex_action_77),AlexAcc (alex_action_78),AlexAcc (alex_action_79),AlexAcc (alex_action_80),AlexAcc (alex_action_81),AlexAcc (alex_action_82),AlexAcc (alex_action_83),AlexAcc (alex_action_84),AlexAcc (alex_action_85),AlexAcc (alex_action_86),AlexAccPred (alex_action_87) (alexRightContext 59)(AlexAccNone),AlexAcc (alex_action_88),AlexAcc (alex_action_89),AlexAcc (alex_action_90),AlexAcc (alex_action_91),AlexAcc (alex_action_92),AlexAcc (alex_action_92),AlexAcc (alex_action_92),AlexAcc (alex_action_92),AlexAcc (alex_action_92),AlexAcc (alex_action_93),AlexAcc (alex_action_93),AlexAcc (alex_action_93),AlexAcc (alex_action_93),AlexAcc (alex_action_93),AlexAcc (alex_action_93),AlexAcc (alex_action_93),AlexAcc (alex_action_93),AlexAcc (alex_action_94),AlexAcc (alex_action_94),AlexAcc (alex_action_94),AlexAcc (alex_action_94),AlexAcc (alex_action_94),AlexAcc (alex_action_94),AlexAcc (alex_action_94),AlexAcc (alex_action_94),AlexAcc (alex_action_94),AlexAcc (alex_action_94),AlexAcc (alex_action_94),AlexAcc (alex_action_94),AlexAcc (alex_action_94),AlexAcc (alex_action_94),AlexAcc (alex_action_94),AlexAcc (alex_action_94),AlexAcc (alex_action_94),AlexAcc (alex_action_94),AlexAcc (alex_action_94),AlexAcc (alex_action_94),AlexAcc (alex_action_94),AlexAcc (alex_action_94),AlexAcc (alex_action_94),AlexAcc (alex_action_94),AlexAcc (alex_action_94),AlexAcc (alex_action_94),AlexAcc (alex_action_94),AlexAcc (alex_action_94),AlexAcc (alex_action_94),AlexAcc (alex_action_94),AlexAcc (alex_action_94),AlexAcc (alex_action_94),AlexAcc (alex_action_94),AlexAcc (alex_action_94),AlexAcc (alex_action_94),AlexAcc (alex_action_94),AlexAcc (alex_action_94),AlexAcc (alex_action_94),AlexAcc (alex_action_94),AlexAcc (alex_action_94),AlexAcc (alex_action_94),AlexAcc (alex_action_94),AlexAcc (alex_action_94),AlexAcc (alex_action_94),AlexAcc (alex_action_94),AlexAcc (alex_action_94),AlexAcc (alex_action_94),AlexAcc (alex_action_94),AlexAcc (alex_action_94),AlexAcc (alex_action_94),AlexAcc (alex_action_94),AlexAcc (alex_action_94),AlexAcc (alex_action_94),AlexAcc (alex_action_94),AlexAcc (alex_action_94),AlexAcc (alex_action_94),AlexAcc (alex_action_94),AlexAcc (alex_action_94),AlexAcc (alex_action_94),AlexAcc (alex_action_94),AlexAcc (alex_action_94),AlexAcc (alex_action_94),AlexAcc (alex_action_94),AlexAcc (alex_action_94),AlexAcc (alex_action_94),AlexAcc (alex_action_94),AlexAcc (alex_action_94),AlexAcc (alex_action_94),AlexAcc (alex_action_94),AlexAcc (alex_action_94),AlexAcc (alex_action_94),AlexAcc (alex_action_94),AlexAcc (alex_action_94),AlexAcc (alex_action_94),AlexAcc (alex_action_94),AlexAcc (alex_action_94),AlexAcc (alex_action_94),AlexAcc (alex_action_94),AlexAcc (alex_action_94),AlexAcc (alex_action_94),AlexAcc (alex_action_94),AlexAcc (alex_action_94),AlexAcc (alex_action_94),AlexAcc (alex_action_94),AlexAcc (alex_action_94),AlexAcc (alex_action_94),AlexAcc (alex_action_94),AlexAcc (alex_action_94),AlexAcc (alex_action_94),AlexAcc (alex_action_94),AlexAcc (alex_action_94),AlexAcc (alex_action_94),AlexAcc (alex_action_94),AlexAcc (alex_action_94),AlexAcc (alex_action_94),AlexAcc (alex_action_94),AlexAcc (alex_action_94),AlexAcc (alex_action_94),AlexAcc (alex_action_94),AlexAcc (alex_action_94),AlexAcc (alex_action_94),AlexAcc (alex_action_94),AlexAcc (alex_action_94),AlexAcc (alex_action_94),AlexAcc (alex_action_94),AlexAcc (alex_action_94),AlexAcc (alex_action_94),AlexAcc (alex_action_94),AlexAcc (alex_action_94),AlexAcc (alex_action_94),AlexAcc (alex_action_94),AlexAcc (alex_action_94),AlexAcc (alex_action_94),AlexAcc (alex_action_94),AlexAcc (alex_action_94),AlexAcc (alex_action_94),AlexAcc (alex_action_94),AlexAcc (alex_action_94),AlexAcc (alex_action_94),AlexAcc (alex_action_94),AlexAcc (alex_action_94),AlexAcc (alex_action_94),AlexAcc (alex_action_94),AlexAcc (alex_action_94),AlexAcc (alex_action_94),AlexAcc (alex_action_94),AlexAcc (alex_action_94),AlexAcc (alex_action_94),AlexAcc (alex_action_94),AlexAcc (alex_action_94),AlexAcc (alex_action_94),AlexAcc (alex_action_94),AlexAcc (alex_action_94),AlexAcc (alex_action_94),AlexAcc (alex_action_94),AlexAcc (alex_action_94),AlexAcc (alex_action_94),AlexAcc (alex_action_94),AlexAcc (alex_action_94),AlexAcc (alex_action_94),AlexAcc (alex_action_94),AlexAcc (alex_action_94),AlexAcc (alex_action_94),AlexAcc (alex_action_94),AlexAcc (alex_action_94),AlexAcc (alex_action_94),AlexAcc (alex_action_94),AlexAcc (alex_action_94),AlexAcc (alex_action_94),AlexAcc (alex_action_94),AlexAcc (alex_action_94),AlexAcc (alex_action_94),AlexAcc (alex_action_94),AlexAcc (alex_action_94),AlexAcc (alex_action_94)]
{-# LINE 212 "src/full/Agda/Syntax/Parser/Lexer.x" #-}
@@ -237,7 +237,7 @@ alex_action_94 = identifier
{-# LINE 1 "templates/GenericTemplate.hs" #-}
{-# LINE 1 "templates/GenericTemplate.hs" #-}
{-# LINE 1 "<built-in>" #-}
-{-# LINE 1 "<command line>" #-}
+{-# LINE 1 "<command-line>" #-}
{-# LINE 1 "templates/GenericTemplate.hs" #-}
-- -----------------------------------------------------------------------------
-- ALEX TEMPLATE
@@ -248,9 +248,9 @@ alex_action_94 = identifier
-- -----------------------------------------------------------------------------
-- INTERNALS and main scanner engine
-{-# LINE 37 "templates/GenericTemplate.hs" #-}
+{-# LINE 35 "templates/GenericTemplate.hs" #-}
-{-# LINE 47 "templates/GenericTemplate.hs" #-}
+{-# LINE 45 "templates/GenericTemplate.hs" #-}
data AlexAddr = AlexA# Addr#
@@ -281,14 +281,14 @@ alexIndexInt32OffAddr (AlexA# arr) off =
#ifdef WORDS_BIGENDIAN
narrow32Int# i
where
- !i = word2Int# ((b3 `uncheckedShiftL#` 24#) `or#`
+ i = word2Int# ((b3 `uncheckedShiftL#` 24#) `or#`
(b2 `uncheckedShiftL#` 16#) `or#`
(b1 `uncheckedShiftL#` 8#) `or#` b0)
- !b3 = int2Word# (ord# (indexCharOffAddr# arr (off' +# 3#)))
- !b2 = int2Word# (ord# (indexCharOffAddr# arr (off' +# 2#)))
- !b1 = int2Word# (ord# (indexCharOffAddr# arr (off' +# 1#)))
- !b0 = int2Word# (ord# (indexCharOffAddr# arr off'))
- !off' = off *# 4#
+ b3 = int2Word# (ord# (indexCharOffAddr# arr (off' +# 3#)))
+ b2 = int2Word# (ord# (indexCharOffAddr# arr (off' +# 2#)))
+ b1 = int2Word# (ord# (indexCharOffAddr# arr (off' +# 1#)))
+ b0 = int2Word# (ord# (indexCharOffAddr# arr off'))
+ off' = off *# 4#
#else
indexInt32OffAddr# arr off
#endif
@@ -363,35 +363,40 @@ alex_scan_tkn user orig_input len input s last_acc =
- let
- (base) = alexIndexInt32OffAddr alex_base s
- ((I# (ord_c))) = fromIntegral c
- (offset) = (base +# ord_c)
- (check) = alexIndexInt16OffAddr alex_check offset
+ case fromIntegral c of { (I# (ord_c)) ->
+ let
+ base = alexIndexInt32OffAddr alex_base s
+ offset = (base +# ord_c)
+ check = alexIndexInt16OffAddr alex_check offset
- (new_s) = if (offset >=# 0#) && (check ==# ord_c)
+ new_s = if (offset >=# 0#) && (check ==# ord_c)
then alexIndexInt16OffAddr alex_table offset
else alexIndexInt16OffAddr alex_deflt s
in
- case new_s of
+ case new_s of
-1# -> (new_acc, input)
-- on an error, we want to keep the input *before* the
-- character that failed, not after.
_ -> alex_scan_tkn user orig_input (if c < 0x80 || c >= 0xC0 then (len +# 1#) else len)
-- note that the length is increased ONLY if this is the 1st byte in a char encoding)
new_input new_s new_acc
-
+ }
where
- check_accs [] = last_acc
- check_accs (AlexAcc a : _) = AlexLastAcc a input (I# (len))
- check_accs (AlexAccSkip : _) = AlexLastSkip input (I# (len))
- check_accs (AlexAccPred a predx : rest)
+ check_accs (AlexAccNone) = last_acc
+ check_accs (AlexAcc a ) = AlexLastAcc a input (I# (len))
+ check_accs (AlexAccSkip) = AlexLastSkip input (I# (len))
+
+ check_accs (AlexAccPred a predx rest)
| predx user orig_input (I# (len)) input
= AlexLastAcc a input (I# (len))
- check_accs (AlexAccSkipPred predx : rest)
+ | otherwise
+ = check_accs rest
+ check_accs (AlexAccSkipPred predx rest)
| predx user orig_input (I# (len)) input
= AlexLastSkip input (I# (len))
- check_accs (_ : rest) = check_accs rest
+ | otherwise
+ = check_accs rest
+
data AlexLastAcc a
= AlexNone
@@ -404,10 +409,12 @@ instance Functor AlexLastAcc where
fmap f (AlexLastSkip x y) = AlexLastSkip x y
data AlexAcc a user
- = AlexAcc a
+ = AlexAccNone
+ | AlexAcc a
| AlexAccSkip
- | AlexAccPred a (AlexAccPred user)
- | AlexAccSkipPred (AlexAccPred user)
+
+ | AlexAccPred a (AlexAccPred user) (AlexAcc a user)
+ | AlexAccSkipPred (AlexAccPred user) (AlexAcc a user)
type AlexAccPred user = user -> AlexInput -> Int -> AlexInput -> Bool
@@ -434,5 +441,6 @@ alexRightContext (I# (sc)) user _ _ input =
-- match when checking the right context, just
-- the first match will do.
+
-- used by wrappers
iUnbox (I# (i)) = i
diff --git a/dist/build/Agda/Syntax/Parser/Parser.hs b/dist/build/Agda/Syntax/Parser/Parser.hs
index 0a4f0a2..920e056 100644
--- a/dist/build/Agda/Syntax/Parser/Parser.hs
+++ b/dist/build/Agda/Syntax/Parser/Parser.hs
@@ -51,7 +51,7 @@ import Agda.Utils.Tuple
import qualified Data.Array as Happy_Data_Array
import qualified GHC.Exts as Happy_GHC_Exts
--- parser produced by Happy Version 1.18.8
+-- parser produced by Happy Version 1.18.10
newtype HappyAbsSyn t10 t11 t12 t30 t33 t36 t37 t38 t42 t43 t70 = HappyAbsSyn HappyAny
#if __GLASGOW_HASKELL__ >= 607
@@ -5044,7 +5044,7 @@ tests = runTests "Agda.Syntax.Parser.Parser"
{-# LINE 1 "templates/GenericTemplate.hs" #-}
{-# LINE 1 "templates/GenericTemplate.hs" #-}
{-# LINE 1 "<built-in>" #-}
-{-# LINE 1 "<command line>" #-}
+{-# LINE 1 "<command-line>" #-}
{-# LINE 1 "templates/GenericTemplate.hs" #-}
-- Id: GenericTemplate.hs,v 1.26 2005/01/14 14:47:22 simonmar Exp
diff --git a/doc/release-notes/2-3-2-1.txt b/doc/release-notes/2-3-2-1.txt
new file mode 100644
index 0000000..a8b646f
--- /dev/null
+++ b/doc/release-notes/2-3-2-1.txt
@@ -0,0 +1,18 @@
+------------------------------------------------------------------------
+-- Release notes for Agda 2 version 2.3.2.1
+------------------------------------------------------------------------
+
+Important changes since 2.3.2:
+
+Installation
+============
+
+* Made it possible to compile Agda with more recent versions of
+ hashable, QuickCheck and Win32.
+
+* Excluded mtl-2.1.
+
+Type checking
+=============
+
+* Fixed bug in the termination checker (issue 754).
diff --git a/src/data/emacs-mode/agda2-mode.el b/src/data/emacs-mode/agda2-mode.el
index b4ed667..edc22ff 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.3.2"
+(defvar agda2-version "2.3.2.1"
"The version of the Agda mode.
Note that the same version of the Agda executable must be used.")
diff --git a/src/full/Agda/Syntax/Abstract/Name.hs b/src/full/Agda/Syntax/Abstract/Name.hs
index 03ad29b..31a0f3c 100644
--- a/src/full/Agda/Syntax/Abstract/Name.hs
+++ b/src/full/Agda/Syntax/Abstract/Name.hs
@@ -239,8 +239,8 @@ instance Show Name where
show x = show (nameConcrete x) -- ++ "|" ++ show (nameId x)
instance Hashable Name where
- {-# INLINE hash #-}
- hash = hash . nameId
+ {-# INLINE hashWithSalt #-}
+ hashWithSalt salt = (hashWithSalt salt) . nameId
instance Show QName where
show q = concat $ intersperse "." $ map show $ qnameToList q
@@ -255,8 +255,8 @@ instance Ord QName where
compare = compare `on` qnameName
instance Hashable QName where
- {-# INLINE hash #-}
- hash = hash . qnameName
+ {-# INLINE hashWithSalt #-}
+ hashWithSalt salt = (hashWithSalt salt) . qnameName
instance HasRange Name where
getRange = getRange . nameConcrete
diff --git a/src/full/Agda/Syntax/Common.hs b/src/full/Agda/Syntax/Common.hs
index 6c9e357..40dff4d 100644
--- a/src/full/Agda/Syntax/Common.hs
+++ b/src/full/Agda/Syntax/Common.hs
@@ -272,8 +272,8 @@ instance Enum NameId where
fromEnum (NameId n _) = fromIntegral n
instance Hashable NameId where
- {-# INLINE hash #-}
- hash (NameId n m) = hash (n, m)
+ {-# INLINE hashWithSalt #-}
+ hashWithSalt salt (NameId n m) = hashWithSalt salt (n, m)
newtype Constr a = Constr a
diff --git a/src/full/Agda/Termination/CallGraph.hs b/src/full/Agda/Termination/CallGraph.hs
index dc1b072..46db0cb 100644
--- a/src/full/Agda/Termination/CallGraph.hs
+++ b/src/full/Agda/Termination/CallGraph.hs
@@ -213,7 +213,8 @@ This makes order multiplication associative.
-}
collapse :: (?cutoff :: Int) => Matrix Integer Order -> Order
-collapse m = case (toLists (Matrix.transpose m)) of
+collapse m = -- if not $ Matrix.matrixInvariant m then __IMPOSSIBLE__ else
+ case toLists $ Matrix.transpose m of
[] -> __IMPOSSIBLE__ -- This can never happen if order matrices are generated by the smart constructor
m' -> foldl1 (.*.) $ map (foldl1 maxO) m'
diff --git a/src/full/Agda/Termination/SparseMatrix.hs b/src/full/Agda/Termination/SparseMatrix.hs
index 06b28cd..fe651f9 100644
--- a/src/full/Agda/Termination/SparseMatrix.hs
+++ b/src/full/Agda/Termination/SparseMatrix.hs
@@ -40,8 +40,10 @@ module Agda.Termination.SparseMatrix
import Data.Array
import qualified Data.List as List
-import Agda.Utils.Pretty hiding (isEmpty)
+import Data.Maybe
import Data.Monoid
+
+import Agda.Utils.Pretty hiding (isEmpty)
import Agda.Utils.QuickCheck
import Agda.Utils.TestHelpers
import Agda.Termination.Semiring (HasZero(..), SemiRing, Semiring)
@@ -129,12 +131,12 @@ strictlySorted (MIx i j) ((MIx i' j', b) : l) =
(i < i' || i == i' && j < j' ) && strictlySorted (MIx i' j') b
-}
-instance (Ord i, Integral i, Enum i, Show i, Show b, HasZero b) => Show (Matrix i b) where
+instance (Ord i, Integral i, Enum i, Ix i, Show i, Show b, HasZero b) => Show (Matrix i b) where
showsPrec _ m =
showString "Agda.Termination.Matrix.fromLists " . shows (size m) .
showString " " . shows (toLists m)
-instance (Show i, Integral i, HasZero b, Pretty b) =>
+instance (Show i, Integral i, Ix i, HasZero b, Pretty b) =>
Pretty (Matrix i b) where
pretty = vcat . map (hsep . map pretty) . toLists
@@ -142,7 +144,7 @@ instance (Arbitrary i, Num i, Integral i, Arbitrary b, HasZero b)
=> Arbitrary (Matrix i b) where
arbitrary = matrix =<< arbitrary
-instance (Show i, Ord i, Integral i, Enum i, CoArbitrary b, HasZero b) => CoArbitrary (Matrix i b) where
+instance (Show i, Ord i, Integral i, Enum i, Ix i, CoArbitrary b, HasZero b) => CoArbitrary (Matrix i b) where
coarbitrary m = coarbitrary (toLists m)
@@ -214,18 +216,20 @@ blowUpSparseVec zero n l = aux 1 l
| otherwise = zero : aux (i+1) []
aux i ((j,b):l) | i <= n && j == i = b : aux (succ i) l
aux i ((j,b):l) | i <= n && j >= i = zero : aux (succ i) ((j,b):l)
- aux i l = error $ "blowUpSparseVec (n = " ++ show n ++ ") aux i=" ++ show i ++ " j=" ++ show (fst (head l)) ++ " length l = " ++ show (length l)
--- __IMPOSSIBLE__
+ aux i l = __IMPOSSIBLE__
+ -- error $ "blowUpSparseVec (n = " ++ show n ++ ") aux i=" ++ show i ++ " j=" ++ show (fst (head l)) ++ " length l = " ++ show (length l)
-- | Converts a matrix to a list of row lists.
-toLists :: (Show i, Ord i, Integral i, Enum i, HasZero b) => Matrix i b -> [[b]]
-toLists m = blowUpSparseVec emptyRow (rows sz) $
- map (\ (i,r) -> (i, blowUpSparseVec zeroElement (cols sz) r)) $ toSparseRows m
--- [ [ maybe zeroElement id $ lookup (MIx { row = r, col = c }) (unM m)
--- | c <- [1 .. cols sz] ] | r <- [1 .. rows sz] ]
- where sz = size m
- emptyRow = take (fromIntegral (cols sz)) $ repeat zeroElement
+toLists :: (Show i, Ord i, Integral i, Enum i, Ix i, HasZero b) => Matrix i b -> [[b]]
+toLists m = -- if not $ matrixInvariant m then __IMPOSSIBLE__ else
+ blowUpSparseVec emptyRow nr $
+ map (\ (i,r) -> (i, blowUpSparseVec zeroElement nc r)) $ toSparseRows m
+ where
+ sz = size m
+ nr = rows sz
+ nc = cols sz
+ emptyRow = take (fromIntegral nc) $ repeat zeroElement
prop_fromLists_toLists :: TM -> Bool
prop_fromLists_toLists m = fromLists (size m) (toLists m) == m
@@ -276,12 +280,24 @@ transpose m = M { size = transposeSize (size m)
, unM = List.sortBy (\ (i,a) (j,b) -> compare i j) $
map (\(MIx i j, b) -> (MIx j i, b)) $ unM m }
+prop_transpose :: TM -> Bool
+prop_transpose m = matrixInvariant m' && m == transpose m'
+ where m' = transpose m
+
-- | @'add' (+) m1 m2@ adds @m1@ and @m2 at . Uses @(+)@ to add values.
--
--- Precondition: @'size' m1 == 'size' m2 at .
+-- No longer precondition: @'size' m1 == 'size' m2 at .
add :: (Ord i) => (a -> a -> a) -> Matrix i a -> Matrix i a -> Matrix i a
-add plus m1 m2 = M (size m1) $ mergeAssocWith plus (unM m1) (unM m2)
+add plus m1 m2 = M (supSize m1 m2) $ mergeAssocWith plus (unM m1) (unM m2)
+
+-- | Compute the matrix size of the union of two matrices.
+supSize m1 m2 = Size { rows = r, cols = c }
+ where
+ sz1 = size m1
+ sz2 = size m2
+ r = max (rows sz1) (rows sz2)
+ c = max (cols sz1) (cols sz2)
-- | assoc list union
mergeAssocWith :: (Ord i) => (a -> a -> a) -> [(i,a)] -> [(i,a)] -> [(i,a)]
@@ -295,10 +311,18 @@ mergeAssocWith f l@((i,a):l') m@((j,b):m')
-- | @'intersectWith' f m1 m2@ build the pointwise conjunction @m1@ and @m2 at .
-- Uses @f@ to combine non-zero values.
--
--- Precondition: @'size' m1 == 'size' m2 at .
+-- No longer precondition: @'size' m1 == 'size' m2 at .
intersectWith :: (Ord i) => (a -> a -> a) -> Matrix i a -> Matrix i a -> Matrix i a
-intersectWith f m1 m2 = M (size m1) $ interAssocWith f (unM m1) (unM m2)
+intersectWith f m1 m2 = M (infSize m1 m2) $ interAssocWith f (unM m1) (unM m2)
+
+-- | Compute the matrix size of the intersection of two matrices.
+infSize m1 m2 = Size { rows = r, cols = c }
+ where
+ sz1 = size m1
+ sz2 = size m2
+ r = min (rows sz1) (rows sz2)
+ c = min (cols sz1) (cols sz2)
-- | assoc list intersection
interAssocWith :: (Ord i) => (a -> a -> a) -> [(i,a)] -> [(i,a)] -> [(i,a)]
@@ -353,12 +377,18 @@ prop_mul sz =
-- | @'diagonal' m@ extracts the diagonal of @m at .
--
--- Precondition: @'square' m at .
+-- No longer precondition: @'square' m at .
diagonal :: (Show i, Enum i, Num i, Ix i, HasZero b) => Matrix i b -> Array i b
-diagonal m = listArray (1, rows sz) $ blowUpSparseVec zeroElement (rows sz) $
- map (\ ((MIx i j),b) -> (i,b)) $ filter (\ ((MIx i j),b) -> i==j) (unM m)
- where sz = size m
+diagonal m = -- if r /= c then __IMPOSSIBLE__ else -- works also for non-square
+ listArray (1, n) $ blowUpSparseVec zeroElement n $
+ mapMaybe (\ ((MIx i j),b) -> if i==j then Just (i,b) else Nothing) $ unM m
+-- map (\ ((MIx i j),b) -> (i,b)) $ filter (\ ((MIx i j),b) -> i==j) (unM m)
+ where
+ sz = size m
+ r = rows sz
+ c = cols sz
+ n = max r c
prop_diagonal =
forAll natural $ \n ->
@@ -416,7 +446,8 @@ zipWith f m1 m2
tests :: IO Bool
tests = runTests "Agda.Termination.Matrix"
- [ quickCheck' prop_Arbitrary_Size
+ [ quickCheck' prop_transpose
+ , quickCheck' prop_Arbitrary_Size
, quickCheck' prop_Arbitrary_Matrix
, quickCheck' prop_Arbitrary_MIx
, quickCheck' prop_fromIndexList
diff --git a/src/full/Agda/Utils/Pointer.hs b/src/full/Agda/Utils/Pointer.hs
index 2d281d3..0887006 100644
--- a/src/full/Agda/Utils/Pointer.hs
+++ b/src/full/Agda/Utils/Pointer.hs
@@ -71,7 +71,7 @@ instance Ord (Ptr a) where
compare = compare `on` ptrTag
instance Hashable (Ptr a) where
- hash = hash . ptrTag
+ hashWithSalt salt = (hashWithSalt salt) . ptrTag
instance NFData (Ptr a) where
--
Packaging for Agda
More information about the Pkg-haskell-commits
mailing list