extraction errors
Two extraction errors reported by Thomas Herzog.
Why3 platform, version 1.3.1 ocamlc --version: 4.10.0
(* repro.mlw *)
module ErrOneTime
use mach.onetime.OneTime
let ot_zero () : OneTime.t = zero ()
end
module ErrTuples
type pos = (unit, unit)
type range = Range pos pos
let merge (a b: range) : range
= let Range x y = a in
let Range w z = b in
Range x z
end
Extraction command: why3 extract -D ocaml64 repro.mlw > extracted.ml
(* extracted.ml *)
let ot_zero (_: unit) : int = 0 ()
(*
Error: This expression has type int
This is not a function; it cannot be applied.
*)
type pos = unit * unit
type range =
| Range of unit * unit * unit * unit
let merge (a: range) (b: range) : range =
let Range (x, y) = a in let Range (w, z) = b in Range (x, z)
(*
Error: The constructor Range expects 4 argument(s),
but is applied here to 2 argument(s)
*)
The mach.onetime.OneTime.zero
function should either be a constant
(like in mach.peano.Peano
) or the ocaml64 driver should emit (fun () -> 0)
for the zero
function
The issue with tuples is more interesting because nested tuples are "inlined", maybe the printer doesn't assign correct precedence to the tuples?
Both Range of (unit * unit) * (unit * unit)
and Range of pos * pos
work as expected.