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"
33 ML_file "check-unique.sml"
34 ML_file "specification.sml"
35 ML_file "celem-4.sml" (*pat*)
36 ML_file "problem-def.sml"
37 ML_file "method-def.sml"
39 ML_file "thy-html.sml"
45 section \<open>Knowledge elements for problems and methods\<close>
47 (* Knowledge (and Exercises) are held by "Know_Store" in Isac's Java front-end.
48 In the front-end Knowledge comprises theories, problems and methods.
49 Elements of problems and methods are defined in theories alongside
50 the development of respective language elements.
51 However, the structure of methods and problems is independent from theories'
52 deductive structure. Thus respective structures are built in Build_Thydata.thy.
54 Most elements of problems and methods are implemented in "Knowledge/", but some
55 of them are implemented in "ProgLang/" already; thus "Know_Store.thy" got this
56 location in the directory structure.
58 get_* retrieves all * of the respective theory PLUS of all ancestor theories.
60 signature KESTORE_ELEMS =
62 val get_rlss: theory -> (Rule_Set.id * (ThyC.id * Rule_Set.T)) list
63 val add_rlss: (Rule_Set.id * (ThyC.id * Rule_Set.T)) list -> theory -> theory
64 val get_calcs: theory -> (Exec_Def.prog_calcID * (Exec_Def.calID * Exec_Def.eval_fn)) list
65 val add_calcs: (Exec_Def.prog_calcID * (Exec_Def.calID * Exec_Def.eval_fn)) list -> theory -> theory
66 val get_cas: theory -> CAS_Def.T list
67 val add_cas: CAS_Def.T list -> theory -> theory
68 val get_ptyps: theory -> Probl_Def.store
69 val add_pbts: (Probl_Def.T * Spec.pblID) list -> theory -> theory
70 val get_mets: theory -> Meth_Def.store
71 val add_mets: (Meth_Def.T * Spec.metID) list -> theory -> theory
72 val get_thes: theory -> (Thy_Html.thydata Store.ptyp) list
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
75 val get_ref_thy: unit -> theory
76 val set_ref_thy: theory -> unit
79 structure KEStore_Elems: KESTORE_ELEMS =
81 fun union_overwrite eq l1 l2 = fold (insert eq) l2 (*..swapped..*) l1;
83 structure Data = Theory_Data (
84 type T = (Rule_Set.id * (ThyC.id * Rule_Set.T)) list;
87 val merge = Rule_Set.to_kestore;
89 fun get_rlss thy = Data.get thy
90 fun add_rlss rlss = Data.map (union_overwrite Rule_Set.equal rlss)
92 structure Data = Theory_Data (
93 type T = (Exec_Def.prog_calcID * (Exec_Def.calID * Exec_Def.eval_fn)) list;
96 val merge = merge Exec_Def.calc_eq;
98 fun get_calcs thy = Data.get thy
99 fun add_calcs calcs = Data.map (union_overwrite Exec_Def.calc_eq calcs)
101 structure Data = Theory_Data (
102 type T = (term * (Spec.spec * (term list -> (term * term list) list))) list;
105 val merge = merge CAS_Def.equal;
107 fun get_cas thy = Data.get thy
108 fun add_cas cas = Data.map (union_overwrite CAS_Def.equal cas)
110 structure Data = Theory_Data (
111 type T = Probl_Def.store;
112 val empty = [Probl_Def.empty_store];
114 val merge = Store.merge_ptyps;
116 fun get_ptyps thy = Data.get thy;
117 fun add_pbts pbts thy = let
118 fun add_pbt (pbt as {guh,...}, pblID) =
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 ();
121 rev pblID |> Store.insrt pblID pbt);
122 in Data.map (fold add_pbt pbts) thy end;
124 structure Data = Theory_Data (
125 type T = Meth_Def.store;
126 val empty = [Meth_Def.empty_store];
128 val merge = Store.merge_ptyps;
130 val get_mets = Data.get;
131 fun add_mets mets thy = let
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 ();
134 Store.insrt metID met metID);
135 in Data.map (fold add_met mets) thy end;
137 structure Data = Theory_Data (
138 type T = (Thy_Html.thydata Store.ptyp) list;
141 val merge = Store.merge_ptyps; (* relevant for store_thm, store_rls *)
143 fun get_thes thy = Data.get thy
144 fun add_thes thes thy = let
145 fun add_the (thydata, theID) = Thy_Html.add_thydata ([], theID) thydata
146 in Data.map (fold add_the thes) thy end;
147 fun insert_fillpats fis thy =
149 fun update_elem (theID, fillpats) =
151 val hthm = Store.get_py (Data.get thy) theID theID
152 val hthm' = Thy_Html.update_hthm hthm fillpats
154 error ("insert_fillpats: " ^ strs2str theID ^ "must address a theorem")
155 in Store.update_ptyps theID theID hthm' end
156 in Data.map (fold update_elem fis) thy end
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 ! *)
160 fun get_ref_thy () = Synchronized.value cur_thy;
164 section \<open>Re-use existing access functions for knowledge elements\<close>
166 The independence of problems' and methods' structure enforces the accesse
167 functions to use "Isac_Knowledge", the final theory which comprises all knowledge defined.
170 val get_ref_thy = KEStore_Elems.get_ref_thy;
172 fun assoc_rls (rls' : Rule_Set.id) =
173 case AList.lookup (op =) (KEStore_Elems.get_rlss (ThyC.get_theory "Isac_Knowledge")) rls' of
175 | NONE => raise ERROR ("rls \""^ rls' ^ "\" missing in Know_Store.\n" ^
176 "TODO exception hierarchy needs to be established.")
178 fun assoc_rls' thy (rls' : Rule_Set.id) =
179 case AList.lookup (op =) (KEStore_Elems.get_rlss thy) rls' of
181 | NONE => raise ERROR ("rls \""^ rls' ^ "\" missing in Know_Store.\n" ^
182 "TODO exception hierarchy needs to be established.")
184 fun assoc_calc thy calID = let
186 error ("assoc_calc: '" ^ key ^ "' not found in theory " ^ (Context.theory_name thy))
187 | ass ((calc, (keyi, _)) :: pairs, key) =
188 if key = keyi then calc else ass (pairs, key);
189 in ass (thy |> KEStore_Elems.get_calcs, calID) end;
191 fun assoc_calc' thy key = let
193 error ("assoc_calc': '" ^ key' ^ "' not found in theory " ^ (Context.theory_name thy))
194 | ass ((all as (keyi, _)) :: pairs, key') =
195 if key' = keyi then all else ass (pairs, key');
196 in ass (KEStore_Elems.get_calcs thy, key) end;
198 fun assoc_cas thy key = assoc (KEStore_Elems.get_cas thy, key);
200 fun get_ptyps () = get_ref_thy () |> KEStore_Elems.get_ptyps;
201 fun get_mets () = get_ref_thy () |> KEStore_Elems.get_mets;
202 fun get_thes () = get_ref_thy () |> KEStore_Elems.get_thes;
204 setup \<open>KEStore_Elems.add_rlss
205 [("empty", (Context.theory_name @{theory}, Rule_Set.empty)),
206 ("e_rrls", (Context.theory_name @{theory}, Rule_Set.e_rrls))]\<close>
208 section \<open>determine sequence of main parts in thehier\<close>
210 KEStore_Elems.add_thes
211 [(Thy_Html.Html {guh = Thy_Html.part2guh ["IsacKnowledge"], html = "",
212 mathauthors = ["Isac team"], coursedesign = []}, ["IsacKnowledge"]),
213 (Thy_Html.Html {guh = Thy_Html.part2guh ["Isabelle"], html = "",
214 mathauthors = ["Isabelle team, TU Munich"], coursedesign = []}, ["Isabelle"]),
215 (Thy_Html.Html {guh = Thy_Html.part2guh ["IsacScripts"], html = "",
216 mathauthors = ["Isac team"], coursedesign = []}, ["IsacScripts"])]
219 section \<open>Functions for checking KEStore_Elems\<close>
221 fun short_string_of_rls Rule_Set.Empty = "Erls"
222 | short_string_of_rls (Rule_Def.Repeat {calc, rules, ...}) =
223 "Rls {#calc = " ^ string_of_int (length calc) ^
224 ", #rules = " ^ string_of_int (length rules) ^ ", ..."
225 | short_string_of_rls (Rule_Set.Sequence {calc, rules, ...}) =
226 "Seq {#calc = " ^ string_of_int (length calc) ^
227 ", #rules = " ^ string_of_int (length rules) ^ ", ..."
228 | short_string_of_rls (Rule_Set.Rrls _) = "Rrls {...}";
229 fun check_kestore_rls (rls', (thyID, rls)) =
230 "(" ^ rls' ^ ", (" ^ thyID ^ ", " ^ short_string_of_rls rls ^ "))";
232 fun check_kestore_calc ((id, (c, _)) : Rule_Def.calc) = "(" ^ id ^ ", (" ^ c ^ ", fn))";
234 (* we avoid term_to_string''' defined later *)
235 fun check_kestore_cas ((t, (s, _)) : CAS_Def.T) =
236 "(" ^ (Print_Mode.setmp [] (Syntax.string_of_term (Config.put show_markup false
237 (Proof_Context.init_global @{theory})))) t ^ ", " ^ Spec.spec2str s ^ ")";
239 fun count_kestore_ptyps [] = 0
240 | count_kestore_ptyps ((Store.Ptyp (_, _, ps)) :: 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) ^ ", " ^
243 (strfun pbts) ^ ", " ^ (map (check_kestore_ptyp' strfun) pts |> list2str) ^ ")" |> linefeed;
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);
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' _ [] = []
248 | sort_kestore_ptyp' ordfun ((Store.Ptyp (key, pbts, ps)) :: ps') =
249 ((Store.Ptyp (key, sort ordfun pbts, sort_kestore_ptyp' ordfun ps |> sort ptyp_ord))
250 :: sort_kestore_ptyp' ordfun ps');
251 val sort_kestore_ptyp = sort_kestore_ptyp' pbt_ord;
253 fun metguh2str ({guh,...} : Meth_Def.T) = guh : string;
254 fun check_kestore_met (mp: Meth_Def.T Store.ptyp) =
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);
257 val sort_kestore_met = sort_kestore_ptyp' met_ord;
259 fun check_kestore_thes thes = ((map writeln) o (map (check_kestore_ptyp' Thy_Html.thes2str))) thes
260 fun write_thes thydata_list =
262 |> map (fn (id, the) => (Thy_Html.theID2str id, Thy_Html.the2str the))