Add documentation

1 files changed, 80 insertions, 0 deletions

diff --git a/doc/docs/frontend/syntax.md b/doc/docs/frontend/syntax.md
new file mode 100644
index 0000000..836201c
--- /dev/null
+++ b/doc/docs/frontend/syntax.md
@@ -0,0 +1,80 @@
+---
+vim: noexpandtab tabstop=2 shiftwidth=2
+---
+
+# Syntax
+
+Snug syntax is based on [S-expressions][] to simplify parsing, with some
+modifications.
+
+Importantly, parentheses are meaningful as they are used to express lists in
+the syntax. For instance, the list of arguments to a function is enclosed in
+parentheses. In such contexts it is an error to use redundant parentheses, or
+to omit parentheses in case of a single element.
+
+## Data types
+
+Algebraic data types can be defined with:
+
+```snug
+(data List (a) (
+	Nil
+	(Cons a (List a))))
+```
+
+In abstract terms, the syntax is:
+
+```snug
+(data NAME (VARIABLES) (CONSTRUCTORS))
+```
+
+where constructors are of the form `NAME` (without arguments) or
+`(NAME TYPE [TYPE..])` (with arguments).
+
+Type synonyms can be defined with:
+
+```snug
+(type String (List Char))
+```
+
+## Functions
+
+```snug
+(fun length ((xs : List a)) : Int
+	(length_acc 0 xs))
+
+(fun length_acc ((n : Int) (xs : List a)) : Int
+	(case xs (
+		(Nil -> n)
+		(Cons _ xs -> length_acc (+ n 1) xs))))
+```
+
+In abstract terms, the syntax is:
+
+```snug
+(fun NAME (ARGUMENTS) : TYPE (EXPRESSION))
+```
+
+where arguments are of the form `(NAME : TYPE)`.
+
+## Expressions
+
+Expressions are:
+
+- Basic values like `37` or `'A'`
+- Symbol identifiers, either global or local
+- Data constructor identifiers
+- Function applications
+- Case expressions
+
+Case expressions have the following syntax:
+
+```snug
+(case EXPRESSION (ALTERNATIVES))
+```
+
+and alternatives have the form `(PATTERN -> EXPRESSION)`. Patterns use the same
+form as expressions, but only basic values, symbol identifiers (for variable
+binding), and fully saturated data constructors are allowed.
+
+[S-expressions]: https://en.wikipedia.org/wiki/S-expression