Documentation: update language reference (#1829)

* Closes #1627

docs/org/SUMMARY.org

@@ -28,6 +28,8 @@
   - [[./reference/language/functions.md][Functions]]
   - [[./reference/language/datatypes.md][Data types]]
   - [[./reference/language/modules.md][Modules]]
+  - [[./reference/language/let.md][Local definitions]]
+  - [[./reference/language/control.md][Control structures]]
   - [[./reference/language/comments.md][Comments]]
   - [[./reference/language/axioms.md][Axioms]]
 - [[./reference/examples.md][Example programs]]

docs/org/reference/language/README.org

@@ -1,5 +1,7 @@
   - [[./functions.md][Functions]]
   - [[./datatypes.md][Data types]]
   - [[./modules.md][Modules]]
+  - [[./let.md][Local definitions]]
+  - [[./control.md][Control structures]]
   - [[./comments.md][Comments]]
   - [[./axioms.md][Axioms]]

docs/org/reference/language/axioms.org

@@ -12,5 +12,4 @@ module Example;
 end;
 #+end_src
 
-Terms introduced by the =axiom= keyword lack any computational content. However,
-it is possible to attach computational content to an axiom by giving compilation rules, see [[./compileblocks.md][the =compile= keyword]].
+Terms introduced by the =axiom= keyword lack any computational content. Programs containing axioms not marked as builtins cannot be compiled to most targets.

docs/org/reference/language/control.org

@@ -0,0 +1,27 @@
+* Control structures
+
+** Case
+
+A case expression has the following syntax:
+
+#+begin_example
+case value
+| pat1 := branch1
+..
+| patN := branchN
+#+end_example
+
+For example, one can evaluate the following expression in the REPL:
+#+begin_example
+Stdlib.Prelude> case 2 | zero := 0 | suc x := x | _ := 19
+1
+#+end_example
+
+** Lazy builtins
+
+The standard library provides several builtin functions which are treated specially and evaluated lazily. These builtins must always be fully applied.
+
+- =if condition branch1 branch2=. First evaluates =condition=, if true evaluates and returns =branch1=, otherwise evaluates and returns =branch2=.
+- =a || b=. Lazy disjunction. First evaluates =a=, if true returns true, otherwise evaluates and returns =b=.
+- =a && b=. Lazy conjunction. First evaluates =a=, if false returns false, otherwise evaluates and returns =b=.
+- =a >> b=. Sequences two IO actions. Lazy in the second argument.

docs/org/reference/language/functions.org

@@ -14,7 +14,7 @@ multiplyByTwo n := 2 * n;
 #+end_example
 
 A function may have more than one function clause. When a function is called,
-the first clause that matches the argument is used.
+the first clause that matches the arguments is used.
 
 The following function has two clauses.
 
@@ -37,13 +37,52 @@ Function declarations can depend on each other recursively. In the following exa
 #+begin_example
 open import Stdlib.Prelude;
 
-odd : Nat → Bool;
-
-even : Nat → Bool;
+odd : Nat -> Bool;
+even : Nat -> Bool;
 
 odd zero := false;
 odd (suc n) := even n;
 
 even zero := true;
 even (suc n) := odd n;
 #+end_example
+
+** Anonymous functions
+
+Anonymous functions, or /lambdas/, are introduced with the syntax:
+
+#+begin_example
+\{| pat1 .. patN_1 := clause1
+  | ..
+  | pat1 .. patN_M := clauseM}
+#+end_example
+
+The first pipe =|= is optional. Instead of =\= one can also use =λ=.
+
+An anonymous function just lists all clauses of a function without
+naming it. Any function declaration can be converted to use anonymous
+functions:
+
+#+begin_example
+open import Stdlib.Prelude;
+
+odd : Nat -> Bool;
+even : Nat -> Bool;
+
+odd := \{
+  | zero := false
+  | (suc n) := even n
+};
+
+even := \{
+  | zero := true
+  | (suc n) := odd n
+};
+#+end_example
+
+** Short definitions
+
+A function definition can be written in one line, with the body immediately following the signature:
+#+begin_example
+multiplyByTwo : Nat -> Nat := \{n := 2 * n};
+#+end_example

docs/org/reference/language/let.org

@@ -0,0 +1,16 @@
+* Local definitions
+
+Local definitions are introduced with the =let= construct.
+
+#+begin_example
+sum : NList -> Nat;
+sum lst :=
+  let
+    go : Nat -> NList -> Nat;
+    go acc nnil := acc;
+    go acc (ncons x xs) := go (acc + x) xs;
+  in
+  go 0 lst;
+#+end_example
+
+The declaractions in a =let= have the same syntax as declarations inside a module, but they are visible only in the expression following the =in= keyword.

docs/org/reference/language/modules.org

@@ -139,8 +139,8 @@ The module =C= below does not typecheck. Both symbols, originally defined in
 module =A=, are not visible in module =C= after importing =B=. The symbols =A=
 and =a= are not exported by the module =B=. To export symbols from an imported
 module, one can use the =public= keyword at the end of the corresponding =open=
-statement. For example, in module =B=, after marking the import of =A= as
-=public=, the module =C= typechecks.
+statement. For example, the module =C= typechecks after marking the import of =A= as
+=public= in module =B=.
 
 #+begin_example
 -- A.juvix