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