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*)
37 ML_file "celem-92.sml" (**)
38 ML_file "celem-93.sml" (**)
46 section \<open>Knowledge elements for problems and methods\<close>
48 (* Knowledge (and Exercises) are held by "Know_Store" 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.
55 Most elements of problems and methods are implemented in "Knowledge/", but some
56 of them are implemented in "ProgLang/" already; thus "Know_Store.thy" got this
57 location in the directory structure.
59 get_* retrieves all * of the respective theory PLUS of all ancestor theories.
61 signature KESTORE_ELEMS =
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 Celem1.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
80 structure KEStore_Elems: KESTORE_ELEMS =
82 fun union_overwrite eq l1 l2 = fold (insert eq) l2 (*..swapped..*) l1;
84 structure Data = Theory_Data (
85 type T = (Rule_Set.id * (ThyC.id * Rule_Set.T)) list;
88 val merge = Rule_Set.to_kestore;
90 fun get_rlss thy = Data.get thy
91 fun add_rlss rlss = Data.map (union_overwrite Rule_Set.equal rlss)
93 structure Data = Theory_Data (
94 type T = (Exec_Def.prog_calcID * (Exec_Def.calID * Exec_Def.eval_fn)) list;
97 val merge = merge Exec_Def.calc_eq;
99 fun get_calcs thy = Data.get thy
100 fun add_calcs calcs = Data.map (union_overwrite Exec_Def.calc_eq calcs)
102 structure Data = Theory_Data (
103 type T = (term * (Celem.spec * (term list -> (term * term list) list))) list;
106 val merge = merge Celem.cas_eq;
108 fun get_cas thy = Data.get thy
109 fun add_cas cas = Data.map (union_overwrite Celem.cas_eq cas)
111 structure Data = Theory_Data (
112 type T = Celem.ptyps;
113 val empty = [Celem.e_Ptyp];
115 val merge = Celem.merge_ptyps;
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;
125 structure Data = Theory_Data (
127 val empty = [Celem.e_Mets];
129 val merge = Celem.merge_ptyps;
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;
138 structure Data = Theory_Data (
139 type T = (Celem.thydata Celem1.ptyp) list;
142 val merge = Celem.merge_ptyps; (* relevant for store_thm, store_rls *)
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 =
150 fun update_elem (theID, fillpats) =
152 val hthm = Celem.get_py (Data.get thy) theID theID
153 val hthm' = Celem.update_hthm hthm fillpats
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
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;
165 section \<open>Re-use existing access functions for knowledge elements\<close>
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.
171 val get_ref_thy = KEStore_Elems.get_ref_thy;
173 fun assoc_rls (rls' : Rule_Set.id) =
174 case AList.lookup (op =) (KEStore_Elems.get_rlss (ThyC.get_theory "Isac_Knowledge")) rls' of
176 | NONE => raise ERROR ("rls \""^ rls' ^ "\" missing in Know_Store.\n" ^
177 "TODO exception hierarchy needs to be established.")
179 fun assoc_rls' thy (rls' : Rule_Set.id) =
180 case AList.lookup (op =) (KEStore_Elems.get_rlss thy) rls' of
182 | NONE => raise ERROR ("rls \""^ rls' ^ "\" missing in Know_Store.\n" ^
183 "TODO exception hierarchy needs to be established.")
185 fun assoc_calc thy calID = let
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;
192 fun assoc_calc' thy key = let
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;
199 fun assoc_cas thy key = assoc (KEStore_Elems.get_cas thy, key);
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;
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>
209 section \<open>determine sequence of main parts in thehier\<close>
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"])]
220 section \<open>Functions for checking KEStore_Elems\<close>
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 ^ "))";
233 fun check_kestore_calc ((id, (c, _)) : Rule_Def.calc) = "(" ^ id ^ ", (" ^ c ^ ", fn))";
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 ^ ")";
240 fun count_kestore_ptyps [] = 0
241 | count_kestore_ptyps ((Celem1.Ptyp (_, _, ps)) :: ps') =
242 1 + count_kestore_ptyps ps + count_kestore_ptyps ps';
243 fun check_kestore_ptyp' strfun (Celem1.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 ((Celem1.Ptyp (s1, _, _)), (Celem1.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 ((Celem1.Ptyp (key, pbts, ps)) :: ps') =
250 ((Celem1.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;
254 fun metguh2str ({guh,...} : Celem.met) = guh : string;
255 fun check_kestore_met (mp: Celem.met Celem1.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;
260 fun check_kestore_thes thes = ((map writeln) o (map (check_kestore_ptyp' Celem.thes2str))) thes
261 fun write_thes thydata_list =
263 |> map (fn (id, the) => (Celem.theID2str id, Celem.the2str the))