diff -r 7c01a86def85 -r 6002cb6bfb0a src/Pure/Syntax/syntax_phases.ML --- a/src/Pure/Syntax/syntax_phases.ML Tue Oct 15 23:44:42 2024 +0200 +++ b/src/Pure/Syntax/syntax_phases.ML Wed Oct 16 16:20:35 2024 +0200 @@ -66,14 +66,16 @@ fun markup_bound def ps (name, id) = Markup.bound :: map (fn pos => Position.make_entity_markup def id Markup.boundN (name, pos)) ps; -fun markup_entity ctxt 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 []}); +fun markup_entity_cache ctxt = + Symtab.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; @@ -161,13 +163,15 @@ if Lexicon.is_literal tok andalso null (Lexicon.literal_markup (Lexicon.str_of_token tok)) then Position.none else Lexicon.pos_of_token tok; + val markup_cache = markup_entity_cache ctxt; + fun report_literals a ts = List.app (report_literal a) ts and report_literal a t = (case t of Parser.Markup (_, ts) => report_literals a ts | Parser.Node _ => () | Parser.Tip tok => - if Lexicon.is_literal tok then report (report_pos tok) (markup_entity ctxt) a else ()); + if Lexicon.is_literal tok then report (report_pos tok) markup_cache a else ()); fun trans a args = (case trf a of @@ -273,56 +277,63 @@ in -fun decode_term _ (result as (_: Position.report_text list, Exn.Exn _)) = result - | decode_term ctxt (reports0, Exn.Res tm) = - let - val reports = Unsynchronized.ref reports0; - fun report ps = Position.store_reports reports ps; - val append_reports = Position.append_reports reports; +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)); + + fun decode (result as (_: Position.report_text list, Exn.Exn _)) = result + | decode (reports0, Exn.Res tm) = + let + val reports = Unsynchronized.ref reports0; + fun report ps = Position.store_reports reports ps; + val append_reports = Position.append_reports reports; - fun decode ps qs bs (Const ("_constrain", _) $ t $ typ) = - (case Term_Position.decode_position typ of - SOME (p, T) => Type.constraint T (decode (p :: ps) qs bs t) - | NONE => Type.constraint (decode_typ typ) (decode ps qs bs t)) - | decode ps qs bs (Const ("_constrainAbs", _) $ t $ typ) = - (case Term_Position.decode_position typ of - SOME (q, T) => Type.constraint (T --> dummyT) (decode ps (q :: qs) bs t) - | NONE => Type.constraint (decode_typ typ --> dummyT) (decode ps qs bs t)) - | decode _ qs bs (Abs (x, T, t)) = - let - val id = serial (); - val _ = report qs (markup_bound {def = true} qs) (x, id); - in Abs (x, T, decode [] [] ((qs, (x, id)) :: bs) t) end - | decode _ _ bs (t $ u) = decode [] [] bs t $ decode [] [] bs u - | decode ps _ _ (Const (a, T)) = - (case try Lexicon.unmark_fixed a of - SOME x => (report ps (markup_free ctxt) x; Free (x, T)) - | NONE => + fun decode ps qs bs (Const ("_constrain", _) $ t $ typ) = + (case Term_Position.decode_position typ of + SOME (p, T) => Type.constraint T (decode (p :: ps) qs bs t) + | NONE => Type.constraint (decode_typ typ) (decode ps qs bs t)) + | decode ps qs bs (Const ("_constrainAbs", _) $ t $ typ) = + (case Term_Position.decode_position typ of + SOME (q, T) => Type.constraint (T --> dummyT) (decode ps (q :: qs) bs t) + | NONE => Type.constraint (decode_typ typ --> dummyT) (decode ps qs bs t)) + | decode _ qs bs (Abs (x, T, t)) = let - val c = - (case try Lexicon.unmark_const a of - SOME c => c - | NONE => #1 (decode_const ctxt (a, []))); - val _ = report ps (markup_const ctxt) c; - in Const (c, T) end) - | decode ps _ _ (Free (a, T)) = - ((Name.reject_internal (a, ps) handle ERROR msg => - error (msg ^ Proof_Context.consts_completion_message ctxt (a, ps))); - (case get_free ctxt a of - SOME x => (report ps (markup_free ctxt) x; Free (x, T)) - | NONE => - let - val (c, rs) = decode_const ctxt (a, ps); - val _ = append_reports rs; - in Const (c, T) end)) - | decode ps _ _ (Var (xi, T)) = (report ps markup_var xi; Var (xi, T)) - | decode ps _ bs (t as Bound i) = - (case try (nth bs) i of - SOME (qs, (x, id)) => (report ps (markup_bound {def = false} qs) (x, id); t) - | NONE => t); + val id = serial (); + val _ = report qs (markup_bound {def = true} qs) (x, id); + in Abs (x, T, decode [] [] ((qs, (x, id)) :: bs) t) end + | decode _ _ bs (t $ u) = decode [] [] bs t $ decode [] [] bs u + | decode ps _ _ (Const (a, T)) = + (case try Lexicon.unmark_fixed a of + SOME x => (report ps markup_free_cache x; Free (x, T)) + | NONE => + let + val c = + (case try Lexicon.unmark_const a of + SOME c => c + | NONE => #1 (decode_const ctxt (a, []))); + val _ = report ps markup_const_cache c; + in Const (c, T) end) + | decode ps _ _ (Free (a, T)) = + ((Name.reject_internal (a, ps) handle ERROR msg => + error (msg ^ Proof_Context.consts_completion_message ctxt (a, ps))); + (case get_free ctxt a of + SOME x => (report ps markup_free_cache x; Free (x, T)) + | NONE => + let + val (c, rs) = decode_const ctxt (a, ps); + val _ = append_reports rs; + in Const (c, T) end)) + | decode ps _ _ (Var (xi, T)) = (report ps markup_var xi; Var (xi, T)) + | decode ps _ bs (t as Bound i) = + (case try (nth bs) i of + SOME (qs, (x, id)) => (report ps (markup_bound {def = false} qs) (x, id); t) + | NONE => t); - val tm' = Exn.result (fn () => decode [] [] [] tm) (); - in (! reports, tm') end; + val tm' = Exn.result (fn () => decode [] [] [] tm) (); + in (! reports, tm') end; + + in decode end; end; @@ -473,7 +484,9 @@ val reports = Unsynchronized.ref ([]: Position.report_text list); fun report ps = Position.store_reports reports ps; - fun decode_const ps c = (report ps (markup_entity ctxt) c; Ast.Constant c); + val markup_cache = markup_entity_cache ctxt; + + fun decode_const ps c = (report ps markup_cache c; Ast.Constant c); fun decode_var ps x = (report ps (fn () => [Markup.name x Markup.free]) (); Ast.Variable x); fun decode_appl ps asts = Ast.Appl (map (decode ps) asts) and decode ps (Ast.Constant c) = decode_const ps c @@ -719,30 +732,32 @@ fun extern_fixed ctxt x = if Name.is_skolem x then Variable.revert_fixed ctxt x else x; -fun extern ctxt c = - (case Syntax.get_consts (Proof_Context.syntax_of ctxt) c of - [b] => b - | bs => - (case filter Lexicon.is_marked bs of - [] => c - | [b] => b - | _ => error ("Multiple logical entities for " ^ quote c ^ ": " ^ commas_quote bs))) - |> Lexicon.unmark - {case_class = Proof_Context.extern_class ctxt, - case_type = Proof_Context.extern_type ctxt, - case_const = Proof_Context.extern_const ctxt, - case_fixed = extern_fixed ctxt, - case_default = I}; +fun extern_cache ctxt = + Symtab.unsynchronized_cache (fn c => + (case Syntax.get_consts (Proof_Context.syntax_of ctxt) c of + [b] => b + | bs => + (case filter Lexicon.is_marked bs of + [] => c + | [b] => b + | _ => error ("Multiple logical entities for " ^ quote c ^ ": " ^ commas_quote bs))) + |> Lexicon.unmark + {case_class = Proof_Context.extern_class ctxt, + case_type = Proof_Context.extern_type ctxt, + case_const = Proof_Context.extern_const ctxt, + case_fixed = extern_fixed ctxt, + case_default = I}) + |> #apply; -fun free_or_skolem ctxt x = (markup_free ctxt x, extern_fixed ctxt x); - -fun var_or_skolem 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)); +val var_or_skolem_cache = + Symtab.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; val typing_elem = YXML.output_markup_elem Markup.typing; val sorting_elem = YXML.output_markup_elem Markup.sorting; @@ -756,17 +771,20 @@ val syn = Proof_Context.syntax_of ctxt; val prtabs = Syntax.prtabs syn; val trf = Syntax.print_ast_translation syn; - val markup_extern = (markup_entity ctxt, extern ctxt); + val markup_extern = (markup_entity_cache ctxt, extern_cache ctxt); + + val free_or_skolem_cache = + #apply (Symtab.unsynchronized_cache (fn x => (markup_free ctxt x, 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); fun token_trans "_tfree" x = SOME (Pretty.mark_str (Markup.tfree, x)) | token_trans "_tvar" x = SOME (Pretty.mark_str (Markup.tvar, x)) - | token_trans "_free" x = SOME (Pretty.marks_str (free_or_skolem ctxt x)) + | token_trans "_free" x = SOME (Pretty.marks_str (free_or_skolem_cache x)) | token_trans "_bound" x = SOME (Pretty.mark_str (Markup.bound, x)) | token_trans "_loose" x = SOME (Pretty.mark_str (Markup.bad (), x)) - | token_trans "_var" x = SOME (Pretty.mark_str (var_or_skolem x)) + | token_trans "_var" x = SOME (Pretty.mark_str (var_or_skolem_cache x)) | token_trans "_numeral" x = SOME (Pretty.mark_str (Markup.numeral, x)) | token_trans "_inner_string" x = SOME (Pretty.mark_str (Markup.inner_string, x)) | token_trans _ _ = NONE;