[Pkg-haskell-commits] [agda] branch upstream updated (6770868 -> daa6a3e)
Iain Lane
laney at moszumanska.debian.org
Wed May 20 11:52:00 UTC 2015
This is an automated email from the git hooks/post-receive script.
laney pushed a change to branch upstream
in repository agda.
from 6770868 Imported Upstream version 2.4.2
new daa6a3e Imported Upstream version 2.4.2.2
The 1 revisions listed above as "new" are entirely new to this
repository and will be described in separate emails. The revisions
listed as "adds" were already present in the repository and have only
been added to this reference.
Summary of changes:
Agda.cabal | 150 +-
CHANGELOG | 216 +++
dist/build/Agda/Syntax/Parser/Lexer.hs | 172 +-
dist/build/Agda/Syntax/Parser/Parser.hs | 1831 ++++++++++----------
src/data/agda.sty | 25 +-
src/data/emacs-mode/agda2-highlight.el | 112 +-
src/data/emacs-mode/agda2-mode.el | 18 +-
src/full/Agda/Auto/Auto.hs | 710 ++++----
src/full/Agda/Auto/CaseSplit.hs | 36 +-
src/full/Agda/Auto/Convert.hs | 110 +-
src/full/Agda/Auto/NarrowingSearch.hs | 16 +-
src/full/Agda/Auto/SearchControl.hs | 54 +-
src/full/Agda/Auto/Syntax.hs | 7 +-
src/full/Agda/Auto/Typecheck.hs | 32 +-
src/full/Agda/Compiler/CallCompiler.hs | 2 +-
src/full/Agda/Compiler/Epic/AuxAST.hs | 28 +-
src/full/Agda/Compiler/Epic/CompileState.hs | 51 +-
src/full/Agda/Compiler/Epic/Compiler.hs | 55 +-
src/full/Agda/Compiler/Epic/Epic.hs | 2 +-
src/full/Agda/Compiler/Epic/Erasure.hs | 34 +-
src/full/Agda/Compiler/Epic/ForceConstrs.hs | 4 +-
src/full/Agda/Compiler/Epic/Forcing.hs | 18 +-
src/full/Agda/Compiler/Epic/FromAgda.hs | 14 +-
src/full/Agda/Compiler/Epic/Injection.hs | 87 +-
src/full/Agda/Compiler/Epic/Interface.hs | 3 +-
src/full/Agda/Compiler/Epic/NatDetection.hs | 7 +-
src/full/Agda/Compiler/Epic/Primitive.hs | 28 +-
src/full/Agda/Compiler/Epic/Smashing.hs | 20 +-
src/full/Agda/Compiler/Epic/Static.hs | 26 +-
src/full/Agda/Compiler/HaskellTypes.hs | 5 +-
src/full/Agda/Compiler/JS/Case.hs | 2 +-
src/full/Agda/Compiler/JS/Compiler.hs | 18 +-
src/full/Agda/Compiler/JS/Syntax.hs | 1 +
src/full/Agda/Compiler/MAlonzo/Compiler.hs | 121 +-
src/full/Agda/Compiler/MAlonzo/Encode.hs | 3 +
src/full/Agda/Compiler/MAlonzo/Misc.hs | 43 +-
src/full/Agda/Compiler/MAlonzo/Pretty.hs | 10 +-
src/full/Agda/Compiler/MAlonzo/Primitives.hs | 34 +-
src/full/Agda/ImpossibleTest.hs | 1 +
src/full/Agda/Interaction/BasicOps.hs | 104 +-
.../Agda/Interaction/CommandLine/CommandLine.hs | 208 +--
src/full/Agda/Interaction/EmacsCommand.hs | 8 +-
src/full/Agda/Interaction/EmacsTop.hs | 2 -
src/full/Agda/Interaction/Exceptions.hs | 3 +-
src/full/Agda/Interaction/FindFile.hs | 5 +-
src/full/Agda/Interaction/Highlighting/Dot.hs | 4 +-
src/full/Agda/Interaction/Highlighting/Emacs.hs | 16 +-
src/full/Agda/Interaction/Highlighting/Generate.hs | 254 ++-
src/full/Agda/Interaction/Highlighting/HTML.hs | 14 +-
src/full/Agda/Interaction/Highlighting/LaTeX.hs | 62 +-
src/full/Agda/Interaction/Highlighting/Precise.hs | 113 +-
src/full/Agda/Interaction/Highlighting/Range.hs | 10 +-
src/full/Agda/Interaction/Highlighting/Vim.hs | 60 +-
src/full/Agda/Interaction/Imports.hs | 188 +-
src/full/Agda/Interaction/InteractionTop.hs | 81 +-
src/full/Agda/Interaction/MakeCase.hs | 85 +-
src/full/Agda/Interaction/Monad.hs | 9 +-
src/full/Agda/Interaction/Options.hs | 410 +++--
src/full/Agda/Interaction/Options/Lenses.hs | 8 +-
src/full/Agda/Interaction/Response.hs | 10 +-
src/full/Agda/Main.hs | 36 +-
src/full/Agda/Syntax/Abstract.hs | 638 ++++---
src/full/Agda/Syntax/Abstract/Copatterns.hs | 19 +-
src/full/Agda/Syntax/Abstract/Name.hs | 130 +-
src/full/Agda/Syntax/Abstract/Pretty.hs | 1 +
src/full/Agda/Syntax/Abstract/Views.hs | 97 +-
src/full/Agda/Syntax/Common.hs | 44 +-
src/full/Agda/Syntax/Concrete.hs | 698 ++++----
src/full/Agda/Syntax/Concrete/Definitions.hs | 454 +++--
src/full/Agda/Syntax/Concrete/Generic.hs | 10 +-
src/full/Agda/Syntax/Concrete/Name.hs | 40 +-
src/full/Agda/Syntax/Concrete/Operators.hs | 173 +-
src/full/Agda/Syntax/Concrete/Operators/Parser.hs | 62 +-
src/full/Agda/Syntax/Concrete/Pretty.hs | 438 ++---
src/full/Agda/Syntax/Fixity.hs | 153 +-
src/full/Agda/Syntax/Info.hs | 106 +-
src/full/Agda/Syntax/Internal.hs | 154 +-
src/full/Agda/Syntax/Internal/Defs.hs | 6 +-
src/full/Agda/Syntax/Internal/Generic.hs | 6 +-
src/full/Agda/Syntax/Internal/Pattern.hs | 116 +-
src/full/Agda/Syntax/Literal.hs | 15 +-
src/full/Agda/Syntax/Notation.hs | 164 +-
src/full/Agda/Syntax/Parser.hs | 12 +-
src/full/Agda/Syntax/Parser/Alex.hs | 43 +-
src/full/Agda/Syntax/Parser/Comments.hs | 28 +-
src/full/Agda/Syntax/Parser/Layout.hs | 76 +-
src/full/Agda/Syntax/Parser/LexActions.hs | 124 +-
src/full/Agda/Syntax/Parser/Lexer.x | 170 +-
src/full/Agda/Syntax/Parser/LookAhead.hs | 63 +-
src/full/Agda/Syntax/Parser/Monad.hs | 173 +-
src/full/Agda/Syntax/Parser/Parser.y | 551 +++---
src/full/Agda/Syntax/Parser/StringLiterals.hs | 137 +-
src/full/Agda/Syntax/Parser/Tokens.hs | 71 +-
src/full/Agda/Syntax/Position.hs | 210 ++-
src/full/Agda/Syntax/Scope/Base.hs | 319 ++--
src/full/Agda/Syntax/Scope/Monad.hs | 226 ++-
.../Agda/Syntax/Translation/AbstractToConcrete.hs | 42 +-
.../Agda/Syntax/Translation/ConcreteToAbstract.hs | 389 +++--
.../Agda/Syntax/Translation/InternalToAbstract.hs | 35 +-
src/full/Agda/Termination/CallGraph.hs | 34 +-
src/full/Agda/Termination/CallMatrix.hs | 18 +-
src/full/Agda/Termination/Inlining.hs | 6 +-
src/full/Agda/Termination/Monad.hs | 78 +-
src/full/Agda/Termination/Order.hs | 18 +-
src/full/Agda/Termination/RecCheck.hs | 4 +-
src/full/Agda/Termination/Semiring.hs | 3 +
src/full/Agda/Termination/SparseMatrix.hs | 31 +-
src/full/Agda/Termination/TermCheck.hs | 215 ++-
src/full/Agda/Termination/Termination.hs | 2 +-
src/full/Agda/Tests.hs | 21 +-
src/full/Agda/TheTypeChecker.hs | 1 -
src/full/Agda/TypeChecking/Abstract.hs | 10 +-
src/full/Agda/TypeChecking/CheckInternal.hs | 21 +-
src/full/Agda/TypeChecking/CompiledClause.hs | 62 +-
.../Agda/TypeChecking/CompiledClause/Compile.hs | 7 +-
src/full/Agda/TypeChecking/CompiledClause/Match.hs | 4 +-
src/full/Agda/TypeChecking/Constraints.hs | 13 +-
src/full/Agda/TypeChecking/Conversion.hs | 111 +-
src/full/Agda/TypeChecking/Coverage.hs | 238 +--
src/full/Agda/TypeChecking/Coverage/Match.hs | 6 +-
src/full/Agda/TypeChecking/Coverage/SplitTree.hs | 3 +-
src/full/Agda/TypeChecking/Datatypes.hs | 10 +-
src/full/Agda/TypeChecking/DisplayForm.hs | 19 +-
src/full/Agda/TypeChecking/DropArgs.hs | 6 +-
src/full/Agda/TypeChecking/Errors.hs | 688 ++++----
src/full/Agda/TypeChecking/EtaContract.hs | 8 +-
src/full/Agda/TypeChecking/Forcing.hs | 2 +-
src/full/Agda/TypeChecking/Free.hs | 285 ++-
src/full/Agda/TypeChecking/Implicit.hs | 10 +-
src/full/Agda/TypeChecking/Injectivity.hs | 46 +-
src/full/Agda/TypeChecking/InstanceArguments.hs | 42 +-
src/full/Agda/TypeChecking/Level.hs | 6 +-
src/full/Agda/TypeChecking/LevelConstraints.hs | 2 +-
src/full/Agda/TypeChecking/MetaVars.hs | 132 +-
src/full/Agda/TypeChecking/MetaVars.hs-boot | 8 +-
src/full/Agda/TypeChecking/MetaVars/Mention.hs | 7 +-
src/full/Agda/TypeChecking/MetaVars/Occurs.hs | 40 +-
src/full/Agda/TypeChecking/Monad/Base.hs | 1013 +++++++----
src/full/Agda/TypeChecking/Monad/Base/Benchmark.hs | 11 +-
src/full/Agda/TypeChecking/Monad/Base/KillRange.hs | 8 +-
src/full/Agda/TypeChecking/Monad/Benchmark.hs | 2 +-
src/full/Agda/TypeChecking/Monad/Builtin.hs | 206 ++-
src/full/Agda/TypeChecking/Monad/Closure.hs | 1 -
src/full/Agda/TypeChecking/Monad/Constraints.hs | 20 +-
src/full/Agda/TypeChecking/Monad/Context.hs | 24 +-
src/full/Agda/TypeChecking/Monad/Debug.hs | 1 -
src/full/Agda/TypeChecking/Monad/Env.hs | 27 +-
src/full/Agda/TypeChecking/Monad/Exception.hs | 9 +-
src/full/Agda/TypeChecking/Monad/Imports.hs | 43 +-
src/full/Agda/TypeChecking/Monad/MetaVars.hs | 60 +-
src/full/Agda/TypeChecking/Monad/Mutual.hs | 14 +-
src/full/Agda/TypeChecking/Monad/Open.hs | 13 +-
src/full/Agda/TypeChecking/Monad/Options.hs | 33 +-
src/full/Agda/TypeChecking/Monad/Sharing.hs | 2 +-
src/full/Agda/TypeChecking/Monad/Signature.hs | 107 +-
src/full/Agda/TypeChecking/Monad/SizedTypes.hs | 21 +-
src/full/Agda/TypeChecking/Monad/State.hs | 91 +-
src/full/Agda/TypeChecking/Monad/Statistics.hs | 33 +-
src/full/Agda/TypeChecking/Monad/Trace.hs | 9 +-
src/full/Agda/TypeChecking/Patterns/Abstract.hs | 48 +-
src/full/Agda/TypeChecking/Patterns/Match.hs | 60 +-
src/full/Agda/TypeChecking/Polarity.hs | 10 +-
src/full/Agda/TypeChecking/Positivity.hs | 22 +-
src/full/Agda/TypeChecking/Pretty.hs | 132 +-
src/full/Agda/TypeChecking/Pretty.hs-boot | 4 +-
src/full/Agda/TypeChecking/Primitive.hs | 243 +--
src/full/Agda/TypeChecking/ProjectionLike.hs | 8 +-
src/full/Agda/TypeChecking/Quote.hs | 461 +----
src/full/Agda/TypeChecking/RecordPatterns.hs | 12 +-
src/full/Agda/TypeChecking/Records.hs | 8 +-
src/full/Agda/TypeChecking/Reduce.hs | 289 ++-
src/full/Agda/TypeChecking/Reduce/Monad.hs | 34 +-
src/full/Agda/TypeChecking/Rewriting.hs | 2 +-
src/full/Agda/TypeChecking/Rules/Builtin.hs | 12 +-
.../Agda/TypeChecking/Rules/Builtin/Coinduction.hs | 9 +-
src/full/Agda/TypeChecking/Rules/Data.hs | 140 +-
src/full/Agda/TypeChecking/Rules/Decl.hs | 199 ++-
src/full/Agda/TypeChecking/Rules/Def.hs | 215 +--
src/full/Agda/TypeChecking/Rules/Def.hs-boot | 6 +-
src/full/Agda/TypeChecking/Rules/LHS.hs | 731 ++++----
src/full/Agda/TypeChecking/Rules/LHS/Implicit.hs | 22 +-
.../Agda/TypeChecking/Rules/LHS/Instantiate.hs | 32 +-
src/full/Agda/TypeChecking/Rules/LHS/Problem.hs | 75 +-
.../Agda/TypeChecking/Rules/LHS/ProblemRest.hs | 4 +-
src/full/Agda/TypeChecking/Rules/LHS/Split.hs | 369 ++--
src/full/Agda/TypeChecking/Rules/LHS/Unify.hs | 184 +-
src/full/Agda/TypeChecking/Rules/Record.hs | 117 +-
src/full/Agda/TypeChecking/Rules/Term.hs | 347 ++--
src/full/Agda/TypeChecking/Rules/Term.hs-boot | 4 +-
src/full/Agda/TypeChecking/Serialise.hs | 1155 ++++++++----
src/full/Agda/TypeChecking/SizedTypes.hs | 21 +-
src/full/Agda/TypeChecking/SizedTypes/Solve.hs | 18 +-
src/full/Agda/TypeChecking/SizedTypes/Syntax.hs | 18 +-
src/full/Agda/TypeChecking/SizedTypes/Tests.hs | 94 +-
src/full/Agda/TypeChecking/SizedTypes/Utils.hs | 10 +-
.../Agda/TypeChecking/SizedTypes/WarshallSolver.hs | 43 +-
src/full/Agda/TypeChecking/Substitute.hs | 194 ++-
src/full/Agda/TypeChecking/SyntacticEquality.hs | 12 +-
src/full/Agda/TypeChecking/Telescope.hs | 42 +-
src/full/Agda/TypeChecking/Test/Generators.hs | 192 +-
src/full/Agda/TypeChecking/Tests.hs | 17 +-
src/full/Agda/TypeChecking/Unquote.hs | 403 +++++
src/full/Agda/TypeChecking/With.hs | 8 +-
src/full/Agda/Utils/AssocList.hs | 79 +
src/full/Agda/Utils/Bag.hs | 217 +++
src/full/Agda/Utils/BiMap.hs | 15 +-
src/full/Agda/Utils/Char.hs | 46 +-
src/full/Agda/Utils/Cluster.hs | 91 +-
src/full/Agda/Utils/Either.hs | 59 +-
src/full/Agda/Utils/Empty.hs | 24 +
src/full/Agda/Utils/Except.hs | 62 +
src/full/Agda/Utils/Favorites.hs | 13 +-
src/full/Agda/Utils/FileName.hs | 11 +-
src/full/Agda/Utils/Fresh.hs | 23 -
src/full/Agda/Utils/Function.hs | 47 +-
src/full/Agda/Utils/Functor.hs | 13 +
src/full/Agda/Utils/Geniplate.hs | 5 +
src/full/Agda/Utils/Graph/AdjacencyMap.hs | 6 +-
.../Utils/Graph/AdjacencyMap/Unidirectional.hs | 29 +-
src/full/Agda/Utils/HashMap.hs | 1 -
src/full/Agda/Utils/IO/UTF8.hs | 17 +-
src/full/Agda/Utils/IORef.hs | 29 +
src/full/Agda/Utils/Lens.hs | 68 +
src/full/Agda/Utils/Lens/Examples.hs | 18 +
src/full/Agda/Utils/List.hs | 88 +-
src/full/Agda/Utils/Map.hs | 22 +-
src/full/Agda/Utils/Maybe.hs | 2 +-
src/full/Agda/Utils/Maybe/Strict.hs | 4 +-
src/full/Agda/Utils/Monad.hs | 58 +-
src/full/Agda/Utils/Null.hs | 20 +
src/full/Agda/Utils/PartialOrd.hs | 41 +-
src/full/Agda/Utils/Permutation.hs | 84 +-
src/full/Agda/Utils/Permutation/Tests.hs | 117 ++
src/full/Agda/Utils/Pointer.hs | 1 +
src/full/Agda/Utils/Pretty.hs | 49 +-
src/full/Agda/Utils/ReadP.hs | 17 +-
src/full/Agda/Utils/SemiRing.hs | 1 -
src/full/Agda/Utils/Size.hs | 56 +-
src/full/Agda/Utils/String.hs | 5 +-
src/full/Agda/Utils/Suffix.hs | 32 +-
src/full/Agda/Utils/Time.hs | 26 +-
src/full/Agda/Utils/Trie.hs | 13 +-
src/full/Agda/Utils/Tuple.hs | 6 +-
src/full/Agda/Utils/Unicode.hs | 26 -
src/full/Agda/Utils/Update.hs | 1 +
src/full/Agda/Utils/VarSet.hs | 19 +-
src/full/Agda/Utils/Warshall.hs | 28 +-
src/full/Agda/Version.hs | 1 -
src/full/{Agda => }/undefined.h | 0
249 files changed, 13467 insertions(+), 10103 deletions(-)
create mode 100644 src/full/Agda/TypeChecking/Unquote.hs
create mode 100644 src/full/Agda/Utils/AssocList.hs
create mode 100644 src/full/Agda/Utils/Bag.hs
create mode 100644 src/full/Agda/Utils/Empty.hs
create mode 100644 src/full/Agda/Utils/Except.hs
delete mode 100644 src/full/Agda/Utils/Fresh.hs
create mode 100644 src/full/Agda/Utils/IORef.hs
create mode 100644 src/full/Agda/Utils/Lens.hs
create mode 100644 src/full/Agda/Utils/Lens/Examples.hs
create mode 100644 src/full/Agda/Utils/Permutation/Tests.hs
delete mode 100644 src/full/Agda/Utils/Unicode.hs
rename src/full/{Agda => }/undefined.h (100%)
--
Alioth's /usr/local/bin/git-commit-notice on /srv/git.debian.org/git/pkg-haskell/agda.git
More information about the Pkg-haskell-commits
mailing list