sml-050211c-menu-finished: sml-050211c-menu-finished
authorwneuper
Fri, 11 Feb 2005 18:15:10 +0100
changeset 2083af2ff429de9a
parent 2082 1f418b3acd49
child 2084 62c642b010d6
sml-050211c-menu-finished:
intermediateSteps, getTactic, fetchApplicableTactics,
getAssumptions, getAccumulatedAsms
src/sml/FE-interface/interface.sml
src/sml/ROOT.ML
src/sml/systest/FE-interface.sml
src/sml/xmlsrc/datatypes.sml
src/sml/xmlsrc/interface-xml.sml
     1.1 --- a/src/sml/FE-interface/interface.sml	Fri Feb 11 17:06:17 2005 +0100
     1.2 +++ b/src/sml/FE-interface/interface.sml	Fri Feb 11 18:15:10 2005 +0100
     1.3 @@ -147,9 +147,9 @@
     1.4   @see #TACTICS_ALL
     1.5   @see #TACTICS_CURRENT_THEORY
     1.6   @see #TACTICS_CURRENT_METHOD  ..the only impl.WN.040307.*)
     1.7 -fun fetchApplicableTactics cI scope =
     1.8 +fun fetchApplicableTactics cI (p:pos') (*scope*) =
     1.9      let val ((pt, _), _) = get_calc cI
    1.10 -	val p = get_pos cI 1
    1.11 +	(*val p = get_pos cI 1*)
    1.12      in (applicabletacticsOK cI (sel_rules pt p))
    1.13         handle _ => sysERROR2xml cI "syserror in getApplicableTactics" end;
    1.14  
    1.15 @@ -158,12 +158,15 @@
    1.16  	 val (_, _, asms) = pt_extract (pt, p)
    1.17       in getasmsOK2xml cI asms end)
    1.18      handle _ => sysERROR2xml cI "syserror in getAssumptions"; 
    1.19 -(*   
    1.20 +
    1.21 +(*WN0502 @see ME/ctree: type asms: illdesigned, thus no positions returned*)  
    1.22  fun getAccumulatedAsms cI (p:pos') =
    1.23      (let val ((pt, _), _) = get_calc cI
    1.24 -     in accuasmsOK2xml cI (get_assumptions_ pt p) end)
    1.25 -    handle _ => sysERROR2xml cI "syserror in getAccumulatedAsms" end;
    1.26 -*)
    1.27 +	 val ass = map fst (get_assumptions_ pt p)
    1.28 +     in (*getaccuasmsOK2xml cI (get_assumptions_ pt p)*) 
    1.29 +     getasmsOK2xml cI ass end)
    1.30 +    handle _ => sysERROR2xml cI "syserror in getAccumulatedAsms";
    1.31 +
    1.32  
    1.33  (*since moveActive* does NOT transfer pos java --> sml (only sml --> java)
    1.34    refFormula might become involved in far-off errors !!!*)
     2.1 --- a/src/sml/ROOT.ML	Fri Feb 11 17:06:17 2005 +0100
     2.2 +++ b/src/sml/ROOT.ML	Fri Feb 11 18:15:10 2005 +0100
     2.3 @@ -75,7 +75,7 @@
     2.4  
     2.5  *)
     2.6  
     2.7 -  val version_kernel = "sml-050210b";
     2.8 +  val version_kernel = "sml-050211c-menu-finished";
     2.9  
    2.10    print_depth 3; 
    2.11  
     3.1 --- a/src/sml/systest/FE-interface.sml	Fri Feb 11 17:06:17 2005 +0100
     3.2 +++ b/src/sml/systest/FE-interface.sml	Fri Feb 11 18:15:10 2005 +0100
     3.3 @@ -823,6 +823,7 @@
     3.4   moveActiveDown 1;
     3.5   moveActiveDown 1; (*-1 + x = 0*);
     3.6  
     3.7 + (*UC\label{SOLVE:INFO:intermediate-steps}*)
     3.8   interSteps 1 ([2],Res);
     3.9   
    3.10   moveActiveUp 1; 
    3.11 @@ -847,7 +848,8 @@
    3.12  "--------- getTactic, fetchApplicableTactics ---------------------";
    3.13  "--------- getTactic, fetchApplicableTactics ---------------------";
    3.14   states:=[];
    3.15 - CalcTree
    3.16 + CalcTree(**)
    3.17 +
    3.18   [(["equality (x+1=2)", "solveFor x","solutions L"], 
    3.19     ("Test.thy", 
    3.20      ["sqroot-test","univariate","equation","test"],
    3.21 @@ -857,12 +859,14 @@
    3.22   val ((pt,_),_) = get_calc 1;
    3.23   show_pt pt;
    3.24  
    3.25 - fetchApplicableTactics 1 3 
    3.26 - (*TACTICS_CURRENT_METHOD^^^ the only one impl.WN.040307*);
    3.27 - moveActiveUp 1;
    3.28 - moveActiveUp 1;
    3.29 - moveActiveUp 1;
    3.30 - fetchApplicableTactics 1 3;
    3.31 + (*UC\label{SOLVE:HIDE:getTactic}*)
    3.32 + getTactic 1 ([1],Res);
    3.33 + getTactic 1 ([2],Res);
    3.34 + getTactic 1 ([],Res);
    3.35 +
    3.36 +(*UC\label{SOLVE:MANUAL:TACTIC:listall}*)
    3.37 + fetchApplicableTactics 1 ([],Frm) ;
    3.38 + fetchApplicableTactics 1 ([3,1],Frm);
    3.39  
    3.40  
    3.41  "--------- getAssumptions, getAccumulatedAsms --------------------";
    3.42 @@ -878,9 +882,12 @@
    3.43  val ((pt,_),_) = get_calc 1;
    3.44  show_pt pt;
    3.45  
    3.46 +(*UC\label{SOLVE:HELP:assumptions}*)
    3.47  getAssumptions 1 ([3], Res);
    3.48 -
    3.49 -
    3.50 +getAssumptions 1 ([5], Res);
    3.51 +(*UC\label{SOLVE:HELP:assumptions-origin} WN0502 still without positions*)
    3.52 +getAccumulatedAsms 1 ([3], Res);
    3.53 +getAccumulatedAsms 1 ([5], Res);
    3.54  
    3.55  
    3.56  "--------- arbitrary combinations of steps -----------------------";
     4.1 --- a/src/sml/xmlsrc/datatypes.sml	Fri Feb 11 17:06:17 2005 +0100
     4.2 +++ b/src/sml/xmlsrc/datatypes.sml	Fri Feb 11 18:15:10 2005 +0100
     4.3 @@ -57,6 +57,7 @@
     4.4  (* writeln(formulae2xml 6 [str2term "1+1=2", str2term "1+1+1=3"]);
     4.5     *)
     4.6  
     4.7 +(*WN0502 @see ME/ctree: type asms: illdesigned, thus not used*)
     4.8  fun posform2xml j (p:pos', term) =
     4.9      (indt j ^     "<POSFORM>\n" ^
    4.10       pos'2xml (j+i) ("POSITION", p) ^
     5.1 --- a/src/sml/xmlsrc/interface-xml.sml	Fri Feb 11 17:06:17 2005 +0100
     5.2 +++ b/src/sml/xmlsrc/interface-xml.sml	Fri Feb 11 18:15:10 2005 +0100
     5.3 @@ -125,17 +125,20 @@
     5.4  	     \@@@@@end@@@@@");
     5.5  (* getasmsOK2xml 333 [str2term "1+1=2", str2term "1+1+1=3"];
     5.6     *)
     5.7 +
     5.8 +(*WN0502 @see ME/ctree: type asms: illdesigned, thus not used*)
     5.9  fun getaccuasmsOK2xml cI asms =
    5.10      writeln ("@@@@@begin@@@@@\n "^string_of_int cI^" \n\
    5.11  	     \<GETACCUMULATEDASMS>\n\
    5.12  	     \  <CALCID> "^string_of_int cI^" </CALCID>\n\
    5.13 -	     \  <POSASMLIST>\n"^
    5.14 -	     posforms2xml (i+i) asms^
    5.15 -	     "  </POSASMLIST>\n\
    5.16 +	     \  <ASMLIST>\n"^
    5.17 +	     formulae2xml (i+i) asms^
    5.18 +	     "  </ASMLIST>\n\
    5.19  	     \</GETACCUMULATEDASMS>\n\
    5.20  	     \@@@@@end@@@@@");
    5.21  (* getaccuasmsOK2xml 333 [(([1],Res), str2term "1+1=2"),
    5.22  			  (([2],Res), str2term "1+1+1=3")];
    5.23 +   getaccuasmsOK2xml 333 [str2term "1+1=2", str2term "1+1+1=3"];
    5.24     *)
    5.25  
    5.26  fun getintervalOK (cI:calcID) fs =