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