Skip to content

Commit 6ef3281

Browse files
clarusclarus
authored
Merge pull request #336 from formal-land/guillaume-claret@fix-functions_closures.v
Handle the particular case of closure without parameters
2 parents 7db3cee + 7e8a2f2 commit 6ef3281

16 files changed

+223
-250
lines changed

‎CoqOfRust/blacklist.txt‎

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -50,7 +50,6 @@ examples/functions/functions_closures_forced_capturing_with_move.v
5050
examples/functions/functions_closures_input_functions.v
5151
examples/functions/functions_closures_type_anonymity_define_and_use.v
5252
examples/functions/functions_closures_type_anonymity_define.v
53-
examples/functions/functions_closures.v
5453
examples/functions/functions.v
5554
examples/functions/higher_order_functions.v
5655
examples/generics/generics_bounds.v

‎CoqOfRust/ink/erc20.v‎

Lines changed: 43 additions & 54 deletions
Original file line numberDiff line numberDiff line change
@@ -2179,57 +2179,52 @@ Module Impl_parity_scale_codec_codec_Decode_for_erc20_erc20___ink_EventBase.
21792179
| __codec_x_edqy =>
21802180
let* _ :=
21812181
let* α0 :=
2182-
(fun =>
2183-
let* __codec_res_edqy :=
2184-
(parity_scale_codec.codec.Decode.decode
2185-
(Self := erc20.erc20.Transfer))
2186-
__codec_input_edqy in
2187-
let* α0 :=
2188-
match __codec_res_edqy with
2189-
| core.result.Result.Err e =>
2190-
let* α0 :=
2191-
e.["chain"]
2192-
"Could not decode `__ink_EventBase::Transfer.0`" in
2193-
Return (core.result.Result.Err α0)
2194-
| core.result.Result.Ok __codec_res_edqy =>
2195-
Pure __codec_res_edqy
2196-
end in
2197-
Pure
2198-
(core.result.Result.Ok
2199-
(erc20.erc20.__ink_EventBase.Transfer α0))) in
2182+
let* __codec_res_edqy :=
2183+
(parity_scale_codec.codec.Decode.decode
2184+
(Self := erc20.erc20.Transfer))
2185+
__codec_input_edqy in
2186+
let* α0 :=
2187+
match __codec_res_edqy with
2188+
| core.result.Result.Err e =>
2189+
let* α0 :=
2190+
e.["chain"]
2191+
"Could not decode `__ink_EventBase::Transfer.0`" in
2192+
Return (core.result.Result.Err α0)
2193+
| core.result.Result.Ok __codec_res_edqy => Pure __codec_res_edqy
2194+
end in
2195+
Pure
2196+
(core.result.Result.Ok
2197+
(erc20.erc20.__ink_EventBase.Transfer α0)) in
22002198
Return α0 in
22012199
Pure tt
22022200
| __codec_x_edqy =>
22032201
let* _ :=
22042202
let* α0 :=
2205-
(fun =>
2206-
let* __codec_res_edqy :=
2207-
(parity_scale_codec.codec.Decode.decode
2208-
(Self := erc20.erc20.Approval))
2209-
__codec_input_edqy in
2210-
let* α0 :=
2211-
match __codec_res_edqy with
2212-
| core.result.Result.Err e =>
2213-
let* α0 :=
2214-
e.["chain"]
2215-
"Could not decode `__ink_EventBase::Approval.0`" in
2216-
Return (core.result.Result.Err α0)
2217-
| core.result.Result.Ok __codec_res_edqy =>
2218-
Pure __codec_res_edqy
2219-
end in
2220-
Pure
2221-
(core.result.Result.Ok
2222-
(erc20.erc20.__ink_EventBase.Approval α0))) in
2203+
let* __codec_res_edqy :=
2204+
(parity_scale_codec.codec.Decode.decode
2205+
(Self := erc20.erc20.Approval))
2206+
__codec_input_edqy in
2207+
let* α0 :=
2208+
match __codec_res_edqy with
2209+
| core.result.Result.Err e =>
2210+
let* α0 :=
2211+
e.["chain"]
2212+
"Could not decode `__ink_EventBase::Approval.0`" in
2213+
Return (core.result.Result.Err α0)
2214+
| core.result.Result.Ok __codec_res_edqy => Pure __codec_res_edqy
2215+
end in
2216+
Pure
2217+
(core.result.Result.Ok
2218+
(erc20.erc20.__ink_EventBase.Approval α0)) in
22232219
Return α0 in
22242220
Pure tt
22252221
| _ =>
22262222
let* _ :=
22272223
let* α0 :=
2228-
(fun =>
2229-
let* α0 :=
2230-
(core.convert.Into.into (Self := _))
2231-
"Could not decode `__ink_EventBase`, variant doesn't exist" in
2232-
Pure (core.result.Result.Err α0)) in
2224+
let* α0 :=
2225+
(core.convert.Into.into (Self := _))
2226+
"Could not decode `__ink_EventBase`, variant doesn't exist" in
2227+
Pure (core.result.Result.Err α0) in
22332228
Return α0 in
22342229
Pure tt
22352230
end.
@@ -7191,29 +7186,23 @@ Module Impl_parity_scale_codec_codec_Decode_for_erc20_erc20_Error.
71917186
| __codec_x_edqy =>
71927187
let* _ :=
71937188
let* α0 :=
7194-
(fun =>
7195-
Pure
7196-
(core.result.Result.Ok
7197-
erc20.erc20.Error.InsufficientBalance)) in
7189+
Pure (core.result.Result.Ok erc20.erc20.Error.InsufficientBalance) in
71987190
Return α0 in
71997191
Pure tt
72007192
| __codec_x_edqy =>
72017193
let* _ :=
72027194
let* α0 :=
7203-
(fun =>
7204-
Pure
7205-
(core.result.Result.Ok
7206-
erc20.erc20.Error.InsufficientAllowance)) in
7195+
Pure
7196+
(core.result.Result.Ok erc20.erc20.Error.InsufficientAllowance) in
72077197
Return α0 in
72087198
Pure tt
72097199
| _ =>
72107200
let* _ :=
72117201
let* α0 :=
7212-
(fun =>
7213-
let* α0 :=
7214-
(core.convert.Into.into (Self := _))
7215-
"Could not decode `Error`, variant doesn't exist" in
7216-
Pure (core.result.Result.Err α0)) in
7202+
let* α0 :=
7203+
(core.convert.Into.into (Self := _))
7204+
"Could not decode `Error`, variant doesn't exist" in
7205+
Pure (core.result.Result.Err α0) in
72177206
Return α0 in
72187207
Pure tt
72197208
end.

‎coq_translation/default/examples/error_handling/boxing_errors.v‎

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -86,8 +86,7 @@ Definition double_first
8686
(vec : alloc.vec.Vec (ref str) alloc.vec.Vec.Default.A)
8787
: M (H := H') (boxing_errors.Result i32) :=
8888
let* α0 := vec.["first"] in
89-
let* α1 :=
90-
α0.["ok_or_else"] (fun => boxing_errors.EmptyVec.Build.["into"]) in
89+
let* α1 := α0.["ok_or_else"] boxing_errors.EmptyVec.Build.["into"] in
9190
α1.["and_then"]
9291
(fun s =>
9392
let* α0 := s.["parse"] : M i32 in

‎coq_translation/default/examples/error_handling/unpacking_options_and_defaults_via_get_or_insert_with.v‎

Lines changed: 7 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -55,16 +55,15 @@ Definition main `{H' : State.Trait} : M (H := H') unit :=
5555
unpacking_options_and_defaults_via_get_or_insert_with.Fruit :=
5656
core.option.Option.None in
5757
let get_lemon_as_fallback :=
58-
fun =>
58+
let* _ :=
5959
let* _ :=
60-
let* _ :=
61-
let* α0 :=
62-
format_arguments::["new_const"]
63-
(addr_of [ "Providing lemon as fallback
60+
let* α0 :=
61+
format_arguments::["new_const"]
62+
(addr_of [ "Providing lemon as fallback
6463
" ]) in
65-
std.io.stdio._print α0 in
66-
Pure tt in
67-
Pure unpacking_options_and_defaults_via_get_or_insert_with.Fruit.Lemon in
64+
std.io.stdio._print α0 in
65+
Pure tt in
66+
Pure unpacking_options_and_defaults_via_get_or_insert_with.Fruit.Lemon in
6867
let* first_available_fruit :=
6968
my_fruit.["get_or_insert_with"] get_lemon_as_fallback in
7069
let* _ :=

‎coq_translation/default/examples/error_handling/unpacking_options_and_defaults_via_or_else.v‎

Lines changed: 18 additions & 20 deletions
Original file line numberDiff line numberDiff line change
@@ -49,31 +49,29 @@ Definition main `{H' : State.Trait} : M (H := H') unit :=
4949
core.option.Option unpacking_options_and_defaults_via_or_else.Fruit :=
5050
core.option.Option.None in
5151
let get_kiwi_as_fallback :=
52-
fun =>
52+
let* _ :=
5353
let* _ :=
54-
let* _ :=
55-
let* α0 :=
56-
format_arguments::["new_const"]
57-
(addr_of [ "Providing kiwi as fallback
54+
let* α0 :=
55+
format_arguments::["new_const"]
56+
(addr_of [ "Providing kiwi as fallback
5857
" ]) in
59-
std.io.stdio._print α0 in
60-
Pure tt in
61-
Pure
62-
(core.option.Option.Some
63-
unpacking_options_and_defaults_via_or_else.Fruit.Kiwi) in
58+
std.io.stdio._print α0 in
59+
Pure tt in
60+
Pure
61+
(core.option.Option.Some
62+
unpacking_options_and_defaults_via_or_else.Fruit.Kiwi) in
6463
let get_lemon_as_fallback :=
65-
fun =>
64+
let* _ :=
6665
let* _ :=
67-
let* _ :=
68-
let* α0 :=
69-
format_arguments::["new_const"]
70-
(addr_of [ "Providing lemon as fallback
66+
let* α0 :=
67+
format_arguments::["new_const"]
68+
(addr_of [ "Providing lemon as fallback
7169
" ]) in
72-
std.io.stdio._print α0 in
73-
Pure tt in
74-
Pure
75-
(core.option.Option.Some
76-
unpacking_options_and_defaults_via_or_else.Fruit.Lemon) in
70+
std.io.stdio._print α0 in
71+
Pure tt in
72+
Pure
73+
(core.option.Option.Some
74+
unpacking_options_and_defaults_via_or_else.Fruit.Lemon) in
7775
let* first_available_fruit :=
7876
let* α0 := no_fruit.["or_else"] get_kiwi_as_fallback in
7977
α0.["or_else"] get_lemon_as_fallback in

‎coq_translation/default/examples/functions/functions_closures.v‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -28,7 +28,7 @@ Definition main `{H' : State.Trait} : M (H := H') unit :=
2828
(addr_of [ α1 ]) in
2929
std.io.stdio._print α2 in
3030
Pure tt in
31-
let one := fun => Pure 1 in
31+
let one := Pure 1 in
3232
let* _ :=
3333
let* _ :=
3434
let* α0 := one in

‎coq_translation/default/examples/functions/functions_closures_as_input_parameters.v‎

Lines changed: 24 additions & 25 deletions
Original file line numberDiff line numberDiff line change
@@ -23,38 +23,37 @@ Definition main `{H' : State.Trait} : M (H := H') unit :=
2323
let greeting := "hello" in
2424
let* farewell := "goodbye".["to_owned"] in
2525
let diary :=
26-
fun =>
26+
let* _ :=
2727
let* _ :=
28-
let* _ :=
29-
let* α0 := format_argument::["new_display"] (addr_of greeting) in
30-
let* α1 :=
31-
format_arguments::["new_v1"]
32-
(addr_of [ "I said "; ".
28+
let* α0 := format_argument::["new_display"] (addr_of greeting) in
29+
let* α1 :=
30+
format_arguments::["new_v1"]
31+
(addr_of [ "I said "; ".
3332
" ])
34-
(addr_of [ α0 ]) in
35-
std.io.stdio._print α1 in
36-
Pure tt in
37-
let* _ := farewell.["push_str"] "!!!" in
33+
(addr_of [ α0 ]) in
34+
std.io.stdio._print α1 in
35+
Pure tt in
36+
let* _ := farewell.["push_str"] "!!!" in
37+
let* _ :=
3838
let* _ :=
39-
let* _ :=
40-
let* α0 := format_argument::["new_display"] (addr_of farewell) in
41-
let* α1 :=
42-
format_arguments::["new_v1"]
43-
(addr_of [ "Then I screamed "; ".
39+
let* α0 := format_argument::["new_display"] (addr_of farewell) in
40+
let* α1 :=
41+
format_arguments::["new_v1"]
42+
(addr_of [ "Then I screamed "; ".
4443
" ])
45-
(addr_of [ α0 ]) in
46-
std.io.stdio._print α1 in
47-
Pure tt in
44+
(addr_of [ α0 ]) in
45+
std.io.stdio._print α1 in
46+
Pure tt in
47+
let* _ :=
4848
let* _ :=
49-
let* _ :=
50-
let* α0 :=
51-
format_arguments::["new_const"]
52-
(addr_of [ "Now I can sleep. zzzzz
49+
let* α0 :=
50+
format_arguments::["new_const"]
51+
(addr_of [ "Now I can sleep. zzzzz
5352
" ]) in
54-
std.io.stdio._print α0 in
55-
Pure tt in
56-
let* _ := core.mem.drop farewell in
53+
std.io.stdio._print α0 in
5754
Pure tt in
55+
let* _ := core.mem.drop farewell in
56+
Pure tt in
5857
let* _ := functions_closures_as_input_parameters.apply diary in
5958
let double := fun x => 2.["mul"] x in
6059
let* _ :=

‎coq_translation/default/examples/functions/functions_closures_as_output_parameters.v‎

Lines changed: 24 additions & 27 deletions
Original file line numberDiff line numberDiff line change
@@ -4,46 +4,43 @@ Require Import CoqOfRust.CoqOfRust.
44
Definition create_fn `{H' : State.Trait} : M (H := H') _ (* OpaqueTy *) :=
55
let* text := "Fn".["to_owned"] in
66
Pure
7-
(fun =>
8-
let* _ :=
9-
let* α0 := format_argument::["new_display"] (addr_of text) in
10-
let* α1 :=
11-
format_arguments::["new_v1"]
12-
(addr_of [ "This is a: "; "
7+
let* _ :=
8+
let* α0 := format_argument::["new_display"] (addr_of text) in
9+
let* α1 :=
10+
format_arguments::["new_v1"]
11+
(addr_of [ "This is a: "; "
1312
" ])
14-
(addr_of [ α0 ]) in
15-
std.io.stdio._print α1 in
16-
Pure tt).
13+
(addr_of [ α0 ]) in
14+
std.io.stdio._print α1 in
15+
Pure tt.
1716

1817
Error OpaqueTy.
1918

2019
Definition create_fnmut `{H' : State.Trait} : M (H := H') _ (* OpaqueTy *) :=
2120
let* text := "FnMut".["to_owned"] in
2221
Pure
23-
(fun =>
24-
let* _ :=
25-
let* α0 := format_argument::["new_display"] (addr_of text) in
26-
let* α1 :=
27-
format_arguments::["new_v1"]
28-
(addr_of [ "This is a: "; "
22+
let* _ :=
23+
let* α0 := format_argument::["new_display"] (addr_of text) in
24+
let* α1 :=
25+
format_arguments::["new_v1"]
26+
(addr_of [ "This is a: "; "
2927
" ])
30-
(addr_of [ α0 ]) in
31-
std.io.stdio._print α1 in
32-
Pure tt).
28+
(addr_of [ α0 ]) in
29+
std.io.stdio._print α1 in
30+
Pure tt.
3331

3432
Definition create_fnonce `{H' : State.Trait} : M (H := H') _ (* OpaqueTy *) :=
3533
let* text := "FnOnce".["to_owned"] in
3634
Pure
37-
(fun =>
38-
let* _ :=
39-
let* α0 := format_argument::["new_display"] (addr_of text) in
40-
let* α1 :=
41-
format_arguments::["new_v1"]
42-
(addr_of [ "This is a: "; "
35+
let* _ :=
36+
let* α0 := format_argument::["new_display"] (addr_of text) in
37+
let* α1 :=
38+
format_arguments::["new_v1"]
39+
(addr_of [ "This is a: "; "
4340
" ])
44-
(addr_of [ α0 ]) in
45-
std.io.stdio._print α1 in
46-
Pure tt).
41+
(addr_of [ α0 ]) in
42+
std.io.stdio._print α1 in
43+
Pure tt.
4744

4845
(* #[allow(dead_code)] - function was ignored by the compiler *)
4946
Definition main `{H' : State.Trait} : M (H := H') unit :=

0 commit comments

Comments
 (0)