Skip to content

Commit

Permalink
fix: fix translation of constructors without parameters
Browse files Browse the repository at this point in the history
  • Loading branch information
@clarus
clarus committed May 26, 2024
1 parent 844ca0e commit fcf6cb5
Show file tree
Hide file tree
Showing 183 changed files with 5,573 additions and 994 deletions.
10 changes: 10 additions & 0 deletions CoqOfRust/M.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -822,6 +822,16 @@ Definition is_constant_or_break_match (value expected_value : Value.t) : M :=
else
break_match.

Definition is_struct_tuple (value : Value.t) (constructor : string) : M :=
match value with
| Value.StructTuple current_constructor _ =>
if String.eqb current_constructor constructor then
pure (Value.Tuple [])
else
break_match
| _ => break_match
end.

Parameter pointer_coercion : Value.t -> Value.t.

(** This function is explicitely called in the Rust AST, and should take two
Expand Down
4 changes: 3 additions & 1 deletion CoqOfRust/alloc/borrow.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -450,7 +450,9 @@ Module borrow.
[
fun γ =>
ltac:(M.monadic
(M.alloc (|
(let _ :=
M.is_struct_tuple (| γ, "alloc::borrow::Cow::Borrowed" |) in
M.alloc (|
M.never_to_any (|
M.call_closure (|
M.get_function (| "core::panicking::panic", [] |),
Expand Down
7 changes: 6 additions & 1 deletion CoqOfRust/alloc/collections/binary_heap/mod.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2716,7 +2716,12 @@ Module collections.
[
fun γ =>
ltac:(M.monadic
(M.alloc (|
(let _ :=
M.is_struct_tuple (|
γ,
"core::option::Option::None"
|) in
M.alloc (|
M.never_to_any (| M.read (| M.break (||) |) |)
|)));
fun γ =>
Expand Down
14 changes: 12 additions & 2 deletions CoqOfRust/alloc/collections/btree/append.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -254,7 +254,12 @@ Module collections.
[
fun γ =>
ltac:(M.monadic
(M.alloc (|
(let _ :=
M.is_struct_tuple (|
γ,
"core::option::Option::None"
|) in
M.alloc (|
M.never_to_any (| M.read (| M.break (||) |) |)
|)));
fun γ =>
Expand Down Expand Up @@ -666,7 +671,12 @@ Module collections.
[
fun γ =>
ltac:(M.monadic
(M.alloc (|
(let _ :=
M.is_struct_tuple (|
γ,
"core::option::Option::None"
|) in
M.alloc (|
M.never_to_any (|
M.read (|
M.break (||)
Expand Down
8 changes: 6 additions & 2 deletions CoqOfRust/alloc/collections/btree/dedup_sorted_iter.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -128,7 +128,9 @@ Module collections.
next));
fun γ =>
ltac:(M.monadic
(M.alloc (|
(let _ :=
M.is_struct_tuple (| γ, "core::option::Option::None" |) in
M.alloc (|
M.never_to_any (|
M.read (|
M.return_ (|
Expand Down Expand Up @@ -174,7 +176,9 @@ Module collections.
peeked));
fun γ =>
ltac:(M.monadic
(M.alloc (|
(let _ :=
M.is_struct_tuple (| γ, "core::option::Option::None" |) in
M.alloc (|
M.never_to_any (|
M.read (|
M.return_ (|
Expand Down
2 changes: 2 additions & 0 deletions CoqOfRust/alloc/collections/btree/fix.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -466,6 +466,8 @@ Module collections.
"core::result::Result::Ok",
0
|) in
let _ :=
M.is_struct_tuple (| γ0_0, "core::option::Option::None" |) in
M.alloc (|
M.never_to_any (|
M.read (| M.return_ (| Value.Bool true |) |)
Expand Down
49 changes: 35 additions & 14 deletions CoqOfRust/alloc/collections/btree/map.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -6687,7 +6687,8 @@ Module collections.
[
fun γ =>
ltac:(M.monadic
(M.alloc (|
(let _ := M.is_struct_tuple (| γ, "core::option::Option::None" |) in
M.alloc (|
Value.StructTuple
"alloc::collections::btree::map::entry::Entry::Vacant"
[
Expand Down Expand Up @@ -8168,7 +8169,8 @@ Module collections.
[
fun γ =>
ltac:(M.monadic
(M.alloc (|
(let _ := M.is_struct_tuple (| γ, "core::option::Option::None" |) in
M.alloc (|
M.never_to_any (|
M.read (|
M.return_ (|
Expand Down Expand Up @@ -8450,7 +8452,9 @@ Module collections.
[
fun γ =>
ltac:(M.monadic
(M.alloc (|
(let _ :=
M.is_struct_tuple (| γ, "core::option::Option::None" |) in
M.alloc (|
M.never_to_any (|
M.read (|
M.return_ (|
Expand Down Expand Up @@ -8720,7 +8724,8 @@ Module collections.
[
fun γ =>
ltac:(M.monadic
(M.alloc (|
(let _ := M.is_struct_tuple (| γ, "core::option::Option::None" |) in
M.alloc (|
M.never_to_any (|
M.read (|
M.return_ (|
Expand Down Expand Up @@ -9002,7 +9007,9 @@ Module collections.
[
fun γ =>
ltac:(M.monadic
(M.alloc (|
(let _ :=
M.is_struct_tuple (| γ, "core::option::Option::None" |) in
M.alloc (|
M.never_to_any (|
M.read (|
M.return_ (|
Expand Down Expand Up @@ -14921,7 +14928,9 @@ Module collections.
[
fun γ =>
ltac:(M.monadic
(M.alloc (|
(let _ :=
M.is_struct_tuple (| γ, "core::option::Option::None" |) in
M.alloc (|
M.never_to_any (| M.read (| M.break (||) |) |)
|)));
fun γ =>
Expand Down Expand Up @@ -15908,7 +15917,8 @@ Module collections.
[
fun γ =>
ltac:(M.monadic
(let~ _ :=
(let _ := M.is_struct_tuple (| γ, "core::option::Option::None" |) in
let~ _ :=
M.write (|
M.SubPointer.get_struct_record_field (|
M.read (| self |),
Expand Down Expand Up @@ -16322,7 +16332,8 @@ Module collections.
[
fun γ =>
ltac:(M.monadic
(let~ _ :=
(let _ := M.is_struct_tuple (| γ, "core::option::Option::None" |) in
let~ _ :=
M.write (|
M.SubPointer.get_struct_record_field (|
M.read (| self |),
Expand Down Expand Up @@ -17531,7 +17542,8 @@ Module collections.
[
fun γ =>
ltac:(M.monadic
(let~ _ :=
(let _ := M.is_struct_tuple (| γ, "core::option::Option::None" |) in
let~ _ :=
M.write (|
M.SubPointer.get_struct_record_field (|
M.read (| self |),
Expand Down Expand Up @@ -17992,7 +18004,8 @@ Module collections.
[
fun γ =>
ltac:(M.monadic
(let~ _ :=
(let _ := M.is_struct_tuple (| γ, "core::option::Option::None" |) in
let~ _ :=
M.write (|
M.SubPointer.get_struct_record_field (|
M.read (| self |),
Expand Down Expand Up @@ -19413,7 +19426,8 @@ Module collections.
[
fun γ =>
ltac:(M.monadic
(M.alloc (|
(let _ := M.is_struct_tuple (| γ, "core::option::Option::None" |) in
M.alloc (|
M.call_closure (|
M.get_associated_function (|
Ty.apply
Expand Down Expand Up @@ -20132,7 +20146,8 @@ Module collections.
[
fun γ =>
ltac:(M.monadic
(M.alloc (|
(let _ := M.is_struct_tuple (| γ, "core::option::Option::None" |) in
M.alloc (|
M.call_closure (|
M.get_associated_function (|
Ty.apply
Expand Down Expand Up @@ -21090,7 +21105,8 @@ Module collections.
[
fun γ =>
ltac:(M.monadic
(M.match_operator (|
(let _ := M.is_struct_tuple (| γ, "core::option::Option::None" |) in
M.match_operator (|
M.alloc (|
M.call_closure (|
M.get_associated_function (|
Expand Down Expand Up @@ -21131,6 +21147,8 @@ Module collections.
ltac:(M.monadic
(let root := M.copy (| γ |) in
let γ := M.read (| γ |) in
let _ :=
M.is_struct_tuple (| γ, "core::option::Option::None" |) in
M.alloc (|
M.never_to_any (|
M.read (|
Expand Down Expand Up @@ -21818,7 +21836,8 @@ Module collections.
[
fun γ =>
ltac:(M.monadic
(M.match_operator (|
(let _ := M.is_struct_tuple (| γ, "core::option::Option::None" |) in
M.match_operator (|
M.alloc (|
M.call_closure (|
M.get_associated_function (|
Expand Down Expand Up @@ -21859,6 +21878,8 @@ Module collections.
ltac:(M.monadic
(let root := M.copy (| γ |) in
let γ := M.read (| γ |) in
let _ :=
M.is_struct_tuple (| γ, "core::option::Option::None" |) in
M.alloc (|
M.never_to_any (|
M.read (|
Expand Down
3 changes: 2 additions & 1 deletion CoqOfRust/alloc/collections/btree/map/entry.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1299,7 +1299,8 @@ Module collections.
[
fun γ =>
ltac:(M.monadic
(let~ map :=
(let _ := M.is_struct_tuple (| γ, "core::option::Option::None" |) in
let~ map :=
M.alloc (|
M.call_closure (|
M.get_associated_function (|
Expand Down
17 changes: 13 additions & 4 deletions CoqOfRust/alloc/collections/btree/merge_iter.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -551,7 +551,8 @@ Module collections.
M.alloc (| Value.Tuple [] |)));
fun γ =>
ltac:(M.monadic
(let~ _ :=
(let _ := M.is_struct_tuple (| γ, "core::option::Option::None" |) in
let~ _ :=
M.write (|
a_next,
M.call_closure (|
Expand Down Expand Up @@ -641,7 +642,9 @@ Module collections.
[
fun γ =>
ltac:(M.monadic
(M.write (|
(let _ :=
M.is_struct_tuple (| γ, "core::cmp::Ordering::Less" |) in
M.write (|
M.SubPointer.get_struct_record_field (|
M.read (| self |),
"alloc::collections::btree::merge_iter::MergeIterInner",
Expand Down Expand Up @@ -682,7 +685,9 @@ Module collections.
|)));
fun γ =>
ltac:(M.monadic
(M.write (|
(let _ :=
M.is_struct_tuple (| γ, "core::cmp::Ordering::Greater" |) in
M.write (|
M.SubPointer.get_struct_record_field (|
M.read (| self |),
"alloc::collections::btree::merge_iter::MergeIterInner",
Expand Down Expand Up @@ -721,7 +726,11 @@ Module collections.
]
|)
|)));
fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
fun γ =>
ltac:(M.monadic
(let _ :=
M.is_struct_tuple (| γ, "core::cmp::Ordering::Equal" |) in
M.alloc (| Value.Tuple [] |)))
]
|)));
fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
Expand Down
16 changes: 14 additions & 2 deletions CoqOfRust/alloc/collections/btree/navigate.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2491,6 +2491,7 @@ Module collections.
fun γ =>
ltac:(M.monadic
(let γ := M.read (| γ |) in
let _ := M.is_struct_tuple (| γ, "core::option::Option::None" |) in
M.alloc (| Value.StructTuple "core::option::Option::None" [] |)));
fun γ =>
ltac:(M.monadic
Expand Down Expand Up @@ -2661,6 +2662,7 @@ Module collections.
fun γ =>
ltac:(M.monadic
(let γ := M.read (| γ |) in
let _ := M.is_struct_tuple (| γ, "core::option::Option::None" |) in
M.alloc (| Value.StructTuple "core::option::Option::None" [] |)));
fun γ =>
ltac:(M.monadic
Expand Down Expand Up @@ -6639,7 +6641,12 @@ Module collections.
|)));
fun γ =>
ltac:(M.monadic
(M.alloc (|
(let _ :=
M.is_struct_tuple (|
γ,
"core::option::Option::None"
|) in
M.alloc (|
M.never_to_any (|
M.read (|
M.return_ (|
Expand Down Expand Up @@ -6939,7 +6946,12 @@ Module collections.
|)));
fun γ =>
ltac:(M.monadic
(M.alloc (|
(let _ :=
M.is_struct_tuple (|
γ,
"core::option::Option::None"
|) in
M.alloc (|
M.never_to_any (|
M.read (|
M.return_ (|
Expand Down
Loading

0 comments on commit fcf6cb5

Please sign in to comment.