src/HOL/Tools/recfun_codegen.ML
author berghofe
Fri Jul 01 14:13:40 2005 +0200 (2005-07-01)
changeset 16645 a152d6b21c31
parent 16424 18a07ad8fea8
child 17144 6642e0f96f44
permissions -rw-r--r--
Adapted to modular code generation.
     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 tsig = Sign.tsig_of (sign_of thy);
    64       val matches = curry
    65         (Pattern.matches tsig o pairself (lhs_of o fst))
    66     in del_redundant thy (eq :: eqs) (filter_out (matches eq) eqs') end;
    67 
    68 fun get_equations thy defs (s, T) =
    69   (case Symtab.lookup (CodegenData.get thy, s) of
    70      NONE => ([], "")
    71    | SOME thms => 
    72        let val thms' = del_redundant thy []
    73          (List.filter (fn (thm, _) => is_instance thy T
    74            (snd (const_of (prop_of thm)))) thms)
    75        in if null thms' then ([], "")
    76          else (preprocess thy (map fst thms'),
    77            case snd (snd (split_last thms')) of
    78                NONE => (case get_defn thy defs s T of
    79                    NONE => thyname_of_const s thy
    80                  | SOME ((_, (thyname, _)), _) => thyname)
    81              | SOME thyname => thyname)
    82        end);
    83 
    84 fun mk_suffix thy defs (s, T) = (case get_defn thy defs s T of
    85   SOME (_, SOME i) => "_def" ^ string_of_int i | _ => "");
    86 
    87 exception EQN of string * typ * string;
    88 
    89 fun cycle g (xs, x) =
    90   if x mem xs then xs
    91   else Library.foldl (cycle g) (x :: xs, List.concat (Graph.find_paths g (x, x)));
    92 
    93 fun add_rec_funs thy defs gr dep eqs thyname =
    94   let
    95     fun dest_eq t = (fst (const_of t) ^ mk_suffix thy defs (const_of t),
    96       dest_eqn (rename_term t));
    97     val eqs' = map dest_eq eqs;
    98     val (dname, _) :: _ = eqs';
    99     val (s, T) = const_of (hd eqs);
   100 
   101     fun mk_fundef thyname fname prfx gr [] = (gr, [])
   102       | mk_fundef thyname fname prfx gr ((fname', (lhs, rhs)) :: xs) =
   103       let
   104         val (gr1, pl) = invoke_codegen thy defs dname thyname false (gr, lhs);
   105         val (gr2, pr) = invoke_codegen thy defs dname thyname false (gr1, rhs);
   106         val (gr3, rest) = mk_fundef thyname fname' "and " gr2 xs
   107       in
   108         (gr3, Pretty.blk (4, [Pretty.str (if fname = fname' then "  | " else prfx),
   109            pl, Pretty.str " =", Pretty.brk 1, pr]) :: rest)
   110       end;
   111 
   112     fun put_code thyname fundef = Graph.map_node dname
   113       (K (SOME (EQN ("", dummyT, dname)), thyname, Pretty.string_of (Pretty.blk (0,
   114       separate Pretty.fbrk fundef @ [Pretty.str ";"])) ^ "\n\n"));
   115 
   116   in
   117     (case try (Graph.get_node gr) dname of
   118        NONE =>
   119          let
   120            val gr1 = Graph.add_edge (dname, dep)
   121              (Graph.new_node (dname, (SOME (EQN (s, T, "")), "", "")) gr);
   122            val (gr2, fundef) = mk_fundef thyname "" "fun " gr1 eqs';
   123            val xs = cycle gr2 ([], dname);
   124            val cs = map (fn x => case Graph.get_node gr2 x of
   125                (SOME (EQN (s, T, _)), _, _) => (s, T)
   126              | _ => error ("RecfunCodegen: illegal cyclic dependencies:\n" ^
   127                 implode (separate ", " xs))) xs
   128          in (case xs of
   129              [_] => put_code thyname fundef gr2
   130            | _ =>
   131              if not (dep mem xs) then
   132                let
   133                  val thmss as (_, thyname) :: _ = map (get_equations thy defs) cs;
   134                  val eqs'' = map (dest_eq o prop_of) (List.concat (map fst thmss));
   135                  val (gr3, fundef') = mk_fundef thyname "" "fun "
   136                    (Graph.add_edge (dname, dep)
   137                      (foldr (uncurry Graph.new_node) (Graph.del_nodes xs gr2)
   138                        (map (fn k =>
   139                          (k, (SOME (EQN ("", dummyT, dname)), thyname, ""))) xs))) eqs''
   140                in put_code thyname fundef' gr3 end
   141              else gr2)
   142          end
   143      | SOME (SOME (EQN (_, _, s)), _, _) =>
   144          if s = "" then
   145            if dname = dep then gr else Graph.add_edge (dname, dep) gr
   146          else if s = dep then gr else Graph.add_edge (s, dep) gr)
   147   end;
   148 
   149 fun recfun_codegen thy defs gr dep thyname 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 (gr', ps) = foldl_map
   156             (invoke_codegen thy defs dep thyname true) (gr, ts);
   157           val suffix = mk_suffix thy defs p
   158         in
   159           SOME (add_rec_funs thy defs gr' dep (map prop_of eqns) thyname',
   160             mk_app brack (Pretty.str
   161               (mk_const_id (sign_of thy) thyname thyname' s ^ suffix)) ps)
   162         end)
   163   | _ => NONE);
   164 
   165 
   166 val setup =
   167   [CodegenData.init,
   168    add_codegen "recfun" recfun_codegen,
   169    add_attribute ""
   170      (   Args.del |-- Scan.succeed del
   171       || Scan.option (Args.$$$ "target" |-- Args.colon |-- Args.name) >> add)];
   172 
   173 end;