Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with HTTPS or Subversion.

Download ZIP
Newer
Older
100644 83 lines (70 sloc) 3.64 kb
5528447 Not really mini any more...
Edwin Brady authored
1 Name: idris
a94fd81 Remove Eq constraint from Num
Edwin Brady authored
2 Version: 0.9.3
dc0c198 First lot of source files and paper
Edwin Brady authored
3 License: BSD3
4 License-file: LICENSE
5 Author: Edwin Brady
6 Maintainer: Edwin Brady <eb@cs.st-andrews.ac.uk>
7 Homepage: http://www.idris-lang.org/
8
b47740d cabal changes
Edwin Brady authored
9 Stability: Beta
dc0c198 First lot of source files and paper
Edwin Brady authored
10 Category: Compilers/Interpreters, Dependent Types
8baaa42 Error message tinker
Edwin Brady authored
11 Synopsis: Functional Programming Language with Dependent Types
38da9bc Update .cabal; require up to date epic
Edwin Brady authored
12 Description: Idris is a general purpose language with full dependent types.
9538419 Update description
Edwin Brady authored
13 It is compiled, with eager evaluation.
27fc1f2 Update .cabal and README
Edwin Brady authored
14 Dependent types allow types to be predicated on values,
15 meaning that some aspects of a program's behaviour can be
16 specified precisely in the type. The language is closely
38da9bc Update .cabal; require up to date epic
Edwin Brady authored
17 related to Epigram and Agda. There is a tutorial at <http://www.idris-lang.org/documentation>.
9538419 Update description
Edwin Brady authored
18 Features include:
19 .
20 * Full dependent types with dependent pattern matching
21 .
22 * where clauses, with rule, simple case expressions,
23 pattern matching let and lambda bindings
24 .
25 * Type classes, monad comprehensions
26 .
27 * do notation, idiom brackets, syntactic conveniences for lists,
28 tuples, dependent pairs
29 .
30 * Indentation significant syntax, extensible syntax
31 .
32 * Tactic based theorem proving (influenced by Coq)
33 .
34 * Cumulative universes
35 .
36 * Simple foreign function interface (to C)
37 .
38 * Hugs style interactive environment
dc0c198 First lot of source files and paper
Edwin Brady authored
39
40 Cabal-Version: >= 1.6
ec7c1b8 Get cabal to check library after install
Edwin Brady authored
41 Build-type: Custom
dc0c198 First lot of source files and paper
Edwin Brady authored
42
ffc7b69 First baby steps towards a new RTS (and towards removing epic dependency...
Edwin Brady authored
43 Data-files: rts/libidris_rts.a rts/closure.h
2a50169 Added lib/network directory, and network.cgi module
Edwin Brady authored
44 Extra-source-files: lib/Makefile lib/*.idr lib/prelude/*.idr lib/network/*.idr
e7906ba Added support/ directory so that library can use C support files
Edwin Brady authored
45 lib/control/monad/*.idr lib/language/*.idr
46 tutorial/examples/*.idr
ffc7b69 First baby steps towards a new RTS (and towards removing epic dependency...
Edwin Brady authored
47 rts/*.c rts/*.h rts/Makefile
20bf4d7 Added lib/ and prelude
Edwin Brady authored
48
b47740d cabal changes
Edwin Brady authored
49 source-repository head
50 type: git
51 location: git://github.com/edwinb/Idris-dev.git
52
53
5528447 Not really mini any more...
Edwin Brady authored
54 Executable idris
dc0c198 First lot of source files and paper
Edwin Brady authored
55 Main-is: Main.hs
56 hs-source-dirs: src
ff5f762 Rename Core to TT
Edwin Brady authored
57 Other-modules: Core.TT, Core.Evaluate, Core.Typecheck,
0ae24f1 Shift core TT into a separate directory (for ease of reuse)
Edwin Brady authored
58 Core.ProofShell, Core.ProofState, Core.CoreParser,
554c395 Made a start on the high level language
Edwin Brady authored
59 Core.ShellParser, Core.Unify, Core.Elaborate,
3b5e50c Added universe constraint checker and --typeintype command line option
Edwin Brady authored
60 Core.CaseTree, Core.Constraints,
554c395 Made a start on the high level language
Edwin Brady authored
61
06a81c9 Elaborating types and data declarations
Edwin Brady authored
62 Idris.AbsSyntax, Idris.Parser, Idris.REPL,
59c1eb1 Pretty printing of TT terms as PTerms
Edwin Brady authored
63 Idris.REPLParser, Idris.ElabDecls, Idris.Error,
ca6a5e1 import statement
Edwin Brady authored
64 Idris.Delaborate, Idris.Primitives, Idris.Imports,
60c4ef9 Added 'impossible' keyword
Edwin Brady authored
65 Idris.Compiler, Idris.Prover, Idris.ElabTerm,
dea8d48 Added support for literate programming with bird tracks (use .lidr exten...
Edwin Brady authored
66 Idris.Coverage, Idris.IBC, Idris.Unlit,
dc3f0f9 added dsl blocks
Edwin Brady authored
67 Idris.DataOpts, Idris.Transforms, Idris.DSL,
ca6a5e1 import statement
Edwin Brady authored
68
067f4fa Util.Pretty missing
Edwin Brady authored
69 Util.Pretty,
70
fa0ecde Started C generation
Edwin Brady authored
71 RTS.Bytecode, RTS.SC, RTS.PreC, RTS.CodegenC,
38a9365 More towards the new compiler
Edwin Brady authored
72
5528447 Not really mini any more...
Edwin Brady authored
73 Paths_idris
dc0c198 First lot of source files and paper
Edwin Brady authored
74
49e426a @Mathnerd314 Switch from readline to haskeline
Mathnerd314 authored
75 Build-depends: base>=4 && <5, parsec, mtl, Cabal, haskeline,
20861ec Enough Epic to compile 'hello world' (but not much else yet...)
Edwin Brady authored
76 containers, process, transformers, filepath, directory,
ffc7b69 First baby steps towards a new RTS (and towards removing epic dependency...
Edwin Brady authored
77 binary, bytestring, epic>=0.9.3.1, pretty
dc0c198 First lot of source files and paper
Edwin Brady authored
78
79 Extensions: MultiParamTypeClasses, FunctionalDependencies,
8f77986 Added some serialisation
Edwin Brady authored
80 FlexibleInstances, TemplateHaskell
59d07f7 Quicker resolution of overloaded names
Edwin Brady authored
81 ghc-prof-options: -auto-all -caf-all
3501adb Changed way of building pattern match terms
Edwin Brady authored
82 ghc-options: -rtsopts
Something went wrong with that request. Please try again.