Commit 7bc008c5 authored by Ralf Jung's avatar Ralf Jung

introduce notation for value comparison

parent 472aa3bc
......@@ -184,6 +184,10 @@ Fixpoint val_for_compare (v : val) : val :=
| RecV f x e => RecV BAnon BAnon (Val $ LitV $ LitUnit)
end.
(** Now we can define how to compare values. *)
Notation "v1 =ᵥ v2" := (val_for_compare v1 = val_for_compare v2) (at level 70) : stdpp_scope.
Notation "v1 ≠ᵥ v2" := (val_for_compare v1 val_for_compare v2) (at level 70) : stdpp_scope.
(** The state: heaps of vals. *)
Record state : Type := {
heap: gmap loc val;
......@@ -518,7 +522,7 @@ Definition bin_op_eval_bool (op : bin_op) (b1 b2 : bool) : option base_lit :=
Definition bin_op_eval (op : bin_op) (v1 v2 : val) : option val :=
if decide (op = EqOp) then
Some $ LitV $ LitBool $ bool_decide (val_for_compare v1 = val_for_compare v2)
Some $ LitV $ LitBool $ bool_decide (v1 = v2)
else
match v1, v2 with
| LitV (LitInt n1), LitV (LitInt n2) => LitV <$> bin_op_eval_int op n1 n2
......@@ -636,13 +640,13 @@ Inductive head_step : expr → state → list observation → expr → state →
| CasFailS l v1 v2 vl σ :
vals_cas_compare_safe vl v1
σ.(heap) !! l = Some vl
val_for_compare vl val_for_compare v1
vl ≠ᵥ v1
head_step (CAS (Val $ LitV $ LitLoc l) (Val v1) (Val v2)) σ []
(Val $ LitV $ LitBool false) σ []
| CasSucS l v1 v2 vl σ :
vals_cas_compare_safe vl v1
σ.(heap) !! l = Some vl
val_for_compare vl = val_for_compare v1
vl = v1
head_step (CAS (Val $ LitV $ LitLoc l) (Val v1) (Val v2)) σ
[]
(Val $ LitV $ LitBool true) (state_upd_heap <[l:=v2]> σ)
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment