Idris-dev/CHANGELOG

New in 0.9.14:
--------------
* Tactic for case analysis in proofs
* Induction and case tactic now work on expressions
* Support for running tests for a package with the tests section of .ipkg files and the
  --testpkg command-line option
* Clearly distinguish between type providers and postulate providers at the use site
* Allow dependent function syntax to be overridden in dsl blocks, similarly to
  functions and let. The keyword for this is "pi".
* Experimental 'neweffects' library, with simplified API
* All new JavaScript backend (avoids callstack overflows)
* Add support for %lib directive for NodeJS
* Quasiquotes and quasiquote patterns allow easier work with reflected terms.
  `(EXPR) quasiquotes EXPR, causing the elaborator to be used to produce a reflected
  version of it. Subterms prefixed with ~ are unquoted - on the RHS, they are reflected
  terms to splice in, while on the LHS they are patterns.
  A quasiquote expression can be given a goal type for the elaborator, which helps with
  disambiguation. For instance, `(() : ()) quotes the unit constructor, while `(() : Type)
  quotes the unit type.
  Both goal types and quasiquote are typechecked in the global environment.
* Better inference of unbound implicits

New in 0.9.13:
--------------
* IDE support for retrieving structured information about metavariables
* Experimental Bits support for JavaScript
* IdrisDoc: a Haddock- and JavaDoc-like HTML documentation generator
* Command line option -e (or --eval) to evaluate expressions without loading the
  REPL. This is useful for writing more portable tests.
* Many more of the basic functions and datatypes are documented.
* Primitive types such as Int and String are documented
* Removed javascript lib in favor of idris-hackers/iQuery
* Specify codegen for :compile REPL command (e.g. :compile javascript program.js)
* Remove :info REPL command, subsume and enhance its functionality in the :doc command
* New (first class) nested record update/access syntax:
  record { a->b->c = val } x -- sets field accessed by c (b (a x)) to val
  record { a->b->c } x -- accesses field, equivalent to c (b (a x))
* The banner at startup can be suppressed by adding :set nobanner to the initialisation script.
* :apropos now accepts space-delimited lists of query items, and searches for the conjunction
  of its inputs. It also accepts binder syntax as search strings - for instance, -> finds
  functions.
* Totality errors are now treated as warnings until code generation time, when they become
  errors again. This allows users to use the interactive editing features to fix totality
  issues, but no programs that violate the stated assumptions will actually run.
* Added :makelemma command, which adds a new top level definition to solve
  a metavariable.
* Extend :addclause to add instance bodies as well as definitions
* Reverse parameters to BoundedList -- now matches Vect, and is easier to instantiate classes.
* Move foldl into Foldable so it can be overridden.
* Experimental :search REPL command for finding functions by type

Internal changes

* New implementation of erasure

New in 0.9.12:
--------------

* Proof search now works for metavariables in types, giving some interactive
  type inference.
* New 'Lazy' type, replacing laziness annotations.
* JavaScript and Node codegen now understand the %include directive.
* Concept of 'null' is now understood in the JavaScript and Node codegen.
* Lots of performance patches for generated JavaScript.
* New commands :eval (:e) and :type (:t) in the prover, which either normalise
  or show the type of expressions.
* Allow type providers to return postulates in addition to terms.
* Syntax for dealing with match failure in <- and pattern matching let.
* New syntax for inline documentation. Documentation starts with |||, and
  arguments are documented by preceding their name with @. Example:
  ||| Add two natural numbers
  ||| @ n the first number (examined by the function)
  ||| @ m the second number (not examined)
  plus (n, m : Nat) -> Nat
* Allow the auto-solve behaviour in the prover to be disabled, for easier 
  debugging of proof automation. Use ":set autosolve" and ":unset autosolve".
* Updated 'effects' library
* New :apropos command at REPL to search documentation, names, and types
* Unification errors are now slightly more informative
* Support mixed induction/coinduction with 'Inf' type
* Add 'covering' function option, which checks whether a function and all
  descendants cover all possible inputs

New in 0.9.11:
--------------

* Agda-style equational reasoning (in Syntax.PreorderReasoning)
* 'case' construct now abstracts over the scrutinee in its type
* Added label type 'name (equivalent to the empty type).
  This is intended for field/effect disambiguation. "name" can be any
  valid identifier. Two labels are definitionally equal if they have the
  same name.
* General improvements in error messages, especially %error_reverse
  annotation, which allows a hint as to how to display a term in error
  messages
* --ideslave mode now transmits semantic information about many of the
  strings that it emits, which can be used by clients to implement
  semantic highlighting like that of the REPL. This has been implemented
  in the Emacs mode and the IRC bot, which can serve as examples.
* New expression form: with NAME EXPR privileges the namespace NAME
  when disambiguating overloaded names. For example, it is possible to
  write "with Vect [1,2,3]" at the REPL instead of "the (Vect _ _) [1,2,3]",
  because the Vect constructors are defined in a namespace called Vect.
* assert_smaller internal function, which marks an expression as smaller than
  a pattern for use in totality checking. 
  e.g. "assert_smaller (x :: xs) (f xs)" asserts that "f xs" will always be
  structurally smaller than "(x :: xs)"
* assert_total internal function, which marks a subexpression as assumed to
  be total, e.g "assert_total (tail (x :: xs))".
* Terminal width is automatically detected if Idris is compiled with curses
  support. If curses is not available, automatic mode assumes 80 columns.
* Changed argument order for Prelude.Either.either.
* Experimental 'neweffects' library, intended to replace 'effects' in the
  next release.

Internal changes

* Faster elaboration
* Smaller .ibc files
* Pretty-printer now used for all term output


New in 0.9.10:
--------------

* Type classes now implemented as dependent records, meaning that method
  types may now depend on earlier methods.
* More flexible class instance resolution, so that function types and lambda
  expressions can be made instances of a type class.
* Add !expr notation for implicit binding of intermediate results in 
  monadic/do/etc expressions.
* Extend Effects package to cope with possibly failing operations, using
  "if_valid", "if_error", etc.
* At the REPL, "it" now refers to the previous expression.
* Semantic colouring at the REPL. Turn this off with --nocolour.
* Some prettifying of error messages.
* The contents of ~/.idris/repl/init are run at REPL start-up.
* The REPL stores a command history in ~/.idris/repl/history.
* The [a..b], [a,b..c], [a..], and [a,b..] syntax now pass the totality
  checker and can thus be used in types. The [x..] syntax now returns an
  actually infinite stream.
* Add '%reflection' option for functions, for compile-time operations on
  syntax.
* Add expression form 'quoteGoal x by p in e' which applies p to the expected
  expression type and binds the result to x in the scope e.
* Performance improvements in Strings library.
* Library reorganisation, separated into prelude/ and base/.

Internal changes

* New module/dependency tree checking.
* New parser implementation with more precise errors.
* Improved type class resolution.
* Compiling Nat via GMP integers.
* Performance improvements in elaboration.
* Improvements in termination checking.
* Various REPL commands to support interactive editing, and a client/server
  mode to allow external invocation of REPL commands.

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 the result type of a rewrite to be specified
* 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.
* Experimental LLVM backend
* Added Data.HVect module
* Fix fromInteger to take an Integer, rather than an Int
* Integer literals for Fin
* Renamed O to Z, and fO to fZ
* Swapped Vect arguments, now Vect : Nat -> Type -> Type
* Added DecEq instances
* Add 'equiv' tactic, which rewrites a goal to an equivalent (convertible) goal

Internal changes

* Add annotation for unification traces
* Add 'mrefine' tactic for refining by matching against a type
* Type class resolution fixes
* Much faster coverage checking

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 
(ecb10@st-andrews.ac.uk).