berghofe@12447: (* Title: HOL/recfun_codegen.ML berghofe@12447: ID: $Id$ berghofe@12447: Author: Stefan Berghofer, TU Muenchen berghofe@12447: License: GPL (GNU GENERAL PUBLIC LICENSE) berghofe@12447: berghofe@12447: Code generator for recursive functions. berghofe@12447: *) berghofe@12447: berghofe@12447: signature RECFUN_CODEGEN = berghofe@12447: sig berghofe@12447: val add: theory attribute berghofe@12447: val setup: (theory -> theory) list berghofe@12447: end; berghofe@12447: berghofe@12447: structure RecfunCodegen : RECFUN_CODEGEN = berghofe@12447: struct berghofe@12447: berghofe@12447: open Codegen; berghofe@12447: berghofe@12556: structure CodegenArgs = berghofe@12447: struct berghofe@12447: val name = "HOL/recfun_codegen"; berghofe@12447: type T = thm list Symtab.table; berghofe@12447: val empty = Symtab.empty; berghofe@12447: val copy = I; berghofe@12447: val prep_ext = I; wenzelm@13105: val merge = Symtab.merge_multi Drule.eq_thm_prop; berghofe@12447: fun print _ _ = (); berghofe@12447: end; berghofe@12447: berghofe@12556: structure CodegenData = TheoryDataFun(CodegenArgs); berghofe@12447: berghofe@12447: val prop_of = #prop o rep_thm; berghofe@12447: val dest_eqn = HOLogic.dest_eq o HOLogic.dest_Trueprop; berghofe@12447: val const_of = dest_Const o head_of o fst o dest_eqn; berghofe@12447: berghofe@12447: fun warn thm = warning ("RecfunCodegen: Not a proper equation:\n" ^ berghofe@12447: string_of_thm thm); berghofe@12447: berghofe@12447: fun add (p as (thy, thm)) = berghofe@12447: let berghofe@12447: val tsig = Sign.tsig_of (sign_of thy); berghofe@12556: val tab = CodegenData.get thy; berghofe@12447: val (s, _) = const_of (prop_of thm); berghofe@12447: berghofe@12447: val matches = curry berghofe@12447: (Pattern.matches tsig o pairself (fst o dest_eqn o prop_of)); berghofe@12447: berghofe@12556: in (CodegenData.put (Symtab.update ((s, berghofe@12447: filter_out (matches thm) (if_none (Symtab.lookup (tab, s)) []) @ [thm]), berghofe@12447: tab)) thy, thm) berghofe@12447: end handle TERM _ => (warn thm; p) | Pattern.Pattern => (warn thm; p); berghofe@12447: berghofe@12447: fun get_equations thy (s, T) = berghofe@12556: (case Symtab.lookup (CodegenData.get thy, s) of berghofe@12447: None => [] berghofe@12447: | Some thms => filter (fn thm => is_instance thy T berghofe@12447: (snd (const_of (prop_of thm)))) thms); berghofe@12447: berghofe@12447: fun mk_poly_id thy (s, T) = mk_const_id (sign_of thy) s ^ berghofe@12447: (case get_defn thy s T of berghofe@12447: Some (_, Some i) => "_def" ^ string_of_int i berghofe@12447: | _ => ""); berghofe@12447: berghofe@12447: exception EQN of string * typ * string; berghofe@12447: berghofe@12447: fun cycle g (xs, x) = berghofe@12447: if x mem xs then xs berghofe@12447: else foldl (cycle g) (x :: xs, flat (Graph.find_paths g (x, x))); berghofe@12447: berghofe@12447: fun add_rec_funs thy gr dep eqs = berghofe@12447: let berghofe@12447: fun dest_eq t = berghofe@12447: (mk_poly_id thy (const_of t), dest_eqn (rename_term t)); berghofe@12447: val eqs' = map dest_eq eqs; berghofe@12447: val (dname, _) :: _ = eqs'; berghofe@12447: val (s, T) = const_of (hd eqs); berghofe@12447: berghofe@12447: fun mk_fundef fname prfx gr [] = (gr, []) berghofe@12447: | mk_fundef fname prfx gr ((fname', (lhs, rhs)) :: xs) = berghofe@12447: let berghofe@12447: val (gr1, pl) = invoke_codegen thy dname false (gr, lhs); berghofe@12447: val (gr2, pr) = invoke_codegen thy dname false (gr1, rhs); berghofe@12447: val (gr3, rest) = mk_fundef fname' "and " gr2 xs berghofe@12447: in berghofe@12447: (gr3, Pretty.blk (4, [Pretty.str (if fname = fname' then " | " else prfx), berghofe@12447: pl, Pretty.str " =", Pretty.brk 1, pr]) :: rest) berghofe@12447: end; berghofe@12447: berghofe@12447: fun put_code fundef = Graph.map_node dname berghofe@12447: (K (Some (EQN ("", dummyT, dname)), Pretty.string_of (Pretty.blk (0, berghofe@12447: separate Pretty.fbrk fundef @ [Pretty.str ";"])) ^ "\n\n")); berghofe@12447: berghofe@12447: in berghofe@12447: (case try (Graph.get_node gr) dname of berghofe@12447: None => berghofe@12447: let berghofe@12447: val gr1 = Graph.add_edge (dname, dep) berghofe@12447: (Graph.new_node (dname, (Some (EQN (s, T, "")), "")) gr); berghofe@12447: val (gr2, fundef) = mk_fundef "" "fun " gr1 eqs'; berghofe@12447: val xs = cycle gr2 ([], dname); berghofe@12447: val cs = map (fn x => case Graph.get_node gr2 x of berghofe@12447: (Some (EQN (s, T, _)), _) => (s, T) berghofe@12447: | _ => error ("RecfunCodegen: illegal cyclic dependencies:\n" ^ berghofe@12447: implode (separate ", " xs))) xs berghofe@12447: in (case xs of berghofe@12447: [_] => put_code fundef gr2 berghofe@12447: | _ => berghofe@12447: if not (dep mem xs) then berghofe@12447: let berghofe@12447: val eqs'' = map (dest_eq o prop_of) berghofe@12447: (flat (map (get_equations thy) cs)); berghofe@12447: val (gr3, fundef') = mk_fundef "" "fun " berghofe@12447: (Graph.add_edge (dname, dep) berghofe@12447: (foldr (uncurry Graph.new_node) (map (fn k => berghofe@12447: (k, (Some (EQN ("", dummyT, dname)), ""))) xs, berghofe@12447: Graph.del_nodes xs gr2))) eqs'' berghofe@12447: in put_code fundef' gr3 end berghofe@12447: else gr2) berghofe@12447: end berghofe@12447: | Some (Some (EQN (_, _, s)), _) => berghofe@12447: if s = "" then berghofe@12447: if dname = dep then gr else Graph.add_edge (dname, dep) gr berghofe@12447: else if s = dep then gr else Graph.add_edge (s, dep) gr) berghofe@12447: end; berghofe@12447: berghofe@12447: fun recfun_codegen thy gr dep brack t = (case strip_comb t of berghofe@12447: (Const p, ts) => (case get_equations thy p of berghofe@12447: [] => None berghofe@12447: | eqns => berghofe@12447: let val (gr', ps) = foldl_map (invoke_codegen thy dep true) (gr, ts) berghofe@12447: in berghofe@12447: Some (add_rec_funs thy gr' dep (map prop_of eqns), berghofe@12447: mk_app brack (Pretty.str (mk_poly_id thy p)) ps) berghofe@12447: end) berghofe@12447: | _ => None); berghofe@12447: berghofe@12447: berghofe@12447: val setup = berghofe@12556: [CodegenData.init, berghofe@12447: add_codegen "recfun" recfun_codegen, berghofe@12556: add_attribute "" add]; berghofe@12447: berghofe@12447: end;