# HG changeset patch # User wenzelm # Date 1728994798 -7200 # Node ID 26ecbac09941c4db9982fa274ae8300e18d1e7a8 # Parent 0278f6d87bad67095e457316e3f835e8e4658f59 allow type constraints for const_syntax; cope with that in ast translations and mixfix templates; minor adjustments to print_ast_translation functions in ML; diff -r 0278f6d87bad -r 26ecbac09941 NEWS --- a/NEWS Tue Oct 15 12:18:02 2024 +0200 +++ b/NEWS Tue Oct 15 14:19:58 2024 +0200 @@ -46,6 +46,14 @@ 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 option "show_consts_markup". 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. + * The Simplifier now supports special "congprocs", using keyword 'congproc' or 'weak_congproc' in the 'simproc_setup' command (or ML antiquotation of the same name). See also diff -r 0278f6d87bad -r 26ecbac09941 src/Pure/Isar/attrib.ML --- a/src/Pure/Isar/attrib.ML Tue Oct 15 12:18:02 2024 +0200 +++ b/src/Pure/Isar/attrib.ML Tue Oct 15 14:19:58 2024 +0200 @@ -606,6 +606,7 @@ register_config_bool Printer.show_sorts #> register_config_bool Printer.show_types #> register_config_bool Printer.show_markup #> + register_config_bool Printer.show_consts_markup #> register_config_bool Printer.show_structs #> register_config_bool Printer.show_question_marks #> register_config_bool Syntax.ambiguity_warning #> diff -r 0278f6d87bad -r 26ecbac09941 src/Pure/Syntax/ast.ML --- a/src/Pure/Syntax/ast.ML Tue Oct 15 12:18:02 2024 +0200 +++ b/src/Pure/Syntax/ast.ML Tue Oct 15 14:19:58 2024 +0200 @@ -137,13 +137,16 @@ fun fold_ast_p c = uncurry (fold_rev (fn x => fn xs => Appl [Constant c, x, xs])); -fun unfold_ast c (y as Appl [Constant c', x, xs]) = +fun unfold_ast c (y as Appl [Appl [Constant "_constrain", Constant c', _], x, xs]) = + if c = c' then x :: unfold_ast c xs else [y] + | 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]; -fun unfold_ast_p c (y as Appl [Constant c', x, xs]) = - if c = c' then apfst (cons x) (unfold_ast_p c xs) - else ([], y) +fun unfold_ast_p c (y as Appl [Appl [Constant "_constrain", Constant c', _], x, xs]) = + if c = c' then apfst (cons x) (unfold_ast_p c xs) else ([], y) + | unfold_ast_p c (y as Appl [Constant c', x, xs]) = + if c = c' then apfst (cons x) (unfold_ast_p c xs) else ([], y) | unfold_ast_p _ y = ([], y); @@ -156,8 +159,12 @@ 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 +fun const_match (Constant a) b = a = b + | const_match (Variable a) b = a = b + | const_match (Appl [Constant "_constrain", ast, _]) b = const_match ast b + | const_match _ _ = false; + +fun match1 ast (Constant b) env = if const_match ast 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 @@ -195,6 +202,8 @@ fun head_name (Constant a) = SOME a | head_name (Variable a) = SOME a + | head_name (Appl [Constant "_constrain", Constant a, _]) = SOME a + | head_name (Appl (Appl [Constant "_constrain", Constant a, _] :: _)) = SOME a | head_name (Appl (Constant a :: _)) = SOME a | head_name (Appl (Variable a :: _)) = SOME a | head_name _ = NONE; diff -r 0278f6d87bad -r 26ecbac09941 src/Pure/Syntax/printer.ML --- a/src/Pure/Syntax/printer.ML Tue Oct 15 12:18:02 2024 +0200 +++ b/src/Pure/Syntax/printer.ML Tue Oct 15 14:19:58 2024 +0200 @@ -10,6 +10,7 @@ val show_types: bool Config.T val show_sorts: bool Config.T val show_markup: bool Config.T + val show_consts_markup: bool Config.T val show_structs: bool Config.T val show_question_marks: bool Config.T val pretty_priority: int Config.T @@ -52,6 +53,7 @@ val show_sorts = Config.declare_option_bool ("show_sorts", \<^here>); val show_markup_default = Unsynchronized.ref false; val show_markup = Config.declare_bool ("show_markup", \<^here>) (fn _ => ! show_markup_default); +val show_consts_markup = Config.declare_bool ("show_consts_markup", \<^here>) (K false); val show_structs = Config.declare_bool ("show_structs", \<^here>) (K false); val show_question_marks = Config.declare_option_bool ("show_question_marks", \<^here>); val show_type_emphasis = Config.declare_bool ("show_type_emphasis", \<^here>) (K true); @@ -226,9 +228,21 @@ else if curried then Syntax_Trans.applC_ast_tr' else Syntax_Trans.appl_ast_tr'; + fun constrain_trans (Ast.Appl [Ast.Constant (a as "_constrain"), ast, ty]) = + markup_trans a [ast, ty] + | constrain_trans _ = NONE; + fun 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 (cc as Ast.Appl [Ast.Constant "_constrain", c as Ast.Constant a, _]) = + combination p c a [] (SOME cc) + | main p (c as Ast.Constant a) = + combination p c a [] NONE + | main p + (Ast.Appl ((cc as Ast.Appl [Ast.Constant "_constrain", c as Ast.Constant a, _]) :: + (args as _ :: _))) = + combination p c a args (SOME cc) + | main p (Ast.Appl ((c as Ast.Constant a) :: (args as _ :: _))) = + combination p c a args NONE | main p (Ast.Appl (f :: (args as _ :: _))) = main p (application (f, args)) | main _ (ast as Ast.Appl _) = raise Ast.AST ("pretty: malformed ast", [ast]) @@ -240,7 +254,7 @@ |> Config.put pretty_priority p |> pretty) tabs trf markup_trans (markup, extern) ast - and combination p c a args = + and combination p c a args constraint = (case translation p a args of SOME prts => prts | NONE => @@ -254,8 +268,11 @@ in (case entry of NONE => - if nargs = 0 then [Pretty.marks_str (markup a, extern a)] - else main p (application (c, args)) + if nargs = 0 then + (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)) | SOME (symbs, n, q) => if nargs = n then parens p q a (symbs, args) else main p (application (split_args n [c] args))) diff -r 0278f6d87bad -r 26ecbac09941 src/Pure/Syntax/syntax_phases.ML --- a/src/Pure/Syntax/syntax_phases.ML Tue Oct 15 12:18:02 2024 +0200 +++ b/src/Pure/Syntax/syntax_phases.ML Tue Oct 15 14:19:58 2024 +0200 @@ -662,6 +662,7 @@ let val show_types = Config.get ctxt show_types orelse Config.get ctxt show_sorts; val show_markup = Config.get ctxt show_markup; + val show_consts_markup = Config.get ctxt show_consts_markup; fun constrain_ast clean T ast = if T = dummyT then ast @@ -684,11 +685,18 @@ in Ast.mk_appl (var_ast (c $ Syntax.free x) X) (map ast_of ts) end | (Const ("_idtdummy", T), ts) => Ast.mk_appl (var_ast (Syntax.const "_idtdummy") T) (map ast_of ts) - | (Const (c, T), ts) => trans c (Type_Annotation.smash T) ts + | (Const (c, T), ts) => const_ast c T ts | (t, ts) => Ast.mk_appl (simple_ast_of ctxt t) (map ast_of ts)) - and trans a T args = ast_of (trf a ctxt T args) - handle Match => Ast.mk_appl (Ast.Constant a) (map ast_of args) + and const_ast a T args = + (case SOME (trf a ctxt (Type_Annotation.smash T) args) handle Match => NONE of + SOME t => ast_of t + | NONE => + let + val c = + Ast.Constant a + |> (show_markup andalso show_consts_markup) ? constrain_ast {clean = true} T; + in Ast.mk_appl c (map ast_of args) end) and var_ast v T = simple_ast_of ctxt v