src/HOL/Tools/recfun_codegen.ML
author haftmann
Wed May 05 18:25:34 2010 +0200 (2010-05-05)
changeset 36692 54b64d4ad524
parent 35225 dfbcff38c9ed
child 38864 4abe644fcea5
permissions -rw-r--r--
farewell to old-style mem infixes -- type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
     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.bare_thms_of_cert thy
    48       |> map (AxClass.overload thy)
    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     |> rpair module_name
    60   end;
    61 
    62 fun mk_suffix thy defs (s, T) = (case get_defn thy defs s T of
    63   SOME (_, SOME i) => " def" ^ string_of_int i | _ => "");
    64 
    65 exception EQN of string * typ * string;
    66 
    67 fun cycle g x xs =
    68   if member (op =) xs x then xs
    69   else fold (cycle g) (flat (Graph.all_paths (fst g) (x, x))) (x :: xs);
    70 
    71 fun add_rec_funs thy defs dep module eqs gr =
    72   let
    73     fun dest_eq t = (fst (const_of t) ^ mk_suffix thy defs (const_of t),
    74       Logic.dest_equals (rename_term t));
    75     val eqs' = map dest_eq eqs;
    76     val (dname, _) :: _ = eqs';
    77     val (s, T) = const_of (hd eqs);
    78 
    79     fun mk_fundef module fname first [] gr = ([], gr)
    80       | mk_fundef module fname first ((fname' : string, (lhs, rhs)) :: xs) gr =
    81       let
    82         val (pl, gr1) = invoke_codegen thy defs dname module false lhs gr;
    83         val (pr, gr2) = invoke_codegen thy defs dname module false rhs gr1;
    84         val (rest, gr3) = mk_fundef module fname' false xs gr2 ;
    85         val (ty, gr4) = invoke_tycodegen thy defs dname module false T gr3;
    86         val num_args = (length o snd o strip_comb) lhs;
    87         val prfx = if fname = fname' then "  |"
    88           else if not first then "and"
    89           else if num_args = 0 then "val"
    90           else "fun";
    91         val pl' = Pretty.breaks (str prfx
    92           :: (if num_args = 0 then [pl, str ":", ty] else [pl]));
    93       in
    94         (Pretty.blk (4, pl'
    95            @ [str " =", Pretty.brk 1, pr]) :: rest, gr4)
    96       end;
    97 
    98     fun put_code module fundef = map_node dname
    99       (K (SOME (EQN ("", dummyT, dname)), module, string_of (Pretty.blk (0,
   100       separate Pretty.fbrk fundef @ [str ";"])) ^ "\n\n"));
   101 
   102   in
   103     (case try (get_node gr) dname of
   104        NONE =>
   105          let
   106            val gr1 = add_edge (dname, dep)
   107              (new_node (dname, (SOME (EQN (s, T, "")), module, "")) gr);
   108            val (fundef, gr2) = mk_fundef module "" true eqs' gr1 ;
   109            val xs = cycle gr2 dname [];
   110            val cs = map (fn x => case get_node gr2 x of
   111                (SOME (EQN (s, T, _)), _, _) => (s, T)
   112              | _ => error ("RecfunCodegen: illegal cyclic dependencies:\n" ^
   113                 implode (separate ", " xs))) xs
   114          in (case xs of
   115              [_] => (module, put_code module fundef gr2)
   116            | _ =>
   117              if not (member (op =) xs dep) then
   118                let
   119                  val thmss as (_, thyname) :: _ = map (get_equations thy defs) cs;
   120                  val module' = if_library thyname module;
   121                  val eqs'' = map (dest_eq o prop_of) (maps fst thmss);
   122                  val (fundef', gr3) = mk_fundef module' "" true eqs''
   123                    (add_edge (dname, dep)
   124                      (List.foldr (uncurry new_node) (del_nodes xs gr2)
   125                        (map (fn k =>
   126                          (k, (SOME (EQN ("", dummyT, dname)), module', ""))) xs)))
   127                in (module', put_code module' fundef' gr3) end
   128              else (module, gr2))
   129          end
   130      | SOME (SOME (EQN (_, _, s)), module', _) =>
   131          (module', if s = "" then
   132             if dname = dep then gr else add_edge (dname, dep) gr
   133           else if s = dep then gr else add_edge (s, dep) gr))
   134   end;
   135 
   136 fun recfun_codegen thy defs dep module brack t gr = (case strip_comb t of
   137     (Const (p as (s, T)), ts) => (case (get_equations thy defs p, get_assoc_code thy (s, T)) of
   138        (([], _), _) => NONE
   139      | (_, SOME _) => NONE
   140      | ((eqns, thyname), NONE) =>
   141         let
   142           val module' = if_library thyname module;
   143           val (ps, gr') = fold_map
   144             (invoke_codegen thy defs dep module true) ts gr;
   145           val suffix = mk_suffix thy defs p;
   146           val (module'', gr'') =
   147             add_rec_funs thy defs dep module' (map prop_of eqns) gr';
   148           val (fname, gr''') = mk_const_id module'' (s ^ suffix) gr''
   149         in
   150           SOME (mk_app brack (str (mk_qual_id module fname)) ps, gr''')
   151         end)
   152   | _ => NONE);
   153 
   154 val setup = 
   155   add_codegen "recfun" recfun_codegen
   156   #> Code.set_code_target_attr add_thm_target;
   157 
   158 end;