walther@59974
|
1 |
(* Title: "BridgeLibisabelle/thy-hierarchy.sml"
|
walther@59974
|
2 |
Author: Walther Neuper 0601
|
walther@59974
|
3 |
(c) due to copyright terms
|
walther@59974
|
4 |
|
walther@59974
|
5 |
Export theory-data "thehier" to xml.
|
neuper@55490
|
6 |
*)
|
neuper@37906
|
7 |
|
walther@59874
|
8 |
signature THEORY_HIERARCHY =
|
walther@59874
|
9 |
sig
|
walther@59917
|
10 |
val collect_cals: string * ThyC.id -> (Thy_Write.theID * Thy_Write.thydata) list
|
walther@59917
|
11 |
val collect_isab: string -> string * thm -> Thy_Write.theID * Thy_Write.thydata
|
walther@59917
|
12 |
val collect_ords: 'a * ThyC.id -> (Thy_Write.theID * Thy_Write.thydata) list
|
walther@59917
|
13 |
val collect_part: string -> theory -> theory list -> (Thy_Write.theID * Thy_Write.thydata) list
|
walther@59879
|
14 |
val collect_rlss: string -> (Rule_Set.id * (ThyC.id * Rule_Set.T)) list -> theory list ->
|
walther@59917
|
15 |
(Thy_Write.theID * Thy_Write.thydata) list
|
walther@59917
|
16 |
val collect_thms: string -> theory -> (Thy_Write.theID * Thy_Write.thydata) list
|
walther@59874
|
17 |
|
walther@59897
|
18 |
val hierarchy_guh: 'a Store.T -> string
|
walther@59917
|
19 |
val insert_errpatIDs: 'a -> Thy_Write.theID -> Error_Pattern_Def.id list ->
|
walther@59917
|
20 |
Thy_Write.thydata * Thy_Write.theID
|
walther@59918
|
21 |
val update_hrls: Thy_Write.thydata -> Error_Pattern_Def.id list -> Thy_Write.thydata
|
walther@59874
|
22 |
|
walther@59917
|
23 |
val makeHcal: string * ThyC.id -> string * Rule_Def.calc -> Thy_Write.theID * Thy_Write.thydata
|
walther@59907
|
24 |
val makeHord: string * ThyC.id -> string * Rule_Def.rew_ord_ ->
|
walther@59917
|
25 |
Thy_Write.theID * Thy_Write.thydata
|
walther@59879
|
26 |
val makeHrls: string -> Rule_Set.id * (ThyC.id * Rule_Def.rule_set) ->
|
walther@59917
|
27 |
Thy_Write.theID * Thy_Write.thydata
|
walther@59917
|
28 |
val makeHthm: string * ThyC.id -> thm -> Thy_Write.theID * Thy_Write.thydata
|
walther@59917
|
29 |
val make_cal: theory -> Rule_Def.calc -> Thy_Write.authors -> Thy_Write.thydata * Thy_Write.theID
|
walther@59917
|
30 |
val make_isa: theory -> ThyC.id * ThyC.id -> Thy_Write.authors ->
|
walther@59917
|
31 |
Thy_Write.thydata * Thy_Write.theID
|
walther@59917
|
32 |
val make_ord: theory -> Rule_Def.rew_ord_ -> Thy_Write.authors ->
|
walther@59917
|
33 |
Thy_Write.thydata * Thy_Write.theID
|
walther@59917
|
34 |
val make_rls: theory -> Rule_Def.rule_set -> Thy_Write.authors -> Thy_Write.thydata * Thy_Write.theID
|
walther@59917
|
35 |
val make_thm: theory -> string -> string * thm -> Thy_Write.authors -> Thy_Write.thydata * Thy_Write.theID
|
walther@59917
|
36 |
val make_thy: theory -> Thy_Write.authors -> Thy_Write.thydata * Thy_Write.theID
|
walther@59874
|
37 |
|
walther@59874
|
38 |
val show_thes: unit -> unit
|
walther@59874
|
39 |
|
walther@59918
|
40 |
val thes2file: Pbl_Met_Hierarchy.filepath -> unit
|
walther@59874
|
41 |
val thms_of: theory -> thm list
|
walther@59879
|
42 |
val thms_of_rlss: theory -> (Rule_Set.id * (ThyC.id * Rule_Def.rule_set)) list ->
|
walther@59874
|
43 |
(string * thm) list
|
walther@59918
|
44 |
val thy_hierarchy2file: Pbl_Met_Hierarchy.filepath -> unit
|
walther@59918
|
45 |
val thydata2file: Pbl_Met_Hierarchy.filepath -> Pos.pos -> Thy_Write.theID -> Thy_Write.thydata -> unit
|
walther@59917
|
46 |
val thydata2xml: Thy_Write.theID * Thy_Write.thydata -> xml
|
walther@59874
|
47 |
(* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
|
walther@59874
|
48 |
(*NONE*)
|
walther@59886
|
49 |
(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
|
walther@59971
|
50 |
val get_fun_ids: theory -> (string * typ) list
|
walther@59918
|
51 |
val thenode: Pbl_Met_Hierarchy.filepath -> string list -> Pos.pos -> (Pbl_Met_Hierarchy.filepath -> Pos.pos ->
|
walther@59897
|
52 |
string list -> 'a -> 'b) -> 'a Store.node -> unit
|
walther@59918
|
53 |
val thenodes: Pbl_Met_Hierarchy.filepath -> string list -> Pos.pos -> (Pbl_Met_Hierarchy.filepath -> Pos.pos ->
|
walther@59897
|
54 |
string list -> 'a -> 'b) -> 'a Store.T -> unit
|
walther@59886
|
55 |
( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
|
walther@59874
|
56 |
end
|
walther@59874
|
57 |
|
walther@59874
|
58 |
(**)
|
walther@59874
|
59 |
structure Thy_Hierarchy(**): THEORY_HIERARCHY(**) =
|
walther@59874
|
60 |
struct
|
walther@59874
|
61 |
(**)
|
wneuper@59507
|
62 |
open TermC (* allows contains_one_of to be infix *)
|
wneuper@59507
|
63 |
|
walther@60154
|
64 |
fun fun_id_of ({scr = prog, ...} : MethodC.T) =
|
walther@59971
|
65 |
case prog of
|
walther@59971
|
66 |
Rule.Empty_Prog => NONE
|
walther@59971
|
67 |
| Rule.Prog t =>
|
walther@59971
|
68 |
(case t of
|
walther@59971
|
69 |
Const ("HOL.eq", _) $ Free ("t", _) $ Free ("t", _) (*=@{thm refl}*) => NONE
|
walther@59971
|
70 |
| _ => SOME (Program.get_fun_id t))
|
walther@59971
|
71 |
| Rule.Rfuns _ => NONE
|
walther@59971
|
72 |
fun get_fun_ids thy =
|
walther@59971
|
73 |
let
|
walther@59971
|
74 |
val mets = Store.get_all (KEStore_Elems.get_mets thy)
|
walther@59971
|
75 |
(* all mets of the respective theory PLUS of all ancestor theories*)
|
walther@59971
|
76 |
val fun_ids = mets |> map fun_id_of |> filter is_some |> map the
|
walther@59971
|
77 |
in
|
walther@59971
|
78 |
filter (fn (str, _) => ThyC.cut_id str = Context.theory_name thy) fun_ids
|
walther@59971
|
79 |
end
|
walther@59971
|
80 |
|
wneuper@59203
|
81 |
(* copy from mutabelle_extra.ML, fun thms_of *)
|
wneuper@59507
|
82 |
fun thms_of thy = (* das ist zu verbessern *)
|
wneuper@59507
|
83 |
let
|
walther@59971
|
84 |
val fun_ids = get_fun_ids thy
|
wneuper@59507
|
85 |
in
|
wneuper@59507
|
86 |
filter (fn thm => Context.theory_name (Thm.theory_of_thm thm) = Context.theory_name thy
|
wneuper@59549
|
87 |
andalso not (thm contains_one_of fun_ids)
|
walther@59876
|
88 |
andalso not (ThmC.id_of_thm thm = "mono"))
|
wneuper@59549
|
89 |
(* created in Biegelinie by partial_function ^^^^^^*)
|
wneuper@59507
|
90 |
(map snd (Global_Theory.all_thms_of thy false))
|
wneuper@59507
|
91 |
end
|
wneuper@59203
|
92 |
|
neuper@55490
|
93 |
(* wrap theory-data into the uniform type thydata *)
|
neuper@37906
|
94 |
|
walther@59879
|
95 |
fun makeHthm (part : string, thyID : ThyC.id) (thm : thm) =
|
walther@59917
|
96 |
let val theID = [part, thyID, "Theorems"] @ [ThmC.id_of_thm thm] : Thy_Write.theID
|
walther@59917
|
97 |
in (theID, Thy_Write.Hthm {guh = Thy_Write.theID2guh theID, coursedesign = [],
|
neuper@42429
|
98 |
mathauthors = ["isac-team"], fillpats = [], thm = thm})
|
neuper@37906
|
99 |
end;
|
walther@59879
|
100 |
fun makeHrls (part : string) (rls' : Rule_Set.id, thy_rls as (thyID, rls): ThyC.id * Rule_Set.T) =
|
walther@59917
|
101 |
let val theID = [part, thyID,"Rulesets"] @ [rls'] : Thy_Write.theID
|
walther@59917
|
102 |
in (theID, Thy_Write.Hrls {guh = Thy_Write.theID2guh theID, coursedesign = [],
|
neuper@55490
|
103 |
mathauthors = ["isac-team"], thy_rls = thy_rls})
|
neuper@37906
|
104 |
end;
|
walther@59879
|
105 |
fun makeHcal (part : string, thyID : ThyC.id) (calID, cal) =
|
walther@59917
|
106 |
let val theID = [part, thyID,"Operations"] @ [calID] : Thy_Write.theID
|
walther@59917
|
107 |
in (theID, Thy_Write.Hcal {guh = Thy_Write.theID2guh theID, coursedesign=[],
|
neuper@55490
|
108 |
mathauthors = ["isac-team"], calc = cal})
|
neuper@37906
|
109 |
end;
|
walther@59879
|
110 |
fun makeHord (part : string, thyID : ThyC.id) (ordID, ord) =
|
walther@59917
|
111 |
let val theID = [part, thyID,"TODO-Orders"] @ [ordID] : Thy_Write.theID
|
walther@59917
|
112 |
in (theID, Thy_Write.Hord {guh = Thy_Write.theID2guh theID, coursedesign=[],
|
neuper@55490
|
113 |
mathauthors = ["isac-team"], ord = ord})
|
neuper@37906
|
114 |
end;
|
neuper@37906
|
115 |
|
neuper@55490
|
116 |
(* get all theorems from the list of rule-sets (defined in Knowledge) *)
|
walther@59879
|
117 |
fun thms_of_rlss thy rlss = (rlss : (Rule_Set.id * (ThyC.id * Rule_Set.T)) list)
|
walther@59917
|
118 |
|> map (Thy_Present.thms_of_rls o #2 o #2)
|
neuper@55405
|
119 |
|> flat
|
walther@59876
|
120 |
|> map (ThmC.revert_sym_rule thy)
|
wneuper@59416
|
121 |
|> map (fn Rule.Thm (thmID, thm) => (thmID, thm))
|
walther@60017
|
122 |
|> distinct (fn ((thmID1, _), (thmID2, _)) => thmID1 = thmID2)
|
walther@59874
|
123 |
: ThmC.T list
|
neuper@55490
|
124 |
|
neuper@55490
|
125 |
(* collect all thydata defined in in a theory *)
|
neuper@55405
|
126 |
|
neuper@55448
|
127 |
fun collect_thms part thy =
|
wneuper@59203
|
128 |
map (makeHthm (part, Context.theory_name thy)) (rev (thms_of thy))
|
walther@59879
|
129 |
fun collect_rlss part rlss thys = (rlss : (Rule_Set.id * (ThyC.id * Rule_Set.T)) list)
|
neuper@55405
|
130 |
|> filter (fn (_, (thyID, _)) => member (op=) (map Context.theory_name thys) thyID)
|
neuper@55405
|
131 |
|> map (makeHrls part)
|
neuper@37906
|
132 |
fun collect_cals (part, thy') =
|
neuper@55490
|
133 |
let val cals = [] (*FIXXXXXXXXXXME.WN060713 add thyID: (thyID, cal)*)
|
neuper@55490
|
134 |
in map (makeHcal (part, thy')) cals end;
|
neuper@37906
|
135 |
fun collect_ords (part, thy') =
|
walther@59881
|
136 |
let val thy = ThyC.get_theory thy'
|
walther@59917
|
137 |
in [(*TODO.WN060120 rew_ord, Eval*)]:(Thy_Write.theID * Thy_Write.thydata) list end;
|
neuper@37906
|
138 |
|
walther@59887
|
139 |
(* parts are: Isabelle | IsacKnowledge | IsacScripts, see Know_Store.thy *)
|
neuper@55405
|
140 |
fun collect_part part parent thys =
|
neuper@55448
|
141 |
(flat (map (collect_thms part) thys)) @
|
neuper@55448
|
142 |
(collect_rlss part (KEStore_Elems.get_rlss parent) thys) @
|
neuper@55405
|
143 |
[(*TODO: collect_cals, collect_ords*)]
|
neuper@37906
|
144 |
|
neuper@55490
|
145 |
(* collect theorems defined in Isabelle *)
|
neuper@42400
|
146 |
fun collect_isab isa (thmDeriv, thm) =
|
neuper@55490
|
147 |
let val theID =
|
walther@59879
|
148 |
[isa, ThyC.cut_id thmDeriv, "Theorems", ThmC.cut_id thmDeriv]
|
neuper@55490
|
149 |
in
|
walther@59917
|
150 |
(theID: Thy_Write.theID, Thy_Write.Hthm {guh = Thy_Write.theID2guh theID,
|
neuper@55490
|
151 |
mathauthors = ["Isabelle team, TU Munich"],
|
neuper@55490
|
152 |
coursedesign = [],
|
neuper@55490
|
153 |
fillpats = [],
|
neuper@55490
|
154 |
thm = thm})
|
neuper@55490
|
155 |
end
|
neuper@37906
|
156 |
|
walther@59971
|
157 |
fun show_thes () = (writeln o Pbl_Met_Hierarchy.format_pblIDl o (Store.scan [])) (get_thes ());
|
neuper@37906
|
158 |
|
neuper@37906
|
159 |
|
neuper@55490
|
160 |
(** create an xml representation for thehier: hierarchy of entries + files per entry **)
|
neuper@37906
|
161 |
|
neuper@55490
|
162 |
(* create an xml-hierarchy where the filname is created from the guh;
|
neuper@55490
|
163 |
ad DTD: a NODE contains an ID and zero or more NODEs*)
|
neuper@37906
|
164 |
fun hierarchy_guh h =
|
neuper@42407
|
165 |
let
|
neuper@42407
|
166 |
val i = indentation
|
neuper@42407
|
167 |
val j = indentation
|
walther@59897
|
168 |
fun node i p theID (Store.Node (id, _, ns)) =
|
neuper@55490
|
169 |
let
|
walther@59757
|
170 |
val p' = Pos.lev_on p
|
neuper@55490
|
171 |
val theID' = theID @ [id]
|
neuper@55490
|
172 |
in
|
neuper@55490
|
173 |
(indt i) ^ "<NODE>\n" ^
|
neuper@55490
|
174 |
(indt (i+j)) ^ "<ID> " ^ id ^ " </ID>\n" ^
|
neuper@55490
|
175 |
(indt (i+j)) ^ "<NO> " (*on this level*) ^ (string_of_int o last_elem) p' ^ " </NO>\n" ^
|
walther@59917
|
176 |
(indt (i+j)) ^ "<CONTENTREF> " ^ Thy_Write.theID2guh theID' ^ " </CONTENTREF>\n" ^
|
walther@59757
|
177 |
(nodes (i+j) (Pos.lev_dn p') theID' ns) ^
|
neuper@55490
|
178 |
(indt i) ^ "</NODE>\n"
|
neuper@55490
|
179 |
end
|
neuper@55490
|
180 |
and nodes _ _ _ [] = ""
|
walther@59757
|
181 |
| nodes i p theID (n :: ns) = (node i p theID n) ^ (nodes i (Pos.lev_on p) theID ns);
|
neuper@42407
|
182 |
in nodes j [0] [] h end;
|
neuper@37906
|
183 |
|
walther@59918
|
184 |
fun thy_hierarchy2file (path: Pbl_Met_Hierarchy.filepath) =
|
walther@59918
|
185 |
Pbl_Met_Hierarchy.str2file (path ^ "thy_hierarchy.xml")
|
neuper@55490
|
186 |
("<NODE>\n" ^
|
neuper@55490
|
187 |
" <ID> theory hierarchy </ID>\n" ^
|
neuper@55490
|
188 |
" <NO> 1 </NO>\n" ^
|
neuper@55490
|
189 |
" <CONTENTREF> thy_ROOT </CONTENTREF>\n" ^
|
neuper@55490
|
190 |
(hierarchy_guh (get_thes ())) ^
|
neuper@55490
|
191 |
"</NODE>");
|
neuper@37906
|
192 |
|
neuper@55490
|
193 |
(* create the xml-files for the thydata in the hierarchy *)
|
neuper@37906
|
194 |
val i = indentation;
|
neuper@42407
|
195 |
(* analoguous to 'fun met2xml' *)
|
walther@59917
|
196 |
fun thydata2xml (theID: Thy_Write.theID, Thy_Write.Html {guh, coursedesign, mathauthors, html}) =
|
neuper@42407
|
197 |
"<HTMLDATA>\n" ^
|
neuper@42407
|
198 |
indt i ^ "<GUH> "^ guh ^" </GUH>\n" ^
|
neuper@42407
|
199 |
id2xml i theID ^
|
neuper@42407
|
200 |
indt i ^ "<EXPLANATIONS> " ^ html ^ "</EXPLANATIONS>\n" ^
|
neuper@42407
|
201 |
authors2xml i "MATHAUTHORS" mathauthors ^
|
neuper@42407
|
202 |
authors2xml i "COURSEDESIGNS" coursedesign ^
|
walther@59905
|
203 |
"</HTMLDATA>\n" : xml
|
walther@59917
|
204 |
| thydata2xml (theID, Thy_Write.Hthm {guh, coursedesign, mathauthors, fillpats(*TODO?*), thm}) =
|
neuper@42407
|
205 |
"<THEOREMDATA>\n" ^
|
neuper@42407
|
206 |
indt i ^ "<GUH> "^ guh ^" </GUH>\n" ^
|
neuper@42407
|
207 |
id2xml i theID ^
|
neuper@55489
|
208 |
thm''2xml i thm ^
|
neuper@42407
|
209 |
indt i ^ "<PROOF>\n" ^
|
neuper@55490
|
210 |
extref2xml (i+i) "Proof of the theorem" (* TODO "Unsorted"vvv: distinguish Isabelle | Isac *)
|
neuper@55495
|
211 |
("http://www.ist.tugraz.at/projects/isac/www/kbase/thy/browser_info/HOL/HOL-Real/Isac/" ^
|
neuper@55490
|
212 |
nth 2 theID ^ ".html") ^
|
neuper@42407
|
213 |
indt i ^ "</PROOF>\n" ^
|
neuper@42407
|
214 |
indt i ^ "<EXPLANATIONS> </EXPLANATIONS>\n" ^
|
neuper@42407
|
215 |
authors2xml i "MATHAUTHORS" mathauthors ^
|
neuper@42407
|
216 |
authors2xml i "COURSEDESIGNS" coursedesign ^
|
neuper@42407
|
217 |
"</THEOREMDATA>\n"
|
walther@59917
|
218 |
| thydata2xml (theID, Thy_Write.Hrls {guh, coursedesign, mathauthors, thy_rls}) =
|
neuper@42407
|
219 |
"<RULESETDATA>\n" ^
|
neuper@42407
|
220 |
indt i ^ "<GUH> "^ guh ^" </GUH>\n" ^
|
neuper@42407
|
221 |
id2xml i theID ^
|
neuper@55492
|
222 |
rls2xml i thy_rls ^
|
neuper@42407
|
223 |
indt i ^ "<EXPLANATIONS> </EXPLANATIONS>\n" ^
|
neuper@42407
|
224 |
authors2xml i "MATHAUTHORS" mathauthors ^
|
neuper@37906
|
225 |
authors2xml i "COURSEDESIGNS" coursedesign ^
|
neuper@42407
|
226 |
"</RULESETDATA>\n"
|
walther@59917
|
227 |
| thydata2xml (theID, Thy_Write.Hcal {guh, coursedesign, mathauthors, calc}) =
|
neuper@42407
|
228 |
"<RULESETDATA>\n" ^
|
neuper@42407
|
229 |
indt i ^ "<GUH> "^ guh ^" </GUH>\n" ^
|
neuper@42407
|
230 |
id2xml i theID ^
|
walther@59917
|
231 |
calc2xml i (Thy_Write.theID2thyID theID, calc) ^
|
neuper@42407
|
232 |
indt i ^ "<EXPLANATIONS> </EXPLANATIONS>\n" ^
|
neuper@42407
|
233 |
authors2xml i "MATHAUTHORS" mathauthors ^
|
neuper@42407
|
234 |
authors2xml i "COURSEDESIGNS" coursedesign ^
|
neuper@42407
|
235 |
"</RULESETDATA>\n"
|
neuper@37906
|
236 |
| thydata2xml (theID, _) =
|
walther@59962
|
237 |
raise ERROR ("thydata2xml: not implemented for "^ strs2str' theID);
|
neuper@37906
|
238 |
|
neuper@42407
|
239 |
(* analoguous to 'fun met2file' *)
|
walther@59918
|
240 |
fun thydata2file (path : Pbl_Met_Hierarchy.filepath) (pos : Pos.pos) (theID : Thy_Write.theID) thydata =
|
neuper@42407
|
241 |
(writeln ("### thes2file: id = " ^ strs2str theID);
|
walther@59918
|
242 |
Pbl_Met_Hierarchy.str2file (path ^ Thy_Present.theID2filename theID) (thydata2xml (theID, thydata)));
|
neuper@37906
|
243 |
|
neuper@42407
|
244 |
(* analoguous to 'fun node' *)
|
walther@59918
|
245 |
fun thenode (pa : Pbl_Met_Hierarchy.filepath) ids po wfn (Store.Node (id, [n], ns)) =
|
walther@59757
|
246 |
let val po' = Pos.lev_on po
|
walther@59757
|
247 |
in wfn pa po' (ids @ [id]) n; thenodes pa (ids @ [id]) (Pos.lev_dn po') wfn ns end
|
neuper@37906
|
248 |
and thenodes _ _ _ _ [] = ()
|
neuper@42407
|
249 |
| thenodes pa ids po wfn (n::ns) =
|
walther@59757
|
250 |
(thenode pa ids po wfn n; thenodes pa ids (Pos.lev_on po) wfn ns);
|
neuper@37906
|
251 |
|
neuper@42407
|
252 |
(* analoguous to 'fun mets2file' *)
|
walther@59918
|
253 |
fun thes2file (p : Pbl_Met_Hierarchy.filepath) = thenodes p [] [0] thydata2file (get_thes ());
|
neuper@37906
|
254 |
|
neuper@37906
|
255 |
|
neuper@37906
|
256 |
(***.store a single theory element in the hierarchy.***)
|
neuper@37906
|
257 |
|
neuper@37906
|
258 |
(*.for mathauthors only, other html is added to xml exported from here.*)
|
walther@59917
|
259 |
fun make_isa thy (part, thypart) (mathauthors : Thy_Write.authors) =
|
neuper@55490
|
260 |
let
|
walther@59880
|
261 |
val theID = [part, Context.theory_name thy, thypart]
|
neuper@55490
|
262 |
val guh = case theID of
|
walther@59917
|
263 |
[part] => Thy_Write.part2guh theID
|
walther@59917
|
264 |
| [part, thyID, thypart] => Thy_Write.thypart2guh theID
|
walther@59917
|
265 |
val theID = Thy_Present.guh2theID guh
|
walther@59917
|
266 |
val the = Thy_Write.Html {guh = guh, coursedesign = [], mathauthors = mathauthors, html = ""}
|
neuper@55420
|
267 |
in (the, theID) end
|
neuper@55420
|
268 |
|
walther@59917
|
269 |
fun make_thy thy (mathauthors : Thy_Write.authors) =
|
neuper@55490
|
270 |
let
|
walther@59917
|
271 |
val guh = Thy_Write.thy2guh ["IsacKnowledge", Context.theory_name thy]
|
walther@59917
|
272 |
val theID = Thy_Present.guh2theID guh
|
walther@59917
|
273 |
val the = Thy_Write.Html {guh = guh, coursedesign = [], mathauthors = mathauthors, html = ""}
|
neuper@55420
|
274 |
in (the, theID) end
|
neuper@55420
|
275 |
|
walther@59917
|
276 |
fun make_thm thy part (thmID : ThmC.id, thm) (mathauthors : Thy_Write.authors) =
|
neuper@42411
|
277 |
let
|
walther@59917
|
278 |
val guh = Thy_Write.thm2guh (part, Context.theory_name thy) thmID
|
walther@59917
|
279 |
val theID = Thy_Present.guh2theID guh
|
walther@59917
|
280 |
val the = Thy_Write.Hthm {guh = guh, coursedesign = [(*inserted in xml after export*)],
|
neuper@55490
|
281 |
mathauthors = mathauthors, fillpats = [], thm = thm}
|
neuper@55420
|
282 |
in (the, theID) end
|
neuper@37906
|
283 |
|
walther@59917
|
284 |
fun make_rls thy rls (mathauthors : Thy_Write.authors) =
|
neuper@48887
|
285 |
let
|
walther@59917
|
286 |
val guh = Thy_Write.rls2guh ("IsacKnowledge", Context.theory_name thy) ((#id o Rule_Set.rep) rls)
|
walther@59917
|
287 |
val theID = Thy_Present.guh2theID guh
|
walther@59917
|
288 |
val the = Thy_Write.Hrls {guh = guh, coursedesign = [], mathauthors = mathauthors,
|
walther@59880
|
289 |
thy_rls = (Context.theory_name thy, rls)}
|
neuper@48887
|
290 |
(*needs no (!check_guhs_unique) because guh is generated automatically*)
|
neuper@55420
|
291 |
in (the, theID) end
|
neuper@37906
|
292 |
|
walther@59917
|
293 |
fun make_cal thy cal (mathauthors : Thy_Write.authors) =
|
neuper@55490
|
294 |
let
|
walther@59917
|
295 |
val guh = Thy_Write.cal2guh ("IsacKnowledge", Context.theory_name thy) ("TODO store_cal")
|
walther@59917
|
296 |
val theID = Thy_Present.guh2theID guh
|
walther@59917
|
297 |
val the = Thy_Write.Hcal {guh = guh, coursedesign = [], mathauthors = mathauthors, calc = cal}
|
neuper@55420
|
298 |
in (the, theID) end
|
neuper@37906
|
299 |
|
walther@59917
|
300 |
fun make_ord thy ord (mathauthors : Thy_Write.authors) =
|
neuper@55490
|
301 |
let
|
walther@59917
|
302 |
val guh = Thy_Write.ord2guh ("IsacKnowledge", Context.theory_name thy) ("TODO store_ord")
|
walther@59917
|
303 |
val theID = Thy_Present.guh2theID guh
|
walther@59917
|
304 |
val the = Thy_Write.Hord {guh = guh, coursedesign = [], mathauthors = mathauthors, ord = ord}
|
neuper@55420
|
305 |
in (the, theID) end
|
neuper@55420
|
306 |
|
walther@59918
|
307 |
(* for dialog-authoring *)
|
walther@59918
|
308 |
fun update_hrls (Thy_Write.Hrls {guh, coursedesign, mathauthors, thy_rls = (thyID, rls)}) errpatIDs =
|
walther@59918
|
309 |
let
|
walther@59918
|
310 |
val rls' =
|
walther@59918
|
311 |
case rls of
|
walther@59918
|
312 |
Rule_Def.Repeat {id, preconds, rew_ord, erls, srls, calc, rules, scr, ...}
|
walther@59918
|
313 |
=> Rule_Def.Repeat {id = id, preconds = preconds, rew_ord = rew_ord, erls = erls, srls = srls,
|
walther@59918
|
314 |
calc = calc, rules = rules, scr = scr, errpatts = errpatIDs}
|
walther@59918
|
315 |
| Rule_Set.Sequence {id, preconds, rew_ord, erls, srls, calc, rules, scr, ...}
|
walther@59918
|
316 |
=> Rule_Set.Sequence {id = id, preconds = preconds, rew_ord = rew_ord, erls = erls, srls = srls,
|
walther@59918
|
317 |
calc = calc, rules = rules, scr = scr, errpatts = errpatIDs}
|
walther@59918
|
318 |
| Rule_Set.Rrls {id, prepat, rew_ord, erls, calc, scr, ...}
|
walther@59918
|
319 |
=> Rule_Set.Rrls {id = id, prepat = prepat, rew_ord = rew_ord, erls = erls, calc = calc,
|
walther@59918
|
320 |
scr = scr, errpatts = errpatIDs}
|
walther@59918
|
321 |
| Erls => Erls
|
walther@59918
|
322 |
in
|
walther@59918
|
323 |
Thy_Write.Hrls {guh = guh, coursedesign = coursedesign, mathauthors = mathauthors,
|
walther@59918
|
324 |
thy_rls = (thyID, rls')}
|
walther@59918
|
325 |
end
|
walther@59918
|
326 |
| update_hrls _ _ = raise ERROR "update_hrls: wrong arguments";
|
walther@59918
|
327 |
|
neuper@55463
|
328 |
fun insert_errpatIDs thy theID errpatIDs = (* TODO: redo like insert_fillpatts *)
|
neuper@42452
|
329 |
let
|
walther@59970
|
330 |
val hrls = Thy_Read.from_store theID
|
walther@59918
|
331 |
val hrls' = update_hrls hrls errpatIDs
|
walther@59962
|
332 |
handle ERROR _ => raise ERROR ("insert_errpatIDs: " ^ strs2str theID ^ "must address a rule-set")
|
neuper@55420
|
333 |
in (hrls', theID) end
|
neuper@55420
|
334 |
|
walther@59874
|
335 |
(**)end(**)
|
walther@59874
|
336 |
open Thy_Hierarchy
|