Skip to content

Commit 6be7148

Browse files
clarusclarus
committed
simulations: compile the beginning of the gas file
1 parent 568527d commit 6be7148

Some content is hidden

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

89 files changed

+33736
-33332
lines changed

‎CoqOfRust/alloc/collections/vec_deque/into_iter.v

Lines changed: 4 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -1244,13 +1244,12 @@ Module collections.
12441244
(Ty.path "array")
12451245
[ N ]
12461246
[ Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") [] [ T ] ] :=
1247-
repeat (|
1248-
M.read (|
1247+
repeat
1248+
(M.read (|
12491249
M.get_constant
12501250
"alloc::collections::vec_deque::into_iter::next_chunk_discriminant"
1251-
|),
1252-
N
1253-
|) in
1251+
|))
1252+
N in
12541253
let~ raw_arr_ptr : Ty.apply (Ty.path "*mut") [] [ T ] :=
12551254
M.call_closure (|
12561255
Ty.apply (Ty.path "*mut") [] [ T ],

‎CoqOfRust/alloc/str.v

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -7719,7 +7719,7 @@ Module str.
77197719
(Ty.path "array")
77207720
[ Value.Integer IntegerKind.Usize 16 ]
77217721
[ Ty.path "bool" ] :=
7722-
repeat (| Value.Bool false, Value.Integer IntegerKind.Usize 16 |) in
7722+
repeat (Value.Bool false) (Value.Integer IntegerKind.Usize 16) in
77237723
let~ _ : Ty.tuple [] :=
77247724
M.read (|
77257725
M.loop (|

‎CoqOfRust/alloc/string.v

Lines changed: 7 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -5508,10 +5508,9 @@ Module string.
55085508
M.borrow (|
55095509
Pointer.Kind.MutRef,
55105510
M.alloc (|
5511-
repeat (|
5512-
Value.Integer IntegerKind.U8 0,
5513-
Value.Integer IntegerKind.Usize 4
5514-
|)
5511+
repeat
5512+
(Value.Integer IntegerKind.U8 0)
5513+
(Value.Integer IntegerKind.Usize 4)
55155514
|)
55165515
|)
55175516
|)
@@ -7550,7 +7549,7 @@ Module string.
75507549
|) in
75517550
let~ bits :
75527551
Ty.apply (Ty.path "array") [ Value.Integer IntegerKind.Usize 4 ] [ Ty.path "u8" ] :=
7553-
repeat (| Value.Integer IntegerKind.U8 0, Value.Integer IntegerKind.Usize 4 |) in
7552+
repeat (Value.Integer IntegerKind.U8 0) (Value.Integer IntegerKind.Usize 4) in
75547553
let~ bits :
75557554
Ty.apply (Ty.path "&") [] [ Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ] ] :=
75567555
M.call_closure (|
@@ -14586,10 +14585,9 @@ Module string.
1458614585
M.borrow (|
1458714586
Pointer.Kind.MutRef,
1458814587
M.alloc (|
14589-
repeat (|
14590-
Value.Integer IntegerKind.U8 0,
14591-
Value.Integer IntegerKind.Usize 4
14592-
|)
14588+
repeat
14589+
(Value.Integer IntegerKind.U8 0)
14590+
(Value.Integer IntegerKind.Usize 4)
1459314591
|)
1459414592
|)
1459514593
|)

‎CoqOfRust/alloc/vec/into_iter.v

Lines changed: 3 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1815,10 +1815,9 @@ Module vec.
18151815
(Ty.path "array")
18161816
[ N ]
18171817
[ Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") [] [ T ] ] :=
1818-
repeat (|
1819-
M.read (| M.get_constant "alloc::vec::into_iter::next_chunk_discriminant" |),
1820-
N
1821-
|) in
1818+
repeat
1819+
(M.read (| M.get_constant "alloc::vec::into_iter::next_chunk_discriminant" |))
1820+
N in
18221821
let~ len : Ty.path "usize" :=
18231822
M.call_closure (|
18241823
Ty.path "usize",

‎CoqOfRust/core/array/iter.v

Lines changed: 4 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -256,10 +256,7 @@ Module array.
256256
(Ty.path "array")
257257
[ N ]
258258
[ Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") [] [ T ] ] :=
259-
repeat (|
260-
M.read (| M.get_constant "core::array::iter::empty_discriminant" |),
261-
N
262-
|) in
259+
repeat (M.read (| M.get_constant "core::array::iter::empty_discriminant" |)) N in
263260
let~ initialized :
264261
Ty.apply (Ty.path "core::ops::range::Range") [] [ Ty.path "usize" ] :=
265262
Value.StructRecord
@@ -2121,10 +2118,9 @@ Module array.
21212118
"core::array::iter::IntoIter"
21222119
[
21232120
("data",
2124-
repeat (|
2125-
M.read (| M.get_constant "core::array::iter::clone_discriminant" |),
2126-
N
2127-
|));
2121+
repeat
2122+
(M.read (| M.get_constant "core::array::iter::clone_discriminant" |))
2123+
N);
21282124
("alive",
21292125
M.call_closure (|
21302126
Ty.path "core::ops::index_range::IndexRange",

‎CoqOfRust/core/array/mod.v

Lines changed: 10 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -121,7 +121,7 @@ Module array.
121121
[]
122122
[ Ty.associated_in_trait "core::ops::try_trait::Try" [] [] R "Output" ]
123123
] :=
124-
repeat (| M.read (| M.get_constant "core::array::try_from_fn_discriminant" |), N |) in
124+
repeat (M.read (| M.get_constant "core::array::try_from_fn_discriminant" |)) N in
125125
M.match_operator (|
126126
Some
127127
(Ty.associated_in_trait
@@ -6147,14 +6147,13 @@ Module array.
61476147
(let self := M.alloc (| self |) in
61486148
M.read (|
61496149
let~ buf : Ty.apply (Ty.path "array") [ N ] [ Ty.apply (Ty.path "*const") [] [ T ] ] :=
6150-
repeat (|
6151-
M.call_closure (|
6150+
repeat
6151+
(M.call_closure (|
61526152
Ty.apply (Ty.path "*const") [] [ T ],
61536153
M.get_function (| "core::ptr::null", [], [ T ] |),
61546154
[]
6155-
|),
6156-
N
6157-
|) in
6155+
|))
6156+
N in
61586157
let~ i : Ty.path "usize" := Value.Integer IntegerKind.Usize 0 in
61596158
let~ _ : Ty.tuple [] :=
61606159
M.read (|
@@ -6267,14 +6266,13 @@ Module array.
62676266
(let self := M.alloc (| self |) in
62686267
M.read (|
62696268
let~ buf : Ty.apply (Ty.path "array") [ N ] [ Ty.apply (Ty.path "*mut") [] [ T ] ] :=
6270-
repeat (|
6271-
M.call_closure (|
6269+
repeat
6270+
(M.call_closure (|
62726271
Ty.apply (Ty.path "*mut") [] [ T ],
62736272
M.get_function (| "core::ptr::null_mut", [], [ T ] |),
62746273
[]
6275-
|),
6276-
N
6277-
|) in
6274+
|))
6275+
N in
62786276
let~ i : Ty.path "usize" := Value.Integer IntegerKind.Usize 0 in
62796277
let~ _ : Ty.tuple [] :=
62806278
M.read (|
@@ -7708,10 +7706,7 @@ Module array.
77087706
(Ty.path "array")
77097707
[ N ]
77107708
[ Ty.apply (Ty.path "core::mem::maybe_uninit::MaybeUninit") [] [ T ] ] :=
7711-
repeat (|
7712-
M.read (| M.get_constant "core::array::iter_next_chunk_discriminant" |),
7713-
N
7714-
|) in
7709+
repeat (M.read (| M.get_constant "core::array::iter_next_chunk_discriminant" |)) N in
77157710
let~ r : Ty.apply (Ty.path "core::result::Result") [] [ Ty.tuple []; Ty.path "usize" ] :=
77167711
M.call_closure (|
77177712
Ty.apply (Ty.path "core::result::Result") [] [ Ty.tuple []; Ty.path "usize" ],

‎CoqOfRust/core/escape.v

Lines changed: 6 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -91,7 +91,7 @@ Module escape.
9191
M.read (| M.get_constant "core::escape::backslash_discriminant" |) in
9292
let~ output :
9393
Ty.apply (Ty.path "array") [ N ] [ Ty.path "core::ascii::ascii_char::AsciiChar" ] :=
94-
repeat (| Value.StructTuple "core::ascii::ascii_char::AsciiChar::Null" [], N |) in
94+
repeat (Value.StructTuple "core::ascii::ascii_char::AsciiChar::Null" []) N in
9595
let~ _ : Ty.tuple [] :=
9696
M.write (|
9797
M.SubPointer.get_array_field (| output, Value.Integer IntegerKind.Usize 0 |),
@@ -150,7 +150,7 @@ Module escape.
150150
M.read (| M.get_constant "core::escape::hex_escape_discriminant" |) in
151151
let~ output :
152152
Ty.apply (Ty.path "array") [ N ] [ Ty.path "core::ascii::ascii_char::AsciiChar" ] :=
153-
repeat (| Value.StructTuple "core::ascii::ascii_char::AsciiChar::Null" [], N |) in
153+
repeat (Value.StructTuple "core::ascii::ascii_char::AsciiChar::Null" []) N in
154154
let~ hi : Ty.path "core::ascii::ascii_char::AsciiChar" :=
155155
M.read (|
156156
M.SubPointer.get_array_field (|
@@ -231,7 +231,7 @@ Module escape.
231231
M.read (| M.get_constant "core::escape::verbatim_discriminant" |) in
232232
let~ output :
233233
Ty.apply (Ty.path "array") [ N ] [ Ty.path "core::ascii::ascii_char::AsciiChar" ] :=
234-
repeat (| Value.StructTuple "core::ascii::ascii_char::AsciiChar::Null" [], N |) in
234+
repeat (Value.StructTuple "core::ascii::ascii_char::AsciiChar::Null" []) N in
235235
let~ _ : Ty.tuple [] :=
236236
M.write (|
237237
M.SubPointer.get_array_field (| output, Value.Integer IntegerKind.Usize 0 |),
@@ -475,7 +475,7 @@ Module escape.
475475
ltac:(M.monadic
476476
(let~ arr :
477477
Ty.apply (Ty.path "array") [ Value.Integer IntegerKind.Usize 256 ] [ Ty.path "u8" ] :=
478-
repeat (| Value.Integer IntegerKind.U8 0, Value.Integer IntegerKind.Usize 256 |) in
478+
repeat (Value.Integer IntegerKind.U8 0) (Value.Integer IntegerKind.Usize 256) in
479479
let~ idx : Ty.path "usize" := Value.Integer IntegerKind.Usize 0 in
480480
let~ _ : Ty.tuple [] :=
481481
M.read (|
@@ -683,7 +683,7 @@ Module escape.
683683
|) in
684684
let~ output :
685685
Ty.apply (Ty.path "array") [ N ] [ Ty.path "core::ascii::ascii_char::AsciiChar" ] :=
686-
repeat (| Value.StructTuple "core::ascii::ascii_char::AsciiChar::Null" [], N |) in
686+
repeat (Value.StructTuple "core::ascii::ascii_char::AsciiChar::Null" []) N in
687687
let~ _ : Ty.tuple [] :=
688688
M.write (|
689689
M.SubPointer.get_array_field (| output, Value.Integer IntegerKind.Usize 3 |),
@@ -1174,8 +1174,7 @@ Module escape.
11741174
(Value.StructRecord
11751175
"core::escape::EscapeIterInner"
11761176
[
1177-
("data",
1178-
repeat (| Value.StructTuple "core::ascii::ascii_char::AsciiChar::Null" [], N |));
1177+
("data", repeat (Value.StructTuple "core::ascii::ascii_char::AsciiChar::Null" []) N);
11791178
("alive",
11801179
Value.StructRecord
11811180
"core::ops::range::Range"

0 commit comments

Comments
 (0)