--- 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] \<Rightarrow> 'a set" ("(1{_./ _})")
translations
"{x. P}" == "CONST Collect(\<lambda>x. P)"
+syntax_consts
+ "_Coll" == Collect
lemma CollectI: "P(a) \<Longrightarrow> a : {x. P(x)}"
apply (rule mem_Collect_iff [THEN iffD2])
@@ -53,6 +55,9 @@
translations
"ALL x:A. P" == "CONST Ball(A, \<lambda>x. P)"
"EX x:A. P" == "CONST Bex(A, \<lambda>x. P)"
+syntax_consts
+ "_Ball" == Ball and
+ "_Bex" == Bex
lemma ballI: "(\<And>x. x:A \<Longrightarrow> P(x)) \<Longrightarrow> ALL x:A. P(x)"
by (simp add: Ball_def)
@@ -127,6 +132,9 @@
translations
"INT x:A. B" == "CONST INTER(A, \<lambda>x. B)"
"UN x:A. B" == "CONST UNION(A, \<lambda>x. B)"
+syntax_consts
+ "_INTER" == INTER and
+ "_UNION" == UNION
definition Inter :: "(('a set)set) \<Rightarrow> 'a set"
where "Inter(S) == (INT x:S. x)"
--- 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]\<Rightarrow>i" ("(3let _ be _/ in _)" [0,0,60] 60)
translations "let x be a in e" == "CONST let1(a, \<lambda>x. e)"
+syntax_consts "_let1" == let1
definition letrec :: "[[i,i\<Rightarrow>i]\<Rightarrow>i,(i\<Rightarrow>i)\<Rightarrow>i]\<Rightarrow>i"
where "letrec(h, b) == b(\<lambda>x. fix(\<lambda>f. lam x. h(x,\<lambda>y. f`y))`x)"
@@ -122,6 +123,10 @@
(\<^const_syntax>\<open>letrec3\<close>, K letrec3_tr')]
end
\<close>
+syntax_consts
+ "_letrec" == letrec and
+ "_letrec2" == letrec2 and
+ "_letrec3" == letrec3
definition nrec :: "[i,i,[i,i]\<Rightarrow>i]\<Rightarrow>i"
where "nrec(n,b,c) == letrec g x be ncase(x, b, \<lambda>y. c(y,g(y))) in g(n)"
--- 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] \<Rightarrow> 'a set" ("(1{_: _ ./ _})")
translations
"{x: A. B}" == "CONST Subtype(A, \<lambda>x. B)"
+syntax_consts
+ "_Subtype" == Subtype
definition Unit :: "i set"
where "Unit == {x. x=one}"
@@ -48,6 +50,9 @@
(\<^const_syntax>\<open>Sigma\<close>,
fn _ => Syntax_Trans.dependent_tr' (\<^syntax_const>\<open>_Sigma\<close>, \<^syntax_const>\<open>_star\<close>))]
\<close>
+syntax_consts
+ "_Pi" "_arrow" \<rightleftharpoons> Pi and
+ "_Sigma" "_star" \<rightleftharpoons> Sigma
definition Nat :: "i set"
where "Nat == lfp(\<lambda>X. Unit + X)"
--- 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
"\<Prod>x:A. B" \<rightleftharpoons> "CONST Prod(A, \<lambda>x. B)"
"\<Sum>x:A. B" \<rightleftharpoons> "CONST Sum(A, \<lambda>x. B)"
+syntax_consts
+ "_PROD" \<rightleftharpoons> Prod and
+ "_SUM" \<rightleftharpoons> Sum
abbreviation Arrow :: "[t,t]\<Rightarrow>t" (infixr "\<longrightarrow>" 30)
where "A \<longrightarrow> B \<equiv> \<Prod>_:A. B"
--- 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>\<open>Prod\<close>,
fn _ => Syntax_Trans.dependent_tr' (\<^syntax_const>\<open>_Pi\<close>, \<^syntax_const>\<open>_arrow\<close>))]
\<close>
+syntax_consts
+ "_Trueprop" \<rightleftharpoons> Trueprop and
+ "_MT_context" \<rightleftharpoons> MT_context and
+ "_Context" \<rightleftharpoons> Context and
+ "_Has_type" \<rightleftharpoons> Has_type and
+ "_Lam" \<rightleftharpoons> Abs and
+ "_Pi" "_arrow" \<rightleftharpoons> Prod
axiomatization where
s_b: "*: \<box>" and
--- 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 \<Rightarrow> o \<Rightarrow> o" ("(2\<exists>\<^sub>\<le>\<^sub>1 _./ _)" [0, 10] 10)
translations "\<exists>\<^sub>\<le>\<^sub>1x. P" \<rightleftharpoons> "CONST Uniq (\<lambda>x. P)"
+syntax_consts "_Uniq" \<rightleftharpoons> Uniq
print_translation \<open>
[Syntax_Trans.preserve_binder_abs_tr' \<^const_syntax>\<open>Uniq\<close> \<^syntax_const>\<open>_Uniq\<close>]
@@ -746,10 +747,10 @@
"" :: \<open>letbind => letbinds\<close> (\<open>_\<close>)
"_binds" :: \<open>[letbind, letbinds] => letbinds\<close> (\<open>_;/ _\<close>)
"_Let" :: \<open>[letbinds, 'a] => 'a\<close> (\<open>(let (_)/ in (_))\<close> 10)
-
translations
"_Let(_binds(b, bs), e)" == "_Let(b, _Let(bs, e))"
"let x = a in e" == "CONST Let(a, \<lambda>x. e)"
+syntax_consts "_Let" \<rightleftharpoons> Let
lemma LetI:
assumes \<open>\<And>x. x = t \<Longrightarrow> P(u(x))\<close>
--- 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 =
--- 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 =
--- 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>\<open>\<rightleftharpoons>\<close> || \<^keyword>\<open>==\<close>)) --
+ Parse.!!! (Scan.repeat1 Parse.name_position));
+
+val _ =
+ Outer_Syntax.command \<^command_keyword>\<open>syntax_consts\<close> "declare syntax const dependencies"
+ (syntax_consts >> (Toplevel.theory o Isar_Cmd.syntax_consts));
+
+val _ =
+ Outer_Syntax.command \<^command_keyword>\<open>syntax_types\<close> "declare syntax const dependencies (type names)"
+ (syntax_consts >> (Toplevel.theory o Isar_Cmd.syntax_types));
+
val trans_pat =
Scan.optional
(\<^keyword>\<open>(\<close> |-- Parse.!!! (Parse.inner_syntax Parse.name --| \<^keyword>\<open>)\<close>)) "logic"
--- 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;
--- 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;
--- 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 " \<leadsto> " (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;
--- 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 ([], []);
--- 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;
--- 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 \<Rightarrow> prop", NoSyn),
(qualify (Binding.make ("sort_constraint", \<^here>)), typ "'a itself \<Rightarrow> prop", NoSyn),
--- 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) =
--- 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 \<open>Tools/numeral_syntax.ML\<close>
+syntax_consts
+ "_Int0" "_Int1" "_Int2" "_Int" "_Neg_Int1" "_Neg_Int2" "_Neg_Int" \<rightleftharpoons> integ_of
declare bin.intros [simp,TC]
--- 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] \<Rightarrow> i" (\<open>(1{# _ \<in> _./ _#})\<close>)
translations
"{#x \<in> M. P#}" == "CONST MCollect(M, \<lambda>x. P)"
+syntax_consts "_MColl" \<rightleftharpoons> MCollect
(* multiset orderings *)
--- 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 (\<open>[]\<close>)
"_List" :: "is \<Rightarrow> i" (\<open>[(_)]\<close>)
-
translations
"[x, xs]" == "CONST Cons(x, [xs])"
"[x]" == "CONST Cons(x, [])"
"[]" == "CONST Nil"
-
+syntax_consts "_List" \<rightleftharpoons> Cons
consts
length :: "i\<Rightarrow>i"
--- 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 @@
"\<forall>x<a. P" \<rightleftharpoons> "CONST oall(a, \<lambda>x. P)"
"\<exists>x<a. P" \<rightleftharpoons> "CONST oex(a, \<lambda>x. P)"
"\<Union>x<a. B" \<rightleftharpoons> "CONST OUnion(a, \<lambda>x. B)"
+syntax_consts
+ "_oall" \<rightleftharpoons> oall and
+ "_oex" \<rightleftharpoons> oex and
+ "_OUNION" \<rightleftharpoons> OUnion
subsubsection \<open>simplification of the new quantifiers\<close>
@@ -197,6 +201,9 @@
translations
"\<forall>x[M]. P" \<rightleftharpoons> "CONST rall(M, \<lambda>x. P)"
"\<exists>x[M]. P" \<rightleftharpoons> "CONST rex(M, \<lambda>x. P)"
+syntax_consts
+ "_rall" \<rightleftharpoons> rall and
+ "_rex" \<rightleftharpoons> rex
subsubsection\<open>Relativized universal quantifier\<close>
--- 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] \<Rightarrow> i" (\<open>(3QSUM _ \<in> _./ _)\<close> 10)
translations
"QSUM x \<in> A. B" => "CONST QSigma(A, \<lambda>x. B)"
+syntax_consts
+ "_QSUM" \<rightleftharpoons> QSigma
abbreviation
qprod (infixr \<open><*>\<close> 80) where
--- 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] \<Rightarrow> i" (\<open>(3\<Squnion>_./ _)\<close> 10)
"_JOIN" :: "[pttrn, i, i] \<Rightarrow> i" (\<open>(3\<Squnion>_ \<in> _./ _)\<close> 10)
-
translations
"\<Squnion>x \<in> A. B" == "CONST JOIN(A, (\<lambda>x. B))"
"\<Squnion>x y. B" == "\<Squnion>x. \<Squnion>y. B"
"\<Squnion>x. B" == "CONST JOIN(CONST state, (\<lambda>x. B))"
+syntax_consts
+ "_JOIN1" "_JOIN" == JOIN
subsection\<open>SKIP\<close>
--- 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
"\<forall>x\<in>A. P" \<rightleftharpoons> "CONST Ball(A, \<lambda>x. P)"
"\<exists>x\<in>A. P" \<rightleftharpoons> "CONST Bex(A, \<lambda>x. P)"
+syntax_consts
+ "_Ball" \<rightleftharpoons> Ball and
+ "_Bex" \<rightleftharpoons> Bex
subsection \<open>Variations on Replacement\<close>
@@ -52,9 +55,11 @@
where "Replace(A,P) \<equiv> PrimReplace(A, \<lambda>x y. (\<exists>!z. P(x,z)) \<and> P(x,y))"
syntax
- "_Replace" :: "[pttrn, pttrn, i, o] \<Rightarrow> i" (\<open>(1{_ ./ _ \<in> _, _})\<close>)
+ "_Replace" :: "[pttrn, pttrn, i, o] \<Rightarrow> i" (\<open>(1{_ ./ _ \<in> _, _})\<close>)
translations
"{y. x\<in>A, Q}" \<rightleftharpoons> "CONST Replace(A, \<lambda>x y. Q)"
+syntax_consts
+ "_Replace" \<rightleftharpoons> Replace
(* Functional form of replacement -- analgous to ML's map functional *)
@@ -66,7 +71,8 @@
"_RepFun" :: "[i, pttrn, i] \<Rightarrow> i" (\<open>(1{_ ./ _ \<in> _})\<close> [51,0,51])
translations
"{b. x\<in>A}" \<rightleftharpoons> "CONST RepFun(A, \<lambda>x. b)"
-
+syntax_consts
+ "_RepFun" \<rightleftharpoons> 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] \<Rightarrow> i" (\<open>(1{_ \<in> _ ./ _})\<close>)
translations
"{x\<in>A. P}" \<rightleftharpoons> "CONST Collect(A, \<lambda>x. P)"
+syntax_consts
+ "_Collect" \<rightleftharpoons> Collect
subsection \<open>General union and intersection\<close>
@@ -90,6 +98,9 @@
translations
"\<Union>x\<in>A. B" == "CONST Union({B. x\<in>A})"
"\<Inter>x\<in>A. B" == "CONST Inter({B. x\<in>A})"
+syntax_consts
+ "_UNION" == Union and
+ "_INTER" == Inter
subsection \<open>Finite sets and binary operations\<close>
@@ -126,6 +137,8 @@
translations
"{x, xs}" == "CONST cons(x, {xs})"
"{x}" == "CONST cons(x, 0)"
+syntax_consts
+ "_Finset" == cons
subsection \<open>Axioms\<close>
@@ -191,6 +204,9 @@
"\<langle>x, y\<rangle>" == "CONST Pair(x, y)"
"\<lambda>\<langle>x,y,zs\<rangle>.b" == "CONST split(\<lambda>x \<langle>y,zs\<rangle>.b)"
"\<lambda>\<langle>x,y\<rangle>.b" == "CONST split(\<lambda>x y. b)"
+syntax_consts
+ "_pattern" "_patterns" == split and
+ "_Tuple" == Pair
definition Sigma :: "[i, i \<Rightarrow> i] \<Rightarrow> i"
where "Sigma(A,B) \<equiv> \<Union>x\<in>A. \<Union>y\<in>B(x). {\<langle>x,y\<rangle>}"
@@ -256,6 +272,10 @@
"\<Prod>x\<in>A. B" == "CONST Pi(A, \<lambda>x. B)"
"\<Sum>x\<in>A. B" == "CONST Sigma(A, \<lambda>x. B)"
"\<lambda>x\<in>A. f" == "CONST Lambda(A, \<lambda>x. f)"
+syntax_consts
+ "_PROD" == Pi and
+ "_SUM" == Sigma and
+ "_lam" == Lambda
subsection \<open>ASCII syntax\<close>
--- 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] \<Rightarrow> updbind" (\<open>(2_ :=/ _)\<close>)
"" :: "updbind \<Rightarrow> updbinds" (\<open>_\<close>)
"_updbinds" :: "[updbind, updbinds] \<Rightarrow> updbinds" (\<open>_,/ _\<close>)
"_Update" :: "[i, updbinds] \<Rightarrow> i" (\<open>_/'((_)')\<close> [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" \<rightleftharpoons> update
lemma update_apply [simp]: "f(x:=y) ` z = (if z=x then y else f`z)"
apply (simp add: update_def)