Version push – 4.3.0 (#255 )

* Version push – 4.3.0 . * Fixed ordering of diffs in CHANGELOG
Prepare 4.3.0 (#254 )
2020-04-02 15:10:53 +02:00 · 2020-04-02 13:59:22 +02:00 · 2020-04-02 12:29:14 +02:00 · 2020-04-01 13:11:02 +02:00 · 2020-03-31 13:14:13 +02:00 · 2020-03-30 14:52:16 +02:00
46 changed files with 4565 additions and 478 deletions
@@ -9,7 +9,54 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 ### Changed
 ### Removed

-## [4.1.0-rc1] - 2019-11-25
+## [4.3.0]
+### Added
+- Added documentation (moved from `protocol`)
+- `Frac.aes` – library for rational numbers
+- Added some more meaningful error messages
+- Exported several parsing functionalities
+ - With option `keep_included` it is possible to see which files were included during the parse
+ - There is a function `run_parser` that be used to evaluate any parsing rule
+ - Exported parsers: `body`, `type` and `decl`
+### Changed
+- Performance improvements in the standard library
+- Fixed ACI encoder to handle `-` unary operator
+- Fixed including by absolute path
+- Fixed variant type printing in the ACI error messages
+- Fixed pretty printing of combined function clauses
+### Removed
+- `let` definitions are no longer supported in the toplevel of the contract
+- type declarations are no longer supported
+
+## [4.2.0] - 2020-01-15
+### Added
+- Allow separate entrypoint/function type signature and definition, and pattern
+  matching in left-hand sides:
+  ```
+    function
+      length : list('a) => int
+      length([])      = 0
+      length(x :: xs) = 1 + length(xs)
+  ```
+- Allow pattern matching in list comprehension generators (filtering out match
+  failures):
+  ```
+    function somes(xs : list(option('a))) : list('a) =
+      [ x | Some(x) <- xs ]
+  ```
+- Allow pattern matching in let-bindings (aborting on match failures):
+  ```
+    function test(m : map(int, int)) =
+        let Some(x) = Map.lookup(m, 0)
+        x
+  ```
+### Changed
+- FATE code generator improvements.
+- Bug fix: Handle qualified constructors in patterns.
+- Bug fix: Allow switching also on negative numbers.
+### Removed
+
+## [4.1.0] - 2019-11-26
 ### Added
 - Support encoding and decoding bit fields in call arguments and results.
 ### Changed
@@ -25,7 +72,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
  (de-)construct byte arrays.
 - `[a..b]` language construct, returning the list of numbers between
  `a` and `b` (inclusive). Returns the empty list if `a` > `b`.
- [Standard libraries] (https://github.com/aeternity/protocol/blob/master/contracts/sophia_stdlib.md)
+- [Standard libraries](https://github.com/aeternity/aesophia/blob/master/docs/sophia_stdlib.md)
 - Checks that `init` is not called from other functions.
 - FATE backend - the compiler is able to produce VM code for both `AEVM` and `FATE`. Many
  of the APIs now take `{backend, aevm | fate}` to decide wich backend to produce artifacts
@@ -164,12 +211,11 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 - Simplify calldata creation - instead of passing a compiled contract, simply
  pass a (stubbed) contract string.

-[Unreleased]: https://github.com/aeternity/aesophia/compare/v4.0.0...HEAD
-[4.0.0]: https://github.com/aeternity/aesophia/compare/v4.0.0...v3.2.0
-[4.0.0-rc5]: https://github.com/aeternity/aesophia/compare/v4.0.0-rc4...v4.0.0-rc5
-[4.0.0-rc4]: https://github.com/aeternity/aesophia/compare/v4.0.0-rc3...v4.0.0-rc4
-[4.0.0-rc3]: https://github.com/aeternity/aesophia/compare/v4.0.0-rc1...v4.0.0-rc3
-[4.0.0-rc1]: https://github.com/aeternity/aesophia/compare/v3.2.0...v4.0.0-rc1
+[Unreleased]: https://github.com/aeternity/aesophia/compare/v4.3.0...HEAD
+[4.3.0]: https://github.com/aeternity/aesophia/compare/v4.2.0...v4.3.0
+[4.2.0]: https://github.com/aeternity/aesophia/compare/v4.1.0...v4.2.0
+[4.1.0]: https://github.com/aeternity/aesophia/compare/v4.0.0...v4.1.0
+[4.0.0]: https://github.com/aeternity/aesophia/compare/v3.2.0...v4.0.0
 [3.2.0]: https://github.com/aeternity/aesophia/compare/v3.1.0...v3.2.0
 [3.1.0]: https://github.com/aeternity/aesophia/compare/v3.0.0...v3.1.0
 [3.0.0]: https://github.com/aeternity/aesophia/compare/v2.1.0...v3.0.0
@@ -2,13 +2,19 @@

 This is the __sophia__ compiler for the æternity system which compiles contracts written in __sophia__ code to the æternity VM code.

-For more information about æternity smart contracts and the sophia language see [Smart Contracts](https://github.com/aeternity/protocol/blob/master/contracts/contracts.md) and the [Sophia Language](https://github.com/aeternity/protocol/blob/master/contracts/sophia.md).
-
 It is an OTP application written in Erlang and is by default included in
 [the æternity node](https://github.com/aeternity/epoch). However, it can
 also be included in other systems to compile contracts coded in sophia which
 can then be loaded into the æternity system.

+
+## Documentation
+
+* [Smart Contracts on aeternity Blockchain](https://github.com/aeternity/protocol/blob/master/contracts/contracts.md).
+* [Sophia Documentation](docs/sophia.md).
+* [Sophia Standard Library](docs/sophia_stdlib.md).
+
+
 ## Versioning

 `aesophia` has a version that is only loosely connected to the version of the
@@ -17,6 +23,7 @@ minor/patch version. The `aesophia` compiler version MUST be bumped whenever
 there is a change in how byte code is generated, but it MAY also be bumped upon
 API changes etc.

+
 ## Interface Modules

 The basic modules for interfacing the compiler:
@@ -0,0 +1,183 @@
+namespace Frac =
+
+  private function gcd(a : int, b : int) =
+    if (b == 0) a else gcd(b, a mod b)
+
+  private function abs_int(a : int) = if (a < 0) -a else a
+
+  datatype frac = Pos(int, int) | Zero | Neg(int, int)
+
+/** Checks if the internal representation is correct.
+  * Numerator and denominator must be positive.
+  * Exposed for debug purposes
+  */
+  function is_sane(f : frac) : bool = switch(f)
+    Pos(n, d) => n > 0 && d > 0
+    Zero => true
+    Neg(n, d) => n > 0 && d > 0
+
+  function num(f : frac) : int = switch(f)
+    Pos(n, _) => n
+    Neg(n, _) => -n
+    Zero      => 0
+
+  function den(f : frac) : int = switch(f)
+    Pos(_, d) => d
+    Neg(_, d) => d
+    Zero      => 1
+
+  function to_pair(f : frac) : int * int = switch(f)
+    Pos(n, d) => (n, d)
+    Neg(n, d) => (-n, d)
+    Zero      => (0, 1)
+
+  function sign(f : frac) : int = switch(f)
+    Pos(_, _) => 1
+    Neg(_, _) => -1
+    Zero      => 0
+
+  function to_str(f : frac) : string = switch(f)
+    Pos(n, d) => String.concat(Int.to_str(n), if (d == 1) "" else String.concat("/", Int.to_str(d)))
+    Neg(n, d) => String.concat("-", to_str(Pos(n, d)))
+    Zero      => "0"
+
+/** Reduce fraction to normal form
+ */
+  function simplify(f : frac) : frac =
+    switch(f)
+      Neg(n, d) =>
+        let cd = gcd(n, d)
+        Neg(n / cd, d / cd)
+      Zero  => Zero
+      Pos(n, d)  =>
+        let cd = gcd(n, d)
+        Pos(n / cd, d / cd)
+
+/** Integer to rational division
+ */
+  function make_frac(n : int, d : int) : frac =
+    if (d == 0) abort("Zero denominator")
+    elif (n == 0) Zero
+    elif ((n < 0) == (d < 0)) simplify(Pos(abs_int(n), abs_int(d)))
+    else simplify(Neg(abs_int(n), abs_int(d)))
+
+  function one() : frac = Pos(1, 1)
+  function zero() : frac = Zero
+
+  function eq(a : frac, b : frac) : bool =
+    let (na, da) = to_pair(a)
+    let (nb, db) = to_pair(b)
+    (na == nb && da == db) || na * db == nb * da // they are more likely to be normalized
+
+  function neq(a : frac, b : frac) : bool =
+    let (na, da) = to_pair(a)
+    let (nb, db) = to_pair(b)
+    (na != nb || da != db) && na * db != nb * da
+
+  function geq(a : frac, b : frac) : bool = num(a) * den(b) >= num(b) * den(a)
+
+  function leq(a : frac, b : frac) : bool = num(a) * den(b) =< num(b) * den(a)
+
+  function gt(a : frac, b : frac) : bool = num(a) * den(b) > num(b) * den(a)
+
+  function lt(a : frac, b : frac) : bool = num(a) * den(b) < num(b) * den(a)
+
+  function min(a : frac, b : frac) : frac = if (leq(a, b)) a else b 
+
+  function max(a : frac, b : frac) : frac = if (geq(a, b)) a else b 
+
+  function abs(f : frac) : frac = switch(f)
+    Pos(n, d) => Pos(n, d)
+    Zero      => Zero
+    Neg(n, d) => Pos(n, d)
+
+  function from_int(n : int) : frac =
+    if   (n > 0) Pos(n, 1)
+    elif (n < 0) Neg(-n, 1)
+    else Zero
+
+  function floor(f : frac) : int = switch(f)
+    Pos(n, d) => n / d
+    Zero      => 0
+    Neg(n, d) => -(n + d - 1) / d
+
+  function ceil(f : frac) : int = switch(f)
+    Pos(n, d) => (n + d - 1) / d
+    Zero      => 0
+    Neg(n, d) => -n / d
+  
+  function round_to_zero(f : frac) : int = switch(f)
+    Pos(n, d) => n / d
+    Zero      => 0
+    Neg(n, d) => -n / d
+
+  function round_from_zero(f : frac) : int = switch(f)
+    Pos(n, d) => (n + d - 1) / d
+    Zero      => 0
+    Neg(n, d) => -(n + d - 1) / d
+
+/** Round towards nearest integer. If two integers are in the same
+ * distance, choose the even one.
+ */
+  function round(f : frac) : int =
+    let fl = floor(f)
+    let cl = ceil(f)
+    let dif_fl = abs(sub(f, from_int(fl)))
+    let dif_cl = abs(sub(f, from_int(cl)))
+    if   (gt(dif_fl, dif_cl)) cl
+    elif (gt(dif_cl, dif_fl)) fl
+    elif (fl mod 2 == 0) fl
+    else cl
+
+  function add(a : frac, b : frac) : frac =
+    let (na, da) = to_pair(a)
+    let (nb, db) = to_pair(b)
+    if   (da == db) make_frac(na + nb, da)
+    else make_frac(na * db + nb * da, da * db)
+
+  function neg(a : frac) : frac = switch(a)
+    Neg(n, d) => Pos(n, d)
+    Zero      => Zero
+    Pos(n, d) => Neg(n, d)
+
+  function sub(a : frac, b : frac) : frac = add(a, neg(b))
+
+  function inv(a : frac) : frac = switch(a)
+    Neg(n, d) => Neg(d, n)
+    Zero      => abort("Inversion of zero")
+    Pos(n, d) => Pos(d, n)
+
+  function mul(a : frac, b : frac) : frac = make_frac(num(a) * num(b), den(a) * den(b))
+
+  function div(a : frac, b : frac) : frac = switch(b)
+    Neg(n, d) => mul(a, Neg(d, n))
+    Zero      => abort("Division by zero")
+    Pos(n, d) => mul(a, Pos(d, n))
+
+/** `b` to the power of `e`
+ */
+  function int_exp(b : frac, e : int) : frac =
+    if (sign(b) == 0 && e == 0) abort("Zero to the zero exponentation")
+    elif (e < 0) inv(int_exp_(b, -e))
+    else int_exp_(b, e)
+  private function int_exp_(b : frac, e : int) =
+      if (e == 0) from_int(1)
+      elif (e == 1) b
+      else
+        let half = int_exp_(b, e / 2)
+        if (e mod 2 == 1) mul(mul(half, half), b)
+        else mul(half, half)
+
+/** Reduces the fraction's in-memory size by dividing its components by two until the
+ * the error is bigger than `loss` value
+ */
+  function optimize(f : frac, loss : frac) : frac =
+    require(geq(loss, Zero), "negative loss optimize")
+    let s = sign(f)
+    mul(from_int(s), run_optimize(abs(f), abs(f), loss))
+  private function run_optimize(orig : frac, f : frac, loss : frac) : frac =
+    let (n, d) = to_pair(f)
+    let t = make_frac((n+1)/2, (d+1)/2)
+    if(gt(abs(sub(t, orig)), loss)) f
+    elif (eq(t, f)) f
+    else run_optimize(orig, t, loss)
@@ -12,35 +12,66 @@ namespace Func =

  function rapply(x : 'a, f : 'a => 'b) : 'b = f(x)

-  /* The Z combinator - replacement for local and anonymous recursion.
-   */
+/** The Z combinator - replacement for local and anonymous recursion.
+  */
  function recur(f : ('arg => 'res, 'arg) => 'res) : 'arg => 'res =
    (x) => f(recur(f), x)

+/** n-times composition with itself
+ */
  function iter(n : int, f : 'a => 'a) : 'a => 'a = iter_(n, f, (x) => x)
  private function iter_(n : int, f : 'a => 'a, acc : 'a => 'a) : 'a => 'a =
    if(n == 0) acc
    elif(n == 1) comp(f, acc)
    else iter_(n / 2, comp(f, f), if(n mod 2 == 0) acc else comp(f, acc))

-  function curry2(f : ('a, 'b) => 'c) : 'a => ('b => 'c) =
+/** Turns an ugly, bad and disgusting arity-n function into
+ * a beautiful and sweet function taking the first argument
+ * and returning a function watiting for the remaining ones
+ * in the same manner
+ */
+  function curry2(f : ('a, 'b) => 'x) : 'a => ('b => 'x) =
    (x) => (y) => f(x, y)
-  function curry3(f : ('a, 'b, 'c) => 'd) : 'a => ('b => ('c => 'd)) =
+  function curry3(f : ('a, 'b, 'c) => 'x) : 'a => ('b => ('c => 'x)) =
    (x) => (y) => (z) => f(x, y, z)
+  function curry4(f : ('a, 'b, 'c, 'd) => 'x) : 'a => ('b => ('c => ('d => 'x))) =
+    (x) => (y) => (z) => (w) => f(x, y, z, w)
+  function curry5(f : ('a, 'b, 'c, 'd, 'e) => 'x) : 'a => ('b => ('c => ('d => ('e => 'x)))) =
+    (x) => (y) => (z) => (w) => (q) => f(x, y, z, w, q)

-  function uncurry2(f : 'a => ('b => 'c)) : ('a, 'b) => 'c =
+/** Opposite of curry. Gross
+ */
+  function uncurry2(f : 'a => ('b => 'x)) : ('a, 'b) => 'x =
    (x, y) => f(x)(y)
-  function uncurry3(f : 'a => ('b => ('c => 'd))) : ('a, 'b, 'c) => 'd =
+  function uncurry3(f : 'a => ('b => ('c => 'x))) : ('a, 'b, 'c) => 'x =
    (x, y, z) => f(x)(y)(z)
+  function uncurry4(f : 'a => ('b => ('c => ('d => 'x)))) : ('a, 'b, 'c, 'd) => 'x =
+    (x, y, z, w) => f(x)(y)(z)(w)
+  function uncurry5(f : 'a => ('b => ('c => ('d => ('e => 'x))))) : ('a, 'b, 'c, 'd, 'e) => 'x =
+    (x, y, z, w, q) => f(x)(y)(z)(w)(q)

-  function tuplify2(f : ('a, 'b) => 'c) : (('a * 'b)) => 'c =
+/** Turns an arity-n function into a function taking n-tuple
+ */
+  function tuplify2(f : ('a, 'b) => 'x) : (('a * 'b)) => 'x =
    (t) => switch(t)
      (x, y) => f(x, y)
-  function tuplify3(f : ('a, 'b, 'c) => 'd) : 'a * 'b * 'c => 'd =
+  function tuplify3(f : ('a, 'b, 'c) => 'x) : 'a * 'b * 'c => 'x =
    (t) => switch(t)
      (x, y, z) => f(x, y, z)
+  function tuplify4(f : ('a, 'b, 'c, 'd) => 'x) : 'a * 'b * 'c * 'd => 'x =
+    (t) => switch(t)
+      (x, y, z, w) => f(x, y, z, w)
+  function tuplify5(f : ('a, 'b, 'c, 'd, 'e) => 'x) : 'a * 'b * 'c * 'd * 'e => 'x =
+    (t) => switch(t)
+      (x, y, z, w, q) => f(x, y, z, w, q)

-  function untuplify2(f : 'a * 'b => 'c) : ('a, 'b) => 'c =
+/** Opposite of tuplify
+ */
+  function untuplify2(f : 'a * 'b => 'x) : ('a, 'b) => 'x =
    (x, y) => f((x, y))
-  function untuplify3(f : 'a * 'b * 'c => 'd) : ('a, 'b, 'c) => 'd =
+  function untuplify3(f : 'a * 'b * 'c => 'x) : ('a, 'b, 'c) => 'x =
    (x, y, z) => f((x, y, z))
+  function untuplify4(f : 'a * 'b * 'c * 'd => 'x) : ('a, 'b, 'c, 'd) => 'x =
+    (x, y, z, w) => f((x, y, z, w))
+  function untuplify5(f : 'a * 'b * 'c * 'd * 'e => 'x) : ('a, 'b, 'c, 'd, 'e) => 'x =
+    (x, y, z, w, q) => f((x, y, z, w, q))
@@ -19,10 +19,15 @@ namespace List =
    [x] => Some(x)
    _::t => last(t)

+/** Finds first element of `l` fulfilling predicate `p` as `Some` or `None`
+ * if no such element exists.
+ */
  function find(p : 'a => bool, l : list('a)) : option('a) = switch(l)
    []   => None
    h::t => if(p(h)) Some(h) else find(p, t)

+/** Returns list of all indices of elements from `l` that fulfill the predicate `p`.
+ */
  function find_indices(p : 'a => bool, l : list('a)) : list(int) = find_indices_(p, l, 0, [])
  private function find_indices_( p : 'a => bool
                                , l : list('a)
@@ -50,14 +55,22 @@ namespace List =
    _::t => length_(t, acc + 1)


+/** Creates an ascending sequence of all integer numbers
+ * between `a` and `b` (including `a` and `b`)
+ */
  function from_to(a : int, b : int) : list(int) = [a..b]

+/** Creates an ascending sequence of integer numbers betweeen
+ * `a` and `b` jumping by given `step`. Includes `a` and takes
+ * `b` only if `(b - a) mod step == 0`. `step` should be bigger than 0.
+ */
  function from_to_step(a : int, b : int, s : int) : list(int) = from_to_step_(a, b, s, [])
  private function from_to_step_(a, b, s, acc) =
    if (a > b) reverse(acc) else from_to_step_(a + s, b, s, a :: acc)


-  /* Unsafe. Replaces `n`th element of `l` with `e`. Crashes on over/underflow */
+/** Unsafe. Replaces `n`th element of `l` with `e`. Crashes on over/underflow
+ */
  function replace_at(n : int, e : 'a, l : list('a)) : list('a) =
    if(n<0) abort("insert_at underflow") else replace_at_(n, e, l, [])
  private function replace_at_(n : int, e : 'a, l : list('a), acc : list('a)) : list('a) =
@@ -66,7 +79,8 @@ namespace List =
     h::t => if (n == 0) reverse(e::acc) ++ t
             else replace_at_(n-1, e, t, h::acc)

-  /* Unsafe. Adds `e` to `l` to be its `n`th element. Crashes on over/underflow */
+/** Unsafe. Adds `e` to `l` to be its `n`th element. Crashes on over/underflow
+ */
  function insert_at(n : int, e : 'a, l : list('a)) : list('a) =
    if(n<0) abort("insert_at underflow") else insert_at_(n, e, l, [])
  private function insert_at_(n : int, e : 'a, l : list('a), acc : list('a)) : list('a) =
@@ -75,6 +89,9 @@ namespace List =
     []   => abort("insert_at overflow")
     h::t => insert_at_(n-1, e, t, h::acc)

+/** Assuming that cmp represents `<` comparison, inserts `x` before
+ * the first element in the list `l` which is greater than it
+ */
  function insert_by(cmp : (('a, 'a) => bool), x : 'a, l : list('a)) : list('a) =
    insert_by_(cmp, x, l, [])
  private function insert_by_(cmp : (('a, 'a) => bool), x : 'a, l : list('a), acc : list('a)) : list('a) =
@@ -109,6 +126,8 @@ namespace List =
    []   => reverse(acc)
    h::t => map_(f, t, f(h)::acc)

+/** Effectively composition of `map` and `flatten`
+ */
  function flat_map(f : 'a => list('b), l : list('a)) : list('b) =
    ListInternal.flat_map(f, l)

@@ -117,7 +136,8 @@ namespace List =
    []   => reverse(acc)
    h::t => filter_(p, t, if(p(h)) h::acc else acc)

-  /* Take `n` first elements */
+/** Take `n` first elements
+ */
  function take(n : int, l : list('a)) : list('a) =
    if(n < 0) abort("Take negative number of elements") else take_(n, l, [])
  private function take_(n : int, l : list('a), acc : list('a)) : list('a) =
@@ -126,7 +146,8 @@ namespace List =
      []   => reverse(acc)
      h::t => take_(n-1, t, h::acc)

-  /* Drop `n` first elements */
+/** Drop `n` first elements
+ */
  function drop(n : int, l : list('a)) : list('a) =
   if(n < 0) abort("Drop negative number of elements")
   elif (n == 0) l
@@ -134,18 +155,23 @@ namespace List =
      []   => []
      h::t => drop(n-1, t)

-  /* Get the longest prefix of a list in which every element matches predicate `p` */
+/** Get the longest prefix of a list in which every element
+ * matches predicate `p`
+ */
  function take_while(p : 'a => bool, l : list('a)) : list('a) = take_while_(p, l, [])
  private function take_while_(p : 'a => bool, l : list('a), acc : list('a)) : list('a) = switch(l)
    []   => reverse(acc)
    h::t => if(p(h)) take_while_(p, t, h::acc) else reverse(acc)

-  /* Drop elements from `l` until `p` holds */
+/** Drop elements from `l` until `p` holds
+ */
  function drop_while(p : 'a => bool, l : list('a)) : list('a) = switch(l)
    []   => []
    h::t => if(p(h)) drop_while(p, t) else l

-  /* Splits list into two lists of elements that respectively match and don't match predicate `p` */
+/** Splits list into two lists of elements that respectively
+ * match and don't match predicate `p`
+ */
  function partition(p : 'a => bool, l : list('a)) : (list('a) * list('a)) = partition_(p, l, [], [])
  private function partition_( p : 'a => bool
                             , l : list('a)
@@ -155,7 +181,8 @@ namespace List =
    []   => (reverse(acc_t), reverse(acc_f))
    h::t => if(p(h)) partition_(p, t, h::acc_t, acc_f) else partition_(p, t, acc_t, h::acc_f)

-
+/** Flattens list of lists into a single list
+ */
  function flatten(ll : list(list('a))) : list('a) = foldr((l1, l2) => l1 ++ l2, [], ll)

  function all(p : 'a => bool, l : list('a)) : bool = switch(l)
@@ -171,7 +198,9 @@ namespace List =
  function product(l : list(int)) : int = foldl((a, b) => a * b, 1, l)


-  /* Zips two list by applying bimapping function on respective elements. Drops longer tail. */
+/** Zips two list by applying bimapping function on respective elements.
+ * Drops longer tail.
+ */
  function zip_with(f : ('a, 'b) => 'c, l1 : list('a), l2 : list('b)) : list('c) = zip_with_(f, l1, l2, [])
  private function zip_with_( f : ('a, 'b) => 'c
                            , l1 : list('a)
@@ -181,7 +210,8 @@ namespace List =
    (h1::t1, h2::t2) => zip_with_(f, t1, t2, f(h1, h2)::acc)
    _ => reverse(acc)

-  /* Zips two lists into list of pairs. Drops longer tail. */
+/** Zips two lists into list of pairs. Drops longer tail.
+ */
  function zip(l1 : list('a), l2 : list('b)) : list('a * 'b) = zip_with((a, b) => (a, b), l1, l2)

  function unzip(l : list('a * 'b)) : list('a) * list('b) = unzip_(l, [], [])
@@ -199,7 +229,8 @@ namespace List =
    h::t => switch (partition((x) => lesser_cmp(x, h), t))
      (lesser, bigger) => sort(lesser_cmp, lesser) ++ h::sort(lesser_cmp, bigger)

-
+/** Puts `delim` between every two members of the list
+ */
  function intersperse(delim : 'a, l : list('a)) : list('a) = intersperse_(delim, l, [])
  private function intersperse_(delim : 'a, l : list('a), acc : list('a)) : list('a) = switch(l)
    []   => reverse(acc)
@@ -207,6 +238,8 @@ namespace List =
    h::t => intersperse_(delim, t, delim::h::acc)


+/** Effectively a zip with an infinite sequence of natural numbers
+ */
  function enumerate(l : list('a)) : list(int * 'a) = enumerate_(l, 0, [])
  private function enumerate_(l : list('a), n : int, acc : list(int * 'a)) : list(int * 'a) = switch(l)
    []   => reverse(acc)
@@ -10,13 +10,18 @@ namespace Option =
    None => false
    Some(_) => true

-
+/** Catamorphism on `option`. Also known as inlined pattern matching.
+ */
  function match(n : 'b, s : 'a => 'b, o : option('a)) : 'b = switch(o)
    None => n
    Some(x) => s(x)

+/** Escape option providing default if `None`
+ */
  function default(def : 'a, o : option('a)) : 'a = match(def, (x) => x, o)

+/** Assume it is `Some`
+ */
  function force(o : option('a)) : 'a = default(abort("Forced None value"), o)

  function on_elem(o : option('a), f : 'a => unit) : unit = match((), f, o)
@@ -40,10 +45,14 @@ namespace Option =
    (Some(x1), Some(x2), Some(x3)) => Some(f(x1, x2, x3))
    _ => None

+/** Like `map`, but the function is in `option`
+ */
  function app_over(f : option ('a => 'b), o : option('a)) : option('b) = switch((f, o))
    (Some(ff), Some(xx)) => Some(ff(xx))
    _ => None

+/** Monadic bind
+ */
  function flat_map(f : 'a => option('b), o : option('a)) : option('b) = switch(o)
    None => None
    Some(x) => f(x)
@@ -53,22 +62,31 @@ namespace Option =
    None => []
    Some(x) => [x]

+/** Turns list of options into a list of elements that are under `Some`s.
+ * Safe.
+ */
  function filter_options(l : list(option('a))) : list('a) = filter_options_(l, [])
  private function filter_options_(l : list (option('a)), acc : list('a)) : list('a) = switch(l)
    []         => List.reverse(acc)
    None::t    => filter_options_(t, acc)
    Some(x)::t => filter_options_(t, x::acc)

+/** Just like `filter_options` but requires all elements to be `Some` and returns
+ * None if any of them is not
+ */
  function seq_options(l : list (option('a))) : option (list('a)) = seq_options_(l, [])
  private function seq_options_(l : list (option('a)), acc : list('a)) : option(list('a)) = switch(l)
    []         => Some(List.reverse(acc))
    None::t    => None
    Some(x)::t => seq_options_(t, x::acc)

-
+/** Choose `Some` out of two if possible
+ */
  function choose(o1 : option('a), o2 : option('a)) : option('a) =
    if(is_some(o1)) o1 else o2

+/** Choose `Some` from list of options if possible
+ */
  function choose_first(l : list(option('a))) : option('a) = switch(l)
    [] => None
    None::t    => choose_first(t)
@@ -6,12 +6,18 @@ namespace Pair =
  function snd(t : ('a * 'b)) : 'b = switch(t)
    (_, y) => y

+/** Map over first
+ */
  function map1(f : 'a => 'c, t : ('a * 'b)) : ('c * 'b) = switch(t)
    (x, y) => (f(x), y)

+/** Map over second
+ */
  function map2(f : 'b => 'c, t : ('a * 'b)) : ('a * 'c) = switch(t)
    (x, y) => (x, f(y))

+/** Map over both
+ */
  function bimap(f : 'a => 'c, g : 'b => 'd, t : ('a * 'b)) : ('c * 'd) = switch(t)
    (x, y) => (f(x), g(y))

@@ -10,15 +10,23 @@ namespace Triple =
    (_, _, z) => z


+/** Map over first
+ */
  function map1(f : 'a => 'm, t : ('a * 'b * 'c)) : ('m * 'b * 'c) = switch(t)
    (x, y, z) => (f(x), y, z)

+/** Map over second
+ */
  function map2(f : 'b => 'm, t : ('a * 'b * 'c)) : ('a * 'm * 'c) = switch(t)
    (x, y, z) => (x, f(y), z)

+/** Map over third
+ */
  function map3(f : 'c => 'm, t : ('a * 'b * 'c)) : ('a * 'b * 'm) = switch(t)
    (x, y, z) => (x, y, f(z))

+/** Map over all elements
+ */
  function trimap( f : 'a => 'x
                 , g : 'b => 'y
                 , h : 'c => 'z
@@ -29,9 +37,13 @@ namespace Triple =
  function swap(t : ('a * 'b * 'c)) : ('c * 'b * 'a) = switch(t)
    (x, y, z) => (z, y, x)

+/** Right rotation
+ */
  function rotr(t : ('a * 'b * 'c)) : ('c * 'a * 'b) = switch(t)
    (x, y, z) => (z, x, y)

+/** Left rotation
+ */
  function rotl(t : ('a * 'b * 'c)) : ('b * 'c * 'a) = switch(t)
    (x, y, z) => (y, z, x)

@@ -15,7 +15,7 @@
            {base_plt_apps, [erts, kernel, stdlib, crypto, mnesia]}
           ]}.

-{relx, [{release, {aesophia, "4.1.0-rc1"},
+{relx, [{release, {aesophia, "4.3.0"},
         [aesophia, aebytecode, getopt]},

        {dev_mode, true},
@@ -129,7 +129,7 @@ encode_anon_args(Types) ->

 encode_args(Args) -> [ encode_arg(A) || A <- Args ].

-encode_arg({arg, _, Id, T}) ->
+encode_arg({typed, _, Id, T}) ->
    #{name => encode_type(Id),
      type => encode_type(T)}.

@@ -194,6 +194,8 @@ encode_expr({bytes, _, B})  ->
 encode_expr({Lit, _, L}) when Lit == oracle_pubkey; Lit == oracle_query_id;
                              Lit == contract_pubkey; Lit == account_pubkey ->
    aeser_api_encoder:encode(Lit, L);
+encode_expr({app, _, {'-', _}, [{int, _, N}]}) ->
+  encode_expr({int, [], -N});
 encode_expr({app, _, F, As}) ->
    Ef = encode_expr(F),
    Eas = encode_exprs(As),
@@ -12,7 +12,11 @@

 -module(aeso_ast_infer_types).

-export([infer/1, infer/2, unfold_types_in_type/3]).
+-export([ infer/1
+        , infer/2
+        , unfold_types_in_type/3
+        , pp_type/2
+        ]).

 -type utype() :: {fun_t, aeso_syntax:ann(), named_args_t(), [utype()], utype()}
               | {app_t, aeso_syntax:ann(), utype(), [utype()]}
@@ -621,12 +625,14 @@ infer_contract_top(Env, Kind, Defs0, _Options) ->
 %% infer_contract takes a proplist mapping global names to types, and
 %% a list of definitions.
 -spec infer_contract(env(), main_contract | contract | namespace, [aeso_syntax:decl()]) -> {env(), [aeso_syntax:decl()]}.
-infer_contract(Env0, What, Defs) ->
+infer_contract(Env0, What, Defs0) ->
+    Defs = process_blocks(Defs0),
    Env  = Env0#env{ what = What },
-    Kind = fun({type_def, _, _, _, _})  -> type;
-              ({letfun, _, _, _, _, _}) -> function;
-              ({fun_decl, _, _, _})     -> prototype;
-              (_)                       -> unexpected
+    Kind = fun({type_def, _, _, _, _})    -> type;
+              ({letfun, _, _, _, _, _})   -> function;
+              ({fun_clauses, _, _, _, _}) -> function;
+              ({fun_decl, _, _, _})       -> prototype;
+              (_)                         -> unexpected
           end,
    Get = fun(K) -> [ Def || Def <- Defs, Kind(Def) == K ] end,
    {Env1, TypeDefs} = check_typedefs(Env, Get(type)),
@@ -642,9 +648,11 @@ infer_contract(Env0, What, Defs) ->
    Env3      = bind_funs(ProtoSigs, Env2),
    Functions = Get(function),
    %% Check for duplicates in Functions (we turn it into a map below)
-    _         = bind_funs([{Fun, {tuple_t, Ann, []}} || {letfun, Ann, {id, _, Fun}, _, _, _} <- Functions],
-                          #env{}),
-    FunMap    = maps:from_list([ {Fun, Def} || Def = {letfun, _, {id, _, Fun}, _, _, _} <- Functions ]),
+    FunBind   = fun({letfun, Ann, {id, _, Fun}, _, _, _})   -> {Fun, {tuple_t, Ann, []}};
+                   ({fun_clauses, Ann, {id, _, Fun}, _, _}) -> {Fun, {tuple_t, Ann, []}} end,
+    FunName   = fun(Def) -> {Name, _} = FunBind(Def), Name end,
+    _         = bind_funs(lists:map(FunBind, Functions), #env{}),
+    FunMap    = maps:from_list([ {FunName(Def), Def} || Def <- Functions ]),
    check_reserved_entrypoints(FunMap),
    DepGraph  = maps:map(fun(_, Def) -> aeso_syntax_utils:used_ids(Def) end, FunMap),
    SCCs      = aeso_utils:scc(DepGraph),
@@ -655,6 +663,30 @@ infer_contract(Env0, What, Defs) ->
    destroy_and_report_type_errors(Env4),
    {Env4, TypeDefs ++ Decls ++ Defs1}.

+%% Restructure blocks into multi-clause fundefs (`fun_clauses`).
+-spec process_blocks([aeso_syntax:decl()]) -> [aeso_syntax:decl()].
+process_blocks(Decls) ->
+    lists:flatmap(
+      fun({block, Ann, Ds}) -> process_block(Ann, Ds);
+         (Decl)             -> [Decl] end, Decls).
+
+-spec process_block(aeso_syntax:ann(), [aeso_syntax:decl()]) -> [aeso_syntax:decl()].
+process_block(_, []) -> [];
+process_block(_, [Decl]) -> [Decl];
+process_block(Ann, [Decl | Decls]) ->
+    IsThis = fun(Name) -> fun({letfun, _, {id, _, Name1}, _, _, _}) -> Name == Name1;
+                             (_) -> false end end,
+    case Decl of
+        {fun_decl, Ann1, Id = {id, _, Name}, Type} ->
+            {Clauses, Rest} = lists:splitwith(IsThis(Name), Decls),
+            [{fun_clauses, Ann1, Id, Type, Clauses} |
+             process_block(Ann, Rest)];
+        {letfun, Ann1, Id = {id, _, Name}, _, _, _} ->
+            {Clauses, Rest} = lists:splitwith(IsThis(Name), [Decl | Decls]),
+            [{fun_clauses, Ann1, Id, {id, [{origin, system} | Ann1], "_"}, Clauses} |
+             process_block(Ann, Rest)]
+    end.
+
 -spec check_typedefs(env(), [aeso_syntax:decl()]) -> {env(), [aeso_syntax:decl()]}.
 check_typedefs(Env = #env{ namespace = Ns }, Defs) ->
    create_type_errors(),
@@ -787,9 +819,9 @@ check_type(Env, T) ->
 check_type(Env, T = {tvar, _, _}, Arity) ->
    [ type_error({higher_kinded_typevar, T}) || Arity /= 0 ],
    check_tvar(Env, T);
-check_type(_Env, X = {id, _, "_"}, Arity) ->
+check_type(_Env, X = {id, Ann, "_"}, Arity) ->
    ensure_base_type(X, Arity),
-    X;
+    fresh_uvar(Ann);
 check_type(Env, X = {Tag, _, _}, Arity) when Tag == con; Tag == qcon; Tag == id; Tag == qid ->
    case lookup_type(Env, X) of
        {Q, {_, Def}} ->
@@ -960,8 +992,9 @@ typesig_to_fun_t({type_sig, Ann, _Constr, Named, Args, Res}) ->

 infer_letrec(Env, Defs) ->
    create_constraints(),
-    Funs = [{Name, fresh_uvar(A)}
-                 || {letfun, _, {id, A, Name}, _, _, _} <- Defs],
+    Funs = lists:map(fun({letfun, _, {id, Ann, Name}, _, _, _})   -> {Name, fresh_uvar(Ann)};
+                        ({fun_clauses, _, {id, Ann, Name}, _, _}) -> {Name, fresh_uvar(Ann)}
+                     end, Defs),
    ExtendEnv = bind_funs(Funs, Env),
    Inferred =
        [ begin
@@ -980,26 +1013,51 @@ infer_letrec(Env, Defs) ->
    [print_typesig(S) || S <- TypeSigs],
    {TypeSigs, NewDefs}.

-infer_letfun(Env0, {letfun, Attrib, Fun = {id, NameAttrib, Name}, Args, What, Body}) ->
+infer_letfun(Env, {fun_clauses, Ann, Fun = {id, _, Name}, Type, Clauses}) ->
+    Type1 = check_type(Env, Type),
+    {NameSigs, Clauses1} = lists:unzip([ infer_letfun1(Env, Clause) || Clause <- Clauses ]),
+    {_, Sigs = [Sig | _]} = lists:unzip(NameSigs),
+    _ = [ begin
+            ClauseT = typesig_to_fun_t(ClauseSig),
+            unify(Env, ClauseT, Type1, {check_typesig, Name, ClauseT, Type1})
+          end || ClauseSig <- Sigs ],
+    {{Name, Sig}, desugar_clauses(Ann, Fun, Sig, Clauses1)};
+infer_letfun(Env, LetFun = {letfun, Ann, Fun, _, _, _}) ->
+    {{Name, Sig}, Clause} = infer_letfun1(Env, LetFun),
+    {{Name, Sig}, desugar_clauses(Ann, Fun, Sig, [Clause])}.
+
+infer_letfun1(Env0, {letfun, Attrib, Fun = {id, NameAttrib, Name}, Args, What, Body}) ->
    Env = Env0#env{ stateful = aeso_syntax:get_ann(stateful, Attrib, false),
                    current_function = Fun },
-    check_unique_arg_names(Fun, Args),
-    ArgTypes  = [{ArgName, check_type(Env, arg_type(ArgAnn, T))} || {arg, ArgAnn, ArgName, T} <- Args],
+    {NewEnv, {typed, _, {tuple, _, TypedArgs}, {tuple_t, _, ArgTypes}}} = infer_pattern(Env, {tuple, [{origin, system} | NameAttrib], Args}),
    ExpectedType = check_type(Env, arg_type(NameAttrib, What)),
-    NewBody={typed, _, _, ResultType} = check_expr(bind_vars(ArgTypes, Env), Body, ExpectedType),
-    NewArgs = [{arg, A1, {id, A2, ArgName}, T}
-               || {{_, T}, {arg, A1, {id, A2, ArgName}, _}} <- lists:zip(ArgTypes, Args)],
+    NewBody={typed, _, _, ResultType} = check_expr(NewEnv, Body, ExpectedType),
    NamedArgs = [],
-    TypeSig = {type_sig, Attrib, none, NamedArgs, [T || {arg, _, _, T} <- NewArgs], ResultType},
+    TypeSig = {type_sig, Attrib, none, NamedArgs, ArgTypes, ResultType},
    {{Name, TypeSig},
-     {letfun, Attrib, {id, NameAttrib, Name}, NewArgs, ResultType, NewBody}}.
+     {letfun, Attrib, {id, NameAttrib, Name}, TypedArgs, ResultType, NewBody}}.

-check_unique_arg_names(Fun, Args) ->
-    Name = fun({arg, _, {id, _, X}, _}) -> X end,
-    Names = lists:map(Name, Args),
-    Dups = lists:usort(Names -- lists:usort(Names)),
-    [ type_error({repeated_arg, Fun, Arg}) || Arg <- Dups ],
-    ok.
+desugar_clauses(Ann, Fun, {type_sig, _, _, _, ArgTypes, RetType}, Clauses) ->
+    NeedDesugar =
+        case Clauses of
+            [{letfun, _, _, As, _, _}] -> lists:any(fun({typed, _, {id, _, _}, _}) -> false; (_) -> true end, As);
+            _                          -> true
+        end,
+    case NeedDesugar of
+        false -> [Clause] = Clauses, Clause;
+        true  ->
+            NoAnn = [{origin, system}],
+            Args = [ {typed, NoAnn, {id, NoAnn, "x#" ++ integer_to_list(I)}, Type}
+                     || {I, Type} <- indexed(1, ArgTypes) ],
+            Tuple = fun([X]) -> X;
+                       (As) -> {typed, NoAnn, {tuple, NoAnn, As}, {tuple_t, NoAnn, ArgTypes}}
+                    end,
+            {letfun, Ann, Fun, Args, RetType,
+             {typed, NoAnn,
+              {switch, NoAnn, Tuple(Args),
+                [ {'case', AnnC, Tuple(ArgsC), Body}
+                || {letfun, AnnC, _, ArgsC, _, Body} <- Clauses ]}, RetType}}
+    end.

 print_typesig({Name, TypeSig}) ->
    ?PRINT_TYPES("Inferred ~s : ~s\n", [Name, pp(TypeSig)]).
@@ -1092,9 +1150,9 @@ get_call_chains(Graph, Visited, Queue, Stop, Acc) ->
    end.

 check_expr(Env, Expr, Type) ->
-    E = {typed, _, _, Type1} = infer_expr(Env, Expr),
+    {typed, Ann, Expr1, Type1} = infer_expr(Env, Expr),
    unify(Env, Type1, Type, {check_expr, Expr, Type1, Type}),
-    E.
+    {typed, Ann, Expr1, Type}.  %% Keep the user-given type

 infer_expr(_Env, Body={bool, As, _}) ->
    {typed, As, Body, {id, As, "bool"}};
@@ -1138,21 +1196,20 @@ infer_expr(Env, {list, As, Elems}) ->
    NewElems = [check_expr(Env, X, ElemType) || X <- Elems],
    {typed, As, {list, As, NewElems}, {app_t, As, {id, As, "list"}, [ElemType]}};
 infer_expr(Env, {list_comp, As, Yield, []}) ->
-    {typed, _, TypedYield, Type} = infer_expr(Env, Yield),
+    {typed, _, _, Type} = TypedYield = infer_expr(Env, Yield),
    {typed, As, {list_comp, As, TypedYield, []}, {app_t, As, {id, As, "list"}, [Type]}};
-infer_expr(Env, {list_comp, As, Yield, [{comprehension_bind, Arg, BExpr}|Rest]}) ->
-    BindVarType = fresh_uvar(As),
+infer_expr(Env, {list_comp, As, Yield, [{comprehension_bind, Pat, BExpr}|Rest]}) ->
    TypedBind = {typed, As2, _, TypeBExpr} = infer_expr(Env, BExpr),
+    {NewE, TypedPat = {typed, _, _, PatType}} = infer_pattern(Env, Pat),
    unify( Env
         , TypeBExpr
-         , {app_t, As, {id, As, "list"}, [BindVarType]}
-         , {list_comp, TypedBind, TypeBExpr, {app_t, As2, {id, As, "list"}, [BindVarType]}}),
-    NewE = bind_var(Arg, BindVarType, Env),
+         , {app_t, As, {id, As, "list"}, [PatType]}
+         , {list_comp, TypedBind, TypeBExpr, {app_t, As2, {id, As, "list"}, [PatType]}}),
    {typed, _, {list_comp, _, TypedYield, TypedRest}, ResType} =
        infer_expr(NewE, {list_comp, As, Yield, Rest}),
    { typed
    , As
-    , {list_comp, As, TypedYield, [{comprehension_bind, {typed, Arg, BindVarType}, TypedBind}|TypedRest]}
+    , {list_comp, As, TypedYield, [{comprehension_bind, TypedPat, TypedBind}|TypedRest]}
    , ResType};
 infer_expr(Env, {list_comp, AttrsL, Yield, [{comprehension_if, AttrsIF, Cond}|Rest]}) ->
    NewCond = check_expr(Env, Cond, {id, AttrsIF, "bool"}),
@@ -1162,8 +1219,8 @@ infer_expr(Env, {list_comp, AttrsL, Yield, [{comprehension_if, AttrsIF, Cond}|Re
    , AttrsL
    , {list_comp, AttrsL, TypedYield, [{comprehension_if, AttrsIF, NewCond}|TypedRest]}
    , ResType};
-infer_expr(Env, {list_comp, AsLC, Yield, [{letval, AsLV, Pattern, Type, E}|Rest]}) ->
-    NewE = {typed, _, _, PatType} = infer_expr(Env, {typed, AsLV, E, arg_type(AsLV, Type)}),
+infer_expr(Env, {list_comp, AsLC, Yield, [{letval, AsLV, Pattern, E}|Rest]}) ->
+    NewE = {typed, _, _, PatType} = infer_expr(Env, E),
    BlockType = fresh_uvar(AsLV),
    {'case', _, NewPattern, NewRest} =
        infer_case( Env
@@ -1175,7 +1232,7 @@ infer_expr(Env, {list_comp, AsLC, Yield, [{letval, AsLV, Pattern, Type, E}|Rest]
    {typed, _, {list_comp, _, TypedYield, TypedRest}, ResType} = NewRest,
    { typed
    , AsLC
-    , {list_comp, AsLC, TypedYield, [{letval, AsLV, NewPattern, Type, NewE}|TypedRest]}
+    , {list_comp, AsLC, TypedYield, [{letval, AsLV, NewPattern, NewE}|TypedRest]}
    , ResType
    };
 infer_expr(Env, {list_comp, AsLC, Yield, [Def={letfun, AsLF, _, _, _, _}|Rest]}) ->
@@ -1290,6 +1347,16 @@ infer_expr(Env, {block, Attrs, Stmts}) ->
    BlockType = fresh_uvar(Attrs),
    NewStmts = infer_block(Env, Attrs, Stmts, BlockType),
    {typed, Attrs, {block, Attrs, NewStmts}, BlockType};
+infer_expr(_Env, {record_or_map_error, Attrs, Fields}) ->
+    type_error({mixed_record_and_map, {record, Attrs, Fields}}),
+    Type = fresh_uvar(Attrs),
+    {typed, Attrs, {record, Attrs, []}, Type};
+infer_expr(Env, {record_or_map_error, Attrs, Expr, []}) ->
+    type_error({empty_record_or_map_update, {record, Attrs, Expr, []}}),
+    infer_expr(Env, Expr);
+infer_expr(Env, {record_or_map_error, Attrs, Expr, Fields}) ->
+    type_error({mixed_record_and_map, {record, Attrs, Expr, Fields}}),
+    infer_expr(Env, Expr);
 infer_expr(Env, {lam, Attrs, Args, Body}) ->
    ArgTypes = [fresh_uvar(As) || {arg, As, _, _} <- Args],
    ArgPatterns = [{typed, As, Pat, check_type(Env, T)} || {arg, As, Pat, T} <- Args],
@@ -1298,7 +1365,7 @@ infer_expr(Env, {lam, Attrs, Args, Body}) ->
        infer_case(Env, Attrs, {tuple, Attrs, ArgPatterns}, {tuple_t, Attrs, ArgTypes}, Body, ResultType),
    NewArgs = [{arg, As, NewPat, NewT} || {typed, As, NewPat, NewT} <- NewArgPatterns],
    {typed, Attrs, {lam, Attrs, NewArgs, NewBody}, {fun_t, Attrs, [], ArgTypes, ResultType}};
-infer_expr(Env, Let = {letval, Attrs, _, _, _}) ->
+infer_expr(Env, Let = {letval, Attrs, _, _}) ->
    type_error({missing_body_for_let, Attrs}),
    infer_expr(Env, {block, Attrs, [Let, abort_expr(Attrs, "missing body")]});
 infer_expr(Env, Let = {letfun, Attrs, _, _, _, _}) ->
@@ -1361,15 +1428,19 @@ infer_op(Env, As, Op, Args, InferOp) ->
    unify(Env, ArgTypes, OperandTypes, {infer_app, Op, Args, Inferred, ArgTypes}),
    {typed, As, {app, As, Op, TypedArgs}, ResultType}.

-infer_case(Env, Attrs, Pattern, ExprType, Branch, SwitchType) ->
+infer_pattern(Env, Pattern) ->
    Vars = free_vars(Pattern),
    Names = [N || {id, _, N} <- Vars, N /= "_"],
    case Names -- lists:usort(Names) of
        [] -> ok;
        Nonlinear -> type_error({non_linear_pattern, Pattern, lists:usort(Nonlinear)})
    end,
-    NewEnv = bind_vars([{Var, fresh_uvar(Ann)} || Var = {id, Ann, _} <- Vars], Env#env{ in_pattern = true }),
-    NewPattern = {typed, _, _, PatType} = infer_expr(NewEnv, Pattern),
+    NewEnv = bind_vars([{Var, fresh_uvar(Ann1)} || Var = {id, Ann1, _} <- Vars], Env#env{ in_pattern = true }),
+    NewPattern = infer_expr(NewEnv, Pattern),
+    {NewEnv#env{ in_pattern = Env#env.in_pattern }, NewPattern}.
+
+infer_case(Env, Attrs, Pattern, ExprType, Branch, SwitchType) ->
+    {NewEnv, NewPattern = {typed, _, _, PatType}} = infer_pattern(Env, Pattern),
    NewBranch  = check_expr(NewEnv#env{ in_pattern = false }, Branch, SwitchType),
    unify(Env, PatType, ExprType, {case_pat, Pattern, PatType, ExprType}),
    {'case', Attrs, NewPattern, NewBranch}.
@@ -1384,11 +1455,11 @@ infer_block(Env, Attrs, [Def={letfun, Ann, _, _, _, _}|Rest], BlockType) ->
    FunT = typesig_to_fun_t(TypeSig),
    NewE = bind_var({id, Ann, Name}, FunT, Env),
    [LetFun|infer_block(NewE, Attrs, Rest, BlockType)];
-infer_block(Env, _, [{letval, Attrs, Pattern, Type, E}|Rest], BlockType) ->
-    NewE = {typed, _, _, PatType} = infer_expr(Env, {typed, Attrs, E, arg_type(aeso_syntax:get_ann(Pattern), Type)}),
+infer_block(Env, _, [{letval, Attrs, Pattern, E}|Rest], BlockType) ->
+    NewE = {typed, _, _, PatType} = infer_expr(Env, E),
    {'case', _, NewPattern, {typed, _, {block, _, NewRest}, _}} =
        infer_case(Env, Attrs, Pattern, PatType, {block, Attrs, Rest}, BlockType),
-    [{letval, Attrs, NewPattern, Type, NewE}|NewRest];
+    [{letval, Attrs, NewPattern, NewE}|NewRest];
 infer_block(Env, Attrs, [E|Rest], BlockType) ->
    [infer_expr(Env, E)|infer_block(Env, Attrs, Rest, BlockType)].

@@ -1430,18 +1501,13 @@ infer_prefix({IntOp,As}) when IntOp =:= '-' ->
 abort_expr(Ann, Str) ->
    {app, Ann, {id, Ann, "abort"}, [{string, Ann, Str}]}.

-free_vars({int, _, _}) ->
-    [];
-free_vars({char, _, _}) ->
-    [];
-free_vars({string, _, _}) ->
-    [];
-free_vars({bool, _, _}) ->
-    [];
-free_vars(Id={id, _, _}) ->
-    [Id];
-free_vars({con, _, _}) ->
-    [];
+free_vars({int, _, _})    -> [];
+free_vars({char, _, _})   -> [];
+free_vars({string, _, _}) -> [];
+free_vars({bool, _, _})   -> [];
+free_vars(Id={id, _, _})  -> [Id];
+free_vars({con, _, _})    -> [];
+free_vars({qcon, _, _})   -> [];
 free_vars({tuple, _, Cpts}) ->
    free_vars(Cpts);
 free_vars({list, _, Elems}) ->
@@ -1450,6 +1516,8 @@ free_vars({app, _, {'::', _}, Args}) ->
    free_vars(Args);
 free_vars({app, _, {con, _, _}, Args}) ->
    free_vars(Args);
+free_vars({app, _, {qcon, _, _}, Args}) ->
+    free_vars(Args);
 free_vars({record, _, Fields}) ->
    free_vars([E || {field, _, _, E} <- Fields]);
 free_vars({typed, _, A, _}) ->
@@ -2008,7 +2076,8 @@ unify1(_Env, {qcon, _, Name}, {qcon, _, Name}, _When) ->
    true;
 unify1(_Env, {bytes_t, _, Len}, {bytes_t, _, Len}, _When) ->
    true;
-unify1(Env, {fun_t, _, Named1, Args1, Result1}, {fun_t, _, Named2, Args2, Result2}, When) ->
+unify1(Env, {fun_t, _, Named1, Args1, Result1}, {fun_t, _, Named2, Args2, Result2}, When)
+    when length(Args1) == length(Args2) ->
    unify(Env, Named1, Named2, When) andalso
    unify(Env, Args1, Args2, When) andalso unify(Env, Result1, Result2, When);
 unify1(Env, {app_t, _, {Tag, _, F}, Args1}, {app_t, _, {Tag, _, F}, Args2}, When)
@@ -2197,6 +2266,24 @@ mk_t_err(Pos, Msg) ->
 mk_t_err(Pos, Msg, Ctxt) ->
    aeso_errors:new(type_error, Pos, lists:flatten(Msg), lists:flatten(Ctxt)).

+mk_error({higher_kinded_typevar, T}) ->
+    Msg = io_lib:format("Type ~s is a higher kinded type variable\n"
+                        "(takes another type as an argument)\n", [pp(instantiate(T))]
+                       ),
+    mk_t_err(pos(T), Msg);
+mk_error({wrong_type_arguments, X, ArityGiven, ArityReal}) ->
+    Msg = io_lib:format("Arity for ~s doesn't match. Expected ~p, got ~p\n"
+                       , [pp(instantiate(X)), ArityReal, ArityGiven]
+                       ),
+    mk_t_err(pos(X), Msg);
+mk_error({unnamed_map_update_with_default, Upd}) ->
+    Msg = "Invalid map update with default\n",
+    mk_t_err(pos(Upd), Msg);
+mk_error({fundecl_must_have_funtype, _Ann, Id, Type}) ->
+    Msg = io_lib:format("~s at ~s was declared with an invalid type ~s.\n"
+                       "Entrypoints and functions must have functional types"
+                       , [pp(Id), pp_loc(Id), pp(instantiate(Type))]),
+    mk_t_err(pos(Id), Msg);
 mk_error({cannot_unify, A, B, When}) ->
    Msg = io_lib:format("Cannot unify ~s\n         and ~s\n",
                        [pp(instantiate(A)), pp(instantiate(B))]),
@@ -2279,14 +2366,6 @@ mk_error({indexed_type_must_be_word, Type, Type1}) ->
    Msg = io_lib:format("The indexed type ~s (at ~s) equals ~s which is not a word type\n",
                        [pp_type("", Type), pp_loc(Type), pp_type("", Type1)]),
    mk_t_err(pos(Type), Msg);
-mk_error({payload_type_must_be_string, Type, Type}) ->
-    Msg = io_lib:format("The payload type ~s (at ~s) should be string\n",
-                        [pp_type("", Type), pp_loc(Type)]),
-    mk_t_err(pos(Type), Msg);
-mk_error({payload_type_must_be_string, Type, Type1}) ->
-    Msg = io_lib:format("The payload type ~s (at ~s) equals ~s but it should be string\n",
-                        [pp_type("", Type), pp_loc(Type), pp_type("", Type1)]),
-    mk_t_err(pos(Type), Msg);
 mk_error({event_0_to_3_indexed_values, Constr}) ->
    Msg = io_lib:format("The event constructor ~s (at ~s) has too many indexed values (max 3)\n",
                        [name(Constr), pp_loc(Constr)]),
@@ -2330,13 +2409,21 @@ mk_error({include, _, {string, Pos, Name}}) ->
                        [binary_to_list(Name), pp_loc(Pos)]),
    mk_t_err(pos(Pos), Msg);
 mk_error({namespace, _Pos, {con, Pos, Name}, _Def}) ->
-    Msg = io_lib:format("Nested namespace not allowed\nNamespace '~s' at ~s not defined at top level.\n",
+    Msg = io_lib:format("Nested namespaces are not allowed\nNamespace '~s' at ~s not defined at top level.\n",
+                        [Name, pp_loc(Pos)]),
+    mk_t_err(pos(Pos), Msg);
+mk_error({contract, _Pos, {con, Pos, Name}, _Def}) ->
+    Msg = io_lib:format("Nested contracts are not allowed\nContract '~s' at ~s not defined at top level.\n",
+                        [Name, pp_loc(Pos)]),
+    mk_t_err(pos(Pos), Msg);
+mk_error({type_decl, _, {id, Pos, Name}, _}) ->
+    Msg = io_lib:format("Empty type declarations are not supported\nType ~s at ~s lacks a definition\n",
+                        [Name, pp_loc(Pos)]),
+    mk_t_err(pos(Pos), Msg);
+mk_error({letval, _Pos, {id, Pos, Name}, _Def}) ->
+    Msg = io_lib:format("Toplevel \"let\" definitions are not supported\nValue ~s at ~s could be replaced by 0-argument function\n",
                        [Name, pp_loc(Pos)]),
    mk_t_err(pos(Pos), Msg);
-mk_error({repeated_arg, Fun, Arg}) ->
-    Msg = io_lib:format("Repeated argument ~s to function ~s (at ~s).\n",
-                        [Arg, pp(Fun), pp_loc(Fun)]),
-    mk_t_err(pos(Fun), Msg);
 mk_error({stateful_not_allowed, Id, Fun}) ->
    Msg = io_lib:format("Cannot reference stateful function ~s (at ~s)\nin the definition of non-stateful function ~s.\n",
                        [pp(Id), pp_loc(Id), pp(Fun)]),
@@ -2456,6 +2543,14 @@ mk_error({compiler_version_mismatch, Ann, Version, Op, Bound}) ->
                        "because it does not satisfy the constraint"
                        " ~s ~s ~s\n", [PrintV(Version), Op, PrintV(Bound)]),
    mk_t_err(pos(Ann), Msg);
+mk_error({empty_record_or_map_update, Expr}) ->
+    Msg = io_lib:format("Empty record/map update\n~s",
+                        [pp_expr("  ", Expr)]),
+    mk_t_err(pos(Expr), Msg);
+mk_error({mixed_record_and_map, Expr}) ->
+    Msg = io_lib:format("Mixed record fields and map keys in\n~s",
+                        [pp_expr("  ", Expr)]),
+    mk_t_err(pos(Expr), Msg);
 mk_error(Err) ->
    Msg = io_lib:format("Unknown error: ~p\n", [Err]),
    mk_t_err(pos(0, 0), Msg).
@@ -2733,3 +2828,7 @@ updates_key(Name, Updates) ->
    Updates1 = [ Upd  || {Upd, false, _} <- Xs ],
    More     = [ Rest || {_, true, Rest} <- Xs ],
    {More, Updates1}.
+
+indexed(I, Xs) ->
+    lists:zip(lists:seq(I, I + length(Xs) - 1), Xs).
+
@@ -24,6 +24,8 @@
 -type var_name() :: string().
 -type sophia_name() :: [string()].

+-type state_reg() :: pos_integer().
+
 -type builtin() :: atom().

 -type op() :: '+' | '-' | '*' | '/' | mod | '^' | '++' | '::' |
@@ -61,6 +63,8 @@
               | {funcall, fexpr(), [fexpr()]}  %% Call to unknown function
               | {closure, fun_name(), fexpr()}
               | {switch, fsplit()}
+               | {set_state, state_reg(), fexpr()}
+               | {get_state, state_reg()}
               %% The following (unapplied top-level functions/builtins and
               %% lambdas) are generated by the fcode compiler, but translated
               %% to closures by the lambda lifter.
@@ -109,6 +113,7 @@

 -type fcode() :: #{ contract_name := string(),
                    state_type    := ftype(),
+                    state_layout  := state_layout(),
                    event_type    := ftype() | none,
                    functions     := #{ fun_name() => fun_def() },
                    payable       := boolean() }.
@@ -130,15 +135,18 @@
                 | {namespace, string()}
                 | {abstract_contract, string()}.

-type env() :: #{ type_env   := type_env(),
-                  fun_env    := fun_env(),
-                  con_env    := con_env(),
-                  event_type => aeso_syntax:typedef(),
-                  builtins   := builtins(),
-                  options    := [option()],
-                  context    => context(),
-                  vars       => [var_name()],
-                  functions  := #{ fun_name() => fun_def() } }.
+-type state_layout() :: {tuple, [state_layout()]} | {reg, state_reg()}.
+
+-type env() :: #{ type_env     := type_env(),
+                  fun_env      := fun_env(),
+                  con_env      := con_env(),
+                  event_type   => aeso_syntax:typedef(),
+                  builtins     := builtins(),
+                  options      := [option()],
+                  state_layout => state_layout(),
+                  context      => context(),
+                  vars         => [var_name()],
+                  functions    := #{ fun_name() => fun_def() } }.

 -define(HASH_BYTES, 32).

@@ -149,12 +157,14 @@
 -spec ast_to_fcode(aeso_syntax:ast(), [option()]) -> fcode().
 ast_to_fcode(Code, Options) ->
    Verbose = lists:member(pp_fcode, Options),
+    init_fresh_names(),
    FCode1 = to_fcode(init_env(Options), Code),
    [io:format("-- Before lambda lifting --\n~s\n\n", [format_fcode(FCode1)]) || Verbose],
-    FCode2 = lambda_lift(FCode1),
-    [ io:format("-- After lambda lifting --\n~s\n\n", [format_fcode(FCode2)]) || Verbose, FCode2 /= FCode1 ],
-    FCode3 = optimize_fcode(FCode2),
-    [ io:format("-- After optimization --\n~s\n\n", [format_fcode(FCode3)]) || Verbose, FCode3 /= FCode2 ],
+    FCode2 = optimize_fcode(FCode1),
+    [ io:format("-- After optimization --\n~s\n\n", [format_fcode(FCode2)]) || Verbose, FCode2 /= FCode1 ],
+    FCode3 = lambda_lift(FCode2),
+    [ io:format("-- After lambda lifting --\n~s\n\n", [format_fcode(FCode3)]) || Verbose, FCode3 /= FCode2 ],
+    clear_fresh_names(),
    FCode3.

 %% -- Environment ------------------------------------------------------------
@@ -206,6 +216,8 @@ builtins() ->
                     || {NS, Funs} <- Scopes,
                        {Fun, Arity} <- Funs ]).

+state_layout(Env) -> maps:get(state_layout, Env, {reg, 1}).
+
 -define(type(T),       fun([])     -> T end).
 -define(type(X, T),    fun([X])    -> T end).
 -define(type(X, Y, T), fun([X, Y]) -> T end).
@@ -221,7 +233,7 @@ init_type_env() ->
       ["hash"]         => ?type(hash),
       ["signature"]    => ?type(signature),
       ["oracle"]       => ?type(Q, R, {oracle, Q, R}),
-       ["oracle_query"] => ?type(_, _, oracle_query),    %% TODO: not in Fate
+       ["oracle_query"] => ?type(_, _, oracle_query),
       ["list"]         => ?type(T, {list, T}),
       ["map"]          => ?type(K, V, {map, K, V}),
       ["option"]       => ?type(T, {variant, [[], [T]]}),
@@ -229,7 +241,13 @@ init_type_env() ->
     }.

 is_no_code(Env) ->
-    proplists:get_value(no_code, maps:get(options, Env, []), false).
+    get_option(no_code, Env).
+
+get_option(Opt, Env) ->
+    get_option(Opt, Env, false).
+
+get_option(Opt, Env, Default) ->
+    proplists:get_value(Opt, maps:get(options, Env, []), Default).

 %% -- Compilation ------------------------------------------------------------

@@ -242,11 +260,13 @@ to_fcode(Env, [{contract, Attrs, MainCon = {con, _, Main}, Decls}]) ->
                                          [Main, "Chain", "event"] => {chain_event, 1}} },
    #{ functions := Funs } = Env1 =
        decls_to_fcode(MainEnv, Decls),
-    StateType = lookup_type(Env1, [Main, "state"], [], {tuple, []}),
-    EventType = lookup_type(Env1, [Main, "event"], [], none),
-    Payable   = proplists:get_value(payable, Attrs, false),
+    StateType   = lookup_type(Env1, [Main, "state"], [], {tuple, []}),
+    EventType   = lookup_type(Env1, [Main, "event"], [], none),
+    StateLayout = state_layout(Env1),
+    Payable     = proplists:get_value(payable, Attrs, false),
    #{ contract_name => Main,
       state_type    => StateType,
+       state_layout  => StateLayout,
       event_type    => EventType,
       payable       => Payable,
       functions     => add_init_function(Env1, MainCon, StateType,
@@ -266,14 +286,11 @@ decls_to_fcode(Env, Decls) ->
    %% environment.
    Env1 = add_fun_env(Env, Decls),
    lists:foldl(fun(D, E) ->
-                    init_fresh_names(),
                    R = decl_to_fcode(E, D),
-                    clear_fresh_names(),
                    R
                end, Env1, Decls).

 -spec decl_to_fcode(env(), aeso_syntax:decl()) -> env().
-decl_to_fcode(Env, {type_decl, _, _, _}) -> Env;
 decl_to_fcode(Env = #{context := {main_contract, _}}, {fun_decl, _, Id, _}) ->
    case is_no_code(Env) of
        false -> fcode_error({missing_definition, Id});
@@ -304,14 +321,15 @@ typedef_to_fcode(Env, Id = {id, _, Name}, Xs, Def) ->
    FDef = fun(Args) when length(Args) == length(Xs) ->
                Sub = maps:from_list(lists:zip([X || {tvar, _, X} <- Xs], Args)),
                case Def of
-                    {record_t, Fields} -> {todo, Xs, Args, record_t, Fields};
+                    {record_t, Fields} ->
+                        {tuple, [type_to_fcode(Env, Sub, T) || {field_t, _, _, T} <- Fields]};
                    {variant_t, Cons}  ->
                        FCons = [ begin
                                      {constr_t, _, _, Ts} = Con,
                                      [type_to_fcode(Env, Sub, T) || T <- Ts]
                                  end || Con <- Cons ],
                        {variant, FCons};
-                    {alias_t, Type}    -> {todo, Xs, Args, alias_t, Type}
+                    {alias_t, Type}    -> type_to_fcode(Env, Sub, Type)
                end;
              (Args) -> internal_error({type_arity_mismatch, Name, length(Args), length(Xs)})
           end,
@@ -333,7 +351,34 @@ typedef_to_fcode(Env, Id = {id, _, Name}, Xs, Def) ->
             "event" -> Env1#{ event_type => Def };
             _       -> Env1
           end,
-    bind_type(Env2, Q, FDef).
+    Env3 = compute_state_layout(Env2, Name, FDef),
+    bind_type(Env3, Q, FDef).
+
+compute_state_layout(Env = #{ context := {main_contract, _} }, "state", Type) ->
+    NoLayout = get_option(no_flatten_state, Env),
+    Layout =
+        case Type([]) of
+            _ when NoLayout -> {reg, 1};
+            T ->
+                {_, L} = compute_state_layout(1, T),
+                L
+        end,
+    Env#{ state_layout => Layout };
+compute_state_layout(Env, _, _) -> Env.
+
+compute_state_layout(R, {tuple, [T]}) ->
+    compute_state_layout(R, T);
+compute_state_layout(R, {tuple, Ts}) ->
+    {R1, Ls} = compute_state_layout(R, Ts),
+    {R1, {tuple, Ls}};
+compute_state_layout(R, []) ->
+    {R, []};
+compute_state_layout(R, [H | T]) ->
+    {R1, H1} = compute_state_layout(R, H),
+    {R2, T1} = compute_state_layout(R1, T),
+    {R2, [H1 | T1]};
+compute_state_layout(R, _) ->
+    {R + 1, {reg, R}}.

 check_state_and_event_types(#{ context := {main_contract, _} }, Id, [_ | _]) ->
    case Id of
@@ -369,9 +414,12 @@ type_to_fcode(Env, Sub, {fun_t, _, Named, Args, Res}) ->
 type_to_fcode(_Env, _Sub, Type) ->
    error({todo, Type}).

-spec args_to_fcode(env(), [aeso_syntax:arg()]) -> [{var_name(), ftype()}].
+-spec args_to_fcode(env(), [aeso_syntax:pat()]) -> [{var_name(), ftype()}].
 args_to_fcode(Env, Args) ->
-    [ {Name, type_to_fcode(Env, Type)} || {arg, _, {id, _, Name}, Type} <- Args ].
+    [ case Arg of
+          {id, _, Name} -> {Name, type_to_fcode(Env, Type)};
+          _ -> internal_error({bad_arg, Arg})   %% Pattern matching has been moved to the rhs at this point
+      end || {typed, _, Arg, Type} <- Args ].

 -define(make_let(X, Expr, Body),
        make_let(Expr, fun(X) -> Body end)).
@@ -386,6 +434,13 @@ make_let(Expr, Body) ->
            {'let', X, Expr, Body({var, X})}
    end.

+let_bind(X, {var, Y}, Body) -> rename([{X, Y}], Body);
+let_bind(X, Expr, Body)     -> {'let', X, Expr, Body}.
+
+let_bind(Binds, Body) ->
+    lists:foldr(fun({X, E}, Rest) -> let_bind(X, E, Rest) end,
+                Body, Binds).
+
 -spec expr_to_fcode(env(), aeso_syntax:expr()) -> fexpr().
 expr_to_fcode(Env, {typed, _, Expr, Type}) ->
    expr_to_fcode(Env, Type, Expr);
@@ -446,7 +501,7 @@ expr_to_fcode(Env, _Type, {app, _, {typed, _, {C, _, _} = Con, _}, Args}) when C

 %% Tuples
 expr_to_fcode(Env, _Type, {tuple, _, Es}) ->
-    {tuple, [expr_to_fcode(Env, E) || E <- Es]};
+    make_tuple([expr_to_fcode(Env, E) || E <- Es]);

 %% Records
 expr_to_fcode(Env, Type, {proj, _Ann, Rec = {typed, _, _, RecType}, {id, _, X}}) ->
@@ -458,18 +513,28 @@ expr_to_fcode(Env, Type, {proj, _Ann, Rec = {typed, _, _, RecType}, {id, _, X}})
            FArgs = [type_to_fcode(Env, Arg) || Arg <- Args],
            {remote_u, FArgs, type_to_fcode(Env, Ret), expr_to_fcode(Env, Rec),
                       {entrypoint, list_to_binary(X)}};
+        {record_t, [_]} -> expr_to_fcode(Env, Rec); %% Singleton record
        {record_t, _} ->
            {proj, expr_to_fcode(Env, Rec), field_index(Rec, X)}
    end;

+expr_to_fcode(Env, {record_t, [FieldT]}, {record, _Ann, [_] = Fields}) ->
+    {set, E} = field_value(FieldT, Fields),
+    expr_to_fcode(Env, E);
 expr_to_fcode(Env, {record_t, FieldTypes}, {record, _Ann, Fields}) ->
    FVal = fun(F) ->
             %% All fields are present and no updates
             {set, E} = field_value(F, Fields),
             expr_to_fcode(Env, E)
           end,
-    {tuple, lists:map(FVal, FieldTypes)};
+    make_tuple(lists:map(FVal, FieldTypes));

+expr_to_fcode(Env, {record_t, [FieldT]}, {record, _Ann, Rec, Fields}) ->
+    case field_value(FieldT, Fields) of
+        false       -> expr_to_fcode(Env, Rec);
+        {set, E}    -> expr_to_fcode(Env, E);
+        {upd, Z, E} -> {'let', Z, expr_to_fcode(Env, Rec), expr_to_fcode(bind_var(Env, Z), E)}
+    end;
 expr_to_fcode(Env, {record_t, FieldTypes}, {record, _Ann, Rec, Fields}) ->
    X    = fresh_name(),
    Proj = fun(I) -> {proj, {var, X}, I - 1} end,
@@ -501,9 +566,12 @@ expr_to_fcode(Env, _Type, {app, _, {'..', _}, [A, B]}) ->

 expr_to_fcode(Env, _Type, {list_comp, _, Yield, []}) ->
    {op, '::', [expr_to_fcode(Env, Yield), nil]};
-expr_to_fcode(Env, _Type, {list_comp, As, Yield, [{comprehension_bind, {typed, {id, _, Arg}, _}, BindExpr}|Rest]}) ->
+expr_to_fcode(Env, _Type, {list_comp, As, Yield, [{comprehension_bind, Pat = {typed, _, _, PatType}, BindExpr}|Rest]}) ->
+    Arg  = fresh_name(),
    Env1 = bind_var(Env, Arg),
-    Bind = {lam, [Arg], expr_to_fcode(Env1, {list_comp, As, Yield, Rest})},
+    Bind = {lam, [Arg], expr_to_fcode(Env1, {switch, As, {typed, As, {id, As, Arg}, PatType},
+                                                [{'case', As, Pat, {list_comp, As, Yield, Rest}},
+                                                 {'case', As, {id, As, "_"}, {list, As, []}}]})},
    {def_u, FlatMap, _} = resolve_fun(Env, ["ListInternal", "flat_map"]),
    {def, FlatMap, [Bind, expr_to_fcode(Env, BindExpr)]};
 expr_to_fcode(Env, Type, {list_comp, As, Yield, [{comprehension_if, _, Cond}|Rest]}) ->
@@ -511,7 +579,7 @@ expr_to_fcode(Env, Type, {list_comp, As, Yield, [{comprehension_if, _, Cond}|Res
            expr_to_fcode(Env, Type, {list_comp, As, Yield, Rest}),
            nil
           );
-expr_to_fcode(Env, Type, {list_comp, As, Yield, [LV = {letval, _, _, _, _}|Rest]}) ->
+expr_to_fcode(Env, Type, {list_comp, As, Yield, [LV = {letval, _, _, _}|Rest]}) ->
    expr_to_fcode(Env, Type, {block, As, [LV, {list_comp, As, Yield, Rest}]});
 expr_to_fcode(Env, Type, {list_comp, As, Yield, [LF = {letfun, _, _, _, _, _}|Rest]}) ->
    expr_to_fcode(Env, Type, {block, As, [LF, {list_comp, As, Yield, Rest}]});
@@ -556,8 +624,8 @@ expr_to_fcode(Env, _Type, {app, _, Fun = {typed, _, _, {fun_t, _, NamedArgsT, _,
    Args1 = get_named_args(NamedArgsT, Args),
    FArgs = [expr_to_fcode(Env, Arg) || Arg <- Args1],
    case expr_to_fcode(Env, Fun) of
-        {builtin_u, B, _Ar, TypeArgs}     -> builtin_to_fcode(B, FArgs ++ TypeArgs);
-        {builtin_u, B, _Ar}               -> builtin_to_fcode(B, FArgs);
+        {builtin_u, B, _Ar, TypeArgs}     -> builtin_to_fcode(state_layout(Env), B, FArgs ++ TypeArgs);
+        {builtin_u, B, _Ar}               -> builtin_to_fcode(state_layout(Env), B, FArgs);
        {def_u, F, _Ar}                   -> {def, F, FArgs};
        {remote_u, ArgsT, RetT, Ct, RFun} -> {remote, ArgsT, RetT, Ct, RFun, FArgs};
        FFun ->
@@ -621,6 +689,13 @@ make_if(Cond, Then, Else) ->
    X = fresh_name(),
    {'let', X, Cond, make_if({var, X}, Then, Else)}.

+-spec make_tuple([fexpr()]) -> fexpr().
+make_tuple([E]) -> E;
+make_tuple(Es) -> {tuple, Es}.
+
+-spec strip_singleton_tuples(ftype()) -> ftype().
+strip_singleton_tuples({tuple, [T]}) -> strip_singleton_tuples(T);
+strip_singleton_tuples(T) -> T.

 get_oracle_type(oracle_register,     {fun_t, _, _, _, OType})       -> OType;
 get_oracle_type(oracle_query,        {fun_t, _, _, [OType | _], _}) -> OType;
@@ -649,7 +724,7 @@ validate_aens_resolve_type(Ann, {app_t, _, _, [Type]}, {variant, [[], [FType]]})

 ensure_first_order_entrypoint(Ann, Id = {id, _, Name}, Args, Ret, FArgs, FRet) ->
    [ ensure_first_order(FT, {invalid_entrypoint, higher_order, Ann1, Id, {argument, X, T}})
-      || {{arg, Ann1, X, T}, {_, FT}} <- lists:zip(Args, FArgs) ],
+      || {{typed, Ann1, X, T}, {_, FT}} <- lists:zip(Args, FArgs) ],
    [ ensure_first_order(FRet, {invalid_entrypoint, higher_order, Ann, Id, {result, Ret}})
      || Name /= "init" ],  %% init can return higher-order values, since they're written to the store
                            %% rather than being returned.
@@ -708,10 +783,13 @@ split_tree(Env, Vars, Alts = [{'case', Pats, Body} | _]) ->
            {nosplit, rename(Ren, Body)};
        I when is_integer(I) ->
            {Vars0, [{X, Type} | Vars1]} = lists:split(I - 1, Vars),
+            Type1 = strip_singleton_tuples(Type),
            SAlts = merge_alts(I, X, [ split_alt(I, A) || A <- Alts ]),
-            Cases = [ {'case', SPat, split_tree(Env, Vars0 ++ split_vars(SPat, Type) ++ Vars1, FAlts)}
+            MakeCase = fun({var, Z}, Split) -> {'case', {var, "_"}, rename_split([{Z, X}], Split)};
+                          (SPat, Split)     -> {'case', SPat, Split} end,
+            Cases = [ MakeCase(SPat, split_tree(Env, Vars0 ++ split_vars(SPat, Type1) ++ Vars1, FAlts))
                      || {SPat, FAlts} <- SAlts ],
-            {split, Type, X, Cases}
+            {split, Type1, X, Cases}
    end.

 -spec merge_alts(integer(), var_name(), [{fsplit_pat(), falt()}]) -> [{fsplit_pat(), [falt()]}].
@@ -834,7 +912,7 @@ pat_to_fcode(Env, _Type, {app, _, {typed, _, {C, _, _} = Con, _}, Pats}) when C
    #con_tag{tag = I, arities = As} = lookup_con(Env, Con),
    {con, As, I, [pat_to_fcode(Env, Pat) || Pat <- Pats]};
 pat_to_fcode(Env, _Type, {tuple, _, Pats}) ->
-    {tuple, [ pat_to_fcode(Env, Pat) || Pat <- Pats ]};
+    make_tuple([ pat_to_fcode(Env, Pat) || Pat <- Pats ]);
 pat_to_fcode(_Env, _Type, {bool, _, B})   -> {bool, B};
 pat_to_fcode(_Env, _Type, {int, _, N})    -> {int, N};
 pat_to_fcode(_Env, _Type, {char, _, N})   -> {int, N};
@@ -852,8 +930,8 @@ pat_to_fcode(Env, {record_t, Fields}, {record, _, FieldPats}) ->
                        {set, Pat} -> Pat
                        %% {upd, _, _} is impossible in patterns
                    end end,
-    {tuple, [pat_to_fcode(Env, FieldPat(Field))
-             || Field <- Fields]};
+    make_tuple([pat_to_fcode(Env, FieldPat(Field))
+                || Field <- Fields]);

 pat_to_fcode(_Env, Type, Pat) ->
    error({todo, Pat, ':', Type}).
@@ -887,10 +965,16 @@ decision_tree_to_fcode({'if', A, Then, Else}) ->
 %% -- Statements --

 -spec stmts_to_fcode(env(), [aeso_syntax:stmt()]) -> fexpr().
-stmts_to_fcode(Env, [{letval, _, {typed, _, {id, _, X}, _}, _, Expr} | Stmts]) ->
+stmts_to_fcode(Env, [{letval, _, {typed, _, {id, _, X}, _}, Expr} | Stmts]) ->
    {'let', X, expr_to_fcode(Env, Expr), stmts_to_fcode(bind_var(Env, X), Stmts)};
+stmts_to_fcode(Env, [{letval, Ann, Pat, Expr} | Stmts]) ->
+    expr_to_fcode(Env, {switch, Ann, Expr, [{'case', Ann, Pat, {block, Ann, Stmts}}]});
 stmts_to_fcode(Env, [{letfun, Ann, {id, _, X}, Args, _Type, Expr} | Stmts]) ->
-    {'let', X, expr_to_fcode(Env, {lam, Ann, Args, Expr}),
+    LamArgs = [ case Arg of
+                    {typed, Ann1, Id, T} -> {arg, Ann1, Id, T};
+                    _ -> internal_error({bad_arg, Arg})   %% pattern matching has been desugared
+                end || Arg <- Args ],
+    {'let', X, expr_to_fcode(Env, {lam, Ann, LamArgs, Expr}),
               stmts_to_fcode(bind_var(Env, X), Stmts)};
 stmts_to_fcode(Env, [Expr]) ->
    expr_to_fcode(Env, Expr);
@@ -909,23 +993,40 @@ op_builtins() ->
     crypto_ecverify_secp256k1, crypto_ecrecover_secp256k1
    ].

-builtin_to_fcode(require, [Cond, Msg]) ->
+set_state({reg, R}, Val) ->
+    {set_state, R, Val};
+set_state({tuple, Ls}, Val) ->
+    ?make_let(X, Val,
+    lists:foldr(fun({I, L}, Code) ->
+                    {'let', "_", set_state(L, {proj, X, I - 1}), Code}
+                end, {tuple, []}, indexed(Ls))).
+
+get_state({reg, R}) ->
+    {get_state, R};
+get_state({tuple, Ls}) ->
+    {tuple, [get_state(L) || L <- Ls]}.
+
+builtin_to_fcode(Layout, set_state, [Val]) ->
+    set_state(Layout, Val);
+builtin_to_fcode(Layout, get_state, []) ->
+    get_state(Layout);
+builtin_to_fcode(_Layout, require, [Cond, Msg]) ->
    make_if(Cond, {tuple, []}, {builtin, abort, [Msg]});
-builtin_to_fcode(chain_event, [Event]) ->
+builtin_to_fcode(_Layout, chain_event, [Event]) ->
    {def, event, [Event]};
-builtin_to_fcode(map_delete, [Key, Map]) ->
+builtin_to_fcode(_Layout, map_delete, [Key, Map]) ->
    {op, map_delete, [Map, Key]};
-builtin_to_fcode(map_member, [Key, Map]) ->
+builtin_to_fcode(_Layout, map_member, [Key, Map]) ->
    {op, map_member, [Map, Key]};
-builtin_to_fcode(map_lookup, [Key0, Map0]) ->
+builtin_to_fcode(_Layout, map_lookup, [Key0, Map0]) ->
    ?make_let(Key, Key0,
    ?make_let(Map, Map0,
     make_if({op, map_member, [Map, Key]},
             {con, [0, 1], 1, [{op, map_get, [Map, Key]}]},
             {con, [0, 1], 0, []})));
-builtin_to_fcode(map_lookup_default, [Key, Map, Def]) ->
+builtin_to_fcode(_Layout, map_lookup_default, [Key, Map, Def]) ->
    {op, map_get_d, [Map, Key, Def]};
-builtin_to_fcode(Builtin, Args) ->
+builtin_to_fcode(_Layout, Builtin, Args) ->
    case lists:member(Builtin, op_builtins()) of
        true  -> {op, Builtin, Args};
        false -> {builtin, Builtin, Args}
@@ -940,8 +1041,9 @@ add_init_function(Env, Main, StateType, Funs0) ->
            Funs     = add_default_init_function(Env, Main, StateType, Funs0),
            InitName = {entrypoint, <<"init">>},
            InitFun  = #{ body := InitBody} = maps:get(InitName, Funs),
-            Funs#{ InitName => InitFun#{ return => {tuple, []},
-                                         body   => {builtin, set_state, [InitBody]} } }
+            Funs1 = Funs#{ InitName => InitFun#{ return => {tuple, []},
+                                                 body   => builtin_to_fcode(state_layout(Env), set_state, [InitBody]) } },
+            Funs1
    end.

 add_default_init_function(_Env, Main, StateType, Funs) ->
@@ -992,12 +1094,10 @@ event_function(_Env = #{event_type := {variant_t, EventCons}}, EventType = {vari
 %% the top-level and replace it with a closure.

 -spec lambda_lift(fcode()) -> fcode().
-lambda_lift(FCode = #{ functions := Funs }) ->
-    init_fresh_names(),
+lambda_lift(FCode = #{ functions := Funs, state_layout := StateLayout }) ->
    init_lambda_funs(),
-    Funs1   = maps:map(fun lambda_lift_fun/2, Funs),
+    Funs1   = maps:map(fun(_, Body) -> lambda_lift_fun(StateLayout, Body) end, Funs),
    NewFuns = get_lambda_funs(),
-    clear_fresh_names(),
    FCode#{ functions := maps:merge(Funs1, NewFuns) }.

 -define(lambda_key, '%lambdalifted').
@@ -1010,8 +1110,8 @@ add_lambda_fun(Def) ->
    put(?lambda_key, Funs#{ Name => Def }),
    Name.

-lambda_lift_fun(_, Def = #{ body := Body }) ->
-    Def#{ body := lambda_lift_expr(Body) }.
+lambda_lift_fun(Layout, Def = #{ body := Body }) ->
+    Def#{ body := lambda_lift_expr(Layout, Body) }.

 lifted_fun([Z], Xs, Body) ->
    #{ attrs  => [private],
@@ -1032,10 +1132,10 @@ make_closure(FVs, Xs, Body) ->
    Tup = fun([Y]) -> Y; (Ys) -> {tuple, Ys} end,
    {closure, Fun, Tup([{var, Y} || Y <- FVs])}.

-lambda_lift_expr({lam, Xs, Body}) ->
+lambda_lift_expr(Layout, {lam, Xs, Body}) ->
    FVs   = free_vars({lam, Xs, Body}),
-    make_closure(FVs, Xs, lambda_lift_expr(Body));
-lambda_lift_expr(UExpr) when element(1, UExpr) == def_u; element(1, UExpr) == builtin_u ->
+    make_closure(FVs, Xs, lambda_lift_expr(Layout, Body));
+lambda_lift_expr(Layout, UExpr) when element(1, UExpr) == def_u; element(1, UExpr) == builtin_u ->
    [Tag, F, Ar | _] = tuple_to_list(UExpr),
    ExtraArgs = case UExpr of
                    {builtin_u, _, _, TypeArgs} -> TypeArgs;
@@ -1044,40 +1144,42 @@ lambda_lift_expr(UExpr) when element(1, UExpr) == def_u; element(1, UExpr) == bu
    Xs   = [ lists:concat(["arg", I]) || I <- lists:seq(1, Ar) ],
    Args = [{var, X} || X <- Xs] ++ ExtraArgs,
    Body = case Tag of
-               builtin_u -> builtin_to_fcode(F, Args);
+               builtin_u -> builtin_to_fcode(Layout, F, Args);
               def_u     -> {def, F, Args}
           end,
    make_closure([], Xs, Body);
-lambda_lift_expr({remote_u, ArgsT, RetT, Ct, F}) ->
+lambda_lift_expr(Layout, {remote_u, ArgsT, RetT, Ct, F}) ->
    FVs  = free_vars(Ct),
-    Ct1  = lambda_lift_expr(Ct),
+    Ct1  = lambda_lift_expr(Layout, Ct),
    GasAndValueArgs = 2,
    Xs   = [ lists:concat(["arg", I]) || I <- lists:seq(1, length(ArgsT) + GasAndValueArgs) ],
    Args = [{var, X} || X <- Xs],
    make_closure(FVs, Xs, {remote, ArgsT, RetT, Ct1, F, Args});
-lambda_lift_expr(Expr) ->
+lambda_lift_expr(Layout, Expr) ->
    case Expr of
        {lit, _}               -> Expr;
        nil                    -> Expr;
        {var, _}               -> Expr;
        {closure, _, _}        -> Expr;
-        {def, D, As}           -> {def, D, lambda_lift_exprs(As)};
-        {builtin, B, As}       -> {builtin, B, lambda_lift_exprs(As)};
-        {remote, ArgsT, RetT, Ct, F, As} -> {remote, ArgsT, RetT, lambda_lift_expr(Ct), F, lambda_lift_exprs(As)};
-        {con, Ar, C, As}       -> {con, Ar, C, lambda_lift_exprs(As)};
-        {tuple, As}            -> {tuple, lambda_lift_exprs(As)};
-        {proj, A, I}           -> {proj, lambda_lift_expr(A), I};
-        {set_proj, A, I, B}    -> {set_proj, lambda_lift_expr(A), I, lambda_lift_expr(B)};
-        {op, Op, As}           -> {op, Op, lambda_lift_exprs(As)};
-        {'let', X, A, B}       -> {'let', X, lambda_lift_expr(A), lambda_lift_expr(B)};
-        {funcall, A, Bs}       -> {funcall, lambda_lift_expr(A), lambda_lift_exprs(Bs)};
-        {switch, S}            -> {switch, lambda_lift_expr(S)};
-        {split, Type, X, Alts} -> {split, Type, X, lambda_lift_exprs(Alts)};
-        {nosplit, A}           -> {nosplit, lambda_lift_expr(A)};
-        {'case', P, S}         -> {'case', P, lambda_lift_expr(S)}
+        {def, D, As}           -> {def, D, lambda_lift_exprs(Layout, As)};
+        {builtin, B, As}       -> {builtin, B, lambda_lift_exprs(Layout, As)};
+        {remote, ArgsT, RetT, Ct, F, As} -> {remote, ArgsT, RetT, lambda_lift_expr(Layout, Ct), F, lambda_lift_exprs(Layout, As)};
+        {con, Ar, C, As}       -> {con, Ar, C, lambda_lift_exprs(Layout, As)};
+        {tuple, As}            -> {tuple, lambda_lift_exprs(Layout, As)};
+        {proj, A, I}           -> {proj, lambda_lift_expr(Layout, A), I};
+        {set_proj, A, I, B}    -> {set_proj, lambda_lift_expr(Layout, A), I, lambda_lift_expr(Layout, B)};
+        {op, Op, As}           -> {op, Op, lambda_lift_exprs(Layout, As)};
+        {'let', X, A, B}       -> {'let', X, lambda_lift_expr(Layout, A), lambda_lift_expr(Layout, B)};
+        {funcall, A, Bs}       -> {funcall, lambda_lift_expr(Layout, A), lambda_lift_exprs(Layout, Bs)};
+        {set_state, R, A}      -> {set_state, R, lambda_lift_expr(Layout, A)};
+        {get_state, _}         -> Expr;
+        {switch, S}            -> {switch, lambda_lift_expr(Layout, S)};
+        {split, Type, X, Alts} -> {split, Type, X, lambda_lift_exprs(Layout, Alts)};
+        {nosplit, A}           -> {nosplit, lambda_lift_expr(Layout, A)};
+        {'case', P, S}         -> {'case', P, lambda_lift_expr(Layout, S)}
    end.

-lambda_lift_exprs(As) -> [lambda_lift_expr(A) || A <- As].
+lambda_lift_exprs(Layout, As) -> [lambda_lift_expr(Layout, A) || A <- As].

 %% -- Optimisations ----------------------------------------------------------

@@ -1095,7 +1197,12 @@ optimize_fcode(Code = #{ functions := Funs }) ->
 -spec optimize_fun(fcode(), fun_name(), fun_def()) -> fun_def().
 optimize_fun(Fcode, Fun, Def = #{ body := Body }) ->
    %% io:format("Optimizing ~p =\n~s\n", [_Fun, prettypr:format(pp_fexpr(_Body))]),
-    Def#{ body := inliner(Fcode, Fun, Body) }.
+    Def#{ body := drop_unused_lets(
+                  simplifier(
+                  let_floating(
+                  bind_subexpressions(
+                  inline_local_functions(
+                  inliner(Fcode, Fun, Body)))))) }.

 %% --- Inlining ---

@@ -1111,6 +1218,276 @@ should_inline(_Fcode, _Fun1) -> false == list_to_atom("true").  %% Dialyzer

 inline(_Fcode, Fun, Args) -> {def, Fun, Args}. %% TODO

+%% --- Bind subexpressions ---
+
+-define(make_lets(Xs, Es, Body), make_lets(Es, fun(Xs) -> Body end)).
+
+bind_subexpressions(Expr) ->
+    bottom_up(fun bind_subexpressions/2, Expr).
+
+bind_subexpressions(_, {tuple, Es}) ->
+    ?make_lets(Xs, Es, {tuple, Xs});
+bind_subexpressions(_, {set_proj, A, I, B}) ->
+    ?make_lets([X, Y], [A, B], {set_proj, X, I, Y});
+bind_subexpressions(_, E) -> E.
+
+make_lets(Es, Body) -> make_lets(Es, [], Body).
+
+make_lets([], Xs, Body)       -> Body(lists:reverse(Xs));
+make_lets([{var, _} = E | Es], Xs, Body) ->
+    make_lets(Es, [E | Xs], Body);
+make_lets([{lit, _} = E | Es], Xs, Body) ->
+    make_lets(Es, [E | Xs], Body);
+make_lets([E | Es], Xs, Body) ->
+    ?make_let(X, E, make_lets(Es, [X | Xs], Body)).
+
+%% --- Inline local functions ---
+
+inline_local_functions(Expr) ->
+    bottom_up(fun inline_local_functions/2, Expr).
+
+inline_local_functions(Env, {funcall, {proj, {var, Y}, 0}, [{proj, {var, Y}, 1} | Args]} = Expr) ->
+    %% TODO: Don't always inline local funs?
+    case maps:get(Y, Env, free) of
+        {lam, Xs, Body} -> let_bind(lists:zip(Xs, Args), Body);
+        _               -> Expr
+    end;
+inline_local_functions(_, Expr) -> Expr.
+
+%% --- Let-floating ---
+
+let_floating(Expr) -> bottom_up(fun let_float/2, Expr).
+
+let_float(_, {'let', X, E, Body}) ->
+    pull_out_let({'let', X, {here, E}, Body});
+let_float(_, {proj, E, I}) ->
+    pull_out_let({proj, {here, E}, I});
+let_float(_, {set_proj, E, I, V}) ->
+    pull_out_let({set_proj, {here, E}, I, {here, V}});
+let_float(_, {op, Op, Es}) ->
+    {Lets, Es1} = pull_out_let([{here, E} || E <- Es]),
+    let_bind(Lets, {op, Op, Es1});
+let_float(_, E) -> E.
+
+pull_out_let(Expr) when is_tuple(Expr) ->
+    {Lets, Es} = pull_out_let(tuple_to_list(Expr)),
+    Inner = list_to_tuple(Es),
+    let_bind(Lets, Inner);
+pull_out_let(Es) when is_list(Es) ->
+    case lists:splitwith(fun({here, _}) -> false; (_) -> true end, Es) of
+        {Es0, [{here, E} | Es1]} ->
+            case let_view(E) of
+                {[], _}    ->
+                    {Lets, Es2} = pull_out_let(Es1),
+                    {Lets, Es0 ++ [E] ++ Es2};
+                {Lets, E1} ->
+                    {Lets1, Es2} = pull_out_let(Es1),
+                    {Lets ++ Lets1, Es0 ++ [E1] ++ Es2}
+            end;
+        {_, []} -> {[], Es}
+    end.
+
+%% Also renames the variables to fresh names
+let_view(E) -> let_view(E, [], []).
+
+let_view({'let', X, E, Rest}, Ren, Lets) ->
+    Z = fresh_name(),
+    let_view(Rest, [{X, Z} | Ren], [{Z, rename(Ren, E)} | Lets]);
+let_view(E, Ren, Lets) ->
+    {lists:reverse(Lets), rename(Ren, E)}.
+
+%% --- Simplification ---
+
+-spec simplifier(fexpr()) -> fexpr().
+simplifier(Expr) ->
+    bottom_up(fun simplify/2, Expr).
+
+-spec simplify(#{var_name() => fexpr()}, fexpr()) -> fexpr().
+
+%% (e₀, .., en).i ->
+%% let _ = e₀ in .. let x = ei in .. let _ = en in x
+simplify(_Env, {proj, {tuple, Es}, I}) ->
+    It  = lists:nth(I + 1, Es),
+    X   = fresh_name(),
+    Dup = safe_to_duplicate(It),
+    Val = if Dup -> It; true -> {var, X} end,
+    lists:foldr(
+      fun({J, E}, Rest) when I == J ->
+            case Dup of
+                true  -> Rest;
+                false -> {'let', X, E, Rest}
+            end;
+         ({_, E}, Rest) ->
+            case read_only(E) of
+                true  -> Rest;
+                false -> {'let', "_", E, Rest}
+            end
+        end, Val, indexed(Es));
+
+%% let x = e in .. x.i ..
+simplify(Env, {proj, {var, X}, I} = Expr) ->
+    case simpl_proj(Env, I, {var, X}) of
+        false -> Expr;
+        E     -> E
+    end;
+
+simplify(Env, {switch, Split}) ->
+    case simpl_switch(Env, [], Split) of
+        nomatch -> {builtin, abort, [{lit, {string, <<"Incomplete patterns">>}}]};
+        stuck   -> {switch, Split};
+        Expr    -> Expr
+    end;
+
+simplify(_, E) ->
+    E.
+
+simpl_proj(Env, I, Expr) ->
+    IfSafe = fun(E) -> case safe_to_duplicate(E) of
+                         true -> E;
+                         false -> false
+                       end end,
+    case Expr of
+        false                 -> false;
+        {var, X}              -> simpl_proj(Env, I, maps:get(X, Env, false));
+        {tuple, Es}           -> IfSafe(lists:nth(I + 1, Es));
+        {set_proj, _, I, Val} -> IfSafe(Val);
+        {set_proj, E, _, _}   -> simpl_proj(Env, I, E);
+        {proj, E, J}          -> simpl_proj(Env, I, simpl_proj(Env, J, E));
+        _                     -> false
+    end.
+
+get_catchalls(Alts) ->
+    [ C || C = {'case', {var, _}, _} <- Alts ].
+
+%% The scode compiler can't handle multiple catch-alls, so we need to nest them
+%% inside each other. Instead of
+%%    _ => switch(x) ..
+%%    _ => e
+%% we do
+%%    _ => switch(x)
+%%           ..
+%%           _ => e
+add_catchalls(Alts, []) -> Alts;
+add_catchalls(Alts, Catchalls) ->
+    case lists:splitwith(fun({'case', {var, _}, _}) -> false; (_) -> true end,
+                         Alts) of
+        {Alts1, [C]} -> Alts1 ++ [nest_catchalls([C | Catchalls])];
+        {_, []}      -> Alts  ++ [nest_catchalls(Catchalls)]
+        %% NOTE: relies on catchalls always being at the end
+    end.
+
+nest_catchalls([C = {'case', {var, _}, {nosplit, _}} | _]) -> C;
+nest_catchalls([{'case', P = {var, _}, {split, Type, X, Alts}} | Catchalls]) ->
+    {'case', P, {split, Type, X, add_catchalls(Alts, Catchalls)}}.
+
+simpl_switch(_Env, _, {nosplit, E}) -> E;
+simpl_switch(Env, Catchalls, {split, Type, X, Alts}) ->
+    Alts1 = add_catchalls(Alts, Catchalls),
+    Stuck = {switch, {split, Type, X, Alts1}},
+    case constructor_form(Env, {var, X}) of
+        false -> Stuck;
+        E     ->
+            case simpl_case(Env, E, Alts1) of
+                stuck -> Stuck;
+                Res   -> Res
+            end
+    end.
+
+simpl_case(_, _, []) -> nomatch;
+simpl_case(Env, E, [{'case', Pat, Body} | Alts]) ->
+    case match_pat(Pat, E) of
+        false -> simpl_case(Env, E, Alts);
+        Binds ->
+            Env1 = maps:merge(Env, maps:from_list(Binds)),
+            case simpl_switch(Env1, get_catchalls(Alts), Body) of
+                nomatch -> simpl_case(Env, E, Alts);
+                stuck   -> stuck;
+                Body1   -> let_bind(Binds, Body1)
+            end
+    end.
+
+-spec match_pat(fsplit_pat(), fexpr()) -> false | [{var_name(), fexpr()}].
+match_pat({tuple, Xs}, {tuple, Es})         -> lists:zip(Xs, Es);
+match_pat({con, _, C, Xs}, {con, _, C, Es}) -> lists:zip(Xs, Es);
+match_pat(L, {lit, L})                      -> [];
+match_pat(nil, nil)                         -> [];
+match_pat({'::', X, Y}, {op, '::', [A, B]}) -> [{X, A}, {Y, B}];
+match_pat({var, X}, E)                      -> [{X, E}];
+match_pat(_, _)                             -> false.
+
+constructor_form(Env, Expr) ->
+    case Expr of
+        {var, X} ->
+            case maps:get(X, Env, free) of
+                free -> false;
+                E    -> constructor_form(Env, E)    %% TODO: shadowing?
+            end;
+        {set_proj, E, I, V} ->
+            case constructor_form(Env, E) of
+                {tuple, Es} -> {tuple, setnth(I + 1, V, Es)};
+                _           -> false
+            end;
+        {proj, E, I} ->
+            case constructor_form(Env, E) of
+                {tuple, Es} -> constructor_form(Env, lists:nth(I + 1, Es));
+                _           -> false
+            end;
+        {con, _, _, _} -> Expr;
+        {tuple, _}     -> Expr;
+        {lit, _}       -> Expr;
+        nil            -> Expr;
+        {op, '::', _}  -> Expr;
+        _              -> false
+    end.
+
+%% --- Drop unused lets ---
+
+drop_unused_lets(Expr) -> bottom_up(fun drop_unused_lets/2, Expr).
+
+drop_unused_lets(_, {'let', X, E, Body} = Expr) ->
+    case {read_only(E), not lists:member(X, free_vars(Body))} of
+        {true, true}  -> Body;
+        {false, true} -> {'let', "_", E, Body};
+        _             -> Expr
+    end;
+drop_unused_lets(_, Expr) -> Expr.
+
+%% -- Static analysis --------------------------------------------------------
+
+safe_to_duplicate({lit, _})    -> true;
+safe_to_duplicate({var, _})    -> true;
+safe_to_duplicate(nil)         -> true;
+safe_to_duplicate({tuple, []}) -> true;
+safe_to_duplicate(_)           -> false.
+
+-spec read_only(fexpr() | fsplit() | fcase() | [fexpr()] | [fcase()]) -> boolean().
+read_only({lit, _})                -> true;
+read_only({var, _})                -> true;
+read_only(nil)                     -> true;
+read_only({con, _, _, Es})         -> read_only(Es);
+read_only({tuple, Es})             -> read_only(Es);
+read_only({proj, E, _})            -> read_only(E);
+read_only({set_proj, A, _, B})     -> read_only([A, B]);
+read_only({op, _, Es})             -> read_only(Es);
+read_only({get_state, _})          -> true;
+read_only({set_state, _, _})       -> false;
+read_only({def_u, _, _})           -> true;
+read_only({remote_u, _, _, _, _})  -> true;
+read_only({builtin_u, _, _})       -> true;
+read_only({builtin_u, _, _, _})    -> true;
+read_only({lam, _, _})             -> true;
+read_only({def, _, _})             -> false; %% TODO: purity analysis
+read_only({remote, _, _, _, _, _}) -> false;
+read_only({builtin, _, _})         -> false; %% TODO: some builtins are
+read_only({switch, Split})         -> read_only(Split);
+read_only({split, _, _, Cases})    -> read_only(Cases);
+read_only({nosplit, E})            -> read_only(E);
+read_only({'case', _, Split})      -> read_only(Split);
+read_only({'let', _, A, B})        -> read_only([A, B]);
+read_only({funcall, _, _})         -> false;
+read_only({closure, _, _})         -> internal_error(no_closures_here);
+read_only(Es) when is_list(Es)     -> lists:all(fun read_only/1, Es).
+
 %% --- Deadcode elimination ---

 -spec eliminate_dead_code(fcode()) -> fcode().
@@ -1232,10 +1609,10 @@ resolve_var(#{ vars := Vars } = Env, [X]) ->
    end;
 resolve_var(Env, Q) -> resolve_fun(Env, Q).

-resolve_fun(#{ fun_env := Funs, builtins := Builtin }, Q) ->
+resolve_fun(#{ fun_env := Funs, builtins := Builtin } = Env, Q) ->
    case {maps:get(Q, Funs, not_found), maps:get(Q, Builtin, not_found)} of
        {not_found, not_found} -> internal_error({unbound_variable, Q});
-        {_, {B, none}}         -> {builtin, B, []};
+        {_, {B, none}}         -> builtin_to_fcode(state_layout(Env), B, []);
        {_, {B, Ar}}           -> {builtin_u, B, Ar};
        {{Fun, Ar}, _}         -> {def_u, Fun, Ar}
    end.
@@ -1270,14 +1647,14 @@ pat_vars({con, _, _, Ps})     -> pat_vars(Ps);
 pat_vars(Ps) when is_list(Ps) -> [X || P <- Ps, X <- pat_vars(P)].

 -spec fsplit_pat_vars(fsplit_pat()) -> [var_name()].
-fsplit_pat_vars({var, X})            -> [X || X /= "_"];
-fsplit_pat_vars({bool, _})           -> [];
-fsplit_pat_vars({int, _})            -> [];
-fsplit_pat_vars({string, _})         -> [];
-fsplit_pat_vars(nil)                 -> [];
-fsplit_pat_vars({'::', P, Q})        -> [P, Q];
-fsplit_pat_vars({tuple, Ps})         -> Ps;
-fsplit_pat_vars({con, _, _, Ps})     -> Ps.
+fsplit_pat_vars({var, X})        -> [X || X /= "_"];
+fsplit_pat_vars({bool, _})       -> [];
+fsplit_pat_vars({int, _})        -> [];
+fsplit_pat_vars({string, _})     -> [];
+fsplit_pat_vars(nil)             -> [];
+fsplit_pat_vars({'::', P, Q})    -> [P, Q];
+fsplit_pat_vars({tuple, Ps})     -> Ps;
+fsplit_pat_vars({con, _, _, Ps}) -> Ps.

 free_vars(Xs) when is_list(Xs) ->
    lists:umerge([ free_vars(X) || X <- Xs ]);
@@ -1300,6 +1677,8 @@ free_vars(Expr) ->
        {op, _, As}          -> free_vars(As);
        {'let', X, A, B}     -> free_vars([A, {lam, [X], B}]);
        {funcall, A, Bs}     -> free_vars([A | Bs]);
+        {set_state, _, A}    -> free_vars(A);
+        {get_state, _}       -> [];
        {lam, Xs, B}         -> free_vars(B) -- lists:sort(Xs);
        {closure, _, A}      -> free_vars(A);
        {switch, A}          -> free_vars(A);
@@ -1329,6 +1708,8 @@ used_defs(Expr) ->
        {op, _, As}          -> used_defs(As);
        {'let', _, A, B}     -> used_defs([A, B]);
        {funcall, A, Bs}     -> used_defs([A | Bs]);
+        {set_state, _, A}    -> used_defs(A);
+        {get_state, _}       -> [];
        {lam, _, B}          -> used_defs(B);
        {closure, F, A}      -> lists:umerge([F], used_defs(A));
        {switch, A}          -> used_defs(A);
@@ -1337,6 +1718,50 @@ used_defs(Expr) ->
        {'case', _, A}       -> used_defs(A)
    end.

+bottom_up(F, Expr) -> bottom_up(F, #{}, Expr).
+
+bottom_up(F, Env, Expr) ->
+    F(Env, case Expr of
+        {lit, _}                         -> Expr;
+        nil                              -> Expr;
+        {var, _}                         -> Expr;
+        {def, D, Es}                     -> {def, D, [bottom_up(F, Env, E) || E <- Es]};
+        {def_u, _, _}                    -> Expr;
+        {builtin, B, Es}                 -> {builtin, B, [bottom_up(F, Env, E) || E <- Es]};
+        {builtin_u, _, _}                -> Expr;
+        {builtin_u, _, _, _}             -> Expr;
+        {remote, ArgsT, RetT, Ct, Fun, Es} -> {remote,   ArgsT, RetT, bottom_up(F, Env, Ct), Fun, [bottom_up(F, Env, E) || E <- Es]};
+        {remote_u, ArgsT, RetT, Ct, Fun}   -> {remote_u, ArgsT, RetT, bottom_up(F, Env, Ct), Fun};
+        {con, Ar, I, Es}                 -> {con, Ar, I, [bottom_up(F, Env, E) || E <- Es]};
+        {tuple, Es}                      -> {tuple, [bottom_up(F, Env, E) || E <- Es]};
+        {proj, E, I}                     -> {proj, bottom_up(F, Env, E), I};
+        {set_proj, R, I, E}              -> {set_proj, bottom_up(F, Env, R), I, bottom_up(F, Env, E)};
+        {op, Op, Es}                     -> {op, Op, [bottom_up(F, Env, E) || E <- Es]};
+        {funcall, Fun, Es}               -> {funcall, bottom_up(F, Env, Fun), [bottom_up(F, Env, E) || E <- Es]};
+        {set_state, R, E}                -> {set_state, R, bottom_up(F, Env, E)};
+        {get_state, _}                   -> Expr;
+        {closure, F, CEnv}               -> {closure, F, bottom_up(F, Env, CEnv)};
+        {switch, Split}                  -> {switch, bottom_up(F, Env, Split)};
+        {lam, Xs, B}                     -> {lam, Xs, bottom_up(F, Env, B)};
+        {'let', X, E, Body}              ->
+            E1 = bottom_up(F, Env, E),
+            %% Always freshen user variables to avoid shadowing issues.
+            ShouldFreshen = fun(Y = "%" ++ _) -> maps:is_key(Y, Env);
+                               (_)            -> true end,
+            case ShouldFreshen(X) of
+                true ->
+                    Z = fresh_name(),
+                    Env1 = Env#{ Z => E1 },
+                    {'let', Z, E1, bottom_up(F, Env1, rename([{X, Z}], Body))};
+                false ->
+                    Env1 = Env#{ X => E1 },
+                    {'let', X, E1, bottom_up(F, Env1, Body)}
+            end;
+        {split, Type, X, Cases}          -> {split, Type, X, [bottom_up(F, Env, Case) || Case <- Cases]};
+        {nosplit, E}                     -> {nosplit, bottom_up(F, Env, E)};
+        {'case', Pat, Split}             -> {'case', Pat, bottom_up(F, Env, Split)}
+    end).
+
 get_named_args(NamedArgsT, Args) ->
    IsNamed = fun({named_arg, _, _, _}) -> true;
                 (_) -> false end,
@@ -1371,6 +1796,8 @@ rename(Ren, Expr) ->
        {set_proj, R, I, E}   -> {set_proj, rename(Ren, R), I, rename(Ren, E)};
        {op, Op, Es}          -> {op, Op, [rename(Ren, E) || E <- Es]};
        {funcall, Fun, Es}    -> {funcall, rename(Ren, Fun), [rename(Ren, E) || E <- Es]};
+        {set_state, R, E}     -> {set_state, R, rename(Ren, E)};
+        {get_state, _}        -> Expr;
        {closure, F, Env}     -> {closure, F, rename(Ren, Env)};
        {switch, Split}       -> {switch, rename_split(Ren, Split)};
        {lam, Xs, B} ->
@@ -1477,6 +1904,10 @@ get_attributes(Ann) ->
 indexed(Xs) ->
    lists:zip(lists:seq(1, length(Xs)), Xs).

+setnth(I, X, Xs) ->
+    {Ys, [_ | Zs]} = lists:split(I - 1, Xs),
+    Ys ++ [X] ++ Zs.
+
 -dialyzer({nowarn_function, [fcode_error/1, internal_error/1]}).

 fcode_error(Error) ->
@@ -1579,9 +2010,18 @@ pp_fexpr({op, Op, [A] = Args}) ->
    end;
 pp_fexpr({op, Op, As}) ->
    pp_beside(pp_text(Op), pp_fexpr({tuple, As}));
-pp_fexpr({'let', X, A, B}) ->
-    pp_par([pp_beside([pp_text("let "), pp_text(X), pp_text(" = "), pp_fexpr(A), pp_text(" in")]),
-            pp_fexpr(B)]);
+pp_fexpr({'let', _, _, _} = Expr) ->
+    Lets = fun Lets({'let', Y, C, D}) ->
+                        {Ls, E} = Lets(D),
+                        {[{Y, C} | Ls], E};
+               Lets(E) -> {[], E} end,
+    {Ls, Body} = Lets(Expr),
+    pp_parens(
+      pp_par(
+        [ pp_beside([ pp_text("let "),
+                      pp_above([ pp_par([pp_text(X), pp_text("="), prettypr:nest(2, pp_fexpr(A))]) || {X, A} <- Ls ]),
+                      pp_text(" in ") ]),
+          pp_fexpr(Body) ]));
 pp_fexpr({builtin_u, B, N}) ->
    pp_beside([pp_text(B), pp_text("/"), pp_text(N)]);
 pp_fexpr({builtin_u, B, N, TypeArgs}) ->
@@ -1594,6 +2034,10 @@ pp_fexpr({remote, ArgsT, RetT, Ct, Fun, As}) ->
    pp_call(pp_parens(pp_beside([pp_fexpr(Ct), pp_text("."), pp_fun_name(Fun), pp_text(" : "), pp_ftype({function, ArgsT, RetT})])), As);
 pp_fexpr({funcall, Fun, As}) ->
    pp_call(pp_fexpr(Fun), As);
+pp_fexpr({set_state, R, A}) ->
+    pp_call(pp_text("set_state"), [{lit, {int, R}}, A]);
+pp_fexpr({get_state, R}) ->
+    pp_call(pp_text("get_state"), [{lit, {int, R}}]);
 pp_fexpr({switch, Split}) -> pp_split(Split).

 pp_call(Fun, Args) ->
@@ -1609,7 +2053,7 @@ pp_ftype({tvar, X}) -> pp_text(X);
 pp_ftype({bytes, N}) -> pp_call(pp_text("bytes"), [{lit, {int, N}}]);
 pp_ftype({oracle, Q, R}) -> pp_call_t("oracle", [Q, R]);
 pp_ftype({tuple, Ts}) ->
-    pp_parens(pp_par(pp_punctuate(pp_text(","), [pp_ftype(T) || T <- Ts])));
+    pp_parens(pp_par(pp_punctuate(pp_text(" *"), [pp_ftype(T) || T <- Ts])));
 pp_ftype({list, T}) ->
    pp_call_t("list", [T]);
 pp_ftype({function, Args, Res}) ->
@@ -131,7 +131,7 @@ contract_to_icode([Decl | Code], Icode) ->
 ast_id({id, _, Id}) -> Id;
 ast_id({qid, _, Id}) -> Id.

-ast_args([{arg, _, Name, Type}|Rest], Acc, Icode) ->
+ast_args([{typed, _, Name, Type}|Rest], Acc, Icode) ->
    ast_args(Rest, [{ast_id(Name), ast_typerep1(Type, Icode)}| Acc], Icode);
 ast_args([], Acc, _Icode) -> lists:reverse(Acc).

@@ -318,19 +318,23 @@ ast_body({app, As, Fun, Args}, Icode) ->
    end;
 ast_body({list_comp, _, Yield, []}, Icode) ->
    #list{elems = [ast_body(Yield, Icode)]};
-ast_body({list_comp, As, Yield, [{comprehension_bind, {typed, Arg, ArgType}, BindExpr}|Rest]}, Icode) ->
+ast_body({list_comp, As, Yield, [{comprehension_bind, {typed, _, Pat, ArgType}, BindExpr}|Rest]}, Icode) ->
+    Arg  = "%lc",
+    Body = {switch, As, {typed, As, {id, As, Arg}, ArgType},
+                [{'case', As, Pat, {list_comp, As, Yield, Rest}},
+                 {'case', As, {id, As, "_"}, {list, As, []}}]},
    #funcall
        { function = #var_ref{ name = ["ListInternal", "flat_map"] }
        , args =
-              [ #lambda{ args=[#arg{name = ast_id(Arg), type = ast_type(ArgType, Icode)}]
-                       , body = ast_body({list_comp, As, Yield, Rest}, Icode)
+              [ #lambda{ args=[#arg{name = Arg, type = ast_type(ArgType, Icode)}]
+                       , body = ast_body(Body, Icode)
                       }
              , ast_body(BindExpr, Icode)
              ]
        };
 ast_body({list_comp, As, Yield, [{comprehension_if, AsIF, Cond}|Rest]}, Icode) ->
    ast_body({'if', AsIF, Cond, {list_comp, As, Yield, Rest}, {list, As, []}}, Icode);
-ast_body({list_comp, As, Yield, [LV = {letval, _, _, _, _}|Rest]}, Icode) ->
+ast_body({list_comp, As, Yield, [LV = {letval, _, _, _}|Rest]}, Icode) ->
    ast_body({block, As, [LV, {list_comp, As, Yield, Rest}]}, Icode);
 ast_body({list_comp, As, Yield, [LF = {letfun, _, _, _, _, _}|Rest]}, Icode) ->
    ast_body({block, As, [LF, {list_comp, As, Yield, Rest}]}, Icode);
@@ -344,14 +348,16 @@ ast_body({switch,_,A,Cases}, Icode) ->
    #switch{expr=ast_body(A, Icode),
            cases=[{ast_body(Pat, Icode),ast_body(Body, Icode)}
              || {'case',_,Pat,Body} <- Cases]};
-ast_body({block, As, [{letval, _, Pat, _, E} | Rest]}, Icode) ->
+ast_body({block, As, [{letval, _, Pat, E} | Rest]}, Icode) ->
    E1    = ast_body(E, Icode),
    Pat1  = ast_body(Pat, Icode),
    Rest1 = ast_body({block, As, Rest}, Icode),
    #switch{expr  = E1,
            cases = [{Pat1, Rest1}]};
 ast_body({block, As, [{letfun, Ann, F, Args, _Type, Expr} | Rest]}, Icode) ->
-    ast_body({block, As, [{letval, Ann, F, unused, {lam, Ann, Args, Expr}} | Rest]}, Icode);
+    ToArg   = fun({typed, Ann1, Id, T}) -> {arg, Ann1, Id, T} end,    %% Pattern matching has been desugared
+    LamArgs = lists:map(ToArg, Args),
+    ast_body({block, As, [{letval, Ann, F, {lam, Ann, LamArgs, Expr}} | Rest]}, Icode);
 ast_body({block,_,[]}, _Icode) ->
    #tuple{cpts=[]};
 ast_body({block,_,[E]}, Icode) ->
@@ -800,10 +806,10 @@ check_entrypoint_type(Ann, Name, Args, Ret) ->
                    true  -> ok
                end end,
    [ CheckFirstOrder(T, {invalid_entrypoint, higher_order, Ann1, Name, {argument, X, T}})
-      || {arg, Ann1, X, T} <- Args ],
+      || {typed, Ann1, X, T} <- Args ],
    CheckFirstOrder(Ret, {invalid_entrypoint, higher_order, Ann, Name, {result, Ret}}),
    [ CheckMonomorphic(T, {invalid_entrypoint, polymorphic, Ann1, Name, {argument, X, T}})
-      || {arg, Ann1, X, T} <- Args ],
+      || {typed, Ann1, X, T} <- Args ],
    CheckMonomorphic(Ret, {invalid_entrypoint, polymorphic, Ann, Name, {result, Ret}}).

 check_oracle_type(Ann, Type = ?oracle_t(QType, RType)) ->
@@ -38,6 +38,7 @@
                | pp_assembler
                | pp_bytecode
                | no_code
+		  | keep_included
                | {backend, aevm | fate}
                | {include, {file_system, [string()]} |
                            {explicit_files, #{string() => binary()}}}
@@ -336,12 +337,12 @@ to_sophia_value(ContractString, FunName, ok, Data, Options0) ->
                try
                    {ok, aeso_vm_decode:from_fate(Type, aeb_fate_encoding:deserialize(Data))}
                catch throw:cannot_translate_to_sophia ->
-                        Type1 = prettypr:format(aeso_pretty:type(Type)),
+                        Type1 = prettypr:format(aeso_pretty:type(Type0)),
                        Msg = io_lib:format("Cannot translate FATE value ~p\n  of Sophia type ~s\n",
                                            [aeb_fate_encoding:deserialize(Data), Type1]),
                        {error, [aeso_errors:new(data_error, Msg)]};
                      _:_ ->
-                        Type1 = prettypr:format(aeso_pretty:type(Type)),
+                        Type1 = prettypr:format(aeso_pretty:type(Type0)),
                        Msg = io_lib:format("Failed to decode binary as type ~s\n", [Type1]),
                        {error, [aeso_errors:new(data_error, Msg)]}
               end
@@ -389,8 +390,8 @@ decode_calldata(ContractString, FunName, Calldata, Options0) ->
        #{ typed_ast := TypedAst, type_env  := TypeEnv} = Code,

        {ok, Args, _} = get_decode_type(FunName, TypedAst),
-        DropArg       = fun({arg, _, _, T}) -> T; (T) -> T end,
-        ArgTypes      = lists:map(DropArg, Args),
+        GetType       = fun({typed, _, _, T}) -> T; (T) -> T end,
+        ArgTypes      = lists:map(GetType, Args),
        Type0         = {tuple_t, [], ArgTypes},
        %% user defined data types such as variants needed to match against
        Type          = aeso_ast_infer_types:unfold_types_in_type(TypeEnv, Type0, [unfold_record_types, unfold_variant_types]),
@@ -650,8 +651,9 @@ pp_fate_type(T) -> io_lib:format("~w", [T]).

 %% -------------------------------------------------------------------

+-spec sophia_type_to_typerep(string()) -> {error, bad_type} | {ok, aeb_aevm_data:type()}.
 sophia_type_to_typerep(String) ->
-    {ok, Ast} = aeso_parser:type(String),
+    Ast = aeso_parser:run_parser(aeso_parser:type(), String),
    try aeso_ast_to_icode:ast_typerep(Ast) of
        Type -> {ok, Type}
    catch _:_ -> {error, bad_type}
@@ -41,8 +41,8 @@
 -define(TODO(What), error({todo, ?FILE, ?LINE, ?FUNCTION_NAME, What})).

 -define(i(X), {immediate, X}).
-define(a, {stack, 0}).
-define(s, {store, 1}).
+-define(a,    {stack, 0}).
+-define(s(N), {store, N}).
 -define(void, {var, 9999}).

 -record(env, { contract, vars = [], locals = [], current_function, tailpos = true }).
@@ -120,9 +120,10 @@ type_to_scode(name)            -> name;
 type_to_scode(channel)         -> channel;
 type_to_scode(bits)            -> bits;
 type_to_scode(any)             -> any;
-type_to_scode({variant, Cons}) -> {variant, lists:map(fun(T) -> type_to_scode({tuple, T}) end, Cons)};
+type_to_scode({variant, Cons}) -> {variant, [{tuple, types_to_scode(Con)} || Con <- Cons]};
 type_to_scode({list, Type})    -> {list, type_to_scode(Type)};
-type_to_scode({tuple, Types})  -> {tuple, lists:map(fun type_to_scode/1, Types)};
+type_to_scode({tuple, [Type]}) -> type_to_scode(Type);
+type_to_scode({tuple, Types})  -> {tuple, types_to_scode(Types)};
 type_to_scode({map, Key, Val}) -> {map, type_to_scode(Key), type_to_scode(Val)};
 type_to_scode({function, _Args, _Res}) -> {tuple, [string, any]};
 type_to_scode({tvar, X}) ->
@@ -134,6 +135,8 @@ type_to_scode({tvar, X}) ->
        J -> {tvar, J}
    end.

+types_to_scode(Ts) -> lists:map(fun type_to_scode/1, Ts).
+
 %% -- Phase I ----------------------------------------------------------------
 %%  Icode to structured assembly

@@ -179,84 +182,99 @@ lit_to_fate(L) ->
        {typerep, T}         -> aeb_fate_data:make_typerep(type_to_scode(T))
     end.

-term_to_fate({lit, L}) ->
+term_to_fate(E) -> term_to_fate(#{}, E).
+
+term_to_fate(_Env, {lit, L}) ->
    lit_to_fate(L);
 %% negative literals are parsed as 0 - N
-term_to_fate({op, '-', [{lit, {int, 0}}, {lit, {int, N}}]}) ->
+term_to_fate(_Env, {op, '-', [{lit, {int, 0}}, {lit, {int, N}}]}) ->
    aeb_fate_data:make_integer(-N);
-term_to_fate(nil) ->
+term_to_fate(_Env, nil) ->
    aeb_fate_data:make_list([]);
-term_to_fate({op, '::', [Hd, Tl]}) ->
+term_to_fate(Env, {op, '::', [Hd, Tl]}) ->
    %% The Tl will translate into a list, because FATE lists are just lists
-    [term_to_fate(Hd) | term_to_fate(Tl)];
-term_to_fate({tuple, As}) ->
-    aeb_fate_data:make_tuple(list_to_tuple([ term_to_fate(A) || A<-As]));
-term_to_fate({con, Ar, I, As}) ->
-    FateAs = [ term_to_fate(A) || A <- As ],
+    [term_to_fate(Env, Hd) | term_to_fate(Env, Tl)];
+term_to_fate(Env, {tuple, As}) ->
+    aeb_fate_data:make_tuple(list_to_tuple([ term_to_fate(Env, A) || A<-As]));
+term_to_fate(Env, {con, Ar, I, As}) ->
+    FateAs = [ term_to_fate(Env, A) || A <- As ],
    aeb_fate_data:make_variant(Ar, I, list_to_tuple(FateAs));
-term_to_fate({builtin, bits_all, []}) ->
+term_to_fate(_Env, {builtin, bits_all, []}) ->
    aeb_fate_data:make_bits(-1);
-term_to_fate({builtin, bits_none, []}) ->
+term_to_fate(_Env, {builtin, bits_none, []}) ->
    aeb_fate_data:make_bits(0);
-term_to_fate({op, bits_set, [B, I]}) ->
+term_to_fate(_Env, {op, bits_set, [B, I]}) ->
    {bits, N} = term_to_fate(B),
    J         = term_to_fate(I),
    {bits, N bor (1 bsl J)};
-term_to_fate({op, bits_clear, [B, I]}) ->
+term_to_fate(_Env, {op, bits_clear, [B, I]}) ->
    {bits, N} = term_to_fate(B),
    J         = term_to_fate(I),
    {bits, N band bnot (1 bsl J)};
-term_to_fate({builtin, map_empty, []}) ->
+term_to_fate(Env, {'let', X, E, Body}) ->
+    Env1 = Env#{ X => term_to_fate(Env, E) },
+    term_to_fate(Env1, Body);
+term_to_fate(Env, {var, X}) ->
+    case maps:get(X, Env, undefined) of
+        undefined -> throw(not_a_fate_value);
+        V         -> V
+    end;
+term_to_fate(_Env, {builtin, map_empty, []}) ->
    aeb_fate_data:make_map(#{});
-term_to_fate({'let', _, {builtin, map_empty, []}, Set}) ->
-    aeb_fate_data:make_map(map_to_fate(Set)).
+term_to_fate(Env, {op, map_set, [M, K, V]}) ->
+    Map = term_to_fate(Env, M),
+    Map#{term_to_fate(Env, K) => term_to_fate(Env, V)};
+term_to_fate(_Env, _) ->
+    throw(not_a_fate_value).

-map_to_fate({op, map_set, [{var, _}, K, V]}) ->
-    #{term_to_fate(K) => term_to_fate(V)};
-map_to_fate({op, map_set, [Set, K, V]}) ->
-    Map = map_to_fate(Set), Map#{term_to_fate(K) => term_to_fate(V)}.
+to_scode(Env, T) ->
+    try term_to_fate(T) of
+        V -> [push(?i(V))]
+    catch throw:not_a_fate_value ->
+        to_scode1(Env, T)
+    end.

-to_scode(_Env, {lit, L}) ->
+to_scode1(_Env, {lit, L}) ->
    [push(?i(lit_to_fate(L)))];

-to_scode(_Env, nil) ->
+to_scode1(_Env, nil) ->
    [aeb_fate_ops:nil(?a)];

-to_scode(Env, {var, X}) ->
+to_scode1(Env, {var, X}) ->
    [push(lookup_var(Env, X))];

-to_scode(Env, {con, Ar, I, As}) ->
+to_scode1(Env, {con, Ar, I, As}) ->
    N = length(As),
    [[to_scode(notail(Env), A) || A <- As],
     aeb_fate_ops:variant(?a, ?i(Ar), ?i(I), ?i(N))];

-to_scode(Env, {tuple, As}) ->
+to_scode1(Env, {tuple, As}) ->
    N = length(As),
    [[ to_scode(notail(Env), A) || A <- As ],
     tuple(N)];

-to_scode(Env, {proj, E, I}) ->
+to_scode1(Env, {proj, E, I}) ->
    [to_scode(notail(Env), E),
     aeb_fate_ops:element_op(?a, ?i(I), ?a)];

-to_scode(Env, {set_proj, R, I, E}) ->
+to_scode1(Env, {set_proj, R, I, E}) ->
    [to_scode(notail(Env), E),
     to_scode(notail(Env), R),
     aeb_fate_ops:setelement(?a, ?i(I), ?a, ?a)];

-to_scode(Env, {op, Op, Args}) ->
+to_scode1(Env, {op, Op, Args}) ->
    call_to_scode(Env, op_to_scode(Op), Args);

-to_scode(Env, {'let', X, {var, Y}, Body}) ->
+to_scode1(Env, {'let', X, {var, Y}, Body}) ->
    Env1 = bind_var(X, lookup_var(Env, Y), Env),
    to_scode(Env1, Body);
-to_scode(Env, {'let', X, Expr, Body}) ->
+to_scode1(Env, {'let', X, Expr, Body}) ->
    {I, Env1} = bind_local(X, Env),
    [ to_scode(notail(Env), Expr),
      aeb_fate_ops:store({var, I}, {stack, 0}),
      to_scode(Env1, Body) ];

-to_scode(Env = #env{ current_function = Fun, tailpos = true }, {def, Fun, Args}) ->
+to_scode1(Env = #env{ current_function = Fun, tailpos = true }, {def, Fun, Args}) ->
    %% Tail-call to current function, f(e0..en). Compile to
    %%      [ let xi = ei ]
    %%      [ STORE argi xi ]
@@ -274,17 +292,17 @@ to_scode(Env = #env{ current_function = Fun, tailpos = true }, {def, Fun, Args})
        || {I, J} <- lists:zip(lists:seq(0, length(Vars) - 1),
                               lists:reverse(Vars)) ],
      loop ];
-to_scode(Env, {def, Fun, Args}) ->
+to_scode1(Env, {def, Fun, Args}) ->
    FName = make_function_id(Fun),
    Lbl   = aeb_fate_data:make_string(FName),
    call_to_scode(Env, local_call(Env, ?i(Lbl)), Args);
-to_scode(Env, {funcall, Fun, Args}) ->
+to_scode1(Env, {funcall, Fun, Args}) ->
    call_to_scode(Env, [to_scode(Env, Fun), local_call(Env, ?a)], Args);

-to_scode(Env, {builtin, B, Args}) ->
+to_scode1(Env, {builtin, B, Args}) ->
    builtin_to_scode(Env, B, Args);

-to_scode(Env, {remote, ArgsT, RetT, Ct, Fun, [Gas, Value | Args]}) ->
+to_scode1(Env, {remote, ArgsT, RetT, Ct, Fun, [Gas, Value | Args]}) ->
    Lbl = make_function_id(Fun),
    {ArgTypes, RetType0} = typesig_to_scode([{"_", T} || T <- ArgsT], RetT),
    ArgType = ?i(aeb_fate_data:make_typerep({tuple, ArgTypes})),
@@ -298,10 +316,16 @@ to_scode(Env, {remote, ArgsT, RetT, Ct, Fun, [Gas, Value | Args]}) ->
            call_to_scode(Env, Call, [Ct, Value, Gas | Args])
    end;

-to_scode(Env, {closure, Fun, FVs}) ->
+to_scode1(_Env, {get_state, Reg}) ->
+    [push(?s(Reg))];
+to_scode1(Env, {set_state, Reg, Val}) ->
+    call_to_scode(Env, [{'STORE', ?s(Reg), ?a},
+                        tuple(0)], [Val]);
+
+to_scode1(Env, {closure, Fun, FVs}) ->
    to_scode(Env, {tuple, [{lit, {string, make_function_id(Fun)}}, FVs]});

-to_scode(Env, {switch, Case}) ->
+to_scode1(Env, {switch, Case}) ->
    split_to_scode(Env, Case).

 local_call( Env, Fun) when Env#env.tailpos -> aeb_fate_ops:call_t(Fun);
@@ -420,11 +444,6 @@ call_to_scode(Env, CallCode, Args) ->
    [[to_scode(notail(Env), A) || A <- lists:reverse(Args)],
     CallCode].

-builtin_to_scode(_Env, get_state, []) ->
-    [push(?s)];
-builtin_to_scode(Env, set_state, [_] = Args) ->
-    call_to_scode(Env, [{'STORE', ?s, ?a},
-                        tuple(0)], Args);
 builtin_to_scode(Env, chain_event, Args) ->
    call_to_scode(Env, [erlang:apply(aeb_fate_ops, log, lists:duplicate(length(Args), ?a)),
                        tuple(0)], Args);
@@ -645,11 +664,11 @@ pp_op(loop) -> "LOOP";
 pp_op(I)    ->
    aeb_fate_pp:format_op(I, #{}).

-pp_arg(?i(I))      -> io_lib:format("~w", [I]);
-pp_arg({arg, N})   -> io_lib:format("arg~p", [N]);
-pp_arg({store, N}) -> io_lib:format("store~p", [N]);
-pp_arg({var, N})   -> io_lib:format("var~p", [N]);
-pp_arg(?a)         -> "a".
+pp_arg(?i(I))    -> io_lib:format("~w", [I]);
+pp_arg({arg, N}) -> io_lib:format("arg~p", [N]);
+pp_arg(?s(N))    -> io_lib:format("store~p", [N]);
+pp_arg({var, N}) -> io_lib:format("var~p", [N]);
+pp_arg(?a)       -> "a".

 %% -- Analysis --

@@ -1368,7 +1387,7 @@ desugar_args(I) when is_tuple(I) ->
    list_to_tuple([Op | lists:map(fun desugar_arg/1, Args)]);
 desugar_args(I) -> I.

-desugar_arg({store, N}) -> {var, -N};
+desugar_arg(?s(N)) -> {var, -N};
 desugar_arg(A) -> A.

 %% -- Phase III --------------------------------------------------------------
@@ -1578,6 +1597,7 @@ tweak_returns(['RETURN', {'PUSH', A} | Code])          -> [{'RETURNR', A} | Code
 tweak_returns(['RETURN' | Code = [{'CALL_T', _} | _]]) -> Code;
 tweak_returns(['RETURN' | Code = [{'ABORT', _} | _]])  -> Code;
 tweak_returns(['RETURN' | Code = [{'EXIT', _} | _]])   -> Code;
+tweak_returns(['RETURN' | Code = [loop | _]])          -> Code;
 tweak_returns(Code) -> Code.

 %% -- Split basic blocks at CALL instructions --
@@ -1591,8 +1611,7 @@ split_calls(Ref, [], Acc, Blocks) ->
 split_calls(Ref, [I | Code], Acc, Blocks) when element(1, I) == 'CALL';
                                               element(1, I) == 'CALL_R';
                                               element(1, I) == 'CALL_GR';
-                                               element(1, I) == 'jumpif';
-                                               I == loop ->
+                                               element(1, I) == 'jumpif' ->
    split_calls(make_ref(), Code, [], [{Ref, lists:reverse([I | Acc])} | Blocks]);
 split_calls(Ref, [{'ABORT', _} = I | _Code], Acc, Blocks) ->
    lists:reverse([{Ref, lists:reverse([I | Acc])} | Blocks]);
@@ -3,20 +3,33 @@
 %%% Description :
 %%% Created     : 1 Mar 2018 by Ulf Norell
 -module(aeso_parser).
+-compile({no_auto_import,[map_get/2]}).

 -export([string/1,
         string/2,
         string/3,
+         auto_imports/1,
         hash_include/2,
-         type/1]).
+         decl/0,
+         type/0,
+         body/0,
+         maybe_block/1,
+         run_parser/2,
+         run_parser/3]).

 -include("aeso_parse_lib.hrl").
 -import(aeso_parse_lib, [current_file/0, set_current_file/1]).

-type parse_result() :: aeso_syntax:ast() | none().
+-type parse_result() :: aeso_syntax:ast() | {aeso_syntax:ast(), sets:set(include_hash())} | none().

 -type include_hash() :: {string(), binary()}.

+
+escape_errors({ok, Ok}) ->
+    Ok;
+escape_errors({error, Err}) ->
+    parse_error(Err).
+
 -spec string(string()) -> parse_result().
 string(String) ->
    string(String, sets:new(), []).
@@ -30,21 +43,17 @@ string(String, Opts) ->

 -spec string(string(), sets:set(include_hash()), aeso_compiler:options()) -> parse_result().
 string(String, Included, Opts) ->
-    case parse_and_scan(file(), String, Opts) of
-        {ok, AST} ->
-            case expand_includes(AST, Included, Opts) of
-                {ok, AST1}   -> AST1;
-                {error, Err} -> parse_error(Err)
-            end;
-        {error, Err} ->
-            parse_error(Err)
+    AST = run_parser(file(), String, Opts),
+    case expand_includes(AST, Included, Opts) of
+        {ok, AST1}   -> AST1;
+        {error, Err} -> parse_error(Err)
    end.

-type(String) ->
-    case parse_and_scan(type(), String, []) of
-        {ok, AST}    -> {ok, AST};
-        {error, Err} -> {error, [mk_error(Err)]}
-    end.
+
+run_parser(P, Inp) ->
+    escape_errors(parse_and_scan(P, Inp, [])).
+run_parser(P, Inp, Opts) ->
+    escape_errors(parse_and_scan(P, Inp, Opts)).

 parse_and_scan(P, S, Opts) ->
    set_current_file(proplists:get_value(src_file, Opts, no_file)),
@@ -101,11 +110,19 @@ decl() ->
    , ?RULE(keyword(datatype), id(), type_vars(), tok('='), typedef(variant), {type_def, _1, _2, _3, _5})

      %% Function declarations
-    , ?RULE(modifiers(), fun_or_entry(), id(), tok(':'), type(), add_modifiers(_1, _2, {fun_decl, get_ann(_2), _3, _5}))
-    , ?RULE(modifiers(), fun_or_entry(), fundef(),               add_modifiers(_1, _2, set_pos(get_pos(get_ann(_2)), _3)))
-    , ?RULE(keyword('let'),    valdef(),                         set_pos(get_pos(_1), _2))
+    , ?RULE(modifiers(), fun_or_entry(), maybe_block(fundef_or_decl()), fun_block(_1, _2, _3))
+    , ?RULE(keyword('let'), valdef(), set_pos(get_pos(_1), _2))
    ])).

+fun_block(Mods, Kind, [Decl]) ->
+    add_modifiers(Mods, Kind, set_pos(get_pos(Kind), Decl));
+fun_block(Mods, Kind, Decls) ->
+    {block, get_ann(Kind), [ add_modifiers(Mods, Kind, Decl) || Decl <- Decls ]}.
+
+fundef_or_decl() ->
+    choice([?RULE(id(), tok(':'), type(), {fun_decl, get_ann(_1), _1, _3}),
+            fundef()]).
+
 pragma() ->
    Op = choice([token(T) || T <- ['<', '=<', '==', '>=', '>']]),
    ?RULE(tok('@'), id("compiler"), Op, version(), {pragma, get_ann(_1), {compiler, element(1, _3), _4}}).
@@ -117,7 +134,7 @@ mk_version({int, _, Maj}, Rest) ->
    [Maj | [N || {_, {int, _, N}} <- Rest]].

 fun_or_entry() ->
-    choice([?RULE(keyword(function), {function, _1}),
+    choice([?RULE(keyword(function),   {function,   _1}),
            ?RULE(keyword(entrypoint), {entrypoint, _1})]).

 modifiers() ->
@@ -164,20 +181,19 @@ letdecl() ->
 letdef() -> choice(valdef(), fundef()).

 valdef() ->
-    choice(
-        ?RULE(id(),                   tok('='), body(), {letval, [], _1, type_wildcard(), _3}),
-        ?RULE(id(), tok(':'), type(), tok('='), body(), {letval, [], _1, _3, _5})).
+    ?RULE(pattern(), tok('='), body(), {letval, [], _1, _3}).

 fundef() ->
    choice(
-    [ ?RULE(id(), args(),                   tok('='), body(), {letfun, [], _1, _2, type_wildcard(), _4})
-    , ?RULE(id(), args(), tok(':'), type(), tok('='), body(), {letfun, [], _1, _2, _4, _6})
+    [ ?RULE(id(), args(),                   tok('='), body(), {letfun, get_ann(_1), _1, _2, type_wildcard(get_ann(_1)), _4})
+    , ?RULE(id(), args(), tok(':'), type(), tok('='), body(), {letfun, get_ann(_1), _1, _2, _4, _6})
    ]).

-args() -> paren_list(arg()).
+args() -> paren_list(pattern()).
+lam_args() -> paren_list(arg()).

 arg() -> choice(
-    ?RULE(id(),                   {arg, get_ann(_1), _1, type_wildcard()}),
+    ?RULE(id(),                   {arg, get_ann(_1), _1, type_wildcard(get_ann(_1))}),
    ?RULE(id(), tok(':'), type(), {arg, get_ann(_1), _1, _3})).

 %% -- Types ------------------------------------------------------------------
@@ -238,7 +254,7 @@ branch() ->
    ?RULE(pattern(), keyword('=>'), body(), {'case', _2, _1, _3}).

 pattern() ->
-    ?LET_P(E, expr500(), parse_pattern(E)).
+    ?LET_P(E, expr(), parse_pattern(E)).

 %% -- Expressions ------------------------------------------------------------

@@ -248,7 +264,7 @@ expr100() ->
    Expr100 = ?LAZY_P(expr100()),
    Expr200 = ?LAZY_P(expr200()),
    choice(
-    [ ?RULE(args(), keyword('=>'), body(), {lam, _2, _1, _3})   %% TODO: better location
+    [ ?RULE(lam_args(), keyword('=>'), body(), {lam, _2, _1, _3})   %% TODO: better location
    , {'if', keyword('if'), parens(Expr100), Expr200, right(tok(else), Expr100)}
    , ?RULE(Expr200, optional(right(tok(':'), type())),
            case _2 of
@@ -297,7 +313,7 @@ comprehension_if() ->
    ?RULE(keyword('if'), parens(expr()), {comprehension_if, _1, _2}).

 comprehension_bind() ->
-    ?RULE(id(), tok('<-'), expr(), {comprehension_bind, _1, _3}).
+    ?RULE(pattern(), tok('<-'), expr(), {comprehension_bind, _1, _3}).

 arg_expr() ->
    ?LAZY_P(
@@ -349,7 +365,9 @@ record(Fs) ->
                        bad_expr_err("Cannot use '@' in map construction", infix({lvalue, FAnn, LV}, {'@', Ann}, Id));
                    ({field, FAnn, LV, _}) ->
                        bad_expr_err("Cannot use nested fields or keys in map construction", {lvalue, FAnn, LV}) end,
-            {map, Ann, lists:map(KV, Fs)}
+            {map, Ann, lists:map(KV, Fs)};
+        record_or_map_error ->
+            {record_or_map_error, get_ann(hd(Fs)), Fs}
    end.

 record_or_map(Fields) ->
@@ -361,9 +379,7 @@ record_or_map(Fields) ->
    case lists:usort(lists:map(Kind, Fields)) of
        [proj]    -> record;
        [map_get] -> map;
-        _         ->
-            [{field, Ann, _, _} | _] = Fields,
-            bad_expr_err("Mixed record fields and map keys in", {record, Ann, Fields})
+        _         -> record_or_map_error %% Defer error until type checking
    end.

 field_assignment() ->
@@ -494,8 +510,8 @@ infix(L, Op, R) -> set_ann(format, infix,  {app, get_ann(L), Op, [L, R]}).
 prefixes(Ops, E) -> lists:foldr(fun prefix/2, E, Ops).
 prefix(Op, E)    -> set_ann(format, prefix, {app, get_ann(Op), Op, [E]}).

-type_wildcard() ->
-    {id, [{origin, system}], "_"}.
+type_wildcard(Ann) ->
+    {id, [{origin, system} | Ann], "_"}.

 block_e(Stmts) ->
    group_ifs(Stmts, []).
@@ -545,7 +561,9 @@ list_comp_e(Ann, Expr, Binds) -> {list_comp, Ann, Expr, Binds}.
 -spec parse_pattern(aeso_syntax:expr()) -> aeso_parse_lib:parser(aeso_syntax:pat()).
 parse_pattern({app, Ann, Con = {'::', _}, Es}) ->
    {app, Ann, Con, lists:map(fun parse_pattern/1, Es)};
-parse_pattern({app, Ann, Con = {con, _, _}, Es}) ->
+parse_pattern({app, Ann, {'-', _}, [{int, _, N}]}) ->
+    {int, Ann, -N};
+parse_pattern({app, Ann, Con = {Tag, _, _}, Es}) when Tag == con; Tag == qcon ->
    {app, Ann, Con, lists:map(fun parse_pattern/1, Es)};
 parse_pattern({tuple, Ann, Es}) ->
    {tuple, Ann, lists:map(fun parse_pattern/1, Es)};
@@ -553,7 +571,10 @@ parse_pattern({list, Ann, Es}) ->
    {list, Ann, lists:map(fun parse_pattern/1, Es)};
 parse_pattern({record, Ann, Fs}) ->
    {record, Ann, lists:map(fun parse_field_pattern/1, Fs)};
+parse_pattern({typed, Ann, E, Type}) ->
+    {typed, Ann, parse_pattern(E), Type};
 parse_pattern(E = {con, _, _})    -> E;
+parse_pattern(E = {qcon, _, _})   -> E;
 parse_pattern(E = {id, _, _})     -> E;
 parse_pattern(E = {int, _, _})    -> E;
 parse_pattern(E = {bool, _, _})   -> E;
@@ -584,8 +605,13 @@ expand_includes(AST, Included, Opts) ->
             || File <- lists:usort(auto_imports(AST)) ] ++ AST,
    expand_includes(AST1, Included, [], Opts).

-expand_includes([], _Included, Acc, _Opts) ->
-    {ok, lists:reverse(Acc)};
+expand_includes([], Included, Acc, Opts) ->
+    case lists:member(keep_included, Opts) of
+        false ->
+            {ok, lists:reverse(Acc)};
+        true ->
+            {ok, {lists:reverse(Acc), Included}}
+    end;
 expand_includes([{include, Ann, {string, _SAnn, File}} | AST], Included, Acc, Opts) ->
    case get_include_code(File, Ann, Opts) of
        {ok, Code} ->
@@ -644,8 +670,14 @@ stdlib_options() ->

 get_include_code(File, Ann, Opts) ->
    case {read_file(File, Opts), read_file(File, stdlib_options())} of
-        {{ok, _}, {ok,_ }} ->
-            fail(ann_pos(Ann), "Illegal redefinition of standard library " ++ File);
+        {{ok, Bin}, {ok, _}} ->
+            case filename:basename(File) == File of
+                true -> { error
+                        , fail( ann_pos(Ann)
+                              , "Illegal redefinition of standard library " ++ binary_to_list(File))};
+                %% If a path is provided then the stdlib takes lower priority
+                false -> {ok, binary_to_list(Bin)}
+            end;
        {_, {ok, Bin}} ->
            {ok, binary_to_list(Bin)};
        {{ok, Bin}, _} ->
@@ -145,8 +145,12 @@ decl(D, Options) ->
    with_options(Options, fun() -> decl(D) end).

 -spec decl(aeso_syntax:decl()) -> doc().
-decl({contract, _, C, Ds}) ->
-    block(follow(text("contract"), hsep(name(C), text("="))), decls(Ds));
+decl({contract, Attrs, C, Ds}) ->
+    Mod = fun({Mod, true}) when Mod == payable ->
+                  text(atom_to_list(Mod));
+             (_) -> empty() end,
+    block(follow( hsep(lists:map(Mod, Attrs) ++ [text("contract")])
+                , hsep(name(C), text("="))), decls(Ds));
 decl({namespace, _, C, Ds}) ->
    block(follow(text("namespace"), hsep(name(C), text("="))), decls(Ds));
 decl({pragma, _, Pragma}) -> pragma(Pragma);
@@ -155,13 +159,16 @@ decl({type_def, _, T, Vars, Def}) ->
    Kind = element(1, Def),
    equals(typedecl(Kind, T, Vars), typedef(Def));
 decl({fun_decl, Ann, F, T}) ->
+    Mod = fun({Mod, true}) when Mod == private; Mod == stateful; Mod == payable ->
+                  text(atom_to_list(Mod));
+             (_) -> empty() end,
    Fun = case aeso_syntax:get_ann(entrypoint, Ann, false) of
            true  -> text("entrypoint");
            false -> text("function")
          end,
-    hsep(Fun, typed(name(F), T));
+    hsep(lists:map(Mod, Ann) ++ [Fun, typed(name(F), T)]);
 decl(D = {letfun, Attrs, _, _, _, _}) ->
-    Mod = fun({Mod, true}) when Mod == private; Mod == stateful ->
+    Mod = fun({Mod, true}) when Mod == private; Mod == stateful; Mod == payable ->
                            text(atom_to_list(Mod));
             (_) -> empty() end,
    Fun = case aeso_syntax:get_ann(entrypoint, Attrs, false) of
@@ -169,7 +176,11 @@ decl(D = {letfun, Attrs, _, _, _, _}) ->
              false -> "function"
          end,
    hsep(lists:map(Mod, Attrs) ++ [letdecl(Fun, D)]);
-decl(D = {letval, _, _, _, _}) -> letdecl("let", D).
+decl({fun_clauses, Ann, Name, Type, Clauses}) ->
+    above([ decl(D) || D <- [{fun_decl, Ann, Name, Type} | Clauses] ]);
+decl(D = {letval, _, _, _}) -> letdecl("let", D);
+decl({block, _, Ds}) ->
+    above([ decl(D) || D <- Ds ]).

 -spec pragma(aeso_syntax:pragma()) -> doc().
 pragma({compiler, Op, Ver}) ->
@@ -193,10 +204,10 @@ name({tvar, _, Name})  -> text(Name);
 name({typed, _, Name, _}) -> name(Name).

 -spec letdecl(string(), aeso_syntax:letbind()) -> doc().
-letdecl(Let, {letval, _, F, T, E}) ->
-    block_expr(0, hsep([text(Let), typed(name(F), T), text("=")]), E);
+letdecl(Let, {letval, _, P, E}) ->
+    block_expr(0, hsep([text(Let), expr(P), text("=")]), E);
 letdecl(Let, {letfun, _, F, Args, T, E}) ->
-    block_expr(0, hsep([text(Let), typed(beside(name(F), args(Args)), T), text("=")]), E).
+    block_expr(0, hsep([text(Let), typed(beside(name(F), expr({tuple, [], Args})), T), text("=")]), E).

 -spec args([aeso_syntax:arg()]) -> doc().
 args(Args) ->
@@ -305,6 +316,8 @@ expr_p(_, {tuple, _, Es}) ->
    tuple(lists:map(fun expr/1, Es));
 expr_p(_, {list, _, Es}) ->
    list(lists:map(fun expr/1, Es));
+expr_p(_, {list_comp, _, E, Binds}) ->
+    list([follow(expr(E), hsep(text("|"), par(punctuate(text(","), lists:map(fun lc_bind/1, Binds)), 0)), 0)]);
 expr_p(_, {record, _, Fs}) ->
    record(lists:map(fun field/1, Fs));
 expr_p(_, {map, Ann, KVs}) ->
@@ -358,7 +371,8 @@ expr_p(_, {Type, _, Bin})
         Type == oracle_query_id ->
    text(binary_to_list(aeser_api_encoder:encode(Type, Bin)));
 expr_p(_, {string, _, <<>>}) -> text("\"\"");
-expr_p(_, {string, _, S}) -> term(binary_to_list(S));
+expr_p(_, {string, _, S}) ->
+    text(io_lib:format("\"~s\"", [binary_to_list(S)]));
 expr_p(_, {char, _, C}) ->
    case C of
        $' -> text("'\\''");
@@ -387,6 +401,13 @@ stmt_p({else, Else}) ->
        _ -> block_expr(200, text("else"), Else)
    end.

+lc_bind({comprehension_bind, P, E}) ->
+    follow(hsep(expr(P), text("<-")), expr(E));
+lc_bind({comprehension_if, _, E}) ->
+    beside([text("if("), expr(E), text(")")]);
+lc_bind(Let) ->
+    letdecl("let", Let).
+
 -spec bin_prec(aeso_syntax:bin_op()) -> {integer(), integer(), integer()}.
 bin_prec('..')   -> {  0,   0,   0};  %% Always printed inside '[ ]'
 bin_prec('=')    -> {  0,   0,   0};  %% Always printed inside '[ ]'
@@ -450,7 +471,7 @@ elim1(Get={map_get, _, _})    -> elim(Get);
 elim1(Get={map_get, _, _, _}) -> elim(Get).

 alt({'case', _, Pat, Body}) ->
-    block_expr(0, hsep(expr_p(500, Pat), text("=>")), Body).
+    block_expr(0, hsep(expr(Pat), text("=>")), Body).

 block_expr(_, Header, {block, _, Ss}) ->
    block(Header, statements(Ss));
@@ -460,7 +481,7 @@ block_expr(P, Header, E) ->
 statements(Stmts) ->
    above([ statement(S) || S <- Stmts ]).

-statement(S = {letval, _, _, _, _})    -> letdecl("let", S);
+statement(S = {letval, _, _, _})       -> letdecl("let", S);
 statement(S = {letfun, _, _, _, _, _}) -> letdecl("let", S);
 statement(E) -> expr(E).

@@ -473,6 +494,3 @@ get_elifs(If = {'if', Ann, Cond, Then, Else}, Elifs) ->
    end;
 get_elifs(Else, Elifs) -> {lists:reverse(Elifs), {else, Else}}.

-fmt(Fmt, Args) -> text(lists:flatten(io_lib:format(Fmt, Args))).
-term(X) -> fmt("~p", [X]).
-
@@ -37,18 +37,24 @@
 -type decl() :: {contract, ann(), con(), [decl()]}
              | {namespace, ann(), con(), [decl()]}
              | {pragma, ann(), pragma()}
-              | {type_decl, ann(), id(), [tvar()]}
+              | {type_decl, ann(), id(), [tvar()]} % Only for error msgs
              | {type_def, ann(), id(), [tvar()], typedef()}
              | {fun_decl, ann(), id(), type()}
-              | letbind().
+              | {fun_clauses, ann(), id(), type(), [letbind()]}
+              | {block, ann(), [decl()]}
+              | letfun()
+              | letval(). % Only for error msgs

 -type compiler_version() :: [non_neg_integer()].

 -type pragma() :: {compiler, '==' | '<' | '>' | '=<' | '>=', compiler_version()}.

+
+-type letval() :: {letval, ann(), pat(), expr()}.
+-type letfun() :: {letfun, ann(), id(), [pat()], type(), expr()}.
 -type letbind()
-    :: {letval, ann(), id(), type(), expr()}
-     | {letfun, ann(), id(), [arg()], type(), expr()}.
+    :: letfun()
+     | letval().

 -type arg() :: {arg, ann(), id(), type()}.

@@ -100,9 +106,8 @@
     | {list, ann(), [expr()]}
     | {list_comp, ann(), expr(), [comprehension_exp()]}
     | {typed, ann(), expr(), type()}
-     | {record, ann(), [field(expr())]}
-     | {record, ann(), expr(), [field(expr())]} %% record update
-     | {map, ann(), expr(), [field(expr())]}    %% map update
+     | {record_or_map(), ann(), [field(expr())]}
+     | {record_or_map(), ann(), expr(), [field(expr())]} %% record/map update
     | {map, ann(), [{expr(), expr()}]}
     | {map_get, ann(), expr(), expr()}
     | {map_get, ann(), expr(), expr(), expr()}
@@ -111,7 +116,9 @@
     | id() | qid() | con() | qcon()
     | constant().

-type comprehension_exp() :: [ {comprehension_bind, id(), expr()}
+-type record_or_map() :: record | map | record_or_map_error.
+
+-type comprehension_exp() :: [ {comprehension_bind, pat(), expr()}
                             | {comprehension_if, ann(), expr()}
                             | letbind() ].

@@ -139,6 +146,7 @@
 -type pat() :: {app, ann(), con() | op(), [pat()]}
             | {tuple, ann(), [pat()]}
             | {list, ann(), [pat()]}
+             | {typed, ann(), pat(), type()}
             | {record, ann(), [field(pat())]}
             | constant()
             | con()
@@ -45,11 +45,11 @@ fold(Alg = #alg{zero = Zero, plus = Plus, scoped = Scoped}, Fun, K, X) ->
            %% decl()
            {contract, _, _, Ds}     -> Decl(Ds);
            {namespace, _, _, Ds}    -> Decl(Ds);
-            {type_decl, _, I, _}     -> BindType(I);
            {type_def, _, I, _, D}   -> Plus(BindType(I), Decl(D));
            {fun_decl, _, _, T}      -> Type(T);
-            {letval, _, F, T, E}     -> Sum([BindExpr(F), Type(T), Expr(E)]);
+            {letval, _, P, E}        -> Scoped(BindExpr(P), Expr(E));
            {letfun, _, F, Xs, T, E} -> Sum([BindExpr(F), Type(T), Expr(Xs ++ [E])]);
+            {fun_clauses, _, _, T, Cs} -> Sum([Type(T) | [Decl(C) || C <- Cs]]);
            %% typedef()
            {alias_t, T}    -> Type(T);
            {record_t, Fs}  -> Type(Fs);
@@ -76,8 +76,8 @@ fold(Alg = #alg{zero = Zero, plus = Plus, scoped = Scoped}, Fun, K, X) ->
                Plus(Expr(E), Scoped(BindExpr(I), Expr({list_comp, A, Y, R})));
            {list_comp, A, Y, [{comprehension_if, _, E}|R]} ->
                Plus(Expr(E), Expr({list_comp, A, Y, R}));
-            {list_comp, A, Y, [D = {letval, _, F, _, _} | R]} ->
-                Plus(Decl(D), Scoped(BindExpr(F), Expr({list_comp, A, Y, R})));
+            {list_comp, A, Y, [D = {letval, _, Pat, _} | R]} ->
+                Plus(Decl(D), Scoped(BindExpr(Pat), Expr({list_comp, A, Y, R})));
            {list_comp, A, Y, [D = {letfun, _, F, _, _, _} | R]} ->
                Plus(Decl(D), Scoped(BindExpr(F), Expr({list_comp, A, Y, R})));
            {typed, _, E, T}       -> Plus(Expr(E), Type(T));
@@ -1,6 +1,6 @@
 {application, aesophia,
 [{description, "Contract Language for aeternity"},
-  {vsn, "4.1.0-rc1"},
+  {vsn, "4.3.0"},
  {registered, []},
  {applications,
   [kernel,
@@ -106,7 +106,7 @@ aci_test_contract(Name) ->
    ok.

 check_stub(Stub, Options) ->
-    case aeso_parser:string(binary_to_list(Stub), Options) of
+    try aeso_parser:string(binary_to_list(Stub), Options) of
        Ast ->
            try
                %% io:format("AST: ~120p\n", [Ast]),
@@ -117,9 +117,9 @@ check_stub(Stub, Options) ->
                  _:R ->
                io:format("Error: ~p\n", [R]),
                error(R)
-            end;
-        {error, E} ->
-            io:format("Error: ~p\n", [E]),
-            error({parse_error, E})
+            end
+    catch throw:{error, Errs} ->
+        _ = [ io:format("~s\n", [aeso_errors:pp(E)]) || E <- Errs ],
+        error({parse_errors, Errs})
    end.

@@ -138,6 +138,7 @@ compilable_contracts() ->
     "test",
     "builtin_bug",
     "builtin_map_get_bug",
+     "lc_record_bug",
     "nodeadcode",
     "deadcode",
     "variant_types",
@@ -161,7 +162,10 @@ compilable_contracts() ->
     "list_comp",
     "payable",
     "unapplied_builtins",
-     "underscore_number_literals"
+     "underscore_number_literals",
+     "qualified_constructor",
+     "let_patterns",
+     "lhs_matching"
    ].

 not_yet_compilable(fate) -> [];
@@ -296,9 +300,22 @@ failing_contracts() ->
          "Repeated name x in pattern\n"
          "  x :: x (at line 26, column 7)">>,
        <<?Pos(44, 14)
-          "Repeated argument x to function repeated_arg (at line 44, column 14).">>,
-        <<?Pos(44, 14)
-          "Repeated argument y to function repeated_arg (at line 44, column 14).">>,
+          "Repeated names x, y in pattern\n"
+          "  (x : int, y, x : string, y : bool) (at line 44, column 14)">>,
+        <<?Pos(44, 39)
+          "Cannot unify int\n"
+          "         and string\n"
+          "when checking the type of the expression at line 44, column 39\n"
+          "  x : int\n"
+          "against the expected type\n"
+          "  string">>,
+        <<?Pos(44, 72)
+          "Cannot unify int\n"
+          "         and string\n"
+          "when checking the type of the expression at line 44, column 72\n"
+          "  x : int\n"
+          "against the expected type\n"
+          "  string">>,
        <<?Pos(14, 24)
          "No record type with fields y, z (at line 14, column 24)">>,
        <<?Pos(15, 26)
@@ -358,79 +375,17 @@ failing_contracts() ->
           "  r.foo : (gas : int, value : int) => Remote.themap\n"
           "against the expected type\n"
           "  (gas : int, value : int) => map(string, int)">>])
-    , ?TYPE_ERROR(bad_include_and_ns,
-        [<<?Pos(2, 11)
-           "Include of 'included.aes' at line 2, column 11\nnot allowed, include only allowed at top level.">>,
-         <<?Pos(3, 13)
-           "Nested namespace not allowed\nNamespace 'Foo' at line 3, column 13 not defined at top level.">>])
+    , ?TYPE_ERROR(not_toplevel_include,
+                  [<<?Pos(2, 11)
+                     "Include of 'included.aes' at line 2, column 11\nnot allowed, include only allowed at top level.">>])
+    , ?TYPE_ERROR(not_toplevel_namespace,
+                  [<<?Pos(2, 13)
+                     "Nested namespaces are not allowed\nNamespace 'Foo' at line 2, column 13 not defined at top level.">>])
+    , ?TYPE_ERROR(not_toplevel_contract,
+        [<<?Pos(2, 12)
+           "Nested contracts are not allowed\nContract 'Con' at line 2, column 12 not defined at top level.">>])
    , ?TYPE_ERROR(bad_address_literals,
-        [<<?Pos(32, 5)
-           "The type bytes(32) is not a contract type\n"
-           "when checking that the contract literal\n"
-           "  ct_Ez6MyeTMm17YnTnDdHTSrzMEBKmy7Uz2sXu347bTDPgVH2ifJ\n"
-           "has the type\n"
-           "  bytes(32)">>,
-         <<?Pos(30, 5)
-           "The type oracle(int, bool) is not a contract type\n"
-           "when checking that the contract literal\n"
-           "  ct_Ez6MyeTMm17YnTnDdHTSrzMEBKmy7Uz2sXu347bTDPgVH2ifJ\n"
-           "has the type\n"
-           "  oracle(int, bool)">>,
-         <<?Pos(28, 5)
-           "The type address is not a contract type\n"
-           "when checking that the contract literal\n"
-           "  ct_Ez6MyeTMm17YnTnDdHTSrzMEBKmy7Uz2sXu347bTDPgVH2ifJ\n"
-           "has the type\n"
-           "  address">>,
-         <<?Pos(25, 5)
-           "Cannot unify oracle_query('a, 'b)\n"
-           "         and Remote\n"
-           "when checking the type of the expression at line 25, column 5\n"
-           "  oq_2oRvyowJuJnEkxy58Ckkw77XfWJrmRgmGaLzhdqb67SKEL1gPY :\n"
-           "    oracle_query('a, 'b)\n"
-           "against the expected type\n"
-           "  Remote">>,
-         <<?Pos(23, 5)
-           "Cannot unify oracle_query('c, 'd)\n"
-           "         and bytes(32)\n"
-           "when checking the type of the expression at line 23, column 5\n"
-           "  oq_2oRvyowJuJnEkxy58Ckkw77XfWJrmRgmGaLzhdqb67SKEL1gPY :\n"
-           "    oracle_query('c, 'd)\n"
-           "against the expected type\n"
-           "  bytes(32)">>,
-         <<?Pos(21, 5)
-           "Cannot unify oracle_query('e, 'f)\n"
-           "         and oracle(int, bool)\n"
-           "when checking the type of the expression at line 21, column 5\n"
-           "  oq_2oRvyowJuJnEkxy58Ckkw77XfWJrmRgmGaLzhdqb67SKEL1gPY :\n"
-           "    oracle_query('e, 'f)\n"
-           "against the expected type\n"
-           "  oracle(int, bool)">>,
-         <<?Pos(18, 5)
-           "Cannot unify oracle('g, 'h)\n"
-           "         and Remote\n"
-           "when checking the type of the expression at line 18, column 5\n"
-           "  ok_2YNyxd6TRJPNrTcEDCe9ra59SVUdp9FR9qWC5msKZWYD9bP9z5 :\n"
-           "    oracle('g, 'h)\n"
-           "against the expected type\n"
-           "  Remote">>,
-         <<?Pos(16, 5)
-           "Cannot unify oracle('i, 'j)\n"
-           "         and bytes(32)\n"
-           "when checking the type of the expression at line 16, column 5\n"
-           "  ok_2YNyxd6TRJPNrTcEDCe9ra59SVUdp9FR9qWC5msKZWYD9bP9z5 :\n"
-           "    oracle('i, 'j)\n"
-           "against the expected type\n"
-           "  bytes(32)">>,
-         <<?Pos(14, 5)
-           "Cannot unify oracle('k, 'l)\n"
-           "         and oracle_query(int, bool)\n"
-           "when checking the type of the expression at line 14, column 5\n"
-           "  ok_2YNyxd6TRJPNrTcEDCe9ra59SVUdp9FR9qWC5msKZWYD9bP9z5 :\n"
-           "    oracle('k, 'l)\n"
-           "against the expected type\n"
-           "  oracle_query(int, bool)">>,
-         <<?Pos(11, 5)
+        [<<?Pos(11, 5)
           "Cannot unify address\n"
           "         and oracle(int, bool)\n"
           "when checking the type of the expression at line 11, column 5\n"
@@ -451,6 +406,72 @@ failing_contracts() ->
           "  ak_2gx9MEFxKvY9vMG5YnqnXWv1hCsX7rgnfvBLJS4aQurustR1rt : address\n"
           "against the expected type\n"
           "  bytes(32)">>,
+         <<?Pos(14, 5)
+           "Cannot unify oracle('a, 'b)\n"
+           "         and oracle_query(int, bool)\n"
+           "when checking the type of the expression at line 14, column 5\n"
+           "  ok_2YNyxd6TRJPNrTcEDCe9ra59SVUdp9FR9qWC5msKZWYD9bP9z5 :\n"
+           "    oracle('a, 'b)\n"
+           "against the expected type\n"
+           "  oracle_query(int, bool)">>,
+         <<?Pos(16, 5)
+           "Cannot unify oracle('c, 'd)\n"
+           "         and bytes(32)\n"
+           "when checking the type of the expression at line 16, column 5\n"
+           "  ok_2YNyxd6TRJPNrTcEDCe9ra59SVUdp9FR9qWC5msKZWYD9bP9z5 :\n"
+           "    oracle('c, 'd)\n"
+           "against the expected type\n"
+           "  bytes(32)">>,
+         <<?Pos(18, 5)
+           "Cannot unify oracle('e, 'f)\n"
+           "         and Remote\n"
+           "when checking the type of the expression at line 18, column 5\n"
+           "  ok_2YNyxd6TRJPNrTcEDCe9ra59SVUdp9FR9qWC5msKZWYD9bP9z5 :\n"
+           "    oracle('e, 'f)\n"
+           "against the expected type\n"
+           "  Remote">>,
+         <<?Pos(21, 5)
+           "Cannot unify oracle_query('g, 'h)\n"
+           "         and oracle(int, bool)\n"
+           "when checking the type of the expression at line 21, column 5\n"
+           "  oq_2oRvyowJuJnEkxy58Ckkw77XfWJrmRgmGaLzhdqb67SKEL1gPY :\n"
+           "    oracle_query('g, 'h)\n"
+           "against the expected type\n"
+           "  oracle(int, bool)">>,
+         <<?Pos(23, 5)
+           "Cannot unify oracle_query('i, 'j)\n"
+           "         and bytes(32)\n"
+           "when checking the type of the expression at line 23, column 5\n"
+           "  oq_2oRvyowJuJnEkxy58Ckkw77XfWJrmRgmGaLzhdqb67SKEL1gPY :\n"
+           "    oracle_query('i, 'j)\n"
+           "against the expected type\n"
+           "  bytes(32)">>,
+         <<?Pos(25, 5)
+           "Cannot unify oracle_query('k, 'l)\n"
+           "         and Remote\n"
+           "when checking the type of the expression at line 25, column 5\n"
+           "  oq_2oRvyowJuJnEkxy58Ckkw77XfWJrmRgmGaLzhdqb67SKEL1gPY :\n"
+           "    oracle_query('k, 'l)\n"
+           "against the expected type\n"
+           "  Remote">>,
+         <<?Pos(28, 5)
+           "The type address is not a contract type\n"
+           "when checking that the contract literal\n"
+           "  ct_Ez6MyeTMm17YnTnDdHTSrzMEBKmy7Uz2sXu347bTDPgVH2ifJ\n"
+           "has the type\n"
+           "  address">>,
+         <<?Pos(30, 5)
+           "The type oracle(int, bool) is not a contract type\n"
+           "when checking that the contract literal\n"
+           "  ct_Ez6MyeTMm17YnTnDdHTSrzMEBKmy7Uz2sXu347bTDPgVH2ifJ\n"
+           "has the type\n"
+           "  oracle(int, bool)">>,
+         <<?Pos(32, 5)
+           "The type bytes(32) is not a contract type\n"
+           "when checking that the contract literal\n"
+           "  ct_Ez6MyeTMm17YnTnDdHTSrzMEBKmy7Uz2sXu347bTDPgVH2ifJ\n"
+           "has the type\n"
+           "  bytes(32)">>,
         <<?Pos(34, 5),
           "The type address is not a contract type\n"
           "when checking that the call to\n"
@@ -566,7 +587,7 @@ failing_contracts() ->
            "Failed to resolve byte array lengths in call to Bytes.split with argument of type\n"
            "  - 'f  (at line 12, column 20)\n"
            "and result types\n"
-            "  - 'e  (at line 13, column 5)\n"
+            "  - 'e  (at line 12, column 25)\n"
            "  - bytes(20)  (at line 12, column 29)">>,
          <<?Pos(16, 5)
            "Failed to resolve byte array lengths in call to Bytes.split with argument of type\n"
@@ -579,7 +600,7 @@ failing_contracts() ->
            "  - 'b  (at line 18, column 20)\n"
            "and result types\n"
            "  - bytes(20)  (at line 18, column 25)\n"
-            "  - 'a  (at line 19, column 5)">>])
+            "  - 'a  (at line 18, column 37)">>])
    , ?TYPE_ERROR(wrong_compiler_version,
        [<<?Pos(1, 1)
           "Cannot compile with this version of the compiler,\n"
@@ -595,6 +616,77 @@ failing_contracts() ->
         [<<?Pos(5, 28)
            "Invalid call to contract entrypoint 'Foo.foo'.\n"
            "It must be called as 'c.foo' for some c : Foo.">>])
+    , ?TYPE_ERROR(toplevel_let,
+                  [<<?Pos(2, 7)
+                     "Toplevel \"let\" definitions are not supported\n"
+                     "Value this_is_illegal at line 2, column 7 could be replaced by 0-argument function">>])
+    , ?TYPE_ERROR(empty_typedecl,
+                  [<<?Pos(2, 8)
+                     "Empty type declarations are not supported\n"
+                     "Type t at line 2, column 8 lacks a definition">>])
+    , ?TYPE_ERROR(higher_kinded_type,
+                  [<<?Pos(2, 35)
+                     "Type 'm is a higher kinded type variable\n"
+                     "(takes another type as an argument)">>])
+    , ?TYPE_ERROR(bad_arity,
+                  [<<?Pos(3, 20)
+                     "Arity for id doesn't match. Expected 1, got 0">>,
+                   <<?Pos(3, 25)
+                     "Cannot unify int\n"
+                     "         and id\n"
+                     "when checking the type of the expression at line 3, column 25\n"
+                     "  123 : int\n"
+                     "against the expected type\n"
+                     "  id">>,
+                   <<?Pos(4, 20)
+                     "Arity for id doesn't match. Expected 1, got 2">>,
+                   <<?Pos(4, 35)
+                     "Cannot unify int\n"
+                     "         and id(int, int)\n"
+                     "when checking the type of the expression at line 4, column 35\n"
+                     "  123 : int\n"
+                     "against the expected type\n"
+                     "  id(int, int)">>])
+    , ?TYPE_ERROR(bad_unnamed_map_update_default,
+                  [<<?Pos(4, 17)
+                     "Invalid map update with default">>])
+    , ?TYPE_ERROR(non_functional_entrypoint,
+                  [<<?Pos(2, 14)
+                     "f at line 2, column 14 was declared with an invalid type int.\n"
+                     "Entrypoints and functions must have functional types">>])
+    , ?TYPE_ERROR(bad_records,
+        [<<?Pos(3, 16)
+           "Mixed record fields and map keys in\n"
+           "  {x = 0, [0] = 1}">>,
+         <<?Pos(4, 6)
+           "Mixed record fields and map keys in\n"
+           "  r {x = 0, [0] = 1}">>,
+         <<?Pos(5, 6)
+           "Empty record/map update\n"
+           "  r {}">>
+        ])
+    , ?TYPE_ERROR(bad_number_of_args,
+                  [<<?Pos(3, 39)
+                     "Cannot unify () => unit\n"
+                     "         and (int) => 'a\n",
+                     "when checking the application at line 3, column 39 of\n"
+                     "  f : () => unit\n"
+                     "to arguments\n"
+                     "  1 : int">>,
+                   <<?Pos(4, 20)
+                     "Cannot unify (int, string) => 'e\n"
+                     "         and (int) => 'd\n"
+                     "when checking the application at line 4, column 20 of\n"
+                     "  g : (int, string) => 'e\n"
+                     "to arguments\n"
+                     "  1 : int">>,
+                   <<?Pos(5, 20)
+                     "Cannot unify (int, string) => 'c\n"
+                     "         and (string) => 'b\n"
+                     "when checking the application at line 5, column 20 of\n"
+                     "  g : (int, string) => 'c\nto arguments\n"
+                     "  \"Litwo, ojczyzno moja\" : string">>
+                  ])
    ].

 -define(Path(File), "code_errors/" ??File).
@@ -4,6 +4,8 @@

 -include_lib("eunit/include/eunit.hrl").

+id(X) -> X.
+
 simple_contracts_test_() ->
    {foreach,
     fun() -> ok end,
@@ -14,7 +16,7 @@ simple_contracts_test_() ->
                   "  function id(x) = x\n",
            ?assertMatch(
                [{contract, _, {con, _, "Identity"},
-                    [{letfun, _, {id, _, "id"}, [{arg, _, {id, _, "x"}, {id, _, "_"}}], {id, _, "_"},
+                    [{letfun, _, {id, _, "id"}, [{id, _, "x"}], {id, _, "_"},
                        {id, _, "x"}}]}], parse_string(Text)),
            ok
       end},
@@ -30,7 +32,7 @@ simple_contracts_test_() ->
                    end,
            Parse = fun(S) ->
                    try remove_line_numbers(parse_expr(S))
-                    catch _:_ -> ?assertMatch(ok, {parse_fail, S}) end
+                    catch _:_ -> ?assertMatch(ok, id({parse_fail, S})) end
                end,
            CheckParens = fun(Expr) ->
                    ?assertEqual(Parse(NoPar(Expr)), Parse(Par(Expr)))
@@ -38,7 +40,6 @@ simple_contracts_test_() ->
            LeftAssoc  = fun(Op) -> CheckParens({{a, Op, b}, Op, c}) end,
            RightAssoc = fun(Op) -> CheckParens({a, Op, {b, Op, c}}) end,
            NonAssoc   = fun(Op) ->
-                            OpAtom = list_to_atom(Op),
                            ?assertThrow({error, [_]},
                                         parse_expr(NoPar({a, Op, {b, Op, c}}))) end,
            Stronger = fun(Op1, Op2) ->
@@ -77,7 +78,7 @@ parse_string(Text, Opts) ->
    aeso_parser:string(Text, Opts).

 parse_expr(Text) ->
-    [{letval, _, _, _, Expr}] =
+    [{letval, _, _, Expr}] =
        parse_string("let _ = " ++ Text),
    Expr.

@@ -58,8 +58,7 @@ contract Greeter =

    let state = { greeting = "Hello" }

-    let setGreeting =
-        (greeting: string) =>
+    function setGreeting(greeting: string) =
            state{ greeting = greeting }


@@ -1,44 +1,78 @@
 // Try to cover all syntactic constructs.
+@compiler > 0
+@compiler =< 10.1.1.1.1.1.2.3.4

-contract AllSyntaxType =
-  type typeDecl /* bla */
-  type paramTypeDecl('a, 'b)

+namespace Ns =
+  datatype d('a) = D | S(int) | M('a, list('a), int)
+  private function fff() = 123
+
+  stateful entrypoint
+    f (1, x) = (_) => x
+
+payable contract AllSyntaxType =
  /** Multi-
    * line
    * comment
    */
-  function foo : _
+  stateful function foo : _
+  entrypoint bar : int => (int * 'a)
+

 contract AllSyntax =

-  type typeDecl = int
-  type paramTypeDecl('a, 'b) = (('a, 'b) => 'b) => list('a) => 'b => 'b
+  datatype mickiewicz = Adam | Mickiewicz
+  record goethe('a, 'b) = {
+    johann : int,
+    wolfgang : 'a,
+    von : 'a * 'b * int,
+    goethe : unit
+    }
+  type dante = Ns.d(int)
+  type shakespeare('a) = goethe('a, 'a)

-  record nestedRecord = { x : int }
-  record recordType = { z : nestedRecord, y : int }
-  datatype variantType('a) = None | Some('a)
+  type state = shakespeare(int)

-  let valWithType : map(int, int) => option(int) = (m) => Map.get(m, 42)
-  let valNoType =
-        if(valWithType(Map.empty) == None)
-          print(42 mod 10 * 5 / 3)
+  entrypoint init() = {
+    johann = 1000,
+    wolfgang = -10,
+    von = (2 + 2, 0, List.sum([x | k <- [1,2,3]
+                                 , let l = k + 1
+                                 , if(l < 10)
+                                 , let f(x) = x + 100
+                                 , Adam <- [Adam, Mickiewicz]
+                                 , let x = f(l)
+                                 ])),
+    goethe = () }

-  function funWithType(x : int, y) : int * list(int) = (x, 0 :: [y] ++ [])
-  function funNoType() =
-    let foo = (x, y : bool) =>
-                if (! (y && x =< 0x0b || true)) [x]
-                else [11..20]
-    let setY(r : recordType) : unit = r{ y = 5 }
-    let setX(r : recordType, x : int) : recordType = r { z.x = x }  // nested record update
-    let getY(r) = switch(r) {y = y} => y
-    switch (funWithType(1, -2))
-      (x, [y, z]) => bar({x = z, y = -y + - -z * (-1)})
-      (x, y :: _) => ()
+  function f() =
+     let kp = "nietzsche"
+     let p = "Пушкин"
+     let k(x : bytes(8)) : bytes(8) = Bytes.to_int(#fedcba9876543210)

-  let hash : address = #01ab0fff11
-  let b = false
-  let qcon = Mod.Con
-  let str = "blabla\nfoo"
-  let chr = '"'
+     let f : () => address = () => ak_2gx9MEFxKvY9vMG5YnqnXWv1hCsX7rgnfvBLJS4aQurustR1rt
+     if(Bits.test(Bits.all, 10))
+       abort("ohno")
+     if(true && false)
+       require(true, "ohyes")
+     elif(false || 2 == 2)
+       ()
+     else
+       ()
+     if(true) f(1,2)((1,2))
+     else switch(1::[1,2,3])
+       [] => 1
+       a::b => 123
+       1::2::3 => 123123
+       [2,3,4] => 1
+       _ => 13
+       1::[2] => 2138
+     put(state{johann = 1})
+     
+     let m = {["foo"] = 19, /*hey wanna talk about inlined comments?*/ ["bar"] = 42}
+     let n = {}
+     m{ ["x" = 0] @ z = z + state.johann }

+     let sh : shakespeare(shakespeare(int)) =
+       {wolfgang = state}
+     sh{wolfgang.wolfgang = sh.wolfgang} // comment
@@ -0,0 +1,4 @@
+contract C =
+  type id('a) = 'a
+  entrypoint f() : id = 123
+  entrypoint g() : id(int, int) = 123
@@ -0,0 +1,6 @@
+contract Test =
+  entrypoint f() = ()
+  entrypoint g(x : int, y : string) = f(1)
+  entrypoint h() = g(1)
+  entrypoint i() = g("Litwo, ojczyzno moja")
+  
@@ -0,0 +1,5 @@
+contract BadRecord =
+  entrypoint foo() =
+    let r = {x = 0, [0] = 1}
+    r{x = 0, [0] = 1}
+    r{}
@@ -0,0 +1,5 @@
+contract C =
+  entrypoint f() =
+    let z = 123
+    {}{ [1 = 0] = z + 1 }
+    2
@@ -0,0 +1,3 @@
+contract C =
+  type t
+  entrypoint f() = 123
@@ -11,7 +11,7 @@ contract Factorial =

  stateful entrypoint set_worker(worker) = put(state{worker = worker})

-  entrypoint fac(x : int) : int =
-    if(x == 0) 1
-    else x * state.worker.fac(x - 1)
-
+  entrypoint
+    fac : int => int
+    fac(0) = 1
+    fac(x) = x * state.worker.fac(x - 1)
@@ -0,0 +1,3 @@
+contract IWantToBelieve =
+  type stateT('s, 'm, 'a) = 's => 'm('a * 's)
+  entrypoint s() = 123
@@ -0,0 +1,4 @@
+contract Foo =
+  record r = {x : int}
+  // Crashed in the backend due to missing type annotation on the lc body.
+  entrypoint lc(xs) = [ {x = x} | x <- xs ]
@@ -0,0 +1,15 @@
+contract LetPatterns =
+
+  record r = {x : int, y : int, b : bool}
+
+  entrypoint test() = foo([1, 0], (2, 3), Some(4), {x = 5, y = 6, b = false})
+
+  entrypoint foo(xs : list(int), p : int * int, some : option(int), r : r) =
+    let x :: _  = xs
+    let (a, b)  = p
+    let Some(n) = some
+    let {x = i, y = j} = r
+    x + a + b + n + i + j
+
+  entrypoint lc(xs : list(option(int))) : list(int) =
+    [ x | Some(x) <- xs ]
@@ -0,0 +1,22 @@
+contract LHSMatching =
+
+  function from_some(Some(x)) = x
+
+  function
+    length : list('a) => int
+    length([])      = 0
+    length(_ :: xs) = 1 + length(xs)
+
+  function
+    append([], ys)      = ys
+    append(x :: xs, ys) = x :: append(xs, ys)
+
+  function local_match(xs : list('a)) =
+    let null([])     = true
+    let null(_ :: _) = false
+    !null(xs)
+
+  entrypoint main() =
+    from_some(Some([0]))
+      ++ append([length([true]), 2, 3], [4, 5, 6])
+      ++ [7 | if (local_match([false]))]
@@ -15,7 +15,7 @@ contract MultiSig =
      | OwnerRemoved (address)          // of { .removedOwner : Address }
      | ReqChanged   (int)             // of { .newReq : int }

-    let maxOwners : int = 250
+    function maxOwners() : int = 250

    record state = { nRequired    : int
                 , nOwners      : int
@@ -68,7 +68,7 @@ contract MultiSig =
      switch(check_pending(callhash()))
        CheckFail(state') => { state = state' }
        CheckOk(state') =>
-            if(state.nOwners >= maxOwners) () /* TODO */
+            if(state.nOwners >= maxOwners()) () /* TODO */
            else
              let nOwners' = state'.nOwners + 1
              { state = state' { owners    = Map.insert(nOwners', newOwner, state'.owners)
@@ -0,0 +1,5 @@
+contract C1 =
+  entrypoint f : int
+
+contract C =
+  entrypoint f() = 123
@@ -0,0 +1,6 @@
+namespace BadNs =
+  contract Con =
+    entrypoint e : () => int
+
+contract Con =
+  entrypoint foo() = 43
@@ -0,0 +1,5 @@
+namespace BadNs =
+  include "included.aes"
+
+contract Con =
+  entrypoint foo() = 43
@@ -1,5 +1,4 @@
-contract Bad =
-  include "included.aes"
+contract BadCon =
  namespace Foo =
    function foo() = 42

@@ -0,0 +1,8 @@
+namespace Foo =
+  datatype x = A | B(int)
+
+contract Bar =
+  entrypoint f(a : Foo.x) =
+    switch(a)
+      Foo.A     => 0
+      Foo.B(n)  => n
@@ -8,10 +8,9 @@ contract Stack =

  entrypoint init(ss : list(string)) = { stack = ss, size = length(ss) }

-  function length(xs) =
-    switch(xs)
-      [] => 0
-      _ :: xs => length(xs) + 1
+  function
+    length([])      = 0
+    length(_ :: xs) = length(xs) + 1

  stateful entrypoint pop() : string =
    switch(state.stack)
@@ -0,0 +1,3 @@
+contract C =
+  let this_is_illegal = 2/0
+  entrypoint this_is_legal() = 2/0
@@ -1,16 +1,3 @@
-
-/* Contract type */
-contract VotingType =
-  type state
-  function init            : list(string) => state
-
-  function giveRightToVote : address => unit
-  function delegate        : address => unit
-  function vote            : int => unit
-  function winnerName      : unit => string
-  function currentTally    : unit => list(string * int)
-
-/* Contract implementation */
 contract Voting =

  // Types
Author	SHA1	Message	Date
Radosław Rowicki	962ddf5303	Version push – 4.3.0 (#255 ) * Version push – 4.3.0 . * Fixed ordering of diffs in CHANGELOG	2020-04-02 15:10:53 +02:00
Radosław Rowicki	85b151aa65	Prepare 4.3.0 (#254 )	2020-04-02 13:59:22 +02:00
Radosław Rowicki	93341dc13b	Prepared for REPL usage (#218 ) * Prepared for REPL usage Exposed expr parsing ets init in constant Exposing and fixing exposed expr This will be squashed either Expose letdef Error handling exposed autoimport remove unnecessary changes Fix types Parser update Expose body parser remove map_get warning make dialyzer happy * Formatting Co-Authored-By: Hans Svensson <hanssv@gmail.com> Co-authored-by: Hans Svensson <hanssv@gmail.com>	2020-04-02 12:29:14 +02:00
Radosław Rowicki	98036eff65	Update TOC in sophia.md (#245 )	2020-04-01 13:11:02 +02:00
Radosław Rowicki	dc977f7354	Fixed example (#249 )	2020-03-31 13:14:13 +02:00
Radosław Rowicki	4f554acee6	Fix error messages for some illegal constructions, fix absolute path includes (#251 ) * Updated tests, banned type decls and toplevel letvals * Properly ban nested contracts * Fix including by path * Fix error message test * Fix prettpr attr display. Make dialyzer happy * More tests * Fixed type printing * Updated docs	2020-03-30 14:52:16 +02:00
Radosław Rowicki	48b52cb501	Enchanted Frac library a bit (#253 )	2020-03-29 17:14:01 +02:00
Ulf Norell	515838e2f9	Handle negative numbers in aci (#247 ) * Handle negative numbers in aci Fixes aeternity/aesophia_http#59 * Updated CHANGELOG Updated CHANGELOG1 Co-authored-by: radrow <radrowicki@gmail.com>	2020-03-23 18:11:00 +01:00
Radosław Rowicki	83e03f3013	Added documentation (#239 ) * Added documentation * Update readme * Update readme * Format fix * Events * Stdlib mention * Frac doc * Frac doc comparison warning * Typos * Format fix, TOC added * Fixed link * Update editor message * Split TOC * Moved out AEVM ABI * Minor format Co-Authored-By: Hans Svensson <hanssv@gmail.com> * Typo Co-Authored-By: Hans Svensson <hanssv@gmail.com> * Grammar Co-Authored-By: Hans Svensson <hanssv@gmail.com> * Language Co-authored-by: Hans Svensson <hanssv@gmail.com>	2020-03-10 12:39:39 +01:00
Radosław Rowicki	d7fa4d65ec	More comments in stdlib (#237 )	2020-02-25 12:56:51 +01:00
Radosław Rowicki	bd7ed2ef8c	Instant unification error on arguments count mismatch (#225 ) * Instant unification error on arguments count mismatch * add testcase * Add newline	2020-02-21 10:28:55 +01:00
Radosław Rowicki	2bf65cfd98	Add Frac (#222 ) Fix bugs in Frac Added optimizer	2020-02-13 11:02:47 +01:00
Hans Svensson	efd45df820	Merge pull request #212 from aeternity/GH-211-prepare_release_4_2_0 Prepare release 4.2.0	2020-01-15 11:58:47 +01:00
Hans Svensson	a6f51d23f3	Bump version to 4.2.0 and fix CHANGELOG	2020-01-15 11:39:25 +01:00
Ulf Norell	4d4a14a9ab	GH-196 pattern matching lhs (#210 ) * Allow block with separate type signature and definition of a function For instance, ``` function add : (int, int) => int add(x, y) = x + y ``` cc #196 * Allow pattern matching in left-hand sides * Changelog * Fix type spec * partial case-on-constructor * Changelog for pattern-matching lets	2020-01-15 09:41:03 +01:00
Ulf Norell	f7abaf07fa	Add list comprehension match to test case	2019-12-16 17:04:49 +01:00
Ulf Norell	d019e44924	Compile values to immediates when possible	2019-12-16 17:04:49 +01:00
Ulf Norell	ad54134961	Parse negative literal patterns	2019-12-16 17:04:49 +01:00
Ulf Norell	b51a79b5e1	Allow patterns in lets and list comprehension binds	2019-12-16 17:04:49 +01:00
Ulf Norell	d844c4d276	Fix missing type annotation in list comprehension body	2019-12-12 09:39:13 +01:00
Ulf Norell	64e2fff91a	Handle list comprehensions in pretty printer	2019-12-12 09:39:13 +01:00
Ulf Norell	d4f291f252	Handle qualified constructors in patterns	2019-12-12 09:34:26 +01:00
Ulf Norell	b9f585ebaf	Merge pull request #205 from aeternity/fate-flatten-store FATE backend optimisations	2019-12-12 09:22:37 +01:00
Ulf Norell	954af13f59	Fix debug printing of store registers	2019-12-12 09:14:34 +01:00
Ulf Norell	2e4558b3b4	Changelog	2019-12-10 12:57:52 +01:00
Ulf Norell	a403a9d227	Unbox singleton tuples and records	2019-12-10 12:24:05 +01:00
Ulf Norell	c7b846cbfe	Merge pull request #190 from aeternity/GH-189-parse-error-crash Fix parse errors causing crashes instead of nice errors	2019-12-09 10:27:20 +01:00
Ulf Norell	bf5e2e2443	Fix parse errors causing crashes instead of nice errors	2019-12-09 08:45:55 +01:00
Ulf Norell	46a30b118f	Get rid of unnecessary return instruction after tail-call	2019-11-26 13:33:11 +01:00
Ulf Norell	bb1a45c557	Improve case-on-constructor optimisation	2019-11-26 13:10:58 +01:00
Ulf Norell	0a22c7a34a	More let-floating	2019-11-26 13:10:58 +01:00
Ulf Norell	c8153f94a6	More aggressive freshening to avoid shadowing issues	2019-11-26 13:10:58 +01:00
Ulf Norell	63d51baaa3	Dialyzer issues	2019-11-26 13:10:58 +01:00
Ulf Norell	cb045b0256	whitespace	2019-11-26 13:10:58 +01:00
Ulf Norell	c84064da7f	Inline local functions and simplify case-on-constructor	2019-11-26 13:10:58 +01:00
Ulf Norell	ad88797cef	Proper handling of lets in term_to_fate	2019-11-26 13:10:58 +01:00
Ulf Norell	6c3932b10c	Flattened state layout ... with necessary optimizations.	2019-11-26 13:10:56 +01:00
Ulf Norell	8d7c637241	Don't confuse variables and store registers in fate asm generation	2019-11-26 13:10:04 +01:00
Ulf Norell	a8119f1219	Track state layout ... but only default layout still.	2019-11-26 13:10:04 +01:00
Ulf Norell	d0fdd06d66	Change get_state and set_state fcode primitives to take a register	2019-11-26 13:10:04 +01:00
Ulf Norell	99ecda4b7b	Fix warnings in test suites	2019-11-26 13:10:04 +01:00
Ulf Norell	e645a8d034	Optimize before lambda lifting (lambdas are either in dead code or not dead, so dead code elimination won't be affected)	2019-11-26 13:10:04 +01:00
Ulf Norell	499e2f8200	Handle records and type aliases correctly in fcode	2019-11-26 13:10:04 +01:00
Ulf Norell	5465b74ac9	Allow specifying store register in FATE backend	2019-11-26 13:10:04 +01:00
Hans Svensson	6ca63e4b40	Merge pull request #184 from aeternity/GH-181-prepare-4.1.0 Bump version to 4.1.0	2019-11-26 09:02:56 +01:00
Ulf Norell	08b6148223	Bump version to 4.1.0	2019-11-26 09:02:26 +01:00