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