Mentions légales du service

Skip to content

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