1(* ===================================================================== *)
2(* FILE          : hhReconstruct.sml                                     *)
3(* DESCRIPTION   : Reconstruct a proof from the lemmas given by an ATP   *)
4(*                 and minimize them.                                    *)
5(* AUTHOR        : (c) Thibault Gauthier, University of Innsbruck        *)
6(* DATE          : 2015                                                  *)
7(* ===================================================================== *)
8
9structure hhReconstruct :> hhReconstruct =
10struct
11
12open HolKernel boolLib Dep Tag tttTools tttExec hhWriter
13
14val ERR = mk_HOL_ERR "hhReconstruct"
15
16(*----------------------------------------------------------------------------
17   Settings
18 -----------------------------------------------------------------------------*)
19
20val reconstruct_flag = ref true
21val minimization_timeout = ref 1.0
22val reconstruction_timeout = ref 1.0
23
24(*----------------------------------------------------------------------------
25   Reading the ATP output
26 -----------------------------------------------------------------------------*)
27
28fun remove_white_spaces s =
29  let fun f c = if Char.isSpace c then "" else Char.toString c in
30    String.translate f s
31  end
32
33fun not_reserved s = String.isPrefix "thm." s
34fun is_dot c = c = #"."
35
36fun read_status atp_status =
37  remove_white_spaces (hd (readl atp_status))
38  handle Interrupt => raise Interrupt
39       | _         => "Unknown"
40
41fun read_lemmas atp_out =
42  let
43    val l1 = readl atp_out
44    val l2 = map hhTranslate.unescape l1
45    val l3 = filter not_reserved l2
46    fun f s =
47      let
48        val sl1 = String.fields is_dot s
49        val sl2 = tl (butlast sl1)
50      in
51        String.concatWith "." sl2
52      end
53  in
54    mk_fast_set String.compare (map f l3)
55  end
56
57fun get_lemmas (atp_status,atp_out) =
58  if read_status atp_status = "Theorem"
59  then SOME (read_lemmas atp_out)
60  else NONE
61
62(*----------------------------------------------------------------------------
63   Minimization and pretty-printing
64 -----------------------------------------------------------------------------*)
65
66fun hh_reconstruct lemmas g =
67  if not (!reconstruct_flag)
68  then (print_endline (mk_metis_call lemmas);
69        raise ERR "hh_minimize" "reconstruction off")
70  else
71    let
72      val stac = mk_metis_call lemmas
73      val t1 = !minimization_timeout
74      val t2 = !reconstruction_timeout
75      val newstac = hide_out (tttMinimize.minimize_stac t1 stac g) []
76      val tac = hide_out tactic_of_sml newstac
77    in
78      case hide_out (app_tac t2 tac) g of
79        SOME _ => (newstac,tac)
80      | NONE   => raise ERR "hh_reconstruct" "reconstruction failed"
81    end
82
83end
84