walther@59887
|
1 |
(* Title: src/Tools/isac/Know_Store.thy
|
wneuper@59586
|
2 |
Author: Mathias Lehnfeld
|
walther@59871
|
3 |
|
walther@59890
|
4 |
Calc work on Problem employing Method; both are collected in a respective Store;
|
walther@59890
|
5 |
The collections' structure is independent from the dependency graph of Isabelle's theories
|
walther@59890
|
6 |
in Knowledge.
|
walther@59917
|
7 |
Store is also used by Thy_Write, required for Isac's Java front end, irrelevant for PIDE.
|
walther@59890
|
8 |
|
walther@59887
|
9 |
The files (in "xxxxx-def.sml") contain definitions required for Know_Store;
|
walther@59871
|
10 |
they also include minimal code required for other "xxxxx-def.sml" files.
|
walther@59871
|
11 |
These files have companion files "xxxxx.sml" with all further code,
|
walther@59871
|
12 |
located at appropriate positions in the file structure.
|
walther@59871
|
13 |
|
walther@59871
|
14 |
The separation of "xxxxx-def.sml" from "xxxxx.sml" should be overcome by
|
walther@59871
|
15 |
appropriate use of polymorphic high order functions.
|
wneuper@59586
|
16 |
*)
|
wneuper@59586
|
17 |
|
walther@59887
|
18 |
theory Know_Store imports Complex_Main
|
wneuper@59586
|
19 |
|
wneuper@59586
|
20 |
begin
|
wneuper@59586
|
21 |
ML_file libraryC.sml
|
walther@59880
|
22 |
ML_file theoryC.sml
|
walther@59868
|
23 |
ML_file unparseC.sml
|
walther@59874
|
24 |
ML_file "rule-def.sml"
|
walther@59875
|
25 |
ML_file "thmC-def.sml"
|
walther@59919
|
26 |
ML_file "eval-def.sml" (*rename identifiers by use of struct.id*)
|
walther@59867
|
27 |
ML_file "rewrite-order.sml" (*rename identifiers by use of struct.id*)
|
wneuper@59586
|
28 |
ML_file rule.sml
|
walther@59909
|
29 |
ML_file "error-pattern-def.sml"
|
walther@59850
|
30 |
ML_file "rule-set.sml"
|
walther@59882
|
31 |
|
walther@59891
|
32 |
ML_file "store.sml"
|
walther@59892
|
33 |
ML_file "check-unique.sml"
|
walther@59891
|
34 |
ML_file "specification.sml"
|
walther@59884
|
35 |
ML_file "celem-4.sml" (*pat*)
|
walther@59893
|
36 |
ML_file "problem-def.sml"
|
walther@59893
|
37 |
ML_file "method-def.sml"
|
walther@59893
|
38 |
ML_file "cas-def.sml"
|
walther@59917
|
39 |
ML_file "thy-write.sml"
|
walther@59882
|
40 |
|
wneuper@59586
|
41 |
ML \<open>
|
wneuper@59586
|
42 |
\<close> ML \<open>
|
wneuper@59587
|
43 |
\<close> ML \<open>
|
wneuper@59586
|
44 |
\<close>
|
wneuper@59586
|
45 |
section \<open>Knowledge elements for problems and methods\<close>
|
wneuper@59586
|
46 |
ML \<open>
|
walther@59887
|
47 |
(* Knowledge (and Exercises) are held by "Know_Store" in Isac's Java front-end.
|
wneuper@59586
|
48 |
In the front-end Knowledge comprises theories, problems and methods.
|
wneuper@59586
|
49 |
Elements of problems and methods are defined in theories alongside
|
wneuper@59586
|
50 |
the development of respective language elements.
|
wneuper@59586
|
51 |
However, the structure of methods and problems is independent from theories'
|
wneuper@59586
|
52 |
deductive structure. Thus respective structures are built in Build_Thydata.thy.
|
wneuper@59586
|
53 |
|
wneuper@59586
|
54 |
Most elements of problems and methods are implemented in "Knowledge/", but some
|
walther@59887
|
55 |
of them are implemented in "ProgLang/" already; thus "Know_Store.thy" got this
|
wneuper@59586
|
56 |
location in the directory structure.
|
wneuper@59586
|
57 |
|
wneuper@59586
|
58 |
get_* retrieves all * of the respective theory PLUS of all ancestor theories.
|
wneuper@59586
|
59 |
*)
|
wneuper@59586
|
60 |
signature KESTORE_ELEMS =
|
wneuper@59586
|
61 |
sig
|
walther@59879
|
62 |
val get_rlss: theory -> (Rule_Set.id * (ThyC.id * Rule_Set.T)) list
|
walther@59879
|
63 |
val add_rlss: (Rule_Set.id * (ThyC.id * Rule_Set.T)) list -> theory -> theory
|
walther@59919
|
64 |
val get_calcs: theory -> (Eval_Def.prog_calcID * (Eval_Def.calID * Eval_Def.eval_fn)) list
|
walther@59919
|
65 |
val add_calcs: (Eval_Def.prog_calcID * (Eval_Def.calID * Eval_Def.eval_fn)) list -> theory -> theory
|
walther@59896
|
66 |
val get_cas: theory -> CAS_Def.T list
|
walther@59896
|
67 |
val add_cas: CAS_Def.T list -> theory -> theory
|
walther@59894
|
68 |
val get_ptyps: theory -> Probl_Def.store
|
walther@59903
|
69 |
val add_pbts: (Probl_Def.T * Spec.id) list -> theory -> theory
|
walther@59895
|
70 |
val get_mets: theory -> Meth_Def.store
|
walther@59903
|
71 |
val add_mets: (Meth_Def.T * Spec.id) list -> theory -> theory
|
walther@59917
|
72 |
val get_thes: theory -> (Thy_Write.thydata Store.node) list
|
walther@59917
|
73 |
val add_thes: (Thy_Write.thydata * Thy_Write.theID) list -> theory -> theory (* thydata dropped at existing elems *)
|
walther@59917
|
74 |
val insert_fillpats: (Thy_Write.theID * Error_Pattern_Def.fill_in list) list -> theory -> theory
|
wneuper@59586
|
75 |
val get_ref_thy: unit -> theory
|
wneuper@59586
|
76 |
val set_ref_thy: theory -> unit
|
wneuper@59586
|
77 |
end;
|
wneuper@59586
|
78 |
|
wneuper@59586
|
79 |
structure KEStore_Elems: KESTORE_ELEMS =
|
wneuper@59586
|
80 |
struct
|
wneuper@59586
|
81 |
fun union_overwrite eq l1 l2 = fold (insert eq) l2 (*..swapped..*) l1;
|
wneuper@59586
|
82 |
|
wneuper@59586
|
83 |
structure Data = Theory_Data (
|
walther@59879
|
84 |
type T = (Rule_Set.id * (ThyC.id * Rule_Set.T)) list;
|
wneuper@59586
|
85 |
val empty = [];
|
wneuper@59586
|
86 |
val extend = I;
|
walther@59852
|
87 |
val merge = Rule_Set.to_kestore;
|
wneuper@59586
|
88 |
);
|
wneuper@59586
|
89 |
fun get_rlss thy = Data.get thy
|
walther@59852
|
90 |
fun add_rlss rlss = Data.map (union_overwrite Rule_Set.equal rlss)
|
wneuper@59586
|
91 |
|
wneuper@59586
|
92 |
structure Data = Theory_Data (
|
walther@59919
|
93 |
type T = (Eval_Def.prog_calcID * (Eval_Def.calID * Eval_Def.eval_fn)) list;
|
wneuper@59586
|
94 |
val empty = [];
|
wneuper@59586
|
95 |
val extend = I;
|
walther@59919
|
96 |
val merge = merge Eval_Def.calc_eq;
|
wneuper@59586
|
97 |
);
|
wneuper@59586
|
98 |
fun get_calcs thy = Data.get thy
|
walther@59919
|
99 |
fun add_calcs calcs = Data.map (union_overwrite Eval_Def.calc_eq calcs)
|
wneuper@59586
|
100 |
|
wneuper@59586
|
101 |
structure Data = Theory_Data (
|
walther@59903
|
102 |
type T = (term * (Spec.T * (term list -> (term * term list) list))) list;
|
wneuper@59586
|
103 |
val empty = [];
|
wneuper@59586
|
104 |
val extend = I;
|
walther@59896
|
105 |
val merge = merge CAS_Def.equal;
|
wneuper@59586
|
106 |
);
|
wneuper@59586
|
107 |
fun get_cas thy = Data.get thy
|
walther@59896
|
108 |
fun add_cas cas = Data.map (union_overwrite CAS_Def.equal cas)
|
wneuper@59586
|
109 |
|
wneuper@59586
|
110 |
structure Data = Theory_Data (
|
walther@59894
|
111 |
type T = Probl_Def.store;
|
walther@59894
|
112 |
val empty = [Probl_Def.empty_store];
|
wneuper@59586
|
113 |
val extend = I;
|
walther@59897
|
114 |
val merge = Store.merge;
|
wneuper@59586
|
115 |
);
|
wneuper@59586
|
116 |
fun get_ptyps thy = Data.get thy;
|
wneuper@59586
|
117 |
fun add_pbts pbts thy = let
|
wneuper@59586
|
118 |
fun add_pbt (pbt as {guh,...}, pblID) =
|
wneuper@59586
|
119 |
(* the pblID has the leaf-element as first; better readability achieved *)
|
walther@59904
|
120 |
(if (!Check_Unique.on) then Probl_Def.check_unique guh (Data.get thy) else ();
|
walther@59897
|
121 |
rev pblID |> Store.insert pblID pbt);
|
wneuper@59586
|
122 |
in Data.map (fold add_pbt pbts) thy end;
|
wneuper@59586
|
123 |
|
wneuper@59586
|
124 |
structure Data = Theory_Data (
|
walther@59895
|
125 |
type T = Meth_Def.store;
|
walther@59895
|
126 |
val empty = [Meth_Def.empty_store];
|
wneuper@59586
|
127 |
val extend = I;
|
walther@59897
|
128 |
val merge = Store.merge;
|
wneuper@59586
|
129 |
);
|
wneuper@59586
|
130 |
val get_mets = Data.get;
|
wneuper@59586
|
131 |
fun add_mets mets thy = let
|
wneuper@59586
|
132 |
fun add_met (met as {guh,...}, metID) =
|
walther@59904
|
133 |
(if (!Check_Unique.on) then Meth_Def.check_unique guh (Data.get thy) else ();
|
walther@59897
|
134 |
Store.insert metID met metID);
|
wneuper@59586
|
135 |
in Data.map (fold add_met mets) thy end;
|
wneuper@59586
|
136 |
|
wneuper@59586
|
137 |
structure Data = Theory_Data (
|
walther@59917
|
138 |
type T = (Thy_Write.thydata Store.node) list;
|
wneuper@59586
|
139 |
val empty = [];
|
wneuper@59586
|
140 |
val extend = I;
|
walther@59897
|
141 |
val merge = Store.merge; (* relevant for store_thm, store_rls *)
|
wneuper@59586
|
142 |
);
|
wneuper@59586
|
143 |
fun get_thes thy = Data.get thy
|
wneuper@59586
|
144 |
fun add_thes thes thy = let
|
walther@59917
|
145 |
fun add_the (thydata, theID) = Thy_Write.add_thydata ([], theID) thydata
|
wneuper@59586
|
146 |
in Data.map (fold add_the thes) thy end;
|
wneuper@59586
|
147 |
fun insert_fillpats fis thy =
|
wneuper@59586
|
148 |
let
|
wneuper@59586
|
149 |
fun update_elem (theID, fillpats) =
|
wneuper@59586
|
150 |
let
|
walther@59897
|
151 |
val hthm = Store.get (Data.get thy) theID theID
|
walther@59917
|
152 |
val hthm' = Thy_Write.update_hthm hthm fillpats
|
wneuper@59586
|
153 |
handle ERROR _ =>
|
wneuper@59586
|
154 |
error ("insert_fillpats: " ^ strs2str theID ^ "must address a theorem")
|
walther@59897
|
155 |
in Store.update theID theID hthm' end
|
wneuper@59586
|
156 |
in Data.map (fold update_elem fis) thy end
|
wneuper@59586
|
157 |
|
wneuper@59586
|
158 |
val cur_thy = Synchronized.var "finally_knowledge_complete" @{theory};
|
wneuper@59586
|
159 |
fun set_ref_thy thy = Synchronized.change cur_thy (fn _ => thy); (* never RE-set ! *)
|
wneuper@59586
|
160 |
fun get_ref_thy () = Synchronized.value cur_thy;
|
wneuper@59586
|
161 |
end;
|
wneuper@59586
|
162 |
\<close>
|
wneuper@59586
|
163 |
|
wneuper@59586
|
164 |
section \<open>Re-use existing access functions for knowledge elements\<close>
|
wneuper@59586
|
165 |
text \<open>
|
wneuper@59586
|
166 |
The independence of problems' and methods' structure enforces the accesse
|
wneuper@59592
|
167 |
functions to use "Isac_Knowledge", the final theory which comprises all knowledge defined.
|
wneuper@59586
|
168 |
\<close>
|
wneuper@59586
|
169 |
ML \<open>
|
wneuper@59586
|
170 |
val get_ref_thy = KEStore_Elems.get_ref_thy;
|
wneuper@59586
|
171 |
|
walther@59867
|
172 |
fun assoc_rls (rls' : Rule_Set.id) =
|
walther@59879
|
173 |
case AList.lookup (op =) (KEStore_Elems.get_rlss (ThyC.get_theory "Isac_Knowledge")) rls' of
|
wneuper@59586
|
174 |
SOME (_, rls) => rls
|
walther@59887
|
175 |
| NONE => raise ERROR ("rls \""^ rls' ^ "\" missing in Know_Store.\n" ^
|
wneuper@59586
|
176 |
"TODO exception hierarchy needs to be established.")
|
wneuper@59586
|
177 |
|
walther@59867
|
178 |
fun assoc_rls' thy (rls' : Rule_Set.id) =
|
wneuper@59586
|
179 |
case AList.lookup (op =) (KEStore_Elems.get_rlss thy) rls' of
|
wneuper@59586
|
180 |
SOME (_, rls) => rls
|
walther@59887
|
181 |
| NONE => raise ERROR ("rls \""^ rls' ^ "\" missing in Know_Store.\n" ^
|
wneuper@59586
|
182 |
"TODO exception hierarchy needs to be established.")
|
wneuper@59586
|
183 |
|
wneuper@59586
|
184 |
fun assoc_calc thy calID = let
|
wneuper@59586
|
185 |
fun ass ([], key) =
|
wneuper@59586
|
186 |
error ("assoc_calc: '" ^ key ^ "' not found in theory " ^ (Context.theory_name thy))
|
wneuper@59586
|
187 |
| ass ((calc, (keyi, _)) :: pairs, key) =
|
wneuper@59586
|
188 |
if key = keyi then calc else ass (pairs, key);
|
wneuper@59586
|
189 |
in ass (thy |> KEStore_Elems.get_calcs, calID) end;
|
wneuper@59586
|
190 |
|
wneuper@59586
|
191 |
fun assoc_calc' thy key = let
|
wneuper@59586
|
192 |
fun ass ([], key') =
|
wneuper@59586
|
193 |
error ("assoc_calc': '" ^ key' ^ "' not found in theory " ^ (Context.theory_name thy))
|
wneuper@59586
|
194 |
| ass ((all as (keyi, _)) :: pairs, key') =
|
wneuper@59586
|
195 |
if key' = keyi then all else ass (pairs, key');
|
wneuper@59586
|
196 |
in ass (KEStore_Elems.get_calcs thy, key) end;
|
wneuper@59586
|
197 |
|
wneuper@59586
|
198 |
fun assoc_cas thy key = assoc (KEStore_Elems.get_cas thy, key);
|
wneuper@59586
|
199 |
|
wneuper@59586
|
200 |
fun get_ptyps () = get_ref_thy () |> KEStore_Elems.get_ptyps;
|
wneuper@59586
|
201 |
fun get_mets () = get_ref_thy () |> KEStore_Elems.get_mets;
|
wneuper@59586
|
202 |
fun get_thes () = get_ref_thy () |> KEStore_Elems.get_thes;
|
wneuper@59586
|
203 |
\<close>
|
wneuper@59586
|
204 |
setup \<open>KEStore_Elems.add_rlss
|
walther@59852
|
205 |
[("empty", (Context.theory_name @{theory}, Rule_Set.empty)),
|
walther@59850
|
206 |
("e_rrls", (Context.theory_name @{theory}, Rule_Set.e_rrls))]\<close>
|
wneuper@59586
|
207 |
|
wneuper@59586
|
208 |
section \<open>determine sequence of main parts in thehier\<close>
|
wneuper@59586
|
209 |
setup \<open>
|
wneuper@59586
|
210 |
KEStore_Elems.add_thes
|
walther@59917
|
211 |
[(Thy_Write.Html {guh = Thy_Write.part2guh ["IsacKnowledge"], html = "",
|
wneuper@59586
|
212 |
mathauthors = ["Isac team"], coursedesign = []}, ["IsacKnowledge"]),
|
walther@59917
|
213 |
(Thy_Write.Html {guh = Thy_Write.part2guh ["Isabelle"], html = "",
|
wneuper@59586
|
214 |
mathauthors = ["Isabelle team, TU Munich"], coursedesign = []}, ["Isabelle"]),
|
walther@59917
|
215 |
(Thy_Write.Html {guh = Thy_Write.part2guh ["IsacScripts"], html = "",
|
wneuper@59586
|
216 |
mathauthors = ["Isac team"], coursedesign = []}, ["IsacScripts"])]
|
wneuper@59586
|
217 |
\<close>
|
wneuper@59586
|
218 |
|
wneuper@59586
|
219 |
section \<open>Functions for checking KEStore_Elems\<close>
|
wneuper@59586
|
220 |
ML \<open>
|
walther@59851
|
221 |
fun short_string_of_rls Rule_Set.Empty = "Erls"
|
walther@59851
|
222 |
| short_string_of_rls (Rule_Def.Repeat {calc, rules, ...}) =
|
wneuper@59586
|
223 |
"Rls {#calc = " ^ string_of_int (length calc) ^
|
wneuper@59586
|
224 |
", #rules = " ^ string_of_int (length rules) ^ ", ..."
|
walther@59878
|
225 |
| short_string_of_rls (Rule_Set.Sequence {calc, rules, ...}) =
|
wneuper@59586
|
226 |
"Seq {#calc = " ^ string_of_int (length calc) ^
|
wneuper@59586
|
227 |
", #rules = " ^ string_of_int (length rules) ^ ", ..."
|
walther@59850
|
228 |
| short_string_of_rls (Rule_Set.Rrls _) = "Rrls {...}";
|
wneuper@59586
|
229 |
fun check_kestore_rls (rls', (thyID, rls)) =
|
wneuper@59586
|
230 |
"(" ^ rls' ^ ", (" ^ thyID ^ ", " ^ short_string_of_rls rls ^ "))";
|
wneuper@59586
|
231 |
|
walther@59852
|
232 |
fun check_kestore_calc ((id, (c, _)) : Rule_Def.calc) = "(" ^ id ^ ", (" ^ c ^ ", fn))";
|
wneuper@59586
|
233 |
|
walther@59846
|
234 |
(* we avoid term_to_string''' defined later *)
|
walther@59896
|
235 |
fun check_kestore_cas ((t, (s, _)) : CAS_Def.T) =
|
walther@59846
|
236 |
"(" ^ (Print_Mode.setmp [] (Syntax.string_of_term (Config.put show_markup false
|
walther@59902
|
237 |
(Proof_Context.init_global @{theory})))) t ^ ", " ^ Spec.to_string s ^ ")";
|
wneuper@59586
|
238 |
|
wneuper@59586
|
239 |
fun count_kestore_ptyps [] = 0
|
walther@59897
|
240 |
| count_kestore_ptyps ((Store.Node (_, _, ps)) :: ps') =
|
wneuper@59586
|
241 |
1 + count_kestore_ptyps ps + count_kestore_ptyps ps';
|
walther@59897
|
242 |
fun check_kestore_ptyp' strfun (Store.Node (key, pbts, pts)) = "Ptyp (" ^ (quote key) ^ ", " ^
|
walther@59888
|
243 |
(strfun pbts) ^ ", " ^ (map (check_kestore_ptyp' strfun) pts |> list2str) ^ ")" |> linefeed;
|
walther@59894
|
244 |
val check_kestore_ptyp = check_kestore_ptyp' Probl_Def.s_to_string;
|
walther@59897
|
245 |
fun ptyp_ord ((Store.Node (s1, _, _)), (Store.Node (s2, _, _))) = string_ord (s1, s2);
|
walther@59894
|
246 |
fun pbt_ord ({guh = guh'1, ...} : Probl_Def.T, {guh = guh'2, ...} : Probl_Def.T) = string_ord (guh'1, guh'2);
|
wneuper@59586
|
247 |
fun sort_kestore_ptyp' _ [] = []
|
walther@59897
|
248 |
| sort_kestore_ptyp' ordfun ((Store.Node (key, pbts, ps)) :: ps') =
|
walther@59897
|
249 |
((Store.Node (key, sort ordfun pbts, sort_kestore_ptyp' ordfun ps |> sort ptyp_ord))
|
wneuper@59586
|
250 |
:: sort_kestore_ptyp' ordfun ps');
|
wneuper@59586
|
251 |
val sort_kestore_ptyp = sort_kestore_ptyp' pbt_ord;
|
wneuper@59586
|
252 |
|
walther@59895
|
253 |
fun metguh2str ({guh,...} : Meth_Def.T) = guh : string;
|
walther@59897
|
254 |
fun check_kestore_met (mp: Meth_Def.T Store.node) =
|
wneuper@59586
|
255 |
check_kestore_ptyp' (fn xs => map metguh2str xs |> strs2str) mp;
|
walther@59895
|
256 |
fun met_ord ({guh = guh'1, ...} : Meth_Def.T, {guh = guh'2, ...} : Meth_Def.T) = string_ord (guh'1, guh'2);
|
wneuper@59586
|
257 |
val sort_kestore_met = sort_kestore_ptyp' met_ord;
|
wneuper@59586
|
258 |
|
walther@59917
|
259 |
fun check_kestore_thes thes = ((map writeln) o (map (check_kestore_ptyp' Thy_Write.thes2str))) thes
|
wneuper@59586
|
260 |
fun write_thes thydata_list =
|
wneuper@59586
|
261 |
thydata_list
|
walther@59917
|
262 |
|> map (fn (id, the) => (Thy_Write.theID2str id, Thy_Write.the2str the))
|
wneuper@59586
|
263 |
|> map pair2str
|
wneuper@59586
|
264 |
|> map writeln
|
wneuper@59586
|
265 |
\<close>
|
wneuper@59586
|
266 |
ML \<open>
|
wneuper@59586
|
267 |
\<close> ML \<open>
|
wneuper@59586
|
268 |
\<close> ML \<open>
|
wneuper@59586
|
269 |
\<close>
|
wneuper@59586
|
270 |
end
|