diff --git a/Makefile b/Makefile index e2a3b18f..9df891f1 100644 --- a/Makefile +++ b/Makefile @@ -27,14 +27,16 @@ distclean: clean # All of these tests must be run with with_tezos=true -NTESTS=20 +NTESTS=32 +NTESTS=21 +NREVTESTS=6 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_left_match OTHER_TESTS=others/broker others/demo others/auction -REV_TESTS=`seq -f 'test%.0f' 0 5` +REV_TESTS=`seq -f 'test%.0f' 0 $(NREVTESTS)` NEW_TEZOS_TESTS= fail weather_insurance FAILING_TEZOS_TESTS= originator diff --git a/check.sh b/check.sh index b3dff903..0e63e8ba 100755 --- a/check.sh +++ b/check.sh @@ -7,28 +7,32 @@ test=$1 echo "\n[check.sh] test = $test" LIQUIDITY=liquidity +TEZOS_FULL_PATH=./tezos/_obuild/tezos-client/tezos-client.asm +LIQUID_FULL_PATH=./_obuild/${LIQUIDITY}/${LIQUIDITY}.asm +LIQARGS=--verbose +LIQEXEC="${LIQUID_FULL_PATH} ${LIQARGS}" -echo ./_obuild/${LIQUIDITY}/${LIQUIDITY}.asm tests/$test.liq -./_obuild/${LIQUIDITY}/${LIQUIDITY}.asm tests/$test.liq || exit 2 +echo ${LIQEXEC} tests/$test.liq +${LIQEXEC} tests/$test.liq || exit 2 -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 +if [ -f ${TEZOS_FULL_PATH} ] ; then + ${TEZOS_FULL_PATH} 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" + echo "\n${RED}${TEZOS_FULL_PATH} 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 +echo ${LIQEXEC} tests/$test.liq.tz +${LIQEXEC} tests/$test.liq.tz || exit 2 -echo ./_obuild/${LIQUIDITY}/${LIQUIDITY}.asm tests/$test.liq.tz.liq -./_obuild/${LIQUIDITY}/${LIQUIDITY}.asm tests/$test.liq.tz.liq || exit 2 +echo ${LIQEXEC} tests/$test.liq.tz.liq +${LIQEXEC} tests/$test.liq.tz.liq || exit 2 -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 +if [ -f ${TEZOS_FULL_PATH} ] ; then + ${TEZOS_FULL_PATH} 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" + echo "\n${RED}${TEZOS_FULL_PATH} 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 +./_obuild/ocp-liquidity-comp/ocp-liquidity-comp.asm -I +../zarith zarith.cma -I _obuild/liquidity-env unix.cma ./_obuild/liquidity-env/liquidity-env.cma -dsource -impl tests/$test.liq || exit 2 rm -f a.out diff --git a/libs/deps-michelson/build.ocp2 b/libs/deps-michelson/build.ocp2 index 2637907c..71c74761 100644 --- a/libs/deps-michelson/build.ocp2 +++ b/libs/deps-michelson/build.ocp2 @@ -10,15 +10,14 @@ (* This part of the library is made to create a minimal set of dependencies to be able to run code that was directly extracted from Tezos *) -if( with_tezos ) { -OCaml.library("michelson-deps", ocaml + { - bytelink = [ "-custom" ]; - files = [ +OCaml.library("ocplib-blockchain-crypto", ocaml + { + bytelink = [ "-custom" ]; + files = [ "sha256.c"; (* from Polar SSL *) "sha256-stubs.c"; - + "tweetnacl.c"; "blake2b-ref.c"; (* from BLAKE/BLAKE *) "blake2b-stubs.c"; @@ -32,6 +31,18 @@ OCaml.library("michelson-deps", ocaml + { "mBytes.ml"; "hex_encode.ml"; "nocrypto.ml"; + ]; + requires = [ + "ocplib-endian"; + ]; + cclib = [ "-lsecp256k1" ] + }); + +if( with_tezos ) { + +OCaml.library("michelson-deps", ocaml + { + files = [ + "sodium.ml"; @@ -50,9 +61,9 @@ OCaml.library("michelson-deps", ocaml + { "updater.ml"; ]; requires = [ - "ocplib-endian"; (* mBytes *) + + "ocplib-blockchain-crypto"; ]; - cclib = [ "-lsecp256k1" ] }); } diff --git a/libs/deps-michelson/mBytes.ml b/libs/deps-michelson/mBytes.ml index 02a84299..2bbcd4f0 100644 --- a/libs/deps-michelson/mBytes.ml +++ b/libs/deps-michelson/mBytes.ml @@ -1,6 +1,6 @@ type t = bytes -let create = String.create +let create = Bytes.create let length = String.length let compare = compare @@ -11,7 +11,7 @@ let of_string s = s let blit = String.blit let blit_from_string = String.blit let blit_to_bytes = String.blit -let copy = String.copy +let copy = Bytes.copy let sub = String.sub let substring = String.sub let concat = (^) diff --git a/libs/deps-michelson/mBytes.mli b/libs/deps-michelson/mBytes.mli index 29c477f9..e2887552 100644 --- a/libs/deps-michelson/mBytes.mli +++ b/libs/deps-michelson/mBytes.mli @@ -1,11 +1,3 @@ -(**************************************************************************) -(* *) -(* Copyright (c) 2014 - 2016. *) -(* Dynamic Ledger Solutions, Inc. *) -(* *) -(* All rights reserved. No warranty, explicit or implicit, provided. *) -(* *) -(**************************************************************************) type t = bytes @@ -14,12 +6,6 @@ val create: int -> t val length: t -> int val compare : t -> t -> int -(* - -open Bigarray - -type t = (char, int8_unsigned_elt, c_layout) Array1.t - *) val copy: t -> t @@ -28,12 +14,6 @@ val sub: t -> int -> int -> t and of length [len]. No copying of elements is involved: the sub-array and the original array share the same storage space. *) - (* - -val shift: t -> int -> t -(** [shift src ofs] is equivalent to [sub src ofs (length src - ofs)] *) - *) - val blit: t -> int -> t -> int -> int -> unit (** [blit src ofs_src dst ofs_dst len] copy [len] bytes from [src] starting at [ofs_src] into [dst] starting at [ofs_dst].] *) @@ -41,9 +21,6 @@ val blit: t -> int -> t -> int -> int -> unit val blit_from_string: string -> int -> t -> int -> int -> unit (** See [blit] *) -val blit_to_bytes: t -> int -> bytes -> int -> int -> unit -(** See [blit] *) - val of_string: string -> t (** [of_string s] create an byte array filled with the same content than [s]. *) @@ -74,7 +51,6 @@ val set_int8: t -> int -> int -> unit (** [set_int8 buff i v] writes the least significant 8 bits of [v] to [buff] at offset [i] *) -(** Functions reading according to Big Endian byte order *) val get_uint16: t -> int -> int (** [get_uint16 buff i] reads 2 bytes at offset i as an unsigned int @@ -90,9 +66,6 @@ val get_int32: t -> int -> int32 val get_int64: t -> int -> int64 (** [get_int64 buff i] reads 8 bytes at offset i as an int64. *) -val get_float: t -> int -> float -(** [get_float buff i] reads 4 bytes at offset i as an IEEE754 float. *) - val get_double: t -> int -> float (** [get_float buff i] reads 8 bytes at offset i as an IEEE754 double. *) @@ -106,52 +79,8 @@ val set_int32: t -> int -> int32 -> unit val set_int64: t -> int -> int64 -> unit (** [set_int64 buff i v] writes [v] to [buff] at offset [i] *) + val set_double: t -> int -> float -> unit (** [set_double buff i v] writes [v] to [buff] at offset [i] *) -(* - -val set_float: t -> int -> float -> unit -(** [set_float buff i v] writes [v] to [buff] at offset [i] *) -val of_float: float -> t - -module LE: sig - - (** Functions reading according to Little Endian byte order *) - - val get_uint16: t -> int -> int - (** [get_uint16 buff i] reads 2 bytes at offset i as an unsigned int - of 16 bits. i.e. It returns a value between 0 and 2^16-1 *) - - val get_int16: t -> int -> int - (** [get_int16 buff i] reads 2 byte at offset i as a signed int of - 16 bits. i.e. It returns a value between -2^15 and 2^15-1 *) - - val get_int32: t -> int -> int32 - (** [get_int32 buff i] reads 4 bytes at offset i as an int32. *) - - val get_int64: t -> int -> int64 - (** [get_int64 buff i] reads 8 bytes at offset i as an int64. *) - - val set_int16: t -> int -> int -> unit - (** [set_int16 buff i v] writes the least significant 16 bits of [v] - to [buff] at offset [i] *) - - val set_int32: t -> int -> int32 -> unit - (** [set_int32 buff i v] writes [v] to [buff] at offset [i] *) - - val set_int64: t -> int -> int64 -> unit - (** [set_int64 buff i v] writes [v] to [buff] at offset [i] *) - -end - -val (=) : t -> t -> bool -val (<>) : t -> t -> bool -val (<) : t -> t -> bool -val (<=) : t -> t -> bool -val (>=) : t -> t -> bool -val (>) : t -> t -> bool -val compare : t -> t -> int - *) - val concat: t -> t -> t diff --git a/libs/deps-michelson/secp256k1-stubs.c b/libs/deps-michelson/secp256k1-stubs.c index 8205adbf..fd8b11d3 100644 --- a/libs/deps-michelson/secp256k1-stubs.c +++ b/libs/deps-michelson/secp256k1-stubs.c @@ -386,8 +386,8 @@ value secp256k1_ec_pubkey_create_ml const secp256k1_context* ctx = (const secp256k1_context*) String_val(ctx_v); - const secp256k1_pubkey *pubkey = - (const secp256k1_pubkey *) + secp256k1_pubkey *pubkey = + (secp256k1_pubkey *) String_val(pubkey_v); const unsigned char *seckey = (const unsigned char *) diff --git a/libs/michelson/base58.ml b/libs/michelson/base58.ml index a13c1aee..9cb4cecc 100644 --- a/libs/michelson/base58.ml +++ b/libs/michelson/base58.ml @@ -1 +1,2 @@ + #include "../../tezos/src/utils/base58.ml" diff --git a/libs/michelson/seed_storage.ml b/libs/michelson/seed_storage.ml index f9ce870e..d0e806c4 100644 --- a/libs/michelson/seed_storage.ml +++ b/libs/michelson/seed_storage.ml @@ -4,4 +4,6 @@ open Hash open Utils open Tezos_data +open Storage.Seed +open Level_repr #include "../../tezos/src/proto/alpha/seed_storage.ml" diff --git a/libs/michelson/vote_storage.ml b/libs/michelson/vote_storage.ml index f6ad154d..87d49b5e 100644 --- a/libs/michelson/vote_storage.ml +++ b/libs/michelson/vote_storage.ml @@ -4,4 +4,6 @@ open Hash open Utils open Tezos_data +open Vote_repr +open Voting_period_repr #include "../../tezos/src/proto/alpha/vote_storage.ml" diff --git a/tests/others/auction.liq b/tests/others/auction.liq index efbd5cc8..696adb32 100644 --- a/tests/others/auction.liq +++ b/tests/others/auction.liq @@ -1,6 +1,6 @@ (* Auction contract from https://www.michelson-lang.com/contract-a-day.html *) -[%%version 0.11] +[%%version 0.13] type storage = { auction_end : timestamp; @@ -11,11 +11,14 @@ type storage = { let%entry main (parameter : key_hash) (storage : storage) - : unit * storage = + : unit * storage + [@requires storage.highest_bid < Current.balance () ] + [@ensures @storage.highest_bid < Current.balance () ] + = (* Check if auction has ended *) if Current.time () > storage.auction_end then Current.fail (); - + let new_bid = Current.amount () in let new_bidder = parameter in (* Check if new bid is higher that the last *) diff --git a/tests/others/broker.liq b/tests/others/broker.liq index d16f0f28..380da830 100644 --- a/tests/others/broker.liq +++ b/tests/others/broker.liq @@ -1,5 +1,5 @@ -[%%version 0.11] +[%%version 0.13] type storage = { state : string; diff --git a/tests/others/demo.liq b/tests/others/demo.liq index 9b091eb6..8ff6c6ab 100644 --- a/tests/others/demo.liq +++ b/tests/others/demo.liq @@ -1,5 +1,5 @@ -[%%version 0.11] +[%%version 0.13] let%entry main (parameter : string) diff --git a/tests/others/multisig.liq b/tests/others/multisig.liq new file mode 100644 index 00000000..38ef7446 --- /dev/null +++ b/tests/others/multisig.liq @@ -0,0 +1,132 @@ +[%%version 0.13] + +(* A proposition of transfer to a destination, the address of (unit, unit) + contract *) +type proposition = { + destination : key_hash; + amount : tez; +} + +(* An owner can submit a proposition or remove a previously submitted + proposition *) +type action = proposition option + +(* The multisig contract can be payed to, simply transfering tokens to it, + or an owner can submit an action *) +type parameter = + | Pay + | Manage of action + +(* min is the minimum number of owner who must agree for the transaction to + proceed + actions is a map from owners to their submited action, for an address to be + an owner it must have a binding in this map +*) +type storage = { + owners : (key_hash, nat) map; + actions : (nat, proposition) map; + owners_length : nat; + min_agree : nat; +} + +(* fails if the proposition is not a valid one *) +let check_proposition (p:proposition) + (* [@fails p.amount > Current.balance () ] *) + = + if p.amount > Current.balance () then Current.fail () else () + + +(* returns the address of the current caller of this multisig contract *) +let get_caller (_ : unit) + (* [@ensures @result = source_address ] *) + = + let c = (Source : (unit, unit) contract) in + Contract.manager c + +(* returns true if the current caller is also an owner *) +let check_caller_owner (s : storage) + (* [@fails s.actions[source_address] = None ] *) + = + let k = get_caller () in + match Map.find k s.owners with + | Some _ -> () + | None -> Current.fail () + +(* returns true if two proositions are identical *) +let equal_props ((p1:proposition), (p2:proposition)) + (* [@ensures @result = p1 = p2 ] *) + = + p1.destination = p2.destination & + p1.amount = p2.amount + +(*@why3 + +use map.Occ + +*) + +(* returns true if a proposition p should be executed immediately *) +let should_execute ((p : proposition), (storage : storage)) + (* [@ensures + @result <=> + Occ.occ p 0p storage.owners_length >= storage.min_agree + ] *) + = + let nb_agree = + Map.reduce (fun (((_i:nat), (p':proposition)), (cpt:nat)) -> + if equal_props (p, p') then cpt + 1p else cpt + ) storage.actions 0p + in + nb_agree >= storage.min_agree + + +let%entry main + (parameter : parameter) + (storage : storage) + : unit * storage + [@ensures + let delta = Current.balance () - old (Current.balance ()) in + match parameter with + | Pay -> delta >= 0tz + | Manage a -> + match a with + | None -> delta = 0tz + | Some p -> + (* Map.find (Contract.manager (Source : (unit, unit) contract)) *) + (* storage.owners <> (None : nat option) *) + (* /\ *) delta <= 0tz + /\ (delta < 0tz => p.amount + delta = 0tz) + ] + = + match parameter with + | Pay -> + (* Simple payment, nothing to do *) + (), storage + | Manage action -> + (* Owner want to perform an action *) + let k = get_caller () in + match Map.find k storage.owners with + | None -> Current.fail () (* the caller must be an owner*) + | Some owner -> + (* Register the desired action in the storage *) + let storage = + storage.actions <- Map.update owner action storage.actions in + let storage = + match action with + | None -> + (* If the action is to remove previous proposition, then nothing to + tdo *) + storage + | Some p -> + (* The action is new proposition *) + check_proposition p; (* it must be a valid one *) + if should_execute (p, storage) then + (* execute proposition, i.e. transfer tokens *) + let c_dest = Account.default p.destination in + let _, storage = Contract.call c_dest p.amount storage () in + (* reset the map of actions *) + storage.actions <- (Map [] : (nat, proposition) map) + else + storage + in + (), storage diff --git a/tests/reports/issue39.liq b/tests/reports/issue39.liq new file mode 100644 index 00000000..6a9b54b3 --- /dev/null +++ b/tests/reports/issue39.liq @@ -0,0 +1,119 @@ +[%%version 0.12] + +type token_p = +| Token_info +| Balance of key_hash +| Transfer_token of (key_hash * nat) +| Approve of (key_hash * nat) +| Transfer_token_from_approve_dict of (key_hash * key_hash * nat) + +type token_r = +| General_return of nat +| Token_info_return of nat * nat * string * string +| Balance_return of nat + +type token_contract = (token_p, token_r) contract + +type token = nat +type odd_index = nat +type odd_decimal = nat (* it should be div 1000 *) + +type state = +| Open +| Disabled of string +| Settled + +type info = { + name : string; + created_date : timestamp; + bet_time_range : timestamp * timestamp; + report_time_range : timestamp * timestamp; + odds_lst : string list; +} + +type bookmaker = { + key : key_hash option; + margin : token; + odds : (odd_index, odd_decimal) map; +} + +type storage_t = { + self_key : key_hash; + token_contract : token_contract; + + state : state; + info : info; + bookmaker : bookmaker; + + all_token_amount : token; + all_bets_token_amount: (odd_index, token) map; + orders : (odd_index, (key_hash * odd_decimal * token) list) map; + reports : (key_hash, odd_index) map; + distribution: (key_hash, token) map; +} + +type bet_parameter_t = +| Check +| Override of (key_hash * token) option * storage_t + +type bet_return_t = nat * storage_t + +type mod_parameter_t = key_hash * (token * odd_index * odd_decimal) * storage_t * (bet_parameter_t, bet_return_t) contract + +type return_t = +| Success +| Transfer_fail of nat +| Fail of string + +type parameter_t = (token * odd_index * odd_decimal) * (mod_parameter_t, return_t) contract * (bet_parameter_t, bet_return_t) contract + +let%entry main (parameter : parameter_t) (storage : parameter_t): return_t * parameter_t = + (* let bet_contract = parameter.(2) in + let (result, parameter) = Contract.call bet_contract 0tz parameter Check in *) + + (* let ((token, odd_index, odd_decimal), _, _) = parameter in *) + + let odds_reduce (x : ((odd_index * token) * token)) = + (* let curr_odd_index = x.(0).(0) in + let token = x.(0).(1) in *) + (* let acc_token = x.(1) in *) + (* if curr_odd_index <> 1p then + acc_token + token + else *) + 0p + in + (* let bet_storage = result.(1) in + let bet_tokens = Map.reduce odds_reduce bet_storage.all_bets_token_amount 0p in *) + (* let all_margin = bet_storage.bookmaker.margin + bet_tokens in + let orders_reduce (x : ((key_hash * odd_decimal * token) * token)) = + let odd_decimal = x.(0).(1) in + let token = x.(0).(2) in + let acc_token = x.(1) in + let result = match token * odd_decimal / 1000p with + | None -> 0p + | Some x -> x.(0) + in + acc_token + result + in *) + (* let bet_lst = + let source = Contract.manager (Source : (unit, unit) contract) in + match Map.find odd_index bet_storage.orders with + | None -> [(source, odd_decimal, token)] + | Some x -> (source, odd_decimal, token) :: x + in + let counter_margin = List.reduce orders_reduce bet_lst 0p in *) + Current.fail () + (* if all_margin >= counter_margin then + let source = Contract.manager (Source : (unit, unit) contract) in + let arg = (source, parameter.(0), bet_storage, parameter.(2)) in + let (result, parameter) = Contract.call parameter.(1) 0tz parameter arg in + (result, parameter) + else + (Fail "Insufficient margin", parameter) *) + +(* +with arg + +(Pair (Pair 0 (Pair 0 0)) (Pair "TZ1nk13rZbQ6i1pns7C3V3qpoAfXWEryheLT" "TZ1kjNxXUqvJKRKWFNZtgSCUiPr2GdRkA7cp")) +*) + diff --git a/tests/reverse/test6.tz b/tests/reverse/test6.tz new file mode 100644 index 00000000..90c72b04 --- /dev/null +++ b/tests/reverse/test6.tz @@ -0,0 +1,15 @@ +parameter bool; +return int; +storage int; +code {DUP; CAR; + DIP { CDR; PUSH int 1 }; + # stack is: parameter :: 1 :: storage + IF # if parameter = true + { DROP; DUP; + # stack is storage :: storage + } + { + # stack is 1 :: storage + }; + PAIR; + } diff --git a/tests/test0.liq b/tests/test0.liq index 00759bcb..e55aa4e5 100644 --- a/tests/test0.liq +++ b/tests/test0.liq @@ -1,5 +1,5 @@ -[%%version 0.11] +[%%version 0.13] type storage = string * (* 0: S *) timestamp * (* 1: T *) diff --git a/tests/test1.liq b/tests/test1.liq index 05174679..b6da1be5 100644 --- a/tests/test1.liq +++ b/tests/test1.liq @@ -1,5 +1,5 @@ -[%%version 0.11] +[%%version 0.13] type storage = string * (* 0: S *) timestamp * (* 1: T *) diff --git a/tests/test10.liq b/tests/test10.liq index 1473f848..3eaabd7d 100644 --- a/tests/test10.liq +++ b/tests/test10.liq @@ -1,7 +1,7 @@ (* constructors *) -[%%version 0.11] +[%%version 0.13] type s = bool * diff --git a/tests/test11.liq b/tests/test11.liq index 238dcc0d..4a7133bb 100644 --- a/tests/test11.liq +++ b/tests/test11.liq @@ -1,7 +1,7 @@ (* strings *) -[%%version 0.11] +[%%version 0.13] let%entry main (parameter : string) diff --git a/tests/test12.liq b/tests/test12.liq index 60edd7ac..a0a6c215 100644 --- a/tests/test12.liq +++ b/tests/test12.liq @@ -1,7 +1,7 @@ (* sets *) -[%%version 0.11] +[%%version 0.13] let%entry main (parameter : string) diff --git a/tests/test13.liq b/tests/test13.liq index 7e85401c..dce74d32 100644 --- a/tests/test13.liq +++ b/tests/test13.liq @@ -1,7 +1,7 @@ (* lists *) -[%%version 0.11] +[%%version 0.13] let%entry main (parameter : string) diff --git a/tests/test14.liq b/tests/test14.liq index fd496ccc..7a8d807b 100644 --- a/tests/test14.liq +++ b/tests/test14.liq @@ -1,7 +1,7 @@ (* loops *) -[%%version 0.11] +[%%version 0.13] let%entry main (parameter : int) diff --git a/tests/test15.liq b/tests/test15.liq index 67d58634..fe17817b 100644 --- a/tests/test15.liq +++ b/tests/test15.liq @@ -1,5 +1,5 @@ -[%%version 0.11] +[%%version 0.13] type point = { x : string; y : bool; z : int } type vector = { orig : point; dest : point } diff --git a/tests/test19.liq b/tests/test19.liq index 00fa0063..bf50fada 100644 --- a/tests/test19.liq +++ b/tests/test19.liq @@ -11,6 +11,11 @@ let%entry main storage = (* let c = Current.contract () in *) let key_hash = Crypto.hash_key storage.key in + if key_hash = tz1KqTpEZ7Yob7QbPE4Hy4Wo8fHG8LhKxZSx then + Current.fail (); + if key_hash = + Crypto.hash_key edpkuTXkJDGcFd5nh6VvMz8phXxU3Bi7h6hqgywNFi1vZTfQNnS1RV then + Current.fail (); let manager = Contract.manager (Source : (unit,unit) contract) in let spendable = Crypto.check storage.key (parameter, storage.hash) in let amount = Current.amount () in diff --git a/tests/test2.liq b/tests/test2.liq index 7bdfd79d..2c3c8d74 100644 --- a/tests/test2.liq +++ b/tests/test2.liq @@ -1,5 +1,5 @@ -[%%version 0.11] +[%%version 0.13] type storage = string * (* 0: S *) timestamp * (* 1: T *) diff --git a/tests/test21.liq b/tests/test21.liq new file mode 100644 index 00000000..9290ac28 --- /dev/null +++ b/tests/test21.liq @@ -0,0 +1,14 @@ +[%%version 0.13] + +let%entry main + (parameter : int) + (storage : int) + : nat * int = + + let r = match%nat (parameter + 1) with + | Plus x -> x + 2p + | Minus y -> y + 3p + in + let x = r + 10p in + let storage = abs storage in + (x, storage) diff --git a/tests/test22.liq b/tests/test22.liq new file mode 100644 index 00000000..774fe5ab --- /dev/null +++ b/tests/test22.liq @@ -0,0 +1,19 @@ +[%%version 0.13] + +type t = A of int | B | C of (int * nat) + +let%entry main + (parameter : (unit, unit) contract * t) + (storage : int) + : int * int = + + let (c, m) = parameter in + match m with + | A i -> + (i, storage) + | B -> + let (_, storage) = Contract.call c 0tz storage () in + (0, storage) + | C _ -> + let (_, storage) = Contract.call c 1tz storage () in + (1, storage) diff --git a/tests/test23.liq b/tests/test23.liq new file mode 100644 index 00000000..bacdec0c --- /dev/null +++ b/tests/test23.liq @@ -0,0 +1,16 @@ +[%%version 0.13] + +let%entry main + (parameter : (nat, nat) contract) + (storage : int) + : nat * int = + + let r, storage = match%nat (storage + 1) with + | Plus x -> (x + 2p, storage) + | Minus y -> + let (w, storage) = Contract.call parameter 0tz storage y in + (w, storage) + in + let x = r + 10p in + let storage = abs storage in + (x, storage) diff --git a/tests/test24.liq b/tests/test24.liq new file mode 100644 index 00000000..42539fb9 --- /dev/null +++ b/tests/test24.liq @@ -0,0 +1,20 @@ +[%%version 0.13] + +type t = A of int | B | C of (int * nat) + +let%entry main + (parameter : (unit, unit) contract * t) + (storage : int) + : int * int = + + let (c, m) = parameter in + match m with + | A _ -> + let (_, storage) = Contract.call c 0tz storage () in + (0, storage) + | B -> + let (_, storage) = Contract.call c 0tz storage () in + (0, storage) + | C _ -> + let (_, storage) = Contract.call c 1tz storage () in + (1, storage) diff --git a/tests/test25.liq b/tests/test25.liq new file mode 100644 index 00000000..510233cc --- /dev/null +++ b/tests/test25.liq @@ -0,0 +1,18 @@ +[%%version 0.13] + +let%entry main + (parameter : (nat, nat) contract) + (storage : int) + : nat * int = + + let r, storage = match%nat (storage + 1) with + | Plus x -> + let (w, storage) = Contract.call parameter 0tz storage x in + (w + 2p, storage) + | Minus y -> + let (w, storage) = Contract.call parameter 0tz storage y in + (w, storage) + in + let x = r + 10p in + let storage = abs storage in + (x, storage) diff --git a/tests/test26.liq b/tests/test26.liq new file mode 100644 index 00000000..37755fa9 --- /dev/null +++ b/tests/test26.liq @@ -0,0 +1,14 @@ +[%%version 0.13] + +let%entry main + (parameter : (nat, bool) contract) + (storage : bool) + : bool * bool = + + if + let (b, _) = Contract.call parameter 0tz storage 1p in + b + then + false, false + else + true, false diff --git a/tests/test27.liq b/tests/test27.liq new file mode 100644 index 00000000..74372d6b --- /dev/null +++ b/tests/test27.liq @@ -0,0 +1,13 @@ +[%%version 0.13] + +let%entry main + (parameter : (nat, bool) contract) + (storage : bool * (nat, bool) contract) + : bool * (bool * (nat, bool) contract) = + + let (b, c) = storage in + if b then + false, storage + else + let (b, storage) = Contract.call c 0tz storage 0p in + b, storage diff --git a/tests/test28.liq b/tests/test28.liq new file mode 100644 index 00000000..0d9506e3 --- /dev/null +++ b/tests/test28.liq @@ -0,0 +1,13 @@ +[%%version 0.13] + +let%entry main + (parameter : (nat, bool) contract) + (storage : bool * (nat, bool) contract) + : bool * (bool * (nat, bool) contract) = + + let (b, c) = storage in + if b then + let (b, storage) = Contract.call c 0tz storage 0p in + b, storage + else + false, storage diff --git a/tests/test29.liq b/tests/test29.liq new file mode 100644 index 00000000..13b399f5 --- /dev/null +++ b/tests/test29.liq @@ -0,0 +1,14 @@ +[%%version 0.13] + +let%entry main + (parameter : (int, unit) contract * int list) + (storage : int) + : unit * int = + + let (c, l) = parameter in + match l with + | [] -> + ((), storage) + | x :: _ -> + let (result, storage) = Contract.call c 0tz storage x in + (result, storage) diff --git a/tests/test3.liq b/tests/test3.liq index e5a7b7dd..5b5598a4 100644 --- a/tests/test3.liq +++ b/tests/test3.liq @@ -1,5 +1,5 @@ -[%%version 0.11] +[%%version 0.13] type storage = string * (* 0: S *) timestamp * (* 1: T *) diff --git a/tests/test30.liq b/tests/test30.liq new file mode 100644 index 00000000..79a3476e --- /dev/null +++ b/tests/test30.liq @@ -0,0 +1,14 @@ +[%%version 0.13] + +let%entry main + (parameter : (int, unit) contract * int list) + (storage : int) + : unit * int = + + let (c, l) = parameter in + match l with + | [] -> + let (result, storage) = Contract.call c 0tz storage (-1) in + (result, storage) + | _ :: _ -> + ((), storage) diff --git a/tests/test31.liq b/tests/test31.liq new file mode 100644 index 00000000..11c03e4d --- /dev/null +++ b/tests/test31.liq @@ -0,0 +1,14 @@ +[%%version 0.13] + +let%entry main + (parameter : (int, unit) contract * int option) + (storage : int) + : unit * int = + + let (c, l) = parameter in + match l with + | None -> + ((), storage) + | Some x -> + let (result, storage) = Contract.call c 0tz storage x in + (result, storage) diff --git a/tests/test32.liq b/tests/test32.liq new file mode 100644 index 00000000..d090aee3 --- /dev/null +++ b/tests/test32.liq @@ -0,0 +1,15 @@ +[%%version 0.13] + +type t = A of int | B of (int * ((bool * unit) * nat)) + +let%entry main + (parameter : t) + (storage : int) + : int * int = + + match parameter with + | A i -> + (i, storage) + | B (_, ((b, _), n)) -> + if b then (int n, storage) + else (0, storage) diff --git a/tests/test4.liq b/tests/test4.liq index 50403c77..d2893bad 100644 --- a/tests/test4.liq +++ b/tests/test4.liq @@ -1,5 +1,5 @@ -[%%version 0.11] +[%%version 0.13] type storage = string * (* 0: S *) timestamp * (* 1: T *) (tez * tez) * (* 2: P N *) diff --git a/tests/test5.liq b/tests/test5.liq index dfc078a1..c3c3878e 100644 --- a/tests/test5.liq +++ b/tests/test5.liq @@ -1,5 +1,5 @@ -[%%version 0.11] +[%%version 0.13] type storage = string * (* 0: S *) timestamp * (* 1: T *) diff --git a/tests/test6.liq b/tests/test6.liq index ee343310..950b416e 100644 --- a/tests/test6.liq +++ b/tests/test6.liq @@ -1,5 +1,5 @@ -[%%version 0.11] +[%%version 0.13] type storage = string * (* 0: S *) timestamp * (* 1: T *) diff --git a/tests/test7.liq b/tests/test7.liq index 14ecd25c..e964252f 100644 --- a/tests/test7.liq +++ b/tests/test7.liq @@ -1,5 +1,5 @@ -[%%version 0.11] +[%%version 0.13] type t = tez type s = (t * tez) diff --git a/tests/test8.liq b/tests/test8.liq index 17fe7167..9cfe482a 100644 --- a/tests/test8.liq +++ b/tests/test8.liq @@ -1,11 +1,16 @@ -[%%version 0.11] +[%%version 0.13] let%entry main (parameter : timestamp) (storage : tez * tez (* 2: P N *) ) : unit * (tez * tez) = - let p = get storage 1 in + let p = + if parameter = 2017-10-18 then + storage.(0) + else + storage.(1) + in let storage = set storage 1 p in ( (), storage ) diff --git a/tests/test9.liq b/tests/test9.liq index 9a6eb4a8..3d01cb97 100644 --- a/tests/test9.liq +++ b/tests/test9.liq @@ -1,7 +1,7 @@ (* constants *) -[%%version 0.11] +[%%version 0.13] type storage = bool * int option * diff --git a/tests/test_closure.liq b/tests/test_closure.liq index 81a064ef..4858accd 100644 --- a/tests/test_closure.liq +++ b/tests/test_closure.liq @@ -1,5 +1,5 @@ -[%%version 0.11] +[%%version 0.13] let%entry main (parameter : int) diff --git a/tests/test_closure2.liq b/tests/test_closure2.liq index 454b24c8..b82fa3fa 100644 --- a/tests/test_closure2.liq +++ b/tests/test_closure2.liq @@ -1,5 +1,5 @@ -[%%version 0.11] +[%%version 0.13] let%entry main (parameter : int) diff --git a/tests/test_closure3.liq b/tests/test_closure3.liq index 3ca4f304..141c7f03 100644 --- a/tests/test_closure3.liq +++ b/tests/test_closure3.liq @@ -1,5 +1,5 @@ -[%%version 0.11] +[%%version 0.13] let%entry main (parameter : int) diff --git a/tests/test_extfun.liq b/tests/test_extfun.liq index e78da63c..7c7862f9 100644 --- a/tests/test_extfun.liq +++ b/tests/test_extfun.liq @@ -1,5 +1,5 @@ -[%%version 0.11] +[%%version 0.13] let f ((x : unit), (_ : int) ) = x diff --git a/tests/test_if.liq b/tests/test_if.liq index 8e1a7414..b39c39b1 100644 --- a/tests/test_if.liq +++ b/tests/test_if.liq @@ -1,7 +1,7 @@ (* constants *) -[%%version 0.11] +[%%version 0.13] type storage = bool * diff --git a/tests/test_ifcons.liq b/tests/test_ifcons.liq index 105b4a5f..4ce7d337 100644 --- a/tests/test_ifcons.liq +++ b/tests/test_ifcons.liq @@ -1,7 +1,7 @@ (* lists *) -[%%version 0.11] +[%%version 0.13] let%entry main (parameter : string) diff --git a/tests/test_loop.liq b/tests/test_loop.liq index 541195f7..7a70327a 100644 --- a/tests/test_loop.liq +++ b/tests/test_loop.liq @@ -1,7 +1,7 @@ (* loops *) -[%%version 0.11] +[%%version 0.13] let%entry main (parameter : int) diff --git a/tests/test_map.liq b/tests/test_map.liq index ceedfed8..351cd33d 100644 --- a/tests/test_map.liq +++ b/tests/test_map.liq @@ -1,6 +1,6 @@ (* List.map *) -[%%version 0.11] +[%%version 0.13] let succ (x : int) = x + 1 diff --git a/tests/test_map_closure.liq b/tests/test_map_closure.liq index c322218b..3bde18fa 100644 --- a/tests/test_map_closure.liq +++ b/tests/test_map_closure.liq @@ -1,6 +1,6 @@ (* List.map with closure *) -[%%version 0.1] +[%%version 0.13] let%entry main (parameter : int) diff --git a/tests/test_mapmap_closure.liq b/tests/test_mapmap_closure.liq index 503700cb..6fc5b6bf 100644 --- a/tests/test_mapmap_closure.liq +++ b/tests/test_mapmap_closure.liq @@ -1,4 +1,4 @@ -[%%version 0.11] +[%%version 0.13] let%entry main (parameter : string) (storage : (string, tez) map) diff --git a/tests/test_reduce_closure.liq b/tests/test_reduce_closure.liq index 3ae6dea4..4703c2c8 100644 --- a/tests/test_reduce_closure.liq +++ b/tests/test_reduce_closure.liq @@ -1,6 +1,6 @@ (* loops *) -[%%version 0.1] +[%%version 0.13] let%entry main (parameter : int list) diff --git a/tests/test_rev.liq b/tests/test_rev.liq index 81b036af..4ae06fd5 100644 --- a/tests/test_rev.liq +++ b/tests/test_rev.liq @@ -1,6 +1,6 @@ (* List.rev *) -[%%version 0.11] +[%%version 0.13] let%entry main (parameter : int) diff --git a/tests/test_transfer.liq b/tests/test_transfer.liq index 14ad0b44..b07993d7 100644 --- a/tests/test_transfer.liq +++ b/tests/test_transfer.liq @@ -1,7 +1,7 @@ (* transfers *) -[%%version 0.11] +[%%version 0.13] let%entry main (parameter : (unit,unit) contract) diff --git a/tools/liquidity/build.ocp2 b/tools/liquidity/build.ocp2 index e30dc088..66e32440 100644 --- a/tools/liquidity/build.ocp2 +++ b/tools/liquidity/build.ocp2 @@ -40,7 +40,9 @@ if(with_version){ OCaml.library("ocplib-liquidity", ocaml + { files = [ - + + "iSO8601.ml"; + "liquidVersion.ml", version_info; "liquidMisc.ml"; @@ -53,9 +55,10 @@ OCaml.library("ocplib-liquidity", "liquidEmit.ml"; "liquidPeephole.ml"; + "liquidCheck.ml"; + "liquidEncode.ml"; "liquidMichelson.ml"; "liquidSimplify.ml"; - "liquidCheck.ml"; "liquidClean.ml"; "liquidInterp.ml"; diff --git a/tools/liquidity/env/liquidityEnv.ml b/tools/liquidity/env/liquidityEnv.ml index 5b96026a..fa901f80 100644 --- a/tools/liquidity/env/liquidityEnv.ml +++ b/tools/liquidity/env/liquidityEnv.ml @@ -11,16 +11,40 @@ file that has been correctly typechecked by the `liquidity` typechecker. *) -type timestamp = string -type kind = Tez | Int -type integer = Z.t * kind +exception Fail + +type integer = + Int of Z.t +| Tez of Z.t +| Timestamp of Z.t +type timestamp = integer type tez = integer type nat = integer -type key -type key_hash -type signature + +type key = Key of string +type key_hash = Key_hash of string +type signature = Signature of string + type ('arg, 'res) contract +module Signature : sig + val of_string : string -> signature +end = struct + let of_string s = Signature s +end + +module Key : sig + val of_string : string -> key + end = struct + let of_string s = Key s +end + +module Key_hash : sig + val of_string : string -> key_hash + end = struct + let of_string s = Key_hash s +end + module Tez : sig val of_string : string -> tez @@ -38,7 +62,7 @@ module Tez : sig with Not_found -> Z.of_string s, Z.of_int 0 in - Z.add (Z.mul (Z.of_int 100) tezzies) centiles, Tez + Tez (Z.add (Z.mul (Z.of_int 100) tezzies) centiles) end @@ -48,10 +72,16 @@ module Int : sig end = struct - let of_string n = Z.of_string n, Int + let of_string n = Int (Z.of_string n) end +module Timestamp : sig + val of_string : string -> timestamp +end = struct + let of_string time = assert false +end + module Current : sig val amount : unit -> tez @@ -64,9 +94,9 @@ module Current : sig end = struct - let amount () = Z.of_int 100, Tez - let fail () = assert false (* TODO *) - let time () = assert false (* TODO *) + let amount () = Tez (Z.of_int 100) + let fail () = raise Fail + let time () = Timestamp (Z.of_float (Unix.gettimeofday ())) let balance () = assert false (* TODO *) let gas () = assert false let contract () = assert false @@ -74,6 +104,11 @@ end = struct end +let z_of_int = function + Tez n -> n + | Int n -> n + | Timestamp n -> n + module Array : sig val get : 'a -> integer -> 'b val set : 'a -> integer -> 'b -> 'a @@ -81,12 +116,12 @@ module Array : sig end = struct (* Arrays are for tuples, not typable in OCaml *) let get t n = - let n,_ = n in + let n = z_of_int 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_of_int n in let n = Z.to_int n in let t = Obj.repr t in let t = Obj.dup t in @@ -230,42 +265,96 @@ end type 'key set = 'key Set.set -type int = integer +module Arith : sig -let (+) (x,unit) (y,_) = Z.add x y, unit -let (-) (x,unit) (y,_) = Z.sub x y, unit -let (@) = (^) + val (+) : integer -> integer -> integer + val (-) : integer -> integer -> integer + val ( * ) : integer -> integer -> integer + val ( / ) : integer -> integer -> (integer * integer) option + val int : integer -> integer + val abs : integer -> integer -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 +end = struct -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 + let (+) = Z.add + let (+) x y = + match x,y with + | Timestamp x, Int y + | Int x, Timestamp y + -> Timestamp (x + y) + | Tez x, Tez y -> Tez (x+y) + | Int x, Int y -> Int (x+y) + | Tez _, (Int _|Timestamp _) + | (Int _ | Timestamp _), Tez _ + | Timestamp _, Timestamp _ + -> assert false + + + let (-) = Z.sub + let (-) x y = + match x,y with + | Timestamp x, Timestamp y -> Int (x - y) + | Timestamp x, Int y + -> Timestamp (x - y) + | Tez x, Tez y -> Tez (x-y) + | Int x, Int y -> Int (x-y) + | Tez _, (Int _|Timestamp _) + | (Int _ | Timestamp _), Tez _ + | Int _, Timestamp _ + -> assert false + + let ediv x y = + try + let (q, r) = Z.ediv_rem x y in + Some (q, r) + with _ -> None + let (/) x y = + try + let (q, r) = + let x = z_of_int x in + let y = z_of_int y in + Z.ediv_rem x y in + Some (match x,y with + Tez _, Tez _ -> Int q, Tez r + | Tez _, Int _ -> Tez q, Tez r + | Int _, Int _ -> Int q, Int r + | Int _, Tez _ + | Int _, Timestamp _ + | Tez _, Timestamp _ + | Timestamp _, Tez _ + | Timestamp _, Int _ + | Timestamp _, Timestamp _ + -> assert false + ) + with _ -> None + + let ( * ) = Z.mul + let ( * ) x y = + match x,y with + | Tez x, Int y + | Int x, Tez y -> Tez (x * y) + | Int x, Int y -> Int (x * y) + | Tez _, Tez _ + | Int _, Timestamp _ + | Tez _, Timestamp _ + | Timestamp _, Tez _ + | Timestamp _, Int _ + | Timestamp _, Timestamp _ + -> assert false + + let int x = x + + let abs = function Int x -> Int (Z.abs x) + | Tez _ + | Timestamp _ -> assert false + +end + +let (@) = (^) + +include Arith module Lambda : sig val pipe : 'a -> ('a -> 'b) -> 'b @@ -282,8 +371,6 @@ end = struct else ret end -let int x = x - module Contract : sig val call : ('arg, 'res) contract -> tez -> 'storage -> 'arg -> @@ -313,7 +400,7 @@ 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 + val size : 'a list -> integer end = struct @@ -325,7 +412,7 @@ end = struct let map = List.map let rev = List.rev - let size list = Z.of_int (List.length list), Int + let size list = Int (Z.of_int (List.length list)) end @@ -347,3 +434,5 @@ end = struct let hash_key _ = assert false (*TODO *) let check _key (_sig, _hash) = assert false (* TODO *) end + +type int = integer diff --git a/tools/liquidity/iSO8601.ml b/tools/liquidity/iSO8601.ml new file mode 100644 index 00000000..31122fba --- /dev/null +++ b/tools/liquidity/iSO8601.ml @@ -0,0 +1,31 @@ +(**************************************************************************) +(* *) +(* Copyright (c) 2017 . *) +(* Fabrice Le Fessant, OCamlPro SAS *) +(* *) +(* All rights reserved. No warranty, explicit or implicit, provided. *) +(* *) +(**************************************************************************) + +let cut_at s c = + try + let pos = String.index s c in + String.sub s 0 pos, + Some (String.sub s (pos+1) (String.length s - pos -1)) + with Not_found -> s, None + +let of_string s = + let date, hour = cut_at s 'T' in + let hour, timezone = + match hour with + | None -> "00:00:00", "00:00" + | Some s -> + let hour, timezone = cut_at s '+' in + let hour = if String.length hour = 5 then hour ^ ":00" else hour in + let timezone = match timezone with + None -> "00:00" + | Some timezone -> timezone + in + (hour, timezone) + in + Printf.sprintf "%sT%s+%s" date hour timezone diff --git a/tools/liquidity/liquidBoundVariables.ml b/tools/liquidity/liquidBoundVariables.ml index dc8a8414..d3cd8f66 100644 --- a/tools/liquidity/liquidBoundVariables.ml +++ b/tools/liquidity/liquidBoundVariables.ml @@ -60,6 +60,12 @@ let rec bv code = (StringSet.union (bv ifnone) (StringSet.remove some_pat (bv ifsome))) + | MatchNat (exp, loc, p, ifplus, m, ifminus) -> + StringSet.union (bv exp) + (StringSet.union + (StringSet.remove m (bv ifminus)) + (StringSet.remove p (bv ifplus))) + | MatchList (exp, loc, head_pat, tail_pat, ifcons, ifnil) -> StringSet.union (bv exp) @@ -95,6 +101,14 @@ let rec bv code = | Constructor (_loc, _lid, arg) -> bv arg + | And (_loc, a1, a2) | Or (_loc, a1, a2) + | Implies (_loc, a1, a2) | Equiv (_loc, a1, a2) -> + StringSet.union (bv a1) (bv a2) + + | Forall (_, vars, body) | Exists (_, vars, body) -> + List.fold_left (fun bvs (v, _) -> StringSet.remove v bvs) + (bv body) vars + | MatchVariant (exp, _loc, args) -> StringSet.union (bv exp) (List.fold_left (fun set (pat, exp) -> @@ -109,7 +123,7 @@ let rec bv code = StringSet.union set bv_case ) StringSet.empty args) -let mk desc exp bv = { desc; ty = exp.ty; bv; fail = exp.fail } +let mk desc exp bv = { exp with desc; bv } let rec bound code = match code.desc with @@ -208,6 +222,20 @@ let rec bound code = let desc = MatchOption(exp,loc,ifnone, some_pat, ifsome) in mk desc code bv + + | MatchNat (exp, loc, p, ifplus, m, ifminus) -> + let exp = bound exp in + let ifplus = bound ifplus in + let ifminus = bound ifminus in + let bv = + StringSet.union exp.bv + (StringSet.union + (StringSet.remove m ifminus.bv) + (StringSet.remove p ifplus.bv)) + in + let desc = MatchNat (exp, loc, p, ifplus, m, ifminus) in + mk desc code bv + | MatchList (exp, loc, head_pat, tail_pat, ifcons, ifnil) -> let exp = bound exp in let ifnil = bound ifnil in @@ -279,6 +307,31 @@ let rec bound code = let desc = Constructor(loc,lid,arg) in mk desc code arg.bv + | And (loc, a1, a2) | Or (loc, a1, a2) + | Implies (loc, a1, a2) | Equiv (loc, a1, a2) -> + let a1 = bound a1 in + let a2 = bound a2 in + let desc = match code.desc with + | And _ -> And (loc, a1, a2) + | Or _ -> Or (loc, a1, a2) + | Implies _ -> Implies (loc, a1, a2) + | Equiv _ -> Equiv (loc, a1, a2) + | _ -> assert false + in + mk desc code (StringSet.union a1.bv a2.bv) + + | Forall (loc, vars, body) | Exists (loc, vars, body) -> + let body = bound body in + let bv = + List.fold_left (fun bvs (v, _) -> StringSet.remove v bvs) + body.bv vars in + let desc = match code.desc with + | Forall _ -> Forall (loc, vars, body) + | Exists _ -> Exists (loc, vars, body) + | _ -> assert false + in + mk desc code bv + | MatchVariant (exp, loc, args) -> let exp = bound exp in let args = diff --git a/tools/liquidity/liquidBoundVariables.mli b/tools/liquidity/liquidBoundVariables.mli index b72f9054..e147492d 100644 --- a/tools/liquidity/liquidBoundVariables.mli +++ b/tools/liquidity/liquidBoundVariables.mli @@ -10,6 +10,6 @@ open LiquidTypes (* Compute free variables of an expression *) -val bound_contract : 'a exp contract -> 'a exp contract -val bound : 'a exp -> 'a exp -val bv : 'a exp -> StringSet.t +val bound_contract : (('a, 'b) exp, 'c) contract -> (('a, 'b) exp, 'c) contract +val bound : ('a, 'b) exp -> ('a, 'b) exp +val bv : ('a, 'b) exp -> StringSet.t diff --git a/tools/liquidity/liquidCheck.ml b/tools/liquidity/liquidCheck.ml index c6e58386..5edc810c 100644 --- a/tools/liquidity/liquidCheck.ml +++ b/tools/liquidity/liquidCheck.ml @@ -36,65 +36,29 @@ let error loc msg = LiquidLoc.raise_error ~loc ("Type error: " ^^ msg ^^ "%!") let comparable_ty ty1 ty2 = - match ty1, ty2 with - | (Tint|Tnat|Ttez), (Tint|Tnat|Ttez) - | Ttimestamp, Ttimestamp - | Tstring, Tstring - | Tkey_hash, Tkey_hash -> true + match get_type ty1, get_type ty2 with + | (Tint|Tnat), (Tint|Tnat) + | Ttez, Ttez + | Ttimestamp, Ttimestamp + | Tstring, Tstring + | Tkey_hash, Tkey_hash -> true | _ -> false let error_not_comparable loc prim ty1 ty2 = error loc "arguments of %s not comparable: %s\nwith\n%s\n" (LiquidTypes.string_of_primitive prim) - (LiquidPrinter.Michelson.string_of_type ty1) - (LiquidPrinter.Michelson.string_of_type ty2) - -let mk = - let bv = StringSet.empty in - fun desc (ty : datatype) fail -> { desc; ty; bv; fail } - -let mk_nat i = - mk (Const (Tnat, CNat (LiquidPrinter.integer_of_int i))) Tnat false - -let mk_nil list_ty = - mk (Const (list_ty, CList [])) list_ty false - -let mk_tuple loc l fail = - let tuple_ty = Ttuple (List.map (fun t -> t.ty) l) in - mk (Apply (Prim_tuple, loc, l)) tuple_ty fail - -let const_unit = mk (Const (Tunit, CUnit)) Tunit false - -let const_true = mk (Const (Tbool, CBool true)) Tbool false - -let const_false = mk (Const (Tbool, CBool false)) Tbool false - -let mk_untyped = - let bv = StringSet.empty in - fun desc -> { desc; ty = (); bv; fail = false } - -let untyped_int i = - mk_untyped (Const (Tint, CInt (LiquidPrinter.integer_of_int i))) - -let untyped_nil list_ty = - mk_untyped (Const (list_ty, CList [])) - -let mk_untyped_tuple loc l = - mk_untyped (Apply (Prim_tuple, loc, l)) - -let unused env ty = - mk (Apply(Prim_unused, noloc env, [const_unit])) ty false + (LiquidPrinter.Liquid.string_of_type_expl ty1) + (LiquidPrinter.Liquid.string_of_type_expl ty2) let uniq_ident env name = env.counter := !(env.counter) + 1; Printf.sprintf "%s/%d" name !(env.counter) let new_binding env name ty = - let new_name = uniq_ident env name in let count = ref 0 in let env = { env with - vars = StringMap.add name (new_name, ty, count) env.vars } in - (new_name, env, count) + vars = StringMap.add name (name, ty, count) env.vars } in + (env, count) let check_used env name loc count = if env.warnings && !count = 0 && name.[0] <> '_' then begin @@ -115,96 +79,19 @@ let check_used_in_env env name loc = with Not_found -> check_used env name loc (ref 0) +let check_specs_allowed env loc = + if not env.allow_spec then + error loc "logic specification is not allowed in programs" + (* Find variable name in either the global environment or the closure environment, returns a corresponding variable expression *) let find_var ?(count_used=true) env loc name = try let (name, ty, count) = StringMap.find name env.vars in if count_used then incr count; - mk (Var (name, loc, [])) ty false + mk (Var (name, loc, [])) ty with Not_found -> - match env.clos_env with - | None -> error loc "unbound variable %S" name - | Some ce -> - try - let v, (cpt_in, cpt_out) = StringMap.find name ce.env_bindings in - if count_used then begin - incr cpt_in; - incr cpt_out; - end; - v - with Not_found -> - error loc "unbound variable %S" name - -(* Create environment for closure *) -let env_for_clos env loc bvs arg_name arg_type = - let _, free_vars = StringSet.fold (fun v (index, free_vars) -> - try - let index = index + 1 in - match env.clos_env with - | None -> - let (bname, btype, cpt_out) = StringMap.find v env.vars in - (index, - StringMap.add v (bname, btype, index, (ref 0, cpt_out)) free_vars) - | Some ce -> - let bname, btype, _, (cpt_in, cpt_out) = - StringMap.find v ce.env_vars in - (index, - StringMap.add v (bname, btype, index, (cpt_in, cpt_out)) free_vars) - with Not_found -> - (index, free_vars) - ) bvs (0, StringMap.empty) - in - let free_vars_l = - StringMap.bindings free_vars - |> List.sort (fun (_, (_,_,i1,_)) (_, (_,_,i2,_)) -> compare i1 i2) - in - let ext_env = env in - let env = { env with vars = StringMap.empty } in - match free_vars_l with - | [] -> (* no closure environment *) - let (new_name, env, _) = new_binding env arg_name arg_type in - env, new_name, arg_type, [] - | _ -> - let env_arg_name = uniq_ident env "closure_env" in - let env_arg_type = - Ttuple (arg_type :: List.map (fun (_, (_,ty,_,_)) -> ty) free_vars_l) in - let env_arg_var = mk (Var (env_arg_name, loc, [])) env_arg_type false in - let new_name = uniq_ident env arg_name in - let env_vars = - StringMap.add arg_name - (new_name, arg_type, 0, (ref 0, ref 0)) free_vars in - let size = StringMap.cardinal env_vars in - let env_bindings = - StringMap.map (fun (_, ty, index, count) -> - let ei = mk_nat index in - let accessor = - if index + 1 = size then Prim_tuple_get_last - else Prim_tuple_get in - let exp = mk (Apply(accessor, loc, [env_arg_var; ei])) ty false in - exp, count - ) env_vars - in - let call_bindings = List.map (fun (name, _) -> - name, find_var ~count_used:false ext_env loc name - ) free_vars_l - in - (* Format.eprintf "--- Closure %s ---@." env_arg_name; *) - (* StringMap.iter (fun name (e,_) -> *) - (* Format.eprintf "%s -> %s@." *) - (* name (LiquidPrinter.Liquid.string_of_code e) *) - (* ) env_bindings; *) - let env_closure = { - env_vars; - env_bindings; - call_bindings; - } in - let env = - { env with - clos_env = Some env_closure - } - in - env, env_arg_name, env_arg_type, call_bindings + error loc "unbound variable %S" name let maybe_reset_vars env transfer = if transfer then @@ -214,17 +101,11 @@ let maybe_reset_vars env transfer = } else env -let fprint_2types fmt (ty1, ty2) = - Format.fprintf fmt "First type:\n %s\n" - (LiquidPrinter.Liquid.string_of_type ty1); - Format.fprintf fmt "Second type:\n %s" - (LiquidPrinter.Liquid.string_of_type ty2) - let type_error loc msg actual expected = error loc "%s.\nExpected type:\n %s\nActual type:\n %s" msg - (LiquidPrinter.Liquid.string_of_type expected) - (LiquidPrinter.Liquid.string_of_type actual) + (LiquidPrinter.Liquid.string_of_type_expl expected) + (LiquidPrinter.Liquid.string_of_type_expl actual) let error_prim loc prim args expected_args = @@ -237,12 +118,12 @@ let error_prim loc prim args expected_args = else let args = List.map (fun { ty } -> ty) args in List.iteri (fun i (arg, expected) -> - if arg <> expected then + if not (eq_types 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) + (LiquidPrinter.Liquid.string_of_type_expl expected) + (LiquidPrinter.Liquid.string_of_type_expl arg) ) (List.combine args expected_args); Printf.eprintf "Fatal error on typechecking primitive %S\n%!" prim; @@ -252,207 +133,183 @@ let error_prim loc prim args expected_args = (* approximate location *) let rec loc_exp env e = match e.desc with | Var (_, loc, _) - | SetVar (_, loc, _, _) - | Apply (_, loc, _) - | LetTransfer (_, _, loc, _, _, _, _, _) - | MatchOption (_, loc, _, _, _) - | MatchList (_, loc, _, _, _, _) - | Loop (_, loc, _, _) - | Lambda (_, _, loc, _, _) - | Closure (_, _, loc, _, _, _) - | Record (loc, _) - | Constructor (loc, _, _) - | MatchVariant (_, loc, _) -> loc + | SetVar (_, loc, _, _) + | Apply (_, loc, _) + | LetTransfer (_, _, loc, _, _, _, _, _) + | MatchOption (_, loc, _, _, _) + | MatchNat (_, loc, _, _, _, _) + | MatchList (_, loc, _, _, _, _) + | Loop (_, loc, _, _) + | Lambda (_, _, loc, _, _) + | Closure (_, _, loc, _, _, _) + | Record (loc, _) + | Constructor (loc, _, _) + | MatchVariant (_, loc, _) + | And (loc, _, _) + | Or (loc, _, _) + | Implies (loc, _, _) + | Equiv (loc, _, _) + | Forall (loc, _, _) + | Exists (loc, _, _) -> loc | Let (_, _, _, e) -> loc_exp env e | Const _ -> noloc env | If (e1, _, e2) - | Seq (e1, e2) -> - match loc_exp env e1, loc_exp env e2 with - | ({ loc_pos = Some ( loc_begin , _ ) } as loc), - { loc_pos = Some ( _, loc_end ) } -> - { loc with loc_pos = Some (loc_begin, loc_end) } - | loc, _ -> loc + | Seq (e1, e2) -> + match loc_exp env e1, loc_exp env e2 with + | ({ loc_pos = Some ( loc_begin , _ ) } as loc), + { loc_pos = Some ( _, loc_end ) } -> + { loc with loc_pos = Some (loc_begin, loc_end) } + | loc, _ -> loc (* this function returns a triple with * the expression annotated with its type * whether the expression can fail * whether the expression performs a TRANSFER_TOKENS *) -let rec typecheck env ( exp : LiquidTypes.syntax_exp ) = +let rec typecheck env ( exp : syntax_exp ) : typed_exp = match exp.desc with - | Const (ty, cst ) -> - let desc = Const (ty, cst ) in - let fail = false in - mk desc ty fail, fail, false + | Const (ty, cst) -> + mk (Const (ty, cst)) ty | 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 + let exp = typecheck env exp in + if eq_types exp.ty Tfail then error loc "cannot assign failure"; + let env = maybe_reset_vars env exp.transfer in + let (env, count) = new_binding env name exp.ty in + let body = typecheck env body in + let desc = Let (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) } + mk desc body.ty + + | Var (name, loc, (_::_ as labels)) -> + begin match find_var env loc name with + | { desc = Var (name, _, []); ty } -> + let ty = + List.fold_left (fun ty label -> + match get_type ty with + | Trecord ltys -> + begin try + let _, _, ty = StringMap.find label env.env.labels in + let ty' = List.assoc label ltys in + if not (eq_types ty ty') then + error loc "label for wrong record"; + ty' + with Not_found -> error loc "bad label" + end + | _ -> error loc "not a record : %s" + (LiquidPrinter.Liquid.string_of_type_expl ty) + ) ty labels + in + mk (Var (name, loc, labels)) ty + | _ -> assert false + end + + | Var (name, loc, labels) -> find_var env loc name + + | SetVar (name, loc, [], e) -> + let e = typecheck env e in + mk (SetVar (name, loc, [], e)) e.ty + + | SetVar (name, loc, ((l :: _) as labels), arg) -> + (* let arg = typecheck env arg in *) + let { ty } = find_var env loc name in + (* let label_types = match get_type ty with *) + (* | Trecord label_types -> label_types *) + (* | _ -> error loc "not a record %s" *) + (* (LiquidPrinter.Liquid.string_of_type_expl ty) *) + (* in *) + (* let lty = *) + (* try List.assoc l label_types *) + (* with Not_found -> *) + (* error loc "label %s does not belong to type %s" l *) + (* (LiquidPrinter.Liquid.string_of_type_expl ty) *) + (* in *) + let exp_ty = + List.fold_left (fun lty label -> + let ty_name, _, ty = + try StringMap.find label env.env.labels + with Not_found -> error loc "unbound label %S" label 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 + let record_ty = StringMap.find ty_name env.env.types in + if not (eq_types lty record_ty) then + error loc "label %s does not belong to type %s" l + (LiquidPrinter.Liquid.string_of_type_expl lty); + ty + ) ty labels + in + let arg = typecheck_expected "set" env exp_ty arg in + mk (SetVar (name, loc, labels, arg)) ty | 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 + let exp1 = typecheck_expected "sequence" env Tunit exp1 in + let exp2 = typecheck env exp2 in + let desc = Seq (exp1, exp2) in + (* TODO: if not fail1 then remove exp1 *) + mk desc exp2.ty | If (cond, ifthen, ifelse) -> - let cond, fail1, transfer1 = + let cond = 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 = + let ifthen = typecheck env ifthen in + let ifelse, ty = if ifthen.ty = Tfail then - let ifelse, fail3, transfer3 = typecheck env ifelse in - ifelse, fail3, transfer3, ifelse.ty + let ifelse = typecheck env ifelse in + ifelse, ifelse.ty else - let ifelse, fail3, transfer3 = + let ifelse = typecheck_expected "if-result" env ifthen.ty ifelse in - ifelse, fail3, transfer3, ifthen.ty + ifelse, 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 + mk desc ty | 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 + let tez_exp = typecheck_expected "call-amount" env Ttez tez_exp in + let contract_exp = 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 = + let arg_exp = typecheck_expected "call-arg" env arg_ty arg_exp in + let storage_exp = typecheck_expected "call-storage" - env env.contract.storage storage_exp in - if transfer1 || transfer2 || transfer3 || transfer4 then + env env.contract.storage storage_exp in + if tez_exp.transfer || contract_exp.transfer + || arg_exp.transfer || storage_exp.transfer then error loc "transfer within transfer arguments"; - let (new_storage, env, storage_count) = + let (env, storage_count) = new_binding env storage_name env.contract.storage in - let (new_result, env, result_count) = + let (env, result_count) = new_binding env result_name return_ty in - let body, fail5, transfer5 = typecheck env body in + let body = 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, + let desc = LetTransfer(storage_name, result_name, 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%!" + mk desc body.ty + | ty -> + error (loc_exp env contract_exp) + "Bad contract type.\nExpected type:\n ('a, 'b) contract\n\ + Actual type:\n %s" + (LiquidPrinter.Liquid.string_of_type_expl ty) end + | Apply (Prim_unknown, loc, + ({ desc = Var ("old", varloc, [])} :: [arg])) + when env.allow_spec && env.in_post -> + let exp = typecheck env arg in + mk (Apply (Prim_old, loc, [exp])) exp.ty + | Apply (Prim_unknown, loc, ({ desc = Var (name, varloc, [])} as f) :: ((_ :: _) as r)) when StringMap.mem name env.vars -> @@ -463,10 +320,16 @@ let rec typecheck env ( exp : LiquidTypes.syntax_exp ) = 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]) } + ({ desc = Var ("Contract.call", varloc, [])} :: args)) -> + let nb_args = List.length args in + if nb_args <> 4 then + error loc + "Contract.call expects 4 arguments, it was given %d arguments." + nb_args + else + error loc + "The result of Contract.call must be bound under a \ + \"let (result, storage) =\" directly." | Apply (Prim_unknown, loc, ({ desc = Var (name, varloc, [])} ::args)) -> @@ -484,448 +347,212 @@ let rec typecheck env ( exp : LiquidTypes.syntax_exp ) = 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" + let arg = typecheck env arg in + let arg_ty = match get_type arg.ty with + | Tfail -> error loc "cannot match failure" | Toption ty -> ty - | _ -> - error loc "not an option type" + | _ -> 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 + let env = maybe_reset_vars env arg.transfer in + let ifnone = typecheck env ifnone in + let (env, count) = new_binding env name arg_ty in + let ifsome = typecheck env ifsome in check_used env name loc count; - let desc = MatchOption (arg, loc, ifnone, new_name, ifsome ) in + let desc = MatchOption (arg, loc, ifnone, name, ifsome ) in let ty = - match ifnone.ty, ifsome.ty with - | ty, Tfail - | Tfail, ty -> ty + match get_type ifnone.ty, get_type 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 + mk desc ty + + | MatchNat (arg, loc, plus_name, ifplus, minus_name, ifminus) -> + let arg = typecheck_expected "match%nat" env Tint arg in + let env = maybe_reset_vars env arg.transfer in + let (env2, count_p) = new_binding env plus_name Tnat in + let ifplus = typecheck env2 ifplus in + let (env3, count_m) = new_binding env minus_name Tnat in + let ifminus = typecheck env3 ifminus in + check_used env plus_name loc count_p; + check_used env minus_name loc count_m; + let desc = MatchNat (arg, loc, plus_name, ifplus, minus_name, ifminus) in + let ty = + match get_type ifplus.ty, get_type ifminus.ty with + | ty, Tfail | Tfail, ty -> ty + | ty1, ty2 -> + if ty1 <> ty2 then + type_error loc "branches of match%nat must have the same type" + ty2 ty1; + ty1 + in + mk desc ty | 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 + let arg = typecheck env arg in + if get_type arg.ty = Tfail then error loc "loop arg is a failure"; + let env = maybe_reset_vars env arg.transfer in + let (env, count) = new_binding env name arg.ty in + let body = + 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 + mk (Loop (name, loc, body, arg)) arg.ty | 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" + let arg = typecheck env arg in + let arg_ty = match get_type arg.ty with + | Tfail -> error loc "cannot match failure" | Tlist ty -> ty - | _ -> - error loc "not a list type" + | _ -> 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 + let env = maybe_reset_vars env arg.transfer in + let ifnil = typecheck env ifnil in + let (env, count) = new_binding env head_name arg_ty in + let (env, count) = new_binding env tail_name (Tlist arg_ty) in + let ifcons = 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 desc = MatchList (arg, loc, head_name, tail_name, ifcons, ifnil) in let ty = - match ifnil.ty, ifcons.ty with - | ty, Tfail - | Tfail, ty -> ty + match get_type ifnil.ty, get_type 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 + mk desc ty | 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 = - env_for_clos env loc bvs arg_name arg_type in - let body, _fail, transfer = typecheck env body in - if transfer then - error loc "no transfer in closure"; - (* begin match env.clos_env with *) - (* | None -> () *) - (* | Some clos_env -> *) - (* Format.eprintf "--- Closure %s (real:%b)---@." arg_name is_real_closure; *) - (* StringMap.iter (fun name (e, (cpt_in, cpt_out)) -> *) - (* Format.eprintf "%s -> %s , (%d, %d)@." *) - (* name (LiquidPrinter.Liquid.string_of_code e) !cpt_in !cpt_out *) - (* ) clos_env.env_bindings *) - (* end; *) - check_used_in_env env lambda_arg_name loc; - let desc = - Closure (arg_name, arg_type, loc, call_env, body, body.ty) in - let call_env_type = match call_env with - | [] -> assert false - | [_, t] -> t.ty - | _ -> Ttuple (List.map (fun (_, t) -> t.ty) call_env) - in - let ty = Tclosure ((lambda_arg_type, call_env_type), body.ty) in - mk desc ty false, false, false + let lambda_arg_type = arg_type in + let lambda_arg_name = arg_name in + let lambda_body = body in + assert (res_type = Tunit); + (* allow closures at typechecking, do not reset env *) + let (env, arg_count) = new_binding env lambda_arg_name lambda_arg_type in + let body = typecheck env lambda_body in + if body.transfer then error loc "no transfer in lambda"; + check_used env lambda_arg_name loc arg_count; + let desc = Lambda (arg_name, lambda_arg_type, loc, body, body.ty) in + let ty = Tlambda (lambda_arg_type, body.ty) in + mk desc ty | 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 + 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 + let record_ty = StringMap.find ty_name env.env.types in + let remaining_labels = match record_ty with + | Trecord rtys -> List.map fst rtys |> StringSet.of_list |> ref + | _ -> assert false in + let lab_exp = List.map (fun (label, exp) -> + let ty_name', _, ty = try StringMap.find label env.env.labels - with Not_found -> - error loc "unbound label %S" label + 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 + if ty_name <> ty_name' then error loc "inconsistent list of labels"; + let exp = typecheck_expected ("label "^ label) env ty exp in + if exp.transfer then error loc "transfer not allowed in record"; + remaining_labels := StringSet.remove label !remaining_labels; + (label, exp) + ) lab_x_exp_list in + if not (StringSet.is_empty !remaining_labels) then + error loc "label %s is not defined" (StringSet.choose !remaining_labels); 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 + mk (Record (loc, lab_exp)) ty | 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 + let arg = typecheck_expected "constr-arg" env arg_ty arg in + if arg.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 - in - iter constrs - in - mk exp.desc (Ttype (ty_name, constr_ty)) can_fail, can_fail, false + let constr_ty = StringMap.find ty_name env.env.types in + let ty = Ttype (ty_name, constr_ty) in + mk (Constructor(loc, Constr constr, arg)) ty | Constructor(loc, Left right_ty, arg) -> - let arg, can_fail, transfer = typecheck env arg in - if transfer then + let arg = typecheck env arg in + if arg.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 + let ty = Tor (arg.ty, right_ty) in + mk (Constructor(loc, Left right_ty, arg)) ty | Constructor(loc, Right left_ty, arg) -> - let arg, can_fail, transfer = typecheck env arg in - if transfer then + let arg = typecheck env arg in + if arg.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 + let ty = Tor (left_ty, arg.ty) in + mk (Constructor(loc, Right left_ty, arg)) ty + + | Constructor(loc, Source (from_ty, to_ty), arg) -> + let arg = typecheck env arg in + let ty = Tcontract(from_ty, to_ty) in + mk (Constructor(loc, Source (from_ty, to_ty), arg)) ty + + | And (loc, e1, e2) | Or (loc, e1, e2) + | Implies (loc, e1, e2) | Equiv (loc, e1, e2) -> + check_specs_allowed env loc; + let e1 = typecheck_expected "logic" env Tbool e1 in + let e2 = typecheck_expected "logic" env Tbool e2 in + if e1.transfer || e2.transfer then + error loc "transfer not allowed in specification"; + if e1.fail || e2.fail then + error loc "expressions in specifications cannot fail"; + let desc = match exp.desc with + | And _ -> And (loc, e1, e2) + | Or _ -> Or (loc, e1, e2) + | Implies _ -> Implies (loc, e1, e2) + | Equiv _ -> Equiv (loc, e1, e2) + | _ -> assert false + in + mk desc Tbool + + | Forall (loc, qvs, e) | Exists (loc, qvs, e) -> + check_specs_allowed env loc; + let env = List.fold_left (fun env (v, ty) -> + new_binding env v ty |> fst + ) env qvs + in + let e = typecheck_expected "logic" env Tbool e in + if e.transfer then + error loc "transfer not allowed in specification"; + if e.fail then + error loc "expressions in specifications cannot fail"; + let desc = match exp.desc with + | Forall _ -> Forall (loc, qvs, e) + | Exists _ -> Exists (loc, qvs, e) + | _ -> assert false + in + mk desc Tbool | MatchVariant (arg, loc, cases) -> - let arg, can_fail, transfer1 = typecheck env arg in - let ty_name, constrs, is_left_right = + let arg = typecheck env arg in + let constrs, is_left_right = try - match arg.ty with + match get_type 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 + | Tsum constrs -> + (List.map fst constrs, None) | 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)) + (["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) + (LiquidPrinter.Liquid.string_of_type_expl arg.ty) in - let env = maybe_reset_vars env transfer1 in - let match_can_fail = ref can_fail in + let env = maybe_reset_vars env arg.transfer 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 @@ -942,7 +569,7 @@ let rec typecheck env ( exp : LiquidTypes.syntax_exp ) = 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; + (LiquidPrinter.Liquid.string_of_type arg.ty); let cases = List.map (fun (constr, vars, e) -> let var_ty = match is_left_right, constr with @@ -954,45 +581,44 @@ let rec typecheck env ( exp : LiquidTypes.syntax_exp ) = try StringMap.find constr env.env.constrs with Not_found -> error loc "unknown constructor %S" constr in - if ty_name <> ty_name' then error loc "inconsistent constructors"; + (* if ty_name <> ty_name' then error loc "inconsistent constructors"; *) var_ty in - let name = + let env, count_opt = match vars with - | [] -> "_" - | [ var ] -> var + | [] -> env, None + | [ var ] -> + let (env, count) = new_binding env var var_ty in + env, Some count | _ -> error loc "cannot deconstruct constructor args" in - let (new_name, env, count) = - new_binding env name var_ty in - let (e, can_fail, transfer) = + let e = 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 + let e = typecheck env e in + begin match e.ty with | Tfail -> () | _ -> expected_type := Some e.ty end; - (e, can_fail, transfer) + e 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) + begin match vars, count_opt with + | [name], Some count -> check_used env name loc count + | _ -> () + end; + (CConstr (constr, vars), e) ) cases in - let desc = MatchVariant (arg, loc, cases ) 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 + mk desc ty and find_case loc env constr cases = match List.find_all (function @@ -1010,16 +636,16 @@ and find_case loc env constr cases = | 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 }; + | Prim_tuple_get, [ { ty = tuple_ty }; { desc = Const (_, (CInt n | CNat n)) }] -> + let tuple = match (get_type tuple_ty) with + | Ttuple tuple -> tuple + | Trecord rtys -> List.map snd rtys + | _ -> error loc "get takes a tuple as first argument, got:\n%s" + (LiquidPrinter.Liquid.string_of_type_expl tuple_ty) + in let n = LiquidPrinter.int_of_integer n in let size = List.length tuple in let prim = @@ -1034,9 +660,15 @@ and typecheck_prim1 env prim loc args = let ty = List.nth tuple n in prim, ty - | Prim_tuple_set, [ { ty = Ttuple tuple }; + | Prim_tuple_set, [ { ty = tuple_ty }; { desc = Const (_, (CInt n | CNat n)) }; { ty } ] -> + let tuple = match (get_type tuple_ty) with + | Ttuple tuple -> tuple + | Trecord rtys -> List.map snd rtys + | _ -> error loc "set takes a tuple as first argument, got:\n%s" + (LiquidPrinter.Liquid.string_of_type_expl tuple_ty) + in let n = LiquidPrinter.int_of_integer n in let expected_ty = List.nth tuple n in let size = List.length tuple in @@ -1049,9 +681,9 @@ and typecheck_prim1 env prim loc args = else Prim_tuple_set in - let ty = if ty <> expected_ty && ty <> Tfail then + let ty = if not (eq_types ty expected_ty || eq_types ty Tfail) then error loc "prim set bad type" - else Ttuple tuple + else tuple_ty in prim, ty @@ -1079,135 +711,132 @@ and typecheck_prim1 env prim loc args = prim, typecheck_prim2 env prim loc args and typecheck_prim2 env prim loc args = - match prim, args with + match prim, List.map (fun a -> get_type a.ty) args with | ( Prim_neq | Prim_lt | Prim_gt | Prim_eq | Prim_le | Prim_ge ), - [ { ty = ty1 }; { ty = ty2 } ] -> + [ ty1; ty2 ] -> if comparable_ty ty1 ty2 then Tbool else error_not_comparable loc prim ty1 ty2 | Prim_compare, - [ { ty = ty1 }; { ty = ty2 } ] -> + [ ty1; 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; (Ttez | Tint | Tnat) ] + | [ (Tint | Tnat); 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 + | (Prim_add|Prim_mul), [ Tnat; Tnat ] -> Tnat + | (Prim_add|Prim_sub|Prim_mul), [ (Tint|Tnat); + (Tint|Tnat) ] -> Tint + | Prim_add, [ Ttimestamp; Tint|Tnat ] -> Ttimestamp + | Prim_add, [ Tint|Tnat; Ttimestamp ] -> Ttimestamp (* TODO: improve types of ediv in Michelson ! *) - | Prim_ediv, [ { ty = Tnat }; { ty = Tnat } ] -> + | Prim_ediv, [ Tnat; Tnat ] -> Toption (Ttuple [Tnat; Tnat]) - | Prim_ediv, [ { ty = Tint|Tnat }; { ty = Tint|Tnat } ] -> + | Prim_ediv, [ Tint|Tnat; Tint|Tnat ] -> Toption (Ttuple [Tint; Tnat]) - | Prim_ediv, [ { ty = Ttez }; { ty = Tnat } ] -> + | Prim_ediv, [ Ttez; 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, [ Tbool; Tbool ] -> Tbool + | Prim_or, [ Tbool; Tbool ] -> Tbool + | Prim_and, [ Tbool; Tbool ] -> Tbool + | Prim_not, [ 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_xor, [ Tnat; Tnat ] -> Tnat + | Prim_xor, [ Tint|Tnat; Tint|Tnat ] -> Tint + | Prim_or, [ Tnat; Tnat ] -> Tnat + | Prim_or, [ Tint|Tnat; Tint|Tnat ] -> Tint + | Prim_and, [ Tnat; Tnat ] -> Tnat + | Prim_and, [ Tint|Tnat; Tint|Tnat ] -> Tint + | Prim_not, [ Tint|Tnat ] -> Tint - | Prim_abs, [ { ty = Tint } ] -> Tnat - | Prim_int, [ { ty = Tnat } ] -> Tint - | Prim_sub, [ { ty = Tint|Tnat } ] -> Tint + | Prim_abs, [ Tint ] -> Tint + | Prim_int, [ Tnat ] -> Tint + | Prim_sub, [ Tint|Tnat ] -> Tint - | (Prim_lsl|Prim_lsr), [ { ty = Tnat} ; { ty = Tnat } ] -> Tnat + | (Prim_lsl|Prim_lsr), [ Tnat ; Tnat ] -> Tnat - | Prim_tuple, args -> Ttuple (List.map (fun e -> e.ty) args) + | Prim_tuple, ty_args -> Ttuple (List.map (fun e -> e.ty) args) - | Prim_map_find, [ { ty = key_ty }; { ty = Tmap (expected_key_ty, value_ty) }] + | Prim_map_find, [ key_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) }] + | Prim_map_update, [ key_ty; + Toption value_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,_) }] + | Prim_map_mem, [ key_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 }] + | Prim_set_mem,[ key_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_list_size, [ Tlist _] -> Tnat + | Prim_set_size, [ Tset _] -> Tnat + | Prim_map_size, [ Tmap _] -> Tnat - | Prim_set_update, [ { ty = key_ty }; { ty = Tbool }; - { ty = Tset expected_key_ty }] + | Prim_set_update, [ key_ty; Tbool; 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 } ] -> + | Prim_Some, [ ty ] -> Toption ty + | Prim_fail, [ Tunit ] -> Tfail + | Prim_self, [ 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_now, [ Tunit ] -> Ttimestamp + | Prim_balance, [ Tunit ] -> Ttez + (* | "Current.source", [ Tunit ] -> ... *) + | Prim_amount, [ Tunit ] -> Ttez + | Prim_gas, [ Tunit ] -> Tnat | Prim_hash, [ _ ] -> Tstring - | Prim_hash_key, [ { ty = Tkey } ] -> Tkey_hash - | Prim_check, [ { ty = Tkey }; - { ty = Ttuple [Tsignature; Tstring] } ] -> + | Prim_hash_key, [ Tkey ] -> Tkey_hash + | Prim_check, [ Tkey; Ttuple [Tsignature; Tstring] ] -> Tbool - | Prim_check, args -> + | Prim_check, _ -> error_prim loc Prim_check args [Tkey; Ttuple [Tsignature; Tstring]] - | Prim_manager, [ { ty = Tcontract(_,_) } ] -> + | Prim_manager, [ Tcontract(_,_) ] -> Tkey_hash - | Prim_create_account, [ { ty = Tkey_hash }; { ty = Toption Tkey_hash }; - { ty = Tbool }; { ty = Ttez } ] -> + | Prim_create_account, [ Tkey_hash; Toption Tkey_hash; Tbool; Ttez ] -> Tcontract (Tunit, Tunit) - | Prim_create_account, args -> + | Prim_create_account, _ -> error_prim loc Prim_create_account args [ Tkey_hash; Toption Tkey_hash; Tbool; Ttez ] - | Prim_default_account, [ { ty = Tkey_hash } ] -> + | Prim_default_account, [ 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 } + | Prim_create_contract, [ Tkey_hash; (* manager *) + Toption Tkey_hash; (* delegate *) + Tbool; (* spendable *) + Tbool; (* delegatable *) + Ttez; (* initial amount *) + Tlambda ( + Ttuple [ arg_type; + storage_arg], + Ttuple [ result_type; storage_res]); + storage_init ] -> if storage_arg <> storage_res then error loc "Contract.create: inconsistent storage in contract"; @@ -1216,7 +845,7 @@ and typecheck_prim2 env prim loc args = Tcontract (arg_type, result_type) - | Prim_create_contract, args -> + | Prim_create_contract, _ -> let expected_args = [ Tkey_hash; Toption Tkey_hash; Tbool; Tbool; Ttez ] in @@ -1233,44 +862,47 @@ and typecheck_prim2 env prim loc args = 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) + (LiquidPrinter.Liquid.string_of_type_expl expected) + (LiquidPrinter.Liquid.string_of_type_expl arg) ) (List.combine args expected_args); error loc - "Primitive %s, argument %d:\nExpected type: (arg * storage) -> (res * storage)\nProvided type:%s" + "Primitive %s, argument %d:\n\ + Expected type: (arg * storage) -> (res * storage)\n\ + Provided 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)) }] -> + | Prim_exec, [ 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 | ( Prim_list_map - (* | Prim_list_reduce *) - | Prim_set_reduce + | 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) + ), Tclosure _ :: _ -> + error loc "Cannot use closures in %s" (LiquidTypes.string_of_primitive prim) + + | Prim_list_rev, [ Tlist ty ] -> Tlist ty | Prim_list_map, [ - { ty = Tlambda (from_ty, to_ty) }; - { ty = Tlist ty } ] -> + Tlambda (from_ty, to_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 }; + Tlambda (Ttuple [src_ty; dst_ty], dst_ty'); + Tlist src_ty'; + acc_ty; ] -> if src_ty <> src_ty' then type_error loc "Bad argument source type in List.reduce" src_ty' src_ty; @@ -1281,9 +913,9 @@ and typecheck_prim2 env prim loc args = acc_ty | Prim_set_reduce, [ - { ty = Tlambda (Ttuple [src_ty; dst_ty], dst_ty') }; - { ty = Tset src_ty' }; - { ty = acc_ty }; + Tlambda (Ttuple [src_ty; dst_ty], dst_ty'); + Tset src_ty'; + acc_ty; ] -> if src_ty <> src_ty' then type_error loc "Bad argument source type in Set.reduce" src_ty' src_ty; @@ -1294,9 +926,9 @@ and typecheck_prim2 env prim loc args = 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 }; + Tlambda (Ttuple [Ttuple [key_ty; src_ty]; dst_ty], dst_ty'); + Tmap (key_ty', src_ty'); + acc_ty; ] -> if src_ty <> src_ty' then type_error loc "Bad argument source type in Map.reduce" src_ty' src_ty; @@ -1309,8 +941,8 @@ and typecheck_prim2 env prim loc args = acc_ty | Prim_map_map, [ - { ty = Tlambda (Ttuple [from_key_ty; from_value_ty], to_value_ty) }; - { ty = Tmap (key_ty, value_ty) } ] -> + Tlambda (Ttuple [from_key_ty; from_value_ty], to_value_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 @@ -1319,61 +951,80 @@ and typecheck_prim2 env prim loc args = Tmap (key_ty, to_value_ty) - | Prim_concat, [ { ty = Tstring }; { ty = Tstring }] -> Tstring - | Prim_Cons, [ { ty = head_ty }; { ty = Tunit } ] -> + | Prim_concat, [ Tstring; Tstring] -> Tstring + | Prim_Cons, [ head_ty; Tunit ] -> Tlist head_ty - | Prim_Cons, [ { ty = head_ty }; { ty = Tlist tail_ty } ] -> + | Prim_Cons, [ head_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 -> + | Prim_old, _ -> + error loc "old can only be used in post-conditions" + | prim, _ -> 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) + LiquidPrinter.Liquid.string_of_type_expl 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 + let exp = typecheck env exp in + let exp_ty = get_type exp.ty in + if exp_ty <> get_type expected_ty && exp_ty <> Tfail then type_error (loc_exp env exp) ("Unexpected type for "^info) exp.ty expected_ty; - exp, fail, transfer + exp 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 + let arg = typecheck env arg in + if arg.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 - + mk (Apply (prim, loc, args)) ty + +let typecheck_spec env env_ensures = function + | Requires f -> + let env = { env_ensures with in_post = false } in + let f = typecheck env f in + if f.transfer then + error (loc_exp env f) "transfer not allowed in specification"; + if f.fail then + error (loc_exp env f) "expressions in specifications cannot fail"; + Requires f + | Ensures f -> + let env = { env_ensures with in_post = true } in + let f = typecheck env f in + if f.transfer then + error (loc_exp env f) "transfer not allowed in specification"; + if f.fail then + error (loc_exp env f) "expressions in specifications cannot fail"; + Ensures f + | Fails f -> + let env = { env with in_post = true } in + let f = typecheck env f in + if f.transfer then + error (loc_exp env f) "transfer not allowed in specification"; + if f.fail then + error (loc_exp env f) "expressions in specifications cannot fail"; + Fails f + +let typecheck_specs env env_ensures l = + let env = { env with allow_spec = true } in + let env_ensures = { env_ensures with allow_spec = true } in + List.map (typecheck_spec env env_ensures) l let typecheck_contract ~warnings env contract = let env = { warnings; + allow_spec = false; + in_post = false; counter = ref 0; vars = StringMap.empty; to_inline = ref StringMap.empty; @@ -1382,21 +1033,23 @@ let typecheck_contract ~warnings env contract = contract; } in - (* "storage/1" *) - let (_ , env, _) = new_binding env "storage" contract.storage in - (* "parameter/2" *) - let (_, env, _) = new_binding env "parameter" contract.parameter in + let (env, _) = new_binding env "storage" contract.storage in + let (env, _) = new_binding env "parameter" contract.parameter in + let (env_ensures, _) = new_binding env "@storage" contract.storage in + let (env_ensures, _) = new_binding env_ensures "@result" contract.return in + let spec = typecheck_specs env env_ensures contract.spec in let expected_ty = Ttuple [contract.return; contract.storage] in - - let code, _can_fail, _transfer = + let code = typecheck_expected "return value" env expected_ty contract.code in - { contract with code }, ! (env.to_inline) + { contract with spec; code } let typecheck_code ~warnings env contract expected_ty code = let env = { warnings; + allow_spec = false; + in_post = false; counter = ref 0; vars = StringMap.empty; to_inline = ref StringMap.empty; @@ -1405,14 +1058,12 @@ let typecheck_code ~warnings env contract expected_ty code = contract ; } in - let code, _can_fail, _transfer = - typecheck_expected "value" env expected_ty code in - code + typecheck_expected "value" env expected_ty code -let check_const_type ~to_tez loc ty cst = +let check_const_type ?(from_mic=false) ~to_tez loc ty cst = let rec check_const_type ty cst = - match ty, cst with + match get_type ty, cst with | Tunit, CUnit -> CUnit | Tbool, CBool b -> CBool b @@ -1420,41 +1071,16 @@ let check_const_type ~to_tez loc ty cst = | Tint, CNat s -> CInt s | Tnat, CInt s - | Tnat, CNat s -> CNat s + | Tnat, CNat s -> CNat s | Tstring, CString s -> CString s | Ttez, CTez s -> CTez s - | Ttez, CString s -> CTez (to_tez s) - - | 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 *) - try Scanf.sscanf s "%_d-%_d-%_dT%_d:%_d:%_dZ%!" () - with _ -> - try Scanf.sscanf s "%_d-%_d-%_d %_d:%_d:%_dZ%!" () - with _ -> - try Scanf.sscanf s "%_d-%_d-%_dT%_d:%_d:%_d-%_d:%_d%!" () - with _ -> - try Scanf.sscanf s "%_d-%_d-%_dT%_d:%_d:%_d+%_d:%_d%!" () - with _ -> - try Scanf.sscanf s "%_d-%_d-%_d %_d:%_d:%_d-%_d:%_d%!" () - with _ -> - try Scanf.sscanf s "%_d-%_d-%_d %_d:%_d:%_d+%_d:%_d%!" () - with _ -> - error loc "Bad format for timestamp" - end; - CTimestamp s - - - | Tsignature, CSignature s - | Tsignature, CString s -> CSignature s + + | Tkey, CKey s -> CKey s + | Tkey_hash, CKey_hash s -> CKey_hash s + | Ttimestamp, CTimestamp s -> CTimestamp s + | Tsignature, CSignature s -> CSignature s | Ttuple tys, CTuple csts -> begin @@ -1478,8 +1104,55 @@ let check_const_type ~to_tez loc ty cst = | Tset ty, CSet csts -> CSet (List.map (check_const_type ty) csts) + | Trecord labels, CRecord fields -> + CRecord (List.map (fun (f, cst) -> + try + let ty = List.assoc f labels in + f, check_const_type ty cst + with Not_found -> + error loc "Record field %s is not in type %s" f + (LiquidPrinter.Liquid.string_of_type ty) + ) fields) + + | Tsum constrs, CConstr (c, cst) -> + CConstr (c, + try + let ty = List.assoc c constrs in + check_const_type ty cst + with Not_found -> + error loc "Constructor %s does not belong to type %s" c + (LiquidPrinter.Liquid.string_of_type ty) + ) + | _ -> - error loc "constant type mismatch" + if from_mic then + match ty, cst with + | Ttimestamp, CString s -> + begin (* approximation of correct tezos timestamp *) + try Scanf.sscanf s "%_d-%_d-%_dT%_d:%_d:%_dZ%!" () + with _ -> + try Scanf.sscanf s "%_d-%_d-%_d %_d:%_d:%_dZ%!" () + with _ -> + try Scanf.sscanf s "%_d-%_d-%_dT%_d:%_d:%_d-%_d:%_d%!" () + with _ -> + try Scanf.sscanf s "%_d-%_d-%_dT%_d:%_d:%_d+%_d:%_d%!" () + with _ -> + try Scanf.sscanf s "%_d-%_d-%_d %_d:%_d:%_d-%_d:%_d%!" () + with _ -> + try Scanf.sscanf s "%_d-%_d-%_d %_d:%_d:%_d+%_d:%_d%!" () + with _ -> + error loc "Bad format for timestamp" + end; + CTimestamp s + + | Ttez, CString s -> CTez (to_tez s) + | Tkey_hash, CString s -> CKey_hash s + | Tkey, CString s -> CKey s + | Tsignature, CString s -> CSignature s + + | _ -> error loc "constant type mismatch" + else + error loc "constant type mismatch" in check_const_type ty cst diff --git a/tools/liquidity/liquidCheck.mli b/tools/liquidity/liquidCheck.mli index 50258056..4da42009 100644 --- a/tools/liquidity/liquidCheck.mli +++ b/tools/liquidity/liquidCheck.mli @@ -13,10 +13,8 @@ val error : location -> ('a, Format.formatter, unit, unit, unit, 'b) format6 -> 'a -val typecheck_contract : warnings:bool -> env -> - syntax_exp contract -> - typed_exp contract - * datatype exp StringMap.t +val typecheck_contract : + warnings:bool -> env -> syntax_contract -> typed_contract (* val uniq_ident : string -> string @@ -24,12 +22,13 @@ val uniq_ident : string -> string val typecheck_code : warnings:bool -> env -> - syntax_exp contract -> + syntax_contract -> LiquidTypes.datatype -> syntax_exp -> typed_exp val check_const_type : + ?from_mic:bool -> to_tez:(string -> LiquidTypes.tez) -> LiquidTypes.location -> LiquidTypes.datatype -> LiquidTypes.const -> LiquidTypes.const diff --git a/tools/liquidity/liquidClean.mli b/tools/liquidity/liquidClean.mli index 30eb98a1..ac66601c 100644 --- a/tools/liquidity/liquidClean.mli +++ b/tools/liquidity/liquidClean.mli @@ -10,4 +10,4 @@ open LiquidTypes val clean_code : loc_michelson -> loc_michelson -val clean_contract : loc_michelson contract -> loc_michelson contract +val clean_contract : loc_michelson_contract -> loc_michelson_contract diff --git a/tools/liquidity/liquidData.ml b/tools/liquidity/liquidData.ml index fba3b0e9..43d77e25 100644 --- a/tools/liquidity/liquidData.ml +++ b/tools/liquidity/liquidData.ml @@ -22,7 +22,7 @@ let rec translate_const_exp loc exp = (* removed during typechecking *) | Record (_, _) - | Constructor (_, _, _) -> assert false + | Constructor (_, _, _) -> assert false | Apply (Prim_Left, _, [x; _ty]) -> CLeft (translate_const_exp loc x) | Apply (Prim_Right, _, [x; _ty]) -> CRight (translate_const_exp loc x) @@ -38,33 +38,35 @@ let rec translate_const_exp loc exp = (LiquidTypes.string_of_primitive prim) (List.length args) | Var (_, _, _) - | SetVar (_, _, _, _) - | If (_, _, _) - | Seq (_, _) - | LetTransfer (_, _, _, _, _, _, _, _) - | MatchOption (_, _, _, _, _) - | MatchList (_, _, _, _, _, _) - | Loop (_, _, _, _) - | Lambda (_, _, _, _, _) - | Closure (_, _, _, _, _, _) - | MatchVariant (_, _, _) + | SetVar (_, _, _, _) + | If (_, _, _) + | Seq (_, _) + | LetTransfer (_, _, _, _, _, _, _, _) + | MatchOption (_, _, _, _, _) + | MatchNat (_, _, _, _, _, _) + | MatchList (_, _, _, _, _, _) + | Loop (_, _, _, _) + | Lambda (_, _, _, _, _) + | Closure (_, _, _, _, _, _) + | MatchVariant (_, _, _) + | And _ | Or _ | Implies _ | Equiv _ | Forall _ | Exists _ -> - LiquidLoc.raise_error ~loc "non-constant expression" + LiquidLoc.raise_error ~loc "non-constant expression" let data_of_liq ~filename ~contract ~parameter ~storage = (* first, extract the types *) let ocaml_ast = LiquidFromOCaml.structure_of_string ~filename contract in let contract, env = LiquidFromOCaml.translate ~filename ocaml_ast in - let _, _ = LiquidCheck.typecheck_contract + let _ = LiquidCheck.typecheck_contract ~warnings:true env contract in let translate filename s ty = try let ml_exp = LiquidFromOCaml.expression_of_string ~filename s in let sy_exp = LiquidFromOCaml.translate_expression env ml_exp in - let ty_exp = - LiquidCheck.typecheck_code ~warnings:true env contract ty sy_exp in + let ty_exp = LiquidCheck.typecheck_code + ~warnings:true env contract ty sy_exp in let loc = LiquidLoc.loc_in_file filename in let ty_exp = translate_const_exp loc ty_exp in let s = LiquidPrinter.Michelson.line_of_const ty_exp in diff --git a/tools/liquidity/liquidDecomp.ml b/tools/liquidity/liquidDecomp.ml index d3743a43..e29b175d 100644 --- a/tools/liquidity/liquidDecomp.ml +++ b/tools/liquidity/liquidDecomp.ml @@ -11,7 +11,7 @@ open LiquidTypes let noloc = LiquidLoc.noloc -let mk desc = { desc; ty = (); bv = StringSet.empty; fail = false } +let mk desc = mk desc () let const_name_of_datatype = function | Tunit -> "u" @@ -26,6 +26,8 @@ let const_name_of_datatype = function | Tsignature -> "sig" | Ttuple _ -> "tuple" | Toption _ -> "opt" + | Trecord _ -> "record" + | Tsum _ -> "sum" | Tlist _ -> "l" | Tset _ -> "s" | Tmap _ -> "map" @@ -47,6 +49,8 @@ let rec var_of node = | N_IF_CONS _ -> Printf.sprintf "if_cons%d" node.num | N_IF_LEFT _ -> Printf.sprintf "if_left%d" node.num | N_IF_RIGHT _ -> Printf.sprintf "if_right%d" node.num + | N_IF_PLUS _ -> Printf.sprintf "if_plus%d" node.num + | N_IF_MINUS _ -> Printf.sprintf "if_minus%d" node.num | N_LEFT _ -> Printf.sprintf "left%d" node.num | N_RIGHT _ -> Printf.sprintf "right%d" node.num | N_TRANSFER _ -> Printf.sprintf "transfer%d" node.num @@ -134,6 +138,15 @@ let decompile contract = mk(Apply(Prim_tuple_get,noloc,[ mk(Var(var_of node,noloc,[])); int_zero])))) + (* ABS : int -> int *) + | N_ABS, [arg] -> + mklet node (Apply(Prim_abs, noloc, [arg_of arg])) + + (* ABS as match%nat *) + | N_PRIM "ABS", [arg] -> + let x = var_of arg in + let vx = mk (Var (x, noloc, [])) in + mklet node (MatchNat(arg_of arg, noloc, x, vx, x, vx)) | N_PRIM prim, _ -> let prim, args = @@ -175,7 +188,6 @@ let decompile contract = | "EDIV" -> Prim_ediv | "EXEC" -> Prim_exec | "INT" -> Prim_int - | "ABS" -> Prim_abs | "H" -> Prim_hash | "HASH_KEY" -> Prim_hash_key | "CHECK_SIGNATURE" -> Prim_check @@ -212,7 +224,7 @@ let decompile contract = | N_FAIL, _ -> mk (Apply (Prim_fail, noloc, [unit])) | N_CONST (ty, cst), [] -> - let cst = LiquidCheck.check_const_type + let cst = LiquidCheck.check_const_type ~from_mic:true ~to_tez:LiquidPrinter.tez_of_mic noloc ty cst in mklet node (Const (ty, cst)) @@ -235,6 +247,12 @@ let decompile contract = decompile_next then_node, var_of var0, decompile_next else_node) + | N_IF_PLUS (_, var0), N_IF_MINUS (_,var1) -> + MatchNat(arg_of arg, noloc, + var_of var0, + decompile_next then_node, + var_of var1, + decompile_next else_node) | N_IF_LEFT (_, var0), N_IF_RIGHT (_,var1) -> MatchVariant(arg_of arg, noloc, [ @@ -292,7 +310,7 @@ let decompile contract = | ( N_LAMBDA_END _ - | N_LAMBDA _ + | N_LAMBDA _ | N_TRANSFER _ | N_LOOP _ | N_IF _ @@ -302,7 +320,7 @@ let decompile contract = | N_SOURCE _ | N_LEFT _ | N_RIGHT _ - + | N_ABS | N_START | N_LAMBDA_BEGIN | N_VAR _ @@ -316,6 +334,8 @@ let decompile contract = | N_IF_CONS (_, _, _) | N_IF_LEFT (_, _) | N_IF_RIGHT (_, _) + | N_IF_PLUS (_, _) + | N_IF_MINUS (_, _) | N_TRANSFER_RESULT _ | N_LOOP_BEGIN _ | N_LOOP_ARG (_, _) @@ -353,4 +373,4 @@ let decompile contract = ])), code)) in *) - { contract with code } + { contract with code; spec = [] } diff --git a/tools/liquidity/liquidDecomp.mli b/tools/liquidity/liquidDecomp.mli index 60b8efc6..3cffebfb 100644 --- a/tools/liquidity/liquidDecomp.mli +++ b/tools/liquidity/liquidDecomp.mli @@ -9,5 +9,4 @@ open LiquidTypes -val decompile : node_exp LiquidTypes.contract -> - syntax_exp LiquidTypes.contract +val decompile : node_contract -> syntax_contract diff --git a/tools/liquidity/liquidDot.ml b/tools/liquidity/liquidDot.ml index aaf0a2e7..848f6ad0 100644 --- a/tools/liquidity/liquidDot.ml +++ b/tools/liquidity/liquidDot.ml @@ -57,44 +57,46 @@ let to_string contract = let deps = match node.kind with | N_UNKNOWN _ - | N_START - | N_FAIL - | N_LAMBDA_BEGIN - | N_END - | N_VAR _ - | N_CONST (_, _) - | N_PRIM _ - | N_SOURCE _ - | N_LEFT _ - | N_RIGHT _ - | N_TRANSFER_RESULT _ - + | N_START + | N_FAIL + | N_LAMBDA_BEGIN + | N_END + | N_VAR _ + | N_CONST (_, _) + | N_PRIM _ + | N_SOURCE _ + | N_LEFT _ + | N_RIGHT _ + | N_TRANSFER_RESULT _ + | N_ABS -> [] | N_LOOP_END (x,y,z) - | N_IF_CONS (x, y, z)-> [x;y;z] + | N_IF_CONS (x, y, z)-> [x;y;z] - | N_TRANSFER (x,y) - | N_LOOP_RESULT (x,y,_) - | N_IF_SOME (x,y) - | N_IF_LEFT (x,y) - | N_IF_RIGHT (x,y) - | N_IF_END_RESULT (x,Some y,_) + | N_TRANSFER (x,y) + | N_LOOP_RESULT (x,y,_) + | N_IF_SOME (x,y) + | N_IF_LEFT (x,y) + | N_IF_RIGHT (x,y) + | N_IF_PLUS (x,y) + | N_IF_MINUS (x,y) + | N_IF_END_RESULT (x,Some y,_) | N_IF_END (x,y) | N_IF (x,y) - | N_LOOP (x,y) - | N_LAMBDA (x,y,_,_) -> [x;y] + | N_LOOP (x,y) + | N_LAMBDA (x,y,_,_) -> [x;y] - | N_IF_END_RESULT (x,None,_) - | N_IF_RESULT (x,_) - | N_IF_THEN x - | N_IF_ELSE x - | N_IF_NONE x - | N_IF_NIL x - | N_LOOP_BEGIN x - | N_LOOP_ARG (x,_) - | N_LAMBDA_END x -> [x] + | N_IF_END_RESULT (x,None,_) + | N_IF_RESULT (x,_) + | N_IF_THEN x + | N_IF_ELSE x + | N_IF_NONE x + | N_IF_NIL x + | N_LOOP_BEGIN x + | N_LOOP_ARG (x,_) + | N_LAMBDA_END x -> [x] in List.iter (fun arg -> add_edge node arg [ ] @@ -105,7 +107,7 @@ let to_string contract = List.iter iter deps; List.iter iter node.args; iter_next node - end + end in iter begin_node; Ocamldot.to_string g diff --git a/tools/liquidity/liquidDot.mli b/tools/liquidity/liquidDot.mli index 713f3d08..b80bd372 100644 --- a/tools/liquidity/liquidDot.mli +++ b/tools/liquidity/liquidDot.mli @@ -9,4 +9,4 @@ open LiquidTypes -val to_string : node_exp contract -> string +val to_string : node_contract -> string diff --git a/tools/liquidity/liquidEmit.mli b/tools/liquidity/liquidEmit.mli index e25d7139..3c95988c 100644 --- a/tools/liquidity/liquidEmit.mli +++ b/tools/liquidity/liquidEmit.mli @@ -10,4 +10,4 @@ open LiquidTypes val emit_code : noloc_michelson -> michelson_exp -val emit_contract : noloc_michelson contract -> michelson_exp contract +val emit_contract : noloc_michelson_contract -> michelson_contract diff --git a/tools/liquidity/liquidEncode.ml b/tools/liquidity/liquidEncode.ml new file mode 100644 index 00000000..87cd7b4a --- /dev/null +++ b/tools/liquidity/liquidEncode.ml @@ -0,0 +1,931 @@ +(**************************************************************************) +(* *) +(* Copyright (c) 2017 . *) +(* Fabrice Le Fessant, OCamlPro SAS *) +(* *) +(* All rights reserved. No warranty, explicit or implicit, provided. *) +(* *) +(**************************************************************************) + +open LiquidTypes + +let noloc env = LiquidLoc.loc_in_file env.env.filename + +let error loc msg = + LiquidLoc.raise_error ~loc ("Type error: " ^^ msg ^^ "%!") + +let mk_typed (desc: (datatype, typed) exp_desc) ty = mk desc ty +let mk (desc: (datatype, encoded) exp_desc) ty = mk desc ty + +let mk_typed_nat i = + mk_typed (Const (Tnat, CNat (LiquidPrinter.integer_of_int i))) Tnat + +let mk_nat i = + mk (Const (Tnat, CNat (LiquidPrinter.integer_of_int i))) Tnat + +let mk_nil list_ty = + mk (Const (list_ty, CList [])) list_ty + +let mk_typed_nil list_ty = + mk_typed (Const (list_ty, CList [])) list_ty + +let mk_tuple loc l = + let tuple_ty = Ttuple (List.map (fun t -> t.ty) l) in + mk (Apply (Prim_tuple, loc, l)) tuple_ty + +let const_unit = mk (Const (Tunit, CUnit)) Tunit + +let const_true = mk (Const (Tbool, CBool true)) Tbool + +let const_false = mk (Const (Tbool, CBool false)) Tbool + +let unused env ty = + mk (Apply(Prim_unused, noloc env, [const_unit])) ty + +let uniq_ident env name = + env.counter := !(env.counter) + 1; + Printf.sprintf "%s/%d" name !(env.counter) + +let new_binding env name ty = + let new_name = uniq_ident env name in + let count = ref 0 in + let env = { env with + vars = StringMap.add name (new_name, ty, count) env.vars } in + (new_name, env, count) + +let maybe_reset_vars env transfer = + if transfer then + { env with + vars = StringMap.empty; + clos_env = None; + } + else env + +(* Find variable name in either the global environment or the closure + environment, returns a corresponding expression *) +let find_var ?(count_used=true) env loc name = + try + let (name, ty, count) = StringMap.find name env.vars in + if count_used then incr count; + mk (Var (name, loc, [])) ty + with Not_found -> + match env.clos_env with + | None -> error loc "unbound variable %S" name + | Some ce -> + try + let v, (cpt_in, cpt_out) = StringMap.find name ce.env_bindings in + if count_used then begin + incr cpt_in; + incr cpt_out; + end; + v + with Not_found -> + error loc "unbound variable %S" name + +(* Create environment for closure *) +let env_for_clos env loc bvs arg_name arg_type = + let _, free_vars = StringSet.fold (fun v (index, free_vars) -> + let index = index + 1 in + let free_vars = + try + let (bname, btype, cpt_out) = StringMap.find v env.vars in + StringMap.add v (bname, btype, index, (ref 0, cpt_out)) free_vars + with Not_found -> + match env.clos_env with + | None -> free_vars + | Some ce -> + try + let bname, btype, _, (cpt_in, cpt_out) = + StringMap.find v ce.env_vars in + StringMap.add v (bname, btype, index, (cpt_in, cpt_out)) free_vars + with Not_found -> free_vars + in + (index, free_vars) + ) bvs (0, StringMap.empty) + in + let free_vars_l = + StringMap.bindings free_vars + |> List.sort (fun (_, (_,_,i1,_)) (_, (_,_,i2,_)) -> compare i1 i2) + in + let ext_env = env in + let env = { env with vars = StringMap.empty } in + match free_vars_l with + | [] -> (* no closure environment *) + let (new_name, env, _) = new_binding env arg_name arg_type in + env, new_name, arg_type, [] + | _ -> + let env_arg_name = uniq_ident env "closure_env" in + let env_arg_type = + Ttuple (arg_type :: List.map (fun (_, (_,ty,_,_)) -> ty) free_vars_l) in + let env_arg_var = mk (Var (env_arg_name, loc, [])) env_arg_type in + let new_name = uniq_ident env arg_name in + let env_vars = + StringMap.add arg_name + (new_name, arg_type, 0, (ref 0, ref 0)) free_vars in + let size = StringMap.cardinal env_vars in + let env_bindings = + StringMap.map (fun (_, ty, index, count) -> + let ei = mk_nat index in + let accessor = + if index + 1 = size then Prim_tuple_get_last + else Prim_tuple_get in + let exp = mk (Apply(accessor, loc, [env_arg_var; ei])) ty in + exp, count + ) env_vars + in + let call_bindings = List.map (fun (name, _) -> + name, find_var ~count_used:false ext_env loc name + ) free_vars_l + in + (* Format.eprintf "--- Closure %s ---@." env_arg_name; *) + (* StringMap.iter (fun name (e,_) -> *) + (* Format.eprintf "%s -> %s@." *) + (* name (LiquidPrinter.Liquid.string_of_code e) *) + (* ) env_bindings; *) + let env_closure = { + env_vars; + env_bindings; + call_bindings; + } in + let env = + { env with + clos_env = Some env_closure + } + in + env, env_arg_name, env_arg_type, call_bindings + + +let rec encode_type ?(keepalias=true) ty = + (* if env.only_typecheck then ty *) + (* else *) + match ty with + | Ttez | Tunit | Ttimestamp | Tint | Tnat | Tbool | Tkey | Tkey_hash + | Tsignature | Tstring | Tfail -> ty + | Ttuple tys -> + let tys' = List.map (encode_type ~keepalias) tys in + if List.for_all2 (==) tys tys' then ty + else Ttuple tys' + | Tset t | Tlist t | Toption t -> + let t' = encode_type ~keepalias t in + if t' == t then ty + else begin match ty with + | Tset t -> Tset t' + | Tlist t -> Tlist t' + | Toption t -> Toption t' + | _ -> assert false + end + | Tor (t1, t2) | Tcontract (t1, t2) | Tlambda (t1, t2) | Tmap (t1, t2) -> + let t1', t2' = encode_type ~keepalias t1, encode_type ~keepalias t2 in + if t1 == t1' && t2 == t2' then ty + else begin match ty with + | Tor (t1, t2) -> Tor (t1', t2') + | Tcontract (t1, t2) -> Tcontract (t1', t2') + | Tlambda (t1, t2) -> Tlambda (t1', t2') + | Tmap (t1, t2) -> Tmap (t1', t2') + | _ -> assert false + end + | Tclosure ((t1, t2), t3) -> + let t1' = encode_type ~keepalias t1 in + let t2' = encode_type ~keepalias t2 in + let t3' = encode_type ~keepalias t3 in + if t1 == t1' && t2 == t2' && t3 == t3' then ty + else Tclosure ((t1', t2'), t3') + | Ttype (name, t) -> + let t' = encode_type ~keepalias t in + if not keepalias then t' + else if t' == t then ty + else Ttype (name, t') + | Trecord labels -> encode_record_type ~keepalias labels + | Tsum cstys -> encode_sum_type ~keepalias cstys + +and encode_record_type ~keepalias labels = + Ttuple (List.map (fun (_, ty) -> encode_type ~keepalias ty) labels) + +and encode_sum_type ~keepalias cstys = + let rec rassoc = function + | [] -> assert false + | [_, ty] -> encode_type ~keepalias ty + | (_, lty) :: rstys -> + Tor (encode_type ~keepalias lty, rassoc rstys) + in + rassoc cstys + +let rec encode_const env c = match c with + | CUnit | CBool _ | CInt _ | CNat _ | CTez _ | CTimestamp _ | CString _ + | CKey _ | CSignature _ | CNone | CKey_hash _ -> c + + | CSome x -> CSome (encode_const env x) + | CLeft x -> CLeft (encode_const env x) + | CRight x -> CRight (encode_const env x) + + | CTuple xs -> CTuple (List.map (encode_const env) xs) + | CList xs -> CList (List.map (encode_const env) xs) + | CSet xs -> CSet (List.map (encode_const env) xs) + + | CMap l -> + CMap (List.map (fun (x,y) -> encode_const env x, encode_const env y) l) + + | CRecord labels -> + CTuple (List.map (fun (_, x) -> encode_const env x) labels) + + | CConstr (constr, x) -> + try + let ty_name, _ = StringMap.find constr env.env.constrs in + let constr_ty = StringMap.find ty_name env.env.types in + match constr_ty with + | Tsum constrs -> + let rec iter constrs = + match constrs with + | [] -> assert false + | [c, _] -> + assert (c = constr); + encode_const env x + | (c, _) :: constrs -> + if c = constr then CLeft (encode_const env x) + else CRight (iter constrs) + in + iter constrs + | _ -> raise Not_found + with Not_found -> + error (noloc env) "unknown constructor %s" constr + + +let encode_prim_get arg n = + let size = match (get_type arg.ty) with + | Ttuple tuple -> List.length tuple + | Trecord rtys -> List.length rtys + | _ -> assert false + in + let prim = + if size = n + 1 then + Prim_tuple_get_last + else + Prim_tuple_get + in + prim, [arg; mk_nat n] + + +let encode_prim_set arg n v = + let size = match (get_type arg.ty) with + | Ttuple tuple -> List.length tuple + | Trecord rtys -> List.length rtys + | _ -> assert false + in + let prim = + if size = n + 1 then + Prim_tuple_set_last + else + Prim_tuple_set + in + prim, [arg; mk_nat n; v] + +let rec encode env ( exp : typed_exp ) : encoded_exp = + match exp.desc with + + | Const (ty, cst) -> + mk (Const (ty, encode_const env cst)) ty + + | Let (name, loc, e, body) -> + + let e = encode env e in + let env = maybe_reset_vars env e.transfer in + let (new_name, env, count) = new_binding env name e.ty in + let body = encode env body in + (* check_used env name loc count; *) + if (not e.transfer) && (not e.fail) 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 e !(env.to_inline) + | _ -> () + end; + mk (Let (new_name, loc, e, body)) body.ty + + | Var (name, loc, labels) -> + let e = find_var env loc name in + List.fold_left + (fun e label -> + (* let ty = match first_alias e.ty with *) + (* | Some (ty_name, (Trecord _ as ty)) -> ty_name, ty *) + (* | _ -> error loc "not a record" *) + (* in *) + let arg1 = mk e.desc e.ty in + let n, label_ty = + try + let (ty_name', n, label_ty) = + StringMap.find label env.env.labels in + n, label_ty + with Not_found -> + error loc "bad label" + in + let prim, args = encode_prim_get arg1 n in + mk (Apply(prim, loc, args)) label_ty + ) e labels + + | SetVar (name, loc, [], e) -> encode env e + + | SetVar (name, loc, label :: labels, arg) -> + let arg1 = find_var env loc name in + let label_types = match get_type arg1.ty with + | Trecord label_types -> label_types + | _ -> assert false + in + let exception Return of (int * datatype) in + let n, lty = + try + List.iteri (fun n (l, lty) -> + if l = label then raise (Return (n, lty)) + ) label_types; + error loc "bad label" + with Return n -> n + in + let arg = + match labels with + | [] -> + let arg = encode env arg in + if arg.transfer then error loc "transfer within set-field"; + arg + | _::_ -> + let prim, args = encode_prim_get arg1 n in + let get_exp = mk (Apply(prim, loc, args)) lty in + let tmp_name = uniq_ident env "tmp#" in + let (new_name, env, count) = new_binding env tmp_name lty in + let body = + encode env + (mk_typed (SetVar (tmp_name, loc, labels, arg)) exp.ty) + in + mk (Let (new_name, loc, get_exp, body)) body.ty + in + let prim, args = encode_prim_set arg1 n arg in + mk (Apply(prim, loc, args)) arg1.ty + + | Seq (exp1, exp2) -> + (* TODO: if not exp.fail then remove exp1 *) + let exp1 = encode env exp1 in + let exp2 = encode env exp2 in + mk (Seq (exp1, exp2)) exp.ty + + | If (cond, ifthen, ifelse) -> + let cond = encode env cond in + let ifthen = encode env ifthen in + let ifelse = encode env ifelse in + mk (If (cond, ifthen, ifelse)) exp.ty + + | LetTransfer (storage_name, result_name, + loc, + contract_exp, tez_exp, + storage_exp, arg_exp, body) -> + let tez_exp = encode env tez_exp in + let contract_exp = encode env contract_exp in + let arg_exp = encode env arg_exp in + let storage_exp = encode env storage_exp in + let return_ty = match contract_exp.ty with + | Tcontract (_, return_ty) -> return_ty + | _ -> assert false + in + 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 = encode env body in + (* check_used env storage_name loc storage_count; *) + (* check_used env result_name loc result_count; *) + mk (LetTransfer(new_storage, new_result, + loc, + contract_exp, tez_exp, + storage_exp, arg_exp, body)) body.ty + + | Apply (Prim_unknown, _, _) -> assert false + + + (* List.rev -> List.reduce (::) *) + | Apply (Prim_list_rev, loc, [l]) -> + let l = encode env l in + let elt_ty = match l.ty with + | Tlist ty -> ty + | _ -> assert false + in + let list_ty = l.ty in + let arg_name = uniq_ident env "arg" in + let arg_ty = Ttuple [elt_ty; list_ty] in + let arg = mk (Var (arg_name, loc, [])) arg_ty in + let e = mk (Apply(Prim_tuple_get, loc, [arg; mk_nat 0])) elt_ty in + let acc = + mk (Apply(Prim_tuple_get_last, loc, [arg; mk_nat 1])) list_ty in + let f_body = mk (Apply (Prim_Cons, loc, [e; acc])) list_ty 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)) 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 + + (* List.reduce (closure) -> Loop.loop *) + | Apply (Prim_list_reduce, loc, [f; l; acc]) -> + let f = encode env f in + let l = encode env l in + let acc = encode env acc in + let args = [f; l; acc] in + begin match f.ty with + | Tclosure ((arg_ty, env_ty), acc_ty) -> + let elt_ty = match l.ty with + | Tlist ty -> ty + | _ -> assert false + 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 in + let head = mk (Var (head_name, loc, [])) elt_ty in + let tail = mk (Var (tail_name, loc, [])) list_ty in + let l' = + mk (Apply(Prim_tuple_get, loc, [arg; mk_nat 0])) list_ty in + let acc' = + mk (Apply(Prim_tuple_get_last, loc, [arg; mk_nat 1])) acc_ty in + let nil_case = mk_tuple loc [ + const_false ; + mk_tuple loc [mk_nil list_ty; acc'] + ] in + let cons_case = + mk_tuple loc [ + const_true; + mk_tuple loc [ + tail; + mk (Apply (Prim_exec, loc, [ + mk_tuple loc [head; acc']; + f + ])) acc_ty + ] + ] + in + let loop_body = mk + (MatchList (l', loc, head_name, tail_name, cons_case, nil_case)) + loop_body_ty + in + let loop = mk + (Loop (loop_arg_name, loc, loop_body, + mk_tuple loc [l; acc])) + (Ttuple [list_ty; acc_ty]) + in + mk (Apply (Prim_tuple_get_last, loc, [loop; mk_nat 1])) + acc_ty + | _ -> + mk (Apply (Prim_list_reduce, loc, args)) acc.ty + end + + (* List.map (closure) -> {List.rev(List.reduce (closure)} *) + | Apply (Prim_list_map, loc, [f; l]) -> + let f' = encode env f in + begin match get_type f'.ty with + | Tlambda _ -> + let l = encode env l in + mk (Apply (Prim_list_map, loc, [f'; l])) exp.ty + | Tclosure ((arg_ty, _), ty_ret) -> + let arg_name = uniq_ident env "arg" in + let acc_ty = Tlist ty_ret in + let rarg_ty = Ttuple [arg_ty; Tlist ty_ret] in + let arg = mk_typed (Var (arg_name, loc, [])) rarg_ty in + let x = + mk_typed (Apply(Prim_tuple_get, loc, [arg; mk_typed_nat 0])) arg_ty in + let acc = + mk_typed (Apply(Prim_tuple_get, loc, [arg; mk_typed_nat 1])) acc_ty in + let f_body = mk_typed (Apply(Prim_Cons, loc, [ + mk_typed (Apply(Prim_exec, loc, [x; f])) ty_ret; + acc + ])) acc_ty in + let f_red = + mk_typed (Lambda (arg_name, rarg_ty, loc, f_body, acc_ty)) + (Tlambda (rarg_ty, acc_ty)) in + let red = + mk_typed (Apply (Prim_list_reduce, loc, + [f_red; l; mk_typed_nil acc_ty])) acc_ty in + let rev_red = mk_typed (Apply (Prim_list_rev, loc, [red])) acc_ty in + encode env rev_red + | _ -> assert false + end + + (* Map.reduce (closure) -> {Map.reduce (::) |> List.rev |> List.reduce} *) + | Apply (Prim_map_reduce, loc, [f; m; acc]) -> + let f' = encode env f in + begin match get_type f'.ty with + | Tlambda _ -> + let m = encode env m in + let acc = encode env acc in + mk (Apply (Prim_map_reduce, loc, [f'; m; acc])) exp.ty + | Tclosure ((Ttuple [kv_ty; acc_ty], _), ty_ret) -> + let arg_name = uniq_ident env "arg" in + let elts_ty = Tlist kv_ty in + let arg_ty = Ttuple [kv_ty; elts_ty] in + let arg = mk_typed (Var (arg_name, loc, [])) elts_ty in + let kv = + mk_typed (Apply(Prim_tuple_get, loc, [arg; mk_typed_nat 0])) kv_ty in + let acc_elts = + mk_typed (Apply(Prim_tuple_get, loc, [arg; mk_typed_nat 1])) elts_ty in + let gather_body = + mk_typed (Apply(Prim_Cons, loc, [kv; acc_elts])) elts_ty in + let gather_fun = + mk_typed (Lambda (arg_name, arg_ty, loc, gather_body, elts_ty)) + (Tlambda (arg_ty, elts_ty)) + in + let rev_elts = + mk_typed (Apply(Prim_map_reduce, loc, + [gather_fun; m; mk_typed_nil elts_ty])) + elts_ty + in + let elts = mk_typed (Apply(Prim_list_rev, loc, [rev_elts])) elts_ty in + let red = mk_typed + (Apply(Prim_list_reduce, loc, [f; elts; acc])) acc_ty in + encode env red + | _ -> assert false + end + + (* Map.map (closure) -> {Map.reduce (Map.update)} *) + | Apply (Prim_map_map, loc, [f; m]) -> + let f' = encode env f in + begin match get_type f'.ty with + | Tlambda _ -> + let m = encode env m in + mk (Apply (Prim_map_map, loc, [f'; m])) exp.ty + | Tclosure ((Ttuple [k_ty; v_ty] as kv_ty, _), ty_ret) -> + let arg_name = uniq_ident env "arg" in + let acc_ty = Tmap (k_ty, ty_ret) in + let arg_ty = Ttuple [kv_ty; acc_ty] in + let arg = mk_typed (Var (arg_name, loc, [])) arg_ty in + let kv = + mk_typed (Apply(Prim_tuple_get, loc, [arg; mk_typed_nat 0])) kv_ty in + let acc = + mk_typed (Apply(Prim_tuple_get, loc, [arg; mk_typed_nat 1])) acc_ty in + let k = + mk_typed (Apply(Prim_tuple_get, loc, [kv; mk_typed_nat 0])) k_ty in + let acc_ty = Tmap (k_ty, ty_ret) in + let update_body = + mk_typed (Apply(Prim_map_update, loc, [ + k; + mk_typed (Apply(Prim_Some, loc, [ + mk_typed (Apply(Prim_exec, loc, [kv; f])) ty_ret + ])) (Toption ty_ret); + acc + ])) acc_ty in + let update_fun = + mk_typed (Lambda (arg_name, arg_ty, loc, update_body, acc_ty)) + (Tlambda (arg_ty, acc_ty)) + in + let red = + mk_typed (Apply (Prim_map_reduce, loc, [ + update_fun; m; + mk_typed (Const (acc_ty, CMap [])) acc_ty + ])) acc_ty in + encode env red + | _ -> assert false + end + + (* Set.reduce (closure) -> {Set.reduce (::) |> List.rev |> List.reduce} *) + | Apply (Prim_set_reduce, loc, [f; s; acc]) -> + let f' = encode env f in + begin match get_type f'.ty with + | Tlambda _ -> + let s = encode env s in + let acc = encode env acc in + mk (Apply (Prim_set_reduce, loc, [f'; s; acc])) exp.ty + | Tclosure ((Ttuple [elt_ty; acc_ty], _), ty_ret) -> + let arg_name = uniq_ident env "arg" in + let elts_ty = Tlist elt_ty in + let arg_ty = Ttuple [elt_ty; elts_ty] in + let arg = mk_typed (Var (arg_name, loc, [])) arg_ty in + let elt = + mk_typed (Apply(Prim_tuple_get, loc, [arg; mk_typed_nat 0])) elt_ty in + let acc_elts = + mk_typed + (Apply(Prim_tuple_get, loc, [arg; mk_typed_nat 1])) elts_ty in + let gather_body = + mk_typed (Apply(Prim_Cons, loc, [elt; acc_elts])) elts_ty in + let gather_fun = + mk_typed (Lambda (arg_name, arg_ty, loc, gather_body, elts_ty)) + (Tlambda (arg_ty, elts_ty)) + in + let rev_elts = + mk_typed (Apply(Prim_set_reduce, loc, + [gather_fun; s; mk_typed_nil elts_ty])) + elts_ty + in + let elts = mk_typed (Apply(Prim_list_rev, loc, [rev_elts])) elts_ty in + let red = mk_typed + (Apply(Prim_list_reduce, loc, [f; elts; acc])) acc_ty in + encode env red + | _ -> assert false + end + + | Apply (prim, loc, args) -> + encode_apply env prim loc args exp.ty + + | MatchOption (arg, loc, ifnone, name, ifsome) -> + let arg = encode env arg in + let name_ty = match arg.ty with + | Toption ty -> ty + | _ -> assert false + in + let env = maybe_reset_vars env arg.transfer in + let ifnone = encode env ifnone in + let (new_name, env, count) = new_binding env name name_ty in + let ifsome = encode env ifsome in + mk (MatchOption (arg, loc, ifnone, new_name, ifsome)) exp.ty + + | MatchNat (arg, loc, plus_name, ifplus, minus_name, ifminus) -> + let arg = encode env arg in + let env = maybe_reset_vars env arg.transfer in + let (plus_name, env2, count_p) = new_binding env plus_name Tnat in + let ifplus = encode env2 ifplus in + let (minus_name, env3, count_m) = new_binding env minus_name Tnat in + let ifminus = encode env3 ifminus in + (* check_used env plus_name loc count_p; *) + (* check_used env minus_name loc count_m; *) + mk (MatchNat (arg, loc, plus_name, ifplus, minus_name, ifminus)) exp.ty + + | Loop (name, loc, body, arg) -> + let arg = encode env arg in + let env = maybe_reset_vars env arg.transfer in + let (new_name, env, count) = new_binding env name arg.ty in + let body = encode env body in + (* check_used env name loc count; *) + mk (Loop (new_name, loc, body, arg)) exp.ty + + | MatchList (arg, loc, head_name, tail_name, ifcons, ifnil) -> + let arg = encode env arg in + let elt_ty = match arg.ty with + | Tlist ty -> ty + | _ -> assert false + in + let env = maybe_reset_vars env arg.transfer in + let ifnil = encode env ifnil in + let (new_head_name, env, count) = new_binding env head_name elt_ty in + let (new_tail_name, env, count) = new_binding env tail_name arg.ty in + let ifcons = encode env ifcons in + (* check_used env head_name loc count; *) + (* check_used env tail_name loc count; *) + mk (MatchList (arg, loc, new_head_name, new_tail_name, ifcons, ifnil)) + exp.ty + + | Lambda (arg_name, arg_type, loc, body, _) -> + 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 + 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 = encode env lambda_body in + (* check_used env lambda_arg_name loc arg_count; *) + let ty = Tlambda (lambda_arg_type, body.ty) in + mk (Lambda (new_arg_name, lambda_arg_type, loc, body, body.ty)) ty + else + (* create closure with environment *) + let env, arg_name, arg_type, call_env = + env_for_clos env loc bvs arg_name arg_type in + let body = encode env body in + (* begin match env.clos_env with *) + (* | None -> () *) + (* | Some clos_env -> *) + (* Format.eprintf "--- Closure %s ---@." arg_name; *) + (* StringMap.iter (fun name (e, (cpt_in, cpt_out)) -> *) + (* Format.eprintf "%s -> %s , (%d, %d)@." *) + (* name (LiquidPrinter.Liquid.string_of_code e) !cpt_in !cpt_out *) + (* ) clos_env.env_bindings *) + (* end; *) + let desc = + Closure (arg_name, arg_type, loc, call_env, body, body.ty) in + let call_env_type = match call_env with + | [] -> assert false + | [_, t] -> t.ty + | _ -> Ttuple (List.map (fun (_, t) -> t.ty) call_env) + in + let ty = Tclosure ((lambda_arg_type, call_env_type), body.ty) in + mk desc ty + + | 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 = StringMap.find ty_name env.env.types in + let len = List.length (match record_ty with + | Trecord rtys -> rtys + | _ -> assert false) in + let t = Array.make len const_unit in + List.iteri (fun i (label, exp) -> + let ty_name', label_pos, ty = StringMap.find label env.env.labels in + let exp = encode env exp in + t.(label_pos) <- exp; + ) lab_x_exp_list; + let args = Array.to_list t in + let ty = Ttype (ty_name, record_ty) in + let desc = Apply(Prim_tuple, loc, args) in + mk desc ty + + | Constructor(loc, Constr constr, arg) -> + let ty_name, arg_ty = StringMap.find constr env.env.constrs in + let arg = encode env arg in + let constr_ty = StringMap.find ty_name env.env.types in + let ty = Ttype (ty_name, constr_ty) in + let exp = + match constr_ty with + | Tsum constrs -> + let rec iter constrs orty = + match constrs, orty with + | [], _ -> assert false + | [c, _], orty -> + assert (c = constr); + arg + (* | (c, ty, left_ty, right_ty) :: constrs -> *) + | (c, cty) :: constrs, orty -> + let left_ty, right_ty = match orty with + | Tor (left_ty, right_ty) -> left_ty, right_ty + | _ -> assert false + in + 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 right_ty in + Apply(Prim_Right, loc, [arg; unused env left_ty]) + in + mk desc orty + in + iter constrs (encode_type ~keepalias:false ty) + | _ -> assert false + in + mk exp.desc ty + + | Constructor(loc, Left right_ty, arg) -> + let arg = encode env arg in + let ty = Tor(arg.ty, right_ty) in + let desc = Apply(Prim_Left,loc,[arg; unused env right_ty]) in + mk desc ty + + | Constructor(loc, Right left_ty, arg) -> + let arg = encode env arg in + let ty = Tor(left_ty, arg.ty) in + let desc = Apply(Prim_Right,loc,[arg; unused env left_ty]) in + mk desc ty + + | 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 + + | MatchVariant (arg, loc, cases) -> + let arg = encode env arg in + let constrs = match get_type arg.ty with + | Tsum constrs -> constrs + | Tor (left_ty, right_ty) -> + [ "Left", left_ty; "Right", right_ty] + | _ -> assert false + in + let cases = List.map (fun case -> + let c, var, e = match case with + | CConstr (c, []), e -> c, "_", e + | CConstr (c, [var]), e -> c, var, e + | CAny, _ | CConstr _, _ -> assert false + in + let var_ty = List.assoc c constrs in + let (var, env, _) = new_binding env var var_ty in + let e = encode env e in + (CConstr (c, [var]), e) + ) cases + in + mk (MatchVariant (arg, loc, cases)) exp.ty + + | And (loc, e1, e2) | Or (loc, e1, e2) + | Implies (loc, e1, e2) | Equiv (loc, e1, e2) -> + let e1 = encode env e1 in + let e2 = encode env e2 in + let desc = match exp.desc with + | And _ -> And (loc, e1, e2) + | Or _ -> Or (loc, e1, e2) + | Implies _ -> Implies (loc, e1, e2) + | Equiv _ -> Equiv (loc, e1, e2) + | _ -> assert false + in + mk desc Tbool + + | Forall (loc, qvs, e) | Exists (loc, qvs, e) -> + let rvars, env = List.fold_left (fun (rvars, env) (v, ty) -> + let (new_v, env, _) = new_binding env v ty in + (new_v, ty) :: rvars, env + ) ([], env) qvs + in + let vars = List.rev rvars in + let e = encode env e in + let desc = match exp.desc with + | Forall _ -> Forall (loc, vars, e) + | Exists _ -> Exists (loc, vars, e) + | _ -> assert false + in + mk desc Tbool + + +and encode_apply env prim loc args ty = + let args = List.map (encode env) args in + match prim, args with + | Prim_exec, [ x; { ty = Tclosure (_, ty) | Tlambda (_,ty) } ] -> + mk (Apply (prim, loc, args)) ty + + | Prim_tuple_get, [ { ty = tuple_ty }; + { desc = Const (_, (CInt n | CNat n)) }] -> + let tuple = match (get_type tuple_ty) with + | Ttuple tuple -> tuple + | Trecord rtys -> List.map snd rtys + | _ -> assert false + in + let n = LiquidPrinter.int_of_integer n in + let size = List.length tuple in + let prim = + if size = n + 1 then + Prim_tuple_get_last + else + Prim_tuple_get + in + let ty = List.nth tuple n in + mk (Apply (prim, loc, args)) ty + + | Prim_tuple_set, [ { ty = tuple_ty }; + { desc = Const (_, (CInt n | CNat n)) }; + { ty } ] -> + let tuple = match (get_type tuple_ty) with + | Ttuple tuple -> tuple + | Trecord rtys -> List.map snd rtys + | _ -> assert false + in + let n = LiquidPrinter.int_of_integer n in + let size = List.length tuple in + let prim = + if size = n + 1 then + Prim_tuple_set_last + else + Prim_tuple_set + in + let ty = tuple_ty in + mk (Apply (prim, loc, args)) ty + + | _ -> mk (Apply (prim, loc, args)) ty + +let encode_spec env env_ensures = function + | Requires f -> Requires (encode env f) + | Ensures f -> Ensures (encode env_ensures f) + | Fails f -> Fails (encode env f) + +let encode_contract ~warnings env contract = + let env = + { + warnings; + allow_spec = false; + in_post = false; + counter = ref 0; + vars = StringMap.empty; + to_inline = ref StringMap.empty; + env = env; + clos_env = None; + contract; + } in + + (* "storage/1" *) + let (_ , env, _) = new_binding env "storage" contract.storage in + (* "parameter/2" *) + let (_, env, _) = new_binding env "parameter" contract.parameter in + + let (_, env_ensures, _) = new_binding env "@storage" contract.storage in + let (_, env_ensures, _) = new_binding env_ensures "@result" contract.return in + + let code = encode env contract.code in + let spec = List.map (encode_spec env env_ensures) contract.spec in + { contract with code; spec }, ! (env.to_inline) + + +let encode_code ~warnings env contract code = + let env = + { + warnings; + allow_spec = false; + in_post = false; + counter = ref 0; + vars = StringMap.empty; + to_inline = ref StringMap.empty; + env = env; + clos_env = None; + contract ; + } in + + encode env code diff --git a/tools/liquidity/liquidEncode.mli b/tools/liquidity/liquidEncode.mli new file mode 100644 index 00000000..5520b21b --- /dev/null +++ b/tools/liquidity/liquidEncode.mli @@ -0,0 +1,19 @@ +(**************************************************************************) +(* *) +(* Copyright (c) 2017 . *) +(* Fabrice Le Fessant, OCamlPro SAS *) +(* *) +(* All rights reserved. No warranty, explicit or implicit, provided. *) +(* *) +(**************************************************************************) + +open LiquidTypes + +val encode_type : ?keepalias:bool -> datatype -> datatype + +val encode_contract : + warnings:bool -> env -> typed_contract -> + encoded_contract * encoded_exp StringMap.t + +val encode_code : + warnings:bool -> env -> syntax_contract -> typed_exp -> encoded_exp diff --git a/tools/liquidity/liquidFromOCaml.ml b/tools/liquidity/liquidFromOCaml.ml index 1a511b01..a383c32b 100644 --- a/tools/liquidity/liquidFromOCaml.ml +++ b/tools/liquidity/liquidFromOCaml.ml @@ -28,9 +28,11 @@ let () = "else", ELSE; "end", END; (* "exception", EXCEPTION; *) + "exists", EXISTS; (* "external", EXTERNAL; *) "false", FALSE; "for", FOR; + "forall", FORALL; "fun", FUN; "function", FUNCTION; (* "functor", FUNCTOR; *) @@ -80,28 +82,10 @@ let () = (* The minimal version of liquidity files that are accepted by this compiler *) -let minimal_version = 0.1 -(* -let contract - (parameter : timestamp) - (storage: (string * timestamp * (tez * tez) * - ( (unit,unit) contract * - (unit, unit) contract * - (unit, unit) contract)) ) - [%return : unit] = - ... - *) +let minimal_version = 0.13 (* 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 = - ... - *) +let maximal_version = 0.13 open Asttypes @@ -183,8 +167,8 @@ let rec translate_type env typ = | { ptyp_desc = Ptyp_constr ({ txt = Lident "map" }, [parameter_type; return_type]) } -> Tmap (translate_type env parameter_type, translate_type env return_type) - | { ptyp_desc = Ptyp_constr ({ txt = Lident "lambda" }, - [parameter_type; return_type]) } -> + + | { ptyp_desc = Ptyp_arrow (_, parameter_type, return_type) } -> Tlambda (translate_type env parameter_type, translate_type env return_type) | { ptyp_desc = Ptyp_tuple types } -> @@ -193,9 +177,7 @@ let rec translate_type env typ = | { ptyp_desc = Ptyp_constr ({ txt = Lident ty_name }, []) } -> begin try - match StringMap.find ty_name env.types with - | ty, Type_alias -> ty - | ty, _ -> Ttype (ty_name, ty) + Ttype (ty_name, StringMap.find ty_name env.types) with Not_found -> unbound_type typ.ptyp_loc ty_name end @@ -221,11 +203,28 @@ let rec translate_const env exp = CInt (LiquidPrinter.integer_of_liq s), Some Tint | { pexp_desc = Pexp_constant (Pconst_integer (s, Some 'p')) } -> CNat (LiquidPrinter.integer_of_liq s), Some Tnat + | { pexp_desc = Pexp_constant (Pconst_integer (s, Some '\231')) } -> CTez (LiquidPrinter.tez_of_liq s), Some Ttez | { pexp_desc = Pexp_constant (Pconst_float (s, Some '\231')) } -> CTez (LiquidPrinter.tez_of_liq s), Some Ttez + (* Timestamps *) + | { pexp_desc = Pexp_constant (Pconst_integer (s, Some '\232')) } -> + CTimestamp (ISO8601.of_string s), Some Ttimestamp + + (* Key_hash *) + | { pexp_desc = Pexp_constant (Pconst_integer (s, Some '\233')) } -> + CKey_hash s, Some Tkey_hash + + (* Key *) + | { pexp_desc = Pexp_constant (Pconst_integer (s, Some '\234')) } -> + CKey s, Some Tkey + + (* Signature *) + | { pexp_desc = Pexp_constant (Pconst_integer (s, Some '\235')) } -> + CSignature s, Some Tkey + | { pexp_desc = Pexp_constant (Pconst_string (s, None)) } -> CString s, Some Tstring @@ -353,22 +352,6 @@ let rec translate_const env exp = LiquidCheck.check_const_type ~to_tez:LiquidPrinter.tez_of_liq loc ty cst, Some ty | Some ty_infer -> LiquidCheck.check_const_type ~to_tez:LiquidPrinter.tez_of_liq loc ty cst, Some ty - (* - if ty <> ty_infer then begin - let cst = - match ty, cst with - | Ttez, CString s -> CTez s - | Tkey, CString s -> CKey s - | Tsignature, CString s -> CSignature s - | Tint, CNat s -> CInt s - | _ -> - error_loc exp.pexp_loc "constant type mismatch"; - in - cst, Some ty - end - else - cst, Some ty - *) end | _ -> raise NotAConstant @@ -388,12 +371,13 @@ and translate_pair exp = | Pexp_tuple [e1; e2] -> (e1, e2) | _ -> error_loc exp.pexp_loc "pair expected" -let mk desc = { desc; ty = (); bv = StringSet.empty; fail = false } -let deconstruct_pat env pat = - let rec deconstruct_pat_aux acc indexes = function +let mk desc = mk desc () + +let vars_info_pat env pat = + let rec vars_info_pat_aux acc indexes = function | { ppat_desc = Ppat_constraint (pat, ty) } -> - let acc, _ = deconstruct_pat_aux acc indexes pat in + let acc, _ = vars_info_pat_aux acc indexes pat in acc, translate_type env ty | { ppat_desc = Ppat_var { txt = var; loc } } -> @@ -405,7 +389,7 @@ let deconstruct_pat env pat = | { 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 + let acc, ty = vars_info_pat_aux acc (i :: indexes) pat in i + 1, acc, ty :: tys ) (0, acc, []) pats in @@ -414,7 +398,7 @@ let deconstruct_pat env pat = | { ppat_loc } -> error_loc ppat_loc "cannot deconstruct this pattern" in - deconstruct_pat_aux [] [] pat + vars_info_pat_aux [] [] pat let access_of_deconstruct var_name loc indexes = let a = mk (Var (var_name, loc, [])) in @@ -425,6 +409,22 @@ let access_of_deconstruct var_name loc indexes = ])) ) indexes a +let deconstruct_pat env pat e = + let vars_infos, ty = vars_info_pat env pat in + match vars_infos with + | [] -> assert false + | [v, _loc, []] -> v, ty, e + | _ -> + let var_name = + String.concat "_" (List.rev_map (fun (v,_,_) -> v) vars_infos) in + let e = + List.fold_left (fun e (v, loc, indexes) -> + let access = access_of_deconstruct var_name loc indexes in + mk (Let (v, loc, access, e)) + ) e vars_infos + in + var_name, ty, e + let rec translate_code env exp = let desc = match exp with @@ -469,11 +469,9 @@ let rec translate_code env exp = { ppat_desc = Ppat_tuple [ - { ppat_desc = Ppat_var { txt = result } }; - { ppat_desc = Ppat_var { txt = - ("storage" | "_storage")as storage_name - } }; - ] + { ppat_desc = (Ppat_any | Ppat_var _) as res}; + { ppat_desc = (Ppat_any | Ppat_var _) as sto}; + ] }; pvb_expr = { pexp_desc = @@ -490,6 +488,16 @@ let rec translate_code env exp = ]) } } ], body) } -> + let result = match res with + | Ppat_any -> "_" + | Ppat_var { txt = result } -> result + | _ -> assert false + in + let storage_name = match sto with + | Ppat_any -> "_" + | Ppat_var { txt = storage_name } -> storage_name + | _ -> assert false + in LetTransfer (storage_name, result, loc_of_loc exp.pexp_loc, translate_code env contract_exp, @@ -501,24 +509,10 @@ let rec translate_code env exp = | { pexp_desc = Pexp_let (Nonrecursive, [ { pvb_pat = pat; pvb_expr = var_exp; - } ], body); pexp_loc } -> - - let vars_infos, _ = deconstruct_pat env pat in + } ], body) } -> 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 + let var_name, _, body = deconstruct_pat env pat body in + Let (var_name, loc_of_loc pat.ppat_loc, exp, body) | { pexp_desc = Pexp_sequence (exp1, exp2) } -> Seq (translate_code env exp1, translate_code env exp2) @@ -542,15 +536,85 @@ let rec translate_code env exp = | { pexp_desc = Pexp_apply ( - exp, - args); pexp_loc = loc } -> - let exp = translate_code env exp in - Apply(Prim_unknown, loc_of_loc loc, exp :: List.map ( - function (Nolabel, exp) -> - translate_code env exp - | (_, { pexp_loc }) -> - error_loc pexp_loc "in arg" - ) args) + { pexp_desc = Pexp_ident ({ txt = Lident "/\\"}) }, + [Nolabel, e1; Nolabel, e2]); pexp_loc = loc } -> + let e1, e2 = translate_code env e1, translate_code env e2 in + And(loc_of_loc loc, e1, e2) + + | { pexp_desc = + Pexp_apply ( + { pexp_desc = Pexp_ident ({ txt = Lident "\\/"}) }, + [Nolabel, e1; Nolabel, e2]); pexp_loc = loc } -> + let e1, e2 = translate_code env e1, translate_code env e2 in + Or(loc_of_loc loc, e1, e2) + + | { pexp_desc = + Pexp_apply ( + { pexp_desc = Pexp_ident ({ txt = Lident "=>"}) }, + [Nolabel, e1; Nolabel, e2]); pexp_loc = loc } -> + let e1, e2 = translate_code env e1, translate_code env e2 in + Implies(loc_of_loc loc, e1, e2) + + | { pexp_desc = + Pexp_apply ( + { pexp_desc = Pexp_ident ({ txt = Lident "<=>"}) }, + [Nolabel, e1; Nolabel, e2]); pexp_loc = loc } -> + let e1, e2 = translate_code env e1, translate_code env e2 in + Equiv(loc_of_loc loc, e1, e2) + + | { pexp_desc = + Pexp_apply ( + exp, + args); pexp_loc = loc } -> + let exp = translate_code env exp in + (* Format.eprintf "aply>> %s@." (LiquidPrinter.Liquid.string_of_code exp); *) + Apply(Prim_unknown, loc_of_loc loc, exp :: List.map ( + function (Nolabel, exp) -> + translate_code env exp + | (_, { pexp_loc }) -> + error_loc pexp_loc "in arg" + ) args) + + | { pexp_desc = Pexp_extension ( + { txt = ("forall"| "exists") as q }, + PPat ({ppat_desc = Ppat_tuple vars_pat}, Some exp) + ); pexp_loc = loc } -> + let vars = List.map (function + | { ppat_desc = Ppat_constraint ( + { ppat_desc = Ppat_var { txt = v } }, ty) } -> + v, translate_type env ty + | { ppat_loc } -> + error_loc ppat_loc + "quantified variable must be of the form \"(v : ty)\"" + ) vars_pat + in + let e = translate_code env exp in + begin match q with + | "forall" -> Forall (loc_of_loc loc, vars, e) + | "exists" -> Exists (loc_of_loc loc, vars, e) + | _ -> assert false + end + + | { pexp_desc = Pexp_extension ( + { txt = "nat" }, + PStr [{ pstr_desc = Pstr_eval ( + { pexp_desc = Pexp_match (e, cases); pexp_loc }, + []) + }] + )} -> + let e = translate_code env e in + let cases = List.map (translate_case env) cases in + begin + match cases with + | [ CConstr ("Plus", [p]), ifplus; CConstr ("Minus", [m]), ifminus ] + | [ CConstr ("Minus", [m]), ifminus; CConstr ("Plus", [p]), ifplus ] -> + MatchNat(e, loc_of_loc pexp_loc, p, ifplus, m, ifminus) + | [ CConstr ("Plus", [p]), ifplus; CAny, ifminus ] -> + MatchNat(e, loc_of_loc pexp_loc, p, ifplus, "_", ifminus) + | [ CConstr ("Minus", [m]), ifminus; CAny, ifplus ] -> + MatchNat(e, loc_of_loc pexp_loc, "_", ifplus, m, ifminus) + | _ -> error_loc pexp_loc "match%nat patterns are Plus _, Minus _" + end | { pexp_desc = Pexp_match (e, cases); pexp_loc } -> let e = translate_code env e in @@ -577,26 +641,10 @@ let rec translate_code env exp = | { pexp_desc = Pexp_fun (Nolabel, None, pat, body_exp) } -> let body_exp = translate_code env body_exp in - 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 + let arg_name, arg_type, body_exp = deconstruct_pat env pat body_exp in + Lambda (arg_name, arg_type, loc_of_loc exp.pexp_loc, + body_exp, + Tunit) (* not yet inferred *) | { pexp_desc = Pexp_record (lab_x_exp_list, None) } -> let lab_x_exp_list = @@ -751,13 +799,15 @@ and translate_case env case = (CConstr (name, []), e) | { ppat_desc = Ppat_construct ( - { txt = Lident name } , + { txt = Lident "::" } , Some { ppat_desc = Ppat_tuple [ p1; p2 ]} ) } -> - (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) + (CConstr ("::", [var_of_pat p1; var_of_pat p2]), e) + + | { ppat_desc = Ppat_construct ({ txt = Lident name } , Some pat) } -> + let var_name, _, e = deconstruct_pat env pat e in + (CConstr (name, [var_name]), e) + | { ppat_loc } -> error_loc ppat_loc "bad pattern" @@ -779,7 +829,19 @@ let rec inline_funs exp = function } in inline_funs f_in_exp funs -let rec translate_head env ext_funs head_exp args = +let translate_specs env l = + List.map (function + | { txt = "requires" }, PStr [{ pstr_desc = Pstr_eval (exp, [])}] -> + Requires (translate_code env exp) + | { txt = "ensures" }, PStr [{ pstr_desc = Pstr_eval (exp, [])}] -> + Ensures (translate_code env exp) + | { txt = "fails" }, PStr [{ pstr_desc = Pstr_eval (exp, [])}] -> + Fails (translate_code env exp) + | { txt; loc }, _ -> + error_loc loc ("bad specification: " ^ txt) + ) l + +let rec translate_head env ext_funs head_exp args specs = match head_exp with | { pexp_desc = Pexp_fun ( @@ -796,13 +858,13 @@ 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) specs | { 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 + if not (eq_types sto_ty storage) then error_loc pexp_loc "Second component of return type must be identical to storage type"; ret_ty @@ -810,7 +872,9 @@ let rec translate_head env ext_funs head_exp args = error_loc pexp_loc "return type must be a product of some type and the storage type" in + let nspecs = translate_specs env return_type.ptyp_attributes in translate_head env ext_funs head_exp (("return", return) :: args) + (specs @ nspecs) | { pexp_desc = Pexp_fun ( @@ -820,7 +884,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) specs | { pexp_desc = Pexp_fun ( @@ -839,56 +903,44 @@ let rec translate_head env ext_funs head_exp args = let code = translate_code env (inline_funs exp ext_funs) in { code; + spec = specs; parameter = List.assoc "parameter" args; storage = List.assoc "storage" args; return = List.assoc "return" args; } let translate_record ty_name labels env = - let map = ref StringMap.empty in - let tys = List.mapi - (fun i pld -> - let label = pld.pld_name.txt in - if StringMap.mem label env.labels then - error_loc pld.pld_loc "label already defined"; - - let ty = translate_type env pld.pld_type in - env.labels <- StringMap.add label (ty_name, i, ty) env.labels; - map := StringMap.add label i !map; - ty) labels + let rtys = List.mapi + (fun i pld -> + let label = pld.pld_name.txt in + if StringMap.mem label env.labels then + error_loc pld.pld_loc "label already defined"; + + let ty = translate_type env pld.pld_type in + env.labels <- StringMap.add label (ty_name, i, ty) env.labels; + label, ty) labels in - let ty = Ttuple tys in - env.types <- StringMap.add ty_name (ty, Type_record (tys,!map)) env.types + let ty = Trecord rtys in + env.types <- StringMap.add ty_name ty env.types let translate_variant ty_name constrs env = - let constrs = List.map - (fun pcd -> - let constr = pcd.pcd_name.txt in - if StringMap.mem constr env.constrs then - error_loc pcd.pcd_loc "constructor already defined"; - - let ty = match pcd.pcd_args with - | Pcstr_tuple [ ty ] -> translate_type env ty - | Pcstr_tuple [] -> Tunit - | Pcstr_tuple tys -> Ttuple (List.map (translate_type env) tys) - | Pcstr_record _ -> error_loc pcd.pcd_loc "syntax error" - in - env.constrs <- StringMap.add constr (ty_name, ty) env.constrs; - constr, ty) constrs - in - - let rec iter constrs = - match constrs with - | [] -> assert false - | [ constr, ty ] -> ty, [constr, ty, ty, ty] - | (constr, left_ty) :: constrs -> - let right_ty, right_constrs = iter constrs in - let ty = Tor (left_ty, right_ty) in - ty, (constr, ty, left_ty, right_ty) :: right_constrs + (fun pcd -> + let constr = pcd.pcd_name.txt in + if StringMap.mem constr env.constrs then + error_loc pcd.pcd_loc "constructor already defined"; + + let ty = match pcd.pcd_args with + | Pcstr_tuple [ ty ] -> translate_type env ty + | Pcstr_tuple [] -> Tunit + | Pcstr_tuple tys -> Ttuple (List.map (translate_type env) tys) + | Pcstr_record _ -> error_loc pcd.pcd_loc "syntax error" + in + env.constrs <- StringMap.add constr (ty_name, ty) env.constrs; + constr, ty) constrs in - let ty, constrs = iter constrs in - env.types <- StringMap.add ty_name (ty, Type_variant constrs) env.types + let ty = Tsum constrs in + env.types <- StringMap.add ty_name ty env.types let check_version = function | { pexp_desc = Pexp_constant (Pconst_float (s, None)); pexp_loc } -> @@ -925,7 +977,7 @@ let rec translate_structure funs env ast = ]) } ] ), []) } :: _ast (* TODO *) -> - translate_head env funs head_exp default_args + translate_head env funs head_exp default_args [] | { pstr_desc = Pstr_value ( @@ -981,7 +1033,7 @@ let rec translate_structure funs env ast = } ]) } :: ast -> let ty = translate_type env ct in - env.types <- StringMap.add ty_name (ty, Type_alias) env.types; + env.types <- StringMap.add ty_name ty env.types; translate_structure funs env ast | [] -> @@ -1001,9 +1053,9 @@ let predefined_constructors = "None", ("'a option", Tunit); "::", ("'a list", Tunit); "[]", ("'a list", Tunit); - "Left", ("'a variant", Tunit); - "Right", ("'a variant", Tunit); - "Source", ("'a contract", Tunit); + "Left", ("('a, 'b) variant", Tunit); + "Right", ("('a, 'b) variant", Tunit); + "Source", ("('a, 'b) contract", Tunit); ] let predefined_types = @@ -1012,18 +1064,20 @@ let predefined_types = (* Enter predefined types with dummy-info to prevent the user from overriding them *) [ - "int", (Tunit, Type_variant []); - "unit", (Tunit, Type_variant []); - "bool", (Tunit, Type_variant []); - "nat", (Tunit, Type_variant []); - "tez", (Tunit, Type_variant []); - "string", (Tunit, Type_variant []); - "key", (Tunit, Type_variant []); - "signature", (Tunit, Type_variant []); - "option", (Tunit, Type_variant []); - "list", (Tunit, Type_variant []); - "map", (Tunit, Type_variant []); - "set", (Tunit, Type_variant []); + "int", Tunit; + "unit", Tunit; + "bool", Tunit; + "nat", Tunit; + "tez", Tunit; + "string", Tunit; + "key", Tunit; + "signature", Tunit; + "option", Tunit; + "list", Tunit; + "map", Tunit; + "set", Tunit; + "variant", Tunit; + "contract", Tunit; ] let initial_env filename = diff --git a/tools/liquidity/liquidFromOCaml.mli b/tools/liquidity/liquidFromOCaml.mli index 475b12a4..c097af16 100644 --- a/tools/liquidity/liquidFromOCaml.mli +++ b/tools/liquidity/liquidFromOCaml.mli @@ -11,11 +11,10 @@ open LiquidTypes val initial_env : string -> env val translate : filename:string -> - Parsetree.structure -> syntax_exp contract * env + Parsetree.structure -> syntax_contract * env val read_file : string -> Parsetree.structure -val translate_expression : - LiquidTypes.env -> Parsetree.expression -> LiquidTypes.syntax_exp +val translate_expression : env -> Parsetree.expression -> syntax_exp val structure_of_string : ?filename:string -> string -> Parsetree.structure diff --git a/tools/liquidity/liquidInterp.ml b/tools/liquidity/liquidInterp.ml index de0267ab..a8daca33 100644 --- a/tools/liquidity/liquidInterp.ml +++ b/tools/liquidity/liquidInterp.ml @@ -23,9 +23,6 @@ let node loc kind args prevs = Hashtbl.add nodes num node; node -let bv = StringSet.empty -let mk desc = { desc ; ty = (); bv; fail = false } - let fprint_stack msg fmt stack = Format.fprintf fmt "Stack %s:\n" msg; List.iter (fun node -> @@ -100,7 +97,8 @@ let rec merge_stacks if_stack end_node1 end_node2 stack1 stack2 = | Some node -> node.args <- List.rev node.args); stack with Exit -> - LiquidLoc.raise_error "interp error merging stacks:\n%a%a" + LiquidLoc.raise_error ~loc:end_node1.loc + "interp error merging stacks:\n%a%a" (fprint_stack "stack1 ") stack1 (fprint_stack "stack2 ") stack2 @@ -110,9 +108,41 @@ let interp contract = Hashtbl.clear nodes; let rec decompile_seq stack (seq : node) code = - match code with - | [] -> (stack, seq) - | ins :: code -> + match code, stack with + | [], _ -> (stack, seq) + + (* Special case for abs *) + | {ins=ABS; loc} :: {ins=INT} :: code, x :: stack -> + let n = node loc N_ABS [x] [seq] in + let stack, seq = n :: stack, n in + decompile_seq stack seq code + + (* Special case for match%nat *) + | {ins=DUP 1; loc} :: + {ins=ABS} :: + {ins=SWAP} :: + {ins=GE} :: + {ins=IF(ifplus, ifminus)} :: + code, + x :: stack -> + let if_node = node loc (N_UNKNOWN "IF_PLUS") [x] [seq] in + + let var0 = node ifplus.loc (N_IF_RESULT (if_node, 0)) [] [] in + let then_node = node ifplus.loc (N_IF_PLUS (if_node, var0)) [] [] in + let then_stack = var0 :: stack in + + let var0 = node ifminus.loc (N_IF_RESULT (if_node, 0)) [] [] in + let else_node = node ifminus.loc (N_IF_MINUS (if_node, var0)) [] [] in + let else_stack = var0 :: stack in + + let stack, seq = + decompile_if if_node stack + ifplus then_node then_stack + ifminus else_node else_stack + in + decompile_seq stack seq code + + | ins :: code, _ -> let stack, seq = decompile stack seq ins in decompile_seq stack seq code diff --git a/tools/liquidity/liquidInterp.mli b/tools/liquidity/liquidInterp.mli index a253f789..c71dff56 100644 --- a/tools/liquidity/liquidInterp.mli +++ b/tools/liquidity/liquidInterp.mli @@ -9,4 +9,4 @@ open LiquidTypes -val interp : loc_michelson contract -> node_exp contract +val interp : loc_michelson_contract -> node_contract diff --git a/tools/liquidity/liquidMain.ml b/tools/liquidity/liquidMain.ml index 6d77bbc2..108da37e 100644 --- a/tools/liquidity/liquidMain.ml +++ b/tools/liquidity/liquidMain.ml @@ -19,32 +19,45 @@ open LiquidTypes to Michelson. No type-checking yet. *) -let debug = ref (try - ignore (Sys.getenv "LIQUID_DEBUG"); true - with Not_found -> false) +let verbosity = ref (try + int_of_string (Sys.getenv "LIQUID_VERBOSITY") + with + | Not_found -> 0 + | _ -> 1 (* LIQUID_DEBUG not a number *) + ) let arg_peephole = ref true let arg_keepon = ref false +let arg_typeonly = ref false +let arg_parseonly = ref false let compile_liquid_file filename = let ocaml_ast = LiquidFromOCaml.read_file filename in - if !debug then + if !verbosity>0 then FileString.write_file (filename ^ ".ocaml") - (LiquidOCamlPrinter.contract_ast ocaml_ast); + (LiquidOCamlPrinter.contract_ast ocaml_ast); + if !arg_parseonly then exit 0; let syntax_ast, env = LiquidFromOCaml.translate filename ocaml_ast in - if !debug then + if !verbosity>0 then FileString.write_file (filename ^ ".syntax") (LiquidPrinter.Liquid.string_of_contract syntax_ast); - let typed_ast, to_inline = - LiquidCheck.typecheck_contract ~warnings:true env syntax_ast in - if !debug then - FileString.write_file (filename ^ ".typed") - (LiquidPrinter.Liquid.string_of_contract - typed_ast); - - let live_ast = LiquidSimplify.simplify_contract typed_ast to_inline in - if !debug then + let typed_ast = LiquidCheck.typecheck_contract + ~warnings:true env syntax_ast in + if !verbosity>0 then + FileString.write_file (filename ^ ".typed") + (LiquidPrinter.Liquid.string_of_contract_types + typed_ast); + let encoded_ast, to_inline = + LiquidEncode.encode_contract ~warnings:true env typed_ast in + if !verbosity>0 then + FileString.write_file (filename ^ ".encoded") + (LiquidPrinter.Liquid.string_of_encoded_contract + encoded_ast); + if !arg_typeonly then exit 0; + + let live_ast = LiquidSimplify.simplify_contract encoded_ast to_inline in + if !verbosity>0 then FileString.write_file (filename ^ ".simple") (LiquidPrinter.Liquid.string_of_contract live_ast); @@ -74,22 +87,25 @@ let compile_tezos_file filename = 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 + if !arg_parseonly then exit 0; + if !verbosity>0 then begin FileString.write_file (filename ^ ".dot") (LiquidDot.to_string c); let cmd = Ocamldot.dot2pdf_cmd (filename ^ ".dot") (filename ^ ".pdf") in if Sys.command cmd <> 0 then Printf.eprintf "Warning: could not generate pdf from .dot file\n%!"; end; + if !arg_typeonly then exit 0; let c = LiquidDecomp.decompile c in - if !debug then + if !verbosity>0 then FileString.write_file (filename ^ ".liq.pre") (LiquidPrinter.Liquid.string_of_contract c); let env = LiquidFromOCaml.initial_env filename in - let typed_ast, to_inline = - LiquidCheck.typecheck_contract ~warnings:false env c in + let typed_ast = LiquidCheck.typecheck_contract ~warnings:false env c in + let encode_ast, to_inline = + LiquidEncode.encode_contract ~warnings:false env typed_ast in (* Printf.eprintf "Inlining: %d\n%!" (StringMap.cardinal to_inline); *) - let live_ast = LiquidSimplify.simplify_contract typed_ast to_inline in + let live_ast = LiquidSimplify.simplify_contract encode_ast to_inline in let untyped_ast = LiquidUntype.untype_contract live_ast in let output = filename ^ ".liq" in FileString.write_file output @@ -104,7 +120,7 @@ let compile_tezos_file filename = () -let compile_file filename = +let handle_file filename = if Filename.check_suffix filename ".liq" then compile_liquid_file filename else @@ -115,9 +131,9 @@ let compile_file filename = exit 2 end -let compile_file filename = +let handle_file filename = try - compile_file filename + handle_file filename with (LiquidError _) as e -> if not !arg_keepon then raise e @@ -150,32 +166,35 @@ let main () = let work_done = ref false in let arg_list = Arg.align [ "-k", Arg.Set arg_keepon, " Continue on error"; + "--verbose", Arg.Unit (fun () -> incr verbosity), " Increment verbosity"; "--no-peephole", Arg.Clear arg_peephole, " Disable peephole optimizations"; + "--type-only", Arg.Set arg_typeonly, "Stop after type checking"; + "--parse-only", Arg.Set arg_parseonly, "Stop after parsing"; "--data", Arg.Tuple [ - Arg.String (fun s -> Data.contract := s); - Arg.String (fun s -> Data.parameter := s); - Arg.String (fun s -> Data.storage := s); - Arg.Unit (fun () -> - work_done := true; - Data.translate ()); - ], + Arg.String (fun s -> Data.contract := s); + Arg.String (fun s -> Data.parameter := s); + Arg.String (fun s -> Data.storage := s); + Arg.Unit (fun () -> + work_done := true; + Data.translate ()); + ], "FILE.liq PARAMETER STORAGE Translate to Michelson"; - ] @ LiquidToTezos.arg_list work_done + ] @ LiquidToTezos.arg_list work_done in let arg_usage = String.concat "\n" [ -"liquidity [OPTIONS] FILES"; -""; -"The liquidity compiler can translate files from Liquidity to Michelson"; -"and from Michelson to Liquidity. Liquidity files must end with the .liq"; -"extension. Michelson files must end with the .tz extension."; -""; -"Available options:"; - ] + "liquidity [OPTIONS] FILES"; + ""; + "The liquidity compiler can translate files from Liquidity to Michelson"; + "and from Michelson to Liquidity. Liquidity files must end with the .liq"; + "extension. Michelson files must end with the .tz extension."; + ""; + "Available options:"; + ] in - Arg.parse arg_list (fun s -> work_done := true; compile_file s) - arg_usage; + Arg.parse arg_list (fun s -> work_done := true; handle_file s) + arg_usage; if not !work_done then Arg.usage arg_list arg_usage diff --git a/tools/liquidity/liquidMichelson.ml b/tools/liquidity/liquidMichelson.ml index c909662d..f37f99a6 100644 --- a/tools/liquidity/liquidMichelson.ml +++ b/tools/liquidity/liquidMichelson.ml @@ -21,7 +21,7 @@ let dup n = {i=DUP n} (* n = size of preserved head of stack *) let dip n exprs = {i=DIP (n, seq exprs)} -let push ty cst = {i=PUSH (ty, cst)} +let push ty cst = {i=PUSH (LiquidEncode.encode_type ty, cst)} (* n = size of preserved head of stack *) let drop_stack n depth = @@ -77,9 +77,11 @@ let translate_code code = let env = StringMap.empty in let env = StringMap.add arg_name 0 env in let depth = 1 in + let arg_type = LiquidEncode.encode_type arg_type in + let res_type = LiquidEncode.encode_type res_type in let body = compile_no_transfer depth env body in [ {i=LAMBDA (arg_type, res_type, seq (body @ [ - {i=DIP_DROP (1,1)}]))} ], false + {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 @@ -87,27 +89,32 @@ let translate_code code = | [_, e] -> compile_no_transfer depth env e | _ -> compile_tuple depth env (List.rev_map snd call_env) in + let p_arg_type = LiquidEncode.encode_type p_arg_type in + let res_type = LiquidEncode.encode_type res_type in call_env_code @ (compile_desc depth env (Lambda (arg_name, p_arg_type, loc, body, res_type)) |> fst) @ [ ii PAIR ], false | If (cond, ifthen, ifelse) -> - let cond = compile_no_transfer depth env cond in - let (ifthen, transfer1) = compile depth env ifthen in - let (ifelse, transfer2) = compile depth env ifelse in - let (ifthen_end, ifelse_end) = - match transfer1, transfer2 with - | false, false -> [], [] - | true, true -> [], [] - (* We need to empty the stack before returning, keeping only - the last value *) - | true, false -> [], drop_stack 1 depth - | false, true -> drop_stack 1 depth, [] - in - cond @ [ {i= IF (seq (ifthen @ ifthen_end), - seq (ifelse @ ifelse_end) )}], - transfer1 || transfer2 + let cond, transfer1 = compile depth env cond in + let (depth, env) = + if transfer1 then (0, StringMap.empty) else (depth, env) + in + let (ifthen, transfer2) = compile depth env ifthen in + let (ifelse, transfer3) = compile depth env ifelse in + let (ifthen_end, ifelse_end) = + match transfer2, transfer3 with + | false, false -> [], [] + | true, true -> [], [] + (* We need to empty the stack before returning, keeping only + the last value *) + | true, false -> [], drop_stack 1 depth + | false, true -> drop_stack 1 depth, [] + in + cond @ [ {i= IF (seq (ifthen @ ifthen_end), + seq (ifelse @ ifelse_end) )}], + transfer1 || transfer2 || transfer3 | LetTransfer( storage_name, result_name, _loc, @@ -139,6 +146,9 @@ let translate_code code = f_env @ arg @ [ dip 1 [ dup 1; ii CAR; ii SWAP; ii CDR] ] @ [ ii PAIR ; ii EXEC ], false + | Apply (prim, _loc, ([_; { ty = Tlambda _ } ] as args)) -> + compile_prim depth env prim args, false + | Apply (prim, _loc, args) -> compile_prim depth env prim args, false @@ -152,7 +162,7 @@ let translate_code code = let depth = depth + 1 in let ifsome, transfer3 = compile depth env ifsome in let (ifnone_end, ifsome_end) = - match transfer1, transfer2 with + match transfer2, transfer3 with | false, false -> [], [ {i=DIP_DROP(1,1)} ] | true, true -> [], [] | true, false -> [], drop_stack 1 depth @@ -162,6 +172,29 @@ let translate_code code = seq (ifsome @ ifsome_end) )}], transfer1 || transfer2 || transfer3 + | MatchNat(arg, loc, plus_name, ifplus, minus_name, ifminus) -> + let arg, transfer1 = compile depth env arg in + let (depth, env) = + if transfer1 then (0, StringMap.empty) else (depth, env) + in + let env' = StringMap.add plus_name depth env in + let ifplus, transfer2 = compile (depth + 1) env' ifplus in + let env'' = StringMap.add minus_name depth env in + let ifminus, transfer3 = compile (depth + 1) env'' ifminus in + let depth = depth + 1 in + let (ifplus_end, ifminus_end) = + match transfer2, transfer3 with + | false, false -> [ {i=DIP_DROP(1,1)} ], [ {i=DIP_DROP(1,1)} ] + | true, true -> [], [] + | true, false -> [], drop_stack 1 depth + | false, true -> drop_stack 1 depth, [] + in + arg @ [ + dup 1; ii ABS; ii SWAP; ii GE; + {i=IF (seq (ifplus @ ifplus_end), + seq (ifminus @ ifminus_end) )}], + transfer1 || transfer2 || transfer3 + | MatchList(arg, loc, head_name, tail_name, ifcons, ifnil) -> let arg, transfer1 = compile depth env arg in let (depth, env) = @@ -173,7 +206,7 @@ let translate_code code = let depth = depth + 2 in let ifcons, transfer3 = compile depth env ifcons in let (ifnil_end, ifcons_end) = - match transfer1, transfer2 with + match transfer2, transfer3 with | false, false -> [], [ {i=DIP_DROP(1,2)} ] | true, true -> [], [] | true, false -> [], drop_stack 1 depth @@ -190,14 +223,14 @@ let translate_code code = in let has_transfer = ref false in let cases = List.map (function - | 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 - if transfer then has_transfer := true; - e, transfer, depth - | _ -> assert false) cases in - + | 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 + if transfer then has_transfer := true; + e, transfer, depth + | _ -> assert false) cases + in let rec iter cases = match cases with | [] -> assert false @@ -207,7 +240,7 @@ let translate_code code = | true, true -> [] | false, false -> [ {i=DIP_DROP(1,1)} ] | false, true -> assert false - | true, false -> drop_stack 1 (depth-1) + | true, false -> drop_stack 1 depth in let left = left @ left_end in match cases with @@ -216,7 +249,7 @@ let translate_code code = let right = iter cases in [ {i=IF_LEFT( seq left, seq right )} ] in - arg @ iter cases, !has_transfer + arg @ iter cases, transfer1 || !has_transfer | Loop (name, _loc, body, arg) -> let arg, transfer1 = compile depth env arg in @@ -238,6 +271,8 @@ let translate_code code = (* removed during typechecking, replaced by tuple *) | Record _ -> assert false | Constructor _ -> assert false + | And _ | Or _ | Implies _ | Equiv _ | Forall _ | Exists _ -> assert false + and compile_prim depth env prim args = match prim, args with @@ -284,27 +319,33 @@ set x n y = x + [ DUP; CAR; SWAP; CDR ]*n + | Prim_gas, _ -> [ ii STEPS_TO_QUOTA ] | Prim_Left, [ arg; { ty = right_ty }] -> - compile_no_transfer depth env arg @ - [ {i=LEFT right_ty} ] + let right_ty = LiquidEncode.encode_type right_ty in + compile_no_transfer depth env arg @ + [ {i=LEFT right_ty} ] | Prim_Left, _ -> assert false | Prim_Right, [ arg; { ty = left_ty } ] -> - compile_no_transfer depth env arg @ - [ {i=RIGHT left_ty} ] + let left_ty = LiquidEncode.encode_type left_ty in + compile_no_transfer depth env arg @ + [ {i=RIGHT left_ty} ] | Prim_Right, _ -> assert false | Prim_Source, [ { ty = from_ty }; { ty = to_ty } ] -> - [ {i=SOURCE (from_ty, to_ty)} ] + let from_ty = LiquidEncode.encode_type from_ty in + let to_ty = LiquidEncode.encode_type to_ty in + [ {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 - [ {i=PUSH (Tlist ty, CList[])} ] @ arg @ [ ii CONS ] + let ty = LiquidEncode.encode_type ty in + let arg = compile_no_transfer (depth+1) env arg in + [ {i=PUSH (Tlist ty, CList[])} ] @ arg @ [ ii CONS ] - (* Should be removed in LiquidCheck *) + (* Should be removed in LiquidEncode *) | Prim_unknown, _ + | Prim_old, _ | Prim_list_rev, _ -> assert false (* Should have disappeared *) @@ -368,7 +409,7 @@ the ending NIL is not annotated with a type *) | Prim_and, 2 -> [ ii AND ] | Prim_xor, 2 -> [ ii XOR ] | Prim_not, 1 -> [ ii NOT ] - | Prim_abs, 1 -> [ ii ABS ] + | Prim_abs, 1 -> [ ii ABS; ii INT ] | Prim_int, 1 -> [ ii INT ] | Prim_neg, 1 -> [ ii NEG ] | Prim_lsr, 2 -> [ ii LSR ] @@ -398,7 +439,7 @@ the ending NIL is not annotated with a type *) | Prim_Left|Prim_Right|Prim_Source|Prim_unused | Prim_coll_find|Prim_coll_update|Prim_coll_mem | Prim_coll_reduce|Prim_coll_map|Prim_coll_size - | Prim_list_rev), _ -> + | Prim_list_rev|Prim_old), _ -> (* already filtered out *) assert false @@ -491,4 +532,8 @@ let translate filename ~peephole contract = { contract with code } *) let translate contract = - { contract with code = translate_code contract.code } + { parameter = LiquidEncode.encode_type contract.parameter; + storage = LiquidEncode.encode_type contract.storage; + return = LiquidEncode.encode_type contract.return; + spec = (); + code = translate_code contract.code } diff --git a/tools/liquidity/liquidMichelson.mli b/tools/liquidity/liquidMichelson.mli index 983a2949..af607c0a 100644 --- a/tools/liquidity/liquidMichelson.mli +++ b/tools/liquidity/liquidMichelson.mli @@ -9,4 +9,4 @@ open LiquidTypes -val translate : typed_exp contract -> noloc_michelson contract +val translate : encoded_contract -> noloc_michelson_contract diff --git a/tools/liquidity/liquidPeephole.mli b/tools/liquidity/liquidPeephole.mli index 06f1fe6a..5fabe3bb 100644 --- a/tools/liquidity/liquidPeephole.mli +++ b/tools/liquidity/liquidPeephole.mli @@ -9,4 +9,4 @@ open LiquidTypes -val simplify : noloc_michelson contract -> noloc_michelson contract +val simplify : noloc_michelson_contract -> noloc_michelson_contract diff --git a/tools/liquidity/liquidPrinter.ml b/tools/liquidity/liquidPrinter.ml index c89010a2..93e604ee 100644 --- a/tools/liquidity/liquidPrinter.ml +++ b/tools/liquidity/liquidPrinter.ml @@ -125,6 +125,7 @@ module Michelson = struct | Tkey_hash -> Printf.bprintf b "key_hash" | Tsignature -> Printf.bprintf b "signature" | Ttuple tys -> bprint_type_pairs b indent tys + | Trecord _ | Tsum _ -> assert false | Tcontract (ty1, ty2) -> let indent = indent ^ " " in Printf.bprintf b "(contract\n%s" indent; @@ -256,6 +257,7 @@ module Michelson = struct bprint_const fmt b indent cst; ) csts; Printf.bprintf b "%c%s)" fmt.newline indent; + | CConstr _ | CRecord _ -> assert false and bprint_const_pairs fmt b indent tys = match tys with @@ -456,7 +458,100 @@ end module Liquid = struct - let rec bprint_type b indent ty = + let bprint_type_base expand definition b indent ty = + let rec bprint_type b indent ty = + match ty with + | Tfail -> Printf.bprintf b "failure" + | Tunit -> Printf.bprintf b "unit" + | Tbool -> Printf.bprintf b "bool" + | Tint -> Printf.bprintf b "int" + | Tnat -> Printf.bprintf b "nat" + | Ttez -> Printf.bprintf b "tez" + | 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 [] -> assert false + | Ttuple (ty :: tys) -> + Printf.bprintf b "("; + bprint_type b "" ty; + List.iter (fun ty -> + Printf.bprintf b " * "; + bprint_type b "" ty; + ) tys; + Printf.bprintf b ")"; + | Trecord [] -> assert false + | Trecord ((f, ty) :: rtys) -> + Printf.bprintf b "{ "; + Printf.bprintf b "%s: " f; + bprint_type b "" ty; + List.iter (fun (f, ty) -> + Printf.bprintf b "; %s: " f; + bprint_type b "" ty; + ) rtys; + Printf.bprintf b " }"; + | Tsum [] -> assert false + | Tsum ((c, ty) :: rtys) -> + Printf.bprintf b "%s of " c; + bprint_type b "" ty; + List.iter (fun (c, ty) -> + Printf.bprintf b " | %s of " c; + bprint_type b "" ty; + ) rtys; + | Tcontract (ty1, ty2) -> + Printf.bprintf b "("; + bprint_type b "" ty1; + Printf.bprintf b ", "; + bprint_type b "" ty2; + Printf.bprintf b ") contract"; + | Tor (ty1, ty2) -> + Printf.bprintf b "("; + bprint_type b "" ty1; + Printf.bprintf b ", "; + bprint_type b "" ty2; + Printf.bprintf b ") variant"; + | Toption ty -> + bprint_type b "" ty; + Printf.bprintf b " option"; + | Tlist ty -> + bprint_type b "" ty; + Printf.bprintf b " list"; + | Tset ty -> + bprint_type b "" ty; + Printf.bprintf b " set"; + | Tmap (ty1, ty2) -> + Printf.bprintf b "("; + bprint_type b "" ty1; + Printf.bprintf b ", "; + bprint_type b "" ty2; + Printf.bprintf b ") map"; + | Tlambda (ty1, ty2) -> + bprint_type b "" ty1; + Printf.bprintf b " -> "; + bprint_type b "" ty2; + | Tclosure ((ty_arg, ty_env), ty_r) -> + bprint_type b "" ty_arg; + Printf.bprintf b " {"; + bprint_type b "" ty_env; + Printf.bprintf b "}-> "; + bprint_type b "" ty_r; + | Ttype (ty_name, ty) when definition -> + Printf.bprintf b "%S = " ty_name; + bprint_type b "" ty; + | Ttype (ty_name, ty) when expand -> + bprint_type b "" ty; + | Ttype (ty_name, ty) -> + Printf.bprintf b "%s" ty_name + + in + bprint_type b indent ty + + let rec bprint_type ?(expand=false) ?(definition=false) b indent ty = + bprint_type_base expand definition b indent ty + + + let bprint_type2 b indent ty = let set = ref StringSet.empty in let todo = ref [None, ty] in let rec iter () = @@ -484,10 +579,76 @@ module Liquid = struct in iter () - let bprint_const b indent cst = - Michelson.bprint_const b indent cst - - let rec bprint_code ~debug b indent code = + let rec bprint_const b indent cst = + 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" (liq_of_tez s) + | CInt n -> Printf.bprintf b "%s" (liq_of_integer n) + | CNat n -> Printf.bprintf b "%s" (liq_of_integer n) + | CTimestamp s -> Printf.bprintf b "%s" s + | CBool v -> Printf.bprintf b "%b" v + | CUnit -> Printf.bprintf b "()" + | CNone -> Printf.bprintf b "None" + | CSome cst -> + Printf.bprintf b "(Some "; + bprint_const b "" cst; + Printf.bprintf b ")"; + | CLeft cst -> + Printf.bprintf b "(Left "; + bprint_const b "" cst; + Printf.bprintf b ")"; + | CRight cst -> + Printf.bprintf b "(Right "; + bprint_const b "" cst; + Printf.bprintf b ")"; + | CTuple [] -> assert false + | CTuple (c :: cs) -> + Printf.bprintf b "("; + bprint_const b "" c; + List.iter (fun c -> + Printf.bprintf b " * "; + bprint_const b "" c; + ) cs; + Printf.bprintf b ")"; + | CMap pairs -> + Printf.bprintf b "(Map ["; + Format.pp_print_list ~pp_sep:(fun fmt () -> Format.fprintf fmt "; ") + (fun _ (c1, c2) -> + bprint_const b "" c1; + Printf.bprintf b ", "; + bprint_const b "" c2) + (Format.formatter_of_buffer b) pairs; + Printf.bprintf b "])"; + | CList csts -> + Printf.bprintf b "["; + Format.pp_print_list ~pp_sep:(fun fmt () -> Format.fprintf fmt "; ") + (fun _ c -> bprint_const b "" c) + (Format.formatter_of_buffer b) csts; + Printf.bprintf b "]"; + | CSet csts -> + Printf.bprintf b "(Set ["; + Format.pp_print_list ~pp_sep:(fun fmt () -> Format.fprintf fmt "; ") + (fun _ c -> bprint_const b "" c) + (Format.formatter_of_buffer b) csts; + Printf.bprintf b "])" + | CConstr (c, cst) -> + Printf.bprintf b "(%s " c; + bprint_const b "" cst; + Printf.bprintf b ")"; + | CRecord labels -> + Printf.bprintf b "{"; + Format.pp_print_list ~pp_sep:(fun fmt () -> Format.fprintf fmt "; ") + (fun _ (f, cst) -> + Printf.bprintf b "%s = " f; + bprint_const b "" cst) + (Format.formatter_of_buffer b) labels; + Printf.bprintf b "}" + + + let rec bprint_code_base bprint_code_rec ~debug b indent code = if debug && not (StringSet.is_empty code.bv) then begin Printf.bprintf b "\n%s(*\n" indent; (* bprint_type b indent code.ty; *) @@ -500,20 +661,16 @@ module Liquid = struct | Let (name, _loc, exp, body) -> let indent2 = indent ^ " " in Printf.bprintf b "\n%slet %s =" indent name; - bprint_code ~debug b indent2 exp; + bprint_code_rec ~debug b indent2 exp; Printf.bprintf b "\n%sin" indent; - bprint_code ~debug b indent body + bprint_code_rec ~debug b indent body | Const (ty, cst) -> - let indent2 = indent ^ " " in - Printf.bprintf b "\n%s(const\n%s" indent indent2; - bprint_type b indent2 ty; - Printf.bprintf b "\n%s" indent2; - bprint_const b indent2 cst; - Printf.bprintf b ")"; + Printf.bprintf b "\n%s" indent; + bprint_const b indent cst; | SetVar (name, _loc, labels, e) -> let indent2 = indent ^ " " in Printf.bprintf b "\n%s(%s <-" indent (String.concat "." (name :: labels)); - bprint_code ~debug b indent2 e; + bprint_code_rec ~debug b indent2 e; Printf.bprintf b ")"; | Var (name, _loc, labels) -> Printf.bprintf b "\n%s%s" indent (String.concat "." (name :: labels)) @@ -522,62 +679,73 @@ module Liquid = struct (LiquidTypes.string_of_primitive prim); let indent2 = indent ^ " " in List.iter (fun exp -> - bprint_code ~debug b indent2 exp + bprint_code_rec ~debug b indent2 exp ) args; Printf.bprintf b ")" | If (cond, ifthen, ifelse) -> let indent2 = indent ^ " " in Printf.bprintf b "\n%sif" indent; - bprint_code ~debug b indent2 cond; + bprint_code_rec ~debug b indent2 cond; Printf.bprintf b "\n%sthen" indent; - bprint_code ~debug b indent2 ifthen; + bprint_code_rec ~debug b indent2 ifthen; Printf.bprintf b "\n%selse" indent; - bprint_code ~debug b indent2 ifelse; + bprint_code_rec ~debug b indent2 ifelse; | Seq (exp1, exp2) -> - bprint_code ~debug b indent exp1; + bprint_code_rec ~debug b indent exp1; Printf.bprintf b ";"; - bprint_code ~debug b indent exp2 + bprint_code_rec ~debug b indent exp2 | LetTransfer (storage, result, _loc, contract_exp, tez_exp, storage_exp, arg_exp, body) -> let indent2 = indent ^ " " in let indent4 = indent2 ^ " " in Printf.bprintf b "\n%slet %s, %s =" indent storage result; Printf.bprintf b "\n%sContract.call" indent2; - bprint_code ~debug b indent4 contract_exp; - bprint_code ~debug b indent4 tez_exp; - bprint_code ~debug b indent4 storage_exp; - bprint_code ~debug b indent4 arg_exp; + bprint_code_rec ~debug b indent4 contract_exp; + bprint_code_rec ~debug b indent4 tez_exp; + bprint_code_rec ~debug b indent4 storage_exp; + bprint_code_rec ~debug b indent4 arg_exp; Printf.bprintf b "\n%sin" indent; - bprint_code ~debug b indent body + bprint_code_rec ~debug b indent body | MatchOption (arg, _loc, ifnone, var, ifsome) -> let indent2 = indent ^ " " in let indent4 = indent2 ^ " " in Printf.bprintf b "\n%smatch " indent; - bprint_code ~debug b indent2 arg; + bprint_code_rec ~debug b indent2 arg; Printf.bprintf b " with\n"; Printf.bprintf b "\n%s| None ->\n" indent2; - bprint_code ~debug b indent4 ifnone; + bprint_code_rec ~debug b indent4 ifnone; Printf.bprintf b "\n%s| Some %s ->\n" indent2 var; - bprint_code ~debug b indent4 ifsome; + bprint_code_rec ~debug b indent4 ifsome; + () + | MatchNat (arg, _loc, p, ifplus, m, ifminus) -> + let indent2 = indent ^ " " in + let indent4 = indent2 ^ " " in + Printf.bprintf b "\n%smatch%%nat " indent; + bprint_code_rec ~debug b indent2 arg; + Printf.bprintf b " with\n"; + Printf.bprintf b "\n%s| Plus %s ->\n" indent2 p; + bprint_code_rec ~debug b indent4 ifplus; + Printf.bprintf b "\n%s| Minus %s ->\n" indent2 m; + bprint_code_rec ~debug b indent4 ifminus; () | MatchList (arg, _loc, head_name, tail_name, ifcons, ifnil) -> let indent2 = indent ^ " " in let indent4 = indent2 ^ " " in Printf.bprintf b "\n%smatch " indent; - bprint_code ~debug b indent2 arg; + bprint_code_rec ~debug b indent2 arg; Printf.bprintf b " with\n"; Printf.bprintf b "\n%s| [] ->\n" indent2; - bprint_code ~debug b indent4 ifnil; + bprint_code_rec ~debug b indent4 ifnil; Printf.bprintf b "\n%s| %s :: %s ->\n" indent2 head_name tail_name; - bprint_code ~debug b indent4 ifcons; + bprint_code_rec ~debug b indent4 ifcons; () | Loop (name, _loc, body, arg) -> let indent2 = indent ^ " " in let indent4 = indent2 ^ " " in Printf.bprintf b "\n%sLoop.loop (fun %s -> " indent name; - bprint_code ~debug b indent4 body; + bprint_code_rec ~debug b indent4 body; Printf.bprintf b ")\n%s" indent2; - bprint_code ~debug b indent2 arg; + bprint_code_rec ~debug b indent2 arg; () | Closure (arg_name, arg_type, _loc, _, body, res_type) (* FIXME change this *) @@ -587,7 +755,7 @@ module Liquid = struct Printf.bprintf b "\n%s(fun ( %s : " indent arg_name; bprint_type b indent2 arg_type; Printf.bprintf b ") ->\n%s" indent2; - bprint_code ~debug b indent4 body; + bprint_code_rec ~debug b indent4 body; Printf.bprintf b ")" | Record (_loc, lab_x_exp_list) -> let indent2 = indent ^ " " in @@ -595,23 +763,23 @@ module Liquid = struct Printf.bprintf b "\n%s{" indent; List.iter (fun (label, exp) -> Printf.bprintf b "\n%s%s = " indent2 label; - bprint_code ~debug b indent4 exp; + bprint_code_rec ~debug b indent4 exp; Printf.bprintf b ";"; ) lab_x_exp_list; Printf.bprintf b "}" | Constructor (_loc, Constr constr, arg) -> Printf.bprintf b "\n%s%s (" indent constr; - bprint_code ~debug b (indent ^ " ") arg; + bprint_code_rec ~debug b (indent ^ " ") arg; Printf.bprintf b ")" | Constructor (_loc, Left right_ty, arg) -> Printf.bprintf b "\n%s(Left " indent; - bprint_code ~debug b (indent ^ " ") arg; + bprint_code_rec ~debug b (indent ^ " ") arg; Printf.bprintf b " : (_, "; bprint_type b (indent ^ " ") right_ty; Printf.bprintf b ") variant)" | Constructor (_loc, Right right_ty, arg) -> Printf.bprintf b "\n%s(Right " indent; - bprint_code ~debug b (indent ^ " ") arg; + bprint_code_rec ~debug b (indent ^ " ") arg; Printf.bprintf b " : ( "; bprint_type b (indent ^ " ") right_ty; Printf.bprintf b ", _) variant)" @@ -626,42 +794,116 @@ module Liquid = struct let indent2 = indent ^ " " in let indent4 = indent2 ^ " " in Printf.bprintf b "\n%smatch " indent; - bprint_code ~debug b indent2 arg; + bprint_code_rec ~debug b indent2 arg; Printf.bprintf b " with\n"; 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; + bprint_code_rec ~debug b indent4 e; | CAny, e -> Printf.bprintf b "\n%s| _ ->\n" indent2; - bprint_code ~debug b indent4 e; + bprint_code_rec ~debug b indent4 e; ) cases; () + | And (_loc, e1, e2) + | Or (_loc, e1, e2) + | Implies (_loc, e1, e2) + | Equiv (_loc, e1, e2) -> + let op = match code.desc with + | And _ -> "/\\" + | Or _ -> "\\/" + | Implies _ -> "=>" + | Equiv _ -> "<=>" + | _ -> assert false + in + Printf.bprintf b "\n%s(" indent; + let indent2 = indent ^ " " in + bprint_code_rec ~debug b indent2 e1; + Printf.bprintf b " %s " op; + bprint_code_rec ~debug b indent2 e2; + Printf.bprintf b ")" + | Forall (_loc, vars, e) + | Exists (_loc, vars, e) -> + let q = match code.desc with + | Forall _ -> "forall" + | Exists _ -> "exists" + | _ -> assert false + in + Printf.bprintf b "\n%s(%s" indent q; + List.iter (fun (v, ty) -> + Printf.bprintf b " (%s: " v; + bprint_type b indent ty; + Printf.bprintf b ")"; + ) vars; + Printf.bprintf b ". "; + let indent2 = indent ^ " " in + bprint_code_rec ~debug b indent2 e; + Printf.bprintf b ")" + + + let rec bprint_code_types ~debug b indent code = + bprint_code_base + (fun ~debug b indent code -> + bprint_code_types ~debug b indent code; + Printf.bprintf b "\n%s(* : " indent; + bprint_type b (indent^" ") code.ty; + Printf.bprintf b " *)"; + ) + ~debug b indent code + let rec bprint_code ~debug b indent code = + bprint_code_base bprint_code ~debug b indent code - let bprint_contract ~debug b indent contract = + let bprint_spec bprint_code ~debug b indent = + let indent2 = indent ^ " " in + function + | Requires e -> + Printf.bprintf b "\n%s[%%requires" indent; + bprint_code ~debug b indent2 e; + Printf.bprintf b "]"; + | Ensures e -> + Printf.bprintf b "\n%s[%%ensures" indent; + bprint_code ~debug b indent2 e; + Printf.bprintf b "]"; + | Fails e -> + Printf.bprintf b "\n%s[%%fails" indent; + bprint_code ~debug b indent2 e; + Printf.bprintf b "]" + + let bprint_specs bprint_code ~debug b indent l = + List.iter (bprint_spec bprint_code ~debug b indent) l + + let bprint_contract bprint_code bprint_specs ~debug b indent contract = let indent2 = indent ^ " " in - Printf.bprintf b "let contract\n"; - Printf.bprintf b " (amount: tez)\n"; - Printf.bprintf b " (parameter: "; + Printf.bprintf b "let%%entry main\n"; + (* Printf.bprintf b " (amount: tez)\n"; *) + Printf.bprintf b " (parameter/2: "; bprint_type b indent2 contract.parameter; Printf.bprintf b ")\n"; - Printf.bprintf b " (storage: "; + Printf.bprintf b " (storage/1: "; bprint_type b indent2 contract.storage; Printf.bprintf b ")\n"; - Printf.bprintf b " (return: "; - bprint_type b indent2 contract.return; - Printf.bprintf b ") = \n"; + Printf.bprintf b " : "; + bprint_type b indent2 (Ttuple [contract.return; contract.storage]); + bprint_specs bprint_code ~debug b indent2 contract.spec; + Printf.bprintf b "= \n"; bprint_code ~debug b indent contract.code let string_of_type = to_string bprint_type + let string_of_type_expl = to_string (fun b -> bprint_type ~definition:true b) let string_of_const = to_string bprint_const let string_of_code ?(debug=false) code = to_string (bprint_code ~debug) code + let string_of_code_types ?(debug=false) code = + to_string (bprint_code_types ~debug) code let string_of_contract ?(debug=false) cmd = - to_string (bprint_contract ~debug) cmd + to_string (bprint_contract bprint_code (fun _ ~debug _ _ _ -> ()) ~debug) cmd + let string_of_encoded_contract ?(debug=false) cmd = + to_string (bprint_contract bprint_code bprint_specs ~debug) cmd + let string_of_contract_types ?(debug=false) cmd = + to_string (bprint_contract bprint_code_types bprint_specs ~debug) cmd end @@ -681,6 +923,8 @@ let string_of_node node = | N_IF_CONS _ -> "N_IF_CONS" | N_IF_LEFT _ -> "N_IF_LEFT" | N_IF_RIGHT _ -> "N_IF_RIGHT" + | N_IF_PLUS _ -> "N_IF_PLUS" + | N_IF_MINUS _ -> "N_IF_MINUS" | N_TRANSFER _ -> "N_TRANSFER" | N_TRANSFER_RESULT int -> Printf.sprintf "N_TRANSFER_RESULT %d" int | N_CONST (ty, cst) -> "N_CONST " ^ Michelson.string_of_const cst @@ -700,3 +944,4 @@ let string_of_node node = | N_SOURCE _ -> "N_SOURCE" | N_LEFT _ -> "N_LEFT" | N_RIGHT _ -> "N_RIGHT" + | N_ABS -> "N_ABS" diff --git a/tools/liquidity/liquidPrinter.mli b/tools/liquidity/liquidPrinter.mli index 4250d620..c4967642 100644 --- a/tools/liquidity/liquidPrinter.mli +++ b/tools/liquidity/liquidPrinter.mli @@ -25,24 +25,25 @@ val int_of_integer : integer -> int val integer_of_int : int -> integer - module Liquid : sig - val string_of_type : LiquidTypes.datatype -> string - val string_of_const : LiquidTypes.const -> string - val string_of_contract : ?debug:bool -> - 'a LiquidTypes.exp LiquidTypes.contract -> string - val string_of_code : ?debug:bool -> 'a LiquidTypes.exp -> string + val string_of_type : datatype -> string + val string_of_type_expl : datatype -> string + val string_of_const : const -> string + val string_of_contract : ?debug:bool -> (('a, 'b) exp, 'c) contract -> string + val string_of_contract_types : ?debug:bool -> typed_contract -> string + val string_of_encoded_contract : ?debug:bool -> encoded_contract -> string + val string_of_code : ?debug:bool -> ('a, 'b) exp -> string + val string_of_code_types : ?debug:bool -> typed_exp -> string end module Michelson : sig - val string_of_type : LiquidTypes.datatype -> string - val string_of_const : LiquidTypes.const -> string - val line_of_const : LiquidTypes.const -> string - val string_of_contract : - LiquidTypes.michelson_exp LiquidTypes.contract -> string - val string_of_code : LiquidTypes.michelson_exp -> string - val string_of_noloc_michelson : LiquidTypes.noloc_michelson -> string - val string_of_loc_michelson : LiquidTypes.loc_michelson -> string + val string_of_type : datatype -> string + val string_of_const : const -> string + val line_of_const : const -> string + val string_of_contract : michelson_contract -> string + val string_of_code : michelson_exp -> string + val string_of_noloc_michelson : noloc_michelson -> string + val string_of_loc_michelson : loc_michelson -> string end -val string_of_node : LiquidTypes.node -> string +val string_of_node : node -> string diff --git a/tools/liquidity/liquidSimplify.ml b/tools/liquidity/liquidSimplify.ml index b4576a07..634bb4e9 100644 --- a/tools/liquidity/liquidSimplify.ml +++ b/tools/liquidity/liquidSimplify.ml @@ -50,6 +50,12 @@ let compute code to_inline = let ifsome = iter ifsome in { exp with desc = MatchOption(arg,loc,ifnone,name,ifsome) } + | MatchNat(arg, loc, p, ifplus, m, ifminus) -> + let arg = iter arg in + let ifplus = iter ifplus in + let ifminus = iter ifminus in + { exp with desc = MatchNat(arg, loc, p, ifplus, m, ifminus) } + | MatchList(arg, loc, head_name, tail_name, ifcons, ifnil) -> let arg = iter arg in let ifcons = iter ifcons in @@ -113,10 +119,36 @@ let compute code to_inline = lab_x_exp_list in { exp with desc = Record(loc, lab_x_exp_list) } - | Constructor _ -> assert false (* never found in typed_exp *) + | And (loc, e1, e2) | Or (loc, e1, e2) + | Implies (loc, e1, e2) | Equiv (loc, e1, e2) -> + let e1 = iter e1 in + let e2 = iter e2 in + { exp with desc = match exp.desc with + | And _ -> And (loc, e1, e2) + | Or _ -> Or (loc, e1, e2) + | Implies _ -> Implies (loc, e1, e2) + | Equiv _ -> Equiv (loc, e1, e2) + | _ -> assert false } + + | Forall (loc, vars, body) -> + { exp with desc = Forall (loc, vars, iter body) } + | Exists (loc, vars, body) -> + { exp with desc = Exists (loc, vars, iter body) } + + | Constructor _ -> assert false (* never found in encoded_exp *) in iter code +let simplify_specs l to_inline = + List.map (function + | Requires f -> Requires (compute f to_inline) + | Ensures f -> Ensures (compute f to_inline) + | Fails f -> Fails (compute f to_inline) + ) l + let simplify_contract contract to_inline = - { contract with code = compute contract.code to_inline } + { contract with + code = compute contract.code to_inline; + spec = simplify_specs contract.spec to_inline; + } diff --git a/tools/liquidity/liquidSimplify.mli b/tools/liquidity/liquidSimplify.mli index 999ba191..d0dc9b77 100644 --- a/tools/liquidity/liquidSimplify.mli +++ b/tools/liquidity/liquidSimplify.mli @@ -10,4 +10,4 @@ open LiquidTypes val simplify_contract : - typed_exp contract -> typed_exp StringMap.t -> typed_exp contract + encoded_contract -> encoded_exp StringMap.t -> encoded_contract diff --git a/tools/liquidity/liquidToOCaml.ml b/tools/liquidity/liquidToOCaml.ml index 249463b9..8e2dd0ee 100644 --- a/tools/liquidity/liquidToOCaml.ml +++ b/tools/liquidity/liquidToOCaml.ml @@ -8,7 +8,7 @@ (**************************************************************************) (* The version that will be required to compile the generated files. *) -let output_version = "0.11" +let output_version = "0.13" (* type storage = ... @@ -46,15 +46,14 @@ let rec convert_type ty = | Ttuple args -> Typ.tuple (List.map convert_type args) | Tor (x,y) -> typ_constr "variant" [convert_type x; convert_type y] | Tcontract (x,y) -> typ_constr "contract" [convert_type x;convert_type y] - | Tlambda (x,y) -> typ_constr "lambda" [convert_type x; convert_type y] - | Tclosure ((x,e),r) -> - typ_constr "closure" [convert_type x; convert_type e; convert_type r] + | Tlambda (x,y) -> Typ.arrow Nolabel (convert_type x) (convert_type y) + | Tclosure ((x,e),r) -> Typ.arrow Nolabel (convert_type x) (convert_type r) | Tmap (x,y) -> typ_constr "map" [convert_type x;convert_type y] | Tset x -> typ_constr "set" [convert_type x] | Tlist x -> typ_constr "list" [convert_type x] | Toption x -> typ_constr "option" [convert_type x] - | Tfail -> assert false | Ttype (_, ty) -> convert_type ty + | Tfail | Trecord _ | Tsum _ -> assert false let rec convert_const expr = match expr with @@ -72,20 +71,15 @@ let rec convert_const expr = (Some (convert_const x)) | CRight x -> Exp.construct (lid "Right") (Some (convert_const x)) + | CConstr (c, x) -> Exp.construct (lid c) + (Some (convert_const x)) | CTuple args -> Exp.tuple (List.map convert_const args) - | CTez n -> Exp.constraint_ ( - Exp.constant (Const.float ~suffix:'\231' - (LiquidPrinter.liq_of_tez n))) - (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) - - | CTimestamp s -> Exp.constraint_ (convert_const (CString s)) - (convert_type Ttimestamp) + | CTez n -> Exp.constant (Const.float ~suffix:'\231' + (LiquidPrinter.liq_of_tez n)) + | CTimestamp s -> Exp.constant (Pconst_integer (s, Some '\232')) + | CKey_hash n -> Exp.constant (Pconst_integer (n, Some '\233')) + | CKey n -> Exp.constant (Pconst_integer (n, Some '\234')) + | CSignature n -> Exp.constant (Pconst_integer (n, Some '\235')) | CList [] -> Exp.construct (lid "[]") None | CList (head :: tail) -> @@ -115,6 +109,10 @@ let rec convert_const expr = ) (Exp.construct (lid "[]") None) list in Exp.construct (lid "Map") (Some args) + | CRecord labels -> + Exp.record + (List.map (fun (f, x) -> lid f, convert_const x) labels) + None let rec convert_code expr = match expr.desc with @@ -140,6 +138,8 @@ let rec convert_code expr = | Tnat | Tstring | Tunit + | Ttimestamp + | Ttez | Tbool -> convert_const cst | _ -> Exp.constraint_ (convert_const cst) (convert_type ty) @@ -203,6 +203,20 @@ let rec convert_code expr = (convert_code ifsome); ] + | MatchNat (exp, _loc, p, ifplus, m, ifminus) -> + Exp.extension (loc "nat", PStr [ + Str.eval ( + Exp.match_ (convert_code exp) + [ + Exp.case (Pat.construct (lid "Plus") + (Some (Pat.var (loc p)))) + (convert_code ifplus); + Exp.case (Pat.construct (lid "Minus") + (Some (Pat.var (loc m)))) + (convert_code ifminus); + ]) + ]) + | MatchList (exp, _loc, head_pat, tail_pat, ifcons, ifnil) -> Exp.match_ (convert_code exp) [ @@ -300,6 +314,10 @@ let rec convert_code expr = [convert_type from_ty; convert_type to_ty]) + | And _ | Or _ | Implies _ | Equiv _ | Forall _ | Exists _ -> + assert false + + let structure_of_contract contract = let code = convert_code contract.code in [ diff --git a/tools/liquidity/liquidToOCaml.mli b/tools/liquidity/liquidToOCaml.mli index 341460bc..70807674 100644 --- a/tools/liquidity/liquidToOCaml.mli +++ b/tools/liquidity/liquidToOCaml.mli @@ -11,8 +11,8 @@ open LiquidTypes val output_version : string -val structure_of_contract : syntax_exp contract -> Parsetree.structure +val structure_of_contract : (syntax_exp, 'a) contract -> Parsetree.structure val string_of_structure : Parsetree.structure -> string -val translate_expression : unit LiquidTypes.exp -> Parsetree.expression +val translate_expression : syntax_exp -> Parsetree.expression val string_of_expression : Parsetree.expression -> string diff --git a/tools/liquidity/liquidTypes.ml b/tools/liquidity/liquidTypes.ml index e49efef5..2190e8d5 100644 --- a/tools/liquidity/liquidTypes.ml +++ b/tools/liquidity/liquidTypes.ml @@ -39,8 +39,11 @@ type const = | CKey_hash of string - and datatype = - (* michelson *) + | CRecord of (string * const) list + | CConstr of string * const + +type datatype = + (* michelson *) | Tunit | Tbool | Tint @@ -54,6 +57,9 @@ type const = | Ttuple of datatype list + | Trecord of (string * datatype) list + | Tsum of (string * datatype) list + | Toption of datatype | Tlist of datatype | Tset of datatype @@ -68,13 +74,63 @@ type const = | Tfail | Ttype of string * datatype +let rec get_type ty = match ty with + | Ttez | Tunit | Ttimestamp | Tint | Tnat | Tbool | Tkey | Tkey_hash + | Tsignature | Tstring | Tfail -> ty + | Ttuple tys -> + let tys' = List.map get_type tys in + if List.for_all2 (==) tys tys' then ty + else Ttuple tys' + | Tset t | Tlist t | Toption t -> + let t' = get_type t in + if t' == t then ty + else begin match ty with + | Tset t -> Tset t' + | Tlist t -> Tlist t' + | Toption t -> Toption t' + | _ -> assert false + end + | Tor (t1, t2) | Tcontract (t1, t2) | Tlambda (t1, t2) | Tmap (t1, t2) -> + let t1', t2' = get_type t1, get_type t2 in + if t1 == t1' && t2 == t2' then ty + else begin match ty with + | Tor (t1, t2) -> Tor (t1', t2') + | Tcontract (t1, t2) -> Tcontract (t1', t2') + | Tlambda (t1, t2) -> Tlambda (t1', t2') + | Tmap (t1, t2) -> Tmap (t1', t2') + | _ -> assert false + end + | Tclosure ((t1, t2), t3) -> + let t1', t2', t3' = get_type t1, get_type t2, get_type t3 in + if t1 == t1' && t2 == t2' && t3 == t3' then ty + else Tclosure ((t1', t2'), t3') + | Trecord ntys | Tsum ntys -> + let change = ref false in + let ntys' = List.map (fun (l, ty) -> + let ty' = get_type ty in + if ty' != ty then change := true; + (l, ty') + ) ntys in + if !change then match ty with + | Trecord _ -> Trecord ntys' + | Tsum _ -> Tsum ntys' + | _ -> assert false + else ty + + | Ttype (name, t) -> get_type t + +let first_alias ty = + let rec aux acc ty = match acc, ty with + | _, Ttype (name, ty) -> aux (Some name) ty + | Some name, ty -> Some (name, ty) + | None, _ -> None + in + aux None ty + +let eq_types t1 t2 = + get_type t1 = get_type t2 + -type 'exp contract = { - parameter : datatype; - storage : datatype; - return : datatype; - code : 'exp; - } type location = { loc_file : string; @@ -171,6 +227,8 @@ type primitive = | Prim_exec + (* Specs *) + | Prim_old let primitive_of_string = Hashtbl.create 101 let string_of_primitive = Hashtbl.create 101 @@ -272,6 +330,7 @@ let () = "", Prim_unknown; "", Prim_unused; + "old", Prim_old; ] let primitive_of_string s = @@ -304,67 +363,161 @@ type pattern = | CConstr of string * string list | CAny -type 'ty exp = { - desc : 'ty exp_desc; +type ('ty, 'a) exp = { + desc : ('ty, 'a) exp_desc; ty : 'ty; bv : StringSet.t; fail : bool; + transfer : bool; + isspec : bool; } - and 'ty exp_desc = - | Let of string * location * 'ty exp * 'ty exp +and ('ty, 'a) exp_desc = + | Let of string * location * ('ty, 'a) exp * ('ty, 'a) exp | Var of string * location * string list - | SetVar of string * location * string list * 'ty exp + | SetVar of string * location * string list * ('ty, 'a) exp | Const of datatype * const - | Apply of primitive * location * 'ty exp list - | If of 'ty exp * 'ty exp * 'ty exp - | Seq of 'ty exp * 'ty exp + | Apply of primitive * location * ('ty, 'a) exp list + | If of ('ty, 'a) exp * ('ty, 'a) exp * ('ty, 'a) exp + | Seq of ('ty, 'a) exp * ('ty, 'a) exp | LetTransfer of (* storage *) string * (* result *) string * location - * (* contract_ *) 'ty exp - * (* tez_ *) 'ty exp - * (* storage_ *) 'ty exp - * (* arg_ *) 'ty exp - * 'ty exp (* body *) - | MatchOption of 'ty exp (* argument *) + * (* contract_ *) ('ty, 'a) exp + * (* tez_ *) ('ty, 'a) exp + * (* storage_ *) ('ty, 'a) exp + * (* arg_ *) ('ty, 'a) exp + * ('ty, 'a) exp (* body *) + | MatchOption of ('ty, 'a) exp (* argument *) * location - * 'ty exp (* ifnone *) - * string * 'ty exp (* ifsome *) - | MatchList of 'ty exp (* argument *) + * ('ty, 'a) exp (* ifnone *) + * string * ('ty, 'a) exp (* ifsome *) + | MatchList of ('ty, 'a) exp (* argument *) * location - * string * string * 'ty exp * (* ifcons *) - 'ty exp (* ifnil *) + * string * string * ('ty, 'a) exp * (* ifcons *) + ('ty, 'a) exp (* ifnil *) | Loop of string * location - * 'ty exp (* body *) - * 'ty exp (* arg *) + * ('ty, 'a) exp (* body *) + * ('ty, 'a) exp (* arg *) | Lambda of string (* argument name *) * datatype (* argument type *) * location - * 'ty exp (* body *) + * ('ty, 'a) exp (* body *) * datatype (* final datatype, inferred during typechecking *) | Closure of string (* argument name *) * datatype (* argument type *) * location - * (string * 'ty exp) list (* call environment *) - * 'ty exp (* body *) + * (string * ('ty, 'a) exp) list (* call environment *) + * ('ty, 'a) exp (* body *) * datatype (* final datatype, inferred during typechecking *) - | Record of location * (string * 'ty exp) list - | Constructor of location * constructor * 'ty exp + | Record of location * (string * ('ty, 'a) exp) list + | Constructor of location * constructor * ('ty, 'a) exp - | MatchVariant of 'ty exp + | MatchVariant of ('ty, 'a) exp * location - * (pattern * 'ty exp) list - -type syntax_exp = unit exp -type typed_exp = datatype exp -type live_exp = (datatype * datatype StringMap.t) exp - + * (pattern * ('ty, 'a) exp) list + + | MatchNat of ('ty, 'a) exp (* argument *) + * location + * string * ('ty, 'a) exp (* ifplus *) + * string * ('ty, 'a) exp (* ifminus *) + + (* Specs *) + | And of location * ('ty, 'a) exp * ('ty, 'a) exp + | Or of location * ('ty, 'a) exp * ('ty, 'a) exp + | Implies of location * ('ty, 'a) exp * ('ty, 'a) exp + | Equiv of location * ('ty, 'a) exp * ('ty, 'a) exp + | Forall of location * (string * datatype) list * ('ty, 'a) exp + | Exists of location * (string * datatype) list * ('ty, 'a) exp + +type typed +type encoded +type syntax_exp = (unit, unit) exp +type typed_exp = (datatype, typed) exp +type encoded_exp = (datatype, encoded) exp +type live_exp = (datatype * datatype StringMap.t, encoded) exp + + +type 'a spec = + | Requires of 'a + | Ensures of 'a + | Fails of 'a + +type 'a specs = 'a spec list +type syntax_specs = syntax_exp specs +type typed_specs = typed_exp specs +type encoded_specs = encoded_exp specs + +type ('exp, 'spec) contract = { + parameter : datatype; + storage : datatype; + return : datatype; + spec : 'spec; + code : 'exp; +} +let mk = + let bv = StringSet.empty in + fun desc ty -> + let fail, transfer, isspec = match desc with + | Const (_, _) + | Var (_, _, _) -> false, false, false + + | LetTransfer _ -> true, true, false + + | SetVar (_, _, _, e) + | Constructor (_, _, e) + | Lambda (_, _, _, e, _) + -> e.fail, e.transfer, e.isspec + + | Forall (_, _, e) + | Exists (_, _, e) + -> e.fail, e.transfer, true + + | Seq (e1, e2) + | Let (_, _, e1, e2) + | Loop (_, _, e1, e2) -> + e1.fail || e2.fail, e1.transfer || e2.transfer, e1.isspec || e2.isspec + + | And (_, e1, e2) + | Or (_, e1, e2) + | Implies (_, e1, e2) + | Equiv (_, e1, e2) + -> e1.fail || e2.fail, e1.transfer || e2.transfer, true + + | If (e1, e2, e3) + | MatchOption (e1, _, e2, _, e3) + | MatchNat (e1, _, _, e2, _, e3) + | MatchList (e1, _, _, _, e2, e3) -> + e1.fail || e2.fail || e3.fail, + e1.transfer || e2.transfer || e3.transfer, + e1.isspec || e2.isspec || e3.isspec + + | Apply (prim, _, l) -> + prim = Prim_fail || List.exists (fun e -> e.fail) l, + List.exists (fun e -> e.transfer) l, + List.exists (fun e -> e.isspec) l + + | Closure (_, _, _, env, e, _) -> + e.fail || List.exists (fun (_, e) -> e.fail) env, + e.transfer || List.exists (fun (_, e) -> e.transfer) env, + e.isspec || List.exists (fun (_, e) -> e.isspec) env + + | Record (_, labels) -> + List.exists (fun (_, e) -> e.fail) labels, + List.exists (fun (_, e) -> e.transfer) labels, + List.exists (fun (_, e) -> e.isspec) labels + + | MatchVariant (e, _, cases) -> + e.fail || List.exists (fun (_, e) -> e.fail) cases, + e.transfer || List.exists (fun (_, e) -> e.transfer) cases, + e.isspec || List.exists (fun (_, e) -> e.isspec) cases + in + { desc; ty; bv; fail; transfer; isspec } type michelson_exp = @@ -457,16 +610,6 @@ type loc_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 - * datatype (* final type *) - * datatype (* left type *) - * datatype (* right type *) - ) list - type closure_env = { env_vars : (string (* name outside closure *) * datatype @@ -474,11 +617,11 @@ type closure_env = { * (int ref * (* usage counter inside closure *) int ref (* usage counter outside closure *) )) StringMap.t; - env_bindings : (typed_exp (* expression to access variable inside closure *) + env_bindings : (encoded_exp (* expression to access variable inside closure *) * (int ref * (* usage counter inside closure *) int ref (* usage counter outside closure *) )) StringMap.t; - call_bindings : (string * typed_exp) list; + call_bindings : (string * encoded_exp) list; } type env = { @@ -487,7 +630,7 @@ type env = { (* fields modified in LiquidFromOCaml *) (* type definitions *) - mutable types : (datatype * type_kind) StringMap.t; + mutable types : datatype StringMap.t; (* labels of records in type definitions *) mutable labels : (string * int * datatype) StringMap.t; (* constructors of sum-types in type definitions *) @@ -495,13 +638,15 @@ type env = { } (* fields updated in LiquidCheck *) -type 'a typecheck_env = { +type ('a, 'b) typecheck_env = { warnings : bool; + allow_spec : bool; + in_post : bool; counter : int ref; vars : (string * datatype * int ref) StringMap.t; env : env; - to_inline : datatype exp StringMap.t ref; - contract : 'a contract; + to_inline : encoded_exp StringMap.t ref; + contract : ('a, 'b) contract; clos_env : closure_env option; } @@ -517,7 +662,7 @@ type node = { mutable prevs : node list; } - and node_kind = +and node_kind = | N_UNKNOWN of string | N_VAR of string | N_START @@ -533,6 +678,8 @@ type node = { | N_IF_CONS of node * node * node | N_IF_LEFT of node * node | N_IF_RIGHT of node * node + | N_IF_PLUS of node * node + | N_IF_MINUS of node * node | N_TRANSFER of node * node | N_TRANSFER_RESULT of int | N_CONST of datatype * const @@ -553,9 +700,18 @@ type node = { | N_LEFT of datatype | N_RIGHT of datatype | N_SOURCE of datatype * datatype + | N_ABS type node_exp = node * node +type syntax_contract = (syntax_exp, syntax_specs) contract +type typed_contract = (typed_exp, typed_specs) contract +type encoded_contract = (encoded_exp, encoded_specs) contract +type michelson_contract = (michelson_exp, unit) contract +type node_contract = (node_exp, unit) contract +type noloc_michelson_contract = (noloc_michelson, unit) contract +type loc_michelson_contract = (loc_michelson, unit) contract + type warning = | Unused of string | UnusedMatched of string diff --git a/tools/liquidity/liquidUntype.ml b/tools/liquidity/liquidUntype.ml index b3f93dd8..3e584a14 100644 --- a/tools/liquidity/liquidUntype.ml +++ b/tools/liquidity/liquidUntype.ml @@ -13,7 +13,7 @@ open LiquidTypes -let mk desc = { desc; ty = (); bv = StringSet.empty; fail = false } +let mk desc = mk desc () type env = { env_map : string StringMap.t; @@ -75,7 +75,7 @@ let find_free env var_arg bv = scopes. Unfortunately, without hash-consing, this can be quite expensive. *) -let rec untype (env : env) (code : typed_exp) = +let rec untype (env : env) (code : encoded_exp) : syntax_exp = let desc = match code.desc with | If (cond, ifthen, ifelse) -> @@ -135,6 +135,13 @@ let rec untype (env : env) (code : typed_exp) = untype env ifnone, some_pat', untype env' ifsome) + | MatchNat (exp, loc, p, ifplus, m, ifminus) -> + let (p, env') = find_free env p ifplus.bv in + let (m, env'') = find_free env m ifminus.bv in + MatchNat (untype env exp, loc, + p, untype env' ifplus, + m, untype env'' ifminus) + | MatchList (exp, loc, head_pat, tail_pat, ifcons, ifnil) -> let bv = ifcons.bv in let (head_pat, env') = find_free env head_pat bv in @@ -177,8 +184,9 @@ let rec untype (env : env) (code : typed_exp) = ]) | Record (_, _) - | Constructor (_, _, _) - | MatchVariant (_, _, _) -> + | And _ | Or _ | Implies _ | Equiv _ | Forall _ | Exists _ + | Constructor (_, _, _) + | MatchVariant (_, _, _) -> LiquidLoc.raise_error "untype: unimplemented code:\n%s%!" @@ -198,4 +206,4 @@ let untype_contract contract = let env = empty_env () in let env = new_binding "storage/1" "storage" env in let env = new_binding "parameter/2" "parameter" env in - { contract with code = untype env contract.code } + { contract with code = untype env contract.code; spec = () } diff --git a/tools/liquidity/liquidUntype.mli b/tools/liquidity/liquidUntype.mli index 56a5a303..13adf53d 100644 --- a/tools/liquidity/liquidUntype.mli +++ b/tools/liquidity/liquidUntype.mli @@ -9,4 +9,4 @@ open LiquidTypes -val untype_contract : typed_exp contract -> syntax_exp contract +val untype_contract : encoded_contract -> (syntax_exp, unit) contract diff --git a/tools/liquidity/ocaml/liquidOCamlLexer.mll b/tools/liquidity/ocaml/liquidOCamlLexer.mll index 700fefda..77c32bd6 100644 --- a/tools/liquidity/ocaml/liquidOCamlLexer.mll +++ b/tools/liquidity/ocaml/liquidOCamlLexer.mll @@ -19,6 +19,12 @@ { +let tez_char = '\231' +let timestamp_char = '\232' +let keyhash_char = '\233' +let key_char = '\234' +let signature_char = '\235' + open Lexing open Misc open LiquidOCamlParser @@ -52,9 +58,11 @@ let default_keywords = "else", ELSE; "end", END; "exception", EXCEPTION; + "exists", EXISTS; "external", EXTERNAL; "false", FALSE; "for", FOR; + "forall", FORALL; "fun", FUN; "function", FUNCTION; "functor", FUNCTOR; @@ -326,6 +334,23 @@ let bin_literal = '0' ['b' 'B'] ['0'-'1'] ['0'-'1' '_']* let int_literal = decimal_literal | hex_literal | oct_literal | bin_literal +let base58_char = + ['1'-'9' 'A'-'H' 'J'-'N' 'P'-'Z' 'a'-'k' 'm'-'z' ] +let keyhash_literal = + ['t' 'T'] "z1" base58_char* (* 36 *) +let key_literal = + "edpk" base58_char* (* 54 *) +let signature_literal = + "edsig" base58_char* (* 99 *) +let digit = [ '0'-'9'] +let day_literal = + digit digit digit digit '-' digit digit '-' digit digit +let hour_literal = + digit digit ':' digit digit ( ':' digit digit )? +let timezone_literal = + digit digit ':' digit digit +let date_literal = + day_literal ('T' hour_literal ('+' timezone_literal )?)? (* remove hex_float_literal and remove exponential from float. *) @@ -360,10 +385,45 @@ rule token = parse { OPTLABEL (get_label_name lexbuf) } | "?" lowercase_latin1 identchar_latin1 * ':' { warn_latin1 lexbuf; OPTLABEL (get_label_name lexbuf) } + | keyhash_literal + { + let s = Lexing.lexeme lexbuf in + if String.length s = 36 then + INT (s, Some keyhash_char) + else begin + (* TODO warning *) + if s.[0] = 'T' then UIDENT s else LIDENT s + end + } + | key_literal + { + let s = Lexing.lexeme lexbuf in + if String.length s = 54 then + INT (s, Some key_char) + else begin + (* TODO warning *) + LIDENT s + end + } + | signature_literal + { + let s = Lexing.lexeme lexbuf in + if String.length s = 99 then + INT (s, Some signature_char) + else begin + (* TODO warning *) + LIDENT s + end + } + | date_literal + { let date = Lexing.lexeme lexbuf in + INT(date, Some timestamp_char) } | lowercase identchar * { let s = Lexing.lexeme lexbuf in try token_of_keyword s with Not_found -> LIDENT s } + | '@' lowercase identchar * + { LIDENT (Lexing.lexeme lexbuf) } | lowercase_latin1 identchar_latin1 * { warn_latin1 lexbuf; LIDENT (Lexing.lexeme lexbuf) } | uppercase identchar * @@ -372,13 +432,13 @@ rule token = parse { warn_latin1 lexbuf; UIDENT(Lexing.lexeme lexbuf) } | int_literal { INT (Lexing.lexeme lexbuf, None) } | (int_literal as lit) "tz" - { INT (lit, Some '\231') } + { INT (lit, Some tez_char) } | (int_literal as lit) (literal_modifier as modif) { INT (lit, Some modif) } | float_literal { FLOAT (Lexing.lexeme lexbuf, None) } | ((float_literal) as lit) "tz" - { FLOAT (lit, Some '\231') } + { FLOAT (lit, Some tez_char) } | ((float_literal) as lit) (literal_modifier as modif) { FLOAT (lit, Some modif) } | (float_literal | int_literal) identchar+ @@ -496,6 +556,10 @@ rule token = parse | ":>" { COLONGREATER } | ";" { SEMI } | ";;" { SEMISEMI } + | "/\\" { LOGICAND } + | "\\/" { LOGICOR } + | "=>" { LOGICIMPL } + | "<=>" { LOGICEQUIV } | "<" { LESS } | "<-" { LESSMINUS } | "=" { EQUAL } diff --git a/tools/liquidity/ocaml/liquidOCamlParser.mly b/tools/liquidity/ocaml/liquidOCamlParser.mly index f444810e..12ebcd45 100644 --- a/tools/liquidity/ocaml/liquidOCamlParser.mly +++ b/tools/liquidity/ocaml/liquidOCamlParser.mly @@ -445,10 +445,12 @@ let package_type_of_module_type pmty = %token EOF %token EQUAL %token EXCEPTION +%token EXISTS %token EXTERNAL %token FALSE %token FLOAT %token FOR +%token FORALL %token FUN %token FUNCTION %token FUNCTOR @@ -480,6 +482,10 @@ let package_type_of_module_type pmty = %token LESSMINUS %token LET %token LIDENT +%token LOGICAND +%token LOGICEQUIV +%token LOGICIMPL +%token LOGICOR %token LPAREN %token LBRACKETAT %token LBRACKETATAT @@ -563,6 +569,10 @@ The precedences must be listed from low to high. %nonassoc IN %nonassoc below_SEMI %nonassoc SEMI /* below EQUAL ({lbl=...; lbl=...}) */ +%nonassoc prec_forall prec_exists +%right LOGICIMPL LOGICEQUIV +%right LOGICOR /* expr (e \/ e \/ e) */ +%right LOGICAND /* expr (e /\ e /\ e) */ %nonassoc LET /* above SEMI ( ...; let ... in ...) */ %nonassoc below_WITH %nonassoc FUNCTION WITH /* below BAR (match ... with ...) */ @@ -1391,6 +1401,14 @@ expr: { mkinfix $1 "&" $3 } | expr AMPERAMPER expr { mkinfix $1 "&&" $3 } + | expr LOGICAND expr + { mkinfix $1 "/\\" $3 } + | expr LOGICOR expr + { mkinfix $1 "\\/" $3 } + | expr LOGICIMPL expr + { mkinfix $1 "=>" $3 } + | expr LOGICEQUIV expr + { mkinfix $1 "<=>" $3 } | expr COLONEQUAL expr { mkinfix $1 ":=" $3 } | subtractive expr %prec prec_unary_minus @@ -1419,6 +1437,12 @@ expr: { unclosed "object" 1 "end" 4 } | expr attribute { Exp.attr $1 $2 } + | FORALL quantified_val_idents DOT expr %prec prec_forall + { let qfv = mkpat (Ppat_tuple $2) in + mkexp (Pexp_extension (mkrhs "forall" 1, PPat (qfv, Some $4))) } + | EXISTS quantified_val_idents DOT expr %prec prec_exists + { let qfv = mkpat (Ppat_tuple $2) in + mkexp (Pexp_extension (mkrhs "exists" 1, PPat (qfv, Some $4))) } | UNDERSCORE { not_expecting 1 "wildcard \"_\"" } ; @@ -1683,6 +1707,14 @@ opt_type_constraint: type_constraint { Some $1 } | /* empty */ { None } ; +quantified_val_ident: + | LPAREN val_ident COLON core_type RPAREN + { mkpat(Ppat_constraint(mkpatvar $2 1, $4)) } +; +quantified_val_idents: + quantified_val_ident { [$1] } + | quantified_val_ident quantified_val_idents { $1 :: $2 } +; /* Patterns */ diff --git a/tools/liquidity/ocaml/liquidOCamlPrinter.ml b/tools/liquidity/ocaml/liquidOCamlPrinter.ml index 994d8b60..1121048e 100644 --- a/tools/liquidity/ocaml/liquidOCamlPrinter.ml +++ b/tools/liquidity/ocaml/liquidOCamlPrinter.ml @@ -211,6 +211,10 @@ let constant f = function | Pconst_string (i, None) -> pp f "%S" i | Pconst_string (i, Some delim) -> pp f "{%s|%s|%s}" delim i delim | Pconst_integer (i, None) -> paren (i.[0]='-') (fun f -> pp f "%s") f i + | Pconst_integer (s, Some '\232') -> pp f "%s" s + | Pconst_integer (s, Some '\233') -> pp f "%s" s + | Pconst_integer (s, Some '\234') -> pp f "%s" s + | Pconst_integer (s, Some '\235') -> pp f "%s" s | Pconst_integer (i, Some m) -> paren (i.[0]='-') (fun f (i, m) -> if m = '\231' then diff --git a/tools/liquidity/ocaml/liquidOCamlTranslate.ml b/tools/liquidity/ocaml/liquidOCamlTranslate.ml index c276ead3..031847b6 100644 --- a/tools/liquidity/ocaml/liquidOCamlTranslate.ml +++ b/tools/liquidity/ocaml/liquidOCamlTranslate.ml @@ -27,13 +27,15 @@ let clean_ast = (({ Asttypes.txt = "version" }, PStr [{ pstr_desc = Pstr_eval (exp,[])}]),[]) } -> - Str.eval (Exp.constant (Const.int 0)) + 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 ); @@ -53,6 +55,26 @@ let clean_ast = Exp.apply ~loc (exp_ident ~loc "Tez.of_string") [Nolabel, exp_string ~loc s] + | Pexp_constant (Pconst_integer (s, Some '\232')) + -> + Exp.apply ~loc (exp_ident ~loc "Timestamp.of_string") + [Nolabel, exp_string ~loc s] + + | Pexp_constant (Pconst_integer (s, Some '\233')) + -> + Exp.apply ~loc (exp_ident ~loc "Key_hash.of_string") + [Nolabel, exp_string ~loc s] + + | Pexp_constant (Pconst_integer (s, Some '\234')) + -> + Exp.apply ~loc (exp_ident ~loc "Key.of_string") + [Nolabel, exp_string ~loc s] + + | Pexp_constant (Pconst_integer (s, Some '\235')) + -> + Exp.apply ~loc (exp_ident ~loc "Signature.of_string") + [Nolabel, exp_string ~loc s] + | Pexp_constant ( Pconst_float (s, Some '\231') ) @@ -121,6 +143,52 @@ let clean_ast = Exp.record ~loc [label1, value] (Some record) end + | Pexp_extension ( + { txt = "nat" }, + PStr [{ pstr_desc = Pstr_eval ( + { pexp_desc = Pexp_match (e, cases); pexp_loc=loc }, + []) + }] + ) -> + let exception Found of (string * Parsetree.expression) in + let find_constr c = + try + List.iter (fun case -> + match case.pc_lhs with + | { ppat_desc = Ppat_construct ( + { txt = Lident name } , + Some { ppat_desc = Ppat_var { txt = var } }) } + when name = c -> + raise (Found (var, default_mapper.expr mapper case.pc_rhs)) + | _ -> () + ) cases; + assert false + with Found v_e -> v_e + in + let id = "matchnat#" in + let p, ifplus = find_constr "Plus" in + let m, ifminus = find_constr "Minus" in + let exp = default_mapper.expr mapper e in + Exp.let_ ~loc Nonrecursive + [ Vb.mk (Pat.var { txt = id; loc }) exp] + (Exp.ifthenelse ~loc + (Exp.apply ~loc (exp_ident ~loc ">=") + [ Nolabel, exp_ident ~loc id ; + Nolabel, Exp.apply ~loc (exp_ident ~loc "Int.of_string") + [Nolabel, exp_string ~loc "0"]]) + (Exp.let_ ~loc Nonrecursive + [ Vb.mk (Pat.var { txt = p; loc }) + (Exp.apply ~loc:ifplus.pexp_loc + (exp_ident ~loc "abs") + [Nolabel, exp_ident ~loc id])] + ifplus) + (Some (Exp.let_ ~loc Nonrecursive + [ Vb.mk (Pat.var { txt = m; loc }) + (Exp.apply ~loc:ifminus.pexp_loc + (exp_ident ~loc "abs") + [Nolabel, exp_ident ~loc id])] + ifminus))) + | _ -> default_mapper.expr mapper expr ); (* `String of int * string` is compiled as `String of (int * string)` *) diff --git a/tools/liquidity/with-tezos/liquidFromTezos.ml b/tools/liquidity/with-tezos/liquidFromTezos.ml index e86948c4..923bf5b2 100644 --- a/tools/liquidity/with-tezos/liquidFromTezos.ml +++ b/tools/liquidity/with-tezos/liquidFromTezos.ml @@ -248,7 +248,7 @@ let convert_contract loc_table 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 loc_table c.Script_repr.code in - { code; storage; return; parameter } + { code; spec = (); storage; return; parameter } let liquid_loc_of_script_loc f { Script_located_ir.start; stop } = { loc_file = f; diff --git a/tools/liquidity/with-tezos/liquidToTezos.ml b/tools/liquidity/with-tezos/liquidToTezos.ml index c214e28e..0067ae83 100644 --- a/tools/liquidity/with-tezos/liquidToTezos.ml +++ b/tools/liquidity/with-tezos/liquidToTezos.ml @@ -97,7 +97,7 @@ let rec convert_type expr = | Tset x -> prim "set" [convert_type x] | Tlist x -> prim "list" [convert_type x] | Toption x -> prim "option" [convert_type x] - | Tfail -> assert false + | Tfail | Trecord _ | Tsum _ -> assert false | Ttype (_, ty) -> convert_type ty let rec convert_code expr = diff --git a/tools/liquidity/without-tezos/liquidToTezos.ml b/tools/liquidity/without-tezos/liquidToTezos.ml index 97988e5b..135a8042 100644 --- a/tools/liquidity/without-tezos/liquidToTezos.ml +++ b/tools/liquidity/without-tezos/liquidToTezos.ml @@ -9,10 +9,10 @@ open LiquidTypes -let string_of_contract (c : michelson_exp contract) = +let string_of_contract (c : michelson_contract) = LiquidPrinter.Michelson.string_of_contract c -let convert_contract (c : noloc_michelson contract) = +let convert_contract (c : noloc_michelson_contract) = LiquidEmit.emit_contract c let read_tezos_file (_filename : string) = assert false