[extraction] extracts modules mach.array.ArrayXX

parent 33452dfb
......@@ -39,7 +39,7 @@ as follows:
result: Tuple2(45, 10)
globals:
\end{verbatim}
We get the excepted output, namely the pair \texttt{(45, 10)}.
We get the expected output, namely the pair \texttt{(45, 10)}.
\section{Compiling \whyml to OCaml}
\index{OCaml}\index{extraction}
......@@ -65,10 +65,10 @@ among which we find a file \texttt{maxsum\_\_MaxAndSum.ml} containing
the OCaml code for functions \texttt{max\_sum} and \texttt{test}.
To compile it, we create a file \texttt{main.ml}
containing a call to \texttt{test}, that is for example
containing a call to \texttt{test}, that is, for example,
\begin{whycode}
let (s,m) = test () in
Format.printf "sum=%s, max=%s@."
Format.printf "sum=%s, max=%s@."
(Why3__BigInt.to_string s) (Why3__BigInt.to_string m)
\end{whycode}
and we pass both files \texttt{maxsum\_\_MaxAndSum.ml} and
......@@ -85,6 +85,12 @@ Depending on the way \why was installed, it depends either on library
assumed the latter. It is likely that additional options \texttt{-I}
must be passed to the OCaml compiler for libraries
\texttt{zarith.cmxa} and \texttt{why3extract.cmxa} to be found.
For instance, it could be
\begin{verbatim}
> ocamlopt -I `ocamlfind query zarith` zarith.cmxa \
-I `why3 --print-libdir`/why3 why3extract.cmxa \
...
\end{verbatim}
%%% Local Variables:
......
......@@ -215,6 +215,3 @@ module mach.array.Array31
syntax val self_blit "Array.blit"
end
(* TODO
- mach.array.Array32 -> Bigarray sur 32-bit / Array sur 64-bit ?
*)
(* OCaml driver for 32-bit architecture *)
(* OCaml driver for 32-bit architecture
Note: module mach.int.Array32 is currently unsupported on a 32-bit OCaml *)
import "ocaml-gen.drv"
......
......@@ -83,3 +83,34 @@ module mach.int.Int64
syntax val (>) "(>)"
end
(* arrays *)
module mach.array.Array32
syntax type array "(%1 array)"
syntax val make "Array.make"
syntax val ([]) "Array.get"
syntax val ([]<-) "Array.set"
syntax val length "Array.length"
syntax val append "Array.append"
syntax val sub "Array.sub"
syntax val copy "Array.copy"
syntax val fill "Array.fill"
syntax val blit "Array.blit"
syntax val self_blit "Array.blit"
end
module mach.array.Array63
syntax type array "(%1 array)"
syntax val make "Array.make"
syntax val ([]) "Array.get"
syntax val ([]<-) "Array.set"
syntax val length "Array.length"
syntax val append "Array.append"
syntax val sub "Array.sub"
syntax val copy "Array.copy"
syntax val fill "Array.fill"
syntax val blit "Array.blit"
syntax val self_blit "Array.blit"
end
......@@ -238,7 +238,123 @@ module Array31
end
(** {2 Arrays with 63-bit indices} *)
module Array63
use import mach.int.Int63
use import map.Map as M
type array 'a model { length: int63; mutable elts: map int 'a }
invariant { 0 <= to_int self.length }
function get (a: array ~'a) (i: int) : 'a = M.get a.elts i
function set (a: array ~'a) (i: int) (v: 'a) : array 'a =
{ a with elts = M.set a.elts i v }
(** syntactic sugar *)
function ([]) (a: array 'a) (i: int) : 'a = get a i
function ([<-]) (a: array 'a) (i: int) (v: 'a) : array 'a = set a i v
val ([]) (a: array ~'a) (i: int63) : 'a
requires { 0 <= to_int i < to_int a.length }
ensures { result = a[to_int i] }
val ([]<-) (a: array ~'a) (i: int63) (v: 'a) : unit writes {a}
requires { 0 <= to_int i < to_int a.length }
ensures { a.elts = M.set (old a.elts) (to_int i) v }
val length (a: array ~'a) : int63 ensures { result = a.length }
(** unsafe get/set operations with no precondition *)
exception OutOfBounds
let defensive_get (a: array 'a) (i: int63)
ensures { 0 <= to_int i < to_int a.length }
ensures { result = a[to_int i] }
raises { OutOfBounds -> to_int i < 0 \/ to_int i >= to_int a.length }
= if i < of_int 0 || i >= length a then raise OutOfBounds;
a[i]
let defensive_set (a: array 'a) (i: int63) (v: 'a)
ensures { 0 <= to_int i < to_int a.length }
ensures { a = (old a)[to_int i <- v] }
raises { OutOfBounds -> to_int i < 0 \/ to_int i >= to_int a.length }
= if i < of_int 0 || i >= length a then raise OutOfBounds;
a[i] <- v
function make (n: int63) (v: ~'a) : array 'a =
{ length = n; elts = M.const v }
val make (n: int63) (v: ~'a) : array 'a
requires { to_int n >= 0 }
ensures { result = make n v }
val append (a1: array ~'a) (a2: array 'a) : array 'a
ensures { to_int result.length = to_int a1.length + to_int a2.length }
ensures { forall i:int. 0 <= i < to_int a1.length -> result[i] = a1[i] }
ensures { forall i:int. 0 <= i < to_int a2.length ->
result[to_int a1.length + i] = a2[i] }
val sub (a: array ~'a) (ofs: int63) (len: int63) : array 'a
requires { 0 <= to_int ofs /\ 0 <= to_int len }
requires { to_int ofs + to_int len <= to_int a.length }
ensures { result.length = len }
ensures { forall i:int. 0 <= i < to_int len ->
result[i] = a[to_int ofs + i] }
val copy (a: array ~'a) : array 'a
ensures { result.length = a.length }
ensures { forall i:int. 0 <= i < to_int result.length -> result[i] = a[i] }
let fill (a: array ~'a) (ofs: int63) (len: int63) (v: 'a)
requires { 0 <= to_int ofs /\ 0 <= to_int len }
requires { to_int ofs + to_int len <= to_int a.length }
ensures { forall i:int.
(0 <= i < to_int ofs \/
to_int ofs + to_int len <= i < to_int a.length) -> a[i] = (old a)[i] }
ensures { forall i:int. to_int ofs <= i < to_int ofs + to_int len ->
a[i] = v }
= 'Init:
for k = 0 to Int.(-) (to_int len) 1 do (* FIXME: for loop on int63 *)
invariant { forall i:int.
(0 <= i < to_int ofs \/
to_int ofs + to_int len <= i < to_int a.length) ->
a[i] = (at a 'Init)[i] }
invariant { forall i:int. to_int ofs <= i < to_int ofs + k -> a[i] = v }
let k = of_int k in
a[ofs + k] <- v
done
val blit (a1: array ~'a) (ofs1: int63)
(a2: array 'a) (ofs2: int63) (len: int63) : unit writes {a2}
requires { 0 <= to_int ofs1 /\ 0 <= to_int len }
requires { to_int ofs1 + to_int len <= to_int a1.length }
requires { 0 <= to_int ofs2 /\
to_int ofs2 + to_int len <= to_int a2.length }
ensures { forall i:int.
(0 <= i < to_int ofs2 \/
to_int ofs2 + to_int len <= i < to_int a2.length) ->
a2[i] = (old a2)[i] }
ensures { forall i:int.
to_int ofs2 <= i < to_int ofs2 + to_int len ->
a2[i] = a1[to_int ofs1 + i - to_int ofs2] }
val self_blit (a: array ~'a) (ofs1: int63) (ofs2: int63) (len: int63) : unit
writes {a}
requires { 0 <= to_int ofs1 /\ 0 <= to_int len /\
to_int ofs1 + to_int len <= to_int a.length }
requires { 0 <= to_int ofs2 /\ to_int ofs2 + to_int len <= to_int a.length }
ensures { forall i:int.
(0 <= i < to_int ofs2 \/
to_int ofs2 + to_int len <= i < to_int a.length) -> a[i] = (old a)[i] }
ensures { forall i:int.
to_int ofs2 <= i < to_int ofs2 + to_int len ->
a[i] = (old a)[to_int ofs1 + i - to_int ofs2] }
end
(* TODO
- Array63
- Array64
- Array64 ?
*)
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