author | bulwahn |
Sat, 24 Oct 2009 20:27:26 +0200 | |
changeset 33150 | 75eddea4abef |
parent 33149 | 2c8f1c450b47 |
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 |
Book-keeping datastructure for the predicate compiler |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
4 |
|
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
5 |
*) |
33140
83951822bfd0
cleaning the signature of the predicate compiler core; renaming signature and structures to uniform long names
bulwahn
parents:
33130
diff
changeset
|
6 |
signature PREDICATE_COMPILE_DATA = |
32668
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
7 |
sig |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
8 |
type specification_table; |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
9 |
val make_const_spec_table : theory -> specification_table |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
10 |
val get_specification : specification_table -> string -> thm list |
33107
6aa76ce59ef2
added filtering of case constants in the definition retrieval of the predicate compiler
bulwahn
parents:
33104
diff
changeset
|
11 |
val obtain_specification_graph : theory -> specification_table -> string -> thm list Graph.T |
32668
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
12 |
val normalize_equation : theory -> thm -> thm |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
13 |
end; |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
14 |
|
33140
83951822bfd0
cleaning the signature of the predicate compiler core; renaming signature and structures to uniform long names
bulwahn
parents:
33130
diff
changeset
|
15 |
structure Predicate_Compile_Data : PREDICATE_COMPILE_DATA = |
32668
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
16 |
struct |
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 |
open Predicate_Compile_Aux; |
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 |
structure Data = TheoryDataFun |
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 |
type T = |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
23 |
{const_spec_table : thm list Symtab.table}; |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
24 |
val empty = |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
25 |
{const_spec_table = Symtab.empty}; |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
26 |
val copy = I; |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
27 |
val extend = I; |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
28 |
fun merge _ |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
29 |
({const_spec_table = const_spec_table1}, |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
30 |
{const_spec_table = const_spec_table2}) = |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
31 |
{const_spec_table = Symtab.merge (K true) (const_spec_table1, const_spec_table2)} |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
32 |
); |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
33 |
|
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
34 |
fun mk_data c = {const_spec_table = c} |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
35 |
fun map_data f {const_spec_table = c} = mk_data (f c) |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
36 |
|
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
37 |
type specification_table = thm list Symtab.table |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
38 |
|
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
39 |
fun defining_const_of_introrule_term t = |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
40 |
let |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
41 |
val _ $ u = Logic.strip_imp_concl t |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
42 |
val (pred, all_args) = strip_comb u |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
43 |
in case pred of |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
44 |
Const (c, T) => c |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
45 |
| _ => raise TERM ("defining_const_of_introrule_term failed: Not a constant", [t]) |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
46 |
end |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
47 |
|
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
48 |
val defining_const_of_introrule = defining_const_of_introrule_term o prop_of |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
49 |
|
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
50 |
(*TODO*) |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
51 |
fun is_introlike_term t = true |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
52 |
|
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
53 |
val is_introlike = is_introlike_term o prop_of |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
54 |
|
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
55 |
fun check_equation_format_term (t as (Const ("==", _) $ u $ v)) = |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
56 |
(case strip_comb u of |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
57 |
(Const (c, T), args) => |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
58 |
if (length (binder_types T) = length args) then |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
59 |
true |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
60 |
else |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
61 |
raise TERM ("check_equation_format_term failed: Number of arguments mismatch", [t]) |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
62 |
| _ => raise TERM ("check_equation_format_term failed: Not a constant", [t])) |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
63 |
| check_equation_format_term t = |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
64 |
raise TERM ("check_equation_format_term failed: Not an equation", [t]) |
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 |
val check_equation_format = check_equation_format_term o prop_of |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
67 |
|
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
68 |
fun defining_const_of_equation_term (t as (Const ("==", _) $ u $ v)) = |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
69 |
(case fst (strip_comb u) of |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
70 |
Const (c, _) => c |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
71 |
| _ => raise TERM ("defining_const_of_equation_term failed: Not a constant", [t])) |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
72 |
| defining_const_of_equation_term t = |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
73 |
raise TERM ("defining_const_of_equation_term failed: Not an equation", [t]) |
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 |
val defining_const_of_equation = defining_const_of_equation_term o prop_of |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
76 |
|
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
77 |
(* Normalizing equations *) |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
78 |
|
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
79 |
fun mk_meta_equation th = |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
80 |
case prop_of th of |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
81 |
Const ("Trueprop", _) $ (Const ("op =", _) $ _ $ _) => th RS @{thm eq_reflection} |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
82 |
| _ => th |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
83 |
|
33104 | 84 |
val meta_fun_cong = @{lemma "f == g ==> f x == g x" by simp} |
85 |
||
32668
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
86 |
fun full_fun_cong_expand th = |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
87 |
let |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
88 |
val (f, args) = strip_comb (fst (Logic.dest_equals (prop_of th))) |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
89 |
val i = length (binder_types (fastype_of f)) - length args |
33104 | 90 |
in funpow i (fn th => th RS meta_fun_cong) th end; |
32668
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
91 |
|
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
92 |
fun declare_names s xs ctxt = |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
93 |
let |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
94 |
val res = Name.names ctxt s xs |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
95 |
in (res, fold Name.declare (map fst res) ctxt) end |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
96 |
|
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
97 |
fun split_all_pairs thy th = |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
98 |
let |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
99 |
val ctxt = ProofContext.init thy |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
100 |
val ((_, [th']), ctxt') = Variable.import true [th] ctxt |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
101 |
val t = prop_of th' |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
102 |
val frees = Term.add_frees t [] |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
103 |
val freenames = Term.add_free_names t [] |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
104 |
val nctxt = Name.make_context freenames |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
105 |
fun mk_tuple_rewrites (x, T) nctxt = |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
106 |
let |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
107 |
val Ts = HOLogic.flatten_tupleT T |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
108 |
val (xTs, nctxt') = declare_names x Ts nctxt |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
109 |
val paths = HOLogic.flat_tupleT_paths T |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
110 |
in ((Free (x, T), HOLogic.mk_ptuple paths T (map Free xTs)), nctxt') end |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
111 |
val (rewr, _) = fold_map mk_tuple_rewrites frees nctxt |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
112 |
val t' = Pattern.rewrite_term thy rewr [] t |
32970
fbd2bb2489a8
operations of structure Skip_Proof (formerly SkipProof) no longer require quick_and_dirty mode;
wenzelm
parents:
32966
diff
changeset
|
113 |
val tac = Skip_Proof.cheat_tac thy |
32668
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
114 |
val th'' = Goal.prove ctxt (Term.add_free_names t' []) [] t' (fn {...} => tac) |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
115 |
val th''' = LocalDefs.unfold ctxt [@{thm split_conv}] th'' |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
116 |
in |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
117 |
th''' |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
118 |
end; |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
119 |
|
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
120 |
fun normalize_equation thy th = |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
121 |
mk_meta_equation th |
33150
75eddea4abef
further changes due to the previous merge in the predicate compiler
bulwahn
parents:
33149
diff
changeset
|
122 |
|> Predicate_Compile_Set.unfold_set_notation |
32668
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
123 |
|> full_fun_cong_expand |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
124 |
|> split_all_pairs thy |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
125 |
|> tap check_equation_format |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
126 |
|
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
127 |
fun inline_equations thy th = Conv.fconv_rule (Simplifier.rewrite |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
128 |
((Simplifier.theory_context thy Simplifier.empty_ss) addsimps (Predicate_Compile_Inline_Defs.get (ProofContext.init thy)))) th |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
129 |
|
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
130 |
fun store_thm_in_table ignore_consts thy th= |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
131 |
let |
33119
bf18c8174571
added theory with alternative definitions for the predicate compiler; cleaned up examples
bulwahn
parents:
33112
diff
changeset
|
132 |
val th = th |
32668
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
133 |
|> inline_equations thy |
33140
83951822bfd0
cleaning the signature of the predicate compiler core; renaming signature and structures to uniform long names
bulwahn
parents:
33130
diff
changeset
|
134 |
|> Predicate_Compile_Set.unfold_set_notation |
33130
7eac458c2b22
added option show_mode_inference; added splitting of conjunctions in expand_tuples
bulwahn
parents:
33129
diff
changeset
|
135 |
|> AxClass.unoverload thy |
32668
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
136 |
val (const, th) = |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
137 |
if is_equationlike th then |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
138 |
let |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
139 |
val eq = normalize_equation thy th |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
140 |
in |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
141 |
(defining_const_of_equation eq, eq) |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
142 |
end |
33119
bf18c8174571
added theory with alternative definitions for the predicate compiler; cleaned up examples
bulwahn
parents:
33112
diff
changeset
|
143 |
else if (is_introlike th) then (defining_const_of_introrule th, th) |
32668
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
144 |
else error "store_thm: unexpected definition format" |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
145 |
in |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
146 |
if not (member (op =) ignore_consts const) then |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
147 |
Symtab.cons_list (const, th) |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
148 |
else I |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
149 |
end |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
150 |
|
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
151 |
fun make_const_spec_table thy = |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
152 |
let |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
153 |
fun store ignore_const f = fold (store_thm_in_table ignore_const thy) (map (Thm.transfer thy) (f (ProofContext.init thy))) |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
154 |
val table = Symtab.empty |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
155 |
|> store [] Predicate_Compile_Alternative_Defs.get |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
156 |
val ignore_consts = Symtab.keys table |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
157 |
in |
33141
89b23fad5e02
modifying the depth-limited compilation to be sound, but now throws an error undefined in case of hitting the depth limit in an negative context; cleaning up the examples
bulwahn
parents:
33140
diff
changeset
|
158 |
table |
32668
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
159 |
|> store ignore_consts Predicate_Compile_Preproc_Const_Defs.get |
33056
791a4655cae3
renamed "nitpick_const_xxx" attributes to "nitpick_xxx" and "nitpick_ind_intros" to "nitpick_intros"
blanchet
parents:
32970
diff
changeset
|
160 |
|> store ignore_consts Nitpick_Simps.get |
791a4655cae3
renamed "nitpick_const_xxx" attributes to "nitpick_xxx" and "nitpick_ind_intros" to "nitpick_intros"
blanchet
parents:
32970
diff
changeset
|
161 |
|> store ignore_consts Nitpick_Intros.get |
32668
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
162 |
end |
33123
3c7c4372f9ad
cleaned up debugging messages; added options to code_pred command
bulwahn
parents:
33119
diff
changeset
|
163 |
|
32668
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
164 |
fun get_specification table constname = |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
165 |
case Symtab.lookup table constname of |
33123
3c7c4372f9ad
cleaned up debugging messages; added options to code_pred command
bulwahn
parents:
33119
diff
changeset
|
166 |
SOME thms => thms |
32668
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
167 |
| NONE => error ("get_specification: lookup of constant " ^ quote constname ^ " failed") |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
168 |
|
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
169 |
val logic_operator_names = |
33123
3c7c4372f9ad
cleaned up debugging messages; added options to code_pred command
bulwahn
parents:
33119
diff
changeset
|
170 |
[@{const_name "=="}, @{const_name "op ="}, @{const_name "op -->"}, @{const_name "All"}, @{const_name "Ex"}, |
3c7c4372f9ad
cleaned up debugging messages; added options to code_pred command
bulwahn
parents:
33119
diff
changeset
|
171 |
@{const_name "op &"}] |
32668
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
172 |
|
33119
bf18c8174571
added theory with alternative definitions for the predicate compiler; cleaned up examples
bulwahn
parents:
33112
diff
changeset
|
173 |
val special_cases = member (op =) [ |
bf18c8174571
added theory with alternative definitions for the predicate compiler; cleaned up examples
bulwahn
parents:
33112
diff
changeset
|
174 |
@{const_name "False"}, |
bf18c8174571
added theory with alternative definitions for the predicate compiler; cleaned up examples
bulwahn
parents:
33112
diff
changeset
|
175 |
@{const_name "Suc"}, @{const_name Nat.zero_nat_inst.zero_nat}, |
32668
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
176 |
@{const_name Nat.one_nat_inst.one_nat}, |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
177 |
@{const_name "HOL.ord_class.less"}, @{const_name "HOL.ord_class.less_eq"}, @{const_name "HOL.zero_class.zero"}, |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
178 |
@{const_name "HOL.one_class.one"}, @{const_name HOL.plus_class.plus}, |
32672
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32669
diff
changeset
|
179 |
@{const_name Nat.ord_nat_inst.less_eq_nat}, |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32669
diff
changeset
|
180 |
@{const_name number_nat_inst.number_of_nat}, |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32669
diff
changeset
|
181 |
@{const_name Int.Bit0}, |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32669
diff
changeset
|
182 |
@{const_name Int.Bit1}, |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32669
diff
changeset
|
183 |
@{const_name Int.Pls}, |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32669
diff
changeset
|
184 |
@{const_name "Int.zero_int_inst.zero_int"}, |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
32669
diff
changeset
|
185 |
@{const_name "List.filter"}] |
32668
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
186 |
|
33107
6aa76ce59ef2
added filtering of case constants in the definition retrieval of the predicate compiler
bulwahn
parents:
33104
diff
changeset
|
187 |
fun case_consts thy s = is_some (Datatype.info_of_case thy s) |
6aa76ce59ef2
added filtering of case constants in the definition retrieval of the predicate compiler
bulwahn
parents:
33104
diff
changeset
|
188 |
|
6aa76ce59ef2
added filtering of case constants in the definition retrieval of the predicate compiler
bulwahn
parents:
33104
diff
changeset
|
189 |
fun obtain_specification_graph thy table constname = |
32668
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
190 |
let |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
191 |
fun is_nondefining_constname c = member (op =) logic_operator_names c |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
192 |
val is_defining_constname = member (op =) (Symtab.keys table) |
33112
6672184a736b
added a few tricky examples with tuples; added alternative introduction rules for some constants; corrected mode analysis with negation; improved fetching of definitions
bulwahn
parents:
33107
diff
changeset
|
193 |
fun has_code_pred_intros c = is_some (try (Predicate_Compile_Core.intros_of thy) c) |
32668
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
194 |
fun defiants_of specs = |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
195 |
fold (Term.add_const_names o prop_of) specs [] |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
196 |
|> filter is_defining_constname |
33123
3c7c4372f9ad
cleaned up debugging messages; added options to code_pred command
bulwahn
parents:
33119
diff
changeset
|
197 |
|> filter_out is_nondefining_constname |
33112
6672184a736b
added a few tricky examples with tuples; added alternative introduction rules for some constants; corrected mode analysis with negation; improved fetching of definitions
bulwahn
parents:
33107
diff
changeset
|
198 |
|> filter_out has_code_pred_intros |
33107
6aa76ce59ef2
added filtering of case constants in the definition retrieval of the predicate compiler
bulwahn
parents:
33104
diff
changeset
|
199 |
|> filter_out (case_consts thy) |
32668
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
200 |
|> filter_out special_cases |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
201 |
fun extend constname = |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
202 |
let |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
203 |
val specs = get_specification table constname |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
204 |
in (specs, defiants_of specs) end; |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
205 |
in |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
206 |
Graph.extend extend constname Graph.empty |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
207 |
end; |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
208 |
|
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
209 |
|
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
210 |
end; |