src/HOL/Tools/recfun_codegen.ML
author haftmann
Wed Jan 13 12:20:37 2010 +0100 (2010-01-13)
changeset 34895 19fd499cddff
parent 34893 ecdc526af73a
child 35225 dfbcff38c9ed
permissions -rw-r--r--
explicit abstract type of code certificates
haftmann@24584
     1
(*  Title:      HOL/Tools/recfun_codegen.ML
berghofe@12447
     2
    Author:     Stefan Berghofer, TU Muenchen
berghofe@12447
     3
berghofe@12447
     4
Code generator for recursive functions.
berghofe@12447
     5
*)
berghofe@12447
     6
berghofe@12447
     7
signature RECFUN_CODEGEN =
berghofe@12447
     8
sig
wenzelm@18708
     9
  val setup: theory -> theory
berghofe@12447
    10
end;
berghofe@12447
    11
berghofe@12447
    12
structure RecfunCodegen : RECFUN_CODEGEN =
berghofe@12447
    13
struct
berghofe@12447
    14
berghofe@12447
    15
open Codegen;
berghofe@12447
    16
haftmann@32358
    17
val const_of = dest_Const o head_of o fst o Logic.dest_equals;
haftmann@32358
    18
wenzelm@33522
    19
structure ModuleData = Theory_Data
wenzelm@22846
    20
(
haftmann@28522
    21
  type T = string Symtab.table;
berghofe@12447
    22
  val empty = Symtab.empty;
wenzelm@16424
    23
  val extend = I;
wenzelm@33522
    24
  fun merge data = Symtab.merge (K true) data;
wenzelm@22846
    25
);
berghofe@12447
    26
haftmann@31998
    27
fun add_thm_target module_name thm thy =
haftmann@31998
    28
  let
haftmann@31998
    29
    val (thm', _) = Code.mk_eqn thy (thm, true)
haftmann@31998
    30
  in
haftmann@31998
    31
    thy
haftmann@31998
    32
    |> ModuleData.map (Symtab.update (fst (Code.const_typ_eqn thy thm'), module_name))
haftmann@31998
    33
  end;
haftmann@24624
    34
haftmann@32358
    35
fun avoid_value thy [thm] =
haftmann@32358
    36
      let val (_, T) = Code.const_typ_eqn thy thm
haftmann@32358
    37
      in if null (Term.add_tvarsT T []) orelse (null o fst o strip_type) T
haftmann@32358
    38
        then [thm]
haftmann@34895
    39
        else [Code.expand_eta thy 1 thm]
haftmann@32358
    40
      end
haftmann@32358
    41
  | avoid_value thy thms = thms;
haftmann@28522
    42
haftmann@32358
    43
fun get_equations thy defs (raw_c, T) = if raw_c = @{const_name "op ="} then ([], "") else
haftmann@32358
    44
  let
haftmann@32358
    45
    val c = AxClass.unoverload_const thy (raw_c, T);
haftmann@34893
    46
    val raw_thms = Code.get_cert thy (Code_Preproc.preprocess_functrans thy) c
haftmann@34895
    47
      |> Code.equations_thms_cert thy
haftmann@34895
    48
      |> snd
haftmann@34895
    49
      |> map_filter (fn (_, (thm, proper)) => if proper then SOME thm else NONE)
haftmann@34891
    50
      |> map (AxClass.overload thy)
haftmann@32358
    51
      |> filter (is_instance T o snd o const_of o prop_of);
haftmann@32358
    52
    val module_name = case Symtab.lookup (ModuleData.get thy) c
haftmann@32358
    53
     of SOME module_name => module_name
haftmann@32358
    54
      | NONE => case get_defn thy defs c T
haftmann@32358
    55
         of SOME ((_, (thyname, _)), _) => thyname
haftmann@32358
    56
          | NONE => Codegen.thyname_of_const thy c;
haftmann@32358
    57
  in if null raw_thms then ([], "") else
haftmann@32358
    58
    raw_thms
haftmann@32358
    59
    |> preprocess thy
haftmann@32358
    60
    |> avoid_value thy
haftmann@32358
    61
    |> rpair module_name
haftmann@32358
    62
  end;
berghofe@12447
    63
berghofe@16645
    64
fun mk_suffix thy defs (s, T) = (case get_defn thy defs s T of
berghofe@17144
    65
  SOME (_, SOME i) => " def" ^ string_of_int i | _ => "");
berghofe@12447
    66
berghofe@12447
    67
exception EQN of string * typ * string;
berghofe@12447
    68
wenzelm@33244
    69
fun cycle g x xs =
haftmann@22887
    70
  if member (op =) xs x then xs
wenzelm@33244
    71
  else fold (cycle g) (flat (Graph.all_paths (fst g) (x, x))) (x :: xs);
berghofe@12447
    72
haftmann@28535
    73
fun add_rec_funs thy defs dep module eqs gr =
berghofe@12447
    74
  let
berghofe@16645
    75
    fun dest_eq t = (fst (const_of t) ^ mk_suffix thy defs (const_of t),
haftmann@32358
    76
      Logic.dest_equals (rename_term t));
berghofe@12447
    77
    val eqs' = map dest_eq eqs;
berghofe@12447
    78
    val (dname, _) :: _ = eqs';
berghofe@12447
    79
    val (s, T) = const_of (hd eqs);
berghofe@12447
    80
haftmann@28535
    81
    fun mk_fundef module fname first [] gr = ([], gr)
haftmann@28535
    82
      | mk_fundef module fname first ((fname' : string, (lhs, rhs)) :: xs) gr =
berghofe@12447
    83
      let
haftmann@28535
    84
        val (pl, gr1) = invoke_codegen thy defs dname module false lhs gr;
haftmann@28535
    85
        val (pr, gr2) = invoke_codegen thy defs dname module false rhs gr1;
haftmann@28535
    86
        val (rest, gr3) = mk_fundef module fname' false xs gr2 ;
haftmann@28535
    87
        val (ty, gr4) = invoke_tycodegen thy defs dname module false T gr3;
haftmann@28535
    88
        val num_args = (length o snd o strip_comb) lhs;
haftmann@28535
    89
        val prfx = if fname = fname' then "  |"
haftmann@28535
    90
          else if not first then "and"
haftmann@28535
    91
          else if num_args = 0 then "val"
haftmann@28535
    92
          else "fun";
haftmann@28535
    93
        val pl' = Pretty.breaks (str prfx
haftmann@28535
    94
          :: (if num_args = 0 then [pl, str ":", ty] else [pl]));
berghofe@12447
    95
      in
haftmann@28535
    96
        (Pretty.blk (4, pl'
haftmann@28535
    97
           @ [str " =", Pretty.brk 1, pr]) :: rest, gr4)
berghofe@12447
    98
      end;
berghofe@12447
    99
berghofe@17144
   100
    fun put_code module fundef = map_node dname
berghofe@26975
   101
      (K (SOME (EQN ("", dummyT, dname)), module, string_of (Pretty.blk (0,
berghofe@26975
   102
      separate Pretty.fbrk fundef @ [str ";"])) ^ "\n\n"));
berghofe@12447
   103
berghofe@12447
   104
  in
berghofe@17144
   105
    (case try (get_node gr) dname of
skalberg@15531
   106
       NONE =>
berghofe@12447
   107
         let
berghofe@17144
   108
           val gr1 = add_edge (dname, dep)
berghofe@17144
   109
             (new_node (dname, (SOME (EQN (s, T, "")), module, "")) gr);
haftmann@28535
   110
           val (fundef, gr2) = mk_fundef module "" true eqs' gr1 ;
wenzelm@33244
   111
           val xs = cycle gr2 dname [];
berghofe@17144
   112
           val cs = map (fn x => case get_node gr2 x of
berghofe@16645
   113
               (SOME (EQN (s, T, _)), _, _) => (s, T)
berghofe@12447
   114
             | _ => error ("RecfunCodegen: illegal cyclic dependencies:\n" ^
berghofe@12447
   115
                implode (separate ", " xs))) xs
berghofe@12447
   116
         in (case xs of
haftmann@28535
   117
             [_] => (module, put_code module fundef gr2)
berghofe@12447
   118
           | _ =>
berghofe@12447
   119
             if not (dep mem xs) then
berghofe@12447
   120
               let
berghofe@16645
   121
                 val thmss as (_, thyname) :: _ = map (get_equations thy defs) cs;
berghofe@17144
   122
                 val module' = if_library thyname module;
wenzelm@32952
   123
                 val eqs'' = map (dest_eq o prop_of) (maps fst thmss);
haftmann@28535
   124
                 val (fundef', gr3) = mk_fundef module' "" true eqs''
berghofe@17144
   125
                   (add_edge (dname, dep)
wenzelm@30190
   126
                     (List.foldr (uncurry new_node) (del_nodes xs gr2)
skalberg@15574
   127
                       (map (fn k =>
haftmann@28535
   128
                         (k, (SOME (EQN ("", dummyT, dname)), module', ""))) xs)))
haftmann@28535
   129
               in (module', put_code module' fundef' gr3) end
haftmann@28535
   130
             else (module, gr2))
berghofe@12447
   131
         end
berghofe@17144
   132
     | SOME (SOME (EQN (_, _, s)), module', _) =>
haftmann@28535
   133
         (module', if s = "" then
berghofe@17144
   134
            if dname = dep then gr else add_edge (dname, dep) gr
haftmann@28535
   135
          else if s = dep then gr else add_edge (s, dep) gr))
berghofe@12447
   136
  end;
berghofe@12447
   137
haftmann@28535
   138
fun recfun_codegen thy defs dep module brack t gr = (case strip_comb t of
haftmann@22921
   139
    (Const (p as (s, T)), ts) => (case (get_equations thy defs p, get_assoc_code thy (s, T)) of
berghofe@16645
   140
       (([], _), _) => NONE
skalberg@15531
   141
     | (_, SOME _) => NONE
berghofe@17144
   142
     | ((eqns, thyname), NONE) =>
berghofe@16645
   143
        let
berghofe@17144
   144
          val module' = if_library thyname module;
haftmann@28535
   145
          val (ps, gr') = fold_map
haftmann@28535
   146
            (invoke_codegen thy defs dep module true) ts gr;
berghofe@17144
   147
          val suffix = mk_suffix thy defs p;
haftmann@28535
   148
          val (module'', gr'') =
haftmann@28535
   149
            add_rec_funs thy defs dep module' (map prop_of eqns) gr';
haftmann@28535
   150
          val (fname, gr''') = mk_const_id module'' (s ^ suffix) gr''
berghofe@12447
   151
        in
haftmann@28535
   152
          SOME (mk_app brack (str (mk_qual_id module fname)) ps, gr''')
berghofe@12447
   153
        end)
skalberg@15531
   154
  | _ => NONE);
berghofe@12447
   155
haftmann@31998
   156
val setup = 
haftmann@24219
   157
  add_codegen "recfun" recfun_codegen
haftmann@31998
   158
  #> Code.set_code_target_attr add_thm_target;
berghofe@12447
   159
berghofe@12447
   160
end;