new module for hash tables (in progress)

modules/array.mlw

@@ -19,10 +19,19 @@ module Array
     { 0 <= i < length a } unit writes a { a = (old a)[i <- v] }
 
   (* unsafe get/set operations with no precondition *)
-  parameter unsafe_get : a:array 'a -> i:int ->
-    { } 'a reads a { result = a[i] }
-  parameter unsafe_set : a:array 'a -> i:int -> v:'a ->
-    { } unit writes a { a = (old a)[i <- v] }
+  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 }
 
   parameter length : a:array 'a -> {} int { result = a.length }
 

modules/hashtbl.mlw

+
+module Hashtbl
+
+  use import list.List
+  use import map.Map
+
+  type key
+
+  type t 'a model {| mutable contents: map key (list 'a) |}
+
+  logic ([]) (h: t 'a) (k: key) : list 'a = get h k
+
+  parameter create: n:int ->
+    {} t 'a { forall k: key. result[k] = Nil }
+
+  parameter clear: h: t 'a ->
+    {} unit writes h { forall k: key. h[k] = Nil }
+
+  parameter add: h: t 'a -> k: key -> v: 'a ->
+    {}
+    unit writes h
+    { h[k] = Cons v (old h)[k] and
+      forall k': key. k' <> k -> h[k'] = (old h)[k'] }
+
+(*
+       val copy : ('a, 'b) t -> ('a, 'b) t
+
+       val find : ('a, 'b) t -> 'a -> 'b
+
+       val find_all : ('a, 'b) t -> 'a -> 'b list
+
+       val mem : ('a, 'b) t -> 'a -> bool
+       val remove : ('a, 'b) t -> 'a -> unit
+
+       val replace : ('a, 'b) t -> 'a -> 'b -> unit
+
+       val iter : ('a -> 'b -> unit) -> ('a, 'b) t -> unit
+
+       val fold : ('a -> 'b -> 'c -> 'c) -> ('a, 'b) t -> 'c -> 'c
+
+       val length : ('a, 'b) t -> int
+*)
+
+end
+
+(*
+Local Variables:
+compile-command: "unset LANG; make -C .. modules/hashtbl"
+End:
+*)