77 SMTLIB2.S (SMTLIB2.Sym "exists" :: SMTLIB2.S quantified_vars :: t :: []) |
79 SMTLIB2.S (SMTLIB2.Sym "exists" :: SMTLIB2.S quantified_vars :: t :: []) |
78 end |
80 end |
79 | fix_quantification (SMTLIB2.S l) = SMTLIB2.S (map fix_quantification l) |
81 | fix_quantification (SMTLIB2.S l) = SMTLIB2.S (map fix_quantification l) |
80 | fix_quantification x = x |
82 | fix_quantification x = x |
81 |
83 |
82 fun parse_proof cx = |
84 fun replace_bound_var_by_free_var (q $ Abs (var, ty, u)) free_var replaced n = |
|
85 (case List.find (fn v => String.isPrefix v var) free_var of |
|
86 NONE => q $ Abs (var, ty, replace_bound_var_by_free_var u free_var replaced (n+1)) |
|
87 | SOME _ => |
|
88 replace_bound_var_by_free_var u free_var ((n, Free (var ^ veriT_var_suffix, ty)) :: replaced) |
|
89 (n+1)) |
|
90 | replace_bound_var_by_free_var (Bound n) _ replaced_vars _ = |
|
91 (case List.find (curry (op =) n o fst) replaced_vars of |
|
92 NONE => Bound n |
|
93 | SOME (_, var) => var) |
|
94 | replace_bound_var_by_free_var (u $ v) free_vars replaced n = |
|
95 replace_bound_var_by_free_var u free_vars replaced n $ |
|
96 replace_bound_var_by_free_var v free_vars replaced n |
|
97 | replace_bound_var_by_free_var u _ _ _ = u |
|
98 |
|
99 fun find_type_in_formula (Abs(v, ty, u)) var_name = |
|
100 if var_name = v then SOME ty else find_type_in_formula u var_name |
|
101 | find_type_in_formula (u $ v) var_name = |
|
102 (case find_type_in_formula u var_name of |
|
103 NONE => find_type_in_formula v var_name |
|
104 | a => a) |
|
105 | find_type_in_formula _ _ = NONE |
|
106 |
|
107 |
|
108 fun update_ctxt cx bounds concl = |
|
109 fold_index (fn (_, a) => fn b => update_binding a b) |
|
110 (map (fn s => ((s, Term (Free (s ^ "__" ^ veriT_var_suffix, |
|
111 the_default dummyT (find_type_in_formula concl s)))))) bounds) cx |
|
112 |
|
113 fun update_step cx (st as VeriT_Node {id, rule, prems, concl, bounds}) = |
|
114 if rule = veriT_proof_ite_elim_rule then |
|
115 (mk_node id rule prems concl bounds, update_ctxt cx bounds concl) |
|
116 else if rule = veriT_tmp_skolemize then |
|
117 let |
|
118 val concl' = replace_bound_var_by_free_var concl bounds [] 0 |
|
119 in |
|
120 (mk_node id rule prems concl' [], update_ctxt cx bounds concl) |
|
121 end |
|
122 else |
|
123 (st, cx) |
|
124 |
|
125 fun fix_subproof_steps number_of_steps ((((id, rule), prems), subproof), ((step_concl, bounds), |
|
126 cx)) = |
|
127 let |
|
128 fun inline_assumption assumption assumption_id (st as VeriT_Node {id, rule, prems, concl, |
|
129 bounds}) = |
|
130 if List.find (curry (op =) assumption_id) prems <> NONE then |
|
131 mk_node (id + number_of_steps) rule (filter_out (curry (op =) assumption_id) prems) |
|
132 ((Const ("Pure.imp", @{typ "prop => prop => prop"}) $ assumption) $ concl) |
|
133 bounds |
|
134 else |
|
135 st |
|
136 fun inline_assumption_in_conclusion concl (VeriT_Node {rule, concl = assumption,...} :: l) = |
|
137 if rule = veriT_input_rule then |
|
138 inline_assumption_in_conclusion |
|
139 (Const (@{const_name Pure.imp}, @{typ "prop => prop => prop"}) $ assumption $ concl) l |
|
140 else |
|
141 inline_assumption_in_conclusion concl l |
|
142 | inline_assumption_in_conclusion concl [] = concl |
|
143 fun find_assumption_and_inline (VeriT_Node {id, rule, prems, concl, bounds} :: l) = |
|
144 if rule = veriT_input_rule then |
|
145 map (inline_assumption step_concl (veriT_step_prefix ^ string_of_int id)) l |
|
146 else |
|
147 (mk_node (id + number_of_steps) rule prems concl bounds) :: find_assumption_and_inline l |
|
148 | find_assumption_and_inline [] = [] |
|
149 in |
|
150 (find_assumption_and_inline subproof, |
|
151 (((((id, rule), prems), inline_assumption_in_conclusion step_concl subproof), bounds), cx)) |
|
152 end |
|
153 |
|
154 (* |
|
155 (set id rule :clauses(...) :args(..) :conclusion (...)). |
|
156 or |
|
157 (set id subproof (set ...) :conclusion (...)). |
|
158 *) |
|
159 |
|
160 fun parse_proof_step number_of_steps cx = |
83 let |
161 let |
84 fun rotate_pair (a, (b, c)) = ((a, b), c) |
162 fun rotate_pair (a, (b, c)) = ((a, b), c) |
85 fun get_id (SMTLIB2.S [SMTLIB2.Sym "set", SMTLIB2.Sym id, SMTLIB2.S l]) = (id, l) |
163 fun get_id (SMTLIB2.S [SMTLIB2.Sym "set", SMTLIB2.Sym id, SMTLIB2.S l]) = (id, l) |
86 | get_id t = raise Fail ("unrecognized VeriT Proof" ^ PolyML.makestring t) |
164 | get_id t = raise Fail ("unrecognized VeriT Proof" ^ PolyML.makestring t) |
87 fun change_id_to_number x = (unprefix verit_step_prefix #> Int.fromString #> the) x |
165 fun change_id_to_number x = (unprefix veriT_step_prefix #> Int.fromString #> the) x |
88 fun parse_rule (SMTLIB2.Sym rule :: l) = (rule, l) |
166 fun parse_rule (SMTLIB2.Sym rule :: l) = (rule, l) |
89 fun parse_source (SMTLIB2.Key "clauses" :: SMTLIB2.S source ::l) = |
167 fun parse_source (SMTLIB2.Key "clauses" :: SMTLIB2.S source ::l) = |
90 (SOME (map (fn (SMTLIB2.Sym id) => id) source), l) |
168 (SOME (map (fn (SMTLIB2.Sym id) => id) source), l) |
91 | parse_source l = (NONE, l) |
169 | parse_source l = (NONE, l) |
|
170 fun parse_subproof cx ((subproof_step as SMTLIB2.S (SMTLIB2.Sym "set" :: _)) :: l) = |
|
171 let val (step, cx') = parse_proof_step number_of_steps cx subproof_step in |
|
172 apfst (apfst (cons step)) (parse_subproof cx' l) |
|
173 end |
|
174 | parse_subproof cx l = (([], cx), l) |
|
175 |
92 fun skip_args (SMTLIB2.Key "args" :: SMTLIB2.S _ :: l) = l |
176 fun skip_args (SMTLIB2.Key "args" :: SMTLIB2.S _ :: l) = l |
93 | skip_args l = l |
177 | skip_args l = l |
94 |
178 |
95 fun parse_conclusion [SMTLIB2.Key "conclusion", SMTLIB2.S concl] = concl |
179 fun parse_conclusion (SMTLIB2.Key "conclusion" :: SMTLIB2.S concl :: []) = concl |
96 |
180 |
97 fun make_or_from_clausification l = |
181 fun make_or_from_clausification l = |
98 foldl1 (fn ((concl1, bounds1), (concl2, bounds2)) => (HOLogic.mk_disj (concl1, concl2), |
182 foldl1 (fn ((concl1, bounds1), (concl2, bounds2)) => (HOLogic.mk_disj (concl1, concl2), |
99 bounds1 @ bounds2)) l |
183 bounds1 @ bounds2)) l |
100 (*the conclusion is empty, ie no false*) |
184 fun to_node (((((id, rule), prems), concl), bounds), cx) = (mk_node id rule |
101 fun to_node ((((id, rule), prems), ([], cx))) = (mk_node id rule (the_default [] prems) |
185 (the_default [] prems) concl bounds, cx) |
102 @{const False} [], cx) |
|
103 | to_node ((((id, rule), prems), (concls, cx))) = |
|
104 let val (concl, bounds) = make_or_from_clausification concls in |
|
105 (mk_node id rule (the_default [] prems) concl bounds, cx) end |
|
106 in |
186 in |
107 get_id |
187 get_id |
108 #>> change_id_to_number |
188 #>> change_id_to_number |
109 ##> parse_rule |
189 ##> parse_rule |
110 #> rotate_pair |
190 #> rotate_pair |
111 ##> parse_source |
191 ##> parse_source |
112 #> rotate_pair |
192 #> rotate_pair |
113 ##> skip_args |
193 ##> skip_args |
|
194 ##> parse_subproof cx |
|
195 #> rotate_pair |
114 ##> parse_conclusion |
196 ##> parse_conclusion |
115 ##> map fix_quantification |
197 ##> map fix_quantification |
116 ##> (fn terms => fold_map (fn t => fn cx => node_of t cx) terms cx) |
198 #> (fn ((((id, rule), prems), (subproof, cx)), terms) => |
117 ##> apfst (map (fn (VeriT_Node {concl, bounds,...}) => (concl, bounds))) |
199 (((((id, rule), prems), subproof), fold_map (fn t => fn cx => node_of t cx) terms cx))) |
118 #> to_node |
200 ##> apfst ((map (fn (VeriT_Node {concl, bounds,...}) => (concl, bounds)))) |
119 end |
201 (*the conclusion is the empty list, ie no false is written, we have to add it.*) |
|
202 ##> (apfst (fn [] => (@{const False}, []) |
|
203 | concls => make_or_from_clausification concls)) |
|
204 #> fix_subproof_steps number_of_steps |
|
205 ##> to_node |
|
206 #> (fn (subproof, (step, cx)) => (subproof @ [step], cx)) |
|
207 #> (fn (steps, cx) => update_step cx (List.last steps)) |
|
208 end |
|
209 |
|
210 fun seperate_into_lines_and_subproof lines = |
|
211 let |
|
212 fun count ("(" :: l) n = count l (n+1) |
|
213 | count (")" :: l) n = count l (n-1) |
|
214 | count (_ :: l) n = count l n |
|
215 | count [] n = n |
|
216 fun seperate (line :: l) actual_lines m = |
|
217 let val n = count (raw_explode line) 0 in |
|
218 if m + n = 0 then |
|
219 [actual_lines ^ line] :: seperate l "" 0 |
|
220 else seperate l (actual_lines ^ line) (m + n) |
|
221 end |
|
222 | seperate [] _ 0 = [] |
|
223 in |
|
224 seperate lines "" 0 |
|
225 end |
|
226 |
|
227 (*VeriT adds @ before every variable.*) |
|
228 fun remove_all_at (SMTLIB2.Sym v :: l) = |
|
229 SMTLIB2.Sym (if nth_string v 0 = "@" then String.extract (v, 1, NONE) else v) :: remove_all_at l |
|
230 | remove_all_at (SMTLIB2.S l :: l') = SMTLIB2.S (remove_all_at l) :: remove_all_at l' |
|
231 | remove_all_at (SMTLIB2.Key v :: l) = SMTLIB2.Key v :: remove_all_at l |
|
232 | remove_all_at (v :: l) = v :: remove_all_at l |
|
233 | remove_all_at [] = [] |
|
234 |
|
235 fun replace_all_by_exist (Const (@{const_name Pure.all}, ty) $ Abs (var, ty', u)) bounds = |
|
236 (case List.find (fn v => String.isPrefix v var) bounds of |
|
237 NONE => (Const (@{const_name Pure.all}, ty) $ Abs (var, ty', replace_all_by_exist u bounds)) |
|
238 | SOME _ => Const (@{const_name HOL.Ex}, (ty' --> @{typ bool}) --> @{typ bool}) $ |
|
239 Abs (var ^ veriT_var_suffix, ty', replace_all_by_exist u bounds)) |
|
240 | replace_all_by_exist (@{term "Trueprop"} $ g) bounds = replace_all_by_exist g bounds |
|
241 | replace_all_by_exist (f $ g) bounds = |
|
242 replace_all_by_exist f bounds $ replace_all_by_exist g bounds |
|
243 | replace_all_by_exist (Abs (var, ty, u)) bounds = Abs (var, ty, replace_all_by_exist u bounds) |
|
244 | replace_all_by_exist f _ = f |
|
245 |
|
246 |
|
247 fun correct_veriT_steps num_of_steps (st as VeriT_Node {id = id, rule = rule, prems = prems, |
|
248 concl = concl, bounds = bounds}) = |
|
249 if rule = "tmp_ite_elim" then |
|
250 let |
|
251 val concl' = replace_bound_var_by_free_var concl bounds [] 0 |
|
252 in |
|
253 [mk_node (num_of_steps + id) rule prems (@{term "Trueprop"} $ |
|
254 replace_all_by_exist concl bounds) [], |
|
255 mk_node id veriT_tmp_skolemize (veriT_step_prefix ^ (string_of_int (num_of_steps + id)) :: |
|
256 []) concl' []] |
|
257 end |
|
258 else |
|
259 [st] |
|
260 |
120 |
261 |
121 |
262 |
122 (* overall proof parser *) |
263 (* overall proof parser *) |
123 fun parse typs funs lines ctxt = |
264 fun parse typs funs lines ctxt = |
124 let |
265 let |
|
266 val smtlib2_lines_without_at = |
|
267 remove_all_at (map SMTLIB2.parse (seperate_into_lines_and_subproof lines)) |
125 val (u, env) = |
268 val (u, env) = |
126 fold_map (fn l => fn cx => parse_proof cx l) (map (fn f => SMTLIB2.parse [f]) lines) |
269 fold_map (fn l => fn cx => parse_proof_step (length lines) cx l) smtlib2_lines_without_at |
127 (empty_context ctxt typs funs) |
270 (empty_context ctxt typs funs) |
128 val t = |
271 val t = map (correct_veriT_steps (1 + length u)) u |> flat |
129 map (fn (VeriT_Node {id, rule, prems, concl, bounds, ...}) => |
272 fun node_to_step (VeriT_Node {id, rule, prems, concl, bounds, ...}) = |
130 mk_step id rule prems concl bounds) u |
273 mk_step id rule prems concl bounds |
131 in |
274 in |
132 (t, ctxt_of env) |
275 (map node_to_step t, ctxt_of env) |
133 end |
276 end |
134 |
277 |
135 end; |
278 end; |