[isabelle] Bug in Proofterm.all_oracles_of

[Dominique Unruh]

Hi,

this is the current implementation (Isabelle2018 stable) of all_oracles_of:

val all_oracles_of =
let
fun collect (PBody {oracles, thms, ...}) =
tap join_thms thms |> fold (fn (i, thm_node) => fn (x, seen) =>
if Inttab.defined seen i then (x, seen)
else
let
val body = Future.join (thm_node_body thm_node);
val (x', seen') = collect body (x, Inttab.update (i, ()) seen);
in (if null oracles then x' else oracles :: x', seen') end);
in fn body => unions_oracles (#1 (collect body ([], Inttab.empty))) end;

The function collect here collects oracles from two places: the argument
oracles, and the recursive collect calls on thms. However, the oracles from
the argument oracles are added inside the fold that iterates over (not yet
seen) thms. That is, if thms has more than one element, the same oracles
are added several times (not critical since they will be filtered later),
and if thms is empty (or all seen), then the oracles from the argument
oracles will never been added. (Or, to say it shorter: collect
(PBody{oracles, []}) does nothing.) The effect is that some oracles get
missed.

Here is a fixed function:

val all_oracles_of =
let
fun collect_inner thms =
tap join_thms thms |> fold (fn (i, thm_node) => fn (x, seen) =>
if Inttab.defined seen i then (x, seen)
else
let
val body = Future.join (thm_node_body thm_node);
val (x', seen') = collect body (x, Inttab.update (i, ())
seen);
in (x', seen') end)
and collect (PBody {oracles, thms, ...}) seen = case collect_inner thms
seen of (x,seen) =>
(if null oracles then x else oracles :: x, seen)
in fn body => unions_oracles (#1 (collect body ([], Inttab.empty))) end;


Best wishes,
Dominique.

[Makarius]

Post by Dominique Unruh
val all_oracles_of

I will look at this in further detail later.

Just note that whenever you find some odd function in the Isabelle
sources you need to figure out its overall context and status:

* by looking at its definition in ML

* by looking at its uses in application

* by looking through the documentation

Doing this briefly shows that all_oracles_of is an isolated point that
is not connected anywhere. Thus it has formally no meaning, and words
like "bug" or "fix" are even less meaningful than usual.

Moreover there is a more profound omission in the tracking of oracles in
Isabelle: certain kernel operations don't record anything. This is just
an incomplete implementation and TODO-item over many years. We don't
advertize oracle tracking anywhere -- and if some document claims that
we need to change the text to avoid confusion.


Makarius