src/HOL/Tools/float_syntax.ML
 author wenzelm Sun, 01 Mar 2009 23:36:12 +0100 changeset 30190 479806475f3c parent 28952 15a4b2cf8c34 child 32603 e08fdd615333 permissions -rw-r--r--
use long names for old-style fold combinators;
```
(*  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;
```