modifying doc and test for loops (Cameligo and pascaligo)

This commit is contained in:
Pierre-Emmanuel Wulfman 2020-03-09 00:13:07 +01:00
parent fa5983e9d3
commit c46002b160
9 changed files with 124 additions and 111 deletions

View File

@ -57,45 +57,21 @@ constant, therefore it makes no sense in CameLIGO to feature loops,
which we understand as syntactic constructs where the state of a
stopping condition is mutated, as with "while" loops in PascaLIGO.
Instead, CameLIGO implements a *folded operation* by means of a
predefined function named `Loop.fold_while`. It takes an initial value
of a certain type, called an *accumulator*, and repeatedly calls a
given function, called *folded function*, that takes that
accumulator and returns the next value of the accumulator, until a
condition is met and the fold stops with the final value of the
accumulator. The iterated function needs to have a special type: if
the type of the accumulator is `t`, then it must have the type `bool *
t` (not simply `t`). It is the boolean value that denotes whether the
stopping condition has been reached.
Instead, CameLIGO loops are written by means of a tail recursive function
Here is how to compute the greatest common divisors of two natural
numbers by means of Euclid's algorithm:
```cameligo group=a
let iter (x,y : nat * nat) : bool * (nat * nat) =
if y = 0n then false, (x,y) else true, (y, x mod y)
let rec iter (x,y : nat * nat) : nat =
if y = 0n then x else iter (y, x mod y)
let gcd (x,y : nat * nat) : nat =
let x,y = if x < y then y,x else x,y in
let x,y = Loop.fold_while iter (x,y)
in x
iter (x,y)
```
To ease the writing and reading of the iterated functions (here,
`iter`), two predefined functions are provided: `Loop.resume` and
`Loop.stop`:
```cameligo group=a
let iter (x,y : nat * nat) : bool * (nat * nat) =
if y = 0n then Loop.stop (x,y) else Loop.resume (y, x mod y)
let gcd (x,y : nat * nat) : nat =
let x,y = if x < y then y,x else x,y in
let x,y = Loop.fold_while iter (x,y)
in x
```
> Note that `stop` and `continue` (now `Loop.resume`) are
> Note that `fold_while`, `stop` and `continue` (now `Loop.resume`) are
> *deprecated*.
You can call the function `gcd` defined above using the LIGO compiler
@ -114,47 +90,22 @@ constant, therefore it makes no sense in ReasonLIGO to feature loops,
which we understand as syntactic constructs where the state of a
stopping condition is mutated, as with "while" loops in PascaLIGO.
Instead, ReasonLIGO features a *fold operation* as a predefined
function named `Loop.fold_while`. It takes an initial value of a
certain type, called an *accumulator*, and repeatedly calls a given
function, called *iterated function*, that takes that accumulator and
returns the next value of the accumulator, until a condition is met
and the fold stops with the final value of the accumulator. The
iterated function needs to have a special type: if the type of the
accumulator is `t`, then it must have the type `bool * t` (not simply
`t`). It is the boolean value that denotes whether the stopping
condition has been reached.
Instead, ReasonLIGO loops are written by means of tail recursive functions
Here is how to compute the greatest common divisors of two natural
numbers by means of Euclid's algorithm:
```reasonligo group=a
let iter = ((x,y) : (nat, nat)) : (bool, (nat, nat)) =>
if (y == 0n) { (false, (x,y)); } else { (true, (y, x mod y)); };
let rec iter = ((x,y) : (nat, nat)) : nat =>
if (y == 0n) { x; } else { iter ((y, x mod y)); };
let gcd = ((x,y) : (nat, nat)) : nat => {
let (x,y) = if (x < y) { (y,x); } else { (x,y); };
let (x,y) = Loop.fold_while (iter, (x,y));
x
iter ((x,y))
};
```
To ease the writing and reading of the iterated functions (here,
`iter`), two predefined functions are provided: `Loop.resume` and
`Loop.stop`:
```reasonligo group=b
let iter = ((x,y) : (nat, nat)) : (bool, (nat, nat)) =>
if (y == 0n) { Loop.stop ((x,y)); } else { Loop.resume ((y, x mod y)); };
let gcd = ((x,y) : (nat, nat)) : nat => {
let (x,y) = if (x < y) { (y,x); } else { (x,y); };
let (x,y) = Loop.fold_while (iter, (x,y));
x
};
```
> Note that `stop` and `continue` (now `Loop.resume`) are
> Note that `fold_while`, `stop` and `continue` (now `Loop.resume`) are
> *deprecated*.
</Syntax>

View File

@ -1174,7 +1174,7 @@ let%expect_test _ =
let%expect_test _ =
run_ligo_bad [ "compile-contract" ; bad_contract "create_contract_toplevel.mligo" ; "main" ] ;
[%expect {|
ligo: in file "create_contract_toplevel.mligo", line 4, character 35 to line 8, character 8. No free variable allowed in this lambda: variable 'store' {"expression":"CREATE_CONTRACT(lambda (#P:Some(( nat * string ))) : None return let rhs#810 = #P in let p = rhs#810.0 in let s = rhs#810.1 in ( list[] : (TO_list(operation)) , store ) , NONE() : (TO_option(key_hash)) , 300000000mutez , \"un\")","location":"in file \"create_contract_toplevel.mligo\", line 4, character 35 to line 8, character 8"}
ligo: in file "create_contract_toplevel.mligo", line 4, character 35 to line 8, character 8. No free variable allowed in this lambda: variable 'store' {"expression":"CREATE_CONTRACT(lambda (#P:Some(( nat * string ))) : None return let rhs#808 = #P in let p = rhs#808.0 in let s = rhs#808.1 in ( list[] : (TO_list(operation)) , store ) , NONE() : (TO_option(key_hash)) , 300000000mutez , \"un\")","location":"in file \"create_contract_toplevel.mligo\", line 4, character 35 to line 8, character 8"}
If you're not sure how to fix this error, you can
@ -1187,7 +1187,7 @@ ligo: in file "create_contract_toplevel.mligo", line 4, character 35 to line 8,
run_ligo_bad [ "compile-contract" ; bad_contract "create_contract_var.mligo" ; "main" ] ;
[%expect {|
ligo: in file "create_contract_var.mligo", line 6, character 35 to line 10, character 5. No free variable allowed in this lambda: variable 'a' {"expression":"CREATE_CONTRACT(lambda (#P:Some(( nat * int ))) : None return let rhs#813 = #P in let p = rhs#813.0 in let s = rhs#813.1 in ( list[] : (TO_list(operation)) , a ) , NONE() : (TO_option(key_hash)) , 300000000mutez , 1)","location":"in file \"create_contract_var.mligo\", line 6, character 35 to line 10, character 5"}
ligo: in file "create_contract_var.mligo", line 6, character 35 to line 10, character 5. No free variable allowed in this lambda: variable 'a' {"expression":"CREATE_CONTRACT(lambda (#P:Some(( nat * int ))) : None return let rhs#811 = #P in let p = rhs#811.0 in let s = rhs#811.1 in ( list[] : (TO_list(operation)) , a ) , NONE() : (TO_option(key_hash)) , 300000000mutez , 1)","location":"in file \"create_contract_var.mligo\", line 6, character 35 to line 10, character 5"}
If you're not sure how to fix this error, you can

View File

@ -345,7 +345,7 @@ let rec simpl_expression :
trace (simplifying_expr t) @@
match t with
Raw.ELetIn e ->
let Raw.{binding; body; attributes; _} = e.value in
let Raw.{kwd_rec; binding; body; attributes; _} = e.value in
let inline = List.exists (fun (a: Raw.attribute) -> a.value = "inline") attributes in
let Raw.{binders; lhs_type; let_rhs; _} = binding in
begin match binders with
@ -393,10 +393,50 @@ let rec simpl_expression :
(chain_let_in tl body)
| [] -> body (* Precluded by corner case assertion above *)
in
if List.length prep_vars = 1
then ok (chain_let_in prep_vars body)
(* Bind the right hand side so we only evaluate it once *)
else ok (e_let_in (rhs_b, ty_opt) false inline rhs' (chain_let_in prep_vars body))
let%bind ty_opt = match ty_opt with
| None -> (match let_rhs with
| EFun {value={binders;lhs_type}} ->
let f_args = nseq_to_list (binders) in
let%bind lhs_type' = bind_map_option (fun x -> simpl_type_expression (snd x)) lhs_type in
let%bind ty = bind_map_list typed_pattern_to_typed_vars f_args in
let aux acc ty = Option.map (t_function (snd ty)) acc in
ok @@ (List.fold_right' aux lhs_type' ty)
| _ -> ok None
)
| Some t -> ok @@ Some t
in
let%bind ret_expr = if List.length prep_vars = 1
then ok (chain_let_in prep_vars body)
(* Bind the right hand side so we only evaluate it once *)
else ok (e_let_in (rhs_b, ty_opt) false inline rhs' (chain_let_in prep_vars body))
in
let%bind ret_expr = match kwd_rec with
| None -> ok @@ ret_expr
| Some _ ->
match ret_expr.expression_content with
| E_let_in li -> (
let%bind lambda =
let rec aux rhs = match rhs.expression_content with
| E_lambda l -> ok @@ l
| E_ascription a -> aux a.anno_expr
| _ -> fail @@ corner_case "recursive only supported for lambda"
in
aux rhs'
in
let fun_name = fst @@ List.hd prep_vars in
let%bind fun_type = match ty_opt with
| Some t -> ok @@ t
| None -> match rhs'.expression_content with
| E_ascription a -> ok a.type_annotation
| _ -> fail @@ untyped_recursive_function e
in
let expression_content = E_recursive {fun_name;fun_type;lambda} in
let expression_content = E_let_in {li with rhs = {li.rhs with expression_content}} in
ok @@ {ret_expr with expression_content}
)
| _ -> fail @@ corner_case "impossible"
in
ok ret_expr
(* let f p1 ps... = rhs in body *)
| (f, p1 :: ps) ->
@ -670,7 +710,8 @@ and simpl_fun lamb' : expr result =
e_lambda ~loc (binder) (Some input_type) output_type (layer_arguments tl)
| [] -> body
in
return @@ layer_arguments params'
let ret_lamb = layer_arguments params' in
return @@ ret_lamb
and simpl_logic_expression ?te_annot (t:Raw.logic_expr) : expr result =

View File

@ -1263,11 +1263,12 @@ and simpl_for_int : Raw.for_int -> (_ -> expression result) result = fun fi ->
let%bind bound = simpl_expression fi.bound in
let cond = e_annotation (e_constant C_LE [var ; bound]) t_bool in
let step = e_int 1 in
let continue_expr = e_constant C_FOLD_CONTINUE [(e_variable binder)] in
let ctrl =
e_let_in (it,Some t_int) false false (e_constant C_ADD [ var ; step ])
(e_let_in (binder, None) false false (e_update (e_variable binder) "1" var)
(e_variable binder))
in
e_let_in (it,Some t_int) false false (e_constant C_ADD [ var ; step ]) @@
e_let_in (binder, None) false false (e_update (e_variable binder) "1" var)@@
continue_expr
in
(* Modify the body loop*)
let%bind for_body = simpl_block fi.block.value in
let%bind for_body = for_body @@ Some ctrl in
@ -1281,11 +1282,10 @@ and simpl_for_int : Raw.for_int -> (_ -> expression result) result = fun fi ->
let restore = fun expr -> List.fold_right aux captured_name_list expr in
(*Prep the lambda for the fold*)
let continue_expr = e_constant C_FOLD_CONTINUE [restore(for_body)] in
let stop_expr = e_constant C_FOLD_STOP [e_variable binder] in
let aux_func = e_lambda binder None None @@
e_let_in (it,Some t_int) false false (e_accessor (e_variable binder) "1") @@
e_cond cond continue_expr (stop_expr) in
e_cond cond (restore for_body) (stop_expr) in
(* Make the fold_while en precharge the vakye *)
let loop = e_constant C_FOLD_WHILE [aux_func; e_variable env_rec] in

View File

@ -102,6 +102,15 @@ them. please report this to the developers." in
] in
error ~data title content
let unsupported_recursive_function expression_variable =
let title () = "unsupported recursive function yet" in
let content () = "only fuction with one variable are supported" in
let data = [
("value" , fun () -> Format.asprintf "%a" AST.PP.expression_variable expression_variable) ;
] in
error ~data title content
end
open Errors
@ -521,12 +530,14 @@ and transpile_lambda l (input_type , output_type) =
ok @@ Combinators.Expression.make_tpl (closure , tv)
and transpile_recursive {fun_name; fun_type; lambda} =
let rec map_lambda : AST.expression_variable -> type_value -> AST.expression -> expression result = fun fun_name loop_type e ->
let rec map_lambda : AST.expression_variable -> type_value -> AST.expression -> (expression * expression_variable list) result = fun fun_name loop_type e ->
match e.expression_content with
E_lambda {binder;result} ->
let%bind body = map_lambda fun_name loop_type result in
ok @@ Expression.make (E_closure {binder;body}) loop_type|
_ -> replace_callback fun_name loop_type e
let%bind (body,l) = map_lambda fun_name loop_type result in
ok @@ (Expression.make (E_closure {binder;body}) loop_type, binder::l)
| _ ->
let%bind res = replace_callback fun_name loop_type e in
ok @@ (res, [])
and replace_callback : AST.expression_variable -> type_value -> AST.expression -> expression result = fun fun_name loop_type e ->
match e.expression_content with
@ -629,10 +640,13 @@ and transpile_recursive {fun_name; fun_type; lambda} =
let%bind fun_type = transpile_type fun_type in
let%bind (input_type,output_type) = get_t_function fun_type in
let loop_type = t_union (None, input_type) (None, output_type) in
let%bind body = map_lambda fun_name loop_type lambda.result in
let expr = Expression.make_tpl (E_variable fun_name, input_type) in
let%bind (body,binder) = map_lambda fun_name loop_type lambda.result in
let binder = lambda.binder::binder in
List.iter (Format.printf "inder %a\n%!" Var.pp) binder ;
let%bind binder = match binder with hd::[] -> ok @@ hd | _ -> fail @@ unsupported_recursive_function fun_name in
let expr = Expression.make_tpl (E_variable binder, input_type) in
let body = Expression.make (E_iterator (C_LOOP_LEFT, ((lambda.binder, loop_type),body), expr)) output_type in
ok @@ Expression.make (E_closure {binder=fun_name;body}) fun_type
ok @@ Expression.make (E_closure {binder;body}) fun_type
let transpile_declaration env (d:AST.declaration) : toplevel_statement result =
match d with

View File

@ -168,6 +168,17 @@ let get_t_function (t:type_expression) : (type_expression * type_expression) res
| T_arrow {type1;type2} -> ok (type1,type2)
| _ -> simple_fail "not a function"
let get_t_function_full (t:type_expression) : (type_expression * type_expression) result =
let%bind _ = get_t_function t in
let rec aux n t = match t.type_content with
| T_arrow {type1;type2} ->
let (l, o) = aux (n+1) type2 in
((Label (string_of_int n),type1)::l,o)
| _ -> ([],t)
in
let (input,output) = aux 0 t in
ok @@ (t_record (LMap.of_list input) (),output)
let get_t_sum (t:type_expression) : type_expression constructor_map result = match t.type_content with
| T_sum m -> ok m
| _ -> fail @@ Errors.not_a_x_type "sum" t ()

View File

@ -62,6 +62,7 @@ val get_t_key_hash : type_expression -> unit result
val get_t_tuple : type_expression -> type_expression list result
val get_t_pair : type_expression -> ( type_expression * type_expression ) result
val get_t_function : type_expression -> ( type_expression * type_expression ) result
val get_t_function_full : type_expression -> ( type_expression * type_expression ) result
val get_t_sum : type_expression -> type_expression constructor_map result
val get_t_record : type_expression -> type_expression label_map result
val get_t_map : type_expression -> ( type_expression * type_expression ) result

View File

@ -1,10 +1,9 @@
(* Test functional iterators in CameLIGO *)
let aux_simple (i : int) : bool * int =
if i < 100 then Loop.resume (i + 1) else Loop.stop i
let rec aux_simple (i : int) : int =
if i < 100 then aux_simple (i + 1) else i
let counter_simple (n : int) : int =
Loop.fold_while aux_simple n
let counter_simple (n : int) : int = aux_simple n
type sum_aggregator = {
counter : int;
@ -13,25 +12,23 @@ type sum_aggregator = {
let counter (n : int) : int =
let initial : sum_aggregator = {counter=0; sum=0} in
let aggregate = fun (prev : sum_aggregator) ->
let rec aggregate : sum_aggregator -> int = fun (prev: sum_aggregator) ->
if prev.counter <= n then
Loop.resume {counter = prev.counter + 1;
aggregate {counter = prev.counter + 1;
sum = prev.counter + prev.sum}
else
Loop.stop {counter = prev.counter; sum = prev.sum} in
let out : sum_aggregator =
Loop.fold_while aggregate initial
in out.sum
prev.sum
in
aggregate initial
let aux_nest (prev : sum_aggregator) : bool * sum_aggregator =
let rec aux_nest (prev : sum_aggregator) : int =
if prev.counter < 100 then
let sum : int =
prev.sum + Loop.fold_while aux_simple prev.counter
in Loop.resume {counter = prev.counter + 1; sum = sum}
let sum = prev.sum + (aux_simple prev.counter) in
aux_nest {counter = prev.counter + 1; sum = sum}
else
Loop.stop {counter = prev.counter; sum = prev.sum}
prev.sum
let counter_nest (n : int) : int =
let initial : sum_aggregator = {counter=0; sum=0} in
let out : sum_aggregator = Loop.fold_while aux_nest initial
in out.sum
let out = aux_nest initial
in out

View File

@ -1,9 +1,9 @@
/* Test loops in ReasonLIGO */
let aux_simple = (i : int) : (bool, int) =>
if (i < 100) { Loop.resume (i + 1); } else { Loop.stop (i); };
let rec aux_simple = (i : int) : int =>
if (i < 100) { aux_simple (i + 1); } else { i; };
let counter_simple = (n : int) : int => Loop.fold_while (aux_simple, n);
let counter_simple = (n : int) : int => aux_simple (n);
type sum_aggregator = {
counter : int,
@ -12,30 +12,28 @@ type sum_aggregator = {
let counter = (n : int) : int => {
let initial : sum_aggregator = {counter: 0, sum: 0};
let aggregate = (prev : sum_aggregator) =>
let rec aggregate = (prev : sum_aggregator):int =>
if (prev.counter <= n) {
Loop.resume ({counter : prev.counter + 1,
aggregate ({counter : prev.counter + 1,
sum : prev.counter + prev.sum});
} else {
Loop.stop ({counter: prev.counter, sum: prev.sum});
prev.sum;
};
let out : sum_aggregator =
Loop.fold_while (aggregate, initial);
out.sum;
aggregate (initial);
};
let aux_nest = (prev : sum_aggregator) : (bool, sum_aggregator) =>
let rec aux_nest = (prev : sum_aggregator) : sum_aggregator =>
if (prev.counter < 100) {
let sum : int =
prev.sum + Loop.fold_while (aux_simple, prev.counter);
Loop.resume ({counter: prev.counter + 1,
prev.sum + aux_simple (prev.counter);
aux_nest ({counter: prev.counter + 1,
sum: sum});
} else {
Loop.stop ({counter: prev.counter, sum: prev.sum});
({counter: prev.counter, sum: prev.sum});
};
let counter_nest = (n : int) : int => {
let initial : sum_aggregator = {counter: 0, sum: 0};
let out : sum_aggregator = Loop.fold_while (aux_nest, initial);
let out : sum_aggregator = aux_nest (initial);
out.sum;
};