author | wenzelm |
Wed, 25 Jul 2012 18:05:07 +0200 | |
changeset 48502 | fd03877ad5bc |
parent 47108 | 2a1953f0d20d |
child 52143 | 36ffe23b25f8 |
permissions | -rw-r--r-- |
37744 | 1 |
(* Title: HOL/Tools/float_syntax.ML |
2 |
Author: Tobias Nipkow, TU Muenchen |
|
28906 | 3 |
|
35115 | 4 |
Concrete syntax for floats. |
28906 | 5 |
*) |
6 |
||
7 |
signature FLOAT_SYNTAX = |
|
8 |
sig |
|
9 |
val setup: theory -> theory |
|
10 |
end; |
|
11 |
||
35123 | 12 |
structure Float_Syntax: FLOAT_SYNTAX = |
28906 | 13 |
struct |
14 |
||
15 |
(* parse translation *) |
|
16 |
||
17 |
local |
|
18 |
||
19 |
fun mk_number i = |
|
20 |
let |
|
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46236
diff
changeset
|
21 |
fun mk 1 = Syntax.const @{const_syntax Num.One} |
35115 | 22 |
| mk i = |
23 |
let val (q, r) = Integer.div_mod i 2 |
|
24 |
in HOLogic.mk_bit r $ (mk q) end; |
|
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46236
diff
changeset
|
25 |
in |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46236
diff
changeset
|
26 |
if i = 0 then Syntax.const @{const_syntax Groups.zero} |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46236
diff
changeset
|
27 |
else if i > 0 then Syntax.const @{const_syntax Num.numeral} $ mk i |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46236
diff
changeset
|
28 |
else Syntax.const @{const_syntax Num.neg_numeral} $ mk (~i) |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46236
diff
changeset
|
29 |
end; |
28906 | 30 |
|
31 |
fun mk_frac str = |
|
32 |
let |
|
42290
b1f544c84040
discontinued special treatment of structure Lexicon;
wenzelm
parents:
37744
diff
changeset
|
33 |
val {mant = i, exp = n} = Lexicon.read_float str; |
35115 | 34 |
val exp = Syntax.const @{const_syntax Power.power}; |
28906 | 35 |
val ten = mk_number 10; |
35115 | 36 |
val exp10 = if n = 1 then ten else exp $ ten $ mk_number n; |
37 |
in Syntax.const @{const_syntax divide} $ mk_number i $ exp10 end; |
|
38 |
||
28906 | 39 |
in |
40 |
||
46236
ae79f2978a67
position constraints for numerals enable PIDE markup;
wenzelm
parents:
42290
diff
changeset
|
41 |
fun float_tr [(c as Const (@{syntax_const "_constrain"}, _)) $ t $ u] = c $ float_tr [t] $ u |
ae79f2978a67
position constraints for numerals enable PIDE markup;
wenzelm
parents:
42290
diff
changeset
|
42 |
| float_tr [t as Const (str, _)] = mk_frac str |
ae79f2978a67
position constraints for numerals enable PIDE markup;
wenzelm
parents:
42290
diff
changeset
|
43 |
| float_tr ts = raise TERM ("float_tr", ts); |
28906 | 44 |
|
45 |
end; |
|
46 |
||
47 |
||
48 |
(* theory setup *) |
|
49 |
||
50 |
val setup = |
|
35115 | 51 |
Sign.add_trfuns ([], [(@{syntax_const "_Float"}, float_tr)], [], []); |
28906 | 52 |
|
53 |
end; |