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