src/HOL/Tools/recfun_codegen.ML
author haftmann
Thu, 08 Jul 2010 16:19:24 +0200
changeset 37744 3daaf23b9ab4
parent 36692 54b64d4ad524
child 38864 4abe644fcea5
permissions -rw-r--r--
tuned titles
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
32358
98c00ee9e786 proper eta expansion in recfun_codegen.ML; no eta expansion at all in code_thingol.ML
haftmann
parents: 32353
diff changeset
    17
val const_of = dest_Const o head_of o fst o Logic.dest_equals;
98c00ee9e786 proper eta expansion in recfun_codegen.ML; no eta expansion at all in code_thingol.ML
haftmann
parents: 32353
diff changeset
    18
33522
737589bb9bb8 adapted Theory_Data;
wenzelm
parents: 33244
diff changeset
    19
structure ModuleData = Theory_Data
22846
fb79144af9a3 simplified DataFun interfaces;
wenzelm
parents: 22484
diff changeset
    20
(
28522
eacb54d9e78d only one theorem table for both code generators
haftmann
parents: 28370
diff changeset
    21
  type T = string Symtab.table;
12447
e752c9aecdec Code generator for recursive functions.
berghofe
parents:
diff changeset
    22
  val empty = Symtab.empty;
16424
18a07ad8fea8 accomodate change of TheoryDataFun;
wenzelm
parents: 15700
diff changeset
    23
  val extend = I;
33522
737589bb9bb8 adapted Theory_Data;
wenzelm
parents: 33244
diff changeset
    24
  fun merge data = Symtab.merge (K true) data;
22846
fb79144af9a3 simplified DataFun interfaces;
wenzelm
parents: 22484
diff changeset
    25
);
12447
e752c9aecdec Code generator for recursive functions.
berghofe
parents:
diff changeset
    26
31998
2c7a24f74db9 code attributes use common underscore convention
haftmann
parents: 31962
diff changeset
    27
fun add_thm_target module_name thm thy =
2c7a24f74db9 code attributes use common underscore convention
haftmann
parents: 31962
diff changeset
    28
  let
2c7a24f74db9 code attributes use common underscore convention
haftmann
parents: 31962
diff changeset
    29
    val (thm', _) = Code.mk_eqn thy (thm, true)
2c7a24f74db9 code attributes use common underscore convention
haftmann
parents: 31962
diff changeset
    30
  in
2c7a24f74db9 code attributes use common underscore convention
haftmann
parents: 31962
diff changeset
    31
    thy
2c7a24f74db9 code attributes use common underscore convention
haftmann
parents: 31962
diff changeset
    32
    |> ModuleData.map (Symtab.update (fst (Code.const_typ_eqn thy thm'), module_name))
2c7a24f74db9 code attributes use common underscore convention
haftmann
parents: 31962
diff changeset
    33
  end;
24624
b8383b1bbae3 distinction between regular and default code theorems
haftmann
parents: 24584
diff changeset
    34
32358
98c00ee9e786 proper eta expansion in recfun_codegen.ML; no eta expansion at all in code_thingol.ML
haftmann
parents: 32353
diff changeset
    35
fun avoid_value thy [thm] =
98c00ee9e786 proper eta expansion in recfun_codegen.ML; no eta expansion at all in code_thingol.ML
haftmann
parents: 32353
diff changeset
    36
      let val (_, T) = Code.const_typ_eqn thy thm
98c00ee9e786 proper eta expansion in recfun_codegen.ML; no eta expansion at all in code_thingol.ML
haftmann
parents: 32353
diff changeset
    37
      in if null (Term.add_tvarsT T []) orelse (null o fst o strip_type) T
98c00ee9e786 proper eta expansion in recfun_codegen.ML; no eta expansion at all in code_thingol.ML
haftmann
parents: 32353
diff changeset
    38
        then [thm]
34895
19fd499cddff explicit abstract type of code certificates
haftmann
parents: 34893
diff changeset
    39
        else [Code.expand_eta thy 1 thm]
32358
98c00ee9e786 proper eta expansion in recfun_codegen.ML; no eta expansion at all in code_thingol.ML
haftmann
parents: 32353
diff changeset
    40
      end
98c00ee9e786 proper eta expansion in recfun_codegen.ML; no eta expansion at all in code_thingol.ML
haftmann
parents: 32353
diff changeset
    41
  | avoid_value thy thms = thms;
28522
eacb54d9e78d only one theorem table for both code generators
haftmann
parents: 28370
diff changeset
    42
32358
98c00ee9e786 proper eta expansion in recfun_codegen.ML; no eta expansion at all in code_thingol.ML
haftmann
parents: 32353
diff changeset
    43
fun get_equations thy defs (raw_c, T) = if raw_c = @{const_name "op ="} then ([], "") else
98c00ee9e786 proper eta expansion in recfun_codegen.ML; no eta expansion at all in code_thingol.ML
haftmann
parents: 32353
diff changeset
    44
  let
98c00ee9e786 proper eta expansion in recfun_codegen.ML; no eta expansion at all in code_thingol.ML
haftmann
parents: 32353
diff changeset
    45
    val c = AxClass.unoverload_const thy (raw_c, T);
34893
ecdc526af73a function transformer preprocessor applies to both code generators
haftmann
parents: 34891
diff changeset
    46
    val raw_thms = Code.get_cert thy (Code_Preproc.preprocess_functrans thy) c
35225
dfbcff38c9ed using Code.bare_thms_of_cert
haftmann
parents: 34895
diff changeset
    47
      |> Code.bare_thms_of_cert thy
34891
99b9a6290446 code certificates as integral part of code generation
haftmann
parents: 33522
diff changeset
    48
      |> map (AxClass.overload thy)
32358
98c00ee9e786 proper eta expansion in recfun_codegen.ML; no eta expansion at all in code_thingol.ML
haftmann
parents: 32353
diff changeset
    49
      |> filter (is_instance T o snd o const_of o prop_of);
98c00ee9e786 proper eta expansion in recfun_codegen.ML; no eta expansion at all in code_thingol.ML
haftmann
parents: 32353
diff changeset
    50
    val module_name = case Symtab.lookup (ModuleData.get thy) c
98c00ee9e786 proper eta expansion in recfun_codegen.ML; no eta expansion at all in code_thingol.ML
haftmann
parents: 32353
diff changeset
    51
     of SOME module_name => module_name
98c00ee9e786 proper eta expansion in recfun_codegen.ML; no eta expansion at all in code_thingol.ML
haftmann
parents: 32353
diff changeset
    52
      | NONE => case get_defn thy defs c T
98c00ee9e786 proper eta expansion in recfun_codegen.ML; no eta expansion at all in code_thingol.ML
haftmann
parents: 32353
diff changeset
    53
         of SOME ((_, (thyname, _)), _) => thyname
98c00ee9e786 proper eta expansion in recfun_codegen.ML; no eta expansion at all in code_thingol.ML
haftmann
parents: 32353
diff changeset
    54
          | NONE => Codegen.thyname_of_const thy c;
98c00ee9e786 proper eta expansion in recfun_codegen.ML; no eta expansion at all in code_thingol.ML
haftmann
parents: 32353
diff changeset
    55
  in if null raw_thms then ([], "") else
98c00ee9e786 proper eta expansion in recfun_codegen.ML; no eta expansion at all in code_thingol.ML
haftmann
parents: 32353
diff changeset
    56
    raw_thms
98c00ee9e786 proper eta expansion in recfun_codegen.ML; no eta expansion at all in code_thingol.ML
haftmann
parents: 32353
diff changeset
    57
    |> preprocess thy
98c00ee9e786 proper eta expansion in recfun_codegen.ML; no eta expansion at all in code_thingol.ML
haftmann
parents: 32353
diff changeset
    58
    |> avoid_value thy
98c00ee9e786 proper eta expansion in recfun_codegen.ML; no eta expansion at all in code_thingol.ML
haftmann
parents: 32353
diff changeset
    59
    |> rpair module_name
98c00ee9e786 proper eta expansion in recfun_codegen.ML; no eta expansion at all in code_thingol.ML
haftmann
parents: 32353
diff changeset
    60
  end;
12447
e752c9aecdec Code generator for recursive functions.
berghofe
parents:
diff changeset
    61
16645
a152d6b21c31 Adapted to modular code generation.
berghofe
parents: 16424
diff changeset
    62
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
    63
  SOME (_, SOME i) => " def" ^ string_of_int i | _ => "");
12447
e752c9aecdec Code generator for recursive functions.
berghofe
parents:
diff changeset
    64
e752c9aecdec Code generator for recursive functions.
berghofe
parents:
diff changeset
    65
exception EQN of string * typ * string;
e752c9aecdec Code generator for recursive functions.
berghofe
parents:
diff changeset
    66
33244
db230399f890 Datatype.read_typ: standard argument order;
wenzelm
parents: 32952
diff changeset
    67
fun cycle g x xs =
22887
haftmann
parents: 22846
diff changeset
    68
  if member (op =) xs x then xs
33244
db230399f890 Datatype.read_typ: standard argument order;
wenzelm
parents: 32952
diff changeset
    69
  else fold (cycle g) (flat (Graph.all_paths (fst g) (x, x))) (x :: xs);
12447
e752c9aecdec Code generator for recursive functions.
berghofe
parents:
diff changeset
    70
28535
38fb0780b58b made SMLNJ happy
haftmann
parents: 28522
diff changeset
    71
fun add_rec_funs thy defs dep module eqs gr =
12447
e752c9aecdec Code generator for recursive functions.
berghofe
parents:
diff changeset
    72
  let
16645
a152d6b21c31 Adapted to modular code generation.
berghofe
parents: 16424
diff changeset
    73
    fun dest_eq t = (fst (const_of t) ^ mk_suffix thy defs (const_of t),
32358
98c00ee9e786 proper eta expansion in recfun_codegen.ML; no eta expansion at all in code_thingol.ML
haftmann
parents: 32353
diff changeset
    74
      Logic.dest_equals (rename_term t));
12447
e752c9aecdec Code generator for recursive functions.
berghofe
parents:
diff changeset
    75
    val eqs' = map dest_eq eqs;
e752c9aecdec Code generator for recursive functions.
berghofe
parents:
diff changeset
    76
    val (dname, _) :: _ = eqs';
e752c9aecdec Code generator for recursive functions.
berghofe
parents:
diff changeset
    77
    val (s, T) = const_of (hd eqs);
e752c9aecdec Code generator for recursive functions.
berghofe
parents:
diff changeset
    78
28535
38fb0780b58b made SMLNJ happy
haftmann
parents: 28522
diff changeset
    79
    fun mk_fundef module fname first [] gr = ([], gr)
38fb0780b58b made SMLNJ happy
haftmann
parents: 28522
diff changeset
    80
      | mk_fundef module fname first ((fname' : string, (lhs, rhs)) :: xs) gr =
12447
e752c9aecdec Code generator for recursive functions.
berghofe
parents:
diff changeset
    81
      let
28535
38fb0780b58b made SMLNJ happy
haftmann
parents: 28522
diff changeset
    82
        val (pl, gr1) = invoke_codegen thy defs dname module false lhs gr;
38fb0780b58b made SMLNJ happy
haftmann
parents: 28522
diff changeset
    83
        val (pr, gr2) = invoke_codegen thy defs dname module false rhs gr1;
38fb0780b58b made SMLNJ happy
haftmann
parents: 28522
diff changeset
    84
        val (rest, gr3) = mk_fundef module fname' false xs gr2 ;
38fb0780b58b made SMLNJ happy
haftmann
parents: 28522
diff changeset
    85
        val (ty, gr4) = invoke_tycodegen thy defs dname module false T gr3;
38fb0780b58b made SMLNJ happy
haftmann
parents: 28522
diff changeset
    86
        val num_args = (length o snd o strip_comb) lhs;
38fb0780b58b made SMLNJ happy
haftmann
parents: 28522
diff changeset
    87
        val prfx = if fname = fname' then "  |"
38fb0780b58b made SMLNJ happy
haftmann
parents: 28522
diff changeset
    88
          else if not first then "and"
38fb0780b58b made SMLNJ happy
haftmann
parents: 28522
diff changeset
    89
          else if num_args = 0 then "val"
38fb0780b58b made SMLNJ happy
haftmann
parents: 28522
diff changeset
    90
          else "fun";
38fb0780b58b made SMLNJ happy
haftmann
parents: 28522
diff changeset
    91
        val pl' = Pretty.breaks (str prfx
38fb0780b58b made SMLNJ happy
haftmann
parents: 28522
diff changeset
    92
          :: (if num_args = 0 then [pl, str ":", ty] else [pl]));
12447
e752c9aecdec Code generator for recursive functions.
berghofe
parents:
diff changeset
    93
      in
28535
38fb0780b58b made SMLNJ happy
haftmann
parents: 28522
diff changeset
    94
        (Pretty.blk (4, pl'
38fb0780b58b made SMLNJ happy
haftmann
parents: 28522
diff changeset
    95
           @ [str " =", Pretty.brk 1, pr]) :: rest, gr4)
12447
e752c9aecdec Code generator for recursive functions.
berghofe
parents:
diff changeset
    96
      end;
e752c9aecdec Code generator for recursive functions.
berghofe
parents:
diff changeset
    97
17144
6642e0f96f44 Implemented incremental code generation.
berghofe
parents: 16645
diff changeset
    98
    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
    99
      (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
   100
      separate Pretty.fbrk fundef @ [str ";"])) ^ "\n\n"));
12447
e752c9aecdec Code generator for recursive functions.
berghofe
parents:
diff changeset
   101
e752c9aecdec Code generator for recursive functions.
berghofe
parents:
diff changeset
   102
  in
17144
6642e0f96f44 Implemented incremental code generation.
berghofe
parents: 16645
diff changeset
   103
    (case try (get_node gr) dname of
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15321
diff changeset
   104
       NONE =>
12447
e752c9aecdec Code generator for recursive functions.
berghofe
parents:
diff changeset
   105
         let
17144
6642e0f96f44 Implemented incremental code generation.
berghofe
parents: 16645
diff changeset
   106
           val gr1 = add_edge (dname, dep)
6642e0f96f44 Implemented incremental code generation.
berghofe
parents: 16645
diff changeset
   107
             (new_node (dname, (SOME (EQN (s, T, "")), module, "")) gr);
28535
38fb0780b58b made SMLNJ happy
haftmann
parents: 28522
diff changeset
   108
           val (fundef, gr2) = mk_fundef module "" true eqs' gr1 ;
33244
db230399f890 Datatype.read_typ: standard argument order;
wenzelm
parents: 32952
diff changeset
   109
           val xs = cycle gr2 dname [];
17144
6642e0f96f44 Implemented incremental code generation.
berghofe
parents: 16645
diff changeset
   110
           val cs = map (fn x => case get_node gr2 x of
16645
a152d6b21c31 Adapted to modular code generation.
berghofe
parents: 16424
diff changeset
   111
               (SOME (EQN (s, T, _)), _, _) => (s, T)
12447
e752c9aecdec Code generator for recursive functions.
berghofe
parents:
diff changeset
   112
             | _ => error ("RecfunCodegen: illegal cyclic dependencies:\n" ^
e752c9aecdec Code generator for recursive functions.
berghofe
parents:
diff changeset
   113
                implode (separate ", " xs))) xs
e752c9aecdec Code generator for recursive functions.
berghofe
parents:
diff changeset
   114
         in (case xs of
28535
38fb0780b58b made SMLNJ happy
haftmann
parents: 28522
diff changeset
   115
             [_] => (module, put_code module fundef gr2)
12447
e752c9aecdec Code generator for recursive functions.
berghofe
parents:
diff changeset
   116
           | _ =>
36692
54b64d4ad524 farewell to old-style mem infixes -- type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
haftmann
parents: 35225
diff changeset
   117
             if not (member (op =) xs dep) then
12447
e752c9aecdec Code generator for recursive functions.
berghofe
parents:
diff changeset
   118
               let
16645
a152d6b21c31 Adapted to modular code generation.
berghofe
parents: 16424
diff changeset
   119
                 val thmss as (_, thyname) :: _ = map (get_equations thy defs) cs;
17144
6642e0f96f44 Implemented incremental code generation.
berghofe
parents: 16645
diff changeset
   120
                 val module' = if_library thyname module;
32952
aeb1e44fbc19 replaced String.concat by implode;
wenzelm
parents: 32927
diff changeset
   121
                 val eqs'' = map (dest_eq o prop_of) (maps fst thmss);
28535
38fb0780b58b made SMLNJ happy
haftmann
parents: 28522
diff changeset
   122
                 val (fundef', gr3) = mk_fundef module' "" true eqs''
17144
6642e0f96f44 Implemented incremental code generation.
berghofe
parents: 16645
diff changeset
   123
                   (add_edge (dname, dep)
30190
479806475f3c use long names for old-style fold combinators;
wenzelm
parents: 29272
diff changeset
   124
                     (List.foldr (uncurry new_node) (del_nodes xs gr2)
15574
b1d1b5bfc464 Removed practically all references to Library.foldr.
skalberg
parents: 15570
diff changeset
   125
                       (map (fn k =>
28535
38fb0780b58b made SMLNJ happy
haftmann
parents: 28522
diff changeset
   126
                         (k, (SOME (EQN ("", dummyT, dname)), module', ""))) xs)))
38fb0780b58b made SMLNJ happy
haftmann
parents: 28522
diff changeset
   127
               in (module', put_code module' fundef' gr3) end
38fb0780b58b made SMLNJ happy
haftmann
parents: 28522
diff changeset
   128
             else (module, gr2))
12447
e752c9aecdec Code generator for recursive functions.
berghofe
parents:
diff changeset
   129
         end
17144
6642e0f96f44 Implemented incremental code generation.
berghofe
parents: 16645
diff changeset
   130
     | SOME (SOME (EQN (_, _, s)), module', _) =>
28535
38fb0780b58b made SMLNJ happy
haftmann
parents: 28522
diff changeset
   131
         (module', if s = "" then
17144
6642e0f96f44 Implemented incremental code generation.
berghofe
parents: 16645
diff changeset
   132
            if dname = dep then gr else add_edge (dname, dep) gr
28535
38fb0780b58b made SMLNJ happy
haftmann
parents: 28522
diff changeset
   133
          else if s = dep then gr else add_edge (s, dep) gr))
12447
e752c9aecdec Code generator for recursive functions.
berghofe
parents:
diff changeset
   134
  end;
e752c9aecdec Code generator for recursive functions.
berghofe
parents:
diff changeset
   135
28535
38fb0780b58b made SMLNJ happy
haftmann
parents: 28522
diff changeset
   136
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
   137
    (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
   138
       (([], _), _) => NONE
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15321
diff changeset
   139
     | (_, SOME _) => NONE
17144
6642e0f96f44 Implemented incremental code generation.
berghofe
parents: 16645
diff changeset
   140
     | ((eqns, thyname), NONE) =>
16645
a152d6b21c31 Adapted to modular code generation.
berghofe
parents: 16424
diff changeset
   141
        let
17144
6642e0f96f44 Implemented incremental code generation.
berghofe
parents: 16645
diff changeset
   142
          val module' = if_library thyname module;
28535
38fb0780b58b made SMLNJ happy
haftmann
parents: 28522
diff changeset
   143
          val (ps, gr') = fold_map
38fb0780b58b made SMLNJ happy
haftmann
parents: 28522
diff changeset
   144
            (invoke_codegen thy defs dep module true) ts gr;
17144
6642e0f96f44 Implemented incremental code generation.
berghofe
parents: 16645
diff changeset
   145
          val suffix = mk_suffix thy defs p;
28535
38fb0780b58b made SMLNJ happy
haftmann
parents: 28522
diff changeset
   146
          val (module'', gr'') =
38fb0780b58b made SMLNJ happy
haftmann
parents: 28522
diff changeset
   147
            add_rec_funs thy defs dep module' (map prop_of eqns) gr';
38fb0780b58b made SMLNJ happy
haftmann
parents: 28522
diff changeset
   148
          val (fname, gr''') = mk_const_id module'' (s ^ suffix) gr''
12447
e752c9aecdec Code generator for recursive functions.
berghofe
parents:
diff changeset
   149
        in
28535
38fb0780b58b made SMLNJ happy
haftmann
parents: 28522
diff changeset
   150
          SOME (mk_app brack (str (mk_qual_id module fname)) ps, gr''')
12447
e752c9aecdec Code generator for recursive functions.
berghofe
parents:
diff changeset
   151
        end)
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15321
diff changeset
   152
  | _ => NONE);
12447
e752c9aecdec Code generator for recursive functions.
berghofe
parents:
diff changeset
   153
31998
2c7a24f74db9 code attributes use common underscore convention
haftmann
parents: 31962
diff changeset
   154
val setup = 
24219
e558fe311376 new structure for code generator modules
haftmann
parents: 22921
diff changeset
   155
  add_codegen "recfun" recfun_codegen
31998
2c7a24f74db9 code attributes use common underscore convention
haftmann
parents: 31962
diff changeset
   156
  #> Code.set_code_target_attr add_thm_target;
12447
e752c9aecdec Code generator for recursive functions.
berghofe
parents:
diff changeset
   157
e752c9aecdec Code generator for recursive functions.
berghofe
parents:
diff changeset
   158
end;