# HG changeset patch # User haftmann # Date 1145889472 -7200 # Node ID 2041d472fc17c582db2038b8889cb1baec61f335 # Parent a70f1b0f09cda7a6361a099bc0049f699a01f4ee seperated typedef codegen from main code diff -r a70f1b0f09cd -r 2041d472fc17 src/HOL/Tools/typedef_codegen.ML --- /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; diff -r a70f1b0f09cd -r 2041d472fc17 src/HOL/Tools/typedef_package.ML --- 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; diff -r a70f1b0f09cd -r 2041d472fc17 src/HOL/Typedef.thy --- a/src/HOL/Typedef.thy Mon Apr 24 16:37:37 2006 +0200 +++ b/src/HOL/Typedef.thy Mon Apr 24 16:37:52 2006 +0200 @@ -7,7 +7,7 @@ theory Typedef imports Set -uses ("Tools/typedef_package.ML") +uses ("Tools/typedef_package.ML") ("Tools/typedef_codegen.ML") begin locale type_definition = @@ -83,7 +83,8 @@ qed use "Tools/typedef_package.ML" +use "Tools/typedef_codegen.ML" -setup TypedefPackage.setup +setup {* TypedefPackage.setup #> TypedefCodegen.setup *} end