# HG changeset patch # User wenzelm # Date 1729277281 -7200 # Node ID 0e27325da568746f1666fa01702aee907ef06332 # Parent 878f94921bec161e9a0b38b9aa6fe60c69842de5 print type constraints for consts with mixfix syntax; diff -r 878f94921bec -r 0e27325da568 NEWS --- a/NEWS Fri Oct 18 19:00:51 2024 +0200 +++ b/NEWS Fri Oct 18 20:48:01 2024 +0200 @@ -46,14 +46,16 @@ hyperlinks work properly e.g. for "['a, 'b] \ 'c" or "\A; B\ \ C" in Pure, and "\x\A. B x" or "\x\A. B x" in HOL. -* Inner syntax printing now supports type constraints for constants: -this is guarded by the configuration options "show_consts_markup" -(default true) and "show_markup" (default true for PIDE interaction). -Ast translation rules (command 'translations') and mixfix notation work -with or without such extra constraints, but ML translation functions -(command 'print_ast_translation') need may need to be changed slightly. -Rare INCOMPATIBILITY. The Prover IDE displays type constraints for -constants as for variables, e.g. via C-mouse hovering. +* Inner syntax printing now supports type constraints for constants, +optionally with mixfix syntax (infix, binder etc.). This is guarded by +the configuration options "show_consts_markup" (default true) and +"show_markup" (default true for PIDE interaction). The Prover IDE +displays type constraints as usual via C-mouse hovering. Ast translation +rules (command 'translations') already work with extra type constraints, +but the result omits the type of a matched constant. ML translation +functions (command 'print_ast_translation') based on Ast.unfold_ast etc. +work in the same manner, but more complex translations may require +manual changes: rare INCOMPATIBILITY. * The Simplifier now supports special "congprocs", using keyword 'congproc' or 'weak_congproc' in the 'simproc_setup' command (or ML diff -r 878f94921bec -r 0e27325da568 src/Pure/Syntax/printer.ML --- a/src/Pure/Syntax/printer.ML Fri Oct 18 19:00:51 2024 +0200 +++ b/src/Pure/Syntax/printer.ML Fri Oct 18 20:48:01 2024 +0200 @@ -36,6 +36,7 @@ val merge_prtabs: prtabs * prtabs -> prtabs val pretty: {type_mode: bool, curried: bool} -> Proof.context -> prtab list -> (string -> Proof.context -> Ast.ast list -> Ast.ast) -> + (Ast.ast -> Pretty.T -> Pretty.T) -> (string -> Ast.ast list -> Pretty.T option) -> ((string -> Markup.T list) * (string -> string)) -> Ast.ast -> Pretty.T list @@ -222,7 +223,7 @@ val type_mode_flags = {type_mode = true, curried = false}; -fun pretty {type_mode, curried} ctxt prtabs trf markup_trans (markup, extern) = +fun pretty {type_mode, curried} ctxt prtabs trf constrain_output markup_trans (markup, extern) = let val show_brackets = Config.get ctxt show_brackets; @@ -253,7 +254,7 @@ if type_mode then main p ast else pretty type_mode_flags (Config.put pretty_priority p ctxt) - prtabs trf markup_trans (markup, extern) ast + prtabs trf constrain_output markup_trans (markup, extern) ast and combination p c a args constraint = (case translation p a args of @@ -261,6 +262,7 @@ | NONE => (*find matching table entry, or print as prefix / postfix*) let + val cc = the_default c constraint; val nargs = length args; val entry = prtabs |> get_first (fn prtab => @@ -273,10 +275,10 @@ (case Option.mapPartial constrain_trans constraint of SOME prt => [prt] | NONE => [Pretty.marks_str (markup a, extern a)]) - else main p (application (the_default c constraint, args)) + else main p (application (cc, args)) | SOME (symbs, n, q) => - if nargs = n then parens p q a (symbs, args) - else main p (application (split_args n [c] args))) + if nargs = n then parens p q a (symbs, args) constraint + else main p (application (split_args n [cc] args))) end) and translation p a args = @@ -284,12 +286,16 @@ SOME prt => SOME [prt] | NONE => Option.map (main p) (SOME (trf a ctxt args) handle Match => NONE)) - and parens p q a (symbs, args) = + and parens p q a (symbs, args) constraint = 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 + val output = + (case constraint of + SOME (Ast.Appl [Ast.Constant "_constrain", _, ty]) => constrain_output ty + | _ => I); + in #1 (syntax (markup a, output) (symbs', args)) end and syntax _ ([], args) = ([], args) | syntax m (Arg p :: symbs, arg :: args) = @@ -298,11 +304,13 @@ | syntax m (Arg_Type 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) = + | syntax (m as (ms, output)) (String (literal_markup, s) :: symbs, args) = let val (prts, args') = syntax m (symbs, args); - val m' = if null literal_markup then [] else m @ literal_markup - in (Pretty.marks_str (m', s) :: prts, args') end + val prt = + if null literal_markup then Pretty.str s + else output (Pretty.marks_str (ms @ literal_markup, s)); + in (prt :: prts, args') end | syntax m (Block (block, bsymbs) :: symbs, args) = let val (body, args') = syntax m (bsymbs, args); diff -r 878f94921bec -r 0e27325da568 src/Pure/Syntax/syntax_phases.ML --- a/src/Pure/Syntax/syntax_phases.ML Fri Oct 18 19:00:51 2024 +0200 +++ b/src/Pure/Syntax/syntax_phases.ML Fri Oct 18 20:48:01 2024 +0200 @@ -806,29 +806,33 @@ then SOME (markup_ast false ty s) else NONE and pretty_typ_ast m ast = ast - |> pretty_type_mode ctxt prtabs trf markup_trans markup_extern + |> pretty_type_mode ctxt prtabs trf constrain_output markup_trans markup_extern |> Pretty.markup m and pretty_ast m ast = ast - |> prt_t ctxt prtabs trf markup_trans markup_extern + |> prt_t ctxt prtabs trf constrain_output markup_trans markup_extern |> Pretty.markup m and markup_ast is_typing a A = - Pretty.make_block (markup_block is_typing A) - [(if is_typing then pretty_ast else pretty_typ_ast) Markup.empty a] + make_block is_typing A + ((if is_typing then pretty_ast else pretty_typ_ast) Markup.empty a) - and markup_block is_typing A = - let val cache = if is_typing then cache1 else cache2 in - (case Ast.Table.lookup (! cache) A of - SOME block => block - | NONE => - let - val ((bg1, bg2), en) = if is_typing then typing_elem else sorting_elem; - val B = Pretty.symbolic_output (pretty_typ_ast Markup.empty A); - val bg = implode (bg1 :: Bytes.contents B @ [bg2]); - val block = {markup = (bg, en), open_block = false, consistent = false, indent = 0}; - in Unsynchronized.change cache (Ast.Table.update (A, block)); block end) - end; + and make_block is_typing A = + let + val cache = if is_typing then cache1 else cache2; + val block = + (case Ast.Table.lookup (! cache) A of + SOME block => block + | NONE => + let + val ((bg1, bg2), en) = if is_typing then typing_elem else sorting_elem; + val B = Pretty.symbolic_output (pretty_typ_ast Markup.empty A); + val bg = implode (bg1 :: Bytes.contents B @ [bg2]); + val block = {markup = (bg, en), open_block = false, consistent = false, indent = 0}; + in Unsynchronized.change cache (Ast.Table.update (A, block)); block end); + in Pretty.make_block block o single end + + and constrain_output A prt = make_block true A prt; in t_to_ast ctxt (Syntax.print_translation syn) t |> Ast.normalize ctxt (Syntax.print_rules syn)