run Know_Store independent from Celem. in calcelements.sml
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*)
43 section \<open>Knowledge elements for problems and methods\<close>
45 (* Knowledge (and Exercises) are held by "Know_Store" in Isac's Java front-end.
46 In the front-end Knowledge comprises theories, problems and methods.
47 Elements of problems and methods are defined in theories alongside
48 the development of respective language elements.
49 However, the structure of methods and problems is independent from theories'
50 deductive structure. Thus respective structures are built in Build_Thydata.thy.
52 Most elements of problems and methods are implemented in "Knowledge/", but some
53 of them are implemented in "ProgLang/" already; thus "Know_Store.thy" got this
54 location in the directory structure.
56 get_* retrieves all * of the respective theory PLUS of all ancestor theories.
58 signature KESTORE_ELEMS =
60 val get_rlss: theory -> (Rule_Set.id * (ThyC.id * Rule_Set.T)) list
61 val add_rlss: (Rule_Set.id * (ThyC.id * Rule_Set.T)) list -> theory -> theory
62 val get_calcs: theory -> (Exec_Def.prog_calcID * (Exec_Def.calID * Exec_Def.eval_fn)) list
63 val add_calcs: (Exec_Def.prog_calcID * (Exec_Def.calID * Exec_Def.eval_fn)) list -> theory -> theory
64 val get_cas: theory -> Celem7.cas_elem list
65 val add_cas: Celem7.cas_elem list -> theory -> theory
66 val get_ptyps: theory -> Celem5.ptyps
67 val add_pbts: (Celem5.pbt * Celem3.pblID) list -> theory -> theory
68 val get_mets: theory -> Celem6.mets
69 val add_mets: (Celem6.met * Celem3.metID) list -> theory -> theory
70 val get_thes: theory -> (Celem8.thydata Celem1.ptyp) list
71 val add_thes: (Celem8.thydata * Celem8.theID) list -> theory -> theory (* thydata dropped at existing elems *)
72 val insert_fillpats: (Celem8.theID * Error_Fill_Def.fillpat list) list -> theory -> theory
73 val get_ref_thy: unit -> theory
74 val set_ref_thy: theory -> unit
77 structure KEStore_Elems: KESTORE_ELEMS =
79 fun union_overwrite eq l1 l2 = fold (insert eq) l2 (*..swapped..*) l1;
81 structure Data = Theory_Data (
82 type T = (Rule_Set.id * (ThyC.id * Rule_Set.T)) list;
85 val merge = Rule_Set.to_kestore;
87 fun get_rlss thy = Data.get thy
88 fun add_rlss rlss = Data.map (union_overwrite Rule_Set.equal rlss)
90 structure Data = Theory_Data (
91 type T = (Exec_Def.prog_calcID * (Exec_Def.calID * Exec_Def.eval_fn)) list;
94 val merge = merge Exec_Def.calc_eq;
96 fun get_calcs thy = Data.get thy
97 fun add_calcs calcs = Data.map (union_overwrite Exec_Def.calc_eq calcs)
99 structure Data = Theory_Data (
100 type T = (term * (Celem3.spec * (term list -> (term * term list) list))) list;
103 val merge = merge Celem7.cas_eq;
105 fun get_cas thy = Data.get thy
106 fun add_cas cas = Data.map (union_overwrite Celem7.cas_eq cas)
108 structure Data = Theory_Data (
109 type T = Celem5.ptyps;
110 val empty = [Celem5.e_Ptyp];
112 val merge = Celem1.merge_ptyps;
114 fun get_ptyps thy = Data.get thy;
115 fun add_pbts pbts thy = let
116 fun add_pbt (pbt as {guh,...}, pblID) =
117 (* the pblID has the leaf-element as first; better readability achieved *)
118 (if (!Celem91.check_guhs_unique) then Celem91.check_pblguh_unique guh (Data.get thy) else ();
119 rev pblID |> Celem1.insrt pblID pbt);
120 in Data.map (fold add_pbt pbts) thy end;
122 structure Data = Theory_Data (
123 type T = Celem6.mets;
124 val empty = [Celem6.e_Mets];
126 val merge = Celem1.merge_ptyps;
128 val get_mets = Data.get;
129 fun add_mets mets thy = let
130 fun add_met (met as {guh,...}, metID) =
131 (if (!Celem91.check_guhs_unique) then Celem91.check_metguh_unique guh (Data.get thy) else ();
132 Celem1.insrt metID met metID);
133 in Data.map (fold add_met mets) thy end;
135 structure Data = Theory_Data (
136 type T = (Celem8.thydata Celem1.ptyp) list;
139 val merge = Celem1.merge_ptyps; (* relevant for store_thm, store_rls *)
141 fun get_thes thy = Data.get thy
142 fun add_thes thes thy = let
143 fun add_the (thydata, theID) = Celem8.add_thydata ([], theID) thydata
144 in Data.map (fold add_the thes) thy end;
145 fun insert_fillpats fis thy =
147 fun update_elem (theID, fillpats) =
149 val hthm = Celem1.get_py (Data.get thy) theID theID
150 val hthm' = Celem8.update_hthm hthm fillpats
152 error ("insert_fillpats: " ^ strs2str theID ^ "must address a theorem")
153 in Celem1.update_ptyps theID theID hthm' end
154 in Data.map (fold update_elem fis) thy end
156 val cur_thy = Synchronized.var "finally_knowledge_complete" @{theory};
157 fun set_ref_thy thy = Synchronized.change cur_thy (fn _ => thy); (* never RE-set ! *)
158 fun get_ref_thy () = Synchronized.value cur_thy;
162 section \<open>Re-use existing access functions for knowledge elements\<close>
164 The independence of problems' and methods' structure enforces the accesse
165 functions to use "Isac_Knowledge", the final theory which comprises all knowledge defined.
168 val get_ref_thy = KEStore_Elems.get_ref_thy;
170 fun assoc_rls (rls' : Rule_Set.id) =
171 case AList.lookup (op =) (KEStore_Elems.get_rlss (ThyC.get_theory "Isac_Knowledge")) rls' of
173 | NONE => raise ERROR ("rls \""^ rls' ^ "\" missing in Know_Store.\n" ^
174 "TODO exception hierarchy needs to be established.")
176 fun assoc_rls' thy (rls' : Rule_Set.id) =
177 case AList.lookup (op =) (KEStore_Elems.get_rlss thy) rls' of
179 | NONE => raise ERROR ("rls \""^ rls' ^ "\" missing in Know_Store.\n" ^
180 "TODO exception hierarchy needs to be established.")
182 fun assoc_calc thy calID = let
184 error ("assoc_calc: '" ^ key ^ "' not found in theory " ^ (Context.theory_name thy))
185 | ass ((calc, (keyi, _)) :: pairs, key) =
186 if key = keyi then calc else ass (pairs, key);
187 in ass (thy |> KEStore_Elems.get_calcs, calID) end;
189 fun assoc_calc' thy key = let
191 error ("assoc_calc': '" ^ key' ^ "' not found in theory " ^ (Context.theory_name thy))
192 | ass ((all as (keyi, _)) :: pairs, key') =
193 if key' = keyi then all else ass (pairs, key');
194 in ass (KEStore_Elems.get_calcs thy, key) end;
196 fun assoc_cas thy key = assoc (KEStore_Elems.get_cas thy, key);
198 fun get_ptyps () = get_ref_thy () |> KEStore_Elems.get_ptyps;
199 fun get_mets () = get_ref_thy () |> KEStore_Elems.get_mets;
200 fun get_thes () = get_ref_thy () |> KEStore_Elems.get_thes;
202 setup \<open>KEStore_Elems.add_rlss
203 [("empty", (Context.theory_name @{theory}, Rule_Set.empty)),
204 ("e_rrls", (Context.theory_name @{theory}, Rule_Set.e_rrls))]\<close>
206 section \<open>determine sequence of main parts in thehier\<close>
208 KEStore_Elems.add_thes
209 [(Celem8.Html {guh = Celem8.part2guh ["IsacKnowledge"], html = "",
210 mathauthors = ["Isac team"], coursedesign = []}, ["IsacKnowledge"]),
211 (Celem8.Html {guh = Celem8.part2guh ["Isabelle"], html = "",
212 mathauthors = ["Isabelle team, TU Munich"], coursedesign = []}, ["Isabelle"]),
213 (Celem8.Html {guh = Celem8.part2guh ["IsacScripts"], html = "",
214 mathauthors = ["Isac team"], coursedesign = []}, ["IsacScripts"])]
217 section \<open>Functions for checking KEStore_Elems\<close>
219 fun short_string_of_rls Rule_Set.Empty = "Erls"
220 | short_string_of_rls (Rule_Def.Repeat {calc, rules, ...}) =
221 "Rls {#calc = " ^ string_of_int (length calc) ^
222 ", #rules = " ^ string_of_int (length rules) ^ ", ..."
223 | short_string_of_rls (Rule_Set.Sequence {calc, rules, ...}) =
224 "Seq {#calc = " ^ string_of_int (length calc) ^
225 ", #rules = " ^ string_of_int (length rules) ^ ", ..."
226 | short_string_of_rls (Rule_Set.Rrls _) = "Rrls {...}";
227 fun check_kestore_rls (rls', (thyID, rls)) =
228 "(" ^ rls' ^ ", (" ^ thyID ^ ", " ^ short_string_of_rls rls ^ "))";
230 fun check_kestore_calc ((id, (c, _)) : Rule_Def.calc) = "(" ^ id ^ ", (" ^ c ^ ", fn))";
232 (* we avoid term_to_string''' defined later *)
233 fun check_kestore_cas ((t, (s, _)) : Celem7.cas_elem) =
234 "(" ^ (Print_Mode.setmp [] (Syntax.string_of_term (Config.put show_markup false
235 (Proof_Context.init_global @{theory})))) t ^ ", " ^ Celem3.spec2str s ^ ")";
237 fun count_kestore_ptyps [] = 0
238 | count_kestore_ptyps ((Celem1.Ptyp (_, _, ps)) :: ps') =
239 1 + count_kestore_ptyps ps + count_kestore_ptyps ps';
240 fun check_kestore_ptyp' strfun (Celem1.Ptyp (key, pbts, pts)) = "Ptyp (" ^ (quote key) ^ ", " ^
241 (strfun pbts) ^ ", " ^ (map (check_kestore_ptyp' strfun) pts |> list2str) ^ ")" |> linefeed;
242 val check_kestore_ptyp = check_kestore_ptyp' Celem5.pbts2str;
243 fun ptyp_ord ((Celem1.Ptyp (s1, _, _)), (Celem1.Ptyp (s2, _, _))) = string_ord (s1, s2);
244 fun pbt_ord ({guh = guh'1, ...} : Celem5.pbt, {guh = guh'2, ...} : Celem5.pbt) = string_ord (guh'1, guh'2);
245 fun sort_kestore_ptyp' _ [] = []
246 | sort_kestore_ptyp' ordfun ((Celem1.Ptyp (key, pbts, ps)) :: ps') =
247 ((Celem1.Ptyp (key, sort ordfun pbts, sort_kestore_ptyp' ordfun ps |> sort ptyp_ord))
248 :: sort_kestore_ptyp' ordfun ps');
249 val sort_kestore_ptyp = sort_kestore_ptyp' pbt_ord;
251 fun metguh2str ({guh,...} : Celem6.met) = guh : string;
252 fun check_kestore_met (mp: Celem6.met Celem1.ptyp) =
253 check_kestore_ptyp' (fn xs => map metguh2str xs |> strs2str) mp;
254 fun met_ord ({guh = guh'1, ...} : Celem6.met, {guh = guh'2, ...} : Celem6.met) = string_ord (guh'1, guh'2);
255 val sort_kestore_met = sort_kestore_ptyp' met_ord;
257 fun check_kestore_thes thes = ((map writeln) o (map (check_kestore_ptyp' Celem8.thes2str))) thes
258 fun write_thes thydata_list =
260 |> map (fn (id, the) => (Celem8.theID2str id, Celem8.the2str the))