From c078119bc46045088076d4397506aa92e720b674 Mon Sep 17 00:00:00 2001 From: Gaith Hallak Date: Thu, 12 Jan 2023 16:23:36 +0300 Subject: [PATCH] Add hole expression (#433) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit * Add hole expressions * Fix the issue of unreported holes * Add tests * New line in the end of the test file * Update CHANGELOG * Add hole expression to the docs * Do not treat hole as a special type * Update docs * Update docs/sophia_features.md Co-authored-by: Radosław Rowicki <35342116+radrow@users.noreply.github.com> Co-authored-by: Radosław Rowicki <35342116+radrow@users.noreply.github.com> --- CHANGELOG.md | 1 + docs/sophia_features.md | 13 +++++++++++++ docs/sophia_syntax.md | 1 + src/aeso_ast_infer_types.erl | 7 +++++++ src/aeso_parser.erl | 3 +++ test/aeso_compiler_tests.erl | 10 ++++++++++ test/contracts/hole_expression.aes | 13 +++++++++++++ 7 files changed, 48 insertions(+) create mode 100644 test/contracts/hole_expression.aes diff --git a/CHANGELOG.md b/CHANGELOG.md index b2c6d22..79b6781 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -14,6 +14,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0 entrypoint f(c : Main) : int = c.spend(10) ``` - Return a mapping from variables to FATE registers in the compilation output. +- Hole expression. ### Changed - Type definitions serialised to ACI as `typedefs` field instead of `type_defs` to increase compatibility. - Check contracts and entrypoints modifiers when implementing interfaces. diff --git a/docs/sophia_features.md b/docs/sophia_features.md index 973dc22..7fa0450 100644 --- a/docs/sophia_features.md +++ b/docs/sophia_features.md @@ -560,6 +560,19 @@ Sophia has the following types: | oracle_query('a, 'b) | `oq_2oRvyowJuJnEkxy58Ckkw77XfWJrmRgmGaLzhdqb67SKEL1gPY` | | contract | `ct_Ez6MyeTMm17YnTnDdHTSrzMEBKmy7Uz2sXu347bTDPgVH2ifJ` | +## Hole expression + +Hole expressions, written as `???`, are expressions that are used as a placeholder. During compilation, the compiler will generate a type error indication the type of the hole expression. + +``` +include "List.aes" +contract C = + entrypoint f() = + List.sum(List.map(???, [1,2,3])) +``` + +A hole expression found in the example above will generate the error `` Found a hole of type `(int) => int` ``. This says that the compiler expects a function from `int` to `int` in place of the `???` placeholder. + ## Arithmetic Sophia integers (`int`) are represented by arbitrary-sized signed words and support the following diff --git a/docs/sophia_syntax.md b/docs/sophia_syntax.md index abae005..e57cc84 100644 --- a/docs/sophia_syntax.md +++ b/docs/sophia_syntax.md @@ -238,6 +238,7 @@ Expr ::= '(' LamArgs ')' '=>' Block(Stmt) // Anonymous function (x) => x + | Int | Bytes | String | Char // Literals 123, 0xff, #00abc123, "foo", '%' | AccountAddress | ContractAddress // Chain identifiers | OracleAddress | OracleQueryId // Chain identifiers + | '???' // Hole expression 1 + ??? Generator ::= Pattern '<-' Expr // Generator | 'if' '(' Expr ')' // Guard diff --git a/src/aeso_ast_infer_types.erl b/src/aeso_ast_infer_types.erl index 55ba29e..2184662 100644 --- a/src/aeso_ast_infer_types.erl +++ b/src/aeso_ast_infer_types.erl @@ -1843,6 +1843,10 @@ infer_expr(_Env, Body={contract_pubkey, As, _}) -> {typed, As, Body, Con}; infer_expr(_Env, Body={id, As, "_"}) -> {typed, As, Body, fresh_uvar(As)}; +infer_expr(_Env, Body={id, As, "???"}) -> + T = fresh_uvar(As), + type_error({hole_found, As, T}), + {typed, As, Body, T}; infer_expr(Env, Id = {Tag, As, _}) when Tag == id; Tag == qid -> {QName, Type} = lookup_name(Env, As, Id), {typed, As, QName, Type}; @@ -3396,6 +3400,9 @@ mk_error({cannot_unify, A, B, Cxt, When}) -> [pp(instantiate(A)), pp(instantiate(B))]), {Pos, Ctxt} = pp_when(When), mk_t_err(Pos, Msg, Ctxt); +mk_error({hole_found, Ann, Type}) -> + Msg = io_lib:format("Found a hole of type `~s`", [pp(instantiate(Type))]), + mk_t_err(pos(Ann), Msg); mk_error({unbound_variable, Id}) -> Msg = io_lib:format("Unbound variable `~s`", [pp(Id)]), case Id of diff --git a/src/aeso_parser.erl b/src/aeso_parser.erl index f844942..d1d92cb 100644 --- a/src/aeso_parser.erl +++ b/src/aeso_parser.erl @@ -359,9 +359,12 @@ exprAtom() -> , ?RULE(tok('['), Expr, binop('..'), Expr, tok(']'), _3(_2, _4)) , ?RULE(keyword('('), comma_sep(Expr), tok(')'), tuple_e(_1, _2)) , letpat() + , hole() ]) end). +hole() -> ?RULE(token('???'), {id, get_ann(_1), "???"}). + comprehension_exp() -> ?LAZY_P(choice( [ comprehension_bind() diff --git a/test/aeso_compiler_tests.erl b/test/aeso_compiler_tests.erl index 1c724a5..e070fd7 100644 --- a/test/aeso_compiler_tests.erl +++ b/test/aeso_compiler_tests.erl @@ -1182,6 +1182,16 @@ failing_contracts() -> , ?TYPE_ERROR(using_contract_as_namespace, [<>]) + , ?TYPE_ERROR(hole_expression, + [<>, + <>, + < int`">>, + <> + ]) ]. validation_test_() -> diff --git a/test/contracts/hole_expression.aes b/test/contracts/hole_expression.aes new file mode 100644 index 0000000..99594d8 --- /dev/null +++ b/test/contracts/hole_expression.aes @@ -0,0 +1,13 @@ +include "List.aes" + +contract C = + entrypoint f() = + let ??? = true + let v = ??? + let q = v == "str" + let xs = [1, 2, 3, 4] + switch (List.first(List.map(???, xs))) + Some(x) => x + 1 + None => 0 + + function g() = ???