1(* ========================================================================== *)
2(* FILE          : tttThmData.sml                                               *)
3(* DESCRIPTION   :                                                            *)
4(*                                                                            *)
5(* AUTHOR        : (c) Thibault Gauthier, University of Innsbruck             *)
6(* DATE          : 2017                                                       *)
7(* ========================================================================== *)
8
9structure tttThmData :> tttThmData =
10struct
11
12open HolKernel boolLib Abbrev tttTools tttExec tttLexer tttFeature tttPredict
13tttSetup
14
15val ERR = mk_HOL_ERR "tttThmData"
16
17(* --------------------------------------------------------------------------
18   Import
19   -------------------------------------------------------------------------- *)
20
21fun thm_of_string s =
22  let val (a,b) = split_string "Theory." s in DB.fetch a b end
23
24fun parse_thmfea s = case ttt_lex s of
25    a :: m => (SOME (dest_thm (thm_of_string a), (a, map string_to_int m))
26      handle _ => NONE)
27  | _ => raise ERR "parse_thmfea" s
28
29fun read_thmfea thy =
30  let
31    val l0 = readl (ttt_thmfea_dir ^ "/" ^ thy)
32      handle _ => (if mem thy ["min","bool"] then () else debug thy; [])
33    val l1 = List.mapPartial parse_thmfea l0
34  in
35    ttt_thmfea := daddl l1 (!ttt_thmfea)
36  end
37
38fun import_thmfea thyl = app read_thmfea thyl
39
40(* --------------------------------------------------------------------------
41   Update
42   -------------------------------------------------------------------------- *)
43
44fun update_thmfea cthy =
45  let
46    val thml = DB.thms cthy
47    fun f (s,thm) =
48      let
49        val name = cthy ^ "Theory." ^ s
50        val goal = dest_thm thm
51        val fea = snd (dfind goal (!ttt_thmfea))
52          handle _ => fea_of_goal goal
53      in
54        ttt_thmfea := dadd goal (name,fea) (!ttt_thmfea)
55      end
56  in
57    app f thml
58  end
59
60(* --------------------------------------------------------------------------
61   Export
62   -------------------------------------------------------------------------- *)
63
64fun export_thmfea cthy =
65  let
66    val _ = update_thmfea cthy
67    val namel = map fst (DB.thms cthy)
68    fun in_curthy (_,(s,_)) =
69      let val (thy,name) = split_string "Theory." s in
70        thy = cthy andalso mem name namel
71      end
72    val fname = ttt_thmfea_dir ^ "/" ^ cthy
73    val l0 = filter in_curthy (dlist (!ttt_thmfea))
74    fun f (_,(name,fea)) =
75      String.concatWith " " (name :: map int_to_string fea)
76    val l1 = map f l0
77  in
78    writel fname l1
79  end
80
81end (* struct *)
82