src/HOL/Tools/float_syntax.ML
author haftmann
Fri Sep 18 09:07:50 2009 +0200 (2009-09-18)
changeset 32603 e08fdd615333
parent 28952 15a4b2cf8c34
child 35115 446c5063e4fd
permissions -rw-r--r--
tuned const_name antiquotations
     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;