[isabelle-dev] Odd name space problem in quickcheck or codegen (due to change in typedef)
Makarius
makarius at sketis.net
Fri Feb 26 22:57:55 CET 2016
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
-------------- next part --------------
# HG changeset patch
# User wenzelm
# Date 1456522724 -3600
# Fri Feb 26 22:38:44 2016 +0100
# Node ID e3040a415576794474b34caf3d4bda9c1321acbd
# Parent 6dce7bf7960becde9cb44ef3b5c109d26da16f21
take qualification of type name more seriously: derived consts and facts are qualified uniformly;
diff -r 6dce7bf7960b -r e3040a415576 src/HOL/Import/import_rule.ML
--- a/src/HOL/Import/import_rule.ML Fri Feb 26 15:49:35 2016 +0100
+++ b/src/HOL/Import/import_rule.ML Fri Feb 26 22:38:44 2016 +0100
@@ -219,8 +219,9 @@
val tfrees = Term.add_tfrees c []
val tnames = sort_strings (map fst tfrees)
val typedef_bindings =
- Typedef.make_morphisms (Binding.name tycname)
- (SOME (Binding.name rep_name, Binding.name abs_name))
+ {Rep_name = Binding.name rep_name,
+ Abs_name = Binding.name abs_name,
+ type_definition_name = Binding.name ("type_definition_" ^ tycname)}
val ((_, typedef_info), thy') =
Typedef.add_typedef_global {overloaded = false}
(Binding.name tycname, map (rpair dummyS) tnames, NoSyn) c
diff -r 6dce7bf7960b -r e3040a415576 src/HOL/Tools/hologic.ML
--- a/src/HOL/Tools/hologic.ML Fri Feb 26 15:49:35 2016 +0100
+++ b/src/HOL/Tools/hologic.ML Fri Feb 26 22:38:44 2016 +0100
@@ -644,9 +644,9 @@
val literalT = Type ("String.literal", []);
-fun mk_literal s = Const ("String.STR", stringT --> literalT)
+fun mk_literal s = Const ("String.literal.STR", stringT --> literalT)
$ mk_string s;
-fun dest_literal (Const ("String.STR", _) $ t) =
+fun dest_literal (Const ("String.literal.STR", _) $ t) =
dest_string t
| dest_literal t = raise TERM ("dest_literal", [t]);
diff -r 6dce7bf7960b -r e3040a415576 src/HOL/Tools/typedef.ML
--- a/src/HOL/Tools/typedef.ML Fri Feb 26 15:49:35 2016 +0100
+++ b/src/HOL/Tools/typedef.ML Fri Feb 26 22:38:44 2016 +0100
@@ -176,27 +176,30 @@
type bindings = {Rep_name: binding, Abs_name: binding, type_definition_name: binding};
+fun prefix_binding prfx name =
+ Binding.qualified false (prfx ^ Binding.name_of name) name;
+
+fun qualify_binding name = Binding.qualify false (Binding.name_of name);
+
fun default_bindings name =
- {Rep_name = Binding.prefix_name "Rep_" name,
- Abs_name = Binding.prefix_name "Abs_" name,
- type_definition_name = Binding.prefix_name "type_definition_" name};
+ {Rep_name = prefix_binding "Rep_" name,
+ Abs_name = prefix_binding "Abs_" name,
+ type_definition_name = prefix_binding "type_definition_" name};
fun make_bindings name NONE = default_bindings name
| make_bindings _ (SOME bindings) = bindings;
fun make_morphisms name NONE = default_bindings name
| make_morphisms name (SOME (Rep_name, Abs_name)) =
- {Rep_name = Rep_name, Abs_name = Abs_name,
- type_definition_name = #type_definition_name (default_bindings name)};
+ {Rep_name = qualify_binding name Rep_name,
+ Abs_name = qualify_binding name Abs_name,
+ type_definition_name = #type_definition_name (default_bindings name)};
(* prepare_typedef *)
fun prepare_typedef prep_term overloaded (name, raw_args, mx) raw_set opt_bindings lthy =
let
- val bname = Binding.name_of name;
-
-
(* rhs *)
val tmp_ctxt = lthy |> fold (Variable.declare_typ o TFree) raw_args;
@@ -207,6 +210,7 @@
val oldT = HOLogic.dest_setT setT handle TYPE _ =>
error ("Not a set type: " ^ quote (Syntax.string_of_typ lthy setT));
+ val bname = Binding.name_of name;
val goal = mk_inhabited set;
val goal_pat = mk_inhabited (Var (the_default (bname, 0) (Lexicon.read_variable bname), setT));
@@ -235,8 +239,8 @@
(* result *)
- fun note_qualify ((b, atts), th) =
- Local_Theory.note ((Binding.qualify false bname b, map (Attrib.internal o K) atts), [th])
+ fun note ((b, atts), th) =
+ Local_Theory.note ((b, map (Attrib.internal o K) atts), [th])
#>> (fn (_, [th']) => th');
fun typedef_result inhabited lthy1 =
@@ -246,25 +250,25 @@
val (((((((((((_, [type_definition]), Rep), Rep_inverse), Abs_inverse), Rep_inject),
Abs_inject), Rep_cases), Abs_cases), Rep_induct), Abs_induct), lthy2) = lthy1
|> Local_Theory.note ((type_definition_name, []), [typedef'])
- ||>> note_qualify ((Rep_name, []), make @{thm type_definition.Rep})
- ||>> note_qualify ((Binding.suffix_name "_inverse" Rep_name, []),
+ ||>> note ((Rep_name, []), make @{thm type_definition.Rep})
+ ||>> note ((Binding.suffix_name "_inverse" Rep_name, []),
make @{thm type_definition.Rep_inverse})
- ||>> note_qualify ((Binding.suffix_name "_inverse" Abs_name, []),
+ ||>> note ((Binding.suffix_name "_inverse" Abs_name, []),
make @{thm type_definition.Abs_inverse})
- ||>> note_qualify ((Binding.suffix_name "_inject" Rep_name, []),
+ ||>> note ((Binding.suffix_name "_inject" Rep_name, []),
make @{thm type_definition.Rep_inject})
- ||>> note_qualify ((Binding.suffix_name "_inject" Abs_name, []),
+ ||>> note ((Binding.suffix_name "_inject" Abs_name, []),
make @{thm type_definition.Abs_inject})
- ||>> note_qualify ((Binding.suffix_name "_cases" Rep_name,
+ ||>> note ((Binding.suffix_name "_cases" Rep_name,
[Rule_Cases.case_names [Binding.name_of Rep_name], Induct.cases_pred full_name]),
make @{thm type_definition.Rep_cases})
- ||>> note_qualify ((Binding.suffix_name "_cases" Abs_name,
+ ||>> note ((Binding.suffix_name "_cases" Abs_name,
[Rule_Cases.case_names [Binding.name_of Abs_name], Induct.cases_type full_name]),
make @{thm type_definition.Abs_cases})
- ||>> note_qualify ((Binding.suffix_name "_induct" Rep_name,
+ ||>> note ((Binding.suffix_name "_induct" Rep_name,
[Rule_Cases.case_names [Binding.name_of Rep_name], Induct.induct_pred full_name]),
make @{thm type_definition.Rep_induct})
- ||>> note_qualify ((Binding.suffix_name "_induct" Abs_name,
+ ||>> note ((Binding.suffix_name "_induct" Abs_name,
[Rule_Cases.case_names [Binding.name_of Abs_name], Induct.induct_type full_name]),
make @{thm type_definition.Abs_induct});
More information about the isabelle-dev
mailing list