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;
wenzelm@35115
     1
(*  Author:     Tobias Nipkow, TU Muenchen
nipkow@28906
     2
wenzelm@35115
     3
Concrete syntax for floats.
nipkow@28906
     4
*)
nipkow@28906
     5
nipkow@28906
     6
signature FLOAT_SYNTAX =
nipkow@28906
     7
sig
nipkow@28906
     8
  val setup: theory -> theory
nipkow@28906
     9
end;
nipkow@28906
    10
nipkow@28906
    11
structure FloatSyntax: FLOAT_SYNTAX =
nipkow@28906
    12
struct
nipkow@28906
    13
nipkow@28906
    14
(* parse translation *)
nipkow@28906
    15
nipkow@28906
    16
local
nipkow@28906
    17
nipkow@28906
    18
fun mk_number i =
nipkow@28906
    19
  let
wenzelm@35115
    20
    fun mk 0 = Syntax.const @{const_syntax Int.Pls}
wenzelm@35115
    21
      | mk ~1 = Syntax.const @{const_syntax Int.Min}
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;
wenzelm@35115
    25
  in Syntax.const @{const_syntax Int.number_of} $ mk i end;
nipkow@28906
    26
nipkow@28906
    27
fun mk_frac str =
nipkow@28906
    28
  let
wenzelm@35115
    29
    val {mant = i, exp = n} = Syntax.read_float str;
wenzelm@35115
    30
    val exp = Syntax.const @{const_syntax Power.power};
nipkow@28906
    31
    val ten = mk_number 10;
wenzelm@35115
    32
    val exp10 = if n = 1 then ten else exp $ ten $ mk_number n;
wenzelm@35115
    33
  in Syntax.const @{const_syntax divide} $ mk_number i $ exp10 end;
wenzelm@35115
    34
nipkow@28906
    35
in
nipkow@28906
    36
nipkow@28906
    37
fun float_tr (*"_Float"*) [t as Const (str, _)] = mk_frac str
nipkow@28906
    38
  | float_tr (*"_Float"*) ts = raise TERM ("float_tr", ts);
nipkow@28906
    39
nipkow@28906
    40
end;
nipkow@28906
    41
nipkow@28906
    42
nipkow@28906
    43
(* theory setup *)
nipkow@28906
    44
nipkow@28906
    45
val setup =
wenzelm@35115
    46
  Sign.add_trfuns ([], [(@{syntax_const "_Float"}, float_tr)], [], []);
nipkow@28906
    47
nipkow@28906
    48
end;