1 (* use"systest/subp-rooteq.sml";
6 "---------------- solve_linear as rootpbl -----------------";
7 "---------------- solve_plain_square as rootpbl -----------";
8 "==========================================================";
15 "---------------- solve_linear as rootpbl -----------------";
16 "---------------- solve_linear as rootpbl -----------------";
17 "---------------- solve_linear as rootpbl -----------------";
18 val fmz = ["equality (1+-1*2+x=(0::real))",
19 "solveFor x", "solutions L"];
21 ("Test",["LINEAR", "univariate", "equation", "test"],
22 ["Test", "solve_linear"]);
24 val (p,_,f,nxt,_,pt) = Test_Code.init_calc @{context} [(fmz, (dI',pI',mI'))];
25 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
26 (*val nxt = ("Add_Given",Add_Given "equality (x + #1 + #-1 * #2 = #0)")*)
27 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
28 (*val nxt = ("Add_Given",Add_Given "solveFor x") : string * tac*)
29 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
30 (*val nxt = ("Add_Find",Add_Find "solutions L") : string * tac*)
31 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
32 (*val nxt = ("Specify_Theory",Specify_Theory "Test") : string * tac*)
33 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
34 (*val nxt = ("Specify_Problem",Specify_Problem ["univariate", "equation"])*)
35 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
36 (*val nxt = ("Specify_Method",Specify_Method ("Test", "solve_linear"))*)
37 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
38 (*val nxt = ("Apply_Method",Apply_Method ("Test", "solve_linear"))*)
39 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
40 (*val f = Form' (Test_Out.FormKF (~1,EdUndef,1,Nundef,"#1 + #-1 * #2 + x = #0"))
41 val nxt = ("Rewrite_Set_Inst",Rewrite_Set_Inst ([#],"isolate_bdv"))*)
43 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
44 (*val f = Form' (Test_Out.FormKF (~1,EdUndef,1,Nundef,"x = #0 + #-1 * (#1 + #-1 * #2)"))
45 val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify") : string * tac*)
47 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
48 (*val f = Form' (Test_Out.FormKF (~1,EdUndef,1,Nundef,"x = #1")) : mout val nxt = ("Check_Postcond",Check_Postcond ["univariate", "equation"])*)
50 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
51 (*val f = Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,"[x = #1]")) : mout
52 val nxt = ("End_Proof'",End_Proof') : string * tac*)
53 val Form' (Test_Out.FormKF (_,EdUndef,0,Nundef,res)) = f;
54 if (snd nxt)=End_Proof' andalso res="[x = 1]" then ()
55 else error "subp-rooteq.sml: new.behav. in solve_linear as rootpbl";
58 "---------------- solve_plain_square as rootpbl -----------";
59 "---------------- solve_plain_square as rootpbl -----------";
60 "---------------- solve_plain_square as rootpbl -----------";
61 val fmz = ["equality (9 + -1 * x \<up> 2 = 0)", "solveFor x",
64 ("Test",["plain_square", "univariate", "equation", "test"],
65 ["Test", "solve_plain_square"]);
66 val (p,_,f,nxt,_,pt) = Test_Code.init_calc @{context} [(fmz, (dI',pI',mI'))];
67 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
69 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
70 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
71 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
72 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
73 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
74 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
75 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
76 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
77 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
78 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
79 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
80 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
81 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
82 val Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,res)) = f;
83 if snd nxt=End_Proof' andalso res="[x = -3, x = 3]" then ()
84 else error "subp-rooteq.sml: new.behav. in solve_plain_square as rootpbl";