1.1 --- a/src/sml/ME/ctree.sml Sat Feb 19 18:57:29 2005 +0100
1.2 +++ b/src/sml/ME/ctree.sml Sat Feb 19 23:34:39 2005 +0100
1.3 @@ -823,13 +823,17 @@
1.4 (*.get from obj at pos by f : ppobj -> 'a.*)
1.5 fun get_obj f EmptyPtree _ = raise PTREE "get_obj f EmptyPtree"
1.6 | get_obj f (Nd (b, _)) [] = f b
1.7 - | get_obj f (Nd (b, bs)) (p::ps) =
1.8 + | get_obj f (Nd (b, bs)) (p::ps) =
1.9 +(* val (f, Nd (b, bs), (p::ps)) = (I, pt, p);
1.10 + *)
1.11 let val _ = (nth p bs) handle _ => raise PTREE ("get_obj: pos = "^
1.12 (ints2str' (p::ps))^" does not exist");
1.13 in (get_obj f (nth p bs) (ps:pos))
1.14 - handle _ => raise PTREE ("get_obj: at pos = "^
1.15 - (ints2str' (p::ps))^" wrong type of ppobj")
1.16 - (*FIXME: 'wrong type..' raised also if pos doesn't exist*)
1.17 + (*before WN050419: 'wrong type..' raised also if pos doesn't exist*)
1.18 + handle _ => raise PTREE (*"get_obj: at pos = "^
1.19 + (ints2str' (p::ps))^" wrong type of ppobj"*)
1.20 + ("get_obj: pos = "^
1.21 + (ints2str' (p::ps))^" does not exist")
1.22 end;
1.23 fun get_nd EmptyPtree _ = raise PTREE "get_nd EmptyPtree"
1.24 | get_nd n [] = n
1.25 @@ -1237,15 +1241,8 @@
1.26 (e_term,[]) Incomplete) pt p);
1.27
1.28
1.29 -
1.30 -(*.specialize 'take' for nodes of a ptree regarding Frm,Pbl,Met -- Res.*)
1.31 -(*WN050219 ?redesign with integrating the 'cuts' returned???*)
1.32 -fun take_nds (p:posel, bs: ptree list) Res = take (p, bs)
1.33 - | take_nds (1, b::_) p_ = [delete_result b []]
1.34 - | take_nds (p, bs: ptree list) p_ =
1.35 - (take (p-1, bs)) @ [delete_result (nth p bs) []];
1.36 -
1.37 -(*.cuts the nodes at a pos' + below + after ON SAME LEVEL until 'test_trans'
1.38 +(*.cuts the nodes at a pos (_NOT_ pos' because called by cappend_*..pos..)
1.39 + + below + after ON SAME LEVEL until 'test_trans'
1.40 and returns the pos' cut, found by get_allpos's + possibly head;
1.41 regards, if only Frm is present, but _NOT_ Res (*#*)
1.42 pos' list: for collecting during descent into ptree
1.43 @@ -1254,19 +1251,30 @@
1.44 pos' : ... below and after this
1.45 .*)
1.46 (*WN050219 ?redesign wrt cappend_*: regard only pos .v., _NOT_ pos' ????*)
1.47 -(*#################################################################(**)
1.48 +(*##GOON with this...##############################################(**)
1.49 fun cut_level (_:pos' list) (_:pos) EmptyPtree (_:pos') =
1.50 raise PTREE "cut_level EmptyPtree _"
1.51 | cut_level _ _ (Nd ( _, _)) ([],_) = raise PTREE "cut_level _ []"
1.52 +(* val (cuts, P, pt as Nd (b, bs), (p::[],p_)) = ([], [], pt, pos);
1.53 + *)
1.54 + | cut_level cuts P (pt as Nd (b, bs)) (1::[],p_) =
1.55 + if test_trans b
1.56 + then (Nd (b, []),
1.57 + cuts @
1.58 + (if p_ = Frm andalso (*#*) g_ostate b = Complete
1.59 + then [(P@[1],Res)] else ([]:pos' list)) @
1.60 + (*WN041020 here we assume what is presented on the worksheet ?!*)
1.61 + (get_allpos's (P, 1+1) bs))
1.62 + else (pt, cuts)
1.63
1.64 | cut_level cuts P (pt as Nd (b, bs)) (p::[],p_) =
1.65 if test_trans b
1.66 - then (Nd (b, take_nds (p:posel, bs) p_),
1.67 + then (Nd (b, take (p-1, bs)),
1.68 cuts @
1.69 (if p_ = Frm andalso (*#*) g_ostate b = Complete
1.70 then [(P@[p],Res)] else ([]:pos' list)) @
1.71 (*WN041020 here we assume what is presented on the worksheet ?!*)
1.72 - (get_allpos's (P, p+1) (takerest (p, bs))))
1.73 + (get_allpos's (P, p+1) (takerest (p-1, bs))))
1.74 else (pt, cuts)
1.75
1.76 | cut_level cuts P (Nd (b, bs)) ((p::ps),p_) =
1.77 @@ -1294,9 +1302,10 @@
1.78 then [] else [([], Res)])) end;
1.79 (*.cuts the nodes at and after the given pos' until 'not test_trans'
1.80 returns the pos's cut .*)
1.81 -(*####################################################################(**)
1.82 +(*##GOON with this...##############################################(**)
1.83 fun cut_tree _ (([],_):pos') = raise PTREE "cut_tree _ ([],_)"
1.84 -
1.85 +(* val (pt as Nd (b,_), pos as ([p],_)) = (pt, (p,Frm));
1.86 + *)
1.87 | cut_tree (pt as Nd (b,_)) (pos as ([p],_)) =
1.88 let val (pt', cuts') = cut_level ([]:pos' list) [] pt pos
1.89 val (pt'', cuts'') =
1.90 @@ -1306,15 +1315,19 @@
1.91 then [] else[([],Res)]))
1.92 else (pt', cuts')
1.93 in (pt'', cuts'') end
1.94 -
1.95 +(* val (p,p_) = ([3,1],Frm);
1.96 + *)
1.97 | cut_tree pt (p,p_) =
1.98 - let
1.99 - fun cutfn pt cuts (p,p_) =
1.100 - let val (pt', cuts') = cut_level [] (lev_up p) pt (p,p_)
1.101 + let val _= writeln("###cut_tree: at pos= "^pos'2str (p,p_));
1.102 + fun cutfn pt cuts (p,p_) =
1.103 +(* val (cuts) = ([]);
1.104 + *)
1.105 + let val _= writeln("###cutfn: at pos= "^pos'2str (p,p_));
1.106 + val (pt', cuts') = cut_level [] (lev_up p) pt (p,p_)
1.107 val (pt'', cuts'') =
1.108 - if test_trans (get_obj I pt p)
1.109 + (if test_trans (get_obj I pt p)
1.110 then (delete_result pt' [], cuts' @ [(lev_up p,Res)])
1.111 - else (pt', cuts')
1.112 + else (pt', cuts')) handle _ => (pt', [])
1.113
1.114 in if length cuts' > 0 andalso length p > 1
1.115 then cutfn pt' (cuts @ cuts') (lev_up p, Frm(*-->(p,Res)*))
1.116 @@ -1377,6 +1390,9 @@
1.117 result= (e_term,[]),
1.118 ostate= Incomplete}) pt p
1.119 );
1.120 +(* val (p,loc,f) = ([1], e_istate, str2term "x + 1 = 2");
1.121 + val (p,loc,f) = (fst p, e_istate, str2term "-1 + x = 0");
1.122 + *)
1.123 fun cappend_form pt p loc f =
1.124 (writeln("###cappend_form: pos ="^pos2str p);
1.125 apfst (append_form p loc f) (cut_tree pt (p,Frm))
2.1 --- a/src/sml/ROOT.ML Sat Feb 19 18:57:29 2005 +0100
2.2 +++ b/src/sml/ROOT.ML Sat Feb 19 23:34:39 2005 +0100
2.3 @@ -69,10 +69,7 @@
2.4 cd"~/proto2/isac/src/sml";
2.5 use"ROOT.ML";
2.6
2.7 - Compiler.Control.Print.printDepth:=9; (*4 default*)
2.8 -
2.9 - print_depth 11;step;print_depth 3;
2.10 -
2.11 +############## unten: (*systest/ctree.sml*) wegen cut_tree in ME/ctree !!!
2.12 *)
2.13
2.14 val version_kernel = "sml-050217a-fetchApplicableTactics";
2.15 @@ -162,7 +159,7 @@
2.16
2.17 cd "systest";
2.18 (*+ check kbtest/diffapp.sml for additional items in met-model*)
2.19 - (* use"ctree.sml";*)
2.20 + (** use"ctree.sml"; **)
2.21 use"calculate.sml";
2.22 use"details.sml"; (*can notyet ackn. 'Rewrite_Set "cancel"' *);
2.23 use"root-equ.sml";
2.24 @@ -215,12 +212,12 @@
2.25 use"logexp.sml";
2.26 use"poly.sml";
2.27 use"polyeq.sml"; (*TODO 31.b, n1., 44.a, 1.a~, 1.b (all'expanded')WN
2.28 - ? also check others without check 'diff.behav.'*)
2.29 + ? also check others without check 'diff.behav.'*);
2.30 use"rateq.sml" (*TODO //? 8.9.03: meOLD instead meNEW !!!*);
2.31 use"rational.sml" (*TODO add_fractions_p throws overflow-exn WN*);
2.32 use"rlang.sml"; (*WN.12.6.03: for TODOs search 'writeln',
2.33 for simplification search MG
2.34 - erls: 98a(1) 104a(1) 104a(2) 68a *)
2.35 + erls: 98a(1) 104a(1) 104a(2) 68a *);
2.36 use"root.sml";
2.37 use"rooteq.sml";
2.38 use"rootrateq.sml";
2.39 @@ -229,6 +226,7 @@
2.40 use"vect.sml";
2.41 use"wn.sml";
2.42 "******* kbtests complete *******";
2.43 + "******* build and tests complete *******";
2.44 cd "../";
2.45
2.46 (*
2.47 @@ -239,6 +237,6 @@
2.48 Compiler.Control.Print.printDepth:=4; (*4 default*)
2.49
2.50 *)
2.51 -(**=======================================================================*)
2.52 +(**=======================================================================*)
2.53
2.54 states:=[];
3.1 --- a/src/sml/systest/ctree.sml Sat Feb 19 18:57:29 2005 +0100
3.2 +++ b/src/sml/systest/ctree.sml Sat Feb 19 23:34:39 2005 +0100
3.3 @@ -13,6 +13,8 @@
3.4 "=====new ptree 2 miniscript with mini-subpbl ====================";
3.5 "-------------- cut_tree (intermedi.ptree: 3rd level)-------------";
3.6 "-------------- cappend (from ptree above)------------------------";
3.7 +"-------------- cappend minisubpbl -------------------------------";
3.8 +
3.9 "=====new ptree 3 ================================================";
3.10 "-------------- move_dn ------------------------------------------";
3.11 "-------------- move_dn: Frm -> Res ------------------------------";
3.12 @@ -40,6 +42,9 @@
3.13 "-----------------------------------------------------------------";
3.14
3.15
3.16 +
3.17 +
3.18 +
3.19 "=====new ptree 1 miniscript with mini-subpbl ====================";
3.20 "=====new ptree 1 miniscript with mini-subpbl ====================";
3.21 "=====new ptree 1 miniscript with mini-subpbl ====================";
3.22 @@ -59,16 +64,29 @@
3.23 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.24 (* (writeln o (itms2str thy)) (get_obj g_pbl pt (fst p));
3.25 *)
3.26 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.27 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.28 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.29 +(*###cappend_form: pos =[1] ... while calculating nxt, which pt is dropped
3.30 +val nxt = ("Apply_Method", Apply_Method ["Test", "squ-equ-test-subpbl1"])*)
3.31 +
3.32 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt(*cappend_form: pos =[1]*);
3.33 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt(*cappend_atomic: pos =[1]*);
3.34 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt(*cappend_atomic: pos =[2]*);
3.35 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;(*cappend_problem: pos =[3]*)
3.36 +
3.37 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.38 +(*val nxt = ("Add_Given", Add_Given "equality (-1 + x = 0)").....*)
3.39 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.40 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.41 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.42 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.43 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.44 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.45 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.46 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.47 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.48 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.49 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.50 +(*val nxt = ("Apply_Method", Apply_Method ["Test", "solve_linear"])*)
3.51 +
3.52 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt(*cappend_form: pos =[3,1]*);
3.53 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt(*cappend_atomic: pos =[3,1]*);
3.54 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.55 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.56 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.57 val Form' (FormKF (~1,EdUndef,0,Nundef,res)) = f;
3.58 if (snd nxt)=End_Proof' andalso res="[x = 1]" then ()
3.59 @@ -360,10 +378,99 @@
3.60
3.61
3.62
3.63 -writeln(pr_ptree pr_short pt');
3.64 +"-------------- cappend minisubpbl -------------------------------";
3.65 +"-------------- cappend minisubpbl -------------------------------";
3.66 +"-------------- cappend minisubpbl -------------------------------";
3.67 +"=====new ptree 1 miniscript with mini-subpbl ====================";
3.68 +val fmz = ["equality (x+1=2)",
3.69 + "solveFor x","solutions L"];
3.70 +val (dI',pI',mI') =
3.71 + ("Test.thy",["sqroot-test","univariate","equation","test"],
3.72 + ["Test","squ-equ-test-subpbl1"]);
3.73 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
3.74 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.75 +(* nxt = Add_Given "equality (x + 1 = 2)"
3.76 + (writeln o (itms2str thy)) (get_obj g_pbl pt (fst p));
3.77 + *)
3.78 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.79 +(* (writeln o (itms2str thy)) (get_obj g_pbl pt (fst p));
3.80 + *)
3.81 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.82 +(* (writeln o (itms2str thy)) (get_obj g_pbl pt (fst p));
3.83 + *)
3.84 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.85 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.86 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.87 +(*###cappend_form: pos =[1] ... while calculating nxt, which pt is dropped
3.88 +val nxt = ("Apply_Method", Apply_Method ["Test", "squ-equ-test-subpbl1"])*)
3.89
3.90 -print_depth 99;cuts;print_depth 3;
3.91 -
3.92 +(*val (p,_,f,nxt,_,pt) = me nxt p [1] pt(**)cappend_form: pos =[1]*);
3.93 +val p = ([1], Frm);
3.94 +val (pt,cuts) = cappend_form pt (fst p) e_istate (str2term "x + 1 = 2");
3.95 +val form = get_obj g_form pt (fst p);
3.96 +val (res,_) = get_obj g_result pt (fst p);
3.97 +if term2str form = "x + 1 = 2" andalso res = e_term then () else
3.98 +raise error "ctree.sml, diff.behav. cappend minisubpbl ([1],Frm)";
3.99 +if not (existpt ((lev_on o fst) p) pt) then () else
3.100 +raise error "ctree.sml, diff.behav. cappend minisubpbl ([1],Frm) nxt";
3.101 +
3.102 +(*val (p,_,f,nxt,_,pt) = me nxt p [1] pt(**)cappend_atomic: pos =[1]*);
3.103 +val p = ([1], Res);
3.104 +val (pt,cuts) =
3.105 + cappend_atomic pt (fst p) e_istate (str2term "x + 1 = 2")
3.106 + Empty_Tac (str2term "x + 1 + -1 * 2 = 0",[]) Incomplete;
3.107 +val form = get_obj g_form pt (fst p);
3.108 +val (res,_) = get_obj g_result pt (fst p);
3.109 +if term2str form = "x + 1 = 2" andalso term2str res = "x + 1 + -1 * 2 = 0"
3.110 +then () else raise error "ctree.sml, diff.behav. cappend minisubpbl ([1],Res)";
3.111 +if not (existpt ((lev_on o fst) p) pt) then () else
3.112 +raise error "ctree.sml, diff.behav. cappend minisubpbl ([1],Res) nxt";
3.113 +
3.114 +(*val (p,_,f,nxt,_,pt) = me nxt p [1] pt(**)cappend_atomic: pos =[2]*);
3.115 +val p = ([2], Res);
3.116 +val (pt,cuts) =
3.117 + cappend_atomic pt (fst p) e_istate (str2term "x + 1 + -1 * 2 = 0")
3.118 + Empty_Tac (str2term "-1 + x = 0",[]) Incomplete;
3.119 +val form = get_obj g_form pt (fst p);
3.120 +val (res,_) = get_obj g_result pt (fst p);
3.121 +if term2str form = "x + 1 + -1 * 2 = 0" andalso term2str res = "-1 + x = 0"
3.122 +then () else raise error "ctree.sml, diff.behav. cappend minisubpbl ([2],Res)";
3.123 +if not (existpt ((lev_on o fst) p) pt) then () else
3.124 +raise error "ctree.sml, diff.behav. cappend minisubpbl ([2],Res) nxt";
3.125 +
3.126 +
3.127 +(*val (p,_,f,nxt,_,pt) = me nxt p [1] pt;(**)cappend_problem: pos =[3]*)
3.128 +val p = ([3], Pbl);
3.129 +val (pt,cuts) = cappend_problem pt (fst p) e_istate e_fmz ([],e_spec,e_term);
3.130 +if is_pblobj (get_obj I pt (fst p)) then () else
3.131 +raise error "ctree.sml, diff.behav. cappend minisubpbl ([3],Pbl)";
3.132 +if not (existpt ((lev_on o fst) p) pt) then () else
3.133 +raise error "ctree.sml, diff.behav. cappend minisubpbl ([3],Pbl) nxt";
3.134 +
3.135 +(* ...complete calchead skipped...*)
3.136 +
3.137 +(*val (p,_,f,nxt,_,pt) = me nxt p [1] pt(**)cappend_form: pos =[3,1]*);
3.138 +val p = ([3, 1], Frm);
3.139 +val (pt,cuts) = cappend_form pt (fst p) e_istate (str2term "-1 + x = 0");
3.140 +val form = get_obj g_form pt (fst p);
3.141 +val (res,_) = get_obj g_result pt (fst p);
3.142 +if term2str form = "-1 + x = 0" andalso res = e_term then () else
3.143 +raise error "ctree.sml, diff.behav. cappend minisubpbl ([3,1],Frm)";
3.144 +if not (existpt ((lev_on o fst) p) pt) then () else
3.145 +raise error "ctree.sml, diff.behav. cappend minisubpbl ([3,1],Frm) nxt";
3.146 +
3.147 +(*val (p,_,f,nxt,_,pt) = me nxt p [1] pt;(**)cappend_atomic: pos =[3,1]*)
3.148 +val p = ([3, 1], Res);
3.149 +val (pt,cuts) =
3.150 + cappend_atomic pt (fst p) e_istate (str2term "-1 + x = 0")
3.151 + Empty_Tac (str2term "x = 0 + -1 * -1",[]) Incomplete;
3.152 +val form = get_obj g_form pt (fst p);
3.153 +val (res,_) = get_obj g_result pt (fst p);
3.154 +if term2str form = "-1 + x = 0" andalso term2str res = "x = 0 + -1 * -1" then()
3.155 +else raise error "ctree.sml, diff.behav. cappend minisubpbl ([3,1],Res)";
3.156 +if not (existpt ((lev_on o fst) p) pt) then () else
3.157 +raise error "ctree.sml, diff.behav. cappend minisubpbl ([3,1],Res) nxt";
3.158 +
3.159
3.160
3.161 "=====new ptree 3 ================================================";