21 of them are implemented in "ProgLang/" already; thus "KEStore.thy" got this |
46 of them are implemented in "ProgLang/" already; thus "KEStore.thy" got this |
22 location in the directory structure. |
47 location in the directory structure. |
23 *) |
48 *) |
24 signature KESTORE_ELEMS = |
49 signature KESTORE_ELEMS = |
25 sig |
50 sig |
26 val get_rlss: theory -> (rls' * (theory' * rls)) list |
51 val get_rlss: theory -> (Celem.rls' * (Celem.theory' * Celem.rls)) list |
27 val add_rlss: (rls' * (theory' * rls)) list -> theory -> theory |
52 val add_rlss: (Celem.rls' * (Celem.theory' * Celem.rls)) list -> theory -> theory |
28 val get_calcs: theory -> (prog_calcID * (calID * eval_fn)) list |
53 val get_calcs: theory -> (Celem.prog_calcID * (Celem.calID * Celem.eval_fn)) list |
29 val add_calcs: (prog_calcID * (calID * eval_fn)) list -> theory -> theory |
54 val add_calcs: (Celem.prog_calcID * (Celem.calID * Celem.eval_fn)) list -> theory -> theory |
30 val get_cas: theory -> cas_elem list |
55 val get_cas: theory -> Celem.cas_elem list |
31 val add_cas: cas_elem list -> theory -> theory |
56 val add_cas: Celem.cas_elem list -> theory -> theory |
32 val get_ptyps: theory -> ptyps |
57 val get_ptyps: theory -> Celem.ptyps |
33 val add_pbts: (pbt * pblID) list -> theory -> theory |
58 val add_pbts: (Celem.pbt * Celem.pblID) list -> theory -> theory |
34 val get_mets: theory -> mets |
59 val get_mets: theory -> Celem.mets |
35 val add_mets: (met * metID) list -> theory -> theory |
60 val add_mets: (Celem.met * Celem.metID) list -> theory -> theory |
36 val get_thes: theory -> (thydata ptyp) list |
61 val get_thes: theory -> (Celem.thydata Celem.ptyp) list |
37 val add_thes: (thydata * theID) list -> theory -> theory (* thydata dropped at existing elems *) |
62 val add_thes: (Celem.thydata * Celem.theID) list -> theory -> theory (* thydata dropped at existing elems *) |
38 val insert_fillpats: (theID * fillpat list) list -> theory -> theory |
63 val insert_fillpats: (Celem.theID * Celem.fillpat list) list -> theory -> theory |
39 val get_ref_thy: unit -> theory |
64 val get_ref_thy: unit -> theory |
40 val set_ref_thy: theory -> unit |
65 val set_ref_thy: theory -> unit |
41 end; |
66 end; |
42 |
67 |
43 structure KEStore_Elems: KESTORE_ELEMS = |
68 structure KEStore_Elems: KESTORE_ELEMS = |
44 struct |
69 struct |
45 fun union_overwrite eq l1 l2 = fold (insert eq) l2 (*..swapped..*) l1; |
70 fun union_overwrite eq l1 l2 = fold (insert eq) l2 (*..swapped..*) l1; |
46 |
71 |
47 structure Data = Theory_Data ( |
72 structure Data = Theory_Data ( |
48 type T = (rls' * (theory' * rls)) list; |
73 type T = (Celem.rls' * (Celem.theory' * Celem.rls)) list; |
49 val empty = []; |
74 val empty = []; |
50 val extend = I; |
75 val extend = I; |
51 val merge = merge_rlss; |
76 val merge = Celem.merge_rlss; |
52 ); |
77 ); |
53 fun get_rlss thy = Data.get thy |
78 fun get_rlss thy = Data.get thy |
54 fun add_rlss rlss = Data.map (union_overwrite rls_eq rlss) |
79 fun add_rlss rlss = Data.map (union_overwrite Celem.rls_eq rlss) |
55 |
80 |
56 structure Data = Theory_Data ( |
81 structure Data = Theory_Data ( |
57 type T = (prog_calcID * (calID * eval_fn)) list; |
82 type T = (Celem.prog_calcID * (Celem.calID * Celem.eval_fn)) list; |
58 val empty = []; |
83 val empty = []; |
59 val extend = I; |
84 val extend = I; |
60 val merge = merge calc_eq; |
85 val merge = merge Celem.calc_eq; |
61 ); |
86 ); |
62 fun get_calcs thy = Data.get thy |
87 fun get_calcs thy = Data.get thy |
63 fun add_calcs calcs = Data.map (union_overwrite calc_eq calcs) |
88 fun add_calcs calcs = Data.map (union_overwrite Celem.calc_eq calcs) |
64 |
89 |
65 structure Data = Theory_Data ( |
90 structure Data = Theory_Data ( |
66 type T = (term * (spec * (term list -> (term * term list) list))) list; |
91 type T = (term * (Celem.spec * (term list -> (term * term list) list))) list; |
67 val empty = []; |
92 val empty = []; |
68 val extend = I; |
93 val extend = I; |
69 val merge = merge cas_eq; |
94 val merge = merge Celem.cas_eq; |
70 ); |
95 ); |
71 fun get_cas thy = Data.get thy |
96 fun get_cas thy = Data.get thy |
72 fun add_cas cas = Data.map (union_overwrite cas_eq cas) |
97 fun add_cas cas = Data.map (union_overwrite Celem.cas_eq cas) |
73 |
98 |
74 structure Data = Theory_Data ( |
99 structure Data = Theory_Data ( |
75 type T = ptyps; |
100 type T = Celem.ptyps; |
76 val empty = [e_Ptyp]; |
101 val empty = [Celem.e_Ptyp]; |
77 val extend = I; |
102 val extend = I; |
78 val merge = merge_ptyps; |
103 val merge = Celem.merge_ptyps; |
79 ); |
104 ); |
80 fun get_ptyps thy = Data.get thy; |
105 fun get_ptyps thy = Data.get thy; |
81 fun add_pbts pbts thy = let |
106 fun add_pbts pbts thy = let |
82 fun add_pbt (pbt as {guh,...}, pblID) = |
107 fun add_pbt (pbt as {guh,...}, pblID) = |
83 (* the pblID has the leaf-element as first; better readability achieved *) |
108 (* the pblID has the leaf-element as first; better readability achieved *) |
84 (if (!check_guhs_unique) then check_pblguh_unique guh (Data.get thy) else (); |
109 (if (!Celem.check_guhs_unique) then Celem.check_pblguh_unique guh (Data.get thy) else (); |
85 rev pblID |> insrt pblID pbt); |
110 rev pblID |> Celem.insrt pblID pbt); |
86 in Data.map (fold add_pbt pbts) thy end; |
111 in Data.map (fold add_pbt pbts) thy end; |
87 |
112 |
88 structure Data = Theory_Data ( |
113 structure Data = Theory_Data ( |
89 type T = mets; |
114 type T = Celem.mets; |
90 val empty = [e_Mets]; |
115 val empty = [Celem.e_Mets]; |
91 val extend = I; |
116 val extend = I; |
92 val merge = merge_ptyps; |
117 val merge = Celem.merge_ptyps; |
93 ); |
118 ); |
94 val get_mets = Data.get; |
119 val get_mets = Data.get; |
95 fun add_mets mets thy = let |
120 fun add_mets mets thy = let |
96 fun add_met (met as {guh,...}, metID) = |
121 fun add_met (met as {guh,...}, metID) = |
97 (if (!check_guhs_unique) then check_metguh_unique guh (Data.get thy) else (); |
122 (if (!Celem.check_guhs_unique) then Celem.check_metguh_unique guh (Data.get thy) else (); |
98 insrt metID met metID); |
123 Celem.insrt metID met metID); |
99 in Data.map (fold add_met mets) thy end; |
124 in Data.map (fold add_met mets) thy end; |
100 |
125 |
101 structure Data = Theory_Data ( |
126 structure Data = Theory_Data ( |
102 type T = (thydata ptyp) list; |
127 type T = (Celem.thydata Celem.ptyp) list; |
103 val empty = []; |
128 val empty = []; |
104 val extend = I; |
129 val extend = I; |
105 val merge = merge_ptyps; (* relevant for store_thm, store_rls *) |
130 val merge = Celem.merge_ptyps; (* relevant for store_thm, store_rls *) |
106 ); |
131 ); |
107 fun get_thes thy = Data.get thy |
132 fun get_thes thy = Data.get thy |
108 fun add_thes thes thy = let |
133 fun add_thes thes thy = let |
109 fun add_the (thydata, theID) = add_thydata ([], theID) thydata |
134 fun add_the (thydata, theID) = Celem.add_thydata ([], theID) thydata |
110 in Data.map (fold add_the thes) thy end; |
135 in Data.map (fold add_the thes) thy end; |
111 fun insert_fillpats fis thy = |
136 fun insert_fillpats fis thy = |
112 let |
137 let |
113 fun update_elem (theID, fillpats) = |
138 fun update_elem (theID, fillpats) = |
114 let |
139 let |
115 val hthm = get_py (Data.get thy) theID theID |
140 val hthm = Celem.get_py (Data.get thy) theID theID |
116 val hthm' = update_hthm hthm fillpats |
141 val hthm' = Celem.update_hthm hthm fillpats |
117 handle ERROR _ => |
142 handle ERROR _ => |
118 error ("insert_fillpats: " ^ strs2str theID ^ "must address a theorem") |
143 error ("insert_fillpats: " ^ strs2str theID ^ "must address a theorem") |
119 in update_ptyps theID theID hthm' end |
144 in Celem.update_ptyps theID theID hthm' end |
120 in Data.map (fold update_elem fis) thy end |
145 in Data.map (fold update_elem fis) thy end |
121 |
146 |
122 val cur_thy = Synchronized.var "finally_knowledge_complete" @{theory}; |
147 val cur_thy = Synchronized.var "finally_knowledge_complete" @{theory}; |
123 fun set_ref_thy thy = Synchronized.change cur_thy (fn _ => thy); (* never RE-set ! *) |
148 fun set_ref_thy thy = Synchronized.change cur_thy (fn _ => thy); (* never RE-set ! *) |
124 fun get_ref_thy () = Synchronized.value cur_thy; |
149 fun get_ref_thy () = Synchronized.value cur_thy; |
164 fun get_ptyps () = get_ref_thy () |> KEStore_Elems.get_ptyps; |
189 fun get_ptyps () = get_ref_thy () |> KEStore_Elems.get_ptyps; |
165 fun get_mets () = get_ref_thy () |> KEStore_Elems.get_mets; |
190 fun get_mets () = get_ref_thy () |> KEStore_Elems.get_mets; |
166 fun get_thes () = get_ref_thy () |> KEStore_Elems.get_thes; |
191 fun get_thes () = get_ref_thy () |> KEStore_Elems.get_thes; |
167 *} |
192 *} |
168 setup {* KEStore_Elems.add_rlss |
193 setup {* KEStore_Elems.add_rlss |
169 [("e_rls", (Context.theory_name @{theory}, e_rls)), |
194 [("e_rls", (Context.theory_name @{theory}, Celem.e_rls)), |
170 ("e_rrls", (Context.theory_name @{theory}, e_rrls))] *} |
195 ("e_rrls", (Context.theory_name @{theory}, Celem.e_rrls))] *} |
171 |
196 |
172 section {* determine sequence of main parts in thehier *} |
197 section {* determine sequence of main parts in thehier *} |
173 setup {* |
198 setup {* |
174 KEStore_Elems.add_thes |
199 KEStore_Elems.add_thes |
175 [(Html {guh = part2guh ["IsacKnowledge"], html = "", |
200 [(Celem.Html {guh = Celem.part2guh ["IsacKnowledge"], html = "", |
176 mathauthors = ["Isac team"], coursedesign = []}, ["IsacKnowledge"]), |
201 mathauthors = ["Isac team"], coursedesign = []}, ["IsacKnowledge"]), |
177 (Html {guh = part2guh ["Isabelle"], html = "", |
202 (Celem.Html {guh = Celem.part2guh ["Isabelle"], html = "", |
178 mathauthors = ["Isabelle team, TU Munich"], coursedesign = []}, ["Isabelle"]), |
203 mathauthors = ["Isabelle team, TU Munich"], coursedesign = []}, ["Isabelle"]), |
179 (Html {guh = part2guh ["IsacScripts"], html = "", |
204 (Celem.Html {guh = Celem.part2guh ["IsacScripts"], html = "", |
180 mathauthors = ["Isac team"], coursedesign = []}, ["IsacScripts"])] |
205 mathauthors = ["Isac team"], coursedesign = []}, ["IsacScripts"])] |
181 *} |
206 *} |
182 |
207 |
183 section {* Functions for checking KEStore_Elems *} |
208 section {* Functions for checking KEStore_Elems *} |
184 ML {* |
209 ML {* |
185 fun short_string_of_rls Erls = "Erls" |
210 fun short_string_of_rls Erls = "Erls" |
186 | short_string_of_rls (Rls {calc, rules, ...}) = |
211 (* |
|
212 | short_string_of_rls (Celem.Rls {calc, rules, ...}) = |
187 "Rls {#calc = " ^ string_of_int (length calc) ^ |
213 "Rls {#calc = " ^ string_of_int (length calc) ^ |
188 ", #rules = " ^ string_of_int (length rules) ^ ", ..." |
214 ", #rules = " ^ string_of_int (length rules) ^ ", ..." |
189 | short_string_of_rls (Seq {calc, rules, ...}) = |
215 | short_string_of_rls (Celem.Seq {calc, rules, ...}) = |
190 "Seq {#calc = " ^ string_of_int (length calc) ^ |
216 "Seq {#calc = " ^ string_of_int (length calc) ^ |
191 ", #rules = " ^ string_of_int (length rules) ^ ", ..." |
217 ", #rules = " ^ string_of_int (length rules) ^ ", ..." |
192 | short_string_of_rls (Rrls _) = "Rrls {...}"; |
218 | short_string_of_rls (Celem.Rrls _) = "Rrls {...}"; |
193 |
219 *) |
194 fun check_kestore_rls (rls', (thyID, rls)) = |
220 fun check_kestore_rls (rls', (thyID, rls)) = |
195 "(" ^ rls' ^ ", (" ^ thyID ^ ", " ^ short_string_of_rls rls ^ "))"; |
221 "(" ^ rls' ^ ", (" ^ thyID ^ ", " ^ short_string_of_rls rls ^ "))"; |
196 |
222 |
197 fun check_kestore_calc ((id, (c, _)) : calc) = "(" ^ id ^ ", (" ^ c ^ ", fn))"; |
223 fun check_kestore_calc ((id, (c, _)) : Celem.calc) = "(" ^ id ^ ", (" ^ c ^ ", fn))"; |
198 |
224 |
199 fun check_kestore_cas ((t, (s, _)):cas_elem) = |
225 fun check_kestore_cas ((t, (s, _)) : Celem.cas_elem) = |
200 "(" ^ (term_to_string''' @{theory} t) ^ ", " ^ (spec2str s) ^ ")"; |
226 "(" ^ (Celem.term_to_string''' @{theory} t) ^ ", " ^ (Celem.spec2str s) ^ ")"; |
201 |
227 |
202 fun count_kestore_ptyps [] = 0 |
228 fun count_kestore_ptyps [] = 0 |
203 | count_kestore_ptyps ((Ptyp (_, _, ps)) :: ps') = |
229 | count_kestore_ptyps ((Celem.Ptyp (_, _, ps)) :: ps') = |
204 1 + count_kestore_ptyps ps + count_kestore_ptyps ps'; |
230 1 + count_kestore_ptyps ps + count_kestore_ptyps ps'; |
205 fun check_kestore_ptyp' strfun (Ptyp (key, pbts, pts)) = "Ptyp (" ^ (quote key) ^ ", " ^ |
231 fun check_kestore_ptyp' strfun (Celem.Ptyp (key, pbts, pts)) = "Ptyp (" ^ (quote key) ^ ", " ^ |
206 (strfun pbts) ^ ", " ^ (map (check_kestore_ptyp' strfun) pts |> list2str) ^ ")" |> linefeed; |
232 (strfun pbts) ^ ", " ^ (map (check_kestore_ptyp' strfun) pts |> list2str) ^ ")" |> Celem.linefeed; |
207 val check_kestore_ptyp = check_kestore_ptyp' pbts2str; |
233 val check_kestore_ptyp = check_kestore_ptyp' Celem.pbts2str; |
208 fun ptyp_ord ((Ptyp (s1, _, _)), (Ptyp (s2, _, _))) = string_ord (s1, s2); |
234 fun ptyp_ord ((Celem.Ptyp (s1, _, _)), (Celem.Ptyp (s2, _, _))) = string_ord (s1, s2); |
209 fun pbt_ord ({guh = guh'1, ...} : pbt, {guh = guh'2, ...} : pbt) = string_ord (guh'1, guh'2); |
235 fun pbt_ord ({guh = guh'1, ...} : Celem.pbt, {guh = guh'2, ...} : Celem.pbt) = string_ord (guh'1, guh'2); |
210 fun sort_kestore_ptyp' _ [] = [] |
236 fun sort_kestore_ptyp' _ [] = [] |
211 | sort_kestore_ptyp' ordfun ((Ptyp (key, pbts, ps)) :: ps') = |
237 | sort_kestore_ptyp' ordfun ((Celem.Ptyp (key, pbts, ps)) :: ps') = |
212 ((Ptyp (key, sort ordfun pbts, sort_kestore_ptyp' ordfun ps |> sort ptyp_ord)) |
238 ((Celem.Ptyp (key, sort ordfun pbts, sort_kestore_ptyp' ordfun ps |> sort ptyp_ord)) |
213 :: sort_kestore_ptyp' ordfun ps'); |
239 :: sort_kestore_ptyp' ordfun ps'); |
214 val sort_kestore_ptyp = sort_kestore_ptyp' pbt_ord; |
240 val sort_kestore_ptyp = sort_kestore_ptyp' pbt_ord; |
215 |
241 |
216 fun metguh2str ({guh,...}:met) = guh : string; |
242 fun metguh2str ({guh,...} : Celem.met) = guh : string; |
217 fun check_kestore_met (mp:met ptyp) = |
243 fun check_kestore_met (mp: Celem.met Celem.ptyp) = |
218 check_kestore_ptyp' (fn xs => map metguh2str xs |> strs2str) mp; |
244 check_kestore_ptyp' (fn xs => map metguh2str xs |> strs2str) mp; |
219 fun met_ord ({guh = guh'1, ...} : met, {guh = guh'2, ...} : met) = string_ord (guh'1, guh'2); |
245 fun met_ord ({guh = guh'1, ...} : Celem.met, {guh = guh'2, ...} : Celem.met) = string_ord (guh'1, guh'2); |
220 val sort_kestore_met = sort_kestore_ptyp' met_ord; |
246 val sort_kestore_met = sort_kestore_ptyp' met_ord; |
221 |
247 |
222 fun check_kestore_thes thes = ((map writeln) o (map (check_kestore_ptyp' thes2str))) thes |
248 fun check_kestore_thes thes = ((map writeln) o (map (check_kestore_ptyp' Celem.thes2str))) thes |
223 fun write_thes thydata_list = |
249 fun write_thes thydata_list = |
224 thydata_list |
250 thydata_list |
225 |> map (fn (id, the) => (theID2str id, the2str the)) |
251 |> map (fn (id, the) => (Celem.theID2str id, Celem.the2str the)) |
226 |> map pair2str |
252 |> map pair2str |
227 |> map writeln |
253 |> map writeln |
228 *} |
254 *} |
229 ML {* |
255 ML {* |
230 *} ML {* |
256 *} ML {* |