arith.mlw 1.27 KB
Newer Older
1

MARCHE Claude's avatar
MARCHE Claude committed
2 3 4 5
(** {1 Arithmetic for programs} *)

(** {2 Integer Division} 

6
It is checked that divisor is not null.
MARCHE Claude's avatar
MARCHE Claude committed
7 8

*)
9 10 11 12 13 14 15 16 17 18

module Int

  use export int.Int
  use export int.ComputerDivision

  let (/) (x: int) (y:int) = { y <> 0 } div x y { result = div x y }

end

MARCHE Claude's avatar
MARCHE Claude committed
19 20
(** {2 Machine integers}

21
32-bit integers and such go here.
MARCHE Claude's avatar
MARCHE Claude committed
22 23

*)
24

25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48
module Int32

  use export int.Int

  function min_int : int = -2147483648
  function max_int : int =  2147483647

  let (+) (x: int) (y:int) =
    { min_int <= x + y <= max_int } x + y { result = x + y }
  let (-) (x: int) (y:int) =
    { min_int <= x - y <= max_int } x - y { result = x - y }

  let (-_) (x: int) =
    { min_int <= -x <= max_int } -x { result = -x  }

  let ( * ) (x: int) (y:int) =
    { min_int <= x * y <= max_int } x * y { result = x * y }

  use export int.ComputerDivision

  let (/) (x: int) (y:int) =
    { y <> 0 && min_int <= div x y <= max_int } div x y { result = div x y }

end
49

50
(** {2 Division on real numbers}
MARCHE Claude's avatar
MARCHE Claude committed
51

52
See also {h <a href="floating_point.why.html">Floating-Point theories</a>.}
MARCHE Claude's avatar
MARCHE Claude committed
53 54

*)
55

56 57 58 59 60 61 62 63 64 65
module Real

  use import real.Real
  use export real.RealInfix
  use export real.FromInt

  let (/.) (x: real) (y: real) = { y <> 0. } x / y { result = x / y }

end

MARCHE Claude's avatar
MARCHE Claude committed
66
(***
67 68 69 70
Local Variables:
compile-command: "unset LANG; make -C .. modules/arith"
End:
*)