Repository: tweag/nickel
Pull request #315 (2021-03-08 19:17:08)

Remove assume from the AST, improve contract error reporting
Depend on #314. Following #314, `Assume` as a standalone AST node isn't useful anymore, as it can be implemented in terms of existing operations. This PR removes the `Assume` node, now implemented by the `ApplyContract` operator.

`ApplyContract` is also splitt in two more atomic operators, one named `Assume` that is in charge of filling the label with required information and track the contract argument, while `ToCtrFn` is a wrapper that in charge of converting contracts as record to vanilla contract functions.

As a reward, tracked arguments introduced in #302, that were basically restricted to flat contracts, now works with composed (sub)contracts (records, lists, and functions): in the following example, although the contract is higher-order, the error pinpoints the value of ground type actually causing the problem, which was not the case previously.

```
nickel> let Nat = fun l x =>
  if (builtins.isNum x && x % 1 == 0 && x >= 0) then
    x
  else
    contracts.blame l
nickel> let f | ((#Nat -> #Nat) -> #Nat) -> #Nat =
  fun ev => ev (fun x => x + 0.5)
nickel> f (fun f => f 10)

error: Blame error: contract broken by a function.
  ┌─ :1:11
  │
1 │ ((#Nat -> #Nat) -> #Nat) -> #Nat
  │           ---- expected return type of a sub-function passed as an argument of an inner call
  │
  ┌─ repl-input-6:2:26
  │
2 │   fun ev => ev (fun x => x + 0.5)
  │                          ------- evaluated to this expression
  │
  ┌─ <unkown> (generated by evaluation):1:1
  │
1 │ 10.5
  │ ---- evaluated to this value
  │
[...]
```


Patch:
diff --git a/README.md b/README.md
index f85f2fa6..2232d92f 100644
--- a/README.md
+++ b/README.md
@@ -104,15 +104,10 @@ decisions and trade-offs.
 
 ### Run
 
-1. *(optional)* make a symbolic link to the executable:
+1. (*optional*) Make a symbolic link to the executable:
   ```
   nickel$ ln -S nickel target/debug/nickel
   ```
-  Alternatively, you can use `cargo run` to launch nickel. To pass arguments to
-  nickel using `cargo run`, use `--`:
-  ```
-  nickel$ cargo run -- -f program.ncl
-  ```
 
 2. Run your first program:
   ```
@@ -123,32 +118,12 @@ decisions and trade-offs.
   Or load it from a file:
   ```
   nickel$ echo 'let s = "world" in "Hello, " ++ s' > program.ncl
-  nickel$ ./nickel -f program.ncl
+  nickel$ ./nickel < program.ncl
   Typechecked: Ok(Types(Dyn))
   Done: Str("Hello, world")
   ```
 
-3. Start an REPL:
-  ```
-  nickel$ ./nickel repl
-  nickel> let x = 2 in x + x
-  nickel> x
-  4
-
-  nickel>
-  ```
-  Use `:help` for a list of available commands.
-
-4. Export your configuration to JSON, YAML or TOML:
-  ```
-  nickel$ ./nickel export --format json <<< '{foo = "Hello, world!"}'
-  {
-    "foo": "Hello, world!"
-  }
-  ```
-
-Use `nickel help` for a list of subcommands, and `nickel help <subcommand>`
-for help about a specific subcommand.
+By default, Nickel reads from the standard input. It may change in the future.
 
 ### Tests
 ```
@@ -175,11 +150,12 @@ and others important practical aspects are still being debated. We aim to
 transition from an experimental stage to a minimum viable product stage.  The
 next points to deal with are:
 
-- [Stdlib stabilization](https://github.com/tweag/nickel/issues/321)
-- [Overriding](https://github.com/tweag/nickel/pull/330)
-- Memory management (use reference counting) & basic performance improvements
+- Imports
 - [List comprehensions](https://github.com/tweag/nickel/issues/80)
 - [Destructuring](https://github.com/tweag/nickel/issues/81)
+- [String interpolation](https://github.com/tweag/nickel/issues/82)
+- [Recursive records](https://github.com/tweag/nickel/issues/83)
+- Syntax
 
 ## Related projects and inspirations
 - [Cue](https://cuelang.org/) is a configuration language with a focus on data
diff --git a/src/error.rs b/src/error.rs
index f85900f6..b2bf96cf 100644
--- a/src/error.rs
+++ b/src/error.rs
@@ -870,66 +870,66 @@ impl ToDiagnostic<FileId> for EvalError {
                 let mut labels = vec![path_label];
 
                 if let Some(ref arg_pos) = l.arg_pos.into_opt() {
-                    labels.push(primary(&arg_pos).with_message("applied to this expression"));
+                    // In some cases, if the blame error is located in an argument or return value
+                    // of an higher order functions for example, the original argument position can
+                    // point to the builtin implementation contract like `func` or `record`, so
+                    // there's no good reason to show it. Note than even in that case, the
+                    // information contained in the argument thunk can still be useful.
+                    if contract_id
+                        .map(|ctrs_id| arg_pos.src_id != ctrs_id)
+                        .unwrap_or(true)
+                    {
+                        labels.push(primary(&arg_pos).with_message("applied to this expression"));
+                    }
                 }
 
                 // If we have a reference to the thunk that was being tested, we can try to show
                 // more information about the final, evaluated value that is responsible for the
                 // blame.
                 if let Some(ref thunk) = l.arg_thunk {
-                    // The indication may be verbose, and are less useful in case of a function
-                    // contract. We only show the following information for ground types.
-                    if ty_path::has_no_arrow(&l.path) {
-                        let mut val = thunk.get_owned().body;
-
-                        match (val.pos, l.arg_pos.as_opt_ref(), contract_id) {
-                            // Avoid showing a position inside builtin contracts, it's rarely
-                            // informative.
-                            (TermPos::Original(val_pos), _, Some(c_id))
-                                if val_pos.src_id == c_id =>
-                            {
-                                val.pos = TermPos::None;
-                                labels.push(
-                                    secondary_term(&val, files)
-                                        .with_message("evaluated to this value"),
-                                );
-                            }
-                            // Do not show the same thing twice: if arg_pos and val_pos are the same,
-                            // the first label "applied to this value" is sufficient.
-                            (TermPos::Original(ref val_pos), Some(arg_pos), _)
-                                if val_pos == arg_pos => {}
-                            (TermPos::Original(ref val_pos), ..) => labels.push(
+                    let mut val = thunk.get_owned().body;
+
+                    match (val.pos, l.arg_pos.as_opt_ref(), contract_id) {
+                        // Avoid showing a position inside builtin contracts, it's rarely
+                        // informative.
+                        (TermPos::Original(val_pos), _, Some(c_id)) if val_pos.src_id == c_id => {
+                            val.pos = TermPos::None;
+                            labels.push(
+                                secondary_term(&val, files).with_message("evaluated to this value"),
+                            );
+                        }
+                        // Do not show the same thing twice: if arg_pos and val_pos are the same,
+                        // the first label "applied to this value" is sufficient.
+                        (TermPos::Original(ref val_pos), Some(arg_pos), _)
+                            if val_pos == arg_pos => {}
+                        (TermPos::Original(ref val_pos), ..) => labels
+                            .push(secondary(val_pos).with_message("evaluated to this expression")),
+                        // If the final thunk is a direct reduct of the original value, rather
+                        // print the actual value than referring to the same position as
+                        // before.
+                        (TermPos::Inherited(ref val_pos), Some(arg_pos), _)
+                            if val_pos == arg_pos =>
+                        {
+                            val.pos = TermPos::None;
+                            labels.push(
+                                secondary_term(&val, files).with_message("evaluated to this value"),
+                            );
+                        }
+                        // Finally, if the parameter reduced to a value which originates from a
+                        // different expression, show both the expression and the value.
+                        (TermPos::Inherited(ref val_pos), ..) => {
+                            labels.push(
                                 secondary(val_pos).with_message("evaluated to this expression"),
-                            ),
-                            // If the final thunk is a direct reduct of the original value, rather
-                            // print the actual value than referring to the same position as
-                            // before.
-                            (TermPos::Inherited(ref val_pos), Some(arg_pos), _)
-                                if val_pos == arg_pos =>
-                            {
-                                val.pos = TermPos::None;
-                                labels.push(
-                                    secondary_term(&val, files)
-                                        .with_message("evaluated to this value"),
-                                );
-                            }
-                            // Finally, if the parameter reduced to a value which originates from a
-                            // different expression, show both the expression and the value.
-                            (TermPos::Inherited(ref val_pos), ..) => {
-                                labels.push(
-                                    secondary(val_pos).with_message("evaluated to this expression"),
-                                );
-                                val.pos = TermPos::None;
-                                labels.push(
-                                    secondary_term(&val, files)
-                                        .with_message("evaluated to this value"),
-                                );
-                            }
-                            (TermPos::None, ..) => labels.push(
-                                secondary_term(&val, files)
-                                    .with_message("value evaluated to this value"),
-                            ),
+                            );
+                            val.pos = TermPos::None;
+                            labels.push(
+                                secondary_term(&val, files).with_message("evaluated to this value"),
+                            );
                         }
+                        (TermPos::None, ..) => labels.push(
+                            secondary_term(&val, files)
+                                .with_message("value evaluated to this value"),
+                        ),
                     }
                 }
 
diff --git a/src/eval.rs b/src/eval.rs
index b961fa7e..4862db7d 100644
--- a/src/eval.rs
+++ b/src/eval.rs
@@ -575,7 +575,7 @@ where
                     }
                 }
             },
-            Term::Promise(ty, mut l, t) | Term::Assume(ty, mut l, t) => {
+            Term::Promise(ty, mut l, t) => {
                 l.arg_pos = t.pos;
                 let thunk = Thunk::new(
                     Closure {
@@ -840,11 +840,6 @@ pub fn subst(rt: RichTerm, global_env: &Environment, env: &Environment) -> RichT
 
                 RichTerm::new(Term::Promise(ty, l, t), pos)
             }
-            Term::Assume(ty, l, t) => {
-                let t = subst_(t, global_env, env, bound);
-
-                RichTerm::new(Term::Assume(ty, l, t), pos)
-            }
             Term::Wrapped(i, t) => {
                 let t = subst_(t, global_env, env, bound);
 
@@ -1103,7 +1098,7 @@ mod tests {
     fn imports() {
         let mut resolver = SimpleResolver::new();
         resolver.add_source(String::from("two"), String::from("1 + 1"));
-        resolver.add_source(String::from("lib"), String::from("{f = true}"));
+        resolver.add_source(String::from("lib"), String::from("{ f = true }"));
         resolver.add_source(String::from("bad"), String::from("^$*/.23ab 0°@"));
         resolver.add_source(
             String::from("nested"),
@@ -1111,7 +1106,7 @@ mod tests {
         );
         resolver.add_source(
             String::from("cycle"),
-            String::from("let x = import \"cycle_b\" in {a = 1, b = x.a}"),
+            String::from("let x = import \"cycle_b\" in {a = 1; b = x.a}"),
         );
         resolver.add_source(
             String::from("cycle_b"),
@@ -1319,11 +1314,11 @@ mod tests {
                 .unwrap()
         );
 
-        let t = parse("switch {x => [1, glob1], y => loc2, z => {id = true, other = glob3}} loc1")
+        let t = parse("switch {x => [1, glob1], y => loc2, z => {id = true; other = glob3},} loc1")
             .unwrap();
         assert_eq!(
             subst(t, &global_env, &env),
-            parse("switch {x => [1, 1], y => (if false then 1 else \"Glob2\"), z => {id = true, other = false}} true").unwrap()
+            parse("switch {x => [1, 1], y => (if false then 1 else \"Glob2\"), z => {id = true; other = false},} true").unwrap()
         );
     }
 }
diff --git a/src/grammar.lalrpop b/src/grammar.lalrpop
index f68994cd..e90618c0 100644
--- a/src/grammar.lalrpop
+++ b/src/grammar.lalrpop
@@ -34,7 +34,7 @@ MetaAnnotAtom: MetaValue = {
         priority: MergePriority::Default,
         value: None,
     },
-    "|" "doc" <s: StaticString> => MetaValue {
+    "|" "doc" <s: Str> => MetaValue {
         doc: Some(strip_indent_doc(s)),
         types: None,
         contracts: Vec::new(),
@@ -148,7 +148,7 @@ RichTerm: RichTerm = {
     },
     "if" <b:Term> "then" <t:Term> "else" <e:SpTerm<RichTerm>> =>
         mk_app!(Term::Op1(UnaryOp::Ite(), b), t, e),
-    "import" <s: StaticString> => RichTerm::from(Term::Import(OsString::from(s))),
+    "import" <s: Str> => RichTerm::from(Term::Import(OsString::from(s))),
     SpTerm<InfixExpr>,
 };
 
@@ -180,7 +180,7 @@ Atom: RichTerm = {
     <StrChunks>,
     Ident => RichTerm::from(Term::Var(<>)),
     "`" <Ident> => RichTerm::from(Term::Enum(<>)),
-    "{" <fields: (<RecordField> ",")*> <last: RecordField?> "}" => {
+    "{" <fields: (<RecordField> ";")*> <last: RecordField?> "}" => {
         let fields = fields.into_iter().chain(last.into_iter());
         RichTerm::from(build_record(fields))
     },
@@ -241,7 +241,7 @@ Bool: bool = {
 StrChunks : RichTerm = {
   <start: StringStart> <fst: ChunkLiteral?> <chunks: (ChunkExpr+ChunkLiteral)*> <lasts:
     ChunkExpr*> <end: StringEnd> => {
-        debug_assert_eq!(start, end);
+        assert_eq!(start, end);
 
         let chunks: Vec<StrChunk<RichTerm>> = fst.into_iter()
             .map(StrChunk::Literal)
@@ -292,7 +292,7 @@ ChunkExpr: StrChunk<RichTerm> = HashBrace <t: SpTerm<RichTerm>> "}" => StrChunk:
 
 HashBrace = { "#{", "multstr #{" };
 
-StaticString: String = StringStart <s: ChunkLiteral> StringEnd => s;
+Str: String = "\"" <s: ChunkLiteral> "\"" => s;
 
 ChunkLiteralPart: ChunkLiteralPart<'input> = {
     "str literal" => ChunkLiteralPart::Str(<>),
@@ -311,7 +311,6 @@ UOp: UnaryOp = {
     "isList" => UnaryOp::IsList(),
     "isRecord" => UnaryOp::IsRecord(),
     "blame" => UnaryOp::Blame(),
-    "applyContract" => UnaryOp::ApplyContract(),
     "chngPol" => UnaryOp::ChangePolarity(),
     "polarity" => UnaryOp::Pol(),
     "goDom" => UnaryOp::GoDom(),
@@ -447,7 +446,6 @@ BOpPre: BinaryOp = {
     "hash" => BinaryOp::Hash(),
     "serialize" => BinaryOp::Serialize(),
     "deserialize" => BinaryOp::Deserialize(),
-    "pow" => BinaryOp::Pow(),
 }
 
 Types: Types = {
@@ -557,6 +555,7 @@ extern {
         "$" => Token::Normal(NormalToken::Dollar),
         "=" => Token::Normal(NormalToken::Equals),
         "!=" => Token::Normal(NormalToken::NotEquals),
+        ";" => Token::Normal(NormalToken::SemiCol),
         "&" => Token::Normal(NormalToken::Ampersand),
         "." => Token::Normal(NormalToken::Dot),
         "$[" => Token::Normal(NormalToken::DollarBracket),
@@ -595,7 +594,6 @@ extern {
         "List" => Token::Normal(NormalToken::List),
 
         "tag" => Token::Normal(NormalToken::Tag),
-        "applyContract" => Token::Normal(NormalToken::ApplyContract),
         "isNum" => Token::Normal(NormalToken::IsNum),
         "isBool" => Token::Normal(NormalToken::IsBool),
         "isStr" => Token::Normal(NormalToken::IsStr),
@@ -619,7 +617,6 @@ extern {
         "tail" => Token::Normal(NormalToken::Tail),
         "length" => Token::Normal(NormalToken::Length),
         "fieldsOf" => Token::Normal(NormalToken::FieldsOf),
-        "pow" => Token::Normal(NormalToken::Pow),
 
         "hasField" => Token::Normal(NormalToken::HasField),
         "map" => Token::Normal(NormalToken::Map),
diff --git a/src/merge.rs b/src/merge.rs
index f4276c6c..b1c5ffa7 100644
--- a/src/merge.rs
+++ b/src/merge.rs
@@ -54,7 +54,7 @@
 use crate::error::EvalError;
 use crate::eval::{Closure, Environment};
 use crate::position::TermPos;
-use crate::term::{BinaryOp, Contract, MetaValue, RichTerm, Term};
+use crate::term::{make as mk_term, BinaryOp, Contract, MetaValue, RichTerm, Term};
 use crate::transformations::Closurizable;
 use std::collections::HashMap;
 
@@ -362,7 +362,7 @@ fn cross_apply_contracts<'a>(
     let result = it2
         .fold(t1, |acc, ctr| {
             let ty_closure = ctr.types.clone().closurize(&mut env1_local, env2.clone());
-            RichTerm::new(Term::Assume(ty_closure, ctr.label.clone(), acc), pos)
+            mk_term::assume(ty_closure, ctr.label.clone(), acc).with_pos(pos)
         })
         .closurize(&mut env, env1_local);
 
diff --git a/src/operation.rs b/src/operation.rs
index d540272a..afefdce7 100644
--- a/src/operation.rs
+++ b/src/operation.rs
@@ -241,34 +241,6 @@ fn process_unary_operation(
                 ))
             }
         }
-        UnaryOp::ApplyContract() => {
-            match *t {
-                Term::Fun(..) => Ok(Closure {
-                    body: RichTerm { term: t, pos },
-                    env,
-                }),
-                Term::Record(..) => {
-                    let mut new_env = Environment::new();
-                    let closurized = RichTerm { term: t, pos }.closurize(&mut new_env, env);
-
-                    // Convert the record to the function `fun l x => contract & x`.
-                    let body = mk_fun!(
-                        "l",
-                        "x",
-                        mk_term::op2(BinaryOp::Merge(), closurized, mk_term::var("x"))
-                    )
-                    .with_pos(pos.into_inherited());
-
-                    Ok(Closure { body, env: new_env })
-                }
-                _ => Err(EvalError::TypeError(
-                    String::from("Function or record"),
-                    String::from("contract application"),
-                    arg_pos,
-                    RichTerm { term: t, pos },
-                )),
-            }
-        }
         UnaryOp::Embed(_id) => {
             if let en @ Term::Enum(_) = *t {
                 Ok(Closure::atomic_closure(RichTerm::new(en, pos_op_inh)))
@@ -876,17 +848,17 @@ fn process_binary_operation(
                 ))
             }
         }
-        BinaryOp::Pow() => {
-            if let Term::Num(n1) = *t1 {
-                if let Term::Num(n2) = *t2 {
+        BinaryOp::PlusStr() => {
+            if let Term::Str(s1) = *t1 {
+                if let Term::Str(s2) = *t2 {
                     Ok(Closure::atomic_closure(RichTerm::new(
-                        Term::Num(n1.powf(n2)),
+                        Term::Str(s1 + &s2),
                         pos_op_inh,
                     )))
                 } else {
                     Err(EvalError::TypeError(
-                        String::from("Num"),
-                        String::from("pow, 2nd argument"),
+                        String::from("Str"),
+                        String::from("++, 2nd argument"),
                         snd_pos,
                         RichTerm {
                             term: t2,
@@ -896,8 +868,8 @@ fn process_binary_operation(
                 }
             } else {
                 Err(EvalError::TypeError(
-                    String::from("Num"),
-                    String::from("pow, 1st argument"),
+                    String::from("Str"),
+                    String::from("++, 1st argument"),
                     fst_pos,
                     RichTerm {
                         term: t1,
@@ -906,32 +878,65 @@ fn process_binary_operation(
                 ))
             }
         }
-        BinaryOp::PlusStr() => {
-            if let Term::Str(s1) = *t1 {
-                if let Term::Str(s2) = *t2 {
-                    Ok(Closure::atomic_closure(RichTerm::new(
-                        Term::Str(s1 + &s2),
-                        pos_op_inh,
-                    )))
-                } else {
-                    Err(EvalError::TypeError(
-                        String::from("Str"),
-                        String::from("++, 2nd argument"),
-                        snd_pos,
+        BinaryOp::Assume() => {
+            if let Term::Lbl(mut l) = *t2 {
+                // Track the contract argument for better error reporting, and push back the label
+                // on the stack, so that it becomes the first argument of the contract.
+                let thunk = stack
+                    .track_arg()
+                    .ok_or_else(|| EvalError::NotEnoughArgs(3, String::from("assume"), pos_op))?;
+                l.arg_pos = thunk.borrow().body.pos;
+                l.arg_thunk = Some(thunk);
+
+                stack.push_arg(
+                    Closure::atomic_closure(RichTerm::new(Term::Lbl(l), pos2.into_inherited())),
+                    pos2.into_inherited(),
+                );
+
+                match *t1 {
+                    Term::Fun(..) => Ok(Closure {
+                        body: RichTerm {
+                            term: t1,
+                            pos: pos1,
+                        },
+                        env: env1,
+                    }),
+                    Term::Record(..) => {
+                        let mut new_env = Environment::new();
+                        let closurized = RichTerm {
+                            term: t1,
+                            pos: pos1,
+                        }
+                        .closurize(&mut new_env, env1);
+
+                        // Convert the record to the function `fun l x => contract & x`.
+                        let body = mk_fun!(
+                            "_l",
+                            "x",
+                            mk_term::op2(BinaryOp::Merge(), closurized, mk_term::var("x"))
+                        )
+                        .with_pos(pos1.into_inherited());
+
+                        Ok(Closure { body, env: new_env })
+                    }
+                    _ => Err(EvalError::TypeError(
+                        String::from("Function or Record"),
+                        String::from("assume, 1st argument"),
+                        fst_pos,
                         RichTerm {
-                            term: t2,
-                            pos: pos2,
+                            term: t1,
+                            pos: pos1,
                         },
-                    ))
+                    )),
                 }
             } else {
                 Err(EvalError::TypeError(
-                    String::from("Str"),
-                    String::from("++, 1st argument"),
-                    fst_pos,
+                    String::from("Label"),
+                    String::from("assume, 2nd argument"),
+                    snd_pos,
                     RichTerm {
-                        term: t1,
-                        pos: pos1,
+                        term: t2,
+                        pos: pos2,
                     },
                 ))
             }
diff --git a/src/parser/lexer.rs b/src/parser/lexer.rs
index 7820a182..647823b6 100644
--- a/src/parser/lexer.rs
+++ b/src/parser/lexer.rs
@@ -86,6 +86,8 @@ pub enum NormalToken<'input> {
     Equals,
     #[token("!=")]
     NotEquals,
+    #[token(";")]
+    SemiCol,
     #[token("&")]
     Ampersand,
     #[token(".")]
@@ -168,8 +170,6 @@ pub enum NormalToken<'input> {
     GoField,
     #[token("%goList%")]
     GoList,
-    #[token("%applyCtr%")]
-    ApplyContract,
 
     #[token("%wrap%")]
     Wrap,
@@ -191,8 +191,6 @@ pub enum NormalToken<'input> {
     Length,
     #[token("%fieldsOf%")]
     FieldsOf,
-    #[token("%pow%")]
-    Pow,
 
     #[token("%hasField%")]
     HasField,
diff --git a/src/program.rs b/src/program.rs
index 7103646d..a93a0bfa 100644
--- a/src/program.rs
+++ b/src/program.rs
@@ -264,7 +264,8 @@ mod tests {
         assert_eq!(t, *expd.term);
 
         let t = clean_pos(
-            eval_full("let x = 1 in let y = 1 + x in let z = {foo.bar.baz = y} in z").unwrap(),
+            eval_full("let x = 1 in let y = 1 + x in let z = { foo = {bar = { baz  = y } } } in z")
+                .unwrap(),
         );
         // Records are parsed as RecRecords, so we need to build one by hand
         let expd = mk_record!((
@@ -277,6 +278,6 @@ mod tests {
         // Check that substitution do not replace bound variables. Before the fixing commit, this
         // example would go into an infinite loop, and stack overflow. If it does, this just means
         // that this test fails.
-        eval_full("{y = fun x => x, x = fun y => y}").unwrap();
+        eval_full("{y = fun x => x; x = fun y => y}").unwrap();
     }
 }
diff --git a/src/serialize.rs b/src/serialize.rs
index 54f09c16..6c004b1d 100644
--- a/src/serialize.rs
+++ b/src/serialize.rs
@@ -334,7 +334,7 @@ mod tests {
     #[test]
     fn records() {
         assert_json_eq!(
-            "{a = 1, b = 2+2, c = 3, d = null}",
+            "{a = 1; b = 2+2; c = 3; d = null}",
             json!({"a": 1, "b": 4, "c": 3, "d": null})
         );
 
@@ -344,15 +344,15 @@ mod tests {
         );
 
         assert_json_eq!(
-            "{foo = let z = 0.5 + 0.5 in z, bar = [\"str\", true || false], baz = {subfoo = !false} & {subbar = 1 - 1}}",
+            "{foo = let z = 0.5 + 0.5 in z; bar = [\"str\", true || false]; baz = {subfoo = !false} & {subbar = 1 - 1}}",
             json!({"foo": 1, "bar": ["str", true], "baz": {"subfoo": true, "subbar": 0}})
         );
     }
 
     #[test]
-    fn meta_values() {
+    fn enriched_values() {
         assert_json_eq!(
-            "{a | default = 1, b | doc \"doc\" = 2+2, c = 3}",
+            "{a | default = 1; b | doc \"doc\" = 2+2; c = 3}",
             json!({"a": 1, "b": 4, "c": 3})
         );
 
@@ -369,10 +369,10 @@ mod tests {
 
     #[test]
     fn prevalidation() {
-        assert_pass_validation!(ExportFormat::Json, "{a = 1, b = {c = fun x => x}}", false);
+        assert_pass_validation!(ExportFormat::Json, "{a = 1; b = { c = fun x => x }}", false);
         assert_pass_validation!(
             ExportFormat::Json,
-            "{foo.bar = let y = \"a\" in y, b = [[fun x => x]]}",
+            "{foo = { bar = let y = \"a\" in y}; b = [[fun x => x]] }",
             false
         );
         assert_pass_validation!(ExportFormat::Json, "{foo = null}", true);
@@ -384,6 +384,8 @@ mod tests {
         assert_involutory!("{val = 1 + 1}");
         assert_involutory!("{val = \"Some string\"}");
         assert_involutory!("{val = [\"a\", 3, []]}");
-        assert_involutory!("{a.foo.bar = \"2\", b = false, c = [{d = \"e\"}, {d = \"f\"}]}");
+        assert_involutory!(
+            "{a = {foo = {bar = \"2\"}}; b = false; c = [{d = \"e\"}, {d = \"f\"}]}"
+        );
     }
 }
diff --git a/src/stack.rs b/src/stack.rs
index 4127679a..89a6658a 100644
--- a/src/stack.rs
+++ b/src/stack.rs
@@ -262,6 +262,21 @@ impl Stack {
     pub fn clear_eqs(&mut self) {
         while self.pop_eq().is_some() {}
     }
+
+    /// Turning the top element of the stack into a tracked arg if it was not already. Returns the
+    /// corresponding thunk, or `None` if the top element wasn't an argument.
+    pub fn track_arg(&mut self) -> Option<Thunk> {
+        match self.0.last_mut() {
+            Some(Marker::TrackedArg(thunk, _)) => Some(thunk.clone()),
+            Some(Marker::Arg(..)) => {
+                let (closure, pos) = self.pop_arg().unwrap();
+                let thunk = Thunk::new(closure, IdentKind::Lam());
+                self.push_tracked_arg(thunk.clone(), pos);
+                Some(thunk)
+            }
+            _ => None,
+        }
+    }
 }
 
 #[cfg(test)]
diff --git a/src/stdlib.rs b/src/stdlib.rs
index 89e5d7fb..4ce0f371 100644
--- a/src/stdlib.rs
+++ b/src/stdlib.rs
@@ -13,11 +13,10 @@ pub const CONTRACTS: (&str, &str) = (
 );
 pub const LISTS: (&str, &str) = ("<stdlib/lists>", include_str!("../stdlib/lists.ncl"));
 pub const RECORDS: (&str, &str) = ("<stdlib/records>", include_str!("../stdlib/records.ncl"));
-pub const NUMS: (&str, &str) = ("<stdlib/nums>", include_str!("../stdlib/nums.ncl"));
 
 /// Return the list `(name, source_code)` of all the stdlib modules.
 pub fn modules() -> Vec<(&'static str, &'static str)> {
-    vec![BUILTINS, CONTRACTS, LISTS, RECORDS, NUMS]
+    vec![BUILTINS, CONTRACTS, LISTS, RECORDS]
 }
 
 /// Accessors to the builtin contracts.
diff --git a/src/term.rs b/src/term.rs
index 8f734c43..3616533b 100644
--- a/src/term.rs
+++ b/src/term.rs
@@ -104,14 +104,6 @@ pub enum Term {
     #[serde(skip)]
     Promise(Types, Label, RichTerm),
 
-    /// An assume.
-    ///
-    /// Represent a subterm which is to be dynamically typechecked (dynamic types are also called.
-    /// It ensures at runtime that the term satisfies the contract corresponding to the type, or it
-    /// will blame the label instead.
-    #[serde(skip)]
-    Assume(Types, Label, RichTerm),
-
     /// A symbol.
     ///
     /// A unique tag corresponding to a type variable. See `Wrapped` below.
@@ -298,7 +290,6 @@ impl Term {
             Fun(_, ref mut t)
             | Op1(_, ref mut t)
             | Promise(_, _, ref mut t)
-            | Assume(_, _, ref mut t)
             | Wrapped(_, ref mut t) => {
                 func(t);
             }
@@ -354,7 +345,6 @@ impl Term {
             | Term::Op1(_, _)
             | Term::Op2(_, _, _)
             | Term::Promise(_, _, _)
-            | Term::Assume(_, _, _)
             | Term::Import(_)
             | Term::ResolvedImport(_)
             | Term::StrChunks(_) => None,
@@ -419,7 +409,6 @@ impl Term {
             | Term::Op1(_, _)
             | Term::Op2(_, _, _)
             | Term::Promise(_, _, _)
-            | Term::Assume(_, _, _)
             | Term::Import(_)
             | Term::ResolvedImport(_) => String::from("<unevaluated>"),
         }
@@ -445,7 +434,6 @@ impl Term {
             | Term::Op1(_, _)
             | Term::Op2(_, _, _)
             | Term::Promise(_, _, _)
-            | Term::Assume(_, _, _)
             | Term::Wrapped(_, _)
             | Term::MetaValue(_)
             | Term::Import(_)
@@ -483,7 +471,6 @@ impl Term {
             | Term::Op1(_, _)
             | Term::Op2(_, _, _)
             | Term::Promise(_, _, _)
-            | Term::Assume(_, _, _)
             | Term::Wrapped(_, _)
             | Term::MetaValue(_)
             | Term::Import(_)
@@ -531,13 +518,6 @@ pub enum UnaryOp {
 
     /// Raise a blame, which stops the execution and prints an error according to the label argument.
     Blame(),
-    /// Apply a contract to a label and a value. The label and the value are stored on the stack, unevaluated.
-    ///
-    /// Operationally equivalent to the standard application for contracts given as functions, this
-    /// operator additionally marks the location of the tested value for better error reporting. It
-    /// also accepts contracts as records, which are translated to a merge operation instead of
-    /// function application.
-    ApplyContract(),
 
     /// Typecast an enum to a larger enum type.
     ///
@@ -636,8 +616,6 @@ pub enum BinaryOp {
     Div(),
     /// Modulo of numerals.
     Modulo(),
-    /// Raise a number to a power.
-    Pow(),
     /// Concatenation of strings.
     PlusStr(),
     /// Polymorphic equality.
@@ -650,6 +628,14 @@ pub enum BinaryOp {
     GreaterThan(),
     /// Greater than or equal comparison operator.
     GreaterOrEq(),
+    /// An assume.
+    ///
+    /// Apply a contract to a label and a value. The value is is stored on the stack unevaluated,
+    /// while the contract and the label are the strict arguments to this operator. Assume also
+    /// accepts contracts as records, that are translates to a function that performs a merge
+    /// operation with its argument. Finally, this operator marks the location of the contract
+    /// argument for better error reporting.
+    Assume(),
     /// Unwrap a tagged term.
     ///
     /// See `Wrap` in [`UnaryOp`](enum.UnaryOp.html).
@@ -838,16 +824,6 @@ impl RichTerm {
                     state,
                 )
             }
-            Term::Assume(ty, l, t) => {
-                let t = t.traverse(f, state)?;
-                f(
-                    RichTerm {
-                        term: Box::new(Term::Assume(ty, l, t)),
-                        pos,
-                    },
-                    state,
-                )
-            }
             Term::Wrapped(i, t) => {
                 let t = t.traverse(f, state)?;
                 f(
@@ -1105,6 +1081,16 @@ pub mod make {
         Term::Op2(op, t1.into(), t2.into()).into()
     }
 
+    pub fn assume<T>(types: Types, l: Label, t: T) -> RichTerm
+    where
+        T: Into<RichTerm>,
+    {
+        mk_app!(
+            op2(BinaryOp::Assume(), types.contract(), Term::Lbl(l)),
+            t.into()
+        )
+    }
+
     pub fn string<S>(s: S) -> RichTerm
     where
         S: Into<String>,
diff --git a/src/transformations.rs b/src/transformations.rs
index 326b35e8..10133b2b 100644
--- a/src/transformations.rs
+++ b/src/transformations.rs
@@ -224,6 +224,7 @@ pub mod import_resolution {
 /// value is unwrapped.
 pub mod apply_contracts {
     use super::{RichTerm, Term};
+    use crate::mk_app;
 
     /// If the top-level node of the AST is a meta-value, wrap the inner value inside generated
     /// `Assume`s corresponding to the meta-value's contracts. Otherwise, return the term
@@ -236,7 +237,12 @@ pub mod apply_contracts {
                 let inner = meta.types.iter().chain(meta.contracts.iter()).fold(
                     meta.value.take().unwrap(),
                     |acc, ctr| {
-                        RichTerm::new(Term::Assume(ctr.types.clone(), ctr.label.clone(), acc), pos)
+                        mk_app!(
+                            ctr.types.clone().contract(),
+                            Term::Lbl(ctr.label.clone()),
+                            acc
+                        )
+                        .with_pos(pos)
                     },
                 );
 
@@ -316,7 +322,7 @@ where
 }
 
 /// Generate a new fresh variable which do not clash with user-defined variables.
-fn fresh_var() -> Ident {
+pub fn fresh_var() -> Ident {
     Ident(format!("%{}", FreshVarCounter::next()))
 }
 
diff --git a/src/typecheck.rs b/src/typecheck.rs
index 54e14b0a..73b8b0da 100644
--- a/src/typecheck.rs
+++ b/src/typecheck.rs
@@ -673,42 +673,26 @@ fn type_check_(
             type_check_(state, envs.clone(), strict, e, src1)?;
             type_check_(state, envs, strict, t, src2)
         }
-        Term::Promise(ty2, _, t) => {
-            let tyw2 = to_typewrapper(ty2.clone());
-
-            let instantiated = instantiate_foralls(state, tyw2, ForallInst::Constant);
-
-            unify(state, strict, ty, to_typewrapper(ty2.clone()))
-                .map_err(|err| err.into_typecheck_err(state, rt.pos))?;
-            type_check_(state, envs, true, t, instantiated)
-        }
-        Term::Assume(ty2, _, t) => {
-            unify(state, strict, ty, to_typewrapper(ty2.clone()))
-                .map_err(|err| err.into_typecheck_err(state, rt.pos))?;
-            let new_ty = TypeWrapper::Ptr(new_var(state.table));
-            type_check_(state, envs, false, t, new_ty)
-        }
-        Term::Sym(_) => unify(state, strict, ty, mk_typewrapper::sym())
-            .map_err(|err| err.into_typecheck_err(state, rt.pos)),
-        Term::Wrapped(_, t) => type_check_(state, envs, strict, t, ty),
+        Term::Promise(ty2, _, t)
         // A non-empty metavalue with a type annotation is a promise.
-        Term::MetaValue(MetaValue {
+        | Term::MetaValue(MetaValue {
             types: Some(Contract { types: ty2, .. }),
             value: Some(t),
             ..
         }) => {
             let tyw2 = to_typewrapper(ty2.clone());
+
             let instantiated = instantiate_foralls(state, tyw2, ForallInst::Constant);
 
             unify(state, strict, ty, to_typewrapper(ty2.clone()))
                 .map_err(|err| err.into_typecheck_err(state, rt.pos))?;
             type_check_(state, envs, true, t, instantiated)
         }
-        // A non-empty metavalue with at least one contract is an assume. If there's several
+        // A metavalue with at least one contract is an assume. If there's several
         // contracts, we arbitrarily chose the first one as the type annotation.
         Term::MetaValue(MetaValue {
             contracts,
-            value: Some(t),
+            value,
             ..
         }) if !contracts.is_empty() => {
             let ctr = contracts.get(0).unwrap();
@@ -716,13 +700,30 @@ fn type_check_(
 
             unify(state, strict, ty, to_typewrapper(ty2.clone()))
                 .map_err(|err| err.into_typecheck_err(state, rt.pos))?;
-            type_check_(state, envs, false, t, mk_typewrapper::dynamic())
+
+            // if there's an inner value, we have to recursively typecheck it, but in non strict
+            // mode.
+            if let Some(t) = value {
+                type_check_(state, envs, false, t, mk_typewrapper::dynamic())
+            }
+            else {
+                Ok(())
+            }
         }
-        // A metavalue without a type or contract annotation is typechecked in the same way as its inner value
+        Term::Sym(_) => unify(state, strict, ty, mk_typewrapper::sym())
+            .map_err(|err| err.into_typecheck_err(state, rt.pos)),
+        Term::Wrapped(_, t) => type_check_(state, envs, strict, t, ty),
+        // A non-empty metavalue without a type or contract annotation is typechecked in the same way as its inner value
         Term::MetaValue(MetaValue { value: Some(t), .. }) => {
             type_check_(state, envs, strict, t, ty)
         }
-        Term::MetaValue(_) => Ok(()),
+        // A metavalue without a body nor a type annotation is a record field without definition.
+        // This should probably be non representable in the syntax, as it doesn't really make
+        // sense. In any case, we infer it to be of type `Dyn` for now.
+        Term::MetaValue(_) => {
+             unify(state, strict, ty, mk_typewrapper::dynamic())
+                .map_err(|err| err.into_typecheck_err(state, rt.pos))
+        },
         Term::Import(_) => unify(state, strict, ty, mk_typewrapper::dynamic())
             .map_err(|err| err.into_typecheck_err(state, rt.pos)),
         Term::ResolvedImport(file_id) => {
@@ -811,12 +812,12 @@ impl Into<TypeWrapper> for ApparentType {
 ///   the future, such as `Dyn -> Dyn` for functions, `{ | Dyn}` for records, and so on).
 pub fn apparent_type(t: &Term, envs: Option<&Envs>) -> ApparentType {
     match t {
-        Term::Assume(ty, _, _) | Term::Promise(ty, _, _) => ApparentType::Annotated(ty.clone()),
-        // For metavalues, chose first the type annotation if any, or the first contract appearing.
-        Term::MetaValue(MetaValue {
-            types: Some(ty_ctr),
+        Term::Promise(ty, _, _)
+        | Term::MetaValue(MetaValue {
+            types: Some(Contract { types: ty, .. }),
             ..
-        }) => ApparentType::Annotated(ty_ctr.types.clone()),
+        }) => ApparentType::Annotated(ty.clone()),
+        // For metavalues, if there's no type annotation, choose the first contract appearing.
         Term::MetaValue(MetaValue { contracts, .. }) if !contracts.is_empty() => {
             ApparentType::Annotated(contracts.get(0).unwrap().types.clone())
         }
@@ -1533,8 +1534,6 @@ pub fn get_uop_type(state: &mut State, op: &UnaryOp) -> Result<TypeWrapper, Type
 
             mk_tyw_arrow!(AbsType::Dyn(), res)
         }
-        // This should not happen, as `ApplyContract()` is only produced during evaluation.
-        UnaryOp::ApplyContract() => panic!("cannot typecheck ApplyContract()"),
         // Dyn -> Bool
         UnaryOp::Pol() => mk_tyw_arrow!(AbsType::Dyn(), AbsType::Bool()),
         // forall rows. < | rows> -> <id | rows>
@@ -1631,6 +1630,8 @@ pub fn get_bop_type(state: &mut State, op: &BinaryOp) -> Result<TypeWrapper, Typ
         // Str -> Str -> Str
         BinaryOp::PlusStr() => mk_tyw_arrow!(AbsType::Str(), AbsType::Str(), AbsType::Str()),
         // Sym -> Dyn -> Dyn -> Dyn
+        // This should not happen, as `ApplyContract()` is only produced during evaluation.
+        BinaryOp::Assume() => panic!("cannot typecheck assume"),
         BinaryOp::Unwrap() => mk_tyw_arrow!(
             AbsType::Sym(),
             AbsType::Dyn(),
@@ -1721,11 +1722,6 @@ pub fn get_bop_type(state: &mut State, op: &BinaryOp) -> Result<TypeWrapper, Typ
             mk_typewrapper::str(),
             mk_typewrapper::dynamic()
         ),
-        BinaryOp::Pow() => mk_tyw_arrow!(
-            mk_typewrapper::num(),
-            mk_typewrapper::num(),
-            mk_typewrapper::num()
-        ),
     })
 }
 
diff --git a/src/types.rs b/src/types.rs
index cdd41e90..1f94cec3 100644
--- a/src/types.rs
+++ b/src/types.rs
@@ -53,7 +53,7 @@
 //! untyped parts.
 use crate::identifier::Ident;
 use crate::term::make as mk_term;
-use crate::term::{RichTerm, Term, UnaryOp};
+use crate::term::{BinaryOp, RichTerm, Term, UnaryOp};
 use crate::{mk_app, mk_fun};
 use std::collections::HashMap;
 use std::fmt;
@@ -179,14 +179,15 @@ impl Types {
         sy: &mut i32,
     ) -> RichTerm {
         use crate::stdlib::contracts;
+        use crate::transformations::fresh_var;
 
-        match self.0 {
+        let ctr = match self.0 {
             AbsType::Dyn() => contracts::dynamic(),
             AbsType::Num() => contracts::num(),
             AbsType::Bool() => contracts::bool(),
             AbsType::Str() => contracts::string(),
             //TODO: optimization: have a specialized contract for `List Dyn`, to avoid mapping an
-            //always succesful contract on each element.
+            //always successful contract on each element.
             AbsType::List(ref ty) => mk_app!(contracts::list(), ty.contract_open(h, pol, sy)),
             AbsType::Sym() => panic!("Are you trying to check a Sym at runtime?"),
             AbsType::Arrow(ref s, ref t) => mk_app!(
@@ -194,9 +195,7 @@ impl Types {
                 s.contract_open(h.clone(), !pol, sy),
                 t.contract_open(h, pol, sy)
             ),
-            AbsType::Flat(ref t) => {
-                mk_term::op1(UnaryOp::ApplyContract(), t.clone()).with_pos(t.pos)
-            }
+            AbsType::Flat(ref t) => t.clone(),
             AbsType::Var(ref i) => {
                 let (rt, _) = h
                     .get(i)
@@ -288,7 +287,24 @@ impl Types {
             AbsType::DynRecord(ref ty) => {
                 mk_app!(contracts::dyn_record(), ty.contract_open(h, pol, sy))
             }
-        }
+        };
+
+        // To track the argument to contracts and support contracts as record, we need to wrap the
+        // function contracts as an `Assume`. Since `Assume` is strict in the label and need to be
+        // fully applied, we need to wrap the whole expression back as a standard function, that is
+        // to form: `fun l val => %assume% ctr l val`
+        let var_l = fresh_var();
+        let var_val = fresh_var();
+        let pos = ctr.pos;
+        mk_fun!(
+            var_l.clone(),
+            var_val.clone(),
+            mk_app!(
+                mk_term::op2(BinaryOp::Assume(), ctr, Term::Var(var_l)),
+                Term::Var(var_val)
+            )
+        )
+        .with_pos(pos.into_inherited())
     }
 
     /// Find a binding in a record row type. Return `None` if there is no such binding, if the type
diff --git a/stdlib/builtins.ncl b/stdlib/builtins.ncl
index 27615dc1..a7a1188c 100644
--- a/stdlib/builtins.ncl
+++ b/stdlib/builtins.ncl
@@ -1,11 +1,11 @@
 {
   builtins = {
-    isNum : Dyn -> Bool = fun x => %isNum% x,
-    isBool : Dyn -> Bool = fun x => %isBool% x,
-    isStr : Dyn -> Bool = fun x => %isStr% x,
-    isFun : Dyn -> Bool = fun x => %isFun% x,
-    isList : Dyn -> Bool = fun x => %isList% x,
-    isRecord : Dyn -> Bool = fun x => %isRecord% x,
+    isNum : Dyn -> Bool = fun x => %isNum% x;
+    isBool : Dyn -> Bool = fun x => %isBool% x;
+    isStr : Dyn -> Bool = fun x => %isStr% x;
+    isFun : Dyn -> Bool = fun x => %isFun% x;
+    isList : Dyn -> Bool = fun x => %isList% x;
+    isRecord : Dyn -> Bool = fun x => %isRecord% x;
     typeOf : Dyn -> <
       TypeNum,
       TypeBool,
@@ -20,20 +20,20 @@
       else if %isFun% x then `TypeFun
       else if %isList% x then `TypeList
       else if %isRecord% x then `TypeRecord
-      else `Other,
+      else `Other;
 
-    seq : forall a. Dyn -> a -> a = fun x y => %seq% x y,
-    deepSeq : forall a. Dyn -> a -> a = fun x y => %deepSeq% x y,
+    seq : forall a. Dyn -> a -> a = fun x y => %seq% x y;
+    deepSeq : forall a. Dyn -> a -> a = fun x y => %deepSeq% x y;
 
-    id : forall a. a -> a = fun x => x,
+    id : forall a. a -> a = fun x => x;
 
     hash : <Md5, Sha1, Sha256, Sha512> -> Str -> Str =
-      fun type s => %hash% type s,
+      fun type s => %hash% type s;
 
     serialize : <Json, Toml, Yaml> -> Dyn -> Str = fun format x =>
-      %serialize% format (%deepSeq% x x),
+      %serialize% format (%deepSeq% x x);
 
     deserialize : <Json, Toml, Yaml> -> Str -> Dyn = fun format x =>
-      %deserialize% format x,
+      %deserialize% format x;
   }
 }
diff --git a/stdlib/contracts.ncl b/stdlib/contracts.ncl
index 1a952575..68ec43e5 100644
--- a/stdlib/contracts.ncl
+++ b/stdlib/contracts.ncl
@@ -1,46 +1,46 @@
 {
-  dyn = fun l t => t,
+  dyn = fun l t => t;
 
-  num = fun l t => if %isNum% t then t else %blame% l,
+  num = fun l t => if %isNum% t then t else %blame% l;
 
-  bool = fun l t => if %isBool% t then t else %blame% l,
+  bool = fun l t => if %isBool% t then t else %blame% l;
 
-  string = fun l t => if %isStr% t then t else %blame% l,
+  string = fun l t => if %isStr% t then t else %blame% l;
 
-  list = fun elt l t => if %isList% t then %map% t (elt (%goList% l)) else %blame% l,
+  list = fun elt l t => if %isList% t then %map% t (elt (%goList% l)) else %blame% l;
 
   func = fun s t l e =>
       if %isFun% e then
           (fun x => t (%goCodom% l) (e (s (%chngPol% (%goDom% l)) x)))
       else
-          %blame% l,
+          %blame% l;
 
   forall_var = fun sy pol l t =>
       let lPol = %polarity% l in
       if pol == lPol then
           %unwrap% sy t (%blame% l)
       else
-          %wrap% sy t,
+          %wrap% sy t;
 
-  fail = fun l t => %blame% (%tag% "Fail" l),
+  fail = fun l t => %blame% (%tag% "Fail" l);
 
   row_extend = fun contr case l t =>
       if (case t) then
           t
       else
-          contr (%tag% "NotRowExt" l) t,
+          contr (%tag% "NotRowExt" l) t;
 
   record = fun cont l t =>
       if %isRecord% t then
           cont {} l t
       else
-          %blame% (%tag% "not a record" l),
+          %blame% (%tag% "not a record" l);
 
   dyn_record = fun contr l t =>
       if %isRecord% t then
           %recordMap% t (fun _field => contr l)
       else
-          %blame% (%tag% "not a record" l),
+          %blame% (%tag% "not a record" l);
 
   record_extend = fun field contr cont acc l t =>
       if %hasField% field t then
@@ -48,7 +48,7 @@
           let t = t -$ field in
           cont acc l t
       else
-          %blame% (%tag% "missing field `#{field}`" l),
+          %blame% (%tag% "missing field `#{field}`" l);
 
   forall_tail = fun sy pol acc l t =>
       let magic_fld = "_%wrapped" in
@@ -64,16 +64,16 @@
           else
               %blame% (%tag% "missing polymorphic part" l)
       else
-          acc$[magic_fld = %wrap% sy t],
+          acc$[magic_fld = %wrap% sy t];
 
-  dyn_tail = fun acc l t => acc & t,
+  dyn_tail = fun acc l t => acc & t;
 
   empty_tail = fun acc l t =>
       if t == {} then acc
-      else %blame% (%tag% "extra field `#{%head% (%fieldsOf% t)}`" l),
+      else %blame% (%tag% "extra field `#{%head% (%fieldsOf% t)}`" l);
 
   contracts = {
-    blame = fun l => %blame% l,
-    tag = fun msg l => %tag% msg l,
-  },
+    blame = fun l => %blame% l;
+    tag = fun msg l => %tag% msg l;
+  };
 }
diff --git a/stdlib/lists.ncl b/stdlib/lists.ncl
index d3ec025a..0ad2c076 100644
--- a/stdlib/lists.ncl
+++ b/stdlib/lists.ncl
@@ -1,16 +1,16 @@
 {
   lists = {
-    head : forall a. List a -> a = fun l => %head% l,
+    head : forall a. List a -> a = fun l => %head% l;
 
-    tail : forall a. List a -> List a = fun l => %tail% l,
+    tail : forall a. List a -> List a = fun l => %tail% l;
 
-    length : forall a. List a -> Num = fun l => %length% l,
+    length : forall a. List a -> Num = fun l => %length% l;
 
-    map : forall a b. (a -> b) -> List a -> List b = fun f l => %map% l f,
+    map : forall a b. (a -> b) -> List a -> List b = fun f l => %map% l f;
 
-    elemAt : forall a. List a -> Num -> a = fun l n => %elemAt% l n,
+    elemAt : forall a. List a -> Num -> a = fun l n => %elemAt% l n;
 
-    concat : forall a. List a -> List a -> List a = fun l1 l2 => l1 @ l2,
+    concat : forall a. List a -> List a -> List a = fun l1 l2 => l1 @ l2;
 
     foldl : forall a b. (a -> b -> a) -> a -> List b -> a =
       fun f fst l =>
@@ -18,33 +18,33 @@
           fst
         else
           let rest = foldl f fst (%tail% l) in
-          %seq% rest (f rest (%head% l)),
+          %seq% rest (f rest (%head% l));
 
     fold : forall a b. (a -> b -> b) -> List a -> b -> b =
       fun f l fst =>
         if %length% l == 0 then
           fst
         else
-          f (%head% l) (fold f (%tail% l) fst),
+          f (%head% l) (fold f (%tail% l) fst);
 
-    cons : forall a. a -> List a -> List a = fun x l => [x] @ l,
+    cons : forall a. a -> List a -> List a = fun x l => [x] @ l;
 
     filter : forall a. (a -> Bool) -> List a -> List a =
       fun pred l =>
-        fold (fun x acc => if pred x then acc @ [x] else acc) l [],
+        fold (fun x acc => if pred x then acc @ [x] else acc) l [];
 
     //TODO: this enforces a List contract at each iteration. Get rid of it once
     //parametrized list types lands and `fold` get a more precise type.
     flatten : forall a. List (List a) -> List a =
       fun l =>
-        fold (fun l acc => l @ acc) l [],
+        fold (fun l acc => l @ acc) l [];
 
     all : forall a. (a -> Bool) -> List a -> Bool =
       fun pred l =>
-        fold (fun x acc => if pred x then acc else false) l true,
+        fold (fun x acc => if pred x then acc else false) l true;
 
     any : forall a. (a -> Bool) -> List a -> Bool =
       fun pred l =>
-        fold (fun x acc => if pred x then true else acc) l false,
+        fold (fun x acc => if pred x then true else acc) l false;
   }
 }
diff --git a/stdlib/nums.ncl b/stdlib/nums.ncl
deleted file mode 100644
index d8f12f9c..00000000
--- a/stdlib/nums.ncl
+++ /dev/null
@@ -1,64 +0,0 @@
-{
-  nums = {
-    Int = fun label value =>
-      if %isNum% value then
-        if value % 1 == 0 then
-          value
-        else
-          %blame% (%tag% "not an integer" label)
-      else
-        %blame% (%tag% "not a number" label),
-
-    Nat = fun label value =>
-      if %isNum% value then
-        if value % 1 == 0 && value >= 0 then
-          value
-        else
-          %blame% (%tag% "not a natural" label)
-      else
-        %blame% (%tag% "not a number" label),
-
-    PosNat = fun label value =>
-      if %isNum% value then
-        if value % 1 == 0 && value > 0 then
-          value
-        else
-          %blame% (%tag% "not positive integer" label)
-      else
-        %blame% (%tag% "not a number" label),
-
-    NonZero = fun label value =>
-      if %isNum% value then
-        if value != 0 then
-          value
-        else
-          %blame% (%tag% "non-zero" label)
-      else
-        %blame% (%tag% "not a number" label),
-
-    isInt : Num -> Bool = fun x =>
-      %isNum% x && (x % 1 == 0),
-
-    min : Num -> Num -> Num = fun x y =>
-      if x <= y then x else y,
-
-    max : Num -> Num -> Num = fun x y =>
-      if x >= y then x else y,
-
-    floor : Num -> Num = fun x =>
-      if x >= 0 then x - (x % 1)
-      else x - 1 - (x % 1),
-
-    abs : Num -> Num = fun x =>
-      if x < 0 then -x else x,
-
-    fract : Num -> Num = fun x =>
-      x % 1,
-
-    trunc : Num -> Num = fun x =>
-      x - (x % 1),
-
-    pow : Num -> Num -> Num = fun x n =>
-      %pow% x n,
-  }
-}
diff --git a/stdlib/records.ncl b/stdlib/records.ncl
index 42b850c8..8349657c 100644
--- a/stdlib/records.ncl
+++ b/stdlib/records.ncl
@@ -1,10 +1,10 @@
 {
   records = {
-    map : forall a b. (Str -> a -> b) -> {_: a} -> {_: b} = fun f r => %recordMap% r f,
+    map : forall a b. (Str -> a -> b) -> {_: a} -> {_: b} = fun f r => %recordMap% r f;
 
     // TODO: change Dyn to { | Dyn} once the PR introducing open contracts lands
-    fieldsOf : Dyn -> List Str = fun r => %fieldsOf% r,
+    fieldsOf : Dyn -> List Str = fun r => %fieldsOf% r;
 
-    hasField : Str -> Dyn -> Bool = fun r field => %hasField% r field,
+    hasField : Str -> Dyn -> Bool = fun r field => %hasField% r field;
   }
 }


Test patch:
diff --git a/src/parser/tests.rs b/src/parser/tests.rs
index d9c0e39d..c4f8695e 100644
--- a/src/parser/tests.rs
+++ b/src/parser/tests.rs
@@ -163,7 +163,7 @@ fn enum_terms() {
 #[test]
 fn record_terms() {
     assert_eq!(
-        parse_without_pos("{ a = 1, b = 2, c = 3}"),
+        parse_without_pos("{ a = 1; b = 2; c = 3;}"),
         RecRecord(
             vec![
                 (Ident::from("a"), Num(1.).into()),
@@ -177,7 +177,7 @@ fn record_terms() {
     );
 
     assert_eq!(
-        parse_without_pos("{ a = 1, \"#{123}\" = (if 4 then 5 else 6), d = 42}"),
+        parse_without_pos("{ a = 1; \"#{123}\" = (if 4 then 5 else 6); d = 42;}"),
         mk_app!(
             mk_term::op2(
                 BinaryOp::DynExtend(),
@@ -336,7 +336,7 @@ fn line_comments() {
     assert_eq!(
         parse_without_pos(
             "{ // Some comment
-            field = foo, // Some description
+            field = foo; // Some description
             } // Some other"
         ),
         parse_without_pos("{field = foo}")
diff --git a/tests/contracts_fail.rs b/tests/contracts_fail.rs
index 23258e22..dd3e4084 100644
--- a/tests/contracts_fail.rs
+++ b/tests/contracts_fail.rs
@@ -60,7 +60,7 @@ fn merge_compose_contract() {
             "let Even = fun l x => if x % 2 == 0 then x else %blame% l in
         let DivBy3 = fun l x => if x % 3 ==  0 then x else %blame% l in
         let composed = {{a | #Even}} & {{a | #DivBy3}} in
-        (({{a = {},}}) & composed).a",
+        (({{a = {};}}) & composed).a",
             arg
         )
     };
@@ -76,21 +76,21 @@ fn merge_compose_contract() {
 fn records_contracts_simple() {
     assert_raise_blame!("{a=1} | {}");
 
-    assert_raise_blame!("let x | {a: Num, s: Str} = {a = 1, s = 2} in %deepSeq% x x");
-    assert_raise_blame!("let x | {a: Num, s: Str} = {a = \"a\", s = \"b\"} in %deepSeq% x x");
+    assert_raise_blame!("let x | {a: Num, s: Str} = {a = 1; s = 2} in %deepSeq% x x");
+    assert_raise_blame!("let x | {a: Num, s: Str} = {a = \"a\"; s = \"b\"} in %deepSeq% x x");
     assert_raise_blame!("let x | {a: Num, s: Str} = {a = 1} in %deepSeq% x x");
     assert_raise_blame!("let x | {a: Num, s: Str} = {s = \"a\"} in %deepSeq% x x");
     assert_raise_blame!(
-        "let x | {a: Num, s: Str} = {a = 1, s = \"a\", extra = 1} in %deepSeq% x x"
+        "let x | {a: Num, s: Str} = {a = 1; s = \"a\"; extra = 1} in %deepSeq% x x"
     );
 
     assert_raise_blame!(
-        "let x | {a: Num, s: {foo: Bool}} = {a = 1, s = {foo = 2}} in %deepSeq% x x"
+        "let x | {a: Num, s: {foo: Bool}} = {a = 1; s = {foo = 2}} in %deepSeq% x x"
     );
     assert_raise_blame!(
-        "let x | {a: Num, s: {foo: Bool}} = {a = 1, s = {foo = true, extra = 1}} in %deepSeq% x x"
+        "let x | {a: Num, s: {foo: Bool}} = {a = 1; s = {foo = true; extra = 1}} in %deepSeq% x x"
     );
-    assert_raise_blame!("let x | {a: Num, s: {foo: Bool}} = {a = 1, s = {}} in %deepSeq% x x");
+    assert_raise_blame!("let x | {a: Num, s: {foo: Bool}} = {a = 1; s = {}} in %deepSeq% x x");
 }
 
 #[test]
@@ -103,7 +103,7 @@ fn records_contracts_poly() {
     assert_raise_blame!(&format!("{} {{}}", remv));
 
     let bad_cst = "let f | forall a. { | a} -> { | a} = fun x => {a=1} in f";
-    let bad_acc = "let f | forall a. { | a} -> { | a} = fun x => %seq% x.a x in f";
+    let bad_acc = "let f | forall a. { | a} -> { | a} = fun x => %seq% (x.a) x in f";
     let bad_extd = "let f | forall a. { | a} -> {foo: Num | a} = fun x => x-$\"foo\" in f";
     let bad_rmv = "let f | forall a. {foo: Num | a} -> { | a} = fun x => x$[\"foo\"=1] in f";
 
@@ -126,7 +126,7 @@ fn records_contracts_poly() {
                 -> {a: Num | a}
                 -> { | a}
             = fun f rec => (f rec) -$ \"a\" -$ \"b\" in
-        f (fun x => x) {a = 1, b = true, c = 3}"
+        f (fun x => x) {a = 1; b = true; c = 3}"
     );
 }
 
diff --git a/tests/infinite_rec.rs b/tests/infinite_rec.rs
index c1ac5995..0216de3d 100644
--- a/tests/infinite_rec.rs
+++ b/tests/infinite_rec.rs
@@ -11,15 +11,15 @@ fn infinite_loops() {
         Err(Error::EvalError(EvalError::InfiniteRecursion(..)))
     );
     assert_matches!(
-        eval("{x = y, y = z, z = x }.x"),
+        eval("{x = y; y = z; z = x }.x"),
         Err(Error::EvalError(EvalError::InfiniteRecursion(..)))
     );
     assert_matches!(
-        eval("{x = y + z, y = z + x, z = 1}.x"),
+        eval("{x = y + z; y = z + x; z = 1}.x"),
         Err(Error::EvalError(EvalError::InfiniteRecursion(..)))
     );
     assert_matches!(
-        eval("{x = (fun a => a + y) 0, y = (fun a => a + x) 0}.x"),
+        eval("{x = (fun a => a + y) 0; y = (fun a => a + x) 0}.x"),
         Err(Error::EvalError(EvalError::InfiniteRecursion(..)))
     );
 }
diff --git a/tests/pass/builtins.ncl b/tests/pass/builtins.ncl
index 1e2bac24..3795a036 100644
--- a/tests/pass/builtins.ncl
+++ b/tests/pass/builtins.ncl
@@ -7,16 +7,16 @@ let Assert = fun l x => x || %blame% l in
 /// just that the evaluation succeeds
 (%seq% 1 true | #Assert) &&
 (let x = (1 + 1) in %seq% x x == 2 | #Assert) &&
-(let r = {a=(1 + 1),} in
+(let r = {a=(1 + 1);} in
   %deepSeq% r (r.a) == 2 | #Assert) &&
-(let r = {a=(1 + 1),b=("a" ++ "b"),} in
+(let r = {a=(1 + 1);b=("a" ++ "b");} in
   %deepSeq% r (r.b) == "ab" | #Assert) &&
 (let r = {a = {b = 1 + 1}} in
   %deepSeq% r (r.a.b) == 2 | #Assert) &&
 
 (let inj = fun x => {b=(x + 2)} in
   let cat = fun x => fun y => x ++ y in
-  let r = {a=(inj 1),b=(cat "a" "b")} in
+  let r = {a=(inj 1);b=(cat "a" "b")} in
   %deepSeq% r (r.a.b) == 3 | #Assert) &&
 
 true
diff --git a/tests/pass/contracts.ncl b/tests/pass/contracts.ncl
index 3cea5432..53980e8f 100644
--- a/tests/pass/contracts.ncl
+++ b/tests/pass/contracts.ncl
@@ -41,12 +41,12 @@ f `boo == 3) &&
 
 // records_simple
 (({} | {}) == {} | #Assert) &&
-(let x | {a: Num, s: Str} = {a = 1, s = "a"} in
-  %deepSeq% x x == {a = 1, s = "a"}
+(let x | {a: Num, s: Str} = {a = 1; s = "a"} in
+  %deepSeq% x x == {a = 1; s = "a"}
   | #Assert) &&
 
-(let x | {a: Num, s: {foo: Bool}} = {a = 1, s = { foo = true}} in
-  %deepSeq% x x == {a = 1, s = { foo = true}}
+(let x | {a: Num, s: {foo: Bool}} = {a = 1; s = { foo = true}} in
+  %deepSeq% x x == {a = 1; s = { foo = true}}
   | #Assert) &&
 
 // polymorphism
@@ -57,27 +57,27 @@ f `boo == 3) &&
     x -$ "foo" in
 
   (id {} == {} | #Assert) &&
-  (id {a = 1, b = false} == {a = 1, b = false} | #Assert) &&
+  (id {a = 1; b = false} == {a = 1; b = false} | #Assert) &&
   (extend {} == {foo = 1} | #Assert) &&
-  (extend {bar = false} == {foo = 1, bar = false} | #Assert) &&
+  (extend {bar = false} == {foo = 1; bar = false} | #Assert) &&
   (remove {foo = 1} == {} | #Assert) &&
-  (remove {foo = 1, bar = 1} == {bar = 1} | #Assert) &&
+  (remove {foo = 1; bar = 1} == {bar = 1} | #Assert) &&
   (remove (extend {}) == {} | #Assert) &&
   (extend (remove {foo = 2}) == {foo =1} | #Assert) &&
   (let f | forall a b. {f: a -> a, arg: a | b} -> a =
       fun rec => rec.f (rec.arg) in
-    f { f = fun x => x ++ " suffix", arg = "foo" }
+    f { f = fun x => x ++ " suffix"; arg = "foo" }
     == "foo suffix"
     | #Assert)
 ) &&
 
 // records_dynamic_tail
-(({a = 1, b = "b"} | {a: Num, b: Str | Dyn}) == {a = 1, b = "b"}
+(({a = 1; b = "b"} | {a: Num, b: Str | Dyn}) == {a = 1; b = "b"}
   | #Assert) &&
-(({a = 1, b = "b", c = false} | {a: Num, b: Str | Dyn})
-  == {a = 1, b = "b", c = false}
+(({a = 1; b = "b"; c = false} | {a: Num, b: Str | Dyn})
+  == {a = 1; b = "b"; c = false}
   | #Assert) &&
-((fun r => r.b | {a: Num | Dyn} -> Dyn) {a = 1, b = 2} == 2
+((fun r => r.b | {a: Num | Dyn} -> Dyn) {a = 1; b = 2} == 2
   | #Assert) &&
 
 
diff --git a/tests/pass/eq.ncl b/tests/pass/eq.ncl
index b605e992..da314768 100644
--- a/tests/pass/eq.ncl
+++ b/tests/pass/eq.ncl
@@ -36,30 +36,30 @@ let Assert = fun l x => x || %blame% l in
 // records
 ({} == {} | #Assert) &&
 ({}$["a" = 1]$["b" = true]
-  == {a = 1, b = true}
+  == {a = 1; b = true}
   | #Assert) &&
-({a = 1 + 0, b = 1 + 1, c = 1 + 1 + 1}
-  == { a = 1, b = 2, c = 3 }
+({a = 1 + 0; b = 1 + 1; c = 1 + 1 + 1}
+  == { a = 1; b = 2; c = 3 }
   | #Assert) &&
 ({
-    foo = 1 + 0,
-    bar = "a" ++ "b",
+    foo = 1 + 0;
+    bar = "a" ++ "b";
     baz = if true then true else false
-  } == {foo = 1, bar = "ab", baz = true}
+  } == {foo = 1; bar = "ab"; baz = true}
   | #Assert) &&
 
 ({}$["a" = { a = { a = {} } }]
   == { a = { a = { a = {} } } }
   | #Assert) &&
 ({
-    foo = {bar = 2 + (-1)},
+    foo = {bar = 2 + (-1)};
     baz = {foo = {bar = 1 + 1}}
   }
-  == {foo = {bar = 1}, baz = {foo = {bar = 2}}}
+  == {foo = {bar = 1}; baz = {foo = {bar = 2}}}
   | #Assert) &&
 ({} != {a = true} | #Assert) &&
 ({a = 1} != {a = 2} | #Assert) &&
-({ a = "a", b = true } != { a = true, b = "a"} | #Assert) &&
+({ a = "a"; b = true } != { a = true; b = "a"} | #Assert) &&
 ({ a = { a = true } } != {a = { a = { a = true } } } | #Assert) &&
 
 // Now that the equality operator directly uses the stack to store its continuation (see
@@ -71,8 +71,8 @@ let Assert = fun l x => x || %blame% l in
       if b then true else false in
     not (not (not (not ((x) == (y))))) in
   (eq_with_ctxt
-      {a = 1 + 0, b = 1 + 1 + a, c = 0, d = 0}
-      { a = 1, b = 3, c = 0, d = 0}
+      {a = 1 + 0; b = 1 + 1 + a; c = 0; d = 0}
+      { a = 1; b = 3; c = 0; d = 0}
     | #Assert) &&
   (eq_with_ctxt
       [[1,2,3,4], [1,0,3,4], [1,2,3,4], [1,2,3,4]]
diff --git a/tests/pass/metavalues.ncl b/tests/pass/metavalues.ncl
index 4bd158aa..39a5b4fe 100644
--- a/tests/pass/metavalues.ncl
+++ b/tests/pass/metavalues.ncl
@@ -8,23 +8,23 @@ let Assert = fun l x => x || %blame% l in
   builtins.seq (x.a) ((x & {a=2}).a) == 2 | #Assert) &&
 
 // merge_default
-(({a = 2} & {a | default = 0, b | default = true}) == {a = 2, b = true}
+(({a = 2} & {a | default = 0; b | default = true}) == {a = 2; b = true}
   | #Assert) &&
-({a | default = {x = 1}} & {a | default = {y = "y"}} == {a = {x = 1, y = "y"}}
+({a | default = {x = 1}} & {a | default = {y = "y"}} == {a = {x = 1; y = "y"}}
   | #Assert) &&
 
 // merge_contract
-({a = 2, b | Bool} & {a | Num, b | default = true}
-  == {a = 2, b = true}
+({a = 2; b | Bool} & {a | Num; b | default = true}
+  == {a = 2; b = true}
   | #Assert) &&
 
 // merge_default_contract
-({a = 2} & {a | default | Num = 0, b | default = true}
-  == {a = 2, b = true}
+({a = 2} & {a | default | Num = 0; b | default = true}
+  == {a = 2; b = true}
   | #Assert) &&
 
 ({a=2} & {a | Num} & {a | default = 3} == {a = 2} | #Assert) &&
-({a=2} & {b | Num} & {b | default = 3} == {a = 2, b = 3} | #Assert) &&
+({a=2} & {b | Num} & {b | default = 3} == {a = 2; b = 3} | #Assert) &&
 (({a | default = 1} & {b | Num} & {a | default = 1}).a
   == 1
   | #Assert) &&
diff --git a/tests/pass/records.ncl b/tests/pass/records.ncl
index ec728c10..c4c1e437 100644
--- a/tests/pass/records.ncl
+++ b/tests/pass/records.ncl
@@ -1,13 +1,13 @@
 let Assert = fun l x => x || %blame% l in
 
 // accesses
-(({foo = 3, bar = true}).bar == true | #Assert) &&
-({"#{if true then "foo" else "bar"}" = false, bar = true}.foo
+(({foo = 3; bar = true}).bar == true | #Assert) &&
+({"#{if true then "foo" else "bar"}" = false; bar = true}.foo
   == false
   | #Assert) &&
 
-(({foo = 3, bar = true})."bar" == true | #Assert) &&
-({"#{if true then "foo" else "bar"}" = false, bar = true}."#{"foo"}"
+(({foo = 3; bar = true})."bar" == true | #Assert) &&
+({"#{if true then "foo" else "bar"}" = false; bar = true}."#{"foo"}"
  == false 
  | #Assert) &&
 
@@ -15,67 +15,67 @@ let Assert = fun l x => x || %blame% l in
   | #Assert) &&
 
 // primitive_ops
-(records.hasField "foo" {foo = 1, bar = 2} | #Assert) &&
-(records.hasField "fop" {foo = 1, bar = 2} == false | #Assert) &&
-(records.hasField "foo" ({foo = 2, bar = 3} -$ "foo")
+(records.hasField "foo" {foo = 1; bar = 2} | #Assert) &&
+(records.hasField "fop" {foo = 1; bar = 2} == false | #Assert) &&
+(records.hasField "foo" ({foo = 2; bar = 3} -$ "foo")
   == false
   | #Assert) &&
 
 (records.hasField "foo" ({bar = 3}$["foo" = 1]) | #Assert) &&
 
 // lazyness of map
-((records.map (fun x y => y + 1) {foo = 1, bar = "it's lazy"}).foo
+((records.map (fun x y => y + 1) {foo = 1; bar = "it's lazy"}).foo
   == 2
   | #Assert) &&
 
 (let r = records.map
     (fun y x => if %isNum% x then x + 1 else 0)
-    {foo = 1, bar = "it's lazy"} in
+    {foo = 1; bar = "it's lazy"} in
   (r.foo) + (r.bar) == 2
   | #Assert) &&
 
 // merging
-({a = 1} & {b=true} == {a = 1, b = true} | #Assert) &&
-({a = 1, b = 2} & {b = 2, c = 3}
-  == {a = 1, b = 2, c = 3}
+({a = 1} & {b=true} == {a = 1; b = true} | #Assert) &&
+({a = 1; b = 2} & {b = 2; c = 3}
+  == {a = 1; b = 2; c = 3}
   | #Assert) &&
 
 ({a = {b = 1}} & {a = {c = true}}
-  == {a = {b = 1, c = true}}
+  == {a = {b = 1; c = true}}
   | #Assert) &&
 
 // merge_complex
 (let rec1 = {
-    a = false,
-    b = if true then (1 + 1) else (2 + 0),
-    c= ((fun x => x) (fun y => y)) 2,
+    a = false;
+    b = if true then (1 + 1) else (2 + 0);
+    c= ((fun x => x) (fun y => y)) 2;
   } in
   let rec2 = {
-    b = ((fun x => x) (fun y => y)) 2,
-    c = if true then (1 + 1) else (2 + 0),
-    d = true,
+    b = ((fun x => x) (fun y => y)) 2;
+    c = if true then (1 + 1) else (2 + 0);
+    d = true;
   } in
   let result = {
-    a = false,
-    b = 2,
-    c = 2,
-    d = true,
+    a = false;
+    b = 2;
+    c = 2;
+    d = true;
   } in
   rec1 & rec2 == result
   | #Assert) &&
 
 // merge_with_env
 ((fun y => ((fun x => {a=y}) 1) & ({b=false})) 2
-  == {a = 2, b = false}
+  == {a = 2; b = false}
   | #Assert) &&
 
 // merge_with_env_nested
-({b={c=10}} & ((fun x => {a=x, b={c=x}}) 10)
-  == {a=10, b = {c = 10}}
+({b={c=10}} & ((fun x => {a=x; b={c=x}}) 10)
+  == {a=10; b = {c = 10}}
   | #Assert) &&
 
 // recursive_records
-({a = 1, b = a + 1, c = b + a} == {a = 1, b = 2, c = 3} | #Assert) &&
+({a = 1; b = a + 1; c = b + a} == {a = 1; b = 2; c = 3} | #Assert) &&
 ({f = fun x y =>
     if x == 0 then y else f (x + (-1)) (y + 1)
   }.f 5 5
@@ -87,7 +87,7 @@ let Assert = fun l x => x || %blame% l in
     f = fun x =>
       if x == 0 then
         res
-      else g x,
+      else g x;
     g = fun y => f (y + (-1))
   }.f 10 in
   with_res "done" == "done"
diff --git a/tests/pass/serialize.ncl b/tests/pass/serialize.ncl
index bca17a1e..54cbfc79 100644
--- a/tests/pass/serialize.ncl
+++ b/tests/pass/serialize.ncl
@@ -18,15 +18,15 @@ let assertDeserInv = fun x =>
 (assertSerInv {val = 1 + 1} | #Assert) &&
 (assertSerInv {val = "Some string"} | #Assert) &&
 (assertSerInv {val = ["a", 3, []]} | #Assert) &&
-(assertSerInv {a.foo.bar = "2", b = false, c = [{d = "e"}, {d = "f"}]}
+(assertSerInv {a.foo.bar = "2"; b = false; c = [{d = "e"}, {d = "f"}]}
   | #Assert) &&
 
-(assertDeserInv {a = 1, b = 4, c = 3} | #Assert) &&
+(assertDeserInv {a = 1; b = 4; c = 3} | #Assert) &&
 (assertDeserInv {a.b.c = "richtig"} | #Assert) &&
 (assertDeserInv {
-    foo = 1,
-    bar = ["str", true],
-    baz = {subfoo = true, subbar = 0}
+    foo = 1;
+    bar = ["str", true];
+    baz = {subfoo = true; subbar = 0}
   } | #Assert) &&
 
 
diff --git a/tests/pass/typechecking.ncl b/tests/pass/typechecking.ncl
index b0264fa0..24fa3f8f 100644
--- a/tests/pass/typechecking.ncl
+++ b/tests/pass/typechecking.ncl
@@ -76,22 +76,22 @@ let typecheck = [
 
   // static records
   ({bla = 1} : {bla : Num}),
-  ({blo = true, bla = 1} : {bla : Num, blo : Bool}),
+  ({blo = true; bla = 1} : {bla : Num, blo : Bool}),
   ({blo = 1}.blo : Num),
-  ({bla = true, blo = 1}.blo : Num),
-  let r : {bla : Bool, blo : Num} = {blo = 1, bla = true} in
+  ({bla = true; blo = 1}.blo : Num),
+  let r : {bla : Bool, blo : Num} = {blo = 1; bla = true} in
     ((if r.bla then r.blo else 2) : Num),
 
   let f : forall a. (forall r. {bla : Bool, blo : a, ble : a | r} -> a) =
       fun r => if r.bla then r.blo else r.ble in
-    (if (f {bla = true, blo = false, ble = true, blip = 1, }) then
-      (f {bla = true, blo = 1, ble = 2, blip = `blip, })
+    (if (f {bla = true; blo = false; ble = true; blip = 1; }) then
+      (f {bla = true; blo = 1; ble = 2; blip = `blip; })
     else
-      (f {bla = true, blo = 3, ble = 4, bloppo = `bloppop, }) : Num),
+      (f {bla = true; blo = 3; ble = 4; bloppo = `bloppop; }) : Num),
 
-  ({ "#{if true then "foo" else "bar"}" = 2, } : {_ : Num}),
-  ({ "#{if true then "foo" else "bar"}" = 2, }."bla" : Num),
-  ({ foo = 3, bar = 4, } : {_ : Num}),
+  ({ "#{if true then "foo" else "bar"}" = 2; } : {_ : Num}),
+  ({ "#{if true then "foo" else "bar"}" = 2; }."bla" : Num),
+  ({ foo = 3; bar = 4; } : {_ : Num}),
 
   // seq
   (%seq% false 1 : Num),
@@ -115,18 +115,18 @@ let typecheck = [
   fun i l => %elemAt% l i : forall a. Num -> List a -> a,
 
   // recursive_records
-  {a : Num = 1, b = a + 1} : {a : Num, b : Num},
+  {a : Num = 1; b = a + 1} : {a : Num, b : Num},
   {a : Num = 1 + a} : {a : Num},
   {a : Num = 1 + a} : {a : Num},
 
   // let_inference
   (let x = 1 + 2 in let f = fun x => x + 1 in f x) : Num, 
   // (let x = 1 + 2 in let f = fun x => x ++ "a" in f x) : Num,
-  {a = 1, b = 1 + a} : {a : Num, b : Num},
-  {f = fun x => if x == 0 then 1 else 1 + (f (x + (-1))),}
+  {a = 1; b = 1 + a} : {a : Num, b : Num},
+  {f = fun x => if x == 0 then 1 else 1 + (f (x + (-1)));}
     : {f : Num -> Num},
 
-  { f = fun x => if x == 0 then 1 else 1 + (f (x + (-1))),}
+  { f = fun x => if x == 0 then 1 else 1 + (f (x + (-1)));}
     : {f : Num -> Num},
 
   // polymorphic_row_constraints
@@ -134,8 +134,8 @@ let typecheck = [
     let remove | forall c. {a: Str | c} -> { | c} = 0 in
     (let good = remove (extend {}) in 0) : Num,
 
-  let r | {a: Num | Dyn} = {a = 1, b = 2} in (r.a : Num),
-  ({a = 1, b = 2} | {a: Num | Dyn}) : {a: Num | Dyn},
+  let r | {a: Num | Dyn} = {a = 1; b = 2} in (r.a : Num),
+  ({a = 1; b = 2} | {a: Num | Dyn}) : {a: Num | Dyn},
 
   //Regression test following [#270](https://github.com/tweag/nickel/issues/270). Check that
   //unifying a variable with itself doesn't introduce a loop. The failure of this test results
diff --git a/tests/records_fail.rs b/tests/records_fail.rs
index 59655ee5..fc608f1b 100644
--- a/tests/records_fail.rs
+++ b/tests/records_fail.rs
@@ -11,7 +11,7 @@ fn records_access() {
         Err(Error::EvalError(EvalError::FieldMissing(..)))
     );
     assert_matches!(
-        eval("({ \"#{(if false then \"foo\" else \"bar\")}\" = false, bar = true, }).foo"),
+        eval("({ \"#{(if false then \"foo\" else \"bar\")}\" = false; bar = true; }).foo"),
         Err(Error::EvalError(EvalError::Other(msg, ..))) if msg.starts_with("$[ .. ]"));
 }
 
@@ -22,7 +22,7 @@ fn non_mergeable() {
         Err(Error::EvalError(EvalError::MergeIncompatibleArgs(..)))
     );
     assert_matches!(
-        eval("({a | default = false} & {a | default = true}).a"),
+        eval("({a | default = false;} & {a | default = true}).a"),
         Err(Error::EvalError(EvalError::MergeIncompatibleArgs(..)))
     );
     assert_matches!(
diff --git a/tests/typecheck_fail.rs b/tests/typecheck_fail.rs
index a7284081..01146aba 100644
--- a/tests/typecheck_fail.rs
+++ b/tests/typecheck_fail.rs
@@ -119,19 +119,19 @@ fn static_record_simple() {
     assert_typecheck_fails!(
         "let f : forall a. (forall r. {bla : Bool, blo : a, ble : a | r} -> a) =
             fun r => if r.bla then r.blo else r.ble in
-         (f {bla = true, blo = 1, ble = true, blip = `blip} : Num)"
+         (f {bla = true; blo = 1; ble = true; blip = `blip} : Num)"
     );
     assert_typecheck_fails!(
         "let f : forall a. (forall r. {bla : Bool, blo : a, ble : a | r} -> a) =
             fun r => if r.bla then (r.blo + 1) else r.ble in
-         (f {bla = true, blo = 1, ble = 2, blip = `blip} : Num)"
+         (f {bla = true; blo = 1; ble = 2; blip = `blip} : Num)"
     );
 }
 
 #[test]
 fn dynamic_record_simple() {
     assert_typecheck_fails!(
-        "({ \"#{if true then \"foo\" else \"bar\"}\" = 2, \"foo\" = true, }.\"bla\") : Num"
+        "({ \"#{if true then \"foo\" else \"bar\"}\" = 2; \"foo\" = true; }.\"bla\") : Num"
     );
 }
 
@@ -186,8 +186,8 @@ fn imports() {
 
 #[test]
 fn recursive_records() {
-    assert_typecheck_fails!("{a : Num = true, b = a + 1} : {a : Num, b : Num}");
-    assert_typecheck_fails!("{a = 1, b : Bool = a} : {a : Num, b : Bool}");
+    assert_typecheck_fails!("{a : Num = true; b = a + 1} : {a : Num, b : Num}");
+    assert_typecheck_fails!("{a = 1; b : Bool = a} : {a : Num, b : Bool}");
 }
 
 #[test]
@@ -223,7 +223,7 @@ fn polymorphic_row_constraints() {
 
     let mut res = type_check_expr(
         "let extend | forall c. { | c} -> {a: Str | c} = null in
-           (let bad = extend {a = 1} in 0) : Num",
+           (let bad = extend {a = 1;} in 0) : Num",
     );
     assert_row_conflict(res);
 
@@ -238,7 +238,7 @@ fn polymorphic_row_constraints() {
 fn dynamic_row_tail() {
     // Currently, typechecking is conservative wrt the dynamic row type, meaning it can't
     // convert to a less precise type with a dynamic tail.
-    assert_typecheck_fails!("{a = 1, b = 2} : {a: Num | Dyn}");
+    assert_typecheck_fails!("{a = 1; b = 2} : {a: Num | Dyn}");
     assert_typecheck_fails!("{a = 1} : {a: Num | Dyn}");
     assert_typecheck_fails!("({a = 1} | {a: Num | Dyn}) : {a: Num}");
     assert_typecheck_fails!("{a = 1} : {a: Num | Dyn}");