readmes and package files updated

README.md

@@ -67,7 +67,16 @@ Now run
     git clone https://github.com/granule-project/granule \
     && cd granule \
     && stack setup \
-    && stack install --test
+    && stack install :gr --test
+    && stack install :grepl
+
+This will instance the main frontend `gr` and the interactive mode
+`grepl`.
+
+If you would also like to install the LLVM compiler (experimental and a
+work in progress) you can then run:
+
+    stack install :grc
 
 More details about how to install can be found on the [wiki
 page](https://github.com/granule-project/granule/wiki/Installing-Granule).

changelog

@@ -0,0 +1,64 @@
+  # 0.7.7.0
+  - Standard library changes
+    - `Cake`: back in to StdLib
+    - `Choice`: new library (provides linear tensor)
+    - `Prelude` change: generalised `pull`
+    - `Vec` addition: `pushVec`
+    - `Graph` bug fixes: `size` and `vertexcount` changed due to a bug fix in Granule;
+  - Modules can now have headers where data constructors can be hidden on export,
+	   e.g. module Cake hiding (Cake, Happy) where...
+  - Fixed some bugs in `grepl` (now reads the .granule config file instead of its own)
+  - `grepl` can now give the type of general expressions (if the checker can infer it)
+  - Various refactorings in the compilation of constraints to SMT; fixes a bug with `Graph` lib
+
+  # 0.7.6.0
+  - LLVM compiler for a simple subset now included.
+  - Various internal changes which allow effect modalities (graded possibility) to be richer.
+  - Type-level sets support improved with some syntax changes, e.g., <{Read, Write}>.
+  - Nat-graded monads now provided.
+  - Some renaming, R and W replaced with Stdin and Stdio so as to avoid conflicts with HandleType.
+  - More flexibility when combining different grading types.
+  - Type holes.
+  - `grin` renamed to `grepl`.
+  - Various tweaks to the standard library and various bug fixes.
+
+  # 0.7.2.0
+  - Ability to include additional predicates in type signatures
+  - More pervasive unicode support
+  - Support fewer type annotations
+  - Literate mode for LaTeX/Granule files
+  - Integers can be linearly consumed in patterns
+  - Some bug fixes
+
+  # 0.7.1.0
+  - Various improvements to error reporting
+  - New features for allowing interacting between coeffects due to nested unboxing
+  - Bug fixes on linearity in nested cases expressions
+  - FileIO modality renamed to IO
+  - Some internal reworking of security levels to match the theory
+
+  # 0.7.0.0
+  - Functions can now be written as a set of equations, and this is the best way to get dependent pattern matching
+  - Various key bug fixes
+  - Existentials
+
+  # 0.6.0.5
+  - IOMode is now a primitive type rather than being used primitively but being defined in a library
+
+  # 0.6.0.4
+
+  - Improved type support in `grin`
+  - Refactoring to how ASTs are internally represented
+  - Some fixes regarding consumption effects in pattern matches.
+
+  # 0.6.0.1
+
+  Simplified internals of kinds and coeffect types
+
+  # 0.6.0.0
+
+  Granule REPL added, called 'grin'
+
+  # 0.5.5.7
+
+  Session type duality and fork, forkRep, send, recv, close primitives.

compiler/package.yaml

@@ -1,5 +1,5 @@
 name: granule-compiler
-version: '0.7.0.0'
+version: '0.7.7.0'
 synopsis: The Granule compiler
 author: Dominic Orchard, Vilem-Benjamin Liepelt, Harley Eades III, Preston Keel
 copyright: 2018 authors

repl/README.md

@@ -25,7 +25,7 @@ A REPL for the Granule language
 
 To install `grepl`, run
 ```
-$ stack install
+$ stack install :grepl
 ```
 
 To launch, run
@@ -37,16 +37,16 @@ $ grepl
 
 The following commands are available for use in the REPL
 ```
-:help                (:h)  
-:quit                (:q)  
-:type <term>         (:t)  
+:help                (:h)
+:quit                (:q)
+:type <term>         (:t)
 :type_scheme <type>  (:ts)
-:show <term>         (:s)  
-:parse <expression>  (:p)  
-:lexer <string>      (:x)  
-:debug <filepath>    (:d)  
-:dump                ()   
-:load <filepath>     (:l)  
+:show <term>         (:s)
+:parse <expression>  (:p)
+:lexer <string>      (:x)
+:debug <filepath>    (:d)
+:dump                ()
+:load <filepath>     (:l)
 :module <filepath>   (:m)
 ```
 
@@ -64,17 +64,19 @@ Leave the REPL
 Load a file into the REPL.  This will erase content in state and replace with loaded file.
 ```
 Granule> :l Vec.gr
-S:\Documents\Research\granule\StdLib\Vec.gr, interpreted
+Vec.gr, interpreted
 ```
 #### :type <term\> (:t)
 <a id="type"></a>
-Display the type of a term in the REPL state
+Display the type of an expression in the REPL state
 ```
 Granule> :l Vec.gr
-S:\Documents\Research\granule\StdLib\Vec.gr, interpreted
+Vec.gr, interpreted
 
 Granule> :t head
-head : forall a : Type, n : Nat. ((Vec n + 1 a) |1|) → a
+head :
+  forall {a : Type, n : ↑Nat} .
+   (Vec (n + 1) a) [0..1] -> a
 ```
 
 #### :show <term\> (:s)
@@ -142,55 +144,20 @@ Granule> :dump
 <a id="module"></a>
 Adds a file to the REPL by appending to the current REPL state
 ```
-Granule> :m Files.gr
-S:\Documents\Research\granule\examples\Files.gr, interpreted
+Granule> :m Prelude.gr
+Prelude.gr, interpreted
 ```
 #### :reload (:r)
-Reload the last file loaded into the Repl
+Reload the last file loaded into the Repl (included all the additionally loaded modules)
 ```
 Granule> :l example.gr
-S:\Documents\Research\granule\tests\regression\good\example.gr, interpreted
+example.gr, interpreted
 Granule> :r
-S:\Documents\Research\granule\tests\regression\good\example.gr, interpreted
+example.gr, interpreted
 ```
 ## Configuration File
 <a id="configuration-file"></a>
 
-The congiuration file contains various variables used for set up of the REPL
-#### Config file creation
-<a id="config-file-creation"></a>
-The configuration file needs to be created by the user.  It needs to be named
-`.grepl`.  This file needs to be placed in the home directory
-###### Windows
-```
-C:\Users\<username>
-```
-###### Linux
-```
-/home/<username> or directory of users $HOME environmental variable
-```
-###### Mac OS X
-```
-/Users/<username>
-```
-#### Config File Format
-<a id="config-file-format"></a>
-The config file is set up so the config variable is on the far left (needs to be lowercase)
-followed by an equals and then the value(s).  For multiple value a newline and white space
-is needed.  
-```
-<config var 1> = someValue
-<config var 2> = aValue1
-                 aValue2
-                 aValue3
-```
-#### Config File Use
-<a id="config-file-use"></a>
-Currently the config file uses a `path` variable to make loading files into the REPL easier.
-If the path variable is set up you can use just a file name instead of the full path to load the files.  To set up add the `path = <directory paths>` to the config file.  
-NOTE: The REPL will search subdirectories when looking for a matching file.
-```
-path = S:\Documents\Research\granule\StdLib
-       S:\Documents\Research\granule\examples
-       S:\Documents\Research\granule\tests\regression\good
-```
+The configuration file for `grepl` is the same as that as
+`gr`. See README.md in the top-level directory for how to setup
+the `.granule` file for the global configuration.

stack.yaml

@@ -1,6 +1,6 @@
 resolver: lts-13.21
 packages:
-#- compiler/ enable to build the compiler - requires llvm 8.0
+- compiler/ #enable to build the compiler - requires llvm 8.0
 - frontend/
 - interpreter/
 - repl/
@@ -9,9 +9,8 @@ packages:
 # (e.g., acme-missiles-0.3)
 extra-deps:
 - ConfigFile-1.1.4
-# disabled, requires update - llvm-hs-pretty-0.6.1.0
-- llvm-hs-8.0.0
 - llvm-hs-pure-8.0.0
+- llvm-hs-8.0.0
 - text-replace-0.0.0.4
 - sbv-8.2