src/HOL/Tools/float_arith.ML
author wenzelm
Sun, 01 Mar 2009 23:36:12 +0100
changeset 30190 479806475f3c
parent 29804 e15b74577368
child 37391 476270a6c2dc
permissions -rw-r--r--
use long names for old-style fold combinators;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
29804
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 28952
diff changeset
     1
(*  Title:  HOL/Tools/float_arith.ML
22964
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
     2
    Author: Steven Obua
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
     3
*)
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
     4
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
     5
signature FLOAT_ARITH =
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
     6
sig
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
     7
  exception Destruct_floatstr of string
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
     8
  val destruct_floatstr: (char -> bool) -> (char -> bool) -> string -> bool * string * string * bool * string
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
     9
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
    10
  exception Floating_point of string
24630
351a308ab58d simplified type int (eliminated IntInf.int, integer);
wenzelm
parents: 24584
diff changeset
    11
  val approx_dec_by_bin: int -> Float.float -> Float.float * Float.float
22964
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
    12
  val approx_decstr_by_bin: int -> string -> Float.float * Float.float
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
    13
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
    14
  val mk_float: Float.float -> term
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
    15
  val dest_float: term -> Float.float
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
    16
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
    17
  val approx_float: int -> (Float.float * Float.float -> Float.float * Float.float)
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
    18
    -> string -> term * term
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
    19
end;
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
    20
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
    21
structure FloatArith : FLOAT_ARITH =
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
    22
struct
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
    23
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
    24
exception Destruct_floatstr of string;
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
    25
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
    26
fun destruct_floatstr isDigit isExp number =
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
    27
  let
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
    28
    val numlist = filter (not o Char.isSpace) (String.explode number)
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
    29
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
    30
    fun countsigns ((#"+")::cs) = countsigns cs
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
    31
      | countsigns ((#"-")::cs) =
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
    32
      let
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
    33
        val (positive, rest) = countsigns cs
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
    34
      in
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
    35
        (not positive, rest)
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
    36
      end
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
    37
      | countsigns cs = (true, cs)
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
    38
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
    39
    fun readdigits [] = ([], [])
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
    40
      | readdigits (q as c::cs) =
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
    41
      if (isDigit c) then
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
    42
        let
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
    43
          val (digits, rest) = readdigits cs
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
    44
        in
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
    45
          (c::digits, rest)
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
    46
        end
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
    47
      else
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
    48
        ([], q)
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
    49
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
    50
    fun readfromexp_helper cs =
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
    51
      let
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
    52
        val (positive, rest) = countsigns cs
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
    53
        val (digits, rest') = readdigits rest
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
    54
      in
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
    55
        case rest' of
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
    56
          [] => (positive, digits)
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
    57
          | _ => raise (Destruct_floatstr number)
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
    58
      end
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
    59
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
    60
    fun readfromexp [] = (true, [])
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
    61
      | readfromexp (c::cs) =
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
    62
      if isExp c then
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
    63
        readfromexp_helper cs
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
    64
      else
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
    65
        raise (Destruct_floatstr number)
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
    66
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
    67
    fun readfromdot [] = ([], readfromexp [])
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
    68
      | readfromdot ((#".")::cs) =
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
    69
      let
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
    70
        val (digits, rest) = readdigits cs
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
    71
        val exp = readfromexp rest
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
    72
      in
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
    73
        (digits, exp)
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
    74
      end
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
    75
      | readfromdot cs = readfromdot ((#".")::cs)
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
    76
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
    77
    val (positive, numlist) = countsigns numlist
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
    78
    val (digits1, numlist) = readdigits numlist
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
    79
     val (digits2, exp) = readfromdot numlist
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
    80
  in
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
    81
    (positive, String.implode digits1, String.implode digits2, fst exp, String.implode (snd exp))
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
    82
  end
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
    83
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
    84
exception Floating_point of string;
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
    85
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
    86
val ln2_10 = Math.ln 10.0 / Math.ln 2.0;
23569
6be49c181c66 fixed argument order in calls to Integer.pow
obua
parents: 23297
diff changeset
    87
fun exp5 x = Integer.pow x 5;
6be49c181c66 fixed argument order in calls to Integer.pow
obua
parents: 23297
diff changeset
    88
fun exp10 x = Integer.pow x 10;
25300
bc3a1c964704 corrected fucked up integer tuning
obua
parents: 24630
diff changeset
    89
fun exp2 x = Integer.pow x 2;
22964
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
    90
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
    91
fun find_most_significant q r =
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
    92
  let
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
    93
    fun int2real i =
24630
351a308ab58d simplified type int (eliminated IntInf.int, integer);
wenzelm
parents: 24584
diff changeset
    94
      case (Real.fromString o string_of_int) i of
22964
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
    95
        SOME r => r
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
    96
        | NONE => raise (Floating_point "int2real")
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
    97
    fun subtract (q, r) (q', r') =
24630
351a308ab58d simplified type int (eliminated IntInf.int, integer);
wenzelm
parents: 24584
diff changeset
    98
      if r <= r' then
23297
06f108974fa1 simplified type integer;
wenzelm
parents: 23261
diff changeset
    99
        (q - q' * exp10 (r' - r), r)
22964
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
   100
      else
23297
06f108974fa1 simplified type integer;
wenzelm
parents: 23261
diff changeset
   101
        (q * exp10 (r - r') - q', r')
22964
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
   102
    fun bin2dec d =
24630
351a308ab58d simplified type int (eliminated IntInf.int, integer);
wenzelm
parents: 24584
diff changeset
   103
      if 0 <= d then
25300
bc3a1c964704 corrected fucked up integer tuning
obua
parents: 24630
diff changeset
   104
        (exp2 d, 0)
22964
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
   105
      else
23297
06f108974fa1 simplified type integer;
wenzelm
parents: 23261
diff changeset
   106
        (exp5 (~ d), d)
22964
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
   107
24630
351a308ab58d simplified type int (eliminated IntInf.int, integer);
wenzelm
parents: 24584
diff changeset
   108
    val L = Real.floor (int2real (IntInf.log2 q) + int2real r * ln2_10)
23297
06f108974fa1 simplified type integer;
wenzelm
parents: 23261
diff changeset
   109
    val L1 = L + 1
22964
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
   110
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
   111
    val (q1, r1) = subtract (q, r) (bin2dec L1) 
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
   112
  in
24630
351a308ab58d simplified type int (eliminated IntInf.int, integer);
wenzelm
parents: 24584
diff changeset
   113
    if 0 <= q1 then
22964
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
   114
      let
23297
06f108974fa1 simplified type integer;
wenzelm
parents: 23261
diff changeset
   115
        val (q2, r2) = subtract (q, r) (bin2dec (L1 + 1))
22964
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
   116
      in
24630
351a308ab58d simplified type int (eliminated IntInf.int, integer);
wenzelm
parents: 24584
diff changeset
   117
        if 0 <= q2 then
22964
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
   118
          raise (Floating_point "find_most_significant")
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
   119
        else
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
   120
          (L1, (q1, r1))
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
   121
      end
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
   122
    else
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
   123
      let
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
   124
        val (q0, r0) = subtract (q, r) (bin2dec L)
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
   125
      in
24630
351a308ab58d simplified type int (eliminated IntInf.int, integer);
wenzelm
parents: 24584
diff changeset
   126
        if 0 <= q0 then
22964
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
   127
          (L, (q0, r0))
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
   128
        else
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
   129
          raise (Floating_point "find_most_significant")
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
   130
      end
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
   131
  end
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
   132
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
   133
fun approx_dec_by_bin n (q,r) =
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
   134
  let
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
   135
    fun addseq acc d' [] = acc
25300
bc3a1c964704 corrected fucked up integer tuning
obua
parents: 24630
diff changeset
   136
      | addseq acc d' (d::ds) = addseq (acc + exp2 (d - d')) d' ds
22964
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
   137
23297
06f108974fa1 simplified type integer;
wenzelm
parents: 23261
diff changeset
   138
    fun seq2bin [] = (0, 0)
24630
351a308ab58d simplified type int (eliminated IntInf.int, integer);
wenzelm
parents: 24584
diff changeset
   139
      | seq2bin (d::ds) = (addseq 0 d ds + 1, d)
22964
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
   140
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
   141
    fun approx d_seq d0 precision (q,r) =
23297
06f108974fa1 simplified type integer;
wenzelm
parents: 23261
diff changeset
   142
      if q = 0 then
22964
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
   143
        let val x = seq2bin d_seq in
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
   144
          (x, x)
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
   145
        end
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
   146
      else
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
   147
        let
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
   148
          val (d, (q', r')) = find_most_significant q r
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
   149
        in
24630
351a308ab58d simplified type int (eliminated IntInf.int, integer);
wenzelm
parents: 24584
diff changeset
   150
          if precision < d0 - d then
22964
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
   151
            let
23297
06f108974fa1 simplified type integer;
wenzelm
parents: 23261
diff changeset
   152
              val d' = d0 - precision
22964
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
   153
              val x1 = seq2bin (d_seq)
25300
bc3a1c964704 corrected fucked up integer tuning
obua
parents: 24630
diff changeset
   154
              val x2 = (fst x1 * exp2 (snd x1 - d') + 1,  d') (* = seq2bin (d'::d_seq) *)
22964
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
   155
            in
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
   156
              (x1, x2)
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
   157
            end
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
   158
          else
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
   159
            approx (d::d_seq) d0 precision (q', r')
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
   160
        end
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
   161
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
   162
    fun approx_start precision (q, r) =
24630
351a308ab58d simplified type int (eliminated IntInf.int, integer);
wenzelm
parents: 24584
diff changeset
   163
      if q = 0 then
23297
06f108974fa1 simplified type integer;
wenzelm
parents: 23261
diff changeset
   164
        ((0, 0), (0, 0))
22964
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
   165
      else
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
   166
        let
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
   167
          val (d, (q', r')) = find_most_significant q r
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
   168
        in
24630
351a308ab58d simplified type int (eliminated IntInf.int, integer);
wenzelm
parents: 24584
diff changeset
   169
          if precision <= 0 then
22964
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
   170
            let
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
   171
              val x1 = seq2bin [d]
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
   172
            in
23297
06f108974fa1 simplified type integer;
wenzelm
parents: 23261
diff changeset
   173
              if q' = 0 then
22964
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
   174
                (x1, x1)
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
   175
              else
24630
351a308ab58d simplified type int (eliminated IntInf.int, integer);
wenzelm
parents: 24584
diff changeset
   176
                (x1, seq2bin [d + 1])
22964
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
   177
            end
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
   178
          else
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
   179
            approx [d] d precision (q', r')
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
   180
        end
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
   181
  in
24630
351a308ab58d simplified type int (eliminated IntInf.int, integer);
wenzelm
parents: 24584
diff changeset
   182
    if 0 <= q then
22964
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
   183
      approx_start n (q,r)
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
   184
    else
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
   185
      let
23297
06f108974fa1 simplified type integer;
wenzelm
parents: 23261
diff changeset
   186
        val ((a1,b1), (a2, b2)) = approx_start n (~ q, r)
22964
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
   187
      in
23297
06f108974fa1 simplified type integer;
wenzelm
parents: 23261
diff changeset
   188
        ((~ a2, b2), (~ a1, b1))
22964
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
   189
      end
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
   190
  end
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
   191
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
   192
fun approx_decstr_by_bin n decstr =
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
   193
  let
24630
351a308ab58d simplified type int (eliminated IntInf.int, integer);
wenzelm
parents: 24584
diff changeset
   194
    fun str2int s = the_default 0 (Int.fromString s)
351a308ab58d simplified type int (eliminated IntInf.int, integer);
wenzelm
parents: 24584
diff changeset
   195
    fun signint p x = if p then x else ~ x
22964
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
   196
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
   197
    val (p, d1, d2, ep, e) = destruct_floatstr Char.isDigit (fn e => e = #"e" orelse e = #"E") decstr
24630
351a308ab58d simplified type int (eliminated IntInf.int, integer);
wenzelm
parents: 24584
diff changeset
   198
    val s = size d2
22964
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
   199
23297
06f108974fa1 simplified type integer;
wenzelm
parents: 23261
diff changeset
   200
    val q = signint p (str2int d1 * exp10 s + str2int d2)
06f108974fa1 simplified type integer;
wenzelm
parents: 23261
diff changeset
   201
    val r = signint ep (str2int e) - s
22964
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
   202
  in
24630
351a308ab58d simplified type int (eliminated IntInf.int, integer);
wenzelm
parents: 24584
diff changeset
   203
    approx_dec_by_bin n (q,r)
22964
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
   204
  end
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
   205
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
   206
fun mk_float (a, b) = @{term "float"} $
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
   207
  HOLogic.mk_prod (pairself (HOLogic.mk_number HOLogic.intT) (a, b));
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
   208
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
   209
fun dest_float (Const ("Float.float", _) $ (Const ("Pair", _) $ a $ b)) =
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
   210
      pairself (snd o HOLogic.dest_number) (a, b)
23297
06f108974fa1 simplified type integer;
wenzelm
parents: 23261
diff changeset
   211
  | dest_float t = ((snd o HOLogic.dest_number) t, 0);
22964
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
   212
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
   213
fun approx_float prec f value =
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
   214
  let
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
   215
    val interval = approx_decstr_by_bin prec value
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
   216
    val (flower, fupper) = f interval
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
   217
  in
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
   218
    (mk_float flower, mk_float fupper)
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
   219
  end;
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
   220
2284e0d02e7f reorganized float arithmetic
haftmann
parents:
diff changeset
   221
end;