1 (* Title: src/Tools/isac/Know_Store.thy |
1 (* Title: src/Tools/isac/Know_Store.thy |
2 Author: Mathias Lehnfeld |
2 Author: Mathias Lehnfeld |
|
3 |
|
4 Calc work on Problem employing Method; both are collected in a respective Store; |
|
5 The collections' structure is independent from the dependency graph of Isabelle's theories |
|
6 in Knowledge. |
|
7 Store is also used by Thy_Html, required for Isac's Java front end, irrelevant for PIDE. |
3 |
8 |
4 The files (in "xxxxx-def.sml") contain definitions required for Know_Store; |
9 The files (in "xxxxx-def.sml") contain definitions required for Know_Store; |
5 they also include minimal code required for other "xxxxx-def.sml" files. |
10 they also include minimal code required for other "xxxxx-def.sml" files. |
6 These files have companion files "xxxxx.sml" with all further code, |
11 These files have companion files "xxxxx.sml" with all further code, |
7 located at appropriate positions in the file structure. |
12 located at appropriate positions in the file structure. |
65 val add_cas: Celem7.cas_elem list -> theory -> theory |
70 val add_cas: Celem7.cas_elem list -> theory -> theory |
66 val get_ptyps: theory -> Celem5.ptyps |
71 val get_ptyps: theory -> Celem5.ptyps |
67 val add_pbts: (Celem5.pbt * Celem3.pblID) list -> theory -> theory |
72 val add_pbts: (Celem5.pbt * Celem3.pblID) list -> theory -> theory |
68 val get_mets: theory -> Celem6.mets |
73 val get_mets: theory -> Celem6.mets |
69 val add_mets: (Celem6.met * Celem3.metID) list -> theory -> theory |
74 val add_mets: (Celem6.met * Celem3.metID) list -> theory -> theory |
70 val get_thes: theory -> (Celem8.thydata Celem1.ptyp) list |
75 val get_thes: theory -> (Celem8.thydata Store.ptyp) list |
71 val add_thes: (Celem8.thydata * Celem8.theID) list -> theory -> theory (* thydata dropped at existing elems *) |
76 val add_thes: (Celem8.thydata * Celem8.theID) list -> theory -> theory (* thydata dropped at existing elems *) |
72 val insert_fillpats: (Celem8.theID * Error_Fill_Def.fillpat list) list -> theory -> theory |
77 val insert_fillpats: (Celem8.theID * Error_Fill_Def.fillpat list) list -> theory -> theory |
73 val get_ref_thy: unit -> theory |
78 val get_ref_thy: unit -> theory |
74 val set_ref_thy: theory -> unit |
79 val set_ref_thy: theory -> unit |
75 end; |
80 end; |
107 |
112 |
108 structure Data = Theory_Data ( |
113 structure Data = Theory_Data ( |
109 type T = Celem5.ptyps; |
114 type T = Celem5.ptyps; |
110 val empty = [Celem5.e_Ptyp]; |
115 val empty = [Celem5.e_Ptyp]; |
111 val extend = I; |
116 val extend = I; |
112 val merge = Celem1.merge_ptyps; |
117 val merge = Store.merge_ptyps; |
113 ); |
118 ); |
114 fun get_ptyps thy = Data.get thy; |
119 fun get_ptyps thy = Data.get thy; |
115 fun add_pbts pbts thy = let |
120 fun add_pbts pbts thy = let |
116 fun add_pbt (pbt as {guh,...}, pblID) = |
121 fun add_pbt (pbt as {guh,...}, pblID) = |
117 (* the pblID has the leaf-element as first; better readability achieved *) |
122 (* the pblID has the leaf-element as first; better readability achieved *) |
118 (if (!Celem91.check_guhs_unique) then Celem91.check_pblguh_unique guh (Data.get thy) else (); |
123 (if (!Celem91.check_guhs_unique) then Celem91.check_pblguh_unique guh (Data.get thy) else (); |
119 rev pblID |> Celem1.insrt pblID pbt); |
124 rev pblID |> Store.insrt pblID pbt); |
120 in Data.map (fold add_pbt pbts) thy end; |
125 in Data.map (fold add_pbt pbts) thy end; |
121 |
126 |
122 structure Data = Theory_Data ( |
127 structure Data = Theory_Data ( |
123 type T = Celem6.mets; |
128 type T = Celem6.mets; |
124 val empty = [Celem6.e_Mets]; |
129 val empty = [Celem6.e_Mets]; |
125 val extend = I; |
130 val extend = I; |
126 val merge = Celem1.merge_ptyps; |
131 val merge = Store.merge_ptyps; |
127 ); |
132 ); |
128 val get_mets = Data.get; |
133 val get_mets = Data.get; |
129 fun add_mets mets thy = let |
134 fun add_mets mets thy = let |
130 fun add_met (met as {guh,...}, metID) = |
135 fun add_met (met as {guh,...}, metID) = |
131 (if (!Celem91.check_guhs_unique) then Celem91.check_metguh_unique guh (Data.get thy) else (); |
136 (if (!Celem91.check_guhs_unique) then Celem91.check_metguh_unique guh (Data.get thy) else (); |
132 Celem1.insrt metID met metID); |
137 Store.insrt metID met metID); |
133 in Data.map (fold add_met mets) thy end; |
138 in Data.map (fold add_met mets) thy end; |
134 |
139 |
135 structure Data = Theory_Data ( |
140 structure Data = Theory_Data ( |
136 type T = (Celem8.thydata Celem1.ptyp) list; |
141 type T = (Celem8.thydata Store.ptyp) list; |
137 val empty = []; |
142 val empty = []; |
138 val extend = I; |
143 val extend = I; |
139 val merge = Celem1.merge_ptyps; (* relevant for store_thm, store_rls *) |
144 val merge = Store.merge_ptyps; (* relevant for store_thm, store_rls *) |
140 ); |
145 ); |
141 fun get_thes thy = Data.get thy |
146 fun get_thes thy = Data.get thy |
142 fun add_thes thes thy = let |
147 fun add_thes thes thy = let |
143 fun add_the (thydata, theID) = Celem8.add_thydata ([], theID) thydata |
148 fun add_the (thydata, theID) = Celem8.add_thydata ([], theID) thydata |
144 in Data.map (fold add_the thes) thy end; |
149 in Data.map (fold add_the thes) thy end; |
145 fun insert_fillpats fis thy = |
150 fun insert_fillpats fis thy = |
146 let |
151 let |
147 fun update_elem (theID, fillpats) = |
152 fun update_elem (theID, fillpats) = |
148 let |
153 let |
149 val hthm = Celem1.get_py (Data.get thy) theID theID |
154 val hthm = Store.get_py (Data.get thy) theID theID |
150 val hthm' = Celem8.update_hthm hthm fillpats |
155 val hthm' = Celem8.update_hthm hthm fillpats |
151 handle ERROR _ => |
156 handle ERROR _ => |
152 error ("insert_fillpats: " ^ strs2str theID ^ "must address a theorem") |
157 error ("insert_fillpats: " ^ strs2str theID ^ "must address a theorem") |
153 in Celem1.update_ptyps theID theID hthm' end |
158 in Store.update_ptyps theID theID hthm' end |
154 in Data.map (fold update_elem fis) thy end |
159 in Data.map (fold update_elem fis) thy end |
155 |
160 |
156 val cur_thy = Synchronized.var "finally_knowledge_complete" @{theory}; |
161 val cur_thy = Synchronized.var "finally_knowledge_complete" @{theory}; |
157 fun set_ref_thy thy = Synchronized.change cur_thy (fn _ => thy); (* never RE-set ! *) |
162 fun set_ref_thy thy = Synchronized.change cur_thy (fn _ => thy); (* never RE-set ! *) |
158 fun get_ref_thy () = Synchronized.value cur_thy; |
163 fun get_ref_thy () = Synchronized.value cur_thy; |
233 fun check_kestore_cas ((t, (s, _)) : Celem7.cas_elem) = |
238 fun check_kestore_cas ((t, (s, _)) : Celem7.cas_elem) = |
234 "(" ^ (Print_Mode.setmp [] (Syntax.string_of_term (Config.put show_markup false |
239 "(" ^ (Print_Mode.setmp [] (Syntax.string_of_term (Config.put show_markup false |
235 (Proof_Context.init_global @{theory})))) t ^ ", " ^ Celem3.spec2str s ^ ")"; |
240 (Proof_Context.init_global @{theory})))) t ^ ", " ^ Celem3.spec2str s ^ ")"; |
236 |
241 |
237 fun count_kestore_ptyps [] = 0 |
242 fun count_kestore_ptyps [] = 0 |
238 | count_kestore_ptyps ((Celem1.Ptyp (_, _, ps)) :: ps') = |
243 | count_kestore_ptyps ((Store.Ptyp (_, _, ps)) :: ps') = |
239 1 + count_kestore_ptyps ps + count_kestore_ptyps ps'; |
244 1 + count_kestore_ptyps ps + count_kestore_ptyps ps'; |
240 fun check_kestore_ptyp' strfun (Celem1.Ptyp (key, pbts, pts)) = "Ptyp (" ^ (quote key) ^ ", " ^ |
245 fun check_kestore_ptyp' strfun (Store.Ptyp (key, pbts, pts)) = "Ptyp (" ^ (quote key) ^ ", " ^ |
241 (strfun pbts) ^ ", " ^ (map (check_kestore_ptyp' strfun) pts |> list2str) ^ ")" |> linefeed; |
246 (strfun pbts) ^ ", " ^ (map (check_kestore_ptyp' strfun) pts |> list2str) ^ ")" |> linefeed; |
242 val check_kestore_ptyp = check_kestore_ptyp' Celem5.pbts2str; |
247 val check_kestore_ptyp = check_kestore_ptyp' Celem5.pbts2str; |
243 fun ptyp_ord ((Celem1.Ptyp (s1, _, _)), (Celem1.Ptyp (s2, _, _))) = string_ord (s1, s2); |
248 fun ptyp_ord ((Store.Ptyp (s1, _, _)), (Store.Ptyp (s2, _, _))) = string_ord (s1, s2); |
244 fun pbt_ord ({guh = guh'1, ...} : Celem5.pbt, {guh = guh'2, ...} : Celem5.pbt) = string_ord (guh'1, guh'2); |
249 fun pbt_ord ({guh = guh'1, ...} : Celem5.pbt, {guh = guh'2, ...} : Celem5.pbt) = string_ord (guh'1, guh'2); |
245 fun sort_kestore_ptyp' _ [] = [] |
250 fun sort_kestore_ptyp' _ [] = [] |
246 | sort_kestore_ptyp' ordfun ((Celem1.Ptyp (key, pbts, ps)) :: ps') = |
251 | sort_kestore_ptyp' ordfun ((Store.Ptyp (key, pbts, ps)) :: ps') = |
247 ((Celem1.Ptyp (key, sort ordfun pbts, sort_kestore_ptyp' ordfun ps |> sort ptyp_ord)) |
252 ((Store.Ptyp (key, sort ordfun pbts, sort_kestore_ptyp' ordfun ps |> sort ptyp_ord)) |
248 :: sort_kestore_ptyp' ordfun ps'); |
253 :: sort_kestore_ptyp' ordfun ps'); |
249 val sort_kestore_ptyp = sort_kestore_ptyp' pbt_ord; |
254 val sort_kestore_ptyp = sort_kestore_ptyp' pbt_ord; |
250 |
255 |
251 fun metguh2str ({guh,...} : Celem6.met) = guh : string; |
256 fun metguh2str ({guh,...} : Celem6.met) = guh : string; |
252 fun check_kestore_met (mp: Celem6.met Celem1.ptyp) = |
257 fun check_kestore_met (mp: Celem6.met Store.ptyp) = |
253 check_kestore_ptyp' (fn xs => map metguh2str xs |> strs2str) mp; |
258 check_kestore_ptyp' (fn xs => map metguh2str xs |> strs2str) mp; |
254 fun met_ord ({guh = guh'1, ...} : Celem6.met, {guh = guh'2, ...} : Celem6.met) = string_ord (guh'1, guh'2); |
259 fun met_ord ({guh = guh'1, ...} : Celem6.met, {guh = guh'2, ...} : Celem6.met) = string_ord (guh'1, guh'2); |
255 val sort_kestore_met = sort_kestore_ptyp' met_ord; |
260 val sort_kestore_met = sort_kestore_ptyp' met_ord; |
256 |
261 |
257 fun check_kestore_thes thes = ((map writeln) o (map (check_kestore_ptyp' Celem8.thes2str))) thes |
262 fun check_kestore_thes thes = ((map writeln) o (map (check_kestore_ptyp' Celem8.thes2str))) thes |