[agda] branch upstream updated (daa6a3e -> a116bca)
Iain Lane
laney at moszumanska.debian.org
Mon Jan 4 13:02:32 UTC 2016
This is an automated email from the git hooks/post-receive script.
laney pushed a change to branch upstream
in repository agda.
from daa6a3e Imported Upstream version 2.4.2.2
new 2fafd4d Imported Upstream version 2.4.2.3
new a116bca Imported Upstream version 2.4.2.5
The 2 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 | 257 +-
CHANGELOG | 577 +++
LICENSE | 34 +-
README.md | 45 +-
dist/build/Agda/Syntax/Parser/Lexer.hs | 115 +-
dist/build/Agda/Syntax/Parser/Parser.hs | 4139 ++++++++++----------
src/agda-mode/Main.hs | 31 +-
src/data/EpicInclude/AgdaPrelude.e | 207 -
src/data/EpicInclude/stdagda.c | 95 -
src/data/EpicInclude/stdagda.h | 41 -
src/data/agda.sty | 1 +
src/data/emacs-mode/agda-input.el | 3 +-
src/data/emacs-mode/agda2-mode.el | 202 +-
src/data/emacs-mode/agda2.el | 6 +-
src/data/emacs-mode/annotation.el | 57 +-
src/full/Agda/Auto/Auto.hs | 645 +--
src/full/Agda/Auto/CaseSplit.hs | 4 +-
src/full/Agda/Auto/Convert.hs | 11 +-
src/full/Agda/Auto/NarrowingSearch.hs | 17 +-
src/full/Agda/Auto/SearchControl.hs | 43 +-
src/full/Agda/Auto/Syntax.hs | 2 +-
src/full/Agda/Auto/Typecheck.hs | 6 +-
src/full/Agda/Benchmarking.hs | 109 +
src/full/Agda/Compiler/CallCompiler.hs | 2 +-
src/full/Agda/Compiler/Epic/CompileState.hs | 6 +-
src/full/Agda/Compiler/Epic/Compiler.hs | 5 +-
src/full/Agda/Compiler/Epic/Erasure.hs | 25 +-
src/full/Agda/Compiler/Epic/ForceConstrs.hs | 18 +-
src/full/Agda/Compiler/Epic/Forcing.hs | 8 +-
src/full/Agda/Compiler/Epic/FromAgda.hs | 10 +-
src/full/Agda/Compiler/Epic/Injection.hs | 23 +-
src/full/Agda/Compiler/Epic/Interface.hs | 2 +-
src/full/Agda/Compiler/Epic/NatDetection.hs | 4 +-
src/full/Agda/Compiler/Epic/Smashing.hs | 8 +-
src/full/Agda/Compiler/Epic/Static.hs | 12 +-
src/full/Agda/Compiler/HaskellTypes.hs | 2 +-
src/full/Agda/Compiler/JS/Compiler.hs | 17 +-
src/full/Agda/Compiler/MAlonzo/Compiler.hs | 521 ++-
src/full/Agda/Compiler/MAlonzo/Compiler.hs-boot | 4 +-
src/full/Agda/Compiler/MAlonzo/Misc.hs | 19 +-
src/full/Agda/Compiler/MAlonzo/Primitives.hs | 8 +-
src/full/Agda/Interaction/BasicOps.hs | 162 +-
.../Interaction/{CommandLine => }/CommandLine.hs | 34 +-
src/full/Agda/Interaction/EmacsCommand.hs | 3 +-
src/full/Agda/Interaction/Exceptions.hs | 6 +-
src/full/Agda/Interaction/FindFile.hs | 14 +-
src/full/Agda/Interaction/Highlighting/Generate.hs | 99 +-
src/full/Agda/Interaction/Highlighting/HTML.hs | 61 +-
src/full/Agda/Interaction/Highlighting/LaTeX.hs | 4 +-
src/full/Agda/Interaction/Highlighting/Precise.hs | 18 +-
src/full/Agda/Interaction/Imports.hs | 252 +-
src/full/Agda/Interaction/InteractionTop.hs | 238 +-
src/full/Agda/Interaction/InteractionTop.hs-boot | 5 +
src/full/Agda/Interaction/MakeCase.hs | 169 +-
src/full/Agda/Interaction/Monad.hs | 21 +-
src/full/Agda/Interaction/Options.hs | 156 +-
src/full/Agda/Interaction/Response.hs | 7 +-
src/full/Agda/Interaction/Response.hs-boot | 12 -
src/full/Agda/Main.hs | 61 +-
src/full/Agda/Syntax/Abstract.hs | 102 +-
src/full/Agda/Syntax/Abstract/Copatterns.hs | 58 +-
src/full/Agda/Syntax/Abstract/Name.hs | 111 +-
src/full/Agda/Syntax/Abstract/Views.hs | 80 +-
src/full/Agda/Syntax/Common.hs | 228 +-
src/full/Agda/Syntax/Concrete.hs | 176 +-
src/full/Agda/Syntax/Concrete/Definitions.hs | 320 +-
src/full/Agda/Syntax/Concrete/Generic.hs | 9 +-
src/full/Agda/Syntax/Concrete/Name.hs | 67 +-
src/full/Agda/Syntax/Concrete/Operators.hs | 257 +-
src/full/Agda/Syntax/Concrete/Operators/Parser.hs | 69 +-
src/full/Agda/Syntax/Concrete/Pretty.hs | 117 +-
src/full/Agda/Syntax/Fixity.hs | 122 +-
src/full/Agda/Syntax/Fixity.hs-boot | 10 +
src/full/Agda/Syntax/Info.hs | 48 +-
src/full/Agda/Syntax/Internal.hs | 547 ++-
src/full/Agda/Syntax/Internal/Defs.hs | 8 +-
src/full/Agda/Syntax/Internal/Generic.hs | 11 +-
src/full/Agda/Syntax/Internal/Pattern.hs | 38 +-
src/full/Agda/Syntax/Literal.hs | 2 +-
src/full/Agda/Syntax/Notation.hs | 11 +-
src/full/Agda/Syntax/Parser.hs | 7 +
src/full/Agda/Syntax/Parser/LookAhead.hs | 2 +-
src/full/Agda/Syntax/Parser/Monad.hs | 85 +-
src/full/Agda/Syntax/Parser/Parser.y | 564 +--
src/full/Agda/Syntax/Position.hs | 153 +-
src/full/Agda/Syntax/Scope/Base.hs | 118 +-
src/full/Agda/Syntax/Scope/Monad.hs | 160 +-
.../Agda/Syntax/Translation/AbstractToConcrete.hs | 315 +-
.../Agda/Syntax/Translation/ConcreteToAbstract.hs | 475 ++-
.../Agda/Syntax/Translation/InternalToAbstract.hs | 549 +--
src/full/Agda/Termination/CallGraph.hs | 52 +-
src/full/Agda/Termination/CallMatrix.hs | 40 +-
src/full/Agda/Termination/CutOff.hs | 4 +-
src/full/Agda/Termination/Inlining.hs | 70 +-
src/full/Agda/Termination/Monad.hs | 201 +-
src/full/Agda/Termination/Order.hs | 28 +-
src/full/Agda/Termination/Semiring.hs | 16 -
src/full/Agda/Termination/SparseMatrix.hs | 42 +-
src/full/Agda/Termination/TermCheck.hs | 524 +--
src/full/Agda/Tests.hs | 14 +-
src/full/Agda/TypeChecking/Abstract.hs | 16 +-
src/full/Agda/TypeChecking/CheckInternal.hs | 62 +-
src/full/Agda/TypeChecking/CheckInternal.hs-boot | 1 +
src/full/Agda/TypeChecking/CompiledClause.hs | 73 +-
.../Agda/TypeChecking/CompiledClause/Compile.hs | 143 +-
src/full/Agda/TypeChecking/CompiledClause/Match.hs | 226 +-
src/full/Agda/TypeChecking/Constraints.hs | 9 +-
src/full/Agda/TypeChecking/Constraints.hs-boot | 1 +
src/full/Agda/TypeChecking/Conversion.hs | 709 ++--
src/full/Agda/TypeChecking/Coverage.hs | 110 +-
src/full/Agda/TypeChecking/Coverage/Match.hs | 6 +-
src/full/Agda/TypeChecking/DisplayForm.hs | 45 +-
src/full/Agda/TypeChecking/DropArgs.hs | 5 +-
src/full/Agda/TypeChecking/Empty.hs | 38 +-
src/full/Agda/TypeChecking/Errors.hs | 1835 +++++----
src/full/Agda/TypeChecking/EtaContract.hs | 10 +-
src/full/Agda/TypeChecking/Forcing.hs | 162 +-
src/full/Agda/TypeChecking/Free.hs | 199 +-
src/full/Agda/TypeChecking/Free/Lazy.hs | 390 ++
.../Agda/TypeChecking/{Free.hs => Free/Old.hs} | 16 +-
src/full/Agda/TypeChecking/Free/Tests.hs | 125 +
src/full/Agda/TypeChecking/Implicit.hs | 22 +-
src/full/Agda/TypeChecking/Injectivity.hs | 8 +-
src/full/Agda/TypeChecking/InstanceArguments.hs | 239 +-
src/full/Agda/TypeChecking/Irrelevance.hs | 65 +-
src/full/Agda/TypeChecking/Level.hs | 6 +-
src/full/Agda/TypeChecking/MetaVars.hs | 599 ++-
src/full/Agda/TypeChecking/MetaVars/Mention.hs | 9 +-
src/full/Agda/TypeChecking/MetaVars/Occurs.hs | 463 ++-
src/full/Agda/TypeChecking/Monad.hs | 2 -
src/full/Agda/TypeChecking/Monad/Base.hs | 567 ++-
src/full/Agda/TypeChecking/Monad/Base.hs-boot | 15 +-
src/full/Agda/TypeChecking/Monad/Base/Benchmark.hs | 78 -
src/full/Agda/TypeChecking/Monad/Base/KillRange.hs | 120 -
src/full/Agda/TypeChecking/Monad/Benchmark.hs | 116 +-
src/full/Agda/TypeChecking/Monad/Builtin.hs | 86 +-
src/full/Agda/TypeChecking/Monad/Constraints.hs | 4 +-
src/full/Agda/TypeChecking/Monad/Context.hs | 29 +-
src/full/Agda/TypeChecking/Monad/Debug.hs | 6 -
src/full/Agda/TypeChecking/Monad/Exception.hs | 6 +-
src/full/Agda/TypeChecking/Monad/MetaVars.hs | 57 +-
src/full/Agda/TypeChecking/Monad/Mutual.hs | 9 +-
src/full/Agda/TypeChecking/Monad/Options.hs | 32 +-
src/full/Agda/TypeChecking/Monad/Signature.hs | 393 +-
src/full/Agda/TypeChecking/Monad/SizedTypes.hs | 17 +-
src/full/Agda/TypeChecking/Monad/State.hs | 25 +-
src/full/Agda/TypeChecking/Monad/Statistics.hs | 16 +-
src/full/Agda/TypeChecking/Monad/Trace.hs | 121 +-
src/full/Agda/TypeChecking/Patterns/Abstract.hs | 14 +-
src/full/Agda/TypeChecking/Patterns/Match.hs | 176 +-
src/full/Agda/TypeChecking/Patterns/Match.hs-boot | 2 +-
src/full/Agda/TypeChecking/Polarity.hs | 166 +-
src/full/Agda/TypeChecking/Positivity.hs | 454 ++-
.../Agda/TypeChecking/Positivity/Occurrence.hs | 148 +
src/full/Agda/TypeChecking/Positivity/Tests.hs | 27 +
src/full/Agda/TypeChecking/Pretty.hs | 260 +-
src/full/Agda/TypeChecking/Pretty.hs-boot | 21 +-
src/full/Agda/TypeChecking/Primitive.hs | 335 +-
src/full/Agda/TypeChecking/ProjectionLike.hs | 141 +-
src/full/Agda/TypeChecking/Quote.hs | 12 +-
src/full/Agda/TypeChecking/RecordPatterns.hs | 145 +-
src/full/Agda/TypeChecking/Records.hs | 168 +-
src/full/Agda/TypeChecking/Reduce.hs | 185 +-
src/full/Agda/TypeChecking/Reduce/Monad.hs | 26 +-
src/full/Agda/TypeChecking/Rewriting.hs | 301 +-
src/full/Agda/TypeChecking/Rewriting.hs-boot | 2 +-
.../Agda/TypeChecking/Rewriting/NonLinMatch.hs | 281 ++
src/full/Agda/TypeChecking/Rules/Builtin.hs | 86 +-
.../Agda/TypeChecking/Rules/Builtin/Coinduction.hs | 48 +-
src/full/Agda/TypeChecking/Rules/Data.hs | 28 +-
src/full/Agda/TypeChecking/Rules/Decl.hs | 286 +-
src/full/Agda/TypeChecking/Rules/Def.hs | 588 +--
src/full/Agda/TypeChecking/Rules/Def.hs-boot | 2 +-
src/full/Agda/TypeChecking/Rules/LHS.hs | 641 +--
src/full/Agda/TypeChecking/Rules/LHS/Implicit.hs | 78 +-
.../Agda/TypeChecking/Rules/LHS/Instantiate.hs | 4 +-
src/full/Agda/TypeChecking/Rules/LHS/Problem.hs | 26 +-
.../Agda/TypeChecking/Rules/LHS/ProblemRest.hs | 9 +-
src/full/Agda/TypeChecking/Rules/LHS/Split.hs | 196 +-
src/full/Agda/TypeChecking/Rules/LHS/Unify.hs | 182 +-
src/full/Agda/TypeChecking/Rules/Record.hs | 239 +-
src/full/Agda/TypeChecking/Rules/Term.hs | 543 ++-
src/full/Agda/TypeChecking/Rules/Term.hs-boot | 6 +-
src/full/Agda/TypeChecking/Serialise.hs | 1659 +-------
src/full/Agda/TypeChecking/Serialise/Base.hs | 640 +++
src/full/Agda/TypeChecking/Serialise/Instances.hs | 19 +
.../TypeChecking/Serialise/Instances/Abstract.hs | 279 ++
.../TypeChecking/Serialise/Instances/Common.hs | 437 +++
.../TypeChecking/Serialise/Instances/Compilers.hs | 126 +
.../Serialise/Instances/Highlighting.hs | 93 +
.../TypeChecking/Serialise/Instances/Internal.hs | 418 ++
src/full/Agda/TypeChecking/SizedTypes.hs | 231 +-
src/full/Agda/TypeChecking/SizedTypes/Solve.hs | 87 +-
src/full/Agda/TypeChecking/SizedTypes/Syntax.hs | 41 +-
src/full/Agda/TypeChecking/SizedTypes/Tests.hs | 19 +-
src/full/Agda/TypeChecking/SizedTypes/Utils.hs | 3 +
.../Agda/TypeChecking/SizedTypes/WarshallSolver.hs | 116 +-
src/full/Agda/TypeChecking/Substitute.hs | 290 +-
src/full/Agda/TypeChecking/SyntacticEquality.hs | 16 +-
src/full/Agda/TypeChecking/Telescope.hs | 61 +-
src/full/Agda/TypeChecking/Test/Generators.hs | 11 +-
src/full/Agda/TypeChecking/Unquote.hs | 13 +-
src/full/Agda/TypeChecking/With.hs | 681 ++--
src/full/Agda/Utils/AssocList.hs | 2 +-
src/full/Agda/Utils/Bag.hs | 15 +-
src/full/Agda/Utils/Benchmark.hs | 165 +
src/full/Agda/Utils/BiMap.hs | 12 +-
src/full/Agda/Utils/Cluster.hs | 6 +-
src/full/Agda/Utils/Either.hs | 34 +-
src/full/Agda/Utils/Empty.hs | 2 +-
src/full/Agda/Utils/Except.hs | 26 +-
src/full/Agda/Utils/Favorites.hs | 31 +-
src/full/Agda/Utils/FileName.hs | 14 +-
src/full/Agda/Utils/Function.hs | 14 +
src/full/Agda/Utils/Functor.hs | 22 +-
src/full/Agda/Utils/Graph/AdjacencyMap.hs | 390 --
.../Utils/Graph/AdjacencyMap/Unidirectional.hs | 609 ++-
.../Graph/AdjacencyMap/Unidirectional/Tests.hs | 372 ++
src/full/Agda/Utils/HashMap.hs | 26 +-
src/full/Agda/Utils/IORef.hs | 14 +-
src/full/Agda/Utils/Impossible.hs | 2 +-
src/full/Agda/Utils/Lens.hs | 23 +-
src/full/Agda/Utils/Lens/Examples.hs | 2 +-
src/full/Agda/Utils/List.hs | 29 +-
src/full/Agda/Utils/ListT.hs | 148 +
src/full/Agda/Utils/ListT/Tests.hs | 48 +
src/full/Agda/Utils/Maybe.hs | 48 +-
src/full/Agda/Utils/Maybe/Strict.hs | 24 +-
src/full/Agda/Utils/Monad.hs | 31 +-
src/full/Agda/Utils/Null.hs | 52 +-
src/full/Agda/Utils/PartialOrd.hs | 12 +-
src/full/Agda/Utils/Permutation.hs | 60 +-
src/full/Agda/Utils/Permutation/Tests.hs | 18 +-
src/full/Agda/Utils/Pointed.hs | 19 -
src/full/Agda/Utils/Pointer.hs | 4 +-
src/full/Agda/Utils/Pretty.hs | 46 +-
src/full/Agda/Utils/ReadP.hs | 23 +-
src/full/Agda/Utils/SemiRing.hs | 17 +
src/full/Agda/Utils/Singleton.hs | 73 +
src/full/Agda/Utils/Size.hs | 19 +-
src/full/Agda/Utils/String.hs | 24 +-
src/full/Agda/Utils/Suffix.hs | 2 +-
src/full/Agda/Utils/Time.hs | 41 +-
src/full/Agda/Utils/Trie.hs | 23 +-
src/full/Agda/Utils/Tuple.hs | 8 +-
src/full/Agda/Utils/VarSet.hs | 6 -
src/full/Agda/Utils/Warshall.hs | 17 +-
247 files changed, 21081 insertions(+), 14322 deletions(-)
delete mode 100644 src/data/EpicInclude/AgdaPrelude.e
delete mode 100644 src/data/EpicInclude/stdagda.c
delete mode 100644 src/data/EpicInclude/stdagda.h
create mode 100644 src/full/Agda/Benchmarking.hs
rename src/full/Agda/Interaction/{CommandLine => }/CommandLine.hs (92%)
create mode 100644 src/full/Agda/Interaction/InteractionTop.hs-boot
delete mode 100644 src/full/Agda/Interaction/Response.hs-boot
create mode 100644 src/full/Agda/Syntax/Fixity.hs-boot
create mode 100644 src/full/Agda/TypeChecking/Free/Lazy.hs
copy src/full/Agda/TypeChecking/{Free.hs => Free/Old.hs} (97%)
create mode 100644 src/full/Agda/TypeChecking/Free/Tests.hs
delete mode 100644 src/full/Agda/TypeChecking/Monad/Base/Benchmark.hs
delete mode 100644 src/full/Agda/TypeChecking/Monad/Base/KillRange.hs
delete mode 100644 src/full/Agda/TypeChecking/Monad/Debug.hs
create mode 100644 src/full/Agda/TypeChecking/Positivity/Occurrence.hs
create mode 100644 src/full/Agda/TypeChecking/Positivity/Tests.hs
create mode 100644 src/full/Agda/TypeChecking/Rewriting/NonLinMatch.hs
create mode 100644 src/full/Agda/TypeChecking/Serialise/Base.hs
create mode 100644 src/full/Agda/TypeChecking/Serialise/Instances.hs
create mode 100644 src/full/Agda/TypeChecking/Serialise/Instances/Abstract.hs
create mode 100644 src/full/Agda/TypeChecking/Serialise/Instances/Common.hs
create mode 100644 src/full/Agda/TypeChecking/Serialise/Instances/Compilers.hs
create mode 100644 src/full/Agda/TypeChecking/Serialise/Instances/Highlighting.hs
create mode 100644 src/full/Agda/TypeChecking/Serialise/Instances/Internal.hs
create mode 100644 src/full/Agda/Utils/Benchmark.hs
delete mode 100644 src/full/Agda/Utils/Graph/AdjacencyMap.hs
create mode 100644 src/full/Agda/Utils/Graph/AdjacencyMap/Unidirectional/Tests.hs
create mode 100644 src/full/Agda/Utils/ListT.hs
create mode 100644 src/full/Agda/Utils/ListT/Tests.hs
delete mode 100644 src/full/Agda/Utils/Pointed.hs
create mode 100644 src/full/Agda/Utils/Singleton.hs
--
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