Commit dd8fb7be authored by Ralf Jung's avatar Ralf Jung

get the pair out of the snapshot

parent db346db7
Pipeline #18196 passed with stage
in 18 minutes and 21 seconds
...@@ -13,7 +13,7 @@ Set Default Proof Using "Type". ...@@ -13,7 +13,7 @@ Set Default Proof Using "Type".
(* (*
newPair v := new_snapshot v :=
ref (ref (v, 0)) ref (ref (v, 0))
*) *)
Definition new_snapshot : val := Definition new_snapshot : val :=
...@@ -56,10 +56,10 @@ Definition read : val := ...@@ -56,10 +56,10 @@ Definition read : val :=
let (_, v') = !!xp in let (_, v') = !!xp in
if v = v' if v = v'
then (x, y) then (x, y)
else readPair l else read_with l
*) *)
Definition read_with_proph : val := Definition read_with_proph : val :=
rec: "readPair" "xp" "l" := rec: "read_with" "xp" "l" :=
let: "proph" := NewProph in let: "proph" := NewProph in
let: "x" := ! !"xp" in let: "x" := ! !"xp" in
let: "y" := !"l" in let: "y" := !"l" in
...@@ -68,7 +68,7 @@ Definition read_with_proph : val := ...@@ -68,7 +68,7 @@ Definition read_with_proph : val :=
resolve_proph: "proph" to: "v_eq" ;; resolve_proph: "proph" to: "v_eq" ;;
if: "v_eq" if: "v_eq"
then (Fst "x", "y") then (Fst "x", "y")
else "readPair" "xp" "l". else "read_with" "xp" "l".
(** The CMRA & functor we need. *) (** The CMRA & functor we need. *)
......
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