conditional compilation via system option "isac_test" and antiquotation \<^isac_test>CARTOUCHE:
option is provided in session ROOT, or interactively via $ISABELLE_HOME_USER/etc/preferences (i.e. Isabelle/jEdit plugin preferences);
1 (* Title: src/Tools/isac/Know_Store.thy
2 Author: Mathias Lehnfeld
4 Calc work on Problem employing MethodC; 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_Write, 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
22 ML_Antiquotation.conditional \<^binding>\<open>isac_test\<close>
23 (fn _ => Options.default_bool \<^system_option>\<open>isac_test\<close>)
29 ML_file "rule-def.sml"
30 ML_file "thmC-def.sml"
31 ML_file "eval-def.sml" (*rename identifiers by use of struct.id*)
32 ML_file "rewrite-order.sml" (*rename identifiers by use of struct.id*)
34 ML_file "error-pattern-def.sml"
35 ML_file "rule-set.sml"
38 ML_file "check-unique.sml"
39 ML_file "references-def.sml"
40 ML_file "model-pattern.sml"
41 ML_file "problem-def.sml"
42 ML_file "method-def.sml"
44 ML_file "thy-write.sml"
50 section \<open>Knowledge elements for problems and methods\<close>
52 (* Knowledge (and Exercises) are held by "Know_Store" in Isac's Java front-end.
53 In the front-end Knowledge comprises theories, problems and methods.
54 Elements of problems and methods are defined in theories alongside
55 the development of respective language elements.
56 However, the structure of methods and problems is independent from theories'
57 deductive structure. Thus respective structures are built in Build_Thydata.thy.
59 Most elements of problems and methods are implemented in "Knowledge/", but some
60 of them are implemented in "ProgLang/" already; thus "Know_Store.thy" got this
61 location in the directory structure.
63 get_* retrieves all * of the respective theory PLUS of all ancestor theories.
65 signature KESTORE_ELEMS =
67 val get_rlss: theory -> (Rule_Set.id * (ThyC.id * Rule_Set.T)) list
68 val add_rlss: (Rule_Set.id * (ThyC.id * Rule_Set.T)) list -> theory -> theory
69 val get_calcs: theory -> (Eval_Def.prog_calcID * (Eval_Def.calID * Eval_Def.eval_fn)) list
70 val add_calcs: (Eval_Def.prog_calcID * (Eval_Def.calID * Eval_Def.eval_fn)) list -> theory -> theory
71 val get_cas: theory -> CAS_Def.T list
72 val add_cas: CAS_Def.T list -> theory -> theory
73 val get_ptyps: theory -> Probl_Def.store
74 val add_pbts: (Probl_Def.T * References_Def.id) list -> theory -> theory
75 val get_mets: theory -> Meth_Def.store
76 val add_mets: (Meth_Def.T * References_Def.id) list -> theory -> theory
77 val get_thes: theory -> (Thy_Write.thydata Store.node) list
78 val add_thes: (Thy_Write.thydata * Thy_Write.theID) list -> theory -> theory (* thydata dropped at existing elems *)
79 val insert_fillpats: (Thy_Write.theID * Error_Pattern_Def.fill_in list) list -> theory -> theory
80 val get_ref_thy: unit -> theory
81 val set_ref_thy: theory -> unit
84 structure KEStore_Elems: KESTORE_ELEMS =
86 fun union_overwrite eq l1 l2 = fold (insert eq) l2 (*..swapped..*) l1;
88 structure Data = Theory_Data (
89 type T = (Rule_Set.id * (ThyC.id * Rule_Set.T)) list;
92 val merge = Rule_Set.to_kestore;
94 fun get_rlss thy = Data.get thy
95 fun add_rlss rlss = Data.map (union_overwrite Rule_Set.equal rlss)
97 structure Data = Theory_Data (
98 type T = (Eval_Def.prog_calcID * (Eval_Def.calID * Eval_Def.eval_fn)) list;
101 val merge = merge Eval_Def.calc_eq;
103 fun get_calcs thy = Data.get thy
104 fun add_calcs calcs = Data.map (union_overwrite Eval_Def.calc_eq calcs)
106 structure Data = Theory_Data (
107 type T = (term * (References_Def.T * (term list -> (term * term list) list))) list;
110 val merge = merge CAS_Def.equal;
112 fun get_cas thy = Data.get thy
113 fun add_cas cas = Data.map (union_overwrite CAS_Def.equal cas)
115 structure Data = Theory_Data (
116 type T = Probl_Def.store;
117 val empty = [Probl_Def.empty_store];
119 val merge = Store.merge;
121 fun get_ptyps thy = Data.get thy;
122 fun add_pbts pbts thy = let
123 fun add_pbt (pbt as {guh,...}, pblID) =
124 (* the pblID has the leaf-element as first; better readability achieved *)
125 (if (!Check_Unique.on) then Probl_Def.check_unique guh (Data.get thy) else ();
126 rev pblID |> Store.insert pblID pbt);
127 in Data.map (fold add_pbt pbts) thy end;
129 structure Data = Theory_Data (
130 type T = Meth_Def.store;
131 val empty = [Meth_Def.empty_store];
133 val merge = Store.merge;
135 val get_mets = Data.get;
136 fun add_mets mets thy = let
137 fun add_met (met as {guh,...}, metID) =
138 (if (!Check_Unique.on) then Meth_Def.check_unique guh (Data.get thy) else ();
139 Store.insert metID met metID);
140 in Data.map (fold add_met mets) thy end;
142 structure Data = Theory_Data (
143 type T = (Thy_Write.thydata Store.node) list;
146 val merge = Store.merge; (* relevant for store_thm, store_rls *)
148 fun get_thes thy = Data.get thy
149 fun add_thes thes thy = let
150 fun add_the (thydata, theID) = Thy_Write.add_thydata ([], theID) thydata
151 in Data.map (fold add_the thes) thy end;
152 fun insert_fillpats fis thy =
154 fun update_elem (theID, fillpats) =
156 val hthm = Store.get (Data.get thy) theID theID
157 val hthm' = Thy_Write.update_hthm hthm fillpats
159 raise ERROR ("insert_fillpats: " ^ strs2str theID ^ "must address a theorem")
160 in Store.update theID theID hthm' end
161 in Data.map (fold update_elem fis) thy end
163 val cur_thy = Synchronized.var "finally_knowledge_complete" @{theory};
164 fun set_ref_thy thy = Synchronized.change cur_thy (fn _ => thy); (* never RE-set ! *)
165 fun get_ref_thy () = Synchronized.value cur_thy;
169 section \<open>Re-use existing access functions for knowledge elements\<close>
171 The independence of problems' and methods' structure enforces the accesse
172 functions to use "Isac_Knowledge", the final theory which comprises all knowledge defined.
175 val get_ref_thy = KEStore_Elems.get_ref_thy;
177 fun assoc_rls (rls' : Rule_Set.id) =
178 case AList.lookup (op =) (KEStore_Elems.get_rlss (ThyC.get_theory "Isac_Knowledge")) rls' of
180 | NONE => raise ERROR ("rls \""^ rls' ^ "\" missing in Know_Store.\n" ^
181 "TODO exception hierarchy needs to be established.")
183 fun assoc_rls' thy (rls' : Rule_Set.id) =
184 case AList.lookup (op =) (KEStore_Elems.get_rlss thy) rls' of
186 | NONE => raise ERROR ("rls \""^ rls' ^ "\" missing in Know_Store.\n" ^
187 "TODO exception hierarchy needs to be established.")
189 fun assoc_calc thy calID = let
191 raise ERROR ("assoc_calc: '" ^ key ^ "' not found in theory " ^ (Context.theory_name thy))
192 | ass ((calc, (keyi, _)) :: pairs, key) =
193 if key = keyi then calc else ass (pairs, key);
194 in ass (thy |> KEStore_Elems.get_calcs, calID) end;
196 fun assoc_calc' thy key = let
198 raise ERROR ("assoc_calc': '" ^ key' ^ "' not found in theory " ^ (Context.theory_name thy))
199 | ass ((all as (keyi, _)) :: pairs, key') =
200 if key' = keyi then all else ass (pairs, key');
201 in ass (KEStore_Elems.get_calcs thy, key) end;
203 fun assoc_cas thy key = assoc (KEStore_Elems.get_cas thy, key);
205 fun get_ptyps () = get_ref_thy () |> KEStore_Elems.get_ptyps;
206 fun get_mets () = get_ref_thy () |> KEStore_Elems.get_mets;
207 fun get_thes () = get_ref_thy () |> KEStore_Elems.get_thes;
209 setup \<open>KEStore_Elems.add_rlss
210 [("empty", (Context.theory_name @{theory}, Rule_Set.empty)),
211 ("e_rrls", (Context.theory_name @{theory}, Rule_Set.e_rrls))]\<close>
213 section \<open>determine sequence of main parts in thehier\<close>
215 KEStore_Elems.add_thes
216 [(Thy_Write.Html {guh = Thy_Write.part2guh ["IsacKnowledge"], html = "",
217 mathauthors = ["Isac team"], coursedesign = []}, ["IsacKnowledge"]),
218 (Thy_Write.Html {guh = Thy_Write.part2guh ["Isabelle"], html = "",
219 mathauthors = ["Isabelle team, TU Munich"], coursedesign = []}, ["Isabelle"]),
220 (Thy_Write.Html {guh = Thy_Write.part2guh ["IsacScripts"], html = "",
221 mathauthors = ["Isac team"], coursedesign = []}, ["IsacScripts"])]
224 section \<open>Functions for checking KEStore_Elems\<close>
226 fun short_string_of_rls Rule_Set.Empty = "Erls"
227 | short_string_of_rls (Rule_Def.Repeat {calc, rules, ...}) =
228 "Rls {#calc = " ^ string_of_int (length calc) ^
229 ", #rules = " ^ string_of_int (length rules) ^ ", ..."
230 | short_string_of_rls (Rule_Set.Sequence {calc, rules, ...}) =
231 "Seq {#calc = " ^ string_of_int (length calc) ^
232 ", #rules = " ^ string_of_int (length rules) ^ ", ..."
233 | short_string_of_rls (Rule_Set.Rrls _) = "Rrls {...}";
234 fun check_kestore_rls (rls', (thyID, rls)) =
235 "(" ^ rls' ^ ", (" ^ thyID ^ ", " ^ short_string_of_rls rls ^ "))";
237 fun check_kestore_calc ((id, (c, _)) : Rule_Def.calc) = "(" ^ id ^ ", (" ^ c ^ ", fn))";
239 (* we avoid term_to_string''' defined later *)
240 fun check_kestore_cas ((t, (s, _)) : CAS_Def.T) =
241 "(" ^ (Print_Mode.setmp [] (Syntax.string_of_term (Config.put show_markup false
242 (Proof_Context.init_global @{theory})))) t ^ ", " ^ References_Def.to_string s ^ ")";
244 fun count_kestore_ptyps [] = 0
245 | count_kestore_ptyps ((Store.Node (_, _, ps)) :: ps') =
246 1 + count_kestore_ptyps ps + count_kestore_ptyps ps';
247 fun check_kestore_ptyp' strfun (Store.Node (key, pbts, pts)) = "Ptyp (" ^ (quote key) ^ ", " ^
248 (strfun pbts) ^ ", " ^ (map (check_kestore_ptyp' strfun) pts |> list2str) ^ ")" |> linefeed;
249 val check_kestore_ptyp = check_kestore_ptyp' Probl_Def.s_to_string;
250 fun ptyp_ord ((Store.Node (s1, _, _)), (Store.Node (s2, _, _))) = string_ord (s1, s2);
251 fun pbt_ord ({guh = guh'1, ...} : Probl_Def.T, {guh = guh'2, ...} : Probl_Def.T) = string_ord (guh'1, guh'2);
252 fun sort_kestore_ptyp' _ [] = []
253 | sort_kestore_ptyp' ordfun ((Store.Node (key, pbts, ps)) :: ps') =
254 ((Store.Node (key, sort ordfun pbts, sort_kestore_ptyp' ordfun ps |> sort ptyp_ord))
255 :: sort_kestore_ptyp' ordfun ps');
256 val sort_kestore_ptyp = sort_kestore_ptyp' pbt_ord;
258 fun metguh2str ({guh,...} : Meth_Def.T) = guh : string;
259 fun check_kestore_met (mp: Meth_Def.T Store.node) =
260 check_kestore_ptyp' (fn xs => map metguh2str xs |> strs2str) mp;
261 fun met_ord ({guh = guh'1, ...} : Meth_Def.T, {guh = guh'2, ...} : Meth_Def.T) = string_ord (guh'1, guh'2);
262 val sort_kestore_met = sort_kestore_ptyp' met_ord;
264 fun check_kestore_thes thes = ((map writeln) o (map (check_kestore_ptyp' Thy_Write.thes2str))) thes
265 fun write_thes thydata_list =
267 |> map (fn (id, the) => (Thy_Write.theID2str id, Thy_Write.the2str the))