Name: idris Version: 0.9.11.2 License: BSD3 License-file: LICENSE Author: Edwin Brady Maintainer: Edwin Brady 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 . 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: 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/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/Concurrency/*.idr libs/base/Syntax/*.idr libs/effects/Makefile libs/effects/effects.ipkg libs/effects/Effect/*.idr libs/effects/*.idr libs/neweffects/Makefile libs/neweffects/neweffects.ipkg libs/neweffects/Effect/*.idr libs/neweffects/*.idr libs/javascript/*.idr libs/javascript/JavaScript/*.idr libs/javascript/Makefile libs/javascript/javascript.ipkg 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/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/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/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/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/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/interactive001/run test/interactive001/input test/interactive001/*.idr test/interactive001/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/records001/run test/records001/*.idr test/records001/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 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 Library hs-source-dirs: src Exposed-modules: 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.CaseSplit , Idris.Chaser , Idris.Colours , Idris.Completion , Idris.Coverage , Idris.DSL , Idris.DataOpts , Idris.DeepSeq , Idris.Delaborate , Idris.Docs , Idris.ElabDecls , Idris.ElabTerm , Idris.Error , Idris.ErrReverse , Idris.Help , Idris.IBC , Idris.IdeSlave , Idris.Imports , Idris.Inliner , 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.Unlit , Idris.UnusedArgs , IRTS.BCImp , IRTS.Bytecode , IRTS.CodegenC , IRTS.CodegenCommon , IRTS.CodegenJava , IRTS.CodegenJavaScript , 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 , binary , bytestring , containers >= 0.5 , directory , directory >= 1.2 , filepath , haskeline >= 0.7 , language-java >= 0.2.6 , mtl , parsers >= 0.9 , pretty , process , split , text , time >= 1.4 , transformers , trifecta >= 1.1 , unordered-containers , utf8-string , vector , vector-binary-instances , network , xml , deepseq , zlib 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 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