[isabelle-dev] Odd name space problem in quickcheck or codegen (due to change in typedef)

[Florian Haftmann]

(Sorry for the noise, the previous reply was a misguided)

The matter turned out quite simple: a literal type constructor name has
to be adjusted:

> diff -r eef7af6af2ce thys/Native_Word/Uint32.thy
> --- a/thys/Native_Word/Uint32.thy	Thu Mar 03 08:24:04 2016 +0100
> +++ b/thys/Native_Word/Uint32.thy	Thu Mar 03 13:13:04 2016 +0100
> @@ -300,7 +300,7 @@
>    defines "TR \<equiv> typerep.Typerep" and "bit0 \<equiv> STR ''Numeral_Type.bit0''" 
>    shows
>    "term_of_class.term_of x = 
> -   Code_Evaluation.App (Code_Evaluation.Const (STR ''Uint32.Abs_uint32'') (TR (STR ''fun'') [TR (STR ''Word.word'') [TR bit0 [TR bit0 [TR bit0 [TR bit0 [TR bit0 [TR (STR ''Numeral_Type.num1'') []]]]]]], TR (STR ''Uint32.uint32'') []]))
> +   Code_Evaluation.App (Code_Evaluation.Const (STR ''Uint32.uint32.Abs_uint32'') (TR (STR ''fun'') [TR (STR ''Word.word'') [TR bit0 [TR bit0 [TR bit0 [TR bit0 [TR bit0 [TR (STR ''Numeral_Type.num1'') []]]]]]], TR (STR ''Uint32.uint32'') []]))
>         (term_of_class.term_of (Rep_uint32' x))"
>  by(simp add: term_of_anything)

Maybe it is high time for me to provide input syntax CONSTANT ''…'' and
TYPE_CONSTRUCTOR ''…'' for safe references to named entities in HOL.

Hope this helps,
	Florian

Am 26.02.2016 um 22:57 schrieb Makarius:
> Included is an attempt to refine name qualification for typedef.
> 
> This leads to an odd name space problem in quickcheck or codegen, the
> effect can be seen in AFP/6e4cc77be100 in
> Native_Word/Native_Word_Test.thy line 81:
> 
>   lemma "x AND y = x OR (y :: uint32)"
>   quickcheck[random, expect=counterexample]
> 
>   Testing conjecture with Quickcheck-exhaustive...
>   exception TYPE raised (line 105 of "consts.ML"): Unknown constant:
>   "Uint32.Abs_uint32"
> 
> As can be seen here, the Abs_name of that type is
> "Uint32.uint32.Abs_uint32" and not "Uint32.Abs_uint32":
> 
>   ML ‹Typedef.get_info @{context} @{type_name uint32}›
> 
> 
> It is unclear to me, why quickcheck (or codegen) try this underqualified
> name. In principle, long names are never analyzed by tools, but it is
> well-known that quickcheck is a dark corner in that respect.
> 
> Is there an expert on that code who can disentangle that?
> 
> 
> The point is not just to get the above change through, but to sort out
> violations of Isabelle name space discipline. For more than 10 years, we
> are moving towards qualified theory names, and such incidents point at
> remaining problems.
> 
> 
>     Makarius
> 
> 
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
> 

-- 

PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 836 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20160303/cd80bb57/attachment.sig>