1structure spec_databaseLib :> spec_databaseLib = 2struct 3 4open HolKernel boolLib bossLib 5 6val ERR = Feedback.mk_HOL_ERR "spec_databaseLib" 7 8(* ------------------------------------------------------------------------ *) 9 10datatype ''opt entry = Pending of thm * term | Built of (''opt list * thm) list 11 12fun thm_eq thm1 thm2 = Term.aconv (Thm.concl thm1) (Thm.concl thm2) 13 14(* ------------------------------------------------------------------------- 15 mk_spec_database 16 17 Tools for maintaining a database of specification theorems. 18 19 The type ''opt represents configuration options. 20 21 - basic_opt : unit -> ''opt 22 23 Get the options corresponding with the specification that comes directly 24 from applying "basic_spec". 25 26 - default_opt 27 28 The default build option. 29 30 - proj_opt 31 32 Used to determine if the current option setting is different from 33 "basic_opt". 34 35 - closeness : ''opt -> ''opt -> int 36 37 Gives value to ease with which one options setting can be converted to 38 another. A negative result corresponds with "impossible", whereas 39 a high value indicates a close match. 40 41 - convert_opt_rule 42 43 Gives the rule for conversting from one option setting to another. 44 45 - get_opcode 46 47 Extracts the database index key (usual the instructions op-code) from 48 the specification theorom. 49 50 - basic_spec : thm * term -> thm 51 52 Gives the basic spcification. 53 ------------------------------------------------------------------------- *) 54 55fun mk_spec_database basic_opt (default_opt: ''opt) proj_opt closeness 56 convert_opt_rule get_opcode basic_spec = 57 let 58 val current_opt = ref default_opt 59 fun set_current_opt opt = current_opt := opt 60 fun get_current_opt () = !current_opt 61 val db = ref (LVTermNet.empty: (''opt entry) LVTermNet.lvtermnet) 62 val add1 = 63 fn x as Pending (_, tm) => 64 db := LVTermNet.insert (!db, ([], get_opcode (ASSUME tm)), x) 65 | x as Built [] => raise ERR "add1" "" 66 | x as Built ((_, thm) :: _) => 67 db := LVTermNet.insert (!db, ([], get_opcode thm), x) 68 val add1_pending = add1 o Pending 69 fun reset_db () = 70 ( print "\nResetting specifications database.\n\n" 71 ; db := LVTermNet.empty 72 ) 73 fun current_opt_rule target = convert_opt_rule (basic_opt ()) target 74 fun not_basic (opt: ''opt) = proj_opt opt <> proj_opt (basic_opt ()) 75 fun sub1 k = db := fst (LVTermNet.delete (!db, k)) 76 fun replace f (k, tm: term, new) = 77 let 78 val l = List.filter (f tm) (LVTermNet.find (!db, k)) 79 in 80 sub1 k; List.app add1 (l @ [Built new]) 81 end 82 val replace_pending = 83 replace (fn tm => fn Pending (_, t) => t <> tm | _ => true) 84 val replace_built = 85 replace (fn tm => fn Built ((_, th) :: _) => Thm.concl th <> tm 86 | _ => true) 87 fun closest target = fst o utilsLib.maximal Int.compare (closeness target) 88 fun find_closest target = 89 (closest target ## I) o fst o 90 utilsLib.maximal Int.compare (closeness target o closest target o fst) 91 fun insert_thm (opt: ''opt, thm) = 92 let 93 val eq_thm = thm_eq thm 94 fun iter a = 95 fn [] => ([opt], thm) :: List.rev a 96 | (h as (opts, th)) :: t => 97 if eq_thm th 98 then List.revAppend (a, (opt :: opts, th) :: t) 99 else iter (h :: a) t 100 in 101 iter [] 102 end 103 val extract_spec = 104 fn (k, Pending (x as (thm, tm))) => 105 let 106 val opt = !current_opt 107 val () = print "+" 108 val basic = basic_spec x 109 val l = [([basic_opt ()], basic)] 110 val l = if not_basic opt 111 then insert_thm (opt, current_opt_rule opt basic) l 112 else l 113 in 114 replace_pending (k, tm, l) 115 ; (true, Lib.with_exn (snd o hd) l (ERR "extract_spec" "empty")) 116 end 117 | (_, Built []) => raise ERR "extract_spec" "empty built" 118 | (k, Built (l as (_, th) :: _)) => 119 let 120 val opt = !current_opt 121 in 122 (false, 123 case List.find (Lib.mem opt o fst) l of 124 SOME (_, thm) => thm 125 | NONE => let 126 val (close_opt, close_thm) = find_closest opt l 127 val thm = convert_opt_rule close_opt opt close_thm 128 in 129 replace_built 130 (k, Thm.concl th, insert_thm (opt, thm) l) 131 ; thm 132 end) 133 end 134 fun find_thms opc = 135 case LVTermNet.match (!db, opc) of 136 [] => NONE 137 | l => let 138 val (new, thms) = ListPair.unzip (List.map extract_spec l) 139 in 140 SOME (List.exists I new, thms) 141 end 142 fun list_db () = List.map (snd ## I) (LVTermNet.listItems (!db)) 143 in 144 (reset_db, set_current_opt, get_current_opt, add1_pending, find_thms, 145 list_db) 146 end 147 148(* ------------------------------------------------------------------------ *) 149 150end 151