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

[Florian Haftmann]

Hi 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.

strange indeed.  The code generator of course does a lot of name
substitution, but only towards exported code and not back to the logic.

Are you still close enough to obtain an ML traceback?  It will take some
time for me to analyze this.

Cheers,
	Florian

-- 

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/20160227/ec3da6e5/attachment.sig>