Add hole expression (#433)

* 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>
This commit is contained in:
Gaith Hallak 2023-01-12 16:23:36 +03:00 committed by GitHub
parent 31fd8fe24f
commit c078119bc4
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
7 changed files with 48 additions and 0 deletions

View File

@ -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.

View File

@ -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

View File

@ -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

View File

@ -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

View File

@ -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()

View File

@ -1182,6 +1182,16 @@ failing_contracts() ->
, ?TYPE_ERROR(using_contract_as_namespace,
[<<?Pos(5,3)
"Cannot use undefined namespace F">>])
, ?TYPE_ERROR(hole_expression,
[<<?Pos(5,13)
"Found a hole of type `bool`">>,
<<?Pos(6,17)
"Found a hole of type `string`">>,
<<?Pos(9,37)
"Found a hole of type `(int) => int`">>,
<<?Pos(13,20)
"Found a hole of type `'a`">>
])
].
validation_test_() ->

View File

@ -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() = ???