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
POTTIER Francois
menhir
Commits
af5963f0
Commit
af5963f0
authored
Jan 08, 2015
by
POTTIER Francois
Browse files
New functions _via in LinearizedArray.
parent
9980f815
Changes
2
Hide whitespace changes
Inline
Side-by-side
src/LinearizedArray.ml
View file @
af5963f0
...
...
@@ -38,20 +38,30 @@ let length ((_, entry) : 'a t) : int =
let
row_length
((
_
,
entry
)
:
'
a
t
)
i
:
int
=
entry
.
(
i
+
1
)
-
entry
.
(
i
)
let
row_length_via
get_entry
i
=
get_entry
(
i
+
1
)
-
get_entry
i
let
read
((
data
,
entry
)
as
la
:
'
a
t
)
i
j
:
'
a
=
assert
(
0
<=
j
&&
j
<
row_length
la
i
);
data
.
(
entry
.
(
i
)
+
j
)
let
read_via
get_data
get_entry
i
j
=
assert
(
0
<=
j
&&
j
<
row_length_via
get_entry
i
);
get_data
(
get_entry
i
+
j
)
let
write
((
data
,
entry
)
as
la
:
'
a
t
)
i
j
(
v
:
'
a
)
:
unit
=
assert
(
0
<=
j
&&
j
<
row_length
la
i
);
data
.
(
entry
.
(
i
)
+
j
)
<-
v
let
rec
read_interval
data
i
j
=
let
rec
read_interval
_via
get_
data
i
j
=
if
i
=
j
then
[]
else
data
.
(
i
)
::
read_interval
data
(
i
+
1
)
j
get_data
i
::
read_interval_via
get_data
(
i
+
1
)
j
let
read_row_via
get_data
get_entry
i
=
read_interval_via
get_data
(
get_entry
i
)
(
get_entry
(
i
+
1
))
let
read_row
((
data
,
entry
)
:
'
a
t
)
i
:
'
a
list
=
read_
interval
data
entry
.
(
i
)
entry
.
(
i
+
1
)
read_
row_via
(
Array
.
get
data
)
(
Array
.
get
entry
)
i
src/LinearizedArray.mli
View file @
af5963f0
...
...
@@ -36,3 +36,24 @@ val row_length: 'a t -> int -> int
val
read_row
:
'
a
t
->
int
->
'
a
list
(* The following variants read the linearized array via accessors
[get_data : int -> 'a] and [get_entry : int -> int]. *)
val
row_length_via
:
(* get_entry: *)
(
int
->
int
)
->
(* i: *)
int
->
int
val
read_via
:
(* get_data: *)
(
int
->
'
a
)
->
(* get_entry: *)
(
int
->
int
)
->
(* i: *)
int
->
(* j: *)
int
->
'
a
val
read_row_via
:
(* get_data: *)
(
int
->
'
a
)
->
(* get_entry: *)
(
int
->
int
)
->
(* i: *)
int
->
'
a
list
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