swh:1:snp:aeaf3dbb58f5be84b565e73b5ade1503ee8cb6d6
Raw File
Tip revision: f94b06de7edcb61d3c49f19417e53dc7dc21d552 authored by Anish Tondwalkar on 22 June 2021, 08:13:54 UTC
updated README
Tip revision: f94b06d
pointersMap_noalias.ml
(* module M = Map.Make(struct type t = int let compare = compare end) *)

let find x m = m x
let add k v m kk = if kk = k then v else m kk

let ret x s = (x, s)
let dnib f ma s = match ma s with
    | (x, s') -> f x s'
let bind ma f s = match ma s with
    | (x, s') -> f x s'
let thenn ma mb = bind ma (fun _ -> mb)
let get s = (s,s)
let put x s = ((),x)

let decr (r:int) = bind get (fun (m) -> put (add r ((find r m) - 1) m))

let rec zero r = bind get (fun m -> let n = find r m in if n <= 0 then ret () else (thenn (decr r) (zero r)))

let test n1 n2 =
  if n1 < 0 || n2 < 0 then ret () else
  let r1 = 0 in let r2 = 1 in
  bind get (fun m ->
    (thenn
    (thenn
    (thenn (put (add r1 n1 (add r2 n2 m)))
           (zero r1))
           (zero r2))
           (bind get (fun m -> ret (assert (find r1 m = 0 && find r2 m = 0))))))
back to top