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