From d7426504d04803b3e3742899ca56cfe6abe827a1 Mon Sep 17 00:00:00 2001 From: Galfour Date: Sat, 20 Apr 2019 11:06:40 +0000 Subject: [PATCH] replace tuples by records --- src/ligo/compiler/compiler_program.ml | 14 -------- src/ligo/contracts/heap-instance.ligo | 3 ++ src/ligo/contracts/heap.ligo | 22 ++++++++---- src/ligo/contracts/shadow.ligo | 4 +++ src/ligo/ligo.ml | 18 ++++++++-- src/ligo/operators/operators.ml | 50 +++++++++++++-------------- src/ligo/simplify.ml | 44 +++++++++++------------ src/ligo/test/integration_tests.ml | 20 +++++++++-- src/ligo/transpiler.ml | 41 ++++++++++------------ src/ligo/typer.ml | 12 +++++-- 10 files changed, 129 insertions(+), 99 deletions(-) create mode 100644 src/ligo/contracts/shadow.ligo diff --git a/src/ligo/compiler/compiler_program.ml b/src/ligo/compiler/compiler_program.ml index 50912f999..44f27a73f 100644 --- a/src/ligo/compiler/compiler_program.ml +++ b/src/ligo/compiler/compiler_program.ml @@ -166,20 +166,6 @@ and translate_expression ?(first=false) (expr:expression) : michelson result = i_pair ; i_exec ; (* output :: stack :: env *) ] - (* return @@ virtual_push @@ seq [ - * i_comment "(\* unit :: env *\)" ; - * i_comment "compute closure" ; - * f' ; - * i_comment "(\* (closure * unit) :: env *\)" ; - * i_comment "compute arg" ; - * arg' ; - * i_comment "(\* (arg * closure * unit) :: env *\)" ; - * i_comment "separate stuff" ; - * i_unpair ; dip i_unpair ; dip i_unpair ; - * i_comment "(\* arg :: capture :: f :: unit :: env *\)" ; - * i_pair ; - * i_exec ; (\* output :: stack :: env *\) - * ] *) ) | _ -> simple_fail "E_applicationing something not appliable" ) diff --git a/src/ligo/contracts/heap-instance.ligo b/src/ligo/contracts/heap-instance.ligo index 4a165c68b..b214f0fab 100644 --- a/src/ligo/contracts/heap-instance.ligo +++ b/src/ligo/contracts/heap-instance.ligo @@ -1,3 +1,6 @@ type heap_element is int * string +function heap_element_lt(const x : heap_element ; const y : heap_element) : bool is + block { skip } with x.0 < y.0 + #include "heap.ligo" diff --git a/src/ligo/contracts/heap.ligo b/src/ligo/contracts/heap.ligo index 9039eba20..20f7dcf97 100644 --- a/src/ligo/contracts/heap.ligo +++ b/src/ligo/contracts/heap.ligo @@ -13,14 +13,22 @@ function pop_switch (const h : heap) : heap is const last : heap_element = get_force(s, h) ; remove 1n from map h ; h[1n] := last ; - } with h ; + } with h - -// function pop (const h : heap) : heap is +// function largest_child (const h : heap) : nat is // block { // const result : heap_element = get_top (h) ; // const s : nat = size(h) ; -// const last : heap_element = get_force(int(s), h) ; -// remove 1 from map h ; -// h[1] := last ; -// } with h ; +// var current : heap_element := get_force(s, h) ; +// const i : nat = 1n ; +// const left : nat = 2n * i ; +// const right : nat = left + 1n ; +// remove 1n from map h ; +// h[1n] := current ; +// var largest : nat := i ; +// if (left <= s and heap_element_lt(get_force(s , h) , get_force(left , h))) then +// largest := left +// else if (right <= s and heap_element_lt(get_force(s , h) , get_force(right , h))) then +// largest := right +// else skip +// } with largest diff --git a/src/ligo/contracts/shadow.ligo b/src/ligo/contracts/shadow.ligo new file mode 100644 index 000000000..4232cb0a6 --- /dev/null +++ b/src/ligo/contracts/shadow.ligo @@ -0,0 +1,4 @@ +function foo (const i : int) : int is + function bar (const i : int) : int is + block { skip } with i ; + block { skip } with bar (0) diff --git a/src/ligo/ligo.ml b/src/ligo/ligo.ml index 154078da7..ec6231d5f 100644 --- a/src/ligo/ligo.ml +++ b/src/ligo/ligo.ml @@ -35,13 +35,25 @@ let parse_file (source: string) : AST_Raw.t result = let start = Lexing.lexeme_start_p lexbuf in let end_ = Lexing.lexeme_end_p lexbuf in let str = Format.sprintf - "Parse error at \"%s\" from (%d, %d) to (%d, %d)\n" + "Parse error at \"%s\" from (%d, %d) to (%d, %d). In file \"%s|%s\"\n" (Lexing.lexeme lexbuf) start.pos_lnum (start.pos_cnum - start.pos_bol) - end_.pos_lnum (end_.pos_cnum - end_.pos_bol) in + end_.pos_lnum (end_.pos_cnum - end_.pos_bol) + start.pos_fname source + in simple_error str ) - | _ -> simple_error "unrecognized parse_ error" + | _ -> + let start = Lexing.lexeme_start_p lexbuf in + let end_ = Lexing.lexeme_end_p lexbuf in + let str = Format.sprintf + "Unrecognized error at \"%s\" from (%d, %d) to (%d, %d). In file \"%s|%s\"\n" + (Lexing.lexeme lexbuf) + start.pos_lnum (start.pos_cnum - start.pos_bol) + end_.pos_lnum (end_.pos_cnum - end_.pos_bol) + start.pos_fname source + in + simple_error str ) @@ (fun () -> let raw = Parser.contract read lexbuf in close () ; diff --git a/src/ligo/operators/operators.ml b/src/ligo/operators/operators.ml index 041e002fb..49a7b661d 100644 --- a/src/ligo/operators/operators.ml +++ b/src/ligo/operators/operators.ml @@ -162,31 +162,31 @@ module Typer = struct let typer_to_kv : typer -> (string * _) = fun (a, b, c) -> (a, (b, c)) in Map.String.of_list @@ List.map typer_to_kv [ - same_2 "ADD" [ - ("ADD_INT" , t_int ()) ; - ("ADD_NAT" , t_nat ()) ; - ("CONCAT" , t_string ()) ; - ] ; - same_2 "TIMES" [ - ("TIMES_INT" , t_int ()) ; - ("TIMES_NAT" , t_nat ()) ; - ] ; - sub ; - none ; - some ; - comparator "EQ" ; - comparator "LT" ; - comparator "GT" ; - comparator "LE" ; - comparator "GE" ; - boolean_operator_2 "OR" ; - boolean_operator_2 "AND" ; - map_remove ; - map_update ; - int ; - size ; - get_force ; - ] + same_2 "ADD" [ + ("ADD_INT" , t_int ()) ; + ("ADD_NAT" , t_nat ()) ; + ("CONCAT" , t_string ()) ; + ] ; + same_2 "TIMES" [ + ("TIMES_INT" , t_int ()) ; + ("TIMES_NAT" , t_nat ()) ; + ] ; + sub ; + none ; + some ; + comparator "EQ" ; + comparator "LT" ; + comparator "GT" ; + comparator "LE" ; + comparator "GE" ; + boolean_operator_2 "OR" ; + boolean_operator_2 "AND" ; + map_remove ; + map_update ; + int ; + size ; + get_force ; + ] end diff --git a/src/ligo/simplify.ml b/src/ligo/simplify.ml index 47ae1154c..0308c1446 100644 --- a/src/ligo/simplify.ml +++ b/src/ligo/simplify.ml @@ -318,16 +318,29 @@ and simpl_fun_declaration : Raw.fun_decl -> named_expression result = fun x -> ok {name;annotated_expression = {expression;type_annotation}} ) | lst -> ( + let arguments_name = "arguments" in let%bind params = bind_map_list simpl_param lst in let input = - let type_expression = T_record ( - SMap.of_list - @@ List.map (fun (x:named_type_expression) -> x.type_name, x.type_expression) - params - ) in - { type_name = "arguments" ; type_expression } in + let aux = fun x -> x.type_expression in + let type_expression = T_tuple (List.map aux params) in + { type_name = arguments_name ; type_expression } in let binder = input.type_name in let input_type = input.type_expression in + let tpl_declarations = + let aux = fun i (x:named_type_expression) -> + let ass = I_assignment { + name = x.type_name ; + annotated_expression = { + expression = E_accessor ({ + expression = E_variable arguments_name ; + type_annotation = Some input.type_expression ; + } , [ Access_tuple i ] ) ; + type_annotation = Some (x.type_expression) ; + } + } in + ass + in + List.mapi aux params in let%bind local_declarations = let%bind typed = bind_map_list simpl_local_declaration local_decls in ok (List.map fst typed) @@ -336,22 +349,9 @@ and simpl_fun_declaration : Raw.fun_decl -> named_expression result = fun x -> let%bind instructions = bind_list @@ List.map simpl_statement @@ npseq_to_list block.value.statements in - let%bind (body, result) = - let renamings = - let aux ({type_name}:named_type_expression) : Rename.Value.renaming = - type_name, ("arguments", [Access_record type_name]) - in - List.map aux params - in - let%bind r = - let%bind tmp = simpl_expression return in - Rename.Value.rename_annotated_expression renamings tmp - in - let%bind b = - let tmp = local_declarations @ instructions in - Rename.Value.rename_block renamings tmp - in - ok (b, r) in + + let body = tpl_declarations @ local_declarations @ instructions in + let%bind result = simpl_expression return in let expression = E_lambda {binder ; input_type ; output_type ; result ; body } in let type_annotation = Some (T_function (input_type, output_type)) in ok {name = name.value;annotated_expression = {expression;type_annotation}} diff --git a/src/ligo/test/integration_tests.ml b/src/ligo/test/integration_tests.ml index 576a1289e..731268a70 100644 --- a/src/ligo/test/integration_tests.ml +++ b/src/ligo/test/integration_tests.ml @@ -67,6 +67,21 @@ let closure () : unit result = @@ [0 ; 2 ; 42 ; 163 ; -1] in ok () +let shadow () : unit result = + let%bind program = type_file "./contracts/shadow.ligo" in + let%bind _foo = trace (simple_error "test foo") @@ + let aux n = + let open AST_Typed.Combinators in + let input = e_a_int n in + let%bind result = easy_run_typed "foo" program input in + let expected = e_a_int 0 in + AST_Typed.assert_value_eq (expected, result) + in + bind_list + @@ List.map aux + @@ [3 ; 2 ; 0 ; 42 ; 163 ; -1] in + ok () + let higher_order () : unit result = let%bind program = type_file "./contracts/high-order.ligo" in let%bind _foo = trace (simple_error "test foo") @@ @@ -314,7 +329,7 @@ let map () : unit result = let aux n = let input = let m = ez [(23, 0) ; (42, 0)] in - AST_Typed.Combinators.(ez_e_a_record [("n", e_a_int n) ; ("m", m)]) + AST_Typed.Combinators.(e_a_tuple [ e_a_int n ; m ]) in let%bind result = easy_run_typed "set_" program input in let expect = ez [(23, n) ; (42, 0)] in @@ -552,6 +567,8 @@ let main = "Integration (End to End)", [ test "complex function" complex_function ; test "closure" closure ; test "shared function" shared_function ; + test "shadow" shadow ; + test "multiple parameters" multiple_parameters ; test "bool" bool_expression ; test "arithmetic" arithmetic ; test "unit" unit_expression ; @@ -560,7 +577,6 @@ let main = "Integration (End to End)", [ test "option" option ; test "map" map ; test "list" list ; - test "multiple parameters" multiple_parameters ; test "condition" condition ; test "loop" loop ; test "matching" matching ; diff --git a/src/ligo/transpiler.ml b/src/ligo/transpiler.ml index ee5f9356d..8064acc3f 100644 --- a/src/ligo/transpiler.ml +++ b/src/ligo/transpiler.ml @@ -61,26 +61,21 @@ let rec translate_type (t:AST.type_value) : type_value result = let%bind result' = translate_type result in ok (T_function (param', result')) -let tuple_access_to_lr : type_value -> type_value list -> int -> (type_value * (type_value * [`Left | `Right]) list) result = fun ty tys ind -> +let tuple_access_to_lr : type_value -> type_value list -> int -> (type_value * [`Left | `Right]) list result = fun ty tys ind -> let node_tv = Append_tree.of_list @@ List.mapi (fun i a -> (i, a)) tys in - let leaf (i, _) : (type_value * (type_value * [`Left | `Right]) list) result = - if i = ind then ( - ok (ty, []) - ) else ( - simple_fail "bad leaf" - ) in - let node a b : (type_value * (type_value * [`Left | `Right]) list) result = - match%bind bind_lr (a, b) with - | `Left (t, acc) -> - let%bind (a, _) = get_t_pair t in - ok @@ (t, (a, `Left) :: acc) - | `Right (t, acc) -> ( - let%bind (_, b) = get_t_pair t in - ok @@ (t, (b, `Right) :: acc) - ) in - let error_content () = Format.asprintf "(%a).%d" (PP.list_sep_d PP.type_) tys ind in - trace_strong (fun () -> error (thunk "bad index in tuple (shouldn't happen here)") error_content ()) @@ - Append_tree.fold_ne leaf node node_tv + let%bind path = + let aux (i , _) = i = ind in + trace_option (simple_error "no leaf with given index") @@ + Append_tree.exists_path aux node_tv in + let lr_path = List.map (fun b -> if b then `Right else `Left) path in + let%bind (_ , lst) = + let aux = fun (ty , acc) cur -> + let%bind (a , b) = get_t_pair ty in + match cur with + | `Left -> ok (a , (a , `Left) :: acc) + | `Right -> ok (b , (b , `Right) :: acc) in + bind_fold_list aux (ty , []) lr_path in + ok lst let record_access_to_lr : type_value -> type_value AST.type_name_map -> string -> (type_value * (type_value * [`Left | `Right]) list) result = fun ty tym ind -> let tys = kv_list_of_map tym in @@ -133,7 +128,7 @@ and translate_instruction (env:Environment.t) (i:AST.instruction) : statement li | Access_tuple ind -> let%bind ty_lst = AST.Combinators.get_t_tuple prev in let%bind ty'_lst = bind_map_list translate_type ty_lst in - let%bind (_, path) = tuple_access_to_lr ty' ty'_lst ind in + let%bind path = tuple_access_to_lr ty' ty'_lst ind in let path' = List.map snd path in ok (List.nth ty_lst ind, path' @ acc) | Access_record prop -> @@ -243,17 +238,17 @@ and translate_annotated_expression (env:Environment.t) (ae:AST.annotated_express in Append_tree.fold_ne (translate_annotated_expression env) aux node | E_tuple_accessor (tpl, ind) -> + let%bind ty' = translate_type tpl.type_annotation in let%bind ty_lst = get_t_tuple tpl.type_annotation in let%bind ty'_lst = bind_map_list translate_type ty_lst in - let%bind ty' = translate_type tpl.type_annotation in - let%bind (_, path) = tuple_access_to_lr ty' ty'_lst ind in + let%bind path = tuple_access_to_lr ty' ty'_lst ind in let aux = fun pred (ty, lr) -> let c = match lr with | `Left -> "CAR" | `Right -> "CDR" in Combinators.Expression.make_tpl (E_constant (c, [pred]) , ty , env) in let%bind tpl' = translate_annotated_expression env tpl in - let expr = List.fold_left aux tpl' path in + let expr = List.fold_right' aux tpl' path in ok expr | E_record m -> let node = Append_tree.of_list @@ list_of_map m in diff --git a/src/ligo/typer.ml b/src/ligo/typer.ml index b7e63c290..c4e8bc124 100644 --- a/src/ligo/typer.ml +++ b/src/ligo/typer.ml @@ -326,7 +326,8 @@ and type_annotated_expression (e:environment) (ae:I.annotated_expression) : O.an generic_try (simple_error "bad tuple index") @@ (fun () -> List.nth tpl_tv index) in let%bind type_annotation = check tv in - ok O.{expression = O.E_tuple_accessor (prev, index) ; type_annotation} + let annotated_expression = O.{expression = E_tuple_accessor (prev, index) ; type_annotation} in + ok annotated_expression ) | Access_record property -> ( let%bind r_tv = get_t_record prev.type_annotation in @@ -468,8 +469,13 @@ and type_constant (name:string) (lst:O.type_value list) (tv_opt:O.type_value opt Assert.assert_true (arity = l) in let error = - let title () = "typing: unrecognized constant" in - let content () = name in + let title () = "typing: constant predicates all failed" in + let content () = + Format.asprintf "%s in %a" + name + PP_helpers.(list_sep Ast_typed.PP.type_value (const " , ")) + lst + in error title content in let rec aux = fun ts -> match ts with