1(* ========================================================================== *) 2(* FILE : tttMinimize.sml *) 3(* DESCRIPTION : Minimize proof script including minimization *) 4(* AUTHOR : (c) Thibault Gauthier, University of Innsbruck *) 5(* DATE : 2017 *) 6(* ========================================================================== *) 7 8structure tttMinimize :> tttMinimize = 9struct 10 11open HolKernel boolLib Abbrev tttTools tttExec tttLexer tttTimeout tttSetup 12 13val ERR = mk_HOL_ERR "tttMinimize" 14 15(* -------------------------------------------------------------------------- 16 Tests 17 -------------------------------------------------------------------------- *) 18 19fun same_effect tim stac1 stac2 g = 20 let 21 val gl1o = rec_stac tim stac1 g 22 val gl2o = rec_stac tim stac2 g 23 in 24 gl1o <> NONE andalso gl2o <> NONE andalso gl1o = gl2o 25 end 26 27fun is_proof stac g = (rec_sproof stac g = SOME []) 28 29fun is_effect tim stac g gl = (rec_stac tim stac g = SOME gl) 30 31(*--------------------------------------------------------------------------- 32 Removing unnecessary parentheses 33 ----------------------------------------------------------------------------*) 34 35fun rm_par sl = case sl of 36 [] => [] 37 | ["(",a,")"] => [a] 38 | ["(","(",a,")",")"] => [a] 39 | "(" :: a :: ")" :: m => a :: rm_par m 40 | "(" :: "(" :: a :: ")" :: ")" :: m => a :: rm_par m 41 | a :: m => a :: rm_par m 42 43(*---------------------------------------------------------------------------- 44 Minimizing the space between parentheses 45 ----------------------------------------------------------------------------*) 46 47fun minspace_sl sl = case sl of 48 [] => "" 49 | [a] => a 50 | a :: b :: m => 51 ( 52 if mem a ["[","("] orelse mem b ["]",")",",",";"] 53 then a ^ minspace_sl (b :: m) 54 else a ^ " " ^ minspace_sl (b :: m) 55 ) 56 57(*---------------------------------------------------------------------------- 58 Remove infix guards 59 ----------------------------------------------------------------------------*) 60 61fun is_infix_open s = 62 String.isPrefix "ttt_infix" s andalso 63 String.isSuffix "open" s 64 65fun is_infix_close s = 66 String.isPrefix "ttt_infix" s andalso 67 String.isSuffix "close" s 68 69fun rm_infix sl = case sl of 70 [] => [] 71 | a :: b :: c :: m => 72 if is_infix_open a andalso is_infix_close c 73 then b :: rm_infix m 74 else a :: rm_infix (b :: c :: m) 75 | a :: m => a :: rm_infix m 76 77(*---------------------------------------------------------------------------- 78 Removing module declaration 79 ----------------------------------------------------------------------------*) 80 81fun rm_prefix sl = 82 let 83 fun rm_one_prefix s = 84 let 85 val l = String.tokens (fn x => x = #".") s 86 val s' = last l 87 in 88 if List.length l = 1 orelse not (is_pointer_eq s s') 89 then s 90 else s' 91 end 92 in 93 map rm_one_prefix sl 94 end 95 96(*---------------------------------------------------------------------------- 97 Remove DB.fetch 98 ----------------------------------------------------------------------------*) 99 100fun rm_dbfetch sl = case sl of 101 [] => [] 102 | ["DB.fetch",a,b] => 103 (( 104 if unquote_string a = current_theory () 105 then ["DB.fetch",a,b] 106 else [unquote_string a ^ "Theory." ^ unquote_string b] 107 ) 108 handle _ => ["DB.fetch",a,b]) 109 | "DB.fetch" :: a :: b :: m => 110 (( 111 if unquote_string a = current_theory () 112 then ["DB.fetch",a,b] 113 else [unquote_string a ^ "Theory." ^ unquote_string b] 114 ) 115 handle _ => ["DB.fetch",a,b]) 116 @ 117 rm_dbfetch m 118 | a :: m => a :: rm_dbfetch m 119 120(*---------------------------------------------------------------------------- 121 Prettification of a string tactic. 122 ----------------------------------------------------------------------------*) 123 124fun prettify1_stac stac = 125 (minspace_sl o rm_infix o rm_prefix o rm_par o rm_dbfetch) 126 (ttt_lex stac) 127 128fun prettify2_stac stac = 129 (minspace_sl o ttt_lex) stac 130 131(*---------------------------------------------------------------------------- 132 Externalizing local declaration 133 ----------------------------------------------------------------------------*) 134 135fun find_local_aux loc_acc acc sl = case sl of 136 [] => (rev loc_acc, rev acc) 137 | "let" :: m => 138 let 139 val (decl,cont0) = split_level "in" m 140 val (body,cont1) = split_level "end" cont0 141 in 142 if length body <> 1 143 then raise ERR "find_local" "" 144 else find_local_aux (decl :: loc_acc) (hd body :: acc) cont1 145 end 146 | a :: m => find_local_aux loc_acc (a :: acc) m 147 148fun find_local stac = find_local_aux [] [] (ttt_lex stac) 149 150(*---------------------------------------------------------------------------- 151 Prettifying proofs 152 ----------------------------------------------------------------------------*) 153 154datatype Proof = 155 Tactic of (string * goal) 156 | Then of (Proof * Proof) 157 | Thenl of (Proof * Proof list) 158 159fun pretty_allstac tim proof = case proof of 160 Tactic (s,g) => 161 let val (s1,s2) = (prettify1_stac s, prettify2_stac s) in 162 if same_effect tim s s1 g then Tactic (s1,g) else Tactic (s2,g) 163 end 164 | Then (p1,p2) => Then (pretty_allstac tim p1, pretty_allstac tim p2) 165 | Thenl (p,pl) => Thenl (pretty_allstac tim p, map (pretty_allstac tim) pl) 166 167(*---------------------------------------------------------------------------- 168 Printing proofs and extracting local declarations 169 ----------------------------------------------------------------------------*) 170 171fun string_of_proof proof = 172 let 173 val decll_ref = ref [] 174 fun loop proof = case proof of 175 Tactic (s,_) => 176 let val (decll,news) = find_local s in 177 decll_ref := decll @ (!decll_ref); 178 minspace_sl news 179 end 180 | Then (p1,p2) => loop p1 ^ " THEN\n " ^ loop p2 181 | Thenl (p,pl) => 182 let 183 val sl = map loop pl 184 val set = mk_fast_set String.compare sl 185 in 186 if length set = 1 187 then loop p ^ " THEN\n " ^ hd set 188 else loop p ^ " THENL\n [" ^ String.concatWith ",\n " sl ^ "]" 189 end 190 val body = loop proof 191 val decll = mk_fast_set (list_compare String.compare) (!decll_ref) 192 val decls = map (String.concatWith " ") decll 193 in 194 if null decls 195 then body 196 else "let\n " ^ 197 String.concatWith "\n " decls ^ "\nin\n " ^ body ^ "\nend" 198 end 199 200fun safestring_of_proof proof = case proof of 201 Tactic (s,_) => "(" ^ s ^ ")" 202 | Then (p1,p2) => string_of_proof p1 ^ " THEN " ^ string_of_proof p2 203 | Thenl (p,pl) => 204 let 205 val sl = map string_of_proof pl 206 val set = mk_fast_set String.compare sl 207 in 208 if length set = 1 209 then string_of_proof p ^ " THEN " ^ "(" ^ hd set ^ ")" 210 else string_of_proof p ^ " THENL " ^ 211 "[" ^ String.concatWith ", " sl ^ "]" 212 end 213 214(*---------------------------------------------------------------------------- 215 Minimizing lists 216 ----------------------------------------------------------------------------*) 217 218fun decompose sl = case sl of 219 [] => [] 220 | "[" :: m => 221 let 222 val (body,cont) = split_level "]" m 223 val l = map (String.concatWith " ") (rpt_split_level "," body) 224 in 225 (true, ([],l)) :: decompose cont 226 end 227 | a :: m => (false, ([],[a])) :: decompose m 228 229fun list_to_string sl = "[ " ^ String.concatWith " , " sl ^ " ]" 230 231fun group_to_string l = 232 let fun to_string (b,(l1',l2')) = 233 if b then list_to_string (l1' @ l2') else hd l2' 234 in 235 String.concatWith " " (map to_string l) 236 end 237 238fun mini_stac tim g gl pl l = case l of 239 [] => group_to_string pl 240 | (false,a) :: m => mini_stac tim g gl (pl @ [(false,a)]) m 241 | (true,(l1,l2)) :: m => 242 if null l2 243 then mini_stac tim g gl (pl @ [(true,(l1,l2))]) m 244 else 245 let val new_stac = group_to_string (pl @ [(true, (l1, tl l2))] @ m) in 246 if is_effect tim new_stac g gl 247 then mini_stac tim g gl pl ((true, (l1, tl l2)) :: m) 248 else mini_stac tim g gl pl ((true, (l1 @ [hd l2], tl l2)) :: m) 249 end 250 251fun mini_stac_g_gl tim stac g gl = 252 mini_stac tim g gl [] (decompose (ttt_lex stac)) 253 254(*---------------------------------------------------------------------------- 255 Minimizing lists in all tactics of a proof 256 ----------------------------------------------------------------------------*) 257 258fun mini_proofstac stac g = 259 let 260 val gl = fst (tactic_of_sml stac g) 261 handle _ => (debug "Error: minimize"; raise ERR "minimize" stac) 262 val tim = Real.max (!ttt_tactic_time, !ttt_metis_time) 263 in 264 mini_stac tim g gl [] (decompose (ttt_lex stac)) 265 end 266 267fun mini_allstac proof = case proof of 268 Tactic (s,g) => Tactic (mini_proofstac s g,g) 269 | Then (p1,p2) => Then (mini_allstac p1, mini_allstac p2) 270 | Thenl (p,pl) => Thenl (mini_allstac p, map mini_allstac pl) 271 272(*---------------------------------------------------------------------------- 273 Trivial proof minimization 274 ----------------------------------------------------------------------------*) 275(* could be replaced by minimization search, 276 favorising breadth first, with a high exploration coefficient *) 277fun mini_proof proof = case proof of 278 Tactic _ => proof 279 | Then (Tactic (_,g),p2) => 280 let val s = string_of_proof p2 in 281 if is_proof s g then p2 else proof 282 end 283 | Then (p1,p2) => Then (mini_proof p1, mini_proof p2) 284 | Thenl (p,pl) => Thenl (mini_proof p, map mini_proof pl) 285 286fun mini_proof_wrap p = 287 if !ttt_minimize_flag then 288 let 289 val _ = debug "Starting minimization" 290 val newp = mini_proof (mini_allstac p) 291 val _ ="End minimization" 292 in 293 newp 294 end 295 else p 296 297(*---------------------------------------------------------------------------- 298 Combining minimization and prettification. 299 ----------------------------------------------------------------------------*) 300 301fun minimize_stac tim stac g gl = prettify1_stac (mini_stac_g_gl tim stac g gl) 302 303fun pretty_proof_wrap p = 304 if !ttt_prettify_flag then 305 let 306 val _ = debug "Starting prettification" 307 val tim = Real.max (!ttt_tactic_time, !ttt_metis_time) 308 val newp = pretty_allstac tim p 309 val _ = debug "End prettification" 310 in 311 newp 312 end 313 else p 314 315fun minimize_proof p = 316 (pretty_proof_wrap o mini_proof_wrap) p 317 handle _ => 318 (debug "Error: prettification or minimization failed"; p) 319 320(*---------------------------------------------------------------------------- 321 Reconstructing the proof. 322 ----------------------------------------------------------------------------*) 323 324fun proof_length proof = case proof of 325 Tactic (s,g) => 1 326| Then (p1,p2) => proof_length p1 + proof_length p2 327| Thenl (p,pl) => proof_length p + sum_int (map proof_length pl) 328 329fun reconstruct_aux g proof sproof = 330 let 331 val tim = Time.toReal (!ttt_search_time) 332 val tac = tactic_of_sml sproof handle _ => NO_TAC 333 val new_tim = snd (add_time (timeOut tim Tactical.TAC_PROOF) (g,tac)) 334 handle _ => (debug ("Warning: reconstruct: " ^ sproof); tim) 335 in 336 debug_proof ("proof length: " ^ int_to_string (proof_length proof)); 337 debug_proof ("proof time: " ^ Real.toString new_tim); 338 sproof 339 end 340 341fun requote sl = case sl of 342 [] => [] 343 | "[" :: "QUOTE" :: s :: "]" :: m => 344 if tttTools.is_string s 345 then ("`" ^ rm_space (rm_comment (rm_squote s)) ^ "`") :: requote m 346 else hd sl :: requote (tl sl) 347 | "Term" :: "[" :: "QUOTE" :: s :: "]" :: m => 348 if tttTools.is_string s 349 then ("``" ^ rm_space (rm_comment (rm_squote s)) ^ "``") :: requote m 350 else hd sl :: requote (tl sl) 351 | a :: m => a :: requote m 352 353fun requote_sproof s = (minspace_sl o requote o ttt_lex) s 354 355fun unsafe_reconstruct g proof = 356 reconstruct_aux g proof (requote_sproof (string_of_proof proof)) 357 358fun safe_reconstruct g proof = 359 reconstruct_aux g proof (safestring_of_proof proof) 360 361fun reconstruct g proof = 362 ( 363 if !ttt_prettify_flag 364 then (unsafe_reconstruct g proof handle _ => safe_reconstruct g proof) 365 else safe_reconstruct g proof 366 ) 367 handle _ => 368 (debug ("Error: reconstruction failed" ^ string_of_proof proof); 369 string_of_proof proof) 370 371end (* struct *) 372