- + + + - - Changelog + + + + +Changelog All notable changes to this project will be documented in this file. The format is based on Keep a Changelog, and this project adheres to Semantic Versioning. @@ -1880,54 +1897,35 @@ Bytes.to_int : bytes(_) => int Simplify calldata creation - instead of passing a compiled contract, simply pass a (stubbed) contract string. - - - - - - - + + + + +
- - Changelog + + + + +Changelog All notable changes to this project will be documented in this file. The format is based on Keep a Changelog, and this project adheres to Semantic Versioning. @@ -1880,54 +1897,35 @@ Bytes.to_int : bytes(_) => int Simplify calldata creation - instead of passing a compiled contract, simply pass a (stubbed) contract string. - - - - - -
- + + + - - aeso_aci + + + + +aeso_aci Module aeso_aci The ACI interface encoder and decoder. @@ -420,59 +436,59 @@ interface. As yet the interface is very basic. function new_answer(q : string, a : int) : answers() = { [q] = a } generates the following JSON structure representing the contract interface: -{ - "contract": { - "functions": [ - { - "arguments": [], - "name": "init", - "returns": "Answers.state", - "stateful": true - }, - { - "arguments": [ - { - "name": "q", - "type": "string" - }, - { - "name": "a", - "type": "int" - } - ], - "name": "new_answer", - "returns": { - "map": [ - "string", - "int" - ] - }, - "stateful": false - } - ], - "name": "Answers", - "state": { - "record": [ - { - "name": "a", - "type": "Answers.answers" - } - ] - }, - "typedefs": [ - { - "name": "answers", - "typedef": { - "map": [ - "string", - "int" - ] - }, - "vars": [] - } - ] - } -} +{ + "contract": { + "functions": [ + { + "arguments": [], + "name": "init", + "returns": "Answers.state", + "stateful": true + }, + { + "arguments": [ + { + "name": "q", + "type": "string" + }, + { + "name": "a", + "type": "int" + } + ], + "name": "new_answer", + "returns": { + "map": [ + "string", + "int" + ] + }, + "stateful": false + } + ], + "name": "Answers", + "state": { + "record": [ + { + "name": "a", + "type": "Answers.answers" + } + ] + }, + "typedefs": [ + { + "name": "answers", + "typedef": { + "map": [ + "string", + "int" + ] + }, + "vars": [] + } + ] + } +} When that encoding is decoded the following include definition is generated: contract Answers = @@ -482,9 +498,9 @@ interface. As yet the interface is very basic. function new_answer : (string, int) => map(string, int) Types --type aci_type() :: json | string. --type json() :: jsx:json_term(). --type json_text() :: binary(). +-type aci_type() :: json | string. +-type json() :: jsx:json_term(). +-type json_text() :: binary(). Exports contract_interface(aci_type(), string()) -> {ok, json() | string()} | {error, term()} @@ -499,66 +515,67 @@ called aci_test.aes contains the contract in the description from w want to generate files aci_test.json which is the JSON encoding of the contract interface and aci_test.include which is the contract definition to be included inside another contract. -1> {ok,Contract} = file:read_file("aci_test.aes"). -{ok,<<"contract Answers =\n record state = { a : answers }\n type answers() = map(string, int)\n\n stateful function"...>>} -2> {ok,JsonACI} = aeso_aci:contract_interface(json, Contract). -{ok,[#{contract => - #{functions => - [#{arguments => [],name => <<"init">>, - returns => <<"Answers.state">>,stateful => true}, - #{arguments => - [#{name => <<"q">>,type => <<"string">>}, - #{name => <<"a">>,type => <<"int">>}], - name => <<"new_answer">>, - returns => #{<<"map">> => [<<"string">>,<<"int">>]}, - stateful => false}], - name => <<"Answers">>, - state => - #{record => - [#{name => <<"a">>,type => <<"Answers.answers">>}]}, - typedefs => - [#{name => <<"answers">>, - typedef => #{<<"map">> => [<<"string">>,<<"int">>]}, - vars => []}]}}]} -3> file:write_file("aci_test.aci", jsx:encode(JsonACI)). -ok -4> {ok,InterfaceStub} = aeso_aci:render_aci_json(JsonACI). -{ok,<<"contract Answers =\n record state = {a : Answers.answers}\n type answers = map(string, int)\n function init "...>>} -5> file:write_file("aci_test.include", InterfaceStub). -ok -6> jsx:prettify(jsx:encode(JsonACI)). -<<"[\n {\n \"contract\": {\n \"functions\": [\n {\n \"arguments\": [],\n \"name\": \"init\",\n "...>> +1> {ok,Contract} = file:read_file("aci_test.aes"). +{ok,<<"contract Answers =\n record state = { a : answers }\n type answers() = map(string, int)\n\n stateful function"...>>} +2> {ok,JsonACI} = aeso_aci:contract_interface(json, Contract). +{ok,[#{contract => + #{functions => + [#{arguments => [],name => <<"init">>, + returns => <<"Answers.state">>,stateful => true}, + #{arguments => + [#{name => <<"q">>,type => <<"string">>}, + #{name => <<"a">>,type => <<"int">>}], + name => <<"new_answer">>, + returns => #{<<"map">> => [<<"string">>,<<"int">>]}, + stateful => false}], + name => <<"Answers">>, + state => + #{record => + [#{name => <<"a">>,type => <<"Answers.answers">>}]}, + typedefs => + [#{name => <<"answers">>, + typedef => #{<<"map">> => [<<"string">>,<<"int">>]}, + vars => []}]}}]} +3> file:write_file("aci_test.aci", jsx:encode(JsonACI)). +ok +4> {ok,InterfaceStub} = aeso_aci:render_aci_json(JsonACI). +{ok,<<"contract Answers =\n record state = {a : Answers.answers}\n type answers = map(string, int)\n function init "...>>} +5> file:write_file("aci_test.include", InterfaceStub). +ok +6> jsx:prettify(jsx:encode(JsonACI)). +<<"[\n {\n \"contract\": {\n \"functions\": [\n {\n \"arguments\": [],\n \"name\": \"init\",\n "...>> The final call to jsx:prettify(jsx:encode(JsonACI)) returns the encoding in a more easily readable form. This is what is shown in the description above. - - - - - - - + + + + + + + + + + - -
- - aeso_aci + + + + +aeso_aci Module aeso_aci The ACI interface encoder and decoder. @@ -420,59 +436,59 @@ interface. As yet the interface is very basic. function new_answer(q : string, a : int) : answers() = { [q] = a }
- + + + - - aeso_compiler + + + + +aeso_compiler Module aeso_compiler The Sophia compiler @@ -403,24 +419,24 @@ This module provides the interface to the standard Sophia compiler. It returns the compiled module in a map which can then be loaded. Types -contract_string() = string() | binary() -contract_map() = #{bytecode => binary(), - compiler_version => binary(), - contract_souce => string(), - type_info => type_info()} -type_info() -errorstring() = binary() +contract_string() = string() | binary() +contract_map() = #{bytecode => binary(), + compiler_version => binary(), + contract_souce => string(), + type_info => type_info()} +type_info() +errorstring() = binary() Exports file(File) file(File, Options) -> CompRet from_string(ContractString, Options) -> CompRet Types -ContractString = contract_string() -Options = [Option] -CompRet = {ok,ContractMap} | {error,ErrorString} -ContractMap = contract_map() -ErrorString = errorstring() +ContractString = contract_string() +Options = [Option] +CompRet = {ok,ContractMap} | {error,ErrorString} +ContractMap = contract_map() +ErrorString = errorstring() Compile a contract defined in a file or in a string. The pp_ options all print to standard output the following: @@ -465,37 +481,38 @@ Type = term() Check a call in contract through the __call function. version() -> {ok, Version} | {error, term()} Types -Version = binary() +Version = binary() Get the current version of the Sophia compiler. - - - - - - - + + + + + + + + + + - - + + + + + + + @@ -81,11 +102,11 @@ - + - + @@ -107,20 +128,18 @@ - - + - - + @@ -129,26 +148,25 @@ - + - - + - - + + - - + + - - + + @@ -161,7 +179,7 @@ Initializing search - + @@ -170,11 +188,10 @@ - - + - + GitHub @@ -209,18 +226,17 @@ - + æternity Sophia Language - - + - + GitHub @@ -241,7 +257,7 @@ - + @@ -343,7 +359,6 @@ - @@ -357,12 +372,15 @@ - - - + + + - - Introduction + + + + +Introduction Sophia is a functional language designed for smart contract development. It is strongly typed and has restricted mutable state. Sophia is customized for smart contracts, which can be published @@ -376,54 +394,35 @@ some æternity blockchain specific primitive For playing around and diving deeper into the language itself check out the REPL! - - - - - - - + + + + + + + + + + - - + + + + + + + @@ -76,11 +95,11 @@ - + - + @@ -102,20 +121,18 @@ - - + - - + @@ -124,26 +141,25 @@ - + - - + - - + + - - + + - - + + @@ -156,7 +172,7 @@ Initializing search - + @@ -165,11 +181,10 @@ - - + - + GitHub @@ -204,18 +219,17 @@ - + æternity Sophia Language - - + - + GitHub @@ -322,43 +336,61 @@ + + + + + + + + + + + + + + + + - - - - - - Sophia - - This file has been moved here - - - + + + + - - - + +This file has been moved here + + + + + + + + + + + + - - + + + + + + + @@ -81,11 +104,11 @@ - + - + @@ -107,20 +130,18 @@ - - + - - + @@ -129,26 +150,25 @@ - + - - + - - + + - - + + - - + + @@ -161,7 +181,7 @@ Initializing search - + @@ -170,11 +190,10 @@ - - + - + GitHub @@ -209,18 +228,17 @@ - + æternity Sophia Language - - + - + GitHub @@ -301,7 +319,7 @@ - + @@ -318,7 +336,6 @@ - @@ -382,7 +399,6 @@ - @@ -418,75 +434,78 @@ - - - + + + - - Contract examples + + + + +Contract examples Crowdfunding /* * A simple crowd-funding example - */ -contract FundMe = + */ +contract FundMe = - record spend_args = { recipient : address, - amount : int } + record spend_args = { recipient : address, + amount : int } - record state = { contributions : map(address, int), - total : int, - beneficiary : address, - deadline : int, - goal : int } + record state = { contributions : map(address, int), + total : int, + beneficiary : address, + deadline : int, + goal : int } - stateful function spend(args : spend_args) = - Chain.spend(args.recipient, args.amount) + stateful function spend(args : spend_args) = + Chain.spend(args.recipient, args.amount) - entrypoint init(beneficiary, deadline, goal) : state = - { contributions = {}, - beneficiary = beneficiary, - deadline = deadline, - total = 0, - goal = goal } + entrypoint init(beneficiary, deadline, goal) : state = + { contributions = {}, + beneficiary = beneficiary, + deadline = deadline, + total = 0, + goal = goal } - function is_contributor(addr) = - Map.member(addr, state.contributions) + function is_contributor(addr) = + Map.member(addr, state.contributions) - stateful entrypoint contribute() = - if(Chain.block_height >= state.deadline) + stateful entrypoint contribute() = + if(Chain.block_height >= state.deadline) spend({ recipient = Call.caller, amount = Call.value }) // Refund money - false - else - let amount = - switch(Map.lookup(Call.caller, state.contributions)) - None => Call.value - Some(n) => n + Call.value - put(state{ contributions[Call.caller] = amount, - total @ tot = tot + Call.value }) - true + false + else + let amount = + switch(Map.lookup(Call.caller, state.contributions)) + None => Call.value + Some(n) => n + Call.value + put(state{ contributions[Call.caller] = amount, + total @ tot = tot + Call.value }) + true - stateful entrypoint withdraw() = - if(Chain.block_height < state.deadline) - abort("Cannot withdraw before deadline") - if(Call.caller == state.beneficiary) - withdraw_beneficiary() - elif(is_contributor(Call.caller)) - withdraw_contributor() - else - abort("Not a contributor or beneficiary") + stateful entrypoint withdraw() = + if(Chain.block_height < state.deadline) + abort("Cannot withdraw before deadline") + if(Call.caller == state.beneficiary) + withdraw_beneficiary() + elif(is_contributor(Call.caller)) + withdraw_contributor() + else + abort("Not a contributor or beneficiary") - stateful function withdraw_beneficiary() = - require(state.total >= state.goal, "Project was not funded") - spend({recipient = state.beneficiary, - amount = Contract.balance }) + stateful function withdraw_beneficiary() = + require(state.total >= state.goal, "Project was not funded") + spend({recipient = state.beneficiary, + amount = Contract.balance }) - stateful function withdraw_contributor() = - if(state.total >= state.goal) - abort("Project was funded") - let to = Call.caller - spend({recipient = to, - amount = state.contributions[to]}) - put(state{ contributions @ c = Map.delete(to, c) }) + stateful function withdraw_contributor() = + if(state.total >= state.goal) + abort("Project was funded") + let to = Call.caller + spend({recipient = to, + amount = state.contributions[to]}) + put(state{ contributions @ c = Map.delete(to, c) }) Repositories This is a list with repositories that include smart contracts written in Sophia: @@ -496,69 +515,35 @@ - - - - - - - + + + + + + + + + + - - + + + + + + + @@ -81,11 +104,11 @@ - + - + @@ -107,20 +130,18 @@ - - + - - + @@ -129,26 +150,25 @@ - + - - + - - + + - - + + - - + + @@ -161,7 +181,7 @@ Initializing search - + @@ -170,11 +190,10 @@ - - + - + GitHub @@ -209,18 +228,17 @@ - + æternity Sophia Language - - + - + GitHub @@ -271,7 +289,7 @@ - + @@ -288,7 +306,6 @@ - @@ -697,7 +714,6 @@ - @@ -1048,12 +1064,15 @@ - - - + + + - - Features + + + + +Features Contracts The main unit of code in Sophia is the contract. @@ -1075,22 +1094,22 @@ and the Call namespaces in the documentatio the contract. The type of the address must be a contract type, which consists of a number of type definitions and entrypoint declarations. For instance, // A contract type -contract interface VotingType = - entrypoint vote : string => unit +contract interface VotingType = + entrypoint vote : string => unit Now given contract address of type VotingType you can call the vote entrypoint of that contract: -contract VoteTwice = - entrypoint voteTwice(v : VotingType, alt : string) = - v.vote(alt) - v.vote(alt) +contract VoteTwice = + entrypoint voteTwice(v : VotingType, alt : string) = + v.vote(alt) + v.vote(alt) Contract calls take two optional named arguments gas : int and value : int that lets you set a gas limit and provide tokens to a contract call. If omitted the defaults are no gas limit and no tokens. Suppose there is a fee for voting: - entrypoint voteTwice(v : VotingType, fee : int, alt : string) = - v.vote(value = fee, alt) - v.vote(value = fee, alt) + entrypoint voteTwice(v : VotingType, fee : int, alt : string) = + v.vote(value = fee, alt) + v.vote(value = fee, alt) Named arguments can be given in any order. Note that reentrant calls are not permitted. In other words, when calling @@ -1104,8 +1123,8 @@ fails. To recover the underlying address of a contract instance there is a field address : address. For instance, to send tokens to the voting contract (given that it is payable) without calling it you can write - entrypoint pay(v : VotingType, amount : int) = - Chain.spend(v.address, amount) + entrypoint pay(v : VotingType, amount : int) = + Chain.spend(v.address, amount) Protected contract calls If a contract call fails for any reason (for instance, the remote contract @@ -1116,14 +1135,14 @@ contract calls takes a named argument protected : bool (default option type. If the call fails the result is None, otherwise it's Some(r) where r is the return value of the call. -contract interface VotingType = - entrypoint : vote : string => unit +contract interface VotingType = + entrypoint : vote : string => unit -contract Voter = - entrypoint tryVote(v : VotingType, alt : string) = - switch(v.vote(alt, protected = true) : option(unit)) - None => "Voting failed" - Some(_) => "Voting successful" +contract Voter = + entrypoint tryVote(v : VotingType, alt : string) = + switch(v.vote(alt, protected = true) : option(unit)) + None => "Voting failed" + Some(_) => "Voting successful" Any gas that was consumed by the contract call before the failure stays consumed, which means that in order to protect against the remote contract @@ -1145,15 +1164,15 @@ arguments – please refer to their documentation for the details. While Chain.clone requires only a contract interface and a living instance of a given contract on the chain, Chain.create needs a full definition of a to-create contract defined by the standard contract syntax, for example -contract IntHolder = - type state = int - entrypoint init(x) = x - entrypoint get() = state +contract IntHolder = + type state = int + entrypoint init(x) = x + entrypoint get() = state -main contract IntHolderFactory = - stateful entrypoint new(x : int) : IntHolder = - let ih = Chain.create(x) : IntHolder - ih +main contract IntHolderFactory = + stateful entrypoint new(x : int) : IntHolder = + let ih = Chain.create(x) : IntHolder + ih In case of a presence of child contracts (IntHolder in this case), the main contract must be pointed out with the main keyword as shown in the example. @@ -1229,21 +1248,21 @@ contract interface X : Z = A type is said to be on a "covariant" position when it describes output or a result of some computation. Analogously, position is "contravariant" when it is an input, or a parameter. Intuitively, when a part of the type is produced by values of it, it is covariant. When it is consumed, it is contravariant. When a type appears to be simultaneously input and output, it is described as invariant. If a type is neither of those (that is, it's unused) it's bivariant. Furthermore, whenever a complex type appears on a contravariant position, all its covariant components become contravariant and vice versa. Variance influences how subtyping is applied. Types on covariant positions are subtyped normally, while contravariant the opposite way. Invariant types have to be exactly the same in order for subtyping to work. Bivariant types are always compatible. A good example of where it matters can be pictured by subtyping of function types. Let us assume there is a contract interface Animal and two contracts that implement it: Dog and Cat. -contract interface Animal = - entrypoint age : () => int +contract interface Animal = + entrypoint age : () => int -contract Dog : Animal = +contract Dog : Animal = entrypoint age() = // ... - entrypoint woof() = "woof" + entrypoint woof() = "woof" -contract Cat : Animal = +contract Cat : Animal = entrypoint age() = // ... - entrypoint meow() = "meow" + entrypoint meow() = "meow" The assumption of this exercise is that cats do not bark (because Cat does not define the woof entrypoint). If subtyping rules were applied naively, that is if we let Dog => Dog be a subtype of Animal => Animal, the following code would break: -let f : (Dog) => string = d => d.woof() -let g : (Animal) => string = f -let c : Cat = Chain.create() +let f : (Dog) => string = d => d.woof() +let g : (Animal) => string = f +let c : Cat = Chain.create() g(c) // Cat barking! That is because arguments of functions are contravariant, as opposed to return the type which is covariant. Because of that, the assignment of f to g is invalid - while Dog is a subtype of Animal, Dog => string is not a subtype of Animal => string. However, Animal => string is a subtype of Dog => string. More than that, (Dog => Animal) => Dog is a subtype of (Animal => Dog) => Animal. @@ -1331,8 +1350,8 @@ provides special syntax for map/record updates. Top-level functions and entrypoints must be annotated with the stateful keyword to be allowed to affect the state of the running contract. For instance, - stateful entrypoint set_state(s : state) = - put(s) + stateful entrypoint set_state(s : state) = + put(s) Without the stateful annotation the compiler does not allow the call to put. A stateful annotation is required to @@ -1364,8 +1383,8 @@ For instance, a contract (either a Chain.spend or a normal spend transaction) will fail. If a contract shall be able to receive funds in this way it has to be declared payable: // A payable contract -payable contract ExampleContract = - stateful entrypoint do_stuff() = ... +payable contract ExampleContract = + stateful entrypoint do_stuff() = ... If in doubt, it is possible to check if an address is payable using Address.is_payable(addr). @@ -1374,11 +1393,11 @@ contract shall be able to receive funds in this way it has to be declared (either a Remote call or a contract call transaction) that has a non-zero value will fail. Contract entrypoints that should be called with a non-zero value should be declared payable. -payable stateful entrypoint buy(to : address) = - if(Call.value > 42) - transfer_item(to) - else - abort("Value too low") +payable stateful entrypoint buy(to : address) = + if(Call.value > 42) + transfer_item(to) + else + abort("Value too low") Namespaces Code can be split into libraries using the namespace construct. Namespaces @@ -1386,13 +1405,13 @@ can appear at the top-level and can contain type and function definitions, but not entrypoints. Outside the namespace you can refer to the (non-private) names by qualifying them with the namespace (Namespace.name). For example, -namespace Library = - type number = int - function inc(x : number) : number = x + 1 +namespace Library = + type number = int + function inc(x : number) : number = x + 1 -contract MyContract = - entrypoint plus2(x) : Library.number = - Library.inc(Library.inc(x)) +contract MyContract = + entrypoint plus2(x) : Library.number = + Library.inc(Library.inc(x)) Functions in namespaces have access to the same environment (including the Chain, Call, and Contract, builtin namespaces) as function in a contract, @@ -1452,13 +1471,13 @@ contract level, namespace level, or in the function level. statement. These must appear at the top-level (outside the main contract). The included file can contain one or more namespaces and abstract contracts. For example, if the file library.aes contains -namespace Library = - function inc(x) = x + 1 +namespace Library = + function inc(x) = x + 1 you can use it from another file using an include: -include "library.aes" -contract MyContract = - entrypoint plus2(x) = Library.inc(Library.inc(x)) +include "library.aes" +contract MyContract = + entrypoint plus2(x) = Library.inc(Library.inc(x)) This behaves as if the contents of library.aes was textually inserted into the file, except that error messages will refer to the original source @@ -1471,13 +1490,13 @@ namespaces like Chain, Contract, Map are included by default and are supported internally by the compiler. Others like List, Frac, Option need to be manually included using the include directive. For example -include "List.aes" -include "Pair.aes" --- Map is already there! +include "List.aes" +include "Pair.aes" +-- Map is already there! -namespace C = - entrypoint keys(m : map('a, 'b)) : list('a) = - List.map(Pair.fst, (Map.to_list(m))) +namespace C = + entrypoint keys(m : map('a, 'b)) : list('a) = + List.map(Pair.fst, (Map.to_list(m))) Types Sophia has the following types: @@ -1707,8 +1726,8 @@ corresponding integer, so setting very high bits can be expensive). Type aliases Type aliases can be introduced with the type keyword and can be parameterized. For instance -type number = int -type string_map('a) = map(string, 'a) +type number = int +type string_map('a) = map(string, 'a) A type alias and its definition can be used interchangeably. Sophia does not support higher-kinded types, meaning that following type alias is invalid: type wrap('f, 'a) = 'f('a) @@ -1716,47 +1735,47 @@ higher-kinded types, meaning that following type alias is invalid: type wr Sophia supports algebraic data types (variant types) and pattern matching. Data types are declared by giving a list of constructors with their respective arguments. For instance, -datatype one_or_both('a, 'b) = Left('a) | Right('b) | Both('a, 'b) +datatype one_or_both('a, 'b) = Left('a) | Right('b) | Both('a, 'b) Elements of data types can be pattern matched against, using the switch construct: -function get_left(x : one_or_both('a, 'b)) : option('a) = - switch(x) - Left(x) => Some(x) - Right(_) => None - Both(x, _) => Some(x) +function get_left(x : one_or_both('a, 'b)) : option('a) = + switch(x) + Left(x) => Some(x) + Right(_) => None + Both(x, _) => Some(x) or directly in the left-hand side: -function - get_left : one_or_both('a, 'b) => option('a) - get_left(Left(x)) = Some(x) - get_left(Right(_)) = None - get_left(Both(x, _)) = Some(x) +function + get_left : one_or_both('a, 'b) => option('a) + get_left(Left(x)) = Some(x) + get_left(Right(_)) = None + get_left(Both(x, _)) = Some(x) NOTE: Data types cannot currently be recursive. Sophia also supports the assignment of patterns to variables: -function f(x) = switch(x) +function f(x) = switch(x) h1::(t = h2::_) => (h1 + h2)::t // same as `h1::h2::k => (h1 + h2)::h2::k` - _ => x + _ => x -function g(p : int * option(int)) : int = +function g(p : int * option(int)) : int = let (a, (o = Some(b))) = p // o is equal to Pair.snd(p) - b + b Guards are boolean expressions that can be used on patterns in both switch statements and functions definitions. If a guard expression evaluates to true, then the corresponding body will be used. Otherwise, the next pattern will be checked: -function get_left_if_positive(x : one_or_both(int, 'b)) : option(int) = - switch(x) - Left(x) | x > 0 => Some(x) - Both(x, _) | x > 0 => Some(x) - _ => None +function get_left_if_positive(x : one_or_both(int, 'b)) : option(int) = + switch(x) + Left(x) | x > 0 => Some(x) + Both(x, _) | x > 0 => Some(x) + _ => None -function - get_left_if_positive : one_or_both(int, 'b) => option(int) - get_left_if_positive(Left(x)) | x > 0 = Some(x) - get_left_if_positive(Both(x, _)) | x > 0 = Some(x) - get_left_if_positive(_) = None +function + get_left_if_positive : one_or_both(int, 'b) => option(int) + get_left_if_positive(Left(x)) | x > 0 = Some(x) + get_left_if_positive(Both(x, _)) | x > 0 = Some(x) + get_left_if_positive(_) = None Guards cannot be stateful even when used inside a stateful function. Lists @@ -1765,9 +1784,9 @@ linked list. A list is constructed with the syntax [1, 2, 3]. The elements of a list can be any of datatype but they must have the same type. The type of lists with elements of type 'e is written list('e). For example we can have the following lists: -[1, 33, 2, 666] : list(int) -[(1, "aaa"), (10, "jjj"), (666, "the beast")] : list(int * string) -[{[1] = "aaa", [10] = "jjj"}, {[5] = "eee", [666] = "the beast"}] : list(map(int, string)) +[1, 33, 2, 666] : list(int) +[(1, "aaa"), (10, "jjj"), (666, "the beast")] : list(int * string) +[{[1] = "aaa", [10] = "jjj"}, {[5] = "eee", [666] = "the beast"}] : list(map(int, string)) New elements can be prepended to the front of a list with the :: operator. So 42 :: [1, 2, 3] returns the list [42, 1, 2, 3]. The @@ -1776,20 +1795,20 @@ and returns the resulting list. So concatenating two lists [1, 22, 33] ++ [10, 18, 55] returns the list [1, 22, 33, 10, 18, 55]. Sophia supports list comprehensions known from languages like Python, Haskell or Erlang. Example syntax: -[x + y | x <- [1,2,3,4,5], let k = x*x, if (k > 5), y <- [k, k+1, k+2]] +[x + y | x <- [1,2,3,4,5], let k = x*x, if (k > 5), y <- [k, k+1, k+2]] // yields [12,13,14,20,21,22,30,31,32] Lists can be constructed using the range syntax using special .. operator: -[1..4] == [1,2,3,4] +[1..4] == [1,2,3,4] The ranges are always ascending and have step equal to 1. Please refer to the standard library for the predefined functionalities. Maps and records A Sophia record type is given by a fixed set of fields with associated, possibly different, types. For instance - record account = { name : string, - balance : int, - history : list(transaction) } + record account = { name : string, + balance : int, + history : list(transaction) } Maps, on the other hand, can contain an arbitrary number of key-value bindings, but of a fixed type. The type of maps with keys of type 'k and values of type @@ -1799,18 +1818,18 @@ contain a map or a function type. Constructing maps and records A value of record type is constructed by giving a value for each of the fields. For the example above, - function new_account(name) = - {name = name, balance = 0, history = []} + function new_account(name) = + {name = name, balance = 0, history = []} Maps are constructed similarly, with keys enclosed in square brackets - function example_map() : map(string, int) = - {["key1"] = 1, ["key2"] = 2} + function example_map() : map(string, int) = + {["key1"] = 1, ["key2"] = 2} The empty map is written {}. Accessing values Record fields access is written r.f and map lookup m[k]. For instance, - function get_balance(a : address, accounts : map(address, account)) = - accounts[a].balance + function get_balance(a : address, accounts : map(address, account)) = + accounts[a].balance Looking up a non-existing key in a map results in contract execution failing. A default value to return for non-existing keys can be provided using the syntax @@ -1829,13 +1848,13 @@ in the map or execution fails, but a default value can be provided: m{ [k = default] @ x = v }. In this case x is bound to default if k is not in the map. Updates can be nested: -function clear_history(a : address, accounts : map(address, account)) : map(address, account) = - accounts{ [a].history = [] } +function clear_history(a : address, accounts : map(address, account)) : map(address, account) = + accounts{ [a].history = [] } This is equivalent to accounts{ [a] @ acc = acc{ history = [] } } and thus requires a to be present in the accounts map. To have clear_history create an account if a is not in the map you can write (given a function empty_account): - accounts{ [a = empty_account()].history = [] } + accounts{ [a = empty_account()].history = [] } Map implementation Internally in the VM maps are implemented as hash maps and support fast lookup @@ -1875,53 +1894,53 @@ through the Oracle interface. For a functionality documentation refer to the standard library. Example Example for an oracle answering questions of type string with answers of type int: -contract Oracles = +contract Oracles = - stateful entrypoint registerOracle(acct : address, + stateful entrypoint registerOracle(acct : address, sign : signature, // Signed network id + oracle address + contract address - qfee : int, - ttl : Chain.ttl) : oracle(string, int) = - Oracle.register(acct, signature = sign, qfee, ttl) + qfee : int, + ttl : Chain.ttl) : oracle(string, int) = + Oracle.register(acct, signature = sign, qfee, ttl) - entrypoint queryFee(o : oracle(string, int)) : int = - Oracle.query_fee(o) + entrypoint queryFee(o : oracle(string, int)) : int = + Oracle.query_fee(o) - payable stateful entrypoint createQuery(o : oracle_query(string, int), - q : string, - qfee : int, - qttl : Chain.ttl, - rttl : int) : oracle_query(string, int) = - require(qfee =< Call.value, "insufficient value for qfee") - Oracle.query(o, q, qfee, qttl, RelativeTTL(rttl)) + payable stateful entrypoint createQuery(o : oracle_query(string, int), + q : string, + qfee : int, + qttl : Chain.ttl, + rttl : int) : oracle_query(string, int) = + require(qfee =< Call.value, "insufficient value for qfee") + Oracle.query(o, q, qfee, qttl, RelativeTTL(rttl)) - stateful entrypoint extendOracle(o : oracle(string, int), - ttl : Chain.ttl) : unit = - Oracle.extend(o, ttl) + stateful entrypoint extendOracle(o : oracle(string, int), + ttl : Chain.ttl) : unit = + Oracle.extend(o, ttl) - stateful entrypoint signExtendOracle(o : oracle(string, int), + stateful entrypoint signExtendOracle(o : oracle(string, int), sign : signature, // Signed network id + oracle address + contract address - ttl : Chain.ttl) : unit = - Oracle.extend(o, signature = sign, ttl) + ttl : Chain.ttl) : unit = + Oracle.extend(o, signature = sign, ttl) - stateful entrypoint respond(o : oracle(string, int), - q : oracle_query(string, int), + stateful entrypoint respond(o : oracle(string, int), + q : oracle_query(string, int), sign : signature, // Signed network id + oracle query id + contract address - r : int) = - Oracle.respond(o, q, signature = sign, r) + r : int) = + Oracle.respond(o, q, signature = sign, r) - entrypoint getQuestion(o : oracle(string, int), - q : oracle_query(string, int)) : string = - Oracle.get_question(o, q) + entrypoint getQuestion(o : oracle(string, int), + q : oracle_query(string, int)) : string = + Oracle.get_question(o, q) - entrypoint hasAnswer(o : oracle(string, int), - q : oracle_query(string, int)) = - switch(Oracle.get_answer(o, q)) - None => false - Some(_) => true + entrypoint hasAnswer(o : oracle(string, int), + q : oracle_query(string, int)) = + switch(Oracle.get_answer(o, q)) + None => false + Some(_) => true - entrypoint getAnswer(o : oracle(string, int), - q : oracle_query(string, int)) : option(int) = - Oracle.get_answer(o, q) + entrypoint getAnswer(o : oracle(string, int), + q : oracle_query(string, int)) : option(int) = + Oracle.get_answer(o, q) Sanity checks When an Oracle literal is passed to a contract, no deep checks are performed. @@ -1938,29 +1957,29 @@ an account with address addr. In order to allow a contract ct signature sig of addr | name.hash | ct.address. Armed with this information we can for example write a function that extends the name if it expires within 1000 blocks: - stateful entrypoint extend_if_necessary(addr : address, name : string, sig : signature) = - switch(AENS.lookup(name)) - None => () - Some(AENS.Name(_, FixedTTL(expiry), _)) => - if(Chain.block_height + 1000 > expiry) - AENS.update(addr, name, Some(RelativeTTL(50000)), None, None, signature = sig) + stateful entrypoint extend_if_necessary(addr : address, name : string, sig : signature) = + switch(AENS.lookup(name)) + None => () + Some(AENS.Name(_, FixedTTL(expiry), _)) => + if(Chain.block_height + 1000 > expiry) + AENS.update(addr, name, Some(RelativeTTL(50000)), None, None, signature = sig) And we can write functions that adds and removes keys from the pointers of the name: - stateful entrypoint add_key(addr : address, name : string, key : string, - pt : AENS.pointee, sig : signature) = - switch(AENS.lookup(name)) - None => () - Some(AENS.Name(_, _, ptrs)) => - AENS.update(addr, name, None, None, Some(ptrs{[key] = pt}), signature = sig) + stateful entrypoint add_key(addr : address, name : string, key : string, + pt : AENS.pointee, sig : signature) = + switch(AENS.lookup(name)) + None => () + Some(AENS.Name(_, _, ptrs)) => + AENS.update(addr, name, None, None, Some(ptrs{[key] = pt}), signature = sig) - stateful entrypoint delete_key(addr : address, name : string, - key : string, sig : signature) = - switch(AENS.lookup(name)) - None => () - Some(AENS.Name(_, _, ptrs)) => - let ptrs = Map.delete(key, ptrs) - AENS.update(addr, name, None, None, Some(ptrs), signature = sig) + stateful entrypoint delete_key(addr : address, name : string, + key : string, sig : signature) = + switch(AENS.lookup(name)) + None => () + Some(AENS.Name(_, _, ptrs)) => + let ptrs = Map.delete(key, ptrs) + AENS.update(addr, name, None, None, Some(ptrs), signature = sig) Note: From the Iris hardfork more strict rules apply for AENS pointers, when a Sophia contract lookup or update (bad) legacy pointers, the bad keys are @@ -1972,11 +1991,11 @@ Solidity. Events are further discussed in the protocol. To use events a contract must declare a datatype event, and events are then logged using the Chain.event function: - datatype event - = Event1(int, int, string) - | Event2(string, address) + datatype event + = Event1(int, int, string) + | Event2(string, address) - Chain.event(e : event) : unit + Chain.event(e : event) : unit The event can have 0-3 indexed fields, and an optional payload field. A field is indexed if it fits in a 32-byte word, i.e. @@ -1993,18 +2012,18 @@ The fields can appear in any order. NOTE: Indexing is not part of the core æternity node. Events are emitted by using the Chain.event function. The following function will emit one Event of each kind in the example. - entrypoint emit_events() : () = - Chain.event(Event1(42, 34, "foo")) - Chain.event(Event2("This is not indexed", Contract.address)) + entrypoint emit_events() : () = + Chain.event(Event1(42, 34, "foo")) + Chain.event(Event2("This is not indexed", Contract.address)) Argument order It is only possible to have one (1) string parameter in the event, but it can be placed in any position (and its value will end up in the data field), i.e. -AnotherEvent(string, indexed address) +AnotherEvent(string, indexed address) -... +... -Chain.event(AnotherEvent("This is not indexed", Contract.address)) +Chain.event(AnotherEvent("This is not indexed", Contract.address)) would yield exactly the same result in the example above! Compiler pragmas @@ -2012,8 +2031,8 @@ would yield exactly the same result in the example above! Sophia compiler, you can give one or more @compiler pragmas at the top-level (typically at the beginning) of a file. For instance, to enforce that a contract is compiled with version 4.3 of the compiler you write -@compiler >= 4.3 -@compiler < 4.4 +@compiler >= 4.3 +@compiler < 4.4 Valid operators in compiler pragmas are <, =<, ==, >=, and >. Version numbers are given as a sequence of non-negative integers separated by dots. @@ -2021,18 +2040,18 @@ Trailing zeros are ignored, so 4.0.0 == 4. If a constraint is viola error is reported and compilation fails. Exceptions Contracts can fail with an (uncatchable) exception using the built-in function -abort(reason : string) : 'a +abort(reason : string) : 'a Calling abort causes the top-level call transaction to return an error result containing the reason string. Only the gas used up to and including the abort call is charged. This is different from termination due to a crash which consumes all available gas. For convenience the following function is also built-in: -function require(b : bool, err : string) = - if(!b) abort(err) +function require(b : bool, err : string) = + if(!b) abort(err) Aside from that, there is an almost equivalent function exit -exit(reason : string) : 'a +exit(reason : string) : 'a Just like abort, it breaks the execution with the given reason. The difference however is in the gas consumption — while abort returns unused gas, a call to @@ -2043,69 +2062,35 @@ optional delegation signature. This is typically used when a user/accounts would like to allow a contract to act on it's behalf. The exact data to be signed varies for the different operations, but in all cases you should prepend the signature data with the network_id (ae_mainnet for the æternity mainnet, etc.). - - - - - - - + + + + + + + + + + - - + + + + + + + @@ -81,11 +104,11 @@ - + - + @@ -107,20 +130,18 @@ - - + - - + @@ -129,26 +150,25 @@ - + - - + - - + + - - + + - - + + @@ -161,7 +181,7 @@ Initializing search - + @@ -170,11 +190,10 @@ - - + - + GitHub @@ -209,18 +228,17 @@ - + æternity Sophia Language - - + - + GitHub @@ -286,7 +304,7 @@ - + @@ -303,7 +321,6 @@ - @@ -438,7 +455,7 @@ - BLS1295381 + BLS12_381 @@ -555,7 +572,6 @@ - @@ -690,7 +706,7 @@ - BLS1295381 + BLS12_381 @@ -764,12 +780,15 @@ - - - + + + - - GitHub @@ -209,18 +228,17 @@ - + æternity Sophia Language - - + - + GitHub @@ -256,7 +274,7 @@ - + @@ -273,7 +291,6 @@ - @@ -458,7 +475,6 @@ - @@ -570,12 +586,15 @@ - - - + + + - - Syntax + + + + +Syntax Lexical syntax Comments Single line comments start with // and block comments are enclosed in /* @@ -662,11 +681,11 @@ indented more than the currently enclosing layout block. Blocks with a single element can be written on the same line as the previous token. Each element of the block must share the same indentation and no part of an element may be indented less than the indentation of the block. For instance -contract Layout = +contract Layout = function foo() = 0 // no layout function bar() = // layout block starts on next line let x = foo() // indented more than 2 spaces - x + x + 1 // the '+' is indented more than the 'x' Notation @@ -687,107 +706,107 @@ element may be indented less than the indentation of the block. For instance Declarations A Sophia file consists of a sequence of declarations in a layout block. -File ::= Block(TopDecl) +File ::= Block(TopDecl) -TopDecl ::= ['payable'] ['main'] 'contract' Con [Implement] '=' Block(Decl) - | 'contract' 'interface' Con [Implement] '=' Block(Decl) - | 'namespace' Con '=' Block(Decl) - | '@compiler' PragmaOp Version - | 'include' String - | Using +TopDecl ::= ['payable'] ['main'] 'contract' Con [Implement] '=' Block(Decl) + | 'contract' 'interface' Con [Implement] '=' Block(Decl) + | 'namespace' Con '=' Block(Decl) + | '@compiler' PragmaOp Version + | 'include' String + | Using -Implement ::= ':' Sep1(Con, ',') +Implement ::= ':' Sep1(Con, ',') -Decl ::= 'type' Id ['(' TVar* ')'] '=' TypeAlias - | 'record' Id ['(' TVar* ')'] '=' RecordType - | 'datatype' Id ['(' TVar* ')'] '=' DataType - | (EModifier* 'entrypoint' | FModifier* 'function') Block(FunDecl) - | Using +Decl ::= 'type' Id ['(' TVar* ')'] '=' TypeAlias + | 'record' Id ['(' TVar* ')'] '=' RecordType + | 'datatype' Id ['(' TVar* ')'] '=' DataType + | (EModifier* 'entrypoint' | FModifier* 'function') Block(FunDecl) + | Using FunDecl ::= Id ':' Type // Type signature | Id Args [':' Type] '=' Block(Stmt) // Definition | Id Args [':' Type] Block(GuardedDef) // Guarded definitions -GuardedDef ::= '|' Sep1(Expr, ',') '=' Block(Stmt) +GuardedDef ::= '|' Sep1(Expr, ',') '=' Block(Stmt) -Using ::= 'using' Con ['as' Con] [UsingParts] -UsingParts ::= 'for' '[' Sep1(Id, ',') ']' - | 'hiding' '[' Sep1(Id, ',') ']' +Using ::= 'using' Con ['as' Con] [UsingParts] +UsingParts ::= 'for' '[' Sep1(Id, ',') ']' + | 'hiding' '[' Sep1(Id, ',') ']' -PragmaOp ::= '<' | '=<' | '==' | '>=' | '>' -Version ::= Sep1(Int, '.') +PragmaOp ::= '<' | '=<' | '==' | '>=' | '>' +Version ::= Sep1(Int, '.') -EModifier ::= 'payable' | 'stateful' -FModifier ::= 'stateful' | 'private' +EModifier ::= 'payable' | 'stateful' +FModifier ::= 'stateful' | 'private' -Args ::= '(' Sep(Pattern, ',') ')' +Args ::= '(' Sep(Pattern, ',') ')' Contract declarations must appear at the top-level. For example, -contract Test = - type t = int - entrypoint add (x : t, y : t) = x + y +contract Test = + type t = int + entrypoint add (x : t, y : t) = x + y There are three forms of type declarations: type aliases (declared with the type keyword), record type definitions (record) and data type definitions (datatype): -TypeAlias ::= Type -RecordType ::= '{' Sep(FieldType, ',') '}' -DataType ::= Sep1(ConDecl, '|') +TypeAlias ::= Type +RecordType ::= '{' Sep(FieldType, ',') '}' +DataType ::= Sep1(ConDecl, '|') -FieldType ::= Id ':' Type -ConDecl ::= Con ['(' Sep1(Type, ',') ')'] +FieldType ::= Id ':' Type +ConDecl ::= Con ['(' Sep1(Type, ',') ')'] For example, -record point('a) = {x : 'a, y : 'a} -datatype shape('a) = Circle(point('a), 'a) | Rect(point('a), point('a)) -type int_shape = shape(int) +record point('a) = {x : 'a, y : 'a} +datatype shape('a) = Circle(point('a), 'a) | Rect(point('a), point('a)) +type int_shape = shape(int) Types Type ::= Domain '=>' Type // Function type | Type '(' Sep(Type, ',') ')' // Type application | '(' Type ')' // Parens | 'unit' | Sep(Type, '*') // Tuples - | Id | QId | TVar + | Id | QId | TVar Domain ::= Type // Single argument | '(' Sep(Type, ',') ')' // Multiple arguments The function type arrow associates to the right. Example, -'a => list('a) => (int * list('a)) +'a => list('a) => (int * list('a)) Statements Function bodies are blocks of statements, where a statement is one of the following -Stmt ::= 'switch' '(' Expr ')' Block(Case) - | 'if' '(' Expr ')' Block(Stmt) - | 'elif' '(' Expr ')' Block(Stmt) - | 'else' Block(Stmt) - | 'let' LetDef - | Using - | Expr +Stmt ::= 'switch' '(' Expr ')' Block(Case) + | 'if' '(' Expr ')' Block(Stmt) + | 'elif' '(' Expr ')' Block(Stmt) + | 'else' Block(Stmt) + | 'let' LetDef + | Using + | Expr LetDef ::= Id Args [':' Type] '=' Block(Stmt) // Function definition | Pattern '=' Block(Stmt) // Value definition -Case ::= Pattern '=>' Block(Stmt) - | Pattern Block(GuardedCase) +Case ::= Pattern '=>' Block(Stmt) + | Pattern Block(GuardedCase) -GuardedCase ::= '|' Sep1(Expr, ',') '=>' Block(Stmt) +GuardedCase ::= '|' Sep1(Expr, ',') '=>' Block(Stmt) -Pattern ::= Expr +Pattern ::= Expr if statements can be followed by zero or more elif statements and an optional final else statement. For example, -let x : int = 4 -switch(f(x)) - None => 0 - Some(y) => - if(y > 10) - "too big" - elif(y < 3) - "too small" - else - "just right" +let x : int = 4 +switch(f(x)) + None => 0 + Some(y) => + if(y > 10) + "too big" + elif(y < 3) + "too small" + else + "just right" Expressions Expr ::= '(' LamArgs ')' '=>' Block(Stmt) // Anonymous function (x) => x + 1 @@ -801,7 +820,7 @@ element may be indented less than the indentation of the block. For instance | Expr '[' Expr ']' // Map lookup map[key] | Expr '{' Sep(FieldUpdate, ',') '}' // Record or map update r{ fld[key].x = y } | '[' Sep(Expr, ',') ']' // List [1, 2, 3] - | '[' Expr '|' Sep(Generator, ',') ']' + | '[' Expr '|' Sep(Generator, ',') ']' // List comprehension [k | x <- [1], if (f(x)), let k = x+1] | '[' Expr '..' Expr ']' // List range [1..n] | '{' Sep(FieldUpdate, ',') '}' // Record or map value {x = 0, y = 1}, {[key] = val} @@ -817,19 +836,19 @@ element may be indented less than the indentation of the block. For instance | 'if' '(' Expr ')' // Guard | LetDef // Definition -LamArgs ::= '(' Sep(LamArg, ',') ')' -LamArg ::= Id [':' Type] +LamArgs ::= '(' Sep(LamArg, ',') ')' +LamArg ::= Id [':' Type] -FieldUpdate ::= Path '=' Expr +FieldUpdate ::= Path '=' Expr Path ::= Id // Record field | '[' Expr ']' // Map key | Path '.' Id // Nested record field | Path '[' Expr ']' // Nested map key -BinOp ::= '||' | '&&' | '<' | '>' | '=<' | '>=' | '==' | '!=' - | '::' | '++' | '+' | '-' | '*' | '/' | 'mod' | '^' - | '|>' -UnOp ::= '-' | '!' +BinOp ::= '||' | '&&' | '<' | '>' | '=<' | '>=' | '==' | '!=' + | '::' | '++' | '+' | '-' | '*' | '/' | 'mod' | '^' + | '|>' +UnOp ::= '-' | '!' Operators types @@ -914,69 +933,35 @@ element may be indented less than the indentation of the block. For instance - - - - - - - + + + + + + + + + + - -
- - aeso_compiler + + + + +aeso_compiler Module aeso_compiler The Sophia compiler @@ -403,24 +419,24 @@ This module provides the interface to the standard Sophia compiler. It returns the compiled module in a map which can then be loaded. Types -contract_string() = string() | binary() -contract_map() = #{bytecode => binary(), - compiler_version => binary(), - contract_souce => string(), - type_info => type_info()} -type_info() -errorstring() = binary() +contract_string() = string() | binary() +contract_map() = #{bytecode => binary(), + compiler_version => binary(), + contract_souce => string(), + type_info => type_info()} +type_info() +errorstring() = binary() Exports file(File) file(File, Options) -> CompRet from_string(ContractString, Options) -> CompRet Types -ContractString = contract_string() -Options = [Option] -CompRet = {ok,ContractMap} | {error,ErrorString} -ContractMap = contract_map() -ErrorString = errorstring() +ContractString = contract_string() +Options = [Option] +CompRet = {ok,ContractMap} | {error,ErrorString} +ContractMap = contract_map() +ErrorString = errorstring() Compile a contract defined in a file or in a string. The pp_ options all print to standard output the following: @@ -465,37 +481,38 @@ Type = term() Check a call in contract through the __call function. version() -> {ok, Version} | {error, term()} Types -Version = binary() +Version = binary() Get the current version of the Sophia compiler. - - - - - - - + + + + + + + + + + - -
- + + + - - Introduction + + + + +Introduction Sophia is a functional language designed for smart contract development. It is strongly typed and has restricted mutable state. Sophia is customized for smart contracts, which can be published @@ -376,54 +394,35 @@ some æternity blockchain specific primitive For playing around and diving deeper into the language itself check out the REPL! - - - - - -
- - Introduction + + + + +Introduction Sophia is a functional language designed for smart contract development. It is strongly typed and has restricted mutable state. Sophia is customized for smart contracts, which can be published @@ -376,54 +394,35 @@ some æternity blockchain specific primitive For playing around and diving deeper into the language itself check out the REPL!
- - - - Sophia - - This file has been moved here - - - + + + + - - - + +This file has been moved here + + + + + + +
- + + + - - Contract examples + + + + +Contract examples Crowdfunding /* * A simple crowd-funding example - */ -contract FundMe = + */ +contract FundMe = - record spend_args = { recipient : address, - amount : int } + record spend_args = { recipient : address, + amount : int } - record state = { contributions : map(address, int), - total : int, - beneficiary : address, - deadline : int, - goal : int } + record state = { contributions : map(address, int), + total : int, + beneficiary : address, + deadline : int, + goal : int } - stateful function spend(args : spend_args) = - Chain.spend(args.recipient, args.amount) + stateful function spend(args : spend_args) = + Chain.spend(args.recipient, args.amount) - entrypoint init(beneficiary, deadline, goal) : state = - { contributions = {}, - beneficiary = beneficiary, - deadline = deadline, - total = 0, - goal = goal } + entrypoint init(beneficiary, deadline, goal) : state = + { contributions = {}, + beneficiary = beneficiary, + deadline = deadline, + total = 0, + goal = goal } - function is_contributor(addr) = - Map.member(addr, state.contributions) + function is_contributor(addr) = + Map.member(addr, state.contributions) - stateful entrypoint contribute() = - if(Chain.block_height >= state.deadline) + stateful entrypoint contribute() = + if(Chain.block_height >= state.deadline) spend({ recipient = Call.caller, amount = Call.value }) // Refund money - false - else - let amount = - switch(Map.lookup(Call.caller, state.contributions)) - None => Call.value - Some(n) => n + Call.value - put(state{ contributions[Call.caller] = amount, - total @ tot = tot + Call.value }) - true + false + else + let amount = + switch(Map.lookup(Call.caller, state.contributions)) + None => Call.value + Some(n) => n + Call.value + put(state{ contributions[Call.caller] = amount, + total @ tot = tot + Call.value }) + true - stateful entrypoint withdraw() = - if(Chain.block_height < state.deadline) - abort("Cannot withdraw before deadline") - if(Call.caller == state.beneficiary) - withdraw_beneficiary() - elif(is_contributor(Call.caller)) - withdraw_contributor() - else - abort("Not a contributor or beneficiary") + stateful entrypoint withdraw() = + if(Chain.block_height < state.deadline) + abort("Cannot withdraw before deadline") + if(Call.caller == state.beneficiary) + withdraw_beneficiary() + elif(is_contributor(Call.caller)) + withdraw_contributor() + else + abort("Not a contributor or beneficiary") - stateful function withdraw_beneficiary() = - require(state.total >= state.goal, "Project was not funded") - spend({recipient = state.beneficiary, - amount = Contract.balance }) + stateful function withdraw_beneficiary() = + require(state.total >= state.goal, "Project was not funded") + spend({recipient = state.beneficiary, + amount = Contract.balance }) - stateful function withdraw_contributor() = - if(state.total >= state.goal) - abort("Project was funded") - let to = Call.caller - spend({recipient = to, - amount = state.contributions[to]}) - put(state{ contributions @ c = Map.delete(to, c) }) + stateful function withdraw_contributor() = + if(state.total >= state.goal) + abort("Project was funded") + let to = Call.caller + spend({recipient = to, + amount = state.contributions[to]}) + put(state{ contributions @ c = Map.delete(to, c) }) Repositories This is a list with repositories that include smart contracts written in Sophia: @@ -496,69 +515,35 @@ - - - - - - - + + + + +
- - Contract examples + + + + +Contract examples Crowdfunding /* * A simple crowd-funding example - */ -contract FundMe = + */ +contract FundMe = - record spend_args = { recipient : address, - amount : int } + record spend_args = { recipient : address, + amount : int } - record state = { contributions : map(address, int), - total : int, - beneficiary : address, - deadline : int, - goal : int } + record state = { contributions : map(address, int), + total : int, + beneficiary : address, + deadline : int, + goal : int } - stateful function spend(args : spend_args) = - Chain.spend(args.recipient, args.amount) + stateful function spend(args : spend_args) = + Chain.spend(args.recipient, args.amount) - entrypoint init(beneficiary, deadline, goal) : state = - { contributions = {}, - beneficiary = beneficiary, - deadline = deadline, - total = 0, - goal = goal } + entrypoint init(beneficiary, deadline, goal) : state = + { contributions = {}, + beneficiary = beneficiary, + deadline = deadline, + total = 0, + goal = goal } - function is_contributor(addr) = - Map.member(addr, state.contributions) + function is_contributor(addr) = + Map.member(addr, state.contributions) - stateful entrypoint contribute() = - if(Chain.block_height >= state.deadline) + stateful entrypoint contribute() = + if(Chain.block_height >= state.deadline) spend({ recipient = Call.caller, amount = Call.value }) // Refund money - false - else - let amount = - switch(Map.lookup(Call.caller, state.contributions)) - None => Call.value - Some(n) => n + Call.value - put(state{ contributions[Call.caller] = amount, - total @ tot = tot + Call.value }) - true + false + else + let amount = + switch(Map.lookup(Call.caller, state.contributions)) + None => Call.value + Some(n) => n + Call.value + put(state{ contributions[Call.caller] = amount, + total @ tot = tot + Call.value }) + true - stateful entrypoint withdraw() = - if(Chain.block_height < state.deadline) - abort("Cannot withdraw before deadline") - if(Call.caller == state.beneficiary) - withdraw_beneficiary() - elif(is_contributor(Call.caller)) - withdraw_contributor() - else - abort("Not a contributor or beneficiary") + stateful entrypoint withdraw() = + if(Chain.block_height < state.deadline) + abort("Cannot withdraw before deadline") + if(Call.caller == state.beneficiary) + withdraw_beneficiary() + elif(is_contributor(Call.caller)) + withdraw_contributor() + else + abort("Not a contributor or beneficiary") - stateful function withdraw_beneficiary() = - require(state.total >= state.goal, "Project was not funded") - spend({recipient = state.beneficiary, - amount = Contract.balance }) + stateful function withdraw_beneficiary() = + require(state.total >= state.goal, "Project was not funded") + spend({recipient = state.beneficiary, + amount = Contract.balance }) - stateful function withdraw_contributor() = - if(state.total >= state.goal) - abort("Project was funded") - let to = Call.caller - spend({recipient = to, - amount = state.contributions[to]}) - put(state{ contributions @ c = Map.delete(to, c) }) + stateful function withdraw_contributor() = + if(state.total >= state.goal) + abort("Project was funded") + let to = Call.caller + spend({recipient = to, + amount = state.contributions[to]}) + put(state{ contributions @ c = Map.delete(to, c) }) Repositories This is a list with repositories that include smart contracts written in Sophia: @@ -496,69 +515,35 @@ - - - - - -
- + + + - - Features + + + + +Features Contracts The main unit of code in Sophia is the contract. @@ -1075,22 +1094,22 @@ and the Call namespaces in the documentatio the contract. The type of the address must be a contract type, which consists of a number of type definitions and entrypoint declarations. For instance, // A contract type -contract interface VotingType = - entrypoint vote : string => unit +contract interface VotingType = + entrypoint vote : string => unit Now given contract address of type VotingType you can call the vote entrypoint of that contract: -contract VoteTwice = - entrypoint voteTwice(v : VotingType, alt : string) = - v.vote(alt) - v.vote(alt) +contract VoteTwice = + entrypoint voteTwice(v : VotingType, alt : string) = + v.vote(alt) + v.vote(alt) Contract calls take two optional named arguments gas : int and value : int that lets you set a gas limit and provide tokens to a contract call. If omitted the defaults are no gas limit and no tokens. Suppose there is a fee for voting: - entrypoint voteTwice(v : VotingType, fee : int, alt : string) = - v.vote(value = fee, alt) - v.vote(value = fee, alt) + entrypoint voteTwice(v : VotingType, fee : int, alt : string) = + v.vote(value = fee, alt) + v.vote(value = fee, alt) Named arguments can be given in any order. Note that reentrant calls are not permitted. In other words, when calling @@ -1104,8 +1123,8 @@ fails. To recover the underlying address of a contract instance there is a field address : address. For instance, to send tokens to the voting contract (given that it is payable) without calling it you can write - entrypoint pay(v : VotingType, amount : int) = - Chain.spend(v.address, amount) + entrypoint pay(v : VotingType, amount : int) = + Chain.spend(v.address, amount) Protected contract calls If a contract call fails for any reason (for instance, the remote contract @@ -1116,14 +1135,14 @@ contract calls takes a named argument protected : bool (default option type. If the call fails the result is None, otherwise it's Some(r) where r is the return value of the call. -contract interface VotingType = - entrypoint : vote : string => unit +contract interface VotingType = + entrypoint : vote : string => unit -contract Voter = - entrypoint tryVote(v : VotingType, alt : string) = - switch(v.vote(alt, protected = true) : option(unit)) - None => "Voting failed" - Some(_) => "Voting successful" +contract Voter = + entrypoint tryVote(v : VotingType, alt : string) = + switch(v.vote(alt, protected = true) : option(unit)) + None => "Voting failed" + Some(_) => "Voting successful" Any gas that was consumed by the contract call before the failure stays consumed, which means that in order to protect against the remote contract @@ -1145,15 +1164,15 @@ arguments – please refer to their documentation for the details. While Chain.clone requires only a contract interface and a living instance of a given contract on the chain, Chain.create needs a full definition of a to-create contract defined by the standard contract syntax, for example -contract IntHolder = - type state = int - entrypoint init(x) = x - entrypoint get() = state +contract IntHolder = + type state = int + entrypoint init(x) = x + entrypoint get() = state -main contract IntHolderFactory = - stateful entrypoint new(x : int) : IntHolder = - let ih = Chain.create(x) : IntHolder - ih +main contract IntHolderFactory = + stateful entrypoint new(x : int) : IntHolder = + let ih = Chain.create(x) : IntHolder + ih In case of a presence of child contracts (IntHolder in this case), the main contract must be pointed out with the main keyword as shown in the example. @@ -1229,21 +1248,21 @@ contract interface X : Z = A type is said to be on a "covariant" position when it describes output or a result of some computation. Analogously, position is "contravariant" when it is an input, or a parameter. Intuitively, when a part of the type is produced by values of it, it is covariant. When it is consumed, it is contravariant. When a type appears to be simultaneously input and output, it is described as invariant. If a type is neither of those (that is, it's unused) it's bivariant. Furthermore, whenever a complex type appears on a contravariant position, all its covariant components become contravariant and vice versa. Variance influences how subtyping is applied. Types on covariant positions are subtyped normally, while contravariant the opposite way. Invariant types have to be exactly the same in order for subtyping to work. Bivariant types are always compatible. A good example of where it matters can be pictured by subtyping of function types. Let us assume there is a contract interface Animal and two contracts that implement it: Dog and Cat. -contract interface Animal = - entrypoint age : () => int +contract interface Animal = + entrypoint age : () => int -contract Dog : Animal = +contract Dog : Animal = entrypoint age() = // ... - entrypoint woof() = "woof" + entrypoint woof() = "woof" -contract Cat : Animal = +contract Cat : Animal = entrypoint age() = // ... - entrypoint meow() = "meow" + entrypoint meow() = "meow" The assumption of this exercise is that cats do not bark (because Cat does not define the woof entrypoint). If subtyping rules were applied naively, that is if we let Dog => Dog be a subtype of Animal => Animal, the following code would break: -let f : (Dog) => string = d => d.woof() -let g : (Animal) => string = f -let c : Cat = Chain.create() +let f : (Dog) => string = d => d.woof() +let g : (Animal) => string = f +let c : Cat = Chain.create() g(c) // Cat barking! That is because arguments of functions are contravariant, as opposed to return the type which is covariant. Because of that, the assignment of f to g is invalid - while Dog is a subtype of Animal, Dog => string is not a subtype of Animal => string. However, Animal => string is a subtype of Dog => string. More than that, (Dog => Animal) => Dog is a subtype of (Animal => Dog) => Animal. @@ -1331,8 +1350,8 @@ provides special syntax for map/record updates. Top-level functions and entrypoints must be annotated with the stateful keyword to be allowed to affect the state of the running contract. For instance, - stateful entrypoint set_state(s : state) = - put(s) + stateful entrypoint set_state(s : state) = + put(s) Without the stateful annotation the compiler does not allow the call to put. A stateful annotation is required to @@ -1364,8 +1383,8 @@ For instance, a contract (either a Chain.spend or a normal spend transaction) will fail. If a contract shall be able to receive funds in this way it has to be declared payable: // A payable contract -payable contract ExampleContract = - stateful entrypoint do_stuff() = ... +payable contract ExampleContract = + stateful entrypoint do_stuff() = ... If in doubt, it is possible to check if an address is payable using Address.is_payable(addr). @@ -1374,11 +1393,11 @@ contract shall be able to receive funds in this way it has to be declared (either a Remote call or a contract call transaction) that has a non-zero value will fail. Contract entrypoints that should be called with a non-zero value should be declared payable. -payable stateful entrypoint buy(to : address) = - if(Call.value > 42) - transfer_item(to) - else - abort("Value too low") +payable stateful entrypoint buy(to : address) = + if(Call.value > 42) + transfer_item(to) + else + abort("Value too low") Namespaces Code can be split into libraries using the namespace construct. Namespaces @@ -1386,13 +1405,13 @@ can appear at the top-level and can contain type and function definitions, but not entrypoints. Outside the namespace you can refer to the (non-private) names by qualifying them with the namespace (Namespace.name). For example, -namespace Library = - type number = int - function inc(x : number) : number = x + 1 +namespace Library = + type number = int + function inc(x : number) : number = x + 1 -contract MyContract = - entrypoint plus2(x) : Library.number = - Library.inc(Library.inc(x)) +contract MyContract = + entrypoint plus2(x) : Library.number = + Library.inc(Library.inc(x)) Functions in namespaces have access to the same environment (including the Chain, Call, and Contract, builtin namespaces) as function in a contract, @@ -1452,13 +1471,13 @@ contract level, namespace level, or in the function level. statement. These must appear at the top-level (outside the main contract). The included file can contain one or more namespaces and abstract contracts. For example, if the file library.aes contains -namespace Library = - function inc(x) = x + 1 +namespace Library = + function inc(x) = x + 1 you can use it from another file using an include: -include "library.aes" -contract MyContract = - entrypoint plus2(x) = Library.inc(Library.inc(x)) +include "library.aes" +contract MyContract = + entrypoint plus2(x) = Library.inc(Library.inc(x)) This behaves as if the contents of library.aes was textually inserted into the file, except that error messages will refer to the original source @@ -1471,13 +1490,13 @@ namespaces like Chain, Contract, Map are included by default and are supported internally by the compiler. Others like List, Frac, Option need to be manually included using the include directive. For example -include "List.aes" -include "Pair.aes" --- Map is already there! +include "List.aes" +include "Pair.aes" +-- Map is already there! -namespace C = - entrypoint keys(m : map('a, 'b)) : list('a) = - List.map(Pair.fst, (Map.to_list(m))) +namespace C = + entrypoint keys(m : map('a, 'b)) : list('a) = + List.map(Pair.fst, (Map.to_list(m))) Types Sophia has the following types: @@ -1707,8 +1726,8 @@ corresponding integer, so setting very high bits can be expensive). Type aliases Type aliases can be introduced with the type keyword and can be parameterized. For instance -type number = int -type string_map('a) = map(string, 'a) +type number = int +type string_map('a) = map(string, 'a) A type alias and its definition can be used interchangeably. Sophia does not support higher-kinded types, meaning that following type alias is invalid: type wrap('f, 'a) = 'f('a) @@ -1716,47 +1735,47 @@ higher-kinded types, meaning that following type alias is invalid: type wr Sophia supports algebraic data types (variant types) and pattern matching. Data types are declared by giving a list of constructors with their respective arguments. For instance, -datatype one_or_both('a, 'b) = Left('a) | Right('b) | Both('a, 'b) +datatype one_or_both('a, 'b) = Left('a) | Right('b) | Both('a, 'b) Elements of data types can be pattern matched against, using the switch construct: -function get_left(x : one_or_both('a, 'b)) : option('a) = - switch(x) - Left(x) => Some(x) - Right(_) => None - Both(x, _) => Some(x) +function get_left(x : one_or_both('a, 'b)) : option('a) = + switch(x) + Left(x) => Some(x) + Right(_) => None + Both(x, _) => Some(x) or directly in the left-hand side: -function - get_left : one_or_both('a, 'b) => option('a) - get_left(Left(x)) = Some(x) - get_left(Right(_)) = None - get_left(Both(x, _)) = Some(x) +function + get_left : one_or_both('a, 'b) => option('a) + get_left(Left(x)) = Some(x) + get_left(Right(_)) = None + get_left(Both(x, _)) = Some(x) NOTE: Data types cannot currently be recursive. Sophia also supports the assignment of patterns to variables: -function f(x) = switch(x) +function f(x) = switch(x) h1::(t = h2::_) => (h1 + h2)::t // same as `h1::h2::k => (h1 + h2)::h2::k` - _ => x + _ => x -function g(p : int * option(int)) : int = +function g(p : int * option(int)) : int = let (a, (o = Some(b))) = p // o is equal to Pair.snd(p) - b + b Guards are boolean expressions that can be used on patterns in both switch statements and functions definitions. If a guard expression evaluates to true, then the corresponding body will be used. Otherwise, the next pattern will be checked: -function get_left_if_positive(x : one_or_both(int, 'b)) : option(int) = - switch(x) - Left(x) | x > 0 => Some(x) - Both(x, _) | x > 0 => Some(x) - _ => None +function get_left_if_positive(x : one_or_both(int, 'b)) : option(int) = + switch(x) + Left(x) | x > 0 => Some(x) + Both(x, _) | x > 0 => Some(x) + _ => None -function - get_left_if_positive : one_or_both(int, 'b) => option(int) - get_left_if_positive(Left(x)) | x > 0 = Some(x) - get_left_if_positive(Both(x, _)) | x > 0 = Some(x) - get_left_if_positive(_) = None +function + get_left_if_positive : one_or_both(int, 'b) => option(int) + get_left_if_positive(Left(x)) | x > 0 = Some(x) + get_left_if_positive(Both(x, _)) | x > 0 = Some(x) + get_left_if_positive(_) = None Guards cannot be stateful even when used inside a stateful function. Lists @@ -1765,9 +1784,9 @@ linked list. A list is constructed with the syntax [1, 2, 3]. The elements of a list can be any of datatype but they must have the same type. The type of lists with elements of type 'e is written list('e). For example we can have the following lists: -[1, 33, 2, 666] : list(int) -[(1, "aaa"), (10, "jjj"), (666, "the beast")] : list(int * string) -[{[1] = "aaa", [10] = "jjj"}, {[5] = "eee", [666] = "the beast"}] : list(map(int, string)) +[1, 33, 2, 666] : list(int) +[(1, "aaa"), (10, "jjj"), (666, "the beast")] : list(int * string) +[{[1] = "aaa", [10] = "jjj"}, {[5] = "eee", [666] = "the beast"}] : list(map(int, string)) New elements can be prepended to the front of a list with the :: operator. So 42 :: [1, 2, 3] returns the list [42, 1, 2, 3]. The @@ -1776,20 +1795,20 @@ and returns the resulting list. So concatenating two lists [1, 22, 33] ++ [10, 18, 55] returns the list [1, 22, 33, 10, 18, 55]. Sophia supports list comprehensions known from languages like Python, Haskell or Erlang. Example syntax: -[x + y | x <- [1,2,3,4,5], let k = x*x, if (k > 5), y <- [k, k+1, k+2]] +[x + y | x <- [1,2,3,4,5], let k = x*x, if (k > 5), y <- [k, k+1, k+2]] // yields [12,13,14,20,21,22,30,31,32] Lists can be constructed using the range syntax using special .. operator: -[1..4] == [1,2,3,4] +[1..4] == [1,2,3,4] The ranges are always ascending and have step equal to 1. Please refer to the standard library for the predefined functionalities. Maps and records A Sophia record type is given by a fixed set of fields with associated, possibly different, types. For instance - record account = { name : string, - balance : int, - history : list(transaction) } + record account = { name : string, + balance : int, + history : list(transaction) } Maps, on the other hand, can contain an arbitrary number of key-value bindings, but of a fixed type. The type of maps with keys of type 'k and values of type @@ -1799,18 +1818,18 @@ contain a map or a function type. Constructing maps and records A value of record type is constructed by giving a value for each of the fields. For the example above, - function new_account(name) = - {name = name, balance = 0, history = []} + function new_account(name) = + {name = name, balance = 0, history = []} Maps are constructed similarly, with keys enclosed in square brackets - function example_map() : map(string, int) = - {["key1"] = 1, ["key2"] = 2} + function example_map() : map(string, int) = + {["key1"] = 1, ["key2"] = 2} The empty map is written {}. Accessing values Record fields access is written r.f and map lookup m[k]. For instance, - function get_balance(a : address, accounts : map(address, account)) = - accounts[a].balance + function get_balance(a : address, accounts : map(address, account)) = + accounts[a].balance Looking up a non-existing key in a map results in contract execution failing. A default value to return for non-existing keys can be provided using the syntax @@ -1829,13 +1848,13 @@ in the map or execution fails, but a default value can be provided: m{ [k = default] @ x = v }. In this case x is bound to default if k is not in the map. Updates can be nested: -function clear_history(a : address, accounts : map(address, account)) : map(address, account) = - accounts{ [a].history = [] } +function clear_history(a : address, accounts : map(address, account)) : map(address, account) = + accounts{ [a].history = [] } This is equivalent to accounts{ [a] @ acc = acc{ history = [] } } and thus requires a to be present in the accounts map. To have clear_history create an account if a is not in the map you can write (given a function empty_account): - accounts{ [a = empty_account()].history = [] } + accounts{ [a = empty_account()].history = [] } Map implementation Internally in the VM maps are implemented as hash maps and support fast lookup @@ -1875,53 +1894,53 @@ through the Oracle interface. For a functionality documentation refer to the standard library. Example Example for an oracle answering questions of type string with answers of type int: -contract Oracles = +contract Oracles = - stateful entrypoint registerOracle(acct : address, + stateful entrypoint registerOracle(acct : address, sign : signature, // Signed network id + oracle address + contract address - qfee : int, - ttl : Chain.ttl) : oracle(string, int) = - Oracle.register(acct, signature = sign, qfee, ttl) + qfee : int, + ttl : Chain.ttl) : oracle(string, int) = + Oracle.register(acct, signature = sign, qfee, ttl) - entrypoint queryFee(o : oracle(string, int)) : int = - Oracle.query_fee(o) + entrypoint queryFee(o : oracle(string, int)) : int = + Oracle.query_fee(o) - payable stateful entrypoint createQuery(o : oracle_query(string, int), - q : string, - qfee : int, - qttl : Chain.ttl, - rttl : int) : oracle_query(string, int) = - require(qfee =< Call.value, "insufficient value for qfee") - Oracle.query(o, q, qfee, qttl, RelativeTTL(rttl)) + payable stateful entrypoint createQuery(o : oracle_query(string, int), + q : string, + qfee : int, + qttl : Chain.ttl, + rttl : int) : oracle_query(string, int) = + require(qfee =< Call.value, "insufficient value for qfee") + Oracle.query(o, q, qfee, qttl, RelativeTTL(rttl)) - stateful entrypoint extendOracle(o : oracle(string, int), - ttl : Chain.ttl) : unit = - Oracle.extend(o, ttl) + stateful entrypoint extendOracle(o : oracle(string, int), + ttl : Chain.ttl) : unit = + Oracle.extend(o, ttl) - stateful entrypoint signExtendOracle(o : oracle(string, int), + stateful entrypoint signExtendOracle(o : oracle(string, int), sign : signature, // Signed network id + oracle address + contract address - ttl : Chain.ttl) : unit = - Oracle.extend(o, signature = sign, ttl) + ttl : Chain.ttl) : unit = + Oracle.extend(o, signature = sign, ttl) - stateful entrypoint respond(o : oracle(string, int), - q : oracle_query(string, int), + stateful entrypoint respond(o : oracle(string, int), + q : oracle_query(string, int), sign : signature, // Signed network id + oracle query id + contract address - r : int) = - Oracle.respond(o, q, signature = sign, r) + r : int) = + Oracle.respond(o, q, signature = sign, r) - entrypoint getQuestion(o : oracle(string, int), - q : oracle_query(string, int)) : string = - Oracle.get_question(o, q) + entrypoint getQuestion(o : oracle(string, int), + q : oracle_query(string, int)) : string = + Oracle.get_question(o, q) - entrypoint hasAnswer(o : oracle(string, int), - q : oracle_query(string, int)) = - switch(Oracle.get_answer(o, q)) - None => false - Some(_) => true + entrypoint hasAnswer(o : oracle(string, int), + q : oracle_query(string, int)) = + switch(Oracle.get_answer(o, q)) + None => false + Some(_) => true - entrypoint getAnswer(o : oracle(string, int), - q : oracle_query(string, int)) : option(int) = - Oracle.get_answer(o, q) + entrypoint getAnswer(o : oracle(string, int), + q : oracle_query(string, int)) : option(int) = + Oracle.get_answer(o, q) Sanity checks When an Oracle literal is passed to a contract, no deep checks are performed. @@ -1938,29 +1957,29 @@ an account with address addr. In order to allow a contract ct signature sig of addr | name.hash | ct.address. Armed with this information we can for example write a function that extends the name if it expires within 1000 blocks: - stateful entrypoint extend_if_necessary(addr : address, name : string, sig : signature) = - switch(AENS.lookup(name)) - None => () - Some(AENS.Name(_, FixedTTL(expiry), _)) => - if(Chain.block_height + 1000 > expiry) - AENS.update(addr, name, Some(RelativeTTL(50000)), None, None, signature = sig) + stateful entrypoint extend_if_necessary(addr : address, name : string, sig : signature) = + switch(AENS.lookup(name)) + None => () + Some(AENS.Name(_, FixedTTL(expiry), _)) => + if(Chain.block_height + 1000 > expiry) + AENS.update(addr, name, Some(RelativeTTL(50000)), None, None, signature = sig) And we can write functions that adds and removes keys from the pointers of the name: - stateful entrypoint add_key(addr : address, name : string, key : string, - pt : AENS.pointee, sig : signature) = - switch(AENS.lookup(name)) - None => () - Some(AENS.Name(_, _, ptrs)) => - AENS.update(addr, name, None, None, Some(ptrs{[key] = pt}), signature = sig) + stateful entrypoint add_key(addr : address, name : string, key : string, + pt : AENS.pointee, sig : signature) = + switch(AENS.lookup(name)) + None => () + Some(AENS.Name(_, _, ptrs)) => + AENS.update(addr, name, None, None, Some(ptrs{[key] = pt}), signature = sig) - stateful entrypoint delete_key(addr : address, name : string, - key : string, sig : signature) = - switch(AENS.lookup(name)) - None => () - Some(AENS.Name(_, _, ptrs)) => - let ptrs = Map.delete(key, ptrs) - AENS.update(addr, name, None, None, Some(ptrs), signature = sig) + stateful entrypoint delete_key(addr : address, name : string, + key : string, sig : signature) = + switch(AENS.lookup(name)) + None => () + Some(AENS.Name(_, _, ptrs)) => + let ptrs = Map.delete(key, ptrs) + AENS.update(addr, name, None, None, Some(ptrs), signature = sig) Note: From the Iris hardfork more strict rules apply for AENS pointers, when a Sophia contract lookup or update (bad) legacy pointers, the bad keys are @@ -1972,11 +1991,11 @@ Solidity. Events are further discussed in the protocol. To use events a contract must declare a datatype event, and events are then logged using the Chain.event function: - datatype event - = Event1(int, int, string) - | Event2(string, address) + datatype event + = Event1(int, int, string) + | Event2(string, address) - Chain.event(e : event) : unit + Chain.event(e : event) : unit The event can have 0-3 indexed fields, and an optional payload field. A field is indexed if it fits in a 32-byte word, i.e. @@ -1993,18 +2012,18 @@ The fields can appear in any order. NOTE: Indexing is not part of the core æternity node. Events are emitted by using the Chain.event function. The following function will emit one Event of each kind in the example. - entrypoint emit_events() : () = - Chain.event(Event1(42, 34, "foo")) - Chain.event(Event2("This is not indexed", Contract.address)) + entrypoint emit_events() : () = + Chain.event(Event1(42, 34, "foo")) + Chain.event(Event2("This is not indexed", Contract.address)) Argument order It is only possible to have one (1) string parameter in the event, but it can be placed in any position (and its value will end up in the data field), i.e. -AnotherEvent(string, indexed address) +AnotherEvent(string, indexed address) -... +... -Chain.event(AnotherEvent("This is not indexed", Contract.address)) +Chain.event(AnotherEvent("This is not indexed", Contract.address)) would yield exactly the same result in the example above! Compiler pragmas @@ -2012,8 +2031,8 @@ would yield exactly the same result in the example above! Sophia compiler, you can give one or more @compiler pragmas at the top-level (typically at the beginning) of a file. For instance, to enforce that a contract is compiled with version 4.3 of the compiler you write -@compiler >= 4.3 -@compiler < 4.4 +@compiler >= 4.3 +@compiler < 4.4 Valid operators in compiler pragmas are <, =<, ==, >=, and >. Version numbers are given as a sequence of non-negative integers separated by dots. @@ -2021,18 +2040,18 @@ Trailing zeros are ignored, so 4.0.0 == 4. If a constraint is viola error is reported and compilation fails. Exceptions Contracts can fail with an (uncatchable) exception using the built-in function -abort(reason : string) : 'a +abort(reason : string) : 'a Calling abort causes the top-level call transaction to return an error result containing the reason string. Only the gas used up to and including the abort call is charged. This is different from termination due to a crash which consumes all available gas. For convenience the following function is also built-in: -function require(b : bool, err : string) = - if(!b) abort(err) +function require(b : bool, err : string) = + if(!b) abort(err) Aside from that, there is an almost equivalent function exit -exit(reason : string) : 'a +exit(reason : string) : 'a Just like abort, it breaks the execution with the given reason. The difference however is in the gas consumption — while abort returns unused gas, a call to @@ -2043,69 +2062,35 @@ optional delegation signature. This is typically used when a user/accounts would like to allow a contract to act on it's behalf. The exact data to be signed varies for the different operations, but in all cases you should prepend the signature data with the network_id (ae_mainnet for the æternity mainnet, etc.). - - - - - - - + + + + + + + + + + - - + + + + + + + @@ -81,11 +104,11 @@ - + - + @@ -107,20 +130,18 @@ - - + - - + @@ -129,26 +150,25 @@ - + - - + - - + + - - + + - - + + @@ -161,7 +181,7 @@ Initializing search - + @@ -170,11 +190,10 @@ - - + - + GitHub @@ -209,18 +228,17 @@ - + æternity Sophia Language - - + - + GitHub @@ -286,7 +304,7 @@ - + @@ -303,7 +321,6 @@ - @@ -438,7 +455,7 @@ - BLS1295381 + BLS12_381 @@ -555,7 +572,6 @@ - @@ -690,7 +706,7 @@ - BLS1295381 + BLS12_381 @@ -764,12 +780,15 @@ - - - + + + - - GitHub @@ -209,18 +228,17 @@ - + æternity Sophia Language - - + - + GitHub @@ -256,7 +274,7 @@ - + @@ -273,7 +291,6 @@ - @@ -458,7 +475,6 @@ - @@ -570,12 +586,15 @@ - - - + + + - - Syntax + + + + +Syntax Lexical syntax Comments Single line comments start with // and block comments are enclosed in /* @@ -662,11 +681,11 @@ indented more than the currently enclosing layout block. Blocks with a single element can be written on the same line as the previous token. Each element of the block must share the same indentation and no part of an element may be indented less than the indentation of the block. For instance -contract Layout = +contract Layout = function foo() = 0 // no layout function bar() = // layout block starts on next line let x = foo() // indented more than 2 spaces - x + x + 1 // the '+' is indented more than the 'x' Notation @@ -687,107 +706,107 @@ element may be indented less than the indentation of the block. For instance Declarations A Sophia file consists of a sequence of declarations in a layout block. -File ::= Block(TopDecl) +File ::= Block(TopDecl) -TopDecl ::= ['payable'] ['main'] 'contract' Con [Implement] '=' Block(Decl) - | 'contract' 'interface' Con [Implement] '=' Block(Decl) - | 'namespace' Con '=' Block(Decl) - | '@compiler' PragmaOp Version - | 'include' String - | Using +TopDecl ::= ['payable'] ['main'] 'contract' Con [Implement] '=' Block(Decl) + | 'contract' 'interface' Con [Implement] '=' Block(Decl) + | 'namespace' Con '=' Block(Decl) + | '@compiler' PragmaOp Version + | 'include' String + | Using -Implement ::= ':' Sep1(Con, ',') +Implement ::= ':' Sep1(Con, ',') -Decl ::= 'type' Id ['(' TVar* ')'] '=' TypeAlias - | 'record' Id ['(' TVar* ')'] '=' RecordType - | 'datatype' Id ['(' TVar* ')'] '=' DataType - | (EModifier* 'entrypoint' | FModifier* 'function') Block(FunDecl) - | Using +Decl ::= 'type' Id ['(' TVar* ')'] '=' TypeAlias + | 'record' Id ['(' TVar* ')'] '=' RecordType + | 'datatype' Id ['(' TVar* ')'] '=' DataType + | (EModifier* 'entrypoint' | FModifier* 'function') Block(FunDecl) + | Using FunDecl ::= Id ':' Type // Type signature | Id Args [':' Type] '=' Block(Stmt) // Definition | Id Args [':' Type] Block(GuardedDef) // Guarded definitions -GuardedDef ::= '|' Sep1(Expr, ',') '=' Block(Stmt) +GuardedDef ::= '|' Sep1(Expr, ',') '=' Block(Stmt) -Using ::= 'using' Con ['as' Con] [UsingParts] -UsingParts ::= 'for' '[' Sep1(Id, ',') ']' - | 'hiding' '[' Sep1(Id, ',') ']' +Using ::= 'using' Con ['as' Con] [UsingParts] +UsingParts ::= 'for' '[' Sep1(Id, ',') ']' + | 'hiding' '[' Sep1(Id, ',') ']' -PragmaOp ::= '<' | '=<' | '==' | '>=' | '>' -Version ::= Sep1(Int, '.') +PragmaOp ::= '<' | '=<' | '==' | '>=' | '>' +Version ::= Sep1(Int, '.') -EModifier ::= 'payable' | 'stateful' -FModifier ::= 'stateful' | 'private' +EModifier ::= 'payable' | 'stateful' +FModifier ::= 'stateful' | 'private' -Args ::= '(' Sep(Pattern, ',') ')' +Args ::= '(' Sep(Pattern, ',') ')' Contract declarations must appear at the top-level. For example, -contract Test = - type t = int - entrypoint add (x : t, y : t) = x + y +contract Test = + type t = int + entrypoint add (x : t, y : t) = x + y There are three forms of type declarations: type aliases (declared with the type keyword), record type definitions (record) and data type definitions (datatype): -TypeAlias ::= Type -RecordType ::= '{' Sep(FieldType, ',') '}' -DataType ::= Sep1(ConDecl, '|') +TypeAlias ::= Type +RecordType ::= '{' Sep(FieldType, ',') '}' +DataType ::= Sep1(ConDecl, '|') -FieldType ::= Id ':' Type -ConDecl ::= Con ['(' Sep1(Type, ',') ')'] +FieldType ::= Id ':' Type +ConDecl ::= Con ['(' Sep1(Type, ',') ')'] For example, -record point('a) = {x : 'a, y : 'a} -datatype shape('a) = Circle(point('a), 'a) | Rect(point('a), point('a)) -type int_shape = shape(int) +record point('a) = {x : 'a, y : 'a} +datatype shape('a) = Circle(point('a), 'a) | Rect(point('a), point('a)) +type int_shape = shape(int) Types Type ::= Domain '=>' Type // Function type | Type '(' Sep(Type, ',') ')' // Type application | '(' Type ')' // Parens | 'unit' | Sep(Type, '*') // Tuples - | Id | QId | TVar + | Id | QId | TVar Domain ::= Type // Single argument | '(' Sep(Type, ',') ')' // Multiple arguments The function type arrow associates to the right. Example, -'a => list('a) => (int * list('a)) +'a => list('a) => (int * list('a)) Statements Function bodies are blocks of statements, where a statement is one of the following -Stmt ::= 'switch' '(' Expr ')' Block(Case) - | 'if' '(' Expr ')' Block(Stmt) - | 'elif' '(' Expr ')' Block(Stmt) - | 'else' Block(Stmt) - | 'let' LetDef - | Using - | Expr +Stmt ::= 'switch' '(' Expr ')' Block(Case) + | 'if' '(' Expr ')' Block(Stmt) + | 'elif' '(' Expr ')' Block(Stmt) + | 'else' Block(Stmt) + | 'let' LetDef + | Using + | Expr LetDef ::= Id Args [':' Type] '=' Block(Stmt) // Function definition | Pattern '=' Block(Stmt) // Value definition -Case ::= Pattern '=>' Block(Stmt) - | Pattern Block(GuardedCase) +Case ::= Pattern '=>' Block(Stmt) + | Pattern Block(GuardedCase) -GuardedCase ::= '|' Sep1(Expr, ',') '=>' Block(Stmt) +GuardedCase ::= '|' Sep1(Expr, ',') '=>' Block(Stmt) -Pattern ::= Expr +Pattern ::= Expr if statements can be followed by zero or more elif statements and an optional final else statement. For example, -let x : int = 4 -switch(f(x)) - None => 0 - Some(y) => - if(y > 10) - "too big" - elif(y < 3) - "too small" - else - "just right" +let x : int = 4 +switch(f(x)) + None => 0 + Some(y) => + if(y > 10) + "too big" + elif(y < 3) + "too small" + else + "just right" Expressions Expr ::= '(' LamArgs ')' '=>' Block(Stmt) // Anonymous function (x) => x + 1 @@ -801,7 +820,7 @@ element may be indented less than the indentation of the block. For instance | Expr '[' Expr ']' // Map lookup map[key] | Expr '{' Sep(FieldUpdate, ',') '}' // Record or map update r{ fld[key].x = y } | '[' Sep(Expr, ',') ']' // List [1, 2, 3] - | '[' Expr '|' Sep(Generator, ',') ']' + | '[' Expr '|' Sep(Generator, ',') ']' // List comprehension [k | x <- [1], if (f(x)), let k = x+1] | '[' Expr '..' Expr ']' // List range [1..n] | '{' Sep(FieldUpdate, ',') '}' // Record or map value {x = 0, y = 1}, {[key] = val} @@ -817,19 +836,19 @@ element may be indented less than the indentation of the block. For instance | 'if' '(' Expr ')' // Guard | LetDef // Definition -LamArgs ::= '(' Sep(LamArg, ',') ')' -LamArg ::= Id [':' Type] +LamArgs ::= '(' Sep(LamArg, ',') ')' +LamArg ::= Id [':' Type] -FieldUpdate ::= Path '=' Expr +FieldUpdate ::= Path '=' Expr Path ::= Id // Record field | '[' Expr ']' // Map key | Path '.' Id // Nested record field | Path '[' Expr ']' // Nested map key -BinOp ::= '||' | '&&' | '<' | '>' | '=<' | '>=' | '==' | '!=' - | '::' | '++' | '+' | '-' | '*' | '/' | 'mod' | '^' - | '|>' -UnOp ::= '-' | '!' +BinOp ::= '||' | '&&' | '<' | '>' | '=<' | '>=' | '==' | '!=' + | '::' | '++' | '+' | '-' | '*' | '/' | 'mod' | '^' + | '|>' +UnOp ::= '-' | '!' Operators types @@ -914,69 +933,35 @@ element may be indented less than the indentation of the block. For instance - - - - - - - + + + + + + + + + + - -
- - Features + + + + +Features Contracts The main unit of code in Sophia is the contract. @@ -1075,22 +1094,22 @@ and the Call namespaces in the documentatio the contract. The type of the address must be a contract type, which consists of a number of type definitions and entrypoint declarations. For instance, // A contract type -contract interface VotingType = - entrypoint vote : string => unit +contract interface VotingType = + entrypoint vote : string => unit Now given contract address of type VotingType you can call the vote entrypoint of that contract: -contract VoteTwice = - entrypoint voteTwice(v : VotingType, alt : string) = - v.vote(alt) - v.vote(alt) +contract VoteTwice = + entrypoint voteTwice(v : VotingType, alt : string) = + v.vote(alt) + v.vote(alt) Contract calls take two optional named arguments gas : int and value : int that lets you set a gas limit and provide tokens to a contract call. If omitted the defaults are no gas limit and no tokens. Suppose there is a fee for voting: - entrypoint voteTwice(v : VotingType, fee : int, alt : string) = - v.vote(value = fee, alt) - v.vote(value = fee, alt) + entrypoint voteTwice(v : VotingType, fee : int, alt : string) = + v.vote(value = fee, alt) + v.vote(value = fee, alt) Named arguments can be given in any order. Note that reentrant calls are not permitted. In other words, when calling @@ -1104,8 +1123,8 @@ fails. To recover the underlying address of a contract instance there is a field address : address. For instance, to send tokens to the voting contract (given that it is payable) without calling it you can write - entrypoint pay(v : VotingType, amount : int) = - Chain.spend(v.address, amount) + entrypoint pay(v : VotingType, amount : int) = + Chain.spend(v.address, amount) Protected contract calls If a contract call fails for any reason (for instance, the remote contract @@ -1116,14 +1135,14 @@ contract calls takes a named argument protected : bool (default option type. If the call fails the result is None, otherwise it's Some(r) where r is the return value of the call. -contract interface VotingType = - entrypoint : vote : string => unit +contract interface VotingType = + entrypoint : vote : string => unit -contract Voter = - entrypoint tryVote(v : VotingType, alt : string) = - switch(v.vote(alt, protected = true) : option(unit)) - None => "Voting failed" - Some(_) => "Voting successful" +contract Voter = + entrypoint tryVote(v : VotingType, alt : string) = + switch(v.vote(alt, protected = true) : option(unit)) + None => "Voting failed" + Some(_) => "Voting successful" Any gas that was consumed by the contract call before the failure stays consumed, which means that in order to protect against the remote contract @@ -1145,15 +1164,15 @@ arguments – please refer to their documentation for the details. While Chain.clone requires only a contract interface and a living instance of a given contract on the chain, Chain.create needs a full definition of a to-create contract defined by the standard contract syntax, for example -contract IntHolder = - type state = int - entrypoint init(x) = x - entrypoint get() = state +contract IntHolder = + type state = int + entrypoint init(x) = x + entrypoint get() = state -main contract IntHolderFactory = - stateful entrypoint new(x : int) : IntHolder = - let ih = Chain.create(x) : IntHolder - ih +main contract IntHolderFactory = + stateful entrypoint new(x : int) : IntHolder = + let ih = Chain.create(x) : IntHolder + ih In case of a presence of child contracts (IntHolder in this case), the main contract must be pointed out with the main keyword as shown in the example. @@ -1229,21 +1248,21 @@ contract interface X : Z = A type is said to be on a "covariant" position when it describes output or a result of some computation. Analogously, position is "contravariant" when it is an input, or a parameter. Intuitively, when a part of the type is produced by values of it, it is covariant. When it is consumed, it is contravariant. When a type appears to be simultaneously input and output, it is described as invariant. If a type is neither of those (that is, it's unused) it's bivariant. Furthermore, whenever a complex type appears on a contravariant position, all its covariant components become contravariant and vice versa. Variance influences how subtyping is applied. Types on covariant positions are subtyped normally, while contravariant the opposite way. Invariant types have to be exactly the same in order for subtyping to work. Bivariant types are always compatible. A good example of where it matters can be pictured by subtyping of function types. Let us assume there is a contract interface Animal and two contracts that implement it: Dog and Cat. -contract interface Animal = - entrypoint age : () => int +contract interface Animal = + entrypoint age : () => int -contract Dog : Animal = +contract Dog : Animal = entrypoint age() = // ... - entrypoint woof() = "woof" + entrypoint woof() = "woof" -contract Cat : Animal = +contract Cat : Animal = entrypoint age() = // ... - entrypoint meow() = "meow" + entrypoint meow() = "meow" The assumption of this exercise is that cats do not bark (because Cat does not define the woof entrypoint). If subtyping rules were applied naively, that is if we let Dog => Dog be a subtype of Animal => Animal, the following code would break: -let f : (Dog) => string = d => d.woof() -let g : (Animal) => string = f -let c : Cat = Chain.create() +let f : (Dog) => string = d => d.woof() +let g : (Animal) => string = f +let c : Cat = Chain.create() g(c) // Cat barking! That is because arguments of functions are contravariant, as opposed to return the type which is covariant. Because of that, the assignment of f to g is invalid - while Dog is a subtype of Animal, Dog => string is not a subtype of Animal => string. However, Animal => string is a subtype of Dog => string. More than that, (Dog => Animal) => Dog is a subtype of (Animal => Dog) => Animal. @@ -1331,8 +1350,8 @@ provides special syntax for map/record updates. Top-level functions and entrypoints must be annotated with the stateful keyword to be allowed to affect the state of the running contract. For instance, - stateful entrypoint set_state(s : state) = - put(s) + stateful entrypoint set_state(s : state) = + put(s) Without the stateful annotation the compiler does not allow the call to put. A stateful annotation is required to @@ -1364,8 +1383,8 @@ For instance, a contract (either a Chain.spend or a normal spend transaction) will fail. If a contract shall be able to receive funds in this way it has to be declared payable: // A payable contract -payable contract ExampleContract = - stateful entrypoint do_stuff() = ... +payable contract ExampleContract = + stateful entrypoint do_stuff() = ... If in doubt, it is possible to check if an address is payable using Address.is_payable(addr). @@ -1374,11 +1393,11 @@ contract shall be able to receive funds in this way it has to be declared (either a Remote call or a contract call transaction) that has a non-zero value will fail. Contract entrypoints that should be called with a non-zero value should be declared payable. -payable stateful entrypoint buy(to : address) = - if(Call.value > 42) - transfer_item(to) - else - abort("Value too low") +payable stateful entrypoint buy(to : address) = + if(Call.value > 42) + transfer_item(to) + else + abort("Value too low") Namespaces Code can be split into libraries using the namespace construct. Namespaces @@ -1386,13 +1405,13 @@ can appear at the top-level and can contain type and function definitions, but not entrypoints. Outside the namespace you can refer to the (non-private) names by qualifying them with the namespace (Namespace.name). For example, -namespace Library = - type number = int - function inc(x : number) : number = x + 1 +namespace Library = + type number = int + function inc(x : number) : number = x + 1 -contract MyContract = - entrypoint plus2(x) : Library.number = - Library.inc(Library.inc(x)) +contract MyContract = + entrypoint plus2(x) : Library.number = + Library.inc(Library.inc(x)) Functions in namespaces have access to the same environment (including the Chain, Call, and Contract, builtin namespaces) as function in a contract, @@ -1452,13 +1471,13 @@ contract level, namespace level, or in the function level. statement. These must appear at the top-level (outside the main contract). The included file can contain one or more namespaces and abstract contracts. For example, if the file library.aes contains -namespace Library = - function inc(x) = x + 1 +namespace Library = + function inc(x) = x + 1 you can use it from another file using an include: -include "library.aes" -contract MyContract = - entrypoint plus2(x) = Library.inc(Library.inc(x)) +include "library.aes" +contract MyContract = + entrypoint plus2(x) = Library.inc(Library.inc(x)) This behaves as if the contents of library.aes was textually inserted into the file, except that error messages will refer to the original source @@ -1471,13 +1490,13 @@ namespaces like Chain, Contract, Map are included by default and are supported internally by the compiler. Others like List, Frac, Option need to be manually included using the include directive. For example -include "List.aes" -include "Pair.aes" --- Map is already there! +include "List.aes" +include "Pair.aes" +-- Map is already there! -namespace C = - entrypoint keys(m : map('a, 'b)) : list('a) = - List.map(Pair.fst, (Map.to_list(m))) +namespace C = + entrypoint keys(m : map('a, 'b)) : list('a) = + List.map(Pair.fst, (Map.to_list(m))) Types Sophia has the following types: @@ -1707,8 +1726,8 @@ corresponding integer, so setting very high bits can be expensive). Type aliases Type aliases can be introduced with the type keyword and can be parameterized. For instance -type number = int -type string_map('a) = map(string, 'a) +type number = int +type string_map('a) = map(string, 'a) A type alias and its definition can be used interchangeably. Sophia does not support higher-kinded types, meaning that following type alias is invalid: type wrap('f, 'a) = 'f('a) @@ -1716,47 +1735,47 @@ higher-kinded types, meaning that following type alias is invalid: type wr Sophia supports algebraic data types (variant types) and pattern matching. Data types are declared by giving a list of constructors with their respective arguments. For instance, -datatype one_or_both('a, 'b) = Left('a) | Right('b) | Both('a, 'b) +datatype one_or_both('a, 'b) = Left('a) | Right('b) | Both('a, 'b) Elements of data types can be pattern matched against, using the switch construct: -function get_left(x : one_or_both('a, 'b)) : option('a) = - switch(x) - Left(x) => Some(x) - Right(_) => None - Both(x, _) => Some(x) +function get_left(x : one_or_both('a, 'b)) : option('a) = + switch(x) + Left(x) => Some(x) + Right(_) => None + Both(x, _) => Some(x) or directly in the left-hand side: -function - get_left : one_or_both('a, 'b) => option('a) - get_left(Left(x)) = Some(x) - get_left(Right(_)) = None - get_left(Both(x, _)) = Some(x) +function + get_left : one_or_both('a, 'b) => option('a) + get_left(Left(x)) = Some(x) + get_left(Right(_)) = None + get_left(Both(x, _)) = Some(x) NOTE: Data types cannot currently be recursive. Sophia also supports the assignment of patterns to variables: -function f(x) = switch(x) +function f(x) = switch(x) h1::(t = h2::_) => (h1 + h2)::t // same as `h1::h2::k => (h1 + h2)::h2::k` - _ => x + _ => x -function g(p : int * option(int)) : int = +function g(p : int * option(int)) : int = let (a, (o = Some(b))) = p // o is equal to Pair.snd(p) - b + b Guards are boolean expressions that can be used on patterns in both switch statements and functions definitions. If a guard expression evaluates to true, then the corresponding body will be used. Otherwise, the next pattern will be checked: -function get_left_if_positive(x : one_or_both(int, 'b)) : option(int) = - switch(x) - Left(x) | x > 0 => Some(x) - Both(x, _) | x > 0 => Some(x) - _ => None +function get_left_if_positive(x : one_or_both(int, 'b)) : option(int) = + switch(x) + Left(x) | x > 0 => Some(x) + Both(x, _) | x > 0 => Some(x) + _ => None -function - get_left_if_positive : one_or_both(int, 'b) => option(int) - get_left_if_positive(Left(x)) | x > 0 = Some(x) - get_left_if_positive(Both(x, _)) | x > 0 = Some(x) - get_left_if_positive(_) = None +function + get_left_if_positive : one_or_both(int, 'b) => option(int) + get_left_if_positive(Left(x)) | x > 0 = Some(x) + get_left_if_positive(Both(x, _)) | x > 0 = Some(x) + get_left_if_positive(_) = None Guards cannot be stateful even when used inside a stateful function. Lists @@ -1765,9 +1784,9 @@ linked list. A list is constructed with the syntax [1, 2, 3]. The elements of a list can be any of datatype but they must have the same type. The type of lists with elements of type 'e is written list('e). For example we can have the following lists: -[1, 33, 2, 666] : list(int) -[(1, "aaa"), (10, "jjj"), (666, "the beast")] : list(int * string) -[{[1] = "aaa", [10] = "jjj"}, {[5] = "eee", [666] = "the beast"}] : list(map(int, string)) +[1, 33, 2, 666] : list(int) +[(1, "aaa"), (10, "jjj"), (666, "the beast")] : list(int * string) +[{[1] = "aaa", [10] = "jjj"}, {[5] = "eee", [666] = "the beast"}] : list(map(int, string)) New elements can be prepended to the front of a list with the :: operator. So 42 :: [1, 2, 3] returns the list [42, 1, 2, 3]. The @@ -1776,20 +1795,20 @@ and returns the resulting list. So concatenating two lists [1, 22, 33] ++ [10, 18, 55] returns the list [1, 22, 33, 10, 18, 55]. Sophia supports list comprehensions known from languages like Python, Haskell or Erlang. Example syntax: -[x + y | x <- [1,2,3,4,5], let k = x*x, if (k > 5), y <- [k, k+1, k+2]] +[x + y | x <- [1,2,3,4,5], let k = x*x, if (k > 5), y <- [k, k+1, k+2]] // yields [12,13,14,20,21,22,30,31,32] Lists can be constructed using the range syntax using special .. operator: -[1..4] == [1,2,3,4] +[1..4] == [1,2,3,4] The ranges are always ascending and have step equal to 1. Please refer to the standard library for the predefined functionalities. Maps and records A Sophia record type is given by a fixed set of fields with associated, possibly different, types. For instance - record account = { name : string, - balance : int, - history : list(transaction) } + record account = { name : string, + balance : int, + history : list(transaction) } Maps, on the other hand, can contain an arbitrary number of key-value bindings, but of a fixed type. The type of maps with keys of type 'k and values of type @@ -1799,18 +1818,18 @@ contain a map or a function type. Constructing maps and records A value of record type is constructed by giving a value for each of the fields. For the example above, - function new_account(name) = - {name = name, balance = 0, history = []} + function new_account(name) = + {name = name, balance = 0, history = []} Maps are constructed similarly, with keys enclosed in square brackets - function example_map() : map(string, int) = - {["key1"] = 1, ["key2"] = 2} + function example_map() : map(string, int) = + {["key1"] = 1, ["key2"] = 2} The empty map is written {}. Accessing values Record fields access is written r.f and map lookup m[k]. For instance, - function get_balance(a : address, accounts : map(address, account)) = - accounts[a].balance + function get_balance(a : address, accounts : map(address, account)) = + accounts[a].balance Looking up a non-existing key in a map results in contract execution failing. A default value to return for non-existing keys can be provided using the syntax @@ -1829,13 +1848,13 @@ in the map or execution fails, but a default value can be provided: m{ [k = default] @ x = v }. In this case x is bound to default if k is not in the map. Updates can be nested: -function clear_history(a : address, accounts : map(address, account)) : map(address, account) = - accounts{ [a].history = [] } +function clear_history(a : address, accounts : map(address, account)) : map(address, account) = + accounts{ [a].history = [] } This is equivalent to accounts{ [a] @ acc = acc{ history = [] } } and thus requires a to be present in the accounts map. To have clear_history create an account if a is not in the map you can write (given a function empty_account): - accounts{ [a = empty_account()].history = [] } + accounts{ [a = empty_account()].history = [] } Map implementation Internally in the VM maps are implemented as hash maps and support fast lookup @@ -1875,53 +1894,53 @@ through the Oracle interface. For a functionality documentation refer to the standard library. Example Example for an oracle answering questions of type string with answers of type int: -contract Oracles = +contract Oracles = - stateful entrypoint registerOracle(acct : address, + stateful entrypoint registerOracle(acct : address, sign : signature, // Signed network id + oracle address + contract address - qfee : int, - ttl : Chain.ttl) : oracle(string, int) = - Oracle.register(acct, signature = sign, qfee, ttl) + qfee : int, + ttl : Chain.ttl) : oracle(string, int) = + Oracle.register(acct, signature = sign, qfee, ttl) - entrypoint queryFee(o : oracle(string, int)) : int = - Oracle.query_fee(o) + entrypoint queryFee(o : oracle(string, int)) : int = + Oracle.query_fee(o) - payable stateful entrypoint createQuery(o : oracle_query(string, int), - q : string, - qfee : int, - qttl : Chain.ttl, - rttl : int) : oracle_query(string, int) = - require(qfee =< Call.value, "insufficient value for qfee") - Oracle.query(o, q, qfee, qttl, RelativeTTL(rttl)) + payable stateful entrypoint createQuery(o : oracle_query(string, int), + q : string, + qfee : int, + qttl : Chain.ttl, + rttl : int) : oracle_query(string, int) = + require(qfee =< Call.value, "insufficient value for qfee") + Oracle.query(o, q, qfee, qttl, RelativeTTL(rttl)) - stateful entrypoint extendOracle(o : oracle(string, int), - ttl : Chain.ttl) : unit = - Oracle.extend(o, ttl) + stateful entrypoint extendOracle(o : oracle(string, int), + ttl : Chain.ttl) : unit = + Oracle.extend(o, ttl) - stateful entrypoint signExtendOracle(o : oracle(string, int), + stateful entrypoint signExtendOracle(o : oracle(string, int), sign : signature, // Signed network id + oracle address + contract address - ttl : Chain.ttl) : unit = - Oracle.extend(o, signature = sign, ttl) + ttl : Chain.ttl) : unit = + Oracle.extend(o, signature = sign, ttl) - stateful entrypoint respond(o : oracle(string, int), - q : oracle_query(string, int), + stateful entrypoint respond(o : oracle(string, int), + q : oracle_query(string, int), sign : signature, // Signed network id + oracle query id + contract address - r : int) = - Oracle.respond(o, q, signature = sign, r) + r : int) = + Oracle.respond(o, q, signature = sign, r) - entrypoint getQuestion(o : oracle(string, int), - q : oracle_query(string, int)) : string = - Oracle.get_question(o, q) + entrypoint getQuestion(o : oracle(string, int), + q : oracle_query(string, int)) : string = + Oracle.get_question(o, q) - entrypoint hasAnswer(o : oracle(string, int), - q : oracle_query(string, int)) = - switch(Oracle.get_answer(o, q)) - None => false - Some(_) => true + entrypoint hasAnswer(o : oracle(string, int), + q : oracle_query(string, int)) = + switch(Oracle.get_answer(o, q)) + None => false + Some(_) => true - entrypoint getAnswer(o : oracle(string, int), - q : oracle_query(string, int)) : option(int) = - Oracle.get_answer(o, q) + entrypoint getAnswer(o : oracle(string, int), + q : oracle_query(string, int)) : option(int) = + Oracle.get_answer(o, q) Sanity checks When an Oracle literal is passed to a contract, no deep checks are performed. @@ -1938,29 +1957,29 @@ an account with address addr. In order to allow a contract ct signature sig of addr | name.hash | ct.address. Armed with this information we can for example write a function that extends the name if it expires within 1000 blocks: - stateful entrypoint extend_if_necessary(addr : address, name : string, sig : signature) = - switch(AENS.lookup(name)) - None => () - Some(AENS.Name(_, FixedTTL(expiry), _)) => - if(Chain.block_height + 1000 > expiry) - AENS.update(addr, name, Some(RelativeTTL(50000)), None, None, signature = sig) + stateful entrypoint extend_if_necessary(addr : address, name : string, sig : signature) = + switch(AENS.lookup(name)) + None => () + Some(AENS.Name(_, FixedTTL(expiry), _)) => + if(Chain.block_height + 1000 > expiry) + AENS.update(addr, name, Some(RelativeTTL(50000)), None, None, signature = sig) And we can write functions that adds and removes keys from the pointers of the name: - stateful entrypoint add_key(addr : address, name : string, key : string, - pt : AENS.pointee, sig : signature) = - switch(AENS.lookup(name)) - None => () - Some(AENS.Name(_, _, ptrs)) => - AENS.update(addr, name, None, None, Some(ptrs{[key] = pt}), signature = sig) + stateful entrypoint add_key(addr : address, name : string, key : string, + pt : AENS.pointee, sig : signature) = + switch(AENS.lookup(name)) + None => () + Some(AENS.Name(_, _, ptrs)) => + AENS.update(addr, name, None, None, Some(ptrs{[key] = pt}), signature = sig) - stateful entrypoint delete_key(addr : address, name : string, - key : string, sig : signature) = - switch(AENS.lookup(name)) - None => () - Some(AENS.Name(_, _, ptrs)) => - let ptrs = Map.delete(key, ptrs) - AENS.update(addr, name, None, None, Some(ptrs), signature = sig) + stateful entrypoint delete_key(addr : address, name : string, + key : string, sig : signature) = + switch(AENS.lookup(name)) + None => () + Some(AENS.Name(_, _, ptrs)) => + let ptrs = Map.delete(key, ptrs) + AENS.update(addr, name, None, None, Some(ptrs), signature = sig) Note: From the Iris hardfork more strict rules apply for AENS pointers, when a Sophia contract lookup or update (bad) legacy pointers, the bad keys are @@ -1972,11 +1991,11 @@ Solidity. Events are further discussed in the protocol. To use events a contract must declare a datatype event, and events are then logged using the Chain.event function: - datatype event - = Event1(int, int, string) - | Event2(string, address) + datatype event + = Event1(int, int, string) + | Event2(string, address) - Chain.event(e : event) : unit + Chain.event(e : event) : unit The event can have 0-3 indexed fields, and an optional payload field. A field is indexed if it fits in a 32-byte word, i.e. @@ -1993,18 +2012,18 @@ The fields can appear in any order. NOTE: Indexing is not part of the core æternity node. Events are emitted by using the Chain.event function. The following function will emit one Event of each kind in the example. - entrypoint emit_events() : () = - Chain.event(Event1(42, 34, "foo")) - Chain.event(Event2("This is not indexed", Contract.address)) + entrypoint emit_events() : () = + Chain.event(Event1(42, 34, "foo")) + Chain.event(Event2("This is not indexed", Contract.address)) Argument order It is only possible to have one (1) string parameter in the event, but it can be placed in any position (and its value will end up in the data field), i.e. -AnotherEvent(string, indexed address) +AnotherEvent(string, indexed address) -... +... -Chain.event(AnotherEvent("This is not indexed", Contract.address)) +Chain.event(AnotherEvent("This is not indexed", Contract.address)) would yield exactly the same result in the example above! Compiler pragmas @@ -2012,8 +2031,8 @@ would yield exactly the same result in the example above! Sophia compiler, you can give one or more @compiler pragmas at the top-level (typically at the beginning) of a file. For instance, to enforce that a contract is compiled with version 4.3 of the compiler you write -@compiler >= 4.3 -@compiler < 4.4 +@compiler >= 4.3 +@compiler < 4.4 Valid operators in compiler pragmas are <, =<, ==, >=, and >. Version numbers are given as a sequence of non-negative integers separated by dots. @@ -2021,18 +2040,18 @@ Trailing zeros are ignored, so 4.0.0 == 4. If a constraint is viola error is reported and compilation fails. Exceptions Contracts can fail with an (uncatchable) exception using the built-in function -abort(reason : string) : 'a +abort(reason : string) : 'a Calling abort causes the top-level call transaction to return an error result containing the reason string. Only the gas used up to and including the abort call is charged. This is different from termination due to a crash which consumes all available gas. For convenience the following function is also built-in: -function require(b : bool, err : string) = - if(!b) abort(err) +function require(b : bool, err : string) = + if(!b) abort(err) Aside from that, there is an almost equivalent function exit -exit(reason : string) : 'a +exit(reason : string) : 'a Just like abort, it breaks the execution with the given reason. The difference however is in the gas consumption — while abort returns unused gas, a call to @@ -2043,69 +2062,35 @@ optional delegation signature. This is typically used when a user/accounts would like to allow a contract to act on it's behalf. The exact data to be signed varies for the different operations, but in all cases you should prepend the signature data with the network_id (ae_mainnet for the æternity mainnet, etc.). - - - - - - - + + + + + + + + + + - - + + + + + + + @@ -81,11 +104,11 @@ - + - + @@ -107,20 +130,18 @@ - - + - - + @@ -129,26 +150,25 @@ - + - - + - - + + - - + + - - + + @@ -161,7 +181,7 @@ Initializing search - + @@ -170,11 +190,10 @@ - - + - + GitHub @@ -209,18 +228,17 @@ - + æternity Sophia Language - - + - + GitHub @@ -286,7 +304,7 @@ - + @@ -303,7 +321,6 @@ - @@ -438,7 +455,7 @@ - BLS1295381 + BLS12_381 @@ -555,7 +572,6 @@ - @@ -690,7 +706,7 @@ - BLS1295381 + BLS12_381 @@ -764,12 +780,15 @@ - - - + + + - - GitHub @@ -209,18 +228,17 @@ - + æternity Sophia Language - - + - + GitHub @@ -256,7 +274,7 @@ - + @@ -273,7 +291,6 @@ - @@ -458,7 +475,6 @@ - @@ -570,12 +586,15 @@ - - - + + + - - Syntax + + + + +Syntax Lexical syntax Comments Single line comments start with // and block comments are enclosed in /* @@ -662,11 +681,11 @@ indented more than the currently enclosing layout block. Blocks with a single element can be written on the same line as the previous token. Each element of the block must share the same indentation and no part of an element may be indented less than the indentation of the block. For instance -contract Layout = +contract Layout = function foo() = 0 // no layout function bar() = // layout block starts on next line let x = foo() // indented more than 2 spaces - x + x + 1 // the '+' is indented more than the 'x' Notation @@ -687,107 +706,107 @@ element may be indented less than the indentation of the block. For instance Declarations A Sophia file consists of a sequence of declarations in a layout block. -File ::= Block(TopDecl) +File ::= Block(TopDecl) -TopDecl ::= ['payable'] ['main'] 'contract' Con [Implement] '=' Block(Decl) - | 'contract' 'interface' Con [Implement] '=' Block(Decl) - | 'namespace' Con '=' Block(Decl) - | '@compiler' PragmaOp Version - | 'include' String - | Using +TopDecl ::= ['payable'] ['main'] 'contract' Con [Implement] '=' Block(Decl) + | 'contract' 'interface' Con [Implement] '=' Block(Decl) + | 'namespace' Con '=' Block(Decl) + | '@compiler' PragmaOp Version + | 'include' String + | Using -Implement ::= ':' Sep1(Con, ',') +Implement ::= ':' Sep1(Con, ',') -Decl ::= 'type' Id ['(' TVar* ')'] '=' TypeAlias - | 'record' Id ['(' TVar* ')'] '=' RecordType - | 'datatype' Id ['(' TVar* ')'] '=' DataType - | (EModifier* 'entrypoint' | FModifier* 'function') Block(FunDecl) - | Using +Decl ::= 'type' Id ['(' TVar* ')'] '=' TypeAlias + | 'record' Id ['(' TVar* ')'] '=' RecordType + | 'datatype' Id ['(' TVar* ')'] '=' DataType + | (EModifier* 'entrypoint' | FModifier* 'function') Block(FunDecl) + | Using FunDecl ::= Id ':' Type // Type signature | Id Args [':' Type] '=' Block(Stmt) // Definition | Id Args [':' Type] Block(GuardedDef) // Guarded definitions -GuardedDef ::= '|' Sep1(Expr, ',') '=' Block(Stmt) +GuardedDef ::= '|' Sep1(Expr, ',') '=' Block(Stmt) -Using ::= 'using' Con ['as' Con] [UsingParts] -UsingParts ::= 'for' '[' Sep1(Id, ',') ']' - | 'hiding' '[' Sep1(Id, ',') ']' +Using ::= 'using' Con ['as' Con] [UsingParts] +UsingParts ::= 'for' '[' Sep1(Id, ',') ']' + | 'hiding' '[' Sep1(Id, ',') ']' -PragmaOp ::= '<' | '=<' | '==' | '>=' | '>' -Version ::= Sep1(Int, '.') +PragmaOp ::= '<' | '=<' | '==' | '>=' | '>' +Version ::= Sep1(Int, '.') -EModifier ::= 'payable' | 'stateful' -FModifier ::= 'stateful' | 'private' +EModifier ::= 'payable' | 'stateful' +FModifier ::= 'stateful' | 'private' -Args ::= '(' Sep(Pattern, ',') ')' +Args ::= '(' Sep(Pattern, ',') ')' Contract declarations must appear at the top-level. For example, -contract Test = - type t = int - entrypoint add (x : t, y : t) = x + y +contract Test = + type t = int + entrypoint add (x : t, y : t) = x + y There are three forms of type declarations: type aliases (declared with the type keyword), record type definitions (record) and data type definitions (datatype): -TypeAlias ::= Type -RecordType ::= '{' Sep(FieldType, ',') '}' -DataType ::= Sep1(ConDecl, '|') +TypeAlias ::= Type +RecordType ::= '{' Sep(FieldType, ',') '}' +DataType ::= Sep1(ConDecl, '|') -FieldType ::= Id ':' Type -ConDecl ::= Con ['(' Sep1(Type, ',') ')'] +FieldType ::= Id ':' Type +ConDecl ::= Con ['(' Sep1(Type, ',') ')'] For example, -record point('a) = {x : 'a, y : 'a} -datatype shape('a) = Circle(point('a), 'a) | Rect(point('a), point('a)) -type int_shape = shape(int) +record point('a) = {x : 'a, y : 'a} +datatype shape('a) = Circle(point('a), 'a) | Rect(point('a), point('a)) +type int_shape = shape(int) Types Type ::= Domain '=>' Type // Function type | Type '(' Sep(Type, ',') ')' // Type application | '(' Type ')' // Parens | 'unit' | Sep(Type, '*') // Tuples - | Id | QId | TVar + | Id | QId | TVar Domain ::= Type // Single argument | '(' Sep(Type, ',') ')' // Multiple arguments The function type arrow associates to the right. Example, -'a => list('a) => (int * list('a)) +'a => list('a) => (int * list('a)) Statements Function bodies are blocks of statements, where a statement is one of the following -Stmt ::= 'switch' '(' Expr ')' Block(Case) - | 'if' '(' Expr ')' Block(Stmt) - | 'elif' '(' Expr ')' Block(Stmt) - | 'else' Block(Stmt) - | 'let' LetDef - | Using - | Expr +Stmt ::= 'switch' '(' Expr ')' Block(Case) + | 'if' '(' Expr ')' Block(Stmt) + | 'elif' '(' Expr ')' Block(Stmt) + | 'else' Block(Stmt) + | 'let' LetDef + | Using + | Expr LetDef ::= Id Args [':' Type] '=' Block(Stmt) // Function definition | Pattern '=' Block(Stmt) // Value definition -Case ::= Pattern '=>' Block(Stmt) - | Pattern Block(GuardedCase) +Case ::= Pattern '=>' Block(Stmt) + | Pattern Block(GuardedCase) -GuardedCase ::= '|' Sep1(Expr, ',') '=>' Block(Stmt) +GuardedCase ::= '|' Sep1(Expr, ',') '=>' Block(Stmt) -Pattern ::= Expr +Pattern ::= Expr if statements can be followed by zero or more elif statements and an optional final else statement. For example, -let x : int = 4 -switch(f(x)) - None => 0 - Some(y) => - if(y > 10) - "too big" - elif(y < 3) - "too small" - else - "just right" +let x : int = 4 +switch(f(x)) + None => 0 + Some(y) => + if(y > 10) + "too big" + elif(y < 3) + "too small" + else + "just right" Expressions Expr ::= '(' LamArgs ')' '=>' Block(Stmt) // Anonymous function (x) => x + 1 @@ -801,7 +820,7 @@ element may be indented less than the indentation of the block. For instance | Expr '[' Expr ']' // Map lookup map[key] | Expr '{' Sep(FieldUpdate, ',') '}' // Record or map update r{ fld[key].x = y } | '[' Sep(Expr, ',') ']' // List [1, 2, 3] - | '[' Expr '|' Sep(Generator, ',') ']' + | '[' Expr '|' Sep(Generator, ',') ']' // List comprehension [k | x <- [1], if (f(x)), let k = x+1] | '[' Expr '..' Expr ']' // List range [1..n] | '{' Sep(FieldUpdate, ',') '}' // Record or map value {x = 0, y = 1}, {[key] = val} @@ -817,19 +836,19 @@ element may be indented less than the indentation of the block. For instance | 'if' '(' Expr ')' // Guard | LetDef // Definition -LamArgs ::= '(' Sep(LamArg, ',') ')' -LamArg ::= Id [':' Type] +LamArgs ::= '(' Sep(LamArg, ',') ')' +LamArg ::= Id [':' Type] -FieldUpdate ::= Path '=' Expr +FieldUpdate ::= Path '=' Expr Path ::= Id // Record field | '[' Expr ']' // Map key | Path '.' Id // Nested record field | Path '[' Expr ']' // Nested map key -BinOp ::= '||' | '&&' | '<' | '>' | '=<' | '>=' | '==' | '!=' - | '::' | '++' | '+' | '-' | '*' | '/' | 'mod' | '^' - | '|>' -UnOp ::= '-' | '!' +BinOp ::= '||' | '&&' | '<' | '>' | '=<' | '>=' | '==' | '!=' + | '::' | '++' | '+' | '-' | '*' | '/' | 'mod' | '^' + | '|>' +UnOp ::= '-' | '!' Operators types @@ -914,69 +933,35 @@ element may be indented less than the indentation of the block. For instance - - - - - - - + + + + + + + + + + - -
- + + + - - GitHub @@ -209,18 +228,17 @@ - + æternity Sophia Language - - + - + GitHub @@ -256,7 +274,7 @@ - + @@ -273,7 +291,6 @@ - @@ -458,7 +475,6 @@ - @@ -570,12 +586,15 @@ - - - + + + - - Syntax + + + + +Syntax Lexical syntax Comments Single line comments start with // and block comments are enclosed in /* @@ -662,11 +681,11 @@ indented more than the currently enclosing layout block. Blocks with a single element can be written on the same line as the previous token. Each element of the block must share the same indentation and no part of an element may be indented less than the indentation of the block. For instance -contract Layout = +contract Layout = function foo() = 0 // no layout function bar() = // layout block starts on next line let x = foo() // indented more than 2 spaces - x + x + 1 // the '+' is indented more than the 'x' Notation @@ -687,107 +706,107 @@ element may be indented less than the indentation of the block. For instance Declarations A Sophia file consists of a sequence of declarations in a layout block. -File ::= Block(TopDecl) +File ::= Block(TopDecl) -TopDecl ::= ['payable'] ['main'] 'contract' Con [Implement] '=' Block(Decl) - | 'contract' 'interface' Con [Implement] '=' Block(Decl) - | 'namespace' Con '=' Block(Decl) - | '@compiler' PragmaOp Version - | 'include' String - | Using +TopDecl ::= ['payable'] ['main'] 'contract' Con [Implement] '=' Block(Decl) + | 'contract' 'interface' Con [Implement] '=' Block(Decl) + | 'namespace' Con '=' Block(Decl) + | '@compiler' PragmaOp Version + | 'include' String + | Using -Implement ::= ':' Sep1(Con, ',') +Implement ::= ':' Sep1(Con, ',') -Decl ::= 'type' Id ['(' TVar* ')'] '=' TypeAlias - | 'record' Id ['(' TVar* ')'] '=' RecordType - | 'datatype' Id ['(' TVar* ')'] '=' DataType - | (EModifier* 'entrypoint' | FModifier* 'function') Block(FunDecl) - | Using +Decl ::= 'type' Id ['(' TVar* ')'] '=' TypeAlias + | 'record' Id ['(' TVar* ')'] '=' RecordType + | 'datatype' Id ['(' TVar* ')'] '=' DataType + | (EModifier* 'entrypoint' | FModifier* 'function') Block(FunDecl) + | Using FunDecl ::= Id ':' Type // Type signature | Id Args [':' Type] '=' Block(Stmt) // Definition | Id Args [':' Type] Block(GuardedDef) // Guarded definitions -GuardedDef ::= '|' Sep1(Expr, ',') '=' Block(Stmt) +GuardedDef ::= '|' Sep1(Expr, ',') '=' Block(Stmt) -Using ::= 'using' Con ['as' Con] [UsingParts] -UsingParts ::= 'for' '[' Sep1(Id, ',') ']' - | 'hiding' '[' Sep1(Id, ',') ']' +Using ::= 'using' Con ['as' Con] [UsingParts] +UsingParts ::= 'for' '[' Sep1(Id, ',') ']' + | 'hiding' '[' Sep1(Id, ',') ']' -PragmaOp ::= '<' | '=<' | '==' | '>=' | '>' -Version ::= Sep1(Int, '.') +PragmaOp ::= '<' | '=<' | '==' | '>=' | '>' +Version ::= Sep1(Int, '.') -EModifier ::= 'payable' | 'stateful' -FModifier ::= 'stateful' | 'private' +EModifier ::= 'payable' | 'stateful' +FModifier ::= 'stateful' | 'private' -Args ::= '(' Sep(Pattern, ',') ')' +Args ::= '(' Sep(Pattern, ',') ')' Contract declarations must appear at the top-level. For example, -contract Test = - type t = int - entrypoint add (x : t, y : t) = x + y +contract Test = + type t = int + entrypoint add (x : t, y : t) = x + y There are three forms of type declarations: type aliases (declared with the type keyword), record type definitions (record) and data type definitions (datatype): -TypeAlias ::= Type -RecordType ::= '{' Sep(FieldType, ',') '}' -DataType ::= Sep1(ConDecl, '|') +TypeAlias ::= Type +RecordType ::= '{' Sep(FieldType, ',') '}' +DataType ::= Sep1(ConDecl, '|') -FieldType ::= Id ':' Type -ConDecl ::= Con ['(' Sep1(Type, ',') ')'] +FieldType ::= Id ':' Type +ConDecl ::= Con ['(' Sep1(Type, ',') ')'] For example, -record point('a) = {x : 'a, y : 'a} -datatype shape('a) = Circle(point('a), 'a) | Rect(point('a), point('a)) -type int_shape = shape(int) +record point('a) = {x : 'a, y : 'a} +datatype shape('a) = Circle(point('a), 'a) | Rect(point('a), point('a)) +type int_shape = shape(int) Types Type ::= Domain '=>' Type // Function type | Type '(' Sep(Type, ',') ')' // Type application | '(' Type ')' // Parens | 'unit' | Sep(Type, '*') // Tuples - | Id | QId | TVar + | Id | QId | TVar Domain ::= Type // Single argument | '(' Sep(Type, ',') ')' // Multiple arguments The function type arrow associates to the right. Example, -'a => list('a) => (int * list('a)) +'a => list('a) => (int * list('a)) Statements Function bodies are blocks of statements, where a statement is one of the following -Stmt ::= 'switch' '(' Expr ')' Block(Case) - | 'if' '(' Expr ')' Block(Stmt) - | 'elif' '(' Expr ')' Block(Stmt) - | 'else' Block(Stmt) - | 'let' LetDef - | Using - | Expr +Stmt ::= 'switch' '(' Expr ')' Block(Case) + | 'if' '(' Expr ')' Block(Stmt) + | 'elif' '(' Expr ')' Block(Stmt) + | 'else' Block(Stmt) + | 'let' LetDef + | Using + | Expr LetDef ::= Id Args [':' Type] '=' Block(Stmt) // Function definition | Pattern '=' Block(Stmt) // Value definition -Case ::= Pattern '=>' Block(Stmt) - | Pattern Block(GuardedCase) +Case ::= Pattern '=>' Block(Stmt) + | Pattern Block(GuardedCase) -GuardedCase ::= '|' Sep1(Expr, ',') '=>' Block(Stmt) +GuardedCase ::= '|' Sep1(Expr, ',') '=>' Block(Stmt) -Pattern ::= Expr +Pattern ::= Expr if statements can be followed by zero or more elif statements and an optional final else statement. For example, -let x : int = 4 -switch(f(x)) - None => 0 - Some(y) => - if(y > 10) - "too big" - elif(y < 3) - "too small" - else - "just right" +let x : int = 4 +switch(f(x)) + None => 0 + Some(y) => + if(y > 10) + "too big" + elif(y < 3) + "too small" + else + "just right" Expressions Expr ::= '(' LamArgs ')' '=>' Block(Stmt) // Anonymous function (x) => x + 1 @@ -801,7 +820,7 @@ element may be indented less than the indentation of the block. For instance | Expr '[' Expr ']' // Map lookup map[key] | Expr '{' Sep(FieldUpdate, ',') '}' // Record or map update r{ fld[key].x = y } | '[' Sep(Expr, ',') ']' // List [1, 2, 3] - | '[' Expr '|' Sep(Generator, ',') ']' + | '[' Expr '|' Sep(Generator, ',') ']' // List comprehension [k | x <- [1], if (f(x)), let k = x+1] | '[' Expr '..' Expr ']' // List range [1..n] | '{' Sep(FieldUpdate, ',') '}' // Record or map value {x = 0, y = 1}, {[key] = val} @@ -817,19 +836,19 @@ element may be indented less than the indentation of the block. For instance | 'if' '(' Expr ')' // Guard | LetDef // Definition -LamArgs ::= '(' Sep(LamArg, ',') ')' -LamArg ::= Id [':' Type] +LamArgs ::= '(' Sep(LamArg, ',') ')' +LamArg ::= Id [':' Type] -FieldUpdate ::= Path '=' Expr +FieldUpdate ::= Path '=' Expr Path ::= Id // Record field | '[' Expr ']' // Map key | Path '.' Id // Nested record field | Path '[' Expr ']' // Nested map key -BinOp ::= '||' | '&&' | '<' | '>' | '=<' | '>=' | '==' | '!=' - | '::' | '++' | '+' | '-' | '*' | '/' | 'mod' | '^' - | '|>' -UnOp ::= '-' | '!' +BinOp ::= '||' | '&&' | '<' | '>' | '=<' | '>=' | '==' | '!=' + | '::' | '++' | '+' | '-' | '*' | '/' | 'mod' | '^' + | '|>' +UnOp ::= '-' | '!' Operators types @@ -914,69 +933,35 @@ element may be indented less than the indentation of the block. For instance - - - - - - - + + + + + + + + + + - -
- + + + - - Syntax + + + + +Syntax Lexical syntax Comments Single line comments start with // and block comments are enclosed in /* @@ -662,11 +681,11 @@ indented more than the currently enclosing layout block. Blocks with a single element can be written on the same line as the previous token. Each element of the block must share the same indentation and no part of an element may be indented less than the indentation of the block. For instance -contract Layout = +contract Layout = function foo() = 0 // no layout function bar() = // layout block starts on next line let x = foo() // indented more than 2 spaces - x + x + 1 // the '+' is indented more than the 'x' Notation @@ -687,107 +706,107 @@ element may be indented less than the indentation of the block. For instance Declarations A Sophia file consists of a sequence of declarations in a layout block. -File ::= Block(TopDecl) +File ::= Block(TopDecl) -TopDecl ::= ['payable'] ['main'] 'contract' Con [Implement] '=' Block(Decl) - | 'contract' 'interface' Con [Implement] '=' Block(Decl) - | 'namespace' Con '=' Block(Decl) - | '@compiler' PragmaOp Version - | 'include' String - | Using +TopDecl ::= ['payable'] ['main'] 'contract' Con [Implement] '=' Block(Decl) + | 'contract' 'interface' Con [Implement] '=' Block(Decl) + | 'namespace' Con '=' Block(Decl) + | '@compiler' PragmaOp Version + | 'include' String + | Using -Implement ::= ':' Sep1(Con, ',') +Implement ::= ':' Sep1(Con, ',') -Decl ::= 'type' Id ['(' TVar* ')'] '=' TypeAlias - | 'record' Id ['(' TVar* ')'] '=' RecordType - | 'datatype' Id ['(' TVar* ')'] '=' DataType - | (EModifier* 'entrypoint' | FModifier* 'function') Block(FunDecl) - | Using +Decl ::= 'type' Id ['(' TVar* ')'] '=' TypeAlias + | 'record' Id ['(' TVar* ')'] '=' RecordType + | 'datatype' Id ['(' TVar* ')'] '=' DataType + | (EModifier* 'entrypoint' | FModifier* 'function') Block(FunDecl) + | Using FunDecl ::= Id ':' Type // Type signature | Id Args [':' Type] '=' Block(Stmt) // Definition | Id Args [':' Type] Block(GuardedDef) // Guarded definitions -GuardedDef ::= '|' Sep1(Expr, ',') '=' Block(Stmt) +GuardedDef ::= '|' Sep1(Expr, ',') '=' Block(Stmt) -Using ::= 'using' Con ['as' Con] [UsingParts] -UsingParts ::= 'for' '[' Sep1(Id, ',') ']' - | 'hiding' '[' Sep1(Id, ',') ']' +Using ::= 'using' Con ['as' Con] [UsingParts] +UsingParts ::= 'for' '[' Sep1(Id, ',') ']' + | 'hiding' '[' Sep1(Id, ',') ']' -PragmaOp ::= '<' | '=<' | '==' | '>=' | '>' -Version ::= Sep1(Int, '.') +PragmaOp ::= '<' | '=<' | '==' | '>=' | '>' +Version ::= Sep1(Int, '.') -EModifier ::= 'payable' | 'stateful' -FModifier ::= 'stateful' | 'private' +EModifier ::= 'payable' | 'stateful' +FModifier ::= 'stateful' | 'private' -Args ::= '(' Sep(Pattern, ',') ')' +Args ::= '(' Sep(Pattern, ',') ')' Contract declarations must appear at the top-level. For example, -contract Test = - type t = int - entrypoint add (x : t, y : t) = x + y +contract Test = + type t = int + entrypoint add (x : t, y : t) = x + y There are three forms of type declarations: type aliases (declared with the type keyword), record type definitions (record) and data type definitions (datatype): -TypeAlias ::= Type -RecordType ::= '{' Sep(FieldType, ',') '}' -DataType ::= Sep1(ConDecl, '|') +TypeAlias ::= Type +RecordType ::= '{' Sep(FieldType, ',') '}' +DataType ::= Sep1(ConDecl, '|') -FieldType ::= Id ':' Type -ConDecl ::= Con ['(' Sep1(Type, ',') ')'] +FieldType ::= Id ':' Type +ConDecl ::= Con ['(' Sep1(Type, ',') ')'] For example, -record point('a) = {x : 'a, y : 'a} -datatype shape('a) = Circle(point('a), 'a) | Rect(point('a), point('a)) -type int_shape = shape(int) +record point('a) = {x : 'a, y : 'a} +datatype shape('a) = Circle(point('a), 'a) | Rect(point('a), point('a)) +type int_shape = shape(int) Types Type ::= Domain '=>' Type // Function type | Type '(' Sep(Type, ',') ')' // Type application | '(' Type ')' // Parens | 'unit' | Sep(Type, '*') // Tuples - | Id | QId | TVar + | Id | QId | TVar Domain ::= Type // Single argument | '(' Sep(Type, ',') ')' // Multiple arguments The function type arrow associates to the right. Example, -'a => list('a) => (int * list('a)) +'a => list('a) => (int * list('a)) Statements Function bodies are blocks of statements, where a statement is one of the following -Stmt ::= 'switch' '(' Expr ')' Block(Case) - | 'if' '(' Expr ')' Block(Stmt) - | 'elif' '(' Expr ')' Block(Stmt) - | 'else' Block(Stmt) - | 'let' LetDef - | Using - | Expr +Stmt ::= 'switch' '(' Expr ')' Block(Case) + | 'if' '(' Expr ')' Block(Stmt) + | 'elif' '(' Expr ')' Block(Stmt) + | 'else' Block(Stmt) + | 'let' LetDef + | Using + | Expr LetDef ::= Id Args [':' Type] '=' Block(Stmt) // Function definition | Pattern '=' Block(Stmt) // Value definition -Case ::= Pattern '=>' Block(Stmt) - | Pattern Block(GuardedCase) +Case ::= Pattern '=>' Block(Stmt) + | Pattern Block(GuardedCase) -GuardedCase ::= '|' Sep1(Expr, ',') '=>' Block(Stmt) +GuardedCase ::= '|' Sep1(Expr, ',') '=>' Block(Stmt) -Pattern ::= Expr +Pattern ::= Expr if statements can be followed by zero or more elif statements and an optional final else statement. For example, -let x : int = 4 -switch(f(x)) - None => 0 - Some(y) => - if(y > 10) - "too big" - elif(y < 3) - "too small" - else - "just right" +let x : int = 4 +switch(f(x)) + None => 0 + Some(y) => + if(y > 10) + "too big" + elif(y < 3) + "too small" + else + "just right" Expressions Expr ::= '(' LamArgs ')' '=>' Block(Stmt) // Anonymous function (x) => x + 1 @@ -801,7 +820,7 @@ element may be indented less than the indentation of the block. For instance | Expr '[' Expr ']' // Map lookup map[key] | Expr '{' Sep(FieldUpdate, ',') '}' // Record or map update r{ fld[key].x = y } | '[' Sep(Expr, ',') ']' // List [1, 2, 3] - | '[' Expr '|' Sep(Generator, ',') ']' + | '[' Expr '|' Sep(Generator, ',') ']' // List comprehension [k | x <- [1], if (f(x)), let k = x+1] | '[' Expr '..' Expr ']' // List range [1..n] | '{' Sep(FieldUpdate, ',') '}' // Record or map value {x = 0, y = 1}, {[key] = val} @@ -817,19 +836,19 @@ element may be indented less than the indentation of the block. For instance | 'if' '(' Expr ')' // Guard | LetDef // Definition -LamArgs ::= '(' Sep(LamArg, ',') ')' -LamArg ::= Id [':' Type] +LamArgs ::= '(' Sep(LamArg, ',') ')' +LamArg ::= Id [':' Type] -FieldUpdate ::= Path '=' Expr +FieldUpdate ::= Path '=' Expr Path ::= Id // Record field | '[' Expr ']' // Map key | Path '.' Id // Nested record field | Path '[' Expr ']' // Nested map key -BinOp ::= '||' | '&&' | '<' | '>' | '=<' | '>=' | '==' | '!=' - | '::' | '++' | '+' | '-' | '*' | '/' | 'mod' | '^' - | '|>' -UnOp ::= '-' | '!' +BinOp ::= '||' | '&&' | '<' | '>' | '=<' | '>=' | '==' | '!=' + | '::' | '++' | '+' | '-' | '*' | '/' | 'mod' | '^' + | '|>' +UnOp ::= '-' | '!' Operators types @@ -914,69 +933,35 @@ element may be indented less than the indentation of the block. For instance - - - - - - - + + + + + + + + + + - -
- - Syntax + + + + +Syntax Lexical syntax Comments Single line comments start with // and block comments are enclosed in /* @@ -662,11 +681,11 @@ indented more than the currently enclosing layout block. Blocks with a single element can be written on the same line as the previous token. Each element of the block must share the same indentation and no part of an element may be indented less than the indentation of the block. For instance -contract Layout = +contract Layout = function foo() = 0 // no layout function bar() = // layout block starts on next line let x = foo() // indented more than 2 spaces - x + x + 1 // the '+' is indented more than the 'x' Notation @@ -687,107 +706,107 @@ element may be indented less than the indentation of the block. For instance Declarations A Sophia file consists of a sequence of declarations in a layout block. -File ::= Block(TopDecl) +File ::= Block(TopDecl) -TopDecl ::= ['payable'] ['main'] 'contract' Con [Implement] '=' Block(Decl) - | 'contract' 'interface' Con [Implement] '=' Block(Decl) - | 'namespace' Con '=' Block(Decl) - | '@compiler' PragmaOp Version - | 'include' String - | Using +TopDecl ::= ['payable'] ['main'] 'contract' Con [Implement] '=' Block(Decl) + | 'contract' 'interface' Con [Implement] '=' Block(Decl) + | 'namespace' Con '=' Block(Decl) + | '@compiler' PragmaOp Version + | 'include' String + | Using -Implement ::= ':' Sep1(Con, ',') +Implement ::= ':' Sep1(Con, ',') -Decl ::= 'type' Id ['(' TVar* ')'] '=' TypeAlias - | 'record' Id ['(' TVar* ')'] '=' RecordType - | 'datatype' Id ['(' TVar* ')'] '=' DataType - | (EModifier* 'entrypoint' | FModifier* 'function') Block(FunDecl) - | Using +Decl ::= 'type' Id ['(' TVar* ')'] '=' TypeAlias + | 'record' Id ['(' TVar* ')'] '=' RecordType + | 'datatype' Id ['(' TVar* ')'] '=' DataType + | (EModifier* 'entrypoint' | FModifier* 'function') Block(FunDecl) + | Using FunDecl ::= Id ':' Type // Type signature | Id Args [':' Type] '=' Block(Stmt) // Definition | Id Args [':' Type] Block(GuardedDef) // Guarded definitions -GuardedDef ::= '|' Sep1(Expr, ',') '=' Block(Stmt) +GuardedDef ::= '|' Sep1(Expr, ',') '=' Block(Stmt) -Using ::= 'using' Con ['as' Con] [UsingParts] -UsingParts ::= 'for' '[' Sep1(Id, ',') ']' - | 'hiding' '[' Sep1(Id, ',') ']' +Using ::= 'using' Con ['as' Con] [UsingParts] +UsingParts ::= 'for' '[' Sep1(Id, ',') ']' + | 'hiding' '[' Sep1(Id, ',') ']' -PragmaOp ::= '<' | '=<' | '==' | '>=' | '>' -Version ::= Sep1(Int, '.') +PragmaOp ::= '<' | '=<' | '==' | '>=' | '>' +Version ::= Sep1(Int, '.') -EModifier ::= 'payable' | 'stateful' -FModifier ::= 'stateful' | 'private' +EModifier ::= 'payable' | 'stateful' +FModifier ::= 'stateful' | 'private' -Args ::= '(' Sep(Pattern, ',') ')' +Args ::= '(' Sep(Pattern, ',') ')' Contract declarations must appear at the top-level. For example, -contract Test = - type t = int - entrypoint add (x : t, y : t) = x + y +contract Test = + type t = int + entrypoint add (x : t, y : t) = x + y There are three forms of type declarations: type aliases (declared with the type keyword), record type definitions (record) and data type definitions (datatype): -TypeAlias ::= Type -RecordType ::= '{' Sep(FieldType, ',') '}' -DataType ::= Sep1(ConDecl, '|') +TypeAlias ::= Type +RecordType ::= '{' Sep(FieldType, ',') '}' +DataType ::= Sep1(ConDecl, '|') -FieldType ::= Id ':' Type -ConDecl ::= Con ['(' Sep1(Type, ',') ')'] +FieldType ::= Id ':' Type +ConDecl ::= Con ['(' Sep1(Type, ',') ')'] For example, -record point('a) = {x : 'a, y : 'a} -datatype shape('a) = Circle(point('a), 'a) | Rect(point('a), point('a)) -type int_shape = shape(int) +record point('a) = {x : 'a, y : 'a} +datatype shape('a) = Circle(point('a), 'a) | Rect(point('a), point('a)) +type int_shape = shape(int) Types Type ::= Domain '=>' Type // Function type | Type '(' Sep(Type, ',') ')' // Type application | '(' Type ')' // Parens | 'unit' | Sep(Type, '*') // Tuples - | Id | QId | TVar + | Id | QId | TVar Domain ::= Type // Single argument | '(' Sep(Type, ',') ')' // Multiple arguments The function type arrow associates to the right. Example, -'a => list('a) => (int * list('a)) +'a => list('a) => (int * list('a)) Statements Function bodies are blocks of statements, where a statement is one of the following -Stmt ::= 'switch' '(' Expr ')' Block(Case) - | 'if' '(' Expr ')' Block(Stmt) - | 'elif' '(' Expr ')' Block(Stmt) - | 'else' Block(Stmt) - | 'let' LetDef - | Using - | Expr +Stmt ::= 'switch' '(' Expr ')' Block(Case) + | 'if' '(' Expr ')' Block(Stmt) + | 'elif' '(' Expr ')' Block(Stmt) + | 'else' Block(Stmt) + | 'let' LetDef + | Using + | Expr LetDef ::= Id Args [':' Type] '=' Block(Stmt) // Function definition | Pattern '=' Block(Stmt) // Value definition -Case ::= Pattern '=>' Block(Stmt) - | Pattern Block(GuardedCase) +Case ::= Pattern '=>' Block(Stmt) + | Pattern Block(GuardedCase) -GuardedCase ::= '|' Sep1(Expr, ',') '=>' Block(Stmt) +GuardedCase ::= '|' Sep1(Expr, ',') '=>' Block(Stmt) -Pattern ::= Expr +Pattern ::= Expr if statements can be followed by zero or more elif statements and an optional final else statement. For example, -let x : int = 4 -switch(f(x)) - None => 0 - Some(y) => - if(y > 10) - "too big" - elif(y < 3) - "too small" - else - "just right" +let x : int = 4 +switch(f(x)) + None => 0 + Some(y) => + if(y > 10) + "too big" + elif(y < 3) + "too small" + else + "just right" Expressions Expr ::= '(' LamArgs ')' '=>' Block(Stmt) // Anonymous function (x) => x + 1 @@ -801,7 +820,7 @@ element may be indented less than the indentation of the block. For instance | Expr '[' Expr ']' // Map lookup map[key] | Expr '{' Sep(FieldUpdate, ',') '}' // Record or map update r{ fld[key].x = y } | '[' Sep(Expr, ',') ']' // List [1, 2, 3] - | '[' Expr '|' Sep(Generator, ',') ']' + | '[' Expr '|' Sep(Generator, ',') ']' // List comprehension [k | x <- [1], if (f(x)), let k = x+1] | '[' Expr '..' Expr ']' // List range [1..n] | '{' Sep(FieldUpdate, ',') '}' // Record or map value {x = 0, y = 1}, {[key] = val} @@ -817,19 +836,19 @@ element may be indented less than the indentation of the block. For instance | 'if' '(' Expr ')' // Guard | LetDef // Definition -LamArgs ::= '(' Sep(LamArg, ',') ')' -LamArg ::= Id [':' Type] +LamArgs ::= '(' Sep(LamArg, ',') ')' +LamArg ::= Id [':' Type] -FieldUpdate ::= Path '=' Expr +FieldUpdate ::= Path '=' Expr Path ::= Id // Record field | '[' Expr ']' // Map key | Path '.' Id // Nested record field | Path '[' Expr ']' // Nested map key -BinOp ::= '||' | '&&' | '<' | '>' | '=<' | '>=' | '==' | '!=' - | '::' | '++' | '+' | '-' | '*' | '/' | 'mod' | '^' - | '|>' -UnOp ::= '-' | '!' +BinOp ::= '||' | '&&' | '<' | '>' | '=<' | '>=' | '==' | '!=' + | '::' | '++' | '+' | '-' | '*' | '/' | 'mod' | '^' + | '|>' +UnOp ::= '-' | '!' Operators types @@ -914,69 +933,35 @@ element may be indented less than the indentation of the block. For instance - - - - - - - + + + + + + + + + + - -