OCaml driver for matrix.Matrix

parent efc1378b
......@@ -1270,7 +1270,8 @@ clean::
# Ocaml realizations
#######################
OCAMLLIBS_FILES = why3__BigInt_compat why3__BigInt why3__IntAux why3__Array
OCAMLLIBS_FILES = why3__BigInt_compat why3__BigInt why3__IntAux why3__Array \
why3__Matrix
OCAMLLIBS_MODULES := $(addprefix lib/ocaml/, $(OCAMLLIBS_FILES))
......
......@@ -119,6 +119,23 @@ module array.Array
syntax val blit "Why3__Array.blit"
end
module matrix.Matrix
syntax type matrix "(%1 Why3__Matrix.t)"
syntax function get "(Why3__Matrix.get %1 %2)"
syntax exception OutOfBounds "Why3__Matrix.OutOfBounds"
syntax val get "Why3__Matrix.get"
syntax val set "Why3__Matrix.set"
syntax val rows "Why3__Matrix.rows"
syntax val columns "Why3__Matrix.columns"
syntax val defensive_get "Why3__Matrix.defensive_get"
syntax val defensive_set "Why3__Matrix.defensive_set"
syntax val make "Why3__Matrix.make"
syntax val copy "Why3__Matrix.copy"
end
module mach.int.Int
syntax val ( / ) "Why3__BigInt.computer_div"
syntax val ( % ) "Why3__BigInt.computer_mod"
......
open Why3__BigInt
type 'a t = 'a array array
let get m (i,j) = m.(to_int i).(to_int j)
let set m (i,j) v = m.(to_int i).(to_int j) <- v
let rows m = of_int (Array.length m)
let columns m =
if Array.length m = 0 then invalid_arg "Why3__Matrix.columns";
of_int (Array.length m.(0))
exception OutOfBounds
let check_bounds a i = if i < 0 || i >= Array.length a then raise OutOfBounds
let defensive_get m (i,j) =
let i = to_int i in let j = to_int j in
check_bounds m i; check_bounds m.(i) j; m.(i).(j)
let defensive_set m (i,j) v =
let i = to_int i in let j = to_int j in
check_bounds m i; check_bounds m.(i) j; m.(i).(j) <- v
let make n m v = Array.make_matrix (to_int n) (to_int m) v
let copy m = Array.map Array.copy m
......@@ -26,7 +26,7 @@ module Matrix
ensures { result = get a i }
val set (a: matrix 'a) (i: index) (v: 'a) : unit writes {a}
requires { let r,c = i in 0 <= r < a.rows /\ 0 <= c < a.columns }
requires { valid_index a i }
ensures { let r,c = i in
a.elts = M.set (old a.elts) r (M.set (M.get (old a.elts) r) c v) }
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment