# HG changeset patch
# User wenzelm
# Date 1721039175 -7200
# Node ID 69cf3c308d6c78b73a46aee0991d9da97b626740
# Parent  fbb655bf62d4465cb4ee5989baf20a822feefd98
clarified signature: more operations;

diff -r fbb655bf62d4 -r 69cf3c308d6c src/Pure/General/table.ML
--- a/src/Pure/General/table.ML	Sun Jul 14 18:10:06 2024 +0200
+++ b/src/Pure/General/table.ML	Mon Jul 15 12:26:15 2024 +0200
@@ -66,7 +66,8 @@
   val insert_set: key -> set -> set
   val remove_set: key -> set -> set
   val make_set: key list -> set
-  val unsynchronized_cache: (key -> 'a) -> key -> 'a
+  type 'a cache_ops = {apply: key -> 'a, reset: unit -> unit}
+  val unsynchronized_cache: (key -> 'a) -> 'a cache_ops
 end;
 
 functor Table(Key: KEY): TABLE =
@@ -591,12 +592,13 @@
 
 (* cache *)
 
+type 'a cache_ops = {apply: key -> 'a, reset: unit -> unit};
+
 fun unsynchronized_cache f =
   let
     val cache1 = Unsynchronized.ref empty;
     val cache2 = Unsynchronized.ref empty;
-  in
-    fn x =>
+    fun apply x =
       (case lookup (! cache1) x of
         SOME y => y
       | NONE =>
@@ -605,8 +607,9 @@
           | NONE =>
               (case Exn.result f x of
                 Exn.Res y => (Unsynchronized.change cache1 (update (x, y)); y)
-              | Exn.Exn exn => (Unsynchronized.change cache2 (update (x, exn)); Exn.reraise exn))))
-  end;
+              | Exn.Exn exn => (Unsynchronized.change cache2 (update (x, exn)); Exn.reraise exn))));
+    fun reset () = (cache2 := empty; cache1 := empty);
+  in {apply = apply, reset = reset} end;
 
 
 (* ML pretty-printing *)
diff -r fbb655bf62d4 -r 69cf3c308d6c src/Pure/term_items.ML
--- a/src/Pure/term_items.ML	Sun Jul 14 18:10:06 2024 +0200
+++ b/src/Pure/term_items.ML	Mon Jul 15 12:26:15 2024 +0200
@@ -34,7 +34,8 @@
   val make1: key * 'a -> 'a table
   val make2: key * 'a -> key * 'a -> 'a table
   val make3: key * 'a -> key * 'a -> key * 'a -> 'a table
-  val unsynchronized_cache: (key -> 'a) -> key -> 'a
+  type 'a cache_ops = {apply: key -> 'a, reset: unit -> unit};
+  val unsynchronized_cache: (key -> 'a) -> 'a cache_ops
   type set = int table
   val add_set: key -> set -> set
   val make_set: key list -> set
@@ -86,6 +87,7 @@
 fun make2 e1 e2 = build (add e1 #> add e2);
 fun make3 e1 e2 e3 = build (add e1 #> add e2 #> add e3);
 
+type 'a cache_ops = 'a Table.cache_ops;
 val unsynchronized_cache = Table.unsynchronized_cache;
 
 
diff -r fbb655bf62d4 -r 69cf3c308d6c src/Pure/thm.ML
--- a/src/Pure/thm.ML	Sun Jul 14 18:10:06 2024 +0200
+++ b/src/Pure/thm.ML	Mon Jul 15 12:26:15 2024 +0200
@@ -1100,8 +1100,8 @@
                 SOME T' => T'
               | NONE => raise Fail "strip_shyps: bad type variable in proof term"));
         val map_ztyp =
-          ZTypes.unsynchronized_cache
-            (ZTerm.subst_type_same (ZTerm.ztyp_of o map_atyp o ZTerm.typ_of o ZTVar));
+          #apply (ZTypes.unsynchronized_cache
+            (ZTerm.subst_type_same (ZTerm.ztyp_of o map_atyp o ZTerm.typ_of o ZTVar)));
 
         val zproof' = ZTerm.map_proof_types {hyps = true} map_ztyp zproof;
         val proof' = Proofterm.map_proof_types (Term.map_atyps_same map_atyp) proof;
diff -r fbb655bf62d4 -r 69cf3c308d6c src/Pure/zterm.ML
--- a/src/Pure/zterm.ML	Sun Jul 14 18:10:06 2024 +0200
+++ b/src/Pure/zterm.ML	Mon Jul 15 12:26:15 2024 +0200
@@ -470,7 +470,7 @@
 
 fun instantiate_type_same instT =
   if ZTVars.is_empty instT then Same.same
-  else ZTypes.unsynchronized_cache (subst_type_same (Same.function (ZTVars.lookup instT)));
+  else #apply (ZTypes.unsynchronized_cache (subst_type_same (Same.function (ZTVars.lookup instT))));
 
 fun instantiate_term_same typ inst =
   subst_term_same typ (Same.function (ZVars.lookup inst));
@@ -587,7 +587,7 @@
   | ztyp_of (Type (c, [T])) = ZType1 (c, ztyp_of T)
   | ztyp_of (Type (c, ts)) = ZType (c, map ztyp_of ts);
 
-fun ztyp_cache () = Typtab.unsynchronized_cache ztyp_of;
+fun ztyp_cache () = #apply (Typtab.unsynchronized_cache ztyp_of);
 
 fun zterm_cache thy =
   let
@@ -622,7 +622,7 @@
   | typ_of (ZType1 (c, T)) = Type (c, [typ_of T])
   | typ_of (ZType (c, Ts)) = Type (c, map typ_of Ts);
 
-fun typ_cache () = ZTypes.unsynchronized_cache typ_of;
+fun typ_cache () = #apply (ZTypes.unsynchronized_cache typ_of);
 
 fun term_of thy =
   let
@@ -721,7 +721,7 @@
   let
     val lookup =
       if Vartab.is_empty tenv then K NONE
-      else ZVars.unsynchronized_cache (apsnd typ #> Envir.lookup envir #> Option.map zterm);
+      else #apply (ZVars.unsynchronized_cache (apsnd typ #> Envir.lookup envir #> Option.map zterm));
 
     val normT = norm_type_same ztyp tyenv;
 
@@ -870,7 +870,8 @@
     val typ_operation = #typ_operation ucontext {strip_sorts = true};
     val unconstrain_typ = Same.commit typ_operation;
     val unconstrain_ztyp =
-      ZTypes.unsynchronized_cache (Same.function_eq (op =) (typ_of #> unconstrain_typ #> ztyp_of));
+      #apply (ZTypes.unsynchronized_cache
+        (Same.function_eq (op =) (typ_of #> unconstrain_typ #> ztyp_of)));
     val unconstrain_zterm = zterm o Term.map_types typ_operation;
     val unconstrain_proof = Same.commit (map_proof_types {hyps = true} unconstrain_ztyp);
 
@@ -1087,10 +1088,10 @@
     val typ =
       if Names.is_empty tfrees then Same.same
       else
-        ZTypes.unsynchronized_cache
+        #apply (ZTypes.unsynchronized_cache
           (subst_type_same (fn ((a, i), S) =>
             if i = ~1 andalso Names.defined tfrees a then ZTVar ((a, idx), S)
-            else raise Same.SAME));
+            else raise Same.SAME)));
     val term =
       subst_term_same typ (fn ((x, i), T) =>
         if i = ~1 andalso Names.defined frees x then ZVar ((x, idx), T)
@@ -1112,10 +1113,10 @@
     let
       val tab = ZTVars.build (names |> fold (fn ((a, S), b) => ZTVars.add (((a, ~1), S), b)));
       val typ =
-        ZTypes.unsynchronized_cache (subst_type_same (fn v =>
+        #apply (ZTypes.unsynchronized_cache (subst_type_same (fn v =>
           (case ZTVars.lookup tab v of
             NONE => raise Same.SAME
-          | SOME w => ZTVar w)));
+          | SOME w => ZTVar w))));
     in map_proof_types {hyps = false} typ prf end;
 
 fun legacy_freezeT_proof t prf =
@@ -1124,7 +1125,7 @@
   | SOME f =>
       let
         val tvar = ztyp_of o Same.function f;
-        val typ = ZTypes.unsynchronized_cache (subst_type_same tvar);
+        val typ = #apply (ZTypes.unsynchronized_cache (subst_type_same tvar));
       in map_proof_types {hyps = false} typ prf end);
 
 
@@ -1158,7 +1159,7 @@
   if inc = 0 then Same.same
   else
     let fun tvar ((a, i), S) = if i >= 0 then ZTVar ((a, i + inc), S) else raise Same.SAME
-    in ZTypes.unsynchronized_cache (subst_type_same tvar) end;
+    in #apply (ZTypes.unsynchronized_cache (subst_type_same tvar)) end;
 
 fun incr_indexes_proof inc prf =
   let
@@ -1296,8 +1297,8 @@
     val algebra = Sign.classes_of thy;
 
     val typ =
-      ZTypes.unsynchronized_cache
-        (typ_of #> #typ_operation ucontext {strip_sorts = true} #> ztyp_of);
+      #apply (ZTypes.unsynchronized_cache
+        (typ_of #> #typ_operation ucontext {strip_sorts = true} #> ztyp_of));
 
     val typ_sort = #typ_operation ucontext {strip_sorts = false};