--- a/src/HOL/Tools/typedef_package.ML Mon Apr 24 16:37:37 2006 +0200
+++ b/src/HOL/Tools/typedef_package.ML Mon Apr 24 16:37:52 2006 +0200
@@ -23,8 +23,9 @@
* (string * string) option -> theory -> Proof.state
val typedef_i: (bool * string) * (bstring * string list * mixfix) * term
* (string * string) option -> theory -> Proof.state
+ type typedef_info = (typ * typ * string * string) * (thm option * thm * thm)
+ val get_typedef_info: theory -> string -> typedef_info option
val setup: theory -> theory
- structure TypedefData : THEORY_DATA
end;
structure TypedefPackage: TYPEDEF_PACKAGE =
@@ -72,10 +73,12 @@
(* theory data *)
+type typedef_info = (typ * typ * string * string) * (thm option * thm * thm);
+
structure TypedefData = TheoryDataFun
(struct
val name = "HOL/typedef";
- type T = ((typ * typ * string * string) * (thm option * thm * thm)) Symtab.table;
+ type T = typedef_info Symtab.table;
val empty = Symtab.empty;
val copy = I;
val extend = I;
@@ -83,6 +86,8 @@
fun print _ _ = ();
end);
+val get_typedef_info = Symtab.lookup o TypedefData.get;
+
fun put_typedef newT oldT Abs_name Rep_name def inject inverse =
TypedefData.map (Symtab.update_new (fst (dest_Type newT),
((newT, oldT, Abs_name, Rep_name), (def, inject, inverse))));
@@ -274,140 +279,9 @@
val typedef = gen_typedef read_term;
val typedef_i = gen_typedef cert_term;
-end;
-
-
-
-(** trivial code generator **)
-
-fun typedef_codegen thy defs gr dep module brack t =
- let
- fun get_name (Type (tname, _)) = tname
- | get_name _ = "";
- fun mk_fun s T ts =
- let
- val (gr', _) = Codegen.invoke_tycodegen thy defs dep module false (gr, T);
- val (gr'', ps) =
- foldl_map (Codegen.invoke_codegen thy defs dep module true) (gr', ts);
- val id = Codegen.mk_qual_id module (Codegen.get_const_id s gr'')
- in SOME (gr'', Codegen.mk_app brack (Pretty.str id) ps) end;
- fun lookup f T =
- (case Symtab.lookup (TypedefData.get thy) (get_name T) of
- NONE => ""
- | SOME (s, _) => f s);
- in
- (case strip_comb t of
- (Const (s, Type ("fun", [T, U])), ts) =>
- if lookup #4 T = s andalso
- is_none (Codegen.get_assoc_type thy (get_name T))
- then mk_fun s T ts
- else if lookup #3 U = s andalso
- is_none (Codegen.get_assoc_type thy (get_name U))
- then mk_fun s U ts
- else NONE
- | _ => NONE)
- end;
-
-fun mk_tyexpr [] s = Pretty.str s
- | mk_tyexpr [p] s = Pretty.block [p, Pretty.str (" " ^ s)]
- | mk_tyexpr ps s = Pretty.list "(" (") " ^ s) ps;
+end; (*local*)
-fun typedef_tycodegen thy defs gr dep module brack (Type (s, Ts)) =
- (case Symtab.lookup (TypedefData.get thy) s of
- NONE => NONE
- | SOME ((newT as Type (tname, Us), 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 tname thy) module;
- val node_id = tname ^ " (type)";
- val (gr', (((qs, (_, Abs_id)), (_, Rep_id)), ty_id)) = foldl_map
- (Codegen.invoke_tycodegen thy defs dep module (length Ts = 1))
- (gr, 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 (case try (Codegen.get_node gr') node_id of
- NONE =>
- let
- val (gr'', p :: ps) = foldl_map
- (Codegen.invoke_tycodegen thy defs node_id module' false)
- (Codegen.add_edge (node_id, dep)
- (Codegen.new_node (node_id, (NONE, "", "")) gr'), oldT :: Us);
- val s =
- Pretty.string_of (Pretty.block [Pretty.str "datatype ",
- mk_tyexpr ps (snd ty_id),
- Pretty.str " =", Pretty.brk 1, Pretty.str (Abs_id ^ " of"),
- Pretty.brk 1, p, Pretty.str ";"]) ^ "\n\n" ^
- Pretty.string_of (Pretty.block [Pretty.str ("fun " ^ Rep_id),
- Pretty.brk 1, Pretty.str ("(" ^ Abs_id), Pretty.brk 1,
- Pretty.str "x) = x;"]) ^ "\n\n" ^
- (if "term_of" mem !Codegen.mode then
- Pretty.string_of (Pretty.block [Pretty.str "fun ",
- Codegen.mk_term_of gr'' module' false newT, Pretty.brk 1,
- Pretty.str ("(" ^ Abs_id), Pretty.brk 1,
- Pretty.str "x) =", Pretty.brk 1,
- Pretty.block [Pretty.str ("Const (\"" ^ Abs_name ^ "\","),
- Pretty.brk 1, Codegen.mk_type false (oldT --> newT),
- Pretty.str ")"], Pretty.str " $", Pretty.brk 1,
- Codegen.mk_term_of gr'' module' false oldT, Pretty.brk 1,
- Pretty.str "x;"]) ^ "\n\n"
- else "") ^
- (if "test" mem !Codegen.mode then
- Pretty.string_of (Pretty.block [Pretty.str "fun ",
- Codegen.mk_gen gr'' module' false [] "" newT, Pretty.brk 1,
- Pretty.str "i =", Pretty.brk 1,
- Pretty.block [Pretty.str (Abs_id ^ " ("),
- Codegen.mk_gen gr'' module' false [] "" oldT, Pretty.brk 1,
- Pretty.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', tyexpr)
- end)
- | typedef_tycodegen thy defs gr dep module brack _ = NONE;
-
-fun typedef_type_extr thy tyco =
- case Symtab.lookup (TypedefData.get thy) tyco
- of SOME ((ty_abs, ty_rep, c_abs, c_rep), (SOME def, inject, _)) =>
- let
- val exists_thm =
- UNIV_I
- |> Drule.instantiate' [SOME (ctyp_of thy ty_rep)] []
- |> rewrite_rule [symmetric def];
- in case try (Tactic.rule_by_tactic ((ALLGOALS o resolve_tac) [exists_thm])) inject
- of SOME eq_thm => SOME (((Term.typ_tfrees o Type.no_tvars) ty_abs, [(c_abs, [ty_rep])]),
- (ALLGOALS o resolve_tac) [eq_reflection]
- THEN (ALLGOALS o resolve_tac) [eq_thm])
- | NONE => NONE
- end
- | _ => NONE;
-
-fun typedef_fun_extr thy (c, ty) =
- case (fst o strip_type) ty
- of Type (tyco, _) :: _ =>
- (case Symtab.lookup (TypedefData.get thy) tyco
- of SOME ((ty_abs, ty_rep, c_abs, c_rep), (SOME def, _, inverse)) =>
- if c = c_rep then
- let
- val exists_thm =
- UNIV_I
- |> Drule.instantiate' [SOME (ctyp_of thy ty_rep)] []
- |> rewrite_rule [symmetric def]
- in case try (Tactic.rule_by_tactic ((ALLGOALS o resolve_tac) [exists_thm])) inverse
- of SOME eq_thm => SOME [eq_thm]
- | NONE => NONE
- end
- else NONE
- | _ => NONE)
- | _ => NONE;
-
-val setup =
- TypedefData.init
- #> Codegen.add_codegen "typedef" typedef_codegen
- #> Codegen.add_tycodegen "typedef" typedef_tycodegen
- #> CodegenTheorems.add_fun_extr (these oo typedef_fun_extr)
- #> CodegenTheorems.add_datatype_extr typedef_type_extr
+val setup = TypedefData.init;