seperated typedef codegen from main code
authorhaftmann
Mon Apr 24 16:37:52 2006 +0200 (2006-04-24)
changeset 194592041d472fc17
parent 19458 a70f1b0f09cd
child 19460 2b37469d52ad
seperated typedef codegen from main code
src/HOL/Tools/typedef_codegen.ML
src/HOL/Tools/typedef_package.ML
src/HOL/Typedef.thy
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Tools/typedef_codegen.ML	Mon Apr 24 16:37:52 2006 +0200
     1.3 @@ -0,0 +1,147 @@
     1.4 +(*  Title:      HOL/Tools/typedef_codegen.ML
     1.5 +    ID:         $Id$
     1.6 +    Author:     Stefan Berghofer and Florian Haftmann, TU Muenchen
     1.7 +
     1.8 +Code generators for trivial typedefs.
     1.9 +*)
    1.10 +
    1.11 +signature TYPEDEF_CODEGEN =
    1.12 +sig
    1.13 +  val typedef_fun_extr: theory -> string * typ -> thm list option
    1.14 +  val typedef_type_extr: theory -> string
    1.15 +      -> (((string * sort) list * (string * typ list) list) * tactic) option
    1.16 +  val setup: theory -> theory;
    1.17 +end;
    1.18 +
    1.19 +structure TypedefCodegen: TYPEDEF_CODEGEN =
    1.20 +struct
    1.21 +
    1.22 +fun typedef_codegen thy defs gr dep module brack t =
    1.23 +  let
    1.24 +    fun get_name (Type (tname, _)) = tname
    1.25 +      | get_name _ = "";
    1.26 +    fun mk_fun s T ts =
    1.27 +      let
    1.28 +        val (gr', _) = Codegen.invoke_tycodegen thy defs dep module false (gr, T);
    1.29 +        val (gr'', ps) =
    1.30 +          foldl_map (Codegen.invoke_codegen thy defs dep module true) (gr', ts);
    1.31 +        val id = Codegen.mk_qual_id module (Codegen.get_const_id s gr'')
    1.32 +      in SOME (gr'', Codegen.mk_app brack (Pretty.str id) ps) end;
    1.33 +    fun lookup f T =
    1.34 +      (case TypedefPackage.get_typedef_info thy (get_name T) of
    1.35 +        NONE => ""
    1.36 +      | SOME (s, _) => f s);
    1.37 +  in
    1.38 +    (case strip_comb t of
    1.39 +       (Const (s, Type ("fun", [T, U])), ts) =>
    1.40 +         if lookup #4 T = s andalso
    1.41 +           is_none (Codegen.get_assoc_type thy (get_name T))
    1.42 +         then mk_fun s T ts
    1.43 +         else if lookup #3 U = s andalso
    1.44 +           is_none (Codegen.get_assoc_type thy (get_name U))
    1.45 +         then mk_fun s U ts
    1.46 +         else NONE
    1.47 +     | _ => NONE)
    1.48 +  end;
    1.49 +
    1.50 +fun mk_tyexpr [] s = Pretty.str s
    1.51 +  | mk_tyexpr [p] s = Pretty.block [p, Pretty.str (" " ^ s)]
    1.52 +  | mk_tyexpr ps s = Pretty.list "(" (") " ^ s) ps;
    1.53 +
    1.54 +fun typedef_tycodegen thy defs gr dep module brack (Type (s, Ts)) =
    1.55 +      (case TypedefPackage.get_typedef_info thy s of
    1.56 +         NONE => NONE
    1.57 +       | SOME ((newT as Type (tname, Us), oldT, Abs_name, Rep_name), _) =>
    1.58 +           if is_some (Codegen.get_assoc_type thy tname) then NONE else
    1.59 +           let
    1.60 +             val module' = Codegen.if_library
    1.61 +               (Codegen.thyname_of_type tname thy) module;
    1.62 +             val node_id = tname ^ " (type)";
    1.63 +             val (gr', (((qs, (_, Abs_id)), (_, Rep_id)), ty_id)) = foldl_map
    1.64 +                 (Codegen.invoke_tycodegen thy defs dep module (length Ts = 1))
    1.65 +                   (gr, Ts) |>>>
    1.66 +               Codegen.mk_const_id module' Abs_name |>>>
    1.67 +               Codegen.mk_const_id module' Rep_name |>>>
    1.68 +               Codegen.mk_type_id module' s;
    1.69 +             val tyexpr = mk_tyexpr qs (Codegen.mk_qual_id module ty_id)
    1.70 +           in SOME (case try (Codegen.get_node gr') node_id of
    1.71 +               NONE =>
    1.72 +               let
    1.73 +                 val (gr'', p :: ps) = foldl_map
    1.74 +                   (Codegen.invoke_tycodegen thy defs node_id module' false)
    1.75 +                   (Codegen.add_edge (node_id, dep)
    1.76 +                      (Codegen.new_node (node_id, (NONE, "", "")) gr'), oldT :: Us);
    1.77 +                 val s =
    1.78 +                   Pretty.string_of (Pretty.block [Pretty.str "datatype ",
    1.79 +                     mk_tyexpr ps (snd ty_id),
    1.80 +                     Pretty.str " =", Pretty.brk 1, Pretty.str (Abs_id ^ " of"),
    1.81 +                     Pretty.brk 1, p, Pretty.str ";"]) ^ "\n\n" ^
    1.82 +                   Pretty.string_of (Pretty.block [Pretty.str ("fun " ^ Rep_id),
    1.83 +                     Pretty.brk 1, Pretty.str ("(" ^ Abs_id), Pretty.brk 1,
    1.84 +                     Pretty.str "x) = x;"]) ^ "\n\n" ^
    1.85 +                   (if "term_of" mem !Codegen.mode then
    1.86 +                      Pretty.string_of (Pretty.block [Pretty.str "fun ",
    1.87 +                        Codegen.mk_term_of gr'' module' false newT, Pretty.brk 1,
    1.88 +                        Pretty.str ("(" ^ Abs_id), Pretty.brk 1,
    1.89 +                        Pretty.str "x) =", Pretty.brk 1,
    1.90 +                        Pretty.block [Pretty.str ("Const (\"" ^ Abs_name ^ "\","),
    1.91 +                          Pretty.brk 1, Codegen.mk_type false (oldT --> newT),
    1.92 +                          Pretty.str ")"], Pretty.str " $", Pretty.brk 1,
    1.93 +                        Codegen.mk_term_of gr'' module' false oldT, Pretty.brk 1,
    1.94 +                        Pretty.str "x;"]) ^ "\n\n"
    1.95 +                    else "") ^
    1.96 +                   (if "test" mem !Codegen.mode then
    1.97 +                      Pretty.string_of (Pretty.block [Pretty.str "fun ",
    1.98 +                        Codegen.mk_gen gr'' module' false [] "" newT, Pretty.brk 1,
    1.99 +                        Pretty.str "i =", Pretty.brk 1,
   1.100 +                        Pretty.block [Pretty.str (Abs_id ^ " ("),
   1.101 +                          Codegen.mk_gen gr'' module' false [] "" oldT, Pretty.brk 1,
   1.102 +                          Pretty.str "i);"]]) ^ "\n\n"
   1.103 +                    else "")
   1.104 +               in Codegen.map_node node_id (K (NONE, module', s)) gr'' end
   1.105 +             | SOME _ => Codegen.add_edge (node_id, dep) gr', tyexpr)
   1.106 +           end)
   1.107 +  | typedef_tycodegen thy defs gr dep module brack _ = NONE;
   1.108 +
   1.109 +fun typedef_type_extr thy tyco =
   1.110 +  case TypedefPackage.get_typedef_info thy tyco
   1.111 +   of SOME ((ty_abs, ty_rep, c_abs, c_rep), (SOME def, inject, _)) =>
   1.112 +        let
   1.113 +          val exists_thm =
   1.114 +            UNIV_I
   1.115 +            |> Drule.instantiate' [SOME (ctyp_of thy ty_rep)] []
   1.116 +            |> rewrite_rule [symmetric def];
   1.117 +        in case try (Tactic.rule_by_tactic ((ALLGOALS o match_tac) [exists_thm])) inject
   1.118 +         of SOME eq_thm => SOME (((Term.typ_tfrees o Type.no_tvars) ty_abs, [(c_abs, [ty_rep])]),
   1.119 +             (ALLGOALS o match_tac) [eq_reflection]
   1.120 +            THEN (ALLGOALS o match_tac) [eq_thm])
   1.121 +          | NONE => NONE
   1.122 +        end
   1.123 +    | _ => NONE;
   1.124 +
   1.125 +fun typedef_fun_extr thy (c, ty) =
   1.126 +  case (fst o strip_type) ty
   1.127 +   of Type (tyco, _) :: _ =>
   1.128 +    (case TypedefPackage.get_typedef_info thy tyco
   1.129 +     of SOME ((ty_abs, ty_rep, c_abs, c_rep), (SOME def, _, inverse)) =>
   1.130 +          if c = c_rep then
   1.131 +            let
   1.132 +              val exists_thm =
   1.133 +                UNIV_I
   1.134 +                |> Drule.instantiate' [SOME (ctyp_of thy ty_rep)] []
   1.135 +                |> rewrite_rule [symmetric def]
   1.136 +            in case try (Tactic.rule_by_tactic ((ALLGOALS o match_tac) [exists_thm])) inverse
   1.137 +             of SOME eq_thm => SOME [eq_thm]
   1.138 +              | NONE => NONE
   1.139 +            end
   1.140 +          else NONE
   1.141 +      | _ => NONE)
   1.142 +    | _ => NONE;
   1.143 +
   1.144 +val setup =
   1.145 +  Codegen.add_codegen "typedef" typedef_codegen
   1.146 +  #> Codegen.add_tycodegen "typedef" typedef_tycodegen
   1.147 +  #> CodegenTheorems.add_fun_extr (these oo typedef_fun_extr)
   1.148 +  #> CodegenTheorems.add_datatype_extr typedef_type_extr
   1.149 +
   1.150 +end;
     2.1 --- a/src/HOL/Tools/typedef_package.ML	Mon Apr 24 16:37:37 2006 +0200
     2.2 +++ b/src/HOL/Tools/typedef_package.ML	Mon Apr 24 16:37:52 2006 +0200
     2.3 @@ -23,8 +23,9 @@
     2.4      * (string * string) option -> theory -> Proof.state
     2.5    val typedef_i: (bool * string) * (bstring * string list * mixfix) * term
     2.6      * (string * string) option -> theory -> Proof.state
     2.7 +  type typedef_info = (typ * typ * string * string) * (thm option * thm * thm)
     2.8 +  val get_typedef_info: theory -> string -> typedef_info option
     2.9    val setup: theory -> theory
    2.10 -  structure TypedefData : THEORY_DATA
    2.11  end;
    2.12  
    2.13  structure TypedefPackage: TYPEDEF_PACKAGE =
    2.14 @@ -72,10 +73,12 @@
    2.15  
    2.16  (* theory data *)
    2.17  
    2.18 +type typedef_info = (typ * typ * string * string) * (thm option * thm * thm);
    2.19 +
    2.20  structure TypedefData = TheoryDataFun
    2.21  (struct
    2.22    val name = "HOL/typedef";
    2.23 -  type T = ((typ * typ * string * string) * (thm option * thm * thm)) Symtab.table;
    2.24 +  type T = typedef_info Symtab.table;
    2.25    val empty = Symtab.empty;
    2.26    val copy = I;
    2.27    val extend = I;
    2.28 @@ -83,6 +86,8 @@
    2.29    fun print _ _ = ();
    2.30  end);
    2.31  
    2.32 +val get_typedef_info = Symtab.lookup o TypedefData.get;
    2.33 +
    2.34  fun put_typedef newT oldT Abs_name Rep_name def inject inverse =
    2.35    TypedefData.map (Symtab.update_new (fst (dest_Type newT),
    2.36      ((newT, oldT, Abs_name, Rep_name), (def, inject, inverse))));
    2.37 @@ -274,140 +279,9 @@
    2.38  val typedef = gen_typedef read_term;
    2.39  val typedef_i = gen_typedef cert_term;
    2.40  
    2.41 -end;
    2.42 -
    2.43 -
    2.44 -
    2.45 -(** trivial code generator **)
    2.46 -
    2.47 -fun typedef_codegen thy defs gr dep module brack t =
    2.48 -  let
    2.49 -    fun get_name (Type (tname, _)) = tname
    2.50 -      | get_name _ = "";
    2.51 -    fun mk_fun s T ts =
    2.52 -      let
    2.53 -        val (gr', _) = Codegen.invoke_tycodegen thy defs dep module false (gr, T);
    2.54 -        val (gr'', ps) =
    2.55 -          foldl_map (Codegen.invoke_codegen thy defs dep module true) (gr', ts);
    2.56 -        val id = Codegen.mk_qual_id module (Codegen.get_const_id s gr'')
    2.57 -      in SOME (gr'', Codegen.mk_app brack (Pretty.str id) ps) end;
    2.58 -    fun lookup f T =
    2.59 -      (case Symtab.lookup (TypedefData.get thy) (get_name T) of
    2.60 -        NONE => ""
    2.61 -      | SOME (s, _) => f s);
    2.62 -  in
    2.63 -    (case strip_comb t of
    2.64 -       (Const (s, Type ("fun", [T, U])), ts) =>
    2.65 -         if lookup #4 T = s andalso
    2.66 -           is_none (Codegen.get_assoc_type thy (get_name T))
    2.67 -         then mk_fun s T ts
    2.68 -         else if lookup #3 U = s andalso
    2.69 -           is_none (Codegen.get_assoc_type thy (get_name U))
    2.70 -         then mk_fun s U ts
    2.71 -         else NONE
    2.72 -     | _ => NONE)
    2.73 -  end;
    2.74 -
    2.75 -fun mk_tyexpr [] s = Pretty.str s
    2.76 -  | mk_tyexpr [p] s = Pretty.block [p, Pretty.str (" " ^ s)]
    2.77 -  | mk_tyexpr ps s = Pretty.list "(" (") " ^ s) ps;
    2.78 +end; (*local*)
    2.79  
    2.80 -fun typedef_tycodegen thy defs gr dep module brack (Type (s, Ts)) =
    2.81 -      (case Symtab.lookup (TypedefData.get thy) s of
    2.82 -         NONE => NONE
    2.83 -       | SOME ((newT as Type (tname, Us), oldT, Abs_name, Rep_name), _) =>
    2.84 -           if is_some (Codegen.get_assoc_type thy tname) then NONE else
    2.85 -           let
    2.86 -             val module' = Codegen.if_library
    2.87 -               (Codegen.thyname_of_type tname thy) module;
    2.88 -             val node_id = tname ^ " (type)";
    2.89 -             val (gr', (((qs, (_, Abs_id)), (_, Rep_id)), ty_id)) = foldl_map
    2.90 -                 (Codegen.invoke_tycodegen thy defs dep module (length Ts = 1))
    2.91 -                   (gr, Ts) |>>>
    2.92 -               Codegen.mk_const_id module' Abs_name |>>>
    2.93 -               Codegen.mk_const_id module' Rep_name |>>>
    2.94 -               Codegen.mk_type_id module' s;
    2.95 -             val tyexpr = mk_tyexpr qs (Codegen.mk_qual_id module ty_id)
    2.96 -           in SOME (case try (Codegen.get_node gr') node_id of
    2.97 -               NONE =>
    2.98 -               let
    2.99 -                 val (gr'', p :: ps) = foldl_map
   2.100 -                   (Codegen.invoke_tycodegen thy defs node_id module' false)
   2.101 -                   (Codegen.add_edge (node_id, dep)
   2.102 -                      (Codegen.new_node (node_id, (NONE, "", "")) gr'), oldT :: Us);
   2.103 -                 val s =
   2.104 -                   Pretty.string_of (Pretty.block [Pretty.str "datatype ",
   2.105 -                     mk_tyexpr ps (snd ty_id),
   2.106 -                     Pretty.str " =", Pretty.brk 1, Pretty.str (Abs_id ^ " of"),
   2.107 -                     Pretty.brk 1, p, Pretty.str ";"]) ^ "\n\n" ^
   2.108 -                   Pretty.string_of (Pretty.block [Pretty.str ("fun " ^ Rep_id),
   2.109 -                     Pretty.brk 1, Pretty.str ("(" ^ Abs_id), Pretty.brk 1,
   2.110 -                     Pretty.str "x) = x;"]) ^ "\n\n" ^
   2.111 -                   (if "term_of" mem !Codegen.mode then
   2.112 -                      Pretty.string_of (Pretty.block [Pretty.str "fun ",
   2.113 -                        Codegen.mk_term_of gr'' module' false newT, Pretty.brk 1,
   2.114 -                        Pretty.str ("(" ^ Abs_id), Pretty.brk 1,
   2.115 -                        Pretty.str "x) =", Pretty.brk 1,
   2.116 -                        Pretty.block [Pretty.str ("Const (\"" ^ Abs_name ^ "\","),
   2.117 -                          Pretty.brk 1, Codegen.mk_type false (oldT --> newT),
   2.118 -                          Pretty.str ")"], Pretty.str " $", Pretty.brk 1,
   2.119 -                        Codegen.mk_term_of gr'' module' false oldT, Pretty.brk 1,
   2.120 -                        Pretty.str "x;"]) ^ "\n\n"
   2.121 -                    else "") ^
   2.122 -                   (if "test" mem !Codegen.mode then
   2.123 -                      Pretty.string_of (Pretty.block [Pretty.str "fun ",
   2.124 -                        Codegen.mk_gen gr'' module' false [] "" newT, Pretty.brk 1,
   2.125 -                        Pretty.str "i =", Pretty.brk 1,
   2.126 -                        Pretty.block [Pretty.str (Abs_id ^ " ("),
   2.127 -                          Codegen.mk_gen gr'' module' false [] "" oldT, Pretty.brk 1,
   2.128 -                          Pretty.str "i);"]]) ^ "\n\n"
   2.129 -                    else "")
   2.130 -               in Codegen.map_node node_id (K (NONE, module', s)) gr'' end
   2.131 -             | SOME _ => Codegen.add_edge (node_id, dep) gr', tyexpr)
   2.132 -           end)
   2.133 -  | typedef_tycodegen thy defs gr dep module brack _ = NONE;
   2.134 -
   2.135 -fun typedef_type_extr thy tyco =
   2.136 -  case Symtab.lookup (TypedefData.get thy) tyco
   2.137 -   of SOME ((ty_abs, ty_rep, c_abs, c_rep), (SOME def, inject, _)) =>
   2.138 -        let
   2.139 -          val exists_thm =
   2.140 -            UNIV_I
   2.141 -            |> Drule.instantiate' [SOME (ctyp_of thy ty_rep)] []
   2.142 -            |> rewrite_rule [symmetric def];
   2.143 -        in case try (Tactic.rule_by_tactic ((ALLGOALS o resolve_tac) [exists_thm])) inject
   2.144 -         of SOME eq_thm => SOME (((Term.typ_tfrees o Type.no_tvars) ty_abs, [(c_abs, [ty_rep])]),
   2.145 -             (ALLGOALS o resolve_tac) [eq_reflection]
   2.146 -            THEN (ALLGOALS o resolve_tac) [eq_thm])
   2.147 -          | NONE => NONE
   2.148 -        end
   2.149 -    | _ => NONE;
   2.150 -
   2.151 -fun typedef_fun_extr thy (c, ty) =
   2.152 -  case (fst o strip_type) ty
   2.153 -   of Type (tyco, _) :: _ =>
   2.154 -    (case Symtab.lookup (TypedefData.get thy) tyco
   2.155 -     of SOME ((ty_abs, ty_rep, c_abs, c_rep), (SOME def, _, inverse)) =>
   2.156 -          if c = c_rep then
   2.157 -            let
   2.158 -              val exists_thm =
   2.159 -                UNIV_I
   2.160 -                |> Drule.instantiate' [SOME (ctyp_of thy ty_rep)] []
   2.161 -                |> rewrite_rule [symmetric def]
   2.162 -            in case try (Tactic.rule_by_tactic ((ALLGOALS o resolve_tac) [exists_thm])) inverse
   2.163 -             of SOME eq_thm => SOME [eq_thm]
   2.164 -              | NONE => NONE
   2.165 -            end
   2.166 -          else NONE
   2.167 -      | _ => NONE)
   2.168 -    | _ => NONE;
   2.169 -
   2.170 -val setup =
   2.171 -  TypedefData.init
   2.172 -  #> Codegen.add_codegen "typedef" typedef_codegen
   2.173 -  #> Codegen.add_tycodegen "typedef" typedef_tycodegen
   2.174 -  #> CodegenTheorems.add_fun_extr (these oo typedef_fun_extr)
   2.175 -  #> CodegenTheorems.add_datatype_extr typedef_type_extr
   2.176 +val setup = TypedefData.init;
   2.177  
   2.178  
   2.179  
     3.1 --- a/src/HOL/Typedef.thy	Mon Apr 24 16:37:37 2006 +0200
     3.2 +++ b/src/HOL/Typedef.thy	Mon Apr 24 16:37:52 2006 +0200
     3.3 @@ -7,7 +7,7 @@
     3.4  
     3.5  theory Typedef
     3.6  imports Set
     3.7 -uses ("Tools/typedef_package.ML")
     3.8 +uses ("Tools/typedef_package.ML") ("Tools/typedef_codegen.ML")
     3.9  begin
    3.10  
    3.11  locale type_definition =
    3.12 @@ -83,7 +83,8 @@
    3.13  qed
    3.14  
    3.15  use "Tools/typedef_package.ML"
    3.16 +use "Tools/typedef_codegen.ML"
    3.17  
    3.18 -setup TypedefPackage.setup
    3.19 +setup {* TypedefPackage.setup #> TypedefCodegen.setup *}
    3.20  
    3.21  end