my_cosine.mlw 1.14 KB
Newer Older
1
module M
Claude Marche's avatar
Claude Marche committed
2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31

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

parameter single_of_real_exact : x:real ->
  { }
  single
  { value result = x }

parameter add : x:single -> y:single ->
  { no_overflow NearestTiesToEven ((value x) +. (value y)) }
  single
  { value result = round NearestTiesToEven ((value x) +. (value y))}

parameter sub : x:single -> y:single ->
  { no_overflow NearestTiesToEven ((value x) -. (value y)) }
  single
  { value result = round NearestTiesToEven ((value x) -. (value y))}

parameter mul : x:single -> y:single ->
  { 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:
*)