1(* ========================================================================= *)
2(* FILE          : mlThmData.sml                                             *)
3(* DESCRIPTION   : Theorem data used by the nearest neighbor predictor       *)
4(* AUTHOR        : (c) Thibault Gauthier, University of Innsbruck            *)
5(* DATE          : 2017                                                      *)
6(* ========================================================================= *)
7
8structure mlThmData :> mlThmData =
9struct
10
11open HolKernel boolLib aiLib smlLexer smlExecute smlRedirect mlFeature
12
13val ERR = mk_HOL_ERR "mlThmData"
14
15type thmid = string
16type thmdata = (int, real) Redblackmap.dict * (thmid * fea) list
17val empty_thmdata = (dempty Int.compare,[])
18
19(* -------------------------------------------------------------------------
20   Artificial theory name for theorems from the namespace.
21   Warning: conflict if a theory is named namespace_tag.
22   ------------------------------------------------------------------------- *)
23
24val namespace_tag = "namespace_tag"
25
26(* -------------------------------------------------------------------------
27   Namespace theorems
28   ------------------------------------------------------------------------- *)
29
30fun unsafe_namespace_thms () =
31  let
32    val l0 = #allVal (PolyML.globalNameSpace) ()
33    val l1 = filter (fn x => is_thm_value l0 x andalso x <> "it") (map fst l0)
34  in
35    case thml_of_sml l1 of
36      SOME l2 => combine (l1,l2)
37    | NONE => List.mapPartial thm_of_sml l1
38  end
39
40fun safe_namespace_thms () =
41  let
42    val l0 = #allVal (PolyML.globalNameSpace) ()
43    val l1 = filter (fn x => x <> "it") (map fst l0)
44  in
45    List.mapPartial thm_of_sml l1
46  end
47
48(* -------------------------------------------------------------------------
49   Metis string
50   ------------------------------------------------------------------------- *)
51
52fun dbfetch_of_thmid s =
53  let val (a,b) = split_string "Theory." s in
54    if a = current_theory ()
55      then String.concatWith " " ["DB.fetch", mlquote a, mlquote b]
56    else
57      if mem a [namespace_tag] then b else s
58  end
59
60fun mk_metis_call sl =
61  "metisTools.METIS_TAC " ^
62  "[" ^ String.concatWith " , " (map dbfetch_of_thmid sl) ^ "]"
63
64(* -------------------------------------------------------------------------
65   Theorem dependencies
66   ------------------------------------------------------------------------- *)
67
68fun depnumber_of_thm thm =
69  (Dep.depnumber_of o Dep.depid_of o Tag.dep_of o Thm.tag) thm
70  handle HOL_ERR _ => raise ERR "depnumber_of_thm" ""
71
72fun depidl_of_thm thm =
73  (Dep.depidl_of o Tag.dep_of o Thm.tag) thm
74  handle HOL_ERR _ => raise ERR "depidl_of_thm" ""
75
76fun depid_of_thm thm =
77  (Dep.depid_of o Tag.dep_of o Thm.tag) thm
78  handle HOL_ERR _ => raise ERR "depidl_of_thm" ""
79
80fun thmid_of_depid (thy,n) =
81  let fun has_depnumber n (_,thm) = n = depnumber_of_thm thm in
82    case List.find (has_depnumber n) (DB.thms thy) of
83      SOME (name,_) =>
84        if can (DB.fetch thy) name andalso uptodate_thm (DB.fetch thy name)
85        then SOME (thy ^ "Theory." ^ name)
86        else NONE
87    | NONE => NONE
88  end
89
90fun intactdep_of_thm thm =
91  let
92    val l0 = depidl_of_thm thm
93    val l1 = List.mapPartial thmid_of_depid l0
94  in
95    (length l0 = length l1, l1)
96  end
97
98fun validdep_of_thmid thmid =
99  let val (a,b) = split_string "Theory." thmid in
100    if mem a [namespace_tag]
101    then []
102    else List.mapPartial thmid_of_depid (depidl_of_thm (DB.fetch a b))
103  end
104
105(* -------------------------------------------------------------------------
106   Theorem features
107   ------------------------------------------------------------------------- *)
108
109fun add_thmfea thy ((name,thm),(thmfea,symfreq,nodupl)) =
110  let
111    val g = dest_thm thm
112    val thmid = thy ^ "Theory." ^ name
113    val newnodupl = dadd g () nodupl
114  in
115    if not (dmem g nodupl) andalso uptodate_thm thm
116    then
117      let
118        val fea = fea_of_goal_cached true g
119        val newthmfea = (thmid,fea) :: thmfea
120        val newsymfreq = count_dict symfreq fea
121      in
122        (newthmfea,newsymfreq,newnodupl)
123      end
124    else (thmfea,symfreq,newnodupl)
125  end
126
127fun add_thmfea_from_thy (thy,acc) =
128  foldl (add_thmfea thy) acc (DB.thms thy)
129
130fun thmfea_from_thyl thyl =
131  foldl add_thmfea_from_thy ([], dempty Int.compare, dempty goal_compare) thyl
132
133fun add_namespacethm acc =
134  let val l = unsafe_namespace_thms () in
135    foldl (add_thmfea namespace_tag) acc l
136  end
137
138val create_thmdata_time = ref 0.0
139
140val create_thmdata_cache = ref (dempty (list_compare String.compare))
141
142fun clean_create_thmdata_cache () =
143  create_thmdata_cache := dempty (list_compare String.compare)
144
145val add_cthy_time = ref 0.0
146val add_namespace_time = ref 0.0
147val thmdata_tfidf_time = ref 0.0
148
149fun create_thmdata () =
150  let
151    val thy = current_theory ()
152    val thyl = ancestry thy
153    val acc1 =
154      dfind thyl (!create_thmdata_cache) handle NotFound =>
155      let val r = thmfea_from_thyl thyl in
156        create_thmdata_cache := dadd thyl r (!create_thmdata_cache); r
157      end
158    val acc2 = total_time add_cthy_time add_thmfea_from_thy (thy,acc1)
159    val (thmfea3,symfreq3,_) = total_time add_namespace_time
160      add_namespacethm acc2
161    val n = int_to_string (length thmfea3)
162  in
163    print_endline ("Loading " ^ n ^ " theorems");
164    (total_time thmdata_tfidf_time
165     (learn_tfidf_symfreq_nofilter (length thmfea3)) symfreq3, thmfea3)
166  end
167
168(* -------------------------------------------------------------------------
169   Convert theorem identifier to a theorem value (used by holyhammer)
170   ------------------------------------------------------------------------- *)
171
172fun in_namespace s = fst (split_string "Theory." s) = namespace_tag
173
174fun thm_of_name s =
175  if in_namespace s
176  then (case thm_of_sml (snd (split_string "Theory." s)) of
177      SOME (_,thm) => SOME (s,thm)
178    | NONE => NONE)
179  else
180    let val (a,b) = split_string "Theory." s in
181      SOME (s, DB.fetch a b)
182    end
183
184fun thml_of_namel sl = List.mapPartial thm_of_name sl
185
186(* -------------------------------------------------------------------------
187   Convert a theorem value to sml code.
188   ------------------------------------------------------------------------- *)
189
190fun dbfetch_of_depid thm =
191  if can depid_of_thm thm then
192    let
193      val (thy,n) = depid_of_thm thm
194      val thml = DB.thms thy
195      val thmdict = dnew goal_compare (map (fn (a,b) => (dest_thm b,a)) thml)
196      val goal = dest_thm thm
197    in
198      if dmem goal thmdict
199      then
200        let val name = dfind goal thmdict in
201          SOME (String.concatWith " "
202            ["(","DB.fetch", mlquote thy, mlquote name,")"])
203        end
204      else NONE
205    end
206  else NONE
207
208
209end (* struct *)
210