1(* Title: HOL/Tools/SMT/verit_proof.ML 2 Author: Mathias Fleury, ENS Rennes 3 Author: Sascha Boehme, TU Muenchen 4 5VeriT proofs: parsing and abstract syntax tree. 6*) 7 8signature VERIT_PROOF = 9sig 10 (*proofs*) 11 datatype veriT_step = VeriT_Step of { 12 id: string, 13 rule: string, 14 prems: string list, 15 proof_ctxt: term list, 16 concl: term, 17 fixes: string list} 18 19 datatype veriT_replay_node = VeriT_Replay_Node of { 20 id: string, 21 rule: string, 22 args: term list, 23 prems: string list, 24 proof_ctxt: term list, 25 concl: term, 26 bounds: (string * typ) list, 27 subproof: (string * typ) list * term list * veriT_replay_node list} 28 29 (*proof parser*) 30 val parse: typ Symtab.table -> term Symtab.table -> string list -> 31 Proof.context -> veriT_step list * Proof.context 32 val parse_replay: typ Symtab.table -> term Symtab.table -> string list -> 33 Proof.context -> veriT_replay_node list * Proof.context 34 35 val map_replay_prems: (string list -> string list) -> veriT_replay_node -> veriT_replay_node 36 val veriT_step_prefix : string 37 val veriT_input_rule: string 38 val veriT_normalized_input_rule: string 39 val veriT_la_generic_rule : string 40 val veriT_rewrite_rule : string 41 val veriT_simp_arith_rule : string 42 val veriT_tmp_skolemize_rule : string 43 val veriT_subproof_rule : string 44 val veriT_local_input_rule : string 45end; 46 47structure VeriT_Proof: VERIT_PROOF = 48struct 49 50open SMTLIB_Proof 51 52datatype raw_veriT_node = Raw_VeriT_Node of { 53 id: string, 54 rule: string, 55 args: SMTLIB.tree, 56 prems: string list, 57 concl: SMTLIB.tree, 58 subproof: raw_veriT_node list} 59 60fun mk_raw_node id rule args prems concl subproof = 61 Raw_VeriT_Node {id = id, rule = rule, args = args, prems = prems, concl = concl, 62 subproof = subproof} 63 64datatype veriT_node = VeriT_Node of { 65 id: string, 66 rule: string, 67 prems: string list, 68 proof_ctxt: term list, 69 concl: term, 70 bounds: string list} 71 72fun mk_node id rule prems proof_ctxt concl bounds = 73 VeriT_Node {id = id, rule = rule, prems = prems, proof_ctxt = proof_ctxt, concl = concl, 74 bounds = bounds} 75 76datatype veriT_replay_node = VeriT_Replay_Node of { 77 id: string, 78 rule: string, 79 args: term list, 80 prems: string list, 81 proof_ctxt: term list, 82 concl: term, 83 bounds: (string * typ) list, 84 subproof: (string * typ) list * term list * veriT_replay_node list} 85 86fun mk_replay_node id rule args prems proof_ctxt concl bounds subproof = 87 VeriT_Replay_Node {id = id, rule = rule, args = args, prems = prems, proof_ctxt = proof_ctxt, 88 concl = concl, bounds = bounds, subproof = subproof} 89 90datatype veriT_step = VeriT_Step of { 91 id: string, 92 rule: string, 93 prems: string list, 94 proof_ctxt: term list, 95 concl: term, 96 fixes: string list} 97 98fun mk_step id rule prems proof_ctxt concl fixes = 99 VeriT_Step {id = id, rule = rule, prems = prems, proof_ctxt = proof_ctxt, concl = concl, 100 fixes = fixes} 101 102val veriT_step_prefix = ".c" 103val veriT_input_rule = "input" 104val veriT_la_generic_rule = "la_generic" 105val veriT_normalized_input_rule = "__normalized_input" (* arbitrary *) 106val veriT_rewrite_rule = "__rewrite" (* arbitrary *) 107val veriT_subproof_rule = "subproof" 108val veriT_local_input_rule = "__local_input" (* arbitrary *) 109val veriT_simp_arith_rule = "simp_arith" 110 111(* Even the veriT developer do not know if the following rule can still appear in proofs: *) 112val veriT_tmp_skolemize_rule = "tmp_skolemize" 113 114(* proof parser *) 115 116fun node_of p cx = 117 ([], cx) 118 ||>> `(with_fresh_names (term_of p)) 119 |>> snd 120 121fun find_type_in_formula (Abs (v, T, u)) var_name = 122 if String.isPrefix var_name v then SOME T else find_type_in_formula u var_name 123 | find_type_in_formula (u $ v) var_name = 124 (case find_type_in_formula u var_name of 125 NONE => find_type_in_formula v var_name 126 | some_T => some_T) 127 | find_type_in_formula (Free(v, T)) var_name = 128 if String.isPrefix var_name v then SOME T else NONE 129 | find_type_in_formula _ _ = NONE 130 131fun find_type_of_free_in_formula (Free (v, T) $ u) var_name = 132 if String.isPrefix var_name v then SOME T else find_type_in_formula u var_name 133 | find_type_of_free_in_formula (Abs (v, T, u)) var_name = 134 if String.isPrefix var_name v then SOME T else find_type_in_formula u var_name 135 | find_type_of_free_in_formula (u $ v) var_name = 136 (case find_type_in_formula u var_name of 137 NONE => find_type_in_formula v var_name 138 | some_T => some_T) 139 | find_type_of_free_in_formula _ _ = NONE 140 141fun add_bound_variables_to_ctxt concl = 142 fold (update_binding o 143 (fn s => (s, Term (Free (s, the_default dummyT (find_type_in_formula concl s)))))) 144 145 146local 147 148 fun remove_Sym (SMTLIB.Sym y) = y 149 150 fun extract_symbols bds = 151 bds 152 |> map (fn SMTLIB.S [SMTLIB.Key _, SMTLIB.Sym x, SMTLIB.Sym y] => [x, y] 153 | SMTLIB.S syms => map remove_Sym syms) 154 |> flat 155 156 fun extract_symbols_map bds = 157 bds 158 |> map (fn SMTLIB.S [SMTLIB.Key _, SMTLIB.Sym x, _] => [x] 159 | SMTLIB.S syms => map remove_Sym syms) 160 |> flat 161in 162 163fun bound_vars_by_rule "bind" (SMTLIB.S bds) = extract_symbols bds 164 | bound_vars_by_rule "qnt_simplify" (SMTLIB.S bds) = extract_symbols_map bds 165 | bound_vars_by_rule "sko_forall" (SMTLIB.S bds) = extract_symbols_map bds 166 | bound_vars_by_rule "sko_ex" (SMTLIB.S bds) = extract_symbols_map bds 167 | bound_vars_by_rule _ _ = [] 168 169fun global_bound_vars_by_rule _ _ = [] 170 171(* VeriT adds "?" before some variable. *) 172fun remove_all_qm (SMTLIB.Sym v :: l) = 173 SMTLIB.Sym (perhaps (try (unprefix "?")) v) :: remove_all_qm l 174 | remove_all_qm (SMTLIB.S l :: l') = SMTLIB.S (remove_all_qm l) :: remove_all_qm l' 175 | remove_all_qm (SMTLIB.Key v :: l) = SMTLIB.Key v :: remove_all_qm l 176 | remove_all_qm (v :: l) = v :: remove_all_qm l 177 | remove_all_qm [] = [] 178 179fun remove_all_qm2 (SMTLIB.Sym v) = SMTLIB.Sym (perhaps (try (unprefix "?")) v) 180 | remove_all_qm2 (SMTLIB.S l) = SMTLIB.S (remove_all_qm l) 181 | remove_all_qm2 (SMTLIB.Key v) = SMTLIB.Key v 182 | remove_all_qm2 v = v 183 184val parse_rule_and_args = 185 let 186 fun parse_rule_name (SMTLIB.Sym rule :: l) = (rule, l) 187 | parse_rule_name l = (veriT_subproof_rule, l) 188 fun parse_args (SMTLIB.Key "args" :: args :: l) = (remove_all_qm2 args, l) 189 | parse_args l = (SMTLIB.S [], l) 190 in 191 parse_rule_name 192 ##> parse_args 193 end 194 195end 196 197fun parse_raw_proof_step (p : SMTLIB.tree) : raw_veriT_node = 198 let 199 fun rotate_pair (a, (b, c)) = ((a, b), c) 200 fun get_id (SMTLIB.S [SMTLIB.Sym "set", SMTLIB.Sym id, SMTLIB.S l]) = (id, l) 201 | get_id t = raise Fail ("unrecognized VeriT proof " ^ \<^make_string> t) 202 fun parse_source (SMTLIB.Key "clauses" :: SMTLIB.S source ::l) = 203 (SOME (map (fn (SMTLIB.Sym id) => id) source), l) 204 | parse_source l = (NONE, l) 205 fun parse_subproof rule args id_of_father_step ((subproof_step as SMTLIB.S (SMTLIB.Sym "set" :: _)) :: l) = 206 let 207 val subproof_steps = parse_raw_proof_step subproof_step 208 in 209 apfst (curry (op ::) subproof_steps) (parse_subproof rule args id_of_father_step l) 210 end 211 | parse_subproof _ _ _ l = ([], l) 212 213 fun parse_and_clausify_conclusion (SMTLIB.Key "conclusion" :: SMTLIB.S [] :: []) = 214 SMTLIB.Sym "false" 215 | parse_and_clausify_conclusion (SMTLIB.Key "conclusion" :: SMTLIB.S concl :: []) = 216 (SMTLIB.S (remove_all_qm (SMTLIB.Sym "or" :: concl))) 217 218 fun to_raw_node ((((((id, rule), args), prems), subproof), concl)) = 219 (mk_raw_node id rule args (the_default [] prems) concl subproof) 220 in 221 (get_id 222 ##> parse_rule_and_args 223 #> rotate_pair 224 #> rotate_pair 225 ##> parse_source 226 #> rotate_pair 227 #> (fn ((((id, rule), args), prems), sub) => 228 ((((id, rule), args), prems), parse_subproof rule args id sub)) 229 #> rotate_pair 230 ##> parse_and_clausify_conclusion 231 #> to_raw_node) 232 p 233 end 234 235fun proof_ctxt_of_rule "bind" t = t 236 | proof_ctxt_of_rule "sko_forall" t = t 237 | proof_ctxt_of_rule "sko_ex" t = t 238 | proof_ctxt_of_rule "let" t = t 239 | proof_ctxt_of_rule "qnt_simplify" t = t 240 | proof_ctxt_of_rule _ _ = [] 241 242fun args_of_rule "forall_inst" t = t 243 | args_of_rule _ _ = [] 244 245fun map_replay_prems f (VeriT_Replay_Node {id, rule, args, prems, proof_ctxt, concl, bounds, 246 subproof = (bound, assms, subproof)}) = 247 (VeriT_Replay_Node {id = id, rule = rule, args = args, prems = f prems, proof_ctxt = proof_ctxt, 248 concl = concl, bounds = bounds, subproof = (bound, assms, map (map_replay_prems f) subproof)}) 249 250fun map_replay_id f (VeriT_Replay_Node {id, rule, args, prems, proof_ctxt, concl, bounds, 251 subproof = (bound, assms, subproof)}) = 252 (VeriT_Replay_Node {id = f id, rule = rule, args = args, prems = prems, proof_ctxt = proof_ctxt, 253 concl = concl, bounds = bounds, subproof = (bound, assms, map (map_replay_id f) subproof)}) 254 255fun id_of_last_step prems = 256 if null prems then [] 257 else 258 let val VeriT_Replay_Node {id, ...} = List.last prems in [id] end 259 260val extract_assumptions_from_subproof = 261 let fun extract_assumptions_from_subproof (VeriT_Replay_Node {rule, concl, ...}) = 262 if rule = veriT_local_input_rule then [concl] else [] 263 in 264 map extract_assumptions_from_subproof 265 #> flat 266 end 267 268fun normalized_rule_name id rule = 269 (case (rule = veriT_input_rule, can (unprefix SMTLIB_Interface.assert_prefix) id) of 270 (true, true) => veriT_normalized_input_rule 271 | (true, _) => veriT_local_input_rule 272 | _ => rule) 273 274fun is_assm_repetition id rule = 275 rule = veriT_input_rule andalso can (unprefix SMTLIB_Interface.assert_prefix) id 276 277fun postprocess_proof ctxt step = 278 let fun postprocess (Raw_VeriT_Node {id = id, rule = rule, args = args, 279 prems = prems, concl = concl, subproof = subproof}) cx = 280 let 281 val ((concl, bounds), cx') = node_of concl cx 282 283 val bound_vars = bound_vars_by_rule rule args 284 285 (* postprocess conclusion *) 286 val new_global_bounds = global_bound_vars_by_rule rule args 287 val concl = SMTLIB_Isar.unskolemize_names ctxt concl 288 289 val _ = (SMT_Config.veriT_msg ctxt) (fn () => \<^print> ("id =", id, "concl =", concl)) 290 val _ = (SMT_Config.veriT_msg ctxt) (fn () => \<^print> ("id =", id, "cx' =", cx', 291 "bound_vars =", bound_vars)) 292 val bound_vars = filter_out (member ((op =)) new_global_bounds) bound_vars 293 val bound_tvars = 294 map (fn s => (s, the (find_type_in_formula concl s))) bound_vars 295 val subproof_cx = add_bound_variables_to_ctxt concl bound_vars cx 296 val (p : veriT_replay_node list list, _) = 297 fold_map postprocess subproof subproof_cx 298 299 (* postprocess assms *) 300 val SMTLIB.S stripped_args = args 301 val sanitized_args = 302 proof_ctxt_of_rule rule stripped_args 303 |> map 304 (fn SMTLIB.S [SMTLIB.Key "=", x, y] => SMTLIB.S [SMTLIB.Sym "=", x, y] 305 | SMTLIB.S syms => 306 SMTLIB.S (SMTLIB.Sym "and" :: map (fn x => SMTLIB.S [SMTLIB.Sym "=", x, x]) syms) 307 | x => x) 308 val (termified_args, _) = fold_map node_of sanitized_args subproof_cx |> apfst (map fst) 309 val normalized_args = map (SMTLIB_Isar.unskolemize_names ctxt) termified_args 310 311 val subproof_assms = proof_ctxt_of_rule rule normalized_args 312 313 (* postprocess arguments *) 314 val rule_args = args_of_rule rule stripped_args 315 val (termified_args, _) = fold_map term_of rule_args subproof_cx 316 val normalized_args = map (SMTLIB_Isar.unskolemize_names ctxt) termified_args 317 val rule_args = normalized_args 318 319 (* fix subproof *) 320 val p = flat p 321 val p = map (map_replay_prems (map (curry (op ^) id))) p 322 val p = map (map_replay_id (curry (op ^) id)) p 323 324 val extra_assms2 = 325 (if rule = veriT_subproof_rule then extract_assumptions_from_subproof p else []) 326 327 (* fix step *) 328 val bound_t = 329 bounds 330 |> map (fn s => (s, the_default dummyT (find_type_of_free_in_formula concl s))) 331 val fixed_prems = 332 (if null subproof then prems else map (curry (op ^) id) prems) @ 333 (if is_assm_repetition id rule then [id] else []) @ 334 id_of_last_step p 335 val normalized_rule = normalized_rule_name id rule 336 val step = mk_replay_node id normalized_rule rule_args fixed_prems subproof_assms concl 337 bound_t (bound_tvars, subproof_assms @ extra_assms2, p) 338 in 339 ([step], cx') 340 end 341 in postprocess step end 342 343 344(*subproofs are written on multiple lines: SMTLIB can not parse then, because parentheses are 345unbalanced on each line*) 346fun seperate_into_steps lines = 347 let 348 fun count ("(" :: l) n = count l (n + 1) 349 | count (")" :: l) n = count l (n - 1) 350 | count (_ :: l) n = count l n 351 | count [] n = n 352 fun seperate (line :: l) actual_lines m = 353 let val n = count (raw_explode line) 0 in 354 if m + n = 0 then 355 [actual_lines ^ line] :: seperate l "" 0 356 else 357 seperate l (actual_lines ^ line) (m + n) 358 end 359 | seperate [] _ 0 = [] 360 in 361 seperate lines "" 0 362 end 363 364fun unprefix_all_syms c (SMTLIB.Sym v :: l) = 365 SMTLIB.Sym (perhaps (try (unprefix c)) v) :: unprefix_all_syms c l 366 | unprefix_all_syms c (SMTLIB.S l :: l') = SMTLIB.S (unprefix_all_syms c l) :: unprefix_all_syms c l' 367 | unprefix_all_syms c (SMTLIB.Key v :: l) = SMTLIB.Key v :: unprefix_all_syms c l 368 | unprefix_all_syms c (v :: l) = v :: unprefix_all_syms c l 369 | unprefix_all_syms _ [] = [] 370 371(* VeriT adds "@" before every variable. *) 372val remove_all_ats = unprefix_all_syms "@" 373 374val linearize_proof = 375 let 376 fun linearize (VeriT_Replay_Node {id = id, rule = rule, args = _, prems = prems, 377 proof_ctxt = proof_ctxt, concl = concl, bounds = bounds, subproof = (_, _, subproof)}) = 378 let 379 fun mk_prop_of_term concl = 380 concl |> fastype_of concl = \<^typ>\<open>bool\<close> ? curry (op $) \<^term>\<open>Trueprop\<close> 381 fun remove_assumption_id assumption_id prems = 382 filter_out (curry (op =) assumption_id) prems 383 fun inline_assumption assumption assumption_id 384 (VeriT_Node {id, rule, prems, proof_ctxt, concl, bounds}) = 385 mk_node id rule (remove_assumption_id assumption_id prems) proof_ctxt 386 (\<^const>\<open>Pure.imp\<close> $ mk_prop_of_term assumption $ mk_prop_of_term concl) bounds 387 fun find_input_steps_and_inline [] = [] 388 | find_input_steps_and_inline 389 (VeriT_Node {id = id', rule, prems, concl, bounds, ...} :: steps) = 390 if rule = veriT_input_rule then 391 find_input_steps_and_inline (map (inline_assumption concl id') steps) 392 else 393 mk_node (id') rule prems [] concl bounds :: find_input_steps_and_inline steps 394 395 val subproof = flat (map linearize subproof) 396 val subproof' = find_input_steps_and_inline subproof 397 in 398 subproof' @ [mk_node id rule prems proof_ctxt concl (map fst bounds)] 399 end 400 in linearize end 401 402local 403 fun import_proof_and_post_process typs funs lines ctxt = 404 let 405 val smtlib_lines_without_at = 406 seperate_into_steps lines 407 |> map SMTLIB.parse 408 |> remove_all_ats 409 in apfst flat (fold_map (fn l => postprocess_proof ctxt (parse_raw_proof_step l)) 410 smtlib_lines_without_at (empty_context ctxt typs funs)) end 411in 412 413fun parse typs funs lines ctxt = 414 let 415 val (u, env) = import_proof_and_post_process typs funs lines ctxt 416 val t = flat (map linearize_proof u) 417 fun node_to_step (VeriT_Node {id, rule, prems, concl, bounds, ...}) = 418 mk_step id rule prems [] concl bounds 419 in 420 (map node_to_step t, ctxt_of env) 421 end 422 423fun parse_replay typs funs lines ctxt = 424 let 425 val (u, env) = import_proof_and_post_process typs funs lines ctxt 426 val _ = (SMT_Config.veriT_msg ctxt) (fn () => \<^print> u) 427 in 428 (u, ctxt_of env) 429 end 430end 431 432end; 433