# HG changeset patch
# User wneuper
# Date 1110039981 -3600
# Node ID a863de293415ee7fbbb0ae1f2f0e5ad48aff8284
# Parent  8df2ab3d17c96c3d048af37232028f9e4ffc0e1d
sml-050305b-cut_tree: after sticky tags

diff -r 8df2ab3d17c9 -r a863de293415 src/sml/ME/ctree.sml
--- a/src/sml/ME/ctree.sml	Sat Mar 05 14:36:49 2005 +0100
+++ b/src/sml/ME/ctree.sml	Sat Mar 05 17:26:21 2005 +0100
@@ -1231,6 +1231,8 @@
   | update_loc pt (p,_) x = 
     let val (_,lres) = get_obj g_loc pt p
     in appl_obj (repl_loc (Some x,lres)) pt p end;
+(*WN050305 for handling cut_tree in cappend_atomic -- TODO redesign !*)
+fun update_loc' pt p iss = appl_obj (repl_loc iss) pt p;
 
 (*13.8.02---------------------------
 fun get_loc EmptyPtree _ = None
@@ -1824,7 +1826,7 @@
 	    in cut_levup (cuts @ cuts') clevup' pt pt'' (P, p) (get_nd pt P)
 	    end
     end;
-
+ 
 
 fun cut_tree pt (pos,_) =
     if not (existpt pos pt) 
@@ -1870,14 +1872,39 @@
   apfst (append_atomic p loc f r f' s) (cut_tree pt (p,Frm))
 );
 fun cappend_atomic pt p loc f r f' s = 
-let val _= writeln("##@cappend_atomic: pos ="^pos2str p)
-    val _= writeln("##@cappend_atomic before cut_tree: loc ="^istate2str loc)
-    val (pt', cs) = cut_tree pt (p,Frm)
+let val _= writeln("##@cappend_atomic: pos ="^pos2str p);
+    val _= writeln("##@cappend_atomic arg loc ="^istate2str loc);
+    val _= if existpt  p pt
+	   then writeln("##@cappend_atomic before cut_ loc ="^
+			istates2str (get_obj g_loc pt p))
+	   else  writeln("##@cappend_atomic pos not existent before cut_");
+    val (pt', cs) = cut_tree pt (p,Frm);
+    val _= if existpt  p pt'
+	   then writeln("##@cappend_atomic after cut_ loc ="^
+		   istates2str (get_obj g_loc pt' p))
+	   else  writeln("##@cappend_atomic pos not existent after cut_");
+    val pt'' = append_atomic p loc f r f' s pt';
+    val _= writeln("##@cappend_atomic after append: loc ="^
+		   istates2str (get_obj g_loc pt'' p));
+in (pt'', cs) end;
+
+fun cappend_atomic pt p loc f r f' s = 
+let val (pt', cs) = cut_tree pt (p,Frm)
     val pt'' = append_atomic p loc f r f' s pt'
-    val _= writeln("##@cappend_atomic after append: loc ="^
-		   istates2str (get_obj g_loc pt'' p))
 in (pt'', cs) end;
 
+fun cappend_atomic pt p ist_res f r f' s = 
+    if existpt p pt andalso get_obj g_tac pt p=Empty_Tac
+    then (*after Take: transfer Frm and respective istate*)
+	let val (ist_form, f) = (get_loc pt (p,Frm), 
+				 get_obj g_form pt p)
+	    val (pt, cs) = cut_tree pt (p,Frm)
+	    val pt = append_atomic p e_istate f r f' s pt
+	    val pt = update_loc' pt p (Some ist_form, Some ist_res)
+	in (pt, cs) end
+    else apfst (append_atomic p ist_res f r f' s) (cut_tree pt (p,Frm));
+
+
 (* called by Take *)
 fun append_form p l f pt = 
 (writeln("##@append_form: pos ="^pos2str p);
diff -r 8df2ab3d17c9 -r a863de293415 src/sml/systest/auto-inform.sml
--- a/src/sml/systest/auto-inform.sml	Sat Mar 05 14:36:49 2005 +0100
+++ b/src/sml/systest/auto-inform.sml	Sat Mar 05 17:26:21 2005 +0100
@@ -9,15 +9,15 @@
 "--------- maximum-example: complete_mod -------------------------";
 "appendForm with miniscript with mini-subpbl:";
 "--------- appendFormula: on Res + equ_nrls ----------------------";
-"--------- appendFormula: on Frm + equ_nrls ----------------------X";
+"--------- appendFormula: on Frm + equ_nrls ----------------------";
 "--------- appendFormula: on Res + NO deriv ----------------------";
 "--------- appendFormula: on Res + late deriv --------------------";
 "--------- appendFormula: on Res + late deriv [x = 3 + -2]---///--";
 "replaceForm with miniscript with mini-subpbl:";
 "--------- replaceFormula: on Res + = ----------------------------";
-"--------- replaceFormula: on Res + = 1st Nd ---------------------X";
+"--------- replaceFormula: on Res + = 1st Nd ---------------------";
 "--------- replaceFormula: on Frm + = 1st Nd ---------------------";
-"--------- replaceFormula: cut calculation -----------------------X";
+"--------- replaceFormula: cut calculation -----------------------";
 
 
 
@@ -309,49 +309,8 @@
  Iterator 1; moveActiveRoot 1;
  autoCalculate 1 CompleteCalcHead;
  autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1) (*x + 1 = 2*);
- (*> ###generate1 Apply_Method': pos = ([1], Frm)
-###generate1 Apply_Method': topt= Some x + 1 = 2
-###generate1 Apply_Method': is  = ScrState (["
-(e_, x + 1 = 2)","
-(v_, x)"],
- [], None,
- ??.empty, Safe, true)
-##@cappend_form: pos =[1]
-##@cappend_form before cut_tree: loc =ScrState (["
-(e_, x + 1 = 2)","
-(v_, x)"],
- [], None,
- ??.empty, Safe, true)
-##@append_form: pos =[1]
-##@cappend_form after append: loc =(#Some ScrState (["
-(e_, x + 1 = 2)","
-(v_, x)"],
- [], None,
- ??.empty, Safe, true),
- #None)
-###generate1 Apply_Method: after cappend
-*)
+
  appendFormula 1 "2+ -1 + x = 2"; refFormula 1 (get_pos 1 1);
-(**)@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@;(**) 
-(*
->  appendFormula 1 "2+ -1 + x = 2";
-###generate1 Rewrite_Set': pos= ([1], Frm)
-##@cappend_atomic: pos =[1]
-##@cappend_atomic before cut_tree: loc =ScrState (["
-(e_, x + 1 = 2)","
-(v_, x)"],
- [R,L,R,L,L,R,R], Some e_,
- x + 1 + -1 * 2 = 0, Sundef, false)
-#@append_atomic: pos =[1]
-##@cappend_atomic after append: loc =(#None,
-#Some ScrState (["
-(e_, x + 1 = 2)","
-(v_, x)"],
- [R,L,R,L,L,R,R], Some e_,
- x + 1 + -1 * 2 = 0, Sundef, false))
-Exception- Bind raised
-*)
-
 
  moveDown 1 ([],Pbl); refFormula 1 ([1],Frm) (*x + 1 = 2*);
 >>>>>>> 1.8
@@ -375,8 +334,6 @@
  val ((pt,_),_) = get_calc 1;
  if "[x = 1]" = term2str (fst (get_obj g_result pt [])) then ()
  else raise error "auto-inform.sml: diff.behav.appendFormula: on Frm + equ 3";
-(**@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@**) 
- 
 
 
 "--------- appendFormula: on Res + NO deriv ----------------------";
@@ -486,7 +443,7 @@
  val str = pr_ptree pr_short pt;
  writeln str;
  if str=".    ----- pblobj -----\n1.   x + 1 = 2\n2.   x + 1 + -1 * 2 = 0\n2.1.   x + 1 + -1 * 2 = 0\n2.2.   -1 * 2 + (x + 1) = 0\n2.3.   -1 * 2 + (1 + x) = 0\n2.4.   1 + (-1 * 2 + x) = 0\n2.5.   1 + (-2 + x) = 0\n2.6.   1 + (-2 * 1 + x) = 0\n" then()
- else raise error "auto-inform.sml: diff.behav.replaceFormula: on Res + = 1";
+ else raise error "auto-inform.sml: diff.behav.replaceFormula: on Res += 1";
  autoCalculate 1 CompleteCalc;
  val ((pt,pos as(p,_)),_) = get_calc 1;
  if pos=([],Res)andalso"[x = 1]"=(term2str o fst)(get_obj g_result pt p)then()
@@ -496,7 +453,6 @@
 "--------- replaceFormula: on Res + = 1st Nd ---------------------";
 "--------- replaceFormula: on Res + = 1st Nd ---------------------";
 "--------- replaceFormula: on Res + = 1st Nd ---------------------";
-(**@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@(**) 
  states:=[];
  CalcTree [(["equality (x+1=2)", "solveFor x","solutions L"], 
 	    ("Test.thy", 
@@ -517,7 +473,6 @@
  val ((pt,pos as(p,_)),_) = get_calc 1;
  if pos=([],Res)andalso"[x = 1]"=(term2str o fst)(get_obj g_result pt p)then()
  else raise error "auto-inform.sml: diff.behav.replaceFormula: on Res + = 2";
-(**)@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@**) 
 
 
 "--------- replaceFormula: on Frm + = 1st Nd ---------------------";
@@ -547,7 +502,6 @@
 "--------- replaceFormula: cut calculation -----------------------";
 "--------- replaceFormula: cut calculation -----------------------";
 "--------- replaceFormula: cut calculation -----------------------";
-(**@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@(**) 
  states:=[];
  CalcTree [(["equality (x+1=2)", "solveFor x","solutions L"], 
 	    ("Test.thy", 
@@ -565,7 +519,6 @@
  writeln str;
  if p = ([1], Res) then ()
  else raise error "auto-inform.sml: diff.behav. cut calculation 2";
-(**)@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@**)