Skip to content

Commit 2e0d08e

Browse files
clarusclarus
authored
Merge pull request #534 from formal-land/guillaume-claret@s-assign-write
Replace assign by the existing write method
2 parents 3d20908 + 8d8ff12 commit 2e0d08e

Some content is hidden

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

46 files changed

+261
-287
lines changed

‎CoqOfRust/M.v

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -773,8 +773,6 @@ Definition get_struct_record_field
773773

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

776-
Parameter assign : Value.t -> Value.t -> M.
777-
778776
Definition get_struct_tuple_field_or_break_match
779777
(value : Value.t) (constructor : string) (index : Z) :
780778
M :=

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

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -24,7 +24,7 @@ Definition with_impls (τ : list Ty.t) (α : list Value.t) : M :=
2424
M.read (|
2525
let x := M.copy (| func |) in
2626
let _ :=
27-
M.assign (|
27+
M.write (|
2828
x,
2929
M.call_closure (|
3030
M.get_trait_method (| "core::default::Default", impl_Default, [], "default", [] |),
@@ -33,7 +33,7 @@ Definition with_impls (τ : list Ty.t) (α : list Value.t) : M :=
3333
|) in
3434
let y := M.copy (| func2 |) in
3535
let _ :=
36-
M.assign (|
36+
M.write (|
3737
y,
3838
M.call_closure (|
3939
M.get_trait_method (| "core::default::Default", impl_Default'1, [], "default", [] |),

‎CoqOfRust/examples/default/examples/ink_contracts/basic_contract_caller.v

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -119,7 +119,7 @@ Module Impl_basic_contract_caller_OtherContract.
119119
(let self := M.alloc (| self |) in
120120
M.read (|
121121
let _ :=
122-
M.assign (|
122+
M.write (|
123123
M.get_struct_record_field
124124
(M.read (| self |))
125125
"basic_contract_caller::OtherContract"

‎CoqOfRust/examples/default/examples/ink_contracts/conditional_compilation.v

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -306,7 +306,7 @@ Module Impl_conditional_compilation_ConditionalCompilation.
306306
(let self := M.alloc (| self |) in
307307
M.read (|
308308
let _ :=
309-
M.assign (|
309+
M.write (|
310310
M.get_struct_record_field
311311
(M.read (| self |))
312312
"conditional_compilation::ConditionalCompilation"
@@ -450,7 +450,7 @@ Module Impl_conditional_compilation_ConditionalCompilation.
450450
|)
451451
|) in
452452
let _ :=
453-
M.assign (|
453+
M.write (|
454454
M.get_struct_record_field
455455
(M.read (| self |))
456456
"conditional_compilation::ConditionalCompilation"
@@ -526,7 +526,7 @@ Module Impl_conditional_compilation_Flip_for_conditional_compilation_Conditional
526526
(let self := M.alloc (| self |) in
527527
M.read (|
528528
let _ :=
529-
M.assign (|
529+
M.write (|
530530
M.get_struct_record_field
531531
(M.read (| self |))
532532
"conditional_compilation::ConditionalCompilation"
@@ -632,7 +632,7 @@ Module Impl_conditional_compilation_Flip_for_conditional_compilation_Conditional
632632
|)
633633
|) in
634634
let _ :=
635-
M.assign (|
635+
M.write (|
636636
M.get_struct_record_field
637637
(M.read (| self |))
638638
"conditional_compilation::ConditionalCompilation"

‎CoqOfRust/examples/default/examples/ink_contracts/custom_allocator.v

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -98,7 +98,7 @@ Module Impl_custom_allocator_CustomAllocator.
9898
(let self := M.alloc (| self |) in
9999
M.read (|
100100
let _ :=
101-
M.assign (|
101+
M.write (|
102102
M.call_closure (|
103103
M.get_trait_method (|
104104
"core::ops::index::IndexMut",

‎CoqOfRust/examples/default/examples/ink_contracts/erc1155.v

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -720,7 +720,7 @@ Module Impl_erc1155_Contract.
720720
let _ :=
721721
let β :=
722722
M.get_struct_record_field (M.read (| self |)) "erc1155::Contract" "token_id_nonce" in
723-
M.assign (| β, BinOp.Panic.add (| M.read (| β |), Value.Integer Integer.U128 1 |) |) in
723+
M.write (| β, BinOp.Panic.add (| M.read (| β |), Value.Integer Integer.U128 1 |) |) in
724724
let _ :=
725725
M.alloc (|
726726
M.call_closure (|
@@ -1037,7 +1037,7 @@ Module Impl_erc1155_Contract.
10371037
|) in
10381038
let _ :=
10391039
let β := sender_balance in
1040-
M.assign (| β, BinOp.Panic.sub (| M.read (| β |), M.read (| value |) |) |) in
1040+
M.write (| β, BinOp.Panic.sub (| M.read (| β |), M.read (| value |) |) |) in
10411041
let _ :=
10421042
M.alloc (|
10431043
M.call_closure (|
@@ -1084,7 +1084,7 @@ Module Impl_erc1155_Contract.
10841084
|) in
10851085
let _ :=
10861086
let β := recipient_balance in
1087-
M.assign (| β, BinOp.Panic.add (| M.read (| β |), M.read (| value |) |) |) in
1087+
M.write (| β, BinOp.Panic.add (| M.read (| β |), M.read (| value |) |) |) in
10881088
let _ :=
10891089
M.alloc (|
10901090
M.call_closure (|

‎CoqOfRust/examples/default/examples/ink_contracts/flipper.v

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -62,7 +62,7 @@ Module Impl_flipper_Flipper.
6262
(let self := M.alloc (| self |) in
6363
M.read (|
6464
let _ :=
65-
M.assign (|
65+
M.write (|
6666
M.get_struct_record_field (M.read (| self |)) "flipper::Flipper" "value",
6767
UnOp.Pure.not
6868
(M.read (|

‎CoqOfRust/examples/default/examples/ink_contracts/incrementer.v

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -65,7 +65,7 @@ Module Impl_incrementer_Incrementer.
6565
let _ :=
6666
let β :=
6767
M.get_struct_record_field (M.read (| self |)) "incrementer::Incrementer" "value" in
68-
M.assign (| β, BinOp.Panic.add (| M.read (| β |), M.read (| by_ |) |) |) in
68+
M.write (| β, BinOp.Panic.add (| M.read (| β |), M.read (| by_ |) |) |) in
6969
M.alloc (| Value.Tuple [] |)
7070
|)))
7171
| _, _ => M.impossible

‎CoqOfRust/examples/default/examples/ink_contracts/lang_err_integration_tests/contract_ref.v

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -251,7 +251,7 @@ Module Impl_contract_ref_FlipperRef.
251251
(let self := M.alloc (| self |) in
252252
M.read (|
253253
let _ :=
254-
M.assign (|
254+
M.write (|
255255
M.get_struct_record_field (M.read (| self |)) "contract_ref::FlipperRef" "value",
256256
UnOp.Pure.not
257257
(M.read (|

‎CoqOfRust/examples/default/examples/ink_contracts/lang_err_integration_tests/integration_flipper.v

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -145,7 +145,7 @@ Module Impl_integration_flipper_Flipper.
145145
(let self := M.alloc (| self |) in
146146
M.read (|
147147
let _ :=
148-
M.assign (|
148+
M.write (|
149149
M.get_struct_record_field (M.read (| self |)) "integration_flipper::Flipper" "value",
150150
UnOp.Pure.not
151151
(M.read (|

‎CoqOfRust/examples/default/examples/ink_contracts/multisig.v

Lines changed: 10 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -1277,12 +1277,12 @@ Module Impl_multisig_Multisig.
12771277
]
12781278
|)) in
12791279
let _ :=
1280-
M.assign (|
1280+
M.write (|
12811281
M.get_struct_record_field contract "multisig::Multisig" "owners",
12821282
M.read (| owners |)
12831283
|) in
12841284
let _ :=
1285-
M.assign (|
1285+
M.write (|
12861286
M.get_struct_record_field contract "multisig::Multisig" "transaction_list",
12871287
M.call_closure (|
12881288
M.get_trait_method (|
@@ -1296,7 +1296,7 @@ Module Impl_multisig_Multisig.
12961296
|)
12971297
|) in
12981298
let _ :=
1299-
M.assign (|
1299+
M.write (|
13001300
M.get_struct_record_field contract "multisig::Multisig" "requirement",
13011301
M.read (| requirement |)
13021302
|) in
@@ -2150,7 +2150,7 @@ Module Impl_multisig_Multisig.
21502150
|) in
21512151
let _ :=
21522152
let β := count in
2153-
M.assign (|
2153+
M.write (|
21542154
β,
21552155
BinOp.Panic.sub (|
21562156
M.read (| β |),
@@ -2312,7 +2312,7 @@ Module Impl_multisig_Multisig.
23122312
|)
23132313
|) in
23142314
let _ :=
2315-
M.assign (|
2315+
M.write (|
23162316
M.get_struct_record_field (M.read (| self |)) "multisig::Multisig" "requirement",
23172317
M.read (| requirement |)
23182318
|) in
@@ -2409,7 +2409,7 @@ Module Impl_multisig_Multisig.
24092409
|)
24102410
|) in
24112411
let _ :=
2412-
M.assign (|
2412+
M.write (|
24132413
M.call_closure (|
24142414
M.get_trait_method (|
24152415
"core::ops::index::IndexMut",
@@ -2572,7 +2572,7 @@ Module Impl_multisig_Multisig.
25722572
|)
25732573
|) in
25742574
let _ :=
2575-
M.assign (|
2575+
M.write (|
25762576
M.get_struct_record_field (M.read (| self |)) "multisig::Multisig" "requirement",
25772577
M.read (| new_requirement |)
25782578
|) in
@@ -2706,7 +2706,7 @@ Module Impl_multisig_Multisig.
27062706
let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
27072707
let _ :=
27082708
let β := count in
2709-
M.assign (|
2709+
M.write (|
27102710
β,
27112711
BinOp.Panic.add (| M.read (| β |), Value.Integer Integer.U32 1 |)
27122712
|) in
@@ -2897,7 +2897,7 @@ Module Impl_multisig_Multisig.
28972897
"next_id"
28982898
|) in
28992899
let _ :=
2900-
M.assign (|
2900+
M.write (|
29012901
M.get_struct_record_field
29022902
(M.get_struct_record_field
29032903
(M.read (| self |))
@@ -3653,7 +3653,7 @@ Module Impl_multisig_Multisig.
36533653
|) in
36543654
let _ :=
36553655
let β := confirmation_count in
3656-
M.assign (|
3656+
M.write (|
36573657
β,
36583658
BinOp.Panic.sub (| M.read (| β |), Value.Integer Integer.U32 1 |)
36593659
|) in

‎CoqOfRust/examples/default/examples/ink_contracts/payment_channel.v

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1454,7 +1454,7 @@ Module Impl_payment_channel_PaymentChannel.
14541454
|)
14551455
|) in
14561456
let _ :=
1457-
M.assign (|
1457+
M.write (|
14581458
M.get_struct_record_field
14591459
(M.read (| self |))
14601460
"payment_channel::PaymentChannel"
@@ -1811,7 +1811,7 @@ Module Impl_payment_channel_PaymentChannel.
18111811
(M.read (| self |))
18121812
"payment_channel::PaymentChannel"
18131813
"withdrawn" in
1814-
M.assign (|
1814+
M.write (|
18151815
β,
18161816
BinOp.Panic.add (| M.read (| β |), M.read (| amount_to_withdraw |) |)
18171817
|) in

‎CoqOfRust/examples/default/examples/ink_contracts/set_code_hash.v

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -96,7 +96,7 @@ Module Impl_set_code_hash_Incrementer.
9696
let _ :=
9797
let β :=
9898
M.get_struct_record_field (M.read (| self |)) "set_code_hash::Incrementer" "count" in
99-
M.assign (| β, BinOp.Panic.add (| M.read (| β |), Value.Integer Integer.U32 1 |) |) in
99+
M.write (| β, BinOp.Panic.add (| M.read (| β |), Value.Integer Integer.U32 1 |) |) in
100100
let _ :=
101101
let _ :=
102102
M.alloc (|

‎CoqOfRust/examples/default/examples/ink_contracts/set_code_hash/updated_incrementer.v

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -185,7 +185,7 @@ Module Impl_updated_incrementer_Incrementer.
185185
(M.read (| self |))
186186
"updated_incrementer::Incrementer"
187187
"count" in
188-
M.assign (| β, BinOp.Panic.add (| M.read (| β |), Value.Integer Integer.U32 4 |) |) in
188+
M.write (| β, BinOp.Panic.add (| M.read (| β |), Value.Integer Integer.U32 4 |) |) in
189189
let _ :=
190190
let _ :=
191191
M.alloc (|

‎CoqOfRust/examples/default/examples/ink_contracts/trait_flipper.v

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -61,7 +61,7 @@ Module Impl_trait_flipper_Flip_for_trait_flipper_Flipper.
6161
(let self := M.alloc (| self |) in
6262
M.read (|
6363
let _ :=
64-
M.assign (|
64+
M.write (|
6565
M.get_struct_record_field (M.read (| self |)) "trait_flipper::Flipper" "value",
6666
UnOp.Pure.not
6767
(M.read (|

‎CoqOfRust/examples/default/examples/ink_contracts/trait_incrementer.v

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -51,7 +51,7 @@ Module Impl_trait_incrementer_Incrementer.
5151
(M.read (| self |))
5252
"trait_incrementer::Incrementer"
5353
"value" in
54-
M.assign (| β, BinOp.Panic.add (| M.read (| β |), M.read (| delta |) |) |) in
54+
M.write (| β, BinOp.Panic.add (| M.read (| β |), M.read (| delta |) |) |) in
5555
M.alloc (| Value.Tuple [] |)
5656
|)))
5757
| _, _ => M.impossible
@@ -119,7 +119,7 @@ Module Impl_trait_incrementer_Reset_for_trait_incrementer_Incrementer.
119119
(let self := M.alloc (| self |) in
120120
M.read (|
121121
let _ :=
122-
M.assign (|
122+
M.write (|
123123
M.get_struct_record_field
124124
(M.read (| self |))
125125
"trait_incrementer::Incrementer"

‎CoqOfRust/examples/default/examples/rust_book/custom_types/enums_testcase_linked_list.v

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -298,7 +298,7 @@ Definition main (τ : list Ty.t) (α : list Value.t) : M :=
298298
|)
299299
|) in
300300
let _ :=
301-
M.assign (|
301+
M.write (|
302302
list,
303303
M.call_closure (|
304304
M.get_associated_function (|
@@ -310,7 +310,7 @@ Definition main (τ : list Ty.t) (α : list Value.t) : M :=
310310
|)
311311
|) in
312312
let _ :=
313-
M.assign (|
313+
M.write (|
314314
list,
315315
M.call_closure (|
316316
M.get_associated_function (|
@@ -322,7 +322,7 @@ Definition main (τ : list Ty.t) (α : list Value.t) : M :=
322322
|)
323323
|) in
324324
let _ :=
325-
M.assign (|
325+
M.write (|
326326
list,
327327
M.call_closure (|
328328
M.get_associated_function (|

‎CoqOfRust/examples/default/examples/rust_book/flow_of_control/for_and_iterators_iter_mut.v

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -135,7 +135,7 @@ Definition main (τ : list Ty.t) (α : list Value.t) : M :=
135135
0
136136
|) in
137137
let name := M.copy (| γ0_0 |) in
138-
M.assign (|
138+
M.write (|
139139
M.read (| name |),
140140
M.read (|
141141
M.match_operator (|

‎CoqOfRust/examples/default/examples/rust_book/flow_of_control/infinite_loop.v

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -60,7 +60,7 @@ Definition main (τ : list Ty.t) (α : list Value.t) : M :=
6060
ltac:(M.monadic
6161
(let _ :=
6262
let β := count in
63-
M.assign (| β, BinOp.Panic.add (| M.read (| β |), Value.Integer Integer.U32 1 |) |) in
63+
M.write (| β, BinOp.Panic.add (| M.read (| β |), Value.Integer Integer.U32 1 |) |) in
6464
let _ :=
6565
M.match_operator (|
6666
M.alloc (| Value.Tuple [] |),

‎CoqOfRust/examples/default/examples/rust_book/flow_of_control/loop_returning_from_loops.v

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -28,7 +28,7 @@ Definition main (τ : list Ty.t) (α : list Value.t) : M :=
2828
ltac:(M.monadic
2929
(let _ :=
3030
let β := counter in
31-
M.assign (|
31+
M.write (|
3232
β,
3333
BinOp.Panic.add (| M.read (| β |), Value.Integer Integer.I32 1 |)
3434
|) in

‎CoqOfRust/examples/default/examples/rust_book/flow_of_control/match_destructuring_pointers_ref.v

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -235,7 +235,7 @@ Definition main (τ : list Ty.t) (α : list Value.t) : M :=
235235
(let m := M.alloc (| γ |) in
236236
let _ :=
237237
let β := M.read (| m |) in
238-
M.assign (|
238+
M.write (|
239239
β,
240240
BinOp.Panic.add (| M.read (| β |), Value.Integer Integer.I32 10 |)
241241
|) in

‎CoqOfRust/examples/default/examples/rust_book/flow_of_control/while.v

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -254,7 +254,7 @@ Definition main (τ : list Ty.t) (α : list Value.t) : M :=
254254
|) in
255255
let _ :=
256256
let β := n in
257-
M.assign (|
257+
M.write (|
258258
β,
259259
BinOp.Panic.add (| M.read (| β |), Value.Integer Integer.I32 1 |)
260260
|) in

‎CoqOfRust/examples/default/examples/rust_book/flow_of_control/while_let.v

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -87,7 +87,7 @@ Definition main (τ : list Ty.t) (α : list Value.t) : M :=
8787
|) in
8888
M.alloc (| Value.Tuple [] |) in
8989
let _ :=
90-
M.assign (|
90+
M.write (|
9191
optional,
9292
Value.StructTuple "core::option::Option::None" []
9393
|) in
@@ -139,7 +139,7 @@ Definition main (τ : list Ty.t) (α : list Value.t) : M :=
139139
|) in
140140
M.alloc (| Value.Tuple [] |) in
141141
let _ :=
142-
M.assign (|
142+
M.write (|
143143
optional,
144144
Value.StructTuple
145145
"core::option::Option::Some"

0 commit comments

Comments
 (0)