walther@59882
|
1 |
(* Title: BaseDefinitions/celem-8.sml
|
walther@59882
|
2 |
Author: Walther Neuper
|
walther@59882
|
3 |
(c) due to copyright terms
|
walther@59882
|
4 |
|
walther@59919
|
5 |
Here is a minimum of code required for Know_Store.thy.
|
walther@59919
|
6 |
For main code see structure Thy_Write and structure Thy_Present.
|
walther@59919
|
7 |
|
walther@59919
|
8 |
The latter is legacy for HTML representation of theory data in Isac's Java front end.
|
walther@59893
|
9 |
*)
|
walther@59917
|
10 |
signature THEORY_DATA_STORE_WRITE =
|
walther@59882
|
11 |
sig
|
walther@59884
|
12 |
type authors
|
walther@59884
|
13 |
datatype thydata
|
walther@59904
|
14 |
= Hcal of {calc: Rule_Def.calc, coursedesign: authors, guh: Check_Unique.id, mathauthors: authors}
|
walther@59907
|
15 |
| Hord of {coursedesign: authors, guh: Check_Unique.id, mathauthors: authors, ord: Rule_Def.rew_ord_}
|
walther@59904
|
16 |
| Hrls of {coursedesign: authors, guh: Check_Unique.id, mathauthors: authors, thy_rls: ThyC.id * Rule_Set.T}
|
walther@59909
|
17 |
| Hthm of {coursedesign: authors, fillpats: Error_Pattern_Def.fill_in list, guh: Check_Unique.id, mathauthors: authors, thm: thm}
|
walther@59904
|
18 |
| Html of {coursedesign: authors, guh: Check_Unique.id, html: string, mathauthors: authors}
|
walther@59884
|
19 |
type theID
|
walther@59888
|
20 |
val theID2str: string list -> string
|
walther@59884
|
21 |
val the2str: thydata -> string
|
walther@59884
|
22 |
val thes2str: thydata list -> string
|
walther@59884
|
23 |
val theID2thyID: theID -> ThyC.id
|
walther@59888
|
24 |
|
walther@59904
|
25 |
val part2guh: theID -> Check_Unique.id
|
walther@59904
|
26 |
val thy2guh: theID -> Check_Unique.id
|
walther@59904
|
27 |
val thypart2guh: theID -> Check_Unique.id
|
walther@59904
|
28 |
val thm2guh: string * ThyC.id -> ThmC_Def.id -> Check_Unique.id
|
walther@59904
|
29 |
val rls2guh: string * ThyC.id -> Rule_Set.id -> Check_Unique.id
|
walther@59904
|
30 |
val cal2guh: string * ThyC.id -> string -> Check_Unique.id
|
walther@59904
|
31 |
val ord2guh: string * ThyC.id -> string -> Check_Unique.id
|
walther@59904
|
32 |
val theID2guh: theID -> Check_Unique.id
|
walther@59888
|
33 |
|
walther@59897
|
34 |
val add_thydata: string list * string list -> thydata -> thydata Store.T -> thydata Store.T
|
walther@59909
|
35 |
val update_hthm: thydata -> Error_Pattern_Def.fill_in list -> thydata
|
walther@59882
|
36 |
(* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
|
walther@59882
|
37 |
(*NONE*)
|
walther@59886
|
38 |
(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
|
walther@59882
|
39 |
(*NONE*)
|
walther@59886
|
40 |
( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
|
walther@59882
|
41 |
end
|
walther@59882
|
42 |
|
walther@59882
|
43 |
(**)
|
walther@59917
|
44 |
structure Thy_Write(**): THEORY_DATA_STORE_WRITE(**) =
|
walther@59882
|
45 |
struct
|
walther@59882
|
46 |
(**)
|
walther@59882
|
47 |
|
walther@59884
|
48 |
(*the key into the hierarchy ob theory elements*)
|
walther@59884
|
49 |
type theID = string list;
|
walther@59884
|
50 |
val theID2str = strs2str; (*theID eg. is ["IsacKnowledge", "Test", "Rulesets", "ac_plus_times"]*)
|
walther@59884
|
51 |
fun theID2thyID theID =
|
walther@59884
|
52 |
if length theID >= 3 then (last_elem o (drop_last_n 2)) theID
|
walther@59962
|
53 |
else raise ERROR ("theID2thyID called with " ^ theID2str theID);
|
walther@59884
|
54 |
type authors = string list;
|
walther@59884
|
55 |
(* datatype for collecting thydata for hierarchy *)
|
walther@59884
|
56 |
(*WN060720 more consistent naming would be 'type thyelem' or 'thelem'*)
|
walther@59884
|
57 |
datatype thydata =
|
walther@59904
|
58 |
Html of {guh: Check_Unique.id, coursedesign: authors, mathauthors: authors, html: string}
|
walther@59909
|
59 |
| Hthm of {guh: Check_Unique.id, coursedesign: authors, mathauthors: authors, fillpats: Error_Pattern_Def.fill_in list,
|
walther@59884
|
60 |
thm: thm} (* here no sym_thm, thus no thmID required *)
|
walther@59904
|
61 |
| Hrls of {guh: Check_Unique.id, coursedesign: authors, mathauthors: authors, thy_rls: (ThyC.id * Rule_Set.T)}
|
walther@59904
|
62 |
| Hcal of {guh: Check_Unique.id, coursedesign: authors, mathauthors: authors, calc: Rule_Def.calc}
|
walther@59904
|
63 |
| Hord of {guh: Check_Unique.id, coursedesign: authors, mathauthors: authors,
|
walther@59910
|
64 |
ord: (subst -> (term * term) -> bool)};
|
walther@59884
|
65 |
fun the2str (Html {guh, ...}) = guh
|
walther@59884
|
66 |
| the2str (Hthm {guh, ...}) = guh
|
walther@59884
|
67 |
| the2str (Hrls {guh, ...}) = guh
|
walther@59884
|
68 |
| the2str (Hcal {guh, ...}) = guh
|
walther@59884
|
69 |
| the2str (Hord {guh, ...}) = guh
|
walther@59884
|
70 |
fun thes2str thes = map the2str thes |> list2str;
|
walther@59884
|
71 |
|
walther@59884
|
72 |
(* notes on thehier concerning sym_thmID theorems (created in derivations, reverse rewriting)
|
walther@59884
|
73 |
(a): thehier does not contain sym_thmID theorems
|
walther@59884
|
74 |
(b): lookup for sym_thmID directly from Isabelle using sym_thm
|
walther@59884
|
75 |
(within math-engine NO lookup in thehier -- within java in *.xml only!)
|
walther@59884
|
76 |
TODO (c): export from thehier to xml
|
walther@59884
|
77 |
TODO (c1) creates one entry for "thmID" (and NONE for "sym_thmID") in the hierarchy
|
walther@59884
|
78 |
TODO (c2) creates 2 files "thy_*-thm-thmID.xml" and "thy_*-thm-sym_thmID.xml"
|
walther@59884
|
79 |
TODO (d): 1 entry in the MiniBrowser's hierarchy (generated from xml)
|
walther@59884
|
80 |
stands for both, "thmID" and "sym_thmID"
|
walther@59884
|
81 |
TODO (d1) lookup from calctxt
|
walther@59884
|
82 |
TODO (d1) lookup from from rule set in MiniBrowser *)
|
walther@59897
|
83 |
type thehier = (thydata Store.node) list;
|
walther@59887
|
84 |
(* required to determine sequence of main nodes of thehier in Know_Store.thy *)
|
walther@59884
|
85 |
fun part2guh [str] = (case str of
|
walther@59904
|
86 |
"Isabelle" => "thy_isab_" ^ str ^ "-part" : Check_Unique.id
|
walther@59884
|
87 |
| "IsacScripts" => "thy_scri_" ^ str ^ "-part"
|
walther@59884
|
88 |
| "IsacKnowledge" => "thy_isac_" ^ str ^ "-part"
|
walther@59884
|
89 |
| str => raise ERROR ("thy2guh: called with \""^ str ^"\""))
|
walther@59884
|
90 |
| part2guh theID = raise ERROR ("part2guh called with theID = \"" ^ theID2str theID ^ "'");
|
walther@59884
|
91 |
|
walther@59884
|
92 |
fun thy2guh [part, thyID] = (case part of
|
walther@59884
|
93 |
"Isabelle" => "thy_isab_" ^ thyID
|
walther@59884
|
94 |
| "IsacScripts" => "thy_scri_" ^ thyID
|
walther@59884
|
95 |
| "IsacKnowledge" => "thy_isac_" ^ thyID
|
walther@59884
|
96 |
| str => raise ERROR ("thy2guh: called with \"" ^ str ^ "\""))
|
walther@59884
|
97 |
| thy2guh theID = raise ERROR ("thy2guh called with \"" ^ strs2str' theID ^ "\"");
|
walther@59884
|
98 |
|
walther@59884
|
99 |
fun thypart2guh ([part, thyID, thypart] : theID) = (case part of
|
walther@59904
|
100 |
"Isabelle" => "thy_isab_" ^ thyID ^ "-" ^ thypart : Check_Unique.id
|
walther@59884
|
101 |
| "IsacScripts" => "thy_scri_" ^ thyID ^ "-" ^ thypart
|
walther@59884
|
102 |
| "IsacKnowledge" => "thy_isac_" ^ thyID ^ "-" ^ thypart
|
walther@59884
|
103 |
| str => raise ERROR ("thypart2guh: called with '" ^ str ^ "'"))
|
walther@59884
|
104 |
| thypart2guh strs = raise ERROR ("thypart2guh called with \"" ^ strs2str' strs ^ "\"");
|
walther@59884
|
105 |
|
walther@59884
|
106 |
|
walther@59884
|
107 |
(* convert the data got via contextToThy to a globally unique handle.
|
walther@59884
|
108 |
there is another way to get the guh: get out of the 'theID' in the hierarchy *)
|
walther@59884
|
109 |
fun thm2guh (isa, thyID) thmID = case isa of
|
walther@59904
|
110 |
"Isabelle" => "thy_isab_" ^ thyID ^ "-thm-" ^ strip_thy thmID : Check_Unique.id
|
walther@59884
|
111 |
| "IsacKnowledge" => "thy_isac_" ^ thyID ^ "-thm-" ^ strip_thy thmID
|
walther@59884
|
112 |
| "IsacScripts" => "thy_scri_" ^ thyID ^ "-thm-" ^ strip_thy thmID
|
walther@59884
|
113 |
| _ => raise ERROR
|
walther@59884
|
114 |
("thm2guh called with (isa, thyID) = (" ^ isa ^ ", " ^ thyID ^ ") for thm = \"" ^ thmID ^ "\"");
|
walther@59884
|
115 |
|
walther@59884
|
116 |
fun rls2guh (isa, thyID) rls' = case isa of
|
walther@59904
|
117 |
"Isabelle" => "thy_isab_" ^ thyID ^ "-rls-" ^ rls' : Check_Unique.id
|
walther@59884
|
118 |
| "IsacKnowledge" => "thy_isac_" ^ thyID ^ "-rls-" ^ rls'
|
walther@59884
|
119 |
| "IsacScripts" => "thy_scri_" ^ thyID ^ "-rls-" ^ rls'
|
walther@59884
|
120 |
| _ => raise ERROR
|
walther@59884
|
121 |
("rls2guh called with (isa, thyID) = (" ^ isa ^ ", " ^ thyID ^ ") for rls = \"" ^ rls' ^ "\"");
|
walther@59884
|
122 |
|
walther@59884
|
123 |
fun cal2guh (isa, thyID) calID = case isa of
|
walther@59904
|
124 |
"Isabelle" => "thy_isab_" ^ thyID ^ "-cal-" ^ calID : Check_Unique.id
|
walther@59884
|
125 |
| "IsacKnowledge" => "thy_isac_" ^ thyID ^ "-cal-" ^ calID
|
walther@59884
|
126 |
| "IsacScripts" => "thy_scri_" ^ thyID ^ "-cal-" ^ calID
|
walther@59884
|
127 |
| _ => raise ERROR
|
walther@59884
|
128 |
("cal2guh called with (isa, thyID) = (" ^ isa ^ ", " ^ thyID ^ ") for cal = \"" ^ calID ^ "\"");
|
walther@59884
|
129 |
|
walther@59884
|
130 |
fun ord2guh (isa, thyID) rew_ord' = case isa of
|
walther@59904
|
131 |
"Isabelle" => "thy_isab_" ^ thyID ^ "-ord-" ^ rew_ord' : Check_Unique.id
|
walther@59884
|
132 |
| "IsacKnowledge" => "thy_isac_" ^ thyID ^ "-ord-" ^ rew_ord'
|
walther@59884
|
133 |
| "IsacScripts" => "thy_scri_" ^ thyID ^ "-ord-" ^ rew_ord'
|
walther@59884
|
134 |
| _ => raise ERROR
|
walther@59884
|
135 |
("ord2guh called with (isa, thyID) = (" ^ isa ^ ", " ^ thyID ^ ") for ord = \"" ^ rew_ord' ^ "\"");
|
walther@59884
|
136 |
|
walther@59884
|
137 |
(* TODO
|
walther@59884
|
138 |
fun theID2guh theID = case length theID of
|
walther@59962
|
139 |
0 => raise ERROR ("theID2guh: called with theID = " ^ strs2str' theID)
|
walther@59884
|
140 |
| 1 => part2guh theID
|
walther@59884
|
141 |
| 2 => thy2guh theID
|
walther@59884
|
142 |
| 3 => thypart2guh theID
|
walther@59884
|
143 |
| 4 =>
|
walther@59884
|
144 |
let val [isa, thyID, typ, elemID] = theID
|
walther@59884
|
145 |
in case typ of
|
walther@59884
|
146 |
"Theorems" => thm2guh (isa, thyID) elemID
|
walther@59884
|
147 |
| "Rulesets" => rls2guh (isa, thyID) elemID
|
walther@59884
|
148 |
| "Calculations" => cal2guh (isa, thyID) elemID
|
walther@59884
|
149 |
| "Orders" => ord2guh (isa, thyID) elemID
|
walther@59884
|
150 |
| "Theorems" => thy2guh [isa, thyID]
|
walther@59884
|
151 |
| str => raise ERROR ("theID2guh: called with theID = " ^ strs2str' theID)
|
walther@59884
|
152 |
end
|
walther@59884
|
153 |
| n => raise ERROR ("theID2guh called with theID = " ^ strs2str' theID);
|
walther@59884
|
154 |
*)
|
walther@59884
|
155 |
(* not only for thydata, but also for thy's etc *)
|
walther@59884
|
156 |
fun theID2guh [] = raise ERROR ("theID2guh: called with []")
|
walther@59884
|
157 |
| theID2guh [str] = part2guh [str]
|
walther@59884
|
158 |
| theID2guh [s1, s2] = thy2guh [s1, s2]
|
walther@59884
|
159 |
| theID2guh [s1, s2, s3] = thypart2guh [s1, s2, s3]
|
walther@59884
|
160 |
| theID2guh (strs as [isa, thyID, typ, elemID]) = (case typ of
|
walther@59884
|
161 |
"Theorems" => thm2guh (isa, thyID) elemID
|
walther@59884
|
162 |
| "Rulesets" => rls2guh (isa, thyID) elemID
|
walther@59884
|
163 |
| "Calculations" => cal2guh (isa, thyID) elemID
|
walther@59884
|
164 |
| "Orders" => ord2guh (isa, thyID) elemID
|
walther@59884
|
165 |
| _ => raise ERROR ("theID2guh: called with theID = " ^ strs2str' strs))
|
walther@59884
|
166 |
| theID2guh strs = raise ERROR ("theID2guh called with theID = " ^ strs2str' strs);
|
walther@59884
|
167 |
|
walther@59884
|
168 |
(* not only for thydata, but also for thy's etc *)
|
walther@59884
|
169 |
fun theID2guh [] = raise ERROR ("theID2guh: called with []")
|
walther@59884
|
170 |
| theID2guh [str] = part2guh [str]
|
walther@59884
|
171 |
| theID2guh [s1, s2] = thy2guh [s1, s2]
|
walther@59884
|
172 |
| theID2guh [s1, s2, s3] = thypart2guh [s1, s2, s3]
|
walther@59884
|
173 |
| theID2guh (strs as [isa, thyID, typ, elemID]) = (case typ of
|
walther@59884
|
174 |
"Theorems" => thm2guh (isa, thyID) elemID
|
walther@59884
|
175 |
| "Rulesets" => rls2guh (isa, thyID) elemID
|
walther@59884
|
176 |
| "Calculations" => cal2guh (isa, thyID) elemID
|
walther@59884
|
177 |
| "Orders" => ord2guh (isa, thyID) elemID
|
walther@59884
|
178 |
| _ => raise ERROR ("theID2guh: called with theID = " ^ strs2str' strs))
|
walther@59884
|
179 |
| theID2guh strs = raise ERROR ("theID2guh called with theID = " ^ strs2str' strs);
|
walther@59914
|
180 |
|
walther@59884
|
181 |
fun Html_default exist = (Html {guh = theID2guh exist,
|
walther@59884
|
182 |
coursedesign = ["isac team 2006"], mathauthors = [], html = ""})
|
walther@59884
|
183 |
|
walther@59897
|
184 |
fun fill_parents (_, [i]) thydata = Store.Node (i, [thydata], [])
|
walther@59884
|
185 |
| fill_parents (exist, i :: is) thydata =
|
walther@59897
|
186 |
Store.Node (i, [Html_default (exist @ [i])], [fill_parents (exist @ [i], is) thydata])
|
walther@59884
|
187 |
| fill_parents _ _ = raise ERROR "Html_default: avoid ML warning: Matches are not exhaustive"
|
walther@59884
|
188 |
|
walther@59884
|
189 |
fun add_thydata (exist, is) thydata [] = [fill_parents (exist, is) thydata]
|
walther@59897
|
190 |
| add_thydata (exist, [i]) data (pys as (py as Store.Node (key, _, _)) :: pyss) =
|
walther@59884
|
191 |
if i = key
|
walther@59884
|
192 |
then pys (* preserve existing thydata *)
|
walther@59884
|
193 |
else py :: add_thydata (exist, [i]) data pyss
|
walther@59897
|
194 |
| add_thydata (exist, iss as (i :: is)) data ((py as Store.Node (key, d, pys)) :: pyss) =
|
walther@59884
|
195 |
if i = key
|
walther@59884
|
196 |
then
|
walther@59884
|
197 |
if length pys = 0
|
walther@59897
|
198 |
then Store.Node (key, d, [fill_parents (exist @ [i], is) data]) :: pyss
|
walther@59897
|
199 |
else Store.Node (key, d, add_thydata (exist @ [i], is) data pys) :: pyss
|
walther@59884
|
200 |
else py :: add_thydata (exist, iss) data pyss
|
walther@59884
|
201 |
| add_thydata _ _ _ = raise ERROR "add_thydata: avoid ML warning: Matches are not exhaustive"
|
walther@59884
|
202 |
|
walther@59884
|
203 |
fun update_hthm (Hthm {guh, coursedesign, mathauthors, thm, ...}) fillpats' =
|
walther@59884
|
204 |
Hthm {guh = guh, coursedesign = coursedesign, mathauthors = mathauthors,
|
walther@59884
|
205 |
fillpats = fillpats', thm = thm}
|
walther@59884
|
206 |
| update_hthm _ _ = raise ERROR "update_hthm: wrong arguments";
|
walther@59882
|
207 |
|
walther@59882
|
208 |
(**)end(**)
|