Re: [isabelle] Quickcheck-Narrowing



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

On 17/02/14 14:31, Peter Lammich wrote:
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.

--
   Peter






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.