--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Sat Mar 13 14:43:04 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Sat Mar 13 14:44:47 2010 +0100
@@ -560,14 +560,15 @@
set_def = NONE, prop_of_Rep = @{prop "Rep_Frac x \<in> Frac"}
|> Logic.varify,
set_name = @{const_name Frac}, Abs_inverse = NONE, Rep_inverse = NONE}
- else case Typedef.get_info thy s of
- SOME {abs_type, rep_type, Abs_name, Rep_name, set_def, Rep, Abs_inverse,
- Rep_inverse, ...} =>
+ else case Typedef.get_info_global thy s of
+ (* FIXME handle multiple typedef interpretations (!??) *)
+ [{abs_type, rep_type, Abs_name, Rep_name, set_def, Rep, Abs_inverse,
+ Rep_inverse, ...}] =>
SOME {abs_type = abs_type, rep_type = rep_type, Abs_name = Abs_name,
Rep_name = Rep_name, set_def = set_def, prop_of_Rep = prop_of Rep,
set_name = set_prefix ^ s, Abs_inverse = SOME Abs_inverse,
Rep_inverse = SOME Rep_inverse}
- | NONE => NONE
+ | _ => NONE
(* theory -> string -> bool *)
val is_typedef = is_some oo typedef_info
--- a/src/HOL/Tools/typecopy.ML Sat Mar 13 14:43:04 2010 +0100
+++ b/src/HOL/Tools/typecopy.ML Sat Mar 13 14:44:47 2010 +0100
@@ -80,7 +80,7 @@
end
in
thy
- |> Typedef.add_typedef false (SOME raw_tyco) (raw_tyco, map fst vs, NoSyn)
+ |> Typedef.add_typedef_global false (SOME raw_tyco) (raw_tyco, map fst vs, NoSyn)
(HOLogic.mk_UNIV ty) (Option.map swap constr_proj) tac
|-> (fn (tyco, info) => add_info tyco info)
end;
@@ -91,8 +91,9 @@
fun add_default_code tyco thy =
let
val SOME { constr = c, proj = (proj, _), proj_def = proj_eq, vs = vs,
- typ = ty_rep, ... } = get_info thy tyco;
- val SOME { Rep_inject = proj_inject, ... } = Typedef.get_info thy tyco;
+ typ = ty_rep, ... } = get_info thy tyco;
+ (* FIXME handle multiple typedef interpretations (!??) *)
+ val [{ Rep_inject = proj_inject, ... }] = Typedef.get_info_global thy tyco;
val constr = (c, Logic.unvarifyT (Sign.the_const_type thy c));
val ty = Type (tyco, map TFree vs);
val proj = Const (proj, ty --> ty_rep);
--- a/src/HOL/Tools/typedef_codegen.ML Sat Mar 13 14:43:04 2010 +0100
+++ b/src/HOL/Tools/typedef_codegen.ML Sat Mar 13 14:44:47 2010 +0100
@@ -24,9 +24,10 @@
val id = Codegen.mk_qual_id module (Codegen.get_const_id gr'' s)
in SOME (Codegen.mk_app brack (Codegen.str id) ps, gr'') end;
fun lookup f T =
- (case Typedef.get_info thy (get_name T) of
- NONE => ""
- | SOME info => f info);
+ (* FIXME handle multiple typedef interpretations (!??) *)
+ (case Typedef.get_info_global thy (get_name T) of
+ [info] => f info
+ | _ => "");
in
(case strip_comb t of
(Const (s, Type ("fun", [T, U])), ts) =>
@@ -45,58 +46,61 @@
| mk_tyexpr ps s = Pretty.list "(" (") " ^ s) ps;
fun typedef_tycodegen thy defs dep module brack (Type (s, Ts)) gr =
- (case Typedef.get_info thy s of
- NONE => NONE
- | SOME {abs_type as newT as Type (tname, Us), rep_type = oldT, Abs_name, Rep_name, ...} =>
- if is_some (Codegen.get_assoc_type thy tname) then NONE else
- let
- val module' = Codegen.if_library
- (Codegen.thyname_of_type thy tname) module;
- val node_id = tname ^ " (type)";
- val ((((qs, (_, Abs_id)), (_, Rep_id)), ty_id), gr') = gr |> fold_map
- (Codegen.invoke_tycodegen thy defs dep module (length Ts = 1))
- Ts ||>>
- Codegen.mk_const_id module' Abs_name ||>>
- Codegen.mk_const_id module' Rep_name ||>>
- Codegen.mk_type_id module' s;
- val tyexpr = mk_tyexpr qs (Codegen.mk_qual_id module ty_id)
- in SOME (tyexpr, case try (Codegen.get_node gr') node_id of
- NONE =>
- let
- val (p :: ps, gr'') = fold_map
- (Codegen.invoke_tycodegen thy defs node_id module' false)
- (oldT :: Us) (Codegen.add_edge (node_id, dep)
- (Codegen.new_node (node_id, (NONE, "", "")) gr'));
- val s =
- Codegen.string_of (Pretty.block [Codegen.str "datatype ",
- mk_tyexpr ps (snd ty_id),
- Codegen.str " =", Pretty.brk 1, Codegen.str (Abs_id ^ " of"),
- Pretty.brk 1, p, Codegen.str ";"]) ^ "\n\n" ^
- Codegen.string_of (Pretty.block [Codegen.str ("fun " ^ Rep_id),
- Pretty.brk 1, Codegen.str ("(" ^ Abs_id), Pretty.brk 1,
- Codegen.str "x) = x;"]) ^ "\n\n" ^
- (if "term_of" mem !Codegen.mode then
- Codegen.string_of (Pretty.block [Codegen.str "fun ",
- Codegen.mk_term_of gr'' module' false newT, Pretty.brk 1,
- Codegen.str ("(" ^ Abs_id), Pretty.brk 1,
- Codegen.str "x) =", Pretty.brk 1,
- Pretty.block [Codegen.str ("Const (\"" ^ Abs_name ^ "\","),
- Pretty.brk 1, Codegen.mk_type false (oldT --> newT),
- Codegen.str ")"], Codegen.str " $", Pretty.brk 1,
- Codegen.mk_term_of gr'' module' false oldT, Pretty.brk 1,
- Codegen.str "x;"]) ^ "\n\n"
- else "") ^
- (if "test" mem !Codegen.mode then
- Codegen.string_of (Pretty.block [Codegen.str "fun ",
- Codegen.mk_gen gr'' module' false [] "" newT, Pretty.brk 1,
- Codegen.str "i =", Pretty.brk 1,
- Pretty.block [Codegen.str (Abs_id ^ " ("),
- Codegen.mk_gen gr'' module' false [] "" oldT, Pretty.brk 1,
- Codegen.str "i);"]]) ^ "\n\n"
- else "")
- in Codegen.map_node node_id (K (NONE, module', s)) gr'' end
- | SOME _ => Codegen.add_edge (node_id, dep) gr')
- end)
+ (case Typedef.get_info_global thy s of
+ (* FIXME handle multiple typedef interpretations (!??) *)
+ [{abs_type as newT as Type (tname, Us), rep_type = oldT, Abs_name, Rep_name, ...}] =>
+ if is_some (Codegen.get_assoc_type thy tname) then NONE
+ else
+ let
+ val module' = Codegen.if_library
+ (Codegen.thyname_of_type thy tname) module;
+ val node_id = tname ^ " (type)";
+ val ((((qs, (_, Abs_id)), (_, Rep_id)), ty_id), gr') = gr |> fold_map
+ (Codegen.invoke_tycodegen thy defs dep module (length Ts = 1))
+ Ts ||>>
+ Codegen.mk_const_id module' Abs_name ||>>
+ Codegen.mk_const_id module' Rep_name ||>>
+ Codegen.mk_type_id module' s;
+ val tyexpr = mk_tyexpr qs (Codegen.mk_qual_id module ty_id)
+ in
+ SOME (tyexpr, case try (Codegen.get_node gr') node_id of
+ NONE =>
+ let
+ val (p :: ps, gr'') = fold_map
+ (Codegen.invoke_tycodegen thy defs node_id module' false)
+ (oldT :: Us) (Codegen.add_edge (node_id, dep)
+ (Codegen.new_node (node_id, (NONE, "", "")) gr'));
+ val s =
+ Codegen.string_of (Pretty.block [Codegen.str "datatype ",
+ mk_tyexpr ps (snd ty_id),
+ Codegen.str " =", Pretty.brk 1, Codegen.str (Abs_id ^ " of"),
+ Pretty.brk 1, p, Codegen.str ";"]) ^ "\n\n" ^
+ Codegen.string_of (Pretty.block [Codegen.str ("fun " ^ Rep_id),
+ Pretty.brk 1, Codegen.str ("(" ^ Abs_id), Pretty.brk 1,
+ Codegen.str "x) = x;"]) ^ "\n\n" ^
+ (if "term_of" mem !Codegen.mode then
+ Codegen.string_of (Pretty.block [Codegen.str "fun ",
+ Codegen.mk_term_of gr'' module' false newT, Pretty.brk 1,
+ Codegen.str ("(" ^ Abs_id), Pretty.brk 1,
+ Codegen.str "x) =", Pretty.brk 1,
+ Pretty.block [Codegen.str ("Const (\"" ^ Abs_name ^ "\","),
+ Pretty.brk 1, Codegen.mk_type false (oldT --> newT),
+ Codegen.str ")"], Codegen.str " $", Pretty.brk 1,
+ Codegen.mk_term_of gr'' module' false oldT, Pretty.brk 1,
+ Codegen.str "x;"]) ^ "\n\n"
+ else "") ^
+ (if "test" mem !Codegen.mode then
+ Codegen.string_of (Pretty.block [Codegen.str "fun ",
+ Codegen.mk_gen gr'' module' false [] "" newT, Pretty.brk 1,
+ Codegen.str "i =", Pretty.brk 1,
+ Pretty.block [Codegen.str (Abs_id ^ " ("),
+ Codegen.mk_gen gr'' module' false [] "" oldT, Pretty.brk 1,
+ Codegen.str "i);"]]) ^ "\n\n"
+ else "")
+ in Codegen.map_node node_id (K (NONE, module', s)) gr'' end
+ | SOME _ => Codegen.add_edge (node_id, dep) gr')
+ end
+ | _ => NONE)
| typedef_tycodegen thy defs dep module brack _ gr = NONE;
val setup =