1 (* Title: src/Tools/isac/KEStore.thy |
|
2 Author: Mathias Lehnfeld |
|
3 |
|
4 The files (in "xxxxx-def.sml") contain definitions required for KEStore; |
|
5 they also include minimal code required for other "xxxxx-def.sml" files. |
|
6 These files have companion files "xxxxx.sml" with all further code, |
|
7 located at appropriate positions in the file structure. |
|
8 |
|
9 The separation of "xxxxx-def.sml" from "xxxxx.sml" should be overcome by |
|
10 appropriate use of polymorphic high order functions. |
|
11 *) |
|
12 |
|
13 theory KEStore imports Complex_Main |
|
14 |
|
15 begin |
|
16 ML_file libraryC.sml |
|
17 ML_file theoryC.sml |
|
18 ML_file unparseC.sml |
|
19 ML_file "rule-def.sml" |
|
20 ML_file "thmC-def.sml" |
|
21 ML_file "exec-def.sml" (*rename identifiers by use of struct.id*) |
|
22 ML_file "rewrite-order.sml" (*rename identifiers by use of struct.id*) |
|
23 ML_file rule.sml |
|
24 ML_file "error-fill-def.sml" (*rename identifiers by use of struct.id*) |
|
25 ML_file "rule-set.sml" |
|
26 |
|
27 ML_file "celem-0.sml" (*survey Celem.*) |
|
28 ML_file "celem-1.sml" (*datatype 'a ptyp*) |
|
29 ML_file "celem-2.sml" (*guh*) |
|
30 ML_file "celem-3.sml" (*spec*) |
|
31 ML_file "celem-4.sml" (*pat*) |
|
32 ML_file "celem-5.sml" (*ptyps*) |
|
33 ML_file "celem-6.sml" (*mets*) |
|
34 ML_file "celem-7.sml" (*cas_elem*) |
|
35 ML_file "celem-8.sml" (*thydata*) |
|
36 ML_file "celem-91.sml" (*check_guhs_unique*) |
|
37 ML_file "celem-92.sml" (**) |
|
38 ML_file "celem-93.sml" (**) |
|
39 |
|
40 ML_file calcelems.sml |
|
41 ML_file tracing.sml |
|
42 ML \<open> |
|
43 \<close> ML \<open> |
|
44 \<close> ML \<open> |
|
45 \<close> |
|
46 section \<open>Knowledge elements for problems and methods\<close> |
|
47 ML \<open> |
|
48 (* Knowledge (and Exercises) are held by "KEStore" in Isac's Java front-end. |
|
49 In the front-end Knowledge comprises theories, problems and methods. |
|
50 Elements of problems and methods are defined in theories alongside |
|
51 the development of respective language elements. |
|
52 However, the structure of methods and problems is independent from theories' |
|
53 deductive structure. Thus respective structures are built in Build_Thydata.thy. |
|
54 |
|
55 Most elements of problems and methods are implemented in "Knowledge/", but some |
|
56 of them are implemented in "ProgLang/" already; thus "KEStore.thy" got this |
|
57 location in the directory structure. |
|
58 |
|
59 get_* retrieves all * of the respective theory PLUS of all ancestor theories. |
|
60 *) |
|
61 signature KESTORE_ELEMS = |
|
62 sig |
|
63 val get_rlss: theory -> (Rule_Set.id * (ThyC.id * Rule_Set.T)) list |
|
64 val add_rlss: (Rule_Set.id * (ThyC.id * Rule_Set.T)) list -> theory -> theory |
|
65 val get_calcs: theory -> (Exec_Def.prog_calcID * (Exec_Def.calID * Exec_Def.eval_fn)) list |
|
66 val add_calcs: (Exec_Def.prog_calcID * (Exec_Def.calID * Exec_Def.eval_fn)) list -> theory -> theory |
|
67 val get_cas: theory -> Celem.cas_elem list |
|
68 val add_cas: Celem.cas_elem list -> theory -> theory |
|
69 val get_ptyps: theory -> Celem.ptyps |
|
70 val add_pbts: (Celem.pbt * Celem.pblID) list -> theory -> theory |
|
71 val get_mets: theory -> Celem.mets |
|
72 val add_mets: (Celem.met * Celem.metID) list -> theory -> theory |
|
73 val get_thes: theory -> (Celem.thydata Celem.ptyp) list |
|
74 val add_thes: (Celem.thydata * Celem.theID) list -> theory -> theory (* thydata dropped at existing elems *) |
|
75 val insert_fillpats: (Celem.theID * Error_Fill_Def.fillpat list) list -> theory -> theory |
|
76 val get_ref_thy: unit -> theory |
|
77 val set_ref_thy: theory -> unit |
|
78 end; |
|
79 |
|
80 structure KEStore_Elems: KESTORE_ELEMS = |
|
81 struct |
|
82 fun union_overwrite eq l1 l2 = fold (insert eq) l2 (*..swapped..*) l1; |
|
83 |
|
84 structure Data = Theory_Data ( |
|
85 type T = (Rule_Set.id * (ThyC.id * Rule_Set.T)) list; |
|
86 val empty = []; |
|
87 val extend = I; |
|
88 val merge = Rule_Set.to_kestore; |
|
89 ); |
|
90 fun get_rlss thy = Data.get thy |
|
91 fun add_rlss rlss = Data.map (union_overwrite Rule_Set.equal rlss) |
|
92 |
|
93 structure Data = Theory_Data ( |
|
94 type T = (Exec_Def.prog_calcID * (Exec_Def.calID * Exec_Def.eval_fn)) list; |
|
95 val empty = []; |
|
96 val extend = I; |
|
97 val merge = merge Exec_Def.calc_eq; |
|
98 ); |
|
99 fun get_calcs thy = Data.get thy |
|
100 fun add_calcs calcs = Data.map (union_overwrite Exec_Def.calc_eq calcs) |
|
101 |
|
102 structure Data = Theory_Data ( |
|
103 type T = (term * (Celem.spec * (term list -> (term * term list) list))) list; |
|
104 val empty = []; |
|
105 val extend = I; |
|
106 val merge = merge Celem.cas_eq; |
|
107 ); |
|
108 fun get_cas thy = Data.get thy |
|
109 fun add_cas cas = Data.map (union_overwrite Celem.cas_eq cas) |
|
110 |
|
111 structure Data = Theory_Data ( |
|
112 type T = Celem.ptyps; |
|
113 val empty = [Celem.e_Ptyp]; |
|
114 val extend = I; |
|
115 val merge = Celem.merge_ptyps; |
|
116 ); |
|
117 fun get_ptyps thy = Data.get thy; |
|
118 fun add_pbts pbts thy = let |
|
119 fun add_pbt (pbt as {guh,...}, pblID) = |
|
120 (* the pblID has the leaf-element as first; better readability achieved *) |
|
121 (if (!Celem.check_guhs_unique) then Celem.check_pblguh_unique guh (Data.get thy) else (); |
|
122 rev pblID |> Celem.insrt pblID pbt); |
|
123 in Data.map (fold add_pbt pbts) thy end; |
|
124 |
|
125 structure Data = Theory_Data ( |
|
126 type T = Celem.mets; |
|
127 val empty = [Celem.e_Mets]; |
|
128 val extend = I; |
|
129 val merge = Celem.merge_ptyps; |
|
130 ); |
|
131 val get_mets = Data.get; |
|
132 fun add_mets mets thy = let |
|
133 fun add_met (met as {guh,...}, metID) = |
|
134 (if (!Celem.check_guhs_unique) then Celem.check_metguh_unique guh (Data.get thy) else (); |
|
135 Celem.insrt metID met metID); |
|
136 in Data.map (fold add_met mets) thy end; |
|
137 |
|
138 structure Data = Theory_Data ( |
|
139 type T = (Celem.thydata Celem.ptyp) list; |
|
140 val empty = []; |
|
141 val extend = I; |
|
142 val merge = Celem.merge_ptyps; (* relevant for store_thm, store_rls *) |
|
143 ); |
|
144 fun get_thes thy = Data.get thy |
|
145 fun add_thes thes thy = let |
|
146 fun add_the (thydata, theID) = Celem.add_thydata ([], theID) thydata |
|
147 in Data.map (fold add_the thes) thy end; |
|
148 fun insert_fillpats fis thy = |
|
149 let |
|
150 fun update_elem (theID, fillpats) = |
|
151 let |
|
152 val hthm = Celem.get_py (Data.get thy) theID theID |
|
153 val hthm' = Celem.update_hthm hthm fillpats |
|
154 handle ERROR _ => |
|
155 error ("insert_fillpats: " ^ strs2str theID ^ "must address a theorem") |
|
156 in Celem.update_ptyps theID theID hthm' end |
|
157 in Data.map (fold update_elem fis) thy end |
|
158 |
|
159 val cur_thy = Synchronized.var "finally_knowledge_complete" @{theory}; |
|
160 fun set_ref_thy thy = Synchronized.change cur_thy (fn _ => thy); (* never RE-set ! *) |
|
161 fun get_ref_thy () = Synchronized.value cur_thy; |
|
162 end; |
|
163 \<close> |
|
164 |
|
165 section \<open>Re-use existing access functions for knowledge elements\<close> |
|
166 text \<open> |
|
167 The independence of problems' and methods' structure enforces the accesse |
|
168 functions to use "Isac_Knowledge", the final theory which comprises all knowledge defined. |
|
169 \<close> |
|
170 ML \<open> |
|
171 val get_ref_thy = KEStore_Elems.get_ref_thy; |
|
172 |
|
173 fun assoc_rls (rls' : Rule_Set.id) = |
|
174 case AList.lookup (op =) (KEStore_Elems.get_rlss (ThyC.get_theory "Isac_Knowledge")) rls' of |
|
175 SOME (_, rls) => rls |
|
176 | NONE => raise ERROR ("rls \""^ rls' ^ "\" missing in KEStore.\n" ^ |
|
177 "TODO exception hierarchy needs to be established.") |
|
178 |
|
179 fun assoc_rls' thy (rls' : Rule_Set.id) = |
|
180 case AList.lookup (op =) (KEStore_Elems.get_rlss thy) rls' of |
|
181 SOME (_, rls) => rls |
|
182 | NONE => raise ERROR ("rls \""^ rls' ^ "\" missing in KEStore.\n" ^ |
|
183 "TODO exception hierarchy needs to be established.") |
|
184 |
|
185 fun assoc_calc thy calID = let |
|
186 fun ass ([], key) = |
|
187 error ("assoc_calc: '" ^ key ^ "' not found in theory " ^ (Context.theory_name thy)) |
|
188 | ass ((calc, (keyi, _)) :: pairs, key) = |
|
189 if key = keyi then calc else ass (pairs, key); |
|
190 in ass (thy |> KEStore_Elems.get_calcs, calID) end; |
|
191 |
|
192 fun assoc_calc' thy key = let |
|
193 fun ass ([], key') = |
|
194 error ("assoc_calc': '" ^ key' ^ "' not found in theory " ^ (Context.theory_name thy)) |
|
195 | ass ((all as (keyi, _)) :: pairs, key') = |
|
196 if key' = keyi then all else ass (pairs, key'); |
|
197 in ass (KEStore_Elems.get_calcs thy, key) end; |
|
198 |
|
199 fun assoc_cas thy key = assoc (KEStore_Elems.get_cas thy, key); |
|
200 |
|
201 fun get_ptyps () = get_ref_thy () |> KEStore_Elems.get_ptyps; |
|
202 fun get_mets () = get_ref_thy () |> KEStore_Elems.get_mets; |
|
203 fun get_thes () = get_ref_thy () |> KEStore_Elems.get_thes; |
|
204 \<close> |
|
205 setup \<open>KEStore_Elems.add_rlss |
|
206 [("empty", (Context.theory_name @{theory}, Rule_Set.empty)), |
|
207 ("e_rrls", (Context.theory_name @{theory}, Rule_Set.e_rrls))]\<close> |
|
208 |
|
209 section \<open>determine sequence of main parts in thehier\<close> |
|
210 setup \<open> |
|
211 KEStore_Elems.add_thes |
|
212 [(Celem.Html {guh = Celem.part2guh ["IsacKnowledge"], html = "", |
|
213 mathauthors = ["Isac team"], coursedesign = []}, ["IsacKnowledge"]), |
|
214 (Celem.Html {guh = Celem.part2guh ["Isabelle"], html = "", |
|
215 mathauthors = ["Isabelle team, TU Munich"], coursedesign = []}, ["Isabelle"]), |
|
216 (Celem.Html {guh = Celem.part2guh ["IsacScripts"], html = "", |
|
217 mathauthors = ["Isac team"], coursedesign = []}, ["IsacScripts"])] |
|
218 \<close> |
|
219 |
|
220 section \<open>Functions for checking KEStore_Elems\<close> |
|
221 ML \<open> |
|
222 fun short_string_of_rls Rule_Set.Empty = "Erls" |
|
223 | short_string_of_rls (Rule_Def.Repeat {calc, rules, ...}) = |
|
224 "Rls {#calc = " ^ string_of_int (length calc) ^ |
|
225 ", #rules = " ^ string_of_int (length rules) ^ ", ..." |
|
226 | short_string_of_rls (Rule_Set.Sequence {calc, rules, ...}) = |
|
227 "Seq {#calc = " ^ string_of_int (length calc) ^ |
|
228 ", #rules = " ^ string_of_int (length rules) ^ ", ..." |
|
229 | short_string_of_rls (Rule_Set.Rrls _) = "Rrls {...}"; |
|
230 fun check_kestore_rls (rls', (thyID, rls)) = |
|
231 "(" ^ rls' ^ ", (" ^ thyID ^ ", " ^ short_string_of_rls rls ^ "))"; |
|
232 |
|
233 fun check_kestore_calc ((id, (c, _)) : Rule_Def.calc) = "(" ^ id ^ ", (" ^ c ^ ", fn))"; |
|
234 |
|
235 (* we avoid term_to_string''' defined later *) |
|
236 fun check_kestore_cas ((t, (s, _)) : Celem.cas_elem) = |
|
237 "(" ^ (Print_Mode.setmp [] (Syntax.string_of_term (Config.put show_markup false |
|
238 (Proof_Context.init_global @{theory})))) t ^ ", " ^ Celem.spec2str s ^ ")"; |
|
239 |
|
240 fun count_kestore_ptyps [] = 0 |
|
241 | count_kestore_ptyps ((Celem.Ptyp (_, _, ps)) :: ps') = |
|
242 1 + count_kestore_ptyps ps + count_kestore_ptyps ps'; |
|
243 fun check_kestore_ptyp' strfun (Celem.Ptyp (key, pbts, pts)) = "Ptyp (" ^ (quote key) ^ ", " ^ |
|
244 (strfun pbts) ^ ", " ^ (map (check_kestore_ptyp' strfun) pts |> list2str) ^ ")" |> Celem.linefeed; |
|
245 val check_kestore_ptyp = check_kestore_ptyp' Celem.pbts2str; |
|
246 fun ptyp_ord ((Celem.Ptyp (s1, _, _)), (Celem.Ptyp (s2, _, _))) = string_ord (s1, s2); |
|
247 fun pbt_ord ({guh = guh'1, ...} : Celem.pbt, {guh = guh'2, ...} : Celem.pbt) = string_ord (guh'1, guh'2); |
|
248 fun sort_kestore_ptyp' _ [] = [] |
|
249 | sort_kestore_ptyp' ordfun ((Celem.Ptyp (key, pbts, ps)) :: ps') = |
|
250 ((Celem.Ptyp (key, sort ordfun pbts, sort_kestore_ptyp' ordfun ps |> sort ptyp_ord)) |
|
251 :: sort_kestore_ptyp' ordfun ps'); |
|
252 val sort_kestore_ptyp = sort_kestore_ptyp' pbt_ord; |
|
253 |
|
254 fun metguh2str ({guh,...} : Celem.met) = guh : string; |
|
255 fun check_kestore_met (mp: Celem.met Celem.ptyp) = |
|
256 check_kestore_ptyp' (fn xs => map metguh2str xs |> strs2str) mp; |
|
257 fun met_ord ({guh = guh'1, ...} : Celem.met, {guh = guh'2, ...} : Celem.met) = string_ord (guh'1, guh'2); |
|
258 val sort_kestore_met = sort_kestore_ptyp' met_ord; |
|
259 |
|
260 fun check_kestore_thes thes = ((map writeln) o (map (check_kestore_ptyp' Celem.thes2str))) thes |
|
261 fun write_thes thydata_list = |
|
262 thydata_list |
|
263 |> map (fn (id, the) => (Celem.theID2str id, Celem.the2str the)) |
|
264 |> map pair2str |
|
265 |> map writeln |
|
266 \<close> |
|
267 ML \<open> |
|
268 \<close> ML \<open> |
|
269 \<close> ML \<open> |
|
270 \<close> |
|
271 end |
|