1(* ========================================================================== *) 2(* FILE : tttLearn.sml *) 3(* DESCRIPTION : Learning from tactic calls during search and recording *) 4(* AUTHOR : (c) Thibault Gauthier, University of Innsbruck *) 5(* DATE : 2017 *) 6(* ========================================================================== *) 7 8structure tttLearn :> tttLearn = 9struct 10 11open HolKernel boolLib Abbrev tttTools tttPredict tttExec tttMinimize 12tttTimeout tttFeature tttThmData tttGoallistData tttSetup tttLexer 13 14val ERR = mk_HOL_ERR "tttLearn" 15 16(*---------------------------------------------------------------------------- 17 * Abstracting theorem list in tactics 18 *----------------------------------------------------------------------------*) 19 20(* Unsafe 21 22val thm_cache = ref (dempty String.compare) 23 24fun is_thm_cache s = 25 dfind s (!thm_cache) handle _ => 26 let val b = hide_out is_thm s in 27 thm_cache := dadd s b (!thm_cache); 28 b 29 end 30*) 31 32val thmlarg_placeholder = "tactictoe_thmlarg" 33 34fun is_thmlarg_stac stac = mem thmlarg_placeholder (ttt_lex stac) 35 36fun change_thml thml = case thml of 37 [] => NONE 38 | a :: m => 39 ( 40 if is_thm (String.concatWith " " a) 41 then SOME thml 42 else NONE 43 ) 44 45fun abstract_thmlarg_loop thmlacc l = case l of 46 [] => [] 47 | "[" :: m => 48 let 49 val (el,cont) = split_level "]" m 50 val thml = rpt_split_level "," el 51 in 52 case change_thml thml of 53 NONE => "[" :: abstract_thmlarg_loop thmlacc m 54 | SOME x => 55 ( 56 thmlacc := map (String.concatWith " ") thml :: !thmlacc; 57 ["[",thmlarg_placeholder,"]"] @ 58 abstract_thmlarg_loop thmlacc cont 59 ) 60 end 61 | a :: m => a :: abstract_thmlarg_loop thmlacc m 62 63fun pe_abs stac = 64 let 65 val sl1 = ttt_lex stac 66 val lref = ref [] 67 val sl2 = abstract_thmlarg_loop lref sl1 68 in 69 ( 70 String.concatWith " " sl2, 71 map (List.mapPartial thm_of_sml) (List.rev (!lref)) 72 ) 73 end 74 75fun abstract_thmlarg stac = 76 if is_thmlarg_stac stac then stac else 77 let 78 val sl1 = ttt_lex stac 79 val sl2 = abstract_thmlarg_loop (ref []) sl1 80 in 81 if sl2 = sl1 then stac else String.concatWith " " sl2 82 end 83 84(*---------------------------------------------------------------------------- 85 * Instantiating tactics with theorem list 86 *----------------------------------------------------------------------------*) 87 88fun inst_thmlarg_loop thmls l = 89 let fun f x = if x = thmlarg_placeholder then thmls else x in 90 map f l 91 end 92 93fun inst_thmlarg thmls stac = 94 let val sl = ttt_lex stac in 95 if mem thmlarg_placeholder sl 96 then String.concatWith " " (inst_thmlarg_loop thmls sl) 97 else stac 98 end 99 100(* 101val s = "METIS_TAC [arithmeticTheory.LESS_EQ]"; 102val s1 = abstract_stac s; 103val s2 = inst_thmlarg "bonjour" s1; 104*) 105 106(*---------------------------------------------------------------------------- 107 * Abstracting term (first occurence) 108 *----------------------------------------------------------------------------*) 109 110val termarg_placeholder = "tactictoe_termarg" 111 112fun abs_termarg_loop l = case l of 113 [] => ([], NONE) 114 | "[" :: "HolKernel.QUOTE" :: s :: "]" :: m => 115 (termarg_placeholder :: m, SOME s) 116 | "[" :: "QUOTE" :: s :: "]" :: m => 117 (termarg_placeholder :: m, SOME s) 118 | a :: m => 119 let val (sl,so) = abs_termarg_loop m in (a :: sl, so) end 120 121fun abs_termarg stac = 122 let 123 val sl1 = ttt_lex stac 124 val (sl2,so) = abs_termarg_loop sl1 125 in 126 case so of 127 NONE => NONE 128 | SOME s => 129 let 130 val qtacs = String.concatWith " " 131 (["fn", termarg_placeholder,"=>", "Tactical.VALID","("] @ sl2 @ [")"]) 132 val qtac = qtactic_of_sml qtacs 133 in 134 if is_stype s then NONE else SOME (term_of_sml s, qtac) 135 end 136 end 137 handle _ => (debug ("Error: abs_termarg: " ^ stac); NONE) 138 139(*---------------------------------------------------------------------------- 140 * Instantiate tactics with term 141 *----------------------------------------------------------------------------*) 142 143fun with_types f x = 144 let 145 val mem = !show_types 146 val _ = show_types := true 147 val r = f x 148 val _ = show_types := mem 149 in 150 r 151 end 152 153fun inst_termarg_loop term l = case l of 154 [] => [] 155 | "[" :: "HolKernel.QUOTE" :: _ :: "]" :: m => 156 "[" :: "HolKernel.QUOTE" :: mlquote (with_types term_to_string term) :: "]" :: m 157 | "[" :: "QUOTE" :: s :: "]" :: m => 158 "[" :: "QUOTE" :: mlquote (with_types term_to_string term) :: "]" :: m 159 | a :: m => a :: inst_termarg_loop term m 160 161fun inst_termarg stac term = 162 String.concatWith " " (inst_termarg_loop term (ttt_lex stac)) 163 164(* 165load "tttLearn"; 166val stac = 167"boolLib.SPEC_TAC ( ( Parse.Term [ HolKernel.QUOTE \" (*#loc 1 119422*)m:num\"" 168^ " ] ) , ( Parse.Term [ HolKernel.QUOTE \" (*#loc 1 119435*)m:num\" ] ) )"; 169val stac2 = tttLearn.inst_termarg stac ``v:num``; 170val tac = tttExec.tactic_of_sml stac2; 171 172val s = mlquote (term_to_string ``A /\ B``); 173val s1 = "SPEC_TAC (Term [QUOTE \"x:bool\"],Term[QUOTE" ^ s ^ "])"; 174val tac = tttExec.tactic_of_sml s1; 175*) 176 177(*---------------------------------------------------------------------------- 178 Combining abstractions and instantiations 179 *----------------------------------------------------------------------------*) 180 181fun is_absarg_stac s = is_thmlarg_stac s 182 183fun abstract_stac stac = 184 let 185 val stac1 = 186 if !ttt_thmlarg_flag 187 then abstract_thmlarg stac 188 else stac 189 in 190 if stac1 <> stac then SOME stac1 else NONE 191 end 192 193fun prefix_absstac stac = [abstract_stac stac, SOME stac] 194 195fun concat_absstacl ostac stacl = 196 let val l = List.concat (map prefix_absstac stacl) @ [abstract_stac ostac] in 197 mk_sameorder_set String.compare (List.mapPartial I l) 198 end 199 200fun inst_stac thmls g stac = 201 if !ttt_thmlarg_flag then inst_thmlarg thmls stac else stac 202 203fun inst_stacl thmls g stacl = map (fn x => (x, inst_stac thmls g x)) stacl 204 205(*---------------------------------------------------------------------------- 206 * Orthogonalization. 207 *----------------------------------------------------------------------------*) 208 209fun record_glfea b (g,gl) = 210 if !ttt_recgl_flag 211 then update_glfea (fea_of_goallist gl) (b,(hash_goal g)) 212 else () 213 214val (TC_OFF : tactic -> tactic) = trace ("show_typecheck_errors", 0) 215 216fun test_stac g gl (stac, istac) = 217 let val (new_gl,_) = 218 ( 219 debug ("test_stac " ^ stac ^ "\n" ^ istac); 220 let val tac = tactic_of_sml istac 221 handle _ => (debug ("Warning: tactic_of_sml: " ^ istac); NO_TAC) 222 in 223 timeOut (!ttt_tactic_time) (TC_OFF tac) g 224 end 225 ) 226 in 227 if all (fn x => mem x gl) new_gl 228 then (record_glfea true (g,new_gl); SOME (stac,0.0,g,new_gl)) 229 else (record_glfea false (g,new_gl); NONE) 230 end 231 handle _ => NONE 232 233fun orthogonalize (lbl as (ostac,t,g,gl),fea) = 234 let 235 (* predict tactics *) 236 val _ = debug "predict tactics" 237 val feavl0 = dlist (!ttt_tacfea) 238 val symweight = learn_tfidf feavl0 239 val lbls = stacknn symweight (!ttt_ortho_radius) feavl0 fea 240 val stacl1 = mk_sameorder_set String.compare (map #1 lbls) 241 val stacl2 = filter (fn x => not (x = ostac)) stacl1 242 (* order tactics by frequency *) 243 val _ = debug "order tactics" 244 fun score x = dfind x (!ttt_taccov) handle _ => 0 245 val oscore = score ostac 246 val stacl3 = filter (fn x => score x > oscore) stacl2 247 fun n_compare (x,y) = Int.compare (score y, score x) 248 val stacl4 = dict_sort n_compare stacl3 249 (* try abstracted tactic x before x *) 250 val _ = debug "concat abstract tactics" 251 val stacl5 = concat_absstacl ostac stacl4 252 (* predicting theorems only once *) 253 val _ = debug "predict theorems" 254 val thml = 255 if !ttt_thmlarg_flag 256 then thmknn_std (!ttt_thmlarg_radius) g 257 else [] 258 val thmls = String.concatWith " , " (map dbfetch_of_string thml) 259 (* instantiate arguments *) 260 val _ = debug "instantiate argument" 261 val stacl6 = inst_stacl thmls g stacl5 262 (* test produced tactics *) 263 val _ = debug "test tactics" 264 val testo = findSome (test_stac g gl) stacl6 265 in 266 case testo of 267 NONE => lbl 268 | SOME newlbl => newlbl 269 end 270 271end (* struct *) 272