# HG changeset patch # User wenzelm # Date 1728763898 -7200 # Node ID b16e6cacf739934a3b9fa84716ca6409699c6b60 # Parent 503e5280ba726401ebfacaa6b6f460594c45ab45# Parent c681b1a7b78edd7b649305d21508f1fcab41b366 merged diff -r 503e5280ba72 -r b16e6cacf739 src/HOL/Analysis/Infinite_Set_Sum.thy --- a/src/HOL/Analysis/Infinite_Set_Sum.thy Sat Oct 12 12:45:29 2024 +0900 +++ b/src/HOL/Analysis/Infinite_Set_Sum.thy Sat Oct 12 22:11:38 2024 +0200 @@ -126,24 +126,10 @@ "_qinfsetsum" \ infsetsum translations "\\<^sub>ax|P. t" => "CONST infsetsum (\x. t) {x. P}" - print_translation \ -let - fun sum_tr' [Abs (x, Tx, t), Const (\<^const_syntax>\Collect\, _) $ Abs (y, Ty, P)] = - if x <> y then raise Match - else - let - val x' = Syntax_Trans.mark_bound_body (x, Tx); - val t' = subst_bound (x', t); - val P' = subst_bound (x', P); - in - Syntax.const \<^syntax_const>\_qinfsetsum\ $ Syntax_Trans.mark_bound_abs (x, Tx) $ P' $ t' - end - | sum_tr' _ = raise Match; -in [(\<^const_syntax>\infsetsum\, K sum_tr')] end + [(\<^const_syntax>\infsetsum\, K (Collect_binder_tr' \<^syntax_const>\_qinfsetsum\))] \ - lemma restrict_count_space_subset: "A \ B \ restrict_space (count_space B) A = count_space A" by (subst restrict_count_space) (simp_all add: Int_absorb2) diff -r 503e5280ba72 -r b16e6cacf739 src/HOL/Analysis/Infinite_Sum.thy --- a/src/HOL/Analysis/Infinite_Sum.thy Sat Oct 12 12:45:29 2024 +0900 +++ b/src/HOL/Analysis/Infinite_Sum.thy Sat Oct 12 22:11:38 2024 +0200 @@ -74,21 +74,8 @@ "_qinfsum" \ infsum translations "\\<^sub>\x|P. t" => "CONST infsum (\x. t) {x. P}" - print_translation \ -let - fun sum_tr' [Abs (x, Tx, t), Const (@{const_syntax Collect}, _) $ Abs (y, Ty, P)] = - if x <> y then raise Match - else - let - val x' = Syntax_Trans.mark_bound_body (x, Tx); - val t' = subst_bound (x', t); - val P' = subst_bound (x', P); - in - Syntax.const @{syntax_const "_qinfsum"} $ Syntax_Trans.mark_bound_abs (x, Tx) $ P' $ t' - end - | sum_tr' _ = raise Match; -in [(@{const_syntax infsum}, K sum_tr')] end + [(\<^const_syntax>\infsum\, K (Collect_binder_tr' \<^syntax_const>\_qinfsum\))] \ subsection \General properties\ diff -r 503e5280ba72 -r b16e6cacf739 src/HOL/Analysis/Sparse_In.thy --- a/src/HOL/Analysis/Sparse_In.thy Sat Oct 12 12:45:29 2024 +0900 +++ b/src/HOL/Analysis/Sparse_In.thy Sat Oct 12 22:11:38 2024 +0200 @@ -177,23 +177,8 @@ "_qeventually_cosparse" == eventually translations "\\<^sub>\x|P. t" => "CONST eventually (\x. t) (CONST cosparse {x. P})" - print_translation \ -let - fun ev_cosparse_tr' [Abs (x, Tx, t), - Const (\<^const_syntax>\cosparse\, _) $ (Const (\<^const_syntax>\Collect\, _) $ Abs (y, Ty, P))] = - if x <> y then raise Match - else - let - val x' = Syntax_Trans.mark_bound_body (x, Tx); - val t' = subst_bound (x', t); - val P' = subst_bound (x', P); - in - Syntax.const \<^syntax_const>\_qeventually_cosparse\ $ - Syntax_Trans.mark_bound_abs (x, Tx) $ P' $ t' - end - | ev_cosparse_tr' _ = raise Match; -in [(\<^const_syntax>\eventually\, K ev_cosparse_tr')] end + [(\<^const_syntax>\eventually\, K (Collect_binder_tr' \<^syntax_const>\_qeventually_cosparse\))] \ lemma eventually_cosparse: "eventually P (cosparse A) \ {x. \P x} sparse_in A" diff -r 503e5280ba72 -r b16e6cacf739 src/HOL/Groups_Big.thy --- a/src/HOL/Groups_Big.thy Sat Oct 12 12:45:29 2024 +0900 +++ b/src/HOL/Groups_Big.thy Sat Oct 12 22:11:38 2024 +0200 @@ -671,24 +671,10 @@ syntax_consts "_qsum" == sum - translations "\x|P. t" => "CONST sum (\x. t) {x. P}" - print_translation \ - let - fun sum_tr' [Abs (x, Tx, t), Const (\<^const_syntax>\Collect\, _) $ Abs (y, Ty, P)] = - if x <> y then raise Match - else - let - val x' = Syntax_Trans.mark_bound_body (x, Tx); - val t' = subst_bound (x', t); - val P' = subst_bound (x', P); - in - Syntax.const \<^syntax_const>\_qsum\ $ Syntax_Trans.mark_bound_abs (x, Tx) $ P' $ t' - end - | sum_tr' _ = raise Match; - in [(\<^const_syntax>\sum\, K sum_tr')] end + [(\<^const_syntax>\sum\, K (Collect_binder_tr' \<^syntax_const>\_qsum\))] \ @@ -1441,24 +1427,10 @@ syntax_consts "_qprod" == prod - translations "\x|P. t" => "CONST prod (\x. t) {x. P}" - print_translation \ - let - fun prod_tr' [Abs (x, Tx, t), Const (\<^const_syntax>\Collect\, _) $ Abs (y, Ty, P)] = - if x <> y then raise Match - else - let - val x' = Syntax_Trans.mark_bound_body (x, Tx); - val t' = subst_bound (x', t); - val P' = subst_bound (x', P); - in - Syntax.const \<^syntax_const>\_qprod\ $ Syntax_Trans.mark_bound_abs (x, Tx) $ P' $ t' - end - | prod_tr' _ = raise Match; - in [(\<^const_syntax>\prod\, K prod_tr')] end + [(\<^const_syntax>\prod\, K (Collect_binder_tr' \<^syntax_const>\_qprod\))] \ context comm_monoid_mult diff -r 503e5280ba72 -r b16e6cacf739 src/HOL/Set.thy --- a/src/HOL/Set.thy Sat Oct 12 12:45:29 2024 +0900 +++ b/src/HOL/Set.thy Sat Oct 12 22:11:38 2024 +0200 @@ -53,6 +53,18 @@ translations "{p:A. P}" \ "CONST Collect (\p. p \ A \ P)" +ML \ + fun Collect_binder_tr' c [Abs (x, T, t), Const (\<^const_syntax>\Collect\, _) $ Abs (y, _, P)] = + if x = y then + let + val x' = Syntax_Trans.mark_bound_body (x, T); + val t' = subst_bound (x', t); + val P' = subst_bound (x', P); + in Syntax.const c $ Syntax_Trans.mark_bound_abs (x, T) $ P' $ t' end + else raise Match + | Collect_binder_tr' _ _ = raise Match +\ + lemma CollectI: "P a \ a \ {x. P x}" by simp diff -r 503e5280ba72 -r b16e6cacf739 src/Pure/Pure.thy --- a/src/Pure/Pure.thy Sat Oct 12 12:45:29 2024 +0900 +++ b/src/Pure/Pure.thy Sat Oct 12 22:11:38 2024 +0200 @@ -1581,11 +1581,11 @@ bundle constrain_space_syntax \ \type constraints with spacing\ begin no_syntax (output) - "_constrain" :: "logic => type => logic" (\_::_\ [4, 0] 3) - "_constrain" :: "prop' => type => prop'" (\_::_\ [4, 0] 3) + "_constrain" :: "logic \ type \ logic" (\_::_\ [4, 0] 3) + "_constrain" :: "prop' \ type \ prop'" (\_::_\ [4, 0] 3) syntax (output) - "_constrain" :: "logic => type => logic" (\_ :: _\ [4, 0] 3) - "_constrain" :: "prop' => type => prop'" (\_ :: _\ [4, 0] 3) + "_constrain" :: "logic \ type \ logic" (\_ :: _\ [4, 0] 3) + "_constrain" :: "prop' \ type \ prop'" (\_ :: _\ [4, 0] 3) end diff -r 503e5280ba72 -r b16e6cacf739 src/Pure/Syntax/ast.ML --- a/src/Pure/Syntax/ast.ML Sat Oct 12 12:45:29 2024 +0900 +++ b/src/Pure/Syntax/ast.ML Sat Oct 12 22:11:38 2024 +0200 @@ -15,10 +15,11 @@ val ast_ord: ast ord structure Table: TABLE structure Set: SET + val pretty_var: string -> Pretty.T val pretty_ast: ast -> Pretty.T val pretty_rule: ast * ast -> Pretty.T val strip_positions: ast -> ast - val head_of_rule: ast * ast -> string + val rule_index: ast * ast -> string val rule_error: ast * ast -> string option val fold_ast: string -> ast list -> ast val fold_ast_p: string -> ast list * ast -> ast @@ -79,14 +80,15 @@ structure Set = Set(Table.Key); +(* print asts in a LISP-like style *) -(** print asts in a LISP-like style **) +fun pretty_var x = + (case Term_Position.decode x of + SOME pos => Term_Position.pretty pos + | NONE => Pretty.str x); fun pretty_ast (Constant a) = Pretty.quote (Pretty.str a) - | pretty_ast (Variable x) = - (case Term_Position.decode x of - SOME pos => Term_Position.pretty pos - | NONE => Pretty.str x) + | pretty_ast (Variable x) = pretty_var x | pretty_ast (Appl asts) = Pretty.enclose "(" ")" (Pretty.breaks (map pretty_ast asts)); fun pretty_rule (lhs, rhs) = @@ -105,17 +107,11 @@ | strip_positions ast = ast; -(* head_of_ast and head_of_rule *) - -fun head_of_ast (Constant a) = a - | head_of_ast (Appl (Constant a :: _)) = a - | head_of_ast _ = ""; +(* translation rules *) -fun head_of_rule (lhs, _) = head_of_ast lhs; - - - -(** check translation rules **) +fun rule_index (Constant a, _: ast) = a + | rule_index (Appl (Constant a :: _), _) = a + | rule_index _ = ""; fun rule_error (lhs, rhs) = let @@ -132,10 +128,7 @@ end; - -(** ast translation utilities **) - -(* fold asts *) +(* ast translation utilities *) fun fold_ast _ [] = raise Match | fold_ast _ [y] = y @@ -144,8 +137,6 @@ fun fold_ast_p c = uncurry (fold_rev (fn x => fn xs => Appl [Constant c, x, xs])); -(* unfold asts *) - fun unfold_ast c (y as Appl [Constant c', x, xs]) = if c = c' then x :: unfold_ast c xs else [y] | unfold_ast _ y = [y]; @@ -161,22 +152,23 @@ (* match *) +local + +exception NO_MATCH; + +fun match1 (Constant a) (Constant b) env = if a = b then env else raise NO_MATCH + | match1 (Variable a) (Constant b) env = if a = b then env else raise NO_MATCH + | match1 ast (Variable x) env = Symtab.update (x, ast) env + | match1 (Appl asts) (Appl pats) env = match2 asts pats env + | match1 _ _ _ = raise NO_MATCH +and match2 (ast :: asts) (pat :: pats) env = match1 ast pat env |> match2 asts pats + | match2 [] [] env = env + | match2 _ _ _ = raise NO_MATCH; + +in + fun match ast pat = let - exception NO_MATCH; - - fun mtch (Constant a) (Constant b) env = - if a = b then env else raise NO_MATCH - | mtch (Variable a) (Constant b) env = - if a = b then env else raise NO_MATCH - | mtch ast (Variable x) env = Symtab.update (x, ast) env - | mtch (Appl asts) (Appl pats) env = mtch_lst asts pats env - | mtch _ _ _ = raise NO_MATCH - and mtch_lst (ast :: asts) (pat :: pats) env = - mtch_lst asts pats (mtch ast pat env) - | mtch_lst [] [] env = env - | mtch_lst _ _ _ = raise NO_MATCH; - val (head, args) = (case (ast, pat) of (Appl asts, Appl pats) => @@ -185,9 +177,9 @@ else (ast, []) end | _ => (ast, [])); - in - SOME (Symtab.build (mtch head pat), args) handle NO_MATCH => NONE - end; + in SOME (Symtab.build (match1 head pat), args) handle NO_MATCH => NONE end; + +end; (* normalize *) @@ -195,9 +187,23 @@ val trace = Config.declare_bool ("syntax_ast_trace", \<^here>) (K false); val stats = Config.declare_bool ("syntax_ast_stats", \<^here>) (K false); +local + +fun subst _ (ast as Constant _) = ast + | subst env (Variable x) = the (Symtab.lookup env x) + | subst env (Appl asts) = Appl (map (subst env) asts); + +fun head_name (Constant a) = SOME a + | head_name (Variable a) = SOME a + | head_name (Appl (Constant a :: _)) = SOME a + | head_name (Appl (Variable a :: _)) = SOME a + | head_name _ = NONE; + fun message head body = Pretty.string_of (Pretty.block [Pretty.str head, Pretty.brk 1, body]); +in + (*the normalizer works yoyo-like: top-down, bottom-up, top-down, ...*) fun normalize ctxt get_rules pre_ast = let @@ -208,61 +214,53 @@ val failed_matches = Unsynchronized.ref 0; val changes = Unsynchronized.ref 0; - fun subst _ (ast as Constant _) = ast - | subst env (Variable x) = the (Symtab.lookup env x) - | subst env (Appl asts) = Appl (map (subst env) asts); - - fun try_rules ((lhs, rhs) :: pats) ast = + fun rewrite1 ((lhs, rhs) :: pats) ast = (case match ast lhs of SOME (env, args) => (Unsynchronized.inc changes; SOME (mk_appl (subst env rhs) args)) - | NONE => (Unsynchronized.inc failed_matches; try_rules pats ast)) - | try_rules [] _ = NONE; - val try_headless_rules = try_rules (get_rules ""); + | NONE => (Unsynchronized.inc failed_matches; rewrite1 pats ast)) + | rewrite1 [] _ = NONE; - fun try ast a = - (case try_rules (get_rules a) ast of - NONE => try_headless_rules ast - | some => some); + fun rewrite2 (SOME a) ast = + (case rewrite1 (get_rules a) ast of + NONE => rewrite2 NONE ast + | some => some) + | rewrite2 NONE ast = rewrite1 (get_rules "") ast; - fun rewrite (ast as Constant a) = try ast a - | rewrite (ast as Variable a) = try ast a - | rewrite (ast as Appl (Constant a :: _)) = try ast a - | rewrite (ast as Appl (Variable a :: _)) = try ast a - | rewrite ast = try_headless_rules ast; + fun rewrite ast = rewrite2 (head_name ast) ast; fun rewrote old_ast new_ast = if trace then tracing (message "rewrote:" (pretty_rule (old_ast, new_ast))) else (); - fun norm_root ast = + fun norm1 ast = (case rewrite ast of - SOME new_ast => (rewrote ast new_ast; norm_root new_ast) + SOME new_ast => (rewrote ast new_ast; norm1 new_ast) | NONE => ast); - fun norm ast = - (case norm_root ast of + fun norm2 ast = + (case norm1 ast of Appl sub_asts => let val old_changes = ! changes; - val new_ast = Appl (map norm sub_asts); + val new_ast = Appl (map norm2 sub_asts); in - if old_changes = ! changes then new_ast else norm_root new_ast + if old_changes = ! changes then new_ast else norm1 new_ast end | atomic_ast => atomic_ast); - fun normal ast = + fun norm ast = let val old_changes = ! changes; - val new_ast = norm ast; + val new_ast = norm2 ast; in Unsynchronized.inc passes; - if old_changes = ! changes then new_ast else normal new_ast + if old_changes = ! changes then new_ast else norm new_ast end; val _ = if trace then tracing (message "pre:" (pretty_ast pre_ast)) else (); - val post_ast = normal pre_ast; + val post_ast = norm pre_ast; val _ = if trace orelse stats then tracing (message "post:" (pretty_ast post_ast) ^ "\nnormalize: " ^ @@ -273,3 +271,5 @@ in post_ast end; end; + +end; diff -r 503e5280ba72 -r b16e6cacf739 src/Pure/Syntax/local_syntax.ML --- a/src/Pure/Syntax/local_syntax.ML Sat Oct 12 12:45:29 2024 +0900 +++ b/src/Pure/Syntax/local_syntax.ML Sat Oct 12 22:11:38 2024 +0200 @@ -27,8 +27,8 @@ (* datatype T *) type local_mixfix = - (string * bool) * (*name, fixed?*) - ((bool * bool * Syntax.mode) * (string * typ * mixfix)); (*type?, add?, mode, declaration*) + {name: string, is_fixed: bool} * + ({is_type: bool, add: bool, mode: Syntax.mode} * (string * typ * mixfix)); datatype T = Syntax of {thy_syntax: Syntax.syntax, @@ -54,9 +54,10 @@ let val thy = Proof_Context.theory_of ctxt; val thy_syntax = Sign.syntax_of thy; - fun update_gram ((true, add, m), decls) = Syntax.update_type_gram ctxt add m decls - | update_gram ((false, add, m), decls) = - Syntax.update_const_gram ctxt add (Sign.logical_types thy) m decls; + fun update_gram ({is_type = true, add, mode}, decls) = + Syntax.update_type_gram ctxt add mode decls + | update_gram ({is_type = false, add, mode}, decls) = + Syntax.update_const_gram ctxt add (Sign.logical_types thy) mode decls; val local_syntax = thy_syntax |> fold update_gram (AList.coalesce (op =) (rev (map snd mixfixes))); @@ -77,11 +78,14 @@ local -fun prep_mixfix _ _ (_, (_, _, Structure _)) = NONE - | prep_mixfix add mode (Type, decl as (x, _, _)) = SOME ((x, false), ((true, add, mode), decl)) - | prep_mixfix add mode (Const, decl as (x, _, _)) = SOME ((x, false), ((false, add, mode), decl)) +fun prep_mixfix _ _ (_, (_, _, Structure _)) = (NONE: local_mixfix option) + | prep_mixfix add mode (Type, decl as (x, _, _)) = + SOME ({name = x, is_fixed = false}, ({is_type = true, add = add, mode = mode}, decl)) + | prep_mixfix add mode (Const, decl as (x, _, _)) = + SOME ({name = x, is_fixed = false}, ({is_type = false, add = add, mode = mode}, decl)) | prep_mixfix add mode (Fixed, (x, T, mx)) = - SOME ((x, true), ((false, add, mode), (Lexicon.mark_fixed x, T, mx))); + SOME (({name = x, is_fixed = true}, + ({is_type = false, add = add, mode = mode}, (Lexicon.mark_fixed x, T, mx)))); fun prep_struct (Fixed, (c, _, Structure _)) = SOME c | prep_struct (_, (c, _, Structure _)) = error ("Bad structure mixfix declaration for " ^ quote c) @@ -103,7 +107,7 @@ {structs = if add then #structs idents @ new_structs else subtract (op =) new_structs (#structs idents), - fixes = fold (fn ((x, true), _) => cons x | _ => I) mixfixes' []}; + fixes = fold (fn ({name = x, is_fixed = true}, _) => cons x | _ => I) mixfixes' []}; val syntax' = build_syntax ctxt mode mixfixes'; in (if idents = idents' then NONE else SOME idents', syntax') end); diff -r 503e5280ba72 -r b16e6cacf739 src/Pure/Syntax/printer.ML --- a/src/Pure/Syntax/printer.ML Sat Oct 12 12:45:29 2024 +0900 +++ b/src/Pure/Syntax/printer.ML Sat Oct 12 22:11:38 2024 +0200 @@ -211,90 +211,93 @@ in -fun pretty ctxt tabs trf markup_trans markup_extern ast0 = +fun pretty ctxt tabs trf markup_trans (markup, extern) = let val type_mode = Config.get ctxt pretty_type_mode; val curried = Config.get ctxt pretty_curried; val show_brackets = Config.get ctxt show_brackets; - (*default applications: prefix / postfix*) - val appT = + val application = if type_mode then Syntax_Trans.tappl_ast_tr' else if curried then Syntax_Trans.applC_ast_tr' else Syntax_Trans.appl_ast_tr'; - fun synT _ ([], args) = ([], args) - | synT m (Arg p :: symbs, t :: args) = - let val (Ts, args') = synT m (symbs, args); - in (astT (t, p) @ Ts, args') end - | synT m (TypArg p :: symbs, t :: args) = - let - val (Ts, args') = synT m (symbs, args); - in - if type_mode then (astT (t, p) @ Ts, args') - else - let val ctxt' = ctxt - |> Config.put pretty_type_mode true - |> Config.put pretty_priority p - in (pretty ctxt' tabs trf markup_trans markup_extern t @ Ts, args') end - end - | synT m (String (literal_markup, s) :: symbs, args) = + fun split_args 0 [x] ys = (x, ys) + | split_args 0 rev_xs ys = (Ast.Appl (rev rev_xs), ys) + | split_args n rev_xs (y :: ys) = split_args (n - 1) (y :: rev_xs) ys; + + fun syntax _ ([], args) = ([], args) + | syntax m (Arg p :: symbs, arg :: args) = + let val (prts, args') = syntax m (symbs, args); + in (main p arg @ prts, args') end + | syntax m (TypArg p :: symbs, arg :: args) = + let val (prts, args') = syntax m (symbs, args); + in (main_type p arg @ prts, args') end + | syntax m (String (literal_markup, s) :: symbs, args) = let - val (Ts, args') = synT m (symbs, args); - val T = Pretty.marks_str (if null literal_markup then [] else m @ literal_markup, s); - in (T :: Ts, args') end - | synT m (Block (block, bsymbs) :: symbs, args) = + val (prts, args') = syntax m (symbs, args); + val prt = Pretty.marks_str (if null literal_markup then [] else m @ literal_markup, s); + in (prt :: prts, args') end + | syntax m (Block (block, bsymbs) :: symbs, args) = + let + val (body, args') = syntax m (bsymbs, args); + val (prts, args'') = syntax m (symbs, args'); + val prt = Syntax_Ext.pretty_block block body; + in (prt :: prts, args'') end + | syntax m (Break i :: symbs, args) = let - val {markup, open_block, consistent, unbreakable, indent} = block; - val (bTs, args') = synT m (bsymbs, args); - val (Ts, args'') = synT m (symbs, args'); - val prt_block = - {markup = markup, open_block = open_block, consistent = consistent, indent = indent}; - val T = Pretty.markup_blocks prt_block bTs |> unbreakable ? Pretty.unbreakable; - in (T :: Ts, args'') end - | synT m (Break i :: symbs, args) = - let - val (Ts, args') = synT m (symbs, args); - val T = if i < 0 then Pretty.fbrk else Pretty.brk i; - in (T :: Ts, args') end + val (prts, args') = syntax m (symbs, args); + val prt = if i < 0 then Pretty.fbrk else Pretty.brk i; + in (prt :: prts, args') end + + and parens p q a (symbs, args) = + let + val symbs' = + if p > q orelse (show_brackets andalso q <> 1000 andalso not (is_chain symbs)) + then [Block (par_block, par_bg :: symbs @ [par_en])] else symbs; + in #1 (syntax (markup a) (symbs', args)) end - and parT m (pr, args, p, p') = #1 (synT m - (if p > p' orelse (show_brackets andalso p' <> 1000 andalso not (is_chain pr)) - then [Block (par_block, par_bg :: pr @ [par_en])] else pr, args)) - - and atomT a = Pretty.marks_str (#1 markup_extern a, #2 markup_extern a) - - and prefixT (_, a, [], _) = [atomT a] - | prefixT (c, _, args, p) = astT (appT (c, args), p) - - and splitT 0 ([x], ys) = (x, ys) - | splitT 0 (rev_xs, ys) = (Ast.Appl (rev rev_xs), ys) - | splitT n (rev_xs, y :: ys) = splitT (n - 1) (y :: rev_xs, ys) - - and combT (tup as (c, a, args, p)) = - let - val nargs = length args; + and translation p a args = + (case markup_trans a args of + SOME prt => SOME [prt] + | NONE => Option.map (main p) (SOME (trf a ctxt args) handle Match => NONE)) - (*find matching table entry, or print as prefix / postfix*) - fun prnt ([], []) = prefixT tup - | prnt ([], tb :: tbs) = prnt (Symtab.lookup_list tb a, tbs) - | prnt ((pr, n, p') :: prnps, tbs) = - if nargs = n then parT (#1 markup_extern a) (pr, args, p, p') - else if nargs > n andalso not type_mode then - astT (appT (splitT n ([c], args)), p) - else prnt (prnps, tbs); - in - (case markup_trans a args of - SOME prt => [prt] - | NONE => astT (trf a ctxt args, p) handle Match => prnt ([], tabs)) - end + and combination p c a args = + (case translation p a args of + SOME res => res + | NONE => + (*find matching table entry, or print as prefix / postfix*) + let + val nargs = length args; + val entry = + tabs |> get_first (fn tab => + Symtab.lookup_list tab a |> find_first (fn (_, n, _) => + nargs = n orelse nargs > n andalso not type_mode)); + in + (case entry of + NONE => + if nargs = 0 then [Pretty.marks_str (markup a, extern a)] + else main p (application (c, args)) + | SOME (symbs, n, q) => + if nargs = n then parens p q a (symbs, args) + else main p (application (split_args n [c] args))) + end) - and astT (c as Ast.Constant a, p) = combT (c, a, [], p) - | astT (ast as Ast.Variable _, _) = [Ast.pretty_ast ast] - | astT (Ast.Appl ((c as Ast.Constant a) :: (args as _ :: _)), p) = combT (c, a, args, p) - | astT (Ast.Appl (f :: (args as _ :: _)), p) = astT (appT (f, args), p) - | astT (ast as Ast.Appl _, _) = raise Ast.AST ("pretty: malformed ast", [ast]); - in astT (ast0, Config.get ctxt pretty_priority) end; + and main _ (Ast.Variable x) = [Ast.pretty_var x] + | main p (c as Ast.Constant a) = combination p c a [] + | main p (Ast.Appl ((c as Ast.Constant a) :: (args as _ :: _))) = combination p c a args + | main p (Ast.Appl (f :: (args as _ :: _))) = main p (application (f, args)) + | main _ (ast as Ast.Appl _) = raise Ast.AST ("pretty: malformed ast", [ast]) + + and main_type p ast = + if type_mode then main p ast + else + (ctxt + |> Config.put pretty_type_mode true + |> Config.put pretty_priority p + |> pretty) tabs trf markup_trans (markup, extern) ast; + + in main (Config.get ctxt pretty_priority) end; end; diff -r 503e5280ba72 -r b16e6cacf739 src/Pure/Syntax/syntax.ML --- a/src/Pure/Syntax/syntax.ML Sat Oct 12 12:45:29 2024 +0900 +++ b/src/Pure/Syntax/syntax.ML Sat Oct 12 22:11:38 2024 +0200 @@ -405,8 +405,8 @@ fun dest_ruletab tab = Symtab.dest tab |> sort_by #1 |> maps #2; -val update_ruletab = fold_rev (fn r => Symtab.update_list (op =) (Ast.head_of_rule r, r)); -val remove_ruletab = fold (fn r => Symtab.remove_list (op =) (Ast.head_of_rule r, r)); +val update_ruletab = fold_rev (fn r => Symtab.update_list (op =) (Ast.rule_index r, r)); +val remove_ruletab = fold (fn r => Symtab.remove_list (op =) (Ast.rule_index r, r)); fun merge_ruletabs tab1 tab2 = Symtab.merge_list (op =) (tab1, tab2); diff -r 503e5280ba72 -r b16e6cacf739 src/Pure/Syntax/syntax_ext.ML --- a/src/Pure/Syntax/syntax_ext.ML Sat Oct 12 12:45:29 2024 +0900 +++ b/src/Pure/Syntax/syntax_ext.ML Sat Oct 12 22:11:38 2024 +0200 @@ -10,6 +10,7 @@ type block = {markup: Markup.T list, open_block: bool, consistent: bool, unbreakable: bool, indent: int} val block_indent: int -> block + val pretty_block: block -> Pretty.T list -> Pretty.T datatype xsymb = Delim of string | Argument of string * int | @@ -69,6 +70,11 @@ fun block_indent indent : block = {markup = [], open_block = false, consistent = false, unbreakable = false, indent = indent}; +fun pretty_block {markup, open_block, consistent, indent, unbreakable} body = + Pretty.markup_blocks + {markup = markup, open_block = open_block, consistent = consistent, indent = indent} body + |> unbreakable ? Pretty.unbreakable; + datatype xsymb = Delim of string | Argument of string * int |