Commit 0206d921 authored by William Mansky's avatar William Mansky

Another attempt at a higher-level data structure.

parent fadc131d
This diff is collapsed.
From gpfsl.examples Require Export kvnode_code.
Definition read_all : val :=
rec: "read_all" ["n"; "out"] :=
let: "snap" := !ᵃᶜ("n" + #version) in
if: "snap" `mod` #2 = #1 then "read_all" ["n"; "out"]
else (for: ("i" := #0; "i" < #Nd; "i" + #1)
"ni" <- !ᵃᶜ("n" + #data + "i");;
"read" ["ni"; "out" + (#Nd * "i")]);;
let: "v" := !ᵃᶜ("n" + #version) in
if: "v" = "snap" then # else "read_all" ["n"; "out"].
Definition write_all : val :=
λ: ["n"; "in"],
let: "v" := !ᵃᶜ("n" + #version) in
"n" + #version <-ʳᵉˡ "v" + #1 ;;
(for: ("i" := #0; "i" < #Nd; "i" + #1)
"ni" <- !ᵃᶜ("n" + #data + "i");;
"write" ["ni"; "in" + (#Nd * "i")]) ;;
"n" + #version <-ʳᵉˡ "v" + #2.
(* TODO: this is split in 2 funtions because solve_closed can't work at once. *)
(* Definition make_node : val :=
λ: [<>],
let: "n" := new [ #(Nd + 1) ] in
("n" + #version) <- #0 ;;
(for: ("i" := #0; "i" < #Nd; "i" + #1)
("n" + #data + "i") <- #0) ;;
"n". *)
Definition init_node : val :=
λ: ["n"],
("n" + #version) <- #0;;
(for: ("i" := #0; "i" < #Nd; "i" + #1)
("n" + #data + "i") <- #0);;
"n".
Definition make_node : val :=
λ: [<>], let: "n" := new [ #(Nd + 1)] in init_node ["n"].
......@@ -8,9 +8,9 @@ Notation next := 1.
Definition push : val :=
λ: ["st"],
let: "n" := new [ #2] in
("n" + #store) <-ʳᵉˡ !(make_node []);;
("n" + #store) <-ʳᵉˡ (make_node []);;
("n" + #next) <-ʳᵉˡ !"st";;
"st".
"n".
Definition nth : val :=
rec: "nth" ["st"; "i"] :=
......
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