Failure in why3_open when using Isabelle
Reported by Grzegorz Fabiański: "In the code attached below, the filterExtendesSpec vc extracts correctly in the Isabelle, although using Isabelle on any goal after it results in an error on Isabelle's side during "why3_open"."
module BugInIsabelleExtraction
use list.List
use list.NumOcc
let rec function filter (p : 'a -> bool) (l : list 'a) : list 'a =
match l with
| Nil -> Nil
| Cons hd tl ->
let filteredRest = filter p tl in
if p hd then
Cons hd filteredRest
else
filteredRest
end
(*vc's of this are extracted correctly *)
let rec lemma filterExtendesSpec (x : 'a) (p : 'a -> bool) (l : list 'a) =
variant {l }
ensures { p x -> num_occ x (filter p l) = num_occ x l }
ensures { not p x -> num_occ x (filter p l) = 0 }
match l with
| Nil -> ()
| Cons hd tl ->
filterExtendesSpec x p tl
end
(* but any goal after this fail "why3_open" in Isabelle, even the simplest ones *)
goal test : 4=4
end