# HG changeset patch # User wenzelm # Date 1724447813 -7200 # Node ID 2c0604845f745ba299dd6ac09d8ed7c2fc8accf5 # Parent 6adf6cc82013288577404bd218415ad8a7f63880# Parent 701912f5645a025519be6735fb1970437ed364c5 merged diff -r 6adf6cc82013 -r 2c0604845f74 src/CCL/Set.thy --- a/src/CCL/Set.thy Fri Aug 23 18:40:12 2024 +0200 +++ b/src/CCL/Set.thy Fri Aug 23 23:16:53 2024 +0200 @@ -21,6 +21,8 @@ "_Coll" :: "[idt, o] \ 'a set" ("(1{_./ _})") translations "{x. P}" == "CONST Collect(\x. P)" +syntax_consts + "_Coll" == Collect lemma CollectI: "P(a) \ a : {x. P(x)}" apply (rule mem_Collect_iff [THEN iffD2]) @@ -53,6 +55,9 @@ translations "ALL x:A. P" == "CONST Ball(A, \x. P)" "EX x:A. P" == "CONST Bex(A, \x. P)" +syntax_consts + "_Ball" == Ball and + "_Bex" == Bex lemma ballI: "(\x. x:A \ P(x)) \ ALL x:A. P(x)" by (simp add: Ball_def) @@ -127,6 +132,9 @@ translations "INT x:A. B" == "CONST INTER(A, \x. B)" "UN x:A. B" == "CONST UNION(A, \x. B)" +syntax_consts + "_INTER" == INTER and + "_UNION" == UNION definition Inter :: "(('a set)set) \ 'a set" where "Inter(S) == (INT x:S. x)" diff -r 6adf6cc82013 -r 2c0604845f74 src/CCL/Term.thy --- a/src/CCL/Term.thy Fri Aug 23 18:40:12 2024 +0200 +++ b/src/CCL/Term.thy Fri Aug 23 23:16:53 2024 +0200 @@ -50,6 +50,7 @@ syntax "_let1" :: "[idt,i,i]\i" ("(3let _ be _/ in _)" [0,0,60] 60) translations "let x be a in e" == "CONST let1(a, \x. e)" +syntax_consts "_let1" == let1 definition letrec :: "[[i,i\i]\i,(i\i)\i]\i" where "letrec(h, b) == b(\x. fix(\f. lam x. h(x,\y. f`y))`x)" @@ -122,6 +123,10 @@ (\<^const_syntax>\letrec3\, K letrec3_tr')] end \ +syntax_consts + "_letrec" == letrec and + "_letrec2" == letrec2 and + "_letrec3" == letrec3 definition nrec :: "[i,i,[i,i]\i]\i" where "nrec(n,b,c) == letrec g x be ncase(x, b, \y. c(y,g(y))) in g(n)" diff -r 6adf6cc82013 -r 2c0604845f74 src/CCL/Type.thy --- a/src/CCL/Type.thy Fri Aug 23 18:40:12 2024 +0200 +++ b/src/CCL/Type.thy Fri Aug 23 23:16:53 2024 +0200 @@ -16,6 +16,8 @@ "_Subtype" :: "[idt, 'a set, o] \ 'a set" ("(1{_: _ ./ _})") translations "{x: A. B}" == "CONST Subtype(A, \x. B)" +syntax_consts + "_Subtype" == Subtype definition Unit :: "i set" where "Unit == {x. x=one}" @@ -48,6 +50,9 @@ (\<^const_syntax>\Sigma\, fn _ => Syntax_Trans.dependent_tr' (\<^syntax_const>\_Sigma\, \<^syntax_const>\_star\))] \ +syntax_consts + "_Pi" "_arrow" \ Pi and + "_Sigma" "_star" \ Sigma definition Nat :: "i set" where "Nat == lfp(\X. Unit + X)" diff -r 6adf6cc82013 -r 2c0604845f74 src/CTT/CTT.thy --- a/src/CTT/CTT.thy Fri Aug 23 18:40:12 2024 +0200 +++ b/src/CTT/CTT.thy Fri Aug 23 23:16:53 2024 +0200 @@ -61,6 +61,9 @@ translations "\x:A. B" \ "CONST Prod(A, \x. B)" "\x:A. B" \ "CONST Sum(A, \x. B)" +syntax_consts + "_PROD" \ Prod and + "_SUM" \ Sum abbreviation Arrow :: "[t,t]\t" (infixr "\" 30) where "A \ B \ \_:A. B" diff -r 6adf6cc82013 -r 2c0604845f74 src/Cube/Cube.thy --- a/src/Cube/Cube.thy Fri Aug 23 18:40:12 2024 +0200 +++ b/src/Cube/Cube.thy Fri Aug 23 23:16:53 2024 +0200 @@ -52,6 +52,13 @@ [(\<^const_syntax>\Prod\, fn _ => Syntax_Trans.dependent_tr' (\<^syntax_const>\_Pi\, \<^syntax_const>\_arrow\))] \ +syntax_consts + "_Trueprop" \ Trueprop and + "_MT_context" \ MT_context and + "_Context" \ Context and + "_Has_type" \ Has_type and + "_Lam" \ Abs and + "_Pi" "_arrow" \ Prod axiomatization where s_b: "*: \" and diff -r 6adf6cc82013 -r 2c0604845f74 src/FOL/IFOL.thy --- a/src/FOL/IFOL.thy Fri Aug 23 18:40:12 2024 +0200 +++ b/src/FOL/IFOL.thy Fri Aug 23 23:16:53 2024 +0200 @@ -103,6 +103,7 @@ syntax "_Uniq" :: "pttrn \ o \ o" ("(2\\<^sub>\\<^sub>1 _./ _)" [0, 10] 10) translations "\\<^sub>\\<^sub>1x. P" \ "CONST Uniq (\x. P)" +syntax_consts "_Uniq" \ Uniq print_translation \ [Syntax_Trans.preserve_binder_abs_tr' \<^const_syntax>\Uniq\ \<^syntax_const>\_Uniq\] @@ -746,10 +747,10 @@ "" :: \letbind => letbinds\ (\_\) "_binds" :: \[letbind, letbinds] => letbinds\ (\_;/ _\) "_Let" :: \[letbinds, 'a] => 'a\ (\(let (_)/ in (_))\ 10) - translations "_Let(_binds(b, bs), e)" == "_Let(b, _Let(bs, e))" "let x = a in e" == "CONST Let(a, \x. e)" +syntax_consts "_Let" \ Let lemma LetI: assumes \\x. x = t \ P(u(x))\ diff -r 6adf6cc82013 -r 2c0604845f74 src/Pure/Isar/isar_cmd.ML --- a/src/Pure/Isar/isar_cmd.ML Fri Aug 23 18:40:12 2024 +0200 +++ b/src/Pure/Isar/isar_cmd.ML Fri Aug 23 23:16:53 2024 +0200 @@ -1,5 +1,5 @@ (* Title: Pure/Isar/isar_cmd.ML - Author: Markus Wenzel, TU Muenchen + Author: Makarius Miscellaneous Isar commands. *) @@ -15,6 +15,10 @@ val print_ast_translation: Input.source -> theory -> theory val translations: (xstring * string) Syntax.trrule list -> theory -> theory val no_translations: (xstring * string) Syntax.trrule list -> theory -> theory + val syntax_consts: ((string * Position.T) list * (xstring * Position.T) list) list -> + theory -> theory + val syntax_types: ((string * Position.T) list * (xstring * Position.T) list) list -> + theory -> theory val oracle: bstring * Position.range -> Input.source -> theory -> theory val declaration: {syntax: bool, pervasive: bool} -> Input.source -> local_theory -> local_theory val qed: Method.text_range option -> Toplevel.transition -> Toplevel.transition @@ -108,6 +112,44 @@ fun no_translations args thy = Sign.del_trrules (read_trrules thy args) thy; +(* syntax consts/types (after translation) *) + +local + +fun syntax_deps_cmd f args thy = + let + val ctxt = Proof_Context.init_global thy; + + val check_lhs = Proof_Context.check_syntax_const ctxt; + fun check_rhs (b: xstring, pos: Position.T) = + let + val (c: string, reports) = f ctxt (b, pos); + val _ = Context_Position.reports ctxt reports; + in c end; + + fun check (raw_lhs, raw_rhs) = + let + val lhs = map check_lhs raw_lhs; + val rhs = map check_rhs raw_rhs; + in map (fn l => (l, rhs)) lhs end; + in Sign.syntax_deps (maps check args) thy end; + +fun check_const ctxt (s, pos) = + Proof_Context.check_const {proper = false, strict = true} ctxt (s, [pos]) + |>> (Term.dest_Const_name #> Lexicon.mark_const); + +fun check_type_name ctxt arg = + Proof_Context.check_type_name {proper = false, strict = true} ctxt arg + |>> (Term.dest_Type_name #> Lexicon.mark_type); + +in + +val syntax_consts = syntax_deps_cmd check_const; +val syntax_types = syntax_deps_cmd check_type_name; + +end; + + (* oracles *) fun oracle (name, range) source = diff -r 6adf6cc82013 -r 2c0604845f74 src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML Fri Aug 23 18:40:12 2024 +0200 +++ b/src/Pure/Isar/proof_context.ML Fri Aug 23 23:16:53 2024 +0200 @@ -155,6 +155,7 @@ val apply_case: Rule_Cases.T -> Proof.context -> (string * term list) list * Proof.context val check_case: Proof.context -> bool -> string * Position.T -> binding option list -> Rule_Cases.T + val is_syntax_const: Proof.context -> string -> bool val check_syntax_const: Proof.context -> string * Position.T -> string val syntax: bool -> Syntax.mode -> (string * typ * mixfix) list -> Proof.context -> Proof.context @@ -570,8 +571,7 @@ let val reports = ps |> filter (Context_Position.is_reported ctxt) - |> map (fn pos => - (pos, Markup.name x (if Name.is_skolem x then Markup.skolem else Markup.free))); + |> map (fn pos => (pos, Markup.name x (Variable.markup ctxt x))); in (Free (x, infer_type ctxt (x, dummyT)), reports) end | (_, SOME d) => let @@ -1126,8 +1126,10 @@ (* syntax *) +val is_syntax_const = Syntax.is_const o syntax_of; + fun check_syntax_const ctxt (c, pos) = - if is_some (Syntax.lookup_const (syntax_of ctxt) c) then c + if is_syntax_const ctxt c then c else error ("Unknown syntax const: " ^ quote c ^ Position.here pos); fun syntax add mode args ctxt = diff -r 6adf6cc82013 -r 2c0604845f74 src/Pure/Pure.thy --- a/src/Pure/Pure.thy Fri Aug 23 18:40:12 2024 +0200 +++ b/src/Pure/Pure.thy Fri Aug 23 23:16:53 2024 +0200 @@ -15,9 +15,10 @@ and "text" "txt" :: document_body and "text_raw" :: document_raw and "default_sort" :: thy_decl - and "typedecl" "nonterminal" "judgment" "consts" "syntax" "no_syntax" "translations" - "no_translations" "type_notation" "no_type_notation" "notation" "no_notation" "alias" - "type_alias" "declare" "hide_class" "hide_type" "hide_const" "hide_fact" :: thy_decl + and "typedecl" "nonterminal" "judgment" "consts" "syntax" "no_syntax" "syntax_consts" + "syntax_types" "translations" "no_translations" "type_notation" "no_type_notation" "notation" + "no_notation" "alias" "type_alias" "declare" "hide_class" "hide_type" "hide_const" + "hide_fact" :: thy_decl and "type_synonym" "definition" "abbreviation" "lemmas" :: thy_defn and "axiomatization" :: thy_stmt and "external_file" "bibtex_file" "ROOTS_file" :: thy_load @@ -401,6 +402,19 @@ (Parse.syntax_mode -- Scan.repeat1 Parse.const_decl >> uncurry (Local_Theory.syntax_cmd false)); +val syntax_consts = + Parse.and_list1 + ((Scan.repeat1 Parse.name_position --| (\<^keyword>\\\ || \<^keyword>\==\)) -- + Parse.!!! (Scan.repeat1 Parse.name_position)); + +val _ = + Outer_Syntax.command \<^command_keyword>\syntax_consts\ "declare syntax const dependencies" + (syntax_consts >> (Toplevel.theory o Isar_Cmd.syntax_consts)); + +val _ = + Outer_Syntax.command \<^command_keyword>\syntax_types\ "declare syntax const dependencies (type names)" + (syntax_consts >> (Toplevel.theory o Isar_Cmd.syntax_types)); + val trans_pat = Scan.optional (\<^keyword>\(\ |-- Parse.!!! (Parse.inner_syntax Parse.name --| \<^keyword>\)\)) "logic" diff -r 6adf6cc82013 -r 2c0604845f74 src/Pure/Syntax/mixfix.ML --- a/src/Pure/Syntax/mixfix.ML Fri Aug 23 18:40:12 2024 +0200 +++ b/src/Pure/Syntax/mixfix.ML Fri Aug 23 23:16:53 2024 +0200 @@ -182,7 +182,7 @@ val mfix = map mfix_of type_decls; val _ = map2 check_args type_decls mfix; - val consts = map (fn (t, _, _) => (t, "")) type_decls; + val consts = map (fn (t, _, _) => (t, [])) type_decls; in Syntax_Ext.syn_ext [] (map_filter I mfix) consts ([], [], [], []) ([], []) end; @@ -235,7 +235,9 @@ |> map (Syntax_Ext.stamp_trfun binder_stamp o apsnd Syntax_Trans.non_typed_tr' o Syntax_Trans.mk_binder_tr' o swap); - val consts = binders @ map (fn (c, _, _) => (c, "")) const_decls; + val consts = + map (fn (c, b) => (c, [b])) binders @ + map (fn (c, _, _) => (c, [])) const_decls; in Syntax_Ext.syn_ext logical_types mfix consts ([], binder_trs, binder_trs', []) ([], []) end; end; diff -r 6adf6cc82013 -r 2c0604845f74 src/Pure/Syntax/printer.ML --- a/src/Pure/Syntax/printer.ML Fri Aug 23 18:40:12 2024 +0200 +++ b/src/Pure/Syntax/printer.ML Fri Aug 23 23:16:53 2024 +0200 @@ -33,12 +33,13 @@ val pretty_term_ast: bool -> Proof.context -> prtabs -> (string -> Proof.context -> Ast.ast list -> Ast.ast) -> (string -> Ast.ast list -> Pretty.T option) -> - (string -> Markup.T list * string) -> + ((string -> Markup.T list) * (string -> string)) -> Ast.ast -> Pretty.T list val pretty_typ_ast: Proof.context -> prtabs -> (string -> Proof.context -> Ast.ast list -> Ast.ast) -> (string -> Ast.ast list -> Pretty.T option) -> - (string -> Markup.T list * string) -> Ast.ast -> Pretty.T list + ((string -> Markup.T list) * (string -> string)) -> + Ast.ast -> Pretty.T list end; structure Printer: PRINTER = @@ -202,10 +203,14 @@ | is_chain [Arg _] = true | is_chain _ = false; +val pretty_type_mode = Config.declare_bool ("Syntax.pretty_type_mode", \<^here>) (K false); +val pretty_curried = Config.declare_bool ("Syntax.pretty_curried", \<^here>) (K false); val pretty_priority = Config.declare_int ("Syntax.pretty_priority", \<^here>) (K 0); -fun pretty type_mode curried ctxt tabs trf markup_trans markup_extern ast0 = +fun pretty ctxt tabs trf markup_trans markup_extern ast0 = 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*) @@ -224,8 +229,10 @@ in if type_mode then (astT (t, p) @ Ts, args') else - (pretty true curried (Config.put pretty_priority p ctxt) - tabs trf markup_trans markup_extern t @ Ts, args') + 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 (do_mark, s) :: symbs, args) = let @@ -254,7 +261,7 @@ [Block (Syntax_Ext.block_indent 1, String (false, "(") :: pr @ [String (false, ")")])] else pr, args)) - and atomT a = Pretty.marks_str (markup_extern a) + 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) @@ -271,7 +278,7 @@ 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') + 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); @@ -291,14 +298,20 @@ (* pretty_term_ast *) -fun pretty_term_ast curried ctxt prtabs trf markup_trans extern ast = - pretty false curried ctxt (mode_tabs prtabs (print_mode_value ())) trf markup_trans extern ast; +fun pretty_term_ast curried ctxt prtabs trf markup_trans markup_extern ast = + let val ctxt' = ctxt + |> Config.put pretty_type_mode false + |> Config.put pretty_curried curried + in pretty ctxt' (mode_tabs prtabs (print_mode_value ())) trf markup_trans markup_extern ast end; (* pretty_typ_ast *) -fun pretty_typ_ast ctxt prtabs trf markup_trans extern ast = - pretty true false ctxt (mode_tabs prtabs (print_mode_value ())) trf markup_trans extern ast; +fun pretty_typ_ast ctxt prtabs trf markup_trans markup_extern ast = + let val ctxt' = ctxt + |> Config.put pretty_type_mode true + |> Config.put pretty_curried false + in pretty ctxt' (mode_tabs prtabs (print_mode_value ())) trf markup_trans markup_extern ast end; end; diff -r 6adf6cc82013 -r 2c0604845f74 src/Pure/Syntax/syntax.ML --- a/src/Pure/Syntax/syntax.ML Fri Aug 23 18:40:12 2024 +0200 +++ b/src/Pure/Syntax/syntax.ML Fri Aug 23 23:16:53 2024 +0200 @@ -77,7 +77,8 @@ val eq_syntax: syntax * syntax -> bool datatype approx = Prefix of string | Infix of {assoc: Printer.assoc, delim: string, pri: int} val get_approx: syntax -> string -> approx option - val lookup_const: syntax -> string -> string option + val get_consts: syntax -> string -> string list + val is_const: syntax -> string -> bool val is_keyword: syntax -> string -> bool val tokenize: syntax -> bool -> Symbol_Pos.T list -> Lexicon.token list val parse: syntax -> string -> Lexicon.token list -> Parser.parsetree list @@ -111,6 +112,7 @@ val update_type_gram: bool -> mode -> (string * typ * mixfix) list -> syntax -> syntax val update_const_gram: bool -> string list -> mode -> (string * typ * mixfix) list -> syntax -> syntax + val update_consts: (string * string list) list -> syntax -> syntax val update_trrules: Ast.ast trrule list -> syntax -> syntax val remove_trrules: Ast.ast trrule list -> syntax -> syntax val const: string -> term @@ -411,7 +413,7 @@ input: Syntax_Ext.xprod list, lexicon: Scan.lexicon, gram: Parser.gram Synchronized.cache, - consts: string Symtab.table, + consts: unit Graph.T, prmodes: string list, parse_ast_trtab: ((Proof.context -> Ast.ast list -> Ast.ast) * stamp) Symtab.table, parse_ruletab: ruletab, @@ -440,7 +442,7 @@ | NONE => Printer.get_binder prtabs c) |> Option.map Prefix); -fun lookup_const (Syntax ({consts, ...}, _)) = Symtab.lookup consts; +fun is_const (Syntax ({consts, ...}, _)) = Graph.defined consts; fun is_keyword (Syntax ({lexicon, ...}, _)) = Scan.is_literal lexicon o Symbol.explode; fun tokenize (Syntax ({lexicon, ...}, _)) = Lexicon.tokenize lexicon; fun parse (Syntax ({gram, ...}, _)) = Parser.parse (cache_eval gram); @@ -466,13 +468,35 @@ Synchronized.cache (fn () => Parser.make_gram new_xprods [] NONE); +(* syntax consts *) + +fun err_cyclic_consts css = + error (cat_lines (map (fn cs => + "Cycle in syntax consts: " ^ (space_implode " \ " (map quote cs))) css)); + +fun get_consts (Syntax ({consts, ...}, _)) c = + if Graph.defined consts c then + Graph.all_preds consts [c] + |> filter (Graph.Keys.is_empty o Graph.imm_preds consts) + else [c]; + +fun update_consts (c, bs) consts = + if c = "" orelse (null bs andalso (Lexicon.is_marked c orelse Graph.defined consts c)) + then consts + else + consts + |> fold (fn a => Graph.default_node (a, ())) (c :: bs) + |> Graph.add_deps_acyclic (c, bs) + handle Graph.CYCLES css => err_cyclic_consts css; + + (* empty_syntax *) val empty_syntax = Syntax ({input = [], lexicon = Scan.empty_lexicon, gram = Synchronized.cache (fn () => Parser.empty_gram), - consts = Symtab.empty, + consts = Graph.empty, prmodes = [], parse_ast_trtab = Symtab.empty, parse_ruletab = Symtab.empty, @@ -485,11 +509,6 @@ (* update_syntax *) -fun update_const (c, b) tab = - if c = "" orelse (b = "" andalso (Lexicon.is_marked c orelse Symtab.defined tab c)) - then tab - else Symtab.update (c, b) tab; - fun update_syntax (mode, inout) syn_ext (Syntax (tabs, _)) = let val {input, lexicon, gram, consts = consts1, prmodes, parse_ast_trtab, parse_ruletab, @@ -505,7 +524,7 @@ ({input = new_xprods @ input, lexicon = fold Scan.extend_lexicon (Syntax_Ext.delims_of new_xprods) lexicon, gram = if null new_xprods then gram else extend_gram new_xprods input gram, - consts = fold update_const consts2 consts1, + consts = fold update_consts consts2 consts1, prmodes = insert (op =) mode prmodes, parse_ast_trtab = update_trtab "parse ast translation" (if_inout parse_ast_translation) parse_ast_trtab, @@ -577,7 +596,9 @@ ({input = input', lexicon = Scan.merge_lexicons (lexicon1, lexicon2), gram = gram', - consts = Symtab.merge (K true) (consts1, consts2), + consts = + Graph.merge_acyclic (op =) (consts1, consts2) + handle Graph.CYCLES css => err_cyclic_consts css, prmodes = Library.merge (op =) (prmodes1, prmodes2), parse_ast_trtab = merge_trtabs "parse ast translation" parse_ast_trtab1 parse_ast_trtab2, @@ -620,7 +641,7 @@ val {consts, parse_ast_trtab, parse_ruletab, parse_trtab, print_trtab, print_ruletab, print_ast_trtab, ...} = tabs; in - [pretty_tab "consts:" consts, + [pretty_strs_qs "consts:" (sort_strings (Graph.keys consts)), pretty_tab "parse_ast_translation:" parse_ast_trtab, pretty_ruletab "parse_rules:" parse_ruletab, pretty_tab "parse_translation:" parse_trtab, @@ -692,6 +713,8 @@ fun update_const_gram add logical_types prmode decls = (if add then update_syntax else remove_syntax) prmode (Mixfix.syn_ext_consts logical_types decls); +val update_consts = update_syntax mode_default o Syntax_Ext.syn_ext_consts; + val update_trrules = update_syntax mode_default o Syntax_Ext.syn_ext_rules o check_rules; val remove_trrules = remove_syntax mode_default o Syntax_Ext.syn_ext_rules o check_rules; diff -r 6adf6cc82013 -r 2c0604845f74 src/Pure/Syntax/syntax_ext.ML --- a/src/Pure/Syntax/syntax_ext.ML Fri Aug 23 18:40:12 2024 +0200 +++ b/src/Pure/Syntax/syntax_ext.ML Fri Aug 23 23:16:53 2024 +0200 @@ -23,7 +23,7 @@ datatype syn_ext = Syn_Ext of { xprods: xprod list, - consts: (string * string) list, + consts: (string * string list) list, parse_ast_translation: (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list, parse_rules: (Ast.ast * Ast.ast) list, parse_translation: (string * ((Proof.context -> term list -> term) * stamp)) list, @@ -34,11 +34,12 @@ val mixfix_args: Input.source -> int val escape: string -> string val syn_ext: string list -> mfix list -> - (string * string) list -> (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list * + (string * string list) list -> (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list * (string * ((Proof.context -> term list -> term) * stamp)) list * (string * ((Proof.context -> typ -> term list -> term) * stamp)) list * (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list -> (Ast.ast * Ast.ast) list * (Ast.ast * Ast.ast) list -> syn_ext + val syn_ext_consts: (string * string list) list -> syn_ext val syn_ext_rules: (Ast.ast * Ast.ast) list * (Ast.ast * Ast.ast) list -> syn_ext val syn_ext_trfuns: (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list * @@ -345,7 +346,7 @@ Ast.mk_appl (Ast.Constant indexed_const) (xs1 @ [Ast.mk_appl (Ast.Constant "_index") [i]] @ xs2); val rhs = Ast.mk_appl (Ast.Constant const) (i :: xs); - in (indexed_const, rangeT, SOME (indexed_const, const), SOME (lhs, rhs)) end; + in (indexed_const, rangeT, SOME (indexed_const, [const]), SOME (lhs, rhs)) end; val (symbs1, lhs) = add_args symbs0 typ' pris; @@ -389,7 +390,7 @@ datatype syn_ext = Syn_Ext of { xprods: xprod list, - consts: (string * string) list, + consts: (string * string list) list, parse_ast_translation: (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list, parse_rules: (Ast.ast * Ast.ast) list, parse_translation: (string * ((Proof.context -> term list -> term) * stamp)) list, @@ -409,7 +410,7 @@ val xprods = map #1 xprod_results; val consts' = map_filter #2 xprod_results; val parse_rules' = rev (map_filter #3 xprod_results); - val mfix_consts = map (fn Mfix x => (#3 x, "")) mfixes @ map (fn XProd x => (#3 x, "")) xprods; + val mfix_consts = map (fn Mfix x => (#3 x, [])) mfixes @ map (fn XProd x => (#3 x, [])) xprods; in Syn_Ext { xprods = xprods, @@ -423,6 +424,7 @@ end; +fun syn_ext_consts consts = syn_ext [] [] consts ([], [], [], []) ([], []); fun syn_ext_rules rules = syn_ext [] [] [] ([], [], [], []) rules; fun syn_ext_trfuns trfuns = syn_ext [] [] [] trfuns ([], []); diff -r 6adf6cc82013 -r 2c0604845f74 src/Pure/Syntax/syntax_phases.ML --- a/src/Pure/Syntax/syntax_phases.ML Fri Aug 23 18:40:12 2024 +0200 +++ b/src/Pure/Syntax/syntax_phases.ML Fri Aug 23 23:16:53 2024 +0200 @@ -53,10 +53,13 @@ [Name_Space.markup (Consts.space_of (Proof_Context.consts_of ctxt)) c]; fun markup_free ctxt x = - Variable.markup ctxt x :: - (if Variable.is_body ctxt orelse Variable.is_fixed ctxt x - then [Variable.markup_fixed ctxt x] - else []); + let + val m1 = + if Variable.is_fixed ctxt x then Variable.markup_fixed ctxt x + else if not (Variable.is_body ctxt) orelse Syntax.is_pretty_global ctxt then Markup.fixed x + else Markup.intensify; + val m2 = Variable.markup ctxt x; + in [m1, m2] end; fun markup_var xi = [Markup.name (Term.string_of_vname xi) Markup.var]; @@ -64,10 +67,8 @@ Markup.bound :: map (fn pos => Position.make_entity_markup def id Markup.boundN (name, pos)) ps; fun markup_entity ctxt c = - (case Syntax.lookup_const (Proof_Context.syntax_of ctxt) c of - SOME "" => [] - | SOME b => markup_entity ctxt b - | NONE => c |> Lexicon.unmark + 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, @@ -468,7 +469,7 @@ fun decode_appl ps asts = Ast.Appl (map (decode ps) asts) and decode ps (Ast.Constant c) = decode_const ps c | decode ps (Ast.Variable x) = - if is_some (Syntax.lookup_const syn x) orelse Long_Name.is_qualified x + if Syntax.is_const syn x orelse Long_Name.is_qualified x then decode_const ps x else decode_var ps x | decode ps (Ast.Appl (asts as (Ast.Constant c :: ast :: Ast.Variable x :: args))) = @@ -619,7 +620,7 @@ in (t1' $ t2', seen'') end; in #1 (prune (tm, [])) end; -fun mark_atoms is_syntax_const ctxt tm = +fun mark_atoms ctxt tm = let val {structs, fixes} = Syntax_Trans.get_idents ctxt; val show_structs = Config.get ctxt show_structs; @@ -630,7 +631,7 @@ | mark (t $ u) = mark t $ mark u | mark (Abs (x, T, t)) = Abs (x, T, mark t) | mark (t as Const (c, T)) = - if is_syntax_const c then t + if Proof_Context.is_syntax_const ctxt c then t else Const (Lexicon.mark_const c, T) | mark (t as Free (x, T)) = let val i = find_index (fn s => s = x) structs + 1 in @@ -648,7 +649,7 @@ in -fun term_to_ast is_syntax_const ctxt trf tm = +fun term_to_ast ctxt trf tm = let val show_types = Config.get ctxt show_types orelse Config.get ctxt show_sorts; val show_markup = Config.get ctxt show_markup; @@ -691,7 +692,7 @@ |> mark_aprop |> show_types ? prune_types |> Variable.revert_bounds ctxt - |> mark_atoms is_syntax_const ctxt + |> mark_atoms ctxt |> ast_of end; @@ -703,23 +704,32 @@ local -fun free_or_skolem ctxt x = - let - val m = - if Variable.is_fixed ctxt x orelse Syntax.is_pretty_global ctxt - then Markup.fixed x else Markup.intensify; - in - if Name.is_skolem x - then ([m, Markup.skolem], Variable.revert_fixed ctxt x) - else ([m, Markup.free], x) - end; +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 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 - NONE => (Markup.var, s) - | SOME x' => (Markup.skolem, Term.string_of_vname (x', i))) + SOME x' => (Markup.skolem, Term.string_of_vname (x', i)) + | NONE => (Markup.var, s)) | NONE => (Markup.var, s)); val typing_elem = YXML.output_markup_elem Markup.typing; @@ -734,17 +744,7 @@ val syn = Proof_Context.syntax_of ctxt; val prtabs = Syntax.prtabs syn; val trf = Syntax.print_ast_translation syn; - - fun markup_extern c = - (case Syntax.lookup_const syn c of - SOME "" => ([], c) - | SOME b => markup_extern b - | NONE => c |> Lexicon.unmark - {case_class = fn x => (markup_class ctxt x, Proof_Context.extern_class ctxt x), - case_type = fn x => (markup_type ctxt x, Proof_Context.extern_type ctxt x), - case_const = fn x => (markup_const ctxt x, Proof_Context.extern_const ctxt x), - case_fixed = fn x => free_or_skolem ctxt x, - case_default = fn x => ([], x)}); + val markup_extern = (markup_entity ctxt, extern ctxt); fun token_trans "_tfree" x = SOME (Pretty.mark_str (Markup.tfree, x)) | token_trans "_tvar" x = SOME (Pretty.mark_str (Markup.tvar, x)) @@ -801,12 +801,8 @@ fun unparse_term ctxt = let val thy = Proof_Context.theory_of ctxt; - val syn = Proof_Context.syntax_of ctxt; - in - unparse_t (term_to_ast (is_some o Syntax.lookup_const syn)) - (Printer.pretty_term_ast (not (Pure_Thy.old_appl_syntax thy))) - (Markup.language_term false) ctxt - end; + val curried = not (Pure_Thy.old_appl_syntax thy); + in unparse_t term_to_ast (Printer.pretty_term_ast curried) (Markup.language_term false) ctxt end; end; diff -r 6adf6cc82013 -r 2c0604845f74 src/Pure/pure_thy.ML --- a/src/Pure/pure_thy.ML Fri Aug 23 18:40:12 2024 +0200 +++ b/src/Pure/pure_thy.ML Fri Aug 23 23:16:53 2024 +0200 @@ -220,6 +220,8 @@ #> Sign.parse_ast_translation Syntax_Trans.pure_parse_ast_translation #> Sign.parse_translation Syntax_Trans.pure_parse_translation #> Sign.print_ast_translation Syntax_Trans.pure_print_ast_translation + #> Sign.syntax_deps + [("_bracket", ["\<^type>fun"]), ("_bigimpl", ["\<^const>Pure.imp"])] #> Sign.add_consts [(qualify (Binding.make ("term", \<^here>)), typ "'a \ prop", NoSyn), (qualify (Binding.make ("sort_constraint", \<^here>)), typ "'a itself \ prop", NoSyn), diff -r 6adf6cc82013 -r 2c0604845f74 src/Pure/sign.ML --- a/src/Pure/sign.ML Fri Aug 23 18:40:12 2024 +0200 +++ b/src/Pure/sign.ML Fri Aug 23 23:16:53 2024 +0200 @@ -78,6 +78,7 @@ val add_type_abbrev: Proof.context -> binding * string list * typ -> theory -> theory val syntax: bool -> Syntax.mode -> (string * typ * mixfix) list -> theory -> theory val syntax_cmd: bool -> Syntax.mode -> (string * string * mixfix) list -> theory -> theory + val syntax_deps: (string * string list) list -> theory -> theory val type_notation: bool -> Syntax.mode -> (typ * mixfix) list -> theory -> theory val notation: bool -> Syntax.mode -> (term * mixfix) list -> theory -> theory val declare_const: Proof.context -> (binding * typ) * mixfix -> theory -> term * theory @@ -392,6 +393,8 @@ val syntax = gen_syntax (K I); val syntax_cmd = gen_syntax Syntax.read_typ; +val syntax_deps = map_syn o Syntax.update_consts; + fun type_notation add mode args = let fun type_syntax (Type (c, args), mx) = diff -r 6adf6cc82013 -r 2c0604845f74 src/ZF/Bin.thy --- a/src/ZF/Bin.thy Fri Aug 23 18:40:12 2024 +0200 +++ b/src/ZF/Bin.thy Fri Aug 23 23:16:53 2024 +0200 @@ -119,6 +119,8 @@ ML_file \Tools/numeral_syntax.ML\ +syntax_consts + "_Int0" "_Int1" "_Int2" "_Int" "_Neg_Int1" "_Neg_Int2" "_Neg_Int" \ integ_of declare bin.intros [simp,TC] diff -r 6adf6cc82013 -r 2c0604845f74 src/ZF/Induct/Multiset.thy --- a/src/ZF/Induct/Multiset.thy Fri Aug 23 18:40:12 2024 +0200 +++ b/src/ZF/Induct/Multiset.thy Fri Aug 23 23:16:53 2024 +0200 @@ -77,6 +77,7 @@ "_MColl" :: "[pttrn, i, o] \ i" (\(1{# _ \ _./ _#})\) translations "{#x \ M. P#}" == "CONST MCollect(M, \x. P)" +syntax_consts "_MColl" \ MCollect (* multiset orderings *) diff -r 6adf6cc82013 -r 2c0604845f74 src/ZF/List.thy --- a/src/ZF/List.thy Fri Aug 23 18:40:12 2024 +0200 +++ b/src/ZF/List.thy Fri Aug 23 23:16:53 2024 +0200 @@ -17,12 +17,11 @@ syntax "_Nil" :: i (\[]\) "_List" :: "is \ i" (\[(_)]\) - translations "[x, xs]" == "CONST Cons(x, [xs])" "[x]" == "CONST Cons(x, [])" "[]" == "CONST Nil" - +syntax_consts "_List" \ Cons consts length :: "i\i" diff -r 6adf6cc82013 -r 2c0604845f74 src/ZF/OrdQuant.thy --- a/src/ZF/OrdQuant.thy Fri Aug 23 18:40:12 2024 +0200 +++ b/src/ZF/OrdQuant.thy Fri Aug 23 23:16:53 2024 +0200 @@ -30,6 +30,10 @@ "\x "CONST oall(a, \x. P)" "\x "CONST oex(a, \x. P)" "\x "CONST OUnion(a, \x. B)" +syntax_consts + "_oall" \ oall and + "_oex" \ oex and + "_OUNION" \ OUnion subsubsection \simplification of the new quantifiers\ @@ -197,6 +201,9 @@ translations "\x[M]. P" \ "CONST rall(M, \x. P)" "\x[M]. P" \ "CONST rex(M, \x. P)" +syntax_consts + "_rall" \ rall and + "_rex" \ rex subsubsection\Relativized universal quantifier\ diff -r 6adf6cc82013 -r 2c0604845f74 src/ZF/QPair.thy --- a/src/ZF/QPair.thy Fri Aug 23 18:40:12 2024 +0200 +++ b/src/ZF/QPair.thy Fri Aug 23 23:16:53 2024 +0200 @@ -48,6 +48,8 @@ "_QSUM" :: "[idt, i, i] \ i" (\(3QSUM _ \ _./ _)\ 10) translations "QSUM x \ A. B" => "CONST QSigma(A, \x. B)" +syntax_consts + "_QSUM" \ QSigma abbreviation qprod (infixr \<*>\ 80) where diff -r 6adf6cc82013 -r 2c0604845f74 src/ZF/UNITY/Union.thy --- a/src/ZF/UNITY/Union.thy Fri Aug 23 18:40:12 2024 +0200 +++ b/src/ZF/UNITY/Union.thy Fri Aug 23 23:16:53 2024 +0200 @@ -43,11 +43,12 @@ syntax "_JOIN1" :: "[pttrns, i] \ i" (\(3\_./ _)\ 10) "_JOIN" :: "[pttrn, i, i] \ i" (\(3\_ \ _./ _)\ 10) - translations "\x \ A. B" == "CONST JOIN(A, (\x. B))" "\x y. B" == "\x. \y. B" "\x. B" == "CONST JOIN(CONST state, (\x. B))" +syntax_consts + "_JOIN1" "_JOIN" == JOIN subsection\SKIP\ diff -r 6adf6cc82013 -r 2c0604845f74 src/ZF/ZF_Base.thy --- a/src/ZF/ZF_Base.thy Fri Aug 23 18:40:12 2024 +0200 +++ b/src/ZF/ZF_Base.thy Fri Aug 23 23:16:53 2024 +0200 @@ -41,6 +41,9 @@ translations "\x\A. P" \ "CONST Ball(A, \x. P)" "\x\A. P" \ "CONST Bex(A, \x. P)" +syntax_consts + "_Ball" \ Ball and + "_Bex" \ Bex subsection \Variations on Replacement\ @@ -52,9 +55,11 @@ where "Replace(A,P) \ PrimReplace(A, \x y. (\!z. P(x,z)) \ P(x,y))" syntax - "_Replace" :: "[pttrn, pttrn, i, o] \ i" (\(1{_ ./ _ \ _, _})\) + "_Replace" :: "[pttrn, pttrn, i, o] \ i" (\(1{_ ./ _ \ _, _})\) translations "{y. x\A, Q}" \ "CONST Replace(A, \x y. Q)" +syntax_consts + "_Replace" \ Replace (* Functional form of replacement -- analgous to ML's map functional *) @@ -66,7 +71,8 @@ "_RepFun" :: "[i, pttrn, i] \ i" (\(1{_ ./ _ \ _})\ [51,0,51]) translations "{b. x\A}" \ "CONST RepFun(A, \x. b)" - +syntax_consts + "_RepFun" \ RepFun (* Separation and Pairing can be derived from the Replacement and Powerset Axioms using the following definitions. *) @@ -77,6 +83,8 @@ "_Collect" :: "[pttrn, i, o] \ i" (\(1{_ \ _ ./ _})\) translations "{x\A. P}" \ "CONST Collect(A, \x. P)" +syntax_consts + "_Collect" \ Collect subsection \General union and intersection\ @@ -90,6 +98,9 @@ translations "\x\A. B" == "CONST Union({B. x\A})" "\x\A. B" == "CONST Inter({B. x\A})" +syntax_consts + "_UNION" == Union and + "_INTER" == Inter subsection \Finite sets and binary operations\ @@ -126,6 +137,8 @@ translations "{x, xs}" == "CONST cons(x, {xs})" "{x}" == "CONST cons(x, 0)" +syntax_consts + "_Finset" == cons subsection \Axioms\ @@ -191,6 +204,9 @@ "\x, y\" == "CONST Pair(x, y)" "\\x,y,zs\.b" == "CONST split(\x \y,zs\.b)" "\\x,y\.b" == "CONST split(\x y. b)" +syntax_consts + "_pattern" "_patterns" == split and + "_Tuple" == Pair definition Sigma :: "[i, i \ i] \ i" where "Sigma(A,B) \ \x\A. \y\B(x). {\x,y\}" @@ -256,6 +272,10 @@ "\x\A. B" == "CONST Pi(A, \x. B)" "\x\A. B" == "CONST Sigma(A, \x. B)" "\x\A. f" == "CONST Lambda(A, \x. f)" +syntax_consts + "_PROD" == Pi and + "_SUM" == Sigma and + "_lam" == Lambda subsection \ASCII syntax\ diff -r 6adf6cc82013 -r 2c0604845f74 src/ZF/func.thy --- a/src/ZF/func.thy Fri Aug 23 18:40:12 2024 +0200 +++ b/src/ZF/func.thy Fri Aug 23 23:16:53 2024 +0200 @@ -448,18 +448,14 @@ nonterminal updbinds and updbind syntax - - (* Let expressions *) - "_updbind" :: "[i, i] \ updbind" (\(2_ :=/ _)\) "" :: "updbind \ updbinds" (\_\) "_updbinds" :: "[updbind, updbinds] \ updbinds" (\_,/ _\) "_Update" :: "[i, updbinds] \ i" (\_/'((_)')\ [900,0] 900) - translations "_Update (f, _updbinds(b,bs))" == "_Update (_Update(f,b), bs)" "f(x:=y)" == "CONST update(f,x,y)" - +syntax_consts "_Update" "_updbind" \ update lemma update_apply [simp]: "f(x:=y) ` z = (if z=x then y else f`z)" apply (simp add: update_def)