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