diff --git a/.gitignore b/.gitignore index f69711ed..8ab4e658 100644 --- a/.gitignore +++ b/.gitignore @@ -1,3 +1,5 @@ *~ _obuild /tezos +/tests/*.cm? +/tests/*/*.cm? diff --git a/.travis.yml b/.travis.yml new file mode 100644 index 00000000..ff408e31 --- /dev/null +++ b/.travis.yml @@ -0,0 +1,24 @@ +# branches: +# only: +# - master +dist: trusty +language: ocaml +sudo: required + +before_install: +- sh travis-scripts/prepare-trusty.sh + +install: +- sh travis-scripts/prepare-opam.sh + +script: +- export OPAMYES=1 +- opam sw 4.05.0 +- eval `opam config env` +- make clone-tezos +- make +- make tests-mini +- make tests +- make rev-tests + +# TODO > how to compile and test with tezos (I.e. with a fully compiled version of tezos)? diff --git a/Makefile b/Makefile index 7d5d4c39..e2a3b18f 100644 --- a/Makefile +++ b/Makefile @@ -1,10 +1,10 @@ all: build -tezos/Makefile: - git clone git@gitlab.com:tezos/tezos.git +clone-tezos: + git clone -b alphanet https://github.com/tezos/tezos.git # clone with https -build: _obuild tezos/Makefile +build: _obuild ocp-build build install: _obuild @@ -14,18 +14,7 @@ _obuild: Makefile ocp-build init clean-tests: - rm -f tests/*.liq.tz \ - tests/*.liq.debug \ - tests/*.liq.tz.liq \ - tests/*.pdf \ - tests/*.dot \ - tests/*.syntax \ - tests/*.typed \ - tests/*.mic \ - tests/*.normal \ - tests/*.pre \ - tests/others/*.*.* - rm -f *~ tests/*~ tests/others/*~ + $(MAKE) -C tests clean clean-sources: rm -f tools/*/*~ libs/*/*~ @@ -38,12 +27,12 @@ distclean: clean # All of these tests must be run with with_tezos=true -NTESTS=18 +NTESTS=20 SIMPLE_TESTS= `seq -f 'test%.0f' 0 $(NTESTS)` MORE_TESTS=test_ifcons test_if test_loop test_option test_transfer test_left \ test_extfun test_left_constr test_closure test_closure2 test_closure3 \ test_map test_rev test_reduce_closure test_map_closure test_mapreduce_closure \ - test_mapmap_closure test_setreduce_closure + test_mapmap_closure test_setreduce_closure test_left_match OTHER_TESTS=others/broker others/demo others/auction REV_TESTS=`seq -f 'test%.0f' 0 5` diff --git a/README.md b/README.md index 3ef860be..de3b57f7 100644 --- a/README.md +++ b/README.md @@ -1,3 +1,8 @@ +next | master +------------ | ------------- +[![Travis-CI Build Status](https://travis-ci.org/OCamlPro/liquidity.svg?branch=next)](https://travis-ci.org/OCamlPro/liquidity) | [![Travis-CI Build Status](https://travis-ci.org/OCamlPro/liquidity.svg?branch=master)](https://travis-ci.org/OCamlPro/liquidity) + + Liquidity: a Smart Contract Language for Tezos ============================================== diff --git a/USAGE.md b/USAGE.md index 8392ff5c..5f80a893 100644 --- a/USAGE.md +++ b/USAGE.md @@ -14,7 +14,14 @@ You need the following dependencies to be installed to compile `liquidity`: Compilation and installation ---------------------------- -In the top-directory, use `make` and `make install` +In the top-directory, use: +* `make clone-tezos` +* `make` +* `make install` + +If you want limited features, you can pass the first step, you will +only get a program `liquidity-mini` with only compilation features, +no decompilation. You can also use `make clean` to clean the directories, and `make tests` to run the compiler on examples in the diff --git a/build.ocp2 b/build.ocp2 index 3496f46c..f3f95451 100644 --- a/build.ocp2 +++ b/build.ocp2 @@ -1,15 +1,26 @@ -(* Version of the Liquidity compiler *) - -version = "1.0"; - (* Disable to compile without the sources of Tezos. The following features with be disabled: * Decompilation of Michelson files * Execution of Michelson contracts *) +Sys = module("ocp-build:Sys", "1.0"); + (* This value is used if with_tezos is not set before *) -default_with_tezos = true; +default_with_tezos = Sys.file_exists("tezos/README.md"); try { with_tezos = with_tezos; } catch("unknown-variable",x){ with_tezos = default_with_tezos; } + +(* By default, liquidity will contain some version information + (Git commit, build date, etc.). However, during development, it + makes recompilation slower, so you can create a file DEVEL here + to tell ocp-build not to include version information. + The flag can also be controled in an inclusing project by using + the 'with_version' option. +*) + +default_with_version = !Sys.file_exists("DEVEL"); + +try { with_version = with_version; } + catch("unknown-variable",x){ with_version = default_with_version; } diff --git a/check-mini.sh b/check-mini.sh index 7e9cfdf9..331ca233 100755 --- a/check-mini.sh +++ b/check-mini.sh @@ -1,17 +1,27 @@ #!/bin/sh +DEFAULT='\033[0m' +RED='\033[0;31m' + test=$1 -echo $test +echo "\n[check-mini.sh] test = $test" LIQUIDITY=liquidity ./_obuild/${LIQUIDITY}-mini/${LIQUIDITY}-mini.asm tests/$test.liq || exit 2 -./tezos/_obuild/tezos-client/tezos-client.asm typecheck program tests/$test.liq.tz - +if [ -f ./tezos/_obuild/tezos-client/tezos-client.asm ] ; then + ./tezos/_obuild/tezos-client/tezos-client.asm typecheck program tests/$test.liq.tz +else + echo "\n${RED}./tezos/_obuild/tezos-client/tezos-client.asm not present ! typechecking of tests/$test.liq.tz skipped${DEFAULT}\n" +fi ./_obuild/${LIQUIDITY}/${LIQUIDITY}.asm tests/$test.liq.tz || exit 2 ./_obuild/${LIQUIDITY}-mini/${LIQUIDITY}-mini.asm tests/$test.liq.tz.liq || exit 2 -./tezos/_obuild/tezos-client/tezos-client.asm typecheck program tests/$test.liq.tz.liq.tz +if [ -f ./tezos/_obuild/tezos-client/tezos-client.asm ] ; then + ./tezos/_obuild/tezos-client/tezos-client.asm typecheck program tests/$test.liq.tz.liq.tz +else + echo "\n${RED}./tezos/_obuild/tezos-client/tezos-client.asm not present ! typechecking of tests/$test.liq.tz.liq.tz skipped${DEFAULT}\n" +fi diff --git a/check-rev.sh b/check-rev.sh index 23cecdf6..c4d20def 100755 --- a/check-rev.sh +++ b/check-rev.sh @@ -3,12 +3,20 @@ echo '=============================================================' echo +DEFAULT='\033[0m' +RED='\033[0;31m' + TESTDIR=$1 test=$2 -echo $test -echo "Testing $test.tz ---------------------------------------------" -./tezos/_obuild/tezos-client/tezos-client.asm typecheck program $TESTDIR/$test.tz +echo "\n[check-rev.sh] test = $test, TESTDIR = $TESTDIR" + +if [ -f ./tezos/_obuild/tezos-client/tezos-client.asm ] ; then + echo "Testing $test.tz ---------------------------------------------" + ./tezos/_obuild/tezos-client/tezos-client.asm typecheck program $TESTDIR/$test.tz +else + echo "\n${RED}./tezos/_obuild/tezos-client/tezos-client.asm not present ! typechecking of $TESTDIR/$test.tz skipped${DEFAULT}\n" +fi echo "Generating $test.tz.liq --------------------------------------" ./_obuild/liquidity/liquidity.asm $TESTDIR/$test.tz || exit 2 @@ -16,8 +24,12 @@ echo "Generating $test.tz.liq --------------------------------------" echo "Compiling $test.tz.liq ---------------------------------------" ./_obuild/liquidity/liquidity.asm $TESTDIR/$test.tz.liq || exit 2 -echo "Testing $test.tz.liq.tz --------------------------------------" -./tezos/_obuild/tezos-client/tezos-client.asm typecheck program $TESTDIR/$test.tz.liq.tz || exit 2 +if [ -f ./tezos/_obuild/tezos-client/tezos-client.asm ] ; then + echo "Testing $test.tz.liq.tz --------------------------------------" + ./tezos/_obuild/tezos-client/tezos-client.asm typecheck program $TESTDIR/$test.tz.liq.tz || exit 2 +else + echo "\n${RED}./tezos/_obuild/tezos-client/tezos-client.asm not present ! typechecking of $TESTDIR/$test.tz.liq.tz skipped${DEFAULT}\n" +fi echo echo GOOD diff --git a/check.sh b/check.sh index bbdc1a0c..b3dff903 100755 --- a/check.sh +++ b/check.sh @@ -1,15 +1,21 @@ #!/bin/sh +DEFAULT='\033[0m' +RED='\033[0;31m' + test=$1 -echo $test +echo "\n[check.sh] test = $test" LIQUIDITY=liquidity echo ./_obuild/${LIQUIDITY}/${LIQUIDITY}.asm tests/$test.liq ./_obuild/${LIQUIDITY}/${LIQUIDITY}.asm tests/$test.liq || exit 2 -./tezos/_obuild/tezos-client/tezos-client.asm typecheck program tests/$test.liq.tz - +if [ -f ./tezos/_obuild/tezos-client/tezos-client.asm ] ; then + ./tezos/_obuild/tezos-client/tezos-client.asm typecheck program tests/$test.liq.tz || exit 2 +else + echo "\n${RED}./tezos/_obuild/tezos-client/tezos-client.asm not present ! typechecking of tests/$test.liq.tz skipped${DEFAULT}\n" +fi echo ./_obuild/${LIQUIDITY}/${LIQUIDITY}.asm tests/$test.liq.tz ./_obuild/${LIQUIDITY}/${LIQUIDITY}.asm tests/$test.liq.tz || exit 2 @@ -17,4 +23,12 @@ echo ./_obuild/${LIQUIDITY}/${LIQUIDITY}.asm tests/$test.liq.tz echo ./_obuild/${LIQUIDITY}/${LIQUIDITY}.asm tests/$test.liq.tz.liq ./_obuild/${LIQUIDITY}/${LIQUIDITY}.asm tests/$test.liq.tz.liq || exit 2 -./tezos/_obuild/tezos-client/tezos-client.asm typecheck program tests/$test.liq.tz.liq.tz +if [ -f ./tezos/_obuild/tezos-client/tezos-client.asm ] ; then + ./tezos/_obuild/tezos-client/tezos-client.asm typecheck program tests/$test.liq.tz.liq.tz || exit 2 +else + echo "\n${RED}./tezos/_obuild/tezos-client/tezos-client.asm not present ! typechecking of tests/$test.liq.tz.liq.tz skipped${DEFAULT}\n" +fi + +echo ./_obuild/ocp-liquidity-comp/ocp-liquidity-comp.asm -I +../zarith zarith.cma -I _obuild/liquidity-env ./_obuild/liquidity-env/liquidity-env.cma -impl tests/$test.liq +./_obuild/ocp-liquidity-comp/ocp-liquidity-comp.asm -I +../zarith zarith.cma -I _obuild/liquidity-env ./_obuild/liquidity-env/liquidity-env.cma -dsource -impl tests/$test.liq +rm -f a.out diff --git a/docs/liquidity.md b/docs/liquidity.md index 5427fe97..550494d8 100644 --- a/docs/liquidity.md +++ b/docs/liquidity.md @@ -27,7 +27,7 @@ All the contracts have the following form: let%entry main (parameter : TYPE) (storage : TYPE) - [%return : TYPE] = + : TYPE = BODY ``` @@ -40,17 +40,17 @@ network. The `main` function is the default entry point for the contract. `let%entry` is the construct used to declare entry points (there is currently only one entry point, but there will be probably more in the -future). The declaration takes three parameters with names -`parameter`, `storage` and `return`. The first two parameters, -`parameter` and `storage` are arguments to the function, while the -latest one, `return`, is only used to specified the return type of the -function. The types of the three parameters must always be specified. +future). The declaration takes two parameters with names +`parameter`, `storage`, the arguments to the function. Their types must +always be specified. The return type of the function must also be +specified by a type annotation. A contract always returns a pair `(return, storage)`, where `return` is the return value to the caller, and `storage` is the final state of the contract after the call. The type of the pair must match the type -of a pair with the two parameters, `return` and `storage`, that were -specified at the beginning of `main`. +of a pair where the first component is the return type of the function +specified in its signature and the second is the type of the argument +`storage` of `main`. <... local declarations ...> is an optional set of optional type and function declarations. Type declarations can be used to define records diff --git a/libs/deps-michelson/utils.ml b/libs/deps-michelson/utils.ml index 6957ee80..75b8cc86 100644 --- a/libs/deps-michelson/utils.ml +++ b/libs/deps-michelson/utils.ml @@ -95,3 +95,5 @@ let split delim ?(limit = max_int) path = do_slashes [] limit 0 else [ path ] + +module StringMap = Map.Make (String) diff --git a/libs/michelson/cli_entries.ml b/libs/michelson/cli_entries.ml index d896497e..835ef6a9 100644 --- a/libs/michelson/cli_entries.ml +++ b/libs/michelson/cli_entries.ml @@ -1,3 +1,4 @@ +open Utils #include "../../tezos/src/utils/cli_entries.ml" (* diff --git a/libs/michelson/client_proto_args.mli b/libs/michelson/client_proto_args.mli new file mode 100644 index 00000000..8a0339ba --- /dev/null +++ b/libs/michelson/client_proto_args.mli @@ -0,0 +1,4 @@ + +open Tezos_context + +#include "../../tezos/src/client/embedded/alpha/client_proto_args.mli" diff --git a/libs/michelson/client_proto_programs.ml b/libs/michelson/client_proto_programs.ml index d515e894..3b1a8e49 100644 --- a/libs/michelson/client_proto_programs.ml +++ b/libs/michelson/client_proto_programs.ml @@ -35,6 +35,7 @@ end module Environment = struct module Ed25519 = Ed25519 + module Error_monad = Error_monad end #include "../../tezos/src/client/embedded/alpha/client_proto_programs.ml" diff --git a/misc/build-tezos.ocp2-inc b/misc/build-tezos.ocp2-inc new file mode 100644 index 00000000..75496e6f --- /dev/null +++ b/misc/build-tezos.ocp2-inc @@ -0,0 +1,864 @@ +(* Script to build Tezos with ocp-build. + +To use this script, checkout Tezos in a sub-directory `tezos/`, and +create a file `build.ocp2` in `tezos/src/` containing only: + +``` +include "../../misc/build-tezos.ocp2-inc"; +``` + +*) + +(* We want to use Posix threads when linking leveldb: *) +OCaml.library("threads", ocaml + { + generated = true; + dirname = "%{OCAMLLIB}%"; + requires = [ "threads.posix" ]; + }); + + + +(* For now, disable webclient, since it does not compile *) +build_webclient = false; + +List = module("ocp-build:List", "1.0"); +OCaml = module("ocp-build:OCaml", "1.0"); +Sys = module("ocp-build:Sys", "1.0"); + +has_securenv = Sys.file_exists(dirname + "/ppx/ppx_securenv.ml"); +has_check = Sys.file_exists(dirname + "/minutils/check.ml"); +has_liquidity = Sys.file_exists(dirname + "/liquidity"); +has_liquidity = false; + + +if( has_liquidity ) { + liquidity_files = [ "client_proto_programs_commands.ml" ]; +} else { + liquidity_files = []; +} + + +OCaml.program("tezos_protocol_environment_sigs_packer", + ocaml + { + files = [ + "environment/tezos_protocol_environment_sigs_packer.ml"; + ]; + }); + + +ocaml.debug = true; + +compflags = [ "-bin-annot"; "-g"; "-thread"; "-short-paths"; "-safe-string"; + "-w"; "+27-30-40"; ]; +min_opens = [ + "-open"; "Error_monad"; + "-open"; "Hash"; + "-open"; "Utils"; +]; + +opens = min_opens + [ + "-open"; "Tezos_data"; +]; + +basic_packages = [ "cstruct"; "lwt"; "ocplib-json-typed.bson"; + "ocplib-resto.directory"; "base64"; "calendar"; "ezjsonm"; + "ipaddr.unix"; "lwt.unix"; "mtime.clock.os"; "nocrypto"; + "sodium"; "zarith"; "compiler-libs.optcomp"; "lwt.unix"; + "ocplib-endian"; "ocplib-ocamlres"; "unix"; ]; + +more_packages = basic_packages + [ "calendar"; "cmdliner"; + "cohttp.lwt"; "dynlink"; "git"; (* "ipv6-multicast"; *) "irmin-unix"; + "ocplib-resto.directory"; "ssl"; "leveldb" ]; + +ocaml_without_opens = ocaml + { + dep = []; + bytecomp = compflags; + asmcomp = compflags; + }; + +ocaml_with_opens = ocaml + { + dep = opens; + bytecomp = compflags + opens; + asmcomp = compflags + opens; + }; + +if( has_securenv ){ + + OCaml.program("ppx_securenv", { + files = [ "ppx/ppx_securenv.ml" ]; + requires = [ "compiler-libs.common" ]; + }); + securenv_mls = [ "securenv.ml" ]; + securenv_mlis = [ "securenv.mli" ]; +} else { + securenv_mlis = []; + securenv_mls = []; +} + +if( has_check ){ + check_mls = [ "check.ml" ]; + check_mlis = [ "check.mli" ]; +} else { + check_mls = []; + check_mlis = []; +} + +function lib_with_opens(name, o){ + OCaml.library(name, ocaml_with_opens + o); +} + +function lib_without_opens(name, o){ + OCaml.library(name, ocaml_without_opens + o); +} + +function program_with_opens(name, o){ + OCaml.program(name, ocaml_with_opens + o); +} + +function program_without_opens(name, o){ + OCaml.program(name, ocaml_without_opens + o); +} + +lib_without_opens("minutils", { + subdir = "minutils"; + files = securenv_mls + [ + "mBytes.ml"; + "hex_encode.ml"; + "utils.ml"; + "compare.ml"; + ] + check_mls + [ + "data_encoding.ml"; + "RPC.ml"; ]; + requires = [ + "cstruct"; "lwt"; "ocplib-json-typed.bson"; + "ocplib-resto.directory"; + ]; + }); + + + +lib_without_opens("utils", { + subdir = "utils"; + files = [ + "base58.ml"; + "error_monad_sig.ml"; + "error_monad.ml"; + "cli_entries.ml"; + "data_encoding_ezjsonm.ml"; + "time.ml"; + "hash.ml"; + "crypto_box.ml"; + "lwt_exit.ml"; + "logging.ml"; + "lwt_utils.ml"; + "lwt_pipe.ml"; "IO.ml"; + "moving_average.ml"; + "ring.ml"; + "watcher.ml"; + "tezos_data.ml"; + ]; + requires = [ + "minutils"; + ] + basic_packages; + }); + +utils_packages = [ "utils"; "minutils" ]; + + + + + + +begin + + compflags += [ ]; + + OCaml.objects("sigs", + ocaml + { + + dep = opens; + bytecomp = compflags + opens; + asmcomp = compflags + opens; + + files = [ + "environment/tezos_protocol_environment_sigs_v1.ml", { + deps = []; + bytecomp = compflags + [ "-nopervasives" ]; + asmcomp = compflags + [ "-nopervasives" ]; + }; + + "compiler/tezos_protocol_registerer.ml",{ + bytecomp = compflags + [ "-opaque" ] + opens; + asmcomp = compflags + [ "-opaque" ] + opens; + }; + ]; + requires = [ "minutils"; "utils";"proto"; ]; + }); +end + +OCaml.rules("embedded", ocaml + { + subdir = "compiler"; + build_rules = [ + "compiler/tezos_compiler_embedded_cmis.ml", + { + build_target = true; + sources = [ + "%{OCAMLLIB}%/camlinternalFormatBasics.cmi"; + "%{sigs_FULL_DST_DIR}%/tezos_protocol_environment_sigs_v1.cmi"; + "%{sigs_FULL_DST_DIR}%/tezos_protocol_registerer.cmi"; + ]; + commands = [ + OCaml.system( + [ + "ocp-ocamlres"; "-format"; "ocaml"; + "-o"; "compiler/tezos_compiler_embedded_cmis.ml"; + "%{OCAMLLIB}%/camlinternalFormatBasics.cmi"; + "%{sigs_FULL_DST_DIR}%/tezos_protocol_environment_sigs_v1.cmi"; + "%{sigs_FULL_DST_DIR}%/tezos_protocol_registerer.cmi"; + ] + ); + ]; + }; + ]; + requires = [ "sigs" ]; + }); + + + +lib_with_opens("packer", { + subdir = "packer"; + files = [ "tezos_protocol_packer.ml" ]; + requires = [] + utils_packages; + }); + + +lib_with_opens("compiler", { + subdir = "compiler"; + files = [ + "tezos_compiler_embedded_cmis.ml"; + "tezos_compiler.ml" + ]; + requires = [ + (* We cannot depend directly on [cmis], because they would be linked + in this library. Instead, we depend on a "rules" package. *) + "embedded"; "packer"; + ] + utils_packages; + }); + + +program_without_opens("tezos-protocol-compiler", { + files = [ "compiler_main.ml"; ]; + requires = [ + "minutils"; "utils"; "compiler"; + ] + basic_packages; + }); + +begin + mlis = [ + "pervasives.mli"; + ] + securenv_mlis + [ + "compare.mli"; + ] + check_mlis + [ + "array.mli"; + "list.mli"; + "bytes.mli"; + "string.mli"; + "set.mli"; + "map.mli"; + "int32.mli"; + "int64.mli"; + "buffer.mli"; + "format.mli"; + "z.mli"; + "lwt_sequence.mli"; + "lwt.mli"; + "lwt_list.mli"; + "mBytes.mli"; + "hex_encode.mli"; + "uri.mli"; + "data_encoding.mli"; + "error_monad.mli"; + "logging.mli"; + "time.mli"; + "base58.mli"; + "hash.mli"; + "ed25519.mli"; + "tezos_data.mli"; + "persist.mli"; + "context.mli"; + "RPC.mli"; + "updater.mli"; + ]; + + mlis = List.map( + function(file){ return ("environment/v1/" + file); }, + mlis ); + + generator = DSTDIR("tezos_protocol_environment_sigs_packer", + "tezos_protocol_environment_sigs_packer.byte"); + generated_file = "environment/tezos_protocol_environment_sigs_v1.ml"; + env.build_rules = [ + generated_file, { + build_target = true; + sources = mlis + [ generator ]; + commands = [ + OCaml.system([generator] + mlis , + { stdout = generated_file; }); + ]; + }; + ]; + env.requires = [ "tezos_protocol_environment_sigs_packer" ]; + OCaml.rules("proto", env); +end + +lib_with_opens("node", { + + files = [ + "compiler/node_compiler_main.ml"; + "node/net/p2p_types.ml"; + "node/net/p2p_io_scheduler.ml"; + "node/net/p2p_connection.ml"; + "node/net/p2p_connection_pool_types.ml"; + "node/net/p2p_connection_pool.ml"; + "node/net/p2p_welcome.ml"; + "node/net/p2p_discovery.ml"; + "node/net/p2p_maintenance.ml"; + "node/net/p2p.ml"; + "node/net/RPC_server.ml"; + + "node/db/persist.ml"; + "node/db/context.ml"; + + "node/db/raw_store.ml"; + "node/db/store_sigs.mli"; + "node/db/store_helpers.ml"; + "node/db/store.ml"; + "node/updater/updater.ml"; + "node/updater/tezos_protocol_environment.ml"; + "node/updater/register.ml"; + + "node/shell/state.ml"; + "node/shell/distributed_db_functors.ml"; + "node/shell/distributed_db_message.ml"; + "node/shell/distributed_db_metadata.ml"; + "node/shell/distributed_db.ml"; + "node/shell/chain_traversal.ml"; + "node/shell/chain.ml"; + "node/shell/prevalidation.ml"; + "node/shell/prevalidator.ml"; + "node/shell/validator.ml"; + + "node/shell/node_rpc_services.ml"; + "node/shell/node.ml"; + "node/shell/node_rpc.ml"; + ]; + + requires = [ + "minutils"; "utils"; "compiler"; "proto"; "sigs"; + ] + more_packages; + + }); + +function read_sources(protocol) +{ + dir = "proto/" + protocol; + files = Sys_readdir(dir, "*.ml") + Sys_readdir(dir, "*.mli"); + files = List.map(function(file){return dir + "/" + file;},files); + return files; +} + +protocol_sources["alpha"] = read_sources("alpha"); +protocol_sources["demo"] = read_sources("demo"); +protocol_sources["genesis"] = read_sources("genesis"); + + begin + + compiler = + "%{tezos-protocol-compiler_FULL_DST_DIR}%/tezos-protocol-compiler.asm"; + + function compile(lib, dir, sources){ + + return OCaml.make([ + "proto/" + lib + ".o"; + "proto/" + lib + ".cmi"; + "proto/" + lib + ".cmx"; + ], + [ compiler ] + sources, + [ + [ + compiler; "-static"; + "-bin-annot"; "-g"; + "proto/"+lib; + dir; + ] + ] + ); + } + + function embedded_proto(name){ + env.build_rules = List.flatten([ + compile("tezos_embedded_protocol_" + name, "proto/" + name, + protocol_sources[name]); + ]); + env.requires = [ "tezos-protocol-compiler" ]; + env.tolink = true; + env.asm_targets = [ "proto/tezos_embedded_protocol_" + name + ".cmx" ]; + env.byte_targets = [ "proto/tezos_embedded_protocol_" + name + ".cma" ]; + env.intf_targets = [ "proto/tezos_embedded_protocol_" + name + ".cmi"; + "proto/tezos_embedded_protocol_" + name + ".cmx"; + ]; + + OCaml.rules("tezos_embedded_protocol_" + name, env); + } + + embedded_proto("alpha"); + embedded_proto("demo"); + embedded_proto("genesis"); + + end + +program_with_opens("tezos-node", + { + has_byte = false; + asmlink = [ "-linkall"; "-g" ]; + bytelink = [ "-linkall"; "-g" ]; + files = [ + "node/main/node_identity_file.ml"; + "node/main/node_config_file.ml"; + "node/main/node_shared_arg.ml"; + "node/main/node_run_command.ml"; + "node/main/node_config_command.ml"; + "node/main/node_identity_command.ml"; + "node_main.ml"; + ]; + requires = [ + "tezos_embedded_protocol_alpha"; + "tezos_embedded_protocol_demo"; + "tezos_embedded_protocol_genesis"; + + "minutils"; "utils"; "compiler"; "node"; + ] + more_packages; + }); + + + + + + + + + + + + + + + + + + + + + + + + +lib_with_opens("client", { + + subdir = "client"; + requires = basic_packages + utils_packages + [ "node" ]; + files = [ + "client_rpcs.ml"; + "client_node_rpcs.ml"; + "client_commands.ml"; + "client_config.ml"; + "client_generic_rpcs.ml"; + "client_helpers.ml"; + "client_aliases.ml"; + "client_tags.ml"; + "client_keys.ml"; + "client_protocols.ml"; + "client_network.ml"; + ]; + }); + + + +function client_objects(proto, o){ + + + base_opens = []; + + more_opens = [ + "-open"; "Client_proto_" + proto; + "-open"; "Error_monad"; + "-open"; "Hash"; + "-open"; "Tezos_data" + ] + o.opens; + + ocaml.subdir = "client/embedded/" + proto; + ocaml.more_deps = + [ "%{tezos_embedded_protocol_" + proto + "_FULL_SRC_DIR}%/proto/tezos_embedded_protocol_" + proto + ".cmx"; ]; + + requires = [ "utils"; "minutils"; "node"; "client"; "lwt"; "zarith"; + "ocplib-json-typed"; "sodium"; "sigs"; "ocplib-endian"; "uri"]; + includes = + List.flatten( + List.map(function(dep){ + return ["-I"; DSTDIR(dep) ]; + }, requires)); + + compflags += [ "-I"; "%{tezos_embedded_protocol_" + proto + "_FULL_SRC_DIR}%/proto" ] + includes; + + packed_files = + [ + "client_proto_" + proto + ".ml", { + dep = base_opens; + asmcomp = compflags + base_opens; + bytecomp = compflags + base_opens; + }; + ] + List.map(function(file){ + return file, { + dep = more_opens; + asmcomp = compflags + more_opens; + bytecomp = compflags + more_opens; + }; + },o.packed_files); + + ocaml.dep = more_opens; + ocaml.asmcomp = compflags; + ocaml.bytecomp = compflags; + + + ocaml.files = OCaml.pack("Client_" + proto, packed_files); + ocaml.requires = o.requires; + OCaml.objects("client_" + proto, ocaml); +} + + + +client_objects("genesis", { + opens = []; + packed_files = [ + "client_proto_main.ml"; + ]; + requires = [ + "client"; "client_alpha"; + "tezos_embedded_protocol_alpha", { tolink = true; }; + "tezos_embedded_protocol_genesis", { tolink = true; }; + ]; + + }); + + +(* "client_alpha": specific part of the client to interact with + the "alpha" protocol. *) +client_objects("alpha", { + opens = [ + + "-open"; "Error_monad"; "-open"; "Hash"; "-open"; "Tezos_data"; + "-open"; "Tezos_context"; +]; + packed_files = [ + "script_located_ir.ml"; + "michelson_macros.ml"; + "michelson_parser.ml"; + "client_proto_rpcs.ml"; + "client_proto_args.ml"; + "client_proto_contracts.ml"; + "client_proto_programs.ml"; + ] + liquidity_files + [ + "client_proto_context.ml"; + "client_proto_nonces.ml"; + "client_proto_main.ml"; + "baker/client_mining_blocks.ml"; + "baker/client_mining_operations.ml"; + "baker/client_mining_endorsement.ml"; + "baker/client_mining_denunciation.ml"; + "baker/client_mining_revelation.ml"; + "baker/client_mining_forge.ml"; + "baker/client_mining_daemon.ml"; + "baker/client_mining_main.ml"; + ]; + requires = [ + "tezos_embedded_protocol_alpha"; "node"; "client"; + ]; + }); + +client_objects("demo", { + opens = []; + packed_files = [ + "client_proto_rpcs.ml"; + "client_proto_main.ml"; + ]; + requires = [ + "tezos_embedded_protocol_demo"; "client" + ]; + }); + + +program_with_opens("tezos-client", { + has_byte = false; + asmlink = [ "-linkall";"-g" ]; + bytelink = [ "-linkall";"-g" ]; + files = [ + "client_main.ml"; + ]; + requires = [ + "tezos_embedded_protocol_alpha", { tolink = true }; + "tezos_embedded_protocol_demo", { tolink = true }; + "tezos_embedded_protocol_genesis", { tolink = true }; + "client_alpha"; "client_demo"; "client_genesis"; + "minutils"; "utils"; "compiler"; "node"; "client"; + ] + more_packages; + }); + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +(* + + +if( build_webclient ) { + + + + + +begin + + ocaml.dep = opens; + ocaml.asmcomp = compflags + opens; + ocaml.bytecomp = compflags + opens; + ocaml.requires = more_packages + [ + "minutils"; "utils"; "compiler"; "node"; + ]; + ocaml.files = [ "client/webclient_version.ml" ]; + OCaml.library("webclient", ocaml); +end + +main_js = "client/embedded/alpha/webclient/static/main.js"; + +begin + ocaml.has_byte = true; + ocaml.has_asm = false; + ppx = [ "-ppx"; "%{js_of_ocaml.ppx_FULL_SRC_DIR}%/ppx_js" ]; + ocaml.asmcomp = compflags + ppx; + ocaml.bytecomp = compflags + ppx; + ocaml.subdir = "client/embedded/alpha/webclient"; + ocaml.requires = [ + "lwt"; "cstruct"; "ocplib-json-typed.browser"; + "ocplib-json-typed.bson"; "ocplib-resto.directory"; + "js_of_ocaml.tyxml"; "js_of_ocaml.ppx"; + ] + + [ "minutils" ]; + ocaml.files = [ + "shared/webclient_proto_services.ml"; + "browser/webclient_main.ml"; + ]; + ocaml.build_rules = OCaml.make( + [main_js], + [ "%{main_FULL_DST_DIR}%/main.byte" ], + [[ "js_of_ocaml"; "+weak.js"; "%{main_FULL_DST_DIR}%/main.byte"; + "-o"; main_js ]]); + + OCaml.program("main", ocaml); +end + +begin + ocaml.has_byte = false; + + opens = [ + "-I"; "src/proto"; + "-open"; "Client_embedded_proto_alpha"; + "-open"; "Register_client_embedded_proto_alpha"; + "-open"; "Error_monad"; + "-open"; "Hash"; + "-open"; "Client_alpha"; + "-open"; "Tezos_context"; + ]; + + compflags = [ "-g"; "-short-paths"; "-safe-string"; + "-w"; "+27-30-40" ]; + ocaml.dep = opens; + ocaml.bytecomp = compflags + opens; + ocaml.asmcomp = compflags + opens; + + ocaml.requires = [ + "lwt"; "ocplib-json-typed"; "sodium"; "ocplib-ocamlres"; + ] + [ + "minutils"; "utils"; + "main"; "client_embedded_proto_alpha"; "client_alpha"; "webclient" ]; + + subdir = "client/embedded/alpha/webclient/"; + + ocaml.files = + OCaml.pack("Webclient_alpha", + (* empty asmcomp, to avoid -open with -pack: since + ocp-build does not provide -I during -pack, -open + would fail *) + ocaml + { asmcomp = [] }, + [ + subdir + "webclient_proto_static.ml"; + subdir + "shared/webclient_proto_services.ml"; + subdir + "webclient_proto_service_directory.ml" + (* , { + asmcomp = ocaml.asmcomp + extra_opens; + } *); + subdir + "webclient_proto_main.ml"; + ] + ); + + ocaml.build_rules = OCaml.make( + [subdir + "webclient_proto_static.ml"], [ main_js ], + [[ "ocp-ocamlres"; subdir + "static"; + "-o"; subdir + "webclient_proto_static.ml" ]]); + + OCaml.objects("webclient_alpha", ocaml); +end + + +begin + + subdir = "client/embedded/alpha/webclient/"; + compflags = compflags + ["-linkall"]; + opens = [ + "-open"; "Client_embedded_proto_demo"; + "-open"; "Register_client_embedded_proto_demo"; + "-open"; "Error_monad"; + "-open"; "Hash"; + ]; + + ocaml.dep = opens; + ocaml.bytecomp = compflags + opens; + ocaml.asmcomp = compflags + opens; + + requires = [ "minutils"; "utils"; "node"; "client" ] + + [ "lwt"; "ocplib-json-typed"; "sodium"; + "ocplib-ocamlres" ]; + + files = OCaml.pack("Webclient_demo", []); + + OCaml.objects("webclient_demo", ocaml); + + end + + + + begin + + subdir = "client/embedded/alpha/webclient/"; + compflags = compflags + ["-linkall"]; + opens = [ + "-open"; "client_embedded_proto_genesis"; + "-open"; "Register_client_embedded_proto_genesis"; + "-open"; "Error_monad"; + "-open"; "Hash"; + ]; + + ocaml.dep = opens; + ocaml.bytecomp = compflags + opens; + ocaml.asmcomp = compflags + opens; + + requires = [ "minutils"; "utils"; "node"; "client" ] + + [ "lwt"; "ocplib-json-typed"; "sodium"; + "ocplib-ocamlres" ]; + + files = OCaml.pack("Webclient_genesis", + [ ]); + + OCaml.objects("webclient_genesis", ocaml); + + end + + begin + + opens = [ "-open"; "Error_monad"; "-open"; "Hash"; "-open"; "Utils" ]; + + ocaml.dep = opens; + ocaml.bytecomp = compflags + opens; + ocaml.asmcomp = compflags + opens; + + + ocaml.files = [ + "webclient_static.ml"; + "webclient_main.ml"; + ]; + ocaml.requires = more_packages + + [ + "minutils"; "utils"; "compiler"; "node"; "client"; "webclient"; + "client_embedded_proto_alpha"; "client_embedded_proto_demo"; + "client_embedded_proto_genesis"; "client_alpha"; "client_demo"; + "client_genesis"; "webclient_alpha"; "webclient_demo"; + "webclient_genesis"; + ]; + + ocaml.build_rules = OCaml.make( + ["webclient_static.ml"], + List.map(function(file){ + return "webclient_static/" + file; + }, Sys_readdir("webclient_static")), + [[ "ocp-ocamlres"; "webclient_static"; + "-o"; "webclient_static.ml"; ]]); + OCaml.program("tezos-webclient", ocaml); + end + + +} + *) diff --git a/tests/Makefile b/tests/Makefile index b1ffbf72..26e079e6 100644 --- a/tests/Makefile +++ b/tests/Makefile @@ -4,6 +4,7 @@ all: clean: for dir in . others reverse; do \ rm -f $$dir/*~; \ + rm -f $$dir/*.cm?; \ rm -f $$dir/*.liq.tz; \ rm -f $$dir/*.liq.ocaml; \ rm -f $$dir/*.liq.simple; \ diff --git a/tests/others/auction.liq b/tests/others/auction.liq index 34b52cc4..efbd5cc8 100644 --- a/tests/others/auction.liq +++ b/tests/others/auction.liq @@ -1,17 +1,17 @@ (* Auction contract from https://www.michelson-lang.com/contract-a-day.html *) -[%%version 0.1] +[%%version 0.11] type storage = { auction_end : timestamp; highest_bid : tez; - bidder : key; + bidder : key_hash; } let%entry main - (parameter : key) + (parameter : key_hash) (storage : storage) - [%return : unit] = + : unit * storage = (* Check if auction has ended *) if Current.time () > storage.auction_end then Current.fail (); diff --git a/tests/others/broker.liq b/tests/others/broker.liq index dd602fcc..d16f0f28 100644 --- a/tests/others/broker.liq +++ b/tests/others/broker.liq @@ -1,5 +1,5 @@ -[%%version 0.1] +[%%version 0.11] type storage = { state : string; @@ -13,14 +13,14 @@ type storage = { let%entry main (parameter : timestamp) (storage : storage) - [%return : unit] = + : unit * storage = if storage.state <> "open" then Current.fail () else if Current.time () < storage.timeout then (* Before timeout *) (* We compute ((1 + P) + N) tez for keeping the contract alive *) - let pn = storage.pn in - let cost = 1.00tz + pn.(0) + pn.(1) in + let (pn0, pn1) = storage.pn in + let cost = 1.00tz + pn0 + pn1 in let b = Current.balance () in if cost < b then (* # Not enough cash, we just accept the transaction @@ -30,15 +30,17 @@ let%entry main (* # Enough cash, successful ending # We update the global*) let storage = storage.state <- "success" in + let (pn0, _) = storage.pn in let (_result, storage) = - Contract.call storage.x storage.pn.(0) storage () in + Contract.call storage.x pn0 storage () in + let (_, pn1) = storage.pn in let (_result, storage) = - Contract.call storage.a storage.pn.(1) storage () in + Contract.call storage.a pn1 storage () in ( (), storage ) else (* # After timeout, we refund # We update the global *) - let p = storage.pn.(0) in + let (p, _) = storage.pn in let storage = storage.state <- "timeout" in (* # We try to transfer the fee to the broker *) let bal = Current.balance () in diff --git a/tests/others/demo.liq b/tests/others/demo.liq index 95d06605..9b091eb6 100644 --- a/tests/others/demo.liq +++ b/tests/others/demo.liq @@ -1,14 +1,14 @@ -[%%version 0.1] +[%%version 0.11] let%entry main (parameter : string) (storage : (string, int) map) - [%return : unit] = + : unit * (string, int) map = let amount = Current.amount() in - if amount < ("5.00" : tez) then + if amount < 5.00tz then Current.fail () else match Map.find parameter storage with diff --git a/tests/others/morpion.liq b/tests/others/morpion.liq index 44586bf1..06c99a2a 100644 --- a/tests/others/morpion.liq +++ b/tests/others/morpion.liq @@ -9,7 +9,7 @@ type parameter = { play : bool; x : int; y : int } let contract ( storage : storage ) ( parameter : parameter ) - [%return : (bool option) option ] + : (bool option) option = let s = "This is a Tic Tac Toe game. Still work in progress" in diff --git a/tests/reverse/test1.tz b/tests/reverse/test1.tz index bedac32f..93b59fa3 100644 --- a/tests/reverse/test1.tz +++ b/tests/reverse/test1.tz @@ -1,4 +1,4 @@ -parameter key; +parameter key_hash; return unit; storage unit; code {CAR; DEFAULT_ACCOUNT; # Create an account for the recipient of the funds diff --git a/tests/test0.liq b/tests/test0.liq index 1196dea2..00759bcb 100644 --- a/tests/test0.liq +++ b/tests/test0.liq @@ -1,13 +1,14 @@ -[%%version 0.1] +[%%version 0.11] +type storage = string * (* 0: S *) + timestamp * (* 1: T *) + (tez * tez) * (* 2: P N *) + (unit,unit) contract * (* 3: X *) + (unit,unit) contract * (* 4: A *) + (unit,unit) contract (* 5: B *) let%entry main (parameter : timestamp) - (storage : string * (* 0: S *) - timestamp * (* 1: T *) - (tez * tez) * (* 2: P N *) - (unit,unit) contract * (* 3: X *) - (unit,unit) contract * (* 4: A *) - (unit,unit) contract) (* 5: B *) - [%return : unit] = + (storage : storage) + : (unit * storage) = ( (), storage ) diff --git a/tests/test1.liq b/tests/test1.liq index 672fb5ea..05174679 100644 --- a/tests/test1.liq +++ b/tests/test1.liq @@ -1,15 +1,17 @@ -[%%version 0.1] +[%%version 0.11] + +type storage = string * (* 0: S *) + timestamp * (* 1: T *) + (tez * tez) * (* 2: P N *) + (unit,unit) contract * (* 3: X *) + (unit,unit) contract * (* 4: A *) + (unit,unit) contract (* 5: B *) let%entry main (parameter : timestamp) - (storage : string * (* 0: S *) - timestamp * (* 1: T *) - (tez * tez) * (* 2: P N *) - (unit,unit) contract * (* 3: X *) - (unit,unit) contract * (* 4: A *) - (unit,unit) contract) (* 5: B *) - [%return : (timestamp * tez) * (tez * timestamp) ] = + (storage : storage) + : ((timestamp * tez) * (tez * timestamp)) * storage = let amount = Current.amount () in let x = (parameter, amount) in let y = (amount, parameter) in diff --git a/tests/test10.liq b/tests/test10.liq index 98b44126..1473f848 100644 --- a/tests/test10.liq +++ b/tests/test10.liq @@ -1,17 +1,18 @@ (* constructors *) -[%%version 0.1] +[%%version 0.11] -let%entry main - (parameter : bool) - (storage : +type s = bool * int option * (string,int) map - ) - [%return : unit] = - + +let%entry main + (parameter : bool) + (storage : s) + : unit * s = + (* options *) let x = 3 in let option = Some x in diff --git a/tests/test11.liq b/tests/test11.liq index 72c92f8d..238dcc0d 100644 --- a/tests/test11.liq +++ b/tests/test11.liq @@ -1,18 +1,18 @@ (* strings *) -[%%version 0.1] +[%%version 0.11] let%entry main (parameter : string) (storage : string) - [%return : unit] = - + : unit * string = + (* options *) let storage = if parameter = "" then storage else storage @ parameter - in + in ( (), storage ) diff --git a/tests/test12.liq b/tests/test12.liq index 41816f80..60edd7ac 100644 --- a/tests/test12.liq +++ b/tests/test12.liq @@ -1,13 +1,13 @@ (* sets *) -[%%version 0.1] +[%%version 0.11] let%entry main (parameter : string) (storage : string set) - [%return : unit] = - + : unit * string set = + let set = (Set : string set) in let set = Set.update "a" true set in let set = Set.update "b" true set in diff --git a/tests/test13.liq b/tests/test13.liq index f421a9a7..7e85401c 100644 --- a/tests/test13.liq +++ b/tests/test13.liq @@ -1,12 +1,12 @@ (* lists *) -[%%version 0.1] +[%%version 0.11] let%entry main (parameter : string) (storage : string list) - [%return : unit] = + : unit * string list = let set = ([] : string list) in let set = "a" :: set in @@ -18,7 +18,7 @@ let%entry main else match x with | [] -> set - | y :: z -> z + | _ :: z -> z in ( (), storage ) diff --git a/tests/test14.liq b/tests/test14.liq index 47ad59b5..fd496ccc 100644 --- a/tests/test14.liq +++ b/tests/test14.liq @@ -1,12 +1,12 @@ (* loops *) -[%%version 0.1] +[%%version 0.11] let%entry main (parameter : int) (storage : int set) - [%return : unit] = + : unit * int set = let x = Loop.loop (fun x -> diff --git a/tests/test15.liq b/tests/test15.liq index 70b1b229..67d58634 100644 --- a/tests/test15.liq +++ b/tests/test15.liq @@ -1,5 +1,5 @@ -[%%version 0.1] +[%%version 0.11] type point = { x : string; y : bool; z : int } type vector = { orig : point; dest : point } @@ -12,8 +12,8 @@ type storage = { let%entry main (parameter : int) (storage : storage) - [%return : unit] = + : unit * storage = - let storage = storage.v.dest.z <- parameter in +(* let storage = storage.v.dest.z <- parameter in *) let storage = storage.v.orig <- { x="0"; y=true; z = parameter } in ( (), storage ) diff --git a/tests/test16.liq b/tests/test16.liq index 3a202b8a..4ab6c6b1 100644 --- a/tests/test16.liq +++ b/tests/test16.liq @@ -2,7 +2,7 @@ let%entry main (parameter : int) (storage : unit) - [%return : unit] = + : unit * unit = let f = fun ( arg : unit * int ) -> arg.(0) in diff --git a/tests/test17.liq b/tests/test17.liq index e14686be..a14ebb4b 100644 --- a/tests/test17.liq +++ b/tests/test17.liq @@ -7,7 +7,7 @@ type storage = let%entry main (parameter : int) (storage : storage) - [%return : unit] = + : unit * storage = let _a = Nothing in let b = Int 3 in let c = String ("toto",0) in diff --git a/tests/test18.liq b/tests/test18.liq index 11528a51..a2e71618 100644 --- a/tests/test18.liq +++ b/tests/test18.liq @@ -2,7 +2,7 @@ let%entry main (parameter : int) (storage : nat) - [%return : int] = + : int * nat = match int storage / parameter with | None -> ( 0, 0p) diff --git a/tests/test19.liq b/tests/test19.liq new file mode 100644 index 00000000..00fa0063 --- /dev/null +++ b/tests/test19.liq @@ -0,0 +1,35 @@ + +type storage = { + key : key; + hash : string; + } + +let%entry main + (parameter : signature) + (storage : storage) + : ( (unit,unit) contract * (unit,int) contract) * + storage = + (* let c = Current.contract () in *) + let key_hash = Crypto.hash_key storage.key in + let manager = Contract.manager (Source : (unit,unit) contract) in + let spendable = Crypto.check storage.key (parameter, storage.hash) in + let amount = Current.amount () in + let amount = match amount / 2p with + None -> Current.fail () (* not possible *) + | Some qr -> qr + in + let account = Account.create + key_hash (Some manager) spendable + (amount.(0) + amount.(1)) in + let delegatable = false in + let c = Contract.create + key_hash (Some manager) + spendable delegatable + amount.(0) + (fun (x : unit * int) -> + let n = x.(1) in + n, n+1 + ) + 0 + in + ( (account,c), storage ) diff --git a/tests/test2.liq b/tests/test2.liq index 21a4f1de..7bdfd79d 100644 --- a/tests/test2.liq +++ b/tests/test2.liq @@ -1,15 +1,17 @@ -[%%version 0.1] +[%%version 0.11] + +type storage = string * (* 0: S *) + timestamp * (* 1: T *) + (tez * tez) * (* 2: P N *) + (unit,unit) contract * (* 3: X *) + (unit,unit) contract * (* 4: A *) + (unit,unit) contract (* 5: B *) let%entry main (parameter : timestamp) - (storage : string * (* 0: S *) - timestamp * (* 1: T *) - (tez * tez) * (* 2: P N *) - (unit,unit) contract * (* 3: X *) - (unit,unit) contract * (* 4: A *) - (unit,unit) contract) (* 5: B *) - [%return : (tez * tez) * (unit,unit) contract ] = + (storage : storage) + : ((tez * tez) * (unit,unit) contract) * storage = let x = storage.(2) in let y = storage.(3) in ( (x,y), storage ) diff --git a/tests/test20.liq b/tests/test20.liq new file mode 100644 index 00000000..8456e2f6 --- /dev/null +++ b/tests/test20.liq @@ -0,0 +1,10 @@ +type storage = tez * int * ((nat * unit) * bool) + +let%entry main + (parameter : unit) + (storage : storage) + : (nat * tez) * storage = + + let x, y = 0p, 1p in + let amount, _, ((n, _), b) = storage in + ((n + x + y, amount), storage) diff --git a/tests/test3.liq b/tests/test3.liq index f19aefed..e5a7b7dd 100644 --- a/tests/test3.liq +++ b/tests/test3.liq @@ -1,15 +1,17 @@ -[%%version 0.1] +[%%version 0.11] + +type storage = string * (* 0: S *) + timestamp * (* 1: T *) + (tez * tez) * (* 2: P N *) + (unit,unit) contract * (* 3: X *) + (unit,unit) contract * (* 4: A *) + (unit,unit) contract (* 5: B *) let%entry main (parameter : timestamp) - (storage : string * (* 0: S *) - timestamp * (* 1: T *) - (tez * tez) * (* 2: P N *) - (unit,unit) contract * (* 3: X *) - (unit,unit) contract * (* 4: A *) - (unit,unit) contract) (* 5: B *) - [%return : unit ] = + (storage : storage) + : (unit * storage) = let s = get storage 0 in let storage = set storage 0 s in ( (), storage ) diff --git a/tests/test4.liq b/tests/test4.liq index aa36c577..50403c77 100644 --- a/tests/test4.liq +++ b/tests/test4.liq @@ -1,14 +1,15 @@ -[%%version 0.1] +[%%version 0.11] +type storage = string * (* 0: S *) + timestamp * (* 1: T *) + (tez * tez) * (* 2: P N *) + (unit,unit) contract * (* 3: X *) + (unit,unit) contract * (* 4: A *) + (unit,unit) contract (* 5: B *) let%entry main (parameter : timestamp) - (storage : string * (* 0: S *) - timestamp * (* 1: T *) - (tez * tez) * (* 2: P N *) - (unit,unit) contract * (* 3: X *) - (unit,unit) contract * (* 4: A *) - (unit,unit) contract) (* 5: B *) - [%return : unit ] = + (storage : storage) + : (unit * storage) = let storage = set storage 1 parameter in ( (), storage ) diff --git a/tests/test5.liq b/tests/test5.liq index 9887b90c..dfc078a1 100644 --- a/tests/test5.liq +++ b/tests/test5.liq @@ -1,15 +1,17 @@ -[%%version 0.1] +[%%version 0.11] + +type storage = string * (* 0: S *) + timestamp * (* 1: T *) + (tez * tez) * (* 2: P N *) + (unit,unit) contract * (* 3: X *) + (unit,unit) contract * (* 4: A *) + (unit,unit) contract (* 5: B *) let%entry main (parameter : timestamp) - (storage : string * (* 0: S *) - timestamp * (* 1: T *) - (tez * tez) * (* 2: P N *) - (unit,unit) contract * (* 3: X *) - (unit,unit) contract * (* 4: A *) - (unit,unit) contract) (* 5: B *) - [%return : unit ] = + (storage : storage) + : (unit * storage) = let pn = get storage 2 in let p = get pn 0 in let p = p + 1tz in diff --git a/tests/test6.liq b/tests/test6.liq index f7f468fc..ee343310 100644 --- a/tests/test6.liq +++ b/tests/test6.liq @@ -1,15 +1,17 @@ -[%%version 0.1] +[%%version 0.11] + +type storage = string * (* 0: S *) + timestamp * (* 1: T *) + (tez * tez) * (* 2: P N *) + (unit,unit) contract * (* 3: X *) + (unit,unit) contract * (* 4: A *) + (unit,unit) contract (* 5: B *) let%entry main (parameter : timestamp) - (storage : string * (* 0: S *) - timestamp * (* 1: T *) - (tez * tez) * (* 2: P N *) - (unit,unit) contract * (* 3: X *) - (unit,unit) contract * (* 4: A *) - (unit,unit) contract) (* 5: B *) - [%return : unit ] = + (storage : storage) + : (unit * storage) = let pn = get storage 2 in let storage = set storage 2 pn in ( (), storage ) diff --git a/tests/test7.liq b/tests/test7.liq index 01784ede..14ecd25c 100644 --- a/tests/test7.liq +++ b/tests/test7.liq @@ -1,11 +1,13 @@ -[%%version 0.1] +[%%version 0.11] + +type t = tez +type s = (t * tez) let%entry main (parameter : timestamp) - (storage : (tez * tez) (* 2: P N *) - ) - [%return : int list] = + (storage : s) + : (int list * (tez * t)) = let p = get storage 0 in let n = get storage 1 in diff --git a/tests/test8.liq b/tests/test8.liq index f7656b8e..17fe7167 100644 --- a/tests/test8.liq +++ b/tests/test8.liq @@ -1,11 +1,11 @@ -[%%version 0.1] +[%%version 0.11] let%entry main (parameter : timestamp) (storage : tez * tez (* 2: P N *) ) - [%return : unit] = + : unit * (tez * tez) = let p = get storage 1 in let storage = set storage 1 p in ( (), storage ) diff --git a/tests/test9.liq b/tests/test9.liq index 9197463b..9a6eb4a8 100644 --- a/tests/test9.liq +++ b/tests/test9.liq @@ -1,18 +1,18 @@ (* constants *) -[%%version 0.1] +[%%version 0.11] + +type storage = bool * + int option * + (string,int) map * + int set * + int list let%entry main (parameter : bool) - (storage : - bool * - int option * - (string,int) map * - int set * - int list - ) - [%return : unit] = + (storage : storage) + : unit * storage = (* booleans *) let bool = diff --git a/tests/test_closure.liq b/tests/test_closure.liq index de7cf046..81a064ef 100644 --- a/tests/test_closure.liq +++ b/tests/test_closure.liq @@ -1,10 +1,10 @@ -[%%version 0.1] +[%%version 0.11] let%entry main (parameter : int) (storage : int) - [%return : unit] = + : unit * int = let x = parameter + 10 in let f = fun ( arg : int * int ) -> arg.(1) + x diff --git a/tests/test_closure2.liq b/tests/test_closure2.liq index bdc6ecd5..454b24c8 100644 --- a/tests/test_closure2.liq +++ b/tests/test_closure2.liq @@ -1,10 +1,10 @@ -[%%version 0.1] +[%%version 0.11] let%entry main (parameter : int) (storage : int) - [%return : unit] = + : unit * int = let x = parameter + 10 in let f ( arg : int * int ) (y : int) = arg.(0) + x + y diff --git a/tests/test_closure3.liq b/tests/test_closure3.liq index e7c6ff9f..3ca4f304 100644 --- a/tests/test_closure3.liq +++ b/tests/test_closure3.liq @@ -1,10 +1,10 @@ -[%%version 0.1] +[%%version 0.11] let%entry main (parameter : int) (storage : int) - [%return : unit] = + : unit * int = let x = parameter + 10 in let f ( arg : int * int ) (y : int) = 0 diff --git a/tests/test_extfun.liq b/tests/test_extfun.liq index 53c96bbc..e78da63c 100644 --- a/tests/test_extfun.liq +++ b/tests/test_extfun.liq @@ -1,11 +1,11 @@ -[%%version 0.1] +[%%version 0.11] -let f ( arg : unit * int ) = arg.(0) +let f ((x : unit), (_ : int) ) = x let%entry main (parameter : int) (storage : unit) - [%return : unit] = + : unit * unit = let storage = f (storage, parameter) in ( (), storage ) diff --git a/tests/test_if.liq b/tests/test_if.liq index 059c1c6b..8e1a7414 100644 --- a/tests/test_if.liq +++ b/tests/test_if.liq @@ -1,18 +1,19 @@ (* constants *) -[%%version 0.1] +[%%version 0.11] -let%entry main - (parameter : bool) - (storage : +type storage = bool * int option * (string,int) map * int set * int list - ) - [%return : unit] = + +let%entry main + (parameter : bool) + (storage : storage) + : unit * storage = (* booleans *) let bool = diff --git a/tests/test_ifcons.liq b/tests/test_ifcons.liq index 0e0319e3..105b4a5f 100644 --- a/tests/test_ifcons.liq +++ b/tests/test_ifcons.liq @@ -1,12 +1,12 @@ (* lists *) -[%%version 0.1] +[%%version 0.11] let%entry main (parameter : string) (storage : string list) - [%return : unit] = + : unit * string list = let a = "1" in let set = ([] : string list) in @@ -15,7 +15,7 @@ let%entry main let storage = match x with | [] -> set - | y :: z -> z + | _ :: z -> z in ( (), storage ) diff --git a/tests/test_left.liq b/tests/test_left.liq index 5cf443ca..d177386c 100644 --- a/tests/test_left.liq +++ b/tests/test_left.liq @@ -2,7 +2,7 @@ let%entry main (parameter : int) (storage : int) - [%return : unit] = + : unit * int = let a = (Left 3 : (_, string) variant) in let b = (Right a : (int, _) variant) in @@ -11,7 +11,7 @@ let%entry main | Right r -> match r with | Left x -> x - | Right s -> storage + | Right _ -> storage in ( (), storage ) diff --git a/tests/test_left_constr.liq b/tests/test_left_constr.liq index 6d8c293d..aa1fb07a 100644 --- a/tests/test_left_constr.liq +++ b/tests/test_left_constr.liq @@ -2,6 +2,6 @@ let%entry main (parameter : int) (storage : (int, string) variant) - [%return : unit] = + : unit * (int, string) variant = let a = (Left parameter : (_, string) variant) in ( (), a ) diff --git a/tests/test_left_match.liq b/tests/test_left_match.liq index 2de92a21..0e8d58da 100644 --- a/tests/test_left_match.liq +++ b/tests/test_left_match.liq @@ -2,8 +2,8 @@ let%entry main (parameter : (int, string) variant) (storage : int) - [%return : string] = - + : string * int = + match parameter with | Left left -> ("", left) | Right right -> (right, storage) diff --git a/tests/test_loop.liq b/tests/test_loop.liq index 07863080..541195f7 100644 --- a/tests/test_loop.liq +++ b/tests/test_loop.liq @@ -1,12 +1,12 @@ (* loops *) -[%%version 0.1] +[%%version 0.11] let%entry main (parameter : int) (storage : int) - [%return : unit] = + : unit * int = let storage = Loop.loop (fun x -> diff --git a/tests/test_map.liq b/tests/test_map.liq index b2b0b475..ceedfed8 100644 --- a/tests/test_map.liq +++ b/tests/test_map.liq @@ -1,13 +1,13 @@ (* List.map *) -[%%version 0.1] +[%%version 0.11] let succ (x : int) = x + 1 let%entry main (parameter : int) (storage : int list) - [%return : unit] = + : unit * int list = let l = List.map succ storage in ( (), l) diff --git a/tests/test_map_closure.liq b/tests/test_map_closure.liq index a6e685cb..c322218b 100644 --- a/tests/test_map_closure.liq +++ b/tests/test_map_closure.liq @@ -5,7 +5,7 @@ let%entry main (parameter : int) (storage : int list) - [%return : unit] = + : unit * int list = let add_param (x : int) = x + parameter in let l = List.map add_param storage in ( (), l ) diff --git a/tests/test_mapmap_closure.liq b/tests/test_mapmap_closure.liq index d597a9f1..503700cb 100644 --- a/tests/test_mapmap_closure.liq +++ b/tests/test_mapmap_closure.liq @@ -1,7 +1,8 @@ +[%%version 0.11] let%entry main (parameter : string) (storage : (string, tez) map) - [%return : (string, bool) map] = + : (string, bool) map * (string, tez) map = let amount = Current.amount() in let f (arg: (string * tez)) = diff --git a/tests/test_mapreduce_closure.liq b/tests/test_mapreduce_closure.liq index 41ecdf7f..ae3c7694 100644 --- a/tests/test_mapreduce_closure.liq +++ b/tests/test_mapreduce_closure.liq @@ -1,7 +1,7 @@ let%entry main (parameter : string) (storage : (string, tez) map) - [%return : bool] = + : bool * (string, tez) map = let amount = Current.amount() in let f (arg: (string * tez) * bool) = diff --git a/tests/test_option.liq b/tests/test_option.liq index 3d736789..0418c5d9 100644 --- a/tests/test_option.liq +++ b/tests/test_option.liq @@ -1,7 +1,7 @@ let%entry main (parameter : int option) (storage : unit) - [%return : int] = + : int * unit = let x = match parameter with | None -> 1 diff --git a/tests/test_reduce_closure.liq b/tests/test_reduce_closure.liq index 9d051ff3..3ae6dea4 100644 --- a/tests/test_reduce_closure.liq +++ b/tests/test_reduce_closure.liq @@ -5,7 +5,7 @@ let%entry main (parameter : int list) (storage : int) - [%return : unit] = + : unit * int = let c = 1 in diff --git a/tests/test_rev.liq b/tests/test_rev.liq index a521d0b8..81b036af 100644 --- a/tests/test_rev.liq +++ b/tests/test_rev.liq @@ -1,10 +1,10 @@ (* List.rev *) -[%%version 0.1] +[%%version 0.11] let%entry main (parameter : int) (storage : int list) - [%return : unit] = + : unit * int list = let l = List.rev storage in ( (), l ) diff --git a/tests/test_right_constr.liq b/tests/test_right_constr.liq index b82caabb..af1e2312 100644 --- a/tests/test_right_constr.liq +++ b/tests/test_right_constr.liq @@ -2,6 +2,6 @@ let%entry main (parameter : string) (storage : (int, string) variant) - [%return : unit] = + : unit = let a = (Right parameter : (int, _) variant) in ( (), a ) diff --git a/tests/test_setreduce_closure.liq b/tests/test_setreduce_closure.liq index ca072189..7b0a63bc 100644 --- a/tests/test_setreduce_closure.liq +++ b/tests/test_setreduce_closure.liq @@ -1,7 +1,7 @@ let%entry main (parameter : string) (storage : tez set) - [%return : bool] = + : bool * tez set = let amount = Current.amount() in let f (arg: tez * bool) = diff --git a/tests/test_transfer.liq b/tests/test_transfer.liq index 83358351..14ad0b44 100644 --- a/tests/test_transfer.liq +++ b/tests/test_transfer.liq @@ -1,12 +1,12 @@ (* transfers *) -[%%version 0.1] +[%%version 0.11] let%entry main (parameter : (unit,unit) contract) (storage : tez) - [%return : unit] = + : unit * tez = let amount = Current.amount () in let storage = storage + amount in diff --git a/tools/liquidity/.merlin b/tools/liquidity/.merlin index 23965ef5..9d94d61b 100644 --- a/tools/liquidity/.merlin +++ b/tools/liquidity/.merlin @@ -1,6 +1,9 @@ S ./** S ../../libs/** B ../../_obuild/** + +FLG -rectypes + PKG ocplib-file PKG ocplib-ocamlres PKG ocplib-endian diff --git a/tools/liquidity/build.ocp2 b/tools/liquidity/build.ocp2 index 40c1f11c..e30dc088 100644 --- a/tools/liquidity/build.ocp2 +++ b/tools/liquidity/build.ocp2 @@ -27,15 +27,21 @@ *) - -OCaml.library("ocplib-liquidity", - ocaml + { - files = [ - "liquidVersion.ml", { ocp2ml=true; +if(with_version){ + version_info = { ocp2ml=true; env_strings = [ "ocp::commit"; "ocp::dates"; ]; }; +} else { + version_info = {}; +} + +OCaml.library("ocplib-liquidity", + ocaml + { + files = [ + + "liquidVersion.ml", version_info; "liquidMisc.ml"; "liquidTypes.ml"; @@ -62,9 +68,9 @@ OCaml.library("ocplib-liquidity", }); + OCaml.library("ocplib-liquidity-ocaml", ocaml + { - version = version; files = [ "ocaml/liquidOCamlParser.mly"; "ocaml/liquidOCamlLexer.mll"; @@ -78,10 +84,25 @@ OCaml.library("ocplib-liquidity-ocaml", requires = [ "ocplib-liquidity"; "compiler-libs.common"; + "compiler-libs.bytecomp"; ]; }); +OCaml.program("ocp-liquidity-comp", + ocaml + { + requires = [ "ocplib-liquidity-ocaml" ]; + files = [ + "ocaml/liquidOCamlPparse.ml"; + + "ocaml/liquidOCamlTranslate.ml"; + + + "ocaml/liquidOCamlCompile.ml"; + "ocaml/liquidOCamlMain.ml"; + ]; + }); + if ( with_tezos ) { OCaml.library("ocplib-liquidity-with-tezos", ocaml + { @@ -136,3 +157,9 @@ OCaml.program("liquidity-mini", ]; }); + +OCaml.library("liquidity-env", + ocaml + { + files = [ "env/liquidityEnv.ml" ]; + requires = [ "zarith" ]; + }); diff --git a/tools/liquidity/env/liquidityEnv.ml b/tools/liquidity/env/liquidityEnv.ml new file mode 100644 index 00000000..5b96026a --- /dev/null +++ b/tools/liquidity/env/liquidityEnv.ml @@ -0,0 +1,349 @@ +(**************************************************************************) +(* *) +(* Copyright (c) 2017 . *) +(* Fabrice Le Fessant, OCamlPro SAS *) +(* *) +(* All rights reserved. No warranty, explicit or implicit, provided. *) +(* *) +(**************************************************************************) + +(* This module is completely unsafe: it can only by used to execute a +file that has been correctly typechecked by the `liquidity` +typechecker. *) + +type timestamp = string +type kind = Tez | Int +type integer = Z.t * kind +type tez = integer +type nat = integer +type key +type key_hash +type signature +type ('arg, 'res) contract + +module Tez : sig + + val of_string : string -> tez + + end = struct + + let of_string s = + let (tezzies, centiles) = + try + let pos = String.index s '.' in + let tezzies = String.sub s 0 pos in + let len = String.length s in + let centiles = "0" ^ String.sub s (pos+1) (len-pos-1) in + Z.of_string tezzies, Z.of_string centiles + with Not_found -> + Z.of_string s, Z.of_int 0 + in + Z.add (Z.mul (Z.of_int 100) tezzies) centiles, Tez + +end + +module Int : sig + + val of_string : string -> integer + +end = struct + + let of_string n = Z.of_string n, Int + +end + +module Current : sig + + val amount : unit -> tez + val fail : unit -> 'a + val time : unit -> timestamp + val balance : unit -> tez + val gas : unit -> tez (* NOT TESTED *) + val contract : unit -> ('a,'b) contract (* unsafe, NOT IMPLEMENTED !! *) + val source : unit -> ('a,'b) contract (* NOT TESTED *) + +end = struct + + let amount () = Z.of_int 100, Tez + let fail () = assert false (* TODO *) + let time () = assert false (* TODO *) + let balance () = assert false (* TODO *) + let gas () = assert false + let contract () = assert false + let source () = assert false +end + + +module Array : sig + val get : 'a -> integer -> 'b + val set : 'a -> integer -> 'b -> 'a + +end = struct (* Arrays are for tuples, not typable in OCaml *) + + let get t n = + let n,_ = n in + let n = Z.to_int n in + Obj.magic (Obj.field (Obj.magic t) n) + + let set t n x = + let n,_ = n in + let n = Z.to_int n in + let t = Obj.repr t in + let t = Obj.dup t in + Obj.set_field t n (Obj.repr x); + Obj.magic t + +end + +module Map : sig + + type ('key, 'value) map + + val empty : unit -> ('key,'value) map + val make : ('key * 'value) list -> ('key, 'value) map + val reduce : ( ('key * 'value) * 'acc -> 'acc) -> + ('key,'value) map -> 'acc -> 'acc + + val map : ( 'key * 'value -> 'res) -> + ('key,'value) map -> + ('key,'res) map + + val find : 'key -> ('key, 'value) map -> 'value option + + val update : 'key -> 'value option -> ('key, 'value) map -> + ('key, 'value) map + + val mem : 'key -> ('key, 'value) map -> bool (* NOT TESTED *) + val size : ('key, 'value) map -> int + +end = struct + + module ObjMap = Map.Make(struct + type t = Obj.t + let compare = compare + end) + + type ('key, 'value) map + let empty _ = Obj.magic ObjMap.empty + let make list = + let map = + List.fold_left (fun map (key,value) -> + let key = Obj.repr key in + let value = Obj.repr value in + ObjMap.add key value map + ) (empty 0) list + in + Obj.magic map + + let reduce f map acc = + let f = (Obj.magic f : (Obj.t * 'value) * Obj.t -> Obj.t) in + let acc = Obj.repr acc in + let map = (Obj.magic map : 'value ObjMap.t) in + let (acc : Obj.t) = ObjMap.fold (fun key value acc -> + f ( (key,value), acc ) + ) map acc + in + Obj.magic acc + + let map f map = + let f = (Obj.magic f : Obj.t * 'value -> 'value) in + let map = (Obj.magic map : 'value ObjMap.t) in + let map = ObjMap.map (fun key value -> f (key,value)) map in + Obj.magic map + + let find key map = + try + let key = Obj.repr key in + let map = (Obj.magic map : 'value ObjMap.t) in + Some (ObjMap.find key map) + with Not_found -> None + + let update key value map = assert false (* TODO *) + let mem key map = assert false (* TODO, NOT TESTED *) + let size map = ObjMap.cardinal (Obj.magic map) + +end +include Array (* Remove ? *) + + +type ('key,'value) map = ('key,'value) Map.map + +module Set : sig + + type 'key set + val empty : unit -> 'key set + val make : 'key list -> 'key set + val update : 'key -> bool -> 'key set -> 'key set + val mem : 'key -> 'key set -> bool + val reduce : ( 'key * 'acc -> 'acc) -> + 'key set -> 'acc -> 'acc + val map : ('key -> 'res) -> 'key set -> 'res set + val size : 'key set -> int + +end = struct + + module ObjSet = Set.Make(struct + type t = Obj.t + let compare = compare + end) + + type 'key set + + let empty _ = Obj.magic ObjSet.empty + let make list = + let set = + List.fold_left (fun set key -> + let key = Obj.repr key in + ObjSet.add key set + ) (empty 0) list + in + Obj.magic set + let update key bool set = + let key = Obj.repr key in + let set = (Obj.magic set : ObjSet.t) in + let set = + if bool then + ObjSet.add key set + else + ObjSet.remove key set + in + Obj.magic set + let mem key set = + let key = Obj.repr key in + let set = (Obj.magic set : ObjSet.t) in + ObjSet.mem key set + + let reduce f set acc = + let f = (Obj.magic f : Obj.t * Obj.t -> Obj.t) in + let acc = Obj.repr acc in + let set = (Obj.magic set : ObjSet.t) in + let (acc : Obj.t) = ObjSet.fold (fun key acc -> + f (key, acc ) + ) set acc + in + Obj.magic acc + + let map f set = assert false (* TODO, NOT TESTED *) + let size set = ObjSet.cardinal (Obj.magic set) + +end + +type 'key set = 'key Set.set + +type int = integer + +let (+) (x,unit) (y,_) = Z.add x y, unit +let (-) (x,unit) (y,_) = Z.sub x y, unit +let (@) = (^) + + +let ediv x y = + try + let (q, r) = Z.ediv_rem x y in + Some (q, r) + with _ -> None + +let (/) (x,xu) (y,yu) = + try + let (q, r) = Z.ediv_rem x y in + let (qu, ru) = + match xu, yu with + Tez, Tez -> Int, Tez + | Tez, Int -> Tez, Tez + | Int, Int -> Int, Int + | _ -> assert false + in + Some ((q,qu), (r,ru)) + with _ -> None + +let ( * ) (x,xu) (y,yu) = (* NOT TESTED *) + let u = + match xu, yu with + | Int, Int -> Int + | Tez, Int + | Int, Tez -> Tez + | _ -> assert false + in + Z.mul x y, u + + +module Lambda : sig + val pipe : 'a -> ('a -> 'b) -> 'b +end = struct + let pipe x f = f x +end + +module Loop : sig + val loop : ('a -> bool * 'a) -> 'a -> 'a +end = struct + let rec loop f x = + let (bool, ret) = f x in + if bool then loop f ret + else ret +end + +let int x = x + +module Contract : sig + + val call : ('arg, 'res) contract -> tez -> 'storage -> 'arg -> + 'res * 'storage + + val manager : ('a,'b) contract -> key_hash + val create : key_hash -> key_hash option -> + bool -> bool -> tez -> + ( ('a *'b) -> ('c * 'b) ) -> 'b -> + ('a,'c) contract + val source : unit -> ('a,'b) contract + +end = struct + + let call contract amount storage arg = assert false (* TODO *) + let manager _contract = assert false (* TODO *) + let create _key _manager + _spendable _delegatable _amount + _f _storage = assert false (* TODO *) + let source () = assert false (* TODO *) +end + +type ('a,'b) variant = Left of 'a | Right of 'b + +module List : sig + + val reduce : ('a * 'b -> 'b) -> 'a list -> 'b -> 'b + val map : ('a -> 'b) -> 'a list -> 'b list + val rev : 'a list -> 'a list + val size : 'a list -> int + +end = struct + + let rec reduce f list b = + match list with + | [] -> b + | a :: list -> + reduce f list (f (a,b)) + + let map = List.map + let rev = List.rev + let size list = Z.of_int (List.length list), Int + +end + +module Account : sig + val create : key_hash -> key_hash option -> + bool -> tez -> (unit,unit) contract + val default : key_hash -> (unit,unit) contract +end = struct + let create key key_opt _spendable _amount = assert false (* TODO NOT TESTED *) + let default _key = assert false (* TODO *) +end + +module Crypto : sig + val hash : 'a -> string + val hash_key : key -> key_hash + val check : key -> signature * string -> bool +end = struct + let hash _ = assert false (*TODO *) + let hash_key _ = assert false (*TODO *) + let check _key (_sig, _hash) = assert false (* TODO *) +end diff --git a/tools/liquidity/liquidBoundVariables.ml b/tools/liquidity/liquidBoundVariables.ml index 4963d26b..dc8a8414 100644 --- a/tools/liquidity/liquidBoundVariables.ml +++ b/tools/liquidity/liquidBoundVariables.ml @@ -96,13 +96,18 @@ let rec bv code = bv arg | MatchVariant (exp, _loc, args) -> - StringSet.union (bv exp) - (List.fold_left (fun set (_constr, var_args, exp) -> - StringSet.union set ( - List.fold_left (fun set var_arg -> - StringSet.remove var_arg set - ) (bv exp) var_args) - ) StringSet.empty args) + StringSet.union (bv exp) + (List.fold_left (fun set (pat, exp) -> + let bv_exp = bv exp in + let bv_case = match pat with + | CConstr (_constr, var_args) -> + List.fold_left (fun set var_arg -> + StringSet.remove var_arg set + ) bv_exp var_args + | CAny -> bv_exp + in + StringSet.union set bv_case + ) StringSet.empty args) let mk desc exp bv = { desc; ty = exp.ty; bv; fail = exp.fail } @@ -277,18 +282,22 @@ let rec bound code = | MatchVariant (exp, loc, args) -> let exp = bound exp in let args = - List.map (fun (constr, var_args, exp) -> - (constr, var_args, bound exp) + List.map (fun (pat, exp) -> + (pat, bound exp) ) args in - let bv = - StringSet.union (exp.bv) - (List.fold_left (fun set (_constr, var_args, exp) -> - StringSet.union set ( - List.fold_left (fun set var_arg -> - StringSet.remove var_arg set - ) exp.bv var_args) - ) StringSet.empty args) + let bv = List.fold_left (fun set (pat, exp) -> + let bv_exp = bv exp in + let bv_case = match pat with + | CConstr (_constr, var_args) -> + List.fold_left (fun set var_arg -> + StringSet.remove var_arg set + ) bv_exp var_args + | CAny -> bv_exp + in + StringSet.union set bv_case + ) StringSet.empty args in + let bv = StringSet.union (exp.bv) bv in let desc = MatchVariant(exp,loc,args) in mk desc code bv diff --git a/tools/liquidity/liquidCheck.ml b/tools/liquidity/liquidCheck.ml index d3cb47e5..c6e58386 100644 --- a/tools/liquidity/liquidCheck.ml +++ b/tools/liquidity/liquidCheck.ml @@ -7,6 +7,9 @@ (* *) (**************************************************************************) +(* TODO: we should check that the keys of maps and sets are comparable, + in particular to avoid using `key` in maps instead of `key_hash`. *) + (* TODO: we don't handle correctly all the occurrences of Tfail, i.e. when an error occurs in a sub-part of a type and another type is expected, we should probably unify. @@ -37,7 +40,7 @@ let comparable_ty ty1 ty2 = | (Tint|Tnat|Ttez), (Tint|Tnat|Ttez) | Ttimestamp, Ttimestamp | Tstring, Tstring - | Tkey, Tkey -> true + | Tkey_hash, Tkey_hash -> true | _ -> false let error_not_comparable loc prim ty1 ty2 = @@ -223,6 +226,29 @@ let type_error loc msg actual expected = (LiquidPrinter.Liquid.string_of_type expected) (LiquidPrinter.Liquid.string_of_type actual) + +let error_prim loc prim args expected_args = + let prim = LiquidTypes.string_of_primitive prim in + let nargs = List.length args in + let nexpected = List.length expected_args in + if nargs <> nexpected then + error loc "Prim %S: %d args provided, %d args expected" + prim nargs nexpected + else + let args = List.map (fun { ty } -> ty) args in + List.iteri (fun i (arg, expected) -> + if arg <> expected then + error loc + "Primitive %s, argument %d:\nExpected type:%sProvided type:%s" + prim (i+1) + (LiquidPrinter.Liquid.string_of_type expected) + (LiquidPrinter.Liquid.string_of_type arg) + + ) (List.combine args expected_args); + Printf.eprintf "Fatal error on typechecking primitive %S\n%!" prim; + assert false + + (* approximate location *) let rec loc_exp env e = match e.desc with | Var (_, loc, _) @@ -255,502 +281,502 @@ let rec loc_exp env e = match e.desc with * whether the expression can fail * whether the expression performs a TRANSFER_TOKENS *) - let rec typecheck env ( exp : LiquidTypes.syntax_exp ) = - match exp.desc with - - | Const (ty, cst ) -> - let desc = Const (ty, cst ) in - let fail = false in - mk desc ty fail, fail, false - - | Let (name, loc, exp, body) -> - let exp, fail1, transfer1 = typecheck env exp in - if exp.ty = Tfail then - error loc "cannot assign failure"; - let env = maybe_reset_vars env transfer1 in - let (new_name, env, count) = new_binding env name exp.ty in - let body, fail2, transfer2 = typecheck env body in - let desc = Let (new_name, loc, exp, body ) in - check_used env name loc count; - if (not transfer1) && (not fail1) then begin - match !count with - | 0 -> - env.to_inline := StringMap.add new_name const_unit - ! (env.to_inline) - | 1 -> - env.to_inline := StringMap.add new_name exp - ! (env.to_inline) - | _ -> () - end; - let fail = fail1 || fail2 in - mk desc body.ty fail, fail, transfer1 || transfer2 - - | Var (name, loc, labels) -> - let e = find_var env loc name in - let e = - List.fold_left - (fun e label -> - let ty_name, ty = match e.ty with - | Ttype (ty_name, ty) -> ty_name, ty - | _ -> - error loc "not a record" - in - let arg1 = mk e.desc ty false in - let n = - try - let (ty_name', n, _label_ty) = - StringMap.find label env.env.labels in - if ty_name' <> ty_name then - error loc "label for wrong record"; - n - with Not_found -> - error loc "bad label" - in - let arg2 = mk_nat n in - let args = [ arg1; arg2] in - let prim, ty = typecheck_prim1 env Prim_tuple_get loc args in - mk (Apply(prim, loc, args)) ty false - ) e labels in - e, false, false - - | SetVar (name, loc, [], e) -> typecheck env e - - | SetVar (name, loc, label :: labels, arg) -> - let arg1_t = find_var env loc name in - let ty = arg1_t.ty in - let ty_name, tuple_ty = match ty with - | Ttype (ty_name, ty) -> ty_name, ty - | _ -> - error loc "not a record" - in - let arg1 = { arg1_t with ty = tuple_ty } in - let n = - try - let (ty_name', n, _label_ty) = - StringMap.find label env.env.labels in - if ty_name' <> ty_name then - error loc "label for wrong record"; - n - with Not_found -> - error loc "bad label" - in - let arg2 = mk_nat n in - let arg, can_fail = - match labels with - | [] -> - let (arg, can_fail, transfer) = typecheck env arg in - if transfer then - error loc "transfer within set-field"; - (arg, can_fail) - | _::_ -> - let args = [ arg1; arg2] in - let prim, ty = typecheck_prim1 env Prim_tuple_get loc args in - let get_exp = mk (Apply(prim, loc, args)) ty false in - let tmp_name = uniq_ident env "tmp#" in - let (new_name, env, count) = new_binding env tmp_name ty in - let body, can_fail, _transfer = - typecheck env - { exp with desc = SetVar (tmp_name, loc, - labels, arg) } - in - let desc = Let (new_name, loc, get_exp, body ) in - mk desc body.ty can_fail, can_fail - - in - let args = [ arg1; arg2; arg] in - let prim, tuple_ty' = typecheck_prim1 env Prim_tuple_set loc args in - mk (Apply(prim, loc, args)) ty can_fail, can_fail, false - - | Seq (exp1, exp2) -> - let exp1, fail1, transfer1 = - typecheck_expected "sequence" env Tunit exp1 in - let exp2, fail2, transfer2 = typecheck env exp2 in - let desc = Seq (exp1, exp2) in - (* TODO: if not fail1 then remove exp1 *) - let can_fail = fail1 || fail2 in - mk desc exp2.ty can_fail, can_fail, transfer1 || transfer2 - - | If (cond, ifthen, ifelse) -> - let cond, fail1, transfer1 = - typecheck_expected "if-cond" env Tbool cond in - if transfer1 then - error (noloc env) "transfer within if condition"; - let ifthen, fail2, transfer2 = typecheck env ifthen in - let ifelse, fail3, transfer3, ty = - if ifthen.ty = Tfail then - let ifelse, fail3, transfer3 = typecheck env ifelse in - ifelse, fail3, transfer3, ifelse.ty - else - let ifelse, fail3, transfer3 = - typecheck_expected "if-result" env ifthen.ty ifelse in - ifelse, fail3, transfer3, ifthen.ty - in - let desc = If(cond, ifthen, ifelse) in - let can_fail = fail1 || fail2 || fail3 in - mk desc ty can_fail, - can_fail, - transfer2 || transfer3 - - | LetTransfer (storage_name, result_name, - loc, - contract_exp, tez_exp, - storage_exp, arg_exp, body) -> - let tez_exp, fail1, transfer1 = - typecheck_expected "call-amount" env Ttez tez_exp in - let contract_exp, fail2, transfer2 = typecheck env contract_exp in - begin - match contract_exp.ty with - | Tcontract (arg_ty, return_ty) -> - let arg_exp, fail3, transfer3 = - typecheck_expected "call-arg" env arg_ty arg_exp in - let storage_exp, fail4, transfer4 = - typecheck_expected "call-storage" - env env.contract.storage storage_exp in - if transfer1 || transfer2 || transfer3 || transfer4 then - error loc "transfer within transfer arguments"; - let (new_storage, env, storage_count) = - new_binding env storage_name env.contract.storage in - let (new_result, env, result_count) = - new_binding env result_name return_ty in - let body, fail5, transfer5 = typecheck env body in - check_used env storage_name loc storage_count; - check_used env result_name loc result_count; - let desc = LetTransfer(new_storage, new_result, - loc, - contract_exp, tez_exp, - storage_exp, arg_exp, body) - in - mk desc body.ty true, - true, true - | _ -> - LiquidLoc.raise_error "typecheck error: Contract expected%!" - end - - - | Apply (Prim_unknown, loc, - ({ desc = Var (name, varloc, [])} as f) :: ((_ :: _) as r)) - when StringMap.mem name env.vars -> - let exp = List.fold_left (fun f x -> - { exp with desc = Apply (Prim_exec, loc, [x; f]) } - ) f r - in - typecheck env exp - - | Apply (Prim_unknown, loc, - [ { desc = Var (name, _, _)} as f; x ]) - when StringMap.mem name env.vars -> - typecheck env { exp with - desc = Apply(Prim_exec, loc, [x;f]) } - - | Apply (Prim_unknown, loc, - ({ desc = Var (name, varloc, [])} ::args)) -> - let prim = - try - LiquidTypes.primitive_of_string name - with Not_found -> - error loc "Unknown identifier %S" name - in - typecheck env { exp with - desc = Apply(prim, loc, args) } - - | Apply (Prim_unknown, loc, [f ; x ]) -> - typecheck env { exp with - desc = Apply(Prim_exec, loc, [x; f]) } - - - (* List.rev -> List.reduce (::) *) - | Apply (Prim_list_rev, loc, [l]) -> - let l, fail, transfer = typecheck env l in - if transfer then error loc "transfer within List.rev args"; - let elt_ty = match l.ty with - | Tlist ty -> ty - | _ -> error loc "Argument of List.rev must be a list" - in - let arg_name = uniq_ident env "arg" in - let list_ty = Tlist elt_ty in - let arg_ty = Ttuple [elt_ty; list_ty] in - let arg = mk (Var (arg_name, loc, [])) arg_ty false in - let e = mk (Apply(Prim_tuple_get, loc, [arg; mk_nat 0])) elt_ty false in - let acc = - mk (Apply(Prim_tuple_get_last, loc, [arg; mk_nat 1])) list_ty false in - let f_body = mk (Apply (Prim_Cons, loc, [e; acc])) list_ty false in - let f_desc = Lambda (arg_name, arg_ty, loc, f_body, list_ty) in - let f = mk f_desc (Tlambda (arg_ty, list_ty)) false in - let empty_acc = mk_nil list_ty in - let desc = Apply (Prim_list_reduce, loc, [f; l; empty_acc]) in - mk desc list_ty fail, fail, false - - (* List.reduce (closure) -> Loop.loop *) - | Apply (Prim_list_reduce, loc, [f; l; acc]) -> - let f, _, _ = typecheck env f in - let l, can_fail1, transfer1 = typecheck env l in - let acc, can_fail2, transfer2 = typecheck env acc in - if transfer1 || transfer2 then - error loc "transfer within List.reduce args"; - let args = [f; l; acc] in - let _, ty = typecheck_prim1 env Prim_list_reduce loc args in - let can_fail = can_fail1 || can_fail2 in - begin match f.ty with - | Tclosure ((arg_ty, env_ty), acc_ty) -> - let elt_ty = match l.ty with - | Tlist ty -> ty - | _ -> error loc "Argument of List.reduce must be a list" - in - let loop_arg_name = uniq_ident env "arg" in - let head_name = uniq_ident env "head" in - let tail_name = uniq_ident env "tail" in - (* let loop_arg_ty = arg_ty in *) - let loop_body_ty = Ttuple [Tbool; arg_ty] in - let list_ty = Tlist elt_ty in - let arg = mk (Var (loop_arg_name, loc, [])) arg_ty false in - let head = mk (Var (head_name, loc, [])) elt_ty false in - let tail = mk (Var (tail_name, loc, [])) list_ty false in - let l' = - mk (Apply(Prim_tuple_get, loc, [arg; mk_nat 0])) list_ty can_fail in - let acc' = - mk (Apply(Prim_tuple_get_last, loc, [arg; mk_nat 1])) - acc_ty can_fail in - let nil_case = mk_tuple loc [ - const_false; - mk_tuple loc [mk_nil list_ty; acc'] can_fail - ] can_fail in - let cons_case = - mk_tuple loc [ - const_true; - mk_tuple loc [ - tail; - mk (Apply (Prim_exec, loc, [ - mk_tuple loc [head; acc'] can_fail; - f - ])) acc_ty can_fail - ] can_fail - ] can_fail - in - let loop_body = mk - (MatchList (l', loc, head_name, tail_name, cons_case, nil_case)) - loop_body_ty can_fail +let rec typecheck env ( exp : LiquidTypes.syntax_exp ) = + match exp.desc with + + | Const (ty, cst ) -> + let desc = Const (ty, cst ) in + let fail = false in + mk desc ty fail, fail, false + + | Let (name, loc, exp, body) -> + let exp, fail1, transfer1 = typecheck env exp in + if exp.ty = Tfail then + error loc "cannot assign failure"; + let env = maybe_reset_vars env transfer1 in + let (new_name, env, count) = new_binding env name exp.ty in + let body, fail2, transfer2 = typecheck env body in + let desc = Let (new_name, loc, exp, body ) in + check_used env name loc count; + if (not transfer1) && (not fail1) then begin + match !count with + | 0 -> + env.to_inline := StringMap.add new_name const_unit + ! (env.to_inline) + | 1 -> + env.to_inline := StringMap.add new_name exp + ! (env.to_inline) + | _ -> () + end; + let fail = fail1 || fail2 in + mk desc body.ty fail, fail, transfer1 || transfer2 + + | Var (name, loc, labels) -> + let e = find_var env loc name in + let e = + List.fold_left + (fun e label -> + let ty_name, ty = match e.ty with + | Ttype (ty_name, ty) -> ty_name, ty + | _ -> + error loc "not a record" + in + let arg1 = mk e.desc ty false in + let n = + try + let (ty_name', n, _label_ty) = + StringMap.find label env.env.labels in + if ty_name' <> ty_name then + error loc "label for wrong record"; + n + with Not_found -> + error loc "bad label" + in + let arg2 = mk_nat n in + let args = [ arg1; arg2] in + let prim, ty = typecheck_prim1 env Prim_tuple_get loc args in + mk (Apply(prim, loc, args)) ty false + ) e labels in + e, false, false + + | SetVar (name, loc, [], e) -> typecheck env e + + | SetVar (name, loc, label :: labels, arg) -> + let arg1_t = find_var env loc name in + let ty = arg1_t.ty in + let ty_name, tuple_ty = match ty with + | Ttype (ty_name, ty) -> ty_name, ty + | _ -> + error loc "not a record" + in + let arg1 = { arg1_t with ty = tuple_ty } in + let n = + try + let (ty_name', n, _label_ty) = + StringMap.find label env.env.labels in + if ty_name' <> ty_name then + error loc "label for wrong record"; + n + with Not_found -> + error loc "bad label" + in + let arg2 = mk_nat n in + let arg, can_fail = + match labels with + | [] -> + let (arg, can_fail, transfer) = typecheck env arg in + if transfer then + error loc "transfer within set-field"; + (arg, can_fail) + | _::_ -> + let args = [ arg1; arg2] in + let prim, ty = typecheck_prim1 env Prim_tuple_get loc args in + let get_exp = mk (Apply(prim, loc, args)) ty false in + let tmp_name = uniq_ident env "tmp#" in + let (new_name, env, count) = new_binding env tmp_name ty in + let body, can_fail, _transfer = + typecheck env + { exp with desc = SetVar (tmp_name, loc, + labels, arg) } in - let loop = mk - (Loop (loop_arg_name, loc, loop_body, - mk_tuple loc [l; acc] can_fail1)) - (Ttuple [list_ty; acc_ty]) can_fail + let desc = Let (new_name, loc, get_exp, body ) in + mk desc body.ty can_fail, can_fail + + in + let args = [ arg1; arg2; arg] in + let prim, tuple_ty' = typecheck_prim1 env Prim_tuple_set loc args in + mk (Apply(prim, loc, args)) ty can_fail, can_fail, false + + | Seq (exp1, exp2) -> + let exp1, fail1, transfer1 = + typecheck_expected "sequence" env Tunit exp1 in + let exp2, fail2, transfer2 = typecheck env exp2 in + let desc = Seq (exp1, exp2) in + (* TODO: if not fail1 then remove exp1 *) + let can_fail = fail1 || fail2 in + mk desc exp2.ty can_fail, can_fail, transfer1 || transfer2 + + | If (cond, ifthen, ifelse) -> + let cond, fail1, transfer1 = + typecheck_expected "if-cond" env Tbool cond in + if transfer1 then + error (noloc env) "transfer within if condition"; + let ifthen, fail2, transfer2 = typecheck env ifthen in + let ifelse, fail3, transfer3, ty = + if ifthen.ty = Tfail then + let ifelse, fail3, transfer3 = typecheck env ifelse in + ifelse, fail3, transfer3, ifelse.ty + else + let ifelse, fail3, transfer3 = + typecheck_expected "if-result" env ifthen.ty ifelse in + ifelse, fail3, transfer3, ifthen.ty + in + let desc = If(cond, ifthen, ifelse) in + let can_fail = fail1 || fail2 || fail3 in + mk desc ty can_fail, + can_fail, + transfer2 || transfer3 + + | LetTransfer (storage_name, result_name, + loc, + contract_exp, tez_exp, + storage_exp, arg_exp, body) -> + let tez_exp, fail1, transfer1 = + typecheck_expected "call-amount" env Ttez tez_exp in + let contract_exp, fail2, transfer2 = typecheck env contract_exp in + begin + match contract_exp.ty with + | Tcontract (arg_ty, return_ty) -> + let arg_exp, fail3, transfer3 = + typecheck_expected "call-arg" env arg_ty arg_exp in + let storage_exp, fail4, transfer4 = + typecheck_expected "call-storage" + env env.contract.storage storage_exp in + if transfer1 || transfer2 || transfer3 || transfer4 then + error loc "transfer within transfer arguments"; + let (new_storage, env, storage_count) = + new_binding env storage_name env.contract.storage in + let (new_result, env, result_count) = + new_binding env result_name return_ty in + let body, fail5, transfer5 = typecheck env body in + check_used env storage_name loc storage_count; + check_used env result_name loc result_count; + let desc = LetTransfer(new_storage, new_result, + loc, + contract_exp, tez_exp, + storage_exp, arg_exp, body) in - mk (Apply (Prim_tuple_get_last, loc, [loop; mk_nat 1])) - acc_ty can_fail, can_fail, false - | _ -> - mk (Apply (Prim_list_reduce, loc, args)) ty can_fail, can_fail, false - end - - (* List.map (closure) -> {List.rev(List.reduce (closure)} *) - | Apply (Prim_list_map, loc, [f; l]) -> - begin match is_closure env f with - | None -> typecheck_apply env Prim_list_map loc [f; l] - | Some ((arg_ty, _), ty_ret) -> - let arg_name = uniq_ident env "arg" in - let arg = mk_untyped (Var (arg_name, loc, [])) in - let x = - mk_untyped (Apply(Prim_tuple_get, loc, [arg; untyped_int 0])) in - let acc = - mk_untyped (Apply(Prim_tuple_get, loc, [arg; untyped_int 1])) in - let f_body = mk_untyped (Apply(Prim_Cons, loc, [ - mk_untyped (Apply(Prim_exec, loc, [x; f])); - acc - ])) in - let f_red = - mk_untyped (Lambda (arg_name, Ttuple [arg_ty; Tlist arg_ty], - loc, f_body, Tunit)) in - let red = - mk_untyped (Apply (Prim_list_reduce, loc, - [f_red; l; untyped_nil (Tlist arg_ty)])) in - let rev_red = mk_untyped (Apply (Prim_list_rev, loc, [red])) in - typecheck env rev_red - end - - (* Map.reduce (closure) -> {Map.reduce (::) |> List.rev |> List.reduce} *) - | Apply (Prim_map_reduce, loc, [f; m; acc]) -> - begin match is_closure env f with - | None -> typecheck_apply env Prim_map_reduce loc [f; m; acc] - | Some ((Ttuple [kv_ty; acc_ty], _), ty_ret) -> - let arg_name = uniq_ident env "arg" in - let arg = mk_untyped (Var (arg_name, loc, [])) in - let kv = - mk_untyped (Apply(Prim_tuple_get, loc, [arg; untyped_int 0])) in - let acc_elts = - mk_untyped (Apply(Prim_tuple_get, loc, [arg; untyped_int 1])) in - let gather_body = - mk_untyped (Apply(Prim_Cons, loc, [kv; acc_elts])) in - let gather_fun = - mk_untyped (Lambda (arg_name, Ttuple [kv_ty; Tlist kv_ty], - loc, gather_body, Tunit)) in - let rev_elts = - mk_untyped (Apply(Prim_map_reduce, loc, - [gather_fun; m; untyped_nil (Tlist kv_ty)])) in - let elts = mk_untyped (Apply(Prim_list_rev, loc, [rev_elts])) in - let red = mk_untyped (Apply(Prim_list_reduce, loc, [f; elts; acc])) in - typecheck env red - | Some _ -> error loc "bad closure type in Map.reduce" - end - - (* Map.map (closure) -> {Map.reduce (Map.update)} *) - | Apply (Prim_map_map, loc, [f; m]) -> - begin match is_closure env f with - | None -> typecheck_apply env Prim_map_map loc [f; m] - | Some ((Ttuple [k_ty; v_ty], _), ty_ret) -> - let arg_name = uniq_ident env "arg" in - let arg = mk_untyped (Var (arg_name, loc, [])) in - let kv = - mk_untyped (Apply(Prim_tuple_get, loc, [arg; untyped_int 0])) in - let acc = - mk_untyped (Apply(Prim_tuple_get, loc, [arg; untyped_int 1])) in - let k = - mk_untyped (Apply(Prim_tuple_get, loc, [kv; untyped_int 0])) in - let acc_ty = Tmap (k_ty, ty_ret) in - let update_body = - mk_untyped (Apply(Prim_map_update, loc, [ - k; - mk_untyped (Apply(Prim_Some, loc, [ - mk_untyped (Apply(Prim_exec, loc, [kv; f])) - ])); - acc - ])) in - let update_fun = - mk_untyped (Lambda (arg_name, Ttuple [Ttuple [k_ty; v_ty]; acc_ty], - loc, update_body, Tunit)) in - let red = - mk_untyped (Apply (Prim_map_reduce, loc, [ - update_fun; m; - mk_untyped (Const (acc_ty, CMap [])) - ])) in - typecheck env red - | Some _ -> error loc "bad closure type in Map.map" - end - - (* Set.reduce (closure) -> {Set.reduce (::) |> List.rev |> List.reduce} *) - | Apply (Prim_set_reduce, loc, [f; s; acc]) -> - begin match is_closure env f with - | None -> typecheck_apply env Prim_set_reduce loc [f; s; acc] - | Some ((Ttuple [elt_ty; acc_ty], _), ty_ret) -> - let arg_name = uniq_ident env "arg" in - let arg = mk_untyped (Var (arg_name, loc, [])) in - let elt = - mk_untyped (Apply(Prim_tuple_get, loc, [arg; untyped_int 0])) in - let acc_elts = - mk_untyped (Apply(Prim_tuple_get, loc, [arg; untyped_int 1])) in - let gather_body = - mk_untyped (Apply(Prim_Cons, loc, [elt; acc_elts])) in - let gather_fun = - mk_untyped (Lambda (arg_name, Ttuple [elt_ty; Tlist elt_ty], - loc, gather_body, Tunit)) in - let rev_elts = - mk_untyped (Apply(Prim_set_reduce, loc, - [gather_fun; s; untyped_nil (Tlist elt_ty)])) in - let elts = mk_untyped (Apply(Prim_list_rev, loc, [rev_elts])) in - let red = mk_untyped (Apply(Prim_list_reduce, loc, [f; elts; acc])) in - typecheck env red - | Some _ -> error loc "bad closure type in Set.reduce" - end - - | Apply (prim, loc, args) -> typecheck_apply env prim loc args - - | MatchOption (arg, loc, ifnone, name, ifsome) -> - let arg, fail1, transfer1 = typecheck env arg in - let arg_ty = match arg.ty with - | Tfail -> - error loc "cannot match failure" - | Toption ty -> ty - | _ -> - error loc "not an option type" - in - let env = maybe_reset_vars env transfer1 in - let ifnone, fail2, transfer2 = typecheck env ifnone in - let (new_name, env, count) = new_binding env name arg_ty in - let ifsome, fail3, transfer3 = typecheck env ifsome in - check_used env name loc count; - let desc = MatchOption (arg, loc, ifnone, new_name, ifsome ) in - let ty = - match ifnone.ty, ifsome.ty with - | ty, Tfail - | Tfail, ty -> ty - | ty1, ty2 -> - if ty1 <> ty2 then type_error loc "Bad option type in match" ty2 ty1; - ty1 - in - let can_fail = fail1 || fail2 || fail3 in - mk desc ty can_fail, - can_fail, - transfer1 || transfer2 || transfer3 - - | Loop (name, loc, body, arg) -> - let arg, fail1, transfer1 = typecheck env arg in - if arg.ty = Tfail then - error loc "loop arg is a failure"; - let env = maybe_reset_vars env transfer1 in - let (new_name, env, count) = new_binding env name arg.ty in - let body, fail2, transfer2 = - typecheck_expected "loop-body" env - (Ttuple [Tbool; arg.ty]) - body in - check_used env name loc count; - let can_fail = fail1 || fail2 in - mk (Loop (new_name, loc, body, arg)) arg.ty can_fail, - can_fail, - transfer1 || transfer2 - - | MatchList (arg, loc, head_name, tail_name, ifcons, ifnil) -> - let arg, fail1, transfer1 = typecheck env arg in - let arg_ty = match arg.ty with - | Tfail -> - error loc "cannot match failure" - | Tlist ty -> ty - | _ -> - error loc "not a list type" - in - let env = maybe_reset_vars env transfer1 in - let ifnil, fail2, transfer2 = typecheck env ifnil in - let (new_head_name, env, count) = new_binding env head_name arg_ty in - let (new_tail_name, env, count) = - new_binding env tail_name (Tlist arg_ty) in - let ifcons, fail3, transfer3 = typecheck env ifcons in - check_used env head_name loc count; - check_used env tail_name loc count; - let desc = MatchList (arg, loc, new_head_name, new_tail_name, ifcons, - ifnil ) in - let ty = - match ifnil.ty, ifcons.ty with - | ty, Tfail - | Tfail, ty -> ty - | ty1, ty2 -> - if ty1 <> ty2 then - error loc "not the same type"; - ty1 - in - let can_fail = fail1 || fail2 || fail3 in - mk desc ty can_fail, - can_fail, - transfer1 || transfer2 || transfer3 - - | Lambda (arg_name, arg_type, loc, body, res_type) -> - let env_at_lambda = env in - let lambda_arg_type = arg_type in - let lambda_arg_name = arg_name in - let lambda_body = body in - assert (res_type = Tunit); - (* let env = { env with vars = StringMap.empty } in *) - (* let (arg_name, env, arg_count) = new_binding env arg_name arg_type in *) - let bvs = LiquidBoundVariables.bv exp in - if StringSet.is_empty bvs then - (* not a closure, create a real lambda *) - let env = { env_at_lambda with vars = StringMap.empty } in - let (new_arg_name, env, arg_count) = - new_binding env lambda_arg_name lambda_arg_type in - let body, _fail, transfer = typecheck env lambda_body in - if transfer then - error loc "no transfer in lambda"; - check_used env lambda_arg_name loc arg_count; - let desc = - Lambda (new_arg_name, lambda_arg_type, loc, body, body.ty) in - let ty = Tlambda (lambda_arg_type, body.ty) in - mk desc ty false, false, false + mk desc body.ty true, + true, true + | _ -> + LiquidLoc.raise_error "typecheck error: Contract expected%!" + end + + + | Apply (Prim_unknown, loc, + ({ desc = Var (name, varloc, [])} as f) :: ((_ :: _) as r)) + when StringMap.mem name env.vars -> + let exp = List.fold_left (fun f x -> + { exp with desc = Apply (Prim_exec, loc, [x; f]) } + ) f r + in + typecheck env exp + + | Apply (Prim_unknown, loc, + [ { desc = Var (name, _, _)} as f; x ]) + when StringMap.mem name env.vars -> + typecheck env { exp with + desc = Apply(Prim_exec, loc, [x;f]) } + + | Apply (Prim_unknown, loc, + ({ desc = Var (name, varloc, [])} ::args)) -> + let prim = + try + LiquidTypes.primitive_of_string name + with Not_found -> + error loc "Unknown identifier %S" name + in + typecheck env { exp with + desc = Apply(prim, loc, args) } + + | Apply (Prim_unknown, loc, [f ; x ]) -> + typecheck env { exp with + desc = Apply(Prim_exec, loc, [x; f]) } + + + (* List.rev -> List.reduce (::) *) + | Apply (Prim_list_rev, loc, [l]) -> + let l, fail, transfer = typecheck env l in + if transfer then error loc "transfer within List.rev args"; + let elt_ty = match l.ty with + | Tlist ty -> ty + | _ -> error loc "Argument of List.rev must be a list" + in + let arg_name = uniq_ident env "arg" in + let list_ty = Tlist elt_ty in + let arg_ty = Ttuple [elt_ty; list_ty] in + let arg = mk (Var (arg_name, loc, [])) arg_ty false in + let e = mk (Apply(Prim_tuple_get, loc, [arg; mk_nat 0])) elt_ty false in + let acc = + mk (Apply(Prim_tuple_get_last, loc, [arg; mk_nat 1])) list_ty false in + let f_body = mk (Apply (Prim_Cons, loc, [e; acc])) list_ty false in + let f_desc = Lambda (arg_name, arg_ty, loc, f_body, list_ty) in + let f = mk f_desc (Tlambda (arg_ty, list_ty)) false in + let empty_acc = mk_nil list_ty in + let desc = Apply (Prim_list_reduce, loc, [f; l; empty_acc]) in + mk desc list_ty fail, fail, false + + (* List.reduce (closure) -> Loop.loop *) + | Apply (Prim_list_reduce, loc, [f; l; acc]) -> + let f, _, _ = typecheck env f in + let l, can_fail1, transfer1 = typecheck env l in + let acc, can_fail2, transfer2 = typecheck env acc in + if transfer1 || transfer2 then + error loc "transfer within List.reduce args"; + let args = [f; l; acc] in + let _, ty = typecheck_prim1 env Prim_list_reduce loc args in + let can_fail = can_fail1 || can_fail2 in + begin match f.ty with + | Tclosure ((arg_ty, env_ty), acc_ty) -> + let elt_ty = match l.ty with + | Tlist ty -> ty + | _ -> error loc "Argument of List.reduce must be a list" + in + let loop_arg_name = uniq_ident env "arg" in + let head_name = uniq_ident env "head" in + let tail_name = uniq_ident env "tail" in + (* let loop_arg_ty = arg_ty in *) + let loop_body_ty = Ttuple [Tbool; arg_ty] in + let list_ty = Tlist elt_ty in + let arg = mk (Var (loop_arg_name, loc, [])) arg_ty false in + let head = mk (Var (head_name, loc, [])) elt_ty false in + let tail = mk (Var (tail_name, loc, [])) list_ty false in + let l' = + mk (Apply(Prim_tuple_get, loc, [arg; mk_nat 0])) list_ty can_fail in + let acc' = + mk (Apply(Prim_tuple_get_last, loc, [arg; mk_nat 1])) + acc_ty can_fail in + let nil_case = mk_tuple loc [ + const_false; + mk_tuple loc [mk_nil list_ty; acc'] can_fail + ] can_fail in + let cons_case = + mk_tuple loc [ + const_true; + mk_tuple loc [ + tail; + mk (Apply (Prim_exec, loc, [ + mk_tuple loc [head; acc'] can_fail; + f + ])) acc_ty can_fail + ] can_fail + ] can_fail + in + let loop_body = mk + (MatchList (l', loc, head_name, tail_name, cons_case, nil_case)) + loop_body_ty can_fail + in + let loop = mk + (Loop (loop_arg_name, loc, loop_body, + mk_tuple loc [l; acc] can_fail1)) + (Ttuple [list_ty; acc_ty]) can_fail + in + mk (Apply (Prim_tuple_get_last, loc, [loop; mk_nat 1])) + acc_ty can_fail, can_fail, false + | _ -> + mk (Apply (Prim_list_reduce, loc, args)) ty can_fail, can_fail, false + end + + (* List.map (closure) -> {List.rev(List.reduce (closure)} *) + | Apply (Prim_list_map, loc, [f; l]) -> + begin match is_closure env f with + | None -> typecheck_apply env Prim_list_map loc [f; l] + | Some ((arg_ty, _), ty_ret) -> + let arg_name = uniq_ident env "arg" in + let arg = mk_untyped (Var (arg_name, loc, [])) in + let x = + mk_untyped (Apply(Prim_tuple_get, loc, [arg; untyped_int 0])) in + let acc = + mk_untyped (Apply(Prim_tuple_get, loc, [arg; untyped_int 1])) in + let f_body = mk_untyped (Apply(Prim_Cons, loc, [ + mk_untyped (Apply(Prim_exec, loc, [x; f])); + acc + ])) in + let f_red = + mk_untyped (Lambda (arg_name, Ttuple [arg_ty; Tlist arg_ty], + loc, f_body, Tunit)) in + let red = + mk_untyped (Apply (Prim_list_reduce, loc, + [f_red; l; untyped_nil (Tlist arg_ty)])) in + let rev_red = mk_untyped (Apply (Prim_list_rev, loc, [red])) in + typecheck env rev_red + end + + (* Map.reduce (closure) -> {Map.reduce (::) |> List.rev |> List.reduce} *) + | Apply (Prim_map_reduce, loc, [f; m; acc]) -> + begin match is_closure env f with + | None -> typecheck_apply env Prim_map_reduce loc [f; m; acc] + | Some ((Ttuple [kv_ty; acc_ty], _), ty_ret) -> + let arg_name = uniq_ident env "arg" in + let arg = mk_untyped (Var (arg_name, loc, [])) in + let kv = + mk_untyped (Apply(Prim_tuple_get, loc, [arg; untyped_int 0])) in + let acc_elts = + mk_untyped (Apply(Prim_tuple_get, loc, [arg; untyped_int 1])) in + let gather_body = + mk_untyped (Apply(Prim_Cons, loc, [kv; acc_elts])) in + let gather_fun = + mk_untyped (Lambda (arg_name, Ttuple [kv_ty; Tlist kv_ty], + loc, gather_body, Tunit)) in + let rev_elts = + mk_untyped (Apply(Prim_map_reduce, loc, + [gather_fun; m; untyped_nil (Tlist kv_ty)])) in + let elts = mk_untyped (Apply(Prim_list_rev, loc, [rev_elts])) in + let red = mk_untyped (Apply(Prim_list_reduce, loc, [f; elts; acc])) in + typecheck env red + | Some _ -> error loc "bad closure type in Map.reduce" + end + + (* Map.map (closure) -> {Map.reduce (Map.update)} *) + | Apply (Prim_map_map, loc, [f; m]) -> + begin match is_closure env f with + | None -> typecheck_apply env Prim_map_map loc [f; m] + | Some ((Ttuple [k_ty; v_ty], _), ty_ret) -> + let arg_name = uniq_ident env "arg" in + let arg = mk_untyped (Var (arg_name, loc, [])) in + let kv = + mk_untyped (Apply(Prim_tuple_get, loc, [arg; untyped_int 0])) in + let acc = + mk_untyped (Apply(Prim_tuple_get, loc, [arg; untyped_int 1])) in + let k = + mk_untyped (Apply(Prim_tuple_get, loc, [kv; untyped_int 0])) in + let acc_ty = Tmap (k_ty, ty_ret) in + let update_body = + mk_untyped (Apply(Prim_map_update, loc, [ + k; + mk_untyped (Apply(Prim_Some, loc, [ + mk_untyped (Apply(Prim_exec, loc, [kv; f])) + ])); + acc + ])) in + let update_fun = + mk_untyped (Lambda (arg_name, Ttuple [Ttuple [k_ty; v_ty]; acc_ty], + loc, update_body, Tunit)) in + let red = + mk_untyped (Apply (Prim_map_reduce, loc, [ + update_fun; m; + mk_untyped (Const (acc_ty, CMap [])) + ])) in + typecheck env red + | Some _ -> error loc "bad closure type in Map.map" + end + + (* Set.reduce (closure) -> {Set.reduce (::) |> List.rev |> List.reduce} *) + | Apply (Prim_set_reduce, loc, [f; s; acc]) -> + begin match is_closure env f with + | None -> typecheck_apply env Prim_set_reduce loc [f; s; acc] + | Some ((Ttuple [elt_ty; acc_ty], _), ty_ret) -> + let arg_name = uniq_ident env "arg" in + let arg = mk_untyped (Var (arg_name, loc, [])) in + let elt = + mk_untyped (Apply(Prim_tuple_get, loc, [arg; untyped_int 0])) in + let acc_elts = + mk_untyped (Apply(Prim_tuple_get, loc, [arg; untyped_int 1])) in + let gather_body = + mk_untyped (Apply(Prim_Cons, loc, [elt; acc_elts])) in + let gather_fun = + mk_untyped (Lambda (arg_name, Ttuple [elt_ty; Tlist elt_ty], + loc, gather_body, Tunit)) in + let rev_elts = + mk_untyped (Apply(Prim_set_reduce, loc, + [gather_fun; s; untyped_nil (Tlist elt_ty)])) in + let elts = mk_untyped (Apply(Prim_list_rev, loc, [rev_elts])) in + let red = mk_untyped (Apply(Prim_list_reduce, loc, [f; elts; acc])) in + typecheck env red + | Some _ -> error loc "bad closure type in Set.reduce" + end + + | Apply (prim, loc, args) -> typecheck_apply env prim loc args + + | MatchOption (arg, loc, ifnone, name, ifsome) -> + let arg, fail1, transfer1 = typecheck env arg in + let arg_ty = match arg.ty with + | Tfail -> + error loc "cannot match failure" + | Toption ty -> ty + | _ -> + error loc "not an option type" + in + let env = maybe_reset_vars env transfer1 in + let ifnone, fail2, transfer2 = typecheck env ifnone in + let (new_name, env, count) = new_binding env name arg_ty in + let ifsome, fail3, transfer3 = typecheck env ifsome in + check_used env name loc count; + let desc = MatchOption (arg, loc, ifnone, new_name, ifsome ) in + let ty = + match ifnone.ty, ifsome.ty with + | ty, Tfail + | Tfail, ty -> ty + | ty1, ty2 -> + if ty1 <> ty2 then type_error loc "Bad option type in match" ty2 ty1; + ty1 + in + let can_fail = fail1 || fail2 || fail3 in + mk desc ty can_fail, + can_fail, + transfer1 || transfer2 || transfer3 + + | Loop (name, loc, body, arg) -> + let arg, fail1, transfer1 = typecheck env arg in + if arg.ty = Tfail then + error loc "loop arg is a failure"; + let env = maybe_reset_vars env transfer1 in + let (new_name, env, count) = new_binding env name arg.ty in + let body, fail2, transfer2 = + typecheck_expected "loop-body" env + (Ttuple [Tbool; arg.ty]) + body in + check_used env name loc count; + let can_fail = fail1 || fail2 in + mk (Loop (new_name, loc, body, arg)) arg.ty can_fail, + can_fail, + transfer1 || transfer2 + + | MatchList (arg, loc, head_name, tail_name, ifcons, ifnil) -> + let arg, fail1, transfer1 = typecheck env arg in + let arg_ty = match arg.ty with + | Tfail -> + error loc "cannot match failure" + | Tlist ty -> ty + | _ -> + error loc "not a list type" + in + let env = maybe_reset_vars env transfer1 in + let ifnil, fail2, transfer2 = typecheck env ifnil in + let (new_head_name, env, count) = new_binding env head_name arg_ty in + let (new_tail_name, env, count) = + new_binding env tail_name (Tlist arg_ty) in + let ifcons, fail3, transfer3 = typecheck env ifcons in + check_used env head_name loc count; + check_used env tail_name loc count; + let desc = MatchList (arg, loc, new_head_name, new_tail_name, ifcons, + ifnil ) in + let ty = + match ifnil.ty, ifcons.ty with + | ty, Tfail + | Tfail, ty -> ty + | ty1, ty2 -> + if ty1 <> ty2 then + error loc "not the same type"; + ty1 + in + let can_fail = fail1 || fail2 || fail3 in + mk desc ty can_fail, + can_fail, + transfer1 || transfer2 || transfer3 + + | Lambda (arg_name, arg_type, loc, body, res_type) -> + let env_at_lambda = env in + let lambda_arg_type = arg_type in + let lambda_arg_name = arg_name in + let lambda_body = body in + assert (res_type = Tunit); + (* let env = { env with vars = StringMap.empty } in *) + (* let (arg_name, env, arg_count) = new_binding env arg_name arg_type in *) + let bvs = LiquidBoundVariables.bv exp in + if StringSet.is_empty bvs then + (* not a closure, create a real lambda *) + let env = { env_at_lambda with vars = StringMap.empty } in + let (new_arg_name, env, arg_count) = + new_binding env lambda_arg_name lambda_arg_type in + let body, _fail, transfer = typecheck env lambda_body in + if transfer then + error loc "no transfer in lambda"; + check_used env lambda_arg_name loc arg_count; + let desc = + Lambda (new_arg_name, lambda_arg_type, loc, body, body.ty) in + let ty = Tlambda (lambda_arg_type, body.ty) in + mk desc ty false, false, false else (* create closure with environment *) let env, arg_name, arg_type, call_env = @@ -778,539 +804,570 @@ let rec loc_exp env e = match e.desc with let ty = Tclosure ((lambda_arg_type, call_env_type), body.ty) in mk desc ty false, false, false - | Closure _ -> assert false - - | Record (_loc, []) -> assert false - | Record (loc, (( (label, _) :: _ ) as lab_x_exp_list)) -> - let ty_name, _, _ = - try - StringMap.find label env.env.labels - with Not_found -> - error loc "unbound label %S" label - in - let record_ty, ty_kind = StringMap.find ty_name env.env.types in - let len = List.length (match ty_kind with - | Type_record (tys,_labels) -> tys - | Type_variant _ -> assert false) in - let t = Array.make len None in - let record_can_fail = ref false in - List.iteri (fun i (label, exp) -> - let ty_name', label_pos, ty = try - StringMap.find label env.env.labels - with Not_found -> - error loc "unbound label %S" label - in - if ty_name <> ty_name' then - error loc "inconsistent list of labels"; - let exp, can_fail, transfer = - typecheck_expected ("label "^ label) env ty exp in - if transfer then - error loc "transfer not allowed in record"; - t.(label_pos) <- Some exp; - if can_fail then record_can_fail := true - ) lab_x_exp_list; - let args = Array.to_list t in - let args = List.map (function - | None -> - error loc "some labels are not defined" - | Some exp -> exp) args in - let ty = Ttype (ty_name, record_ty) in - let desc = Apply(Prim_tuple, loc, args) in - mk desc ty !record_can_fail, !record_can_fail, false - - | Constructor(loc, Constr constr, arg) -> - let ty_name, arg_ty = StringMap.find constr env.env.constrs in - let arg, can_fail, transfer = - typecheck_expected "constr-arg" env arg_ty arg in - if transfer then - error loc "transfer not allowed in constructor argument"; - let constr_ty, ty_kind = StringMap.find ty_name env.env.types in - let exp = - match ty_kind with - | Type_record _ -> assert false - | Type_variant constrs -> - let rec iter constrs = - match constrs with - | [] -> assert false - | [c,_, _left_ty, _right_ty] -> - assert (c = constr); - arg - | (c, ty, left_ty, right_ty) :: constrs -> - let desc = - if c = constr then - (* We use an unused argument to carry the type to + | Closure _ -> assert false + + | Record (_loc, []) -> assert false + | Record (loc, (( (label, _) :: _ ) as lab_x_exp_list)) -> + let ty_name, _, _ = + try + StringMap.find label env.env.labels + with Not_found -> + error loc "unbound label %S" label + in + let record_ty, ty_kind = StringMap.find ty_name env.env.types in + let len = List.length (match ty_kind with + | Type_record (tys,_labels) -> tys + | Type_variant _ | Type_alias -> assert false) in + let t = Array.make len None in + let record_can_fail = ref false in + List.iteri (fun i (label, exp) -> + let ty_name', label_pos, ty = try + StringMap.find label env.env.labels + with Not_found -> + error loc "unbound label %S" label + in + if ty_name <> ty_name' then + error loc "inconsistent list of labels"; + let exp, can_fail, transfer = + typecheck_expected ("label "^ label) env ty exp in + if transfer then + error loc "transfer not allowed in record"; + t.(label_pos) <- Some exp; + if can_fail then record_can_fail := true + ) lab_x_exp_list; + let args = Array.to_list t in + let args = List.map (function + | None -> + error loc "some labels are not defined" + | Some exp -> exp) args in + let ty = Ttype (ty_name, record_ty) in + let desc = Apply(Prim_tuple, loc, args) in + mk desc ty !record_can_fail, !record_can_fail, false + + | Constructor(loc, Constr constr, arg) -> + let ty_name, arg_ty = StringMap.find constr env.env.constrs in + let arg, can_fail, transfer = + typecheck_expected "constr-arg" env arg_ty arg in + if transfer then + error loc "transfer not allowed in constructor argument"; + let constr_ty, ty_kind = StringMap.find ty_name env.env.types in + let exp = + match ty_kind with + | Type_record _ | Type_alias -> assert false + | Type_variant constrs -> + let rec iter constrs = + match constrs with + | [] -> assert false + | [c,_, _left_ty, _right_ty] -> + assert (c = constr); + arg + | (c, ty, left_ty, right_ty) :: constrs -> + let desc = + if c = constr then + (* We use an unused argument to carry the type to the code generator *) - Apply(Prim_Left, loc, [arg; unused env right_ty]) - else - let arg = iter constrs in - Apply(Prim_Right, loc, [arg; unused env left_ty]) - in - mk desc ty can_fail + Apply(Prim_Left, loc, [arg; unused env right_ty]) + else + let arg = iter constrs in + Apply(Prim_Right, loc, [arg; unused env left_ty]) + in + mk desc ty can_fail + in + iter constrs + in + mk exp.desc (Ttype (ty_name, constr_ty)) can_fail, can_fail, false + + | Constructor(loc, Left right_ty, arg) -> + let arg, can_fail, transfer = typecheck env arg in + if transfer then + error loc "transfer not allowed in constructor argument"; + let ty = Tor(arg.ty, right_ty) in + let desc = Apply(Prim_Left,loc,[arg; unused env right_ty]) in + mk desc ty can_fail, can_fail, false + + | Constructor(loc, Source (from_ty, to_ty), _arg) -> + let ty = Tcontract(from_ty, to_ty) in + let desc = Apply(Prim_Source,loc,[unused env from_ty; unused env to_ty]) in + mk desc ty false, false, false + + | Constructor(loc, Right left_ty, arg) -> + let arg, can_fail, transfer = typecheck env arg in + if transfer then + error loc "transfer not allowed in constructor argument"; + let ty = Tor(left_ty, arg.ty) in + let desc = Apply(Prim_Right,loc,[arg; unused env left_ty]) in + mk desc ty can_fail, can_fail, false + + | MatchVariant (arg, loc, cases) -> + let arg, can_fail, transfer1 = typecheck env arg in + let ty_name, constrs, is_left_right = + try + match arg.ty with + | Tfail -> + error loc "cannot match failure" + | Ttype (ty_name, _) -> + begin + let constr_ty, ty_kind = StringMap.find ty_name env.env.types in + match ty_kind with + | Type_variant constrs -> + (ty_name, List.map (fun (c, _, _, _) -> c) constrs, None) + | Type_record _ | Type_alias -> raise Not_found + end + | Tor (left_ty, right_ty) -> + (* Left, Right pattern matching *) + let ty_name = LiquidPrinter.Liquid.string_of_type arg.ty in + (ty_name, ["Left"; "Right"], Some (left_ty, right_ty)) + | _ -> raise Not_found + with Not_found -> + error loc "not a variant type: %s" + (LiquidPrinter.Liquid.string_of_type arg.ty) + in + let env = maybe_reset_vars env transfer1 in + let match_can_fail = ref can_fail in + let expected_type = ref None in + let has_transfer = ref transfer1 in + let cases_extra_constrs = + List.fold_left (fun acc -> function + | CAny, _ -> acc + | CConstr (c, _), _ -> StringSet.add c acc + ) StringSet.empty cases + |> ref + in + let cases = List.map (fun constr -> + let cve = find_case loc env constr cases in + cases_extra_constrs := StringSet.remove constr !cases_extra_constrs; + cve + ) constrs in + + if not (StringSet.is_empty !cases_extra_constrs) then + error loc "constructors %s do not belong to type %s" + (String.concat ", " (StringSet.elements !cases_extra_constrs)) + ty_name; + + let cases = List.map (fun (constr, vars, e) -> + let var_ty = match is_left_right, constr with + | Some (left_ty, _), "Left" -> left_ty + | Some (_, right_ty), "Right" -> right_ty + | Some _, _ -> error loc "unknown constructor %S" constr + | None, _ -> + let ty_name', var_ty = + try StringMap.find constr env.env.constrs + with Not_found -> error loc "unknown constructor %S" constr in - iter constrs - in - mk exp.desc (Ttype (ty_name, constr_ty)) can_fail, can_fail, false - - | Constructor(loc, Left right_ty, arg) -> - let arg, can_fail, transfer = typecheck env arg in - if transfer then - error loc "transfer not allowed in constructor argument"; - let ty = Tor(arg.ty, right_ty) in - let desc = Apply(Prim_Left,loc,[arg; unused env right_ty]) in - mk desc ty can_fail, can_fail, false - - | Constructor(loc, Source (from_ty, to_ty), _arg) -> - let ty = Tcontract(from_ty, to_ty) in - let desc = Apply(Prim_Source,loc,[unused env from_ty; unused env to_ty]) in - mk desc ty false, false, false + if ty_name <> ty_name' then error loc "inconsistent constructors"; + var_ty + in + let name = + match vars with + | [] -> "_" + | [ var ] -> var + | _ -> + error loc "cannot deconstruct constructor args" + in + let (new_name, env, count) = + new_binding env name var_ty in + let (e, can_fail, transfer) = + match !expected_type with + | Some expected_type -> + typecheck_expected "pattern matching branch" env expected_type e + | None -> + let (e, can_fail, transfer) = + typecheck env e in + begin + match e.ty with + | Tfail -> () + | _ -> expected_type := Some e.ty + end; + (e, can_fail, transfer) + in + if can_fail then match_can_fail := true; + if transfer then has_transfer := true; + check_used env name loc count; + (CConstr (constr, [new_name]), e) + ) cases + in - | Constructor(loc, Right left_ty, arg) -> - let arg, can_fail, transfer = typecheck env arg in - if transfer then - error loc "transfer not allowed in constructor argument"; - let ty = Tor(left_ty, arg.ty) in - let desc = Apply(Prim_Right,loc,[arg; unused env left_ty]) in - mk desc ty can_fail, can_fail, false - - | MatchVariant (arg, loc, - [ "Left", [left_arg], left_exp; - "Right", [right_arg], right_exp; - ]) -> - let arg, can_fail, transfer1 = typecheck env arg in - let (left_ty, right_ty) = match arg.ty with - | Tor(left_ty, right_ty) -> (left_ty, right_ty) - | _ -> - error loc "not a Left-Right variant type: %s" - (LiquidPrinter.Michelson.string_of_type arg.ty) - in - let env = maybe_reset_vars env transfer1 in - let left_arg, left_exp, can_fail1, transfer1 = - typecheck_case env left_arg left_exp left_ty in - let right_arg, right_exp, can_fail2, transfer2 = - typecheck_case env right_arg right_exp right_ty in - let desc = MatchVariant(arg, loc, - [ "Left", [left_arg], left_exp; - "Right", [right_arg], right_exp; - ]) - in - if left_exp.ty <> right_exp.ty then begin - error loc "inconsistent return type" - end; - let can_fail = can_fail || can_fail1 || can_fail2 in - mk desc left_exp.ty can_fail, - can_fail, - transfer1 || transfer2 - - | MatchVariant (arg, loc, - [ ("Left" | "Right"), _, _; ] - ) -> - error loc "non-exhaustive pattern-matching" - - | MatchVariant (arg, loc, cases) -> - let arg, can_fail, transfer1 = typecheck env arg in - let ty_name, constrs = - try - match arg.ty with - | Tfail -> - error loc "cannot match failure" - | Ttype (ty_name, _) -> - begin - let constr_ty, ty_kind = StringMap.find ty_name env.env.types in - match ty_kind with - | Type_variant constrs -> (ty_name, constrs) - | Type_record _ -> raise Not_found - end - | _ -> raise Not_found - with Not_found -> - error loc "not a variant type: %s" - (LiquidPrinter.Michelson.string_of_type arg.ty) - in - let env = maybe_reset_vars env transfer1 in - let match_can_fail = ref can_fail in - let expected_type = ref None in - let has_transfer = ref transfer1 in - let present_constrs = ref StringMap.empty in - List.iter (fun (constr, vars, e) -> - let ty_name', var_ty = - try - StringMap.find constr env.env.constrs - with Not_found -> - error loc "unknown constructor" - in - if ty_name <> ty_name' then - error loc "inconsistent constructors"; - if StringMap.mem constr !present_constrs then - error loc "constructor matched twice"; - let name = - match vars with - | [] -> "_" - | [ var ] -> var - | _ -> - error loc "cannot deconstruct constructor args" - in - let (new_name, env, count) = - new_binding env name var_ty in - let (e, can_fail, transfer) = - match !expected_type with - | Some expected_type -> - typecheck_expected "constr-match" env expected_type e - | None -> - let (e, can_fail, transfer) = - typecheck env e in - begin - match e.ty with - | Tfail -> () - | _ -> expected_type := Some e.ty - end; - (e, can_fail, transfer) - in - if can_fail then match_can_fail := true; - if transfer then has_transfer := true; - check_used env name loc count; - present_constrs := StringMap.add constr - (new_name, e) - !present_constrs - ) cases; - - let cases = List.map (fun (constr, _ty, _left_ty, _right_ty) -> - let (new_name, e) = - try - StringMap.find constr !present_constrs - with Not_found -> - error loc "non-exhaustive pattern" - in - (constr, [new_name], e) - ) constrs in - - let desc = MatchVariant (arg, loc, cases ) in - let ty = match !expected_type with - | None -> Tfail - | Some ty -> ty - in - mk desc ty !match_can_fail, !match_can_fail, !has_transfer - - and typecheck_case env name exp var_ty = - let (new_name, env, count) = - new_binding env name var_ty in - let (exp, can_fail, transfer) = typecheck env exp in - (new_name, exp, can_fail, transfer) - - and typecheck_prim1 env prim loc args = - match prim, args with - | Prim_tuple_get, [ { ty = Ttuple tuple }; - { desc = Const (_, (CInt n | CNat n)) }] -> - let n = LiquidPrinter.int_of_integer n in - let size = List.length tuple in - let prim = - if size <= n then - error loc "get outside tuple" + let desc = MatchVariant (arg, loc, cases ) in + let ty = match !expected_type with + | None -> Tfail + | Some ty -> ty + in + mk desc ty !match_can_fail, !match_can_fail, !has_transfer + +and find_case loc env constr cases = + match List.find_all (function + | CAny, _ -> true + | CConstr (cname, _), _ -> cname = constr + ) cases + with + | [] -> + error loc "non-exhaustive pattern. Constructor %s is not matched." constr + | m :: unused -> + List.iter (fun (_, e) -> + LiquidLoc.warn (loc_exp env e) (UnusedMatched constr) + ) unused; + match m with + | CAny, e -> constr, [], e + | CConstr (_, vars), e -> constr, vars, e + +and typecheck_case env name exp var_ty = + let (new_name, env, count) = + new_binding env name var_ty in + let (exp, can_fail, transfer) = typecheck env exp in + (new_name, exp, can_fail, transfer) + +and typecheck_prim1 env prim loc args = + match prim, args with + | Prim_tuple_get, [ { ty = Ttuple tuple }; + { desc = Const (_, (CInt n | CNat n)) }] -> + let n = LiquidPrinter.int_of_integer n in + let size = List.length tuple in + let prim = + if size <= n then + error loc "get outside tuple" + else + if size = n + 1 then + Prim_tuple_get_last else - if size = n + 1 then - Prim_tuple_get_last - else - Prim_tuple_get - in - let ty = List.nth tuple n in - prim, ty - - | Prim_tuple_set, [ { ty = Ttuple tuple }; - { desc = Const (_, (CInt n | CNat n)) }; - { ty } ] -> - let n = LiquidPrinter.int_of_integer n in - let expected_ty = List.nth tuple n in - let size = List.length tuple in - let prim = - if size <= n then - error loc "set outside tuple" + Prim_tuple_get + in + let ty = List.nth tuple n in + prim, ty + + | Prim_tuple_set, [ { ty = Ttuple tuple }; + { desc = Const (_, (CInt n | CNat n)) }; + { ty } ] -> + let n = LiquidPrinter.int_of_integer n in + let expected_ty = List.nth tuple n in + let size = List.length tuple in + let prim = + if size <= n then + error loc "set outside tuple" + else + if size = n + 1 then + Prim_tuple_set_last else - if size = n + 1 then - Prim_tuple_set_last - else - Prim_tuple_set - in - let ty = if ty <> expected_ty && ty <> Tfail then - error loc "prim set bad type" - else Ttuple tuple - in - prim, ty + Prim_tuple_set + in + let ty = if ty <> expected_ty && ty <> Tfail then + error loc "prim set bad type" + else Ttuple tuple + in + prim, ty - | _ -> - let prim = - (* Unqualified versions of primitives. They should not be used, + | _ -> + let prim = + (* Unqualified versions of primitives. They should not be used, but they can be generated by decompiling Michelson. *) - match prim, args with - | Prim_coll_update, [ _; _; { ty = Tset _ }] -> Prim_set_update - | Prim_coll_update, [ _; _; { ty = Tmap _ }] -> Prim_map_update - | Prim_coll_mem, [ _; { ty = Tset _ } ] -> Prim_set_mem - | Prim_coll_mem, [ _; { ty = Tmap _ } ] -> Prim_map_mem - | Prim_coll_find, [ _; { ty = Tmap _ } ] -> Prim_map_find - | Prim_coll_map, [ _; { ty = Tlist _ } ] -> Prim_list_map - | Prim_coll_map, [_; { ty = Tmap _ } ] -> Prim_map_map - | Prim_coll_map, [_; { ty = Tset _ } ] -> Prim_set_map - | Prim_coll_reduce, [_; { ty = Tlist _ }; _ ] -> Prim_list_reduce - | Prim_coll_reduce, [_; { ty = Tset _ }; _ ] -> Prim_set_reduce - | Prim_coll_reduce, [_; { ty = Tmap _ }; _ ] -> Prim_map_reduce - | Prim_coll_size, [{ ty = Tlist _ } ] -> Prim_list_size - | Prim_coll_size, [{ ty = Tset _ } ] -> Prim_set_size - | Prim_coll_size, [{ ty = Tmap _ } ] -> Prim_map_size - | _ -> prim - in - prim, typecheck_prim2 env prim loc args - - and typecheck_prim2 env prim loc args = - match prim, args with - | ( Prim_neq | Prim_lt | Prim_gt | Prim_eq | Prim_le | Prim_ge ), - [ { ty = ty1 }; { ty = ty2 } ] -> - if comparable_ty ty1 ty2 then Tbool - else error_not_comparable loc prim ty1 ty2 - | Prim_compare, - [ { ty = ty1 }; { ty = ty2 } ] -> - if comparable_ty ty1 ty2 then Tint - else error_not_comparable loc prim ty1 ty2 - - | (Prim_add|Prim_sub|Prim_mul), - ( [ { ty = Ttez }; { ty = (Ttez | Tint | Tnat) } ] - | [ { ty = (Tint | Tnat) }; { ty = Ttez } ]) - -> Ttez - | (Prim_add|Prim_mul), [ { ty = Tnat }; { ty = Tnat } ] -> Tnat - | (Prim_add|Prim_sub|Prim_mul), [ { ty = (Tint|Tnat) }; - { ty = (Tint|Tnat) } ] -> Tint - | Prim_add, [ { ty = Ttimestamp }; { ty = Tint|Tnat } ] -> Ttimestamp - | Prim_add, [ { ty = Tint|Tnat }; { ty = Ttimestamp } ] -> Ttimestamp - - (* TODO: improve types of ediv in Michelson ! *) - | Prim_ediv, [ { ty = Tnat }; { ty = Tnat } ] -> - Toption (Ttuple [Tnat; Tnat]) - | Prim_ediv, [ { ty = Tint|Tnat }; { ty = Tint|Tnat } ] -> - Toption (Ttuple [Tint; Tnat]) - | Prim_ediv, [ { ty = Ttez }; { ty = Tint } ] -> - Toption (Ttuple [Ttez; Ttez]) - - | Prim_xor, [ { ty = Tbool }; { ty = Tbool } ] -> Tbool - | Prim_or, [ { ty = Tbool }; { ty = Tbool } ] -> Tbool - | Prim_and, [ { ty = Tbool }; { ty = Tbool } ] -> Tbool - | Prim_not, [ { ty = Tbool } ] -> Tbool - - | Prim_xor, [ { ty = Tnat }; { ty = Tnat } ] -> Tnat - | Prim_xor, [ { ty = Tint|Tnat }; { ty = Tint|Tnat } ] -> Tint - | Prim_or, [ { ty = Tnat }; { ty = Tnat } ] -> Tnat - | Prim_or, [ { ty = Tint|Tnat }; { ty = Tint|Tnat } ] -> Tint - | Prim_and, [ { ty = Tnat }; { ty = Tnat } ] -> Tnat - | Prim_and, [ { ty = Tint|Tnat }; { ty = Tint|Tnat } ] -> Tint - | Prim_not, [ { ty = Tint|Tnat } ] -> Tint - - | Prim_abs, [ { ty = Tint } ] -> Tnat - | Prim_int, [ { ty = Tnat } ] -> Tint - | Prim_sub, [ { ty = Tint|Tnat } ] -> Tint - - | (Prim_lsl|Prim_lsr), [ { ty = Tnat} ; { ty = Tnat } ] -> Tnat - - - - | Prim_tuple, args -> Ttuple (List.map (fun e -> e.ty) args) - - | Prim_map_find, [ { ty = key_ty }; { ty = Tmap (expected_key_ty, value_ty) }] - -> - if expected_key_ty <> key_ty then - error loc "bad Map.find key type"; - Toption value_ty - | Prim_map_update, [ { ty = key_ty }; - { ty = Toption value_ty }; - { ty = Tmap (expected_key_ty, expected_value_ty) }] - -> - if expected_key_ty <> key_ty then - error loc "bad Map.update key type"; - if expected_value_ty <> value_ty then - error loc "bad Map.update value type"; - Tmap (key_ty, value_ty) - | Prim_map_mem, [ { ty = key_ty }; { ty = Tmap (expected_key_ty,_) }] - -> - if expected_key_ty <> key_ty then - error loc "bad Mem.mem key type"; - Tbool - - | Prim_set_mem,[ { ty = key_ty }; { ty = Tset expected_key_ty }] - -> - if expected_key_ty <> key_ty then - error loc "bad Set.mem key type"; - Tbool - - | Prim_list_size, [ { ty = Tlist _ }] -> Tnat - | Prim_set_size, [ { ty = Tset _ }] -> Tnat - | Prim_map_size, [ { ty = Tmap _ }] -> Tnat - - | Prim_set_update, [ { ty = key_ty }; { ty = Tbool }; - { ty = Tset expected_key_ty }] - -> - if expected_key_ty <> key_ty then - error loc "bad Set.update key type"; - Tset key_ty - - - | Prim_Some, [ { ty } ] -> Toption ty - | Prim_fail, [ { ty = Tunit } ] -> Tfail - | Prim_self, [ { ty = Tunit } ] -> - Tcontract (env.contract.parameter, env.contract.return) - | Prim_now, [ { ty = Tunit } ] -> Ttimestamp - | Prim_balance, [ { ty = Tunit } ] -> Ttez - (* | "Current.source", [ { ty = Tunit } ] -> ... *) - | Prim_amount, [ { ty = Tunit } ] -> Ttez - | Prim_gas, [ { ty = Tunit } ] -> Tnat - | Prim_hash, [ _ ] -> Tstring - | Prim_check, [ { ty = Tkey }; - { ty = Ttuple [Tsignature; Tstring] } ] -> - Tbool - | Prim_manager, [ { ty = Tcontract(_,_) } ] -> - Tkey - | Prim_create_account, [ { ty = Tkey }; { ty = Toption Tkey }; - { ty = Tbool }; { ty = Ttez } ] -> - Tcontract (Tunit, Tunit) - | Prim_default_account, [ { ty = Tkey } ] -> - Tcontract (Tunit, Tunit) - | Prim_create_contract, [ { ty = Tkey }; (* manager *) - { ty = Toption Tkey }; (* delegate *) - { ty = Tbool }; (* spendable *) - { ty = Tbool }; (* delegatable *) - { ty = Ttez }; (* initial amount *) - { ty = Tlambda ( - Ttuple [ arg_type; - storage_arg], - Ttuple [ result_type; storage_res]); }; - { ty = storage_init } - ] -> - if storage_arg <> storage_res then - error loc "Contract.create: inconsistent storage in contract"; - if storage_res <> storage_init then - error loc "Contract.create: wrong type for storage init"; - - Tcontract (arg_type, result_type) - - | Prim_exec, [ { ty }; - { ty = ( Tlambda(from_ty, to_ty) + match prim, args with + | Prim_coll_update, [ _; _; { ty = Tset _ }] -> Prim_set_update + | Prim_coll_update, [ _; _; { ty = Tmap _ }] -> Prim_map_update + | Prim_coll_mem, [ _; { ty = Tset _ } ] -> Prim_set_mem + | Prim_coll_mem, [ _; { ty = Tmap _ } ] -> Prim_map_mem + | Prim_coll_find, [ _; { ty = Tmap _ } ] -> Prim_map_find + | Prim_coll_map, [ _; { ty = Tlist _ } ] -> Prim_list_map + | Prim_coll_map, [_; { ty = Tmap _ } ] -> Prim_map_map + | Prim_coll_map, [_; { ty = Tset _ } ] -> Prim_set_map + | Prim_coll_reduce, [_; { ty = Tlist _ }; _ ] -> Prim_list_reduce + | Prim_coll_reduce, [_; { ty = Tset _ }; _ ] -> Prim_set_reduce + | Prim_coll_reduce, [_; { ty = Tmap _ }; _ ] -> Prim_map_reduce + | Prim_coll_size, [{ ty = Tlist _ } ] -> Prim_list_size + | Prim_coll_size, [{ ty = Tset _ } ] -> Prim_set_size + | Prim_coll_size, [{ ty = Tmap _ } ] -> Prim_map_size + | _ -> prim + in + prim, typecheck_prim2 env prim loc args + +and typecheck_prim2 env prim loc args = + match prim, args with + | ( Prim_neq | Prim_lt | Prim_gt | Prim_eq | Prim_le | Prim_ge ), + [ { ty = ty1 }; { ty = ty2 } ] -> + if comparable_ty ty1 ty2 then Tbool + else error_not_comparable loc prim ty1 ty2 + | Prim_compare, + [ { ty = ty1 }; { ty = ty2 } ] -> + if comparable_ty ty1 ty2 then Tint + else error_not_comparable loc prim ty1 ty2 + + | (Prim_add|Prim_sub|Prim_mul), + ( [ { ty = Ttez }; { ty = (Ttez | Tint | Tnat) } ] + | [ { ty = (Tint | Tnat) }; { ty = Ttez } ]) + -> Ttez + | (Prim_add|Prim_mul), [ { ty = Tnat }; { ty = Tnat } ] -> Tnat + | (Prim_add|Prim_sub|Prim_mul), [ { ty = (Tint|Tnat) }; + { ty = (Tint|Tnat) } ] -> Tint + | Prim_add, [ { ty = Ttimestamp }; { ty = Tint|Tnat } ] -> Ttimestamp + | Prim_add, [ { ty = Tint|Tnat }; { ty = Ttimestamp } ] -> Ttimestamp + + (* TODO: improve types of ediv in Michelson ! *) + | Prim_ediv, [ { ty = Tnat }; { ty = Tnat } ] -> + Toption (Ttuple [Tnat; Tnat]) + | Prim_ediv, [ { ty = Tint|Tnat }; { ty = Tint|Tnat } ] -> + Toption (Ttuple [Tint; Tnat]) + | Prim_ediv, [ { ty = Ttez }; { ty = Tnat } ] -> + Toption (Ttuple [Ttez; Ttez]) + + | Prim_xor, [ { ty = Tbool }; { ty = Tbool } ] -> Tbool + | Prim_or, [ { ty = Tbool }; { ty = Tbool } ] -> Tbool + | Prim_and, [ { ty = Tbool }; { ty = Tbool } ] -> Tbool + | Prim_not, [ { ty = Tbool } ] -> Tbool + + | Prim_xor, [ { ty = Tnat }; { ty = Tnat } ] -> Tnat + | Prim_xor, [ { ty = Tint|Tnat }; { ty = Tint|Tnat } ] -> Tint + | Prim_or, [ { ty = Tnat }; { ty = Tnat } ] -> Tnat + | Prim_or, [ { ty = Tint|Tnat }; { ty = Tint|Tnat } ] -> Tint + | Prim_and, [ { ty = Tnat }; { ty = Tnat } ] -> Tnat + | Prim_and, [ { ty = Tint|Tnat }; { ty = Tint|Tnat } ] -> Tint + | Prim_not, [ { ty = Tint|Tnat } ] -> Tint + + | Prim_abs, [ { ty = Tint } ] -> Tnat + | Prim_int, [ { ty = Tnat } ] -> Tint + | Prim_sub, [ { ty = Tint|Tnat } ] -> Tint + + | (Prim_lsl|Prim_lsr), [ { ty = Tnat} ; { ty = Tnat } ] -> Tnat + + + + | Prim_tuple, args -> Ttuple (List.map (fun e -> e.ty) args) + + | Prim_map_find, [ { ty = key_ty }; { ty = Tmap (expected_key_ty, value_ty) }] + -> + if expected_key_ty <> key_ty then + error loc "bad Map.find key type"; + Toption value_ty + | Prim_map_update, [ { ty = key_ty }; + { ty = Toption value_ty }; + { ty = Tmap (expected_key_ty, expected_value_ty) }] + -> + if expected_key_ty <> key_ty then + error loc "bad Map.update key type"; + if expected_value_ty <> value_ty then + error loc "bad Map.update value type"; + Tmap (key_ty, value_ty) + | Prim_map_mem, [ { ty = key_ty }; { ty = Tmap (expected_key_ty,_) }] + -> + if expected_key_ty <> key_ty then + error loc "bad Mem.mem key type"; + Tbool + + | Prim_set_mem,[ { ty = key_ty }; { ty = Tset expected_key_ty }] + -> + if expected_key_ty <> key_ty then + error loc "bad Set.mem key type"; + Tbool + + | Prim_list_size, [ { ty = Tlist _ }] -> Tnat + | Prim_set_size, [ { ty = Tset _ }] -> Tnat + | Prim_map_size, [ { ty = Tmap _ }] -> Tnat + + | Prim_set_update, [ { ty = key_ty }; { ty = Tbool }; + { ty = Tset expected_key_ty }] + -> + if expected_key_ty <> key_ty then + error loc "bad Set.update key type"; + Tset key_ty + + + | Prim_Some, [ { ty } ] -> Toption ty + | Prim_fail, [ { ty = Tunit } ] -> Tfail + | Prim_self, [ { ty = Tunit } ] -> + Tcontract (env.contract.parameter, env.contract.return) + | Prim_now, [ { ty = Tunit } ] -> Ttimestamp + | Prim_balance, [ { ty = Tunit } ] -> Ttez + (* | "Current.source", [ { ty = Tunit } ] -> ... *) + | Prim_amount, [ { ty = Tunit } ] -> Ttez + | Prim_gas, [ { ty = Tunit } ] -> Tnat + | Prim_hash, [ _ ] -> Tstring + | Prim_hash_key, [ { ty = Tkey } ] -> Tkey_hash + | Prim_check, [ { ty = Tkey }; + { ty = Ttuple [Tsignature; Tstring] } ] -> + Tbool + | Prim_check, args -> + error_prim loc Prim_check args [Tkey; Ttuple [Tsignature; Tstring]] + + | Prim_manager, [ { ty = Tcontract(_,_) } ] -> + Tkey_hash + + | Prim_create_account, [ { ty = Tkey_hash }; { ty = Toption Tkey_hash }; + { ty = Tbool }; { ty = Ttez } ] -> + Tcontract (Tunit, Tunit) + | Prim_create_account, args -> + error_prim loc Prim_create_account args + [ Tkey_hash; Toption Tkey_hash; Tbool; Ttez ] + + | Prim_default_account, [ { ty = Tkey_hash } ] -> + Tcontract (Tunit, Tunit) + + | Prim_create_contract, [ { ty = Tkey_hash }; (* manager *) + { ty = Toption Tkey_hash }; (* delegate *) + { ty = Tbool }; (* spendable *) + { ty = Tbool }; (* delegatable *) + { ty = Ttez }; (* initial amount *) + { ty = Tlambda ( + Ttuple [ arg_type; + storage_arg], + Ttuple [ result_type; storage_res]); }; + { ty = storage_init } + ] -> + if storage_arg <> storage_res then + error loc "Contract.create: inconsistent storage in contract"; + if storage_res <> storage_init then + error loc "Contract.create: wrong type for storage init"; + + Tcontract (arg_type, result_type) + + | Prim_create_contract, args -> + + let expected_args = [ Tkey_hash; Toption Tkey_hash; + Tbool; Tbool; Ttez ] in + let nexpected = 7 in + let prim = LiquidTypes.string_of_primitive Prim_create_contract in + let nargs = List.length args in + if nargs <> nexpected then + error loc "Prim %S: %d args provided, %d args expected" + prim nargs nexpected + else + let args = List.map (fun { ty } -> ty) args in + List.iteri (fun i (arg, expected) -> + if arg <> expected then + error loc + "Primitive %s, argument %d:\nExpected type:%sProvided type:%s" + prim (i+1) + (LiquidPrinter.Liquid.string_of_type expected) + (LiquidPrinter.Liquid.string_of_type arg) + + ) (List.combine args expected_args); + error loc + "Primitive %s, argument %d:\nExpected type: (arg * storage) -> (res * storage)\nProvided type:%s" + prim 6 + (LiquidPrinter.Liquid.string_of_type (List.nth args 5)) + + | Prim_exec, [ { ty }; + { ty = ( Tlambda(from_ty, to_ty) | Tclosure((from_ty, _), to_ty)) }] -> - if ty <> from_ty then - type_error loc "Bad argument type in function application" ty from_ty; - to_ty + if ty <> from_ty then + type_error loc "Bad argument type in function application" ty from_ty; + to_ty - | ( Prim_list_map + | ( Prim_list_map (* | Prim_list_reduce *) | Prim_set_reduce - | Prim_map_reduce - | Prim_map_map - | Prim_coll_map - | Prim_coll_reduce - ), { ty = Tclosure _ } :: _ -> - error loc "Cannot use closures in %s" (LiquidTypes.string_of_primitive prim) - - | Prim_list_map, [ - { ty = Tlambda (from_ty, to_ty) }; - { ty = Tlist ty } ] -> - if ty <> from_ty then - type_error loc "Bad argument type in List.map" ty from_ty; - Tlist to_ty - - | Prim_list_reduce, [ - { ty = ( Tlambda (Ttuple [src_ty; dst_ty], dst_ty') + | Prim_map_reduce + | Prim_map_map + | Prim_coll_map + | Prim_coll_reduce + ), { ty = Tclosure _ } :: _ -> + error loc "Cannot use closures in %s" (LiquidTypes.string_of_primitive prim) + + | Prim_list_map, [ + { ty = Tlambda (from_ty, to_ty) }; + { ty = Tlist ty } ] -> + if ty <> from_ty then + type_error loc "Bad argument type in List.map" ty from_ty; + Tlist to_ty + + | Prim_list_reduce, [ + { ty = ( Tlambda (Ttuple [src_ty; dst_ty], dst_ty') | Tclosure ((Ttuple [src_ty; dst_ty], _), dst_ty')) }; - { ty = Tlist src_ty' }; - { ty = acc_ty }; - ] -> - if src_ty <> src_ty' then - type_error loc "Bad argument source type in List.reduce" src_ty' src_ty; - if dst_ty <> dst_ty' then - type_error loc "Bad function type in List.reduce" dst_ty' dst_ty; - if acc_ty <> dst_ty' then - type_error loc "Bad accumulator type in List.reduce" acc_ty dst_ty'; - acc_ty - - | Prim_set_reduce, [ - { ty = Tlambda (Ttuple [src_ty; dst_ty], dst_ty') }; - { ty = Tset src_ty' }; - { ty = acc_ty }; - ] -> - if src_ty <> src_ty' then - type_error loc "Bad argument source type in Set.reduce" src_ty' src_ty; - if dst_ty <> dst_ty' then - type_error loc "Bad function type in Set.reduce" dst_ty' dst_ty; - if acc_ty <> dst_ty' then - type_error loc "Bad accumulator type in Set.reduce" acc_ty dst_ty'; - acc_ty - - | Prim_map_reduce, [ - { ty = Tlambda (Ttuple [Ttuple [key_ty; src_ty]; dst_ty], dst_ty') }; - { ty = Tmap (key_ty', src_ty') }; - { ty = acc_ty }; - ] -> - if src_ty <> src_ty' then - type_error loc "Bad argument source type in Map.reduce" src_ty' src_ty; - if dst_ty <> dst_ty' then - type_error loc "Bad function type in Map.reduce" dst_ty' dst_ty; - if acc_ty <> dst_ty' then - type_error loc "Bad accumulator type in Map.reduce" acc_ty dst_ty'; - if key_ty <> key_ty' then - type_error loc "Bad function key type in Map.reduce" key_ty' key_ty; - acc_ty - - | Prim_map_map, [ - { ty = Tlambda (Ttuple [from_key_ty; from_value_ty], to_value_ty) }; - { ty = Tmap (key_ty, value_ty) } ] -> - if from_key_ty <> key_ty then - type_error loc "Bad function key type in Map.map" key_ty from_key_ty; - if from_value_ty <> value_ty then - type_error loc "Bad function value type in Map.map" - value_ty from_value_ty; - Tmap (key_ty, to_value_ty) - - - | Prim_concat, [ { ty = Tstring }; { ty = Tstring }] -> Tstring - | Prim_Cons, [ { ty = head_ty }; { ty = Tunit } ] -> - Tlist head_ty - | Prim_Cons, [ { ty = head_ty }; { ty = Tlist tail_ty } ] -> - if head_ty <> tail_ty then - type_error loc "Bad types for list" head_ty tail_ty; - Tlist tail_ty - | prim, args -> - error loc "Bad %d args for primitive %S:\n %s\n" (List.length args) - (LiquidTypes.string_of_primitive prim) - (String.concat "\n " - (List.map - (fun arg -> - LiquidPrinter.Liquid.string_of_type arg.ty) - args)) - ; - - and typecheck_expected info env expected_ty exp = - let exp, fail, transfer = typecheck env exp in - if exp.ty <> expected_ty && exp.ty <> Tfail then - type_error (loc_exp env exp) - ("Unexpected type for "^info) exp.ty expected_ty; - exp, fail, transfer - - and typecheck_apply env prim loc args = - let can_fail = ref false in - let args = List.map (fun arg -> - let arg, fail, transfer = typecheck env arg in - if transfer then - error loc "transfer within prim args"; - if fail then can_fail := true; - arg - ) args in - let prim, ty = typecheck_prim1 env prim loc args in - let can_fail = - match prim with - | Prim_fail -> true - | _ -> !can_fail - in - mk (Apply (prim, loc, args)) ty can_fail, can_fail, false + { ty = Tlist src_ty' }; + { ty = acc_ty }; + ] -> + if src_ty <> src_ty' then + type_error loc "Bad argument source type in List.reduce" src_ty' src_ty; + if dst_ty <> dst_ty' then + type_error loc "Bad function type in List.reduce" dst_ty' dst_ty; + if acc_ty <> dst_ty' then + type_error loc "Bad accumulator type in List.reduce" acc_ty dst_ty'; + acc_ty + + | Prim_set_reduce, [ + { ty = Tlambda (Ttuple [src_ty; dst_ty], dst_ty') }; + { ty = Tset src_ty' }; + { ty = acc_ty }; + ] -> + if src_ty <> src_ty' then + type_error loc "Bad argument source type in Set.reduce" src_ty' src_ty; + if dst_ty <> dst_ty' then + type_error loc "Bad function type in Set.reduce" dst_ty' dst_ty; + if acc_ty <> dst_ty' then + type_error loc "Bad accumulator type in Set.reduce" acc_ty dst_ty'; + acc_ty + + | Prim_map_reduce, [ + { ty = Tlambda (Ttuple [Ttuple [key_ty; src_ty]; dst_ty], dst_ty') }; + { ty = Tmap (key_ty', src_ty') }; + { ty = acc_ty }; + ] -> + if src_ty <> src_ty' then + type_error loc "Bad argument source type in Map.reduce" src_ty' src_ty; + if dst_ty <> dst_ty' then + type_error loc "Bad function type in Map.reduce" dst_ty' dst_ty; + if acc_ty <> dst_ty' then + type_error loc "Bad accumulator type in Map.reduce" acc_ty dst_ty'; + if key_ty <> key_ty' then + type_error loc "Bad function key type in Map.reduce" key_ty' key_ty; + acc_ty + + | Prim_map_map, [ + { ty = Tlambda (Ttuple [from_key_ty; from_value_ty], to_value_ty) }; + { ty = Tmap (key_ty, value_ty) } ] -> + if from_key_ty <> key_ty then + type_error loc "Bad function key type in Map.map" key_ty from_key_ty; + if from_value_ty <> value_ty then + type_error loc "Bad function value type in Map.map" + value_ty from_value_ty; + Tmap (key_ty, to_value_ty) + + + | Prim_concat, [ { ty = Tstring }; { ty = Tstring }] -> Tstring + | Prim_Cons, [ { ty = head_ty }; { ty = Tunit } ] -> + Tlist head_ty + | Prim_Cons, [ { ty = head_ty }; { ty = Tlist tail_ty } ] -> + if head_ty <> tail_ty then + type_error loc "Bad types for list" head_ty tail_ty; + Tlist tail_ty + | prim, args -> + error loc "Bad %d args for primitive %S:\n %s\n" (List.length args) + (LiquidTypes.string_of_primitive prim) + (String.concat "\n " + (List.map + (fun arg -> + LiquidPrinter.Liquid.string_of_type arg.ty) + args)) + ; + +and typecheck_expected info env expected_ty exp = + let exp, fail, transfer = typecheck env exp in + if exp.ty <> expected_ty && exp.ty <> Tfail then + type_error (loc_exp env exp) + ("Unexpected type for "^info) exp.ty expected_ty; + exp, fail, transfer + +and typecheck_apply env prim loc args = + let can_fail = ref false in + let args = List.map (fun arg -> + let arg, fail, transfer = typecheck env arg in + if transfer then + error loc "transfer within prim args"; + if fail then can_fail := true; + arg + ) args in + let prim, ty = typecheck_prim1 env prim loc args in + let can_fail = + match prim with + | Prim_fail -> true + | _ -> !can_fail + in + mk (Apply (prim, loc, args)) ty can_fail, can_fail, false - (* FIXME ugly hack *) - and is_closure env exp = - match typecheck env exp with - | { ty = Tclosure ((ty_arg, ty_env), ty_ret) }, _, _ -> - Some ((ty_arg, ty_env), ty_ret) - | _ -> - None +(* FIXME ugly hack *) +and is_closure env exp = + match typecheck env exp with + | { ty = Tclosure ((ty_arg, ty_env), ty_ret) }, _, _ -> + Some ((ty_arg, ty_env), ty_ret) + | _ -> + None let typecheck_contract ~warnings env contract = @@ -1330,10 +1387,10 @@ let typecheck_contract ~warnings env contract = (* "parameter/2" *) let (_, env, _) = new_binding env "parameter" contract.parameter in - let expected_ty = Ttuple [ contract.return; contract.storage ] in + let expected_ty = Ttuple [contract.return; contract.storage] in let code, _can_fail, _transfer = - typecheck_expected "final value" env expected_ty contract.code in + typecheck_expected "return value" env expected_ty contract.code in { contract with code }, ! (env.to_inline) let typecheck_code ~warnings env contract expected_ty code = @@ -1373,6 +1430,9 @@ let check_const_type ~to_tez loc ty cst = | Tkey, CKey s | Tkey, CString s -> CKey s + | Tkey_hash, CKey_hash s + | Tkey_hash, CString s -> CKey_hash s + | Ttimestamp, CString s | Ttimestamp, CTimestamp s -> begin (* approximation of correct tezos timestamp *) diff --git a/tools/liquidity/liquidClean.ml b/tools/liquidity/liquidClean.ml index c2f54133..b96f14db 100644 --- a/tools/liquidity/liquidClean.ml +++ b/tools/liquidity/liquidClean.ml @@ -10,12 +10,9 @@ open LiquidTypes -let string_of_pre pre = - LiquidPrinter.Michelson.string_of_code (LiquidEmit.emit_code (SEQ pre)) - let rec clean_code code = - let code = - match code with + let ins = + match code.ins with | SEQ expr -> SEQ (clean_seq expr) | IF (e1, e2) -> IF (clean_code e1, clean_code e2) | IF_NONE (e1, e2) -> IF_NONE (clean_code e1, clean_code e2) @@ -25,12 +22,12 @@ let rec clean_code code = | LOOP e -> LOOP (clean_code e) | LAMBDA (arg_type, res_type, e) -> LAMBDA (arg_type, res_type, clean_code e) - | _ -> code + | ins -> ins in - match code with - | DIP (_, SEQ [FAIL]) | DIP (_, FAIL) - | LOOP (SEQ [FAIL]) | LOOP FAIL - -> FAIL + match ins with + | DIP (_, {ins=SEQ [{ins=FAIL}]}) | DIP (_, {ins=FAIL}) + | LOOP ({ins=SEQ [{ins=FAIL}]}) | LOOP {ins=FAIL} + -> { code with ins = FAIL } | _ -> code and clean_seq exprs = @@ -38,11 +35,11 @@ and clean_seq exprs = | [] -> [] | e :: exprs -> let e = clean_code e in - if e = FAIL then [FAIL] + if e.ins = FAIL then [e] else let exprs = clean_seq exprs in match e, exprs with - | _, FAIL :: _ -> [FAIL] + | _, ({ins=FAIL} as fail) :: _ -> [fail] | _ -> e :: exprs let clean_contract contract = diff --git a/tools/liquidity/liquidClean.mli b/tools/liquidity/liquidClean.mli index 53bce808..30eb98a1 100644 --- a/tools/liquidity/liquidClean.mli +++ b/tools/liquidity/liquidClean.mli @@ -9,5 +9,5 @@ open LiquidTypes -val clean_code : pre_michelson -> pre_michelson -val clean_contract : pre_michelson contract -> pre_michelson contract +val clean_code : loc_michelson -> loc_michelson +val clean_contract : loc_michelson contract -> loc_michelson contract diff --git a/tools/liquidity/liquidDecomp.ml b/tools/liquidity/liquidDecomp.ml index bf1b5bf5..d3743a43 100644 --- a/tools/liquidity/liquidDecomp.ml +++ b/tools/liquidity/liquidDecomp.ml @@ -22,6 +22,7 @@ let const_name_of_datatype = function | Tstring -> "s" | Ttimestamp -> "time" | Tkey -> "key" + | Tkey_hash -> "key_hash" | Tsignature -> "sig" | Ttuple _ -> "tuple" | Toption _ -> "opt" @@ -176,6 +177,7 @@ let decompile contract = | "INT" -> Prim_int | "ABS" -> Prim_abs | "H" -> Prim_hash + | "HASH_KEY" -> Prim_hash_key | "CHECK_SIGNATURE" -> Prim_check | "CREATE_ACCOUNT" -> Prim_create_account | "CREATE_CONTRACT" -> Prim_create_contract @@ -236,9 +238,9 @@ let decompile contract = | N_IF_LEFT (_, var0), N_IF_RIGHT (_,var1) -> MatchVariant(arg_of arg, noloc, [ - "Left", [var_of var0], + CConstr ("Left", [var_of var0]), decompile_next then_node; - "Right", [var_of var1], + CConstr ("Right", [var_of var1]), decompile_next else_node ]) | _ -> diff --git a/tools/liquidity/liquidEmit.ml b/tools/liquidity/liquidEmit.ml index 3b312a76..83c21816 100644 --- a/tools/liquidity/liquidEmit.ml +++ b/tools/liquidity/liquidEmit.ml @@ -11,7 +11,7 @@ open LiquidTypes let rec emit_code code = - match code with + match code.i with | SEQ exprs -> M_INS_EXP ("SEQ", [], List.map emit_code exprs) | IF (ifthen, ifelse) -> M_INS_EXP ("IF", [], [emit_code ifthen; emit_code ifelse]) @@ -57,7 +57,9 @@ let rec emit_code code = | BALANCE -> M_INS "BALANCE" | SWAP -> M_INS "SWAP" | DIP_DROP (n,m) -> - emit_code (DIP (n, SEQ (LiquidMisc.list_init m (fun _ -> DROP)))) + emit_code {i= DIP (n, + { i = SEQ (LiquidMisc.list_init m + (fun _ -> {i=DROP}))})} | SOME -> M_INS "SOME" | GET -> M_INS "GET" | UPDATE -> M_INS "UPDATE" @@ -70,6 +72,7 @@ let rec emit_code code = | MANAGER -> M_INS "MANAGER" | CREATE_ACCOUNT -> M_INS "CREATE_ACCOUNT" | H -> M_INS "H" + | HASH_KEY -> M_INS "HASH_KEY" | CHECK_SIGNATURE -> M_INS "CHECK_SIGNATURE" | SIZE -> M_INS "SIZE" | DEFAULT_ACCOUNT -> M_INS "DEFAULT_ACCOUNT" diff --git a/tools/liquidity/liquidEmit.mli b/tools/liquidity/liquidEmit.mli index ce9c2e67..e25d7139 100644 --- a/tools/liquidity/liquidEmit.mli +++ b/tools/liquidity/liquidEmit.mli @@ -9,5 +9,5 @@ open LiquidTypes -val emit_code : pre_michelson -> michelson_exp -val emit_contract : pre_michelson contract -> michelson_exp contract +val emit_code : noloc_michelson -> michelson_exp +val emit_contract : noloc_michelson contract -> michelson_exp contract diff --git a/tools/liquidity/liquidFromOCaml.ml b/tools/liquidity/liquidFromOCaml.ml index 22682005..1a511b01 100644 --- a/tools/liquidity/liquidFromOCaml.ml +++ b/tools/liquidity/liquidFromOCaml.ml @@ -81,10 +81,6 @@ let () = (* The minimal version of liquidity files that are accepted by this compiler *) let minimal_version = 0.1 - -(* The maximal version of liquidity files that are accepted by this compiler *) -let maximal_version = 0.1 - (* let contract (parameter : timestamp) @@ -96,6 +92,18 @@ let contract ... *) +(* The maximal version of liquidity files that are accepted by this compiler *) +let maximal_version = 0.11 +(* +type storage = ... +let contract + (parameter : timestamp) + (storage: storage ) + : unit * storage = + ... + *) + + open Asttypes open Longident open Parsetree @@ -153,6 +161,7 @@ let rec translate_type env typ = | { ptyp_desc = Ptyp_constr ({ txt = Lident "string" }, []) } -> Tstring | { ptyp_desc = Ptyp_constr ({ txt = Lident "timestamp" }, []) } -> Ttimestamp | { ptyp_desc = Ptyp_constr ({ txt = Lident "key" }, []) } -> Tkey + | { ptyp_desc = Ptyp_constr ({ txt = Lident "key_hash" }, []) } -> Tkey_hash | { ptyp_desc = Ptyp_constr ({ txt = Lident "signature" }, []) } -> Tsignature @@ -184,8 +193,9 @@ let rec translate_type env typ = | { ptyp_desc = Ptyp_constr ({ txt = Lident ty_name }, []) } -> begin try - let ty,_ = StringMap.find ty_name env.types in - Ttype (ty_name, ty) + match StringMap.find ty_name env.types with + | ty, Type_alias -> ty + | ty, _ -> Ttype (ty_name, ty) with Not_found -> unbound_type typ.ptyp_loc ty_name end @@ -380,6 +390,41 @@ and translate_pair exp = let mk desc = { desc; ty = (); bv = StringSet.empty; fail = false } +let deconstruct_pat env pat = + let rec deconstruct_pat_aux acc indexes = function + | { ppat_desc = Ppat_constraint (pat, ty) } -> + let acc, _ = deconstruct_pat_aux acc indexes pat in + acc, translate_type env ty + + | { ppat_desc = Ppat_var { txt = var; loc } } -> + (var, loc_of_loc loc, indexes) :: acc, Tunit (* Dummy type value *) + + | { ppat_desc = Ppat_any; ppat_loc } -> + ("_", loc_of_loc ppat_loc, indexes) :: acc, Tunit (* Dummy type value *) + + | { ppat_desc = Ppat_tuple pats } -> + let _, acc, tys = + List.fold_left (fun (i, acc, tys) pat -> + let acc, ty = deconstruct_pat_aux acc (i :: indexes) pat in + i + 1, acc, ty :: tys + ) (0, acc, []) pats + in + acc, Ttuple (List.rev tys) + + | { ppat_loc } -> + error_loc ppat_loc "cannot deconstruct this pattern" + in + deconstruct_pat_aux [] [] pat + +let access_of_deconstruct var_name loc indexes = + let a = mk (Var (var_name, loc, [])) in + List.fold_right (fun i a -> + mk (Apply (Prim_tuple_get, loc, [ + a; + mk (Const (Tnat, CNat (LiquidPrinter.integer_of_int i))) + ])) + ) indexes a + let rec translate_code env exp = let desc = match exp with @@ -453,16 +498,27 @@ let rec translate_code env exp = translate_code env arg_exp, translate_code env body) - | { pexp_desc = Pexp_let (Nonrecursive, - [ - { - pvb_pat = { ppat_desc = - Ppat_var { txt = var; loc } }; - pvb_expr = var_exp; - } - ], body) } -> - Let (var, loc_of_loc loc, - translate_code env var_exp, translate_code env body) + | { pexp_desc = Pexp_let (Nonrecursive, [ { + pvb_pat = pat; + pvb_expr = var_exp; + } ], body); pexp_loc } -> + + let vars_infos, _ = deconstruct_pat env pat in + let exp, body = translate_code env var_exp, translate_code env body in + begin match vars_infos with + | [] -> assert false + | [v, loc, []] -> Let (v, loc, exp, body) + | _ -> + let var_name = + String.concat "_" (List.rev_map (fun (v,_,_) -> v) vars_infos) in + let lets_body = + List.fold_left (fun e (v, loc, indexes) -> + let access = access_of_deconstruct var_name loc indexes in + mk (Let (v, loc, access, e)) + ) body vars_infos + in + Let (var_name, loc_of_loc pexp_loc, exp, lets_body) + end | { pexp_desc = Pexp_sequence (exp1, exp2) } -> Seq (translate_code env exp1, translate_code env exp2) @@ -500,32 +556,47 @@ let rec translate_code env exp = let e = translate_code env e in let cases = List.map (translate_case env) cases in begin - match List.sort compare cases with - | [ "None", [], ifnone; - "Some", [arg], ifsome] -> - MatchOption(e, loc_of_loc pexp_loc, ifnone, arg, ifsome) - | [ "::", [head; tail], ifcons; - "[]", [], ifnil ] -> - MatchList(e, loc_of_loc pexp_loc, head, tail, ifcons, ifnil) + match cases with + | [ CConstr ("None", []), ifnone; CConstr ("Some", [arg]), ifsome ] + | [ CConstr ("Some", [arg]), ifsome; CConstr ("None", []), ifnone ] + | [ CConstr ("Some", [arg]), ifsome; CAny, ifnone ] -> + MatchOption(e, loc_of_loc pexp_loc, ifnone, arg, ifsome) + | [ CConstr ("None", []), ifnone; CAny, ifsome ] -> + MatchOption(e, loc_of_loc pexp_loc, ifnone, "_", ifsome) + + | [ CConstr ("[]", []), ifnil; CConstr ("::", [head; tail]), ifcons ] + | [ CConstr ("::", [head; tail]), ifcons; CConstr ("[]", []), ifnil ] + | [ CConstr ("::", [head; tail]), ifcons; CAny, ifnil ] -> + MatchList(e, loc_of_loc pexp_loc, head, tail, ifcons, ifnil) + | [ CConstr ("[]", []), ifnil; CAny, ifcons ] -> + MatchList(e, loc_of_loc pexp_loc, "_head", "_tail", ifcons, ifnil) + | args -> - MatchVariant(e, loc_of_loc pexp_loc, args) + MatchVariant(e, loc_of_loc pexp_loc, args) end - | { pexp_desc = - Pexp_fun ( - Nolabel, None, - { ppat_desc = - Ppat_constraint( - { ppat_desc = - Ppat_var { txt = arg_name } }, - arg_type) - }, - body_exp) } -> + | { pexp_desc = Pexp_fun (Nolabel, None, pat, body_exp) } -> let body_exp = translate_code env body_exp in - let arg_type = translate_type env arg_type in - Lambda (arg_name, arg_type, loc_of_loc exp.pexp_loc, - body_exp, - Tunit) (* not yet inferred *) + let vars_infos, arg_type = deconstruct_pat env pat in + begin match vars_infos with + | [] -> assert false + | [arg_name, loc, []] -> + Lambda (arg_name, arg_type, loc_of_loc exp.pexp_loc, + body_exp, + Tunit) (* not yet inferred *) + | _ -> + let arg_name = + String.concat "_" (List.rev_map (fun (v,_,_) -> v) vars_infos) in + let lets_body = + List.fold_left (fun e (v, loc, indexes) -> + let access = access_of_deconstruct arg_name loc indexes in + mk (Let (v, loc, access, e)) + ) body_exp vars_infos + in + Lambda (arg_name, arg_type, loc_of_loc exp.pexp_loc, + lets_body, + Tunit) (* not yet inferred *) + end | { pexp_desc = Pexp_record (lab_x_exp_list, None) } -> let lab_x_exp_list = @@ -674,26 +745,30 @@ and translate_case env case = let e = case.pc_rhs in let e = translate_code env e in match case.pc_lhs with + | { ppat_desc = Ppat_any } -> + (CAny, e) | { ppat_desc = Ppat_construct ( { txt = Lident name } , None) } -> - (name, [], e) - | { ppat_desc = Ppat_construct ( - { txt = Lident name } , - Some { ppat_desc = Ppat_var { txt } } ) } -> - (name, [txt], e) + (CConstr (name, []), e) | { ppat_desc = Ppat_construct ( { txt = Lident name } , - Some { ppat_desc = - Ppat_tuple [ - { ppat_desc = Ppat_var { txt = var1 } }; - { ppat_desc = Ppat_var { txt = var2 } }; - ] - } + Some { ppat_desc = Ppat_tuple [ p1; p2 ]} ) } -> - (name, [var1; var2], e) + (CConstr (name, [var_of_pat p1; var_of_pat p2]), e) + | { ppat_desc = Ppat_construct ( + { txt = Lident name } , Some p ) } -> + (CConstr (name, [var_of_pat p]), e) | { ppat_loc } -> error_loc ppat_loc "bad pattern" +and var_of_pat = function + | { ppat_desc = Ppat_var { txt = var } } -> var + | { ppat_desc = Ppat_any } -> "_" + | { ppat_desc = Ppat_construct _; ppat_loc } -> + error_loc ppat_loc "cannot match deep" + | { ppat_loc } -> + error_loc ppat_loc "bad pattern" + let rec inline_funs exp = function | [] -> exp | (f_pvb, f_loc) :: funs -> @@ -721,7 +796,21 @@ let rec translate_head env ext_funs head_exp args = }, head_exp) } -> translate_head env ext_funs head_exp - ((arg, translate_type env arg_type) :: args) + ((arg, translate_type env arg_type) :: args) + + | { pexp_desc = Pexp_constraint (head_exp, return_type); pexp_loc } -> + let return = match translate_type env return_type with + | Ttuple [ ret_ty; sto_ty ] -> + let storage = List.assoc "storage" args in + if sto_ty <> storage then + error_loc pexp_loc + "Second component of return type must be identical to storage type"; + ret_ty + | _ -> + error_loc pexp_loc + "return type must be a product of some type and the storage type" + in + translate_head env ext_funs head_exp (("return", return) :: args) | { pexp_desc = Pexp_fun ( @@ -731,7 +820,7 @@ let rec translate_head env ext_funs head_exp args = }, head_exp) } -> translate_head env ext_funs head_exp - (("return", translate_type env arg_type) :: args) + (("return", translate_type env arg_type) :: args) | { pexp_desc = Pexp_fun ( @@ -878,6 +967,23 @@ let rec translate_structure funs env ast = end; translate_structure funs env ast + (* type alias *) + | { pstr_desc = Pstr_type (Recursive, + [ + { ptype_name = { txt = ty_name }; + ptype_params = []; + ptype_cstrs = []; + ptype_private = Public; + ptype_manifest = Some ct; + ptype_attributes = []; + ptype_loc; + ptype_kind; + } + ]) } :: ast -> + let ty = translate_type env ct in + env.types <- StringMap.add ty_name (ty, Type_alias) env.types; + translate_structure funs env ast + | [] -> Location.raise_errorf "No entry point found in file %S%!" env.filename diff --git a/tools/liquidity/liquidInterp.ml b/tools/liquidity/liquidInterp.ml index 5d81cd94..de0267ab 100644 --- a/tools/liquidity/liquidInterp.ml +++ b/tools/liquidity/liquidInterp.ml @@ -11,10 +11,10 @@ open LiquidTypes let counter = ref 0 let nodes = Hashtbl.create 1000 -let node kind args prevs = +let node loc kind args prevs = incr counter; let num = !counter in - let node = { num; kind; args; next = None; prevs } in + let node = { num; loc; kind; args; next = None; prevs } in List.iter (fun prev -> match prev.next with | None -> prev.next <- Some node @@ -50,9 +50,10 @@ let rec uniformize_stack if_stack stack = LiquidMisc.list_remove (if_stack_length - stack_length) if_stack else LiquidMisc.list_make (stack_length - if_stack_length) - { num = -1; kind = N_UNKNOWN "STACK"; args = []; - next = None; prevs = [] } - @ if_stack + { num = -1; loc = LiquidLoc.noloc; + kind = N_UNKNOWN "STACK"; args = []; + next = None; prevs = [] } + @ if_stack let rec merge_stacks if_stack end_node1 end_node2 stack1 stack2 = match stack1, stack2 with @@ -80,8 +81,9 @@ let rec merge_stacks if_stack end_node1 end_node2 stack1 stack2 = if s1 == s2 then s1 :: (merge i stack1 stack2) else - let arg = node (N_IF_END_RESULT (end_node1, end_node2, i)) - [] [] in + let arg = node end_node1.loc + (N_IF_END_RESULT (end_node1, end_node2, i)) + [] [] in end_node1.args <- s1 :: end_node1.args; (match end_node2 with @@ -115,7 +117,7 @@ let interp contract = decompile_seq stack seq code and decompile stack (seq : node) ins = - match ins, stack with + match ins.ins, stack with | SEQ exprs, _ -> decompile_seq stack seq exprs @@ -126,26 +128,42 @@ let interp contract = avoid infinite loops here... *) - | IF (SEQ [FAIL], SEQ ( (_ :: _) as ifelse )),_ -> - decompile stack seq - (SEQ (IF (SEQ [FAIL], SEQ []) :: ifelse)) - | IF (SEQ ( (_ :: _) as ifthen ), SEQ [FAIL]),_ -> - decompile stack seq - (SEQ (IF (SEQ [], SEQ [FAIL]) :: ifthen)) - | IF_NONE (SEQ ( (_::_) as ifthen), SEQ [FAIL]),_ -> - decompile stack seq - (SEQ (IF_NONE (SEQ [], SEQ [FAIL]) :: ifthen)) - | IF_CONS (SEQ [FAIL], SEQ ( (_::_) as ifelse ) ),_ -> - decompile stack seq - (SEQ (IF_CONS (SEQ [FAIL], SEQ []) :: ifelse)) + | IF ({ins=SEQ [{ins=FAIL}]} as seq_fail, + {ins=SEQ ( (_ :: _) as ifelse )}),_ -> + decompile stack seq + (mic_loc ins.loc + (SEQ (mic_loc ins.loc + (IF (seq_fail, + mic_loc ins.loc (SEQ []))) :: ifelse))) + | IF ({ins=SEQ ( (_ :: _) as ifthen )}, + ({ins=SEQ [{ins=FAIL}]} as seq_fail)),_ -> + decompile stack seq + (mic_loc ins.loc + (SEQ (mic_loc ins.loc + (IF (mic_loc ins.loc (SEQ []), + seq_fail)) :: ifthen))) + | IF_NONE ({ins=SEQ ( (_::_) as ifthen)}, + ({ins=SEQ [{ins=FAIL}]} as seq_fail)),_ -> + decompile stack seq + (mic_loc ins.loc + (SEQ (mic_loc ins.loc + (IF_NONE (mic_loc ins.loc (SEQ []), + seq_fail)) :: ifthen))) + | IF_CONS ({ins=SEQ [{ins=FAIL}]} as seq_fail, + {ins=SEQ ( (_::_) as ifelse )} ),_ -> + decompile stack seq + (mic_loc ins.loc + (SEQ (mic_loc ins.loc + (IF_CONS (seq_fail, + mic_loc ins.loc (SEQ []))) :: ifelse))) | IF (ifthen, ifelse), x :: stack -> - let if_node = node (N_UNKNOWN "IF") [x] [seq] in + let if_node = node ins.loc (N_UNKNOWN "IF") [x] [seq] in - let then_node = node (N_IF_THEN if_node) [] [] in + let then_node = node ifthen.loc (N_IF_THEN if_node) [] [] in let then_stack = stack in - let else_node = node (N_IF_ELSE if_node) [] [] in + let else_node = node ifelse.loc (N_IF_ELSE if_node) [] [] in let else_stack = stack in decompile_if if_node stack @@ -153,13 +171,13 @@ let interp contract = ifelse else_node else_stack | IF_NONE (ifthen, ifelse), x :: stack -> - let if_node = node (N_UNKNOWN "IF_NONE") [x] [seq] in + let if_node = node ins.loc (N_UNKNOWN "IF_NONE") [x] [seq] in - let then_node = node (N_IF_NONE if_node) [] [] in + let then_node = node ifthen.loc (N_IF_NONE if_node) [] [] in let then_stack = stack in - let var0 = node (N_IF_RESULT (if_node, 0)) [] [] in - let else_node = node (N_IF_SOME (if_node, var0)) [] [] in + let var0 = node ifelse.loc (N_IF_RESULT (if_node, 0)) [] [] in + let else_node = node ifelse.loc (N_IF_SOME (if_node, var0)) [] [] in let else_stack = var0 :: stack in decompile_if if_node stack @@ -167,14 +185,14 @@ let interp contract = ifelse else_node else_stack | IF_LEFT (ifthen, ifelse), x :: stack -> - let if_node = node (N_UNKNOWN "IF_LEFT") [x] [seq] in + let if_node = node ins.loc (N_UNKNOWN "IF_LEFT") [x] [seq] in - let var0 = node (N_IF_RESULT (if_node,0)) [] [] in - let then_node = node (N_IF_LEFT (if_node, var0)) [] [] in + let var0 = node ifthen.loc (N_IF_RESULT (if_node,0)) [] [] in + let then_node = node ifthen.loc (N_IF_LEFT (if_node, var0)) [] [] in let then_stack = var0 :: stack in - let var0 = node (N_IF_RESULT (if_node,0)) [] [] in - let else_node = node (N_IF_RIGHT (if_node, var0)) [] [] in + let var0 = node ifelse.loc (N_IF_RESULT (if_node,0)) [] [] in + let else_node = node ifelse.loc (N_IF_RIGHT (if_node, var0)) [] [] in let else_stack = var0 :: stack in decompile_if if_node stack @@ -183,14 +201,15 @@ let interp contract = | IF_CONS (ifthen, ifelse), x :: stack -> - let if_node = node (N_UNKNOWN "IF_CONS") [x] [seq] in + let if_node = node ins.loc (N_UNKNOWN "IF_CONS") [x] [seq] in - let var0 = node (N_IF_RESULT (if_node,0)) [] [] in - let var1 = node (N_IF_RESULT (if_node, 1)) [] [] in - let then_node = node (N_IF_CONS (if_node, var0, var1)) [] [] in + let var0 = node ifthen.loc (N_IF_RESULT (if_node,0)) [] [] in + let var1 = node ifthen.loc (N_IF_RESULT (if_node, 1)) [] [] in + let then_node = + node ifthen.loc (N_IF_CONS (if_node, var0, var1)) [] [] in let then_stack = var0 :: var1 :: stack in - let else_node = node (N_IF_NIL if_node) [] [] in + let else_node = node ifelse.loc (N_IF_NIL if_node) [] [] in let else_stack = stack in decompile_if if_node stack @@ -199,10 +218,10 @@ let interp contract = | LOOP code, x :: prev_stack -> - let loop_node = node (N_UNKNOWN "LOOP") [x] [seq] in - let begin_node = node (N_LOOP_BEGIN loop_node) [] [] in + let loop_node = node ins.loc (N_UNKNOWN "LOOP") [x] [seq] in + let begin_node = node code.loc (N_LOOP_BEGIN loop_node) [] [] in - let pseudo_node = node (N_UNKNOWN "LOOP") [] [] in + let pseudo_node = node ins.loc (N_UNKNOWN "LOOP") [] [] in begin match decompile prev_stack pseudo_node code with | [],_ -> assert false | x :: end_stack,_ -> @@ -218,7 +237,7 @@ let interp contract = if s1 == s2 then s1 :: (merge i stack1 stack2) else - let arg = node (N_LOOP_ARG (begin_node,i)) [] [] in + let arg = node code.loc (N_LOOP_ARG (begin_node,i)) [] [] in begin_node.args <- s1 :: begin_node.args; arg :: (merge (i+1) stack1 stack2) | _ -> assert false @@ -231,8 +250,9 @@ let interp contract = | [], _ -> assert false | x :: end_stack, loop_seq -> - let end_node = node (N_LOOP_END (loop_node, begin_node, x)) [] - [ loop_seq ] in + let end_node = node x.loc + (N_LOOP_END (loop_node, begin_node, x)) [] + [ loop_seq ] in let rec merge i stack1 stack2 = if stack1 == stack2 then stack1 @@ -244,12 +264,13 @@ let interp contract = | { kind = N_LOOP_ARG (n, i) }:: stack1, s2 :: stack2 when n == begin_node -> - let arg = node (N_LOOP_RESULT (loop_node, begin_node, i)) [] [] in - end_node.args <- s2 :: end_node.args; - arg :: merge (i+1) stack1 stack2 + let arg = node ins.loc + (N_LOOP_RESULT (loop_node, begin_node, i)) [] [] in + end_node.args <- s2 :: end_node.args; + arg :: merge (i+1) stack1 stack2 | s1 :: stack1, s2 :: stack2 -> - assert (s1 == s2); - s1 :: (merge i stack1 stack2) + assert (s1 == s2); + s1 :: (merge i stack1 stack2) | _ -> assert false in @@ -262,15 +283,16 @@ let interp contract = | LAMBDA (arg_ty, res_ty, code), stack -> - let begin_node = node N_LAMBDA_BEGIN [] [] in + let begin_node = node ins.loc N_LAMBDA_BEGIN [] [] in let lambda_stack, lambda_seq = decompile [ begin_node ] begin_node code in begin match lambda_stack with | [] | _ :: _ :: _ -> assert false | [res_node] -> - let end_node = node (N_LAMBDA_END begin_node) [res_node] + let end_node = node res_node.loc (N_LAMBDA_END begin_node) [res_node] [lambda_seq] in - let lambda_node = node (N_LAMBDA (begin_node, end_node, arg_ty, res_ty)) [] [seq] + let lambda_node = node ins.loc + (N_LAMBDA (begin_node, end_node, arg_ty, res_ty)) [] [seq] in lambda_node :: stack, lambda_node end @@ -291,140 +313,143 @@ let interp contract = (* Primitives *) | PUSH (ty, cst), stack -> - let x = node (N_CONST (ty, cst)) [] [seq] in + let x = node ins.loc (N_CONST (ty, cst)) [] [seq] in x :: stack, x | FAIL, _ -> - let x = node N_FAIL [] [seq] in + let x = node ins.loc N_FAIL [] [seq] in [x], x | TRANSFER_TOKENS, arg :: amount :: contract :: arg_storage :: [] -> - let res_storage = node (N_VAR "storage") [] [] in - let result = node (N_TRANSFER_RESULT 1) [] [] in - let x = node (N_TRANSFER (res_storage, result)) + let res_storage = node ins.loc (N_VAR "storage") [] [] in + let result = node ins.loc (N_TRANSFER_RESULT 1) [] [] in + let x = node ins.loc (N_TRANSFER (res_storage, result)) [contract; amount; arg_storage; arg ] [seq] in [ result ; res_storage ], x | SOURCE (arg_ty, res_ty), stack -> (* TODO : keep types too ! *) - let x = node (N_SOURCE (arg_ty, res_ty)) [] [seq] in + let x = node ins.loc (N_SOURCE (arg_ty, res_ty)) [] [seq] in x :: stack, x | NOW, stack -> - let x = node (N_PRIM "NOW") [] [seq] in + let x = node ins.loc (N_PRIM "NOW") [] [seq] in x :: stack, x | BALANCE, stack -> - let x = node (N_PRIM "BALANCE") [] [seq] in + let x = node ins.loc (N_PRIM "BALANCE") [] [seq] in x :: stack, x | AMOUNT, stack -> - let x = node (N_PRIM "AMOUNT") [] [seq] in + let x = node ins.loc (N_PRIM "AMOUNT") [] [seq] in x :: stack, x | DEFAULT_ACCOUNT, key :: stack -> - let x = node (N_PRIM "DEFAULT_ACCOUNT") [key] [seq] in + let x = node ins.loc (N_PRIM "DEFAULT_ACCOUNT") [key] [seq] in x :: stack, x | MANAGER, x :: stack -> - let x = node (N_PRIM "MANAGER") [x] [seq] in + let x = node ins.loc (N_PRIM "MANAGER") [x] [seq] in x :: stack, x | H, x :: stack -> - let x = node (N_PRIM "H") [x] [seq] in + let x = node ins.loc (N_PRIM "H") [x] [seq] in + x :: stack, x + | HASH_KEY, x :: stack -> + let x = node ins.loc (N_PRIM "HASH_KEY") [x] [seq] in x :: stack, x | SOME, x :: stack -> - let x = node (N_PRIM "SOME") [x] [seq] in + let x = node ins.loc (N_PRIM "SOME") [x] [seq] in x :: stack, x | LEFT right_ty, x :: stack -> (* TODO : keep types too ! *) - let x = node (N_LEFT right_ty) [x] [seq] in + let x = node ins.loc (N_LEFT right_ty) [x] [seq] in x :: stack, x | RIGHT left_ty, x :: stack -> (* TODO : keep types too ! *) - let x = node (N_RIGHT left_ty) [x] [seq] in + let x = node ins.loc (N_RIGHT left_ty) [x] [seq] in x :: stack, x | INT, x :: stack -> - let x = node (N_PRIM "INT") [x] [seq] in + let x = node ins.loc (N_PRIM "INT") [x] [seq] in x :: stack, x | ABS, x :: stack -> - let x = node (N_PRIM "ABS") [x] [seq] in + let x = node ins.loc (N_PRIM "ABS") [x] [seq] in x :: stack, x | CAR, { kind = N_PRIM "PAIR"; args = [x;_] } :: stack -> x :: stack, seq | CDR, { kind = N_PRIM "PAIR"; args = [_;x] } :: stack -> x :: stack, seq | CAR, x :: stack -> - let x = node (N_PRIM "CAR") [x] [seq] in + let x = node ins.loc (N_PRIM "CAR") [x] [seq] in x :: stack, x | CDR, x :: stack -> - let x = node (N_PRIM "CDR") [x] [seq] in + let x = node ins.loc (N_PRIM "CDR") [x] [seq] in x :: stack, x | NEQ, { kind = N_PRIM "COMPARE"; args = [x;y] } :: stack-> - let x = node (N_PRIM "NEQ") [x;y] [seq] in + let x = node ins.loc (N_PRIM "NEQ") [x;y] [seq] in x :: stack, x | NEQ, x :: stack -> - let x = node (N_PRIM "NEQ") [x] [seq] in + let x = node ins.loc (N_PRIM "NEQ") [x] [seq] in x :: stack, x | EQ, { kind = N_PRIM "COMPARE"; args = [x;y] } :: stack-> - let x = node (N_PRIM "EQ") [x;y] [seq] in + let x = node ins.loc (N_PRIM "EQ") [x;y] [seq] in x :: stack, x | EQ, x :: stack -> - let x = node (N_PRIM "EQ") [x] [seq] in + let x = node ins.loc (N_PRIM "EQ") [x] [seq] in x :: stack, x | LE, { kind = N_PRIM "COMPARE"; args = [x;y] } :: stack-> - let x = node (N_PRIM "LE") [x;y] [seq] in + let x = node ins.loc (N_PRIM "LE") [x;y] [seq] in x :: stack, x | LE, x :: stack -> - let x = node (N_PRIM "LE") [x] [seq] in + let x = node ins.loc (N_PRIM "LE") [x] [seq] in x :: stack, x | LT, { kind = N_PRIM "COMPARE"; args = [x;y] } :: stack-> - let x = node (N_PRIM "LT") [x;y] [seq] in + let x = node ins.loc (N_PRIM "LT") [x;y] [seq] in x :: stack, x | LT, x :: stack -> - let x = node (N_PRIM "LT") [x] [seq] in + let x = node ins.loc (N_PRIM "LT") [x] [seq] in x :: stack, x | GE, { kind = N_PRIM "COMPARE"; args = [x;y] } :: stack-> - let x = node (N_PRIM "GE") [x;y] [seq] in + let x = node ins.loc (N_PRIM "GE") [x;y] [seq] in x :: stack, x | GE, x :: stack -> - let x = node (N_PRIM "GE") [x] [seq] in + let x = node ins.loc (N_PRIM "GE") [x] [seq] in x :: stack, x | GT, { kind = N_PRIM "COMPARE"; args = [x;y] } :: stack-> - let x = node (N_PRIM "GT") [x;y] [seq] in + let x = node ins.loc (N_PRIM "GT") [x;y] [seq] in x :: stack, x | GT, x :: stack -> - let x = node (N_PRIM "GT") [x] [seq] in + let x = node ins.loc (N_PRIM "GT") [x] [seq] in x :: stack, x | CHECK_SIGNATURE, x :: y :: stack -> - let x = node (N_PRIM "CHECK_SIGNATURE") [x; y] [seq] in + let x = node ins.loc (N_PRIM "CHECK_SIGNATURE") [x; y] [seq] in x :: stack, x | MOD, x :: y :: stack -> - let x = node (N_PRIM "MOD") [x; y] [seq] in + let x = node ins.loc (N_PRIM "MOD") [x; y] [seq] in x :: stack, x | DIV, x :: y :: stack -> - let x = node (N_PRIM "DIV") [x; y] [seq] in + let x = node ins.loc (N_PRIM "DIV") [x; y] [seq] in x :: stack, x | CONS, x :: y :: stack -> - let x = node (N_PRIM "CONS") [x; y] [seq] in + let x = node ins.loc (N_PRIM "CONS") [x; y] [seq] in x :: stack, x | MEM, x :: y :: stack -> - let x = node (N_PRIM "MEM") [x;y] [seq] in + let x = node ins.loc (N_PRIM "MEM") [x;y] [seq] in x :: stack, x | CONCAT, x :: y :: stack -> - let x = node (N_PRIM "CONCAT") [x;y] [seq] in + let x = node ins.loc (N_PRIM "CONCAT") [x;y] [seq] in x :: stack, x | OR, x :: y :: stack -> - let x = node (N_PRIM "OR") [x;y] [seq] in + let x = node ins.loc (N_PRIM "OR") [x;y] [seq] in x :: stack, x | MUL, x :: y :: stack -> - let x = node (N_PRIM "MUL") [x;y] [seq] in + let x = node ins.loc (N_PRIM "MUL") [x;y] [seq] in x :: stack, x | EDIV, x :: y :: stack -> - let x = node (N_PRIM "EDIV") [x;y] [seq] in + let x = node ins.loc (N_PRIM "EDIV") [x;y] [seq] in x :: stack, x | ADD, x :: y :: stack -> - let x = node (N_PRIM "ADD") [x;y] [seq] in + let x = node ins.loc (N_PRIM "ADD") [x;y] [seq] in x :: stack, x | SUB, x :: y :: stack -> - let x = node (N_PRIM "SUB") [x;y] [seq] in + let x = node ins.loc (N_PRIM "SUB") [x;y] [seq] in x :: stack, x | PAIR, x :: y :: stack -> - let x = node (N_PRIM "PAIR") [x;y] [seq] in + let x = node ins.loc (N_PRIM "PAIR") [x;y] [seq] in x :: stack, x | COMPARE, x :: { kind = N_CONST (Tint,CInt n)} :: stack @@ -433,65 +458,65 @@ let interp contract = x :: stack, seq | COMPARE, x :: y :: stack -> - let x = node (N_PRIM "COMPARE") [x;y] [seq] in + let x = node ins.loc (N_PRIM "COMPARE") [x;y] [seq] in x :: stack, x | GET, x :: y :: stack -> - let x = node (N_PRIM "GET") [x;y] [seq] in + let x = node ins.loc (N_PRIM "GET") [x;y] [seq] in x :: stack, x | EXEC, x :: y :: stack -> - let x = node (N_PRIM "EXEC") [x;y] [seq] in + let x = node ins.loc (N_PRIM "EXEC") [x;y] [seq] in x :: stack, x | UPDATE, x :: y :: z :: stack -> - let x = node (N_PRIM "UPDATE") [x;y;z] [seq] in + let x = node ins.loc (N_PRIM "UPDATE") [x;y;z] [seq] in x :: stack, x | REDUCE, x :: y :: z :: stack -> - let x = node (N_PRIM "REDUCE") [x;y;z] [seq] in + let x = node ins.loc (N_PRIM "REDUCE") [x;y;z] [seq] in x :: stack, x | MAP, x :: y :: stack -> - let x = node (N_PRIM "MAP") [x;y] [seq] in + let x = node ins.loc (N_PRIM "MAP") [x;y] [seq] in x :: stack, x | SIZE, x :: stack -> - let x = node (N_PRIM "SIZE") [x] [seq] in + let x = node ins.loc (N_PRIM "SIZE") [x] [seq] in x :: stack, x | AND, x :: y :: stack -> - let x = node (N_PRIM "AND") [x; y] [seq] in + let x = node ins.loc (N_PRIM "AND") [x; y] [seq] in x :: stack, x | XOR, x :: y :: stack -> - let x = node (N_PRIM "XOR") [x; y] [seq] in + let x = node ins.loc (N_PRIM "XOR") [x; y] [seq] in x :: stack, x | NOT, x :: stack -> - let x = node (N_PRIM "NOT") [x] [seq] in + let x = node ins.loc (N_PRIM "NOT") [x] [seq] in x :: stack, x | STEPS_TO_QUOTA, stack -> - let x = node (N_PRIM "STEPS_TO_QUOTA") [] [seq] in + let x = node ins.loc (N_PRIM "STEPS_TO_QUOTA") [] [seq] in x :: stack, x | CREATE_ACCOUNT, manager :: delegate :: delegatable :: amount :: stack -> - let x = node (N_PRIM "CREATE_ACCOUNT") + let x = node ins.loc (N_PRIM "CREATE_ACCOUNT") [manager; delegate; delegatable; amount] [seq] in x :: stack, x | CREATE_CONTRACT, manager :: delegate :: spendable :: delegatable :: amount :: contract :: storage :: stack -> - let x = node (N_PRIM "CREATE_CONTRACT") + let x = node ins.loc (N_PRIM "CREATE_CONTRACT") [manager; delegate; spendable; delegatable; amount; contract; storage] [seq] in x :: stack, x | _ -> - let ins = LiquidEmit.emit_code ins in - let s = LiquidPrinter.Michelson.string_of_code ins in - LiquidLoc.raise_error "Error while decompiling:\n %s!" s + (* let ins = LiquidEmit.emit_code ins in *) + let s = LiquidPrinter.Michelson.string_of_loc_michelson ins in + LiquidLoc.raise_error ~loc:ins.loc "Error while decompiling:\n %s%!" s and decompile_if if_node if_stack ifthen then_node then_stack @@ -504,9 +529,9 @@ let interp contract = decompile else_stack else_node ifelse in - let then_end_node = node (N_IF_END (if_node, then_node)) [] + let then_end_node = node ifthen.loc (N_IF_END (if_node, then_node)) [] [ then_seq ] in - let else_end_node = node (N_IF_END (if_node, else_node)) [] + let else_end_node = node ifelse.loc (N_IF_END (if_node, else_node)) [] [ else_seq ] in let stack = merge_stacks if_stack then_end_node (Some else_end_node) @@ -516,21 +541,23 @@ let interp contract = stack, if_node in - let start_node = node N_START [] [] in - let initial_code = match contract.code with - | SEQ code -> SEQ (PAIR :: code) + let initial_code = match contract.code.ins with + | SEQ code -> mic_loc contract.code.loc + (SEQ (mic_loc contract.code.loc PAIR :: code)) | _ -> assert false in + let start_node = node contract.code.loc N_START [] [] in + let initial_stack = [ - node (N_VAR "parameter") [] []; - node (N_VAR "storage") [] []; + node contract.code.loc (N_VAR "parameter") [] []; + node contract.code.loc (N_VAR "storage") [] []; ] in let stack, seq = decompile initial_stack start_node initial_code in let end_node = match stack with - [ arg ] -> node N_END [arg] [seq] + [ arg ] -> node arg.loc N_END [arg] [seq] | _ -> assert false in let code = (start_node, end_node) in diff --git a/tools/liquidity/liquidInterp.mli b/tools/liquidity/liquidInterp.mli index 6dc81e3b..a253f789 100644 --- a/tools/liquidity/liquidInterp.mli +++ b/tools/liquidity/liquidInterp.mli @@ -9,4 +9,4 @@ open LiquidTypes -val interp : pre_michelson contract -> node_exp contract +val interp : loc_michelson contract -> node_exp contract diff --git a/tools/liquidity/liquidLoc.ml b/tools/liquidity/liquidLoc.ml index ef6c602b..1a787442 100644 --- a/tools/liquidity/liquidLoc.ml +++ b/tools/liquidity/liquidLoc.ml @@ -47,8 +47,11 @@ let default_warning_printer loc w = Format.eprintf "%a: Warning: @[%a@]\n%!" print_loc loc (fun fmt -> function | Unused name -> - Format.fprintf fmt "unused variable %S" name) - w + Format.fprintf fmt "unused variable %S" name + | UnusedMatched constr -> + Format.fprintf fmt + "unused branch, constructor %S is already matched" constr + ) w let warning_printer = ref default_warning_printer diff --git a/tools/liquidity/liquidMain.ml b/tools/liquidity/liquidMain.ml index 9c6a485b..6d77bbc2 100644 --- a/tools/liquidity/liquidMain.ml +++ b/tools/liquidity/liquidMain.ml @@ -64,13 +64,14 @@ let compile_liquid_file filename = (LiquidToTezos.string_of_contract (LiquidToTezos.convert_contract pre_michelson)); Printf.eprintf "File %S generated\n%!" output; - Printf.eprintf "Typecheck with:\n tezos-client typecheck program %s\n" output + Printf.eprintf "If tezos is compiled, you may want to typecheck with:\n"; + Printf.eprintf " tezos-client typecheck program %s\n" output let compile_tezos_file filename = - let code, contract_hash = LiquidToTezos.read_tezos_file filename in + let code, contract_hash, loc_table = LiquidToTezos.read_tezos_file filename in - let c = LiquidFromTezos.convert_contract code in + let c = LiquidFromTezos.convert_contract loc_table code in let c = LiquidClean.clean_contract c in let c = LiquidInterp.interp c in if !debug then begin diff --git a/tools/liquidity/liquidMichelson.ml b/tools/liquidity/liquidMichelson.ml index dfed3fa6..c909662d 100644 --- a/tools/liquidity/liquidMichelson.ml +++ b/tools/liquidity/liquidMichelson.ml @@ -12,27 +12,26 @@ open LiquidTypes (* Translation to Michelson *) +let ii i = {i} +let seq exprs = {i=SEQ exprs} -let seq exprs = SEQ exprs - -let dup n = DUP n +let dup n = {i=DUP n} (* n = size of preserved head of stack *) -let dip n exprs = - DIP (n, seq exprs) +let dip n exprs = {i=DIP (n, seq exprs)} -let push ty cst = PUSH (ty, cst) +let push ty cst = {i=PUSH (ty, cst)} (* n = size of preserved head of stack *) let drop_stack n depth = if depth = 0 then [] else let rec drop_stack depth = if depth = 0 then [] else - DROP :: (drop_stack (depth-1)) + {i=DROP} :: (drop_stack (depth-1)) in let exps = drop_stack depth in - if n = 0 then exps else [DIP_DROP (n, List.length exps)] + if n = 0 then exps else [{i=DIP_DROP (n, List.length exps)}] (* The type of a contract code is usually: lambda (pair (pair tez 'arg) 'global) -> (pair 'ret 'global) *) @@ -59,7 +58,7 @@ let translate_code code = if transfer1 then (0, StringMap.empty) else (depth, env) in let e2, transfer2 = compile depth env e2 in - e1 @ [ DROP ] @ e2, transfer1 || transfer2 + e1 @ [ ii DROP ] @ e2, transfer1 || transfer2 | Let (name, loc, e1, e2) -> let e1, transfer1 = compile depth env e1 in @@ -70,7 +69,7 @@ let translate_code code = let depth = depth + 1 in let e2, transfer2 = compile depth env e2 in let cleanup_stack = - if transfer2 then [] else [ DIP_DROP (1,1)] + if transfer2 then [] else [ {i=DIP_DROP (1,1)}] in e1 @ e2 @ cleanup_stack, transfer1 || transfer2 @@ -79,7 +78,8 @@ let translate_code code = let env = StringMap.add arg_name 0 env in let depth = 1 in let body = compile_no_transfer depth env body in - [ LAMBDA (arg_type, res_type, seq (body @ [DIP_DROP (1,1)])) ], false + [ {i=LAMBDA (arg_type, res_type, seq (body @ [ + {i=DIP_DROP (1,1)}]))} ], false | Closure (arg_name, p_arg_type, loc, call_env, body, res_type) -> let call_env_code = match call_env with @@ -90,7 +90,7 @@ let translate_code code = call_env_code @ (compile_desc depth env (Lambda (arg_name, p_arg_type, loc, body, res_type)) |> fst) @ - [ PAIR ], false + [ ii PAIR ], false | If (cond, ifthen, ifelse) -> let cond = compile_no_transfer depth env cond in @@ -105,8 +105,8 @@ let translate_code code = | true, false -> [], drop_stack 1 depth | false, true -> drop_stack 1 depth, [] in - cond @ [ (IF (seq (ifthen @ ifthen_end), - seq (ifelse @ ifelse_end) ))], + cond @ [ {i= IF (seq (ifthen @ ifthen_end), + seq (ifelse @ ifelse_end) )}], transfer1 || transfer2 | LetTransfer( storage_name, result_name, @@ -125,10 +125,10 @@ let translate_code code = let body, transfer = compile 2 env body_exp in let cleanup_stack = if transfer then [] - else [ DIP_DROP (1,2) ] + else [ {i=DIP_DROP (1,2)} ] in storage @ contract @ amount @ arg @ drop @ - [ TRANSFER_TOKENS ] @ body @ + [ ii TRANSFER_TOKENS ] @ body @ cleanup_stack, true | Apply (Prim_unknown, _loc, args) -> assert false @@ -136,8 +136,8 @@ let translate_code code = | Apply (Prim_exec, _loc, [arg; { ty = Tclosure _ } as f]) -> let f_env = compile_no_transfer depth env f in let arg = compile_no_transfer (depth+1) env arg in - f_env @ arg @ [ dip 1 [ dup 1; CAR; SWAP; CDR] ] @ - [ PAIR ; EXEC ], false + f_env @ arg @ [ dip 1 [ dup 1; ii CAR; ii SWAP; ii CDR] ] @ + [ ii PAIR ; ii EXEC ], false | Apply (prim, _loc, args) -> compile_prim depth env prim args, false @@ -153,13 +153,13 @@ let translate_code code = let ifsome, transfer3 = compile depth env ifsome in let (ifnone_end, ifsome_end) = match transfer1, transfer2 with - | false, false -> [], [ DIP_DROP(1,1) ] + | false, false -> [], [ {i=DIP_DROP(1,1)} ] | true, true -> [], [] | true, false -> [], drop_stack 1 depth | false, true -> drop_stack 1 (depth-1), [] in - arg @ [ (IF_NONE (seq (ifnone @ ifnone_end), - seq (ifsome @ ifsome_end) ))], + arg @ [ {i=IF_NONE (seq (ifnone @ ifnone_end), + seq (ifsome @ ifsome_end) )}], transfer1 || transfer2 || transfer3 | MatchList(arg, loc, head_name, tail_name, ifcons, ifnil) -> @@ -174,13 +174,13 @@ let translate_code code = let ifcons, transfer3 = compile depth env ifcons in let (ifnil_end, ifcons_end) = match transfer1, transfer2 with - | false, false -> [], [ DIP_DROP(1,2) ] + | false, false -> [], [ {i=DIP_DROP(1,2)} ] | true, true -> [], [] | true, false -> [], drop_stack 1 depth | false, true -> drop_stack 1 (depth-2), [] in - arg @ [ (IF_CONS (seq (ifcons @ ifcons_end), - seq (ifnil @ ifnil_end) ))], + arg @ [ {i=IF_CONS (seq (ifcons @ ifcons_end), + seq (ifnil @ ifnil_end) )}], transfer1 || transfer2 || transfer3 | MatchVariant(arg, loc, cases) -> @@ -190,7 +190,7 @@ let translate_code code = in let has_transfer = ref false in let cases = List.map (function - | (constr, [ arg_name ], e) -> + | CConstr (constr, [ arg_name ]), e -> let env = StringMap.add arg_name depth env in let depth = depth + 1 in let e, transfer = compile depth env e in @@ -205,7 +205,7 @@ let translate_code code = let left_end = match !has_transfer, transfer with | true, true -> [] - | false, false -> [ DIP_DROP(1,1) ] + | false, false -> [ {i=DIP_DROP(1,1)} ] | false, true -> assert false | true, false -> drop_stack 1 (depth-1) in @@ -214,7 +214,7 @@ let translate_code code = | [] -> left | _ -> let right = iter cases in - [ IF_LEFT( seq left, seq right ) ] + [ {i=IF_LEFT( seq left, seq right )} ] in arg @ iter cases, !has_transfer @@ -226,10 +226,13 @@ let translate_code code = let env = StringMap.add name depth env in let depth = depth + 1 in let body, transfer2 = compile depth env body in - let body_end = [ DIP_DROP (1,1); DUP 1; CAR; DIP (1, seq [ CDR ]) ] in + let body_end = [ {i=DIP_DROP (1,1)}; + {i=DUP 1}; + ii CAR; + {i=DIP (1, seq [ ii CDR ])} ] in arg - @ [ PUSH (Tbool, CBool true)] - @ [ LOOP (seq (body @ body_end)) ], + @ [ {i=PUSH (Tbool, CBool true)}] + @ [ {i=LOOP (seq (body @ body_end))} ], transfer1 || transfer2 (* removed during typechecking, replaced by tuple *) @@ -244,13 +247,13 @@ let translate_code code = | Prim_tuple_get, [arg; { desc = Const (_, (CInt n | CNat n))} ] -> let arg = compile_no_transfer depth env arg in let n = LiquidPrinter.int_of_integer n in - arg @ [ CDAR n ] + arg @ [ {i=CDAR n} ] | Prim_tuple_get, _ -> assert false | Prim_tuple_get_last, [arg; { desc = Const (_, (CInt n | CNat n))} ] -> let arg = compile_no_transfer depth env arg in let n = LiquidPrinter.int_of_integer n in - arg @ [ CDDR (n-1) ] + arg @ [ {i=CDDR (n-1)} ] | Prim_tuple_get_last, _ -> assert false (* @@ -273,32 +276,32 @@ set x n y = x + [ DUP; CAR; SWAP; CDR ]*n + x_code @ set_code | Prim_tuple_set_last, _ -> assert false - | Prim_fail,_ -> [ FAIL ] - | Prim_self, _ -> [ SELF ] - | Prim_balance, _ -> [ BALANCE ] - | Prim_now, _ -> [ NOW ] - | Prim_amount, _ -> [ AMOUNT ] - | Prim_gas, _ -> [ STEPS_TO_QUOTA ] + | Prim_fail,_ -> [ ii FAIL ] + | Prim_self, _ -> [ ii SELF ] + | Prim_balance, _ -> [ ii BALANCE ] + | Prim_now, _ -> [ ii NOW ] + | Prim_amount, _ -> [ ii AMOUNT ] + | Prim_gas, _ -> [ ii STEPS_TO_QUOTA ] | Prim_Left, [ arg; { ty = right_ty }] -> compile_no_transfer depth env arg @ - [ LEFT right_ty] + [ {i=LEFT right_ty} ] | Prim_Left, _ -> assert false | Prim_Right, [ arg; { ty = left_ty } ] -> compile_no_transfer depth env arg @ - [ RIGHT left_ty ] + [ {i=RIGHT left_ty} ] | Prim_Right, _ -> assert false | Prim_Source, [ { ty = from_ty }; { ty = to_ty } ] -> - [ SOURCE (from_ty, to_ty) ] + [ {i=SOURCE (from_ty, to_ty)} ] | Prim_Source, _ -> assert false (* catch the special case of [a;b;c] where the ending NIL is not annotated with a type *) | Prim_Cons, [ { ty } as arg; { ty = Tunit } ] -> let arg = compile_no_transfer (depth+1) env arg in - [ PUSH (Tlist ty, CList[]) ] @ arg @ [ CONS ] + [ {i=PUSH (Tlist ty, CList[])} ] @ arg @ [ ii CONS ] (* Should be removed in LiquidCheck *) | Prim_unknown, _ @@ -315,62 +318,63 @@ the ending NIL is not annotated with a type *) | Prim_set_update|Prim_set_mem|Prim_set_reduce|Prim_Some | Prim_concat|Prim_list_reduce|Prim_list_map|Prim_manager | Prim_create_account|Prim_create_contract|Prim_set_map - | Prim_hash|Prim_check|Prim_default_account|Prim_list_size + | Prim_hash|Prim_hash_key|Prim_check|Prim_default_account|Prim_list_size | Prim_set_size|Prim_map_size|Prim_or|Prim_and|Prim_xor | Prim_not|Prim_abs|Prim_int|Prim_neg|Prim_lsr|Prim_lsl | Prim_exec|Prim_Cons),_ -> let _depth, args_code = compile_args depth env args in let prim_code = match prim, List.length args with - | Prim_eq, 2 -> [ COMPARE; EQ ] - | Prim_neq, 2 -> [ COMPARE; NEQ ] - | Prim_lt, 2 -> [ COMPARE; LT ] - | Prim_le, 2 -> [ COMPARE; LE ] - | Prim_gt, 2 -> [ COMPARE; GT ] - | Prim_ge, 2 -> [ COMPARE; GE ] - | Prim_compare, 2 -> [ COMPARE ] - | Prim_add, 2 -> [ ADD ] - | Prim_sub, 2 -> [ SUB ] - | Prim_mul, 2 -> [ MUL ] - | Prim_ediv, 2 -> [ EDIV ] - | Prim_map_find, 2 -> [ GET ] - | Prim_map_update, 3 -> [ UPDATE ] - | Prim_map_mem, 2 -> [ MEM ] - | Prim_map_reduce, 3 -> [ REDUCE ] - | Prim_map_map, 2 -> [ MAP ] - - | Prim_set_update, 3 -> [ UPDATE ] - | Prim_set_mem, 2 -> [ MEM ] - | Prim_set_reduce, 3 -> [ REDUCE ] - | Prim_set_map, 2 -> [ MAP ] - - | Prim_Some, 1 -> [ SOME ] - | Prim_concat, 2 -> [ CONCAT ] - - | Prim_list_reduce, 3 -> [ REDUCE ] - | Prim_list_map, 2 -> [ MAP ] - - | Prim_manager, 1 -> [ MANAGER ] - | Prim_create_account, 4 -> [ CREATE_ACCOUNT ] - | Prim_create_contract, 7 -> [ CREATE_CONTRACT ] - | Prim_hash, 1 -> [ H ] - | Prim_check, 2 -> [ CHECK_SIGNATURE ] - | Prim_default_account, 1 -> [ DEFAULT_ACCOUNT ] - | Prim_list_size, 1 -> [ SIZE ] - | Prim_set_size, 1 -> [ SIZE ] - | Prim_map_size, 1 -> [ SIZE ] - - | Prim_Cons, 2 -> [ CONS ] - | Prim_or, 2 -> [ OR ] - | Prim_and, 2 -> [ AND ] - | Prim_xor, 2 -> [ XOR ] - | Prim_not, 1 -> [ NOT ] - | Prim_abs, 1 -> [ ABS ] - | Prim_int, 1 -> [ INT ] - | Prim_neg, 1 -> [ NEG ] - | Prim_lsr, 2 -> [ LSR ] - | Prim_lsl, 2 -> [ LSL ] - - | Prim_exec, 2 -> [ EXEC ] + | Prim_eq, 2 -> [ ii COMPARE; ii EQ ] + | Prim_neq, 2 -> [ ii COMPARE; ii NEQ ] + | Prim_lt, 2 -> [ ii COMPARE; ii LT ] + | Prim_le, 2 -> [ ii COMPARE; ii LE ] + | Prim_gt, 2 -> [ ii COMPARE; ii GT ] + | Prim_ge, 2 -> [ ii COMPARE; ii GE ] + | Prim_compare, 2 -> [ ii COMPARE ] + | Prim_add, 2 -> [ ii ADD ] + | Prim_sub, 2 -> [ ii SUB ] + | Prim_mul, 2 -> [ ii MUL ] + | Prim_ediv, 2 -> [ ii EDIV ] + | Prim_map_find, 2 -> [ ii GET ] + | Prim_map_update, 3 -> [ ii UPDATE ] + | Prim_map_mem, 2 -> [ ii MEM ] + | Prim_map_reduce, 3 -> [ ii REDUCE ] + | Prim_map_map, 2 -> [ ii MAP ] + + | Prim_set_update, 3 -> [ ii UPDATE ] + | Prim_set_mem, 2 -> [ ii MEM ] + | Prim_set_reduce, 3 -> [ ii REDUCE ] + | Prim_set_map, 2 -> [ ii MAP ] + + | Prim_Some, 1 -> [ ii SOME ] + | Prim_concat, 2 -> [ ii CONCAT ] + + | Prim_list_reduce, 3 -> [ ii REDUCE ] + | Prim_list_map, 2 -> [ ii MAP ] + + | Prim_manager, 1 -> [ ii MANAGER ] + | Prim_create_account, 4 -> [ ii CREATE_ACCOUNT ] + | Prim_create_contract, 7 -> [ ii CREATE_CONTRACT ] + | Prim_hash, 1 -> [ ii H ] + | Prim_hash_key, 1 -> [ ii HASH_KEY ] + | Prim_check, 2 -> [ ii CHECK_SIGNATURE ] + | Prim_default_account, 1 -> [ ii DEFAULT_ACCOUNT ] + | Prim_list_size, 1 -> [ ii SIZE ] + | Prim_set_size, 1 -> [ ii SIZE ] + | Prim_map_size, 1 -> [ ii SIZE ] + + | Prim_Cons, 2 -> [ ii CONS ] + | Prim_or, 2 -> [ ii OR ] + | Prim_and, 2 -> [ ii AND ] + | Prim_xor, 2 -> [ ii XOR ] + | Prim_not, 1 -> [ ii NOT ] + | Prim_abs, 1 -> [ ii ABS ] + | Prim_int, 1 -> [ ii INT ] + | Prim_neg, 1 -> [ ii NEG ] + | Prim_lsr, 2 -> [ ii LSR ] + | Prim_lsl, 2 -> [ ii LSL ] + + | Prim_exec, 2 -> [ ii EXEC ] | (Prim_eq|Prim_neq|Prim_lt|Prim_le|Prim_gt|Prim_ge | Prim_compare|Prim_add|Prim_sub|Prim_mul|Prim_ediv|Prim_map_find @@ -378,7 +382,7 @@ the ending NIL is not annotated with a type *) | Prim_set_update|Prim_set_mem|Prim_set_reduce|Prim_Some | Prim_concat|Prim_list_reduce|Prim_list_map|Prim_manager | Prim_create_account|Prim_create_contract - | Prim_hash|Prim_check|Prim_default_account|Prim_list_size + | Prim_hash|Prim_hash_key|Prim_check|Prim_default_account|Prim_list_size | Prim_set_size|Prim_map_size|Prim_or|Prim_and|Prim_xor | Prim_not|Prim_abs|Prim_int|Prim_neg|Prim_lsr|Prim_lsl | Prim_exec|Prim_Cons|Prim_set_map),n -> @@ -405,14 +409,14 @@ the ending NIL is not annotated with a type *) and compile_prim_set last depth env n y = if n = 0 then if last then - [ DROP ] + [ ii DROP ] @ compile_no_transfer (depth-1) env y else - [ CDR ] @ compile_no_transfer depth env y @ [ PAIR ] + [ ii CDR ] @ compile_no_transfer depth env y @ [ ii PAIR ] else - [ DUP 1; CAR; SWAP; CDR ] @ + [ {i=DUP 1}; ii CAR; ii SWAP; ii CDR ] @ compile_prim_set last (depth+1) env (n-1) y @ - [ SWAP; PAIR ] + [ ii SWAP; ii PAIR ] and compile_desc_no_transfer depth env e = let (e, transfer) = compile_desc depth env e in @@ -442,7 +446,7 @@ the ending NIL is not annotated with a type *) | arg :: args -> let arg = compile_no_transfer (depth+1) env arg in let args = compile_tuple1 depth env args in - arg @ [ PAIR ] @ args + arg @ [ ii PAIR ] @ args and compile depth env e = compile_desc depth env e.desc @@ -462,8 +466,8 @@ the ending NIL is not annotated with a type *) (* replace ( parameter, storage ) *) let header = [ dup 1; - dip 1 [ CDR ]; - CAR; + dip 1 [ ii CDR ]; + ii CAR; ] in let trailer = if transfer then [] else drop_stack 1 depth in diff --git a/tools/liquidity/liquidMichelson.mli b/tools/liquidity/liquidMichelson.mli index 47cfcb6e..983a2949 100644 --- a/tools/liquidity/liquidMichelson.mli +++ b/tools/liquidity/liquidMichelson.mli @@ -9,4 +9,4 @@ open LiquidTypes -val translate : typed_exp contract -> pre_michelson contract +val translate : typed_exp contract -> noloc_michelson contract diff --git a/tools/liquidity/liquidPeephole.ml b/tools/liquidity/liquidPeephole.ml index f98ab403..c20ac7b3 100644 --- a/tools/liquidity/liquidPeephole.ml +++ b/tools/liquidity/liquidPeephole.ml @@ -10,91 +10,116 @@ open LiquidTypes -let string_of_pre pre = - LiquidPrinter.Michelson.string_of_code (LiquidEmit.emit_code (SEQ pre)) +(* let string_of_pre pre = *) +(* LiquidPrinter.Michelson.string_of_code (LiquidEmit.emit_code (SEQ pre)) *) (* Try to simplify Michelson with peepholes optims: mostly, move DIP_DROPs backwards to decrease the size of the stack. *) -let drops n = LiquidMisc.list_init n (fun _ -> DROP) +let ii i = { i } + +let drops n = LiquidMisc.list_init n (fun _ -> ii DROP) let dip_drop (a,b)= - if a = 0 then drops b else [DIP_DROP(a,b)] - -let rec simplify_pre code = - match code with - | SEQ expr -> SEQ (simplify_seq expr) - | IF (e1, e2) -> IF (simplify_pre e1, simplify_pre e2) - | IF_NONE (e1, e2) -> IF_NONE (simplify_pre e1, simplify_pre e2) - | IF_LEFT (e1, e2) -> IF_LEFT (simplify_pre e1, simplify_pre e2) - | IF_CONS (e1, e2) -> IF_CONS (simplify_pre e1, simplify_pre e2) - | DIP (n, e) -> DIP (n, simplify_pre e) - | LOOP e -> LOOP (simplify_pre e) - | LAMBDA (arg_type, res_type, e) -> - LAMBDA (arg_type, res_type, simplify_pre e) - | _ -> code + if a = 0 then drops b else [ii (DIP_DROP(a,b))] + +let rec simplify_pre { i } = + ii ( + match i with + | SEQ expr -> SEQ (simplify_seq expr) + | IF (e1, e2) -> IF (simplify_pre e1, simplify_pre e2) + | IF_NONE (e1, e2) -> IF_NONE (simplify_pre e1, simplify_pre e2) + | IF_LEFT (e1, e2) -> IF_LEFT (simplify_pre e1, simplify_pre e2) + | IF_CONS (e1, e2) -> IF_CONS (simplify_pre e1, simplify_pre e2) + | DIP (n, e) -> DIP (n, simplify_pre e) + | LOOP e -> LOOP (simplify_pre e) + | LAMBDA (arg_type, res_type, e) -> + LAMBDA (arg_type, res_type, simplify_pre e) + | _ -> i + ) and simplify_seq exprs = match exprs with | [] -> [] | e :: exprs -> let e = simplify_pre e in - if e = FAIL then [FAIL] + if e.i = FAIL then [ii FAIL] else let exprs = simplify_seq exprs in simplify_step e exprs and simplify_step e exprs = - match e, exprs with + match e.i, exprs with | SEQ e, exprs -> simplify_steps e exprs | DIP_DROP(n,0), exprs -> exprs | DIP (0, e), exprs -> simplify_step e exprs - | DUP _, DROP :: exprs -> exprs - | PUSH _, FAIL :: _ - | FAIL, _ -> [FAIL] - - | IF(SEQ (DROP :: e1), SEQ (DROP :: e2)), exprs -> - simplify_step (DIP_DROP(1,1)) - (simplify_step (IF (SEQ e1, SEQ e2)) exprs) - | IF(SEQ (DIP_DROP(n,m) :: e1), SEQ (DIP_DROP(n',m') :: e2)), exprs - when n=n' - -> - let min_m = min m m' in - simplify_step (DIP_DROP(n,min_m)) - (simplify_step - (IF (SEQ - (simplify_step (DIP_DROP(n,m-min_m)) e1), - SEQ - (simplify_step (DIP_DROP(n,m'-min_m)) e2))) exprs) - - | IF (SEQ [FAIL], SEQ [PUSH _]), DROP :: exprs -> - simplify_step (IF (SEQ [FAIL], SEQ [])) exprs - - | IF (SEQ [FAIL], SEQ []), DROP :: exprs -> - simplify_step (DIP_DROP(1,1)) - (simplify_step (IF (SEQ [FAIL], SEQ [])) exprs) - - | IF (SEQ [FAIL], SEQ []), DIP_DROP(n,m) :: exprs -> - simplify_step (DIP_DROP(n+1,m)) - (simplify_step (IF (SEQ [FAIL], SEQ [])) exprs) + | DUP _, {i=DROP} :: exprs -> exprs + | PUSH _, {i=FAIL} :: _ + | FAIL, _ -> [ii FAIL] + + | IF(i1,i2), exprs -> + begin + match i1.i, i2.i,exprs with + | SEQ ({i=DROP} :: e1), SEQ ({i=DROP} :: e2), exprs -> + simplify_stepi (DIP_DROP(1,1)) + (simplify_stepi (IF ( { i = SEQ e1 }, + { i = SEQ e2 })) exprs) + + | SEQ ({ i=DIP_DROP(n,m)} :: e1), + SEQ ({ i=DIP_DROP(n',m')} :: e2), + exprs when n=n' + -> + let min_m = min m m' in + simplify_stepi (DIP_DROP(n,min_m)) + (simplify_stepi + (IF + ({i=SEQ + (simplify_stepi (DIP_DROP(n,m-min_m)) e1)}, + {i=SEQ + (simplify_stepi (DIP_DROP(n,m'-min_m)) e2)} + )) exprs) + + | SEQ [{i=FAIL}], + SEQ [{i=PUSH _}], + {i=DROP} :: exprs -> + simplify_step {i=IF ({i=SEQ [ii FAIL]}, {i=SEQ []})} exprs + + | SEQ [{i=FAIL}], + SEQ [], + {i=DROP} :: exprs -> + simplify_stepi (DIP_DROP(1,1)) + (simplify_stepi + (IF ({i=SEQ [ii FAIL]}, + {i=SEQ []})) exprs) + + | SEQ [{i=FAIL}], + SEQ [], + {i=DIP_DROP(n,m)} :: exprs -> + simplify_stepi (DIP_DROP(n+1,m)) + (simplify_stepi + (IF ({i=SEQ [ii FAIL]}, + {i=SEQ []})) exprs) + + | _ -> e :: exprs + end (* takes nothing, add one item on stack : 0 -> 1 *) | (PUSH _ | NOW | BALANCE | SELF | SOURCE _ | AMOUNT | STEPS_TO_QUOTA | LAMBDA _ ), - DIP_DROP (n,m) :: exprs -> + {i=DIP_DROP (n,m)} :: exprs -> if n > 0 then dip_drop (n-1,m) @ simplify_step e exprs else if m = 1 then exprs else - DIP_DROP (n,m-1) :: exprs + {i=DIP_DROP (n,m-1)} :: exprs | (PUSH _ | NOW | BALANCE | SELF | SOURCE _ | AMOUNT | STEPS_TO_QUOTA | LAMBDA _ - ), DROP :: exprs -> exprs + ), {i=DROP} :: exprs -> exprs (* takes one item on stack, creates one : 1 -> 1 *) @@ -103,8 +128,8 @@ and simplify_step e exprs = | MANAGER | H | NOT | ABS | INT | NEG | LEFT _ | RIGHT _ | EDIV | LSL | LSR ), - DIP_DROP (n,m) :: exprs when n > 0 -> - simplify_step (DIP_DROP (n,m)) + {i=DIP_DROP (n,m)} :: exprs when n > 0 -> + simplify_stepi (DIP_DROP (n,m)) (simplify_step e exprs) | (CAR | CDR | CDAR _ | CDDR _ @@ -112,92 +137,91 @@ and simplify_step e exprs = | MANAGER | H | NOT | ABS | INT | NEG | LEFT _ | RIGHT _ | EDIV | LSL | LSR ), - DROP :: exprs -> DROP :: exprs + {i=DROP} :: exprs -> {i=DROP} :: exprs (* takes two items on stack, creates one : 2 -> 1 *) | (PAIR | ADD | SUB | COMPARE | GET | CONCAT | MEM | CONS | CHECK_SIGNATURE | EXEC | MAP | OR | AND | XOR | MUL), - DIP_DROP (n,m) :: exprs when n > 0 -> - simplify_step (DIP_DROP (n+1,m)) + {i=DIP_DROP (n,m)} :: exprs when n > 0 -> + simplify_stepi (DIP_DROP (n+1,m)) (simplify_step e exprs) (* takes three items on stack, creates one *) | (UPDATE | REDUCE), - DIP_DROP (n,m) :: exprs when n > 0 -> - simplify_step (DIP_DROP (n+2,m)) + {i=DIP_DROP (n,m)} :: exprs when n > 0 -> + simplify_stepi (DIP_DROP (n+2,m)) (simplify_step e exprs) (* takes four items on stack, creates one : 4 -> 1 *) | (CREATE_ACCOUNT), - DIP_DROP (n,m) :: exprs when n > 0 -> - simplify_step (DIP_DROP (n+3,m)) + {i=DIP_DROP (n,m)} :: exprs when n > 0 -> + simplify_stepi (DIP_DROP (n+3,m)) (simplify_step e exprs) (* takes two items on stack, creates two : 2 -> 2 *) | SWAP, - DIP_DROP (n,m) :: exprs when n > 1 -> - simplify_step (DIP_DROP (n,m)) + {i=DIP_DROP (n,m)} :: exprs when n > 1 -> + simplify_stepi (DIP_DROP (n,m)) (simplify_step e exprs) - - | DIP (n,e), DROP :: exprs when n > 0 -> - DROP :: simplify_step (DIP(n-1,e)) exprs + | DIP (n,e), {i=DROP} :: exprs when n > 0 -> + {i=DROP} :: simplify_stepi (DIP(n-1,e)) exprs - | DIP_DROP (n,m), DIP_DROP (n',m') :: exprs when n = n' -> - DIP_DROP (n, m+m') :: exprs + | DIP_DROP (n,m), {i=DIP_DROP (n',m')} :: exprs when n = n' -> + {i=DIP_DROP (n, m+m')} :: exprs - | PUSH (ty', CList tail), PUSH (ty, head) :: CONS :: exprs + | PUSH (ty', CList tail), {i=PUSH (ty, head)} :: {i=CONS} :: exprs when ty' = Tlist ty -> - simplify_step (PUSH (ty', CList (head :: tail))) exprs - - | DUP 1, DIP_DROP (1,1) :: exprs -> exprs - | DUP 1, DIP_DROP (1,m) :: exprs when m > 1 -> - simplify_step (DIP_DROP (1, m-1)) exprs - - | DUP 2, DIP_DROP (1,1) :: exprs -> - simplify_step DROP (simplify_step (DUP 1) exprs) - | DUP 2, DIP_DROP (1,2) :: exprs -> - simplify_step DROP exprs - - | DUP 3, DIP_DROP (2,2) :: exprs -> - simplify_step SWAP (simplify_step DROP (simplify_step SWAP exprs)) - | DUP 2, SWAP :: DROP :: exprs -> - simplify_step DROP - (simplify_step (DUP 1) exprs) - | DUP 2, DIP_DROP (2,1) :: exprs -> - simplify_step SWAP exprs - | DUP n, DIP_DROP(m,p) :: exprs -> + simplify_stepi (PUSH (ty', CList (head :: tail))) exprs + + | DUP 1, {i=DIP_DROP (1,1)} :: exprs -> exprs + | DUP 1, {i=DIP_DROP (1,m)} :: exprs when m > 1 -> + simplify_stepi (DIP_DROP (1, m-1)) exprs + + | DUP 2, {i=DIP_DROP (1,1)} :: exprs -> + simplify_stepi DROP (simplify_stepi (DUP 1) exprs) + | DUP 2, {i=DIP_DROP (1,2)} :: exprs -> + simplify_stepi DROP exprs + + | DUP 3, {i=DIP_DROP (2,2)} :: exprs -> + simplify_stepi SWAP (simplify_stepi DROP (simplify_stepi SWAP exprs)) + | DUP 2, {i=SWAP} :: {i=DROP} :: exprs -> + simplify_stepi DROP + (simplify_stepi (DUP 1) exprs) + | DUP 2, {i=DIP_DROP (2,1)} :: exprs -> + simplify_stepi SWAP exprs + | DUP n, {i=DIP_DROP(m,p)} :: exprs -> (* let before = DUP n :: DIP_DROP(m,p) :: exprs in *) let after = if n= m+p then if m = 1 then - drops p @ (simplify_step (DUP (n-p)) exprs) + drops p @ (simplify_stepi (DUP (n-p)) exprs) else - simplify_step (DIP_DROP (m-1,p)) - (simplify_step (DUP (n-p)) exprs) + simplify_stepi (DIP_DROP (m-1,p)) + (simplify_stepi (DUP (n-p)) exprs) else if p = 1 then - (DUP n) :: DIP_DROP(m,p) :: exprs + {i=DUP n} :: {i=DIP_DROP(m,p)} :: exprs else let x = n-m in let y = p -x - 1 in let code = - simplify_step (DUP(n-x)) - (simplify_step (DIP_DROP(m,1)) exprs) + simplify_stepi (DUP(n-x)) + (simplify_stepi (DIP_DROP(m,1)) exprs) in let code = if y > 0 then - simplify_step (DIP_DROP(m,y)) code + simplify_stepi (DIP_DROP(m,y)) code else code in let code = @@ -216,6 +240,8 @@ and simplify_step e exprs = after | _ -> e :: exprs +and simplify_stepi i code = simplify_step {i} code + and simplify_steps list tail = let rec iter list_rev tail = match list_rev with diff --git a/tools/liquidity/liquidPeephole.mli b/tools/liquidity/liquidPeephole.mli index 9e6f09b0..06f1fe6a 100644 --- a/tools/liquidity/liquidPeephole.mli +++ b/tools/liquidity/liquidPeephole.mli @@ -7,6 +7,6 @@ (* *) (**************************************************************************) -val simplify : - LiquidTypes.pre_michelson LiquidTypes.contract -> - LiquidTypes.pre_michelson LiquidTypes.contract +open LiquidTypes + +val simplify : noloc_michelson contract -> noloc_michelson contract diff --git a/tools/liquidity/liquidPrinter.ml b/tools/liquidity/liquidPrinter.ml index 13712f04..c89010a2 100644 --- a/tools/liquidity/liquidPrinter.ml +++ b/tools/liquidity/liquidPrinter.ml @@ -122,6 +122,7 @@ module Michelson = struct | Tstring -> Printf.bprintf b "string" | Ttimestamp -> Printf.bprintf b "timestamp" | Tkey -> Printf.bprintf b "key" + | Tkey_hash -> Printf.bprintf b "key_hash" | Tsignature -> Printf.bprintf b "signature" | Ttuple tys -> bprint_type_pairs b indent tys | Tcontract (ty1, ty2) -> @@ -200,6 +201,7 @@ module Michelson = struct match cst with | CString s -> Printf.bprintf b "%S" s | CKey s -> Printf.bprintf b "%S" s + | CKey_hash s -> Printf.bprintf b "%S" s | CSignature s -> Printf.bprintf b "%S" s | CTez s -> Printf.bprintf b "%S" (mic_of_tez s) | CInt n -> Printf.bprintf b "%s" (mic_of_integer n) @@ -321,14 +323,131 @@ module Michelson = struct Printf.bprintf b "\n"; () + let bprint_pre_michelson bprint_arg b = function + | SEQ args -> + Printf.bprintf b "{ "; + List.iter (fun a -> bprint_arg b a; Printf.bprintf b " ; ") args; + Printf.bprintf b " }"; + | DIP (i, a) -> + Printf.bprintf b "D%sP " + (String.concat "" (LiquidMisc.list_init i (fun _ -> "I"))); + bprint_arg b a; + | IF (a1, a2) -> + Printf.bprintf b "IF "; + bprint_arg b a1; + bprint_arg b a2; + | IF_NONE (a1, a2) -> + Printf.bprintf b "IF_NONE "; + bprint_arg b a1; + bprint_arg b a2; + | IF_CONS (a1, a2) -> + Printf.bprintf b "IF_CONS "; + bprint_arg b a1; + bprint_arg b a2; + | IF_LEFT (a1, a2) -> + Printf.bprintf b "IF_LEFT "; + bprint_arg b a1; + bprint_arg b a2; + | LOOP a -> + Printf.bprintf b "LOOP "; + bprint_arg b a; + | LAMBDA (ty1, ty2, a) -> + Printf.bprintf b "LAMBDA "; + bprint_type b "" ty1; + Printf.bprintf b " "; + bprint_type b "" ty2; + bprint_arg b a; + | EXEC -> Printf.bprintf b "EXEC" + | DUP i -> + Printf.bprintf b "D%sP" + (String.concat "" (LiquidMisc.list_init i (fun _ -> "U"))); + | DIP_DROP (i, r) -> + Printf.bprintf b "DIP_DROP (%d, %d)" i r; + | DROP -> Printf.bprintf b "DROP" + | CAR -> Printf.bprintf b "CAR" + | CDR -> Printf.bprintf b "CDR" + | CDAR i -> + Printf.bprintf b "C%sAR " + (String.concat "" (LiquidMisc.list_init i (fun _ -> "D"))); + | CDDR i -> + Printf.bprintf b "C%sDR " + (String.concat "" (LiquidMisc.list_init i (fun _ -> "D"))); + | PUSH (ty, c) -> + Printf.bprintf b "PUSH "; + bprint_type b "" ty; + bprint_const b "" c; + | PAIR -> Printf.bprintf b "PAIR" + | COMPARE -> Printf.bprintf b "COMPARE" + | LE -> Printf.bprintf b "LE" + | LT -> Printf.bprintf b "LT" + | GE -> Printf.bprintf b "GE" + | GT -> Printf.bprintf b "GT" + | NEQ -> Printf.bprintf b "NEQ" + | EQ -> Printf.bprintf b "EQ" + | FAIL -> Printf.bprintf b "FAIL" + | NOW -> Printf.bprintf b "NOW" + | TRANSFER_TOKENS -> Printf.bprintf b "TRANSFER_TOKENS" + | ADD -> Printf.bprintf b "ADD" + | SUB -> Printf.bprintf b "SUB" + | BALANCE -> Printf.bprintf b "BALANCE" + | SWAP -> Printf.bprintf b "SWAP" + | GET -> Printf.bprintf b "GET" + | UPDATE -> Printf.bprintf b "UPDATE" + | SOME -> Printf.bprintf b "SOME" + | CONCAT -> Printf.bprintf b "CONCAT" + | MEM -> Printf.bprintf b "MEM" + | MAP -> Printf.bprintf b "MAP" + | REDUCE -> Printf.bprintf b "REDUCE" + | SELF -> Printf.bprintf b "SELF" + | AMOUNT -> Printf.bprintf b "AMOUNT" + | STEPS_TO_QUOTA -> Printf.bprintf b "STEPS_TO_QUOTA" + | MANAGER -> Printf.bprintf b "MANAGER" + | CREATE_ACCOUNT -> Printf.bprintf b "CREATE_ACCOUNT" + | CREATE_CONTRACT -> Printf.bprintf b "CREATE_CONTRACT" + | H -> Printf.bprintf b "H" + | HASH_KEY -> Printf.bprintf b "HASH_KEY" + | CHECK_SIGNATURE -> Printf.bprintf b "CHECK_SIGNATURE" + | CONS -> Printf.bprintf b "CONS" + | OR -> Printf.bprintf b "OR" + | XOR -> Printf.bprintf b "XOR" + | AND -> Printf.bprintf b "AND" + | NOT -> Printf.bprintf b "NOT" + | INT -> Printf.bprintf b "INT" + | ABS -> Printf.bprintf b "ABS" + | NEG -> Printf.bprintf b "NEG" + | MUL -> Printf.bprintf b "MUL" + | LEFT ty -> + Printf.bprintf b "LEFT"; + bprint_type b "" ty; + | RIGHT ty -> + Printf.bprintf b "RIGHT"; + bprint_type b "" ty; + | EDIV -> Printf.bprintf b "EDIV" + | LSL -> Printf.bprintf b "LSL" + | LSR -> Printf.bprintf b "LSR" + | SOURCE (ty1, ty2) -> + Printf.bprintf b "SOURCE"; + bprint_type b "" ty1; + bprint_type b "" ty2; + | SIZE -> Printf.bprintf b "SIZE" + | DEFAULT_ACCOUNT -> Printf.bprintf b "DEFAULT_ACCOUNT" + | MOD -> Printf.bprintf b "MOD" + | DIV -> Printf.bprintf b "DIV" + + let rec bprint_noloc_michelson b ins= + bprint_pre_michelson bprint_noloc_michelson b ins.i + + let rec bprint_loc_michelson b m = + bprint_pre_michelson bprint_loc_michelson b m.ins + let string_of_type = to_string bprint_type let string_of_code code = to_string bprint_code code let string_of_const = to_string bprint_const let line_of_const = to_string bprint_const_single let string_of_contract cmd = to_string (bprint_contract bprint_code) cmd - - + let string_of_noloc_michelson = to_string (fun b _ -> bprint_noloc_michelson b) + let string_of_loc_michelson = to_string (fun b _ -> bprint_loc_michelson b) end @@ -509,10 +628,14 @@ module Liquid = struct Printf.bprintf b "\n%smatch " indent; bprint_code ~debug b indent2 arg; Printf.bprintf b " with\n"; - List.iter (fun (constr, vars, e) -> - Printf.bprintf b "\n%s| %s (%s) ->\n" indent2 constr - (String.concat ", " vars); - bprint_code ~debug b indent4 e; + List.iter (function + | CConstr (constr, vars), e -> + Printf.bprintf b "\n%s| %s (%s) ->\n" indent2 constr + (String.concat ", " vars); + bprint_code ~debug b indent4 e; + | CAny, e -> + Printf.bprintf b "\n%s| _ ->\n" indent2; + bprint_code ~debug b indent4 e; ) cases; () diff --git a/tools/liquidity/liquidPrinter.mli b/tools/liquidity/liquidPrinter.mli index ef3120a9..4250d620 100644 --- a/tools/liquidity/liquidPrinter.mli +++ b/tools/liquidity/liquidPrinter.mli @@ -41,7 +41,8 @@ module Michelson : sig val string_of_contract : LiquidTypes.michelson_exp LiquidTypes.contract -> string val string_of_code : LiquidTypes.michelson_exp -> string - - end + val string_of_noloc_michelson : LiquidTypes.noloc_michelson -> string + val string_of_loc_michelson : LiquidTypes.loc_michelson -> string +end val string_of_node : LiquidTypes.node -> string diff --git a/tools/liquidity/liquidSimplify.ml b/tools/liquidity/liquidSimplify.ml index e0a74bf3..b4576a07 100644 --- a/tools/liquidity/liquidSimplify.ml +++ b/tools/liquidity/liquidSimplify.ml @@ -60,8 +60,7 @@ let compute code to_inline = | MatchVariant(arg, loc, cases) -> let arg = iter arg in - let cases = List.map (fun (constr, vars, e) -> - constr, vars, iter e) cases in + let cases = List.map (fun (pat, e) -> pat, iter e) cases in { exp with desc = MatchVariant(arg,loc, cases) } | Loop(name, loc, body, arg) -> diff --git a/tools/liquidity/liquidToOCaml.ml b/tools/liquidity/liquidToOCaml.ml index da038a10..249463b9 100644 --- a/tools/liquidity/liquidToOCaml.ml +++ b/tools/liquidity/liquidToOCaml.ml @@ -8,16 +8,14 @@ (**************************************************************************) (* The version that will be required to compile the generated files. *) -let output_version = "0.1" +let output_version = "0.11" (* +type storage = ... let contract (parameter : timestamp) - (storage: (string * timestamp * (tez * tez) * - ( (unit,unit) contract * - (unit, unit) contract * - (unit, unit) contract)) ) - [%return : unit] = + (storage: storage ) + : unit * storage = ... *) @@ -42,6 +40,7 @@ let rec convert_type ty = | Tnat -> typ_constr "nat" [] | Tbool -> typ_constr "bool" [] | Tkey -> typ_constr "key" [] + | Tkey_hash -> typ_constr "key_hash" [] | Tsignature -> typ_constr "signature" [] | Tstring -> typ_constr "string" [] | Ttuple args -> Typ.tuple (List.map convert_type args) @@ -80,6 +79,8 @@ let rec convert_const expr = (convert_type Ttez) | CKey n -> Exp.constraint_ (convert_const (CString n)) (convert_type Tkey) + | CKey_hash n -> Exp.constraint_ (convert_const (CString n)) + (convert_type Tkey_hash) | CSignature n -> Exp.constraint_ (convert_const (CString n)) (convert_type Tsignature) @@ -254,22 +255,25 @@ let rec convert_code expr = | MatchVariant (arg, _loc, cases) -> Exp.match_ (convert_code arg) - (List.map (fun (constr, var_args, exp) -> - Exp.case - (Pat.construct (lid constr) - (match var_args with - | [] -> None - | [var_arg] -> - Some (Pat.var (loc var_arg)) - | var_args -> - Some - (Pat.tuple (List.map - (fun var_arg -> - Pat.var (loc var_arg) - ) var_args)) - )) - (convert_code exp) - ) cases) + (List.map (function + | CAny, exp -> + Exp.case (Pat.any ()) (convert_code exp) + | CConstr (constr, var_args), exp -> + Exp.case + (Pat.construct (lid constr) + (match var_args with + | [] -> None + | [var_arg] -> + Some (Pat.var (loc var_arg)) + | var_args -> + Some + (Pat.tuple (List.map + (fun var_arg -> + Pat.var (loc var_arg) + ) var_args)) + )) + (convert_code exp) + ) cases) | Constructor (_loc, Constr id, { desc = Const (Tunit, CUnit) } ) -> Exp.construct (lid id) None @@ -304,6 +308,12 @@ let structure_of_contract contract = Str.eval (Exp.constant (Const.float output_version)) ]); + + Str.type_ Recursive [ + Type.mk ~manifest:(convert_type contract.storage) + { txt = "storage"; loc = !default_loc } + ]; + Str.extension ( { txt = "entry"; loc = !default_loc }, PStr [ Str.value Nonrecursive @@ -317,14 +327,12 @@ let structure_of_contract contract = (Exp.fun_ Nolabel None (Pat.constraint_ (Pat.var (loc "storage")) - (convert_type contract.storage) - ) - (Exp.fun_ Nolabel None - (Pat.extension - (loc "return", - PTyp (convert_type contract.return)) + (typ_constr "storage" []) ) - code))) + (Exp.constraint_ + code (Typ.tuple [convert_type contract.return; + typ_constr "storage" []])) + )) ] ])] diff --git a/tools/liquidity/liquidTypes.ml b/tools/liquidity/liquidTypes.ml index 3b5dd96c..e49efef5 100644 --- a/tools/liquidity/liquidTypes.ml +++ b/tools/liquidity/liquidTypes.ml @@ -37,7 +37,10 @@ type const = | CLeft of const | CRight of const -and datatype = + | CKey_hash of string + + and datatype = + (* michelson *) | Tunit | Tbool | Tint @@ -46,6 +49,7 @@ and datatype = | Tstring | Ttimestamp | Tkey + | Tkey_hash | Tsignature | Ttuple of datatype list @@ -58,8 +62,9 @@ and datatype = | Tcontract of datatype * datatype | Tor of datatype * datatype | Tlambda of datatype * datatype - | Tclosure of (datatype * datatype) * datatype + (* liquidity extensions *) + | Tclosure of (datatype * datatype) * datatype | Tfail | Ttype of string * datatype @@ -73,7 +78,7 @@ type 'exp contract = { type location = { loc_file : string; - loc_pos : ( (int * int) * (int*int) ) option; + loc_pos : ((int * int) * (int * int)) option; } type error = { err_loc: location; err_msg: string } @@ -148,6 +153,7 @@ type primitive = | Prim_create_account | Prim_create_contract | Prim_hash + | Prim_hash_key | Prim_check | Prim_default_account @@ -168,6 +174,13 @@ type primitive = let primitive_of_string = Hashtbl.create 101 let string_of_primitive = Hashtbl.create 101 + + +(* Some primitives should be kept internal: +* get and set +* get_last and set_last +* tuple +*) let () = List.iter (fun (n,p) -> Hashtbl.add primitive_of_string n p; @@ -176,17 +189,20 @@ let () = [ "get", Prim_tuple_get; "get_last", Prim_tuple_get_last; - "Array.get", Prim_tuple_get; "set_last", Prim_tuple_set_last; "set", Prim_tuple_set; - "Array.set", Prim_tuple_set; "tuple", Prim_tuple; + + "Array.get", Prim_tuple_get; + "Array.set", Prim_tuple_set; + "Current.fail", Prim_fail; "Current.contract", Prim_self; "Current.balance", Prim_balance; "Current.time", Prim_now; "Current.amount", Prim_amount; "Current.gas", Prim_gas; + "Left", Prim_Left; "Right", Prim_Right; "Source", Prim_Source; @@ -207,11 +223,13 @@ let () = "Map.mem", Prim_map_mem; "Map.reduce", Prim_map_reduce; "Map.map", Prim_map_map; + "Map.size", Prim_map_size; "Set.update", Prim_set_update; "Set.mem", Prim_set_mem; "Set.reduce", Prim_set_reduce; "Set.map", Prim_set_map; + "Set.size", Prim_set_size; "Some", Prim_Some; "@", Prim_concat; @@ -219,16 +237,17 @@ let () = "List.reduce", Prim_list_reduce; "List.map", Prim_list_map; "List.rev", Prim_list_rev; + "List.size", Prim_list_size; "Contract.manager", Prim_manager; - "Account.create", Prim_create_account; "Contract.create", Prim_create_contract; + + "Account.create", Prim_create_account; + "Account.default", Prim_default_account; + "Crypto.hash", Prim_hash; + "Crypto.hash_key", Prim_hash_key; "Crypto.check", Prim_check; - "Account.default", Prim_default_account; - "List.size", Prim_list_size; - "Set.size", Prim_set_size; - "Map.size", Prim_map_size; "::", Prim_Cons; "or", Prim_or; @@ -281,6 +300,10 @@ type constructor = | Right of datatype | Source of datatype * datatype +type pattern = + | CConstr of string * string list + | CAny + type 'ty exp = { desc : 'ty exp_desc; ty : 'ty; @@ -335,7 +358,7 @@ type 'ty exp = { | MatchVariant of 'ty exp * location - * (string * string list * 'ty exp) list + * (pattern * 'ty exp) list type syntax_exp = unit exp type typed_exp = datatype exp @@ -349,16 +372,16 @@ type michelson_exp = | M_INS_CST of string * datatype * const | M_INS_EXP of string * datatype list * michelson_exp list -type pre_michelson = - | SEQ of pre_michelson list - | DIP of int * pre_michelson - | IF of pre_michelson * pre_michelson - | IF_NONE of pre_michelson * pre_michelson - | IF_CONS of pre_michelson * pre_michelson - | IF_LEFT of pre_michelson * pre_michelson - | LOOP of pre_michelson +type 'a pre_michelson = + | SEQ of 'a list + | DIP of int * 'a + | IF of 'a * 'a + | IF_NONE of 'a * 'a + | IF_CONS of 'a * 'a + | IF_LEFT of 'a * 'a + | LOOP of 'a - | LAMBDA of datatype * datatype * pre_michelson + | LAMBDA of datatype * datatype * 'a | EXEC | DUP of int @@ -394,6 +417,7 @@ type pre_michelson = | CREATE_ACCOUNT | CREATE_CONTRACT | H + | HASH_KEY | CHECK_SIGNATURE | CONS @@ -423,7 +447,18 @@ type pre_michelson = | MOD | DIV +type noloc_michelson = { i : noloc_michelson pre_michelson } + +type loc_michelson = { + loc : location; + ins : loc_michelson pre_michelson; +} + +let mic ins = ins +let mic_loc loc ins = { loc; ins } + type type_kind = + | Type_alias | Type_record of datatype list * int StringMap.t | Type_variant of (string @@ -473,13 +508,14 @@ type 'a typecheck_env = { (* decompilation *) type node = { - num : int; - mutable kind : node_kind; - mutable args : node list; (* dependencies *) + num : int; + loc : location; + mutable kind : node_kind; + mutable args : node list; (* dependencies *) - mutable next : node option; - mutable prevs : node list; - } + mutable next : node option; + mutable prevs : node list; +} and node_kind = | N_UNKNOWN of string @@ -522,3 +558,4 @@ type node_exp = node * node type warning = | Unused of string + | UnusedMatched of string diff --git a/tools/liquidity/liquidUntype.ml b/tools/liquidity/liquidUntype.ml index d596016c..b3f93dd8 100644 --- a/tools/liquidity/liquidUntype.ml +++ b/tools/liquidity/liquidUntype.ml @@ -164,16 +164,16 @@ let rec untype (env : env) (code : typed_exp) = | MatchVariant (arg, loc, [ - "Left", [left_var], left_arg; - "Right", [right_var], right_arg; + CConstr ("Left", [left_var]), left_arg; + CConstr ("Right", [right_var]), right_arg; ]) -> let arg = untype env arg in let left_var, left_arg = untype_case env left_var left_arg in let right_var, right_arg = untype_case env right_var right_arg in MatchVariant (arg, loc, [ - "Left", [left_var], left_arg; - "Right", [right_var], right_arg; + CConstr ("Left", [left_var]), left_arg; + CConstr ("Right", [right_var]), right_arg; ]) | Record (_, _) diff --git a/tools/liquidity/liquidVersion.ml b/tools/liquidity/liquidVersion.ml new file mode 100644 index 00000000..55b717bd --- /dev/null +++ b/tools/liquidity/liquidVersion.ml @@ -0,0 +1,11 @@ +(**************************************************************************) +(* *) +(* Copyright (c) 2017 . *) +(* Fabrice Le Fessant, OCamlPro SAS *) +(* *) +(* All rights reserved. No warranty, explicit or implicit, provided. *) +(* *) +(**************************************************************************) + +let commit = "" +let en_date = "" diff --git a/tools/liquidity/ocaml/liquidOCamlCompile.ml b/tools/liquidity/ocaml/liquidOCamlCompile.ml new file mode 100644 index 00000000..6f443f77 --- /dev/null +++ b/tools/liquidity/ocaml/liquidOCamlCompile.ml @@ -0,0 +1,119 @@ +(**************************************************************************) +(* *) +(* OCaml *) +(* *) +(* Xavier Leroy, projet Cristal, INRIA Rocquencourt *) +(* *) +(* Copyright 2002 Institut National de Recherche en Informatique et *) +(* en Automatique. *) +(* *) +(* All rights reserved. This file is distributed under the terms of *) +(* the GNU Lesser General Public License version 2.1, with the *) +(* special exception on linking described in the file LICENSE. *) +(* *) +(**************************************************************************) + +(* Also a patch to add "LiquidityEnv" to open_modules *) +module Pparse = LiquidOCamlPparse + +(* The batch compiler *) + +open Misc +open Format +open Typedtree +open Compenv + +(* Compile a .mli file *) + +(* Keep in sync with the copy in optcompile.ml *) + +let tool_name = "ocamlc" + +let interface ppf sourcefile outputprefix = + Compmisc.init_path false; + let modulename = module_of_filename ppf sourcefile outputprefix in + Env.set_unit_name modulename; + let initial_env = Compmisc.initial_env () in + let ast = Pparse.parse_interface ~tool_name ppf sourcefile in + + if !Clflags.dump_parsetree then fprintf ppf "%a@." Printast.interface ast; + if !Clflags.dump_source then fprintf ppf "%a@." Pprintast.signature ast; + Timings.(time_call (Typing sourcefile)) (fun () -> + let tsg = Typemod.type_interface sourcefile initial_env ast in + if !Clflags.dump_typedtree then fprintf ppf "%a@." Printtyped.interface tsg; + let sg = tsg.sig_type in + if !Clflags.print_types then + Printtyp.wrap_printing_env initial_env (fun () -> + fprintf std_formatter "%a@." + Printtyp.signature (Typemod.simplify_signature sg)); + ignore (Includemod.signatures initial_env sg sg); + Typecore.force_delayed_checks (); + Warnings.check_fatal (); + if not !Clflags.print_types then begin + let deprecated = Builtin_attributes.deprecated_of_sig ast in + let sg = + Env.save_signature ~deprecated sg modulename (outputprefix ^ ".cmi") + in + Typemod.save_signature modulename tsg outputprefix sourcefile + initial_env sg ; + end + ) + +(* Compile a .ml file *) + +let print_if ppf flag printer arg = + if !flag then fprintf ppf "%a@." printer arg; + arg + +let (++) x f = f x + +let implementation ppf sourcefile outputprefix = + Clflags.open_modules := "LiquidityEnv" :: !Clflags.open_modules; + Compmisc.init_path false; + let modulename = module_of_filename ppf sourcefile outputprefix in + Env.set_unit_name modulename; + let env = Compmisc.initial_env() in + try + let (typedtree, coercion) = + Pparse.parse_implementation ~tool_name ppf sourcefile + ++ print_if ppf Clflags.dump_parsetree Printast.implementation + ++ print_if ppf Clflags.dump_source Pprintast.structure + ++ Timings.(time (Typing sourcefile)) + (Typemod.type_implementation sourcefile outputprefix modulename env) + ++ print_if ppf Clflags.dump_typedtree + Printtyped.implementation_with_coercion + in + if !Clflags.print_types then begin + Warnings.check_fatal (); + Stypes.dump (Some (outputprefix ^ ".annot")) + end else begin + let bytecode, required_globals = + (typedtree, coercion) + ++ Timings.(time (Transl sourcefile)) + (Translmod.transl_implementation modulename) + ++ Timings.(accumulate_time (Generate sourcefile)) + (fun { Lambda.code = lambda; required_globals } -> + print_if ppf Clflags.dump_rawlambda Printlambda.lambda lambda + ++ Simplif.simplify_lambda sourcefile + ++ print_if ppf Clflags.dump_lambda Printlambda.lambda + ++ Bytegen.compile_implementation modulename + ++ print_if ppf Clflags.dump_instr Printinstr.instrlist + ++ fun bytecode -> bytecode, required_globals) + in + let objfile = outputprefix ^ ".cmo" in + let oc = open_out_bin objfile in + try + bytecode + ++ Timings.(accumulate_time (Generate sourcefile)) + (Emitcode.to_file oc modulename objfile ~required_globals); + Warnings.check_fatal (); + close_out oc; + Stypes.dump (Some (outputprefix ^ ".annot")) + with x -> + close_out oc; + remove_file objfile; + raise x + end + with x -> + Stypes.dump (Some (outputprefix ^ ".annot")); + raise x diff --git a/tools/liquidity/ocaml/liquidOCamlMain.ml b/tools/liquidity/ocaml/liquidOCamlMain.ml new file mode 100644 index 00000000..c7e04b96 --- /dev/null +++ b/tools/liquidity/ocaml/liquidOCamlMain.ml @@ -0,0 +1,206 @@ +(**************************************************************************) +(* *) +(* OCaml *) +(* *) +(* Xavier Leroy, projet Cristal, INRIA Rocquencourt *) +(* *) +(* Copyright 1996 Institut National de Recherche en Informatique et *) +(* en Automatique. *) +(* *) +(* All rights reserved. This file is distributed under the terms of *) +(* the GNU Lesser General Public License version 2.1, with the *) +(* special exception on linking described in the file LICENSE. *) +(* *) +(**************************************************************************) + +let () = LiquidOCamlTranslate.init () + +module Compile = LiquidOCamlCompile + +open Clflags +open Compenv + +let usage = "Usage: ocamlc \nOptions are:" + +(* Error messages to standard error formatter *) +let ppf = Format.err_formatter + +let show_config () = + Config.print_config stdout; + exit 0; +;; + +module Options = Main_args.Make_bytecomp_options (struct + let set r () = r := true + let unset r () = r := false + let _a = set make_archive + let _absname = set Location.absname + let _annot = set annotations + let _binannot = set binary_annotations + let _c = set compile_only + let _cc s = c_compiler := Some s + let _cclib s = Compenv.defer (ProcessObjects (Misc.rev_split_words s)) + let _ccopt s = first_ccopts := s :: !first_ccopts + let _compat_32 = set bytecode_compatible_32 + let _config = show_config + let _custom = set custom_runtime + let _no_check_prims = set no_check_prims + let _dllib s = defer (ProcessDLLs (Misc.rev_split_words s)) + let _dllpath s = dllpaths := !dllpaths @ [s] + let _for_pack s = for_package := Some s + let _g = set debug + let _i () = print_types := true; compile_only := true + let _I s = include_dirs := s :: !include_dirs + let _impl = impl + let _intf = intf + let _intf_suffix s = Config.interface_suffix := s + let _keep_docs = set keep_docs + let _no_keep_docs = unset keep_docs + let _keep_locs = set keep_locs + let _no_keep_locs = unset keep_locs + let _labels = unset classic + let _linkall = set link_everything + let _make_runtime () = + custom_runtime := true; make_runtime := true; link_everything := true + let _alias_deps = unset transparent_modules + let _no_alias_deps = set transparent_modules + let _app_funct = set applicative_functors + let _no_app_funct = unset applicative_functors + let _noassert = set noassert + let _nolabels = set classic + let _noautolink = set no_auto_link + let _nostdlib = set no_std_include + let _o s = output_name := Some s + let _opaque = set opaque + let _open s = open_modules := s :: !open_modules + let _output_obj () = output_c_object := true; custom_runtime := true + let _output_complete_obj () = + output_c_object := true; + output_complete_object := true; + custom_runtime := true + let _pack = set make_package + let _pp s = preprocessor := Some s + let _ppx s = first_ppx := s :: !first_ppx + let _plugin p = Compplugin.load p + let _principal = set principal + let _no_principal = unset principal + let _rectypes = set recursive_types + let _no_rectypes = unset recursive_types + let _runtime_variant s = runtime_variant := s + let _safe_string = unset unsafe_string + let _short_paths = unset real_paths + let _strict_sequence = set strict_sequence + let _no_strict_sequence = unset strict_sequence + let _strict_formats = set strict_formats + let _no_strict_formats = unset strict_formats + let _thread = set use_threads + let _vmthread = set use_vmthreads + let _unboxed_types = set unboxed_types + let _no_unboxed_types = unset unboxed_types + let _unsafe = set fast + let _unsafe_string = set unsafe_string + let _use_prims s = use_prims := s + let _use_runtime s = use_runtime := s + let _v () = print_version_and_library "compiler" + let _version = print_version_string + let _vnum = print_version_string + let _w = (Warnings.parse_options false) + let _warn_error = (Warnings.parse_options true) + let _warn_help = Warnings.help_warnings + let _color option = + begin match parse_color_setting option with + | None -> () + | Some setting -> color := Some setting + end + let _where = print_standard_library + let _verbose = set verbose + let _nopervasives = set nopervasives + let _dsource = set dump_source + let _dparsetree = set dump_parsetree + let _dtypedtree = set dump_typedtree + let _drawlambda = set dump_rawlambda + let _dlambda = set dump_lambda + let _dinstr = set dump_instr + let _dtimings = set print_timings + + let _args = Arg.read_arg + let _args0 = Arg.read_arg0 + + let anonymous = anonymous +end) + +let main () = + Clflags.add_arguments __LOC__ Options.list; + try + readenv ppf Before_args; + Clflags.parse_arguments anonymous usage; + Compmisc.read_color_env ppf; + begin try + Compenv.process_deferred_actions + (ppf, + Compile.implementation, + Compile.interface, + ".cmo", + ".cma"); + with Arg.Bad msg -> + begin + prerr_endline msg; + Clflags.print_arguments usage; + exit 2 + end + end; + readenv ppf Before_link; + if + List.length (List.filter (fun x -> !x) + [make_archive;make_package;compile_only;output_c_object]) + > 1 + then + if !print_types then + fatal "Option -i is incompatible with -pack, -a, -output-obj" + else + fatal "Please specify at most one of -pack, -a, -c, -output-obj"; + if !make_archive then begin + Compmisc.init_path false; + + Bytelibrarian.create_archive ppf + (Compenv.get_objfiles ~with_ocamlparam:false) + (extract_output !output_name); + Warnings.check_fatal (); + end + else if !make_package then begin + Compmisc.init_path false; + let extracted_output = extract_output !output_name in + let revd = get_objfiles ~with_ocamlparam:false in + Bytepackager.package_files ppf (Compmisc.initial_env ()) + revd (extracted_output); + Warnings.check_fatal (); + end + else if not !compile_only && !objfiles <> [] then begin + let target = + if !output_c_object then + let s = extract_output !output_name in + if (Filename.check_suffix s Config.ext_obj + || Filename.check_suffix s Config.ext_dll + || Filename.check_suffix s ".c") + then s + else + fatal + (Printf.sprintf + "The extension of the output file must be .c, %s or %s" + Config.ext_obj Config.ext_dll + ) + else + default_output !output_name + in + Compmisc.init_path false; + Bytelink.link ppf (get_objfiles ~with_ocamlparam:true) target; + Warnings.check_fatal (); + end; + with x -> + Location.report_exception ppf x; + exit 2 + +let _ = + Timings.(time All) main (); + if !Clflags.print_timings then Timings.print Format.std_formatter; + exit 0 diff --git a/tools/liquidity/ocaml/liquidOCamlPparse.ml b/tools/liquidity/ocaml/liquidOCamlPparse.ml new file mode 100644 index 00000000..30e28c86 --- /dev/null +++ b/tools/liquidity/ocaml/liquidOCamlPparse.ml @@ -0,0 +1,246 @@ +(**************************************************************************) +(* *) +(* OCaml *) +(* *) +(* Daniel de Rauglaudre, projet Cristal, INRIA Rocquencourt *) +(* *) +(* Copyright 2002 Institut National de Recherche en Informatique et *) +(* en Automatique. *) +(* *) +(* All rights reserved. This file is distributed under the terms of *) +(* the GNU Lesser General Public License version 2.1, with the *) +(* special exception on linking described in the file LICENSE. *) +(* *) +(**************************************************************************) + +module Parse = LiquidOCamlParse +module Parser = LiquidOCamlParser + + +open Format + +type error = + | CannotRun of string + | WrongMagic of string + +exception Error of error + +(* Optionally preprocess a source file *) + +let call_external_preprocessor sourcefile pp = + let tmpfile = Filename.temp_file "ocamlpp" "" in + let comm = Printf.sprintf "%s %s > %s" + pp (Filename.quote sourcefile) tmpfile + in + if Ccomp.command comm <> 0 then begin + Misc.remove_file tmpfile; + raise (Error (CannotRun comm)); + end; + tmpfile + +let preprocess sourcefile = + match !Clflags.preprocessor with + None -> sourcefile + | Some pp -> + Timings.(time (Dash_pp sourcefile)) + (call_external_preprocessor sourcefile) pp + + +let remove_preprocessed inputfile = + match !Clflags.preprocessor with + None -> () + | Some _ -> Misc.remove_file inputfile + +type 'a ast_kind = +| Structure : Parsetree.structure ast_kind +| Signature : Parsetree.signature ast_kind + +let magic_of_kind : type a . a ast_kind -> string = function + | Structure -> Config.ast_impl_magic_number + | Signature -> Config.ast_intf_magic_number + +(* Note: some of the functions here should go to Ast_mapper instead, + which would encapsulate the "binary AST" protocol. *) + +let write_ast (type a) (kind : a ast_kind) fn (ast : a) = + let oc = open_out_bin fn in + output_string oc (magic_of_kind kind); + output_value oc (!Location.input_name : string); + output_value oc (ast : a); + close_out oc + +let apply_rewriter kind fn_in ppx = + let magic = magic_of_kind kind in + let fn_out = Filename.temp_file "camlppx" "" in + let comm = + Printf.sprintf "%s %s %s" ppx (Filename.quote fn_in) (Filename.quote fn_out) + in + let ok = Ccomp.command comm = 0 in + Misc.remove_file fn_in; + if not ok then begin + Misc.remove_file fn_out; + raise (Error (CannotRun comm)); + end; + if not (Sys.file_exists fn_out) then + raise (Error (WrongMagic comm)); + (* check magic before passing to the next ppx *) + let ic = open_in_bin fn_out in + let buffer = + try really_input_string ic (String.length magic) with End_of_file -> "" in + close_in ic; + if buffer <> magic then begin + Misc.remove_file fn_out; + raise (Error (WrongMagic comm)); + end; + fn_out + +let read_ast (type a) (kind : a ast_kind) fn : a = + let ic = open_in_bin fn in + try + let magic = magic_of_kind kind in + let buffer = really_input_string ic (String.length magic) in + assert(buffer = magic); (* already checked by apply_rewriter *) + Location.input_name := (input_value ic : string); + let ast = (input_value ic : a) in + close_in ic; + Misc.remove_file fn; + ast + with exn -> + close_in ic; + Misc.remove_file fn; + raise exn + +let rewrite kind ppxs ast = + let fn = Filename.temp_file "camlppx" "" in + write_ast kind fn ast; + let fn = List.fold_left (apply_rewriter kind) fn (List.rev ppxs) in + read_ast kind fn + +let apply_rewriters_str ?(restore = true) ~tool_name ast = + match !Clflags.all_ppx with + | [] -> ast + | ppxs -> + ast + |> Ast_mapper.add_ppx_context_str ~tool_name + |> rewrite Structure ppxs + |> Ast_mapper.drop_ppx_context_str ~restore + +let apply_rewriters_sig ?(restore = true) ~tool_name ast = + match !Clflags.all_ppx with + | [] -> ast + | ppxs -> + ast + |> Ast_mapper.add_ppx_context_sig ~tool_name + |> rewrite Signature ppxs + |> Ast_mapper.drop_ppx_context_sig ~restore + +let apply_rewriters ?restore ~tool_name + (type a) (kind : a ast_kind) (ast : a) : a = + match kind with + | Structure -> + apply_rewriters_str ?restore ~tool_name ast + | Signature -> + apply_rewriters_sig ?restore ~tool_name ast + +(* Parse a file or get a dumped syntax tree from it *) + +exception Outdated_version + +let open_and_check_magic inputfile ast_magic = + let ic = open_in_bin inputfile in + let is_ast_file = + try + let buffer = really_input_string ic (String.length ast_magic) in + if buffer = ast_magic then true + else if String.sub buffer 0 9 = String.sub ast_magic 0 9 then + raise Outdated_version + else false + with + Outdated_version -> + Misc.fatal_error "OCaml and preprocessor have incompatible versions" + | _ -> false + in + (ic, is_ast_file) + +let parse (type a) (kind : a ast_kind) lexbuf : a = + match kind with + | Structure -> Parse.implementation lexbuf + | Signature -> Parse.interface lexbuf + +let file_aux ppf ~tool_name inputfile (type a) parse_fun invariant_fun + (kind : a ast_kind) = + let ast_magic = magic_of_kind kind in + let source_file = !Location.input_name in + let (ic, is_ast_file) = open_and_check_magic inputfile ast_magic in + let ast = + try + if is_ast_file then begin + if !Clflags.fast then + (* FIXME make this a proper warning *) + fprintf ppf "@[Warning: %s@]@." + "option -unsafe used with a preprocessor returning a syntax tree"; + Location.input_name := (input_value ic : string); + (input_value ic : a) + end else begin + seek_in ic 0; + Location.input_name := inputfile; + let lexbuf = Lexing.from_channel ic in + Location.init lexbuf inputfile; + Timings.(time_call (Parser source_file)) (fun () -> + parse_fun lexbuf) + end + with x -> close_in ic; raise x + in + close_in ic; + let ast = + Timings.(time_call (Dash_ppx source_file)) (fun () -> + apply_rewriters ~restore:false ~tool_name kind ast) in + if is_ast_file || !Clflags.all_ppx <> [] then invariant_fun ast; + ast + +let file ppf ~tool_name inputfile parse_fun ast_kind = + file_aux ppf ~tool_name inputfile parse_fun ignore ast_kind + +let report_error ppf = function + | CannotRun cmd -> + fprintf ppf "Error while running external preprocessor@.\ + Command line: %s@." cmd + | WrongMagic cmd -> + fprintf ppf "External preprocessor does not produce a valid file@.\ + Command line: %s@." cmd + +let () = + Location.register_error_of_exn + (function + | Error err -> Some (Location.error_of_printer_file report_error err) + | _ -> None + ) + +let parse_file ~tool_name invariant_fun apply_hooks kind ppf sourcefile = + Location.input_name := sourcefile; + let inputfile = preprocess sourcefile in + let ast = + try file_aux ppf ~tool_name inputfile (parse kind) invariant_fun kind + with exn -> + remove_preprocessed inputfile; + raise exn + in + remove_preprocessed inputfile; + let ast = apply_hooks { Misc.sourcefile } ast in + ast + +module ImplementationHooks = Misc.MakeHooks(struct + type t = Parsetree.structure + end) +module InterfaceHooks = Misc.MakeHooks(struct + type t = Parsetree.signature + end) + +let parse_implementation ppf ~tool_name sourcefile = + Timings.(time_call (Parsing sourcefile)) (fun () -> + parse_file ~tool_name Ast_invariants.structure + ImplementationHooks.apply_hooks Structure ppf sourcefile) +let parse_interface ppf ~tool_name sourcefile = + Timings.(time_call (Parsing sourcefile)) (fun () -> + parse_file ~tool_name Ast_invariants.signature + InterfaceHooks.apply_hooks Signature ppf sourcefile) diff --git a/tools/liquidity/ocaml/liquidOCamlPrinter.ml b/tools/liquidity/ocaml/liquidOCamlPrinter.ml index 710b8052..994d8b60 100644 --- a/tools/liquidity/ocaml/liquidOCamlPrinter.ml +++ b/tools/liquidity/ocaml/liquidOCamlPrinter.ml @@ -1145,6 +1145,18 @@ and binding ctxt f {pvb_pat=p; pvb_expr=x; _} = let rec pp_print_pexp_function f x = if x.pexp_attributes <> [] then pp f "=@;%a" (expression ctxt) x else match x.pexp_desc with + | Pexp_fun (label, eo, p, + { pexp_desc = Pexp_constraint (e, rty) }) -> + if label=Nolabel then + pp f "%a@ : %a@ %a" + (simple_pattern ctxt) p + (core_type ctxt) rty + pp_print_pexp_function e + else + pp f "%a@ : %a@ %a" + (label_exp ctxt) (label,eo,p) + (core_type ctxt) rty + pp_print_pexp_function e | Pexp_fun (label, eo, p, e) -> if label=Nolabel then pp f "%a@ %a" (simple_pattern ctxt) p pp_print_pexp_function e diff --git a/tools/liquidity/ocaml/liquidOCamlTranslate.ml b/tools/liquidity/ocaml/liquidOCamlTranslate.ml new file mode 100644 index 00000000..c276ead3 --- /dev/null +++ b/tools/liquidity/ocaml/liquidOCamlTranslate.ml @@ -0,0 +1,143 @@ +(**************************************************************************) +(* *) +(* Copyright (c) 2017 . *) +(* Fabrice Le Fessant, OCamlPro SAS *) +(* *) +(* All rights reserved. No warranty, explicit or implicit, provided. *) +(* *) +(**************************************************************************) + +let clean_ast = + let open Asttypes in + let open Longident in + let open Parsetree in + let open Ast_mapper in + let open Ast_helper in + let lident ~loc s = { txt = Longident.parse s; loc } in + let exp_ident ~loc s = + Exp.ident ~loc (lident ~loc s) in + let exp_unit ~loc = Exp.construct ~loc { txt = Lident "()"; loc } None in + let exp_string ~loc s = Exp.constant ~loc (Pconst_string (s,None)) in + { + default_mapper with + structure_item = (fun mapper item -> + match item with + | { pstr_desc = + Pstr_extension + (({ Asttypes.txt = "version" }, + PStr [{ pstr_desc = Pstr_eval (exp,[])}]),[]) + } -> + Str.eval (Exp.constant (Const.int 0)) + | { pstr_desc = + Pstr_extension + (({ Asttypes.txt = "entry" }, + PStr [entry]),[]) + } -> + mapper.structure_item mapper entry + | _ -> + default_mapper.structure_item mapper item + ); + expr = (fun mapper expr -> + let loc = expr.pexp_loc in + match expr.pexp_desc with + | Pexp_constant ( + Pconst_integer (s, Some 'p') + | Pconst_integer (s, None) + ) + -> + Exp.apply ~loc (exp_ident ~loc "Int.of_string") + [Nolabel, exp_string ~loc s] + + | Pexp_constant (Pconst_integer (s, Some '\231')) + -> + Exp.apply ~loc (exp_ident ~loc "Tez.of_string") + [Nolabel, exp_string ~loc s] + + | Pexp_constant ( + Pconst_float (s, Some '\231') + ) + -> + Exp.apply ~loc (exp_ident ~loc "Tez.of_string") + [Nolabel, exp_string ~loc s] + + | Pexp_construct ({ txt = Lident "Map" }, None) + -> + Exp.apply ~loc (exp_ident ~loc "Map.empty") [Nolabel, exp_unit ~loc] + + | Pexp_construct ( + { txt = Lident "Map" }, Some list + ) + -> + let list = default_mapper.expr mapper list in + Exp.apply ~loc (exp_ident ~loc "Map.make") [Nolabel, list] + + + | Pexp_construct ( + { txt = Lident "Set" }, None + ) + -> + Exp.apply ~loc (exp_ident ~loc "Set.empty") [Nolabel, exp_unit ~loc] + + | Pexp_construct ( + { txt = Lident "Set" }, Some list + ) + -> + let list = default_mapper.expr mapper list in + Exp.apply ~loc (exp_ident ~loc "Set.make") [Nolabel, list] + + + | Pexp_construct ( + { txt = Lident "Source" }, None + ) + -> + Exp.apply ~loc (exp_ident ~loc "Contract.source") + [Nolabel, exp_unit ~loc] + + | Pexp_setfield (record, label1, value) -> + let value = default_mapper.expr mapper value in + begin + match record.pexp_desc with + | Pexp_field (record, label2) -> + let record = default_mapper.expr mapper record in + let id = "record#" in + Exp.let_ + ~loc Nonrecursive + [Vb.mk ~loc (Pat.var ~loc { txt = id; loc }) record] + (Exp.record + ~loc + [label2, + Exp.record + ~loc [ + label1, value + ] + (Some (Exp.field ~loc (Exp.ident ~loc + { txt = Lident id; loc}) + label2)) + ] + (Some (Exp.ident ~loc { txt = Lident id; loc})) + ) + | _ -> + let record = default_mapper.expr mapper record in + Exp.record ~loc [label1, value] (Some record) + end + + | _ -> default_mapper.expr mapper expr + ); + (* `String of int * string` is compiled as `String of (int * string)` *) + constructor_declaration = (fun mapper pcd -> + match pcd.pcd_args with + | Pcstr_tuple [] + | Pcstr_tuple [_] -> pcd + | Pcstr_tuple list -> { pcd with pcd_args = + Pcstr_tuple [Typ.tuple list] } + | _ -> pcd + ); + } + + +let init () = + let open Ast_mapper in + LiquidOCamlPparse.ImplementationHooks.add_hook + "liquid" (fun hook_info ast -> + clean_ast.structure clean_ast ast + ) diff --git a/tools/liquidity/with-tezos/liquidFromTezos.ml b/tools/liquidity/with-tezos/liquidFromTezos.ml index de981d98..e86948c4 100644 --- a/tools/liquidity/with-tezos/liquidFromTezos.ml +++ b/tools/liquidity/with-tezos/liquidFromTezos.ml @@ -64,6 +64,7 @@ let rec convert_type expr = | Script_repr.Prim(_, "nat", [], _debug) -> Tnat | Script_repr.Prim(_, "bool", [], _debug) -> Tbool | Script_repr.Prim(_, "key", [], _debug) -> Tkey + | Script_repr.Prim(_, "key_hash", [], _debug) -> Tkey_hash | Script_repr.Prim(_, "signature", [], _debug) -> Tsignature | Script_repr.Prim(_, "string", [], _debug) -> Tstring | Script_repr.Prim(_, "pair", [x;y], _debug) -> Ttuple [convert_type x; @@ -84,106 +85,185 @@ let rec convert_type expr = | Script_repr.Prim(_, "option", [x], _debug) -> Toption (convert_type x) | _ -> unknown_expr "convert_type" expr -let rec convert_code expr = +let loc_of_int loc_table index = + try List.assoc index loc_table + with Not_found -> LiquidLoc.noloc + +let rec convert_code loc_table expr = match expr with - | Script_repr.Seq (_loc, exprs, _debug) -> - SEQ (List.map convert_code exprs) - | Script_repr.Prim(_, "DUP", [], _debug) -> DUP 1 - | Script_repr.Prim(_, "DROP", [], _debug) -> DROP - | Script_repr.Prim(_, "DIP", [ arg ], _debug) -> DIP (1, convert_code arg) - | Script_repr.Prim(_, "CAR", [], _debug) -> CAR - | Script_repr.Prim(_, "CDR", [], _debug) -> CDR - | Script_repr.Prim(_, "SWAP", [], _debug) -> SWAP - | Script_repr.Prim(_, "IF", [x;y], _debug) -> - IF (convert_code x, convert_code y) - | Script_repr.Prim(_, "IF_NONE", [x;y], _debug) -> - IF_NONE (convert_code x, convert_code y) - | Script_repr.Prim(_, "IF_LEFT", [x;y], _debug) -> - IF_LEFT (convert_code x, convert_code y) - | Script_repr.Prim(_, "IF_CONS", [x;y], _debug) -> - IF_CONS (convert_code x, convert_code y) - | Script_repr.Prim(_, "NOW", [], _debug) -> NOW - | Script_repr.Prim(_, "PAIR", [], _debug) -> PAIR - | Script_repr.Prim(_, "BALANCE", [], _debug) -> BALANCE - | Script_repr.Prim(_, "SUB", [], _debug) -> SUB - | Script_repr.Prim(_, "ADD", [], _debug) -> ADD - | Script_repr.Prim(_, "MUL", [], _debug) -> MUL - | Script_repr.Prim(_, "NEQ", [], _debug) -> NEQ - | Script_repr.Prim(_, "EQ", [], _debug) -> EQ - | Script_repr.Prim(_, "LT", [], _debug) -> LT - | Script_repr.Prim(_, "LE", [], _debug) -> LE - | Script_repr.Prim(_, "GT", [], _debug) -> GT - | Script_repr.Prim(_, "GE", [], _debug) -> GE - | Script_repr.Prim(_, "GET", [], _debug) -> GET - | Script_repr.Prim(_, "UPDATE", [], _debug) -> UPDATE - | Script_repr.Prim(_, "MEM", [], _debug) -> MEM - | Script_repr.Prim(_, "SOME", [], _debug) -> SOME - | Script_repr.Prim(_, "MANAGER", [], _debug) -> MANAGER - | Script_repr.Prim(_, "SOURCE", [ty1; ty2], _debug) -> - SOURCE (convert_type ty1, convert_type ty2) - | Script_repr.Prim(_, "MAP", [], _debug) -> MAP - | Script_repr.Prim(_, "OR", [], _debug) -> OR - | Script_repr.Prim(_, "LAMBDA", [ty1; ty2; expr], _debug) -> - LAMBDA (convert_type ty1, convert_type ty2, convert_code expr) - | Script_repr.Prim(_, "REDUCE", [], _debug) -> REDUCE - | Script_repr.Prim(_, "COMPARE", [], _debug) -> COMPARE - | Script_repr.Prim(_, "FAIL", [], _debug) -> FAIL - | Script_repr.Prim(_, "UNIT", [], _debug) -> PUSH (Tunit, CUnit) - | Script_repr.Prim(_, "TRANSFER_TOKENS", [], _debug) -> TRANSFER_TOKENS - | Script_repr.Prim(_, "PUSH", [ ty; cst ], _debug) -> + | Script_repr.Seq (index, exprs, _debug) -> + mic_loc (loc_of_int loc_table index) + (SEQ (List.map (convert_code loc_table) exprs)) + | Script_repr.Prim(index, "DUP", [], _debug) -> + mic_loc (loc_of_int loc_table index) (DUP 1) + | Script_repr.Prim(index, "DROP", [], _debug) -> + mic_loc (loc_of_int loc_table index) (DROP) + | Script_repr.Prim(index, "DIP", [ arg ], _debug) -> + mic_loc (loc_of_int loc_table index) (DIP (1, convert_code loc_table arg)) + | Script_repr.Prim(index, "CAR", [], _debug) -> + mic_loc (loc_of_int loc_table index) (CAR) + | Script_repr.Prim(index, "CDR", [], _debug) -> + mic_loc (loc_of_int loc_table index) (CDR) + | Script_repr.Prim(index, "SWAP", [], _debug) -> + mic_loc (loc_of_int loc_table index) (SWAP) + | Script_repr.Prim(index, "IF", [x;y], _debug) -> + mic_loc (loc_of_int loc_table index) + (IF (convert_code loc_table x, convert_code loc_table y)) + | Script_repr.Prim(index, "IF_NONE", [x;y], _debug) -> + mic_loc (loc_of_int loc_table index) + (IF_NONE (convert_code loc_table x, convert_code loc_table y)) + | Script_repr.Prim(index, "IF_LEFT", [x;y], _debug) -> + mic_loc (loc_of_int loc_table index) + (IF_LEFT (convert_code loc_table x, convert_code loc_table y)) + | Script_repr.Prim(index, "IF_CONS", [x;y], _debug) -> + mic_loc (loc_of_int loc_table index) + (IF_CONS (convert_code loc_table x, convert_code loc_table y)) + | Script_repr.Prim(index, "NOW", [], _debug) -> + mic_loc (loc_of_int loc_table index) (NOW) + | Script_repr.Prim(index, "PAIR", [], _debug) -> + mic_loc (loc_of_int loc_table index) (PAIR) + | Script_repr.Prim(index, "BALANCE", [], _debug) -> + mic_loc (loc_of_int loc_table index) (BALANCE) + | Script_repr.Prim(index, "SUB", [], _debug) -> + mic_loc (loc_of_int loc_table index) (SUB) + | Script_repr.Prim(index, "ADD", [], _debug) -> + mic_loc (loc_of_int loc_table index) (ADD) + | Script_repr.Prim(index, "MUL", [], _debug) -> + mic_loc (loc_of_int loc_table index) (MUL) + | Script_repr.Prim(index, "NEQ", [], _debug) -> + mic_loc (loc_of_int loc_table index) (NEQ) + | Script_repr.Prim(index, "EQ", [], _debug) -> + mic_loc (loc_of_int loc_table index) (EQ) + | Script_repr.Prim(index, "LT", [], _debug) -> + mic_loc (loc_of_int loc_table index) (LT) + | Script_repr.Prim(index, "LE", [], _debug) -> + mic_loc (loc_of_int loc_table index) (LE) + | Script_repr.Prim(index, "GT", [], _debug) -> + mic_loc (loc_of_int loc_table index) (GT) + | Script_repr.Prim(index, "GE", [], _debug) -> + mic_loc (loc_of_int loc_table index) (GE) + | Script_repr.Prim(index, "GET", [], _debug) -> + mic_loc (loc_of_int loc_table index) (GET) + | Script_repr.Prim(index, "UPDATE", [], _debug) -> + mic_loc (loc_of_int loc_table index) (UPDATE) + | Script_repr.Prim(index, "MEM", [], _debug) -> + mic_loc (loc_of_int loc_table index) (MEM) + | Script_repr.Prim(index, "SOME", [], _debug) -> + mic_loc (loc_of_int loc_table index) (SOME) + | Script_repr.Prim(index, "MANAGER", [], _debug) -> + mic_loc (loc_of_int loc_table index) (MANAGER) + | Script_repr.Prim(index, "SOURCE", [ty1; ty2], _debug) -> + mic_loc (loc_of_int loc_table index) + (SOURCE (convert_type ty1, convert_type ty2)) + | Script_repr.Prim(index, "MAP", [], _debug) -> + mic_loc (loc_of_int loc_table index) (MAP) + | Script_repr.Prim(index, "OR", [], _debug) -> + mic_loc (loc_of_int loc_table index) (OR) + | Script_repr.Prim(index, "LAMBDA", [ty1; ty2; expr], _debug) -> + mic_loc (loc_of_int loc_table index) + (LAMBDA (convert_type ty1, convert_type ty2, convert_code loc_table expr)) + | Script_repr.Prim(index, "REDUCE", [], _debug) -> + mic_loc (loc_of_int loc_table index) (REDUCE) + | Script_repr.Prim(index, "COMPARE", [], _debug) -> + mic_loc (loc_of_int loc_table index) (COMPARE) + | Script_repr.Prim(index, "FAIL", [], _debug) -> + mic_loc (loc_of_int loc_table index) (FAIL) + | Script_repr.Prim(index, "UNIT", [], _debug) -> + mic_loc (loc_of_int loc_table index) (PUSH (Tunit, CUnit)) + | Script_repr.Prim(index, "TRANSFER_TOKENS", [], _debug) -> + mic_loc (loc_of_int loc_table index) (TRANSFER_TOKENS) + | Script_repr.Prim(index, "PUSH", [ ty; cst ], _debug) -> begin match convert_type ty, convert_const cst with | Tnat, CInt n -> - PUSH (Tnat, CNat n) + mic_loc (loc_of_int loc_table index) (PUSH (Tnat, CNat n)) | ty, cst -> - PUSH (ty, cst) + mic_loc (loc_of_int loc_table index) (PUSH (ty, cst)) end - | Script_repr.Prim(_, "H", [], _debug) -> H - | Script_repr.Prim(_, "CHECK_SIGNATURE", [], _debug) -> CHECK_SIGNATURE - | Script_repr.Prim(_, "CONCAT", [], _debug) -> CONCAT - | Script_repr.Prim(_, "EDIV", [], _debug) -> EDIV - | Script_repr.Prim(_, "EXEC", [], _debug) -> EXEC - | Script_repr.Prim(_, "MOD", [], _debug) -> MOD - | Script_repr.Prim(_, "DIV", [], _debug) -> DIV - | Script_repr.Prim(_, "AMOUNT", [], _debug) -> AMOUNT - | Script_repr.Prim(_, "NIL", [ty], _debug) -> - PUSH (Tlist (convert_type ty), CList []) - | Script_repr.Prim(_, "EMPTY_SET", [ty], _debug) -> - PUSH (Tset (convert_type ty), CSet []) - | Script_repr.Prim(_, "EMPTY_MAP", [ty1; ty2], _debug) -> - PUSH (Tmap (convert_type ty1, convert_type ty2), CMap []) - | Script_repr.Prim(_, "NONE", [ty], _debug) -> - PUSH (Toption (convert_type ty), CNone) - | Script_repr.Prim(_, "LEFT", [ty], _debug) -> - LEFT (convert_type ty) - | Script_repr.Prim(_, "CONS", [], _debug) -> CONS - | Script_repr.Prim(_, "LOOP", [loop], _debug) -> LOOP (convert_code loop) - | Script_repr.Prim(_, "RIGHT", [ty], _debug) -> - RIGHT (convert_type ty) - | Script_repr.Prim(_, "INT", [], _debug) -> INT - | Script_repr.Prim(_, "SIZE", [], _debug) -> SIZE - | Script_repr.Prim(_, "AND", [], _debug) -> AND - | Script_repr.Prim(_, "XOR", [], _debug) -> XOR - | Script_repr.Prim(_, "ABS", [], _debug) -> ABS - | Script_repr.Prim(_, "NOT", [], _debug) -> NOT - | Script_repr.Prim(_, "STEPS_TO_QUOTA", [], _debug) -> STEPS_TO_QUOTA - | Script_repr.Prim(_, "CREATE_ACCOUNT", [], _debug) -> CREATE_ACCOUNT - | Script_repr.Prim(_, "CREATE_CONTRACT", [], _debug) -> CREATE_CONTRACT - | Script_repr.Prim(_, "DEFAULT_ACCOUNT", [], _debug) -> DEFAULT_ACCOUNT - + | Script_repr.Prim(index, "H", [], _debug) -> + mic_loc (loc_of_int loc_table index) (H) + | Script_repr.Prim(index, "HASH_KEY", [], _debug) -> + mic_loc (loc_of_int loc_table index) (HASH_KEY) + | Script_repr.Prim(index, "CHECK_SIGNATURE", [], _debug) -> + mic_loc (loc_of_int loc_table index) (CHECK_SIGNATURE) + | Script_repr.Prim(index, "CONCAT", [], _debug) -> + mic_loc (loc_of_int loc_table index) (CONCAT) + | Script_repr.Prim(index, "EDIV", [], _debug) -> + mic_loc (loc_of_int loc_table index) (EDIV) + | Script_repr.Prim(index, "EXEC", [], _debug) -> + mic_loc (loc_of_int loc_table index) (EXEC) + | Script_repr.Prim(index, "MOD", [], _debug) -> + mic_loc (loc_of_int loc_table index) (MOD) + | Script_repr.Prim(index, "DIV", [], _debug) -> + mic_loc (loc_of_int loc_table index) (DIV) + | Script_repr.Prim(index, "AMOUNT", [], _debug) -> + mic_loc (loc_of_int loc_table index) (AMOUNT) + | Script_repr.Prim(index, "NIL", [ty], _debug) -> + mic_loc (loc_of_int loc_table index) + (PUSH (Tlist (convert_type ty), CList [])) + | Script_repr.Prim(index, "EMPTY_SET", [ty], _debug) -> + mic_loc (loc_of_int loc_table index) + (PUSH (Tset (convert_type ty), CSet [])) + | Script_repr.Prim(index, "EMPTY_MAP", [ty1; ty2], _debug) -> + mic_loc (loc_of_int loc_table index) + (PUSH (Tmap (convert_type ty1, convert_type ty2), CMap [])) + | Script_repr.Prim(index, "NONE", [ty], _debug) -> + mic_loc (loc_of_int loc_table index) + (PUSH (Toption (convert_type ty), CNone)) + | Script_repr.Prim(index, "LEFT", [ty], _debug) -> + mic_loc (loc_of_int loc_table index) + (LEFT (convert_type ty)) + | Script_repr.Prim(index, "CONS", [], _debug) -> + mic_loc (loc_of_int loc_table index) (CONS) + | Script_repr.Prim(index, "LOOP", [loop], _debug) -> + mic_loc (loc_of_int loc_table index) + (LOOP (convert_code loc_table loop)) + | Script_repr.Prim(index, "RIGHT", [ty], _debug) -> + mic_loc (loc_of_int loc_table index) + (RIGHT (convert_type ty)) + | Script_repr.Prim(index, "INT", [], _debug) -> + mic_loc (loc_of_int loc_table index) (INT) + | Script_repr.Prim(index, "SIZE", [], _debug) -> + mic_loc (loc_of_int loc_table index) (SIZE) + | Script_repr.Prim(index, "AND", [], _debug) -> + mic_loc (loc_of_int loc_table index) (AND) + | Script_repr.Prim(index, "XOR", [], _debug) -> + mic_loc (loc_of_int loc_table index) (XOR) + | Script_repr.Prim(index, "ABS", [], _debug) -> + mic_loc (loc_of_int loc_table index) (ABS) + | Script_repr.Prim(index, "NOT", [], _debug) -> + mic_loc (loc_of_int loc_table index) (NOT) + | Script_repr.Prim(index, "STEPS_TO_QUOTA", [], _debug) -> + mic_loc (loc_of_int loc_table index) (STEPS_TO_QUOTA) + | Script_repr.Prim(index, "CREATE_ACCOUNT", [], _debug) -> + mic_loc (loc_of_int loc_table index) (CREATE_ACCOUNT) + | Script_repr.Prim(index, "CREATE_CONTRACT", [], _debug) -> + mic_loc (loc_of_int loc_table index) (CREATE_CONTRACT) + | Script_repr.Prim(index, "DEFAULT_ACCOUNT", [], _debug) -> + mic_loc (loc_of_int loc_table index) (DEFAULT_ACCOUNT) | _ -> unknown_expr "convert_code" expr -let convert_contract c = +let convert_contract loc_table c = let return = convert_type c.Script_repr.ret_type in let parameter = convert_type c.Script_repr.arg_type in let storage = convert_type c.Script_repr.storage_type in - let code = convert_code c.Script_repr.code in - { code; - storage; return; parameter } + let code = convert_code loc_table c.Script_repr.code in + { code; storage; return; parameter } + +let liquid_loc_of_script_loc f { Script_located_ir.start; stop } = + { loc_file = f; + loc_pos = Some ( + (start.Script_located_ir.line, start.Script_located_ir.column), + (stop.Script_located_ir.line, stop.Script_located_ir.column)) + } + +let convert_loc_table f loc_table = + let loc_table = List.assoc "code" loc_table in + List.map (fun (i, p) -> (i, liquid_loc_of_script_loc f p)) loc_table -let contract_of_string s = +let contract_of_string filename s = match Client_proto_programs.parse_program s with - | Ok parsed -> Some parsed.ast + | Ok parsed -> Some (parsed.ast, convert_loc_table filename parsed.loc_table) | Error _ -> None let data_of_string s = diff --git a/tools/liquidity/with-tezos/liquidToTezos.ml b/tools/liquidity/with-tezos/liquidToTezos.ml index a66c2988..c214e28e 100644 --- a/tools/liquidity/with-tezos/liquidToTezos.ml +++ b/tools/liquidity/with-tezos/liquidToTezos.ml @@ -63,6 +63,7 @@ let rec convert_const expr = *) | CTimestamp s -> Script_repr.String (0, s) | CKey s -> Script_repr.String (0, s) + | CKey_hash s -> Script_repr.String (0, s) | CSignature s -> Script_repr.String (0, s) | _ -> @@ -79,6 +80,7 @@ let rec convert_type expr = | Tnat -> prim "nat" [] | Tbool -> prim "bool" [] | Tkey -> prim "key" [] + | Tkey_hash -> prim "key_hash" [] | Tsignature -> prim "signature" [] | Tstring -> prim "string" [] | Ttuple [x] -> assert false @@ -99,7 +101,7 @@ let rec convert_type expr = | Ttype (_, ty) -> convert_type ty let rec convert_code expr = - match expr with + match expr.i with | SEQ exprs -> Script_repr.Seq (0, List.map convert_code exprs, debug) | DROP -> prim "DROP" [] @@ -146,6 +148,7 @@ let rec convert_code expr = | PUSH (ty, cst) -> prim "PUSH" [ convert_type ty; convert_const cst ] | H -> prim "H" [] + | HASH_KEY -> prim "HASH_KEY" [] | CHECK_SIGNATURE -> prim "CHECK_SIGNATURE" [] | CONCAT -> prim "CONCAT" [] | EDIV -> prim "EDIV" [] @@ -185,7 +188,9 @@ let rec convert_code expr = | LSL -> prim "LSL" [] | LSR -> prim "LSR" [] | DIP_DROP (ndip, ndrop) -> - convert_code (DIP (ndip, SEQ (LiquidMisc.list_init ndrop (fun _ -> DROP)))) + convert_code {i=DIP (ndip, + {i=SEQ (LiquidMisc.list_init ndrop + (fun _ -> {i=DROP}))})} | CDAR n -> prim (Printf.sprintf "C%sAR" (String.make n 'D')) [] | CDDR n -> prim (Printf.sprintf "C%sDR" (String.make n 'D')) [] | SIZE -> prim "SIZE" [] @@ -237,16 +242,16 @@ let get_context () = let read_tezos_file filename = let s = FileString.read_file filename in let contract_hash = Hash.Operation_hash.hash_bytes [s] in - match LiquidFromTezos.contract_of_string s with - | Some code -> + match LiquidFromTezos.contract_of_string filename s with + | Some (code, loc_table) -> Printf.eprintf "Program %S parsed\n%!" filename; - code, contract_hash + code, contract_hash, loc_table | None -> Printf.eprintf "Errors parsing in %S\n%!" filename; exit 2 let execute_contract_file filename = - let contract, contract_hash = read_tezos_file filename in + let contract, contract_hash, _ = read_tezos_file filename in let origination = Contract.initial_origination_nonce contract_hash in let destination = Contract.originated_contract origination in diff --git a/tools/liquidity/without-tezos/liquidFromTezos.ml b/tools/liquidity/without-tezos/liquidFromTezos.ml index 5f60e0d9..c7ea4ebf 100644 --- a/tools/liquidity/without-tezos/liquidFromTezos.ml +++ b/tools/liquidity/without-tezos/liquidFromTezos.ml @@ -10,7 +10,7 @@ open LiquidTypes -let convert_contract string = assert false +let convert_contract loc_table string = assert false (* open Client_proto_programs @@ -181,8 +181,7 @@ let convert_contract c = let parameter = convert_type c.Script_repr.arg_type in let storage = convert_type c.Script_repr.storage_type in let code = convert_code c.Script_repr.code in - { code; - storage; return; parameter } + { code; storage; return; parameter } let contract_of_string s = match Client_proto_programs.parse_program s with diff --git a/tools/liquidity/without-tezos/liquidToTezos.ml b/tools/liquidity/without-tezos/liquidToTezos.ml index 933e1d8e..97988e5b 100644 --- a/tools/liquidity/without-tezos/liquidToTezos.ml +++ b/tools/liquidity/without-tezos/liquidToTezos.ml @@ -12,7 +12,7 @@ open LiquidTypes let string_of_contract (c : michelson_exp contract) = LiquidPrinter.Michelson.string_of_contract c -let convert_contract (c : pre_michelson contract) = +let convert_contract (c : noloc_michelson contract) = LiquidEmit.emit_contract c let read_tezos_file (_filename : string) = assert false diff --git a/travis-scripts/prepare-opam.sh b/travis-scripts/prepare-opam.sh new file mode 100755 index 00000000..3f34b198 --- /dev/null +++ b/travis-scripts/prepare-opam.sh @@ -0,0 +1,15 @@ +# This script is used in .travis.yml for continuous integration on travis. +# BTW, it also show some needed system packages to build liquidity +# Travis CI is done on Ubuntu trusty + +wget -qq https://raw.github.com/ocaml/opam/master/shell/opam_installer.sh -O - | sh -s /usr/local/bin +export OPAMYES=1 + +# currently, we only target OCaml 4.05.0 because we reuse parser of OCaml 4.05.0 +opam init --comp 4.05.0 + +eval `opam config env` + +opam update +opam install ocp-build zarith uutf uri uchar stringext sexplib re ocplib-json-typed ocplib-endian jsonm hex ezjsonm cstruct calendar +# TODO > other deps are missing ? diff --git a/travis-scripts/prepare-trusty.sh b/travis-scripts/prepare-trusty.sh new file mode 100755 index 00000000..e4e3314c --- /dev/null +++ b/travis-scripts/prepare-trusty.sh @@ -0,0 +1,13 @@ +# This script is used in .travis.yml for continuous integration on travis. +# BTW, it also show some needed system packages to build liquidity. +# Travis CI is done on Ubuntu trusty + +sudo apt-get update -qq +sudo apt-get install -y -qq libgmp-dev # ocaml ocaml-native-compilers + +# do this in a second step to only install libsecp256k1-dev libsecp256k1-0 +# for ubuntu, these packages are not available in trusty +sudo add-apt-repository "deb http://cz.archive.ubuntu.com/ubuntu artful main universe" +sudo apt-get update -qq +sudo apt-get install -y -qq libsecp256k1-dev libsecp256k1-0 +