# HG changeset patch # User wenzelm # Date 1733168112 -3600 # Node ID 58073f3d748a27b7e463499beb16ca23a65f4aad # Parent 8e4ca2c87e86476ca18c564eb3535accb8600157 tuned signature; diff -r 8e4ca2c87e86 -r 58073f3d748a src/Pure/General/table.ML --- a/src/Pure/General/table.ML Mon Dec 02 18:53:45 2024 +0100 +++ b/src/Pure/General/table.ML Mon Dec 02 20:35:12 2024 +0100 @@ -68,6 +68,7 @@ val make_set: key list -> set type 'a cache_ops = {apply: key -> 'a, reset: unit -> unit, size: unit -> int} val unsynchronized_cache: (key -> 'a) -> 'a cache_ops + val apply_unsynchronized_cache: (key -> 'a) -> key -> 'a end; functor Table(Key: KEY): TABLE = @@ -610,6 +611,8 @@ fun total_size () = size (! cache1) + size (! cache2); in {apply = apply, reset = reset, size = total_size} end; +fun apply_unsynchronized_cache f = #apply (unsynchronized_cache f); + (* ML pretty-printing *) diff -r 8e4ca2c87e86 -r 58073f3d748a src/Pure/Syntax/syntax_phases.ML --- a/src/Pure/Syntax/syntax_phases.ML Mon Dec 02 18:53:45 2024 +0100 +++ b/src/Pure/Syntax/syntax_phases.ML Mon Dec 02 20:35:12 2024 +0100 @@ -65,15 +65,14 @@ Markup.bound :: map (fn pos => Position.make_entity_markup def id Markup.boundN (name, pos)) ps; fun markup_entity_cache ctxt = - Symtab.unsynchronized_cache (fn c => + Symtab.apply_unsynchronized_cache (fn c => Syntax.get_consts (Proof_Context.syntax_of ctxt) c |> maps (Lexicon.unmark {case_class = markup_class ctxt, case_type = markup_type ctxt, case_const = markup_const ctxt, case_fixed = markup_free ctxt, - case_default = K []})) - |> #apply; + case_default = K []})); @@ -267,8 +266,8 @@ fun decode_term ctxt = let - val markup_free_cache = #apply (Symtab.unsynchronized_cache (markup_free ctxt)); - val markup_const_cache = #apply (Symtab.unsynchronized_cache (markup_const ctxt)); + val markup_free_cache = Symtab.apply_unsynchronized_cache (markup_free ctxt); + val markup_const_cache = Symtab.apply_unsynchronized_cache (markup_const ctxt); fun decode (result as (_: Position.report_text list, Exn.Exn _)) = result | decode (reports0, Exn.Res tm) = @@ -714,7 +713,7 @@ local fun extern_cache ctxt = - Symtab.unsynchronized_cache (fn c => + Symtab.apply_unsynchronized_cache (fn c => (case Syntax.get_consts (Proof_Context.syntax_of ctxt) c of [b] => b | bs => @@ -722,18 +721,16 @@ [] => c | [b] => b | _ => error ("Multiple logical entities for " ^ quote c ^ ": " ^ commas_quote bs))) - |> Proof_Context.extern_entity ctxt) - |> #apply; + |> Proof_Context.extern_entity ctxt); val var_or_skolem_cache = - Symtab.unsynchronized_cache (fn s => + Symtab.apply_unsynchronized_cache (fn s => (case Lexicon.read_variable s of SOME (x, i) => (case try Name.dest_skolem x of SOME x' => (Markup.skolem, Term.string_of_vname (x', i)) | NONE => (Markup.var, s)) - | NONE => (Markup.var, s))) - |> #apply; + | NONE => (Markup.var, s))); val typing_elem = YXML.output_markup_elem Markup.typing; val sorting_elem = YXML.output_markup_elem Markup.sorting; @@ -751,8 +748,8 @@ val extern = extern_cache ctxt; val free_or_skolem_cache = - Symtab.unsynchronized_cache (fn x => (markup_free ctxt x, Proof_Context.extern_fixed ctxt x)) - |> #apply; + Symtab.apply_unsynchronized_cache (fn x => + (markup_free ctxt x, Proof_Context.extern_fixed ctxt x)); val cache1 = Unsynchronized.ref (Ast.Table.empty: Markup.output Pretty.block Ast.Table.table); val cache2 = Unsynchronized.ref (Ast.Table.empty: Markup.output Pretty.block Ast.Table.table); diff -r 8e4ca2c87e86 -r 58073f3d748a src/Pure/term_items.ML --- a/src/Pure/term_items.ML Mon Dec 02 18:53:45 2024 +0100 +++ b/src/Pure/term_items.ML Mon Dec 02 20:35:12 2024 +0100 @@ -36,6 +36,7 @@ val make3: key * 'a -> key * 'a -> key * 'a -> 'a table type 'a cache_ops = {apply: key -> 'a, reset: unit -> unit, size: unit -> int}; val unsynchronized_cache: (key -> 'a) -> 'a cache_ops + val apply_unsynchronized_cache: (key -> 'a) -> key -> 'a type set = int table val add_set: key -> set -> set val make_set: key list -> set @@ -89,6 +90,7 @@ type 'a cache_ops = 'a Table.cache_ops; val unsynchronized_cache = Table.unsynchronized_cache; +val apply_unsynchronized_cache = Table.apply_unsynchronized_cache; (* set with order of addition *) diff -r 8e4ca2c87e86 -r 58073f3d748a src/Pure/thm.ML --- a/src/Pure/thm.ML Mon Dec 02 18:53:45 2024 +0100 +++ b/src/Pure/thm.ML Mon Dec 02 20:35:12 2024 +0100 @@ -1095,8 +1095,8 @@ SOME T' => T' | NONE => raise Fail "strip_shyps: bad type variable in proof term")); val map_ztyp = - #apply (ZTypes.unsynchronized_cache - (ZTerm.subst_type_same (ZTerm.ztyp_of o map_atyp o ZTerm.typ_of o ZTVar))); + ZTypes.apply_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 8e4ca2c87e86 -r 58073f3d748a src/Pure/zterm.ML --- a/src/Pure/zterm.ML Mon Dec 02 18:53:45 2024 +0100 +++ b/src/Pure/zterm.ML Mon Dec 02 20:35:12 2024 +0100 @@ -548,7 +548,7 @@ fun instantiate_type_same instT = if ZTVars.is_empty instT then Same.same - else #apply (ZTypes.unsynchronized_cache (subst_type_same (Same.function (ZTVars.lookup instT)))); + else ZTypes.apply_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)); @@ -863,9 +863,7 @@ let val lookup = if Vartab.is_empty tenv then K NONE - else - #apply (ZVars.unsynchronized_cache - (apsnd typ_of #> Envir.lookup envir #> Option.map zterm)); + else ZVars.apply_unsynchronized_cache (apsnd typ_of #> Envir.lookup envir #> Option.map zterm); val normT = norm_type_same ztyp tyenv; @@ -1008,8 +1006,8 @@ val typ_operation = #typ_operation ucontext {strip_sorts = true}; val unconstrain_typ = Same.commit typ_operation; val unconstrain_ztyp = - #apply (ZTypes.unsynchronized_cache - (Same.function_eq (op =) (typ_of #> unconstrain_typ #> ztyp_of))); + ZTypes.apply_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); @@ -1226,10 +1224,10 @@ val typ = if Names.is_empty tfrees then Same.same else - #apply (ZTypes.unsynchronized_cache + ZTypes.apply_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) @@ -1251,10 +1249,10 @@ let val tab = ZTVars.build (names |> fold (fn ((a, S), b) => ZTVars.add (((a, ~1), S), b))); val typ = - #apply (ZTypes.unsynchronized_cache (subst_type_same (fn v => + ZTypes.apply_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 = @@ -1263,7 +1261,7 @@ | SOME f => let val tvar = ztyp_of o Same.function f; - val typ = #apply (ZTypes.unsynchronized_cache (subst_type_same tvar)); + val typ = ZTypes.apply_unsynchronized_cache (subst_type_same tvar); in map_proof_types {hyps = false} typ prf end); @@ -1297,7 +1295,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 #apply (ZTypes.unsynchronized_cache (subst_type_same tvar)) end; + in ZTypes.apply_unsynchronized_cache (subst_type_same tvar) end; fun incr_indexes_proof inc prf = let @@ -1437,8 +1435,8 @@ val typ_cache = typ_cache thy; val typ = - #apply (ZTypes.unsynchronized_cache - (typ_of #> #typ_operation ucontext {strip_sorts = true} #> ztyp_of)); + ZTypes.apply_unsynchronized_cache + (typ_of #> #typ_operation ucontext {strip_sorts = true} #> ztyp_of); val typ_sort = #typ_operation ucontext {strip_sorts = false};