Email Gateway (Aug 22 2022 at 20:38): Email Gateway (Aug 22 2022 at 20:38):From: Thomas Genet <thomas.genet@irisa.fr>
Dear Isabelle users,
I have a theory parameterized by a constant stack_lim which defines the
maximal stack_size of a given stack machine.
I defined:
consts
stack_lim::nat
I also have a function, eval, running the stack machine and using the
stack_size constant to check that no stack overflow has occured.
However, to test my eval function I'd like to run some small tests using
"value". The problem is that stack_lim is not defined (has no code
equations) and value fails.
Would it be possible to define "stack_lim" for a particular test.
Something like:
value "let stack_lim=4 in (eval ...)"
??
Thanks in advance and best regards,
Thomas
Email Gateway (Aug 22 2022 at 20:39):From: Tobias Nipkow <nipkow@in.tum.de>
This is not possible. You have to make it an explicit parameter of all relevant
functions or use a locale.
Tobias
smime.p7s
Email Gateway (Aug 22 2022 at 20:39):From: Thomas Genet <thomas.genet@irisa.fr>
Dear Tobias,
thank you for your answer.
Thomas
Email Gateway (Aug 22 2022 at 20:39):From: Dominique Unruh <unruh@ut.ee>
Hello,
I think there are two possibilities, but both I would recommend only for
experiments, not for the final theory (because of potential unsoundness).
Approach 1: Use code_printing (see Section 7.4 of the code generation
tutorial) and write something like: code_printing constant stack_size =>
(SML) "123".
Approach 2: Use an unproven fact. I.e., write lemma stack_size[code]:
"stack_size = 123" sorry . If you write this inside an "experiment
begin ... end" block, it should be safe. (You can also use
"axiomatization" instead of "lemma ... sorry" but that does not work in
an experiment block.)
Best wishes,
Dominique.
Email Gateway (Aug 22 2022 at 20:39):From: Thomas Genet <thomas.genet@irisa.fr>
Dear Dominique,
Thank you very much.
I tried to play with the second approach (that I prefer because of the
expected soundness of it (?)). The "lemma[code]" construct produces the
equation but not inside an experiment block.
theory temp
imports Main
begin
consts
stack_size::nat
fun f::"bool ⇒ nat"
where
"f _ = stack_size"
experiment
begin
lemma stack_size[code]: "stack_size=4"
sorry
value "f True" (* fails *)
end
lemma stack_size[code]: "stack_size=4"
sorry
value "f True" (* succeeds! *)
end
Email Gateway (Aug 22 2022 at 20:39):From: Dominique Unruh <unruh@ut.ee>
Then, unfortunately, I don't have any better ideas than using the unsafe
approach (possibly in a separate theory that cannot be included in other
theories by accident, this can be achieved by omitting the final "end"
in that theory). If it is for experiments only, this should work.
Best wishes,
Dominique.
Email Gateway (Aug 22 2022 at 20:39):From: Thomas Genet <thomas.genet@irisa.fr>
OK,
thank you very much. This will be very helpful anyway.
Best regards,
Thomas
Last updated: Apr 26 2024 at 01:06 UTC