Code.v 1.68 KB
 Jacques-Henri Jourdan committed Oct 25, 2018 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 ``````From iris.heap_lang Require Import notation lib.assert. From iris_time Require Import MachineIntegers. Notation ROOT x := (InjL x). Notation ROOTV x := (InjLV x). Notation LINK x := (InjR x). Notation LINKV x := (InjRV x). Notation "'match:' e0 'with' 'ROOT' ( r , v ) => e1 | 'LINK' x => e2 'end'" := (Match e0 "__x" (let: r%bind := Fst "__x" in let: v%bind := Snd "__x" in e1) x%bind e2) (e0, r, v, e1, x, e2 at level 200, only parsing) : expr_scope. Definition make : val := λ: "v", ref (ROOT (#0, "v")). Definition find : val := rec: "find" "x" := match: !"x" with ROOT (<>, <>) => "x" | LINK "y" => let: "z" := "find" "y" in "x" <- LINK "z";; "z" end. Definition eq : val := λ: "x" "y", find "x" = find "y". Definition get : val := λ: "x", let: "x" := find "x" in match: !"x" with ROOT (<>, "v") => "v" | LINK <> => assert: #false end. Definition set : val := λ: "x" "v", let: "x" := find "x" in match: !"x" with ROOT ("r", <>) => "x" <- ROOT ("r", "v") | LINK <> => assert: #false end. Definition link : val := λ: "x" "y", if: "x" = "y" then "x" else match: !"x" with ROOT ("rx", "vx") => match: !"y" with ROOT ("ry", <>) => if: "rx" < "ry" then "x" <- LINK "y";; "y" else if: "ry" < "rx" then "y" <- LINK "x";; "x" else "y" <- LINK "x";; `````` Jacques-Henri Jourdan committed Oct 29, 2018 59 `````` "x" <- ROOT (machine_int_add "rx" #1, "vx");; `````` Jacques-Henri Jourdan committed Oct 25, 2018 60 61 62 63 64 65 66 67 68 69 `````` "x" | LINK <> => assert: #false end | LINK <> => assert: #false end. Definition union : val := λ: "x" "y", link (find "x") (find "y").``````