Skip to content

Commit 38e12ee

Browse files
clarusclarus
committed
fix: fix translation of constructors without parameters
1 parent 844ca0e commit 38e12ee

File tree

184 files changed

+5573
-995
lines changed

Some content is hidden

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

184 files changed

+5573
-995
lines changed

‎CoqOfRust/M.v‎

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -822,6 +822,16 @@ Definition is_constant_or_break_match (value expected_value : Value.t) : M :=
822822
else
823823
break_match.
824824

825+
Definition is_struct_tuple (value : Value.t) (constructor : string) : M :=
826+
match value with
827+
| Value.StructTuple current_constructor _ =>
828+
if String.eqb current_constructor constructor then
829+
pure (Value.Tuple [])
830+
else
831+
break_match
832+
| _ => break_match
833+
end.
834+
825835
Parameter pointer_coercion : Value.t -> Value.t.
826836

827837
(** This function is explicitely called in the Rust AST, and should take two

‎CoqOfRust/alloc/borrow.v‎

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -450,7 +450,9 @@ Module borrow.
450450
[
451451
fun γ =>
452452
ltac:(M.monadic
453-
(M.alloc (|
453+
(let _ :=
454+
M.is_struct_tuple (| γ, "alloc::borrow::Cow::Borrowed" |) in
455+
M.alloc (|
454456
M.never_to_any (|
455457
M.call_closure (|
456458
M.get_function (| "core::panicking::panic", [] |),

‎CoqOfRust/alloc/collections/binary_heap/mod.v‎

Lines changed: 6 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2716,7 +2716,12 @@ Module collections.
27162716
[
27172717
fun γ =>
27182718
ltac:(M.monadic
2719-
(M.alloc (|
2719+
(let _ :=
2720+
M.is_struct_tuple (|
2721+
γ,
2722+
"core::option::Option::None"
2723+
|) in
2724+
M.alloc (|
27202725
M.never_to_any (| M.read (| M.break (||) |) |)
27212726
|)));
27222727
fun γ =>

‎CoqOfRust/alloc/collections/btree/append.v‎

Lines changed: 12 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -254,7 +254,12 @@ Module collections.
254254
[
255255
fun γ =>
256256
ltac:(M.monadic
257-
(M.alloc (|
257+
(let _ :=
258+
M.is_struct_tuple (|
259+
γ,
260+
"core::option::Option::None"
261+
|) in
262+
M.alloc (|
258263
M.never_to_any (| M.read (| M.break (||) |) |)
259264
|)));
260265
fun γ =>
@@ -666,7 +671,12 @@ Module collections.
666671
[
667672
fun γ =>
668673
ltac:(M.monadic
669-
(M.alloc (|
674+
(let _ :=
675+
M.is_struct_tuple (|
676+
γ,
677+
"core::option::Option::None"
678+
|) in
679+
M.alloc (|
670680
M.never_to_any (|
671681
M.read (|
672682
M.break (||)

‎CoqOfRust/alloc/collections/btree/dedup_sorted_iter.v‎

Lines changed: 6 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -128,7 +128,9 @@ Module collections.
128128
next));
129129
fun γ =>
130130
ltac:(M.monadic
131-
(M.alloc (|
131+
(let _ :=
132+
M.is_struct_tuple (| γ, "core::option::Option::None" |) in
133+
M.alloc (|
132134
M.never_to_any (|
133135
M.read (|
134136
M.return_ (|
@@ -174,7 +176,9 @@ Module collections.
174176
peeked));
175177
fun γ =>
176178
ltac:(M.monadic
177-
(M.alloc (|
179+
(let _ :=
180+
M.is_struct_tuple (| γ, "core::option::Option::None" |) in
181+
M.alloc (|
178182
M.never_to_any (|
179183
M.read (|
180184
M.return_ (|

‎CoqOfRust/alloc/collections/btree/fix.v‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -466,6 +466,8 @@ Module collections.
466466
"core::result::Result::Ok",
467467
0
468468
|) in
469+
let _ :=
470+
M.is_struct_tuple (| γ0_0, "core::option::Option::None" |) in
469471
M.alloc (|
470472
M.never_to_any (|
471473
M.read (| M.return_ (| Value.Bool true |) |)

‎CoqOfRust/alloc/collections/btree/map.v‎

Lines changed: 35 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -6687,7 +6687,8 @@ Module collections.
66876687
[
66886688
fun γ =>
66896689
ltac:(M.monadic
6690-
(M.alloc (|
6690+
(let _ := M.is_struct_tuple (| γ, "core::option::Option::None" |) in
6691+
M.alloc (|
66916692
Value.StructTuple
66926693
"alloc::collections::btree::map::entry::Entry::Vacant"
66936694
[
@@ -8168,7 +8169,8 @@ Module collections.
81688169
[
81698170
fun γ =>
81708171
ltac:(M.monadic
8171-
(M.alloc (|
8172+
(let _ := M.is_struct_tuple (| γ, "core::option::Option::None" |) in
8173+
M.alloc (|
81728174
M.never_to_any (|
81738175
M.read (|
81748176
M.return_ (|
@@ -8450,7 +8452,9 @@ Module collections.
84508452
[
84518453
fun γ =>
84528454
ltac:(M.monadic
8453-
(M.alloc (|
8455+
(let _ :=
8456+
M.is_struct_tuple (| γ, "core::option::Option::None" |) in
8457+
M.alloc (|
84548458
M.never_to_any (|
84558459
M.read (|
84568460
M.return_ (|
@@ -8720,7 +8724,8 @@ Module collections.
87208724
[
87218725
fun γ =>
87228726
ltac:(M.monadic
8723-
(M.alloc (|
8727+
(let _ := M.is_struct_tuple (| γ, "core::option::Option::None" |) in
8728+
M.alloc (|
87248729
M.never_to_any (|
87258730
M.read (|
87268731
M.return_ (|
@@ -9002,7 +9007,9 @@ Module collections.
90029007
[
90039008
fun γ =>
90049009
ltac:(M.monadic
9005-
(M.alloc (|
9010+
(let _ :=
9011+
M.is_struct_tuple (| γ, "core::option::Option::None" |) in
9012+
M.alloc (|
90069013
M.never_to_any (|
90079014
M.read (|
90089015
M.return_ (|
@@ -14921,7 +14928,9 @@ Module collections.
1492114928
[
1492214929
fun γ =>
1492314930
ltac:(M.monadic
14924-
(M.alloc (|
14931+
(let _ :=
14932+
M.is_struct_tuple (| γ, "core::option::Option::None" |) in
14933+
M.alloc (|
1492514934
M.never_to_any (| M.read (| M.break (||) |) |)
1492614935
|)));
1492714936
fun γ =>
@@ -15908,7 +15917,8 @@ Module collections.
1590815917
[
1590915918
fun γ =>
1591015919
ltac:(M.monadic
15911-
(let~ _ :=
15920+
(let _ := M.is_struct_tuple (| γ, "core::option::Option::None" |) in
15921+
let~ _ :=
1591215922
M.write (|
1591315923
M.SubPointer.get_struct_record_field (|
1591415924
M.read (| self |),
@@ -16322,7 +16332,8 @@ Module collections.
1632216332
[
1632316333
fun γ =>
1632416334
ltac:(M.monadic
16325-
(let~ _ :=
16335+
(let _ := M.is_struct_tuple (| γ, "core::option::Option::None" |) in
16336+
let~ _ :=
1632616337
M.write (|
1632716338
M.SubPointer.get_struct_record_field (|
1632816339
M.read (| self |),
@@ -17531,7 +17542,8 @@ Module collections.
1753117542
[
1753217543
fun γ =>
1753317544
ltac:(M.monadic
17534-
(let~ _ :=
17545+
(let _ := M.is_struct_tuple (| γ, "core::option::Option::None" |) in
17546+
let~ _ :=
1753517547
M.write (|
1753617548
M.SubPointer.get_struct_record_field (|
1753717549
M.read (| self |),
@@ -17992,7 +18004,8 @@ Module collections.
1799218004
[
1799318005
fun γ =>
1799418006
ltac:(M.monadic
17995-
(let~ _ :=
18007+
(let _ := M.is_struct_tuple (| γ, "core::option::Option::None" |) in
18008+
let~ _ :=
1799618009
M.write (|
1799718010
M.SubPointer.get_struct_record_field (|
1799818011
M.read (| self |),
@@ -19413,7 +19426,8 @@ Module collections.
1941319426
[
1941419427
fun γ =>
1941519428
ltac:(M.monadic
19416-
(M.alloc (|
19429+
(let _ := M.is_struct_tuple (| γ, "core::option::Option::None" |) in
19430+
M.alloc (|
1941719431
M.call_closure (|
1941819432
M.get_associated_function (|
1941919433
Ty.apply
@@ -20132,7 +20146,8 @@ Module collections.
2013220146
[
2013320147
fun γ =>
2013420148
ltac:(M.monadic
20135-
(M.alloc (|
20149+
(let _ := M.is_struct_tuple (| γ, "core::option::Option::None" |) in
20150+
M.alloc (|
2013620151
M.call_closure (|
2013720152
M.get_associated_function (|
2013820153
Ty.apply
@@ -21090,7 +21105,8 @@ Module collections.
2109021105
[
2109121106
fun γ =>
2109221107
ltac:(M.monadic
21093-
(M.match_operator (|
21108+
(let _ := M.is_struct_tuple (| γ, "core::option::Option::None" |) in
21109+
M.match_operator (|
2109421110
M.alloc (|
2109521111
M.call_closure (|
2109621112
M.get_associated_function (|
@@ -21131,6 +21147,8 @@ Module collections.
2113121147
ltac:(M.monadic
2113221148
(let root := M.copy (| γ |) in
2113321149
let γ := M.read (| γ |) in
21150+
let _ :=
21151+
M.is_struct_tuple (| γ, "core::option::Option::None" |) in
2113421152
M.alloc (|
2113521153
M.never_to_any (|
2113621154
M.read (|
@@ -21818,7 +21836,8 @@ Module collections.
2181821836
[
2181921837
fun γ =>
2182021838
ltac:(M.monadic
21821-
(M.match_operator (|
21839+
(let _ := M.is_struct_tuple (| γ, "core::option::Option::None" |) in
21840+
M.match_operator (|
2182221841
M.alloc (|
2182321842
M.call_closure (|
2182421843
M.get_associated_function (|
@@ -21859,6 +21878,8 @@ Module collections.
2185921878
ltac:(M.monadic
2186021879
(let root := M.copy (| γ |) in
2186121880
let γ := M.read (| γ |) in
21881+
let _ :=
21882+
M.is_struct_tuple (| γ, "core::option::Option::None" |) in
2186221883
M.alloc (|
2186321884
M.never_to_any (|
2186421885
M.read (|

‎CoqOfRust/alloc/collections/btree/map/entry.v‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1299,7 +1299,8 @@ Module collections.
12991299
[
13001300
fun γ =>
13011301
ltac:(M.monadic
1302-
(let~ map :=
1302+
(let _ := M.is_struct_tuple (| γ, "core::option::Option::None" |) in
1303+
let~ map :=
13031304
M.alloc (|
13041305
M.call_closure (|
13051306
M.get_associated_function (|

‎CoqOfRust/alloc/collections/btree/merge_iter.v‎

Lines changed: 13 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -551,7 +551,8 @@ Module collections.
551551
M.alloc (| Value.Tuple [] |)));
552552
fun γ =>
553553
ltac:(M.monadic
554-
(let~ _ :=
554+
(let _ := M.is_struct_tuple (| γ, "core::option::Option::None" |) in
555+
let~ _ :=
555556
M.write (|
556557
a_next,
557558
M.call_closure (|
@@ -641,7 +642,9 @@ Module collections.
641642
[
642643
fun γ =>
643644
ltac:(M.monadic
644-
(M.write (|
645+
(let _ :=
646+
M.is_struct_tuple (| γ, "core::cmp::Ordering::Less" |) in
647+
M.write (|
645648
M.SubPointer.get_struct_record_field (|
646649
M.read (| self |),
647650
"alloc::collections::btree::merge_iter::MergeIterInner",
@@ -682,7 +685,9 @@ Module collections.
682685
|)));
683686
fun γ =>
684687
ltac:(M.monadic
685-
(M.write (|
688+
(let _ :=
689+
M.is_struct_tuple (| γ, "core::cmp::Ordering::Greater" |) in
690+
M.write (|
686691
M.SubPointer.get_struct_record_field (|
687692
M.read (| self |),
688693
"alloc::collections::btree::merge_iter::MergeIterInner",
@@ -721,7 +726,11 @@ Module collections.
721726
]
722727
|)
723728
|)));
724-
fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
729+
fun γ =>
730+
ltac:(M.monadic
731+
(let _ :=
732+
M.is_struct_tuple (| γ, "core::cmp::Ordering::Equal" |) in
733+
M.alloc (| Value.Tuple [] |)))
725734
]
726735
|)));
727736
fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))

‎CoqOfRust/alloc/collections/btree/navigate.v‎

Lines changed: 14 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -2491,6 +2491,7 @@ Module collections.
24912491
fun γ =>
24922492
ltac:(M.monadic
24932493
(let γ := M.read (| γ |) in
2494+
let _ := M.is_struct_tuple (| γ, "core::option::Option::None" |) in
24942495
M.alloc (| Value.StructTuple "core::option::Option::None" [] |)));
24952496
fun γ =>
24962497
ltac:(M.monadic
@@ -2661,6 +2662,7 @@ Module collections.
26612662
fun γ =>
26622663
ltac:(M.monadic
26632664
(let γ := M.read (| γ |) in
2665+
let _ := M.is_struct_tuple (| γ, "core::option::Option::None" |) in
26642666
M.alloc (| Value.StructTuple "core::option::Option::None" [] |)));
26652667
fun γ =>
26662668
ltac:(M.monadic
@@ -6639,7 +6641,12 @@ Module collections.
66396641
|)));
66406642
fun γ =>
66416643
ltac:(M.monadic
6642-
(M.alloc (|
6644+
(let _ :=
6645+
M.is_struct_tuple (|
6646+
γ,
6647+
"core::option::Option::None"
6648+
|) in
6649+
M.alloc (|
66436650
M.never_to_any (|
66446651
M.read (|
66456652
M.return_ (|
@@ -6939,7 +6946,12 @@ Module collections.
69396946
|)));
69406947
fun γ =>
69416948
ltac:(M.monadic
6942-
(M.alloc (|
6949+
(let _ :=
6950+
M.is_struct_tuple (|
6951+
γ,
6952+
"core::option::Option::None"
6953+
|) in
6954+
M.alloc (|
69436955
M.never_to_any (|
69446956
M.read (|
69456957
M.return_ (|

0 commit comments

Comments
 (0)