src/HOL/Tools/numeral_syntax.ML
 changeset 20067 26bac504ef90 parent 19481 a6205c6203ea child 20094 99f27df2b6d0
```     1.1 --- a/src/HOL/Tools/numeral_syntax.ML	Mon Jul 10 21:02:29 2006 +0200
1.2 +++ b/src/HOL/Tools/numeral_syntax.ML	Tue Jul 11 00:43:54 2006 +0200
1.3 @@ -1,6 +1,6 @@
1.4  (*  Title:      HOL/Tools/numeral_syntax.ML
1.5      ID:         \$Id\$
1.6 -    Author:     Markus Wenzel, TU Muenchen
1.7 +    Authors:    Markus Wenzel, TU Muenchen
1.8
1.9  Concrete syntax for generic numerals.  Assumes consts and syntax of
1.10  theory HOL/Numeral.
1.11 @@ -37,8 +37,34 @@
1.12
1.13  (* translation of integer numeral tokens to and from bitstrings *)
1.14
1.15 +(*additional translations of binary and hex numbers to normal numbers*)
1.16 +local
1.17 +
1.18 +(*get A => ord"0" + 10, etc*)
1.19 +fun remap_hex c =
1.20 +  let
1.21 +    val zero = ord"0";
1.22 +    val a  = ord"a";
1.23 +    val ca = ord"A";
1.24 +    val x  = ord c;
1.25 +  in
1.26 +    if x >= a then chr (x - a + zero + 10)
1.27 +    else if x >= ca then chr (x - ca + zero + 10)
1.28 +    else c
1.29 +  end;
1.30 +
1.31 +fun str_to_int' ("0" :: "x" :: ds) = read_radixint (16, map remap_hex ds) |> #1
1.32 +  | str_to_int' ("0" :: "b" :: ds) = read_radixint (2, ds) |> #1
1.33 +  | str_to_int' ds = implode ds |> IntInf.fromString |> valOf;
1.34 +
1.35 +in
1.36 +
1.37 +val str_to_int = str_to_int' o explode;
1.38 +
1.39 +end;
1.40 +
1.41  fun numeral_tr (*"_Numeral"*) [t as Const (str, _)] =
1.42 -      (Syntax.const "Numeral.number_of" \$ (HOLogic.mk_binum (valOf (IntInf.fromString str))))
1.43 +      (Syntax.const "Numeral.number_of" \$ (HOLogic.mk_binum (str_to_int str)))
1.44    | numeral_tr (*"_Numeral"*) ts = raise TERM ("numeral_tr", ts);
1.45
1.46  fun numeral_tr' show_sorts (*"number_of"*) (Type ("fun", [_, T])) (t :: ts) =
```