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

merge step and down reemoval

Browse Source 
WIP

WIP
This commit is contained in:
Lesenechal Remi 2019-10-22 12:12:19 +02:00
parent 536b5648c8
commit 730c130fb3
3 changed files with 60 additions and 67 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

52
src/passes/2-simplify/pascaligo.ml
View File

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

58
src/test/contracts/loop.ligo
View File

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

17
src/test/integration_tests.ml
View File

@ -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 ()