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;
--- 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 ***
--- 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 "\<dots>"} @{verbatim "''"} \\
@{syntax_def (inner) string_token} & = & @{verbatim "\""} @{text "\<dots>"} @{verbatim "\""} \\
@{syntax_def (inner) cartouche} & = & @{verbatim "\<open>"} @{text "\<dots>"} @{verbatim "\<close>"} \\
@@ -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.
*}
--- 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
*}
--- 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;
--- 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 "'\\<index>"),
--- 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" \<rightleftharpoons> "CONST integ_of(CONST Pls)"
+ "#1" \<rightleftharpoons> "CONST integ_of(CONST Pls BIT 1)"
+ "#2" \<rightleftharpoons> "CONST integ_of(CONST Pls BIT 1 BIT 0)"
+ "#-1" \<rightleftharpoons> "CONST integ_of(CONST Min)"
+ "#-2" \<rightleftharpoons> "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]
--- 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;