forked from idris-lang/Idris-dev
-
Notifications
You must be signed in to change notification settings - Fork 1
/
CHANGELOG
225 lines (175 loc) · 7.05 KB
/
CHANGELOG
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
New in 0.9.9:
-------------
* Apply functions by return type, rather than with arguments:
"t <== f" means "apply f with arguments such that it returns a value
of type t"
* Allow names to be attached to provisional definitions
lhs ?= {name} rhs -- generates a lemma called 'name' which makes the
types of the lhs and rhs match. {name} is optional - a unique name is
generated if it is absent.
* Added Data.HVect module
* Fix fromInteger to take an Integer, rather than an Int
* Integer literals for Fin
Internal changes
* Add annotation for unification traces
* Add 'mrefine' tactic for refining by matching against a type
* Type class resolution fixes
New in 0.9.8:
-------------
User visible changes:
* Added "rewrite ... in ..." construct
* Allow type class constraints in 'using' clauses
* Renamed EFF to EFFECT in Effect package
* Experimental Java backend
* Tab completion in REPL
* Dynamic loading of C libraries in the interpreter
* Testing IO actions at the REPL with :x command
* Improve rendering of :t
* Fixed some INTERNAL ERROR messages
Internal changes:
* Fix non-linear pattern checking
* Improved name disambiguation
* More flexible unification and elaboration of lambdas
* Various unification and totality checking bug fixes
New in 0.9.7:
-------------
User visible changes:
* 'implicit' keyword, for implicit type conversion
* Added Effects package
* Primitives for 8,16,32 and 64 bit integers
Internal changes:
* Change unification so that it keeps track of failed constraints in case
later information helps to resolve them
* Distinguishing parameters and indices in data types
* Faster termination/coverage checking
* Split 'javascript' target into 'javascript' and 'node'
New in 0.9.6:
-------------
User visible changes:
* The type of types is now 'Type' rather than 'Set'
* Forward declarations of data allowed
- supporting induction recursion and mutually recursive data
* Type inference of definitions in 'where' clauses
- Provided that the type can be completely determined from the first
application of the function (in the top level definition)
* 'mutual' blocks added
- effect is to elaborate all types of declarations in the block before
elaborating their definitions
- allows inductive-recursive definitions
* Expression inspected by 'with' clause now abstracted from the goal
- i.e. "magic" with
* Implicit arguments will be added automatically only if their initial
letter is lower case, or they are in a using declaration
* Added documentation comments (Haddock style) and ':doc' REPL command
* Pattern matching on strings, big integers and characters
* Added System.Concurrency modules
* Added 'postulate' declarations
* Allow type annotations on 'let' tactic
* EXPERIMENTAL JavaScript generation, with '--target javascript' option
Internal changes:
* Separate inlining methods at compile-time and run-time
* Fixed nested parameters blocks
* Improve efficiency of elaborator by:
- only normalising when necessary
- reducing backtracking with resolving ambiguities
* Better compilation of case trees
New in 0.9.5:
-------------
User visible changes:
* Added codata
- as data declarations, but constructor arguments are evaluated lazily
- functions which return a codata type do not reduce at compile time
* Added 'parameters' blocks
* Allow local data definitions in where blocks
* Added '%default' directive to declare total-by-default or partial-by-default
for functions, and a corresponding "partial" reserved words to mark functions
as allowed to be partial. Also "--total" and "--partial" added as command
line options.
* Command line option "--warnpartial" for flagging all undeclared
partial functions, without error.
* New termination checker supporting mutually recursive definitions.
* Added ':load' command to REPL, for loading a new file
* Added ':module' command to REPL, for adding modules
* Renamed library modules (now have initial capital)
Internal changes:
* Several improvements and fixes to unification
* Added collapsing optimisation and more aggressive erasure
New in 0.9.4:
-------------
User visible changes:
* Simple packaging system
* Added --dumpc flag for displaying generated code
Internal changes:
* Improve overloading resolution (especially where this is a type error)
* Various important bug fixes with evaluation and compilation
* More aggressive compile-time evaluation
New in 0.9.3:
-------------
User visible changes:
* Added binding forms to syntax rules
* Named class instances
* Added ':set' command, with options 'errorcontext' for displaying local
variables in scope when a unification error occurs, and 'showimplicits'
for displaying elaborated terms in full
* Added '--errorcontext' command line switch
* Added ':proofs' and ':rmproofs' commands
* Various minor REPL improvements and fixes
Internal changes:
* Completely new run time system (not based on Epic or relying on Boehm GC)
* Normalise before forcing to catch more forceable arguments
* Types no longer exported in normal form
* Try to resolve overloading by inspecting types, rather than full type
checking
New in 0.9.2:
-------------
User visible changes:
* backtick notation added: x `foo` y ==> foo x y
* case expressions allowed in type signatures
* Library extensions in prelude.vect and prelude.algebra
* malloc/trace_malloc added to builtins.idr
Internal changes:
* Some type class resolution fixes
* Several minor bug fixes
* Performance improvements in resolving overloading and type classes
New in 0.9.1:
-------------
User visible changes:
* DSL notation, for overloading lambda and let bindings
* Dependent records, with projection and update
* Totality checking and 'total' keyword
* Auto implicits and default argument values {auto n : T}, {default val n : T}
* Overlapping type class instances disallowed
* Many extensions to prelude.nat and prelude.list libraries (mostly thanks to
Dominic Mulligan)
* New libraries: control.monad.identity, control.monad.state
* Small improvements in error reporting
Internal changes:
* Faster compilation (only compiling names which are used)
* Better type class resolution
* Lots of minor bug fixes
0.1.x to 0.9.0:
Complete rewrite. User visible changes:
* New proof/tactics syntax
* New syntax for pairs/dependent pairs
* Indentation-significant syntax
* Added type classes
* Added where clauses
* Added case expressions, pattern matching let and lambda
* Added monad comprehensions
* Added cumulativity and universe checking
* Ad-hoc name overloading
- Resolved by type or explicit namespace
* Modules (Haskell-style)
* public, abstract and private access to functions and types
* Separate type-checking
* Improved interactive environment
* Replaced 'do using' with Monad class
* Extended syntax macros
Internal changes:
* Everything :-)
* All definitions (functions, classes and instances) are elaborated to top
level, fully explicit, data declarations and pattern matching definitions,
which are verified by a minimal type checker.
This is the first release of a complete reimplementation. There will be bugs.
If you find any, please do not hesitate to contact Edwin Brady