Name: idris Version: 1.3.0 License: BSD3 License-file: LICENSE Author: Edwin Brady Maintainer: Edwin Brady Homepage: http://www.idris-lang.org/ Bug-reports: https://github.com/idris-lang/Idris-dev/issues 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, first class, dependent types with dependent pattern matching . * where clauses, with rule, case expressions, pattern matching let and lambda bindings . * Interfaces (similar to type classes), monad comprehensions . * do notation, idiom brackets, syntactic conveniences for lists, tuples, dependent pairs . * Totality checking . * Coinductive types . * Indentation significant syntax, extensible syntax . * Cumulative universes . * Simple foreign function interface (to C) . * Hugs style interactive environment Cabal-Version: >= 1.22 Build-type: Custom Tested-With: GHC == 7.10.3, GHC == 8.0.1 Data-files: idrisdoc/styles.css jsrts/jsbn/jsbn-browser.js jsrts/jsbn/jsbn-node.js jsrts/Runtime-common.js jsrts/Runtime-javascript.js jsrts/Runtime-node.js jsrts/jsbn/LICENSE rts/arduino/idris_main.c rts/idris_bitstring.c rts/idris_bitstring.h rts/idris_gc.c rts/idris_gc.h rts/idris_gmp.c rts/idris_gmp.h rts/idris_heap.c rts/idris_heap.h rts/idris_main.c rts/idris_net.c rts/idris_net.h rts/idris_opts.c rts/idris_opts.h rts/idris_rts.c rts/idris_rts.h rts/idris_stats.c rts/idris_stats.h rts/idris_stdfgn.c rts/idris_stdfgn.h rts/mini-gmp.c rts/mini-gmp.h rts/libtest.c Extra-doc-files: CHANGELOG.md CITATION.md CONTRIBUTING.md CONTRIBUTORS README.md RELEASE-CHECKS.md idris-tutorial.pdf samples/effects/*.idr samples/misc/*.idr samples/misc/*.lidr samples/tutorial/*.idr -- extra-source-files is generated by Setup.hs using `git --ls-files`. Extra-source-files: source-repository head type: git location: git://github.com/idris-lang/Idris-dev.git custom-setup setup-depends: Cabal >= 1.10 && <2.3, base >= 4 && <5, directory, filepath, process Flag FFI Description: Build support for libffi Default: False manual: True Flag GMP Description: Use GMP for Integers 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 Flag CI Description: Built everything using "-Werror", meant for CI-builds only Default: False manual: True Flag execonly Description: Build executables only, skip the libraries and RTS 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.TT , Idris.Core.Typecheck , Idris.Core.Unify , Idris.Core.WHNF , Idris.Elab.Utils , Idris.Elab.Type , Idris.Elab.AsPat , Idris.Elab.Clause , Idris.Elab.Data , Idris.Elab.Record , Idris.Elab.Interface , Idris.Elab.Implementation , Idris.Elab.Provider , Idris.Elab.RunElab , Idris.Elab.Transform , Idris.Elab.Value , Idris.Elab.Term , Idris.Elab.Quasiquote , Idris.Elab.Rewrite , Idris.REPL.Browse , 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.Directives , Idris.Docs , Idris.Docstrings , Idris.ElabDecls , Idris.Erasure , Idris.Error , Idris.ErrReverse , Idris.Help , Idris.IBC , Idris.IdeMode , Idris.IdrisDoc , Idris.Imports , Idris.Info , Idris.Info.Show , Idris.Inliner , Idris.Interactive , Idris.Output , Idris.Main , Idris.ModeCommon , Idris.Options , Idris.Parser , Idris.Parser.Data , Idris.Parser.Expr , Idris.Parser.Helpers , Idris.Parser.Ops , Idris.Parser.Stack , Idris.PartialEval , Idris.Primitives , Idris.ProofSearch , Idris.Prover , Idris.Providers , Idris.Reflection , Idris.REPL , Idris.REPL.Parser , Idris.REPL.Commands , Idris.Termination , Idris.Transforms , Idris.TypeSearch , Idris.Unlit , Idris.WhoCalls , Idris.CmdOptions , IRTS.Bytecode , IRTS.CodegenC , IRTS.CodegenCommon , IRTS.CodegenJavaScript , IRTS.Exports , IRTS.JavaScript.AST , IRTS.JavaScript.Name , IRTS.JavaScript.Codegen , IRTS.JavaScript.LangTransforms , IRTS.JavaScript.Specialize , IRTS.JavaScript.PrimOp , IRTS.Compiler , IRTS.Defunctionalise , IRTS.DumpBC , IRTS.Inliner , IRTS.Lang , IRTS.LangOpts , IRTS.Portable , IRTS.Simplified , IRTS.System , Idris.Package , Idris.Package.Common , Idris.Package.Parser , Util.DynamicLinker , Util.ScreenSize , Util.System Other-modules: Util.Pretty , Util.Net -- Auto Generated , Paths_idris , Version_idris , Tools_idris , BuildFlags_idris Build-depends: base >=4 && <5 , aeson >= 0.6 && < 1.3 , annotated-wl-pprint >= 0.7 && < 0.8 , ansi-terminal < 0.9 , ansi-wl-pprint < 0.7 , array >= 0.4.0.1 && < 0.6 , base64-bytestring < 1.1 , binary >= 0.8.4.1 && < 0.9 , blaze-html >= 0.6.1.3 && < 0.10 , blaze-markup >= 0.5.2.1 && < 0.9 , bytestring < 0.11 , cheapskate >= 0.1.1 && < 0.2 , code-page >= 0.1 && < 0.2 , containers >= 0.5 && < 0.6 , deepseq < 1.5 , directory >= 1.2.2.0 && < 1.2.3.0 || > 1.2.3.0 , filepath < 1.5 , fingertree >= 0.1.4.1 && < 0.2 , haskeline >= 0.7 && < 0.8 , ieee754 >= 0.7 && < 0.9 , megaparsec >= 6.2 , mtl >= 2.1 && < 2.3 , network < 2.7 , optparse-applicative >= 0.13 && < 0.15 , pretty < 1.2 , process < 1.7 , regex-tdfa >= 1.2 , safe >= 0.3.9 , split < 0.3 , terminal-size < 0.4 , text >=1.2.1.0 && < 1.3 , time >= 1.4 && < 1.9 , transformers >= 0.5 && < 0.6 , uniplate >=1.6 && < 1.7 , unordered-containers < 0.3 , utf8-string < 1.1 , vector < 0.13 , vector-binary-instances < 0.3 , zip-archive > 0.2.3.5 && < 0.4 , fsnotify >= 0.2 && < 2.2 , async < 2.3 if !impl(ghc >= 8.0) Build-Depends: semigroups == 0.18.* Default-Language: Haskell2010 ghc-prof-options: -auto-all -caf-all if os(windows) build-depends: mintty >= 0.1 && < 0.2 , Win32 < 2.7 else build-depends: unix < 2.8 if flag(FFI) build-depends: libffi < 0.2 cpp-options: -DIDRIS_FFI if flag(GMP) build-depends: libffi < 0.2 extra-libraries: gmp cpp-options: -DIDRIS_GMP if flag(freestanding) other-modules: Target_idris cpp-options: -DFREESTANDING if flag(CI) ghc-options: -Werror Executable idris Main-is: Main.hs hs-source-dirs: main Build-depends: idris , base , filepath , directory , haskeline >= 0.7 , transformers Default-Language: Haskell2010 ghc-prof-options: -auto-all -caf-all ghc-options: -threaded -rtsopts -funbox-strict-fields -with-rtsopts=-I0 Test-suite regression-and-feature-tests Type: exitcode-stdio-1.0 Main-is: TestRun.hs Other-modules: TestData hs-source-dirs: test Build-depends: idris , base , containers , process , time , filepath , directory , haskeline >= 0.7 , optparse-applicative >= 0.13 && < 0.15 , tagged , tasty >= 0.8 , tasty-golden >= 2.0 , tasty-rerun >= 1.0.0 , bytestring , transformers Default-Language: Haskell2010 ghc-prof-options: -auto-all -caf-all ghc-options: -threaded -rtsopts -with-rtsopts=-N -funbox-strict-fields Executable idris-codegen-c Main-is: Main.hs other-modules: Paths_idris hs-source-dirs: codegen/idris-codegen-c Build-depends: idris , base , filepath , haskeline >= 0.7 , transformers Default-Language: Haskell2010 ghc-prof-options: -auto-all -caf-all ghc-options: -threaded -rtsopts -funbox-strict-fields Executable idris-codegen-javascript Main-is: Main.hs other-modules: Paths_idris hs-source-dirs: codegen/idris-codegen-javascript Build-depends: idris , base , filepath , haskeline >= 0.7 , transformers Default-Language: Haskell2010 ghc-prof-options: -auto-all -caf-all ghc-options: -threaded -rtsopts -funbox-strict-fields Executable idris-codegen-node Main-is: Main.hs other-modules: Paths_idris hs-source-dirs: codegen/idris-codegen-node Build-depends: idris , base , filepath , haskeline >= 0.7 , transformers Default-Language: Haskell2010 ghc-prof-options: -auto-all -caf-all ghc-options: -threaded -rtsopts -funbox-strict-fields