src/HOL/Tools/recfun_codegen.ML
author krauss
Fri Nov 24 13:44:51 2006 +0100 (2006-11-24)
changeset 21512 3786eb1b69d6
parent 21410 c212b002fc8c
child 22360 26ead7ed4f4b
permissions -rw-r--r--
Lemma "fundef_default_value" uses predicate instead of set.
     1 (*  Title:      HOL/recfun_codegen.ML
     2     ID:         $Id$
     3     Author:     Stefan Berghofer, TU Muenchen
     4 
     5 Code generator for recursive functions.
     6 *)
     7 
     8 signature RECFUN_CODEGEN =
     9 sig
    10   val add: string option -> attribute
    11   val del: attribute
    12   val setup: theory -> theory
    13 end;
    14 
    15 structure RecfunCodegen : RECFUN_CODEGEN =
    16 struct
    17 
    18 open Codegen;
    19 
    20 structure RecCodegenData = TheoryDataFun
    21 (struct
    22   val name = "HOL/recfun_codegen";
    23   type T = (thm * string option) list Symtab.table;
    24   val empty = Symtab.empty;
    25   val copy = I;
    26   val extend = I;
    27   fun merge _ = Symtab.merge_list (Drule.eq_thm_prop o pairself fst);
    28   fun print _ _ = ();
    29 end);
    30 
    31 
    32 val dest_eqn = HOLogic.dest_eq o HOLogic.dest_Trueprop;
    33 val lhs_of = fst o dest_eqn o prop_of;
    34 val const_of = dest_Const o head_of o fst o dest_eqn;
    35 
    36 fun warn thm = warning ("RecfunCodegen: Not a proper equation:\n" ^
    37   string_of_thm thm);
    38 
    39 fun add optmod =
    40   let
    41     fun add thm =
    42       if Pattern.pattern (lhs_of thm) then
    43         RecCodegenData.map
    44           (Symtab.update_list ((fst o const_of o prop_of) thm, (thm, optmod)))
    45       else tap (fn _ => warn thm)
    46       handle TERM _ => tap (fn _ => warn thm);
    47   in
    48     Thm.declaration_attribute (fn thm => Context.mapping
    49       (add thm #> CodegenData.add_func_legacy thm) I)
    50   end;
    51 
    52 fun del_thm thm thy =
    53   let
    54     val tab = RecCodegenData.get thy;
    55     val (s, _) = const_of (prop_of thm);
    56   in case Symtab.lookup tab s of
    57       NONE => thy
    58     | SOME thms =>
    59         RecCodegenData.put (Symtab.update (s, remove (eq_thm o apsnd fst) thm thms) tab) thy
    60   end handle TERM _ => (warn thm; thy);
    61 
    62 val del = Thm.declaration_attribute
    63   (fn thm => Context.mapping (del_thm thm #> CodegenData.del_func thm) I)
    64 
    65 fun del_redundant thy eqs [] = eqs
    66   | del_redundant thy eqs (eq :: eqs') =
    67     let
    68       val matches = curry
    69         (Pattern.matches thy o pairself (lhs_of o fst))
    70     in del_redundant thy (eq :: eqs) (filter_out (matches eq) eqs') end;
    71 
    72 fun get_equations thy defs (s, T) =
    73   (case Symtab.lookup (RecCodegenData.get thy) s of
    74      NONE => ([], "")
    75    | SOME thms => 
    76        let val thms' = del_redundant thy []
    77          (List.filter (fn (thm, _) => is_instance thy T
    78            (snd (const_of (prop_of thm)))) thms)
    79        in if null thms' then ([], "")
    80          else (preprocess thy (map fst thms'),
    81            case snd (snd (split_last thms')) of
    82                NONE => (case get_defn thy defs s T of
    83                    NONE => thyname_of_const s thy
    84                  | SOME ((_, (thyname, _)), _) => thyname)
    85              | SOME thyname => thyname)
    86        end);
    87 
    88 fun mk_suffix thy defs (s, T) = (case get_defn thy defs s T of
    89   SOME (_, SOME i) => " def" ^ string_of_int i | _ => "");
    90 
    91 exception EQN of string * typ * string;
    92 
    93 fun cycle g (xs, x) =
    94   if x mem xs then xs
    95   else Library.foldl (cycle g) (x :: xs, List.concat (Graph.all_paths (fst g) (x, x)));
    96 
    97 fun add_rec_funs thy defs gr dep eqs module =
    98   let
    99     fun dest_eq t = (fst (const_of t) ^ mk_suffix thy defs (const_of t),
   100       dest_eqn (rename_term t));
   101     val eqs' = map dest_eq eqs;
   102     val (dname, _) :: _ = eqs';
   103     val (s, T) = const_of (hd eqs);
   104 
   105     fun mk_fundef module fname prfx gr [] = (gr, [])
   106       | mk_fundef module fname prfx gr ((fname' : string, (lhs, rhs)) :: xs) =
   107       let
   108         val (gr1, pl) = invoke_codegen thy defs dname module false (gr, lhs);
   109         val (gr2, pr) = invoke_codegen thy defs dname module false (gr1, rhs);
   110         val (gr3, rest) = mk_fundef module fname' "and " gr2 xs
   111       in
   112         (gr3, Pretty.blk (4, [Pretty.str (if fname = fname' then "  | " else prfx),
   113            pl, Pretty.str " =", Pretty.brk 1, pr]) :: rest)
   114       end;
   115 
   116     fun put_code module fundef = map_node dname
   117       (K (SOME (EQN ("", dummyT, dname)), module, Pretty.string_of (Pretty.blk (0,
   118       separate Pretty.fbrk fundef @ [Pretty.str ";"])) ^ "\n\n"));
   119 
   120   in
   121     (case try (get_node gr) dname of
   122        NONE =>
   123          let
   124            val gr1 = add_edge (dname, dep)
   125              (new_node (dname, (SOME (EQN (s, T, "")), module, "")) gr);
   126            val (gr2, fundef) = mk_fundef module "" "fun " gr1 eqs';
   127            val xs = cycle gr2 ([], dname);
   128            val cs = map (fn x => case get_node gr2 x of
   129                (SOME (EQN (s, T, _)), _, _) => (s, T)
   130              | _ => error ("RecfunCodegen: illegal cyclic dependencies:\n" ^
   131                 implode (separate ", " xs))) xs
   132          in (case xs of
   133              [_] => (put_code module fundef gr2, module)
   134            | _ =>
   135              if not (dep mem xs) then
   136                let
   137                  val thmss as (_, thyname) :: _ = map (get_equations thy defs) cs;
   138                  val module' = if_library thyname module;
   139                  val eqs'' = map (dest_eq o prop_of) (List.concat (map fst thmss));
   140                  val (gr3, fundef') = mk_fundef module' "" "fun "
   141                    (add_edge (dname, dep)
   142                      (foldr (uncurry new_node) (del_nodes xs gr2)
   143                        (map (fn k =>
   144                          (k, (SOME (EQN ("", dummyT, dname)), module', ""))) xs))) eqs''
   145                in (put_code module' fundef' gr3, module') end
   146              else (gr2, module))
   147          end
   148      | SOME (SOME (EQN (_, _, s)), module', _) =>
   149          (if s = "" then
   150             if dname = dep then gr else add_edge (dname, dep) gr
   151           else if s = dep then gr else add_edge (s, dep) gr,
   152           module'))
   153   end;
   154 
   155 fun recfun_codegen thy defs gr dep module brack t = (case strip_comb t of
   156     (Const (p as (s, T)), ts) => (case (get_equations thy defs p, get_assoc_code thy s T) of
   157        (([], _), _) => NONE
   158      | (_, SOME _) => NONE
   159      | ((eqns, thyname), NONE) =>
   160         let
   161           val module' = if_library thyname module;
   162           val (gr', ps) = foldl_map
   163             (invoke_codegen thy defs dep module true) (gr, ts);
   164           val suffix = mk_suffix thy defs p;
   165           val (gr'', module'') =
   166             add_rec_funs thy defs gr' dep (map prop_of eqns) module';
   167           val (gr''', fname) = mk_const_id module'' (s ^ suffix) gr''
   168         in
   169           SOME (gr''', mk_app brack (Pretty.str (mk_qual_id module fname)) ps)
   170         end)
   171   | _ => NONE);
   172 
   173 
   174 val setup =
   175   RecCodegenData.init #>
   176   add_codegen "recfun" recfun_codegen #>
   177   add_attribute ""
   178     (Args.del |-- Scan.succeed del
   179      || Scan.option (Args.$$$ "target" |-- Args.colon |-- Args.name) >> add);
   180 
   181 end;