extraction of records fields used as functions
The following is allowed by Why3:
use int.Int
type t = {
is_p: bool;
n: int;
}
let f (x: t) (pred: t -> bool) : int
=
if pred x then x.n else 0
let g () =
f { is_p = true; n = 42 } is_p
But then, when extracted using:
why3 extract -L . -D ocaml64 --recursive f.mlw -o f.ml
ocamlfind ocamlopt -package zarith -c -i f.ml
Here's the generated OCaml file:
type t = {
is_p: bool;
n: Z.t;
}
let f (x: t) (pred: t -> (bool)) : Z.t =
if pred x then begin x.n end else begin Z.zero end
let g (_: unit) : Z.t = f ({ is_p = true; n = (Z.of_string "42") }) is_p
The is_p
on the last line should be replaced by (fun el -> el.is_p)
, otherwise it fails with this error:
why3 extract -L . -D ocaml64 --recursive f.mlw -o f.ml
ocamlfind ocamlopt -package zarith -c -i f.ml
File "f.ml", line 9, characters 68-72:
Error: Unbound value is_p
make: *** [Makefile:4: extract] Error 2