1.1 --- a/src/Tools/isac/Frontend/interface.sml Sun Sep 13 12:37:57 2015 +0200
1.2 +++ b/src/Tools/isac/Frontend/interface.sml Sun Sep 20 11:29:49 2015 +0200
1.3 @@ -510,7 +510,7 @@
1.4 val ((pt,_),_) = get_calc cI
1.5 val pp = par_pblobj pt p
1.6 val chd = tryrefine pblID pt (pp, p_)
1.7 - in xml_of_matchpbl cI chd end)
1.8 + in contextpblOK2xml cI chd end)
1.9 handle _ => sysERROR2xml cI "error in kernel 16";
1.10
1.11 (* append a formula to the calculation *)
1.12 @@ -698,14 +698,14 @@
1.13 ((let val ((pt,_),_) = get_calc cI
1.14 val pp = par_pblobj pt p
1.15 val chd = initcontext_pbl pt (pp,p_)
1.16 - in xml_of_matchpbl cI chd end)
1.17 + in contextpblOK2xml cI chd end)
1.18 handle _ => sysERROR2xml cI "error in kernel 32")
1.19
1.20 | initContext cI Met_ (pos as (p,p_):pos') =
1.21 ((let val ((pt,_),_) = get_calc cI
1.22 val pp = par_pblobj pt p
1.23 val chd = initcontext_met pt (pp,p_)
1.24 - in xml_of_matchmet cI chd end)
1.25 + in contextmetOK2xml cI chd end)
1.26 handle _ => sysERROR2xml cI "error in kernel 33");
1.27
1.28 (* match a theorem, a ruleset (etc., selected in the knowledge-browser)
1.29 @@ -735,7 +735,7 @@
1.30 val pp = par_pblobj pt p
1.31 val keID = guh2kestoreID guh
1.32 val chd = context_pbl keID pt pp
1.33 - in xml_of_matchpbl cI chd end
1.34 + in contextpblOK2xml cI chd end
1.35 ) handle _ => sysERROR2xml cI "error in kernel 35")
1.36 | "met_" =>
1.37 ((let
1.38 @@ -743,7 +743,7 @@
1.39 val pp = par_pblobj pt p
1.40 val keID = guh2kestoreID guh
1.41 val chd = context_met keID pt pp
1.42 - in xml_of_matchmet cI chd end
1.43 + in contextmetOK2xml cI chd end
1.44 ) handle _ => sysERROR2xml cI "error in kernel 36")
1.45 | str => sysERROR2xml cI ("checkContext: str = " ^ str)
1.46
2.1 --- a/src/Tools/isac/Frontend/states.sml Sun Sep 13 12:37:57 2015 +0200
2.2 +++ b/src/Tools/isac/Frontend/states.sml Sun Sep 20 11:29:49 2015 +0200
2.3 @@ -138,9 +138,6 @@
2.4 | is_detail _ _ _ = false;
2.5 ----------------------------------------*)
2.6
2.7 -type iterID = int;
2.8 -type calcID = int;
2.9 -
2.10 val states = Synchronized.var "isac_states"
2.11 ([]:(calcID *
2.12 (calcstate *
3.1 --- a/src/Tools/isac/calcelems.sml Sun Sep 13 12:37:57 2015 +0200
3.2 +++ b/src/Tools/isac/calcelems.sml Sun Sep 20 11:29:49 2015 +0200
3.3 @@ -27,6 +27,9 @@
3.4 revise funs : id_of_thm, thm_of_thm, rep_thm_G', eq_thmI, eq_thmI', thm'_of_thm thm.
3.5 activate : thmID_of_derivation_name'
3.6 *)
3.7 +type iterID = int;
3.8 +type calcID = int;
3.9 +
3.10 type thmID = string; (* identifier for a thm (the shortest possible identifier) *)
3.11 type thmDeriv = string; (* WN120524 deprecated
3.12 thyID ^"."^ xxx ^"."^ thmID, see fun thmID_of_derivation_name
3.13 @@ -487,6 +490,12 @@
3.14 | str2ketype "Pbl_" = Pbl_
3.15 | str2ketype "Met_" = Met_
3.16 | str2ketype str = raise ERROR ("str2ketype: WRONG arg = " ^ str)
3.17 +(* for conversion from XML *)
3.18 +fun str2ketype' "exp" = Exp_
3.19 + | str2ketype' "thy" = Thy_
3.20 + | str2ketype' "pbl" = Pbl_
3.21 + | str2ketype' "met" = Met_
3.22 + | str2ketype' str = raise ERROR ("str2ketype': WRONG arg = " ^ str)
3.23
3.24 (*rewrite orders, also stored in 'type met' and type 'and rls'
3.25 The association list is required for 'rewrite.."rew_ord"..'
4.1 --- a/src/Tools/isac/xmlsrc/datatypes.sml Sun Sep 13 12:37:57 2015 +0200
4.2 +++ b/src/Tools/isac/xmlsrc/datatypes.sml Sun Sep 20 11:29:49 2015 +0200
4.3 @@ -73,7 +73,7 @@
4.4 fun xml_to_bool (XML.Elem (("BOOL", []), [XML.Text b])) = string_to_bool b
4.5 | xml_to_bool tree = raise ERROR ("xml_to_bool: wrong XML.tree \n" ^ xmlstr 0 tree)
4.6
4.7 -fun xml_to_ketype (XML.Elem (("KETYPE", []), [XML.Text str])) = str2ketype str
4.8 +fun xml_to_ketype (XML.Elem (("KETYPE", []), [XML.Text str])) = str2ketype' str
4.9 | xml_to_ketype tree = raise ERROR ("xml_to_ketype: wrong XML.tree \n" ^ xmlstr 0 tree)
4.10
4.11 (*.handles string list like 'fun id2xml'.*)
4.12 @@ -1144,64 +1144,110 @@
4.13
4.14 | xml_of_contthy (ContThm {thyID, thm, applto, applat, reword,
4.15 asms,lhs, rhs, result, resasms, asmrls}) =
4.16 - [XML.Elem (("GUH", []), [XML.Text thm]),
4.17 - XML.Elem (("APPLTO", []), [xml_of_term applto]),
4.18 - XML.Elem (("APPLAT", []), [xml_of_term applat]),
4.19 - XML.Elem (("ORDER", []), [ (* should be a theref2xml *)
4.20 - XML.Elem (("ID", []), [XML.Text reword])]),
4.21 - XML.Elem (("ASMSEVAL", []), map xml_of_asm_val asms),
4.22 - XML.Elem (("LHS", []), [xml_of_term (fst lhs)]),
4.23 - XML.Elem (("LHSINST", []), [xml_of_term (snd lhs)]),
4.24 - XML.Elem (("RHS", []), [xml_of_term (fst rhs)]),
4.25 - XML.Elem (("RHSINST", []), [xml_of_term (snd rhs)]),
4.26 - XML.Elem (("RESULT", []), [xml_of_term result]),
4.27 - XML.Elem (("ASSUMPTIONS", []), map xml_of_term resasms),
4.28 - XML.Elem (("EVALRLS", []), [xml_of_theref thyID "Rulesets" asmrls])]
4.29 + XML.Elem (("CONTEXTDATA", []), [
4.30 + XML.Elem (("GUH", []), [XML.Text thm]),
4.31 + XML.Elem (("APPLTO", []), [xml_of_term applto]),
4.32 + XML.Elem (("APPLAT", []), [xml_of_term applat]),
4.33 + XML.Elem (("ORDER", []), [ (* should be a theref2xml *)
4.34 + XML.Elem (("ID", []), [XML.Text reword])]),
4.35 + XML.Elem (("ASMSEVAL", []), map xml_of_asm_val asms),
4.36 + XML.Elem (("LHS", []), [xml_of_term (fst lhs)]),
4.37 + XML.Elem (("LHSINST", []), [xml_of_term (snd lhs)]),
4.38 + XML.Elem (("RHS", []), [xml_of_term (fst rhs)]),
4.39 + XML.Elem (("RHSINST", []), [xml_of_term (snd rhs)]),
4.40 + XML.Elem (("RESULT", []), [xml_of_term result]),
4.41 + XML.Elem (("ASSUMPTIONS", []), map xml_of_term resasms),
4.42 + XML.Elem (("EVALRLS", []), [xml_of_theref thyID "Rulesets" asmrls])])
4.43
4.44 | xml_of_contthy (ContThmInst {thyID, thm, bdvs, thminst, applto, applat,
4.45 reword, asms, lhs, rhs, result, resasms, asmrls}) =
4.46 - [XML.Elem (("GUH", []), [XML.Text thm]),
4.47 - XML.Elem (("SUBSLIST", []), [ (* should be an environment = substitution *)
4.48 - xml_of_cterm (subst2str' bdvs)]),
4.49 - XML.Elem (("INSTANTIATED", []), [xml_of_term thminst]),
4.50 - XML.Elem (("APPLTO", []), [xml_of_term applto]),
4.51 - XML.Elem (("APPLAT", []), [xml_of_term applat]),
4.52 - XML.Elem (("ORDER", []), [ (* should be a theref2xml *)
4.53 - XML.Elem (("ID", []), [XML.Text reword])]),
4.54 - XML.Elem (("ASMSEVAL", []), map xml_of_asm_val asms),
4.55 - XML.Elem (("LHS", []), [xml_of_term (fst lhs)]),
4.56 - XML.Elem (("LHSINST", []), [xml_of_term (snd lhs)]),
4.57 - XML.Elem (("RHS", []), [xml_of_term (fst rhs)]),
4.58 - XML.Elem (("RHSINST", []), [xml_of_term (snd rhs)]),
4.59 - XML.Elem (("RESULT", []), [xml_of_term result]),
4.60 - XML.Elem (("ASSUMPTIONS", []), map xml_of_term resasms),
4.61 - XML.Elem (("EVALRLS", []), [xml_of_theref thyID "Rulesets" asmrls])]
4.62 + XML.Elem (("CONTEXTDATA", []), [
4.63 + XML.Elem (("GUH", []), [XML.Text thm]),
4.64 + XML.Elem (("SUBSLIST", []), [ (* should be an environment = substitution *)
4.65 + xml_of_cterm (subst2str' bdvs)]),
4.66 + XML.Elem (("INSTANTIATED", []), [xml_of_term thminst]),
4.67 + XML.Elem (("APPLTO", []), [xml_of_term applto]),
4.68 + XML.Elem (("APPLAT", []), [xml_of_term applat]),
4.69 + XML.Elem (("ORDER", []), [ (* should be a theref2xml *)
4.70 + XML.Elem (("ID", []), [XML.Text reword])]),
4.71 + XML.Elem (("ASMSEVAL", []), map xml_of_asm_val asms),
4.72 + XML.Elem (("LHS", []), [xml_of_term (fst lhs)]),
4.73 + XML.Elem (("LHSINST", []), [xml_of_term (snd lhs)]),
4.74 + XML.Elem (("RHS", []), [xml_of_term (fst rhs)]),
4.75 + XML.Elem (("RHSINST", []), [xml_of_term (snd rhs)]),
4.76 + XML.Elem (("RESULT", []), [xml_of_term result]),
4.77 + XML.Elem (("ASSUMPTIONS", []), map xml_of_term resasms),
4.78 + XML.Elem (("EVALRLS", []), [xml_of_theref thyID "Rulesets" asmrls])])
4.79
4.80 | xml_of_contthy (ContRls {thyID = _, rls, applto, result, asms}) =
4.81 - [XML.Elem (("GUH", []), [XML.Text rls]),
4.82 - XML.Elem (("APPLTO", []), [xml_of_term applto]),
4.83 - XML.Elem (("RESULT", []), [xml_of_term result]),
4.84 - XML.Elem (("ASSUMPTIONS", []), map xml_of_term asms)]
4.85 + XML.Elem (("CONTEXTDATA", []), [
4.86 + XML.Elem (("GUH", []), [XML.Text rls]),
4.87 + XML.Elem (("APPLTO", []), [xml_of_term applto]),
4.88 + XML.Elem (("RESULT", []), [xml_of_term result]),
4.89 + XML.Elem (("ASSUMPTIONS", []), map xml_of_term asms)])
4.90
4.91 | xml_of_contthy (ContRlsInst {thyID = _, rls, bdvs, applto, result, asms}) =
4.92 - [XML.Elem (("GUH", []), [XML.Text rls]),
4.93 - XML.Elem (("SUBSLIST", []), [ (* should be an environment = substitution *)
4.94 - xml_of_cterm (subst2str' bdvs)]),
4.95 - XML.Elem (("INSTANTIATED", []), [xml_of_cterm (subst2str' bdvs)]),
4.96 - XML.Elem (("APPLTO", []), [xml_of_term applto]),
4.97 - XML.Elem (("RESULT", []), [xml_of_term result]),
4.98 - XML.Elem (("ASSUMPTIONS", []), map xml_of_term asms)]
4.99 + XML.Elem (("CONTEXTDATA", []), [
4.100 + XML.Elem (("GUH", []), [XML.Text rls]),
4.101 + XML.Elem (("SUBSLIST", []), [ (* should be an environment = substitution *)
4.102 + xml_of_cterm (subst2str' bdvs)]),
4.103 + XML.Elem (("INSTANTIATED", []), [xml_of_cterm (subst2str' bdvs)]),
4.104 + XML.Elem (("APPLTO", []), [xml_of_term applto]),
4.105 + XML.Elem (("RESULT", []), [xml_of_term result]),
4.106 + XML.Elem (("ASSUMPTIONS", []), map xml_of_term asms)])
4.107
4.108 | xml_of_contthy (ContNOrew {thyID = _, thm_rls, applto}) =
4.109 - [XML.Elem (("GUH", []), [XML.Text thm_rls]),
4.110 - XML.Elem (("APPLTO", []), [xml_of_term applto])]
4.111 + XML.Elem (("CONTEXTDATA", []), [
4.112 + XML.Elem (("GUH", []), [XML.Text thm_rls]),
4.113 + XML.Elem (("APPLTO", []), [xml_of_term applto])])
4.114
4.115 | xml_of_contthy (ContNOrewInst{thyID = _, thm_rls, bdvs, thminst, applto}) =
4.116 - [XML.Elem (("GUH", []), [XML.Text thm_rls]),
4.117 - XML.Elem (("SUBSLIST", []), [ (* should be an environment = substitution *)
4.118 - xml_of_cterm (subst2str' bdvs)]),
4.119 - XML.Elem (("INSTANTIATED", []), [xml_of_term thminst]),
4.120 - XML.Elem (("APPLTO", []), [xml_of_term applto])]
4.121 + XML.Elem (("CONTEXTDATA", []), [
4.122 + XML.Elem (("GUH", []), [XML.Text thm_rls]),
4.123 + XML.Elem (("SUBSLIST", []), [ (* should be an environment = substitution *)
4.124 + xml_of_cterm (subst2str' bdvs)]),
4.125 + XML.Elem (("INSTANTIATED", []), [xml_of_term thminst]),
4.126 + XML.Elem (("APPLTO", []), [xml_of_term applto])])
4.127 +
4.128 +fun matchpbl2xml (cI:calcID) (model_ok, pI, hdl, pbl, pre) =
4.129 + writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
4.130 + "<CONTEXTPBL>\n" ^
4.131 + " <GUH> " ^ pblID2guh pI ^ " </GUH>\n" ^
4.132 + " <STATUS> " ^ (if model_ok
4.133 + then "correct"
4.134 + else "incorrect") ^ " </STATUS>\n" ^
4.135 + " <HEAD>\n" ^
4.136 + term2xml i hdl ^ "\n" ^
4.137 + " </HEAD>\n" ^
4.138 + model2xml i pbl pre ^
4.139 + "</CONTEXTPBL>\n" ^
4.140 + "@@@@@end@@@@@");
4.141 +fun xml_of_matchpbl (model_ok, pI, hdl, pbl, pre) =
4.142 + XML.Elem (("CONTEXTDATA", []), [
4.143 + XML.Elem (("GUH", []), [XML.Text (pblID2guh pI)]),
4.144 + XML.Elem (("STATUS", []), [
4.145 + XML.Text ((if model_ok then "correct" else "incorrect"))]),
4.146 + XML.Elem (("HEAD", []), [xml_of_term hdl]),
4.147 + xml_of_model pbl pre])
4.148 +
4.149 +fun matchmet2xml (cI:calcID) (model_ok, pI, scr, pbl, pre) =
4.150 + writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
4.151 + "<CONTEXTMET>\n" ^
4.152 + " <GUH> " ^ metID2guh pI ^ " </GUH>\n" ^
4.153 + " <STATUS> " ^ (if model_ok
4.154 + then "correct"
4.155 + else "incorrect") ^ " </STATUS>\n" ^
4.156 + scr2xml i scr ^
4.157 + model2xml i pbl pre ^
4.158 + "</CONTEXTMET>\n" ^
4.159 + "@@@@@end@@@@@");
4.160 +fun xml_of_matchmet (model_ok, pI, scr, pbl, pre) =
4.161 + XML.Elem (("CONTEXTDATA", []), [
4.162 + XML.Elem (("GUH", []), [XML.Text (pblID2guh pI)]),
4.163 + XML.Elem (("STATUS", []), [
4.164 + XML.Text ((if model_ok then "correct" else "incorrect"))]),
4.165 + XML.Elem (("PROGRAM", []), [xml_of_src scr]),
4.166 + xml_of_model pbl pre])
4.167
4.168 fun xml_of_calcchanged calcid tag old del new = (*TODO: make analogous to xml_to_calcchanged*)
4.169 XML.Elem ((tag, []),[
5.1 --- a/src/Tools/isac/xmlsrc/interface-xml.sml Sun Sep 13 12:37:57 2015 +0200
5.2 +++ b/src/Tools/isac/xmlsrc/interface-xml.sml Sun Sep 20 11:29:49 2015 +0200
5.3 @@ -14,9 +14,6 @@
5.4 WN071004 these 2 simplifications are begun with CALCMESSAGE
5.5 *)
5.6
5.7 -type iterID = int;
5.8 -type calcID = int;
5.9 -
5.10
5.11
5.12 (** add and delete users -----------------------------------------------
5.13 @@ -222,48 +219,6 @@
5.14 [XML.Elem (("CALCID", []), [XML.Text (string_of_int calcid)]),
5.15 XML.Elem (("FORMHEADS", []), map xml_of_posterm fs)])
5.16
5.17 -fun matchpbl2xml (cI:calcID) (model_ok, pI, hdl, pbl, pre) =
5.18 - writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
5.19 - "<CONTEXTPBL>\n" ^
5.20 - " <GUH> " ^ pblID2guh pI ^ " </GUH>\n" ^
5.21 - " <STATUS> " ^ (if model_ok
5.22 - then "correct"
5.23 - else "incorrect") ^ " </STATUS>\n" ^
5.24 - " <HEAD>\n" ^
5.25 - term2xml i hdl ^ "\n" ^
5.26 - " </HEAD>\n" ^
5.27 - model2xml i pbl pre ^
5.28 - "</CONTEXTPBL>\n" ^
5.29 - "@@@@@end@@@@@");
5.30 -fun xml_of_matchpbl (_ : calcID) (model_ok, pI, hdl, pbl, pre) =
5.31 - XML.Elem (("CONTEXTPBL", []),
5.32 - ( (* WN150530: calcid will be required for asynchronous communication *)
5.33 - XML.Elem (("GUH", []), [XML.Text (pblID2guh pI)]) ::
5.34 - XML.Elem (("STATUS", []), [
5.35 - XML.Text ((if model_ok then "correct" else "incorrect"))]) ::
5.36 - XML.Elem (("HEAD", []), [xml_of_term hdl]) ::
5.37 - (xml_of_model pbl pre) :: []))
5.38 -
5.39 -fun matchmet2xml (cI:calcID) (model_ok, pI, scr, pbl, pre) =
5.40 - writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
5.41 - "<CONTEXTMET>\n" ^
5.42 - " <GUH> " ^ metID2guh pI ^ " </GUH>\n" ^
5.43 - " <STATUS> " ^ (if model_ok
5.44 - then "correct"
5.45 - else "incorrect") ^ " </STATUS>\n" ^
5.46 - scr2xml i scr ^
5.47 - model2xml i pbl pre ^
5.48 - "</CONTEXTMET>\n" ^
5.49 - "@@@@@end@@@@@");
5.50 -fun xml_of_matchmet (_ : calcID) (model_ok, pI, scr, pbl, pre) =
5.51 - XML.Elem (("CONTEXTMET", []),
5.52 - ( (* WN150530: calcid will be required for asynchronous communication *)
5.53 - XML.Elem (("GUH", []), [XML.Text (pblID2guh pI)]) ::
5.54 - XML.Elem (("STATUS", []), [
5.55 - XML.Text ((if model_ok then "correct" else "incorrect"))]) ::
5.56 - XML.Elem (("HEAD", []), [xml_of_src scr]) ::
5.57 - (xml_of_model pbl pre) :: []))
5.58 -
5.59 fun tryrefineOK2xml (cI:calcID) (ModSpec modspec) =
5.60 writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
5.61 "<TRYREFINE>\n" ^
5.62 @@ -456,7 +411,16 @@
5.63 fun contextthyOK2xml calcid contthy =
5.64 XML.Elem (("CONTEXTTHY", []), [
5.65 XML.Elem (("CALCID", []), [XML.Text (string_of_int calcid)]),
5.66 - XML.Elem (("CONTEXTDATA", []), xml_of_contthy contthy)])
5.67 + xml_of_contthy contthy])
5.68 +
5.69 +fun contextpblOK2xml calcid contpbl =
5.70 + XML.Elem (("CONTEXTPBL", []), [
5.71 + XML.Elem (("CALCID", []), [XML.Text (string_of_int calcid)]),
5.72 + xml_of_matchpbl contpbl])
5.73 +fun contextmetOK2xml calcid contmet =
5.74 + XML.Elem (("CONTEXTMET", []), [
5.75 + XML.Elem (("CALCID", []), [XML.Text (string_of_int calcid)]),
5.76 + xml_of_matchmet contmet])
5.77
5.78 fun findFillpatterns2xml (cI:calcID) pattIDs =
5.79 writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^