Email Gateway (Aug 19 2022 at 13:36): Email Gateway (Aug 19 2022 at 13:36):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Peter,
You can still install custom narrowing generators for types by using the functions that
are only hidden openly. I've added narrowing generators for the Coinductive entry, but I
am unable to push. I repeat them here such that you can take some inspiration from them:
instantiation llist :: (narrowing) narrowing begin
function narrowing_llist where
"narrowing_llist n = Quickcheck_Narrowing.sum
(Quickcheck_Narrowing.cons LNil)
(Quickcheck_Narrowing.apply (Quickcheck_Narrowing.apply
(Quickcheck_Narrowing.cons LCons) narrowing) narrowing_llist)
n"
by pat_completeness simp
termination by(relation "measure nat_of_integer")(simp_all, transfer, simp)
instance ..
end
Regarding Native_Word, it is important to think about the generation strategy. The
narrowing engine calls the generators whenever it encounters an variable in a goal in
order to refine it. For datatypes, the generator returns a list of refined terms such as
the constructors of the datatype. The generator for ints, however, just returns the
numbers around 0. A first attempt for words could be to produce the first few values of
the word, but I would expect better results if it also generates larger word values. In
principle, one can consider a word as a list of bits of fixed length and have the
generator behave similarly to the one for list.
Since Native_Word has a custom serialisation, you also have to provide the partial_term_of
instantiation. I have not yet figured out how it interacts with the generators but it
looks as if they must work together. Lukas should know more.
Best,
Andreas
Email Gateway (Aug 19 2022 at 13:36):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Peter,
Here are a few more thoughts on this. Refinement works for datatypes, because the
functions on them are defined by pattern-matching. That is, when a variable is refined to
the list of possible constructors, evaluation can continue and might even report a
definitive value without examining the data structure any further. Since Native_Word maps
the word types to atomic types in the target language, and operations to built-in
operations which are usually strict, we cannot exploit incremental refinements here,
because we cannot symbolically represent such words. Therefore, it is probably best to
just enumerate values, maybe in some clever way. Narrowing in Quickcheck adapts
LazySmallCheck from Haskell (http://hackage.haskell.org/package/lazysmallcheck), so I had
a look there. Its generators for the primitive Haskell types also just enumerates some values.
Andreas
Email Gateway (Aug 19 2022 at 13:51):From: Peter Lammich <lammich@in.tum.de>
Hi List.
Is there a way to extend quickcheck-narrowing for your own types,
for example the native-word types from the Native_Word library.
In attempting so, I had trouble to even define the instantiation, as all
the required types and constants are hidden with a hide_XXX command at
the end of Quickcheck_Narrowing.thy. The proof obligation reads like
instantiation
uint32 :: narrowing
narrowing_uint32 == narrowing ::
integer \<Rightarrow> uint32 ??.Quickcheck_Narrowing.narrowing_cons
But I cannot see the type "??.Quickcheck_Narrowing.narrowing_cons" any
more.
Last updated: Apr 25 2024 at 12:23 UTC