Name: idris Version: 0.9.14.3 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: 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/reg048/run test/reg048/*.idr test/reg048/expected test/reg049/run test/reg049/*.idr test/reg049/expected test/reg050/run test/reg050/*.idr test/reg050/expected test/reg051/run test/reg051/*.idr test/reg051/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/quasiquote004/run test/quasiquote004/*.idr test/quasiquote004/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 test/unique001/run test/unique001/*.idr test/unique001/expected test/unique002/run test/unique002/*.idr test/unique002/expected test/unique003/run test/unique003/*.idr test/unique003/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.ProofTerm , Idris.Core.TC , Idris.Core.TT , Idris.Core.Typecheck , Idris.Core.Unify , Idris.Elab.Utils , Idris.Elab.Type , Idris.Elab.Clause , Idris.Elab.Data , Idris.Elab.Record , Idris.Elab.Class , Idris.Elab.Instance , Idris.Elab.Provider , Idris.Elab.Value , 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.LangOpts , 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.13 , 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.10 Extensions: MultiParamTypeClasses , DeriveFoldable , DeriveTraversable , 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(dragonfly) -- cpp-options: -DDRAGONFLY -- 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 Executable idris-c Main-is: Main.hs hs-source-dirs: codegen/idris-c Build-depends: idris , base , filepath , haskeline >= 0.7 , transformers ghc-prof-options: -auto-all -caf-all ghc-options: -threaded -rtsopts -funbox-strict-fields Executable idris-javascript Main-is: Main.hs hs-source-dirs: codegen/idris-javascript Build-depends: idris , base , filepath , haskeline >= 0.7 , transformers ghc-prof-options: -auto-all -caf-all ghc-options: -threaded -rtsopts -funbox-strict-fields Executable idris-node Main-is: Main.hs hs-source-dirs: codegen/idris-node Build-depends: idris , base , filepath , haskeline >= 0.7 , transformers ghc-prof-options: -auto-all -caf-all ghc-options: -threaded -rtsopts -funbox-strict-fields