Agda 2.3.2 → 2.3.2.1
raw patch · 10 files changed
+127/−68 lines, 10 filesdep ~Agdadep ~QuickCheckdep ~Win32new-uploader
Dependency ranges changed: Agda, QuickCheck, Win32, hashable, mtl
Files
- Agda.cabal +9/−8
- dist/build/Agda/Syntax/Parser/Lexer.hs +35/−27
- dist/build/Agda/Syntax/Parser/Parser.hs +2/−2
- doc/release-notes/2-3-2-1.txt +18/−0
- src/data/emacs-mode/agda2-mode.el +1/−1
- src/full/Agda/Syntax/Abstract/Name.hs +4/−4
- src/full/Agda/Syntax/Common.hs +2/−2
- src/full/Agda/Termination/CallGraph.hs +2/−1
- src/full/Agda/Termination/SparseMatrix.hs +53/−22
- src/full/Agda/Utils/Pointer.hs +1/−1
Agda.cabal view
@@ -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 @@ 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 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 @@ 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 @@ 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 @@ 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
dist/build/Agda/Syntax/Parser/Lexer.hs view
@@ -61,7 +61,7 @@ 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 @@ {-# 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 @@ -- ----------------------------------------------------------------------------- -- 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 @@ #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,36 +363,41 @@ - 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 | AlexLastAcc a !AlexInput !Int@@ -404,11 +409,13 @@ 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 -- -----------------------------------------------------------------------------@@ -433,6 +440,7 @@ -- TODO: there's no need to find the longest -- match when checking the right context, just -- the first match will do.+ -- used by wrappers iUnbox (I# (i)) = i
dist/build/Agda/Syntax/Parser/Parser.hs view
@@ -51,7 +51,7 @@ 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 @@ {-# 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
+ doc/release-notes/2-3-2-1.txt view
@@ -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).
src/data/emacs-mode/agda2-mode.el view
@@ -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.")
src/full/Agda/Syntax/Abstract/Name.hs view
@@ -239,8 +239,8 @@ 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 @@ 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
src/full/Agda/Syntax/Common.hs view
@@ -272,8 +272,8 @@ 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
src/full/Agda/Termination/CallGraph.hs view
@@ -213,7 +213,8 @@ -} 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'
src/full/Agda/Termination/SparseMatrix.hs view
@@ -40,8 +40,10 @@ 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 @@ (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 @@ => 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 @@ | 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,13 +280,25 @@ , 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@. Uses @(+)@ to add values. ----- Precondition: @'size' m1 == 'size' m2@.+-- No longer precondition: @'size' m1 == 'size' m2@. 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)] mergeAssocWith f [] m = m@@ -295,11 +311,19 @@ -- | @'intersectWith' f m1 m2@ build the pointwise conjunction @m1@ and @m2@. -- Uses @f@ to combine non-zero values. ----- Precondition: @'size' m1 == 'size' m2@.+-- No longer precondition: @'size' m1 == 'size' m2@. 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)] interAssocWith f [] m = []@@ -353,12 +377,18 @@ -- | @'diagonal' m@ extracts the diagonal of @m@. ----- Precondition: @'square' m@.+-- No longer precondition: @'square' m@. 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 @@ 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
src/full/Agda/Utils/Pointer.hs view
@@ -71,7 +71,7 @@ compare = compare `on` ptrTag instance Hashable (Ptr a) where- hash = hash . ptrTag+ hashWithSalt salt = (hashWithSalt salt) . ptrTag instance NFData (Ptr a) where