src/HOL/Tools/float_syntax.ML
author wenzelm
Sat, 13 Feb 2010 23:24:57 +0100
changeset 35123 e286d5df187a
parent 35115 446c5063e4fd
child 37744 3daaf23b9ab4
permissions -rw-r--r--
modernized structures;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
35115
446c5063e4fd modernized translations;
wenzelm
parents: 32603
diff changeset
     1
(*  Author:     Tobias Nipkow, TU Muenchen
28906
5f568bfc58d7 Floats for Real.
nipkow
parents:
diff changeset
     2
35115
446c5063e4fd modernized translations;
wenzelm
parents: 32603
diff changeset
     3
Concrete syntax for floats.
28906
5f568bfc58d7 Floats for Real.
nipkow
parents:
diff changeset
     4
*)
5f568bfc58d7 Floats for Real.
nipkow
parents:
diff changeset
     5
5f568bfc58d7 Floats for Real.
nipkow
parents:
diff changeset
     6
signature FLOAT_SYNTAX =
5f568bfc58d7 Floats for Real.
nipkow
parents:
diff changeset
     7
sig
5f568bfc58d7 Floats for Real.
nipkow
parents:
diff changeset
     8
  val setup: theory -> theory
5f568bfc58d7 Floats for Real.
nipkow
parents:
diff changeset
     9
end;
5f568bfc58d7 Floats for Real.
nipkow
parents:
diff changeset
    10
35123
e286d5df187a modernized structures;
wenzelm
parents: 35115
diff changeset
    11
structure Float_Syntax: FLOAT_SYNTAX =
28906
5f568bfc58d7 Floats for Real.
nipkow
parents:
diff changeset
    12
struct
5f568bfc58d7 Floats for Real.
nipkow
parents:
diff changeset
    13
5f568bfc58d7 Floats for Real.
nipkow
parents:
diff changeset
    14
(* parse translation *)
5f568bfc58d7 Floats for Real.
nipkow
parents:
diff changeset
    15
5f568bfc58d7 Floats for Real.
nipkow
parents:
diff changeset
    16
local
5f568bfc58d7 Floats for Real.
nipkow
parents:
diff changeset
    17
5f568bfc58d7 Floats for Real.
nipkow
parents:
diff changeset
    18
fun mk_number i =
5f568bfc58d7 Floats for Real.
nipkow
parents:
diff changeset
    19
  let
35115
446c5063e4fd modernized translations;
wenzelm
parents: 32603
diff changeset
    20
    fun mk 0 = Syntax.const @{const_syntax Int.Pls}
446c5063e4fd modernized translations;
wenzelm
parents: 32603
diff changeset
    21
      | mk ~1 = Syntax.const @{const_syntax Int.Min}
446c5063e4fd modernized translations;
wenzelm
parents: 32603
diff changeset
    22
      | mk i =
446c5063e4fd modernized translations;
wenzelm
parents: 32603
diff changeset
    23
          let val (q, r) = Integer.div_mod i 2
446c5063e4fd modernized translations;
wenzelm
parents: 32603
diff changeset
    24
          in HOLogic.mk_bit r $ (mk q) end;
446c5063e4fd modernized translations;
wenzelm
parents: 32603
diff changeset
    25
  in Syntax.const @{const_syntax Int.number_of} $ mk i end;
28906
5f568bfc58d7 Floats for Real.
nipkow
parents:
diff changeset
    26
5f568bfc58d7 Floats for Real.
nipkow
parents:
diff changeset
    27
fun mk_frac str =
5f568bfc58d7 Floats for Real.
nipkow
parents:
diff changeset
    28
  let
35115
446c5063e4fd modernized translations;
wenzelm
parents: 32603
diff changeset
    29
    val {mant = i, exp = n} = Syntax.read_float str;
446c5063e4fd modernized translations;
wenzelm
parents: 32603
diff changeset
    30
    val exp = Syntax.const @{const_syntax Power.power};
28906
5f568bfc58d7 Floats for Real.
nipkow
parents:
diff changeset
    31
    val ten = mk_number 10;
35115
446c5063e4fd modernized translations;
wenzelm
parents: 32603
diff changeset
    32
    val exp10 = if n = 1 then ten else exp $ ten $ mk_number n;
446c5063e4fd modernized translations;
wenzelm
parents: 32603
diff changeset
    33
  in Syntax.const @{const_syntax divide} $ mk_number i $ exp10 end;
446c5063e4fd modernized translations;
wenzelm
parents: 32603
diff changeset
    34
28906
5f568bfc58d7 Floats for Real.
nipkow
parents:
diff changeset
    35
in
5f568bfc58d7 Floats for Real.
nipkow
parents:
diff changeset
    36
5f568bfc58d7 Floats for Real.
nipkow
parents:
diff changeset
    37
fun float_tr (*"_Float"*) [t as Const (str, _)] = mk_frac str
5f568bfc58d7 Floats for Real.
nipkow
parents:
diff changeset
    38
  | float_tr (*"_Float"*) ts = raise TERM ("float_tr", ts);
5f568bfc58d7 Floats for Real.
nipkow
parents:
diff changeset
    39
5f568bfc58d7 Floats for Real.
nipkow
parents:
diff changeset
    40
end;
5f568bfc58d7 Floats for Real.
nipkow
parents:
diff changeset
    41
5f568bfc58d7 Floats for Real.
nipkow
parents:
diff changeset
    42
5f568bfc58d7 Floats for Real.
nipkow
parents:
diff changeset
    43
(* theory setup *)
5f568bfc58d7 Floats for Real.
nipkow
parents:
diff changeset
    44
5f568bfc58d7 Floats for Real.
nipkow
parents:
diff changeset
    45
val setup =
35115
446c5063e4fd modernized translations;
wenzelm
parents: 32603
diff changeset
    46
  Sign.add_trfuns ([], [(@{syntax_const "_Float"}, float_tr)], [], []);
28906
5f568bfc58d7 Floats for Real.
nipkow
parents:
diff changeset
    47
5f568bfc58d7 Floats for Real.
nipkow
parents:
diff changeset
    48
end;