--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/float_syntax.ML Wed Dec 03 15:58:44 2008 +0100
@@ -0,0 +1,47 @@
+(* ID: $Id$
+ Authors: Tobias Nipkow, TU Muenchen
+
+Concrete syntax for floats
+*)
+
+signature FLOAT_SYNTAX =
+sig
+ val setup: theory -> theory
+end;
+
+structure FloatSyntax: FLOAT_SYNTAX =
+struct
+
+(* parse translation *)
+
+local
+
+fun mk_number i =
+ let
+ fun mk 0 = Syntax.const @{const_name Int.Pls}
+ | mk ~1 = Syntax.const @{const_name Int.Min}
+ | mk i = let val (q, r) = Integer.div_mod i 2
+ in HOLogic.mk_bit r $ (mk q) end;
+ in Syntax.const @{const_name Int.number_of} $ mk i end;
+
+fun mk_frac str =
+ let
+ val {mant=i, exp = n} = Syntax.read_float str;
+ val exp = Syntax.const @{const_name "Power.power"};
+ val ten = mk_number 10;
+ val exp10 = if n=1 then ten else exp $ ten $ (mk_number n);
+ in (Syntax.const @{const_name "divide"}) $ (mk_number i) $ exp10 end
+in
+
+fun float_tr (*"_Float"*) [t as Const (str, _)] = mk_frac str
+ | float_tr (*"_Float"*) ts = raise TERM ("float_tr", ts);
+
+end;
+
+
+(* theory setup *)
+
+val setup =
+ Sign.add_trfuns ([], [("_Float", float_tr)], [], []);
+
+end;