Skip to content
GitLab
Menu
Projects
Groups
Snippets
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
Why3
why3
Commits
f6150a86
Commit
f6150a86
authored
Apr 23, 2010
by
Andrei Paskevich
Browse files
rename Hashweak.add to Hashweak.set to stress its one-time semantic
parent
34d2825e
Changes
3
Hide whitespace changes
Inline
Side-by-side
src/core/trans.ml
View file @
f6150a86
...
...
@@ -54,7 +54,7 @@ let fold fn v =
let
h
=
WHtask
.
create
63
in
let
rewind
acc
task
=
let
acc
=
fn
task
acc
in
WHtask
.
add
h
task
acc
;
WHtask
.
set
h
task
acc
;
acc
in
let
current
task
=
...
...
src/util/hashweak.ml
View file @
f6150a86
...
...
@@ -38,12 +38,12 @@ module Make (S : Util.Tagged) = struct
let
mem_tag
h
=
Hashtbl
.
mem
h
.
table
let
find_tag
h
=
Hashtbl
.
find
h
.
table
let
add
_tag
h
t
e
v
=
let
set
_tag
h
t
e
v
=
assert
(
not
(
mem_tag
h
t
));
Gc
.
finalise
h
.
final
e
;
add_tag
h
t
v
let
add
h
e
=
add
_tag
h
(
S
.
tag
e
)
e
let
set
h
e
=
set
_tag
h
(
S
.
tag
e
)
e
let
mem
h
e
=
mem_tag
h
(
S
.
tag
e
)
let
find
h
e
=
find_tag
h
(
S
.
tag
e
)
...
...
@@ -53,7 +53,7 @@ module Make (S : Util.Tagged) = struct
try
find_tag
h
t
with
Not_found
->
let
v
=
fn
e
in
add
_tag
h
t
e
v
;
set
_tag
h
t
e
v
;
v
let
memoize_option
n
fn
=
...
...
src/util/hashweak.mli
View file @
f6150a86
...
...
@@ -31,8 +31,8 @@ module Make (S : Util.Tagged) : sig
val
mem
:
'
a
t
->
S
.
t
->
bool
(* test if a key is bound *)
val
add
:
'
a
t
->
S
.
t
->
'
a
->
unit
(* bind the key with the
value given
*)
val
set
:
'
a
t
->
S
.
t
->
'
a
->
unit
(* bind the key
_once_
with the
given value
*)
val
memoize
:
int
->
(
S
.
t
->
'
a
)
->
(
S
.
t
->
'
a
)
(* create a memoizing function *)
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment