balsoft/ligo
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

type new operators

Browse Source
This commit is contained in:
galfour 2019-07-19 12:13:09 +02:00
parent 4b6a58907d
commit 7b9d861a34
7 changed files with 222 additions and 47 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

8
src/ast_typed/combinators.ml
View File

@ -141,6 +141,11 @@ let get_t_map (t:type_value) : (type_value * type_value) result =
| T_constant ("map", [k;v]) -> ok (k, v)
| _ -> simple_fail "get: not a map"
let get_t_big_map (t:type_value) : (type_value * type_value) result =
match t.type_value' with
| T_constant ("big_map", [k;v]) -> ok (k, v)
| _ -> simple_fail "get: not a big_map"
let get_t_map_key : type_value -> type_value result = fun t ->
let%bind (key , _) = get_t_map t in
ok key
@ -154,6 +159,7 @@ let assert_t_map = fun t ->
ok ()
let is_t_map = Function.compose to_bool get_t_map
let is_t_big_map = Function.compose to_bool get_t_big_map
let assert_t_tez : type_value -> unit result = get_t_tez
let assert_t_key = get_t_key
@ -165,8 +171,10 @@ let assert_t_list t =
ok ()
let is_t_list = Function.compose to_bool get_t_list
let is_t_set = Function.compose to_bool get_t_set
let is_t_nat = Function.compose to_bool get_t_nat
let is_t_string = Function.compose to_bool get_t_string
let is_t_bytes = Function.compose to_bool get_t_bytes
let is_t_int = Function.compose to_bool get_t_int
let assert_t_bytes = fun t ->

5
src/compiler/compiler_program.ml
View File

@ -21,6 +21,11 @@ let get_predicate : string -> type_value -> expression list -> predicate result
let%bind m_ty = Compiler_type.type_ ty' in
ok @@ simple_unary @@ prim ~children:[m_ty] I_NONE
)
| "NIL" -> (
let%bind ty' = Mini_c.get_t_list ty in
let%bind m_ty = Compiler_type.type_ ty' in
ok @@ simple_unary @@ prim ~children:[m_ty] I_NIL
)
| "UNPACK" -> (
let%bind ty' = Mini_c.get_t_option ty in
let%bind m_ty = Compiler_type.type_ ty' in

3
src/contracts/arithmetic.ligo
View File

@ -15,3 +15,6 @@ function div_op (const n : int) : int is
function int_op (const n : nat) : int is
block { skip } with int(n)
function neg_op (const n : int) : int is
begin skip end with -n

35
src/operators/helpers.ml
View File

@ -70,6 +70,33 @@ module Typer = struct
| _ -> fail @@ wrong_param_number s 3 lst
let typer_3 name f : typer = (name , typer'_3 name f)
let typer'_4 : name -> (type_value -> type_value -> type_value -> type_value -> type_value result) -> typer' = fun s f lst _ ->
match lst with
| [ a ; b ; c ; d ] -> (
let%bind tv' = f a b c d in
ok (s , tv')
)
| _ -> fail @@ wrong_param_number s 4 lst
let typer_4 name f : typer = (name , typer'_4 name f)
let typer'_5 : name -> (type_value -> type_value -> type_value -> type_value -> type_value -> type_value result) -> typer' = fun s f lst _ ->
match lst with
| [ a ; b ; c ; d ; e ] -> (
let%bind tv' = f a b c d e in
ok (s , tv')
)
| _ -> fail @@ wrong_param_number s 5 lst
let typer_5 name f : typer = (name , typer'_5 name f)
let typer'_6 : name -> (type_value -> type_value -> type_value -> type_value -> type_value -> type_value -> type_value result) -> typer' = fun s f lst _ ->
match lst with
| [ a ; b ; c ; d ; e ; f_ ] -> (
let%bind tv' = f a b c d e f_ in
ok (s , tv')
)
| _ -> fail @@ wrong_param_number s 6 lst
let typer_6 name f : typer = (name , typer'_6 name f)
let constant name cst = typer_0 name (fun _ -> ok cst)
open Combinators
@ -77,6 +104,8 @@ module Typer = struct
let eq_1 a cst = type_value_eq (a , cst)
let eq_2 (a , b) cst = type_value_eq (a , cst) && type_value_eq (b , cst)
let assert_eq_1 a b = Assert.assert_true (eq_1 a b)
let comparator : string -> typer = fun s -> typer_2 s @@ fun a b ->
let%bind () =
trace_strong (error_uncomparable_types a b) @@
@ -114,8 +143,14 @@ module Compiler = struct
| Unary of michelson
| Binary of michelson
| Ternary of michelson
| Tetrary of michelson
| Pentary of michelson
| Hexary of michelson
let simple_constant c = Constant c
let simple_unary c = Unary c
let simple_binary c = Binary c
let simple_ternary c = Ternary c
let simple_tetrary c = Tetrary c
let simple_pentary c = Pentary c
let simple_hexary c = Hexary c
end

206
src/operators/operators.ml
View File

@ -91,7 +91,7 @@ module Simplify = struct
module Ligodity = struct
let constants = [
("assert" , "ASSERT") ;
("Current.balance", "BALANCE") ;
("balance", "BALANCE") ;
("Current.time", "NOW") ;
@ -132,7 +132,7 @@ module Simplify = struct
("Map.update" , "MAP_UPDATE") ;
("Map.add" , "MAP_ADD") ;
("Map.remove" , "MAP_REMOVE") ;
("String.length", "SIZE") ;
("String.size", "SIZE") ;
("String.slice", "SLICE") ;
@ -196,6 +196,8 @@ module Typer = struct
then ok @@ t_int () else
if (eq_2 (a , b) (t_timestamp ()))
then ok @@ t_int () else
if (eq_1 a (t_timestamp ()) && eq_1 b (t_int ()))
then ok @@ t_timestamp () else
if (eq_2 (a , b) (t_tez ()))
then ok @@ t_tez () else
fail (simple_error "Typing substraction, bad parameters.")
@ -220,7 +222,7 @@ module Typer = struct
let%bind () = assert_type_value_eq (dst, v') in
ok m
let map_mem : typer = typer_2 "MAP_MEM_TODO" @@ fun k m ->
let map_mem : typer = typer_2 "MAP_MEM" @@ fun k m ->
let%bind (src, _dst) = get_t_map m in
let%bind () = assert_type_value_eq (src, k) in
ok @@ t_bool ()
@ -235,46 +237,77 @@ module Typer = struct
let%bind () = assert_type_value_eq (src, k) in
ok @@ t_option dst ()
let map_fold : typer = typer_3 "MAP_FOLD_TODO" @@ fun f m acc ->
let%bind (src, dst) = get_t_map m in
let expected_f_type = t_function (t_tuple [(t_tuple [src ; dst] ()) ; acc] ()) acc () in
let%bind () = assert_type_value_eq (f, expected_f_type) in
ok @@ acc
let map_map : typer = typer_2 "MAP_MAP_TODO" @@ fun f m ->
let map_iter : typer = typer_2 "MAP_ITER" @@ fun f m ->
let%bind (k, v) = get_t_map m in
let%bind (input_type, result_type) = get_t_function f in
let%bind () = assert_type_value_eq (input_type, t_tuple [k ; v] ()) in
ok @@ t_map k result_type ()
let map_map_fold : typer = typer_3 "MAP_MAP_TODO" @@ fun f m acc ->
let%bind (k, v) = get_t_map m in
let%bind (input_type, result_type) = get_t_function f in
let%bind () = assert_type_value_eq (input_type, t_tuple [t_tuple [k ; v] () ; acc] ()) in
let%bind ttuple = get_t_tuple result_type in
match ttuple with
| [result_acc ; result_dst ] ->
ok @@ t_tuple [ t_map k result_dst () ; result_acc ] ()
(* TODO: error message *)
| _ -> fail @@ simple_error "function passed to map should take (k * v) * acc as an argument"
let map_iter : typer = typer_2 "MAP_MAP_TODO" @@ fun f m ->
let%bind (k, v) = get_t_map m in
let%bind () = assert_type_value_eq (f, t_function (t_tuple [k ; v] ()) (t_unit ()) ()) in
let%bind (arg_1 , res) = get_t_function f in
let%bind (arg_2 , res') = get_t_function res in
let%bind () = assert_eq_1 arg_1 k in
let%bind () = assert_eq_1 arg_2 v in
let%bind () = assert_eq_1 res' (t_unit ()) in
ok @@ t_unit ()
let map_map : typer = typer_2 "MAP_MAP" @@ fun f m ->
let%bind (k, v) = get_t_map m in
let%bind (arg_1 , res) = get_t_function f in
let%bind (arg_2 , res') = get_t_function res in
let%bind () = assert_eq_1 arg_1 k in
let%bind () = assert_eq_1 arg_2 v in
ok @@ res'
let map_fold : typer = typer_2 "MAP_FOLD" @@ fun f m ->
let%bind (k, v) = get_t_map m in
let%bind (arg_1 , res) = get_t_function f in
let%bind (arg_2 , res') = get_t_function res in
let%bind (arg_3 , res'') = get_t_function res' in
let%bind () = assert_eq_1 arg_1 k in
let%bind () = assert_eq_1 arg_2 v in
let%bind () = assert_eq_1 arg_3 res'' in
ok @@ res'
let big_map_remove : typer = typer_2 "BIG_MAP_REMOVE" @@ fun k m ->
let%bind (src , _) = get_t_big_map m in
let%bind () = assert_type_value_eq (src , k) in
ok m
let big_map_add : typer = typer_3 "BIG_MAP_ADD" @@ fun k v m ->
let%bind (src, dst) = get_t_big_map m in
let%bind () = assert_type_value_eq (src, k) in
let%bind () = assert_type_value_eq (dst, v) in
ok m
let big_map_update : typer = typer_3 "BIG_MAP_UPDATE" @@ fun k v m ->
let%bind (src, dst) = get_t_big_map m in
let%bind () = assert_type_value_eq (src, k) in
let%bind v' = get_t_option v in
let%bind () = assert_type_value_eq (dst, v') in
ok m
let big_map_mem : typer = typer_2 "BIG_MAP_MEM" @@ fun k m ->
let%bind (src, _dst) = get_t_big_map m in
let%bind () = assert_type_value_eq (src, k) in
ok @@ t_bool ()
let big_map_find : typer = typer_2 "BIG_MAP_FIND" @@ fun k m ->
let%bind (src, dst) = get_t_big_map m in
let%bind () = assert_type_value_eq (src, k) in
ok @@ dst
let size = typer_1 "SIZE" @@ fun t ->
let%bind () =
Assert.assert_true @@
(is_t_map t || is_t_list t || is_t_string t) in
(is_t_map t || is_t_list t || is_t_string t || is_t_bytes t || is_t_set t || is_t_big_map t) in
ok @@ t_nat ()
let slice = typer_3 "SLICE" @@ fun i j s ->
let%bind () =
Assert.assert_true @@
(is_t_nat i && is_t_nat j && is_t_string s) in
ok @@ t_string ()
let%bind () = assert_eq_1 i (t_nat ()) in
let%bind () = assert_eq_1 j (t_nat ()) in
if eq_1 s (t_string ())
then ok @@ t_string ()
else if eq_1 s (t_bytes ())
then ok @@ t_bytes ()
else simple_fail "bad slice"
let failwith_ = typer_1 "FAILWITH" @@ fun t ->
let%bind () =
Assert.assert_true @@
@ -319,7 +352,7 @@ module Typer = struct
let%bind () = assert_t_signature s in
let%bind () = assert_t_bytes b in
ok @@ t_bool ()
let sender = constant "SENDER" @@ t_address ()
let source = constant "SOURCE" @@ t_address ()
@ -328,6 +361,8 @@ module Typer = struct
let amount = constant "AMOUNT" @@ t_tez ()
let balance = constant "BALANCE" @@ t_tez ()
let address = constant "ADDRESS" @@ t_address ()
let now = constant "NOW" @@ t_timestamp ()
@ -338,6 +373,19 @@ module Typer = struct
let%bind () = assert_type_value_eq (param , contract_param) in
ok @@ t_operation ()
let originate = typer_6 "ORIGINATE" @@ fun manager delegate_opt spendable delegatable init_balance code ->
let%bind () = assert_eq_1 manager (t_key_hash ()) in
let%bind () = assert_eq_1 delegate_opt (t_option (t_key_hash ()) ()) in
let%bind () = assert_eq_1 spendable (t_bool ()) in
let%bind () = assert_eq_1 delegatable (t_bool ()) in
let%bind () = assert_t_tez init_balance in
let%bind (arg , res) = get_t_function code in
let%bind (_param , storage) = get_t_pair arg in
let%bind (storage' , op_lst) = get_t_pair res in
let%bind () = assert_eq_1 storage storage' in
let%bind () = assert_eq_1 op_lst (t_list (t_operation ()) ()) in
ok @@ (t_pair (t_operation ()) (t_address ()) ())
let get_contract = typer_1_opt "CONTRACT" @@ fun _ tv_opt ->
let%bind tv =
trace_option (simple_error "get_contract needs a type annotation") tv_opt in
@ -346,15 +394,23 @@ module Typer = struct
get_t_contract tv in
ok @@ t_contract tv' ()
let set_delegate = typer_1 "SET_DELEGATE" @@ fun delegate_opt ->
let%bind () = assert_eq_1 delegate_opt (t_option (t_key_hash ()) ()) in
ok @@ t_operation ()
let abs = typer_1 "ABS" @@ fun t ->
let%bind () = assert_t_int t in
ok @@ t_nat ()
let neg = typer_1 "NEG" @@ fun t ->
let%bind () = Assert.assert_true (eq_1 t (t_nat ()) || eq_1 t (t_int ())) in
ok @@ t_int ()
let assertion = typer_1 "ASSERT" @@ fun a ->
if eq_1 a (t_bool ())
then ok @@ t_unit ()
else simple_fail "Asserting a non-bool"
let times = typer_2 "TIMES" @@ fun a b ->
if eq_2 (a , b) (t_nat ())
then ok @@ t_nat () else
@ -387,6 +443,8 @@ module Typer = struct
then ok @@ t_tez () else
if (eq_1 a (t_nat ()) && eq_1 b (t_int ())) || (eq_1 b (t_nat ()) && eq_1 a (t_int ()))
then ok @@ t_int () else
if (eq_1 a (t_timestamp ()) && eq_1 b (t_int ())) || (eq_1 b (t_timestamp ()) && eq_1 a (t_int ()))
then ok @@ t_timestamp () else
simple_fail "Adding with wrong types. Expected nat, int or tez."
let set_mem = typer_2 "SET_MEM" @@ fun elt set ->
@ -407,11 +465,79 @@ module Typer = struct
then ok set
else simple_fail "Set_remove: elt and set don't match"
let set_iter = typer_2 "SET_ITER" @@ fun set body ->
let%bind (arg , res) = get_t_function body in
let%bind () = Assert.assert_true (eq_1 res (t_unit ())) in
let%bind key = get_t_set set in
if eq_1 key arg
then ok (t_unit ())
else simple_fail "bad set iter"
let list_iter = typer_2 "LIST_ITER" @@ fun lst body ->
let%bind (arg , res) = get_t_function body in
let%bind () = Assert.assert_true (eq_1 res (t_unit ())) in
let%bind key = get_t_list lst in
if eq_1 key arg
then ok (t_unit ())
else simple_fail "bad list iter"
let list_map = typer_2 "LIST_MAP" @@ fun lst body ->
let%bind (arg , res) = get_t_function body in
let%bind key = get_t_list lst in
if eq_1 key arg
then ok res
else simple_fail "bad list iter"
let not_ = typer_1 "NOT" @@ fun elt ->
if eq_1 elt (t_bool ())
then ok @@ t_bool ()
else if eq_1 elt (t_nat ()) || eq_1 elt (t_int ())
then ok @@ t_int ()
else simple_fail "bad parameter to not"
let or_ = typer_2 "OR" @@ fun a b ->
if eq_2 (a , b) (t_bool ())
then ok @@ t_bool ()
else if eq_2 (a , b) (t_nat ())
then ok @@ t_nat ()
else simple_fail "bad or"
let xor = typer_2 "XOR" @@ fun a b ->
if eq_2 (a , b) (t_bool ())
then ok @@ t_bool ()
else if eq_2 (a , b) (t_nat ())
then ok @@ t_nat ()
else simple_fail "bad xor"
let and_ = typer_2 "AND" @@ fun a b ->
if eq_2 (a , b) (t_bool ())
then ok @@ t_bool ()
else if eq_2 (a , b) (t_nat ()) || (eq_1 b (t_nat ()) && eq_1 a (t_int ()))
then ok @@ t_nat ()
else simple_fail "bad end"
let lsl_ = typer_2 "LSL" @@ fun a b ->
if eq_2 (a , b) (t_nat ())
then ok @@ t_nat ()
else simple_fail "bad lsl"
let lsr_ = typer_2 "LSR" @@ fun a b ->
if eq_2 (a , b) (t_nat ())
then ok @@ t_nat ()
else simple_fail "bad lsr"
let concat = typer_2 "CONCAT" @@ fun a b ->
if eq_2 (a , b) (t_string ())
then ok @@ t_string ()
else if eq_2 (a , b) (t_bytes ())
then ok @@ t_bytes ()
else simple_fail "bad concat"
let cons = typer_2 "CONS" @@ fun hd tl ->
let%bind elt = get_t_list tl in
let%bind () = assert_eq_1 hd elt in
ok tl
let constant_typers = Map.String.of_list [
add ;
times ;
@ -428,20 +554,19 @@ module Typer = struct
comparator "GE" ;
boolean_operator_2 "OR" ;
boolean_operator_2 "AND" ;
boolean_operator_2 "XOR" ;
not_ ;
map_remove ;
map_add ;
map_update ;
map_mem ;
map_find ;
map_map_fold ;
map_map ;
map_fold ;
map_iter ;
set_mem ;
set_add ;
set_remove ;
(* map_size ; (* use size *) *)
int ;
size ;
failwith_ ;
@ -459,6 +584,7 @@ module Typer = struct
amount ;
transaction ;
get_contract ;
neg ;
abs ;
now ;
slice ;
@ -539,5 +665,5 @@ module Compiler = struct
]
(* Some complex predicates will need to be added in compiler/compiler_program *)
end

11
src/simplify/pascaligo.ml
View File

@ -468,12 +468,11 @@ let rec simpl_expression (t:Raw.expr) : expr result =
return @@ e_literal ~loc (Literal_nat n)
)
| EArith (Mtz n) -> (
let (n , loc) = r_split n in
let n = Z.to_int @@ snd @@ n in
return @@ e_literal ~loc (Literal_tez n)
)
| EArith _ as e ->
fail @@ unsupported_arith_op e
let (n , loc) = r_split n in
let n = Z.to_int @@ snd @@ n in
return @@ e_literal ~loc (Literal_tez n)
)
| EArith (Neg e) -> simpl_unop "NEG" e
| EString (String s) ->
let (s , loc) = r_split s in
let s' =

1
src/test/integration_tests.ml
View File

@ -127,7 +127,6 @@ let arithmetic () : unit result =
("plus_op", fun n -> (n + 42)) ;
("minus_op", fun n -> (n - 42)) ;
("times_op", fun n -> (n * 42)) ;
(* ("div_op", fun n -> (n / 2)) ; *)
] in
let%bind () = expect_eq_n_pos program "int_op" e_nat e_int in
let%bind () = expect_eq_n_pos program "mod_op" e_int (fun n -> e_nat (n mod 42)) in