hex and binary numerals (contributed by Rafal Kolanski)
authorkleing
Tue Jul 11 00:43:54 2006 +0200 (2006-07-11)
changeset 2006726bac504ef90
parent 20066 b045b835cb3b
child 20068 19c7361db4a3
hex and binary numerals (contributed by Rafal Kolanski)
CONTRIBUTORS
NEWS
src/HOL/Tools/numeral_syntax.ML
src/Pure/General/symbol.ML
src/Pure/Syntax/lexicon.ML
     1.1 --- a/CONTRIBUTORS	Mon Jul 10 21:02:29 2006 +0200
     1.2 +++ b/CONTRIBUTORS	Tue Jul 11 00:43:54 2006 +0200
     1.3 @@ -1,6 +1,9 @@
     1.4  Contributions to Isabelle
     1.5  -------------------------
     1.6  
     1.7 +* July 2006: Rafal Kolanski, NICTA
     1.8 +  Hex (0xFF) and binary (0b1011) numerals.
     1.9 +
    1.10  * May 2006: Klaus Aehlig, LMU
    1.11    Command 'normal_form': normalization by evaluation.
    1.12  
     2.1 --- a/NEWS	Mon Jul 10 21:02:29 2006 +0200
     2.2 +++ b/NEWS	Tue Jul 11 00:43:54 2006 +0200
     2.3 @@ -488,6 +488,7 @@
     2.4    (i.e. a boolean expression) by compiling it to ML. The goal is
     2.5    "proved" (via the oracle "Evaluation") if it evaluates to True.
     2.6  
     2.7 +* Support for hex (0x20) and binary (0b1001) numerals. 
     2.8  
     2.9  *** HOL-Complex ***
    2.10  
     3.1 --- a/src/HOL/Tools/numeral_syntax.ML	Mon Jul 10 21:02:29 2006 +0200
     3.2 +++ b/src/HOL/Tools/numeral_syntax.ML	Tue Jul 11 00:43:54 2006 +0200
     3.3 @@ -1,6 +1,6 @@
     3.4  (*  Title:      HOL/Tools/numeral_syntax.ML
     3.5      ID:         $Id$
     3.6 -    Author:     Markus Wenzel, TU Muenchen
     3.7 +    Authors:    Markus Wenzel, TU Muenchen
     3.8  
     3.9  Concrete syntax for generic numerals.  Assumes consts and syntax of
    3.10  theory HOL/Numeral.
    3.11 @@ -37,8 +37,34 @@
    3.12  
    3.13  (* translation of integer numeral tokens to and from bitstrings *)
    3.14  
    3.15 +(*additional translations of binary and hex numbers to normal numbers*)
    3.16 +local
    3.17 +
    3.18 +(*get A => ord"0" + 10, etc*)
    3.19 +fun remap_hex c =
    3.20 +  let 
    3.21 +    val zero = ord"0"; 
    3.22 +    val a  = ord"a";
    3.23 +    val ca = ord"A";
    3.24 +    val x  = ord c;
    3.25 +  in
    3.26 +    if x >= a then chr (x - a + zero + 10)
    3.27 +    else if x >= ca then chr (x - ca + zero + 10) 
    3.28 +    else c
    3.29 +  end;
    3.30 +
    3.31 +fun str_to_int' ("0" :: "x" :: ds) = read_radixint (16, map remap_hex ds) |> #1
    3.32 +  | str_to_int' ("0" :: "b" :: ds) = read_radixint (2, ds) |> #1
    3.33 +  | str_to_int' ds = implode ds |> IntInf.fromString |> valOf; 
    3.34 +
    3.35 +in
    3.36 +
    3.37 +val str_to_int = str_to_int' o explode;
    3.38 +
    3.39 +end;
    3.40 +
    3.41  fun numeral_tr (*"_Numeral"*) [t as Const (str, _)] =
    3.42 -      (Syntax.const "Numeral.number_of" $ (HOLogic.mk_binum (valOf (IntInf.fromString str))))
    3.43 +      (Syntax.const "Numeral.number_of" $ (HOLogic.mk_binum (str_to_int str)))
    3.44    | numeral_tr (*"_Numeral"*) ts = raise TERM ("numeral_tr", ts);
    3.45  
    3.46  fun numeral_tr' show_sorts (*"number_of"*) (Type ("fun", [_, T])) (t :: ts) =
     4.1 --- a/src/Pure/General/symbol.ML	Mon Jul 10 21:02:29 2006 +0200
     4.2 +++ b/src/Pure/General/symbol.ML	Tue Jul 11 00:43:54 2006 +0200
     4.3 @@ -23,6 +23,7 @@
     4.4    val malformed: symbol
     4.5    val is_ascii: symbol -> bool
     4.6    val is_ascii_letter: symbol -> bool
     4.7 +  val is_hex_letter: symbol -> bool
     4.8    val is_ascii_digit: symbol -> bool
     4.9    val is_ascii_quasi: symbol -> bool
    4.10    val is_ascii_blank: symbol -> bool
    4.11 @@ -125,6 +126,11 @@
    4.12     (ord "A" <= ord s andalso ord s <= ord "Z" orelse
    4.13      ord "a" <= ord s andalso ord s <= ord "z");
    4.14  
    4.15 +fun is_hex_letter s =
    4.16 +  is_char s andalso
    4.17 +   (ord "A" <= ord s andalso ord s <= ord "F" orelse
    4.18 +    ord "a" <= ord s andalso ord s <= ord "f");
    4.19 +
    4.20  fun is_ascii_digit s =
    4.21    is_char s andalso ord "0" <= ord s andalso ord s <= ord "9";
    4.22  
     5.1 --- a/src/Pure/Syntax/lexicon.ML	Mon Jul 10 21:02:29 2006 +0200
     5.2 +++ b/src/Pure/Syntax/lexicon.ML	Tue Jul 11 00:43:54 2006 +0200
     5.3 @@ -18,6 +18,8 @@
     5.4    val scan_tvar: string list -> string * string list
     5.5    val scan_nat: string list -> string * string list
     5.6    val scan_int: string list -> string * string list
     5.7 +  val scan_hex: string list -> string * string list
     5.8 +  val scan_bin: string list -> string * string list
     5.9    val string_of_vname: indexname -> string
    5.10    val string_of_vname': indexname -> string
    5.11    val indexname: string -> indexname
    5.12 @@ -92,6 +94,8 @@
    5.13  
    5.14  val scan_letter_letdigs = Scan.one Symbol.is_letter -- Scan.any Symbol.is_letdig >> op ::;
    5.15  val scan_digits1 = Scan.any1 Symbol.is_digit;
    5.16 +val scan_hex1 = Scan.any1 (Symbol.is_digit orf Symbol.is_hex_letter);
    5.17 +val scan_bin1 = Scan.any1 (fn s => s = "0" orelse s = "1");
    5.18  
    5.19  val scan_id = scan_letter_letdigs >> implode;
    5.20  val scan_longid = scan_id ^^ (Scan.repeat1 ($$ "." ^^ scan_id) >> implode);
    5.21 @@ -100,6 +104,9 @@
    5.22  val scan_nat = scan_digits1 >> implode;
    5.23  val scan_int = $$ "-" ^^ scan_nat || scan_nat;
    5.24  
    5.25 +val scan_hex = ($$ "0") ^^ ($$ "x") ^^ (scan_hex1 >> implode);
    5.26 +val scan_bin = ($$ "0") ^^ ($$ "b") ^^ (scan_bin1 >> implode);
    5.27 +
    5.28  val scan_id_nat = scan_id ^^ Scan.optional ($$ "." ^^ scan_nat) "";
    5.29  val scan_var = $$ "?" ^^ scan_id_nat;
    5.30  val scan_tvar = $$ "?" ^^ $$ "'" ^^ scan_id_nat;
    5.31 @@ -261,6 +268,8 @@
    5.32        scan_tvar >> pair TVarSy ||
    5.33        scan_var >> pair VarSy ||
    5.34        scan_tid >> pair TFreeSy ||
    5.35 +      scan_hex >> pair NumSy ||
    5.36 +      scan_bin >> pair NumSy ||
    5.37        scan_int >> pair NumSy ||
    5.38        $$ "#" ^^ scan_int >> pair XNumSy ||
    5.39        scan_longid >> pair LongIdentSy ||