Merge branch 'feature/new-operators' into 'dev'

Feature/new operators

See merge request ligolang/ligo!53
This commit is contained in:
Gabriel Alfour 2019-07-21 09:53:34 +00:00
commit 18f5601035
26 changed files with 696 additions and 165 deletions

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 ->

View File

@ -87,16 +87,20 @@ let add : environment -> (string * type_value) -> michelson result = fun e (_s ,
ok code
let select : environment -> string list -> michelson result = fun e lst ->
let select ?(rev = false) ?(keep = true) : environment -> string list -> michelson result = fun e lst ->
let module L = Logger.Stateful() in
let e_lst =
let e_lst = Environment.to_list e in
let aux selector (s , _) =
L.log @@ Format.asprintf "Selector : %a\n" PP_helpers.(list_sep string (const " , ")) selector ;
match List.mem s selector with
| true -> List.remove_element s selector , true
| false -> selector , false in
let e_lst' = List.fold_map_right aux lst e_lst in
| true -> List.remove_element s selector , keep
| false -> selector , not keep in
let e_lst' =
if rev = keep
then List.fold_map aux lst e_lst
else List.fold_map_right aux lst e_lst
in
let e_lst'' = List.combine e_lst e_lst' in
e_lst'' in
let code =
@ -144,8 +148,8 @@ let clear : environment -> (michelson * environment) result = fun e ->
let%bind first_name =
trace_option (simple_error "try to clear empty env") @@
List.nth_opt lst 0 in
let%bind code = select e [ first_name ] in
let e' = Environment.select [ first_name ] e in
let%bind code = select ~rev:true e [ first_name ] in
let e' = Environment.select ~rev:true [ first_name ] e in
ok (code , e')
let pack : environment -> michelson result = fun e ->

View File

@ -19,7 +19,17 @@ let get_predicate : string -> type_value -> expression list -> predicate result
| "NONE" -> (
let%bind ty' = Mini_c.get_t_option ty in
let%bind m_ty = Compiler_type.type_ ty' in
ok @@ simple_unary @@ prim ~children:[m_ty] I_NONE
ok @@ simple_constant @@ 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
)
| "SET_EMPTY" -> (
let%bind ty' = Mini_c.get_t_set ty in
let%bind m_ty = Compiler_type.type_ ty' in
ok @@ simple_constant @@ prim ~children:[m_ty] I_EMPTY_SET
)
| "UNPACK" -> (
let%bind ty' = Mini_c.get_t_option ty in
@ -81,14 +91,16 @@ let rec translate_value (v:value) : michelson result = match v with
ok @@ prim ~children:[s'] D_Some
| D_map lst ->
let%bind lst' = bind_map_list (bind_map_pair translate_value) lst in
let sorted = List.sort (fun (x , _) (y , _) -> compare x y) lst' in
let aux (a, b) = prim ~children:[a;b] D_Elt in
ok @@ seq @@ List.map aux lst'
ok @@ seq @@ List.map aux sorted
| D_list lst ->
let%bind lst' = bind_map_list translate_value lst in
ok @@ seq lst'
| D_set lst ->
let%bind lst' = bind_map_list translate_value lst in
ok @@ seq lst'
let sorted = List.sort compare lst' in
ok @@ seq sorted
| D_operation _ ->
simple_fail "can't compile an operation"
@ -96,30 +108,50 @@ and translate_function (content:anon_function) : michelson result =
let%bind body = translate_quote_body content in
ok @@ seq [ body ]
and translate_expression ?(first=false) (expr:expression) (env:environment) : (michelson * environment) result =
and translate_expression ?push_var_name (expr:expression) (env:environment) : (michelson * environment) result =
let (expr' , ty) = Combinators.Expression.(get_content expr , get_type expr) in
let error_message () =
Format.asprintf "\n- expr: %a\n- type: %a\n" PP.expression expr PP.type_ ty
in
let i_skip = i_push_unit in
(* let i_skip = i_push_unit in *)
let return ?prepend_env ?end_env code =
let return ?prepend_env ?end_env ?(unit_opt = false) code =
let code =
if unit_opt && push_var_name <> None
then seq [code ; i_push_unit]
else code
in
let%bind env' =
match (prepend_env , end_env) with
| (Some _ , Some _) -> simple_fail ("two args to return at " ^ __LOC__)
| None , None -> ok @@ Environment.add ("_tmp_expression" , ty) env
| Some prepend_env , None ->
match (prepend_env , end_env , push_var_name) with
| (Some _ , Some _ , _) ->
simple_fail ("two args to return at " ^ __LOC__)
| None , None , None ->
ok @@ Environment.add ("_tmp_expression" , ty) env
| None , None , Some push_var_name ->
ok @@ Environment.add (push_var_name , ty) env
| Some prepend_env , None , None ->
ok @@ Environment.add ("_tmp_expression" , ty) prepend_env
| None , Some end_env -> ok end_env in
| Some prepend_env , None , Some push_var_name ->
ok @@ Environment.add (push_var_name , ty) prepend_env
| None , Some end_env , None ->
ok end_env
| None , Some end_env , Some push_var_name -> (
if unit_opt
then ok @@ Environment.add (push_var_name , ty) end_env
else ok end_env
)
in
let%bind (Stack.Ex_stack_ty input_stack_ty) = Compiler_type.Ty.environment env in
let%bind output_type = Compiler_type.type_ ty in
let%bind (Stack.Ex_stack_ty output_stack_ty) = Compiler_type.Ty.environment env' in
let error_message () =
let%bind schema_michelsons = Compiler_type.environment env in
ok @@ Format.asprintf
"expression : %a\ncode : %a\nschema type : %a\noutput type : %a"
"expression : %a\ncode : %a\npreenv : %a\npostenv : %a\nschema type : %a\noutput type : %a"
PP.expression expr
Michelson.pp code
PP.environment env
PP.environment env'
PP_helpers.(list_sep Michelson.pp (const ".")) schema_michelsons
Michelson.pp output_type
in
@ -138,28 +170,27 @@ and translate_expression ?(first=false) (expr:expression) (env:environment) : (m
trace (error (thunk "compiling expression") error_message) @@
match expr' with
| E_skip -> return @@ i_skip
| E_skip -> return ~end_env:env ~unit_opt:true @@ seq []
| E_environment_capture c ->
let%bind code = Compiler_environment.pack_select env c in
return @@ code
| E_environment_load (expr , load_env) ->
let%bind (expr' , _) = translate_expression expr env in
| E_environment_load (expr , load_env) -> (
let%bind (expr' , _) = translate_expression ~push_var_name:"env_to_load" expr env in
let%bind clear = Compiler_environment.select env [] in
let%bind unpack = Compiler_environment.unpack load_env in
return ~prepend_env:load_env @@ seq [
return ~end_env:load_env @@ seq [
expr' ;
dip clear ;
unpack ;
i_skip ;
]
)
| E_environment_select sub_env ->
let%bind code = Compiler_environment.select_env env sub_env in
return ~prepend_env:sub_env @@ seq [
return ~end_env:sub_env @@ seq [
code ;
i_skip ;
]
| E_environment_return expr -> (
let%bind (expr' , env) = translate_expression expr env in
let%bind (expr' , env) = translate_expression ~push_var_name:"return_clause" expr env in
let%bind (code , cleared_env) = Compiler_environment.clear env in
return ~end_env:cleared_env @@ seq [
expr' ;
@ -174,8 +205,8 @@ and translate_expression ?(first=false) (expr:expression) (env:environment) : (m
match Combinators.Expression.get_type f with
| T_function _ -> (
trace (simple_error "Compiling quote application") @@
let%bind (f , env') = translate_expression ~first f env in
let%bind (arg , _) = translate_expression arg env' in
let%bind (f , env') = translate_expression ~push_var_name:"application_f" f env in
let%bind (arg , _) = translate_expression ~push_var_name:"application_arg" arg env' in
return @@ seq [
i_comment "quote application" ;
i_comment "get f" ;
@ -187,8 +218,8 @@ and translate_expression ?(first=false) (expr:expression) (env:environment) : (m
)
| T_deep_closure (small_env, input_ty , _) -> (
trace (simple_error "Compiling deep closure application") @@
let%bind (arg' , env') = translate_expression arg env in
let%bind (f' , env'') = translate_expression f env' in
let%bind (arg' , env') = translate_expression ~push_var_name:"closure_arg" arg env in
let%bind (f' , env'') = translate_expression ~push_var_name:"closure_f" f env' in
let%bind f_ty = Compiler_type.type_ f.type_value in
let%bind append_closure = Compiler_environment.add_packed_anon small_env input_ty in
let error =
@ -221,20 +252,19 @@ and translate_expression ?(first=false) (expr:expression) (env:environment) : (m
| E_variable x ->
let%bind code = Compiler_environment.get env x in
return code
| E_sequence (a , b) ->
| E_sequence (a , b) -> (
let%bind (a' , env_a) = translate_expression a env in
let%bind env_a' = Compiler_environment.pop env_a in
let%bind (b' , env_b) = translate_expression b env_a' in
let%bind (b' , env_b) = translate_expression b env_a in
return ~end_env:env_b @@ seq [
a' ;
i_drop ;
b' ;
]
)
| E_constant(str, lst) ->
let module L = Logger.Stateful() in
let%bind lst' =
let aux env expr =
let%bind (code , env') = translate_expression expr env in
let%bind (code , env') = translate_expression ~push_var_name:"constant_argx" expr env in
L.log @@ Format.asprintf "\n%a -> %a in %a\n"
PP.expression expr
Michelson.pp code
@ -282,22 +312,22 @@ and translate_expression ?(first=false) (expr:expression) (env:environment) : (m
let%bind o' = Compiler_type.type_ o in
return @@ i_none o'
| E_if_bool (c, a, b) -> (
let%bind (c' , env') = translate_expression c env in
let%bind (c' , env') = translate_expression ~push_var_name:"bool_condition" c env in
let%bind popped = Compiler_environment.pop env' in
let%bind (a' , _) = translate_expression a popped in
let%bind (b' , _) = translate_expression b popped in
let%bind (a' , env_a') = translate_expression ~push_var_name:"if_true" a popped in
let%bind (b' , _env_b') = translate_expression ~push_var_name:"if_false" b popped in
let%bind code = ok (seq [
c' ;
i_if a' b' ;
]) in
return code
return ~end_env:env_a' code
)
| E_if_none (c, n, (ntv , s)) -> (
let%bind (c' , env') = translate_expression c env in
let%bind (c' , env') = translate_expression ~push_var_name:"if_none_condition" c env in
let%bind popped = Compiler_environment.pop env' in
let%bind (n' , _) = translate_expression n popped in
let%bind (n' , _) = translate_expression ~push_var_name:"if_none" n popped in
let s_env = Environment.add ntv popped in
let%bind (s' , s_env') = translate_expression s s_env in
let%bind (s' , s_env') = translate_expression ~push_var_name:"if_some" s s_env in
let%bind popped' = Compiler_environment.pop s_env' in
let%bind restrict_s = Compiler_environment.select_env popped' popped in
let%bind code = ok (seq [
@ -311,11 +341,11 @@ and translate_expression ?(first=false) (expr:expression) (env:environment) : (m
return code
)
| E_if_left (c, (l_ntv , l), (r_ntv , r)) -> (
let%bind (c' , _env') = translate_expression c env in
let%bind (c' , _env') = translate_expression ~push_var_name:"if_left_cond" c env in
let l_env = Environment.add l_ntv env in
let%bind (l' , _) = translate_expression l l_env in
let%bind (l' , _l_env') = translate_expression ~push_var_name:"if_left" l l_env in
let r_env = Environment.add r_ntv env in
let%bind (r' , _) = translate_expression r r_env in
let%bind (r' , _r_env') = translate_expression ~push_var_name:"if_right" r r_env in
let%bind restrict_l = Compiler_environment.select_env l_env env in
let%bind restrict_r = Compiler_environment.select_env r_env env in
let%bind code = ok (seq [
@ -334,11 +364,11 @@ and translate_expression ?(first=false) (expr:expression) (env:environment) : (m
return code
)
| E_let_in (v , expr , body) -> (
let%bind (expr' , expr_env) = translate_expression expr env in
let%bind (expr' , expr_env) = translate_expression ~push_var_name:"let_expr" expr env in
let%bind env' =
let%bind popped = Compiler_environment.pop expr_env in
ok @@ Environment.add v popped in
let%bind (body' , body_env) = translate_expression body env' in
let%bind (body' , body_env) = translate_expression ~push_var_name:"let_body" body env' in
let%bind restrict =
let%bind popped = Compiler_environment.pop body_env in
Compiler_environment.select_env popped env in
@ -350,9 +380,38 @@ and translate_expression ?(first=false) (expr:expression) (env:environment) : (m
]) in
return code
)
| E_iterator (name , (v , body) , expr) -> (
let%bind (expr' , expr_env) = translate_expression ~push_var_name:"iter_expr" expr env in
let%bind popped = Compiler_environment.pop expr_env in
let%bind env' = ok @@ Environment.add v popped in
let%bind (body' , body_env) = translate_expression ~push_var_name:"iter_body" body env' in
match name with
| "ITER" -> (
let%bind restrict =
Compiler_environment.select_env body_env popped in
let%bind code = ok (seq [
expr' ;
i_iter (seq [body' ; restrict]) ;
]) in
return ~end_env:popped code
)
| "MAP" -> (
let%bind restrict =
let%bind popped' = Compiler_environment.pop body_env in
Compiler_environment.select_env popped' popped in
let%bind code = ok (seq [
expr' ;
i_map (seq [body' ; dip restrict]) ;
]) in
return ~prepend_env:popped code
)
| s -> (
let error = error (thunk "bad iterator") (thunk s) in
fail error
)
)
| E_assignment (name , lrs , expr) -> (
let%bind (expr' , env') = translate_expression expr env in
(* Format.printf "\nass env':%a\n" PP.environment env' ; *)
let%bind (expr' , env') = translate_expression ~push_var_name:"assignment_expr" expr env in
let%bind get_code = Compiler_environment.get env' name in
let modify_code =
let aux acc step = match step with
@ -374,7 +433,7 @@ and translate_expression ?(first=false) (expr:expression) (env:environment) : (m
in
error title content in
trace error @@
return ~prepend_env:env @@ seq [
return ~end_env:env ~unit_opt:true @@ seq [
i_comment "assign: start # env" ;
expr' ;
i_comment "assign: compute rhs # rhs : env" ;
@ -386,27 +445,25 @@ and translate_expression ?(first=false) (expr:expression) (env:environment) : (m
i_comment "assign: modify code # name+rhs : env" ;
set_code ;
i_comment "assign: set new # new_env" ;
i_skip ;
]
)
| E_while (expr, block) -> (
let%bind (expr' , env') = translate_expression expr env in
| E_while (expr , block) -> (
let%bind (expr' , env') = translate_expression ~push_var_name:"while_expr" expr env in
let%bind popped = Compiler_environment.pop env' in
let%bind (block' , env'') = translate_expression block popped in
let%bind restrict_block = Compiler_environment.select_env env'' popped in
return @@ seq [
return ~end_env:env ~unit_opt:true @@ seq [
expr' ;
prim ~children:[seq [
block' ;
restrict_block ;
expr']] I_LOOP ;
i_skip ;
]
)
and translate_quote_body ({result ; binder ; input} as f:anon_function) : michelson result =
let env = Environment.(add (binder , input) empty) in
let%bind (expr , _) = translate_expression result env in
let%bind (expr , env') = translate_expression result env in
let code = seq [
i_comment "function result" ;
expr ;
@ -419,10 +476,13 @@ and translate_quote_body ({result ; binder ; input} as f:anon_function) : michel
let output_stack_ty = Stack.(output_ty @: nil) in
let error_message () =
Format.asprintf
"\ncode : %a\ninput : %a\noutput : %a\n"
"\nCode : %a\nMichelson code : %a\ninput : %a\noutput : %a\nstart env : %a\nend env : %a\n"
PP.expression result
Michelson.pp code
PP.type_ f.input
PP.type_ f.output
PP.environment env
PP.environment env'
in
let%bind _ =
Trace.trace_tzresult_lwt (

View File

@ -10,12 +10,14 @@ module Contract_types = Meta_michelson.Types
module Ty = struct
let not_comparable name () = error (thunk "not a comparable type") (fun () -> name) ()
let not_compilable_type name () = error (thunk "not a compilable type") (fun () -> name) ()
let comparable_type_base : type_base -> ex_comparable_ty result = fun tb ->
let open Contract_types in
let return x = ok @@ Ex_comparable_ty x in
match tb with
| Base_unit -> fail (not_comparable "unit")
| Base_void -> fail (not_comparable "void")
| Base_bool -> fail (not_comparable "bool")
| Base_nat -> return nat_k
| Base_tez -> return tez_k
@ -44,6 +46,7 @@ module Ty = struct
let return x = ok @@ Ex_ty x in
match b with
| Base_unit -> return unit
| Base_void -> fail (not_compilable_type "void")
| Base_bool -> return bool
| Base_int -> return int
| Base_nat -> return nat
@ -118,6 +121,7 @@ end
let base_type : type_base -> O.michelson result =
function
| Base_unit -> ok @@ O.prim T_unit
| Base_void -> fail (Ty.not_compilable_type "void")
| Base_bool -> ok @@ O.prim T_bool
| Base_int -> ok @@ O.prim T_int
| Base_nat -> ok @@ O.prim T_nat

View File

@ -68,15 +68,11 @@ let rec translate_value (Ex_typed_value (ty, value)) : value result =
in
ok @@ D_map lst'
| (List_t (ty, _)), lst ->
let lst' =
let aux acc cur = cur :: acc in
let lst = List.fold_left aux lst [] in
List.rev lst in
let%bind lst'' =
let%bind lst' =
let aux = fun t -> translate_value (Ex_typed_value (ty, t)) in
bind_map_list aux lst'
bind_map_list aux lst
in
ok @@ D_list lst''
ok @@ D_list lst'
| (Set_t (ty, _)), (module S) -> (
let lst = S.OPS.elements S.boxed in
let lst' =

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

View File

@ -0,0 +1,8 @@
function or_op (const n : nat) : nat is
begin skip end with bitwise_or(n , 4n)
function and_op (const n : nat) : nat is
begin skip end with bitwise_and(n , 7n)
function xor_op (const n : nat) : nat is
begin skip end with bitwise_xor(n , 7n)

View File

@ -17,3 +17,17 @@ const bl : foobar = list
120 ;
421 ;
end
function iter_op (const s : list(int)) : int is
var r : int := 0 ;
function aggregate (const i : int) : unit is
begin
r := r + i ;
end with unit
begin
list_iter(s , aggregate) ;
end with r
function map_op (const s : list(int)) : list(int) is
function increment (const i : int) : int is block { skip } with i + 1
block { skip } with list_map(s , increment)

View File

@ -31,3 +31,14 @@ const bm : foobar = map
120 -> 23 ;
421 -> 23 ;
end
function iter_op (const m : foobar) : int is
var r : int := 0 ;
function aggregate (const i : int ; const j : int) : unit is block { r := r + i + j } with unit ;
block {
map_iter(m , aggregate) ;
} with r ;
function map_op (const m : foobar) : foobar is
function increment (const i : int ; const j : int) : int is block { skip } with j + 1 ;
block { skip } with map_map(m , increment) ;

View File

@ -0,0 +1,26 @@
function iter_op (const s : set(int)) : int is
var r : int := 0 ;
function aggregate (const i : int) : unit is
begin
r := r + i ;
end with unit
begin
set_iter(s , aggregate) ;
end with r
const s_e : set(string) = (set_empty : set(string))
const s_fb : set(string) = set [
"foo" ;
"bar" ;
]
function add_op (const s : set(string)) : set(string) is
begin skip end with set_add("foobar" , s)
function remove_op (const s : set(string)) : set(string) is
begin skip end with set_remove("foobar" , s)
function mem_op (const s : set(string)) : bool is
begin skip end with set_mem("foobar" , s)

View File

@ -0,0 +1,5 @@
function concat_op (const s : string) : string is
begin skip end with string_concat(s , "toto")
function slice_op (const s : string) : string is
begin skip end with string_slice(1n , 2n , s)

View File

@ -32,8 +32,23 @@ let run_entry ?(debug_michelson = false) ?options (entry:anon_function) (input:v
error title content in
trace error @@
translate_entry entry in
if debug_michelson then Format.printf "Program: %a\n" Michelson.pp compiled.body ;
let%bind input_michelson = translate_value input in
if debug_michelson then (
Format.printf "Program: %a\n" Michelson.pp compiled.body ;
Format.printf "Expression: %a\n" PP.expression entry.result ;
Format.printf "Input: %a\n" PP.value input ;
Format.printf "Input Type: %a\n" PP.type_ entry.input ;
Format.printf "Compiled Input: %a\n" Michelson.pp input_michelson ;
) ;
let%bind ex_ty_value = run_aux ?options compiled input_michelson in
if debug_michelson then (
let (Ex_typed_value (ty , v)) = ex_ty_value in
ignore @@
let%bind michelson_value =
trace_tzresult_lwt (simple_error "debugging run_mini_c") @@
Proto_alpha_utils.Memory_proto_alpha.unparse_michelson_data ty v in
Format.printf "Compiled Output: %a\n" Michelson.pp michelson_value ;
ok ()
) ;
let%bind (result : value) = Compiler.Uncompiler.translate_value ex_ty_value in
ok result

View File

@ -17,8 +17,11 @@ let run_simplityped
let%bind annotated_result = Typer.untype_expression typed_result in
ok annotated_result
let evaluate_simplityped ?options (program : Ast_typed.program) (entry : string)
let evaluate_simplityped
?options
?(debug_mini_c = false) ?(debug_michelson = false)
(program : Ast_typed.program) (entry : string)
: Ast_simplified.expression result =
let%bind typed_result = Run_typed.evaluate_typed ?options entry program in
let%bind typed_result = Run_typed.evaluate_typed ?options ~debug_mini_c ~debug_michelson entry program in
let%bind annotated_result = Typer.untype_expression typed_result in
ok annotated_result

View File

@ -13,12 +13,18 @@ let transpile_value
let%bind r = Run_mini_c.run_entry f input in
ok r
let evaluate_typed ?options (entry:string) (program:Ast_typed.program) : Ast_typed.annotated_expression result =
let evaluate_typed
?(debug_mini_c = false) ?(debug_michelson = false)
?options (entry:string) (program:Ast_typed.program) : Ast_typed.annotated_expression result =
trace (simple_error "easy evaluate typed") @@
let%bind result =
let%bind mini_c_main =
Transpiler.translate_entry program entry in
Run_mini_c.run_entry ?options mini_c_main (Mini_c.Combinators.d_unit) in
(if debug_mini_c then
Format.(printf "Mini_c : %a\n%!" Mini_c.PP.function_ mini_c_main)
) ;
Run_mini_c.run_entry ?options ~debug_michelson mini_c_main (Mini_c.Combinators.d_unit)
in
let%bind typed_result =
let%bind typed_main = Ast_typed.get_entry program entry in
Transpiler.untranspile result typed_main.type_annotation in

View File

@ -10,6 +10,7 @@ let lr = fun ppf -> function `Left -> fprintf ppf "L" | `Right -> fprintf ppf "R
let type_base ppf : type_base -> _ = function
| Base_unit -> fprintf ppf "unit"
| Base_void -> fprintf ppf "void"
| Base_bool -> fprintf ppf "bool"
| Base_int -> fprintf ppf "int"
| Base_nat -> fprintf ppf "nat"
@ -48,7 +49,7 @@ let rec value ppf : value -> unit = function
| D_nat n -> fprintf ppf "+%d" n
| D_timestamp n -> fprintf ppf "+%d" n
| D_tez n -> fprintf ppf "%dtz" n
| D_unit -> fprintf ppf " "
| D_unit -> fprintf ppf "unit"
| D_string s -> fprintf ppf "\"%s\"" s
| D_bytes _ -> fprintf ppf "[bytes]"
| D_pair (a, b) -> fprintf ppf "(%a), (%a)" value a value b
@ -68,12 +69,12 @@ and expression' ppf (e:expression') = match e with
| E_environment_capture s -> fprintf ppf "capture(%a)" (list_sep string (const " ; ")) s
| E_environment_load (expr , env) -> fprintf ppf "load %a in %a" expression expr environment env
| E_environment_select env -> fprintf ppf "select %a" environment env
| E_environment_return expr -> fprintf ppf "return %a" expression expr
| E_environment_return expr -> fprintf ppf "return (%a)" expression expr
| E_skip -> fprintf ppf "skip"
| E_variable v -> fprintf ppf "%s" v
| E_variable v -> fprintf ppf "V(%s)" v
| E_application(a, b) -> fprintf ppf "(%a)@(%a)" expression a expression b
| E_constant(p, lst) -> fprintf ppf "%s %a" p (pp_print_list ~pp_sep:space_sep expression) lst
| E_literal v -> fprintf ppf "%a" value v
| E_literal v -> fprintf ppf "L(%a)" value v
| E_make_empty_map _ -> fprintf ppf "map[]"
| E_make_empty_list _ -> fprintf ppf "list[]"
| E_make_empty_set _ -> fprintf ppf "set[]"
@ -82,10 +83,11 @@ and expression' ppf (e:expression') = match e with
| E_if_none (c, n, ((name, _) , s)) -> fprintf ppf "%a ?? %a : %s -> %a" expression c expression n name expression s
| E_if_left (c, ((name_l, _) , l), ((name_r, _) , r)) ->
fprintf ppf "%a ?? %s -> %a : %s -> %a" expression c name_l expression l name_r expression r
| E_sequence (a , b) -> fprintf ppf "%a ; %a" expression a expression b
(* | E_sequence_drop (a , b) -> fprintf ppf "%a ;- %a" expression a expression b *)
| E_sequence (a , b) -> fprintf ppf "%a ;; %a" expression a expression b
| E_let_in ((name , _) , expr , body) ->
fprintf ppf "let %s = %a in ( %a )" name expression expr expression body
| E_iterator (s , ((name , _) , body) , expr) ->
fprintf ppf "for_%s %s of %a do ( %a )" s name expression expr expression body
| E_assignment (r , path , e) ->
fprintf ppf "%s.%a := %a" r (list_sep lr (const ".")) path expression e
| E_while (e , b) ->

View File

@ -32,14 +32,18 @@ module Environment (* : ENVIRONMENT *) = struct
let get_names : t -> string list = List.map fst
let remove : int -> t -> t = List.remove
let select : string list -> t -> t = fun lst env ->
let select ?(rev = false) ?(keep = true) : string list -> t -> t = fun lst env ->
let e_lst =
let e_lst = to_list env in
let aux selector (s , _) =
match List.mem s selector with
| true -> List.remove_element s selector , true
| false -> selector , false in
let e_lst' = List.fold_map_right aux lst e_lst in
| true -> List.remove_element s selector , keep
| false -> selector , not keep in
let e_lst' =
if rev = keep
then List.fold_map aux lst e_lst
else List.fold_map_right aux lst e_lst
in
let e_lst'' = List.combine e_lst e_lst' in
e_lst'' in
of_list

View File

@ -1,7 +1,7 @@
type type_name = string
type type_base =
| Base_unit
| Base_unit | Base_void
| Base_bool
| Base_int | Base_nat | Base_tez
| Base_timestamp
@ -69,6 +69,7 @@ and expression' =
| E_make_empty_list of type_value
| E_make_empty_set of type_value
| E_make_none of type_value
| E_iterator of (string * ((var_name * type_value) * expression) * expression)
| E_if_bool of expression * expression * expression
| E_if_none of expression * expression * ((var_name * type_value) * expression)
| E_if_left of expression * ((var_name * type_value) * expression) * ((var_name * type_value) * expression)

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

View File

@ -69,6 +69,20 @@ module Simplify = struct
("source" , "SOURCE") ;
("sender" , "SENDER") ;
("failwith" , "FAILWITH") ;
("bitwise_or" , "OR") ;
("bitwise_and" , "AND") ;
("bitwise_xor" , "XOR") ;
("string_concat" , "CONCAT") ;
("string_slice" , "SLICE") ;
("set_empty" , "SET_EMPTY") ;
("set_mem" , "SET_MEM") ;
("set_add" , "SET_ADD") ;
("set_remove" , "SET_REMOVE") ;
("set_iter" , "SET_ITER") ;
("list_iter" , "LIST_ITER") ;
("list_map" , "LIST_MAP") ;
("map_iter" , "MAP_ITER") ;
("map_map" , "MAP_MAP") ;
]
let type_constants = type_constants
@ -189,6 +203,11 @@ module Typer = struct
| None -> simple_fail "untyped NONE"
| Some t -> ok t
let set_empty = typer_0 "SET_EMPTY" @@ fun tv_opt ->
match tv_opt with
| None -> simple_fail "untyped SET_EMPTY"
| Some t -> ok t
let sub = typer_2 "SUB" @@ fun a b ->
if (eq_2 (a , b) (t_int ()))
then ok @@ t_int () else
@ -196,6 +215,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 +241,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,45 +256,72 @@ 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 m f ->
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 , res) = get_t_function f in
let%bind () = assert_eq_1 arg (t_pair k v ()) in
let%bind () = assert_eq_1 res (t_unit ()) in
ok @@ t_unit ()
let map_map : typer = typer_2 "MAP_MAP" @@ fun m f ->
let%bind (k, v) = get_t_map m in
let%bind (arg , res) = get_t_function f in
let%bind () = assert_eq_1 arg (t_pair k v ()) in
ok @@ t_map k 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 () =
@ -328,6 +376,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 +388,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,10 +409,18 @@ 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 ()
@ -387,6 +458,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 +480,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 (t_list 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 ;
@ -420,28 +561,34 @@ module Typer = struct
sub ;
none ;
some ;
concat ;
slice ;
comparator "EQ" ;
comparator "NEQ" ;
comparator "LT" ;
comparator "GT" ;
comparator "LE" ;
comparator "GE" ;
boolean_operator_2 "OR" ;
boolean_operator_2 "AND" ;
or_ ;
and_ ;
xor ;
not_ ;
map_remove ;
map_add ;
map_update ;
map_mem ;
map_find ;
map_map_fold ;
map_map ;
map_fold ;
map_iter ;
map_map ;
set_empty ;
set_mem ;
set_add ;
set_remove ;
(* map_size ; (* use size *) *)
set_iter ;
list_iter ;
list_map ;
int ;
size ;
failwith_ ;
@ -459,6 +606,7 @@ module Typer = struct
amount ;
transaction ;
get_contract ;
neg ;
abs ;
now ;
slice ;
@ -525,17 +673,19 @@ module Compiler = struct
("CALL" , simple_ternary @@ prim I_TRANSFER_TOKENS) ;
("SOURCE" , simple_constant @@ prim I_SOURCE) ;
("SENDER" , simple_constant @@ prim I_SENDER) ;
("MAP_ADD" , simple_ternary @@ seq [dip (i_some) ; prim I_UPDATE ]) ;
("MAP_ADD" , simple_ternary @@ seq [dip (i_some) ; prim I_UPDATE]) ;
("MAP_UPDATE" , simple_ternary @@ prim I_UPDATE) ;
("SET_MEM" , simple_binary @@ prim I_MEM) ;
("SET_ADD" , simple_binary @@ seq [dip (i_push (prim T_bool) (prim D_True)) ; prim I_UPDATE]) ;
("SLICE" , simple_ternary @@ prim I_SLICE) ;
("SET_REMOVE" , simple_binary @@ seq [dip (i_push (prim T_bool) (prim D_False)) ; prim I_UPDATE]) ;
("SLICE" , simple_ternary @@ seq [prim I_SLICE ; i_assert_some_msg (i_push_string "SLICE")]) ;
("SHA256" , simple_unary @@ prim I_SHA256) ;
("SHA512" , simple_unary @@ prim I_SHA512) ;
("BLAKE2B" , simple_unary @@ prim I_BLAKE2B) ;
("CHECK_SIGNATURE" , simple_ternary @@ prim I_CHECK_SIGNATURE) ;
("HASH_KEY" , simple_unary @@ prim I_HASH_KEY) ;
("PACK" , simple_unary @@ prim I_PACK) ;
("CONCAT" , simple_binary @@ prim I_CONCAT) ;
]
(* Some complex predicates will need to be added in compiler/compiler_program *)

View File

@ -135,7 +135,7 @@ module Errors = struct
let unsupported_for_loops region =
let title () = "bounded iterators" in
let message () =
Format.asprintf "for loops are not supported yet" in
Format.asprintf "only simple for loops are supported yet" in
let data = [
("loop_loc",
fun () -> Format.asprintf "%a" Location.pp_lift @@ region)
@ -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' =
@ -485,7 +484,7 @@ let rec simpl_expression (t:Raw.expr) : expr result =
fail @@ unsupported_string_catenation e
| ELogic l -> simpl_logic_expression l
| EList l -> simpl_list_expression l
| ESet _ -> fail @@ unsupported_set_expr t
| ESet s -> simpl_set_expression s
| ECase c -> (
let (c , loc) = r_split c in
let%bind e = simpl_expression c.expr in
@ -572,6 +571,21 @@ and simpl_list_expression (t:Raw.list_expr) : expression result =
return @@ e_list ~loc []
)
and simpl_set_expression (t:Raw.set_expr) : expression result =
match t with
| SetMem x -> (
let (x' , loc) = r_split x in
let%bind set' = simpl_expression x'.set in
let%bind element' = simpl_expression x'.element in
ok @@ e_constant ~loc "SET_MEM" [ element' ; set' ]
)
| SetInj x -> (
let (x' , loc) = r_split x in
let elements = pseq_to_list x'.elements in
let%bind elements' = bind_map_list simpl_expression elements in
ok @@ e_set ~loc elements'
)
and simpl_binop (name:string) (t:_ Raw.bin_op Region.reg) : expression result =
let return x = ok x in
let (t , loc) = r_split t in
@ -730,8 +744,19 @@ and simpl_statement : Raw.statement -> (_ -> expression result) result =
and simpl_single_instruction : Raw.single_instr -> (_ -> expression result) result =
fun t ->
match t with
| ProcCall call ->
fail @@ unsupported_proc_calls call
| ProcCall x -> (
let ((name, args) , loc) = r_split x in
let (f , f_loc) = r_split name in
let (args , args_loc) = r_split args in
let args' = npseq_to_list args.inside in
match List.assoc_opt f constants with
| None ->
let%bind arg = simpl_tuple_expression ~loc:args_loc args' in
return @@ e_application ~loc (e_variable ~loc:f_loc f) arg
| Some s ->
let%bind lst = bind_map_list simpl_expression args' in
return @@ e_constant ~loc s lst
)
| Fail e -> (
let%bind expr = simpl_expression e.value.fail_expr in
return @@ e_failwith expr
@ -746,7 +771,13 @@ and simpl_single_instruction : Raw.single_instr -> (_ -> expression result) resu
let%bind body = simpl_block l.block.value in
let%bind body = body None in
return @@ e_loop cond body
| Loop (For (ForInt {region; _} | ForCollect {region; _})) ->
(* | Loop (For (ForCollect x)) -> (
* let (x' , loc) = r_split x in
* let%bind expr = simpl_expression x'.expr in
* let%bind body = simpl_block x'.block.value in
* ok _
* ) *)
| Loop (For (ForInt {region; _} | ForCollect {region ; _})) ->
fail @@ unsupported_for_loops region
| Cond c -> (
let (c , loc) = r_split c in

View File

@ -127,13 +127,70 @@ 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)) ; *)
("neg_op", fun n -> (-n)) ;
] 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
let%bind () = expect_eq_n_pos program "div_op" e_int (fun n -> e_int (n / 2)) in
ok ()
let bitwise_arithmetic () : unit result =
let%bind program = type_file "./contracts/bitwise_arithmetic.ligo" in
let%bind () = expect_eq program "or_op" (e_nat 7) (e_nat 7) in
let%bind () = expect_eq program "or_op" (e_nat 3) (e_nat 7) in
let%bind () = expect_eq program "or_op" (e_nat 2) (e_nat 6) in
let%bind () = expect_eq program "or_op" (e_nat 14) (e_nat 14) in
let%bind () = expect_eq program "or_op" (e_nat 10) (e_nat 14) in
let%bind () = expect_eq program "and_op" (e_nat 7) (e_nat 7) in
let%bind () = expect_eq program "and_op" (e_nat 3) (e_nat 3) in
let%bind () = expect_eq program "and_op" (e_nat 2) (e_nat 2) in
let%bind () = expect_eq program "and_op" (e_nat 14) (e_nat 6) in
let%bind () = expect_eq program "and_op" (e_nat 10) (e_nat 2) in
let%bind () = expect_eq program "xor_op" (e_nat 0) (e_nat 7) in
let%bind () = expect_eq program "xor_op" (e_nat 7) (e_nat 0) in
ok ()
let string_arithmetic () : unit result =
let%bind program = type_file "./contracts/string_arithmetic.ligo" in
let%bind () = expect_eq program "concat_op" (e_string "foo") (e_string "foototo") in
let%bind () = expect_eq program "concat_op" (e_string "") (e_string "toto") in
let%bind () = expect_eq program "slice_op" (e_string "tata") (e_string "at") in
let%bind () = expect_eq program "slice_op" (e_string "foo") (e_string "oo") in
let%bind () = expect_fail program "slice_op" (e_string "ba") in
ok ()
let set_arithmetic () : unit result =
let%bind program = type_file "./contracts/set_arithmetic.ligo" in
let%bind () =
expect_eq program "add_op"
(e_set [e_string "foo" ; e_string "bar"])
(e_set [e_string "foo" ; e_string "bar" ; e_string "foobar"]) in
let%bind () =
expect_eq program "add_op"
(e_set [e_string "foo" ; e_string "bar" ; e_string "foobar"])
(e_set [e_string "foo" ; e_string "bar" ; e_string "foobar"]) in
let%bind () =
expect_eq program "remove_op"
(e_set [e_string "foo" ; e_string "bar"])
(e_set [e_string "foo" ; e_string "bar"]) in
let%bind () =
expect_eq program "remove_op"
(e_set [e_string "foo" ; e_string "bar" ; e_string "foobar"])
(e_set [e_string "foo" ; e_string "bar"]) in
let%bind () =
expect_eq program "mem_op"
(e_set [e_string "foo" ; e_string "bar" ; e_string "foobar"])
(e_bool true) in
let%bind () =
expect_eq program "mem_op"
(e_set [e_string "foo" ; e_string "bar"])
(e_bool false) in
let%bind () =
expect_eq program "iter_op"
(e_set [e_int 2 ; e_int 4 ; e_int 7])
(e_int 13) in
ok ()
let unit_expression () : unit result =
let%bind program = type_file "./contracts/unit.ligo" in
expect_eq_evaluate program "u" (e_unit ())
@ -291,6 +348,16 @@ let map () : unit result =
let expected = ez [23, 23] in
expect_eq program "rm" input expected
in
let%bind () =
let input = ez [(1 , 10) ; (2 , 20) ; (3 , 30) ] in
let expected = e_int 66 in
expect_eq program "iter_op" input expected
in
let%bind () =
let input = ez [(1 , 10) ; (2 , 20) ; (3 , 30) ] in
let expected = ez [(1 , 11) ; (2 , 21) ; (3 , 31) ] in
expect_eq program "map_op" input expected
in
ok ()
let list () : unit result =
@ -299,19 +366,29 @@ let list () : unit result =
let lst' = List.map e_int lst in
e_typed_list lst' t_int
in
let%bind () =
let expected = ez [23 ; 42] in
expect_eq_evaluate program "fb" expected
in
let%bind () =
let make_input = fun n -> (ez @@ List.range n) in
let make_expected = e_nat in
expect_eq_n_strict_pos_small program "size_" make_input make_expected
in
let%bind () =
let expected = ez [23 ; 42] in
expect_eq_evaluate program "fb" expected
in
let%bind () =
let expected = ez [144 ; 51 ; 42 ; 120 ; 421] in
expect_eq_evaluate program "bl" expected
in
let%bind () =
expect_eq program "iter_op"
(e_list [e_int 2 ; e_int 4 ; e_int 7])
(e_int 13)
in
let%bind () =
expect_eq program "map_op"
(e_list [e_int 2 ; e_int 4 ; e_int 7])
(e_list [e_int 3 ; e_int 5 ; e_int 8])
in
ok ()
let condition () : unit result =
@ -343,8 +420,7 @@ let loop () : unit result =
let make_expected = fun n -> e_nat (n * (n + 1) / 2) in
expect_eq_n_pos_mid program "sum" make_input make_expected
in
ok()
ok ()
let matching () : unit result =
let%bind program = type_file "./contracts/match.ligo" in
@ -563,6 +639,9 @@ let main = test_suite "Integration (End to End)" [
test "multiple parameters" multiple_parameters ;
test "bool" bool_expression ;
test "arithmetic" arithmetic ;
test "bitiwse_arithmetic" bitwise_arithmetic ;
test "string_arithmetic" string_arithmetic ;
test "set_arithmetic" set_arithmetic ;
test "unit" unit_expression ;
test "string" string_expression ;
test "option" option ;

View File

@ -32,7 +32,13 @@ let rec error_pp out (e : error) =
| `Null -> ""
| `List lst -> Format.asprintf "@[<v2>%a@]" PP_helpers.(list_sep error_pp (tag "@,")) lst
| _ -> " " ^ (J.to_string infos) ^ "\n" in
Format.fprintf out "%s%s%s.\n%s%s" title error_code message data infos
let children =
let children = e |> member "children" in
match children with
| `Null -> ""
| `List lst -> Format.asprintf "@[<v2>%a@]" PP_helpers.(list_sep error_pp (tag "@,")) lst
| _ -> " " ^ (J.to_string children) ^ "\n" in
Format.fprintf out "%s%s%s.\n%s%s%s" title error_code message data infos children
let test name f =
@ -62,6 +68,17 @@ let expect ?options program entry_point input expecter =
Ligo.Run.run_simplityped ~debug_michelson:true ?options program entry_point input in
expecter result
let expect_fail ?options program entry_point input =
let run_error =
let title () = "expect run" in
let content () = Format.asprintf "Entry_point: %s" entry_point in
error title content
in
trace run_error @@
Assert.assert_fail
@@ Ligo.Run.run_simplityped ~debug_michelson:true ?options program entry_point input
let expect_eq ?options program entry_point input expected =
let expecter = fun result ->
let expect_error =
@ -80,7 +97,7 @@ let expect_evaluate program entry_point expecter =
let content () = Format.asprintf "Entry_point: %s" entry_point in
error title content in
trace error @@
let%bind result = Ligo.Run.evaluate_simplityped program entry_point in
let%bind result = Ligo.Run.evaluate_simplityped ~debug_mini_c:true ~debug_michelson:true program entry_point in
expecter result
let expect_eq_evaluate program entry_point expected =

View File

@ -32,12 +32,22 @@ them. please report this to the developers." in
let content () = name in
error title content
let row_loc l = ("location" , fun () -> Format.asprintf "%a" Location.pp l)
let unsupported_pattern_matching kind location =
let title () = "unsupported pattern-matching" in
let content () = Format.asprintf "%s patterns aren't supported yet" kind in
let data = [
("location" , fun () -> Format.asprintf "%a" Location.pp location) ;
] in
row_loc location ;
] in
error ~data title content
let unsupported_iterator location =
let title () = "unsupported iterator" in
let content () = "only lambda are supported as iterators" in
let data = [
row_loc location ;
] in
error ~data title content
let not_functional_main location =
@ -341,15 +351,50 @@ and translate_annotated_expression (ae:AST.annotated_expression) : expression re
let%bind record' = translate_annotated_expression record in
let expr = List.fold_left aux record' path in
ok expr
| E_constant (name, lst) -> (
let%bind lst' = bind_map_list (translate_annotated_expression) lst in
match name, lst with
| "NONE", [] ->
let%bind o =
trace_strong (corner_case ~loc:__LOC__ "not an option") @@
Mini_c.Combinators.get_t_option tv in
return @@ E_make_none o
| _ -> return @@ E_constant (name, lst')
| E_constant (name , lst) -> (
let (iter , map) =
let iterator name = fun (lst : AST.annotated_expression list) -> match lst with
| [i ; f] -> (
let%bind f' = match f.expression with
| E_lambda l -> (
let%bind body' = translate_annotated_expression l.result in
let%bind input' = translate_type l.input_type in
ok ((l.binder , input') , body')
)
| E_variable v -> (
let%bind elt =
trace_option (corner_case ~loc:__LOC__ "missing var") @@
AST.Environment.get_opt v f.environment in
match elt.definition with
| ED_declaration (f , _) -> (
match f.expression with
| E_lambda l -> (
let%bind body' = translate_annotated_expression l.result in
let%bind input' = translate_type l.input_type in
ok ((l.binder , input') , body')
)
| _ -> fail @@ unsupported_iterator f.location
)
| _ -> fail @@ unsupported_iterator f.location
)
| _ -> fail @@ unsupported_iterator f.location
in
let%bind i' = translate_annotated_expression i in
return @@ E_iterator (name , f' , i')
)
| _ -> fail @@ corner_case ~loc:__LOC__ "bad iterator arity"
in
iterator "ITER" , iterator "MAP" in
match (name , lst) with
| ("SET_ITER" , lst) -> iter lst
| ("LIST_ITER" , lst) -> iter lst
| ("MAP_ITER" , lst) -> iter lst
| ("LIST_MAP" , lst) -> map lst
| ("MAP_MAP" , lst) -> map lst
| _ -> (
let%bind lst' = bind_map_list (translate_annotated_expression) lst in
return @@ E_constant (name , lst')
)
)
| E_lambda l ->
let%bind env =
@ -364,7 +409,7 @@ and translate_annotated_expression (ae:AST.annotated_expression) : expression re
let aux : expression -> expression -> expression result = fun prev cur ->
return @@ E_constant ("CONS", [cur ; prev]) in
let%bind (init : expression) = return @@ E_make_empty_list t in
bind_fold_list aux init lst'
bind_fold_right_list aux init lst'
)
| E_set lst -> (
let%bind t =
@ -372,7 +417,7 @@ and translate_annotated_expression (ae:AST.annotated_expression) : expression re
Mini_c.Combinators.get_t_set tv in
let%bind lst' = bind_map_list (translate_annotated_expression) lst in
let aux : expression -> expression -> expression result = fun prev cur ->
return @@ E_constant ("CONS", [cur ; prev]) in
return @@ E_constant ("SET_ADD", [cur ; prev]) in
let%bind (init : expression) = return @@ E_make_empty_set t in
bind_fold_list aux init lst'
)
@ -539,7 +584,7 @@ and translate_lambda env l =
let%bind output = translate_type output_type in
let tv = Combinators.t_function input output in
let content = D_function {binder;input;output;result=result'} in
ok @@ Combinators.Expression.make_tpl (E_literal content, tv)
ok @@ Combinators.Expression.make_tpl (E_literal content , tv)
)
| _ -> (
translate_lambda_deep env l

View File

@ -26,10 +26,12 @@ let trace_tzresult err =
let trace_tzresult_r err_thunk_may_fail =
function
| Result.Ok x -> ok x
| Error _errs ->
(* let tz_errs = List.map of_tz_error errs in *)
| Error errs ->
let tz_errs = List.map of_tz_error errs in
match err_thunk_may_fail () with
| Simple_utils.Trace.Ok (err, annotations) -> ignore annotations; Error (err)
| Simple_utils.Trace.Ok (err, annotations) ->
ignore annotations ;
Error (fun () -> patch_children tz_errs (err ()))
| Error errors_while_generating_error ->
(* TODO: the complexity could be O(n*n) in the worst case,
this should use some catenable lists. *)

View File

@ -48,6 +48,8 @@ let i_push_string str = i_push t_string (string str)
let i_none ty = prim ~children:[ty] I_NONE
let i_nil ty = prim ~children:[ty] I_NIL
let i_empty_set ty = prim ~children:[ty] I_EMPTY_SET
let i_iter body = prim ~children:[body] I_ITER
let i_map body = prim ~children:[body] I_MAP
let i_some = prim I_SOME
let i_lambda arg ret body = prim ~children:[arg;ret;body] I_LAMBDA
let i_empty_map src dst = prim ~children:[src;dst] I_EMPTY_MAP