stdlib.mlw 3.14 KB
Newer Older
1

2
(* References *)
3

4
module Ref
5 6 7 8 9

  mutable type ref 'a model 'a

  parameter ref : v:'a -> {} ref 'a { result=v }

10
  parameter (!) : r:ref 'a -> {} 'a reads r { result=r }
11

12
  parameter (:=) : r:ref 'a -> v:'a -> {} unit writes r { r=v }
13 14 15

end

16 17 18 19 20 21 22 23 24 25 26
module Refint

  use export int.Int
  use export module Ref

  parameter incr : r:ref int -> {} unit writes r { r = old r + 1 }

  parameter decr : r:ref int -> {} unit writes r { r = old r - 1 }

end

27 28 29 30 31
(* Arrays *)

module Array

  use import int.Int
32
  use export array.ArrayLength
33

34
  mutable type array 'a model t int 'a
35

36
  parameter ([]) : a:array 'a -> i:int ->
37
    { 0 <= i < length a } 'a reads a { result = a[i] }
38

39
  parameter ([<-]) : a:array 'a -> i:int -> v:'a ->
40
    { 0 <= i < length a } unit writes a { a = (old a)[i <- v] }
41

42 43
  parameter length : a:array 'a -> {} int reads a { result = length a }

44 45 46
  parameter make : n:int -> v:'a ->
    {}
    array 'a
47 48 49 50 51 52 53 54 55 56 57 58 59 60 61
    { length result = n and forall i:int. 0 <= i < n -> result[i] = v}

  parameter append : a1:array 'a -> a2:array 'a ->
    {}
    array 'a
    { length result = length a1 + length a2 and
      (forall i:int. 0 <= i < length a1 -> result[i] = a1[i]) and
      (forall i:int. 0 <= i < length a2 -> result[length a1 + i] = a2[i]) }

  parameter sub : a:array 'a -> ofs:int -> len:int ->
    { 0 <= ofs and ofs + len <= length a }
    array 'a
    { length result = len and
      forall i:int. 0 <= i < len -> result[i] = a[ofs + i] }

62 63 64 65
  parameter copy : a:array 'a ->
    {}
    array 'a
    { length result = length a and
66 67 68 69 70 71
      forall i:int. 0 <= i < length result -> result[i] = a[i] }

  parameter fill : a:array 'a -> ofs:int -> len:int -> v:'a ->
   { 0 <= ofs and ofs + len <= length a }
   unit
   writes a
72 73 74
   { (forall i:int.
       (0 <= i < ofs or ofs + len <= i < length a) -> a[i] = (old a)[i])
     and
75 76 77
     (forall i:int.
       ofs <= i < ofs + len -> a[i] = v) }

78
  parameter blit :
79 80 81 82 83
   a1:array 'a -> ofs1:int -> a2:array 'a -> ofs2:int -> len:int ->
   { 0 <= ofs1 and ofs1 + len <= length a1 and
     0 <= ofs2 and ofs2 + len <= length a2 }
   unit
   writes a2
84 85 86
   { (forall i:int.
       (0 <= i < ofs2 or ofs2 + len <= i < length a2) -> a2[i] = (old a2)[i])
     and
87 88
     (forall i:int.
       ofs2 <= i < ofs2 + len -> a2[i] = a1[ofs1 + i - ofs2]) }
89

90 91 92
  (* TODO?
     - concat : 'a array list -> 'a array
     - to_list
93
     - of_list
94
  *)
95 96 97 98 99 100 101 102

end

module TestArray

  use import int.Int
  use import module Array

103
  let test_append () =
104 105 106 107 108 109 110 111 112 113 114 115
    let a1 = make 17 2 in
    assert { a1[3] = 2 };
    a1[3 <- 4];
    assert { a1[3] = 4 };
    let a2 = make 25 3 in
    assert { a2[0] = 3 }; (* needed to prove a[17]=3 below *)
    let a  = append a1 a2 in
    assert { length a = 42 };
    assert { a[3] = 4 };
    assert { a[17] = 3 };
    ()

116
  let test_fill () =
117 118 119
    let a = make 17 True in
    fill a 10 4 False;
    assert { a[10] = False }
120

121 122 123 124 125 126 127 128 129 130
  let test_blit () =
    let a1 = make 17 True in
    let a2 = make 25 False in
    blit a1 10 a2 17 7;
    assert { a1[10] = True  };
    assert { a2[16] = False };
    assert { a2[17] = True  };
    assert { a2[23] = True  };
    assert { a2[24] = False }

131 132
end

133
(*
134
Local Variables:
135
compile-command: "unset LANG; make -C .. modules/stdlib"
136
End:
137
*)