src/HOL/Tools/float_syntax.ML
author wenzelm
Sun, 01 Mar 2009 23:36:12 +0100
changeset 30190 479806475f3c
parent 28952 15a4b2cf8c34
child 32603 e08fdd615333
permissions -rw-r--r--
use long names for old-style fold combinators;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
28906
5f568bfc58d7 Floats for Real.
nipkow
parents:
diff changeset
     1
(*  ID:         $Id$
5f568bfc58d7 Floats for Real.
nipkow
parents:
diff changeset
     2
    Authors:    Tobias Nipkow, TU Muenchen
5f568bfc58d7 Floats for Real.
nipkow
parents:
diff changeset
     3
5f568bfc58d7 Floats for Real.
nipkow
parents:
diff changeset
     4
Concrete syntax for floats
5f568bfc58d7 Floats for Real.
nipkow
parents:
diff changeset
     5
*)
5f568bfc58d7 Floats for Real.
nipkow
parents:
diff changeset
     6
5f568bfc58d7 Floats for Real.
nipkow
parents:
diff changeset
     7
signature FLOAT_SYNTAX =
5f568bfc58d7 Floats for Real.
nipkow
parents:
diff changeset
     8
sig
5f568bfc58d7 Floats for Real.
nipkow
parents:
diff changeset
     9
  val setup: theory -> theory
5f568bfc58d7 Floats for Real.
nipkow
parents:
diff changeset
    10
end;
5f568bfc58d7 Floats for Real.
nipkow
parents:
diff changeset
    11
5f568bfc58d7 Floats for Real.
nipkow
parents:
diff changeset
    12
structure FloatSyntax: FLOAT_SYNTAX =
5f568bfc58d7 Floats for Real.
nipkow
parents:
diff changeset
    13
struct
5f568bfc58d7 Floats for Real.
nipkow
parents:
diff changeset
    14
5f568bfc58d7 Floats for Real.
nipkow
parents:
diff changeset
    15
(* parse translation *)
5f568bfc58d7 Floats for Real.
nipkow
parents:
diff changeset
    16
5f568bfc58d7 Floats for Real.
nipkow
parents:
diff changeset
    17
local
5f568bfc58d7 Floats for Real.
nipkow
parents:
diff changeset
    18
5f568bfc58d7 Floats for Real.
nipkow
parents:
diff changeset
    19
fun mk_number i =
5f568bfc58d7 Floats for Real.
nipkow
parents:
diff changeset
    20
  let
5f568bfc58d7 Floats for Real.
nipkow
parents:
diff changeset
    21
    fun mk 0 = Syntax.const @{const_name Int.Pls}
5f568bfc58d7 Floats for Real.
nipkow
parents:
diff changeset
    22
      | mk ~1 =  Syntax.const @{const_name Int.Min}
5f568bfc58d7 Floats for Real.
nipkow
parents:
diff changeset
    23
      | mk i = let val (q, r) = Integer.div_mod i 2
5f568bfc58d7 Floats for Real.
nipkow
parents:
diff changeset
    24
               in HOLogic.mk_bit r $ (mk q) end;
5f568bfc58d7 Floats for Real.
nipkow
parents:
diff changeset
    25
  in Syntax.const @{const_name Int.number_of} $ mk i end;
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
5f568bfc58d7 Floats for Real.
nipkow
parents:
diff changeset
    29
    val {mant=i, exp = n} = Syntax.read_float str;
5f568bfc58d7 Floats for Real.
nipkow
parents:
diff changeset
    30
    val exp = Syntax.const @{const_name "Power.power"};
5f568bfc58d7 Floats for Real.
nipkow
parents:
diff changeset
    31
    val ten = mk_number 10;
5f568bfc58d7 Floats for Real.
nipkow
parents:
diff changeset
    32
    val exp10 = if n=1 then ten else exp $ ten $ (mk_number n);
5f568bfc58d7 Floats for Real.
nipkow
parents:
diff changeset
    33
  in (Syntax.const @{const_name "divide"}) $ (mk_number i) $ exp10 end
5f568bfc58d7 Floats for Real.
nipkow
parents:
diff changeset
    34
in
5f568bfc58d7 Floats for Real.
nipkow
parents:
diff changeset
    35
5f568bfc58d7 Floats for Real.
nipkow
parents:
diff changeset
    36
fun float_tr (*"_Float"*) [t as Const (str, _)] = mk_frac str
5f568bfc58d7 Floats for Real.
nipkow
parents:
diff changeset
    37
  | float_tr (*"_Float"*) ts = raise TERM ("float_tr", ts);
5f568bfc58d7 Floats for Real.
nipkow
parents:
diff changeset
    38
5f568bfc58d7 Floats for Real.
nipkow
parents:
diff changeset
    39
end;
5f568bfc58d7 Floats for Real.
nipkow
parents:
diff changeset
    40
5f568bfc58d7 Floats for Real.
nipkow
parents:
diff changeset
    41
5f568bfc58d7 Floats for Real.
nipkow
parents:
diff changeset
    42
(* theory setup *)
5f568bfc58d7 Floats for Real.
nipkow
parents:
diff changeset
    43
5f568bfc58d7 Floats for Real.
nipkow
parents:
diff changeset
    44
val setup =
5f568bfc58d7 Floats for Real.
nipkow
parents:
diff changeset
    45
  Sign.add_trfuns ([], [("_Float", float_tr)], [], []);
5f568bfc58d7 Floats for Real.
nipkow
parents:
diff changeset
    46
5f568bfc58d7 Floats for Real.
nipkow
parents:
diff changeset
    47
end;