Email Gateway (Aug 22 2022 at 14:41): Email Gateway (Aug 22 2022 at 14:41):From: Lars Hupel <hupel@in.tum.de>
Dear Florian,
you changed the representation of characters a while back, but it seems
like the Quickcheck setup is lacking a "full_exhaustive" instance.
The stupidest possible workaround is
quickcheck_generator char constructors: char_of_nat
... which I have just added locally to my theories.
Maybe we should think about a proper implementation.
Cheers
Lars
Email Gateway (Aug 22 2022 at 16:22):From: Lars Hupel <hupel@in.tum.de>
Dear list,
some time around 2016 the instance char :: full_exhaustive got commented
out and FIXME'd. I'm assuming this has something to do with the change
in char representation in HOL.
The big problem with the missing instance is that Auto Quickcheck
doesn't appear to trigger for goals containing strings, or containing
datatypes that contain strings. This in particular is annoying because
one always has to remember typing "quickcheck [random]".
Can this situation be rectified easily? Unfortunately I still don't know
how to properly write those instances, so if somebody could point me to
a similar example, I could implement it. Otherwise I'd like to defer to
Florian.
(The instance is still not present in the repository as of today.)
Cheers
Lars
Email Gateway (Aug 22 2022 at 16:23):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear Lars,
Here's my suggestion how to implement full_exhaustive for Chars with the constructors 0
and Char:
instantiation char :: full_exhaustive
begin
definition full_exhaustive_char
where
"full_exhaustive_char f i =
(if 0 < i then
case f (0, λ_ :: unit. Code_Evaluation.Const (STR ''Groups.zero_class.zero'')
(TYPEREP(char))) of
Some x ⇒ Some x
| None ⇒ full_exhaustive_class.full_exhaustive
(λ(num, t). f (Char num, λ_ :: unit. Code_Evaluation.Const (STR
''String.char'') TYPEREP(num ⇒ char)))
(min (i - 1) 8) (* generate at most 8 bits *)
else None)"
instance ..
end
Andreas
Email Gateway (Aug 22 2022 at 16:23):From: Lars Hupel <hupel@in.tum.de>
Dear Andreas,
Here's my suggestion how to implement full_exhaustive for Chars with the
constructors 0 and Char:
I have just tried that out:
lemma "list_all (λx. x ≠ 0) x ⟹ x ≠ [] ⟹ (x :: char list) = y"
quickcheck
Testing conjecture with Quickcheck-exhaustive...
exception TYPE raised (line 278 of "sign.ML"):
Type error in application: incompatible operand type
Operator: op # :: char ⇒ char list ⇒ char list
Operand: ??.String.char :: num ⇒ char
char ⇒ char list ⇒ char list
num ⇒ char
op #
??.String.char
Cheers
Lars
Email Gateway (Aug 22 2022 at 16:23):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear Lars,
Here's a version that should work:
definition full_exhaustive_char
where
"full_exhaustive_char f i =
(if 0 < i then
case f (0, λ_ :: unit. Code_Evaluation.Const (STR ''Groups.zero_class.zero'')
(TYPEREP(char))) of
Some x ⇒ Some x
| None ⇒ full_exhaustive_class.full_exhaustive
(λ(num, t). f (Char num, λ_ :: unit. Code_Evaluation.App (Code_Evaluation.Const
(STR ''String.Char'') TYPEREP(num ⇒ char)) (t ())))
(min (i - 1) 8) (* generate at most 8 bits *)
else None)"
instance ..
end
Andreas
Email Gateway (Aug 22 2022 at 16:23):From: Lars Hupel <hupel@in.tum.de>
Dear Andreas,
Here's a version that should work:
that appears to work. I've pushed it to testboard now. Thanks!
Lars
Email Gateway (Aug 22 2022 at 16:23):From: Lars Hupel <hupel@in.tum.de>
that appears to work. I've pushed it to testboard now. Thanks!
This is harder than it ought to be. This time we're being sabotaged by
"Code_Char":
theory Scratch
imports
"HOL-Library.Code_Char"
begin
lemma "(x::char list) = x"
quickcheck
Illegal character expression,
in equation full_exhaustive_char_inst.full_exhaustive_char
It looks like the code generator really does not like occurrences of
"Char x" where "x" is not a numeral.
Cheers
Lars
Email Gateway (Aug 22 2022 at 16:23):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Lars,
OK, here is version 3:
instantiation char :: full_exhaustive
begin
definition full_exhaustive_char
where
"full_exhaustive_char f i =
(if 0 < i then
case f (0, λ_ :: unit. Code_Evaluation.Const (STR ''Groups.zero_class.zero'')
(TYPEREP(char))) of
Some x ⇒ Some x
| None ⇒ full_exhaustive_class.full_exhaustive
(λ(num, t). f (char_of_nat (nat_of_num num), λ_ :: unit. Code_Evaluation.App
(Code_Evaluation.Const (STR ''String.Char'') TYPEREP(num ⇒ char)) (t ())))
(min (i - 1) 8) (* generate at most 8 bits *)
else None)"
instance ..
end
Andreas
Email Gateway (Aug 22 2022 at 16:24):From: Lars Hupel <hupel@in.tum.de>
OK, here is version 3:
This seems to have done the trick! See now 8fa951baba0d.
Cheers
Lars
Email Gateway (Aug 22 2022 at 16:24):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Lars,
Finally! Thanks for doing all the testing and integrating.
Andreas
Email Gateway (Aug 22 2022 at 16:25):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Andreas,
thanks for working that out. When working on characters, that slipped
somehow through my fingers.
Cheers,
Florian
signature.asc
Last updated: Nov 21 2024 at 12:39 UTC