From 7cdd2de6e48a108fd5654c32c72117b04d368284 Mon Sep 17 00:00:00 2001 From: Gaith Hallak Date: Mon, 2 Jan 2023 23:15:48 +0300 Subject: [PATCH 1/9] Add hole expressions --- src/aeso_ast_infer_types.erl | 11 +++++++++++ src/aeso_parser.erl | 3 +++ 2 files changed, 14 insertions(+) diff --git a/src/aeso_ast_infer_types.erl b/src/aeso_ast_infer_types.erl index 55ba29e..6bc6cbd 100644 --- a/src/aeso_ast_infer_types.erl +++ b/src/aeso_ast_infer_types.erl @@ -1843,6 +1843,8 @@ 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, "???"}) -> + {typed, As, Body, {id, As, "hole"}}; infer_expr(Env, Id = {Tag, As, _}) when Tag == id; Tag == qid -> {QName, Type} = lookup_name(Env, As, Id), {typed, As, QName, Type}; @@ -2939,6 +2941,12 @@ unify1(_Env, _A, {id, _, "void"}, Variance, _When) unify1(_Env, {id, _, "void"}, _B, Variance, _When) when Variance == contravariant orelse Variance == bivariant -> true; +unify1(_Env, {id, Ann, "hole"}, B, _Variance, _When) -> + type_error({hole_found, Ann, B}), + true; +unify1(_Env, A, {id, Ann, "hole"}, _Variance, _When) -> + type_error({hole_found, Ann, A}), + true; unify1(_Env, {id, _, Name}, {id, _, Name}, _Variance, _When) -> true; unify1(Env, A = {con, _, NameA}, B = {con, _, NameB}, Variance, When) -> @@ -3396,6 +3404,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() -- 2.30.2 From abee3d89ed2bd9af0c72402578dc4995d2ae9425 Mon Sep 17 00:00:00 2001 From: Gaith Hallak Date: Sat, 7 Jan 2023 23:56:04 +0300 Subject: [PATCH 2/9] Fix the issue of unreported holes --- src/aeso_ast_infer_types.erl | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/src/aeso_ast_infer_types.erl b/src/aeso_ast_infer_types.erl index 6bc6cbd..c0f2c6b 100644 --- a/src/aeso_ast_infer_types.erl +++ b/src/aeso_ast_infer_types.erl @@ -2912,6 +2912,12 @@ unify1(_Env, {uvar, _, R}, {uvar, _, R}, _Variance, _When) -> true; unify1(_Env, {uvar, _, _}, {fun_t, _, _, var_args, _}, _Variance, When) -> type_error({unify_varargs, When}); +unify1(_Env, {id, Ann, "hole"}, B, _Variance, _When) -> + type_error({hole_found, Ann, B}), + true; +unify1(_Env, A, {id, Ann, "hole"}, _Variance, _When) -> + type_error({hole_found, Ann, A}), + true; unify1(Env, {uvar, A, R}, T, _Variance, When) -> case occurs_check(R, T) of true -> @@ -2941,12 +2947,6 @@ unify1(_Env, _A, {id, _, "void"}, Variance, _When) unify1(_Env, {id, _, "void"}, _B, Variance, _When) when Variance == contravariant orelse Variance == bivariant -> true; -unify1(_Env, {id, Ann, "hole"}, B, _Variance, _When) -> - type_error({hole_found, Ann, B}), - true; -unify1(_Env, A, {id, Ann, "hole"}, _Variance, _When) -> - type_error({hole_found, Ann, A}), - true; unify1(_Env, {id, _, Name}, {id, _, Name}, _Variance, _When) -> true; unify1(Env, A = {con, _, NameA}, B = {con, _, NameB}, Variance, When) -> -- 2.30.2 From 48f87c7cc759d00f95319e7708e1a35db9ad2a59 Mon Sep 17 00:00:00 2001 From: Gaith Hallak Date: Sat, 7 Jan 2023 23:56:11 +0300 Subject: [PATCH 3/9] Add tests --- test/aeso_compiler_tests.erl | 10 ++++++++++ test/contracts/hole_expression.aes | 13 +++++++++++++ 2 files changed, 23 insertions(+) create mode 100644 test/contracts/hole_expression.aes 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..d1e26d1 --- /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() = ??? \ No newline at end of file -- 2.30.2 From abb1a3f4e86ef070b765a8c5b89d24c2a3cee35c Mon Sep 17 00:00:00 2001 From: Gaith Hallak Date: Sun, 8 Jan 2023 09:14:17 +0300 Subject: [PATCH 4/9] New line in the end of the test file --- test/contracts/hole_expression.aes | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/test/contracts/hole_expression.aes b/test/contracts/hole_expression.aes index d1e26d1..99594d8 100644 --- a/test/contracts/hole_expression.aes +++ b/test/contracts/hole_expression.aes @@ -10,4 +10,4 @@ contract C = Some(x) => x + 1 None => 0 - function g() = ??? \ No newline at end of file + function g() = ??? -- 2.30.2 From 361bdd4daa63c3cae56a1f0661fbb2cd419bbf0e Mon Sep 17 00:00:00 2001 From: Gaith Hallak Date: Sun, 8 Jan 2023 09:14:29 +0300 Subject: [PATCH 5/9] Update CHANGELOG --- CHANGELOG.md | 1 + 1 file changed, 1 insertion(+) 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. -- 2.30.2 From f772276fb6234e070d2377ad2afb648a49548321 Mon Sep 17 00:00:00 2001 From: Gaith Hallak Date: Sun, 8 Jan 2023 10:48:01 +0300 Subject: [PATCH 6/9] Add hole expression to the docs --- docs/sophia_syntax.md | 1 + 1 file changed, 1 insertion(+) 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 -- 2.30.2 From 50d2507c434407af15780b38ade55e3da5469eea Mon Sep 17 00:00:00 2001 From: Gaith Hallak Date: Tue, 10 Jan 2023 07:37:03 +0300 Subject: [PATCH 7/9] Do not treat hole as a special type --- src/aeso_ast_infer_types.erl | 10 +++------- 1 file changed, 3 insertions(+), 7 deletions(-) diff --git a/src/aeso_ast_infer_types.erl b/src/aeso_ast_infer_types.erl index c0f2c6b..2184662 100644 --- a/src/aeso_ast_infer_types.erl +++ b/src/aeso_ast_infer_types.erl @@ -1844,7 +1844,9 @@ infer_expr(_Env, Body={contract_pubkey, As, _}) -> infer_expr(_Env, Body={id, As, "_"}) -> {typed, As, Body, fresh_uvar(As)}; infer_expr(_Env, Body={id, As, "???"}) -> - {typed, As, Body, {id, As, "hole"}}; + 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}; @@ -2912,12 +2914,6 @@ unify1(_Env, {uvar, _, R}, {uvar, _, R}, _Variance, _When) -> true; unify1(_Env, {uvar, _, _}, {fun_t, _, _, var_args, _}, _Variance, When) -> type_error({unify_varargs, When}); -unify1(_Env, {id, Ann, "hole"}, B, _Variance, _When) -> - type_error({hole_found, Ann, B}), - true; -unify1(_Env, A, {id, Ann, "hole"}, _Variance, _When) -> - type_error({hole_found, Ann, A}), - true; unify1(Env, {uvar, A, R}, T, _Variance, When) -> case occurs_check(R, T) of true -> -- 2.30.2 From 3b25c298fa0bf144cbc0719da6014fa678e1387d Mon Sep 17 00:00:00 2001 From: Gaith Hallak Date: Tue, 10 Jan 2023 07:52:37 +0300 Subject: [PATCH 8/9] Update docs --- docs/sophia_features.md | 13 +++++++++++++ 1 file changed, 13 insertions(+) diff --git a/docs/sophia_features.md b/docs/sophia_features.md index 973dc22..3e4ebe1 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])) +``` + +The hole expression found on the last line of the above example will generate the error `` Found a hole of type `(int) => int` ``. Meaning that a function from `int` to `int` should be used instead of the `???` placeholder. + ## Arithmetic Sophia integers (`int`) are represented by arbitrary-sized signed words and support the following -- 2.30.2 From cdf801e2673840937af84dc0ebdb57f18507fdc8 Mon Sep 17 00:00:00 2001 From: Gaith Hallak Date: Thu, 12 Jan 2023 12:04:13 +0300 Subject: [PATCH 9/9] Update docs/sophia_features.md MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: Radosław Rowicki <35342116+radrow@users.noreply.github.com> --- docs/sophia_features.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/sophia_features.md b/docs/sophia_features.md index 3e4ebe1..7fa0450 100644 --- a/docs/sophia_features.md +++ b/docs/sophia_features.md @@ -571,7 +571,7 @@ contract C = List.sum(List.map(???, [1,2,3])) ``` -The hole expression found on the last line of the above example will generate the error `` Found a hole of type `(int) => int` ``. Meaning that a function from `int` to `int` should be used instead of the `???` placeholder. +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 -- 2.30.2