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