Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Incompatibility between code generation, HOL-L...


view this post on Zulip Email Gateway (Feb 05 2021 at 13:21):

From: Dominique Unruh <unruh@ut.ee>
Hi,

when importing both HOL-Library.Numeral_Type (from Isabelle) and
Containers.Set_Impl (from AFP), then the code generation for computing
the cardinality of "UNIV::unit set" (which should be 1) produces
nonterminating code.

As shown in the attached theory, it defines a trivially diverging
recursive function "fun card A_ = card A_".

If only one of those two theories is included, the generated code
returns 1 immediately.

I don't understand where the recursive function comes from.

(I don't need a hotfix because this problem occurred only during
experimentation. But it might be good to understand where this comes
from and whether it relates to some deeper problem.)

Best wishes,
Dominique.
Test.thy

view this post on Zulip Email Gateway (Jun 30 2021 at 07:25):

From: Andreas Lochbihler <mail@andreas-lochbihler.de>
Hi Dominique,

Sorry for taking so long to respond.

HOL-Library.Numeral_Type imports HOL-Library.Cardinality, which installs some code setup
for card that is incompatible with the code setup from Containers.Set_Impl. Basically,
HOL-Library.Cardinality adds a code_unfold equation, which Containers.Set_Impl replaces
with another code_unfold equation. However, when both Numeral_Type and Set_Impl are
merged, the declarations from both Cardinality and Set_Impl become active again so that
the code generator now has two code_unfold equations that ultimately lead to this
situation. This is a known limitation of theory merges that is not easy to remedy. In
https://isabelle.in.tum.de/repos/isabelle/rev/93ba8e3fdcdf, I've now split off the code
generator setup from HOL-Library.Cardinality into a separate theory
HOL-Library.Code_Cardinality. This should avoid the problem with importing Numeral_Type
and Set_Impl.

Best,
Andreas


Last updated: Dec 05 2021 at 22:18 UTC