my_cosine.mlw 1.12 KB
Newer Older
1
module M
Claude Marche's avatar
Claude Marche committed
2 3 4 5 6 7 8

  use import real.RealInfix
  use import real.Abs
  use import real.Trigonometry
  use import floating_point.Rounding
  use import floating_point.Single

Andrei Paskevich's avatar
Andrei Paskevich committed
9
val single_of_real_exact : x:real ->
Claude Marche's avatar
Claude Marche committed
10 11 12 13
  { }
  single
  { value result = x }

Andrei Paskevich's avatar
Andrei Paskevich committed
14
val add : x:single -> y:single ->
Claude Marche's avatar
Claude Marche committed
15 16 17 18
  { no_overflow NearestTiesToEven ((value x) +. (value y)) }
  single
  { value result = round NearestTiesToEven ((value x) +. (value y))}

Andrei Paskevich's avatar
Andrei Paskevich committed
19
val sub : x:single -> y:single ->
Claude Marche's avatar
Claude Marche committed
20 21 22 23
  { no_overflow NearestTiesToEven ((value x) -. (value y)) }
  single
  { value result = round NearestTiesToEven ((value x) -. (value y))}

Andrei Paskevich's avatar
Andrei Paskevich committed
24
val mul : x:single -> y:single ->
Claude Marche's avatar
Claude Marche committed
25 26 27 28 29 30 31
  { no_overflow NearestTiesToEven ((value x) *. (value y)) }
  single
  { value result = round NearestTiesToEven ((value x) *. (value y))}


let my_cosine (x:single) : single =
{ abs (value x) <=. 0x1p-5 }
32 33
  assert {
    abs (1.0 -. (value x) *. (value x) *. 0.5 -. cos (value x)) <=. 0x1p-24
Claude Marche's avatar
Claude Marche committed
34 35 36 37 38
  };
  sub (single_of_real_exact 1.0)
      (mul (mul x x) (single_of_real_exact 0.5))
{ abs (value result -. cos (value x)) <=. 0x1p-23 }

39 40
end

Claude Marche's avatar
Claude Marche committed
41 42
(*
Local Variables:
43
compile-command: "../../bin/whyide.byte my_cosine.mlw"
Claude Marche's avatar
Claude Marche committed
44 45
End:
*)