67 val add_cas: CAS_Def.T list -> theory -> theory |
67 val add_cas: CAS_Def.T list -> theory -> theory |
68 val get_ptyps: theory -> Probl_Def.store |
68 val get_ptyps: theory -> Probl_Def.store |
69 val add_pbts: (Probl_Def.T * Spec.pblID) list -> theory -> theory |
69 val add_pbts: (Probl_Def.T * Spec.pblID) list -> theory -> theory |
70 val get_mets: theory -> Meth_Def.store |
70 val get_mets: theory -> Meth_Def.store |
71 val add_mets: (Meth_Def.T * Spec.metID) list -> theory -> theory |
71 val add_mets: (Meth_Def.T * Spec.metID) list -> theory -> theory |
72 val get_thes: theory -> (Thy_Html.thydata Store.ptyp) list |
72 val get_thes: theory -> (Thy_Html.thydata Store.node) list |
73 val add_thes: (Thy_Html.thydata * Thy_Html.theID) list -> theory -> theory (* thydata dropped at existing elems *) |
73 val add_thes: (Thy_Html.thydata * Thy_Html.theID) list -> theory -> theory (* thydata dropped at existing elems *) |
74 val insert_fillpats: (Thy_Html.theID * Error_Fill_Def.fillpat list) list -> theory -> theory |
74 val insert_fillpats: (Thy_Html.theID * Error_Fill_Def.fillpat list) list -> theory -> theory |
75 val get_ref_thy: unit -> theory |
75 val get_ref_thy: unit -> theory |
76 val set_ref_thy: theory -> unit |
76 val set_ref_thy: theory -> unit |
77 end; |
77 end; |
109 |
109 |
110 structure Data = Theory_Data ( |
110 structure Data = Theory_Data ( |
111 type T = Probl_Def.store; |
111 type T = Probl_Def.store; |
112 val empty = [Probl_Def.empty_store]; |
112 val empty = [Probl_Def.empty_store]; |
113 val extend = I; |
113 val extend = I; |
114 val merge = Store.merge_ptyps; |
114 val merge = Store.merge; |
115 ); |
115 ); |
116 fun get_ptyps thy = Data.get thy; |
116 fun get_ptyps thy = Data.get thy; |
117 fun add_pbts pbts thy = let |
117 fun add_pbts pbts thy = let |
118 fun add_pbt (pbt as {guh,...}, pblID) = |
118 fun add_pbt (pbt as {guh,...}, pblID) = |
119 (* the pblID has the leaf-element as first; better readability achieved *) |
119 (* the pblID has the leaf-element as first; better readability achieved *) |
120 (if (!Check_Unique.check_guhs_unique) then Probl_Def.check_unique guh (Data.get thy) else (); |
120 (if (!Check_Unique.check_guhs_unique) then Probl_Def.check_unique guh (Data.get thy) else (); |
121 rev pblID |> Store.insrt pblID pbt); |
121 rev pblID |> Store.insert pblID pbt); |
122 in Data.map (fold add_pbt pbts) thy end; |
122 in Data.map (fold add_pbt pbts) thy end; |
123 |
123 |
124 structure Data = Theory_Data ( |
124 structure Data = Theory_Data ( |
125 type T = Meth_Def.store; |
125 type T = Meth_Def.store; |
126 val empty = [Meth_Def.empty_store]; |
126 val empty = [Meth_Def.empty_store]; |
127 val extend = I; |
127 val extend = I; |
128 val merge = Store.merge_ptyps; |
128 val merge = Store.merge; |
129 ); |
129 ); |
130 val get_mets = Data.get; |
130 val get_mets = Data.get; |
131 fun add_mets mets thy = let |
131 fun add_mets mets thy = let |
132 fun add_met (met as {guh,...}, metID) = |
132 fun add_met (met as {guh,...}, metID) = |
133 (if (!Check_Unique.check_guhs_unique) then Meth_Def.check_unique guh (Data.get thy) else (); |
133 (if (!Check_Unique.check_guhs_unique) then Meth_Def.check_unique guh (Data.get thy) else (); |
134 Store.insrt metID met metID); |
134 Store.insert metID met metID); |
135 in Data.map (fold add_met mets) thy end; |
135 in Data.map (fold add_met mets) thy end; |
136 |
136 |
137 structure Data = Theory_Data ( |
137 structure Data = Theory_Data ( |
138 type T = (Thy_Html.thydata Store.ptyp) list; |
138 type T = (Thy_Html.thydata Store.node) list; |
139 val empty = []; |
139 val empty = []; |
140 val extend = I; |
140 val extend = I; |
141 val merge = Store.merge_ptyps; (* relevant for store_thm, store_rls *) |
141 val merge = Store.merge; (* relevant for store_thm, store_rls *) |
142 ); |
142 ); |
143 fun get_thes thy = Data.get thy |
143 fun get_thes thy = Data.get thy |
144 fun add_thes thes thy = let |
144 fun add_thes thes thy = let |
145 fun add_the (thydata, theID) = Thy_Html.add_thydata ([], theID) thydata |
145 fun add_the (thydata, theID) = Thy_Html.add_thydata ([], theID) thydata |
146 in Data.map (fold add_the thes) thy end; |
146 in Data.map (fold add_the thes) thy end; |
147 fun insert_fillpats fis thy = |
147 fun insert_fillpats fis thy = |
148 let |
148 let |
149 fun update_elem (theID, fillpats) = |
149 fun update_elem (theID, fillpats) = |
150 let |
150 let |
151 val hthm = Store.get_py (Data.get thy) theID theID |
151 val hthm = Store.get (Data.get thy) theID theID |
152 val hthm' = Thy_Html.update_hthm hthm fillpats |
152 val hthm' = Thy_Html.update_hthm hthm fillpats |
153 handle ERROR _ => |
153 handle ERROR _ => |
154 error ("insert_fillpats: " ^ strs2str theID ^ "must address a theorem") |
154 error ("insert_fillpats: " ^ strs2str theID ^ "must address a theorem") |
155 in Store.update_ptyps theID theID hthm' end |
155 in Store.update theID theID hthm' end |
156 in Data.map (fold update_elem fis) thy end |
156 in Data.map (fold update_elem fis) thy end |
157 |
157 |
158 val cur_thy = Synchronized.var "finally_knowledge_complete" @{theory}; |
158 val cur_thy = Synchronized.var "finally_knowledge_complete" @{theory}; |
159 fun set_ref_thy thy = Synchronized.change cur_thy (fn _ => thy); (* never RE-set ! *) |
159 fun set_ref_thy thy = Synchronized.change cur_thy (fn _ => thy); (* never RE-set ! *) |
160 fun get_ref_thy () = Synchronized.value cur_thy; |
160 fun get_ref_thy () = Synchronized.value cur_thy; |
235 fun check_kestore_cas ((t, (s, _)) : CAS_Def.T) = |
235 fun check_kestore_cas ((t, (s, _)) : CAS_Def.T) = |
236 "(" ^ (Print_Mode.setmp [] (Syntax.string_of_term (Config.put show_markup false |
236 "(" ^ (Print_Mode.setmp [] (Syntax.string_of_term (Config.put show_markup false |
237 (Proof_Context.init_global @{theory})))) t ^ ", " ^ Spec.spec2str s ^ ")"; |
237 (Proof_Context.init_global @{theory})))) t ^ ", " ^ Spec.spec2str s ^ ")"; |
238 |
238 |
239 fun count_kestore_ptyps [] = 0 |
239 fun count_kestore_ptyps [] = 0 |
240 | count_kestore_ptyps ((Store.Ptyp (_, _, ps)) :: ps') = |
240 | count_kestore_ptyps ((Store.Node (_, _, ps)) :: ps') = |
241 1 + count_kestore_ptyps ps + count_kestore_ptyps ps'; |
241 1 + count_kestore_ptyps ps + count_kestore_ptyps ps'; |
242 fun check_kestore_ptyp' strfun (Store.Ptyp (key, pbts, pts)) = "Ptyp (" ^ (quote key) ^ ", " ^ |
242 fun check_kestore_ptyp' strfun (Store.Node (key, pbts, pts)) = "Ptyp (" ^ (quote key) ^ ", " ^ |
243 (strfun pbts) ^ ", " ^ (map (check_kestore_ptyp' strfun) pts |> list2str) ^ ")" |> linefeed; |
243 (strfun pbts) ^ ", " ^ (map (check_kestore_ptyp' strfun) pts |> list2str) ^ ")" |> linefeed; |
244 val check_kestore_ptyp = check_kestore_ptyp' Probl_Def.s_to_string; |
244 val check_kestore_ptyp = check_kestore_ptyp' Probl_Def.s_to_string; |
245 fun ptyp_ord ((Store.Ptyp (s1, _, _)), (Store.Ptyp (s2, _, _))) = string_ord (s1, s2); |
245 fun ptyp_ord ((Store.Node (s1, _, _)), (Store.Node (s2, _, _))) = string_ord (s1, s2); |
246 fun pbt_ord ({guh = guh'1, ...} : Probl_Def.T, {guh = guh'2, ...} : Probl_Def.T) = string_ord (guh'1, guh'2); |
246 fun pbt_ord ({guh = guh'1, ...} : Probl_Def.T, {guh = guh'2, ...} : Probl_Def.T) = string_ord (guh'1, guh'2); |
247 fun sort_kestore_ptyp' _ [] = [] |
247 fun sort_kestore_ptyp' _ [] = [] |
248 | sort_kestore_ptyp' ordfun ((Store.Ptyp (key, pbts, ps)) :: ps') = |
248 | sort_kestore_ptyp' ordfun ((Store.Node (key, pbts, ps)) :: ps') = |
249 ((Store.Ptyp (key, sort ordfun pbts, sort_kestore_ptyp' ordfun ps |> sort ptyp_ord)) |
249 ((Store.Node (key, sort ordfun pbts, sort_kestore_ptyp' ordfun ps |> sort ptyp_ord)) |
250 :: sort_kestore_ptyp' ordfun ps'); |
250 :: sort_kestore_ptyp' ordfun ps'); |
251 val sort_kestore_ptyp = sort_kestore_ptyp' pbt_ord; |
251 val sort_kestore_ptyp = sort_kestore_ptyp' pbt_ord; |
252 |
252 |
253 fun metguh2str ({guh,...} : Meth_Def.T) = guh : string; |
253 fun metguh2str ({guh,...} : Meth_Def.T) = guh : string; |
254 fun check_kestore_met (mp: Meth_Def.T Store.ptyp) = |
254 fun check_kestore_met (mp: Meth_Def.T Store.node) = |
255 check_kestore_ptyp' (fn xs => map metguh2str xs |> strs2str) mp; |
255 check_kestore_ptyp' (fn xs => map metguh2str xs |> strs2str) mp; |
256 fun met_ord ({guh = guh'1, ...} : Meth_Def.T, {guh = guh'2, ...} : Meth_Def.T) = string_ord (guh'1, guh'2); |
256 fun met_ord ({guh = guh'1, ...} : Meth_Def.T, {guh = guh'2, ...} : Meth_Def.T) = string_ord (guh'1, guh'2); |
257 val sort_kestore_met = sort_kestore_ptyp' met_ord; |
257 val sort_kestore_met = sort_kestore_ptyp' met_ord; |
258 |
258 |
259 fun check_kestore_thes thes = ((map writeln) o (map (check_kestore_ptyp' Thy_Html.thes2str))) thes |
259 fun check_kestore_thes thes = ((map writeln) o (map (check_kestore_ptyp' Thy_Html.thes2str))) thes |