--- 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" \<rightleftharpoons> infsetsum
translations
"\<Sum>\<^sub>ax|P. t" => "CONST infsetsum (\<lambda>x. t) {x. P}"
-
print_translation \<open>
-let
- fun sum_tr' [Abs (x, Tx, t), Const (\<^const_syntax>\<open>Collect\<close>, _) $ 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>\<open>_qinfsetsum\<close> $ Syntax_Trans.mark_bound_abs (x, Tx) $ P' $ t'
- end
- | sum_tr' _ = raise Match;
-in [(\<^const_syntax>\<open>infsetsum\<close>, K sum_tr')] end
+ [(\<^const_syntax>\<open>infsetsum\<close>, K (Collect_binder_tr' \<^syntax_const>\<open>_qinfsetsum\<close>))]
\<close>
-
lemma restrict_count_space_subset:
"A \<subseteq> B \<Longrightarrow> restrict_space (count_space B) A = count_space A"
by (subst restrict_count_space) (simp_all add: Int_absorb2)
--- 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" \<rightleftharpoons> infsum
translations
"\<Sum>\<^sub>\<infinity>x|P. t" => "CONST infsum (\<lambda>x. t) {x. P}"
-
print_translation \<open>
-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>\<open>infsum\<close>, K (Collect_binder_tr' \<^syntax_const>\<open>_qinfsum\<close>))]
\<close>
subsection \<open>General properties\<close>
--- 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
"\<forall>\<^sub>\<approx>x|P. t" => "CONST eventually (\<lambda>x. t) (CONST cosparse {x. P})"
-
print_translation \<open>
-let
- fun ev_cosparse_tr' [Abs (x, Tx, t),
- Const (\<^const_syntax>\<open>cosparse\<close>, _) $ (Const (\<^const_syntax>\<open>Collect\<close>, _) $ 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>\<open>_qeventually_cosparse\<close> $
- Syntax_Trans.mark_bound_abs (x, Tx) $ P' $ t'
- end
- | ev_cosparse_tr' _ = raise Match;
-in [(\<^const_syntax>\<open>eventually\<close>, K ev_cosparse_tr')] end
+ [(\<^const_syntax>\<open>eventually\<close>, K (Collect_binder_tr' \<^syntax_const>\<open>_qeventually_cosparse\<close>))]
\<close>
lemma eventually_cosparse: "eventually P (cosparse A) \<longleftrightarrow> {x. \<not>P x} sparse_in A"
--- 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
"\<Sum>x|P. t" => "CONST sum (\<lambda>x. t) {x. P}"
-
print_translation \<open>
- let
- fun sum_tr' [Abs (x, Tx, t), Const (\<^const_syntax>\<open>Collect\<close>, _) $ 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>\<open>_qsum\<close> $ Syntax_Trans.mark_bound_abs (x, Tx) $ P' $ t'
- end
- | sum_tr' _ = raise Match;
- in [(\<^const_syntax>\<open>sum\<close>, K sum_tr')] end
+ [(\<^const_syntax>\<open>sum\<close>, K (Collect_binder_tr' \<^syntax_const>\<open>_qsum\<close>))]
\<close>
@@ -1441,24 +1427,10 @@
syntax_consts
"_qprod" == prod
-
translations
"\<Prod>x|P. t" => "CONST prod (\<lambda>x. t) {x. P}"
-
print_translation \<open>
- let
- fun prod_tr' [Abs (x, Tx, t), Const (\<^const_syntax>\<open>Collect\<close>, _) $ 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>\<open>_qprod\<close> $ Syntax_Trans.mark_bound_abs (x, Tx) $ P' $ t'
- end
- | prod_tr' _ = raise Match;
- in [(\<^const_syntax>\<open>prod\<close>, K prod_tr')] end
+ [(\<^const_syntax>\<open>prod\<close>, K (Collect_binder_tr' \<^syntax_const>\<open>_qprod\<close>))]
\<close>
context comm_monoid_mult
--- 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}" \<rightharpoonup> "CONST Collect (\<lambda>p. p \<in> A \<and> P)"
+ML \<open>
+ fun Collect_binder_tr' c [Abs (x, T, t), Const (\<^const_syntax>\<open>Collect\<close>, _) $ 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
+\<close>
+
lemma CollectI: "P a \<Longrightarrow> a \<in> {x. P x}"
by simp
--- 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 \<comment> \<open>type constraints with spacing\<close>
begin
no_syntax (output)
- "_constrain" :: "logic => type => logic" (\<open>_::_\<close> [4, 0] 3)
- "_constrain" :: "prop' => type => prop'" (\<open>_::_\<close> [4, 0] 3)
+ "_constrain" :: "logic \<Rightarrow> type \<Rightarrow> logic" (\<open>_::_\<close> [4, 0] 3)
+ "_constrain" :: "prop' \<Rightarrow> type \<Rightarrow> prop'" (\<open>_::_\<close> [4, 0] 3)
syntax (output)
- "_constrain" :: "logic => type => logic" (\<open>_ :: _\<close> [4, 0] 3)
- "_constrain" :: "prop' => type => prop'" (\<open>_ :: _\<close> [4, 0] 3)
+ "_constrain" :: "logic \<Rightarrow> type \<Rightarrow> logic" (\<open>_ :: _\<close> [4, 0] 3)
+ "_constrain" :: "prop' \<Rightarrow> type \<Rightarrow> prop'" (\<open>_ :: _\<close> [4, 0] 3)
end
--- 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;
--- 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);
--- 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;
--- 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);
--- 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 |