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