idris-0.9.14: idris.cabal
Name: idris
Version: 0.9.14
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.8
Build-type: Custom
Data-files: idrisdoc/styles.css
jsrts/Runtime-browser.js
jsrts/Runtime-common.js
jsrts/Runtime-node.js
jsrts/jsbn/jsbn.js
jsrts/jsbn/LICENSE
rts/idris_gc.h
rts/idris_gmp.h
rts/idris_main.c
rts/idris_rts.h
rts/idris_net.h
rts/idris_stdfgn.h
rts/libtest.c
Extra-source-files:
Makefile
config.mk
rts/*.c
rts/*.h
rts/windows/*.c
rts/Makefile
libs/Makefile
libs/prelude/prelude.ipkg
libs/prelude/Prelude/*.idr
libs/prelude/Decidable/*.idr
libs/prelude/Makefile
libs/prelude/*.idr
libs/base/base.ipkg
libs/base/*.idr
libs/base/Control/*.idr
libs/base/Control/Isomorphism/*.idr
libs/base/Control/Monad/*.idr
libs/base/Data/*.idr
libs/base/Data/Vect/*.idr
libs/base/Debug/*.idr
libs/base/Decidable/*.idr
libs/base/Language/*.idr
libs/base/Language/Reflection/*.idr
libs/base/Makefile
libs/base/Network/*.idr
libs/base/System/*.idr
libs/base/System/Concurrency/*.idr
libs/base/Syntax/*.idr
libs/effects/Makefile
libs/effects/effects.ipkg
libs/effects/Effect/*.idr
libs/effects/*.idr
llvm/*.c
llvm/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/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/reg021/run
test/reg021/*.idr
test/reg021/expected
test/reg022/run
test/reg022/*.idr
test/reg022/expected
test/reg023/run
test/reg023/*.idr
test/reg023/expected
test/reg024/run
test/reg024/*.idr
test/reg024/expected
test/reg025/run
test/reg025/*.idr
test/reg025/expected
test/reg026/run
test/reg026/*.idr
test/reg026/expected
test/reg027/run
test/reg027/*.idr
test/reg027/expected
test/reg028/run
test/reg028/*.idr
test/reg028/expected
test/reg029/run
test/reg029/*.idr
test/reg029/expected
test/reg030/run
test/reg030/*.idr
test/reg030/expected
test/reg031/run
test/reg031/*.idr
test/reg031/expected
test/reg032/run
test/reg032/*.idr
test/reg032/expected
test/reg033/run
test/reg033/*.idr
test/reg033/expected
test/reg034/run
test/reg034/*.idr
test/reg034/expected
test/reg035/run
test/reg035/*.idr
test/reg035/*.lidr
test/reg035/expected
test/reg036/run
test/reg036/*.idr
test/reg036/expected
test/reg037/run
test/reg037/*.idr
test/reg037/expected
test/reg038/run
test/reg038/*.idr
test/reg038/expected
test/reg039/run
test/reg039/*.idr
test/reg039/expected
test/reg040/run
test/reg040/*.idr
test/reg040/expected
test/reg041/run
test/reg041/*.idr
test/reg041/expected
test/reg042/run
test/reg042/*.idr
test/reg042/expected
test/reg044/run
test/reg044/*.idr
test/reg044/expected
test/reg045/run
test/reg045/*.idr
test/reg045/expected
test/reg046/run
test/reg046/*.idr
test/reg046/expected
test/reg047/run
test/reg047/*.idr
test/reg047/expected
test/basic001/run
test/basic001/*.idr
test/basic001/expected
test/basic002/run
test/basic002/*.idr
test/basic002/expected
test/basic003/run
test/basic003/*.idr
test/basic003/expected
test/basic004/run
test/basic004/*.idr
test/basic004/expected
test/basic005/run
test/basic005/*.lidr
test/basic005/expected
test/basic006/run
test/basic006/*.idr
test/basic006/expected
test/basic007/run
test/basic007/*.idr
test/basic007/expected
test/basic008/run
test/basic008/*.idr
test/basic008/expected
test/basic009/run
test/basic009/*.idr
test/basic009/expected
test/basic009/B/*.idr
test/basic010/run
test/basic010/*.idr
test/basic010/expected
test/buffer001-disabled/*.idr
test/buffer001-disabled/run
test/buffer001-disabled/expected
test/dsl001/run
test/dsl001/*.idr
test/dsl001/expected
test/dsl002/run
test/dsl002/test
test/dsl002/*.idr
test/dsl002/expected
test/dsl003/run
test/dsl003/*.idr
test/dsl003/expected
test/effects001/run
test/effects001/*.idr
test/effects001/expected
test/effects001/testFile
test/effects002/run
test/effects002/*.idr
test/effects002/expected
test/error001/run
test/error001/*.idr
test/error001/expected
test/error002/run
test/error002/*.idr
test/error002/expected
test/error003/run
test/error003/*.idr
test/error003/expected
test/error004/run
test/error004/*.idr
test/error004/expected
test/ffi001/run
test/ffi001/*.idr
test/ffi001/expected
test/ffi002/run
test/ffi002/*.idr
test/ffi002/expected
test/ffi003/run
test/ffi003/*.idr
test/ffi003/expected
test/ffi003/input
test/ffi004/run
test/ffi004/*.idr
test/ffi004/theType
test/ffi004/theOtherType
test/ffi004/expected
test/ffi005/*.idr
test/ffi005/run
test/ffi005/expected
test/idrisdoc001/run
test/idrisdoc001/expected
test/idrisdoc001/*.idr
test/idrisdoc001/*.ipkg
test/idrisdoc002/run
test/idrisdoc002/expected
test/idrisdoc002/*.idr
test/idrisdoc002/*.ipkg
test/idrisdoc003/run
test/idrisdoc003/expected
test/idrisdoc003/*.idr
test/idrisdoc003/*.ipkg
test/idrisdoc004/run
test/idrisdoc004/expected
test/idrisdoc004/*.idr
test/idrisdoc004/*.ipkg
test/idrisdoc005/run
test/idrisdoc005/expected
test/idrisdoc005/*.idr
test/idrisdoc005/*.ipkg
test/idrisdoc006/run
test/idrisdoc006/expected
test/idrisdoc006/A/fully/Qualified/NAME.idr
test/idrisdoc006/*.idr
test/idrisdoc006/*.ipkg
test/idrisdoc007/run
test/idrisdoc007/expected
test/idrisdoc007/*.idr
test/idrisdoc007/*.ipkg
test/idrisdoc008/run
test/idrisdoc008/expected
test/idrisdoc008/*.idr
test/idrisdoc008/*.ipkg
test/interactive001/run
test/interactive001/input
test/interactive001/*.idr
test/interactive001/expected
test/interactive002/run
test/interactive002/input
test/interactive002/*.idr
test/interactive002/expected
test/interactive003/run
test/interactive003/input
test/interactive003/*.idr
test/interactive003/expected
test/interactive004/run
test/interactive004/input
test/interactive004/*.idr
test/interactive004/expected
test/io001/run
test/io001/*.idr
test/io001/expected
test/io002/run
test/io002/*.idr
test/io002/expected
test/io003/run
test/io003/*.idr
test/io003/expected
test/literate001/run
test/literate001/*.lidr
test/literate001/expected
test/primitives001/run
test/primitives001/*.idr
test/primitives001/expected
test/primitives002/run
test/primitives002/expected
test/primitives003/run
test/primitives003/*.idr
test/primitives003/expected
test/proof001/run
test/proof001/*.idr
test/proof001/expected
test/proof002/run
test/proof002/*.idr
test/proof002/expected
test/proof003/run
test/proof003/*.idr
test/proof003/expected
test/proof004/run
test/proof004/*.idr
test/proof004/expected
test/quasiquote001/run
test/quasiquote001/*.idr
test/quasiquote001/expected
test/quasiquote002/run
test/quasiquote002/*.idr
test/quasiquote002/expected
test/quasiquote003/run
test/quasiquote003/*.idr
test/quasiquote003/expected
test/records001/run
test/records001/*.idr
test/records001/expected
test/records002/run
test/records002/*.idr
test/records002/expected
test/records003/run
test/records003/*.idr
test/records003/expected
test/sugar001/run
test/sugar001/*.idr
test/sugar001/expected
test/sugar002/run
test/sugar002/*.idr
test/sugar002/expected
test/sugar003/run
test/sugar003/*.idr
test/sugar003/expected
test/totality001/run
test/totality001/*.idr
test/totality001/expected
test/totality002/run
test/totality002/*.idr
test/totality002/expected
test/totality003/run
test/totality003/*.idr
test/totality003/expected
test/totality004/run
test/totality004/*.idr
test/totality004/expected
test/totality005/run
test/totality005/*.idr
test/totality005/expected
test/totality006/run
test/totality006/*.idr
test/totality006/expected
test/totality007/run
test/totality007/*.ipkg
test/totality007/src/*.idr
test/totality007/expected
test/totality008/run
test/totality008/*.idr
test/totality008/expected
test/tutorial001/run
test/tutorial001/*.idr
test/tutorial001/expected
test/tutorial002/run
test/tutorial002/*.idr
test/tutorial002/expected
test/tutorial003/run
test/tutorial003/*.idr
test/tutorial003/expected
test/tutorial004/run
test/tutorial004/*.idr
test/tutorial004/expected
test/tutorial005/run
test/tutorial005/*.idr
test/tutorial005/expected
test/tutorial006/run
test/tutorial006/*.idr
test/tutorial006/expected
source-repository head
type: git
location: git://github.com/idris-lang/Idris-dev.git
Flag LLVM
Description: Build the LLVM backend
Default: False
manual: True
Flag FFI
Description: Build support for libffi
Default: False
manual: True
Flag GMP
Description: Use GMP for Integers
Default: False
manual: True
Flag curses
Description: Use Curses to get the screen width
Default: False
manual: True
-- This flag determines whether to show Git hashes in version strings
-- Defaults to True because Hackage is a source release
Flag release
Description: This is an official release
Default: True
manual: True
Flag freestanding
Description: Build an Idris that doesn't use cabal
Default: False
manual: True
Library
hs-source-dirs: src
Exposed-modules:
Idris.Core.Binary
, Idris.Core.CaseTree
, Idris.Core.Constraints
, Idris.Core.DeepSeq
, Idris.Core.Elaborate
, Idris.Core.Evaluate
, Idris.Core.Execute
, Idris.Core.ProofState
, Idris.Core.TC
, Idris.Core.TT
, Idris.Core.Typecheck
, Idris.Core.Unify
, Idris.AbsSyntax
, Idris.AbsSyntaxTree
, Idris.Apropos
, Idris.ASTUtils
, Idris.CaseSplit
, Idris.Chaser
, Idris.Colours
, Idris.Completion
, Idris.Coverage
, Idris.DSL
, Idris.DataOpts
, Idris.DeepSeq
, Idris.Delaborate
, Idris.Docs
, Idris.Docstrings
, Idris.ElabDecls
, Idris.ElabQuasiquote
, Idris.ElabTerm
, Idris.Erasure
, Idris.Error
, Idris.ErrReverse
, Idris.Help
, Idris.IBC
, Idris.IdeSlave
, Idris.IdrisDoc
, Idris.Imports
, Idris.Inliner
, Idris.Interactive
, Idris.Output
, Idris.Parser
, Idris.ParseHelpers
, Idris.ParseOps
, Idris.ParseExpr
, Idris.ParseData
, Idris.PartialEval
, Idris.Primitives
, Idris.ProofSearch
, Idris.Prover
, Idris.Providers
, Idris.REPL
, Idris.REPLParser
, Idris.Transforms
, Idris.TypeSearch
, Idris.Unlit
, Idris.WhoCalls
, Idris.CmdOptions
, IRTS.BCImp
, IRTS.Bytecode
, IRTS.CodegenC
, IRTS.CodegenCommon
, IRTS.CodegenJava
, IRTS.CodegenJavaScript
, IRTS.JavaScript.AST
, IRTS.Compiler
, IRTS.Defunctionalise
, IRTS.DumpBC
, IRTS.Inliner
, IRTS.Java.ASTBuilding
, IRTS.Java.JTypes
, IRTS.Java.Mangling
, IRTS.Java.Pom
, IRTS.Lang
, IRTS.Simplified
, IRTS.System
, Pkg.Package
, Util.DynamicLinker
, Util.ScreenSize
Other-modules:
Util.Pretty
, Util.System
, Util.Net
, Util.Zlib
, Pkg.PParser
-- Auto Generated
, Paths_idris
, Version_idris
Build-depends: base >=4 && <5
, Cabal
, annotated-wl-pprint >= 0.5.3
, ansi-terminal
, ansi-wl-pprint
, base64-bytestring
, binary
, blaze-html >= 0.6.1.3
, blaze-markup >= 0.5.2.1 && < 0.7.0.0
, bytestring
, cheapskate
, containers >= 0.5
, directory
, directory >= 1.2
, filepath
, fingertree >= 0.1
, haskeline >= 0.7
, language-java >= 0.2.6
, lens >= 4.1.1
, mtl
, parsers >= 0.9 && < 0.11.0.2
, pretty
, process
, split
, text
, time >= 1.4
, transformers
, trifecta >= 1.1
, unordered-containers
, utf8-string
, vector
, vector-binary-instances
, network
, xml
, deepseq
, zlib
, optparse-applicative >= 0.8
Extensions: MultiParamTypeClasses
, FunctionalDependencies
, FlexibleContexts
, FlexibleInstances
, TemplateHaskell
ghc-prof-options: -auto-all -caf-all
ghc-options: -threaded -rtsopts
if os(linux)
cpp-options: -DLINUX
build-depends: unix
if os(freebsd)
cpp-options: -DFREEBSD
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.8.*
, llvm-general-pure == 3.3.8.*
else
other-modules: Util.LLVMStubs
if flag(FFI)
build-depends: libffi
cpp-options: -DIDRIS_FFI
if flag(GMP)
build-depends: libffi
cpp-options: -DIDRIS_GMP
if flag(curses)
build-depends: hscurses
cpp-options: -DCURSES
if flag(freestanding)
other-modules: Target_idris
cpp-options: -DFREESTANDING
Executable idris
Main-is: Main.hs
hs-source-dirs: main
Build-depends: idris
, base
, filepath
, haskeline >= 0.7
, transformers
ghc-prof-options: -auto-all -caf-all
ghc-options: -threaded -rtsopts -funbox-strict-fields