1structure ThmSetData :> ThmSetData =
2struct
3
4open DB Lib HolKernel
5
6type data = LoadableThyData.t
7
8fun splitnm nm = let
9  val comps = String.fields (equal #".") nm
10in
11  case comps of
12    (thy::nm::_) => (thy, nm)
13  | [name] => (current_theory(), name)
14  | [] => raise Fail "String.fields returns empty list??"
15end
16
17fun lookup ty s nm =
18    SOME (uncurry DB.fetch (splitnm nm))
19    handle HOL_ERR _ =>
20           (Feedback.HOL_WARNING "ThmSetData" "lookup"
21                                 ("Bad theorem name: \"" ^ nm ^ "\" from string \"" ^
22                                  s ^ "\" and set-type \"" ^ ty ^ "\"");
23            NONE)
24
25fun read ty s =
26  SOME (List.mapPartial
27            (fn n => if n = "" then NONE
28                     else
29                       Option.map (fn r => (n,r)) (lookup ty s n))
30            (String.fields Char.isSpace s))
31  handle HOL_ERR _ => NONE
32
33fun writeset set = let
34  fun foldthis ((nm,_), acc) = let
35    val (thy,nm) = splitnm nm
36  in
37    (thy^"."^nm)::acc
38  end
39  val list = List.foldr foldthis [] set
40in
41  String.concatWith " " list
42end
43
44(* ----------------------------------------------------------------------
45    destfn: takes polymorphic theory data and turns it into the
46            structured theorem data we want to use
47    storefn: takes a theorem name and stores the associated theorem into
48             the theory data.  Doesn't perform any associated update in
49             the run-time memory
50    exportfn: takes a string and a list of names and theorems and does
51              something with them at runtime (adds them to a simpset,
52              say). The string is expected to be the name of the
53              theory with which these theorems are associated.
54   ---------------------------------------------------------------------- *)
55type destfn = data -> (string * thm) list option
56type storefn = string -> unit
57type exportfn = (string -> (string * thm) list -> unit) option
58val data_map = let
59  open Binarymap
60in
61  ref (mkDict String.compare : (string,destfn * storefn * exportfn) dict)
62end
63
64fun data_storefn s = Option.map #2 (Binarymap.peek(!data_map,s))
65fun data_exportfn s = Option.join (Option.map #3 (Binarymap.peek(!data_map,s)))
66
67fun all_set_types () = Binarymap.foldr (fn (k,_,acc) => k::acc) [] (!data_map)
68
69fun foldli f a l = let
70  fun recurse a i l =
71      case l of
72        [] => a
73      | h::t => recurse (f (i,h,a)) (i + 1) t
74in
75  recurse a 0 l
76end
77
78fun set_alist_merge(a1, a2) = let
79  open Binarymap
80  val emptyd = mkDict String.compare
81  val offset = length a2
82  val d1 = foldli (fn (i,(s,th),d) => insert(d,s,(i,th))) emptyd a1
83  val d2 = foldli (fn (i,(s,th),d) => insert(d,s,(i+offset,th))) d1 a2
84  val items0 = listItems d2
85  val items = Listsort.sort (inv_img_cmp (#1 o #2) Int.compare) items0
86in
87  List.map (fn (s,(i,th)) => (s,th)) items
88end
89
90fun new ty = let
91  val (mk,dest) = LoadableThyData.new {merge = set_alist_merge,
92                                       read = Lib.K (read ty), terms = Lib.K [],
93                                       write = Lib.K writeset, thydataty = ty}
94  fun foldthis (nm,set) =
95      case lookup ty ("<internal>: "^nm) nm of
96        SOME r => (nm, r) :: set
97      | NONE => raise mk_HOL_ERR "ThmSetData" "new" ("Bad theorem name: "^nm)
98  fun mk' slist =
99      let val unencoded = foldl foldthis [] slist
100      in
101        (mk unencoded, unencoded)
102      end
103  fun store s = let
104    val (data, _) = mk' [s]
105  in
106    LoadableThyData.write_data_update {thydataty = ty, data = data}
107  end
108
109  val _ = data_map := Binarymap.insert(!data_map,ty,(dest,store,NONE))
110in
111  (mk',dest)
112end
113
114fun theory_data {settype = key, thy} =
115    case Binarymap.peek(!data_map, key) of
116      NONE => raise mk_HOL_ERR "ThmSetData" "theory_data"
117                    ("No ThmSetData with name "^Lib.quote key)
118    | SOME (df,_,_) => let
119        open LoadableThyData
120      in
121        case segment_data {thy = thy, thydataty = key} of
122          NONE => []
123        | SOME d => valOf (df d)
124                    handle Option =>
125                    raise mk_HOL_ERR "ThmSetData" "theory_data"
126                          ("ThmSetData for name " ^ Lib.quote key ^
127                           " doesn't decode")
128      end
129
130fun current_data s = theory_data { settype = s, thy = current_theory() }
131
132fun all_data s = map (fn thy => (thy, theory_data {settype = s, thy = thy}))
133                     (current_theory() :: ancestry "-")
134
135fun new_exporter name addfn = let
136  val (mk,dest) = new name
137  open LoadableThyData TheoryDelta
138  fun onload thyname =
139      case segment_data {thy = thyname, thydataty = name} of
140        NONE => ()
141      | SOME d => let
142          val thms = valOf (dest d)
143        in
144          addfn thyname thms
145        end
146  fun revise_data P td =
147      case segment_data {thy = current_theory(), thydataty = name} of
148        NONE => ()
149      | SOME d => let
150          val alist = valOf (dest d)
151          val (ok,notok) = Lib.partition P alist
152        in
153          case notok of
154            [] => ()
155          | _ => (HOL_WARNING
156                      "ThmSetData" "revise_data"
157                      ("\n  Theorems in set " ^ Lib.quote name ^
158                       ":\n    " ^ String.concatWith ", " (map #1 notok) ^
159                       "\n  invalidated by " ^ TheoryDelta.toString td);
160                  set_theory_data {thydataty = name,
161                                   data = #1 (mk (map #1 ok))})
162        end
163
164  fun hook (TheoryLoaded s) = onload s
165    | hook (td as DelConstant _) = revise_data (uptodate_thm o #2) td
166    | hook (td as DelTypeOp _) = revise_data (uptodate_thm o #2) td
167    | hook (td as NewConstant _) = revise_data (uptodate_thm o #2) td
168    | hook (td as NewTypeOp _) = revise_data (uptodate_thm o #2) td
169    | hook (td as DelBinding s) = revise_data (not o equal s o #1) td
170    | hook _ = ()
171  fun export s = let
172    val (data, namedthms) = mk [s]
173  in
174    addfn (current_theory()) namedthms;
175    write_data_update {thydataty = name, data = data}
176  end
177  val store = #2 (Binarymap.find(!data_map,name))
178in
179  data_map := Binarymap.insert(!data_map,name,(dest,store,SOME addfn));
180  register_hook ("ThmSetData.onload." ^ name, hook);
181  List.app onload (ancestry "-");
182  {export = export, mk = mk, dest = dest}
183end
184
185fun new_storage_attribute s = let
186in
187  new_exporter s (fn _ => fn _ => ());
188  Theory.adjoin_to_theory {
189    sig_ps = NONE,
190    struct_ps = SOME
191      (fn _ =>
192          PP.add_string
193                 ("val _ = ThmSetData.new_exporter "^Lib.mlquote s^
194                  " (fn _ => fn _ => ())\n"))
195  }
196end
197
198fun store_attribute {attribute, thm_name} =
199    case data_storefn attribute of
200        NONE => raise mk_HOL_ERR "ThmSetData" "store_attribute"
201                      ("Unknown attribute: "^attribute)
202      | SOME f => f thm_name
203
204end (* struct *)
205