src/HOL/Tools/float_syntax.ML
author wenzelm
Thu Feb 11 23:00:22 2010 +0100 (2010-02-11)
changeset 35115 446c5063e4fd
parent 32603 e08fdd615333
child 35123 e286d5df187a
permissions -rw-r--r--
modernized translations;
formal markup of @{syntax_const} and @{const_syntax};
minor tuning;
     1 (*  Author:     Tobias Nipkow, TU Muenchen
     2 
     3 Concrete syntax for floats.
     4 *)
     5 
     6 signature FLOAT_SYNTAX =
     7 sig
     8   val setup: theory -> theory
     9 end;
    10 
    11 structure FloatSyntax: FLOAT_SYNTAX =
    12 struct
    13 
    14 (* parse translation *)
    15 
    16 local
    17 
    18 fun mk_number i =
    19   let
    20     fun mk 0 = Syntax.const @{const_syntax Int.Pls}
    21       | mk ~1 = Syntax.const @{const_syntax Int.Min}
    22       | mk i =
    23           let val (q, r) = Integer.div_mod i 2
    24           in HOLogic.mk_bit r $ (mk q) end;
    25   in Syntax.const @{const_syntax 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_syntax 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_syntax divide} $ mk_number i $ exp10 end;
    34 
    35 in
    36 
    37 fun float_tr (*"_Float"*) [t as Const (str, _)] = mk_frac str
    38   | float_tr (*"_Float"*) ts = raise TERM ("float_tr", ts);
    39 
    40 end;
    41 
    42 
    43 (* theory setup *)
    44 
    45 val setup =
    46   Sign.add_trfuns ([], [(@{syntax_const "_Float"}, float_tr)], [], []);
    47 
    48 end;