28906
|
1 |
(* ID: $Id$
|
|
2 |
Authors: Tobias Nipkow, TU Muenchen
|
|
3 |
|
|
4 |
Concrete syntax for floats
|
|
5 |
*)
|
|
6 |
|
|
7 |
signature FLOAT_SYNTAX =
|
|
8 |
sig
|
|
9 |
val setup: theory -> theory
|
|
10 |
end;
|
|
11 |
|
|
12 |
structure FloatSyntax: FLOAT_SYNTAX =
|
|
13 |
struct
|
|
14 |
|
|
15 |
(* parse translation *)
|
|
16 |
|
|
17 |
local
|
|
18 |
|
|
19 |
fun mk_number i =
|
|
20 |
let
|
|
21 |
fun mk 0 = Syntax.const @{const_name Int.Pls}
|
|
22 |
| mk ~1 = Syntax.const @{const_name Int.Min}
|
|
23 |
| mk i = let val (q, r) = Integer.div_mod i 2
|
|
24 |
in HOLogic.mk_bit r $ (mk q) end;
|
|
25 |
in Syntax.const @{const_name Int.number_of} $ mk i end;
|
|
26 |
|
|
27 |
fun mk_frac str =
|
|
28 |
let
|
|
29 |
val {mant=i, exp = n} = Syntax.read_float str;
|
|
30 |
val exp = Syntax.const @{const_name "Power.power"};
|
|
31 |
val ten = mk_number 10;
|
|
32 |
val exp10 = if n=1 then ten else exp $ ten $ (mk_number n);
|
|
33 |
in (Syntax.const @{const_name "divide"}) $ (mk_number i) $ exp10 end
|
|
34 |
in
|
|
35 |
|
|
36 |
fun float_tr (*"_Float"*) [t as Const (str, _)] = mk_frac str
|
|
37 |
| float_tr (*"_Float"*) ts = raise TERM ("float_tr", ts);
|
|
38 |
|
|
39 |
end;
|
|
40 |
|
|
41 |
|
|
42 |
(* theory setup *)
|
|
43 |
|
|
44 |
val setup =
|
|
45 |
Sign.add_trfuns ([], [("_Float", float_tr)], [], []);
|
|
46 |
|
|
47 |
end;
|