author | bulwahn |
Sat, 24 Oct 2009 16:55:42 +0200 | |
changeset 33111 | db5af7b86a2f |
parent 33108 | 9d9afd478016 |
child 33113 | 0f6e30b87cf1 |
permissions | -rw-r--r-- |
32668
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
1 |
(* Author: Lukas Bulwahn, TU Muenchen |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
2 |
|
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
3 |
*) |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
4 |
signature PREDICATE_COMPILE = |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
5 |
sig |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
6 |
val setup : theory -> theory |
32672
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32669
diff
changeset
|
7 |
val preprocess : string -> theory -> theory |
32668
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
8 |
end; |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
9 |
|
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
10 |
structure Predicate_Compile : PREDICATE_COMPILE = |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
11 |
struct |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
12 |
|
33108
9d9afd478016
added test for higher-order function inductification; added debug messages
bulwahn
parents:
33107
diff
changeset
|
13 |
(* options *) |
33111 | 14 |
val fail_safe_mode = true |
33108
9d9afd478016
added test for higher-order function inductification; added debug messages
bulwahn
parents:
33107
diff
changeset
|
15 |
|
32668
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
16 |
open Predicate_Compile_Aux; |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
17 |
|
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
18 |
val priority = tracing; |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
19 |
|
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
20 |
(* Some last processing *) |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
21 |
fun remove_pointless_clauses intro = |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
22 |
if Logic.strip_imp_prems (prop_of intro) = [@{prop "False"}] then |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
23 |
[] |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
24 |
else [intro] |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
25 |
|
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
26 |
fun preprocess_strong_conn_constnames gr constnames thy = |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
27 |
let |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
28 |
val get_specs = map (fn k => (k, Graph.get_node gr k)) |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
29 |
val _ = priority ("Preprocessing scc of " ^ commas constnames) |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
30 |
val (prednames, funnames) = List.partition (is_pred thy) constnames |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
31 |
(* untangle recursion by defining predicates for all functions *) |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
32 |
val _ = priority "Compiling functions to predicates..." |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
33 |
val _ = Output.tracing ("funnames: " ^ commas funnames) |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
34 |
val thy' = |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
35 |
thy |> not (null funnames) ? Predicate_Compile_Fun.define_predicates |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
36 |
(get_specs funnames) |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
37 |
val _ = priority "Compiling predicates to flat introrules..." |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
38 |
val (intross, thy'') = apfst flat (fold_map Predicate_Compile_Pred.preprocess |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
39 |
(get_specs prednames) thy') |
32672
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32669
diff
changeset
|
40 |
val _ = tracing ("Flattened introduction rules: " ^ |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32669
diff
changeset
|
41 |
commas (map (Display.string_of_thm_global thy'') (flat intross))) |
32668
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
42 |
val _ = priority "Replacing functions in introrules..." |
32672
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32669
diff
changeset
|
43 |
(* val _ = burrow (maps (Predicate_Compile_Fun.rewrite_intro thy'')) intross *) |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32669
diff
changeset
|
44 |
val intross' = |
33108
9d9afd478016
added test for higher-order function inductification; added debug messages
bulwahn
parents:
33107
diff
changeset
|
45 |
if fail_safe_mode then |
9d9afd478016
added test for higher-order function inductification; added debug messages
bulwahn
parents:
33107
diff
changeset
|
46 |
case try (burrow (maps (Predicate_Compile_Fun.rewrite_intro thy''))) intross of |
9d9afd478016
added test for higher-order function inductification; added debug messages
bulwahn
parents:
33107
diff
changeset
|
47 |
SOME intross' => intross' |
9d9afd478016
added test for higher-order function inductification; added debug messages
bulwahn
parents:
33107
diff
changeset
|
48 |
| NONE => let val _ = warning "Function replacement failed!" in intross end |
9d9afd478016
added test for higher-order function inductification; added debug messages
bulwahn
parents:
33107
diff
changeset
|
49 |
else burrow (maps (Predicate_Compile_Fun.rewrite_intro thy'')) intross |
32672
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32669
diff
changeset
|
50 |
val _ = tracing ("Introduction rules with replaced functions: " ^ |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32669
diff
changeset
|
51 |
commas (map (Display.string_of_thm_global thy'') (flat intross'))) |
32669
462b1dd67a58
added context free grammar example; removed dead code; adapted to work without quick and dirty mode; fixed typo
bulwahn
parents:
32668
diff
changeset
|
52 |
val intross'' = burrow (maps remove_pointless_clauses) intross' |
32672
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32669
diff
changeset
|
53 |
val intross'' = burrow (map (AxClass.overload thy'')) intross'' |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32669
diff
changeset
|
54 |
val _ = priority "Registering intro rules..." |
32668
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
55 |
val thy''' = fold Predicate_Compile_Core.register_intros intross'' thy'' |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
56 |
in |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
57 |
thy''' |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
58 |
end; |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
59 |
|
32672
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32669
diff
changeset
|
60 |
fun preprocess const thy = |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32669
diff
changeset
|
61 |
let |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32669
diff
changeset
|
62 |
val _ = Output.tracing ("Fetching definitions from theory...") |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32669
diff
changeset
|
63 |
val table = Pred_Compile_Data.make_const_spec_table thy |
33107
6aa76ce59ef2
added filtering of case constants in the definition retrieval of the predicate compiler
bulwahn
parents:
32672
diff
changeset
|
64 |
val gr = Pred_Compile_Data.obtain_specification_graph thy table const |
32672
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32669
diff
changeset
|
65 |
val _ = Output.tracing (commas (Graph.all_succs gr [const])) |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32669
diff
changeset
|
66 |
val gr = Graph.subgraph (member (op =) (Graph.all_succs gr [const])) gr |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32669
diff
changeset
|
67 |
in fold_rev (preprocess_strong_conn_constnames gr) |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32669
diff
changeset
|
68 |
(Graph.strong_conn gr) thy |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32669
diff
changeset
|
69 |
end |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32669
diff
changeset
|
70 |
|
32668
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
71 |
fun code_pred_cmd ((inductify_all, rpred), raw_const) lthy = |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
72 |
if inductify_all then |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
73 |
let |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
74 |
val thy = ProofContext.theory_of lthy |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
75 |
val const = Code.read_const thy raw_const |
32672
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32669
diff
changeset
|
76 |
val lthy' = LocalTheory.theory (preprocess const) lthy |
32668
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
77 |
|> LocalTheory.checkpoint |
32672
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32669
diff
changeset
|
78 |
val _ = tracing "Starting Predicate Compile Core..." |
32668
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
79 |
in Predicate_Compile_Core.code_pred_cmd rpred raw_const lthy' end |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
80 |
else |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
81 |
Predicate_Compile_Core.code_pred_cmd rpred raw_const lthy |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
82 |
|
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
83 |
val setup = Predicate_Compile_Fun.setup_oracle #> Predicate_Compile_Core.setup |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
84 |
|
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
85 |
val _ = List.app OuterKeyword.keyword ["inductify_all", "rpred"] |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
86 |
|
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
87 |
local structure P = OuterParse |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
88 |
in |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
89 |
|
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
90 |
val _ = OuterSyntax.local_theory_to_proof "code_pred" |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
91 |
"prove equations for predicate specified by intro/elim rules" |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
92 |
OuterKeyword.thy_goal (P.opt_keyword "inductify_all" -- P.opt_keyword "rpred" -- P.term_group >> code_pred_cmd) |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
93 |
|
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
94 |
end |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
95 |
|
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
96 |
end |