1.1 --- a/src/sml/FE-interface/interface.sml	Mon Sep 22 17:28:37 2008 +0200
     1.2 +++ b/src/sml/FE-interface/interface.sml	Tue Oct 28 15:16:31 2008 +0100
     1.3 @@ -331,9 +331,13 @@
     1.4      in getintervalOK cI [(to, headline)] end)
     1.5      handle _ => sysERROR2xml cI "error in kernel")
     1.6  
     1.7 +  | getFormulaeFromTo cI (from as ([],Pbl):pos') (to as ([],Met):pos')_ false =
     1.8 +    getFormulaeFromTo cI ([],Pbl) ([],Pbl) (~00000) false
     1.9 +
    1.10    | getFormulaeFromTo cI (from:pos') (to:pos') level false =
    1.11  (* val (cI, from, to, level) = (1, unc, gen, 0);
    1.12     val (cI, from, to, level) = (1, unc, gen, 1);
    1.13 +   val (cI, from, to, level) = (1, ([],Pbl), ([],Met), 1);
    1.14     *)
    1.15      (if from = to then sysERROR2xml cI "getFormulaeFromTo: From = To"
    1.16       else

     2.1 --- a/src/sml/ME/inform.sml	Mon Sep 22 17:28:37 2008 +0200
     2.2 +++ b/src/sml/ME/inform.sml	Tue Oct 28 15:16:31 2008 +0100
     2.3 @@ -719,7 +719,7 @@
     2.4  	   else case cas_input ifo of
     2.5  (* val Some (pt, _) = cas_input ifo;
     2.6     *)
     2.7 -		    Some (pt, _) => ("ok",([],[],(pt, (p, Pbl))))
     2.8 +		    Some (pt, _) => ("ok",([],[],(pt, (p, Met))))
     2.9  		  | None =>
    2.10  		    compare_step ([],[],(pt,
    2.11  				     (*last step re-calc in compare_step TODO*)

     3.1 --- a/src/smltest/IsacKnowledge/diff.sml	Mon Sep 22 17:28:37 2008 +0200
     3.2 +++ b/src/smltest/IsacKnowledge/diff.sml	Tue Oct 28 15:16:31 2008 +0100
     3.3 @@ -21,7 +21,6 @@
     3.4  "----------- autoCalculate diff after_simplification -------------";
     3.5  "----------- autoCalculate differentiate_equality ----------------";
     3.6  "----------- tests for examples ----------------------------------";
     3.7 -"----------- CAS input -------------------------------------------";
     3.8  "------------inform for x^2+x+1 ----------------------------------";
     3.9  "-----------------------------------------------------------------";
    3.10  "-----------------------------------------------------------------";
    3.11 @@ -671,74 +670,6 @@
    3.12  trace_rewrite := false;
    3.13  *)
    3.14  
    3.15 -"----------- CAS input -------------------------------------------";
    3.16 -"----------- CAS input -------------------------------------------";
    3.17 -"----------- CAS input -------------------------------------------";
    3.18 -val t = str2term "Diff (x^^^2 + x + 1, x)";
    3.19 -case t of Const ("Diff.Diff", _) $ _ => ()
    3.20 -	| _ => raise error "diff.sml behav.changed for CAS Diff (..., x)";
    3.21 -atomty t;
    3.22 -"-----------------------------------------------------------------";
    3.23 -states:=[];
    3.24 -CalcTree [([], ("e_domID", ["e_pblID"], ["e_metID"]))];
    3.25 -Iterator 1;
    3.26 -moveActiveRoot 1;
    3.27 -replaceFormula 1 "Diff (x^2 + x + 1, x)";
    3.28 -val ((pt,_),_) = get_calc 1;
    3.29 -val PblObj {probl, meth, spec, fmz, env, loc, ...} = get_obj I pt [];
    3.30 -val None = env;
    3.31 -val (Some istate, None) = loc;
    3.32 -print_depth 5;
    3.33 -writeln"-----------------------------------------------------------";
    3.34 -spec;
    3.35 -writeln (itms2str thy probl);
    3.36 -writeln (itms2str thy meth);
    3.37 -writeln (istate2str istate);
    3.38 -
    3.39 -print_depth 3;
    3.40 -
    3.41 -
    3.42 -autoCalculate 1 (Step 1);
    3.43 -val ((pt,p),_) = get_calc 1; show_pt pt;
    3.44 -
    3.45 -"-----------------------------------------------------------------";
    3.46 -states:=[];
    3.47 -CalcTree
    3.48 -[(["functionTerm (x^2 + x + 1)",
    3.49 -   "differentiateFor x", "derivative f_'_"], 
    3.50 -  ("Isac.thy", ["derivative_of","function"],
    3.51 -  ["diff","differentiate_on_R"]))];
    3.52 -Iterator 1;
    3.53 -moveActiveRoot 1;
    3.54 -print_depth 5; get_obj g_spec pt []; print_depth 3; 
    3.55 -autoCalculate 1 CompleteCalcHead;
    3.56 -val ((pt,_),_) = get_calc 1;
    3.57 -val PblObj {probl, meth, spec, fmz, env, loc, ...} = get_obj I pt [];
    3.58 -val None = env;
    3.59 -val (Some istate, None) = loc;
    3.60 -print_depth 5;
    3.61 -writeln"-----------------------------------------------------------";
    3.62 -spec;
    3.63 -writeln (itms2str thy probl);
    3.64 -writeln (itms2str thy meth);
    3.65 -writeln (istate2str istate);
    3.66 -
    3.67 -print_depth 3;
    3.68 -
    3.69 -
    3.70 -
    3.71 -autoCalculate 1 (Step 1);
    3.72 -val ((pt,p),_) = get_calc 1; show_pt pt;
    3.73 -
    3.74 -autoCalculate 1 CompleteCalc;
    3.75 -val ((pt,p),_) = get_calc 1;
    3.76 -val Form res = (#1 o pt_extract) (pt, ([],Res));
    3.77 -show_pt pt;
    3.78 -(* WN070703 does not work like Integrate due to error in next-pos
    3.79 -if p = ([], Res) andalso term2str res = "1 + 2 * x" then ()
    3.80 -else raise error "diff.sml behav.changed for Diff (x^2 + x + 1, x)";
    3.81 -*)
    3.82 -
    3.83  "------------inform for x^2+x+1 ----------------------------------";
    3.84  "------------inform for x^2+x+1 ----------------------------------";
    3.85  "------------inform for x^2+x+1 ----------------------------------";

     4.1 --- a/src/smltest/ME/inform.sml	Mon Sep 22 17:28:37 2008 +0200
     4.2 +++ b/src/smltest/ME/inform.sml	Tue Oct 28 15:16:31 2008 +0100
     4.3 @@ -29,6 +29,9 @@
     4.4  "--------- CAS-command on ([],Pbl) -------------------------------";
     4.5  "--------- CAS-command on ([],Pbl) FE-interface ------------------";
     4.6  "--------- inform [rational,simplification] ----------------------";
     4.7 +"--------- Take as 1st tac, start with <NEW> (CAS input) ---------";
     4.8 +"--------- Take as 1st tac, start from exp -----------------------";
     4.9 +"--------- init_form, start with <NEW> (CAS input) ---------------";
    4.10  "-----------------------------------------------------------------";
    4.11  "-----------------------------------------------------------------";
    4.12  "-----------------------------------------------------------------";
    4.13 @@ -496,3 +499,274 @@
    4.14  if p = ([6], Res) andalso (length o children o (get_nd pt)) (fst p) = 2 then ()
    4.15  else raise error ("inform.sml: [rational,simplification] 3");
    4.16  show_pt pt;
    4.17 +
    4.18 +"--------- Take as 1st tac, start with <NEW> (CAS input) ---------";
    4.19 +"--------- Take as 1st tac, start with <NEW> (CAS input) ---------";
    4.20 +"--------- Take as 1st tac, start with <NEW> (CAS input) ---------";
    4.21 +val t = str2term "Diff (x^^^2 + x + 1, x)";
    4.22 +case t of Const ("Diff.Diff", _) $ _ => ()
    4.23 +	| _ => raise 
    4.24 +	      error "diff.sml behav.changed for CAS Diff (..., x)";
    4.25 +atomty t;
    4.26 +"-----------------------------------------------------------------";
    4.27 +(*1>*)states:=[];
    4.28 +(*2>*)CalcTree [([], ("e_domID", ["e_pblID"], ["e_metID"]))];
    4.29 +(*3>*)Iterator 1;moveActiveRoot 1;
    4.30 +"----- here the Headline has been finished";
    4.31 +(*4>*)moveActiveFormula 1 ([],Pbl);
    4.32 +(*5>*)replaceFormula 1 "Diff (x^2 + x + 1, x)";
    4.33 +val ((pt,_),_) = get_calc 1;
    4.34 +val PblObj {probl, meth, spec, fmz, env, loc, ...} = get_obj I pt [];
    4.35 +val None = env;
    4.36 +val (Some istate, None) = loc;
    4.37 +print_depth 5;
    4.38 +writeln"-----------------------------------------------------------";
    4.39 +spec;
    4.40 +writeln (itms2str thy probl);
    4.41 +writeln (itms2str thy meth);
    4.42 +writeln (istate2str istate);
    4.43 +
    4.44 +print_depth 3;
    4.45 +
    4.46 +refFormula 1 ([],Pbl) (*--> correct CalcHead*);
    4.47 + (*081016 NOT necessary (but leave it in Java):*)
    4.48 +(*6>*)(*completeCalcHead*)autoCalculate 1 CompleteCalcHead;
    4.49 +"----- here the CalcHead has been completed --- ONCE MORE ?????";
    4.50 +
    4.51 +(***difference II***)
    4.52 +val ((pt,p),_) = get_calc 1;
    4.53 +(*val p = ([], Pbl)*)
    4.54 +val PblObj {probl, meth, spec, fmz, env, loc, ...} = get_obj I pt [];
    4.55 +val None = env;
    4.56 +val (Some istate, None) = loc;
    4.57 +print_depth 5; writeln (istate2str istate);  print_depth 3;
    4.58 +(*ScrState ([],
    4.59 + [], None,
    4.60 + ??.empty, Sundef, false)*)
    4.61 +print_depth 5; spec; print_depth 3;
    4.62 +(*("Isac.thy",
    4.63 +      ["derivative_of", "function"],
    4.64 +      ["diff", "differentiate_on_R"]) : spec*)
    4.65 +writeln (itms2str thy probl);
    4.66 +(*[
    4.67 +(1 ,[1] ,true ,#Given ,Cor functionTerm (x ^^^ 2 + x + 1) ,(f_, [x ^^^ 2 + x + 1])),
    4.68 +(2 ,[1] ,true ,#Given ,Cor differentiateFor x ,(v_, [x])),
    4.69 +(3 ,[1] ,true ,#Find ,Cor derivative f_'_ ,(f_'_, [f_'_]))]*)
    4.70 +writeln (itms2str thy meth);
    4.71 +(*[
    4.72 +(1 ,[1] ,true ,#Given ,Cor functionTerm (x ^^^ 2 + x + 1) ,(f_, [x ^^^ 2 + x + 1])),
    4.73 +(2 ,[1] ,true ,#Given ,Cor differentiateFor x ,(v_, [x])),
    4.74 +(3 ,[1] ,true ,#Find ,Cor derivative f_'_ ,(f_'_, [f_'_]))]*)
    4.75 +writeln"-----------------------------------------------------------";
    4.76 +(*7>*)fetchProposedTactic 1 (*--> Apply_Method*);
    4.77 +(*WN081028 fixed <ERROR> helpless </ERROR> by inform returning ...(.,Met)*)
    4.78 +autoCalculate 1 CompleteCalc;
    4.79 +val ((pt,p),_) = get_calc 1;
    4.80 +val Form res = (#1 o pt_extract) (pt, ([],Res));
    4.81 +show_pt pt;
    4.82 +if p = ([], Res) andalso term2str res = "1 + 2 * x" then ()
    4.83 +else raise error "diff.sml behav.changed for Diff (x^2 + x + 1, x)";
    4.84 +
    4.85 +
    4.86 +"--------- Take as 1st tac, start from exp -----------------------";
    4.87 +"--------- Take as 1st tac, start from exp -----------------------";
    4.88 +"--------- Take as 1st tac, start from exp -----------------------";
    4.89 +(*the following input is copied from BridgeLog Java <==> SML,
    4.90 +  omitting unnecessary inputs*)
    4.91 +(*1>*)states:=[];
    4.92 +(*2>*)CalcTree [(["functionTerm (x^2 + x + 1)", "differentiateFor x", "derivative f_'_"],("Isac.thy",["derivative_of","function"],["diff","differentiate_on_R"]))];
    4.93 +(*3>*)Iterator 1; moveActiveRoot 1;
    4.94 +
    4.95 +(*6>*)(*completeCalcHead*)autoCalculate 1 CompleteCalcHead;
    4.96 +
    4.97 +(***difference II***)
    4.98 +val ((pt,_),_) = get_calc 1;
    4.99 +val PblObj {probl, meth, spec, fmz, env, loc, ...} = get_obj I pt [];
   4.100 +val None = env;
   4.101 +val (Some istate, None) = loc;
   4.102 +print_depth 5; writeln (istate2str istate);  print_depth 3;
   4.103 +(*ScrState ([],
   4.104 + [], None,
   4.105 + ??.empty, Sundef, false)*)
   4.106 +print_depth 5; spec; print_depth 3;
   4.107 +(*("Isac.thy",
   4.108 +      ["derivative_of", "function"],
   4.109 +      ["diff", "differentiate_on_R"]) : spec*)
   4.110 +writeln (itms2str thy probl);
   4.111 +(*[
   4.112 +(1 ,[1] ,true ,#Given ,Cor functionTerm (x ^^^ 2 + x + 1) ,(f_, [x ^^^ 2 + x + 1])),
   4.113 +(2 ,[1] ,true ,#Given ,Cor differentiateFor x ,(v_, [x])),
   4.114 +(3 ,[1] ,true ,#Find ,Cor derivative f_'_ ,(f_'_, [f_'_]))]*)
   4.115 +writeln (itms2str thy meth);
   4.116 +(*[
   4.117 +(1 ,[1] ,true ,#Given ,Cor functionTerm (x ^^^ 2 + x + 1) ,(f_, [x ^^^ 2 + x + 1])),
   4.118 +(2 ,[1] ,true ,#Given ,Cor differentiateFor x ,(v_, [x])),
   4.119 +(3 ,[1] ,true ,#Find ,Cor derivative f_'_ ,(f_'_, [f_'_]))]*)
   4.120 +writeln"-----------------------------------------------------------";
   4.121 +(*7>*)fetchProposedTactic 1 (*--> Apply_Method*);
   4.122 +
   4.123 +autoCalculate 1 (Step 1);
   4.124 +val ((pt,p),_) = get_calc 1;
   4.125 +val Form res = (#1 o pt_extract) (pt, p);
   4.126 +if term2str res = "d_d x (x ^^^ 2 + x + 1)" then ()
   4.127 +else raise error "diff.sml Diff (x^2 + x + 1, x) from exp";
   4.128 +
   4.129 +
   4.130 +"--------- init_form, start with <NEW> (CAS input) ---------------";
   4.131 +"--------- init_form, start with <NEW> (CAS input) ---------------";
   4.132 +"--------- init_form, start with <NEW> (CAS input) ---------------";
   4.133 +states:=[];
   4.134 +CalcTree [([], ("e_domID", ["e_pblID"], ["e_metID"]))];
   4.135 +(*[[from sml: > @@@@@begin@@@@@
   4.136 +[[from sml:  1 
   4.137 +[[from sml: <CALCTREE>
   4.138 +[[from sml:    <CALCID> 1 </CALCID>
   4.139 +[[from sml: </CALCTREE>
   4.140 +[[from sml: @@@@@end@@@@@*)
   4.141 +Iterator 1;
   4.142 +(*[[from sml: > @@@@@begin@@@@@
   4.143 +[[from sml:  1 
   4.144 +[[from sml: <ADDUSER>
   4.145 +[[from sml:   <CALCID> 1 </CALCID>
   4.146 +[[from sml:   <USERID> 1 </USERID>
   4.147 +[[from sml: </ADDUSER>
   4.148 +[[from sml: @@@@@end@@@@@*)
   4.149 +moveActiveRoot 1;
   4.150 +(*[[from sml: > @@@@@begin@@@@@
   4.151 +[[from sml:  1 
   4.152 +[[from sml: <CALCITERATOR>
   4.153 +[[from sml:   <CALCID> 1 </CALCID>
   4.154 +[[from sml:   <POSITION>
   4.155 +[[from sml:     <INTLIST>
   4.156 +[[from sml:     </INTLIST>
   4.157 +[[from sml:     <POS> Pbl </POS>
   4.158 +[[from sml:   </POSITION>
   4.159 +[[from sml: </CALCITERATOR>
   4.160 +[[from sml: @@@@@end@@@@@*)
   4.161 +getFormulaeFromTo 1 ([],Pbl) ([],Pbl) 0 false;
   4.162 +(*[[from sml: > @@@@@begin@@@@@                STILL CORRECT
   4.163 +[[from sml:  1 
   4.164 +[[from sml: <GETELEMENTSFROMTO>
   4.165 +[[from sml:   <CALCID> 1 </CALCID>
   4.166 +[[from sml:   <FORMHEADS>
   4.167 +[[from sml:     <CALCFORMULA>
   4.168 +[[from sml:       <POSITION>
   4.169 +[[from sml:         <INTLIST>
   4.170 +[[from sml:         </INTLIST>
   4.171 +[[from sml:         <POS> Pbl </POS>
   4.172 +[[from sml:       </POSITION>
   4.173 +[[from sml:       <FORMULA>
   4.174 +[[from sml:         <MATHML>
   4.175 +[[from sml:           <ISA> ________________________________________________ </ISA>
   4.176 +[[from sml:         </MATHML>
   4.177 +[[from sml: 
   4.178 +[[from sml:       </FORMULA>
   4.179 +[[from sml:     </CALCFORMULA>
   4.180 +[[from sml:   </FORMHEADS>
   4.181 +[[from sml: </GETELEMENTSFROMTO>
   4.182 +[[from sml: @@@@@end@@@@@*)
   4.183 +refFormula 1 ([],Pbl);
   4.184 +(*[[from sml: > @@@@@begin@@@@@                STILL CORRECT
   4.185 +[[from sml:  1 
   4.186 +[[from sml: <REFFORMULA>
   4.187 +[[from sml:   <CALCID> 1 </CALCID>
   4.188 +[[from sml:   <CALCHEAD status = "incorrect">
   4.189 +[[from sml:     <POSITION>
   4.190 +[[from sml:       <INTLIST>
   4.191 +[[from sml:       </INTLIST>
   4.192 +[[from sml:       <POS> Pbl </POS>
   4.193 +[[from sml:     </POSITION>
   4.194 +[[from sml:     <HEAD>
   4.195 +[[from sml:       <MATHML>
   4.196 +[[from sml:         <ISA> Problem (e_domID, [e_pblID]) </ISA>
   4.197 +[[from sml:       </MATHML>
   4.198 +[[from sml:     </HEAD>
   4.199 +[[from sml:     <MODEL>
   4.200 +[[from sml:       <GIVEN>  </GIVEN>
   4.201 +[[from sml:       <WHERE>  </WHERE>
   4.202 +[[from sml:       <FIND>  </FIND>
   4.203 +[[from sml:       <RELATE>  </RELATE>
   4.204 +[[from sml:     </MODEL>
   4.205 +[[from sml:     <BELONGSTO> Pbl </BELONGSTO>
   4.206 +[[from sml:     <SPECIFICATION>
   4.207 +[[from sml:       <THEORYID> e_domID </THEORYID>
   4.208 +[[from sml:       <PROBLEMID>
   4.209 +[[from sml:         <STRINGLIST>
   4.210 +[[from sml:           <STRING> e_pblID </STRING>
   4.211 +[[from sml:         </STRINGLIST>
   4.212 +[[from sml:       </PROBLEMID>
   4.213 +[[from sml:       <METHODID>
   4.214 +[[from sml:         <STRINGLIST>
   4.215 +[[from sml:           <STRING> e_metID </STRING>
   4.216 +[[from sml:         </STRINGLIST>
   4.217 +[[from sml:       </METHODID>
   4.218 +[[from sml:     </SPECIFICATION>
   4.219 +[[from sml:   </CALCHEAD>
   4.220 +[[from sml: </REFFORMULA>
   4.221 +[[from sml: @@@@@end@@@@@*)
   4.222 +moveActiveFormula 1 ([],Pbl);
   4.223 +(*[[from sml: > @@@@@begin@@@@@
   4.224 +[[from sml:  1 
   4.225 +[[from sml: <CALCITERATOR>
   4.226 +[[from sml:   <CALCID> 1 </CALCID>
   4.227 +[[from sml:   <POSITION>
   4.228 +[[from sml:     <INTLIST>
   4.229 +[[from sml:     </INTLIST>
   4.230 +[[from sml:     <POS> Pbl </POS>
   4.231 +[[from sml:   </POSITION>
   4.232 +[[from sml: </CALCITERATOR>
   4.233 +[[from sml: @@@@@end@@@@@*)
   4.234 +replaceFormula 1 "Simplify (1+2)";
   4.235 +(*[[from sml: > @@@@@begin@@@@@
   4.236 +[[from sml:  1 
   4.237 +[[from sml: <REPLACEFORMULA>
   4.238 +[[from sml:   <CALCID> 1 </CALCID>
   4.239 +[[from sml:   <CALCCHANGED>
   4.240 +[[from sml:     <UNCHANGED>
   4.241 +[[from sml:       <INTLIST>
   4.242 +[[from sml:       </INTLIST>
   4.243 +[[from sml:       <POS> Pbl </POS>
   4.244 +[[from sml:     </UNCHANGED>
   4.245 +[[from sml:     <DELETED>
   4.246 +[[from sml:       <INTLIST>
   4.247 +[[from sml:       </INTLIST>
   4.248 +[[from sml:       <POS> Pbl </POS>
   4.249 +[[from sml:     </DELETED>
   4.250 +[[from sml:     <GENERATED>
   4.251 +[[from sml:       <INTLIST>
   4.252 +[[from sml:       </INTLIST>
   4.253 +[[from sml:       <POS> Met </POS>                           DIFFERENCE: Pbl
   4.254 +[[from sml:     </GENERATED>
   4.255 +[[from sml:   </CALCCHANGED>
   4.256 +[[from sml: </REPLACEFORMULA>
   4.257 +[[from sml: @@@@@end@@@@@*)
   4.258 +getFormulaeFromTo 1 ([],Pbl) ([],Pbl) 0 false(*              DIFFERENCE: Pbl*);
   4.259 +(*@@@@@begin@@@@@
   4.260 + 1
   4.261 +<GETELEMENTSFROMTO>
   4.262 +  <CALCID> 1 </CALCID>
   4.263 +  <FORMHEADS>
   4.264 +    <CALCFORMULA>
   4.265 +      <POSITION>
   4.266 +        <INTLIST>
   4.267 +        </INTLIST>
   4.268 +        <POS> Pbl </POS>
   4.269 +      </POSITION>
   4.270 +      <FORMULA>
   4.271 +        <MATHML>
   4.272 +          <ISA> Simplify (1 + 2) </ISA>                      WORKS !!!!!
   4.273 +        </MATHML>
   4.274 +      </FORMULA>
   4.275 +    </CALCFORMULA>
   4.276 +  </FORMHEADS>
   4.277 +</GETELEMENTSFROMTO>
   4.278 +@@@@@end@@@@@*)
   4.279 +getFormulaeFromTo 1 ([],Pbl) ([],Met) 0 false;
   4.280 +(*[[from sml: > @@@@@begin@@@@@
   4.281 +[[from sml:  1 
   4.282 +[[from sml: <SYSERROR>
   4.283 +[[from sml:   <CALCID> 1 </CALCID>
   4.284 +[[from sml:   <ERROR> error in getFormulaeFromTo </ERROR>
   4.285 +[[from sml: </SYSERROR>
   4.286 +[[from sml: @@@@@end@@@@@*)
   4.287 +(*step into getFormulaeFromTo --- bug corrected...*)