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