← Back to branch summary

~ubuntu-branches/ubuntu/trusty/agda/trusty

~ubuntu-branches/ubuntu/trusty/agda/trusty

« back to all changes in this revision

Viewing changes to src/full/Agda/Termination/Matrix.hs

Committer: Package Import Robot
Author(s): Iain Lane, Kiwamu Okabe, Iain Lane
Date: 2013-04-10 11:46:43 UTC
mfrom: (4.1.5 experimental)
Revision ID: package-import@ubuntu.com-20130410114643-prunhsz59f0fhrdn

Tags: 2.3.2-1

[ Kiwamu Okabe ]
* New patch: Extend haskell-src-exts dependency and fix type miss.

[ Iain Lane ]
* [dfbca48] Imported Upstream version 2.3.2
* [7746bcc] Remove all patches — all upstream.
* [2cdb691] Update build-deps to match control file
* [868ebf4] agda-mode no longer depends on haskell-mode or GHCi.
Remove dependency and update .el file accordingly
* [9e0ba22] Add agda-bin package here, as the separate package has been
removed
* [75a240f] agda-mode needs to depend on agda-bin
* [d290f95] Allow Quickcheck up to 2.7. Fix haskeline build-dep.
* [79190e6] Add missing geniplate and parallel BDs

files added:
.pc/allow-quickcheck-2.7

.pc/allow-quickcheck-2.7/Agda.cabal

debian/agda-bin.install

debian/patches/allow-quickcheck-2.7

doc/release-notes/2-3-2.txt

src/data/agda.sty

src/data/emacs-mode/agda2-queue.el

src/full/Agda/Compiler/CallCompiler.hs

src/full/Agda/Interaction/GhcTop.hs

src/full/Agda/Interaction/Highlighting/Generate.hs-boot

src/full/Agda/Interaction/Highlighting/LaTeX.hs

src/full/Agda/Interaction/InteractionTop.hs

src/full/Agda/Interaction/Response.hs

src/full/Agda/Interaction/Response.hs-boot

src/full/Agda/Syntax/Abstract/Copatterns.hs

src/full/Agda/TypeChecking/Constraints.hs-boot

src/full/Agda/TypeChecking/Coverage/SplitTree.hs

src/full/Agda/TypeChecking/DropArgs.hs

src/full/Agda/TypeChecking/Errors.hs-boot

src/full/Agda/TypeChecking/InstanceArguments.hs

src/full/Agda/TypeChecking/InstanceArguments.hs-boot

src/full/Agda/TypeChecking/Monad/Base.hs-boot

src/full/Agda/TypeChecking/Monad/Sharing.hs

src/full/Agda/TypeChecking/ProjectionLike.hs

src/full/Agda/TypeChecking/ProjectionLike.hs-boot

src/full/Agda/TypeChecking/Rules/LHS/ProblemRest.hs

src/full/Agda/Utils/Geniplate.hs

src/full/Agda/Utils/HashMap.hs

src/full/Agda/Utils/Pointed.hs

src/full/Agda/Utils/Time.hs

src/main

src/main/Main.hs

files removed:
.pc/extend-mtl-dependenc

.pc/extend-mtl-dependenc/Agda.cabal

debian/patches/extend-mtl-dependenc

src/full/Agda/Interaction/GhciTop.hs

src/full/Agda/Syntax/Strict.hs

src/full/Agda/Utils/Generics.hs

src/full/Agda/Utils/IO/Locale.hs

files modified:
.pc/applied-patches

Agda.cabal

LICENSE

README

debian/50agda.el

debian/changelog

debian/control

debian/patches/series

dist/build/Agda/Syntax/Parser/Lexer.hs

dist/build/Agda/Syntax/Parser/Parser.hs

src/agda-mode/Main.hs

src/data/Agda.css

src/data/EpicInclude/AgdaPrelude.e

src/data/emacs-mode/agda-input.el

src/data/emacs-mode/agda2-highlight.el

src/data/emacs-mode/agda2-mode.el

src/data/emacs-mode/annotation.el

src/full/Agda/Auto/Auto.hs

src/full/Agda/Auto/Convert.hs

src/full/Agda/Compiler/Epic/CompileState.hs

src/full/Agda/Compiler/Epic/Compiler.hs

src/full/Agda/Compiler/Epic/Epic.hs

src/full/Agda/Compiler/Epic/Erasure.hs

src/full/Agda/Compiler/Epic/ForceConstrs.hs

src/full/Agda/Compiler/Epic/Forcing.hs

src/full/Agda/Compiler/Epic/FromAgda.hs

src/full/Agda/Compiler/Epic/Injection.hs

src/full/Agda/Compiler/Epic/NatDetection.hs

src/full/Agda/Compiler/Epic/Primitive.hs

src/full/Agda/Compiler/Epic/Smashing.hs

src/full/Agda/Compiler/Epic/Static.hs

src/full/Agda/Compiler/HaskellTypes.hs

src/full/Agda/Compiler/JS/Compiler.hs

src/full/Agda/Compiler/JS/Substitution.hs

src/full/Agda/Compiler/JS/Syntax.hs

src/full/Agda/Compiler/MAlonzo/Compiler.hs

src/full/Agda/Compiler/MAlonzo/Misc.hs

src/full/Agda/Compiler/MAlonzo/Pretty.hs

src/full/Agda/Compiler/MAlonzo/Primitives.hs

src/full/Agda/Interaction/BasicOps.hs

src/full/Agda/Interaction/CommandLine/CommandLine.hs

src/full/Agda/Interaction/EmacsCommand.hs

src/full/Agda/Interaction/Exceptions.hs

src/full/Agda/Interaction/FindFile.hs

src/full/Agda/Interaction/Highlighting/Emacs.hs

src/full/Agda/Interaction/Highlighting/Generate.hs

src/full/Agda/Interaction/Highlighting/Precise.hs

src/full/Agda/Interaction/Highlighting/Range.hs

src/full/Agda/Interaction/Highlighting/Vim.hs

src/full/Agda/Interaction/Imports.hs

src/full/Agda/Interaction/MakeCase.hs

src/full/Agda/Interaction/Options.hs

src/full/Agda/Main.hs

src/full/Agda/Syntax/Abstract.hs

src/full/Agda/Syntax/Abstract/Name.hs

src/full/Agda/Syntax/Abstract/Views.hs

src/full/Agda/Syntax/Common.hs

src/full/Agda/Syntax/Concrete.hs

src/full/Agda/Syntax/Concrete/Definitions.hs

src/full/Agda/Syntax/Concrete/Name.hs

src/full/Agda/Syntax/Concrete/Operators.hs

src/full/Agda/Syntax/Concrete/Operators/Parser.hs

src/full/Agda/Syntax/Concrete/Pretty.hs

src/full/Agda/Syntax/Fixity.hs

src/full/Agda/Syntax/Info.hs

src/full/Agda/Syntax/Internal.hs

src/full/Agda/Syntax/Internal/Generic.hs

src/full/Agda/Syntax/Literal.hs

src/full/Agda/Syntax/Notation.hs

src/full/Agda/Syntax/Parser.hs

src/full/Agda/Syntax/Parser/LexActions.hs

src/full/Agda/Syntax/Parser/Lexer.x

src/full/Agda/Syntax/Parser/Parser.y

src/full/Agda/Syntax/Parser/Tokens.hs

src/full/Agda/Syntax/Position.hs

src/full/Agda/Syntax/Scope/Base.hs

src/full/Agda/Syntax/Scope/Monad.hs

src/full/Agda/Syntax/Translation/AbstractToConcrete.hs

src/full/Agda/Syntax/Translation/ConcreteToAbstract.hs

src/full/Agda/Syntax/Translation/InternalToAbstract.hs

src/full/Agda/Termination/CallGraph.hs

src/full/Agda/Termination/Lexicographic.hs

src/full/Agda/Termination/Matrix.hs

src/full/Agda/Termination/SparseMatrix.hs

src/full/Agda/Termination/TermCheck.hs

src/full/Agda/Termination/Termination.hs

src/full/Agda/Tests.hs

src/full/Agda/TypeChecking/Abstract.hs

src/full/Agda/TypeChecking/CompiledClause.hs

src/full/Agda/TypeChecking/CompiledClause/Compile.hs

src/full/Agda/TypeChecking/CompiledClause/Compile.hs-boot

src/full/Agda/TypeChecking/CompiledClause/Match.hs

src/full/Agda/TypeChecking/Constraints.hs

src/full/Agda/TypeChecking/Conversion.hs

src/full/Agda/TypeChecking/Coverage.hs

src/full/Agda/TypeChecking/Coverage/Match.hs

src/full/Agda/TypeChecking/Datatypes.hs

src/full/Agda/TypeChecking/DisplayForm.hs

src/full/Agda/TypeChecking/Eliminators.hs

src/full/Agda/TypeChecking/Empty.hs

src/full/Agda/TypeChecking/Empty.hs-boot

src/full/Agda/TypeChecking/Errors.hs

src/full/Agda/TypeChecking/EtaContract.hs

src/full/Agda/TypeChecking/Forcing.hs

src/full/Agda/TypeChecking/Free.hs

src/full/Agda/TypeChecking/Implicit.hs

src/full/Agda/TypeChecking/Injectivity.hs

src/full/Agda/TypeChecking/Irrelevance.hs

src/full/Agda/TypeChecking/Level.hs

src/full/Agda/TypeChecking/LevelConstraints.hs

src/full/Agda/TypeChecking/MetaVars.hs

src/full/Agda/TypeChecking/MetaVars.hs-boot

src/full/Agda/TypeChecking/MetaVars/Mention.hs

src/full/Agda/TypeChecking/MetaVars/Occurs.hs

src/full/Agda/TypeChecking/Monad.hs

src/full/Agda/TypeChecking/Monad/Base.hs

src/full/Agda/TypeChecking/Monad/Builtin.hs

src/full/Agda/TypeChecking/Monad/Constraints.hs

src/full/Agda/TypeChecking/Monad/Context.hs

src/full/Agda/TypeChecking/Monad/Context.hs-boot

src/full/Agda/TypeChecking/Monad/Debug.hs

src/full/Agda/TypeChecking/Monad/Env.hs

src/full/Agda/TypeChecking/Monad/Exception.hs

src/full/Agda/TypeChecking/Monad/Imports.hs

src/full/Agda/TypeChecking/Monad/MetaVars.hs

src/full/Agda/TypeChecking/Monad/Mutual.hs

src/full/Agda/TypeChecking/Monad/Open.hs

src/full/Agda/TypeChecking/Monad/Options.hs

src/full/Agda/TypeChecking/Monad/Signature.hs

src/full/Agda/TypeChecking/Monad/SizedTypes.hs

src/full/Agda/TypeChecking/Monad/State.hs

src/full/Agda/TypeChecking/Monad/Trace.hs

src/full/Agda/TypeChecking/Patterns/Match.hs

src/full/Agda/TypeChecking/Polarity.hs

src/full/Agda/TypeChecking/Polarity.hs-boot

src/full/Agda/TypeChecking/Positivity.hs

src/full/Agda/TypeChecking/Pretty.hs

src/full/Agda/TypeChecking/Primitive.hs

src/full/Agda/TypeChecking/Quote.hs

src/full/Agda/TypeChecking/RecordPatterns.hs

src/full/Agda/TypeChecking/Records.hs

src/full/Agda/TypeChecking/Records.hs-boot

src/full/Agda/TypeChecking/Reduce.hs

src/full/Agda/TypeChecking/Rules/Builtin.hs

src/full/Agda/TypeChecking/Rules/Builtin/Coinduction.hs

src/full/Agda/TypeChecking/Rules/Builtin/Coinduction.hs-boot

src/full/Agda/TypeChecking/Rules/Data.hs

src/full/Agda/TypeChecking/Rules/Decl.hs

src/full/Agda/TypeChecking/Rules/Def.hs

src/full/Agda/TypeChecking/Rules/LHS.hs

src/full/Agda/TypeChecking/Rules/LHS/Implicit.hs

src/full/Agda/TypeChecking/Rules/LHS/Instantiate.hs

src/full/Agda/TypeChecking/Rules/LHS/Problem.hs

src/full/Agda/TypeChecking/Rules/LHS/Split.hs

src/full/Agda/TypeChecking/Rules/LHS/Unify.hs

src/full/Agda/TypeChecking/Rules/Record.hs

src/full/Agda/TypeChecking/Rules/Term.hs

src/full/Agda/TypeChecking/Rules/Term.hs-boot

src/full/Agda/TypeChecking/Serialise.hs

src/full/Agda/TypeChecking/SizedTypes.hs

src/full/Agda/TypeChecking/Substitute.hs

src/full/Agda/TypeChecking/Telescope.hs

src/full/Agda/TypeChecking/Test/Generators.hs

src/full/Agda/TypeChecking/Tests.hs

src/full/Agda/TypeChecking/UniversePolymorphism.hs

src/full/Agda/TypeChecking/With.hs

src/full/Agda/Utils/Either.hs

src/full/Agda/Utils/FileName.hs

src/full/Agda/Utils/Graph.hs

src/full/Agda/Utils/IO/UTF8.hs

src/full/Agda/Utils/List.hs

src/full/Agda/Utils/Map.hs

src/full/Agda/Utils/Maybe.hs

src/full/Agda/Utils/Monad.hs

src/full/Agda/Utils/Permutation.hs

src/full/Agda/Utils/Pointer.hs

src/full/Agda/Utils/String.hs

src/full/Agda/Utils/Suffix.hs

src/full/Agda/Utils/TestHelpers.hs

src/full/Agda/Utils/Tuple.hs

src/full/Agda/Utils/VarSet.hs

src/full/Agda/Utils/Warshall.hs

Show diffs side-by-side

added added

removed removed

src/full/Agda/Termination/Matrix.hs

1

{-# LANGUAGE GeneralizedNewtypeDeriving #-}

1

2

-- | Naive implementation of simple matrix library.

2

3

3

4

-- Originally copied from Agda1 sources.

96

97

-- | Type of matrices, parameterised on the type of values.

97

98

98

99

newtype Matrix i b = M { unM :: Array (MIx i) b }

99

deriving (Eq, Ord)

100

deriving (Eq, Ord, Functor)

100

101

101

102

matrixInvariant :: (Num i, Ix i) => Matrix i b -> Bool

102

103

matrixInvariant m =

Older »