Am 01.07.2014 um 19:45 schrieb Makarius <makar...@sketis.net>: > * src/HOL/Tools/ATP/atp_problem_generate.ML > > Two occurrences that are not immediately clear. Looks like plain > structural equality could do the job.
Right. This looks like very minor optimizations. I'm taking them out (pushed to testboard already). > * src/HOL/Tools/BNF/bnf_def.ML > > fun maybe_restore lthy_old lthy = > lthy |> not (pointer_eq (lthy_old, lthy)) ? Local_Theory.restore; > > This looks odd. The normal idiom is to maintain an option value, to > say when a value remains explicitly unchanged (NONE). If this is too > awkward here, It is a bit awkward indeed. > one could try comparing the background theories via > Theory.eq_thy instead (which is strictly speaking just another > approximation, but a deterministic one). One could also try to > express the idea behind the uses of maybe_restore differently. I'll try something like this first. > * Metis has various optimizations using the "portable" alias > pointerEqual. Hard to say if there are potential problems coming from > it. A quick experiment with an always false predicate (which is a > correct approximation) makes metis very slow, but in most situations > it still terminates. (Shall we forward this to Joe Hurd? For the > Isabelle release, Metis is better left alone, though.) >From looking at the code, it looks to me like he's using "pointerEqual" only >as an overapproximation for equality, to speed up some data structure >operations. These uses do not worry me at all, and your experiments just >confirm what the code already strongly suggests. Jasmin _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
