| changeset 59279 | 255c853ea2f0 |
| parent 52107 | f8845fc8f38d |
| child 60566 | 04f8699d2c9d |
| 59278:a474900d5bd2 | 59279:255c853ea2f0 |
|---|---|
1243 |
1243 |
1244 Nevertheless this specification is sufficient for automatically solving the equation --- the appropriate method will be found by refinement within the hierarchy of problem types. |
1244 Nevertheless this specification is sufficient for automatically solving the equation --- the appropriate method will be found by refinement within the hierarchy of problem types. |
1245 |
1245 |
1246 |
1246 |
1247 \section{Initialize the calculation} |
1247 \section{Initialize the calculation} |
1248 The start of a new proof requires the following initializations: The proof state is given by a proof tree {\tt ptree} and a position {\tt pos'}; both are empty at the beginning. The tactic {\tt Init\_Proof} is, like all other tactics, paired with an identifier of type {\tt string} for technical reasons. |
1248 The start of a new proof requires the following initializations: The proof state is given by a proof tree {\tt ctree} and a position {\tt pos'}; both are empty at the beginning. The tactic {\tt Init\_Proof} is, like all other tactics, paired with an identifier of type {\tt string} for technical reasons. |
1249 {\footnotesize\begin{verbatim} |
1249 {\footnotesize\begin{verbatim} |
1250 ML> val (mID,m) = ("Init_Proof",Init_Proof (fmz, (dom,pbt,met))); |
1250 ML> val (mID,m) = ("Init_Proof",Init_Proof (fmz, (dom,pbt,met))); |
1251 val mID = "Init_Proof" : string |
1251 val mID = "Init_Proof" : string |
1252 val m = |
1252 val m = |
1253 Init_Proof |
1253 Init_Proof |
1261 : string * mstep |
1261 : string * mstep |
1262 val pt = |
1262 val pt = |
1263 Nd |
1263 Nd |
1264 (PblObj |
1264 (PblObj |
1265 {branch=#,cell=#,env=#,loc=#,meth=#,model=#,origin=#,ostate=#,probl=#, |
1265 {branch=#,cell=#,env=#,loc=#,meth=#,model=#,origin=#,ostate=#,probl=#, |
1266 result=#,spec=#},[]) : ptree |
1266 result=#,spec=#},[]) : ctree |
1267 \end{verbatim}}%size |
1267 \end{verbatim}}%size |
1268 The mathematics engine {\tt me} returns the resulting formula {\tt f} of type {\tt mout} (which in this case is a problem), the next tactic {\tt nxt}, and a new proof state ({\tt ptree}, {\tt pos'}). |
1268 The mathematics engine {\tt me} returns the resulting formula {\tt f} of type {\tt mout} (which in this case is a problem), the next tactic {\tt nxt}, and a new proof state ({\tt ctree}, {\tt pos'}). |
1269 |
1269 |
1270 We can convince ourselves, that the problem is still empty, by increasing {\tt Compiler.Control.Print.printDepth}: |
1270 We can convince ourselves, that the problem is still empty, by increasing {\tt Compiler.Control.Print.printDepth}: |
1271 {\footnotesize\begin{verbatim} |
1271 {\footnotesize\begin{verbatim} |
1272 ML> Compiler.Control.Print.printDepth:=8; (*4 default*) |
1272 ML> Compiler.Control.Print.printDepth:=8; (*4 default*) |
1273 val it = () : unit |
1273 val it = () : unit |
1345 : string * mstep |
1345 : string * mstep |
1346 val pt = |
1346 val pt = |
1347 Nd |
1347 Nd |
1348 (PblObj |
1348 (PblObj |
1349 {branch=#,cell=#,env=#,loc=#,meth=#,model=#,origin=#,ostate=#,probl=#, |
1349 {branch=#,cell=#,env=#,loc=#,meth=#,model=#,origin=#,ostate=#,probl=#, |
1350 result=#,spec=#},[]) : ptree |
1350 result=#,spec=#},[]) : ctree |
1351 \end{verbatim}}%size |
1351 \end{verbatim}}%size |
1352 The {\tt me} is smart enough to know the appropriate problem type (transferred tacitly with {\tt Init\_Proof}). In order to challenge the student, the dialog guide may hide this information; then the {\tt me} works as follows. |
1352 The {\tt me} is smart enough to know the appropriate problem type (transferred tacitly with {\tt Init\_Proof}). In order to challenge the student, the dialog guide may hide this information; then the {\tt me} works as follows. |
1353 {\footnotesize\begin{verbatim} |
1353 {\footnotesize\begin{verbatim} |
1354 ML> val nxt = ("Specify_Problem", |
1354 ML> val nxt = ("Specify_Problem", |
1355 Specify_Problem ["polynomial","univariate","equation"]); |
1355 Specify_Problem ["polynomial","univariate","equation"]); |