cleaning up

parent bda9f907
......@@ -63,12 +63,8 @@ module Hashtbl
/\
forall k': key. k' <> k -> h[k'] = (old h)[k'] }
val length (h: t 'a) :
{}
int reads h
{} (* = the number of distinct keys *)
(* TODO
- val length: t 'a -> int (the number of distinct key)
- val iter : ('a -> 'b -> unit) -> ('a, 'b) t -> unit
- val fold : ('a -> 'b -> 'c -> 'c) -> ('a, 'b) t -> 'c -> 'c
*)
......
......@@ -9,38 +9,38 @@ module Queue
type t 'a model {| mutable elts: list 'a |}
val create : unit -> {} t 'a { result.elts = Nil }
val create: unit -> {} t 'a { result.elts = Nil }
val push :
x:'a -> s:t 'a -> {} unit writes s { s.elts = old s.elts ++ Cons x Nil }
val push:
x: 'a -> q: t 'a -> {} unit writes q { q.elts = old q.elts ++ Cons x Nil }
exception Empty
val pop :
s:t 'a ->
val pop:
q: t 'a ->
{}
'a
writes s raises Empty
{ match old s.elts with Nil -> false
| Cons x t -> result = x /\ s.elts = t end }
| Empty -> { s.elts = old s.elts = Nil }
writes q raises Empty
{ match old q.elts with Nil -> false
| Cons x t -> result = x /\ q.elts = t end }
| Empty -> { q.elts = old q.elts = Nil }
val top :
s:t 'a ->
val top:
q: t 'a ->
{}
'a
reads s raises Empty
{ match s.elts with Nil -> false | Cons x _ -> result = x end }
| Empty -> { s.elts = Nil }
reads q raises Empty
{ match q.elts with Nil -> false | Cons x _ -> result = x end }
| Empty -> { q.elts = Nil }
val clear : s:t 'a -> {} unit writes s { s.elts = Nil }
val clear: q: t 'a -> {} unit writes q {q.elts = Nil }
val copy : s:t 'a -> {} t 'a { result = s }
val copy: q: t 'a -> {} t 'a { result = q }
val is_empty :
s:t 'a -> {} bool reads s { result=True <-> s.elts = Nil }
val is_empty:
q: t 'a -> {} bool reads q { result=True <-> q.elts = Nil }
val length : s:t 'a -> {} int reads s { result = length s.elts }
val length: q: t 'a -> {} int reads q { result = length q.elts }
end
......
(* References *)
(* References.
A mutable variable, or ``reference'' in ML terminology, is simply a
record with a single mutable field 'contents'.
Creation, access, and assignment are provided as 'ref', prefix '!', and
infix ':=', respectively.
*)
module Ref
......@@ -6,29 +14,27 @@ module Ref
function (!) (x: ref 'a) : 'a = x.contents
(* val ref : v:'a -> {} ref 'a { result = {| contents = v |} } *)
let ref (v: 'a) = {} {| contents = v |} { result = {| contents = v |} }
(* val (!) : r:ref 'a -> {} 'a reads r { result = !r } *)
let (!) (r:ref 'a) = {} r.contents { result = !r }
(* val (:=) : r:ref 'a -> v:'a -> {} unit writes r { !r = v } *)
let (:=) (r:ref 'a) (v:'a) = {} r.contents <- v { !r = v }
end
(* Module Refint adds a few operations specific to integer references. *)
module Refint
use export int.Int
use export module Ref
(* val incr : r:ref int -> {} unit writes r { !r = old !r + 1 } *)
let incr (r: ref int) = {} r := !r + 1 { !r = old !r + 1 }
(* val decr : r:ref int -> {} unit writes r { !r = old !r - 1 } *)
let decr (r: ref int) = {} r := !r - 1 { !r = old !r - 1 }
let (+=) (r: ref int) (v: int) = {} r := !r + v { !r = old !r + v }
let (+=) (r: ref int) (v: int) = {} r := !r + v { !r = old !r + v }
let (-=) (r: ref int) (v: int) = {} r := !r - v { !r = old !r - v }
let ( *= ) (r: ref int) (v: int) = {} r := !r * v { !r = old !r * v }
end
......
......@@ -8,15 +8,15 @@ module Stack
type t 'a model {| mutable elts: list 'a |}
val create : unit -> {} t 'a { result.elts = Nil }
val create: unit -> {} t 'a { result.elts = Nil }
val push :
x:'a -> s:t 'a -> {} unit writes s { s.elts = Cons x (old s.elts) }
val push:
x: 'a -> s: t 'a -> {} unit writes s { s.elts = Cons x (old s.elts) }
exception Empty
val pop :
s:t 'a ->
val pop:
s: t 'a ->
{}
'a
writes s raises Empty
......@@ -24,22 +24,22 @@ module Stack
| Cons x t -> result = x /\ s.elts = t end }
| Empty -> { s.elts = old s.elts = Nil }
val top :
s:t 'a ->
val top:
s: t 'a ->
{}
'a
reads s raises Empty
{ match s.elts with Nil -> false | Cons x _ -> result = x end }
| Empty -> { s.elts = Nil }
val clear : s:t 'a -> {} unit writes s { s.elts = Nil }
val clear: s: t 'a -> {} unit writes s { s.elts = Nil }
val copy : s:t 'a -> {} t 'a { result = s }
val copy: s: t 'a -> {} t 'a { result = s }
val is_empty :
s:t 'a -> {} bool reads s { result=True <-> s.elts = Nil }
val is_empty:
s: t 'a -> {} bool reads s { result=True <-> s.elts = Nil }
val length : s:t 'a -> {} int reads s { result = length s.elts }
val length: s: t 'a -> {} int reads s { result = length s.elts }
end
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment