1(* ========================================================================= *) 2(* FILE : psMinimize.sml *) 3(* DESCRIPTION : Minimize and prettify tactical proofs *) 4(* AUTHOR : (c) Thibault Gauthier, University of Innsbruck *) 5(* DATE : 2017 *) 6(* ========================================================================= *) 7 8structure psMinimize :> psMinimize = 9struct 10 11open HolKernel Abbrev boolLib aiLib 12 smlExecute smlLexer smlTimeout smlPrettify 13 14val ERR = mk_HOL_ERR "psMinimize" 15 16val mini_proof_time = ref 20.0 17val mini_tactic_time = ref 0.2 18val sthen = ">>" 19val sthenl = ">|" 20 21(* ------------------------------------------------------------------------- 22 Tests 23 ------------------------------------------------------------------------- *) 24 25val glopt_eq = option_eq (list_eq goal_eq) 26 27fun same_effect tim stac1 stac2 g = 28 let 29 val gl1o = app_stac tim stac1 g 30 val gl2o = app_stac tim stac2 g 31 in 32 not (glopt_eq gl1o NONE) andalso not (glopt_eq gl2o NONE) andalso 33 glopt_eq gl1o gl2o 34 end 35 36fun is_proof tim stac g = glopt_eq (app_stac stac tim g) (SOME []) 37fun has_effect tim stac g gl = glopt_eq (app_stac tim stac g) (SOME gl) 38 39(* ------------------------------------------------------------------------- 40 Pretty tactic string 41 ------------------------------------------------------------------------- *) 42 43fun unsafe_prettify_stac stac = 44 (smart_space o elim_infix o elim_struct o elim_par o 45 elim_dbfetch o partial_sml_lexer) 46 stac 47 48fun safe_prettify_stac stac = (smart_space o partial_sml_lexer) stac 49 50(* ------------------------------------------------------------------------- 51 Pretty proof steps 52 ------------------------------------------------------------------------- *) 53 54datatype Proof = 55 Tactic of (string * goal) 56 | Then of (Proof * Proof) 57 | Thenl of (Proof * Proof list) 58 59fun pretty_allstac tim proof = case proof of 60 Tactic (s,g) => 61 let val (s1,s2) = (unsafe_prettify_stac s, safe_prettify_stac s) in 62 if same_effect tim s s1 g then Tactic (s1,g) else Tactic (s2,g) 63 end 64 | Then (p1,p2) => Then (pretty_allstac tim p1, pretty_allstac tim p2) 65 | Thenl (p,pl) => Thenl (pretty_allstac tim p, map (pretty_allstac tim) pl) 66 67(* ------------------------------------------------------------------------- 68 Externalizing local declaration 69 ------------------------------------------------------------------------- *) 70 71fun find_local_aux loc_acc acc sl = case sl of 72 [] => (rev loc_acc, rev acc) 73 | "let" :: m => 74 let 75 val (decl,cont0) = split_level "in" m 76 val (body,cont1) = split_level "end" cont0 77 in 78 if length body <> 1 79 then raise ERR "find_local" "" 80 else find_local_aux (decl :: loc_acc) (hd body :: acc) cont1 81 end 82 | a :: m => find_local_aux loc_acc (a :: acc) m 83 84fun find_local stac = find_local_aux [] [] (partial_sml_lexer stac) 85 86fun unsafe_prettify_proof proof = 87 let 88 val decll_ref = ref [] 89 fun loop proof = case proof of 90 Tactic (s,_) => 91 let val (decll,news) = find_local s in 92 decll_ref := decll @ (!decll_ref); 93 smart_space news 94 end 95 | Then (p1,p2) => loop p1 ^ " " ^ sthen ^ " " ^ loop p2 96 | Thenl (p,pl) => 97 let 98 val sl = map loop pl 99 val set = mk_fast_set String.compare sl 100 in 101 if length set = 1 102 then loop p ^ " " ^ sthen ^ " " ^ hd set 103 else loop p ^ " " ^ sthenl ^ " " ^ 104 "[" ^ String.concatWith ", " sl ^ "]" 105 end 106 val body = loop proof 107 val decll = mk_fast_set (list_compare String.compare) (!decll_ref) 108 val decls = map (String.concatWith " ") decll 109 in 110 if null decls 111 then body 112 else "let " ^ String.concatWith " " decls ^ " in " ^ body ^ "end" 113 end 114 115fun safe_prettify_proof proof = case proof of 116 Tactic (s,_) => "(" ^ s ^ ")" 117 | Then (p1,p2) => safe_prettify_proof p1 ^ " " ^ 118 sthen ^ " " ^ safe_prettify_proof p2 119 | Thenl (p,pl) => 120 let val sl = map safe_prettify_proof pl in 121 safe_prettify_proof p ^ " " ^ sthenl ^ " " ^ 122 "[" ^ String.concatWith ", " sl ^ "]" 123 end 124 125(*--------------------------------------------------------------------------- 126 Minimizing lists in one tactic 127 ---------------------------------------------------------------------------*) 128 129fun decompose sl = case sl of 130 [] => [] 131 | "[" :: m => 132 let 133 val (body,cont) = split_level "]" m 134 val l = map (String.concatWith " ") (rpt_split_level "," body) 135 in 136 (true, ([],l)) :: decompose cont 137 end 138 | a :: m => (false, ([],[a])) :: decompose m 139 140fun list_to_string sl = "[ " ^ String.concatWith " , " sl ^ " ]" 141 142fun group_to_string l = 143 let fun to_string (b,(l1',l2')) = 144 if b then list_to_string (l1' @ l2') else hd l2' 145 in 146 String.concatWith " " (map to_string l) 147 end 148 149fun mini_stac_aux tim g gl pl l = case l of 150 [] => group_to_string pl 151 | (false,a) :: m => mini_stac_aux tim g gl (pl @ [(false,a)]) m 152 | (true,(l1,l2)) :: m => 153 if null l2 154 then mini_stac_aux tim g gl (pl @ [(true,(l1,l2))]) m 155 else 156 let val new_stac = group_to_string (pl @ [(true, (l1, tl l2))] @ m) in 157 if has_effect tim new_stac g gl 158 then mini_stac_aux tim g gl pl ((true, (l1, tl l2)) :: m) 159 else mini_stac_aux tim g gl pl ((true, (l1 @ [hd l2], tl l2)) :: m) 160 end 161 162fun mini_stac stac g = 163 let 164 val gl = fst (tactic_of_sml (!mini_tactic_time) stac g) 165 handle Interrupt => raise Interrupt 166 | _ => (debug "Error: minimize"; raise ERR "minimize" stac) 167 val l = decompose (partial_sml_lexer stac) 168 in 169 mini_stac_aux (!mini_tactic_time) g gl [] l 170 end 171 172(*--------------------------------------------------------------------------- 173 Minimizing lists in all tactics of a proof 174 ---------------------------------------------------------------------------*) 175 176fun mini_allstac proof = case proof of 177 Tactic (s,g) => Tactic (mini_stac s g,g) 178 | Then (p1,p2) => Then (mini_allstac p1, mini_allstac p2) 179 | Thenl (p,pl) => Thenl (mini_allstac p, map mini_allstac pl) 180 181(*--------------------------------------------------------------------------- 182 Trivial proof minimization 183 ---------------------------------------------------------------------------*) 184 185fun mini_proof proof = case proof of 186 Tactic _ => proof 187 | Then (Tactic (_,g),p2) => 188 let val s = safe_prettify_proof p2 in 189 if is_proof s (!mini_proof_time) g then p2 else proof 190 end 191 | Then (p1,p2) => Then (mini_proof p1, mini_proof p2) 192 | Thenl (p,pl) => Thenl (mini_proof p, map mini_proof pl) 193 194(*--------------------------------------------------------------------------- 195 Combining minimization and prettification. 196 ---------------------------------------------------------------------------*) 197 198(* tactic (used by holyhammer) *) 199fun minimize_stac tim stac g gl = 200 let val newstac = 201 mini_stac_aux tim g gl [] (decompose (partial_sml_lexer stac)) 202 in 203 unsafe_prettify_stac newstac 204 end 205 206(* proof *) 207fun minimize_proof p = 208 (pretty_allstac (!mini_tactic_time) o mini_proof o mini_allstac) p 209 handle Interrupt => raise Interrupt 210 | _ => (debug "Error: prettification or minimization failed"; p) 211 212(*--------------------------------------------------------------------------- 213 Reconstructing the proof. 214 ---------------------------------------------------------------------------*) 215 216fun proof_length proof = case proof of 217 Tactic (s,g) => 1 218 | Then (p1,p2) => proof_length p1 + proof_length p2 219 | Thenl (p,pl) => proof_length p + sum_int (map proof_length pl) 220 221fun reconstruct_aux g proof sproof = 222 let 223 val tac = tactic_of_sml (!mini_proof_time) sproof 224 handle Interrupt => raise Interrupt | _ => NO_TAC 225 val new_tim = 226 snd (add_time (timeout (!mini_proof_time) Tactical.TAC_PROOF) (g,tac)) 227 handle Interrupt => raise Interrupt | _ => (!mini_proof_time) 228 in 229 debugf "proof length: " int_to_string (proof_length proof); 230 debugf "proof time: " Real.toString new_tim; 231 sproof 232 end 233 234fun requote_sproof s = (smart_space o requote o partial_sml_lexer) s 235 236fun unsafe_reconstruct g proof = 237 reconstruct_aux g proof (requote_sproof (unsafe_prettify_proof proof)) 238 239fun safe_reconstruct g proof = 240 reconstruct_aux g proof (safe_prettify_proof proof) 241 242fun reconstruct g proof = 243 ( 244 unsafe_reconstruct g proof 245 handle Interrupt => raise Interrupt | _ => safe_reconstruct g proof 246 ) 247 handle Interrupt => raise Interrupt | _ => safe_prettify_proof proof 248 249 250end (* struct *) 251