Tags: joneshf/Idris-dev
Tags
Version 0.9.18 change log:
* GHC 7.10 compatibility
* Add support for bundled toolchains.
* Strings are now UTF8 encoded in the default back end
* Idris source files are now assumed to be in UTF8, regardless of locale
settings.
* Some reorganisation of primitives:
+ Buffer and BitVector primitives have been removed (they were not
tested sufficiently, and lack a maintainer)
+ Float has been renamed 'Double' (Float is defined in the Prelude for
compatibility)
+ Externally defined primitives and operations now supported with
'%extern' directive, allowing back ends to define their own special
purpose primitives
+ Ptr and ManagedPtr have been removed and replaced with external primitives
* Add %hint function annotation, which allows functions to be used as
hints in proof search for 'auto' arguments. Only functions which return
an instance of a data or record type are allowed as hints.
* Syntax rules no longer perform variable capture. Users of effects will
need to explicitly name results in dependent effect signatures instead
of using the default name "result".
* Pattern-matching lambdas are allowed to be impossible. For example,
Dec (2 = 3) can now be constructed with No $ \(Refl) impossible, instead of
requiring a separate lemma.
* Case alternatives are allowed to be impossible:
case Vect.Nil {a=Nat} of { (x::xs) impossible ; [] => True }
* The default Semigroup and Monoid instances for Maybe are now prioritised
choice, keeping the first success as Alternative does. The version that
collects successes is now a named instance.
* :exec REPL command now takes an optional expression to compile and run/show
* The return types of `Vect.findIndex`, `Vect.elemIndex` and
`Vect.elemIndexBy` were changed from `Maybe Nat` to `Maybe (Fin n)`
* A new :browse command shows the contents of a namespace
* `{n} is syntax for a quotation of the reflected representation of the name
"n". If "n" is lexically bound, then the resulting quotation will be for it,
whereas if it is not, then it will succeed with a quotation of the unique
global name that matches.
* New syntax for records that closely matches our other record-like structures:
type classes. See the updated tutorial for details.
* Records can be coinductive. Define coinductive records with the "corecord"
keyword.
* Type class constructors can be assigned user-accessible names. This is done
using the same syntax as record constructors.
* if ... then ... else ... is now built-in syntax instead of being defined in
a library. It is shown in REPL output and error messages, rather than its
desugaring.
* The desugaring of if ... then ... else ... has been renamed to ifThenElse from
boolElim. This is for consistency with GHC Haskell and scala-virtualized, and
to reflect that if-notation makes sense with non-Bool datatypes.
* Agda-style semantic highlighting is supported over the IDE protocol.
* Experimental support for elaborator reflection. Users can now script the
elaborator, for use in code generation and proof automation. This feature is
still under rapid development and is subject to change without notice. See
Language.Reflection.Elab and the %runElab constructs
New in 0.9.17:
--------------
* The --ideslave command line option has been replaced with a --ide-mode
command line option with the same semantics.
* A new tactic "claim N TY" that introduces a new hole named N with type TY
* A new tactic "unfocus" that moves the current hole to the bottom of the
hole stack
* Quasiquotation supports the generation of Language.Reflection.Raw terms
in addition to Language.Reflection.TT. Types are used for disambiguation,
defaulting to TT at the REPL.
* Language.Reflection.Quotable now takes an extra type parameter which
determines the type to be quoted to. Instances are provided to quote
common types to both TT and Raw.
* Library operators have been renamed for consistency with Haskell. In
particular, Applicative.(<$>) is now Applicative.(<*>) and (<$>) is
now an alias for Functor.map. Correspondingly, ($>) and (<$) have
been renamed to (<*) and (*>). The cascading effects of this rename
are that Algebra.(<*>) has been renamed to Algebra.(<.>) and
Matrix.(<.>) is now Matrix.(<:>).
* Binding forms in DSL notation are now given an extra argument: a
reflected representation of the name that the user chose.
Specifically, the rewritten lambda, pi, and let binders will now get
an extra argument of type TTName. This allows more understandable
dynamic errors in DSL code and more readable code generation results.
* DSL notation can now be applied with $
* Added FFI_Export type which allows Idris functions to be exportoed and
called from foreign code
* Instances can now have documentation strings.
* Type providers can have documentation strings.
* Unification errors now (where possible) contain information about provenance
of a type
* New REPL command ":core TM" that shows the elaborated form of TM along with
its elaborated type using the syntax of TT. IDE mode has a corresponding
command :elaborate-term for serialized terms.
* Effectful and IO function names for sending data to STDOUT have been
aligned, semantically.
+ `print` is now for putting showable things to STDOUT.
+ `printLn` is for putting showable things to STDOUT with a new line
+ `putCharLn` for putting a single character to STDOUT, with a new line.
* Classes can now be annotated with 'determining parameters' to say which
must be available before resolving instances. Only determining parameters
are checked when checking for overlapping instances.
* New package 'contrib' containing things that are less mature or less used
than the contents of 'base'. 'contrib' is not available by default, so you
may need to add '-p contrib' to your .ipkg file or Idris command line.
* Arguments to class instances are now checked for injectivity.
Unification assumes this, so we need to check when instances are defined.
Version 0.9.16 * Inductive-inductive definitions are now supported (i.e. simultaneously defined types where one is indexed by the other.) * Implicits and type class constraints can now appear in scopes other than the top level. * Importing a module no longer means it is automatically reexported. A new "public" modifier has been added to import statements, which will reexport the names exported from that module. * Implemented @-patterns. A pattern of the form x@p on the left hand side matches p, with x in scope on the right hand side with value p. * A new tactic sourceLocation that fills the current hole with the current source code span, if this information is available. If not, it raises an error. * Better Unicode support for the JavaScript/Node codegen * ':search' and ':apropos' commands can now be given optional package lists to search. * Vect, Fin and So moved out of prelude into base, in modules Data.Vect, Data.Fin and Data.So respectively. * Several long-standing issues resolved, particularly with pattern matching and coverage checking. * Modules can now have API documentation strings.
Version 0.9.15 released * Two new tactics: skip and fail. Skip does nothing, and fail takes a string as an argument and produces it as an error. * Corresponding reflected tactics Skip and Fail. Reflected Fail takes a list of ErrorReportParts as an argument, like error handlers produce, allowing access to the pretty-printer. * Stop showing irrelevant and inaccessible internal names in the interactive prover. * The proof arguments in the List library functions are now implicit and solved automatically. * More efficient representation of proof state, leading to faster elaboration of large expressions. * EXPERIMENTAL Implementation of uniqueness types * Unary negation now desugars to "negate", which is a method of the Neg type class. This allows instances of Num that can't be negative, like Nat, and it makes correct IEEE Float operations easier to encode. Additionally, unary negation is now available to DSL authors. * The Java and LLVM backends have been factored out for separate maintenance. Now, the compiler distribution only ships with the C and JavaScript backends. * New REPL command :printdef displays the internal definition of a name * New REPL command :pprint pretty-prints a definition or term with LaTeX or HTML highlighting * Naming of data and type constructors is made consistent across the standard library (see idris-lang#1516) * Terms in `code blocks` inside of documentation strings are now parsed and type checked. If this succeeds, they are rendered in full color in documentation lookups, and with semantic highlighting for IDEs. * Fenced code blocks in docs defined with the "example" attribute are rendered as code examples. * Fenced code blocks declared to be Idris code that fail to parse or type check now provide error messages to IDE clients. * EXPERIMENTAL support for partial evaluation (Scrapping your Inefficient Engine style)
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". * Updated 'effects' 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
PreviousNext