src/HOL/Tools/recfun_codegen.ML
author wenzelm
Thu Sep 15 17:16:56 2005 +0200 (2005-09-15)
changeset 17412 e26cb20ef0cc
parent 17261 193b84a70ca4
child 18220 43cf5767f992
permissions -rw-r--r--
TableFun/Symtab: curried lookup and update;
     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 -> theory attribute
    11   val del: theory attribute
    12   val setup: (theory -> theory) list
    13 end;
    14 
    15 structure RecfunCodegen : RECFUN_CODEGEN =
    16 struct
    17 
    18 open Codegen;
    19 
    20 structure CodegenData = 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_multi' (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 (p as (thy, thm)) =
    40   let
    41     val tab = CodegenData.get thy;
    42     val (s, _) = const_of (prop_of thm);
    43   in
    44     if Pattern.pattern (lhs_of thm) then
    45       (CodegenData.put (Symtab.update_multi (s, (thm, optmod)) tab) thy, thm)
    46     else (warn thm; p)
    47   end handle TERM _ => (warn thm; p);
    48 
    49 fun del (p as (thy, thm)) =
    50   let
    51     val tab = CodegenData.get thy;
    52     val (s, _) = const_of (prop_of thm);
    53   in case Symtab.lookup tab s of
    54       NONE => p
    55     | SOME thms => (CodegenData.put (Symtab.update (s,
    56         gen_rem (eq_thm o apfst fst) (thms, thm)) tab) thy, thm)
    57   end handle TERM _ => (warn thm; p);
    58 
    59 fun del_redundant thy eqs [] = eqs
    60   | del_redundant thy eqs (eq :: eqs') =
    61     let
    62       val matches = curry
    63         (Pattern.matches thy o pairself (lhs_of o fst))
    64     in del_redundant thy (eq :: eqs) (filter_out (matches eq) eqs') end;
    65 
    66 fun get_equations thy defs (s, T) =
    67   (case Symtab.lookup (CodegenData.get thy) s of
    68      NONE => ([], "")
    69    | SOME thms => 
    70        let val thms' = del_redundant thy []
    71          (List.filter (fn (thm, _) => is_instance thy T
    72            (snd (const_of (prop_of thm)))) thms)
    73        in if null thms' then ([], "")
    74          else (preprocess thy (map fst thms'),
    75            case snd (snd (split_last thms')) of
    76                NONE => (case get_defn thy defs s T of
    77                    NONE => thyname_of_const s thy
    78                  | SOME ((_, (thyname, _)), _) => thyname)
    79              | SOME thyname => thyname)
    80        end);
    81 
    82 fun mk_suffix thy defs (s, T) = (case get_defn thy defs s T of
    83   SOME (_, SOME i) => " def" ^ string_of_int i | _ => "");
    84 
    85 exception EQN of string * typ * string;
    86 
    87 fun cycle g (xs, x) =
    88   if x mem xs then xs
    89   else Library.foldl (cycle g) (x :: xs, List.concat (Graph.find_paths (fst g) (x, x)));
    90 
    91 fun add_rec_funs thy defs gr dep eqs module =
    92   let
    93     fun dest_eq t = (fst (const_of t) ^ mk_suffix thy defs (const_of t),
    94       dest_eqn (rename_term t));
    95     val eqs' = map dest_eq eqs;
    96     val (dname, _) :: _ = eqs';
    97     val (s, T) = const_of (hd eqs);
    98 
    99     fun mk_fundef module fname prfx gr [] = (gr, [])
   100       | mk_fundef module fname prfx gr ((fname', (lhs, rhs)) :: xs) =
   101       let
   102         val (gr1, pl) = invoke_codegen thy defs dname module false (gr, lhs);
   103         val (gr2, pr) = invoke_codegen thy defs dname module false (gr1, rhs);
   104         val (gr3, rest) = mk_fundef module fname' "and " gr2 xs
   105       in
   106         (gr3, Pretty.blk (4, [Pretty.str (if fname = fname' then "  | " else prfx),
   107            pl, Pretty.str " =", Pretty.brk 1, pr]) :: rest)
   108       end;
   109 
   110     fun put_code module fundef = map_node dname
   111       (K (SOME (EQN ("", dummyT, dname)), module, Pretty.string_of (Pretty.blk (0,
   112       separate Pretty.fbrk fundef @ [Pretty.str ";"])) ^ "\n\n"));
   113 
   114   in
   115     (case try (get_node gr) dname of
   116        NONE =>
   117          let
   118            val gr1 = add_edge (dname, dep)
   119              (new_node (dname, (SOME (EQN (s, T, "")), module, "")) gr);
   120            val (gr2, fundef) = mk_fundef module "" "fun " gr1 eqs';
   121            val xs = cycle gr2 ([], dname);
   122            val cs = map (fn x => case get_node gr2 x of
   123                (SOME (EQN (s, T, _)), _, _) => (s, T)
   124              | _ => error ("RecfunCodegen: illegal cyclic dependencies:\n" ^
   125                 implode (separate ", " xs))) xs
   126          in (case xs of
   127              [_] => (put_code module fundef gr2, module)
   128            | _ =>
   129              if not (dep mem xs) then
   130                let
   131                  val thmss as (_, thyname) :: _ = map (get_equations thy defs) cs;
   132                  val module' = if_library thyname module;
   133                  val eqs'' = map (dest_eq o prop_of) (List.concat (map fst thmss));
   134                  val (gr3, fundef') = mk_fundef module' "" "fun "
   135                    (add_edge (dname, dep)
   136                      (foldr (uncurry new_node) (del_nodes xs gr2)
   137                        (map (fn k =>
   138                          (k, (SOME (EQN ("", dummyT, dname)), module', ""))) xs))) eqs''
   139                in (put_code module' fundef' gr3, module') end
   140              else (gr2, module))
   141          end
   142      | SOME (SOME (EQN (_, _, s)), module', _) =>
   143          (if s = "" then
   144             if dname = dep then gr else add_edge (dname, dep) gr
   145           else if s = dep then gr else add_edge (s, dep) gr,
   146           module'))
   147   end;
   148 
   149 fun recfun_codegen thy defs gr dep module brack t = (case strip_comb t of
   150     (Const (p as (s, T)), ts) => (case (get_equations thy defs p, get_assoc_code thy s T) of
   151        (([], _), _) => NONE
   152      | (_, SOME _) => NONE
   153      | ((eqns, thyname), NONE) =>
   154         let
   155           val module' = if_library thyname module;
   156           val (gr', ps) = foldl_map
   157             (invoke_codegen thy defs dep module true) (gr, ts);
   158           val suffix = mk_suffix thy defs p;
   159           val (gr'', module'') =
   160             add_rec_funs thy defs gr' dep (map prop_of eqns) module';
   161           val (gr''', fname) = mk_const_id module'' (s ^ suffix) gr''
   162         in
   163           SOME (gr''', mk_app brack (Pretty.str (mk_qual_id module fname)) ps)
   164         end)
   165   | _ => NONE);
   166 
   167 
   168 val setup =
   169   [CodegenData.init,
   170    add_codegen "recfun" recfun_codegen,
   171    add_attribute ""
   172      (   Args.del |-- Scan.succeed del
   173       || Scan.option (Args.$$$ "target" |-- Args.colon |-- Args.name) >> add)];
   174 
   175 end;