|
neuper@37906
|
1 |
(* use"systest/subp-rooteq.sml";
|
|
neuper@37906
|
2 |
use"subp-rooteq.sml";
|
|
neuper@37906
|
3 |
*)
|
|
neuper@37906
|
4 |
val c = [];
|
|
neuper@37906
|
5 |
|
|
neuper@37906
|
6 |
"---------------- solve_linear as rootpbl -----------------";
|
|
neuper@37906
|
7 |
"---------------- solve_plain_square as rootpbl -----------";
|
|
neuper@37906
|
8 |
"==========================================================";
|
|
neuper@37906
|
9 |
|
|
neuper@37906
|
10 |
|
|
neuper@37906
|
11 |
|
|
neuper@37906
|
12 |
|
|
neuper@37906
|
13 |
|
|
neuper@37906
|
14 |
|
|
neuper@37906
|
15 |
"---------------- solve_linear as rootpbl -----------------";
|
|
neuper@37906
|
16 |
"---------------- solve_linear as rootpbl -----------------";
|
|
neuper@37906
|
17 |
"---------------- solve_linear as rootpbl -----------------";
|
|
neuper@42124
|
18 |
val fmz = ["equality (1+-1*2+x=(0::real))",
|
|
neuper@37906
|
19 |
"solveFor x","solutions L"];
|
|
neuper@37906
|
20 |
val (dI',pI',mI') =
|
|
neuper@55279
|
21 |
("Test",["LINEAR","univariate","equation","test"],
|
|
neuper@37906
|
22 |
["Test","solve_linear"]);
|
|
neuper@37906
|
23 |
|
|
neuper@37906
|
24 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
|
neuper@37906
|
25 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
|
neuper@37906
|
26 |
(*val nxt = ("Add_Given",Add_Given "equality (x + #1 + #-1 * #2 = #0)")*)
|
|
neuper@37906
|
27 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
|
neuper@37906
|
28 |
(*val nxt = ("Add_Given",Add_Given "solveFor x") : string * tac*)
|
|
neuper@37906
|
29 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
|
neuper@37906
|
30 |
(*val nxt = ("Add_Find",Add_Find "solutions L") : string * tac*)
|
|
neuper@37906
|
31 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
|
neuper@38058
|
32 |
(*val nxt = ("Specify_Theory",Specify_Theory "Test") : string * tac*)
|
|
neuper@37906
|
33 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
|
neuper@37906
|
34 |
(*val nxt = ("Specify_Problem",Specify_Problem ["univariate","equation"])*)
|
|
neuper@37906
|
35 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
|
neuper@38058
|
36 |
(*val nxt = ("Specify_Method",Specify_Method ("Test","solve_linear"))*)
|
|
neuper@37906
|
37 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
|
neuper@38058
|
38 |
(*val nxt = ("Apply_Method",Apply_Method ("Test","solve_linear"))*)
|
|
neuper@37906
|
39 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
|
neuper@37906
|
40 |
(*val f = Form' (FormKF (~1,EdUndef,1,Nundef,"#1 + #-1 * #2 + x = #0"))
|
|
neuper@37906
|
41 |
val nxt = ("Rewrite_Set_Inst",Rewrite_Set_Inst ([#],"isolate_bdv"))*)
|
|
neuper@37906
|
42 |
|
|
neuper@37906
|
43 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
|
neuper@37906
|
44 |
(*val f = Form' (FormKF (~1,EdUndef,1,Nundef,"x = #0 + #-1 * (#1 + #-1 * #2)"))
|
|
neuper@37906
|
45 |
val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify") : string * tac*)
|
|
neuper@37906
|
46 |
|
|
neuper@37906
|
47 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
|
neuper@37906
|
48 |
(*val f = Form' (FormKF (~1,EdUndef,1,Nundef,"x = #1")) : mout val nxt = ("Check_Postcond",Check_Postcond ["univariate","equation"])*)
|
|
neuper@37906
|
49 |
|
|
neuper@37906
|
50 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
|
neuper@37906
|
51 |
(*val f = Form' (FormKF (~1,EdUndef,0,Nundef,"[x = #1]")) : mout
|
|
neuper@37906
|
52 |
val nxt = ("End_Proof'",End_Proof') : string * tac*)
|
|
neuper@37906
|
53 |
val Form' (FormKF (_,EdUndef,0,Nundef,res)) = f;
|
|
neuper@37906
|
54 |
if (snd nxt)=End_Proof' andalso res="[x = 1]" then ()
|
|
neuper@38031
|
55 |
else error "subp-rooteq.sml: new.behav. in solve_linear as rootpbl";
|
|
neuper@37906
|
56 |
|
|
neuper@37906
|
57 |
|
|
neuper@37906
|
58 |
"---------------- solve_plain_square as rootpbl -----------";
|
|
neuper@37906
|
59 |
"---------------- solve_plain_square as rootpbl -----------";
|
|
neuper@37906
|
60 |
"---------------- solve_plain_square as rootpbl -----------";
|
|
neuper@37906
|
61 |
val fmz = ["equality (9 + -1 * x ^^^ 2 = 0)","solveFor x",
|
|
neuper@37906
|
62 |
"solutions L"];
|
|
neuper@37906
|
63 |
val (dI',pI',mI') =
|
|
neuper@38058
|
64 |
("Test",["plain_square","univariate","equation","test"],
|
|
neuper@37906
|
65 |
["Test","solve_plain_square"]);
|
|
neuper@37906
|
66 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
|
neuper@37906
|
67 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
|
neuper@37906
|
68 |
|
|
neuper@37906
|
69 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
|
neuper@37906
|
70 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
|
neuper@37906
|
71 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
|
neuper@37906
|
72 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
|
neuper@37906
|
73 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
|
neuper@37906
|
74 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
|
neuper@37906
|
75 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
|
neuper@37906
|
76 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
|
neuper@37906
|
77 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
|
neuper@37906
|
78 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
|
neuper@37906
|
79 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
|
neuper@37906
|
80 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
|
neuper@37906
|
81 |
val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
|
|
neuper@37906
|
82 |
val Form' (FormKF (~1,EdUndef,0,Nundef,res)) = f;
|
|
neuper@37906
|
83 |
if snd nxt=End_Proof' andalso res="[x = -3, x = 3]" then ()
|
|
neuper@38031
|
84 |
else error "subp-rooteq.sml: new.behav. in solve_plain_square as rootpbl";
|
|
neuper@37906
|
85 |
|
|
neuper@37906
|
86 |
|
|
neuper@37906
|
87 |
|
|
neuper@37906
|
88 |
|