src/HOL/Real/float_syntax.ML
changeset 28906 5f568bfc58d7
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Real/float_syntax.ML	Sat Nov 29 13:39:45 2008 +0100
     1.3 @@ -0,0 +1,47 @@
     1.4 +(*  ID:         $Id$
     1.5 +    Authors:    Tobias Nipkow, TU Muenchen
     1.6 +
     1.7 +Concrete syntax for floats
     1.8 +*)
     1.9 +
    1.10 +signature FLOAT_SYNTAX =
    1.11 +sig
    1.12 +  val setup: theory -> theory
    1.13 +end;
    1.14 +
    1.15 +structure FloatSyntax: FLOAT_SYNTAX =
    1.16 +struct
    1.17 +
    1.18 +(* parse translation *)
    1.19 +
    1.20 +local
    1.21 +
    1.22 +fun mk_number i =
    1.23 +  let
    1.24 +    fun mk 0 = Syntax.const @{const_name Int.Pls}
    1.25 +      | mk ~1 =  Syntax.const @{const_name Int.Min}
    1.26 +      | mk i = let val (q, r) = Integer.div_mod i 2
    1.27 +               in HOLogic.mk_bit r $ (mk q) end;
    1.28 +  in Syntax.const @{const_name Int.number_of} $ mk i end;
    1.29 +
    1.30 +fun mk_frac str =
    1.31 +  let
    1.32 +    val {mant=i, exp = n} = Syntax.read_float str;
    1.33 +    val exp = Syntax.const @{const_name "Power.power"};
    1.34 +    val ten = mk_number 10;
    1.35 +    val exp10 = if n=1 then ten else exp $ ten $ (mk_number n);
    1.36 +  in (Syntax.const @{const_name "divide"}) $ (mk_number i) $ exp10 end
    1.37 +in
    1.38 +
    1.39 +fun float_tr (*"_Float"*) [t as Const (str, _)] = mk_frac str
    1.40 +  | float_tr (*"_Float"*) ts = raise TERM ("float_tr", ts);
    1.41 +
    1.42 +end;
    1.43 +
    1.44 +
    1.45 +(* theory setup *)
    1.46 +
    1.47 +val setup =
    1.48 +  Sign.add_trfuns ([], [("_Float", float_tr)], [], []);
    1.49 +
    1.50 +end;