--- a/src/HOL/Library/Datatype_Records.thy Fri Aug 23 15:30:09 2024 +0200
+++ b/src/HOL/Library/Datatype_Records.thy Thu Sep 26 23:04:01 2024 +0200
@@ -30,29 +30,29 @@
"_constify" :: "id => ident" (\<open>_\<close>)
"_constify" :: "longid => ident" (\<open>_\<close>)
- "_field_type" :: "ident => type => field_type" (\<open>(2_ ::/ _)\<close>)
+ "_field_type" :: "ident => type => field_type" (\<open>(\<open>indent=2 notation=\<open>infix field type\<close>\<close>_ ::/ _)\<close>)
"" :: "field_type => field_types" (\<open>_\<close>)
"_field_types" :: "field_type => field_types => field_types" (\<open>_,/ _\<close>)
- "_record_type" :: "field_types => type" (\<open>(3\<lparr>_\<rparr>)\<close>)
- "_record_type_scheme" :: "field_types => type => type" (\<open>(3\<lparr>_,/ (2\<dots> ::/ _)\<rparr>)\<close>)
+ "_record_type" :: "field_types => type" (\<open>(\<open>indent=3 notation=\<open>mixfix record type\<close>\<close>\<lparr>_\<rparr>)\<close>)
+ "_record_type_scheme" :: "field_types => type => type" (\<open>(\<open>indent=3 notation=\<open>mixfix record type\<close>\<close>\<lparr>_,/ (2\<dots> ::/ _)\<rparr>)\<close>)
- "_field" :: "ident => 'a => field" (\<open>(2_ =/ _)\<close>)
+ "_field" :: "ident => 'a => field" (\<open>(\<open>indent=2 notation=\<open>infix field value\<close>\<close>_ =/ _)\<close>)
"" :: "field => fields" (\<open>_\<close>)
"_fields" :: "field => fields => fields" (\<open>_,/ _\<close>)
- "_record" :: "fields => 'a" (\<open>(3\<lparr>_\<rparr>)\<close>)
- "_record_scheme" :: "fields => 'a => 'a" (\<open>(3\<lparr>_,/ (2\<dots> =/ _)\<rparr>)\<close>)
+ "_record" :: "fields => 'a" (\<open>(\<open>indent=3 notation=\<open>mixfix record value\<close>\<close>\<lparr>_\<rparr>)\<close>)
+ "_record_scheme" :: "fields => 'a => 'a" (\<open>(\<open>indent=3 notation=\<open>mixfix record value\<close>\<close>\<lparr>_,/ (2\<dots> =/ _)\<rparr>)\<close>)
- "_field_update" :: "ident => 'a => field_update" (\<open>(2_ :=/ _)\<close>)
+ "_field_update" :: "ident => 'a => field_update" (\<open>(\<open>indent=2 notation=\<open>infix field update\<close>\<close>_ :=/ _)\<close>)
"" :: "field_update => field_updates" (\<open>_\<close>)
"_field_updates" :: "field_update => field_updates => field_updates" (\<open>_,/ _\<close>)
- "_record_update" :: "'a => field_updates => 'b" (\<open>_/(3\<lparr>_\<rparr>)\<close> [900, 0] 900)
+ "_record_update" :: "'a => field_updates => 'b" (\<open>_/(\<open>indent=3 notation=\<open>mixfix record update\<close>\<close>\<lparr>_\<rparr>)\<close> [900, 0] 900)
no_syntax (ASCII)
- "_record_type" :: "field_types => type" (\<open>(3'(| _ |'))\<close>)
- "_record_type_scheme" :: "field_types => type => type" (\<open>(3'(| _,/ (2... ::/ _) |'))\<close>)
- "_record" :: "fields => 'a" (\<open>(3'(| _ |'))\<close>)
- "_record_scheme" :: "fields => 'a => 'a" (\<open>(3'(| _,/ (2... =/ _) |'))\<close>)
- "_record_update" :: "'a => field_updates => 'b" (\<open>_/(3'(| _ |'))\<close> [900, 0] 900)
+ "_record_type" :: "field_types => type" (\<open>(\<open>indent=3 notation=\<open>mixfix record type\<close>\<close>'(| _ |'))\<close>)
+ "_record_type_scheme" :: "field_types => type => type" (\<open>(\<open>indent=3 notation=\<open>mixfix record type\<close>\<close>'(| _,/ (2... ::/ _) |'))\<close>)
+ "_record" :: "fields => 'a" (\<open>(\<open>indent=3 notation=\<open>mixfix record value\<close>\<close>'(| _ |'))\<close>)
+ "_record_scheme" :: "fields => 'a => 'a" (\<open>(\<open>indent=3 notation=\<open>mixfix record value\<close>\<close>'(| _,/ (2... =/ _) |'))\<close>)
+ "_record_update" :: "'a => field_updates => 'b" (\<open>_/(\<open>indent=3 notation=\<open>mixfix record update\<close>\<close>'(| _ |'))\<close> [900, 0] 900)
(* copied and adapted from Record.thy *)
--- a/src/Pure/Syntax/lexicon.ML Fri Aug 23 15:30:09 2024 +0200
+++ b/src/Pure/Syntax/lexicon.ML Thu Sep 26 23:04:01 2024 +0200
@@ -30,6 +30,7 @@
val end_pos_of_token: token -> Position.T
val is_proper: token -> bool
val dummy: token
+ val is_dummy: token -> bool
val literal: string -> token
val is_literal: token -> bool
val tokens_match_ord: token ord
@@ -40,8 +41,6 @@
val terminals: string list
val is_terminal: string -> bool
val get_terminal: string -> token option
- val suppress_literal_markup: string -> bool
- val suppress_markup: token -> bool
val literal_markup: string -> Markup.T list
val reports_of_token: token -> Position.report list
val reported_token_range: Proof.context -> token -> string
@@ -146,7 +145,9 @@
val is_proper = kind_of_token #> (fn Space => false | Comment _ => false | _ => true);
-val dummy = Token (token_kind_index Dummy, "", Position.no_range);
+val dummy_index = token_kind_index Dummy;
+val dummy = Token (dummy_index, "", Position.no_range);
+fun is_dummy tok = index_of_token tok = dummy_index;
(* literals *)
@@ -199,9 +200,6 @@
(* markup *)
-val suppress_literal_markup = Symbol.has_control_block o Symbol.explode;
-fun suppress_markup tok = is_literal tok andalso suppress_literal_markup (str_of_token tok);
-
fun literal_markup s =
let val syms = Symbol.explode s in
if Symbol.has_control_block syms then []
--- a/src/Pure/Syntax/parser.ML Fri Aug 23 15:30:09 2024 +0200
+++ b/src/Pure/Syntax/parser.ML Thu Sep 26 23:04:01 2024 +0200
@@ -14,8 +14,7 @@
datatype parsetree =
Node of string * parsetree list |
Tip of Lexicon.token
- exception PARSETREE of parsetree
- val pretty_parsetree: parsetree -> Pretty.T
+ val pretty_parsetree: parsetree -> Pretty.T list
val parse: gram -> string -> Lexicon.token list -> parsetree list
val branching_level: int Config.T
end;
@@ -32,6 +31,7 @@
type tags = nt Symtab.table;
val tags_empty: tags = Symtab.empty;
+fun tags_size (tags: tags) = Symtab.size tags;
fun tags_content (tags: tags) = sort_by #1 (Symtab.dest tags);
fun tags_lookup (tags: tags) = Symtab.lookup tags;
fun tags_insert tag (tags: tags) = Symtab.update_new tag tags;
@@ -88,9 +88,7 @@
datatype gram =
Gram of
- {nt_count: int,
- prod_count: int,
- tags: tags,
+ {tags: tags,
chains: chains,
lambdas: nts,
prods: nt_gram Vector.vector};
@@ -417,76 +415,75 @@
val empty_gram =
Gram
- {nt_count = 0,
- prod_count = 0,
- tags = tags_empty,
+ {tags = tags_empty,
chains = chains_empty,
lambdas = nts_empty,
prods = Vector.fromList [nt_gram_empty]};
-fun extend_gram xprods (Gram {nt_count, prod_count, tags, chains, lambdas, prods}) =
- let
- (*Get tag for existing nonterminal or create a new one*)
- fun get_tag nt_count tags nt =
- (case tags_lookup tags nt of
- SOME tag => (nt_count, tags, tag)
- | NONE => (nt_count + 1, tags_insert (nt, nt_count) tags, nt_count));
+local
+
+fun make_tag s tags =
+ (case tags_lookup tags s of
+ SOME tag => (tag, tags)
+ | NONE =>
+ let val tag = tags_size tags
+ in (tag, tags_insert (s, tag) tags) end);
- (*Convert symbols to the form used by the parser;
- delimiters and predefined terms are stored as terminals,
- nonterminals are converted to integer tags*)
- fun symb_of [] nt_count tags result = (nt_count, tags, rev result)
- | symb_of (Syntax_Ext.Delim s :: ss) nt_count tags result =
- symb_of ss nt_count tags (Terminal (Lexicon.literal s) :: result)
- | symb_of (Syntax_Ext.Argument (s, p) :: ss) nt_count tags result =
+fun make_arg (s, p) tags =
+ (case Lexicon.get_terminal s of
+ NONE =>
+ let val (tag, tags') = make_tag s tags;
+ in (Nonterminal (tag, p), tags') end
+ | SOME tok => (Terminal tok, tags));
+
+fun extend_gram xprods gram =
+ let
+ fun make_symbs (Syntax_Ext.Delim s :: xsyms) tags =
+ let val (syms, tags') = make_symbs xsyms tags
+ in (Terminal (Lexicon.literal s) :: syms, tags') end
+ | make_symbs (Syntax_Ext.Argument a :: xsyms) tags =
let
- val (nt_count', tags', new_symb) =
- (case Lexicon.get_terminal s of
- NONE =>
- let val (nt_count', tags', s_tag) = get_tag nt_count tags s;
- in (nt_count', tags', Nonterminal (s_tag, p)) end
- | SOME tk => (nt_count, tags, Terminal tk));
- in symb_of ss nt_count' tags' (new_symb :: result) end
- | symb_of (_ :: ss) nt_count tags result = symb_of ss nt_count tags result;
+ val (arg, tags') = make_arg a tags;
+ val (syms, tags'') = make_symbs xsyms tags';
+ in (arg :: syms, tags'') end
+ | make_symbs (_ :: xsyms) tags = make_symbs xsyms tags
+ | make_symbs [] tags = ([], tags);
- (*Convert list of productions by invoking symb_of for each of them*)
- fun prod_of [] nt_count prod_count tags result =
- (nt_count, prod_count, tags, result)
- | prod_of (Syntax_Ext.XProd (lhs, xsymbs, const, pri) :: ps)
- nt_count prod_count tags result =
- let
- val (nt_count', tags', lhs_tag) = get_tag nt_count tags lhs;
- val (nt_count'', tags'', prods) = symb_of xsymbs nt_count' tags' [];
- in
- prod_of ps nt_count'' (prod_count + 1) tags''
- ((lhs_tag, (prods, const, pri)) :: result)
- end;
+ fun make_prod (Syntax_Ext.XProd (lhs, xsymbs, const, pri)) (result, tags) =
+ let
+ val (tag, tags') = make_tag lhs tags;
+ val (symbs, tags'') = make_symbs xsymbs tags';
+ in ((tag, (symbs, const, pri)) :: result, tags'') end;
- val (nt_count', prod_count', tags', xprods') =
- prod_of xprods nt_count prod_count tags [];
+
+ val Gram {tags, chains, lambdas, prods} = gram;
+
+ val (new_prods, tags') = fold make_prod xprods ([], tags);
val array_prods' =
- Array.tabulate (nt_count', fn i =>
- if i < nt_count then Vector.nth prods i
+ Array.tabulate (tags_size tags', fn i =>
+ if i < Vector.length prods then Vector.nth prods i
else nt_gram_empty);
val (chains', lambdas') =
- (chains, lambdas) |> fold (add_production array_prods') xprods';
+ (chains, lambdas) |> fold (add_production array_prods') new_prods;
in
Gram
- {nt_count = nt_count',
- prod_count = prod_count',
- tags = tags',
+ {tags = tags',
chains = chains',
lambdas = lambdas',
prods = Array.vector array_prods'}
end;
+in
+
fun make_gram [] _ (SOME gram) = gram
| make_gram new_xprods _ (SOME gram) = extend_gram new_xprods gram
| make_gram [] [] NONE = empty_gram
| make_gram new_xprods old_xprods NONE = extend_gram (new_xprods @ old_xprods) empty_gram;
+end;
+
(** parser **)
@@ -497,15 +494,11 @@
Node of string * parsetree list |
Tip of Lexicon.token;
-exception PARSETREE of parsetree;
-
-fun pretty_parsetree parsetree =
- let
- fun pretty (Node (c, pts)) =
- [Pretty.enclose "(" ")" (Pretty.breaks (Pretty.quote (Pretty.str c) :: maps pretty pts))]
- | pretty (Tip tok) =
- if Lexicon.valued_token tok then [Pretty.str (Lexicon.str_of_token tok)] else [];
- in (case pretty parsetree of [prt] => prt | _ => raise PARSETREE parsetree) end;
+fun pretty_parsetree (Node (c, pts)) =
+ [Pretty.enclose "(" ")"
+ (Pretty.breaks (Pretty.quote (Pretty.str c) :: maps pretty_parsetree pts))]
+ | pretty_parsetree (Tip tok) =
+ if Lexicon.valued_token tok then [Pretty.str (Lexicon.str_of_token tok)] else [];
(* parser state *)
@@ -562,9 +555,6 @@
fun movedot_nonterm tt (info, Nonterminal _ :: sa, ts) : state = (info, sa, tt @ ts);
-fun movedot_lambda p ((info, sa, ts): state) =
- map_filter (fn (t, k) => if p <= k then SOME (info, sa, t @ ts) else NONE);
-
(*trigger value for warnings*)
val branching_level = Config.declare_int ("syntax_branching_level", \<^here>) (K 600);
@@ -626,16 +616,21 @@
else (used, get_states A prec (Array.nth stateset j));
val States' = map (movedot_nonterm tt) Slist;
in process used' (States' @ States) (S :: Si, Sii) end)
- in process Inttab.empty states ([], []) end;
-fun produce gram stateset i input prev_token =
+ val (Si, Sii) = process Inttab.empty states ([], []);
+ in
+ Array.upd stateset i Si;
+ Array.upd stateset (i + 1) Sii
+ end;
+
+fun produce gram stateset i prev rest =
(case Array.nth stateset i of
[] =>
let
- val toks = if Lexicon.is_eof prev_token then input else prev_token :: input;
- val pos = Position.here (Lexicon.pos_of_token prev_token);
+ val inp = if Lexicon.is_dummy prev then rest else prev :: rest;
+ val pos = Position.here (Lexicon.pos_of_token prev);
in
- if null toks then
+ if null inp then
error ("Inner syntax error: unexpected end of input" ^ pos)
else
error ("Inner syntax error" ^ pos ^
@@ -645,18 +640,13 @@
Pretty.str "at", Pretty.brk 1,
Pretty.block
(Pretty.str "\"" ::
- Pretty.breaks (map (Pretty.str o Lexicon.str_of_token) (#1 (split_last toks))) @
+ Pretty.breaks (map (Pretty.str o Lexicon.str_of_token) (#1 (split_last inp))) @
[Pretty.str "\""])])))
end
| states =>
- (case input of
+ (case rest of
[] => states
- | c :: rest =>
- let
- val (Si, Sii) = process_states gram stateset i c states;
- val _ = Array.upd stateset i Si;
- val _ = Array.upd stateset (i + 1) Sii;
- in produce gram stateset (i + 1) rest c end));
+ | c :: cs => (process_states gram stateset i c states; produce gram stateset (i + 1) c cs)));
in
@@ -678,7 +668,7 @@
val _ = Array.upd stateset 0 [S0];
val pts =
- produce gram stateset 0 input Lexicon.eof
+ produce gram stateset 0 Lexicon.dummy input
|> map_filter (fn (_, _, [pt]) => SOME pt | _ => NONE);
in if null pts then raise Fail "Inner syntax: no parse trees" else pts end;
--- a/src/Pure/Syntax/printer.ML Fri Aug 23 15:30:09 2024 +0200
+++ b/src/Pure/Syntax/printer.ML Thu Sep 26 23:04:01 2024 +0200
@@ -68,7 +68,7 @@
datatype symb =
Arg of int |
TypArg of int |
- String of bool * string |
+ String of Markup.T list * string |
Break of int |
Block of Syntax_Ext.block * symb list;
@@ -131,41 +131,37 @@
(* xprod_to_fmt *)
+fun make_string s = String ([], s);
+fun make_literal s = String (Lexicon.literal_markup s, s);
+
+fun make_arg (s, p) =
+ (if s = "type" then TypArg else Arg)
+ (if Lexicon.is_terminal s then 1000 else p);
+
fun xprod_to_fmt (Syntax_Ext.XProd (_, _, "", _)) = NONE
| xprod_to_fmt (Syntax_Ext.XProd (_, xsymbs, const, pri)) =
let
- fun arg (s, p) =
- (if s = "type" then TypArg else Arg)
- (if Lexicon.is_terminal s then 1000 else p);
-
- fun xsyms_to_syms (Syntax_Ext.Delim s :: xsyms) =
- apfst (cons (String (not (Lexicon.suppress_literal_markup s), s)))
- (xsyms_to_syms xsyms)
- | xsyms_to_syms (Syntax_Ext.Argument s_p :: xsyms) =
- apfst (cons (arg s_p)) (xsyms_to_syms xsyms)
- | xsyms_to_syms (Syntax_Ext.Space s :: xsyms) =
- apfst (cons (String (false, s))) (xsyms_to_syms xsyms)
- | xsyms_to_syms (Syntax_Ext.Bg block :: xsyms) =
+ fun make_symbs (Syntax_Ext.Delim s :: xsyms) = make_symbs xsyms |>> cons (make_literal s)
+ | make_symbs (Syntax_Ext.Argument a :: xsyms) = make_symbs xsyms |>> cons (make_arg a)
+ | make_symbs (Syntax_Ext.Space s :: xsyms) = make_symbs xsyms |>> cons (make_string s)
+ | make_symbs (Syntax_Ext.Bg block :: xsyms) =
let
- val (bsyms, xsyms') = xsyms_to_syms xsyms;
- val (syms, xsyms'') = xsyms_to_syms xsyms';
- in
- (Block (block, bsyms) :: syms, xsyms'')
- end
- | xsyms_to_syms (Syntax_Ext.Brk i :: xsyms) =
- apfst (cons (Break i)) (xsyms_to_syms xsyms)
- | xsyms_to_syms (Syntax_Ext.En :: xsyms) = ([], xsyms)
- | xsyms_to_syms [] = ([], []);
+ val (bsyms, xsyms') = make_symbs xsyms;
+ val (syms, xsyms'') = make_symbs xsyms';
+ in (Block (block, bsyms) :: syms, xsyms'') end
+ | make_symbs (Syntax_Ext.Brk i :: xsyms) = make_symbs xsyms |>> cons (Break i)
+ | make_symbs (Syntax_Ext.En :: xsyms) = ([], xsyms)
+ | make_symbs [] = ([], []);
- fun nargs (Arg _ :: syms) = nargs syms + 1
- | nargs (TypArg _ :: syms) = nargs syms + 1
- | nargs (String _ :: syms) = nargs syms
- | nargs (Break _ :: syms) = nargs syms
- | nargs (Block (_, bsyms) :: syms) = nargs syms + nargs bsyms
- | nargs [] = 0;
+ fun count_args (Arg _ :: syms) = Integer.add 1 #> count_args syms
+ | count_args (TypArg _ :: syms) = Integer.add 1 #> count_args syms
+ | count_args (String _ :: syms) = count_args syms
+ | count_args (Break _ :: syms) = count_args syms
+ | count_args (Block (_, bsyms) :: syms) = count_args syms #> count_args bsyms
+ | count_args [] = I;
in
- (case xsyms_to_syms xsymbs of
- (symbs, []) => SOME (const, (symbs, nargs symbs, pri))
+ (case make_symbs xsymbs of
+ (symbs, []) => SOME (const, (symbs, count_args symbs 0, pri))
| _ => raise Fail "Unbalanced pretty-printing blocks")
end;
@@ -207,6 +203,14 @@
val pretty_curried = Config.declare_bool ("Syntax.pretty_curried", \<^here>) (K false);
val pretty_priority = Config.declare_int ("Syntax.pretty_priority", \<^here>) (K 0);
+local
+
+val par_block = Syntax_Ext.block_indent 1;
+val par_bg = make_literal "(";
+val par_en = make_literal ")";
+
+in
+
fun pretty ctxt tabs trf markup_trans markup_extern ast0 =
let
val type_mode = Config.get ctxt pretty_type_mode;
@@ -234,13 +238,10 @@
|> 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) =
+ | synT m (String (literal_markup, s) :: symbs, args) =
let
val (Ts, args') = synT m (symbs, args);
- val T =
- if do_mark
- then Pretty.marks_str (m @ Lexicon.literal_markup s, s)
- else Pretty.str s;
+ val T = Pretty.marks_str (if null literal_markup then [] else m @ literal_markup, s);
in (T :: Ts, args') end
| synT m (Block ({markup, consistent, unbreakable, indent}, bsymbs) :: symbs, args) =
let
@@ -256,10 +257,9 @@
val T = if i < 0 then Pretty.fbrk else Pretty.brk i;
in (T :: Ts, args') end
- and parT m (pr, args, p, p': int) = #1 (synT m
- (if p > p' orelse (show_brackets andalso p' <> 1000 andalso not (is_chain pr)) then
- [Block (Syntax_Ext.block_indent 1, String (false, "(") :: pr @ [String (false, ")")])]
- else pr, args))
+ 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)
@@ -295,6 +295,8 @@
| astT (ast as Ast.Appl _, _) = raise Ast.AST ("pretty: malformed ast", [ast]);
in astT (ast0, Config.get ctxt pretty_priority) end;
+end;
+
(* pretty_term_ast *)
--- a/src/Pure/Syntax/syntax_phases.ML Fri Aug 23 15:30:09 2024 +0200
+++ b/src/Pure/Syntax/syntax_phases.ML Thu Sep 26 23:04:01 2024 +0200
@@ -158,8 +158,8 @@
val append_reports = Position.append_reports reports;
fun report_pos tok =
- if Lexicon.suppress_markup tok then Position.none
- else Lexicon.pos_of_token tok;
+ if Lexicon.is_literal tok andalso null (Lexicon.literal_markup (Lexicon.str_of_token tok))
+ then Position.none else Lexicon.pos_of_token tok;
fun trans a args =
(case trf a of
@@ -358,8 +358,7 @@
(("Ambiguous input" ^ Position.here (Position.no_range_position pos) ^
" produces " ^ string_of_int len ^ " parse trees" ^
(if len <= limit then "" else " (" ^ string_of_int limit ^ " displayed)") ^ ":") ::
- map (Pretty.string_of o Pretty.item o single o Parser.pretty_parsetree)
- (take limit pts))];
+ map (Pretty.string_of o Pretty.item o Parser.pretty_parsetree) (take limit pts))];
in (ambig_msgs, map (parsetree_to_ast ctxt ast_tr) pts) end;
--- a/src/ZF/ZF_Base.thy Fri Aug 23 15:30:09 2024 +0200
+++ b/src/ZF/ZF_Base.thy Thu Sep 26 23:04:01 2024 +0200
@@ -196,7 +196,7 @@
syntax
"" :: "i \<Rightarrow> tuple_args" (\<open>_\<close>)
"_Tuple_args" :: "[i, tuple_args] \<Rightarrow> tuple_args" (\<open>_,/ _\<close>)
- "_Tuple" :: "[i, tuple_args] \<Rightarrow> i" (\<open>\<langle>(_,/ _)\<rangle>\<close>)
+ "_Tuple" :: "[i, tuple_args] \<Rightarrow> i" (\<open>\<langle>(\<open>notation=\<open>mixfix tuple\<close>\<close>_,/ _)\<rangle>\<close>)
syntax_consts
"_Tuple_args" "_Tuple" == Pair
translations