1.1 --- a/src/Tools/isac/BridgeLibisabelle/interface-xml.sml Fri Sep 09 10:53:51 2022 +0200
1.2 +++ b/src/Tools/isac/BridgeLibisabelle/interface-xml.sml Sun Sep 11 14:31:15 2022 +0200
1.3 @@ -6,49 +6,49 @@
1.4 keep tests of interaction Java-frontend <-> Kernel running.
1.5 *)
1.6
1.7 -fun adduserOK2xml (calcid : calcID) (userid : iterID) =
1.8 +fun adduserOK2xml (calcid : States.calcID) (userid : States.iterID) =
1.9 XML.Elem (("ADDUSER", []),
1.10 [XML.Elem (("CALCID", []), [XML.Text (string_of_int calcid)]),
1.11 XML.Elem (("USERID", []), [XML.Text (string_of_int userid)])])
1.12
1.13 -fun calctreeOK2xml (calcid : calcID) =
1.14 +fun calctreeOK2xml (calcid : States.calcID) =
1.15 XML.Elem (("CALCTREE", []),
1.16 [XML.Elem (("CALCID", []), [XML.Text (string_of_int calcid)])])
1.17 -fun deconstructcalctreeOK2xml (calcid : calcID) =
1.18 +fun deconstructcalctreeOK2xml (calcid : States.calcID) =
1.19 XML.Elem (("DELCALC", []),
1.20 [XML.Elem (("CALCID", []), [XML.Text (string_of_int calcid)])])
1.21
1.22 -fun iteratorOK2xml (calcid : calcID) (p : Pos.pos')=
1.23 +fun iteratorOK2xml (calcid : States.calcID) (p : Pos.pos')=
1.24 XML.Elem (("CALCITERATOR", []),
1.25 [XML.Elem (("CALCID", []), [XML.Text (string_of_int calcid)]),
1.26 xml_of_pos "POSITION" p])
1.27 -fun iteratorERROR2xml (calcid : calcID) =
1.28 +fun iteratorERROR2xml (calcid : States.calcID) =
1.29 XML.Elem (("CALCITERATOR", []),
1.30 [XML.Elem (("CALCID", []), [XML.Text (string_of_int calcid)]),
1.31 XML.Elem (("ERROR", []), [XML.Text " iteratorERROR2xml: pos does not exist "])])
1.32
1.33 -fun sysERROR2xml (calcid : calcID) str =
1.34 +fun sysERROR2xml (calcid : States.calcID) str =
1.35 XML.Elem (("SYSERROR", []),
1.36 [XML.Elem (("CALCID", []), [XML.Text (string_of_int calcid)]),
1.37 XML.Elem (("ERROR", []), [XML.Text (if str = "" then " ERROR in kernel " else str)])])
1.38
1.39 -fun refformulaOK2xml (calcid : calcID) p (Ctree.Form t) =
1.40 +fun refformulaOK2xml (calcid : States.calcID) p (Ctree.Form t) =
1.41 XML.Elem (("REFFORMULA", []),
1.42 [XML.Elem (("CALCID", []), [XML.Text (string_of_int calcid)]),
1.43 XML.Elem (("CALCFORMULA", []), [
1.44 xml_of_pos "POSITION" p,
1.45 xml_of_term_NEW t])])
1.46 - | refformulaOK2xml (calcid : calcID) p (Ctree.ModSpec modspec) =
1.47 + | refformulaOK2xml (calcid : States.calcID) p (Ctree.ModSpec modspec) =
1.48 XML.Elem (("REFFORMULA", []), [
1.49 XML.Elem (("CALCID", []), [XML.Text (string_of_int calcid)]),
1.50 (*L.Elem (("CALCHEAD*) xml_of_posmodspec (p, modspec)])
1.51
1.52 -fun gettacticOK2xml (calcid : calcID) tac =
1.53 +fun gettacticOK2xml (calcid : States.calcID) tac =
1.54 XML.Elem (("GETTACTIC", []),[
1.55 XML.Elem (("CALCID", []), [XML.Text (string_of_int calcid)]),
1.56 xml_of_tac tac])
1.57
1.58 -fun gettacticERROR2xml (calcid : calcID) str =
1.59 +fun gettacticERROR2xml (calcid : States.calcID) str =
1.60 XML.Elem (("GETTACTIC", []),[
1.61 XML.Elem (("CALCID", []), [XML.Text (string_of_int calcid)]),
1.62 XML.Elem (("ERROR", []), [XML.Text str])])
1.63 @@ -58,71 +58,71 @@
1.64 XML.Elem (("CALCID", []), [XML.Text (string_of_int calcid)]),
1.65 XML.Elem (("TACLIST", []), (map xml_of_tac tacs))])
1.66
1.67 -fun getasmsOK2xml (calcid : calcID) terms =
1.68 +fun getasmsOK2xml (calcid : States.calcID) terms =
1.69 XML.Elem (("ASSUMPTIONS", []), [
1.70 XML.Elem (("CALCID", []), [XML.Text (string_of_int calcid)]),
1.71 XML.Elem (("ASMLIST", []), (map xml_of_term_NEW terms))])
1.72
1.73 -fun getintervalOK (calcid : calcID) fs =
1.74 +fun getintervalOK (calcid : States.calcID) fs =
1.75 XML.Elem (("GETELEMENTSFROMTO", []),
1.76 [XML.Elem (("CALCID", []), [XML.Text (string_of_int calcid)]),
1.77 XML.Elem (("FORMHEADS", []), map xml_of_posterm fs)])
1.78
1.79 -fun appendformulaOK2xml (calcid : calcID) (old : Pos.pos') (del : Pos.pos') (new : Pos.pos') =
1.80 +fun appendformulaOK2xml (calcid : States.calcID) (old : Pos.pos') (del : Pos.pos') (new : Pos.pos') =
1.81 xml_of_calcchanged calcid "APPENDFORMULA" old del new
1.82 -fun appendformulaERROR2xml (calcid : calcID) e =
1.83 +fun appendformulaERROR2xml (calcid : States.calcID) e =
1.84 XML.Elem (("APPENDFORMULA", []), [
1.85 XML.Elem (("CALCID", []), [XML.Text (string_of_int calcid)]),
1.86 XML.Elem (("CALCMESSAGE", []), [XML.Text e])])
1.87
1.88 -fun replaceformulaOK2xml (calcid : calcID) (old : Pos.pos') (del : Pos.pos') (new : Pos.pos') =
1.89 +fun replaceformulaOK2xml (calcid : States.calcID) (old : Pos.pos') (del : Pos.pos') (new : Pos.pos') =
1.90 xml_of_calcchanged calcid "REPLACEFORMULA" old del new
1.91 -fun replaceformulaERROR2xml (calcid : calcID) e =
1.92 +fun replaceformulaERROR2xml (calcid : States.calcID) e =
1.93 XML.Elem (("REPLACEFORMULA", []), [
1.94 XML.Elem (("CALCID", []), [XML.Text (string_of_int calcid)]),
1.95 XML.Elem (("CALCMESSAGE", []), [XML.Text e])])
1.96
1.97 -fun message2xml (calcid : calcID) e =
1.98 +fun message2xml (calcid : States.calcID) e =
1.99 XML.Elem (("MESSAGE", []), [
1.100 XML.Elem (("CALCID", []), [XML.Text (string_of_int calcid)]),
1.101 XML.Elem (("STRING", []), [XML.Text e])])
1.102
1.103 -fun setnexttactic2xml (calcid : calcID) e =
1.104 +fun setnexttactic2xml (calcid : States.calcID) e =
1.105 XML.Elem (("SETNEXTTACTIC", []), [
1.106 XML.Elem (("CALCID", []), [XML.Text (string_of_int calcid)]),
1.107 XML.Elem (("MESSAGE", []), [XML.Text e])])
1.108
1.109 -fun fetchproposedtacticOK2xml (calcid : calcID) tac (errpatIDs : Error_Pattern_Def.id list) =
1.110 +fun fetchproposedtacticOK2xml (calcid : States.calcID) tac (errpatIDs : Error_Pattern_Def.id list) =
1.111 XML.Elem (("NEXTTAC", []), [
1.112 XML.Elem (("CALCID", []), [XML.Text (string_of_int calcid)]),
1.113 XML.Elem (("TACTICERRORPATTERNS", []), [xml_of_strs errpatIDs]),
1.114 xml_of_tac tac])
1.115
1.116 -fun fetchproposedtacticERROR2xml (calcid : calcID) e =
1.117 +fun fetchproposedtacticERROR2xml (calcid : States.calcID) e =
1.118 XML.Elem (("NEXTTAC", []), [
1.119 XML.Elem (("CALCID", []), [XML.Text (string_of_int calcid)]),
1.120 XML.Elem (("ERROR", []), [XML.Text e])])
1.121
1.122 -fun autocalculateOK2xml (calcid : calcID) (old : Pos.pos') (del : Pos.pos') (new : Pos.pos') =
1.123 +fun autocalculateOK2xml (calcid : States.calcID) (old : Pos.pos') (del : Pos.pos') (new : Pos.pos') =
1.124 xml_of_calcchanged calcid "AUTOCALC" old del new
1.125 -fun autocalculateERROR2xml (calcid : calcID) e =
1.126 +fun autocalculateERROR2xml (calcid : States.calcID) e =
1.127 XML.Elem (("AUTOCALC", []), [
1.128 XML.Elem (("CALCID", []), [XML.Text (string_of_int calcid)]),
1.129 XML.Elem (("CALCMESSAGE", []), [XML.Text e])])
1.130
1.131 -fun interStepsOK (calcid : calcID) (old : Pos.pos') (del : Pos.pos') (new : Pos.pos') =
1.132 +fun interStepsOK (calcid : States.calcID) (old : Pos.pos') (del : Pos.pos') (new : Pos.pos') =
1.133 xml_of_calcchanged calcid "INTERSTEPS" old del new
1.134 -fun interStepsERROR (calcid : calcID) e =
1.135 +fun interStepsERROR (calcid : States.calcID) e =
1.136 XML.Elem (("INTERSTEPS", []), [
1.137 XML.Elem (("CALCID", []), [XML.Text (string_of_int calcid)]),
1.138 XML.Elem (("CALCMESSAGE", []), [XML.Text e])])
1.139
1.140 -fun calcMessage2xml (cI: calcID) e =
1.141 +fun calcMessage2xml (cI: States.calcID) e =
1.142 writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n" ^
1.143 " <CALCMESSAGE> "^ e ^" </CALCMESSAGE>\n" ^
1.144 "@@@@@end@@@@@");
1.145
1.146 -fun modifycalcheadOK2xml (calcid : calcID) (chd as (complete, _ ,_ ,_ ,_ ,_) : SpecificationC.T) =
1.147 +fun modifycalcheadOK2xml (calcid : States.calcID) (chd as (complete, _ ,_ ,_ ,_ ,_) : SpecificationC.T) =
1.148 XML.Elem (("MODIFYCALCHEAD", []), [
1.149 XML.Elem (("CALCID", []), [XML.Text (string_of_int calcid)]),
1.150 XML.Elem (("STATUS", []), [
1.151 @@ -138,7 +138,7 @@
1.152 XML.Elem (("CALCID", []), [XML.Text (string_of_int calcid)]),
1.153 xml_of_matchmet contmet])
1.154
1.155 -fun findFillpatterns2xml (calcid : calcID) pattIDs =
1.156 +fun findFillpatterns2xml (calcid : States.calcID) pattIDs =
1.157 XML.Elem (("FINDFILLPATTERNS", []), [
1.158 XML.Elem (("CALCID", []), [XML.Text (string_of_int calcid)]),
1.159 xml_of_strs pattIDs])
2.1 --- a/src/Tools/isac/BridgeLibisabelle/interface.sml Fri Sep 09 10:53:51 2022 +0200
2.2 +++ b/src/Tools/isac/BridgeLibisabelle/interface.sml Sun Sep 11 14:31:15 2022 +0200
2.3 @@ -8,48 +8,48 @@
2.4
2.5 signature KERNEL =
2.6 sig
2.7 - val appendFormula : calcID -> TermC.as_string -> XML.tree (*unit future*)
2.8 - val autoCalculate : calcID -> Solve.auto -> XML.tree (*unit future*)
2.9 - val applyTactic : calcID -> Pos.pos' -> Tactic.input -> XML.tree
2.10 + val appendFormula : States.calcID -> TermC.as_string -> XML.tree (*unit future*)
2.11 + val autoCalculate : States.calcID -> Solve.auto -> XML.tree (*unit future*)
2.12 + val applyTactic : States.calcID -> Pos.pos' -> Tactic.input -> XML.tree
2.13 val CalcTree : Formalise.T list -> XML.tree
2.14 - val DEconstrCalcTree : calcID -> XML.tree
2.15 - val fetchApplicableTactics : calcID -> int -> Pos.pos' -> XML.tree
2.16 - val fetchProposedTactic : calcID -> XML.tree
2.17 - val findFillpatterns : calcID -> Error_Pattern_Def.id -> XML.tree
2.18 - val getAccumulatedAsms : calcID -> Pos.pos' -> XML.tree
2.19 - val getActiveFormula : calcID -> XML.tree
2.20 - val getAssumptions : calcID -> Pos.pos' -> XML.tree
2.21 - val getFormulaeFromTo : calcID -> Pos.pos' -> Pos.pos' -> int -> bool -> XML.tree
2.22 - val getTactic : calcID -> Pos.pos' -> XML.tree
2.23 - val inputFillFormula: calcID -> string -> XML.tree
2.24 - val interSteps : calcID -> Pos.pos' -> XML.tree
2.25 - val Iterator : calcID -> XML.tree
2.26 - val IteratorTEST : calcID -> iterID
2.27 - val modelProblem : calcID -> XML.tree
2.28 - val modifyCalcHead : calcID -> P_Spec.icalhd -> XML.tree
2.29 - val moveActiveCalcHead : calcID -> XML.tree
2.30 - val moveActiveDown : calcID -> XML.tree
2.31 - val moveActiveFormula : calcID -> Pos.pos' -> XML.tree
2.32 - val moveActiveLevelDown : calcID -> XML.tree
2.33 - val moveActiveLevelUp : calcID -> XML.tree
2.34 - val moveActiveRoot : calcID -> XML.tree
2.35 - val moveActiveRootTEST : calcID -> XML.tree
2.36 - val moveActiveUp : calcID -> XML.tree
2.37 - val moveCalcHead : calcID -> Pos.pos' -> XML.tree
2.38 - val moveDown : calcID -> Pos.pos' -> XML.tree
2.39 - val moveLevelDown : calcID -> Pos.pos' -> XML.tree
2.40 - val moveLevelUp : calcID -> Pos.pos' -> XML.tree
2.41 - val moveRoot : calcID -> XML.tree
2.42 - val moveUp : calcID -> Pos.pos' -> XML.tree
2.43 - val refFormula : calcID -> Pos.pos' -> XML.tree
2.44 - val refineProblem : calcID -> Pos.pos' -> Check_Unique.id -> XML.tree
2.45 - val replaceFormula : calcID -> TermC.as_string -> XML.tree
2.46 - val requestFillformula : calcID -> Error_Pattern_Def.id * Error_Pattern_Def.fill_in_id -> XML.tree
2.47 - val resetCalcHead : calcID -> XML.tree
2.48 - val setMethod : calcID -> MethodC.id -> XML.tree
2.49 - val setNextTactic : calcID -> Tactic.input -> XML.tree
2.50 - val setProblem : calcID -> Problem.id -> XML.tree
2.51 - val setTheory : calcID -> ThyC.id -> XML.tree
2.52 + val DEconstrCalcTree : States.calcID -> XML.tree
2.53 + val fetchApplicableTactics : States.calcID -> int -> Pos.pos' -> XML.tree
2.54 + val fetchProposedTactic : States.calcID -> XML.tree
2.55 + val findFillpatterns : States.calcID -> Error_Pattern_Def.id -> XML.tree
2.56 + val getAccumulatedAsms : States.calcID -> Pos.pos' -> XML.tree
2.57 + val getActiveFormula : States.calcID -> XML.tree
2.58 + val getAssumptions : States.calcID -> Pos.pos' -> XML.tree
2.59 + val getFormulaeFromTo : States.calcID -> Pos.pos' -> Pos.pos' -> int -> bool -> XML.tree
2.60 + val getTactic : States.calcID -> Pos.pos' -> XML.tree
2.61 + val inputFillFormula: States.calcID -> string -> XML.tree
2.62 + val interSteps : States.calcID -> Pos.pos' -> XML.tree
2.63 + val Iterator : States.calcID -> XML.tree
2.64 + val IteratorTEST : States.calcID -> States.iterID
2.65 + val modelProblem : States.calcID -> XML.tree
2.66 + val modifyCalcHead : States.calcID -> P_Spec.icalhd -> XML.tree
2.67 + val moveActiveCalcHead : States.calcID -> XML.tree
2.68 + val moveActiveDown : States.calcID -> XML.tree
2.69 + val moveActiveFormula : States.calcID -> Pos.pos' -> XML.tree
2.70 + val moveActiveLevelDown : States.calcID -> XML.tree
2.71 + val moveActiveLevelUp : States.calcID -> XML.tree
2.72 + val moveActiveRoot : States.calcID -> XML.tree
2.73 + val moveActiveRootTEST : States.calcID -> XML.tree
2.74 + val moveActiveUp : States.calcID -> XML.tree
2.75 + val moveCalcHead : States.calcID -> Pos.pos' -> XML.tree
2.76 + val moveDown : States.calcID -> Pos.pos' -> XML.tree
2.77 + val moveLevelDown : States.calcID -> Pos.pos' -> XML.tree
2.78 + val moveLevelUp : States.calcID -> Pos.pos' -> XML.tree
2.79 + val moveRoot : States.calcID -> XML.tree
2.80 + val moveUp : States.calcID -> Pos.pos' -> XML.tree
2.81 + val refFormula : States.calcID -> Pos.pos' -> XML.tree
2.82 + val refineProblem : States.calcID -> Pos.pos' -> Check_Unique.id -> XML.tree
2.83 + val replaceFormula : States.calcID -> TermC.as_string -> XML.tree
2.84 + val requestFillformula : States.calcID -> Error_Pattern_Def.id * Error_Pattern_Def.fill_in_id -> XML.tree
2.85 + val resetCalcHead : States.calcID -> XML.tree
2.86 + val setMethod : States.calcID -> MethodC.id -> XML.tree
2.87 + val setNextTactic : States.calcID -> Tactic.input -> XML.tree
2.88 + val setProblem : States.calcID -> Problem.id -> XML.tree
2.89 + val setTheory : States.calcID -> ThyC.id -> XML.tree
2.90 end
2.91
2.92 (**)
2.93 @@ -67,19 +67,19 @@
2.94 the only for updating the calc-tree
2.95 WN.0411: only 'Iterator 1' is stored,
2.96 all others are just calculated on the fly
2.97 - TODO: adapt Iterator, add_user(= add_iterator!),etc. accordingly .*)
2.98 + TODO: adapt Iterator, States.add_user(= add_iterator!),etc. accordingly .*)
2.99 fun Iterator cI = (*returned ID unnecessary after WN.0411*)
2.100 - case \<^try>\<open> (adduserOK2xml cI (add_user cI ))\<close> of
2.101 + case \<^try>\<open> (adduserOK2xml cI (States.add_user cI ))\<close> of
2.102 SOME xml => xml
2.103 | NONE => sysERROR2xml cI "error in kernel 1";
2.104 -fun IteratorTEST cI = add_user cI;
2.105 +fun IteratorTEST cI = States.add_user cI;
2.106
2.107 (* create a calc-tree; compare "fun CalcTreeTEST" *)
2.108 fun CalcTree [(fmz, sp)] (*for several variants lateron*) =
2.109 (case \<^try>\<open>
2.110 let
2.111 val cs = Step_Specify.nxt_specify_init_calc (fmz, sp)
2.112 - val cI = add_calc cs (*FIXME.WN.8.03: error-handling missing*)
2.113 + val cI = States.add_calc cs (*FIXME.WN.8.03: error-handling missing*)
2.114 in calctreeOK2xml cI end
2.115 \<close> of
2.116 SOME xml => xml
2.117 @@ -87,14 +87,14 @@
2.118 | CalcTree [] = raise ERROR "CalcTree: called with []"
2.119 | CalcTree _ = raise ERROR "CalcTree: undef.case in fun.def"
2.120
2.121 -fun DEconstrCalcTree cI = deconstructcalctreeOK2xml (del_calc cI);
2.122 -fun getActiveFormula cI = iteratorOK2xml cI (get_pos cI 1);
2.123 +fun DEconstrCalcTree cI = deconstructcalctreeOK2xml (States.del_calc cI);
2.124 +fun getActiveFormula cI = iteratorOK2xml cI (States.get_pos cI 1);
2.125
2.126 fun moveActiveFormula cI p =
2.127 - let val ((pt,_),_) = get_calc cI
2.128 + let val ((pt,_),_) = States.get_calc cI
2.129 in
2.130 if existpt' p pt
2.131 - then (upd_ipos cI 1 p; iteratorOK2xml cI p)
2.132 + then (States.upd_ipos cI 1 p; iteratorOK2xml cI p)
2.133 else sysERROR2xml cI "frontend sends a non-existing pos"
2.134 end
2.135
2.136 @@ -103,14 +103,14 @@
2.137 compare force NextTactic .*)
2.138 fun setNextTactic cI tac =
2.139 let
2.140 - val ((pt, _), _) = get_calc cI (* retrieve Calc.state_pre from states *)
2.141 - val ip = get_pos cI 1 (* retrieve position from states *)
2.142 + val ((pt, _), _) = States.get_calc cI (* retrieve Calc.state_pre from states *)
2.143 + val ip = States.get_pos cI 1 (* retrieve position from states *)
2.144 in
2.145 case Step.by_tactic tac (pt, ip) of
2.146 ("ok", (tacis, _, _)) => (* update Calc.state_pre in states *)
2.147 - (upd_calc cI ((pt, ip), tacis); setnexttactic2xml cI "ok")
2.148 + (States.upd_calc cI ((pt, ip), tacis); setnexttactic2xml cI "ok")
2.149 | ("unsafe-ok", (tacis, _, _)) =>
2.150 - (upd_calc cI ((pt, ip), tacis); setnexttactic2xml cI "unsafe-ok")
2.151 + (States.upd_calc cI ((pt, ip), tacis); setnexttactic2xml cI "unsafe-ok")
2.152 | ("not-applicable", _) => setnexttactic2xml cI "not-applicable"
2.153 | ("end-of-calculation", _) => setnexttactic2xml cI "end-of-calculation"
2.154 | (msg, _) => sysERROR2xml cI ("setNextTactic: Step.by_tactic returns " ^ msg)
2.155 @@ -120,31 +120,31 @@
2.156 (*WN080226 java-code is missing, errors smltest/Knowledge/polyminus.sml*)
2.157 fun applyTactic cI ip tac =
2.158 let
2.159 - val ((pt, _), _) = get_calc cI
2.160 - val p = get_pos cI 1
2.161 + val ((pt, _), _) = States.get_calc cI
2.162 + val p = States.get_pos cI 1
2.163 in
2.164 case Step.by_tactic tac (pt, ip) of
2.165 ("ok", (_, c, ptp as (_, p'))) =>
2.166 - (upd_calc cI (ptp, []);
2.167 - upd_ipos cI 1 p';
2.168 + (States.upd_calc cI (ptp, []);
2.169 + States.upd_ipos cI 1 p';
2.170 autocalculateOK2xml cI p (if null c then p' else last_elem c) p')
2.171 | ("unsafe-ok", (_, c, ptp as (_, p'))) =>
2.172 - (upd_calc cI (ptp, []);
2.173 - upd_ipos cI 1 p';
2.174 + (States.upd_calc cI (ptp, []);
2.175 + States.upd_ipos cI 1 p';
2.176 autocalculateOK2xml cI p (if null c then p' else last_elem c) p')
2.177 | ("end-of-calculation", (_, c, ptp as (_, p'))) =>
2.178 - (upd_calc cI (ptp, []);
2.179 - upd_ipos cI 1 p';
2.180 + (States.upd_calc cI (ptp, []);
2.181 + States.upd_ipos cI 1 p';
2.182 autocalculateOK2xml cI p (if null c then p' else last_elem c) p')
2.183 | (str, _) => autocalculateERROR2xml cI ("applyTactic: Step.by_tactic returns " ^ str)
2.184 end;
2.185
2.186 fun fetchProposedTactic cI =
2.187 case \<^try>\<open>
2.188 - (case Step.do_next (get_pos cI 1) (get_calc cI) of
2.189 + (case Step.do_next (States.get_pos cI 1) (States.get_calc cI) of
2.190 ("ok", (tacis, _, _)) =>
2.191 let
2.192 - val _ = upd_tacis cI tacis
2.193 + val _ = States.upd_tacis cI tacis
2.194 val (tac, _, _) = last_elem tacis
2.195 in fetchproposedtacticOK2xml cI tac (Error_Pattern.from_store tac) end
2.196 | ("helpless", _) => fetchproposedtacticERROR2xml cI "helpless"
2.197 @@ -157,17 +157,17 @@
2.198
2.199 fun autoCalculate cI auto = (*Future.fork
2.200 (fn () => (( *)let
2.201 - val pold = get_pos cI 1
2.202 + val pold = States.get_pos cI 1
2.203 in
2.204 - case Math_Engine.autocalc [] pold (get_calc cI) auto of
2.205 + case Math_Engine.autocalc [] pold (States.get_calc cI) auto of
2.206 ("ok", c, ptp as (_,p)) =>
2.207 - (upd_calc cI (ptp, []); upd_ipos cI 1 p;
2.208 + (States.upd_calc cI (ptp, []); States.upd_ipos cI 1 p;
2.209 autocalculateOK2xml cI pold (if null c then pold else last_elem c) p)
2.210 | ("dummy", c, ptp as (_,p)) => (*prelim. until \<open>Review modelling- + specification-phase\<close>*)
2.211 - (upd_calc cI (ptp, []); upd_ipos cI 1 p;
2.212 + (States.upd_calc cI (ptp, []); States.upd_ipos cI 1 p;
2.213 autocalculateOK2xml cI pold (if null c then pold else last_elem c) p)
2.214 | ("end-of-calculation", c, ptp as (_,p)) =>
2.215 - (upd_calc cI (ptp, []); upd_ipos cI 1 p;
2.216 + (States.upd_calc cI (ptp, []); States.upd_ipos cI 1 p;
2.217 autocalculateOK2xml cI pold (if null c then pold else last_elem c) p)
2.218 | (str, _, _) => autocalculateERROR2xml cI str
2.219 end (* ) *)
2.220 @@ -176,7 +176,7 @@
2.221 fun getTactic cI (p:pos') =
2.222 case \<^try>\<open>
2.223 let
2.224 - val ((pt, _), _) = get_calc cI
2.225 + val ((pt, _), _) = States.get_calc cI
2.226 val (_, tac, _) = ME_Misc.pt_extract (pt, p)
2.227 in
2.228 case tac of
2.229 @@ -196,7 +196,7 @@
2.230 *)
2.231 fun fetchApplicableTactics cI (_(*scope*): int) (p : pos') =
2.232 case \<^try>\<open>
2.233 - let val ((pt, _), _) = get_calc cI
2.234 + let val ((pt, _), _) = States.get_calc cI
2.235 in (applicabletacticsOK cI (Fetch_Tacs.from_prog pt p))
2.236 handle PTREE str => sysERROR2xml cI str
2.237 end
2.238 @@ -207,7 +207,7 @@
2.239 fun getAssumptions cI (p:pos') =
2.240 case \<^try>\<open>
2.241 let
2.242 - val ((pt, _), _) = get_calc cI
2.243 + val ((pt, _), _) = States.get_calc cI
2.244 val (_, _, asms) = ME_Misc.pt_extract (pt, p)
2.245 in getasmsOK2xml cI asms end
2.246 \<close> of
2.247 @@ -218,7 +218,7 @@
2.248 fun getAccumulatedAsms cI (p:pos') =
2.249 case \<^try>\<open>
2.250 let
2.251 - val ((pt, _), _) = get_calc cI
2.252 + val ((pt, _), _) = States.get_calc cI
2.253 val ass = Ctree.get_assumptions pt p
2.254 in getasmsOK2xml cI ass end
2.255 \<close> of
2.256 @@ -228,7 +228,7 @@
2.257 fun refFormula cI (p: pos') = (*WN0501 rename to "fun getElement" !*)
2.258 case \<^try>\<open>
2.259 let
2.260 - val ((pt, _), _) = get_calc cI
2.261 + val ((pt, _), _) = States.get_calc cI
2.262 val (form, _, _) = ME_Misc.pt_extract (pt, p)
2.263 in refformulaOK2xml cI p form end
2.264 \<close> of
2.265 @@ -242,7 +242,7 @@
2.266 fun getFormulaeFromTo cI (([], Pbl) : pos') (to as ([], Pbl) : pos') _ false =
2.267 (case \<^try>\<open>
2.268 let
2.269 - val ((pt,_),_) = get_calc cI
2.270 + val ((pt,_),_) = States.get_calc cI
2.271 val headline =
2.272 case ME_Misc.pt_extract (pt, to) of
2.273 (ModSpec (_, _, headline, _, _, _), _, _) => headline
2.274 @@ -263,7 +263,7 @@
2.275 "from=([],Res) .. goes beyond result")
2.276 | _ =>
2.277 let
2.278 - val ((pt,_),_) = get_calc cI
2.279 + val ((pt,_),_) = States.get_calc cI
2.280 val f = move_dn [] pt from
2.281 fun max (a,b) = if a < b then b else a
2.282 val lev = max (level, max (lev_of from, lev_of to)) (*... must reach margins *)
2.283 @@ -277,7 +277,7 @@
2.284
2.285 fun interSteps cI ip =
2.286 case \<^try>\<open>
2.287 - let val ((pt, p), tacis) = get_calc cI
2.288 + let val ((pt, p), tacis) = States.get_calc cI
2.289 in
2.290 if (not o is_interpos) ip
2.291 then interStepsERROR cI ("only formulae with position (_,Res) " ^
2.292 @@ -286,7 +286,7 @@
2.293 let val ip' = lev_pred' pt ip
2.294 in case Detail_Step.go pt ip of
2.295 ("detailrls", pt, lastpos) =>
2.296 - (upd_calc cI ((pt, p), tacis); interStepsOK cI ip' ip' lastpos)
2.297 + (States.upd_calc cI ((pt, p), tacis); interStepsOK cI ip' ip' lastpos)
2.298 | ("no-Rewrite_Set...", _, _) => sysERROR2xml cI "no Rewrite_Set..."
2.299 | (_, _, lastpos) => interStepsOK cI ip' ip' lastpos
2.300 end
2.301 @@ -298,9 +298,9 @@
2.302 fun modifyCalcHead cI (ichd as ((p,_),_,_,_,_) : P_Spec.icalhd) =
2.303 case \<^try>\<open>
2.304 let
2.305 - val ((pt,_),_) = get_calc cI
2.306 + val ((pt,_),_) = States.get_calc cI
2.307 val (pt, chd as (_,p_,_,_,_,_)) = P_Spec.input_icalhd pt ichd
2.308 - in (upd_calc cI ((pt, (p,p_)), []); modifycalcheadOK2xml cI chd) end
2.309 + in (States.upd_calc cI ((pt, (p,p_)), []); modifycalcheadOK2xml cI chd) end
2.310 \<close> of
2.311 SOME xml => xml
2.312 | NONE => sysERROR2xml cI "error in kernel 9";
2.313 @@ -310,9 +310,9 @@
2.314 fun resetCalcHead cI =
2.315 case \<^try>\<open>
2.316 let
2.317 - val (ptp,_) = get_calc cI
2.318 + val (ptp,_) = States.get_calc cI
2.319 val ptp = SpecificationC.reset ptp
2.320 - in (upd_calc cI (ptp, []); modifycalcheadOK2xml cI (SpecificationC.get ptp)) end
2.321 + in (States.upd_calc cI (ptp, []); modifycalcheadOK2xml cI (SpecificationC.get ptp)) end
2.322 \<close> of
2.323 SOME xml => xml
2.324 | NONE => sysERROR2xml cI "error in kernel 10";
2.325 @@ -321,10 +321,10 @@
2.326 the Descriptions are for user-guidance; the rest of the items are left empty for user-input *)
2.327 fun modelProblem cI =
2.328 case \<^try>\<open>
2.329 - let val (ptp, _) = get_calc cI
2.330 + let val (ptp, _) = States.get_calc cI
2.331 val ptp = SpecificationC.reset ptp
2.332 val (_, (_, _, ptp)) = Step_Specify.by_tactic_input Tactic.Model_Problem ptp
2.333 - in (upd_calc cI (ptp, []); modifycalcheadOK2xml cI (SpecificationC.get ptp)) end
2.334 + in (States.upd_calc cI (ptp, []); modifycalcheadOK2xml cI (SpecificationC.get ptp)) end
2.335 \<close> of
2.336 SOME xml => xml
2.337 | NONE => sysERROR2xml cI "error in kernel 11";
2.338 @@ -335,13 +335,13 @@
2.339 fun setMethod cI mI =
2.340 case \<^try>\<open>
2.341 let
2.342 - val ((pt, _), _) = get_calc cI
2.343 - val ip as (_, p_) = get_pos cI 1
2.344 + val ((pt, _), _) = States.get_calc cI
2.345 + val ip as (_, p_) = States.get_pos cI 1
2.346 in
2.347 if member op = [Pbl,Met] p_
2.348 then
2.349 let val (pt, chd) = Math_Engine.set_method mI (pt, ip)
2.350 - in (upd_calc cI ((pt, ip), []); modifycalcheadOK2xml cI chd) end
2.351 + in (States.upd_calc cI ((pt, ip), []); modifycalcheadOK2xml cI chd) end
2.352 else sysERROR2xml cI "setMethod requires ActiveFormula on CalcHead"
2.353 end
2.354 \<close> of
2.355 @@ -353,13 +353,13 @@
2.356 fun setProblem cI pI =
2.357 case \<^try>\<open>
2.358 let
2.359 - val ((pt, _), _) = get_calc cI
2.360 - val ip as (_, p_) = get_pos cI 1
2.361 + val ((pt, _), _) = States.get_calc cI
2.362 + val ip as (_, p_) = States.get_pos cI 1
2.363 in
2.364 if member op = [Pbl,Met] p_
2.365 then
2.366 let val (pt, chd) = Math_Engine.set_problem pI (pt, ip)
2.367 - in (upd_calc cI ((pt, ip), []); modifycalcheadOK2xml cI chd) end
2.368 + in (States.upd_calc cI ((pt, ip), []); modifycalcheadOK2xml cI chd) end
2.369 else sysERROR2xml cI "setProblem requires ActiveFormula on CalcHead"
2.370 end
2.371 \<close> of
2.372 @@ -371,13 +371,13 @@
2.373 fun setTheory cI tI =
2.374 case \<^try>\<open>
2.375 let
2.376 - val ((pt, _), _) = get_calc cI
2.377 - val ip as (_, p_) = get_pos cI 1
2.378 + val ((pt, _), _) = States.get_calc cI
2.379 + val ip as (_, p_) = States.get_pos cI 1
2.380 in
2.381 if member op = [Pbl,Met] p_
2.382 then
2.383 let val (pt, chd) = Math_Engine.set_theory tI (pt, ip)
2.384 - in (upd_calc cI ((pt, ip), []); modifycalcheadOK2xml cI chd) end
2.385 + in (States.upd_calc cI ((pt, ip), []); modifycalcheadOK2xml cI chd) end
2.386 else sysERROR2xml cI "setProblem requires ActiveFormula on CalcHead"
2.387 end
2.388 \<close> of
2.389 @@ -390,7 +390,7 @@
2.390 case \<^try>\<open>
2.391 let
2.392 val pblID = Ptool.guh2kestoreID guh
2.393 - val ((pt,_),_) = get_calc cI
2.394 + val ((pt,_),_) = States.get_calc cI
2.395 val pp = par_pblobj pt p
2.396 val chd = Math_Engine.tryrefine pblID pt (pp, p_)
2.397 in contextpblOK2xml cI chd end
2.398 @@ -401,17 +401,17 @@
2.399 (* append a formula to the calculation *)
2.400 fun appendFormula' cI (ifo: TermC.as_string) =
2.401 (let
2.402 - val cs = get_calc cI
2.403 - val pos = get_pos cI 1
2.404 + val cs = States.get_calc cI
2.405 + val pos = States.get_pos cI 1
2.406 in
2.407 case Step.do_next pos cs of
2.408 ("ok", (_, _, ptp)) =>
2.409 (case Step_Solve.by_term ptp (encode ifo) of
2.410 ("ok", (_(*use in DG !!!*), c, ptp as (_, p))) =>
2.411 - (upd_calc cI (ptp, []); upd_ipos cI 1 p;
2.412 + (States.upd_calc cI (ptp, []); States.upd_ipos cI 1 p;
2.413 appendformulaOK2xml cI pos (if null c then pos else last_elem c) p)
2.414 | ("same-formula", (_, c, ptp as (_, p))) =>
2.415 - (upd_calc cI (ptp, []); upd_ipos cI 1 p;
2.416 + (States.upd_calc cI (ptp, []); States.upd_ipos cI 1 p;
2.417 appendformulaOK2xml cI pos (if null c then pos else last_elem c) p)
2.418 | (msg, _) => appendformulaERROR2xml cI msg)
2.419 | (msg, _) => appendformulaERROR2xml cI msg
2.420 @@ -424,15 +424,15 @@
2.421 fun replaceFormula cI ifo =
2.422 case \<^try>\<open>
2.423 let
2.424 - val ((pt, _), _) = get_calc cI
2.425 - val p = get_pos cI 1
2.426 + val ((pt, _), _) = States.get_calc cI
2.427 + val p = States.get_pos cI 1
2.428 in
2.429 case Step_Solve.by_term (pt, p) (encode ifo) of
2.430 ("ok", (_(*tacs used for DG ?*), c, ptp' as (_, p'))) =>
2.431 let
2.432 val unc = if null (fst p) then p else move_up [] pt p
2.433 - val _ = upd_calc cI (ptp', [])
2.434 - val _ = upd_ipos cI 1 p'
2.435 + val _ = States.upd_calc cI (ptp', [])
2.436 + val _ = States.upd_ipos cI 1 p'
2.437 in replaceformulaOK2xml cI unc (if null c then unc else last_elem c) p' end
2.438 | ("same-formula", _) => replaceformulaERROR2xml cI "formula not changed"
2.439 | (msg, _) => replaceformulaERROR2xml cI msg
2.440 @@ -449,7 +449,7 @@
2.441
2.442 fun moveActiveRoot cI =
2.443 case \<^try>\<open>
2.444 - let val _ = upd_ipos cI 1 ([], Pbl)
2.445 + let val _ = States.upd_ipos cI 1 ([], Pbl)
2.446 in iteratorOK2xml cI ([], Pbl) end
2.447 \<close> of
2.448 SOME xml => xml
2.449 @@ -462,7 +462,7 @@
2.450 | NONE => sysERROR2xml cI "";
2.451 fun moveActiveRootTEST cI =
2.452 case \<^try>\<open>
2.453 - let val _ = upd_ipos cI 1 ([], Pbl)
2.454 + let val _ = States.upd_ipos cI 1 ([], Pbl)
2.455 in iteratorOK2xml cI ([], Pbl) end
2.456 \<close> of
2.457 SOME xml => xml
2.458 @@ -471,9 +471,9 @@
2.459 fun moveActiveDown cI =
2.460 case \<^try>\<open>
2.461 (let
2.462 - val ((pt, _), _) = get_calc cI
2.463 - val ip' = move_dn [] pt (get_pos cI 1)
2.464 - val _ = upd_ipos cI 1 ip'
2.465 + val ((pt, _), _) = States.get_calc cI
2.466 + val ip' = move_dn [] pt (States.get_pos cI 1)
2.467 + val _ = States.upd_ipos cI 1 ip'
2.468 in iteratorOK2xml cI ip' end)
2.469 handle (PTREE _) => iteratorERROR2xml cI
2.470 \<close> of
2.471 @@ -482,7 +482,7 @@
2.472 fun moveDown cI p =
2.473 case \<^try>\<open>
2.474 (let
2.475 - val ((pt, _), _) = get_calc cI
2.476 + val ((pt, _), _) = States.get_calc cI
2.477 val ip' = move_dn [] pt p
2.478 in iteratorOK2xml cI ip' end)
2.479 handle (PTREE _) => iteratorERROR2xml cI
2.480 @@ -493,9 +493,9 @@
2.481 fun moveActiveLevelDown cI =
2.482 case \<^try>\<open>
2.483 (let
2.484 - val ((pt, _) ,_) = get_calc cI
2.485 - val ip' = movelevel_dn [] pt (get_pos cI 1)
2.486 - val _ = upd_ipos cI 1 ip'
2.487 + val ((pt, _) ,_) = States.get_calc cI
2.488 + val ip' = movelevel_dn [] pt (States.get_pos cI 1)
2.489 + val _ = States.upd_ipos cI 1 ip'
2.490 in iteratorOK2xml cI ip' end)
2.491 handle (PTREE _) => iteratorERROR2xml cI
2.492 \<close> of
2.493 @@ -504,7 +504,7 @@
2.494 fun moveLevelDown cI p =
2.495 case \<^try>\<open>
2.496 (let
2.497 - val ((pt, _), _) = get_calc cI
2.498 + val ((pt, _), _) = States.get_calc cI
2.499 val ip' = movelevel_dn [] pt p
2.500 in iteratorOK2xml cI ip' end)
2.501 handle (PTREE _) => iteratorERROR2xml cI
2.502 @@ -515,9 +515,9 @@
2.503 fun moveActiveUp cI =
2.504 case \<^try>\<open>
2.505 (let
2.506 - val ((pt, _), _) = get_calc cI
2.507 - val ip' = move_up [] pt (get_pos cI 1)
2.508 - val _ = upd_ipos cI 1 ip'
2.509 + val ((pt, _), _) = States.get_calc cI
2.510 + val ip' = move_up [] pt (States.get_pos cI 1)
2.511 + val _ = States.upd_ipos cI 1 ip'
2.512 in iteratorOK2xml cI ip' end)
2.513 handle PTREE _ => iteratorERROR2xml cI
2.514 \<close> of
2.515 @@ -526,7 +526,7 @@
2.516 fun moveUp cI p =
2.517 case \<^try>\<open>
2.518 (let
2.519 - val ((pt, _), _) = get_calc cI
2.520 + val ((pt, _), _) = States.get_calc cI
2.521 val ip' = move_up [] pt p
2.522 in iteratorOK2xml cI ip' end)
2.523 handle PTREE _ => iteratorERROR2xml cI
2.524 @@ -537,9 +537,9 @@
2.525 fun moveActiveLevelUp cI =
2.526 case \<^try>\<open>
2.527 (let
2.528 - val ((pt, _), _) = get_calc cI
2.529 - val ip' = movelevel_up [] pt (get_pos cI 1)
2.530 - val _ = upd_ipos cI 1 ip'
2.531 + val ((pt, _), _) = States.get_calc cI
2.532 + val ip' = movelevel_up [] pt (States.get_pos cI 1)
2.533 + val _ = States.upd_ipos cI 1 ip'
2.534 in iteratorOK2xml cI ip' end)
2.535 handle PTREE _ => iteratorERROR2xml cI
2.536 \<close> of
2.537 @@ -548,7 +548,7 @@
2.538 fun moveLevelUp cI p =
2.539 case \<^try>\<open>
2.540 (let
2.541 - val ((pt, _), _) = get_calc cI
2.542 + val ((pt, _), _) = States.get_calc cI
2.543 val ip' = movelevel_up [] pt p
2.544 in iteratorOK2xml cI ip' end)
2.545 handle PTREE _ => iteratorERROR2xml cI
2.546 @@ -559,9 +559,9 @@
2.547 fun moveActiveCalcHead cI =
2.548 case \<^try>\<open>
2.549 (let
2.550 - val ((pt, _), _) = get_calc cI
2.551 - val ip' = movecalchd_up pt (get_pos cI 1)
2.552 - val _ = upd_ipos cI 1 ip'
2.553 + val ((pt, _), _) = States.get_calc cI
2.554 + val ip' = movecalchd_up pt (States.get_pos cI 1)
2.555 + val _ = States.upd_ipos cI 1 ip'
2.556 in iteratorOK2xml cI ip' end)
2.557 handle PTREE _ => iteratorERROR2xml cI
2.558 \<close> of
2.559 @@ -570,7 +570,7 @@
2.560 fun moveCalcHead cI p =
2.561 case \<^try>\<open>
2.562 (let
2.563 - val ((pt, _), _) = get_calc cI
2.564 + val ((pt, _), _) = States.get_calc cI
2.565 val ip' = movecalchd_up pt p
2.566 in iteratorOK2xml cI ip' end)
2.567 handle PTREE _ => iteratorERROR2xml cI
2.568 @@ -584,8 +584,8 @@
2.569 *)
2.570 fun findFillpatterns cI errpatID =
2.571 let
2.572 - val ((pt, _), _) = get_calc cI
2.573 - val pos = get_pos cI 1;
2.574 + val ((pt, _), _) = States.get_calc cI
2.575 + val pos = States.get_pos cI 1;
2.576 val fillpats = Error_Pattern.find_fill_patterns (pt, pos) errpatID
2.577 in findFillpatterns2xml cI (map #1 fillpats) end
2.578
2.579 @@ -597,8 +597,8 @@
2.580 *)
2.581 fun requestFillformula cI (errpatID, fillpatID) =
2.582 let
2.583 - val ((pt, _), _) = get_calc cI
2.584 - val pos = get_pos cI 1
2.585 + val ((pt, _), _) = States.get_calc cI
2.586 + val pos = States.get_pos cI 1
2.587 val fillforms = Error_Pattern.find_fill_patterns (pt, pos) errpatID
2.588 in
2.589 case filter ((curry op = fillpatID) o
2.590 @@ -608,7 +608,7 @@
2.591 val (pt, pos') = Step.inconsistent (sube_opt, ThmC.of_thm thm)
2.592 fillform (get_loc pt pos) pos pt
2.593 in
2.594 - (upd_calc cI ((pt, pos'), []); (*upd_ipos cI 1 pos';*)
2.595 + (States.upd_calc cI ((pt, pos'), []); (*States.upd_ipos cI 1 pos';*)
2.596 autocalculateOK2xml cI pos pos' pos')
2.597 end
2.598 | _ => autocalculateERROR2xml cI "no fillpattern found"
2.599 @@ -620,8 +620,8 @@
2.600 The respective thm is stored in the ctree. *)
2.601 fun inputFillFormula cI ifo =
2.602 let
2.603 - val ((pt, _), _) = get_calc cI
2.604 - val pos = get_pos cI 1;
2.605 + val ((pt, _), _) = States.get_calc cI
2.606 + val pos = States.get_pos cI 1;
2.607 in
2.608 case Error_Pattern.filled_exactly (pt, pos) ifo of
2.609 ("ok", tac) =>
2.610 @@ -629,16 +629,16 @@
2.611 in (* cp from applyTactic *)
2.612 case Step.by_tactic tac (pt, pos) of
2.613 ("ok", (_, c, ptp as (_,p'))) =>
2.614 - (upd_calc cI (ptp, []);
2.615 - upd_ipos cI 1 p';
2.616 + (States.upd_calc cI (ptp, []);
2.617 + States.upd_ipos cI 1 p';
2.618 autocalculateOK2xml cI pos (if null c then p' else last_elem c) p')
2.619 | ("unsafe-ok", (_, c, ptp as (_,p'))) =>
2.620 - (upd_calc cI (ptp, []);
2.621 - upd_ipos cI 1 p';
2.622 + (States.upd_calc cI (ptp, []);
2.623 + States.upd_ipos cI 1 p';
2.624 autocalculateOK2xml cI pos (if null c then p' else last_elem c) p')
2.625 | ("end-of-calculation", (_, c, ptp as (_,p'))) =>
2.626 - (upd_calc cI (ptp, []);
2.627 - upd_ipos cI 1 p';
2.628 + (States.upd_calc cI (ptp, []);
2.629 + States.upd_ipos cI 1 p';
2.630 autocalculateOK2xml cI pos (if null c then p' else last_elem c) p')
2.631 | _ => autocalculateERROR2xml cI "failure"
2.632 end
3.1 --- a/src/Tools/isac/Build_Isac.thy Fri Sep 09 10:53:51 2022 +0200
3.2 +++ b/src/Tools/isac/Build_Isac.thy Sun Sep 11 14:31:15 2022 +0200
3.3 @@ -195,7 +195,7 @@
3.4
3.5 section \<open>State of approaching Isabelle by Isac\<close>
3.6 text \<open>
3.7 - Mathias Lehnfeld gives the following list in his thesis in section
3.8 + Mathias Lehnfeld gives the following list in his thesis in section
3.9 4.2.3 Relation to Ongoing Isabelle Development.
3.10 \<close>
3.11 subsection \<open>(0) Survey on remaining Unsynchronized.ref\<close>
4.1 --- a/src/Tools/isac/MathEngine/states.sml Fri Sep 09 10:53:51 2022 +0200
4.2 +++ b/src/Tools/isac/MathEngine/states.sml Sun Sep 11 14:31:15 2022 +0200
4.3 @@ -3,6 +3,40 @@
4.4 use"states.sml";
4.5 *)
4.6
4.7 +signature STATES =
4.8 +sig
4.9 + eqtype iterID
4.10 + eqtype calcID
4.11 + val add_calc: Calc.state_pre -> calcID
4.12 + val get_calc: calcID -> Calc.state_pre
4.13 + val get_pos: calcID -> iterID -> Pos.pos'
4.14 + val del_calc: calcID -> calcID
4.15 + val add_user: calcID -> iterID
4.16 + val del_user: calcID -> iterID -> iterID
4.17 + val reset: unit -> unit
4.18 +(*val reset_states: unit -> unit*)
4.19 + val upd_calc: calcID -> Calc.state_pre -> unit
4.20 + val upd_ipos: calcID -> iterID -> Pos.pos' -> unit
4.21 + val upd_tacis: calcID -> State_Steps.T -> unit
4.22 +
4.23 +\<^isac_test>\<open>
4.24 +(** )val states: (calcID * (Calc.state_pre * (iterID * Pos.pos') list)) list Synchronized.var( **)
4.25 +
4.26 +(** )val del_assoc: (''a * 'b) list * ''a -> (''a * 'b) list( **)
4.27 +(** )val del_assoc2: calcID -> iterID -> (calcID * ('a * (iterID * 'b) list)) list -> (
4.28 + calcID * ('a * (iterID * 'b) list)) list( **)
4.29 +(** )val get_iterID: calcID -> (calcID * (Calc.state_pre * (iterID * Pos.pos') list)) list -> iterID( **)
4.30 +(** )val new_key: (iterID * 'a) list -> iterID -> iterID( **)
4.31 +(** )val overwrite2: (calcID * ('a * (iterID * 'b) list)) list * ((calcID * iterID) * 'b) ->
4.32 + (calcID * ('a * (iterID * 'b) list)) list( **)
4.33 +\<close>
4.34 + end
4.35 +
4.36 +(**)
4.37 +structure States(**): STATES(**) =
4.38 +struct
4.39 +(**)
4.40 +
4.41 type iterID = int;
4.42 type calcID = int;
4.43
4.44 @@ -15,7 +49,7 @@
4.45 (* TODO iterID * pos' should go to java-frontend *)
4.46 ) list)) list);
4.47
4.48 -fun reset_states () = Synchronized.change states (fn _ => []);
4.49 +fun reset () = Synchronized.change states (fn _ => []);
4.50 (*
4.51 states:= [(3,(Calc.state_empty_pre, [(1,e_pos'),
4.52 (3,e_pos')])),
4.53 @@ -50,15 +84,6 @@
4.54 > get_calcID 1 (!states);
4.55 val it = 1 : calcID
4.56 *)
4.57 -(* add users to a Calc.state_pre *)
4.58 -fun get_iterID (cI: calcID)
4.59 - (p: (calcID * (Calc.state_pre * (iterID * Pos.pos') list)) list) =
4.60 - case assoc (p, cI) of
4.61 - NONE => raise ERROR ("get_iterID: no iterID " ^ (string_of_int cI))
4.62 - | SOME (_, us) => (new_key us 1): iterID;
4.63 -(* get_iterID 3 (!states);
4.64 -val it = 2 : iterID*)
4.65 -
4.66
4.67 (** retrieve, update, delete a state by iterID, calcID **)
4.68
4.69 @@ -337,3 +362,5 @@
4.70 | (1, (((EmptyPtree, ([], Und)), []), [])),
4.71 | (3, (((EmptyPtree, ([], Und)), []), []))]
4.72 *)
4.73 +
4.74 +(**)end(*struct*)
5.1 --- a/test/Tools/isac/BridgeLibisabelle/interface.sml Fri Sep 09 10:53:51 2022 +0200
5.2 +++ b/test/Tools/isac/BridgeLibisabelle/interface.sml Sun Sep 11 14:31:15 2022 +0200
5.3 @@ -23,13 +23,13 @@
5.4 (* a simplified getter *)
5.5 fun test_get_calc cI =
5.6 case LibraryC.assoc (!test_states, cI) of
5.7 - NONE => error ("get_calc " ^ string_of_int cI ^ " not existent")
5.8 + NONE => error ("States.get_calc " ^ string_of_int cI ^ " not existent")
5.9 | SOME c => c;
5.10
5.11 (* a simplified updater *)
5.12 fun test_upd_calc cI cs =
5.13 (if is_none (LibraryC.assoc (!test_states, cI))
5.14 - then writeln ("upd_calc created new calculation " ^ string_of_int cI)
5.15 + then writeln ("States.upd_calc created new calculation " ^ string_of_int cI)
5.16 else ();
5.17 test_states := overwrite (!test_states, (cI, cs)))
5.18
5.19 @@ -50,7 +50,7 @@
5.20 "-------- ME_Misc.get_interval from ctree with move_dn:modspec.sml -------------------";
5.21 "-------- ME_Misc.get_interval from ctree with move_dn:modspec.sml -------------------";
5.22 "=====new ctree 1: crippled by cut_level_'_ ======================";
5.23 -reset_states ();
5.24 +States.reset ();
5.25 CalcTree
5.26 [(["equality (x/(x \<up> 2 - 6*x+9) - 1/(x \<up> 2 - 3*x) =1/x)",
5.27 "solveFor x", "solutions L"],
5.28 @@ -81,7 +81,7 @@
5.29
5.30 moveActiveFormula 1 ([4,2],Res)(*4.2.1.*);
5.31 interSteps 1 ([4,2],Res)(*..is activeFormula !?!*);
5.32 -val ((pt,_),_) = get_calc 1;
5.33 +val ((pt,_),_) = States.get_calc 1;
5.34 writeln(pr_ctree pr_short pt);
5.35 (*delete [4,1] in order to make pos [4],[4,4] for pblobjs differen [4],[4,3]:
5.36 ###########################################################################*)
6.1 --- a/test/Tools/isac/BridgeLibisabelle/thy-present.sml Fri Sep 09 10:53:51 2022 +0200
6.2 +++ b/test/Tools/isac/BridgeLibisabelle/thy-present.sml Sun Sep 11 14:31:15 2022 +0200
6.3 @@ -79,7 +79,7 @@
6.4 "----------- debugging on Tests/solve_linear_as_rootpbl -";
6.5 "----------- debugging on Tests/solve_linear_as_rootpbl -";
6.6 "----- initContext -----";
6.7 -reset_states ();
6.8 +States.reset ();
6.9 CalcTree
6.10 [(["equality (1+- 1*2+x=(0::real))", "solveFor x", "solutions L"],
6.11 ("Test",
6.12 @@ -88,11 +88,11 @@
6.13 Iterator 1; moveActiveRoot 1;
6.14 autoCalculate 1 CompleteCalcHead;
6.15
6.16 -autoCalculate 1 (Steps 1); val (ptp as (pt,p), tacis) = get_calc 1; Test_Tool.show_pt pt;
6.17 +autoCalculate 1 (Steps 1); val (ptp as (pt,p), tacis) = States.get_calc 1; Test_Tool.show_pt pt;
6.18 if is_curr_endof_calc pt ([1],Frm) then ()
6.19 else error "rewtools.sml is_curr_endof_calc ([1],Frm)";
6.20
6.21 -autoCalculate 1 (Steps 1); val (ptp as (pt,p), tacis) = get_calc 1; Test_Tool.show_pt pt;
6.22 +autoCalculate 1 (Steps 1); val (ptp as (pt,p), tacis) = States.get_calc 1; Test_Tool.show_pt pt;
6.23
6.24 if not (is_curr_endof_calc pt ([1],Frm)) then ()
6.25 else error "rewtools.sml is_curr_endof_calc ([1],Frm) not";
6.26 @@ -103,7 +103,7 @@
6.27 initContext 1 Ptool.Thy_ ([1],Res);
6.28
6.29 "----- checkContext -----";
6.30 -reset_states ();
6.31 +States.reset ();
6.32 CalcTree
6.33 [(["equality (1+- 1*2+x=(0::real))", "solveFor x", "solutions L"],
6.34 ("Test",
6.35 @@ -113,11 +113,11 @@
6.36 autoCalculate 1 CompleteCalc;
6.37 interSteps 1 ([1],Res);
6.38
6.39 -val (ptp as (pt,p), tacis) = get_calc 1; Test_Tool.show_pt pt;
6.40 +val (ptp as (pt,p), tacis) = States.get_calc 1; Test_Tool.show_pt pt;
6.41 checkContext 1 ([1],Res) "thy_isac_Test-rls-Test_simplify";
6.42
6.43 interSteps 1 ([2],Res);
6.44 -val (ptp as (pt,p), tacis) = get_calc 1; Test_Tool.show_pt pt;
6.45 +val (ptp as (pt,p), tacis) = States.get_calc 1; Test_Tool.show_pt pt;
6.46
6.47 checkContext 1 ([2,1],Res) "thy_isac_Test-rls-Test_simplify";
6.48 checkContext 1 ([2,2],Res) "thy_isac_Test-rls-Test_simplify";
7.1 --- a/test/Tools/isac/BridgeLibisabelle/use-cases.sml Fri Sep 09 10:53:51 2022 +0200
7.2 +++ b/test/Tools/isac/BridgeLibisabelle/use-cases.sml Sun Sep 11 14:31:15 2022 +0200
7.3 @@ -75,7 +75,7 @@
7.4
7.5
7.6 (*------------ set at startup of the Kernel ----------------------*)
7.7 -reset_states (); (*resets all state information in Kernel *)
7.8 +States.reset (); (*resets all state information in Kernel *)
7.9 (*----------------------------------------------------------------*)
7.10
7.11 "--------- empty rootpbl --------------------------------";
7.12 @@ -84,14 +84,14 @@
7.13 CalcTree [([], ("", [], []))];
7.14 Iterator 1;
7.15 moveActiveRoot 1;
7.16 - refFormula 1 (get_pos 1 1);
7.17 + refFormula 1 (States.get_pos 1 1);
7.18 (*WN.040222: stoert das sehr, dass ThyC.id_empty etc. statt leer kommt ???*)
7.19 DEconstrCalcTree 1;
7.20
7.21 "--------- solve_linear as rootpbl FE -------------------";
7.22 "--------- solve_linear as rootpbl FE -------------------";
7.23 "--------- solve_linear as rootpbl FE -------------------";
7.24 -reset_states ();
7.25 +States.reset ();
7.26
7.27 CalcTree (*start of calculation, return No.1*)
7.28 [(["equality (1+- 1*2+x=(0::real))", "solveFor x", "solutions L"],
7.29 @@ -101,58 +101,58 @@
7.30 Iterator 1; (*create an active Iterator on CalcTree No.1*)
7.31
7.32 moveActiveRoot 1;(*sets the CalcIterator No.1 at the root of CalcTree No.1*);
7.33 - refFormula 1 (get_pos 1 1) (*gets CalcHead; model is still empty*);
7.34 + refFormula 1 (States.get_pos 1 1) (*gets CalcHead; model is still empty*);
7.35
7.36
7.37 (*1*) fetchProposedTactic 1 (*by using Iterator No.1*);
7.38 setNextTactic 1 (Model_Problem); (*by using Iterator No.1*)
7.39 autoCalculate 1 (Steps 1);
7.40 - refFormula 1 (get_pos 1 1) (*model contains descriptions for all items*);
7.41 + refFormula 1 (States.get_pos 1 1) (*model contains descriptions for all items*);
7.42 autoCalculate 1 (Steps 1);
7.43 (*-----since Model_Problem + complete_mod_ in case cas of SOME-----*
7.44 (*2*) fetchProposedTactic 1;
7.45 setNextTactic 1 (Add_Given "equality (1 + - 1 * 2 + x = 0)");
7.46 - autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1); (*equality added*);
7.47 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1); (*equality added*);
7.48
7.49 (*3*) fetchProposedTactic 1;
7.50 setNextTactic 1 (Add_Given "solveFor x");
7.51 - autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);
7.52 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
7.53
7.54 (*4*) fetchProposedTactic 1;
7.55 setNextTactic 1 (Add_Find "solutions L");
7.56 - autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);
7.57 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
7.58
7.59 (*5*) fetchProposedTactic 1;
7.60 setNextTactic 1 (Specify_Theory "Test");
7.61 - autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);
7.62 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
7.63 *-----since Model_Problem + complete_mod_ in case cas of SOME-----*)
7.64
7.65 (*6*) fetchProposedTactic 1;
7.66 setNextTactic 1 (Specify_Problem ["LINEAR", "univariate", "equation", "test"]);
7.67 - autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);
7.68 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
7.69 (*-------------------------------------------------------------------------*)
7.70 (*7*) fetchProposedTactic 1;
7.71 - val (ptp as (pt,p), tacis) = get_calc 1; get_pos 1 1;
7.72 + val (ptp as (pt,p), tacis) = States.get_calc 1; States.get_pos 1 1;
7.73
7.74 setNextTactic 1 (Specify_Method ["Test", "solve_linear"]);
7.75 - val (ptp as (pt,p), tacis) = get_calc 1; get_pos 1 1;
7.76 + val (ptp as (pt,p), tacis) = States.get_calc 1; States.get_pos 1 1;
7.77
7.78 - autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);
7.79 - val (ptp as (pt,p), tacis) = get_calc 1; get_pos 1 1;
7.80 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
7.81 + val (ptp as (pt,p), tacis) = States.get_calc 1; States.get_pos 1 1;
7.82
7.83 (*-------------------------------------------------------------------------*)
7.84 (*8*) fetchProposedTactic 1;
7.85 - val (ptp as (pt,p), tacis) = get_calc 1; get_pos 1 1;
7.86 + val (ptp as (pt,p), tacis) = States.get_calc 1; States.get_pos 1 1;
7.87
7.88 (*8*) setNextTactic 1 (Apply_Method ["Test", "solve_linear"]);
7.89 (*ERROR.110620 <SETNEXTTACTIC>..<MESSAGE> end-of-calculation*)
7.90 - val (ptp as (pt,p), tacis) = get_calc 1; get_pos 1 1;
7.91 + val (ptp as (pt,p), tacis) = States.get_calc 1; States.get_pos 1 1;
7.92 SpecificationC.is_complete ptp;
7.93 References.are_complete ptp;
7.94
7.95 -(*8*) autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1); (*<---------------------- orig. test code*)
7.96 +(*8*) autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1); (*<---------------------- orig. test code*)
7.97
7.98 - val (ptp as (pt,p), tacis) = get_calc 1; get_pos 1 1; (*<---------------------- orig. test code*)
7.99 + val (ptp as (pt,p), tacis) = States.get_calc 1; States.get_pos 1 1; (*<---------------------- orig. test code*)
7.100 (*+isa=REP*) if p = ([1], Frm) andalso UnparseC.term (get_obj g_form pt [1]) = "1 + - 1 * 2 + x = 0"
7.101 andalso Istate.string_of (get_istate_LI pt p)
7.102 = "Pstate ([\"\n(e_e, 1 + - 1 * 2 + x = 0)\", \"\n(v_v, x)\"], [], empty, NONE, \n??.empty, ORundef, false, true)"
7.103 @@ -165,8 +165,8 @@
7.104 (*9*) setNextTactic 1 (Rewrite_Set_Inst (["(''bdv'',x)"], "isolate_bdv")); ( *<------- orig. test code*)
7.105
7.106 "~~~~~ fun setNextTactic , args:"; val (cI, tac) = (1, (Rewrite_Set_Inst (["(''bdv'',x)"], "isolate_bdv")));
7.107 - val ((pt'''''_', _), _) = get_calc cI
7.108 - val ip'''''_' = get_pos cI 1;
7.109 + val ((pt'''''_', _), _) = States.get_calc cI
7.110 + val ip'''''_' = States.get_pos cI 1;
7.111
7.112 val xxxxx_x(*"ok", (tacis, _, _)*) = (*case*) Step.by_tactic tac (pt'''''_', ip'''''_') (*of*);
7.113 (*+isa+REP*)val ("ok", ( [ (Rewrite_Set_Inst (["(''bdv'', x)"], "isolate_bdv"),
7.114 @@ -203,15 +203,15 @@
7.115 else error "from locate_input_tactic return --- changed";
7.116
7.117 val ("ok", (tacis'''''_', _, _)) = xxxxx_x;
7.118 -"~~~~~ from TOPLEVEL to states return:"; upd_calc cI ((pt'''''_', ip'''''_'), tacis'''''_');
7.119 +"~~~~~ from TOPLEVEL to states return:"; States.upd_calc cI ((pt'''''_', ip'''''_'), tacis'''''_');
7.120 (*\\=========================================== isa <> REP (1) ===============================//*)
7.121 (*//=========================================== isa <> REP (2) ===============================\\*)
7.122 (*9* ) autoCalculate 1 (Steps 1); (*<-------------------------------------------------- orig. test code*)
7.123 ( *isa: <AUTOCALC><CALCID>1</CALCID><CALCCHANGED><UNCHANGED><INTLIST><INT>1</INT></INTLIST><POS>Frm</POS></UNCHANGED><DELETED><INTLIST><INT>1</INT></INTLIST><POS>Frm</POS></DELETED><GENERATED><INTLIST><INT>1</INT></INTLIST><POS>Res</POS></GENERATED></CALCCHANGED></AUTOCALC>*)
7.124
7.125 "~~~~~ fun autoCalculate , args:"; val (cI, auto) = (1, (Steps 1));
7.126 - val pold = get_pos cI 1;
7.127 - val xxx = (get_calc cI);
7.128 + val pold = States.get_pos cI 1;
7.129 + val xxx = (States.get_calc cI);
7.130 (*isa*) val (**)xxxx(**) (**) = (**)
7.131 (*case*) Math_Engine.autocalc [] pold (xxx) auto (*of*);
7.132 "~~~~~ fun autocalc , args:"; val (c, ip, cs, (Solve.Steps s)) = ([], pold, (xxx), auto);
7.133 @@ -239,20 +239,20 @@
7.134 (*REP*) = "Pstate ([\"\n(e_e, 1 + - 1 * 2 + x = 0)\", \"\n(v_v, x)\"], [R, L, R, L, R, L, R], empty, SOME e_e, \nx = 0 + - 1 * (1 + - 1 * 2), ORundef, true, true)"
7.135 then () else error "REP autoCalculate on (e_e, 1 + - 1 * 2 + x = 0) changed"
7.136
7.137 -"~~~~~ from TOPLEVEL to states return:"; upd_calc cI (ptp, []); upd_ipos cI 1 p;
7.138 +"~~~~~ from TOPLEVEL to states return:"; States.upd_calc cI (ptp, []); States.upd_ipos cI 1 p;
7.139 (*\\=========================================== isa <> REP (2) ===============================//*)
7.140
7.141 (*10*) fetchProposedTactic 1;
7.142 setNextTactic 1 (Rewrite_Set "Test_simplify");
7.143 - autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);
7.144 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
7.145
7.146 (*11*) fetchProposedTactic 1;
7.147 setNextTactic 1 (Check_Postcond ["LINEAR", "univariate", "equation", "test"]);
7.148 - autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);
7.149 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
7.150
7.151 (*======= final test ==================================================*)
7.152 - val ((pt,_),_) = get_calc 1;
7.153 - val ip = get_pos 1 1;
7.154 + val ((pt,_),_) = States.get_calc 1;
7.155 + val ip = States.get_pos 1 1;
7.156
7.157 val (Form f, tac, asms) = ME_Misc.pt_extract (pt, ip);
7.158 (*exception just above means: 'ModSpec' has been returned: error anyway*)
7.159 @@ -277,10 +277,10 @@
7.160 moveActiveDown 1;
7.161 moveActiveDown 1;
7.162 moveActiveDown 1;
7.163 - if get_pos 1 1 = ([2], Res) then () else
7.164 + if States.get_pos 1 1 = ([2], Res) then () else
7.165 error "FE-interface.sml: diff.behav. in a inspect 1 with Iterator 2";
7.166 moveActiveDown 1; refFormula 1 ([], Res);
7.167 - if get_pos 1 1 = ([], Res) then () else
7.168 + if States.get_pos 1 1 = ([], Res) then () else
7.169 error "FE-interface.sml: diff.behav. in b inspect 1 with Iterator 2";
7.170 moveActiveCalcHead 1; refFormula 1 ([],Pbl);
7.171 DEconstrCalcTree 1;
7.172 @@ -297,112 +297,112 @@
7.173 Iterator 1;
7.174
7.175 moveActiveRoot 1;
7.176 - refFormula 1 (get_pos 1 1);
7.177 + refFormula 1 (States.get_pos 1 1);
7.178 fetchProposedTactic 1;
7.179 setNextTactic 1 (Model_Problem);
7.180 - autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);(*gets ModSpec;model is still empty*)
7.181 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);(*gets ModSpec;model is still empty*)
7.182
7.183 fetchProposedTactic 1; (*<SYSERROR><CALCID>1</CALCID><ERROR>error in kernel 3</ERROR></SYSERROR>* )
7.184 setNextTactic 1 (Add_Given "equality (x + 1 = 2)");
7.185 - autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);
7.186 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
7.187
7.188 fetchProposedTactic 1;
7.189 setNextTactic 1 (Add_Given "solveFor x");
7.190 - autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);
7.191 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
7.192
7.193 fetchProposedTactic 1;
7.194 setNextTactic 1 (Add_Find "solutions L");
7.195 - autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);
7.196 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
7.197
7.198 fetchProposedTactic 1;
7.199 setNextTactic 1 (Specify_Theory "Test");
7.200 - autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);
7.201 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
7.202
7.203 fetchProposedTactic 1;
7.204 setNextTactic 1 (Specify_Problem
7.205 ["sqroot-test", "univariate", "equation", "test"]);
7.206 - autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);
7.207 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
7.208 "1-----------------------------------------------------------------";
7.209
7.210 fetchProposedTactic 1;
7.211 setNextTactic 1 (Specify_Method ["Test", "squ-equ-test-subpbl1"]);
7.212 - autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);
7.213 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
7.214
7.215 fetchProposedTactic 1;
7.216 setNextTactic 1 (Apply_Method ["Test", "squ-equ-test-subpbl1"]);
7.217 - autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);
7.218 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
7.219
7.220 fetchProposedTactic 1;
7.221 setNextTactic 1 (Rewrite_Set "norm_equation");
7.222 - autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);
7.223 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
7.224
7.225 fetchProposedTactic 1;
7.226 setNextTactic 1 (Rewrite_Set "Test_simplify");
7.227 - autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);
7.228 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
7.229
7.230 fetchProposedTactic 1;(*----------------Subproblem--------------------*);
7.231 setNextTactic 1 (Subproblem ("Test",
7.232 ["LINEAR", "univariate", "equation", "test"]));
7.233 - autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);
7.234 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
7.235
7.236 fetchProposedTactic 1;
7.237 setNextTactic 1 (Model_Problem );
7.238 - autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);
7.239 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
7.240
7.241 fetchProposedTactic 1;
7.242 setNextTactic 1 (Add_Given "equality (- 1 + x = 0)");
7.243 - autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);
7.244 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
7.245
7.246 fetchProposedTactic 1;
7.247 setNextTactic 1 (Add_Given "solveFor x");
7.248 - autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);
7.249 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
7.250
7.251 fetchProposedTactic 1;
7.252 setNextTactic 1 (Add_Find "solutions x_i");
7.253 - autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);
7.254 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
7.255
7.256 fetchProposedTactic 1;
7.257 setNextTactic 1 (Specify_Theory "Test");
7.258 - autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);
7.259 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
7.260
7.261 fetchProposedTactic 1;
7.262 setNextTactic 1 (Specify_Problem ["LINEAR", "univariate", "equation", "test"]);
7.263 - autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);
7.264 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
7.265 "2-----------------------------------------------------------------";
7.266
7.267 fetchProposedTactic 1;
7.268 setNextTactic 1 (Specify_Method ["Test", "solve_linear"]);
7.269 - autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);
7.270 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
7.271
7.272 fetchProposedTactic 1;
7.273 setNextTactic 1 (Apply_Method ["Test", "solve_linear"]);
7.274 - autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);
7.275 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
7.276
7.277 fetchProposedTactic 1;
7.278 setNextTactic 1 (Rewrite_Set_Inst (["(''bdv'',x)"], "isolate_bdv"));
7.279 - autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);
7.280 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
7.281
7.282 fetchProposedTactic 1;
7.283 setNextTactic 1 (Rewrite_Set "Test_simplify");
7.284 - autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);
7.285 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
7.286
7.287 fetchProposedTactic 1;
7.288 setNextTactic 1 (Check_Postcond ["LINEAR", "univariate", "equation", "test"]);
7.289 - autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);
7.290 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
7.291
7.292 fetchProposedTactic 1;
7.293 setNextTactic 1 (Check_elementwise "Assumptions");
7.294 - autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);
7.295 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
7.296
7.297 val xml = fetchProposedTactic 1;
7.298 setNextTactic 1 (Check_Postcond
7.299 ["sqroot-test", "univariate", "equation", "test"]);
7.300 - autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);
7.301 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
7.302
7.303 - val ((pt,_),_) = get_calc 1;
7.304 + val ((pt,_),_) = States.get_calc 1;
7.305 val str = pr_ctree pr_short pt;
7.306 writeln str;
7.307 - val ip = get_pos 1 1;
7.308 + val ip = States.get_pos 1 1;
7.309 val (Form f, tac, asms) = ME_Misc.pt_extract (pt, ip);
7.310 (*exception just above means: 'ModSpec' has been returned: error anyway*)
7.311 if UnparseC.term f = "[x = 1]" then () else
7.312 @@ -419,43 +419,43 @@
7.313 ["Test", "squ-equ-test-subpbl1"]))];
7.314 Iterator 1;
7.315 moveActiveRoot 1;
7.316 - autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);
7.317 - autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);
7.318 - autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);
7.319 - autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);
7.320 - autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);
7.321 - autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);
7.322 - autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);
7.323 - autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);
7.324 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
7.325 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
7.326 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
7.327 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
7.328 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
7.329 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
7.330 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
7.331 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
7.332 (*here the solve-phase starts*)
7.333 - autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);
7.334 - autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);
7.335 - autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);
7.336 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
7.337 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
7.338 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
7.339 (*------------------------------------*)
7.340 -(* (*default_print_depth 13*) get_calc 1;
7.341 +(* (*default_print_depth 13*) States.get_calc 1;
7.342 *)
7.343 - autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);
7.344 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
7.345 (*calc-head of subproblem*)
7.346 - autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);
7.347 - autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);
7.348 - autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);
7.349 - autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);
7.350 - autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);
7.351 - autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);
7.352 - autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);
7.353 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
7.354 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
7.355 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
7.356 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
7.357 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
7.358 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
7.359 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
7.360 (*solve-phase of the subproblem*)
7.361 - autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);
7.362 - autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);
7.363 - autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);
7.364 - autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);
7.365 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
7.366 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
7.367 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
7.368 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
7.369 (*finish subproblem*)
7.370 - autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);
7.371 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
7.372 (*finish problem*)
7.373 - autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);
7.374 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
7.375
7.376 (*this checks the test for correctness..*)
7.377 - val ((pt,_),_) = get_calc 1;
7.378 - val p = get_pos 1 1;
7.379 + val ((pt,_),_) = States.get_calc 1;
7.380 + val p = States.get_pos 1 1;
7.381 val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
7.382 if UnparseC.term f = "[x = 1]" andalso p = ([], Res) then () else
7.383 error "FE-interface.sml: diff.behav. in miniscript with mini-subpb";
7.384 @@ -479,8 +479,8 @@
7.385 val (unc, del, gen) = (([],Pbl), ([],Pbl), ([],Res));
7.386 getFormulaeFromTo 1 unc gen 1 (*only level 1*) false;
7.387
7.388 - val ((pt,_),_) = get_calc 1;
7.389 - val p = get_pos 1 1;
7.390 + val ((pt,_),_) = States.get_calc 1;
7.391 + val p = States.get_pos 1 1;
7.392 val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
7.393 if UnparseC.term f = "[x = 1]" andalso p = ([], Res) then () else
7.394 error "FE-interface.sml: diff.behav. in solve_linear/rt AUTOCALCULATE ";
7.395 @@ -499,11 +499,11 @@
7.396 moveActiveRoot 1;
7.397
7.398 autoCalculate 1 CompleteCalcHead;
7.399 - refFormula 1 (get_pos 1 1);
7.400 - val ((pt,p),_) = get_calc 1;
7.401 + refFormula 1 (States.get_pos 1 1);
7.402 + val ((pt,p),_) = States.get_calc 1;
7.403
7.404 autoCalculate 1 CompleteCalc;
7.405 - val ((pt,p),_) = get_calc 1;
7.406 + val ((pt,p),_) = States.get_calc 1;
7.407 if p=([], Res) then () else
7.408 error "FE-interface.sml: diff.behav. in solve_linear AUTOC Head/Eval ";
7.409 DEconstrCalcTree 1;
7.410 @@ -518,7 +518,7 @@
7.411 Iterator 1;
7.412 moveActiveRoot 1;
7.413 autoCalculate 1 CompleteCalc;
7.414 - val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
7.415 + val ((pt,p),_) = States.get_calc 1; Test_Tool.show_pt pt;
7.416 (*
7.417 getTactic 1 ([1],Frm);
7.418 getTactic 1 ([1],Res);
7.419 @@ -530,8 +530,8 @@
7.420 getFormulaeFromTo 1 unc gen 1 (*only level 1*) false;
7.421 getFormulaeFromTo 1 unc gen 99999 (*all levels*) false;
7.422
7.423 - val ((pt,_),_) = get_calc 1;
7.424 - val p = get_pos 1 1;
7.425 + val ((pt,_),_) = States.get_calc 1;
7.426 + val p = States.get_pos 1 1;
7.427 val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
7.428 if UnparseC.term f = "[x = 1]" andalso p = ([], Res) then () else
7.429 error "FE-interface.sml: diff.behav. in mini-subpbl AUTOCALCULATE 6";
7.430 @@ -552,7 +552,7 @@
7.431 spec = ("Test", ["sqroot-test", "univariate", "equation", "test"],
7.432 ["Test", "squ-equ-test-subpbl1"]),
7.433 branch = TransitiveB, ostate = Incomplete (*!?\<forall>*), ...}, []),
7.434 - ([], Met)), []) = get_calc 1;
7.435 + ([], Met)), []) = States.get_calc 1;
7.436 if length meth = 3 andalso length probl = 3 (*just some items tested*) then ()
7.437 else error "--- mini-subpbl AUTO CompleteCalcHead ---";
7.438 DEconstrCalcTree 1;
7.439 @@ -560,7 +560,7 @@
7.440 "--------- solve_linear as rootpbl AUTO CompleteModel ---";
7.441 "--------- solve_linear as rootpbl AUTO CompleteModel ---";
7.442 "--------- solve_linear as rootpbl AUTO CompleteModel ---";
7.443 -reset_states ();
7.444 +States.reset ();
7.445 CalcTree
7.446 [(["equality (1+- 1*2+x=(0::real))", "solveFor x", "solutions L"],
7.447 ("Test",
7.448 @@ -569,31 +569,31 @@
7.449 Iterator 1;
7.450 moveActiveRoot 1;
7.451 autoCalculate 1 CompleteModel;
7.452 - refFormula 1 (get_pos 1 1);
7.453 + refFormula 1 (States.get_pos 1 1);
7.454
7.455 setProblem 1 ["LINEAR", "univariate", "equation", "test"];
7.456 -val pos = get_pos 1 1;
7.457 +val pos = States.get_pos 1 1;
7.458 (*setContext 1 pos (Ptool.kestoreID2guh Ptool.Pbl_["LINEAR", "univariate", "equation", "test"]);*)
7.459 - refFormula 1 (get_pos 1 1);
7.460 + refFormula 1 (States.get_pos 1 1);
7.461
7.462 setMethod 1 ["Test", "solve_linear"];
7.463 (*setContext 1 pos (Ptool.kestoreID2guh Ptool.Met_ ["Test", "solve_linear"]);*)
7.464 - refFormula 1 (get_pos 1 1);
7.465 - val ((pt,_),_) = get_calc 1;
7.466 + refFormula 1 (States.get_pos 1 1);
7.467 + val ((pt,_),_) = States.get_calc 1;
7.468 if get_obj g_spec pt [] = (ThyC.id_empty,
7.469 ["LINEAR", "univariate", "equation", "test"],
7.470 ["Test", "solve_linear"]) then ()
7.471 else error "FE-interface.sml: diff.behav. in setProblem, setMethod";
7.472
7.473 autoCalculate 1 CompleteCalcHead;
7.474 - refFormula 1 (get_pos 1 1);
7.475 + refFormula 1 (States.get_pos 1 1);
7.476 autoCalculate 1 CompleteCalc;
7.477 moveActiveDown 1;
7.478 moveActiveDown 1;
7.479 moveActiveDown 1;
7.480 - refFormula 1 (get_pos 1 1);
7.481 - val ((pt,_),_) = get_calc 1;
7.482 - val p = get_pos 1 1;
7.483 + refFormula 1 (States.get_pos 1 1);
7.484 + val ((pt,_),_) = States.get_calc 1;
7.485 + val p = States.get_pos 1 1;
7.486 val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
7.487 if UnparseC.term f = "[x = 1]" andalso p = ([], Res) then () else
7.488 error "FE-interface.sml: diff.behav. in mini-subpbl AUTOCALCULATE 6";
7.489 @@ -602,32 +602,32 @@
7.490 "--------- setContext..Thy ------------------------------";
7.491 "--------- setContext..Thy ------------------------------";
7.492 "--------- setContext..Thy ------------------------------";
7.493 -reset_states ();
7.494 +States.reset ();
7.495 CalcTree [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
7.496 ("Test", ["sqroot-test", "univariate", "equation", "test"],
7.497 ["Test", "squ-equ-test-subpbl1"]))];
7.498 Iterator 1; moveActiveRoot 1;
7.499 autoCalculate 1 CompleteCalcHead;
7.500 autoCalculate 1 (Steps 1);
7.501 - val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt; (*2 lines, OK*)
7.502 + val ((pt,p),_) = States.get_calc 1; Test_Tool.show_pt pt; (*2 lines, OK*)
7.503 (*
7.504 setNextTactic 1 (Rewrite_Set "Test_simplify"); (*--> "thy_isac_Test-rls-Test_simplify"*)
7.505 autoCalculate 1 (Steps 1);
7.506 - val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
7.507 + val ((pt,p),_) = States.get_calc 1; Test_Tool.show_pt pt;
7.508 *)
7.509 "----- \<up> ^^ and vvvvv do the same -----";
7.510 (*setContext 1 p "thy_isac_Test-rls-Test_simplify";*)
7.511 - val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt; (*2 lines, OK*)
7.512 + val ((pt,p),_) = States.get_calc 1; Test_Tool.show_pt pt; (*2 lines, OK*)
7.513
7.514 autoCalculate 1 (Steps 1);
7.515 (*setContext 1 p "thy_isac_Test-rls-Test_simplify";*)
7.516 - val (((pt,_),_), p) = (get_calc 1, get_pos 1 1);
7.517 + val (((pt,_),_), p) = (States.get_calc 1, States.get_pos 1 1);
7.518 val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
7.519 if p = ([1], Res) andalso UnparseC.term (get_obj g_res pt (fst p)) = "x + 1 + - 1 * 2 = 0"
7.520 then () else error "--- setContext..Thy --- autoCalculate 1 (Steps 1) #1";
7.521
7.522 autoCalculate 1 CompleteCalc;
7.523 - val (((pt,_),_), p) = (get_calc 1, get_pos 1 1);
7.524 + val (((pt,_),_), p) = (States.get_calc 1, States.get_pos 1 1);
7.525 val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
7.526
7.527 if UnparseC.term f = "[x = 1]" andalso p = ([], Res) then ()
7.528 @@ -637,14 +637,14 @@
7.529 "--------- mini-subpbl AUTOCALC CompleteToSubpbl --------";
7.530 "--------- mini-subpbl AUTOCALC CompleteToSubpbl --------";
7.531 "--------- mini-subpbl AUTOCALC CompleteToSubpbl --------";
7.532 -reset_states ();
7.533 +States.reset ();
7.534 CalcTree [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
7.535 ("Test", ["sqroot-test", "univariate", "equation", "test"],
7.536 ["Test", "squ-equ-test-subpbl1"]))];
7.537 Iterator 1; moveActiveRoot 1;
7.538 autoCalculate 1 CompleteToSubpbl;
7.539 - refFormula 1 (get_pos 1 1); (*<ISA> - 1 + x = 0 </ISA>*);
7.540 - val ((pt,_),_) = get_calc 1;
7.541 + refFormula 1 (States.get_pos 1 1); (*<ISA> - 1 + x = 0 </ISA>*);
7.542 + val ((pt,_),_) = States.get_calc 1;
7.543 val str = pr_ctree pr_short pt;
7.544 writeln str;
7.545 if str = ". ----- pblobj -----\n1. x + 1 = 2\n2. x + 1 + - 1 * 2 = 0\n"
7.546 @@ -653,12 +653,12 @@
7.547
7.548 autoCalculate 1 (Steps 1); (*proceeds only, if NOT 1 step before subplb*)
7.549 autoCalculate 1 CompleteToSubpbl;
7.550 - val ((pt,_),_) = get_calc 1;
7.551 + val ((pt,_),_) = States.get_calc 1;
7.552 val str = pr_ctree pr_short pt;
7.553 writeln str;
7.554 autoCalculate 1 CompleteCalc; (*das geht ohnehin !*);
7.555 - val ((pt,_),_) = get_calc 1;
7.556 - val p = get_pos 1 1;
7.557 + val ((pt,_),_) = States.get_calc 1;
7.558 + val p = States.get_pos 1 1;
7.559
7.560 val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
7.561 if UnparseC.term f = "[x = 1]" andalso p = ([], Res) then () else
7.562 @@ -747,9 +747,9 @@
7.563 "univariate", "equation"]);
7.564 autoCalculate 1 (Steps 1); fetchProposedTactic 1;
7.565 setNextTactic 1 (Check_Postcond ["rational", "univariate", "equation"]);
7.566 - val (ptp,_) = get_calc 1;
7.567 + val (ptp,_) = States.get_calc 1;
7.568 val (Form t,_,_) = ME_Misc.pt_extract ptp;
7.569 - if get_pos 1 1 = ([], Res) andalso UnparseC.term t = "[x = -4 / 3]" then ()
7.570 + if States.get_pos 1 1 = ([], Res) andalso UnparseC.term t = "[x = -4 / 3]" then ()
7.571 else writeln "FE-inteface.sml: diff.behav. in rat-eq + subpbl: no_met, NO ..";
7.572 DEconstrCalcTree 1;
7.573
7.574 @@ -761,7 +761,7 @@
7.575 * Automatically}\label{SPECIFY:refine-auto}\\} test match and refine with
7.576 * x \<up>2 + 4*x + 5 = 2
7.577 see isac.bridge.TestSpecify#testMatchRefine*)
7.578 -reset_states ();
7.579 +States.reset ();
7.580 CalcTree
7.581 [(["equality (x \<up> 2 + 4*x + 5 = (2::real))", "solveFor x", "solutions L"],
7.582 ("Isac_Knowledge",
7.583 @@ -845,9 +845,9 @@
7.584
7.585 autoCalculate 1 CompleteCalc;
7.586
7.587 - val ((pt,_),_) = get_calc 1;
7.588 + val ((pt,_),_) = States.get_calc 1;
7.589 Test_Tool.show_pt pt;
7.590 - val p = get_pos 1 1;
7.591 + val p = States.get_pos 1 1;
7.592 val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
7.593 if UnparseC.term f = "[x = - 1, x = -3]" andalso p = ([], Res) then () else
7.594 error "FE-interface.sml: diff.behav. in tryMatchProblem, tryRefine";
7.595 @@ -867,10 +867,10 @@
7.596 "--------- now the calc-header is ready for enter 'solving' ----";
7.597 autoCalculate 1 CompleteCalc;
7.598
7.599 - val ((pt,_),_) = get_calc 1;
7.600 + val ((pt,_),_) = States.get_calc 1;
7.601 rootthy pt;
7.602 Test_Tool.show_pt pt;
7.603 - val p = get_pos 1 1;
7.604 + val p = States.get_pos 1 1;
7.605 val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
7.606 if UnparseC.term f = "[x = - 1, x = -3]" andalso p = ([], Res) then () else
7.607 error "FE-interface.sml: diff.behav. in tryMatchProblem, tryRefine";
7.608 @@ -880,7 +880,7 @@
7.609 "--------- modifyCalcHead, resetCalcHead, modelProblem --";
7.610 "--------- modifyCalcHead, resetCalcHead, modelProblem --";
7.611 "--------- modifyCalcHead, resetCalcHead, modelProblem --";
7.612 -reset_states ();
7.613 +States.reset ();
7.614 CalcTree [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
7.615 ("Test", ["sqroot-test", "univariate", "equation", "test"],
7.616 ["Test", "squ-equ-test-subpbl1"]))];
7.617 @@ -910,7 +910,7 @@
7.618 result},
7.619 []),
7.620 ([], Pbl)),
7.621 - []) = get_calc 1;
7.622 + []) = States.get_calc 1;
7.623 (*WN110622: is the same as in 2002, but shouldn't be probl = [3 items?]*)
7.624 if length meth = 0 andalso length probl = 0 (*just some items tested*) then ()
7.625 else error "--- modifyCalcHead, resetCalcHead, modelProblem 1 --";
7.626 @@ -918,7 +918,7 @@
7.627 resetCalcHead 1;
7.628 modelProblem 1;
7.629
7.630 -get_calc 1;
7.631 +States.get_calc 1;
7.632 val ((Nd (PblObj {fmz = (fm, tpm),
7.633 loc = (SOME scrst_ctxt, NONE),
7.634 ctxt,
7.635 @@ -931,7 +931,7 @@
7.636 result},
7.637 []),
7.638 ([], Pbl)),
7.639 - []) = get_calc 1;
7.640 + []) = States.get_calc 1;
7.641 if length meth = 3 andalso length probl = 3 (*just some items tested*) then ()
7.642 else error "--- modifyCalcHead, resetCalcHead, modelProblem 2 --";
7.643
7.644 @@ -966,13 +966,13 @@
7.645 CalcTree [(elems, spec)];
7.646 Iterator 1;
7.647 moveActiveRoot 1;
7.648 - refFormula 1 (get_pos 1 1);
7.649 + refFormula 1 (States.get_pos 1 1);
7.650 (*this gives a completely empty model*)
7.651
7.652 fetchProposedTactic 1;
7.653 (*fill the CalcHead with Descriptions...*)
7.654 setNextTactic 1 (Model_Problem );
7.655 - autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);
7.656 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
7.657
7.658 (*user input is !!!!!EITHER!!!!! _some_ (at least one) items of the model
7.659 !!!!!OR!!!!! _one_ part of the specification !!!!!!!!!!!!!*)
7.660 @@ -992,7 +992,7 @@
7.661 fetchProposedTactic 1;
7.662 (*the student follows the advice*)
7.663 setNextTactic 1 (Add_Find "maximum A"); (*FIXME.17.11.03: does not yet work*)
7.664 - autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);
7.665 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
7.666
7.667 (*this input completes the model*)
7.668 modifyCalcHead 1 (([],Pbl), "not used here",
7.669 @@ -1029,11 +1029,11 @@
7.670 "--------- solve_linear from pbl-hierarchy --------------";
7.671 "--------- solve_linear from pbl-hierarchy --------------";
7.672 "--------- solve_linear from pbl-hierarchy --------------";
7.673 -reset_states ();
7.674 +States.reset ();
7.675 val (fmz, sp) = ([], ("", ["LINEAR", "univariate", "equation", "test"], []));
7.676 CalcTree [(fmz, sp)];
7.677 Iterator 1; moveActiveRoot 1;
7.678 - refFormula 1 (get_pos 1 1);
7.679 + refFormula 1 (States.get_pos 1 1);
7.680 modifyCalcHead 1 (([],Pbl),"solve (1+- 1*2+x=(0::real))",
7.681 [P_Spec.Given ["equality (1+- 1*2+x=(0::real))", "solveFor x"],
7.682 P_Spec.Find ["solutions L"]],
7.683 @@ -1041,9 +1041,9 @@
7.684 ("Test", ["LINEAR", "univariate", "equation", "test"],
7.685 ["Test", "solve_linear"]));
7.686 autoCalculate 1 CompleteCalc;
7.687 - refFormula 1 (get_pos 1 1);
7.688 - val ((pt,_),_) = get_calc 1;
7.689 - val p = get_pos 1 1;
7.690 + refFormula 1 (States.get_pos 1 1);
7.691 + val ((pt,_),_) = States.get_calc 1;
7.692 + val p = States.get_pos 1 1;
7.693 val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
7.694 if UnparseC.term f = "[x = 1]" andalso p = ([], Res) andalso map UnparseC.term asms = [] then ()
7.695 else error "FE-interface.sml: diff.behav. in from pbl -hierarchy 1";
7.696 @@ -1053,15 +1053,15 @@
7.697 "--------- solve_linear as in an algebra system (CAS)----";
7.698 "--------- solve_linear as in an algebra system (CAS)----";
7.699 (*WN120210?not ME:\label{UC:cas-input} UC 30.1.2.5 p.168*)
7.700 -reset_states ();
7.701 +States.reset ();
7.702 val (fmz, sp) = ([], ("", [], []));
7.703 CalcTree [(fmz, sp)];
7.704 Iterator 1; moveActiveRoot 1;
7.705 modifyCalcHead 1 (([],Pbl),"solveTest (1+- 1*2+x=0,x)", [], Pbl, ("", [], []));
7.706 autoCalculate 1 CompleteCalc;
7.707 - refFormula 1 (get_pos 1 1);
7.708 - val ((pt,_),_) = get_calc 1;
7.709 - val p = get_pos 1 1;
7.710 + refFormula 1 (States.get_pos 1 1);
7.711 + val ((pt,_),_) = States.get_calc 1;
7.712 + val p = States.get_pos 1 1;
7.713 val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
7.714 if UnparseC.term f = "[x = 1]" andalso p = ([], Res) andalso map UnparseC.term asms = [] then ()
7.715 else error "FE-interface.sml: diff.behav. in from pbl -hierarchy 2";
7.716 @@ -1076,18 +1076,18 @@
7.717 Iterator 1;
7.718 moveActiveRoot 1;
7.719 autoCalculate 1 CompleteCalc;
7.720 - val ((pt,_),_) = get_calc 1;
7.721 + val ((pt,_),_) = States.get_calc 1;
7.722 Test_Tool.show_pt pt;
7.723
7.724 (*UC\label{UC:inter-steps} UC 30.3.5.5 p.178*)
7.725 interSteps 1 ([2],Res);
7.726 - val ((pt,_),_) = get_calc 1; Test_Tool.show_pt pt (*new ([2,1],Frm)..([2,6],Res)*);
7.727 + val ((pt,_),_) = States.get_calc 1; Test_Tool.show_pt pt (*new ([2,1],Frm)..([2,6],Res)*);
7.728 val (unc, del, gen) = (([1],Res),([1],Res),([2,6],Res));
7.729 getFormulaeFromTo 1 unc gen 1 false;
7.730
7.731 (*UC\label{UC:inter-steps} UC 30.3.5.5 p.178*)
7.732 interSteps 1 ([3,2],Res);
7.733 - val ((pt,_),_) = get_calc 1; Test_Tool.show_pt pt (*new ([3,2,1],Frm)..([3,2,2],Res)*);
7.734 + val ((pt,_),_) = States.get_calc 1; Test_Tool.show_pt pt (*new ([3,2,1],Frm)..([3,2,2],Res)*);
7.735 val (unc, del, gen) = (([3,1],Res),([3,1],Res),([3,2,2],Res));
7.736 getFormulaeFromTo 1 unc gen 1 false;
7.737
7.738 @@ -1113,7 +1113,7 @@
7.739 ["Test", "squ-equ-test-subpbl1"]))];
7.740 Iterator 1; moveActiveRoot 1;
7.741 autoCalculate 1 CompleteCalc;
7.742 - val ((pt,_),_) = get_calc 1;
7.743 + val ((pt,_),_) = States.get_calc 1;
7.744 Test_Tool.show_pt pt;
7.745
7.746 (*UC\label{SOLVE:HIDE:getTactic} \label{SOLVE:AUTO:tactic} UC 30.3.3.1 p.176
7.747 @@ -1138,15 +1138,15 @@
7.748 "--------- getAssumptions, getAccumulatedAsms -----------";
7.749 "--------- getAssumptions, getAccumulatedAsms -----------";
7.750 "--------- getAssumptions, getAccumulatedAsms -----------";
7.751 -reset_states ();
7.752 +States.reset ();
7.753 CalcTree
7.754 [(["equality (x/(x \<up> 2 - 6*x+9) - 1/(x \<up> 2 - 3*x) =1/x)",
7.755 "solveFor x", "solutions L"],
7.756 ("RatEq",["univariate", "equation"],["no_met"]))];
7.757 Iterator 1; moveActiveRoot 1;
7.758 autoCalculate 1 CompleteCalc;
7.759 -val ((pt,_),_) = get_calc 1;
7.760 -val p = get_pos 1 1;
7.761 +val ((pt,_),_) = States.get_calc 1;
7.762 +val p = States.get_pos 1 1;
7.763 val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
7.764 (*============ inhibit exn WN120316 compare 2002-- 2011 ===========================
7.765 if map UnparseC.term asms =
7.766 @@ -1184,7 +1184,7 @@
7.767 Iterator 1; moveActiveRoot 1;
7.768
7.769 fetchProposedTactic 1;
7.770 - (*ERROR get_calc 1 not existent*)
7.771 + (*ERROR States.get_calc 1 not existent*)
7.772 setNextTactic 1 (Model_Problem );
7.773 autoCalculate 1 (Steps 1);
7.774 fetchProposedTactic 1;
7.775 @@ -1215,8 +1215,8 @@
7.776 autoCalculate 1 (Steps 1);
7.777
7.778 autoCalculate 1 CompleteCalc;
7.779 - val ((pt,_),_) = get_calc 1;
7.780 - val p = get_pos 1 1;
7.781 + val ((pt,_),_) = States.get_calc 1;
7.782 + val p = States.get_pos 1 1;
7.783 val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
7.784 if UnparseC.term f = "[x = 1]" andalso p = ([], Res) then () else
7.785 error "FE-interface.sml: diff.behav. in combinations of steps";
7.786 @@ -1238,8 +1238,8 @@
7.787 val (unc, del, gen) = (([1],Res), ([1],Res), ([2],Res));
7.788 getFormulaeFromTo 1 unc gen 99999 (*all levels*) false;
7.789
7.790 - val ((pt,_),_) = get_calc 1;
7.791 - val p = get_pos 1 1;
7.792 + val ((pt,_),_) = States.get_calc 1;
7.793 + val p = States.get_pos 1 1;
7.794 val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
7.795 if UnparseC.term f = "- 1 + x = 0" andalso p = ([2], Res) then () else
7.796 error "FE-interface.sml: diff.behav. in FORMULA:enter} right";
7.797 @@ -1261,8 +1261,8 @@
7.798 getFormulaeFromTo 1 unc gen 99999 (*all levels*) false;
7.799 (*11 elements !!!*)
7.800
7.801 - val ((pt,_),_) = get_calc 1;
7.802 - val p = get_pos 1 1;
7.803 + val ((pt,_),_) = States.get_calc 1;
7.804 + val p = States.get_pos 1 1;
7.805 val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
7.806 if UnparseC.term f = "x - 1 = 0" andalso p = ([2], Res) then () else
7.807 error "FE-interface.sml: diff.behav. in FORMULA:enter} other";
7.808 @@ -1285,8 +1285,8 @@
7.809 getFormulaeFromTo 1 unc gen 99999 (*all levels*) false;
7.810 (*6 elements !!!*)
7.811
7.812 - val ((pt,_),_) = get_calc 1;
7.813 - val p = get_pos 1 1;
7.814 + val ((pt,_),_) = States.get_calc 1;
7.815 + val p = States.get_pos 1 1;
7.816 val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
7.817 if UnparseC.term f = "x = 1" andalso p = ([3,2], Res) then () else
7.818 error "FE-interface.sml: diff.behav. in FORMULA:enter} oth 2";
7.819 @@ -1306,8 +1306,8 @@
7.820 appendFormula 1 "x - 4711 = 0" (*|> Future.join*);
7.821 (*... returns <ERROR> no derivation found </ERROR>*)
7.822
7.823 - val ((pt,_),_) = get_calc 1;
7.824 - val p = get_pos 1 1;
7.825 + val ((pt,_),_) = States.get_calc 1;
7.826 + val p = States.get_pos 1 1;
7.827 val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
7.828 if UnparseC.term f = "x + 1 + - 1 * 2 = 0" andalso p = ([1], Res) then () else
7.829 error "FE-interface.sml: diff.behav. in FORMULA:enter} NOTok";
7.830 @@ -1327,8 +1327,8 @@
7.831 replaceFormula 1 "- 1 + x = 0" (*i.e. repeats input*);
7.832 (*... returns <ERROR> formula not changed </ERROR>*)
7.833
7.834 - val ((pt,_),_) = get_calc 1;
7.835 - val p = get_pos 1 1;
7.836 + val ((pt,_),_) = States.get_calc 1;
7.837 + val p = States.get_pos 1 1;
7.838 val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
7.839 if UnparseC.term f = "- 1 + x = 0" andalso p = ([2], Res) then () else
7.840 error "FE-interface.sml: diff.behav. in FORMULA:replace} right 1";
7.841 @@ -1341,15 +1341,15 @@
7.842 CalcTree [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
7.843 ("Test", ["sqroot-test", "univariate", "equation", "test"],
7.844 ["Test", "squ-equ-test-subpbl1"]))];
7.845 - Iterator 2; (*! ! ! 1 CalcTree inbetween reset_states (); *)
7.846 + Iterator 2; (*! ! ! 1 CalcTree inbetween States.reset (); *)
7.847 moveActiveRoot 2;
7.848 autoCalculate 2 CompleteCalc;
7.849 moveActiveFormula 2 ([2],Res);
7.850 replaceFormula 2 "- 1 + x = 0" (*i.e. repeats input*);
7.851 (*... returns <ERROR> formula not changed </ERROR>*)
7.852
7.853 - val ((pt,_),_) = get_calc 2;
7.854 - val p = get_pos 2 1;
7.855 + val ((pt,_),_) = States.get_calc 2;
7.856 + val p = States.get_pos 2 1;
7.857 val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
7.858 if UnparseC.term f = "- 1 + x = 0" andalso p = ([2], Res) then () else
7.859 error "FE-interface.sml: diff.behav. in FORMULA:replace} right 1";
7.860 @@ -1375,9 +1375,9 @@
7.861 val (unc, del, gen) = (([1],Res), ([4],Res), ([2],Res));
7.862 getFormulaeFromTo 1 unc gen 99999 (*all levels*) false;
7.863
7.864 - val ((pt,_),_) = get_calc 1;
7.865 + val ((pt,_),_) = States.get_calc 1;
7.866 Test_Tool.show_pt pt;
7.867 - val p = get_pos 1 1;
7.868 + val p = States.get_pos 1 1;
7.869 val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
7.870 if UnparseC.term f = "x - 1 = 0" andalso p = ([2], Res) then () else
7.871 error "FE-interface.sml: diff.behav. in FORMULA:replace} other 1";
7.872 @@ -1408,7 +1408,7 @@
7.873 getFormulaeFromTo 1 unc gen 99999 (*all levels*) false;
7.874 (*9 elements !!!*)
7.875
7.876 - val ((pt,_),_) = get_calc 1;
7.877 + val ((pt,_),_) = States.get_calc 1;
7.878 Test_Tool.show_pt pt; (*error: ...ME_Misc.get_interval drops ([3,2],Res) ...*)
7.879 val (t,_) = get_obj g_result pt [3,2]; UnparseC.term t;
7.880 if map fst3 (ME_Misc.get_interval ([1],Res) ([],Res) 9999 pt) =
7.881 @@ -1417,7 +1417,7 @@
7.882 ([3,2],Res)] then () else
7.883 error "FE-interface.sml: diff.behav. in FORMULA:replace} oth2 1";
7.884
7.885 - val p = get_pos 1 1;
7.886 + val p = States.get_pos 1 1;
7.887 val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
7.888 if UnparseC.term f = "x = 1" andalso p = ([3,2], Res) then () else
7.889 error "FE-interface.sml: diff.behav. in FORMULA:replace} oth2 2";
7.890 @@ -1437,9 +1437,9 @@
7.891 replaceFormula 1 "x - 4711 = 0";
7.892 (*... returns <ERROR> no derivation found </ERROR>*)
7.893
7.894 - val ((pt,_),_) = get_calc 1;
7.895 + val ((pt,_),_) = States.get_calc 1;
7.896 Test_Tool.show_pt pt;
7.897 - val p = get_pos 1 1;
7.898 + val p = States.get_pos 1 1;
7.899 val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
7.900 if UnparseC.term f = "- 1 + x = 0" andalso p = ([2], Res) then () else
7.901 error "FE-interface.sml: diff.behav. in FORMULA:replace} NOTok";
7.902 @@ -1461,8 +1461,8 @@
7.903 would recognize "cos (4 * x \<up> (4 - 1)) + 2 * x" as well.
7.904 results in <CALCMESSAGE> error pattern #chain-rule-diff-both# </CALCMESSAGE>
7.905 instead of <CALCMESSAGE> no derivation found </CALCMESSAGE> *)
7.906 - val ((pt,pos), _) = get_calc 1;
7.907 - val p = get_pos 1 1;
7.908 + val ((pt,pos), _) = States.get_calc 1;
7.909 + val p = States.get_pos 1 1;
7.910 val (Form f, _, asms) = ME_Misc.pt_extract (pt, p);
7.911
7.912 if p = ([1], Res) andalso UnparseC.term f = "d_d x (x \<up> 2) + d_d x (sin (x \<up> 4))"
7.913 @@ -1475,8 +1475,8 @@
7.914 findFillpatterns 1 "chain-rule-diff-both"; (*<<<<<<<=================================*)
7.915 (*<CALCMESSAGE> fill patterns #fill-d_d-arg#d_d x (x \<up> 2) + d_d x (sin (x \<up> 4)) =
7.916 d_d x (x \<up> 2) + cos (x \<up> 4) * d_d x ?_dummy_1#fill-both-args#...#...#... *)
7.917 - val ((pt,pos),_) = get_calc 1;
7.918 - val p = get_pos 1 1;
7.919 + val ((pt,pos),_) = States.get_calc 1;
7.920 + val p = States.get_pos 1 1;
7.921
7.922 val (Form f, _, asms) = ME_Misc.pt_extract (pt, p);
7.923 if p = ([1], Res) andalso UnparseC.term f = "d_d x (x \<up> 2) + d_d x (sin (x \<up> 4))" andalso
7.924 @@ -1489,8 +1489,8 @@
7.925 for the DialogGuide to select appropriately. *)
7.926 requestFillformula 1 ("chain-rule-diff-both", "fill-both-args");(*<<<<<<<============*)
7.927 (*<AUTOCALC> ([1], Res) ([2], Res) ([2], Res) </AUTOCALC>*)
7.928 - val ((pt,pos),_) = get_calc 1;
7.929 - val p = get_pos 1 1;
7.930 + val ((pt,pos),_) = States.get_calc 1;
7.931 + val p = States.get_pos 1 1;
7.932 val (Form f, _, asms) = ME_Misc.pt_extract (pt, p);
7.933 if p = ([1], Res) andalso existpt [2] pt andalso
7.934 UnparseC.term f = "d_d x (x \<up> 2) + d_d x (sin (x \<up>\<up> 4))" andalso
7.935 @@ -1498,8 +1498,8 @@
7.936 then () else error "embed fun fill_form changed 3";
7.937
7.938 inputFillFormula 1 "d_d x (x \<up> 2) + cos (x \<up> 4) * d_d x (x \<up> 4)";(*<<<<<<<=====*)
7.939 - val ((pt, _),_) = get_calc 1;
7.940 - val p = get_pos 1 1;
7.941 + val ((pt, _),_) = States.get_calc 1;
7.942 + val p = States.get_pos 1 1;
7.943 val (Form f, _, asms) = ME_Misc.pt_extract (pt, p);
7.944 if p = ([2], Res) andalso
7.945 UnparseC.term f = "d_d x (x \<up> 2) + cos (x \<up> 4) * d_d x (x \<up> 4)" andalso
7.946 @@ -1509,8 +1509,8 @@
7.947 autoCalculate 1 CompleteCalc;
7.948
7.949 "~~~~~ final check: the input formula is inserted as it would have been correct from beginning";
7.950 -val ((pt, _),_) = get_calc 1;
7.951 -val p = get_pos 1 1;
7.952 +val ((pt, _),_) = States.get_calc 1;
7.953 +val p = States.get_pos 1 1;
7.954 val (Form f, _, asms) = ME_Misc.pt_extract (pt, p);
7.955 if p = ([], Res) andalso UnparseC.term f = "2 * x + cos (x \<up> 4) * 4 * x \<up> 3"
7.956 then () else error "inputFillFormula changed 12";
7.957 @@ -1556,7 +1556,7 @@
7.958 Iterator 1;
7.959 moveActiveRoot 1;
7.960 autoCalculate 1 CompleteCalc;
7.961 -val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
7.962 +val ((pt,p),_) = States.get_calc 1; Test_Tool.show_pt pt;
7.963 DEconstrCalcTree 1;
7.964
7.965 "--------- UC errpat, fillpat step to Rewrite_Set ----------------";
7.966 @@ -1607,7 +1607,7 @@
7.967 (* then --- UC errpat, fillpat by input ---*)
7.968 *)
7.969 autoCalculate 1 CompleteCalc;
7.970 -val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
7.971 +val ((pt,p),_) = States.get_calc 1; Test_Tool.show_pt pt;
7.972 (*WN1208 postponed due to efforts required for stepToErrorPatterns (NEW rewrite_set_)*)
7.973 DEconstrCalcTree 1;
7.974
8.1 --- a/test/Tools/isac/Interpret/error-pattern.sml Fri Sep 09 10:53:51 2022 +0200
8.2 +++ b/test/Tools/isac/Interpret/error-pattern.sml Sun Sep 11 14:31:15 2022 +0200
8.3 @@ -52,17 +52,17 @@
8.4 val Prog sc = (#scr o MethodC.from_store) ["Test", "solve_linear"];
8.5 (writeln o UnparseC.term) sc;
8.6
8.7 - reset_states ();
8.8 + States.reset ();
8.9 CalcTree [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
8.10 ("Test", ["sqroot-test", "univariate", "equation", "test"],
8.11 ["Test", "squ-equ-test-subpbl1"]))];
8.12 Iterator 1; moveActiveRoot 1;
8.13 autoCalculate 1 CompleteCalcHead;
8.14 - autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);(*x + 1 = 2*)
8.15 - autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);(*x + 1 + - 1 * 2 = 0*);
8.16 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);(*x + 1 = 2*)
8.17 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);(*x + 1 + - 1 * 2 = 0*);
8.18
8.19 - appendFormula 1 "- 2 * 1 + (1 + x) = 0" (*|> Future.join*); refFormula 1 (get_pos 1 1);
8.20 - val ((pt,_),_) = get_calc 1;
8.21 + appendFormula 1 "- 2 * 1 + (1 + x) = 0" (*|> Future.join*); refFormula 1 (States.get_pos 1 1);
8.22 + val ((pt,_),_) = States.get_calc 1;
8.23 val str = pr_ctree pr_short pt;
8.24 if str =
8.25 (". ----- pblobj -----\n" ^
8.26 @@ -87,24 +87,24 @@
8.27 moveDown 1 ([2,3],Res); refFormula 1 ([2,4],Res);
8.28 moveDown 1 ([2,4],Res); refFormula 1 ([2,5],Res);
8.29 moveDown 1 ([2,5],Res); refFormula 1 ([2,6],Res);
8.30 - val ((pt,_),_) = get_calc 1;
8.31 + val ((pt,_),_) = States.get_calc 1;
8.32 if "- 2 * 1 + (1 + x) = 0" = UnparseC.term (fst (get_obj g_result pt [2,6])) then()
8.33 else error "inform.sml: diff.behav.appendFormula: on Res + equ 2";
8.34
8.35 fetchProposedTactic 1; (*takes Iterator 1 _1_*)
8.36 (* <ERROR> error in kernel </ERROR> ALREADY IN 2009-2*)
8.37 (*========== inhibit exn WN1130701 broken at Isabelle2002 --> 2009-2 =============
8.38 - val (_,(tac,_,_)::_) = get_calc 1;
8.39 + val (_,(tac,_,_)::_) = States.get_calc 1;
8.40 if tac = Rewrite_Set "Test_simplify" then ()
8.41 else error "inform.sml: diff.behav.appendFormula: on Res + equ 3";
8.42 ============ inhibit exn WN1130701 broken at Isabelle2002 --> 2009-2 ============*)
8.43
8.44 autoCalculate 1 CompleteCalc;
8.45 - val ((pt,_),_) = get_calc 1;
8.46 + val ((pt,_),_) = States.get_calc 1;
8.47 if "[x = 1]" = UnparseC.term (fst (get_obj g_result pt [])) then ()
8.48 else error "inform.sml: diff.behav.appendFormula: on Res + equ 4";
8.49 (* autoCalculate 1 CompleteCalc;
8.50 - val ((pt,p),_) = get_calc 1;
8.51 + val ((pt,p),_) = States.get_calc 1;
8.52 (writeln o istates2str) (get_obj g_loc pt [ ]);
8.53 (writeln o istates2str) (get_obj g_loc pt [1]);
8.54 (writeln o istates2str) (get_obj g_loc pt [2]);
8.55 @@ -137,14 +137,14 @@
8.56 "--------- appendFormula: on Frm + equ_nrls ----------------------";
8.57 "--------- appendFormula: on Frm + equ_nrls ----------------------";
8.58 "--------- appendFormula: on Frm + equ_nrls ----------------------";
8.59 - reset_states ();
8.60 + States.reset ();
8.61 CalcTree [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
8.62 ("Test", ["sqroot-test", "univariate", "equation", "test"],
8.63 ["Test", "squ-equ-test-subpbl1"]))];
8.64 Iterator 1; moveActiveRoot 1;
8.65 autoCalculate 1 CompleteCalcHead;
8.66 - autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1) (*x + 1 = 2*);
8.67 - appendFormula 1 "2+ - 1 + x = 2" (*|> Future.join*); refFormula 1 (get_pos 1 1);
8.68 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1) (*x + 1 = 2*);
8.69 + appendFormula 1 "2+ - 1 + x = 2" (*|> Future.join*); refFormula 1 (States.get_pos 1 1);
8.70
8.71 moveDown 1 ([],Pbl); refFormula 1 ([1],Frm) (*x + 1 = 2*);
8.72
8.73 @@ -155,16 +155,16 @@
8.74 moveDown 1 ([1,3],Res); refFormula 1 ([1,4],Res);
8.75 moveDown 1 ([1,4],Res); refFormula 1 ([1,5],Res);
8.76 moveDown 1 ([1,5],Res); refFormula 1 ([1,6],Res);
8.77 - val ((pt,_),_) = get_calc 1;
8.78 + val ((pt,_),_) = States.get_calc 1;
8.79 if "2 + - 1 + x = 2" = UnparseC.term (fst (get_obj g_result pt [1,6])) then()
8.80 else error "inform.sml: diff.behav.appendFormula: on Frm + equ 1";
8.81
8.82 fetchProposedTactic 1; (*takes Iterator 1 _1_*)
8.83 - val (_,(tac,_,_)::_) = get_calc 1;
8.84 + val (_,(tac,_,_)::_) = States.get_calc 1;
8.85 case tac of Rewrite_Set "norm_equation" => ()
8.86 | _ => error "inform.sml: diff.behav.appendFormula: on Frm + equ 2";
8.87 autoCalculate 1 CompleteCalc;
8.88 - val ((pt,_),_) = get_calc 1;
8.89 + val ((pt,_),_) = States.get_calc 1;
8.90 if "[x = 1]" = UnparseC.term (fst (get_obj g_result pt [])) then ()
8.91 else error "inform.sml: diff.behav.appendFormula: on Frm + equ 3";
8.92 DEconstrCalcTree 1;
8.93 @@ -172,17 +172,17 @@
8.94 "--------- appendFormula: on Res + NO deriv ----------------------";
8.95 "--------- appendFormula: on Res + NO deriv ----------------------";
8.96 "--------- appendFormula: on Res + NO deriv ----------------------";
8.97 - reset_states ();
8.98 + States.reset ();
8.99 CalcTree [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
8.100 ("Test", ["sqroot-test", "univariate", "equation", "test"],
8.101 ["Test", "squ-equ-test-subpbl1"]))];
8.102 Iterator 1; moveActiveRoot 1;
8.103 autoCalculate 1 CompleteCalcHead;
8.104 - autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);(*x + 1 = 2*)
8.105 - autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);(*x + 1 + - 1 * 2 = 0*);
8.106 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);(*x + 1 = 2*)
8.107 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);(*x + 1 + - 1 * 2 = 0*);
8.108
8.109 appendFormula 1 "x = 2" (*|> Future.join*);
8.110 - val ((pt,p),_) = get_calc 1;
8.111 + val ((pt,p),_) = States.get_calc 1;
8.112 val str = pr_ctree pr_short pt;
8.113 writeln str;
8.114 if str = ". ----- pblobj -----\n1. x + 1 = 2\n" andalso p = ([1], Res)
8.115 @@ -190,11 +190,11 @@
8.116 else error "inform.sml: diff.behav.appendFormula: Res + NOder 1";
8.117
8.118 fetchProposedTactic 1;
8.119 - val (_,(tac,_,_)::_) = get_calc 1;
8.120 + val (_,(tac,_,_)::_) = States.get_calc 1;
8.121 case tac of Rewrite_Set "Test_simplify" => ()
8.122 | _ => error "inform.sml: diff.behav.appendFormula: Res + NOder 2";
8.123 autoCalculate 1 CompleteCalc;
8.124 - val ((pt,_),_) = get_calc 1;
8.125 + val ((pt,_),_) = States.get_calc 1;
8.126 if "[x = 1]" = UnparseC.term (fst (get_obj g_result pt [])) then ()
8.127 else error "inform.sml: diff.behav.appendFormula: on Frm + equ 3";
8.128 DEconstrCalcTree 1;
8.129 @@ -205,17 +205,17 @@
8.130 (*cp with "fun me" to test/../lucas-interpreter.sml:
8.131 re-build: fun locate_input_term ---------------------------------------------------";
8.132 *)
8.133 - reset_states ();
8.134 + States.reset ();
8.135 CalcTree [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
8.136 ("Test", ["sqroot-test", "univariate", "equation", "test"],
8.137 ["Test", "squ-equ-test-subpbl1"]))];
8.138 Iterator 1; moveActiveRoot 1;
8.139 autoCalculate 1 CompleteCalcHead;
8.140 - autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);(*x + 1 = 2*)
8.141 - autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);(*x + 1 + - 1 * 2 = 0*);
8.142 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);(*x + 1 = 2*)
8.143 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);(*x + 1 + - 1 * 2 = 0*);
8.144
8.145 appendFormula 1 "x = 1" (*|> Future.join*);
8.146 - val ((pt,p),_) = get_calc 1;
8.147 + val ((pt,p),_) = States.get_calc 1;
8.148 val str = pr_ctree pr_short pt;
8.149 writeln str;
8.150 if str = ". ----- pblobj -----\n1. x + 1 = 2\n2. x + 1 + - 1 * 2 = 0\n3. ----- pblobj -----\n3.1. - 1 + x = 0\n3.2. x = 0 + - 1 * - 1\n3.2.1. x = 0 + - 1 * - 1\n3.2.2. x = 0 + 1\n" andalso p = ([3,2], Res)
8.151 @@ -223,11 +223,11 @@
8.152 else error "inform.sml: diff.behav.appendFormula: Res + late d 1";
8.153
8.154 fetchProposedTactic 1;
8.155 - val (_,(tac,_,_)::_) = get_calc 1;
8.156 + val (_,(tac,_,_)::_) = States.get_calc 1;
8.157 case tac of Check_Postcond ["LINEAR", "univariate", "equation", "test"] => ()
8.158 | _ => error "inform.sml: diff.behav.appendFormula: Res + late d 2";
8.159 autoCalculate 1 CompleteCalc;
8.160 - val ((pt,_),_) = get_calc 1;
8.161 + val ((pt,_),_) = States.get_calc 1;
8.162 if "[x = 1]" = UnparseC.term (fst (get_obj g_result pt [])) then ()
8.163 else error "inform.sml: diff.behav.appendFormula: Res + late d 3";
8.164 DEconstrCalcTree 1;
8.165 @@ -235,22 +235,22 @@
8.166 "--------- appendFormula: on Res + late deriv [x = 3 + - 2]---///--";
8.167 "--------- appendFormula: on Res + late deriv [x = 3 + - 2]---///--";
8.168 "--------- appendFormula: on Res + late deriv [x = 3 + - 2]---///--";
8.169 - reset_states ();
8.170 + States.reset ();
8.171 CalcTree [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
8.172 ("Test", ["sqroot-test", "univariate", "equation", "test"],
8.173 ["Test", "squ-equ-test-subpbl1"]))];
8.174 Iterator 1; moveActiveRoot 1;
8.175 autoCalculate 1 CompleteCalcHead;
8.176 - autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);(*x + 1 = 2*)
8.177 - autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);(*x + 1 + - 1 * 2 = 0*);
8.178 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);(*x + 1 = 2*)
8.179 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);(*x + 1 + - 1 * 2 = 0*);
8.180 appendFormula 1 "[x = 3 + -2*1]" (*|> Future.join*);
8.181 - val ((pt,p),_) = get_calc 1;
8.182 + val ((pt,p),_) = States.get_calc 1;
8.183 val str = pr_ctree pr_short pt;
8.184 writeln str;
8.185 if str=". ----- pblobj -----\n1. x + 1 = 2\n2. x + 1 + - 1 * 2 = 0\n3. ----- pblobj -----\n3.1. - 1 + x = 0\n3.2. x = 0 + - 1 * - 1\n4. [x = 1]\n4.1. [x = 1]\n4.2. [x = - 2 + 3]\n4.3. [x = 3 + - 2]\n" then ()
8.186 else error "inform.sml: diff.behav.appendFormula: Res + latEE 1";
8.187 autoCalculate 1 CompleteCalc;
8.188 - val ((pt,p),_) = get_calc 1;
8.189 + val ((pt,p),_) = States.get_calc 1;
8.190 if "[x = 3 + - 2 * 1]" = UnparseC.term (fst (get_obj g_result pt [])) then ()
8.191 (* ~~~~~~~~~~ simplify as last step in any script ?!*)
8.192 else error "inform.sml: diff.behav.appendFormula: Res + latEE 2";
8.193 @@ -259,18 +259,18 @@
8.194 "--------- replaceFormula: on Res + = ----------------------------";
8.195 "--------- replaceFormula: on Res + = ----------------------------";
8.196 "--------- replaceFormula: on Res + = ----------------------------";
8.197 - reset_states ();
8.198 + States.reset ();
8.199 CalcTree [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
8.200 ("Test", ["sqroot-test", "univariate", "equation", "test"],
8.201 ["Test", "squ-equ-test-subpbl1"]))];
8.202 Iterator 1; moveActiveRoot 1;
8.203 autoCalculate 1 CompleteCalcHead;
8.204 - autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);(*x + 1 = 2*)
8.205 - autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);(*x + 1 + - 1 * 2 = 0*);
8.206 - autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);(*- 1 + x*);
8.207 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);(*x + 1 = 2*)
8.208 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);(*x + 1 + - 1 * 2 = 0*);
8.209 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);(*- 1 + x*);
8.210
8.211 - replaceFormula 1 "-2 * 1 + (1 + x) = 0"; refFormula 1 (get_pos 1 1);
8.212 - val ((pt,_),_) = get_calc 1;
8.213 + replaceFormula 1 "-2 * 1 + (1 + x) = 0"; refFormula 1 (States.get_pos 1 1);
8.214 + val ((pt,_),_) = States.get_calc 1;
8.215 val str = pr_ctree pr_short pt;
8.216
8.217 (* before AK110725 this was
8.218 @@ -297,7 +297,7 @@
8.219 else error "inform.sml: diff.behav.replaceFormula: on Res += 1";
8.220
8.221 autoCalculate 1 CompleteCalc;
8.222 - val ((pt,pos as (p,_)),_) = get_calc 1;
8.223 + val ((pt,pos as (p,_)),_) = States.get_calc 1;
8.224 if pos = ([],Res) andalso "[x = 1]" = (UnparseC.term o fst) (get_obj g_result pt p) then()
8.225 else error "inform.sml: diff.behav.replaceFormula: on Res + = 2";
8.226 DEconstrCalcTree 1;
8.227 @@ -305,23 +305,23 @@
8.228 "--------- replaceFormula: on Res + = 1st Nd ---------------------";
8.229 "--------- replaceFormula: on Res + = 1st Nd ---------------------";
8.230 "--------- replaceFormula: on Res + = 1st Nd ---------------------";
8.231 - reset_states ();
8.232 + States.reset ();
8.233 CalcTree [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
8.234 ("Test", ["sqroot-test", "univariate", "equation", "test"],
8.235 ["Test", "squ-equ-test-subpbl1"]))];
8.236 Iterator 1; moveActiveRoot 1;
8.237 autoCalculate 1 CompleteCalcHead;
8.238 - autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);(*x + 1 = 2*)
8.239 - autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);(*x + 1 + - 1 * 2 = 0*);
8.240 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);(*x + 1 = 2*)
8.241 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);(*x + 1 + - 1 * 2 = 0*);
8.242
8.243 - replaceFormula 1 "x + 1 = 4 + -2"; refFormula 1 (get_pos 1 1);
8.244 - val ((pt,_),_) = get_calc 1;
8.245 + replaceFormula 1 "x + 1 = 4 + -2"; refFormula 1 (States.get_pos 1 1);
8.246 + val ((pt,_),_) = States.get_calc 1;
8.247 val str = pr_ctree pr_short pt;
8.248 writeln str;
8.249 if str= ". ----- pblobj -----\n1. x + 1 = 2\n1.1. x + 1 = 2\n1.2. 1 + x = 2\n1.3. 1 + x = - 2 + 4\n1.4. x + 1 = - 2 + 4\n" then ()
8.250 else error "inform.sml: diff.behav.replaceFormula: on Res 1 + = 1";
8.251 autoCalculate 1 CompleteCalc;
8.252 - val ((pt,pos as (p,_)),_) = get_calc 1;
8.253 + val ((pt,pos as (p,_)),_) = States.get_calc 1;
8.254 if pos = ([],Res) andalso "[x = 1]" = (UnparseC.term o fst)(get_obj g_result pt p) then()
8.255 else error "inform.sml: diff.behav.replaceFormula: on Res + = 2";
8.256 DEconstrCalcTree 1;
8.257 @@ -329,22 +329,22 @@
8.258 "--------- replaceFormula: on Frm + = 1st Nd ---------------------";
8.259 "--------- replaceFormula: on Frm + = 1st Nd ---------------------";
8.260 "--------- replaceFormula: on Frm + = 1st Nd ---------------------";
8.261 - reset_states ();
8.262 + States.reset ();
8.263 CalcTree [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
8.264 ("Test", ["sqroot-test", "univariate", "equation", "test"],
8.265 ["Test", "squ-equ-test-subpbl1"]))];
8.266 Iterator 1; moveActiveRoot 1;
8.267 autoCalculate 1 CompleteCalcHead;
8.268 - autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);(*x + 1 = 2*)
8.269 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);(*x + 1 = 2*)
8.270
8.271 - replaceFormula 1 "x + 1 = 4 + -2"; refFormula 1 (get_pos 1 1);
8.272 - val ((pt,_),_) = get_calc 1;
8.273 + replaceFormula 1 "x + 1 = 4 + -2"; refFormula 1 (States.get_pos 1 1);
8.274 + val ((pt,_),_) = States.get_calc 1;
8.275 val str = pr_ctree pr_short pt;
8.276 writeln str;
8.277 if str= ". ----- pblobj -----\n1. x + 1 = 2\n1.1. x + 1 = 2\n1.2. 1 + x = 2\n1.3. 1 + x = - 2 + 4\n1.4. x + 1 = - 2 + 4\n" then ()
8.278 else error "inform.sml: diff.behav.replaceFormula: on Frm 1 + = 1";
8.279 autoCalculate 1 CompleteCalc;
8.280 - val ((pt,pos as (p,_)),_) = get_calc 1;
8.281 + val ((pt,pos as (p,_)),_) = States.get_calc 1;
8.282 if pos = ([],Res) andalso "[x = 1]" = (UnparseC.term o fst)(get_obj g_result pt p) then()
8.283 else error "inform.sml: diff.behav.replaceFormula: on Frm 1 + = 2";
8.284 DEconstrCalcTree 1;
8.285 @@ -352,18 +352,18 @@
8.286 "--------- replaceFormula: cut calculation -----------------------";
8.287 "--------- replaceFormula: cut calculation -----------------------";
8.288 "--------- replaceFormula: cut calculation -----------------------";
8.289 - reset_states ();
8.290 + States.reset ();
8.291 CalcTree [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
8.292 ("Test", ["sqroot-test", "univariate", "equation", "test"],
8.293 ["Test", "squ-equ-test-subpbl1"]))];
8.294 Iterator 1; moveActiveRoot 1;
8.295 autoCalculate 1 CompleteCalc;
8.296 moveActiveRoot 1; moveActiveDown 1;
8.297 - if get_pos 1 1 = ([1], Frm) then ()
8.298 + if States.get_pos 1 1 = ([1], Frm) then ()
8.299 else error "inform.sml: diff.behav. cut calculation 1";
8.300
8.301 - replaceFormula 1 "x + 1 = 4 + -2"; refFormula 1 (get_pos 1 1);
8.302 - val ((pt,p),_) = get_calc 1;
8.303 + replaceFormula 1 "x + 1 = 4 + -2"; refFormula 1 (States.get_pos 1 1);
8.304 + val ((pt,p),_) = States.get_calc 1;
8.305 val str = pr_ctree pr_short pt;
8.306 writeln str;
8.307 if p = ([1], Res) then ()
8.308 @@ -449,17 +449,17 @@
8.309 "--------- syntax error ------------------------------------------";
8.310 "--------- syntax error ------------------------------------------";
8.311 "--------- syntax error ------------------------------------------";
8.312 - reset_states ();
8.313 + States.reset ();
8.314 CalcTree [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
8.315 ("Test", ["sqroot-test", "univariate", "equation", "test"],
8.316 ["Test", "squ-equ-test-subpbl1"]))];
8.317 Iterator 1; moveActiveRoot 1;
8.318 autoCalculate 1 CompleteCalcHead;
8.319 - autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);(*x + 1 = 2*)
8.320 - autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);(*x + 1 + - 1 * 2 = 0*);
8.321 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);(*x + 1 = 2*)
8.322 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);(*x + 1 + - 1 * 2 = 0*);
8.323
8.324 appendFormula 1 " x - "; (*<ERROR> syntax error in ' x - ' </ERROR>*)
8.325 - val ((pt,_),_) = get_calc 1;
8.326 + val ((pt,_),_) = States.get_calc 1;
8.327 val str = pr_ctree pr_short pt;
8.328 writeln str;
8.329 if str = ". ----- pblobj -----\n1. x + 1 = 2\n" then ()
8.330 @@ -491,13 +491,13 @@
8.331 "--------- CAS-command on ([],Pbl) FE-interface ------------------";
8.332 "--------- CAS-command on ([],Pbl) FE-interface ------------------";
8.333 "--------- CAS-command on ([],Pbl) FE-interface ------------------";
8.334 -reset_states ();
8.335 +States.reset ();
8.336 CalcTree [([], References.empty)];
8.337 Iterator 1;
8.338 moveActiveRoot 1;
8.339 replaceFormula 1 "solve(x+1=2,x)";
8.340 autoCalculate 1 CompleteCalc;
8.341 -val ((pt,p),_) = get_calc 1;
8.342 +val ((pt,p),_) = States.get_calc 1;
8.343 Test_Tool.show_pt pt;
8.344 if p = ([], Res) then ()
8.345 else error "inform.sml: diff.behav. CAScmd ([],Pbl) FE-interface";
8.346 @@ -506,7 +506,7 @@
8.347 "--------- inform [rational,simplification] ----------------------";
8.348 "--------- inform [rational,simplification] ----------------------";
8.349 "--------- inform [rational,simplification] ----------------------";
8.350 -reset_states ();
8.351 +States.reset ();
8.352 CalcTree [(["Term (a * x / (b * x) + c * x / (d * x) + e / f)", "normalform N"],
8.353 ("Rational", ["rational", "simplification"], ["simplification", "of_rationals"]))];
8.354 Iterator 1; moveActiveRoot 1;
8.355 @@ -515,7 +515,7 @@
8.356 "--- (- 1) give a preview on the calculation without any input";
8.357 (*
8.358 autoCalculate 1 CompleteCalc;
8.359 -val ((pt, p), _) = get_calc 1;
8.360 +val ((pt, p), _) = States.get_calc 1;
8.361 Test_Tool.show_pt pt;
8.362 [
8.363 (([], Frm), Simplify (a * x / (b * x) + c * x / (d * x) + e / f)),
8.364 @@ -530,7 +530,7 @@
8.365 "--- (0) user input as the *first* step does not work, thus impdo at least 1 step";
8.366 autoCalculate 1 (Steps 1);
8.367 autoCalculate 1 (Steps 1);
8.368 -val ((pt, p), _) = get_calc 1;
8.369 +val ((pt, p), _) = States.get_calc 1;
8.370 (*Test_Tool.show_pt pt;
8.371 [
8.372 (([], Frm), Simplify (a * x / (b * x) + c * x / (d * x) + e / f)),
8.373 @@ -539,7 +539,7 @@
8.374 *)
8.375 "--- (1) input an arbitrary next formula";
8.376 appendFormula 1 "((a * d) + (c * b)) / (b * d) + e / f" (*|> Future.join*);
8.377 -val ((pt, p), _) = get_calc 1;
8.378 +val ((pt, p), _) = States.get_calc 1;
8.379 (*Test_Tool.show_pt pt;
8.380 [
8.381 (([], Frm), Simplify (a * x / (b * x) + c * x / (d * x) + e / f)),
8.382 @@ -550,14 +550,14 @@
8.383 (([2,2], Res), (a * d + c * b) / (b * d) + e / f),
8.384 (([2], Res), (a * d + c * b) / (b * d) + e / f)]
8.385 *)
8.386 -val ((pt,p),_) = get_calc 1;
8.387 +val ((pt,p),_) = States.get_calc 1;
8.388 if p = ([2], Res) andalso (length o children o (get_nd pt)) (fst p) = 2 then ()
8.389 else error ("inform.sml: [rational,simplification] 1");
8.390
8.391 "--- (2) input the next formula that would be presented by mat-engine";
8.392 (* generate a preview:
8.393 autoCalculate 1 (Steps 1);
8.394 -val ((pt, p), _) = get_calc 1;
8.395 +val ((pt, p), _) = States.get_calc 1;
8.396 Test_Tool.show_pt pt;
8.397 [
8.398 (([], Frm), Simplify (a * x / (b * x) + c * x / (d * x) + e / f)),
8.399 @@ -570,7 +570,7 @@
8.400 (([3], Res), (b * d * e + b * c * f + a * d * f) / (b * d * f))] <--- input this
8.401 *)
8.402 appendFormula 1 "(b * d * e + b * c * f + a * d * f) / (b * d * f)" (*|> Future.join*);
8.403 -val ((pt, p), _) = get_calc 1;
8.404 +val ((pt, p), _) = States.get_calc 1;
8.405 (*Test_Tool.show_pt pt;
8.406 [
8.407 (([], Frm), Simplify (a * x / (b * x) + c * x / (d * x) + e / f)),
8.408 @@ -587,7 +587,7 @@
8.409
8.410 "--- (3) input the exact final result";
8.411 appendFormula 1 "(b * d * e + b * c * f + a * d * f) / (b * d * f)" (*|> Future.join*);
8.412 -val ((pt, p), _) = get_calc 1;
8.413 +val ((pt, p), _) = States.get_calc 1;
8.414 (*Test_Tool.show_pt pt;
8.415 [
8.416 (([], Frm), Simplify (a * x / (b * x) + c * x / (d * x) + e / f)),
8.417 @@ -608,7 +608,7 @@
8.418
8.419 "--- (4) finish the calculation + check the postcondition (in the future)";
8.420 autoCalculate 1 CompleteCalc;
8.421 -val ((pt, p), _) = get_calc 1;
8.422 +val ((pt, p), _) = States.get_calc 1;
8.423 val (t, asm) = get_obj g_result pt [];
8.424 if UnparseC.term t = "(a * d * f + b * c * f + b * d * e) / (b * d * f)" andalso
8.425 UnparseC.terms asm =(*"[\"b * d * f \<noteq> 0\",\"d \<noteq> 0\",\"b \<noteq> 0\",\"a * x / (b * x) + c * x / (d * x) + e / f is_ratpolyexp\"]"*)
8.426 @@ -643,13 +643,13 @@
8.427 error "diff.sml behav.changed for CAS Diff (..., x)";
8.428 TermC.atomty t;
8.429 "-----------------------------------------------------------------";
8.430 -(*1>*)reset_states ();
8.431 +(*1>*)States.reset ();
8.432 (*2>*)CalcTree [([], References.empty)];
8.433 (*3>*)Iterator 1;moveActiveRoot 1;
8.434 "----- here the Headline has been finished";
8.435 (*4>*)moveActiveFormula 1 ([],Pbl);
8.436 (*5>*)replaceFormula 1 "Diff (x \<up> 2 + x + 1, x)";
8.437 -val ((pt,_),_) = get_calc 1;
8.438 +val ((pt,_),_) = States.get_calc 1;
8.439 val PblObj {probl, meth, spec, fmz, loc, ...} = get_obj I pt [];
8.440 val (SOME istate, NONE) = loc;
8.441 (*default_print_depth 5;*)
8.442 @@ -665,7 +665,7 @@
8.443 "----- here the CalcHead has been completed --- ONCE MORE ?????";
8.444
8.445 (***difference II***)
8.446 -val ((pt,p),_) = get_calc 1;
8.447 +val ((pt,p),_) = States.get_calc 1;
8.448 (*val p = ([], Pbl)*)
8.449 val PblObj {probl, meth, spec, fmz, loc, ...} = get_obj I pt [];
8.450 val (SOME istate, NONE) = loc;
8.451 @@ -691,7 +691,7 @@
8.452 (*7>*)fetchProposedTactic 1 (*--> Apply_Method*);
8.453 (*WN081028 fixed <ERROR> helpless </ERROR> by inform returning ...(.,Met)*)
8.454 autoCalculate 1 CompleteCalc;
8.455 -val ((pt,p),_) = get_calc 1;
8.456 +val ((pt,p),_) = States.get_calc 1;
8.457 val Form res = (#1 o ME_Misc.pt_extract) (pt, ([],Res));
8.458 Test_Tool.show_pt pt;
8.459
8.460 @@ -704,13 +704,13 @@
8.461 "--------- Take as 1st tac, start from exp -----------------------";
8.462 (*the following input is copied from BridgeLog Java <==> SML,
8.463 omitting unnecessary inputs*)
8.464 -(*1>*)reset_states ();
8.465 +(*1>*)States.reset ();
8.466 (*2>*)CalcTree [(["functionTerm (x \<up> 2 + x + 1)", "differentiateFor x", "derivative f_'_f"],("Isac_Knowledge",["derivative_of", "function"],["diff", "differentiate_on_R"]))];
8.467 (*3>*)Iterator 1; moveActiveRoot 1;
8.468
8.469 (*6>*)(*completeCalcHead*)autoCalculate 1 CompleteCalcHead;
8.470 (***difference II***)
8.471 -val ((pt,_),_) = get_calc 1;
8.472 +val ((pt,_),_) = States.get_calc 1;
8.473 val PblObj {probl, meth, spec, fmz, loc, ...} = get_obj I pt [];
8.474 val (SOME istate, NONE) = loc;
8.475 (*default_print_depth 5;*) writeln (Istate.string_of (fst istate)); (*default_print_depth 3;*)
8.476 @@ -734,7 +734,7 @@
8.477 writeln"-----------------------------------------------------------";
8.478 (*7>*)fetchProposedTactic 1 (*--> Apply_Method*);
8.479 autoCalculate 1 (Steps 1);
8.480 -val ((pt,p),_) = get_calc 1;
8.481 +val ((pt,p),_) = States.get_calc 1;
8.482 val Form res = (#1 o ME_Misc.pt_extract) (pt, p);
8.483 if UnparseC.term res = "d_d x (x \<up> 2 + x + 1)" then ()
8.484 else error "diff.sml Diff (x \<up> 2 + x + 1, x) from exp";
8.485 @@ -743,7 +743,7 @@
8.486 "--------- implicit_take, start with <NEW> (CAS input) ---------------";
8.487 "--------- implicit_take, start with <NEW> (CAS input) ---------------";
8.488 "--------- implicit_take, start with <NEW> (CAS input) ---------------";
8.489 -reset_states ();
8.490 +States.reset ();
8.491 CalcTree [([], References.empty)];
8.492 (*[[from sml: > @@@@@begin@@@@@
8.493 [[from sml: 1
8.494 @@ -1006,7 +1006,7 @@
8.495 "--------- embed fun check_for ------------------------";
8.496 "--------- embed fun check_for ------------------------";
8.497 "--------- embed fun check_for ------------------------";
8.498 -reset_states ();
8.499 +States.reset ();
8.500 CalcTree
8.501 [(["functionTerm (x \<up> 2 + sin (x \<up> 4))", "differentiateFor x", "derivative f_f'"],
8.502 ("Isac_Knowledge", ["derivative_of", "function"], ["diff", "differentiate_on_R"]))];
8.503 @@ -1019,8 +1019,8 @@
8.504
8.505 "~~~~~ fun appendFormula , args:"; val (cI, (ifo:TermC.as_string)) = (1, "d_d x (x \<up> 2) + cos (4 * x \<up> 3)");
8.506 "~~~~~ fun appendFormula' , args:"; val (cI, (ifo: TermC.as_string)) = (cI, ifo);
8.507 - val cs = get_calc cI
8.508 - val pos = get_pos cI 1;
8.509 + val cs = States.get_calc cI
8.510 + val pos = States.get_pos cI 1;
8.511 (*+*)if pos = ([1], Res) then () else error "inform with (positive) Error_Pattern.check_for broken 1";
8.512 val ("ok", cs' as (_, _, ptp)) = (*case*) Step.do_next pos cs (*of*);
8.513 (*case*) Step_Solve.by_term ptp (encode ifo) (*of*); (*ERROR WAS: "no derivation found"*)
8.514 @@ -1065,7 +1065,7 @@
8.515 "--------- embed fun find_fill_patterns ---------------------------";
8.516 "--------- embed fun find_fill_patterns ---------------------------";
8.517 "--------- embed fun find_fill_patterns ---------------------------";
8.518 -reset_states ();
8.519 +States.reset ();
8.520 CalcTree
8.521 [(["functionTerm (x \<up> 2 + sin (x \<up> 4))", "differentiateFor x", "derivative f_f'"],
8.522 ("Isac_Knowledge", ["derivative_of", "function"], ["diff", "differentiate_on_R"]))];
8.523 @@ -1080,8 +1080,8 @@
8.524 <CALCMESSAGE> no derivation found </CALCMESSAGE>*)
8.525
8.526 "~~~~~ fun findFillpatterns, args:"; val (cI, errpatID) = (1, "chain-rule-diff-both");
8.527 - val ((pt, _), _) = get_calc cI
8.528 - val pos = get_pos cI 1;
8.529 + val ((pt, _), _) = States.get_calc cI
8.530 + val pos = States.get_pos cI 1;
8.531 "~~~~~ fun find_fill_patterns , args:"; val ((pt, pos as (p, _)), errpatID) = ((pt, pos), errpatID);
8.532 val f_curr = Ctree.get_curr_formula (pt, pos);
8.533 val pp = Ctree.par_pblobj pt p
8.534 @@ -1150,7 +1150,7 @@
8.535 "--------- build fun is_exactly_equal, inputFillFormula ----------";
8.536 "--------- build fun is_exactly_equal, inputFillFormula ----------";
8.537 "--------- build fun is_exactly_equal, inputFillFormula ----------";
8.538 -reset_states ();
8.539 +States.reset ();
8.540 CalcTree
8.541 [(["functionTerm (x \<up> 2 + sin (x \<up> 4))", "differentiateFor x", "derivative f_f'"],
8.542 ("Isac_Knowledge", ["derivative_of", "function"], ["diff", "differentiate_on_R"]))];
8.543 @@ -1164,8 +1164,8 @@
8.544 would recognize "cos (4 * x \<up> (4 - 1)) + 2 * x" as well.
8.545 results in <CALCMESSAGE> error pattern #chain-rule-diff-both# </CALCMESSAGE>
8.546 instead of <CALCMESSAGE> no derivation found </CALCMESSAGE> *)
8.547 - val ((pt,pos), _) = get_calc 1;
8.548 - val p = get_pos 1 1;
8.549 + val ((pt,pos), _) = States.get_calc 1;
8.550 + val p = States.get_pos 1 1;
8.551 val (Form f, _, asms) = ME_Misc.pt_extract (pt, p);
8.552
8.553 if p = ([1], Res) andalso UnparseC.term f = "d_d x (x \<up> 2) + d_d x (sin (x \<up> 4))" then
8.554 @@ -1179,8 +1179,8 @@
8.555 findFillpatterns 1 "chain-rule-diff-both"; (*<<<<<<<=================================*)
8.556 (*<CALCMESSAGE> fill patterns #fill-d_d-arg#d_d x (x \<up> 2) + d_d x (sin (x \<up> 4)) =
8.557 d_d x (x \<up> 2) + cos (x \<up> 4) * d_d x ?_dummy_1#fill-both-args#...#...#... *)
8.558 - val ((pt,pos),_) = get_calc 1;
8.559 - val p = get_pos 1 1;
8.560 + val ((pt,pos),_) = States.get_calc 1;
8.561 + val p = States.get_pos 1 1;
8.562
8.563 val (Form f, _, asms) = ME_Misc.pt_extract (pt, p);
8.564 if p = ([1], Res) andalso UnparseC.term f = "d_d x (x \<up> 2) + d_d x (sin (x \<up> 4))" then
8.565 @@ -1193,8 +1193,8 @@
8.566
8.567 requestFillformula 1 ("chain-rule-diff-both", "fill-both-args");(*<<<<<<<============*)
8.568 (*<AUTOCALC> ([1], Res) ([2], Res) ([2], Res) </AUTOCALC>*)
8.569 - val ((pt,pos),_) = get_calc 1;
8.570 - val p = get_pos 1 1;
8.571 + val ((pt,pos),_) = States.get_calc 1;
8.572 + val p = States.get_pos 1 1;
8.573 val (Form f, _, asms) = ME_Misc.pt_extract (pt, p);
8.574 if p = ([1], Res) andalso existpt [2] pt
8.575 andalso UnparseC.term f = "d_d x (x \<up> 2) + d_d x (sin (x \<up> 4))"
8.576 @@ -1212,8 +1212,8 @@
8.577 *)
8.578 "~~~~~ fun inputFillFormula, args:"; val (cI, ifo) =
8.579 (1, "d_d x (x \<up> 2) + cos (x \<up> 4) * d_d x (x \<up> 4)");
8.580 - val ((pt, _), _) = get_calc cI
8.581 - val pos = get_pos cI 1;
8.582 + val ((pt, _), _) = States.get_calc cI
8.583 + val pos = States.get_pos cI 1;
8.584
8.585 "~~~~~ fun is_exactly_equal, args:"; val ((pt, pos as (p, p_)), istr) = ((pt, pos), ifo);
8.586 val SOME ifo = parseNEW (ThyC.get_theory "Isac_Knowledge" |> Proof_Context.init_global) istr
8.587 @@ -1227,13 +1227,13 @@
8.588
8.589 "~~~~~ to inputFillFormula return val:"; val ("ok", tac) = ("ok", tac);
8.590 val ("ok", (_, c, ptp as (_,p'))) = Step.by_tactic tac (pt, pos);
8.591 - upd_calc cI (ptp, []);
8.592 - upd_ipos cI 1 p';
8.593 + States.upd_calc cI (ptp, []);
8.594 + States.upd_ipos cI 1 p';
8.595 autocalculateOK2xml cI pos (if null c then p' else last_elem c) p';
8.596
8.597 "~~~~~ final check:";
8.598 -val ((pt, _),_) = get_calc 1;
8.599 -val p = get_pos 1 1;
8.600 +val ((pt, _),_) = States.get_calc 1;
8.601 +val p = States.get_pos 1 1;
8.602 val (Form f, _, asms) = ME_Misc.pt_extract (pt, p);
8.603 if p = ([2], Res) andalso UnparseC.term f = "d_d x (x \<up> 2) + cos (x \<up> 4) * d_d x (x \<up> 4)"
8.604 then case get_obj g_tac pt (fst p) of Rewrite_Inst (["(''bdv'', x)"],
9.1 --- a/test/Tools/isac/Interpret/li-tool.sml Fri Sep 09 10:53:51 2022 +0200
9.2 +++ b/test/Tools/isac/Interpret/li-tool.sml Sun Sep 11 14:31:15 2022 +0200
9.3 @@ -59,14 +59,14 @@
9.4 (* compare test/../interface.sml
9.5 "--------- getTactic, fetchApplicableTactics ------------";
9.6 *)
9.7 - reset_states ();
9.8 + States.reset ();
9.9 CalcTree [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
9.10 ("Test", ["sqroot-test", "univariate", "equation", "test"],
9.11 ["Test", "squ-equ-test-subpbl1"]))];
9.12 Iterator 1;
9.13 moveActiveRoot 1;
9.14 autoCalculate 1 CompleteCalc;
9.15 - val ((pt,_),_) = get_calc 1;
9.16 + val ((pt,_),_) = States.get_calc 1;
9.17 Test_Tool.show_pt pt;
9.18
9.19 (*UC\label{SOLVE:MANUAL:TACTIC:listall} UC 30.3.2.2 p.175*)
9.20 @@ -101,7 +101,7 @@
9.21 "----------- fun specific_from_prog ----------------------------";
9.22 "----------- fun specific_from_prog ----------------------------";
9.23 "----------- fun specific_from_prog ----------------------------";
9.24 - reset_states ();
9.25 + States.reset ();
9.26 CalcTree [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
9.27 ("Test", ["sqroot-test", "univariate", "equation", "test"],
9.28 ["Test", "squ-equ-test-subpbl1"]))];
9.29 @@ -114,7 +114,7 @@
9.30
9.31 fetchApplicableTactics 1 99999 ([1],Res);
9.32 "~~~~~ fun fetchApplicableTactics, args:"; val (cI, (scope:int), (p:pos')) = (1, 99999, ([1],Res));
9.33 -val ((pt, _), _) = get_calc cI;
9.34 +val ((pt, _), _) = States.get_calc cI;
9.35 (*version 1:*)
9.36 case from_prog pt p of [Rewrite_Set "norm_equation", Rewrite_Set "Test_simplify",
9.37 Subproblem ("Test", ["LINEAR", "univariate", "equation", "test"]),
10.1 --- a/test/Tools/isac/Interpret/lucas-interpreter.sml Fri Sep 09 10:53:51 2022 +0200
10.2 +++ b/test/Tools/isac/Interpret/lucas-interpreter.sml Sun Sep 11 14:31:15 2022 +0200
10.3 @@ -527,8 +527,8 @@
10.4
10.5 (*//---------- appendFormula 1 "x = 1" \<longrightarrow> Step_Solve.inform \<longrightarrow> LI.locate_input_term ----------\\*)
10.6 "~~~~~ fun appendFormula , args:"; val ((*cI, *) ifo: TermC.as_string) = ((**) "x = 1");
10.7 - val cs = (*get_calc cI*) ((pt, p), [(*nxt, nxt_, (pos, (ist, ctxt))*)])
10.8 - val pos = (*get_pos cI 1*) p
10.9 + val cs = (*States.get_calc cI*) ((pt, p), [(*nxt, nxt_, (pos, (ist, ctxt))*)])
10.10 + val pos = (*States.get_pos cI 1*) p
10.11
10.12 (*+*)val ptp''''' = (pt, p);
10.13 (*+*)if snd ptp''''' = ([1], Res) then () else error "old_cs changed";
11.1 --- a/test/Tools/isac/Knowledge/algein.sml Fri Sep 09 10:53:51 2022 +0200
11.2 +++ b/test/Tools/isac/Knowledge/algein.sml Sun Sep 11 14:31:15 2022 +0200
11.3 @@ -90,7 +90,7 @@
11.4 Iterator 1;
11.5 moveActiveRoot 1;
11.6 autoCalculate 1 CompleteCalc;
11.7 -val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
11.8 +val ((pt,p),_) = States.get_calc 1; Test_Tool.show_pt pt;
11.9 if p = ([], Res) andalso UnparseC.term (get_obj g_res pt (fst p)) = "L = 104" then()
11.10 else error "algein.sml: 'Berechnung' 'erstSymbolisch' changed";
11.11
12.1 --- a/test/Tools/isac/Knowledge/biegelinie-2.sml Fri Sep 09 10:53:51 2022 +0200
12.2 +++ b/test/Tools/isac/Knowledge/biegelinie-2.sml Sun Sep 11 14:31:15 2022 +0200
12.3 @@ -24,13 +24,13 @@
12.4 val (dI',pI',mI') = ("Biegelinie", ["vonBelastungZu", "Biegelinien"],
12.5 ["Biegelinien", "ausBelastung"]);
12.6
12.7 -reset_states ();
12.8 +States.reset ();
12.9 CalcTree [(fmz, (dI',pI',mI'))];
12.10 Iterator 1;
12.11 moveActiveRoot 1;
12.12 autoCalculate 1 CompleteCalc;
12.13
12.14 -val ((pt, p),_) = get_calc 1;
12.15 +val ((pt, p),_) = States.get_calc 1;
12.16 (* ERROR: THIS TEST WAS BROKEN BEFORE CS "eliminate ThmC.numerals_to_Free",
12.17 UNDETECTED BY Test_Isac_Short.thy ===========================================================\\
12.18 if p = ([], Res) andalso (get_obj g_res pt (fst p) |> UnparseC.term) =
13.1 --- a/test/Tools/isac/Knowledge/biegelinie-3.sml Fri Sep 09 10:53:51 2022 +0200
13.2 +++ b/test/Tools/isac/Knowledge/biegelinie-3.sml Sun Sep 11 14:31:15 2022 +0200
13.3 @@ -24,13 +24,13 @@
13.4 val (dI',pI',mI') = ("Biegelinie", ["setzeRandbedingungen", "Biegelinien"],
13.5 ["Biegelinien", "setzeRandbedingungenEin"]);
13.6
13.7 -reset_states ();
13.8 +States.reset ();
13.9 CalcTree [(fmz, (dI',pI',mI'))];
13.10 Iterator 1;
13.11 moveActiveRoot 1;
13.12 autoCalculate 1 CompleteCalc;
13.13
13.14 -val ((pt, p),_) = get_calc 1;
13.15 +val ((pt, p),_) = States.get_calc 1;
13.16 if p = ([], Res) andalso (get_obj g_res pt (fst p) |> UnparseC.term) =
13.17 "[0 = - 1 * c_4 / - 1,\n 0 =\n (- 24 * c_4 + - 24 * L * c_3 + 12 * L \<up> 2 * c_2 + 4 * L \<up> 3 * c +\n - 1 * L \<up> 4 * q_0) /\n - 24,\n 0 = c_2, 0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2]"
13.18 (*"[0 = - 1 * c_4 / - 1,\n 0 =\n (- 24 * c_4 * EI + - 24 * L * c_3 * EI + 12 * L \<up> 2 * c_2 +\n 4 * L \<up> 3 * c +\n - 1 * L \<up> 4 * q_0) /\n (- 24 * EI),\n 0 = c_2, 0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2]"
14.1 --- a/test/Tools/isac/Knowledge/biegelinie-4.sml Fri Sep 09 10:53:51 2022 +0200
14.2 +++ b/test/Tools/isac/Knowledge/biegelinie-4.sml Sun Sep 11 14:31:15 2022 +0200
14.3 @@ -24,13 +24,13 @@
14.4 "AbleitungBiegelinie dy"];
14.5 val (dI',pI',mI') = ("Biegelinie", ["Biegelinien"], ["IntegrierenUndKonstanteBestimmen2"]);
14.6
14.7 -reset_states ();
14.8 +States.reset ();
14.9 CalcTree [(fmz, (dI',pI',mI'))];
14.10 Iterator 1;
14.11 moveActiveRoot 1;
14.12 autoCalculate 1 CompleteCalc;
14.13
14.14 -val ((pt, p),_) = get_calc 1;
14.15 +val ((pt, p),_) = States.get_calc 1;
14.16 if p = ([], Pbl) then () else error ""
14.17 get_obj I pt (fst p); (*TODO investigate failure*)
14.18
14.19 @@ -59,8 +59,8 @@
14.20 *** Step.add: not impl.for Empty_Tac_
14.21 val it = <AUTOCALC><CALCID>1</CALCID><CALCMESSAGE>helpless</CALCMESSAGE></AUTOCALC>: XML.tree *)
14.22
14.23 -val ((pt,_),_) = get_calc 1;
14.24 -val ip = get_pos 1 1;
14.25 +val ((pt,_),_) = States.get_calc 1;
14.26 +val ip = States.get_pos 1 1;
14.27 val (Form f, tac, asms) = ME_Misc.pt_extract (pt, ip);
14.28
14.29 if ip = ([3, 8, 1], Res) andalso
15.1 --- a/test/Tools/isac/Knowledge/diff-app.sml Fri Sep 09 10:53:51 2022 +0200
15.2 +++ b/test/Tools/isac/Knowledge/diff-app.sml Sun Sep 11 14:31:15 2022 +0200
15.3 @@ -400,7 +400,7 @@
15.4 "--------- autoCalc .. scripts for maximum-example ---------------";
15.5 "--------- autoCalc .. scripts for maximum-example ---------------";
15.6 (*++++++++ see systest/inform.sml 'I_Model.complete' ++++++++*)
15.7 - reset_states ();
15.8 + States.reset ();
15.9 val fmz =
15.10 ["fixedValues [r=Arbfix]", "maximum A",
15.11 "valuesFor [a,b]",
15.12 @@ -420,7 +420,7 @@
15.13 CalcTree [(fmz, (dI',pI',mI'))];
15.14 Iterator 1; moveActiveRoot 1;
15.15 autoCalculate 1 CompleteCalcHead;
15.16 - refFormula 1 (get_pos 1 1);
15.17 + refFormula 1 (States.get_pos 1 1);
15.18
15.19 fetchProposedTactic 1;
15.20 (*autoCalculate 1 (Steps 1);
15.21 @@ -437,7 +437,7 @@
15.22 autoCalculate 1 CompleteCalcHead;
15.23
15.24 fetchProposedTactic 1;
15.25 - val ((pt,p),_) = get_calc 1;
15.26 + val ((pt,p),_) = States.get_calc 1;
15.27 val mits = get_obj g_met pt (fst p);
15.28 writeln (I_Model.to_string ctxt mits);
15.29 (*
16.1 --- a/test/Tools/isac/Knowledge/diff.sml Fri Sep 09 10:53:51 2022 +0200
16.2 +++ b/test/Tools/isac/Knowledge/diff.sml Sun Sep 11 14:31:15 2022 +0200
16.3 @@ -301,7 +301,7 @@
16.4 "----------- autoCalculate differentiate_on_R 2/x \<up> 2 -----";
16.5 "----------- autoCalculate differentiate_on_R 2/x \<up> 2 -----";
16.6 "----------- autoCalculate differentiate_on_R 2/x \<up> 2 -----";
16.7 -reset_states ();
16.8 +States.reset ();
16.9 CalcTree
16.10 [(["functionTerm (x \<up> 2 + x+ 1/x + 2/x \<up> 2)",
16.11 (*"functionTerm ((x \<up> 3) \<up> 5)",*)
16.12 @@ -311,13 +311,13 @@
16.13 Iterator 1;
16.14 moveActiveRoot 1;
16.15 autoCalculate 1 CompleteCalc;
16.16 -val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
16.17 +val ((pt,p),_) = States.get_calc 1; Test_Tool.show_pt pt;
16.18 if p = ([], Res) andalso UnparseC.term (get_obj g_res pt (fst p)) =
16.19 "1 + 2 * x + - 1 / x \<up> 2 + - 4 / x \<up> 3" then ()
16.20 else error "diff.sml: differentiate_on_R 2/x \<up> 2 changed";
16.21
16.22 "---------------------------------------------------------";
16.23 -reset_states ();
16.24 +States.reset ();
16.25 CalcTree
16.26 [(["functionTerm (x \<up> 3 * x \<up> 5)",
16.27 "differentiateFor x", "derivative f_f'"],
16.28 @@ -329,7 +329,7 @@
16.29 (* Rewrite.trace_on := false; (*true false*)
16.30 LItool.trace_on := false;
16.31 *)
16.32 -val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
16.33 +val ((pt,p),_) = States.get_calc 1; Test_Tool.show_pt pt;
16.34
16.35 if p = ([], Res) andalso UnparseC.term (get_obj g_res pt (fst p)) =
16.36 "8 * x \<up> 7" then ()
16.37 @@ -338,7 +338,7 @@
16.38 "----------- autoCalculate diff after_simplification ----";
16.39 "----------- autoCalculate diff after_simplification ----";
16.40 "----------- autoCalculate diff after_simplification ----";
16.41 -reset_states ();
16.42 +States.reset ();
16.43 CalcTree
16.44 [(["functionTerm (x \<up> 3 * x \<up> 5)",
16.45 "differentiateFor x", "derivative f_f'"],
16.46 @@ -353,12 +353,12 @@
16.47 (* Rewrite.trace_on := false; (*true false*)
16.48 LItool.trace_on := false;
16.49 *)
16.50 -val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
16.51 +val ((pt,p),_) = States.get_calc 1; Test_Tool.show_pt pt;
16.52 if p = ([], Res) andalso UnparseC.term (get_obj g_res pt (fst p)) = "8 * x \<up> 7"
16.53 then () else error "biegelinie.sml: 1st biegelin.7.27 changed";
16.54
16.55 "--------------------------------------------------------";
16.56 -reset_states ();
16.57 +States.reset ();
16.58 CalcTree
16.59 [(["functionTerm ((x \<up> 3) \<up> 5)",
16.60 "differentiateFor x", "derivative f_f'"],
16.61 @@ -367,14 +367,14 @@
16.62 Iterator 1;
16.63 moveActiveRoot 1;
16.64 autoCalculate 1 CompleteCalc;
16.65 -val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
16.66 +val ((pt,p),_) = States.get_calc 1; Test_Tool.show_pt pt;
16.67 if p = ([], Res) andalso UnparseC.term (get_obj g_res pt (fst p)) = "15 * x \<up> 14"
16.68 then () else error "biegelinie.sml: 1st biegelin.7.27 changed";
16.69
16.70 "----------- autoCalculate differentiate_equality -------";
16.71 "----------- autoCalculate differentiate_equality -------";
16.72 "----------- autoCalculate differentiate_equality -------";
16.73 -reset_states ();
16.74 +States.reset ();
16.75 CalcTree
16.76 [(["functionEq (A = s * (a - (s::real)))", "differentiateFor s", "derivativeEq f_f'"],
16.77 ("Isac_Knowledge", ["named", "derivative_of", "function"],
16.78 @@ -382,7 +382,7 @@
16.79 Iterator 1;
16.80 moveActiveRoot 1;
16.81 autoCalculate 1 CompleteCalc;
16.82 -val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
16.83 +val ((pt,p),_) = States.get_calc 1; Test_Tool.show_pt pt;
16.84
16.85 "----------- tests for examples -------------------------";
16.86 "----------- tests for examples -------------------------";
16.87 @@ -400,7 +400,7 @@
16.88 "------------inform for x \<up> 2+x+1 -------------------------";
16.89 "------------inform for x \<up> 2+x+1 -------------------------";
16.90 "------------inform for x \<up> 2+x+1 -------------------------";
16.91 -reset_states ();
16.92 +States.reset ();
16.93 CalcTree
16.94 [(["functionTerm (x \<up> 2 + x + 1)",
16.95 "differentiateFor x", "derivative f_f'"],
16.96 @@ -412,9 +412,9 @@
16.97 autoCalculate 1 (Steps 1);
16.98 autoCalculate 1 (Steps 1);
16.99 autoCalculate 1 (Steps 1);
16.100 -val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
16.101 +val ((pt,p),_) = States.get_calc 1; Test_Tool.show_pt pt;
16.102 appendFormula 1 "2*x + d_d x x + d_d x 1" (*|> Future.join*);
16.103 -val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
16.104 +val ((pt,p),_) = States.get_calc 1; Test_Tool.show_pt pt;
16.105 if existpt' ([3], Res) pt then ()
16.106 else error "diff.sml: inform d_d x (x \<up> 2 + x + 1) doesnt work";
16.107
17.1 --- a/test/Tools/isac/Knowledge/eqsystem-2.sml Fri Sep 09 10:53:51 2022 +0200
17.2 +++ b/test/Tools/isac/Knowledge/eqsystem-2.sml Sun Sep 11 14:31:15 2022 +0200
17.3 @@ -111,7 +111,7 @@
17.4 (TermC.str2term "bdv_3", TermC.str2term "c_3"), (TermC.str2term "bdv_4", TermC.str2term "c_4")];
17.5
17.6 "------- Bsp 7.27";
17.7 -reset_states ();
17.8 +States.reset ();
17.9 CalcTree [(
17.10 ["Traegerlaenge L", "Streckenlast q_0", "Biegelinie y",
17.11 "Randbedingungen [y 0 = (0::real), y L = 0, M_b 0 = 0, M_b L = 0]", "FunktionsVariable x"],
17.12 @@ -153,7 +153,7 @@
17.13 *)
17.14
17.15 "------- Bsp 7.28 ---------------vvvvvvvvvvvvv Momentenlinie postponed";
17.16 -reset_states ();
17.17 +States.reset ();
17.18 CalcTree [((*WN130908 <ERROR> error in kernel </ERROR>*)
17.19 ["Traegerlaenge L", "Momentenlinie (-q_0 / L * x \<up> 3 / 6)",
17.20 "Biegelinie y",
17.21 @@ -167,7 +167,7 @@
17.22 *)
17.23
17.24 "------- Bsp 7.69";
17.25 -reset_states ();
17.26 +States.reset ();
17.27 CalcTree [(
17.28 ["Traegerlaenge L", "Streckenlast q_0", "Biegelinie y",
17.29 "Randbedingungen [y 0 = (0::real), y L = 0, y' 0 = 0, y' L = 0]", "FunktionsVariable x"],
17.30 @@ -187,7 +187,7 @@
17.31 "0 = c_3 + (6 * L * c_2 + 3 * L \<up> 2 * c + - 1 * L \<up> 3 * q_0) / (-6 * EI)]");
17.32
17.33 "------- Bsp 7.70";
17.34 -reset_states ();
17.35 +States.reset ();
17.36 CalcTree [(
17.37 ["Traegerlaenge L", "Streckenlast q_0", "Biegelinie y",
17.38 "Randbedingungen [Q 0 = q_0 * L, M_b L = 0, y 0 = (0::real), y' 0 = 0]", "FunktionsVariable x"],
17.39 @@ -305,7 +305,7 @@
17.40 then () else error "eqsystem.sml: 7.70 with met top_down_: me";
17.41
17.42 "------- Bsp 7.71";
17.43 -reset_states ();
17.44 +States.reset ();
17.45 CalcTree [(["Traegerlaenge L", "Streckenlast q_0", "Biegelinie y",
17.46 "Randbedingungen [M_b L = 0, y 0 = (0::real), y L = 0, y' 0 = 0]",
17.47 "FunktionsVariable x", "GleichungsVariablen [c, c_2, c_3, c_4]",
17.48 @@ -326,7 +326,7 @@
17.49 \ 0 = c_3 + 0 / (- 1 * EI)]";
17.50
17.51 "------- Bsp 7.72a ---------------vvvvvvvvvvvvv Momentenlinie postponed";
17.52 -reset_states ();
17.53 +States.reset ();
17.54 CalcTree [(["Traegerlaenge L",
17.55 "Momentenlinie ((q_0 * L)/ 6 * x - q_0 /(6 * L) * x \<up> ^3)",
17.56 "Biegelinie y",
17.57 @@ -340,7 +340,7 @@
17.58 *)
17.59
17.60 "------- Bsp 7.72b";
17.61 -reset_states ();
17.62 +States.reset ();
17.63 CalcTree [(["Traegerlaenge L", "Streckenlast (q_0 / L * x)", "Biegelinie y",
17.64 "Randbedingungen [M_b 0 = 0, M_b L = 0, y 0 = (0::real), y L = 0]",
17.65 "FunktionsVariable x", "GleichungsVariablen [c, c_2, c_3, c_4]",
17.66 @@ -361,7 +361,7 @@
17.67 \ 0 = c_4 + L * c_3 + (60 * L \<up> 2 * c_2 + 20 * L \<up> 3 * c + - 1 * L \<up> 4 * q_0) / (- 120 * EI)]";
17.68
17.69 "------- Bsp 7.73 ---------------vvvvvvvvvvvvv Momentenlinie postponed";
17.70 -reset_states ();
17.71 +States.reset ();
17.72 CalcTree [(["Traegerlaenge L", "Momentenlinie ???",(*description unclear*)
17.73 "Biegelinie y",
17.74 "Randbedingungen [y L = 0, y' L = 0]",
18.1 --- a/test/Tools/isac/Knowledge/equation.sml Fri Sep 09 10:53:51 2022 +0200
18.2 +++ b/test/Tools/isac/Knowledge/equation.sml Sun Sep 11 14:31:15 2022 +0200
18.3 @@ -17,14 +17,14 @@
18.4 "----------- CAS input -------------------------------------------";
18.5 "----------- CAS input -------------------------------------------";
18.6 "----------- CAS input -------------------------------------------";
18.7 -reset_states ();
18.8 +States.reset ();
18.9 CalcTree [([], References.empty)];
18.10 Iterator 1;
18.11 moveActiveRoot 1;
18.12 replaceFormula 1 "solve (x+1=2, x)";
18.13 (*========== inhibit exn 130719 Isabelle2013 ===================================loops
18.14 autoCalculate 1 CompleteCalc;
18.15 -val ((pt,p),_) = get_calc 1;
18.16 +val ((pt,p),_) = States.get_calc 1;
18.17 val Form res = (#1 o ME_Misc.pt_extract) (pt, ([],Res));
18.18 Test_Tool.show_pt pt;
18.19 if p = ([], Res) andalso UnparseC.term res = "[x = 1]" then ()
19.1 --- a/test/Tools/isac/Knowledge/inssort.sml Fri Sep 09 10:53:51 2022 +0200
19.2 +++ b/test/Tools/isac/Knowledge/inssort.sml Sun Sep 11 14:31:15 2022 +0200
19.3 @@ -161,7 +161,7 @@
19.4 "----------- insertion sort: met_Prog_sort_ins_steps -------------------------";
19.5 "----------- insertion sort: met_Prog_sort_ins_steps -------------------------";
19.6 "----------- insertion sort: met_Prog_sort_ins_steps -------------------------";
19.7 -reset_states ();
19.8 +States.reset ();
19.9 CalcTree
19.10 [(["unsorted {||1, 3, 2||}", "sorted s_s"],
19.11 ("InsSort", ["insertion", "SORT", "Programming"],
19.12 @@ -171,7 +171,7 @@
19.13 autoCalculate 1 CompleteCalc;
19.14 interSteps 1 ([],Res);
19.15
19.16 -val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
19.17 +val ((pt,p),_) = States.get_calc 1; Test_Tool.show_pt pt;
19.18
19.19 if p = ([], Res)andalso UnparseC.term (get_obj g_res pt (fst p)) = "{|| 1, 2, 3 ||}"
19.20 andalso length (ME_Misc.get_interval ([], Pbl) ([], Res) 1 pt) = 23 then ()
20.1 --- a/test/Tools/isac/Knowledge/integrate.sml Fri Sep 09 10:53:51 2022 +0200
20.2 +++ b/test/Tools/isac/Knowledge/integrate.sml Sun Sep 11 14:31:15 2022 +0200
20.3 @@ -406,14 +406,14 @@
20.4 "----------- autoCalculate [diff,integration] -----------";
20.5 "----------- autoCalculate [diff,integration] -----------";
20.6 "----------- autoCalculate [diff,integration] -----------";
20.7 -reset_states ();
20.8 +States.reset ();
20.9 CalcTree
20.10 [(["functionTerm (x \<up> 2 + 1)", "integrateBy x", "antiDerivative FF"],
20.11 ("Integrate", ["integrate", "function"], ["diff", "integration"]))];
20.12 Iterator 1;
20.13 moveActiveRoot 1;
20.14 autoCalculate 1 CompleteCalc;
20.15 -val ((pt,p),_) = get_calc 1; @{make_string} p; Test_Tool.show_pt pt;
20.16 +val ((pt,p),_) = States.get_calc 1; @{make_string} p; Test_Tool.show_pt pt;
20.17 val (Form t,_,_) = ME_Misc.pt_extract (pt, p);
20.18 if UnparseC.term t = "c + x + 1 / 3 * x \<up> 3" then ()
20.19 else error "integrate.sml -- interSteps [diff,integration] -- result";
21.1 --- a/test/Tools/isac/Knowledge/inverse_z_transform.sml Fri Sep 09 10:53:51 2022 +0200
21.2 +++ b/test/Tools/isac/Knowledge/inverse_z_transform.sml Sun Sep 11 14:31:15 2022 +0200
21.3 @@ -180,7 +180,7 @@
21.4 "----------- test [SignalProcessing,Z_Transform,Inverse_sub] auto-";
21.5 "----------- test [SignalProcessing,Z_Transform,Inverse_sub] auto-";
21.6 "----------- test [SignalProcessing,Z_Transform,Inverse_sub] auto-";
21.7 -reset_states ();
21.8 +States.reset ();
21.9 val fmz = ["filterExpression (X z = 3 / (z - 1/4 + - 1/8 * (1/(z::real))))",
21.10 "functionName X_z", "stepResponse (x[n::real]::bool)"];
21.11 val (dI, pI, mI) = ("Isac_Knowledge", ["Inverse", "Z_Transform", "SignalProcessing"],
21.12 @@ -190,7 +190,7 @@
21.13 moveActiveRoot 1;
21.14 autoCalculate 1 CompleteCalc;
21.15
21.16 -val ((pt,_),_) = get_calc 1; val p = get_pos 1 1;
21.17 +val ((pt,_),_) = States.get_calc 1; val p = States.get_pos 1 1;
21.18 val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
21.19 if UnparseC.term f = "X_z = 4 * (1 / 2) \<up> ?n * ?u [?n] + -4 * (- 1 / 4) \<up> ?n * ?u [?n]"
21.20 andalso p = ([], Res) then ()
22.1 --- a/test/Tools/isac/Knowledge/partial_fractions.sml Fri Sep 09 10:53:51 2022 +0200
22.2 +++ b/test/Tools/isac/Knowledge/partial_fractions.sml Sun Sep 11 14:31:15 2022 +0200
22.3 @@ -239,7 +239,7 @@
22.4 "----------- autoCalculate for met_partial_fraction -----";
22.5 "----------- autoCalculate for met_partial_fraction -----";
22.6 "----------- autoCalculate for met_partial_fraction -----";
22.7 -reset_states ();
22.8 +States.reset ();
22.9 val fmz =
22.10 ["functionTerm (3 / (z * (z - 1 / 4 + - 1 / 8 * (1 / z))))",
22.11 "solveFor z", "decomposedFunction p_p"];
22.12 @@ -252,7 +252,7 @@
22.13 moveActiveRoot 1;
22.14 autoCalculate 1 CompleteCalc;
22.15
22.16 -val ((pt,p),_) = get_calc 1; val ip = get_pos 1 1;
22.17 +val ((pt,p),_) = States.get_calc 1; val ip = States.get_pos 1 1;
22.18 if p = ip andalso ip = ([], Res) then ()
22.19 else error "autoCalculate for met_partial_fraction changed: final pos'";
22.20
22.21 @@ -409,7 +409,7 @@
22.22 "----------- isolate SubProblem [simplification, of_rationals, to_partial_fraction] auto -------";
22.23 "----------- isolate SubProblem [simplification, of_rationals, to_partial_fraction] auto -------";
22.24 "----------- isolate SubProblem [simplification, of_rationals, to_partial_fraction] auto -------";
22.25 -reset_states ();
22.26 +States.reset ();
22.27 (*val PblObj {fmz_from_Subproblem_of_Inverse_sub, ...} = get_obj I pt (fst p)
22.28 see --- test [SignalProcessing,Z_Transform,Inverse_sub] me = ";*)
22.29
23.1 --- a/test/Tools/isac/Knowledge/poly-2.sml Fri Sep 09 10:53:51 2022 +0200
23.2 +++ b/test/Tools/isac/Knowledge/poly-2.sml Sun Sep 11 14:31:15 2022 +0200
23.3 @@ -665,7 +665,7 @@
23.4 "-------- interSteps for Schalk 299a -----------------------------------------------------------";
23.5 "-------- interSteps for Schalk 299a -----------------------------------------------------------";
23.6 "-------- interSteps for Schalk 299a -----------------------------------------------------------";
23.7 -reset_states ();
23.8 +States.reset ();
23.9 CalcTree
23.10 [(["Term ((x - y)*(x + (y::real)))", "normalform N"],
23.11 ("Poly",["polynomial", "simplification"],
23.12 @@ -673,15 +673,15 @@
23.13 Iterator 1;
23.14 moveActiveRoot 1;
23.15 autoCalculate 1 CompleteCalc;
23.16 -val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
23.17 +val ((pt,p),_) = States.get_calc 1; Test_Tool.show_pt pt;
23.18
23.19 interSteps 1 ([1],Res)(*<ERROR> syserror in Detail_Step.go </ERROR>*);
23.20 -val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
23.21 +val ((pt,p),_) = States.get_calc 1; Test_Tool.show_pt pt;
23.22 if existpt' ([1,1], Frm) pt then ()
23.23 else error "poly.sml: interSteps doesnt work again 1";
23.24
23.25 interSteps 1 ([1,1],Res)(*<ERROR> syserror in Detail_Step.go </ERROR>*);
23.26 -val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
23.27 +val ((pt,p),_) = States.get_calc 1; Test_Tool.show_pt pt;
23.28 (*============ inhibit exn WN120316 ==============================================
23.29 if existpt' ([1,1,1], Frm) pt then ()
23.30 else error "poly.sml: interSteps doesnt work again 2";
24.1 --- a/test/Tools/isac/Knowledge/polyeq-2.sml Fri Sep 09 10:53:51 2022 +0200
24.2 +++ b/test/Tools/isac/Knowledge/polyeq-2.sml Sun Sep 11 14:31:15 2022 +0200
24.3 @@ -262,7 +262,7 @@
24.4 "----------- interSteps ([1],Res); on Schalk Is86Bsp5-------------";
24.5 "----------- interSteps ([1],Res); on Schalk Is86Bsp5-------------";
24.6 "----------- interSteps ([1],Res); on Schalk Is86Bsp5-------------";
24.7 -reset_states ();
24.8 +States.reset ();
24.9 CalcTree
24.10 [(["equality ((3::real)*x - 1 - (5*x - (2 - 4*x)) = - 11)", "solveFor x", "solutions L"],
24.11 ("PolyEq",["univariate", "equation"],["no_met"]))];
24.12 @@ -270,7 +270,7 @@
24.13 moveActiveRoot 1;
24.14
24.15 autoCalculate 1 CompleteCalc;
24.16 -val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
24.17 +val ((pt,p),_) = States.get_calc 1; Test_Tool.show_pt pt;
24.18 interSteps 1 ([1],Res)
24.19 (*BEFORE Isabelle2002 --> 2011: <ERROR> no Rewrite_Set... </ERROR> ?see fun prep_rls?*);
24.20
25.1 --- a/test/Tools/isac/Knowledge/polyminus.sml Fri Sep 09 10:53:51 2022 +0200
25.2 +++ b/test/Tools/isac/Knowledge/polyminus.sml Sun Sep 11 14:31:15 2022 +0200
25.3 @@ -371,66 +371,66 @@
25.4 "----------- pbl polynom vereinfachen p.33 -----------------------";
25.5 "----------- pbl polynom vereinfachen p.33 -----------------------";
25.6 "----------- 140 c ---";
25.7 -reset_states ();
25.8 +States.reset ();
25.9 CalcTree [(["Term (5*e + 6*f - 8*g - 9 - 7*e - 4*f + 10*g + 12)",
25.10 "normalform N"],
25.11 ("PolyMinus",["plus_minus", "polynom", "vereinfachen"],
25.12 ["simplification", "for_polynomials", "with_minus"]))];
25.13 moveActiveRoot 1;
25.14 autoCalculate 1 CompleteCalc;
25.15 -val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
25.16 +val ((pt,p),_) = States.get_calc 1; Test_Tool.show_pt pt;
25.17 if p = ([], Res) andalso
25.18 UnparseC.term (get_obj g_res pt (fst p)) = "3 - 2 * e + 2 * f + 2 * g"
25.19 then () else error "polyminus.sml: Vereinfache (3 - 2 * e + 2 * f...";
25.20
25.21 "======= 140 d ---";
25.22 -reset_states ();
25.23 +States.reset ();
25.24 CalcTree [(["Term (-r - 2*s - 3*t + 5 + 4*r + 8*s - 5*t - 2)",
25.25 "normalform N"],
25.26 ("PolyMinus",["plus_minus", "polynom", "vereinfachen"],
25.27 ["simplification", "for_polynomials", "with_minus"]))];
25.28 moveActiveRoot 1;
25.29 autoCalculate 1 CompleteCalc;
25.30 -val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
25.31 +val ((pt,p),_) = States.get_calc 1; Test_Tool.show_pt pt;
25.32 if p = ([], Res) andalso
25.33 UnparseC.term (get_obj g_res pt (fst p)) = "3 + 3 * r + 6 * s - 8 * t"
25.34 then () else error "polyminus.sml: Vereinfache 140 d)";
25.35
25.36 "======= 139 c ---";
25.37 -reset_states ();
25.38 +States.reset ();
25.39 CalcTree [(["Term (3*e - 6*f - 8*e - 4*f + 5*e + 7*f)",
25.40 "normalform N"],
25.41 ("PolyMinus",["plus_minus", "polynom", "vereinfachen"],
25.42 ["simplification", "for_polynomials", "with_minus"]))];
25.43 moveActiveRoot 1;
25.44 autoCalculate 1 CompleteCalc;
25.45 -val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
25.46 +val ((pt,p),_) = States.get_calc 1; Test_Tool.show_pt pt;
25.47 if p = ([], Res) andalso
25.48 UnparseC.term (get_obj g_res pt (fst p)) = "- (3 * f)"
25.49 then () else error "polyminus.sml: Vereinfache 139 c)";
25.50
25.51 "======= 139 b ---";
25.52 -reset_states ();
25.53 +States.reset ();
25.54 CalcTree [(["Term (8*u - 5*v - 5*u + 7*v - 6*u - 3*v)",
25.55 "normalform N"],
25.56 ("PolyMinus",["plus_minus", "polynom", "vereinfachen"],
25.57 ["simplification", "for_polynomials", "with_minus"]))];
25.58 moveActiveRoot 1;
25.59 autoCalculate 1 CompleteCalc;
25.60 -val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
25.61 +val ((pt,p),_) = States.get_calc 1; Test_Tool.show_pt pt;
25.62 if p = ([], Res) andalso
25.63 UnparseC.term (get_obj g_res pt (fst p)) = "- 3 * u - v"
25.64 then () else error "polyminus.sml: Vereinfache 139 b)";
25.65
25.66 "======= 138 a ---";
25.67 -reset_states ();
25.68 +States.reset ();
25.69 CalcTree [(["Term (2*u - 3*v - 6*u + 5*v)",
25.70 "normalform N"],
25.71 ("PolyMinus",["plus_minus", "polynom", "vereinfachen"],
25.72 ["simplification", "for_polynomials", "with_minus"]))];
25.73 moveActiveRoot 1;
25.74 autoCalculate 1 CompleteCalc;
25.75 -val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
25.76 +val ((pt,p),_) = States.get_calc 1; Test_Tool.show_pt pt;
25.77 if p = ([], Res) andalso
25.78 UnparseC.term (get_obj g_res pt (fst p)) = "- 4 * u + 2 * v"
25.79 then () else error "polyminus.sml: Vereinfache 138 a)";
25.80 @@ -451,7 +451,7 @@
25.81 "----------- pbl polynom probe -----------------------------------";
25.82 "----------- pbl polynom probe -----------------------------------";
25.83 "----------- pbl polynom probe -----------------------------------";
25.84 -reset_states ();
25.85 +States.reset ();
25.86 CalcTree [(["Pruefe ((5::int)*e + 6*f - 8*g - 9 - 7*e - 4*f + 10*g + 12 =\
25.87 \3 - 2 * e + 2 * f + 2 * (g::int))",
25.88 "mitWert [e = (1::int), f = (2::int), g = (3::int)]",
25.89 @@ -463,10 +463,10 @@
25.90 (* autoCalculate 1 CompleteCalcHead;
25.91 autoCalculate 1 (Steps 1);
25.92 autoCalculate 1 (Steps 1);
25.93 - val ((pt,p),_) = get_calc 1; UnparseC.term (get_obj g_res pt (fst p));
25.94 + val ((pt,p),_) = States.get_calc 1; UnparseC.term (get_obj g_res pt (fst p));
25.95 @@@@@WN081114 gives "??.empty", all "Pruefe" are the same,
25.96 although analogies work in interface.sml: FIXME.WN081114 in "Pruefe"*)
25.97 -val ((pt,p),_) = get_calc 1;
25.98 +val ((pt,p),_) = States.get_calc 1;
25.99 if p = ([], Res) andalso UnparseC.term (get_obj g_res pt (fst p)) = "11 = 11"
25.100 then () else error "polyminus.sml: Probe 11 = 11";
25.101 Test_Tool.show_pt pt;
25.102 @@ -475,21 +475,21 @@
25.103 "----------- pbl klammer polynom vereinfachen p.34 ---------------";
25.104 "----------- pbl klammer polynom vereinfachen p.34 ---------------";
25.105 "----------- pbl klammer polynom vereinfachen p.34 ---------------";
25.106 -reset_states ();
25.107 +States.reset ();
25.108 CalcTree [(["Term (2*u - 5 - (3 - 4*u) + (8*u + 9))",
25.109 "normalform N"],
25.110 ("PolyMinus",["klammer", "polynom", "vereinfachen"],
25.111 ["simplification", "for_polynomials", "with_parentheses"]))];
25.112 moveActiveRoot 1;
25.113 autoCalculate 1 CompleteCalc;
25.114 -val ((pt,p),_) = get_calc 1;
25.115 +val ((pt,p),_) = States.get_calc 1;
25.116 if p = ([], Res) andalso
25.117 UnparseC.term (get_obj g_res pt (fst p)) = "1 + 14 * u"
25.118 then () else error "polyminus.sml: Vereinfache (2*u - 5 - (3 - ...";
25.119 Test_Tool.show_pt pt;
25.120
25.121 "======= probe p.34 -----";
25.122 -reset_states ();
25.123 +States.reset ();
25.124 CalcTree [(["Pruefe (2*u - 5 - (3 - 4*u) + (8*u + 9) = 1 + 14 * (u::int))",
25.125 "mitWert [u = (2::int)]",
25.126 "Geprueft b"],
25.127 @@ -497,7 +497,7 @@
25.128 ["probe", "fuer_polynom"]))];
25.129 moveActiveRoot 1;
25.130 autoCalculate 1 CompleteCalc;
25.131 -val ((pt,p),_) = get_calc 1;
25.132 +val ((pt,p),_) = States.get_calc 1;
25.133 if p = ([], Res) andalso UnparseC.term (get_obj g_res pt (fst p)) = "29 = 29"
25.134 then () else error "polyminus.sml: Probe 29 = 29";
25.135 Test_Tool.show_pt pt;
25.136 @@ -506,7 +506,7 @@
25.137 "----------- try fun applyTactics --------------------------------";
25.138 "----------- try fun applyTactics --------------------------------";
25.139 "----------- try fun applyTactics --------------------------------";
25.140 -reset_states ();
25.141 +States.reset ();
25.142 CalcTree [(["Term (5*e + 6*f - 8*g - 9 - 7*e - 4*f + 10*g + 12)",
25.143 "normalform N"],
25.144 ("PolyMinus",["plus_minus", "polynom", "vereinfachen"],
25.145 @@ -515,12 +515,12 @@
25.146 autoCalculate 1 CompleteCalcHead;
25.147 autoCalculate 1 (Steps 1);
25.148 autoCalculate 1 (Steps 1);
25.149 -val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
25.150 +val ((pt,p),_) = States.get_calc 1; Test_Tool.show_pt pt;
25.151 "----- 1 \<up> ";
25.152 fetchApplicableTactics 1 0 p;
25.153 val appltacs = specific_from_prog pt p;
25.154 applyTactic 1 p (hd appltacs) (*addiere_x_plus_minus*);
25.155 -val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
25.156 +val ((pt,p),_) = States.get_calc 1; Test_Tool.show_pt pt;
25.157 "----- 2 \<up> ";
25.158 (*Rewrite.trace_on := true; ..stopped Test_Isac.thy*)
25.159 val erls = erls_ordne_alphabetisch;
25.160 @@ -540,25 +540,25 @@
25.161
25.162
25.163 applyTactic 1 p (hd (specific_from_prog pt p)) (*tausche_minus*);
25.164 -val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
25.165 +val ((pt,p),_) = States.get_calc 1; Test_Tool.show_pt pt;
25.166 "----- 3 \<up> ";
25.167 applyTactic 1 p (hd (specific_from_prog pt p)) (**);
25.168 -val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
25.169 +val ((pt,p),_) = States.get_calc 1; Test_Tool.show_pt pt;
25.170 "----- 4 \<up> ";
25.171 applyTactic 1 p (hd (specific_from_prog pt p)) (**);
25.172 -val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
25.173 +val ((pt,p),_) = States.get_calc 1; Test_Tool.show_pt pt;
25.174 "----- 5 \<up> ";
25.175 applyTactic 1 p (hd (specific_from_prog pt p)) (**);
25.176 -val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
25.177 +val ((pt,p),_) = States.get_calc 1; Test_Tool.show_pt pt;
25.178 "----- 6 \<up> ";
25.179
25.180 (*<CALCMESSAGE> failure </CALCMESSAGE>
25.181 applyTactic 1 p (hd (specific_from_prog pt p)) (**);
25.182 -val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
25.183 +val ((pt,p),_) = States.get_calc 1; Test_Tool.show_pt pt;
25.184 "----- 7 \<up> ";
25.185 *)
25.186 autoCalculate 1 CompleteCalc;
25.187 -val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
25.188 +val ((pt,p),_) = States.get_calc 1; Test_Tool.show_pt pt;
25.189 (*independent from failure above: met_simp_poly_minus not confluent:
25.190 (([9], Res), - (8 * g) + 10 * g + (3 - 2 * e + 2 * f)),
25.191 (([], Res), - (8 * g) + 10 * g + (3 - 2 * e + 2 * f))]
25.192 @@ -569,27 +569,27 @@
25.193
25.194
25.195 "#############################################################################";
25.196 -reset_states ();
25.197 +States.reset ();
25.198 CalcTree [(["Term (- (8 * g) + 10 * g + h)",
25.199 "normalform N"],
25.200 ("PolyMinus",["plus_minus", "polynom", "vereinfachen"],
25.201 ["simplification", "for_polynomials", "with_minus"]))];
25.202 moveActiveRoot 1;
25.203 autoCalculate 1 CompleteCalc;
25.204 -val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
25.205 +val ((pt,p),_) = States.get_calc 1; Test_Tool.show_pt pt;
25.206 if p = ([], Res) andalso UnparseC.term (get_obj g_res pt (fst p)) = "2 * g + h"
25.207 then () else error "polyminus.sml: addiere_vor_minus";
25.208
25.209
25.210 "#############################################################################";
25.211 -reset_states ();
25.212 +States.reset ();
25.213 CalcTree [(["Term (- (8 * g) + 10 * g + f)",
25.214 "normalform N"],
25.215 ("PolyMinus",["plus_minus", "polynom", "vereinfachen"],
25.216 ["simplification", "for_polynomials", "with_minus"]))];
25.217 moveActiveRoot 1;
25.218 autoCalculate 1 CompleteCalc;
25.219 -val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
25.220 +val ((pt,p),_) = States.get_calc 1; Test_Tool.show_pt pt;
25.221 if p = ([], Res) andalso UnparseC.term (get_obj g_res pt (fst p)) = "f + 2 * g"
25.222 then () else error "polyminus.sml: tausche_vor_plus";
25.223
25.224 @@ -627,14 +627,14 @@
25.225 *)
25.226
25.227 (*@@@@@@@*)
25.228 -reset_states ();
25.229 +States.reset ();
25.230 CalcTree [(["Term ((3*a + 2) * (4*a - 1))",
25.231 "normalform N"],
25.232 ("PolyMinus",["binom_klammer", "polynom", "vereinfachen"],
25.233 ["simplification", "for_polynomials", "with_parentheses_mult"]))];
25.234 moveActiveRoot 1;
25.235 autoCalculate 1 CompleteCalc;
25.236 -val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
25.237 +val ((pt,p),_) = States.get_calc 1; Test_Tool.show_pt pt;
25.238
25.239 if p = ([], Res) andalso
25.240 UnparseC.term (get_obj g_res pt (fst p)) =(*"- 2 + 12 * a \<up> 2 + 5 * a" with OLD numerals*)
25.241 @@ -644,13 +644,13 @@
25.242 "----------- pbl binom polynom vereinfachen: cube ----------------";
25.243 "----------- pbl binom polynom vereinfachen: cube ----------------";
25.244 "----------- pbl binom polynom vereinfachen: cube ----------------";
25.245 -reset_states ();
25.246 +States.reset ();
25.247 CalcTree [(["Term (8*(a - q) + a - 2*q + 3*(a - 2*q))", "normalform N"],
25.248 ("PolyMinus",["binom_klammer", "polynom", "vereinfachen"],
25.249 ["simplification", "for_polynomials", "with_parentheses_mult"]))];
25.250 moveActiveRoot 1;
25.251 autoCalculate 1 CompleteCalc;
25.252 -val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
25.253 +val ((pt,p),_) = States.get_calc 1; Test_Tool.show_pt pt;
25.254 if p = ([], Res) andalso UnparseC.term (get_obj g_res pt (fst p)) = "12 * a - 16 * q"
25.255 then () else error "pbl binom polynom vereinfachen: cube";
25.256
26.1 --- a/test/Tools/isac/Knowledge/rateq.sml Fri Sep 09 10:53:51 2022 +0200
26.2 +++ b/test/Tools/isac/Knowledge/rateq.sml Sun Sep 11 14:31:15 2022 +0200
26.3 @@ -52,7 +52,9 @@
26.4 "------------ solve (1/x = 5, x) by me ---------------------------";
26.5 "------------ solve (1/x = 5, x) by me ---------------------------";
26.6 val fmz = ["equality (1/x=(5::real))", "solveFor x", "solutions L"];
26.7 -val (dI',pI',mI') = ("RatEq",["univariate", "equation"],["no_met"]);
26.8 +val (dI',pI',mI') =
26.9 + ((** )"RatEq"( **)"PolyEq"(*rls "make_ratpoly_in" missing in theory "RatEq" (and ancestors)*),
26.10 + ["univariate", "equation"],["no_met"]);
26.11 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
26.12 (* val (p,_,f,nxt,_,pt) = me nxt p [1] pt;------------- now Refine_Tacitly*)
26.13 (* nxt = ("Model_Problem",Model_Problem ["rational", "univariate", "equation"]) *)
26.14 @@ -176,7 +178,9 @@
26.15 "------------ S.68, Bsp.: 40, ((x)/(x - 8) + (x - 8)/(x) = 26/5)--";
26.16 (*EP Schalk_II_p68_n40*)
26.17 val fmz = ["equality ((x)/(x - 8) + (x - 8)/(x) = 26/(5::real))", "solveFor x", "solutions L"];
26.18 -val (dI',pI',mI') = ("RatEq",["univariate", "equation"],["no_met"]);
26.19 +val (dI',pI',mI') =
26.20 + ((** )"RatEq"( **)"PolyEq"(*rls "make_ratpoly_in" missing in theory "RatEq" (and ancestors)*),
26.21 + ["univariate", "equation"],["no_met"]);
26.22 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
26.23 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
26.24 (* nxt = ("Model_Problem",Model_Problem ["rational", "univariate", "equation"])*)
26.25 @@ -228,7 +232,9 @@
26.26 (*ER-7*) (*Schalk I s.87 Bsp 55b*)
26.27 val fmz = ["equality (x/(x \<up> 2 - 6*x+9) - 1/(x \<up> 2 - 3*x) =1/x)",
26.28 "solveFor x", "solutions L"];
26.29 -val spec = ("RatEq",["univariate", "equation"],["no_met"]);
26.30 +val spec =
26.31 + ((** )"RatEq"( **)"PolyEq"(*rls "make_ratpoly_in" missing in theory "RatEq" (and ancestors)*),
26.32 + ["univariate", "equation"],["no_met"]);
26.33 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, spec)]; (* 0. specify-phase *)
26.34 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
26.35 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
26.36 @@ -322,7 +328,9 @@
26.37 "----------- ((5*x)/(x - 2) - x/(x+2)=(4::real)), incl. refine ---------------------------------";
26.38 (*was in test/../usecases.sml*)
26.39 val fmz = ["equality ((5*x)/(x - 2) - x/(x+2)=(4::real))", "solveFor x", "solutions L"];
26.40 -val (dI',pI',mI') = ("RatEq", ["univariate", "equation"], ["no_met"]);
26.41 +val (dI',pI',mI') =
26.42 + ((** )"RatEq"( **)"PolyEq"(*rls "make_ratpoly_in" missing in theory "RatEq" (and ancestors)*),
26.43 + ["univariate", "equation"],["no_met"]);
26.44 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
26.45 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
26.46 (**)val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;(**)
27.1 --- a/test/Tools/isac/Knowledge/rational-2.sml Fri Sep 09 10:53:51 2022 +0200
27.2 +++ b/test/Tools/isac/Knowledge/rational-2.sml Sun Sep 11 14:31:15 2022 +0200
27.3 @@ -1436,13 +1436,13 @@
27.4 "-------- interSteps ..Simp_Rat_Double_No- 1.xml ------------------------------";
27.5 "-------- interSteps ..Simp_Rat_Double_No- 1.xml ------------------------------";
27.6 "-------- interSteps ..Simp_Rat_Double_No- 1.xml ------------------------------";
27.7 -reset_states ();
27.8 +States.reset ();
27.9 CalcTree [(["Term (((2 - x)/(2*a)) / (2*a/(x - 2)))", "normalform N"],
27.10 ("Rational", ["rational", "simplification"], ["simplification", "of_rationals"]))];
27.11 Iterator 1;
27.12 moveActiveRoot 1;
27.13 autoCalculate 1 CompleteCalc;
27.14 -val ((pt, p), _) = get_calc 1;
27.15 +val ((pt, p), _) = States.get_calc 1;
27.16 (*
27.17 Test_Tool.show_pt pt;
27.18 [
27.19 @@ -1455,7 +1455,7 @@
27.20 (([], Res), (-4 + 4 * x + - 1 * x \<up> 2) / (4 * a \<up> 2))]
27.21 *)
27.22 interSteps 1 ([1], Res);
27.23 -val ((pt, p), _) = get_calc 1;
27.24 +val ((pt, p), _) = States.get_calc 1;
27.25 (*Test_Tool.show_pt pt;
27.26 [
27.27 (([], Frm), Simplify ((2 - x) / (2 * a) / (2 * a / (x - 2)))),
27.28 @@ -1481,13 +1481,13 @@
27.29 "-------- interSteps ..Simp_Rat_Cancel_No- 1.xml ------------------------------";
27.30 "-------- interSteps ..Simp_Rat_Cancel_No- 1.xml ------------------------------";
27.31 "-------- interSteps ..Simp_Rat_Cancel_No- 1.xml ------------------------------";
27.32 -reset_states ();
27.33 +States.reset ();
27.34 CalcTree [(["Term ((a \<up> 2 + - 1*b \<up> 2) / (a \<up> 2 + - 2*a*b + b \<up> 2))", "normalform N"],
27.35 ("Rational", ["rational", "simplification"], ["simplification", "of_rationals"]))];
27.36 Iterator 1;
27.37 moveActiveRoot 1;
27.38 autoCalculate 1 CompleteCalc;
27.39 -val ((pt, p), _) = get_calc 1;
27.40 +val ((pt, p), _) = States.get_calc 1;
27.41 (*Test_Tool.show_pt pt;
27.42 [
27.43 (([], Frm), Simplify ((a \<up> 2 + - 1 * b \<up> 2) / (a \<up> 2 + - 2 * a * b + b \<up> 2))),
27.44 @@ -1497,7 +1497,7 @@
27.45 (([], Res), (a + b) / (a + - 1 * b))]
27.46 *)
27.47 interSteps 1 ([2], Res);
27.48 -val ((pt, p), _) = get_calc 1;
27.49 +val ((pt, p), _) = States.get_calc 1;
27.50 (*Test_Tool.show_pt pt;
27.51 [
27.52 (([], Frm), Simplify ((a \<up> 2 + - 1 * b \<up> 2) / (a \<up> 2 + - 2 * a * b + b \<up> 2))),
27.53 @@ -1509,7 +1509,7 @@
27.54 (([], Res), (a + b) / (a + - 1 * b))]
27.55 *)
27.56 interSteps 1 ([2,1],Res);
27.57 -val ((pt, p), _) = get_calc 1;
27.58 +val ((pt, p), _) = States.get_calc 1;
27.59 (*Test_Tool.show_pt pt;
27.60 [
27.61 (([], Frm), Simplify ((a \<up> 2 + - 1 * b \<up> 2) / (a \<up> 2 + - 2 * a * b + b \<up> 2))),
27.62 @@ -1612,13 +1612,13 @@
27.63 "-------- several errpats in complicated term --------------------------------";
27.64 (*WN12xxxx TODO: instead of Gabriella's example here (27.Jul.12) find a simpler one
27.65 WN130912: kept this test, although not clear what for*)
27.66 -reset_states ();
27.67 +States.reset ();
27.68 CalcTree [(["Term ((5*b + 25)/(a^2 - b^2) * (a - b)/(5*b))", "normalform N"],
27.69 ("Rational", ["rational", "simplification"], ["simplification", "of_rationals"]))];
27.70 Iterator 1;
27.71 moveActiveRoot 1;
27.72 autoCalculate 1 CompleteCalc;
27.73 -val ((pt, p), _) = get_calc 1;
27.74 +val ((pt, p), _) = States.get_calc 1;
27.75 (*Test_Tool.show_pt pt;
27.76 [
27.77 (([], Frm), Simplify ((5 * b + 25) / (a \<up> 2 - b \<up> 2) * (a - b) / (5 * b))),
28.1 --- a/test/Tools/isac/Knowledge/simplify.sml Fri Sep 09 10:53:51 2022 +0200
28.2 +++ b/test/Tools/isac/Knowledge/simplify.sml Sun Sep 11 14:31:15 2022 +0200
28.3 @@ -23,14 +23,14 @@
28.4 "----------- CAS-command Simplify -----------------------";
28.5 "----------- CAS-command Simplify -----------------------";
28.6 "----------- CAS-command Simplify -----------------------";
28.7 - reset_states ();
28.8 + States.reset ();
28.9 CalcTree [([], References.empty)];
28.10 Iterator 1;
28.11 moveActiveRoot 1;
28.12 replaceFormula 1 "Simplify (2*a + 3*a)";
28.13 autoCalculate 1 (Steps 1);
28.14 autoCalculate 1 CompleteCalc;
28.15 - val ((pt,p),_) = get_calc 1;
28.16 + val ((pt,p),_) = States.get_calc 1;
28.17 val Form res = (#1 o ME_Misc.pt_extract) (pt, ([],Res)); Test_Tool.show_pt pt; UnparseC.term res;
28.18 if p = ([], Res) andalso UnparseC.term res = "5 * a" then ()
28.19 else error "simplify.sml: diff.behav. CAScmd: Simplify (2*a + 3*a)";
28.20 @@ -39,25 +39,25 @@
28.21 "----------- append inform with final result ------------";
28.22 "----------- append inform with final result ------------";
28.23 "----------- append inform with final result ------------";
28.24 -reset_states ();
28.25 +States.reset ();
28.26 CalcTree [(["Term ((14 * x * y) / ( x * y ))", "normalform N"],
28.27 ("Rational", ["rational", "simplification"], ["simplification", "of_rationals"]))];
28.28 Iterator 1;
28.29 moveActiveRoot 1;
28.30 autoCalculate 1 CompleteCalcHead;
28.31 -val ((pt,p),_) = get_calc 1;
28.32 +val ((pt,p),_) = States.get_calc 1;
28.33 Test_Tool.show_pt pt; (*[
28.34 (([], Frm), Simplify (14 * x * y / (x * y)))] *)
28.35 ME_Misc.pt_extract (pt, p); (*determines SOME (Apply_Method ["simplification", "of_rationals"])*)
28.36
28.37 (*/------------------- step into autoCalculate 1 (Steps 1) \<longrightarrow> Apply_Method ----------------\*)
28.38 "~~~~~ fun autoCalculate , args:"; val (cI, auto) = (1, Steps 1);
28.39 - val pold = get_pos cI 1
28.40 + val pold = States.get_pos cI 1
28.41
28.42 (** )val ("ok", [], (_, ([], Met))) = (*case*) ( *isa*)
28.43 (**)val ("ok", [], (_, ([1], Frm))) = (*case*) (*isa2*)
28.44 -Math_Engine.autocalc [] pold (get_calc cI) auto (*of*);
28.45 -"~~~~~ fun autocalc , args:"; val (c, ip, cs, (Solve.Steps s)) = ([], pold, (get_calc cI), auto);
28.46 +Math_Engine.autocalc [] pold (States.get_calc cI) auto (*of*);
28.47 +"~~~~~ fun autocalc , args:"; val (c, ip, cs, (Solve.Steps s)) = ([], pold, (States.get_calc cI), auto);
28.48 (*if*) s <= 1 (*then*);
28.49
28.50 (** ) val ("ok", ( (*isa*)
28.51 @@ -117,7 +117,7 @@
28.52 (*#### eval asms: "14 * x * y / (x * y) is_ratpolyexp = False" (*isa*)
28.53 True ( *isa2*)
28.54 (*\------------------- step into autoCalculate 1 (Steps 1) \<longrightarrow> Apply_Method ----------------/*)
28.55 -val ((pt,p),_) = get_calc 1;
28.56 +val ((pt,p),_) = States.get_calc 1;
28.57 Test_Tool.show_pt pt;
28.58 (*[
28.59 (([], Frm), Simplify (14 * x * y / (x * y))),
28.60 @@ -125,7 +125,7 @@
28.61
28.62 appendFormula 1 "14::real"
28.63 (* INPUT WITHOUT ^^^^^^^^ VARIABLES (WITH TYPE FROM ctxt) WOULD REQUIRE ADDITIONAL ATTENTION*);
28.64 -val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
28.65 +val ((pt,p),_) = States.get_calc 1; Test_Tool.show_pt pt;
28.66 (*[
28.67 (([], Frm), Simplify (14 * x * y / (x * y))),
28.68 (([1], Frm), 14 * x * y / (x * y)),
28.69 @@ -136,7 +136,7 @@
28.70 (([1], Res), 14)]*)
28.71
28.72 autoCalculate 1 (Steps 1);
28.73 -val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
28.74 +val ((pt,p),_) = States.get_calc 1; Test_Tool.show_pt pt;
28.75 (*[
28.76 (([], Frm), Simplify (14 * x * y / (x * y))),
28.77 (([1], Frm), 14 * x * y / (x * y)),
29.1 --- a/test/Tools/isac/MathEngBasic/ctree.sml Fri Sep 09 10:53:51 2022 +0200
29.2 +++ b/test/Tools/isac/MathEngBasic/ctree.sml Sun Sep 11 14:31:15 2022 +0200
29.3 @@ -381,7 +381,7 @@
29.4 "=====new ctree 2 miniscript with mini-subpbl ====================";
29.5 "=====new ctree 2 miniscript with mini-subpbl ====================";
29.6 "=====new ctree 2 miniscript with mini-subpbl ====================";
29.7 -reset_states ();
29.8 +States.reset ();
29.9 CalcTree [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
29.10 ("Test", ["sqroot-test", "univariate", "equation", "test"],
29.11 ["Test", "squ-equ-test-subpbl1"]))];
29.12 @@ -390,7 +390,7 @@
29.13
29.14 interSteps 1 ([3,2],Res);
29.15
29.16 - val ((pt,_),_) = get_calc 1;
29.17 + val ((pt,_),_) = States.get_calc 1;
29.18 Test_Tool.show_pt pt;
29.19
29.20 if (UnparseC.term o fst) (get_obj g_result pt [3,2,1]) = "x = 0 + 1" then ()
29.21 @@ -549,14 +549,14 @@
29.22 "=====new ctree 3 ================================================";
29.23 "=====new ctree 3 ================================================";
29.24
29.25 -reset_states ();
29.26 +States.reset ();
29.27 CalcTree [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
29.28 ("Test", ["sqroot-test", "univariate", "equation", "test"],
29.29 ["Test", "squ-equ-test-subpbl1"]))];
29.30 Iterator 1; moveActiveRoot 1;
29.31 autoCalculate 1 CompleteCalc;
29.32
29.33 - val ((pt,_),_) = get_calc 1;
29.34 + val ((pt,_),_) = States.get_calc 1;
29.35 Test_Tool.show_pt pt;
29.36
29.37 "-------------- move_dn ------------------------------------------";
29.38 @@ -584,7 +584,7 @@
29.39 "-------------- move_dn: Frm -> Res ------------------------------";
29.40 "-------------- move_dn: Frm -> Res ------------------------------";
29.41 "-------------- move_dn: Frm -> Res ------------------------------";
29.42 - reset_states ();
29.43 + States.reset ();
29.44 CalcTree (*start of calculation, return No.1*)
29.45 [(["equality (1+- 1*2+x=(0::real))", "solveFor x", "solutions L"],
29.46 ("Test",
29.47 @@ -593,19 +593,19 @@
29.48 Iterator 1; moveActiveRoot 1;
29.49 autoCalculate 1 CompleteCalcHead;
29.50 autoCalculate 1 (Steps 1);
29.51 - refFormula 1 (get_pos 1 1);
29.52 + refFormula 1 (States.get_pos 1 1);
29.53
29.54 moveActiveRoot 1;
29.55 moveActiveDown 1;
29.56 - if get_pos 1 1 = ([1], Frm) then ()
29.57 + if States.get_pos 1 1 = ([1], Frm) then ()
29.58 else error "ctree.sml: diff.behav. in move_dn: Frm -> Res (1)";
29.59 moveActiveDown 1; (*<ERROR> pos does not exist </ERROR>*)
29.60
29.61 autoCalculate 1 (Steps 1);
29.62 - refFormula 1 (get_pos 1 1);
29.63 + refFormula 1 (States.get_pos 1 1);
29.64
29.65 moveActiveDown 1; (*<ERROR> pos does not exist </ERROR>*)
29.66 - if get_pos 1 1 = ([1], Res) then ()
29.67 + if States.get_pos 1 1 = ([1], Res) then ()
29.68 else error "ctree.sml: diff.behav. in move_dn: Frm -> Res (1)";
29.69 moveActiveDown 1; (*<ERROR> pos does not exist </ERROR>*)
29.70
29.71 @@ -631,7 +631,7 @@
29.72 "------ move into detail -----------------------------------------";
29.73 "------ move into detail -----------------------------------------";
29.74 "------ move into detail -----------------------------------------";
29.75 - reset_states ();
29.76 + States.reset ();
29.77 CalcTree [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
29.78 ("Test", ["sqroot-test", "univariate", "equation", "test"],
29.79 ["Test", "squ-equ-test-subpbl1"]))];
29.80 @@ -641,12 +641,12 @@
29.81 moveActiveDown 1;
29.82 moveActiveDown 1;
29.83 moveActiveDown 1;
29.84 - refFormula 1 (get_pos 1 1) (* 2 Res, <ISA> - 1 + x = 0 </ISA> *);
29.85 + refFormula 1 (States.get_pos 1 1) (* 2 Res, <ISA> - 1 + x = 0 </ISA> *);
29.86
29.87 interSteps 1 ([2],Res);
29.88
29.89 - val ((pt,_),_) = get_calc 1; Test_Tool.show_pt pt;
29.90 - val p = get_pos 1 1;
29.91 + val ((pt,_),_) = States.get_calc 1; Test_Tool.show_pt pt;
29.92 + val p = States.get_pos 1 1;
29.93
29.94 val p = move_up [] pt p; (*([2, 6], Res)*);
29.95 val p = movelevel_up [] pt p;(*([2], Frm)*);
29.96 @@ -663,7 +663,7 @@
29.97 "=====new ctree 3a ===============================================";
29.98 "=====new ctree 3a ===============================================";
29.99 "=====new ctree 3a ===============================================";
29.100 - reset_states ();
29.101 + States.reset ();
29.102 CalcTree [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
29.103 ("Test", ["sqroot-test", "univariate", "equation", "test"],
29.104 ["Test", "squ-equ-test-subpbl1"]))];
29.105 @@ -672,7 +672,7 @@
29.106 autoCalculate 1 (Steps 1);
29.107 autoCalculate 1 (Steps 1);
29.108 autoCalculate 1 (Steps 1);
29.109 - val ((pt,_),_) = get_calc 1;
29.110 + val ((pt,_),_) = States.get_calc 1;
29.111 val p = move_dn [] pt ([],Pbl) (*-> ([1], Frm)*);
29.112 val p = move_dn [] pt ([1], Frm) (*-> ([1], Res)*);
29.113 val p = move_dn [] pt ([1], Res) (*-> ([2], Res)*);
29.114 @@ -696,7 +696,7 @@
29.115 "=====new ctree 4: crooked by cut_level_'_ =======================";
29.116 "=====new ctree 4: crooked by cut_level_'_ =======================";
29.117 "=====new ctree 4: crooked by cut_level_'_ =======================";
29.118 -reset_states ();
29.119 +States.reset ();
29.120 CalcTree
29.121 [(["equality (x/(x \<up> 2 - 6*x+9) - 1/(x \<up> 2 - 3*x) =1/x)",
29.122 "solveFor x", "solutions L"],
29.123 @@ -727,7 +727,7 @@
29.124
29.125 moveActiveFormula 1 ([4,2],Res)(*4.2.1.*);
29.126 interSteps 1 ([4,2],Res)(*..is activeFormula !?!*);
29.127 -val ((pt,_),_) = get_calc 1;
29.128 +val ((pt,_),_) = States.get_calc 1;
29.129 writeln(pr_ctree pr_short pt);
29.130 (*delete [4,1] in order to make pos [4],[4,4] for pblobjs differen [4],[4,3]:
29.131 ###########################################################################*)
29.132 @@ -912,13 +912,13 @@
29.133 "=====new ctree 5 minisubpbl =====================================";
29.134 "=====new ctree 5 minisubpbl =====================================";
29.135 "=====new ctree 5 minisubpbl =====================================";
29.136 -reset_states ();
29.137 +States.reset ();
29.138 CalcTree [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
29.139 ("Test", ["sqroot-test", "univariate", "equation", "test"],
29.140 ["Test", "squ-equ-test-subpbl1"]))];
29.141 Iterator 1; moveActiveRoot 1;
29.142 autoCalculate 1 CompleteCalc;
29.143 -val ((pt,_),_) = get_calc 1;
29.144 +val ((pt,_),_) = States.get_calc 1;
29.145 Test_Tool.show_pt pt;
29.146
29.147 "-------------- ME_Misc.pt_extract form, tac, asm ------------------------";
29.148 @@ -991,7 +991,7 @@
29.149 "=====new ctree 6 minisubpbl intersteps ==========================";
29.150 "=====new ctree 6 minisubpbl intersteps ==========================";
29.151 "=====new ctree 6 minisubpbl intersteps ==========================";
29.152 -reset_states ();
29.153 +States.reset ();
29.154 CalcTree [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
29.155 ("Test", ["sqroot-test", "univariate", "equation", "test"],
29.156 ["Test", "squ-equ-test-subpbl1"]))];
29.157 @@ -999,7 +999,7 @@
29.158 autoCalculate 1 CompleteCalc;
29.159 interSteps 1 ([2],Res);
29.160 interSteps 1 ([3,2],Res);
29.161 -val ((pt,_),_) = get_calc 1;
29.162 +val ((pt,_),_) = States.get_calc 1;
29.163 Test_Tool.show_pt pt;
29.164
29.165 (**##############################################################**)
30.1 --- a/test/Tools/isac/MathEngine/detail-step.sml Fri Sep 09 10:53:51 2022 +0200
30.2 +++ b/test/Tools/isac/MathEngine/detail-step.sml Sun Sep 11 14:31:15 2022 +0200
30.3 @@ -14,7 +14,7 @@
30.4 "----------- interSteps [diff,integration] -----------------------------------------------------";
30.5 "----------- interSteps [diff,integration] -----------------------------------------------------";
30.6 "----------- interSteps [diff,integration] -----------------------------------------------------";
30.7 -reset_states ();
30.8 +States.reset ();
30.9 CalcTree
30.10 [(["functionTerm (x^2 + 1)", "integrateBy x", "antiDerivative FF"],
30.11 ("Integrate", ["integrate", "function"], ["diff", "integration"]))];
30.12 @@ -22,12 +22,12 @@
30.13 moveActiveRoot 1;
30.14 autoCalculate 1 CompleteCalc;
30.15 interSteps 1 ([1], Res);
30.16 -val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
30.17 +val ((pt,p),_) = States.get_calc 1; Test_Tool.show_pt pt;
30.18 if existpt' ([1, 3], Res) pt then ()
30.19 else error "integrate.sml: interSteps on Rewrite_Set_Inst";
30.20
30.21 "----------------------------------------------------------------------------------------------";
30.22 -reset_states ();
30.23 +States.reset ();
30.24 CalcTree
30.25 [(["functionTerm (Integral x^2 + 1 D x)", "integrateBy x", "antiDerivative FF"],
30.26 ("Integrate", ["integrate", "function"], ["diff", "integration", "test"]))];
30.27 @@ -49,7 +49,7 @@
30.28 autoCalculate 1 (Steps 1);
30.29
30.30 autoCalculate 1 CompleteCalc;
30.31 -val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
30.32 +val ((pt,p),_) = States.get_calc 1; Test_Tool.show_pt pt;
30.33 val (Form t,_,_) = ME_Misc.pt_extract (pt, p); UnparseC.term t;
30.34 if existpt' ([3], Res) pt andalso UnparseC.term t = "c + x + 1 / 3 * x \<up> 3" then ()
30.35 else error "integrate.sml: test-script doesnt work";
31.1 --- a/test/Tools/isac/MathEngine/mathengine-stateless.sml Fri Sep 09 10:53:51 2022 +0200
31.2 +++ b/test/Tools/isac/MathEngine/mathengine-stateless.sml Sun Sep 11 14:31:15 2022 +0200
31.3 @@ -33,7 +33,7 @@
31.4 "----------- tryrefine ----------------------------------";
31.5 "----------- tryrefine ----------------------------------";
31.6 "----------- tryrefine ----------------------------------";
31.7 -reset_states ();
31.8 +States.reset ();
31.9 CalcTree [(["equality (x/(x^2 - 6*x+9) - 1/(x^2 - 3*x) =1/x)",
31.10 "solveFor x", "solutions L"],
31.11 ("RatEq",["univariate", "equation"],["no_met"]))];
31.12 @@ -143,7 +143,7 @@
31.13 "----------- identified error in fun getTactic, ThmC.string_of_thm ---------------";
31.14 "----------- identified error in fun getTactic, ThmC.string_of_thm ---------------";
31.15 "----------- identified error in fun getTactic, ThmC.string_of_thm ---------------";
31.16 -reset_states ();
31.17 +States.reset ();
31.18 CalcTree [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
31.19 ("Test",["sqroot-test", "univariate", "equation", "test"],["Test", "squ-equ-test-subpbl1"]))];
31.20 moveActiveRoot 1;
31.21 @@ -154,7 +154,7 @@
31.22 getTactic 1 ([1],Frm); (*<RULESET> norm_equation </RULESET>*)
31.23 interSteps 1 ([1],Res);
31.24 "~~~~~ fun interSteps, args:"; val (cI, ip) = (1, ([1],Res));
31.25 -val ((pt,p), tacis) = get_calc cI;
31.26 +val ((pt,p), tacis) = States.get_calc cI;
31.27 (not o is_interpos) ip = false;
31.28 val ip' = lev_pred' pt ip;
31.29 "~~~~~ fun go, args:"; val (pt, (pos as (p,p_):pos')) = (pt, ip);
31.30 @@ -236,7 +236,7 @@
31.31 (* HERE THE ERROR OCCURED IN THE FIRST APPROACH
31.32 getTactic 1 ([1,1],Frm); <ERROR> syserror in getTactic </ERROR> <<<<<=========================*)
31.33 "~~~~~ fun getTactic, args:"; val (cI, (p:pos')) = (1, ([1,1],Frm));
31.34 -val ((pt,_),_) = get_calc cI
31.35 +val ((pt,_),_) = States.get_calc cI
31.36 val (form, tac, asms) = ME_Misc.pt_extract (pt, p)
31.37 val SOME ta = tac;
31.38 "~~~~~ fun gettacticOK2xml, args:"; val ((cI:calcID), tac) = (cI, ta);
31.39 @@ -266,15 +266,15 @@
31.40 "----------- improved fun getTactic for interSteps and numeral calculations --";
31.41 "----------- improved fun getTactic for interSteps and numeral calculations --";
31.42 val ctxt = Proof_Context.init_global @{theory Test};
31.43 -reset_states (); val cI = 1;
31.44 +States.reset (); val cI = 1;
31.45 CalcTree [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
31.46 ("Test",["sqroot-test", "univariate", "equation", "test"],["Test", "squ-equ-test-subpbl1"]))];
31.47 moveActiveRoot 1;
31.48 autoCalculate 1 CompleteCalcHead;
31.49 autoCalculate 1 (Steps 1);
31.50
31.51 - val cs = get_calc cI (* we improve from the calcstate here [*] *);
31.52 - val pos as (_,p_) = get_pos cI 1 (* we improve from the calcstate here [*] *);
31.53 + val cs = States.get_calc cI (* we improve from the calcstate here [*] *);
31.54 + val pos as (_,p_) = States.get_pos cI 1 (* we improve from the calcstate here [*] *);
31.55
31.56 appendFormula 1 "x + 4 + -3 = 2" (*|> Future.join*);
31.57 interSteps 1 ([1],Res); (* already done by appendFormula, now showed to frontend *)
31.58 @@ -282,7 +282,7 @@
31.59 (*<ID> sym_#add_Float ((~3,0), (0,0)) __ ((4,0), (0,0)) </ID> <<<<<================== to improve
31.60 <ISA> 1 + x = -3 + (4 + x) </ISA>*)
31.61
31.62 -val ((pt''',p'''), tacis''') = get_calc cI;
31.63 +val ((pt''',p'''), tacis''') = States.get_calc cI;
31.64 Test_Tool.show_pt pt'''
31.65 (*[
31.66 (([], Frm), solve (x + 1 = 2, x)),
31.67 @@ -295,8 +295,8 @@
31.68 (([1], Res), x + 4 + -3 = 2)]*)
31.69 ;
31.70 "~~~~~ fun appendFormula', args:"; val (cI, ifo) = (1, "x + 4 + -3 = 2");
31.71 -(* val cs = get_calc cI (* we improve from the calcstate here [*] *);
31.72 - val pos as (_,p_) = get_pos cI 1 (* we improve from the calcstate here [*] *);*)
31.73 +(* val cs = States.get_calc cI (* we improve from the calcstate here [*] *);
31.74 + val pos as (_,p_) = States.get_pos cI 1 (* we improve from the calcstate here [*] *);*)
31.75 val ("ok", cs' as (_, _, ptp')) = Step.do_next pos cs;
31.76 (*val ("ok", (_, c, ptp as (_,p))) = *)Step_Solve.by_term ptp' (encode ifo);
31.77 "~~~~~ fun Step_Solve.by_term , args:"; val (cs as (_, _, ptp as (pt, pos as (p, p_))), istr) =
32.1 --- a/test/Tools/isac/MathEngine/me-misc.sml Fri Sep 09 10:53:51 2022 +0200
32.2 +++ b/test/Tools/isac/MathEngine/me-misc.sml Sun Sep 11 14:31:15 2022 +0200
32.3 @@ -14,7 +14,7 @@
32.4 "----------- fun get_interval after replace} other 2 -------------------------------------------";
32.5 "----------- fun get_interval after replace} other 2 -------------------------------------------";
32.6 "----------- fun get_interval after replace} other 2 -------------------------------------------";
32.7 -reset_states ();
32.8 +States.reset ();
32.9 CalcTree [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
32.10 ("Test", ["sqroot-test", "univariate", "equation", "test"],
32.11 ["Test", "squ-equ-test-subpbl1"]))];
32.12 @@ -25,7 +25,7 @@
32.13 replaceFormula 1 "x = 1";
32.14 (*... returns calcChangedEvent with ...*)
32.15 val (unc, del, gen) = (([1],Res), ([4],Res), ([3,2],Res));
32.16 - val ((pt,_),_) = get_calc 1;
32.17 + val ((pt,_),_) = States.get_calc 1;
32.18
32.19 (*default_print_depth 99*)map fst3 (ME_Misc.get_interval ([],Pbl) ([],Res) 9999 pt);(*default_print_depth 3*)
32.20 if map fst3 (ME_Misc.get_interval ([],Pbl) ([],Res) 9999 pt) =
33.1 --- a/test/Tools/isac/MathEngine/solve.sml Fri Sep 09 10:53:51 2022 +0200
33.2 +++ b/test/Tools/isac/MathEngine/solve.sml Sun Sep 11 14:31:15 2022 +0200
33.3 @@ -37,12 +37,12 @@
33.4 "--------- interSteps on norm_Rational ---------------------------";
33.5 "--------- interSteps on norm_Rational ---------------------------";
33.6 "--------- interSteps on norm_Rational ---------------------------";
33.7 -reset_states (); (*exp_IsacCore_Simp_Rat_Double_No-7.xml*)
33.8 +States.reset (); (*exp_IsacCore_Simp_Rat_Double_No-7.xml*)
33.9 CalcTree [(["Term ((2/(x+3) + 2/(x - 3)) / (8*x/(x \<up> 2 - 9)))", "normalform N"],
33.10 ("Rational", ["rational", "simplification"], ["simplification", "of_rationals"]))];
33.11 moveActiveRoot 1;
33.12 autoCalculate 1 CompleteCalc;
33.13 -val ((pt, _), _) = get_calc 1; Test_Tool.show_pt pt;
33.14 +val ((pt, _), _) = States.get_calc 1; Test_Tool.show_pt pt;
33.15 case pt of Nd (PblObj _, [Nd _, Nd _, Nd _, Nd _, Nd _, Nd _]) => ()
33.16 | _ => error "solve.sml: interSteps on norm_Rational 1";
33.17 interSteps 1 ([6], Res);
33.18 @@ -51,7 +51,7 @@
33.19 interSteps 1 ([6,1], Res) (*... here get the intermediate steps above*);
33.20
33.21 getTactic 1 ([6,1,1], Frm); (*WN130909 <ERROR> syserror in getTactic </ERROR>*)
33.22 -val ((pt,_),_) = get_calc 1; Test_Tool.show_pt pt;
33.23 +val ((pt,_),_) = States.get_calc 1; Test_Tool.show_pt pt;
33.24 val (Form form, SOME tac, asm) = ME_Misc.pt_extract (pt, ([6], Res));
33.25 case (UnparseC.term form, tac, UnparseC.terms_to_strings asm) of
33.26 ("1 / 2", Check_Postcond ["rational", "simplification"], []) => ()
34.1 --- a/test/Tools/isac/MathEngine/states.sml Fri Sep 09 10:53:51 2022 +0200
34.2 +++ b/test/Tools/isac/MathEngine/states.sml Sun Sep 11 14:31:15 2022 +0200
34.3 @@ -32,7 +32,7 @@
34.4
34.5 (* run n calculations in parallel, return measured time *)
34.6 fun test n = let
34.7 - val _ = reset_states ();
34.8 + val _ = States.reset ();
34.9 fun add_calc i = (CalcTree ex; moveActiveRoot i; i);
34.10 val ls = gen_ls n |> map add_calc;
34.11 fun auto_calc i = autoCalculate i CompleteCalc;
34.12 @@ -40,7 +40,7 @@
34.13 val _ = map auto_calc ls (*|> map Future.join*);
34.14 val t2 = Time.now ();
34.15 fun check i = let
34.16 - val ((pt, p), _) = get_calc i; (*retrieve result, e.g. no.1*)
34.17 + val ((pt, p), _) = States.get_calc i; (*retrieve result, e.g. no.1*)
34.18 in
34.19 if p = ([], Res) andalso UnparseC.term (get_obj g_res pt (fst p)) =(*check result correct*)
34.20 "y x =\n-6 * q_0 * L \<up> 2 / (-24 * EI) * x \<up> 2 +\n4 * L * q_0 / " ^
35.1 --- a/test/Tools/isac/MathEngine/step.sml Fri Sep 09 10:53:51 2022 +0200
35.2 +++ b/test/Tools/isac/MathEngine/step.sml Sun Sep 11 14:31:15 2022 +0200
35.3 @@ -173,7 +173,7 @@
35.4 "--------- embed fun Step.inconsistent -------------------";
35.5 "--------- embed fun Step.inconsistent -------------------";
35.6 "--------- embed fun Step.inconsistent -------------------";
35.7 -reset_states ();
35.8 +States.reset ();
35.9 CalcTree
35.10 [(["functionTerm (x ^ 2 + sin (x ^ 4))", "differentiateFor x", "derivative f_f'"],
35.11 ("Isac_Knowledge", ["derivative_of", "function"], ["diff", "differentiate_on_R"]))];
35.12 @@ -194,8 +194,8 @@
35.13
35.14 "~~~~~ fun requestFillformula, args:"; val (cI, (errpatID, fillpatID)) =
35.15 (1, ("chain-rule-diff-both", "fill-both-args"));
35.16 - val ((pt, _), _) = get_calc cI
35.17 - val pos as (p, _) = get_pos cI 1;
35.18 + val ((pt, _), _) = States.get_calc cI
35.19 + val pos as (p, _) = States.get_pos cI 1;
35.20 val fillforms = Error_Pattern.find_fill_patterns (pt, pos) errpatID;
35.21
35.22 if pos = ([1], Res) then () else error "Step.inconsistent changed 1";
35.23 @@ -229,11 +229,11 @@
35.24 "~~~~~ to requestFillformula return val:"; val (pt, pos') = (pt, pos');
35.25 (*val (pt, pos') = Step.inconsistent (sube_opt, thm'_of_thm thm)
35.26 (fillform, []) (get_loc pt pos) pos' pt*)
35.27 -upd_calc cI ((pt, pos'), []); upd_ipos cI 1 pos';
35.28 +States.upd_calc cI ((pt, pos'), []); States.upd_ipos cI 1 pos';
35.29
35.30 "~~~~~ final check:";
35.31 -val ((pt, _),_) = get_calc 1;
35.32 -val p = get_pos 1 1;
35.33 +val ((pt, _),_) = States.get_calc 1;
35.34 +val p = States.get_pos 1 1;
35.35 val (Form f, _, asms) = ME_Misc.pt_extract (pt, p);
35.36 if p = ([2], Res) andalso
35.37 get_obj g_tac pt (fst p) = Rewrite_Inst (["(''bdv'', x)"], ("diff_sin_chain", "")) andalso
36.1 --- a/test/Tools/isac/Minisubpbl/700-interSteps.sml Fri Sep 09 10:53:51 2022 +0200
36.2 +++ b/test/Tools/isac/Minisubpbl/700-interSteps.sml Sun Sep 11 14:31:15 2022 +0200
36.3 @@ -7,7 +7,7 @@
36.4 "----------- Minisubplb/700-interSteps.sml -----------------------";
36.5 (** adaption from rewtools.sml --- initContext..Ptool.Thy_, fun context_thm ---,
36.6 *into a functional representation, i.e. we outcomment statements with side-effects:
36.7 - ** reset_states ();
36.8 + ** States.reset ();
36.9 ** CalcTree [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
36.10 ** ("Test", ["sqroot-test", "univariate", "equation", "test"],
36.11 ** ["Test", "squ-equ-test-subpbl1"]))];
36.12 @@ -52,12 +52,12 @@
36.13 (** val p = ([], Res);
36.14 ** initContext 1 Ptool.Thy_ p
36.15 *** = <MESSAGE><CALCID>1</CALCID><STRING>no thy-context at result</STRING></MESSAGE>: XML.tree;
36.16 - ** val ((pt,_),_) = get_calc 1; (* 11 lines with subpbl *)
36.17 + ** val ((pt,_),_) = States.get_calc 1; (* 11 lines with subpbl *)
36.18 **
36.19 ** interSteps 1 ([2], Res); (* added [2,1]..[2,6] *)
36.20 **)
36.21 "~~~~~ fun interSteps, args:"; val (cI, ip) = (1, ([2], Res));
36.22 -(** val ((pt, p), tacis) = get_calc cI;*)
36.23 +(** val ((pt, p), tacis) = States.get_calc cI;*)
36.24 val ip' = lev_pred' pt ip;
36.25
36.26 (*+*)ip = ([2], Res);
36.27 @@ -142,7 +142,7 @@
36.28 ** interSteps 1 ([3,1], Res);
36.29 **)
36.30 "~~~~~ fun interSteps, args:"; val (cI, ip) = (1, ([3,1], Res));
36.31 -(**val ((pt, p), tacis) = get_calc cI;*)
36.32 +(**val ((pt, p), tacis) = States.get_calc cI;*)
36.33 val ip' = lev_pred' pt ip;
36.34
36.35 (*+*)ip = ([3, 1], Res);
37.1 --- a/test/Tools/isac/Minisubpbl/800-append-on-Frm.sml Fri Sep 09 10:53:51 2022 +0200
37.2 +++ b/test/Tools/isac/Minisubpbl/800-append-on-Frm.sml Sun Sep 11 14:31:15 2022 +0200
37.3 @@ -32,8 +32,8 @@
37.4
37.5 (*appendFormula 1 "2+ - 1 + x = 2";*)
37.6 "~~~~~ fun appendFormula , args:"; val (ifo) = ("2+ - 1 + x = 2");
37.7 - val cs = (*get_calc cI*) ((pt, p), []) (*..continue fun me*)
37.8 - val pos = (*get_pos cI 1*) p (*..continue fun me*)
37.9 + val cs = (*States.get_calc cI*) ((pt, p), []) (*..continue fun me*)
37.10 + val pos = (*States.get_pos cI 1*) p (*..continue fun me*)
37.11
37.12 val ("ok", cs' as (_, _, ptp''''')) = (*case*)
37.13 Step.do_next pos cs (*of*);
38.1 --- a/test/Tools/isac/OLDTESTS/tacis.sml Fri Sep 09 10:53:51 2022 +0200
38.2 +++ b/test/Tools/isac/OLDTESTS/tacis.sml Sun Sep 11 14:31:15 2022 +0200
38.3 @@ -12,67 +12,67 @@
38.4 "------ fetchProposedTactic -> autoCalculate (Step1 ) ------------";
38.5 "------ fetchProposedTactic -> autoCalculate (Step1 ) ------------";
38.6 "------ fetchProposedTactic -> autoCalculate (Step1 ) ------------";
38.7 - reset_states ();
38.8 + States.reset ();
38.9 CalcTree [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
38.10 ("Test", ["sqroot-test", "univariate", "equation", "test"],
38.11 ["Test", "squ-equ-test-subpbl1"]))];
38.12 Iterator 1; moveActiveRoot 1;
38.13 autoCalculate 1 CompleteCalcHead;
38.14 - autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1) (*x + 1 = 2*);
38.15 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1) (*x + 1 = 2*);
38.16
38.17 fetchProposedTactic 1 (*'Rewrite_Set norm_equation' in tacis*);
38.18 - autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1) (*x + 1 + -1 * 2 = 0*);
38.19 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1) (*x + 1 + -1 * 2 = 0*);
38.20
38.21 fetchProposedTactic 1 (*'Rewrite_Set Test_simplify' in tacis*);
38.22 - autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1) (*-1 + x = 0*);
38.23 - val ((pt,_),_) = get_calc 1;
38.24 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1) (*-1 + x = 0*);
38.25 + val ((pt,_),_) = States.get_calc 1;
38.26 val str = pr_ctree pr_short pt;
38.27 writeln str;
38.28
38.29 fetchProposedTactic 1 (*'Subproblem ...' in tacis*);
38.30 - autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1) (*solve (-1 + x = 0,x)*);
38.31 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1) (*solve (-1 + x = 0,x)*);
38.32
38.33 fetchProposedTactic 1 (*'Model_Problem' in tacis*);
38.34 - autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1) (*equality ///*);
38.35 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1) (*equality ///*);
38.36 (*----- WN060222 since complete_mod_ case cas of SOME headline -----
38.37 fetchProposedTactic 1 (*'Add_Given equality (-1 + x = 0)' in tacis*);
38.38 - autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1) (*equality (-1 + x =0)*);
38.39 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1) (*equality (-1 + x =0)*);
38.40 ---------------------------------------------------------------------*)
38.41
38.42 fetchProposedTactic 1 (*'Add_Given solveFor x' in tacis*);
38.43 (*----- WN060222 since complete_mod_ case cas of SOME headline:
38.44 (*Specify_Theory Test.thy*)
38.45 ---------------------------------------------------------------------*)
38.46 - autoCalculate 1 CompleteCalcHead; refFormula 1 (get_pos 1 1) (*OK*);
38.47 + autoCalculate 1 CompleteCalcHead; refFormula 1 (States.get_pos 1 1) (*OK*);
38.48 (*###########################################autoCalculate 1 (Steps 1);*)
38.49 fetchProposedTactic 1 (*'Apply_Method Test solve_linear' in tacis*);
38.50 (* there was the only error \<up> \<up> \<up> in step/begin_end_prog ..Apply_Method..
38.51 val (str', (tacis', (pt',p'))) = Step.do_next ip (ptp, tacis);
38.52 writeln (State_Steps.to_string tacis');
38.53 ######################################################################*)
38.54 - autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1) (*-1 + x = 0*);
38.55 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1) (*-1 + x = 0*);
38.56
38.57 fetchProposedTactic 1 (*'Rewrite_Set_Inst isolate_bdv' in tacis*);
38.58 - autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1) (*x = 0 + -1 * -1*);
38.59 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1) (*x = 0 + -1 * -1*);
38.60
38.61 fetchProposedTactic 1 (*'Rewrite_Set Test_simplify' in tacis*);
38.62 - autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1) (*x = 1*);
38.63 - val ((pt,_),_) = get_calc 1;
38.64 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1) (*x = 1*);
38.65 + val ((pt,_),_) = States.get_calc 1;
38.66 val str = pr_ctree pr_short pt;
38.67 writeln str;
38.68
38.69 fetchProposedTactic 1 (*'Check_Postcond linear...' in tacis*);
38.70 - autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1) (*[x = 1]*);
38.71 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1) (*[x = 1]*);
38.72
38.73 fetchProposedTactic 1 (*'Check_elementwise Assumptions' in tacis*);
38.74 - autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1) (*[x = 1]*);
38.75 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1) (*[x = 1]*);
38.76
38.77 fetchProposedTactic 1 (*'Check_Postcond sqroot-test...' in tacis*);
38.78 - autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1) (*[x = 1]*);
38.79 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1) (*[x = 1]*);
38.80
38.81 fetchProposedTactic 1 (*'' in tacis*);
38.82 - val ((pt,p),tacis) = get_calc 1;
38.83 - val ip = get_pos 1 1;
38.84 + val ((pt,p),tacis) = States.get_calc 1;
38.85 + val ip = States.get_pos 1 1;
38.86 val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
38.87 if UnparseC.term f = "[x = 1]"andalso p = ([],Res) andalso ip = ([],Res)then()else
38.88 error "tacis.sml: diff.behav. in fetchProposedTactic autoCalculate";
38.89 @@ -82,77 +82,77 @@
38.90 "------ setNextTactic -> autoCalculate (Step1 ) ------------------";
38.91 "------ setNextTactic -> autoCalculate (Step1 ) ------------------";
38.92 "------ setNextTactic -> autoCalculate (Step1 ) ------------------";
38.93 - reset_states ();
38.94 + States.reset ();
38.95 CalcTree [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
38.96 ("Test", ["sqroot-test", "univariate", "equation", "test"],
38.97 ["Test", "squ-equ-test-subpbl1"]))];
38.98 Iterator 1; moveActiveRoot 1;
38.99 autoCalculate 1 CompleteCalcHead;
38.100 - autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1) (*x + 1 = 2*);
38.101 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1) (*x + 1 = 2*);
38.102
38.103 setNextTactic 1 (Rewrite_Set "norm_equation");
38.104 - val (_, tacis) = get_calc 1;
38.105 + val (_, tacis) = States.get_calc 1;
38.106 case tacis of [(Rewrite_Set "norm_equation",_,(([1], Res), _))] => () | _ =>
38.107 error "tacis.sml: diff.behav. in setNextTactic -> autoCalculate (1)";
38.108 - autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1) (*x + 1 + -1 * 2 = 0*);
38.109 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1) (*x + 1 + -1 * 2 = 0*);
38.110
38.111 setNextTactic 1 (Rewrite_Set "Test_simplify");
38.112 - autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1) (*-1 + x = 0*);
38.113 - val ((pt,_),_) = get_calc 1;
38.114 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1) (*-1 + x = 0*);
38.115 + val ((pt,_),_) = States.get_calc 1;
38.116 val str = pr_ctree pr_short pt;
38.117 writeln str;
38.118
38.119 setNextTactic 1 (Subproblem ("Test",["LINEAR", "univariate",
38.120 "equation", "test"]));
38.121 - autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1) (*solve (-1 + x = 0, x)*);
38.122 - val ((pt,_),_) = get_calc 1;
38.123 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1) (*solve (-1 + x = 0, x)*);
38.124 + val ((pt,_),_) = States.get_calc 1;
38.125 val str = pr_ctree pr_short pt;
38.126 writeln str;
38.127
38.128 setNextTactic 1 (Model_Problem (*["LINEAR", "univariate", "equation", "test"]*));
38.129 - autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1) (*equality ///*);
38.130 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1) (*equality ///*);
38.131
38.132 setNextTactic 1 (Add_Given "equality (-1 + x = 0)");
38.133 - autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1) (*equality (-1 + x = 0)*);
38.134 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1) (*equality (-1 + x = 0)*);
38.135
38.136 setNextTactic 1 (Add_Given "solveFor x");
38.137 - autoCalculate 1 CompleteCalcHead; refFormula 1 (get_pos 1 1) (*OK*);
38.138 + autoCalculate 1 CompleteCalcHead; refFormula 1 (States.get_pos 1 1) (*OK*);
38.139
38.140 setNextTactic 1 (Apply_Method ["Test", "solve_linear"]);
38.141 - val (_, tacis) = get_calc 1;
38.142 + val (_, tacis) = States.get_calc 1;
38.143 case tacis of
38.144 [((Apply_Method ["Test", "solve_linear"],_,(([3,1], Frm), _)))] =>() | _ =>
38.145 error "tacis.sml: diff.behav. in setNextTactic -> autoCalculate (2)";
38.146 (*#######################################################################*)
38.147 - autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1) (*-1 + x = 0*);
38.148 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1) (*-1 + x = 0*);
38.149
38.150 setNextTactic 1 (Rewrite_Set_Inst (["(''bdv'',x)"], "isolate_bdv"));
38.151 - autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1) (*x = 0 + -1 * -1*);
38.152 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1) (*x = 0 + -1 * -1*);
38.153
38.154 setNextTactic 1 (Rewrite_Set "Test_simplify");
38.155 - autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1) (*x = 1*);
38.156 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1) (*x = 1*);
38.157
38.158 setNextTactic 1 (Check_Postcond ["LINEAR", "univariate", "equation", "test"]);
38.159 - autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1) (*[x = 1]*);
38.160 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1) (*[x = 1]*);
38.161
38.162 setNextTactic 1 (Check_elementwise "Assumptions");
38.163 - autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1) (*[x = 1]*);
38.164 - val ((pt,_),_) = get_calc 1;
38.165 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1) (*[x = 1]*);
38.166 + val ((pt,_),_) = States.get_calc 1;
38.167 val str = pr_ctree pr_short pt;
38.168 writeln str;
38.169
38.170 setNextTactic 1 (Check_Postcond
38.171 ["sqroot-test", "univariate", "equation", "test"]);
38.172 - val (_, tacis) = get_calc 1;
38.173 + val (_, tacis) = States.get_calc 1;
38.174
38.175 (*case tacis of 040609 suddenly ???!
38.176 [((Check_Postcond _, _,(([], Res), _)))] =>() | _ =>
38.177 error "tacis.sml: diff.behav. in setNextTactic -> autoCalculate (3)";
38.178 #######################################################################*)
38.179 - autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1) (*[x = 1]*);
38.180 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1) (*[x = 1]*);
38.181
38.182 - val ((pt,p),tacis) = get_calc 1;
38.183 - val ip = get_pos 1 1;
38.184 + val ((pt,p),tacis) = States.get_calc 1;
38.185 + val ip = States.get_pos 1 1;
38.186 val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
38.187 if UnparseC.term f = "[x = 1]"andalso p = ([],Res) andalso ip = ([],Res)then()else
38.188 error "tacis.sml: diff.behav. in setNextTactic -> autoCalculate (4)";
39.1 --- a/test/Tools/isac/ProgLang/auto_prog.sml Fri Sep 09 10:53:51 2022 +0200
39.2 +++ b/test/Tools/isac/ProgLang/auto_prog.sml Sun Sep 11 14:31:15 2022 +0200
39.3 @@ -84,7 +84,7 @@
39.4 " ??.empty" (* ..WORKS, NEVERTHELESS*)
39.5 then () else error "Auto_Prog.gen norm_Poly CHANGED";
39.6
39.7 -reset_states (); (*<-- evaluate, if ML-blocks are edited below*)
39.8 +States.reset (); (*<-- evaluate, if ML-blocks are edited below*)
39.9 CalcTree
39.10 [(["Term (b + a - b)", "normalform N"],
39.11 ("Poly",["polynomial", "simplification"],
39.12 @@ -93,7 +93,7 @@
39.13 moveActiveRoot 1;
39.14
39.15 autoCalculate 1 CompleteCalc;
39.16 -val ((pt,p),_) = get_calc 1;
39.17 +val ((pt,p),_) = States.get_calc 1;
39.18 Test_Tool.show_pt pt;
39.19 (* isabisac17 = 15 [
39.20 (([], Frm), Simplify (b + a - b)),
39.21 @@ -102,7 +102,7 @@
39.22 (([], Res), a)] *)
39.23
39.24 interSteps 1 ([], Res);
39.25 -val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
39.26 +val ((pt,p),_) = States.get_calc 1; Test_Tool.show_pt pt;
39.27 Test_Tool.show_pt pt;
39.28 (* isabisac17 = 15 [
39.29 (([], Frm), Simplify (b + a - b)),
39.30 @@ -112,7 +112,7 @@
39.31
39.32 interSteps 1 ([1], Res);(*<SYSERROR><CALCID>1</CALCID><ERROR>error in kernel 8</ERROR></SYSERROR>*)
39.33 "~~~~~ fun interSteps, args:"; val (cI, ip) = (1, ([1], Res));
39.34 - val ((pt, p), tacis) = get_calc cI;
39.35 + val ((pt, p), tacis) = States.get_calc cI;
39.36 (*if*) (not o is_interpos) ip = false;
39.37 val ip' = lev_pred' pt ip;
39.38
39.39 @@ -129,7 +129,7 @@
39.40 if p @ [length (Ctree.children (Ctree.get_nd pt p))] = [1, 4]
39.41 then () else error "detailrls: auto-generated norm_Poly doesnt work";
39.42
39.43 -val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
39.44 +val ((pt,p),_) = States.get_calc 1; Test_Tool.show_pt pt;
39.45 Test_Tool.show_pt pt; (*[
39.46 (([], Frm), Simplify (b + a - b)),
39.47 (([1], Frm), b + a - b),
39.48 @@ -181,7 +181,7 @@
39.49 *** . . . . . . . . Free (discard_parentheses1, ID)
39.50 *** . . Const (empty, 'a)
39.51 ***)
39.52 -reset_states ();
39.53 +States.reset ();
39.54 CalcTree
39.55 [(["Term (b + a - b)", "normalform N"],
39.56 ((** )"Poly"( **)"Rational"(**),["polynomial", "simplification"],
39.57 @@ -191,10 +191,10 @@
39.58 autoCalculate 1 CompleteCalc;
39.59
39.60 interSteps 1 ([], Res);
39.61 -val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
39.62 +val ((pt,p),_) = States.get_calc 1; Test_Tool.show_pt pt;
39.63
39.64 interSteps 1 ([1], Res);
39.65 -val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
39.66 +val ((pt,p),_) = States.get_calc 1; Test_Tool.show_pt pt;
39.67
39.68 (*with "Program SimplifyScript (t_::real) = \
39.69 \ ((Rewrite_Set norm_Rational) t_)"
40.1 --- a/test/Tools/isac/Specify/step-specify.sml Fri Sep 09 10:53:51 2022 +0200
40.2 +++ b/test/Tools/isac/Specify/step-specify.sml Sun Sep 11 14:31:15 2022 +0200
40.3 @@ -16,7 +16,7 @@
40.4 "----------- re-build: Step_Specify.do_next ---------------------------------------------------";
40.5 "----------- re-build: Step_Specify.do_next ---------------------------------------------------";
40.6 "----------- re-build: Step_Specify.do_next ---------------------------------------------------";
40.7 -reset_states ();
40.8 +States.reset ();
40.9 CalcTree (*ATTENTION: encode_fmz ... unlike CalcTreeTEST*)
40.10 [(["functionTerm (x \<up> 2 + 1)", "integrateBy x", "antiDerivative FF"],
40.11 ("Integrate", ["integrate", "function"], ["diff", "integration"]))];
40.12 @@ -24,7 +24,7 @@
40.13 moveActiveRoot 1;
40.14 autoCalculate 1 (Steps 1);
40.15
40.16 -val (ptp as (pt, p), _) = get_calc 1;
40.17 +val (ptp as (pt, p), _) = States.get_calc 1;
40.18 pt;(*isa==REP*)
40.19 val (_, ("Integrate", ["integrate", "function"], ["diff", "integration"]), _)
40.20 = get_obj g_origin pt (fst p);
40.21 @@ -32,10 +32,10 @@
40.22
40.23 (*this steps into according to "----- step 2 ---" below*)
40.24 "~~~~~ fun autoCalculate , args:"; val (cI, auto) = (1, (Steps 1));
40.25 - val pold = get_pos cI 1
40.26 + val pold = States.get_pos cI 1
40.27 ;
40.28 - (*case*) Math_Engine.autocalc [] pold (get_calc cI) auto (*of*);
40.29 -"~~~~~ fun autocalc , args:"; val (c: pos' list, ip, cs, (Solve.Steps s)) = ([], pold, (get_calc cI), auto);
40.30 + (*case*) Math_Engine.autocalc [] pold (States.get_calc cI) auto (*of*);
40.31 +"~~~~~ fun autocalc , args:"; val (c: pos' list, ip, cs, (Solve.Steps s)) = ([], pold, (States.get_calc cI), auto);
40.32 val c''''' = c; (*for from fun nxt_specify_\<longrightarrow>fun Step.do_next\<longrightarrow>fun autocalc, return*)
40.33
40.34 (*if*) s <= 1 (*then*);
40.35 @@ -64,7 +64,7 @@
40.36 "----- step 2 ---";(*isa<>REP*)
40.37 autoCalculate 1 (Steps 1);
40.38
40.39 -val (ptp as (pt, p), _) = get_calc 1;
40.40 +val (ptp as (pt, p), _) = States.get_calc 1;
40.41 pt;(*REP
40.42 val it =
40.43 Nd (PblObj
40.44 @@ -76,7 +76,7 @@
40.45
40.46 "----- step 3 ---";
40.47 autoCalculate 1 (Steps 1);
40.48 -val (ptp as (pt, p), _) = get_calc 1;
40.49 +val (ptp as (pt, p), _) = States.get_calc 1;
40.50
40.51 "----- step 4 ---";
40.52 autoCalculate 1 (Steps 1);
40.53 @@ -89,7 +89,7 @@
40.54 "----- step 8 ---";
40.55 autoCalculate 1 (Steps 1);
40.56
40.57 -val (ptp as (_, p), _) = get_calc 1;
40.58 +val (ptp as (_, p), _) = States.get_calc 1;
40.59
40.60 val (Form t,_,_) = ME_Misc.pt_extract ptp;
40.61