Skip to content

Commit 2d8c898

Browse files
InfiniteEchoesclarus
authored andcommitted
New line after let in
1 parent 3fb39ea commit 2d8c898

File tree

255 files changed

+7531
-3357
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

255 files changed

+7531
-3357
lines changed

CoqOfRust/examples/default/examples/custom/constructor_as_function.v

Lines changed: 14 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -29,7 +29,8 @@ Definition matching (τ : list Ty.t) (α : list Value.t) : M :=
2929
M.alloc (Value.Integer Integer.I32 0);
3030
fun γ =>
3131
let γ0_0 := M.get_tuple_field γ 0 in
32-
let γ0_1 := M.get_tuple_field γ 1 in M.alloc (Value.Integer Integer.I32 1)
32+
let γ0_1 := M.get_tuple_field γ 1 in
33+
M.alloc (Value.Integer Integer.I32 1)
3334
] in
3435
M.read α0
3536
| _, _ => M.impossible
@@ -146,14 +147,16 @@ Definition main (τ : list Ty.t) (α : list Value.t) : M :=
146147
Value.Integer Integer.I32 3
147148
]) in
148149
let* α6 := M.call_closure α4 [ α5 ] in
149-
let* α7 := M.read α6 in M.pure (M.pointer_coercion α7) in
150+
let* α7 := M.read α6 in
151+
M.pure (M.pointer_coercion α7) in
150152
let* α9 := M.call_closure α3 [ α8 ] in
151153
let* α10 := M.call_closure α2 [ α9 ] in
152154
let* α11 :=
153155
M.call_closure
154156
α1
155157
[ α10; M.constructor_as_closure "constructor_as_function::Constructor" ] in
156-
let* α12 := M.call_closure α0 [ α11 ] in M.alloc α12 in
158+
let* α12 := M.call_closure α0 [ α11 ] in
159+
M.alloc α12 in
157160
let* _ :=
158161
let* _ :=
159162
let* α0 := M.get_function "std::io::stdio::_print" [] in
@@ -163,7 +166,8 @@ Definition main (τ : list Ty.t) (α : list Value.t) : M :=
163166
let* α2 := M.read (mk_str "") in
164167
let* α3 := M.read (mk_str "
165168
") in
166-
let* α4 := M.alloc (Value.Array [ α2; α3 ]) in M.pure (M.pointer_coercion α4) in
169+
let* α4 := M.alloc (Value.Array [ α2; α3 ]) in
170+
M.pure (M.pointer_coercion α4) in
167171
let* α9 :=
168172
(* Unsize *)
169173
let* α6 :=
@@ -177,10 +181,13 @@ Definition main (τ : list Ty.t) (α : list Value.t) : M :=
177181
]
178182
] in
179183
let* α7 := M.call_closure α6 [ v ] in
180-
let* α8 := M.alloc (Value.Array [ α7 ]) in M.pure (M.pointer_coercion α8) in
184+
let* α8 := M.alloc (Value.Array [ α7 ]) in
185+
M.pure (M.pointer_coercion α8) in
181186
let* α10 := M.call_closure α1 [ α5; α9 ] in
182-
let* α11 := M.call_closure α0 [ α10 ] in M.alloc α11 in
187+
let* α11 := M.call_closure α0 [ α10 ] in
188+
M.alloc α11 in
183189
M.alloc (Value.Tuple []) in
184-
let* α0 := M.alloc (Value.Tuple []) in M.read α0
190+
let* α0 := M.alloc (Value.Tuple []) in
191+
M.read α0
185192
| _, _ => M.impossible
186193
end.

CoqOfRust/examples/default/examples/custom/hello_world.v

Lines changed: 34 additions & 17 deletions
Original file line numberDiff line numberDiff line change
@@ -54,7 +54,8 @@ Definition main (τ : list Ty.t) (α : list Value.t) : M :=
5454
let* α2 := M.read (mk_str "") in
5555
let* α3 := M.read (mk_str "
5656
") in
57-
let* α4 := M.alloc (Value.Array [ α2; α3 ]) in M.pure (M.pointer_coercion α4) in
57+
let* α4 := M.alloc (Value.Array [ α2; α3 ]) in
58+
M.pure (M.pointer_coercion α4) in
5859
let* α10 :=
5960
(* Unsize *)
6061
let* α6 :=
@@ -64,9 +65,11 @@ Definition main (τ : list Ty.t) (α : list Value.t) : M :=
6465
[ Ty.apply (Ty.path "&") [ Ty.path "str" ] ] in
6566
let* α7 := M.get_constant "hello_world::message" in
6667
let* α8 := M.call_closure α6 [ α7 ] in
67-
let* α9 := M.alloc (Value.Array [ α8 ]) in M.pure (M.pointer_coercion α9) in
68+
let* α9 := M.alloc (Value.Array [ α8 ]) in
69+
M.pure (M.pointer_coercion α9) in
6870
let* α11 := M.call_closure α1 [ α5; α10 ] in
69-
let* α12 := M.call_closure α0 [ α11 ] in M.alloc α12 in
71+
let* α12 := M.call_closure α0 [ α11 ] in
72+
M.alloc α12 in
7073
M.alloc (Value.Tuple []) in
7174
let* number :=
7275
M.alloc (Value.StructTuple "core::option::Option::Some" [ Value.Integer Integer.I32 7 ]) in
@@ -90,7 +93,8 @@ Definition main (τ : list Ty.t) (α : list Value.t) : M :=
9093
let* α2 := M.read (mk_str "Matched ") in
9194
let* α3 := M.read (mk_str "!
9295
") in
93-
let* α4 := M.alloc (Value.Array [ α2; α3 ]) in M.pure (M.pointer_coercion α4) in
96+
let* α4 := M.alloc (Value.Array [ α2; α3 ]) in
97+
M.pure (M.pointer_coercion α4) in
9498
let* α9 :=
9599
(* Unsize *)
96100
let* α6 :=
@@ -99,9 +103,11 @@ Definition main (τ : list Ty.t) (α : list Value.t) : M :=
99103
"new_debug"
100104
[ Ty.path "i32" ] in
101105
let* α7 := M.call_closure α6 [ i ] in
102-
let* α8 := M.alloc (Value.Array [ α7 ]) in M.pure (M.pointer_coercion α8) in
106+
let* α8 := M.alloc (Value.Array [ α7 ]) in
107+
M.pure (M.pointer_coercion α8) in
103108
let* α10 := M.call_closure α1 [ α5; α9 ] in
104-
let* α11 := M.call_closure α0 [ α10 ] in M.alloc α11 in
109+
let* α11 := M.call_closure α0 [ α10 ] in
110+
M.alloc α11 in
105111
M.alloc (Value.Tuple []) in
106112
M.alloc (Value.Tuple []);
107113
fun γ => M.alloc (Value.Tuple [])
@@ -124,7 +130,8 @@ Definition main (τ : list Ty.t) (α : list Value.t) : M :=
124130
let* α2 := M.read (mk_str "Matched ") in
125131
let* α3 := M.read (mk_str "!
126132
") in
127-
let* α4 := M.alloc (Value.Array [ α2; α3 ]) in M.pure (M.pointer_coercion α4) in
133+
let* α4 := M.alloc (Value.Array [ α2; α3 ]) in
134+
M.pure (M.pointer_coercion α4) in
128135
let* α9 :=
129136
(* Unsize *)
130137
let* α6 :=
@@ -133,9 +140,11 @@ Definition main (τ : list Ty.t) (α : list Value.t) : M :=
133140
"new_debug"
134141
[ Ty.path "i32" ] in
135142
let* α7 := M.call_closure α6 [ j ] in
136-
let* α8 := M.alloc (Value.Array [ α7 ]) in M.pure (M.pointer_coercion α8) in
143+
let* α8 := M.alloc (Value.Array [ α7 ]) in
144+
M.pure (M.pointer_coercion α8) in
137145
let* α10 := M.call_closure α1 [ α5; α9 ] in
138-
let* α11 := M.call_closure α0 [ α10 ] in M.alloc α11 in
146+
let* α11 := M.call_closure α0 [ α10 ] in
147+
M.alloc α11 in
139148
M.alloc (Value.Tuple []) in
140149
M.alloc (Value.Tuple []);
141150
fun γ =>
@@ -148,9 +157,11 @@ Definition main (τ : list Ty.t) (α : list Value.t) : M :=
148157
(* Unsize *)
149158
let* α2 := M.read (mk_str "Didn't match a number. Let's go with a letter!
150159
") in
151-
let* α3 := M.alloc (Value.Array [ α2 ]) in M.pure (M.pointer_coercion α3) in
160+
let* α3 := M.alloc (Value.Array [ α2 ]) in
161+
M.pure (M.pointer_coercion α3) in
152162
let* α5 := M.call_closure α1 [ α4 ] in
153-
let* α6 := M.call_closure α0 [ α5 ] in M.alloc α6 in
163+
let* α6 := M.call_closure α0 [ α5 ] in
164+
M.alloc α6 in
154165
M.alloc (Value.Tuple []) in
155166
M.alloc (Value.Tuple [])
156167
] in
@@ -173,7 +184,8 @@ Definition main (τ : list Ty.t) (α : list Value.t) : M :=
173184
let* α2 := M.read (mk_str "Matched ") in
174185
let* α3 := M.read (mk_str "!
175186
") in
176-
let* α4 := M.alloc (Value.Array [ α2; α3 ]) in M.pure (M.pointer_coercion α4) in
187+
let* α4 := M.alloc (Value.Array [ α2; α3 ]) in
188+
M.pure (M.pointer_coercion α4) in
177189
let* α9 :=
178190
(* Unsize *)
179191
let* α6 :=
@@ -182,9 +194,11 @@ Definition main (τ : list Ty.t) (α : list Value.t) : M :=
182194
"new_debug"
183195
[ Ty.path "i32" ] in
184196
let* α7 := M.call_closure α6 [ i ] in
185-
let* α8 := M.alloc (Value.Array [ α7 ]) in M.pure (M.pointer_coercion α8) in
197+
let* α8 := M.alloc (Value.Array [ α7 ]) in
198+
M.pure (M.pointer_coercion α8) in
186199
let* α10 := M.call_closure α1 [ α5; α9 ] in
187-
let* α11 := M.call_closure α0 [ α10 ] in M.alloc α11 in
200+
let* α11 := M.call_closure α0 [ α10 ] in
201+
M.alloc α11 in
188202
M.alloc (Value.Tuple []) in
189203
M.alloc (Value.Tuple []);
190204
fun γ =>
@@ -195,7 +209,8 @@ Definition main (τ : list Ty.t) (α : list Value.t) : M :=
195209
fun γ =>
196210
let γ := M.use i_like_letters in
197211
let* _ :=
198-
let* α0 := M.read γ in M.is_constant_or_break_match α0 (Value.Bool true) in
212+
let* α0 := M.read γ in
213+
M.is_constant_or_break_match α0 (Value.Bool true) in
199214
let* _ :=
200215
let* _ :=
201216
let* α0 := M.get_function "std::io::stdio::_print" [] in
@@ -209,7 +224,8 @@ Definition main (τ : list Ty.t) (α : list Value.t) : M :=
209224
let* α3 := M.alloc (Value.Array [ α2 ]) in
210225
M.pure (M.pointer_coercion α3) in
211226
let* α5 := M.call_closure α1 [ α4 ] in
212-
let* α6 := M.call_closure α0 [ α5 ] in M.alloc α6 in
227+
let* α6 := M.call_closure α0 [ α5 ] in
228+
M.alloc α6 in
213229
M.alloc (Value.Tuple []) in
214230
M.alloc (Value.Tuple []);
215231
fun γ =>
@@ -227,7 +243,8 @@ Definition main (τ : list Ty.t) (α : list Value.t) : M :=
227243
let* α3 := M.alloc (Value.Array [ α2 ]) in
228244
M.pure (M.pointer_coercion α3) in
229245
let* α5 := M.call_closure α1 [ α4 ] in
230-
let* α6 := M.call_closure α0 [ α5 ] in M.alloc α6 in
246+
let* α6 := M.call_closure α0 [ α5 ] in
247+
M.alloc α6 in
231248
M.alloc (Value.Tuple []) in
232249
M.alloc (Value.Tuple [])
233250
]

CoqOfRust/examples/default/examples/custom/if_let.v

Lines changed: 30 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -15,7 +15,8 @@ Definition order (τ : list Ty.t) (α : list Value.t) : M :=
1515
let* b4 := M.alloc b4 in
1616
let* α0 := M.read b1 in
1717
let* α1 := LogicalOp.and α0 (M.read b2) in
18-
let* α2 := LogicalOp.and α1 (M.read b3) in LogicalOp.and α2 (M.read b4)
18+
let* α2 := LogicalOp.and α1 (M.read b3) in
19+
LogicalOp.and α2 (M.read b4)
1920
| _, _ => M.impossible
2021
end.
2122

@@ -65,11 +66,13 @@ Definition extract_value (τ : list Ty.t) (α : list Value.t) : M :=
6566
fun γ =>
6667
let* γ0_0 :=
6768
M.get_struct_tuple_field_or_break_match γ "if_let::Container::Left" 0 in
68-
let* value := M.copy γ0_0 in M.pure (Value.Tuple [ value ]);
69+
let* value := M.copy γ0_0 in
70+
M.pure (Value.Tuple [ value ]);
6971
fun γ =>
7072
let* γ0_0 :=
7173
M.get_struct_tuple_field_or_break_match γ "if_let::Container::Right" 0 in
72-
let* value := M.copy γ0_0 in M.pure (Value.Tuple [ value ])
74+
let* value := M.copy γ0_0 in
75+
M.pure (Value.Tuple [ value ])
7376
]
7477
(M.closure
7578
(fun γ => match γ with | [ value ] => M.pure value | _ => M.impossible end));
@@ -134,7 +137,8 @@ Definition main (τ : list Ty.t) (α : list Value.t) : M :=
134137
let* α2 := M.read (mk_str "if: ") in
135138
let* α3 := M.read (mk_str "
136139
") in
137-
let* α4 := M.alloc (Value.Array [ α2; α3 ]) in M.pure (M.pointer_coercion α4) in
140+
let* α4 := M.alloc (Value.Array [ α2; α3 ]) in
141+
M.pure (M.pointer_coercion α4) in
138142
let* α9 :=
139143
(* Unsize *)
140144
let* α6 :=
@@ -143,9 +147,11 @@ Definition main (τ : list Ty.t) (α : list Value.t) : M :=
143147
"new_display"
144148
[ Ty.path "i32" ] in
145149
let* α7 := M.call_closure α6 [ y ] in
146-
let* α8 := M.alloc (Value.Array [ α7 ]) in M.pure (M.pointer_coercion α8) in
150+
let* α8 := M.alloc (Value.Array [ α7 ]) in
151+
M.pure (M.pointer_coercion α8) in
147152
let* α10 := M.call_closure α1 [ α5; α9 ] in
148-
let* α11 := M.call_closure α0 [ α10 ] in M.alloc α11 in
153+
let* α11 := M.call_closure α0 [ α10 ] in
154+
M.alloc α11 in
149155
M.alloc (Value.Tuple []) in
150156
M.alloc (Value.Tuple []);
151157
fun γ => M.alloc (Value.Tuple [])
@@ -167,7 +173,8 @@ Definition main (τ : list Ty.t) (α : list Value.t) : M :=
167173
let* α2 := M.read (mk_str "match: ") in
168174
let* α3 := M.read (mk_str "
169175
") in
170-
let* α4 := M.alloc (Value.Array [ α2; α3 ]) in M.pure (M.pointer_coercion α4) in
176+
let* α4 := M.alloc (Value.Array [ α2; α3 ]) in
177+
M.pure (M.pointer_coercion α4) in
171178
let* α9 :=
172179
(* Unsize *)
173180
let* α6 :=
@@ -176,9 +183,11 @@ Definition main (τ : list Ty.t) (α : list Value.t) : M :=
176183
"new_display"
177184
[ Ty.path "i32" ] in
178185
let* α7 := M.call_closure α6 [ y ] in
179-
let* α8 := M.alloc (Value.Array [ α7 ]) in M.pure (M.pointer_coercion α8) in
186+
let* α8 := M.alloc (Value.Array [ α7 ]) in
187+
M.pure (M.pointer_coercion α8) in
180188
let* α10 := M.call_closure α1 [ α5; α9 ] in
181-
let* α11 := M.call_closure α0 [ α10 ] in M.alloc α11 in
189+
let* α11 := M.call_closure α0 [ α10 ] in
190+
M.alloc α11 in
182191
M.alloc (Value.Tuple []);
183192
fun γ => M.alloc (Value.Tuple [])
184193
] in
@@ -195,7 +204,9 @@ Definition main (τ : list Ty.t) (α : list Value.t) : M :=
195204
let* α0 := M.read y in
196205
let* α1 := M.alloc (BinOp.Pure.gt α0 (Value.Integer Integer.I32 3)) in
197206
M.pure (M.use α1) in
198-
let* _ := let* α0 := M.read γ in M.is_constant_or_break_match α0 (Value.Bool true) in
207+
let* _ :=
208+
let* α0 := M.read γ in
209+
M.is_constant_or_break_match α0 (Value.Bool true) in
199210
let γ := x in
200211
let* γ0_0 := M.get_struct_tuple_field_or_break_match γ "core::option::Option::Some" 0 in
201212
let* z := M.copy γ0_0 in
@@ -228,7 +239,8 @@ Definition main (τ : list Ty.t) (α : list Value.t) : M :=
228239
let* α11 := M.alloc (Value.Array [ α8; α10 ]) in
229240
M.pure (M.pointer_coercion α11) in
230241
let* α13 := M.call_closure α1 [ α6; α12 ] in
231-
let* α14 := M.call_closure α0 [ α13 ] in M.alloc α14 in
242+
let* α14 := M.call_closure α0 [ α13 ] in
243+
M.alloc α14 in
232244
M.alloc (Value.Tuple []) in
233245
M.alloc (Value.Tuple []);
234246
fun γ => M.alloc (Value.Tuple [])
@@ -243,8 +255,11 @@ Definition main (τ : list Ty.t) (α : list Value.t) : M :=
243255
let* γ0_0 := M.get_struct_tuple_field_or_break_match γ "core::option::Option::Some" 0 in
244256
let* y := M.copy γ0_0 in
245257
let* γ :=
246-
let* α0 := M.read y in M.alloc (BinOp.Pure.gt α0 (Value.Integer Integer.I32 3)) in
247-
let* _ := let* α0 := M.read γ in M.is_constant_or_break_match α0 (Value.Bool true) in
258+
let* α0 := M.read y in
259+
M.alloc (BinOp.Pure.gt α0 (Value.Integer Integer.I32 3)) in
260+
let* _ :=
261+
let* α0 := M.read γ in
262+
M.is_constant_or_break_match α0 (Value.Bool true) in
248263
let γ := x in
249264
let* γ0_0 := M.get_struct_tuple_field_or_break_match γ "core::option::Option::Some" 0 in
250265
let* z := M.copy γ0_0 in
@@ -276,7 +291,8 @@ Definition main (τ : list Ty.t) (α : list Value.t) : M :=
276291
let* α11 := M.alloc (Value.Array [ α8; α10 ]) in
277292
M.pure (M.pointer_coercion α11) in
278293
let* α13 := M.call_closure α1 [ α6; α12 ] in
279-
let* α14 := M.call_closure α0 [ α13 ] in M.alloc α14 in
294+
let* α14 := M.call_closure α0 [ α13 ] in
295+
M.alloc α14 in
280296
M.alloc (Value.Tuple []);
281297
fun γ => M.alloc (Value.Tuple [])
282298
] in

CoqOfRust/examples/default/examples/custom/impl_param.v

Lines changed: 8 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -23,11 +23,13 @@ Definition with_impls (τ : list Ty.t) (α : list Value.t) : M :=
2323
let* x := M.copy func in
2424
let* _ :=
2525
let* α0 := M.get_trait_method "core::default::Default" impl_Default [] "default" [] in
26-
let* α1 := M.call_closure α0 [] in M.assign x α1 in
26+
let* α1 := M.call_closure α0 [] in
27+
M.assign x α1 in
2728
let* y := M.copy func2 in
2829
let* _ :=
2930
let* α0 := M.get_trait_method "core::default::Default" impl_Default'1 [] "default" [] in
30-
let* α1 := M.call_closure α0 [] in M.assign y α1 in
31+
let* α1 := M.call_closure α0 [] in
32+
M.assign y α1 in
3133
let* z := M.copy foo in
3234
let* b :=
3335
let* α0 :=
@@ -40,7 +42,9 @@ Definition with_impls (τ : list Ty.t) (α : list Value.t) : M :=
4042
let* α1 := M.read x in
4143
let* α2 := M.read y in
4244
let* α3 := M.read z in
43-
let* α4 := M.call_closure α0 [ Value.Tuple [ α1; α2; α3 ] ] in M.alloc α4 in
44-
let* α0 := M.alloc (Value.Tuple []) in M.read α0
45+
let* α4 := M.call_closure α0 [ Value.Tuple [ α1; α2; α3 ] ] in
46+
M.alloc α4 in
47+
let* α0 := M.alloc (Value.Tuple []) in
48+
M.read α0
4549
| _, _ => M.impossible
4650
end.

CoqOfRust/examples/default/examples/custom/module_duplicate.v

Lines changed: 18 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -19,11 +19,14 @@ Module foo.
1919
(* Unsize *)
2020
let* α2 := M.read (mk_str "foo::gre::bar
2121
") in
22-
let* α3 := M.alloc (Value.Array [ α2 ]) in M.pure (M.pointer_coercion α3) in
22+
let* α3 := M.alloc (Value.Array [ α2 ]) in
23+
M.pure (M.pointer_coercion α3) in
2324
let* α5 := M.call_closure α1 [ α4 ] in
24-
let* α6 := M.call_closure α0 [ α5 ] in M.alloc α6 in
25+
let* α6 := M.call_closure α0 [ α5 ] in
26+
M.alloc α6 in
2527
M.alloc (Value.Tuple []) in
26-
let* α0 := M.alloc (Value.Tuple []) in M.read α0
28+
let* α0 := M.alloc (Value.Tuple []) in
29+
M.read α0
2730
| _, _ => M.impossible
2831
end.
2932
End gre.
@@ -45,14 +48,18 @@ Module foo.
4548
(* Unsize *)
4649
let* α2 := M.read (mk_str "foo::bar
4750
") in
48-
let* α3 := M.alloc (Value.Array [ α2 ]) in M.pure (M.pointer_coercion α3) in
51+
let* α3 := M.alloc (Value.Array [ α2 ]) in
52+
M.pure (M.pointer_coercion α3) in
4953
let* α5 := M.call_closure α1 [ α4 ] in
50-
let* α6 := M.call_closure α0 [ α5 ] in M.alloc α6 in
54+
let* α6 := M.call_closure α0 [ α5 ] in
55+
M.alloc α6 in
5156
M.alloc (Value.Tuple []) in
5257
let* _ :=
5358
let* α0 := M.get_function "module_duplicate::foo::gre::f_foo_gre" [] in
54-
let* α1 := M.call_closure α0 [] in M.alloc α1 in
55-
let* α0 := M.alloc (Value.Tuple []) in M.read α0
59+
let* α1 := M.call_closure α0 [] in
60+
M.alloc α1 in
61+
let* α0 := M.alloc (Value.Tuple []) in
62+
M.read α0
5663
| _, _ => M.impossible
5764
end.
5865
End foo.
@@ -67,7 +74,9 @@ Definition f (τ : list Ty.t) (α : list Value.t) : M :=
6774
| [], [] =>
6875
let* _ :=
6976
let* α0 := M.get_function "module_duplicate::foo::f_foo" [] in
70-
let* α1 := M.call_closure α0 [] in M.alloc α1 in
71-
let* α0 := M.alloc (Value.Tuple []) in M.read α0
77+
let* α1 := M.call_closure α0 [] in
78+
M.alloc α1 in
79+
let* α0 := M.alloc (Value.Tuple []) in
80+
M.read α0
7281
| _, _ => M.impossible
7382
end.

0 commit comments

Comments
 (0)