Commit 0d728c6c authored by Jacques-Pascal Deplaix's avatar Jacques-Pascal Deplaix
Browse files

Add Array.sub

parent 411ccd95
......@@ -71,6 +71,15 @@ let append a1 a2 =
end
(* Remark: might be optimized by using a sub-array to avoid initialization *)
external sub : 'a array -> int -> int -> 'a array = "caml_array_sub"
(*
(* NOTE: Improved original code below *)
(* TODO: Do we want to expose unsafe_sub ? *)
let sub a ofs len =
assert (not (ofs < 0 || len < 0 || ofs > length a - len));
unsafe_sub a ofs len
*)
let iter f a =
for i = 0 to pred (length a) do
f (get a i)
......
......@@ -64,6 +64,20 @@ Parameter set_spec : curried 2%nat set /\
Hint Extern 1 (RegisterSpec set) => Provide set_spec.
(* NOTE: Check if correct *)
Parameter sub_spec : curried 3%nat sub /\
forall `{Inhab A} (L : list A) (a : loc) (ofs len : int),
0 <= ofs ->
ofs <= len ->
len <= LibListZ.length L ->
app_keep sub [a ofs len]
(a ~> Array L)
(fun a' => Hexists L',
a' ~> Array L' \*
\[LibListZ.length L' = len - ofs] \*
\[forall i, ofs <= i < len -> L'[i] = L[i]]).
Hint Extern 1 (RegisterSpec sub) => Provide sub_spec.
Notation "'App'' r `[ i ]" := (App get r i;)
(at level 69, r at level 0, no associativity,
......
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