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.*)
33 ML_file "celem-1.sml" (*datatype 'a ptyp*)
34 ML_file "celem-2.sml" (*guh*)
35 ML_file "celem-3.sml" (*spec*)
36 ML_file "celem-4.sml" (*pat*)
37 ML_file "celem-5.sml" (*ptyps*)
38 ML_file "celem-6.sml" (*mets*)
39 ML_file "celem-7.sml" (*cas_elem*)
40 ML_file "celem-8.sml" (*thydata*)
41 ML_file "celem-91.sml" (*check_guhs_unique*)
48 section \<open>Knowledge elements for problems and methods\<close>
50 (* Knowledge (and Exercises) are held by "Know_Store" in Isac's Java front-end.
51 In the front-end Knowledge comprises theories, problems and methods.
52 Elements of problems and methods are defined in theories alongside
53 the development of respective language elements.
54 However, the structure of methods and problems is independent from theories'
55 deductive structure. Thus respective structures are built in Build_Thydata.thy.
57 Most elements of problems and methods are implemented in "Knowledge/", but some
58 of them are implemented in "ProgLang/" already; thus "Know_Store.thy" got this
59 location in the directory structure.
61 get_* retrieves all * of the respective theory PLUS of all ancestor theories.
63 signature KESTORE_ELEMS =
65 val get_rlss: theory -> (Rule_Set.id * (ThyC.id * Rule_Set.T)) list
66 val add_rlss: (Rule_Set.id * (ThyC.id * Rule_Set.T)) list -> theory -> theory
67 val get_calcs: theory -> (Exec_Def.prog_calcID * (Exec_Def.calID * Exec_Def.eval_fn)) list
68 val add_calcs: (Exec_Def.prog_calcID * (Exec_Def.calID * Exec_Def.eval_fn)) list -> theory -> theory
69 val get_cas: theory -> Celem7.cas_elem list
70 val add_cas: Celem7.cas_elem list -> theory -> theory
71 val get_ptyps: theory -> Celem5.ptyps
72 val add_pbts: (Celem5.pbt * Celem3.pblID) list -> theory -> theory
73 val get_mets: theory -> Celem6.mets
74 val add_mets: (Celem6.met * Celem3.metID) list -> theory -> theory
75 val get_thes: theory -> (Celem8.thydata Store.ptyp) list
76 val add_thes: (Celem8.thydata * Celem8.theID) list -> theory -> theory (* thydata dropped at existing elems *)
77 val insert_fillpats: (Celem8.theID * Error_Fill_Def.fillpat list) list -> theory -> theory
78 val get_ref_thy: unit -> theory
79 val set_ref_thy: theory -> unit
82 structure KEStore_Elems: KESTORE_ELEMS =
84 fun union_overwrite eq l1 l2 = fold (insert eq) l2 (*..swapped..*) l1;
86 structure Data = Theory_Data (
87 type T = (Rule_Set.id * (ThyC.id * Rule_Set.T)) list;
90 val merge = Rule_Set.to_kestore;
92 fun get_rlss thy = Data.get thy
93 fun add_rlss rlss = Data.map (union_overwrite Rule_Set.equal rlss)
95 structure Data = Theory_Data (
96 type T = (Exec_Def.prog_calcID * (Exec_Def.calID * Exec_Def.eval_fn)) list;
99 val merge = merge Exec_Def.calc_eq;
101 fun get_calcs thy = Data.get thy
102 fun add_calcs calcs = Data.map (union_overwrite Exec_Def.calc_eq calcs)
104 structure Data = Theory_Data (
105 type T = (term * (Celem3.spec * (term list -> (term * term list) list))) list;
108 val merge = merge Celem7.cas_eq;
110 fun get_cas thy = Data.get thy
111 fun add_cas cas = Data.map (union_overwrite Celem7.cas_eq cas)
113 structure Data = Theory_Data (
114 type T = Celem5.ptyps;
115 val empty = [Celem5.e_Ptyp];
117 val merge = Store.merge_ptyps;
119 fun get_ptyps thy = Data.get thy;
120 fun add_pbts pbts thy = let
121 fun add_pbt (pbt as {guh,...}, pblID) =
122 (* the pblID has the leaf-element as first; better readability achieved *)
123 (if (!Celem91.check_guhs_unique) then Celem91.check_pblguh_unique guh (Data.get thy) else ();
124 rev pblID |> Store.insrt pblID pbt);
125 in Data.map (fold add_pbt pbts) thy end;
127 structure Data = Theory_Data (
128 type T = Celem6.mets;
129 val empty = [Celem6.e_Mets];
131 val merge = Store.merge_ptyps;
133 val get_mets = Data.get;
134 fun add_mets mets thy = let
135 fun add_met (met as {guh,...}, metID) =
136 (if (!Celem91.check_guhs_unique) then Celem91.check_metguh_unique guh (Data.get thy) else ();
137 Store.insrt metID met metID);
138 in Data.map (fold add_met mets) thy end;
140 structure Data = Theory_Data (
141 type T = (Celem8.thydata Store.ptyp) list;
144 val merge = Store.merge_ptyps; (* relevant for store_thm, store_rls *)
146 fun get_thes thy = Data.get thy
147 fun add_thes thes thy = let
148 fun add_the (thydata, theID) = Celem8.add_thydata ([], theID) thydata
149 in Data.map (fold add_the thes) thy end;
150 fun insert_fillpats fis thy =
152 fun update_elem (theID, fillpats) =
154 val hthm = Store.get_py (Data.get thy) theID theID
155 val hthm' = Celem8.update_hthm hthm fillpats
157 error ("insert_fillpats: " ^ strs2str theID ^ "must address a theorem")
158 in Store.update_ptyps theID theID hthm' end
159 in Data.map (fold update_elem fis) thy end
161 val cur_thy = Synchronized.var "finally_knowledge_complete" @{theory};
162 fun set_ref_thy thy = Synchronized.change cur_thy (fn _ => thy); (* never RE-set ! *)
163 fun get_ref_thy () = Synchronized.value cur_thy;
167 section \<open>Re-use existing access functions for knowledge elements\<close>
169 The independence of problems' and methods' structure enforces the accesse
170 functions to use "Isac_Knowledge", the final theory which comprises all knowledge defined.
173 val get_ref_thy = KEStore_Elems.get_ref_thy;
175 fun assoc_rls (rls' : Rule_Set.id) =
176 case AList.lookup (op =) (KEStore_Elems.get_rlss (ThyC.get_theory "Isac_Knowledge")) rls' of
178 | NONE => raise ERROR ("rls \""^ rls' ^ "\" missing in Know_Store.\n" ^
179 "TODO exception hierarchy needs to be established.")
181 fun assoc_rls' thy (rls' : Rule_Set.id) =
182 case AList.lookup (op =) (KEStore_Elems.get_rlss thy) rls' of
184 | NONE => raise ERROR ("rls \""^ rls' ^ "\" missing in Know_Store.\n" ^
185 "TODO exception hierarchy needs to be established.")
187 fun assoc_calc thy calID = let
189 error ("assoc_calc: '" ^ key ^ "' not found in theory " ^ (Context.theory_name thy))
190 | ass ((calc, (keyi, _)) :: pairs, key) =
191 if key = keyi then calc else ass (pairs, key);
192 in ass (thy |> KEStore_Elems.get_calcs, calID) end;
194 fun assoc_calc' thy key = let
196 error ("assoc_calc': '" ^ key' ^ "' not found in theory " ^ (Context.theory_name thy))
197 | ass ((all as (keyi, _)) :: pairs, key') =
198 if key' = keyi then all else ass (pairs, key');
199 in ass (KEStore_Elems.get_calcs thy, key) end;
201 fun assoc_cas thy key = assoc (KEStore_Elems.get_cas thy, key);
203 fun get_ptyps () = get_ref_thy () |> KEStore_Elems.get_ptyps;
204 fun get_mets () = get_ref_thy () |> KEStore_Elems.get_mets;
205 fun get_thes () = get_ref_thy () |> KEStore_Elems.get_thes;
207 setup \<open>KEStore_Elems.add_rlss
208 [("empty", (Context.theory_name @{theory}, Rule_Set.empty)),
209 ("e_rrls", (Context.theory_name @{theory}, Rule_Set.e_rrls))]\<close>
211 section \<open>determine sequence of main parts in thehier\<close>
213 KEStore_Elems.add_thes
214 [(Celem8.Html {guh = Celem8.part2guh ["IsacKnowledge"], html = "",
215 mathauthors = ["Isac team"], coursedesign = []}, ["IsacKnowledge"]),
216 (Celem8.Html {guh = Celem8.part2guh ["Isabelle"], html = "",
217 mathauthors = ["Isabelle team, TU Munich"], coursedesign = []}, ["Isabelle"]),
218 (Celem8.Html {guh = Celem8.part2guh ["IsacScripts"], html = "",
219 mathauthors = ["Isac team"], coursedesign = []}, ["IsacScripts"])]
222 section \<open>Functions for checking KEStore_Elems\<close>
224 fun short_string_of_rls Rule_Set.Empty = "Erls"
225 | short_string_of_rls (Rule_Def.Repeat {calc, rules, ...}) =
226 "Rls {#calc = " ^ string_of_int (length calc) ^
227 ", #rules = " ^ string_of_int (length rules) ^ ", ..."
228 | short_string_of_rls (Rule_Set.Sequence {calc, rules, ...}) =
229 "Seq {#calc = " ^ string_of_int (length calc) ^
230 ", #rules = " ^ string_of_int (length rules) ^ ", ..."
231 | short_string_of_rls (Rule_Set.Rrls _) = "Rrls {...}";
232 fun check_kestore_rls (rls', (thyID, rls)) =
233 "(" ^ rls' ^ ", (" ^ thyID ^ ", " ^ short_string_of_rls rls ^ "))";
235 fun check_kestore_calc ((id, (c, _)) : Rule_Def.calc) = "(" ^ id ^ ", (" ^ c ^ ", fn))";
237 (* we avoid term_to_string''' defined later *)
238 fun check_kestore_cas ((t, (s, _)) : Celem7.cas_elem) =
239 "(" ^ (Print_Mode.setmp [] (Syntax.string_of_term (Config.put show_markup false
240 (Proof_Context.init_global @{theory})))) t ^ ", " ^ Celem3.spec2str s ^ ")";
242 fun count_kestore_ptyps [] = 0
243 | count_kestore_ptyps ((Store.Ptyp (_, _, ps)) :: ps') =
244 1 + count_kestore_ptyps ps + count_kestore_ptyps ps';
245 fun check_kestore_ptyp' strfun (Store.Ptyp (key, pbts, pts)) = "Ptyp (" ^ (quote key) ^ ", " ^
246 (strfun pbts) ^ ", " ^ (map (check_kestore_ptyp' strfun) pts |> list2str) ^ ")" |> linefeed;
247 val check_kestore_ptyp = check_kestore_ptyp' Celem5.pbts2str;
248 fun ptyp_ord ((Store.Ptyp (s1, _, _)), (Store.Ptyp (s2, _, _))) = string_ord (s1, s2);
249 fun pbt_ord ({guh = guh'1, ...} : Celem5.pbt, {guh = guh'2, ...} : Celem5.pbt) = string_ord (guh'1, guh'2);
250 fun sort_kestore_ptyp' _ [] = []
251 | sort_kestore_ptyp' ordfun ((Store.Ptyp (key, pbts, ps)) :: ps') =
252 ((Store.Ptyp (key, sort ordfun pbts, sort_kestore_ptyp' ordfun ps |> sort ptyp_ord))
253 :: sort_kestore_ptyp' ordfun ps');
254 val sort_kestore_ptyp = sort_kestore_ptyp' pbt_ord;
256 fun metguh2str ({guh,...} : Celem6.met) = guh : string;
257 fun check_kestore_met (mp: Celem6.met Store.ptyp) =
258 check_kestore_ptyp' (fn xs => map metguh2str xs |> strs2str) mp;
259 fun met_ord ({guh = guh'1, ...} : Celem6.met, {guh = guh'2, ...} : Celem6.met) = string_ord (guh'1, guh'2);
260 val sort_kestore_met = sort_kestore_ptyp' met_ord;
262 fun check_kestore_thes thes = ((map writeln) o (map (check_kestore_ptyp' Celem8.thes2str))) thes
263 fun write_thes thydata_list =
265 |> map (fn (id, the) => (Celem8.theID2str id, Celem8.the2str the))