src/HOL/Tools/recfun_codegen.ML
author haftmann
Sat Aug 28 16:14:32 2010 +0200 (2010-08-28)
changeset 38864 4abe644fcea5
parent 36692 54b64d4ad524
child 40844 5895c525739d
permissions -rw-r--r--
formerly unnamed infix equality now named HOL.eq
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@38864
    43
fun get_equations thy defs (raw_c, T) = if raw_c = @{const_name HOL.eq} 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@35225
    47
      |> Code.bare_thms_of_cert thy
haftmann@34891
    48
      |> map (AxClass.overload thy)
haftmann@32358
    49
      |> filter (is_instance T o snd o const_of o prop_of);
haftmann@32358
    50
    val module_name = case Symtab.lookup (ModuleData.get thy) c
haftmann@32358
    51
     of SOME module_name => module_name
haftmann@32358
    52
      | NONE => case get_defn thy defs c T
haftmann@32358
    53
         of SOME ((_, (thyname, _)), _) => thyname
haftmann@32358
    54
          | NONE => Codegen.thyname_of_const thy c;
haftmann@32358
    55
  in if null raw_thms then ([], "") else
haftmann@32358
    56
    raw_thms
haftmann@32358
    57
    |> preprocess thy
haftmann@32358
    58
    |> avoid_value thy
haftmann@32358
    59
    |> rpair module_name
haftmann@32358
    60
  end;
berghofe@12447
    61
berghofe@16645
    62
fun mk_suffix thy defs (s, T) = (case get_defn thy defs s T of
berghofe@17144
    63
  SOME (_, SOME i) => " def" ^ string_of_int i | _ => "");
berghofe@12447
    64
berghofe@12447
    65
exception EQN of string * typ * string;
berghofe@12447
    66
wenzelm@33244
    67
fun cycle g x xs =
haftmann@22887
    68
  if member (op =) xs x then xs
wenzelm@33244
    69
  else fold (cycle g) (flat (Graph.all_paths (fst g) (x, x))) (x :: xs);
berghofe@12447
    70
haftmann@28535
    71
fun add_rec_funs thy defs dep module eqs gr =
berghofe@12447
    72
  let
berghofe@16645
    73
    fun dest_eq t = (fst (const_of t) ^ mk_suffix thy defs (const_of t),
haftmann@32358
    74
      Logic.dest_equals (rename_term t));
berghofe@12447
    75
    val eqs' = map dest_eq eqs;
berghofe@12447
    76
    val (dname, _) :: _ = eqs';
berghofe@12447
    77
    val (s, T) = const_of (hd eqs);
berghofe@12447
    78
haftmann@28535
    79
    fun mk_fundef module fname first [] gr = ([], gr)
haftmann@28535
    80
      | mk_fundef module fname first ((fname' : string, (lhs, rhs)) :: xs) gr =
berghofe@12447
    81
      let
haftmann@28535
    82
        val (pl, gr1) = invoke_codegen thy defs dname module false lhs gr;
haftmann@28535
    83
        val (pr, gr2) = invoke_codegen thy defs dname module false rhs gr1;
haftmann@28535
    84
        val (rest, gr3) = mk_fundef module fname' false xs gr2 ;
haftmann@28535
    85
        val (ty, gr4) = invoke_tycodegen thy defs dname module false T gr3;
haftmann@28535
    86
        val num_args = (length o snd o strip_comb) lhs;
haftmann@28535
    87
        val prfx = if fname = fname' then "  |"
haftmann@28535
    88
          else if not first then "and"
haftmann@28535
    89
          else if num_args = 0 then "val"
haftmann@28535
    90
          else "fun";
haftmann@28535
    91
        val pl' = Pretty.breaks (str prfx
haftmann@28535
    92
          :: (if num_args = 0 then [pl, str ":", ty] else [pl]));
berghofe@12447
    93
      in
haftmann@28535
    94
        (Pretty.blk (4, pl'
haftmann@28535
    95
           @ [str " =", Pretty.brk 1, pr]) :: rest, gr4)
berghofe@12447
    96
      end;
berghofe@12447
    97
berghofe@17144
    98
    fun put_code module fundef = map_node dname
berghofe@26975
    99
      (K (SOME (EQN ("", dummyT, dname)), module, string_of (Pretty.blk (0,
berghofe@26975
   100
      separate Pretty.fbrk fundef @ [str ";"])) ^ "\n\n"));
berghofe@12447
   101
berghofe@12447
   102
  in
berghofe@17144
   103
    (case try (get_node gr) dname of
skalberg@15531
   104
       NONE =>
berghofe@12447
   105
         let
berghofe@17144
   106
           val gr1 = add_edge (dname, dep)
berghofe@17144
   107
             (new_node (dname, (SOME (EQN (s, T, "")), module, "")) gr);
haftmann@28535
   108
           val (fundef, gr2) = mk_fundef module "" true eqs' gr1 ;
wenzelm@33244
   109
           val xs = cycle gr2 dname [];
berghofe@17144
   110
           val cs = map (fn x => case get_node gr2 x of
berghofe@16645
   111
               (SOME (EQN (s, T, _)), _, _) => (s, T)
berghofe@12447
   112
             | _ => error ("RecfunCodegen: illegal cyclic dependencies:\n" ^
berghofe@12447
   113
                implode (separate ", " xs))) xs
berghofe@12447
   114
         in (case xs of
haftmann@28535
   115
             [_] => (module, put_code module fundef gr2)
berghofe@12447
   116
           | _ =>
haftmann@36692
   117
             if not (member (op =) xs dep) then
berghofe@12447
   118
               let
berghofe@16645
   119
                 val thmss as (_, thyname) :: _ = map (get_equations thy defs) cs;
berghofe@17144
   120
                 val module' = if_library thyname module;
wenzelm@32952
   121
                 val eqs'' = map (dest_eq o prop_of) (maps fst thmss);
haftmann@28535
   122
                 val (fundef', gr3) = mk_fundef module' "" true eqs''
berghofe@17144
   123
                   (add_edge (dname, dep)
wenzelm@30190
   124
                     (List.foldr (uncurry new_node) (del_nodes xs gr2)
skalberg@15574
   125
                       (map (fn k =>
haftmann@28535
   126
                         (k, (SOME (EQN ("", dummyT, dname)), module', ""))) xs)))
haftmann@28535
   127
               in (module', put_code module' fundef' gr3) end
haftmann@28535
   128
             else (module, gr2))
berghofe@12447
   129
         end
berghofe@17144
   130
     | SOME (SOME (EQN (_, _, s)), module', _) =>
haftmann@28535
   131
         (module', if s = "" then
berghofe@17144
   132
            if dname = dep then gr else add_edge (dname, dep) gr
haftmann@28535
   133
          else if s = dep then gr else add_edge (s, dep) gr))
berghofe@12447
   134
  end;
berghofe@12447
   135
haftmann@28535
   136
fun recfun_codegen thy defs dep module brack t gr = (case strip_comb t of
haftmann@22921
   137
    (Const (p as (s, T)), ts) => (case (get_equations thy defs p, get_assoc_code thy (s, T)) of
berghofe@16645
   138
       (([], _), _) => NONE
skalberg@15531
   139
     | (_, SOME _) => NONE
berghofe@17144
   140
     | ((eqns, thyname), NONE) =>
berghofe@16645
   141
        let
berghofe@17144
   142
          val module' = if_library thyname module;
haftmann@28535
   143
          val (ps, gr') = fold_map
haftmann@28535
   144
            (invoke_codegen thy defs dep module true) ts gr;
berghofe@17144
   145
          val suffix = mk_suffix thy defs p;
haftmann@28535
   146
          val (module'', gr'') =
haftmann@28535
   147
            add_rec_funs thy defs dep module' (map prop_of eqns) gr';
haftmann@28535
   148
          val (fname, gr''') = mk_const_id module'' (s ^ suffix) gr''
berghofe@12447
   149
        in
haftmann@28535
   150
          SOME (mk_app brack (str (mk_qual_id module fname)) ps, gr''')
berghofe@12447
   151
        end)
skalberg@15531
   152
  | _ => NONE);
berghofe@12447
   153
haftmann@31998
   154
val setup = 
haftmann@24219
   155
  add_codegen "recfun" recfun_codegen
haftmann@31998
   156
  #> Code.set_code_target_attr add_thm_target;
berghofe@12447
   157
berghofe@12447
   158
end;