src/HOL/Tools/recfun_codegen.ML
author wenzelm
Sun, 01 Mar 2009 23:36:12 +0100
changeset 30190 479806475f3c
parent 29272 fb3ccf499df5
child 31036 64ff53fc0c0c
permissions -rw-r--r--
use long names for old-style fold combinators;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
24584
01e83ffa6c54 fixed title
haftmann
parents: 24219
diff changeset
     1
(*  Title:      HOL/Tools/recfun_codegen.ML
12447
e752c9aecdec Code generator for recursive functions.
berghofe
parents:
diff changeset
     2
    Author:     Stefan Berghofer, TU Muenchen
e752c9aecdec Code generator for recursive functions.
berghofe
parents:
diff changeset
     3
e752c9aecdec Code generator for recursive functions.
berghofe
parents:
diff changeset
     4
Code generator for recursive functions.
e752c9aecdec Code generator for recursive functions.
berghofe
parents:
diff changeset
     5
*)
e752c9aecdec Code generator for recursive functions.
berghofe
parents:
diff changeset
     6
e752c9aecdec Code generator for recursive functions.
berghofe
parents:
diff changeset
     7
signature RECFUN_CODEGEN =
e752c9aecdec Code generator for recursive functions.
berghofe
parents:
diff changeset
     8
sig
18708
4b3dadb4fe33 setup: theory -> theory;
wenzelm
parents: 18702
diff changeset
     9
  val setup: theory -> theory
12447
e752c9aecdec Code generator for recursive functions.
berghofe
parents:
diff changeset
    10
end;
e752c9aecdec Code generator for recursive functions.
berghofe
parents:
diff changeset
    11
e752c9aecdec Code generator for recursive functions.
berghofe
parents:
diff changeset
    12
structure RecfunCodegen : RECFUN_CODEGEN =
e752c9aecdec Code generator for recursive functions.
berghofe
parents:
diff changeset
    13
struct
e752c9aecdec Code generator for recursive functions.
berghofe
parents:
diff changeset
    14
e752c9aecdec Code generator for recursive functions.
berghofe
parents:
diff changeset
    15
open Codegen;
e752c9aecdec Code generator for recursive functions.
berghofe
parents:
diff changeset
    16
28522
eacb54d9e78d only one theorem table for both code generators
haftmann
parents: 28370
diff changeset
    17
structure ModuleData = TheoryDataFun
22846
fb79144af9a3 simplified DataFun interfaces;
wenzelm
parents: 22484
diff changeset
    18
(
28522
eacb54d9e78d only one theorem table for both code generators
haftmann
parents: 28370
diff changeset
    19
  type T = string Symtab.table;
12447
e752c9aecdec Code generator for recursive functions.
berghofe
parents:
diff changeset
    20
  val empty = Symtab.empty;
e752c9aecdec Code generator for recursive functions.
berghofe
parents:
diff changeset
    21
  val copy = I;
16424
18a07ad8fea8 accomodate change of TheoryDataFun;
wenzelm
parents: 15700
diff changeset
    22
  val extend = I;
28522
eacb54d9e78d only one theorem table for both code generators
haftmann
parents: 28370
diff changeset
    23
  fun merge _ = Symtab.merge (K true);
22846
fb79144af9a3 simplified DataFun interfaces;
wenzelm
parents: 22484
diff changeset
    24
);
12447
e752c9aecdec Code generator for recursive functions.
berghofe
parents:
diff changeset
    25
28703
aef727ef30e5 cleanup code default attribute
haftmann
parents: 28535
diff changeset
    26
fun add_thm NONE thm thy = Code.add_eqn thm thy
aef727ef30e5 cleanup code default attribute
haftmann
parents: 28535
diff changeset
    27
  | add_thm (SOME module_name) thm thy =
28522
eacb54d9e78d only one theorem table for both code generators
haftmann
parents: 28370
diff changeset
    28
      case Code_Unit.warning_thm (Code_Unit.mk_eqn thy) thm
eacb54d9e78d only one theorem table for both code generators
haftmann
parents: 28370
diff changeset
    29
       of SOME (thm', _) => let val c = Code_Unit.const_eqn thm'
eacb54d9e78d only one theorem table for both code generators
haftmann
parents: 28370
diff changeset
    30
            in thy
eacb54d9e78d only one theorem table for both code generators
haftmann
parents: 28370
diff changeset
    31
              |> ModuleData.map (Symtab.update (c, module_name))
28703
aef727ef30e5 cleanup code default attribute
haftmann
parents: 28535
diff changeset
    32
              |> Code.add_eqn thm'
28522
eacb54d9e78d only one theorem table for both code generators
haftmann
parents: 28370
diff changeset
    33
            end
28703
aef727ef30e5 cleanup code default attribute
haftmann
parents: 28535
diff changeset
    34
        | NONE => Code.add_eqn thm thy;
24624
b8383b1bbae3 distinction between regular and default code theorems
haftmann
parents: 24584
diff changeset
    35
28522
eacb54d9e78d only one theorem table for both code generators
haftmann
parents: 28370
diff changeset
    36
fun meta_eq_to_obj_eq thy thm =
eacb54d9e78d only one theorem table for both code generators
haftmann
parents: 28370
diff changeset
    37
  let
eacb54d9e78d only one theorem table for both code generators
haftmann
parents: 28370
diff changeset
    38
    val T = (fastype_of o fst o Logic.dest_equals o Thm.prop_of) thm;
eacb54d9e78d only one theorem table for both code generators
haftmann
parents: 28370
diff changeset
    39
  in if Sign.of_sort thy (T, @{sort type})
eacb54d9e78d only one theorem table for both code generators
haftmann
parents: 28370
diff changeset
    40
    then SOME (Conv.fconv_rule Drule.beta_eta_conversion (@{thm meta_eq_to_obj_eq} OF [thm]))
eacb54d9e78d only one theorem table for both code generators
haftmann
parents: 28370
diff changeset
    41
    else NONE
eacb54d9e78d only one theorem table for both code generators
haftmann
parents: 28370
diff changeset
    42
  end;
19344
b4e00947c8a1 added hook for codegen_theorems.ML
haftmann
parents: 19202
diff changeset
    43
28522
eacb54d9e78d only one theorem table for both code generators
haftmann
parents: 28370
diff changeset
    44
fun expand_eta thy [] = []
eacb54d9e78d only one theorem table for both code generators
haftmann
parents: 28370
diff changeset
    45
  | expand_eta thy (thms as thm :: _) =
eacb54d9e78d only one theorem table for both code generators
haftmann
parents: 28370
diff changeset
    46
      let
eacb54d9e78d only one theorem table for both code generators
haftmann
parents: 28370
diff changeset
    47
        val (_, ty) = Code_Unit.const_typ_eqn thm;
29272
fb3ccf499df5 use regular Term.add_XXX etc.;
wenzelm
parents: 28703
diff changeset
    48
      in if null (Term.add_tvarsT ty []) orelse (null o fst o strip_type) ty
28522
eacb54d9e78d only one theorem table for both code generators
haftmann
parents: 28370
diff changeset
    49
        then thms
eacb54d9e78d only one theorem table for both code generators
haftmann
parents: 28370
diff changeset
    50
        else map (Code_Unit.expand_eta thy 1) thms
eacb54d9e78d only one theorem table for both code generators
haftmann
parents: 28370
diff changeset
    51
      end;
14196
be5e838f37bd Added "del" attribute for deleting equations.
berghofe
parents: 13105
diff changeset
    52
28522
eacb54d9e78d only one theorem table for both code generators
haftmann
parents: 28370
diff changeset
    53
fun retrieve_equations thy (c, T) = if c = @{const_name "op ="} then NONE else
eacb54d9e78d only one theorem table for both code generators
haftmann
parents: 28370
diff changeset
    54
  let
eacb54d9e78d only one theorem table for both code generators
haftmann
parents: 28370
diff changeset
    55
    val c' = AxClass.unoverload_const thy (c, T);
eacb54d9e78d only one theorem table for both code generators
haftmann
parents: 28370
diff changeset
    56
    val opt_name = Symtab.lookup (ModuleData.get thy) c';
eacb54d9e78d only one theorem table for both code generators
haftmann
parents: 28370
diff changeset
    57
    val thms = Code.these_raw_eqns thy c'
eacb54d9e78d only one theorem table for both code generators
haftmann
parents: 28370
diff changeset
    58
      |> map_filter (fn (thm, linear) => if linear then SOME thm else NONE)
eacb54d9e78d only one theorem table for both code generators
haftmann
parents: 28370
diff changeset
    59
      |> expand_eta thy
eacb54d9e78d only one theorem table for both code generators
haftmann
parents: 28370
diff changeset
    60
      |> map (AxClass.overload thy)
eacb54d9e78d only one theorem table for both code generators
haftmann
parents: 28370
diff changeset
    61
      |> map_filter (meta_eq_to_obj_eq thy)
eacb54d9e78d only one theorem table for both code generators
haftmann
parents: 28370
diff changeset
    62
      |> Code_Unit.norm_varnames thy Code_Name.purify_tvar Code_Name.purify_var
eacb54d9e78d only one theorem table for both code generators
haftmann
parents: 28370
diff changeset
    63
      |> map (rpair opt_name)
eacb54d9e78d only one theorem table for both code generators
haftmann
parents: 28370
diff changeset
    64
  in if null thms then NONE else SOME thms end;
eacb54d9e78d only one theorem table for both code generators
haftmann
parents: 28370
diff changeset
    65
eacb54d9e78d only one theorem table for both code generators
haftmann
parents: 28370
diff changeset
    66
val dest_eqn = HOLogic.dest_eq o HOLogic.dest_Trueprop;
eacb54d9e78d only one theorem table for both code generators
haftmann
parents: 28370
diff changeset
    67
val const_of = dest_Const o head_of o fst o dest_eqn;
15321
694f9d3ce90d Reimplemented some operations on "code lemma" table to avoid that code
berghofe
parents: 15257
diff changeset
    68
16645
a152d6b21c31 Adapted to modular code generation.
berghofe
parents: 16424
diff changeset
    69
fun get_equations thy defs (s, T) =
28522
eacb54d9e78d only one theorem table for both code generators
haftmann
parents: 28370
diff changeset
    70
  (case retrieve_equations thy (s, T) of
16645
a152d6b21c31 Adapted to modular code generation.
berghofe
parents: 16424
diff changeset
    71
     NONE => ([], "")
a152d6b21c31 Adapted to modular code generation.
berghofe
parents: 16424
diff changeset
    72
   | SOME thms => 
28522
eacb54d9e78d only one theorem table for both code generators
haftmann
parents: 28370
diff changeset
    73
       let val thms' = filter (fn (thm, _) => is_instance T
eacb54d9e78d only one theorem table for both code generators
haftmann
parents: 28370
diff changeset
    74
           (snd (const_of (prop_of thm)))) thms
16645
a152d6b21c31 Adapted to modular code generation.
berghofe
parents: 16424
diff changeset
    75
       in if null thms' then ([], "")
a152d6b21c31 Adapted to modular code generation.
berghofe
parents: 16424
diff changeset
    76
         else (preprocess thy (map fst thms'),
a152d6b21c31 Adapted to modular code generation.
berghofe
parents: 16424
diff changeset
    77
           case snd (snd (split_last thms')) of
a152d6b21c31 Adapted to modular code generation.
berghofe
parents: 16424
diff changeset
    78
               NONE => (case get_defn thy defs s T of
27398
768da1da59d6 simplified retrieval of theory names of consts and types
haftmann
parents: 26975
diff changeset
    79
                   NONE => Codegen.thyname_of_const thy s
16645
a152d6b21c31 Adapted to modular code generation.
berghofe
parents: 16424
diff changeset
    80
                 | SOME ((_, (thyname, _)), _) => thyname)
a152d6b21c31 Adapted to modular code generation.
berghofe
parents: 16424
diff changeset
    81
             | SOME thyname => thyname)
a152d6b21c31 Adapted to modular code generation.
berghofe
parents: 16424
diff changeset
    82
       end);
12447
e752c9aecdec Code generator for recursive functions.
berghofe
parents:
diff changeset
    83
16645
a152d6b21c31 Adapted to modular code generation.
berghofe
parents: 16424
diff changeset
    84
fun mk_suffix thy defs (s, T) = (case get_defn thy defs s T of
17144
6642e0f96f44 Implemented incremental code generation.
berghofe
parents: 16645
diff changeset
    85
  SOME (_, SOME i) => " def" ^ string_of_int i | _ => "");
12447
e752c9aecdec Code generator for recursive functions.
berghofe
parents:
diff changeset
    86
e752c9aecdec Code generator for recursive functions.
berghofe
parents:
diff changeset
    87
exception EQN of string * typ * string;
e752c9aecdec Code generator for recursive functions.
berghofe
parents:
diff changeset
    88
22887
haftmann
parents: 22846
diff changeset
    89
fun cycle g (xs, x : string) =
haftmann
parents: 22846
diff changeset
    90
  if member (op =) xs x then xs
haftmann
parents: 22846
diff changeset
    91
  else Library.foldl (cycle g) (x :: xs, flat (Graph.all_paths (fst g) (x, x)));
12447
e752c9aecdec Code generator for recursive functions.
berghofe
parents:
diff changeset
    92
28535
38fb0780b58b made SMLNJ happy
haftmann
parents: 28522
diff changeset
    93
fun add_rec_funs thy defs dep module eqs gr =
12447
e752c9aecdec Code generator for recursive functions.
berghofe
parents:
diff changeset
    94
  let
16645
a152d6b21c31 Adapted to modular code generation.
berghofe
parents: 16424
diff changeset
    95
    fun dest_eq t = (fst (const_of t) ^ mk_suffix thy defs (const_of t),
a152d6b21c31 Adapted to modular code generation.
berghofe
parents: 16424
diff changeset
    96
      dest_eqn (rename_term t));
12447
e752c9aecdec Code generator for recursive functions.
berghofe
parents:
diff changeset
    97
    val eqs' = map dest_eq eqs;
e752c9aecdec Code generator for recursive functions.
berghofe
parents:
diff changeset
    98
    val (dname, _) :: _ = eqs';
e752c9aecdec Code generator for recursive functions.
berghofe
parents:
diff changeset
    99
    val (s, T) = const_of (hd eqs);
e752c9aecdec Code generator for recursive functions.
berghofe
parents:
diff changeset
   100
28535
38fb0780b58b made SMLNJ happy
haftmann
parents: 28522
diff changeset
   101
    fun mk_fundef module fname first [] gr = ([], gr)
38fb0780b58b made SMLNJ happy
haftmann
parents: 28522
diff changeset
   102
      | mk_fundef module fname first ((fname' : string, (lhs, rhs)) :: xs) gr =
12447
e752c9aecdec Code generator for recursive functions.
berghofe
parents:
diff changeset
   103
      let
28535
38fb0780b58b made SMLNJ happy
haftmann
parents: 28522
diff changeset
   104
        val (pl, gr1) = invoke_codegen thy defs dname module false lhs gr;
38fb0780b58b made SMLNJ happy
haftmann
parents: 28522
diff changeset
   105
        val (pr, gr2) = invoke_codegen thy defs dname module false rhs gr1;
38fb0780b58b made SMLNJ happy
haftmann
parents: 28522
diff changeset
   106
        val (rest, gr3) = mk_fundef module fname' false xs gr2 ;
38fb0780b58b made SMLNJ happy
haftmann
parents: 28522
diff changeset
   107
        val (ty, gr4) = invoke_tycodegen thy defs dname module false T gr3;
38fb0780b58b made SMLNJ happy
haftmann
parents: 28522
diff changeset
   108
        val num_args = (length o snd o strip_comb) lhs;
38fb0780b58b made SMLNJ happy
haftmann
parents: 28522
diff changeset
   109
        val prfx = if fname = fname' then "  |"
38fb0780b58b made SMLNJ happy
haftmann
parents: 28522
diff changeset
   110
          else if not first then "and"
38fb0780b58b made SMLNJ happy
haftmann
parents: 28522
diff changeset
   111
          else if num_args = 0 then "val"
38fb0780b58b made SMLNJ happy
haftmann
parents: 28522
diff changeset
   112
          else "fun";
38fb0780b58b made SMLNJ happy
haftmann
parents: 28522
diff changeset
   113
        val pl' = Pretty.breaks (str prfx
38fb0780b58b made SMLNJ happy
haftmann
parents: 28522
diff changeset
   114
          :: (if num_args = 0 then [pl, str ":", ty] else [pl]));
12447
e752c9aecdec Code generator for recursive functions.
berghofe
parents:
diff changeset
   115
      in
28535
38fb0780b58b made SMLNJ happy
haftmann
parents: 28522
diff changeset
   116
        (Pretty.blk (4, pl'
38fb0780b58b made SMLNJ happy
haftmann
parents: 28522
diff changeset
   117
           @ [str " =", Pretty.brk 1, pr]) :: rest, gr4)
12447
e752c9aecdec Code generator for recursive functions.
berghofe
parents:
diff changeset
   118
      end;
e752c9aecdec Code generator for recursive functions.
berghofe
parents:
diff changeset
   119
17144
6642e0f96f44 Implemented incremental code generation.
berghofe
parents: 16645
diff changeset
   120
    fun put_code module fundef = map_node dname
26975
103dca19ef2e Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents: 26928
diff changeset
   121
      (K (SOME (EQN ("", dummyT, dname)), module, string_of (Pretty.blk (0,
103dca19ef2e Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents: 26928
diff changeset
   122
      separate Pretty.fbrk fundef @ [str ";"])) ^ "\n\n"));
12447
e752c9aecdec Code generator for recursive functions.
berghofe
parents:
diff changeset
   123
e752c9aecdec Code generator for recursive functions.
berghofe
parents:
diff changeset
   124
  in
17144
6642e0f96f44 Implemented incremental code generation.
berghofe
parents: 16645
diff changeset
   125
    (case try (get_node gr) dname of
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15321
diff changeset
   126
       NONE =>
12447
e752c9aecdec Code generator for recursive functions.
berghofe
parents:
diff changeset
   127
         let
17144
6642e0f96f44 Implemented incremental code generation.
berghofe
parents: 16645
diff changeset
   128
           val gr1 = add_edge (dname, dep)
6642e0f96f44 Implemented incremental code generation.
berghofe
parents: 16645
diff changeset
   129
             (new_node (dname, (SOME (EQN (s, T, "")), module, "")) gr);
28535
38fb0780b58b made SMLNJ happy
haftmann
parents: 28522
diff changeset
   130
           val (fundef, gr2) = mk_fundef module "" true eqs' gr1 ;
12447
e752c9aecdec Code generator for recursive functions.
berghofe
parents:
diff changeset
   131
           val xs = cycle gr2 ([], dname);
17144
6642e0f96f44 Implemented incremental code generation.
berghofe
parents: 16645
diff changeset
   132
           val cs = map (fn x => case get_node gr2 x of
16645
a152d6b21c31 Adapted to modular code generation.
berghofe
parents: 16424
diff changeset
   133
               (SOME (EQN (s, T, _)), _, _) => (s, T)
12447
e752c9aecdec Code generator for recursive functions.
berghofe
parents:
diff changeset
   134
             | _ => error ("RecfunCodegen: illegal cyclic dependencies:\n" ^
e752c9aecdec Code generator for recursive functions.
berghofe
parents:
diff changeset
   135
                implode (separate ", " xs))) xs
e752c9aecdec Code generator for recursive functions.
berghofe
parents:
diff changeset
   136
         in (case xs of
28535
38fb0780b58b made SMLNJ happy
haftmann
parents: 28522
diff changeset
   137
             [_] => (module, put_code module fundef gr2)
12447
e752c9aecdec Code generator for recursive functions.
berghofe
parents:
diff changeset
   138
           | _ =>
e752c9aecdec Code generator for recursive functions.
berghofe
parents:
diff changeset
   139
             if not (dep mem xs) then
e752c9aecdec Code generator for recursive functions.
berghofe
parents:
diff changeset
   140
               let
16645
a152d6b21c31 Adapted to modular code generation.
berghofe
parents: 16424
diff changeset
   141
                 val thmss as (_, thyname) :: _ = map (get_equations thy defs) cs;
17144
6642e0f96f44 Implemented incremental code generation.
berghofe
parents: 16645
diff changeset
   142
                 val module' = if_library thyname module;
16645
a152d6b21c31 Adapted to modular code generation.
berghofe
parents: 16424
diff changeset
   143
                 val eqs'' = map (dest_eq o prop_of) (List.concat (map fst thmss));
28535
38fb0780b58b made SMLNJ happy
haftmann
parents: 28522
diff changeset
   144
                 val (fundef', gr3) = mk_fundef module' "" true eqs''
17144
6642e0f96f44 Implemented incremental code generation.
berghofe
parents: 16645
diff changeset
   145
                   (add_edge (dname, dep)
30190
479806475f3c use long names for old-style fold combinators;
wenzelm
parents: 29272
diff changeset
   146
                     (List.foldr (uncurry new_node) (del_nodes xs gr2)
15574
b1d1b5bfc464 Removed practically all references to Library.foldr.
skalberg
parents: 15570
diff changeset
   147
                       (map (fn k =>
28535
38fb0780b58b made SMLNJ happy
haftmann
parents: 28522
diff changeset
   148
                         (k, (SOME (EQN ("", dummyT, dname)), module', ""))) xs)))
38fb0780b58b made SMLNJ happy
haftmann
parents: 28522
diff changeset
   149
               in (module', put_code module' fundef' gr3) end
38fb0780b58b made SMLNJ happy
haftmann
parents: 28522
diff changeset
   150
             else (module, gr2))
12447
e752c9aecdec Code generator for recursive functions.
berghofe
parents:
diff changeset
   151
         end
17144
6642e0f96f44 Implemented incremental code generation.
berghofe
parents: 16645
diff changeset
   152
     | SOME (SOME (EQN (_, _, s)), module', _) =>
28535
38fb0780b58b made SMLNJ happy
haftmann
parents: 28522
diff changeset
   153
         (module', if s = "" then
17144
6642e0f96f44 Implemented incremental code generation.
berghofe
parents: 16645
diff changeset
   154
            if dname = dep then gr else add_edge (dname, dep) gr
28535
38fb0780b58b made SMLNJ happy
haftmann
parents: 28522
diff changeset
   155
          else if s = dep then gr else add_edge (s, dep) gr))
12447
e752c9aecdec Code generator for recursive functions.
berghofe
parents:
diff changeset
   156
  end;
e752c9aecdec Code generator for recursive functions.
berghofe
parents:
diff changeset
   157
28535
38fb0780b58b made SMLNJ happy
haftmann
parents: 28522
diff changeset
   158
fun recfun_codegen thy defs dep module brack t gr = (case strip_comb t of
22921
475ff421a6a3 consts in consts_code Isar commands are now referred to by usual term syntax
haftmann
parents: 22887
diff changeset
   159
    (Const (p as (s, T)), ts) => (case (get_equations thy defs p, get_assoc_code thy (s, T)) of
16645
a152d6b21c31 Adapted to modular code generation.
berghofe
parents: 16424
diff changeset
   160
       (([], _), _) => NONE
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15321
diff changeset
   161
     | (_, SOME _) => NONE
17144
6642e0f96f44 Implemented incremental code generation.
berghofe
parents: 16645
diff changeset
   162
     | ((eqns, thyname), NONE) =>
16645
a152d6b21c31 Adapted to modular code generation.
berghofe
parents: 16424
diff changeset
   163
        let
17144
6642e0f96f44 Implemented incremental code generation.
berghofe
parents: 16645
diff changeset
   164
          val module' = if_library thyname module;
28535
38fb0780b58b made SMLNJ happy
haftmann
parents: 28522
diff changeset
   165
          val (ps, gr') = fold_map
38fb0780b58b made SMLNJ happy
haftmann
parents: 28522
diff changeset
   166
            (invoke_codegen thy defs dep module true) ts gr;
17144
6642e0f96f44 Implemented incremental code generation.
berghofe
parents: 16645
diff changeset
   167
          val suffix = mk_suffix thy defs p;
28535
38fb0780b58b made SMLNJ happy
haftmann
parents: 28522
diff changeset
   168
          val (module'', gr'') =
38fb0780b58b made SMLNJ happy
haftmann
parents: 28522
diff changeset
   169
            add_rec_funs thy defs dep module' (map prop_of eqns) gr';
38fb0780b58b made SMLNJ happy
haftmann
parents: 28522
diff changeset
   170
          val (fname, gr''') = mk_const_id module'' (s ^ suffix) gr''
12447
e752c9aecdec Code generator for recursive functions.
berghofe
parents:
diff changeset
   171
        in
28535
38fb0780b58b made SMLNJ happy
haftmann
parents: 28522
diff changeset
   172
          SOME (mk_app brack (str (mk_qual_id module fname)) ps, gr''')
12447
e752c9aecdec Code generator for recursive functions.
berghofe
parents:
diff changeset
   173
        end)
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15321
diff changeset
   174
  | _ => NONE);
12447
e752c9aecdec Code generator for recursive functions.
berghofe
parents:
diff changeset
   175
28703
aef727ef30e5 cleanup code default attribute
haftmann
parents: 28535
diff changeset
   176
val setup = let
aef727ef30e5 cleanup code default attribute
haftmann
parents: 28535
diff changeset
   177
  fun add opt_module = Thm.declaration_attribute (fn thm => Context.mapping
aef727ef30e5 cleanup code default attribute
haftmann
parents: 28535
diff changeset
   178
    (add_thm opt_module thm) I);
aef727ef30e5 cleanup code default attribute
haftmann
parents: 28535
diff changeset
   179
  val del = Thm.declaration_attribute (fn thm => Context.mapping
aef727ef30e5 cleanup code default attribute
haftmann
parents: 28535
diff changeset
   180
    (Code.del_eqn thm) I);
aef727ef30e5 cleanup code default attribute
haftmann
parents: 28535
diff changeset
   181
in
24219
e558fe311376 new structure for code generator modules
haftmann
parents: 22921
diff changeset
   182
  add_codegen "recfun" recfun_codegen
e558fe311376 new structure for code generator modules
haftmann
parents: 22921
diff changeset
   183
  #> Code.add_attribute ("", Args.del |-- Scan.succeed del
28703
aef727ef30e5 cleanup code default attribute
haftmann
parents: 28535
diff changeset
   184
     || Scan.option (Args.$$$ "target" |-- Args.colon |-- Args.name) >> add)
aef727ef30e5 cleanup code default attribute
haftmann
parents: 28535
diff changeset
   185
end;
12447
e752c9aecdec Code generator for recursive functions.
berghofe
parents:
diff changeset
   186
e752c9aecdec Code generator for recursive functions.
berghofe
parents:
diff changeset
   187
end;