author | bulwahn |
Sat, 24 Oct 2009 16:55:42 +0200 | |
changeset 33130 | 7eac458c2b22 |
parent 33127 | eb91ec1ef6f0 |
child 33132 | 07efd452a698 |
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 |
Auxilary functions for 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 |
|
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
6 |
structure Predicate_Compile_Aux = |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
7 |
struct |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
8 |
|
33130
7eac458c2b22
added option show_mode_inference; added splitting of conjunctions in expand_tuples
bulwahn
parents:
33127
diff
changeset
|
9 |
(* general syntactic functions *) |
7eac458c2b22
added option show_mode_inference; added splitting of conjunctions in expand_tuples
bulwahn
parents:
33127
diff
changeset
|
10 |
|
7eac458c2b22
added option show_mode_inference; added splitting of conjunctions in expand_tuples
bulwahn
parents:
33127
diff
changeset
|
11 |
(*Like dest_conj, but flattens conjunctions however nested*) |
7eac458c2b22
added option show_mode_inference; added splitting of conjunctions in expand_tuples
bulwahn
parents:
33127
diff
changeset
|
12 |
fun conjuncts_aux (Const ("op &", _) $ t $ t') conjs = conjuncts_aux t (conjuncts_aux t' conjs) |
7eac458c2b22
added option show_mode_inference; added splitting of conjunctions in expand_tuples
bulwahn
parents:
33127
diff
changeset
|
13 |
| conjuncts_aux t conjs = t::conjs; |
7eac458c2b22
added option show_mode_inference; added splitting of conjunctions in expand_tuples
bulwahn
parents:
33127
diff
changeset
|
14 |
|
7eac458c2b22
added option show_mode_inference; added splitting of conjunctions in expand_tuples
bulwahn
parents:
33127
diff
changeset
|
15 |
fun conjuncts t = conjuncts_aux t []; |
7eac458c2b22
added option show_mode_inference; added splitting of conjunctions in expand_tuples
bulwahn
parents:
33127
diff
changeset
|
16 |
|
32668
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
17 |
(* syntactic functions *) |
33130
7eac458c2b22
added option show_mode_inference; added splitting of conjunctions in expand_tuples
bulwahn
parents:
33127
diff
changeset
|
18 |
|
32668
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
19 |
fun is_equationlike_term (Const ("==", _) $ _ $ _) = true |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
20 |
| is_equationlike_term (Const ("Trueprop", _) $ (Const ("op =", _) $ _ $ _)) = true |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
21 |
| is_equationlike_term _ = false |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
22 |
|
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
23 |
val is_equationlike = is_equationlike_term o prop_of |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
24 |
|
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
25 |
fun is_pred_equation_term (Const ("==", _) $ u $ v) = |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
26 |
(fastype_of u = @{typ bool}) andalso (fastype_of v = @{typ bool}) |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
27 |
| is_pred_equation_term _ = false |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
28 |
|
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
29 |
val is_pred_equation = is_pred_equation_term o prop_of |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
30 |
|
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
31 |
fun is_intro_term constname t = |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
32 |
case fst (strip_comb (HOLogic.dest_Trueprop (Logic.strip_imp_concl t))) of |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
33 |
Const (c, _) => c = constname |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
34 |
| _ => false |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
35 |
|
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
36 |
fun is_intro constname t = is_intro_term constname (prop_of t) |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
37 |
|
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
38 |
fun is_pred thy constname = |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
39 |
let |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
40 |
val T = (Sign.the_const_type thy constname) |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
41 |
in body_type T = @{typ "bool"} end; |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
42 |
|
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
43 |
|
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
44 |
fun is_predT (T as Type("fun", [_, _])) = (snd (strip_type T) = HOLogic.boolT) |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
45 |
| is_predT _ = false |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
46 |
|
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 |
(*** check if a term contains only constructor functions ***) |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
49 |
fun is_constrt thy = |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
50 |
let |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
51 |
val cnstrs = flat (maps |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
52 |
(map (fn (_, (Tname, _, cs)) => map (apsnd (rpair Tname o length)) cs) o #descr o snd) |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
53 |
(Symtab.dest (Datatype.get_all thy))); |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
54 |
fun check t = (case strip_comb t of |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
55 |
(Free _, []) => true |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
56 |
| (Const (s, T), ts) => (case (AList.lookup (op =) cnstrs s, body_type T) of |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
57 |
(SOME (i, Tname), Type (Tname', _)) => length ts = i andalso Tname = Tname' andalso forall check ts |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
58 |
| _ => false) |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
59 |
| _ => false) |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
60 |
in check end; |
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 |
fun strip_ex (Const ("Ex", _) $ Abs (x, T, t)) = |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
63 |
let |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
64 |
val (xTs, t') = strip_ex t |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
65 |
in |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
66 |
((x, T) :: xTs, t') |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
67 |
end |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
68 |
| strip_ex t = ([], t) |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
69 |
|
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
70 |
fun focus_ex t nctxt = |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
71 |
let |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
72 |
val ((xs, Ts), t') = apfst split_list (strip_ex t) |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
73 |
val (xs', nctxt') = Name.variants xs nctxt; |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
74 |
val ps' = xs' ~~ Ts; |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
75 |
val vs = map Free ps'; |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
76 |
val t'' = Term.subst_bounds (rev vs, t'); |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
77 |
in ((ps', t''), nctxt') end; |
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 |
|
33123
3c7c4372f9ad
cleaned up debugging messages; added options to code_pred command
bulwahn
parents:
33113
diff
changeset
|
80 |
(* introduction rule combinators *) |
32668
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
81 |
|
33123
3c7c4372f9ad
cleaned up debugging messages; added options to code_pred command
bulwahn
parents:
33113
diff
changeset
|
82 |
(* combinators to apply a function to all literals of an introduction rules *) |
32668
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
83 |
|
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
84 |
fun map_atoms f intro = |
33130
7eac458c2b22
added option show_mode_inference; added splitting of conjunctions in expand_tuples
bulwahn
parents:
33127
diff
changeset
|
85 |
let |
7eac458c2b22
added option show_mode_inference; added splitting of conjunctions in expand_tuples
bulwahn
parents:
33127
diff
changeset
|
86 |
val (literals, head) = Logic.strip_horn intro |
7eac458c2b22
added option show_mode_inference; added splitting of conjunctions in expand_tuples
bulwahn
parents:
33127
diff
changeset
|
87 |
fun appl t = (case t of |
7eac458c2b22
added option show_mode_inference; added splitting of conjunctions in expand_tuples
bulwahn
parents:
33127
diff
changeset
|
88 |
(@{term "Not"} $ t') => HOLogic.mk_not (f t') |
7eac458c2b22
added option show_mode_inference; added splitting of conjunctions in expand_tuples
bulwahn
parents:
33127
diff
changeset
|
89 |
| _ => f t) |
7eac458c2b22
added option show_mode_inference; added splitting of conjunctions in expand_tuples
bulwahn
parents:
33127
diff
changeset
|
90 |
in |
7eac458c2b22
added option show_mode_inference; added splitting of conjunctions in expand_tuples
bulwahn
parents:
33127
diff
changeset
|
91 |
Logic.list_implies |
7eac458c2b22
added option show_mode_inference; added splitting of conjunctions in expand_tuples
bulwahn
parents:
33127
diff
changeset
|
92 |
(map (HOLogic.mk_Trueprop o appl o HOLogic.dest_Trueprop) literals, head) |
7eac458c2b22
added option show_mode_inference; added splitting of conjunctions in expand_tuples
bulwahn
parents:
33127
diff
changeset
|
93 |
end |
33123
3c7c4372f9ad
cleaned up debugging messages; added options to code_pred command
bulwahn
parents:
33113
diff
changeset
|
94 |
|
33113 | 95 |
fun fold_atoms f intro s = |
96 |
let |
|
97 |
val (literals, head) = Logic.strip_horn intro |
|
98 |
fun appl t s = (case t of |
|
99 |
(@{term "Not"} $ t') => f t' s |
|
100 |
| _ => f t s) |
|
101 |
in fold appl (map HOLogic.dest_Trueprop literals) s end |
|
102 |
||
32668
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
103 |
fun fold_map_atoms f intro s = |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
104 |
let |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
105 |
val (literals, head) = Logic.strip_horn intro |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
106 |
fun appl t s = (case t of |
33130
7eac458c2b22
added option show_mode_inference; added splitting of conjunctions in expand_tuples
bulwahn
parents:
33127
diff
changeset
|
107 |
(@{term "Not"} $ t') => apfst HOLogic.mk_not (f t' s) |
32668
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
108 |
| _ => f t s) |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
109 |
val (literals', s') = fold_map appl (map HOLogic.dest_Trueprop literals) s |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
110 |
in |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
111 |
(Logic.list_implies (map HOLogic.mk_Trueprop literals', head), s') |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
112 |
end; |
33130
7eac458c2b22
added option show_mode_inference; added splitting of conjunctions in expand_tuples
bulwahn
parents:
33127
diff
changeset
|
113 |
|
7eac458c2b22
added option show_mode_inference; added splitting of conjunctions in expand_tuples
bulwahn
parents:
33127
diff
changeset
|
114 |
fun maps_premises f intro = |
7eac458c2b22
added option show_mode_inference; added splitting of conjunctions in expand_tuples
bulwahn
parents:
33127
diff
changeset
|
115 |
let |
7eac458c2b22
added option show_mode_inference; added splitting of conjunctions in expand_tuples
bulwahn
parents:
33127
diff
changeset
|
116 |
val (premises, head) = Logic.strip_horn intro |
7eac458c2b22
added option show_mode_inference; added splitting of conjunctions in expand_tuples
bulwahn
parents:
33127
diff
changeset
|
117 |
in |
7eac458c2b22
added option show_mode_inference; added splitting of conjunctions in expand_tuples
bulwahn
parents:
33127
diff
changeset
|
118 |
Logic.list_implies (maps f premises, head) |
7eac458c2b22
added option show_mode_inference; added splitting of conjunctions in expand_tuples
bulwahn
parents:
33127
diff
changeset
|
119 |
end |
32668
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
120 |
|
33130
7eac458c2b22
added option show_mode_inference; added splitting of conjunctions in expand_tuples
bulwahn
parents:
33127
diff
changeset
|
121 |
(* lifting term operations to theorems *) |
7eac458c2b22
added option show_mode_inference; added splitting of conjunctions in expand_tuples
bulwahn
parents:
33127
diff
changeset
|
122 |
|
7eac458c2b22
added option show_mode_inference; added splitting of conjunctions in expand_tuples
bulwahn
parents:
33127
diff
changeset
|
123 |
fun map_term thy f th = |
7eac458c2b22
added option show_mode_inference; added splitting of conjunctions in expand_tuples
bulwahn
parents:
33127
diff
changeset
|
124 |
setmp quick_and_dirty true (SkipProof.make_thm thy) (f (prop_of th)) |
7eac458c2b22
added option show_mode_inference; added splitting of conjunctions in expand_tuples
bulwahn
parents:
33127
diff
changeset
|
125 |
|
32668
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 equals_conv lhs_cv rhs_cv ct = |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
128 |
case Thm.term_of ct of |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
129 |
Const ("==", _) $ _ $ _ => Conv.arg_conv cv ct |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
130 |
| _ => error "equals_conv" |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
131 |
*) |
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
132 |
|
33123
3c7c4372f9ad
cleaned up debugging messages; added options to code_pred command
bulwahn
parents:
33113
diff
changeset
|
133 |
(* Different options for compiler *) |
3c7c4372f9ad
cleaned up debugging messages; added options to code_pred command
bulwahn
parents:
33113
diff
changeset
|
134 |
|
3c7c4372f9ad
cleaned up debugging messages; added options to code_pred command
bulwahn
parents:
33113
diff
changeset
|
135 |
datatype options = Options of { |
3c7c4372f9ad
cleaned up debugging messages; added options to code_pred command
bulwahn
parents:
33113
diff
changeset
|
136 |
(*check_modes : (string * int list list) list,*) |
3c7c4372f9ad
cleaned up debugging messages; added options to code_pred command
bulwahn
parents:
33113
diff
changeset
|
137 |
show_steps : bool, |
3c7c4372f9ad
cleaned up debugging messages; added options to code_pred command
bulwahn
parents:
33113
diff
changeset
|
138 |
show_mode_inference : bool, |
33127 | 139 |
show_proof_trace : bool, |
33125 | 140 |
show_intermediate_results : bool, |
33123
3c7c4372f9ad
cleaned up debugging messages; added options to code_pred command
bulwahn
parents:
33113
diff
changeset
|
141 |
(* |
3c7c4372f9ad
cleaned up debugging messages; added options to code_pred command
bulwahn
parents:
33113
diff
changeset
|
142 |
inductify_functions : bool, |
3c7c4372f9ad
cleaned up debugging messages; added options to code_pred command
bulwahn
parents:
33113
diff
changeset
|
143 |
*) |
3c7c4372f9ad
cleaned up debugging messages; added options to code_pred command
bulwahn
parents:
33113
diff
changeset
|
144 |
inductify : bool, |
3c7c4372f9ad
cleaned up debugging messages; added options to code_pred command
bulwahn
parents:
33113
diff
changeset
|
145 |
rpred : bool |
3c7c4372f9ad
cleaned up debugging messages; added options to code_pred command
bulwahn
parents:
33113
diff
changeset
|
146 |
}; |
3c7c4372f9ad
cleaned up debugging messages; added options to code_pred command
bulwahn
parents:
33113
diff
changeset
|
147 |
|
33125 | 148 |
fun show_steps (Options opt) = #show_steps opt |
33130
7eac458c2b22
added option show_mode_inference; added splitting of conjunctions in expand_tuples
bulwahn
parents:
33127
diff
changeset
|
149 |
fun show_mode_inference (Options opt) = #show_mode_inference opt |
33125 | 150 |
fun show_intermediate_results (Options opt) = #show_intermediate_results opt |
33127 | 151 |
fun show_proof_trace (Options opt) = #show_proof_trace opt |
33125 | 152 |
|
33123
3c7c4372f9ad
cleaned up debugging messages; added options to code_pred command
bulwahn
parents:
33113
diff
changeset
|
153 |
fun is_inductify (Options opt) = #inductify opt |
3c7c4372f9ad
cleaned up debugging messages; added options to code_pred command
bulwahn
parents:
33113
diff
changeset
|
154 |
fun is_rpred (Options opt) = #rpred opt |
3c7c4372f9ad
cleaned up debugging messages; added options to code_pred command
bulwahn
parents:
33113
diff
changeset
|
155 |
|
3c7c4372f9ad
cleaned up debugging messages; added options to code_pred command
bulwahn
parents:
33113
diff
changeset
|
156 |
|
3c7c4372f9ad
cleaned up debugging messages; added options to code_pred command
bulwahn
parents:
33113
diff
changeset
|
157 |
val default_options = Options { |
3c7c4372f9ad
cleaned up debugging messages; added options to code_pred command
bulwahn
parents:
33113
diff
changeset
|
158 |
show_steps = false, |
33125 | 159 |
show_intermediate_results = false, |
33127 | 160 |
show_proof_trace = false, |
33123
3c7c4372f9ad
cleaned up debugging messages; added options to code_pred command
bulwahn
parents:
33113
diff
changeset
|
161 |
show_mode_inference = false, |
3c7c4372f9ad
cleaned up debugging messages; added options to code_pred command
bulwahn
parents:
33113
diff
changeset
|
162 |
inductify = false, |
3c7c4372f9ad
cleaned up debugging messages; added options to code_pred command
bulwahn
parents:
33113
diff
changeset
|
163 |
rpred = false |
3c7c4372f9ad
cleaned up debugging messages; added options to code_pred command
bulwahn
parents:
33113
diff
changeset
|
164 |
} |
3c7c4372f9ad
cleaned up debugging messages; added options to code_pred command
bulwahn
parents:
33113
diff
changeset
|
165 |
|
3c7c4372f9ad
cleaned up debugging messages; added options to code_pred command
bulwahn
parents:
33113
diff
changeset
|
166 |
|
3c7c4372f9ad
cleaned up debugging messages; added options to code_pred command
bulwahn
parents:
33113
diff
changeset
|
167 |
fun print_step options s = |
33125 | 168 |
if show_steps options then tracing s else () |
33130
7eac458c2b22
added option show_mode_inference; added splitting of conjunctions in expand_tuples
bulwahn
parents:
33127
diff
changeset
|
169 |
|
32668
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
170 |
|
33124
5378e61add1a
continued cleaning up; moved tuple expanding to core
bulwahn
parents:
33123
diff
changeset
|
171 |
(* tuple processing *) |
5378e61add1a
continued cleaning up; moved tuple expanding to core
bulwahn
parents:
33123
diff
changeset
|
172 |
|
5378e61add1a
continued cleaning up; moved tuple expanding to core
bulwahn
parents:
33123
diff
changeset
|
173 |
fun expand_tuples thy intro = |
5378e61add1a
continued cleaning up; moved tuple expanding to core
bulwahn
parents:
33123
diff
changeset
|
174 |
let |
5378e61add1a
continued cleaning up; moved tuple expanding to core
bulwahn
parents:
33123
diff
changeset
|
175 |
fun rewrite_args [] (pats, intro_t, ctxt) = (pats, intro_t, ctxt) |
5378e61add1a
continued cleaning up; moved tuple expanding to core
bulwahn
parents:
33123
diff
changeset
|
176 |
| rewrite_args (arg::args) (pats, intro_t, ctxt) = |
5378e61add1a
continued cleaning up; moved tuple expanding to core
bulwahn
parents:
33123
diff
changeset
|
177 |
(case HOLogic.strip_tupleT (fastype_of arg) of |
5378e61add1a
continued cleaning up; moved tuple expanding to core
bulwahn
parents:
33123
diff
changeset
|
178 |
(Ts as _ :: _ :: _) => |
5378e61add1a
continued cleaning up; moved tuple expanding to core
bulwahn
parents:
33123
diff
changeset
|
179 |
let |
5378e61add1a
continued cleaning up; moved tuple expanding to core
bulwahn
parents:
33123
diff
changeset
|
180 |
fun rewrite_arg' (Const ("Pair", _) $ _ $ t2, Type ("*", [_, T2])) |
5378e61add1a
continued cleaning up; moved tuple expanding to core
bulwahn
parents:
33123
diff
changeset
|
181 |
(args, (pats, intro_t, ctxt)) = rewrite_arg' (t2, T2) (args, (pats, intro_t, ctxt)) |
5378e61add1a
continued cleaning up; moved tuple expanding to core
bulwahn
parents:
33123
diff
changeset
|
182 |
| rewrite_arg' (t, Type ("*", [T1, T2])) (args, (pats, intro_t, ctxt)) = |
5378e61add1a
continued cleaning up; moved tuple expanding to core
bulwahn
parents:
33123
diff
changeset
|
183 |
let |
5378e61add1a
continued cleaning up; moved tuple expanding to core
bulwahn
parents:
33123
diff
changeset
|
184 |
val ([x, y], ctxt') = Variable.variant_fixes ["x", "y"] ctxt |
5378e61add1a
continued cleaning up; moved tuple expanding to core
bulwahn
parents:
33123
diff
changeset
|
185 |
val pat = (t, HOLogic.mk_prod (Free (x, T1), Free (y, T2))) |
5378e61add1a
continued cleaning up; moved tuple expanding to core
bulwahn
parents:
33123
diff
changeset
|
186 |
val intro_t' = Pattern.rewrite_term thy [pat] [] intro_t |
5378e61add1a
continued cleaning up; moved tuple expanding to core
bulwahn
parents:
33123
diff
changeset
|
187 |
val args' = map (Pattern.rewrite_term thy [pat] []) args |
5378e61add1a
continued cleaning up; moved tuple expanding to core
bulwahn
parents:
33123
diff
changeset
|
188 |
in |
5378e61add1a
continued cleaning up; moved tuple expanding to core
bulwahn
parents:
33123
diff
changeset
|
189 |
rewrite_arg' (Free (y, T2), T2) (args', (pat::pats, intro_t', ctxt')) |
5378e61add1a
continued cleaning up; moved tuple expanding to core
bulwahn
parents:
33123
diff
changeset
|
190 |
end |
5378e61add1a
continued cleaning up; moved tuple expanding to core
bulwahn
parents:
33123
diff
changeset
|
191 |
| rewrite_arg' _ (args, (pats, intro_t, ctxt)) = (args, (pats, intro_t, ctxt)) |
5378e61add1a
continued cleaning up; moved tuple expanding to core
bulwahn
parents:
33123
diff
changeset
|
192 |
val (args', (pats, intro_t', ctxt')) = rewrite_arg' (arg, fastype_of arg) |
5378e61add1a
continued cleaning up; moved tuple expanding to core
bulwahn
parents:
33123
diff
changeset
|
193 |
(args, (pats, intro_t, ctxt)) |
5378e61add1a
continued cleaning up; moved tuple expanding to core
bulwahn
parents:
33123
diff
changeset
|
194 |
in |
5378e61add1a
continued cleaning up; moved tuple expanding to core
bulwahn
parents:
33123
diff
changeset
|
195 |
rewrite_args args' (pats, intro_t', ctxt') |
5378e61add1a
continued cleaning up; moved tuple expanding to core
bulwahn
parents:
33123
diff
changeset
|
196 |
end |
5378e61add1a
continued cleaning up; moved tuple expanding to core
bulwahn
parents:
33123
diff
changeset
|
197 |
| _ => rewrite_args args (pats, intro_t, ctxt)) |
5378e61add1a
continued cleaning up; moved tuple expanding to core
bulwahn
parents:
33123
diff
changeset
|
198 |
fun rewrite_prem atom = |
5378e61add1a
continued cleaning up; moved tuple expanding to core
bulwahn
parents:
33123
diff
changeset
|
199 |
let |
5378e61add1a
continued cleaning up; moved tuple expanding to core
bulwahn
parents:
33123
diff
changeset
|
200 |
val (_, args) = strip_comb atom |
5378e61add1a
continued cleaning up; moved tuple expanding to core
bulwahn
parents:
33123
diff
changeset
|
201 |
in rewrite_args args end |
5378e61add1a
continued cleaning up; moved tuple expanding to core
bulwahn
parents:
33123
diff
changeset
|
202 |
val ctxt = ProofContext.init thy |
5378e61add1a
continued cleaning up; moved tuple expanding to core
bulwahn
parents:
33123
diff
changeset
|
203 |
val (((T_insts, t_insts), [intro']), ctxt1) = Variable.import false [intro] ctxt |
5378e61add1a
continued cleaning up; moved tuple expanding to core
bulwahn
parents:
33123
diff
changeset
|
204 |
val intro_t = prop_of intro' |
5378e61add1a
continued cleaning up; moved tuple expanding to core
bulwahn
parents:
33123
diff
changeset
|
205 |
val concl = Logic.strip_imp_concl intro_t |
5378e61add1a
continued cleaning up; moved tuple expanding to core
bulwahn
parents:
33123
diff
changeset
|
206 |
val (p, args) = strip_comb (HOLogic.dest_Trueprop concl) |
5378e61add1a
continued cleaning up; moved tuple expanding to core
bulwahn
parents:
33123
diff
changeset
|
207 |
val (pats', intro_t', ctxt2) = rewrite_args args ([], intro_t, ctxt1) |
5378e61add1a
continued cleaning up; moved tuple expanding to core
bulwahn
parents:
33123
diff
changeset
|
208 |
val (pats', intro_t', ctxt3) = |
5378e61add1a
continued cleaning up; moved tuple expanding to core
bulwahn
parents:
33123
diff
changeset
|
209 |
fold_atoms rewrite_prem intro_t' (pats', intro_t', ctxt2) |
5378e61add1a
continued cleaning up; moved tuple expanding to core
bulwahn
parents:
33123
diff
changeset
|
210 |
fun rewrite_pat (ct1, ct2) = |
5378e61add1a
continued cleaning up; moved tuple expanding to core
bulwahn
parents:
33123
diff
changeset
|
211 |
(ct1, cterm_of thy (Pattern.rewrite_term thy pats' [] (term_of ct2))) |
5378e61add1a
continued cleaning up; moved tuple expanding to core
bulwahn
parents:
33123
diff
changeset
|
212 |
val t_insts' = map rewrite_pat t_insts |
5378e61add1a
continued cleaning up; moved tuple expanding to core
bulwahn
parents:
33123
diff
changeset
|
213 |
val intro'' = Thm.instantiate (T_insts, t_insts') intro |
5378e61add1a
continued cleaning up; moved tuple expanding to core
bulwahn
parents:
33123
diff
changeset
|
214 |
val [intro'''] = Variable.export ctxt3 ctxt [intro''] |
5378e61add1a
continued cleaning up; moved tuple expanding to core
bulwahn
parents:
33123
diff
changeset
|
215 |
val intro'''' = Simplifier.full_simplify |
5378e61add1a
continued cleaning up; moved tuple expanding to core
bulwahn
parents:
33123
diff
changeset
|
216 |
(HOL_basic_ss addsimps [@{thm fst_conv}, @{thm snd_conv}, @{thm Pair_eq}]) |
5378e61add1a
continued cleaning up; moved tuple expanding to core
bulwahn
parents:
33123
diff
changeset
|
217 |
intro''' |
33130
7eac458c2b22
added option show_mode_inference; added splitting of conjunctions in expand_tuples
bulwahn
parents:
33127
diff
changeset
|
218 |
(* splitting conjunctions introduced by Pair_eq*) |
7eac458c2b22
added option show_mode_inference; added splitting of conjunctions in expand_tuples
bulwahn
parents:
33127
diff
changeset
|
219 |
fun split_conj prem = |
7eac458c2b22
added option show_mode_inference; added splitting of conjunctions in expand_tuples
bulwahn
parents:
33127
diff
changeset
|
220 |
map HOLogic.mk_Trueprop (conjuncts (HOLogic.dest_Trueprop prem)) |
7eac458c2b22
added option show_mode_inference; added splitting of conjunctions in expand_tuples
bulwahn
parents:
33127
diff
changeset
|
221 |
val intro''''' = map_term thy (maps_premises split_conj) intro'''' |
33124
5378e61add1a
continued cleaning up; moved tuple expanding to core
bulwahn
parents:
33123
diff
changeset
|
222 |
in |
33130
7eac458c2b22
added option show_mode_inference; added splitting of conjunctions in expand_tuples
bulwahn
parents:
33127
diff
changeset
|
223 |
intro''''' |
33124
5378e61add1a
continued cleaning up; moved tuple expanding to core
bulwahn
parents:
33123
diff
changeset
|
224 |
end |
5378e61add1a
continued cleaning up; moved tuple expanding to core
bulwahn
parents:
33123
diff
changeset
|
225 |
|
5378e61add1a
continued cleaning up; moved tuple expanding to core
bulwahn
parents:
33123
diff
changeset
|
226 |
|
5378e61add1a
continued cleaning up; moved tuple expanding to core
bulwahn
parents:
33123
diff
changeset
|
227 |
|
32668
b2de45007537
added first prototype of the extended predicate compiler
bulwahn
parents:
diff
changeset
|
228 |
end; |