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@59890
|
7 |
Store is also used by Thy_Html, 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@59867
|
26 |
ML_file "exec-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@59867
|
29 |
ML_file "error-fill-def.sml" (*rename identifiers by use of struct.id*)
|
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@59893
|
39 |
ML_file "thy-html.sml"
|
walther@59882
|
40 |
|
walther@59884
|
41 |
ML_file tracing.sml
|
wneuper@59586
|
42 |
ML \<open>
|
wneuper@59586
|
43 |
\<close> ML \<open>
|
wneuper@59587
|
44 |
\<close> ML \<open>
|
wneuper@59586
|
45 |
\<close>
|
wneuper@59586
|
46 |
section \<open>Knowledge elements for problems and methods\<close>
|
wneuper@59586
|
47 |
ML \<open>
|
walther@59887
|
48 |
(* Knowledge (and Exercises) are held by "Know_Store" in Isac's Java front-end.
|
wneuper@59586
|
49 |
In the front-end Knowledge comprises theories, problems and methods.
|
wneuper@59586
|
50 |
Elements of problems and methods are defined in theories alongside
|
wneuper@59586
|
51 |
the development of respective language elements.
|
wneuper@59586
|
52 |
However, the structure of methods and problems is independent from theories'
|
wneuper@59586
|
53 |
deductive structure. Thus respective structures are built in Build_Thydata.thy.
|
wneuper@59586
|
54 |
|
wneuper@59586
|
55 |
Most elements of problems and methods are implemented in "Knowledge/", but some
|
walther@59887
|
56 |
of them are implemented in "ProgLang/" already; thus "Know_Store.thy" got this
|
wneuper@59586
|
57 |
location in the directory structure.
|
wneuper@59586
|
58 |
|
wneuper@59586
|
59 |
get_* retrieves all * of the respective theory PLUS of all ancestor theories.
|
wneuper@59586
|
60 |
*)
|
wneuper@59586
|
61 |
signature KESTORE_ELEMS =
|
wneuper@59586
|
62 |
sig
|
walther@59879
|
63 |
val get_rlss: theory -> (Rule_Set.id * (ThyC.id * Rule_Set.T)) list
|
walther@59879
|
64 |
val add_rlss: (Rule_Set.id * (ThyC.id * Rule_Set.T)) list -> theory -> theory
|
walther@59854
|
65 |
val get_calcs: theory -> (Exec_Def.prog_calcID * (Exec_Def.calID * Exec_Def.eval_fn)) list
|
walther@59854
|
66 |
val add_calcs: (Exec_Def.prog_calcID * (Exec_Def.calID * Exec_Def.eval_fn)) list -> theory -> theory
|
walther@59893
|
67 |
val get_cas: theory -> CAS_Def.cas_elem list
|
walther@59893
|
68 |
val add_cas: CAS_Def.cas_elem list -> theory -> theory
|
walther@59893
|
69 |
val get_ptyps: theory -> Probl_Def.ptyps
|
walther@59893
|
70 |
val add_pbts: (Probl_Def.pbt * Spec.pblID) list -> theory -> theory
|
walther@59893
|
71 |
val get_mets: theory -> Meth_Def.mets
|
walther@59893
|
72 |
val add_mets: (Meth_Def.met * Spec.metID) list -> theory -> theory
|
walther@59893
|
73 |
val get_thes: theory -> (Thy_Html.thydata Store.ptyp) list
|
walther@59893
|
74 |
val add_thes: (Thy_Html.thydata * Thy_Html.theID) list -> theory -> theory (* thydata dropped at existing elems *)
|
walther@59893
|
75 |
val insert_fillpats: (Thy_Html.theID * Error_Fill_Def.fillpat list) list -> theory -> theory
|
wneuper@59586
|
76 |
val get_ref_thy: unit -> theory
|
wneuper@59586
|
77 |
val set_ref_thy: theory -> unit
|
wneuper@59586
|
78 |
end;
|
wneuper@59586
|
79 |
|
wneuper@59586
|
80 |
structure KEStore_Elems: KESTORE_ELEMS =
|
wneuper@59586
|
81 |
struct
|
wneuper@59586
|
82 |
fun union_overwrite eq l1 l2 = fold (insert eq) l2 (*..swapped..*) l1;
|
wneuper@59586
|
83 |
|
wneuper@59586
|
84 |
structure Data = Theory_Data (
|
walther@59879
|
85 |
type T = (Rule_Set.id * (ThyC.id * Rule_Set.T)) list;
|
wneuper@59586
|
86 |
val empty = [];
|
wneuper@59586
|
87 |
val extend = I;
|
walther@59852
|
88 |
val merge = Rule_Set.to_kestore;
|
wneuper@59586
|
89 |
);
|
wneuper@59586
|
90 |
fun get_rlss thy = Data.get thy
|
walther@59852
|
91 |
fun add_rlss rlss = Data.map (union_overwrite Rule_Set.equal rlss)
|
wneuper@59586
|
92 |
|
wneuper@59586
|
93 |
structure Data = Theory_Data (
|
walther@59854
|
94 |
type T = (Exec_Def.prog_calcID * (Exec_Def.calID * Exec_Def.eval_fn)) list;
|
wneuper@59586
|
95 |
val empty = [];
|
wneuper@59586
|
96 |
val extend = I;
|
walther@59853
|
97 |
val merge = merge Exec_Def.calc_eq;
|
wneuper@59586
|
98 |
);
|
wneuper@59586
|
99 |
fun get_calcs thy = Data.get thy
|
walther@59853
|
100 |
fun add_calcs calcs = Data.map (union_overwrite Exec_Def.calc_eq calcs)
|
wneuper@59586
|
101 |
|
wneuper@59586
|
102 |
structure Data = Theory_Data (
|
walther@59891
|
103 |
type T = (term * (Spec.spec * (term list -> (term * term list) list))) list;
|
wneuper@59586
|
104 |
val empty = [];
|
wneuper@59586
|
105 |
val extend = I;
|
walther@59893
|
106 |
val merge = merge CAS_Def.cas_eq;
|
wneuper@59586
|
107 |
);
|
wneuper@59586
|
108 |
fun get_cas thy = Data.get thy
|
walther@59893
|
109 |
fun add_cas cas = Data.map (union_overwrite CAS_Def.cas_eq cas)
|
wneuper@59586
|
110 |
|
wneuper@59586
|
111 |
structure Data = Theory_Data (
|
walther@59893
|
112 |
type T = Probl_Def.ptyps;
|
walther@59893
|
113 |
val empty = [Probl_Def.e_Ptyp];
|
wneuper@59586
|
114 |
val extend = I;
|
walther@59890
|
115 |
val merge = Store.merge_ptyps;
|
wneuper@59586
|
116 |
);
|
wneuper@59586
|
117 |
fun get_ptyps thy = Data.get thy;
|
wneuper@59586
|
118 |
fun add_pbts pbts thy = let
|
wneuper@59586
|
119 |
fun add_pbt (pbt as {guh,...}, pblID) =
|
wneuper@59586
|
120 |
(* the pblID has the leaf-element as first; better readability achieved *)
|
walther@59893
|
121 |
(if (!Check_Unique.check_guhs_unique) then Probl_Def.check_pblguh_unique guh (Data.get thy) else ();
|
walther@59890
|
122 |
rev pblID |> Store.insrt pblID pbt);
|
wneuper@59586
|
123 |
in Data.map (fold add_pbt pbts) thy end;
|
wneuper@59586
|
124 |
|
wneuper@59586
|
125 |
structure Data = Theory_Data (
|
walther@59893
|
126 |
type T = Meth_Def.mets;
|
walther@59893
|
127 |
val empty = [Meth_Def.e_Mets];
|
wneuper@59586
|
128 |
val extend = I;
|
walther@59890
|
129 |
val merge = Store.merge_ptyps;
|
wneuper@59586
|
130 |
);
|
wneuper@59586
|
131 |
val get_mets = Data.get;
|
wneuper@59586
|
132 |
fun add_mets mets thy = let
|
wneuper@59586
|
133 |
fun add_met (met as {guh,...}, metID) =
|
walther@59893
|
134 |
(if (!Check_Unique.check_guhs_unique) then Meth_Def.check_metguh_unique guh (Data.get thy) else ();
|
walther@59890
|
135 |
Store.insrt metID met metID);
|
wneuper@59586
|
136 |
in Data.map (fold add_met mets) thy end;
|
wneuper@59586
|
137 |
|
wneuper@59586
|
138 |
structure Data = Theory_Data (
|
walther@59893
|
139 |
type T = (Thy_Html.thydata Store.ptyp) list;
|
wneuper@59586
|
140 |
val empty = [];
|
wneuper@59586
|
141 |
val extend = I;
|
walther@59890
|
142 |
val merge = Store.merge_ptyps; (* relevant for store_thm, store_rls *)
|
wneuper@59586
|
143 |
);
|
wneuper@59586
|
144 |
fun get_thes thy = Data.get thy
|
wneuper@59586
|
145 |
fun add_thes thes thy = let
|
walther@59893
|
146 |
fun add_the (thydata, theID) = Thy_Html.add_thydata ([], theID) thydata
|
wneuper@59586
|
147 |
in Data.map (fold add_the thes) thy end;
|
wneuper@59586
|
148 |
fun insert_fillpats fis thy =
|
wneuper@59586
|
149 |
let
|
wneuper@59586
|
150 |
fun update_elem (theID, fillpats) =
|
wneuper@59586
|
151 |
let
|
walther@59890
|
152 |
val hthm = Store.get_py (Data.get thy) theID theID
|
walther@59893
|
153 |
val hthm' = Thy_Html.update_hthm hthm fillpats
|
wneuper@59586
|
154 |
handle ERROR _ =>
|
wneuper@59586
|
155 |
error ("insert_fillpats: " ^ strs2str theID ^ "must address a theorem")
|
walther@59890
|
156 |
in Store.update_ptyps theID theID hthm' end
|
wneuper@59586
|
157 |
in Data.map (fold update_elem fis) thy end
|
wneuper@59586
|
158 |
|
wneuper@59586
|
159 |
val cur_thy = Synchronized.var "finally_knowledge_complete" @{theory};
|
wneuper@59586
|
160 |
fun set_ref_thy thy = Synchronized.change cur_thy (fn _ => thy); (* never RE-set ! *)
|
wneuper@59586
|
161 |
fun get_ref_thy () = Synchronized.value cur_thy;
|
wneuper@59586
|
162 |
end;
|
wneuper@59586
|
163 |
\<close>
|
wneuper@59586
|
164 |
|
wneuper@59586
|
165 |
section \<open>Re-use existing access functions for knowledge elements\<close>
|
wneuper@59586
|
166 |
text \<open>
|
wneuper@59586
|
167 |
The independence of problems' and methods' structure enforces the accesse
|
wneuper@59592
|
168 |
functions to use "Isac_Knowledge", the final theory which comprises all knowledge defined.
|
wneuper@59586
|
169 |
\<close>
|
wneuper@59586
|
170 |
ML \<open>
|
wneuper@59586
|
171 |
val get_ref_thy = KEStore_Elems.get_ref_thy;
|
wneuper@59586
|
172 |
|
walther@59867
|
173 |
fun assoc_rls (rls' : Rule_Set.id) =
|
walther@59879
|
174 |
case AList.lookup (op =) (KEStore_Elems.get_rlss (ThyC.get_theory "Isac_Knowledge")) rls' of
|
wneuper@59586
|
175 |
SOME (_, rls) => rls
|
walther@59887
|
176 |
| NONE => raise ERROR ("rls \""^ rls' ^ "\" missing in Know_Store.\n" ^
|
wneuper@59586
|
177 |
"TODO exception hierarchy needs to be established.")
|
wneuper@59586
|
178 |
|
walther@59867
|
179 |
fun assoc_rls' thy (rls' : Rule_Set.id) =
|
wneuper@59586
|
180 |
case AList.lookup (op =) (KEStore_Elems.get_rlss thy) rls' of
|
wneuper@59586
|
181 |
SOME (_, rls) => rls
|
walther@59887
|
182 |
| NONE => raise ERROR ("rls \""^ rls' ^ "\" missing in Know_Store.\n" ^
|
wneuper@59586
|
183 |
"TODO exception hierarchy needs to be established.")
|
wneuper@59586
|
184 |
|
wneuper@59586
|
185 |
fun assoc_calc thy calID = let
|
wneuper@59586
|
186 |
fun ass ([], key) =
|
wneuper@59586
|
187 |
error ("assoc_calc: '" ^ key ^ "' not found in theory " ^ (Context.theory_name thy))
|
wneuper@59586
|
188 |
| ass ((calc, (keyi, _)) :: pairs, key) =
|
wneuper@59586
|
189 |
if key = keyi then calc else ass (pairs, key);
|
wneuper@59586
|
190 |
in ass (thy |> KEStore_Elems.get_calcs, calID) end;
|
wneuper@59586
|
191 |
|
wneuper@59586
|
192 |
fun assoc_calc' thy key = let
|
wneuper@59586
|
193 |
fun ass ([], key') =
|
wneuper@59586
|
194 |
error ("assoc_calc': '" ^ key' ^ "' not found in theory " ^ (Context.theory_name thy))
|
wneuper@59586
|
195 |
| ass ((all as (keyi, _)) :: pairs, key') =
|
wneuper@59586
|
196 |
if key' = keyi then all else ass (pairs, key');
|
wneuper@59586
|
197 |
in ass (KEStore_Elems.get_calcs thy, key) end;
|
wneuper@59586
|
198 |
|
wneuper@59586
|
199 |
fun assoc_cas thy key = assoc (KEStore_Elems.get_cas thy, key);
|
wneuper@59586
|
200 |
|
wneuper@59586
|
201 |
fun get_ptyps () = get_ref_thy () |> KEStore_Elems.get_ptyps;
|
wneuper@59586
|
202 |
fun get_mets () = get_ref_thy () |> KEStore_Elems.get_mets;
|
wneuper@59586
|
203 |
fun get_thes () = get_ref_thy () |> KEStore_Elems.get_thes;
|
wneuper@59586
|
204 |
\<close>
|
wneuper@59586
|
205 |
setup \<open>KEStore_Elems.add_rlss
|
walther@59852
|
206 |
[("empty", (Context.theory_name @{theory}, Rule_Set.empty)),
|
walther@59850
|
207 |
("e_rrls", (Context.theory_name @{theory}, Rule_Set.e_rrls))]\<close>
|
wneuper@59586
|
208 |
|
wneuper@59586
|
209 |
section \<open>determine sequence of main parts in thehier\<close>
|
wneuper@59586
|
210 |
setup \<open>
|
wneuper@59586
|
211 |
KEStore_Elems.add_thes
|
walther@59893
|
212 |
[(Thy_Html.Html {guh = Thy_Html.part2guh ["IsacKnowledge"], html = "",
|
wneuper@59586
|
213 |
mathauthors = ["Isac team"], coursedesign = []}, ["IsacKnowledge"]),
|
walther@59893
|
214 |
(Thy_Html.Html {guh = Thy_Html.part2guh ["Isabelle"], html = "",
|
wneuper@59586
|
215 |
mathauthors = ["Isabelle team, TU Munich"], coursedesign = []}, ["Isabelle"]),
|
walther@59893
|
216 |
(Thy_Html.Html {guh = Thy_Html.part2guh ["IsacScripts"], html = "",
|
wneuper@59586
|
217 |
mathauthors = ["Isac team"], coursedesign = []}, ["IsacScripts"])]
|
wneuper@59586
|
218 |
\<close>
|
wneuper@59586
|
219 |
|
wneuper@59586
|
220 |
section \<open>Functions for checking KEStore_Elems\<close>
|
wneuper@59586
|
221 |
ML \<open>
|
walther@59851
|
222 |
fun short_string_of_rls Rule_Set.Empty = "Erls"
|
walther@59851
|
223 |
| short_string_of_rls (Rule_Def.Repeat {calc, rules, ...}) =
|
wneuper@59586
|
224 |
"Rls {#calc = " ^ string_of_int (length calc) ^
|
wneuper@59586
|
225 |
", #rules = " ^ string_of_int (length rules) ^ ", ..."
|
walther@59878
|
226 |
| short_string_of_rls (Rule_Set.Sequence {calc, rules, ...}) =
|
wneuper@59586
|
227 |
"Seq {#calc = " ^ string_of_int (length calc) ^
|
wneuper@59586
|
228 |
", #rules = " ^ string_of_int (length rules) ^ ", ..."
|
walther@59850
|
229 |
| short_string_of_rls (Rule_Set.Rrls _) = "Rrls {...}";
|
wneuper@59586
|
230 |
fun check_kestore_rls (rls', (thyID, rls)) =
|
wneuper@59586
|
231 |
"(" ^ rls' ^ ", (" ^ thyID ^ ", " ^ short_string_of_rls rls ^ "))";
|
wneuper@59586
|
232 |
|
walther@59852
|
233 |
fun check_kestore_calc ((id, (c, _)) : Rule_Def.calc) = "(" ^ id ^ ", (" ^ c ^ ", fn))";
|
wneuper@59586
|
234 |
|
walther@59846
|
235 |
(* we avoid term_to_string''' defined later *)
|
walther@59893
|
236 |
fun check_kestore_cas ((t, (s, _)) : CAS_Def.cas_elem) =
|
walther@59846
|
237 |
"(" ^ (Print_Mode.setmp [] (Syntax.string_of_term (Config.put show_markup false
|
walther@59891
|
238 |
(Proof_Context.init_global @{theory})))) t ^ ", " ^ Spec.spec2str s ^ ")";
|
wneuper@59586
|
239 |
|
wneuper@59586
|
240 |
fun count_kestore_ptyps [] = 0
|
walther@59890
|
241 |
| count_kestore_ptyps ((Store.Ptyp (_, _, ps)) :: ps') =
|
wneuper@59586
|
242 |
1 + count_kestore_ptyps ps + count_kestore_ptyps ps';
|
walther@59890
|
243 |
fun check_kestore_ptyp' strfun (Store.Ptyp (key, pbts, pts)) = "Ptyp (" ^ (quote key) ^ ", " ^
|
walther@59888
|
244 |
(strfun pbts) ^ ", " ^ (map (check_kestore_ptyp' strfun) pts |> list2str) ^ ")" |> linefeed;
|
walther@59893
|
245 |
val check_kestore_ptyp = check_kestore_ptyp' Probl_Def.pbts2str;
|
walther@59890
|
246 |
fun ptyp_ord ((Store.Ptyp (s1, _, _)), (Store.Ptyp (s2, _, _))) = string_ord (s1, s2);
|
walther@59893
|
247 |
fun pbt_ord ({guh = guh'1, ...} : Probl_Def.pbt, {guh = guh'2, ...} : Probl_Def.pbt) = string_ord (guh'1, guh'2);
|
wneuper@59586
|
248 |
fun sort_kestore_ptyp' _ [] = []
|
walther@59890
|
249 |
| sort_kestore_ptyp' ordfun ((Store.Ptyp (key, pbts, ps)) :: ps') =
|
walther@59890
|
250 |
((Store.Ptyp (key, sort ordfun pbts, sort_kestore_ptyp' ordfun ps |> sort ptyp_ord))
|
wneuper@59586
|
251 |
:: sort_kestore_ptyp' ordfun ps');
|
wneuper@59586
|
252 |
val sort_kestore_ptyp = sort_kestore_ptyp' pbt_ord;
|
wneuper@59586
|
253 |
|
walther@59893
|
254 |
fun metguh2str ({guh,...} : Meth_Def.met) = guh : string;
|
walther@59893
|
255 |
fun check_kestore_met (mp: Meth_Def.met Store.ptyp) =
|
wneuper@59586
|
256 |
check_kestore_ptyp' (fn xs => map metguh2str xs |> strs2str) mp;
|
walther@59893
|
257 |
fun met_ord ({guh = guh'1, ...} : Meth_Def.met, {guh = guh'2, ...} : Meth_Def.met) = string_ord (guh'1, guh'2);
|
wneuper@59586
|
258 |
val sort_kestore_met = sort_kestore_ptyp' met_ord;
|
wneuper@59586
|
259 |
|
walther@59893
|
260 |
fun check_kestore_thes thes = ((map writeln) o (map (check_kestore_ptyp' Thy_Html.thes2str))) thes
|
wneuper@59586
|
261 |
fun write_thes thydata_list =
|
wneuper@59586
|
262 |
thydata_list
|
walther@59893
|
263 |
|> map (fn (id, the) => (Thy_Html.theID2str id, Thy_Html.the2str the))
|
wneuper@59586
|
264 |
|> map pair2str
|
wneuper@59586
|
265 |
|> map writeln
|
wneuper@59586
|
266 |
\<close>
|
wneuper@59586
|
267 |
ML \<open>
|
wneuper@59586
|
268 |
\<close> ML \<open>
|
wneuper@59586
|
269 |
\<close> ML \<open>
|
wneuper@59586
|
270 |
\<close>
|
wneuper@59586
|
271 |
end
|