1 (* Title: HOL/Tools/SMT2/verit_proof.ML |
|
2 Author: Mathias Fleury, ENS Rennes |
|
3 Author: Sascha Boehme, TU Muenchen |
|
4 |
|
5 VeriT proofs: parsing and abstract syntax tree. |
|
6 *) |
|
7 |
|
8 signature VERIT_PROOF = |
|
9 sig |
|
10 (*proofs*) |
|
11 datatype veriT_step = VeriT_Step of { |
|
12 id: string, |
|
13 rule: string, |
|
14 prems: string list, |
|
15 concl: term, |
|
16 fixes: string list} |
|
17 |
|
18 (*proof parser*) |
|
19 val parse: typ Symtab.table -> term Symtab.table -> string list -> |
|
20 Proof.context -> veriT_step list * Proof.context |
|
21 |
|
22 val veriT_step_prefix : string |
|
23 val veriT_input_rule: string |
|
24 val veriT_la_generic_rule : string |
|
25 val veriT_rewrite_rule : string |
|
26 val veriT_simp_arith_rule : string |
|
27 val veriT_tmp_ite_elim_rule : string |
|
28 val veriT_tmp_skolemize_rule : string |
|
29 end; |
|
30 |
|
31 structure VeriT_Proof: VERIT_PROOF = |
|
32 struct |
|
33 |
|
34 open SMTLIB2_Proof |
|
35 |
|
36 datatype veriT_node = VeriT_Node of { |
|
37 id: string, |
|
38 rule: string, |
|
39 prems: string list, |
|
40 concl: term, |
|
41 bounds: string list} |
|
42 |
|
43 fun mk_node id rule prems concl bounds = |
|
44 VeriT_Node {id = id, rule = rule, prems = prems, concl = concl, bounds = bounds} |
|
45 |
|
46 datatype veriT_step = VeriT_Step of { |
|
47 id: string, |
|
48 rule: string, |
|
49 prems: string list, |
|
50 concl: term, |
|
51 fixes: string list} |
|
52 |
|
53 fun mk_step id rule prems concl fixes = |
|
54 VeriT_Step {id = id, rule = rule, prems = prems, concl = concl, fixes = fixes} |
|
55 |
|
56 val veriT_step_prefix = ".c" |
|
57 val veriT_alpha_conv_rule = "tmp_alphaconv" |
|
58 val veriT_input_rule = "input" |
|
59 val veriT_la_generic_rule = "la_generic" |
|
60 val veriT_rewrite_rule = "__rewrite" (* arbitrary *) |
|
61 val veriT_simp_arith_rule = "simp_arith" |
|
62 val veriT_tmp_ite_elim_rule = "tmp_ite_elim" |
|
63 val veriT_tmp_skolemize_rule = "tmp_skolemize" |
|
64 |
|
65 (* proof parser *) |
|
66 |
|
67 fun node_of p cx = |
|
68 ([], cx) |
|
69 ||>> `(with_fresh_names (term_of p)) |
|
70 |>> snd |
|
71 |
|
72 (*in order to get Z3-style quantification*) |
|
73 fun repair_quantification (SMTLIB2.S (SMTLIB2.Sym "forall" :: l)) = |
|
74 let val (quantified_vars, t) = split_last (map repair_quantification l) |
|
75 in |
|
76 SMTLIB2.S (SMTLIB2.Sym "forall" :: SMTLIB2.S quantified_vars :: t :: []) |
|
77 end |
|
78 | repair_quantification (SMTLIB2.S (SMTLIB2.Sym "exists" :: l)) = |
|
79 let val (quantified_vars, t) = split_last (map repair_quantification l) |
|
80 in |
|
81 SMTLIB2.S (SMTLIB2.Sym "exists" :: SMTLIB2.S quantified_vars :: t :: []) |
|
82 end |
|
83 | repair_quantification (SMTLIB2.S l) = SMTLIB2.S (map repair_quantification l) |
|
84 | repair_quantification x = x |
|
85 |
|
86 fun replace_bound_var_by_free_var (q $ Abs (var, ty, u)) free_var = |
|
87 (case List.find (fn v => String.isPrefix v var) free_var of |
|
88 NONE => q $ Abs (var, ty, replace_bound_var_by_free_var u free_var) |
|
89 | SOME _ => replace_bound_var_by_free_var (Term.subst_bound (Free (var, ty), u)) free_var) |
|
90 | replace_bound_var_by_free_var (u $ v) free_vars = replace_bound_var_by_free_var u free_vars $ |
|
91 replace_bound_var_by_free_var v free_vars |
|
92 | replace_bound_var_by_free_var u _ = u |
|
93 |
|
94 fun find_type_in_formula (Abs(v, ty, u)) var_name = |
|
95 if String.isPrefix var_name v then SOME ty else find_type_in_formula u var_name |
|
96 | find_type_in_formula (u $ v) var_name = |
|
97 (case find_type_in_formula u var_name of |
|
98 NONE => find_type_in_formula v var_name |
|
99 | a => a) |
|
100 | find_type_in_formula _ _ = NONE |
|
101 |
|
102 fun add_bound_variables_to_ctxt cx bounds concl = |
|
103 fold (fn a => fn b => update_binding a b) |
|
104 (map (fn s => ((s, Term (Free (s, the_default dummyT (find_type_in_formula concl s)))))) |
|
105 bounds) cx |
|
106 |
|
107 fun update_step_and_cx (st as VeriT_Node {id, rule, prems, concl, bounds}) cx = |
|
108 if rule = veriT_tmp_ite_elim_rule then |
|
109 (mk_node id rule prems concl bounds, add_bound_variables_to_ctxt cx bounds concl) |
|
110 else if rule = veriT_tmp_skolemize_rule then |
|
111 let |
|
112 val concl' = replace_bound_var_by_free_var concl bounds |
|
113 in |
|
114 (mk_node id rule prems concl' [], add_bound_variables_to_ctxt cx bounds concl) |
|
115 end |
|
116 else |
|
117 (st, cx) |
|
118 |
|
119 (*FIXME: using a reference would be better to know th numbers of the steps to add*) |
|
120 fun fix_subproof_steps ((((id_of_father_step, rule), prems), subproof), ((step_concl, bounds), |
|
121 cx)) = |
|
122 let |
|
123 fun mk_prop_of_term concl = (fastype_of concl = @{typ "bool"} ? |
|
124 curry (op $) @{term "Trueprop"}) concl |
|
125 fun inline_assumption assumption assumption_id (st as VeriT_Node {id, rule, prems, concl, |
|
126 bounds}) = |
|
127 if List.find (curry (op =) assumption_id) prems <> NONE then |
|
128 let |
|
129 val prems' = filter_out (curry (op =) assumption_id) prems |
|
130 in |
|
131 mk_node id rule (filter_out (curry (op =) assumption_id) prems') |
|
132 (Const (@{const_name "Pure.imp"}, @{typ "prop"} --> @{typ "prop"} --> @{typ "prop"}) |
|
133 $ mk_prop_of_term assumption $ mk_prop_of_term concl) bounds |
|
134 end |
|
135 else |
|
136 st |
|
137 fun find_input_steps_and_inline [] last_step = ([], last_step) |
|
138 | find_input_steps_and_inline (VeriT_Node {id = id', rule, prems, concl, bounds} :: steps) |
|
139 last_step = |
|
140 if rule = veriT_input_rule then |
|
141 find_input_steps_and_inline (map (inline_assumption concl id') steps) last_step |
|
142 else |
|
143 apfst (cons (mk_node (id_of_father_step ^ id') rule prems concl bounds)) |
|
144 (find_input_steps_and_inline steps (id_of_father_step ^ id')) |
|
145 val (subproof', last_step_id) = find_input_steps_and_inline subproof "" |
|
146 val prems' = |
|
147 if last_step_id = "" then prems |
|
148 else |
|
149 (case prems of |
|
150 NONE => SOME [last_step_id] |
|
151 | SOME l => SOME (last_step_id :: l)) |
|
152 in |
|
153 (subproof', (((((id_of_father_step, rule), prems'), step_concl), bounds), cx)) |
|
154 end |
|
155 |
|
156 (* |
|
157 (set id rule :clauses(...) :args(..) :conclusion (...)). |
|
158 or |
|
159 (set id subproof (set ...) :conclusion (...)). |
|
160 *) |
|
161 |
|
162 fun parse_proof_step cx = |
|
163 let |
|
164 fun rotate_pair (a, (b, c)) = ((a, b), c) |
|
165 fun get_id (SMTLIB2.S [SMTLIB2.Sym "set", SMTLIB2.Sym id, SMTLIB2.S l]) = (id, l) |
|
166 | get_id t = raise Fail ("unrecognized VeriT Proof" ^ PolyML.makestring t) |
|
167 fun parse_rule (SMTLIB2.Sym rule :: l) = (rule, l) |
|
168 fun parse_source (SMTLIB2.Key "clauses" :: SMTLIB2.S source ::l) = |
|
169 (SOME (map (fn (SMTLIB2.Sym id) => id) source), l) |
|
170 | parse_source l = (NONE, l) |
|
171 fun parse_subproof cx id_of_father_step ((subproof_step as SMTLIB2.S (SMTLIB2.Sym "set" :: _)) :: l) = |
|
172 let val (subproof_steps, cx') = parse_proof_step cx subproof_step in |
|
173 apfst (apfst (curry (op @) subproof_steps)) (parse_subproof cx' id_of_father_step l) |
|
174 end |
|
175 | parse_subproof cx _ l = (([], cx), l) |
|
176 fun skip_args (SMTLIB2.Key "args" :: SMTLIB2.S _ :: l) = l |
|
177 | skip_args l = l |
|
178 fun parse_conclusion (SMTLIB2.Key "conclusion" :: SMTLIB2.S concl :: []) = concl |
|
179 fun make_or_from_clausification l = |
|
180 foldl1 (fn ((concl1, bounds1), (concl2, bounds2)) => |
|
181 (HOLogic.mk_disj (perhaps (try HOLogic.dest_Trueprop) concl1, |
|
182 perhaps (try HOLogic.dest_Trueprop) concl2), bounds1 @ bounds2)) l |
|
183 fun to_node (((((id, rule), prems), concl), bounds), cx) = (mk_node id rule |
|
184 (the_default [] prems) concl bounds, cx) |
|
185 in |
|
186 get_id |
|
187 ##> parse_rule |
|
188 #> rotate_pair |
|
189 ##> parse_source |
|
190 #> rotate_pair |
|
191 ##> skip_args |
|
192 #> (fn (((id, rule), prems), sub) => (((id, rule), prems), parse_subproof cx id sub)) |
|
193 #> rotate_pair |
|
194 ##> parse_conclusion |
|
195 ##> map repair_quantification |
|
196 #> (fn ((((id, rule), prems), (subproof, cx)), terms) => |
|
197 (((((id, rule), prems), subproof), fold_map (fn t => fn cx => node_of t cx) terms cx))) |
|
198 ##> apfst (fn [] => (@{const False}, []) | concls => make_or_from_clausification concls) |
|
199 #> fix_subproof_steps |
|
200 ##> to_node |
|
201 #> (fn (subproof, (step, cx)) => (subproof @ [step], cx)) |
|
202 #-> fold_map update_step_and_cx |
|
203 end |
|
204 |
|
205 (*subproofs are written on multiple lines: SMTLIB can not parse then, because parentheses are |
|
206 unbalanced on each line*) |
|
207 fun seperate_into_steps lines = |
|
208 let |
|
209 fun count ("(" :: l) n = count l (n+1) |
|
210 | count (")" :: l) n = count l (n-1) |
|
211 | count (_ :: l) n = count l n |
|
212 | count [] n = n |
|
213 fun seperate (line :: l) actual_lines m = |
|
214 let val n = count (raw_explode line) 0 in |
|
215 if m + n = 0 then |
|
216 [actual_lines ^ line] :: seperate l "" 0 |
|
217 else seperate l (actual_lines ^ line) (m + n) |
|
218 end |
|
219 | seperate [] _ 0 = [] |
|
220 in |
|
221 seperate lines "" 0 |
|
222 end |
|
223 |
|
224 (* VeriT adds @ before every variable. *) |
|
225 fun remove_all_at (SMTLIB2.Sym v :: l) = SMTLIB2.Sym (perhaps (try (unprefix "@")) v) :: remove_all_at l |
|
226 | remove_all_at (SMTLIB2.S l :: l') = SMTLIB2.S (remove_all_at l) :: remove_all_at l' |
|
227 | remove_all_at (SMTLIB2.Key v :: l) = SMTLIB2.Key v :: remove_all_at l |
|
228 | remove_all_at (v :: l) = v :: remove_all_at l |
|
229 | remove_all_at [] = [] |
|
230 |
|
231 fun find_in_which_step_defined var (VeriT_Node {id, bounds, ...} :: l) = |
|
232 (case List.find (fn v => String.isPrefix v var) bounds of |
|
233 NONE => find_in_which_step_defined var l |
|
234 | SOME _ => id) |
|
235 | find_in_which_step_defined var _ = raise Fail ("undefined " ^ var) |
|
236 |
|
237 (*Yes every case is possible: the introduced var is not on a special size of the equality sign.*) |
|
238 fun find_ite_var_in_term (Const ("HOL.If", _) $ _ $ |
|
239 (Const (@{const_name "HOL.eq"}, _) $ Free (var1, _) $ Free (var2, _) ) $ |
|
240 (Const (@{const_name "HOL.eq"}, _) $ Free (var3, _) $ Free (var4, _) )) = |
|
241 let |
|
242 fun get_number_of_ite_transformed_var var = |
|
243 perhaps (try (unprefix "ite")) var |
|
244 |> Int.fromString |
|
245 fun is_equal_and_has_correct_substring var var' var'' = |
|
246 if var = var' andalso String.isPrefix "ite" var then SOME var' |
|
247 else if var = var'' andalso String.isPrefix "ite" var then SOME var'' else NONE |
|
248 val var1_introduced_var = is_equal_and_has_correct_substring var1 var3 var4 |
|
249 val var2_introduced_var = is_equal_and_has_correct_substring var3 var1 var2 |
|
250 in |
|
251 (case (var1_introduced_var, var2_introduced_var) of |
|
252 (SOME a, SOME b) => |
|
253 (*ill-generated case, might be possible when applying the rule to max a a. Only if the |
|
254 variable have been introduced before. Probably an impossible edge case*) |
|
255 (case (get_number_of_ite_transformed_var a, get_number_of_ite_transformed_var b) of |
|
256 (SOME a, SOME b) => if a < b then var2_introduced_var else var1_introduced_var |
|
257 (*Otherwise, it is a name clase between a parameter name and the introduced variable. |
|
258 Or the name convention has been changed.*) |
|
259 | (NONE, SOME _) => var2_introduced_var |
|
260 | (SOME _, NONE) => var2_introduced_var) |
|
261 | (_, SOME _) => var2_introduced_var |
|
262 | (SOME _, _) => var1_introduced_var) |
|
263 end |
|
264 | find_ite_var_in_term (Const (@{const_name "If"}, _) $ _ $ |
|
265 (Const (@{const_name "HOL.eq"}, _) $ Free (var, _) $ _ ) $ |
|
266 (Const (@{const_name "HOL.eq"}, _) $ Free (var', _) $ _ )) = |
|
267 if var = var' then SOME var else NONE |
|
268 | find_ite_var_in_term (Const (@{const_name "If"}, _) $ _ $ |
|
269 (Const (@{const_name "HOL.eq"}, _) $ _ $ Free (var, _)) $ |
|
270 (Const (@{const_name "HOL.eq"}, _) $ _ $ Free (var', _))) = |
|
271 if var = var' then SOME var else NONE |
|
272 | find_ite_var_in_term (p $ q) = |
|
273 (case find_ite_var_in_term p of |
|
274 NONE => find_ite_var_in_term q |
|
275 | x => x) |
|
276 | find_ite_var_in_term (Abs (_, _, body)) = find_ite_var_in_term body |
|
277 | find_ite_var_in_term _ = NONE |
|
278 |
|
279 fun correct_veriT_step steps (st as VeriT_Node {id, rule, prems, concl, bounds}) = |
|
280 if rule = veriT_tmp_ite_elim_rule then |
|
281 if bounds = [] then |
|
282 (*if the introduced var has already been defined, adding the definition as a dependency*) |
|
283 let |
|
284 val new_prems = |
|
285 (case find_ite_var_in_term concl of |
|
286 NONE => prems |
|
287 | SOME var => find_in_which_step_defined var steps :: prems) |
|
288 in |
|
289 VeriT_Node {id = id, rule = rule, prems = new_prems, concl = concl, bounds = bounds} |
|
290 end |
|
291 else |
|
292 (*some new variables are created*) |
|
293 let |
|
294 val concl' = replace_bound_var_by_free_var concl bounds |
|
295 in |
|
296 mk_node id rule prems concl' [] |
|
297 end |
|
298 else |
|
299 st |
|
300 |
|
301 fun remove_alpha_conversion _ [] = [] |
|
302 | remove_alpha_conversion replace_table (VeriT_Node {id, rule, prems, concl, bounds} :: steps) = |
|
303 let |
|
304 fun correct_dependency prems = |
|
305 map (fn x => perhaps (Symtab.lookup replace_table) x) prems |
|
306 fun find_predecessor prem = perhaps (Symtab.lookup replace_table) prem |
|
307 in |
|
308 if rule = veriT_alpha_conv_rule then |
|
309 remove_alpha_conversion (Symtab.update (id, find_predecessor (hd prems)) |
|
310 replace_table) steps |
|
311 else |
|
312 VeriT_Node {id = id, rule = rule, prems = correct_dependency prems, |
|
313 concl = concl, bounds = bounds} :: remove_alpha_conversion replace_table steps |
|
314 end |
|
315 |
|
316 fun correct_veriT_steps steps = |
|
317 steps |
|
318 |> map (correct_veriT_step steps) |
|
319 |> remove_alpha_conversion Symtab.empty |
|
320 |
|
321 fun parse typs funs lines ctxt = |
|
322 let |
|
323 val smtlib2_lines_without_at = |
|
324 remove_all_at (map SMTLIB2.parse (seperate_into_steps lines)) |
|
325 val (u, env) = apfst flat (fold_map (fn l => fn cx => parse_proof_step cx l) |
|
326 smtlib2_lines_without_at (empty_context ctxt typs funs)) |
|
327 val t = correct_veriT_steps u |
|
328 fun node_to_step (VeriT_Node {id, rule, prems, concl, bounds, ...}) = |
|
329 mk_step id rule prems concl bounds |
|
330 in |
|
331 (map node_to_step t, ctxt_of env) |
|
332 end |
|
333 |
|
334 end; |
|