src/HOL/Tools/recfun_codegen.ML
author Philipp Meyer
Wed Sep 30 11:33:59 2009 +0200 (2009-09-30)
changeset 32866 1238cbb7c08f
parent 32358 98c00ee9e786
child 32927 7a20fd22ba01
permissions -rw-r--r--
atp_minimal using chain_ths again
     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 val const_of = dest_Const o head_of o fst o Logic.dest_equals;
    18 
    19 structure ModuleData = TheoryDataFun
    20 (
    21   type T = string Symtab.table;
    22   val empty = Symtab.empty;
    23   val copy = I;
    24   val extend = I;
    25   fun merge _ = Symtab.merge (K true);
    26 );
    27 
    28 fun add_thm_target module_name thm thy =
    29   let
    30     val (thm', _) = Code.mk_eqn thy (thm, true)
    31   in
    32     thy
    33     |> ModuleData.map (Symtab.update (fst (Code.const_typ_eqn thy thm'), module_name))
    34   end;
    35 
    36 fun avoid_value thy [thm] =
    37       let val (_, T) = Code.const_typ_eqn thy thm
    38       in if null (Term.add_tvarsT T []) orelse (null o fst o strip_type) T
    39         then [thm]
    40         else [Code_Thingol.expand_eta thy 1 thm]
    41       end
    42   | avoid_value thy thms = thms;
    43 
    44 fun get_equations thy defs (raw_c, T) = if raw_c = @{const_name "op ="} then ([], "") else
    45   let
    46     val c = AxClass.unoverload_const thy (raw_c, T);
    47     val raw_thms = Code.these_eqns thy c
    48       |> map_filter (fn (thm, linear) => if linear then SOME thm else NONE)
    49       |> filter (is_instance T o snd o const_of o prop_of);
    50     val module_name = case Symtab.lookup (ModuleData.get thy) c
    51      of SOME module_name => module_name
    52       | NONE => case get_defn thy defs c T
    53          of SOME ((_, (thyname, _)), _) => thyname
    54           | NONE => Codegen.thyname_of_const thy c;
    55   in if null raw_thms then ([], "") else
    56     raw_thms
    57     |> preprocess thy
    58     |> avoid_value thy
    59     |> Code_Thingol.clean_thms thy
    60     |> rpair module_name
    61   end;
    62 
    63 fun mk_suffix thy defs (s, T) = (case get_defn thy defs s T of
    64   SOME (_, SOME i) => " def" ^ string_of_int i | _ => "");
    65 
    66 exception EQN of string * typ * string;
    67 
    68 fun cycle g (xs, x : string) =
    69   if member (op =) xs x then xs
    70   else Library.foldl (cycle g) (x :: xs, flat (Graph.all_paths (fst g) (x, x)));
    71 
    72 fun add_rec_funs thy defs dep module eqs gr =
    73   let
    74     fun dest_eq t = (fst (const_of t) ^ mk_suffix thy defs (const_of t),
    75       Logic.dest_equals (rename_term t));
    76     val eqs' = map dest_eq eqs;
    77     val (dname, _) :: _ = eqs';
    78     val (s, T) = const_of (hd eqs);
    79 
    80     fun mk_fundef module fname first [] gr = ([], gr)
    81       | mk_fundef module fname first ((fname' : string, (lhs, rhs)) :: xs) gr =
    82       let
    83         val (pl, gr1) = invoke_codegen thy defs dname module false lhs gr;
    84         val (pr, gr2) = invoke_codegen thy defs dname module false rhs gr1;
    85         val (rest, gr3) = mk_fundef module fname' false xs gr2 ;
    86         val (ty, gr4) = invoke_tycodegen thy defs dname module false T gr3;
    87         val num_args = (length o snd o strip_comb) lhs;
    88         val prfx = if fname = fname' then "  |"
    89           else if not first then "and"
    90           else if num_args = 0 then "val"
    91           else "fun";
    92         val pl' = Pretty.breaks (str prfx
    93           :: (if num_args = 0 then [pl, str ":", ty] else [pl]));
    94       in
    95         (Pretty.blk (4, pl'
    96            @ [str " =", Pretty.brk 1, pr]) :: rest, gr4)
    97       end;
    98 
    99     fun put_code module fundef = map_node dname
   100       (K (SOME (EQN ("", dummyT, dname)), module, string_of (Pretty.blk (0,
   101       separate Pretty.fbrk fundef @ [str ";"])) ^ "\n\n"));
   102 
   103   in
   104     (case try (get_node gr) dname of
   105        NONE =>
   106          let
   107            val gr1 = add_edge (dname, dep)
   108              (new_node (dname, (SOME (EQN (s, T, "")), module, "")) gr);
   109            val (fundef, gr2) = mk_fundef module "" true eqs' gr1 ;
   110            val xs = cycle gr2 ([], dname);
   111            val cs = map (fn x => case get_node gr2 x of
   112                (SOME (EQN (s, T, _)), _, _) => (s, T)
   113              | _ => error ("RecfunCodegen: illegal cyclic dependencies:\n" ^
   114                 implode (separate ", " xs))) xs
   115          in (case xs of
   116              [_] => (module, put_code module fundef gr2)
   117            | _ =>
   118              if not (dep mem xs) then
   119                let
   120                  val thmss as (_, thyname) :: _ = map (get_equations thy defs) cs;
   121                  val module' = if_library thyname module;
   122                  val eqs'' = map (dest_eq o prop_of) (List.concat (map fst thmss));
   123                  val (fundef', gr3) = mk_fundef module' "" true eqs''
   124                    (add_edge (dname, dep)
   125                      (List.foldr (uncurry new_node) (del_nodes xs gr2)
   126                        (map (fn k =>
   127                          (k, (SOME (EQN ("", dummyT, dname)), module', ""))) xs)))
   128                in (module', put_code module' fundef' gr3) end
   129              else (module, gr2))
   130          end
   131      | SOME (SOME (EQN (_, _, s)), module', _) =>
   132          (module', if s = "" then
   133             if dname = dep then gr else add_edge (dname, dep) gr
   134           else if s = dep then gr else add_edge (s, dep) gr))
   135   end;
   136 
   137 fun recfun_codegen thy defs dep module brack t gr = (case strip_comb t of
   138     (Const (p as (s, T)), ts) => (case (get_equations thy defs p, get_assoc_code thy (s, T)) of
   139        (([], _), _) => NONE
   140      | (_, SOME _) => NONE
   141      | ((eqns, thyname), NONE) =>
   142         let
   143           val module' = if_library thyname module;
   144           val (ps, gr') = fold_map
   145             (invoke_codegen thy defs dep module true) ts gr;
   146           val suffix = mk_suffix thy defs p;
   147           val (module'', gr'') =
   148             add_rec_funs thy defs dep module' (map prop_of eqns) gr';
   149           val (fname, gr''') = mk_const_id module'' (s ^ suffix) gr''
   150         in
   151           SOME (mk_app brack (str (mk_qual_id module fname)) ps, gr''')
   152         end)
   153   | _ => NONE);
   154 
   155 val setup = 
   156   add_codegen "recfun" recfun_codegen
   157   #> Code.set_code_target_attr add_thm_target;
   158 
   159 end;