1 (* Title: src/Tools/isac/Know_Store.thy
2 Author: Mathias Lehnfeld
4 The files (in "xxxxx-def.sml") contain definitions required for Know_Store;
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.
9 The separation of "xxxxx-def.sml" from "xxxxx.sml" should be overcome by
10 appropriate use of polymorphic high order functions.
13 theory Know_Store imports Complex_Main
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*)
24 ML_file "error-fill-def.sml" (*rename identifiers by use of struct.id*)
25 ML_file "rule-set.sml"
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*)
44 section \<open>Knowledge elements for problems and methods\<close>
46 (* Knowledge (and Exercises) are held by "Know_Store" in Isac's Java front-end.
47 In the front-end Knowledge comprises theories, problems and methods.
48 Elements of problems and methods are defined in theories alongside
49 the development of respective language elements.
50 However, the structure of methods and problems is independent from theories'
51 deductive structure. Thus respective structures are built in Build_Thydata.thy.
53 Most elements of problems and methods are implemented in "Knowledge/", but some
54 of them are implemented in "ProgLang/" already; thus "Know_Store.thy" got this
55 location in the directory structure.
57 get_* retrieves all * of the respective theory PLUS of all ancestor theories.
59 signature KESTORE_ELEMS =
61 val get_rlss: theory -> (Rule_Set.id * (ThyC.id * Rule_Set.T)) list
62 val add_rlss: (Rule_Set.id * (ThyC.id * Rule_Set.T)) list -> theory -> theory
63 val get_calcs: theory -> (Exec_Def.prog_calcID * (Exec_Def.calID * Exec_Def.eval_fn)) list
64 val add_calcs: (Exec_Def.prog_calcID * (Exec_Def.calID * Exec_Def.eval_fn)) list -> theory -> theory
65 val get_cas: theory -> Celem.cas_elem list
66 val add_cas: Celem.cas_elem list -> theory -> theory
67 val get_ptyps: theory -> Celem.ptyps
68 val add_pbts: (Celem.pbt * Celem.pblID) list -> theory -> theory
69 val get_mets: theory -> Celem.mets
70 val add_mets: (Celem.met * Celem.metID) list -> theory -> theory
71 val get_thes: theory -> (Celem.thydata Celem1.ptyp) list
72 val add_thes: (Celem.thydata * Celem.theID) list -> theory -> theory (* thydata dropped at existing elems *)
73 val insert_fillpats: (Celem.theID * Error_Fill_Def.fillpat list) list -> theory -> theory
74 val get_ref_thy: unit -> theory
75 val set_ref_thy: theory -> unit
78 structure KEStore_Elems: KESTORE_ELEMS =
80 fun union_overwrite eq l1 l2 = fold (insert eq) l2 (*..swapped..*) l1;
82 structure Data = Theory_Data (
83 type T = (Rule_Set.id * (ThyC.id * Rule_Set.T)) list;
86 val merge = Rule_Set.to_kestore;
88 fun get_rlss thy = Data.get thy
89 fun add_rlss rlss = Data.map (union_overwrite Rule_Set.equal rlss)
91 structure Data = Theory_Data (
92 type T = (Exec_Def.prog_calcID * (Exec_Def.calID * Exec_Def.eval_fn)) list;
95 val merge = merge Exec_Def.calc_eq;
97 fun get_calcs thy = Data.get thy
98 fun add_calcs calcs = Data.map (union_overwrite Exec_Def.calc_eq calcs)
100 structure Data = Theory_Data (
101 type T = (term * (Celem.spec * (term list -> (term * term list) list))) list;
104 val merge = merge Celem.cas_eq;
106 fun get_cas thy = Data.get thy
107 fun add_cas cas = Data.map (union_overwrite Celem.cas_eq cas)
109 structure Data = Theory_Data (
110 type T = Celem.ptyps;
111 val empty = [Celem.e_Ptyp];
113 val merge = Celem1.merge_ptyps;
115 fun get_ptyps thy = Data.get thy;
116 fun add_pbts pbts thy = let
117 fun add_pbt (pbt as {guh,...}, pblID) =
118 (* the pblID has the leaf-element as first; better readability achieved *)
119 (if (!Celem.check_guhs_unique) then Celem.check_pblguh_unique guh (Data.get thy) else ();
120 rev pblID |> Celem1.insrt pblID pbt);
121 in Data.map (fold add_pbt pbts) thy end;
123 structure Data = Theory_Data (
125 val empty = [Celem.e_Mets];
127 val merge = Celem1.merge_ptyps;
129 val get_mets = Data.get;
130 fun add_mets mets thy = let
131 fun add_met (met as {guh,...}, metID) =
132 (if (!Celem.check_guhs_unique) then Celem.check_metguh_unique guh (Data.get thy) else ();
133 Celem1.insrt metID met metID);
134 in Data.map (fold add_met mets) thy end;
136 structure Data = Theory_Data (
137 type T = (Celem.thydata Celem1.ptyp) list;
140 val merge = Celem1.merge_ptyps; (* relevant for store_thm, store_rls *)
142 fun get_thes thy = Data.get thy
143 fun add_thes thes thy = let
144 fun add_the (thydata, theID) = Celem.add_thydata ([], theID) thydata
145 in Data.map (fold add_the thes) thy end;
146 fun insert_fillpats fis thy =
148 fun update_elem (theID, fillpats) =
150 val hthm = Celem1.get_py (Data.get thy) theID theID
151 val hthm' = Celem.update_hthm hthm fillpats
153 error ("insert_fillpats: " ^ strs2str theID ^ "must address a theorem")
154 in Celem1.update_ptyps theID theID hthm' end
155 in Data.map (fold update_elem fis) thy end
157 val cur_thy = Synchronized.var "finally_knowledge_complete" @{theory};
158 fun set_ref_thy thy = Synchronized.change cur_thy (fn _ => thy); (* never RE-set ! *)
159 fun get_ref_thy () = Synchronized.value cur_thy;
163 section \<open>Re-use existing access functions for knowledge elements\<close>
165 The independence of problems' and methods' structure enforces the accesse
166 functions to use "Isac_Knowledge", the final theory which comprises all knowledge defined.
169 val get_ref_thy = KEStore_Elems.get_ref_thy;
171 fun assoc_rls (rls' : Rule_Set.id) =
172 case AList.lookup (op =) (KEStore_Elems.get_rlss (ThyC.get_theory "Isac_Knowledge")) rls' of
174 | NONE => raise ERROR ("rls \""^ rls' ^ "\" missing in Know_Store.\n" ^
175 "TODO exception hierarchy needs to be established.")
177 fun assoc_rls' thy (rls' : Rule_Set.id) =
178 case AList.lookup (op =) (KEStore_Elems.get_rlss thy) rls' of
180 | NONE => raise ERROR ("rls \""^ rls' ^ "\" missing in Know_Store.\n" ^
181 "TODO exception hierarchy needs to be established.")
183 fun assoc_calc thy calID = let
185 error ("assoc_calc: '" ^ key ^ "' not found in theory " ^ (Context.theory_name thy))
186 | ass ((calc, (keyi, _)) :: pairs, key) =
187 if key = keyi then calc else ass (pairs, key);
188 in ass (thy |> KEStore_Elems.get_calcs, calID) end;
190 fun assoc_calc' thy key = let
192 error ("assoc_calc': '" ^ key' ^ "' not found in theory " ^ (Context.theory_name thy))
193 | ass ((all as (keyi, _)) :: pairs, key') =
194 if key' = keyi then all else ass (pairs, key');
195 in ass (KEStore_Elems.get_calcs thy, key) end;
197 fun assoc_cas thy key = assoc (KEStore_Elems.get_cas thy, key);
199 fun get_ptyps () = get_ref_thy () |> KEStore_Elems.get_ptyps;
200 fun get_mets () = get_ref_thy () |> KEStore_Elems.get_mets;
201 fun get_thes () = get_ref_thy () |> KEStore_Elems.get_thes;
203 setup \<open>KEStore_Elems.add_rlss
204 [("empty", (Context.theory_name @{theory}, Rule_Set.empty)),
205 ("e_rrls", (Context.theory_name @{theory}, Rule_Set.e_rrls))]\<close>
207 section \<open>determine sequence of main parts in thehier\<close>
209 KEStore_Elems.add_thes
210 [(Celem.Html {guh = Celem.part2guh ["IsacKnowledge"], html = "",
211 mathauthors = ["Isac team"], coursedesign = []}, ["IsacKnowledge"]),
212 (Celem.Html {guh = Celem.part2guh ["Isabelle"], html = "",
213 mathauthors = ["Isabelle team, TU Munich"], coursedesign = []}, ["Isabelle"]),
214 (Celem.Html {guh = Celem.part2guh ["IsacScripts"], html = "",
215 mathauthors = ["Isac team"], coursedesign = []}, ["IsacScripts"])]
218 section \<open>Functions for checking KEStore_Elems\<close>
220 fun short_string_of_rls Rule_Set.Empty = "Erls"
221 | short_string_of_rls (Rule_Def.Repeat {calc, rules, ...}) =
222 "Rls {#calc = " ^ string_of_int (length calc) ^
223 ", #rules = " ^ string_of_int (length rules) ^ ", ..."
224 | short_string_of_rls (Rule_Set.Sequence {calc, rules, ...}) =
225 "Seq {#calc = " ^ string_of_int (length calc) ^
226 ", #rules = " ^ string_of_int (length rules) ^ ", ..."
227 | short_string_of_rls (Rule_Set.Rrls _) = "Rrls {...}";
228 fun check_kestore_rls (rls', (thyID, rls)) =
229 "(" ^ rls' ^ ", (" ^ thyID ^ ", " ^ short_string_of_rls rls ^ "))";
231 fun check_kestore_calc ((id, (c, _)) : Rule_Def.calc) = "(" ^ id ^ ", (" ^ c ^ ", fn))";
233 (* we avoid term_to_string''' defined later *)
234 fun check_kestore_cas ((t, (s, _)) : Celem.cas_elem) =
235 "(" ^ (Print_Mode.setmp [] (Syntax.string_of_term (Config.put show_markup false
236 (Proof_Context.init_global @{theory})))) t ^ ", " ^ Celem.spec2str s ^ ")";
238 fun count_kestore_ptyps [] = 0
239 | count_kestore_ptyps ((Celem1.Ptyp (_, _, ps)) :: ps') =
240 1 + count_kestore_ptyps ps + count_kestore_ptyps ps';
241 fun check_kestore_ptyp' strfun (Celem1.Ptyp (key, pbts, pts)) = "Ptyp (" ^ (quote key) ^ ", " ^
242 (strfun pbts) ^ ", " ^ (map (check_kestore_ptyp' strfun) pts |> list2str) ^ ")" |> linefeed;
243 val check_kestore_ptyp = check_kestore_ptyp' Celem.pbts2str;
244 fun ptyp_ord ((Celem1.Ptyp (s1, _, _)), (Celem1.Ptyp (s2, _, _))) = string_ord (s1, s2);
245 fun pbt_ord ({guh = guh'1, ...} : Celem.pbt, {guh = guh'2, ...} : Celem.pbt) = string_ord (guh'1, guh'2);
246 fun sort_kestore_ptyp' _ [] = []
247 | sort_kestore_ptyp' ordfun ((Celem1.Ptyp (key, pbts, ps)) :: ps') =
248 ((Celem1.Ptyp (key, sort ordfun pbts, sort_kestore_ptyp' ordfun ps |> sort ptyp_ord))
249 :: sort_kestore_ptyp' ordfun ps');
250 val sort_kestore_ptyp = sort_kestore_ptyp' pbt_ord;
252 fun metguh2str ({guh,...} : Celem.met) = guh : string;
253 fun check_kestore_met (mp: Celem.met Celem1.ptyp) =
254 check_kestore_ptyp' (fn xs => map metguh2str xs |> strs2str) mp;
255 fun met_ord ({guh = guh'1, ...} : Celem.met, {guh = guh'2, ...} : Celem.met) = string_ord (guh'1, guh'2);
256 val sort_kestore_met = sort_kestore_ptyp' met_ord;
258 fun check_kestore_thes thes = ((map writeln) o (map (check_kestore_ptyp' Celem.thes2str))) thes
259 fun write_thes thydata_list =
261 |> map (fn (id, the) => (Celem8.theID2str id, Celem8.the2str the))