1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/sml/systest/stdinout.sml Thu Apr 17 18:01:03 2003 +0200
1.3 @@ -0,0 +1,183 @@
1.4 +(* use"test-FE-KE.sml";
1.5 + W.N.16.4.00
1.6 + *)
1.7 +
1.8 +Compiler.Control.Print.printDepth:=4; (*4 default*)
1.9 +
1.10 +(*#########################################################*)
1.11 +" _________________ stdin: tutor active_________________ ";
1.12 +proofs:=[]; dials:=([],[],[]);
1.13 +(*dmts:= [(PutRuleRes, Tt, Skip),(PutRule, St, SkipNo)];*)
1.14 +
1.15 +StdinSML 0 0 0 0 New_User;
1.16 +StdinSML 1 0 0 0 New_Proof;
1.17 +val fmz = ["equality (sqrt(9+4*x)=sqrt x + sqrt(5+x))",
1.18 + "solveFor x","errorBound (eps=0)",
1.19 + "solutions L"];
1.20 +val (dI',pI',mI') =
1.21 + ("Script.thy",["sqroot-test","univariate","equation"],
1.22 + ("Script.thy","sqrt-equ-test"));
1.23 +"--- s1 ---";
1.24 +val (_,uI,pI,acI,cI,dats,_)=StdinSML 1 1 1 1 (*@@@@@begin !!!!!*)
1.25 + (RuleFK (Init_Proof (fmz,(dI',pI',mI'))));
1.26 +"--- s2 ---";
1.27 +StdinSML 1 1 ~1 ~1 (Command Accept);
1.28 +(*RuleFK (Add_Given "equality (sqrt (#9 + #4 * x) = sqrt x + sqrt (#5 + x))"*)
1.29 +"--- s3 ---";
1.30 +StdinSML 1 1 ~2 ~2 (Command Accept);
1.31 +(*RuleFK (Add_Given "solveFor x")*)
1.32 +"--- s4 ---";
1.33 +StdinSML 1 1 ~3 ~3 (Command Accept);
1.34 +(*RuleFK (Add_Given "errorBound (eps = #0)")*)
1.35 +"--- s5 ---";
1.36 +StdinSML 1 1 ~4 ~4 (Command Accept);
1.37 +(*RuleFK (Add_Find "solutions L")*)
1.38 +"--- s6 ---";
1.39 +StdinSML 1 1 ~5 ~5 (Command Accept);
1.40 +(*RuleFK (Specify_Domain "Script.thy")*)
1.41 +"--- s7 ---";
1.42 +StdinSML 1 1 ~6 ~6 (Command Accept);
1.43 +(*RuleFK (Specify_Problem ["sqroot-test","univariate","equation"])*)
1.44 +"--- s8 ---";
1.45 +StdinSML 1 1 ~7 ~7 (Command Accept);
1.46 +(*RuleFK (Specify_Method ("Script.thy","sqrt-equ-test"))*)
1.47 +"--- s9 ---";
1.48 +StdinSML 1 1 ~8 ~8 (Command Accept);
1.49 +(*RuleFK (Apply_Method ("Script.thy","sqrt-equ-test"))*)
1.50 +"--- 1 ---";
1.51 +StdinSML 1 1 ~9 ~9 (Command Accept);
1.52 +(*RuleFK (Rewrite ("square_equation_left",""))*)
1.53 +"--- 2 ---";
1.54 +StdinSML 1 1 ~10 ~10 (Command Accept);
1.55 +(*RuleFK (Rewrite_Set "SqRoot_simplify")*)
1.56 +"--- 3 ---";
1.57 +StdinSML 1 1 ~11 ~11 (Command Accept);
1.58 +(*RuleFK (Rewrite_Set "rearrange_assoc")*)
1.59 +"--- 4 ---";
1.60 +StdinSML 1 1 ~12 ~12 (Command Accept);
1.61 +(*RuleFK (Rewrite_Set "isolate_root")*)
1.62 +"--- 5 ---";
1.63 +StdinSML 1 1 ~13 ~13 (Command Accept);
1.64 +(*RuleFK (Rewrite_Set "SqRoot_simplify")*)
1.65 +"--- 6 ---";
1.66 +StdinSML 1 1 ~14 ~14 (Command Accept);
1.67 +(*RuleFK (Rewrite ("square_equation_left",""))*)
1.68 +"--- 7 ---";
1.69 +StdinSML 1 1 ~15 ~15 (Command Accept);
1.70 +(*RuleFK (Rewrite_Set "SqRoot_simplify")*)
1.71 +"--- 8 ---";
1.72 +StdinSML 1 1 ~16 ~16 (Command Accept);
1.73 +(*RuleFK (Rewrite_Set "norm_equation")*)
1.74 +"--- 9 ---";
1.75 +StdinSML 1 1 ~17 ~17 (Command Accept);
1.76 +(*RuleFK (Rewrite_Set "SqRoot_simplify")*)
1.77 +"--- 10 ---";
1.78 +StdinSML 1 1 ~18 ~18 (Command Accept);
1.79 +(*RuleFK (Rewrite_Set_Inst ([("bdv","x")],"isolate_bdv"))*)
1.80 +"--- 11 ---";
1.81 +StdinSML 1 1 ~19 ~19 (Command Accept);
1.82 +(*RuleFK (Rewrite_Set "SqRoot_simplify")*)
1.83 +"--- 12 ---";
1.84 +val (begin,uI,pI,acI,cI,dats,eend) =
1.85 +StdinSML 1 1 ~20 ~20 (Command Accept);
1.86 +(*RuleFK (Check_Postcond ("Script.thy","sqrt-equ-test"))*)
1.87 +
1.88 +if (hd dats) <> (FormKF (~21,Protect,0,"[x = 4]"))
1.89 +then raise error "do_ + msteps input: not finished correctly"
1.90 +else "roo-equation, do_ + msteps input: OK";
1.91 +
1.92 +"==========================================================";
1.93 +writeln (get_history 1 1);
1.94 +"==========================================================";
1.95 +
1.96 +
1.97 +
1.98 +(*#########################################################*)
1.99 +" _________________ stdin: student active_________________ ";
1.100 +proofs:=[]; dials:=([],[],[]);
1.101 +(*dmts:= [(PutRuleRes, Tt, Skip),(PutRule, St, SkipNo)];*)
1.102 +
1.103 +StdinSML 0 0 0 0 New_User;
1.104 +StdinSML 1 0 0 0 New_Proof;
1.105 +val fmz = ["equality (sqrt(9+4*x)=sqrt x + sqrt(5+x))",
1.106 + "solveFor x","errorBound (eps=0)",
1.107 + "solutions L"];
1.108 +val (dI',pI',mI') =
1.109 + ("Script.thy",["sqroot-test","univariate","equation"],
1.110 + ("Script.thy","sqrt-equ-test"));
1.111 +"--- s1 ---";
1.112 +val (_,uI,pI,acI,cI,dats,_)=StdinSML 1 1 1 1
1.113 + (RuleFK (Init_Proof (fmz,(dI',pI',mI'))));
1.114 +"--- s2 ---";
1.115 +StdinSML 1 1 ~1 2 (RuleFK
1.116 +(Add_Given "equality (sqrt (9 + 4 * x) = sqrt x + sqrt (5 + x))"));
1.117 +"--- s3 ---";
1.118 +StdinSML 1 1 ~2 3 (RuleFK (Add_Given "solveFor x"));
1.119 +"--- s4 ---";
1.120 +StdinSML 1 1 ~3 4 (RuleFK (Add_Given "errorBound (eps = 0)"));
1.121 +"--- s5 ---";
1.122 +StdinSML 1 1 ~4 5 (RuleFK (Add_Find "solutions L"));
1.123 +"--- s6 ---";
1.124 +StdinSML 1 1 ~5 6 (RuleFK (Specify_Domain "Script.thy"));
1.125 +"--- s7 ---";
1.126 +StdinSML 1 1 ~6 7 (RuleFK
1.127 +(Specify_Problem ["sqroot-test","univariate","equation"]));
1.128 +"--- s8 ---";
1.129 +StdinSML 1 1 ~7 8 (RuleFK (Specify_Method ("Script.thy","sqrt-equ-test")));
1.130 +"--- s9 ---";
1.131 +StdinSML 1 1 ~8 9 (RuleFK (Apply_Method ("Script.thy","sqrt-equ-test")));
1.132 +"--- 1 ---";
1.133 +StdinSML 1 1 ~9 10 (RuleFK
1.134 +(Rewrite ("square_equation_left","")));
1.135 +"--- 2 ---";
1.136 +StdinSML 1 1 ~10 11 (RuleFK (Rewrite_Set "SqRoot_simplify"));
1.137 +"--- 3 ---";
1.138 +StdinSML 1 1 ~11 12 (RuleFK (Rewrite_Set "rearrange_assoc"));
1.139 +"--- 4 ---";
1.140 +StdinSML 1 1 ~12 13 (RuleFK (Rewrite_Set "isolate_root"));
1.141 +"--- 5 ---";
1.142 +StdinSML 1 1 ~13 14 (RuleFK (Rewrite_Set "SqRoot_simplify"));
1.143 +"--- 6 ---";
1.144 +StdinSML 1 1 ~14 15 (RuleFK
1.145 +(Rewrite ("square_equation_left","")));
1.146 +"--- 7 ---";
1.147 +StdinSML 1 1 ~15 16 (RuleFK (Rewrite_Set "SqRoot_simplify"));
1.148 +"--- 8 ---";
1.149 +StdinSML 1 1 ~16 17 (RuleFK (Rewrite_Set "norm_equation"));
1.150 +"--- 9 ---";
1.151 +StdinSML 1 1 ~17 18 (RuleFK (Rewrite_Set "SqRoot_simplify"));
1.152 +"--- 10 ---";
1.153 +StdinSML 1 1 ~18 19 (RuleFK
1.154 +(Rewrite_Set_Inst ([("bdv","x")],"isolate_bdv")));
1.155 +"--- 11 ---";
1.156 +StdinSML 1 1 ~19 20 (RuleFK (Rewrite_Set "SqRoot_simplify"));
1.157 +"--- 12 ---";
1.158 +val (begin,uI,pI,acI,cI,dats,eend) =
1.159 +StdinSML 1 1 ~20 21 (RuleFK
1.160 +(Check_Postcond ("Script.thy","sqrt-equ-test")));
1.161 +
1.162 +if (hd dats) <> (FormKF (~21,Protect,0,"[x = 4]"))
1.163 +then raise error "do_ + msteps input: not finished correctly"
1.164 +else "roo-equation, do_ + msteps input: OK";
1.165 +
1.166 +"==========================================================";
1.167 +writeln (get_history 1 1);
1.168 +"==========================================================";
1.169 +
1.170 +
1.171 +(*=========27.4.01===============================================*)
1.172 + proofs:= []; dials:=([],[],[]);
1.173 +" _________________ exampel [x=4]: Rules 4.2.01a________________ ";
1.174 +val (_,uI,0,0,[],[New_User],_) = StdinSML 0 0 0 0 New_User;
1.175 +val (_,_,pI,0,[],[New_Proof],_) = StdinSML uI 0 0 0 New_Proof;
1.176 +val fmz = ["equality (sqrt(9+4*x)=sqrt x + sqrt(5+x))",
1.177 + "solveFor x","errorBound (eps=0)",
1.178 + "solutions L"];
1.179 +val (dI',pI',mI') =
1.180 + ("SqRoot.thy",["sqroot-test","univariate","equation"],
1.181 + ("SqRoot.thy","squ-equ-test2"));
1.182 +StdinSML uI pI 1 1 (RuleFK (Init_Proof (fmz,(dI',pI',mI'))));
1.183 +
1.184 +StdinSML uI pI ~1 ~1 (Command Accept);
1.185 +
1.186 +StdinSML uI pI ~2 ~2 (RuleFK (Rewrite_Set "norm_equation"));