src/HOL/Tools/float_syntax.ML
author wenzelm
Mon Jan 16 21:50:15 2012 +0100 (2012-01-16)
changeset 46236 ae79f2978a67
parent 42290 b1f544c84040
child 47108 2a1953f0d20d
permissions -rw-r--r--
position constraints for numerals enable PIDE markup;
     1 (*  Title:      HOL/Tools/float_syntax.ML
     2     Author:     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 Float_Syntax: 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_syntax Int.Pls}
    22       | mk ~1 = Syntax.const @{const_syntax Int.Min}
    23       | mk i =
    24           let val (q, r) = Integer.div_mod i 2
    25           in HOLogic.mk_bit r $ (mk q) end;
    26   in Syntax.const @{const_syntax Int.number_of} $ mk i end;
    27 
    28 fun mk_frac str =
    29   let
    30     val {mant = i, exp = n} = Lexicon.read_float str;
    31     val exp = Syntax.const @{const_syntax Power.power};
    32     val ten = mk_number 10;
    33     val exp10 = if n = 1 then ten else exp $ ten $ mk_number n;
    34   in Syntax.const @{const_syntax divide} $ mk_number i $ exp10 end;
    35 
    36 in
    37 
    38 fun float_tr [(c as Const (@{syntax_const "_constrain"}, _)) $ t $ u] = c $ float_tr [t] $ u
    39   | float_tr [t as Const (str, _)] = mk_frac str
    40   | float_tr ts = raise TERM ("float_tr", ts);
    41 
    42 end;
    43 
    44 
    45 (* theory setup *)
    46 
    47 val setup =
    48   Sign.add_trfuns ([], [(@{syntax_const "_Float"}, float_tr)], [], []);
    49 
    50 end;