src/HOL/Tools/recfun_codegen.ML
author haftmann
Wed Jul 08 08:18:07 2009 +0200 (2009-07-08)
changeset 31962 baa8dce5bc45
parent 31958 2133f596c520
child 31998 2c7a24f74db9
permissions -rw-r--r--
tuned structure Code internally
     1 (*  Title:      HOL/Tools/recfun_codegen.ML
     2     Author:     Stefan Berghofer, TU Muenchen
     3 
     4 Code generator for recursive functions.
     5 *)
     6 
     7 signature RECFUN_CODEGEN =
     8 sig
     9   val setup: theory -> theory
    10 end;
    11 
    12 structure RecfunCodegen : RECFUN_CODEGEN =
    13 struct
    14 
    15 open Codegen;
    16 
    17 structure ModuleData = TheoryDataFun
    18 (
    19   type T = string Symtab.table;
    20   val empty = Symtab.empty;
    21   val copy = I;
    22   val extend = I;
    23   fun merge _ = Symtab.merge (K true);
    24 );
    25 
    26 fun add_thm NONE thm thy = Code.add_eqn thm thy
    27   | add_thm (SOME module_name) thm thy =
    28       let
    29         val (thm', _) = Code.mk_eqn thy (thm, true)
    30       in
    31         thy
    32         |> ModuleData.map (Symtab.update (fst (Code.const_typ_eqn thy thm'), module_name))
    33         |> Code.add_eqn thm'
    34       end;
    35 
    36 fun expand_eta thy [] = []
    37   | expand_eta thy (thms as thm :: _) =
    38       let
    39         val (_, ty) = Code.const_typ_eqn thy thm;
    40       in if null (Term.add_tvarsT ty []) orelse (null o fst o strip_type) ty
    41         then thms
    42         else map (Code.expand_eta thy 1) thms
    43       end;
    44 
    45 fun retrieve_equations thy (c, T) = if c = @{const_name "op ="} then NONE else
    46   let
    47     val c' = AxClass.unoverload_const thy (c, T);
    48     val opt_name = Symtab.lookup (ModuleData.get thy) c';
    49     val thms = Code.these_eqns thy c'
    50       |> map_filter (fn (thm, linear) => if linear then SOME thm else NONE)
    51       |> expand_eta thy
    52       |> Code.norm_varnames thy
    53       |> map (rpair opt_name)
    54   in if null thms then NONE else SOME thms end;
    55 
    56 val dest_eqn = Logic.dest_equals;
    57 val const_of = dest_Const o head_of o fst o dest_eqn;
    58 
    59 fun get_equations thy defs (s, T) =
    60   (case retrieve_equations thy (s, T) of
    61      NONE => ([], "")
    62    | SOME thms => 
    63        let val thms' = filter (fn (thm, _) => is_instance T
    64            (snd (const_of (prop_of thm)))) thms
    65        in if null thms' then ([], "")
    66          else (preprocess thy (map fst thms'),
    67            case snd (snd (split_last thms')) of
    68                NONE => (case get_defn thy defs s T of
    69                    NONE => Codegen.thyname_of_const thy s
    70                  | SOME ((_, (thyname, _)), _) => thyname)
    71              | SOME thyname => thyname)
    72        end);
    73 
    74 fun mk_suffix thy defs (s, T) = (case get_defn thy defs s T of
    75   SOME (_, SOME i) => " def" ^ string_of_int i | _ => "");
    76 
    77 exception EQN of string * typ * string;
    78 
    79 fun cycle g (xs, x : string) =
    80   if member (op =) xs x then xs
    81   else Library.foldl (cycle g) (x :: xs, flat (Graph.all_paths (fst g) (x, x)));
    82 
    83 fun add_rec_funs thy defs dep module eqs gr =
    84   let
    85     fun dest_eq t = (fst (const_of t) ^ mk_suffix thy defs (const_of t),
    86       dest_eqn (rename_term t));
    87     val eqs' = map dest_eq eqs;
    88     val (dname, _) :: _ = eqs';
    89     val (s, T) = const_of (hd eqs);
    90 
    91     fun mk_fundef module fname first [] gr = ([], gr)
    92       | mk_fundef module fname first ((fname' : string, (lhs, rhs)) :: xs) gr =
    93       let
    94         val (pl, gr1) = invoke_codegen thy defs dname module false lhs gr;
    95         val (pr, gr2) = invoke_codegen thy defs dname module false rhs gr1;
    96         val (rest, gr3) = mk_fundef module fname' false xs gr2 ;
    97         val (ty, gr4) = invoke_tycodegen thy defs dname module false T gr3;
    98         val num_args = (length o snd o strip_comb) lhs;
    99         val prfx = if fname = fname' then "  |"
   100           else if not first then "and"
   101           else if num_args = 0 then "val"
   102           else "fun";
   103         val pl' = Pretty.breaks (str prfx
   104           :: (if num_args = 0 then [pl, str ":", ty] else [pl]));
   105       in
   106         (Pretty.blk (4, pl'
   107            @ [str " =", Pretty.brk 1, pr]) :: rest, gr4)
   108       end;
   109 
   110     fun put_code module fundef = map_node dname
   111       (K (SOME (EQN ("", dummyT, dname)), module, string_of (Pretty.blk (0,
   112       separate Pretty.fbrk fundef @ [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 (fundef, gr2) = mk_fundef module "" true eqs' gr1 ;
   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              [_] => (module, put_code module fundef gr2)
   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 (fundef', gr3) = mk_fundef module' "" true eqs''
   135                    (add_edge (dname, dep)
   136                      (List.foldr (uncurry new_node) (del_nodes xs gr2)
   137                        (map (fn k =>
   138                          (k, (SOME (EQN ("", dummyT, dname)), module', ""))) xs)))
   139                in (module', put_code module' fundef' gr3) end
   140              else (module, gr2))
   141          end
   142      | SOME (SOME (EQN (_, _, s)), module', _) =>
   143          (module', 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   end;
   147 
   148 fun recfun_codegen thy defs dep module brack t gr = (case strip_comb t of
   149     (Const (p as (s, T)), ts) => (case (get_equations thy defs p, get_assoc_code thy (s, T)) of
   150        (([], _), _) => NONE
   151      | (_, SOME _) => NONE
   152      | ((eqns, thyname), NONE) =>
   153         let
   154           val module' = if_library thyname module;
   155           val (ps, gr') = fold_map
   156             (invoke_codegen thy defs dep module true) ts gr;
   157           val suffix = mk_suffix thy defs p;
   158           val (module'', gr'') =
   159             add_rec_funs thy defs dep module' (map prop_of eqns) gr';
   160           val (fname, gr''') = mk_const_id module'' (s ^ suffix) gr''
   161         in
   162           SOME (mk_app brack (str (mk_qual_id module fname)) ps, gr''')
   163         end)
   164   | _ => NONE);
   165 
   166 val setup = let
   167   fun add opt_module = Thm.declaration_attribute (fn thm => Context.mapping
   168     (add_thm opt_module thm) I);
   169   val del = Thm.declaration_attribute (fn thm => Context.mapping
   170     (Code.del_eqn thm) I);
   171 in
   172   add_codegen "recfun" recfun_codegen
   173   #> Code.add_attribute ("", Args.del |-- Scan.succeed del
   174      || Scan.option (Args.$$$ "target" |-- Args.colon |-- Args.name) >> add)
   175 end;
   176 
   177 end;