From d8e44476baf1cc594fa7851c162dc2295181db52 Mon Sep 17 00:00:00 2001 From: Lesenechal Remi Date: Fri, 11 Oct 2019 17:41:26 +0200 Subject: [PATCH 01/30] First version for ForInt loops --- src/passes/2-simplify/pascaligo.ml | 37 +++++++++++++++++++++++++++++- src/test/contracts/loop.ligo | 8 +++---- src/test/integration_tests.ml | 9 ++++++-- 3 files changed, 47 insertions(+), 7 deletions(-) diff --git a/src/passes/2-simplify/pascaligo.ml b/src/passes/2-simplify/pascaligo.ml index d9fb6266d..08e88bdc7 100644 --- a/src/passes/2-simplify/pascaligo.ml +++ b/src/passes/2-simplify/pascaligo.ml @@ -667,7 +667,42 @@ and simpl_single_instruction : Raw.instruction -> (_ -> expression result) resul let%bind body = simpl_block l.block.value in let%bind body = body None in return_statement @@ e_loop cond body - | Loop (For (ForInt {region; _} | ForCollect {region ; _})) -> + | Loop (For (ForInt fi)) -> + (* cond part *) + let%bind _var = ok @@ e_variable fi.value.assign.value.name.value in + let%bind _value = simpl_expression fi.value.assign.value.expr in + let%bind _bound = simpl_expression fi.value.bound in + let%bind _comp = match fi.value.down with + | Some _ -> ok @@ e_annotation (e_constant "GE" [_var ; _bound]) t_bool + | None -> ok @@ e_annotation (e_constant "LE" [_var ; _bound]) t_bool + in + + (* body part *) + let%bind _body = simpl_block fi.value.block.value in + let%bind _body = _body None in + let%bind _step = match fi.value.step with + | Some (_,e) -> simpl_expression e + | None -> ok (e_int 1) in + let%bind _ctrl = match fi.value.down with + | Some _ -> + let%bind _addi = ok @@ e_constant "SUB" [ _var ; _step ] in + ok @@ e_assign fi.value.assign.value.name.value [] _addi + | None -> + let%bind _subi = ok @@ e_constant "ADD" [ _var ; _step ] in + ok @@ e_assign fi.value.assign.value.name.value [] _subi + in + let rec add_to_seq expr = match expr.expression with + | E_sequence (_,a) -> add_to_seq a + | _ -> e_sequence _body _ctrl in + let%bind _body' = ok @@ add_to_seq _body in + + let%bind _loop = ok @@ e_loop _comp _body' in + + let _ = Format.printf " -> %a\n" Ast_simplified.PP.expression _body' in + + return_statement @@ + e_let_in (fi.value.assign.value.name.value, Some t_int) _value _loop + | Loop (For (ForCollect {region ; _})) -> fail @@ unsupported_for_loops region | Cond c -> ( let (c , loc) = r_split c in diff --git a/src/test/contracts/loop.ligo b/src/test/contracts/loop.ligo index 03cc751a7..8fc4cd254 100644 --- a/src/test/contracts/loop.ligo +++ b/src/test/contracts/loop.ligo @@ -16,12 +16,12 @@ function while_sum (var n : nat) : nat is block { } } with r -(* function for_sum (var n : nat) : nat is block { - for i := 1 to 100 +function for_sum (var n : nat) : nat is block { + for i := 1 to 100 step 1 begin - n := n + 1; + n := n + 1n ; end } - with n *) + with n function dummy (const n : nat) : nat is block { while (False) block { skip } diff --git a/src/test/integration_tests.ml b/src/test/integration_tests.ml index ed60a0966..0644f1189 100644 --- a/src/test/integration_tests.ml +++ b/src/test/integration_tests.ml @@ -658,13 +658,18 @@ let loop () : unit result = let make_input = e_nat in let make_expected = fun n -> e_nat (n * (n + 1) / 2) in expect_eq_n_pos_mid program "while_sum" make_input make_expected +<<<<<<< HEAD in(* For loop is currently unsupported let%bind () = +======= + in + let%bind () = +>>>>>>> First version for ForInt loops let make_input = e_nat in - let make_expected = fun n -> e_nat (n * (n + 1) / 2) in + let make_expected = fun n -> e_nat (n + 100) in expect_eq_n_pos_mid program "for_sum" make_input make_expected - in *) + in ok () (* Don't know how to assert parse error happens in this test framework From b7961fc8ec17e1e54876c5c780d640ae4a01a49c Mon Sep 17 00:00:00 2001 From: Lesenechal Remi Date: Fri, 11 Oct 2019 17:47:04 +0200 Subject: [PATCH 02/30] cleaning --- src/passes/2-simplify/pascaligo.ml | 35 ++++++++++++++---------------- 1 file changed, 16 insertions(+), 19 deletions(-) diff --git a/src/passes/2-simplify/pascaligo.ml b/src/passes/2-simplify/pascaligo.ml index 08e88bdc7..3a438f68b 100644 --- a/src/passes/2-simplify/pascaligo.ml +++ b/src/passes/2-simplify/pascaligo.ml @@ -669,39 +669,36 @@ and simpl_single_instruction : Raw.instruction -> (_ -> expression result) resul return_statement @@ e_loop cond body | Loop (For (ForInt fi)) -> (* cond part *) - let%bind _var = ok @@ e_variable fi.value.assign.value.name.value in - let%bind _value = simpl_expression fi.value.assign.value.expr in - let%bind _bound = simpl_expression fi.value.bound in - let%bind _comp = match fi.value.down with - | Some _ -> ok @@ e_annotation (e_constant "GE" [_var ; _bound]) t_bool - | None -> ok @@ e_annotation (e_constant "LE" [_var ; _bound]) t_bool + let%bind var = ok @@ e_variable fi.value.assign.value.name.value in + let%bind value = simpl_expression fi.value.assign.value.expr in + let%bind bound = simpl_expression fi.value.bound in + let%bind comp = match fi.value.down with + | Some _ -> ok @@ e_annotation (e_constant "GE" [var ; bound]) t_bool + | None -> ok @@ e_annotation (e_constant "LE" [var ; bound]) t_bool in (* body part *) - let%bind _body = simpl_block fi.value.block.value in - let%bind _body = _body None in - let%bind _step = match fi.value.step with + let%bind body = simpl_block fi.value.block.value in + let%bind body = body None in + let%bind step = match fi.value.step with | Some (_,e) -> simpl_expression e | None -> ok (e_int 1) in - let%bind _ctrl = match fi.value.down with + let%bind ctrl = match fi.value.down with | Some _ -> - let%bind _addi = ok @@ e_constant "SUB" [ _var ; _step ] in + let%bind _addi = ok @@ e_constant "SUB" [ var ; step ] in ok @@ e_assign fi.value.assign.value.name.value [] _addi | None -> - let%bind _subi = ok @@ e_constant "ADD" [ _var ; _step ] in + let%bind _subi = ok @@ e_constant "ADD" [ var ; step ] in ok @@ e_assign fi.value.assign.value.name.value [] _subi in let rec add_to_seq expr = match expr.expression with | E_sequence (_,a) -> add_to_seq a - | _ -> e_sequence _body _ctrl in - let%bind _body' = ok @@ add_to_seq _body in - - let%bind _loop = ok @@ e_loop _comp _body' in - - let _ = Format.printf " -> %a\n" Ast_simplified.PP.expression _body' in + | _ -> e_sequence body ctrl in + let%bind body' = ok @@ add_to_seq body in + let%bind loop = ok @@ e_loop comp body' in return_statement @@ - e_let_in (fi.value.assign.value.name.value, Some t_int) _value _loop + e_let_in (fi.value.assign.value.name.value, Some t_int) value loop | Loop (For (ForCollect {region ; _})) -> fail @@ unsupported_for_loops region | Cond c -> ( From 3058a57c626fb90584fd45880220f396b3a1cdb5 Mon Sep 17 00:00:00 2001 From: Lesenechal Remi Date: Fri, 11 Oct 2019 18:31:04 +0200 Subject: [PATCH 03/30] cleaning and better tests --- src/passes/2-simplify/pascaligo.ml | 64 +++++++++++++++--------------- src/test/contracts/loop.ligo | 32 ++++++++++++--- src/test/integration_tests.ml | 14 ++++++- 3 files changed, 72 insertions(+), 38 deletions(-) diff --git a/src/passes/2-simplify/pascaligo.ml b/src/passes/2-simplify/pascaligo.ml index 3a438f68b..f7b5b4211 100644 --- a/src/passes/2-simplify/pascaligo.ml +++ b/src/passes/2-simplify/pascaligo.ml @@ -668,37 +668,9 @@ and simpl_single_instruction : Raw.instruction -> (_ -> expression result) resul let%bind body = body None in return_statement @@ e_loop cond body | Loop (For (ForInt fi)) -> - (* cond part *) - let%bind var = ok @@ e_variable fi.value.assign.value.name.value in - let%bind value = simpl_expression fi.value.assign.value.expr in - let%bind bound = simpl_expression fi.value.bound in - let%bind comp = match fi.value.down with - | Some _ -> ok @@ e_annotation (e_constant "GE" [var ; bound]) t_bool - | None -> ok @@ e_annotation (e_constant "LE" [var ; bound]) t_bool - in - - (* body part *) - let%bind body = simpl_block fi.value.block.value in - let%bind body = body None in - let%bind step = match fi.value.step with - | Some (_,e) -> simpl_expression e - | None -> ok (e_int 1) in - let%bind ctrl = match fi.value.down with - | Some _ -> - let%bind _addi = ok @@ e_constant "SUB" [ var ; step ] in - ok @@ e_assign fi.value.assign.value.name.value [] _addi - | None -> - let%bind _subi = ok @@ e_constant "ADD" [ var ; step ] in - ok @@ e_assign fi.value.assign.value.name.value [] _subi - in - let rec add_to_seq expr = match expr.expression with - | E_sequence (_,a) -> add_to_seq a - | _ -> e_sequence body ctrl in - let%bind body' = ok @@ add_to_seq body in - let%bind loop = ok @@ e_loop comp body' in - - return_statement @@ - e_let_in (fi.value.assign.value.name.value, Some t_int) value loop + let%bind loop = simpl_for_int fi.value in + let%bind loop = loop None in + return_statement @@ loop | Loop (For (ForCollect {region ; _})) -> fail @@ unsupported_for_loops region | Cond c -> ( @@ -993,5 +965,35 @@ and simpl_statements : Raw.statements -> (_ -> expression result) result = and simpl_block : Raw.block -> (_ -> expression result) result = fun t -> simpl_statements t.statements +and simpl_for_int : Raw.for_int -> (_ -> expression result) result = fun fi -> + (* cond part *) + let%bind var = ok @@ e_variable fi.assign.value.name.value in + let%bind value = simpl_expression fi.assign.value.expr in + let%bind bound = simpl_expression fi.bound in + let%bind comp = match fi.down with + | Some _ -> ok @@ e_annotation (e_constant "GE" [var ; bound]) t_bool + | None -> ok @@ e_annotation (e_constant "LE" [var ; bound]) t_bool + in + (* body part *) + let%bind body = simpl_block fi.block.value in + let%bind body = body None in + let%bind step = match fi.step with + | Some (_,e) -> simpl_expression e + | None -> ok (e_int 1) in + let%bind ctrl = match fi.down with + | Some _ -> + let%bind _addi = ok @@ e_constant "SUB" [ var ; step ] in + ok @@ e_assign fi.assign.value.name.value [] _addi + | None -> + let%bind _subi = ok @@ e_constant "ADD" [ var ; step ] in + ok @@ e_assign fi.assign.value.name.value [] _subi + in + let rec add_to_seq expr = match expr.expression with + | E_sequence (_,a) -> add_to_seq a + | _ -> e_sequence body ctrl in + let%bind body' = ok @@ add_to_seq body in + let%bind loop = ok @@ e_loop comp body' in + return_statement @@ e_let_in (fi.assign.value.name.value, Some t_int) value loop + let simpl_program : Raw.ast -> program result = fun t -> bind_list @@ List.map simpl_declaration @@ nseq_to_list t.decl diff --git a/src/test/contracts/loop.ligo b/src/test/contracts/loop.ligo index 8fc4cd254..f3f0db33c 100644 --- a/src/test/contracts/loop.ligo +++ b/src/test/contracts/loop.ligo @@ -16,12 +16,34 @@ function while_sum (var n : nat) : nat is block { } } with r -function for_sum (var n : nat) : nat is block { - for i := 1 to 100 step 1 +function for_sum_up (var n : nat) : int is block { + var acc : int := 0 ; + for i := 1 to int(n) step 1 begin - n := n + 1n ; - end } - with n + acc := acc + i ; + end +} with acc + +function for_sum_down (var n : nat) : int is block { + var acc : int := 0 ; + for i := int(n) down to 1 step 1 + begin + acc := acc + i ; + end +} with acc + +function for_sum_step (var n : nat) : int is block { + var acc : int := 0 ; + var mystep : int := 2 ; + for i := 1 to int(n) step mystep + begin + acc := acc + i ; + end; + for i := 0 to int(n) step mystep + begin + acc := acc + i ; + end; +} with acc function dummy (const n : nat) : nat is block { while (False) block { skip } diff --git a/src/test/integration_tests.ml b/src/test/integration_tests.ml index 0644f1189..d28f628b4 100644 --- a/src/test/integration_tests.ml +++ b/src/test/integration_tests.ml @@ -667,8 +667,18 @@ let loop () : unit result = let%bind () = >>>>>>> First version for ForInt loops let make_input = e_nat in - let make_expected = fun n -> e_nat (n + 100) in - expect_eq_n_pos_mid program "for_sum" make_input make_expected + let make_expected = fun n -> e_int (n * (n + 1) / 2) in + expect_eq_n_pos_mid program "for_sum_up" make_input make_expected + in + let%bind () = + let make_input = e_nat in + let make_expected = fun n -> e_int (n * (n + 1) / 2) in + expect_eq_n_pos_mid program "for_sum_down" make_input make_expected + in + let%bind () = + let make_input = e_nat in + let make_expected = fun n -> e_int (n * (n + 1) / 2) in + expect_eq_n_pos_mid program "for_sum_step" make_input make_expected in ok () From 1d3d57c7c57c37ff7283d762fab297a9b1936473 Mon Sep 17 00:00:00 2001 From: Lesenechal Remi Date: Tue, 15 Oct 2019 13:14:00 +0200 Subject: [PATCH 04/30] not complete for collect tryout --- src/passes/2-simplify/pascaligo.ml | 23 +++++++++++++++++++---- src/test/contracts/loop.ligo | 8 ++++++++ src/test/integration_tests.ml | 5 +++++ 3 files changed, 32 insertions(+), 4 deletions(-) diff --git a/src/passes/2-simplify/pascaligo.ml b/src/passes/2-simplify/pascaligo.ml index f7b5b4211..d1ffb5672 100644 --- a/src/passes/2-simplify/pascaligo.ml +++ b/src/passes/2-simplify/pascaligo.ml @@ -68,7 +68,7 @@ module Errors = struct ] in error ~data title message - let unsupported_for_loops region = + (* let unsupported_for_loops region = let title () = "bounded iterators" in let message () = Format.asprintf "only simple for loops are supported for now" in @@ -76,7 +76,7 @@ module Errors = struct ("loop_loc", fun () -> Format.asprintf "%a" Location.pp_lift @@ region) ] in - error ~data title message + error ~data title message *) let unsupported_non_var_pattern p = let title () = "pattern is not a variable" in @@ -671,8 +671,10 @@ and simpl_single_instruction : Raw.instruction -> (_ -> expression result) resul let%bind loop = simpl_for_int fi.value in let%bind loop = loop None in return_statement @@ loop - | Loop (For (ForCollect {region ; _})) -> - fail @@ unsupported_for_loops region + | Loop (For (ForCollect fc)) -> + let%bind loop = simpl_for_collect fc.value in + let%bind loop = loop None in + return_statement @@ loop | Cond c -> ( let (c , loc) = r_split c in let%bind expr = simpl_expression c.test in @@ -995,5 +997,18 @@ and simpl_for_int : Raw.for_int -> (_ -> expression result) result = fun fi -> let%bind loop = ok @@ e_loop comp body' in return_statement @@ e_let_in (fi.assign.value.name.value, Some t_int) value loop +and simpl_for_collect : Raw.for_collect -> (_ -> expression result) result = fun fc -> + let%bind col = simpl_expression fc.expr in + + let%bind body = simpl_block fc.block.value in + let%bind body = body None in + + let%bind invar = ok @@ e_variable fc.var.value in + let%bind letin = ok @@ e_let_in (fc.var.value, None) invar body in + let%bind lambda = ok @@ e_lambda fc.var.value None (Some t_unit) letin in + (* let%bind lambda = ok @@ e_lambda fc.var.value None (Some t_unit) body in *) + + return_statement @@ e_constant "SET_ITER" [col ; lambda] + let simpl_program : Raw.ast -> program result = fun t -> bind_list @@ List.map simpl_declaration @@ nseq_to_list t.decl diff --git a/src/test/contracts/loop.ligo b/src/test/contracts/loop.ligo index f3f0db33c..27af27a72 100644 --- a/src/test/contracts/loop.ligo +++ b/src/test/contracts/loop.ligo @@ -45,6 +45,14 @@ function for_sum_step (var n : nat) : int is block { end; } with acc +function for_collection (var n : set(int)) : int is block { + var acc : int := 0; + for i in n + begin + acc := acc + i ; + end; +} with acc + function dummy (const n : nat) : nat is block { while (False) block { skip } } with n diff --git a/src/test/integration_tests.ml b/src/test/integration_tests.ml index d28f628b4..f180ff7d5 100644 --- a/src/test/integration_tests.ml +++ b/src/test/integration_tests.ml @@ -680,6 +680,11 @@ let loop () : unit result = let make_expected = fun n -> e_int (n * (n + 1) / 2) in expect_eq_n_pos_mid program "for_sum_step" make_input make_expected in + let%bind () = + let make_input = fun _n -> e_set [e_int 1; e_int 2] in + let make_expected = fun _n -> e_int 3 in + expect_eq_n_pos_mid program "for_sum_step" make_input make_expected + in ok () (* Don't know how to assert parse error happens in this test framework From 536b5648c8a618fb426419584bf841bd42cfff62 Mon Sep 17 00:00:00 2001 From: Lesenechal Remi Date: Tue, 15 Oct 2019 13:56:21 +0200 Subject: [PATCH 05/30] some cleaning --- src/passes/2-simplify/pascaligo.ml | 31 ++++++++++++++---------------- 1 file changed, 14 insertions(+), 17 deletions(-) diff --git a/src/passes/2-simplify/pascaligo.ml b/src/passes/2-simplify/pascaligo.ml index d1ffb5672..148e8d314 100644 --- a/src/passes/2-simplify/pascaligo.ml +++ b/src/passes/2-simplify/pascaligo.ml @@ -969,12 +969,12 @@ and simpl_block : Raw.block -> (_ -> expression result) result = fun t -> and simpl_for_int : Raw.for_int -> (_ -> expression result) result = fun fi -> (* cond part *) - let%bind var = ok @@ e_variable fi.assign.value.name.value in + let var = e_variable fi.assign.value.name.value in let%bind value = simpl_expression fi.assign.value.expr in let%bind bound = simpl_expression fi.bound in - let%bind comp = match fi.down with - | Some _ -> ok @@ e_annotation (e_constant "GE" [var ; bound]) t_bool - | None -> ok @@ e_annotation (e_constant "LE" [var ; bound]) t_bool + let comp = match fi.down with + | Some _ -> e_annotation (e_constant "GE" [var ; bound]) t_bool + | None -> e_annotation (e_constant "LE" [var ; bound]) t_bool in (* body part *) let%bind body = simpl_block fi.block.value in @@ -982,32 +982,29 @@ and simpl_for_int : Raw.for_int -> (_ -> expression result) result = fun fi -> let%bind step = match fi.step with | Some (_,e) -> simpl_expression e | None -> ok (e_int 1) in - let%bind ctrl = match fi.down with + let ctrl = match fi.down with | Some _ -> - let%bind _addi = ok @@ e_constant "SUB" [ var ; step ] in - ok @@ e_assign fi.assign.value.name.value [] _addi + let _addi = e_constant "SUB" [ var ; step ] in + e_assign fi.assign.value.name.value [] _addi | None -> - let%bind _subi = ok @@ e_constant "ADD" [ var ; step ] in - ok @@ e_assign fi.assign.value.name.value [] _subi + let _subi = e_constant "ADD" [ var ; step ] in + e_assign fi.assign.value.name.value [] _subi in let rec add_to_seq expr = match expr.expression with | E_sequence (_,a) -> add_to_seq a | _ -> e_sequence body ctrl in - let%bind body' = ok @@ add_to_seq body in - let%bind loop = ok @@ e_loop comp body' in + let body' = add_to_seq body in + let loop = e_loop comp body' in return_statement @@ e_let_in (fi.assign.value.name.value, Some t_int) value loop and simpl_for_collect : Raw.for_collect -> (_ -> expression result) result = fun fc -> let%bind col = simpl_expression fc.expr in - let%bind body = simpl_block fc.block.value in let%bind body = body None in - - let%bind invar = ok @@ e_variable fc.var.value in - let%bind letin = ok @@ e_let_in (fc.var.value, None) invar body in - let%bind lambda = ok @@ e_lambda fc.var.value None (Some t_unit) letin in + let invar = e_variable fc.var.value in + let letin = e_let_in (fc.var.value, None) invar body in + let lambda = e_lambda fc.var.value None (Some t_unit) letin in (* let%bind lambda = ok @@ e_lambda fc.var.value None (Some t_unit) body in *) - return_statement @@ e_constant "SET_ITER" [col ; lambda] let simpl_program : Raw.ast -> program result = fun t -> From 730c130fb3bdca48d79e9dbd482ef54bf0df4f45 Mon Sep 17 00:00:00 2001 From: Lesenechal Remi Date: Tue, 22 Oct 2019 12:12:19 +0200 Subject: [PATCH 06/30] merge step and down reemoval WIP WIP --- src/passes/2-simplify/pascaligo.ml | 52 +++++++++++++++------------ src/test/contracts/loop.ligo | 58 +++++++++++++++--------------- src/test/integration_tests.ml | 17 +-------- 3 files changed, 60 insertions(+), 67 deletions(-) diff --git a/src/passes/2-simplify/pascaligo.ml b/src/passes/2-simplify/pascaligo.ml index 148e8d314..d7443741a 100644 --- a/src/passes/2-simplify/pascaligo.ml +++ b/src/passes/2-simplify/pascaligo.ml @@ -972,24 +972,14 @@ and simpl_for_int : Raw.for_int -> (_ -> expression result) result = fun fi -> let var = e_variable fi.assign.value.name.value in let%bind value = simpl_expression fi.assign.value.expr in let%bind bound = simpl_expression fi.bound in - let comp = match fi.down with - | Some _ -> e_annotation (e_constant "GE" [var ; bound]) t_bool - | None -> e_annotation (e_constant "LE" [var ; bound]) t_bool + let comp = e_annotation (e_constant "LE" [var ; bound]) t_bool in (* body part *) let%bind body = simpl_block fi.block.value in let%bind body = body None in - let%bind step = match fi.step with - | Some (_,e) -> simpl_expression e - | None -> ok (e_int 1) in - let ctrl = match fi.down with - | Some _ -> - let _addi = e_constant "SUB" [ var ; step ] in - e_assign fi.assign.value.name.value [] _addi - | None -> - let _subi = e_constant "ADD" [ var ; step ] in - e_assign fi.assign.value.name.value [] _subi - in + let step = e_int 1 in + let ctrl = e_assign + fi.assign.value.name.value [] (e_constant "ADD" [ var ; step ]) in let rec add_to_seq expr = match expr.expression with | E_sequence (_,a) -> add_to_seq a | _ -> e_sequence body ctrl in @@ -998,14 +988,30 @@ and simpl_for_int : Raw.for_int -> (_ -> expression result) result = fun fi -> return_statement @@ e_let_in (fi.assign.value.name.value, Some t_int) value loop and simpl_for_collect : Raw.for_collect -> (_ -> expression result) result = fun fc -> - let%bind col = simpl_expression fc.expr in - let%bind body = simpl_block fc.block.value in - let%bind body = body None in - let invar = e_variable fc.var.value in - let letin = e_let_in (fc.var.value, None) invar body in - let lambda = e_lambda fc.var.value None (Some t_unit) letin in - (* let%bind lambda = ok @@ e_lambda fc.var.value None (Some t_unit) body in *) - return_statement @@ e_constant "SET_ITER" [col ; lambda] + let statements = npseq_to_list fc.block.value.statements in + (* building initial record *) + let aux (el : Raw.statement) : Raw.instruction option = match el with + | Raw.Instr (Assign _ as i) -> Some i + | _ -> None in + let assign_instrs = List.filter_map aux statements in + let%bind assign_instrs' = bind_map_list + (fun el -> + let%bind assign' = simpl_instruction el in + let%bind assign' = assign' None in + ok @@ assign') + assign_instrs in + let aux prev ass_exp = + match ass_exp.expression with + | E_variable name -> SMap.add name ass_exp prev + | _ -> prev in + let init_record = e_record (List.fold_left aux SMap.empty assign_instrs') in + (*later , init_record will be placed in a let_in *) + + (* replace assignments to variable to assignments to record *) + + + + return_statement @@ init_record let simpl_program : Raw.ast -> program result = fun t -> - bind_list @@ List.map simpl_declaration @@ nseq_to_list t.decl + bind_list @@ List.map simpl_declaration @@ nseq_to_list t.decl \ No newline at end of file diff --git a/src/test/contracts/loop.ligo b/src/test/contracts/loop.ligo index 27af27a72..2b7447942 100644 --- a/src/test/contracts/loop.ligo +++ b/src/test/contracts/loop.ligo @@ -16,42 +16,44 @@ function while_sum (var n : nat) : nat is block { } } with r -function for_sum_up (var n : nat) : int is block { +function for_sum (var n : nat) : int is block { var acc : int := 0 ; - for i := 1 to int(n) step 1 + for i := 1 to int(n) begin acc := acc + i ; end } with acc -function for_sum_down (var n : nat) : int is block { - var acc : int := 0 ; - for i := int(n) down to 1 step 1 - begin - acc := acc + i ; - end -} with acc -function for_sum_step (var n : nat) : int is block { - var acc : int := 0 ; - var mystep : int := 2 ; - for i := 1 to int(n) step mystep - begin - acc := acc + i ; - end; - for i := 0 to int(n) step mystep - begin - acc := acc + i ; - end; -} with acc +function lamby (var accu : (record st : string ; acc : int end) ; var i : int ) + : (record st : string ; acc : int end) is block { + accu.acc := accu.acc + i ; + accu.st := accu.st ^ "to" ; +} with accu -function for_collection (var n : set(int)) : int is block { - var acc : int := 0; - for i in n - begin - acc := acc + i ; - end; -} with acc +function for_collection (var nee : unit; var nuu : unit) : (int * string) is block { + var acc : int := 0 ; + var st : string := "to" ; + var mylist : list(int) := list 1 ; 1 ; 1 end ; + + var init_record : (record st : string; acc : int end ) := + record st = st; acc = acc; end; + var folded_record : (record st : string; acc : int end ) := + list_fold(mylist , init_record , lamby) ; +} with (folded_record.acc , folded_record.st) + +// function for_collection_ (var nee : unit; var nuu : unit) : (int * string) is block { +// var acc : int := 0 ; +// var st : string := "to" ; +// var mylist : list(int) := list 1 ; 1 ; 1 end ; + +// for x : int in list mylist +// begin +// acc := acc + x ; +// st := st^"to" ; +// end + +// } with acc function dummy (const n : nat) : nat is block { while (False) block { skip } diff --git a/src/test/integration_tests.ml b/src/test/integration_tests.ml index f180ff7d5..0088b0e31 100644 --- a/src/test/integration_tests.ml +++ b/src/test/integration_tests.ml @@ -668,22 +668,7 @@ let loop () : unit result = >>>>>>> First version for ForInt loops let make_input = e_nat in let make_expected = fun n -> e_int (n * (n + 1) / 2) in - expect_eq_n_pos_mid program "for_sum_up" make_input make_expected - in - let%bind () = - let make_input = e_nat in - let make_expected = fun n -> e_int (n * (n + 1) / 2) in - expect_eq_n_pos_mid program "for_sum_down" make_input make_expected - in - let%bind () = - let make_input = e_nat in - let make_expected = fun n -> e_int (n * (n + 1) / 2) in - expect_eq_n_pos_mid program "for_sum_step" make_input make_expected - in - let%bind () = - let make_input = fun _n -> e_set [e_int 1; e_int 2] in - let make_expected = fun _n -> e_int 3 in - expect_eq_n_pos_mid program "for_sum_step" make_input make_expected + expect_eq_n_pos_mid program "for_sum" make_input make_expected in ok () From 79de96136d3e24690061afc5feeef58ac7826d1b Mon Sep 17 00:00:00 2001 From: Lesenechal Remi Date: Sat, 26 Oct 2019 14:18:06 +0200 Subject: [PATCH 07/30] Collection for translation without type annotation on record --- src/passes/2-simplify/dune | 1 + src/passes/2-simplify/pascaligo.ml | 52 +++++++++++++++++-- .../self_ast_simplified.ml | 2 + src/test/contracts/loop.ligo | 27 ++++++---- 4 files changed, 68 insertions(+), 14 deletions(-) diff --git a/src/passes/2-simplify/dune b/src/passes/2-simplify/dune index 9649d13dc..e27b5139d 100644 --- a/src/passes/2-simplify/dune +++ b/src/passes/2-simplify/dune @@ -6,6 +6,7 @@ tezos-utils parser ast_simplified + self_ast_simplified operators) (modules ligodity pascaligo simplify) (preprocess diff --git a/src/passes/2-simplify/pascaligo.ml b/src/passes/2-simplify/pascaligo.ml index d7443741a..321c87cf5 100644 --- a/src/passes/2-simplify/pascaligo.ml +++ b/src/passes/2-simplify/pascaligo.ml @@ -1002,16 +1002,60 @@ and simpl_for_collect : Raw.for_collect -> (_ -> expression result) result = fun assign_instrs in let aux prev ass_exp = match ass_exp.expression with - | E_variable name -> SMap.add name ass_exp prev + | E_assign ( name , _ , _ ) -> + let expr' = e_variable name in + SMap.add name expr' prev | _ -> prev in + let captured_list = List.filter_map + (fun ass_exp -> match ass_exp.expression with + | E_assign ( name, _ , _ ) -> Some name + | _ -> None ) + assign_instrs' in let init_record = e_record (List.fold_left aux SMap.empty assign_instrs') in - (*later , init_record will be placed in a let_in *) - (* replace assignments to variable to assignments to record *) + (* replace assignments to X assignments to record *) + let%bind block' = simpl_block fc.block.value in + let%bind block' = block' None in + let replace_with_record exp = + match exp.expression with + | E_assign ( name , path , expr ) -> + let path' = ( match path with + | [] -> [Access_record name] + (* This will fail for deep tuple access, see LIGO-131 *) + | _ -> ((Access_record name)::path) ) in + ok @@ e_assign "_COMPILER_fold_record" path' expr + | E_variable name -> + if (List.mem name captured_list) then + ok @@ e_accessor (e_variable "_COMPILER_fold_record") [Access_record name] + else ok @@ exp + | _ -> ok @@ exp in + let%bind block'' = Self_ast_simplified.map_expression replace_with_record block' in + (* build the lambda*) + (* let%bind (elt_type' : type_expression) = simpl_type_expression fc.elt_type in *) + (* let%bind (record_type : type_expression) = ... in *) + (* Here it's not possible to know the type of the variable captures in the record ..*) + let lambda = e_lambda "_COMPILER_for_collect_lambda" None None block'' in + let%bind collect = simpl_expression fc.expr in + let fold = e_constant "LIST_FOLD" [collect ; init_record ; lambda] in + let final = e_let_in ("_COMPILER_init_record", None) init_record + @@ (e_let_in ("_COMPILER_folded_record", None) fold (e_skip ())) in - return_statement @@ init_record + (* build the sequence of assigments back to the original variables *) + let aux (prev : expression) (captured_varname : string) = + let access = e_accessor (e_variable "_COMPILER_folded_record") + [Access_record captured_varname] in + let assign = e_assign captured_varname [] access in + e_sequence prev assign in + + let ( final_sequence : expression ) = List.fold_left aux final captured_list in + + return_statement @@ final_sequence + +(** NODE TO AVOID THE DIRT: + have a E_unsimplified 'a which is then transformed in a self pass ?? +**) let simpl_program : Raw.ast -> program result = fun t -> bind_list @@ List.map simpl_declaration @@ nseq_to_list t.decl \ No newline at end of file diff --git a/src/passes/3-self_ast_simplified/self_ast_simplified.ml b/src/passes/3-self_ast_simplified/self_ast_simplified.ml index aa18b4a8c..b73113cdb 100644 --- a/src/passes/3-self_ast_simplified/self_ast_simplified.ml +++ b/src/passes/3-self_ast_simplified/self_ast_simplified.ml @@ -21,3 +21,5 @@ let all_program = let all_expression = let all_p = List.map Helpers.map_expression all in bind_chain all_p + +let map_expression = Helpers.map_expression diff --git a/src/test/contracts/loop.ligo b/src/test/contracts/loop.ligo index 2b7447942..6e5e709a8 100644 --- a/src/test/contracts/loop.ligo +++ b/src/test/contracts/loop.ligo @@ -40,20 +40,27 @@ function for_collection (var nee : unit; var nuu : unit) : (int * string) is blo record st = st; acc = acc; end; var folded_record : (record st : string; acc : int end ) := list_fold(mylist , init_record , lamby) ; + skip ; + st := folded_record.st ; + acc := folded_record.acc ; + } with (folded_record.acc , folded_record.st) -// function for_collection_ (var nee : unit; var nuu : unit) : (int * string) is block { -// var acc : int := 0 ; -// var st : string := "to" ; -// var mylist : list(int) := list 1 ; 1 ; 1 end ; +function for_collection_ (var nee : unit; var nuu : unit) : (int * string) is block { + var acc : int := 0 ; + var st : string := "to" ; + var toto : (string * string) := ("foo","bar") ; -// for x : int in list mylist -// begin -// acc := acc + x ; -// st := st^"to" ; -// end + var mylist : list(int) := list 1 ; 1 ; 1 end ; -// } with acc + for x : int in list mylist + begin + toto.1 := "r"; + acc := acc + x ; + st := st^"to" ; + end + +} with acc function dummy (const n : nat) : nat is block { while (False) block { skip } From db79b6b9da05e23d11585f075fa3479ead452b67 Mon Sep 17 00:00:00 2001 From: Lesenechal Remi Date: Sat, 26 Oct 2019 14:27:29 +0200 Subject: [PATCH 08/30] select op_name from collection key word --- src/passes/2-simplify/pascaligo.ml | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/src/passes/2-simplify/pascaligo.ml b/src/passes/2-simplify/pascaligo.ml index 321c87cf5..4aa92282e 100644 --- a/src/passes/2-simplify/pascaligo.ml +++ b/src/passes/2-simplify/pascaligo.ml @@ -1037,7 +1037,11 @@ and simpl_for_collect : Raw.for_collect -> (_ -> expression result) result = fun (* Here it's not possible to know the type of the variable captures in the record ..*) let lambda = e_lambda "_COMPILER_for_collect_lambda" None None block'' in let%bind collect = simpl_expression fc.expr in - let fold = e_constant "LIST_FOLD" [collect ; init_record ; lambda] in + let op_name = match fc.collection with + | Map _ -> "MAP_FOLD" + | Set _ -> "SET_FOLD" + | List _ -> "LIST_FOLD" in + let fold = e_constant op_name [collect ; init_record ; lambda] in let final = e_let_in ("_COMPILER_init_record", None) init_record @@ (e_let_in ("_COMPILER_folded_record", None) fold (e_skip ())) in From 70502f62cbd3773046243d17e3b610444e3a69c8 Mon Sep 17 00:00:00 2001 From: Lesenechal Remi Date: Sat, 26 Oct 2019 22:07:42 +0200 Subject: [PATCH 09/30] fix the way lambda arguments are accessed --- src/passes/2-simplify/pascaligo.ml | 41 ++++++++++++++++++------------ 1 file changed, 25 insertions(+), 16 deletions(-) diff --git a/src/passes/2-simplify/pascaligo.ml b/src/passes/2-simplify/pascaligo.ml index 4aa92282e..c785ee780 100644 --- a/src/passes/2-simplify/pascaligo.ml +++ b/src/passes/2-simplify/pascaligo.ml @@ -1013,38 +1013,41 @@ and simpl_for_collect : Raw.for_collect -> (_ -> expression result) result = fun assign_instrs' in let init_record = e_record (List.fold_left aux SMap.empty assign_instrs') in - (* replace assignments to X assignments to record *) + (* replace assignments to X assignments to record in the for_collect + block which will become the body of the lambda *) let%bind block' = simpl_block fc.block.value in let%bind block' = block' None in - let replace_with_record exp = + let replace_with_record exp = match exp.expression with | E_assign ( name , path , expr ) -> let path' = ( match path with - | [] -> [Access_record name] + | [] -> [Access_tuple 0 ; Access_record name ] @ path (* This will fail for deep tuple access, see LIGO-131 *) - | _ -> ((Access_record name)::path) ) in - ok @@ e_assign "_COMPILER_fold_record" path' expr + | _ -> [Access_tuple 0 ; Access_record name ] @ path ) in + ok @@ e_assign "arguments" path' expr | E_variable name -> - if (List.mem name captured_list) then - ok @@ e_accessor (e_variable "_COMPILER_fold_record") [Access_record name] + if (name = fc.var.value ) then + ok @@ e_accessor (e_variable "arguments") [Access_tuple 1] + else if (List.mem name captured_list) then + let acc_arg = e_accessor (e_variable "arguments") [Access_tuple 0] in + ok @@ e_accessor (acc_arg) [Access_record name] else ok @@ exp | _ -> ok @@ exp in let%bind block'' = Self_ast_simplified.map_expression replace_with_record block' in + let rec add_return expr = match expr.expression with + | E_sequence (a,b) -> e_sequence a (add_return b) + | _ -> e_sequence expr (e_accessor (e_variable "arguments") [Access_tuple 0]) in + let block_with_return = add_return block'' in (* build the lambda*) - (* let%bind (elt_type' : type_expression) = simpl_type_expression fc.elt_type in *) - (* let%bind (record_type : type_expression) = ... in *) - (* Here it's not possible to know the type of the variable captures in the record ..*) - let lambda = e_lambda "_COMPILER_for_collect_lambda" None None block'' in + let lambda = e_lambda "_COMPILER_for_collect_lambda" None None block_with_return in let%bind collect = simpl_expression fc.expr in let op_name = match fc.collection with | Map _ -> "MAP_FOLD" | Set _ -> "SET_FOLD" | List _ -> "LIST_FOLD" in let fold = e_constant op_name [collect ; init_record ; lambda] in - - let final = e_let_in ("_COMPILER_init_record", None) init_record - @@ (e_let_in ("_COMPILER_folded_record", None) fold (e_skip ())) in + let folded_record = e_let_in ("_COMPILER_folded_record", None) fold (e_skip ()) in (* build the sequence of assigments back to the original variables *) let aux (prev : expression) (captured_varname : string) = @@ -1053,12 +1056,18 @@ and simpl_for_collect : Raw.for_collect -> (_ -> expression result) result = fun let assign = e_assign captured_varname [] access in e_sequence prev assign in - let ( final_sequence : expression ) = List.fold_left aux final captured_list in + let ( final_sequence : expression ) = List.fold_left aux folded_record captured_list in + let _ = Format.printf "___ GEN ____\n %a \n" Ast_simplified.PP.expression final_sequence in return_statement @@ final_sequence (** NODE TO AVOID THE DIRT: - have a E_unsimplified 'a which is then transformed in a self pass ?? + - have a E_unsimplified 'a which is then transformed in a self pass ?? + - need to forbid that ? + for i in somelist + begin + i := .. + end **) let simpl_program : Raw.ast -> program result = fun t -> From 91d92e048d427c3d5ba002ee8758455415f6ce8f Mon Sep 17 00:00:00 2001 From: Lesenechal Remi Date: Sat, 26 Oct 2019 22:15:28 +0200 Subject: [PATCH 10/30] special case for pascaligo generated LIST/SET/MAP_FOLD --- src/passes/4-typer/typer.ml | 31 +++++++++++++++++++++++++++++++ 1 file changed, 31 insertions(+) diff --git a/src/passes/4-typer/typer.ml b/src/passes/4-typer/typer.ml index 28258b9fb..8d6803534 100644 --- a/src/passes/4-typer/typer.ml +++ b/src/passes/4-typer/typer.ml @@ -615,6 +615,37 @@ and type_expression : environment -> ?tv_opt:O.type_value -> I.expression -> O.a let output_type = body.type_annotation in return (E_lambda {binder = fst binder ; body}) (t_function input_type output_type ()) ) + | E_constant ( ("LIST_FOLD"|"MAP_FOLD"|"SET_FOLD") , + [ collect ; + init_record ; + ( { expression = (I.E_lambda { binder = (name, None) ; + input_type = None ; + output_type = None ; + result }) ; + location = _ }) as _lambda + ] ) -> + (* this special case is here force annotation of the lambda + generated by pascaligo's for_collect loop *) + let%bind lst' = bind_list @@ List.map (type_expression e) [collect ; init_record] in + let tv_lst = List.map get_type_annotation lst' in + let tv_col = List.nth tv_lst 0 in + let tv_out = List.nth tv_lst 1 in + let collect_inner_type = match tv_col.type_value' with + | O.T_constant ( ("list"|"set"|"map") , t) -> t + | _ -> failwith "impossible" in + let input_type = t_tuple (tv_out::collect_inner_type) () in + let output_type = Some tv_out in + + let e' = Environment.add_ez_binder name input_type e in + let%bind body = type_expression ?tv_opt:output_type e' result in + let output_type = body.type_annotation in + let%bind lambda' = ok @@ make_a_e (E_lambda {binder = name ; body}) (t_function input_type output_type ()) e in + + let%bind lst' = ok @@ lst'@[lambda'] in + let tv_lst = List.map get_type_annotation lst' in + let%bind (name', tv) = + type_constant name tv_lst tv_opt ae.location in + return (E_constant (name' , lst')) tv | E_constant (name, lst) -> let%bind lst' = bind_list @@ List.map (type_expression e) lst in let tv_lst = List.map get_type_annotation lst' in From 7f7f19854a15212547b59fced59ec7f96859b76d Mon Sep 17 00:00:00 2001 From: Lesenechal Remi Date: Sat, 26 Oct 2019 22:16:17 +0200 Subject: [PATCH 11/30] WIP : make test a bit easier --- src/test/contracts/loop.ligo | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/test/contracts/loop.ligo b/src/test/contracts/loop.ligo index 6e5e709a8..647735953 100644 --- a/src/test/contracts/loop.ligo +++ b/src/test/contracts/loop.ligo @@ -49,13 +49,13 @@ function for_collection (var nee : unit; var nuu : unit) : (int * string) is blo function for_collection_ (var nee : unit; var nuu : unit) : (int * string) is block { var acc : int := 0 ; var st : string := "to" ; - var toto : (string * string) := ("foo","bar") ; + // var toto : (string * string) := ("foo","bar") ; var mylist : list(int) := list 1 ; 1 ; 1 end ; for x : int in list mylist begin - toto.1 := "r"; + // toto.1 := "r"; acc := acc + x ; st := st^"to" ; end From 0cf747144106edacf81c02642ef91aa3de04e8d4 Mon Sep 17 00:00:00 2001 From: Lesenechal Remi Date: Sat, 26 Oct 2019 22:59:17 +0200 Subject: [PATCH 12/30] prepend the body of the lambda with let_in's --- src/passes/2-simplify/pascaligo.ml | 39 +++++++++++++++++++++--------- 1 file changed, 27 insertions(+), 12 deletions(-) diff --git a/src/passes/2-simplify/pascaligo.ml b/src/passes/2-simplify/pascaligo.ml index c785ee780..4b5a1b874 100644 --- a/src/passes/2-simplify/pascaligo.ml +++ b/src/passes/2-simplify/pascaligo.ml @@ -576,6 +576,7 @@ and simpl_fun_declaration : bind_fold_right_list aux result body in let expression : expression = e_lambda ~loc binder (Some input_type) (Some output_type) result in + (* let _toto = Format.printf "TAMERE %a \n" Ast_simplified.PP.expression expression in *) let type_annotation = Some (T_function (input_type, output_type)) in ok ((name , type_annotation) , expression) ) @@ -1017,30 +1018,45 @@ and simpl_for_collect : Raw.for_collect -> (_ -> expression result) result = fun block which will become the body of the lambda *) let%bind block' = simpl_block fc.block.value in let%bind block' = block' None in + let replace_with_record exp = match exp.expression with + (* replace asignement *) | E_assign ( name , path , expr ) -> let path' = ( match path with - | [] -> [Access_tuple 0 ; Access_record name ] @ path + | [] -> [Access_record name] (* This will fail for deep tuple access, see LIGO-131 *) - | _ -> [Access_tuple 0 ; Access_record name ] @ path ) in - ok @@ e_assign "arguments" path' expr + | _ -> ( (Access_record name) :: path ) + ) in + ok @@ e_assign "_COMPILER_acc" path' expr | E_variable name -> if (name = fc.var.value ) then - ok @@ e_accessor (e_variable "arguments") [Access_tuple 1] + (* replace reference to the collection element *) + ok @@ (e_variable "_COMPILER_collec_elt") else if (List.mem name captured_list) then - let acc_arg = e_accessor (e_variable "arguments") [Access_tuple 0] in - ok @@ e_accessor (acc_arg) [Access_record name] + (* replace reference fold accumulator *) + ok @@ e_accessor (e_variable "_COMPILER_acc") [Access_record name] else ok @@ exp | _ -> ok @@ exp in - let%bind block'' = Self_ast_simplified.map_expression replace_with_record block' in + let%bind block' = Self_ast_simplified.map_expression replace_with_record block' in + + (* append the return value *) let rec add_return expr = match expr.expression with | E_sequence (a,b) -> e_sequence a (add_return b) - | _ -> e_sequence expr (e_accessor (e_variable "arguments") [Access_tuple 0]) in - let block_with_return = add_return block'' in + | _ -> e_sequence expr (e_variable "_COMPILER_acc") in + let block' = add_return block' in + + (* prepend the body with let accumulator = argument.0 in let collec_elt = argument.1 in*) + let%bind elt_type = simpl_type_expression fc.elt_type in + let acc = e_accessor (e_variable "arguments") [Access_tuple 0] in + let collec_elt = e_accessor (e_variable "arguments") [Access_tuple 1] in + let args_let_in = e_let_in ("_COMPILER_acc", None) acc @@ + e_let_in ("_COMPILER_collec_elt", Some elt_type) collec_elt (e_skip ()) in + let block' = e_sequence args_let_in block' in + (* build the lambda*) - let lambda = e_lambda "_COMPILER_for_collect_lambda" None None block_with_return in + let lambda = e_lambda "_COMPILER_for_collect_lambda" None None block' in let%bind collect = simpl_expression fc.expr in let op_name = match fc.collection with | Map _ -> "MAP_FOLD" @@ -1049,7 +1065,7 @@ and simpl_for_collect : Raw.for_collect -> (_ -> expression result) result = fun let fold = e_constant op_name [collect ; init_record ; lambda] in let folded_record = e_let_in ("_COMPILER_folded_record", None) fold (e_skip ()) in - (* build the sequence of assigments back to the original variables *) + (* append assigments of fold result to the original captured variables *) let aux (prev : expression) (captured_varname : string) = let access = e_accessor (e_variable "_COMPILER_folded_record") [Access_record captured_varname] in @@ -1057,7 +1073,6 @@ and simpl_for_collect : Raw.for_collect -> (_ -> expression result) result = fun e_sequence prev assign in let ( final_sequence : expression ) = List.fold_left aux folded_record captured_list in - let _ = Format.printf "___ GEN ____\n %a \n" Ast_simplified.PP.expression final_sequence in return_statement @@ final_sequence From d651bfb3a3d6565b085e640eaf6611c589fe120b Mon Sep 17 00:00:00 2001 From: Lesenechal Remi Date: Sun, 27 Oct 2019 11:32:03 +0100 Subject: [PATCH 13/30] remove misplaced 'skip' --- src/passes/2-simplify/pascaligo.ml | 28 ++++++++++++++++------------ 1 file changed, 16 insertions(+), 12 deletions(-) diff --git a/src/passes/2-simplify/pascaligo.ml b/src/passes/2-simplify/pascaligo.ml index 4b5a1b874..f2ee15c73 100644 --- a/src/passes/2-simplify/pascaligo.ml +++ b/src/passes/2-simplify/pascaligo.ml @@ -576,7 +576,6 @@ and simpl_fun_declaration : bind_fold_right_list aux result body in let expression : expression = e_lambda ~loc binder (Some input_type) (Some output_type) result in - (* let _toto = Format.printf "TAMERE %a \n" Ast_simplified.PP.expression expression in *) let type_annotation = Some (T_function (input_type, output_type)) in ok ((name , type_annotation) , expression) ) @@ -1019,7 +1018,7 @@ and simpl_for_collect : Raw.for_collect -> (_ -> expression result) result = fun let%bind block' = simpl_block fc.block.value in let%bind block' = block' None in - let replace_with_record exp = + let replace exp = match exp.expression with (* replace asignement *) | E_assign ( name , path , expr ) -> @@ -1038,7 +1037,7 @@ and simpl_for_collect : Raw.for_collect -> (_ -> expression result) result = fun ok @@ e_accessor (e_variable "_COMPILER_acc") [Access_record name] else ok @@ exp | _ -> ok @@ exp in - let%bind block' = Self_ast_simplified.map_expression replace_with_record block' in + let%bind block' = Self_ast_simplified.map_expression replace block' in (* append the return value *) let rec add_return expr = match expr.expression with @@ -1050,12 +1049,11 @@ and simpl_for_collect : Raw.for_collect -> (_ -> expression result) result = fun let%bind elt_type = simpl_type_expression fc.elt_type in let acc = e_accessor (e_variable "arguments") [Access_tuple 0] in let collec_elt = e_accessor (e_variable "arguments") [Access_tuple 1] in - let args_let_in = e_let_in ("_COMPILER_acc", None) acc @@ - e_let_in ("_COMPILER_collec_elt", Some elt_type) collec_elt (e_skip ()) in - let block' = e_sequence args_let_in block' in + let block' = e_let_in ("_COMPILER_acc", None) acc @@ + e_let_in ("_COMPILER_collec_elt", Some elt_type) collec_elt (block') in - (* build the lambda*) + (* build the X_FOLD constant *) let lambda = e_lambda "_COMPILER_for_collect_lambda" None None block' in let%bind collect = simpl_expression fc.expr in let op_name = match fc.collection with @@ -1063,17 +1061,22 @@ and simpl_for_collect : Raw.for_collect -> (_ -> expression result) result = fun | Set _ -> "SET_FOLD" | List _ -> "LIST_FOLD" in let fold = e_constant op_name [collect ; init_record ; lambda] in - let folded_record = e_let_in ("_COMPILER_folded_record", None) fold (e_skip ()) in (* append assigments of fold result to the original captured variables *) - let aux (prev : expression) (captured_varname : string) = + let aux (prev : expression option) (captured_varname : string) = let access = e_accessor (e_variable "_COMPILER_folded_record") [Access_record captured_varname] in let assign = e_assign captured_varname [] access in - e_sequence prev assign in - - let ( final_sequence : expression ) = List.fold_left aux folded_record captured_list in + match prev with + | None -> Some assign + | Some p -> Some (e_sequence p assign) in + let ( reassign_sequence : expression option ) = List.fold_left aux None captured_list in + let final_sequence = match reassign_sequence with + (* None case means that no variables were captured *) + | None -> e_let_in ("_COMPILER_folded_record", None) fold (e_skip ()) + | Some seq -> e_let_in ("_COMPILER_folded_record", None) fold seq in + return_statement @@ final_sequence (** NODE TO AVOID THE DIRT: @@ -1083,6 +1086,7 @@ and simpl_for_collect : Raw.for_collect -> (_ -> expression result) result = fun begin i := .. end + - global definition of strings **) let simpl_program : Raw.ast -> program result = fun t -> From 164e88e818aa2ec477afaa90c8bb2a735022fe1b Mon Sep 17 00:00:00 2001 From: Lesenechal Remi Date: Sun, 27 Oct 2019 11:34:26 +0100 Subject: [PATCH 14/30] remove shadowing of lambda name over the constant name --- src/passes/4-typer/typer.ml | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/src/passes/4-typer/typer.ml b/src/passes/4-typer/typer.ml index 8d6803534..7b3744d79 100644 --- a/src/passes/4-typer/typer.ml +++ b/src/passes/4-typer/typer.ml @@ -615,7 +615,7 @@ and type_expression : environment -> ?tv_opt:O.type_value -> I.expression -> O.a let output_type = body.type_annotation in return (E_lambda {binder = fst binder ; body}) (t_function input_type output_type ()) ) - | E_constant ( ("LIST_FOLD"|"MAP_FOLD"|"SET_FOLD") , + | E_constant ( ("LIST_FOLD"|"MAP_FOLD"|"SET_FOLD") as opname , [ collect ; init_record ; ( { expression = (I.E_lambda { binder = (name, None) ; @@ -624,28 +624,28 @@ and type_expression : environment -> ?tv_opt:O.type_value -> I.expression -> O.a result }) ; location = _ }) as _lambda ] ) -> - (* this special case is here force annotation of the lambda + (* this special case is here force annotation of the untyped lambda generated by pascaligo's for_collect loop *) let%bind lst' = bind_list @@ List.map (type_expression e) [collect ; init_record] in let tv_lst = List.map get_type_annotation lst' in let tv_col = List.nth tv_lst 0 in let tv_out = List.nth tv_lst 1 in let collect_inner_type = match tv_col.type_value' with - | O.T_constant ( ("list"|"set"|"map") , t) -> t + | O.T_constant ( ("list"|"set"|"map") , [t]) -> t | _ -> failwith "impossible" in - let input_type = t_tuple (tv_out::collect_inner_type) () in + let input_type = t_tuple (tv_out::[collect_inner_type]) () in let output_type = Some tv_out in - let e' = Environment.add_ez_binder name input_type e in + let e' = Environment.add_ez_binder "arguments" input_type e in let%bind body = type_expression ?tv_opt:output_type e' result in let output_type = body.type_annotation in let%bind lambda' = ok @@ make_a_e (E_lambda {binder = name ; body}) (t_function input_type output_type ()) e in let%bind lst' = ok @@ lst'@[lambda'] in let tv_lst = List.map get_type_annotation lst' in - let%bind (name', tv) = - type_constant name tv_lst tv_opt ae.location in - return (E_constant (name' , lst')) tv + let%bind (opname', tv) = + type_constant opname tv_lst tv_opt ae.location in + return (E_constant (opname' , lst')) tv | E_constant (name, lst) -> let%bind lst' = bind_list @@ List.map (type_expression e) lst in let tv_lst = List.map get_type_annotation lst' in From a3deccf352bcbb80ea32ef89ed6885c424b76919 Mon Sep 17 00:00:00 2001 From: Lesenechal Remi Date: Sun, 27 Oct 2019 11:43:51 +0100 Subject: [PATCH 15/30] changing the name of the lambda to 'arguments' make its arguments available --- src/passes/2-simplify/pascaligo.ml | 2 +- src/passes/4-typer/typer.ml | 6 +++--- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/src/passes/2-simplify/pascaligo.ml b/src/passes/2-simplify/pascaligo.ml index f2ee15c73..066949450 100644 --- a/src/passes/2-simplify/pascaligo.ml +++ b/src/passes/2-simplify/pascaligo.ml @@ -1054,7 +1054,7 @@ and simpl_for_collect : Raw.for_collect -> (_ -> expression result) result = fun (* build the X_FOLD constant *) - let lambda = e_lambda "_COMPILER_for_collect_lambda" None None block' in + let lambda = e_lambda "arguments" None None block' in let%bind collect = simpl_expression fc.expr in let op_name = match fc.collection with | Map _ -> "MAP_FOLD" diff --git a/src/passes/4-typer/typer.ml b/src/passes/4-typer/typer.ml index 7b3744d79..73a8144e2 100644 --- a/src/passes/4-typer/typer.ml +++ b/src/passes/4-typer/typer.ml @@ -618,7 +618,7 @@ and type_expression : environment -> ?tv_opt:O.type_value -> I.expression -> O.a | E_constant ( ("LIST_FOLD"|"MAP_FOLD"|"SET_FOLD") as opname , [ collect ; init_record ; - ( { expression = (I.E_lambda { binder = (name, None) ; + ( { expression = (I.E_lambda { binder = (lname, None) ; input_type = None ; output_type = None ; result }) ; @@ -636,10 +636,10 @@ and type_expression : environment -> ?tv_opt:O.type_value -> I.expression -> O.a let input_type = t_tuple (tv_out::[collect_inner_type]) () in let output_type = Some tv_out in - let e' = Environment.add_ez_binder "arguments" input_type e in + let e' = Environment.add_ez_binder lname input_type e in let%bind body = type_expression ?tv_opt:output_type e' result in let output_type = body.type_annotation in - let%bind lambda' = ok @@ make_a_e (E_lambda {binder = name ; body}) (t_function input_type output_type ()) e in + let%bind lambda' = ok @@ make_a_e (E_lambda {binder = lname ; body}) (t_function input_type output_type ()) e in let%bind lst' = ok @@ lst'@[lambda'] in let tv_lst = List.map get_type_annotation lst' in From 7eed9b1856e6c0c9a6c46a45eaa17f051bc4367c Mon Sep 17 00:00:00 2001 From: Lesenechal Remi Date: Sun, 27 Oct 2019 11:47:17 +0100 Subject: [PATCH 16/30] test passing ! --- src/test/contracts/loop.ligo | 6 +++--- src/test/integration_tests.ml | 5 +++++ 2 files changed, 8 insertions(+), 3 deletions(-) diff --git a/src/test/contracts/loop.ligo b/src/test/contracts/loop.ligo index 647735953..d96753105 100644 --- a/src/test/contracts/loop.ligo +++ b/src/test/contracts/loop.ligo @@ -31,7 +31,7 @@ function lamby (var accu : (record st : string ; acc : int end) ; var i : int ) accu.st := accu.st ^ "to" ; } with accu -function for_collection (var nee : unit; var nuu : unit) : (int * string) is block { +function for_collection_ (var nee : unit; var nuu : unit) : (int * string) is block { var acc : int := 0 ; var st : string := "to" ; var mylist : list(int) := list 1 ; 1 ; 1 end ; @@ -46,7 +46,7 @@ function for_collection (var nee : unit; var nuu : unit) : (int * string) is blo } with (folded_record.acc , folded_record.st) -function for_collection_ (var nee : unit; var nuu : unit) : (int * string) is block { +function for_collection (var nee : unit) : (int * string) is block { var acc : int := 0 ; var st : string := "to" ; // var toto : (string * string) := ("foo","bar") ; @@ -60,7 +60,7 @@ function for_collection_ (var nee : unit; var nuu : unit) : (int * string) is bl st := st^"to" ; end -} with acc +} with (acc, st) function dummy (const n : nat) : nat is block { while (False) block { skip } diff --git a/src/test/integration_tests.ml b/src/test/integration_tests.ml index 0088b0e31..992c21d4a 100644 --- a/src/test/integration_tests.ml +++ b/src/test/integration_tests.ml @@ -670,6 +670,11 @@ let loop () : unit result = let make_expected = fun n -> e_int (n * (n + 1) / 2) in expect_eq_n_pos_mid program "for_sum" make_input make_expected in + let%bind () = + let input = e_unit () in + let expected = e_pair (e_int 3) (e_string "totototo") in + expect_eq program "for_collection" input expected + in ok () (* Don't know how to assert parse error happens in this test framework From 5a77b08aa795fd23e63e2ba120f3b46bc84bcad2 Mon Sep 17 00:00:00 2001 From: Lesenechal Remi Date: Sun, 27 Oct 2019 13:03:08 +0100 Subject: [PATCH 17/30] cleaning & documenting --- src/passes/2-simplify/pascaligo.ml | 85 +++++++++++------------------- src/passes/4-typer/typer.ml | 27 +++++----- 2 files changed, 43 insertions(+), 69 deletions(-) diff --git a/src/passes/2-simplify/pascaligo.ml b/src/passes/2-simplify/pascaligo.ml index 066949450..2a8218156 100644 --- a/src/passes/2-simplify/pascaligo.ml +++ b/src/passes/2-simplify/pascaligo.ml @@ -989,105 +989,80 @@ and simpl_for_int : Raw.for_int -> (_ -> expression result) result = fun fi -> and simpl_for_collect : Raw.for_collect -> (_ -> expression result) result = fun fc -> let statements = npseq_to_list fc.block.value.statements in - (* building initial record *) - let aux (el : Raw.statement) : Raw.instruction option = match el with + (* build initial record *) + let filter_assignments (el : Raw.statement) : Raw.instruction option = match el with | Raw.Instr (Assign _ as i) -> Some i | _ -> None in - let assign_instrs = List.filter_map aux statements in + let assign_instrs = List.filter_map filter_assignments statements in let%bind assign_instrs' = bind_map_list (fun el -> let%bind assign' = simpl_instruction el in let%bind assign' = assign' None in ok @@ assign') assign_instrs in - let aux prev ass_exp = - match ass_exp.expression with - | E_assign ( name , _ , _ ) -> - let expr' = e_variable name in - SMap.add name expr' prev - | _ -> prev in - let captured_list = List.filter_map + let captured_name_list = List.filter_map (fun ass_exp -> match ass_exp.expression with - | E_assign ( name, _ , _ ) -> Some name - | _ -> None ) + | E_assign ( name, _ , _ ) -> Some name | _ -> None ) assign_instrs' in - let init_record = e_record (List.fold_left aux SMap.empty assign_instrs') in - - (* replace assignments to X assignments to record in the for_collect - block which will become the body of the lambda *) - let%bind block' = simpl_block fc.block.value in - let%bind block' = block' None in - + let add_to_record (prev: expression type_name_map) (captured_name: string) = + SMap.add captured_name (e_variable captured_name) prev in + let init_record = e_record (List.fold_left add_to_record SMap.empty captured_name_list) in + (* replace references to the future lambda arguments in the for body *) + let%bind for_body = simpl_block fc.block.value in + let%bind for_body = for_body None in let replace exp = + (* TODO: map and set updated/remove must also be captured *) match exp.expression with - (* replace asignement *) | E_assign ( name , path , expr ) -> + (* replace references to fold accumulator as rhs *) let path' = ( match path with | [] -> [Access_record name] - (* This will fail for deep tuple access, see LIGO-131 *) + (* This might fail for deep tuple access, see LIGO-131 *) | _ -> ( (Access_record name) :: path ) ) in ok @@ e_assign "_COMPILER_acc" path' expr | E_variable name -> if (name = fc.var.value ) then - (* replace reference to the collection element *) + (* replace references to the collection element *) ok @@ (e_variable "_COMPILER_collec_elt") - else if (List.mem name captured_list) then - (* replace reference fold accumulator *) + else if (List.mem name captured_name_list) then + (* replace references to fold accumulator as lhs *) ok @@ e_accessor (e_variable "_COMPILER_acc") [Access_record name] else ok @@ exp | _ -> ok @@ exp in - let%bind block' = Self_ast_simplified.map_expression replace block' in - - (* append the return value *) - let rec add_return expr = match expr.expression with + let%bind for_body = Self_ast_simplified.map_expression replace for_body in + (* append the return value (the accumulator) to the for body *) + let rec add_return (expr : expression) = match expr.expression with | E_sequence (a,b) -> e_sequence a (add_return b) | _ -> e_sequence expr (e_variable "_COMPILER_acc") in - let block' = add_return block' in - - (* prepend the body with let accumulator = argument.0 in let collec_elt = argument.1 in*) + let for_body = add_return for_body in + (* prepend for body with args declaration (accumulator and collection element)*) let%bind elt_type = simpl_type_expression fc.elt_type in let acc = e_accessor (e_variable "arguments") [Access_tuple 0] in let collec_elt = e_accessor (e_variable "arguments") [Access_tuple 1] in - let block' = e_let_in ("_COMPILER_acc", None) acc @@ - e_let_in ("_COMPILER_collec_elt", Some elt_type) collec_elt (block') in - - + let for_body = e_let_in ("_COMPILER_acc", None) acc @@ + e_let_in ("_COMPILER_collec_elt", Some elt_type) collec_elt (for_body) in (* build the X_FOLD constant *) - let lambda = e_lambda "arguments" None None block' in let%bind collect = simpl_expression fc.expr in + let lambda = e_lambda "arguments" None None for_body in let op_name = match fc.collection with - | Map _ -> "MAP_FOLD" - | Set _ -> "SET_FOLD" - | List _ -> "LIST_FOLD" in + | Map _ -> "MAP_FOLD" | Set _ -> "SET_FOLD" | List _ -> "LIST_FOLD" in let fold = e_constant op_name [collect ; init_record ; lambda] in - - (* append assigments of fold result to the original captured variables *) - let aux (prev : expression option) (captured_varname : string) = + (* build sequence to re-assign fold result to the original captured variables *) + let assign_back (prev : expression option) (captured_varname : string) : expression option = let access = e_accessor (e_variable "_COMPILER_folded_record") [Access_record captured_varname] in let assign = e_assign captured_varname [] access in match prev with | None -> Some assign | Some p -> Some (e_sequence p assign) in - let ( reassign_sequence : expression option ) = List.fold_left aux None captured_list in - + let reassign_sequence = List.fold_left assign_back None captured_name_list in + (* attach the folded record to the re-assign sequence *) let final_sequence = match reassign_sequence with (* None case means that no variables were captured *) | None -> e_let_in ("_COMPILER_folded_record", None) fold (e_skip ()) | Some seq -> e_let_in ("_COMPILER_folded_record", None) fold seq in - return_statement @@ final_sequence -(** NODE TO AVOID THE DIRT: - - have a E_unsimplified 'a which is then transformed in a self pass ?? - - need to forbid that ? - for i in somelist - begin - i := .. - end - - global definition of strings -**) - let simpl_program : Raw.ast -> program result = fun t -> bind_list @@ List.map simpl_declaration @@ nseq_to_list t.decl \ No newline at end of file diff --git a/src/passes/4-typer/typer.ml b/src/passes/4-typer/typer.ml index 73a8144e2..832e7b04f 100644 --- a/src/passes/4-typer/typer.ml +++ b/src/passes/4-typer/typer.ml @@ -626,22 +626,21 @@ and type_expression : environment -> ?tv_opt:O.type_value -> I.expression -> O.a ] ) -> (* this special case is here force annotation of the untyped lambda generated by pascaligo's for_collect loop *) - let%bind lst' = bind_list @@ List.map (type_expression e) [collect ; init_record] in - let tv_lst = List.map get_type_annotation lst' in - let tv_col = List.nth tv_lst 0 in - let tv_out = List.nth tv_lst 1 in - let collect_inner_type = match tv_col.type_value' with - | O.T_constant ( ("list"|"set"|"map") , [t]) -> t - | _ -> failwith "impossible" in - let input_type = t_tuple (tv_out::[collect_inner_type]) () in - let output_type = Some tv_out in - + let%bind (v_col , v_initr ) = bind_map_pair (type_expression e) (collect , init_record ) in + let tv_col = get_type_annotation v_col in (* this is the type of the collection *) + let tv_out = get_type_annotation v_initr in (* this is the output type of the lambda*) + let%bind col_inner_type = match tv_col.type_value' with + | O.T_constant ( ("list"|"set"|"map") , [t]) -> ok t + | _ -> + let wtype = Format.asprintf + "Loops over collections expect lists, sets or maps, type %a" O.PP.type_value tv_col in + fail @@ simple_error wtype in + let input_type = t_tuple (tv_out::[col_inner_type]) () in let e' = Environment.add_ez_binder lname input_type e in - let%bind body = type_expression ?tv_opt:output_type e' result in + let%bind body = type_expression ?tv_opt:(Some tv_out) e' result in let output_type = body.type_annotation in - let%bind lambda' = ok @@ make_a_e (E_lambda {binder = lname ; body}) (t_function input_type output_type ()) e in - - let%bind lst' = ok @@ lst'@[lambda'] in + let lambda' = make_a_e (E_lambda {binder = lname ; body}) (t_function input_type output_type ()) e in + let lst' = [v_col; v_initr ; lambda'] in let tv_lst = List.map get_type_annotation lst' in let%bind (opname', tv) = type_constant opname tv_lst tv_opt ae.location in From c7056d200dad536635bf7bf2c769f875d2238e04 Mon Sep 17 00:00:00 2001 From: Lesenechal Remi Date: Sun, 27 Oct 2019 13:57:26 +0100 Subject: [PATCH 18/30] merging with dev --- src/test/integration_tests.ml | 6 ------ 1 file changed, 6 deletions(-) diff --git a/src/test/integration_tests.ml b/src/test/integration_tests.ml index 992c21d4a..dbd388cdd 100644 --- a/src/test/integration_tests.ml +++ b/src/test/integration_tests.ml @@ -658,14 +658,8 @@ let loop () : unit result = let make_input = e_nat in let make_expected = fun n -> e_nat (n * (n + 1) / 2) in expect_eq_n_pos_mid program "while_sum" make_input make_expected -<<<<<<< HEAD - in(* For loop is currently unsupported - - let%bind () = -======= in let%bind () = ->>>>>>> First version for ForInt loops let make_input = e_nat in let make_expected = fun n -> e_int (n * (n + 1) / 2) in expect_eq_n_pos_mid program "for_sum" make_input make_expected From b71309bfa2eb1c2230bc354ca32e3da16c7d6f38 Mon Sep 17 00:00:00 2001 From: Lesenechal Remi Date: Sun, 27 Oct 2019 14:09:04 +0100 Subject: [PATCH 19/30] proper error message for deep accesses in loops of collection body --- src/passes/2-simplify/pascaligo.ml | 24 ++++++++++++++++-------- 1 file changed, 16 insertions(+), 8 deletions(-) diff --git a/src/passes/2-simplify/pascaligo.ml b/src/passes/2-simplify/pascaligo.ml index 2a8218156..4ae15d8dd 100644 --- a/src/passes/2-simplify/pascaligo.ml +++ b/src/passes/2-simplify/pascaligo.ml @@ -137,6 +137,17 @@ module Errors = struct ] in error ~data title message + let unsupported_deep_access_for_collection for_col = + let title () = "deep access in loop over collection" in + let message () = + Format.asprintf "currently, we do not support deep \ + accesses in loops over collection" in + let data = [ + ("pattern_loc", + fun () -> Format.asprintf "%a" Location.pp_lift @@ for_col.Region.region) + ] in + error ~data title message + (* Logging *) let simplifying_instruction t = @@ -1013,14 +1024,11 @@ and simpl_for_collect : Raw.for_collect -> (_ -> expression result) result = fun let replace exp = (* TODO: map and set updated/remove must also be captured *) match exp.expression with - | E_assign ( name , path , expr ) -> - (* replace references to fold accumulator as rhs *) - let path' = ( match path with - | [] -> [Access_record name] - (* This might fail for deep tuple access, see LIGO-131 *) - | _ -> ( (Access_record name) :: path ) - ) in - ok @@ e_assign "_COMPILER_acc" path' expr + (* replace references to fold accumulator as rhs *) + | E_assign ( name , path , expr ) -> ( match path with + | [] -> ok @@ e_assign "_COMPILER_acc" [Access_record name] expr + (* This fails for deep accesses, see LIGO-131 *) + | _ -> fail @@ unsupported_deep_access_for_collection fc.block ) | E_variable name -> if (name = fc.var.value ) then (* replace references to the collection element *) From 1a035f9713c970ac08c03e080d6a95240c176317 Mon Sep 17 00:00:00 2001 From: Lesenechal Remi Date: Sun, 27 Oct 2019 14:12:42 +0100 Subject: [PATCH 20/30] tests for sets --- src/test/contracts/loop.ligo | 18 +++++++++++------- src/test/integration_tests.ml | 7 ++++++- 2 files changed, 17 insertions(+), 8 deletions(-) diff --git a/src/test/contracts/loop.ligo b/src/test/contracts/loop.ligo index d96753105..eaa429df7 100644 --- a/src/test/contracts/loop.ligo +++ b/src/test/contracts/loop.ligo @@ -35,7 +35,6 @@ function for_collection_ (var nee : unit; var nuu : unit) : (int * string) is bl var acc : int := 0 ; var st : string := "to" ; var mylist : list(int) := list 1 ; 1 ; 1 end ; - var init_record : (record st : string; acc : int end ) := record st = st; acc = acc; end; var folded_record : (record st : string; acc : int end ) := @@ -43,23 +42,28 @@ function for_collection_ (var nee : unit; var nuu : unit) : (int * string) is bl skip ; st := folded_record.st ; acc := folded_record.acc ; - } with (folded_record.acc , folded_record.st) -function for_collection (var nee : unit) : (int * string) is block { +function for_collection_list (var nee : unit) : (int * string) is block { var acc : int := 0 ; var st : string := "to" ; - // var toto : (string * string) := ("foo","bar") ; - var mylist : list(int) := list 1 ; 1 ; 1 end ; - for x : int in list mylist begin - // toto.1 := "r"; acc := acc + x ; st := st^"to" ; end +} with (acc, st) +function for_collection_set (var nee : unit) : (int * string) is block { + var acc : int := 0 ; + var st : string := "to" ; + var myset : set(int) := set 1 ; 2 ; 3 end ; + for x : int in set myset + begin + acc := acc + x ; + st := st^"to" ; + end } with (acc, st) function dummy (const n : nat) : nat is block { diff --git a/src/test/integration_tests.ml b/src/test/integration_tests.ml index dbd388cdd..3ed6d871e 100644 --- a/src/test/integration_tests.ml +++ b/src/test/integration_tests.ml @@ -667,7 +667,12 @@ let loop () : unit result = let%bind () = let input = e_unit () in let expected = e_pair (e_int 3) (e_string "totototo") in - expect_eq program "for_collection" input expected + expect_eq program "for_collection_list" input expected + in + let%bind () = + let input = e_unit () in + let expected = e_pair (e_int 6) (e_string "totototo") in + expect_eq program "for_collection_set" input expected in ok () From e16eac77a660e97e6a5518808fdbda415e440487 Mon Sep 17 00:00:00 2001 From: Lesenechal Remi Date: Sun, 27 Oct 2019 16:42:11 +0100 Subject: [PATCH 21/30] fixes for loop on map. Untested because of issue with deep tuple access (LIGO-131 LIGO-134) An error message is in the simplifier --- src/passes/2-simplify/pascaligo.ml | 90 +++++++++++++++++++++--------- src/passes/4-typer/typer.ml | 8 +-- src/test/contracts/loop.ligo | 12 +++- 3 files changed, 80 insertions(+), 30 deletions(-) diff --git a/src/passes/2-simplify/pascaligo.ml b/src/passes/2-simplify/pascaligo.ml index 4ae15d8dd..66fe46481 100644 --- a/src/passes/2-simplify/pascaligo.ml +++ b/src/passes/2-simplify/pascaligo.ml @@ -68,16 +68,6 @@ module Errors = struct ] in error ~data title message - (* let unsupported_for_loops region = - let title () = "bounded iterators" in - let message () = - Format.asprintf "only simple for loops are supported for now" in - let data = [ - ("loop_loc", - fun () -> Format.asprintf "%a" Location.pp_lift @@ region) - ] in - error ~data title message *) - let unsupported_non_var_pattern p = let title () = "pattern is not a variable" in let message () = @@ -148,6 +138,16 @@ module Errors = struct ] in error ~data title message + let unsupported_for_collect_map for_col = + let title () = "for loop over map" in + let message () = + Format.asprintf "for loops over map are not supported yet" in + let data = [ + ("loop_loc", + fun () -> Format.asprintf "%a" Location.pp_lift @@ for_col.Region.region) + ] in + error ~data title message + (* Logging *) let simplifying_instruction t = @@ -999,6 +999,7 @@ and simpl_for_int : Raw.for_int -> (_ -> expression result) result = fun fi -> return_statement @@ e_let_in (fi.assign.value.name.value, Some t_int) value loop and simpl_for_collect : Raw.for_collect -> (_ -> expression result) result = fun fc -> + match fc.collection with | Map _ -> fail @@ unsupported_for_collect_map fc.block | _ -> let statements = npseq_to_list fc.block.value.statements in (* build initial record *) let filter_assignments (el : Raw.statement) : Raw.instruction option = match el with @@ -1027,16 +1028,43 @@ and simpl_for_collect : Raw.for_collect -> (_ -> expression result) result = fun (* replace references to fold accumulator as rhs *) | E_assign ( name , path , expr ) -> ( match path with | [] -> ok @@ e_assign "_COMPILER_acc" [Access_record name] expr - (* This fails for deep accesses, see LIGO-131 *) - | _ -> fail @@ unsupported_deep_access_for_collection fc.block ) - | E_variable name -> - if (name = fc.var.value ) then - (* replace references to the collection element *) - ok @@ (e_variable "_COMPILER_collec_elt") - else if (List.mem name captured_name_list) then - (* replace references to fold accumulator as lhs *) - ok @@ e_accessor (e_variable "_COMPILER_acc") [Access_record name] - else ok @@ exp + (* This fails for deep accesses, see LIGO-131 LIGO-134 *) + | _ -> + (* ok @@ e_assign "_COMPILER_acc" ((Access_record name)::path) expr) *) + fail @@ unsupported_deep_access_for_collection fc.block ) + | E_variable name -> ( match fc.collection with + (* loop on map *) + | Map _ -> + let k' = e_variable "_COMPILER_collec_elt_k" in + let v' = e_variable "_COMPILER_collec_elt_v" in + ( match fc.bind_to with + | Some (_,v) -> + if ( name = fc.var.value ) then + ok @@ k' (* replace references to the the key *) + else if ( name = v.value ) then + ok @@ v' (* replace references to the the value *) + else if (List.mem name captured_name_list) then + (* replace references to fold accumulator as lhs *) + ok @@ e_accessor (e_variable "_COMPILER_acc") [Access_record name] + else ok @@ exp + | None -> + if ( name = fc.var.value ) then + ok @@ k' (* replace references to the key *) + else if (List.mem name captured_name_list) then + (* replace references to fold accumulator as lhs *) + ok @@ e_accessor (e_variable "_COMPILER_acc") [Access_record name] + else ok @@ exp + ) + (* loop on set or list *) + | (Set _ | List _) -> + if (name = fc.var.value ) then + (* replace references to the collection element *) + ok @@ (e_variable "_COMPILER_collec_elt") + else if (List.mem name captured_name_list) then + (* replace references to fold accumulator as lhs *) + ok @@ e_accessor (e_variable "_COMPILER_acc") [Access_record name] + else ok @@ exp + ) | _ -> ok @@ exp in let%bind for_body = Self_ast_simplified.map_expression replace for_body in (* append the return value (the accumulator) to the for body *) @@ -1044,12 +1072,24 @@ and simpl_for_collect : Raw.for_collect -> (_ -> expression result) result = fun | E_sequence (a,b) -> e_sequence a (add_return b) | _ -> e_sequence expr (e_variable "_COMPILER_acc") in let for_body = add_return for_body in - (* prepend for body with args declaration (accumulator and collection element)*) + (* prepend for body with args declaration (accumulator and collection elements *) let%bind elt_type = simpl_type_expression fc.elt_type in - let acc = e_accessor (e_variable "arguments") [Access_tuple 0] in - let collec_elt = e_accessor (e_variable "arguments") [Access_tuple 1] in - let for_body = e_let_in ("_COMPILER_acc", None) acc @@ - e_let_in ("_COMPILER_collec_elt", Some elt_type) collec_elt (for_body) in + let for_body = + let ( arg_access: Types.access_path -> expression ) = e_accessor (e_variable "arguments") in + ( match fc.collection with + | Map _ -> + let acc = arg_access [Access_tuple 0 ; Access_tuple 0] in + let collec_elt_v = arg_access [Access_tuple 1 ; Access_tuple 0] in + let collec_elt_k = arg_access [Access_tuple 1 ; Access_tuple 1] in + e_let_in ("_COMPILER_acc", None) acc @@ + e_let_in ("_COMPILER_collec_elt_k", None) collec_elt_v @@ + e_let_in ("_COMPILER_collec_elt_v", None) collec_elt_k (for_body) + | _ -> + let acc = arg_access [Access_tuple 0] in + let collec_elt = arg_access [Access_tuple 1] in + e_let_in ("_COMPILER_acc", None) acc @@ + e_let_in ("_COMPILER_collec_elt", Some elt_type) collec_elt (for_body) + ) in (* build the X_FOLD constant *) let%bind collect = simpl_expression fc.expr in let lambda = e_lambda "arguments" None None for_body in diff --git a/src/passes/4-typer/typer.ml b/src/passes/4-typer/typer.ml index 832e7b04f..99d8adf3c 100644 --- a/src/passes/4-typer/typer.ml +++ b/src/passes/4-typer/typer.ml @@ -629,13 +629,13 @@ and type_expression : environment -> ?tv_opt:O.type_value -> I.expression -> O.a let%bind (v_col , v_initr ) = bind_map_pair (type_expression e) (collect , init_record ) in let tv_col = get_type_annotation v_col in (* this is the type of the collection *) let tv_out = get_type_annotation v_initr in (* this is the output type of the lambda*) - let%bind col_inner_type = match tv_col.type_value' with - | O.T_constant ( ("list"|"set"|"map") , [t]) -> ok t + let%bind input_type = match tv_col.type_value' with + | O.T_constant ( ("list"|"set") , t) -> ok @@ t_tuple (tv_out::t) () + | O.T_constant ( "map" , t) -> ok @@ t_tuple (tv_out::[(t_tuple t ())]) () | _ -> let wtype = Format.asprintf - "Loops over collections expect lists, sets or maps, type %a" O.PP.type_value tv_col in + "Loops over collections expect lists, sets or maps, got type %a" O.PP.type_value tv_col in fail @@ simple_error wtype in - let input_type = t_tuple (tv_out::[col_inner_type]) () in let e' = Environment.add_ez_binder lname input_type e in let%bind body = type_expression ?tv_opt:(Some tv_out) e' result in let output_type = body.type_annotation in diff --git a/src/test/contracts/loop.ligo b/src/test/contracts/loop.ligo index eaa429df7..f559c2816 100644 --- a/src/test/contracts/loop.ligo +++ b/src/test/contracts/loop.ligo @@ -39,7 +39,6 @@ function for_collection_ (var nee : unit; var nuu : unit) : (int * string) is bl record st = st; acc = acc; end; var folded_record : (record st : string; acc : int end ) := list_fold(mylist , init_record , lamby) ; - skip ; st := folded_record.st ; acc := folded_record.acc ; } with (folded_record.acc , folded_record.st) @@ -66,6 +65,17 @@ function for_collection_set (var nee : unit) : (int * string) is block { end } with (acc, st) +// function for_collection_map (var nee : unit) : (int * string) is block { +// var acc : int := 0 ; +// var st : string := "" ; +// var mymap : map(string,int) := map "one" -> 1 ; "two" -> 2 ; "three" -> 3 end ; +// for k -> v : (string * int) in map mymap +// begin +// acc := acc + v ; +// st := k^st ; +// end +// } with (acc, st) + function dummy (const n : nat) : nat is block { while (False) block { skip } } with n From 2ced2e784e3088b3983bdc7fa0516c3faedf744e Mon Sep 17 00:00:00 2001 From: Lesenechal Remi Date: Mon, 28 Oct 2019 18:40:53 +0100 Subject: [PATCH 22/30] add doc --- src/passes/2-simplify/pascaligo.ml | 143 ++++++++++++++++++++++------- 1 file changed, 112 insertions(+), 31 deletions(-) diff --git a/src/passes/2-simplify/pascaligo.ml b/src/passes/2-simplify/pascaligo.ml index 66fe46481..ec38004b3 100644 --- a/src/passes/2-simplify/pascaligo.ml +++ b/src/passes/2-simplify/pascaligo.ml @@ -998,13 +998,88 @@ and simpl_for_int : Raw.for_int -> (_ -> expression result) result = fun fi -> let loop = e_loop comp body' in return_statement @@ e_let_in (fi.assign.value.name.value, Some t_int) value loop +(** simpl_for_collect + For loops over collections, like + + ``` concrete syntax : + for x : int in set myset + begin + myint := myint + x ; + myst := myst ^ "to" ; + end + ``` + + are implemented using a MAP_FOLD, LIST_FOLD or SET_FOLD: + + ``` pseudo Ast_simplified + let #COMPILER#folded_record = list_fold( mylist , + record st = st; acc = acc; end; + lamby = fun arguments -> ( + let #COMPILER#acc = arguments.0 in + let #COMPILER#elt = arguments.1 in + #COMPILER#acc.myint := #COMPILER#acc.myint + #COMPILER#elt ; + #COMPILER#acc.myst := #COMPILER#acc.myst ^ "to" ; + #COMPILER#acc + ) + ) in + { + myst := #COMPILER#folded_record.myst ; + myint := #COMPILER#folded_record.myint ; + } + ``` + + We are performing the following steps: + 1) Filtering out of the body all the constructions that can't + alter the environment (assignements and map/set patches) + and simplifying only those. + + 2) Detect the free variables and build a list of their names + (myint and myst in the previous example) + + 3) Build the initial record (later passed as 2nd argument of + `MAP/SET/LIST_FOLD`) capturing the environment using the + free variables list of (2) + + 4) In the filtered body of (1), replace occurences: + - free variable of name X as rhs ==> accessor `#COMPILER#acc.X` + - free variable of name X as lhs ==> accessor `#COMPILER#acc.X` + And, in the case of a map: + - references to the iterated key ==> variable `#COMPILER#elt_key` + - references to the iterated value ==> variable `#COMPILER#elt_value` + in the case of a set/list: + - references to the iterated value ==> variable `#COMPILER#elt` + + 5) Append the return value to the body + + 6) Prepend the declaration of the lambda arguments to the body which + is a serie of `let .. in`'s + Note that the parameter of the lambda ̀arguments` is a tree of + tuple holding: + * In the case of `list` or ̀set`: + ( folding record , current list/set element ) as + ( #COMPILER#acc , #COMPILER#elt ) + * In the case of `map`: + ( folding record , current map key , current map value ) as + ( #COMPILER#acc , #COMPILER#elt_key , #COMPILER#elt_value ) + + 7) Build the lambda using the final body of (6) + + 8) Build a sequence of assignments for all the captured variables + to their new value, namely an access to the folded record + (#COMPILER#folded_record) + + 9) Attach the sequence of 8 to the ̀let .. in` declaration + of #COMPILER#folded_record + +**) and simpl_for_collect : Raw.for_collect -> (_ -> expression result) result = fun fc -> match fc.collection with | Map _ -> fail @@ unsupported_for_collect_map fc.block | _ -> let statements = npseq_to_list fc.block.value.statements in - (* build initial record *) - let filter_assignments (el : Raw.statement) : Raw.instruction option = match el with - | Raw.Instr (Assign _ as i) -> Some i - | _ -> None in + (* STEP 1 *) + let filter_assignments (el : Raw.statement) : Raw.instruction option = + match el with + | Raw.Instr (Assign _ as i) -> Some i + | _ -> None in let assign_instrs = List.filter_map filter_assignments statements in let%bind assign_instrs' = bind_map_list (fun el -> @@ -1012,31 +1087,37 @@ and simpl_for_collect : Raw.for_collect -> (_ -> expression result) result = fun let%bind assign' = assign' None in ok @@ assign') assign_instrs in + (* STEP 2 *) let captured_name_list = List.filter_map - (fun ass_exp -> match ass_exp.expression with - | E_assign ( name, _ , _ ) -> Some name | _ -> None ) + (fun ass_exp -> + match ass_exp.expression with + | E_assign ( name, _ , _ ) -> Some name + | _ -> None ) assign_instrs' in + (* STEP 3 *) let add_to_record (prev: expression type_name_map) (captured_name: string) = SMap.add captured_name (e_variable captured_name) prev in let init_record = e_record (List.fold_left add_to_record SMap.empty captured_name_list) in - (* replace references to the future lambda arguments in the for body *) + (* STEP 4 *) let%bind for_body = simpl_block fc.block.value in let%bind for_body = for_body None in let replace exp = (* TODO: map and set updated/remove must also be captured *) match exp.expression with (* replace references to fold accumulator as rhs *) - | E_assign ( name , path , expr ) -> ( match path with - | [] -> ok @@ e_assign "_COMPILER_acc" [Access_record name] expr + | E_assign ( name , path , expr ) -> ( + match path with + | [] -> ok @@ e_assign "#COMPILER#acc" [Access_record name] expr (* This fails for deep accesses, see LIGO-131 LIGO-134 *) | _ -> - (* ok @@ e_assign "_COMPILER_acc" ((Access_record name)::path) expr) *) + (* ok @@ e_assign "#COMPILER#acc" ((Access_record name)::path) expr) *) fail @@ unsupported_deep_access_for_collection fc.block ) - | E_variable name -> ( match fc.collection with + | E_variable name -> ( + match fc.collection with (* loop on map *) | Map _ -> - let k' = e_variable "_COMPILER_collec_elt_k" in - let v' = e_variable "_COMPILER_collec_elt_v" in + let k' = e_variable "#COMPILER#collec_elt_k" in + let v' = e_variable "#COMPILER#collec_elt_v" in ( match fc.bind_to with | Some (_,v) -> if ( name = fc.var.value ) then @@ -1045,34 +1126,34 @@ and simpl_for_collect : Raw.for_collect -> (_ -> expression result) result = fun ok @@ v' (* replace references to the the value *) else if (List.mem name captured_name_list) then (* replace references to fold accumulator as lhs *) - ok @@ e_accessor (e_variable "_COMPILER_acc") [Access_record name] + ok @@ e_accessor (e_variable "#COMPILER#acc") [Access_record name] else ok @@ exp | None -> if ( name = fc.var.value ) then ok @@ k' (* replace references to the key *) else if (List.mem name captured_name_list) then (* replace references to fold accumulator as lhs *) - ok @@ e_accessor (e_variable "_COMPILER_acc") [Access_record name] + ok @@ e_accessor (e_variable "#COMPILER#acc") [Access_record name] else ok @@ exp ) (* loop on set or list *) | (Set _ | List _) -> if (name = fc.var.value ) then (* replace references to the collection element *) - ok @@ (e_variable "_COMPILER_collec_elt") + ok @@ (e_variable "#COMPILER#collec_elt") else if (List.mem name captured_name_list) then (* replace references to fold accumulator as lhs *) - ok @@ e_accessor (e_variable "_COMPILER_acc") [Access_record name] + ok @@ e_accessor (e_variable "#COMPILER#acc") [Access_record name] else ok @@ exp ) | _ -> ok @@ exp in let%bind for_body = Self_ast_simplified.map_expression replace for_body in - (* append the return value (the accumulator) to the for body *) + (* STEP 5 *) let rec add_return (expr : expression) = match expr.expression with | E_sequence (a,b) -> e_sequence a (add_return b) - | _ -> e_sequence expr (e_variable "_COMPILER_acc") in + | _ -> e_sequence expr (e_variable "#COMPILER#acc") in let for_body = add_return for_body in - (* prepend for body with args declaration (accumulator and collection elements *) + (* STEP 6 *) let%bind elt_type = simpl_type_expression fc.elt_type in let for_body = let ( arg_access: Types.access_path -> expression ) = e_accessor (e_variable "arguments") in @@ -1081,35 +1162,35 @@ and simpl_for_collect : Raw.for_collect -> (_ -> expression result) result = fun let acc = arg_access [Access_tuple 0 ; Access_tuple 0] in let collec_elt_v = arg_access [Access_tuple 1 ; Access_tuple 0] in let collec_elt_k = arg_access [Access_tuple 1 ; Access_tuple 1] in - e_let_in ("_COMPILER_acc", None) acc @@ - e_let_in ("_COMPILER_collec_elt_k", None) collec_elt_v @@ - e_let_in ("_COMPILER_collec_elt_v", None) collec_elt_k (for_body) + e_let_in ("#COMPILER#acc", None) acc @@ + e_let_in ("#COMPILER#collec_elt_k", None) collec_elt_v @@ + e_let_in ("#COMPILER#collec_elt_v", None) collec_elt_k (for_body) | _ -> let acc = arg_access [Access_tuple 0] in let collec_elt = arg_access [Access_tuple 1] in - e_let_in ("_COMPILER_acc", None) acc @@ - e_let_in ("_COMPILER_collec_elt", Some elt_type) collec_elt (for_body) + e_let_in ("#COMPILER#acc", None) acc @@ + e_let_in ("#COMPILER#collec_elt", Some elt_type) collec_elt (for_body) ) in - (* build the X_FOLD constant *) + (* STEP 7 *) let%bind collect = simpl_expression fc.expr in let lambda = e_lambda "arguments" None None for_body in let op_name = match fc.collection with | Map _ -> "MAP_FOLD" | Set _ -> "SET_FOLD" | List _ -> "LIST_FOLD" in let fold = e_constant op_name [collect ; init_record ; lambda] in - (* build sequence to re-assign fold result to the original captured variables *) + (* STEP 8 *) let assign_back (prev : expression option) (captured_varname : string) : expression option = - let access = e_accessor (e_variable "_COMPILER_folded_record") + let access = e_accessor (e_variable "#COMPILER#folded_record") [Access_record captured_varname] in let assign = e_assign captured_varname [] access in match prev with | None -> Some assign | Some p -> Some (e_sequence p assign) in let reassign_sequence = List.fold_left assign_back None captured_name_list in - (* attach the folded record to the re-assign sequence *) + (* STEP 9 *) let final_sequence = match reassign_sequence with (* None case means that no variables were captured *) - | None -> e_let_in ("_COMPILER_folded_record", None) fold (e_skip ()) - | Some seq -> e_let_in ("_COMPILER_folded_record", None) fold seq in + | None -> e_let_in ("#COMPILER#folded_record", None) fold (e_skip ()) + | Some seq -> e_let_in ("#COMPILER#folded_record", None) fold seq in return_statement @@ final_sequence let simpl_program : Raw.ast -> program result = fun t -> From 37570c6a40351ea1e901e64a4a26bdc3f4b83a14 Mon Sep 17 00:00:00 2001 From: Lesenechal Remi Date: Mon, 28 Oct 2019 18:43:55 +0100 Subject: [PATCH 23/30] clean test --- src/test/contracts/loop.ligo | 19 ------------------- 1 file changed, 19 deletions(-) diff --git a/src/test/contracts/loop.ligo b/src/test/contracts/loop.ligo index f559c2816..10137c07a 100644 --- a/src/test/contracts/loop.ligo +++ b/src/test/contracts/loop.ligo @@ -24,25 +24,6 @@ function for_sum (var n : nat) : int is block { end } with acc - -function lamby (var accu : (record st : string ; acc : int end) ; var i : int ) - : (record st : string ; acc : int end) is block { - accu.acc := accu.acc + i ; - accu.st := accu.st ^ "to" ; -} with accu - -function for_collection_ (var nee : unit; var nuu : unit) : (int * string) is block { - var acc : int := 0 ; - var st : string := "to" ; - var mylist : list(int) := list 1 ; 1 ; 1 end ; - var init_record : (record st : string; acc : int end ) := - record st = st; acc = acc; end; - var folded_record : (record st : string; acc : int end ) := - list_fold(mylist , init_record , lamby) ; - st := folded_record.st ; - acc := folded_record.acc ; -} with (folded_record.acc , folded_record.st) - function for_collection_list (var nee : unit) : (int * string) is block { var acc : int := 0 ; var st : string := "to" ; From e77f3e4903d050de10c554aed900ea39ca61d401 Mon Sep 17 00:00:00 2001 From: Lesenechal Remi Date: Mon, 28 Oct 2019 18:53:40 +0100 Subject: [PATCH 24/30] empty for collection loop --- src/passes/2-simplify/pascaligo.ml | 2 +- src/test/contracts/loop.ligo | 21 +++++++++++++++++++++ src/test/integration_tests.ml | 5 +++++ 3 files changed, 27 insertions(+), 1 deletion(-) diff --git a/src/passes/2-simplify/pascaligo.ml b/src/passes/2-simplify/pascaligo.ml index ec38004b3..a7314317d 100644 --- a/src/passes/2-simplify/pascaligo.ml +++ b/src/passes/2-simplify/pascaligo.ml @@ -1189,7 +1189,7 @@ and simpl_for_collect : Raw.for_collect -> (_ -> expression result) result = fun (* STEP 9 *) let final_sequence = match reassign_sequence with (* None case means that no variables were captured *) - | None -> e_let_in ("#COMPILER#folded_record", None) fold (e_skip ()) + | None -> e_skip () | Some seq -> e_let_in ("#COMPILER#folded_record", None) fold seq in return_statement @@ final_sequence diff --git a/src/test/contracts/loop.ligo b/src/test/contracts/loop.ligo index 10137c07a..7aaa4d7eb 100644 --- a/src/test/contracts/loop.ligo +++ b/src/test/contracts/loop.ligo @@ -46,6 +46,27 @@ function for_collection_set (var nee : unit) : (int * string) is block { end } with (acc, st) +// function for_collection_assignements_in_ifs (var nee : unit) : int is block { +// var acc : int := 0 ; +// var myset : set(int) := set 1 ; 2 ; 3 end ; +// for x : int in set myset +// begin +// if (x=1) then +// acc := acc + x ; +// else +// acc := acc + 10 ; +// end +// } with acc + +function for_collection_empty (var nee : unit) : int is block { + var acc : int := 0 ; + var myset : set(int) := set 1 ; 2 ; 3 end ; + for x : int in set myset + begin + skip ; + end +} with acc + // function for_collection_map (var nee : unit) : (int * string) is block { // var acc : int := 0 ; // var st : string := "" ; diff --git a/src/test/integration_tests.ml b/src/test/integration_tests.ml index 3ed6d871e..26a1fcc63 100644 --- a/src/test/integration_tests.ml +++ b/src/test/integration_tests.ml @@ -674,6 +674,11 @@ let loop () : unit result = let expected = e_pair (e_int 6) (e_string "totototo") in expect_eq program "for_collection_set" input expected in + let%bind () = + let input = e_unit () in + let expected = (e_int 0) in + expect_eq program "for_collection_empty" input expected + in ok () (* Don't know how to assert parse error happens in this test framework From ba00db2b4cf3e2b9b3af22ed97deb0f2284262a2 Mon Sep 17 00:00:00 2001 From: Lesenechal Remi Date: Tue, 29 Oct 2019 10:43:38 +0100 Subject: [PATCH 25/30] add self_ast_simplified fold_expression --- src/passes/3-self_ast_simplified/helpers.ml | 87 ++++++++++++++++++- .../self_ast_simplified.ml | 2 + 2 files changed, 88 insertions(+), 1 deletion(-) diff --git a/src/passes/3-self_ast_simplified/helpers.ml b/src/passes/3-self_ast_simplified/helpers.ml index 0793e8420..04b641f87 100644 --- a/src/passes/3-self_ast_simplified/helpers.ml +++ b/src/passes/3-self_ast_simplified/helpers.ml @@ -1,8 +1,93 @@ open Ast_simplified open Trace -type mapper = expression -> expression result +type 'a folder = 'a -> expression -> 'a result +let rec fold_expression : 'a folder -> 'a -> expression -> 'a result = fun f init e -> + let self = fold_expression f in + let%bind init' = f init e in + match e.expression with + | E_literal _ | E_variable _ | E_skip -> ok init' + | E_list lst | E_set lst | E_tuple lst | E_constant (_ , lst) -> ( + let%bind res' = bind_fold_list self init' lst in + ok res' + ) + | E_map lst | E_big_map lst -> ( + let%bind res' = bind_fold_list (bind_fold_pair self) init' lst in + ok res' + ) + | E_look_up ab | E_sequence ab | E_loop ab | E_application ab -> ( + let%bind res' = bind_fold_pair self init' ab in + ok res' + ) + | E_lambda { binder = _ ; input_type = _ ; output_type = _ ; result = e } + | E_annotation (e , _) | E_constructor (_ , e) -> ( + let%bind res' = self init' e in + ok res' + ) + | E_assign (_ , path , e) | E_accessor (e , path) -> ( + let%bind res' = fold_path f init' path in + let%bind res' = self res' e in + ok res' + ) + | E_matching (e , cases) -> ( + let%bind res = self init' e in + let%bind res = fold_cases f res cases in + ok res + ) + | E_record m -> ( + let aux init'' _ expr = + let%bind res' = fold_expression self init'' expr in + ok res' + in + let%bind res = bind_fold_smap aux (ok init') m in + ok res + ) + | E_let_in { binder = _ ; rhs ; result } -> ( + let%bind res = self init' rhs in + let%bind res = self res result in + ok res + ) +and fold_path : 'a folder -> 'a -> access_path -> 'a result = fun f init p -> bind_fold_list (fold_access f) init p + +and fold_access : 'a folder -> 'a -> access -> 'a result = fun f init a -> + match a with + | Access_map e -> ( + let%bind e' = fold_expression f init e in + ok e' + ) + | _ -> ok init + +and fold_cases : 'a folder -> 'a -> matching_expr -> 'a result = fun f init m -> + match m with + | Match_bool { match_true ; match_false } -> ( + let%bind res = fold_expression f init match_true in + let%bind res = fold_expression f res match_false in + ok res + ) + | Match_list { match_nil ; match_cons = (_ , _ , cons) } -> ( + let%bind res = fold_expression f init match_nil in + let%bind res = fold_expression f res cons in + ok res + ) + | Match_option { match_none ; match_some = (_ , some) } -> ( + let%bind res = fold_expression f init match_none in + let%bind res = fold_expression f res some in + ok res + ) + | Match_tuple (_ , e) -> ( + let%bind res = fold_expression f init e in + ok res + ) + | Match_variant lst -> ( + let aux init' ((_ , _) , e) = + let%bind res' = fold_expression f init' e in + ok res' in + let%bind res = bind_fold_list aux init lst in + ok res + ) + +type mapper = expression -> expression result let rec map_expression : mapper -> expression -> expression result = fun f e -> let self = map_expression f in let%bind e' = f e in diff --git a/src/passes/3-self_ast_simplified/self_ast_simplified.ml b/src/passes/3-self_ast_simplified/self_ast_simplified.ml index b73113cdb..a1ce4b580 100644 --- a/src/passes/3-self_ast_simplified/self_ast_simplified.ml +++ b/src/passes/3-self_ast_simplified/self_ast_simplified.ml @@ -23,3 +23,5 @@ let all_expression = bind_chain all_p let map_expression = Helpers.map_expression + +let fold_expression = Helpers.fold_expression From e86c92bc3bb67a2e21935b8fbcd9a26696cd3ace Mon Sep 17 00:00:00 2001 From: Lesenechal Remi Date: Tue, 29 Oct 2019 11:41:59 +0100 Subject: [PATCH 26/30] improving simplifier --- src/passes/2-simplify/pascaligo.ml | 80 +++++++++++------------------- 1 file changed, 29 insertions(+), 51 deletions(-) diff --git a/src/passes/2-simplify/pascaligo.ml b/src/passes/2-simplify/pascaligo.ml index a7314317d..c73fd67a3 100644 --- a/src/passes/2-simplify/pascaligo.ml +++ b/src/passes/2-simplify/pascaligo.ml @@ -1029,9 +1029,7 @@ and simpl_for_int : Raw.for_int -> (_ -> expression result) result = fun fi -> ``` We are performing the following steps: - 1) Filtering out of the body all the constructions that can't - alter the environment (assignements and map/set patches) - and simplifying only those. + 1) Simplifying the for body using ̀simpl_block` 2) Detect the free variables and build a list of their names (myint and myst in the previous example) @@ -1074,76 +1072,56 @@ and simpl_for_int : Raw.for_int -> (_ -> expression result) result = fun fi -> **) and simpl_for_collect : Raw.for_collect -> (_ -> expression result) result = fun fc -> match fc.collection with | Map _ -> fail @@ unsupported_for_collect_map fc.block | _ -> - let statements = npseq_to_list fc.block.value.statements in (* STEP 1 *) - let filter_assignments (el : Raw.statement) : Raw.instruction option = - match el with - | Raw.Instr (Assign _ as i) -> Some i - | _ -> None in - let assign_instrs = List.filter_map filter_assignments statements in - let%bind assign_instrs' = bind_map_list - (fun el -> - let%bind assign' = simpl_instruction el in - let%bind assign' = assign' None in - ok @@ assign') - assign_instrs in + let%bind for_body = simpl_block fc.block.value in + let%bind for_body = for_body None in (* STEP 2 *) - let captured_name_list = List.filter_map - (fun ass_exp -> + let%bind captured_name_list = Self_ast_simplified.fold_expression + (fun (prev : type_name list) (ass_exp : expression) -> match ass_exp.expression with - | E_assign ( name, _ , _ ) -> Some name - | _ -> None ) - assign_instrs' in + | E_assign ( name , _ , _ ) -> ok (name::prev) + | _ -> ok prev ) + [] + for_body in (* STEP 3 *) let add_to_record (prev: expression type_name_map) (captured_name: string) = SMap.add captured_name (e_variable captured_name) prev in let init_record = e_record (List.fold_left add_to_record SMap.empty captured_name_list) in (* STEP 4 *) - let%bind for_body = simpl_block fc.block.value in - let%bind for_body = for_body None in let replace exp = - (* TODO: map and set updated/remove must also be captured *) match exp.expression with (* replace references to fold accumulator as rhs *) | E_assign ( name , path , expr ) -> ( - match path with - | [] -> ok @@ e_assign "#COMPILER#acc" [Access_record name] expr - (* This fails for deep accesses, see LIGO-131 LIGO-134 *) - | _ -> - (* ok @@ e_assign "#COMPILER#acc" ((Access_record name)::path) expr) *) - fail @@ unsupported_deep_access_for_collection fc.block ) + match path with + | [] -> ok @@ e_assign "#COMPILER#acc" [Access_record name] expr + (* This fails for deep accesses, see LIGO-131 LIGO-134 *) + | _ -> + (* ok @@ e_assign "#COMPILER#acc" ((Access_record name)::path) expr) *) + fail @@ unsupported_deep_access_for_collection fc.block ) | E_variable name -> ( - match fc.collection with + if (List.mem name captured_name_list) then + (* replace references to fold accumulator as lhs *) + ok @@ e_accessor (e_variable "#COMPILER#acc") [Access_record name] + else match fc.collection with (* loop on map *) | Map _ -> let k' = e_variable "#COMPILER#collec_elt_k" in - let v' = e_variable "#COMPILER#collec_elt_v" in - ( match fc.bind_to with - | Some (_,v) -> - if ( name = fc.var.value ) then - ok @@ k' (* replace references to the the key *) - else if ( name = v.value ) then - ok @@ v' (* replace references to the the value *) - else if (List.mem name captured_name_list) then - (* replace references to fold accumulator as lhs *) - ok @@ e_accessor (e_variable "#COMPILER#acc") [Access_record name] - else ok @@ exp - | None -> - if ( name = fc.var.value ) then - ok @@ k' (* replace references to the key *) - else if (List.mem name captured_name_list) then - (* replace references to fold accumulator as lhs *) - ok @@ e_accessor (e_variable "#COMPILER#acc") [Access_record name] - else ok @@ exp + if ( name = fc.var.value ) then + ok @@ k' (* replace references to the the key *) + else ( + match fc.bind_to with + | Some (_,v) -> + let v' = e_variable "#COMPILER#collec_elt_v" in + if ( name = v.value ) then + ok @@ v' (* replace references to the the value *) + else ok @@ exp + | None -> ok @@ exp ) (* loop on set or list *) | (Set _ | List _) -> if (name = fc.var.value ) then (* replace references to the collection element *) ok @@ (e_variable "#COMPILER#collec_elt") - else if (List.mem name captured_name_list) then - (* replace references to fold accumulator as lhs *) - ok @@ e_accessor (e_variable "#COMPILER#acc") [Access_record name] else ok @@ exp ) | _ -> ok @@ exp in From c288f3c81e84767c133a7fe6bf3e80f18c8c289e Mon Sep 17 00:00:00 2001 From: Lesenechal Remi Date: Tue, 29 Oct 2019 11:56:21 +0100 Subject: [PATCH 27/30] simplify the simplifier and now find the free variables with a expression_fold --- src/passes/2-simplify/pascaligo.ml | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/passes/2-simplify/pascaligo.ml b/src/passes/2-simplify/pascaligo.ml index c73fd67a3..0200098ae 100644 --- a/src/passes/2-simplify/pascaligo.ml +++ b/src/passes/2-simplify/pascaligo.ml @@ -1132,7 +1132,6 @@ and simpl_for_collect : Raw.for_collect -> (_ -> expression result) result = fun | _ -> e_sequence expr (e_variable "#COMPILER#acc") in let for_body = add_return for_body in (* STEP 6 *) - let%bind elt_type = simpl_type_expression fc.elt_type in let for_body = let ( arg_access: Types.access_path -> expression ) = e_accessor (e_variable "arguments") in ( match fc.collection with @@ -1147,7 +1146,7 @@ and simpl_for_collect : Raw.for_collect -> (_ -> expression result) result = fun let acc = arg_access [Access_tuple 0] in let collec_elt = arg_access [Access_tuple 1] in e_let_in ("#COMPILER#acc", None) acc @@ - e_let_in ("#COMPILER#collec_elt", Some elt_type) collec_elt (for_body) + e_let_in ("#COMPILER#collec_elt", None) collec_elt (for_body) ) in (* STEP 7 *) let%bind collect = simpl_expression fc.expr in From fd901548af4f161977224f490aa16d6dccf3787b Mon Sep 17 00:00:00 2001 From: Lesenechal Remi Date: Tue, 29 Oct 2019 11:57:15 +0100 Subject: [PATCH 28/30] add more tests --- src/test/contracts/loop.ligo | 71 +++++++++++++++++++++++++++++------ src/test/integration_tests.ml | 45 +++++++++++++--------- 2 files changed, 88 insertions(+), 28 deletions(-) diff --git a/src/test/contracts/loop.ligo b/src/test/contracts/loop.ligo index 7aaa4d7eb..bbf887460 100644 --- a/src/test/contracts/loop.ligo +++ b/src/test/contracts/loop.ligo @@ -46,17 +46,66 @@ function for_collection_set (var nee : unit) : (int * string) is block { end } with (acc, st) -// function for_collection_assignements_in_ifs (var nee : unit) : int is block { -// var acc : int := 0 ; -// var myset : set(int) := set 1 ; 2 ; 3 end ; -// for x : int in set myset -// begin -// if (x=1) then -// acc := acc + x ; -// else -// acc := acc + 10 ; -// end -// } with acc +function for_collection_if_and_local_var (var nee : unit) : int is block { + var acc : int := 0 ; + const theone : int = 1 ; + var myset : set(int) := set 1 ; 2 ; 3 end ; + for x : int in set myset + begin + const thetwo : int = 2 ; + if (x=theone) then + acc := acc + x ; + else if (x=thetwo) then + acc := acc + thetwo ; + else + acc := acc + 10 ; + end +} with acc + +function for_collection_rhs_capture (var nee : unit) : int is block { + var acc : int := 0 ; + const mybigint : int = 1000 ; + var myset : set(int) := set 1 ; 2 ; 3 end ; + for x : int in set myset + begin + if (x=1) then + acc := acc + mybigint ; + else + acc := acc + 10 ; + end +} with acc + +function for_collection_proc_call (var nee : unit) : int is block { + var acc : int := 0 ; + var myset : set(int) := set 1 ; 2 ; 3 end ; + for x : int in set myset + begin + if (x=1) then + acc := acc + for_collection_rhs_capture(unit) ; + else + acc := acc + 10 ; + end +} with acc + +function for_collection_comp_with_acc (var nee : unit) : int is block { + var myint : int := 0 ; + var mylist : list(int) := list 1 ; 10 ; 15 end; + for x : int in list mylist + begin + if (x < myint) then skip ; + else myint := myint + 10 ; + end +} with myint + +function for_collection_with_patches (var nee : unit) : map(string,int) is block { + var myint : int := 12 ; + var mylist : list(string) := list "I" ; "am" ; "foo" end; + var mymap : map(string,int) := map end; + for x : string in list mylist + begin + patch mymap with map [ x -> myint ]; + end +} with mymap function for_collection_empty (var nee : unit) : int is block { var acc : int := 0 ; diff --git a/src/test/integration_tests.ml b/src/test/integration_tests.ml index 26a1fcc63..734b28dba 100644 --- a/src/test/integration_tests.ml +++ b/src/test/integration_tests.ml @@ -647,38 +647,49 @@ let loop () : unit result = let%bind () = let make_input = e_nat in let make_expected = e_nat in - expect_eq_n_pos program "dummy" make_input make_expected - in + expect_eq_n_pos program "dummy" make_input make_expected in let%bind () = let make_input = e_nat in let make_expected = e_nat in - expect_eq_n_pos_mid program "counter" make_input make_expected - in + expect_eq_n_pos_mid program "counter" make_input make_expected in let%bind () = let make_input = e_nat in let make_expected = fun n -> e_nat (n * (n + 1) / 2) in - expect_eq_n_pos_mid program "while_sum" make_input make_expected - in + expect_eq_n_pos_mid program "while_sum" make_input make_expected in let%bind () = let make_input = e_nat in let make_expected = fun n -> e_int (n * (n + 1) / 2) in - expect_eq_n_pos_mid program "for_sum" make_input make_expected - in + expect_eq_n_pos_mid program "for_sum" make_input make_expected in + let input = e_unit () in let%bind () = - let input = e_unit () in let expected = e_pair (e_int 3) (e_string "totototo") in - expect_eq program "for_collection_list" input expected - in + expect_eq program "for_collection_list" input expected in let%bind () = - let input = e_unit () in let expected = e_pair (e_int 6) (e_string "totototo") in - expect_eq program "for_collection_set" input expected - in + expect_eq program "for_collection_set" input expected in let%bind () = - let input = e_unit () in let expected = (e_int 0) in - expect_eq program "for_collection_empty" input expected - in + expect_eq program "for_collection_empty" input expected in + let%bind () = + let expected = (e_int 13) in + expect_eq program "for_collection_if_and_local_var" input expected in + let%bind () = + let expected = (e_int 1020) in + expect_eq program "for_collection_rhs_capture" input expected in + let%bind () = + let expected = (e_int 1040) in + expect_eq program "for_collection_proc_call" input expected in + let%bind () = + let expected = (e_int 20) in + expect_eq program "for_collection_comp_with_acc" input expected in + let%bind () = + let ez lst = + let open Ast_simplified.Combinators in + let lst' = List.map (fun (x, y) -> e_string x, e_int y) lst in + e_typed_map lst' t_string t_int + in + let expected = ez [ ("I" , 12) ; ("am" , 12) ; ("foo" , 12) ] in + expect_eq program "for_collection_with_patches" input expected in ok () (* Don't know how to assert parse error happens in this test framework From 402d849cec742c408fe9ddbb7c3d3f3d38e94257 Mon Sep 17 00:00:00 2001 From: Lesenechal Remi Date: Tue, 29 Oct 2019 15:43:00 +0100 Subject: [PATCH 29/30] use intermediary tuple access to get key and value for maps. add tests. --- src/passes/2-simplify/pascaligo.ml | 21 ++++++++------------- src/test/contracts/loop.ligo | 29 +++++++++++++++++++---------- src/test/integration_tests.ml | 6 ++++++ 3 files changed, 33 insertions(+), 23 deletions(-) diff --git a/src/passes/2-simplify/pascaligo.ml b/src/passes/2-simplify/pascaligo.ml index 0200098ae..54b2c2207 100644 --- a/src/passes/2-simplify/pascaligo.ml +++ b/src/passes/2-simplify/pascaligo.ml @@ -138,16 +138,6 @@ module Errors = struct ] in error ~data title message - let unsupported_for_collect_map for_col = - let title () = "for loop over map" in - let message () = - Format.asprintf "for loops over map are not supported yet" in - let data = [ - ("loop_loc", - fun () -> Format.asprintf "%a" Location.pp_lift @@ for_col.Region.region) - ] in - error ~data title message - (* Logging *) let simplifying_instruction t = @@ -1071,7 +1061,6 @@ and simpl_for_int : Raw.for_int -> (_ -> expression result) result = fun fi -> **) and simpl_for_collect : Raw.for_collect -> (_ -> expression result) result = fun fc -> - match fc.collection with | Map _ -> fail @@ unsupported_for_collect_map fc.block | _ -> (* STEP 1 *) let%bind for_body = simpl_block fc.block.value in let%bind for_body = for_body None in @@ -1136,10 +1125,16 @@ and simpl_for_collect : Raw.for_collect -> (_ -> expression result) result = fun let ( arg_access: Types.access_path -> expression ) = e_accessor (e_variable "arguments") in ( match fc.collection with | Map _ -> - let acc = arg_access [Access_tuple 0 ; Access_tuple 0] in + (* let acc = arg_access [Access_tuple 0 ; Access_tuple 0] in let collec_elt_v = arg_access [Access_tuple 1 ; Access_tuple 0] in - let collec_elt_k = arg_access [Access_tuple 1 ; Access_tuple 1] in + let collec_elt_k = arg_access [Access_tuple 1 ; Access_tuple 1] in *) + (* The above should work, but not yet (see LIGO-131) *) + let temp_kv = arg_access [Access_tuple 1] in + let acc = arg_access [Access_tuple 0] in + let collec_elt_v = e_accessor (e_variable "#COMPILER#temp_kv") [Access_tuple 0] in + let collec_elt_k = e_accessor (e_variable "#COMPILER#temp_kv") [Access_tuple 1] in e_let_in ("#COMPILER#acc", None) acc @@ + e_let_in ("#COMPILER#temp_kv", None) temp_kv @@ e_let_in ("#COMPILER#collec_elt_k", None) collec_elt_v @@ e_let_in ("#COMPILER#collec_elt_v", None) collec_elt_k (for_body) | _ -> diff --git a/src/test/contracts/loop.ligo b/src/test/contracts/loop.ligo index bbf887460..b873853b7 100644 --- a/src/test/contracts/loop.ligo +++ b/src/test/contracts/loop.ligo @@ -116,16 +116,25 @@ function for_collection_empty (var nee : unit) : int is block { end } with acc -// function for_collection_map (var nee : unit) : (int * string) is block { -// var acc : int := 0 ; -// var st : string := "" ; -// var mymap : map(string,int) := map "one" -> 1 ; "two" -> 2 ; "three" -> 3 end ; -// for k -> v : (string * int) in map mymap -// begin -// acc := acc + v ; -// st := k^st ; -// end -// } with (acc, st) +function for_collection_map_kv (var nee : unit) : (int * string) is block { + var acc : int := 0 ; + var st : string := "" ; + var mymap : map(string,int) := map "1" -> 1 ; "2" -> 2 ; "3" -> 3 end ; + for k -> v : (string * int) in map mymap + begin + acc := acc + v ; + st := st^k ; + end +} with (acc, st) + +function for_collection_map_k (var nee : unit) : string is block { + var st : string := "" ; + var mymap : map(string,int) := map "1" -> 1 ; "2" -> 2 ; "3" -> 3 end ; + for k : string in map mymap + begin + st := st^k ; + end +} with st function dummy (const n : nat) : nat is block { while (False) block { skip } diff --git a/src/test/integration_tests.ml b/src/test/integration_tests.ml index 734b28dba..8a644d1b2 100644 --- a/src/test/integration_tests.ml +++ b/src/test/integration_tests.ml @@ -667,6 +667,12 @@ let loop () : unit result = let%bind () = let expected = e_pair (e_int 6) (e_string "totototo") in expect_eq program "for_collection_set" input expected in + let%bind () = + let expected = e_pair (e_int 6) (e_string "123") in + expect_eq program "for_collection_map_kv" input expected in + let%bind () = + let expected = (e_string "123") in + expect_eq program "for_collection_map_k" input expected in let%bind () = let expected = (e_int 0) in expect_eq program "for_collection_empty" input expected in From a140e123949ea653a7d9d19cd0031bed31f497f7 Mon Sep 17 00:00:00 2001 From: Lesenechal Remi Date: Tue, 29 Oct 2019 16:32:28 +0100 Subject: [PATCH 30/30] add test for nested for collection loops (not supported yet) --- src/passes/2-simplify/pascaligo.ml | 6 +++++- src/test/contracts/loop.ligo | 15 +++++++++++++++ src/test/integration_tests.ml | 3 +++ 3 files changed, 23 insertions(+), 1 deletion(-) diff --git a/src/passes/2-simplify/pascaligo.ml b/src/passes/2-simplify/pascaligo.ml index 54b2c2207..4dee47dec 100644 --- a/src/passes/2-simplify/pascaligo.ml +++ b/src/passes/2-simplify/pascaligo.ml @@ -1068,7 +1068,11 @@ and simpl_for_collect : Raw.for_collect -> (_ -> expression result) result = fun let%bind captured_name_list = Self_ast_simplified.fold_expression (fun (prev : type_name list) (ass_exp : expression) -> match ass_exp.expression with - | E_assign ( name , _ , _ ) -> ok (name::prev) + | E_assign ( name , _ , _ ) -> + if (String.contains name '#') then + ok prev + else + ok (name::prev) | _ -> ok prev ) [] for_body in diff --git a/src/test/contracts/loop.ligo b/src/test/contracts/loop.ligo index b873853b7..2f250cf18 100644 --- a/src/test/contracts/loop.ligo +++ b/src/test/contracts/loop.ligo @@ -136,6 +136,21 @@ function for_collection_map_k (var nee : unit) : string is block { end } with st +// function nested_for_collection (var nee : unit) : (int*string) is block { +// var myint : int := 0; +// var myst : string := ""; +// var mylist : list(int) := list 1 ; 2 ; 3 end ; +// for i : int in list mylist +// begin +// myint := myint + i ; +// var myset : set(string) := set "1" ; "2" ; "3" end ; +// for st : string in set myset +// begin +// myst := myst ^ st ; +// end +// end +// } with (myint,myst) + function dummy (const n : nat) : nat is block { while (False) block { skip } } with n diff --git a/src/test/integration_tests.ml b/src/test/integration_tests.ml index 8a644d1b2..10f4d4d06 100644 --- a/src/test/integration_tests.ml +++ b/src/test/integration_tests.ml @@ -688,6 +688,9 @@ let loop () : unit result = let%bind () = let expected = (e_int 20) in expect_eq program "for_collection_comp_with_acc" input expected in + (* let%bind () = + let expected = e_pair (e_int 6) (e_string "123123123") in + expect_eq program "nested_for_collection" input expected in *) let%bind () = let ez lst = let open Ast_simplified.Combinators in