src/HOL/Tools/float_syntax.ML
changeset 52146 ceb31e1ded30
parent 52145 28963df2dffb
child 52147 9943f8067f11
equal deleted inserted replaced
52145:28963df2dffb 52146:ceb31e1ded30
     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 1 = Syntax.const @{const_syntax Num.One}
       
    22       | mk i =
       
    23           let val (q, r) = Integer.div_mod i 2
       
    24           in HOLogic.mk_bit r $ (mk q) end;
       
    25   in
       
    26     if i = 0 then Syntax.const @{const_syntax Groups.zero}
       
    27     else if i > 0 then Syntax.const @{const_syntax Num.numeral} $ mk i
       
    28     else Syntax.const @{const_syntax Num.neg_numeral} $ mk (~i)
       
    29   end;
       
    30 
       
    31 fun mk_frac str =
       
    32   let
       
    33     val {mant = i, exp = n} = Lexicon.read_float str;
       
    34     val exp = Syntax.const @{const_syntax Power.power};
       
    35     val ten = mk_number 10;
       
    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 
       
    39 in
       
    40 
       
    41 fun float_tr [(c as Const (@{syntax_const "_constrain"}, _)) $ t $ u] = c $ float_tr [t] $ u
       
    42   | float_tr [t as Const (str, _)] = mk_frac str
       
    43   | float_tr ts = raise TERM ("float_tr", ts);
       
    44 
       
    45 end;
       
    46 
       
    47 
       
    48 (* theory setup *)
       
    49 
       
    50 val setup = Sign.parse_translation [(@{syntax_const "_Float"}, K float_tr)];
       
    51 
       
    52 end;