|
1 (* Author: Lukas Bulwahn, TU Muenchen |
|
2 |
|
3 *) |
|
4 signature PREDICATE_COMPILE = |
|
5 sig |
|
6 val setup : theory -> theory |
|
7 end; |
|
8 |
|
9 structure Predicate_Compile : PREDICATE_COMPILE = |
|
10 struct |
|
11 |
|
12 open Predicate_Compile_Aux; |
|
13 |
|
14 val priority = tracing; |
|
15 |
|
16 (* Some last processing *) |
|
17 fun remove_pointless_clauses intro = |
|
18 if Logic.strip_imp_prems (prop_of intro) = [@{prop "False"}] then |
|
19 [] |
|
20 else [intro] |
|
21 |
|
22 fun preprocess_strong_conn_constnames gr constnames thy = |
|
23 let |
|
24 val get_specs = map (fn k => (k, Graph.get_node gr k)) |
|
25 val _ = priority ("Preprocessing scc of " ^ commas constnames) |
|
26 val (prednames, funnames) = List.partition (is_pred thy) constnames |
|
27 (* untangle recursion by defining predicates for all functions *) |
|
28 val _ = priority "Compiling functions to predicates..." |
|
29 val _ = Output.tracing ("funnames: " ^ commas funnames) |
|
30 val thy' = |
|
31 thy |> not (null funnames) ? Predicate_Compile_Fun.define_predicates |
|
32 (get_specs funnames) |
|
33 val _ = priority "Compiling predicates to flat introrules..." |
|
34 val (intross, thy'') = apfst flat (fold_map Predicate_Compile_Pred.preprocess |
|
35 (get_specs prednames) thy') |
|
36 val _ = tracing ("intross: " ^ commas (map (Display.string_of_thm_global thy'') (flat intross))) |
|
37 val _ = priority "Replacing functions in introrules..." |
|
38 val intross' = burrow (maps (Predicate_Compile_Fun.rewrite_intro thy'')) intross |
|
39 val intross'' = burrow (maps remove_pointless_clauses) intross |
|
40 val thy''' = fold Predicate_Compile_Core.register_intros intross'' thy'' |
|
41 in |
|
42 thy''' |
|
43 end; |
|
44 |
|
45 fun code_pred_cmd ((inductify_all, rpred), raw_const) lthy = |
|
46 if inductify_all then |
|
47 let |
|
48 val thy = ProofContext.theory_of lthy |
|
49 val const = Code.read_const thy raw_const |
|
50 val _ = Output.tracing ("fetching definition from theory") |
|
51 val table = Pred_Compile_Data.make_const_spec_table thy |
|
52 val gr = Pred_Compile_Data.obtain_specification_graph table const |
|
53 val _ = Output.tracing (commas (Graph.all_succs gr [const])) |
|
54 val gr = Graph.subgraph (member (op =) (Graph.all_succs gr [const])) gr |
|
55 val lthy' = LocalTheory.theory (fold_rev (preprocess_strong_conn_constnames gr) |
|
56 (Graph.strong_conn gr)) lthy |
|
57 |> LocalTheory.checkpoint |
|
58 in Predicate_Compile_Core.code_pred_cmd rpred raw_const lthy' end |
|
59 else |
|
60 Predicate_Compile_Core.code_pred_cmd rpred raw_const lthy |
|
61 |
|
62 val setup = Predicate_Compile_Fun.setup_oracle #> Predicate_Compile_Core.setup |
|
63 |
|
64 val _ = List.app OuterKeyword.keyword ["inductify_all", "rpred"] |
|
65 |
|
66 local structure P = OuterParse |
|
67 in |
|
68 |
|
69 val _ = OuterSyntax.local_theory_to_proof "code_pred" |
|
70 "prove equations for predicate specified by intro/elim rules" |
|
71 OuterKeyword.thy_goal (P.opt_keyword "inductify_all" -- P.opt_keyword "rpred" -- P.term_group >> code_pred_cmd) |
|
72 |
|
73 end |
|
74 |
|
75 end |