Add licence and changelog and update REAMDE

CHANGELOG.md

@@ -0,0 +1,55 @@
+Changes since Idris 2 v0.1.0
+----------------------------
+
+The implementation is now self-hosted. To initialise the build, either use
+the [bootstrapping version of Idris2](https://github.com/edwinb/Idris2-boot)
+or build fromt the generated Scheme, using `make bootstrap`.
+
+Compiler updates:
+
+* Data types with a single constructor, with a single unerased arguments,
+  are translated to just that argument, to save repeated packing and unpacking.
+  (c.f. `newtype` in Haskell)
+  + A data type can opt out of this behaviour by specifying `noNewtype` in its
+    options list. `noNewtype` allows code generators to apply special handling
+    to the generated constructor/deconstructor, for a newtype-like data type,
+    that would otherwise be optimised away.
+* 0-multiplicity constructor arguments are now properly erased, not just
+  given a placeholder null value.
+
+Language extensions:
+
+* %transform directive, for declaring transformation rules on runtime
+  expressions. Transformation rules are automatically added for top level
+  implementations of interfaces.
+* A %spec flag on functions which allows arguments to be marked for partial
+  evaluation, following the rules from "Scrapping Your Inefficient Engine"
+  (ICFP 2010, Brady & Hammond)
+
+Library additions:
+
+* Additional file management operations in `base`
+* New modules in `contrib` for time (`System.Clock`); JSON (`Language.JSON.*`);
+  random numbers (`System.Random`)
+
+Other improvements:
+
+* Various performance improvements in the typechecker:
+  + Noting which metavariables are blocking unification constraints, so that
+    they only get retried if those metavariables make progress.
+  + Evaluating `fromInteger` at compile time.
+  + In the run-time, reuse the old heap after garbage collection if it
+    hasn't been resized, to avoid unnecessary system calls.
+
+* Extend Idris2's literate mode to support reading Markdown and OrgMode files.
+  For more details see: https://idris2.readthedocs.io/en/latest/reference/literate.html
+
+* Fields of records can be accessed (and updated) using the dot syntax,
+  such as `r.field1.field2` or `record { field1.field2 = 42 }`.
+  For details, see https://idris2.readthedocs.io/en/latest/reference/records.html
+
+Changes since Idris 1
+---------------------
+
+Everything :). For full details, see:
+https://idris2.readthedocs.io/en/latest/updates/updates.html

LICENSE

@@ -0,0 +1,32 @@
+Copyright (c) 2020 Edwin Brady
+    School of Computer Science, University of St Andrews
+All rights reserved.
+
+This code is derived from software written by Edwin Brady
+(ecb10@st-andrews.ac.uk).
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions
+are met:
+1. Redistributions of source code must retain the above copyright
+   notice, this list of conditions and the following disclaimer.
+2. Redistributions in binary form must reproduce the above copyright
+   notice, this list of conditions and the following disclaimer in the
+   documentation and/or other materials provided with the distribution.
+3. None of the names of the copyright holders may be used to endorse
+   or promote products derived from this software without specific
+   prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS ``AS IS'' AND ANY
+EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
+IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR
+PURPOSE ARE DISCLAIMED.  IN NO EVENT SHALL THE COPYRIGHT HOLDERS BE
+LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
+CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
+SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR
+BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY,
+WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE
+OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN
+IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+
+*** End of disclaimer. ***

README.md

@@ -1,12 +1,94 @@
-Self-hosted Idris 2
--------------------
+Idris 2
+=======
 
-It finally happened!
+[![Build Status](https://travis-ci.org/edwinb/Idris2-SH.svg?branch=master)](https://travis-ci.org/edwinb/Idris2)
 
-See `INSTALL.md` for installation instructions.
+[Idris 2](https://idris-lang.org/) is a purely functional programming language
+with first class types.
 
-There are no guarantees: This repository might move or be renamed or deleted or
-anything at no notice.  It will eventually turn into the real Idris 2
-repository, one way or another.
+For full installation instructions, see [INSTALL.md](INSTALL.md).  Briefly, if
+you have Chez Scheme installed, with the executable name `chez`, type:
 
-Good luck :)
+* `make bootstrap SCHEME=chez`
+* `make install`
+
+You may need to change `chez` to be the local name of your Chez Scheme. This
+is often one of `scheme`, `chezscheme` or `chezscheme9.5` (depending on the
+version)
+
+Idris 2 is mostly backwards compatible with Idris 1, with some minor
+exceptions. The most notable user visible differences, which might cause Idris
+1 programs to fail to type check, are:
+
++ Unbound implicit arguments are always erased, so it is a type error to
+  attempt to pattern match on one.
++ Simplified resolution of ambiguous names, which might mean you need to
+  explicitly disambiguate more often. As a general rule, Idris 2 will be able
+  to disambiguate between names which have different concrete return types
+  (such as data constructors), or which have different concrete argument
+  types (such as record projections). It may struggle to resolve ambiguities
+  if one name requires an interface to be resolved.
++ Minor differences in the meaning of export modifiers `private`, `export`,
+  and `public export`, which now refer to visibility of names from other
+  *namespaces* rather than visibility from other *files*.
++ Module names must match the filename in which they are defined (unless
+  the module's name is "Main").
++ Anything which uses a `%language` pragma in Idris 1 is likely to be different.
+  Notably, elaborator reflection will exist, but most likely in a slightly
+  different form because the internal details of the elaborator are different.
++ The `Prelude` is much smaller (and easier to replace with an alternative).
++ `let x = val in e` no longer computes with `x` in `e`, instead being
+  essentially equivalent to `(\x => e) val`. This is to make the
+  behaviour of `let` consistent in the presence of `case` and `with` (where
+  it is hard to push the computation inside the `case`/`with` efficiently).
+  Instead, you can define functions locally with `let`, which do have
+  computational force, as follows:
+
+      let x : ?
+          x = val in
+          e
+
+Watch this space for more details and the rationale for the changes, as I
+get around to writing it...
+
+Summary of new features:
+
++ A core language based on "Quantitative Type Theory" which allows explicit
+  annotation of erased types, and linear types.
++ `let` bindings are now more expressive, and can be used to define pattern
+  matching functions locally.
++ Names which are in scope in a type are also always in scope in the body of
+  the corresponding definition.
++ Better inference. Holes are global to a source file, rather than local to
+  a definition, meaning that some holes can be left in function types to be
+  inferred by the type checker. This also gives better inference for the types
+  of `case` expressions, and means fewer annotations are needed in interface
+  declarations.
++ Better type checker implementation which minimises the need for compile
+  time evaluation.
++ New Chez Scheme based back end which both compiles and runs faster than the
+  default Idris 1 back end. (Also, optionally, Racket and Gambit can be used
+  as targets).
++ Everything works faster :).
+
+A significant change in the implementation is that there is an intermediate
+language `TTImp`, which is essentially a desugared Idris, and is cleanly
+separated from the high level language which means it is potentially usable
+as a core language for other high level syntaxes.
+
+Things still missing
+====================
+
++ Disambiguation via 'with'
++ Cumulativity (so we currently have Type : Type! Bear that in mind when you
+  think you've proved something :))
++ 'rewrite' doesn't yet work on dependent types
++ Parts of the ide-mode, particularly syntax highlighting
++ Documentation strings and HTML documentation generation
++ ':search' and ':apropos' at the REPL
++ Metaprogramming (reflection, partial evaluation)
+
+Talks
+=====
+
+[![Idris 2 - Type-driven Development of Idris (Curry On - London 2019)](https://img.youtube.com/vi/DRq2NgeFcO0/0.jpg)](https://www.youtube.com/watch?v=DRq2NgeFcO0 "Idris 2 - Type-driven Development of Idris (Curry On - London 2019)")