# HG changeset patch # User wenzelm # Date 1411414137 -7200 # Node ID 37cbbd8eb4603246a84cdd9f64bb5a14ac68731e # Parent 00bf84d3f5268f04e50f3629bcac721113192e3f discontinued old "xnum" token category; simplified Lexicon.read_num, Lexicon.read_float: no sign here; express ZF numerals via "num" with mixfix grammar; recovered printing of ZF numerals: "one" is abbreviation; diff -r 00bf84d3f526 -r 37cbbd8eb460 NEWS --- a/NEWS Mon Sep 22 17:07:18 2014 +0200 +++ b/NEWS Mon Sep 22 21:28:57 2014 +0200 @@ -25,6 +25,10 @@ of numeral signs, particulary in expressions involving infix syntax like "(- 1) ^ n". +* Old inner token category "xnum" has been discontinued. Potential +INCOMPATIBILITY for exotic syntax: may use mixfix grammar with "num" +token category instead. + *** HOL *** diff -r 00bf84d3f526 -r 37cbbd8eb460 src/Doc/Isar_Ref/Inner_Syntax.thy --- a/src/Doc/Isar_Ref/Inner_Syntax.thy Mon Sep 22 17:07:18 2014 +0200 +++ b/src/Doc/Isar_Ref/Inner_Syntax.thy Mon Sep 22 21:28:57 2014 +0200 @@ -601,7 +601,6 @@ @{syntax_def (inner) tvar} & = & @{syntax_ref typevar} \\ @{syntax_def (inner) num_token} & = & @{syntax_ref nat} \\ @{syntax_def (inner) float_token} & = & @{syntax_ref nat}@{verbatim "."}@{syntax_ref nat} \\ - @{syntax_def (inner) xnum_token} & = & @{verbatim "#"}@{syntax_ref nat}@{text " | "}@{verbatim "#-"}@{syntax_ref nat} \\ @{syntax_def (inner) str_token} & = & @{verbatim "''"} @{text "\"} @{verbatim "''"} \\ @{syntax_def (inner) string_token} & = & @{verbatim "\""} @{text "\"} @{verbatim "\""} \\ @{syntax_def (inner) cartouche} & = & @{verbatim "\"} @{text "\"} @{verbatim "\"} \\ @@ -609,17 +608,15 @@ \end{center} The token categories @{syntax (inner) num_token}, @{syntax (inner) - float_token}, @{syntax (inner) xnum_token}, @{syntax (inner) - str_token}, @{syntax (inner) string_token}, and @{syntax (inner) - cartouche} are not used in Pure. Object-logics may implement - numerals and string literals by adding appropriate syntax - declarations, together with some translation functions (e.g.\ see - @{file "~~/src/HOL/Tools/string_syntax.ML"}). + float_token}, @{syntax (inner) str_token}, @{syntax (inner) string_token}, + and @{syntax (inner) cartouche} are not used in Pure. Object-logics may + implement numerals and string literals by adding appropriate syntax + declarations, together with some translation functions (e.g.\ see @{file + "~~/src/HOL/Tools/string_syntax.ML"}). - The derived categories @{syntax_def (inner) num_const}, @{syntax_def - (inner) float_const}, and @{syntax_def (inner) xnum_const} provide - robust access to the respective tokens: the syntax tree holds a - syntactic constant instead of a free variable. + The derived categories @{syntax_def (inner) num_const}, and @{syntax_def + (inner) float_const}, provide robust access to the respective tokens: the + syntax tree holds a syntactic constant instead of a free variable. *} diff -r 00bf84d3f526 -r 37cbbd8eb460 src/HOL/Num.thy --- a/src/HOL/Num.thy Mon Sep 22 17:07:18 2014 +0200 +++ b/src/HOL/Num.thy Mon Sep 22 21:28:57 2014 +0200 @@ -287,7 +287,7 @@ fun numeral_tr [(c as Const (@{syntax_const "_constrain"}, _)) $ t $ u] = c $ numeral_tr [t] $ u | numeral_tr [Const (num, _)] = - (Numeral.mk_number_syntax o #value o Lexicon.read_xnum) num + (Numeral.mk_number_syntax o #value o Lexicon.read_num) num | numeral_tr ts = raise TERM ("numeral_tr", ts); in [(@{syntax_const "_Numeral"}, K numeral_tr)] end *} diff -r 00bf84d3f526 -r 37cbbd8eb460 src/Pure/Syntax/lexicon.ML --- a/src/Pure/Syntax/lexicon.ML Mon Sep 22 17:07:18 2014 +0200 +++ b/src/Pure/Syntax/lexicon.ML Mon Sep 22 21:28:57 2014 +0200 @@ -16,7 +16,6 @@ val scan_longid: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list val scan_tid: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list val scan_nat: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list - val scan_int: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list val scan_float: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list val scan_hex: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list val scan_bin: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list @@ -25,7 +24,7 @@ val is_tid: string -> bool datatype token_kind = Literal | IdentSy | LongIdentSy | VarSy | TFreeSy | TVarSy | NumSy | - FloatSy | XNumSy | StrSy | StringSy | Cartouche | Space | Comment | EOF + FloatSy | StrSy | StringSy | Cartouche | Space | Comment | EOF datatype token = Token of token_kind * string * Position.range val str_of_token: token -> string val pos_of_token: token -> Position.T @@ -52,7 +51,7 @@ val read_variable: string -> indexname option val read_nat: string -> int option val read_int: string -> int option - val read_xnum: string -> {radix: int, leading_zeros: int, value: int} + val read_num: string -> {radix: int, leading_zeros: int, value: int} val read_float: string -> {mant: int, exp: int} val mark_class: string -> string val unmark_class: string -> string val mark_type: string -> string val unmark_type: string -> string @@ -99,9 +98,9 @@ val scan_nat = Scan.many1 (Symbol.is_digit o Symbol_Pos.symbol); val scan_float = scan_nat @@@ $$$ "." @@@ scan_nat; -val scan_int = $$$ "-" @@@ scan_nat || scan_nat; val scan_hex = $$$ "0" @@@ $$$ "x" @@@ Scan.many1 (Symbol.is_ascii_hex o Symbol_Pos.symbol); val scan_bin = $$$ "0" @@@ $$$ "b" @@@ Scan.many1 (fn (s, _) => s = "0" orelse s = "1"); +val scan_num = scan_hex || scan_bin || scan_nat; val scan_id_nat = scan_id @@@ Scan.optional ($$$ "." @@@ scan_nat) []; val scan_var = $$$ "?" @@@ scan_id_nat; @@ -118,7 +117,7 @@ datatype token_kind = Literal | IdentSy | LongIdentSy | VarSy | TFreeSy | TVarSy | NumSy | - FloatSy | XNumSy | StrSy | StringSy | Cartouche | Space | Comment | EOF; + FloatSy | StrSy | StringSy | Cartouche | Space | Comment | EOF; datatype token = Token of token_kind * string * Position.range; @@ -151,7 +150,6 @@ ("tvar", TVarSy), ("num_token", NumSy), ("float_token", FloatSy), - ("xnum_token", XNumSy), ("str_token", StrSy), ("string_token", StringSy), ("cartouche", Cartouche)]; @@ -172,7 +170,6 @@ | TVarSy => Markup.tvar | NumSy => Markup.numeral | FloatSy => Markup.numeral - | XNumSy => Markup.numeral | StrSy => Markup.inner_string | StringSy => Markup.inner_string | Cartouche => Markup.inner_cartouche @@ -263,16 +260,12 @@ (if xids then $$$ "_" @@@ scan_id || scan_id else scan_id) || $$$ "_" @@@ $$$ "_"; - val scan_num_unsigned = scan_hex || scan_bin || scan_nat; - val scan_num_signed = scan_hex || scan_bin || scan_int; - val scan_val = scan_tvar >> token TVarSy || scan_var >> token VarSy || scan_tid >> token TFreeSy || scan_float >> token FloatSy || - scan_num_unsigned >> token NumSy || - $$$ "#" @@@ scan_num_signed >> token XNumSy || + scan_num >> token NumSy || scan_longid >> token LongIdentSy || scan_xid >> token IdentSy; @@ -378,7 +371,7 @@ end; -(* read_xnum: hex/bin/decimal *) +(* read_num: hex/bin/decimal *) local @@ -400,34 +393,30 @@ in -fun read_xnum str = +fun read_num str = let - val (sign, radix, digs) = - (case Symbol.explode (perhaps (try (unprefix "#")) str) of - "0" :: "x" :: cs => (1, 16, map remap_hex cs) - | "0" :: "b" :: cs => (1, 2, cs) - | "-" :: cs => (~1, 10, cs) - | cs => (1, 10, cs)); + val (radix, digs) = + (case Symbol.explode str of + "0" :: "x" :: cs => (16, map remap_hex cs) + | "0" :: "b" :: cs => (2, cs) + | cs => (10, cs)); in {radix = radix, leading_zeros = leading_zeros digs, - value = sign * #1 (Library.read_radix_int radix digs)} + value = #1 (Library.read_radix_int radix digs)} end; end; fun read_float str = let - val (sign, cs) = - (case Symbol.explode str of - "-" :: cs => (~1, cs) - | cs => (1, cs)); + val cs = Symbol.explode str; val (intpart, fracpart) = (case take_prefix Symbol.is_digit cs of (intpart, "." :: fracpart) => (intpart, fracpart) | _ => raise Fail "read_float"); in - {mant = sign * #1 (Library.read_int (intpart @ fracpart)), + {mant = #1 (Library.read_int (intpart @ fracpart)), exp = length fracpart} end; diff -r 00bf84d3f526 -r 37cbbd8eb460 src/Pure/pure_thy.ML --- a/src/Pure/pure_thy.ML Mon Sep 22 17:07:18 2014 +0200 +++ b/src/Pure/pure_thy.ML Mon Sep 22 21:28:57 2014 +0200 @@ -70,8 +70,8 @@ (map (fn name => Binding.make (name, @{here})) (Lexicon.terminals @ ["logic", "type", "types", "sort", "classes", "args", "cargs", "pttrn", "pttrns", "idt", "idts", "aprop", "asms", - "any", "prop'", "num_const", "float_const", "xnum_const", "num_position", - "float_position", "xnum_position", "index", "struct", "tid_position", + "any", "prop'", "num_const", "float_const", "num_position", + "float_position", "index", "struct", "tid_position", "tvar_position", "id_position", "longid_position", "var_position", "str_position", "string_position", "cartouche_position", "type_name", "class_name"])) @@ -142,10 +142,8 @@ ("_strip_positions", typ "'a", NoSyn), ("_position", typ "num_token => num_position", Delimfix "_"), ("_position", typ "float_token => float_position", Delimfix "_"), - ("_position", typ "xnum_token => xnum_position", Delimfix "_"), ("_constify", typ "num_position => num_const", Delimfix "_"), ("_constify", typ "float_position => float_const", Delimfix "_"), - ("_constify", typ "xnum_position => xnum_const", Delimfix "_"), ("_index", typ "logic => index", Delimfix "(00\\<^bsub>_\\<^esub>)"), ("_indexdefault", typ "index", Delimfix ""), ("_indexvar", typ "index", Delimfix "'\\"), diff -r 00bf84d3f526 -r 37cbbd8eb460 src/ZF/Bin.thy --- a/src/ZF/Bin.thy Mon Sep 22 17:07:18 2014 +0200 +++ b/src/ZF/Bin.thy Mon Sep 22 21:28:57 2014 +0200 @@ -101,10 +101,23 @@ NCons(bin_mult(v,w),0))" syntax - "_Int" :: "xnum_token => i" ("_") + "_Int0" :: i ("#()0") + "_Int1" :: i ("#()1") + "_Int2" :: i ("#()2") + "_Neg_Int1" :: i ("#-()1") + "_Neg_Int2" :: i ("#-()2") +translations + "#0" \ "CONST integ_of(CONST Pls)" + "#1" \ "CONST integ_of(CONST Pls BIT 1)" + "#2" \ "CONST integ_of(CONST Pls BIT 1 BIT 0)" + "#-1" \ "CONST integ_of(CONST Min)" + "#-2" \ "CONST integ_of(CONST Min BIT 0)" + +syntax + "_Int" :: "num_token => i" ("#_" 1000) + "_Neg_Int" :: "num_token => i" ("#-_" 1000) ML_file "Tools/numeral_syntax.ML" -setup Numeral_Syntax.setup declare bin.intros [simp,TC] diff -r 00bf84d3f526 -r 37cbbd8eb460 src/ZF/Tools/numeral_syntax.ML --- a/src/ZF/Tools/numeral_syntax.ML Mon Sep 22 17:07:18 2014 +0200 +++ b/src/ZF/Tools/numeral_syntax.ML Mon Sep 22 21:28:57 2014 +0200 @@ -8,7 +8,6 @@ sig val make_binary: int -> int list val dest_binary: int list -> int - val setup: theory -> theory end; structure Numeral_Syntax: NUMERAL_SYNTAX = @@ -21,6 +20,7 @@ | mk_bit _ = raise Fail "mk_bit"; fun dest_bit (Const (@{const_syntax zero}, _)) = 0 + | dest_bit (Const (@{const_syntax one}, _)) = 1 | dest_bit (Const (@{const_syntax succ}, _) $ Const (@{const_syntax zero}, _)) = 1 | dest_bit _ = raise Match; @@ -58,28 +58,34 @@ fun show_int t = let val rev_digs = bin_of t; - val (sign, zs) = + val (c, zs) = (case rev rev_digs of - ~1 :: bs => ("-", prefix_len (equal 1) bs) - | bs => ("", prefix_len (equal 0) bs)); + ~1 :: bs => (@{syntax_const "_Neg_Int"}, prefix_len (equal 1) bs) + | bs => (@{syntax_const "_Int"}, prefix_len (equal 0) bs)); val num = string_of_int (abs (dest_binary rev_digs)); - in - "#" ^ sign ^ implode (replicate zs "0") ^ num - end; + in (c, implode (replicate zs "0") ^ num) end; (* translation of integer constant tokens to and from binary *) -fun int_tr [t as Free (str, _)] = - Syntax.const @{const_syntax integ_of} $ mk_bin (#value (Lexicon.read_xnum str)) +fun int_tr [Free (s, _)] = + Syntax.const @{const_syntax integ_of} $ mk_bin (#value (Lexicon.read_num s)) | int_tr ts = raise TERM ("int_tr", ts); -fun int_tr' [t] = Syntax.const @{syntax_const "_Int"} $ Syntax.free (show_int t) - | int_tr' _ = raise Match; - +fun neg_int_tr [Free (s, _)] = + Syntax.const @{const_syntax integ_of} $ mk_bin (~ (#value (Lexicon.read_num s))) + | neg_int_tr ts = raise TERM ("neg_int_tr", ts); -val setup = - Sign.parse_translation [(@{syntax_const "_Int"}, K int_tr)] #> - Sign.print_translation [(@{const_syntax integ_of}, K int_tr')]; +fun integ_of_tr' [t] = + let val (c, s) = show_int t + in Syntax.const c $ Syntax.free s end + | integ_of_tr' _ = raise Match; + +val _ = Theory.setup + (Sign.parse_translation + [(@{syntax_const "_Int"}, K int_tr), + (@{syntax_const "_Neg_Int"}, K neg_int_tr)] #> + Sign.print_translation + [(@{const_syntax integ_of}, K integ_of_tr')]); end;