array.mlw 5.43 KB
Newer Older
1

2 3
(* Arrays *)

4 5 6
module Array

  use import int.Int
7
  use import map.Map as M
8

9
  type array 'a model {| length : int; mutable elts : map int 'a |}
10

11 12 13 14 15 16 17 18
  logic get (a: array 'a) (i: int) : 'a = M.get a.elts i

  logic set (a: array 'a) (i: int) (v: 'a) : array 'a =
    {| a with elts = M.set a.elts i v |}

  (* syntactic sugar *)
  logic ([]) (a: array 'a) (i: int) : 'a = get a i
  logic ([<-]) (a: array 'a) (i: int) (v: 'a) : array 'a = set a i v
19

20
  parameter ([]) (a: array 'a) (i: int) :
21
    { 0 <= i < length a } 'a reads a { result = a[i] }
22

23
  parameter ([]<-) (a: array 'a) (i: int) (v: 'a) :
24
    { 0 <= i < length a } unit writes a { a.elts = M.set (old a.elts) i v }
25

26 27
  parameter length (a: array 'a) : {} int { result = a.length }

28
  (* unsafe get/set operations with no precondition *)
29 30
  exception OutOfBounds

31
  let defensive_get (a: array 'a) (i: int) =
32
    { }
33 34
    if i < 0 || i >= length a then raise OutOfBounds;
    a[i]
35 36 37
    { 0 <= i < length a and result = a[i] }
    | OutOfBounds -> { i < 0 or i >= length a }

38
  let defensive_set (a: array 'a) (i: int) (v: 'a) =
39
    { }
40 41
    if i < 0 || i >= length a then raise OutOfBounds;
    a[i] <- v
42 43
    { 0 <= i < length a and a = (old a)[i <- v] }
    | OutOfBounds -> { i < 0 or i >= length a }
44

45
  parameter make (n: int) (v: 'a) :
46 47
    {}
    array 'a
48 49
    { result = {| length = n; elts = M.const v |} }
    (* { length result = n and forall i:int. 0 <= i < n -> result[i] = v} *)
50

51
  parameter append (a1: array 'a) (a2: array 'a) :
52 53 54 55 56 57
    {}
    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]) }

58
  parameter sub (a: array 'a) (ofs: int) (len: int) :
59 60 61 62 63
    { 0 <= ofs and ofs + len <= length a }
    array 'a
    { length result = len and
      forall i:int. 0 <= i < len -> result[i] = a[ofs + i] }

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

70
  let fill (a: array 'a) (ofs: int) (len: int) (v: 'a) =
71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86
    { 0 <= ofs and ofs + len <= length a }
    label Init:
    for k = 0 to len - 1 do
      invariant {
        (forall i:int.
        (0 <= i < ofs or ofs + len <= i < length a) -> a[i] = (at a Init)[i])
        and
        (forall i:int. ofs <= i < ofs + k -> a[i] = v)
      }
      a[ofs + k] <- v
    done
    { (forall i:int.
        (0 <= i < ofs or ofs + len <= i < length a) -> a[i] = (old a)[i])
      and
      (forall i:int.
        ofs <= i < ofs + len -> a[i] = v) }
87

88 89
  parameter blit (a1: array 'a) (ofs1: int)
                 (a2: array 'a) (ofs2: int) (len: int) :
90 91 92 93 94 95 96 97 98
    { 0 <= ofs1 and ofs1 + len <= length a1 and
      0 <= ofs2 and ofs2 + len <= length a2 }
    unit
    writes a2
    { (forall i:int.
        (0 <= i < ofs2 or ofs2 + len <= i < length a2) -> a2[i] = (old a2)[i])
      and
      (forall i:int.
        ofs2 <= i < ofs2 + len -> a2[i] = a1[ofs1 + i - ofs2]) }
99

100 101 102
  (* TODO?
     - concat : 'a array list -> 'a array
     - to_list
103
     - of_list
104
  *)
105 106 107

end

108 109
module ArraySorted

110
  use import int.Int
111
  use import module Array
112
  clone import map.MapSorted as M with type elt = int, logic le = (<=)
113

114
  logic sorted_sub (a : array int) (l u : int) =
115 116
    M.sorted_sub a.elts l u

117
  logic sorted (a : array int) =
118 119 120 121 122 123 124
    M.sorted_sub a.elts 0 a.length

end

module ArrayEq

  use import module Array
125
  use import map.MapEq as M
126 127 128 129

  logic array_eq_sub (a1 a2: array 'a) (l u: int) =
    map_eq_sub a1.elts a2.elts l u

130
  logic array_eq (a1 a2: array 'a) =
131 132 133 134 135 136 137
    a1.length = a2.length and
    array_eq_sub a1 a2 0 a1.length

end

module ArrayPermut

138
  use import int.Int
139 140 141
  use import module Array
  clone import map.MapPermut as M

142 143 144
  logic exchange (a1 a2: array 'a) (i j: int) =
    M.exchange a1.elts a2.elts i j

145
  logic permut_sub (a1 a2: array 'a) (l u: int) =
146 147
    M.permut_sub a1.elts a2.elts l u

148
  logic permut (a1 a2: array 'a) =
149 150
    a1.length = a2.length and M.permut_sub a1.elts a2.elts 0 a1.length

151 152 153 154 155 156
  lemma exchange_permut:
    forall a1 a2: array 'a, i j: int.
    exchange a1 a2 i j -> a1.length = a2.length ->
    0 <= i < a1.length -> 0 <= j < a1.length ->
    permut a1 a2

157 158 159 160 161 162 163 164 165 166
  use import module ArrayEq

  lemma array_eq_sub_permut:
    forall a1 a2: array 'a, l u: int.
    array_eq_sub a1 a2 l u -> permut_sub a1 a2 l u

  lemma array_eq_permut:
    forall a1 a2: array 'a.
    array_eq a1 a2 -> permut a1 a2

167 168
end

169 170 171 172 173 174 175 176 177 178 179
module ArraySum

  use import module Array
  clone import map.MapSum as M

  (* [sum a l h] is the sum of a[i] for l <= i < h *)

  logic sum (a: array int) (l h: int) : int = M.sum a.elts l h

end

180 181 182 183 184
module TestArray

  use import int.Int
  use import module Array

185
  let test_append () =
186 187
    let a1 = make 17 2 in
    assert { a1[3] = 2 };
188
    a1[3] <- 4;
189 190 191 192 193 194 195 196 197
    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 };
    ()

198
  let test_fill () =
199 200
    let a = make 17 True in
    fill a 10 4 False;
201 202 203
    assert { a[9] = True };
    assert { a[10] = False };
    assert { a[14] = True }
204

205 206 207 208 209 210 211 212 213 214
  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 }

215 216
end

217
(*
218
Local Variables:
219
compile-command: "unset LANG; make -C .. modules/array"
220
End:
221
*)