--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/typedef_codegen.ML Mon Apr 24 16:37:52 2006 +0200
@@ -0,0 +1,147 @@
+(* Title: HOL/Tools/typedef_codegen.ML
+ ID: $Id$
+ Author: Stefan Berghofer and Florian Haftmann, TU Muenchen
+
+Code generators for trivial typedefs.
+*)
+
+signature TYPEDEF_CODEGEN =
+sig
+ val typedef_fun_extr: theory -> string * typ -> thm list option
+ val typedef_type_extr: theory -> string
+ -> (((string * sort) list * (string * typ list) list) * tactic) option
+ val setup: theory -> theory;
+end;
+
+structure TypedefCodegen: TYPEDEF_CODEGEN =
+struct
+
+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 TypedefPackage.get_typedef_info 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;
+
+fun typedef_tycodegen thy defs gr dep module brack (Type (s, Ts)) =
+ (case TypedefPackage.get_typedef_info 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 TypedefPackage.get_typedef_info 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 match_tac) [exists_thm])) inject
+ of SOME eq_thm => SOME (((Term.typ_tfrees o Type.no_tvars) ty_abs, [(c_abs, [ty_rep])]),
+ (ALLGOALS o match_tac) [eq_reflection]
+ THEN (ALLGOALS o match_tac) [eq_thm])
+ | NONE => NONE
+ end
+ | _ => NONE;
+
+fun typedef_fun_extr thy (c, ty) =
+ case (fst o strip_type) ty
+ of Type (tyco, _) :: _ =>
+ (case TypedefPackage.get_typedef_info 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 match_tac) [exists_thm])) inverse
+ of SOME eq_thm => SOME [eq_thm]
+ | NONE => NONE
+ end
+ else NONE
+ | _ => NONE)
+ | _ => NONE;
+
+val setup =
+ 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
+
+end;