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