array.mlw 4.28 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
  logic ([]) (a: array 'a) (i :int) : 'a = M.([]) a.elts i
12 13
  logic ([<-]) (a: array 'a) (i :int) (v: 'a) : array 'a =
    {| a with elts = M.([<-]) a.elts i v |}
14

15
  parameter ([]) : a:array 'a -> i:int ->
16
    { 0 <= i < length a } 'a reads a { result = a[i] }
17

18
  parameter ([]<-) : a:array 'a -> i:int -> v:'a ->
19
    { 0 <= i < length a } unit writes a { a.elts = M.([<-]) (old a.elts) i v }
20

21
  (* unsafe get/set operations with no precondition *)
22 23 24 25 26 27 28 29 30 31 32 33 34
  exception OutOfBounds

  parameter defensive_get: a:array 'a -> i:int ->
    { }
    'a reads a raises OutOfBounds
    { 0 <= i < length a and result = a[i] }
    | OutOfBounds -> { i < 0 or i >= length a }

  parameter defensive_set : a:array 'a -> i:int -> v:'a ->
    { }
    unit writes a raises OutOfBounds
    { 0 <= i < length a and a = (old a)[i <- v] }
    | OutOfBounds -> { i < 0 or i >= length a }
35

36 37
  parameter length : a:array 'a -> {} int { result = a.length }

38 39 40
  parameter make : n:int -> v:'a ->
    {}
    array 'a
41 42
    { result = {| length = n; elts = M.const v |} }
    (* { length result = n and forall i:int. 0 <= i < n -> result[i] = v} *)
43 44 45 46 47 48 49 50 51 52 53 54 55 56

  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] }

57 58 59 60
  parameter copy : a:array 'a ->
    {}
    array 'a
    { length result = length a and
61 62 63 64 65
      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
66 67 68 69
   writes a
   { (forall i:int.
       (0 <= i < ofs or ofs + len <= i < length a) -> a[i] = (old a)[i])
     and
70 71 72
     (forall i:int.
       ofs <= i < ofs + len -> a[i] = v) }

73
  parameter blit :
74 75 76 77
   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
78 79 80 81
   writes a2
   { (forall i:int.
       (0 <= i < ofs2 or ofs2 + len <= i < length a2) -> a2[i] = (old a2)[i])
     and
82 83
     (forall i:int.
       ofs2 <= i < ofs2 + len -> a2[i] = a1[ofs1 + i - ofs2]) }
84

85 86 87
  (* TODO?
     - concat : 'a array list -> 'a array
     - to_list
88
     - of_list
89
  *)
90 91 92

end

93 94 95
module ArraySorted

  use import module Array
96
  clone import map.MapSorted as M with type elt = int
97

98
  logic sorted_sub (a : array int) (l u : int) =
99 100
    M.sorted_sub a.elts l u

101
  logic sorted (a : array int) =
102 103 104 105 106 107 108
    M.sorted_sub a.elts 0 a.length

end

module ArrayEq

  use import module Array
109
  use import map.MapEq as M
110 111 112 113

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

114
  logic array_eq (a1 a2: array 'a) =
115 116 117 118 119 120 121 122 123 124
    a1.length = a2.length and
    array_eq_sub a1 a2 0 a1.length

end

module ArrayPermut

  use import module Array
  clone import map.MapPermut as M

125 126 127
  logic exchange (a1 a2: array 'a) (i j: int) =
    M.exchange a1.elts a2.elts i j

128
  logic permut_sub (a1 a2: array 'a) (l u: int) =
129 130
    M.permut_sub a1.elts a2.elts l u

131
  logic permut (a1 a2: array 'a) =
132 133 134 135
    a1.length = a2.length and M.permut_sub a1.elts a2.elts 0 a1.length

end

136
(***
137 138 139 140 141
module TestArray

  use import int.Int
  use import module Array

142
  let test_append () =
143 144
    let a1 = make 17 2 in
    assert { a1[3] = 2 };
145
    set a1 3 4;
146 147 148 149 150 151 152 153 154
    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 };
    ()

155
  let test_fill () =
156 157 158
    let a = make 17 True in
    fill a 10 4 False;
    assert { a[10] = False }
159

160 161 162 163 164 165 166 167 168 169
  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 }

170
end
171
***)
172

173
(*
174
Local Variables:
175
compile-command: "unset LANG; make -C .. modules/array"
176
End:
177
*)