new stdlib module for matrices

parent 825f64be
(** {1 Matrices} *)
module Matrix
use import int.Int
use import map.Map as M
type matrix 'a
model { rows: int; columns: int; mutable elts: map int (map int 'a) }
invariant { 0 <= self.rows /\ 0 <= self.columns }
type index = (int, int)
function get (a: matrix 'a) (i: index) : 'a =
let r,c = i in M.get (M.get a.elts r) c
function set (a: matrix 'a) (i: index) (v: 'a) : matrix 'a =
let r,c = i in
{ a with elts = M.set a.elts r (M.set (M.get a.elts r) c v) }
predicate valid_index (a: matrix 'a) (i: index) =
let r,c = i in 0 <= r < a.rows /\ 0 <= c < a.columns
val get (a: matrix 'a) (i: index) : 'a reads {a}
requires { valid_index a i }
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 }
ensures { let r,c = i in
a.elts = M.set (old a.elts) r (M.set (M.get (old a.elts) r) c v) }
val rows (a: matrix 'a) : int ensures { result = a.rows }
val columns (a: matrix 'a) : int ensures { result = a.columns }
(** unsafe get/set operations with no precondition *)
exception OutOfBounds
let defensive_get (a: matrix 'a) (i: index)
ensures { valid_index a i /\ result = get a i }
raises { OutOfBounds -> not (valid_index a i) }
= let r,c = i in
if r < 0 || r >= a.rows || c < 0 || c >= a.columns then raise OutOfBounds;
get a i
let defensive_set (a: matrix 'a) (i: index) (v: 'a)
ensures { valid_index a i /\ a = set (old a) i v }
raises { OutOfBounds -> not (valid_index a i) }
= let r,c = i in
if r < 0 || r >= a.rows || c < 0 || c >= a.columns then raise OutOfBounds;
set a i v
function make (r c: int) (v: 'a) : matrix 'a =
{ rows = r; columns = c; elts = M.const (M.const v) }
val make (r c: int) (v: 'a) : matrix 'a
requires { r >= 0 /\ c >= 0 } ensures { result = make r c v }
val copy (a: matrix 'a) : matrix 'a
ensures { result.rows = a.rows /\ result.columns = a.columns }
ensures { forall r:int. 0 <= r < result.rows ->
forall c:int. 0 <= c < result.columns ->
get result (r,c) = get a (r,c) }
end
(* {2 Square bracket syntax in both logic and programs} *)
module Syntax
use import int.Int
use export Matrix
function ([]) (a: matrix 'a) (i: index) : 'a = get a i
function ([<-]) (a: matrix 'a) (i: index) (v: 'a) : matrix 'a = set a i v
val ([]) (a: matrix 'a) (i: index) : 'a reads {a}
requires { valid_index a i }
ensures { result = get a i }
val ([]<-) (a: matrix 'a) (i: index) (v: 'a) : unit writes {a}
requires { let r,c = i in 0 <= r < a.rows /\ 0 <= c < a.columns }
ensures { let r,c = i in
a.elts = M.set (old a.elts) r (M.set (M.get (old a.elts) r) c v) }
end
(* {2 Test module} *)
module TestMatrix
use import int.Int
use import Syntax
let test1 () =
let m1 = make 3 3 2 in
assert { m1[(0,0)] = 2 };
m1[(0,0)] <- 4;
assert { m1[(0,0)] = 4 };
assert { m1[(0,1)] = 2 };
assert { m1[(1,0)] = 2 };
()
end
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