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