support for cached evaluation via weak_ref;

--- a/src/Pure/Concurrent/synchronized.ML	Mon May 08 23:00:17 2023 +0200
+++ b/src/Pure/Concurrent/synchronized.ML	Mon May 08 23:30:58 2023 +0200
@@ -14,6 +14,9 @@
   val guarded_access: 'a var -> ('a -> ('b * 'a) option) -> 'b
   val change_result: 'a var -> ('a -> 'b * 'a) -> 'b
   val change: 'a var -> ('a -> 'a) -> unit
+  type 'a cache
+  val cache: (unit -> 'a) -> 'a cache
+  val cache_eval: 'a cache -> 'a
 end;
 
 structure Synchronized: SYNCHRONIZED =
@@ -92,4 +95,24 @@
 
 end;
 
+
+(* cached evaluation via weak_ref *)
+
+abstype 'a cache =
+  Cache of {expr: unit -> 'a, var: 'a Unsynchronized.weak_ref option var}
+with
+
+fun cache expr =
+  Cache {expr = expr, var = var "Synchronized.cache" NONE};
+
+fun cache_eval (Cache {expr, var}) =
+  change_result var (fn state =>
+    (case state of
+      SOME (Unsynchronized.ref (SOME (Unsynchronized.ref result))) => (result, state)
+    | _ =>
+      let val result = expr ()
+      in (result, SOME (Unsynchronized.weak_ref result)) end));
+
 end;
+
+end;

--- a/src/Pure/Concurrent/unsynchronized.ML	Mon May 08 23:00:17 2023 +0200
+++ b/src/Pure/Concurrent/unsynchronized.ML	Mon May 08 23:30:58 2023 +0200
@@ -7,7 +7,6 @@
 signature UNSYNCHRONIZED =
 sig
   datatype ref = datatype ref
-  type 'a weak_ref = 'a ref option ref
   val := : 'a ref * 'a -> unit
   val ! : 'a ref -> 'a
   val change: 'a ref -> ('a -> 'a) -> unit
@@ -16,6 +15,8 @@
   val dec: int ref -> int
   val add: int ref -> int -> int
   val setmp: 'a ref -> 'a -> ('b -> 'c) -> 'b -> 'c
+  type 'a weak_ref = 'a ref option ref
+  val weak_ref: 'a -> 'a weak_ref
 end;
 
 structure Unsynchronized: UNSYNCHRONIZED =
@@ -23,8 +24,6 @@
 
 datatype ref = datatype ref;
 
-type 'a weak_ref = 'a ref option ref;
-
 val op := = op :=;
 val ! = !;
 
@@ -44,6 +43,9 @@
       val _ = flag := orig_value;
     in Exn.release result end) ();
 
+type 'a weak_ref = 'a ref option ref;
+fun weak_ref a = Weak.weak (SOME (ref a));
+
 end;
 
 ML_Name_Space.forget_val "ref";