54 _ $ (Const ("op :", _) $ _ $ t) => (case head_of t of |
54 _ $ (Const ("op :", _) $ _ $ t) => (case head_of t of |
55 Const (s, _) => |
55 Const (s, _) => |
56 let val cs = foldr add_term_consts [] (prems_of thm) |
56 let val cs = foldr add_term_consts [] (prems_of thm) |
57 in (CodegenData.put |
57 in (CodegenData.put |
58 {intros = intros |> |
58 {intros = intros |> |
59 Symtab.curried_update (s, Symtab.curried_lookup_multi intros s @ [(thm, thyname_of s)]), |
59 Symtab.update (s, Symtab.lookup_multi intros s @ [(thm, thyname_of s)]), |
60 graph = foldr (uncurry (Graph.add_edge o pair s)) |
60 graph = foldr (uncurry (Graph.add_edge o pair s)) |
61 (Library.foldl add_node (graph, s :: cs)) cs, |
61 (Library.foldl add_node (graph, s :: cs)) cs, |
62 eqns = eqns} thy, thm) |
62 eqns = eqns} thy, thm) |
63 end |
63 end |
64 | _ => (warn thm; p)) |
64 | _ => (warn thm; p)) |
65 | _ $ (Const ("op =", _) $ t $ _) => (case head_of t of |
65 | _ $ (Const ("op =", _) $ t $ _) => (case head_of t of |
66 Const (s, _) => |
66 Const (s, _) => |
67 (CodegenData.put {intros = intros, graph = graph, |
67 (CodegenData.put {intros = intros, graph = graph, |
68 eqns = eqns |> Symtab.curried_update |
68 eqns = eqns |> Symtab.update |
69 (s, Symtab.curried_lookup_multi eqns s @ [(thm, thyname_of s)])} thy, thm) |
69 (s, Symtab.lookup_multi eqns s @ [(thm, thyname_of s)])} thy, thm) |
70 | _ => (warn thm; p)) |
70 | _ => (warn thm; p)) |
71 | _ => (warn thm; p)) |
71 | _ => (warn thm; p)) |
72 end; |
72 end; |
73 |
73 |
74 fun get_clauses thy s = |
74 fun get_clauses thy s = |
75 let val {intros, graph, ...} = CodegenData.get thy |
75 let val {intros, graph, ...} = CodegenData.get thy |
76 in case Symtab.curried_lookup intros s of |
76 in case Symtab.lookup intros s of |
77 NONE => (case InductivePackage.get_inductive thy s of |
77 NONE => (case InductivePackage.get_inductive thy s of |
78 NONE => NONE |
78 NONE => NONE |
79 | SOME ({names, ...}, {intrs, ...}) => |
79 | SOME ({names, ...}, {intrs, ...}) => |
80 SOME (names, thyname_of_const s thy, |
80 SOME (names, thyname_of_const s thy, |
81 preprocess thy intrs)) |
81 preprocess thy intrs)) |
82 | SOME _ => |
82 | SOME _ => |
83 let |
83 let |
84 val SOME names = find_first |
84 val SOME names = find_first |
85 (fn xs => s mem xs) (Graph.strong_conn graph); |
85 (fn xs => s mem xs) (Graph.strong_conn graph); |
86 val intrs = List.concat (map |
86 val intrs = List.concat (map |
87 (fn s => the (Symtab.curried_lookup intros s)) names); |
87 (fn s => the (Symtab.lookup intros s)) names); |
88 val (_, (_, thyname)) = split_last intrs |
88 val (_, (_, thyname)) = split_last intrs |
89 in SOME (names, thyname, preprocess thy (map fst intrs)) end |
89 in SOME (names, thyname, preprocess thy (map fst intrs)) end |
90 end; |
90 end; |
91 |
91 |
92 |
92 |
714 NONE => NONE |
714 NONE => NONE |
715 | SOME (gr', call_p) => SOME (gr', (if brack then parens else I) |
715 | SOME (gr', call_p) => SOME (gr', (if brack then parens else I) |
716 (Pretty.block [Pretty.str "?! (", call_p, Pretty.str ")"]))) |
716 (Pretty.block [Pretty.str "?! (", call_p, Pretty.str ")"]))) |
717 handle TERM _ => mk_ind_call thy defs gr dep module t u true) |
717 handle TERM _ => mk_ind_call thy defs gr dep module t u true) |
718 | inductive_codegen thy defs gr dep module brack t = (case strip_comb t of |
718 | inductive_codegen thy defs gr dep module brack t = (case strip_comb t of |
719 (Const (s, _), ts) => (case Symtab.curried_lookup (#eqns (CodegenData.get thy)) s of |
719 (Const (s, _), ts) => (case Symtab.lookup (#eqns (CodegenData.get thy)) s of |
720 NONE => list_of_indset thy defs gr dep module brack t |
720 NONE => list_of_indset thy defs gr dep module brack t |
721 | SOME eqns => |
721 | SOME eqns => |
722 let |
722 let |
723 val (_, (_, thyname)) = split_last eqns; |
723 val (_, (_, thyname)) = split_last eqns; |
724 val (gr', id) = mk_fun thy defs s (preprocess thy (map fst eqns)) |
724 val (gr', id) = mk_fun thy defs s (preprocess thy (map fst eqns)) |