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

[Makarius]

On Fri, 26 Feb 2016, Makarius wrote:

> 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}›

Included are exception debugger traces for the two quickcheck invocations 
in that spot (using 5dfcc9697f29 with the posted changeset e3040a415576).


 	Makarius
-------------- next part --------------
Exception trace - exception TYPE raised (line 105 of "consts.ML"): Unknown constant: "Uint32.Abs_uint32"
  Consts.the_entry (line 102 of "consts.ML")
  Consts.certify(4)cert (line 164 of "consts.ML")
  Sign.certify' (line 309 of "sign.ML")
  Thm.global_cterm_of (line 189 of "thm.ML")
  Library.apsnd (line 265 of "library.ML")
  Library.apfst (line 264 of "library.ML")
  Basics.|>> (line 57 of "General/basics.ML")
  Basics.#>> (line 64 of "General/basics.ML")
  Random_Engine.run (line 171 of "~~/src/HOL/Random.thy")
  Basics.|> (line 55 of "General/basics.ML")
  Random_Generators.compile_generator_expr_raw(2)single_tester (line 426 of "~~/src/HOL/Tools/Quickcheck/random_generators.ML")
  Random_Generators.compile_generator_expr_raw(2)iterate_and_collect (line 427 of "~~/src/HOL/Tools/Quickcheck/random_generators.ML")
  Random_Generators.compile_generator_expr_raw(2)iterate_and_collect (line 427 of "~~/src/HOL/Tools/Quickcheck/random_generators.ML")
  Random_Generators.compile_generator_expr_raw(2)iterate_and_collect (line 427 of "~~/src/HOL/Tools/Quickcheck/random_generators.ML")
  Random_Generators.compile_generator_expr_raw(2)(1)(1) (line 437 of "~~/src/HOL/Tools/Quickcheck/random_generators.ML")
  Random_Generators.compile_generator_expr(2)(1)(1) (line 465 of "~~/src/HOL/Tools/Quickcheck/random_generators.ML")
  Quickcheck_Common.test_term(6)with_size(3)time|report|result-(1) (line 102 of "~~/src/HOL/Tools/Quickcheck/quickcheck_common.ML")
  Timing.timing (line 68 of "General/timing.ML")
  Quickcheck_Common.cpu_time (line 77 of "~~/src/HOL/Tools/Quickcheck/quickcheck_common.ML")
  Quickcheck_Common.test_term(6)with_size (line 93 of "~~/src/HOL/Tools/Quickcheck/quickcheck_common.ML")
  Quickcheck_Common.test_term(6)with_size (line 93 of "~~/src/HOL/Tools/Quickcheck/quickcheck_common.ML")
  Quickcheck_Common.test_term(6)exec_time|response-(1) (line 132 of "~~/src/HOL/Tools/Quickcheck/quickcheck_common.ML")
  Timing.timing (line 68 of "General/timing.ML")
  Quickcheck_Common.cpu_time (line 77 of "~~/src/HOL/Tools/Quickcheck/quickcheck_common.ML")
  Quickcheck_Common.test_term (line 81 of "~~/src/HOL/Tools/Quickcheck/quickcheck_common.ML")
  Quickcheck_Common.generator_test_goal_terms(5)test_term' (line 339 of "~~/src/HOL/Tools/Quickcheck/quickcheck_common.ML")
  Quickcheck_Common.collect_results (line 320 of "~~/src/HOL/Tools/Quickcheck/quickcheck_common.ML")
  Quickcheck_Common.generator_test_goal_terms (line 331 of "~~/src/HOL/Tools/Quickcheck/quickcheck_common.ML")
  Quickcheck.test_terms(5)(1)(1) (line 302 of "~~/src/Tools/quickcheck.ML")
  Par_List.get_some(2)results-(1) (line 61 of "Concurrent/par_list.ML")
  Par_Exn.release_first (line 73 of "Concurrent/par_exn.ML")
  Par_List.get_some (line 56 of "Concurrent/par_list.ML")
  Quickcheck.test_terms(5)(1) (line 301 of "~~/src/Tools/quickcheck.ML")
  TimeLimit.timeLimit(3)(1)result-(1)(1) (line 28 of "Concurrent/time_limit.ML")
  TimeLimit.timeLimit(3)(1)result-(1) (line 28 of "Concurrent/time_limit.ML")
  TimeLimit.timeLimit(3)(1) (line 19 of "Concurrent/time_limit.ML")
  TimeLimit.timeLimit (line 18 of "Concurrent/time_limit.ML")
  Quickcheck.limit (line 283 of "~~/src/Tools/quickcheck.ML")
  Quickcheck.test_terms (line 296 of "~~/src/Tools/quickcheck.ML")
  Quickcheck.test_goal (line 339 of "~~/src/Tools/quickcheck.ML")
  Quickcheck.gen_quickcheck(3)(2) (line 505 of "~~/src/Tools/quickcheck.ML")
  Basics.|> (line 55 of "General/basics.ML")
  Quickcheck.gen_quickcheck (line 500 of "~~/src/Tools/quickcheck.ML")
  Quickcheck.quickcheck_cmd (line 513 of "~~/src/Tools/quickcheck.ML")
  Basics.tap(1)(1) (line 70 of "General/basics.ML") 
exception TYPE raised (line 105 of "consts.ML"): Unknown constant: "Uint32.Abs_uint32"
-------------- next part --------------
Exception trace - exception TYPE raised (line 105 of "consts.ML"): Unknown constant: "Uint32.Abs_uint32"
  Consts.the_entry (line 102 of "consts.ML")
  Consts.certify(4)cert (line 164 of "consts.ML")
  Sign.certify' (line 309 of "sign.ML")
  Thm.global_cterm_of (line 189 of "thm.ML")
  Library.apsnd (line 265 of "library.ML")
  Basics.|> (line 55 of "General/basics.ML")
  Exhaustive_Generators.compile_generator_expr_raw(2)compile-(1)(1)(1)(1)(1) (line 480 of "~~/src/HOL/Tools/Quickcheck/exhaustive_generators.ML")
  Exhaustive_Generators.compile_generator_expr_raw(2)(1)(1) (line 483 of "~~/src/HOL/Tools/Quickcheck/exhaustive_generators.ML")
  Exhaustive_Generators.compile_generator_expr(2)(1)(1) (line 491 of "~~/src/HOL/Tools/Quickcheck/exhaustive_generators.ML")
  Quickcheck_Common.test_term(6)with_size(3)time|report|result-(1) (line 102 of "~~/src/HOL/Tools/Quickcheck/quickcheck_common.ML")
  Timing.timing (line 68 of "General/timing.ML")
  Quickcheck_Common.cpu_time (line 77 of "~~/src/HOL/Tools/Quickcheck/quickcheck_common.ML")
  Quickcheck_Common.test_term(6)with_size (line 93 of "~~/src/HOL/Tools/Quickcheck/quickcheck_common.ML")
  Quickcheck_Common.test_term(6)with_size (line 93 of "~~/src/HOL/Tools/Quickcheck/quickcheck_common.ML")
  Quickcheck_Common.test_term(6)exec_time|response-(1) (line 132 of "~~/src/HOL/Tools/Quickcheck/quickcheck_common.ML")
  Timing.timing (line 68 of "General/timing.ML")
  Quickcheck_Common.cpu_time (line 77 of "~~/src/HOL/Tools/Quickcheck/quickcheck_common.ML")
  Quickcheck_Common.test_term (line 81 of "~~/src/HOL/Tools/Quickcheck/quickcheck_common.ML")
  Quickcheck_Common.generator_test_goal_terms(5)test_term' (line 339 of "~~/src/HOL/Tools/Quickcheck/quickcheck_common.ML")
  Quickcheck_Common.collect_results (line 320 of "~~/src/HOL/Tools/Quickcheck/quickcheck_common.ML")
  Quickcheck_Common.generator_test_goal_terms (line 331 of "~~/src/HOL/Tools/Quickcheck/quickcheck_common.ML")
  Quickcheck.test_terms(5)(1)(1) (line 302 of "~~/src/Tools/quickcheck.ML")
  Par_List.get_some(2)results-(1) (line 61 of "Concurrent/par_list.ML")
  Par_Exn.release_first (line 73 of "Concurrent/par_exn.ML")
  Par_List.get_some (line 56 of "Concurrent/par_list.ML")
  Quickcheck.test_terms(5)(1) (line 301 of "~~/src/Tools/quickcheck.ML")
  TimeLimit.timeLimit(3)(1)result-(1)(1) (line 28 of "Concurrent/time_limit.ML")
  TimeLimit.timeLimit(3)(1)result-(1) (line 28 of "Concurrent/time_limit.ML")
  TimeLimit.timeLimit(3)(1) (line 19 of "Concurrent/time_limit.ML")
  TimeLimit.timeLimit (line 18 of "Concurrent/time_limit.ML")
  Quickcheck.limit (line 283 of "~~/src/Tools/quickcheck.ML")
  Quickcheck.test_terms (line 296 of "~~/src/Tools/quickcheck.ML")
  Quickcheck.test_goal (line 339 of "~~/src/Tools/quickcheck.ML")
  Quickcheck.gen_quickcheck(3)(2) (line 505 of "~~/src/Tools/quickcheck.ML")
  Basics.|> (line 55 of "General/basics.ML")
  Quickcheck.gen_quickcheck (line 500 of "~~/src/Tools/quickcheck.ML")
  Quickcheck.quickcheck_cmd (line 513 of "~~/src/Tools/quickcheck.ML")
  Basics.tap(1)(1) (line 70 of "General/basics.ML") 
exception TYPE raised (line 105 of "consts.ML"): Unknown constant: "Uint32.Abs_uint32"