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