Cannot compile extracted program using `list.Nth.nth`
An occurrence of list.Nth.nth
is extracted to List.nth
, but the two functions have incompatible signatures:
- Why3
function nth (n: int) (l: list 'a) : option 'a
- OCaml
val nth : 'a list -> int -> 'a
Example Why3 (cat test.mlw
):
module Test
use option.Option
use list.List
use list.Nth
let f (l:list unit) (n:int) : option unit =
nth n l
end
Extracted OCaml (why3 extract -D ocaml64 -o test.ml test.mlw
):
let f (l: unit list) (n: Z.t) : unit option = List.nth n l
And OCaml complains (ocamlfind ocamlc -c -package zarith test.ml
):
File "test.ml", line 1, characters 55-56:
Error: This expression has type Z.t but an expression was expected of type
'a list
Reversing +6936e73c re-enables the Why3 implementation:
diff --git a/drivers/ocaml64.drv b/drivers/ocaml64.drv
index ad13e1318..3e6793064 100644
--- a/drivers/ocaml64.drv
+++ b/drivers/ocaml64.drv
@@ -52,10 +52,6 @@ theory list.Mem
syntax predicate mem "List.mem %1 %2"
end
-theory list.Nth
- syntax function nth "List.nth %1 %2"
-end
-
theory list.Append
syntax function (++) "List.append %1 %2"
end
In Why3-0.88.3 the equivalent program was extracted, and could be compiled:
(* This file has been generated from Why3 theory list.Nth *)
open Why3extract
let rec nth (n: Why3extract.Why3__BigInt.t) (l: 'a list) =
begin match l with
| [] -> None
| (x :: r) ->
if (Why3extract.Why3__BigInt.eq n Why3extract.Why3__BigInt.zero)
then
(Some x)
else
nth (Why3__BigInt.sub n Why3extract.Why3__BigInt.one) r end