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