Merge branch 'master' into compiler

.dockerignore

@@ -0,0 +1,11 @@
+# Ignore everything
+*
+
+# Whitelist the following
+!LICENSE
+!README.md
+!StdLib
+!frontend
+!interpreter
+!repl
+!stack.yaml

.gitattributes

@@ -0,0 +1,2 @@
+# Use Agda syntax hightlighting for Granule
+*.gr linguist-language=Agda

.gitignore

@@ -60,3 +60,6 @@ Temporary Items
 
 # Compiler Examples
 compiler-examples/
+
+# VSCode
+.vscode

Dockerfile

@@ -0,0 +1,29 @@
+# Stack build environment
+FROM fpco/stack-build:lts-13.21 AS build
+WORKDIR /granule
+COPY . /granule/
+RUN stack install --local-bin-path /usr/bin && stack clean --full
+RUN wget https://github.com/Z3Prover/z3/releases/download/z3-4.8.4/z3-4.8.4.d6df51951f4c-x64-ubuntu-16.04.zip \
+  && unzip z3-4.8.4.d6df51951f4c-x64-ubuntu-16.04.zip \
+  && mv z3-4.8.4.d6df51951f4c-x64-ubuntu-16.04/bin/z3 /usr/bin/z3 \
+  && rm -rf z3-4.8.4.d6df51951f4c-x64-ubuntu-16.04*
+
+# Get a stripped down ubuntu 16.04 for a lean distribution image
+FROM ubuntu:xenial-20190515
+WORKDIR /granule
+COPY --from=build /usr/bin/gr /usr/bin/grin /usr/bin/z3 /usr/bin/
+COPY --from=build /granule /granule
+RUN apt-get update
+# for GHC
+RUN apt-get install -y libgmp10
+# for Z3
+RUN apt-get install -y libgomp1
+# UTF8 support
+RUN apt-get install -y locales \
+  && sed -i -e 's/# en_US.UTF-8 UTF-8/en_US.UTF-8 UTF-8/' /etc/locale.gen \
+  && dpkg-reconfigure --frontend=noninteractive locales \
+  && update-locale LANG=en_US.UTF-8
+ENV LANG en_US.UTF-8
+# add .granule config file
+RUN echo "--include-path /granule/StdLib --alternative-colors" > ~/.granule
+CMD ["bash"]

README.md

@@ -1,18 +1,24 @@
 ```
-                                     ___             
-                                    /\_ \            
-   __   _  _    __      ___   __  __\//\ \      __   
+                                     ___
+                                    /\_ \
+   __   _  _    __      ___   __  __\//\ \      __
  / _  \/\`'__\/ __ \  /' _ `\/\ \/\ \ \ \ \   /'__`\
 /\ \_\ \ \ \//\ \_\ \_/\ \/\ \ \ \_\ \ \_\ \_/\  __/
 \ \____ \ \_\\ \__/ \_\ \_\ \_\ \____/ /\____\ \____\
- \/___L\ \/_/ \/__/\/_/\/_/\/_/\/___/  \/____/\/____/
-   /\____/                                           
+ \/___/\ \/_/ \/__/\/_/\/_/\/_/\/___/  \/____/\/____/
+   /\____/
    \_/__/
 ```
 
-A functional programming language with a linear type system and fine-grained effects and coeffects via **graded modal types**.
+Granule is a functional programming language with a linear type system and
+fine-grained effects and coeffects via **graded modal types**.
 
-A brief introduction to the Granule programming language can be found in [this extended abstract](http://www.cs.ox.ac.uk/conferences/fscd2017/preproceedings_unprotected/TLLA_Orchard.pdf) presented at TLLA'17. The type system is partly based on the one in ["Combining effects and coeffects via grading" (Gaboardi et al. 2016)](https://www.cs.kent.ac.uk/people/staff/dao7/publ/combining-effects-and-coeffects-icfp16.pdf).
+An introduction to Granule can be found in our paper [Quantitative
+program reasoning with graded modal types][1]. More details of the project
+can be found on the [project website][2].
+
+[1]: https://www.cs.kent.ac.uk/people/staff/dao7/publ/granule-icfp19.pdf
+[2]: https://granule-project.github.io/
 
 ## Example
 
@@ -42,90 +48,201 @@ map [_] Nil = Nil;
 map [f] (Cons x xs) = Cons (f x) (map [f] xs)
 ```
 
-This type explains that the parameter function `f` is used exactly `n` times, where `n` is the size
-of the incoming list. Linearity ensures that the entire list is consumed exactly
-once to the produce the result.
+This type explains that the parameter function `f` is used exactly `n` times,
+where `n` is the size of the incoming list. Linearity ensures that the entire
+list is consumed exactly once to the produce the result.
 
 ## Installation
 
-Make sure you have [Z3](https://github.com/Z3Prover/z3) and [Stack](https://docs.haskellstack.org/en/stable/README/) on your system.
+Binary releases are currently available for MacOS only. If you need a newer
+[release](https://github.com/granule-project/granule/releases) than is available
+then please open an issue.
+
+To build Granule from source, make sure you have
+[Z3](https://github.com/Z3Prover/z3) and
+[Stack](https://docs.haskellstack.org/en/stable/README/) on your system.
 
 Now run
 
-    $ git clone https://github.com/granule-project/granule && cd granule && stack setup && stack install --test
+    git clone https://github.com/granule-project/granule \
+    && cd granule \
+    && stack setup \
+    && stack install --test
 
-More details about how to install can be found on the [wiki page](https://github.com/granule-project/granule/wiki/Installing-Granule).
+More details about how to install can be found on the [wiki
+page](https://github.com/granule-project/granule/wiki/Installing-Granule).
 
 ## Running the Interpreter
 
 Granule program files have file extension `.gr`. Use the `gr` command to run the interpreter:
 
     $ gr examples/NonEmpty.gr
     Checking examples/NonEmpty.gr...
-    Ok, evaluating...
-    `main` returned:
+    OK, evaluating...
     1
 
-See the `examples` directory for more sample programs, or `frontend/tests/cases`
-if you dare.
+A good starting point for learning about Granule is the tutorial given in
+[examples/intro.gr.md](https://github.com/granule-project/granule/blob/master/examples/intro.gr.md).
+
+### Setting the Path
+
+Granule has a very basic import system. When `gr` encounters a line `import
+A.B.C` anywhere in the file it will attempt to load the file located at
+`$GRANULE_PATH/A/B/C.gr`, where `$GRANULE_PATH` defaults to `StdLib`, i.e. it
+should work when you are running `gr` from within this project. For a more
+stable setup which lets you run `gr` from any directory you can set the path
+with the `--include-path` flag (see below).
+
+### Configuration
+
+Run `gr` with the `--help` flag for an overview of flags. Flags can be set
+
+  1. in `~/.granule` (the same way as on the command line)
+  2. on the command line
+  3. at the top of the file (prepended with `-- gr `)
+
+and have precedence in that order, e.g. flags set on the command line will
+override flags in the config.
+
+Example `.granule` file:
+
+~~~sh
+$ cat ~/.granule
+--include-path /Users/alice/granule/StdLib
+--solver-timeout 2000
+~~~
+
+### Command line completion
+
+See [here](https://github.com/pcapriotti/optparse-applicative#bash-zsh-and-fish-completions)
+for how to install completion scripts for your shell, although we recommend
+dynamically loading the completions in your shell's startup script to account
+for changes in `gr`'s interface; e.g. for `fish` on MacOS:
+
+~~~ fish
+echo "#granule
+gr --fish-completion-script (which gr) | source" >> ~/.config/fish/config.fish
+~~~
+
+### Accessibility
+
+We aim to make Granule as inclusive as possible. If you experience any
+accessibility hurdles, please open an issue.
+
+#### Alternative Colours
 
-### Literate Granule Files
+The `--alternative-colors`/`--alternative-colours` flag will cause success
+messages to be printed in blue instead of green, which may help with colour
+blindness.
+
+The `--no-color`/`--no-colour` flag will turn off colours altogether.
+
+### Multi-Byte Unicode
+
+The following symbols are interchangeable. You can destructively rewrite all
+occurrences in your source file by passing
+`--ascii-to-unicode`/`--unicode-to-ascii`. `--keep-backup` will save a backup of
+the most recent copy of the input file with `.bak` appended.
+
+| ASCII | Unicode |
+|:---:|:---:|
+| `forall` | `∀` |
+| `Inf` | `∞` |
+| `->` | `→` |
+| `=>` | `⇒` |
+| `<-` | `←` |
+| `/\` | `∧` |
+| `\/` | `∨` |
+| `<=` | `≤` |
+| `>=` | `≥` |
+| `==` | `≡` |
+| `\` | `λ` |
+
+Usages of the operator `∘` get parsed as an application of `compose`.
+
+### Literate Granule
+
+Granule has some basic support for literate programs with Markdown and TeX.
+By default code in `granule` code environments will be run. This can be
+overridden with the flag `--literate-env-name`.
+
+#### Markdown
 
 The interpreter also takes markdown files with the extension `.md`, in which
 case all fenced code blocks labelled with `granule` will get parsed as the input
 source code. All other lines are ignored, but counted as whitespace to retain
 line numbers for error messages.
 
-    # Example literate granule (markdown) file
+~~~~ markdown
+# Example literate granule (markdown) file
 
-    Code blocks can be fenced with twiddles...
+Code blocks can be fenced with twiddles...
 
-    ~~~ granule
-    a : Int
-    a = 1
-    ~~~
+~~~ granule
+a : Int
+a = 1
+~~~
 
-    ... or backticks.
+... or backticks.
 
-    ```granule
-    b : Int
-    b = 2
-    ```
+```granule
+b : Int
+b = 2
+```
 
-    The following code blocks will get ignored.
+The following code blocks will get ignored.
 
-    ~~~
-    c : Int
-    c = 3
-    ~~~
+~~~
+int c = 3;
+~~~
 
-    ```not granule
-    d : Int
-    d = 4
-    ```
+```haskell
+d :: Int
+d = 4
+```
+~~~~
 
+#### TeX
 
+You can run Granule on the TeX file below with `gr --literate-env-name verbatim`.
+You can use XeLaTeX to properly display multi-byte Unicode characters.
 
-### Options
+~~~ tex
+\documentclass{article}
 
-`gr` takes several options, run `gr --help` for more information.
+\title{Literate Granule (\TeX{}) Example}
+\begin{document}
+\author{Grampy Granule}
+\maketitle
 
-You can set default options in `$HOME/.granule`, e.g.:
+Writing things here.
 
-```
-$ cat ~/.granule
-Options
-  { debugging           = Nothing
-  , noColors            = Just True
-  , noEval              = Nothing
-  , suppressInfos       = Nothing
-  , suppressErrors      = Nothing
-  , timestamp           = Nothing
-  , solverTimeoutMillis = Just 2000
-  , includePath         = Just "Users/alice/granule/StdLib"
-  , ascii2unicode       = Just True
-  , keepBackupAscii     = Just False
-  }
-```
+\begin{verbatim}
+import Prelude
+
+foo : String
+foo = "running code here"
+\end{verbatim}
+\end{document}
+~~~
+
+
+## Caveats
+
+Granule is a research project to help us gain intuitions about using linearity
+and graded modalities in programming. It is licensed under a permissive licence,
+so you can use it for whatever, but please don't write your next spaceship
+controller in Granule just yet. The interface is not stable (and nor is the
+code). You have been warned...
 
-All contributions are welcome!
+~~~
+            ( All contributions are welcome! )
+      __//   /
+    /.__.\
+    \ \/ /
+ '__/    \
+  \-      )
+   \_____/
+_____|_|______________________________________
+     " "
+~~~