# HG changeset patch
# User kleing
# Date 1152571434 -7200
# Node ID 26bac504ef90b8a955a2a8fcb4031bd41c4f2930
# Parent  b045b835cb3be1c69310c1b6e336d15a97e97354
hex and binary numerals (contributed by Rafal Kolanski)

diff -r b045b835cb3b -r 26bac504ef90 CONTRIBUTORS
--- a/CONTRIBUTORS	Mon Jul 10 21:02:29 2006 +0200
+++ b/CONTRIBUTORS	Tue Jul 11 00:43:54 2006 +0200
@@ -1,6 +1,9 @@
 Contributions to Isabelle
 -------------------------
 
+* July 2006: Rafal Kolanski, NICTA
+  Hex (0xFF) and binary (0b1011) numerals.
+
 * May 2006: Klaus Aehlig, LMU
   Command 'normal_form': normalization by evaluation.
 
diff -r b045b835cb3b -r 26bac504ef90 NEWS
--- a/NEWS	Mon Jul 10 21:02:29 2006 +0200
+++ b/NEWS	Tue Jul 11 00:43:54 2006 +0200
@@ -488,6 +488,7 @@
   (i.e. a boolean expression) by compiling it to ML. The goal is
   "proved" (via the oracle "Evaluation") if it evaluates to True.
 
+* Support for hex (0x20) and binary (0b1001) numerals. 
 
 *** HOL-Complex ***
 
diff -r b045b835cb3b -r 26bac504ef90 src/HOL/Tools/numeral_syntax.ML
--- a/src/HOL/Tools/numeral_syntax.ML	Mon Jul 10 21:02:29 2006 +0200
+++ b/src/HOL/Tools/numeral_syntax.ML	Tue Jul 11 00:43:54 2006 +0200
@@ -1,6 +1,6 @@
 (*  Title:      HOL/Tools/numeral_syntax.ML
     ID:         $Id$
-    Author:     Markus Wenzel, TU Muenchen
+    Authors:    Markus Wenzel, TU Muenchen
 
 Concrete syntax for generic numerals.  Assumes consts and syntax of
 theory HOL/Numeral.
@@ -37,8 +37,34 @@
 
 (* translation of integer numeral tokens to and from bitstrings *)
 
+(*additional translations of binary and hex numbers to normal numbers*)
+local
+
+(*get A => ord"0" + 10, etc*)
+fun remap_hex c =
+  let 
+    val zero = ord"0"; 
+    val a  = ord"a";
+    val ca = ord"A";
+    val x  = ord c;
+  in
+    if x >= a then chr (x - a + zero + 10)
+    else if x >= ca then chr (x - ca + zero + 10) 
+    else c
+  end;
+
+fun str_to_int' ("0" :: "x" :: ds) = read_radixint (16, map remap_hex ds) |> #1
+  | str_to_int' ("0" :: "b" :: ds) = read_radixint (2, ds) |> #1
+  | str_to_int' ds = implode ds |> IntInf.fromString |> valOf; 
+
+in
+
+val str_to_int = str_to_int' o explode;
+
+end;
+
 fun numeral_tr (*"_Numeral"*) [t as Const (str, _)] =
-      (Syntax.const "Numeral.number_of" $ (HOLogic.mk_binum (valOf (IntInf.fromString str))))
+      (Syntax.const "Numeral.number_of" $ (HOLogic.mk_binum (str_to_int str)))
   | numeral_tr (*"_Numeral"*) ts = raise TERM ("numeral_tr", ts);
 
 fun numeral_tr' show_sorts (*"number_of"*) (Type ("fun", [_, T])) (t :: ts) =
diff -r b045b835cb3b -r 26bac504ef90 src/Pure/General/symbol.ML
--- a/src/Pure/General/symbol.ML	Mon Jul 10 21:02:29 2006 +0200
+++ b/src/Pure/General/symbol.ML	Tue Jul 11 00:43:54 2006 +0200
@@ -23,6 +23,7 @@
   val malformed: symbol
   val is_ascii: symbol -> bool
   val is_ascii_letter: symbol -> bool
+  val is_hex_letter: symbol -> bool
   val is_ascii_digit: symbol -> bool
   val is_ascii_quasi: symbol -> bool
   val is_ascii_blank: symbol -> bool
@@ -125,6 +126,11 @@
    (ord "A" <= ord s andalso ord s <= ord "Z" orelse
     ord "a" <= ord s andalso ord s <= ord "z");
 
+fun is_hex_letter s =
+  is_char s andalso
+   (ord "A" <= ord s andalso ord s <= ord "F" orelse
+    ord "a" <= ord s andalso ord s <= ord "f");
+
 fun is_ascii_digit s =
   is_char s andalso ord "0" <= ord s andalso ord s <= ord "9";
 
diff -r b045b835cb3b -r 26bac504ef90 src/Pure/Syntax/lexicon.ML
--- a/src/Pure/Syntax/lexicon.ML	Mon Jul 10 21:02:29 2006 +0200
+++ b/src/Pure/Syntax/lexicon.ML	Tue Jul 11 00:43:54 2006 +0200
@@ -18,6 +18,8 @@
   val scan_tvar: string list -> string * string list
   val scan_nat: string list -> string * string list
   val scan_int: string list -> string * string list
+  val scan_hex: string list -> string * string list
+  val scan_bin: string list -> string * string list
   val string_of_vname: indexname -> string
   val string_of_vname': indexname -> string
   val indexname: string -> indexname
@@ -92,6 +94,8 @@
 
 val scan_letter_letdigs = Scan.one Symbol.is_letter -- Scan.any Symbol.is_letdig >> op ::;
 val scan_digits1 = Scan.any1 Symbol.is_digit;
+val scan_hex1 = Scan.any1 (Symbol.is_digit orf Symbol.is_hex_letter);
+val scan_bin1 = Scan.any1 (fn s => s = "0" orelse s = "1");
 
 val scan_id = scan_letter_letdigs >> implode;
 val scan_longid = scan_id ^^ (Scan.repeat1 ($$ "." ^^ scan_id) >> implode);
@@ -100,6 +104,9 @@
 val scan_nat = scan_digits1 >> implode;
 val scan_int = $$ "-" ^^ scan_nat || scan_nat;
 
+val scan_hex = ($$ "0") ^^ ($$ "x") ^^ (scan_hex1 >> implode);
+val scan_bin = ($$ "0") ^^ ($$ "b") ^^ (scan_bin1 >> implode);
+
 val scan_id_nat = scan_id ^^ Scan.optional ($$ "." ^^ scan_nat) "";
 val scan_var = $$ "?" ^^ scan_id_nat;
 val scan_tvar = $$ "?" ^^ $$ "'" ^^ scan_id_nat;
@@ -261,6 +268,8 @@
       scan_tvar >> pair TVarSy ||
       scan_var >> pair VarSy ||
       scan_tid >> pair TFreeSy ||
+      scan_hex >> pair NumSy ||
+      scan_bin >> pair NumSy ||
       scan_int >> pair NumSy ||
       $$ "#" ^^ scan_int >> pair XNumSy ||
       scan_longid >> pair LongIdentSy ||