# HG changeset patch # User wenzelm # Date 1682024644 -7200 # Node ID a9626bcb0c3b1e2ee6f095c9fcac706eb9acf980 # Parent 655bd3b0671bd1198b5e98558c1bb146d4f6a57e tuned signature; diff -r 655bd3b0671b -r a9626bcb0c3b src/HOL/Library/refute.ML --- a/src/HOL/Library/refute.ML Thu Apr 20 21:26:35 2023 +0200 +++ b/src/HOL/Library/refute.ML Thu Apr 20 23:04:04 2023 +0200 @@ -2375,7 +2375,7 @@ val result = fold (fn arg_i => fn i => interpretation_apply (i, arg_i)) arg_intrs intr (* update 'REC_OPERATORS' *) - val _ = Array.update (arr, elem, (true, result)) + val _ = Array.upd arr elem (true, result) in result end diff -r 655bd3b0671b -r a9626bcb0c3b src/HOL/Tools/sat.ML --- a/src/HOL/Tools/sat.ML Thu Apr 20 21:26:35 2023 +0200 +++ b/src/HOL/Tools/sat.ML Thu Apr 20 23:04:04 2023 +0200 @@ -226,7 +226,7 @@ val hyps = sort (lit_ord o apply2 fst) (map_filter (fn chyp => Option.map (rpair chyp) (index_of_literal chyp)) (Thm.chyps_of raw)) val clause = (raw, hyps) - val _ = Array.update (clauses, id, RAW_CLAUSE clause) + val _ = Array.upd clauses id (RAW_CLAUSE clause) in clause end @@ -236,7 +236,7 @@ val _ = cond_tracing ctxt (fn () => "Proving clause #" ^ string_of_int id ^ " ...") val ids = the (Inttab.lookup clause_table id) val clause = resolve_raw_clauses ctxt (map prove_clause ids) - val _ = Array.update (clauses, id, RAW_CLAUSE clause) + val _ = Array.upd clauses id (RAW_CLAUSE clause) val _ = cond_tracing ctxt (fn () => "Replay chain successful; clause stored at #" ^ string_of_int id) @@ -358,7 +358,7 @@ val max_idx = fst (the (Inttab.max clause_table)) val clause_arr = Array.array (max_idx + 1, NO_CLAUSE) val _ = - fold (fn thm => fn i => (Array.update (clause_arr, i, ORIG_CLAUSE thm); i + 1)) + fold (fn thm => fn i => (Array.upd clause_arr i (ORIG_CLAUSE thm); i + 1)) cnf_clauses 0 (* replay the proof to derive the empty clause *) (* [c_1 && ... && c_n] |- False *) diff -r 655bd3b0671b -r a9626bcb0c3b src/HOL/Tools/sat_solver.ML --- a/src/HOL/Tools/sat_solver.ML Thu Apr 20 21:26:35 2023 +0200 +++ b/src/HOL/Tools/sat_solver.ML Thu Apr 20 23:04:04 2023 +0200 @@ -667,7 +667,7 @@ fun init_array (Prop_Logic.And (fm1, fm2), n) = init_array (fm2, init_array (fm1, n)) | init_array (fm, n) = - (Array.update (clauses, n, clause_to_lit_list fm); n+1) + (Array.upd clauses n (clause_to_lit_list fm); n+1) val _ = init_array (cnf, 0) (* optimization for the common case where MiniSat "R"s clauses in their *) (* original order: *) diff -r 655bd3b0671b -r a9626bcb0c3b src/Pure/General/array.ML --- a/src/Pure/General/array.ML Thu Apr 20 21:26:35 2023 +0200 +++ b/src/Pure/General/array.ML Thu Apr 20 23:04:04 2023 +0200 @@ -8,6 +8,7 @@ sig include ARRAY val nth: 'a array -> int -> 'a + val upd: 'a array -> int -> 'a -> unit val forall: ('a -> bool) -> 'a array -> bool val member: ('a * 'a -> bool) -> 'a array -> 'a -> bool val fold: ('a -> 'b -> 'b) -> 'a array -> 'b -> 'b @@ -20,6 +21,7 @@ open Array; fun nth arr i = sub (arr, i); +fun upd arr i x = update (arr, i, x); val forall = all; diff -r 655bd3b0671b -r a9626bcb0c3b src/Pure/General/sha1.ML --- a/src/Pure/General/sha1.ML Thu Apr 20 21:26:35 2023 +0200 +++ b/src/Pure/General/sha1.ML Thu Apr 20 23:04:04 2023 +0200 @@ -102,7 +102,7 @@ val hash_array : Word32.word Array.array = Array.fromList [0wx67452301, 0wxEFCDAB89, 0wx98BADCFE, 0wx10325476, 0wxC3D2E1F0]; val hash = Array.nth hash_array; - fun add_hash x i = Array.update (hash_array, i, hash i + x); + fun add_hash x i = Array.upd hash_array i (hash i + x); (*current chunk -- 80 words*) val chunk_array = Array.array (80, 0w0: Word32.word); diff -r 655bd3b0671b -r a9626bcb0c3b src/Pure/Syntax/parser.ML --- a/src/Pure/Syntax/parser.ML Thu Apr 20 21:26:35 2023 +0200 +++ b/src/Pure/Syntax/parser.ML Thu Apr 20 23:04:04 2023 +0200 @@ -141,7 +141,7 @@ val new_tks = Tokens.subtract to_tks from_tks; (*added lookahead tokens*) val to_tks' = Tokens.merge (to_tks, new_tks); - val _ = Array.update (prods, to, ((to_nts, to_tks'), ps)); + val _ = Array.upd prods to ((to_nts, to_tks'), ps); in tokens_add (to, new_tks) end; val tos = chains_all_succs chains' [lhs]; @@ -235,7 +235,7 @@ val new_tks = Tokens.merge (old_tks, added_tks); val added_lambdas' = added_lambdas |> add_lambda ? cons nt; - val _ = Array.update (prods, nt, ((new_nts, new_tks), nt_prods')); + val _ = Array.upd prods nt ((new_nts, new_tks), nt_prods'); (*N.B. that because the tks component is used to access existing productions we have to add new @@ -281,7 +281,7 @@ (if initial then let val ((old_nts, old_tks), ps) = Array.nth prods nt in if nts_member old_nts lhs then () - else Array.update (prods, nt, ((nts_insert lhs old_nts, old_tks), ps)) + else Array.upd prods nt ((nts_insert lhs old_nts, old_tks), ps) end else (); false); @@ -306,9 +306,7 @@ |> nt = lhs ? Tokens.fold store start_tks'; val _ = if not changed andalso Tokens.is_empty new_tks then () - else - Array.update - (prods, nt, ((old_nts, Tokens.merge (old_tks, new_tks)), nt_prods')); + else Array.upd prods nt ((old_nts, Tokens.merge (old_tks, new_tks)), nt_prods'); in add_tks nts (tokens_add (nt, new_tks) added) end; val _ = nts_fold add_nts start_nts true; in add_tks (chains_all_succs chains' [lhs]) [] end; @@ -379,7 +377,7 @@ val added_tks = Tokens.subtract tks new_tks; val tks' = Tokens.merge (tks, added_tks); - val _ = Array.update (prods, nt, ((nts, tks'), nt_prods'')); + val _ = Array.upd prods nt ((nts, tks'), nt_prods''); in tokens_add (nt, added_tks) end; val ((dependent, _), _) = Array.nth prods changed_nt; @@ -677,8 +675,8 @@ | c :: cs => let val (si, sii) = PROCESSS gram stateset i c s; - val _ = Array.update (stateset, i, si); - val _ = Array.update (stateset, i + 1, sii); + val _ = Array.upd stateset i si; + val _ = Array.upd stateset (i + 1) sii; in produce gram stateset (i + 1) cs c end)); @@ -693,7 +691,7 @@ val S0 = [(~1, 0, [], [Nonterminal (start_tag, 0), Terminal Lexicon.eof], "", 0)]; val s = length indata + 1; val Estate = Array.array (s, []); - val _ = Array.update (Estate, 0, S0); + val _ = Array.upd Estate 0 S0; in get_trees (produce gram Estate 0 indata Lexicon.eof) end;