src/Pure/Concurrent/single_assignment_sequential.ML
author wenzelm
Sat, 20 Aug 2011 23:35:30 +0200
changeset 44338 700008399ee5
parent 35014 a725ff6ead26
permissions -rw-r--r--
refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;

(*  Title:      Pure/Concurrent/single_assignment_sequential.ML
    Author:     Makarius

Single-assignment variables (sequential version).
*)

structure Single_Assignment: SINGLE_ASSIGNMENT =
struct

abstype 'a var = Var of 'a SingleAssignment.saref
with

fun var _ = Var (SingleAssignment.saref ());

fun peek (Var var) = SingleAssignment.savalue var;

fun await v =
  (case peek v of
    SOME x => x
  | NONE => Thread.unavailable ());

fun assign (v as Var var) x =
  (case peek v of
    SOME _ => raise Fail "Duplicate assignment to variable"
  | NONE => SingleAssignment.saset (var, x));

end;

end;