# HG changeset patch # User wenzelm # Date 1681939675 -7200 # Node ID 3c837f8c8ed5b25991bcde4f079fa1c8fd29b170 # Parent dae8b7a9a89a2c4d02d53299169e6a2e5a80ff38 tuned; diff -r dae8b7a9a89a -r 3c837f8c8ed5 src/HOL/Tools/sat.ML --- a/src/HOL/Tools/sat.ML Wed Apr 19 23:27:33 2023 +0200 +++ b/src/HOL/Tools/sat.ML Wed Apr 19 23:27:55 2023 +0200 @@ -216,7 +216,7 @@ handle TERM _ => NONE; (* 'chyp' is not a literal *) fun prove_clause id = - (case Array.sub (clauses, id) of + (case Array.nth clauses id of RAW_CLAUSE clause => clause | ORIG_CLAUSE thm => (* convert the original clause *) diff -r dae8b7a9a89a -r 3c837f8c8ed5 src/HOL/Tools/sat_solver.ML --- a/src/HOL/Tools/sat_solver.ML Wed Apr 19 23:27:33 2023 +0200 +++ b/src/HOL/Tools/sat_solver.ML Wed Apr 19 23:27:55 2023 +0200 @@ -682,7 +682,7 @@ original_clause_id_from 0 (* both 'lits' and the list of literals used in 'clauses' are sorted, so *) (* testing for equality should suffice -- barring duplicate literals *) - else if Array.sub (clauses, index) = lits then ( + else if Array.nth clauses index = lits then ( (* success *) last_ref_clause := index; SOME index diff -r dae8b7a9a89a -r 3c837f8c8ed5 src/Pure/General/sha1.ML --- a/src/Pure/General/sha1.ML Wed Apr 19 23:27:33 2023 +0200 +++ b/src/Pure/General/sha1.ML Wed Apr 19 23:27:55 2023 +0200 @@ -101,12 +101,12 @@ (*hash result -- 5 words*) val hash_array : Word32.word Array.array = Array.fromList [0wx67452301, 0wxEFCDAB89, 0wx98BADCFE, 0wx10325476, 0wxC3D2E1F0]; - fun hash i = Array.sub (hash_array, i); + val hash = Array.nth hash_array; fun add_hash x i = Array.update (hash_array, i, hash i + x); (*current chunk -- 80 words*) val chunk_array = Array.array (80, 0w0: Word32.word); - fun chunk i = Array.sub (chunk_array, i); + val chunk = Array.nth chunk_array; fun init_chunk pos = Array.modifyi (fn (i, _) => if i < 16 then text (pos + i) diff -r dae8b7a9a89a -r 3c837f8c8ed5 src/Pure/Syntax/parser.ML --- a/src/Pure/Syntax/parser.ML Wed Apr 19 23:27:33 2023 +0200 +++ b/src/Pure/Syntax/parser.ML Wed Apr 19 23:27:55 2023 +0200 @@ -132,12 +132,12 @@ if not new_chain then ([], lambdas) else let (*lookahead of chain's source*) - val ((_, from_tks), _) = Array.sub (prods, the chain); + val ((_, from_tks), _) = Array.nth prods (the chain); (*copy from's lookahead to chain's destinations*) fun copy_lookahead to = let - val ((to_nts, to_tks), ps) = Array.sub (prods, to); + val ((to_nts, to_tks), ps) = Array.nth prods to; val new_tks = Tokens.subtract to_tks from_tks; (*added lookahead tokens*) val to_tks' = Tokens.merge (to_tks, new_tks); @@ -170,7 +170,7 @@ else (NONE, nts_insert nt nts); (*get all known starting tokens for a nonterminal*) - fun starts_for_nt nt = snd (fst (Array.sub (prods, nt))); + fun starts_for_nt nt = snd (fst (Array.nth prods nt)); (*update prods, lookaheads, and lambdas according to new lambda NTs*) val (added_starts', lambdas') = @@ -180,7 +180,7 @@ | propagate_lambda (l :: ls) added_starts lambdas = let (*get lookahead for lambda NT*) - val ((dependent, l_starts), _) = Array.sub (prods, l); + val ((dependent, l_starts), _) = Array.nth prods l; (*check productions whose lookahead may depend on lambda NT*) fun examine_prods [] add_lambda nt_dependencies added_tks nt_prods = @@ -221,7 +221,7 @@ (*check each NT whose lookahead depends on new lambda NT*) fun process_nts nt (added_lambdas, added_starts) = let - val ((old_nts, old_tks), nt_prods) = Array.sub (prods, nt); + val ((old_nts, old_tks), nt_prods) = Array.nth prods nt; (*existing productions whose lookahead may depend on l*) val tk_prods = prods_lookup nt_prods (get_start l_starts); @@ -279,7 +279,7 @@ (*add lhs NT to list of dependent NTs in lookahead*) fun add_nts nt initial = (if initial then - let val ((old_nts, old_tks), ps) = Array.sub (prods, nt) in + 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)) end @@ -290,7 +290,7 @@ fun add_tks [] added = added | add_tks (nt :: nts) added = let - val ((old_nts, old_tks), nt_prods) = Array.sub (prods, nt); + val ((old_nts, old_tks), nt_prods) = Array.nth prods nt; val new_tks = Tokens.subtract old_tks start_tks; @@ -365,7 +365,7 @@ (*copy existing productions for new starting tokens*) fun process_nts nt = let - val ((nts, tks), nt_prods) = Array.sub (prods, nt); + val ((nts, tks), nt_prods) = Array.nth prods nt; val tk_prods = prods_lookup nt_prods key; @@ -382,7 +382,7 @@ val _ = Array.update (prods, nt, ((nts, tks'), nt_prods'')); in tokens_add (nt, added_tks) end; - val ((dependent, _), _) = Array.sub (prods, changed_nt); + val ((dependent, _), _) = Array.nth prods changed_nt; in add_starts (starts @ nts_fold process_nts dependent []) end; in add_starts added_starts' end; in (chains', lambdas') end; @@ -574,7 +574,7 @@ filter (fn (_, _, _, Nonterminal (B, prec) :: _, _, _) => A = B andalso prec <= max_prec | _ => false) - (Array.sub (Estate, j)); + (Array.nth Estate j); fun movedot_term c (A, j, ts, Terminal a :: sa, id, i) = @@ -652,7 +652,7 @@ fun produce gram stateset i indata prev_token = - (case Array.sub (stateset, i) of + (case Array.nth stateset i of [] => let val toks = if Lexicon.is_eof prev_token then indata else prev_token :: indata;