equal
deleted
inserted
replaced
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; |
|