1.1 --- a/src/Tools/isac/xmlsrc/thy-hierarchy.sml Tue Mar 13 15:04:27 2018 +0100
1.2 +++ b/src/Tools/isac/xmlsrc/thy-hierarchy.sml Thu Mar 15 10:17:44 2018 +0100
1.3 @@ -10,59 +10,59 @@
1.4
1.5 (* wrap theory-data into the uniform type thydata *)
1.6
1.7 -fun makeHthm (part : string, thyID : thyID) (thm : thm) =
1.8 - let val theID = [part, thyID, "Theorems"] @ [thmID_of_derivation_name' thm] : theID
1.9 - in (theID, Hthm {guh = theID2guh theID, coursedesign = [],
1.10 +fun makeHthm (part : string, thyID : Celem.thyID) (thm : thm) =
1.11 + let val theID = [part, thyID, "Theorems"] @ [Celem.thmID_of_derivation_name' thm] : Celem.theID
1.12 + in (theID, Celem.Hthm {guh = Celem.theID2guh theID, coursedesign = [],
1.13 mathauthors = ["isac-team"], fillpats = [], thm = thm})
1.14 end;
1.15 -fun makeHrls (part : string) (rls' : rls', thy_rls as (thyID, rls): thyID * rls) =
1.16 - let val theID = [part, thyID,"Rulesets"] @ [rls'] : theID
1.17 - in (theID, Hrls {guh = theID2guh theID, coursedesign=[],
1.18 +fun makeHrls (part : string) (rls' : Celem.rls', thy_rls as (thyID, rls): Celem.thyID * Celem.rls) =
1.19 + let val theID = [part, thyID,"Rulesets"] @ [rls'] : Celem.theID
1.20 + in (theID, Celem.Hrls {guh = Celem.theID2guh theID, coursedesign = [],
1.21 mathauthors = ["isac-team"], thy_rls = thy_rls})
1.22 end;
1.23 -fun makeHcal (part : string, thyID : thyID) (calID, cal) =
1.24 - let val theID = [part, thyID,"Operations"] @ [calID] : theID
1.25 - in (theID, Hcal {guh = theID2guh theID, coursedesign=[],
1.26 +fun makeHcal (part : string, thyID : Celem.thyID) (calID, cal) =
1.27 + let val theID = [part, thyID,"Operations"] @ [calID] : Celem.theID
1.28 + in (theID, Celem.Hcal {guh = Celem.theID2guh theID, coursedesign=[],
1.29 mathauthors = ["isac-team"], calc = cal})
1.30 end;
1.31 -fun makeHord (part : string, thyID : thyID) (ordID, ord) =
1.32 - let val theID = [part, thyID,"TODO-Orders"] @ [ordID] : theID
1.33 - in (theID, Hord {guh = theID2guh theID, coursedesign=[],
1.34 +fun makeHord (part : string, thyID : Celem.thyID) (ordID, ord) =
1.35 + let val theID = [part, thyID,"TODO-Orders"] @ [ordID] : Celem.theID
1.36 + in (theID, Celem.Hord {guh = Celem.theID2guh theID, coursedesign=[],
1.37 mathauthors = ["isac-team"], ord = ord})
1.38 end;
1.39
1.40 -fun revert_sym thy (Thm (thmID, thm)) =
1.41 - if (Rtools.is_sym o thmID_of_derivation_name) thmID
1.42 +fun revert_sym thy (Celem.Thm (thmID, thm)) =
1.43 + if (Rtools.is_sym o Celem.thmID_of_derivation_name) thmID
1.44 then
1.45 let
1.46 val thmID' = Rtools.sym_drop thmID
1.47 val thm' = Rewrite.assoc_thm' thy (thmID',"")
1.48 val thmDeriv' = Thm.get_name_hint thm'
1.49 - in Thm (thmDeriv', thm') end
1.50 - else Thm (Thm.get_name_hint thm, thm)
1.51 + in Celem.Thm (thmDeriv', thm') end
1.52 + else Celem.Thm (Thm.get_name_hint thm, thm)
1.53
1.54 (* get all theorems from the list of rule-sets (defined in Knowledge) *)
1.55 -fun thms_of_rlss thy rlss = (rlss : (rls' * (theory' * rls)) list)
1.56 +fun thms_of_rlss thy rlss = (rlss : (Celem.rls' * (Celem.theory' * Celem.rls)) list)
1.57 |> map (Rtools.thms_of_rls o #2 o #2)
1.58 |> flat
1.59 |> map (revert_sym thy)
1.60 - |> map (fn Thm (thmID, thm) => (thmID, thm))
1.61 + |> map (fn Celem.Thm (thmID, thm) => (thmID, thm))
1.62 |> gen_distinct (fn ((thmID1, _), (thmID2, _)) => thmID1 = thmID2)
1.63 - : (thmID * thm) list
1.64 + : (Celem.thmID * thm) list
1.65
1.66 (* collect all thydata defined in in a theory *)
1.67
1.68 fun collect_thms part thy =
1.69 map (makeHthm (part, Context.theory_name thy)) (rev (thms_of thy))
1.70 -fun collect_rlss part rlss thys = (rlss : (rls' * (thyID * rls)) list)
1.71 +fun collect_rlss part rlss thys = (rlss : (Celem.rls' * (Celem.thyID * Celem.rls)) list)
1.72 |> filter (fn (_, (thyID, _)) => member (op=) (map Context.theory_name thys) thyID)
1.73 |> map (makeHrls part)
1.74 fun collect_cals (part, thy') =
1.75 let val cals = [] (*FIXXXXXXXXXXME.WN060713 add thyID: (thyID, cal)*)
1.76 in map (makeHcal (part, thy')) cals end;
1.77 fun collect_ords (part, thy') =
1.78 - let val thy = assoc_thy (thyID2theory' thy')
1.79 - in [(*TODO.WN060120 rew_ord, Calc*)]:(theID * thydata) list end;
1.80 + let val thy = Celem.assoc_thy (Celem.thyID2theory' thy')
1.81 + in [(*TODO.WN060120 rew_ord, Calc*)]:(Celem.theID * Celem.thydata) list end;
1.82
1.83 (* parts are: Isabelle | IsacKnowledge | IsacScripts, see KEStore.thy *)
1.84 fun collect_part part parent thys =
1.85 @@ -73,9 +73,9 @@
1.86 (* collect theorems defined in Isabelle *)
1.87 fun collect_isab isa (thmDeriv, thm) =
1.88 let val theID =
1.89 - [isa, thyID_of_derivation_name thmDeriv, "Theorems", thmID_of_derivation_name thmDeriv]
1.90 + [isa, Celem.thyID_of_derivation_name thmDeriv, "Theorems", Celem.thmID_of_derivation_name thmDeriv]
1.91 in
1.92 - (theID:theID, Hthm {guh = theID2guh theID,
1.93 + (theID: Celem.theID, Celem.Hthm {guh = Celem.theID2guh theID,
1.94 mathauthors = ["Isabelle team, TU Munich"],
1.95 coursedesign = [],
1.96 fillpats = [],
1.97 @@ -93,7 +93,7 @@
1.98 let
1.99 val i = indentation
1.100 val j = indentation
1.101 - fun node i p theID (Ptyp (id, _, ns)) =
1.102 + fun node i p theID (Celem.Ptyp (id, _, ns)) =
1.103 let
1.104 val p' = Ctree.lev_on p
1.105 val theID' = theID @ [id]
1.106 @@ -101,7 +101,7 @@
1.107 (indt i) ^ "<NODE>\n" ^
1.108 (indt (i+j)) ^ "<ID> " ^ id ^ " </ID>\n" ^
1.109 (indt (i+j)) ^ "<NO> " (*on this level*) ^ (string_of_int o last_elem) p' ^ " </NO>\n" ^
1.110 - (indt (i+j)) ^ "<CONTENTREF> " ^ theID2guh theID' ^ " </CONTENTREF>\n" ^
1.111 + (indt (i+j)) ^ "<CONTENTREF> " ^ Celem.theID2guh theID' ^ " </CONTENTREF>\n" ^
1.112 (nodes (i+j) (Ctree.lev_dn p') theID' ns) ^
1.113 (indt i) ^ "</NODE>\n"
1.114 end
1.115 @@ -109,7 +109,7 @@
1.116 | nodes i p theID (n :: ns) = (node i p theID n) ^ (nodes i (Ctree.lev_on p) theID ns);
1.117 in nodes j [0] [] h end;
1.118
1.119 -fun thy_hierarchy2file (path:path) =
1.120 +fun thy_hierarchy2file (path: Celem.path) =
1.121 str2file (path ^ "thy_hierarchy.xml")
1.122 ("<NODE>\n" ^
1.123 " <ID> theory hierarchy </ID>\n" ^
1.124 @@ -121,15 +121,15 @@
1.125 (* create the xml-files for the thydata in the hierarchy *)
1.126 val i = indentation;
1.127 (* analoguous to 'fun met2xml' *)
1.128 -fun thydata2xml (theID:theID, Html {guh, coursedesign, mathauthors, html}) =
1.129 +fun thydata2xml (theID: Celem.theID, Celem.Html {guh, coursedesign, mathauthors, html}) =
1.130 "<HTMLDATA>\n" ^
1.131 indt i ^ "<GUH> "^ guh ^" </GUH>\n" ^
1.132 id2xml i theID ^
1.133 indt i ^ "<EXPLANATIONS> " ^ html ^ "</EXPLANATIONS>\n" ^
1.134 authors2xml i "MATHAUTHORS" mathauthors ^
1.135 authors2xml i "COURSEDESIGNS" coursedesign ^
1.136 - "</HTMLDATA>\n" : xml
1.137 - | thydata2xml (theID, Hthm {guh, coursedesign, mathauthors, fillpats(*TODO?*), thm}) =
1.138 + "</HTMLDATA>\n" : Celem.xml
1.139 + | thydata2xml (theID, Celem.Hthm {guh, coursedesign, mathauthors, fillpats(*TODO?*), thm}) =
1.140 "<THEOREMDATA>\n" ^
1.141 indt i ^ "<GUH> "^ guh ^" </GUH>\n" ^
1.142 id2xml i theID ^
1.143 @@ -143,7 +143,7 @@
1.144 authors2xml i "MATHAUTHORS" mathauthors ^
1.145 authors2xml i "COURSEDESIGNS" coursedesign ^
1.146 "</THEOREMDATA>\n"
1.147 - | thydata2xml (theID, Hrls {guh, coursedesign, mathauthors, thy_rls}) =
1.148 + | thydata2xml (theID, Celem.Hrls {guh, coursedesign, mathauthors, thy_rls}) =
1.149 "<RULESETDATA>\n" ^
1.150 indt i ^ "<GUH> "^ guh ^" </GUH>\n" ^
1.151 id2xml i theID ^
1.152 @@ -152,11 +152,11 @@
1.153 authors2xml i "MATHAUTHORS" mathauthors ^
1.154 authors2xml i "COURSEDESIGNS" coursedesign ^
1.155 "</RULESETDATA>\n"
1.156 - | thydata2xml (theID, Hcal {guh, coursedesign, mathauthors, calc}) =
1.157 + | thydata2xml (theID, Celem.Hcal {guh, coursedesign, mathauthors, calc}) =
1.158 "<RULESETDATA>\n" ^
1.159 indt i ^ "<GUH> "^ guh ^" </GUH>\n" ^
1.160 id2xml i theID ^
1.161 - calc2xml i (theID2thyID theID, calc) ^
1.162 + calc2xml i (Celem.theID2thyID theID, calc) ^
1.163 indt i ^ "<EXPLANATIONS> </EXPLANATIONS>\n" ^
1.164 authors2xml i "MATHAUTHORS" mathauthors ^
1.165 authors2xml i "COURSEDESIGNS" coursedesign ^
1.166 @@ -165,12 +165,12 @@
1.167 error ("thydata2xml: not implemented for "^ strs2str' theID);
1.168
1.169 (* analoguous to 'fun met2file' *)
1.170 -fun thydata2file (path : path) (pos : Ctree.pos) (theID : theID) thydata =
1.171 +fun thydata2file (path : Celem.path) (pos : Ctree.pos) (theID : Celem.theID) thydata =
1.172 (writeln ("### thes2file: id = " ^ strs2str theID);
1.173 str2file (path ^ Rtools.theID2filename theID) (thydata2xml (theID, thydata)));
1.174
1.175 (* analoguous to 'fun node' *)
1.176 -fun thenode (pa : path) ids po wfn (Ptyp (id, [n], ns)) =
1.177 +fun thenode (pa : Celem.path) ids po wfn (Celem.Ptyp (id, [n], ns)) =
1.178 let val po' = Ctree.lev_on po
1.179 in wfn pa po' (ids @ [id]) n; thenodes pa (ids @ [id]) (Ctree.lev_dn po') wfn ns end
1.180 and thenodes _ _ _ _ [] = ()
1.181 @@ -178,64 +178,64 @@
1.182 (thenode pa ids po wfn n; thenodes pa ids (Ctree.lev_on po) wfn ns);
1.183
1.184 (* analoguous to 'fun mets2file' *)
1.185 -fun thes2file (p : path) = thenodes p [] [0] thydata2file (get_thes ());
1.186 +fun thes2file (p : Celem.path) = thenodes p [] [0] thydata2file (get_thes ());
1.187
1.188
1.189 (***.store a single theory element in the hierarchy.***)
1.190
1.191 (*.for mathauthors only, other html is added to xml exported from here.*)
1.192 -fun make_isa thy (part, thypart) (mathauthors : authors) =
1.193 +fun make_isa thy (part, thypart) (mathauthors : Celem.authors) =
1.194 let
1.195 - val theID = [part, string_of_thy thy, thypart]
1.196 + val theID = [part, Celem.string_of_thy thy, thypart]
1.197 val guh = case theID of
1.198 - [part] => part2guh theID
1.199 - | [part, thyID, thypart] => thypart2guh theID
1.200 + [part] => Celem.part2guh theID
1.201 + | [part, thyID, thypart] => Celem.thypart2guh theID
1.202 val theID = Rtools.guh2theID guh
1.203 - val the = Html {guh = guh, coursedesign = [], mathauthors = mathauthors, html = ""}
1.204 + val the = Celem.Html {guh = guh, coursedesign = [], mathauthors = mathauthors, html = ""}
1.205 in (the, theID) end
1.206
1.207 -fun make_thy thy (mathauthors : authors) =
1.208 +fun make_thy thy (mathauthors : Celem.authors) =
1.209 let
1.210 - val guh = thy2guh ["IsacKnowledge", theory2thyID thy]
1.211 + val guh = Celem.thy2guh ["IsacKnowledge", Celem.theory2thyID thy]
1.212 val theID = Rtools.guh2theID guh
1.213 - val the = Html {guh = guh, coursedesign = [], mathauthors = mathauthors, html = ""}
1.214 + val the = Celem.Html {guh = guh, coursedesign = [], mathauthors = mathauthors, html = ""}
1.215 in (the, theID) end
1.216
1.217 -fun make_thm thy part (thmID : thmID, thm) (mathauthors : authors) =
1.218 +fun make_thm thy part (thmID : Celem.thmID, thm) (mathauthors : Celem.authors) =
1.219 let
1.220 - val guh = thm2guh (part, theory2thyID thy) thmID
1.221 + val guh = Celem.thm2guh (part, Celem.theory2thyID thy) thmID
1.222 val theID = Rtools.guh2theID guh
1.223 - val the = Hthm {guh = guh, coursedesign = [(*inserted in xml after export*)],
1.224 + val the = Celem.Hthm {guh = guh, coursedesign = [(*inserted in xml after export*)],
1.225 mathauthors = mathauthors, fillpats = [], thm = thm}
1.226 in (the, theID) end
1.227
1.228 -fun make_rls thy rls (mathauthors : authors) =
1.229 +fun make_rls thy rls (mathauthors : Celem.authors) =
1.230 let
1.231 - val guh = rls2guh ("IsacKnowledge", theory2thyID thy) ((#id o rep_rls) rls)
1.232 + val guh = Celem.rls2guh ("IsacKnowledge", Celem.theory2thyID thy) ((#id o Celem.rep_rls) rls)
1.233 val theID = Rtools.guh2theID guh
1.234 - val the = Hrls {guh = guh, coursedesign = [], mathauthors = mathauthors,
1.235 - thy_rls = (theory2thyID thy, rls)}
1.236 + val the = Celem.Hrls {guh = guh, coursedesign = [], mathauthors = mathauthors,
1.237 + thy_rls = (Celem.theory2thyID thy, rls)}
1.238 (*needs no (!check_guhs_unique) because guh is generated automatically*)
1.239 in (the, theID) end
1.240
1.241 -fun make_cal thy cal (mathauthors : authors) =
1.242 +fun make_cal thy cal (mathauthors : Celem.authors) =
1.243 let
1.244 - val guh = cal2guh ("IsacKnowledge", theory2thyID thy) ("TODO store_cal")
1.245 + val guh = Celem.cal2guh ("IsacKnowledge", Celem.theory2thyID thy) ("TODO store_cal")
1.246 val theID = Rtools.guh2theID guh
1.247 - val the = Hcal {guh = guh, coursedesign = [], mathauthors = mathauthors, calc = cal}
1.248 + val the = Celem.Hcal {guh = guh, coursedesign = [], mathauthors = mathauthors, calc = cal}
1.249 in (the, theID) end
1.250
1.251 -fun make_ord thy ord (mathauthors : authors) =
1.252 +fun make_ord thy ord (mathauthors : Celem.authors) =
1.253 let
1.254 - val guh = ord2guh ("IsacKnowledge", theory2thyID thy) ("TODO store_ord")
1.255 + val guh = Celem.ord2guh ("IsacKnowledge", Celem.theory2thyID thy) ("TODO store_ord")
1.256 val theID = Rtools.guh2theID guh
1.257 - val the = Hord {guh = guh, coursedesign = [], mathauthors = mathauthors, ord = ord}
1.258 + val the = Celem.Hord {guh = guh, coursedesign = [], mathauthors = mathauthors, ord = ord}
1.259 in (the, theID) end
1.260
1.261 fun insert_errpatIDs thy theID errpatIDs = (* TODO: redo like insert_fillpatts *)
1.262 let
1.263 val hrls = Specify.get_the theID
1.264 - val hrls' = update_hrls hrls errpatIDs
1.265 + val hrls' = Celem.update_hrls hrls errpatIDs
1.266 handle ERROR _ => error ("insert_errpatIDs: " ^ strs2str theID ^ "must address a rule-set")
1.267 in (hrls', theID) end
1.268