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) =