1(* ===================================================================== *) 2(* FILE : hhReconstruct.sml *) 3(* DESCRIPTION : Reconstruct a proof from the lemmas given by an ATP *) 4(* and minimize them. *) 5(* AUTHOR : (c) Thibault Gauthier, University of Innsbruck *) 6(* DATE : 2015 *) 7(* ===================================================================== *) 8 9structure hhReconstruct :> hhReconstruct = 10struct 11 12open HolKernel boolLib Dep Tag tttTools tttExec hhWriter 13 14val ERR = mk_HOL_ERR "hhReconstruct" 15 16(*---------------------------------------------------------------------------- 17 Settings 18 -----------------------------------------------------------------------------*) 19 20val reconstruct_flag = ref true 21val minimization_timeout = ref 1.0 22val reconstruction_timeout = ref 1.0 23 24(*---------------------------------------------------------------------------- 25 Reading the ATP output 26 -----------------------------------------------------------------------------*) 27 28fun remove_white_spaces s = 29 let fun f c = if Char.isSpace c then "" else Char.toString c in 30 String.translate f s 31 end 32 33fun not_reserved s = String.isPrefix "thm." s 34fun is_dot c = c = #"." 35 36fun read_status atp_status = 37 remove_white_spaces (hd (readl atp_status)) 38 handle Interrupt => raise Interrupt 39 | _ => "Unknown" 40 41fun read_lemmas atp_out = 42 let 43 val l1 = readl atp_out 44 val l2 = map hhTranslate.unescape l1 45 val l3 = filter not_reserved l2 46 fun f s = 47 let 48 val sl1 = String.fields is_dot s 49 val sl2 = tl (butlast sl1) 50 in 51 String.concatWith "." sl2 52 end 53 in 54 mk_fast_set String.compare (map f l3) 55 end 56 57fun get_lemmas (atp_status,atp_out) = 58 if read_status atp_status = "Theorem" 59 then SOME (read_lemmas atp_out) 60 else NONE 61 62(*---------------------------------------------------------------------------- 63 Minimization and pretty-printing 64 -----------------------------------------------------------------------------*) 65 66fun hh_reconstruct lemmas g = 67 if not (!reconstruct_flag) 68 then (print_endline (mk_metis_call lemmas); 69 raise ERR "hh_minimize" "reconstruction off") 70 else 71 let 72 val stac = mk_metis_call lemmas 73 val t1 = !minimization_timeout 74 val t2 = !reconstruction_timeout 75 val newstac = hide_out (tttMinimize.minimize_stac t1 stac g) [] 76 val tac = hide_out tactic_of_sml newstac 77 in 78 case hide_out (app_tac t2 tac) g of 79 SOME _ => (newstac,tac) 80 | NONE => raise ERR "hh_reconstruct" "reconstruction failed" 81 end 82 83end 84