Email Gateway (Aug 22 2022 at 15:49): Email Gateway (Aug 22 2022 at 15:49):From: Mark Wassell <mpwassell@gmail.com>
Hello,
In Predicate_Compile_Examples/Examples.thy there are the following uses of
code_pred and value:
code_pred [inductify] S⇩1p .
code_pred [random_dseq inductify] S⇩1p .
values [random_dseq 5, 5, 5] 5 "{x. S⇩1p x}"
Is there any detailed documentation or description of what the compilation
options such as inductify and random_dseq do? Or will I need to read the ML
?
What I can tell from the equation lines is that these options result in
different code equations with the latter possibly enabling random
generation of the members of the inductive set in a quickcheck like manner.
Cheers
Mark
Email Gateway (Aug 22 2022 at 15:49):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear Mark,
Unfortunately, I'm not aware of any detailed documentation for these options. The option
inductify tries to infer intro and elim rules for constants that have not been defined
with (co)inductive and then call the predicate compiler on those such that they can be
part of the mode inference game. This is particularly useful if you have defined a
predicate using a first-order formula with quantifiers and want to execute it. You might
find something on this and random_dseq in Lukas Bulwahn's PhD thesis.
What do you need these options for?
Most of these random generators for quickcheck are not used much because quickcheck has
been configured to use only exhaustive testing by default.
Cheers,
Andreas
Email Gateway (Aug 22 2022 at 15:49):From: Mark Wassell <mpwassell@gmail.com>
Andreas,
Thank you for your reply.
My general interest is understand in detail how the code generation for
inductive predicates works. My specific interest in random_dseq is in being
able to randomly generate terms in a language from its inductive definition
(for example terms of a particular type) and to do so in a manner where I
have some control over the distribution. I was wondering if the options to
random_dseq in the values statement provided this control or similar.
I have read "Code Generation from Inductive Predicates in Isabelle/HOL"
March 2009, Lukas Bulwahn. Is this the PhD thesis that you refer to?
Cheers
Mark
Email Gateway (Aug 22 2022 at 15:49):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear Mark,
On 31/07/17 11:11, Mark Wassell wrote:
My general interest is understand in detail how the code generation for inductive
predicates works. My specific interest in random_dseq is in being able to randomly
generate terms in a language from its inductive definition (for example terms of a
particular type) and to do so in a manner where I have some control over the distribution.
I was wondering if the options to random_dseq in the values statement provided this
control or similar.Sorry, I cannot help you here. I've never used those smart generators.
I have read "Code Generation from Inductive Predicates in Isabelle/HOL" March 2009, Lukas
Bulwahn. Is this the PhD thesis that you refer to?
No. This is the Lukas' Master's thesis on the predicate compiler. It contains a few more
details about the predicate compiler, but not the integration with quickcheck. Lukas' PhD
thesis is available here:
https://mediatum.ub.tum.de/node?id=1115870
All the best,
Andreas
Last updated: Apr 26 2024 at 12:28 UTC