Code.v 1.68 KB
Newer Older
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";;
59
              "x" <- ROOT (machine_int_add "rx" #1, "vx");;
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").