# HG changeset patch # User wenzelm # Date 1727384641 -7200 # Node ID 980cc422526ecd7ca7cc24049b6178cee8bb10f7 # Parent 97924a26a5c3e80da3f7c17f9bf13239dc558363# Parent cf96b584724df6ff1fa0a2d9b1d13512c8f56db9 merged diff -r 97924a26a5c3 -r 980cc422526e src/HOL/Library/Datatype_Records.thy --- 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" (\_\) "_constify" :: "longid => ident" (\_\) - "_field_type" :: "ident => type => field_type" (\(2_ ::/ _)\) + "_field_type" :: "ident => type => field_type" (\(\indent=2 notation=\infix field type\\_ ::/ _)\) "" :: "field_type => field_types" (\_\) "_field_types" :: "field_type => field_types => field_types" (\_,/ _\) - "_record_type" :: "field_types => type" (\(3\_\)\) - "_record_type_scheme" :: "field_types => type => type" (\(3\_,/ (2\ ::/ _)\)\) + "_record_type" :: "field_types => type" (\(\indent=3 notation=\mixfix record type\\\_\)\) + "_record_type_scheme" :: "field_types => type => type" (\(\indent=3 notation=\mixfix record type\\\_,/ (2\ ::/ _)\)\) - "_field" :: "ident => 'a => field" (\(2_ =/ _)\) + "_field" :: "ident => 'a => field" (\(\indent=2 notation=\infix field value\\_ =/ _)\) "" :: "field => fields" (\_\) "_fields" :: "field => fields => fields" (\_,/ _\) - "_record" :: "fields => 'a" (\(3\_\)\) - "_record_scheme" :: "fields => 'a => 'a" (\(3\_,/ (2\ =/ _)\)\) + "_record" :: "fields => 'a" (\(\indent=3 notation=\mixfix record value\\\_\)\) + "_record_scheme" :: "fields => 'a => 'a" (\(\indent=3 notation=\mixfix record value\\\_,/ (2\ =/ _)\)\) - "_field_update" :: "ident => 'a => field_update" (\(2_ :=/ _)\) + "_field_update" :: "ident => 'a => field_update" (\(\indent=2 notation=\infix field update\\_ :=/ _)\) "" :: "field_update => field_updates" (\_\) "_field_updates" :: "field_update => field_updates => field_updates" (\_,/ _\) - "_record_update" :: "'a => field_updates => 'b" (\_/(3\_\)\ [900, 0] 900) + "_record_update" :: "'a => field_updates => 'b" (\_/(\indent=3 notation=\mixfix record update\\\_\)\ [900, 0] 900) no_syntax (ASCII) - "_record_type" :: "field_types => type" (\(3'(| _ |'))\) - "_record_type_scheme" :: "field_types => type => type" (\(3'(| _,/ (2... ::/ _) |'))\) - "_record" :: "fields => 'a" (\(3'(| _ |'))\) - "_record_scheme" :: "fields => 'a => 'a" (\(3'(| _,/ (2... =/ _) |'))\) - "_record_update" :: "'a => field_updates => 'b" (\_/(3'(| _ |'))\ [900, 0] 900) + "_record_type" :: "field_types => type" (\(\indent=3 notation=\mixfix record type\\'(| _ |'))\) + "_record_type_scheme" :: "field_types => type => type" (\(\indent=3 notation=\mixfix record type\\'(| _,/ (2... ::/ _) |'))\) + "_record" :: "fields => 'a" (\(\indent=3 notation=\mixfix record value\\'(| _ |'))\) + "_record_scheme" :: "fields => 'a => 'a" (\(\indent=3 notation=\mixfix record value\\'(| _,/ (2... =/ _) |'))\) + "_record_update" :: "'a => field_updates => 'b" (\_/(\indent=3 notation=\mixfix record update\\'(| _ |'))\ [900, 0] 900) (* copied and adapted from Record.thy *) diff -r 97924a26a5c3 -r 980cc422526e src/Pure/Syntax/lexicon.ML --- 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 [] diff -r 97924a26a5c3 -r 980cc422526e src/Pure/Syntax/parser.ML --- 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; diff -r 97924a26a5c3 -r 980cc422526e src/Pure/Syntax/printer.ML --- 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 *) diff -r 97924a26a5c3 -r 980cc422526e src/Pure/Syntax/syntax_phases.ML --- 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; diff -r 97924a26a5c3 -r 980cc422526e src/ZF/ZF_Base.thy --- 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 \ tuple_args" (\_\) "_Tuple_args" :: "[i, tuple_args] \ tuple_args" (\_,/ _\) - "_Tuple" :: "[i, tuple_args] \ i" (\\(_,/ _)\\) + "_Tuple" :: "[i, tuple_args] \ i" (\\(\notation=\mixfix tuple\\_,/ _)\\) syntax_consts "_Tuple_args" "_Tuple" == Pair translations