1.1 --- a/src/Tools/isac/Interpret/inform.sml Sun Aug 09 17:52:02 2015 +0200
1.2 +++ b/src/Tools/isac/Interpret/inform.sml Tue Aug 11 15:39:27 2015 +0200
1.3 @@ -113,8 +113,7 @@
1.4
1.5 (*calc-head as input*)
1.6 type icalhd =
1.7 - pos' * (*the position of the calc-head in the calc-tree
1.8 - pos' as (p,p_) where p_ is neglected due to pos_ below*)
1.9 + pos' * (*the position of the calc-head in the calc-tree*)
1.10 cterm' * (*the headline*)
1.11 imodel * (*the model (without Find) of the calc-head*)
1.12 pos_ * (*model belongs to Pbl or Met*)
2.1 --- a/src/Tools/isac/calcelems.sml Sun Aug 09 17:52:02 2015 +0200
2.2 +++ b/src/Tools/isac/calcelems.sml Tue Aug 11 15:39:27 2015 +0200
2.3 @@ -482,6 +482,11 @@
2.4 | ketype2str' Thy_ = "Theory"
2.5 | ketype2str' Pbl_ = "Problem"
2.6 | ketype2str' Met_ = "Method";
2.7 +fun str2ketype "Exp_" = Exp_
2.8 + | str2ketype "Thy_" = Thy_
2.9 + | str2ketype "Pbl_" = Pbl_
2.10 + | str2ketype "Met_" = Met_
2.11 + | str2ketype str = raise ERROR ("str2ketype: WRONG arg = " ^ str)
2.12
2.13 (*rewrite orders, also stored in 'type met' and type 'and rls'
2.14 The association list is required for 'rewrite.."rew_ord"..'
3.1 --- a/src/Tools/isac/xmlsrc/datatypes.sml Sun Aug 09 17:52:02 2015 +0200
3.2 +++ b/src/Tools/isac/xmlsrc/datatypes.sml Tue Aug 11 15:39:27 2015 +0200
3.3 @@ -73,6 +73,9 @@
3.4 fun xml_to_bool (XML.Elem (("BOOL", []), [XML.Text b])) = string_to_bool b
3.5 | xml_to_bool tree = error ("xml_to_bool: wrong XML.tree \n" ^ xmlstr 0 tree)
3.6
3.7 +fun xml_to_ketype (XML.Elem (("KETYPE", []), [XML.Text str])) = str2ketype str
3.8 + | xml_to_ketype tree = error ("xml_to_ketype: wrong XML.tree \n" ^ xmlstr 0 tree)
3.9 +
3.10 (*.handles string list like 'fun id2xml'.*)
3.11 fun authors2xml j str auts =
3.12 let fun autx _ [] = ""
3.13 @@ -471,6 +474,26 @@
3.14 XML.Elem (("BELONGSTO", []), [
3.15 XML.Text (case p_ of Pbl => "Pbl" | Met => "Met" | _ => "Und")]),
3.16 xml_of_spec spec])
3.17 +fun xml_to_imodel
3.18 + (XML.Elem (("IMODEL", []), [
3.19 + XML.Elem (("GIVEN", []), givens),
3.20 + (*XML.Elem (("WHERE", []), wheres), ... Where is never input*)
3.21 + XML.Elem (("FIND", []), finds),
3.22 + XML.Elem (("RELATE", []), relates)])) =
3.23 + ([Given (map xml_to_cterm givens),
3.24 + Find (map xml_to_cterm finds),
3.25 + Relate (map xml_to_cterm relates)]): imodel
3.26 + | xml_to_imodel x = raise ERROR ("xml_to_imodel: WRONG arg = " ^ xmlstr 0 x)
3.27 +fun xml_to_icalhd
3.28 + (XML.Elem (("ICALCHEAD", []), [
3.29 + pos as XML.Elem (("POSITION", []), _),
3.30 + headln as XML.Elem (("MATHML", []), _),
3.31 + imodel as XML.Elem (("MATHML", []), _),
3.32 + XML.Elem (("POS", []), [XML.Text belongsto]),
3.33 + spec as XML.Elem (("SPECIFICATION", []), _)])) =
3.34 + (xml_to_pos pos, xml_to_cterm headln, xml_to_imodel imodel,
3.35 + str2pos_ belongsto, xml_to_spec spec): icalhd
3.36 + | xml_to_icalhd x = raise ERROR ("xml_to_icalhd: WRONG arg = " ^ xmlstr 0 x)
3.37
3.38 fun sub2xml j (id, value) =
3.39 (indt j ^"<PAIR>\n"^
3.40 @@ -1168,13 +1191,16 @@
3.41 XML.Elem (("INSTANTIATED", []), [xml_of_term thminst]),
3.42 XML.Elem (("APPLTO", []), [xml_of_term applto])]
3.43
3.44 -fun xml_of_calcchanged calcid tag old del new =
3.45 +fun xml_of_calcchanged calcid tag old del new = (*TODO: make analogous to xml_to_calcchanged*)
3.46 XML.Elem ((tag, []),[
3.47 XML.Elem (("CALCID", []), [XML.Text (string_of_int calcid)]),
3.48 XML.Elem (("CALCCHANGED", []), [
3.49 xml_of_pos "UNCHANGED" old,
3.50 xml_of_pos "DELETED" del,
3.51 xml_of_pos "GENERATED" new])])
3.52 +fun xml_to_calcchanged (XML.Elem (("CALCCHANGED", []), [old, del, new])) =
3.53 + (xml_to_pos old, xml_to_pos del, xml_to_pos new)
3.54 + | xml_to_calcchanged x = raise ERROR ("xml_to_calcchanged: WRONG arg = " ^ xmlstr 0 x)
3.55 (*------------------------------------------------------------------
3.56 end
3.57 open datatypes;