~ubuntu-branches/ubuntu/raring/agda/raring-proposed

« back to all changes in this revision

Viewing changes to Agda.cabal

Committer: Bazaar Package Importer
Author(s): Iain Lane
Date: 2009-07-20 19:49:41 UTC
Revision ID: james.westby@ubuntu.com-20090720194941-hcjy91vrn16csh7d

Tags: upstream-2.2.4+dfsg

Import upstream version 2.2.4+dfsg

files added:

Agda.cabal

LICENSE

README

Setup.hs

dist

dist/build

dist/build/Agda

dist/build/Agda/Syntax

dist/build/Agda/Syntax/Parser

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

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

doc/release-notes

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

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

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

src/agda-mode

src/agda-mode/Main.hs

src/data

src/data/Agda.css

src/data/emacs-mode

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

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

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

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

src/data/emacs-mode/agda2.el

src/data/emacs-mode/annotation.el

src/data/emacs-mode/eri.el

src/full

src/full/Agda

src/full/Agda/Compiler

src/full/Agda/Compiler/Agate

src/full/Agda/Compiler/Agate/Classify.hs

src/full/Agda/Compiler/Agate/Common.hs

src/full/Agda/Compiler/Agate/Main.hs

src/full/Agda/Compiler/Agate/OptimizedPrinter.hs

src/full/Agda/Compiler/Agate/TranslateName.hs

src/full/Agda/Compiler/Agate/UntypedPrinter.hs

src/full/Agda/Compiler/Alonzo

src/full/Agda/Compiler/Alonzo/Haskell.hs

src/full/Agda/Compiler/Alonzo/Main.hs

src/full/Agda/Compiler/Alonzo/Names.hs

src/full/Agda/Compiler/Alonzo/PatternMonad.hs

src/full/Agda/Compiler/HaskellTypes.hs

src/full/Agda/Compiler/MAlonzo

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

src/full/Agda/Compiler/MAlonzo/Encode.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

src/full/Agda/Interaction/BasicOps.hs

src/full/Agda/Interaction/CommandLine

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

src/full/Agda/Interaction/Exceptions.hs

src/full/Agda/Interaction/GhciTop.hs

src/full/Agda/Interaction/Highlighting

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

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

src/full/Agda/Interaction/Highlighting/HTML.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/Imports.hs-boot

src/full/Agda/Interaction/MakeCase.hs

src/full/Agda/Interaction/Monad.hs

src/full/Agda/Interaction/Options.hs

src/full/Agda/Main.hs

src/full/Agda/Syntax

src/full/Agda/Syntax/Abstract

src/full/Agda/Syntax/Abstract.hs

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

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

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

src/full/Agda/Syntax/Common.hs

src/full/Agda/Syntax/Concrete

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

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

src/full/Agda/Syntax/Internal.hs

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

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

src/full/Agda/Syntax/Literal.hs

src/full/Agda/Syntax/Parser

src/full/Agda/Syntax/Parser.hs

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

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

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

src/full/Agda/Syntax/Parser/Layout.hs-boot

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

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

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

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

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

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

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

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

src/full/Agda/Syntax/Position.hs

src/full/Agda/Syntax/Scope

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

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

src/full/Agda/Syntax/Strict.hs

src/full/Agda/Syntax/Translation

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

src/full/Agda/Termination/CallGraph.hs

src/full/Agda/Termination/Lexicographic.hs

src/full/Agda/Termination/Matrix.hs

src/full/Agda/Termination/Semiring.hs

src/full/Agda/Termination/TermCheck.hs

src/full/Agda/Termination/Termination.hs

src/full/Agda/Tests.hs

src/full/Agda/TypeChecker.hs

src/full/Agda/TypeChecking

src/full/Agda/TypeChecking/Abstract.hs

src/full/Agda/TypeChecking/Constraints.hs

src/full/Agda/TypeChecking/Conversion.hs

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

src/full/Agda/TypeChecking/Coverage

src/full/Agda/TypeChecking/Coverage.hs

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

src/full/Agda/TypeChecking/DisplayForm.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/Free.hs

src/full/Agda/TypeChecking/Implicit.hs

src/full/Agda/TypeChecking/Injectivity.hs

src/full/Agda/TypeChecking/MetaVars.hs

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

src/full/Agda/TypeChecking/Monad

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/Closure.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/Statistics.hs

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

src/full/Agda/TypeChecking/Patterns

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

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

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/Rebind.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

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

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

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

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

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

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

src/full/Agda/TypeChecking/Rules/LHS

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

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

src/full/Agda/TypeChecking/Tests.hs

src/full/Agda/TypeChecking/With.hs

src/full/Agda/Utils

src/full/Agda/Utils/Char.hs

src/full/Agda/Utils/Either.hs

src/full/Agda/Utils/FileName.hs

src/full/Agda/Utils/Fresh.hs

src/full/Agda/Utils/Function.hs

src/full/Agda/Utils/Generics.hs

src/full/Agda/Utils/Graph.hs

src/full/Agda/Utils/Hash.hs

src/full/Agda/Utils/IO.hs

src/full/Agda/Utils/Impossible.hs

src/full/Agda/Utils/List.hs

src/full/Agda/Utils/Map.hs

src/full/Agda/Utils/Maybe.hs

src/full/Agda/Utils/Monad

src/full/Agda/Utils/Monad.hs

src/full/Agda/Utils/Monad/Undo.hs

src/full/Agda/Utils/Permutation.hs

src/full/Agda/Utils/Pointer.hs

src/full/Agda/Utils/Pretty.hs

src/full/Agda/Utils/QuickCheck.hs

src/full/Agda/Utils/ReadP.hs

src/full/Agda/Utils/SemiRing.hs

src/full/Agda/Utils/Serialise.hs

src/full/Agda/Utils/Size.hs

src/full/Agda/Utils/String.hs

src/full/Agda/Utils/Suffix.hs

src/full/Agda/Utils/TestHelpers.hs

src/full/Agda/Utils/Trace.hs

src/full/Agda/Utils/Trie.hs

src/full/Agda/Utils/Tuple.hs

src/full/Agda/Utils/Unicode.hs

src/full/Agda/Utils/Warshall.hs

src/full/Agda/Version.hs

src/full/Agda/undefined.h

Show diffs side-by-side

added added

removed removed

Agda.cabal

name: Agda

version: 2.2.4

cabal-version: >= 1.6.0.3 && < 2

build-type: Simple

license: OtherLicense

license-file: LICENSE

author: Ulf Norell, Nils Anders Danielsson, Catarina Coquand, Makoto Takeyama, Andreas Abel, ...

maintainer: Ulf Norell <ulfn@chalmers.se>

homepage: http://wiki.portal.chalmers.se/agda/

bug-reports: http://code.google.com/p/agda/issues/list

category: Dependent types

synopsis: A dependently typed functional programming language and proof assistant

description:

Agda is a dependently typed functional programming language: It has

inductive families, which are similar to Haskell's GADTs, but they

can be indexed by values and not just types. It also has

parameterised modules, mixfix operators, Unicode characters, and an

interactive Emacs interface (the type checker can assist in the

development of your code).

Agda is also a proof assistant: It is an interactive system for

writing and checking proofs. Agda is based on intuitionistic type

theory, a foundational system for constructive mathematics developed

by the Swedish logician Per Martin-Löf. It has many similarities

with other proof assistants based on dependent types, such as Coq,

Epigram and NuPRL.

Note that if you want to use the command-line program (agda), then

you should also install the Agda-executable package. The Agda

package includes an Emacs mode for Agda, but you need to set up the

Emacs mode yourself (for instance by running @agda-mode setup@; see

the README).

Note also that this library does not follow the package versioning

policy, because the library is only intended to be used by the Emacs

mode and the Agda-executable package.

tested-with: GHC == 6.10.3

extra-source-files: src/full/Agda/undefined.h

README

doc/release-notes/*.txt

data-dir: src/data

data-files: Agda.css

emacs-mode/*.el

source-repository head

type: darcs

location: http://code.haskell.org/Agda/

source-repository this

type: darcs

location: http://code.haskell.org/Agda/

tag: 2.2.4

library

hs-source-dirs: src/full

build-depends: base >= 4.1 && < 4.2,

mtl >= 1.1 && < 2,

QuickCheck == 2.1.0.1,

haskell98 >= 1.0.1 && < 2,

haskell-src >= 1.0.1.1 && < 2,

containers >= 0.1.0 && < 1,

pretty >= 1 && < 2,

directory >= 1 && < 2,

old-time >= 1 && < 2,

bytestring >= 0.9.0.1 && < 1,

array >= 0.1 && < 1,

binary >= 0.4.4 && < 0.6,

zlib >= 0.4.0.1 && < 1,

filepath >= 1.1 && < 2,

process >= 1.0.1.0 && < 2,

haskeline >= 0.3 && < 0.7,

utf8-string >= 0.3 && < 0.4,

xhtml >= 3000.2 && < 3000.3,

syb >= 0.1 && < 0.2

if impl(ghc >= 6.10)

build-depends: ghc-prim >= 0.1 && < 1

build-tools: happy >= 1.15 && < 2,

alex >= 2.0.1 && < 3

exposed-modules: Agda.Main

Agda.Interaction.BasicOps

Agda.Interaction.GhciTop

Agda.Compiler.Agate.Classify

Agda.Compiler.Agate.Common

Agda.Compiler.Agate.Main

Agda.Compiler.Agate.OptimizedPrinter

Agda.Compiler.Agate.TranslateName

Agda.Compiler.Agate.UntypedPrinter

Agda.Compiler.Alonzo.Main

Agda.Compiler.Alonzo.Names

Agda.Compiler.Alonzo.Haskell

Agda.Compiler.Alonzo.PatternMonad

Agda.Compiler.HaskellTypes

Agda.Compiler.MAlonzo.Compiler

Agda.Compiler.MAlonzo.Encode

Agda.Compiler.MAlonzo.Misc

Agda.Compiler.MAlonzo.Pretty

Agda.Compiler.MAlonzo.Primitives

Agda.Interaction.CommandLine.CommandLine

Agda.Interaction.Exceptions

100

Agda.Interaction.Highlighting.Emacs

101

Agda.Interaction.Highlighting.Generate

102

Agda.Interaction.Highlighting.HTML

103

Agda.Interaction.Highlighting.Precise

104

Agda.Interaction.Highlighting.Range

105

Agda.Interaction.Highlighting.Vim

106

Agda.Interaction.Imports

107

Agda.Interaction.MakeCase

108

Agda.Interaction.Monad

109

Agda.Interaction.Options

110

Agda.Syntax.Abstract.Name

111

Agda.Syntax.Abstract.Pretty

112

Agda.Syntax.Abstract.Views

113

Agda.Syntax.Abstract

114

Agda.Syntax.Common

115

Agda.Syntax.Concrete.Definitions

116

Agda.Syntax.Concrete.Name

117

Agda.Syntax.Concrete.Operators.Parser

118

Agda.Syntax.Concrete.Operators

119

Agda.Syntax.Concrete.Pretty

120

Agda.Syntax.Concrete

121

Agda.Syntax.Fixity

122

Agda.Syntax.Info

123

Agda.Syntax.Internal

124

Agda.Syntax.Internal.Generic

125

Agda.Syntax.Internal.Pattern

126

Agda.Syntax.Literal

127

Agda.Syntax.Parser.Alex

128

Agda.Syntax.Parser.Comments

129

Agda.Syntax.Parser.Layout

130

Agda.Syntax.Parser.LexActions

131

Agda.Syntax.Parser.Lexer

132

Agda.Syntax.Parser.LookAhead

133

Agda.Syntax.Parser.Monad

134

Agda.Syntax.Parser.Parser

135

Agda.Syntax.Parser.StringLiterals

136

Agda.Syntax.Parser.Tokens

137

Agda.Syntax.Parser

138

Agda.Syntax.Position

139

Agda.Syntax.Scope.Base

140

Agda.Syntax.Scope.Monad

141

Agda.Syntax.Strict

142

Agda.Syntax.Translation.AbstractToConcrete

143

Agda.Syntax.Translation.ConcreteToAbstract

144

Agda.Syntax.Translation.InternalToAbstract

145

Agda.Termination.CallGraph

146

Agda.Termination.Lexicographic

147

Agda.Termination.Matrix

148

Agda.Termination.Semiring

149

Agda.Termination.TermCheck

150

Agda.Termination.Termination

151

Agda.Tests

152

Agda.TypeChecker

153

Agda.TypeChecking.Abstract

154

Agda.TypeChecking.Constraints

155

Agda.TypeChecking.Conversion

156

Agda.TypeChecking.Coverage

157

Agda.TypeChecking.Coverage.Match

158

Agda.TypeChecking.DisplayForm

159

Agda.TypeChecking.Empty

160

Agda.TypeChecking.EtaContract

161

Agda.TypeChecking.Errors

162

Agda.TypeChecking.Free

163

Agda.TypeChecking.Implicit

164

Agda.TypeChecking.Injectivity

165

Agda.TypeChecking.MetaVars

166

Agda.TypeChecking.Monad.Base

167

Agda.TypeChecking.Monad.Builtin

168

Agda.TypeChecking.Monad.Closure

169

Agda.TypeChecking.Monad.Constraints

170

Agda.TypeChecking.Monad.Context

171

Agda.TypeChecking.Monad.Debug

172

Agda.TypeChecking.Monad.Env

173

Agda.TypeChecking.Monad.Exception

174

Agda.TypeChecking.Monad.Imports

175

Agda.TypeChecking.Monad.MetaVars

176

Agda.TypeChecking.Monad.Mutual

177

Agda.TypeChecking.Monad.Open

178

Agda.TypeChecking.Monad.Options

179

Agda.TypeChecking.Monad.Signature

180

Agda.TypeChecking.Monad.SizedTypes

181

Agda.TypeChecking.Monad.State

182

Agda.TypeChecking.Monad.Statistics

183

Agda.TypeChecking.Monad.Trace

184

Agda.TypeChecking.Monad

185

Agda.TypeChecking.Patterns.Match

186

Agda.TypeChecking.Polarity

187

Agda.TypeChecking.Positivity

188

Agda.TypeChecking.Pretty

189

Agda.TypeChecking.Primitive

190

Agda.TypeChecking.Rebind

191

Agda.TypeChecking.Records

192

Agda.TypeChecking.Reduce

193

Agda.TypeChecking.Rules.Builtin

194

Agda.TypeChecking.Rules.Data

195

Agda.TypeChecking.Rules.Decl

196

Agda.TypeChecking.Rules.Def

197

Agda.TypeChecking.Rules.LHS

198

Agda.TypeChecking.Rules.LHS.Implicit

199

Agda.TypeChecking.Rules.LHS.Instantiate

200

Agda.TypeChecking.Rules.LHS.Problem

201

Agda.TypeChecking.Rules.LHS.Split

202

Agda.TypeChecking.Rules.LHS.Unify

203

Agda.TypeChecking.Rules.Record

204

Agda.TypeChecking.Rules.Term

205

Agda.TypeChecking.Serialise

206

Agda.TypeChecking.SizedTypes

207

Agda.TypeChecking.Substitute

208

Agda.TypeChecking.Telescope

209

Agda.TypeChecking.Test.Generators

210

Agda.TypeChecking.Tests

211

Agda.TypeChecking.With

212

Agda.Utils.Char

213

Agda.Utils.Either

214

Agda.Utils.FileName

215

Agda.Utils.Fresh

216

Agda.Utils.Function

217

Agda.Utils.Generics

218

Agda.Utils.Graph

219

Agda.Utils.Hash

220

Agda.Utils.Impossible

221

Agda.Utils.IO

222

Agda.Utils.List

223

Agda.Utils.Map

224

Agda.Utils.Maybe

225

Agda.Utils.Monad.Undo

226

Agda.Utils.Monad

227

Agda.Utils.Permutation

228

Agda.Utils.Pointer

229

Agda.Utils.Pretty

230

Agda.Utils.QuickCheck

231

Agda.Utils.ReadP

232

Agda.Utils.SemiRing

233

Agda.Utils.Serialise

234

Agda.Utils.Size

235

Agda.Utils.String

236

Agda.Utils.Suffix

237

Agda.Utils.TestHelpers

238

Agda.Utils.Trace

239

Agda.Utils.Trie

240

Agda.Utils.Tuple

241

Agda.Utils.Unicode

242

Agda.Utils.Warshall

243

Agda.Version

244

other-modules: Paths_Agda

245

ghc-options: -auto-all -w -Werror -fwarn-dodgy-imports

246

-fwarn-duplicate-exports -fwarn-hi-shadowing

247

-fwarn-incomplete-patterns -fwarn-missing-fields

248

-fwarn-missing-methods -fwarn-overlapping-patterns

249

if impl(ghc >= 6.10)

250

ghc-options: -fwarn-warnings-deprecations -fwarn-deprecated-flags

251

-fwarn-dodgy-foreign-imports

252

253

executable agda-mode

254

hs-source-dirs: src/agda-mode

255

main-is: Main.hs

256

other-modules: Paths_Agda

257

build-depends: base >= 4.1 && < 4.2,

258

filepath >= 1.1 && < 2,

259

process >= 1.0.1.0 && < 2,

260

utf8-string >= 0.3 && < 0.4

Older »