dropped SML typedef_codegen: does not fit to code equations for record operations any longer
authorhaftmann
Tue Aug 17 16:44:24 2010 +0200 (2010-08-17)
changeset 385367e57a0dcbd4f
parent 38535 9f64860c6ec0
child 38537 6a78c972de27
dropped SML typedef_codegen: does not fit to code equations for record operations any longer
src/HOL/IsaMakefile
src/HOL/Tools/typedef_codegen.ML
src/HOL/Typedef.thy
     1.1 --- a/src/HOL/IsaMakefile	Tue Aug 17 16:44:21 2010 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Tue Aug 17 16:44:24 2010 +0200
     1.3 @@ -213,7 +213,6 @@
     1.4    Tools/sat_funcs.ML \
     1.5    Tools/sat_solver.ML \
     1.6    Tools/split_rule.ML \
     1.7 -  Tools/typedef_codegen.ML \
     1.8    Tools/typedef.ML \
     1.9    Transitive_Closure.thy \
    1.10    Typedef.thy \
     2.1 --- a/src/HOL/Tools/typedef_codegen.ML	Tue Aug 17 16:44:21 2010 +0200
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,110 +0,0 @@
     2.4 -(*  Title:      HOL/Tools/typedef_codegen.ML
     2.5 -    Author:     Stefan Berghofer, TU Muenchen
     2.6 -
     2.7 -Code generators for trivial typedefs.
     2.8 -*)
     2.9 -
    2.10 -signature TYPEDEF_CODEGEN =
    2.11 -sig
    2.12 -  val setup: theory -> theory
    2.13 -end;
    2.14 -
    2.15 -structure TypedefCodegen: TYPEDEF_CODEGEN =
    2.16 -struct
    2.17 -
    2.18 -fun typedef_codegen thy defs dep module brack t gr =
    2.19 -  let
    2.20 -    fun get_name (Type (tname, _)) = tname
    2.21 -      | get_name _ = "";
    2.22 -    fun mk_fun s T ts =
    2.23 -      let
    2.24 -        val (_, gr') = Codegen.invoke_tycodegen thy defs dep module false T gr;
    2.25 -        val (ps, gr'') =
    2.26 -          fold_map (Codegen.invoke_codegen thy defs dep module true) ts gr';
    2.27 -        val id = Codegen.mk_qual_id module (Codegen.get_const_id gr'' s)
    2.28 -      in SOME (Codegen.mk_app brack (Codegen.str id) ps, gr'') end;
    2.29 -    fun lookup f T =
    2.30 -      (* FIXME handle multiple typedef interpretations (!??) *)
    2.31 -      (case Typedef.get_info_global thy (get_name T) of
    2.32 -        [info] => f info
    2.33 -      | _ => "");
    2.34 -  in
    2.35 -    (case strip_comb t of
    2.36 -       (Const (s, Type ("fun", [T, U])), ts) =>
    2.37 -         if lookup (#Rep_name o #1) T = s andalso
    2.38 -           is_none (Codegen.get_assoc_type thy (get_name T))
    2.39 -         then mk_fun s T ts
    2.40 -         else if lookup (#Abs_name o #1) U = s andalso
    2.41 -           is_none (Codegen.get_assoc_type thy (get_name U))
    2.42 -         then mk_fun s U ts
    2.43 -         else NONE
    2.44 -     | _ => NONE)
    2.45 -  end;
    2.46 -
    2.47 -fun mk_tyexpr [] s = Codegen.str s
    2.48 -  | mk_tyexpr [p] s = Pretty.block [p, Codegen.str (" " ^ s)]
    2.49 -  | mk_tyexpr ps s = Pretty.list "(" (") " ^ s) ps;
    2.50 -
    2.51 -fun typedef_tycodegen thy defs dep module brack (Type (s, Ts)) gr =
    2.52 -      (case Typedef.get_info_global thy s of
    2.53 -        (* FIXME handle multiple typedef interpretations (!??) *)
    2.54 -        [({abs_type as newT as Type (tname, Us), rep_type = oldT, Abs_name, Rep_name, ...}, _)] =>
    2.55 -          if is_some (Codegen.get_assoc_type thy tname) then NONE
    2.56 -          else
    2.57 -            let
    2.58 -              val module' = Codegen.if_library
    2.59 -                (Codegen.thyname_of_type thy tname) module;
    2.60 -              val node_id = tname ^ " (type)";
    2.61 -              val ((((qs, (_, Abs_id)), (_, Rep_id)), ty_id), gr') = gr |> fold_map
    2.62 -                  (Codegen.invoke_tycodegen thy defs dep module (length Ts = 1))
    2.63 -                    Ts ||>>
    2.64 -                Codegen.mk_const_id module' Abs_name ||>>
    2.65 -                Codegen.mk_const_id module' Rep_name ||>>
    2.66 -                Codegen.mk_type_id module' s;
    2.67 -              val tyexpr = mk_tyexpr qs (Codegen.mk_qual_id module ty_id)
    2.68 -            in
    2.69 -              SOME (tyexpr, case try (Codegen.get_node gr') node_id of
    2.70 -                NONE =>
    2.71 -                  let
    2.72 -                    val (p :: ps, gr'') = fold_map
    2.73 -                      (Codegen.invoke_tycodegen thy defs node_id module' false)
    2.74 -                      (oldT :: Us) (Codegen.add_edge (node_id, dep)
    2.75 -                        (Codegen.new_node (node_id, (NONE, "", "")) gr'));
    2.76 -                    val s =
    2.77 -                      Codegen.string_of (Pretty.block [Codegen.str "datatype ",
    2.78 -                        mk_tyexpr ps (snd ty_id),
    2.79 -                        Codegen.str " =", Pretty.brk 1, Codegen.str (Abs_id ^ " of"),
    2.80 -                        Pretty.brk 1, p, Codegen.str ";"]) ^ "\n\n" ^
    2.81 -                      Codegen.string_of (Pretty.block [Codegen.str ("fun " ^ Rep_id),
    2.82 -                        Pretty.brk 1, Codegen.str ("(" ^ Abs_id), Pretty.brk 1,
    2.83 -                        Codegen.str "x) = x;"]) ^ "\n\n" ^
    2.84 -                      (if member (op =) (!Codegen.mode) "term_of" then
    2.85 -                        Codegen.string_of (Pretty.block [Codegen.str "fun ",
    2.86 -                          Codegen.mk_term_of gr'' module' false newT, Pretty.brk 1,
    2.87 -                          Codegen.str ("(" ^ Abs_id), Pretty.brk 1,
    2.88 -                          Codegen.str "x) =", Pretty.brk 1,
    2.89 -                          Pretty.block [Codegen.str ("Const (\"" ^ Abs_name ^ "\","),
    2.90 -                            Pretty.brk 1, Codegen.mk_type false (oldT --> newT),
    2.91 -                            Codegen.str ")"], Codegen.str " $", Pretty.brk 1,
    2.92 -                          Codegen.mk_term_of gr'' module' false oldT, Pretty.brk 1,
    2.93 -                          Codegen.str "x;"]) ^ "\n\n"
    2.94 -                       else "") ^
    2.95 -                      (if member (op =) (!Codegen.mode) "test" then
    2.96 -                        Codegen.string_of (Pretty.block [Codegen.str "fun ",
    2.97 -                          Codegen.mk_gen gr'' module' false [] "" newT, Pretty.brk 1,
    2.98 -                          Codegen.str "i =", Pretty.brk 1,
    2.99 -                          Pretty.block [Codegen.str (Abs_id ^ " ("),
   2.100 -                            Codegen.mk_gen gr'' module' false [] "" oldT, Pretty.brk 1,
   2.101 -                            Codegen.str "i);"]]) ^ "\n\n"
   2.102 -                       else "")
   2.103 -                  in Codegen.map_node node_id (K (NONE, module', s)) gr'' end
   2.104 -              | SOME _ => Codegen.add_edge (node_id, dep) gr')
   2.105 -            end
   2.106 -      | _ => NONE)
   2.107 -  | typedef_tycodegen thy defs dep module brack _ gr = NONE;
   2.108 -
   2.109 -val setup =
   2.110 -  Codegen.add_codegen "typedef" typedef_codegen
   2.111 -  #> Codegen.add_tycodegen "typedef" typedef_tycodegen
   2.112 -
   2.113 -end;
     3.1 --- a/src/HOL/Typedef.thy	Tue Aug 17 16:44:21 2010 +0200
     3.2 +++ b/src/HOL/Typedef.thy	Tue Aug 17 16:44:24 2010 +0200
     3.3 @@ -6,9 +6,7 @@
     3.4  
     3.5  theory Typedef
     3.6  imports Set
     3.7 -uses
     3.8 -  ("Tools/typedef.ML")
     3.9 -  ("Tools/typedef_codegen.ML")
    3.10 +uses ("Tools/typedef.ML")
    3.11  begin
    3.12  
    3.13  ML {*
    3.14 @@ -115,6 +113,5 @@
    3.15  end
    3.16  
    3.17  use "Tools/typedef.ML" setup Typedef.setup
    3.18 -use "Tools/typedef_codegen.ML" setup TypedefCodegen.setup
    3.19  
    3.20  end