Email Gateway (Aug 22 2022 at 11:21): Email Gateway (Aug 22 2022 at 11:21):From: Walther Neuper <wneuper@ist.tugraz.at>
Given ...
theory Demo imports Main
begin
function gcd :: "int => int => int"
where "gcd m n = (if n = 0 then m else gcd n (m mod n))"
by auto
value "5 mod 3::int"
--{evaluates to "2" :: "int"}
value "gcd 123456 7890::int"
--{evaluates to "Demo.gcd 123456 7890" :: "int"}
end
... why does "gcd" not evaluate, although "mod" evaluates?
Walther
PS: And how find an answer to such a question myself?
Email Gateway (Aug 22 2022 at 11:21):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear Walther,
You have not yet proven that your function definition terminates. Therefore, the defining
equation (gcd.psimps) still carries the precondition that the function terminates. The
code generator cannot handle such preconditions, so these psimps equations are not
registered as code equations. Once you have proved termination, the function package
derives the unconditional equations gcd.simps from the conditional ones and registers them
with the code generator. Everything should work fine then.
You can find out what is happening by inspecting the code equations for gcd with the command
code_thms gcd
You will see that there are not equations registered.
Best,
Andreas
Last updated: Apr 19 2024 at 20:15 UTC