idris-0.9.9: idris.cabal
Name: idris
Version: 0.9.9
License: BSD3
License-file: LICENSE
Author: Edwin Brady
Maintainer: Edwin Brady <eb@cs.st-andrews.ac.uk>
Homepage: http://www.idris-lang.org/
Stability: Beta
Category: Compilers/Interpreters, Dependent Types
Synopsis: Functional Programming Language with Dependent Types
Description: Idris is a general purpose language with full dependent types.
It is compiled, with eager evaluation.
Dependent types allow types to be predicated on values,
meaning that some aspects of a program's behaviour can be
specified precisely in the type. The language is closely
related to Epigram and Agda. There is a tutorial at <http://www.idris-lang.org/documentation>.
Features include:
.
* Full dependent types with dependent pattern matching
.
* where clauses, with rule, simple case expressions,
pattern matching let and lambda bindings
.
* Type classes, monad comprehensions
.
* do notation, idiom brackets, syntactic conveniences for lists,
tuples, dependent pairs
.
* Totality checking
.
* Coinductive types
.
* Indentation significant syntax, extensible syntax
.
* Tactic based theorem proving (influenced by Coq)
.
* Cumulative universes
.
* Simple foreign function interface (to C)
.
* Hugs style interactive environment
Cabal-Version: >= 1.6
Build-type: Custom
Data-files: rts/idris_rts.h rts/idris_gc.h rts/idris_stdfgn.h
rts/idris_main.c rts/idris_gmp.h
rts/libtest.c
js/Runtime-common.js
js/Runtime-node.js
js/Runtime-browser.js
Extra-source-files: lib/Makefile lib/*.idr lib/Prelude/*.idr
lib/Network/*.idr lib/Control/*.idr
lib/Control/Monad/*.idr lib/Language/*.idr
lib/Language/Reflection/*.idr
lib/System/Concurrency/*.idr
lib/Data/*.idr lib/Debug/*.idr
lib/Data/Vect/*.idr
lib/Decidable/*.idr
tutorial/examples/*.idr lib/base.ipkg
effects/Makefile effects/*.idr effects/Effect/*.idr
effects/effects.ipkg
javascript/Makefile
javascript/JavaScript/*.idr
javascript/*.idr
javascript/javascript.ipkg
config.mk
rts/*.c rts/*.h rts/Makefile
llvm/*.c llvm/Makefile
js/*.js
java/*.xml
Makefile
test/Makefile
test/runtest.pl
test/reg001/run
test/reg001/*.idr
test/reg001/expected
test/reg002/run
test/reg002/*.idr
test/reg002/expected
test/reg003/run
test/reg003/*.idr
test/reg003/expected
test/reg004/run
test/reg004/*.idr
test/reg004/expected
test/reg005/run
test/reg005/*.idr
test/reg005/expected
test/reg006/run
test/reg006/*.idr
test/reg006/expected
test/reg007/run
test/reg007/*.lidr
test/reg007/expected
test/reg008/run
test/reg008/*.idr
test/reg008/expected
test/reg009/run
test/reg009/*.lidr
test/reg009/expected
test/reg010/run
test/reg010/*.idr
test/reg010/expected
test/reg011/run
test/reg011/*.idr
test/reg011/expected
test/reg012/run
test/reg012/*.lidr
test/reg012/expected
test/reg013/run
test/reg013/*.idr
test/reg013/expected
test/reg014/run
test/reg014/*.idr
test/reg014/expected
test/reg015/run
test/reg015/*.idr
test/reg015/expected
test/reg016/run
test/reg016/*.idr
test/reg016/expected
test/reg017/run
test/reg017/*.idr
test/reg017/expected
test/reg018/run
test/reg018/*.idr
test/reg018/expected
test/reg019/run
test/reg019/*.idr
test/reg019/expected
test/reg020/run
test/reg020/*.idr
test/reg020/expected
test/test001/run
test/test001/*.idr
test/test001/expected
test/test002/run
test/test002/*.idr
test/test002/expected
test/test003/run
test/test003/*.lidr
test/test003/expected
test/test004/run
test/test004/*.idr
test/test004/expected
test/test005/run
test/test005/*.idr
test/test005/expected
test/test006/run
test/test006/*.idr
test/test006/expected
test/test007/run
test/test007/*.idr
test/test007/expected
test/test008/run
test/test008/*.idr
test/test008/expected
test/test009/run
test/test009/*.idr
test/test009/expected
test/test010/run
test/test010/*.idr
test/test010/expected
test/test011/run
test/test011/*.idr
test/test011/expected
test/test012/run
test/test012/*.idr
test/test012/expected
test/test013/run
test/test013/*.idr
test/test013/expected
test/test014/run
test/test014/*.idr
test/test014/test
test/test014/expected
test/test015/run
test/test015/*.idr
test/test015/expected
test/test016/run
test/test016/*.idr
test/test016/expected
test/test017/run
test/test017/*.idr
test/test017/expected
test/test018/run
test/test018/*.idr
test/test018/expected
test/test019/run
test/test019/*.lidr
test/test019/expected
test/test020/run
test/test020/*.idr
test/test020/expected
test/test021/run
test/test021/*.idr
test/test021/testFile
test/test021/expected
test/test022/run
test/test022/*.idr
test/test022/expected
test/test023/run
test/test023/*.idr
test/test023/expected
test/test024/run
test/test024/*.idr
test/test024/input
test/test024/expected
test/test025/run
test/test025/*.idr
test/test025/expected
test/test026/run
test/test026/*.idr
test/test026/input
test/test026/theType
test/test026/theOtherType
test/test026/expected
test/test027/run
test/test027/*.idr
test/test027/expected
test/test028/run
test/test028/*.idr
test/test028/expected
source-repository head
type: git
location: git://github.com/edwinb/Idris-dev.git
Flag NoEffects
Description: Do not build the effects package
Default: False
Flag LLVM
Description: Build the LLVM backend
Default: True
manual: True
Executable idris
Main-is: Main.hs
hs-source-dirs: src
Other-modules: Core.TT, Core.Evaluate, Core.Execute, Core.Typecheck,
Core.ProofShell, Core.ProofState, Core.CoreParser,
Core.ShellParser, Core.Unify, Core.Elaborate,
Core.CaseTree, Core.Constraints,
Idris.AbsSyntax, Idris.AbsSyntaxTree,
Idris.Parser, Idris.Help, Idris.IdeSlave, Idris.REPL,
Idris.REPLParser, Idris.ElabDecls, Idris.Error,
Idris.Delaborate, Idris.Primitives, Idris.Imports,
Idris.Compiler, Idris.Prover, Idris.ElabTerm,
Idris.Coverage, Idris.IBC, Idris.Unlit,
Idris.DataOpts, Idris.Transforms, Idris.DSL,
Idris.UnusedArgs, Idris.Docs, Idris.Completion,
Idris.PartialEval, Idris.Providers,
Util.Pretty, Util.System, Util.DynamicLinker,
Pkg.Package, Pkg.PParser,
IRTS.Lang, IRTS.LParser, IRTS.Bytecode, IRTS.Simplified,
IRTS.CodegenC, IRTS.Defunctionalise, IRTS.Inliner,
IRTS.Compiler, IRTS.CodegenJava, IRTS.Java.ASTBuilding,
IRTS.Java.JTypes, IRTS.Java.Mangling, IRTS.BCImp,
IRTS.CodegenJavaScript,
IRTS.CodegenCommon, IRTS.DumpBC
Paths_idris
Build-depends: base>=4 && <5, parsec>=3, mtl, Cabal,
haskeline>=0.7, split, directory,
containers, process, transformers, filepath,
directory, binary, bytestring, text, pretty,
language-java>=0.2.2, libffi,
vector, vector-binary-instances
Extensions: MultiParamTypeClasses, FunctionalDependencies,
FlexibleInstances, TemplateHaskell
ghc-prof-options: -auto-all -caf-all
ghc-options: -rtsopts
if os(linux)
cpp-options: -DLINUX
build-depends: unix
if os(darwin)
cpp-options: -DMACOSX
build-depends: unix
if os(windows)
cpp-options: -DWINDOWS
build-depends: Win32
if flag(LLVM)
other-modules: IRTS.CodegenLLVM
cpp-options: -DIDRIS_LLVM
build-depends: llvm-general==3.3.5.*
else
other-modules: Util.LLVMStubs