hashtbl specification completed

modules/hashtbl.mlw

@@ -10,36 +10,94 @@ module Hashtbl
 
   logic ([]) (h: t 'a) (k: key) : list 'a = Map.([]) h.contents k
 
-  parameter create: n:int ->
+  parameter create (n:int) :
     {} t 'a { forall k: key. result[k] = Nil }
 
-  parameter clear: h: t 'a ->
+  parameter clear (h: t 'a) :
     {} unit writes h { forall k: key. h[k] = Nil }
 
-  parameter add: h: t 'a -> k: key -> v: 'a ->
+  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
+  parameter mem (h: t 'a) (k: key) :
+    {}
+    bool reads h
+    { result=True <-> h[k] <> Nil }
 
-       val find : ('a, 'b) t -> 'a -> 'b
+  parameter find (h: t 'a) (k: key) :
+    { h[k] <> Nil }
+    'a reads h
+    { match h[k] with Nil -> false | Cons v _ -> result = v end }
 
-       val find_all : ('a, 'b) t -> 'a -> 'b list
+  parameter find_all (h: t 'a) (k: key) :
+    {}
+    list 'a reads h
+    { result = h[k] }
 
-       val mem : ('a, 'b) t -> 'a -> bool
-       val remove : ('a, 'b) t -> 'a -> unit
+  exception NotFound
 
-       val replace : ('a, 'b) t -> 'a -> 'b -> unit
+  parameter defensive_find (h: t 'a) (k: key) :
+    {}
+    'a reads h raises NotFound
+    { match h[k] with Nil -> false | Cons v _ -> result = v end }
+    | NotFound -> { h[k] = Nil }
 
-       val iter : ('a -> 'b -> unit) -> ('a, 'b) t -> unit
+  parameter copy (h: t 'a) :
+    {}
+    t 'a reads h
+    { forall k: key. result[k] = h[k] }
 
-       val fold : ('a -> 'b -> 'c -> 'c) -> ('a, 'b) t -> 'c -> 'c
+  parameter remove (h: t 'a) (k: key) :
+    { h[k] <> Nil }
+    unit writes h
+    { (match (old h)[k] with Nil -> false | Cons _ l -> h[k] =l end) and
+      forall k': key. k' <> k -> h[k'] = (old h)[k'] }
+
+  parameter replace (h: t 'a) (k: key) (v: 'a) :
+    {}
+    unit writes h
+    { (h[k] = Cons v (match (old h)[k] with Nil -> Nil | Cons _ l -> l end))
+      and
+      forall k': key. k' <> k -> h[k'] = (old h)[k'] }
+
+  parameter length (h: t 'a) :
+    {}
+    int reads h
+    {} (* = the number of distinct keys *)
+
+  (* TODO
+     - val iter : ('a -> 'b -> unit) -> ('a, 'b) t -> unit
+     - val fold : ('a -> 'b -> 'c -> 'c) -> ('a, 'b) t -> 'c -> 'c
+  *)
+
+end
+
+module TestHashtbl
+
+  use import int.Int
+  use import list.List
+  use import module Hashtbl
+
+  logic k1: key
+  logic k2: key
+  logic k3: key
+  axiom kdiff : k1 <> k2 and k1 <> k3 and k2 <> k3
+
+  let test1 () =
+    let h = create 17 in
+    add h k1 True;
+    assert { h[k1] = Cons True Nil };
+    assert { h[k2] = Nil };
+    let v1 = find h k1 in
+    assert { v1 = True };
+    add h k1 False;
+    assert { h[k1] = Cons False (Cons True Nil) };
+    replace h k1 True;
+    assert { h[k1] = Cons True (Cons True Nil) }
 
-       val length : ('a, 'b) t -> int
-*)
 
 end
 

src/parser/parser.pre.mly

@@ -1322,12 +1322,22 @@ annotation:
 | LEFTBRC lexpr RIGHTBRC { $2 }
 ;
 
+annotation_post:
+| LEFTBRC RIGHTBRC       { mk_pp PPtrue }
+| LEFTBRC lexpr RIGHTBRC { $2 }
+/*
+| LEFTBRC pat_conj BAR lexpr RIGHTBRC
+    { let id = { id = "result"; id_lab = []; id_loc = floc (); } in
+      mk_pp (PPmatch (mk_pp (PPvar (Qident id)), [$2, $4])) }
+*/
+;
+
 pre:
 | annotation { $1 }
 ;
 
 post:
-| annotation list0_post_exn { $1, $2 }
+| annotation_post list0_post_exn { $1, $2 }
 ;
 
 list0_post_exn:

src/programs/TODO

 
-o bug in test-pgm-jcf: incr_fst
-
 o bug in test-pgm-jcf: scope
 
-o old(...) should not contain any local logical variable (let / match)
-
 o freshness analysis
 
 o no `old' in loop invariants
+o use of old in loop invariant should be reported as an error (correctly)
 
 o {| e with x1 = e1; ...; xn = en |}
 
@@ -21,8 +18,6 @@ o automatically add a label pre_f at entrance of each function f
   and then replace (old t) by (at t pre_f)
   (so that there is no more 'old' in the abstract syntax)
 
-o use of old in loop invariant should be reported as an error (correctly)
-
 o what about pervasives old, at, label, unit = ()
   in particular, how to prevent old and at from being used in programs?
   can we get rid of theories/programs.why?

src/programs/pgm_typing.ml

@@ -723,7 +723,9 @@ let iadd_local env x ty =
   in
   env, v
 
-let rec type_effect_term env { pp_loc = loc; pp_desc = d } = match d with
+let rec type_effect_term env t =
+  let loc = t.pp_loc in
+  match t.pp_desc with
   | PPvar (Qident x) when Mstr.mem x.id env.i_effects ->
       let v = Mstr.find x.id env.i_effects in
       v.vs_ty
@@ -735,6 +737,15 @@ let rec type_effect_term env { pp_loc = loc; pp_desc = d } = match d with
       with Not_found ->
         errorm ~loc "unbound symbol %a" print_qualid q
       end
+(***
+  | _ ->
+      let uc = effect_uc env.i_uc in
+      let t = Typing.type_term uc env.i_denv env.i_effects t in
+      begin match t.t_ty with
+        | Some ty -> ty
+        | None -> errorm ~loc "term expected"
+      end
+***)
   | _ ->
       errorm ~loc "unsupported effect syntax"
 

tests/test-pgm-jcf.mlw

@@ -16,13 +16,10 @@ module M
     r := 0
     { !r = 0 }
 
-  logic fst (x: ('a, 'b)) : 'a = let (x1, _) = x in x1
+  use import option.Option
 
-  (* BUG *)
-  let incr_fst (a: (ref int, int)) =
-    {}
-    let (r,_) = a in r := !r + 1
-    { let (x,_) = a in !x = (old !x) + 1 }
+  parameter clear (o : option (ref int)) :
+    {} unit writes (match o with Some r -> r end).contents { !r = 0 }
 
   let test4 () =
     let r = ref 0 in