From 79c5282986422221baf3db12deecfb08e090ce9e Mon Sep 17 00:00:00 2001 From: Georgiy Komarov Date: Thu, 6 Oct 2022 12:40:59 +0500 Subject: [PATCH] feat(formatter): Support comments (#1172) This commit adds an extended syntax for Scilla that preserves comments as annotations for AST nodes. Closes #1086 --- src/base/ErrorUtils.ml | 2 +- src/base/ErrorUtils.mli | 2 +- src/base/FrontEndParser.ml | 1 + src/base/ScillaLexer.mll | 28 +- src/base/ScillaParser.mly | 4 +- src/base/TypeChecker.ml | 10 +- src/base/dune | 6 +- src/formatter/ExtendedSyntax.ml | 766 ++++++++++++++++++ src/{base => formatter}/Formatter.ml | 204 +++-- src/formatter/dune | 16 + src/runners/dune | 3 +- src/runners/scilla_fmt.ml | 6 + .../bad/gold/bad_comment_1.scilla.gold | 2 +- .../bad/gold/bad_comment_2.scilla.gold | 2 +- tests/formatter/comments.t/fields-1.scilla | 21 + .../formatter/comments.t/fields-1.scilla.gold | 26 + tests/formatter/comments.t/libvar-1.scilla | 16 + .../formatter/comments.t/libvar-1.scilla.gold | 21 + tests/formatter/comments.t/pm-1.scilla | 70 ++ tests/formatter/comments.t/pm-1.scilla.gold | 72 ++ tests/formatter/comments.t/run.t | 8 + tests/formatter/comments.t/toplevel-1.scilla | 17 + .../comments.t/toplevel-1.scilla.gold | 21 + tests/formatter/comments.t/toplevel-2.scilla | 38 + .../comments.t/toplevel-2.scilla.gold | 40 + tests/formatter/comments.t/toplevel-3.scilla | 10 + .../comments.t/toplevel-3.scilla.gold | 13 + tests/formatter/comments.t/toplevel-4.scilla | 14 + .../comments.t/toplevel-4.scilla.gold | 16 + tests/formatter/comments.t/toplevel-5.scilla | 14 + .../comments.t/toplevel-5.scilla.gold | 17 + tests/formatter/comments.t/toplevel-6.scilla | 10 + .../comments.t/toplevel-6.scilla.gold | 13 + tests/formatter/comments.t/toplevel-7.scilla | 12 + .../comments.t/toplevel-7.scilla.gold | 13 + tests/formatter/comments.t/toplevel-8.scilla | 11 + .../comments.t/toplevel-8.scilla.gold | 13 + tests/formatter/comments.t/typedef-1.scilla | 21 + .../comments.t/typedef-1.scilla.gold | 28 + .../look_and_feel/Polynetwork.t/run.t | 33 +- .../formatter/look_and_feel/ackermann.t/run.t | 3 + tests/formatter/look_and_feel/ark.t/run.t | 62 +- tests/formatter/look_and_feel/auction.t/run.t | 17 + .../formatter/look_and_feel/bookstore.t/run.t | 92 +++ tests/formatter/look_and_feel/chainid.t/run.t | 3 + .../crowdfunding_governor.t/run.t | 15 +- .../look_and_feel/crowdfunding_proc.t/run.t | 17 +- .../crowdfunding_storage.t/run.t | 11 +- .../look_and_feel/earmarked-coin.t/run.t | 33 +- tests/formatter/look_and_feel/empty.t/run.t | 1 + .../look_and_feel/fungible-token.t/run.t | 21 +- .../look_and_feel/helloWorld.t/run.t | 7 + .../look_and_feel/map_corners_test.t/run.t | 90 ++ tests/formatter/look_and_feel/mappair.t/run.t | 5 + .../look_and_feel/multiple-msgs.t/run.t | 7 + .../look_and_feel/remote_state_reads.t/run.t | 28 + .../formatter/look_and_feel/replicate.t/run.t | 1 + .../formatter/look_and_feel/salarybot.t/run.t | 3 + tests/formatter/look_and_feel/shogi.t/run.t | 100 ++- .../look_and_feel/shogi_proc.t/run.t | 119 ++- .../simple-dex-remote-reads.t/run.t | 93 ++- .../look_and_feel/simple-dex.t/run.t | 44 +- .../formatter/look_and_feel/timestamp.t/run.t | 3 + .../look_and_feel/ud-registry.t/run.t | 1 + tests/formatter/look_and_feel/wallet.t/run.t | 110 ++- .../formatter/look_and_feel/wallet_2.t/run.t | 123 ++- .../formatter/look_and_feel/zil-game.t/run.t | 12 + tests/formatter/look_and_feel/zip.t/run.t | 1 + 68 files changed, 2519 insertions(+), 143 deletions(-) create mode 100644 src/formatter/ExtendedSyntax.ml rename src/{base => formatter}/Formatter.ml (71%) create mode 100644 src/formatter/dune create mode 100644 tests/formatter/comments.t/fields-1.scilla create mode 100644 tests/formatter/comments.t/fields-1.scilla.gold create mode 100644 tests/formatter/comments.t/libvar-1.scilla create mode 100644 tests/formatter/comments.t/libvar-1.scilla.gold create mode 100644 tests/formatter/comments.t/pm-1.scilla create mode 100644 tests/formatter/comments.t/pm-1.scilla.gold create mode 100644 tests/formatter/comments.t/run.t create mode 100644 tests/formatter/comments.t/toplevel-1.scilla create mode 100644 tests/formatter/comments.t/toplevel-1.scilla.gold create mode 100644 tests/formatter/comments.t/toplevel-2.scilla create mode 100644 tests/formatter/comments.t/toplevel-2.scilla.gold create mode 100644 tests/formatter/comments.t/toplevel-3.scilla create mode 100644 tests/formatter/comments.t/toplevel-3.scilla.gold create mode 100644 tests/formatter/comments.t/toplevel-4.scilla create mode 100644 tests/formatter/comments.t/toplevel-4.scilla.gold create mode 100644 tests/formatter/comments.t/toplevel-5.scilla create mode 100644 tests/formatter/comments.t/toplevel-5.scilla.gold create mode 100644 tests/formatter/comments.t/toplevel-6.scilla create mode 100644 tests/formatter/comments.t/toplevel-6.scilla.gold create mode 100644 tests/formatter/comments.t/toplevel-7.scilla create mode 100644 tests/formatter/comments.t/toplevel-7.scilla.gold create mode 100644 tests/formatter/comments.t/toplevel-8.scilla create mode 100644 tests/formatter/comments.t/toplevel-8.scilla.gold create mode 100644 tests/formatter/comments.t/typedef-1.scilla create mode 100644 tests/formatter/comments.t/typedef-1.scilla.gold diff --git a/src/base/ErrorUtils.ml b/src/base/ErrorUtils.ml index 506599fff..634dde6fb 100644 --- a/src/base/ErrorUtils.ml +++ b/src/base/ErrorUtils.ml @@ -26,7 +26,7 @@ type loc = { (* line number *) cnum : int; (* column number *) } -[@@deriving sexp, equal] +[@@deriving sexp, equal, compare] let toLoc (p : Lexing.position) : loc = { diff --git a/src/base/ErrorUtils.mli b/src/base/ErrorUtils.mli index 8463bbb6e..a8a1deed5 100644 --- a/src/base/ErrorUtils.mli +++ b/src/base/ErrorUtils.mli @@ -24,7 +24,7 @@ type loc = { (* line number *) cnum : int; (* column number *) } -[@@deriving sexp, equal] +[@@deriving sexp, equal, compare] val toLoc : Lexing.position -> loc val dummy_loc : loc diff --git a/src/base/FrontEndParser.ml b/src/base/FrontEndParser.ml index ed9f69084..d721eb29f 100644 --- a/src/base/FrontEndParser.ml +++ b/src/base/FrontEndParser.ml @@ -87,4 +87,5 @@ module ScillaFrontEndParser (Literal : ScillaLiteral) = struct let parse_expr_from_stdin () = parse_stdin Parser.Incremental.exp_term let parse_lmodule filename = parse_file Parser.Incremental.lmodule filename let parse_cmodule filename = parse_file Parser.Incremental.cmodule filename + let get_comments () = Lexer.get_comments () end diff --git a/src/base/ScillaLexer.mll b/src/base/ScillaLexer.mll index 7165186a8..57000f6f0 100644 --- a/src/base/ScillaLexer.mll +++ b/src/base/ScillaLexer.mll @@ -29,6 +29,11 @@ module MkLexer (S : ParserUtil.Syn) = struct exception Error of string + let comments = ref [] + let add_comment start_p s = + let loc = ErrorUtils.toLoc start_p in + comments := (loc, s) :: !comments + let get_comments () = List.rev !comments } let digit = ['0'-'9'] @@ -55,7 +60,7 @@ rule read = (* Whitespaces *) | newline { new_line lexbuf; read lexbuf } - | "(*" { comment [lexbuf.lex_curr_p] lexbuf } + | "(*" { comment (Buffer.create 50) [lexbuf.lex_start_p] lexbuf } | white { read lexbuf } (* Numbers and hashes *) @@ -148,16 +153,21 @@ and read_string buf = | eof { raise (Error ("String is not terminated")) } (* Nested comments, keeping a list of where comments open *) -and comment braces = +and comment buf braces = parse - | "(*" { comment (lexbuf.lex_curr_p::braces) lexbuf} + | "(*" { comment buf (lexbuf.lex_curr_p::braces) lexbuf } | "*)" { match braces with - _::[] -> read lexbuf - | _ -> comment (List.tl_exn braces) lexbuf } - | newline { new_line lexbuf; comment braces lexbuf} - | _ { comment braces lexbuf} - | eof { lexbuf.lex_curr_p <- List.hd_exn braces; raise (Error ("Comment unfinished"))} + p::[] -> add_comment p (Buffer.contents buf); + read lexbuf + | _ -> comment buf (List.tl_exn braces) lexbuf } + | newline { new_line lexbuf; + Buffer.add_char buf '\n'; + comment buf braces lexbuf } + | _ { Buffer.add_string buf (Lexing.lexeme lexbuf); + comment buf braces lexbuf } + | eof { lexbuf.lex_curr_p <- List.hd_exn braces; + raise (Error ("Comment unfinished")) } { end -} \ No newline at end of file +} diff --git a/src/base/ScillaParser.mly b/src/base/ScillaParser.mly index 2b4202f60..d3e6e3c21 100644 --- a/src/base/ScillaParser.mly +++ b/src/base/ScillaParser.mly @@ -303,11 +303,11 @@ simple_exp : | LET; x = ID; t = ioption(type_annot) EQ; f = simple_exp; IN; e = exp - {(Let ( to_loc_id x (toLoc $startpos(x)), t, f, e), toLoc $startpos(f)) } + {(Let ( to_loc_id x (toLoc $startpos(x)), t, f, e), toLoc $startpos) } (* Function *) | FUN; LPAREN; iwt = id_with_typ; RPAREN; ARROW; e = exp { match iwt with - | (i, t) -> (Fun (i, t, e), toLoc $startpos(e) ) } + | (i, t) -> (Fun (i, t, e), toLoc $startpos ) } (* Application *) | f = sid; args = nonempty_list(sident) diff --git a/src/base/TypeChecker.ml b/src/base/TypeChecker.ml index d1c82ea8b..3f631228c 100644 --- a/src/base/TypeChecker.ml +++ b/src/base/TypeChecker.ml @@ -324,16 +324,18 @@ module ScillaTypechecker (SR : Rep) (ER : Rep) = struct pure @@ ( TypedSyntax.Builtin ((fst b, q_ret_tag), ts, typed_actuals), (q_ret_typ, rep) ) - | Let (i, topt, lhs, rhs) -> + | Let (i, topt, (lhs, lhs_rep), rhs) -> (* Poor man's error reporting *) - let%bind ((_, (ityp, _)) as checked_lhs) = type_expr lhs tenv in + let%bind ((_, (ityp, _)) as checked_lhs) = + type_expr (lhs, lhs_rep) tenv + in let%bind actual_typ = match topt with | Some tannot -> let%bind () = fromR_TE - @@ assert_type_assignable ~lc:(ER.get_loc rep) ~expected:tannot - ~actual:ityp.tp + @@ assert_type_assignable ~lc:(ER.get_loc lhs_rep) + ~expected:tannot ~actual:ityp.tp in pure (mk_qual_tp tannot) | None -> pure ityp diff --git a/src/base/dune b/src/base/dune index 27aaae918..b5413fcfd 100644 --- a/src/base/dune +++ b/src/base/dune @@ -22,8 +22,8 @@ (wrapped true) (libraries core core_unix core_unix.sys_unix num hex stdint angstrom polynomials cryptokit secp256k1 bitstring yojson fileutils scilla_crypto - menhirLib ocamlgraph pprint) + menhirLib ocamlgraph) (preprocess - (pps ppx_sexp_conv ppx_let ppx_deriving.show ppx_compare - ppx_string_interpolation bisect_ppx --conditional)) + (pps ppx_sexp_conv ppx_let ppx_deriving.show ppx_compare bisect_ppx + --conditional)) (synopsis "Scilla workbench implementation.")) diff --git a/src/formatter/ExtendedSyntax.ml b/src/formatter/ExtendedSyntax.ml new file mode 100644 index 000000000..393611d0f --- /dev/null +++ b/src/formatter/ExtendedSyntax.ml @@ -0,0 +1,766 @@ +(* + This file is part of scilla. + + Copyright (c) 2018 - present Zilliqa Research Pvt. Ltd. + + scilla is free software: you can redistribute it and/or modify it under the + terms of the GNU General Public License as published by the Free Software + Foundation, either version 3 of the License, or (at your option) any later + version. + + scilla is distributed in the hope that it will be useful, but WITHOUT ANY + WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR + A PARTICULAR PURPOSE. See the GNU General Public License for more details. + + You should have received a copy of the GNU General Public License along with + scilla. If not, see . +*) + +open Core +open Sexplib.Std +open Scilla_base +open ErrorUtils +open Literal +open GasCharge + +(** Annotated Scilla syntax extended with comment annotations. *) +module ExtendedScillaSyntax + (SR : Syntax.Rep) + (ER : Syntax.Rep) + (Lit : ScillaLiteral) = +struct + module SLiteral = Lit + module SType = SLiteral.LType + module SIdentifier = SType.TIdentifier + module SGasCharge = ScillaGasCharge (SIdentifier.Name) + + type comment_text = string [@@deriving sexp] + type comment_pos = ComLeft | ComAbove | ComRight [@@deriving sexp] + type comment = loc * comment_text * comment_pos [@@deriving sexp] + type annot_comment = comment list [@@deriving sexp] + + type 'a id_ann = 'a SIdentifier.t * annot_comment [@@deriving sexp] + (** Annotated identifier that may be commented. *) + + (*******************************************************) + (* Expressions *) + (*******************************************************) + + type payload = MLit of SLiteral.t | MVar of ER.rep id_ann [@@deriving sexp] + + type pattern = + | Wildcard + | Binder of ER.rep id_ann + | Constructor of SR.rep id_ann * pattern list + [@@deriving sexp] + + type expr_annot = expr * ER.rep * annot_comment + + and expr = + | Literal of SLiteral.t + | Var of ER.rep id_ann + | Let of ER.rep id_ann * SType.t option * expr_annot * expr_annot + | Message of (string * payload) list + | Fun of ER.rep id_ann * SType.t * expr_annot + | App of ER.rep id_ann * ER.rep id_ann list + | Constr of SR.rep id_ann * SType.t list * ER.rep id_ann list + | MatchExpr of + ER.rep id_ann * (pattern * expr_annot * comment_text list) list + | Builtin of ER.rep Syntax.builtin_annot * SType.t list * ER.rep id_ann list + | TFun of ER.rep id_ann * expr_annot + | TApp of ER.rep id_ann * SType.t list + | Fixpoint of ER.rep id_ann * SType.t * expr_annot + | GasExpr of SGasCharge.gas_charge * expr_annot + [@@deriving sexp] + + (*******************************************************) + (* Statements *) + (*******************************************************) + + type bcinfo_query = + | CurBlockNum + | ChainID + | Timestamp of ER.rep id_ann + | ReplicateContr of (ER.rep id_ann * ER.rep id_ann) + [@@deriving sexp] + + type stmt_annot = stmt * SR.rep * annot_comment + + and stmt = + | Load of ER.rep id_ann * ER.rep id_ann + | RemoteLoad of ER.rep id_ann * ER.rep id_ann * ER.rep id_ann + | Store of ER.rep id_ann * ER.rep id_ann + | Bind of ER.rep id_ann * expr_annot + | MapUpdate of ER.rep id_ann * ER.rep id_ann list * ER.rep id_ann option + | MapGet of ER.rep id_ann * ER.rep id_ann * ER.rep id_ann list * bool + | RemoteMapGet of + ER.rep id_ann + * ER.rep id_ann + * ER.rep id_ann + * ER.rep id_ann list + * bool + | MatchStmt of + ER.rep id_ann * (pattern * stmt_annot list * comment_text list) list + | ReadFromBC of ER.rep id_ann * bcinfo_query + | TypeCast of ER.rep id_ann * ER.rep id_ann * SType.t + | AcceptPayment (** [AcceptPayment] is an [accept] statement. *) + | Iterate of ER.rep id_ann * SR.rep id_ann + | SendMsgs of ER.rep id_ann + | CreateEvnt of ER.rep id_ann + | CallProc of SR.rep id_ann * ER.rep id_ann list + | Throw of ER.rep id_ann option + | GasStmt of SGasCharge.gas_charge + [@@deriving sexp] + + (*******************************************************) + (* Contracts *) + (*******************************************************) + + type component = { + comp_comments : string list; + comp_type : Syntax.component_type; + comp_name : SR.rep id_ann; + comp_params : (ER.rep id_ann * SType.t) list; + comp_body : stmt_annot list; + } + [@@deriving sexp] + + type ctr_def = { + cname : ER.rep id_ann; + c_comments : comment_text list; + c_arg_types : SType.t list; + } + [@@deriving sexp] + + type lib_entry = + | LibVar of comment_text list * ER.rep id_ann * SType.t option * expr_annot + | LibTyp of comment_text list * ER.rep id_ann * ctr_def list + [@@deriving sexp] + + type library = { lname : SR.rep id_ann; lentries : lib_entry list } + [@@deriving sexp] + + type contract = { + cname : SR.rep id_ann; + cparams : (ER.rep id_ann * SType.t) list; + cconstraint : expr_annot; + cfields : (comment_text list * ER.rep id_ann * SType.t * expr_annot) list; + ccomps : component list; + } + [@@deriving sexp] + + type cmodule = { + smver : int; + file_comments : comment_text list; + lib_comments : comment_text list; + libs : library option; + elibs : (SR.rep id_ann * SR.rep id_ann option) list; + contr_comments : comment_text list; + contr : contract; + } + [@@deriving sexp] + (** The structure of the extended [cmodule] is: + scilla_version 0 + + (* File comment *) + + import X + + (* Library comment *) + library ExampleLib + + (* Contract comment *) + contract ExampleContr() + *) + + (* Library module *) + type lmodule = { + smver : int; + (* Scilla major version of the library. *) + (* List of imports / external libs with an optional namespace. *) + elibs : (SR.rep id_ann * SR.rep id_ann option) list; + libs : library; (* lib functions defined in the module *) + } + [@@deriving sexp] + + (* A tree of libraries linked to their dependents *) + type libtree = { + libn : library; + (* The library this node represents *) + deps : libtree list; (* List of dependent libraries *) + } +end + +module ExtendedScillaSyntaxTransformer + (SR : Syntax.Rep) + (ER : Syntax.Rep) + (Lit : Literal.ScillaLiteral) = +struct + module Syn = Syntax.ScillaSyntax (SR) (ER) (Lit) + module ExtSyn = ExtendedScillaSyntax (SR) (ER) (Lit) + module SType = Lit.LType + module SIdentifier = SType.TIdentifier + + type t = { mutable comments : (loc * ExtSyn.comment_text) list } + + let mk comments = + (* Comments are already sorted by line number and column, because the lexer + works by this way. *) + { comments } + + (****************************************************************************) + (* Utility functions *) + (****************************************************************************) + + let nth_comment tr = List.nth tr.comments + let first_comment tr = List.hd tr.comments + let second_comment tr = nth_comment tr 1 + + (** Removes the top comment from the given transformer. *) + let pop_comment tr = + if not @@ List.is_empty tr.comments then + tr.comments <- List.tl_exn tr.comments + + (** Returns true if [comment_loc] is located above the library definition: + (* Library comment *) + library Something + *) + let is_comment_above_lib (cmod : Syn.cmodule) comment_loc = + match cmod.libs with + | None -> false + | Some lib -> + let lib_loc = SR.get_loc (SIdentifier.get_rep lib.lname) in + comment_loc.lnum < lib_loc.lnum + + (** Returns true if [comment_loc] is a file comment located above the + contract definition : + (* Contract comment *) + contract Something() + *) + let is_comment_above_contract (cmod : Syn.cmodule) comment_loc = + let contr_loc = SR.get_loc (SIdentifier.get_rep cmod.contr.cname) in + contr_loc.lnum > comment_loc.lnum + + (****************************************************************************) + (* Collect functions *) + (* *) + (* Collect functions collect comments for the required positions and remove *) + (* them from the Transformer's mutable state. *) + (****************************************************************************) + + (** Collects comment annotations that must be placed between [loc_start] and + [loc_end] and removes them from the [tr.comments] list. *) + let collect_comments tr loc_start loc_end = + let rec aux acc = function + (* Placing comments left *) + | (loc, s) :: xs + when (* (* com *) start end *) + phys_equal loc.lnum loc_start.lnum && loc.cnum < loc_start.cnum -> + pop_comment tr; + aux ((loc, s, ExtSyn.ComLeft) :: acc) xs + (* Placing comments above *) + | (loc, s) :: xs + when (* (* com *) (* com *) + start end start + end *) + loc.lnum < loc_start.lnum + || (* (* com *) start end (* com *) start + end *) + (loc.lnum <= loc_start.lnum && loc.cnum < loc_start.cnum) -> + pop_comment tr; + aux ((loc, s, ExtSyn.ComAbove) :: acc) xs + (* Placing comments right *) + | (loc, s) :: xs + when (* start (* com *) + end *) + phys_equal loc.lnum loc_start.lnum + && loc.lnum > loc_end.lnum && loc.cnum > loc_start.cnum + || (* start (* com *) end *) + phys_equal loc.lnum loc_start.lnum + && phys_equal loc.lnum loc_end.lnum + && loc.cnum > loc_start.cnum && loc.cnum < loc_end.cnum -> + pop_comment tr; + aux ((loc, s, ExtSyn.ComRight) :: acc) xs + | _ -> acc + in + if ErrorUtils.compare_loc loc_start loc_end > 0 then [] + else aux [] tr.comments + + (** A wrapper for [collect_comments] that returns only texts of comments, + without location information. *) + let collect_comment_texts tr loc_start loc_end = + collect_comments tr loc_start loc_end + |> List.map ~f:(fun (_, text, _) -> text) + + (** Collects a list of comments placed above [loc]. *) + let collect_comments_above tr loc = + let rec aux acc = + match List.hd tr.comments with + | Some (comment_loc, comment) when loc.lnum > comment_loc.lnum -> + pop_comment tr; + aux (acc @ [ comment ]) + | _ -> acc + in + aux [] + + (** Collects a list of comments placed on the right of [loc]. *) + let collect_comments_right tr loc = + let rec aux acc = + match List.hd tr.comments with + | Some (comment_loc, comment) + when phys_equal loc.lnum comment_loc.lnum && loc.cnum < comment_loc.cnum + -> + pop_comment tr; + aux (acc @ [ comment ]) + | _ -> acc + in + aux [] + + (* Collects file comments located on the top of the contract module. *) + let collect_file_comments tr (cmod : Syn.cmodule) = + (* Utility function that collects file comments before library or contract + definition when we don't have imports. *) + let get_file_comments f = + let rec aux idx acc = + let result all = + (* [all] contains all the comments above the library/contract + definition. We have to find a group of comments that are separated + with at least a single newline with the comments above + library/contract. If we have multiple comments above the + library/contract comments, they will be considered as a part of + the file comment: + (* file comment1 *) + (* file comment2 *) + + (* file comment3 *) + + (* library comment1 *) + (* library comment2 *) + library Something + *) + let rec first_comment_idx acc idx = + match acc with + | (c1_loc, _) :: (c2_loc, c2) :: cs -> + if c1_loc.lnum > c2_loc.lnum + 1 then Some (idx + 1) + else first_comment_idx ((c2_loc, c2) :: cs) (idx + 1) + | _ -> None + in + let rev_all = List.rev all in + match first_comment_idx rev_all 0 with + | Some idx when (not @@ phys_equal idx 0) && idx < List.length acc -> + List.sub rev_all ~pos:idx ~len:(List.length acc - idx) + |> List.rev + |> List.map ~f:(fun (_loc, c) -> + pop_comment tr; + c) + | _ -> [] + in + match nth_comment tr idx with + | Some (comment1_loc, comment1) -> + if not @@ f cmod comment1_loc then result acc + else aux (idx + 1) (acc @ [ (comment1_loc, comment1) ]) + | _ -> result acc + in + aux 0 [] + in + let has_imports = not @@ List.is_empty cmod.elibs in + let has_library = Option.is_some cmod.libs in + if has_imports then + (* If we have imports then the file comment can be located only above them: + scilla_version 0 + (* File comment *) + import BoolUtils + *) + let first_import_loc = + List.hd_exn cmod.elibs |> fun (id, _) -> + SR.get_loc (SIdentifier.get_rep id) + in + collect_comments_above tr first_import_loc + else if has_library then + (* If we don't have import statements, the file comment may be located + above the library comment. In this case, it must be separated with + the library comment with at least one newline: + scilla_version 0 + (* File comment *) + + (* Library comment *) + library Something + *) + get_file_comments is_comment_above_lib + else + (* If we don't have import statements and library definition, the file + comment may be located above the contract comment: + scilla_version 0 + (* File comment *) + + (* Contract comment *) + contract Something + *) + get_file_comments is_comment_above_contract + + (** Collects library comments that are located above the library definition. *) + let collect_lib_comments tr (cmod : Syn.cmodule) = + let has_library = Option.is_some cmod.libs in + let rec aux acc = + match first_comment tr with + | Some (comment_loc, comment) + when has_library && is_comment_above_lib cmod comment_loc -> + pop_comment tr; + aux (acc @ [ comment ]) + | _ -> acc + in + aux [] + + (** Collects contract comment which is a comment located above the contract definition. *) + let collect_contr_comments tr (cmod : Syn.cmodule) = + let rec aux acc = + match first_comment tr with + | Some (comment_loc, comment) + when is_comment_above_contract cmod comment_loc -> + pop_comment tr; + aux (acc @ [ comment ]) + | _ -> acc + in + aux [] + + (****************************************************************************) + (* Extend functions *) + (* *) + (* Extend functions extend AST with annotations. *) + (****************************************************************************) + + let extend_id ?(rep_end = None) tr id get_loc = + let id_loc = get_loc (SIdentifier.get_rep id) in + let end_loc = + Option.value_map rep_end ~default:id_loc ~f:(fun rep -> get_loc rep) + in + let comments = collect_comments tr id_loc end_loc in + (id, comments) + + let extend_er_id ?(rep_end = None) tr id = extend_id tr id ~rep_end ER.get_loc + let extend_sr_id ?(rep_end = None) tr id = extend_id tr id ~rep_end SR.get_loc + + let extend_payload tr = function + | Syn.MLit l -> ExtSyn.MLit l + | Syn.MVar v -> ExtSyn.MVar (extend_er_id tr v) + + (** Extends the given pattern. + [body_loc] is a start position of the body of this arm. *) + let rec extend_pattern ?(body_loc = None) tr pat = + let get_arm_comments pat_loc = + Option.value_map body_loc + ~f:(fun body_loc -> collect_comment_texts tr pat_loc body_loc) + ~default:(collect_comments_right tr pat_loc) + in + match pat with + | Syn.Wildcard -> + let arm_comments = [] (* TODO: What is the start location here? *) in + (ExtSyn.Wildcard, arm_comments) + | Syn.Binder id -> + let id' = extend_er_id tr id in + let id_loc = ER.get_loc (SIdentifier.get_rep id) in + let arm_comments = get_arm_comments id_loc in + (ExtSyn.Binder id', arm_comments) + | Syn.Constructor (id, args) -> + let id' = extend_sr_id tr id in + let id_loc = SR.get_loc (SIdentifier.get_rep id) in + let args' = + List.map args ~f:(fun arg -> + extend_pattern tr arg |> fun (pat', _) -> pat') + in + let arm_comments = get_arm_comments id_loc in + (ExtSyn.Constructor (id', args'), arm_comments) + + let rec extend_expr tr (e, ann) = + let comment ?(rep_end = ann) () = + collect_comments tr (ER.get_loc ann) (ER.get_loc rep_end) + in + match e with + | Syn.Literal l -> (ExtSyn.Literal l, ann, comment ()) + | Syn.Var id -> + let c = comment () in + let id' = extend_er_id tr id in + (ExtSyn.Var id', ann, c) + | Syn.Let (id, ty, (lhs, lhs_rep), rhs) -> + let c = comment () ~rep_end:(SIdentifier.get_rep id) in + let id' = extend_er_id tr id ~rep_end:(Some lhs_rep) in + let lhs' = extend_expr tr (lhs, lhs_rep) in + let rhs' = extend_expr tr rhs in + (ExtSyn.Let (id', ty, lhs', rhs'), ann, c) + | Syn.Message msgs -> + let c = comment () in + let msgs' = + List.map msgs ~f:(fun (s, pld) -> (s, extend_payload tr pld)) + in + (ExtSyn.Message msgs', ann, c) + | Syn.Fun (id, ty, (body, body_loc)) -> + let c = comment ~rep_end:(SIdentifier.get_rep id) () in + let id' = extend_er_id tr id ~rep_end:(Some body_loc) in + let body' = extend_expr tr (body, body_loc) in + (ExtSyn.Fun (id', ty, body'), ann, c) + | Syn.App (id, args) -> + let c = comment () in + let id' = extend_er_id tr id in + let args' = List.map args ~f:(fun arg -> extend_er_id tr arg) in + (ExtSyn.App (id', args'), ann, c) + | Syn.Constr (id, tys, args) -> + let c = comment () in + let id' = extend_sr_id tr id in + let args' = List.map args ~f:(fun arg -> extend_er_id tr arg) in + (ExtSyn.Constr (id', tys, args'), ann, c) + | Syn.MatchExpr (id, arms) -> + let c = comment () in + let id' = extend_er_id tr id in + let arms' = + List.map arms ~f:(fun (pat, (body, body_rep)) -> + let pat', arm_comments = + let body_loc = Some (ER.get_loc body_rep) in + extend_pattern ~body_loc tr pat + in + let body' = extend_expr tr (body, body_rep) in + (pat', body', arm_comments)) + in + (ExtSyn.MatchExpr (id', arms'), ann, c) + | Syn.Builtin (builtin, ty, args) -> + let c = comment () in + let args' = List.map args ~f:(fun arg -> extend_er_id tr arg) in + (ExtSyn.Builtin (builtin, ty, args'), ann, c) + | Syn.TFun (id, (body, body_loc)) -> + let c = comment ~rep_end:body_loc () in + let id' = extend_er_id tr id in + let body' = extend_expr tr (body, body_loc) in + (ExtSyn.TFun (id', body'), ann, c) + | Syn.TApp (id, tys) -> + let c = comment () in + let id' = extend_er_id tr id in + (ExtSyn.TApp (id', tys), ann, c) + | Syn.Fixpoint (id, ty, (body, body_loc)) -> + let c = comment ~rep_end:body_loc () in + let id' = extend_er_id tr id in + let body' = extend_expr tr (body, body_loc) in + (ExtSyn.Fixpoint (id', ty, body'), ann, c) + | Syn.GasExpr (gc, (body, body_loc)) -> + let c = comment ~rep_end:body_loc () in + let body' = extend_expr tr (body, body_loc) in + let gc' = + Syn.SGasCharge.sexp_of_gas_charge gc + |> ExtSyn.SGasCharge.gas_charge_of_sexp + in + (ExtSyn.GasExpr (gc', body'), ann, c) + + let extend_bcinfo_query tr = function + | Syn.CurBlockNum -> ExtSyn.CurBlockNum + | Syn.ChainID -> ExtSyn.ChainID + | Syn.Timestamp id -> ExtSyn.Timestamp (extend_er_id tr id) + | Syn.ReplicateContr (addr, param) -> + let addr' = extend_er_id tr addr in + let param' = extend_er_id tr param in + ExtSyn.ReplicateContr (addr', param') + + let rec extend_stmt tr (s, ann) = + let comment loc_end = collect_comments tr (SR.get_loc ann) loc_end in + let loc_end_er id = SIdentifier.get_rep id |> ER.get_loc in + let loc_end_sr id = SIdentifier.get_rep id |> SR.get_loc in + match s with + | Syn.Load (lhs, rhs) -> + let c = comment (loc_end_er lhs) in + let lhs' = extend_er_id tr lhs in + let rhs' = extend_er_id tr rhs in + (ExtSyn.Load (lhs', rhs'), ann, c) + | Syn.RemoteLoad (lhs, addr, rhs) -> + let c = comment (loc_end_er lhs) in + let lhs' = + extend_er_id tr lhs ~rep_end:(Some (SIdentifier.get_rep addr)) + in + let addr' = + extend_er_id tr addr ~rep_end:(Some (SIdentifier.get_rep rhs)) + in + let rhs' = extend_er_id tr rhs in + (ExtSyn.RemoteLoad (lhs', addr', rhs'), ann, c) + | Syn.Store (lhs, rhs) -> + let c = comment (loc_end_er lhs) in + let lhs' = extend_er_id tr lhs in + let rhs' = extend_er_id tr rhs in + (ExtSyn.Store (lhs', rhs'), ann, c) + | Syn.Bind (id, body) -> + let c = comment (loc_end_er id) in + let id' = extend_er_id tr id in + let ea' = extend_expr tr body in + (ExtSyn.Bind (id', ea'), ann, c) + | Syn.MapUpdate (m, keys, v) -> + let c = comment (loc_end_er m) in + let m' = extend_er_id tr m in + let keys' = List.map keys ~f:(fun k -> extend_er_id tr k) in + let v' = + Option.value_map v ~default:None ~f:(fun v -> + Some (extend_er_id tr v)) + in + (ExtSyn.MapUpdate (m', keys', v'), ann, c) + | Syn.MapGet (v, m, keys, retrieve) -> + let c = comment (loc_end_er v) in + let v' = extend_er_id tr v in + let m' = extend_er_id tr m in + let keys' = List.map keys ~f:(fun k -> extend_er_id tr k) in + (ExtSyn.MapGet (v', m', keys', retrieve), ann, c) + | Syn.RemoteMapGet (v, addr, m, keys, retrieve) -> + let c = comment (loc_end_er v) in + let v' = extend_er_id tr v in + let addr' = extend_er_id tr addr in + let m' = extend_er_id tr m in + let keys' = List.map keys ~f:(fun k -> extend_er_id tr k) in + (ExtSyn.RemoteMapGet (v', addr', m', keys', retrieve), ann, c) + | Syn.MatchStmt (id, arms) -> + let c = comment (loc_end_er id) in + let id' = extend_er_id tr id in + let arms' = + List.map arms ~f:(fun (pat, stmts) -> + let body_loc = + List.hd stmts + |> Option.value_map + ~f:(fun (_, rep) -> Some (SR.get_loc rep)) + ~default:None + in + let pat', arm_comments = extend_pattern ~body_loc tr pat in + let stmts' = + List.map stmts ~f:(fun stmt -> extend_stmt tr stmt) + in + (pat', stmts', arm_comments)) + in + (ExtSyn.MatchStmt (id', arms'), ann, c) + | Syn.ReadFromBC (id, q) -> + let c = comment (loc_end_er id) in + let id' = extend_er_id tr id in + let q' = extend_bcinfo_query tr q in + (ExtSyn.ReadFromBC (id', q'), ann, c) + | Syn.TypeCast (id, addr, ty) -> + let c = comment (loc_end_er id) in + let id' = extend_er_id tr id in + let addr' = extend_er_id tr addr in + (ExtSyn.TypeCast (id', addr', ty), ann, c) + | Syn.AcceptPayment -> + let c = comment (SR.get_loc ann) in + (ExtSyn.AcceptPayment, ann, c) + | Syn.Iterate (l, f) -> + let c = comment (loc_end_er l) in + let l' = extend_er_id tr l in + let f' = extend_sr_id tr f in + (ExtSyn.Iterate (l', f'), ann, c) + | Syn.SendMsgs id -> + let c = comment (loc_end_er id) in + let id' = extend_er_id tr id in + (ExtSyn.SendMsgs id', ann, c) + | Syn.CreateEvnt id -> + let c = comment (loc_end_er id) in + let id' = extend_er_id tr id in + (ExtSyn.CreateEvnt id', ann, c) + | Syn.CallProc (id, args) -> + let c = comment (loc_end_sr id) in + let id' = extend_sr_id tr id in + let args' = List.map args ~f:(fun arg -> extend_er_id tr arg) in + (ExtSyn.CallProc (id', args'), ann, c) + | Syn.Throw id_opt -> ( + match id_opt with + | Some id -> + let c = comment (loc_end_er id) in + let id' = extend_er_id tr id in + (ExtSyn.Throw (Some id'), ann, c) + | None -> + let c = comment (SR.get_loc ann) in + (ExtSyn.Throw None, ann, c)) + | Syn.GasStmt gc -> + let c = comment (SR.get_loc ann) in + let gc' = + Syn.SGasCharge.sexp_of_gas_charge gc + |> ExtSyn.SGasCharge.gas_charge_of_sexp + in + (ExtSyn.GasStmt gc', ann, c) + + let extend_ctr_def tr (ctr : Syn.ctr_def) = + let cname_loc = ER.get_loc (SIdentifier.get_rep ctr.cname) in + let c_comments = collect_comments_right tr cname_loc in + let cname' = extend_er_id tr ctr.cname in + { ExtSyn.cname = cname'; c_comments; c_arg_types = ctr.c_arg_types } + + let extend_lentry tr = function + | Syn.LibVar (id, ty_opt, ea) -> + let id_loc = ER.get_loc (SIdentifier.get_rep id) in + let comments = + collect_comments_above tr id_loc @ collect_comments_right tr id_loc + in + let id' = extend_er_id tr id in + let ea' = extend_expr tr ea in + ExtSyn.LibVar (comments, id', ty_opt, ea') + | Syn.LibTyp (id, ctrs) -> + let id_loc = ER.get_loc (SIdentifier.get_rep id) in + let comments = + collect_comments_above tr id_loc @ collect_comments_right tr id_loc + in + let id' = extend_er_id tr id in + let ctrs' = List.map ctrs ~f:(fun ctr -> extend_ctr_def tr ctr) in + ExtSyn.LibTyp (comments, id', ctrs') + + let extend_lib tr (lib : Syn.library) = + let lname' = extend_sr_id tr lib.lname in + let lentries' = + List.map lib.lentries ~f:(fun lentry -> extend_lentry tr lentry) + in + { ExtSyn.lname = lname'; lentries = lentries' } + + let extend_elib tr elib = + let import, import_as = elib in + let import' = extend_sr_id tr import in + let import_as' = + Option.value_map import_as ~default:None ~f:(fun id -> + Some (extend_sr_id tr id)) + in + (import', import_as') + + let extend_component tr comp = + let comp_comments = + let comp_name_loc = SR.get_loc (SIdentifier.get_rep comp.Syn.comp_name) in + collect_comments_above tr comp_name_loc + in + let comp_type = comp.Syn.comp_type in + let comp_name = extend_sr_id tr comp.comp_name in + let comp_params = + List.map comp.comp_params ~f:(fun (id, ty) -> (extend_er_id tr id, ty)) + in + let comp_body = + List.map comp.comp_body ~f:(fun stmt -> extend_stmt tr stmt) + in + { comp_comments; ExtSyn.comp_type; comp_name; comp_params; comp_body } + + let extend_contract tr (contr : Syn.contract) : ExtSyn.contract = + let cname = extend_sr_id tr contr.cname in + let cparams = + List.map contr.cparams ~f:(fun (id, ty) -> (extend_er_id tr id, ty)) + in + let cconstraint = extend_expr tr contr.cconstraint in + let cfields = + List.map contr.cfields ~f:(fun (id, ty, init) -> + let id_loc = ER.get_loc (SIdentifier.get_rep id) in + let comments = collect_comments_above tr id_loc in + let id' = extend_er_id tr id in + let init' = extend_expr tr init in + (comments, id', ty, init')) + in + let ccomps = List.map contr.ccomps ~f:(fun c -> extend_component tr c) in + { cname; cparams; cconstraint; cfields; ccomps } + + let extend_cmodule tr (cmod : Syn.cmodule) : ExtSyn.cmodule = + let smver = cmod.smver in + let file_comments = collect_file_comments tr cmod in + let elibs = List.map cmod.elibs ~f:(fun l -> extend_elib tr l) in + let lib_comments = collect_lib_comments tr cmod in + let libs = + Option.value_map cmod.libs ~default:None ~f:(fun l -> + Some (extend_lib tr l)) + in + let contr_comments = collect_contr_comments tr cmod in + let contr = extend_contract tr cmod.contr in + { smver; file_comments; lib_comments; libs; elibs; contr_comments; contr } +end + +module LocalLiteralTransformer = + ExtendedScillaSyntaxTransformer (ParserUtil.ParserRep) (ParserUtil.ParserRep) + (Literal.LocalLiteral) diff --git a/src/base/Formatter.ml b/src/formatter/Formatter.ml similarity index 71% rename from src/base/Formatter.ml rename to src/formatter/Formatter.ml index 789526748..12865e1ba 100644 --- a/src/base/Formatter.ml +++ b/src/formatter/Formatter.ml @@ -18,6 +18,7 @@ (** Scilla code formatter *) +open Scilla_base open Base open PPrint @@ -26,8 +27,8 @@ open PPrint module Format (SR : Syntax.Rep) (ER : Syntax.Rep) (Lit : Literal.ScillaLiteral) = struct - (* instantiated syntax *) - module Ast = Syntax.ScillaSyntax (SR) (ER) (Lit) + (* instantiated syntax extended with comments *) + module Ast = ExtendedSyntax.ExtendedScillaSyntax (SR) (ER) (Lit) module type DOC = sig val of_type : Ast.SType.t -> PPrint.document @@ -91,12 +92,51 @@ struct (* Add parentheses only if the condition if true *) let parens_if cond doc = if cond then parens doc else doc + (* Wrap document in comment symbols *) + let comment = enclose !^"(*" !^"*)" + + (* Concatenate multiple comments to a single comment. *) + let concat_comments ?(sep=hardline) cs = + List.fold_left cs ~init:[] ~f:(fun acc c -> acc @ [comment !^c]) + |> concat_map (fun c -> c ^^^ sep) + + (** Add formatted [comments] around [doc]. *) + let wrap_comments comments doc = + let spaced s = + let has_prefix prefix = String.is_prefix s ~prefix in + let has_suffix suffix = String.is_suffix s ~suffix in + let s = if has_prefix " " || has_prefix "*" then s else " " ^ s in + let s = if has_suffix " " || has_suffix "*" then s else s ^ " " in + s + in + let left, above, right = + List.fold_left comments + ~init:([],[],[]) + ~f:(fun (acc_l, acc_a, acc_r) -> function + | (_, s, Ast.ComLeft) -> + acc_l @ [comment !^(spaced s); space], acc_a, acc_r + | (_, s, Ast.ComAbove) -> + acc_l, (comment !^(spaced s))::acc_a, acc_r + | (_, s, Ast.ComRight) -> + acc_l, acc_a, [space; comment !^(spaced s)] @ acc_r) + |> fun (l, a, r) -> + let a' = if List.is_empty a then empty + else (concat_map (fun c -> c ^^^ hardline) a) + in + let l' = concat l in + let r' = concat r in + l', a', r' + in + concat [above; left; doc; right] + let of_builtin b = !^(Syntax.pp_builtin b) let of_id id = !^(Ast.SIdentifier.as_error_string id) - let of_ids ids = - separate_map space of_id ids + let of_ann_id (id, comments) = of_id id |> wrap_comments comments + + let of_ann_ids ids = + separate_map space of_ann_id ids let rec of_type_with_prec p typ = let open Ast.SType in @@ -149,7 +189,7 @@ struct let of_types typs ~sep = group @@ separate_map sep (fun ty -> of_type_with_prec 1 ty) typs - let of_typed_id id typ = of_id id ^^^ colon ^//^ group (of_type typ) + let of_typed_ann_id id typ = of_ann_id id ^^^ colon ^//^ group (of_type typ) let rec of_literal lit = let rec walk p = function @@ -201,14 +241,14 @@ struct let of_payload = function | Ast.MLit lit -> of_literal lit - | Ast.MVar id -> of_id id + | Ast.MVar id -> of_ann_id id let of_pattern pat = let rec of_pattern_aux ~top_parens = function | Ast.Wildcard -> !^"_" - | Ast.Binder id -> of_id id + | Ast.Binder id -> of_ann_id id | Ast.Constructor (constr_id, pats) -> - let constr_id = of_id constr_id in + let constr_id = of_ann_id constr_id in if List.is_empty pats then constr_id else @@ -217,10 +257,10 @@ struct in of_pattern_aux ~top_parens:false pat - let rec of_expr (expr, _ann) = - match expr with + let rec of_expr (expr, _ann, comments) = + (match expr with | Ast.Literal lit -> of_literal lit - | Ast.Var id -> of_id id + | Ast.Var id -> of_ann_id id | Ast.Fun (id, typ, body) -> (* TODO: nested functions should not be indented: fun (a : String) => @@ -232,20 +272,20 @@ struct let body = of_expr body in (* fun ($id : $typ) => $body *) - fun_kwd ^^^ parens (of_typed_id id typ) ^^^ darrow ^^ indent (hardline ^^ body) + fun_kwd ^^^ parens (of_typed_ann_id id typ) ^^^ darrow ^^ indent (hardline ^^ body) | Ast.App (fid, args) -> - let fid = of_id fid - and args = of_ids args in + let fid = of_ann_id fid + and args = of_ann_ids args in fid ^//^ args | Ast.Builtin ((builtin, _ann), _types, typed_ids) -> let builtin = of_builtin builtin - and args = of_ids typed_ids in + and args = of_ann_ids typed_ids in builtin_kwd ^^^ builtin ^//^ args | Ast.Let (id, otyp, lhs, body) -> let id = match otyp with - | None -> of_id id - | Some typ -> of_typed_id id typ + | None -> of_ann_id id + | Some typ -> of_typed_ann_id id typ and lhs = of_expr lhs and body = of_expr body in (* @@ -270,27 +310,36 @@ struct *) (group (group (let_kwd ^^^ id ^^^ equals ^//^ lhs) ^/^ in_kwd)) ^/^ body | Ast.TFun (ty_var, body) -> - let ty_var = of_id ty_var + let ty_var = of_ann_id ty_var and body = of_expr body in (* tfun $ty_var => $body *) (* (^/^) -- means concat with _breakable_ space *) tfun_kwd ^^^ ty_var ^^^ darrow ^//^ body | Ast.TApp (id, typs) -> - let tfid = of_id id + let tfid = of_ann_id id (* TODO: remove unnecessary parens around primitive types: e.g. "Nat" does not need parens but "forall 'X. 'X" needs them in type applications *) and typs = separate_map space (fun typ -> parens @@ of_type typ) typs in at ^^ tfid ^//^ typs | Ast.MatchExpr (ident, branches) -> - match_kwd ^^^ of_id ident ^^^ with_kwd ^/^ + match_kwd ^^^ of_ann_id ident ^^^ with_kwd ^/^ separate_map hardline - (fun (pat, e) -> group (pipe ^^^ of_pattern pat ^^^ darrow ^//^ group (of_expr e))) + (fun (pat, e, cs) -> + let doc = + pipe ^^^ of_pattern pat ^^^ darrow + in + let doc = if not @@ List.is_empty cs then + doc ^^^ concat_comments ~sep:space cs + else doc + in + let doc = doc ^//^ group (of_expr e) in + group (doc)) branches ^^ hardline ^^ end_kwd | Ast.Constr (id, typs, args) -> - let id = of_id id + let id = of_ann_id id (* TODO: remove unnecessary parens around primitive types *) - and args_doc = of_ids args in + and args_doc = of_ann_ids args in if Base.List.is_empty typs then if Base.List.is_empty args then id else id ^//^ args_doc else @@ -309,46 +358,55 @@ struct rbrace | Fixpoint _ -> failwith "Fixpoints cannot appear in user contracts" | GasExpr _ -> failwith "Gas annotations cannot appear in user contracts's expressions" + ) |> wrap_comments comments let of_map_access map keys = - let map = of_id map - and keys = concat_map (fun k -> brackets @@ of_id k) keys in + let map = of_ann_id map + and keys = concat_map (fun k -> brackets @@ of_ann_id k) keys in map ^^ keys - let rec of_stmt (stmt, _ann) = match stmt with + let rec of_stmt (stmt, _ann, comments) = + (match stmt with | Ast.Load (id, field) -> - of_id id ^^^ rev_arrow ^//^ of_id field + of_ann_id id ^^^ rev_arrow ^//^ of_ann_id field | Ast.RemoteLoad (id, addr, field) -> - of_id id ^^^ blockchain_arrow ^//^ of_id addr ^^ dot ^^ of_id field + of_ann_id id ^^^ blockchain_arrow ^//^ of_ann_id addr ^^ dot ^^ of_ann_id field | Ast.Store (field, id) -> - of_id field ^^^ assign ^//^ of_id id + of_ann_id field ^^^ assign ^//^ of_ann_id id | Ast.Bind (id, expr) -> - of_id id ^^^ equals ^//^ of_expr expr + of_ann_id id ^^^ equals ^//^ of_expr expr | Ast.MapUpdate (map, keys, mode) -> (* m[k1][k2][..] := v OR delete m[k1][k2][...] *) (match mode with - | Some value -> of_map_access map keys ^^^ assign ^//^ of_id value + | Some value -> of_map_access map keys ^^^ assign ^//^ of_ann_id value | None -> delete_kwd ^^^ of_map_access map keys) | Ast.MapGet (id, map, keys, mode) -> (* v <- m[k1][k2][...] OR b <- exists m[k1][k2][...] *) (* If the bool is set, then we interpret this as value retrieve, otherwise as an "exists" query. *) if mode then - of_id id ^^^ rev_arrow ^//^ of_map_access map keys + of_ann_id id ^^^ rev_arrow ^//^ of_map_access map keys else - of_id id ^^^ rev_arrow ^//^ exists_kwd ^^^ of_map_access map keys + of_ann_id id ^^^ rev_arrow ^//^ exists_kwd ^^^ of_map_access map keys | Ast.RemoteMapGet (id, addr, map, keys, mode) -> (* v <-& adr.m[k1][k2][...] OR b <-& exists adr.m[k1][k2][...] *) (* If the bool is set, then we interpret this as value retrieve, otherwise as an "exists" query. *) if mode then - of_id id ^^^ blockchain_arrow ^//^ of_id addr ^^ dot ^^ of_map_access map keys + of_ann_id id ^^^ blockchain_arrow ^//^ of_ann_id addr ^^ dot ^^ of_map_access map keys else - of_id id ^^^ blockchain_arrow ^//^ exists_kwd ^^^ of_id addr ^^ dot ^^ of_map_access map keys + of_ann_id id ^^^ blockchain_arrow ^//^ exists_kwd ^^^ of_ann_id addr ^^ dot ^^ of_map_access map keys | Ast.MatchStmt (id, branches) -> - match_kwd ^^^ of_id id ^^^ with_kwd ^/^ + match_kwd ^^^ of_ann_id id ^^^ with_kwd ^/^ separate_map hardline - (fun (pat, stmts) -> group (pipe ^^^ of_pattern pat ^^^ darrow ^//^ group (of_stmts stmts))) + (fun (pat, stmts, cs) -> + let doc = pipe ^^^ of_pattern pat ^^^ darrow in + let doc = if not @@ List.is_empty cs then + doc ^^^ concat_comments ~sep:space cs + else doc + in + let doc = doc ^//^ group (of_stmts stmts) in + group (doc)) branches ^^ hardline ^^ end_kwd | Ast.ReadFromBC (id, query) -> @@ -356,30 +414,31 @@ struct match query with | CurBlockNum -> blocknumber_kwd | ChainID -> chainid_kwd - | Timestamp ts -> timestamp_kwd ^^ parens (of_id ts) + | Timestamp ts -> timestamp_kwd ^^ parens (of_ann_id ts) | ReplicateContr (addr, init_params) -> - replicate_contract_kwd ^^ parens (of_id addr ^^ comma ^^^ of_id init_params) + replicate_contract_kwd ^^ parens (of_ann_id addr ^^ comma ^^^ of_ann_id init_params) in - of_id id ^^^ blockchain_arrow ^//^ query + of_ann_id id ^^^ blockchain_arrow ^//^ query | Ast.TypeCast (id, addr, typ) -> - of_id id ^^^ blockchain_arrow ^//^ of_id addr ^^^ as_kwd ^^^ of_type typ + of_ann_id id ^^^ blockchain_arrow ^//^ of_ann_id addr ^^^ as_kwd ^^^ of_type typ | Ast.AcceptPayment -> accept_kwd | Ast.Iterate (arg_list, proc) -> (* forall l p *) - forall_kwd ^//^ of_id arg_list ^//^ of_id proc + forall_kwd ^//^ of_ann_id arg_list ^//^ of_ann_id proc | Ast.SendMsgs msgs -> - send_kwd ^//^ of_id msgs + send_kwd ^//^ of_ann_id msgs | Ast.CreateEvnt events -> - event_kwd ^//^ of_id events + event_kwd ^//^ of_ann_id events | Ast.CallProc (proc, args) -> - if List.is_empty args then of_id proc - else of_id proc ^//^ of_ids args + if List.is_empty args then of_ann_id proc + else of_ann_id proc ^//^ of_ann_ids args | Ast.Throw oexc -> (match oexc with | None -> throw_kwd - | Some exc -> throw_kwd ^//^ of_id exc) + | Some exc -> throw_kwd ^//^ of_ann_id exc) | Ast.GasStmt _ -> failwith "Gas annotations cannot appear in user contracts's statements" + ) |> wrap_comments comments and of_stmts stmts = separate_map (semi ^^ hardline) (fun s -> of_stmt s) stmts @@ -390,48 +449,54 @@ struct lparen (separate_map (comma ^^ sep) - (fun (p, typ) -> of_typed_id p typ) + (fun (p, typ) -> of_typed_ann_id p typ) typed_params) rparen - let of_component Ast.{comp_type; comp_name; comp_params; comp_body} = + let of_component Ast.{comp_comments; comp_type; comp_name; comp_params; comp_body} = let comp_type = !^(Syntax.component_type_to_string comp_type) - and comp_name = of_id comp_name + and comp_name = of_ann_id comp_name and comp_params = of_parameters comp_params ~sep:(break 1) and comp_body = of_stmts comp_body in + concat_comments comp_comments ^^ group (comp_type ^^^ comp_name ^//^ comp_params) ^^ indent (hardline ^^ comp_body) ^^ hardline ^^ end_kwd - let of_ctr_def Ast.{cname; c_arg_types} = - let constructor_name = of_id cname + let of_ctr_def Ast.{cname; c_comments; c_arg_types} = + let constructor_name = of_ann_id cname and constructor_args_types = (* TODO: break sequences of long types (e.g. ByStr20 with contract ................... end Uint256 is unreadable) *) of_types ~sep:(break 1) c_arg_types in if List.is_empty c_arg_types then constructor_name + ^//^ concat_comments ~sep:space c_comments else - align (group (constructor_name ^//^ of_kwd) ^//^ constructor_args_types) + align (group (constructor_name ^//^ of_kwd) ^//^ + constructor_args_types ^//^ + concat_comments ~sep:space c_comments) let of_lib_entry = function - | Ast.LibVar (definition, otyp, expr) -> + | Ast.LibVar (comments, definition, otyp, expr) -> let definition = match otyp with - | None -> of_id definition - | Some typ -> of_typed_id definition typ + | None -> of_ann_id definition + | Some typ -> of_typed_ann_id definition typ and expr = of_expr expr in + concat_comments comments ^^ let_kwd ^^^ definition ^^^ equals ^//^ expr - | Ast.LibTyp (typ_name, constr_defs) -> - let typ_name = of_id typ_name + | Ast.LibTyp (comments, typ_name, constr_defs) -> + let typ_name = of_ann_id typ_name and constr_defs = separate_map hardline (fun cd -> pipe ^^^ of_ctr_def cd) constr_defs in + concat_comments comments ^^ type_kwd ^^^ typ_name ^^^ equals ^^ hardline ^^ constr_defs let of_library Ast.{lname; lentries} = - library_kwd ^^^ of_id lname ^^ + library_kwd ^^^ of_ann_id lname ^^ if List.is_empty lentries then hardline else let lentries = @@ -443,12 +508,12 @@ struct twice hardline ^^ lentries ^^ hardline let of_contract Ast.{cname; cparams; cconstraint; cfields; ccomps} = - let cname = of_id cname + let cname = of_ann_id cname and cparams = of_parameters cparams ~sep:hardline and cconstraint = let true_ctr = Lit.LType.TIdentifier.Name.parse_simple_name "True" in match cconstraint with - | (Ast.Literal (Lit.ADTValue (c, [], [])), _annot) when [%equal: _] c true_ctr -> + | (Ast.Literal (Lit.ADTValue (c, [], [])), _annot, _comment) when [%equal: _] c true_ctr -> (* trivially True contract constraint does not get rendered *) empty | _ -> @@ -460,8 +525,9 @@ struct else separate_map (twice hardline) - (fun (field, typ, init) -> - field_kwd ^^^ of_typed_id field typ ^^^ equals ^//^ of_expr init) + (fun (comments, field, typ, init) -> + concat_comments comments ^^ + field_kwd ^^^ of_typed_ann_id field typ ^^^ equals ^//^ of_expr init) cfields ^^ twice hardline and ccomps = @@ -472,12 +538,12 @@ struct cfields ^^ ccomps - let of_contract_module Ast.{smver; libs; elibs; contr} = + let of_contract_module Ast.{smver; file_comments; lib_comments; libs; elibs; contr_comments; contr} = let imports = let import_lib (lib, onamespace) = match onamespace with - | None -> of_id lib - | Some namespace -> of_id lib ^^^ as_kwd ^^^ of_id namespace + | None -> of_ann_id lib + | Some namespace -> of_ann_id lib ^^^ as_kwd ^^^ of_ann_id namespace in let imported_libs = separate_map (hardline) (fun imp -> import_lib imp) elibs @@ -489,9 +555,13 @@ struct | Some lib -> of_library lib ^^ twice hardline | None -> empty in - scilla_version_kwd ^^^ !^(Int.to_string smver) ^^ twice hardline ^^ + scilla_version_kwd ^^^ !^(Int.to_string smver) ^^ hardline ^^ + concat_comments file_comments ^^ + hardline ^^ imports ^^ + concat_comments lib_comments ^^ contract_library ^^ + concat_comments contr_comments ^^ of_contract contr ^^ hardline end diff --git a/src/formatter/dune b/src/formatter/dune new file mode 100644 index 000000000..8f167492a --- /dev/null +++ b/src/formatter/dune @@ -0,0 +1,16 @@ +; (ocamllex +; (modules ExtendedScillaLexer)) + +; (menhir +; (flags "--table") +; (modules ExtendedScillaParser)) + +(library + (name scilla_format) + (modes byte native) + (public_name scilla.format) + (wrapped true) + (libraries core scilla_base pprint) + (synopsis "Library to format Scilla code") + (preprocess + (pps ppx_string_interpolation ppx_compare ppx_sexp_conv))) diff --git a/src/runners/dune b/src/runners/dune index 163d760f0..ed60440cc 100644 --- a/src/runners/dune +++ b/src/runners/dune @@ -7,7 +7,8 @@ (modules scilla_runner eval_runner type_checker scilla_checker scilla_server disambiguate_state_json scilla_fmt) (libraries core core_unix.command_unix angstrom yojson cryptokit fileutils - scilla_base scilla_eval scilla_server_lib scilla_crypto cmdliner) + scilla_base scilla_eval scilla_server_lib scilla_crypto scilla_format + cmdliner) (modes byte native) (preprocess (pps ppx_sexp_conv ppx_let ppx_deriving.show bisect_ppx --conditional))) diff --git a/src/runners/scilla_fmt.ml b/src/runners/scilla_fmt.ml index 27dee7b46..e7801c61b 100644 --- a/src/runners/scilla_fmt.ml +++ b/src/runners/scilla_fmt.ml @@ -18,6 +18,7 @@ open Core open Scilla_base +open Scilla_format open Literal open GlobalConfig open ErrorUtils @@ -91,6 +92,9 @@ let scilla_sexp_fmt deannotated human_readable file = let scilla_source_code_fmt file = let open FilePath in let open StdlibTracker in + let tr () = + ExtendedSyntax.LocalLiteralTransformer.mk (FEParser.get_comments ()) + in if check_extension file file_extn_library then (* library modules *) (* file @@ -101,10 +105,12 @@ let scilla_source_code_fmt file = else if check_extension file file_extn_contract then (* contract modules *) file |> FEParser.parse_cmodule |> unpack_ast_exn + |> ExtendedSyntax.LocalLiteralTransformer.extend_cmodule (tr ()) |> Formatter.LocalLiteralSyntax.contract_to_string else if check_extension file file_extn_expression then (* expressions *) file |> FEParser.parse_expr_from_file |> unpack_ast_exn + |> ExtendedSyntax.LocalLiteralTransformer.extend_expr (tr ()) |> Formatter.LocalLiteralSyntax.expr_to_string else fatal_error (mk_error0 ~kind:"Unknown file extension" ?inst:None) diff --git a/tests/checker/bad/gold/bad_comment_1.scilla.gold b/tests/checker/bad/gold/bad_comment_1.scilla.gold index 29cc93148..487eed54e 100644 --- a/tests/checker/bad/gold/bad_comment_1.scilla.gold +++ b/tests/checker/bad/gold/bad_comment_1.scilla.gold @@ -6,7 +6,7 @@ "start_location": { "file": "checker/bad/bad_comment_1.scilla", "line": 3, - "column": 3 + "column": 1 }, "end_location": { "file": "", "line": 0, "column": 0 } } diff --git a/tests/checker/bad/gold/bad_comment_2.scilla.gold b/tests/checker/bad/gold/bad_comment_2.scilla.gold index 39a32d0d8..a4a6df411 100644 --- a/tests/checker/bad/gold/bad_comment_2.scilla.gold +++ b/tests/checker/bad/gold/bad_comment_2.scilla.gold @@ -6,7 +6,7 @@ "start_location": { "file": "checker/bad/bad_comment_2.scilla", "line": 3, - "column": 3 + "column": 1 }, "end_location": { "file": "", "line": 0, "column": 0 } } diff --git a/tests/formatter/comments.t/fields-1.scilla b/tests/formatter/comments.t/fields-1.scilla new file mode 100644 index 000000000..f46b229fb --- /dev/null +++ b/tests/formatter/comments.t/fields-1.scilla @@ -0,0 +1,21 @@ +scilla_version 0 + +library Fields1 + +contract Fields1() + +(* Field description *) +field f1 : Map Uint256 ByStr32 = Emp Uint256 ByStr32 + +(* + * Multiline + * field + * description + *) +field f2 : Map Uint256 ByStr32 = Emp Uint256 ByStr32 + +field f3 : Map Uint256 ByStr32 = Emp Uint256 ByStr32 +(* Incorrect: the description of [f3] must be above the field. + This comment will be considered as a [f4] description. *) + +field f4 : Map Uint256 ByStr32 = Emp Uint256 ByStr32 diff --git a/tests/formatter/comments.t/fields-1.scilla.gold b/tests/formatter/comments.t/fields-1.scilla.gold new file mode 100644 index 000000000..6f16a8cbb --- /dev/null +++ b/tests/formatter/comments.t/fields-1.scilla.gold @@ -0,0 +1,26 @@ +scilla_version 0 + +library Fields1 + + +contract Fields1 () + + +(* Field description *) +field f1 : Map Uint256 ByStr32 = Emp (Uint256) (ByStr32) + +(* + * Multiline + * field + * description + *) +field f2 : Map Uint256 ByStr32 = Emp (Uint256) (ByStr32) + +field f3 : Map Uint256 ByStr32 = Emp (Uint256) (ByStr32) + +(* Incorrect: the description of [f3] must be above the field. + This comment will be considered as a [f4] description. *) +field f4 : Map Uint256 ByStr32 = Emp (Uint256) (ByStr32) + + + diff --git a/tests/formatter/comments.t/libvar-1.scilla b/tests/formatter/comments.t/libvar-1.scilla new file mode 100644 index 000000000..17e79a11c --- /dev/null +++ b/tests/formatter/comments.t/libvar-1.scilla @@ -0,0 +1,16 @@ +scilla_version 0 + +library Libvar1 + +let a = Int32 0 (* a comment *) + +(* b comment *) +let b = Int32 0 + +let c = Int32 0 +(* d comment *) + +let d = Int32 0 + +contract Libvar1() + diff --git a/tests/formatter/comments.t/libvar-1.scilla.gold b/tests/formatter/comments.t/libvar-1.scilla.gold new file mode 100644 index 000000000..35ef114d5 --- /dev/null +++ b/tests/formatter/comments.t/libvar-1.scilla.gold @@ -0,0 +1,21 @@ +scilla_version 0 + +library Libvar1 + +(* a comment *) +let a = Int32 0 + +(* b comment *) +let b = Int32 0 + +let c = Int32 0 + +(* d comment *) +let d = Int32 0 + + +contract Libvar1 () + + + + diff --git a/tests/formatter/comments.t/pm-1.scilla b/tests/formatter/comments.t/pm-1.scilla new file mode 100644 index 000000000..471857aad --- /dev/null +++ b/tests/formatter/comments.t/pm-1.scilla @@ -0,0 +1,70 @@ +scilla_version 0 + +contract Pm1() + +procedure pr1(a_opt : Uint32 Option) + match a_opt with + | Some a => + (* return a *) + a + | None => (* do nothing *) + end +end + +procedure pr2(a_opt : Uint32 Option) + match a_opt with + | None => (* do nothing *) + | Some a => + (* return a *) + a + end +end + +procedure pr3(a_opt : Uint32 Option) + match a_opt with + | None => + (* do nothing *) + | Some a => + (* return a *) + a + end +end + +procedure pr4(a_opt : Uint32 Option Option) + match a_opt with + | Some a => + match a with + | Some aa => + (* accept *) + accept + | None => (* do nothing1 *) + end + | None => (* do nothing2 *) + end +end + +procedure pr5(a_opt : Uint32 Option Option) + match a_opt with + | None => (* do nothing2 *) + | Some a => + match a with + | None => (* do nothing1 *) + | Some aa => + (* accept *) + accept + end + end +end + +(* No extra whitespaces when there are no arm comments. *) +procedure pr6(a_opt : Uint32 Option Option) + match a_opt with + | None => + | Some a => + match a with + | None => + | Some aa => + accept + end + end +end diff --git a/tests/formatter/comments.t/pm-1.scilla.gold b/tests/formatter/comments.t/pm-1.scilla.gold new file mode 100644 index 000000000..0996f63aa --- /dev/null +++ b/tests/formatter/comments.t/pm-1.scilla.gold @@ -0,0 +1,72 @@ +scilla_version 0 + +contract Pm1 () + + +procedure pr1 (a_opt : Uint32 Option) + match a_opt with + | Some a => + (* return a *) + a + | None => (* do nothing *) + end +end + +procedure pr2 (a_opt : Uint32 Option) + match a_opt with + | None => (* do nothing *) + | Some a => + (* return a *) + a + end +end + +procedure pr3 (a_opt : Uint32 Option) + match a_opt with + | None => + | (* do nothing *) + Some + a => + (* return a *) + a + end +end + +procedure pr4 (a_opt : Uint32 Option Option) + match a_opt with + | Some a => + match a with + | Some aa => + (* accept *) + accept + | None => (* do nothing1 *) + end + | None => (* do nothing2 *) + end +end + +procedure pr5 (a_opt : Uint32 Option Option) + match a_opt with + | None => (* do nothing2 *) + | Some a => + match a with + | None => (* do nothing1 *) + | Some aa => + (* accept *) + accept + end + end +end + +(* No extra whitespaces when there are no arm comments. *) +procedure pr6 (a_opt : Uint32 Option Option) + match a_opt with + | None => + | Some a => + match a with + | None => + | Some aa => accept + end + end +end + diff --git a/tests/formatter/comments.t/run.t b/tests/formatter/comments.t/run.t new file mode 100644 index 000000000..f207e38fa --- /dev/null +++ b/tests/formatter/comments.t/run.t @@ -0,0 +1,8 @@ + $ for f in *.scilla + > do + > scilla-fmt "$f" > FORMATTED-"$f" && + > diff "$f".gold FORMATTED-"$f" + > if [ $? -ne 0 ]; then + > break + > fi + > done diff --git a/tests/formatter/comments.t/toplevel-1.scilla b/tests/formatter/comments.t/toplevel-1.scilla new file mode 100644 index 000000000..3b1bf99c4 --- /dev/null +++ b/tests/formatter/comments.t/toplevel-1.scilla @@ -0,0 +1,17 @@ +scilla_version 0 + +(***************************************************) +(* File comment *) +(***************************************************) + +import BoolUtils + +(***************************************************) +(* Associated library *) +(***************************************************) +library C1 + +(***************************************************) +(* Contract module *) +(***************************************************) +contract C1() diff --git a/tests/formatter/comments.t/toplevel-1.scilla.gold b/tests/formatter/comments.t/toplevel-1.scilla.gold new file mode 100644 index 000000000..81293c834 --- /dev/null +++ b/tests/formatter/comments.t/toplevel-1.scilla.gold @@ -0,0 +1,21 @@ +scilla_version 0 +(***************************************************) +(* File comment *) +(***************************************************) + +import BoolUtils + +(***************************************************) +(* Associated library *) +(***************************************************) +library C1 + + +(***************************************************) +(* Contract module *) +(***************************************************) +contract C1 () + + + + diff --git a/tests/formatter/comments.t/toplevel-2.scilla b/tests/formatter/comments.t/toplevel-2.scilla new file mode 100644 index 000000000..0af6acbd3 --- /dev/null +++ b/tests/formatter/comments.t/toplevel-2.scilla @@ -0,0 +1,38 @@ +scilla_version 0 + +(***************************************************) +(* File comment *) +(***************************************************) + +import BoolUtils + +(***************************************************) +(* Associated library *) +(***************************************************) +library C1 + +(* a variable *) +let a = Int32 42 + +(***************************************************) +(* Contract module *) +(***************************************************) +contract C1() + +(* foo procedure *) +procedure foo() + accept +end + +(* bar transition *) +transition bar() + foo +end + +(* + * transition + * baz + *) +transition baz() + foo +end diff --git a/tests/formatter/comments.t/toplevel-2.scilla.gold b/tests/formatter/comments.t/toplevel-2.scilla.gold new file mode 100644 index 000000000..1dab5e31f --- /dev/null +++ b/tests/formatter/comments.t/toplevel-2.scilla.gold @@ -0,0 +1,40 @@ +scilla_version 0 +(***************************************************) +(* File comment *) +(***************************************************) + +import BoolUtils + +(***************************************************) +(* Associated library *) +(***************************************************) +library C1 + +(* a variable *) +let a = Int32 42 + + +(***************************************************) +(* Contract module *) +(***************************************************) +contract C1 () + + +(* foo procedure *) +procedure foo () + accept +end + +(* bar transition *) +transition bar () + foo +end + +(* + * transition + * baz + *) +transition baz () + foo +end + diff --git a/tests/formatter/comments.t/toplevel-3.scilla b/tests/formatter/comments.t/toplevel-3.scilla new file mode 100644 index 000000000..3d546a39e --- /dev/null +++ b/tests/formatter/comments.t/toplevel-3.scilla @@ -0,0 +1,10 @@ +scilla_version 0 + +(***************************************************) +(* Library definition *) +(***************************************************) + +library Toplevel3 + +contract Toplevel3() + diff --git a/tests/formatter/comments.t/toplevel-3.scilla.gold b/tests/formatter/comments.t/toplevel-3.scilla.gold new file mode 100644 index 000000000..0705824aa --- /dev/null +++ b/tests/formatter/comments.t/toplevel-3.scilla.gold @@ -0,0 +1,13 @@ +scilla_version 0 + +(***************************************************) +(* Library definition *) +(***************************************************) +library Toplevel3 + + +contract Toplevel3 () + + + + diff --git a/tests/formatter/comments.t/toplevel-4.scilla b/tests/formatter/comments.t/toplevel-4.scilla new file mode 100644 index 000000000..76cff4f29 --- /dev/null +++ b/tests/formatter/comments.t/toplevel-4.scilla @@ -0,0 +1,14 @@ +scilla_version 0 +(* file comment 1 *) +(* file comment 2 *) + +(* file comment 3 *) + +(***************************************************) +(* Library definition *) +(***************************************************) + +library Toplevel4 + +contract Toplevel4() + diff --git a/tests/formatter/comments.t/toplevel-4.scilla.gold b/tests/formatter/comments.t/toplevel-4.scilla.gold new file mode 100644 index 000000000..e30b7f902 --- /dev/null +++ b/tests/formatter/comments.t/toplevel-4.scilla.gold @@ -0,0 +1,16 @@ +scilla_version 0 +(* file comment 1 *) +(* file comment 2 *) +(* file comment 3 *) + +(***************************************************) +(* Library definition *) +(***************************************************) +library Toplevel4 + + +contract Toplevel4 () + + + + diff --git a/tests/formatter/comments.t/toplevel-5.scilla b/tests/formatter/comments.t/toplevel-5.scilla new file mode 100644 index 000000000..3d4e87b1a --- /dev/null +++ b/tests/formatter/comments.t/toplevel-5.scilla @@ -0,0 +1,14 @@ +(* file comment 1 *) +scilla_version 0 +(* file comment 2 *) +(* file comment 3 *) + +(* file comment 4 *) +(* file comment 5 *) + +(* library *) +library Toplevel5 + +(* contract comment *) +contract Toplevel5() + diff --git a/tests/formatter/comments.t/toplevel-5.scilla.gold b/tests/formatter/comments.t/toplevel-5.scilla.gold new file mode 100644 index 000000000..791936831 --- /dev/null +++ b/tests/formatter/comments.t/toplevel-5.scilla.gold @@ -0,0 +1,17 @@ +scilla_version 0 +(* file comment 1 *) +(* file comment 2 *) +(* file comment 3 *) +(* file comment 4 *) +(* file comment 5 *) + +(* library *) +library Toplevel5 + + +(* contract comment *) +contract Toplevel5 () + + + + diff --git a/tests/formatter/comments.t/toplevel-6.scilla b/tests/formatter/comments.t/toplevel-6.scilla new file mode 100644 index 000000000..730fafa92 --- /dev/null +++ b/tests/formatter/comments.t/toplevel-6.scilla @@ -0,0 +1,10 @@ +scilla_version 0 + +library Toplevel6 + +(***************************************************) +(* Contract definition *) +(***************************************************) + +contract Toplevel6() + diff --git a/tests/formatter/comments.t/toplevel-6.scilla.gold b/tests/formatter/comments.t/toplevel-6.scilla.gold new file mode 100644 index 000000000..43505c447 --- /dev/null +++ b/tests/formatter/comments.t/toplevel-6.scilla.gold @@ -0,0 +1,13 @@ +scilla_version 0 + +library Toplevel6 + + +(***************************************************) +(* Contract definition *) +(***************************************************) +contract Toplevel6 () + + + + diff --git a/tests/formatter/comments.t/toplevel-7.scilla b/tests/formatter/comments.t/toplevel-7.scilla new file mode 100644 index 000000000..dc8ecb6f0 --- /dev/null +++ b/tests/formatter/comments.t/toplevel-7.scilla @@ -0,0 +1,12 @@ +scilla_version 0 +(* file comment 1 *) +(* file comment 2 *) + +(* file comment 3 *) + +(***************************************************) +(* Contract definition *) +(***************************************************) + +contract Toplevel7() + diff --git a/tests/formatter/comments.t/toplevel-7.scilla.gold b/tests/formatter/comments.t/toplevel-7.scilla.gold new file mode 100644 index 000000000..e3fcf7cdc --- /dev/null +++ b/tests/formatter/comments.t/toplevel-7.scilla.gold @@ -0,0 +1,13 @@ +scilla_version 0 +(* file comment 1 *) +(* file comment 2 *) +(* file comment 3 *) + +(***************************************************) +(* Contract definition *) +(***************************************************) +contract Toplevel7 () + + + + diff --git a/tests/formatter/comments.t/toplevel-8.scilla b/tests/formatter/comments.t/toplevel-8.scilla new file mode 100644 index 000000000..76e7697d8 --- /dev/null +++ b/tests/formatter/comments.t/toplevel-8.scilla @@ -0,0 +1,11 @@ +(* file comment 1 *) +scilla_version 0 +(* file comment 2 *) +(* file comment 3 *) + +(* file comment 4 *) +(* file comment 5 *) + +(* contract comment *) +contract Toplevel8() + diff --git a/tests/formatter/comments.t/toplevel-8.scilla.gold b/tests/formatter/comments.t/toplevel-8.scilla.gold new file mode 100644 index 000000000..14a5adfb5 --- /dev/null +++ b/tests/formatter/comments.t/toplevel-8.scilla.gold @@ -0,0 +1,13 @@ +scilla_version 0 +(* file comment 1 *) +(* file comment 2 *) +(* file comment 3 *) +(* file comment 4 *) +(* file comment 5 *) + +(* contract comment *) +contract Toplevel8 () + + + + diff --git a/tests/formatter/comments.t/typedef-1.scilla b/tests/formatter/comments.t/typedef-1.scilla new file mode 100644 index 000000000..d1cf31ea1 --- /dev/null +++ b/tests/formatter/comments.t/typedef-1.scilla @@ -0,0 +1,21 @@ +scilla_version 0 + +library Typedef1 + +type A = (* A comment *) + | A1 (* A1 comment *) + | A2 of ByStr20 (* A2 comment *) + | A3 + | A4 of ByStr20 + | A5 of ByStr20 ByStr20 + | A6 of ByStr20 ByStr20 (* A6 comment *) + +type B = (* B comment *) + | B1 + | B2 (* Multiline B2 + comment *) + +type C = + | C1 + +contract Typedef1() diff --git a/tests/formatter/comments.t/typedef-1.scilla.gold b/tests/formatter/comments.t/typedef-1.scilla.gold new file mode 100644 index 000000000..83fe72098 --- /dev/null +++ b/tests/formatter/comments.t/typedef-1.scilla.gold @@ -0,0 +1,28 @@ +scilla_version 0 + +library Typedef1 + +(* A comment *) +type A = +| A1 (* A1 comment *) +| A2 of ByStr20 (* A2 comment *) +| A3 +| A4 of ByStr20 +| A5 of ByStr20 ByStr20 +| A6 of ByStr20 ByStr20 (* A6 comment *) + +(* B comment *) +type B = +| B1 +| B2 (* Multiline B2 + comment *) + +type C = +| C1 + + +contract Typedef1 () + + + + diff --git a/tests/formatter/look_and_feel/Polynetwork.t/run.t b/tests/formatter/look_and_feel/Polynetwork.t/run.t index 79f2b9b00..f568ab6cc 100644 --- a/tests/formatter/look_and_feel/Polynetwork.t/run.t +++ b/tests/formatter/look_and_feel/Polynetwork.t/run.t @@ -18,6 +18,11 @@ contract Polynetwork (thisChainID : Uint64) + (* + * Scilla cross chain tx hash indexed by the automatically increased index. + * This map exists for the reason that Poly chain can verify the existence + * of cross chain request tx coming from Scilla + *) field f_zilToPolyTxHashMap : Map Uint256 ByStr32 = Emp (Uint256) (ByStr32) field f_zilToPolyTxHashIndex : Uint256 = Uint256 0 @@ -34,6 +39,7 @@ nextbookkeeper_keepers = verifyPubkey pubkeys; match nextbookkeeper_keepers with | Pair nextBookKeeper keepers => + (* Ensure that Header's nextBookKeeper is same as the one from verifyPubkey *) nbk_eq = builtin eq nextBookKeeper h_nextBookkeeper; match nbk_eq with | True => @@ -139,6 +145,15 @@ end end + (* @notice Verify Poly chain header and proof, execute the cross chain tx from Poly chain to Zilliqa + * @param proof Poly chain tx merkle proof + * @param rawHeader The header containing crossStateRoot to verify the above tx merkle proof + * @param headerProof The header merkle proof used to verify rawHeader + * @param curRawHeader Any header in current epoch consensus of Poly chain + * @param headerSig The coverted signature veriable for solidity derived from Poly chain consensus nodes' signature + * used to verify the validity of curRawHeader + * @return true or false + *) transition verifyHeaderAndExecuteTx ( proof : Proof, @@ -200,7 +215,7 @@ headerHash = get_header_hash rawHeader; proof_ok = builtin eq headerHash proveValue32; match proof_ok with - | True => + | True => (* Do nothing *) | False => e = { _exception : "Merkle proof invalid" }; throw e @@ -222,7 +237,7 @@ | False => signed = verifySig rawHeader headerSig curKeepers m; match signed with - | True => + | True => (* Do nothing *) | False => e = { _exception : "Signature verification failed" }; throw e @@ -250,6 +265,12 @@ end end + (* @notice change Poly chain consensus book keeper + * @param rawHeader Poly chain change book keeper block raw header + * @param pubKeyList Poly chain consensus nodes public key list + * @param sigList Poly chain consensus nodes signature list + * @return true or false + *) transition changeBookKeeper (rawHeader : ByStr, pubkeys : List Pubkey, sigList : List Signature) header_o = deserialize_Header rawHeader zero_uint32; @@ -313,6 +334,13 @@ f_zilToPolyTxHashIndex := newTxHashIndex end + (* @notice ERC20 token cross chain to other blockchain. + * this function push tx event to blockchain + * @param toChainId Target chain id + * @param toContract Target smart contract address in target block chain + * @param txData Transaction data for target chain, include to_address, amount + * @return true or false + *) transition crossChain (toChainId : Uint64, toContract : ByStr, method : ByStr, txData : ByStr) txHashIndex <- f_zilToPolyTxHashIndex; @@ -326,6 +354,7 @@ txp = TxParam paramTxHash crossChainId fromContract toChainId toContract method txData; + (* Serialize the TxParam object *) empty_bystr = let b = 0x in builtin to_bystr b; rawParam = append_TxParam empty_bystr txp; rawParamHash = builtin keccak256hash rawParam; diff --git a/tests/formatter/look_and_feel/ackermann.t/run.t b/tests/formatter/look_and_feel/ackermann.t/run.t index 392cadea7..8a372ffe2 100644 --- a/tests/formatter/look_and_feel/ackermann.t/run.t +++ b/tests/formatter/look_and_feel/ackermann.t/run.t @@ -1,8 +1,10 @@ $ scilla-fmt ackermann.scilexp + (* some helper functions one would hope to find in stdlib *) let nat_succ : Nat -> Nat = fun (n : Nat) => Succ n in + (* [nat_iter 'A f n] = f^n -- functional power operator *) let nat_iter : forall 'A. ('A -> 'A) -> Nat -> 'A -> 'A = tfun 'A => fun (f : 'A -> 'A) => @@ -30,6 +32,7 @@ fun (n : Nat) => iter_nat_nat f n nat_succ in + (* tests *) let uint0 = Uint32 0 in let uint1 = Uint32 1 in let uint2 = Uint32 2 in diff --git a/tests/formatter/look_and_feel/ark.t/run.t b/tests/formatter/look_and_feel/ark.t/run.t index 2d69fb1c7..3f695cf25 100644 --- a/tests/formatter/look_and_feel/ark.t/run.t +++ b/tests/formatter/look_and_feel/ark.t/run.t @@ -1,5 +1,8 @@ $ scilla-fmt ark.scilla scilla_version 0 + (***************************************************) + (* Associated library *) + (***************************************************) import IntUtils @@ -9,26 +12,38 @@ type Denom = | Zil - | Token of ByStr20 + | Token of ByStr20 (* token address / hash *) type Coins = - | Coins of Denom Uint128 + | Coins of Denom Uint128 (* denom, amount *) type NFT = | NFT of (ByStr20 with contract field token_owners : Map Uint256 ByStr20 end) Uint256 + + (* token address*) + (* token id *) type Side = - | Buy + | (* buying or selling the NFT *) + Buy + | Sell + (* a partial trade instruction that can be executed later. + price, token & fee is provided separately and must be combined + to produce a valid full cheque (and cheque hash) *) type Cheque = - | Cheque of Side BNum Uint128 ByStr33 ByStr64 + | Cheque of + Side BNum Uint128 ByStr33 ByStr64 + (* trade direction, expiry, nonce, pubkey, signature *) + (* executing or voiding a cheque *) type Action = | Execute | Void + (* Global variables *) let zero = Uint128 0 let none = None {(ByStr20)} @@ -53,11 +68,13 @@ let void = Void + (* Library functions *) let one_msg = fun (msg : Message) => let nil_msg = Nil {(Message)} in Cons {(Message)} msg nil_msg + (* Error exception *) type Error = | CodeNotOwner | CodeNotPendingOwner @@ -135,6 +152,9 @@ builtin sha256hash p5 + (***************************************************) + (* The contract definition *) + (***************************************************) contract ARK ( contract_owner : ByStr20, @@ -143,6 +163,7 @@ ) + (* Mutable fields *) field current_owner : Option ByStr20 = Some {(ByStr20)} contract_owner field pending_owner : Option ByStr20 = none @@ -154,6 +175,9 @@ field voided_cheques : Map ByStr33 (Map ByStr32 Bool) = Emp (ByStr33) (Map ByStr32 Bool) + (**************************************) + (* Procedures *) + (**************************************) procedure ThrowError (err : Error) e = make_error err; throw e @@ -216,6 +240,7 @@ procedure IsValidPrice (price : Coins) amount = get_amount price; + (* price should be > 0 *) is_zero = builtin eq zero amount; match is_zero with | False => @@ -227,6 +252,7 @@ procedure IsValidFee (price : Coins, fee : Uint128) amount = get_amount price; + (* fee should be < price *) is_valid = builtin lt fee amount; match is_valid with | True => @@ -272,15 +298,21 @@ pubkey : ByStr33, signature : ByStr64 ) + (* reinteprete the cheque hash bytes as a hex string *) hex_hash = builtin to_string cheque_hash; + (* prefix it with action text to disambiguate message type *) action_prefix = get_action_prefix action; action_string = builtin concat action_prefix hex_hash; + (* construct signed message header *) chain_id_string = builtin to_string chain_id; message_header = builtin concat signed_message_prefix chain_id_string; message_header = builtin concat message_header signed_message_suffix; + (* prefix with generic zilliqa signed message header *) message_string = builtin concat message_header action_string; + (* hash the message to the signed data *) signed_hash = builtin sha256hash message_string; signed_data = builtin to_bystr signed_hash; + (* validate the signature *) valid_sig = builtin schnorr_verify pubkey signed_data signature; match valid_sig with | True => @@ -308,6 +340,7 @@ _this_address direction token price fee_amount expiry nonce; IsNotVoided cheque_hash pubkey; IsValidSignature execute cheque_hash pubkey signature; + (* consume cheque by voiding it *) voided_cheques[pubkey][cheque_hash] := true end end @@ -347,6 +380,7 @@ procedure TransferNFT (token : NFT, from : ByStr20, to : ByStr20) match token with | NFT token_address token_id => + (* check the from address so that a cheque can't be reused once the token is transferred *) maybe_token_owner <-& token_address.token_owners[token_id]; match maybe_token_owner with | Some token_owner => @@ -374,6 +408,9 @@ end end + (***************************************) + (* Transitions *) + (***************************************) transition ExecuteTrade ( token : NFT, @@ -393,12 +430,15 @@ seller_receive_amount = builtin sub amount fee_amount; seller_receive_coins = Coins denom seller_receive_amount; fee_receive_coins = Coins denom fee_amount; + (* if zil (non-zrc2), do additional validation and accept amount first *) match denom with | Zil => receiving_from_buyer = builtin eq buyer _sender; match receiving_from_buyer with | True => | False => + (* if the executor is not the buyer, we cannot receive zil, it must be wrapped for pre-approval *) + (* this means that bidders that do not immediately match should always offer in wZIL *) err = CodeInvalidPrice; ThrowError err end; @@ -406,6 +446,8 @@ match correct_amount with | True => | False => + (* the amount of zils need to match the required amount as specified in the price exactly *) + (* otherwise, funds may be stuck and lost forever *) err = CodeInvalidPrice; ThrowError err end; @@ -447,6 +489,7 @@ event e end + (* @dev: Sets the token proxy which calls TransferFrom on ZRC-2 tokens to faciliate transfers. Can only be set once by the owner, and is then immutable. *) transition SetTokenProxy (address : ByStr20) IsOwner _sender; t <- token_proxy; @@ -462,6 +505,9 @@ end end + (** Ownership lifecycle transitions *) + (* @dev: Transfers contract ownership to a new address. The new address must call the AcceptOwnership transition to finalize the transfer. *) + (* @param new_owner: Address of the new current_owner. *) transition TransferOwnership (new_owner : ByStr20) IsOwner _sender; o = Some {(ByStr20)} new_owner; @@ -475,6 +521,7 @@ event e end + (* @dev: Finalizes transfer of contract ownership. Must be called by the new current_owner. *) transition AcceptOwnership () IsPendingOwner _sender; previous_current_owner <- current_owner; @@ -490,6 +537,7 @@ event e end + (* @dev: Removes the current_owner, meaning that new minters can no longer be added. Must not have a pending owner. *) transition RevokeOwnership () IsOwner _sender; NoPendingOwner; @@ -498,11 +546,17 @@ event e end + (*************************************) + (* Callbacks *) + (*************************************) + (* @dev: Handle callback after sending ZRC-1 tokens via TransferFrom *) transition TransferFromSuccessCallBack (from : ByStr20, recipient : ByStr20, token_id : Uint256) end + (* no-op *) + (* @dev: Handle callback after sending ZRC-6 tokens via TransferFrom *) transition ZRC6_TransferFromCallback (from : ByStr20, to : ByStr20, token_id : Uint256) diff --git a/tests/formatter/look_and_feel/auction.t/run.t b/tests/formatter/look_and_feel/auction.t/run.t index 841fa62a5..72f327c7c 100644 --- a/tests/formatter/look_and_feel/auction.t/run.t +++ b/tests/formatter/look_and_feel/auction.t/run.t @@ -1,5 +1,8 @@ $ scilla-fmt auction.scilla scilla_version 0 + (***************************************************) + (* Associated library *) + (***************************************************) import BoolUtils @@ -36,14 +39,19 @@ let auction_end_code = Int32 9 + (***************************************************) + (* The contract definition *) + (***************************************************) contract OpenAuction ( + (* Parameters *) auctionStart : BNum, biddingTime : Uint128, beneficiary : ByStr20 ) + (* Mutable fields *) field ended : Bool = False field highestBidder : Option ByStr20 = None {(ByStr20)} @@ -52,6 +60,7 @@ field pendingReturns : Map ByStr20 Uint128 = Emp (ByStr20) (Uint128) + (* Transition 1: bidding *) transition Bid () blk <-& BLOCKNUMBER; endtime = builtin badd auctionStart biddingTime; @@ -85,6 +94,7 @@ send msgs | False => hb <- highestBid; + (* Checks if the bid is too low *) sufficientBid = builtin lt hb _amount; match sufficientBid with | False => @@ -102,14 +112,18 @@ hbPrev <- highestBidder; match hbPrev with | Some prevHighestBidder => + (* There is already a highest bidder *) option_pendingReturnsForPrevHB <- pendingReturns[prevHighestBidder]; getPRForPrevHighestBidder = match option_pendingReturnsForPrevHB with | Some pendingReturnsForPrevHB => + (* User already has some balance in the pending returns that is not claimed *) builtin add hb pendingReturnsForPrevHB | None => hb end; + (* Prev highest bidder has no pending returns. *) pendingReturns[prevHighestBidder] := getPRForPrevHighestBidder; + (* Update the highest bidder *) bidder = Some {(ByStr20)} _sender; highestBidder := bidder; highestBid := _amount; @@ -122,6 +136,7 @@ }; event ev | None => + (* Process first bid *) first_bidder = Some {(ByStr20)} _sender; highestBidder := first_bidder; highestBid := _amount; @@ -139,6 +154,7 @@ end end + (* Transition 2: claiming money back *) transition Withdraw () prs <- pendingReturns; pr = builtin get prs _sender; @@ -164,6 +180,7 @@ end end + (* Transition 3: auction ends *) transition AuctionEnd () blk <-& BLOCKNUMBER; e <- ended; diff --git a/tests/formatter/look_and_feel/bookstore.t/run.t b/tests/formatter/look_and_feel/bookstore.t/run.t index c306b298e..39be29ec6 100644 --- a/tests/formatter/look_and_feel/bookstore.t/run.t +++ b/tests/formatter/look_and_feel/bookstore.t/run.t @@ -1,6 +1,21 @@ $ scilla-fmt bookstore.scilla scilla_version 0 + (* + * Bookstore Contract + * + * This contract demonstrates how a developer can build a CRUD-like smart contract easily. + * Concepts covered: + * - Procedures + * - Custom ADTs + * - Simple Access Controls + * + * Access control logic is delibrately left out for brevity. You can reference AddMember + * for how you can implement access control to prevent unauthorised access to transitions. + *) + (***************************************************) + (* Associated library *) + (***************************************************) library BookStore let one_msg = @@ -8,6 +23,7 @@ let nil_msg = Nil {(Message)} in Cons {(Message)} msg nil_msg + (* error codes library *) let code_success = Uint32 0 let code_book_not_found = Uint32 1 @@ -20,13 +36,24 @@ let code_store_not_open = Uint32 5 + (* + * Book is an ADT with two fields: + * Book = { book_title, author } + *) type Book = | Book of String String + (* + * Member is an ADT with two fields: + * Member = { name , membership_type } + *) type Member = | Member of String Uint32 + (***************************************************) + (* The contract definition *) + (***************************************************) contract BookStore ( owner : ByStr20, @@ -34,12 +61,30 @@ ) + (* storeName can be immutable if it won't ever be changed *) + (* Membership data consists of three attributes *) + (* Equivalent member data in C++ struct *) + (* struct Member { *) + (* ByStr20 address; *) + (* String name; *) + (* Uint32 membershipType; // 0: Regular, 1: Premium, 2: Corporate *) + (* } *) + (* Where address is the "key" *) field members : Map ByStr20 Member = Emp (ByStr20) (Member) + (* bookstore is opened by default during initialisation *) field is_store_open : Bool = True + (* Bookinventory will store a Map of Books *) field bookInventory : Map Uint32 Book = Emp (Uint32) (Book) + (* Book data consists of three attributes: BookID, Title and Author*) + (* Equivalent member data in C++ struct *) + (* struct Book { *) + (* Uint32 BookID; *) + (* String Book_title; *) + (* String Author; *) + (* } *) procedure EmitMemberEvent (status : Bool, status_code : Uint32, msg : String) match status with | True => @@ -75,7 +120,15 @@ end end + (***************************************************) + (* Transitions *) + (***************************************************) + (* + * OpenStore: Set the store as open or close + * @param: is_open { Boolean } + *) transition OpenStore (is_open : Bool) + (* Access control: Checking if sender is the owner of the Contract *) is_authorized = builtin eq _sender owner; match is_authorized with | True => @@ -83,17 +136,25 @@ e = { _eventname : "OpenStore"; status : is_open }; event e | False => + (* Unauthorized transaction *) status = False; msg = "Unauthorised Transaction"; EmitMemberEvent status code_not_authorized msg end end + (* @notice: add member is an example. It is not used in other functions. *) + (* @dev: in real contracts, a developer can use a members mapping to manage *) + (* access controls to grant a user permission to perform certain actions *) + (* (e.g. add/remove books) *) transition AddMember (name : String, member_address : ByStr20, member_type : Uint32) + (* Access control: Checking if sender is the owner of the Contract *) is_authorized = builtin eq _sender owner; match is_authorized with | True => + (* Only the owner can add member *) + (* Check if membership type is valid. *) valid_type = let three = Uint32 3 in builtin lt member_type three; match valid_type with | True => @@ -102,18 +163,26 @@ status = True; EmitMemberEvent status code_success name | False => + (* Code for the membership type is invalid *) status = False; msg = "Invalid membership type"; EmitMemberEvent status code_invalid_params msg end | False => + (* Unauthorized transaction *) status = False; msg = "Unauthorised Transaction"; EmitMemberEvent status code_not_authorized msg end end + (* @notice: Allows a `_sender` to add a book to the bookstore *) + (* @dev : Access controls are omitted for brevity. In production contracts, *) + (* you will want to implement proper access controls to allow only *) + (* an owner or member to add a book. *) transition AddBook (book_title : String, author : String, book_id : Uint32) + (* @dev: Preconditions can be set to allow only members to add a book *) + (* @dev: Access controls logic omitted for brevity *) is_open <- is_store_open; match is_open with | True => @@ -124,20 +193,30 @@ status = False; EmitBookEvent status code_bookid_exist action book_id | False => + (* Creating a new Book Model *) + (* A new book model is a Pair of book_title and author *) new_book = Book book_title author; + (* Add the new book to the book_inventory Map, with BookID as the key *) bookInventory[book_id] := new_book; action = "Add"; status = True; EmitBookEvent status code_success action book_id end | False => + (* Store is not open *) action = "Add"; status = False; EmitBookEvent status code_store_not_open action book_id end end + (* @notice: Allows a `_sender` to remove a book from the bookstore *) + (* @dev : Access controls are omitted for brevity. In production contracts, *) + (* you will want to implement proper access controls to allow only *) + (* an owner or member to remove a book. *) transition RemoveBook (book_id : Uint32) + (* @dev: Preconditions can be set to allow only members to remove a book *) + (* @dev: Access controls logic omitted for brevity *) is_open <- is_store_open; match is_open with | True => @@ -155,21 +234,34 @@ EmitBookEvent status code_book_not_found action book_id end | False => + (* Store is not open *) action = "Add"; status = False; EmitBookEvent status code_store_not_open action book_id end end + (* @notice: Allows a `_sender` to update a book from the bookstore *) + (* @dev : Access controls are omitted for brevity. In production contracts, *) + (* you will want to implement proper access controls to allow only *) + (* an owner or member to remove a book. *) transition UpdateBook (book_id : Uint32, book_title : String, author : String) + (* @dev: Preconditions can be set to allow only members to update a book *) + (* @dev: Access controls omitted for brevity *) + (* preconditions *) does_book_exist <- exists bookInventory[book_id]; match does_book_exist with | False => + (* Book ID is not found in the records. *) action = "Update"; status = False; EmitBookEvent status code_book_not_found action book_id | True => + (* constructs book model *) + (* Creating a new Book Model *) + (* A new book model is a Pair of book_title and author *) new_book = Book book_title author; + (* Add the new book to the book_inventory Map, with BookID as the key *) bookInventory[book_id] := new_book; action = "Update"; status = True; diff --git a/tests/formatter/look_and_feel/chainid.t/run.t b/tests/formatter/look_and_feel/chainid.t/run.t index f5b2fade0..18555973c 100644 --- a/tests/formatter/look_and_feel/chainid.t/run.t +++ b/tests/formatter/look_and_feel/chainid.t/run.t @@ -1,6 +1,9 @@ $ scilla-fmt chainid.scilla scilla_version 0 + (***************************************************) + (* The contract definition *) + (***************************************************) contract HelloWorld () diff --git a/tests/formatter/look_and_feel/crowdfunding_governor.t/run.t b/tests/formatter/look_and_feel/crowdfunding_governor.t/run.t index 6895eea05..c632d34b5 100644 --- a/tests/formatter/look_and_feel/crowdfunding_governor.t/run.t +++ b/tests/formatter/look_and_feel/crowdfunding_governor.t/run.t @@ -20,6 +20,7 @@ fun (goal : Uint128) => builtin lt balance goal + (* Error exceptions *) type Error = | SenderIsNotContractOwner | SenderAlreadyDonated @@ -53,11 +54,13 @@ storage : ByStr20 with contract field backers : Map ByStr20 Uint128 end ) with + (* these are all the fields of the storage contract *) let zero = Uint128 0 in builtin lt zero goal => + (* no storage fields! *) procedure Throw (error : Error) e = make_error error; throw e @@ -69,7 +72,7 @@ | False => e = SenderIsNotContractOwner; Throw e - | True => + | True => (* do nothing *) end end @@ -105,7 +108,7 @@ | True => e = DeadlineHasPassed; Throw e - | False => + | False => (* do nothing *) end end @@ -116,7 +119,7 @@ | False => e = DeadlineHasNotPassedYet; Throw e - | True => + | True => (* do nothing *) end end @@ -127,7 +130,7 @@ | False => e = TargetIsReached; Throw e - | True => + | True => (* do nothing *) end end @@ -138,7 +141,7 @@ | True => e = TargetIsNotReached; Throw e - | False => + | False => (* do nothing *) end end @@ -148,7 +151,7 @@ | True => e = SenderAlreadyDonated; Throw e - | False => + | False => (* do nothing *) end end diff --git a/tests/formatter/look_and_feel/crowdfunding_proc.t/run.t b/tests/formatter/look_and_feel/crowdfunding_proc.t/run.t index 6022f4956..9268987bb 100644 --- a/tests/formatter/look_and_feel/crowdfunding_proc.t/run.t +++ b/tests/formatter/look_and_feel/crowdfunding_proc.t/run.t @@ -1,5 +1,11 @@ $ scilla-fmt crowdfunding_proc.scilla scilla_version 0 + (***************************************************) + (* Scilla version *) + (***************************************************) + (***************************************************) + (* Associated library *) + (***************************************************) import BoolUtils @@ -55,18 +61,24 @@ let reclaimed_code = Int32 9 + (***************************************************) + (* The contract definition *) + (***************************************************) contract Crowdfunding ( + (* Parameters *) owner : ByStr20, max_block : BNum, goal : Uint128 ) with + (* Contract constraint *) let zero = Uint128 0 in builtin lt zero goal => + (* Mutable fields *) field backers : Map ByStr20 Uint128 = Emp (ByStr20) (Uint128) field funded : Bool = False @@ -178,6 +190,7 @@ send msgs end + (* transition ClaimBack *) transition ClaimBack () blk <-& BLOCKNUMBER; after_deadline = builtin blt max_block blk; @@ -192,7 +205,9 @@ | True => res <- backers[_sender]; match res with - | None => ClaimBackFailure cannot_reclaim_code + | None => + (* Sender has not donated *) + ClaimBackFailure cannot_reclaim_code | Some v => PerformClaimBack v end end diff --git a/tests/formatter/look_and_feel/crowdfunding_storage.t/run.t b/tests/formatter/look_and_feel/crowdfunding_storage.t/run.t index 83909f19a..c85d81fb7 100644 --- a/tests/formatter/look_and_feel/crowdfunding_storage.t/run.t +++ b/tests/formatter/look_and_feel/crowdfunding_storage.t/run.t @@ -3,6 +3,7 @@ library CrowdfundingStorage + (* Error exceptions *) type Error = | GovernorIsNotSetYet | SenderIsNotGovernor @@ -20,11 +21,15 @@ { _exception : "Error"; code : result_code } + (* This contract does not support transferring contract ownership + for the sake of simplicity of exposition *) contract CrowdfundingStorage (contract_owner : ByStr20) + (* fields of the original contract *) field backers : Map ByStr20 Uint128 = Emp (ByStr20) (Uint128) + (* special fields to support upgradeability *) field governor : Option ByStr20 = None {(ByStr20)} procedure Throw (error : Error) @@ -44,7 +49,7 @@ | False => e = SenderIsNotGovernor; Throw e - | True => + | True => (* do nothing *) end end end @@ -55,10 +60,11 @@ | False => e = SenderIsNotContractOwner; Throw e - | True => + | True => (* do nothing *) end end + (* transition to modify the storage fields and field maps *) transition SetBackersKey (key : ByStr20, val : Uint128) RequireGovernor; backers[key] := val @@ -69,6 +75,7 @@ delete backers[key] end + (* transitions to support upgradeability *) transition SetStorageGovernor (new_governor : ByStr20) RequireContractOwner; gov = Some {(ByStr20)} new_governor; diff --git a/tests/formatter/look_and_feel/earmarked-coin.t/run.t b/tests/formatter/look_and_feel/earmarked-coin.t/run.t index e1dbf587a..e77982974 100644 --- a/tests/formatter/look_and_feel/earmarked-coin.t/run.t +++ b/tests/formatter/look_and_feel/earmarked-coin.t/run.t @@ -1,10 +1,19 @@ $ scilla-fmt earmarked-coin.scilla scilla_version 0 + (* + * An implementation of EarmarkedLibraCoin module in Scilla + * https://developers.libra.org/docs/move-overview.html + *) + (* Consider this situation: Bob is going to create an account at address A at + some point in the future. Alice wants to "earmark" some funds for Bob so that he + can pull them into his account once it is created. But she also wants to be able + to reclaim the funds for herself if Bob never creates the account. *) import BoolUtils library EarmarkedCoin + (* funds and their future owner *) type EarmarkedCoin = | EarmarkedCoin of Uint128 ByStr20 @@ -28,6 +37,7 @@ field earmarked_coins : Map ByStr20 EarmarkedCoin = Emp (ByStr20) (EarmarkedCoin) + (* ----- utility procedures ----- *) procedure TransferFunds (amount : Uint128, recipient : ByStr20) msg = { _tag : ""; _recipient : recipient; _amount : amount }; msgs = one_msg msg; @@ -57,6 +67,13 @@ event e end + (* ----- transitions ----- *) + (* + * Earmark `_amount` for the future recipient `recip`. + * This can be done at most one time for each `_sender`. + * To change the earmarked amount or the future recipient, + * invoke `ClaimForCreator` transition and then `Earmark` again. + *) transition Earmark (recip : ByStr20) c <- exists earmarked_coins[_sender]; match c with @@ -69,10 +86,12 @@ end end + (* Claim funds earmarked by a sender with `earmarked_coin_address` *) transition ClaimForRecipient (earmarked_coin_address : ByStr20) e_coin_opt <- earmarked_coins[earmarked_coin_address]; match e_coin_opt with | Some (EarmarkedCoin amount recipient) => + (* transfer only if the funds have been earmarked for the caller *) authorized_to_claim = builtin eq recipient _sender; match authorized_to_claim with | True => @@ -81,18 +100,28 @@ SuccessfulTransferOfFunds _this_address _sender | False => FailedToTransferFunds _this_address _sender not_authorized_code end - | None => FailedToTransferFunds _this_address _sender did_not_earmark_code + | None => + (* nobody with account at `earmarked_coin_address` earmarked any funds *) + FailedToTransferFunds _this_address _sender did_not_earmark_code end end + (* + * The sender (creator) should be able to claim back the earmarked funds + * at any time. This prevents the funds from being frozen if the recipient + * never claims them. + *) transition ClaimForCreator () e_coin_opt <- earmarked_coins[_sender]; match e_coin_opt with | Some (EarmarkedCoin amount _) => + (* get back earmarked money *) TransferFunds amount _sender; delete earmarked_coins[_sender]; SuccessfulTransferOfFunds _this_address _sender - | None => FailedToTransferFunds _this_address _sender did_not_earmark_code + | None => + (* Sender has not earmarked *) + FailedToTransferFunds _this_address _sender did_not_earmark_code end end diff --git a/tests/formatter/look_and_feel/empty.t/run.t b/tests/formatter/look_and_feel/empty.t/run.t index 19cbb03d0..c4c710372 100644 --- a/tests/formatter/look_and_feel/empty.t/run.t +++ b/tests/formatter/look_and_feel/empty.t/run.t @@ -1,5 +1,6 @@ $ scilla-fmt empty.scilla scilla_version 0 + (* import all known libraries to type-check them. *) import BoolUtils diff --git a/tests/formatter/look_and_feel/fungible-token.t/run.t b/tests/formatter/look_and_feel/fungible-token.t/run.t index 206e77dee..409c10be6 100644 --- a/tests/formatter/look_and_feel/fungible-token.t/run.t +++ b/tests/formatter/look_and_feel/fungible-token.t/run.t @@ -1,6 +1,10 @@ $ scilla-fmt fungible-token.scilla scilla_version 0 + (* This contract implements a fungible token interface a la ERC20.*) + (***************************************************) + (* Associated library *) + (***************************************************) library FungibleToken let one = Uint128 1 @@ -30,12 +34,16 @@ end end + (* returns singleton List Message *) let one_msg = fun (msg : Message) => let nil_msg = Nil {(Message)} in Cons {(Message)} msg nil_msg + (***************************************************) + (* The contract definition *) + (***************************************************) contract FungibleToken ( owner : ByStr20, @@ -46,6 +54,7 @@ ) + (* Initial balance is not stated explicitly: it's initialized when creating the contract. *) field balances : Map ByStr20 Uint128 = let m = Emp (ByStr20) (Uint128) in builtin put m owner total_tokens @@ -101,8 +110,10 @@ can_do = le_int tokens b; match can_do with | True => + (* subtract tokens from _sender and add it to "to" *) new_sender_bal = builtin sub b tokens; balances[_sender] := new_sender_bal; + (* Adds tokens to "to" address *) to_bal <- balances[to]; new_to_bal = match to_bal with @@ -122,6 +133,7 @@ msgs = one_msg msg; send msgs | False => + (* balance not sufficient. *) msg = { _tag : "TransferFailure"; @@ -135,6 +147,7 @@ send msgs end | None => + (* no balance record, can't transfer *) msg = { _tag : "TransferFailure"; @@ -151,15 +164,18 @@ transition TransferFrom (from : ByStr20, to : ByStr20, tokens : Uint128) bal <- balances[from]; + (* Check if _sender has been authorized by "from" *) sender_allowed_from <- allowed[from][_sender]; match bal with | Some a => match sender_allowed_from with | Some b => + (* We can only transfer the minimum of available or authorized tokens *) t = min_int a b; can_do = le_int tokens t; match can_do with | True => + (* tokens is what we should subtract from "from" and add to "to" *) new_from_bal = builtin sub a tokens; balances[from] := new_from_bal; to_bal <- balances[to]; @@ -167,8 +183,11 @@ | Some tb => new_to_bal = builtin add tb tokens; balances[to] := new_to_bal - | None => balances[to] := tokens + | None => + (* "to" has no balance. So just set it to tokens *) + balances[to] := tokens end; + (* reduce "allowed" by "tokens" *) new_allowed = builtin sub b tokens; allowed[from][_sender] := new_allowed; msg = diff --git a/tests/formatter/look_and_feel/helloWorld.t/run.t b/tests/formatter/look_and_feel/helloWorld.t/run.t index 1077b55fe..38073f5c5 100644 --- a/tests/formatter/look_and_feel/helloWorld.t/run.t +++ b/tests/formatter/look_and_feel/helloWorld.t/run.t @@ -1,8 +1,12 @@ $ scilla-fmt helloWorld.scilla scilla_version 0 + (* HelloWorld contract *) import ListUtils + (***************************************************) + (* Associated library *) + (***************************************************) library HelloWorld let one_msg = @@ -15,6 +19,9 @@ let set_hello_code = Int32 2 + (***************************************************) + (* The contract definition *) + (***************************************************) contract HelloWorld (owner : ByStr20) diff --git a/tests/formatter/look_and_feel/map_corners_test.t/run.t b/tests/formatter/look_and_feel/map_corners_test.t/run.t index d96aecfb5..b3faf2128 100644 --- a/tests/formatter/look_and_feel/map_corners_test.t/run.t +++ b/tests/formatter/look_and_feel/map_corners_test.t/run.t @@ -1,5 +1,7 @@ $ scilla-fmt map_corners_test.scilla scilla_version 0 + (* A script to run all transitions here against a running IPC server is provided. *) + (* Check out scripts/run_ipc_map_corner_tests.sh. *) import BoolUtils @@ -11,6 +13,8 @@ Cons {(Message)} msg nil_msg + (* The test sequence here is based on the unit tests in Test_ScillaIPCServer.cpp. *) + (* Transitions "t*" are expected to succeed while "f*" are expected to fail. *) contract MapCornersTest () @@ -46,7 +50,9 @@ throw e end + (* test_query_simple *) transition t1 () + (* Check existing value. *) tname = "t1"; f <- f_s1; s = "420"; @@ -55,11 +61,14 @@ | False => fail tname | True => end; + (* Now store back a different value for next test. *) s2 = "421"; f_s1 := s2 end + (* test_query_map_1 *) transition t2 () + (* Check existing value. *) tname = "t2"; f <- f_s1; s = "421"; @@ -68,14 +77,17 @@ | False => fail tname | True => end; + (* Insert value for next test. *) key1 = "key1"; val1 = "420"; f_m1[key1] := val1 end + (* foo_test_query_map_1 *) transition t3 () tname = "t3"; s = "420"; + (* Fetch key1 and ensure value is "420" as set in t2. *) key1 = "key1"; val1 <- f_m1[key1]; match val1 with @@ -89,6 +101,7 @@ end | None => fail tname end; + (* Fetch "key2" and ensure not found. *) key2 = "key2"; val2 <- f_m1[key2]; match val2 with @@ -97,26 +110,32 @@ fail_msg tname m | None => end; + (* Delete key1 for next test. *) delete f_m1[key1] end + (* foo_test_query_map_1 *) transition t4 () tname = "t4"; + (* Ensure key1 not present anymore. *) key1 = "key1"; key1_found <- exists f_m1[key1]; match key1_found with | True => fail tname | False => end; + (* Store data for next test. *) key1a = "key1a"; key2a = "key2a"; s = "420"; f_m2[key1a][key2a] := s end + (* test_query_map_2 *) transition t5 () tname = "t5"; s = "420"; + (* Ensure f_m2[key1a][key2a] has value "420". *) key1a = "key1a"; key2a = "key2a"; val <- f_m2[key1a][key2a]; @@ -131,6 +150,7 @@ end | None => fail tname end; + (* Store data for next test. *) l_m2 = let e = Emp (String) (String) in let key2b = "key2b" in @@ -143,8 +163,13 @@ f_m2[key1b] := l_m2 end + (* test_query_map_2 *) transition t6 () tname = "t6"; + (* We now expect the storage to contain: *) + (* f_m2[key1a][key2a] : 420 *) + (* f_m3[key1b][key2b] : 840 *) + (* f_m2[key1b][key2c] : 841 *) key1a = "key1a"; key2a = "key2a"; c1 <- f_m2[key1a][key2a]; @@ -196,11 +221,15 @@ m = "key1b,key2c not found"; fail_msg tname m end; + (* Delete key1b for next test. *) delete f_m2[key1b] end + (* test_query_delete_to_empty *) transition t7 () tname = "t7"; + (* We now expect the storage to contain: *) + (* f_m2[key1a][key2a] : 420 *) key1a = "key1a"; key2a = "key2a"; c1 <- f_m2[key1a][key2a]; @@ -218,6 +247,7 @@ m = "key1a,key2a not found"; fail_msg tname m end; + (* And _not_ contain f_m2[key1b] *) key1b = "key1b"; c1 <- f_m2[key1b]; match c1 with @@ -226,6 +256,7 @@ fail_msg tname m | None => end; + (* and _not_ contain f_m2[key1b][key2b] *) key1b = "key1b"; key2b = "key2b"; c1 <- f_m2[key1b][key2b]; @@ -235,6 +266,7 @@ fail_msg tname m | None => end; + (* and _not_ contain f_m2[key1b][key2d] (which never existed) *) key1b = "key1b"; key2d = "key2d"; c1 <- f_m2[key1b][key2d]; @@ -244,14 +276,19 @@ fail_msg tname m | None => end; + (* Add f_m2[key1b][key2c] back again, with a different value. *) key1b = "key1b"; key2c = "key2c"; s = "121"; f_m2[key1b][key2c] := s end + (* test_query_map_2 *) transition t8 () tname = "t8"; + (* We now expect the storage to contain: *) + (* f_m2[key1a][key2a] : 420 *) + (* f_m2[key1b][key2c] : 121 *) key1a = "key1a"; key2a = "key2a"; c1 <- f_m2[key1a][key2a]; @@ -286,12 +323,15 @@ m = "key1b,key2c not found"; fail_msg tname m end; + (* For the next test, we replace f_m1 with an empty map. *) em = Emp (String) (String); f_m1 := em end + (* test_query_empty_map *) transition t9 () tname = "t9"; + (* Verify that f_m1 is empty. *) m1 <- f_m1; m1_size = builtin size m1; zero = Uint32 0; @@ -300,14 +340,18 @@ | True => | False => fail tname end; + (* Insert one key for next test. *) key1a = "key1a"; val = "420"; m1 = builtin put m1 key1a val; f_m1 := m1 end + (* test_query_delete_to_empty *) transition t10 () tname = "t10"; + (* We now expect the storage to contain: *) + (* f_m1[key1a] : 420 *) key1a = "key1a"; m1 <- f_m1; c1 = builtin get m1 key1a; @@ -325,11 +369,14 @@ m = "key1a not found"; fail_msg tname m end; + (* Delete key in a map to make it empty and then query the map *) delete f_m1[key1a] end + (* test_query_delete_to_empty *) transition t11 () tname = "t11"; + (* f_m1 should be empty. *) m1 <- f_m1; m1_size = builtin size m1; zero = Uint32 0; @@ -338,12 +385,15 @@ | True => | False => fail tname end; + (* Insert an empty map into f_m2 for next test. *) e2 = Emp (String) (Map String String); f_m2 := e2 end + (* test_query_empty_map_2 *) transition t12 () tname = "t12"; + (* f_m2 should be empty. *) m2 <- f_m2; m2_size = builtin size m2; zero = Uint32 0; @@ -352,13 +402,16 @@ | True => | False => fail tname end; + (* Insert f_m2[key1a] = Emp *) e1 = Emp (String) (String); key1a = "key1a"; f_m2[key1a] := e1 end + (* test_query_empty_map_2 *) transition t13 () tname = "t13"; + (* f_m2[key1a] must be empty *) key1a = "key1a"; mo <- f_m2[key1a]; match mo with @@ -374,6 +427,7 @@ end | None => fail tname end; + (* Insert entries for next test *) m3 = Emp (String) (String); m2 = let key2a = "key2a" in @@ -385,8 +439,10 @@ f_m3 := m3 end + (* test_query_empty_map_3 *) transition t14 () tname = "t14"; + (* f_m3 should be singleton *) m3 <- f_m3; m3_size = builtin size m3; one = Uint32 1; @@ -395,12 +451,15 @@ | True => | False => fail tname end; + (* Now insert something into f_m, whose name is a proper prefix of f_m3 *) e = Emp (String) (Map String String); f_m := e end + (* test_query_empty_map_3 *) transition t15 () tname = "t15"; + (* f_m3 should be [key1a][key2a] = [] *) m3 <- f_m3; m3_size = builtin size m3; one = Uint32 1; @@ -444,6 +503,7 @@ err = "Unexpected empty m2"; fail_msg tname err end; + (* For the next test, insert a non-empty nested map into f_m2 *) key1b = "key1b"; key2b = "key2b"; key1c = "key1c"; @@ -469,8 +529,14 @@ f_m2 := m2_full end + (* test_query_update_fetch_nested *) transition t16 () tname = "t16"; + (* Compare the entries *) + (* f_m2[key1a][key1a] = "420" *) + (* f_m2[key1b][key1b] = "421" *) + (* f_m2[key1c][key1c] = "422" *) + (* f_m2[key1d][key1d] = "423" *) key1a = "key1a"; key2a = "key2a"; key1b = "key1b"; @@ -512,6 +578,7 @@ | True => | False => fail tname end; + (* Insert an empty string key. *) m1 = let k = "" in let v = "420" in @@ -520,19 +587,26 @@ f_m1 := m1 end + (* test_query_empty_key *) transition t17 () tname = "t17"; + (* We now expect the storage to contain: *) + (* f_m1[""] : 420 *) key = ""; found <- exists f_m1[key]; match found with | True => | False => fail tname end; + (* delete key "" for next test *) delete f_m1[key] end + (* test_query_empty_key *) transition t18 () tname = "t18"; + (* We now expect the storage to NOT contain: *) + (* f_m1[""] *) key = ""; found <- exists f_m1[key]; match found with @@ -541,6 +615,7 @@ end end + (* Set field f_s1 and fail. *) transition f1 () tname = "f1"; s = "422"; @@ -548,6 +623,7 @@ expected_fail tname end + (* Check no change to f_s1. *) procedure p1 (tname : String) s <- f_s1; f_s1_original = "421"; @@ -560,15 +636,18 @@ end end + (* Ensure no change to f_s1 after f1 *) transition t19 () tname = "t19"; p1 tname end + (* A call back transition that fails. *) transition callback_expected_fail (tname : String) expected_fail tname end + (* Set field f_s1 and fail via chaincall to callback_expected_fail. *) transition f2 () tname = "f2"; s = "422"; @@ -584,11 +663,13 @@ send ms end + (* Ensure no change to f_s1 after f2. *) transition t20 () tname = "t20"; p1 tname end + (* Set f_m1["foo1"] and fail. *) transition f3 () tname = "f3"; key = "foo1"; @@ -597,6 +678,7 @@ expected_fail tname end + (* Ensure f_m1["foo1"] doesn't exist. *) procedure p2 (tname : String) key = "foo1"; found <- exists f_m1[key]; @@ -606,11 +688,13 @@ end end + (* Ensure f3 was reverted. *) transition t21 () tname = "t21"; p2 tname end + (* Set f_m1["foo1"] and fail via chaincall to callback_expected_fail. *) transition f4 () tname = "f4"; key = "foo1"; @@ -627,11 +711,13 @@ send ms end + (* Ensure f4 was reverted. *) transition t22 () tname = "t22"; p2 tname end + (* f_m2["key1a"]["key2a"] has a key, let's delete it and fail. *) transition f5 () tname = "f5"; key1 = "key1a"; @@ -640,6 +726,7 @@ expected_fail tname end + (* Ensure f_m2["key1a"]["key2a"] exists. *) procedure p3 (tname : String) key1 = "key1a"; key2 = "key2a"; @@ -656,11 +743,13 @@ end end + (* Ensure f5 was reverted. *) transition t23 () tname = "t23"; p3 tname end + (* f_m2["key1a"]["key2a"] has a key, let's delete it and fail via chaincall. *) transition f6 () tname = "f6"; key1 = "key1a"; @@ -677,6 +766,7 @@ send ms end + (* Ensure f6 was reverted. *) transition t24 () tname = "t24"; p3 tname diff --git a/tests/formatter/look_and_feel/mappair.t/run.t b/tests/formatter/look_and_feel/mappair.t/run.t index 4e87e4fb5..781792af4 100644 --- a/tests/formatter/look_and_feel/mappair.t/run.t +++ b/tests/formatter/look_and_feel/mappair.t/run.t @@ -69,10 +69,15 @@ transition addNumToList (num : Int64) p <- gpair; + (* get first of pair = List (Int64) *) l1 = fst_f p; + (* get second of pair = Option (Bool) *) b = snd_f p; + (* have fun: flip the boolean *) bflip = flip_obool b; + (* append num to the list *) l2 = Cons {(Int64)} num l1; + (* Form updated pair *) new_p = Pair {(List Int64) (Option Bool)} l2 bflip; gpair := new_p; len = let my_list_length = @list_length (Int64) in my_list_length l2; diff --git a/tests/formatter/look_and_feel/multiple-msgs.t/run.t b/tests/formatter/look_and_feel/multiple-msgs.t/run.t index 911efb616..26d8550ec 100644 --- a/tests/formatter/look_and_feel/multiple-msgs.t/run.t +++ b/tests/formatter/look_and_feel/multiple-msgs.t/run.t @@ -1,8 +1,12 @@ $ scilla-fmt multiple-msgs.scilla scilla_version 0 + (* HelloWorld contract *) import ListUtils + (***************************************************) + (* Associated library *) + (***************************************************) library HelloWorld let one_msg = @@ -11,6 +15,9 @@ Cons {(Message)} msg nil_msg + (***************************************************) + (* The contract definition *) + (***************************************************) contract HelloWorld () diff --git a/tests/formatter/look_and_feel/remote_state_reads.t/run.t b/tests/formatter/look_and_feel/remote_state_reads.t/run.t index 48c49190d..8b2b1bd48 100644 --- a/tests/formatter/look_and_feel/remote_state_reads.t/run.t +++ b/tests/formatter/look_and_feel/remote_state_reads.t/run.t @@ -3,6 +3,7 @@ library RRLib + (* Tests various aspects of address types and remote state reads *) type AddressADT = | Address1 of (ByStr20 with end) | Address2 of (ByStr20 with contract field admin : ByStr20 with end end) @@ -10,8 +11,11 @@ contract RRContract ( + (* Any address in use *) cparam1 : ByStr20 with end, + (* Any contract address *) cparam2 : ByStr20 with contract end, + (* Address with various fields *) cparam3 : ByStr20 with contract field admin : ByStr20 with end, @@ -52,35 +56,49 @@ field remote_reads_test_res_1_1 : Uint128 = Uint128 0 + (* _balance of remote1 *) field remote_reads_test_res_2_1 : Uint128 = Uint128 0 + (* _balance of remote2 *) field remote_reads_test_res_3_1 : Uint128 = Uint128 0 + (* _balance of remote3 *) field remote_reads_test_res_3_3 : Uint32 = Uint32 0 + (* transactionCount of remote3 *) field remote_reads_test_res_3_4 : ByStr20 with end = cparam3 + (* admin of remote3 *) field remote_reads_test_res_3_5 : Uint128 = Uint128 0 + (* _balance of admin of remote3 *) field remote_reads_test_res_3_6 : Map (ByStr20 with end) Bool = Emp (ByStr20 with end) (Bool) + (* owners of remote3 *) field remote_reads_test_res_3_7 : Bool = True + (* exists of owners[key] in remote3 *) field remote_reads_test_res_3_8 : Option Bool = let x = True in Some {(Bool)} x + (* owners[key] in remote3 *) field remote_reads_test_res_3_9 : Map Uint32 (Map (ByStr20 with end) Bool) = Emp (Uint32) (Map (ByStr20 with end) Bool) + (* signatures of remote3 *) field remote_reads_test_res_3_10 : Bool = False + (* exists of signatures[key] of remote3 *) field remote_reads_test_res_3_11 : Option (Map (ByStr20 with end) Bool) = None {(Map (ByStr20 with end) Bool)} + (* signatures[key] of remote3 *) field remote_reads_test_res_3_12 : Bool = False + (* exists signatures[key1][key2] of remote3 *) field remote_reads_test_res_3_13 : Option Bool = None {(Bool)} + (* signatures[key1][key2] of remote3 *) field sender_balance_pre : Uint128 = Uint128 0 field sender_balance_mid : Uint128 = Uint128 0 @@ -89,8 +107,11 @@ transition RemoteReadsTest ( + (* Any address in use *) remote1 : ByStr20 with end, + (* Any contract address *) remote2 : ByStr20 with contract end, + (* Address with various fields *) remote3 : ByStr20 with contract field admin : ByStr20 with end, @@ -130,6 +151,7 @@ remote_reads_test_res_3_13 := tmp_3_13 end + (* Test the dynamic typecheck of ADT values *) transition RemoteReadsADTTest ( list1 : List (ByStr20 with end), @@ -142,6 +164,8 @@ end + (* Test that outgoing messages and events use ByStr20 for type info, and not the full address type + Also test that this is the case for EventInfo *) transition OutgoingMsgTest () msg = { _tag : ""; _recipient : _sender; _amount : Uint128 0; param : cparam3 }; @@ -153,6 +177,7 @@ event e2 end + (* Test that exceptions use ByStr20 for type info, and not the full address type *) transition ExceptionTest () e = { _exception : "TestException"; value : cparam3 }; throw e @@ -175,12 +200,15 @@ assign_test_10[k1][k2] := x end + (* Check that sender balance is deducted on acceptance *) transition SenderBalanceTest () pre <-& _sender._balance; sender_balance_pre := pre; + (* First accept should cause sender balance to decrease *) accept; mid <-& _sender._balance; sender_balance_mid := mid; + (* Second accept should make no difference *) accept; post <-& _sender._balance; sender_balance_post := post diff --git a/tests/formatter/look_and_feel/replicate.t/run.t b/tests/formatter/look_and_feel/replicate.t/run.t index d47568542..75c2f0f04 100644 --- a/tests/formatter/look_and_feel/replicate.t/run.t +++ b/tests/formatter/look_and_feel/replicate.t/run.t @@ -29,6 +29,7 @@ transition cfdeploy_incorrect (cfaddr : ByStr20 with contract end) owner = _sender; + (* This is incorrect, max_block must be BNum. *) max_block = Uint32 100; goal = Uint128 1000; m = diff --git a/tests/formatter/look_and_feel/salarybot.t/run.t b/tests/formatter/look_and_feel/salarybot.t/run.t index b52ef2ee3..3187741a0 100644 --- a/tests/formatter/look_and_feel/salarybot.t/run.t +++ b/tests/formatter/look_and_feel/salarybot.t/run.t @@ -3,6 +3,9 @@ import ListUtils + (***************************************************) + (* Associated library *) + (***************************************************) library SalaryBotLib let mk_employee_already_exists_event = diff --git a/tests/formatter/look_and_feel/shogi.t/run.t b/tests/formatter/look_and_feel/shogi.t/run.t index 07866353d..da5179f06 100644 --- a/tests/formatter/look_and_feel/shogi.t/run.t +++ b/tests/formatter/look_and_feel/shogi.t/run.t @@ -1,5 +1,7 @@ $ scilla-fmt shogi.scilla scilla_version 0 + (* Import library rather than use contract library *) + (* to test that types are available *) import ShogiLib @@ -98,6 +100,7 @@ fun (origin : Square) => fun (direction : Direction) => fun (distance : Uint32) => + (* Convert to nat in order to perform recursion *) let distance_as_nat = builtin to_nat distance in let init = Nil {(Square)} in let folder = @nat_fold (List Square) in @@ -110,6 +113,7 @@ | Nil => origin end in + (* Check if we have moved off the board *) let off_the_board = match last_square with | Square row column => @@ -124,6 +128,7 @@ orb colum_fail row_fail end in + (* If we have gone off off the board we don't add to the path *) match off_the_board with | True => acc | False => @@ -145,12 +150,14 @@ fun (player_1_in_turn : Bool) => match player_1_in_turn with | True => + (* Attacking northwards *) match direction with | SouthWest => Nil {(Square)} | SouthEast => Nil {(Square)} | _ => let one = Uint32 1 in generate_path square direction one end | False => + (* Attacking southwards *) match direction with | NorthWest => Nil {(Square)} | NorthEast => Nil {(Square)} @@ -164,6 +171,7 @@ fun (player_1_in_turn : Bool) => match player_1_in_turn with | True => + (* Attacking northwards *) match direction with | South => Nil {(Square)} | East => Nil {(Square)} @@ -171,6 +179,7 @@ | _ => let one = Uint32 1 in generate_path square direction one end | False => + (* Attacking southwards *) match direction with | North => Nil {(Square)} | East => Nil {(Square)} @@ -183,8 +192,10 @@ fun (square : Square) => fun (direction : Direction) => fun (player_1_in_turn : Bool) => + (* Knights jump, so path only contains final square *) match player_1_in_turn with | True => + (* Attacking northwards *) let north = North in match direction with | NorthEast => @@ -200,6 +211,7 @@ | _ => Nil {(Square)} end | False => + (* Attacking southwards *) let south = South in match direction with | SouthEast => @@ -222,11 +234,13 @@ fun (player_1_in_turn : Bool) => match player_1_in_turn with | True => + (* Attacking northwards *) match direction with | North => let one = Uint32 1 in generate_path square direction one | _ => Nil {(Square)} end | False => + (* Attacking southwards *) match direction with | South => let one = Uint32 1 in generate_path square direction one | _ => Nil {(Square)} @@ -240,32 +254,40 @@ fun (player_1_in_turn : Bool) => match player_1_in_turn with | True => + (* Attacking northwards *) match direction with | North => generate_path square direction distance | _ => Nil {(Square)} end | False => + (* Attacking southwards *) match direction with | South => generate_path square direction distance | _ => Nil {(Square)} end end + (* Bishops and rooks *) let officer_path = fun (square : Square) => fun (direction : Direction) => fun (distance : Uint32) => generate_path square direction distance + (* Generate the path of squares that a piece moves along *) + (* The first element of the resulting list of squares is the target square of the move *) + (* An empty list indicates an illegal move *) let movement_path = fun (square : Square) => fun (piece : Piece) => fun (promotion_status : PromotionStatus) => fun (direction : Direction) => fun (distance : Uint32) => + (* Determines whether attacking northwards or southwards *) fun (player_1_in_turn : Bool) => match piece with | King => + (* Check distance *) let one = Uint32 1 in let distance_is_one = builtin eq one distance in match distance_is_one with @@ -273,6 +295,7 @@ | False => Nil {(Square)} end | GoldGeneral => + (* Check distance *) let one = Uint32 1 in let distance_is_one = builtin eq one distance in match distance_is_one with @@ -285,7 +308,9 @@ match distance_is_one with | True => match promotion_status with - | Promoted => gold_path square direction player_1_in_turn + | Promoted => + (* Promoted to gold general *) + gold_path square direction player_1_in_turn | NotPromoted => silver_path square direction player_1_in_turn end | False => Nil {(Square)} @@ -293,6 +318,7 @@ | Knight => match promotion_status with | Promoted => + (* Promoted to gold general *) let one = Uint32 1 in let distance_is_one = builtin eq one distance in match distance_is_one with @@ -300,6 +326,8 @@ | False => Nil {(Square)} end | NotPromoted => + (* Knights move 2 squares forward and 1 to the side. *) + (* Represented as NorthEast/NorthWest (for player 1) by 2 squares *) let two = Uint32 2 in let distance_is_two = builtin eq two distance in match distance_is_two with @@ -313,7 +341,9 @@ match distance_is_one with | True => match promotion_status with - | Promoted => gold_path square direction player_1_in_turn + | Promoted => + (* Promoted to gold general *) + gold_path square direction player_1_in_turn | NotPromoted => pawn_path square direction player_1_in_turn end | False => Nil {(Square)} @@ -321,6 +351,7 @@ | Lance => match promotion_status with | Promoted => + (* Promoted to gold general *) let one = Uint32 1 in let distance_is_one = builtin eq one distance in match distance_is_one with @@ -328,6 +359,7 @@ | False => Nil {(Square)} end | NotPromoted => + (* Lances move any number of squares forward. *) let zero = Uint32 0 in let distance_is_greater_that_zero = builtin lt zero distance in @@ -344,6 +376,7 @@ | NorthEast => officer_path square direction distance | NorthWest => officer_path square direction distance | _ => + (* Only allowed if bishop is promoted *) match promotion_status with | NotPromoted => Nil {(Square)} | Promoted => @@ -362,6 +395,7 @@ | East => officer_path square direction distance | North => officer_path square direction distance | _ => + (* Only allowed if rook is promoted *) match promotion_status with | NotPromoted => Nil {(Square)} | Promoted => @@ -382,14 +416,22 @@ fun (target_row : Uint32) => fun (player_1_in_turn : Bool) => match promote with - | False => Some {(PromotionStatus)} promotion_status + | False => + (* No attempt made to promote *) + Some {(PromotionStatus)} promotion_status | True => + (* Attempt to promote *) match promotion_status with - | Promoted => None {(PromotionStatus)} + | Promoted => + (* Cannot promote an already promoted piece *) + None {(PromotionStatus)} | NotPromoted => + (* Check that move happened in opponent territory *) match player_1_in_turn with | True => + (* Move must occur on row 7 or higher *) let seven = Uint32 7 in + (* Attacking northwards *) let origin_not_in_opponent_territory = builtin lt origin_row seven in @@ -401,11 +443,15 @@ origin_not_in_opponent_territory target_not_in_opponent_territory in match not_in_opponent_territory with - | True => None {(PromotionStatus)} + | True => + (* Cannot promote piece outside of opponent territory *) + None {(PromotionStatus)} | False => Some {(PromotionStatus)} promoted end | False => + (* Move must occur on row 3 or lower *) let three = Uint32 3 in + (* Attacking northwards *) let origin_not_in_opponent_territory = builtin lt three origin_row in @@ -417,7 +463,9 @@ origin_not_in_opponent_territory target_not_in_opponent_territory in match not_in_opponent_territory with - | True => None {(PromotionStatus)} + | True => + (* Cannot promote piece outside of opponent territory *) + None {(PromotionStatus)} | False => Some {(PromotionStatus)} promoted end end @@ -438,6 +486,7 @@ let internal_error = InternalError + (* Error events *) let mk_error_event = fun (err : Error) => let err_code = @@ -481,16 +530,20 @@ ) + (* Initialize board *) field board : Map Uint32 (Map Uint32 SquareContents) = initial_board player1 player2 field captured_pieces : Map ByStr20 (Map Uint32 Uint32) = init_captured_pieces player1 player2 + (* player1 moves first *) + (* player_in_turn = None indicates that game is over *) field player_in_turn : Option ByStr20 = Some {(ByStr20)} player1 field winner : Option ByStr20 = None {(ByStr20)} + (* Execute Move action by sending message to execute PlayerAction transition *) transition MoveAction ( row : Uint32, @@ -514,12 +567,14 @@ send msgs end + (* Execute player action *) transition PlayerAction (action : Action) false = False; true = True; current_player_opt <- player_in_turn; match current_player_opt with | None => + (* Game is over *) err = game_is_over; e = mk_error_event err; event e @@ -532,17 +587,21 @@ event e | True => match action with - | Resign => + | (* Resign and award game to opponent *) + Resign => opponent = get_next_player current_player player1 player2; none = None {(ByStr20)}; player_in_turn := none; some_opponent = Some {(ByStr20)} opponent; winner := some_opponent | Place piece (Square row column) => + (* Place a captured piece on the board *) + (* Check that player has captured piece available *) piece_no = piece_to_int piece; capture_count <- captured_pieces[_sender][piece_no]; match capture_count with | None => + (* This should not happen *) none_player = None {(ByStr20)}; player_in_turn := none_player; err = internal_error; @@ -557,15 +616,18 @@ e = mk_error_event err; event e | True => + (* Check if desired square is available *) target_square_content <- board[row][column]; match target_square_content with | Some Free => + (* Remove from captured pieces, and place on board *) one = Uint32 1; new_count = builtin sub count one; captured_pieces[_sender][piece_no] := new_count; new_contents = Occupied piece not_promoted _sender; board[row][column] := new_contents | _ => + (* Square does not exist on board, or square is occupied *) err = illegal_action; e = mk_error_event err; event e @@ -575,6 +637,7 @@ | Move square direction distance promote => match square with | Square row column => + (* Find the contents of the origin square *) contents <- board[row][column]; match contents with | Some (Occupied piece promotion_status owner) => @@ -595,6 +658,7 @@ e = mk_error_event err; event e | Cons (Square target_row target_column) intervening_squares => + (* Piece is allowed to move as requested. Check for blocking pieces. *) board_tmp <- board; blocked_path = let exister = @list_exists (Square) in @@ -622,57 +686,75 @@ e = mk_error_event err; event e | False => + (* Check contents of target square *) contents_at_target <- board[target_row][target_column]; match contents_at_target with | None => + (* Moving off the board *) err = illegal_action; e = mk_error_event err; event e | Some Free => + (* No piece captured *) + (* Check promotion part of move *) new_promotion_status_opt = perform_promotion promote promotion_status row target_row player_1_moves; match new_promotion_status_opt with | None => + (* Illegal promotion *) err = illegal_action; e = mk_error_event err; event e | Some new_promotion_status => + (* Move piece *) + (* Source square is no longer occupied *) board[row][column] := free; + (* Update target square *) new_contents_at_target = Occupied piece new_promotion_status current_player; board[target_row][target_column] := new_contents_at_target end | Some (Occupied captured_piece _ captured_owner) => + (* Target square is occupied. Check ownership *) captured_owner_is_current_player = builtin eq captured_owner current_player; match captured_owner_is_current_player with | True => + (* Target square is blocked *) err = illegal_action; e = mk_error_event err; event e | False => + (* Opponent piece captured. *) + (* Check promotion part of move *) new_promotion_status_opt = perform_promotion promote promotion_status row target_row player_1_moves; match new_promotion_status_opt with | None => + (* Illegal promotion *) err = illegal_action; e = mk_error_event err; event e | Some new_promotion_status => + (* Move own piece *) board[row][column] := free; + (* Update target square *) new_contents_at_target = Occupied piece new_promotion_status current_player; board[target_row][target_column] := new_contents_at_target; + (* Check if captured piece is the king *) match captured_piece with | King => + (* Game is won *) none = None {(ByStr20)}; player_in_turn := none; some_current_player = Some {(ByStr20)} current_player; winner := some_current_player | _ => + (* Add captured piece to list of captured pieces *) captured_piece_no = piece_to_int captured_piece; captured_count_opt <- captured_pieces[current_player][captured_piece_no]; @@ -695,6 +777,7 @@ end end | _ => + (* No piece on the square, or square does not exist *) err = illegal_action; e = mk_error_event err; event e @@ -702,12 +785,15 @@ end end end; + (* Check if a winner has been found *) win <- winner; match win with | Some player => + (* Game is over. Announce winner *) e = mk_winner_event player player1 player2; event e | None => + (* Set player_in_turn to opposite player *) next_player = get_next_player current_player player1 player2; next_player_opt = Some {(ByStr20)} next_player; player_in_turn := next_player_opt diff --git a/tests/formatter/look_and_feel/shogi_proc.t/run.t b/tests/formatter/look_and_feel/shogi_proc.t/run.t index ff2eb022c..8950e8bcd 100644 --- a/tests/formatter/look_and_feel/shogi_proc.t/run.t +++ b/tests/formatter/look_and_feel/shogi_proc.t/run.t @@ -1,5 +1,7 @@ $ scilla-fmt shogi_proc.scilla scilla_version 0 + (* Import library rather than use contract library *) + (* to test that types are available *) import ShogiLib @@ -98,6 +100,7 @@ fun (origin : Square) => fun (direction : Direction) => fun (distance : Uint32) => + (* Convert to nat in order to perform recursion *) let distance_as_nat = builtin to_nat distance in let init = Nil {(Square)} in let folder = @nat_fold (List Square) in @@ -110,6 +113,7 @@ | Nil => origin end in + (* Check if we have moved off the board *) let off_the_board = match last_square with | Square row column => @@ -124,6 +128,7 @@ orb colum_fail row_fail end in + (* If we have gone off off the board we don't add to the path *) match off_the_board with | True => acc | False => @@ -145,12 +150,14 @@ fun (player_1_in_turn : Bool) => match player_1_in_turn with | True => + (* Attacking northwards *) match direction with | SouthWest => Nil {(Square)} | SouthEast => Nil {(Square)} | _ => let one = Uint32 1 in generate_path square direction one end | False => + (* Attacking southwards *) match direction with | NorthWest => Nil {(Square)} | NorthEast => Nil {(Square)} @@ -164,6 +171,7 @@ fun (player_1_in_turn : Bool) => match player_1_in_turn with | True => + (* Attacking northwards *) match direction with | South => Nil {(Square)} | East => Nil {(Square)} @@ -171,6 +179,7 @@ | _ => let one = Uint32 1 in generate_path square direction one end | False => + (* Attacking southwards *) match direction with | North => Nil {(Square)} | East => Nil {(Square)} @@ -183,8 +192,10 @@ fun (square : Square) => fun (direction : Direction) => fun (player_1_in_turn : Bool) => + (* Knights jump, so path only contains final square *) match player_1_in_turn with | True => + (* Attacking northwards *) let north = North in match direction with | NorthEast => @@ -200,6 +211,7 @@ | _ => Nil {(Square)} end | False => + (* Attacking southwards *) let south = South in match direction with | SouthEast => @@ -222,11 +234,13 @@ fun (player_1_in_turn : Bool) => match player_1_in_turn with | True => + (* Attacking northwards *) match direction with | North => let one = Uint32 1 in generate_path square direction one | _ => Nil {(Square)} end | False => + (* Attacking southwards *) match direction with | South => let one = Uint32 1 in generate_path square direction one | _ => Nil {(Square)} @@ -240,32 +254,40 @@ fun (player_1_in_turn : Bool) => match player_1_in_turn with | True => + (* Attacking northwards *) match direction with | North => generate_path square direction distance | _ => Nil {(Square)} end | False => + (* Attacking southwards *) match direction with | South => generate_path square direction distance | _ => Nil {(Square)} end end + (* Bishops and rooks *) let officer_path = fun (square : Square) => fun (direction : Direction) => fun (distance : Uint32) => generate_path square direction distance + (* Generate the path of squares that a piece moves along *) + (* The first element of the resulting list of squares is the target square of the move *) + (* An empty list indicates an illegal move *) let movement_path = fun (square : Square) => fun (piece : Piece) => fun (promotion_status : PromotionStatus) => fun (direction : Direction) => fun (distance : Uint32) => + (* Determines whether attacking northwards or southwards *) fun (player_1_in_turn : Bool) => match piece with | King => + (* Check distance *) let one = Uint32 1 in let distance_is_one = builtin eq one distance in match distance_is_one with @@ -273,6 +295,7 @@ | False => Nil {(Square)} end | GoldGeneral => + (* Check distance *) let one = Uint32 1 in let distance_is_one = builtin eq one distance in match distance_is_one with @@ -285,7 +308,9 @@ match distance_is_one with | True => match promotion_status with - | Promoted => gold_path square direction player_1_in_turn + | Promoted => + (* Promoted to gold general *) + gold_path square direction player_1_in_turn | NotPromoted => silver_path square direction player_1_in_turn end | False => Nil {(Square)} @@ -293,6 +318,7 @@ | Knight => match promotion_status with | Promoted => + (* Promoted to gold general *) let one = Uint32 1 in let distance_is_one = builtin eq one distance in match distance_is_one with @@ -300,6 +326,8 @@ | False => Nil {(Square)} end | NotPromoted => + (* Knights move 2 squares forward and 1 to the side. *) + (* Represented as NorthEast/NorthWest (for player 1) by 2 squares *) let two = Uint32 2 in let distance_is_two = builtin eq two distance in match distance_is_two with @@ -313,7 +341,9 @@ match distance_is_one with | True => match promotion_status with - | Promoted => gold_path square direction player_1_in_turn + | Promoted => + (* Promoted to gold general *) + gold_path square direction player_1_in_turn | NotPromoted => pawn_path square direction player_1_in_turn end | False => Nil {(Square)} @@ -321,6 +351,7 @@ | Lance => match promotion_status with | Promoted => + (* Promoted to gold general *) let one = Uint32 1 in let distance_is_one = builtin eq one distance in match distance_is_one with @@ -328,6 +359,7 @@ | False => Nil {(Square)} end | NotPromoted => + (* Lances move any number of squares forward. *) let zero = Uint32 0 in let distance_is_greater_that_zero = builtin lt zero distance in @@ -344,6 +376,7 @@ | NorthEast => officer_path square direction distance | NorthWest => officer_path square direction distance | _ => + (* Only allowed if bishop is promoted *) match promotion_status with | NotPromoted => Nil {(Square)} | Promoted => @@ -362,6 +395,7 @@ | East => officer_path square direction distance | North => officer_path square direction distance | _ => + (* Only allowed if rook is promoted *) match promotion_status with | NotPromoted => Nil {(Square)} | Promoted => @@ -382,14 +416,22 @@ fun (target_row : Uint32) => fun (player_1_in_turn : Bool) => match promote with - | False => Some {(PromotionStatus)} promotion_status + | False => + (* No attempt made to promote *) + Some {(PromotionStatus)} promotion_status | True => + (* Attempt to promote *) match promotion_status with - | Promoted => None {(PromotionStatus)} + | Promoted => + (* Cannot promote an already promoted piece *) + None {(PromotionStatus)} | NotPromoted => + (* Check that move happened in opponent territory *) match player_1_in_turn with | True => + (* Move must occur on row 7 or higher *) let seven = Uint32 7 in + (* Attacking northwards *) let origin_not_in_opponent_territory = builtin lt origin_row seven in @@ -401,11 +443,15 @@ origin_not_in_opponent_territory target_not_in_opponent_territory in match not_in_opponent_territory with - | True => None {(PromotionStatus)} + | True => + (* Cannot promote piece outside of opponent territory *) + None {(PromotionStatus)} | False => Some {(PromotionStatus)} promoted end | False => + (* Move must occur on row 3 or lower *) let three = Uint32 3 in + (* Attacking northwards *) let origin_not_in_opponent_territory = builtin lt three origin_row in @@ -417,7 +463,9 @@ origin_not_in_opponent_territory target_not_in_opponent_territory in match not_in_opponent_territory with - | True => None {(PromotionStatus)} + | True => + (* Cannot promote piece outside of opponent territory *) + None {(PromotionStatus)} | False => Some {(PromotionStatus)} promoted end end @@ -438,6 +486,7 @@ let internal_error = InternalError + (* Error events *) let mk_error_event = fun (err : Error) => let err_code = @@ -481,12 +530,15 @@ ) + (* Initialize board *) field board : Map Uint32 (Map Uint32 SquareContents) = initial_board player1 player2 field captured_pieces : Map ByStr20 (Map Uint32 Uint32) = init_captured_pieces player1 player2 + (* player1 moves first *) + (* player_in_turn = None indicates that game is over *) field player_in_turn : Option ByStr20 = Some {(ByStr20)} player1 field winner : Option ByStr20 = None {(ByStr20)} @@ -518,27 +570,35 @@ end procedure PlacePiece (piece : Piece, square : Square) + (* Place a captured piece on the board *) + (* Check that player has captured piece available *) piece_no = piece_to_int piece; capture_count <- captured_pieces[_sender][piece_no]; match capture_count with - | None => InternalErrorEvent + | None => + (* This should not happen *) + InternalErrorEvent | Some count => zero = Uint32 0; has_pieces = builtin lt zero count; match has_pieces with | False => IllegalActionEvent | True => + (* Check if desired square is available *) match square with | Square row column => target_square_content <- board[row][column]; match target_square_content with | Some Free => + (* Remove from captured pieces, and place on board *) one = Uint32 1; new_count = builtin sub count one; captured_pieces[_sender][piece_no] := new_count; new_contents = Occupied piece not_promoted _sender; board[row][column] := new_contents - | _ => IllegalActionEvent + | _ => + (* Square does not exist on board, or square is occupied *) + IllegalActionEvent end end end @@ -560,9 +620,14 @@ new_promotion_status_opt = perform_promotion promote promotion_status row target_row player_1_moves; match new_promotion_status_opt with - | None => IllegalActionEvent + | None => + (* Illegal promotion *) + IllegalActionEvent | Some new_promotion_status => + (* Move piece *) + (* Source square is no longer occupied *) board[row][column] := free; + (* Update target square *) new_contents_at_target = Occupied piece new_promotion_status current_player; board[target_row][target_column] := new_contents_at_target end @@ -578,6 +643,7 @@ ) match square with | Square row column => + (* Find the contents of the origin square *) contents <- board[row][column]; match contents with | Some (Occupied piece promotion_status owner) => @@ -592,6 +658,7 @@ match path with | Nil => IllegalActionEvent | Cons (Square target_row target_column) intervening_squares => + (* Piece is allowed to move as requested. Check for blocking pieces. *) board_tmp <- board; blocked_path = let exister = @list_exists (Square) in @@ -616,23 +683,37 @@ match blocked_path with | True => IllegalActionEvent | False => + (* Check contents of target square *) contents_at_target <- board[target_row][target_column]; match contents_at_target with - | None => IllegalActionEvent + | None => + (* Moving off the board *) + IllegalActionEvent | Some Free => + (* No piece captured *) + (* Check promotion, and move *) PerformMoveAndPromote current_player piece promote promotion_status row column target_row target_column player_1_moves | Some (Occupied captured_piece _ captured_owner) => + (* Target square is occupied. Check ownership *) captured_owner_is_current_player = builtin eq captured_owner current_player; match captured_owner_is_current_player with - | True => IllegalActionEvent + | True => + (* Target square is blocked *) + IllegalActionEvent | False => + (* Opponent piece captured. *) + (* Check promotion part of move *) PerformMoveAndPromote current_player piece promote promotion_status row column target_row target_column player_1_moves; + (* Check if captured piece is the king *) match captured_piece with - | King => Winner current_player + | King => + (* Game is won *) + Winner current_player | _ => + (* Add captured piece to list of captured pieces *) captured_piece_no = piece_to_int captured_piece; captured_count_opt <- captured_pieces[current_player][captured_piece_no]; @@ -650,11 +731,14 @@ end end end - | _ => IllegalActionEvent + | _ => + (* No piece on the square, or square does not exist *) + IllegalActionEvent end end end + (* Execute Move action by sending message to execute PlayerAction transition *) transition MoveAction ( row : Uint32, @@ -678,12 +762,14 @@ send msgs end + (* Execute player action *) transition PlayerAction (action : Action) false = False; true = True; current_player_opt <- player_in_turn; match current_player_opt with | None => + (* Game is over *) err = game_is_over; e = mk_error_event err; event e @@ -696,18 +782,23 @@ event e | True => match action with - | Resign => Resign current_player + | (* Resign and award game to opponent *) + Resign => + Resign current_player | Place piece square => PlacePiece piece square | Move square direction distance promote => MovePiece current_player square direction distance promote end end; + (* Check if a winner has been found *) win <- winner; match win with | Some player => + (* Game is over. Announce winner *) e = mk_winner_event player player1 player2; event e | None => + (* Set player_in_turn to opposite player *) next_player = get_next_player current_player player1 player2; next_player_opt = Some {(ByStr20)} next_player; player_in_turn := next_player_opt diff --git a/tests/formatter/look_and_feel/simple-dex-remote-reads.t/run.t b/tests/formatter/look_and_feel/simple-dex-remote-reads.t/run.t index 2be2d6322..12a0eef99 100644 --- a/tests/formatter/look_and_feel/simple-dex-remote-reads.t/run.t +++ b/tests/formatter/look_and_feel/simple-dex-remote-reads.t/run.t @@ -1,10 +1,13 @@ $ scilla-fmt simple-dex-remote-reads.scilla scilla_version 0 + (* This contract is only used in the documentation at scilla.readthedocs.io. + No tests are run as part of our test suite *) import IntUtils library SimpleExchangeLib + (* Order placer, sell token, sell amount, buy token, buy amount *) type Order = | Order of ByStr20 @@ -17,6 +20,8 @@ end) Uint128 + + (* Helper values and functions *) let true = True let false = False @@ -53,7 +58,8 @@ _recipient : token_address; _tag : tag; _amount : Uint128 0; - from : from; + from : (* No Zil are transferred, only custom tokens *) + from; to : to; amount : amount } @@ -64,7 +70,9 @@ fun (from : ByStr20) => fun (to : ByStr20) => fun (amount : Uint128) => + (* Construct a TransferFrom messsage to transfer from seller's allowance to exhange *) let msg = mk_transfer_msg true token_address from to amount in + (* Create a singleton list *) one_msg msg let mk_make_order_msgs : @@ -83,22 +91,48 @@ fun (this_address : ByStr20) => fun (order_placer : ByStr20) => fun (order_maker : ByStr20) => + (* Construct a Transfer messsage to transfer from exchange to maker *) let sell_msg = mk_transfer_msg false token_sell_address this_address order_maker sell_amount in + (* Construct a TransferFrom messsage to transfer from maker to placer *) let buy_msg = mk_transfer_msg true token_buy_address order_maker order_placer buy_amount in + (* Create a singleton list *) two_msgs sell_msg buy_msg - contract SimpleExchange (initial_admin : ByStr20 with end) + contract SimpleExchange + ( + (* Ensure that the initial admin is an address that is in use *) + initial_admin : ByStr20 with end + ) + (* Active admin. *) + (* NOTE: We don't need to read any fields from the admin *) + (* address, so we could have chosen ByStr20 as the field type. This could *) + (* have been done without changing the type of initial_admin or the *) + (* new_admin transition parameter, because ByStr20 with end is a subtype *) + (* of ByStr20, which means that a value of type ByStr20 with end can be *) + (* used when a ByStr20 is expected. initial_admin is checked to be in use *) + (* when the contract is deployed, and new_admin transition parameter is *) + (* checked to be in use when the SetAdmin transition is invoked, so we *) + (* can still be sure that we don't accidentally set an admin field to an *) + (* address that is not in use. *) + (* *) + (* The advantage of choosing ByStr20 with end as the field type is that *) + (* we don't accidentally set the admin address to an unchecked ByStr20 in *) + (* some other part of the code by mistake. *) field admin : ByStr20 with end = initial_admin + (* Tokens listed on the exchange. *) + (* We identify the token by its exchange code, and map it to the address *) + (* of the contract implementing the token. The contract at that address must *) + (* contain an allowances field that we can remote read. *) field listed_tokens : Map String @@ -111,8 +145,10 @@ field allowances : Map ByStr20 (Map ByStr20 Uint128) end) + (* Active orders, identified by the order number *) field active_orders : Map Uint128 Order = Emp (Uint128) (Order) + (* The order number to use when the next order is placed *) field next_order_no : Uint128 = zero procedure ThrowListingStatusException @@ -139,30 +175,45 @@ throw e end + (* Check that _sender is the active admin. *) + (* If not, throw an error and abort the transaction *) procedure CheckSenderIsAdmin () current_admin <- admin; is_admin = builtin eq _sender current_admin; match is_admin with - | True => + | True => (* Nothing to do *) | False => + (* Construct an exception object and throw it *) e = { _exception : "SenderIsNotAdmin" }; throw e end end + (* Change the active admin *) + (* NOTE: Only the former admin is allowed to appoint a new admin *) transition SetAdmin (new_admin : ByStr20 with end) + (* Only the former admin may appoint a new admin *) CheckSenderIsAdmin; admin := new_admin end + (* Check that a given token code is not already listed. If it is, throw an error. *) procedure CheckIsTokenUnlisted (token_code : String) + (* Is the token code listed? *) token_code_is_listed <- exists listed_tokens[token_code]; match token_code_is_listed with - | True => ThrowListingStatusException token_code false token_code_is_listed - | False => + | True => + (* Incorrect listing status *) + ThrowListingStatusException token_code false token_code_is_listed + | False => (* Nothing to do *) end end + (* List a new token on the exchange. Only the admin may list new tokens. *) + (* If a token code is already in use, raise an error *) + (* NOTE: The token address must have an allowances field. If the supplied *) + (* address does not contain such a field, the transition fails, and the *) + (* transaction aborts. *) transition ListToken ( token_code : String, @@ -171,11 +222,15 @@ field allowances : Map ByStr20 (Map ByStr20 Uint128) end ) + (* Only the admin may list new tokens. *) CheckSenderIsAdmin; + (* Only new token codes are allowed. *) CheckIsTokenUnlisted token_code; + (* Everything is ok. The token can be listed *) listed_tokens[token_code] := new_token end + (* Check that the sender has allowed access to sufficient funds *) procedure CheckAllowance ( token : @@ -185,6 +240,7 @@ expected : Uint128 ) actual_opt <-& token.allowances[_sender][_this_address]; + (* Find actual allowance. Use 0 if None is given *) actual = match actual_opt with | Some x => x @@ -192,18 +248,22 @@ end; is_sufficient = uint128_le expected actual; match is_sufficient with - | True => + | True => (* Nothing to do *) | False => ThrowInsufficientAllowanceException token expected actual end end procedure AddOrder (order : Order) + (* Get the next order number *) order_no <- next_order_no; + (* Add the order *) active_orders[order_no] := order; + (* Update the next_order_no field *) new_order_no = builtin add order_no one; next_order_no := new_order_no end + (* Place an order on the exchange *) transition PlaceOrder ( token_code_sell : String, @@ -211,20 +271,29 @@ token_code_buy : String, buy_amount : Uint128 ) + (* Check that the tokens are listed *) token_sell_opt <- listed_tokens[token_code_sell]; token_buy_opt <- listed_tokens[token_code_buy]; match token_sell_opt with | Some token_sell => match token_buy_opt with | Some token_buy => + (* Check that the placer has allowed sufficient funds to be accessed *) CheckAllowance token_sell sell_amount; + (* Transfer the sell tokens to the exchange for holding. Construct a TransferFrom message to the token contract. *) msg = mk_place_order_msg token_sell _sender _this_address sell_amount; + (* Send message when the transition completes. *) send msg; + (* Create order and add to list of active orders *) order = Order _sender token_sell sell_amount token_buy buy_amount; AddOrder order - | None => ThrowListingStatusException token_code_buy true false + | None => + (* Unlisted token *) + ThrowListingStatusException token_code_buy true false end - | None => ThrowListingStatusException token_code_sell true false + | None => + (* Unlisted token *) + ThrowListingStatusException token_code_sell true false end end @@ -232,11 +301,14 @@ order <- active_orders[order_id]; match order with | Some (Order order_placer sell_token sell_amount buy_token buy_amount) => + (* Check that the placer has allowed sufficient funds to be accessed *) CheckAllowance buy_token buy_amount; + (* Create the two transfer messages and send them *) msgs = mk_make_order_msgs sell_token sell_amount buy_token buy_amount _this_address order_placer _sender; send msgs; + (* Order has now been matched, so remove it *) delete active_orders[order_id] | None => e = { _exception : "UnknownOrder"; order_id : order_id }; @@ -247,7 +319,7 @@ procedure CheckInitiator (initiator : ByStr20) initiator_is_this = builtin eq initiator _this_address; match initiator_is_this with - | True => + | True => (* Do nothing *) | False => e = { @@ -261,16 +333,19 @@ transition RecipientAcceptTransferFrom (initiator : ByStr20, sender : ByStr20, recipient : ByStr20, amount : Uint128) + (* The exchange only accepts transfers that it itself has initiated. *) CheckInitiator initiator end transition TransferFromSuccessCallBack (initiator : ByStr20, sender : ByStr20, recipient : ByStr20, amount : Uint128) + (* The exchange only accepts transfers that it itself has initiated. *) CheckInitiator initiator end transition TransferSuccessCallBack (initiator : ByStr20, sender : ByStr20, recipient : ByStr20, amount : Uint128) + (* The exchange only accepts transfers that it itself has initiated. *) CheckInitiator initiator end diff --git a/tests/formatter/look_and_feel/simple-dex.t/run.t b/tests/formatter/look_and_feel/simple-dex.t/run.t index f35816093..d154edb57 100644 --- a/tests/formatter/look_and_feel/simple-dex.t/run.t +++ b/tests/formatter/look_and_feel/simple-dex.t/run.t @@ -3,24 +3,32 @@ import PairUtils + (* Simple DEX : P2P Token Trades *) + (* Disclaimer: This contract is experimental and meant for testing purposes only *) + (* DO NOT USE THIS CONTRACT IN PRODUCTION *) library SimpleDex + (* Pair helpers *) let getAddressFromPair = @fst (ByStr20) (Uint128) let getValueFromPair = @snd (ByStr20) (Uint128) + (* Event for errors *) let make_error_event = fun (location : String) => fun (msg : String) => { _eventname : "Error"; raisedAt : location; message : msg } + (* Order = { tokenA, valueA, tokenB, valueB } *) type Order = | Order of ByStr20 Uint128 ByStr20 Uint128 + (* Create an orderID based on the hash of the parameters *) let createOrderId = fun (order : Order) => builtin sha256hash order + (* Create one transaction message *) let transaction_msg = fun (recipient : ByStr20) => fun (tag : String) => @@ -36,6 +44,7 @@ tokens : transferAmt } + (* Wrap one transaction message as singleton list *) let transaction_msg_as_list = fun (recipient : ByStr20) => fun (tag : String) => @@ -53,6 +62,9 @@ in one_msg msg + (* Compute the new pending return val *) + (* If no existing records are found, return `incomingTokensAmt` *) + (* else, return `incomingTokenAmt` + existing value *) let computePendingReturnsVal = fun (prevVal : Option Uint128) => fun (incomingTokensAmt : Uint128) => @@ -62,17 +74,29 @@ end + (***************************************************) + (* The contract definition *) + (***************************************************) contract SimpleDex (contractOwner : ByStr20) + (* Orderbook: mapping (orderIds => ( (tokenA, valueA) (tokenB, valueB) )) *) + (* @param: tokenA: Contract address of token A *) + (* @param: valueA: total units of token A offered by maker *) + (* @param: tokenB: Contract address of token B *) + (* @param: valueB: total units of token B requsted by maker *) field orderbook : Map ByStr32 Order = Emp (ByStr32) (Order) + (* Order info stores the mapping ( orderId => (tokenOwnerAddress, expirationBlock)) *) field orderInfo : Map ByStr32 (Pair ByStr20 BNum) = Emp (ByStr32) (Pair ByStr20 BNum) + (* Ledger of how much the _sender can claim from the contract *) + (* mapping ( walletAddress => mapping (tokenContracts => amount) ) *) field pendingReturns : Map ByStr20 (Map ByStr20 Uint128) = Emp (ByStr20) (Map ByStr20 Uint128) + (* Maker creates an order to exchange valueA of tokenA for valueB of tokenB *) transition makeOrder ( tokenA : ByStr20, @@ -88,13 +112,16 @@ builtin blt minExpiration expirationBlock; match validExpirationBlock with | True => + (* Creates a new order *) newOrder = Order tokenA valueA tokenB valueB; orderId = createOrderId newOrder; orderbook[orderId] := newOrder; + (* Updates orderInfo with maker's address and expiration blocknumber *) p = Pair {(ByStr20) (BNum)} _sender expirationBlock; orderInfo[orderId] := p; e = { _eventname : "Order Created"; hash : orderId }; event e; + (* Transfer tokens from _sender to the contract address *) msgs = let tag = "TransferFrom" in let zero = Uint128 0 in @@ -111,10 +138,12 @@ end end + (* Taker fills an order *) transition fillOrder (orderId : ByStr32) getOrder <- orderbook[orderId]; match getOrder with | Some (Order tokenA valueA tokenB valueB) => + (* Check the expiration block *) optionOrderInfo <- orderInfo[orderId]; match optionOrderInfo with | Some info => @@ -128,16 +157,19 @@ makerAddr = let getMakerAddr = @fst (ByStr20) (BNum) in getMakerAddr info; + (* Updates taker with the tokens that he is entitled to claim *) prevVal <- pendingReturns[_sender][tokenA]; takerAmt = computePendingReturnsVal prevVal valueA; pendingReturns[_sender][tokenA] := takerAmt; prevVal_1 <- pendingReturns[makerAddr][tokenB]; makerAmt = computePendingReturnsVal prevVal_1 valueB; pendingReturns[makerAddr][tokenB] := makerAmt; + (* Delete orders from the orderbook and orderinfo *) delete orderInfo[orderId]; delete orderbook[orderId]; e = { _eventname : "Order Filled"; hash : orderId }; event e; + (* Transfer tokens from _sender to the contract address *) msgs = let tag = "TransferFrom" in transaction_msg_as_list tokenB tag _sender _this_address valueB; @@ -167,6 +199,7 @@ end end + (* Allows users to claim back their tokens from the smart contract *) transition ClaimBack (token : ByStr20) getAmtOutstanding <- pendingReturns[_sender][token]; match getAmtOutstanding with @@ -180,6 +213,7 @@ amt : amtOutstanding }; event e; + (* Transfer tokens from _sender to the contract address *) msgs = let tag = "TransferFrom" in transaction_msg_as_list token tag _this_address _sender amtOutstanding; @@ -194,6 +228,7 @@ end end + (* Maker can cancel his order *) transition cancelOrder (orderId : ByStr32) getOrderInfo <- orderInfo[orderId]; match getOrderInfo with @@ -204,17 +239,22 @@ checkSender = builtin eq makerAddr _sender; match checkSender with | True => + (* Sender is the maker, proceed with cancellation *) fetchOrder <- orderbook[orderId]; match fetchOrder with | Some (Order tokenA valueA _ _) => + (* Updates taker with the tokens that he is entitled to claim *) prevVal <- pendingReturns[_sender][tokenA]; takerAmt = computePendingReturnsVal prevVal valueA; pendingReturns[_sender][tokenA] := takerAmt; + (* Delete orders from the orderbook and orderinfo *) delete orderInfo[orderId]; delete orderbook[orderId]; e = { _eventname : "Cancel order successful"; hash : orderId }; event e - | None => + | (* @note: For consistency, we use claimback instead of sending the tokens *) + (* back to the maker *) + None => e = let func = "cancelOrder" in let error_msg = "OrderID not found" in @@ -222,6 +262,7 @@ event e end | False => + (* Unauthorized transaction *) e = let func = "cancelOrder" in let error_msg = "Sender is not maker of the order" in @@ -229,6 +270,7 @@ event e end | None => + (* Order ID not found *) e = let func = "cancelOrder" in let error_msg = "OrderID not found" in diff --git a/tests/formatter/look_and_feel/timestamp.t/run.t b/tests/formatter/look_and_feel/timestamp.t/run.t index 8d03ac426..178fde8ed 100644 --- a/tests/formatter/look_and_feel/timestamp.t/run.t +++ b/tests/formatter/look_and_feel/timestamp.t/run.t @@ -1,6 +1,9 @@ $ scilla-fmt timestamp.scilla scilla_version 0 + (***************************************************) + (* The contract definition *) + (***************************************************) contract HelloWorld () diff --git a/tests/formatter/look_and_feel/ud-registry.t/run.t b/tests/formatter/look_and_feel/ud-registry.t/run.t index 11cd04b3a..85e465f75 100644 --- a/tests/formatter/look_and_feel/ud-registry.t/run.t +++ b/tests/formatter/look_and_feel/ud-registry.t/run.t @@ -1,5 +1,6 @@ $ scilla-fmt ud-registry.scilla scilla_version 0 + (* Give some love to the UD Dev Team Bogdan, Ryan, Don and Ali. *) import BoolUtils diff --git a/tests/formatter/look_and_feel/wallet.t/run.t b/tests/formatter/look_and_feel/wallet.t/run.t index 19dcfb089..9d3df64ac 100644 --- a/tests/formatter/look_and_feel/wallet.t/run.t +++ b/tests/formatter/look_and_feel/wallet.t/run.t @@ -5,22 +5,30 @@ ListUtils IntUtils + (***************************************************) + (* Associated library *) + (***************************************************) library WalletLib + (* Event for communicating a new transaction id *) let mk_transaction_added_event = fun (tc : Uint32) => { _eventname : "Transaction created"; transactionId : tc } + (* Event for communicating the signing of a transaction *) let mk_transaction_signed_event = fun (no_of_sigs : Uint32) => { _eventname : "Transaction signed"; signature_count : no_of_sigs } + (* Event for communicating the addition of a new owner *) let mk_candidate_owner_added_event = { _eventname : "Candiate owner added" } + (* Event for communicating the signing off of a new owner *) let mk_owner_signed_event = fun (no_of_sigs : Uint32) => { _eventname : "Owner signed"; signature_count : no_of_sigs } + (* Event for communicating the addition of a new owner *) let mk_new_owner_approved_event = { _eventname : "New owner approved" } type Error = @@ -38,6 +46,7 @@ | UnknownCandidate | CandidateAlreadyOwner + (* Error events *) let mk_error_event = fun (err : Error) => let err_code = @@ -63,9 +72,11 @@ let empty_sigs = Emp (ByStr20) (Bool) + (* One (potential) transaction, consisting of a recipient address and an amount *) type Transaction = | Trans of ByStr20 Uint128 + (* Make map of owners *) let mk_owners_map = fun (initial_owners : List ByStr20) => let init = Emp (ByStr20) (Bool) in @@ -74,13 +85,19 @@ fun (cur_owner : ByStr20) => let mem = builtin get acc cur_owner in match mem with - | Some True => acc - | _ => let t = True in builtin put acc cur_owner t + | Some True => + (* owner already added *) + acc + | _ => + (* owner not yet added, or removed *) + let t = True in + builtin put acc cur_owner t end in let folder = @list_foldl (ByStr20) (Map ByStr20 Bool) in folder iter init initial_owners + (* Check that the number of distinct owners is greater than 0 *) let check_contract_validity = fun (owners : Map ByStr20 Bool) => let no_of_owners = builtin size owners in @@ -89,6 +106,7 @@ let transaction_executed = Int32 2 + (* Create one transaction message *) let transaction_msg = fun (recipient : ByStr20) => fun (amount : Uint128) => @@ -100,6 +118,7 @@ code : transaction_executed } + (* Wrap one transaction message as singleton list *) let transaction_msg_as_list = fun (recipient : ByStr20) => fun (amount : Uint128) => @@ -112,6 +131,7 @@ let msg = transaction_msg recipient amount tag in one_msg msg + (* list_mem for owners *) let address_mem = fun (sender : ByStr20) => fun (mem_map : Map ByStr20 Bool) => @@ -123,6 +143,31 @@ end + (***************************************************) + (* The contract definition *) + (* *) + (* This contract holds funds that can be paid out *) + (* to arbitrary users, provided that enough people *) + (* the collection of owners sign off on the payout *) + (* *) + (* The transaction must be added to the contract *) + (* before signatures can be collected. Once enough *) + (* signatures are collected, the recipient can ask *) + (* for the transaction to be executed and the *) + (* money paid out. *) + (* *) + (* A new owner can be added, provided that every *) + (* existing user signs off on the new owner. Once *) + (* all existing owners have signed for the new *) + (* owner, the new owner can claim ownership and be *) + (* added to the owners map. *) + (* *) + (* If an owner changes his mind about a *) + (* transaction or an owner he has already signed *) + (* for, the signature can be revoked until the *) + (* transaction is executed or the owner has been *) + (* approved. *) + (***************************************************) contract Wallet ( initial_owners : List ByStr20, @@ -130,48 +175,68 @@ ) + (* Funds are not allowed to be added if the contract is not valid *) field validity_checked : Bool = False field contract_valid : Bool = False + (* adr -> True indicates that an owner *) + (* adr not in map indicates non-owner *) + (* adr -> False is not used *) + (* The initial owners will be added as owners when funds are *) + (* initially added to the contract. *) field owners : Map ByStr20 Bool = Emp (ByStr20) (Bool) field transactionCount : Uint32 = Uint32 0 + (* Collected signatures for transactions *) field signatures : Map Uint32 (Map ByStr20 Bool) = Emp (Uint32) (Map ByStr20 Bool) + (* Transactions *) field transactions : Map Uint32 Transaction = Emp (Uint32) (Transaction) + (* Collected signatures for new owners *) field owner_signatures : Map ByStr20 (Map ByStr20 Bool) = Emp (ByStr20) (Map ByStr20 Bool) + (* Submit a transaction for future signoff *) transition SubmitTransaction (recipient : ByStr20, amount : Uint128) tc <- transactionCount; zero = Uint128 0; amount_is_zero = builtin eq amount zero; match amount_is_zero with | True => + (* Illegal transaction *) err = InvalidAmount; e = mk_error_event err; event e | False => + (* Create new transaction *) transaction = Trans recipient amount; + (* Add transaction to outstanding list of transactions *) ts_tmp <- transactions; ts_new = builtin put ts_tmp tc transaction; + (* Add empty list of signatures *) sigs_tmp <- signatures; sigs_new = builtin put sigs_tmp tc empty_sigs; + (* Increment transaction counter *) tc_new = builtin add tc transaction_inc; + (* Update fields *) transactionCount := tc_new; transactions := ts_new; signatures := sigs_new; + (* Create event with transaction Id *) e = mk_transaction_added_event tc; event e end end + (* Sign off on an existing transaction *) transition SignTransaction (transactionId : Uint32) + (* Helper function *) sender_mem = address_mem _sender; + (* Only the owner is allowed to sign off transactions *) owners_tmp <- owners; sender_is_owner = sender_mem owners_tmp; match sender_is_owner with @@ -180,6 +245,7 @@ e = mk_error_event err; event e | True => + (* Transaction must have been submitted *) ts_tmp <- transactions; transaction = builtin get ts_tmp transactionId; match transaction with @@ -188,6 +254,7 @@ e = mk_error_event err; event e | Some (Trans recipient amount) => + (* Transaction must occur in signatures map *) sigs_tmp <- signatures; sigs_opt = builtin get sigs_tmp transactionId; match sigs_opt with @@ -196,6 +263,7 @@ e = mk_error_event err; event e | Some sigs => + (* Sender must not have signed already *) sender_has_signed = sender_mem sigs; match sender_has_signed with | True => @@ -203,6 +271,7 @@ e = mk_error_event err; event e | False => + (* Signature is valid. Add to collected signatures *) t = True; new_sigs = builtin put sigs _sender t; new_signatures = builtin put sigs_tmp transactionId new_sigs; @@ -213,15 +282,18 @@ end end + (* Execute signed-off transaction *) transition ExecuteTransaction (transactionId : Uint32, tag : String) transactions_tmp <- transactions; transaction_opt = builtin get transactions_tmp transactionId; match transaction_opt with | None => + (* Transaction was not found. *) err = UnknownTransactionId; e = mk_error_event err; event e | Some (Trans recipient amount) => + (* Only the recipient can initiate the transaction *) recipient_is_sender = builtin eq recipient _sender; match recipient_is_sender with | False => @@ -229,6 +301,7 @@ e = mk_error_event err; event e | True => + (* Check for sufficient funds *) bal <- _balance; not_enough_money = builtin lt bal amount; match not_enough_money with @@ -241,10 +314,12 @@ sigs_opt = builtin get signatures_tmp transactionId; match sigs_opt with | None => + (* Signatures not found, even though the transaction exists. *) err = UnknownTransactionId; e = mk_error_event err; event e | Some sigs => + (* Check for sufficient number of signatures *) no_of_sigs = builtin size sigs; not_enough_signatures = builtin lt no_of_sigs required_signatures; match not_enough_signatures with @@ -253,6 +328,8 @@ e = mk_error_event err; event e | False => + (* Transaction approved, and enough money available. *) + (* Remove transaction and signatures, and execute. *) new_transactions = builtin remove transactions_tmp transactionId; transactions := new_transactions; new_signatures = builtin remove signatures_tmp transactionId; @@ -266,7 +343,9 @@ end end + (* Revoke signature of existing transaction, if it has not yet been executed. *) transition RevokeSignature (transactionId : Uint32) + (* Transaction must occur in signatures map *) sigs_tmp <- signatures; sigs_opt = builtin get sigs_tmp transactionId; match sigs_opt with @@ -275,6 +354,7 @@ e = mk_error_event err; event e | Some sigs => + (* Sender must have signed already *) sender_has_signed = address_mem _sender sigs; match sender_has_signed with | False => @@ -289,7 +369,9 @@ end end + (* Revoke signature for new owner *) transition RevokeOwnerSignature (new_owner : ByStr20) + (* new owner must occur in signatures map *) sigs_tmp <- owner_signatures; sigs_opt = builtin get sigs_tmp new_owner; match sigs_opt with @@ -298,6 +380,7 @@ e = mk_error_event err; event e | Some sigs => + (* Sender must have signed already *) sender_has_signed = address_mem _sender sigs; match sender_has_signed with | False => @@ -312,7 +395,10 @@ end end + (* Add candidate owner *) transition AddCandidateOwner (candidate : ByStr20) + (* Check validity of contract. *) + (* Owners map must be initialized for new owners to be added. *) checked <- validity_checked; match checked with | False => @@ -324,6 +410,7 @@ validity_checked := checked_now | True => end; + (* Only accept funds if the contract is valid. *) valid <- contract_valid; match valid with | False => @@ -335,6 +422,7 @@ sigs_option = builtin get owner_signatures_tmp candidate; match sigs_option with | Some _ => + (* Candidate already added *) err = CandidateAlreadyAdded; e = mk_error_event err; event e @@ -343,10 +431,12 @@ owner_option = builtin get owners_tmp candidate; match owner_option with | Some _ => + (* Candidate is already an owner *) err = CandidateAlreadyOwner; e = mk_error_event err; event e | None => + (* New candidate *) empty_sigs = Emp (ByStr20) (Bool); new_owner_signatures = builtin put owner_signatures_tmp candidate empty_sigs; @@ -356,9 +446,12 @@ end end + (* Sign off on new owner. *) transition SignOffNewOwner (candidate : ByStr20) + (* Helpers *) sender_mem = address_mem _sender; t = True; + (* Only owners are allowed to sign off new owners *) owners_tmp <- owners; sender_is_owner = sender_mem owners_tmp; match sender_is_owner with @@ -371,10 +464,12 @@ sigs_option = builtin get owner_signatures_tmp candidate; match sigs_option with | None => + (* Unknown candidate *) err = UnknownCandidate; e = mk_error_event err; event e | Some sigs => + (* Sender must not have signed already *) sender_has_signed = sender_mem sigs; match sender_has_signed with | True => @@ -386,6 +481,7 @@ new_owner_signatures = builtin put owner_signatures_tmp candidate new_sigs; owner_signatures := new_owner_signatures; + (* Create event with owner id *) no_of_sigs = builtin size new_sigs; e = mk_owner_signed_event no_of_sigs; event e @@ -394,11 +490,14 @@ end end + (* Promote _sender to owner, if all existing owners have signed *) transition ClaimOwnership () owner_signatures_tmp <- owner_signatures; sigs_option = builtin get owner_signatures_tmp _sender; + (* Check if all owners have signed *) match sigs_option with | None => + (* Unknown candidate *) err = UnknownCandidate; e = mk_error_event err; event e @@ -409,22 +508,28 @@ all_have_signed = uint32_eq no_of_sigs no_of_owners; match all_have_signed with | False => + (* Not enough signatures *) err = NotEnoughSignatures; e = mk_error_event err; event e | True => + (* Enough signatures collected. *) + (* Remove signatures, and add sender to owner collection *) new_owner_signatures = builtin remove owner_signatures_tmp _sender; owner_signatures := new_owner_signatures; t = True; new_owners = builtin put current_owners _sender t; owners := new_owners; + (* Create event with owner id *) e = mk_new_owner_approved_event; event e end end end + (* Add funds to wallet *) transition AddFunds () + (* Check validity of contract. If the contract is invalid, funds may become locked *) checked <- validity_checked; match checked with | False => @@ -436,6 +541,7 @@ validity_checked := checked_now | True => end; + (* Only accept funds if the contract is valid. *) valid <- contract_valid; match valid with | False => diff --git a/tests/formatter/look_and_feel/wallet_2.t/run.t b/tests/formatter/look_and_feel/wallet_2.t/run.t index 53d695984..71612d486 100644 --- a/tests/formatter/look_and_feel/wallet_2.t/run.t +++ b/tests/formatter/look_and_feel/wallet_2.t/run.t @@ -6,10 +6,15 @@ IntUtils BoolUtils + (***************************************************) + (* Associated library *) + (***************************************************) library WalletLib + (* Event emitted when the contract is initialized *) let mk_contract_initialized_event = { _eventname : "Contract initialized" } + (* Event for communicating a new transaction id *) let mk_transaction_added_event = fun (tc : Uint32) => fun (recipient : ByStr20) => @@ -23,6 +28,7 @@ tag : tag } + (* Event for communicating the execution of a transaction *) let mk_transaction_executed_event = fun (tc : Uint32) => fun (recipient : ByStr20) => @@ -36,10 +42,12 @@ tag : tag } + (* Event for communicating that a transaction was signed *) let mk_signed_transaction_event = fun (tc : Uint32) => { _eventname : "Transaction signed"; transactionId : tc } + (* Event for communicating that a signature was revoked *) let mk_signature_revoked_event = fun (tc : Uint32) => { _eventname : "Signature revoked"; transactionId : tc } @@ -58,6 +66,7 @@ | NonOwnerCannotSubmit | IncorrectSignatureCount + (* Error events *) let mk_error_event = fun (err : Error) => let err_code = @@ -88,26 +97,32 @@ let transaction_inc = one + (* One (potential) transaction, consisting of a recipient address, an amount, *) + (* and a tag (in case the recipient is another contract *) type Transaction = | Trans of ByStr20 Uint128 String + (* Make map of owners *) let mk_owners_map = fun (owners : List ByStr20) => let init = Emp (ByStr20) (Bool) in let iter = fun (acc : Map ByStr20 Bool) => fun (cur_owner : ByStr20) => + (* Add owner unconditionally. We check for duplicates later *) builtin put acc cur_owner t in let folder = @list_foldl (ByStr20) (Map ByStr20 Bool) in folder iter init owners + (* Create one transaction message *) let transaction_msg = fun (recipient : ByStr20) => fun (amount : Uint128) => fun (tag : String) => { _tag : tag; _recipient : recipient; _amount : amount } + (* Wrap one transaction message as singleton list *) let transaction_msg_as_list = fun (recipient : ByStr20) => fun (amount : Uint128) => @@ -121,6 +136,74 @@ one_msg msg + (***************************************************) + (* The contract definition *) + (* *) + (* This contract holds funds that can be paid out *) + (* to arbitrary users, provided that enough people *) + (* in the collection of owners sign off on the *) + (* payout. *) + (* *) + (* The transaction must be added to the contract *) + (* before signatures can be collected. Once enough *) + (* signatures are collected, the recipient can ask *) + (* for the transaction to be executed and the *) + (* money paid out. *) + (* *) + (* If an owner changes his mind about a *) + (* transaction, the signature can be revoked until *) + (* the transaction is executed. *) + (* *) + (* This wallet does not allow adding or removing *) + (* owners, or changing the number of required *) + (* signatures. To do any of those things, perform *) + (* the following steps: *) + (* *) + (* 1. Deploy a new wallet with owners and *) + (* required_signatures set to the new values. *) + (* MAKE SURE THAT THE NEW WALLET HAS BEEN *) + (* SUCCESFULLY DEPLOYED WITH THE CORRECT *) + (* PARAMETERS BEFORE CONTINUING! *) + (* 2. Invoke the SubmitTransaction transition on *) + (* the old wallet with the following *) + (* parameters: *) + (* recipient : The address of the new wallet *) + (* amount : The _balance of the old wallet *) + (* tag : "AddFunds" *) + (* 3. Have (a sufficient number of) the owners of *) + (* the old contract invoke the SignTransaction *) + (* transition on the old wallet. The parameter *) + (* transactionId should be set to the Id of the *) + (* transaction created in step 2. *) + (* 4. Have one of the owners of the old contract *) + (* invoke the ExecuteTransaction transition on *) + (* the old contract. This will cause the entire *) + (* balance of the old contract to be *) + (* transferred to the new wallet. Note that no *) + (* un-executed transactions will be transferred *) + (* to the new wallet along with the funds. *) + (* *) + (* WARNING: If a sufficient number of owners lose *) + (* their private keys, or for any other reason are *) + (* unable or unwilling to sign for new *) + (* transactions, the funds in the wallet will be *) + (* locked forever. It is therefore a good idea to *) + (* set required_signatures to a value strictly *) + (* less than the number of owners, so that the *) + (* remaining owners can retrieve the funds should *) + (* such a scenario occur. *) + (* *) + (* If an owner loses his private key, the *) + (* remaining owners should move the funds to a new *) + (* wallet (using the workflow described above) to *) + (* ensure that funds are not locked if another *) + (* owner loses his private key. The owner who *) + (* originally lost his private key can generate a *) + (* new key, and the corresponding address be added *) + (* to the new wallet, so that the same set of *) + (* persons own the new wallet. *) + (* *) + (***************************************************) contract Wallet ( owners_list : List ByStr20, @@ -137,6 +220,8 @@ andb required_sigs_not_too_high required_sigs_not_too_low in let all_ok = andb required_sigs_ok owners_ok in + (* Building the owners map is expensive, so avoid checking the owners map until *) + (* everything else has been checked *) match all_ok with | True => let owners_map = mk_owners_map owners_list in @@ -147,15 +232,21 @@ => + (* adr -> True indicates an owner *) + (* adr not in map indicates non-owner *) + (* adr -> False is not used *) field owners : Map ByStr20 Bool = mk_owners_map owners_list field transactionCount : Uint32 = Uint32 0 + (* Collected signatures for transactions *) field signatures : Map Uint32 (Map ByStr20 Bool) = Emp (Uint32) (Map ByStr20 Bool) + (* Running count of collected signatures for transactions *) field signature_counts : Map Uint32 Uint32 = Emp (Uint32) (Uint32) + (* Transactions *) field transactions : Map Uint32 Transaction = Emp (Uint32) (Transaction) procedure MakeError (err : Error) @@ -163,13 +254,16 @@ event e end + (* Add signature to signature list *) procedure AddSignature (transactionId : Uint32, signee : ByStr20) sig <- exists signatures[transactionId][signee]; match sig with | False => count <- signature_counts[transactionId]; match count with - | None => signature_counts[transactionId] := one + | None => + (* 0 signatures *) + signature_counts[transactionId] := one | Some c => new_c = builtin add c one; signature_counts[transactionId] := new_c @@ -178,13 +272,16 @@ e = mk_signed_transaction_event transactionId; event e | True => + (* Already signed *) err = AlreadySigned; MakeError err end end + (* Submit a transaction for future signoff *) transition SubmitTransaction (recipient : ByStr20, amount : Uint128, tag : String) + (* Only allow owners to submit new transactions *) sender_is_owner <- exists owners[_sender]; match sender_is_owner with | False => @@ -196,50 +293,66 @@ amount_is_zero = builtin eq amount zero; match amount_is_zero with | True => + (* Illegal transaction *) err = InvalidAmount; MakeError err | False => + (* Create new transaction *) transaction = Trans recipient amount tag; + (* Add transaction to outstanding list of transactions *) transactions[tc] := transaction; + (* Sender implicitly signs *) AddSignature tc _sender; + (* Increment transaction counter *) tc_new = builtin add tc transaction_inc; + (* Update transaction count *) transactionCount := tc_new; + (* Create event with transaction Id *) e = mk_transaction_added_event tc recipient amount tag; event e end end end + (* Sign off on an existing transaction *) transition SignTransaction (transactionId : Uint32) + (* Only the owner is allowed to sign off transactions *) sender_is_owner <- exists owners[_sender]; match sender_is_owner with | False => err = NonOwnerCannotSign; MakeError err | True => + (* Transaction must have been submitted *) transaction <- transactions[transactionId]; match transaction with | None => err = UnknownTransactionId; MakeError err - | Some _ => AddSignature transactionId _sender + | Some _ => + (* Remaining error cases handled by AddSignature *) + AddSignature transactionId _sender end end end + (* Delete transaction and signatures *) procedure DeleteTransaction (transactionId : Uint32) delete transactions[transactionId]; delete signatures[transactionId]; delete signature_counts[transactionId] end + (* Execute signed-off transaction *) transition ExecuteTransaction (transactionId : Uint32) transaction_opt <- transactions[transactionId]; match transaction_opt with | None => + (* Transaction was not found. *) err = UnknownTransactionId; MakeError err | Some (Trans recipient amount tag) => + (* Only the recipient or an owner can execute the transaction *) recipient_is_sender = builtin eq recipient _sender; sender_is_owner <- exists owners[_sender]; sender_may_execute = orb recipient_is_sender sender_is_owner; @@ -248,6 +361,7 @@ err = SenderMayNotExecute; MakeError err | True => + (* Check for sufficient funds *) bal <- _balance; not_enough_money = builtin lt bal amount; match not_enough_money with @@ -258,6 +372,7 @@ sig_count_opt <- signature_counts[transactionId]; match sig_count_opt with | None => + (* Signature count not found, even though the transaction exists. *) err = NoSignatureListFound; MakeError err | Some sig_count => @@ -267,6 +382,8 @@ err = NotEnoughSignatures; MakeError err | False => + (* Transaction approved, and enough money available. *) + (* Remove transaction and signatures, and execute. *) DeleteTransaction transactionId; msgs = transaction_msg_as_list recipient amount tag; send msgs; @@ -279,6 +396,7 @@ end end + (* Revoke signature of existing transaction, if it has not yet been executed. *) transition RevokeSignature (transactionId : Uint32) sig <- exists signatures[transactionId][_sender]; match sig with @@ -308,6 +426,7 @@ end end + (* Add funds to wallet *) transition AddFunds () accept end diff --git a/tests/formatter/look_and_feel/zil-game.t/run.t b/tests/formatter/look_and_feel/zil-game.t/run.t index 2d50b0862..0a24f8736 100644 --- a/tests/formatter/look_and_feel/zil-game.t/run.t +++ b/tests/formatter/look_and_feel/zil-game.t/run.t @@ -1,5 +1,8 @@ $ scilla-fmt zil-game.scilla scilla_version 0 + (***************************************************) + (* Associated library *) + (***************************************************) import BoolUtils @@ -42,6 +45,7 @@ Some {(BNum)} b1 end + (* b is within the time window *) let can_play = fun (tm : Option BNum) => fun (b : BNum) => @@ -80,6 +84,7 @@ end end + (* Owner can withdraw balance if deadline has passed *) let can_withdraw = fun (tm : BNum) => fun (b : BNum) => @@ -87,6 +92,7 @@ let deadline = builtin badd tm window in builtin blt deadline b + (* In the case of equal results, or no results the prise goes to the owner *) let determine_winner = fun (puzzle : ByStr32) => fun (guess_a : Option ByStr32) => @@ -130,6 +136,9 @@ let cannot_withdraw = Int32 7 + (***************************************************) + (* The contract definition *) + (***************************************************) contract ZilGame ( owner : ByStr20, @@ -139,6 +148,7 @@ ) + (* Initial balance is not stated explicitly: it's initialized when creating the contract. *) field player_a_hash : Option ByStr32 = None {(ByStr32)} field player_b_hash : Option ByStr32 = None {(ByStr32)} @@ -148,6 +158,7 @@ transition Play (guess : ByStr32) tm_opt <- timer; b <-& BLOCKNUMBER; + (* Check the timer *) c = can_play tm_opt b; match c with | False => @@ -215,6 +226,7 @@ transition ClaimReward (solution : Int128) tm_opt <- timer; b <-& BLOCKNUMBER; + (* Check the timer *) ttc = time_to_claim tm_opt b; match ttc with | False => diff --git a/tests/formatter/look_and_feel/zip.t/run.t b/tests/formatter/look_and_feel/zip.t/run.t index 5949fa413..1455e3b94 100644 --- a/tests/formatter/look_and_feel/zip.t/run.t +++ b/tests/formatter/look_and_feel/zip.t/run.t @@ -45,6 +45,7 @@ fun (h : 'A) => match z with | Pair r b => + (* Get b's head, pair it with h and add to r. *) let header = @list_head ('B) in let tailer = @list_tail ('B) in let bhead = header b in