# HG changeset patch # User wenzelm # Date 1268487887 -3600 # Node ID c506c029a082812293ee5d793f7da89769a18843 # Parent eb8d2f668bfc06a69cbaeb13a8fbf136abd91f8d adapted to localized typedef: handle single global interpretation only; diff -r eb8d2f668bfc -r c506c029a082 src/HOL/Tools/Nitpick/nitpick_hol.ML --- 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 \ 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 diff -r eb8d2f668bfc -r c506c029a082 src/HOL/Tools/typecopy.ML --- 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); diff -r eb8d2f668bfc -r c506c029a082 src/HOL/Tools/typedef_codegen.ML --- 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 =